summaryrefslogtreecommitdiff
path: root/src/smt_util
diff options
context:
space:
mode:
Diffstat (limited to 'src/smt_util')
-rw-r--r--src/smt_util/Makefile.am30
-rw-r--r--src/smt_util/boolean_simplification.cpp65
-rw-r--r--src/smt_util/boolean_simplification.h234
-rw-r--r--src/smt_util/command.cpp1848
-rw-r--r--src/smt_util/command.h904
-rw-r--r--src/smt_util/command.i77
-rw-r--r--src/smt_util/dump.cpp24
-rw-r--r--src/smt_util/dump.h117
-rw-r--r--src/smt_util/ite_removal.cpp192
-rw-r--r--src/smt_util/ite_removal.h93
-rw-r--r--src/smt_util/lemma_input_channel.h39
-rw-r--r--src/smt_util/lemma_output_channel.h47
-rw-r--r--src/smt_util/model.cpp53
-rw-r--r--src/smt_util/model.h78
-rw-r--r--src/smt_util/nary_builder.cpp200
-rw-r--r--src/smt_util/nary_builder.h55
-rw-r--r--src/smt_util/node_visitor.h120
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 */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback