diff options
Diffstat (limited to 'src/theory/quantifiers/sygus')
19 files changed, 74 insertions, 54 deletions
diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp index 99a5126aa..f1caca1c4 100644 --- a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp +++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp @@ -17,8 +17,6 @@ #include "expr/skolem_manager.h" #include "options/quantifiers_options.h" #include "smt/logic_exception.h" -#include "smt/smt_engine.h" -#include "smt/smt_engine_scope.h" #include "smt/smt_statistics_registry.h" #include "theory/arith/arith_msum.h" #include "theory/quantifiers/quantifiers_attributes.h" @@ -39,9 +37,9 @@ namespace cvc5 { namespace theory { namespace quantifiers { -CegSingleInv::CegSingleInv(TermRegistry& tr, SygusStatistics& s) +CegSingleInv::CegSingleInv(Env& env, TermRegistry& tr, SygusStatistics& s) : d_sip(new SingleInvocationPartition), - d_srcons(new SygusReconstruct(tr.getTermDatabaseSygus(), s)), + d_srcons(new SygusReconstruct(env, tr.getTermDatabaseSygus(), s)), d_isSolved(false), d_single_invocation(false), d_treg(tr) diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.h b/src/theory/quantifiers/sygus/ce_guided_single_inv.h index 72d41592a..13757dba9 100644 --- a/src/theory/quantifiers/sygus/ce_guided_single_inv.h +++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.h @@ -91,7 +91,7 @@ class CegSingleInv Node d_single_inv; public: - CegSingleInv(TermRegistry& tr, SygusStatistics& s); + CegSingleInv(Env& env, TermRegistry& tr, SygusStatistics& s); ~CegSingleInv(); // get simplified conjecture diff --git a/src/theory/quantifiers/sygus/cegis_core_connective.cpp b/src/theory/quantifiers/sygus/cegis_core_connective.cpp index 4bcede905..165326db7 100644 --- a/src/theory/quantifiers/sygus/cegis_core_connective.cpp +++ b/src/theory/quantifiers/sygus/cegis_core_connective.cpp @@ -19,8 +19,6 @@ #include "options/base_options.h" #include "printer/printer.h" #include "proof/unsat_core.h" -#include "smt/smt_engine.h" -#include "smt/smt_engine_scope.h" #include "theory/datatypes/theory_datatypes_utils.h" #include "theory/quantifiers/sygus/ce_guided_single_inv.h" #include "theory/quantifiers/sygus/transition_inference.h" diff --git a/src/theory/quantifiers/sygus/enum_value_manager.cpp b/src/theory/quantifiers/sygus/enum_value_manager.cpp index fd92e4d23..8a2d70bfa 100644 --- a/src/theory/quantifiers/sygus/enum_value_manager.cpp +++ b/src/theory/quantifiers/sygus/enum_value_manager.cpp @@ -14,6 +14,7 @@ */ #include "theory/quantifiers/sygus/enum_value_manager.h" +#include "options/base_options.h" #include "options/datatypes_options.h" #include "options/quantifiers_options.h" #include "theory/datatypes/sygus_datatype_utils.h" @@ -33,11 +34,13 @@ namespace theory { namespace quantifiers { EnumValueManager::EnumValueManager(Node e, + QuantifiersState& qs, QuantifiersInferenceManager& qim, TermRegistry& tr, SygusStatistics& s, bool hasExamples) : d_enum(e), + d_qstate(qs), d_qim(qim), d_treg(tr), d_stats(s), @@ -98,14 +101,17 @@ Node EnumValueManager::getEnumeratedValue(bool& activeIncomplete) // create the enumerator callback if (options::sygusSymBreakDynamic()) { + std::ostream* out = nullptr; if (options::sygusRewVerify()) { d_samplerRrV.reset(new SygusSampler); d_samplerRrV->initializeSygus( d_tds, e, options::sygusSamples(), false); + // use the default output for the output of sygusRewVerify + out = d_qstate.options().base.out; } d_secd.reset(new SygusEnumeratorCallbackDefault( - e, &d_stats, d_eec.get(), d_samplerRrV.get())); + e, &d_stats, d_eec.get(), d_samplerRrV.get(), out)); } // if sygus repair const is enabled, we enumerate terms with free // variables as arguments to any-constant constructors diff --git a/src/theory/quantifiers/sygus/enum_value_manager.h b/src/theory/quantifiers/sygus/enum_value_manager.h index e610764e0..c786bb6f1 100644 --- a/src/theory/quantifiers/sygus/enum_value_manager.h +++ b/src/theory/quantifiers/sygus/enum_value_manager.h @@ -42,6 +42,7 @@ class EnumValueManager { public: EnumValueManager(Node e, + QuantifiersState& qs, QuantifiersInferenceManager& qim, TermRegistry& tr, SygusStatistics& s, @@ -71,6 +72,8 @@ class EnumValueManager Node getModelValue(Node n); /** The enumerator */ Node d_enum; + /** Reference to the quantifiers state */ + QuantifiersState& d_qstate; /** Reference to the quantifiers inference manager */ QuantifiersInferenceManager& d_qim; /** Reference to the term registry */ diff --git a/src/theory/quantifiers/sygus/rcons_type_info.cpp b/src/theory/quantifiers/sygus/rcons_type_info.cpp index a1ae53ad1..78f8d303c 100644 --- a/src/theory/quantifiers/sygus/rcons_type_info.cpp +++ b/src/theory/quantifiers/sygus/rcons_type_info.cpp @@ -23,7 +23,8 @@ namespace cvc5 { namespace theory { namespace quantifiers { -void RConsTypeInfo::initialize(TermDbSygus* tds, +void RConsTypeInfo::initialize(Env& env, + TermDbSygus* tds, SygusStatistics& s, TypeNode stn, const std::vector<Node>& builtinVars) @@ -33,7 +34,7 @@ void RConsTypeInfo::initialize(TermDbSygus* tds, d_enumerator.reset(new SygusEnumerator(tds, nullptr, &s, true)); d_enumerator->initialize(sm->mkDummySkolem("sygus_rcons", stn)); - d_crd.reset(new CandidateRewriteDatabase(true, false, true, false)); + d_crd.reset(new CandidateRewriteDatabase(env, true, false, true, false)); // since initial samples are not always useful for equivalence checks, set // their number to 0 d_sygusSampler.initialize(stn, builtinVars, 0); diff --git a/src/theory/quantifiers/sygus/rcons_type_info.h b/src/theory/quantifiers/sygus/rcons_type_info.h index 4c9ae48e0..294454fe2 100644 --- a/src/theory/quantifiers/sygus/rcons_type_info.h +++ b/src/theory/quantifiers/sygus/rcons_type_info.h @@ -41,13 +41,15 @@ class RConsTypeInfo * Initialize a sygus enumerator and a candidate rewrite database for this * class' sygus datatype type. * + * @param env Reference to the environment * @param tds Database for sygus terms * @param s Statistics managed for the synth engine * @param stn The sygus datatype type encoding the syntax restrictions * @param builtinVars A list containing the builtin analog of sygus variable * list for the sygus datatype type */ - void initialize(TermDbSygus* tds, + void initialize(Env& env, + TermDbSygus* tds, SygusStatistics& s, TypeNode stn, const std::vector<Node>& builtinVars); diff --git a/src/theory/quantifiers/sygus/sygus_enumerator_callback.cpp b/src/theory/quantifiers/sygus/sygus_enumerator_callback.cpp index 7b3236832..3b536695f 100644 --- a/src/theory/quantifiers/sygus/sygus_enumerator_callback.cpp +++ b/src/theory/quantifiers/sygus/sygus_enumerator_callback.cpp @@ -63,8 +63,12 @@ bool SygusEnumeratorCallback::addTerm(Node n, std::unordered_set<Node>& bterms) } SygusEnumeratorCallbackDefault::SygusEnumeratorCallbackDefault( - Node e, SygusStatistics* s, ExampleEvalCache* eec, SygusSampler* ssrv) - : SygusEnumeratorCallback(e, s), d_eec(eec), d_samplerRrV(ssrv) + Node e, + SygusStatistics* s, + ExampleEvalCache* eec, + SygusSampler* ssrv, + std::ostream* out) + : SygusEnumeratorCallback(e, s), d_eec(eec), d_samplerRrV(ssrv), d_out(out) { } void SygusEnumeratorCallbackDefault::notifyTermInternal(Node n, @@ -73,7 +77,8 @@ void SygusEnumeratorCallbackDefault::notifyTermInternal(Node n, { if (d_samplerRrV != nullptr) { - d_samplerRrV->checkEquivalent(bn, bnr); + Assert(d_out != nullptr); + d_samplerRrV->checkEquivalent(bn, bnr, *d_out); } } diff --git a/src/theory/quantifiers/sygus/sygus_enumerator_callback.h b/src/theory/quantifiers/sygus/sygus_enumerator_callback.h index 46ca68c51..5ed28b309 100644 --- a/src/theory/quantifiers/sygus/sygus_enumerator_callback.h +++ b/src/theory/quantifiers/sygus/sygus_enumerator_callback.h @@ -86,7 +86,8 @@ class SygusEnumeratorCallbackDefault : public SygusEnumeratorCallback SygusEnumeratorCallbackDefault(Node e, SygusStatistics* s = nullptr, ExampleEvalCache* eec = nullptr, - SygusSampler* ssrv = nullptr); + SygusSampler* ssrv = nullptr, + std::ostream* out = nullptr); virtual ~SygusEnumeratorCallbackDefault() {} protected: @@ -101,6 +102,8 @@ class SygusEnumeratorCallbackDefault : public SygusEnumeratorCallback ExampleEvalCache* d_eec; /** sampler (for --sygus-rr-verify) */ SygusSampler* d_samplerRrV; + /** The output stream to print unsound rewrites for above */ + std::ostream* d_out; }; } // namespace quantifiers diff --git a/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp b/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp index d4d1398f4..209d10297 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp +++ b/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp @@ -21,8 +21,6 @@ #include "expr/dtype_cons.h" #include "expr/node_manager_attributes.h" // for VarNameAttr #include "options/quantifiers_options.h" -#include "smt/smt_engine.h" -#include "smt/smt_engine_scope.h" #include "theory/datatypes/theory_datatypes_utils.h" #include "theory/quantifiers/cegqi/ceg_instantiator.h" #include "theory/quantifiers/sygus/sygus_grammar_cons.h" diff --git a/src/theory/quantifiers/sygus/sygus_interpol.h b/src/theory/quantifiers/sygus/sygus_interpol.h index 07f5ed4ad..e86ac624a 100644 --- a/src/theory/quantifiers/sygus/sygus_interpol.h +++ b/src/theory/quantifiers/sygus/sygus_interpol.h @@ -22,9 +22,11 @@ #include "expr/node.h" #include "expr/type_node.h" -#include "smt/smt_engine.h" namespace cvc5 { + +class SmtEngine; + namespace theory { namespace quantifiers { /** diff --git a/src/theory/quantifiers/sygus/sygus_reconstruct.cpp b/src/theory/quantifiers/sygus/sygus_reconstruct.cpp index 5da282606..3073a472d 100644 --- a/src/theory/quantifiers/sygus/sygus_reconstruct.cpp +++ b/src/theory/quantifiers/sygus/sygus_reconstruct.cpp @@ -26,8 +26,10 @@ namespace cvc5 { namespace theory { namespace quantifiers { -SygusReconstruct::SygusReconstruct(TermDbSygus* tds, SygusStatistics& s) - : d_tds(tds), d_stats(s) +SygusReconstruct::SygusReconstruct(Env& env, + TermDbSygus* tds, + SygusStatistics& s) + : d_env(env), d_tds(tds), d_stats(s) { } @@ -408,7 +410,7 @@ void SygusReconstruct::initialize(TypeNode stn) // the database. for (TypeNode tn : sfTypes) { - d_stnInfo[tn].initialize(d_tds, d_stats, tn, builtinVars); + d_stnInfo[tn].initialize(d_env, d_tds, d_stats, tn, builtinVars); } } diff --git a/src/theory/quantifiers/sygus/sygus_reconstruct.h b/src/theory/quantifiers/sygus/sygus_reconstruct.h index e86b1688c..4102db713 100644 --- a/src/theory/quantifiers/sygus/sygus_reconstruct.h +++ b/src/theory/quantifiers/sygus/sygus_reconstruct.h @@ -144,10 +144,11 @@ class SygusReconstruct : public expr::NotifyMatch /** * Constructor. * + * @param env reference to the environment * @param tds database for sygus terms * @param s statistics managed for the synth engine */ - SygusReconstruct(TermDbSygus* tds, SygusStatistics& s); + SygusReconstruct(Env& env, TermDbSygus* tds, SygusStatistics& s); /** Reconstruct solution. * @@ -297,6 +298,8 @@ class SygusReconstruct : public expr::NotifyMatch void printPool( const std::unordered_map<TypeNode, std::vector<Node>>& pool) const; + /** Reference to the env */ + Env& d_env; /** pointer to the sygus term database */ TermDbSygus* d_tds; /** reference to the statistics of parent */ diff --git a/src/theory/quantifiers/sygus/sygus_repair_const.cpp b/src/theory/quantifiers/sygus/sygus_repair_const.cpp index 739e9ab0d..d4611e6ca 100644 --- a/src/theory/quantifiers/sygus/sygus_repair_const.cpp +++ b/src/theory/quantifiers/sygus/sygus_repair_const.cpp @@ -21,9 +21,6 @@ #include "options/base_options.h" #include "options/quantifiers_options.h" #include "printer/printer.h" -#include "smt/smt_engine.h" -#include "smt/smt_engine_scope.h" -#include "smt/smt_statistics_registry.h" #include "theory/datatypes/theory_datatypes_utils.h" #include "theory/logic_info.h" #include "theory/quantifiers/cegqi/ceg_instantiator.h" @@ -37,8 +34,8 @@ namespace cvc5 { namespace theory { namespace quantifiers { -SygusRepairConst::SygusRepairConst(TermDbSygus* tds) - : d_tds(tds), d_allow_constant_grammar(false) +SygusRepairConst::SygusRepairConst(Env& env, TermDbSygus* tds) + : d_env(env), d_tds(tds), d_allow_constant_grammar(false) { } @@ -192,7 +189,7 @@ bool SygusRepairConst::repairSolution(Node sygusBody, // check whether it is not in the current logic, e.g. non-linear arithmetic. // if so, undo replacements until it is in the current logic. - LogicInfo logic = smt::currentSmtEngine()->getLogicInfo(); + const LogicInfo& logic = d_env.getLogicInfo(); if (logic.isTheoryEnabled(THEORY_ARITH) && logic.isLinear()) { fo_body = fitToLogic(sygusBody, @@ -531,7 +528,7 @@ Node SygusRepairConst::getFoQuery(Node body, } Node SygusRepairConst::fitToLogic(Node body, - LogicInfo& logic, + const LogicInfo& logic, Node n, const std::vector<Node>& candidates, std::vector<Node>& candidate_skeletons, @@ -570,7 +567,7 @@ Node SygusRepairConst::fitToLogic(Node body, return Node::null(); } -bool SygusRepairConst::getFitToLogicExcludeVar(LogicInfo& logic, +bool SygusRepairConst::getFitToLogicExcludeVar(const LogicInfo& logic, Node n, Node& exvar) { diff --git a/src/theory/quantifiers/sygus/sygus_repair_const.h b/src/theory/quantifiers/sygus/sygus_repair_const.h index f0452a59c..ce6c81011 100644 --- a/src/theory/quantifiers/sygus/sygus_repair_const.h +++ b/src/theory/quantifiers/sygus/sygus_repair_const.h @@ -23,6 +23,7 @@ namespace cvc5 { +class Env; class LogicInfo; namespace theory { @@ -48,7 +49,7 @@ class TermDbSygus; class SygusRepairConst { public: - SygusRepairConst(TermDbSygus* tds); + SygusRepairConst(Env& env, TermDbSygus* tds); ~SygusRepairConst() {} /** initialize * @@ -105,6 +106,8 @@ class SygusRepairConst static bool mustRepair(Node n); private: + /** Reference to the env */ + Env& d_env; /** pointer to the sygus term database of d_qe */ TermDbSygus* d_tds; /** @@ -188,7 +191,7 @@ class SygusRepairConst * sk_vars. */ Node fitToLogic(Node body, - LogicInfo& logic, + const LogicInfo& logic, Node n, const std::vector<Node>& candidates, std::vector<Node>& candidate_skeletons, @@ -205,7 +208,7 @@ class SygusRepairConst * exvar to x. * If n is in the given logic, this method returns true. */ - bool getFitToLogicExcludeVar(LogicInfo& logic, Node n, Node& exvar); + bool getFitToLogicExcludeVar(const LogicInfo& logic, Node n, Node& exvar); }; } // namespace quantifiers diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp index 3f7ce158c..eeadbdd54 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.cpp +++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp @@ -24,7 +24,6 @@ #include "options/quantifiers_options.h" #include "printer/printer.h" #include "smt/logic_exception.h" -#include "smt/smt_engine_scope.h" #include "smt/smt_statistics_registry.h" #include "theory/datatypes/sygus_datatype_utils.h" #include "theory/quantifiers/first_order_model.h" @@ -57,13 +56,13 @@ SynthConjecture::SynthConjecture(QuantifiersState& qs, d_treg(tr), d_stats(s), d_tds(tr.getTermDatabaseSygus()), - d_verify(d_tds), + d_verify(qs.options(), d_tds), d_hasSolution(false), - d_ceg_si(new CegSingleInv(tr, s)), + d_ceg_si(new CegSingleInv(qs.getEnv(), tr, s)), d_templInfer(new SygusTemplateInfer), d_ceg_proc(new SynthConjectureProcess), d_ceg_gc(new CegGrammarConstructor(d_tds, this)), - d_sygus_rconst(new SygusRepairConst(d_tds)), + 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)), @@ -514,7 +513,7 @@ bool SynthConjecture::doCheck() { if (printDebug) { - Options& sopts = smt::currentSmtEngine()->getOptions(); + const Options& sopts = d_qstate.options(); std::ostream& out = *sopts.base.out; out << "(sygus-candidate "; Assert(d_quant[0].getNumChildren() == candidate_values.size()); @@ -764,7 +763,7 @@ EnumValueManager* SynthConjecture::getEnumValueManagerFor(Node e) bool hasExamples = (d_exampleInfer->hasExamples(f) && d_exampleInfer->getNumExamples(f) != 0); d_enumManager[e].reset( - new EnumValueManager(e, d_qim, d_treg, d_stats, hasExamples)); + new EnumValueManager(e, d_qstate, d_qim, d_treg, d_stats, hasExamples)); EnumValueManager* eman = d_enumManager[e].get(); // set up the examples if (hasExamples) @@ -800,7 +799,7 @@ void SynthConjecture::printAndContinueStream(const std::vector<Node>& enums, Assert(d_master != nullptr); // we have generated a solution, print it // get the current output stream - Options& sopts = smt::currentSmtEngine()->getOptions(); + const Options& sopts = d_qstate.options(); printSynthSolutionInternal(*sopts.base.out); excludeCurrentSolution(enums, values); } @@ -881,19 +880,21 @@ void SynthConjecture::printSynthSolutionInternal(std::ostream& out) != options::SygusFilterSolMode::NONE)) { Trace("cegqi-sol-debug") << "Run expression mining..." << std::endl; - std::map<Node, ExpressionMinerManager>::iterator its = + std::map<Node, std::unique_ptr<ExpressionMinerManager>>::iterator its = d_exprm.find(prog); if (its == d_exprm.end()) { - d_exprm[prog].initializeSygus( + d_exprm[prog].reset(new ExpressionMinerManager(d_qstate.getEnv())); + ExpressionMinerManager* emm = d_exprm[prog].get(); + emm->initializeSygus( d_tds, d_candidates[i], options::sygusSamples(), true); if (options::sygusRewSynth()) { - d_exprm[prog].enableRewriteRuleSynth(); + emm->enableRewriteRuleSynth(); } if (options::sygusQueryGen()) { - d_exprm[prog].enableQueryGeneration(options::sygusQueryGenThresh()); + emm->enableQueryGeneration(options::sygusQueryGenThresh()); } if (options::sygusFilterSolMode() != options::SygusFilterSolMode::NONE) @@ -901,18 +902,18 @@ void SynthConjecture::printSynthSolutionInternal(std::ostream& out) if (options::sygusFilterSolMode() == options::SygusFilterSolMode::STRONG) { - d_exprm[prog].enableFilterStrongSolutions(); + emm->enableFilterStrongSolutions(); } else if (options::sygusFilterSolMode() == options::SygusFilterSolMode::WEAK) { - d_exprm[prog].enableFilterWeakSolutions(); + emm->enableFilterWeakSolutions(); } } its = d_exprm.find(prog); } bool rew_print = false; - is_unique_term = d_exprm[prog].addTerm(sol, out, rew_print); + is_unique_term = its->second->addTerm(sol, out, rew_print); if (rew_print) { ++(d_stats.d_candidate_rewrites_print); diff --git a/src/theory/quantifiers/sygus/synth_conjecture.h b/src/theory/quantifiers/sygus/synth_conjecture.h index c1635c05c..9cc488fd2 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.h +++ b/src/theory/quantifiers/sygus/synth_conjecture.h @@ -363,7 +363,7 @@ class SynthConjecture * This is used for the sygusRewSynth() option to synthesize new candidate * rewrite rules. */ - std::map<Node, ExpressionMinerManager> d_exprm; + std::map<Node, std::unique_ptr<ExpressionMinerManager>> d_exprm; }; } // namespace quantifiers diff --git a/src/theory/quantifiers/sygus/synth_verify.cpp b/src/theory/quantifiers/sygus/synth_verify.cpp index 2d7255415..23ee0e648 100644 --- a/src/theory/quantifiers/sygus/synth_verify.cpp +++ b/src/theory/quantifiers/sygus/synth_verify.cpp @@ -19,7 +19,6 @@ #include "options/arith_options.h" #include "options/base_options.h" #include "options/quantifiers_options.h" -#include "smt/smt_engine_scope.h" #include "smt/smt_statistics_registry.h" #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/sygus/term_database_sygus.h" @@ -33,12 +32,11 @@ namespace cvc5 { namespace theory { namespace quantifiers { -SynthVerify::SynthVerify(TermDbSygus* tds) : d_tds(tds) +SynthVerify::SynthVerify(const Options& opts, TermDbSygus* tds) : d_tds(tds) { // determine the options to use for the verification subsolvers we spawn - // we start with the options of the current SmtEngine - SmtEngine* smtCurr = smt::currentSmtEngine(); - d_subOptions.copyValues(smtCurr->getOptions()); + // we start with the provided options + d_subOptions.copyValues(opts); // limit the number of instantiation rounds on subcalls d_subOptions.quantifiers.instMaxRounds = d_subOptions.quantifiers.sygusVerifyInstMaxRounds; diff --git a/src/theory/quantifiers/sygus/synth_verify.h b/src/theory/quantifiers/sygus/synth_verify.h index 794908ee5..c4d1052da 100644 --- a/src/theory/quantifiers/sygus/synth_verify.h +++ b/src/theory/quantifiers/sygus/synth_verify.h @@ -34,7 +34,7 @@ namespace quantifiers { class SynthVerify { public: - SynthVerify(TermDbSygus* tds); + SynthVerify(const Options& opts, TermDbSygus* tds); ~SynthVerify(); /** * Verification call, which takes into account specific aspects of the |