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.

17 files changed, 322 insertions, 198 deletions

diff --git a/src/smt/command.cpp b/src/smt/command.cpp
index 64ef60906..38c799fca 100644
--- a/src/smt/command.cpp
+++ b/src/smt/command.cpp
@@ -106,20 +106,6 @@ std::ostream& operator<<(std::ostream& out, BenchmarkStatus status)
 }
 
 // !!! Temporary until commands are migrated to the new API !!!
-std::vector<Node> exprVectorToNodes(const std::vector<Expr>& exprs)
-{
-  std::vector<Node> nodes;
-  nodes.reserve(exprs.size());
-
-  for (Expr e : exprs)
-  {
-    nodes.push_back(Node::fromExpr(e));
-  }
-
-  return nodes;
-}
-
-// !!! Temporary until commands are migrated to the new API !!!
 std::vector<TypeNode> typeVectorToTypeNodes(const std::vector<Type>& types)
 {
   std::vector<TypeNode> typeNodes;
@@ -2977,7 +2963,7 @@ void SetBenchmarkStatusCommand::toStream(std::ostream& out,
                                          size_t dag,
                                          OutputLanguage language) const
 {
-  Result::Sat status;
+  Result::Sat status = Result::SAT_UNKNOWN;
   switch (d_status)
   {
     case BenchmarkStatus::SMT_SATISFIABLE: status = Result::SAT; break;
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\
diff --git a/src/smt/dump.h b/src/smt/dump.h
index 4c0efeb6e..ec13a9ae9 100644
--- a/src/smt/dump.h
+++ b/src/smt/dump.h
@@ -20,11 +20,12 @@
 #define CVC4__DUMP_H
 
 #include "base/output.h"
-#include "smt/command.h"
-#include "smt/node_command.h"
 
 namespace CVC4 {
 
+class Command;
+class NodeCommand;
+
 #if defined(CVC4_DUMPING) && !defined(CVC4_MUZZLE)
 
 class CVC4_PUBLIC CVC4dumpstream
@@ -33,27 +34,14 @@ class CVC4_PUBLIC CVC4dumpstream
   CVC4dumpstream() : d_os(nullptr) {}
   CVC4dumpstream(std::ostream& os) : d_os(&os) {}
 
-  CVC4dumpstream& operator<<(const Command& c) {
-    if (d_os != nullptr)
-    {
-      (*d_os) << c << std::endl;
-    }
-    return *this;
-  }
+  CVC4dumpstream& operator<<(const Command& c);
 
   /** A convenience function for dumping internal commands.
    *
    * Since Commands are now part of the public API, internal code should use
    * NodeCommands and this function (instead of the one above) to dump them.
    */
-  CVC4dumpstream& operator<<(const NodeCommand& nc)
-  {
-    if (d_os != nullptr)
-    {
-      (*d_os) << nc << std::endl;
-    }
-    return *this;
-  }
+  CVC4dumpstream& operator<<(const NodeCommand& nc);
 
  private:
   std::ostream* d_os;
diff --git a/src/smt/dump_manager.cpp b/src/smt/dump_manager.cpp
index 033be405f..849339106 100644
--- a/src/smt/dump_manager.cpp
+++ b/src/smt/dump_manager.cpp
@@ -17,6 +17,7 @@
 #include "expr/expr_manager.h"
 #include "options/smt_options.h"
 #include "smt/dump.h"
+#include "smt/node_command.h"
 
 namespace CVC4 {
 namespace smt {
@@ -98,11 +99,11 @@ void DumpManager::setPrintFuncInModel(Node f, bool p)
   Trace("setp-model") << "Set printInModel " << f << " to " << p << std::endl;
   for (std::unique_ptr<NodeCommand>& c : d_modelGlobalCommands)
   {
-    DeclareFunctionCommand* dfc =
-        dynamic_cast<DeclareFunctionCommand*>(c.get());
+    DeclareFunctionNodeCommand* dfc =
+        dynamic_cast<DeclareFunctionNodeCommand*>(c.get());
     if (dfc != NULL)
     {
-      Node df = Node::fromExpr(dfc->getFunction());
+      Node df = dfc->getFunction();
       if (df == f)
       {
         dfc->setPrintInModel(p);
@@ -111,10 +112,11 @@ void DumpManager::setPrintFuncInModel(Node f, bool p)
   }
   for (NodeCommand* c : d_modelCommands)
   {
-    DeclareFunctionCommand* dfc = dynamic_cast<DeclareFunctionCommand*>(c);
+    DeclareFunctionNodeCommand* dfc =
+        dynamic_cast<DeclareFunctionNodeCommand*>(c);
     if (dfc != NULL)
     {
-      Node df = Node::fromExpr(dfc->getFunction());
+      Node df = dfc->getFunction();
       if (df == f)
       {
         dfc->setPrintInModel(p);
diff --git a/src/smt/dump_manager.h b/src/smt/dump_manager.h
index 2ce0570e4..5954817bd 100644
--- a/src/smt/dump_manager.h
+++ b/src/smt/dump_manager.h
@@ -22,9 +22,11 @@
 
 #include "context/cdlist.h"
 #include "expr/node.h"
-#include "smt/node_command.h"
 
 namespace CVC4 {
+
+class NodeCommand;
+
 namespace smt {
 
 /**
diff --git a/src/smt/listeners.cpp b/src/smt/listeners.cpp
index 52ddcf156..fdf32fa41 100644
--- a/src/smt/listeners.cpp
+++ b/src/smt/listeners.cpp
@@ -18,9 +18,10 @@
 #include "expr/expr.h"
 #include "expr/node_manager_attributes.h"
 #include "options/smt_options.h"
-#include "smt/node_command.h"
+#include "printer/printer.h"
 #include "smt/dump.h"
 #include "smt/dump_manager.h"
+#include "smt/node_command.h"
 #include "smt/smt_engine.h"
 #include "smt/smt_engine_scope.h"
 
@@ -36,7 +37,11 @@ void ResourceOutListener::notify()
   d_smt.interrupt();
 }
 
-SmtNodeManagerListener::SmtNodeManagerListener(DumpManager& dm) : d_dm(dm) {}
+SmtNodeManagerListener::SmtNodeManagerListener(DumpManager& dm,
+                                               OutputManager& outMgr)
+    : d_dm(dm), d_outMgr(outMgr)
+{
+}
 
 void SmtNodeManagerListener::nmNotifyNewSort(TypeNode tn, uint32_t flags)
 {
@@ -92,7 +97,8 @@ void SmtNodeManagerListener::nmNotifyNewSkolem(TNode n,
   DeclareFunctionNodeCommand c(id, n, n.getType());
   if (Dump.isOn("skolems") && comment != "")
   {
-    Dump("skolems") << CommentCommand(id + " is " + comment);
+    d_outMgr.getPrinter().toStreamCmdComment(d_outMgr.getDumpOut(),
+                                             id + " is " + comment);
   }
   if ((flags & ExprManager::VAR_FLAG_DEFINED) == 0)
   {
diff --git a/src/smt/listeners.h b/src/smt/listeners.h
index 77d6d257f..0efbed096 100644
--- a/src/smt/listeners.h
+++ b/src/smt/listeners.h
@@ -24,6 +24,7 @@
 
 namespace CVC4 {
 
+class OutputManager;
 class SmtEngine;
 
 namespace smt {
@@ -49,7 +50,7 @@ class DumpManager;
 class SmtNodeManagerListener : public NodeManagerListener
 {
  public:
-  SmtNodeManagerListener(DumpManager& dm);
+  SmtNodeManagerListener(DumpManager& dm, OutputManager& outMgr);
   /** Notify when new sort is created */
   void nmNotifyNewSort(TypeNode tn, uint32_t flags) override;
   /** Notify when new sort constructor is created */
@@ -69,6 +70,8 @@ class SmtNodeManagerListener : public NodeManagerListener
  private:
   /** Reference to the dump manager of smt engine */
   DumpManager& d_dm;
+  /** Reference to the output manager of the smt engine */
+  OutputManager& d_outMgr;
 };
 
 }  // namespace smt
diff --git a/src/smt/output_manager.cpp b/src/smt/output_manager.cpp
new file mode 100644
index 000000000..a801b7527
--- /dev/null
+++ b/src/smt/output_manager.cpp
@@ -0,0 +1,35 @@
+/*********************                                                        */
+/*! \file output_manager.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Abdalrhman Mohamed
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Implementation of OutputManager functions.
+ **
+ ** Implementation of OutputManager functions.
+ **/
+
+#include "smt/output_manager.h"
+
+#include "smt/smt_engine.h"
+
+namespace CVC4 {
+
+OutputManager::OutputManager(SmtEngine* smt) : d_smt(smt) {}
+
+const Printer& OutputManager::getPrinter() const
+{
+  return *d_smt->getPrinter();
+}
+
+std::ostream& OutputManager::getDumpOut() const
+{
+  return *d_smt->getOptions().getOut();
+}
+
+}  // namespace CVC4
diff --git a/src/smt/output_manager.h b/src/smt/output_manager.h
new file mode 100644
index 000000000..5ffd6b964
--- /dev/null
+++ b/src/smt/output_manager.h
@@ -0,0 +1,57 @@
+/*********************                                                        */
+/*! \file output_manager.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Abdalrhman Mohamed
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief The output manager for the SmtEngine.
+ **
+ ** The output manager provides helper functions for printing commands
+ ** internally.
+ **/
+
+#ifndef CVC4__SMT__OUTPUT_MANAGER_H
+#define CVC4__SMT__OUTPUT_MANAGER_H
+
+#include <ostream>
+
+namespace CVC4 {
+
+class Printer;
+class SmtEngine;
+
+/** This utility class provides helper functions for printing commands
+ * internally */
+class OutputManager
+{
+ public:
+  /** Constructor
+   *
+   * @param smt SMT engine to manage output for
+   */
+  explicit OutputManager(SmtEngine* smt);
+
+  /** Get the current printer based on the current options
+   *
+   * @return the current printer
+   */
+  const Printer& getPrinter() const;
+
+  /** Get the output stream that --dump=X should print to
+   *
+   * @return the output stream
+   */
+  std::ostream& getDumpOut() const;
+
+ private:
+  SmtEngine* d_smt;
+};
+
+}  // namespace CVC4
+
+#endif  // CVC4__SMT__OUTPUT_MANAGER_H
diff --git a/src/smt/preprocessor.cpp b/src/smt/preprocessor.cpp
index ea5ef2bad..c376c99ba 100644
--- a/src/smt/preprocessor.cpp
+++ b/src/smt/preprocessor.cpp
@@ -15,9 +15,10 @@
 #include "smt/preprocessor.h"
 
 #include "options/smt_options.h"
+#include "printer/printer.h"
 #include "smt/abstract_values.h"
 #include "smt/assertions.h"
-#include "smt/command.h"
+#include "smt/dump.h"
 #include "smt/smt_engine.h"
 
 using namespace CVC4::theory;
@@ -128,7 +129,8 @@ Node Preprocessor::simplify(const Node& node, bool removeItes)
   Trace("smt") << "SMT simplify(" << node << ")" << endl;
   if (Dump.isOn("benchmark"))
   {
-    Dump("benchmark") << SimplifyCommand(node.toExpr());
+    d_smt.getOutputManager().getPrinter().toStreamCmdSimplify(
+        d_smt.getOutputManager().getDumpOut(), node);
   }
   Node nas = d_absValues.substituteAbstractValues(node);
   if (options::typeChecking())
diff --git a/src/smt/process_assertions.cpp b/src/smt/process_assertions.cpp
index 33d092def..944f35593 100644
--- a/src/smt/process_assertions.cpp
+++ b/src/smt/process_assertions.cpp
@@ -27,7 +27,9 @@
 #include "options/uf_options.h"
 #include "preprocessing/assertion_pipeline.h"
 #include "preprocessing/preprocessing_pass_registry.h"
+#include "printer/printer.h"
 #include "smt/defined_function.h"
+#include "smt/dump.h"
 #include "smt/smt_engine.h"
 #include "theory/logic_info.h"
 #include "theory/quantifiers/fun_def_process.h"
@@ -562,7 +564,8 @@ void ProcessAssertions::dumpAssertions(const char* key,
     for (unsigned i = 0; i < assertionList.size(); ++i)
     {
       TNode n = assertionList[i];
-      Dump("assertions") << AssertCommand(Expr(n.toExpr()));
+      d_smt.getOutputManager().getPrinter().toStreamCmdAssert(
+          d_smt.getOutputManager().getDumpOut(), n);
     }
   }
 }
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index d271ca05d..d520d664c 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -71,7 +71,7 @@
 #include "smt/abduction_solver.h"
 #include "smt/abstract_values.h"
 #include "smt/assertions.h"
-#include "smt/command.h"
+#include "smt/node_command.h"
 #include "smt/defined_function.h"
 #include "smt/dump_manager.h"
 #include "smt/expr_names.h"
@@ -114,9 +114,19 @@ using namespace CVC4::theory;
 
 namespace CVC4 {
 
-namespace smt {
+// !!! Temporary until commands are migrated to the new API !!!
+std::vector<Node> exprVectorToNodes(const std::vector<Expr>& exprs)
+{
+  std::vector<Node> nodes;
+  nodes.reserve(exprs.size());
 
-}/* namespace CVC4::smt */
+  for (Expr e : exprs)
+  {
+    nodes.push_back(Node::fromExpr(e));
+  }
+
+  return nodes;
+}
 
 SmtEngine::SmtEngine(ExprManager* em, Options* optr)
     : d_state(new SmtEngineState(*this)),
@@ -127,7 +137,7 @@ SmtEngine::SmtEngine(ExprManager* em, Options* optr)
       d_exprNames(new ExprNames(getUserContext())),
       d_dumpm(new DumpManager(getUserContext())),
       d_routListener(new ResourceOutListener(*this)),
-      d_snmListener(new SmtNodeManagerListener(*d_dumpm.get())),
+      d_snmListener(new SmtNodeManagerListener(*d_dumpm.get(), d_outMgr)),
       d_smtSolver(nullptr),
       d_proofManager(nullptr),
       d_pfManager(nullptr),
@@ -143,6 +153,7 @@ SmtEngine::SmtEngine(ExprManager* em, Options* optr)
       d_isInternalSubsolver(false),
       d_statisticsRegistry(nullptr),
       d_stats(nullptr),
+      d_outMgr(this),
       d_resourceManager(nullptr),
       d_optm(nullptr),
       d_pp(nullptr),
@@ -183,7 +194,8 @@ SmtEngine::SmtEngine(ExprManager* em, Options* optr)
   d_smtSolver.reset(
       new SmtSolver(*this, *d_state, d_resourceManager.get(), *d_pp, *d_stats));
   // make the SyGuS solver
-  d_sygusSolver.reset(new SygusSolver(*d_smtSolver, *d_pp, getUserContext()));
+  d_sygusSolver.reset(
+      new SygusSolver(*d_smtSolver, *d_pp, getUserContext(), d_outMgr));
   // make the quantifier elimination solver
   d_quantElimSolver.reset(new QuantElimSolver(*d_smtSolver));
 
@@ -285,12 +297,13 @@ void SmtEngine::finishInit()
   {
       LogicInfo everything;
       everything.lock();
-      Dump("benchmark") << CommentCommand(
+      getOutputManager().getPrinter().toStreamCmdComment(
+          getOutputManager().getDumpOut(),
           "CVC4 always dumps the most general, all-supported logic (below), as "
           "some internals might require the use of a logic more general than "
-          "the input.")
-                        << SetBenchmarkLogicCommand(
-                               everything.getLogicString());
+          "the input.");
+      getOutputManager().getPrinter().toStreamCmdSetBenchmarkLogic(
+          getOutputManager().getDumpOut(), everything.getLogicString());
   }
 
   // initialize the dump manager
@@ -404,8 +417,8 @@ void SmtEngine::setLogic(const std::string& s)
     // dump out a set-logic command
     if (Dump.isOn("raw-benchmark"))
     {
-      Dump("raw-benchmark")
-          << SetBenchmarkLogicCommand(d_logic.getLogicString());
+      getOutputManager().getPrinter().toStreamCmdSetBenchmarkLogic(
+          getOutputManager().getDumpOut(), d_logic.getLogicString());
     }
   }
   catch (IllegalArgumentException& e)
@@ -459,12 +472,14 @@ void SmtEngine::setInfo(const std::string& key, const CVC4::SExpr& value)
   if(Dump.isOn("benchmark")) {
     if(key == "status") {
       string s = value.getValue();
-      BenchmarkStatus status =
-        (s == "sat") ? SMT_SATISFIABLE :
-          ((s == "unsat") ? SMT_UNSATISFIABLE : SMT_UNKNOWN);
-      Dump("benchmark") << SetBenchmarkStatusCommand(status);
+      Result::Sat status =
+          (s == "sat") ? Result::SAT
+                       : ((s == "unsat") ? Result::UNSAT : Result::SAT_UNKNOWN);
+      getOutputManager().getPrinter().toStreamCmdSetBenchmarkStatus(
+          getOutputManager().getDumpOut(), status);
     } else {
-      Dump("benchmark") << SetInfoCommand(key, value);
+      getOutputManager().getPrinter().toStreamCmdSetInfo(
+          getOutputManager().getDumpOut(), key, value);
     }
   }
 
@@ -774,16 +789,15 @@ void SmtEngine::defineFunctionsRec(
 
   if (Dump.isOn("raw-benchmark"))
   {
-    std::vector<api::Term> tFuncs = api::exprVectorToTerms(d_solver, funcs);
-    std::vector<std::vector<api::Term>> tFormals;
+    std::vector<Node> nFuncs = exprVectorToNodes(funcs);
+    std::vector<std::vector<Node>> nFormals;
     for (const std::vector<Expr>& formal : formals)
     {
-      tFormals.emplace_back(api::exprVectorToTerms(d_solver, formal));
+      nFormals.emplace_back(exprVectorToNodes(formal));
     }
-    std::vector<api::Term> tFormulas =
-        api::exprVectorToTerms(d_solver, formulas);
-    Dump("raw-benchmark") << DefineFunctionRecCommand(
-        d_solver, tFuncs, tFormals, tFormulas, global);
+    std::vector<Node> nFormulas = exprVectorToNodes(formulas);
+    getOutputManager().getPrinter().toStreamCmdDefineFunctionRec(
+        getOutputManager().getDumpOut(), nFuncs, nFormals, nFormulas);
   }
 
   ExprManager* em = getExprManager();
@@ -930,7 +944,11 @@ void SmtEngine::notifyPostSolvePost()
 
 Result SmtEngine::checkSat(const Expr& assumption, bool inUnsatCore)
 {
-  Dump("benchmark") << CheckSatCommand(assumption);
+  if (Dump.isOn("benchmark"))
+  {
+    getOutputManager().getPrinter().toStreamCmdCheckSat(
+        getOutputManager().getDumpOut(), assumption);
+  }
   std::vector<Node> assump;
   if (!assumption.isNull())
   {
@@ -941,13 +959,18 @@ Result SmtEngine::checkSat(const Expr& assumption, bool inUnsatCore)
 
 Result SmtEngine::checkSat(const vector<Expr>& assumptions, bool inUnsatCore)
 {
-  if (assumptions.empty())
-  {
-    Dump("benchmark") << CheckSatCommand();
-  }
-  else
+  if (Dump.isOn("benchmark"))
   {
-    Dump("benchmark") << CheckSatAssumingCommand(assumptions);
+    if (assumptions.empty())
+    {
+      getOutputManager().getPrinter().toStreamCmdCheckSat(
+          getOutputManager().getDumpOut());
+    }
+    else
+    {
+      getOutputManager().getPrinter().toStreamCmdCheckSatAssuming(
+          getOutputManager().getDumpOut(), exprVectorToNodes(assumptions));
+    }
   }
   std::vector<Node> assumps;
   for (const Expr& e : assumptions)
@@ -959,7 +982,11 @@ Result SmtEngine::checkSat(const vector<Expr>& assumptions, bool inUnsatCore)
 
 Result SmtEngine::checkEntailed(const Expr& node, bool inUnsatCore)
 {
-  Dump("benchmark") << QueryCommand(node, inUnsatCore);
+  if (Dump.isOn("benchmark"))
+  {
+    getOutputManager().getPrinter().toStreamCmdQuery(
+        getOutputManager().getDumpOut(), node.getNode());
+  }
   return checkSatInternal(node.isNull()
                               ? std::vector<Node>()
                               : std::vector<Node>{Node::fromExpr(node)},
@@ -1045,7 +1072,8 @@ std::vector<Node> SmtEngine::getUnsatAssumptions(void)
   finishInit();
   if (Dump.isOn("benchmark"))
   {
-    Dump("benchmark") << GetUnsatAssumptionsCommand();
+    getOutputManager().getPrinter().toStreamCmdGetUnsatAssumptions(
+        getOutputManager().getDumpOut());
   }
   UnsatCore core = getUnsatCoreInternal();
   std::vector<Node> res;
@@ -1069,7 +1097,8 @@ Result SmtEngine::assertFormula(const Node& formula, bool inUnsatCore)
   Trace("smt") << "SmtEngine::assertFormula(" << formula << ")" << endl;
 
   if (Dump.isOn("raw-benchmark")) {
-    Dump("raw-benchmark") << AssertCommand(formula.toExpr());
+    getOutputManager().getPrinter().toStreamCmdAssert(
+        getOutputManager().getDumpOut(), formula);
   }
 
   // Substitute out any abstract values in ex
@@ -1090,8 +1119,11 @@ void SmtEngine::declareSygusVar(const std::string& id, Node var, TypeNode type)
   SmtScope smts(this);
   finishInit();
   d_sygusSolver->declareSygusVar(id, var, type);
-  Dump("raw-benchmark") << DeclareSygusVarCommand(
-      id, var.toExpr(), type.toType());
+  if (Dump.isOn("raw-benchmark"))
+  {
+    getOutputManager().getPrinter().toStreamCmdDeclareVar(
+        getOutputManager().getDumpOut(), var, type);
+  }
   // don't need to set that the conjecture is stale
 }
 
@@ -1112,22 +1144,14 @@ void SmtEngine::declareSynthFun(const std::string& id,
 
   if (Dump.isOn("raw-benchmark"))
   {
-    std::stringstream ss;
-
-    Printer::getPrinter(options::outputLanguage())
-        ->toStreamCmdSynthFun(ss,
-                              id,
-                              vars,
-                              func.getType().isFunction()
-                                  ? func.getType().getRangeType()
-                                  : func.getType(),
-                              isInv,
-                              sygusType);
-
-    // must print it on the standard output channel since it is not possible
-    // to print anything except for commands with Dump.
-    std::ostream& out = *d_options.getOut();
-    out << ss.str() << std::endl;
+    getOutputManager().getPrinter().toStreamCmdSynthFun(
+        getOutputManager().getDumpOut(),
+        id,
+        vars,
+        func.getType().isFunction() ? func.getType().getRangeType()
+                                    : func.getType(),
+        isInv,
+        sygusType);
   }
 }
 
@@ -1136,7 +1160,11 @@ void SmtEngine::assertSygusConstraint(Node constraint)
   SmtScope smts(this);
   finishInit();
   d_sygusSolver->assertSygusConstraint(constraint);
-  Dump("raw-benchmark") << SygusConstraintCommand(constraint.toExpr());
+  if (Dump.isOn("raw-benchmark"))
+  {
+    getOutputManager().getPrinter().toStreamCmdConstraint(
+        getOutputManager().getDumpOut(), constraint);
+  }
 }
 
 void SmtEngine::assertSygusInvConstraint(Node inv,
@@ -1147,8 +1175,11 @@ void SmtEngine::assertSygusInvConstraint(Node inv,
   SmtScope smts(this);
   finishInit();
   d_sygusSolver->assertSygusInvConstraint(inv, pre, trans, post);
-  Dump("raw-benchmark") << SygusInvConstraintCommand(
-      inv.toExpr(), pre.toExpr(), trans.toExpr(), post.toExpr());
+  if (Dump.isOn("raw-benchmark"))
+  {
+    getOutputManager().getPrinter().toStreamCmdInvConstraint(
+        getOutputManager().getDumpOut(), inv, pre, trans, post);
+  }
 }
 
 Result SmtEngine::checkSynth()
@@ -1192,7 +1223,7 @@ Node SmtEngine::getValue(const Node& ex) const
 
   Trace("smt") << "SMT getValue(" << ex << ")" << endl;
   if(Dump.isOn("benchmark")) {
-    Dump("benchmark") << GetValueCommand(ex.toExpr());
+    d_outMgr.getPrinter().toStreamCmdGetValue(d_outMgr.getDumpOut(), {ex});
   }
   TypeNode expectedType = ex.getType();
 
@@ -1290,7 +1321,8 @@ vector<pair<Expr, Expr>> SmtEngine::getAssignment()
   SmtScope smts(this);
   finishInit();
   if(Dump.isOn("benchmark")) {
-    Dump("benchmark") << GetAssignmentCommand();
+    getOutputManager().getPrinter().toStreamCmdGetAssignment(
+        getOutputManager().getDumpOut());
   }
   if(!options::produceAssignments()) {
     const char* msg =
@@ -1351,7 +1383,8 @@ Model* SmtEngine::getModel() {
   finishInit();
 
   if(Dump.isOn("benchmark")) {
-    Dump("benchmark") << GetModelCommand();
+    getOutputManager().getPrinter().toStreamCmdGetModel(
+        getOutputManager().getDumpOut());
   }
 
   TheoryModel* m = getAvailableModel("get model");
@@ -1384,7 +1417,8 @@ Result SmtEngine::blockModel()
 
   if (Dump.isOn("benchmark"))
   {
-    Dump("benchmark") << BlockModelCommand();
+    getOutputManager().getPrinter().toStreamCmdBlockModel(
+        getOutputManager().getDumpOut());
   }
 
   TheoryModel* m = getAvailableModel("block model");
@@ -1415,7 +1449,8 @@ Result SmtEngine::blockModelValues(const std::vector<Expr>& exprs)
       "block model values must be called on non-empty set of terms");
   if (Dump.isOn("benchmark"))
   {
-    Dump("benchmark") << BlockModelValuesCommand(exprs);
+    getOutputManager().getPrinter().toStreamCmdBlockModelValues(
+        getOutputManager().getDumpOut(), exprVectorToNodes(exprs));
   }
 
   TheoryModel* m = getAvailableModel("block model values");
@@ -1573,7 +1608,8 @@ void SmtEngine::checkModel(bool hardFailure) {
   SubstitutionMap substitutions(&fakeContext, /* substituteUnderQuantifiers = */ false);
 
   for(size_t k = 0; k < m->getNumCommands(); ++k) {
-    const DeclareFunctionCommand* c = dynamic_cast<const DeclareFunctionCommand*>(m->getCommand(k));
+    const DeclareFunctionNodeCommand* c =
+        dynamic_cast<const DeclareFunctionNodeCommand*>(m->getCommand(k));
     Notice() << "SmtEngine::checkModel(): model command " << k << " : " << m->getCommand(k) << endl;
     if(c == NULL) {
       // we don't care about DECLARE-DATATYPES, DECLARE-SORT, ...
@@ -1584,7 +1620,7 @@ void SmtEngine::checkModel(bool hardFailure) {
       // We'll first do some checks, then add to our substitution map
       // the mapping: function symbol |-> value
 
-      Expr func = c->getFunction();
+      Expr func = c->getFunction().toExpr();
       Node val = m->getValue(func);
 
       Notice() << "SmtEngine::checkModel(): adding substitution: " << func << " |-> " << val << endl;
@@ -1767,7 +1803,8 @@ UnsatCore SmtEngine::getUnsatCore() {
   SmtScope smts(this);
   finishInit();
   if(Dump.isOn("benchmark")) {
-    Dump("benchmark") << GetUnsatCoreCommand();
+    getOutputManager().getPrinter().toStreamCmdGetUnsatCore(
+        getOutputManager().getDumpOut());
   }
   return getUnsatCoreInternal();
 }
@@ -1896,7 +1933,8 @@ std::vector<Expr> SmtEngine::getAssertions()
   finishInit();
   d_state->doPendingPops();
   if(Dump.isOn("benchmark")) {
-    Dump("benchmark") << GetAssertionsCommand();
+    getOutputManager().getPrinter().toStreamCmdGetAssertions(
+        getOutputManager().getDumpOut());
   }
   Trace("smt") << "SMT getAssertions()" << endl;
   if(!options::produceAssertions()) {
@@ -1923,7 +1961,8 @@ void SmtEngine::push()
   Trace("smt") << "SMT push()" << endl;
   d_smtSolver->processAssertions(*d_asserts);
   if(Dump.isOn("benchmark")) {
-    Dump("benchmark") << PushCommand();
+    getOutputManager().getPrinter().toStreamCmdPush(
+        getOutputManager().getDumpOut());
   }
   d_state->userPush();
 }
@@ -1933,7 +1972,8 @@ void SmtEngine::pop() {
   finishInit();
   Trace("smt") << "SMT pop()" << endl;
   if(Dump.isOn("benchmark")) {
-    Dump("benchmark") << PopCommand();
+    getOutputManager().getPrinter().toStreamCmdPop(
+        getOutputManager().getDumpOut());
   }
   d_state->userPop();
 
@@ -1954,7 +1994,8 @@ void SmtEngine::reset()
   ExprManager *em = d_exprManager;
   Trace("smt") << "SMT reset()" << endl;
   if(Dump.isOn("benchmark")) {
-    Dump("benchmark") << ResetCommand();
+    getOutputManager().getPrinter().toStreamCmdReset(
+        getOutputManager().getDumpOut());
   }
   std::string filename = d_state->getFilename();
   Options opts;
@@ -1983,7 +2024,8 @@ void SmtEngine::resetAssertions()
   Trace("smt") << "SMT resetAssertions()" << endl;
   if (Dump.isOn("benchmark"))
   {
-    Dump("benchmark") << ResetAssertionsCommand();
+    getOutputManager().getPrinter().toStreamCmdResetAssertions(
+        getOutputManager().getDumpOut());
   }
 
   d_state->notifyResetAssertions();
@@ -2073,7 +2115,8 @@ void SmtEngine::setOption(const std::string& key, const CVC4::SExpr& value)
   Trace("smt") << "SMT setOption(" << key << ", " << value << ")" << endl;
 
   if(Dump.isOn("benchmark")) {
-    Dump("benchmark") << SetOptionCommand(key, value);
+    getOutputManager().getPrinter().toStreamCmdSetOption(
+        getOutputManager().getDumpOut(), key, value);
   }
 
   if(key == "command-verbosity") {
@@ -2126,7 +2169,7 @@ CVC4::SExpr SmtEngine::getOption(const std::string& key) const
   }
 
   if(Dump.isOn("benchmark")) {
-    Dump("benchmark") << GetOptionCommand(key);
+    d_outMgr.getPrinter().toStreamCmdGetOption(d_outMgr.getDumpOut(), key);
   }
 
   if(key == "command-verbosity") {
@@ -2181,4 +2224,11 @@ ResourceManager* SmtEngine::getResourceManager()
 
 DumpManager* SmtEngine::getDumpManager() { return d_dumpm.get(); }
 
+const Printer* SmtEngine::getPrinter() const
+{
+  return Printer::getPrinter(d_options[options::outputLanguage]);
+}
+
+OutputManager& SmtEngine::getOutputManager() { return d_outMgr; }
+
 }/* CVC4 namespace */
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index eec17a5f8..d855e3181 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -31,6 +31,7 @@
 #include "options/options.h"
 #include "proof/unsat_core.h"
 #include "smt/logic_exception.h"
+#include "smt/output_manager.h"
 #include "smt/smt_mode.h"
 #include "theory/logic_info.h"
 #include "util/hash.h"
@@ -63,6 +64,8 @@ class Model;
 class LogicRequest;
 class StatisticsRegistry;
 
+class Printer;
+
 /* -------------------------------------------------------------------------- */
 
 namespace api {
@@ -130,6 +133,8 @@ namespace theory {
   class Rewriter;
 }/* CVC4::theory namespace */
 
+std::vector<Node> exprVectorToNodes(const std::vector<Expr>& exprs);
+
 // TODO: SAT layer (esp. CNF- versus non-clausal solvers under the
 // hood): use a type parameter and have check() delegate, or subclass
 // SmtEngine and override check()?
@@ -862,6 +867,12 @@ class CVC4_PUBLIC SmtEngine
   /** Permit access to the underlying dump manager. */
   smt::DumpManager* getDumpManager();
 
+  /** Get the printer used by this SMT engine */
+  const Printer* getPrinter() const;
+
+  /** Get the output manager for this SMT engine */
+  OutputManager& getOutputManager();
+
   /** Get a pointer to the Rewriter owned by this SmtEngine. */
   theory::Rewriter* getRewriter() { return d_rewriter.get(); }
 
@@ -1139,6 +1150,10 @@ class CVC4_PUBLIC SmtEngine
 
   /** The options object */
   Options d_options;
+
+  /** the output manager for commands */
+  mutable OutputManager d_outMgr;
+
   /**
    * Manager for limiting time and abstract resource usage.
    */
diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp
index c64689be6..922831106 100644
--- a/src/smt/smt_solver.cpp
+++ b/src/smt/smt_solver.cpp
@@ -51,7 +51,8 @@ void SmtSolver::finishInit(const LogicInfo& logicInfo)
                                         d_smt.getUserContext(),
                                         d_rm,
                                         d_pp.getTermFormulaRemover(),
-                                        logicInfo));
+                                        logicInfo,
+                                        d_smt.getOutputManager()));
 
   // Add the theories
   for (theory::TheoryId id = theory::THEORY_FIRST; id < theory::THEORY_LAST;
@@ -65,8 +66,11 @@ void SmtSolver::finishInit(const LogicInfo& logicInfo)
    * are unregistered by the obsolete PropEngine object before registered
    * again by the new PropEngine object */
   d_propEngine.reset(nullptr);
-  d_propEngine.reset(new PropEngine(
-      d_theoryEngine.get(), d_smt.getContext(), d_smt.getUserContext(), d_rm));
+  d_propEngine.reset(new PropEngine(d_theoryEngine.get(),
+                                    d_smt.getContext(),
+                                    d_smt.getUserContext(),
+                                    d_rm,
+                                    d_smt.getOutputManager()));
 
   Trace("smt-debug") << "Setting up theory engine..." << std::endl;
   d_theoryEngine->setPropEngine(getPropEngine());
@@ -82,8 +86,11 @@ void SmtSolver::resetAssertions()
    * statistics are unregistered by the obsolete PropEngine object before
    * registered again by the new PropEngine object */
   d_propEngine.reset(nullptr);
-  d_propEngine.reset(new PropEngine(
-      d_theoryEngine.get(), d_smt.getContext(), d_smt.getUserContext(), d_rm));
+  d_propEngine.reset(new PropEngine(d_theoryEngine.get(),
+                                    d_smt.getContext(),
+                                    d_smt.getUserContext(),
+                                    d_rm,
+                                    d_smt.getOutputManager()));
   d_theoryEngine->setPropEngine(getPropEngine());
   // Notice that we do not reset TheoryEngine, nor does it require calling
   // finishInit again. In particular, TheoryEngine::finishInit does not
diff --git a/src/smt/sygus_solver.cpp b/src/smt/sygus_solver.cpp
index 0fc63d198..979eaec6d 100644
--- a/src/smt/sygus_solver.cpp
+++ b/src/smt/sygus_solver.cpp
@@ -17,6 +17,8 @@
 #include "expr/dtype.h"
 #include "options/quantifiers_options.h"
 #include "options/smt_options.h"
+#include "printer/printer.h"
+#include "smt/dump.h"
 #include "smt/preprocessor.h"
 #include "smt/smt_solver.h"
 #include "theory/smt_engine_subsolver.h"
@@ -30,8 +32,12 @@ namespace smt {
 
 SygusSolver::SygusSolver(SmtSolver& sms,
                          Preprocessor& pp,
-                         context::UserContext* u)
-    : d_smtSolver(sms), d_pp(pp), d_sygusConjectureStale(u, true)
+                         context::UserContext* u,
+                         OutputManager& outMgr)
+    : d_smtSolver(sms),
+      d_pp(pp),
+      d_sygusConjectureStale(u, true),
+      d_outMgr(outMgr)
 {
 }
 
@@ -205,7 +211,10 @@ Result SygusSolver::checkSynth(Assertions& as)
     te->setUserAttribute("sygus", sygusVar, {}, "");
 
     Trace("smt") << "Check synthesis conjecture: " << body << std::endl;
-    Dump("raw-benchmark") << CheckSynthCommand();
+    if (Dump.isOn("raw-benchmark"))
+    {
+      d_outMgr.getPrinter().toStreamCmdCheckSynth(d_outMgr.getDumpOut());
+    }
 
     d_sygusConjectureStale = false;
 
diff --git a/src/smt/sygus_solver.h b/src/smt/sygus_solver.h
index 621bea9f3..deb253142 100644
--- a/src/smt/sygus_solver.h
+++ b/src/smt/sygus_solver.h
@@ -24,6 +24,9 @@
 #include "util/result.h"
 
 namespace CVC4 {
+
+class OutputManager;
+
 namespace smt {
 
 class Preprocessor;
@@ -41,7 +44,10 @@ class SmtSolver;
 class SygusSolver
 {
  public:
-  SygusSolver(SmtSolver& sms, Preprocessor& pp, context::UserContext* u);
+  SygusSolver(SmtSolver& sms,
+              Preprocessor& pp,
+              context::UserContext* u,
+              OutputManager& outMgr);
   ~SygusSolver();
 
   /**
@@ -174,6 +180,8 @@ class SygusSolver
    * Whether we need to reconstruct the sygus conjecture.
    */
   context::CDO<bool> d_sygusConjectureStale;
+  /** Reference to the output manager of the smt engine */
+  OutputManager& d_outMgr;
 };
 
 }  // namespace smt
diff --git a/src/smt/term_formula_removal.h b/src/smt/term_formula_removal.h
index 85f0c30d7..00bf74360 100644
--- a/src/smt/term_formula_removal.h
+++ b/src/smt/term_formula_removal.h
@@ -27,7 +27,6 @@
 #include "expr/node.h"
 #include "expr/term_context_stack.h"
 #include "expr/term_conversion_proof_generator.h"
-#include "smt/dump.h"
 #include "theory/eager_proof_generator.h"
 #include "theory/trust_node.h"
 #include "util/bool.h"