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.

11 files changed, 49 insertions, 163 deletions

diff --git a/src/theory/quantifiers/candidate_rewrite_database.cpp b/src/theory/quantifiers/candidate_rewrite_database.cpp
index fc3474df4..cabd78643 100644
--- a/src/theory/quantifiers/candidate_rewrite_database.cpp
+++ b/src/theory/quantifiers/candidate_rewrite_database.cpp
@@ -129,26 +129,14 @@ bool CandidateRewriteDatabase::addTerm(Node sol,
       // verify it if applicable
       if (options::sygusRewSynthCheck())
       {
-        NodeManager* nm = NodeManager::currentNM();
-
         Node crr = solbr.eqNode(eq_solr).negate();
         Trace("rr-check") << "Check candidate rewrite : " << crr << std::endl;
 
         // Notice we don't set produce-models. rrChecker takes the same
         // options as the SmtEngine we belong to, where we ensure that
         // produce-models is set.
-        bool needExport = false;
-
-        // !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
-        // 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.
-        // !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
-        api::Solver slv(&nm->getOptions());
-        ExprManager* em = slv.getExprManager();
-        SmtEngine* rrChecker = slv.getSmtEngine();
-        ExprManagerMapCollection varMap;
-        initializeChecker(rrChecker, em, varMap, crr, needExport);
+        std::unique_ptr<SmtEngine> rrChecker;
+        initializeChecker(rrChecker, crr);
         Result r = rrChecker->checkSat();
         Trace("rr-check") << "...result : " << r << std::endl;
         if (r.asSatisfiabilityResult().isSat() == Result::SAT)
@@ -181,16 +169,7 @@ bool CandidateRewriteDatabase::addTerm(Node sol,
             if (val.isNull())
             {
               Assert(!refv.isNull() && refv.getKind() != BOUND_VARIABLE);
-              if (needExport)
-              {
-                Expr erefv = refv.toExpr().exportTo(em, varMap);
-                val = Node::fromExpr(rrChecker->getValue(erefv).exportTo(
-                    nm->toExprManager(), varMap));
-              }
-              else
-              {
-                val = Node::fromExpr(rrChecker->getValue(refv.toExpr()));
-              }
+              val = Node::fromExpr(rrChecker->getValue(refv.toExpr()));
             }
             Trace("rr-check") << "  " << v << " -> " << val << std::endl;
             pt.push_back(val);
diff --git a/src/theory/quantifiers/expr_miner.cpp b/src/theory/quantifiers/expr_miner.cpp
index b209fc6ff..6153242e7 100644
--- a/src/theory/quantifiers/expr_miner.cpp
+++ b/src/theory/quantifiers/expr_miner.cpp
@@ -69,32 +69,16 @@ Node ExprMiner::convertToSkolem(Node n)
   return n.substitute(sfvs.begin(), sfvs.end(), sks.begin(), sks.end());
 }
 
-void ExprMiner::initializeChecker(SmtEngine* checker,
-                                  ExprManager* em,
-                                  ExprManagerMapCollection& varMap,
-                                  Node query,
-                                  bool& needExport)
+void ExprMiner::initializeChecker(std::unique_ptr<SmtEngine>& checker,
+                                  Node query)
 {
   // Convert bound variables to skolems. This ensures the satisfiability
   // check is ground.
   Node squery = convertToSkolem(query);
-  if (options::sygusExprMinerCheckUseExport())
-  {
-    initializeSubsolverWithExport(checker,
-                                  em,
-                                  varMap,
-                                  squery.toExpr(),
-                                  true,
-                                  options::sygusExprMinerCheckTimeout());
-    checker->setOption("sygus-rr-synth-input", false);
-    checker->setOption("input-language", "smt2");
-    needExport = true;
-  }
-  else
-  {
-    initializeSubsolver(checker, squery.toExpr());
-    needExport = false;
-  }
+  initializeSubsolver(checker, squery.toExpr());
+  // also set the options
+  checker->setOption("sygus-rr-synth-input", false);
+  checker->setOption("input-language", "smt2");
 }
 
 Result ExprMiner::doCheck(Node query)
@@ -111,18 +95,8 @@ Result ExprMiner::doCheck(Node query)
       return Result(Result::SAT);
     }
   }
-  // !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
-  // 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.
-  // !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
-  NodeManager* nm = NodeManager::currentNM();
-  bool needExport = false;
-  api::Solver slv(&nm->getOptions());
-  ExprManager* em = slv.getExprManager();
-  SmtEngine* smte = slv.getSmtEngine();
-  ExprManagerMapCollection varMap;
-  initializeChecker(smte, em, varMap, queryr, needExport);
+  std::unique_ptr<SmtEngine> smte;
+  initializeChecker(smte, query);
   return smte->checkSat();
 }
 
diff --git a/src/theory/quantifiers/expr_miner.h b/src/theory/quantifiers/expr_miner.h
index eebcebf88..e603075c4 100644
--- a/src/theory/quantifiers/expr_miner.h
+++ b/src/theory/quantifiers/expr_miner.h
@@ -78,22 +78,8 @@ class ExprMiner
    * This function initializes the smt engine smte to check the satisfiability
    * of the argument "query", which is a formula whose free variables (of
    * kind BOUND_VARIABLE) are a subset of d_vars.
-   *
-   * The arguments em and varMap are used for supporting cases where we
-   * want smte to use a different expression manager instead of the current
-   * expression manager. The motivation for this so that different options can
-   * be set for the subcall.
-   *
-   * We update the flag needExport to true if smte is using the expression
-   * manager em. In this case, subsequent expressions extracted from smte
-   * (for instance, model values) must be exported to the current expression
-   * manager.
    */
-  void initializeChecker(SmtEngine* smte,
-                         ExprManager* em,
-                         ExprManagerMapCollection& varMap,
-                         Node query,
-                         bool& needExport);
+  void initializeChecker(std::unique_ptr<SmtEngine>& smte, Node query);
   /**
    * Run the satisfiability check on query and return the result
    * (sat/unsat/unknown).
diff --git a/src/theory/quantifiers/query_generator.cpp b/src/theory/quantifiers/query_generator.cpp
index 4cf65b24a..39d27373d 100644
--- a/src/theory/quantifiers/query_generator.cpp
+++ b/src/theory/quantifiers/query_generator.cpp
@@ -157,20 +157,9 @@ void QueryGenerator::checkQuery(Node qy, unsigned spIndex)
   if (options::sygusQueryGenCheck())
   {
     Trace("sygus-qgen-check") << "  query: check " << qy << "..." << std::endl;
-    NodeManager* nm = NodeManager::currentNM();
     // make the satisfiability query
-    //
-    // !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
-    // 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.
-    // !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
-    bool needExport = false;
-    api::Solver slv(&nm->getOptions());
-    ExprManager* em = slv.getExprManager();
-    SmtEngine* queryChecker = slv.getSmtEngine();
-    ExprManagerMapCollection varMap;
-    initializeChecker(queryChecker, em, varMap, qy, needExport);
+    std::unique_ptr<SmtEngine> queryChecker;
+    initializeChecker(queryChecker, qy);
     Result r = queryChecker->checkSat();
     Trace("sygus-qgen-check") << "  query: ...got : " << r << std::endl;
     if (r.asSatisfiabilityResult().isSat() == Result::UNSAT)
diff --git a/src/theory/quantifiers/solution_filter.cpp b/src/theory/quantifiers/solution_filter.cpp
index e98b875fd..d4637a636 100644
--- a/src/theory/quantifiers/solution_filter.cpp
+++ b/src/theory/quantifiers/solution_filter.cpp
@@ -88,10 +88,10 @@ bool SolutionFilterStrength::addTerm(Node n, std::ostream& out)
       }
       else
       {
-        Options& nodeManagerOptions = nm->getOptions();
-        std::ostream* nodeManagerOut = nodeManagerOptions.getOut();
-        (*nodeManagerOut) << "; (filtered " << (d_isStrong ? s : s.negate())
-                          << ")" << std::endl;
+        Options& opts = smt::currentSmtEngine()->getOptions();
+        std::ostream* smtOut = opts.getOut();
+        (*smtOut) << "; (filtered " << (d_isStrong ? s : s.negate()) << ")"
+                  << std::endl;
       }
     }
     d_curr_sols.clear();
diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
index df21a06eb..d0cac6d58 100644
--- a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
+++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
@@ -26,6 +26,7 @@
 #include "theory/quantifiers/term_enumeration.h"
 #include "theory/quantifiers/term_util.h"
 #include "theory/quantifiers_engine.h"
+#include "theory/smt_engine_subsolver.h"
 
 using namespace CVC4::kind;
 
@@ -374,10 +375,9 @@ bool CegSingleInv::solve()
     siq = nm->mkNode(FORALL, siq[0], siq[1], n_attr);
   }
   // solve the single invocation conjecture using a fresh copy of SMT engine
-  SmtEngine siSmt(nm->toExprManager());
-  siSmt.setLogic(smt::currentSmtEngine()->getLogicInfo());
-  siSmt.assertFormula(siq.toExpr());
-  Result r = siSmt.checkSat();
+  std::unique_ptr<SmtEngine> siSmt;
+  initializeSubsolver(siSmt, siq);
+  Result r = siSmt->checkSat();
   Trace("sygus-si") << "Result: " << r << std::endl;
   if (r.asSatisfiabilityResult().isSat() != Result::UNSAT)
   {
@@ -386,7 +386,7 @@ bool CegSingleInv::solve()
   }
   // now, get the instantiations
   std::vector<Expr> qs;
-  siSmt.getInstantiatedQuantifiedFormulas(qs);
+  siSmt->getInstantiatedQuantifiedFormulas(qs);
   Assert(qs.size() <= 1);
   // track the instantiations, as solution construction is based on this
   Trace("sygus-si") << "#instantiated quantified formulas=" << qs.size()
@@ -398,7 +398,7 @@ bool CegSingleInv::solve()
     TNode qn = Node::fromExpr(q);
     Assert(qn.getKind() == FORALL);
     std::vector<std::vector<Expr> > tvecs;
-    siSmt.getInstantiationTermVectors(q, tvecs);
+    siSmt->getInstantiationTermVectors(q, tvecs);
     Trace("sygus-si") << "#instantiations of " << q << "=" << tvecs.size()
                       << std::endl;
     std::vector<Node> vars;
diff --git a/src/theory/quantifiers/sygus/cegis_core_connective.cpp b/src/theory/quantifiers/sygus/cegis_core_connective.cpp
index 5784e42c0..de75af083 100644
--- a/src/theory/quantifiers/sygus/cegis_core_connective.cpp
+++ b/src/theory/quantifiers/sygus/cegis_core_connective.cpp
@@ -735,9 +735,8 @@ Node CegisCoreConnective::constructSolutionFromPool(Component& ccheck,
   {
     addSuccess = false;
     // try a new core
-    std::unique_ptr<SmtEngine> checkSol(
-        new SmtEngine(NodeManager::currentNM()->toExprManager()));
-    initializeSubsolver(checkSol.get());
+    std::unique_ptr<SmtEngine> checkSol;
+    initializeSubsolver(checkSol);
     Trace("sygus-ccore") << "----- Check candidate " << an << std::endl;
     std::vector<Node> rasserts = asserts;
     rasserts.push_back(d_sc);
@@ -776,9 +775,8 @@ Node CegisCoreConnective::constructSolutionFromPool(Component& ccheck,
         {
           // In terms of Variant #2, this is the check "if S ^ U is unsat"
           Trace("sygus-ccore") << "----- Check side condition" << std::endl;
-          std::unique_ptr<SmtEngine> checkSc(
-              new SmtEngine(NodeManager::currentNM()->toExprManager()));
-          initializeSubsolver(checkSc.get());
+          std::unique_ptr<SmtEngine> checkSc;
+          initializeSubsolver(checkSc);
           std::vector<Node> scasserts;
           scasserts.insert(scasserts.end(), uasserts.begin(), uasserts.end());
           scasserts.push_back(d_sc);
diff --git a/src/theory/quantifiers/sygus/sygus_repair_const.cpp b/src/theory/quantifiers/sygus/sygus_repair_const.cpp
index d34903805..e411dcf2f 100644
--- a/src/theory/quantifiers/sygus/sygus_repair_const.cpp
+++ b/src/theory/quantifiers/sygus/sygus_repair_const.cpp
@@ -177,7 +177,6 @@ bool SygusRepairConst::repairSolution(Node sygusBody,
     return false;
   }
 
-  NodeManager* nm = NodeManager::currentNM();
   Trace("sygus-repair-const") << "Get first-order query..." << std::endl;
   Node fo_body =
       getFoQuery(sygusBody, candidates, candidate_skeletons, sk_vars);
@@ -229,48 +228,17 @@ bool SygusRepairConst::repairSolution(Node sygusBody,
 
   Trace("sygus-engine") << "Repairing previous solution..." << std::endl;
   // make the satisfiability query
-  //
-  // !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
-  // 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.
-  // !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
-  bool needExport = true;
-  std::unique_ptr<SmtEngine> simpleSmte;
-  std::unique_ptr<api::Solver> slv;
-  ExprManager* em = nullptr;
-  SmtEngine* repcChecker = nullptr;
-  ExprManagerMapCollection varMap;
-
-  if (options::sygusRepairConstTimeout.wasSetByUser())
-  {
-    // To support a separate timeout for the subsolver, we need to create
-    // a separate ExprManager with its own options. This requires that
-    // the expressions sent to the subsolver can be exported from on
-    // ExprManager to another.
-    slv.reset(new api::Solver(&nm->getOptions()));
-    em = slv->getExprManager();
-    repcChecker = slv->getSmtEngine();
-    initializeSubsolverWithExport(repcChecker,
-                                  em,
-                                  varMap,
-                                  fo_body.toExpr(),
-                                  true,
-                                  options::sygusRepairConstTimeout());
-    // renable options disabled by sygus
-    repcChecker->setOption("miniscope-quant", true);
-    repcChecker->setOption("miniscope-quant-fv", true);
-    repcChecker->setOption("quant-split", true);
-  }
-  else
-  {
-    needExport = false;
-    em = nm->toExprManager();
-    simpleSmte.reset(new SmtEngine(em));
-    repcChecker = simpleSmte.get();
-    initializeSubsolver(repcChecker, fo_body.toExpr());
-  }
-
+  std::unique_ptr<SmtEngine> repcChecker;
+  // initialize the subsolver using the standard method
+  initializeSubsolver(repcChecker,
+                      fo_body.toExpr(),
+                      options::sygusRepairConstTimeout.wasSetByUser(),
+                      options::sygusRepairConstTimeout());
+  // renable options disabled by sygus
+  repcChecker->setOption("miniscope-quant", true);
+  repcChecker->setOption("miniscope-quant-fv", true);
+  repcChecker->setOption("quant-split", true);
+  // check satisfiability
   Result r = repcChecker->checkSat();
   Trace("sygus-repair-const") << "...got : " << r << std::endl;
   if (r.asSatisfiabilityResult().isSat() == Result::UNSAT
@@ -284,17 +252,7 @@ bool SygusRepairConst::repairSolution(Node sygusBody,
   {
     Assert(d_sk_to_fo.find(v) != d_sk_to_fo.end());
     Node fov = d_sk_to_fo[v];
-    Node fov_m;
-    if (needExport)
-    {
-      Expr e_fov = fov.toExpr().exportTo(em, varMap);
-      fov_m = Node::fromExpr(
-          repcChecker->getValue(e_fov).exportTo(nm->toExprManager(), varMap));
-    }
-    else
-    {
-      fov_m = Node::fromExpr(repcChecker->getValue(fov.toExpr()));
-    }
+    Node fov_m = Node::fromExpr(repcChecker->getValue(fov.toExpr()));
     Trace("sygus-repair-const") << "  " << fov << " = " << fov_m << std::endl;
     // convert to sygus
     Node fov_m_to_sygus = d_tds->getProxyVariable(v.getType(), fov_m);
diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp
index 7e6e74209..a28e76d90 100644
--- a/src/theory/quantifiers/sygus/synth_conjecture.cpp
+++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp
@@ -20,6 +20,7 @@
 #include "options/quantifiers_options.h"
 #include "printer/printer.h"
 #include "prop/prop_engine.h"
+#include "smt/smt_engine_scope.h"
 #include "smt/smt_statistics_registry.h"
 #include "theory/datatypes/sygus_datatype_utils.h"
 #include "theory/quantifiers/first_order_model.h"
@@ -1003,8 +1004,8 @@ void SynthConjecture::printAndContinueStream(const std::vector<Node>& enums,
   // we have generated a solution, print it
   // get the current output stream
   // this output stream should coincide with wherever --dump-synth is output on
-  Options& nodeManagerOptions = NodeManager::currentNM()->getOptions();
-  printSynthSolution(*nodeManagerOptions.getOut());
+  Options& sopts = smt::currentSmtEngine()->getOptions();
+  printSynthSolution(*sopts.getOut());
   excludeCurrentSolution(enums, values);
 }
 
diff --git a/src/theory/quantifiers/sygus/synth_engine.cpp b/src/theory/quantifiers/sygus/synth_engine.cpp
index 590fdaa56..f8349c834 100644
--- a/src/theory/quantifiers/sygus/synth_engine.cpp
+++ b/src/theory/quantifiers/sygus/synth_engine.cpp
@@ -169,9 +169,8 @@ void SynthEngine::assignConjecture(Node q)
     if (!sip.isPurelySingleInvocation() && sip.isNonGroundSingleInvocation())
     {
       // create new smt engine to do quantifier elimination
-      std::unique_ptr<SmtEngine> smt_qe(
-          new SmtEngine(NodeManager::currentNM()->toExprManager()));
-      initializeSubsolver(smt_qe.get());
+      std::unique_ptr<SmtEngine> smt_qe;
+      initializeSubsolver(smt_qe);
       Trace("cegqi-qep") << "Property is non-ground single invocation, run "
                             "QE to obtain single invocation."
                          << std::endl;
diff --git a/src/theory/quantifiers/sygus_sampler.cpp b/src/theory/quantifiers/sygus_sampler.cpp
index 7ad2c54eb..7773b05d5 100644
--- a/src/theory/quantifiers/sygus_sampler.cpp
+++ b/src/theory/quantifiers/sygus_sampler.cpp
@@ -19,6 +19,8 @@
 #include "options/base_options.h"
 #include "options/quantifiers_options.h"
 #include "printer/printer.h"
+#include "smt/smt_engine.h"
+#include "smt/smt_engine_scope.h"
 #include "theory/quantifiers/lazy_trie.h"
 #include "util/bitvector.h"
 #include "util/random.h"
@@ -820,8 +822,8 @@ void SygusSampler::checkEquivalent(Node bv, Node bvr)
       return;
     }
     // we have detected unsoundness in the rewriter
-    Options& nodeManagerOptions = NodeManager::currentNM()->getOptions();
-    std::ostream* out = nodeManagerOptions.getOut();
+    Options& sopts = smt::currentSmtEngine()->getOptions();
+    std::ostream* out = sopts.getOut();
     (*out) << "(unsound-rewrite " << bv << " " << bvr << ")" << std::endl;
     // debugging information
     (*out) << "Terms are not equivalent for : " << std::endl;