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, 15 insertions, 2 deletions

diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h
index aec4257f2..f538a60a1 100644
--- a/src/prop/cnf_stream.h
+++ b/src/prop/cnf_stream.h
@@ -34,6 +34,8 @@
 
 namespace CVC4 {
 
+class OutputManager;
+
 namespace prop {
 
 class PropEngine;
@@ -56,6 +58,9 @@ class CnfStream {
   /** The SAT solver we will be using */
   SatSolver* d_satSolver;
 
+  /** Reference to the output manager of the smt engine */
+  OutputManager* d_outMgr;
+
   /** Boolean variables that we translated */
   context::CDList<TNode> d_booleanVariables;
 
@@ -166,12 +171,17 @@ class CnfStream {
    * @param satSolver the sat solver to use.
    * @param registrar the entity that takes care of preregistration of Nodes.
    * @param context the context that the CNF should respect.
+   * @param outMgr Reference to the output manager of the smt engine. Assertions
+   * will not be dumped if outMgr == nullptr.
    * @param fullLitToNodeMap maintain a full SAT-literal-to-Node mapping.
    * @param name string identifier to distinguish between different instances
    * even for non-theory literals.
    */
-  CnfStream(SatSolver* satSolver, Registrar* registrar,
-            context::Context* context, bool fullLitToNodeMap = false,
+  CnfStream(SatSolver* satSolver,
+            Registrar* registrar,
+            context::Context* context,
+            OutputManager* outMgr = nullptr,
+            bool fullLitToNodeMap = false,
             std::string name = "");
 
   /**
@@ -256,6 +266,8 @@ class TseitinCnfStream : public CnfStream {
    * @param satSolver the sat solver to use
    * @param registrar the entity that takes care of pre-registration of Nodes
    * @param context the context that the CNF should respect.
+   * @param outMgr reference to the output manager of the smt engine. Assertions
+   * will not be dumped if outMgr == nullptr.
    * @param rm the resource manager of the CNF stream
    * @param fullLitToNodeMap maintain a full SAT-literal-to-Node mapping,
    * even for non-theory literals
@@ -263,6 +275,7 @@ class TseitinCnfStream : public CnfStream {
   TseitinCnfStream(SatSolver* satSolver,
                    Registrar* registrar,
                    context::Context* context,
+                   OutputManager* outMgr,
                    ResourceManager* rm,
                    bool fullLitToNodeMap = false,
                    std::string name = "");