Some work on the dump infrastructure to support portfolio work.

  Dump("foo") << FooCommand(...);

now "dumps" the textual representation of the command (in the current
output language) to a file, IF dumping is on at configure-time, AND the
"muzzle" feature is off, AND the "foo" flag is turned on for the dump
stream during this run.

If it's a portfolio build, the above will also store the command in a
CommandSequence, IF the "foo" flag is turned on for the dump stream
during this run.  This is done even if the muzzle is on.

This commit also cleans up some code that used the dump feature (in arrays,
particularly).

22 files changed, 399 insertions, 88 deletions

diff --git a/configure.ac b/configure.ac
index ee6975034..68d7bf026 100644
--- a/configure.ac
+++ b/configure.ac
@@ -891,6 +891,9 @@ if test x$with_portfolio != xyes; then
   with_portfolio=no
 fi
 AM_CONDITIONAL([CVC4_BUILD_PCVC4], [test "$with_portfolio" = yes])
+if test "$with_portfolio" = yes; then
+  CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_PORTFOLIO"
+fi
 
 # Whether to build compatibility library
 CVC4_BUILD_LIBCOMPAT=yes
diff --git a/src/expr/command.cpp b/src/expr/command.cpp
index 3dac28e11..48b6940dd 100644
--- a/src/expr/command.cpp
+++ b/src/expr/command.cpp
@@ -27,6 +27,7 @@
 #include "smt/smt_engine.h"
 #include "smt/bad_option_exception.h"
 #include "util/output.h"
+#include "util/dump.h"
 #include "util/sexpr.h"
 #include "expr/node.h"
 #include "printer/printer.h"
@@ -134,6 +135,10 @@ Command* EmptyCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollecti
   return new EmptyCommand(d_name);
 }
 
+Command* EmptyCommand::clone() const {
+  return new EmptyCommand(d_name);
+}
+
 /* class AssertCommand */
 
 AssertCommand::AssertCommand(const BoolExpr& e) throw() :
@@ -157,6 +162,10 @@ Command* AssertCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollect
   return new AssertCommand(d_expr.exportTo(exprManager, variableMap));
 }
 
+Command* AssertCommand::clone() const {
+  return new AssertCommand(d_expr);
+}
+
 /* class PushCommand */
 
 void PushCommand::invoke(SmtEngine* smtEngine) throw() {
@@ -169,7 +178,11 @@ void PushCommand::invoke(SmtEngine* smtEngine) throw() {
 }
 
 Command* PushCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
-  return new PushCommand;
+  return new PushCommand();
+}
+
+Command* PushCommand::clone() const {
+  return new PushCommand();
 }
 
 /* class PopCommand */
@@ -193,6 +206,10 @@ Command* PopCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection
   return new PopCommand();
 }
 
+Command* PopCommand::clone() const {
+  return new PopCommand();
+}
+
 /* class CheckSatCommand */
 
 CheckSatCommand::CheckSatCommand(const BoolExpr& expr) throw() :
@@ -230,6 +247,12 @@ Command* CheckSatCommand::exportTo(ExprManager* exprManager, ExprManagerMapColle
   return c;
 }
 
+Command* CheckSatCommand::clone() const {
+  CheckSatCommand* c = new CheckSatCommand(d_expr);
+  c->d_result = d_result;
+  return c;
+}
+
 /* class QueryCommand */
 
 QueryCommand::QueryCommand(const BoolExpr& e) throw() :
@@ -267,6 +290,12 @@ Command* QueryCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollecti
   return c;
 }
 
+Command* QueryCommand::clone() const {
+  QueryCommand* c = new QueryCommand(d_expr);
+  c->d_result = d_result;
+  return c;
+}
+
 /* class QuitCommand */
 
 QuitCommand::QuitCommand() throw() {
@@ -281,6 +310,10 @@ Command* QuitCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollectio
   return new QuitCommand();
 }
 
+Command* QuitCommand::clone() const {
+  return new QuitCommand();
+}
+
 /* class CommentCommand */
 
 CommentCommand::CommentCommand(std::string comment) throw() : d_comment(comment) {
@@ -299,6 +332,10 @@ Command* CommentCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollec
   return new CommentCommand(d_comment);
 }
 
+Command* CommentCommand::clone() const {
+  return new CommentCommand(d_comment);
+}
+
 /* class CommandSequence */
 
 CommandSequence::CommandSequence() throw() :
@@ -315,6 +352,10 @@ 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);
@@ -350,6 +391,15 @@ Command* CommandSequence::exportTo(ExprManager* exprManager, ExprManagerMapColle
   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::end() const throw() {
   return d_commandSequence.end();
 }
@@ -386,7 +436,7 @@ Type DeclareFunctionCommand::getType() const throw() {
 }
 
 void DeclareFunctionCommand::invoke(SmtEngine* smtEngine) throw() {
-  Dump("declarations") << *this << endl;
+  Dump("declarations") << *this;
 }
 
 Command* DeclareFunctionCommand::exportTo(ExprManager* exprManager,
@@ -395,6 +445,10 @@ Command* DeclareFunctionCommand::exportTo(ExprManager* exprManager,
                                     d_type.exportTo(exprManager, variableMap));
 }
 
+Command* DeclareFunctionCommand::clone() const {
+  return new DeclareFunctionCommand(d_symbol, d_type);
+}
+
 /* class DeclareTypeCommand */
 
 DeclareTypeCommand::DeclareTypeCommand(const std::string& id, size_t arity, Type t) throw() :
@@ -412,7 +466,7 @@ Type DeclareTypeCommand::getType() const throw() {
 }
 
 void DeclareTypeCommand::invoke(SmtEngine* smtEngine) throw() {
-  Dump("declarations") << *this << endl;
+  Dump("declarations") << *this;
 }
 
 Command* DeclareTypeCommand::exportTo(ExprManager* exprManager,
@@ -421,6 +475,10 @@ Command* DeclareTypeCommand::exportTo(ExprManager* exprManager,
                                 d_type.exportTo(exprManager, variableMap));
 }
 
+Command* DeclareTypeCommand::clone() const {
+  return new DeclareTypeCommand(d_symbol, d_arity, d_type);
+}
+
 /* class DefineTypeCommand */
 
 DefineTypeCommand::DefineTypeCommand(const std::string& id,
@@ -447,7 +505,7 @@ Type DefineTypeCommand::getType() const throw() {
 }
 
 void DefineTypeCommand::invoke(SmtEngine* smtEngine) throw() {
-  Dump("declarations") << *this << endl;
+  Dump("declarations") << *this;
   d_commandStatus = CommandSuccess::instance();
 }
 
@@ -459,6 +517,10 @@ Command* DefineTypeCommand::exportTo(ExprManager* exprManager, ExprManagerMapCol
   return new DefineTypeCommand(d_symbol, params, type);
 }
 
+Command* DefineTypeCommand::clone() const {
+  return new DefineTypeCommand(d_symbol, d_params, d_type);
+}
+
 /* class DefineFunctionCommand */
 
 DefineFunctionCommand::DefineFunctionCommand(const std::string& id,
@@ -493,7 +555,7 @@ Expr DefineFunctionCommand::getFormula() const throw() {
 }
 
 void DefineFunctionCommand::invoke(SmtEngine* smtEngine) throw() {
-  //Dump("declarations") << *this << endl; -- done by SmtEngine
+  //Dump("declarations") << *this; -- done by SmtEngine
   try {
     if(!d_func.isNull()) {
       smtEngine->defineFunction(d_func, d_formals, d_formula);
@@ -513,6 +575,10 @@ Command* DefineFunctionCommand::exportTo(ExprManager* exprManager, ExprManagerMa
   return new DefineFunctionCommand(d_symbol, func, formals, formula);
 }
 
+Command* DefineFunctionCommand::clone() const {
+  return new DefineFunctionCommand(d_symbol, d_func, d_formals, d_formula);
+}
+
 /* class DefineNamedFunctionCommand */
 
 DefineNamedFunctionCommand::DefineNamedFunctionCommand(const std::string& id,
@@ -539,6 +605,10 @@ Command* DefineNamedFunctionCommand::exportTo(ExprManager* exprManager, ExprMana
   return new DefineNamedFunctionCommand(d_symbol, func, formals, formula);
 }
 
+Command* DefineNamedFunctionCommand::clone() const {
+  return new DefineNamedFunctionCommand(d_symbol, d_func, d_formals, d_formula);
+}
+
 /* class Simplify */
 
 SimplifyCommand::SimplifyCommand(Expr term) throw() :
@@ -572,6 +642,12 @@ Command* SimplifyCommand::exportTo(ExprManager* exprManager, ExprManagerMapColle
   return c;
 }
 
+Command* SimplifyCommand::clone() const {
+  SimplifyCommand* c = new SimplifyCommand(d_term);
+  c->d_result = d_result;
+  return c;
+}
+
 /* class GetValueCommand */
 
 GetValueCommand::GetValueCommand(Expr term) throw() :
@@ -610,6 +686,12 @@ Command* GetValueCommand::exportTo(ExprManager* exprManager, ExprManagerMapColle
   return c;
 }
 
+Command* GetValueCommand::clone() const {
+  GetValueCommand* c = new GetValueCommand(d_term);
+  c->d_result = d_result;
+  return c;
+}
+
 /* class GetAssignmentCommand */
 
 GetAssignmentCommand::GetAssignmentCommand() throw() {
@@ -637,7 +719,13 @@ void GetAssignmentCommand::printResult(std::ostream& out) const throw() {
 }
 
 Command* GetAssignmentCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
-  GetAssignmentCommand* c = new GetAssignmentCommand;
+  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;
 }
@@ -669,7 +757,13 @@ void GetProofCommand::printResult(std::ostream& out) const throw() {
 }
 
 Command* GetProofCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
-  GetProofCommand* c = new GetProofCommand;
+  GetProofCommand* c = new GetProofCommand();
+  c->d_result = d_result;
+  return c;
+}
+
+Command* GetProofCommand::clone() const {
+  GetProofCommand* c = new GetProofCommand();
   c->d_result = d_result;
   return c;
 }
@@ -704,7 +798,13 @@ void GetAssertionsCommand::printResult(std::ostream& out) const throw() {
 }
 
 Command* GetAssertionsCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
-  GetAssertionsCommand* c = new GetAssertionsCommand;
+  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;
 }
@@ -732,8 +832,11 @@ void SetBenchmarkStatusCommand::invoke(SmtEngine* smtEngine) throw() {
 }
 
 Command* SetBenchmarkStatusCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
-  SetBenchmarkStatusCommand* c = new SetBenchmarkStatusCommand(d_status);
-  return c;
+  return new SetBenchmarkStatusCommand(d_status);
+}
+
+Command* SetBenchmarkStatusCommand::clone() const {
+  return new SetBenchmarkStatusCommand(d_status);
 }
 
 /* class SetBenchmarkLogicCommand */
@@ -756,8 +859,11 @@ void SetBenchmarkLogicCommand::invoke(SmtEngine* smtEngine) throw() {
 }
 
 Command* SetBenchmarkLogicCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
-  SetBenchmarkLogicCommand* c = new SetBenchmarkLogicCommand(d_logic);
-  return c;
+  return new SetBenchmarkLogicCommand(d_logic);
+}
+
+Command* SetBenchmarkLogicCommand::clone() const {
+  return new SetBenchmarkLogicCommand(d_logic);
 }
 
 /* class SetInfoCommand */
@@ -787,8 +893,11 @@ void SetInfoCommand::invoke(SmtEngine* smtEngine) throw() {
 }
 
 Command* SetInfoCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
-  SetInfoCommand* c = new SetInfoCommand(d_flag, d_sexpr);
-  return c;
+  return new SetInfoCommand(d_flag, d_sexpr);
+}
+
+Command* SetInfoCommand::clone() const {
+  return new SetInfoCommand(d_flag, d_sexpr);
 }
 
 /* class GetInfoCommand */
@@ -832,6 +941,12 @@ Command* GetInfoCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollec
   return c;
 }
 
+Command* GetInfoCommand::clone() const {
+  GetInfoCommand* c = new GetInfoCommand(d_flag);
+  c->d_result = d_result;
+  return c;
+}
+
 /* class SetOptionCommand */
 
 SetOptionCommand::SetOptionCommand(std::string flag, const SExpr& sexpr) throw() :
@@ -859,8 +974,11 @@ void SetOptionCommand::invoke(SmtEngine* smtEngine) throw() {
 }
 
 Command* SetOptionCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
-  SetOptionCommand* c = new SetOptionCommand(d_flag, d_sexpr);
-  return c;
+  return new SetOptionCommand(d_flag, d_sexpr);
+}
+
+Command* SetOptionCommand::clone() const {
+  return new SetOptionCommand(d_flag, d_sexpr);
 }
 
 /* class GetOptionCommand */
@@ -902,6 +1020,12 @@ Command* GetOptionCommand::exportTo(ExprManager* exprManager, ExprManagerMapColl
   return c;
 }
 
+Command* GetOptionCommand::clone() const {
+  GetOptionCommand* c = new GetOptionCommand(d_flag);
+  c->d_result = d_result;
+  return c;
+}
+
 /* class DatatypeDeclarationCommand */
 
 DatatypeDeclarationCommand::DatatypeDeclarationCommand(const DatatypeType& datatype) throw() :
@@ -919,15 +1043,19 @@ DatatypeDeclarationCommand::getDatatypes() const throw() {
 }
 
 void DatatypeDeclarationCommand::invoke(SmtEngine* smtEngine) throw() {
-  Dump("declarations") << *this << endl;
+  Dump("declarations") << *this;
   d_commandStatus = CommandSuccess::instance();
 }
 
 Command* DatatypeDeclarationCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
-  std::cout << "We currently do not support exportTo with Datatypes" << std::endl;
-  exit(1);
+  Warning() << "We currently do not support exportTo with Datatypes" << std::endl;
   return NULL;
 }
+
+Command* DatatypeDeclarationCommand::clone() const {
+  return new DatatypeDeclarationCommand(d_datatypes);
+}
+
 /* output stream insertion operator for benchmark statuses */
 std::ostream& operator<<(std::ostream& out,
                          BenchmarkStatus status) throw() {
diff --git a/src/expr/command.h b/src/expr/command.h
index fa1da4cb1..6bb6fba3d 100644
--- a/src/expr/command.h
+++ b/src/expr/command.h
@@ -225,6 +225,11 @@ public:
    */
   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;
@@ -256,6 +261,7 @@ public:
   std::string getName() const throw();
   void invoke(SmtEngine* smtEngine) throw();
   Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
+  Command* clone() const;
 };/* class EmptyCommand */
 
 class CVC4_PUBLIC AssertCommand : public Command {
@@ -267,6 +273,7 @@ public:
   BoolExpr getExpr() const throw();
   void invoke(SmtEngine* smtEngine) throw();
   Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
+  Command* clone() const;
 };/* class AssertCommand */
 
 class CVC4_PUBLIC PushCommand : public Command {
@@ -274,6 +281,7 @@ public:
   ~PushCommand() throw() {}
   void invoke(SmtEngine* smtEngine) throw();
   Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
+  Command* clone() const;
 };/* class PushCommand */
 
 class CVC4_PUBLIC PopCommand : public Command {
@@ -281,6 +289,7 @@ public:
   ~PopCommand() throw() {}
   void invoke(SmtEngine* smtEngine) throw();
   Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
+  Command* clone() const;
 };/* class PopCommand */
 
 class CVC4_PUBLIC DeclarationDefinitionCommand : public Command {
@@ -301,6 +310,7 @@ public:
   Type getType() const throw();
   void invoke(SmtEngine* smtEngine) throw();
   Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
+  Command* clone() const;
 };/* class DeclareFunctionCommand */
 
 class CVC4_PUBLIC DeclareTypeCommand : public DeclarationDefinitionCommand {
@@ -314,6 +324,7 @@ public:
   Type getType() const throw();
   void invoke(SmtEngine* smtEngine) throw();
   Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
+  Command* clone() const;
 };/* class DeclareTypeCommand */
 
 class CVC4_PUBLIC DefineTypeCommand : public DeclarationDefinitionCommand {
@@ -328,6 +339,7 @@ public:
   Type getType() const throw();
   void invoke(SmtEngine* smtEngine) throw();
   Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
+  Command* clone() const;
 };/* class DefineTypeCommand */
 
 class CVC4_PUBLIC DefineFunctionCommand : public DeclarationDefinitionCommand {
@@ -345,6 +357,7 @@ public:
   Expr getFormula() const throw();
   void invoke(SmtEngine* smtEngine) throw();
   Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
+  Command* clone() const;
 };/* class DefineFunctionCommand */
 
 /**
@@ -358,6 +371,7 @@ public:
                              const std::vector<Expr>& formals, Expr formula) throw();
   void invoke(SmtEngine* smtEngine) throw();
   Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
+  Command* clone() const;
 };/* class DefineNamedFunctionCommand */
 
 class CVC4_PUBLIC CheckSatCommand : public Command {
@@ -373,6 +387,7 @@ public:
   Result getResult() const throw();
   void printResult(std::ostream& out) const throw();
   Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
+  Command* clone() const;
 };/* class CheckSatCommand */
 
 class CVC4_PUBLIC QueryCommand : public Command {
@@ -387,6 +402,7 @@ public:
   Result getResult() const throw();
   void printResult(std::ostream& out) const throw();
   Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
+  Command* clone() const;
 };/* class QueryCommand */
 
 // this is TRANSFORM in the CVC presentation language
@@ -402,6 +418,7 @@ public:
   Expr getResult() const throw();
   void printResult(std::ostream& out) const throw();
   Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
+  Command* clone() const;
 };/* class SimplifyCommand */
 
 class CVC4_PUBLIC GetValueCommand : public Command {
@@ -416,6 +433,7 @@ public:
   Expr getResult() const throw();
   void printResult(std::ostream& out) const throw();
   Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
+  Command* clone() const;
 };/* class GetValueCommand */
 
 class CVC4_PUBLIC GetAssignmentCommand : public Command {
@@ -428,6 +446,7 @@ public:
   SExpr getResult() const throw();
   void printResult(std::ostream& out) const throw();
   Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
+  Command* clone() const;
 };/* class GetAssignmentCommand */
 
 class CVC4_PUBLIC GetProofCommand : public Command {
@@ -440,6 +459,7 @@ public:
   Proof* getResult() const throw();
   void printResult(std::ostream& out) const throw();
   Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
+  Command* clone() const;
 };/* class GetProofCommand */
 
 class CVC4_PUBLIC GetAssertionsCommand : public Command {
@@ -452,6 +472,7 @@ public:
   std::string getResult() const throw();
   void printResult(std::ostream& out) const throw();
   Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
+  Command* clone() const;
 };/* class GetAssertionsCommand */
 
 class CVC4_PUBLIC SetBenchmarkStatusCommand : public Command {
@@ -463,6 +484,7 @@ public:
   BenchmarkStatus getStatus() const throw();
   void invoke(SmtEngine* smtEngine) throw();
   Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
+  Command* clone() const;
 };/* class SetBenchmarkStatusCommand */
 
 class CVC4_PUBLIC SetBenchmarkLogicCommand : public Command {
@@ -474,6 +496,7 @@ public:
   std::string getLogic() const throw();
   void invoke(SmtEngine* smtEngine) throw();
   Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
+  Command* clone() const;
 };/* class SetBenchmarkLogicCommand */
 
 class CVC4_PUBLIC SetInfoCommand : public Command {
@@ -487,6 +510,7 @@ public:
   SExpr getSExpr() const throw();
   void invoke(SmtEngine* smtEngine) throw();
   Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
+  Command* clone() const;
 };/* class SetInfoCommand */
 
 class CVC4_PUBLIC GetInfoCommand : public Command {
@@ -501,6 +525,7 @@ public:
   std::string getResult() const throw();
   void printResult(std::ostream& out) const throw();
   Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
+  Command* clone() const;
 };/* class GetInfoCommand */
 
 class CVC4_PUBLIC SetOptionCommand : public Command {
@@ -514,6 +539,7 @@ public:
   SExpr getSExpr() const throw();
   void invoke(SmtEngine* smtEngine) throw();
   Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
+  Command* clone() const;
 };/* class SetOptionCommand */
 
 class CVC4_PUBLIC GetOptionCommand : public Command {
@@ -528,6 +554,7 @@ public:
   std::string getResult() const throw();
   void printResult(std::ostream& out) const throw();
   Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
+  Command* clone() const;
 };/* class GetOptionCommand */
 
 class CVC4_PUBLIC DatatypeDeclarationCommand : public Command {
@@ -540,6 +567,7 @@ public:
   const std::vector<DatatypeType>& getDatatypes() const throw();
   void invoke(SmtEngine* smtEngine) throw();
   Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
+  Command* clone() const;
 };/* class DatatypeDeclarationCommand */
 
 class CVC4_PUBLIC QuitCommand : public Command {
@@ -548,6 +576,7 @@ public:
   ~QuitCommand() throw() {}
   void invoke(SmtEngine* smtEngine) throw();
   Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
+  Command* clone() const;
 };/* class QuitCommand */
 
 class CVC4_PUBLIC CommentCommand : public Command {
@@ -558,6 +587,7 @@ public:
   std::string getComment() const throw();
   void invoke(SmtEngine* smtEngine) throw();
   Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
+  Command* clone() const;
 };/* class CommentCommand */
 
 class CVC4_PUBLIC CommandSequence : public Command {
@@ -571,6 +601,7 @@ public:
   ~CommandSequence() throw();
 
   void addCommand(Command* cmd) throw();
+  void clear() throw();
 
   void invoke(SmtEngine* smtEngine) throw();
   void invoke(SmtEngine* smtEngine, std::ostream& out) throw();
@@ -585,6 +616,7 @@ public:
   iterator end() throw();
 
   Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
+  Command* clone() const;
 };/* class CommandSequence */
 
 class CVC4_PUBLIC DeclarationSequence : public CommandSequence {
diff --git a/src/main/driver.cpp b/src/main/driver.cpp
index eb70f5c93..ef6b99715 100644
--- a/src/main/driver.cpp
+++ b/src/main/driver.cpp
@@ -38,6 +38,7 @@
 #include "util/configuration.h"
 #include "util/options.h"
 #include "util/output.h"
+#include "util/dump.h"
 #include "util/result.h"
 #include "util/stats.h"
 
diff --git a/src/main/driver_portfolio.cpp b/src/main/driver_portfolio.cpp
index 363901c1d..d8a8e5afa 100644
--- a/src/main/driver_portfolio.cpp
+++ b/src/main/driver_portfolio.cpp
@@ -24,6 +24,7 @@
 #include "util/configuration.h"
 #include "util/options.h"
 #include "util/output.h"
+#include "util/dump.h"
 #include "util/result.h"
 #include "util/stats.h"
 
diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp
index 396454fac..661221441 100644
--- a/src/prop/cnf_stream.cpp
+++ b/src/prop/cnf_stream.cpp
@@ -74,7 +74,7 @@ void CnfStream::assertClause(TNode node, SatClause& c) {
   Debug("cnf") << "Inserting into stream " << c << endl;
   if(Dump.isOn("clauses")) {
     if(c.size() == 1) {
-      Dump("clauses") << AssertCommand(BoolExpr(getNode(c[0]).toExpr())) << endl;
+      Dump("clauses") << AssertCommand(BoolExpr(getNode(c[0]).toExpr()));
     } else {
       Assert(c.size() > 1);
       NodeBuilder<> b(kind::OR);
@@ -82,7 +82,7 @@ void CnfStream::assertClause(TNode node, SatClause& c) {
         b << getNode(c[i]);
       }
       Node n = b;
-      Dump("clauses") << AssertCommand(BoolExpr(n.toExpr())) << endl;
+      Dump("clauses") << AssertCommand(BoolExpr(n.toExpr()));
     }
   }
   d_satSolver->addClause(c, d_removable);
diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index ac3c5e101..980cb1b3f 100644
--- a/src/prop/minisat/core/Solver.cc
+++ b/src/prop/minisat/core/Solver.cc
@@ -322,7 +322,7 @@ void Solver::cancelUntil(int level) {
         for (int l = trail_lim.size() - level; l > 0; --l) {
           context->pop();
           if(Dump.isOn("state")) {
-            Dump("state") << PopCommand() << std::endl;
+            Dump("state") << PopCommand();
           }
         }
         for (int c = trail.size()-1; c >= trail_lim[level]; c--){
diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h
index 8a5472725..ca5b2c30f 100644
--- a/src/prop/minisat/core/Solver.h
+++ b/src/prop/minisat/core/Solver.h
@@ -454,7 +454,7 @@ inline bool     Solver::addClause       (Lit p, bool removable)
 inline bool     Solver::addClause       (Lit p, Lit q, bool removable)          { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); return addClause_(add_tmp, removable); }
 inline bool     Solver::addClause       (Lit p, Lit q, Lit r, bool removable)   { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); add_tmp.push(r); return addClause_(add_tmp, removable); }
 inline bool     Solver::locked          (const Clause& c) const { return value(c[0]) == l_True && isPropagatedBy(var(c[0]), c); }
-inline void     Solver::newDecisionLevel()                      { trail_lim.push(trail.size()); context->push(); if(Dump.isOn("state")) { Dump("state") << CVC4::PushCommand() << std::endl; } }
+inline void     Solver::newDecisionLevel()                      { trail_lim.push(trail.size()); context->push(); if(Dump.isOn("state")) { Dump("state") << CVC4::PushCommand(); } }
 
 inline int      Solver::decisionLevel ()      const   { return trail_lim.size(); }
 inline uint32_t Solver::abstractLevel (Var x) const   { return 1 << (level(x) & 31); }
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index 2538e6d0c..b7b3c685f 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -97,9 +97,9 @@ void PropEngine::assertLemma(TNode node, bool negated, bool removable) {
   Debug("prop::lemmas") << "assertLemma(" << node << ")" << endl;
 
   if(!d_inCheckSat && Dump.isOn("learned")) {
-    Dump("learned") << AssertCommand(BoolExpr(node.toExpr())) << endl;
+    Dump("learned") << AssertCommand(BoolExpr(node.toExpr()));
   } else if(Dump.isOn("lemmas")) {
-    Dump("lemmas") << AssertCommand(BoolExpr(node.toExpr())) << endl;
+    Dump("lemmas") << AssertCommand(BoolExpr(node.toExpr()));
   }
 
   //TODO This comment is now false
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 8b5a93fa9..fee77df39 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -295,7 +295,7 @@ SmtEngine::SmtEngine(ExprManager* em) throw(AssertionException) :
 
 void SmtEngine::shutdown() {
   if(Dump.isOn("benchmark")) {
-    Dump("benchmark") << QuitCommand() << endl;
+    Dump("benchmark") << QuitCommand();
   }
 
   // check to see if a postsolve() is pending
@@ -351,7 +351,7 @@ void SmtEngine::setLogic(const std::string& s) throw(ModalException) {
   }
 
   if(Dump.isOn("benchmark")) {
-    Dump("benchmark") << SetBenchmarkLogicCommand(s) << endl;
+    Dump("benchmark") << SetBenchmarkLogicCommand(s);
   }
 
   setLogicInternal(s);
@@ -377,7 +377,7 @@ void SmtEngine::setInfo(const std::string& key, const SExpr& value)
   throw(BadOptionException, ModalException) {
   Trace("smt") << "SMT setInfo(" << key << ", " << value << ")" << endl;
   if(Dump.isOn("benchmark")) {
-    Dump("benchmark") << SetInfoCommand(key, value) << endl;
+    Dump("benchmark") << SetInfoCommand(key, value);
   }
 
   // Check for CVC4-specific info keys (prefixed with "cvc4-" or "cvc4_")
@@ -462,7 +462,7 @@ void SmtEngine::setOption(const std::string& key, const SExpr& value)
   throw(BadOptionException, ModalException) {
   Trace("smt") << "SMT setOption(" << key << ", " << value << ")" << endl;
   if(Dump.isOn("benchmark")) {
-    Dump("benchmark") << SetOptionCommand(key, value) << endl;
+    Dump("benchmark") << SetOptionCommand(key, value);
   }
 
   if(key == ":print-success") {
@@ -508,7 +508,7 @@ SExpr SmtEngine::getOption(const std::string& key) const
   throw(BadOptionException) {
   Trace("smt") << "SMT getOption(" << key << ")" << endl;
   if(Dump.isOn("benchmark")) {
-    Dump("benchmark") << GetOptionCommand(key) << endl;
+    Dump("benchmark") << GetOptionCommand(key);
   }
   if(key == ":print-success") {
     return SExpr("true");
@@ -543,10 +543,9 @@ void SmtEngine::defineFunction(Expr func,
   Trace("smt") << "SMT defineFunction(" << func << ")" << endl;
   if(Dump.isOn("declarations")) {
     stringstream ss;
-    ss << Expr::setlanguage(Expr::setlanguage::getLanguage(Dump("declarations")))
+    ss << Expr::setlanguage(Expr::setlanguage::getLanguage(Dump.getStream()))
        << func;
-    Dump("declarations") << DefineFunctionCommand(ss.str(), func, formals, formula)
-                         << endl;
+    Dump("declarations") << DefineFunctionCommand(ss.str(), func, formals, formula);
   }
   NodeManagerScope nms(d_nodeManager);
 
@@ -995,7 +994,7 @@ void SmtEnginePrivate::processAssertions() {
     // Push the simplified assertions to the dump output stream
     for (unsigned i = 0; i < d_assertionsToCheck.size(); ++ i) {
       Dump("assertions")
-        << AssertCommand(BoolExpr(d_assertionsToCheck[i].toExpr())) << endl;
+        << AssertCommand(BoolExpr(d_assertionsToCheck[i].toExpr()));
     }
   }
 
@@ -1077,7 +1076,7 @@ Result SmtEngine::checkSat(const BoolExpr& e) {
   // Dump the query if requested
   if(Dump.isOn("benchmark")) {
     // the expr already got dumped out if assertion-dumping is on
-    Dump("benchmark") << CheckSatCommand() << endl;
+    Dump("benchmark") << CheckSatCommand();
   }
 
   // Pop the context
@@ -1134,7 +1133,7 @@ Result SmtEngine::query(const BoolExpr& e) {
   // Dump the query if requested
   if(Dump.isOn("benchmark")) {
     // the expr already got dumped out if assertion-dumping is on
-    Dump("benchmark") << CheckSatCommand() << endl;
+    Dump("benchmark") << CheckSatCommand();
   }
 
   // Pop the context
@@ -1170,7 +1169,7 @@ Expr SmtEngine::simplify(const Expr& e) {
   }
   Trace("smt") << "SMT simplify(" << e << ")" << endl;
   if(Dump.isOn("benchmark")) {
-    Dump("benchmark") << SimplifyCommand(e) << endl;
+    Dump("benchmark") << SimplifyCommand(e);
   }
   return d_private->applySubstitutions(e).toExpr();
 }
@@ -1185,7 +1184,7 @@ Expr SmtEngine::getValue(const Expr& e)
 
   Trace("smt") << "SMT getValue(" << e << ")" << endl;
   if(Dump.isOn("benchmark")) {
-    Dump("benchmark") << GetValueCommand(e) << endl;
+    Dump("benchmark") << GetValueCommand(e);
   }
   if(!Options::current()->produceModels) {
     const char* msg =
@@ -1251,7 +1250,7 @@ SExpr SmtEngine::getAssignment() throw(ModalException, AssertionException) {
   Trace("smt") << "SMT getAssignment()" << endl;
   NodeManagerScope nms(d_nodeManager);
   if(Dump.isOn("benchmark")) {
-    Dump("benchmark") << GetAssignmentCommand() << endl;
+    Dump("benchmark") << GetAssignmentCommand();
   }
   if(!Options::current()->produceAssignments) {
     const char* msg =
@@ -1307,7 +1306,7 @@ Proof* SmtEngine::getProof() throw(ModalException, AssertionException) {
   Trace("smt") << "SMT getProof()" << endl;
   NodeManagerScope nms(d_nodeManager);
   if(Dump.isOn("benchmark")) {
-    Dump("benchmark") << GetProofCommand() << endl;
+    Dump("benchmark") << GetProofCommand();
   }
 #ifdef CVC4_PROOF
   if(!Options::current()->proof) {
@@ -1332,7 +1331,7 @@ Proof* SmtEngine::getProof() throw(ModalException, AssertionException) {
 vector<Expr> SmtEngine::getAssertions()
   throw(ModalException, AssertionException) {
   if(Dump.isOn("benchmark")) {
-    Dump("benchmark") << GetAssertionsCommand() << endl;
+    Dump("benchmark") << GetAssertionsCommand();
   }
   NodeManagerScope nms(d_nodeManager);
   Trace("smt") << "SMT getAssertions()" << endl;
@@ -1356,7 +1355,7 @@ void SmtEngine::push() {
   Trace("smt") << "SMT push()" << endl;
   d_private->processAssertions();
   if(Dump.isOn("benchmark")) {
-    Dump("benchmark") << PushCommand() << endl;
+    Dump("benchmark") << PushCommand();
   }
   if(!Options::current()->incrementalSolving) {
     throw ModalException("Cannot push when not solving incrementally (use --incremental)");
@@ -1378,7 +1377,7 @@ void SmtEngine::pop() {
   NodeManagerScope nms(d_nodeManager);
   Trace("smt") << "SMT pop()" << endl;
   if(Dump.isOn("benchmark")) {
-    Dump("benchmark") << PopCommand() << endl;
+    Dump("benchmark") << PopCommand();
   }
   if(!Options::current()->incrementalSolving) {
     throw ModalException("Cannot pop when not solving incrementally (use --incremental)");
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index fd88c751a..03a9d7a4c 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -1144,15 +1144,7 @@ inline void TheoryArrays::addExtLemma(TNode a, TNode b) {
    NodeManager* nm = NodeManager::currentNM();
    TypeNode ixType = a.getType()[0];
    Node k = nm->mkVar(ixType);
-   if(Dump.isOn("declarations")) {
-     stringstream kss;
-     kss << Expr::setlanguage(Expr::setlanguage::getLanguage(Dump("declarations"))) << k;
-     string ks = kss.str();
-     Dump("declarations")
-       << CommentCommand(ks + " is an extensional lemma index variable "
-                         "from the theory of arrays") << endl
-       << DeclareFunctionCommand(ks, ixType.toType()) << endl;
-   }
+   Dump.declareVar(k.toExpr(), "an extensional lemma index variable from the theory of arrays");
    Node eq = nm->mkNode(kind::EQUAL, a, b);
    Node ak = nm->mkNode(kind::SELECT, a, k);
    Node bk = nm->mkNode(kind::SELECT, b, k);
diff --git a/src/theory/theory.h b/src/theory/theory.h
index 1451568ab..c84d10ca1 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -31,6 +31,7 @@
 #include "context/cdlist.h"
 #include "context/cdo.h"
 #include "util/options.h"
+#include "util/dump.h"
 
 #include <string>
 #include <iostream>
@@ -199,7 +200,7 @@ protected:
     d_factsHead = d_factsHead + 1;
     Trace("theory") << "Theory::get() => " << fact << " (" << d_facts.size() - d_factsHead << " left)" << std::endl;
     if(Dump.isOn("state")) {
-      Dump("state") << AssertCommand(fact.assertion.toExpr()) << std::endl;
+      Dump("state") << AssertCommand(fact.assertion.toExpr());
     }
         
     return fact;
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 2950ad413..ebfc797a1 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -160,8 +160,8 @@ void TheoryEngine::check(Theory::Effort effort) {
 
       if(Dump.isOn("missed-t-conflicts")) {
         Dump("missed-t-conflicts")
-            << CommentCommand("Completeness check for T-conflicts; expect sat") << endl
-            << CheckSatCommand() << endl;
+            << CommentCommand("Completeness check for T-conflicts; expect sat")
+            << CheckSatCommand();
       }
 
       Debug("theory") << "TheoryEngine::check(" << effort << "): running propagation after the initial check" << std::endl;
@@ -311,8 +311,8 @@ void TheoryEngine::propagate(Theory::Effort effort) {
         ++i) {
       if(d_hasPropagated.find(*i) == d_hasPropagated.end()) {
         Dump("missed-t-propagations")
-          << CommentCommand("Completeness check for T-propagations; expect invalid") << endl
-          << QueryCommand((*i).toExpr()) << endl;
+          << CommentCommand("Completeness check for T-propagations; expect invalid")
+          << QueryCommand((*i).toExpr());
       }
     }
   }
@@ -605,8 +605,8 @@ void TheoryEngine::propagate(TNode literal, theory::TheoryId theory) {
   d_propEngine->checkTime();
 
   if(Dump.isOn("t-propagations")) {
-    Dump("t-propagations") << CommentCommand("negation of theory propagation: expect valid") << std::endl
-                           << QueryCommand(literal.toExpr()) << std::endl;
+    Dump("t-propagations") << CommentCommand("negation of theory propagation: expect valid")
+                           << QueryCommand(literal.toExpr());
   }
   if(Dump.isOn("missed-t-propagations")) {
     d_hasPropagated.insert(literal);
@@ -717,8 +717,8 @@ Node TheoryEngine::getExplanation(TNode node) {
 
   Assert(!explanation.isNull());
   if(Dump.isOn("t-explanations")) {
-    Dump("t-explanations") << CommentCommand(std::string("theory explanation from ") + theoryOf(atom)->identify() + ": expect valid") << std::endl
-      << QueryCommand(explanation.impNode(node).toExpr()) << std::endl;
+    Dump("t-explanations") << CommentCommand(std::string("theory explanation from ") + theoryOf(atom)->identify() + ": expect valid")
+      << QueryCommand(explanation.impNode(node).toExpr());
   }
   Assert(properExplanation(node, explanation));
 
@@ -731,8 +731,8 @@ void TheoryEngine::conflict(TNode conflict, TheoryId theoryId) {
   d_inConflict = true;
 
   if(Dump.isOn("t-conflicts")) {
-    Dump("t-conflicts") << CommentCommand("theory conflict: expect unsat") << std::endl
-                        << CheckSatCommand(conflict.toExpr()) << std::endl;
+    Dump("t-conflicts") << CommentCommand("theory conflict: expect unsat")
+                        << CheckSatCommand(conflict.toExpr());
   }
 
   if (d_sharedTermsExist) {
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 4c9309fb6..a8aa62d35 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -390,8 +390,7 @@ class TheoryEngine {
   theory::LemmaStatus lemma(TNode node, bool negated, bool removable) {
     if(Dump.isOn("t-lemmas")) {
       Dump("t-lemmas") << CommentCommand("theory lemma: expect valid")
-                       << std::endl
-                       << QueryCommand(node.toExpr()) << std::endl;
+                       << QueryCommand(node.toExpr());
     }
 
     // Share with other portfolio threads
diff --git a/src/util/Makefile.am b/src/util/Makefile.am
index e8d33fbd4..d52f23a9c 100644
--- a/src/util/Makefile.am
+++ b/src/util/Makefile.am
@@ -57,6 +57,8 @@ libutil_la_SOURCES = \
 	ntuple.h \
 	recursion_breaker.h \
 	subrange_bound.h \
+	dump.h \
+	dump.cpp \
 	predicate.h \
 	predicate.cpp \
 	cardinality.h \
diff --git a/src/util/dump.cpp b/src/util/dump.cpp
new file mode 100644
index 000000000..2b10158d4
--- /dev/null
+++ b/src/util/dump.cpp
@@ -0,0 +1,27 @@
+/*********************                                                        */
+/*! \file dump.cpp
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009-2012  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** 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 "util/dump.h"
+
+using namespace std;
+
+namespace CVC4 {
+
+DumpC DumpChannel CVC4_PUBLIC;
+
+}/* CVC4 namespace */
diff --git a/src/util/dump.h b/src/util/dump.h
new file mode 100644
index 000000000..7318af1a5
--- /dev/null
+++ b/src/util/dump.h
@@ -0,0 +1,130 @@
+/*********************                                                        */
+/*! \file dump.h
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009-2012  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** 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_public.h"
+
+#ifndef __CVC4__DUMP_H
+#define __CVC4__DUMP_H
+
+#include "util/output.h"
+#include "expr/command.h"
+
+namespace CVC4 {
+
+class CVC4_PUBLIC CVC4dumpstream {
+
+#if defined(CVC4_DUMPING) && !defined(CVC4_MUZZLE)
+  std::ostream* d_os;
+#endif /* CVC4_DUMPING && !CVC4_MUZZLE */
+
+#ifdef CVC4_PORTFOLIO
+  CommandSequence* d_commands;
+#endif /* CVC4_PORTFOLIO */
+
+public:
+  CVC4dumpstream() throw()
+#if defined(CVC4_DUMPING) && !defined(CVC4_MUZZLE) && defined(CVC4_PORTFOLIO)
+    : d_os(NULL), d_commands(NULL)
+#elif defined(CVC4_DUMPING) && !defined(CVC4_MUZZLE)
+    : d_os(NULL)
+#elif defined(CVC4_PORTFOLIO)
+    : d_commands(NULL)
+#endif /* CVC4_PORTFOLIO */
+  { }
+
+  CVC4dumpstream(std::ostream& os, CommandSequence& commands) throw()
+#if defined(CVC4_DUMPING) && !defined(CVC4_MUZZLE) && defined(CVC4_PORTFOLIO)
+    : d_os(&os), d_commands(&commands)
+#elif defined(CVC4_DUMPING) && !defined(CVC4_MUZZLE)
+    : d_os(&os)
+#elif defined(CVC4_PORTFOLIO)
+    : d_commands(&commands)
+#endif /* CVC4_PORTFOLIO */
+  { }
+
+  CVC4dumpstream& operator<<(const Command& c) {
+#if defined(CVC4_DUMPING) && !defined(CVC4_MUZZLE)
+    if(d_os != NULL) {
+      (*d_os) << c << std::endl;
+    }
+#endif
+#if defined(CVC4_PORTFOLIO)
+    if(d_commands != NULL) {
+      d_commands->addCommand(c.clone());
+    }
+#endif
+    return *this;
+  }
+};/* class CVC4dumpstream */
+
+/** The dump class */
+class CVC4_PUBLIC DumpC {
+  std::set<std::string> d_tags;
+  CommandSequence d_commands;
+
+public:
+  CVC4dumpstream operator()(const char* tag) {
+    if(!d_tags.empty() && d_tags.find(std::string(tag)) != d_tags.end()) {
+      return CVC4dumpstream(getStream(), d_commands);
+    } else {
+      return CVC4dumpstream();
+    }
+  }
+  CVC4dumpstream operator()(std::string tag) {
+    if(!d_tags.empty() && d_tags.find(tag) != d_tags.end()) {
+      return CVC4dumpstream(getStream(), d_commands);
+    } else {
+      return CVC4dumpstream();
+    }
+  }
+
+  void clear() { d_commands.clear(); }
+  const CommandSequence& getCommands() const { return d_commands; }
+
+  void declareVar(Expr e, std::string comment) {
+    if(isOn("declarations")) {
+      std::stringstream ss;
+      ss << Expr::setlanguage(Expr::setlanguage::getLanguage(getStream())) << e;
+      std::string s = ss.str();
+      CVC4dumpstream(getStream(), d_commands)
+        << CommentCommand(s + " is " + comment)
+        << DeclareFunctionCommand(s, e.getType());
+    }
+  }
+
+  bool on (const char* tag) { d_tags.insert(std::string(tag)); return true; }
+  bool on (std::string tag) { d_tags.insert(tag); return true; }
+  bool off(const char* tag) { d_tags.erase (std::string(tag)); return false; }
+  bool off(std::string tag) { d_tags.erase (tag); return false; }
+  bool off()                { d_tags.clear(); return false; }
+
+  bool isOn(const char* tag) { return d_tags.find(std::string(tag)) != d_tags.end(); }
+  bool isOn(std::string tag) { return d_tags.find(tag) != d_tags.end(); }
+
+  std::ostream& setStream(std::ostream& os) { DumpOut.setStream(os); return os; }
+  std::ostream& getStream() { return DumpOut.getStream(); }
+};/* class DumpC */
+
+/** The dump singleton */
+extern DumpC DumpChannel CVC4_PUBLIC;
+
+#define Dump ::CVC4::DumpChannel
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__DUMP_H */
diff --git a/src/util/ite_removal.cpp b/src/util/ite_removal.cpp
index bd5048040..dfa6e3cba 100644
--- a/src/util/ite_removal.cpp
+++ b/src/util/ite_removal.cpp
@@ -55,13 +55,7 @@ Node RemoveITE::run(TNode node, std::vector<Node>& output) {
       // Make the skolem to represent the ITE
       Node skolem = nodeManager->mkVar(nodeType);
 
-      if(Dump.isOn("declarations")) {
-        stringstream kss;
-        kss << Expr::setlanguage(Expr::setlanguage::getLanguage(Dump("declarations"))) << skolem;
-        string ks = kss.str();
-        Dump("declarations") << CommentCommand(ks + " is a variable introduced due to term-level ITE removal") << endl
-                             << DeclareFunctionCommand(ks, nodeType.toType()) << endl;
-      }
+      Dump.declareVar(skolem.toExpr(), "a variable introduced due to term-level ITE removal");
 
       // The new assertion
       Node newAssertion =
diff --git a/src/util/ite_removal.h b/src/util/ite_removal.h
index 8861d612c..bfb0d4ac8 100644
--- a/src/util/ite_removal.h
+++ b/src/util/ite_removal.h
@@ -22,6 +22,7 @@
 
 #include <vector>
 #include "expr/node.h"
+#include "util/dump.h"
 
 namespace CVC4 {
 
diff --git a/src/util/options.cpp b/src/util/options.cpp
index d21df27ac..f9ab0b480 100644
--- a/src/util/options.cpp
+++ b/src/util/options.cpp
@@ -34,6 +34,7 @@
 #include "util/language.h"
 #include "util/options.h"
 #include "util/output.h"
+#include "util/dump.h"
 
 #include "cvc4autoconfig.h"
 
@@ -609,7 +610,7 @@ throw(OptionException) {
       if(optarg == NULL || *optarg == '\0') {
         throw OptionException(string("Bad file name for --dump-to"));
       } else if(!strcmp(optarg, "-")) {
-        Dump.setStream(DumpC::dump_cout);
+        Dump.setStream(DumpOutC::dump_cout);
       } else {
         ostream* dumpTo = new ofstream(optarg, ofstream::out | ofstream::trunc);
         if(!*dumpTo) {
diff --git a/src/util/output.cpp b/src/util/output.cpp
index 3823f7be6..48a7d51fd 100644
--- a/src/util/output.cpp
+++ b/src/util/output.cpp
@@ -40,8 +40,8 @@ MessageC MessageChannel CVC4_PUBLIC (&cout);
 NoticeC NoticeChannel CVC4_PUBLIC (&cout);
 ChatC ChatChannel CVC4_PUBLIC (&cout);
 TraceC TraceChannel CVC4_PUBLIC (&cout);
-std::ostream DumpC::dump_cout(cout.rdbuf());// copy cout stream buffer
-DumpC DumpChannel CVC4_PUBLIC (&DumpC::dump_cout);
+std::ostream DumpOutC::dump_cout(cout.rdbuf());// copy cout stream buffer
+DumpOutC DumpOutChannel CVC4_PUBLIC (&DumpOutC::dump_cout);
 
 #ifndef CVC4_MUZZLE
 
@@ -159,7 +159,7 @@ int TraceC::printf(std::string tag, const char* fmt, ...) {
 
 #  ifdef CVC4_DUMPING
 
-int DumpC::printf(const char* tag, const char* fmt, ...) {
+int DumpOutC::printf(const char* tag, const char* fmt, ...) {
   if(d_tags.find(string(tag)) == d_tags.end()) {
     return 0;
   }
@@ -174,7 +174,7 @@ int DumpC::printf(const char* tag, const char* fmt, ...) {
   return retval;
 }
 
-int DumpC::printf(std::string tag, const char* fmt, ...) {
+int DumpOutC::printf(std::string tag, const char* fmt, ...) {
   if(d_tags.find(tag) == d_tags.end()) {
     return 0;
   }
diff --git a/src/util/output.h b/src/util/output.h
index 8afb4e05a..308cfcac2 100644
--- a/src/util/output.h
+++ b/src/util/output.h
@@ -347,7 +347,7 @@ public:
 };/* class TraceC */
 
 /** The dump output class */
-class CVC4_PUBLIC DumpC {
+class CVC4_PUBLIC DumpOutC {
   std::set<std::string> d_tags;
   std::ostream* d_os;
 
@@ -358,7 +358,7 @@ public:
    * unlimited). */
   static std::ostream dump_cout;
 
-  explicit DumpC(std::ostream* os) : d_os(os) {}
+  explicit DumpOutC(std::ostream* os) : d_os(os) {}
 
   int printf(const char* tag, const char* fmt, ...) __attribute__ ((format(printf, 3, 4)));
   int printf(std::string tag, const char* fmt, ...) __attribute__ ((format(printf, 3, 4)));
@@ -389,7 +389,7 @@ public:
 
   std::ostream& setStream(std::ostream& os) { d_os = &os; return os; }
   std::ostream& getStream() { return *d_os; }
-};/* class DumpC */
+};/* class DumpOutC */
 
 /** The debug output singleton */
 extern DebugC DebugChannel CVC4_PUBLIC;
@@ -404,7 +404,7 @@ extern ChatC ChatChannel CVC4_PUBLIC;
 /** The trace output singleton */
 extern TraceC TraceChannel CVC4_PUBLIC;
 /** The dump output singleton */
-extern DumpC DumpChannel CVC4_PUBLIC;
+extern DumpOutC DumpOutChannel CVC4_PUBLIC;
 
 #ifdef CVC4_MUZZLE
 
@@ -415,7 +415,7 @@ extern DumpC DumpChannel CVC4_PUBLIC;
 #  define Notice ::CVC4::__cvc4_true() ? ::CVC4::nullCvc4Stream : ::CVC4::NoticeChannel
 #  define Chat ::CVC4::__cvc4_true() ? ::CVC4::nullCvc4Stream : ::CVC4::ChatChannel
 #  define Trace ::CVC4::__cvc4_true() ? ::CVC4::nullCvc4Stream : ::CVC4::TraceChannel
-#  define Dump ::CVC4::__cvc4_true() ? ::CVC4::nullCvc4Stream : ::CVC4::DumpChannel
+#  define DumpOut ::CVC4::__cvc4_true() ? ::CVC4::nullCvc4Stream : ::CVC4::DumpOutChannel
 
 inline int DebugC::printf(const char* tag, const char* fmt, ...) { return 0; }
 inline int DebugC::printf(std::string tag, const char* fmt, ...) { return 0; }
@@ -425,8 +425,8 @@ inline int NoticeC::printf(const char* fmt, ...) { return 0; }
 inline int ChatC::printf(const char* fmt, ...) { return 0; }
 inline int TraceC::printf(const char* tag, const char* fmt, ...) { return 0; }
 inline int TraceC::printf(std::string tag, const char* fmt, ...) { return 0; }
-inline int DumpC::printf(const char* tag, const char* fmt, ...) { return 0; }
-inline int DumpC::printf(std::string tag, const char* fmt, ...) { return 0; }
+inline int DumpOutC::printf(const char* tag, const char* fmt, ...) { return 0; }
+inline int DumpOutC::printf(std::string tag, const char* fmt, ...) { return 0; }
 
 #else /* CVC4_MUZZLE */
 
@@ -450,11 +450,11 @@ inline int TraceC::printf(const char* tag, const char* fmt, ...) { return 0; }
 inline int TraceC::printf(std::string tag, const char* fmt, ...) { return 0; }
 #  endif /* CVC4_TRACING */
 #  ifdef CVC4_DUMPING
-#    define Dump ::CVC4::DumpChannel
+#    define DumpOut ::CVC4::DumpOutChannel
 #  else /* CVC4_DUMPING */
-#    define Dump ::CVC4::__cvc4_true() ? ::CVC4::nullCvc4Stream : ::CVC4::DumpChannel
-inline int DumpC::printf(const char* tag, const char* fmt, ...) { return 0; }
-inline int DumpC::printf(std::string tag, const char* fmt, ...) { return 0; }
+#    define DumpOut ::CVC4::__cvc4_true() ? ::CVC4::nullCvc4Stream : ::CVC4::DumpOutChannel
+inline int DumpOutC::printf(const char* tag, const char* fmt, ...) { return 0; }
+inline int DumpOutC::printf(std::string tag, const char* fmt, ...) { return 0; }
 #  endif /* CVC4_DUMPING */
 
 #endif /* CVC4_MUZZLE */