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

1 files changed, 17 insertions, 18 deletions

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)");