Make ExprManager constructor private (#4669)

This commit makes the ExprManager constructor private and updates the
initialization of subsolvers, unit tests, and system tests accordingly.
This is a step towards making options part of SmtEngine instead of
NodeManager.

8 files changed, 86 insertions, 71 deletions

diff --git a/src/theory/quantifiers/candidate_rewrite_database.cpp b/src/theory/quantifiers/candidate_rewrite_database.cpp
index 0454b6412..fc3474df4 100644
--- a/src/theory/quantifiers/candidate_rewrite_database.cpp
+++ b/src/theory/quantifiers/candidate_rewrite_database.cpp
@@ -14,6 +14,7 @@
 
 #include "theory/quantifiers/candidate_rewrite_database.h"
 
+#include "api/cvc4cpp.h"
 #include "options/base_options.h"
 #include "options/quantifiers_options.h"
 #include "printer/printer.h"
@@ -137,8 +138,15 @@ bool CandidateRewriteDatabase::addTerm(Node sol,
         // options as the SmtEngine we belong to, where we ensure that
         // produce-models is set.
         bool needExport = false;
-        ExprManager em(nm->getOptions());
-        std::unique_ptr<SmtEngine> rrChecker;
+
+        // !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
+        // 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);
         Result r = rrChecker->checkSat();
@@ -175,7 +183,7 @@ bool CandidateRewriteDatabase::addTerm(Node sol,
               Assert(!refv.isNull() && refv.getKind() != BOUND_VARIABLE);
               if (needExport)
               {
-                Expr erefv = refv.toExpr().exportTo(&em, varMap);
+                Expr erefv = refv.toExpr().exportTo(em, varMap);
                 val = Node::fromExpr(rrChecker->getValue(erefv).exportTo(
                     nm->toExprManager(), varMap));
               }
diff --git a/src/theory/quantifiers/expr_miner.cpp b/src/theory/quantifiers/expr_miner.cpp
index 01a46d84a..b209fc6ff 100644
--- a/src/theory/quantifiers/expr_miner.cpp
+++ b/src/theory/quantifiers/expr_miner.cpp
@@ -14,6 +14,7 @@
 
 #include "theory/quantifiers/expr_miner.h"
 
+#include "api/cvc4cpp.h"
 #include "options/quantifiers_options.h"
 #include "smt/smt_engine.h"
 #include "smt/smt_engine_scope.h"
@@ -68,8 +69,8 @@ Node ExprMiner::convertToSkolem(Node n)
   return n.substitute(sfvs.begin(), sfvs.end(), sks.begin(), sks.end());
 }
 
-void ExprMiner::initializeChecker(std::unique_ptr<SmtEngine>& checker,
-                                  ExprManager& em,
+void ExprMiner::initializeChecker(SmtEngine* checker,
+                                  ExprManager* em,
                                   ExprManagerMapCollection& varMap,
                                   Node query,
                                   bool& needExport)
@@ -110,10 +111,16 @@ 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;
-  ExprManager em(nm->getOptions());
-  std::unique_ptr<SmtEngine> smte;
+  api::Solver slv(&nm->getOptions());
+  ExprManager* em = slv.getExprManager();
+  SmtEngine* smte = slv.getSmtEngine();
   ExprManagerMapCollection varMap;
   initializeChecker(smte, em, varMap, queryr, needExport);
   return smte->checkSat();
diff --git a/src/theory/quantifiers/expr_miner.h b/src/theory/quantifiers/expr_miner.h
index d69ef45b4..eebcebf88 100644
--- a/src/theory/quantifiers/expr_miner.h
+++ b/src/theory/quantifiers/expr_miner.h
@@ -89,8 +89,8 @@ class ExprMiner
    * (for instance, model values) must be exported to the current expression
    * manager.
    */
-  void initializeChecker(std::unique_ptr<SmtEngine>& smte,
-                         ExprManager& em,
+  void initializeChecker(SmtEngine* smte,
+                         ExprManager* em,
                          ExprManagerMapCollection& varMap,
                          Node query,
                          bool& needExport);
diff --git a/src/theory/quantifiers/query_generator.cpp b/src/theory/quantifiers/query_generator.cpp
index 9f08ebec7..4cf65b24a 100644
--- a/src/theory/quantifiers/query_generator.cpp
+++ b/src/theory/quantifiers/query_generator.cpp
@@ -16,6 +16,8 @@
 #include "theory/quantifiers/query_generator.h"
 
 #include <fstream>
+
+#include "api/cvc4cpp.h"
 #include "options/quantifiers_options.h"
 #include "smt/smt_engine.h"
 #include "smt/smt_engine_scope.h"
@@ -157,9 +159,16 @@ void QueryGenerator::checkQuery(Node qy, unsigned spIndex)
     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;
-    ExprManager em(nm->getOptions());
-    std::unique_ptr<SmtEngine> queryChecker;
+    api::Solver slv(&nm->getOptions());
+    ExprManager* em = slv.getExprManager();
+    SmtEngine* queryChecker = slv.getSmtEngine();
     ExprManagerMapCollection varMap;
     initializeChecker(queryChecker, em, varMap, qy, needExport);
     Result r = queryChecker->checkSat();
diff --git a/src/theory/quantifiers/sygus/cegis_core_connective.cpp b/src/theory/quantifiers/sygus/cegis_core_connective.cpp
index de75af083..5784e42c0 100644
--- a/src/theory/quantifiers/sygus/cegis_core_connective.cpp
+++ b/src/theory/quantifiers/sygus/cegis_core_connective.cpp
@@ -735,8 +735,9 @@ Node CegisCoreConnective::constructSolutionFromPool(Component& ccheck,
   {
     addSuccess = false;
     // try a new core
-    std::unique_ptr<SmtEngine> checkSol;
-    initializeSubsolver(checkSol);
+    std::unique_ptr<SmtEngine> checkSol(
+        new SmtEngine(NodeManager::currentNM()->toExprManager()));
+    initializeSubsolver(checkSol.get());
     Trace("sygus-ccore") << "----- Check candidate " << an << std::endl;
     std::vector<Node> rasserts = asserts;
     rasserts.push_back(d_sc);
@@ -775,8 +776,9 @@ 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;
-          initializeSubsolver(checkSc);
+          std::unique_ptr<SmtEngine> checkSc(
+              new SmtEngine(NodeManager::currentNM()->toExprManager()));
+          initializeSubsolver(checkSc.get());
           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 1c34bd73a..d34903805 100644
--- a/src/theory/quantifiers/sygus/sygus_repair_const.cpp
+++ b/src/theory/quantifiers/sygus/sygus_repair_const.cpp
@@ -14,6 +14,7 @@
 
 #include "theory/quantifiers/sygus/sygus_repair_const.h"
 
+#include "api/cvc4cpp.h"
 #include "options/base_options.h"
 #include "options/quantifiers_options.h"
 #include "printer/printer.h"
@@ -100,36 +101,6 @@ bool SygusRepairConst::isActive() const
   return !d_base_inst.isNull() && d_allow_constant_grammar;
 }
 
-void SygusRepairConst::initializeChecker(std::unique_ptr<SmtEngine>& checker,
-                                         ExprManager& em,
-                                         ExprManagerMapCollection& varMap,
-                                         Node query,
-                                         bool& needExport)
-{
-  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.
-    initializeSubsolverWithExport(checker,
-                                  em,
-                                  varMap,
-                                  query.toExpr(),
-                                  true,
-                                  options::sygusRepairConstTimeout());
-    // renable options disabled by sygus
-    checker->setOption("miniscope-quant", true);
-    checker->setOption("miniscope-quant-fv", true);
-    checker->setOption("quant-split", true);
-  }
-  else
-  {
-    needExport = false;
-    initializeSubsolver(checker, query.toExpr());
-  }
-}
-
 bool SygusRepairConst::repairSolution(const std::vector<Node>& candidates,
                                       const std::vector<Node>& candidate_values,
                                       std::vector<Node>& repair_cv,
@@ -258,11 +229,48 @@ 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;
-  ExprManager em(nm->getOptions());
-  std::unique_ptr<SmtEngine> repcChecker;
-  initializeChecker(repcChecker, em, varMap, fo_body, needExport);
+
+  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());
+  }
+
   Result r = repcChecker->checkSat();
   Trace("sygus-repair-const") << "...got : " << r << std::endl;
   if (r.asSatisfiabilityResult().isSat() == Result::UNSAT
@@ -279,7 +287,7 @@ bool SygusRepairConst::repairSolution(Node sygusBody,
     Node fov_m;
     if (needExport)
     {
-      Expr e_fov = fov.toExpr().exportTo(&em, varMap);
+      Expr e_fov = fov.toExpr().exportTo(em, varMap);
       fov_m = Node::fromExpr(
           repcChecker->getValue(e_fov).exportTo(nm->toExprManager(), varMap));
     }
diff --git a/src/theory/quantifiers/sygus/sygus_repair_const.h b/src/theory/quantifiers/sygus/sygus_repair_const.h
index dc721b42d..e02ca1f3e 100644
--- a/src/theory/quantifiers/sygus/sygus_repair_const.h
+++ b/src/theory/quantifiers/sygus/sygus_repair_const.h
@@ -209,26 +209,6 @@ class SygusRepairConst
    * If n is in the given logic, this method returns true.
    */
   bool getFitToLogicExcludeVar(LogicInfo& logic, Node n, Node& exvar);
-  /** initialize checker
-   *
-   * This function initializes the smt engine checker to check the
-   * satisfiability of the argument "query"
-   *
-   * The arguments em and varMap are used for supporting cases where we
-   * want checker 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 checker 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(std::unique_ptr<SmtEngine>& checker,
-                         ExprManager& em,
-                         ExprManagerMapCollection& varMap,
-                         Node query,
-                         bool& needExport);
 };
 
 } /* CVC4::theory::quantifiers namespace */
diff --git a/src/theory/quantifiers/sygus/synth_engine.cpp b/src/theory/quantifiers/sygus/synth_engine.cpp
index f8349c834..590fdaa56 100644
--- a/src/theory/quantifiers/sygus/synth_engine.cpp
+++ b/src/theory/quantifiers/sygus/synth_engine.cpp
@@ -169,8 +169,9 @@ void SynthEngine::assignConjecture(Node q)
     if (!sip.isPurelySingleInvocation() && sip.isNonGroundSingleInvocation())
     {
       // create new smt engine to do quantifier elimination
-      std::unique_ptr<SmtEngine> smt_qe;
-      initializeSubsolver(smt_qe);
+      std::unique_ptr<SmtEngine> smt_qe(
+          new SmtEngine(NodeManager::currentNM()->toExprManager()));
+      initializeSubsolver(smt_qe.get());
       Trace("cegqi-qep") << "Property is non-ground single invocation, run "
                             "QE to obtain single invocation."
                          << std::endl;