Dump commands in internal code using command printing functions. (#5040)

This is work towards migrating commands to the new API. Internal code that creates command objects just for dumping is replaced with direct calls to functions that print the those commands.

1 files changed, 26 insertions, 74 deletions

diff --git a/src/smt/dump.cpp b/src/smt/dump.cpp
index d8d486e12..28cf8a34f 100644
--- a/src/smt/dump.cpp
+++ b/src/smt/dump.cpp
@@ -19,9 +19,29 @@
 #include "base/output.h"
 #include "lib/strtok_r.h"
 #include "preprocessing/preprocessing_pass_registry.h"
+#include "smt/command.h"
+#include "smt/node_command.h"
 
 namespace CVC4 {
 
+CVC4dumpstream& CVC4dumpstream::operator<<(const Command& c)
+{
+  if (d_os != nullptr)
+  {
+    (*d_os) << c;
+  }
+  return *this;
+}
+
+CVC4dumpstream& CVC4dumpstream::operator<<(const NodeCommand& nc)
+{
+  if (d_os != nullptr)
+  {
+    (*d_os) << nc;
+  }
+  return *this;
+}
+
 DumpC DumpChannel CVC4_PUBLIC;
 
 std::ostream& DumpC::setStream(std::ostream* os) {
@@ -100,42 +120,6 @@ void DumpC::setDumpFromString(const std::string& optarg) {
                || !strcmp(optargPtr, "bv-rewrites")
                || !strcmp(optargPtr, "theory::fullcheck"))
       {
-        // These are "non-state-dumping" modes.  If state (SAT decisions,
-        // propagations, etc.) is dumped, it will interfere with the validity
-        // of these generated queries.
-        if (Dump.isOn("state"))
-        {
-          throw OptionException(std::string("dump option `") + optargPtr +
-                              "' conflicts with a previous, "
-                              "state-dumping dump option.  You cannot "
-                              "mix stateful and non-stateful dumping modes; "
-                              "see --dump help.");
-        }
-        else
-        {
-          Dump.on("no-permit-state");
-        }
-      }
-      else if (!strcmp(optargPtr, "state")
-               || !strcmp(optargPtr, "missed-t-conflicts")
-               || !strcmp(optargPtr, "t-propagations")
-               || !strcmp(optargPtr, "missed-t-propagations"))
-      {
-        // These are "state-dumping" modes.  If state (SAT decisions,
-        // propagations, etc.) is not dumped, it will interfere with the
-        // validity of these generated queries.
-        if (Dump.isOn("no-permit-state"))
-        {
-          throw OptionException(std::string("dump option `") + optargPtr +
-                              "' conflicts with a previous, "
-                              "non-state-dumping dump option.  You cannot "
-                              "mix stateful and non-stateful dumping modes; "
-                              "see --dump help.");
-        }
-        else
-        {
-          Dump.on("state");
-        }
       }
       else if (!strcmp(optargPtr, "help"))
       {
@@ -152,14 +136,6 @@ void DumpC::setDumpFromString(const std::string& optarg) {
         puts(ss.str().c_str());
         exit(1);
       }
-      else if (!strcmp(optargPtr, "bv-abstraction"))
-      {
-        Dump.on("bv-abstraction");
-      }
-      else if (!strcmp(optargPtr, "bv-algebraic"))
-      {
-        Dump.on("bv-algebraic");
-      }
       else
       {
         throw OptionException(std::string("unknown option for --dump: `")
@@ -222,49 +198,25 @@ clauses\n\
 + Do all the preprocessing outlined above, and dump the CNF-converted\n\
   output\n\
 \n\
-state\n\
-+ Dump all contextual assertions (e.g., SAT decisions, propagations..).\n\
-  Implied by all \"stateful\" modes below and conflicts with all\n\
-  non-stateful modes below.\n\
-\n\
-t-conflicts [non-stateful]\n\
+t-conflicts\n\
 + Output correctness queries for all theory conflicts\n\
 \n\
-missed-t-conflicts [stateful]\n\
-+ Output completeness queries for theory conflicts\n\
-\n\
-t-propagations [stateful]\n\
-+ Output correctness queries for all theory propagations\n\
-\n\
-missed-t-propagations [stateful]\n\
-+ Output completeness queries for theory propagations (LARGE and EXPENSIVE)\n\
-\n\
-t-lemmas [non-stateful]\n\
+t-lemmas\n\
 + Output correctness queries for all theory lemmas\n\
 \n\
-t-explanations [non-stateful]\n\
+t-explanations\n\
 + Output correctness queries for all theory explanations\n\
 \n\
-bv-rewrites [non-stateful]\n\
+bv-rewrites\n\
 + Output correctness queries for all bitvector rewrites\n\
 \n\
-bv-abstraction [non-stateful]\n\
-+ Output correctness queries for all bv abstraction \n\
-\n\
-bv-algebraic [non-stateful]\n\
-+ Output correctness queries for bv algebraic solver. \n\
-\n\
-theory::fullcheck [non-stateful]\n\
+theory::fullcheck\n\
 + Output completeness queries for all full-check effort-level theory checks\n\
 \n\
 Dump modes can be combined with multiple uses of --dump.  Generally you want\n\
 raw-benchmark or, alternatively, one from the assertions category (either\n\
-assertions or clauses), and perhaps one or more stateful or non-stateful modes\n\
+assertions or clauses), and perhaps one or more other modes\n\
 for checking correctness and completeness of decision procedure implementations.\n\
-Stateful modes dump the contextual assertions made by the core solver (all\n\
-decisions and propagations as assertions); this affects the validity of the\n\
-resulting correctness and completeness queries, so of course stateful and\n\
-non-stateful modes cannot be mixed in the same run.\n\
 \n\
 The --output-language option controls the language used for dumping, and\n\
 this allows you to connect CVC4 to another solver implementation via a UNIX\n\