diff options
| -rw-r--r-- | src/preprocessing/passes/sygus_inference.cpp | 12 | ||||
| -rw-r--r-- | src/theory/quantifiers/expr_miner.cpp | 10 | ||||
| -rw-r--r-- | src/theory/quantifiers/sygus/ce_guided_single_inv.cpp | 3 | ||||
| -rw-r--r-- | src/theory/quantifiers/sygus/sygus_repair_const.cpp | 2 | ||||
| -rw-r--r-- | src/theory/smt_engine_subsolver.cpp | 11 | ||||
| -rw-r--r-- | src/theory/smt_engine_subsolver.h | 2 |
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); |