diff options
Diffstat (limited to 'src/theory/quantifiers/sygus')
20 files changed, 72 insertions, 35 deletions
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<SmtEngine> 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<Node>& 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<Node>& 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<SmtEngine> checkSol; - initializeSubsolver(checkSol); + initializeSubsolver(checkSol, d_qstate.getEnv()); Trace("sygus-ccore") << "----- Check candidate " << an << std::endl; std::vector<Node> 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<SmtEngine> checkSc; - initializeSubsolver(checkSc); + initializeSubsolver(checkSc, d_qstate.getEnv()); std::vector<Node> 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<Node>& axioms, const Node& conj) @@ -324,7 +325,7 @@ bool SygusInterpol::solveInterpolation(const std::string& name, mkSygusConjecture(itp, axioms, conj); std::unique_ptr<SmtEngine> 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<SmtEngine> 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<Node>& 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<SynthConjecture>( 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 |