diff options
Diffstat (limited to 'src/smt_util')
-rw-r--r-- | src/smt_util/Makefile.am | 30 | ||||
-rw-r--r-- | src/smt_util/boolean_simplification.cpp | 65 | ||||
-rw-r--r-- | src/smt_util/boolean_simplification.h | 234 | ||||
-rw-r--r-- | src/smt_util/command.cpp | 1848 | ||||
-rw-r--r-- | src/smt_util/command.h | 904 | ||||
-rw-r--r-- | src/smt_util/command.i | 77 | ||||
-rw-r--r-- | src/smt_util/dump.cpp | 24 | ||||
-rw-r--r-- | src/smt_util/dump.h | 117 | ||||
-rw-r--r-- | src/smt_util/ite_removal.cpp | 192 | ||||
-rw-r--r-- | src/smt_util/ite_removal.h | 93 | ||||
-rw-r--r-- | src/smt_util/lemma_input_channel.h | 39 | ||||
-rw-r--r-- | src/smt_util/lemma_output_channel.h | 47 | ||||
-rw-r--r-- | src/smt_util/model.cpp | 53 | ||||
-rw-r--r-- | src/smt_util/model.h | 78 | ||||
-rw-r--r-- | src/smt_util/nary_builder.cpp | 200 | ||||
-rw-r--r-- | src/smt_util/nary_builder.h | 55 | ||||
-rw-r--r-- | src/smt_util/node_visitor.h | 120 |
17 files changed, 4176 insertions, 0 deletions
diff --git a/src/smt_util/Makefile.am b/src/smt_util/Makefile.am new file mode 100644 index 000000000..3b457f641 --- /dev/null +++ b/src/smt_util/Makefile.am @@ -0,0 +1,30 @@ +AM_CPPFLAGS = \ + -D__BUILDING_CVC4LIB \ + -I@builddir@/.. -I@srcdir@/../include -I@srcdir@/.. +AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN) + +noinst_LTLIBRARIES = libsmtutil.la + +libsmtutil_la_SOURCES = \ + Makefile.am \ + Makefile.in \ + boolean_simplification.cpp \ + boolean_simplification.h \ + command.cpp \ + command.h \ + dump.h \ + dump.cpp \ + lemma_input_channel.h \ + lemma_output_channel.h \ + ite_removal.cpp \ + ite_removal.h \ + model.cpp \ + model.h \ + nary_builder.cpp \ + nary_builder.h \ + node_visitor.h + + +EXTRA_DIST = \ + command.i + diff --git a/src/smt_util/boolean_simplification.cpp b/src/smt_util/boolean_simplification.cpp new file mode 100644 index 000000000..fba431350 --- /dev/null +++ b/src/smt_util/boolean_simplification.cpp @@ -0,0 +1,65 @@ +/********************* */ +/*! \file boolean_simplification.cpp + ** \verbatim + ** Original author: Morgan Deters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2014 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Simple routines for Boolean simplification + ** + ** Simple, commonly-used routines for Boolean simplification. + **/ + +#include "smt_util/boolean_simplification.h" + +namespace CVC4 { + +bool +BooleanSimplification::push_back_associative_commute_recursive + (Node n, std::vector<Node>& buffer, Kind k, Kind notK, bool negateNode) + throw(AssertionException) { + Node::iterator i = n.begin(), end = n.end(); + for(; i != end; ++i){ + Node child = *i; + if(child.getKind() == k){ + if(! push_back_associative_commute_recursive(child, buffer, k, notK, negateNode)) { + return false; + } + }else if(child.getKind() == kind::NOT && child[0].getKind() == notK){ + if(! push_back_associative_commute_recursive(child[0], buffer, notK, k, !negateNode)) { + return false; + } + }else{ + if(negateNode){ + if(child.isConst()) { + if((k == kind::AND && child.getConst<bool>()) || + (k == kind::OR && !child.getConst<bool>())) { + buffer.clear(); + buffer.push_back(negate(child)); + return false; + } + } else { + buffer.push_back(negate(child)); + } + }else{ + if(child.isConst()) { + if((k == kind::OR && child.getConst<bool>()) || + (k == kind::AND && !child.getConst<bool>())) { + buffer.clear(); + buffer.push_back(child); + return false; + } + } else { + buffer.push_back(child); + } + } + } + } + return true; +}/* BooleanSimplification::push_back_associative_commute_recursive() */ + +}/* CVC4 namespace */ diff --git a/src/smt_util/boolean_simplification.h b/src/smt_util/boolean_simplification.h new file mode 100644 index 000000000..2732eaea7 --- /dev/null +++ b/src/smt_util/boolean_simplification.h @@ -0,0 +1,234 @@ +/********************* */ +/*! \file boolean_simplification.h + ** \verbatim + ** Original author: Tim King + ** Major contributors: Morgan Deters + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2014 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Simple routines for Boolean simplification + ** + ** Simple, commonly-used routines for Boolean simplification. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__BOOLEAN_SIMPLIFICATION_H +#define __CVC4__BOOLEAN_SIMPLIFICATION_H + +#include <vector> +#include <algorithm> + +#include "base/cvc4_assert.h" +#include "expr/expr_manager_scope.h" +#include "expr/node.h" + +namespace CVC4 { + +/** + * A class to contain a number of useful functions for simple + * simplification of nodes. One never uses it as an object (and + * it cannot be constructed). It is used as a namespace. + */ +class BooleanSimplification { + // cannot construct one of these + BooleanSimplification() CVC4_UNUSED; + BooleanSimplification(const BooleanSimplification&) CVC4_UNUSED; + + static bool push_back_associative_commute_recursive + (Node n, std::vector<Node>& buffer, Kind k, Kind notK, bool negateNode) + throw(AssertionException) CVC4_WARN_UNUSED_RESULT; + +public: + + /** + * The threshold for removing duplicates. (See removeDuplicates().) + */ + static const uint32_t DUPLICATE_REMOVAL_THRESHOLD = 10; + + /** + * Remove duplicate nodes from a vector, modifying it in-place. + * If the vector has size >= DUPLICATE_REMOVAL_THRESHOLD, this + * function is a no-op. + */ + static void removeDuplicates(std::vector<Node>& buffer) + throw(AssertionException) { + if(buffer.size() < DUPLICATE_REMOVAL_THRESHOLD) { + std::sort(buffer.begin(), buffer.end()); + std::vector<Node>::iterator new_end = + std::unique(buffer.begin(), buffer.end()); + buffer.erase(new_end, buffer.end()); + } + } + + /** + * Takes a node with kind AND, collapses all AND and (NOT OR)-kinded + * children of it (as far as possible---see + * push_back_associative_commute()), removes duplicates, and returns + * the resulting Node. + */ + static Node simplifyConflict(Node andNode) throw(AssertionException) { + AssertArgument(!andNode.isNull(), andNode); + AssertArgument(andNode.getKind() == kind::AND, andNode); + + std::vector<Node> buffer; + push_back_associative_commute(andNode, buffer, kind::AND, kind::OR); + + removeDuplicates(buffer); + + if(buffer.size() == 1) { + return buffer[0]; + } + + NodeBuilder<> nb(kind::AND); + nb.append(buffer); + return nb; + } + + /** + * Takes a node with kind OR, collapses all OR and (NOT AND)-kinded + * children of it (as far as possible---see + * push_back_associative_commute()), removes duplicates, and returns + * the resulting Node. + */ + static Node simplifyClause(Node orNode) throw(AssertionException) { + AssertArgument(!orNode.isNull(), orNode); + AssertArgument(orNode.getKind() == kind::OR, orNode); + + std::vector<Node> buffer; + push_back_associative_commute(orNode, buffer, kind::OR, kind::AND); + + removeDuplicates(buffer); + + Assert(buffer.size() > 0); + if(buffer.size() == 1) { + return buffer[0]; + } + + NodeBuilder<> nb(kind::OR); + nb.append(buffer); + return nb; + } + + /** + * Takes a node with kind IMPLIES, converts it to an OR, then + * simplifies the result with simplifyClause(). + * + * The input doesn't actually have to be Horn, it seems, but that's + * the common case(?), hence the name. + */ + static Node simplifyHornClause(Node implication) throw(AssertionException) { + AssertArgument(implication.getKind() == kind::IMPLIES, implication); + + TNode left = implication[0]; + TNode right = implication[1]; + + Node notLeft = negate(left); + Node clause = NodeBuilder<2>(kind::OR) << notLeft << right; + + return simplifyClause(clause); + } + + /** + * Aids in reforming a node. Takes a node of (N-ary) kind k and + * copies its children into an output vector, collapsing its k-kinded + * children into it. Also collapses negations of notK. For example: + * + * push_back_associative_commute( [OR [OR a b] [OR b c d] [NOT [AND e f]]], + * buffer, kind::OR, kind::AND ) + * yields a "buffer" vector of [a b b c d e f] + * + * @param n the node to operate upon + * @param buffer the output vector (must be empty on entry) + * @param k the kind to collapse (should equal the kind of node n) + * @param notK the "negation" of kind k (e.g. OR's negation is AND), + * or kind::UNDEFINED_KIND if none. + * @param negateChildren true if the children of the resulting node + * (that is, the elements in buffer) should all be negated; you want + * this if e.g. you're simplifying the (OR...) in (NOT (OR...)), + * intending to make the result an AND. + */ + static inline void + push_back_associative_commute(Node n, std::vector<Node>& buffer, + Kind k, Kind notK, bool negateChildren = false) + throw(AssertionException) { + AssertArgument(buffer.empty(), buffer); + AssertArgument(!n.isNull(), n); + AssertArgument(k != kind::UNDEFINED_KIND && k != kind::NULL_EXPR, k); + AssertArgument(notK != kind::NULL_EXPR, notK); + AssertArgument(n.getKind() == k, n, + "expected node to have kind %s", kindToString(k).c_str()); + + bool b CVC4_UNUSED = + push_back_associative_commute_recursive(n, buffer, k, notK, false); + + if(buffer.size() == 0) { + // all the TRUEs for an AND (resp FALSEs for an OR) were simplified away + buffer.push_back(NodeManager::currentNM()->mkConst(k == kind::AND ? true : false)); + } + }/* push_back_associative_commute() */ + + /** + * Negates a node, doing all the double-negation elimination + * that's possible. + * + * @param n the node to negate (cannot be the null node) + */ + static Node negate(TNode n) throw(AssertionException) { + AssertArgument(!n.isNull(), n); + + bool polarity = true; + TNode base = n; + while(base.getKind() == kind::NOT){ + base = base[0]; + polarity = !polarity; + } + if(n.isConst()) { + return NodeManager::currentNM()->mkConst(!n.getConst<bool>()); + } + if(polarity){ + return base.notNode(); + }else{ + return base; + } + } + + /** + * Negates an Expr, doing all the double-negation elimination that's + * possible. + * + * @param e the Expr to negate (cannot be the null Expr) + */ + static Expr negate(Expr e) throw(AssertionException) { + ExprManagerScope ems(e); + return negate(Node::fromExpr(e)).toExpr(); + } + + /** + * Simplify an OR, AND, or IMPLIES. This function is the identity + * for all other kinds. + */ + inline static Node simplify(TNode n) throw(AssertionException) { + switch(n.getKind()) { + case kind::AND: + return simplifyConflict(n); + + case kind::OR: + return simplifyClause(n); + + case kind::IMPLIES: + return simplifyHornClause(n); + + default: + return n; + } + } + +};/* class BooleanSimplification */ + +}/* CVC4 namespace */ + +#endif /* __CVC4__BOOLEAN_SIMPLIFICATION_H */ diff --git a/src/smt_util/command.cpp b/src/smt_util/command.cpp new file mode 100644 index 000000000..464a2e0aa --- /dev/null +++ b/src/smt_util/command.cpp @@ -0,0 +1,1848 @@ +/********************* */ +/*! \file command.cpp + ** \verbatim + ** Original author: Morgan Deters + ** Major contributors: none + ** Minor contributors (to current version): Kshitij Bansal, Dejan Jovanovic, Andrew Reynolds, Francois Bobot + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2014 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Implementation of command objects. + ** + ** Implementation of command objects. + **/ + +#include "smt_util/command.h" + +#include <exception> +#include <iostream> +#include <iterator> +#include <sstream> +#include <utility> +#include <vector> + +#include "base/output.h" +#include "expr/node.h" +#include "expr/sexpr.h" +#include "options/options.h" +#include "options/smt_options.h" +#include "printer/printer.h" +#include "smt/smt_engine.h" +#include "smt/smt_engine_scope.h" +#include "smt_util/dump.h" +#include "smt_util/model.h" + +using namespace std; + +namespace CVC4 { + +const int CommandPrintSuccess::s_iosIndex = std::ios_base::xalloc(); +const CommandSuccess* CommandSuccess::s_instance = new CommandSuccess(); +const CommandInterrupted* CommandInterrupted::s_instance = new CommandInterrupted(); + +std::ostream& operator<<(std::ostream& out, const Command& c) throw() { + c.toStream(out, + Node::setdepth::getDepth(out), + Node::printtypes::getPrintTypes(out), + Node::dag::getDag(out), + Node::setlanguage::getLanguage(out)); + return out; +} + +ostream& operator<<(ostream& out, const Command* c) throw() { + if(c == NULL) { + out << "null"; + } else { + out << *c; + } + return out; +} + +std::ostream& operator<<(std::ostream& out, const CommandStatus& s) throw() { + s.toStream(out, Node::setlanguage::getLanguage(out)); + return out; +} + +ostream& operator<<(ostream& out, const CommandStatus* s) throw() { + if(s == NULL) { + out << "null"; + } else { + out << *s; + } + return out; +} + +/* class Command */ + +Command::Command() throw() : d_commandStatus(NULL), d_muted(false) { +} + +Command::Command(const Command& cmd) { + d_commandStatus = (cmd.d_commandStatus == NULL) ? NULL : &cmd.d_commandStatus->clone(); + d_muted = cmd.d_muted; +} + +Command::~Command() throw() { + if(d_commandStatus != NULL && d_commandStatus != CommandSuccess::instance()) { + delete d_commandStatus; + } +} + +bool Command::ok() const throw() { + // either we haven't run the command yet, or it ran successfully + return d_commandStatus == NULL || dynamic_cast<const CommandSuccess*>(d_commandStatus) != NULL; +} + +bool Command::fail() const throw() { + return d_commandStatus != NULL && dynamic_cast<const CommandFailure*>(d_commandStatus) != NULL; +} + +bool Command::interrupted() const throw() { + return d_commandStatus != NULL && dynamic_cast<const CommandInterrupted*>(d_commandStatus) != NULL; +} + +void Command::invoke(SmtEngine* smtEngine, std::ostream& out) throw() { + invoke(smtEngine); + if(!(isMuted() && ok())) { + printResult(out, smtEngine->getOption("command-verbosity:" + getCommandName()).getIntegerValue().toUnsignedInt()); + } +} + +std::string Command::toString() const throw() { + std::stringstream ss; + toStream(ss); + return ss.str(); +} + +void Command::toStream(std::ostream& out, int toDepth, bool types, size_t dag, + OutputLanguage language) const throw() { + Printer::getPrinter(language)->toStream(out, this, toDepth, types, dag); +} + +void CommandStatus::toStream(std::ostream& out, OutputLanguage language) const throw() { + Printer::getPrinter(language)->toStream(out, this); +} + +void Command::printResult(std::ostream& out, uint32_t verbosity) const throw() { + if(d_commandStatus != NULL) { + if((!ok() && verbosity >= 1) || verbosity >= 2) { + out << *d_commandStatus; + } + } +} + +/* class EmptyCommand */ + +EmptyCommand::EmptyCommand(std::string name) throw() : + d_name(name) { +} + +std::string EmptyCommand::getName() const throw() { + return d_name; +} + +void EmptyCommand::invoke(SmtEngine* smtEngine) throw() { + /* empty commands have no implementation */ + d_commandStatus = CommandSuccess::instance(); +} + +Command* EmptyCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + return new EmptyCommand(d_name); +} + +Command* EmptyCommand::clone() const { + return new EmptyCommand(d_name); +} + +std::string EmptyCommand::getCommandName() const throw() { + return "empty"; +} + +/* class EchoCommand */ + +EchoCommand::EchoCommand(std::string output) throw() : + d_output(output) { +} + +std::string EchoCommand::getOutput() const throw() { + return d_output; +} + +void EchoCommand::invoke(SmtEngine* smtEngine) throw() { + /* we don't have an output stream here, nothing to do */ + d_commandStatus = CommandSuccess::instance(); +} + +void EchoCommand::invoke(SmtEngine* smtEngine, std::ostream& out) throw() { + out << d_output << std::endl; + d_commandStatus = CommandSuccess::instance(); + printResult(out, smtEngine->getOption("command-verbosity:" + getCommandName()).getIntegerValue().toUnsignedInt()); +} + +Command* EchoCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + return new EchoCommand(d_output); +} + +Command* EchoCommand::clone() const { + return new EchoCommand(d_output); +} + +std::string EchoCommand::getCommandName() const throw() { + return "echo"; +} + +/* class AssertCommand */ + +AssertCommand::AssertCommand(const Expr& e, bool inUnsatCore) throw() : + d_expr(e), d_inUnsatCore(inUnsatCore) { +} + +Expr AssertCommand::getExpr() const throw() { + return d_expr; +} + +void AssertCommand::invoke(SmtEngine* smtEngine) throw() { + try { + smtEngine->assertFormula(d_expr, d_inUnsatCore); + d_commandStatus = CommandSuccess::instance(); + } catch(UnsafeInterruptException& e) { + d_commandStatus = new CommandInterrupted(); + } catch(exception& e) { + d_commandStatus = new CommandFailure(e.what()); + } +} + +Command* AssertCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + return new AssertCommand(d_expr.exportTo(exprManager, variableMap), d_inUnsatCore); +} + +Command* AssertCommand::clone() const { + return new AssertCommand(d_expr, d_inUnsatCore); +} + +std::string AssertCommand::getCommandName() const throw() { + return "assert"; +} + +/* class PushCommand */ + +void PushCommand::invoke(SmtEngine* smtEngine) throw() { + try { + smtEngine->push(); + d_commandStatus = CommandSuccess::instance(); + } catch(UnsafeInterruptException& e) { + d_commandStatus = new CommandInterrupted(); + } catch(exception& e) { + d_commandStatus = new CommandFailure(e.what()); + } +} + +Command* PushCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + return new PushCommand(); +} + +Command* PushCommand::clone() const { + return new PushCommand(); +} + +std::string PushCommand::getCommandName() const throw() { + return "push"; +} + +/* class PopCommand */ + +void PopCommand::invoke(SmtEngine* smtEngine) throw() { + try { + smtEngine->pop(); + d_commandStatus = CommandSuccess::instance(); + } catch(UnsafeInterruptException& e) { + d_commandStatus = new CommandInterrupted(); + } catch(exception& e) { + d_commandStatus = new CommandFailure(e.what()); + } +} + +Command* PopCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + return new PopCommand(); +} + +Command* PopCommand::clone() const { + return new PopCommand(); +} + +std::string PopCommand::getCommandName() const throw() { + return "pop"; +} + +/* class CheckSatCommand */ + +CheckSatCommand::CheckSatCommand() throw() : + d_expr() { +} + +CheckSatCommand::CheckSatCommand(const Expr& expr, bool inUnsatCore) throw() : + d_expr(expr), d_inUnsatCore(inUnsatCore) { +} + +Expr CheckSatCommand::getExpr() const throw() { + return d_expr; +} + +void CheckSatCommand::invoke(SmtEngine* smtEngine) throw() { + try { + d_result = smtEngine->checkSat(d_expr); + d_commandStatus = CommandSuccess::instance(); + } catch(exception& e) { + d_commandStatus = new CommandFailure(e.what()); + } +} + +Result CheckSatCommand::getResult() const throw() { + return d_result; +} + +void CheckSatCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() { + if(! ok()) { + this->Command::printResult(out, verbosity); + } else { + out << d_result << endl; + } +} + +Command* CheckSatCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + CheckSatCommand* c = new CheckSatCommand(d_expr.exportTo(exprManager, variableMap), d_inUnsatCore); + c->d_result = d_result; + return c; +} + +Command* CheckSatCommand::clone() const { + CheckSatCommand* c = new CheckSatCommand(d_expr, d_inUnsatCore); + c->d_result = d_result; + return c; +} + +std::string CheckSatCommand::getCommandName() const throw() { + return "check-sat"; +} + +/* class QueryCommand */ + +QueryCommand::QueryCommand(const Expr& e, bool inUnsatCore) throw() : + d_expr(e), d_inUnsatCore(inUnsatCore) { +} + +Expr QueryCommand::getExpr() const throw() { + return d_expr; +} + +void QueryCommand::invoke(SmtEngine* smtEngine) throw() { + try { + d_result = smtEngine->query(d_expr); + d_commandStatus = CommandSuccess::instance(); + } catch(exception& e) { + d_commandStatus = new CommandFailure(e.what()); + } +} + +Result QueryCommand::getResult() const throw() { + return d_result; +} + +void QueryCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() { + if(! ok()) { + this->Command::printResult(out, verbosity); + } else { + out << d_result << endl; + } +} + +Command* QueryCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + QueryCommand* c = new QueryCommand(d_expr.exportTo(exprManager, variableMap), d_inUnsatCore); + c->d_result = d_result; + return c; +} + +Command* QueryCommand::clone() const { + QueryCommand* c = new QueryCommand(d_expr, d_inUnsatCore); + c->d_result = d_result; + return c; +} + +std::string QueryCommand::getCommandName() const throw() { + return "query"; +} + +/* class ResetCommand */ + +void ResetCommand::invoke(SmtEngine* smtEngine) throw() { + try { + smtEngine->reset(); + d_commandStatus = CommandSuccess::instance(); + } catch(exception& e) { + d_commandStatus = new CommandFailure(e.what()); + } +} + +Command* ResetCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + return new ResetCommand(); +} + +Command* ResetCommand::clone() const { + return new ResetCommand(); +} + +std::string ResetCommand::getCommandName() const throw() { + return "reset"; +} + +/* class ResetAssertionsCommand */ + +void ResetAssertionsCommand::invoke(SmtEngine* smtEngine) throw() { + try { + smtEngine->resetAssertions(); + d_commandStatus = CommandSuccess::instance(); + } catch(exception& e) { + d_commandStatus = new CommandFailure(e.what()); + } +} + +Command* ResetAssertionsCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + return new ResetAssertionsCommand(); +} + +Command* ResetAssertionsCommand::clone() const { + return new ResetAssertionsCommand(); +} + +std::string ResetAssertionsCommand::getCommandName() const throw() { + return "reset-assertions"; +} + +/* class QuitCommand */ + +void QuitCommand::invoke(SmtEngine* smtEngine) throw() { + Dump("benchmark") << *this; + d_commandStatus = CommandSuccess::instance(); +} + +Command* QuitCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + return new QuitCommand(); +} + +Command* QuitCommand::clone() const { + return new QuitCommand(); +} + +std::string QuitCommand::getCommandName() const throw() { + return "exit"; +} + +/* class CommentCommand */ + +CommentCommand::CommentCommand(std::string comment) throw() : d_comment(comment) { +} + +std::string CommentCommand::getComment() const throw() { + return d_comment; +} + +void CommentCommand::invoke(SmtEngine* smtEngine) throw() { + Dump("benchmark") << *this; + d_commandStatus = CommandSuccess::instance(); +} + +Command* CommentCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + return new CommentCommand(d_comment); +} + +Command* CommentCommand::clone() const { + return new CommentCommand(d_comment); +} + +std::string CommentCommand::getCommandName() const throw() { + return "comment"; +} + +/* class CommandSequence */ + +CommandSequence::CommandSequence() throw() : + d_index(0) { +} + +CommandSequence::~CommandSequence() throw() { + for(unsigned i = d_index; i < d_commandSequence.size(); ++i) { + delete d_commandSequence[i]; + } +} + +void CommandSequence::addCommand(Command* cmd) throw() { + d_commandSequence.push_back(cmd); +} + +void CommandSequence::clear() throw() { + d_commandSequence.clear(); +} + +void CommandSequence::invoke(SmtEngine* smtEngine) throw() { + for(; d_index < d_commandSequence.size(); ++d_index) { + d_commandSequence[d_index]->invoke(smtEngine); + if(! d_commandSequence[d_index]->ok()) { + // abort execution + d_commandStatus = d_commandSequence[d_index]->getCommandStatus(); + return; + } + delete d_commandSequence[d_index]; + } + + AlwaysAssert(d_commandStatus == NULL); + d_commandStatus = CommandSuccess::instance(); +} + +void CommandSequence::invoke(SmtEngine* smtEngine, std::ostream& out) throw() { + for(; d_index < d_commandSequence.size(); ++d_index) { + d_commandSequence[d_index]->invoke(smtEngine, out); + if(! d_commandSequence[d_index]->ok()) { + // abort execution + d_commandStatus = d_commandSequence[d_index]->getCommandStatus(); + return; + } + delete d_commandSequence[d_index]; + } + + AlwaysAssert(d_commandStatus == NULL); + d_commandStatus = CommandSuccess::instance(); +} + +Command* CommandSequence::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + CommandSequence* seq = new CommandSequence(); + for(iterator i = begin(); i != end(); ++i) { + Command* cmd_to_export = *i; + Command* cmd = cmd_to_export->exportTo(exprManager, variableMap); + seq->addCommand(cmd); + Debug("export") << "[export] so far converted: " << seq << endl; + } + seq->d_index = d_index; + return seq; +} + +Command* CommandSequence::clone() const { + CommandSequence* seq = new CommandSequence(); + for(const_iterator i = begin(); i != end(); ++i) { + seq->addCommand((*i)->clone()); + } + seq->d_index = d_index; + return seq; +} + +CommandSequence::const_iterator CommandSequence::begin() const throw() { + return d_commandSequence.begin(); +} + +CommandSequence::const_iterator CommandSequence::end() const throw() { + return d_commandSequence.end(); +} + +CommandSequence::iterator CommandSequence::begin() throw() { + return d_commandSequence.begin(); +} + +CommandSequence::iterator CommandSequence::end() throw() { + return d_commandSequence.end(); +} + +std::string CommandSequence::getCommandName() const throw() { + return "sequence"; +} + +/* class DeclarationSequenceCommand */ + +/* class DeclarationDefinitionCommand */ + +DeclarationDefinitionCommand::DeclarationDefinitionCommand(const std::string& id) throw() : + d_symbol(id) { +} + +std::string DeclarationDefinitionCommand::getSymbol() const throw() { + return d_symbol; +} + +/* class DeclareFunctionCommand */ + +DeclareFunctionCommand::DeclareFunctionCommand(const std::string& id, Expr func, Type t) throw() : + DeclarationDefinitionCommand(id), + d_func(func), + d_type(t), + d_printInModel(true), + d_printInModelSetByUser(false){ +} + +Expr DeclareFunctionCommand::getFunction() const throw() { + return d_func; +} + +Type DeclareFunctionCommand::getType() const throw() { + return d_type; +} + +bool DeclareFunctionCommand::getPrintInModel() const throw() { + return d_printInModel; +} + +bool DeclareFunctionCommand::getPrintInModelSetByUser() const throw() { + return d_printInModelSetByUser; +} + +void DeclareFunctionCommand::setPrintInModel( bool p ) { + d_printInModel = p; + d_printInModelSetByUser = true; +} + +void DeclareFunctionCommand::invoke(SmtEngine* smtEngine) throw() { + d_commandStatus = CommandSuccess::instance(); +} + +Command* DeclareFunctionCommand::exportTo(ExprManager* exprManager, + ExprManagerMapCollection& variableMap) { + DeclareFunctionCommand * dfc = new DeclareFunctionCommand(d_symbol, d_func.exportTo(exprManager, variableMap), + d_type.exportTo(exprManager, variableMap)); + dfc->d_printInModel = d_printInModel; + dfc->d_printInModelSetByUser = d_printInModelSetByUser; + return dfc; +} + +Command* DeclareFunctionCommand::clone() const { + DeclareFunctionCommand * dfc = new DeclareFunctionCommand(d_symbol, d_func, d_type); + dfc->d_printInModel = d_printInModel; + dfc->d_printInModelSetByUser = d_printInModelSetByUser; + return dfc; +} + +std::string DeclareFunctionCommand::getCommandName() const throw() { + return "declare-fun"; +} + +/* class DeclareTypeCommand */ + +DeclareTypeCommand::DeclareTypeCommand(const std::string& id, size_t arity, Type t) throw() : + DeclarationDefinitionCommand(id), + d_arity(arity), + d_type(t) { +} + +size_t DeclareTypeCommand::getArity() const throw() { + return d_arity; +} + +Type DeclareTypeCommand::getType() const throw() { + return d_type; +} + +void DeclareTypeCommand::invoke(SmtEngine* smtEngine) throw() { + d_commandStatus = CommandSuccess::instance(); +} + +Command* DeclareTypeCommand::exportTo(ExprManager* exprManager, + ExprManagerMapCollection& variableMap) { + return new DeclareTypeCommand(d_symbol, d_arity, + d_type.exportTo(exprManager, variableMap)); +} + +Command* DeclareTypeCommand::clone() const { + return new DeclareTypeCommand(d_symbol, d_arity, d_type); +} + +std::string DeclareTypeCommand::getCommandName() const throw() { + return "declare-sort"; +} + +/* class DefineTypeCommand */ + +DefineTypeCommand::DefineTypeCommand(const std::string& id, + Type t) throw() : + DeclarationDefinitionCommand(id), + d_params(), + d_type(t) { +} + +DefineTypeCommand::DefineTypeCommand(const std::string& id, + const std::vector<Type>& params, + Type t) throw() : + DeclarationDefinitionCommand(id), + d_params(params), + d_type(t) { +} + +const std::vector<Type>& DefineTypeCommand::getParameters() const throw() { + return d_params; +} + +Type DefineTypeCommand::getType() const throw() { + return d_type; +} + +void DefineTypeCommand::invoke(SmtEngine* smtEngine) throw() { + d_commandStatus = CommandSuccess::instance(); +} + +Command* DefineTypeCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + vector<Type> params; + transform(d_params.begin(), d_params.end(), back_inserter(params), + ExportTransformer(exprManager, variableMap)); + Type type = d_type.exportTo(exprManager, variableMap); + return new DefineTypeCommand(d_symbol, params, type); +} + +Command* DefineTypeCommand::clone() const { + return new DefineTypeCommand(d_symbol, d_params, d_type); +} + +std::string DefineTypeCommand::getCommandName() const throw() { + return "define-sort"; +} + +/* class DefineFunctionCommand */ + +DefineFunctionCommand::DefineFunctionCommand(const std::string& id, + Expr func, + Expr formula) throw() : + DeclarationDefinitionCommand(id), + d_func(func), + d_formals(), + d_formula(formula) { +} + +DefineFunctionCommand::DefineFunctionCommand(const std::string& id, + Expr func, + const std::vector<Expr>& formals, + Expr formula) throw() : + DeclarationDefinitionCommand(id), + d_func(func), + d_formals(formals), + d_formula(formula) { +} + +Expr DefineFunctionCommand::getFunction() const throw() { + return d_func; +} + +const std::vector<Expr>& DefineFunctionCommand::getFormals() const throw() { + return d_formals; +} + +Expr DefineFunctionCommand::getFormula() const throw() { + return d_formula; +} + +void DefineFunctionCommand::invoke(SmtEngine* smtEngine) throw() { + try { + if(!d_func.isNull()) { + smtEngine->defineFunction(d_func, d_formals, d_formula); + } + d_commandStatus = CommandSuccess::instance(); + } catch(exception& e) { + d_commandStatus = new CommandFailure(e.what()); + } +} + +Command* DefineFunctionCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + Expr func = d_func.exportTo(exprManager, variableMap, /* flags = */ ExprManager::VAR_FLAG_DEFINED); + vector<Expr> formals; + transform(d_formals.begin(), d_formals.end(), back_inserter(formals), + ExportTransformer(exprManager, variableMap)); + Expr formula = d_formula.exportTo(exprManager, variableMap); + return new DefineFunctionCommand(d_symbol, func, formals, formula); +} + +Command* DefineFunctionCommand::clone() const { + return new DefineFunctionCommand(d_symbol, d_func, d_formals, d_formula); +} + +std::string DefineFunctionCommand::getCommandName() const throw() { + return "define-fun"; +} + +/* class DefineNamedFunctionCommand */ + +DefineNamedFunctionCommand::DefineNamedFunctionCommand(const std::string& id, + Expr func, + const std::vector<Expr>& formals, + Expr formula) throw() : + DefineFunctionCommand(id, func, formals, formula) { +} + +void DefineNamedFunctionCommand::invoke(SmtEngine* smtEngine) throw() { + this->DefineFunctionCommand::invoke(smtEngine); + if(!d_func.isNull() && d_func.getType().isBoolean()) { + smtEngine->addToAssignment(d_func.getExprManager()->mkExpr(kind::APPLY, d_func)); + } + d_commandStatus = CommandSuccess::instance(); +} + +Command* DefineNamedFunctionCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + Expr func = d_func.exportTo(exprManager, variableMap); + vector<Expr> formals; + transform(d_formals.begin(), d_formals.end(), back_inserter(formals), + ExportTransformer(exprManager, variableMap)); + Expr formula = d_formula.exportTo(exprManager, variableMap); + return new DefineNamedFunctionCommand(d_symbol, func, formals, formula); +} + +Command* DefineNamedFunctionCommand::clone() const { + return new DefineNamedFunctionCommand(d_symbol, d_func, d_formals, d_formula); +} + +/* class SetUserAttribute */ + +SetUserAttributeCommand::SetUserAttributeCommand( const std::string& attr, Expr expr ) throw() : + d_attr( attr ), d_expr( expr ){ +} + +SetUserAttributeCommand::SetUserAttributeCommand( const std::string& attr, Expr expr, + std::vector<Expr>& values ) throw() : + d_attr( attr ), d_expr( expr ){ + d_expr_values.insert( d_expr_values.begin(), values.begin(), values.end() ); +} + +SetUserAttributeCommand::SetUserAttributeCommand( const std::string& attr, Expr expr, + const std::string& value ) throw() : + d_attr( attr ), d_expr( expr ), d_str_value( value ){ +} + +void SetUserAttributeCommand::invoke(SmtEngine* smtEngine) throw(){ + try { + if(!d_expr.isNull()) { + smtEngine->setUserAttribute( d_attr, d_expr, d_expr_values, d_str_value ); + } + d_commandStatus = CommandSuccess::instance(); + } catch(exception& e) { + d_commandStatus = new CommandFailure(e.what()); + } +} + +Command* SetUserAttributeCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap){ + Expr expr = d_expr.exportTo(exprManager, variableMap); + SetUserAttributeCommand * c = new SetUserAttributeCommand( d_attr, expr, d_str_value ); + c->d_expr_values.insert( c->d_expr_values.end(), d_expr_values.begin(), d_expr_values.end() ); + return c; +} + +Command* SetUserAttributeCommand::clone() const{ + SetUserAttributeCommand * c = new SetUserAttributeCommand( d_attr, d_expr, d_str_value ); + c->d_expr_values.insert( c->d_expr_values.end(), d_expr_values.begin(), d_expr_values.end() ); + return c; +} + +std::string SetUserAttributeCommand::getCommandName() const throw() { + return "set-user-attribute"; +} + +/* class SimplifyCommand */ + +SimplifyCommand::SimplifyCommand(Expr term) throw() : + d_term(term) { +} + +Expr SimplifyCommand::getTerm() const throw() { + return d_term; +} + +void SimplifyCommand::invoke(SmtEngine* smtEngine) throw() { + try { + d_result = smtEngine->simplify(d_term); + d_commandStatus = CommandSuccess::instance(); + } catch(UnsafeInterruptException& e) { + d_commandStatus = new CommandInterrupted(); + } catch(exception& e) { + d_commandStatus = new CommandFailure(e.what()); + } +} + +Expr SimplifyCommand::getResult() const throw() { + return d_result; +} + +void SimplifyCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() { + if(! ok()) { + this->Command::printResult(out, verbosity); + } else { + out << d_result << endl; + } +} + +Command* SimplifyCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + SimplifyCommand* c = new SimplifyCommand(d_term.exportTo(exprManager, variableMap)); + c->d_result = d_result.exportTo(exprManager, variableMap); + return c; +} + +Command* SimplifyCommand::clone() const { + SimplifyCommand* c = new SimplifyCommand(d_term); + c->d_result = d_result; + return c; +} + +std::string SimplifyCommand::getCommandName() const throw() { + return "simplify"; +} + +/* class ExpandDefinitionsCommand */ + +ExpandDefinitionsCommand::ExpandDefinitionsCommand(Expr term) throw() : + d_term(term) { +} + +Expr ExpandDefinitionsCommand::getTerm() const throw() { + return d_term; +} + +void ExpandDefinitionsCommand::invoke(SmtEngine* smtEngine) throw() { + d_result = smtEngine->expandDefinitions(d_term); + d_commandStatus = CommandSuccess::instance(); +} + +Expr ExpandDefinitionsCommand::getResult() const throw() { + return d_result; +} + +void ExpandDefinitionsCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() { + if(! ok()) { + this->Command::printResult(out, verbosity); + } else { + out << d_result << endl; + } +} + +Command* ExpandDefinitionsCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + ExpandDefinitionsCommand* c = new ExpandDefinitionsCommand(d_term.exportTo(exprManager, variableMap)); + c->d_result = d_result.exportTo(exprManager, variableMap); + return c; +} + +Command* ExpandDefinitionsCommand::clone() const { + ExpandDefinitionsCommand* c = new ExpandDefinitionsCommand(d_term); + c->d_result = d_result; + return c; +} + +std::string ExpandDefinitionsCommand::getCommandName() const throw() { + return "expand-definitions"; +} + +/* class GetValueCommand */ + +GetValueCommand::GetValueCommand(Expr term) throw() : + d_terms() { + d_terms.push_back(term); +} + +GetValueCommand::GetValueCommand(const std::vector<Expr>& terms) throw() : + d_terms(terms) { + CheckArgument(terms.size() >= 1, terms, "cannot get-value of an empty set of terms"); +} + +const std::vector<Expr>& GetValueCommand::getTerms() const throw() { + return d_terms; +} + +void GetValueCommand::invoke(SmtEngine* smtEngine) throw() { + try { + vector<Expr> result; + ExprManager* em = smtEngine->getExprManager(); + NodeManager* nm = NodeManager::fromExprManager(em); + for(std::vector<Expr>::const_iterator i = d_terms.begin(); i != d_terms.end(); ++i) { + Assert(nm == NodeManager::fromExprManager((*i).getExprManager())); + smt::SmtScope scope(smtEngine); + Node request = Node::fromExpr(options::expandDefinitions() ? smtEngine->expandDefinitions(*i) : *i); + Node value = Node::fromExpr(smtEngine->getValue(*i)); + if(value.getType().isInteger() && request.getType() == nm->realType()) { + // Need to wrap in special marker so that output printers know this + // is an integer-looking constant that really should be output as + // a rational. Necessary for SMT-LIB standards compliance, but ugly. + value = nm->mkNode(kind::APPLY_TYPE_ASCRIPTION, + nm->mkConst(AscriptionType(em->realType())), value); + } + result.push_back(nm->mkNode(kind::SEXPR, request, value).toExpr()); + } + d_result = em->mkExpr(kind::SEXPR, result); + d_commandStatus = CommandSuccess::instance(); + } catch(UnsafeInterruptException& e) { + d_commandStatus = new CommandInterrupted(); + } catch(exception& e) { + d_commandStatus = new CommandFailure(e.what()); + } +} + +Expr GetValueCommand::getResult() const throw() { + return d_result; +} + +void GetValueCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() { + if(! ok()) { + this->Command::printResult(out, verbosity); + } else { + Expr::dag::Scope scope(out, false); + out << d_result << endl; + } +} + +Command* GetValueCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + vector<Expr> exportedTerms; + for(std::vector<Expr>::const_iterator i = d_terms.begin(); i != d_terms.end(); ++i) { + exportedTerms.push_back((*i).exportTo(exprManager, variableMap)); + } + GetValueCommand* c = new GetValueCommand(exportedTerms); + c->d_result = d_result.exportTo(exprManager, variableMap); + return c; +} + +Command* GetValueCommand::clone() const { + GetValueCommand* c = new GetValueCommand(d_terms); + c->d_result = d_result; + return c; +} + +std::string GetValueCommand::getCommandName() const throw() { + return "get-value"; +} + +/* class GetAssignmentCommand */ + +GetAssignmentCommand::GetAssignmentCommand() throw() { +} + +void GetAssignmentCommand::invoke(SmtEngine* smtEngine) throw() { + try { + d_result = smtEngine->getAssignment(); + d_commandStatus = CommandSuccess::instance(); + } catch(UnsafeInterruptException& e) { + d_commandStatus = new CommandInterrupted(); + } catch(exception& e) { + d_commandStatus = new CommandFailure(e.what()); + } +} + +SExpr GetAssignmentCommand::getResult() const throw() { + return d_result; +} + +void GetAssignmentCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() { + if(! ok()) { + this->Command::printResult(out, verbosity); + } else { + out << d_result << endl; + } +} + +Command* GetAssignmentCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + GetAssignmentCommand* c = new GetAssignmentCommand(); + c->d_result = d_result; + return c; +} + +Command* GetAssignmentCommand::clone() const { + GetAssignmentCommand* c = new GetAssignmentCommand(); + c->d_result = d_result; + return c; +} + +std::string GetAssignmentCommand::getCommandName() const throw() { + return "get-assignment"; +} + +/* class GetModelCommand */ + +GetModelCommand::GetModelCommand() throw() { +} + +void GetModelCommand::invoke(SmtEngine* smtEngine) throw() { + try { + d_result = smtEngine->getModel(); + d_smtEngine = smtEngine; + d_commandStatus = CommandSuccess::instance(); + } catch(UnsafeInterruptException& e) { + d_commandStatus = new CommandInterrupted(); + } catch(exception& e) { + d_commandStatus = new CommandFailure(e.what()); + } +} + +/* Model is private to the library -- for now +Model* GetModelCommand::getResult() const throw() { + return d_result; +} +*/ + +void GetModelCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() { + if(! ok()) { + this->Command::printResult(out, verbosity); + } else { + out << *d_result; + } +} + +Command* GetModelCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + GetModelCommand* c = new GetModelCommand(); + c->d_result = d_result; + c->d_smtEngine = d_smtEngine; + return c; +} + +Command* GetModelCommand::clone() const { + GetModelCommand* c = new GetModelCommand(); + c->d_result = d_result; + c->d_smtEngine = d_smtEngine; + return c; +} + +std::string GetModelCommand::getCommandName() const throw() { + return "get-model"; +} + +/* class GetProofCommand */ + +GetProofCommand::GetProofCommand() throw() { +} + +void GetProofCommand::invoke(SmtEngine* smtEngine) throw() { + try { + d_result = smtEngine->getProof(); + d_commandStatus = CommandSuccess::instance(); + } catch(UnsafeInterruptException& e) { + d_commandStatus = new CommandInterrupted(); + } catch(exception& e) { + d_commandStatus = new CommandFailure(e.what()); + } +} + +Proof* GetProofCommand::getResult() const throw() { + return d_result; +} + +void GetProofCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() { + if(! ok()) { + this->Command::printResult(out, verbosity); + } else { + d_result->toStream(out); + } +} + +Command* GetProofCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + GetProofCommand* c = new GetProofCommand(); + c->d_result = d_result; + return c; +} + +Command* GetProofCommand::clone() const { + GetProofCommand* c = new GetProofCommand(); + c->d_result = d_result; + return c; +} + +std::string GetProofCommand::getCommandName() const throw() { + return "get-proof"; +} + +/* class GetInstantiationsCommand */ + +GetInstantiationsCommand::GetInstantiationsCommand() throw() { +} + +void GetInstantiationsCommand::invoke(SmtEngine* smtEngine) throw() { + try { + d_smtEngine = smtEngine; + d_commandStatus = CommandSuccess::instance(); + } catch(exception& e) { + d_commandStatus = new CommandFailure(e.what()); + } +} + +//Instantiations* GetInstantiationsCommand::getResult() const throw() { +// return d_result; +//} + +void GetInstantiationsCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() { + if(! ok()) { + this->Command::printResult(out, verbosity); + } else { + d_smtEngine->printInstantiations(out); + } +} + +Command* GetInstantiationsCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + GetInstantiationsCommand* c = new GetInstantiationsCommand(); + //c->d_result = d_result; + c->d_smtEngine = d_smtEngine; + return c; +} + +Command* GetInstantiationsCommand::clone() const { + GetInstantiationsCommand* c = new GetInstantiationsCommand(); + //c->d_result = d_result; + c->d_smtEngine = d_smtEngine; + return c; +} + +std::string GetInstantiationsCommand::getCommandName() const throw() { + return "get-instantiations"; +} + +/* class GetSynthSolutionCommand */ + +GetSynthSolutionCommand::GetSynthSolutionCommand() throw() { +} + +void GetSynthSolutionCommand::invoke(SmtEngine* smtEngine) throw() { + try { + d_smtEngine = smtEngine; + d_commandStatus = CommandSuccess::instance(); + } catch(exception& e) { + d_commandStatus = new CommandFailure(e.what()); + } +} + +void GetSynthSolutionCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() { + if(! ok()) { + this->Command::printResult(out, verbosity); + } else { + d_smtEngine->printSynthSolution(out); + } +} + +Command* GetSynthSolutionCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + GetSynthSolutionCommand* c = new GetSynthSolutionCommand(); + c->d_smtEngine = d_smtEngine; + return c; +} + +Command* GetSynthSolutionCommand::clone() const { + GetSynthSolutionCommand* c = new GetSynthSolutionCommand(); + c->d_smtEngine = d_smtEngine; + return c; +} + +std::string GetSynthSolutionCommand::getCommandName() const throw() { + return "get-instantiations"; +} + +/* class GetUnsatCoreCommand */ + +GetUnsatCoreCommand::GetUnsatCoreCommand() throw() { +} + +GetUnsatCoreCommand::GetUnsatCoreCommand(const std::map<Expr, std::string>& names) throw() : d_names(names) { +} + +void GetUnsatCoreCommand::invoke(SmtEngine* smtEngine) throw() { + try { + d_result = smtEngine->getUnsatCore(); + d_commandStatus = CommandSuccess::instance(); + } catch(exception& e) { + d_commandStatus = new CommandFailure(e.what()); + } +} + +void GetUnsatCoreCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() { + if(! ok()) { + this->Command::printResult(out, verbosity); + } else { + d_result.toStream(out, d_names); + } +} + +const UnsatCore& GetUnsatCoreCommand::getUnsatCore() const throw() { + // of course, this will be empty if the command hasn't been invoked yet + return d_result; +} + +Command* GetUnsatCoreCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + GetUnsatCoreCommand* c = new GetUnsatCoreCommand(d_names); + c->d_result = d_result; + return c; +} + +Command* GetUnsatCoreCommand::clone() const { + GetUnsatCoreCommand* c = new GetUnsatCoreCommand(d_names); + c->d_result = d_result; + return c; +} + +std::string GetUnsatCoreCommand::getCommandName() const throw() { + return "get-unsat-core"; +} + +/* class GetAssertionsCommand */ + +GetAssertionsCommand::GetAssertionsCommand() throw() { +} + +void GetAssertionsCommand::invoke(SmtEngine* smtEngine) throw() { + try { + stringstream ss; + const vector<Expr> v = smtEngine->getAssertions(); + ss << "(\n"; + copy( v.begin(), v.end(), ostream_iterator<Expr>(ss, "\n") ); + ss << ")\n"; + d_result = ss.str(); + d_commandStatus = CommandSuccess::instance(); + } catch(exception& e) { + d_commandStatus = new CommandFailure(e.what()); + } +} + +std::string GetAssertionsCommand::getResult() const throw() { + return d_result; +} + +void GetAssertionsCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() { + if(! ok()) { + this->Command::printResult(out, verbosity); + } else { + out << d_result; + } +} + +Command* GetAssertionsCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + GetAssertionsCommand* c = new GetAssertionsCommand(); + c->d_result = d_result; + return c; +} + +Command* GetAssertionsCommand::clone() const { + GetAssertionsCommand* c = new GetAssertionsCommand(); + c->d_result = d_result; + return c; +} + +std::string GetAssertionsCommand::getCommandName() const throw() { + return "get-assertions"; +} + +/* class SetBenchmarkStatusCommand */ + +SetBenchmarkStatusCommand::SetBenchmarkStatusCommand(BenchmarkStatus status) throw() : + d_status(status) { +} + +BenchmarkStatus SetBenchmarkStatusCommand::getStatus() const throw() { + return d_status; +} + +void SetBenchmarkStatusCommand::invoke(SmtEngine* smtEngine) throw() { + try { + stringstream ss; + ss << d_status; + SExpr status = SExpr(ss.str()); + smtEngine->setInfo("status", status); + d_commandStatus = CommandSuccess::instance(); + } catch(exception& e) { + d_commandStatus = new CommandFailure(e.what()); + } +} + +Command* SetBenchmarkStatusCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + return new SetBenchmarkStatusCommand(d_status); +} + +Command* SetBenchmarkStatusCommand::clone() const { + return new SetBenchmarkStatusCommand(d_status); +} + +std::string SetBenchmarkStatusCommand::getCommandName() const throw() { + return "set-info"; +} + +/* class SetBenchmarkLogicCommand */ + +SetBenchmarkLogicCommand::SetBenchmarkLogicCommand(std::string logic) throw() : + d_logic(logic) { +} + +std::string SetBenchmarkLogicCommand::getLogic() const throw() { + return d_logic; +} + +void SetBenchmarkLogicCommand::invoke(SmtEngine* smtEngine) throw() { + try { + smtEngine->setLogic(d_logic); + d_commandStatus = CommandSuccess::instance(); + } catch(exception& e) { + d_commandStatus = new CommandFailure(e.what()); + } +} + +Command* SetBenchmarkLogicCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + return new SetBenchmarkLogicCommand(d_logic); +} + +Command* SetBenchmarkLogicCommand::clone() const { + return new SetBenchmarkLogicCommand(d_logic); +} + +std::string SetBenchmarkLogicCommand::getCommandName() const throw() { + return "set-logic"; +} + +/* class SetInfoCommand */ + +SetInfoCommand::SetInfoCommand(std::string flag, const SExpr& sexpr) throw() : + d_flag(flag), + d_sexpr(sexpr) { +} + +std::string SetInfoCommand::getFlag() const throw() { + return d_flag; +} + +SExpr SetInfoCommand::getSExpr() const throw() { + return d_sexpr; +} + +void SetInfoCommand::invoke(SmtEngine* smtEngine) throw() { + try { + smtEngine->setInfo(d_flag, d_sexpr); + d_commandStatus = CommandSuccess::instance(); + } catch(UnrecognizedOptionException&) { + // As per SMT-LIB spec, silently accept unknown set-info keys + d_commandStatus = CommandSuccess::instance(); + } catch(exception& e) { + d_commandStatus = new CommandFailure(e.what()); + } +} + +Command* SetInfoCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + return new SetInfoCommand(d_flag, d_sexpr); +} + +Command* SetInfoCommand::clone() const { + return new SetInfoCommand(d_flag, d_sexpr); +} + +std::string SetInfoCommand::getCommandName() const throw() { + return "set-info"; +} + +/* class GetInfoCommand */ + +GetInfoCommand::GetInfoCommand(std::string flag) throw() : + d_flag(flag) { +} + +std::string GetInfoCommand::getFlag() const throw() { + return d_flag; +} + +void GetInfoCommand::invoke(SmtEngine* smtEngine) throw() { + try { + vector<SExpr> v; + v.push_back(SExpr(SExpr::Keyword(string(":") + d_flag))); + v.push_back(smtEngine->getInfo(d_flag)); + stringstream ss; + if(d_flag == "all-options" || d_flag == "all-statistics") { + ss << PrettySExprs(true); + } + ss << SExpr(v); + d_result = ss.str(); + d_commandStatus = CommandSuccess::instance(); + } catch(UnrecognizedOptionException&) { + d_commandStatus = new CommandUnsupported(); + } catch(exception& e) { + d_commandStatus = new CommandFailure(e.what()); + } +} + +std::string GetInfoCommand::getResult() const throw() { + return d_result; +} + +void GetInfoCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() { + if(! ok()) { + this->Command::printResult(out, verbosity); + } else if(d_result != "") { + out << d_result << endl; + } +} + +Command* GetInfoCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + GetInfoCommand* c = new GetInfoCommand(d_flag); + c->d_result = d_result; + return c; +} + +Command* GetInfoCommand::clone() const { + GetInfoCommand* c = new GetInfoCommand(d_flag); + c->d_result = d_result; + return c; +} + +std::string GetInfoCommand::getCommandName() const throw() { + return "get-info"; +} + +/* class SetOptionCommand */ + +SetOptionCommand::SetOptionCommand(std::string flag, const SExpr& sexpr) throw() : + d_flag(flag), + d_sexpr(sexpr) { +} + +std::string SetOptionCommand::getFlag() const throw() { + return d_flag; +} + +SExpr SetOptionCommand::getSExpr() const throw() { + return d_sexpr; +} + +void SetOptionCommand::invoke(SmtEngine* smtEngine) throw() { + try { + smtEngine->setOption(d_flag, d_sexpr); + d_commandStatus = CommandSuccess::instance(); + } catch(UnrecognizedOptionException&) { + d_commandStatus = new CommandUnsupported(); + } catch(exception& e) { + d_commandStatus = new CommandFailure(e.what()); + } +} + +Command* SetOptionCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + return new SetOptionCommand(d_flag, d_sexpr); +} + +Command* SetOptionCommand::clone() const { + return new SetOptionCommand(d_flag, d_sexpr); +} + +std::string SetOptionCommand::getCommandName() const throw() { + return "set-option"; +} + +/* class GetOptionCommand */ + +GetOptionCommand::GetOptionCommand(std::string flag) throw() : + d_flag(flag) { +} + +std::string GetOptionCommand::getFlag() const throw() { + return d_flag; +} + +void GetOptionCommand::invoke(SmtEngine* smtEngine) throw() { + try { + SExpr res = smtEngine->getOption(d_flag); + d_result = res.toString(); + d_commandStatus = CommandSuccess::instance(); + } catch(UnrecognizedOptionException&) { + d_commandStatus = new CommandUnsupported(); + } catch(exception& e) { + d_commandStatus = new CommandFailure(e.what()); + } +} + +std::string GetOptionCommand::getResult() const throw() { + return d_result; +} + +void GetOptionCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() { + if(! ok()) { + this->Command::printResult(out, verbosity); + } else if(d_result != "") { + out << d_result << endl; + } +} + +Command* GetOptionCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + GetOptionCommand* c = new GetOptionCommand(d_flag); + c->d_result = d_result; + return c; +} + +Command* GetOptionCommand::clone() const { + GetOptionCommand* c = new GetOptionCommand(d_flag); + c->d_result = d_result; + return c; +} + +std::string GetOptionCommand::getCommandName() const throw() { + return "get-option"; +} + +/* class DatatypeDeclarationCommand */ + +DatatypeDeclarationCommand::DatatypeDeclarationCommand(const DatatypeType& datatype) throw() : + d_datatypes() { + d_datatypes.push_back(datatype); +} + +DatatypeDeclarationCommand::DatatypeDeclarationCommand(const std::vector<DatatypeType>& datatypes) throw() : + d_datatypes(datatypes) { +} + +const std::vector<DatatypeType>& +DatatypeDeclarationCommand::getDatatypes() const throw() { + return d_datatypes; +} + +void DatatypeDeclarationCommand::invoke(SmtEngine* smtEngine) throw() { + d_commandStatus = CommandSuccess::instance(); +} + +Command* DatatypeDeclarationCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + throw ExportUnsupportedException + ("export of DatatypeDeclarationCommand unsupported"); +} + +Command* DatatypeDeclarationCommand::clone() const { + return new DatatypeDeclarationCommand(d_datatypes); +} + +std::string DatatypeDeclarationCommand::getCommandName() const throw() { + return "declare-datatypes"; +} + +/* class RewriteRuleCommand */ + +RewriteRuleCommand::RewriteRuleCommand(const std::vector<Expr>& vars, + const std::vector<Expr>& guards, + Expr head, Expr body, + const Triggers& triggers) throw() : + d_vars(vars), d_guards(guards), d_head(head), d_body(body), d_triggers(triggers) { +} + +RewriteRuleCommand::RewriteRuleCommand(const std::vector<Expr>& vars, + Expr head, Expr body) throw() : + d_vars(vars), d_head(head), d_body(body) { +} + +const std::vector<Expr>& RewriteRuleCommand::getVars() const throw() { + return d_vars; +} + +const std::vector<Expr>& RewriteRuleCommand::getGuards() const throw() { + return d_guards; +} + +Expr RewriteRuleCommand::getHead() const throw() { + return d_head; +} + +Expr RewriteRuleCommand::getBody() const throw() { + return d_body; +} + +const RewriteRuleCommand::Triggers& RewriteRuleCommand::getTriggers() const throw() { + return d_triggers; +} + +void RewriteRuleCommand::invoke(SmtEngine* smtEngine) throw() { + try { + ExprManager* em = smtEngine->getExprManager(); + /** build vars list */ + Expr vars = em->mkExpr(kind::BOUND_VAR_LIST, d_vars); + /** build guards list */ + Expr guards; + if(d_guards.size() == 0) guards = em->mkConst<bool>(true); + else if(d_guards.size() == 1) guards = d_guards[0]; + else guards = em->mkExpr(kind::AND,d_guards); + /** build expression */ + Expr expr; + if( d_triggers.empty() ){ + expr = em->mkExpr(kind::RR_REWRITE,vars,guards,d_head,d_body); + } else { + /** build triggers list */ + std::vector<Expr> vtriggers; + vtriggers.reserve(d_triggers.size()); + for(Triggers::const_iterator i = d_triggers.begin(), + end = d_triggers.end(); i != end; ++i){ + vtriggers.push_back(em->mkExpr(kind::INST_PATTERN,*i)); + } + Expr triggers = em->mkExpr(kind::INST_PATTERN_LIST,vtriggers); + expr = em->mkExpr(kind::RR_REWRITE,vars,guards,d_head,d_body,triggers); + } + smtEngine->assertFormula(expr); + d_commandStatus = CommandSuccess::instance(); + } catch(exception& e) { + d_commandStatus = new CommandFailure(e.what()); + } +} + +Command* RewriteRuleCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + /** Convert variables */ + VExpr vars; vars.reserve(d_vars.size()); + for(VExpr::iterator i = d_vars.begin(), end = d_vars.end(); + i == end; ++i){ + vars.push_back(i->exportTo(exprManager, variableMap)); + }; + /** Convert guards */ + VExpr guards; guards.reserve(d_guards.size()); + for(VExpr::iterator i = d_guards.begin(), end = d_guards.end(); + i == end; ++i){ + guards.push_back(i->exportTo(exprManager, variableMap)); + }; + /** Convert triggers */ + Triggers triggers; triggers.resize(d_triggers.size()); + for(size_t i = 0, end = d_triggers.size(); + i < end; ++i){ + triggers[i].reserve(d_triggers[i].size()); + for(VExpr::iterator j = d_triggers[i].begin(), jend = d_triggers[i].end(); + j == jend; ++i){ + triggers[i].push_back(j->exportTo(exprManager, variableMap)); + }; + }; + /** Convert head and body */ + Expr head = d_head.exportTo(exprManager, variableMap); + Expr body = d_body.exportTo(exprManager, variableMap); + /** Create the converted rules */ + return new RewriteRuleCommand(vars, guards, head, body, triggers); +} + +Command* RewriteRuleCommand::clone() const { + return new RewriteRuleCommand(d_vars, d_guards, d_head, d_body, d_triggers); +} + +std::string RewriteRuleCommand::getCommandName() const throw() { + return "rewrite-rule"; +} + +/* class PropagateRuleCommand */ + +PropagateRuleCommand::PropagateRuleCommand(const std::vector<Expr>& vars, + const std::vector<Expr>& guards, + const std::vector<Expr>& heads, + Expr body, + const Triggers& triggers, + bool deduction) throw() : + d_vars(vars), d_guards(guards), d_heads(heads), d_body(body), d_triggers(triggers), d_deduction(deduction) { +} + +PropagateRuleCommand::PropagateRuleCommand(const std::vector<Expr>& vars, + const std::vector<Expr>& heads, + Expr body, + bool deduction) throw() : + d_vars(vars), d_heads(heads), d_body(body), d_deduction(deduction) { +} + +const std::vector<Expr>& PropagateRuleCommand::getVars() const throw() { + return d_vars; +} + +const std::vector<Expr>& PropagateRuleCommand::getGuards() const throw() { + return d_guards; +} + +const std::vector<Expr>& PropagateRuleCommand::getHeads() const throw() { + return d_heads; +} + +Expr PropagateRuleCommand::getBody() const throw() { + return d_body; +} + +const PropagateRuleCommand::Triggers& PropagateRuleCommand::getTriggers() const throw() { + return d_triggers; +} + +bool PropagateRuleCommand::isDeduction() const throw() { + return d_deduction; +} + +void PropagateRuleCommand::invoke(SmtEngine* smtEngine) throw() { + try { + ExprManager* em = smtEngine->getExprManager(); + /** build vars list */ + Expr vars = em->mkExpr(kind::BOUND_VAR_LIST, d_vars); + /** build guards list */ + Expr guards; + if(d_guards.size() == 0) guards = em->mkConst<bool>(true); + else if(d_guards.size() == 1) guards = d_guards[0]; + else guards = em->mkExpr(kind::AND,d_guards); + /** build heads list */ + Expr heads; + if(d_heads.size() == 1) heads = d_heads[0]; + else heads = em->mkExpr(kind::AND,d_heads); + /** build expression */ + Expr expr; + if( d_triggers.empty() ){ + expr = em->mkExpr(kind::RR_REWRITE,vars,guards,heads,d_body); + } else { + /** build triggers list */ + std::vector<Expr> vtriggers; + vtriggers.reserve(d_triggers.size()); + for(Triggers::const_iterator i = d_triggers.begin(), + end = d_triggers.end(); i != end; ++i){ + vtriggers.push_back(em->mkExpr(kind::INST_PATTERN,*i)); + } + Expr triggers = em->mkExpr(kind::INST_PATTERN_LIST,vtriggers); + expr = em->mkExpr(kind::RR_REWRITE,vars,guards,heads,d_body,triggers); + } + smtEngine->assertFormula(expr); + d_commandStatus = CommandSuccess::instance(); + } catch(exception& e) { + d_commandStatus = new CommandFailure(e.what()); + } +} + +Command* PropagateRuleCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + /** Convert variables */ + VExpr vars; vars.reserve(d_vars.size()); + for(VExpr::iterator i = d_vars.begin(), end = d_vars.end(); + i == end; ++i){ + vars.push_back(i->exportTo(exprManager, variableMap)); + }; + /** Convert guards */ + VExpr guards; guards.reserve(d_guards.size()); + for(VExpr::iterator i = d_guards.begin(), end = d_guards.end(); + i == end; ++i){ + guards.push_back(i->exportTo(exprManager, variableMap)); + }; + /** Convert heads */ + VExpr heads; heads.reserve(d_heads.size()); + for(VExpr::iterator i = d_heads.begin(), end = d_heads.end(); + i == end; ++i){ + heads.push_back(i->exportTo(exprManager, variableMap)); + }; + /** Convert triggers */ + Triggers triggers; triggers.resize(d_triggers.size()); + for(size_t i = 0, end = d_triggers.size(); + i < end; ++i){ + triggers[i].reserve(d_triggers[i].size()); + for(VExpr::iterator j = d_triggers[i].begin(), jend = d_triggers[i].end(); + j == jend; ++i){ + triggers[i].push_back(j->exportTo(exprManager, variableMap)); + }; + }; + /** Convert head and body */ + Expr body = d_body.exportTo(exprManager, variableMap); + /** Create the converted rules */ + return new PropagateRuleCommand(vars, guards, heads, body, triggers); +} + +Command* PropagateRuleCommand::clone() const { + return new PropagateRuleCommand(d_vars, d_guards, d_heads, d_body, d_triggers); +} + +std::string PropagateRuleCommand::getCommandName() const throw() { + return "propagate-rule"; +} + +/* output stream insertion operator for benchmark statuses */ +std::ostream& operator<<(std::ostream& out, + BenchmarkStatus status) throw() { + switch(status) { + + case SMT_SATISFIABLE: + return out << "sat"; + + case SMT_UNSATISFIABLE: + return out << "unsat"; + + case SMT_UNKNOWN: + return out << "unknown"; + + default: + return out << "BenchmarkStatus::[UNKNOWNSTATUS!]"; + } +} + +}/* CVC4 namespace */ diff --git a/src/smt_util/command.h b/src/smt_util/command.h new file mode 100644 index 000000000..b35fb7a7f --- /dev/null +++ b/src/smt_util/command.h @@ -0,0 +1,904 @@ +/********************* */ +/*! \file command.h + ** \verbatim + ** Original author: Morgan Deters + ** Major contributors: none + ** Minor contributors (to current version): Kshitij Bansal, Christopher L. Conway, Dejan Jovanovic, Francois Bobot, Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2014 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Implementation of the command pattern on SmtEngines. + ** + ** Implementation of the command pattern on SmtEngines. Command + ** objects are generated by the parser (typically) to implement the + ** commands in parsed input (see Parser::parseNextCommand()), or by + ** client code. + **/ + +#include "cvc4_public.h" + +#ifndef __CVC4__COMMAND_H +#define __CVC4__COMMAND_H + +#include <iostream> +#include <sstream> +#include <string> +#include <vector> +#include <map> + +#include "expr/datatype.h" +#include "expr/expr.h" +#include "expr/result.h" +#include "expr/sexpr.h" +#include "expr/type.h" +#include "expr/variable_type_map.h" +#include "proof/unsat_core.h" +#include "util/proof.h" + +namespace CVC4 { + +class SmtEngine; +class Command; +class CommandStatus; +class Model; + +std::ostream& operator<<(std::ostream&, const Command&) throw() CVC4_PUBLIC; +std::ostream& operator<<(std::ostream&, const Command*) throw() CVC4_PUBLIC; +std::ostream& operator<<(std::ostream&, const CommandStatus&) throw() CVC4_PUBLIC; +std::ostream& operator<<(std::ostream&, const CommandStatus*) throw() CVC4_PUBLIC; + +/** The status an SMT benchmark can have */ +enum BenchmarkStatus { + /** Benchmark is satisfiable */ + SMT_SATISFIABLE, + /** Benchmark is unsatisfiable */ + SMT_UNSATISFIABLE, + /** The status of the benchmark is unknown */ + SMT_UNKNOWN +};/* enum BenchmarkStatus */ + +std::ostream& operator<<(std::ostream& out, + BenchmarkStatus status) throw() CVC4_PUBLIC; + +/** + * IOStream manipulator to print success messages or not. + * + * out << Command::printsuccess(false) << CommandSuccess(); + * + * prints nothing, but + * + * out << Command::printsuccess(true) << CommandSuccess(); + * + * prints a success message (in a manner appropriate for the current + * output language). + */ +class CVC4_PUBLIC CommandPrintSuccess { + /** + * The allocated index in ios_base for our depth setting. + */ + static const int s_iosIndex; + + /** + * The default setting, for ostreams that haven't yet had a + * setdepth() applied to them. + */ + static const int s_defaultPrintSuccess = false; + + /** + * When this manipulator is used, the setting is stored here. + */ + bool d_printSuccess; + +public: + /** + * Construct a CommandPrintSuccess with the given setting. + */ + CommandPrintSuccess(bool printSuccess) throw() : d_printSuccess(printSuccess) {} + + inline void applyPrintSuccess(std::ostream& out) throw() { + out.iword(s_iosIndex) = d_printSuccess; + } + + static inline bool getPrintSuccess(std::ostream& out) throw() { + return out.iword(s_iosIndex); + } + + static inline void setPrintSuccess(std::ostream& out, bool printSuccess) throw() { + out.iword(s_iosIndex) = printSuccess; + } + + /** + * Set the print-success state on the output stream for the current + * stack scope. This makes sure the old state is reset on the + * stream after normal OR exceptional exit from the scope, using the + * RAII C++ idiom. + */ + class Scope { + std::ostream& d_out; + bool d_oldPrintSuccess; + + public: + + inline Scope(std::ostream& out, bool printSuccess) throw() : + d_out(out), + d_oldPrintSuccess(CommandPrintSuccess::getPrintSuccess(out)) { + CommandPrintSuccess::setPrintSuccess(out, printSuccess); + } + + inline ~Scope() throw() { + CommandPrintSuccess::setPrintSuccess(d_out, d_oldPrintSuccess); + } + + };/* class CommandPrintSuccess::Scope */ + +};/* class CommandPrintSuccess */ + +/** + * Sets the default print-success setting when pretty-printing an Expr + * to an ostream. Use like this: + * + * // let out be an ostream, e an Expr + * out << Expr::setdepth(n) << e << endl; + * + * The depth stays permanently (until set again) with the stream. + */ +inline std::ostream& operator<<(std::ostream& out, CommandPrintSuccess cps) throw() CVC4_PUBLIC; +inline std::ostream& operator<<(std::ostream& out, CommandPrintSuccess cps) throw() { + cps.applyPrintSuccess(out); + return out; +} + +class CVC4_PUBLIC CommandStatus { +protected: + // shouldn't construct a CommandStatus (use a derived class) + CommandStatus() throw() {} +public: + virtual ~CommandStatus() throw() {} + void toStream(std::ostream& out, + OutputLanguage language = language::output::LANG_AUTO) const throw(); + virtual CommandStatus& clone() const = 0; +};/* class CommandStatus */ + +class CVC4_PUBLIC CommandSuccess : public CommandStatus { + static const CommandSuccess* s_instance; +public: + static const CommandSuccess* instance() throw() { return s_instance; } + CommandStatus& clone() const { return const_cast<CommandSuccess&>(*this); } +};/* class CommandSuccess */ + +class CVC4_PUBLIC CommandInterrupted : public CommandStatus { + static const CommandInterrupted* s_instance; +public: + static const CommandInterrupted* instance() throw() { return s_instance; } + CommandStatus& clone() const { return const_cast<CommandInterrupted&>(*this); } +};/* class CommandInterrupted */ + +class CVC4_PUBLIC CommandUnsupported : public CommandStatus { +public: + CommandStatus& clone() const { return *new CommandUnsupported(*this); } +};/* class CommandSuccess */ + +class CVC4_PUBLIC CommandFailure : public CommandStatus { + std::string d_message; +public: + CommandFailure(std::string message) throw() : d_message(message) {} + CommandFailure& clone() const { return *new CommandFailure(*this); } + ~CommandFailure() throw() {} + std::string getMessage() const throw() { return d_message; } +};/* class CommandFailure */ + +class CVC4_PUBLIC Command { +protected: + /** + * This field contains a command status if the command has been + * invoked, or NULL if it has not. This field is either a + * dynamically-allocated pointer, or it's a pointer to the singleton + * CommandSuccess instance. Doing so is somewhat asymmetric, but + * it avoids the need to dynamically allocate memory in the common + * case of a successful command. + */ + const CommandStatus* d_commandStatus; + + /** + * True if this command is "muted"---i.e., don't print "success" on + * successful execution. + */ + bool d_muted; + +public: + typedef CommandPrintSuccess printsuccess; + + Command() throw(); + Command(const Command& cmd); + + virtual ~Command() throw(); + + virtual void invoke(SmtEngine* smtEngine) throw() = 0; + virtual void invoke(SmtEngine* smtEngine, std::ostream& out) throw(); + + virtual void toStream(std::ostream& out, int toDepth = -1, bool types = false, size_t dag = 1, + OutputLanguage language = language::output::LANG_AUTO) const throw(); + + std::string toString() const throw(); + + virtual std::string getCommandName() const throw() = 0; + + /** + * If false, instruct this Command not to print a success message. + */ + void setMuted(bool muted) throw() { d_muted = muted; } + + /** + * Determine whether this Command will print a success message. + */ + bool isMuted() throw() { return d_muted; } + + /** + * Either the command hasn't run yet, or it completed successfully + * (CommandSuccess, not CommandUnsupported or CommandFailure). + */ + bool ok() const throw(); + + /** + * The command completed in a failure state (CommandFailure, not + * CommandSuccess or CommandUnsupported). + */ + bool fail() const throw(); + + /** + * The command was ran but was interrupted due to resource limiting. + */ + bool interrupted() const throw(); + + /** Get the command status (it's NULL if we haven't run yet). */ + const CommandStatus* getCommandStatus() const throw() { return d_commandStatus; } + + virtual void printResult(std::ostream& out, uint32_t verbosity = 2) const throw(); + + /** + * Maps this Command into one for a different ExprManager, using + * variableMap for the translation and extending it with any new + * mappings. + */ + virtual Command* exportTo(ExprManager* exprManager, + ExprManagerMapCollection& variableMap) = 0; + + /** + * Clone this Command (make a shallow copy). + */ + virtual Command* clone() const = 0; + +protected: + class ExportTransformer { + ExprManager* d_exprManager; + ExprManagerMapCollection& d_variableMap; + public: + ExportTransformer(ExprManager* exprManager, ExprManagerMapCollection& variableMap) : + d_exprManager(exprManager), + d_variableMap(variableMap) { + } + Expr operator()(Expr e) { + return e.exportTo(d_exprManager, d_variableMap); + } + Type operator()(Type t) { + return t.exportTo(d_exprManager, d_variableMap); + } + };/* class Command::ExportTransformer */ +};/* class Command */ + +/** + * EmptyCommands are the residue of a command after the parser handles + * them (and there's nothing left to do). + */ +class CVC4_PUBLIC EmptyCommand : public Command { +protected: + std::string d_name; +public: + EmptyCommand(std::string name = "") throw(); + ~EmptyCommand() throw() {} + std::string getName() const throw(); + void invoke(SmtEngine* smtEngine) throw(); + Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); + Command* clone() const; + std::string getCommandName() const throw(); +};/* class EmptyCommand */ + +class CVC4_PUBLIC EchoCommand : public Command { +protected: + std::string d_output; +public: + EchoCommand(std::string output = "") throw(); + ~EchoCommand() throw() {} + std::string getOutput() const throw(); + void invoke(SmtEngine* smtEngine) throw(); + void invoke(SmtEngine* smtEngine, std::ostream& out) throw(); + Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); + Command* clone() const; + std::string getCommandName() const throw(); +};/* class EchoCommand */ + +class CVC4_PUBLIC AssertCommand : public Command { +protected: + Expr d_expr; + bool d_inUnsatCore; +public: + AssertCommand(const Expr& e, bool inUnsatCore = true) throw(); + ~AssertCommand() throw() {} + Expr getExpr() const throw(); + void invoke(SmtEngine* smtEngine) throw(); + Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); + Command* clone() const; + std::string getCommandName() const throw(); +};/* class AssertCommand */ + +class CVC4_PUBLIC PushCommand : public Command { +public: + ~PushCommand() throw() {} + void invoke(SmtEngine* smtEngine) throw(); + Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); + Command* clone() const; + std::string getCommandName() const throw(); +};/* class PushCommand */ + +class CVC4_PUBLIC PopCommand : public Command { +public: + ~PopCommand() throw() {} + void invoke(SmtEngine* smtEngine) throw(); + Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); + Command* clone() const; + std::string getCommandName() const throw(); +};/* class PopCommand */ + +class CVC4_PUBLIC DeclarationDefinitionCommand : public Command { +protected: + std::string d_symbol; +public: + DeclarationDefinitionCommand(const std::string& id) throw(); + ~DeclarationDefinitionCommand() throw() {} + virtual void invoke(SmtEngine* smtEngine) throw() = 0; + std::string getSymbol() const throw(); +};/* class DeclarationDefinitionCommand */ + +class CVC4_PUBLIC DeclareFunctionCommand : public DeclarationDefinitionCommand { +protected: + Expr d_func; + Type d_type; + bool d_printInModel; + bool d_printInModelSetByUser; +public: + DeclareFunctionCommand(const std::string& id, Expr func, Type type) throw(); + ~DeclareFunctionCommand() throw() {} + Expr getFunction() const throw(); + Type getType() const throw(); + bool getPrintInModel() const throw(); + bool getPrintInModelSetByUser() const throw(); + void setPrintInModel( bool p ); + void invoke(SmtEngine* smtEngine) throw(); + Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); + Command* clone() const; + std::string getCommandName() const throw(); +};/* class DeclareFunctionCommand */ + +class CVC4_PUBLIC DeclareTypeCommand : public DeclarationDefinitionCommand { +protected: + size_t d_arity; + Type d_type; +public: + DeclareTypeCommand(const std::string& id, size_t arity, Type t) throw(); + ~DeclareTypeCommand() throw() {} + size_t getArity() const throw(); + Type getType() const throw(); + void invoke(SmtEngine* smtEngine) throw(); + Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); + Command* clone() const; + std::string getCommandName() const throw(); +};/* class DeclareTypeCommand */ + +class CVC4_PUBLIC DefineTypeCommand : public DeclarationDefinitionCommand { +protected: + std::vector<Type> d_params; + Type d_type; +public: + DefineTypeCommand(const std::string& id, Type t) throw(); + DefineTypeCommand(const std::string& id, const std::vector<Type>& params, Type t) throw(); + ~DefineTypeCommand() throw() {} + const std::vector<Type>& getParameters() const throw(); + Type getType() const throw(); + void invoke(SmtEngine* smtEngine) throw(); + Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); + Command* clone() const; + std::string getCommandName() const throw(); +};/* class DefineTypeCommand */ + +class CVC4_PUBLIC DefineFunctionCommand : public DeclarationDefinitionCommand { +protected: + Expr d_func; + std::vector<Expr> d_formals; + Expr d_formula; +public: + DefineFunctionCommand(const std::string& id, Expr func, Expr formula) throw(); + DefineFunctionCommand(const std::string& id, Expr func, + const std::vector<Expr>& formals, Expr formula) throw(); + ~DefineFunctionCommand() throw() {} + Expr getFunction() const throw(); + const std::vector<Expr>& getFormals() const throw(); + Expr getFormula() const throw(); + void invoke(SmtEngine* smtEngine) throw(); + Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); + Command* clone() const; + std::string getCommandName() const throw(); +};/* class DefineFunctionCommand */ + +/** + * This differs from DefineFunctionCommand only in that it instructs + * the SmtEngine to "remember" this function for later retrieval with + * getAssignment(). Used for :named attributes in SMT-LIBv2. + */ +class CVC4_PUBLIC DefineNamedFunctionCommand : public DefineFunctionCommand { +public: + DefineNamedFunctionCommand(const std::string& id, Expr func, + const std::vector<Expr>& formals, Expr formula) throw(); + void invoke(SmtEngine* smtEngine) throw(); + Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); + Command* clone() const; +};/* class DefineNamedFunctionCommand */ + +/** + * The command when an attribute is set by a user. In SMT-LIBv2 this is done + * via the syntax (! expr :attr) + */ +class CVC4_PUBLIC SetUserAttributeCommand : public Command { +protected: + std::string d_attr; + Expr d_expr; + std::vector<Expr> d_expr_values; + std::string d_str_value; +public: + SetUserAttributeCommand( const std::string& attr, Expr expr ) throw(); + SetUserAttributeCommand( const std::string& attr, Expr expr, std::vector<Expr>& values ) throw(); + SetUserAttributeCommand( const std::string& attr, Expr expr, const std::string& value ) throw(); + ~SetUserAttributeCommand() throw() {} + void invoke(SmtEngine* smtEngine) throw(); + Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); + Command* clone() const; + std::string getCommandName() const throw(); +};/* class SetUserAttributeCommand */ + +class CVC4_PUBLIC CheckSatCommand : public Command { +protected: + Expr d_expr; + Result d_result; + bool d_inUnsatCore; +public: + CheckSatCommand() throw(); + CheckSatCommand(const Expr& expr, bool inUnsatCore = true) throw(); + ~CheckSatCommand() throw() {} + Expr getExpr() const throw(); + void invoke(SmtEngine* smtEngine) throw(); + Result getResult() const throw(); + void printResult(std::ostream& out, uint32_t verbosity = 2) const throw(); + Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); + Command* clone() const; + std::string getCommandName() const throw(); +};/* class CheckSatCommand */ + +class CVC4_PUBLIC QueryCommand : public Command { +protected: + Expr d_expr; + Result d_result; + bool d_inUnsatCore; +public: + QueryCommand(const Expr& e, bool inUnsatCore = true) throw(); + ~QueryCommand() throw() {} + Expr getExpr() const throw(); + void invoke(SmtEngine* smtEngine) throw(); + Result getResult() const throw(); + void printResult(std::ostream& out, uint32_t verbosity = 2) const throw(); + Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); + Command* clone() const; + std::string getCommandName() const throw(); +};/* class QueryCommand */ + +// this is TRANSFORM in the CVC presentation language +class CVC4_PUBLIC SimplifyCommand : public Command { +protected: + Expr d_term; + Expr d_result; +public: + SimplifyCommand(Expr term) throw(); + ~SimplifyCommand() throw() {} + Expr getTerm() const throw(); + void invoke(SmtEngine* smtEngine) throw(); + Expr getResult() const throw(); + void printResult(std::ostream& out, uint32_t verbosity = 2) const throw(); + Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); + Command* clone() const; + std::string getCommandName() const throw(); +};/* class SimplifyCommand */ + +class CVC4_PUBLIC ExpandDefinitionsCommand : public Command { +protected: + Expr d_term; + Expr d_result; +public: + ExpandDefinitionsCommand(Expr term) throw(); + ~ExpandDefinitionsCommand() throw() {} + Expr getTerm() const throw(); + void invoke(SmtEngine* smtEngine) throw(); + Expr getResult() const throw(); + void printResult(std::ostream& out, uint32_t verbosity = 2) const throw(); + Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); + Command* clone() const; + std::string getCommandName() const throw(); +};/* class ExpandDefinitionsCommand */ + +class CVC4_PUBLIC GetValueCommand : public Command { +protected: + std::vector<Expr> d_terms; + Expr d_result; +public: + GetValueCommand(Expr term) throw(); + GetValueCommand(const std::vector<Expr>& terms) throw(); + ~GetValueCommand() throw() {} + const std::vector<Expr>& getTerms() const throw(); + void invoke(SmtEngine* smtEngine) throw(); + Expr getResult() const throw(); + void printResult(std::ostream& out, uint32_t verbosity = 2) const throw(); + Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); + Command* clone() const; + std::string getCommandName() const throw(); +};/* class GetValueCommand */ + +class CVC4_PUBLIC GetAssignmentCommand : public Command { +protected: + SExpr d_result; +public: + GetAssignmentCommand() throw(); + ~GetAssignmentCommand() throw() {} + void invoke(SmtEngine* smtEngine) throw(); + SExpr getResult() const throw(); + void printResult(std::ostream& out, uint32_t verbosity = 2) const throw(); + Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); + Command* clone() const; + std::string getCommandName() const throw(); +};/* class GetAssignmentCommand */ + +class CVC4_PUBLIC GetModelCommand : public Command { +protected: + Model* d_result; + SmtEngine* d_smtEngine; +public: + GetModelCommand() throw(); + ~GetModelCommand() throw() {} + void invoke(SmtEngine* smtEngine) throw(); + // Model is private to the library -- for now + //Model* getResult() const throw(); + void printResult(std::ostream& out, uint32_t verbosity = 2) const throw(); + Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); + Command* clone() const; + std::string getCommandName() const throw(); +};/* class GetModelCommand */ + +class CVC4_PUBLIC GetProofCommand : public Command { +protected: + Proof* d_result; +public: + GetProofCommand() throw(); + ~GetProofCommand() throw() {} + void invoke(SmtEngine* smtEngine) throw(); + Proof* getResult() const throw(); + void printResult(std::ostream& out, uint32_t verbosity = 2) const throw(); + Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); + Command* clone() const; + std::string getCommandName() const throw(); +};/* class GetProofCommand */ + +class CVC4_PUBLIC GetInstantiationsCommand : public Command { +protected: + //Instantiations* d_result; + SmtEngine* d_smtEngine; +public: + GetInstantiationsCommand() throw(); + ~GetInstantiationsCommand() throw() {} + void invoke(SmtEngine* smtEngine) throw(); + //Instantiations* getResult() const throw(); + void printResult(std::ostream& out, uint32_t verbosity = 2) const throw(); + Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); + Command* clone() const; + std::string getCommandName() const throw(); +};/* class GetInstantiationsCommand */ + +class CVC4_PUBLIC GetSynthSolutionCommand : public Command { +protected: + SmtEngine* d_smtEngine; +public: + GetSynthSolutionCommand() throw(); + ~GetSynthSolutionCommand() throw() {} + void invoke(SmtEngine* smtEngine) throw(); + void printResult(std::ostream& out, uint32_t verbosity = 2) const throw(); + Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); + Command* clone() const; + std::string getCommandName() const throw(); +};/* class GetSynthSolutionCommand */ + +class CVC4_PUBLIC GetUnsatCoreCommand : public Command { +protected: + UnsatCore d_result; + std::map<Expr, std::string> d_names; +public: + GetUnsatCoreCommand() throw(); + GetUnsatCoreCommand(const std::map<Expr, std::string>& names) throw(); + ~GetUnsatCoreCommand() throw() {} + void invoke(SmtEngine* smtEngine) throw(); + void printResult(std::ostream& out, uint32_t verbosity = 2) const throw(); + const UnsatCore& getUnsatCore() const throw(); + Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); + Command* clone() const; + std::string getCommandName() const throw(); +};/* class GetUnsatCoreCommand */ + +class CVC4_PUBLIC GetAssertionsCommand : public Command { +protected: + std::string d_result; +public: + GetAssertionsCommand() throw(); + ~GetAssertionsCommand() throw() {} + void invoke(SmtEngine* smtEngine) throw(); + std::string getResult() const throw(); + void printResult(std::ostream& out, uint32_t verbosity = 2) const throw(); + Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); + Command* clone() const; + std::string getCommandName() const throw(); +};/* class GetAssertionsCommand */ + +class CVC4_PUBLIC SetBenchmarkStatusCommand : public Command { +protected: + BenchmarkStatus d_status; +public: + SetBenchmarkStatusCommand(BenchmarkStatus status) throw(); + ~SetBenchmarkStatusCommand() throw() {} + BenchmarkStatus getStatus() const throw(); + void invoke(SmtEngine* smtEngine) throw(); + Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); + Command* clone() const; + std::string getCommandName() const throw(); +};/* class SetBenchmarkStatusCommand */ + +class CVC4_PUBLIC SetBenchmarkLogicCommand : public Command { +protected: + std::string d_logic; +public: + SetBenchmarkLogicCommand(std::string logic) throw(); + ~SetBenchmarkLogicCommand() throw() {} + std::string getLogic() const throw(); + void invoke(SmtEngine* smtEngine) throw(); + Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); + Command* clone() const; + std::string getCommandName() const throw(); +};/* class SetBenchmarkLogicCommand */ + +class CVC4_PUBLIC SetInfoCommand : public Command { +protected: + std::string d_flag; + SExpr d_sexpr; +public: + SetInfoCommand(std::string flag, const SExpr& sexpr) throw(); + ~SetInfoCommand() throw() {} + std::string getFlag() const throw(); + SExpr getSExpr() const throw(); + void invoke(SmtEngine* smtEngine) throw(); + Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); + Command* clone() const; + std::string getCommandName() const throw(); +};/* class SetInfoCommand */ + +class CVC4_PUBLIC GetInfoCommand : public Command { +protected: + std::string d_flag; + std::string d_result; +public: + GetInfoCommand(std::string flag) throw(); + ~GetInfoCommand() throw() {} + std::string getFlag() const throw(); + void invoke(SmtEngine* smtEngine) throw(); + std::string getResult() const throw(); + void printResult(std::ostream& out, uint32_t verbosity = 2) const throw(); + Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); + Command* clone() const; + std::string getCommandName() const throw(); +};/* class GetInfoCommand */ + +class CVC4_PUBLIC SetOptionCommand : public Command { +protected: + std::string d_flag; + SExpr d_sexpr; +public: + SetOptionCommand(std::string flag, const SExpr& sexpr) throw(); + ~SetOptionCommand() throw() {} + std::string getFlag() const throw(); + SExpr getSExpr() const throw(); + void invoke(SmtEngine* smtEngine) throw(); + Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); + Command* clone() const; + std::string getCommandName() const throw(); +};/* class SetOptionCommand */ + +class CVC4_PUBLIC GetOptionCommand : public Command { +protected: + std::string d_flag; + std::string d_result; +public: + GetOptionCommand(std::string flag) throw(); + ~GetOptionCommand() throw() {} + std::string getFlag() const throw(); + void invoke(SmtEngine* smtEngine) throw(); + std::string getResult() const throw(); + void printResult(std::ostream& out, uint32_t verbosity = 2) const throw(); + Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); + Command* clone() const; + std::string getCommandName() const throw(); +};/* class GetOptionCommand */ + +class CVC4_PUBLIC DatatypeDeclarationCommand : public Command { +private: + std::vector<DatatypeType> d_datatypes; +public: + DatatypeDeclarationCommand(const DatatypeType& datatype) throw(); + ~DatatypeDeclarationCommand() throw() {} + DatatypeDeclarationCommand(const std::vector<DatatypeType>& datatypes) throw(); + const std::vector<DatatypeType>& getDatatypes() const throw(); + void invoke(SmtEngine* smtEngine) throw(); + Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); + Command* clone() const; + std::string getCommandName() const throw(); +};/* class DatatypeDeclarationCommand */ + +class CVC4_PUBLIC RewriteRuleCommand : public Command { +public: + typedef std::vector< std::vector< Expr > > Triggers; +protected: + typedef std::vector< Expr > VExpr; + VExpr d_vars; + VExpr d_guards; + Expr d_head; + Expr d_body; + Triggers d_triggers; +public: + RewriteRuleCommand(const std::vector<Expr>& vars, + const std::vector<Expr>& guards, + Expr head, + Expr body, + const Triggers& d_triggers) throw(); + RewriteRuleCommand(const std::vector<Expr>& vars, + Expr head, + Expr body) throw(); + ~RewriteRuleCommand() throw() {} + const std::vector<Expr>& getVars() const throw(); + const std::vector<Expr>& getGuards() const throw(); + Expr getHead() const throw(); + Expr getBody() const throw(); + const Triggers& getTriggers() const throw(); + void invoke(SmtEngine* smtEngine) throw(); + Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); + Command* clone() const; + std::string getCommandName() const throw(); +};/* class RewriteRuleCommand */ + +class CVC4_PUBLIC PropagateRuleCommand : public Command { +public: + typedef std::vector< std::vector< Expr > > Triggers; +protected: + typedef std::vector< Expr > VExpr; + VExpr d_vars; + VExpr d_guards; + VExpr d_heads; + Expr d_body; + Triggers d_triggers; + bool d_deduction; +public: + PropagateRuleCommand(const std::vector<Expr>& vars, + const std::vector<Expr>& guards, + const std::vector<Expr>& heads, + Expr body, + const Triggers& d_triggers, + /* true if we want a deduction rule */ + bool d_deduction = false) throw(); + PropagateRuleCommand(const std::vector<Expr>& vars, + const std::vector<Expr>& heads, + Expr body, + bool d_deduction = false) throw(); + ~PropagateRuleCommand() throw() {} + const std::vector<Expr>& getVars() const throw(); + const std::vector<Expr>& getGuards() const throw(); + const std::vector<Expr>& getHeads() const throw(); + Expr getBody() const throw(); + const Triggers& getTriggers() const throw(); + bool isDeduction() const throw(); + void invoke(SmtEngine* smtEngine) throw(); + Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); + Command* clone() const; + std::string getCommandName() const throw(); +};/* class PropagateRuleCommand */ + +class CVC4_PUBLIC ResetCommand : public Command { +public: + ResetCommand() throw() {} + ~ResetCommand() throw() {} + void invoke(SmtEngine* smtEngine) throw(); + Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); + Command* clone() const; + std::string getCommandName() const throw(); +};/* class ResetCommand */ + +class CVC4_PUBLIC ResetAssertionsCommand : public Command { +public: + ResetAssertionsCommand() throw() {} + ~ResetAssertionsCommand() throw() {} + void invoke(SmtEngine* smtEngine) throw(); + Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); + Command* clone() const; + std::string getCommandName() const throw(); +};/* class ResetAssertionsCommand */ + +class CVC4_PUBLIC QuitCommand : public Command { +public: + QuitCommand() throw() {} + ~QuitCommand() throw() {} + void invoke(SmtEngine* smtEngine) throw(); + Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); + Command* clone() const; + std::string getCommandName() const throw(); +};/* class QuitCommand */ + +class CVC4_PUBLIC CommentCommand : public Command { + std::string d_comment; +public: + CommentCommand(std::string comment) throw(); + ~CommentCommand() throw() {} + std::string getComment() const throw(); + void invoke(SmtEngine* smtEngine) throw(); + Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); + Command* clone() const; + std::string getCommandName() const throw(); +};/* class CommentCommand */ + +class CVC4_PUBLIC CommandSequence : public Command { +private: + /** All the commands to be executed (in sequence) */ + std::vector<Command*> d_commandSequence; + /** Next command to be executed */ + unsigned int d_index; +public: + CommandSequence() throw(); + ~CommandSequence() throw(); + + void addCommand(Command* cmd) throw(); + void clear() throw(); + + void invoke(SmtEngine* smtEngine) throw(); + void invoke(SmtEngine* smtEngine, std::ostream& out) throw(); + + typedef std::vector<Command*>::iterator iterator; + typedef std::vector<Command*>::const_iterator const_iterator; + + const_iterator begin() const throw(); + const_iterator end() const throw(); + + iterator begin() throw(); + iterator end() throw(); + + Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); + Command* clone() const; + std::string getCommandName() const throw(); +};/* class CommandSequence */ + +class CVC4_PUBLIC DeclarationSequence : public CommandSequence { +public: + ~DeclarationSequence() throw() {} +};/* class DeclarationSequence */ + +}/* CVC4 namespace */ + +#endif /* __CVC4__COMMAND_H */ diff --git a/src/smt_util/command.i b/src/smt_util/command.i new file mode 100644 index 000000000..e4744c4f4 --- /dev/null +++ b/src/smt_util/command.i @@ -0,0 +1,77 @@ +%{ +#include "smt_util/command.h" + +#ifdef SWIGJAVA + +#include "bindings/java_iterator_adapter.h" +#include "bindings/java_stream_adapters.h" + +#endif /* SWIGJAVA */ +%} + +%ignore CVC4::operator<<(std::ostream&, const Command&) throw(); +%ignore CVC4::operator<<(std::ostream&, const Command*) throw(); +%ignore CVC4::operator<<(std::ostream&, const CommandStatus&) throw(); +%ignore CVC4::operator<<(std::ostream&, const CommandStatus*) throw(); +%ignore CVC4::operator<<(std::ostream&, BenchmarkStatus status) throw(); +%ignore CVC4::operator<<(std::ostream&, CommandPrintSuccess) throw(); + +%ignore CVC4::GetProofCommand; +%ignore CVC4::CommandPrintSuccess::Scope; + +#ifdef SWIGJAVA + +// Instead of CommandSequence::begin() and end(), create an +// iterator() method on the Java side that returns a Java-style +// Iterator. +%ignore CVC4::CommandSequence::begin(); +%ignore CVC4::CommandSequence::end(); +%ignore CVC4::CommandSequence::begin() const; +%ignore CVC4::CommandSequence::end() const; +%extend CVC4::CommandSequence { + CVC4::JavaIteratorAdapter<CVC4::CommandSequence> iterator() { + return CVC4::JavaIteratorAdapter<CVC4::CommandSequence>(*$self); + } +} + +// CommandSequence is "iterable" on the Java side +%typemap(javainterfaces) CVC4::CommandSequence "java.lang.Iterable<edu.nyu.acsys.CVC4.Command>"; + +// the JavaIteratorAdapter should not be public, and implements Iterator +%typemap(javaclassmodifiers) CVC4::JavaIteratorAdapter<CVC4::CommandSequence> "class"; +%typemap(javainterfaces) CVC4::JavaIteratorAdapter<CVC4::CommandSequence> "java.util.Iterator<edu.nyu.acsys.CVC4.Command>"; +// add some functions to the Java side (do it here because there's no way to do these in C++) +%typemap(javacode) CVC4::JavaIteratorAdapter<CVC4::CommandSequence> " + public void remove() { + throw new java.lang.UnsupportedOperationException(); + } + + public edu.nyu.acsys.CVC4.Command next() { + if(hasNext()) { + return getNext(); + } else { + throw new java.util.NoSuchElementException(); + } + } +" +// getNext() just allows C++ iterator access from Java-side next(), make it private +%javamethodmodifiers CVC4::JavaIteratorAdapter<CVC4::CommandSequence>::getNext() "private"; + +// map the types appropriately +%typemap(jni) CVC4::CommandSequence::const_iterator::value_type "jobject"; +%typemap(jtype) CVC4::CommandSequence::const_iterator::value_type "edu.nyu.acsys.CVC4.Command"; +%typemap(jstype) CVC4::CommandSequence::const_iterator::value_type "edu.nyu.acsys.CVC4.Command"; +%typemap(javaout) CVC4::CommandSequence::const_iterator::value_type { return $jnicall; } + +#endif /* SWIGJAVA */ + +%include "smt_util/command.h" + +#ifdef SWIGJAVA + +%include "bindings/java_iterator_adapter.h" +%include "bindings/java_stream_adapters.h" + +%template(JavaIteratorAdapter_CommandSequence) CVC4::JavaIteratorAdapter<CVC4::CommandSequence>; + +#endif /* SWIGJAVA */ diff --git a/src/smt_util/dump.cpp b/src/smt_util/dump.cpp new file mode 100644 index 000000000..56313f4d8 --- /dev/null +++ b/src/smt_util/dump.cpp @@ -0,0 +1,24 @@ +/********************* */ +/*! \file dump.cpp + ** \verbatim + ** Original author: Morgan Deters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2014 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Dump utility classes and functions + ** + ** Dump utility classes and functions. + **/ +#include "smt_util/dump.h" + +#include "base/output.h" + +namespace CVC4 { + +DumpC DumpChannel CVC4_PUBLIC; + +}/* CVC4 namespace */ diff --git a/src/smt_util/dump.h b/src/smt_util/dump.h new file mode 100644 index 000000000..1f4efe640 --- /dev/null +++ b/src/smt_util/dump.h @@ -0,0 +1,117 @@ +/********************* */ +/*! \file dump.h + ** \verbatim + ** Original author: Morgan Deters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2014 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Dump utility classes and functions + ** + ** Dump utility classes and functions. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__DUMP_H +#define __CVC4__DUMP_H + +#include "base/output.h" +#include "smt_util/command.h" + +namespace CVC4 { + +class CVC4_PUBLIC CVC4dumpstream { + +#if defined(CVC4_DUMPING) && !defined(CVC4_MUZZLE) + std::ostream* d_os; +#endif /* CVC4_DUMPING && !CVC4_MUZZLE */ + +#ifdef CVC4_PORTFOLIO + CommandSequence* d_commands; +#endif /* CVC4_PORTFOLIO */ + +public: + CVC4dumpstream() throw() +#if defined(CVC4_DUMPING) && !defined(CVC4_MUZZLE) && defined(CVC4_PORTFOLIO) + : d_os(NULL), d_commands(NULL) +#elif defined(CVC4_DUMPING) && !defined(CVC4_MUZZLE) + : d_os(NULL) +#elif defined(CVC4_PORTFOLIO) + : d_commands(NULL) +#endif /* CVC4_PORTFOLIO */ + { } + + CVC4dumpstream(std::ostream& os, CommandSequence& commands) throw() +#if defined(CVC4_DUMPING) && !defined(CVC4_MUZZLE) && defined(CVC4_PORTFOLIO) + : d_os(&os), d_commands(&commands) +#elif defined(CVC4_DUMPING) && !defined(CVC4_MUZZLE) + : d_os(&os) +#elif defined(CVC4_PORTFOLIO) + : d_commands(&commands) +#endif /* CVC4_PORTFOLIO */ + { } + + CVC4dumpstream& operator<<(const Command& c) { +#if defined(CVC4_DUMPING) && !defined(CVC4_MUZZLE) + if(d_os != NULL) { + (*d_os) << c << std::endl; + } +#endif +#if defined(CVC4_PORTFOLIO) + if(d_commands != NULL) { + d_commands->addCommand(c.clone()); + } +#endif + return *this; + } +};/* class CVC4dumpstream */ + +/** The dump class */ +class CVC4_PUBLIC DumpC { + std::set<std::string> d_tags; + CommandSequence d_commands; + +public: + CVC4dumpstream operator()(const char* tag) { + if(!d_tags.empty() && d_tags.find(std::string(tag)) != d_tags.end()) { + return CVC4dumpstream(getStream(), d_commands); + } else { + return CVC4dumpstream(); + } + } + CVC4dumpstream operator()(std::string tag) { + if(!d_tags.empty() && d_tags.find(tag) != d_tags.end()) { + return CVC4dumpstream(getStream(), d_commands); + } else { + return CVC4dumpstream(); + } + } + + void clear() { d_commands.clear(); } + const CommandSequence& getCommands() const { return d_commands; } + + bool on (const char* tag) { d_tags.insert(std::string(tag)); return true; } + bool on (std::string tag) { d_tags.insert(tag); return true; } + bool off(const char* tag) { d_tags.erase (std::string(tag)); return false; } + bool off(std::string tag) { d_tags.erase (tag); return false; } + bool off() { d_tags.clear(); return false; } + + bool isOn(const char* tag) { return d_tags.find(std::string(tag)) != d_tags.end(); } + bool isOn(std::string tag) { return d_tags.find(tag) != d_tags.end(); } + + std::ostream& setStream(std::ostream& os) { DumpOut.setStream(os); return os; } + std::ostream& getStream() { return DumpOut.getStream(); } +};/* class DumpC */ + +/** The dump singleton */ +extern DumpC DumpChannel CVC4_PUBLIC; + +#define Dump ::CVC4::DumpChannel + +}/* CVC4 namespace */ + +#endif /* __CVC4__DUMP_H */ diff --git a/src/smt_util/ite_removal.cpp b/src/smt_util/ite_removal.cpp new file mode 100644 index 000000000..0d1c7b61e --- /dev/null +++ b/src/smt_util/ite_removal.cpp @@ -0,0 +1,192 @@ +/********************* */ +/*! \file ite_removal.cpp + ** \verbatim + ** Original author: Dejan Jovanovic + ** Major contributors: Tim King, Morgan Deters + ** Minor contributors (to current version): Kshitij Bansal, Andrew Reynolds, Clark Barrett + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2014 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Removal of term ITEs + ** + ** Removal of term ITEs. + **/ +#include "smt_util/ite_removal.h" + +#include <vector> + +#include "proof/proof_manager.h" +#include "smt_util/command.h" +#include "theory/ite_utilities.h" + +using namespace CVC4; +using namespace std; + +namespace CVC4 { + +RemoveITE::RemoveITE(context::UserContext* u) + : d_iteCache(u) +{ + d_containsVisitor = new theory::ContainsTermITEVisitor(); +} + +RemoveITE::~RemoveITE(){ + delete d_containsVisitor; +} + +void RemoveITE::garbageCollect(){ + d_containsVisitor->garbageCollect(); +} + +theory::ContainsTermITEVisitor* RemoveITE::getContainsVisitor() { + return d_containsVisitor; +} + +size_t RemoveITE::collectedCacheSizes() const{ + return d_containsVisitor->cache_size() + d_iteCache.size(); +} + +void RemoveITE::run(std::vector<Node>& output, IteSkolemMap& iteSkolemMap, bool reportDeps) +{ + size_t n = output.size(); + for (unsigned i = 0, i_end = output.size(); i < i_end; ++ i) { + // Do this in two steps to avoid Node problems(?) + // Appears related to bug 512, splitting this into two lines + // fixes the bug on clang on Mac OS + Node itesRemoved = run(output[i], output, iteSkolemMap, false); + // In some calling contexts, not necessary to report dependence information. + if(reportDeps && options::unsatCores()) { + // new assertions have a dependence on the node + PROOF( ProofManager::currentPM()->addDependence(itesRemoved, output[i]); ) + while(n < output.size()) { + PROOF( ProofManager::currentPM()->addDependence(output[n], output[i]); ) + ++n; + } + } + output[i] = itesRemoved; + } +} + +bool RemoveITE::containsTermITE(TNode e) const { + return d_containsVisitor->containsTermITE(e); +} + +Node RemoveITE::run(TNode node, std::vector<Node>& output, + IteSkolemMap& iteSkolemMap, bool inQuant) { + // Current node + Debug("ite") << "removeITEs(" << node << ")" << endl; + + if(node.isVar() || node.isConst() || + (options::biasedITERemoval() && !containsTermITE(node))){ + return Node(node); + } + + // The result may be cached already + std::pair<Node, bool> cacheKey(node, inQuant); + NodeManager *nodeManager = NodeManager::currentNM(); + ITECache::const_iterator i = d_iteCache.find(cacheKey); + if(i != d_iteCache.end()) { + Node cached = (*i).second; + Debug("ite") << "removeITEs: in-cache: " << cached << endl; + return cached.isNull() ? Node(node) : cached; + } + + // Remember that we're inside a quantifier + if(node.getKind() == kind::FORALL || node.getKind() == kind::EXISTS) { + inQuant = true; + } + + // If an ITE replace it + if(node.getKind() == kind::ITE) { + TypeNode nodeType = node.getType(); + if(!nodeType.isBoolean() && (!inQuant || !node.hasBoundVar())) { + Node skolem; + // Make the skolem to represent the ITE + skolem = nodeManager->mkSkolem("termITE", nodeType, "a variable introduced due to term-level ITE removal"); + + // The new assertion + Node newAssertion = + nodeManager->mkNode(kind::ITE, node[0], skolem.eqNode(node[1]), + skolem.eqNode(node[2])); + Debug("ite") << "removeITEs(" << node << ") => " << newAssertion << endl; + + // Attach the skolem + d_iteCache.insert(cacheKey, skolem); + + // Remove ITEs from the new assertion, rewrite it and push it to the output + newAssertion = run(newAssertion, output, iteSkolemMap, inQuant); + + iteSkolemMap[skolem] = output.size(); + output.push_back(newAssertion); + + // The representation is now the skolem + return skolem; + } + } + + // If not an ITE, go deep + vector<Node> newChildren; + bool somethingChanged = false; + if(node.getMetaKind() == kind::metakind::PARAMETERIZED) { + newChildren.push_back(node.getOperator()); + } + // Remove the ITEs from the children + for(TNode::const_iterator it = node.begin(), end = node.end(); it != end; ++it) { + Node newChild = run(*it, output, iteSkolemMap, inQuant); + somethingChanged |= (newChild != *it); + newChildren.push_back(newChild); + } + + // If changes, we rewrite + if(somethingChanged) { + Node cached = nodeManager->mkNode(node.getKind(), newChildren); + d_iteCache.insert(cacheKey, cached); + return cached; + } else { + d_iteCache.insert(cacheKey, Node::null()); + return node; + } +} + +Node RemoveITE::replace(TNode node, bool inQuant) const { + if(node.isVar() || node.isConst() || + (options::biasedITERemoval() && !containsTermITE(node))){ + return Node(node); + } + + // Check the cache + NodeManager *nodeManager = NodeManager::currentNM(); + ITECache::const_iterator i = d_iteCache.find(make_pair(node, inQuant)); + if(i != d_iteCache.end()) { + Node cached = (*i).second; + return cached.isNull() ? Node(node) : cached; + } + + // Remember that we're inside a quantifier + if(node.getKind() == kind::FORALL || node.getKind() == kind::EXISTS) { + inQuant = true; + } + + vector<Node> newChildren; + bool somethingChanged = false; + if(node.getMetaKind() == kind::metakind::PARAMETERIZED) { + newChildren.push_back(node.getOperator()); + } + // Replace in children + for(TNode::const_iterator it = node.begin(), end = node.end(); it != end; ++it) { + Node newChild = replace(*it, inQuant); + somethingChanged |= (newChild != *it); + newChildren.push_back(newChild); + } + + // If changes, we rewrite + if(somethingChanged) { + return nodeManager->mkNode(node.getKind(), newChildren); + } else { + return node; + } +} + +}/* CVC4 namespace */ diff --git a/src/smt_util/ite_removal.h b/src/smt_util/ite_removal.h new file mode 100644 index 000000000..0cc0ea5d0 --- /dev/null +++ b/src/smt_util/ite_removal.h @@ -0,0 +1,93 @@ +/********************* */ +/*! \file ite_removal.h + ** \verbatim + ** Original author: Dejan Jovanovic + ** Major contributors: Kshitij Bansal, Tim King, Morgan Deters + ** Minor contributors (to current version): Clark Barrett + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2014 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Removal of term ITEs + ** + ** Removal of term ITEs. + **/ + +#include "cvc4_private.h" + +#pragma once + +#include <vector> + +#include "context/cdinsert_hashmap.h" +#include "context/context.h" +#include "expr/node.h" +#include "smt_util/dump.h" +#include "util/bool.h" +#include "util/hash.h" + +namespace CVC4 { + +namespace theory { + class ContainsTermITEVisitor; +}/* CVC4::theory namespace */ + +typedef std::hash_map<Node, unsigned, NodeHashFunction> IteSkolemMap; + +class RemoveITE { + typedef context::CDInsertHashMap< std::pair<Node, bool>, Node, PairHashFunction<Node, bool, NodeHashFunction, BoolHashFunction> > ITECache; + ITECache d_iteCache; + + +public: + + RemoveITE(context::UserContext* u); + ~RemoveITE(); + + /** + * Removes the ITE nodes by introducing skolem variables. All + * additional assertions are pushed into assertions. iteSkolemMap + * contains a map from introduced skolem variables to the index in + * assertions containing the new Boolean ite created in conjunction + * with that skolem variable. + * + * With reportDeps true, report reasoning dependences to the proof + * manager (for unsat cores). + */ + void run(std::vector<Node>& assertions, IteSkolemMap& iteSkolemMap, bool reportDeps = false); + + /** + * Removes the ITE from the node by introducing skolem + * variables. All additional assertions are pushed into + * assertions. iteSkolemMap contains a map from introduced skolem + * variables to the index in assertions containing the new Boolean + * ite created in conjunction with that skolem variable. + */ + Node run(TNode node, std::vector<Node>& additionalAssertions, + IteSkolemMap& iteSkolemMap, bool inQuant); + + /** + * Substitute under node using pre-existing cache. Do not remove + * any ITEs not seen during previous runs. + */ + Node replace(TNode node, bool inQuant = false) const; + + /** Returns true if e contains a term ite. */ + bool containsTermITE(TNode e) const; + + /** Returns the collected size of the caches. */ + size_t collectedCacheSizes() const; + + /** Garbage collects non-context dependent data-structures. */ + void garbageCollect(); + + /** Return the RemoveITE's containsVisitor. */ + theory::ContainsTermITEVisitor* getContainsVisitor(); + +private: + theory::ContainsTermITEVisitor* d_containsVisitor; + +};/* class RemoveTTE */ + +}/* CVC4 namespace */ diff --git a/src/smt_util/lemma_input_channel.h b/src/smt_util/lemma_input_channel.h new file mode 100644 index 000000000..66fe06424 --- /dev/null +++ b/src/smt_util/lemma_input_channel.h @@ -0,0 +1,39 @@ +/********************* */ +/*! \file lemma_input_channel.h + ** \verbatim + ** Original author: Morgan Deters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2014 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + +#include "cvc4_public.h" + +#ifndef __CVC4__LEMMA_INPUT_CHANNEL_H +#define __CVC4__LEMMA_INPUT_CHANNEL_H + +#include "base/lemma_input_channel_forward.h" +#include "expr/expr.h" + +namespace CVC4 { + +class CVC4_PUBLIC LemmaInputChannel { +public: + virtual ~LemmaInputChannel() throw() { } + + virtual bool hasNewLemma() = 0; + virtual Expr getNewLemma() = 0; + +};/* class LemmaOutputChannel */ + +}/* CVC4 namespace */ + +#endif /* __CVC4__LEMMA_INPUT_CHANNEL_H */ diff --git a/src/smt_util/lemma_output_channel.h b/src/smt_util/lemma_output_channel.h new file mode 100644 index 000000000..0fabe5721 --- /dev/null +++ b/src/smt_util/lemma_output_channel.h @@ -0,0 +1,47 @@ +/********************* */ +/*! \file lemma_output_channel.h + ** \verbatim + ** Original author: Morgan Deters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2014 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Mechanism for communication about new lemmas + ** + ** This file defines an interface for use by the theory and propositional + ** engines to communicate new lemmas to the "outside world," for example + ** for lemma sharing between threads. + **/ + +#include "cvc4_public.h" + +#ifndef __CVC4__LEMMA_OUTPUT_CHANNEL_H +#define __CVC4__LEMMA_OUTPUT_CHANNEL_H + +#include "base/lemma_output_channel_forward.h" +#include "expr/expr.h" + +namespace CVC4 { + +/** + * This interface describes a mechanism for the propositional and theory + * engines to communicate with the "outside world" about new lemmas being + * discovered. + */ +class CVC4_PUBLIC LemmaOutputChannel { +public: + virtual ~LemmaOutputChannel() throw() { } + + /** + * Notifies this output channel that there's a new lemma. + * The lemma may or may not be in CNF. + */ + virtual void notifyNewLemma(Expr lemma) = 0; +};/* class LemmaOutputChannel */ + +}/* CVC4 namespace */ + +#endif /* __CVC4__LEMMA_OUTPUT_CHANNEL_H */ diff --git a/src/smt_util/model.cpp b/src/smt_util/model.cpp new file mode 100644 index 000000000..3f0423f49 --- /dev/null +++ b/src/smt_util/model.cpp @@ -0,0 +1,53 @@ +/********************* */ +/*! \file model.cpp + ** \verbatim + ** Original author: Andrew Reynolds + ** Major contributors: Morgan Deters + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2014 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief implementation of Model class + **/ + +#include "smt_util/model.h" + +#include <vector> + +#include "smt_util/command.h" +#include "smt/smt_engine_scope.h" +#include "smt/command_list.h" +#include "printer/printer.h" + +using namespace std; + +namespace CVC4 { + +std::ostream& operator<<(std::ostream& out, const Model& m) { + smt::SmtScope smts(&m.d_smt); + Expr::dag::Scope scope(out, false); + Printer::getPrinter(options::outputLanguage())->toStream(out, m); + return out; +} + +Model::Model() : + d_smt(*smt::currentSmtEngine()) { +} + +size_t Model::getNumCommands() const { + return d_smt.d_modelCommands->size() + d_smt.d_modelGlobalCommands.size(); +} + +const Command* Model::getCommand(size_t i) const { + Assert(i < getNumCommands()); + // index the global commands first, then the locals + if(i < d_smt.d_modelGlobalCommands.size()) { + return d_smt.d_modelGlobalCommands[i]; + } else { + return (*d_smt.d_modelCommands)[i - d_smt.d_modelGlobalCommands.size()]; + } +} + +}/* CVC4 namespace */ diff --git a/src/smt_util/model.h b/src/smt_util/model.h new file mode 100644 index 000000000..98794a53d --- /dev/null +++ b/src/smt_util/model.h @@ -0,0 +1,78 @@ +/********************* */ +/*! \file model.h + ** \verbatim + ** Original author: Morgan Deters + ** Major contributors: Andrew Reynolds + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2014 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Model class + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__MODEL_H +#define __CVC4__MODEL_H + +#include <iostream> +#include <vector> + +#include "expr/expr.h" +#include "util/cardinality.h" + +namespace CVC4 { + +class Command; +class SmtEngine; +class Model; + +std::ostream& operator<<(std::ostream&, const Model&); + +class Model { + friend std::ostream& operator<<(std::ostream&, const Model&); + friend class SmtEngine; + + /** the input name (file name, etc.) this model is associated to */ + std::string d_inputName; + +protected: + /** The SmtEngine we're associated with */ + SmtEngine& d_smt; + + /** construct the base class; users cannot do this, only CVC4 internals */ + Model(); + +public: + /** virtual destructor */ + virtual ~Model() { } + /** get number of commands to report */ + size_t getNumCommands() const; + /** get command */ + const Command* getCommand(size_t i) const; + /** get the smt engine that this model is hooked up to */ + SmtEngine* getSmtEngine() { return &d_smt; } + /** get the smt engine (as a pointer-to-const) that this model is hooked up to */ + const SmtEngine* getSmtEngine() const { return &d_smt; } + /** get the input name (file name, etc.) this model is associated to */ + std::string getInputName() const { return d_inputName; } + +public: + /** get value for expression */ + virtual Expr getValue(Expr expr) const = 0; + /** get cardinality for sort */ + virtual Cardinality getCardinality(Type t) const = 0; +};/* class Model */ + +class ModelBuilder { +public: + ModelBuilder() { } + virtual ~ModelBuilder() { } + virtual void buildModel(Model* m, bool fullModel) = 0; +};/* class ModelBuilder */ + +}/* CVC4 namespace */ + +#endif /* __CVC4__MODEL_H */ diff --git a/src/smt_util/nary_builder.cpp b/src/smt_util/nary_builder.cpp new file mode 100644 index 000000000..ec012308f --- /dev/null +++ b/src/smt_util/nary_builder.cpp @@ -0,0 +1,200 @@ +/********************* */ +/*! \file nary_builder.cpp + ** \verbatim + ** Original author: Tim King + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2014 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ +#include "smt_util/nary_builder.h" + +#include "expr/metakind.h" + +using namespace std; + +namespace CVC4 { +namespace util { + +Node NaryBuilder::mkAssoc(Kind kind, const std::vector<Node>& children){ + if(children.size() == 0){ + return zeroArity(kind); + }else if(children.size() == 1){ + return children[0]; + }else{ + const unsigned int max = kind::metakind::getUpperBoundForKind(kind); + const unsigned int min = kind::metakind::getLowerBoundForKind(kind); + + Assert(min <= children.size()); + + unsigned int numChildren = children.size(); + NodeManager* nm = NodeManager::currentNM(); + if( numChildren <= max ) { + return nm->mkNode(kind,children); + } + + typedef std::vector<Node>::const_iterator const_iterator; + const_iterator it = children.begin() ; + const_iterator end = children.end() ; + + /* The new top-level children and the children of each sub node */ + std::vector<Node> newChildren; + std::vector<Node> subChildren; + + while( it != end && numChildren > max ) { + /* Grab the next max children and make a node for them. */ + for(const_iterator next = it + max; it != next; ++it, --numChildren ) { + subChildren.push_back(*it); + } + Node subNode = nm->mkNode(kind,subChildren); + newChildren.push_back(subNode); + subChildren.clear(); + } + + /* If there's children left, "top off" the Expr. */ + if(numChildren > 0) { + /* If the leftovers are too few, just copy them into newChildren; + * otherwise make a new sub-node */ + if(numChildren < min) { + for(; it != end; ++it) { + newChildren.push_back(*it); + } + } else { + for(; it != end; ++it) { + subChildren.push_back(*it); + } + Node subNode = nm->mkNode(kind, subChildren); + newChildren.push_back(subNode); + } + } + + /* It's inconceivable we could have enough children for this to fail + * (more than 2^32, in most cases?). */ + AlwaysAssert( newChildren.size() <= max, + "Too many new children in mkAssociative" ); + + /* It would be really weird if this happened (it would require + * min > 2, for one thing), but let's make sure. */ + AlwaysAssert( newChildren.size() >= min, + "Too few new children in mkAssociative" ); + + return nm->mkNode(kind,newChildren); + } +} + +Node NaryBuilder::zeroArity(Kind k){ + using namespace kind; + NodeManager* nm = NodeManager::currentNM(); + switch(k){ + case AND: + return nm->mkConst(true); + case OR: + return nm->mkConst(false); + case PLUS: + return nm->mkConst(Rational(0)); + case MULT: + return nm->mkConst(Rational(1)); + default: + return Node::null(); + } +} + + +RePairAssocCommutativeOperators::RePairAssocCommutativeOperators() + : d_cache() +{} +RePairAssocCommutativeOperators::~RePairAssocCommutativeOperators(){} +size_t RePairAssocCommutativeOperators::size() const{ return d_cache.size(); } +void RePairAssocCommutativeOperators::clear(){ d_cache.clear(); } + +bool RePairAssocCommutativeOperators::isAssociateCommutative(Kind k){ + using namespace kind; + switch(k){ + case BITVECTOR_CONCAT: + case BITVECTOR_AND: + case BITVECTOR_OR: + case BITVECTOR_XOR: + case BITVECTOR_MULT: + case BITVECTOR_PLUS: + case DISTINCT: + case PLUS: + case MULT: + case AND: + case OR: + return true; + default: + return false; + } +} + +Node RePairAssocCommutativeOperators::rePairAssocCommutativeOperators(TNode n){ + if(d_cache.find(n) != d_cache.end()){ + return d_cache[n]; + } + Node result = + isAssociateCommutative(n.getKind()) ? + case_assoccomm(n) : case_other(n); + + d_cache[n] = result; + return result; +} + +Node RePairAssocCommutativeOperators::case_assoccomm(TNode n){ + Kind k = n.getKind(); + Assert(isAssociateCommutative(k)); + Assert(n.getMetaKind() != kind::metakind::PARAMETERIZED); + unsigned N = n.getNumChildren(); + Assert(N >= 2); + + + Node last = rePairAssocCommutativeOperators( n[N-1]); + Node nextToLast = rePairAssocCommutativeOperators(n[N-2]); + + NodeManager* nm = NodeManager::currentNM(); + Node last2 = nm->mkNode(k, nextToLast, last); + + if(N <= 2){ + return last2; + } else{ + Assert(N > 2); + Node prevRound = last2; + for(unsigned prevPos = N-2; prevPos > 0; --prevPos){ + unsigned currPos = prevPos-1; + Node curr = rePairAssocCommutativeOperators(n[currPos]); + Node round = nm->mkNode(k, curr, prevRound); + prevRound = round; + } + return prevRound; + } +} + +Node RePairAssocCommutativeOperators::case_other(TNode n){ + if(n.isConst() || n.isVar()){ + return n; + } + + NodeBuilder<> nb(n.getKind()); + + if(n.getMetaKind() == kind::metakind::PARAMETERIZED) { + nb << n.getOperator(); + } + + // Remove the ITEs from the children + for(TNode::const_iterator i = n.begin(), end = n.end(); i != end; ++i) { + Node newChild = rePairAssocCommutativeOperators(*i); + nb << newChild; + } + + Node result = (Node)nb; + return result; +} + +}/* util namespace */ +}/* CVC4 namespace */ diff --git a/src/smt_util/nary_builder.h b/src/smt_util/nary_builder.h new file mode 100644 index 000000000..c98e01b1b --- /dev/null +++ b/src/smt_util/nary_builder.h @@ -0,0 +1,55 @@ +/********************* */ +/*! \file nary_builder.h + ** \verbatim + ** Original author: Tim King + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2014 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + + +#include "cvc4_private.h" + +#pragma once + +#include <vector> +#include "expr/node.h" + +namespace CVC4{ +namespace util { + +class NaryBuilder { +public: + static Node mkAssoc(Kind k, const std::vector<Node>& children); + static Node zeroArity(Kind k); +};/* class NaryBuilder */ + +class RePairAssocCommutativeOperators { +public: + RePairAssocCommutativeOperators(); + ~RePairAssocCommutativeOperators(); + + Node rePairAssocCommutativeOperators(TNode n); + + static bool isAssociateCommutative(Kind k); + + size_t size() const; + void clear(); +private: + Node case_assoccomm(TNode n); + Node case_other(TNode n); + + typedef std::hash_map<Node, Node, NodeHashFunction> NodeMap; + NodeMap d_cache; +};/* class RePairAssocCommutativeOperators */ + +}/* util namespace */ +}/* CVC4 namespace */ diff --git a/src/smt_util/node_visitor.h b/src/smt_util/node_visitor.h new file mode 100644 index 000000000..c8958b7b5 --- /dev/null +++ b/src/smt_util/node_visitor.h @@ -0,0 +1,120 @@ +/********************* */ +/*! \file node_visitor.h + ** \verbatim + ** Original author: Dejan Jovanovic + ** Major contributors: Liana Hadarean, Morgan Deters + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2014 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief A simple visitor for nodes + ** + ** A simple visitor for nodes. + **/ + +#pragma once + +#include "cvc4_private.h" + +#include <vector> + +#include "expr/node.h" + +namespace CVC4 { + +/** + * Traverses the nodes reverse-topologically (children before parents), + * calling the visitor in order. + */ +template<typename Visitor> +class NodeVisitor { + + /** For re-entry checking */ + static CVC4_THREADLOCAL(bool) s_inRun; + + /** + * Guard against NodeVisitor<> being re-entrant. + */ + template <class T> + class GuardReentry { + T& d_guard; + public: + GuardReentry(T& guard) + : d_guard(guard) { + Assert(!d_guard); + d_guard = true; + } + ~GuardReentry() { + Assert(d_guard); + d_guard = false; + } + };/* class NodeVisitor<>::GuardReentry */ + +public: + + /** + * Element of the stack. + */ + struct stack_element { + /** The node to be visited */ + TNode node; + /** The parent of the node */ + TNode parent; + /** Have the children been queued up for visitation */ + bool children_added; + stack_element(TNode node, TNode parent) + : node(node), parent(parent), children_added(false) {} + };/* struct preprocess_stack_element */ + + /** + * Performs the traversal. + */ + static typename Visitor::return_type run(Visitor& visitor, TNode node) { + + GuardReentry<CVC4_THREADLOCAL_TYPE(bool)> guard(s_inRun); + + // Notify of a start + visitor.start(node); + + // Do a reverse-topological sort of the subexpressions + std::vector<stack_element> toVisit; + toVisit.push_back(stack_element(node, node)); + while (!toVisit.empty()) { + stack_element& stackHead = toVisit.back(); + // The current node we are processing + TNode current = stackHead.node; + TNode parent = stackHead.parent; + + if (visitor.alreadyVisited(current, parent)) { + // If already visited, we're done + toVisit.pop_back(); + } else if (stackHead.children_added) { + // Call the visitor + visitor.visit(current, parent); + // Done with this node, remove from the stack + toVisit.pop_back(); + } else { + // Mark that we have added the children + stackHead.children_added = true; + // We need to add the children + for(TNode::iterator child_it = current.begin(); child_it != current.end(); ++ child_it) { + TNode childNode = *child_it; + if (!visitor.alreadyVisited(childNode, current)) { + toVisit.push_back(stack_element(childNode, current)); + } + } + } + } + + // Notify that we're done + return visitor.done(node); + } + +};/* class NodeVisitor<> */ + +template <typename Visitor> +CVC4_THREADLOCAL(bool) NodeVisitor<Visitor>::s_inRun = false; + +}/* CVC4 namespace */ |