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

10 files changed, 0 insertions, 3611 deletions

diff --git a/src/smt_util/Makefile.am b/src/smt_util/Makefile.am
index ae1ea1f70..46f6493a9 100644
--- a/src/smt_util/Makefile.am
+++ b/src/smt_util/Makefile.am
@@ -10,23 +10,11 @@ libsmtutil_la_SOURCES = \
 	Makefile.in \
 	boolean_simplification.cpp \
 	boolean_simplification.h \
-	command.cpp \
-	command.h \
-	dump.cpp \
-	dump.h \
-	ite_removal.cpp \
-	ite_removal.h \
 	lemma_channels.cpp \
 	lemma_channels.h \
 	lemma_input_channel.h \
 	lemma_output_channel.h \
-	model.cpp \
-	model.h \
 	nary_builder.cpp \
 	nary_builder.h \
 	node_visitor.h
 
-
-EXTRA_DIST = \
-	command.i
-
diff --git a/src/smt_util/command.cpp b/src/smt_util/command.cpp
deleted file mode 100644
index 83298836f..000000000
--- a/src/smt_util/command.cpp
+++ /dev/null
@@ -1,1855 +0,0 @@
-/*********************                                                        */
-/*! \file command.cpp
- ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): Kshitij Bansal, Dejan Jovanovic, Andrew Reynolds, Francois Bobot
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief Implementation of command objects.
- **
- ** Implementation of command objects.
- **/
-
-#include "smt_util/command.h"
-
-#include <exception>
-#include <iostream>
-#include <iterator>
-#include <sstream>
-#include <utility>
-#include <vector>
-
-#include "base/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/smt_engine.h"
-#include "smt/smt_engine_scope.h"
-#include "smt_util/dump.h"
-#include "smt_util/model.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_util/command.h b/src/smt_util/command.h
deleted file mode 100644
index 248e69b0e..000000000
--- a/src/smt_util/command.h
+++ /dev/null
@@ -1,905 +0,0 @@
-/*********************                                                        */
-/*! \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_util/command.i b/src/smt_util/command.i
deleted file mode 100644
index e4744c4f4..000000000
--- a/src/smt_util/command.i
+++ /dev/null
@@ -1,77 +0,0 @@
-%{
-#include "smt_util/command.h"
-
-#ifdef SWIGJAVA
-
-#include "bindings/java_iterator_adapter.h"
-#include "bindings/java_stream_adapters.h"
-
-#endif /* SWIGJAVA */
-%}
-
-%ignore CVC4::operator<<(std::ostream&, const Command&) throw();
-%ignore CVC4::operator<<(std::ostream&, const Command*) throw();
-%ignore CVC4::operator<<(std::ostream&, const CommandStatus&) throw();
-%ignore CVC4::operator<<(std::ostream&, const CommandStatus*) throw();
-%ignore CVC4::operator<<(std::ostream&, BenchmarkStatus status) throw();
-%ignore CVC4::operator<<(std::ostream&, CommandPrintSuccess) throw();
-
-%ignore CVC4::GetProofCommand;
-%ignore CVC4::CommandPrintSuccess::Scope;
-
-#ifdef SWIGJAVA
-
-// Instead of CommandSequence::begin() and end(), create an
-// iterator() method on the Java side that returns a Java-style
-// Iterator.
-%ignore CVC4::CommandSequence::begin();
-%ignore CVC4::CommandSequence::end();
-%ignore CVC4::CommandSequence::begin() const;
-%ignore CVC4::CommandSequence::end() const;
-%extend CVC4::CommandSequence {
-  CVC4::JavaIteratorAdapter<CVC4::CommandSequence> iterator() {
-    return CVC4::JavaIteratorAdapter<CVC4::CommandSequence>(*$self);
-  }
-}
-
-// CommandSequence is "iterable" on the Java side
-%typemap(javainterfaces) CVC4::CommandSequence "java.lang.Iterable<edu.nyu.acsys.CVC4.Command>";
-
-// the JavaIteratorAdapter should not be public, and implements Iterator
-%typemap(javaclassmodifiers) CVC4::JavaIteratorAdapter<CVC4::CommandSequence> "class";
-%typemap(javainterfaces) CVC4::JavaIteratorAdapter<CVC4::CommandSequence> "java.util.Iterator<edu.nyu.acsys.CVC4.Command>";
-// add some functions to the Java side (do it here because there's no way to do these in C++)
-%typemap(javacode) CVC4::JavaIteratorAdapter<CVC4::CommandSequence> "
-  public void remove() {
-    throw new java.lang.UnsupportedOperationException();
-  }
-
-  public edu.nyu.acsys.CVC4.Command next() {
-    if(hasNext()) {
-      return getNext();
-    } else {
-      throw new java.util.NoSuchElementException();
-    }
-  }
-"
-// getNext() just allows C++ iterator access from Java-side next(), make it private
-%javamethodmodifiers CVC4::JavaIteratorAdapter<CVC4::CommandSequence>::getNext() "private";
-
-// map the types appropriately
-%typemap(jni) CVC4::CommandSequence::const_iterator::value_type "jobject";
-%typemap(jtype) CVC4::CommandSequence::const_iterator::value_type "edu.nyu.acsys.CVC4.Command";
-%typemap(jstype) CVC4::CommandSequence::const_iterator::value_type "edu.nyu.acsys.CVC4.Command";
-%typemap(javaout) CVC4::CommandSequence::const_iterator::value_type { return $jnicall; }
-
-#endif /* SWIGJAVA */
-
-%include "smt_util/command.h"
-
-#ifdef SWIGJAVA
-
-%include "bindings/java_iterator_adapter.h"
-%include "bindings/java_stream_adapters.h"
-
-%template(JavaIteratorAdapter_CommandSequence) CVC4::JavaIteratorAdapter<CVC4::CommandSequence>;
-
-#endif /* SWIGJAVA */
diff --git a/src/smt_util/dump.cpp b/src/smt_util/dump.cpp
deleted file mode 100644
index 66cb6e3d1..000000000
--- a/src/smt_util/dump.cpp
+++ /dev/null
@@ -1,221 +0,0 @@
-/*********************                                                        */
-/*! \file dump.cpp
- ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief Dump utility classes and functions
- **
- ** Dump utility classes and functions.
- **/
-#include "smt_util/dump.h"
-
-#include "base/output.h"
-
-namespace CVC4 {
-
-DumpC DumpChannel CVC4_PUBLIC;
-
-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_util/dump.h b/src/smt_util/dump.h
deleted file mode 100644
index 19f9118e3..000000000
--- a/src/smt_util/dump.h
+++ /dev/null
@@ -1,123 +0,0 @@
-/*********************                                                        */
-/*! \file dump.h
- ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief Dump utility classes and functions
- **
- ** Dump utility classes and functions.
- **/
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__DUMP_H
-#define __CVC4__DUMP_H
-
-#include "base/output.h"
-#include "smt_util/command.h"
-
-namespace CVC4 {
-
-class CVC4_PUBLIC CVC4dumpstream {
-
-#if defined(CVC4_DUMPING) && !defined(CVC4_MUZZLE)
-  std::ostream* d_os;
-#endif /* CVC4_DUMPING && !CVC4_MUZZLE */
-
-#ifdef CVC4_PORTFOLIO
-  CommandSequence* d_commands;
-#endif /* CVC4_PORTFOLIO */
-
-public:
-  CVC4dumpstream() throw()
-#if defined(CVC4_DUMPING) && !defined(CVC4_MUZZLE) && defined(CVC4_PORTFOLIO)
-    : d_os(NULL), d_commands(NULL)
-#elif defined(CVC4_DUMPING) && !defined(CVC4_MUZZLE)
-    : d_os(NULL)
-#elif defined(CVC4_PORTFOLIO)
-    : d_commands(NULL)
-#endif /* CVC4_PORTFOLIO */
-  { }
-
-  CVC4dumpstream(std::ostream& os, CommandSequence& commands) throw()
-#if defined(CVC4_DUMPING) && !defined(CVC4_MUZZLE) && defined(CVC4_PORTFOLIO)
-    : d_os(&os), d_commands(&commands)
-#elif defined(CVC4_DUMPING) && !defined(CVC4_MUZZLE)
-    : d_os(&os)
-#elif defined(CVC4_PORTFOLIO)
-    : d_commands(&commands)
-#endif /* CVC4_PORTFOLIO */
-  { }
-
-  CVC4dumpstream& operator<<(const Command& c) {
-#if defined(CVC4_DUMPING) && !defined(CVC4_MUZZLE)
-    if(d_os != NULL) {
-      (*d_os) << c << std::endl;
-    }
-#endif
-#if defined(CVC4_PORTFOLIO)
-    if(d_commands != NULL) {
-      d_commands->addCommand(c.clone());
-    }
-#endif
-    return *this;
-  }
-};/* class CVC4dumpstream */
-
-/** The dump class */
-class CVC4_PUBLIC DumpC {
-  std::set<std::string> d_tags;
-  CommandSequence d_commands;
-
-  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_util/ite_removal.cpp b/src/smt_util/ite_removal.cpp
deleted file mode 100644
index 0d1c7b61e..000000000
--- a/src/smt_util/ite_removal.cpp
+++ /dev/null
@@ -1,192 +0,0 @@
-/*********************                                                        */
-/*! \file ite_removal.cpp
- ** \verbatim
- ** Original author: Dejan Jovanovic
- ** Major contributors: Tim King, Morgan Deters
- ** Minor contributors (to current version): Kshitij Bansal, Andrew Reynolds, Clark Barrett
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief Removal of term ITEs
- **
- ** Removal of term ITEs.
- **/
-#include "smt_util/ite_removal.h"
-
-#include <vector>
-
-#include "proof/proof_manager.h"
-#include "smt_util/command.h"
-#include "theory/ite_utilities.h"
-
-using namespace CVC4;
-using namespace std;
-
-namespace CVC4 {
-
-RemoveITE::RemoveITE(context::UserContext* u)
-  : d_iteCache(u)
-{
-  d_containsVisitor = new theory::ContainsTermITEVisitor();
-}
-
-RemoveITE::~RemoveITE(){
-  delete d_containsVisitor;
-}
-
-void RemoveITE::garbageCollect(){
-  d_containsVisitor->garbageCollect();
-}
-
-theory::ContainsTermITEVisitor* RemoveITE::getContainsVisitor() {
-  return d_containsVisitor;
-}
-
-size_t RemoveITE::collectedCacheSizes() const{
-  return d_containsVisitor->cache_size() + d_iteCache.size();
-}
-
-void RemoveITE::run(std::vector<Node>& output, IteSkolemMap& iteSkolemMap, bool reportDeps)
-{
-  size_t n = output.size();
-  for (unsigned i = 0, i_end = output.size(); i < i_end; ++ i) {
-    // Do this in two steps to avoid Node problems(?)
-    // Appears related to bug 512, splitting this into two lines
-    // fixes the bug on clang on Mac OS
-    Node itesRemoved = run(output[i], output, iteSkolemMap, false);
-    // In some calling contexts, not necessary to report dependence information.
-    if(reportDeps && options::unsatCores()) {
-      // new assertions have a dependence on the node
-      PROOF( ProofManager::currentPM()->addDependence(itesRemoved, output[i]); )
-      while(n < output.size()) {
-        PROOF( ProofManager::currentPM()->addDependence(output[n], output[i]); )
-        ++n;
-      }
-    }
-    output[i] = itesRemoved;
-  }
-}
-
-bool RemoveITE::containsTermITE(TNode e) const {
-  return d_containsVisitor->containsTermITE(e);
-}
-
-Node RemoveITE::run(TNode node, std::vector<Node>& output,
-                    IteSkolemMap& iteSkolemMap, bool inQuant) {
-  // Current node
-  Debug("ite") << "removeITEs(" << node << ")" << endl;
-
-  if(node.isVar() || node.isConst() ||
-     (options::biasedITERemoval() && !containsTermITE(node))){
-    return Node(node);
-  }
-
-  // The result may be cached already
-  std::pair<Node, bool> cacheKey(node, inQuant);
-  NodeManager *nodeManager = NodeManager::currentNM();
-  ITECache::const_iterator i = d_iteCache.find(cacheKey);
-  if(i != d_iteCache.end()) {
-    Node cached = (*i).second;
-    Debug("ite") << "removeITEs: in-cache: " << cached << endl;
-    return cached.isNull() ? Node(node) : cached;
-  }
-
-  // Remember that we're inside a quantifier
-  if(node.getKind() == kind::FORALL || node.getKind() == kind::EXISTS) {
-    inQuant = true;
-  }
-
-  // If an ITE replace it
-  if(node.getKind() == kind::ITE) {
-    TypeNode nodeType = node.getType();
-    if(!nodeType.isBoolean() && (!inQuant || !node.hasBoundVar())) {
-      Node skolem;
-      // Make the skolem to represent the ITE
-      skolem = nodeManager->mkSkolem("termITE", nodeType, "a variable introduced due to term-level ITE removal");
-
-      // The new assertion
-      Node newAssertion =
-        nodeManager->mkNode(kind::ITE, node[0], skolem.eqNode(node[1]),
-                            skolem.eqNode(node[2]));
-      Debug("ite") << "removeITEs(" << node << ") => " << newAssertion << endl;
-
-      // Attach the skolem
-      d_iteCache.insert(cacheKey, skolem);
-
-      // Remove ITEs from the new assertion, rewrite it and push it to the output
-      newAssertion = run(newAssertion, output, iteSkolemMap, inQuant);
-
-      iteSkolemMap[skolem] = output.size();
-      output.push_back(newAssertion);
-
-      // The representation is now the skolem
-      return skolem;
-    }
-  }
-
-  // If not an ITE, go deep
-  vector<Node> newChildren;
-  bool somethingChanged = false;
-  if(node.getMetaKind() == kind::metakind::PARAMETERIZED) {
-    newChildren.push_back(node.getOperator());
-  }
-  // Remove the ITEs from the children
-  for(TNode::const_iterator it = node.begin(), end = node.end(); it != end; ++it) {
-    Node newChild = run(*it, output, iteSkolemMap, inQuant);
-    somethingChanged |= (newChild != *it);
-    newChildren.push_back(newChild);
-  }
-
-  // If changes, we rewrite
-  if(somethingChanged) {
-    Node cached = nodeManager->mkNode(node.getKind(), newChildren);
-    d_iteCache.insert(cacheKey, cached);
-    return cached;
-  } else {
-    d_iteCache.insert(cacheKey, Node::null());
-    return node;
-  }
-}
-
-Node RemoveITE::replace(TNode node, bool inQuant) const {
-  if(node.isVar() || node.isConst() ||
-     (options::biasedITERemoval() && !containsTermITE(node))){
-    return Node(node);
-  }
-
-  // Check the cache
-  NodeManager *nodeManager = NodeManager::currentNM();
-  ITECache::const_iterator i = d_iteCache.find(make_pair(node, inQuant));
-  if(i != d_iteCache.end()) {
-    Node cached = (*i).second;
-    return cached.isNull() ? Node(node) : cached;
-  }
-
-  // Remember that we're inside a quantifier
-  if(node.getKind() == kind::FORALL || node.getKind() == kind::EXISTS) {
-    inQuant = true;
-  }
-
-  vector<Node> newChildren;
-  bool somethingChanged = false;
-  if(node.getMetaKind() == kind::metakind::PARAMETERIZED) {
-    newChildren.push_back(node.getOperator());
-  }
-  // Replace in children
-  for(TNode::const_iterator it = node.begin(), end = node.end(); it != end; ++it) {
-    Node newChild = replace(*it, inQuant);
-    somethingChanged |= (newChild != *it);
-    newChildren.push_back(newChild);
-  }
-
-  // If changes, we rewrite
-  if(somethingChanged) {
-    return nodeManager->mkNode(node.getKind(), newChildren);
-  } else {
-    return node;
-  }
-}
-
-}/* CVC4 namespace */
diff --git a/src/smt_util/ite_removal.h b/src/smt_util/ite_removal.h
deleted file mode 100644
index 0cc0ea5d0..000000000
--- a/src/smt_util/ite_removal.h
+++ /dev/null
@@ -1,93 +0,0 @@
-/*********************                                                        */
-/*! \file ite_removal.h
- ** \verbatim
- ** Original author: Dejan Jovanovic
- ** Major contributors: Kshitij Bansal, Tim King, Morgan Deters
- ** Minor contributors (to current version): Clark Barrett
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief Removal of term ITEs
- **
- ** Removal of term ITEs.
- **/
-
-#include "cvc4_private.h"
-
-#pragma once
-
-#include <vector>
-
-#include "context/cdinsert_hashmap.h"
-#include "context/context.h"
-#include "expr/node.h"
-#include "smt_util/dump.h"
-#include "util/bool.h"
-#include "util/hash.h"
-
-namespace CVC4 {
-
-namespace theory {
-  class ContainsTermITEVisitor;
-}/* CVC4::theory namespace */
-
-typedef std::hash_map<Node, unsigned, NodeHashFunction> IteSkolemMap;
-
-class RemoveITE {
-  typedef context::CDInsertHashMap< std::pair<Node, bool>, Node, PairHashFunction<Node, bool, NodeHashFunction, BoolHashFunction> > ITECache;
-  ITECache d_iteCache;
-
-
-public:
-
-  RemoveITE(context::UserContext* u);
-  ~RemoveITE();
-
-  /**
-   * Removes the ITE nodes by introducing skolem variables. All
-   * additional assertions are pushed into assertions. iteSkolemMap
-   * contains a map from introduced skolem variables to the index in
-   * assertions containing the new Boolean ite created in conjunction
-   * with that skolem variable.
-   *
-   * With reportDeps true, report reasoning dependences to the proof
-   * manager (for unsat cores).
-   */
-  void run(std::vector<Node>& assertions, IteSkolemMap& iteSkolemMap, bool reportDeps = false);
-
-  /**
-   * Removes the ITE from the node by introducing skolem
-   * variables. All additional assertions are pushed into
-   * assertions. iteSkolemMap contains a map from introduced skolem
-   * variables to the index in assertions containing the new Boolean
-   * ite created in conjunction with that skolem variable.
-   */
-  Node run(TNode node, std::vector<Node>& additionalAssertions,
-           IteSkolemMap& iteSkolemMap, bool inQuant);
-
-  /**
-   * Substitute under node using pre-existing cache.  Do not remove
-   * any ITEs not seen during previous runs.
-   */
-  Node replace(TNode node, bool inQuant = false) const;
-
-  /** Returns true if e contains a term ite. */
-  bool containsTermITE(TNode e) const;
-
-  /** Returns the collected size of the caches. */
-  size_t collectedCacheSizes() const;
-
-  /** Garbage collects non-context dependent data-structures. */
-  void garbageCollect();
-
-  /** Return the RemoveITE's containsVisitor. */
-  theory::ContainsTermITEVisitor* getContainsVisitor();
-
-private:
-  theory::ContainsTermITEVisitor* d_containsVisitor;
-
-};/* class RemoveTTE */
-
-}/* CVC4 namespace */
diff --git a/src/smt_util/model.cpp b/src/smt_util/model.cpp
deleted file mode 100644
index ddac7e263..000000000
--- a/src/smt_util/model.cpp
+++ /dev/null
@@ -1,55 +0,0 @@
-/*********************                                                        */
-/*! \file model.cpp
- ** \verbatim
- ** Original author: Andrew Reynolds
- ** Major contributors: Morgan Deters
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief implementation of Model class
- **/
-
-#include "smt_util/model.h"
-
-#include <vector>
-
-#include "expr/expr_iomanip.h"
-#include "options/base_options.h"
-#include "printer/printer.h"
-#include "smt/command_list.h"
-#include "smt/smt_engine_scope.h"
-#include "smt_util/command.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_util/model.h b/src/smt_util/model.h
deleted file mode 100644
index 33a9312a6..000000000
--- a/src/smt_util/model.h
+++ /dev/null
@@ -1,78 +0,0 @@
-/*********************                                                        */
-/*! \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 */