Split dump manager from SmtEngine (#4824)

Towards splitting SmtEngine.

This moves utilities related to managing information for dumping to its own utility, DumpManager.

Its current responsibilities are to track information about how to print a model, and the implementation of some dumping traces, although its responsibilities should be extended further so that SmtEngine is not responsible for any command dumping. This is future work.

11 files changed, 288 insertions, 214 deletions

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 53d049411..61261afe4 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -225,11 +225,11 @@ libcvc4_add_sources(
   smt/abstract_values.h
   smt/command.cpp
   smt/command.h
-  smt/command_list.cpp
-  smt/command_list.h
   smt/defined_function.h
   smt/dump.cpp
   smt/dump.h
+  smt/dump_manager.cpp
+  smt/dump_manager.h
   smt/listeners.cpp
   smt/listeners.h
   smt/logic_exception.h
diff --git a/src/preprocessing/passes/sort_infer.cpp b/src/preprocessing/passes/sort_infer.cpp
index 92c2e55b1..03f0469bf 100644
--- a/src/preprocessing/passes/sort_infer.cpp
+++ b/src/preprocessing/passes/sort_infer.cpp
@@ -16,6 +16,7 @@
 
 #include "options/smt_options.h"
 #include "options/uf_options.h"
+#include "smt/dump_manager.h"
 #include "theory/rewriter.h"
 #include "theory/sort_inference.h"
 
@@ -65,12 +66,12 @@ PreprocessingPassResult SortInferencePass::applyInternal(
       assertionsToPreprocess->push_back(nar);
     }
     // indicate correspondence between the functions
-    // TODO (#2308): move this to a better place
     SmtEngine* smt = smt::currentSmtEngine();
+    smt::DumpManager* dm = smt->getDumpManager();
     for (const std::pair<const Node, Node>& mrf : model_replace_f)
     {
-      smt->setPrintFuncInModel(mrf.first.toExpr(), false);
-      smt->setPrintFuncInModel(mrf.second.toExpr(), true);
+      dm->setPrintFuncInModel(mrf.first, false);
+      dm->setPrintFuncInModel(mrf.second, true);
     }
   }
   // only need to compute monotonicity on the resulting formula if we are
diff --git a/src/smt/command_list.cpp b/src/smt/command_list.cpp
deleted file mode 100644
index a88efbbec..000000000
--- a/src/smt/command_list.cpp
+++ /dev/null
@@ -1,30 +0,0 @@
-/*********************                                                        */
-/*! \file command_list.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Morgan Deters
- ** 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 A context-sensitive list of Commands, and their cleanup
- **
- ** A context-sensitive list of Commands, and their cleanup.
- **/
-
-// we include both of these to make sure they agree on the typedef
-#include "smt/command.h"
-#include "smt/command_list.h"
-#include "smt/smt_engine.h"
-
-namespace CVC4 {
-namespace smt {
-
-void CommandCleanup::operator()(Command** c) {
-  delete *c;
-}
-
-}/* CVC4::smt namespace */
-}/* CVC4 namespace */
diff --git a/src/smt/command_list.h b/src/smt/command_list.h
deleted file mode 100644
index cdc8e4c22..000000000
--- a/src/smt/command_list.h
+++ /dev/null
@@ -1,39 +0,0 @@
-/*********************                                                        */
-/*! \file command_list.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Morgan Deters, Mathias Preiner
- ** 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 A context-sensitive list of Commands, and their cleanup
- **
- ** A context-sensitive list of Commands, and their cleanup.
- **/
-
-#include "cvc4_private.h"
-
-#ifndef CVC4__SMT__COMMAND_LIST_H
-#define CVC4__SMT__COMMAND_LIST_H
-
-#include "context/cdlist.h"
-
-namespace CVC4 {
-
-class Command;
-
-namespace smt {
-
-struct CommandCleanup {
-  void operator()(Command** c);
-};/* struct CommandCleanup */
-
-typedef context::CDList<Command*, CommandCleanup> CommandList;
-
-}/* CVC4::smt namespace */
-}/* CVC4 namespace */
-
-#endif /* CVC4__SMT__COMMAND_LIST_H */
diff --git a/src/smt/dump_manager.cpp b/src/smt/dump_manager.cpp
new file mode 100644
index 000000000..b8525f24e
--- /dev/null
+++ b/src/smt/dump_manager.cpp
@@ -0,0 +1,140 @@
+/*********************                                                        */
+/*! \file dump_manager.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** 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 the dump manager.
+ **/
+
+#include "smt/dump_manager.h"
+
+#include "expr/expr_manager.h"
+#include "options/smt_options.h"
+#include "smt/dump.h"
+
+namespace CVC4 {
+namespace smt {
+
+DumpManager::DumpManager(context::UserContext* u)
+    : d_modelGlobalCommands(), d_modelCommands(u), d_dumpCommands()
+{
+}
+
+DumpManager::~DumpManager()
+{
+  d_dumpCommands.clear();
+  d_modelCommandsAlloc.clear();
+  d_modelGlobalCommands.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() { d_modelGlobalCommands.clear(); }
+
+void DumpManager::addToModelCommandAndDump(const Command& c,
+                                           uint32_t flags,
+                                           bool userVisible,
+                                           const char* dumpTag)
+{
+  Trace("smt") << "SMT addToModelCommandAndDump(" << c << ")" << std::endl;
+  // If we aren't yet fully inited, the user might still turn on
+  // produce-models.  So let's keep any commands around just in
+  // case.  This is useful in two cases: (1) SMT-LIBv1 auto-declares
+  // sort "U" in QF_UF before setLogic() is run and we still want to
+  // support finding card(U) with --finite-model-find, and (2) to
+  // decouple SmtEngine and ExprManager if the user does a few
+  // ExprManager::mkSort() before SmtEngine::setOption("produce-models")
+  // and expects to find their cardinalities in the model.
+  if ((!d_fullyInited || options::produceModels())
+      && (flags & ExprManager::VAR_FLAG_DEFINED) == 0)
+  {
+    if (flags & ExprManager::VAR_FLAG_GLOBAL)
+    {
+      d_modelGlobalCommands.push_back(std::unique_ptr<Command>(c.clone()));
+    }
+    else
+    {
+      Command* cc = c.clone();
+      d_modelCommands.push_back(cc);
+      // also remember for memory management purposes
+      d_modelCommandsAlloc.push_back(std::unique_ptr<Command>(cc));
+    }
+  }
+  if (Dump.isOn(dumpTag))
+  {
+    if (d_fullyInited)
+    {
+      Dump(dumpTag) << c;
+    }
+    else
+    {
+      d_dumpCommands.push_back(std::unique_ptr<Command>(c.clone()));
+    }
+  }
+}
+
+void DumpManager::setPrintFuncInModel(Node f, bool p)
+{
+  Trace("setp-model") << "Set printInModel " << f << " to " << p << std::endl;
+  for (std::unique_ptr<Command>& c : d_modelGlobalCommands)
+  {
+    DeclareFunctionCommand* dfc =
+        dynamic_cast<DeclareFunctionCommand*>(c.get());
+    if (dfc != NULL)
+    {
+      Node df = Node::fromExpr(dfc->getFunction());
+      if (df == f)
+      {
+        dfc->setPrintInModel(p);
+      }
+    }
+  }
+  for (Command* c : d_modelCommands)
+  {
+    DeclareFunctionCommand* dfc = dynamic_cast<DeclareFunctionCommand*>(c);
+    if (dfc != NULL)
+    {
+      Node df = Node::fromExpr(dfc->getFunction());
+      if (df == f)
+      {
+        dfc->setPrintInModel(p);
+      }
+    }
+  }
+}
+
+size_t DumpManager::getNumModelCommands() const
+{
+  return d_modelCommands.size() + d_modelGlobalCommands.size();
+}
+
+const Command* DumpManager::getModelCommand(size_t i) const
+{
+  Assert(i < getNumModelCommands());
+  // index the global commands first, then the locals
+  if (i < d_modelGlobalCommands.size())
+  {
+    return d_modelGlobalCommands[i].get();
+  }
+  return d_modelCommands[i - d_modelGlobalCommands.size()];
+}
+
+}  // namespace smt
+}  // namespace CVC4
diff --git a/src/smt/dump_manager.h b/src/smt/dump_manager.h
new file mode 100644
index 000000000..6f2ee37a1
--- /dev/null
+++ b/src/smt/dump_manager.h
@@ -0,0 +1,106 @@
+/*********************                                                        */
+/*! \file dump_manager.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** 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 dump manager of the SmtEngine.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__SMT__DUMP_MANAGER_H
+#define CVC4__SMT__DUMP_MANAGER_H
+
+#include <memory>
+#include <vector>
+
+#include "context/cdlist.h"
+#include "expr/node.h"
+#include "smt/command.h"
+
+namespace CVC4 {
+namespace smt {
+
+/**
+ * This utility is responsible for:
+ * (1) storing information required for SMT-LIB queries such as get-model,
+ * which requires knowing what symbols are declared and should be printed in
+ * the model.
+ * (2) implementing some dumping traces e.g. --dump=declarations.
+ */
+class DumpManager
+{
+  typedef context::CDList<Command*> CommandList;
+
+ public:
+  DumpManager(context::UserContext* u);
+  ~DumpManager();
+  /**
+   * Finish init, called during SmtEngine::finishInit, which is triggered
+   * when initialization of options is finished.
+   */
+  void finishInit();
+  /**
+   * Reset assertions, called on SmtEngine::resetAssertions.
+   */
+  void resetAssertions();
+  /**
+   * Add to Model command.  This is used for recording a command
+   * that should be reported during a get-model call.
+   */
+  void addToModelCommandAndDump(const Command& c,
+                                uint32_t flags = 0,
+                                bool userVisible = true,
+                                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);
+  /** get number of commands to report in a model */
+  size_t getNumModelCommands() const;
+  /** get model command at index i */
+  const Command* getModelCommand(size_t i) const;
+
+ private:
+  /** Fully inited */
+  bool d_fullyInited;
+
+  /**
+   * A list of commands that should be in the Model globally (i.e.,
+   * regardless of push/pop).  Only maintained if produce-models option
+   * is on.
+   */
+  std::vector<std::unique_ptr<Command>> d_modelGlobalCommands;
+
+  /**
+   * A list of commands that should be in the Model locally (i.e.,
+   * it is context-dependent on push/pop).  Only maintained if
+   * produce-models option is on.
+   */
+  CommandList d_modelCommands;
+  /**
+   * A list of model commands allocated to d_modelCommands at any time. This
+   * is maintained for memory management purposes.
+   */
+  std::vector<std::unique_ptr<Command>> d_modelCommandsAlloc;
+
+  /**
+   * A vector of declaration commands waiting to be dumped out.
+   * Once the SmtEngine 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<Command>> d_dumpCommands;
+};
+
+}  // namespace smt
+}  // namespace CVC4
+
+#endif
diff --git a/src/smt/listeners.cpp b/src/smt/listeners.cpp
index 452894f62..41602dab2 100644
--- a/src/smt/listeners.cpp
+++ b/src/smt/listeners.cpp
@@ -20,6 +20,7 @@
 #include "options/smt_options.h"
 #include "smt/command.h"
 #include "smt/dump.h"
+#include "smt/dump_manager.h"
 #include "smt/smt_engine.h"
 #include "smt/smt_engine_scope.h"
 
@@ -35,14 +36,14 @@ void ResourceOutListener::notify()
   d_smt.interrupt();
 }
 
-SmtNodeManagerListener::SmtNodeManagerListener(SmtEngine& smt) : d_smt(smt) {}
+SmtNodeManagerListener::SmtNodeManagerListener(DumpManager& dm) : d_dm(dm) {}
 
 void SmtNodeManagerListener::nmNotifyNewSort(TypeNode tn, uint32_t flags)
 {
   DeclareTypeCommand c(tn.getAttribute(expr::VarNameAttr()), 0, tn.toType());
   if ((flags & ExprManager::SORT_FLAG_PLACEHOLDER) == 0)
   {
-    d_smt.addToModelCommandAndDump(c, flags);
+    d_dm.addToModelCommandAndDump(c, flags);
   }
 }
 
@@ -54,7 +55,7 @@ void SmtNodeManagerListener::nmNotifyNewSortConstructor(TypeNode tn,
                        tn.toType());
   if ((flags & ExprManager::SORT_FLAG_PLACEHOLDER) == 0)
   {
-    d_smt.addToModelCommandAndDump(c);
+    d_dm.addToModelCommandAndDump(c);
   }
 }
 
@@ -70,7 +71,7 @@ void SmtNodeManagerListener::nmNotifyNewDatatypes(
       types.push_back(dt.toType());
     }
     DatatypeDeclarationCommand c(types);
-    d_smt.addToModelCommandAndDump(c);
+    d_dm.addToModelCommandAndDump(c);
   }
 }
 
@@ -80,7 +81,7 @@ void SmtNodeManagerListener::nmNotifyNewVar(TNode n, uint32_t flags)
       n.getAttribute(expr::VarNameAttr()), n.toExpr(), n.getType().toType());
   if ((flags & ExprManager::VAR_FLAG_DEFINED) == 0)
   {
-    d_smt.addToModelCommandAndDump(c, flags);
+    d_dm.addToModelCommandAndDump(c, flags);
   }
 }
 
@@ -96,7 +97,7 @@ void SmtNodeManagerListener::nmNotifyNewSkolem(TNode n,
   }
   if ((flags & ExprManager::VAR_FLAG_DEFINED) == 0)
   {
-    d_smt.addToModelCommandAndDump(c, flags, false, "skolems");
+    d_dm.addToModelCommandAndDump(c, flags, false, "skolems");
   }
 }
 
diff --git a/src/smt/listeners.h b/src/smt/listeners.h
index 6054d13af..77d6d257f 100644
--- a/src/smt/listeners.h
+++ b/src/smt/listeners.h
@@ -41,13 +41,15 @@ class ResourceOutListener : public Listener
   SmtEngine& d_smt;
 };
 
+class DumpManager;
+
 /**
  * A listener for node manager calls, which impacts certain dumping traces.
  */
 class SmtNodeManagerListener : public NodeManagerListener
 {
  public:
-  SmtNodeManagerListener(SmtEngine& smt);
+  SmtNodeManagerListener(DumpManager& dm);
   /** Notify when new sort is created */
   void nmNotifyNewSort(TypeNode tn, uint32_t flags) override;
   /** Notify when new sort constructor is created */
@@ -65,8 +67,8 @@ class SmtNodeManagerListener : public NodeManagerListener
   void nmNotifyDeleteNode(TNode n) override {}
 
  private:
-  /** Reference to the smt engine */
-  SmtEngine& d_smt;
+  /** Reference to the dump manager of smt engine */
+  DumpManager& d_dm;
 };
 
 }  // namespace smt
diff --git a/src/smt/model.cpp b/src/smt/model.cpp
index 6f6a09f38..7924698ff 100644
--- a/src/smt/model.cpp
+++ b/src/smt/model.cpp
@@ -20,7 +20,7 @@
 #include "options/base_options.h"
 #include "printer/printer.h"
 #include "smt/command.h"
-#include "smt/command_list.h"
+#include "smt/dump_manager.h"
 #include "smt/smt_engine.h"
 #include "smt/smt_engine_scope.h"
 
@@ -37,18 +37,14 @@ std::ostream& operator<<(std::ostream& out, const Model& m) {
 
 Model::Model() : d_smt(*smt::currentSmtEngine()), d_isKnownSat(false) {}
 
-size_t Model::getNumCommands() const {
-  return d_smt.d_modelCommands->size() + d_smt.d_modelGlobalCommands.size();
+size_t Model::getNumCommands() const
+{
+  return d_smt.getDumpManager()->getNumModelCommands();
 }
 
-const Command* Model::getCommand(size_t i) const {
-  Assert(i < getNumCommands());
-  // index the global commands first, then the locals
-  if(i < d_smt.d_modelGlobalCommands.size()) {
-    return d_smt.d_modelGlobalCommands[i];
-  } else {
-    return (*d_smt.d_modelCommands)[i - d_smt.d_modelGlobalCommands.size()];
-  }
+const Command* Model::getCommand(size_t i) const
+{
+  return d_smt.getDumpManager()->getModelCommand(i);
 }
 
 }/* CVC4 namespace */
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 5d34e6fa2..f114dba7c 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -83,8 +83,8 @@
 #include "smt/abduction_solver.h"
 #include "smt/abstract_values.h"
 #include "smt/command.h"
-#include "smt/command_list.h"
 #include "smt/defined_function.h"
+#include "smt/dump_manager.h"
 #include "smt/listeners.h"
 #include "smt/logic_request.h"
 #include "smt/model_blocker.h"
@@ -137,16 +137,6 @@ extern const char* const plf_signatures;
 
 namespace smt {
 
-struct DeleteCommandFunction : public std::unary_function<const Command*, void>
-{
-  void operator()(const Command* command) { delete command; }
-};
-
-void DeleteAndClearCommandVector(std::vector<Command*>& commands) {
-  std::for_each(commands.begin(), commands.end(), DeleteCommandFunction());
-  commands.clear();
-}
-
 /**
  * This is an inelegant solution, but for the present, it will work.
  * The point of this is to separate the public and private portions of
@@ -338,8 +328,9 @@ SmtEngine::SmtEngine(ExprManager* em, Options* optr)
       d_exprManager(em),
       d_nodeManager(d_exprManager->getNodeManager()),
       d_absValues(new AbstractValues(d_nodeManager)),
+      d_dumpm(new DumpManager(d_userContext.get())),
       d_routListener(new ResourceOutListener(*this)),
-      d_snmListener(new SmtNodeManagerListener(*this)),
+      d_snmListener(new SmtNodeManagerListener(*d_dumpm.get())),
       d_theoryEngine(nullptr),
       d_propEngine(nullptr),
       d_proofManager(nullptr),
@@ -348,9 +339,6 @@ SmtEngine::SmtEngine(ExprManager* em, Options* optr)
       d_abductSolver(nullptr),
       d_assertionList(nullptr),
       d_assignments(nullptr),
-      d_modelGlobalCommands(),
-      d_modelCommands(nullptr),
-      d_dumpCommands(),
       d_defineCommands(),
       d_logic(),
       d_originalOptions(),
@@ -413,7 +401,6 @@ SmtEngine::SmtEngine(ExprManager* em, Options* optr)
 #endif
 
   d_definedFunctions = new (true) DefinedFunctionMap(getUserContext());
-  d_modelCommands = new (true) smt::CommandList(getUserContext());
 }
 
 void SmtEngine::finishInit()
@@ -495,13 +482,8 @@ void SmtEngine::finishInit()
                                everything.getLogicString());
   }
 
-  Trace("smt-debug") << "Dump declaration commands..." << std::endl;
-  // dump out any pending declaration commands
-  for(unsigned i = 0; i < d_dumpCommands.size(); ++i) {
-    Dump("declarations") << *d_dumpCommands[i];
-    delete d_dumpCommands[i];
-  }
-  d_dumpCommands.clear();
+  // initialize the dump manager
+  d_dumpm->finishInit();
 
   // subsolvers
   if (options::produceAbducts())
@@ -579,18 +561,6 @@ SmtEngine::~SmtEngine()
       d_assertionList->deleteSelf();
     }
 
-    for(unsigned i = 0; i < d_dumpCommands.size(); ++i) {
-      delete d_dumpCommands[i];
-      d_dumpCommands[i] = NULL;
-    }
-    d_dumpCommands.clear();
-
-    DeleteAndClearCommandVector(d_modelGlobalCommands);
-
-    if(d_modelCommands != NULL) {
-      d_modelCommands->deleteSelf();
-    }
-
     d_definedFunctions->deleteSelf();
 
     //destroy all passes before destroying things that they refer to
@@ -608,6 +578,7 @@ SmtEngine::~SmtEngine()
 #endif
 
     d_absValues.reset(nullptr);
+    d_dumpm.reset(nullptr);
 
     d_theoryEngine.reset(nullptr);
     d_propEngine.reset(nullptr);
@@ -950,7 +921,7 @@ void SmtEngine::defineFunction(Expr func,
             language::SetLanguage::getLanguage(Dump.getStream()))
      << func;
   DefineFunctionCommand c(ss.str(), func, formals, formula, global);
-  addToModelCommandAndDump(
+  d_dumpm->addToModelCommandAndDump(
       c, ExprManager::VAR_FLAG_DEFINED, true, "declarations");
 
   PROOF(if (options::checkUnsatCores()) {
@@ -2050,35 +2021,6 @@ vector<pair<Expr, Expr>> SmtEngine::getAssignment()
   return res;
 }
 
-void SmtEngine::addToModelCommandAndDump(const Command& c, uint32_t flags, bool userVisible, const char* dumpTag) {
-  Trace("smt") << "SMT addToModelCommandAndDump(" << c << ")" << endl;
-  SmtScope smts(this);
-  // If we aren't yet fully inited, the user might still turn on
-  // produce-models.  So let's keep any commands around just in
-  // case.  This is useful in two cases: (1) SMT-LIBv1 auto-declares
-  // sort "U" in QF_UF before setLogic() is run and we still want to
-  // support finding card(U) with --finite-model-find, and (2) to
-  // decouple SmtEngine and ExprManager if the user does a few
-  // ExprManager::mkSort() before SmtEngine::setOption("produce-models")
-  // and expects to find their cardinalities in the model.
-  if(/* userVisible && */
-     (!d_fullyInited || options::produceModels()) &&
-     (flags & ExprManager::VAR_FLAG_DEFINED) == 0) {
-    if(flags & ExprManager::VAR_FLAG_GLOBAL) {
-      d_modelGlobalCommands.push_back(c.clone());
-    } else {
-      d_modelCommands->push_back(c.clone());
-    }
-  }
-  if(Dump.isOn(dumpTag)) {
-    if(d_fullyInited) {
-      Dump(dumpTag) << c;
-    } else {
-      d_dumpCommands.push_back(c.clone());
-    }
-  }
-}
-
 // TODO(#1108): Simplify the error reporting of this method.
 Model* SmtEngine::getModel() {
   Trace("smt") << "SMT getModel()" << endl;
@@ -3078,7 +3020,7 @@ void SmtEngine::resetAssertions()
     // (see solver execution modes in the SMT-LIB standard)
     Assert(d_context->getLevel() == 0);
     Assert(d_userContext->getLevel() == 0);
-    DeleteAndClearCommandVector(d_modelGlobalCommands);
+    d_dumpm->resetAssertions();
     return;
   }
 
@@ -3100,7 +3042,7 @@ void SmtEngine::resetAssertions()
   Assert(d_userLevels.size() == 0 && d_userContext->getLevel() == 1);
   d_context->popto(0);
   d_userContext->popto(0);
-  DeleteAndClearCommandVector(d_modelGlobalCommands);
+  d_dumpm->resetAssertions();
   d_userContext->push();
   d_context->push();
 
@@ -3177,28 +3119,6 @@ void SmtEngine::setUserAttribute(const std::string& attr,
   d_theoryEngine->setUserAttribute(attr, expr.getNode(), node_values, str_value);
 }
 
-void SmtEngine::setPrintFuncInModel(Expr f, bool p) {
-  Trace("setp-model") << "Set printInModel " << f << " to " << p << std::endl;
-  for( unsigned i=0; i<d_modelGlobalCommands.size(); i++ ){
-    Command * c = d_modelGlobalCommands[i];
-    DeclareFunctionCommand* dfc = dynamic_cast<DeclareFunctionCommand*>(c);
-    if(dfc != NULL) {
-      if( dfc->getFunction()==f ){
-        dfc->setPrintInModel( p );
-      }
-    }
-  }
-  for( unsigned i=0; i<d_modelCommands->size(); i++ ){
-    Command * c = (*d_modelCommands)[i];
-    DeclareFunctionCommand* dfc = dynamic_cast<DeclareFunctionCommand*>(c);
-    if(dfc != NULL) {
-      if( dfc->getFunction()==f ){
-        dfc->setPrintInModel( p );
-      }
-    }
-  }
-}
-
 void SmtEngine::setOption(const std::string& key, const CVC4::SExpr& value)
 {
   // Always check whether the SmtEngine has been initialized (which is done
@@ -3317,6 +3237,8 @@ ResourceManager* SmtEngine::getResourceManager()
   return d_resourceManager.get();
 }
 
+DumpManager* SmtEngine::getDumpManager() { return d_dumpm.get(); }
+
 void SmtEngine::setSygusConjectureStale()
 {
   if (d_private->d_sygusConjectureStale)
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index f260a307b..99b993e7b 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -93,6 +93,7 @@ namespace prop {
 namespace smt {
 /** Utilities */
 class AbstractValues;
+class DumpManager;
 class ResourceOutListener;
 class SmtNodeManagerListener;
 class OptionsManager;
@@ -112,9 +113,6 @@ class SmtScope;
 class ProcessAssertions;
 
 ProofManager* currentProofManager();
-
-struct CommandCleanup;
-typedef context::CDList<Command*, CommandCleanup> CommandList;
 }/* CVC4::smt namespace */
 
 /* -------------------------------------------------------------------------- */
@@ -147,9 +145,6 @@ class CVC4_PUBLIC SmtEngine
   friend class ::CVC4::smt::ProcessAssertions;
   friend ProofManager* ::CVC4::smt::currentProofManager();
   friend class ::CVC4::LogicRequest;
-  friend class ::CVC4::Model;  // to access d_modelCommands
-  friend class ::CVC4::smt::SmtNodeManagerListener;  // to access
-                                                     // addToModelCommandAndDump
   friend class ::CVC4::theory::TheoryModel;
   friend class ::CVC4::theory::Rewriter;
 
@@ -857,9 +852,6 @@ class CVC4_PUBLIC SmtEngine
                         const std::vector<Expr>& expr_values,
                         const std::string& str_value);
 
-  /** Set print function in model. */
-  void setPrintFuncInModel(Expr f, bool p);
-
   /**
    * Get expression name.
    *
@@ -883,6 +875,9 @@ class CVC4_PUBLIC SmtEngine
   /** Get the resource manager of this SMT engine */
   ResourceManager* getResourceManager();
 
+  /** Permit access to the underlying dump manager. */
+  smt::DumpManager* getDumpManager();
+
   /**
    * Get expanded assertions.
    *
@@ -1126,6 +1121,8 @@ class CVC4_PUBLIC SmtEngine
   NodeManager* d_nodeManager;
   /** Abstract values */
   std::unique_ptr<smt::AbstractValues> d_absValues;
+  /** The dump manager */
+  std::unique_ptr<smt::DumpManager> d_dumpm;
   /** Resource out listener */
   std::unique_ptr<smt::ResourceOutListener> d_routListener;
   /** Node manager listener */
@@ -1179,28 +1176,6 @@ class CVC4_PUBLIC SmtEngine
   AssignmentSet* d_assignments;
 
   /**
-   * A list of commands that should be in the Model globally (i.e.,
-   * regardless of push/pop).  Only maintained if produce-models option
-   * is on.
-   */
-  std::vector<Command*> d_modelGlobalCommands;
-
-  /**
-   * A list of commands that should be in the Model locally (i.e.,
-   * it is context-dependent on push/pop).  Only maintained if
-   * produce-models option is on.
-   */
-  smt::CommandList* d_modelCommands;
-
-  /**
-   * A vector of declaration commands waiting to be dumped out.
-   * Once the SmtEngine 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<Command*> d_dumpCommands;
-
-  /**
    * A vector of command definitions to be imported in the new
    * SmtEngine when checking unsat-cores.
    */