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, 5 insertions, 71 deletions

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