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.

10 files changed, 13 insertions, 183 deletions

diff --git a/src/smt/check_models.cpp b/src/smt/check_models.cpp
index 612084de2..56d54eec9 100644
--- a/src/smt/check_models.cpp
+++ b/src/smt/check_models.cpp
@@ -67,24 +67,14 @@ void CheckModels::checkModel(Model* m,
                                 /* substituteUnderQuantifiers = */ false);
 
   Trace("check-model") << "checkModel: Collect substitution..." << std::endl;
-  for (size_t k = 0, ncmd = m->getNumCommands(); k < ncmd; ++k)
+  const std::vector<Node>& decTerms = m->getDeclaredTerms();
+  for (const Node& func : decTerms)
   {
-    const DeclareFunctionNodeCommand* c =
-        dynamic_cast<const DeclareFunctionNodeCommand*>(m->getCommand(k));
-    Notice() << "SmtEngine::checkModel(): model command " << k << " : "
-             << m->getCommand(k)->toString() << std::endl;
-    if (c == nullptr)
-    {
-      // we don't care about DECLARE-DATATYPES, DECLARE-SORT, ...
-      Notice() << "SmtEngine::checkModel(): skipping..." << std::endl;
-      continue;
-    }
     // We have a DECLARE-FUN:
     //
     // We'll first do some checks, then add to our substitution map
     // the mapping: function symbol |-> value
 
-    Node func = c->getFunction();
     Node val = m->getValue(func);
 
     Notice() << "SmtEngine::checkModel(): adding substitution: " << func
diff --git a/src/smt/command.cpp b/src/smt/command.cpp
index fa3eb66c0..e6361be9e 100644
--- a/src/smt/command.cpp
+++ b/src/smt/command.cpp
@@ -1069,25 +1069,12 @@ DeclareFunctionCommand::DeclareFunctionCommand(const std::string& id,
                                                api::Sort sort)
     : DeclarationDefinitionCommand(id),
       d_func(func),
-      d_sort(sort),
-      d_printInModel(true),
-      d_printInModelSetByUser(false)
+      d_sort(sort)
 {
 }
 
 api::Term DeclareFunctionCommand::getFunction() const { return d_func; }
 api::Sort DeclareFunctionCommand::getSort() const { return d_sort; }
-bool DeclareFunctionCommand::getPrintInModel() const { return d_printInModel; }
-bool DeclareFunctionCommand::getPrintInModelSetByUser() const
-{
-  return d_printInModelSetByUser;
-}
-
-void DeclareFunctionCommand::setPrintInModel(bool p)
-{
-  d_printInModel = p;
-  d_printInModelSetByUser = true;
-}
 
 void DeclareFunctionCommand::invoke(api::Solver* solver, SymbolManager* sm)
 {
@@ -1100,8 +1087,6 @@ Command* DeclareFunctionCommand::clone() const
 {
   DeclareFunctionCommand* dfc =
       new DeclareFunctionCommand(d_symbol, d_func, d_sort);
-  dfc->d_printInModel = d_printInModel;
-  dfc->d_printInModelSetByUser = d_printInModelSetByUser;
   return dfc;
 }
 
diff --git a/src/smt/command.h b/src/smt/command.h
index 96a6938d6..0b86f3539 100644
--- a/src/smt/command.h
+++ b/src/smt/command.h
@@ -387,16 +387,11 @@ class CVC4_PUBLIC DeclareFunctionCommand : public DeclarationDefinitionCommand
  protected:
   api::Term d_func;
   api::Sort d_sort;
-  bool d_printInModel;
-  bool d_printInModelSetByUser;
 
  public:
   DeclareFunctionCommand(const std::string& id, api::Term func, api::Sort sort);
   api::Term getFunction() const;
   api::Sort getSort() const;
-  bool getPrintInModel() const;
-  bool getPrintInModelSetByUser() const;
-  void setPrintInModel(bool p);
 
   void invoke(api::Solver* solver, SymbolManager* sm) override;
   Command* clone() const override;
diff --git a/src/smt/dump_manager.cpp b/src/smt/dump_manager.cpp
index 9b7fba5a2..9d3031b4d 100644
--- a/src/smt/dump_manager.cpp
+++ b/src/smt/dump_manager.cpp
@@ -24,8 +24,6 @@ namespace smt {
 
 DumpManager::DumpManager(context::UserContext* u)
     : d_fullyInited(false),
-      d_modelGlobalCommands(),
-      d_modelCommands(u),
       d_dumpCommands()
 {
 }
@@ -33,8 +31,6 @@ DumpManager::DumpManager(context::UserContext* u)
 DumpManager::~DumpManager()
 {
   d_dumpCommands.clear();
-  d_modelCommandsAlloc.clear();
-  d_modelGlobalCommands.clear();
 }
 
 void DumpManager::finishInit()
@@ -49,8 +45,10 @@ void DumpManager::finishInit()
 
   d_fullyInited = true;
 }
-
-void DumpManager::resetAssertions() { d_modelGlobalCommands.clear(); }
+void DumpManager::resetAssertions()
+{
+  // currently, do nothing
+}
 
 void DumpManager::addToModelCommandAndDump(const NodeCommand& c,
                                            uint32_t flags,
@@ -58,29 +56,6 @@ void DumpManager::addToModelCommandAndDump(const NodeCommand& c,
                                            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<NodeCommand>(c.clone()));
-    }
-    else
-    {
-      NodeCommand* cc = c.clone();
-      d_modelCommands.push_back(cc);
-      // also remember for memory management purposes
-      d_modelCommandsAlloc.push_back(std::unique_ptr<NodeCommand>(cc));
-    }
-  }
   if (Dump.isOn(dumpTag))
   {
     if (d_fullyInited)
@@ -97,48 +72,7 @@ void DumpManager::addToModelCommandAndDump(const NodeCommand& c,
 void DumpManager::setPrintFuncInModel(Node f, bool p)
 {
   Trace("setp-model") << "Set printInModel " << f << " to " << p << std::endl;
-  for (std::unique_ptr<NodeCommand>& c : d_modelGlobalCommands)
-  {
-    DeclareFunctionNodeCommand* dfc =
-        dynamic_cast<DeclareFunctionNodeCommand*>(c.get());
-    if (dfc != NULL)
-    {
-      Node df = dfc->getFunction();
-      if (df == f)
-      {
-        dfc->setPrintInModel(p);
-      }
-    }
-  }
-  for (NodeCommand* c : d_modelCommands)
-  {
-    DeclareFunctionNodeCommand* dfc =
-        dynamic_cast<DeclareFunctionNodeCommand*>(c);
-    if (dfc != NULL)
-    {
-      Node df = dfc->getFunction();
-      if (df == f)
-      {
-        dfc->setPrintInModel(p);
-      }
-    }
-  }
-}
-
-size_t DumpManager::getNumModelCommands() const
-{
-  return d_modelCommands.size() + d_modelGlobalCommands.size();
-}
-
-const NodeCommand* 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()];
+  // TODO (cvc4-wishues/issues/75): implement
 }
 
 }  // namespace smt
diff --git a/src/smt/dump_manager.h b/src/smt/dump_manager.h
index 0ba8e0b8b..eaedf39a1 100644
--- a/src/smt/dump_manager.h
+++ b/src/smt/dump_manager.h
@@ -31,14 +31,10 @@ 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.
+ * implementing some dumping traces e.g. --dump=declarations.
  */
 class DumpManager
 {
-  typedef context::CDList<NodeCommand*> CommandList;
 
  public:
   DumpManager(context::UserContext* u);
@@ -65,34 +61,10 @@ class DumpManager
    * 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 NodeCommand* 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<NodeCommand>> 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<NodeCommand>> d_modelCommandsAlloc;
-
   /**
    * A vector of declaration commands waiting to be dumped out.
    * Once the SmtEngine is fully initialized, we'll dump them.
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; }
diff --git a/src/smt/model.h b/src/smt/model.h
index 0913922d1..18675040a 100644
--- a/src/smt/model.h
+++ b/src/smt/model.h
@@ -27,7 +27,6 @@
 namespace CVC4 {
 
 class SmtEngine;
-class NodeCommand;
 
 namespace smt {
 
@@ -49,13 +48,9 @@ class Model {
 
  public:
   /** construct */
-  Model(SmtEngine& smt, theory::TheoryModel* tm);
+  Model(theory::TheoryModel* tm);
   /** virtual destructor */
   ~Model() {}
-  /** get the smt engine that this model is hooked up to */
-  SmtEngine* getSmtEngine() { return &d_smt; }
-  /** get the smt engine (as a pointer-to-const) that this model is hooked up to */
-  const SmtEngine* getSmtEngine() const { return &d_smt; }
   /** get the input name (file name, etc.) this model is associated to */
   std::string getInputName() const { return d_inputName; }
   /**
@@ -77,10 +72,6 @@ class Model {
   /** Does this model have approximations? */
   bool hasApproximations() const;
   //----------------------- end helper methods
-  /** get number of commands to report */
-  size_t getNumCommands() const;
-  /** get command */
-  const NodeCommand* getCommand(size_t i) const;
   //----------------------- model declarations
   /** Clear the current model declarations. */
   void clearModelDeclarations();
@@ -100,8 +91,6 @@ class Model {
   const std::vector<Node>& getDeclaredTerms() const;
   //----------------------- end model declarations
  protected:
-  /** The SmtEngine we're associated with */
-  SmtEngine& d_smt;
   /** the input name (file name, etc.) this model is associated to */
   std::string d_inputName;
   /**
diff --git a/src/smt/node_command.cpp b/src/smt/node_command.cpp
index 91184d27d..815f99132 100644
--- a/src/smt/node_command.cpp
+++ b/src/smt/node_command.cpp
@@ -51,9 +51,7 @@ DeclareFunctionNodeCommand::DeclareFunctionNodeCommand(const std::string& id,
                                                        TypeNode type)
     : d_id(id),
       d_fun(expr),
-      d_type(type),
-      d_printInModel(true),
-      d_printInModelSetByUser(false)
+      d_type(type)
 {
 }
 
@@ -72,22 +70,6 @@ NodeCommand* DeclareFunctionNodeCommand::clone() const
 
 const Node& DeclareFunctionNodeCommand::getFunction() const { return d_fun; }
 
-bool DeclareFunctionNodeCommand::getPrintInModel() const
-{
-  return d_printInModel;
-}
-
-bool DeclareFunctionNodeCommand::getPrintInModelSetByUser() const
-{
-  return d_printInModelSetByUser;
-}
-
-void DeclareFunctionNodeCommand::setPrintInModel(bool p)
-{
-  d_printInModel = p;
-  d_printInModelSetByUser = true;
-}
-
 /* -------------------------------------------------------------------------- */
 /* class DeclareTypeNodeCommand                                               */
 /* -------------------------------------------------------------------------- */
diff --git a/src/smt/node_command.h b/src/smt/node_command.h
index 8cf9a5e10..e1a15e62c 100644
--- a/src/smt/node_command.h
+++ b/src/smt/node_command.h
@@ -68,16 +68,11 @@ class DeclareFunctionNodeCommand : public NodeCommand
       OutputLanguage language = language::output::LANG_AUTO) const override;
   NodeCommand* clone() const override;
   const Node& getFunction() const;
-  bool getPrintInModel() const;
-  bool getPrintInModelSetByUser() const;
-  void setPrintInModel(bool p);
 
  private:
   std::string d_id;
   Node d_fun;
   TypeNode d_type;
-  bool d_printInModel;
-  bool d_printInModelSetByUser;
 };
 
 /**
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 161c2eba6..0f40db530 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -243,7 +243,7 @@ void SmtEngine::finishInit()
   TheoryModel* tm = te->getModel();
   if (tm != nullptr)
   {
-    d_model.reset(new Model(*this, tm));
+    d_model.reset(new Model(tm));
     // make the check models utility
     d_checkModels.reset(new CheckModels(*d_smtSolver.get()));
   }