Refactoring Options Handler & Library Cycle Breaking

What to Know As a User:
A number of files have moved. Users that include files in the public API in more refined ways than using #include <cvc4.h> should consult which files have moved. Note though that some files may move again after being cleaned up. A number of small tweaks have been made to the swig interfaces that may cause issues. Please file bug reports for any problems.

The Problem:
The build order of CVC4 used to be [roughly] specified as:
  options < expr < util < libcvc4 < parsers < main
Each of these had their own directories and their own Makefile.am files. With the exception of the util/ directory, each of the subdirectories built exactly one convenience library. The util/ directory additionally built a statistics library. While the order above was partially correct, the build order was more complicated as options/Makefile.am executed building the sources for expr/Makefile.am as part of its BUILT_SOURCES phase. This options/Makefile.am also build the options/h and options.cpp files in other directories. There were cyclical library dependencies between the first four above libraries. All of these aspects combined to make options extremely brittle and hard to develop. Maintaining these between clang versus gcc, and bazel versus autotools has become increasing unpredictable.

The Solution:
To address these cyclic build problems, I am simplifying the build process. Here are the main things that have to happen:
1. util/ will be split into 3 separate directories: base, util, and smt_util. Each will have their own library and Makefile.am file.
2. Dependencies for options/ will be moved into options/. If a type appears as an option, this file will be moved into options.
3. All of the old options_handlers.h files have been refactored.
4. Some files have moved from util into expr/ to resolve cycles. Some of these moves are temporary.
5. I am removing the libstatistics library.

The constraints that the CVC4 build system will eventually satisfy are:
- The include order for both the .h and .cpp files for a directory must respect the order libraries are built. For example, a file in options/ cannot include from the expr/ directory. This includes built source files such as those coming from */kinds files and */options files.
- The types definitions must also respect the build order. Forward type declarations will be allowed in exceptional, justified cases.
- The Makefile.am for a directory cannot generate a file outside of the directory it controls. (Or call another Makefile.am except through subdirectory calls.)
- One library per Makefile.am.
- No extra copies of libraries will be built for the purpose of distinguishing between external and internal visibility in libraries for building parser/ or main/ libraries and binaries. Any function used by parser/ and main/ will be labeled with CVC4_PUBLIC and be in a public API. (AFAICT, libstatistics was being built exactly to skirt this.)

The build order of CVC4 can now be [roughly] specified as
  base < options < util < expr < smt_util < libcvc4 < parsers < main
The distinction between "base < options < util < expr" are currently clean. The relationship between expr and the subsequent directories/libraries are not yet clean.

More details about the directories:

base/
The new directory base/ contains the shared utilities that are absolutely crucial to starting cvc4. The list currently includes just: cvc4_assert.{h,cpp}, output.{h,cpp}, exception.{h,cpp}, and tls.{h, h.in, cpp}. These are things that are required everywhere.

options/
The options/ directory is self contained.
- It contains all of the enums that appear as options. This includes things like theory/bv/bitblast_mode.h .
- There are exactly 4 classes that handled currently using forward declarations currently to this: LogicInfo, LemmaInputChannel, LemmaOutputChannel, and CommandSequence. These will all be removed from options.
- Functionality of the options_handlers.h files has been moved into smt/smt_options_handler.h. The options library itself only uses an interface class defined in options/options_handler_interface.h. We are now using virtual dispatch to avoid using inlined functions as was previously done.
- The */options_handlers.h files have been removed.
- The generated smt/smt_options.cpp file has been be replaced by pushing the functionality that was generated into: options/options_handler_{get,set}_option_template.cpp . The non-generated functionality was moved into smt_engine.cpp.
- All of the options files have been moved from their directories into options/. This means includes like theory/arith/options.h have changed to change to options/arith_options.h .

util/
The util/ directory continues to contain core utility classes that may be used [almost] everywhere. The exception is that these are not used by options/ or base/. This includes things like rational and integer. These may not use anything in expr/ or libcvc4. A number of files have been moved out of this directory as they have cyclic dependencies graph with exprs and types. The build process up to this directory is currently clean.

expr/
The expr/ directory continues to be the home of expressions. The major change is files moving from util/ moving into expr/. The reason for this is that these files form a cycle with files in expr/.
- An example is datatype.h. This includes "expr/expr.h", "expr/type.h" while "expr/command.h" includes datatype.h.
- Another example is predicate.h. This uses expr.h and is also declared in a kinds file and thus appears in kinds.h.
- The rule of thumb is if expr/ pulls it in it needs to be independent of expr/, in which case it is in util/, or it is not, in which case it is pulled into expr/.
- Some files do not have a strong justification currently. Result, ResourceManager and SExpr can be moved back into util/ once the iostream manipulation routines are refactored out of the Node and Expr classes.
- Note the kinds files are expected to remain in the theory/ directories. These are only read in order to build sources.
- This directory is not yet clean. It contains forward references into libcvc4 such as the printer. It also makes some classes used by main/ and parser CVC4_PUBLIC.

smt_util/
The smt_util/ directory contains those utility classes which require exprs, but expr/ does not require them. These are mostly utilities for working with expressions and nodes. Examples include ite_removal.h, LemmaInputChannel and LemmaOutputChannel.

What is up next:
- A number of new #warning "TODO: ..." items have been scattered throughout the code as reminders to myself. Help with these issues is welcomed.
- The expr/ directory needs to be cleaned up in a similar to options/. Before this happens statistics needs to be cleaned up.

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 */