From 34043bdcd93860969cfd9e87c683340175c640b9 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 14 Jul 2020 01:00:00 -0500 Subject: 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. --- src/theory/quantifiers/expr_miner.cpp | 10 ++++++---- src/theory/quantifiers/sygus/ce_guided_single_inv.cpp | 3 ++- src/theory/quantifiers/sygus/sygus_repair_const.cpp | 2 +- 3 files changed, 9 insertions(+), 6 deletions(-) (limited to 'src/theory/quantifiers') 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& 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 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 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; -- cgit v1.2.3