Moving dump.*, command.*, model.*, and ite_removal.* from smt_util/ to smt/. Breaking an edge between the sat solver and command.h.

12 files changed, 3601 insertions, 4 deletions

diff --git a/src/smt/command.cpp b/src/smt/command.cpp
new file mode 100644
index 000000000..d6ec0769a
--- /dev/null
+++ b/src/smt/command.cpp
@@ -0,0 +1,1855 @@
+/*********************                                                        */
+/*! \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/command.h"
+
+#include <exception>
+#include <iostream>
+#include <iterator>
+#include <sstream>
+#include <utility>
+#include <vector>
+
+#include "base/cvc4_assert.h"
+#include "base/output.h"
+#include "expr/expr_iomanip.h"
+#include "expr/node.h"
+#include "options/options.h"
+#include "options/smt_options.h"
+#include "printer/printer.h"
+#include "smt/dump.h"
+#include "smt/model.h"
+#include "smt/smt_engine.h"
+#include "smt/smt_engine_scope.h"
+#include "util/sexpr.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) {
+  PrettyCheckArgument(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::ExprDag::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_smtEngine = smtEngine;
+    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 {
+    smt::SmtScope scope(d_smtEngine);
+    d_result->toStream(out);
+  }
+}
+
+Command* GetProofCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
+  GetProofCommand* c = new GetProofCommand();
+  c->d_result = d_result;
+  c->d_smtEngine = d_smtEngine;
+  return c;
+}
+
+Command* GetProofCommand::clone() const {
+  GetProofCommand* c = new GetProofCommand();
+  c->d_result = d_result;
+  c->d_smtEngine = d_smtEngine;
+  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/command.h b/src/smt/command.h
new file mode 100644
index 000000000..248e69b0e
--- /dev/null
+++ b/src/smt/command.h
@@ -0,0 +1,905 @@
+/*********************                                                        */
+/*! \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 <iosfwd>
+#include <map>
+#include <sstream>
+#include <string>
+#include <vector>
+
+#include "expr/datatype.h"
+#include "expr/expr.h"
+#include "expr/type.h"
+#include "expr/variable_type_map.h"
+#include "proof/unsat_core.h"
+#include "util/proof.h"
+#include "util/result.h"
+#include "util/sexpr.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;
+  SmtEngine* d_smtEngine;
+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/command.i b/src/smt/command.i
new file mode 100644
index 000000000..0c050201d
--- /dev/null
+++ b/src/smt/command.i
@@ -0,0 +1,77 @@
+%{
+#include "smt/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/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/command_list.cpp b/src/smt/command_list.cpp
index 3e912d338..2319d9539 100644
--- a/src/smt/command_list.cpp
+++ b/src/smt/command_list.cpp
@@ -15,9 +15,9 @@
  **/
 
 // we include both of these to make sure they agree on the typedef
+#include "smt/command.h"
 #include "smt/command_list.h"
 #include "smt/smt_engine.h"
-#include "smt_util/command.h"
 
 namespace CVC4 {
 namespace smt {
diff --git a/src/smt/dump.cpp b/src/smt/dump.cpp
new file mode 100644
index 000000000..3b9ec3273
--- /dev/null
+++ b/src/smt/dump.cpp
@@ -0,0 +1,221 @@
+/*********************                                                        */
+/*! \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/dump.h"
+
+#include "base/output.h"
+
+namespace CVC4 {
+
+DumpC DumpChannel CVC4_PUBLIC;
+
+std::ostream& DumpC::setStream(std::ostream* os) {
+  ::CVC4::DumpOutChannel.setStream(os);
+  return *os;
+}
+std::ostream& DumpC::getStream() { return ::CVC4::DumpOutChannel.getStream(); }
+std::ostream* DumpC::getStreamPointer() { return ::CVC4::DumpOutChannel.getStreamPointer(); }
+
+
+void DumpC::setDumpFromString(const std::string& optarg) {
+#ifdef CVC4_DUMPING
+  char* optargPtr = strdup(optarg.c_str());
+  char* tokstr = optargPtr;
+  char* toksave;
+  while((optargPtr = strtok_r(tokstr, ",", &toksave)) != NULL) {
+    tokstr = NULL;
+    if(!strcmp(optargPtr, "benchmark")) {
+    } else if(!strcmp(optargPtr, "declarations")) {
+    } else if(!strcmp(optargPtr, "assertions")) {
+      Dump.on("assertions:post-everything");
+    } else if(!strncmp(optargPtr, "assertions:", 11)) {
+      const char* p = optargPtr + 11;
+      if(!strncmp(p, "pre-", 4)) {
+        p += 4;
+      } else if(!strncmp(p, "post-", 5)) {
+        p += 5;
+      } else {
+        throw OptionException(std::string("don't know how to dump `") +
+                              optargPtr + "'.  Please consult --dump help.");
+      }
+      if(!strcmp(p, "everything")) {
+      } else if(!strcmp(p, "definition-expansion")) {
+      } else if(!strcmp(p, "boolean-terms")) {
+      } else if(!strcmp(p, "constrain-subtypes")) {
+      } else if(!strcmp(p, "substitution")) {
+      } else if(!strcmp(p, "strings-pp")) {
+      } else if(!strcmp(p, "skolem-quant")) {
+      } else if(!strcmp(p, "simplify")) {
+      } else if(!strcmp(p, "static-learning")) {
+      } else if(!strcmp(p, "ite-removal")) {
+      } else if(!strcmp(p, "repeat-simplify")) {
+      } else if(!strcmp(p, "rewrite-apply-to-const")) {
+      } else if(!strcmp(p, "theory-preprocessing")) {
+      } else if(!strcmp(p, "nonclausal")) {
+      } else if(!strcmp(p, "theorypp")) {
+      } else if(!strcmp(p, "itesimp")) {
+      } else if(!strcmp(p, "unconstrained")) {
+      } else if(!strcmp(p, "repeatsimp")) {
+      } else {
+        throw OptionException(std::string("don't know how to dump `") +
+                              optargPtr + "'.  Please consult --dump help.");
+      }
+      Dump.on("assertions");
+    } else if(!strcmp(optargPtr, "skolems")) {
+    } else if(!strcmp(optargPtr, "clauses")) {
+    } else if(!strcmp(optargPtr, "t-conflicts") ||
+              !strcmp(optargPtr, "t-lemmas") ||
+              !strcmp(optargPtr, "t-explanations") ||
+              !strcmp(optargPtr, "bv-rewrites") ||
+              !strcmp(optargPtr, "theory::fullcheck")) {
+      // These are "non-state-dumping" modes.  If state (SAT decisions,
+      // propagations, etc.) is dumped, it will interfere with the validity
+      // of these generated queries.
+      if(Dump.isOn("state")) {
+        throw OptionException(std::string("dump option `") + optargPtr +
+                              "' conflicts with a previous, "
+                              "state-dumping dump option.  You cannot "
+                              "mix stateful and non-stateful dumping modes; "
+                              "see --dump help.");
+      } else {
+        Dump.on("no-permit-state");
+      }
+    } else if(!strcmp(optargPtr, "state") ||
+              !strcmp(optargPtr, "missed-t-conflicts") ||
+              !strcmp(optargPtr, "t-propagations") ||
+              !strcmp(optargPtr, "missed-t-propagations")) {
+      // These are "state-dumping" modes.  If state (SAT decisions,
+      // propagations, etc.) is not dumped, it will interfere with the
+      // validity of these generated queries.
+      if(Dump.isOn("no-permit-state")) {
+        throw OptionException(std::string("dump option `") + optargPtr +
+                              "' conflicts with a previous, "
+                              "non-state-dumping dump option.  You cannot "
+                              "mix stateful and non-stateful dumping modes; "
+                              "see --dump help.");
+      } else {
+        Dump.on("state");
+      }
+    } else if(!strcmp(optargPtr, "help")) {
+      puts(s_dumpHelp.c_str());
+      exit(1);
+    } else if(!strcmp(optargPtr, "bv-abstraction")) {
+      Dump.on("bv-abstraction");
+    } else if(!strcmp(optargPtr, "bv-algebraic")) {
+      Dump.on("bv-algebraic");
+    } else {
+      throw OptionException(std::string("unknown option for --dump: `") +
+                            optargPtr + "'.  Try --dump help.");
+    }
+
+    Dump.on(optargPtr);
+    Dump.on("benchmark");
+    if(strcmp(optargPtr, "benchmark")) {
+      Dump.on("declarations");
+      if(strcmp(optargPtr, "declarations")) {
+        Dump.on("skolems");
+      }
+    }
+  }
+  free(optargPtr);
+#else /* CVC4_DUMPING */
+  throw OptionException("The dumping feature was disabled in this build of CVC4.");
+#endif /* CVC4_DUMPING */
+}
+
+
+const std::string DumpC::s_dumpHelp = "\
+Dump modes currently supported by the --dump option:\n\
+\n\
+benchmark\n\
++ Dump the benchmark structure (set-logic, push/pop, queries, etc.), but\n\
+  does not include any declarations or assertions.  Implied by all following\n\
+  modes.\n\
+\n\
+declarations\n\
++ Dump user declarations.  Implied by all following modes.\n\
+\n\
+skolems\n\
++ Dump internally-created skolem variable declarations.  These can\n\
+  arise from preprocessing simplifications, existential elimination,\n\
+  and a number of other things.  Implied by all following modes.\n\
+\n\
+assertions\n\
++ Output the assertions after preprocessing and before clausification.\n\
+  Can also specify \"assertions:pre-PASS\" or \"assertions:post-PASS\",\n\
+  where PASS is one of the preprocessing passes: definition-expansion\n\
+  boolean-terms constrain-subtypes substitution strings-pp skolem-quant\n\
+  simplify static-learning ite-removal repeat-simplify\n\
+  rewrite-apply-to-const theory-preprocessing.\n\
+  PASS can also be the special value \"everything\", in which case the\n\
+  assertions are printed before any preprocessing (with\n\
+  \"assertions:pre-everything\") or after all preprocessing completes\n\
+  (with \"assertions:post-everything\").\n\
+\n\
+clauses\n\
++ Do all the preprocessing outlined above, and dump the CNF-converted\n\
+  output\n\
+\n\
+state\n\
++ Dump all contextual assertions (e.g., SAT decisions, propagations..).\n\
+  Implied by all \"stateful\" modes below and conflicts with all\n\
+  non-stateful modes below.\n\
+\n\
+t-conflicts [non-stateful]\n\
++ Output correctness queries for all theory conflicts\n\
+\n\
+missed-t-conflicts [stateful]\n\
++ Output completeness queries for theory conflicts\n\
+\n\
+t-propagations [stateful]\n\
++ Output correctness queries for all theory propagations\n\
+\n\
+missed-t-propagations [stateful]\n\
++ Output completeness queries for theory propagations (LARGE and EXPENSIVE)\n\
+\n\
+t-lemmas [non-stateful]\n\
++ Output correctness queries for all theory lemmas\n\
+\n\
+t-explanations [non-stateful]\n\
++ Output correctness queries for all theory explanations\n\
+\n\
+bv-rewrites [non-stateful]\n\
++ Output correctness queries for all bitvector rewrites\n\
+\n\
+bv-abstraction [non-stateful]\n\
++ Output correctness queries for all bv abstraction \n\
+\n\
+bv-algebraic [non-stateful]\n\
++ Output correctness queries for bv algebraic solver. \n\
+\n\
+theory::fullcheck [non-stateful]\n                                      \
++ Output completeness queries for all full-check effort-level theory checks\n\
+\n\
+Dump modes can be combined with multiple uses of --dump.  Generally you want\n\
+one from the assertions category (either assertions or clauses), and\n\
+perhaps one or more stateful or non-stateful modes for checking correctness\n\
+and completeness of decision procedure implementations.  Stateful modes dump\n\
+the contextual assertions made by the core solver (all decisions and\n\
+propagations as assertions; that affects the validity of the resulting\n\
+correctness and completeness queries, so of course stateful and non-stateful\n\
+modes cannot be mixed in the same run.\n\
+\n\
+The --output-language option controls the language used for dumping, and\n\
+this allows you to connect CVC4 to another solver implementation via a UNIX\n\
+pipe to perform on-line checking.  The --dump-to option can be used to dump\n\
+to a file.\n\
+";
+
+}/* CVC4 namespace */
diff --git a/src/smt/dump.h b/src/smt/dump.h
new file mode 100644
index 000000000..a6fa899da
--- /dev/null
+++ b/src/smt/dump.h
@@ -0,0 +1,123 @@
+/*********************                                                        */
+/*! \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/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;
+
+  static const std::string s_dumpHelp;
+
+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);
+  std::ostream& getStream();
+  std::ostream* getStreamPointer();
+
+  void setDumpFromString(const std::string& optarg);
+};/* 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/ite_removal.cpp b/src/smt/ite_removal.cpp
new file mode 100644
index 000000000..c0c6ed02b
--- /dev/null
+++ b/src/smt/ite_removal.cpp
@@ -0,0 +1,190 @@
+/*********************                                                        */
+/*! \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/ite_removal.h"
+
+#include <vector>
+
+#include "proof/proof_manager.h"
+#include "theory/ite_utilities.h"
+
+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/ite_removal.h b/src/smt/ite_removal.h
new file mode 100644
index 000000000..d6d820f89
--- /dev/null
+++ b/src/smt/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/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/model.cpp b/src/smt/model.cpp
new file mode 100644
index 000000000..15ecbadfb
--- /dev/null
+++ b/src/smt/model.cpp
@@ -0,0 +1,55 @@
+/*********************                                                        */
+/*! \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/model.h"
+
+#include <vector>
+
+#include "expr/expr_iomanip.h"
+#include "options/base_options.h"
+#include "printer/printer.h"
+#include "smt/command.h"
+#include "smt/command_list.h"
+#include "smt/smt_engine_scope.h"
+
+using namespace std;
+
+namespace CVC4 {
+
+std::ostream& operator<<(std::ostream& out, const Model& m) {
+  smt::SmtScope smts(&m.d_smt);
+  expr::ExprDag::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/model.h b/src/smt/model.h
new file mode 100644
index 000000000..33a9312a6
--- /dev/null
+++ b/src/smt/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 <iosfwd>
+#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/smt_engine.cpp b/src/smt/smt_engine.cpp
index df3466d92..850b37fe0 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -72,15 +72,15 @@
 #include "proof/unsat_core.h"
 #include "prop/prop_engine.h"
 #include "smt/boolean_terms.h"
+#include "smt/command.h"
 #include "smt/command_list.h"
+#include "smt/ite_removal.h"
 #include "smt/logic_request.h"
 #include "smt/managed_ostreams.h"
 #include "smt/model_postprocessor.h"
 #include "smt/smt_engine_scope.h"
 #include "smt/update_ostream.h"
 #include "smt_util/boolean_simplification.h"
-#include "smt_util/command.h"
-#include "smt_util/ite_removal.h"
 #include "smt_util/nary_builder.h"
 #include "smt_util/node_visitor.h"
 #include "theory/arith/pseudoboolean_proc.h"
diff --git a/src/smt/update_ostream.h b/src/smt/update_ostream.h
index c5f09a2a9..b87ed69d2 100644
--- a/src/smt/update_ostream.h
+++ b/src/smt/update_ostream.h
@@ -28,7 +28,7 @@
 #include "options/language.h"
 #include "options/set_language.h"
 #include "options/base_options.h"
-#include "smt_util/dump.h"
+#include "smt/dump.h"
 
 namespace CVC4 {