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.

diff --git a/src/preprocessing/passes/sygus_inference.cpp b/src/preprocessing/passes/sygus_inference.cpp
index 4500c78803a5674b57fe8c50b269744028b739ca..31f9273599903652a730cbd49e665a09d5353793 100644 (file)
--- 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 6153242e762dfa32bbaacd7f82654689b814f107..00a627adff8758c2039bfd2df77fdaeb13a8dd8e 100644 (file)
--- 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 d0cac6d5846ecd54e83a212745432ba140572f88..0612c85f8ba7eed18f31e7d8651a9cce28957cfe 100644 (file)
--- 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 e411dcf2ff9349ee86f07e594c88bb8df6d8f328..cff8f581dc19325a73ccf1cb9bfa58a8d47dcdf6 100644 (file)
--- 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 45c115524767c849377405eee4d0a8a08ced122a..863d1ab865286bc96d85edd9b3f5af1eb18a2fc5 100644 (file)
--- 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 64646ac052ef132421c49dfc752c929761fa1c16..cbc871cce2b941b811e22fb008af830b002fc7aa 100644 (file)
--- 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);