Minor refactoring of subsolver initialization (#4731)

This decouples asserting a formula with initialization (previously it was a complex process to assert a formula due to having to clone/export to a new ExprManager). Now it is trivial.

This commit fixes an unintended consequence of the previous complications. Previously, SmtEngine::setOption would be set after asserting formulas to an SmtEngine subsolver, which is technically incorrect, as options should be finalized before the first assert.

This is required for further cleaning up of options listeners.

6 files changed, 19 insertions, 21 deletions

diff --git a/src/preprocessing/passes/sygus_inference.cpp b/src/preprocessing/passes/sygus_inference.cpp
index 4500c7880..31f927359 100644
--- a/src/preprocessing/passes/sygus_inference.cpp
+++ b/src/preprocessing/passes/sygus_inference.cpp
@@ -20,6 +20,7 @@
 #include "theory/quantifiers/quantifiers_attributes.h"
 #include "theory/quantifiers/quantifiers_rewriter.h"
 #include "theory/quantifiers/sygus/sygus_grammar_cons.h"
+#include "theory/smt_engine_subsolver.h"
 
 using namespace std;
 using namespace CVC4::kind;
@@ -300,12 +301,11 @@ bool SygusInference::solveSygus(std::vector<Node>& assertions,
   Trace("sygus-infer") << "*** Return sygus inference : " << body << std::endl;
 
   // make a separate smt call
-  SmtEngine* currSmt = smt::currentSmtEngine();
-  SmtEngine rrSygus(nm->toExprManager(), &currSmt->getOptions());
-  rrSygus.setLogic(currSmt->getLogicInfo());
-  rrSygus.assertFormula(body.toExpr());
+  std::unique_ptr<SmtEngine> rrSygus;
+  theory::initializeSubsolver(rrSygus);
+  rrSygus->assertFormula(body.toExpr());
   Trace("sygus-infer") << "*** Check sat..." << std::endl;
-  Result r = rrSygus.checkSat();
+  Result r = rrSygus->checkSat();
   Trace("sygus-infer") << "...result : " << r << std::endl;
   if (r.asSatisfiabilityResult().isSat() != Result::UNSAT)
   {
@@ -314,7 +314,7 @@ bool SygusInference::solveSygus(std::vector<Node>& assertions,
   }
   // get the synthesis solutions
   std::map<Expr, Expr> synth_sols;
-  rrSygus.getSynthSolutions(synth_sols);
+  rrSygus->getSynthSolutions(synth_sols);
 
   std::vector<Node> final_ff;
   std::vector<Node> final_ff_sol;
diff --git a/src/theory/quantifiers/expr_miner.cpp b/src/theory/quantifiers/expr_miner.cpp
index 6153242e7..00a627adf 100644
--- a/src/theory/quantifiers/expr_miner.cpp
+++ b/src/theory/quantifiers/expr_miner.cpp
@@ -72,13 +72,15 @@ Node ExprMiner::convertToSkolem(Node n)
 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);
-  initializeSubsolver(checker, squery.toExpr());
+  Assert (!query.isNull());
+  initializeSubsolver(checker);
   // also set the options
   checker->setOption("sygus-rr-synth-input", false);
   checker->setOption("input-language", "smt2");
+  // Convert bound variables to skolems. This ensures the satisfiability
+  // check is ground.
+  Node squery = convertToSkolem(query);
+  checker->assertFormula(squery.toExpr());
 }
 
 Result ExprMiner::doCheck(Node query)
diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
index d0cac6d58..0612c85f8 100644
--- a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
+++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
@@ -376,7 +376,8 @@ bool CegSingleInv::solve()
   }
   // solve the single invocation conjecture using a fresh copy of SMT engine
   std::unique_ptr<SmtEngine> siSmt;
-  initializeSubsolver(siSmt, siq);
+  initializeSubsolver(siSmt);
+  siSmt->assertFormula(siq.toExpr());
   Result r = siSmt->checkSat();
   Trace("sygus-si") << "Result: " << r << std::endl;
   if (r.asSatisfiabilityResult().isSat() != Result::UNSAT)
diff --git a/src/theory/quantifiers/sygus/sygus_repair_const.cpp b/src/theory/quantifiers/sygus/sygus_repair_const.cpp
index e411dcf2f..cff8f581d 100644
--- a/src/theory/quantifiers/sygus/sygus_repair_const.cpp
+++ b/src/theory/quantifiers/sygus/sygus_repair_const.cpp
@@ -231,13 +231,13 @@ bool SygusRepairConst::repairSolution(Node sygusBody,
   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);
+  repcChecker->assertFormula(fo_body.toExpr());
   // check satisfiability
   Result r = repcChecker->checkSat();
   Trace("sygus-repair-const") << "...got : " << r << std::endl;
diff --git a/src/theory/smt_engine_subsolver.cpp b/src/theory/smt_engine_subsolver.cpp
index 45c115524..863d1ab86 100644
--- a/src/theory/smt_engine_subsolver.cpp
+++ b/src/theory/smt_engine_subsolver.cpp
@@ -42,7 +42,6 @@ Result quickCheck(Node& query)
 }
 
 void initializeSubsolver(std::unique_ptr<SmtEngine>& smte,
-                         Node query,
                          bool needsTimeout,
                          unsigned long timeout)
 {
@@ -57,10 +56,6 @@ void initializeSubsolver(std::unique_ptr<SmtEngine>& smte,
     smte->setTimeLimit(timeout, true);
   }
   smte->setLogic(smt::currentSmtEngine()->getLogicInfo());
-  if (!query.isNull())
-  {
-    smte->assertFormula(query.toExpr());
-  }
 }
 
 Result checkWithSubsolver(std::unique_ptr<SmtEngine>& smte,
@@ -74,7 +69,8 @@ Result checkWithSubsolver(std::unique_ptr<SmtEngine>& smte,
   {
     return r;
   }
-  initializeSubsolver(smte, query, needsTimeout, timeout);
+  initializeSubsolver(smte, needsTimeout, timeout);
+  smte->assertFormula(query.toExpr());
   return smte->checkSat();
 }
 
@@ -109,7 +105,8 @@ Result checkWithSubsolver(Node query,
     return r;
   }
   std::unique_ptr<SmtEngine> smte;
-  initializeSubsolver(smte, query, needsTimeout, timeout);
+  initializeSubsolver(smte, needsTimeout, timeout);
+  smte->assertFormula(query.toExpr());
   r = smte->checkSat();
   if (r.asSatisfiabilityResult().isSat() == Result::SAT)
   {
diff --git a/src/theory/smt_engine_subsolver.h b/src/theory/smt_engine_subsolver.h
index 64646ac05..cbc871cce 100644
--- a/src/theory/smt_engine_subsolver.h
+++ b/src/theory/smt_engine_subsolver.h
@@ -35,12 +35,10 @@ namespace theory {
  * of the argument "query".
  *
  * @param smte The smt engine pointer to initialize
- * @param query The query to check (if provided)
  * @param needsTimeout Whether we would like to set a timeout
  * @param timeout The timeout (in milliseconds)
  */
 void initializeSubsolver(std::unique_ptr<SmtEngine>& smte,
-                         Node query = Node::null(),
                          bool needsTimeout = false,
                          unsigned long timeout = 0);