Transfer ownership of internal Options from NodeManager to SmtEngine (#4682)

This PR decouples Options from NodeManager. Instead, options now live in SmtEngine.

The changes that were required for this PR include:

The main internal options object is now owned by SmtEngine instead of ExprManager.
The ownership resource manager is moved from NodeManager to SmtEngine.
Node manager listeners are deleted, timeouts and resource limits are set during SmtEngine::finishInit.
A temporary hack was added to make the last constructed SmtEngine to be the one in scope. This ensures that options are in scope whenever an SmtEngine is created.
The methods for invoking "subsolvers" (theory/smt_engine_subsolver.h,cpp) was simplified, as versions of these calls that change options do not have to clone a new copy of the ExprManager anymore.
Resource manager was removed from the smt2 parser.
Minor refactoring was done in SmtEngine to copy "original options" so that options are restored to their state after parsing command line options on reset.
Updates to unit tests to ensure conformance to new options scoping.

1 files changed, 22 insertions, 78 deletions

diff --git a/src/theory/smt_engine_subsolver.cpp b/src/theory/smt_engine_subsolver.cpp
index f529d3fea..45c115524 100644
--- a/src/theory/smt_engine_subsolver.cpp
+++ b/src/theory/smt_engine_subsolver.cpp
@@ -41,52 +41,32 @@ Result quickCheck(Node& query)
   return Result(Result::SAT_UNKNOWN, Result::REQUIRES_FULL_CHECK);
 }
 
-void initializeSubsolver(SmtEngine* smte)
+void initializeSubsolver(std::unique_ptr<SmtEngine>& smte,
+                         Node query,
+                         bool needsTimeout,
+                         unsigned long timeout)
 {
+  NodeManager* nm = NodeManager::currentNM();
+  SmtEngine* smtCurr = smt::currentSmtEngine();
+  // must copy the options
+  smte.reset(new SmtEngine(nm->toExprManager(), &smtCurr->getOptions()));
   smte->setIsInternalSubsolver();
-  smte->setLogic(smt::currentSmtEngine()->getLogicInfo());
-}
-
-void initializeSubsolverWithExport(SmtEngine* smte,
-                                   ExprManager* em,
-                                   ExprManagerMapCollection& varMap,
-                                   Node query,
-                                   bool needsTimeout,
-                                   unsigned long timeout)
-{
-  // To support a separate timeout for the subsolver, we need to use
-  // a separate ExprManager with its own options. This requires that
-  // the expressions sent to the subsolver can be exported from on
-  // ExprManager to another. If the export fails, we throw an
-  // OptionException.
-  try
+  smte->setLogic(smtCurr->getLogicInfo());
+  if (needsTimeout)
   {
-    smte->setIsInternalSubsolver();
-    if (needsTimeout)
-    {
-      smte->setTimeLimit(timeout, true);
-    }
-    smte->setLogic(smt::currentSmtEngine()->getLogicInfo());
-    Expr equery = query.toExpr().exportTo(em, varMap);
-    smte->assertFormula(equery);
+    smte->setTimeLimit(timeout, true);
   }
-  catch (const CVC4::ExportUnsupportedException& e)
+  smte->setLogic(smt::currentSmtEngine()->getLogicInfo());
+  if (!query.isNull())
   {
-    std::stringstream msg;
-    msg << "Unable to export " << query
-        << " but exporting expressions is "
-           "required for a subsolver.";
-    throw OptionException(msg.str());
+    smte->assertFormula(query.toExpr());
   }
 }
 
-void initializeSubsolver(SmtEngine* smte, Node query)
-{
-  initializeSubsolver(smte);
-  smte->assertFormula(query.toExpr());
-}
-
-Result checkWithSubsolver(SmtEngine* smte, Node query)
+Result checkWithSubsolver(std::unique_ptr<SmtEngine>& smte,
+                          Node query,
+                          bool needsTimeout,
+                          unsigned long timeout)
 {
   Assert(query.getType().isBoolean());
   Result r = quickCheck(query);
@@ -94,7 +74,7 @@ Result checkWithSubsolver(SmtEngine* smte, Node query)
   {
     return r;
   }
-  initializeSubsolver(smte, query);
+  initializeSubsolver(smte, query, needsTimeout, timeout);
   return smte->checkSat();
 }
 
@@ -128,50 +108,14 @@ Result checkWithSubsolver(Node query,
     }
     return r;
   }
-
-  // !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
-  // This is only temporarily until we have separate options for each
-  // SmtEngine instance. We should reuse the same ExprManager with
-  // a different SmtEngine (and different options) here, eventually.
-  // !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
-  std::unique_ptr<SmtEngine> simpleSmte;
-  std::unique_ptr<api::Solver> slv;
-  ExprManager* em = nullptr;
-  SmtEngine* smte = nullptr;
-  ExprManagerMapCollection varMap;
-  NodeManager* nm = NodeManager::currentNM();
-  bool needsExport = false;
-  if (needsTimeout)
-  {
-    slv.reset(new api::Solver(&nm->getOptions()));
-    em = slv->getExprManager();
-    smte = slv->getSmtEngine();
-    needsExport = true;
-    initializeSubsolverWithExport(
-        smte, em, varMap, query, needsTimeout, timeout);
-  }
-  else
-  {
-    em = nm->toExprManager();
-    simpleSmte.reset(new SmtEngine(em));
-    smte = simpleSmte.get();
-    initializeSubsolver(smte, query);
-  }
+  std::unique_ptr<SmtEngine> smte;
+  initializeSubsolver(smte, query, needsTimeout, timeout);
   r = smte->checkSat();
   if (r.asSatisfiabilityResult().isSat() == Result::SAT)
   {
     for (const Node& v : vars)
     {
-      Expr val;
-      if (needsExport)
-      {
-        Expr ev = v.toExpr().exportTo(em, varMap);
-        val = smte->getValue(ev).exportTo(nm->toExprManager(), varMap);
-      }
-      else
-      {
-        val = smte->getValue(v.toExpr());
-      }
+      Expr val = smte->getValue(v.toExpr());
       modelVals.push_back(Node::fromExpr(val));
     }
   }