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.

1 files changed, 7 insertions, 11 deletions

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 */