From 21fa888738ea77e4436ef164c184e61683a55fb5 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 26 Aug 2021 11:55:59 -0500 Subject: [PATCH] Eliminate currentSmtEngine for subsolver calls (#7068) This eliminates another occurrence of smt::currentSmtEngine by making it required to pass options + logic for all subsolver calls. --- src/preprocessing/passes/sygus_inference.cpp | 4 +- .../preprocessing_pass_context.cpp | 9 ++++- .../preprocessing_pass_context.h | 6 ++- src/smt/abduction_solver.cpp | 11 ++++-- src/smt/abduction_solver.h | 5 ++- src/smt/env.cpp | 2 +- src/smt/env.h | 2 +- src/smt/interpolation_solver.cpp | 9 +++-- src/smt/interpolation_solver.h | 5 ++- src/smt/optimization_solver.cpp | 9 ++++- src/smt/optimization_solver.h | 3 ++ src/smt/quant_elim_solver.cpp | 7 +++- src/smt/quant_elim_solver.h | 6 ++- src/smt/smt_engine.cpp | 20 +++++----- src/smt/smt_engine.h | 2 +- src/smt/sygus_solver.cpp | 15 +++----- src/smt/sygus_solver.h | 9 ++--- .../quantifiers/cegqi/inst_strategy_cegqi.cpp | 2 +- src/theory/quantifiers/cegqi/nested_qe.cpp | 15 ++++---- src/theory/quantifiers/cegqi/nested_qe.h | 11 ++++-- src/theory/quantifiers/expr_miner.cpp | 8 ++-- .../sygus/ce_guided_single_inv.cpp | 5 ++- .../quantifiers/sygus/ce_guided_single_inv.h | 2 + src/theory/quantifiers/sygus/cegis.cpp | 5 ++- src/theory/quantifiers/sygus/cegis.h | 5 ++- .../sygus/cegis_core_connective.cpp | 13 ++++--- .../quantifiers/sygus/cegis_core_connective.h | 3 +- src/theory/quantifiers/sygus/cegis_unif.cpp | 2 +- .../quantifiers/sygus/sygus_interpol.cpp | 5 ++- src/theory/quantifiers/sygus/sygus_interpol.h | 6 ++- src/theory/quantifiers/sygus/sygus_module.cpp | 5 ++- src/theory/quantifiers/sygus/sygus_module.h | 6 ++- src/theory/quantifiers/sygus/sygus_pbe.cpp | 5 ++- src/theory/quantifiers/sygus/sygus_pbe.h | 3 +- .../quantifiers/sygus/sygus_qe_preproc.cpp | 4 +- .../quantifiers/sygus/sygus_qe_preproc.h | 9 ++++- .../quantifiers/sygus/sygus_repair_const.cpp | 3 +- .../quantifiers/sygus/synth_conjecture.cpp | 11 +++--- src/theory/quantifiers/sygus/synth_engine.cpp | 2 +- src/theory/quantifiers/sygus/synth_verify.cpp | 7 +++- src/theory/quantifiers/sygus/synth_verify.h | 6 ++- src/theory/smt_engine_subsolver.cpp | 37 +++++++++++-------- src/theory/smt_engine_subsolver.h | 26 ++++++++++--- 43 files changed, 212 insertions(+), 118 deletions(-) diff --git a/src/preprocessing/passes/sygus_inference.cpp b/src/preprocessing/passes/sygus_inference.cpp index 33a2e38d9..c0cddda5e 100644 --- a/src/preprocessing/passes/sygus_inference.cpp +++ b/src/preprocessing/passes/sygus_inference.cpp @@ -295,7 +295,9 @@ bool SygusInference::solveSygus(const std::vector& assertions, // make a separate smt call std::unique_ptr rrSygus; - theory::initializeSubsolver(rrSygus); + theory::initializeSubsolver(rrSygus, + d_preprocContext->getOptions(), + d_preprocContext->getLogicInfo()); rrSygus->assertFormula(body); Trace("sygus-infer") << "*** Check sat..." << std::endl; Result r = rrSygus->checkSat(); diff --git a/src/preprocessing/preprocessing_pass_context.cpp b/src/preprocessing/preprocessing_pass_context.cpp index b21fcb261..7fefafce6 100644 --- a/src/preprocessing/preprocessing_pass_context.cpp +++ b/src/preprocessing/preprocessing_pass_context.cpp @@ -36,7 +36,14 @@ PreprocessingPassContext::PreprocessingPassContext( d_symsInAssertions(env.getUserContext()) { } - +const Options& PreprocessingPassContext::getOptions() +{ + return d_env.getOptions(); +} +const LogicInfo& PreprocessingPassContext::getLogicInfo() +{ + return d_env.getLogicInfo(); +} theory::TrustSubstitutionMap& PreprocessingPassContext::getTopLevelSubstitutions() { diff --git a/src/preprocessing/preprocessing_pass_context.h b/src/preprocessing/preprocessing_pass_context.h index 1af73e453..aab1b453d 100644 --- a/src/preprocessing/preprocessing_pass_context.h +++ b/src/preprocessing/preprocessing_pass_context.h @@ -61,8 +61,10 @@ class PreprocessingPassContext void spendResource(Resource r); - /** Get the current logic info of the SmtEngine */ - const LogicInfo& getLogicInfo() { return d_smt->getLogicInfo(); } + /** Get the options of the environment */ + const Options& getOptions(); + /** Get the current logic info of the environment */ + const LogicInfo& getLogicInfo(); /** Gets a reference to the top-level substitution map */ theory::TrustSubstitutionMap& getTopLevelSubstitutions(); diff --git a/src/smt/abduction_solver.cpp b/src/smt/abduction_solver.cpp index ff1337fe1..b773d8d57 100644 --- a/src/smt/abduction_solver.cpp +++ b/src/smt/abduction_solver.cpp @@ -32,7 +32,10 @@ using namespace cvc5::theory; namespace cvc5 { namespace smt { -AbductionSolver::AbductionSolver(SmtEngine* parent) : d_parent(parent) {} +AbductionSolver::AbductionSolver(Env& env, SmtEngine* parent) + : d_env(env), d_parent(parent) +{ +} AbductionSolver::~AbductionSolver() {} bool AbductionSolver::getAbduct(const Node& goal, @@ -48,7 +51,7 @@ bool AbductionSolver::getAbduct(const Node& goal, std::vector axioms = d_parent->getExpandedAssertions(); std::vector asserts(axioms.begin(), axioms.end()); // must expand definitions - Node conjn = d_parent->getEnv().getTopLevelSubstitutions().apply(goal); + Node conjn = d_env.getTopLevelSubstitutions().apply(goal); // now negate conjn = conjn.negate(); d_abdConj = conjn; @@ -63,7 +66,7 @@ bool AbductionSolver::getAbduct(const Node& goal, Trace("sygus-abduct") << "SmtEngine::getAbduct: made conjecture : " << aconj << ", solving for " << d_sssf << std::endl; // we generate a new smt engine to do the abduction query - initializeSubsolver(d_subsolver); + initializeSubsolver(d_subsolver, d_env); // get the logic LogicInfo l = d_subsolver->getLogicInfo().getUnlockedCopy(); // enable everything needed for sygus @@ -153,7 +156,7 @@ void AbductionSolver::checkAbduct(Node a) << ": make new SMT engine" << std::endl; // Start new SMT engine to check solution std::unique_ptr abdChecker; - initializeSubsolver(abdChecker); + initializeSubsolver(abdChecker, d_env); Trace("check-abduct") << "SmtEngine::checkAbduct: phase " << j << ": asserting formulas" << std::endl; for (const Node& e : asserts) diff --git a/src/smt/abduction_solver.h b/src/smt/abduction_solver.h index c7f9db035..b408fe060 100644 --- a/src/smt/abduction_solver.h +++ b/src/smt/abduction_solver.h @@ -23,6 +23,7 @@ namespace cvc5 { +class Env; class SmtEngine; namespace smt { @@ -37,7 +38,7 @@ namespace smt { class AbductionSolver { public: - AbductionSolver(SmtEngine* parent); + AbductionSolver(Env& env, SmtEngine* parent); ~AbductionSolver(); /** * This method asks this SMT engine to find an abduct with respect to the @@ -84,6 +85,8 @@ class AbductionSolver * problems. */ bool getAbductInternal(Node& abd); + /** Reference to the env */ + Env& d_env; /** The parent SMT engine */ SmtEngine* d_parent; /** The SMT engine subsolver diff --git a/src/smt/env.cpp b/src/smt/env.cpp index d6677c343..7efefabcd 100644 --- a/src/smt/env.cpp +++ b/src/smt/env.cpp @@ -33,7 +33,7 @@ using namespace cvc5::smt; namespace cvc5 { -Env::Env(NodeManager* nm, Options* opts) +Env::Env(NodeManager* nm, const Options* opts) : d_context(new context::Context()), d_userContext(new context::UserContext()), d_nodeManager(nm), diff --git a/src/smt/env.h b/src/smt/env.h index 68148ec00..7c12c86b9 100644 --- a/src/smt/env.h +++ b/src/smt/env.h @@ -61,7 +61,7 @@ class Env /** * Construct an Env with the given node manager. */ - Env(NodeManager* nm, Options* opts); + Env(NodeManager* nm, const Options* opts); /** Destruct the env. */ ~Env(); diff --git a/src/smt/interpolation_solver.cpp b/src/smt/interpolation_solver.cpp index fbbdb1b90..ab7002205 100644 --- a/src/smt/interpolation_solver.cpp +++ b/src/smt/interpolation_solver.cpp @@ -32,7 +32,8 @@ using namespace cvc5::theory; namespace cvc5 { namespace smt { -InterpolationSolver::InterpolationSolver(SmtEngine* parent) : d_parent(parent) +InterpolationSolver::InterpolationSolver(Env& env, SmtEngine* parent) + : d_env(env), d_parent(parent) { } @@ -52,10 +53,10 @@ bool InterpolationSolver::getInterpol(const Node& conj, << std::endl; std::vector axioms = d_parent->getExpandedAssertions(); // must expand definitions - Node conjn = d_parent->getEnv().getTopLevelSubstitutions().apply(conj); + Node conjn = d_env.getTopLevelSubstitutions().apply(conj); std::string name("A"); - quantifiers::SygusInterpol interpolSolver; + quantifiers::SygusInterpol interpolSolver(d_env); if (interpolSolver.solveInterpolation( name, axioms, conjn, grammarType, interpol)) { @@ -94,7 +95,7 @@ void InterpolationSolver::checkInterpol(Node interpol, << ": make new SMT engine" << std::endl; // Start new SMT engine to check solution std::unique_ptr itpChecker; - initializeSubsolver(itpChecker); + initializeSubsolver(itpChecker, d_env); Trace("check-interpol") << "SmtEngine::checkInterpol: phase " << j << ": asserting formulas" << std::endl; if (j == 0) diff --git a/src/smt/interpolation_solver.h b/src/smt/interpolation_solver.h index 03f8ab6a1..19bb54c61 100644 --- a/src/smt/interpolation_solver.h +++ b/src/smt/interpolation_solver.h @@ -23,6 +23,7 @@ namespace cvc5 { +class Env; class SmtEngine; namespace smt { @@ -37,7 +38,7 @@ namespace smt { class InterpolationSolver { public: - InterpolationSolver(SmtEngine* parent); + InterpolationSolver(Env& env, SmtEngine* parent); ~InterpolationSolver(); /** @@ -77,6 +78,8 @@ class InterpolationSolver const Node& conj); private: + /** Reference to the env */ + Env& d_env; /** The parent SMT engine */ SmtEngine* d_parent; }; diff --git a/src/smt/optimization_solver.cpp b/src/smt/optimization_solver.cpp index fecf65275..67de9728c 100644 --- a/src/smt/optimization_solver.cpp +++ b/src/smt/optimization_solver.cpp @@ -22,6 +22,7 @@ #include "options/language.h" #include "options/smt_options.h" #include "smt/assertions.h" +#include "smt/env.h" #include "smt/smt_engine.h" #include "theory/smt_engine_subsolver.h" @@ -147,7 +148,8 @@ std::unique_ptr OptimizationSolver::createOptCheckerWithTimeout( std::unique_ptr optChecker; // initializeSubSolver will copy the options and theories enabled // from the current solver to optChecker and adds timeout - theory::initializeSubsolver(optChecker, nullptr, needsTimeout, timeout); + theory::initializeSubsolver( + optChecker, parentSMTSolver->getEnv(), needsTimeout, timeout); // we need to be in incremental mode for multiple objectives since we need to // push pop we need to produce models to inrement on our objective optChecker->setOption("incremental", "true"); @@ -275,7 +277,10 @@ Result OptimizationSolver::optimizeLexicographicIterative() Result OptimizationSolver::optimizeParetoNaiveGIA() { // initial call to Pareto optimizer, create the checker - if (!d_optChecker) d_optChecker = createOptCheckerWithTimeout(d_parent); + if (!d_optChecker) + { + d_optChecker = createOptCheckerWithTimeout(d_parent); + } NodeManager* nm = d_optChecker->getNodeManager(); // checks whether the current set of assertions are satisfied or not diff --git a/src/smt/optimization_solver.h b/src/smt/optimization_solver.h index 339ba9ea7..04a960282 100644 --- a/src/smt/optimization_solver.h +++ b/src/smt/optimization_solver.h @@ -26,6 +26,7 @@ namespace cvc5 { +class Env; class SmtEngine; namespace smt { @@ -254,6 +255,8 @@ class OptimizationSolver private: /** * Initialize an SMT subsolver for offline optimization purpose + * @param env the environment, which determines options and logic for the + * subsolver * @param parentSMTSolver the parental solver containing the assertions * @param needsTimeout specifies whether it needs timeout for each single * query diff --git a/src/smt/quant_elim_solver.cpp b/src/smt/quant_elim_solver.cpp index e675feaa0..087aa0e06 100644 --- a/src/smt/quant_elim_solver.cpp +++ b/src/smt/quant_elim_solver.cpp @@ -32,7 +32,10 @@ using namespace cvc5::kind; namespace cvc5 { namespace smt { -QuantElimSolver::QuantElimSolver(SmtSolver& sms) : d_smtSolver(sms) {} +QuantElimSolver::QuantElimSolver(Env& env, SmtSolver& sms) + : d_env(env), d_smtSolver(sms) +{ +} QuantElimSolver::~QuantElimSolver() {} @@ -51,7 +54,7 @@ Node QuantElimSolver::getQuantifierElimination(Assertions& as, // ensure the body is rewritten q = nm->mkNode(q.getKind(), q[0], Rewriter::rewrite(q[1])); // do nested quantifier elimination if necessary - q = quantifiers::NestedQe::doNestedQe(q, true); + q = quantifiers::NestedQe::doNestedQe(d_env, q, true); Trace("smt-qe") << "QuantElimSolver: after nested quantifier elimination : " << q << std::endl; // tag the quantified formula with the quant-elim attribute diff --git a/src/smt/quant_elim_solver.h b/src/smt/quant_elim_solver.h index 4396694e9..f890deba0 100644 --- a/src/smt/quant_elim_solver.h +++ b/src/smt/quant_elim_solver.h @@ -22,6 +22,8 @@ #include "smt/assertions.h" namespace cvc5 { +class Env; + namespace smt { class SmtSolver; @@ -37,7 +39,7 @@ class SmtSolver; class QuantElimSolver { public: - QuantElimSolver(SmtSolver& sms); + QuantElimSolver(Env& env, SmtSolver& sms); ~QuantElimSolver(); /** @@ -95,6 +97,8 @@ class QuantElimSolver bool isInternalSubsolver); private: + /** Reference to the env */ + Env& d_env; /** The SMT solver, which is used during doQuantifierElimination. */ SmtSolver& d_smtSolver; }; diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 45056057d..ea253e4ef 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -84,7 +84,7 @@ using namespace cvc5::theory; namespace cvc5 { -SmtEngine::SmtEngine(NodeManager* nm, Options* optr) +SmtEngine::SmtEngine(NodeManager* nm, const Options* optr) : d_env(new Env(nm, optr)), d_state(new SmtEngineState(*d_env.get(), *this)), d_absValues(new AbstractValues(getNodeManager())), @@ -131,11 +131,9 @@ SmtEngine::SmtEngine(NodeManager* nm, Options* optr) // make the SMT solver d_smtSolver.reset(new SmtSolver(*d_env.get(), *d_state, *d_pp, *d_stats)); // make the SyGuS solver - d_sygusSolver.reset( - new SygusSolver(*d_smtSolver, *d_pp, getUserContext(), d_outMgr)); + d_sygusSolver.reset(new SygusSolver(*d_env.get(), *d_smtSolver, *d_pp)); // make the quantifier elimination solver - d_quantElimSolver.reset(new QuantElimSolver(*d_smtSolver)); - + d_quantElimSolver.reset(new QuantElimSolver(*d_env.get(), *d_smtSolver)); } bool SmtEngine::isFullyInited() const { return d_state->isFullyInited(); } @@ -259,12 +257,12 @@ void SmtEngine::finishInit() // subsolvers if (d_env->getOptions().smt.produceAbducts) { - d_abductSolver.reset(new AbductionSolver(this)); + d_abductSolver.reset(new AbductionSolver(*d_env.get(), this)); } if (d_env->getOptions().smt.produceInterpols != options::ProduceInterpols::NONE) { - d_interpolSolver.reset(new InterpolationSolver(this)); + d_interpolSolver.reset(new InterpolationSolver(*d_env.get(), this)); } d_pp->finishInit(); @@ -1119,7 +1117,7 @@ Node SmtEngine::getValue(const Node& ex) const Trace("smt") << "SMT getValue(" << ex << ")" << endl; if (Dump.isOn("benchmark")) { - getPrinter().toStreamCmdGetValue(d_outMgr.getDumpOut(), {ex}); + getPrinter().toStreamCmdGetValue(d_env->getDumpOut(), {ex}); } TypeNode expectedType = ex.getType(); @@ -1408,7 +1406,7 @@ std::vector SmtEngine::reduceUnsatCore(const std::vector& core) for (const Node& skip : core) { std::unique_ptr coreChecker; - initializeSubsolver(coreChecker); + initializeSubsolver(coreChecker, *d_env.get()); coreChecker->setLogic(getLogicInfo()); coreChecker->getOptions().smt.checkUnsatCores = false; // disable all proof options @@ -1474,7 +1472,7 @@ void SmtEngine::checkUnsatCore() { // initialize the core checker std::unique_ptr coreChecker; - initializeSubsolver(coreChecker); + initializeSubsolver(coreChecker, *d_env.get()); coreChecker->getOptions().smt.checkUnsatCores = false; // disable all proof options coreChecker->getOptions().smt.produceProofs = false; @@ -1988,7 +1986,7 @@ std::string SmtEngine::getOption(const std::string& key) const if (Dump.isOn("benchmark")) { - getPrinter().toStreamCmdGetOption(d_outMgr.getDumpOut(), key); + getPrinter().toStreamCmdGetOption(d_env->getDumpOut(), key); } if (key == "command-verbosity") diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 208c83db8..d9786f6a1 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -126,7 +126,7 @@ class CVC5_EXPORT SmtEngine * If provided, optr is a pointer to a set of options that should initialize the values * of the options object owned by this class. */ - SmtEngine(NodeManager* nm, Options* optr = nullptr); + SmtEngine(NodeManager* nm, const Options* optr = nullptr); /** Destruct the SMT engine. */ ~SmtEngine(); diff --git a/src/smt/sygus_solver.cpp b/src/smt/sygus_solver.cpp index d5cfe274e..b7b6d9c18 100644 --- a/src/smt/sygus_solver.cpp +++ b/src/smt/sygus_solver.cpp @@ -41,14 +41,11 @@ using namespace cvc5::kind; namespace cvc5 { namespace smt { -SygusSolver::SygusSolver(SmtSolver& sms, - Preprocessor& pp, - context::UserContext* u, - OutputManager& outMgr) - : d_smtSolver(sms), +SygusSolver::SygusSolver(Env& env, SmtSolver& sms, Preprocessor& pp) + : d_env(env), + d_smtSolver(sms), d_pp(pp), - d_sygusConjectureStale(u, true), - d_outMgr(outMgr) + d_sygusConjectureStale(env.getUserContext(), true) { } @@ -212,7 +209,7 @@ Result SygusSolver::checkSynth(Assertions& as) Trace("smt") << "Check synthesis conjecture: " << body << std::endl; if (Dump.isOn("raw-benchmark")) { - d_outMgr.getPrinter().toStreamCmdCheckSynth(d_outMgr.getDumpOut()); + d_env.getPrinter().toStreamCmdCheckSynth(d_env.getDumpOut()); } d_sygusConjectureStale = false; @@ -332,7 +329,7 @@ void SygusSolver::checkSynthSolution(Assertions& as) { // Start new SMT engine to check solutions std::unique_ptr solChecker; - initializeSubsolver(solChecker); + initializeSubsolver(solChecker, d_env); solChecker->getOptions().smt.checkSynthSol = false; solChecker->getOptions().quantifiers.sygusRecFun = false; // get the solution for this conjecture diff --git a/src/smt/sygus_solver.h b/src/smt/sygus_solver.h index ff9b7e513..82dfab3cc 100644 --- a/src/smt/sygus_solver.h +++ b/src/smt/sygus_solver.h @@ -45,10 +45,7 @@ class SmtSolver; class SygusSolver { public: - SygusSolver(SmtSolver& sms, - Preprocessor& pp, - context::UserContext* u, - OutputManager& outMgr); + SygusSolver(Env& env, SmtSolver& sms, Preprocessor& pp); ~SygusSolver(); /** @@ -161,6 +158,8 @@ class SygusSolver * previously not stale. */ void setSygusConjectureStale(); + /** Reference to the env class */ + Env& d_env; /** The SMT solver, which is used during checkSynth. */ SmtSolver& d_smtSolver; /** The preprocessor, used for checkSynthSolution. */ @@ -180,8 +179,6 @@ class SygusSolver * Whether we need to reconstruct the sygus conjecture. */ context::CDO d_sygusConjectureStale; - /** Reference to the output manager of the smt engine */ - OutputManager& d_outMgr; }; } // namespace smt diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp index f65828d2f..81366fabd 100644 --- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp +++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp @@ -70,7 +70,7 @@ InstStrategyCegqi::InstStrategyCegqi(QuantifiersState& qs, } if (options::cegqiNestedQE()) { - d_nestedQe.reset(new NestedQe(qs.getUserContext())); + d_nestedQe.reset(new NestedQe(qs.getEnv())); } } diff --git a/src/theory/quantifiers/cegqi/nested_qe.cpp b/src/theory/quantifiers/cegqi/nested_qe.cpp index a20c37043..869ebe036 100644 --- a/src/theory/quantifiers/cegqi/nested_qe.cpp +++ b/src/theory/quantifiers/cegqi/nested_qe.cpp @@ -18,13 +18,14 @@ #include "expr/node_algorithm.h" #include "expr/subs.h" +#include "smt/env.h" #include "theory/smt_engine_subsolver.h" namespace cvc5 { namespace theory { namespace quantifiers { -NestedQe::NestedQe(context::UserContext* u) : d_qnqe(u) {} +NestedQe::NestedQe(Env& env) : d_env(env), d_qnqe(d_env.getUserContext()) {} bool NestedQe::process(Node q, std::vector& lems) { @@ -35,7 +36,7 @@ bool NestedQe::process(Node q, std::vector& lems) return (*it).second != q; } Trace("cegqi-nested-qe") << "Check nested QE on " << q << std::endl; - Node qqe = doNestedQe(q, true); + Node qqe = doNestedQe(d_env, q, true); d_qnqe[q] = qqe; if (qqe == q) { @@ -67,7 +68,7 @@ bool NestedQe::hasNestedQuantification(Node q) return getNestedQuantification(q, nqs); } -Node NestedQe::doNestedQe(Node q, bool keepTopLevel) +Node NestedQe::doNestedQe(Env& env, Node q, bool keepTopLevel) { NodeManager* nm = NodeManager::currentNM(); Node qOrig = q; @@ -88,7 +89,7 @@ Node NestedQe::doNestedQe(Node q, bool keepTopLevel) return qOrig; } // just do ordinary quantifier elimination - Node qqe = doQe(q); + Node qqe = doQe(env, q); Trace("cegqi-nested-qe-debug") << "...did ordinary qe" << std::endl; return qqe; } @@ -104,7 +105,7 @@ Node NestedQe::doNestedQe(Node q, bool keepTopLevel) for (const Node& nq : nqs) { Node nqk = sk.apply(nq); - Node nqqe = doNestedQe(nqk); + Node nqqe = doNestedQe(env, nqk); if (nqqe == nqk) { // failed @@ -130,14 +131,14 @@ Node NestedQe::doNestedQe(Node q, bool keepTopLevel) return nm->mkNode(inputExists ? kind::EXISTS : kind::FORALL, qargs); } -Node NestedQe::doQe(Node q) +Node NestedQe::doQe(Env& env, Node q) { Assert(q.getKind() == kind::FORALL); Trace("cegqi-nested-qe") << " Apply qe to " << q << std::endl; NodeManager* nm = NodeManager::currentNM(); q = nm->mkNode(kind::EXISTS, q[0], q[1].negate()); std::unique_ptr smt_qe; - initializeSubsolver(smt_qe); + initializeSubsolver(smt_qe, env); Node qqe = smt_qe->getQuantifierElimination(q, true, false); if (expr::hasBoundVar(qqe)) { diff --git a/src/theory/quantifiers/cegqi/nested_qe.h b/src/theory/quantifiers/cegqi/nested_qe.h index f6e15d4c6..f577a504c 100644 --- a/src/theory/quantifiers/cegqi/nested_qe.h +++ b/src/theory/quantifiers/cegqi/nested_qe.h @@ -25,6 +25,9 @@ #include "expr/node.h" namespace cvc5 { + +class Env; + namespace theory { namespace quantifiers { @@ -33,7 +36,7 @@ class NestedQe using NodeNodeMap = context::CDHashMap; public: - NestedQe(context::UserContext* u); + NestedQe(Env& env); ~NestedQe() {} /** * Process quantified formula. If this returns true, then q was processed @@ -64,15 +67,17 @@ class NestedQe * returned formula is quantifier-free. Otherwise, it is a quantified formula * with no nested quantification. */ - static Node doNestedQe(Node q, bool keepTopLevel = false); + static Node doNestedQe(Env& env, Node q, bool keepTopLevel = false); /** * Run quantifier elimination on quantified formula q, where q has no nested * quantification. This method invokes a subsolver for performing quantifier * elimination. */ - static Node doQe(Node q); + static Node doQe(Env& env, Node q); private: + /** Reference to the env */ + Env& d_env; /** * Mapping from quantified formulas q to the result of doNestedQe(q, true). */ diff --git a/src/theory/quantifiers/expr_miner.cpp b/src/theory/quantifiers/expr_miner.cpp index fa156c839..49b1d56fa 100644 --- a/src/theory/quantifiers/expr_miner.cpp +++ b/src/theory/quantifiers/expr_miner.cpp @@ -56,12 +56,14 @@ void ExprMiner::initializeChecker(std::unique_ptr& checker, Assert (!query.isNull()); if (Options::current().quantifiers.sygusExprMinerCheckTimeoutWasSetByUser) { - initializeSubsolver( - checker, nullptr, true, options::sygusExprMinerCheckTimeout()); + initializeSubsolver(checker, + d_env, + true, + options::sygusExprMinerCheckTimeout()); } else { - initializeSubsolver(checker); + initializeSubsolver(checker, d_env); } // also set the options checker->setOption("sygus-rr-synth-input", "false"); diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp index f1caca1c4..99716806f 100644 --- a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp +++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp @@ -38,7 +38,8 @@ namespace theory { namespace quantifiers { CegSingleInv::CegSingleInv(Env& env, TermRegistry& tr, SygusStatistics& s) - : d_sip(new SingleInvocationPartition), + : d_env(env), + d_sip(new SingleInvocationPartition), d_srcons(new SygusReconstruct(env, tr.getTermDatabaseSygus(), s)), d_isSolved(false), d_single_invocation(false), @@ -227,7 +228,7 @@ bool CegSingleInv::solve() } // solve the single invocation conjecture using a fresh copy of SMT engine std::unique_ptr siSmt; - initializeSubsolver(siSmt); + initializeSubsolver(siSmt, d_env); siSmt->assertFormula(siq); Result r = siSmt->checkSat(); Trace("sygus-si") << "Result: " << r << std::endl; diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.h b/src/theory/quantifiers/sygus/ce_guided_single_inv.h index 13757dba9..f7d6e5bb9 100644 --- a/src/theory/quantifiers/sygus/ce_guided_single_inv.h +++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.h @@ -51,6 +51,8 @@ class CegSingleInv std::map< Node, std::vector< Node > >& teq, Node n, std::vector< Node >& conj ); private: + /** Reference to the env */ + Env& d_env; // single invocation inference utility SingleInvocationPartition* d_sip; /** solution reconstruction */ diff --git a/src/theory/quantifiers/sygus/cegis.cpp b/src/theory/quantifiers/sygus/cegis.cpp index dff44eb1c..57b763044 100644 --- a/src/theory/quantifiers/sygus/cegis.cpp +++ b/src/theory/quantifiers/sygus/cegis.cpp @@ -32,10 +32,11 @@ namespace cvc5 { namespace theory { namespace quantifiers { -Cegis::Cegis(QuantifiersInferenceManager& qim, +Cegis::Cegis(QuantifiersState& qs, + QuantifiersInferenceManager& qim, TermDbSygus* tds, SynthConjecture* p) - : SygusModule(qim, tds, p), + : SygusModule(qs, qim, tds, p), d_eval_unfold(tds->getEvalUnfold()), d_usingSymCons(false) { diff --git a/src/theory/quantifiers/sygus/cegis.h b/src/theory/quantifiers/sygus/cegis.h index f5114d7ca..d6678a305 100644 --- a/src/theory/quantifiers/sygus/cegis.h +++ b/src/theory/quantifiers/sygus/cegis.h @@ -42,7 +42,10 @@ namespace quantifiers { class Cegis : public SygusModule { public: - Cegis(QuantifiersInferenceManager& qim, TermDbSygus* tds, SynthConjecture* p); + Cegis(QuantifiersState& qs, + QuantifiersInferenceManager& qim, + TermDbSygus* tds, + SynthConjecture* p); ~Cegis() override {} /** initialize */ virtual bool initialize(Node conj, diff --git a/src/theory/quantifiers/sygus/cegis_core_connective.cpp b/src/theory/quantifiers/sygus/cegis_core_connective.cpp index 165326db7..9a9d8f02d 100644 --- a/src/theory/quantifiers/sygus/cegis_core_connective.cpp +++ b/src/theory/quantifiers/sygus/cegis_core_connective.cpp @@ -68,10 +68,11 @@ bool VariadicTrie::hasSubset(const std::vector& is) const return false; } -CegisCoreConnective::CegisCoreConnective(QuantifiersInferenceManager& qim, +CegisCoreConnective::CegisCoreConnective(QuantifiersState& qs, + QuantifiersInferenceManager& qim, TermDbSygus* tds, SynthConjecture* p) - : Cegis(qim, tds, p) + : Cegis(qs, qim, tds, p) { d_true = NodeManager::currentNM()->mkConst(true); d_false = NodeManager::currentNM()->mkConst(false); @@ -628,7 +629,9 @@ bool CegisCoreConnective::getUnsatCore( Result CegisCoreConnective::checkSat(Node n, std::vector& mvs) const { Trace("sygus-ccore-debug") << "...check-sat " << n << "..." << std::endl; - Result r = checkWithSubsolver(n, d_vars, mvs); + Env& env = d_qstate.getEnv(); + Result r = + checkWithSubsolver(n, d_vars, mvs, env.getOptions(), env.getLogicInfo()); Trace("sygus-ccore-debug") << "...got " << r << std::endl; return r; } @@ -736,7 +739,7 @@ Node CegisCoreConnective::constructSolutionFromPool(Component& ccheck, addSuccess = false; // try a new core std::unique_ptr checkSol; - initializeSubsolver(checkSol); + initializeSubsolver(checkSol, d_qstate.getEnv()); Trace("sygus-ccore") << "----- Check candidate " << an << std::endl; std::vector rasserts = asserts; rasserts.push_back(d_sc); @@ -776,7 +779,7 @@ 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 checkSc; - initializeSubsolver(checkSc); + initializeSubsolver(checkSc, d_qstate.getEnv()); std::vector scasserts; scasserts.insert(scasserts.end(), uasserts.begin(), uasserts.end()); scasserts.push_back(d_sc); diff --git a/src/theory/quantifiers/sygus/cegis_core_connective.h b/src/theory/quantifiers/sygus/cegis_core_connective.h index 005e85706..e9a73e9bb 100644 --- a/src/theory/quantifiers/sygus/cegis_core_connective.h +++ b/src/theory/quantifiers/sygus/cegis_core_connective.h @@ -160,7 +160,8 @@ class VariadicTrie class CegisCoreConnective : public Cegis { public: - CegisCoreConnective(QuantifiersInferenceManager& qim, + CegisCoreConnective(QuantifiersState& qs, + QuantifiersInferenceManager& qim, TermDbSygus* tds, SynthConjecture* p); ~CegisCoreConnective() {} diff --git a/src/theory/quantifiers/sygus/cegis_unif.cpp b/src/theory/quantifiers/sygus/cegis_unif.cpp index 0b7255e2d..c4d9cbd4a 100644 --- a/src/theory/quantifiers/sygus/cegis_unif.cpp +++ b/src/theory/quantifiers/sygus/cegis_unif.cpp @@ -34,7 +34,7 @@ CegisUnif::CegisUnif(QuantifiersState& qs, QuantifiersInferenceManager& qim, TermDbSygus* tds, SynthConjecture* p) - : Cegis(qim, tds, p), d_sygus_unif(p), d_u_enum_manager(qs, qim, tds, p) + : Cegis(qs, qim, tds, p), d_sygus_unif(p), d_u_enum_manager(qs, qim, tds, p) { } diff --git a/src/theory/quantifiers/sygus/sygus_interpol.cpp b/src/theory/quantifiers/sygus/sygus_interpol.cpp index 426ad07ef..0dad29893 100644 --- a/src/theory/quantifiers/sygus/sygus_interpol.cpp +++ b/src/theory/quantifiers/sygus/sygus_interpol.cpp @@ -22,6 +22,7 @@ #include "expr/dtype.h" #include "expr/node_algorithm.h" #include "options/smt_options.h" +#include "smt/env.h" #include "theory/datatypes/sygus_datatype_utils.h" #include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/sygus/sygus_grammar_cons.h" @@ -32,7 +33,7 @@ namespace cvc5 { namespace theory { namespace quantifiers { -SygusInterpol::SygusInterpol() {} +SygusInterpol::SygusInterpol(Env& env) : d_env(env) {} void SygusInterpol::collectSymbols(const std::vector& axioms, const Node& conj) @@ -324,7 +325,7 @@ bool SygusInterpol::solveInterpolation(const std::string& name, mkSygusConjecture(itp, axioms, conj); std::unique_ptr subSolver; - initializeSubsolver(subSolver); + initializeSubsolver(subSolver, d_env); // get the logic LogicInfo l = subSolver->getLogicInfo().getUnlockedCopy(); // enable everything needed for sygus diff --git a/src/theory/quantifiers/sygus/sygus_interpol.h b/src/theory/quantifiers/sygus/sygus_interpol.h index e86ac624a..d4aedad8a 100644 --- a/src/theory/quantifiers/sygus/sygus_interpol.h +++ b/src/theory/quantifiers/sygus/sygus_interpol.h @@ -25,6 +25,7 @@ namespace cvc5 { +class Env; class SmtEngine; namespace theory { @@ -61,7 +62,7 @@ namespace quantifiers { class SygusInterpol { public: - SygusInterpol(); + SygusInterpol(Env& env); /** * Returns the sygus conjecture in interpol corresponding to the interpolation @@ -173,7 +174,8 @@ class SygusInterpol * @param itp the interpolation predicate. */ bool findInterpol(SmtEngine* subsolver, Node& interpol, Node itp); - + /** Reference to the env */ + Env& d_env; /** * symbols from axioms and conjecture. */ diff --git a/src/theory/quantifiers/sygus/sygus_module.cpp b/src/theory/quantifiers/sygus/sygus_module.cpp index b134eb993..4cb333849 100644 --- a/src/theory/quantifiers/sygus/sygus_module.cpp +++ b/src/theory/quantifiers/sygus/sygus_module.cpp @@ -19,10 +19,11 @@ namespace cvc5 { namespace theory { namespace quantifiers { -SygusModule::SygusModule(QuantifiersInferenceManager& qim, +SygusModule::SygusModule(QuantifiersState& qs, + QuantifiersInferenceManager& qim, TermDbSygus* tds, SynthConjecture* p) - : d_qim(qim), d_tds(tds), d_parent(p) + : d_qstate(qs), d_qim(qim), d_tds(tds), d_parent(p) { } diff --git a/src/theory/quantifiers/sygus/sygus_module.h b/src/theory/quantifiers/sygus/sygus_module.h index d93957a15..d7e0caa5b 100644 --- a/src/theory/quantifiers/sygus/sygus_module.h +++ b/src/theory/quantifiers/sygus/sygus_module.h @@ -28,6 +28,7 @@ namespace quantifiers { class SynthConjecture; class TermDbSygus; +class QuantifiersState; class QuantifiersInferenceManager; /** SygusModule @@ -51,7 +52,8 @@ class QuantifiersInferenceManager; class SygusModule { public: - SygusModule(QuantifiersInferenceManager& qim, + SygusModule(QuantifiersState& qs, + QuantifiersInferenceManager& qim, TermDbSygus* tds, SynthConjecture* p); virtual ~SygusModule() {} @@ -147,6 +149,8 @@ class SygusModule virtual bool usingRepairConst() { return false; } protected: + /** Reference to the state of the quantifiers engine */ + QuantifiersState& d_qstate; /** Reference to the quantifiers inference manager */ QuantifiersInferenceManager& d_qim; /** sygus term database of d_qe */ diff --git a/src/theory/quantifiers/sygus/sygus_pbe.cpp b/src/theory/quantifiers/sygus/sygus_pbe.cpp index 27a1e3f3b..26621eb96 100644 --- a/src/theory/quantifiers/sygus/sygus_pbe.cpp +++ b/src/theory/quantifiers/sygus/sygus_pbe.cpp @@ -30,10 +30,11 @@ namespace cvc5 { namespace theory { namespace quantifiers { -SygusPbe::SygusPbe(QuantifiersInferenceManager& qim, +SygusPbe::SygusPbe(QuantifiersState& qs, + QuantifiersInferenceManager& qim, TermDbSygus* tds, SynthConjecture* p) - : SygusModule(qim, tds, p) + : SygusModule(qs, qim, tds, p) { d_true = NodeManager::currentNM()->mkConst(true); d_false = NodeManager::currentNM()->mkConst(false); diff --git a/src/theory/quantifiers/sygus/sygus_pbe.h b/src/theory/quantifiers/sygus/sygus_pbe.h index e27f4ce35..867764617 100644 --- a/src/theory/quantifiers/sygus/sygus_pbe.h +++ b/src/theory/quantifiers/sygus/sygus_pbe.h @@ -86,7 +86,8 @@ class SynthConjecture; class SygusPbe : public SygusModule { public: - SygusPbe(QuantifiersInferenceManager& qim, + SygusPbe(QuantifiersState& qs, + QuantifiersInferenceManager& qim, TermDbSygus* tds, SynthConjecture* p); ~SygusPbe(); diff --git a/src/theory/quantifiers/sygus/sygus_qe_preproc.cpp b/src/theory/quantifiers/sygus/sygus_qe_preproc.cpp index c6ff7e61a..5cf7122f3 100644 --- a/src/theory/quantifiers/sygus/sygus_qe_preproc.cpp +++ b/src/theory/quantifiers/sygus/sygus_qe_preproc.cpp @@ -27,7 +27,7 @@ namespace cvc5 { namespace theory { namespace quantifiers { -SygusQePreproc::SygusQePreproc() {} +SygusQePreproc::SygusQePreproc(Env& env) : d_env(env) {} Node SygusQePreproc::preprocess(Node q) { @@ -53,7 +53,7 @@ Node SygusQePreproc::preprocess(Node q) } // create new smt engine to do quantifier elimination std::unique_ptr smt_qe; - initializeSubsolver(smt_qe); + initializeSubsolver(smt_qe, d_env); Trace("cegqi-qep") << "Property is non-ground single invocation, run " "QE to obtain single invocation." << std::endl; diff --git a/src/theory/quantifiers/sygus/sygus_qe_preproc.h b/src/theory/quantifiers/sygus/sygus_qe_preproc.h index 551dd1611..0cbd96914 100644 --- a/src/theory/quantifiers/sygus/sygus_qe_preproc.h +++ b/src/theory/quantifiers/sygus/sygus_qe_preproc.h @@ -19,6 +19,9 @@ #include "expr/node.h" namespace cvc5 { + +class Env; + namespace theory { namespace quantifiers { @@ -35,13 +38,17 @@ namespace quantifiers { class SygusQePreproc { public: - SygusQePreproc(); + SygusQePreproc(Env& env); ~SygusQePreproc() {} /** * Preprocess. Returns a lemma of the form q = nq where nq is obtained * by the quantifier elimination technique outlined above. */ Node preprocess(Node q); + + private: + /** Reference to the env */ + Env& d_env; }; } // namespace quantifiers diff --git a/src/theory/quantifiers/sygus/sygus_repair_const.cpp b/src/theory/quantifiers/sygus/sygus_repair_const.cpp index d4611e6ca..4a8d0406b 100644 --- a/src/theory/quantifiers/sygus/sygus_repair_const.cpp +++ b/src/theory/quantifiers/sygus/sygus_repair_const.cpp @@ -232,7 +232,8 @@ bool SygusRepairConst::repairSolution(Node sygusBody, // initialize the subsolver using the standard method initializeSubsolver( repcChecker, - nullptr, + d_env.getOptions(), + d_env.getLogicInfo(), Options::current().quantifiers.sygusRepairConstTimeoutWasSetByUser, options::sygusRepairConstTimeout()); // renable options disabled by sygus diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp index eeadbdd54..3e7095c12 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.cpp +++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp @@ -56,7 +56,7 @@ SynthConjecture::SynthConjecture(QuantifiersState& qs, d_treg(tr), d_stats(s), d_tds(tr.getTermDatabaseSygus()), - d_verify(qs.options(), d_tds), + d_verify(qs.options(), qs.getLogicInfo(), d_tds), d_hasSolution(false), d_ceg_si(new CegSingleInv(qs.getEnv(), tr, s)), d_templInfer(new SygusTemplateInfer), @@ -64,10 +64,10 @@ SynthConjecture::SynthConjecture(QuantifiersState& qs, d_ceg_gc(new CegGrammarConstructor(d_tds, this)), d_sygus_rconst(new SygusRepairConst(qs.getEnv(), d_tds)), d_exampleInfer(new ExampleInfer(d_tds)), - d_ceg_pbe(new SygusPbe(qim, d_tds, this)), - d_ceg_cegis(new Cegis(qim, d_tds, this)), + d_ceg_pbe(new SygusPbe(qs, qim, d_tds, this)), + d_ceg_cegis(new Cegis(qs, qim, d_tds, this)), d_ceg_cegisUnif(new CegisUnif(qs, qim, d_tds, this)), - d_sygus_ccore(new CegisCoreConnective(qim, d_tds, this)), + d_sygus_ccore(new CegisCoreConnective(qs, qim, d_tds, this)), d_master(nullptr), d_set_ce_sk_vars(false), d_repair_index(0), @@ -609,7 +609,8 @@ bool SynthConjecture::checkSideCondition(const std::vector& cvals) const } Trace("sygus-engine") << "Check side condition..." << std::endl; Trace("cegqi-debug") << "Check side condition : " << sc << std::endl; - Result r = checkWithSubsolver(sc); + Env& env = d_qstate.getEnv(); + Result r = checkWithSubsolver(sc, env.getOptions(), env.getLogicInfo()); Trace("cegqi-debug") << "...got side condition : " << r << std::endl; if (r == Result::UNSAT) { diff --git a/src/theory/quantifiers/sygus/synth_engine.cpp b/src/theory/quantifiers/sygus/synth_engine.cpp index 65907cb31..cdcbeb85d 100644 --- a/src/theory/quantifiers/sygus/synth_engine.cpp +++ b/src/theory/quantifiers/sygus/synth_engine.cpp @@ -30,7 +30,7 @@ SynthEngine::SynthEngine(QuantifiersState& qs, QuantifiersInferenceManager& qim, QuantifiersRegistry& qr, TermRegistry& tr) - : QuantifiersModule(qs, qim, qr, tr), d_conj(nullptr), d_sqp() + : QuantifiersModule(qs, qim, qr, tr), d_conj(nullptr), d_sqp(qs.getEnv()) { d_conjs.push_back(std::unique_ptr( new SynthConjecture(qs, qim, qr, tr, d_statistics))); diff --git a/src/theory/quantifiers/sygus/synth_verify.cpp b/src/theory/quantifiers/sygus/synth_verify.cpp index 9e8171fdc..db09b45ed 100644 --- a/src/theory/quantifiers/sygus/synth_verify.cpp +++ b/src/theory/quantifiers/sygus/synth_verify.cpp @@ -32,7 +32,10 @@ namespace cvc5 { namespace theory { namespace quantifiers { -SynthVerify::SynthVerify(const Options& opts, TermDbSygus* tds) : d_tds(tds) +SynthVerify::SynthVerify(const Options& opts, + const LogicInfo& logicInfo, + TermDbSygus* tds) + : d_tds(tds), d_subLogicInfo(logicInfo) { // determine the options to use for the verification subsolvers we spawn // we start with the provided options @@ -102,7 +105,7 @@ Result SynthVerify::verify(Node query, } } Trace("sygus-engine") << " *** Verify with subcall..." << std::endl; - Result r = checkWithSubsolver(query, vars, mvs, &d_subOptions); + Result r = checkWithSubsolver(query, vars, mvs, d_subOptions, d_subLogicInfo); Trace("sygus-engine") << " ...got " << r << std::endl; if (r.asSatisfiabilityResult().isSat() == Result::SAT) { diff --git a/src/theory/quantifiers/sygus/synth_verify.h b/src/theory/quantifiers/sygus/synth_verify.h index c4d1052da..948a70787 100644 --- a/src/theory/quantifiers/sygus/synth_verify.h +++ b/src/theory/quantifiers/sygus/synth_verify.h @@ -34,7 +34,9 @@ namespace quantifiers { class SynthVerify { public: - SynthVerify(const Options& opts, TermDbSygus* tds); + SynthVerify(const Options& opts, + const LogicInfo& logicInfo, + TermDbSygus* tds); ~SynthVerify(); /** * Verification call, which takes into account specific aspects of the @@ -55,6 +57,8 @@ class SynthVerify TermDbSygus* d_tds; /** The options for subsolver calls */ Options d_subOptions; + /** The logic info for subsolver calls */ + const LogicInfo& d_subLogicInfo; }; } // namespace quantifiers diff --git a/src/theory/smt_engine_subsolver.cpp b/src/theory/smt_engine_subsolver.cpp index 5f285dc07..dda065d7b 100644 --- a/src/theory/smt_engine_subsolver.cpp +++ b/src/theory/smt_engine_subsolver.cpp @@ -16,6 +16,7 @@ #include "theory/smt_engine_subsolver.h" +#include "smt/env.h" #include "smt/smt_engine.h" #include "smt/smt_engine_scope.h" #include "theory/rewriter.h" @@ -42,30 +43,34 @@ Result quickCheck(Node& query) } void initializeSubsolver(std::unique_ptr& smte, - Options* opts, + const Options& opts, + const LogicInfo& logicInfo, bool needsTimeout, unsigned long timeout) { NodeManager* nm = NodeManager::currentNM(); - SmtEngine* smtCurr = smt::currentSmtEngine(); - if (opts == nullptr) - { - // must copy the options - opts = &smtCurr->getOptions(); - } - smte.reset(new SmtEngine(nm, opts)); + smte.reset(new SmtEngine(nm, &opts)); smte->setIsInternalSubsolver(); - smte->setLogic(smtCurr->getLogicInfo()); + smte->setLogic(logicInfo); // set the options if (needsTimeout) { smte->setTimeLimit(timeout); } } +void initializeSubsolver(std::unique_ptr& smte, + const Env& env, + bool needsTimeout, + unsigned long timeout) +{ + initializeSubsolver( + smte, env.getOptions(), env.getLogicInfo(), needsTimeout, timeout); +} Result checkWithSubsolver(std::unique_ptr& smte, Node query, - Options* opts, + const Options& opts, + const LogicInfo& logicInfo, bool needsTimeout, unsigned long timeout) { @@ -75,26 +80,28 @@ Result checkWithSubsolver(std::unique_ptr& smte, { return r; } - initializeSubsolver(smte, opts, needsTimeout, timeout); + initializeSubsolver(smte, opts, logicInfo, needsTimeout, timeout); smte->assertFormula(query); return smte->checkSat(); } Result checkWithSubsolver(Node query, - Options* opts, + const Options& opts, + const LogicInfo& logicInfo, bool needsTimeout, unsigned long timeout) { std::vector vars; std::vector modelVals; return checkWithSubsolver( - query, vars, modelVals, opts, needsTimeout, timeout); + query, vars, modelVals, opts, logicInfo, needsTimeout, timeout); } Result checkWithSubsolver(Node query, const std::vector& vars, std::vector& modelVals, - Options* opts, + const Options& opts, + const LogicInfo& logicInfo, bool needsTimeout, unsigned long timeout) { @@ -116,7 +123,7 @@ Result checkWithSubsolver(Node query, return r; } std::unique_ptr smte; - initializeSubsolver(smte, opts, needsTimeout, timeout); + initializeSubsolver(smte, opts, logicInfo, needsTimeout, timeout); smte->assertFormula(query); 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 2d80831f2..028c35cd8 100644 --- a/src/theory/smt_engine_subsolver.h +++ b/src/theory/smt_engine_subsolver.h @@ -41,13 +41,22 @@ namespace theory { * if the current SMT engine has declared a separation logic heap. * * @param smte The smt engine pointer to initialize - * @param opts The options for the subsolver. If nullptr, then we copy the - * options from the current SmtEngine in scope. + * @param opts The options for the subsolver. + * @param logicInfo The logic info to set on the subsolver * @param needsTimeout Whether we would like to set a timeout * @param timeout The timeout (in milliseconds) */ void initializeSubsolver(std::unique_ptr& smte, - Options* opts = nullptr, + const Options& opts, + const LogicInfo& logicInfo, + bool needsTimeout = false, + unsigned long timeout = 0); + +/** + * Version that uses the options and logicInfo in an environment. + */ +void initializeSubsolver(std::unique_ptr& smte, + const Env& env, bool needsTimeout = false, unsigned long timeout = 0); @@ -59,7 +68,8 @@ void initializeSubsolver(std::unique_ptr& smte, */ Result checkWithSubsolver(std::unique_ptr& smte, Node query, - Options* opts = nullptr, + const Options& opts, + const LogicInfo& logicInfo, bool needsTimeout = false, unsigned long timeout = 0); @@ -71,11 +81,13 @@ Result checkWithSubsolver(std::unique_ptr& smte, * * @param query The query to check * @param opts The options for the subsolver + * @param logicInfo The logic info to set on the subsolver * @param needsTimeout Whether we would like to set a timeout * @param timeout The timeout (in milliseconds) */ Result checkWithSubsolver(Node query, - Options* opts = nullptr, + const Options& opts, + const LogicInfo& logicInfo, bool needsTimeout = false, unsigned long timeout = 0); @@ -88,13 +100,15 @@ Result checkWithSubsolver(Node query, * @param vars The variables we are interesting in getting a model for. * @param modelVals A vector storing the model values of variables in vars. * @param opts The options for the subsolver + * @param logicInfo The logic info to set on the subsolver * @param needsTimeout Whether we would like to set a timeout * @param timeout The timeout (in milliseconds) */ Result checkWithSubsolver(Node query, const std::vector& vars, std::vector& modelVals, - Options* opts = nullptr, + const Options& opts, + const LogicInfo& logicInfo, bool needsTimeout = false, unsigned long timeout = 0); -- 2.30.2