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

8 files changed, 178 insertions, 23 deletions

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 */