Replace the old dump infrastructure (#7572)

This deletes the old dumping infrastructure, which due to changes in our usage of SolverEngine does not print valid benchmarks.

This eliminates the concept of a "NodeManagerListener" which has been problematic to maintain.

This PR reimplements the --dump=assertions:pre-X and --dump=assertions:post-X as -t assertions::pre-X and -t assertions::post-X. This is done in a self contained utility method in ProcessAssertions using smt::PrintBenchmark and does not require keeping the rest of the code in sync.

The other dumping tags are deleted for now, and will be reimplemented as needed.

38 files changed, 127 insertions, 1475 deletions

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 268668dfd..1adf40695 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -281,10 +281,6 @@ libcvc5_add_sources(
   smt/command.h
   smt/difficulty_post_processor.cpp
   smt/difficulty_post_processor.h
-  smt/dump.cpp
-  smt/dump.h
-  smt/dump_manager.cpp
-  smt/dump_manager.h
   smt/env.cpp
   smt/env.h
   smt/env_obj.cpp
@@ -302,18 +298,16 @@ libcvc5_add_sources(
   smt/model_core_builder.h
   smt/model_blocker.cpp
   smt/model_blocker.h
-  smt/node_command.cpp
-  smt/node_command.h
   smt/optimization_solver.cpp
   smt/optimization_solver.h
-  smt/output_manager.cpp
-  smt/output_manager.h
   smt/quant_elim_solver.cpp
   smt/quant_elim_solver.h
   smt/preprocessor.cpp
   smt/preprocessor.h
   smt/preprocess_proof_generator.cpp
   smt/preprocess_proof_generator.h
+  smt/print_benchmark.cpp
+  smt/print_benchmark.h
   smt/process_assertions.cpp
   smt/process_assertions.h
   smt/proof_manager.cpp
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index 3734e5860..b8e22c6f7 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -365,10 +365,6 @@ void NodeManager::reclaimZombies() {
         TNode n;
         n.d_nv = nv;
         nv->d_rc = 1; // so that TNode doesn't assert-fail
-        for (NodeManagerListener* listener : d_listeners)
-        {
-          listener->nmNotifyDeleteNode(n);
-        }
         // this would mean that one of the listeners stowed away
         // a reference to this node!
         Assert(nv->d_rc == 1);
@@ -662,11 +658,6 @@ std::vector<TypeNode> NodeManager::mkMutualDatatypeTypes(
     }
   }
 
-  for (NodeManagerListener* nml : d_listeners)
-  {
-    nml->nmNotifyNewDatatypes(dtts, flags);
-  }
-
   return dtts;
 }
 
@@ -830,11 +821,7 @@ TypeNode NodeManager::mkSort(uint32_t flags) {
   NodeBuilder nb(this, kind::SORT_TYPE);
   Node sortTag = NodeBuilder(this, kind::SORT_TAG);
   nb << sortTag;
-  TypeNode tn = nb.constructTypeNode();
-  for(std::vector<NodeManagerListener*>::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) {
-    (*i)->nmNotifyNewSort(tn, flags);
-  }
-  return tn;
+  return nb.constructTypeNode();
 }
 
 TypeNode NodeManager::mkSort(const std::string& name, uint32_t flags) {
@@ -843,9 +830,6 @@ TypeNode NodeManager::mkSort(const std::string& name, uint32_t flags) {
   nb << sortTag;
   TypeNode tn = nb.constructTypeNode();
   setAttribute(tn, expr::VarNameAttr(), name);
-  for(std::vector<NodeManagerListener*>::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) {
-    (*i)->nmNotifyNewSort(tn, flags);
-  }
   return tn;
 }
 
@@ -869,9 +853,6 @@ TypeNode NodeManager::mkSort(TypeNode constructor,
   nb.append(children);
   TypeNode type = nb.constructTypeNode();
   setAttribute(type, expr::VarNameAttr(), name);
-  for(std::vector<NodeManagerListener*>::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) {
-    (*i)->nmNotifyInstantiateSortConstructor(constructor, type, flags);
-  }
   return type;
 }
 
@@ -886,9 +867,6 @@ TypeNode NodeManager::mkSortConstructor(const std::string& name,
   TypeNode type = nb.constructTypeNode();
   setAttribute(type, expr::VarNameAttr(), name);
   setAttribute(type, expr::SortArityAttr(), arity);
-  for(std::vector<NodeManagerListener*>::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) {
-    (*i)->nmNotifyNewSortConstructor(type, flags);
-  }
   return type;
 }
 
@@ -898,9 +876,6 @@ Node NodeManager::mkVar(const std::string& name, const TypeNode& type)
   setAttribute(n, TypeAttr(), type);
   setAttribute(n, TypeCheckedAttr(), true);
   setAttribute(n, expr::VarNameAttr(), name);
-  for(std::vector<NodeManagerListener*>::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) {
-    (*i)->nmNotifyNewVar(n);
-  }
   return n;
 }
 
@@ -1021,9 +996,6 @@ Node NodeManager::mkVar(const TypeNode& type)
   Node n = NodeBuilder(this, kind::VARIABLE);
   setAttribute(n, TypeAttr(), type);
   setAttribute(n, TypeCheckedAttr(), true);
-  for(std::vector<NodeManagerListener*>::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) {
-    (*i)->nmNotifyNewVar(n);
-  }
   return n;
 }
 
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 5b5f07e6f..d0c607a4b 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -56,30 +56,6 @@ namespace expr {
   class TypeChecker;
   }  // namespace expr
 
-/**
- * An interface that an interested party can implement and then subscribe
- * to NodeManager events via NodeManager::subscribeEvents(this).
- */
-class NodeManagerListener {
- public:
-  virtual ~NodeManagerListener() {}
-  virtual void nmNotifyNewSort(TypeNode tn, uint32_t flags) {}
-  virtual void nmNotifyNewSortConstructor(TypeNode tn, uint32_t flags) {}
-  virtual void nmNotifyInstantiateSortConstructor(TypeNode ctor, TypeNode sort,
-                                                  uint32_t flags) {}
-  virtual void nmNotifyNewDatatypes(const std::vector<TypeNode>& datatypes,
-                                    uint32_t flags)
-  {
-  }
-  virtual void nmNotifyNewVar(TNode n) {}
-  /**
-   * Notify a listener of a Node that's being GCed.  If this function stores a
-   * reference
-   * to the Node somewhere, very bad things will happen.
-   */
-  virtual void nmNotifyDeleteNode(TNode n) {}
-}; /* class NodeManagerListener */
-
 class NodeManager
 {
   friend class api::Solver;
@@ -175,11 +151,6 @@ class NodeManager
   /** unique vars per (Kind,Type) */
   std::map< Kind, std::map< TypeNode, Node > > d_unique_vars;
 
-  /**
-   * A list of subscribers for NodeManager events.
-   */
-  std::vector<NodeManagerListener*> d_listeners;
-
   /** A list of datatypes owned by this node manager */
   std::vector<std::unique_ptr<DType> > d_dtypes;
 
@@ -370,21 +341,6 @@ class NodeManager
   /** Get this node manager's bound variable manager */
   BoundVarManager* getBoundVarManager() { return d_bvManager.get(); }
 
-  /** Subscribe to NodeManager events */
-  void subscribeEvents(NodeManagerListener* listener) {
-    Assert(std::find(d_listeners.begin(), d_listeners.end(), listener)
-           == d_listeners.end())
-        << "listener already subscribed";
-    d_listeners.push_back(listener);
-  }
-
-  /** Unsubscribe from NodeManager events */
-  void unsubscribeEvents(NodeManagerListener* listener) {
-    std::vector<NodeManagerListener*>::iterator elt = std::find(d_listeners.begin(), d_listeners.end(), listener);
-    Assert(elt != d_listeners.end()) << "listener not subscribed";
-    d_listeners.erase(elt);
-  }
-
   /**
    * Return the datatype at the given index owned by this class. Type nodes are
    * associated with datatypes through the DatatypeIndexConstant class. The
diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp
index b58063dbb..d5d61977c 100644
--- a/src/options/options_handler.cpp
+++ b/src/options/options_handler.cpp
@@ -38,7 +38,6 @@
 #include "options/smt_options.h"
 #include "options/theory_options.h"
 #include "smt/command.h"
-#include "smt/dump.h"
 #include "util/didyoumean.h"
 
 namespace cvc5 {
@@ -375,7 +374,6 @@ void OptionsHandler::setDefaultDagThresh(const std::string& flag, int dag)
   Chat.getStream() << expr::ExprDag(dag);
   CVC5Message.getStream() << expr::ExprDag(dag);
   Warning.getStream() << expr::ExprDag(dag);
-  Dump.getStream() << expr::ExprDag(dag);
 }
 
 static void print_config(const char* str, std::string config)
@@ -475,27 +473,5 @@ void OptionsHandler::showTraceTags(const std::string& flag)
   std::exit(0);
 }
 
-void OptionsHandler::setDumpMode(const std::string& flag,
-                                 const std::string& optarg)
-{
-#ifdef CVC5_DUMPING
-  Dump.setDumpFromString(optarg);
-#else  /* CVC5_DUMPING */
-  throw OptionException(
-      "The dumping feature was disabled in this build of cvc5.");
-#endif /* CVC5_DUMPING */
-}
-
-void OptionsHandler::setDumpStream(const std::string& flag,
-                                   const ManagedOut& mo)
-{
-#ifdef CVC5_DUMPING
-  Dump.setStream(mo);
-#else  /* CVC5_DUMPING */
-  throw OptionException(
-      "The dumping feature was disabled in this build of cvc5.");
-#endif /* CVC5_DUMPING */
-}
-
 }  // namespace options
 }  // namespace cvc5
diff --git a/src/options/options_handler.h b/src/options/options_handler.h
index 077e2119d..884298930 100644
--- a/src/options/options_handler.h
+++ b/src/options/options_handler.h
@@ -130,12 +130,6 @@ class OptionsHandler
   /** Show all trace tags and exit */
   void showTraceTags(const std::string& flag);
 
-  /******************************* smt options *******************************/
-  /** Set a mode on the dumping output stream. */
-  void setDumpMode(const std::string& flag, const std::string& optarg);
-  /** Set the dumping output stream. */
-  void setDumpStream(const std::string& flag, const ManagedOut& mo);
-
  private:
   /** Pointer to the containing Options object.*/
   Options* d_options;
diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml
index 420496190..2e2742e73 100644
--- a/src/options/smt_options.toml
+++ b/src/options/smt_options.toml
@@ -2,23 +2,6 @@ id     = "SMT"
 name   = "SMT Layer"
 
 [[option]]
-  name       = "dumpModeString"
-  category   = "common"
-  long       = "dump=MODE"
-  type       = "std::string"
-  help       = "dump preprocessed assertions, etc., see --dump=help"
-  predicates = ["setDumpMode"]
-
-[[option]]
-  name       = "dumpToFileName"
-  category   = "common"
-  long       = "dump-to=FILE"
-  type       = "ManagedOut"
-  help       = "all dumping goes to FILE (instead of stdout)"
-  predicates = ["setDumpStream"]
-  includes   = ["<iostream>", "options/managed_streams.h"]
-
-[[option]]
   name       = "ackermann"
   category   = "regular"
   long       = "ackermann"
diff --git a/src/preprocessing/passes/sort_infer.cpp b/src/preprocessing/passes/sort_infer.cpp
index 68fb89e1f..107e789bb 100644
--- a/src/preprocessing/passes/sort_infer.cpp
+++ b/src/preprocessing/passes/sort_infer.cpp
@@ -19,7 +19,6 @@
 #include "options/uf_options.h"
 #include "preprocessing/assertion_pipeline.h"
 #include "preprocessing/preprocessing_pass_context.h"
-#include "smt/dump_manager.h"
 #include "theory/rewriter.h"
 #include "theory/sort_inference.h"
 #include "theory/theory_engine.h"
@@ -70,13 +69,9 @@ PreprocessingPassResult SortInferencePass::applyInternal(
           << endl;
       assertionsToPreprocess->push_back(nar);
     }
-    // indicate correspondence between the functions
-    smt::DumpManager* dm = d_env.getDumpManager();
-    for (const std::pair<const Node, Node>& mrf : model_replace_f)
-    {
-      dm->setPrintFuncInModel(mrf.first, false);
-      dm->setPrintFuncInModel(mrf.second, true);
-    }
+    // could indicate correspondence between the functions
+    // for (f1, f2) in model_replace_f, f1's model should be based on f2.
+    // See cvc4-wishues/issues/75.
   }
   // only need to compute monotonicity on the resulting formula if we are
   // using this option
diff --git a/src/preprocessing/preprocessing_pass.cpp b/src/preprocessing/preprocessing_pass.cpp
index 244e551f7..f7e300a2d 100644
--- a/src/preprocessing/preprocessing_pass.cpp
+++ b/src/preprocessing/preprocessing_pass.cpp
@@ -18,9 +18,7 @@
 #include "preprocessing/assertion_pipeline.h"
 #include "preprocessing/preprocessing_pass_context.h"
 #include "printer/printer.h"
-#include "smt/dump.h"
 #include "smt/env.h"
-#include "smt/output_manager.h"
 #include "smt/smt_statistics_registry.h"
 #include "smt/solver_engine_scope.h"
 #include "util/statistics_stats.h"
@@ -33,29 +31,11 @@ PreprocessingPassResult PreprocessingPass::apply(
   TimerStat::CodeTimer codeTimer(d_timer);
   Trace("preprocessing") << "PRE " << d_name << std::endl;
   Chat() << d_name << "..." << std::endl;
-  dumpAssertions(("pre-" + d_name).c_str(), *assertionsToPreprocess);
   PreprocessingPassResult result = applyInternal(assertionsToPreprocess);
-  dumpAssertions(("post-" + d_name).c_str(), *assertionsToPreprocess);
   Trace("preprocessing") << "POST " << d_name << std::endl;
   return result;
 }
 
-void PreprocessingPass::dumpAssertions(const char* key,
-                                       const AssertionPipeline& assertionList) {
-  if (Dump.isOn("assertions") && Dump.isOn(std::string("assertions:") + key))
-  {
-    // Push the simplified assertions to the dump output stream
-    Env& env = d_preprocContext->getEnv();
-    const Printer& printer = env.getPrinter();
-    std::ostream& out = env.getDumpOut();
-
-    for (const auto& n : assertionList)
-    {
-      printer.toStreamCmdAssert(out, n);
-    }
-  }
-}
-
 PreprocessingPass::PreprocessingPass(PreprocessingPassContext* preprocContext,
                                      const std::string& name)
     : EnvObj(preprocContext->getEnv()),
diff --git a/src/preprocessing/preprocessing_pass.h b/src/preprocessing/preprocessing_pass.h
index cc438e5c6..bd141261f 100644
--- a/src/preprocessing/preprocessing_pass.h
+++ b/src/preprocessing/preprocessing_pass.h
@@ -60,11 +60,6 @@ class PreprocessingPass : protected EnvObj
   virtual ~PreprocessingPass();
 
  protected:
-  /*
-   * Method for dumping assertions within a pass. Also called before and after
-   * applying the pass.
-   */
-  void dumpAssertions(const char* key, const AssertionPipeline& assertionList);
 
   /*
    * Abstract method that each pass implements to do the actual preprocessing.
diff --git a/src/printer/ast/ast_printer.cpp b/src/printer/ast/ast_printer.cpp
index e8bdab039..c35d55d05 100644
--- a/src/printer/ast/ast_printer.cpp
+++ b/src/printer/ast/ast_printer.cpp
@@ -24,7 +24,6 @@
 #include "options/language.h"  // for LANG_AST
 #include "printer/let_binding.h"
 #include "smt/command.h"
-#include "smt/node_command.h"
 
 using namespace std;
 
diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp
index cc9df91f4..b66ae5728 100644
--- a/src/printer/printer.cpp
+++ b/src/printer/printer.cpp
@@ -23,7 +23,6 @@
 #include "printer/tptp/tptp_printer.h"
 #include "proof/unsat_core.h"
 #include "smt/command.h"
-#include "smt/node_command.h"
 #include "theory/quantifiers/instantiation_list.h"
 
 using namespace std;
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index da8e56448..51458d66e 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -41,8 +41,6 @@
 #include "printer/let_binding.h"
 #include "proof/unsat_core.h"
 #include "smt/command.h"
-#include "smt/node_command.h"
-#include "smt/solver_engine.h"
 #include "smt_util/boolean_simplification.h"
 #include "theory/arrays/theory_arrays_rewriter.h"
 #include "theory/datatypes/sygus_datatype_utils.h"
diff --git a/src/printer/tptp/tptp_printer.cpp b/src/printer/tptp/tptp_printer.cpp
index e5f2ea55d..fe44becb6 100644
--- a/src/printer/tptp/tptp_printer.cpp
+++ b/src/printer/tptp/tptp_printer.cpp
@@ -24,7 +24,6 @@
 #include "options/smt_options.h"  // for unsat cores
 #include "proof/unsat_core.h"
 #include "smt/command.h"
-#include "smt/node_command.h"
 #include "smt/solver_engine.h"
 
 using namespace std;
diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp
index 1bac953fd..4026760f7 100644
--- a/src/prop/cnf_stream.cpp
+++ b/src/prop/cnf_stream.cpp
@@ -26,7 +26,6 @@
 #include "prop/minisat/minisat.h"
 #include "prop/prop_engine.h"
 #include "prop/theory_proxy.h"
-#include "smt/dump.h"
 #include "smt/env.h"
 #include "smt/smt_statistics_registry.h"
 #include "smt/solver_engine_scope.h"
@@ -61,26 +60,6 @@ CnfStream::CnfStream(SatSolver* satSolver,
 bool CnfStream::assertClause(TNode node, SatClause& c)
 {
   Trace("cnf") << "Inserting into stream " << c << " node = " << node << "\n";
-  if (Dump.isOn("clauses") && d_env != nullptr)
-  {
-    const Printer& printer = d_env->getPrinter();
-    std::ostream& out = d_env->getDumpOut();
-    if (c.size() == 1)
-    {
-      printer.toStreamCmdAssert(out, getNode(c[0]));
-    }
-    else
-    {
-      Assert(c.size() > 1);
-      NodeBuilder b(kind::OR);
-      for (unsigned i = 0; i < c.size(); ++i)
-      {
-        b << getNode(c[i]);
-      }
-      Node n = b;
-      printer.toStreamCmdAssert(out, n);
-    }
-  }
 
   ClauseId clauseId = d_satSolver->addClause(c, d_removable);
 
@@ -207,8 +186,7 @@ SatLiteral CnfStream::newLiteral(TNode node, bool isTheoryAtom, bool preRegister
   }
 
   // If it's a theory literal, need to store it for back queries
-  if (isTheoryAtom || d_flitPolicy == FormulaLitPolicy::TRACK
-      || (Dump.isOn("clauses")))
+  if (isTheoryAtom || d_flitPolicy == FormulaLitPolicy::TRACK)
   {
     d_literalToNodeMap.insert_safe(lit, node);
     d_literalToNodeMap.insert_safe(~lit, node.notNode());
diff --git a/src/smt/check_models.cpp b/src/smt/check_models.cpp
index 13e504835..d7f654fc6 100644
--- a/src/smt/check_models.cpp
+++ b/src/smt/check_models.cpp
@@ -18,7 +18,6 @@
 #include "base/modal_exception.h"
 #include "options/smt_options.h"
 #include "smt/env.h"
-#include "smt/node_command.h"
 #include "smt/preprocessor.h"
 #include "smt/smt_solver.h"
 #include "theory/rewriter.h"
diff --git a/src/smt/command.cpp b/src/smt/command.cpp
index 1794765b4..a15e20998 100644
--- a/src/smt/command.cpp
+++ b/src/smt/command.cpp
@@ -36,7 +36,6 @@
 #include "options/smt_options.h"
 #include "printer/printer.h"
 #include "proof/unsat_core.h"
-#include "smt/dump.h"
 #include "smt/model.h"
 #include "util/smt2_quote_string.h"
 #include "util/unsafe_interrupt_exception.h"
@@ -991,7 +990,6 @@ void ResetAssertionsCommand::toStream(std::ostream& out,
 
 void QuitCommand::invoke(api::Solver* solver, SymbolManager* sm)
 {
-  Dump("benchmark") << *this;
   d_commandStatus = CommandSuccess::instance();
 }
 
diff --git a/src/smt/dump.cpp b/src/smt/dump.cpp
deleted file mode 100644
index ab6144e02..000000000
--- a/src/smt/dump.cpp
+++ /dev/null
@@ -1,231 +0,0 @@
-/******************************************************************************
- * Top contributors (to current version):
- *   Andres Noetzli, Morgan Deters, Tim King
- *
- * This file is part of the cvc5 project.
- *
- * Copyright (c) 2009-2021 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.
- * ****************************************************************************
- *
- * Dump utility classes and functions.
- */
-
-#include "smt/dump.h"
-
-#include "base/configuration.h"
-#include "base/output.h"
-#include "lib/strtok_r.h"
-#include "options/option_exception.h"
-#include "preprocessing/preprocessing_pass_registry.h"
-#include "smt/command.h"
-#include "smt/node_command.h"
-
-namespace cvc5 {
-
-#if defined(CVC5_DUMPING) && !defined(CVC5_MUZZLE)
-
-CVC5dumpstream& CVC5dumpstream::operator<<(const Command& c)
-{
-  if (d_os != nullptr)
-  {
-    (*d_os) << c;
-  }
-  return *this;
-}
-
-CVC5dumpstream& CVC5dumpstream::operator<<(const NodeCommand& nc)
-{
-  if (d_os != nullptr)
-  {
-    (*d_os) << nc;
-  }
-  return *this;
-}
-
-#else
-
-CVC5dumpstream& CVC5dumpstream::operator<<(const Command& c) { return *this; }
-CVC5dumpstream& CVC5dumpstream::operator<<(const NodeCommand& nc)
-{
-  return *this;
-}
-
-#endif /* CVC5_DUMPING && !CVC5_MUZZLE */
-
-DumpC DumpChannel;
-
-std::ostream& DumpC::setStream(std::ostream* os)
-{
-  ::cvc5::DumpOutChannel.setStream(os);
-  return *os;
-}
-std::ostream& DumpC::getStream() { return ::cvc5::DumpOutChannel.getStream(); }
-std::ostream* DumpC::getStreamPointer()
-{
-  return ::cvc5::DumpOutChannel.getStreamPointer();
-}
-
-void DumpC::setDumpFromString(const std::string& optarg)
-{
-  if (Configuration::isDumpingBuild())
-  {
-    // Make a copy of optarg for strtok_r to use.
-    std::string optargCopy = optarg;
-    char* optargPtr = const_cast<char*>(optargCopy.c_str());
-    char* tokstr = optargPtr;
-    char* toksave;
-    while ((optargPtr = strtok_r(tokstr, ",", &toksave)) != NULL)
-    {
-      tokstr = NULL;
-      if (!strcmp(optargPtr, "benchmark"))
-      {
-      }
-      else if (!strcmp(optargPtr, "declarations"))
-      {
-      }
-      else if (!strcmp(optargPtr, "assertions"))
-      {
-        Dump.on("assertions:post-everything");
-      }
-      else if (!strncmp(optargPtr, "assertions:", 11))
-      {
-        const char* p = optargPtr + 11;
-        if (!strncmp(p, "pre-", 4))
-        {
-          p += 4;
-        }
-        else if (!strncmp(p, "post-", 5))
-        {
-          p += 5;
-        }
-        else
-        {
-          throw OptionException(std::string("don't know how to dump `")
-                                + optargPtr
-                                + "'.  Please consult --dump help.");
-        }
-        // hard-coded cases
-        if (!strcmp(p, "everything") || !strcmp(p, "definition-expansion")
-            || !strcmp(p, "simplify") || !strcmp(p, "repeat-simplify"))
-        {
-        }
-        else if (preprocessing::PreprocessingPassRegistry::getInstance()
-                     .hasPass(p))
-        {
-        }
-        else
-        {
-          throw OptionException(std::string("don't know how to dump `")
-                                + optargPtr
-                                + "'.  Please consult --dump help.");
-        }
-        Dump.on("assertions");
-      }
-      else if (!strcmp(optargPtr, "skolems"))
-      {
-      }
-      else if (!strcmp(optargPtr, "clauses"))
-      {
-      }
-      else if (!strcmp(optargPtr, "t-conflicts")
-               || !strcmp(optargPtr, "t-lemmas")
-               || !strcmp(optargPtr, "t-explanations")
-               || !strcmp(optargPtr, "theory::fullcheck"))
-      {
-      }
-      else if (!strcmp(optargPtr, "help"))
-      {
-        puts(s_dumpHelp.c_str());
-
-        std::stringstream ss;
-        ss << "Available preprocessing passes:\n";
-        for (const std::string& pass :
-             preprocessing::PreprocessingPassRegistry::getInstance()
-                 .getAvailablePasses())
-        {
-          ss << "- " << pass << "\n";
-        }
-        puts(ss.str().c_str());
-        exit(1);
-      }
-      else
-      {
-        throw OptionException(std::string("unknown option for --dump: `")
-                              + optargPtr + "'.  Try --dump help.");
-      }
-
-      Dump.on(optargPtr);
-      Dump.on("benchmark");
-      if (strcmp(optargPtr, "benchmark"))
-      {
-        Dump.on("declarations");
-      }
-    }
-  }
-  else
-  {
-    throw OptionException(
-        "The dumping feature was disabled in this build of cvc5.");
-  }
-}
-
-const std::string DumpC::s_dumpHelp =
-    "\
-Dump modes currently supported by the --dump option:\n\
-\n\
-benchmark\n\
-+ Dump the benchmark structure (set-logic, push/pop, queries, etc.), but\n\
-  does not include any declarations or assertions.  Implied by all following\n\
-  modes.\n\
-\n\
-declarations\n\
-+ Dump user declarations.  Implied by all following modes.\n\
-\n\
-skolems\n\
-+ Dump internally-created skolem variable declarations.  These can\n\
-  arise from preprocessing simplifications, existential elimination,\n\
-  and a number of other things.  Implied by all following modes.\n\
-\n\
-assertions\n\
-+ Output the assertions after preprocessing and before clausification.\n\
-  Can also specify \"assertions:pre-PASS\" or \"assertions:post-PASS\",\n\
-  where PASS is one of the preprocessing passes: definition-expansion\n\
-  boolean-terms constrain-subtypes substitution bv-to-bool bool-to-bv\n\
-  strings-pp skolem-quant simplify static-learning ite-removal\n\
-  repeat-simplify rewrite-apply-to-const theory-preprocessing.\n\
-  PASS can also be the special value \"everything\", in which case the\n\
-  assertions are printed before any preprocessing (with\n\
-  \"assertions:pre-everything\") or after all preprocessing completes\n\
-  (with \"assertions:post-everything\").\n\
-\n\
-clauses\n\
-+ Do all the preprocessing outlined above, and dump the CNF-converted\n\
-  output\n\
-\n\
-t-conflicts\n\
-+ Output correctness queries for all theory conflicts\n\
-\n\
-t-lemmas\n\
-+ Output correctness queries for all theory lemmas\n\
-\n\
-t-explanations\n\
-+ Output correctness queries for all theory explanations\n\
-\n\
-theory::fullcheck\n\
-+ Output completeness queries for all full-check effort-level theory checks\n\
-\n\
-Dump modes can be combined by concatenating the above values with \",\" in\n\
-between them.  Generally you want one from the assertions category (either\n\
-assertions or clauses), and perhaps one or more other modes for checking\n\
-correctness and completeness of decision procedure implementations.\n\
-\n\
-The --output-language option controls the language used for dumping, and\n\
-this allows you to connect cvc5 to another solver implementation via a UNIX\n\
-pipe to perform on-line checking.  The --dump-to option can be used to dump\n\
-to a file.\n\
-";
-
-}  // namespace cvc5
diff --git a/src/smt/dump.h b/src/smt/dump.h
deleted file mode 100644
index 3038d8996..000000000
--- a/src/smt/dump.h
+++ /dev/null
@@ -1,118 +0,0 @@
-/******************************************************************************
- * Top contributors (to current version):
- *   Morgan Deters, Andres Noetzli, Abdalrhman Mohamed
- *
- * This file is part of the cvc5 project.
- *
- * Copyright (c) 2009-2021 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.
- * ****************************************************************************
- *
- * Dump utility classes and functions.
- */
-
-#include "cvc5_private.h"
-
-#ifndef CVC5__DUMP_H
-#define CVC5__DUMP_H
-
-#include "base/output.h"
-
-namespace cvc5 {
-
-class Command;
-class NodeCommand;
-
-#if defined(CVC5_DUMPING) && !defined(CVC5_MUZZLE)
-
-class CVC5dumpstream
-{
- public:
-  CVC5dumpstream() : d_os(nullptr) {}
-  CVC5dumpstream(std::ostream& os) : d_os(&os) {}
-
-  CVC5dumpstream& 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.
-   */
-  CVC5dumpstream& operator<<(const NodeCommand& nc);
-
- private:
-  std::ostream* d_os;
-}; /* class CVC5dumpstream */
-
-#else
-
-/**
- * Dummy implementation of the dump stream when dumping is disabled or the
- * build is muzzled.
- */
-class CVC5dumpstream
-{
- public:
-  CVC5dumpstream() {}
-  CVC5dumpstream(std::ostream& os) {}
-  CVC5dumpstream& operator<<(const Command& c);
-  CVC5dumpstream& operator<<(const NodeCommand& nc);
-}; /* class CVC5dumpstream */
-
-#endif /* CVC5_DUMPING && !CVC5_MUZZLE */
-
-/** The dump class */
-class DumpC
-{
- public:
-  CVC5dumpstream operator()(const char* tag)
-  {
-    if(!d_tags.empty() && d_tags.find(std::string(tag)) != d_tags.end()) {
-      return CVC5dumpstream(getStream());
-    } else {
-      return CVC5dumpstream();
-    }
-  }
-
-  CVC5dumpstream operator()(std::string tag)
-  {
-    if(!d_tags.empty() && d_tags.find(tag) != d_tags.end()) {
-      return CVC5dumpstream(getStream());
-    } else {
-      return CVC5dumpstream();
-    }
-  }
-
-  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);
-  std::ostream& getStream();
-  std::ostream* getStreamPointer();
-
-  void setDumpFromString(const std::string& optarg);
-
- private:
-  /** Set of dumping tags that are currently active. */
-  std::set<std::string> d_tags;
-
-  /** The message printed on `--dump help`. */
-  static const std::string s_dumpHelp;
-};/* class DumpC */
-
-/** The dump singleton */
-extern DumpC DumpChannel;
-
-#define Dump ::cvc5::DumpChannel
-
-}  // namespace cvc5
-
-#endif /* CVC5__DUMP_H */
diff --git a/src/smt/dump_manager.cpp b/src/smt/dump_manager.cpp
deleted file mode 100644
index 83ff8e6b9..000000000
--- a/src/smt/dump_manager.cpp
+++ /dev/null
@@ -1,76 +0,0 @@
-/******************************************************************************
- * Top contributors (to current version):
- *   Andrew Reynolds, Gereon Kremer, Morgan Deters
- *
- * This file is part of the cvc5 project.
- *
- * Copyright (c) 2009-2021 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.
- * ****************************************************************************
- *
- * Implementation of the dump manager.
- */
-
-#include "smt/dump_manager.h"
-
-#include "options/smt_options.h"
-#include "smt/dump.h"
-#include "smt/node_command.h"
-
-namespace cvc5 {
-namespace smt {
-
-DumpManager::DumpManager(context::UserContext* u)
-    : d_fullyInited(false),
-      d_dumpCommands()
-{
-}
-
-DumpManager::~DumpManager()
-{
-  d_dumpCommands.clear();
-}
-
-void DumpManager::finishInit()
-{
-  Trace("smt-debug") << "Dump declaration commands..." << std::endl;
-  // dump out any pending declaration commands
-  for (size_t i = 0, ncoms = d_dumpCommands.size(); i < ncoms; ++i)
-  {
-    Dump("declarations") << *d_dumpCommands[i];
-  }
-  d_dumpCommands.clear();
-
-  d_fullyInited = true;
-}
-void DumpManager::resetAssertions()
-{
-  // currently, do nothing
-}
-
-void DumpManager::addToDump(const NodeCommand& c, const char* dumpTag)
-{
-  Trace("smt") << "SMT addToDump(" << c << ")" << std::endl;
-  if (Dump.isOn(dumpTag))
-  {
-    if (d_fullyInited)
-    {
-      Dump(dumpTag) << c;
-    }
-    else
-    {
-      d_dumpCommands.push_back(std::unique_ptr<NodeCommand>(c.clone()));
-    }
-  }
-}
-
-void DumpManager::setPrintFuncInModel(Node f, bool p)
-{
-  Trace("setp-model") << "Set printInModel " << f << " to " << p << std::endl;
-  // TODO (cvc4-wishues/issues/75): implement
-}
-
-}  // namespace smt
-}  // namespace cvc5
diff --git a/src/smt/dump_manager.h b/src/smt/dump_manager.h
deleted file mode 100644
index b6e0ccfa2..000000000
--- a/src/smt/dump_manager.h
+++ /dev/null
@@ -1,81 +0,0 @@
-/******************************************************************************
- * Top contributors (to current version):
- *   Andrew Reynolds, Morgan Deters, Gereon Kremer
- *
- * This file is part of the cvc5 project.
- *
- * Copyright (c) 2009-2021 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.
- * ****************************************************************************
- *
- * The dump manager of the SolverEngine.
- */
-
-#include "cvc5_private.h"
-
-#ifndef CVC5__SMT__DUMP_MANAGER_H
-#define CVC5__SMT__DUMP_MANAGER_H
-
-#include <memory>
-#include <vector>
-
-#include "expr/node.h"
-
-namespace cvc5 {
-
-class NodeCommand;
-
-namespace context {
-class UserContext;
-}
-
-namespace smt {
-
-/**
- * This utility is responsible for:
- * implementing some dumping traces e.g. --dump=declarations.
- */
-class DumpManager
-{
-
- public:
-  DumpManager(context::UserContext* u);
-  ~DumpManager();
-  /**
-   * Finish init, called during SolverEngine::finishInit, which is triggered
-   * when initialization of options is finished.
-   */
-  void finishInit();
-  /**
-   * Reset assertions, called on SolverEngine::resetAssertions.
-   */
-  void resetAssertions();
-  /**
-   * Add to dump command.  This is used for recording a command
-   * that should be reported via the dumpTag trace.
-   */
-  void addToDump(const NodeCommand& c, const char* dumpTag = "declarations");
-
-  /**
-   * Set that function f should print in the model if and only if p is true.
-   */
-  void setPrintFuncInModel(Node f, bool p);
-
- private:
-  /** Fully inited */
-  bool d_fullyInited;
-  /**
-   * A vector of declaration commands waiting to be dumped out.
-   * Once the SolverEngine is fully initialized, we'll dump them.
-   * This ensures the declarations come after the set-logic and
-   * any necessary set-option commands are dumped.
-   */
-  std::vector<std::unique_ptr<NodeCommand>> d_dumpCommands;
-};
-
-}  // namespace smt
-}  // namespace cvc5
-
-#endif
diff --git a/src/smt/env.cpp b/src/smt/env.cpp
index dc9efdf91..641360456 100644
--- a/src/smt/env.cpp
+++ b/src/smt/env.cpp
@@ -24,7 +24,6 @@
 #include "options/strings_options.h"
 #include "printer/printer.h"
 #include "proof/conv_proof_generator.h"
-#include "smt/dump_manager.h"
 #include "smt/solver_engine_stats.h"
 #include "theory/evaluator.h"
 #include "theory/rewriter.h"
@@ -45,7 +44,6 @@ Env::Env(NodeManager* nm, const Options* opts)
       d_evalRew(nullptr),
       d_eval(nullptr),
       d_topLevelSubs(new theory::TrustSubstitutionMap(d_userContext.get())),
-      d_dumpManager(new DumpManager(d_userContext.get())),
       d_logic(),
       d_statisticsRegistry(std::make_unique<StatisticsRegistry>(*this)),
       d_options(),
@@ -80,7 +78,6 @@ void Env::setProofNodeManager(ProofNodeManager* pnm)
 void Env::shutdown()
 {
   d_rewriter.reset(nullptr);
-  d_dumpManager.reset(nullptr);
   // d_resourceManager must be destroyed before d_statisticsRegistry
   d_resourceManager.reset(nullptr);
 }
@@ -123,8 +120,6 @@ theory::TrustSubstitutionMap& Env::getTopLevelSubstitutions()
   return *d_topLevelSubs.get();
 }
 
-DumpManager* Env::getDumpManager() { return d_dumpManager.get(); }
-
 const LogicInfo& Env::getLogicInfo() const { return d_logic; }
 
 StatisticsRegistry& Env::getStatisticsRegistry()
@@ -146,8 +141,6 @@ const Printer& Env::getPrinter()
   return *Printer::getPrinter(d_options.base.outputLanguage);
 }
 
-std::ostream& Env::getDumpOut() { return *d_options.base.out; }
-
 bool Env::isOutputOn(OutputTag tag) const
 {
   return d_options.base.outputTagHolder[static_cast<size_t>(tag)];
diff --git a/src/smt/env.h b/src/smt/env.h
index 25f8d0b71..f94d8efea 100644
--- a/src/smt/env.h
+++ b/src/smt/env.h
@@ -44,7 +44,6 @@ class UserContext;
 }  // namespace context
 
 namespace smt {
-class DumpManager;
 class PfManager;
 }
 
@@ -119,9 +118,6 @@ class Env
   /** Get a reference to the top-level substitution map */
   theory::TrustSubstitutionMap& getTopLevelSubstitutions();
 
-  /** Get a pointer to the underlying dump manager. */
-  smt::DumpManager* getDumpManager();
-
   /** Get the options object (const version only) owned by this Env. */
   const Options& getOptions() const;
 
@@ -146,12 +142,6 @@ class Env
   const Printer& getPrinter();
 
   /**
-   * Get the output stream that --dump=X should print to
-   * @return the output stream
-   */
-  std::ostream& getDumpOut();
-
-  /**
    * Check whether the output for the given output tag is enabled. Output tags
    * are enabled via the `output` option (or `-o` on the command line).
    */
@@ -284,8 +274,6 @@ class Env
   std::unique_ptr<theory::Evaluator> d_eval;
   /** The top level substitutions */
   std::unique_ptr<theory::TrustSubstitutionMap> d_topLevelSubs;
-  /** The dump manager */
-  std::unique_ptr<smt::DumpManager> d_dumpManager;
   /**
    * The logic we're in. This logic may be an extension of the logic set by the
    * user, which may be different from the user-provided logic due to the
diff --git a/src/smt/listeners.cpp b/src/smt/listeners.cpp
index 7a1951d95..628457a31 100644
--- a/src/smt/listeners.cpp
+++ b/src/smt/listeners.cpp
@@ -15,14 +15,6 @@
 
 #include "smt/listeners.h"
 
-#include "base/configuration.h"
-#include "expr/attribute.h"
-#include "expr/node_manager_attributes.h"
-#include "options/smt_options.h"
-#include "printer/printer.h"
-#include "smt/dump.h"
-#include "smt/dump_manager.h"
-#include "smt/node_command.h"
 #include "smt/solver_engine.h"
 #include "smt/solver_engine_scope.h"
 
@@ -38,56 +30,5 @@ void ResourceOutListener::notify()
   d_slv.interrupt();
 }
 
-SmtNodeManagerListener::SmtNodeManagerListener(DumpManager& dm,
-                                               OutputManager& outMgr)
-    : d_dm(dm), d_outMgr(outMgr)
-{
-}
-
-void SmtNodeManagerListener::nmNotifyNewSort(TypeNode tn, uint32_t flags)
-{
-  DeclareTypeNodeCommand c(tn.getAttribute(expr::VarNameAttr()), 0, tn);
-  if ((flags & NodeManager::SORT_FLAG_PLACEHOLDER) == 0)
-  {
-    d_dm.addToDump(c);
-  }
-}
-
-void SmtNodeManagerListener::nmNotifyNewSortConstructor(TypeNode tn,
-                                                        uint32_t flags)
-{
-  DeclareTypeNodeCommand c(tn.getAttribute(expr::VarNameAttr()),
-                           tn.getAttribute(expr::SortArityAttr()),
-                           tn);
-  if ((flags & NodeManager::SORT_FLAG_PLACEHOLDER) == 0)
-  {
-    d_dm.addToDump(c);
-  }
-}
-
-void SmtNodeManagerListener::nmNotifyNewDatatypes(
-    const std::vector<TypeNode>& dtts, uint32_t flags)
-{
-  if ((flags & NodeManager::DATATYPE_FLAG_PLACEHOLDER) == 0)
-  {
-    if (Configuration::isAssertionBuild())
-    {
-      for (CVC5_UNUSED const TypeNode& dt : dtts)
-      {
-        Assert(dt.isDatatype());
-      }
-    }
-    DeclareDatatypeNodeCommand c(dtts);
-    d_dm.addToDump(c);
-  }
-}
-
-void SmtNodeManagerListener::nmNotifyNewVar(TNode n)
-{
-  DeclareFunctionNodeCommand c(
-      n.getAttribute(expr::VarNameAttr()), n, n.getType());
-  d_dm.addToDump(c);
-}
-
 }  // namespace smt
 }  // namespace cvc5
diff --git a/src/smt/listeners.h b/src/smt/listeners.h
index df99f8008..a20051bd7 100644
--- a/src/smt/listeners.h
+++ b/src/smt/listeners.h
@@ -43,34 +43,6 @@ class ResourceOutListener : public Listener
   SolverEngine& d_slv;
 };
 
-class DumpManager;
-
-/**
- * A listener for node manager calls, which impacts certain dumping traces.
- */
-class SmtNodeManagerListener : public NodeManagerListener
-{
- public:
-  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 */
-  void nmNotifyNewSortConstructor(TypeNode tn, uint32_t flags) override;
-  /** Notify when list of datatypes is created */
-  void nmNotifyNewDatatypes(const std::vector<TypeNode>& dtts,
-                            uint32_t flags) override;
-  /** Notify when new variable is created */
-  void nmNotifyNewVar(TNode n) override;
-  /** Notify when a term is deleted */
-  void nmNotifyDeleteNode(TNode n) override {}
-
- 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
 }  // namespace cvc5
 
diff --git a/src/smt/node_command.cpp b/src/smt/node_command.cpp
deleted file mode 100644
index 000107341..000000000
--- a/src/smt/node_command.cpp
+++ /dev/null
@@ -1,160 +0,0 @@
-/******************************************************************************
- * Top contributors (to current version):
- *   Abdalrhman Mohamed, Yoni Zohar, Andrew Reynolds
- *
- * This file is part of the cvc5 project.
- *
- * Copyright (c) 2009-2021 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.
- * ****************************************************************************
- *
- * Implementation of NodeCommand functions.
- */
-
-#include "smt/node_command.h"
-
-#include <sstream>
-
-#include "printer/printer.h"
-
-namespace cvc5 {
-
-/* -------------------------------------------------------------------------- */
-/* class NodeCommand                                                          */
-/* -------------------------------------------------------------------------- */
-
-NodeCommand::~NodeCommand() {}
-
-std::string NodeCommand::toString() const
-{
-  std::stringstream ss;
-  toStream(ss);
-  return ss.str();
-}
-
-std::ostream& operator<<(std::ostream& out, const NodeCommand& nc)
-{
-  nc.toStream(out,
-              Node::setdepth::getDepth(out),
-              Node::dag::getDag(out),
-              Node::setlanguage::getLanguage(out));
-  return out;
-}
-
-/* -------------------------------------------------------------------------- */
-/* class DeclareFunctionNodeCommand                                           */
-/* -------------------------------------------------------------------------- */
-
-DeclareFunctionNodeCommand::DeclareFunctionNodeCommand(const std::string& id,
-                                                       Node expr,
-                                                       TypeNode type)
-    : d_id(id),
-      d_fun(expr),
-      d_type(type)
-{
-}
-
-void DeclareFunctionNodeCommand::toStream(std::ostream& out,
-                                          int toDepth,
-                                          size_t dag,
-                                          Language language) const
-{
-  Printer::getPrinter(language)->toStreamCmdDeclareFunction(out, d_id, d_type);
-}
-
-NodeCommand* DeclareFunctionNodeCommand::clone() const
-{
-  return new DeclareFunctionNodeCommand(d_id, d_fun, d_type);
-}
-
-const Node& DeclareFunctionNodeCommand::getFunction() const { return d_fun; }
-
-/* -------------------------------------------------------------------------- */
-/* class DeclareTypeNodeCommand                                               */
-/* -------------------------------------------------------------------------- */
-
-DeclareTypeNodeCommand::DeclareTypeNodeCommand(const std::string& id,
-                                               size_t arity,
-                                               TypeNode type)
-    : d_id(id), d_arity(arity), d_type(type)
-{
-}
-
-void DeclareTypeNodeCommand::toStream(std::ostream& out,
-                                      int toDepth,
-                                      size_t dag,
-                                      Language language) const
-{
-  Printer::getPrinter(language)->toStreamCmdDeclareType(out, d_type);
-}
-
-NodeCommand* DeclareTypeNodeCommand::clone() const
-{
-  return new DeclareTypeNodeCommand(d_id, d_arity, d_type);
-}
-
-const std::string DeclareTypeNodeCommand::getSymbol() const { return d_id; }
-
-const TypeNode& DeclareTypeNodeCommand::getType() const { return d_type; }
-
-/* -------------------------------------------------------------------------- */
-/* class DeclareDatatypeNodeCommand                                           */
-/* -------------------------------------------------------------------------- */
-
-DeclareDatatypeNodeCommand::DeclareDatatypeNodeCommand(
-    const std::vector<TypeNode>& datatypes)
-    : d_datatypes(datatypes)
-{
-}
-
-void DeclareDatatypeNodeCommand::toStream(std::ostream& out,
-                                          int toDepth,
-                                          size_t dag,
-                                          Language language) const
-{
-  Printer::getPrinter(language)->toStreamCmdDatatypeDeclaration(out,
-                                                                d_datatypes);
-}
-
-NodeCommand* DeclareDatatypeNodeCommand::clone() const
-{
-  return new DeclareDatatypeNodeCommand(d_datatypes);
-}
-
-/* -------------------------------------------------------------------------- */
-/* class DefineFunctionNodeCommand                                            */
-/* -------------------------------------------------------------------------- */
-
-DefineFunctionNodeCommand::DefineFunctionNodeCommand(
-    const std::string& id,
-    Node fun,
-    const std::vector<Node>& formals,
-    Node formula)
-    : d_id(id), d_fun(fun), d_formals(formals), d_formula(formula)
-{
-}
-
-void DefineFunctionNodeCommand::toStream(std::ostream& out,
-                                         int toDepth,
-                                         size_t dag,
-                                         Language language) const
-{
-  TypeNode tn = d_fun.getType();
-  bool hasRange =
-      (tn.isFunction() || tn.isConstructor() || tn.isSelector());
-  Printer::getPrinter(language)->toStreamCmdDefineFunction(
-      out,
-      d_fun.toString(),
-      d_formals,
-      (hasRange ? d_fun.getType().getRangeType() : tn),
-      d_formula);
-}
-
-NodeCommand* DefineFunctionNodeCommand::clone() const
-{
-  return new DefineFunctionNodeCommand(d_id, d_fun, d_formals, d_formula);
-}
-
-}  // namespace cvc5
diff --git a/src/smt/node_command.h b/src/smt/node_command.h
deleted file mode 100644
index 3399cb6fb..000000000
--- a/src/smt/node_command.h
+++ /dev/null
@@ -1,141 +0,0 @@
-/******************************************************************************
- * Top contributors (to current version):
- *   Abdalrhman Mohamed
- *
- * This file is part of the cvc5 project.
- *
- * Copyright (c) 2009-2021 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.
- * ****************************************************************************
- *
- * Datastructures used for printing commands internally.
- */
-
-#include "cvc5_private.h"
-
-#ifndef CVC5__SMT__NODE_COMMAND_H
-#define CVC5__SMT__NODE_COMMAND_H
-
-#include <string>
-
-#include "expr/node.h"
-#include "expr/type_node.h"
-#include "options/language.h"
-
-namespace cvc5 {
-
-/**
- * A node version of Command. DO NOT use this version unless there is a need
- * to buffer commands for later use (e.g., printing models).
- */
-class NodeCommand
-{
- public:
-  /** Destructor */
-  virtual ~NodeCommand();
-
-  /** Print this NodeCommand to output stream */
-  virtual void toStream(std::ostream& out,
-                        int toDepth = -1,
-                        size_t dag = 1,
-                        Language language = Language::LANG_AUTO) const = 0;
-
-  /** Get a string representation of this NodeCommand */
-  std::string toString() const;
-
-  /** Clone this NodeCommand (make a shallow copy). */
-  virtual NodeCommand* clone() const = 0;
-};
-
-std::ostream& operator<<(std::ostream& out, const NodeCommand& nc);
-
-/**
- * Declare n-ary function symbol.
- * SMT-LIB: ( declare-fun <id> ( <type.getArgTypes()> ) <type.getRangeType()> )
- */
-class DeclareFunctionNodeCommand : public NodeCommand
-{
- public:
-  DeclareFunctionNodeCommand(const std::string& id, Node fun, TypeNode type);
-  void toStream(std::ostream& out,
-                int toDepth = -1,
-                size_t dag = 1,
-                Language language = Language::LANG_AUTO) const override;
-  NodeCommand* clone() const override;
-  const Node& getFunction() const;
-
- private:
-  std::string d_id;
-  Node d_fun;
-  TypeNode d_type;
-};
-
-/**
- * Create datatype sort.
- * SMT-LIB: ( declare-datatypes ( <datatype decls>{n+1} ) ( <datatypes>{n+1} ) )
- */
-class DeclareDatatypeNodeCommand : public NodeCommand
-{
- public:
-  DeclareDatatypeNodeCommand(const std::vector<TypeNode>& datatypes);
-  void toStream(std::ostream& out,
-                int toDepth = -1,
-                size_t dag = 1,
-                Language language = Language::LANG_AUTO) const override;
-  NodeCommand* clone() const override;
-
- private:
-  std::vector<TypeNode> d_datatypes;
-};
-
-/**
- * Declare uninterpreted sort.
- * SMT-LIB: ( declare-sort <id> <arity> )
- */
-class DeclareTypeNodeCommand : public NodeCommand
-{
- public:
-  DeclareTypeNodeCommand(const std::string& id, size_t arity, TypeNode type);
-  void toStream(std::ostream& out,
-                int toDepth = -1,
-                size_t dag = 1,
-                Language language = Language::LANG_AUTO) const override;
-  NodeCommand* clone() const override;
-  const std::string getSymbol() const;
-  const TypeNode& getType() const;
-
- private:
-  std::string d_id;
-  size_t d_arity;
-  TypeNode d_type;
-};
-
-/**
- * Define n-ary function.
- * SMT-LIB: ( define-fun <id> ( <formals> ) <fun.getType()> <formula> )
- */
-class DefineFunctionNodeCommand : public NodeCommand
-{
- public:
-  DefineFunctionNodeCommand(const std::string& id,
-                            Node fun,
-                            const std::vector<Node>& formals,
-                            Node formula);
-  void toStream(std::ostream& out,
-                int toDepth = -1,
-                size_t dag = 1,
-                Language language = Language::LANG_AUTO) const override;
-  NodeCommand* clone() const override;
-
- private:
-  std::string d_id;
-  Node d_fun;
-  std::vector<Node> d_formals;
-  Node d_formula;
-};
-
-}  // namespace cvc5
-
-#endif /* CVC5__SMT__NODE_COMMAND_H */
diff --git a/src/smt/output_manager.cpp b/src/smt/output_manager.cpp
deleted file mode 100644
index 0a363c08a..000000000
--- a/src/smt/output_manager.cpp
+++ /dev/null
@@ -1,32 +0,0 @@
-/******************************************************************************
- * Top contributors (to current version):
- *   Abdalrhman Mohamed, Andrew Reynolds
- *
- * This file is part of the cvc5 project.
- *
- * Copyright (c) 2009-2021 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.
- * ****************************************************************************
- *
- * Implementation of OutputManager functions.
- */
-
-#include "smt/output_manager.h"
-
-#include "options/base_options.h"
-#include "smt/solver_engine.h"
-
-namespace cvc5 {
-
-OutputManager::OutputManager(SolverEngine* slv) : d_slv(slv) {}
-
-const Printer& OutputManager::getPrinter() const { return d_slv->getPrinter(); }
-
-std::ostream& OutputManager::getDumpOut() const
-{
-  return *d_slv->getOptions().base.out;
-}
-
-}  // namespace cvc5
diff --git a/src/smt/output_manager.h b/src/smt/output_manager.h
deleted file mode 100644
index 34dcc41b4..000000000
--- a/src/smt/output_manager.h
+++ /dev/null
@@ -1,58 +0,0 @@
-/******************************************************************************
- * Top contributors (to current version):
- *   Abdalrhman Mohamed
- *
- * This file is part of the cvc5 project.
- *
- * Copyright (c) 2009-2021 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.
- * ****************************************************************************
- *
- * The output manager for the SolverEngine.
- *
- * The output manager provides helper functions for printing commands
- * internally.
- */
-
-#ifndef CVC5__SMT__OUTPUT_MANAGER_H
-#define CVC5__SMT__OUTPUT_MANAGER_H
-
-#include <ostream>
-
-namespace cvc5 {
-
-class Printer;
-class SolverEngine;
-
-/** This utility class provides helper functions for printing commands
- * internally */
-class OutputManager
-{
- public:
-  /** Constructor
-   *
-   * @param smt SMT engine to manage output for
-   */
-  explicit OutputManager(SolverEngine* 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:
-  SolverEngine* d_slv;
-};
-
-}  // namespace cvc5
-
-#endif  // CVC5__SMT__OUTPUT_MANAGER_H
diff --git a/src/smt/preprocessor.cpp b/src/smt/preprocessor.cpp
index 3aed58b30..1835e61db 100644
--- a/src/smt/preprocessor.cpp
+++ b/src/smt/preprocessor.cpp
@@ -22,7 +22,6 @@
 #include "printer/printer.h"
 #include "smt/abstract_values.h"
 #include "smt/assertions.h"
-#include "smt/dump.h"
 #include "smt/env.h"
 #include "smt/preprocess_proof_generator.h"
 #include "smt/solver_engine.h"
@@ -145,10 +144,6 @@ void Preprocessor::expandDefinitions(std::vector<Node>& ns)
 Node Preprocessor::simplify(const Node& node)
 {
   Trace("smt") << "SMT simplify(" << node << ")" << endl;
-  if (Dump.isOn("benchmark"))
-  {
-    d_env.getPrinter().toStreamCmdSimplify(d_env.getDumpOut(), node);
-  }
   Node ret = expandDefinitions(node);
   ret = rewrite(ret);
   return ret;
diff --git a/src/smt/preprocessor.h b/src/smt/preprocessor.h
index 40a84981a..957b5e36e 100644
--- a/src/smt/preprocessor.h
+++ b/src/smt/preprocessor.h
@@ -62,6 +62,8 @@ class Preprocessor : protected EnvObj
   /**
    * Process the assertions that have been asserted in argument as. Returns
    * true if no conflict was discovered while preprocessing them.
+   *
+   * @param as The assertions.
    */
   bool process(Assertions& as);
   /**
diff --git a/src/smt/print_benchmark.cpp b/src/smt/print_benchmark.cpp
index c1913e209..598cb9afc 100644
--- a/src/smt/print_benchmark.cpp
+++ b/src/smt/print_benchmark.cpp
@@ -159,6 +159,11 @@ void PrintBenchmark::printDeclaredFuns(std::ostream& out,
   for (const Node& f : funs)
   {
     Assert(f.isVar());
+    // do not print selectors, constructors
+    if (!f.getType().isFirstClass())
+    {
+      continue;
+    }
     if (alreadyPrinted.find(f) == alreadyPrinted.end())
     {
       d_printer->toStreamCmdDeclareFunction(out, f);
diff --git a/src/smt/process_assertions.cpp b/src/smt/process_assertions.cpp
index 47deddac3..468b754cc 100644
--- a/src/smt/process_assertions.cpp
+++ b/src/smt/process_assertions.cpp
@@ -27,11 +27,9 @@
 #include "options/strings_options.h"
 #include "options/uf_options.h"
 #include "preprocessing/assertion_pipeline.h"
-#include "preprocessing/preprocessing_pass.h"
 #include "preprocessing/preprocessing_pass_registry.h"
 #include "printer/printer.h"
 #include "smt/assertions.h"
-#include "smt/dump.h"
 #include "smt/expand_definitions.h"
 #include "smt/print_benchmark.h"
 #include "smt/solver_engine_stats.h"
@@ -98,7 +96,8 @@ bool ProcessAssertions::apply(Assertions& as)
   AssertionPipeline& assertions = as.getAssertionPipeline();
   Assert(d_preprocessingPassContext != nullptr);
   // Dump the assertions
-  dumpAssertions("pre-everything", as);
+  dumpAssertions("assertions::pre-everything", as);
+  Trace("assertions::pre-everything") << std::endl;
 
   Trace("smt-proc") << "ProcessAssertions::processAssertions() begin" << endl;
   Trace("smt") << "ProcessAssertions::processAssertions()" << endl;
@@ -114,7 +113,7 @@ bool ProcessAssertions::apply(Assertions& as)
 
   if (options().bv.bvGaussElim)
   {
-    d_passes["bv-gauss"]->apply(&assertions);
+    applyPass("bv-gauss", as);
   }
 
   // Add dummy assertion in last position - to be used as a
@@ -129,44 +128,42 @@ bool ProcessAssertions::apply(Assertions& as)
   Trace("smt-proc")
       << "ProcessAssertions::processAssertions() : pre-definition-expansion"
       << endl;
-  dumpAssertions("pre-definition-expansion", as);
   // Apply substitutions first. If we are non-incremental, this has only the
   // effect of replacing defined functions with their definitions.
   // We do not call theory-specific expand definitions here, since we want
   // to give the opportunity to rewrite/preprocess terms before expansion.
-  d_passes["apply-substs"]->apply(&assertions);
+  applyPass("apply-substs", as);
   Trace("smt-proc")
       << "ProcessAssertions::processAssertions() : post-definition-expansion"
       << endl;
-  dumpAssertions("post-definition-expansion", as);
 
   Debug("smt") << " assertions     : " << assertions.size() << endl;
 
   if (options().quantifiers.globalNegate)
   {
     // global negation of the formula
-    d_passes["global-negate"]->apply(&assertions);
+    applyPass("global-negate", as);
     as.flipGlobalNegated();
   }
 
   if (options().arith.nlExtPurify)
   {
-    d_passes["nl-ext-purify"]->apply(&assertions);
+    applyPass("nl-ext-purify", as);
   }
 
   if (options().smt.solveRealAsInt)
   {
-    d_passes["real-to-int"]->apply(&assertions);
+    applyPass("real-to-int", as);
   }
 
   if (options().smt.solveIntAsBV > 0)
   {
-    d_passes["int-to-bv"]->apply(&assertions);
+    applyPass("int-to-bv", as);
   }
 
   if (options().smt.ackermann)
   {
-    d_passes["ackermann"]->apply(&assertions);
+    applyPass("ackermann", as);
   }
 
   Debug("smt") << " assertions     : " << assertions.size() << endl;
@@ -175,92 +172,93 @@ bool ProcessAssertions::apply(Assertions& as)
 
   if (options().smt.extRewPrep)
   {
-    d_passes["ext-rew-pre"]->apply(&assertions);
+    applyPass("ext-rew-pre", as);
   }
 
   // Unconstrained simplification
   if (options().smt.unconstrainedSimp)
   {
-    d_passes["rewrite"]->apply(&assertions);
-    d_passes["unconstrained-simplifier"]->apply(&assertions);
+    applyPass("rewrite", as);
+    applyPass("unconstrained-simplifier", as);
   }
 
   if (options().bv.bvIntroducePow2)
   {
-    d_passes["bv-intro-pow2"]->apply(&assertions);
+    applyPass("bv-intro-pow2", as);
   }
 
   // Lift bit-vectors of size 1 to bool
   if (options().bv.bitvectorToBool)
   {
-    d_passes["bv-to-bool"]->apply(&assertions);
+    applyPass("bv-to-bool", as);
   }
   if (options().smt.solveBVAsInt != options::SolveBVAsIntMode::OFF)
   {
-    d_passes["bv-to-int"]->apply(&assertions);
+    applyPass("bv-to-int", as);
   }
   if (options().smt.foreignTheoryRewrite)
   {
-    d_passes["foreign-theory-rewrite"]->apply(&assertions);
+    applyPass("foreign-theory-rewrite", as);
   }
 
   // Since this pass is not robust for the information tracking necessary for
   // unsat cores, it's only applied if we are not doing unsat core computation
-  d_passes["apply-substs"]->apply(&assertions);
+  applyPass("apply-substs", as);
 
   // Assertions MUST BE guaranteed to be rewritten by this point
-  d_passes["rewrite"]->apply(&assertions);
+  applyPass("rewrite", as);
 
   // Convert non-top-level Booleans to bit-vectors of size 1
   if (options().bv.boolToBitvector != options::BoolToBVMode::OFF)
   {
-    d_passes["bool-to-bv"]->apply(&assertions);
+    applyPass("bool-to-bv", as);
   }
   if (options().sep.sepPreSkolemEmp)
   {
-    d_passes["sep-skolem-emp"]->apply(&assertions);
+    applyPass("sep-skolem-emp", as);
   }
 
   if (logicInfo().isQuantified())
   {
     // remove rewrite rules, apply pre-skolemization to existential quantifiers
-    d_passes["quantifiers-preprocess"]->apply(&assertions);
+    applyPass("quantifiers-preprocess", as);
 
     // fmf-fun : assume admissible functions, applying preprocessing reduction
     // to FMF
     if (options().quantifiers.fmfFunWellDefined)
     {
-      d_passes["fun-def-fmf"]->apply(&assertions);
+      applyPass("fun-def-fmf", as);
     }
   }
   if (!options().strings.stringLazyPreproc)
   {
-    d_passes["strings-eager-pp"]->apply(&assertions);
+    applyPass("strings-eager-pp", as);
   }
   if (options().smt.sortInference || options().uf.ufssFairnessMonotone)
   {
-    d_passes["sort-inference"]->apply(&assertions);
+    applyPass("sort-inference", as);
   }
 
   if (options().arith.pbRewrites)
   {
-    d_passes["pseudo-boolean-processor"]->apply(&assertions);
+    applyPass("pseudo-boolean-processor", as);
   }
 
   // rephrasing normal inputs as sygus problems
   if (options().quantifiers.sygusInference)
   {
-    d_passes["sygus-infer"]->apply(&assertions);
+    applyPass("sygus-infer", as);
   }
   else if (options().quantifiers.sygusRewSynthInput)
   {
     // do candidate rewrite rule synthesis
-    d_passes["synth-rr"]->apply(&assertions);
+    applyPass("synth-rr", as);
   }
 
   Trace("smt-proc") << "ProcessAssertions::processAssertions() : pre-simplify"
                     << endl;
-  dumpAssertions("pre-simplify", as);
+  dumpAssertions("assertions::pre-simplify", as);
+  Trace("assertions::pre-simplify") << std::endl;
   Chat() << "simplifying assertions..." << endl;
   noConflict = simplifyAssertions(as);
   if (!noConflict)
@@ -269,31 +267,33 @@ bool ProcessAssertions::apply(Assertions& as)
   }
   Trace("smt-proc") << "ProcessAssertions::processAssertions() : post-simplify"
                     << endl;
-  dumpAssertions("post-simplify", as);
+  dumpAssertions("assertions::post-simplify", as);
+  Trace("assertions::post-simplify") << std::endl;
 
   if (options().smt.doStaticLearning)
   {
-    d_passes["static-learning"]->apply(&assertions);
+    applyPass("static-learning", as);
   }
   Debug("smt") << " assertions     : " << assertions.size() << endl;
 
   if (options().smt.learnedRewrite)
   {
-    d_passes["learned-rewrite"]->apply(&assertions);
+    applyPass("learned-rewrite", as);
   }
 
   if (options().smt.earlyIteRemoval)
   {
     d_slvStats.d_numAssertionsPre += assertions.size();
-    d_passes["ite-removal"]->apply(&assertions);
+    applyPass("ite-removal", as);
     // This is needed because when solving incrementally, removeITEs may
     // introduce skolems that were solved for earlier and thus appear in the
     // substitution map.
-    d_passes["apply-substs"]->apply(&assertions);
+    applyPass("apply-substs", as);
     d_slvStats.d_numAssertionsPost += assertions.size();
   }
 
-  dumpAssertions("pre-repeat-simplify", as);
+  dumpAssertions("assertions::pre-repeat-simplify", as);
+  Trace("assertions::pre-repeat-simplify") << std::endl;
   if (options().smt.repeatSimp)
   {
     Trace("smt-proc")
@@ -306,11 +306,12 @@ bool ProcessAssertions::apply(Assertions& as)
         << "ProcessAssertions::processAssertions() : post-repeat-simplify"
         << endl;
   }
-  dumpAssertions("post-repeat-simplify", as);
+  dumpAssertions("assertions::post-repeat-simplify", as);
+  Trace("assertions::post-repeat-simplify") << std::endl;
 
   if (logicInfo().isHigherOrder())
   {
-    d_passes["ho-elim"]->apply(&assertions);
+    applyPass("ho-elim", as);
   }
   
   // begin: INVARIANT to maintain: no reordering of assertions or
@@ -323,21 +324,22 @@ bool ProcessAssertions::apply(Assertions& as)
   Debug("smt") << " assertions     : " << assertions.size() << endl;
 
   // ensure rewritten
-  d_passes["rewrite"]->apply(&assertions);
+  applyPass("rewrite", as);
   // rewrite equalities based on theory-specific rewriting
-  d_passes["theory-rewrite-eq"]->apply(&assertions);
+  applyPass("theory-rewrite-eq", as);
   // apply theory preprocess, which includes ITE removal
-  d_passes["theory-preprocess"]->apply(&assertions);
+  applyPass("theory-preprocess", as);
   // notice that we do not apply substitutions as a last step here, since
   // the range of substitutions is not theory-preprocessed.
 
   if (options().bv.bitblastMode == options::BitblastMode::EAGER)
   {
-    d_passes["bv-eager-atoms"]->apply(&assertions);
+    applyPass("bv-eager-atoms", as);
   }
 
   Trace("smt-proc") << "ProcessAssertions::apply() end" << endl;
-  dumpAssertions("post-everything", as);
+  dumpAssertions("assertions::post-everything", as);
+  Trace("assertions::post-everything") << std::endl;
 
   return noConflict;
 }
@@ -356,8 +358,7 @@ bool ProcessAssertions::simplifyAssertions(Assertions& as)
     if (options().smt.simplificationMode != options::SimplificationMode::NONE)
     {
       // Perform non-clausal simplification
-      PreprocessingPassResult res =
-          d_passes["non-clausal-simp"]->apply(&assertions);
+      PreprocessingPassResult res = applyPass("non-clausal-simp", as);
       if (res == PreprocessingPassResult::CONFLICT)
       {
         return false;
@@ -374,7 +375,7 @@ bool ProcessAssertions::simplifyAssertions(Assertions& as)
           // re-simplification, which we don't expect to be useful anyway)
           assertions.getRealAssertionsEnd() == assertions.size())
       {
-        d_passes["miplib-trick"]->apply(&assertions);
+        applyPass("miplib-trick", as);
       }
       else
       {
@@ -389,7 +390,7 @@ bool ProcessAssertions::simplifyAssertions(Assertions& as)
     if (options().smt.doITESimp
         && (d_simplifyAssertionsDepth <= 1 || options().smt.doITESimpOnRepeat))
     {
-      PreprocessingPassResult res = d_passes["ite-simp"]->apply(&assertions);
+      PreprocessingPassResult res = applyPass("ite-simp", as);
       if (res == PreprocessingPassResult::CONFLICT)
       {
         Chat() << "...ITE simplification found unsat..." << endl;
@@ -402,15 +403,14 @@ bool ProcessAssertions::simplifyAssertions(Assertions& as)
     // Unconstrained simplification
     if (options().smt.unconstrainedSimp)
     {
-      d_passes["unconstrained-simplifier"]->apply(&assertions);
+      applyPass("unconstrained-simplifier", as);
     }
 
     if (options().smt.repeatSimp
         && options().smt.simplificationMode
                != options::SimplificationMode::NONE)
     {
-      PreprocessingPassResult res =
-          d_passes["non-clausal-simp"]->apply(&assertions);
+      PreprocessingPassResult res = applyPass("non-clausal-simp", as);
       if (res == PreprocessingPassResult::CONFLICT)
       {
         return false;
@@ -435,18 +435,65 @@ bool ProcessAssertions::simplifyAssertions(Assertions& as)
   return true;
 }
 
-void ProcessAssertions::dumpAssertions(const char* key, Assertions& as)
+void ProcessAssertions::dumpAssertions(const std::string& key, Assertions& as)
 {
-  if (Dump.isOn("assertions") && Dump.isOn(string("assertions:") + key))
-  {
-    const AssertionPipeline& assertionList = as.getAssertionPipeline();
-    // Push the simplified assertions to the dump output stream
-    for (unsigned i = 0; i < assertionList.size(); ++i)
+  bool isTraceOn = Trace.isOn(key);
+  if (!isTraceOn)
+  {
+    return;
+  }
+  // Cannot print unless produce assertions is enabled. Otherwise, the printing
+  // is misleading, since it does not capture what symbols were provided
+  // as definitions.
+  if (!options().smt.produceAssertions)
+  {
+    Warning()
+        << "Assertions not available for dumping (use --produce-assertions)."
+        << std::endl;
+    return;
+  }
+  PrintBenchmark pb(&d_env.getPrinter());
+  std::vector<Node> assertions;
+  // Notice that the following list covers define-fun and define-fun-rec
+  // from input. The former does not impact the assertions since define-fun are
+  // added as top-level substitutions. The latter do get added to the list
+  // of assertions. Since we are interested in printing the result of
+  // preprocessed quantified formulas corresponding to recursive function
+  // definitions and not the original definitions, we discard the latter
+  // in the loop below.
+  //
+  // In summary, this means that define-fun-rec are expanded to
+  // (declare-fun ...) + (assert (forall ...)) in the printing below, whereas
+  // define-fun are preserved.
+  const context::CDList<Node>& asld = as.getAssertionListDefinitions();
+  std::vector<Node> defs;
+  for (const Node& d : asld)
+  {
+    if (d.getKind() != FORALL)
     {
-      TNode n = assertionList[i];
-      d_env.getPrinter().toStreamCmdAssert(d_env.getDumpOut(), n);
+      defs.push_back(d);
     }
   }
+  AssertionPipeline& ap = as.getAssertionPipeline();
+  for (size_t i = 0, size = ap.size(); i < size; i++)
+  {
+    assertions.push_back(ap[i]);
+  }
+  std::stringstream ss;
+  pb.printBenchmark(ss, logicInfo().getLogicString(), defs, assertions);
+  Trace(key) << ";;; " << key << " start" << std::endl;
+  Trace(key) << ss.str();
+  Trace(key) << ";;; " << key << " end " << std::endl;
+}
+
+PreprocessingPassResult ProcessAssertions::applyPass(const std::string& pname,
+                                                     Assertions& as)
+{
+  dumpAssertions("assertions::pre-" + pname, as);
+  AssertionPipeline& assertions = as.getAssertionPipeline();
+  PreprocessingPassResult res = d_passes[pname]->apply(&assertions);
+  dumpAssertions("assertions::post-" + pname, as);
+  return res;
 }
 
 }  // namespace smt
diff --git a/src/smt/process_assertions.h b/src/smt/process_assertions.h
index 84c5d1d43..81ea9f475 100644
--- a/src/smt/process_assertions.h
+++ b/src/smt/process_assertions.h
@@ -22,6 +22,7 @@
 
 #include "context/cdlist.h"
 #include "expr/node.h"
+#include "preprocessing/preprocessing_pass.h"
 #include "smt/env_obj.h"
 #include "util/resource_manager.h"
 
@@ -29,8 +30,6 @@ namespace cvc5 {
 
 namespace preprocessing {
 class AssertionPipeline;
-class PreprocessingPass;
-class PreprocessingPassContext;
 }
 
 namespace smt {
@@ -111,7 +110,10 @@ class ProcessAssertions : protected EnvObj
    * Dump assertions. Print the current assertion list to the dump
    * assertions:`key` if it is enabled.
    */
-  void dumpAssertions(const char* key, Assertions& as);
+  void dumpAssertions(const std::string& key, Assertions& as);
+  /** apply pass */
+  preprocessing::PreprocessingPassResult applyPass(const std::string& pass,
+                                                   Assertions& as);
 };
 
 }  // namespace smt
diff --git a/src/smt/solver_engine.cpp b/src/smt/solver_engine.cpp
index fddea7649..264e1ec0b 100644
--- a/src/smt/solver_engine.cpp
+++ b/src/smt/solver_engine.cpp
@@ -40,15 +40,12 @@
 #include "smt/abstract_values.h"
 #include "smt/assertions.h"
 #include "smt/check_models.h"
-#include "smt/dump.h"
-#include "smt/dump_manager.h"
 #include "smt/env.h"
 #include "smt/interpolation_solver.h"
 #include "smt/listeners.h"
 #include "smt/logic_exception.h"
 #include "smt/model_blocker.h"
 #include "smt/model_core_builder.h"
-#include "smt/node_command.h"
 #include "smt/preprocessor.h"
 #include "smt/proof_manager.h"
 #include "smt/quant_elim_solver.h"
@@ -90,7 +87,6 @@ SolverEngine::SolverEngine(NodeManager* nm, const Options* optr)
       d_absValues(new AbstractValues(getNodeManager())),
       d_asserts(new Assertions(*d_env.get(), *d_absValues.get())),
       d_routListener(new ResourceOutListener(*this)),
-      d_snmListener(new SmtNodeManagerListener(*getDumpManager(), d_outMgr)),
       d_smtSolver(nullptr),
       d_checkModels(nullptr),
       d_pfManager(nullptr),
@@ -101,7 +97,6 @@ SolverEngine::SolverEngine(NodeManager* nm, const Options* optr)
       d_quantElimSolver(nullptr),
       d_isInternalSubsolver(false),
       d_stats(nullptr),
-      d_outMgr(this),
       d_scope(nullptr)
 {
   // !!!!!!!!!!!!!!!!!!!!!! temporary hack: this makes the current SolverEngine
@@ -116,8 +111,6 @@ SolverEngine::SolverEngine(NodeManager* nm, const Options* optr)
   // hand, this hack breaks use cases where multiple SolverEngine objects are
   // created by the user.
   d_scope.reset(new SolverEngineScope(this));
-  // listen to node manager events
-  getNodeManager()->subscribeEvents(d_snmListener.get());
   // listen to resource out
   getResourceManager()->registerListener(d_routListener.get());
   // make statistics
@@ -224,25 +217,6 @@ void SolverEngine::finishInit()
   Trace("smt-debug") << "Set up assertions..." << std::endl;
   d_asserts->finishInit();
 
-  // dump out a set-logic command only when raw-benchmark is disabled to avoid
-  // dumping the command twice.
-  if (Dump.isOn("benchmark"))
-  {
-    LogicInfo everything;
-    everything.lock();
-    getPrinter().toStreamCmdSetInfo(
-        d_env->getDumpOut(),
-        "notes",
-        "cvc5 always dumps the most general, all-supported logic (below), as "
-        "some internals might require the use of a logic more general than "
-        "the input.");
-    getPrinter().toStreamCmdSetBenchmarkLogic(d_env->getDumpOut(),
-                                              everything.getLogicString());
-  }
-
-  // initialize the dump manager
-  getDumpManager()->finishInit();
-
   // subsolvers
   if (d_env->getOptions().smt.produceAbducts)
   {
@@ -302,8 +276,6 @@ SolverEngine::~SolverEngine()
     d_smtSolver.reset(nullptr);
 
     d_stats.reset(nullptr);
-    getNodeManager()->unsubscribeEvents(d_snmListener.get());
-    d_snmListener.reset(nullptr);
     d_routListener.reset(nullptr);
     // destroy the state
     d_state.reset(nullptr);
@@ -374,11 +346,6 @@ void SolverEngine::setInfo(const std::string& key, const std::string& value)
 
   Trace("smt") << "SMT setInfo(" << key << ", " << value << ")" << endl;
 
-  if (Dump.isOn("benchmark"))
-  {
-    getPrinter().toStreamCmdSetInfo(d_env->getDumpOut(), key, value);
-  }
-
   if (key == "filename")
   {
     d_env->d_options.driver.filename = value;
@@ -572,14 +539,6 @@ void SolverEngine::defineFunction(Node func,
   Trace("smt") << "SMT defineFunction(" << func << ")" << endl;
   debugCheckFormals(formals, func);
 
-  stringstream ss;
-  ss << language::SetLanguage(
-      language::SetLanguage::getLanguage(Dump.getStream()))
-     << func;
-
-  DefineFunctionNodeCommand nc(ss.str(), func, formals, formula);
-  getDumpManager()->addToDump(nc, "declarations");
-
   // type check body
   debugCheckFunctionBody(formula, formals, func);
 
@@ -786,10 +745,6 @@ Result SolverEngine::checkSat()
 
 Result SolverEngine::checkSat(const Node& assumption)
 {
-  if (Dump.isOn("benchmark"))
-  {
-    getPrinter().toStreamCmdCheckSatAssuming(d_env->getDumpOut(), {assumption});
-  }
   std::vector<Node> assump;
   if (!assumption.isNull())
   {
@@ -800,27 +755,11 @@ Result SolverEngine::checkSat(const Node& assumption)
 
 Result SolverEngine::checkSat(const std::vector<Node>& assumptions)
 {
-  if (Dump.isOn("benchmark"))
-  {
-    if (assumptions.empty())
-    {
-      getPrinter().toStreamCmdCheckSat(d_env->getDumpOut());
-    }
-    else
-    {
-      getPrinter().toStreamCmdCheckSatAssuming(d_env->getDumpOut(),
-                                               assumptions);
-    }
-  }
   return checkSatInternal(assumptions, false);
 }
 
 Result SolverEngine::checkEntailed(const Node& node)
 {
-  if (Dump.isOn("benchmark"))
-  {
-    getPrinter().toStreamCmdQuery(d_env->getDumpOut(), node);
-  }
   return checkSatInternal(
              node.isNull() ? std::vector<Node>() : std::vector<Node>{node},
              true)
@@ -929,10 +868,6 @@ std::vector<Node> SolverEngine::getUnsatAssumptions(void)
         "UNSAT/ENTAILED.");
   }
   finishInit();
-  if (Dump.isOn("benchmark"))
-  {
-    getPrinter().toStreamCmdGetUnsatAssumptions(d_env->getDumpOut());
-  }
   UnsatCore core = getUnsatCoreInternal();
   std::vector<Node> res;
   std::vector<Node>& assumps = d_asserts->getAssumptions();
@@ -1056,10 +991,6 @@ Node SolverEngine::getValue(const Node& ex) const
   SolverEngineScope smts(this);
 
   Trace("smt") << "SMT getValue(" << ex << ")" << endl;
-  if (Dump.isOn("benchmark"))
-  {
-    getPrinter().toStreamCmdGetValue(d_env->getDumpOut(), {ex});
-  }
   TypeNode expectedType = ex.getType();
 
   // Substitute out any abstract values in ex and expand
@@ -1202,11 +1133,6 @@ Result SolverEngine::blockModel()
 
   finishInit();
 
-  if (Dump.isOn("benchmark"))
-  {
-    getPrinter().toStreamCmdBlockModel(d_env->getDumpOut());
-  }
-
   TheoryModel* m = getAvailableModel("block model");
 
   if (d_env->getOptions().smt.blockModelsMode == options::BlockModelsMode::NONE)
@@ -1232,11 +1158,6 @@ Result SolverEngine::blockModelValues(const std::vector<Node>& exprs)
 
   finishInit();
 
-  if (Dump.isOn("benchmark"))
-  {
-    getPrinter().toStreamCmdBlockModelValues(d_env->getDumpOut(), exprs);
-  }
-
   TheoryModel* m = getAvailableModel("block model values");
 
   // get expanded assertions
@@ -1538,10 +1459,6 @@ UnsatCore SolverEngine::getUnsatCore()
   Trace("smt") << "SMT getUnsatCore()" << std::endl;
   SolverEngineScope smts(this);
   finishInit();
-  if (Dump.isOn("benchmark"))
-  {
-    getPrinter().toStreamCmdGetUnsatCore(d_env->getDumpOut());
-  }
   return getUnsatCoreInternal();
 }
 
@@ -1563,10 +1480,6 @@ std::string SolverEngine::getProof()
   Trace("smt") << "SMT getProof()\n";
   SolverEngineScope smts(this);
   finishInit();
-  if (Dump.isOn("benchmark"))
-  {
-    getPrinter().toStreamCmdGetProof(d_env->getDumpOut());
-  }
   if (!d_env->getOptions().smt.produceProofs)
   {
     throw ModalException("Cannot get a proof when proof option is off.");
@@ -1775,10 +1688,6 @@ std::vector<Node> SolverEngine::getAssertions()
   SolverEngineScope smts(this);
   finishInit();
   d_state->doPendingPops();
-  if (Dump.isOn("benchmark"))
-  {
-    getPrinter().toStreamCmdGetAssertions(d_env->getDumpOut());
-  }
   Trace("smt") << "SMT getAssertions()" << endl;
   if (!d_env->getOptions().smt.produceAssertions)
   {
@@ -1795,10 +1704,6 @@ void SolverEngine::getDifficultyMap(std::map<Node, Node>& dmap)
   Trace("smt") << "SMT getDifficultyMap()\n";
   SolverEngineScope smts(this);
   finishInit();
-  if (Dump.isOn("benchmark"))
-  {
-    getPrinter().toStreamCmdGetDifficulty(d_env->getDumpOut());
-  }
   if (!d_env->getOptions().smt.produceDifficulty)
   {
     throw ModalException(
@@ -1820,10 +1725,6 @@ void SolverEngine::push()
   d_state->doPendingPops();
   Trace("smt") << "SMT push()" << endl;
   d_smtSolver->processAssertions(*d_asserts);
-  if (Dump.isOn("benchmark"))
-  {
-    getPrinter().toStreamCmdPush(d_env->getDumpOut());
-  }
   d_state->userPush();
 }
 
@@ -1832,10 +1733,6 @@ void SolverEngine::pop()
   SolverEngineScope smts(this);
   finishInit();
   Trace("smt") << "SMT pop()" << endl;
-  if (Dump.isOn("benchmark"))
-  {
-    getPrinter().toStreamCmdPop(d_env->getDumpOut());
-  }
   d_state->userPop();
 
   // Clear out assertion queues etc., in case anything is still in there
@@ -1859,19 +1756,13 @@ void SolverEngine::resetAssertions()
     // (see solver execution modes in the SMT-LIB standard)
     Assert(getContext()->getLevel() == 0);
     Assert(getUserContext()->getLevel() == 0);
-    getDumpManager()->resetAssertions();
     return;
   }
 
   Trace("smt") << "SMT resetAssertions()" << endl;
-  if (Dump.isOn("benchmark"))
-  {
-    getPrinter().toStreamCmdResetAssertions(d_env->getDumpOut());
-  }
 
   d_asserts->clearCurrent();
   d_state->notifyResetAssertions();
-  getDumpManager()->resetAssertions();
   // push the state to maintain global context around everything
   d_state->setup();
 
@@ -1939,11 +1830,6 @@ void SolverEngine::setOption(const std::string& key, const std::string& value)
 {
   Trace("smt") << "SMT setOption(" << key << ", " << value << ")" << endl;
 
-  if (Dump.isOn("benchmark"))
-  {
-    getPrinter().toStreamCmdSetOption(d_env->getDumpOut(), key, value);
-  }
-
   if (key == "command-verbosity")
   {
     size_t fstIndex = value.find(" ");
@@ -1999,11 +1885,6 @@ std::string SolverEngine::getOption(const std::string& key) const
     return "2";
   }
 
-  if (Dump.isOn("benchmark"))
-  {
-    getPrinter().toStreamCmdGetOption(d_env->getDumpOut(), key);
-  }
-
   if (key == "command-verbosity")
   {
     vector<Node> result;
@@ -2047,12 +1928,8 @@ ResourceManager* SolverEngine::getResourceManager() const
   return d_env->getResourceManager();
 }
 
-DumpManager* SolverEngine::getDumpManager() { return d_env->getDumpManager(); }
-
 const Printer& SolverEngine::getPrinter() const { return d_env->getPrinter(); }
 
-OutputManager& SolverEngine::getOutputManager() { return d_outMgr; }
-
 theory::Rewriter* SolverEngine::getRewriter() { return d_env->getRewriter(); }
 
 }  // namespace cvc5
diff --git a/src/smt/solver_engine.h b/src/smt/solver_engine.h
index 75e653656..7096aec92 100644
--- a/src/smt/solver_engine.h
+++ b/src/smt/solver_engine.h
@@ -15,8 +15,8 @@
 
 #include "cvc5_public.h"
 
-#ifndef CVC5__SOLVER_ENGINE_H
-#define CVC5__SOLVER_ENGINE_H
+#ifndef CVC5__SMT__SOLVER_ENGINE_H
+#define CVC5__SMT__SOLVER_ENGINE_H
 
 #include <map>
 #include <memory>
@@ -26,7 +26,6 @@
 #include "context/cdhashmap_forward.h"
 #include "cvc5_export.h"
 #include "options/options.h"
-#include "smt/output_manager.h"
 #include "smt/smt_mode.h"
 #include "theory/logic_info.h"
 #include "util/result.h"
@@ -80,7 +79,6 @@ namespace smt {
 class SolverEngineState;
 class AbstractValues;
 class Assertions;
-class DumpManager;
 class ResourceOutListener;
 class SmtNodeManagerListener;
 class OptionsManager;
@@ -847,15 +845,9 @@ class CVC5_EXPORT SolverEngine
   /** Get the resource manager of this SMT engine */
   ResourceManager* getResourceManager() const;
 
-  /** 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 SolverEngine. */
   theory::Rewriter* getRewriter();
   /**
@@ -1055,8 +1047,6 @@ class CVC5_EXPORT SolverEngine
   std::unique_ptr<smt::Assertions> d_asserts;
   /** Resource out listener */
   std::unique_ptr<smt::ResourceOutListener> d_routListener;
-  /** Node manager listener */
-  std::unique_ptr<smt::SmtNodeManagerListener> d_snmListener;
 
   /** The SMT solver */
   std::unique_ptr<smt::SmtSolver> d_smtSolver;
@@ -1104,8 +1094,6 @@ class CVC5_EXPORT SolverEngine
   /** The statistics class */
   std::unique_ptr<smt::SolverEngineStatistics> d_stats;
 
-  /** the output manager for commands */
-  mutable OutputManager d_outMgr;
   /**
    * The global scope object. Upon creation of this SolverEngine, it becomes the
    * SolverEngine in scope. It says the SolverEngine in scope until it is
diff --git a/src/theory/bv/theory_bv_rewrite_rules.h b/src/theory/bv/theory_bv_rewrite_rules.h
index 613942d19..208f0ebd3 100644
--- a/src/theory/bv/theory_bv_rewrite_rules.h
+++ b/src/theory/bv/theory_bv_rewrite_rules.h
@@ -24,7 +24,6 @@
 
 #include "context/context.h"
 #include "printer/printer.h"
-#include "smt/dump.h"
 #include "smt/solver_engine.h"
 #include "smt/solver_engine_scope.h"
 #include "theory/bv/theory_bv_utils.h"
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 5aafae367..53365e1b6 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -30,10 +30,8 @@
 #include "proof/proof_checker.h"
 #include "proof/proof_ensure_closed.h"
 #include "prop/prop_engine.h"
-#include "smt/dump.h"
 #include "smt/env.h"
 #include "smt/logic_exception.h"
-#include "smt/output_manager.h"
 #include "theory/combination_care_graph.h"
 #include "theory/decision_manager.h"
 #include "theory/quantifiers/first_order_model.h"
@@ -349,54 +347,6 @@ void TheoryEngine::printAssertions(const char* tag) {
   }
 }
 
-void TheoryEngine::dumpAssertions(const char* tag) {
-  if (Dump.isOn(tag)) {
-    const Printer& printer = d_env.getPrinter();
-    std::ostream& out = d_env.getDumpOut();
-    printer.toStreamCmdSetInfo(out, "notes", "Starting completeness check");
-    for (TheoryId theoryId = THEORY_FIRST; theoryId < THEORY_LAST; ++theoryId) {
-      Theory* theory = d_theoryTable[theoryId];
-      if (theory && d_logicInfo.isTheoryEnabled(theoryId)) {
-        printer.toStreamCmdSetInfo(out, "notes", "Completeness check");
-        printer.toStreamCmdPush(out);
-
-        // Dump the shared terms
-        if (d_logicInfo.isSharingEnabled()) {
-          printer.toStreamCmdSetInfo(out, "notes", "Shared terms");
-          context::CDList<TNode>::const_iterator it = theory->shared_terms_begin(), it_end = theory->shared_terms_end();
-          for (unsigned i = 0; it != it_end; ++ it, ++i) {
-              stringstream ss;
-              ss << (*it);
-              printer.toStreamCmdSetInfo(out, "notes", ss.str());
-          }
-        }
-
-        // Dump the assertions
-        printer.toStreamCmdSetInfo(out, "notes", "Assertions");
-        context::CDList<Assertion>::const_iterator it = theory->facts_begin(), it_end = theory->facts_end();
-        for (; it != it_end; ++ it) {
-          // Get the assertion
-          Node assertionNode = (*it).d_assertion;
-          // Purify all the terms
-
-          if ((*it).d_isPreregistered)
-          {
-            printer.toStreamCmdSetInfo(out, "notes", "Preregistered");
-          }
-          else
-          {
-            printer.toStreamCmdSetInfo(out, "notes", "Shared assertion");
-          }
-          printer.toStreamCmdAssert(out, assertionNode);
-        }
-        printer.toStreamCmdCheckSat(out);
-
-        printer.toStreamCmdPop(out);
-      }
-    }
-  }
-}
-
 /**
  * Check all (currently-active) theories for conflicts.
  * @param effort the effort level to use
@@ -544,12 +494,6 @@ void TheoryEngine::check(Theory::Effort effort) {
   } catch(const theory::Interrupted&) {
     Trace("theory") << "TheoryEngine::check() => interrupted" << endl;
   }
-  // If fulleffort, check all theories
-  if(Dump.isOn("theory::fullcheck") && Theory::fullEffort(effort)) {
-    if (!d_inConflict && !needCheck()) {
-      dumpAssertions("theory::fullcheck");
-    }
-  }
 }
 
 void TheoryEngine::propagate(Theory::Effort effort)
@@ -1351,15 +1295,6 @@ void TheoryEngine::lemma(TrustNode tlemma,
     tlemma.debugCheckClosed("te-proof-debug", "TheoryEngine::lemma_initial");
   }
 
-  if(Dump.isOn("t-lemmas")) {
-    // we dump the negation of the lemma, to show validity of the lemma
-    Node n = lemma.negate();
-    const Printer& printer = d_env.getPrinter();
-    std::ostream& out = d_env.getDumpOut();
-    printer.toStreamCmdSetInfo(out, "notes", "theory lemma: expect valid");
-    printer.toStreamCmdCheckSatAssuming(out, {n});
-  }
-
   // assert the lemma
   d_propEngine->assertLemma(tlemma, p);
 
@@ -1412,13 +1347,6 @@ void TheoryEngine::conflict(TrustNode tconflict, TheoryId theoryId)
   // Mark that we are in conflict
   markInConflict();
 
-  if(Dump.isOn("t-conflicts")) {
-    const Printer& printer = d_env.getPrinter();
-    std::ostream& out = d_env.getDumpOut();
-    printer.toStreamCmdSetInfo(out, "notes", "theory conflict: expect unsat");
-    printer.toStreamCmdCheckSatAssuming(out, {conflict});
-  }
-
   // In the multiple-theories case, we need to reconstruct the conflict
   if (d_logicInfo.isSharingEnabled()) {
     // Create the workplace for explanations
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 0a9b67979..efde513a9 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -499,9 +499,6 @@ class TheoryEngine : protected EnvObj
   void ensureLemmaAtoms(const std::vector<TNode>& atoms,
                         theory::TheoryId atomsTo);
 
-  /** Dump the assertions to the dump */
-  void dumpAssertions(const char* tag);
-
   /** Associated PropEngine engine */
   prop::PropEngine* d_propEngine;