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.

5 files changed, 27 insertions, 66 deletions

diff --git a/src/theory/bv/abstraction.cpp b/src/theory/bv/abstraction.cpp
index a9ec7aa53..d7899f010 100644
--- a/src/theory/bv/abstraction.cpp
+++ b/src/theory/bv/abstraction.cpp
@@ -15,12 +15,14 @@
 #include "theory/bv/abstraction.h"
 
 #include "options/bv_options.h"
+#include "printer/printer.h"
 #include "smt/dump.h"
+#include "smt/smt_engine.h"
+#include "smt/smt_engine_scope.h"
 #include "smt/smt_statistics_registry.h"
 #include "theory/bv/theory_bv_utils.h"
 #include "theory/rewriter.h"
 
-
 using namespace CVC4;
 using namespace CVC4::theory;
 using namespace CVC4::theory::bv;
@@ -691,15 +693,6 @@ Node AbstractionModule::substituteArguments(TNode signature, TNode apply, unsign
 }
 
 Node AbstractionModule::simplifyConflict(TNode conflict) {
-  if (Dump.isOn("bv-abstraction")) {
-    NodeNodeMap seen;
-    Node c = reverseAbstraction(conflict, seen);
-    Dump("bv-abstraction") << PushCommand();
-    Dump("bv-abstraction") << AssertCommand(c.toExpr());
-    Dump("bv-abstraction") << CheckSatCommand();
-    Dump("bv-abstraction") << PopCommand();
-  }
-
   Debug("bv-abstraction-dbg") << "AbstractionModule::simplifyConflict " << conflict << "\n";
   if (conflict.getKind() != kind::AND)
     return conflict;
@@ -742,16 +735,6 @@ Node AbstractionModule::simplifyConflict(TNode conflict) {
   Debug("bv-abstraction") << "AbstractionModule::simplifyConflict conflict " << conflict <<"\n";
   Debug("bv-abstraction") << "   => " << new_conflict <<"\n";
 
-  if (Dump.isOn("bv-abstraction")) {
-
-    NodeNodeMap seen;
-    Node nc = reverseAbstraction(new_conflict, seen);
-    Dump("bv-abstraction") << PushCommand();
-    Dump("bv-abstraction") << AssertCommand(nc.toExpr());
-    Dump("bv-abstraction") << CheckSatCommand();
-    Dump("bv-abstraction") << PopCommand();
-  }
-
   return new_conflict;
 }
 
@@ -836,15 +819,6 @@ void AbstractionModule::generalizeConflict(TNode conflict, std::vector<Node>& le
       lemmas.push_back(lemma);
       Debug("bv-abstraction-gen") << "adding lemma " << lemma << "\n";
       storeLemma(lemma);
-
-      if (Dump.isOn("bv-abstraction")) {
-        NodeNodeMap seen;
-        Node l = reverseAbstraction(lemma, seen);
-        Dump("bv-abstraction") << PushCommand();
-        Dump("bv-abstraction") << AssertCommand(l.toExpr());
-        Dump("bv-abstraction") << CheckSatCommand();
-        Dump("bv-abstraction") << PopCommand();
-      }
     }
   }
 }
diff --git a/src/theory/bv/bitblast/eager_bitblaster.cpp b/src/theory/bv/bitblast/eager_bitblaster.cpp
index 6417740fd..48aa0fbd6 100644
--- a/src/theory/bv/bitblast/eager_bitblaster.cpp
+++ b/src/theory/bv/bitblast/eager_bitblaster.cpp
@@ -20,6 +20,7 @@
 #include "options/bv_options.h"
 #include "prop/cnf_stream.h"
 #include "prop/sat_solver_factory.h"
+#include "smt/smt_engine.h"
 #include "smt/smt_statistics_registry.h"
 #include "theory/bv/bv_solver_lazy.h"
 #include "theory/bv/theory_bv.h"
@@ -71,6 +72,7 @@ EagerBitblaster::EagerBitblaster(BVSolverLazy* theory_bv, context::Context* c)
   d_cnfStream.reset(new prop::TseitinCnfStream(d_satSolver.get(),
                                                d_bitblastingRegistrar.get(),
                                                d_nullContext.get(),
+                                               nullptr,
                                                rm,
                                                false,
                                                "EagerBitblaster"));
diff --git a/src/theory/bv/bitblast/lazy_bitblaster.cpp b/src/theory/bv/bitblast/lazy_bitblaster.cpp
index 1813784d7..93c91719b 100644
--- a/src/theory/bv/bitblast/lazy_bitblaster.cpp
+++ b/src/theory/bv/bitblast/lazy_bitblaster.cpp
@@ -21,6 +21,7 @@
 #include "prop/cnf_stream.h"
 #include "prop/sat_solver.h"
 #include "prop/sat_solver_factory.h"
+#include "smt/smt_engine.h"
 #include "smt/smt_statistics_registry.h"
 #include "theory/bv/abstraction.h"
 #include "theory/bv/bv_solver_lazy.h"
@@ -82,6 +83,7 @@ TLazyBitblaster::TLazyBitblaster(context::Context* c,
   d_cnfStream.reset(new prop::TseitinCnfStream(d_satSolver.get(),
                                                d_nullRegistrar.get(),
                                                d_nullContext.get(),
+                                               nullptr,
                                                rm,
                                                false,
                                                "LazyBitblaster"));
@@ -573,8 +575,11 @@ void TLazyBitblaster::clearSolver() {
   d_satSolver.reset(
       prop::SatSolverFactory::createMinisat(d_ctx, smtStatisticsRegistry()));
   ResourceManager* rm = smt::currentResourceManager();
-  d_cnfStream.reset(new prop::TseitinCnfStream(
-      d_satSolver.get(), d_nullRegistrar.get(), d_nullContext.get(), rm));
+  d_cnfStream.reset(new prop::TseitinCnfStream(d_satSolver.get(),
+                                               d_nullRegistrar.get(),
+                                               d_nullContext.get(),
+                                               nullptr,
+                                               rm));
   d_satSolverNotify.reset(
       d_emptyNotify
           ? (prop::BVSatSolverNotify*)new MinisatEmptyNotify()
diff --git a/src/theory/bv/bv_subtheory_algebraic.cpp b/src/theory/bv/bv_subtheory_algebraic.cpp
index e900566f9..52f68c6ef 100644
--- a/src/theory/bv/bv_subtheory_algebraic.cpp
+++ b/src/theory/bv/bv_subtheory_algebraic.cpp
@@ -19,6 +19,10 @@
 
 #include "expr/node_algorithm.h"
 #include "options/bv_options.h"
+#include "printer/printer.h"
+#include "smt/dump.h"
+#include "smt/smt_engine.h"
+#include "smt/smt_engine_scope.h"
 #include "smt/smt_statistics_registry.h"
 #include "smt_util/boolean_simplification.h"
 #include "theory/bv/bv_quick_check.h"
@@ -321,16 +325,6 @@ bool AlgebraicSolver::check(Theory::Effort e)
     TNode fact = worklist[r].node;
     unsigned id = worklist[r].id;
 
-    if (Dump.isOn("bv-algebraic")) {
-      Node expl = d_explanations[id];
-      Node query = utils::mkNot(nm->mkNode(kind::IMPLIES, expl, fact));
-      Dump("bv-algebraic") << EchoCommand("ThoeryBV::AlgebraicSolver::substitution explanation");
-      Dump("bv-algebraic") << PushCommand();
-      Dump("bv-algebraic") << AssertCommand(query.toExpr());
-      Dump("bv-algebraic") << CheckSatCommand();
-      Dump("bv-algebraic") << PopCommand();
-    }
-
     if (fact.isConst() &&
         fact.getConst<bool>() == true) {
       continue;
@@ -344,16 +338,6 @@ bool AlgebraicSolver::check(Theory::Effort e)
       d_isComplete.set(true);
       Debug("bv-subtheory-algebraic") << " UNSAT: assertion simplfies to false with conflict: "<< conflict << "\n";
 
-      if (Dump.isOn("bv-algebraic")) {
-        Dump("bv-algebraic")
-            << EchoCommand("BVSolverLazy::AlgebraicSolver::conflict");
-        Dump("bv-algebraic") << PushCommand();
-        Dump("bv-algebraic") << AssertCommand(conflict.toExpr());
-        Dump("bv-algebraic") << CheckSatCommand();
-        Dump("bv-algebraic") << PopCommand();
-      }
-
-
       ++(d_statistics.d_numSimplifiesToFalse);
       ++(d_numSolved);
       return false;
@@ -536,17 +520,6 @@ bool AlgebraicSolver::solve(TNode fact, TNode reason, SubstitutionEx& subst) {
     Node new_right = nm->mkNode(kind::BITVECTOR_XOR, right, inverse);
     bool changed = subst.addSubstitution(var, new_right, reason);
 
-    if (Dump.isOn("bv-algebraic")) {
-      Node query = utils::mkNot(nm->mkNode(
-          kind::EQUAL, fact, nm->mkNode(kind::EQUAL, var, new_right)));
-      Dump("bv-algebraic") << EchoCommand("ThoeryBV::AlgebraicSolver::substitution explanation");
-      Dump("bv-algebraic") << PushCommand();
-      Dump("bv-algebraic") << AssertCommand(query.toExpr());
-      Dump("bv-algebraic") << CheckSatCommand();
-      Dump("bv-algebraic") << PopCommand();
-    }
-
-
     return changed;
   }
 
diff --git a/src/theory/bv/theory_bv_rewrite_rules.h b/src/theory/bv/theory_bv_rewrite_rules.h
index 0dbb51753..549843421 100644
--- a/src/theory/bv/theory_bv_rewrite_rules.h
+++ b/src/theory/bv/theory_bv_rewrite_rules.h
@@ -22,7 +22,10 @@
 #include <sstream>
 
 #include "context/context.h"
-#include "smt/command.h"
+#include "printer/printer.h"
+#include "smt/dump.h"
+#include "smt/smt_engine.h"
+#include "smt/smt_engine_scope.h"
 #include "theory/bv/theory_bv_utils.h"
 #include "theory/theory.h"
 #include "util/statistics_registry.h"
@@ -449,9 +452,13 @@ public:
 
           Node condition = node.eqNode(result).notNode();
 
-          Dump("bv-rewrites")
-            << CommentCommand(os.str())
-            << CheckSatCommand(condition.toExpr());
+          const Printer& printer =
+              smt::currentSmtEngine()->getOutputManager().getPrinter();
+          std::ostream& out =
+              smt::currentSmtEngine()->getOutputManager().getDumpOut();
+
+          printer.toStreamCmdComment(out, os.str());
+          printer.toStreamCmdCheckSat(out, condition);
         }
       }
       Debug("theory::bv::rewrite") << "RewriteRule<" << rule << ">(" << node << ") => " << result << std::endl;