Removing infrastructure related to SMT model (#5527)

Now, SMT models do not store an internal list of commands, and are not dependent on a reference to SmtEngine.

The next cleanup step will be to merge OutputManager, DumpManager, and SmtEngineNodeListener.

1 files changed, 1 insertions, 13 deletions

diff --git a/src/smt/model.cpp b/src/smt/model.cpp
index b734ad9e9..8a9f944d2 100644
--- a/src/smt/model.cpp
+++ b/src/smt/model.cpp
@@ -26,29 +26,17 @@
 namespace CVC4 {
 namespace smt {
 
-Model::Model(SmtEngine& smt, theory::TheoryModel* tm)
-    : d_smt(smt), d_isKnownSat(false), d_tmodel(tm)
+Model::Model(theory::TheoryModel* tm) : d_isKnownSat(false), d_tmodel(tm)
 {
   Assert(d_tmodel != nullptr);
 }
 
 std::ostream& operator<<(std::ostream& out, const Model& m) {
-  smt::SmtScope smts(&m.d_smt);
   expr::ExprDag::Scope scope(out, false);
   Printer::getPrinter(options::outputLanguage())->toStream(out, m);
   return out;
 }
 
-size_t Model::getNumCommands() const
-{
-  return d_smt.getDumpManager()->getNumModelCommands();
-}
-
-const NodeCommand* Model::getCommand(size_t i) const
-{
-  return d_smt.getDumpManager()->getModelCommand(i);
-}
-
 theory::TheoryModel* Model::getTheoryModel() { return d_tmodel; }
 
 const theory::TheoryModel* Model::getTheoryModel() const { return d_tmodel; }