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).

diff --git a/configure.ac b/configure.ac
index ee6975034b83b5cb667d70c14d9b8370179169d5..68d7bf026ed704eae0866c40e2172d05569c7a28 100644 (file)
--- 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 3dac28e11e71823b9b7ae403a52b46547f603934..48b6940dd9d751792c50c828c8d69c2aa835ae01 100644 (file)
--- 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 fa1da4cb187243e911cb86a47b202fdfb8942cd3..6bb6fba3dc174d5e018649fc79cd3e92fcc3e68c 100644 (file)
--- 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 eb70f5c93ea949a950489054298893803cdde37d..ef6b997154b35c48866d2df9a3141238824bf670 100644 (file)
--- 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 363901c1de679b20534c48b4528c7d09b6d7b014..d8a8e5afa042abbad22085fa77f579efc7541b75 100644 (file)
--- 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 396454fac0d7e7c84ae0ec759843e3c67113ce5e..661221441db6f839faf2b314ee4a9a0301ecd5ef 100644 (file)
--- 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 ac3c5e1011f33c224d16004c435ef435e7bef725..980cb1b3fa6d0ead766dd77832441f1fac021a1a 100644 (file)
--- 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 8a54727256b541d26bd0318d29e5e4eac228ecba..ca5b2c30ffdecd18911bc5572c9d64c2ae5b92fb 100644 (file)
--- 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 2538e6d0c7f4272aa8ea9a45c14a06c0a2d13d6d..b7b3c685f459b546fae814fdc3ab57856e63b989 100644 (file)
--- 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 8b5a93fa91871c8b594a6c43284580963827817b..fee77df39283ad235932000db2511c7f43f711f7 100644 (file)
--- 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 fd88c751a23ad27d2442888b61898dc2d2aa92ca..03a9d7a4c64b9c929f3abc933a6ad0fca5b17f06 100644 (file)
--- 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 1451568abddbb96fdee08a9cf0b08fec87db76a6..c84d10ca18bb6674c2bb3407ee93b383ff5072de 100644 (file)
--- 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 2950ad413fe3cf7d442860a01bda27be2ad47b2e..ebfc797a11e45bc1e4de7903b645bdb0c15d97ea 100644 (file)
--- 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 4c9309fb63710e492a65e85700d22e3de7d75489..a8aa62d35c5e19ab46fe0b2663cd163f592d39a4 100644 (file)
--- 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 e8d33fbd457976f9b428d568514b6871f163a603..d52f23a9c3360c7394274bdb722d9e2d4d4ff380 100644 (file)
--- 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 (file)
index 0000000..2b10158
--- /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 (file)
index 0000000..7318af1
--- /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 bd504804011fc9bbfef97f388046097ebfa4e163..dfa6e3cba7f70f198bbde24baa1596afa72c3c96 100644 (file)
--- 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 8861d612c8fd0ed61acd41887518ab62d961163e..bfb0d4ac81767920a1fcbe709acac43576360bda 100644 (file)
--- 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 d21df27ac979b9a0d4794547ac1ab8e35f2dd404..f9ab0b48026e173cdb5aba4275008755910acab7 100644 (file)
--- 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 3823f7be695bb7814ab2679bfa5a45b98a55b5af..48a7d51fd7804f32f4a037250b74c775fc56f2fa 100644 (file)
--- 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 8afb4e05a74f83eaa60886e1783839bc7f719ccd..308cfcac21ea7d7f7282b8df68546907f84b7ce6 100644 (file)
--- 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 */