diff options
Diffstat (limited to 'src/theory/quantifiers/sygus')
31 files changed, 122 insertions, 182 deletions
diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp index d2c616238..9c43e8b51 100644 --- a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp +++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp @@ -228,6 +228,9 @@ bool CegSingleInv::solve() // solve the single invocation conjecture using a fresh copy of SMT engine std::unique_ptr<SmtEngine> siSmt; initializeSubsolver(siSmt, d_env); + // do not use shared selectors in subsolver, since this leads to solutions + // with non-user symbols + siSmt->setOption("dt-share-sel", "false"); siSmt->assertFormula(siq); Result r = siSmt->checkSat(); Trace("sygus-si") << "Result: " << r << std::endl; @@ -400,7 +403,7 @@ Node CegSingleInv::getSolutionFromInst(size_t index) } //simplify the solution using the extended rewriter Trace("csi-sol") << "Solution (pre-simplification): " << s << std::endl; - s = d_treg.getTermDatabaseSygus()->getExtRewriter()->extendedRewrite(s); + s = extendedRewrite(s); Trace("csi-sol") << "Solution (post-simplification): " << s << std::endl; // wrap into lambda, as needed return SygusUtils::wrapSolutionForSynthFun(prog, s); @@ -467,7 +470,7 @@ Node CegSingleInv::reconstructToSyntax(Node s, { Trace("csi-sol") << "Post-process solution..." << std::endl; Node prev = sol; - sol = d_treg.getTermDatabaseSygus()->getExtRewriter()->extendedRewrite(sol); + sol = extendedRewrite(sol); if (prev != sol) { Trace("csi-sol") << "Solution (after post process) : " << sol diff --git a/src/theory/quantifiers/sygus/cegis.cpp b/src/theory/quantifiers/sygus/cegis.cpp index 57b763044..f5774c761 100644 --- a/src/theory/quantifiers/sygus/cegis.cpp +++ b/src/theory/quantifiers/sygus/cegis.cpp @@ -32,11 +32,12 @@ namespace cvc5 { namespace theory { namespace quantifiers { -Cegis::Cegis(QuantifiersState& qs, +Cegis::Cegis(Env& env, + QuantifiersState& qs, QuantifiersInferenceManager& qim, TermDbSygus* tds, SynthConjecture* p) - : SygusModule(qs, qim, tds, p), + : SygusModule(env, qs, qim, tds, p), d_eval_unfold(tds->getEvalUnfold()), d_usingSymCons(false) { @@ -345,7 +346,7 @@ void Cegis::addRefinementLemma(Node lem) d_rl_vals.end()); } // rewrite with extended rewriter - slem = d_tds->getExtRewriter()->extendedRewrite(slem); + slem = d_tds->rewriteNode(slem); // collect all variables in slem expr::getSymbols(slem, d_refinement_lemma_vars); std::vector<Node> waiting; @@ -509,7 +510,7 @@ bool Cegis::getRefinementEvalLemmas(const std::vector<Node>& vs, Node lemcs = lem.substitute(vs.begin(), vs.end(), ms.begin(), ms.end()); Trace("sygus-cref-eval2") << "...under substitution it is : " << lemcs << std::endl; - Node lemcsu = vsit.doEvaluateWithUnfolding(d_tds, lemcs); + Node lemcsu = d_tds->rewriteNode(lemcs); Trace("sygus-cref-eval2") << "...after unfolding is : " << lemcsu << std::endl; if (lemcsu.isConst() && !lemcsu.getConst<bool>()) diff --git a/src/theory/quantifiers/sygus/cegis.h b/src/theory/quantifiers/sygus/cegis.h index d6678a305..d72805950 100644 --- a/src/theory/quantifiers/sygus/cegis.h +++ b/src/theory/quantifiers/sygus/cegis.h @@ -19,6 +19,8 @@ #define CVC5__THEORY__QUANTIFIERS__CEGIS_H #include <map> + +#include "smt/env_obj.h" #include "theory/quantifiers/sygus/sygus_module.h" #include "theory/quantifiers/sygus_sampler.h" @@ -42,7 +44,8 @@ namespace quantifiers { class Cegis : public SygusModule { public: - Cegis(QuantifiersState& qs, + Cegis(Env& env, + QuantifiersState& qs, QuantifiersInferenceManager& qim, TermDbSygus* tds, SynthConjecture* p); diff --git a/src/theory/quantifiers/sygus/cegis_core_connective.cpp b/src/theory/quantifiers/sygus/cegis_core_connective.cpp index 9a9d8f02d..a42323227 100644 --- a/src/theory/quantifiers/sygus/cegis_core_connective.cpp +++ b/src/theory/quantifiers/sygus/cegis_core_connective.cpp @@ -68,11 +68,12 @@ bool VariadicTrie::hasSubset(const std::vector<Node>& is) const return false; } -CegisCoreConnective::CegisCoreConnective(QuantifiersState& qs, +CegisCoreConnective::CegisCoreConnective(Env& env, + QuantifiersState& qs, QuantifiersInferenceManager& qim, TermDbSygus* tds, SynthConjecture* p) - : Cegis(qs, qim, tds, p) + : Cegis(env, qs, qim, tds, p) { d_true = NodeManager::currentNM()->mkConst(true); d_false = NodeManager::currentNM()->mkConst(false); @@ -629,9 +630,7 @@ bool CegisCoreConnective::getUnsatCore( Result CegisCoreConnective::checkSat(Node n, std::vector<Node>& mvs) const { Trace("sygus-ccore-debug") << "...check-sat " << n << "..." << std::endl; - Env& env = d_qstate.getEnv(); - Result r = - checkWithSubsolver(n, d_vars, mvs, env.getOptions(), env.getLogicInfo()); + Result r = checkWithSubsolver(n, d_vars, mvs, options(), logicInfo()); Trace("sygus-ccore-debug") << "...got " << r << std::endl; return r; } @@ -739,7 +738,7 @@ Node CegisCoreConnective::constructSolutionFromPool(Component& ccheck, addSuccess = false; // try a new core std::unique_ptr<SmtEngine> checkSol; - initializeSubsolver(checkSol, d_qstate.getEnv()); + initializeSubsolver(checkSol, d_env); Trace("sygus-ccore") << "----- Check candidate " << an << std::endl; std::vector<Node> rasserts = asserts; rasserts.push_back(d_sc); @@ -779,7 +778,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, d_qstate.getEnv()); + initializeSubsolver(checkSc, d_env); 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 e9a73e9bb..80ba6f26e 100644 --- a/src/theory/quantifiers/sygus/cegis_core_connective.h +++ b/src/theory/quantifiers/sygus/cegis_core_connective.h @@ -22,6 +22,7 @@ #include "expr/node.h" #include "expr/node_trie.h" +#include "smt/env_obj.h" #include "theory/evaluator.h" #include "theory/quantifiers/sygus/cegis.h" #include "util/result.h" @@ -160,7 +161,8 @@ class VariadicTrie class CegisCoreConnective : public Cegis { public: - CegisCoreConnective(QuantifiersState& qs, + CegisCoreConnective(Env& env, + QuantifiersState& qs, QuantifiersInferenceManager& qim, TermDbSygus* tds, SynthConjecture* p); diff --git a/src/theory/quantifiers/sygus/cegis_unif.cpp b/src/theory/quantifiers/sygus/cegis_unif.cpp index 797aecdab..871a85fbd 100644 --- a/src/theory/quantifiers/sygus/cegis_unif.cpp +++ b/src/theory/quantifiers/sygus/cegis_unif.cpp @@ -30,13 +30,14 @@ namespace cvc5 { namespace theory { namespace quantifiers { -CegisUnif::CegisUnif(QuantifiersState& qs, +CegisUnif::CegisUnif(Env& env, + QuantifiersState& qs, QuantifiersInferenceManager& qim, TermDbSygus* tds, SynthConjecture* p) - : Cegis(qs, qim, tds, p), - d_sygus_unif(qs.getEnv(), p), - d_u_enum_manager(qs, qim, tds, p) + : Cegis(env, qs, qim, tds, p), + d_sygus_unif(env, p), + d_u_enum_manager(env, qs, qim, tds, p) { } @@ -403,6 +404,7 @@ void CegisUnif::registerRefinementLemma(const std::vector<Node>& vars, Node lem) } CegisUnifEnumDecisionStrategy::CegisUnifEnumDecisionStrategy( + Env& env, QuantifiersState& qs, QuantifiersInferenceManager& qim, TermDbSygus* tds, diff --git a/src/theory/quantifiers/sygus/cegis_unif.h b/src/theory/quantifiers/sygus/cegis_unif.h index 0cddff9c1..da47aabbe 100644 --- a/src/theory/quantifiers/sygus/cegis_unif.h +++ b/src/theory/quantifiers/sygus/cegis_unif.h @@ -20,6 +20,7 @@ #include <map> #include <vector> +#include "smt/env_obj.h" #include "theory/decision_strategy.h" #include "theory/quantifiers/sygus/cegis.h" #include "theory/quantifiers/sygus/sygus_unif_rl.h" @@ -49,7 +50,8 @@ namespace quantifiers { class CegisUnifEnumDecisionStrategy : public DecisionStrategyFmf { public: - CegisUnifEnumDecisionStrategy(QuantifiersState& qs, + CegisUnifEnumDecisionStrategy(Env& env, + QuantifiersState& qs, QuantifiersInferenceManager& qim, TermDbSygus* tds, SynthConjecture* parent); @@ -207,7 +209,8 @@ class CegisUnifEnumDecisionStrategy : public DecisionStrategyFmf class CegisUnif : public Cegis { public: - CegisUnif(QuantifiersState& qs, + CegisUnif(Env& env, + QuantifiersState& qs, QuantifiersInferenceManager& qim, TermDbSygus* tds, SynthConjecture* p); diff --git a/src/theory/quantifiers/sygus/enum_stream_substitution.cpp b/src/theory/quantifiers/sygus/enum_stream_substitution.cpp index f853ac8e8..a5be4ebd6 100644 --- a/src/theory/quantifiers/sygus/enum_stream_substitution.cpp +++ b/src/theory/quantifiers/sygus/enum_stream_substitution.cpp @@ -16,15 +16,16 @@ #include "theory/quantifiers/sygus/enum_stream_substitution.h" +#include <numeric> // for std::iota +#include <sstream> + #include "expr/dtype_cons.h" #include "options/base_options.h" #include "options/datatypes_options.h" #include "options/quantifiers_options.h" #include "printer/printer.h" #include "theory/quantifiers/sygus/term_database_sygus.h" - -#include <numeric> // for std::iota -#include <sstream> +#include "theory/rewriter.h" using namespace cvc5::kind; @@ -32,7 +33,7 @@ namespace cvc5 { namespace theory { namespace quantifiers { -EnumStreamPermutation::EnumStreamPermutation(quantifiers::TermDbSygus* tds) +EnumStreamPermutation::EnumStreamPermutation(TermDbSygus* tds) : d_tds(tds), d_first(true), d_curr_ind(0) { } @@ -124,8 +125,7 @@ Node EnumStreamPermutation::getNext() { d_first = false; Node bultin_value = d_tds->sygusToBuiltin(d_value, d_value.getType()); - d_perm_values.insert( - d_tds->getExtRewriter()->extendedRewrite(bultin_value)); + d_perm_values.insert(Rewriter::callExtendedRewrite(bultin_value)); return d_value; } unsigned n_classes = d_perm_state_class.size(); @@ -194,8 +194,7 @@ Node EnumStreamPermutation::getNext() << " ......perm builtin is " << bultin_perm_value; if (options::sygusSymBreakDynamic()) { - bultin_perm_value = - d_tds->getExtRewriter()->extendedRewrite(bultin_perm_value); + bultin_perm_value = Rewriter::callExtendedRewrite(bultin_perm_value); Trace("synth-stream-concrete-debug") << " and rewrites to " << bultin_perm_value; } @@ -515,8 +514,7 @@ Node EnumStreamSubstitution::getNext() d_tds->sygusToBuiltin(comb_value, comb_value.getType()); if (options::sygusSymBreakDynamic()) { - builtin_comb_value = - d_tds->getExtRewriter()->extendedRewrite(builtin_comb_value); + builtin_comb_value = Rewriter::callExtendedRewrite(builtin_comb_value); } if (Trace.isOn("synth-stream-concrete")) { diff --git a/src/theory/quantifiers/sygus/enum_value_manager.cpp b/src/theory/quantifiers/sygus/enum_value_manager.cpp index 8a2d70bfa..e7b3bbaa9 100644 --- a/src/theory/quantifiers/sygus/enum_value_manager.cpp +++ b/src/theory/quantifiers/sygus/enum_value_manager.cpp @@ -33,13 +33,15 @@ namespace cvc5 { namespace theory { namespace quantifiers { -EnumValueManager::EnumValueManager(Node e, +EnumValueManager::EnumValueManager(Env& env, QuantifiersState& qs, QuantifiersInferenceManager& qim, TermRegistry& tr, SygusStatistics& s, + Node e, bool hasExamples) - : d_enum(e), + : EnvObj(env), + d_enum(e), d_qstate(qs), d_qim(qim), d_treg(tr), @@ -108,7 +110,7 @@ Node EnumValueManager::getEnumeratedValue(bool& activeIncomplete) d_samplerRrV->initializeSygus( d_tds, e, options::sygusSamples(), false); // use the default output for the output of sygusRewVerify - out = d_qstate.options().base.out; + out = options().base.out; } d_secd.reset(new SygusEnumeratorCallbackDefault( e, &d_stats, d_eec.get(), d_samplerRrV.get(), out)); diff --git a/src/theory/quantifiers/sygus/enum_value_manager.h b/src/theory/quantifiers/sygus/enum_value_manager.h index c786bb6f1..23fdc7391 100644 --- a/src/theory/quantifiers/sygus/enum_value_manager.h +++ b/src/theory/quantifiers/sygus/enum_value_manager.h @@ -19,6 +19,7 @@ #define CVC5__THEORY__QUANTIFIERS__SYGUS__ENUM_VALUE_MANAGER_H #include "expr/node.h" +#include "smt/env_obj.h" #include "theory/quantifiers/sygus/enum_val_generator.h" #include "theory/quantifiers/sygus/example_eval_cache.h" #include "theory/quantifiers/sygus/sygus_enumerator_callback.h" @@ -38,14 +39,15 @@ class SygusStatistics; * not actively generated, or may be determined by the (fast) enumerator * when it is actively generated. */ -class EnumValueManager +class EnumValueManager : protected EnvObj { public: - EnumValueManager(Node e, + EnumValueManager(Env& env, QuantifiersState& qs, QuantifiersInferenceManager& qim, TermRegistry& tr, SygusStatistics& s, + Node e, bool hasExamples); ~EnumValueManager(); /** diff --git a/src/theory/quantifiers/sygus/sygus_enumerator_basic.cpp b/src/theory/quantifiers/sygus/sygus_enumerator_basic.cpp index f45b976ec..743f67cec 100644 --- a/src/theory/quantifiers/sygus/sygus_enumerator_basic.cpp +++ b/src/theory/quantifiers/sygus/sygus_enumerator_basic.cpp @@ -15,6 +15,7 @@ #include "theory/quantifiers/sygus/sygus_enumerator_basic.h" #include "options/datatypes_options.h" +#include "theory/rewriter.h" using namespace cvc5::kind; using namespace std; @@ -40,7 +41,7 @@ bool EnumValGeneratorBasic::increment() if (options::sygusSymBreakDynamic()) { Node nextb = d_tds->sygusToBuiltin(d_currTerm); - nextb = d_tds->getExtRewriter()->extendedRewrite(nextb); + nextb = Rewriter::callExtendedRewrite(nextb); if (d_cache.find(nextb) == d_cache.end()) { d_cache.insert(nextb); diff --git a/src/theory/quantifiers/sygus/sygus_enumerator_callback.cpp b/src/theory/quantifiers/sygus/sygus_enumerator_callback.cpp index 3b536695f..1b5b3f5af 100644 --- a/src/theory/quantifiers/sygus/sygus_enumerator_callback.cpp +++ b/src/theory/quantifiers/sygus/sygus_enumerator_callback.cpp @@ -19,6 +19,7 @@ #include "theory/quantifiers/sygus/example_eval_cache.h" #include "theory/quantifiers/sygus/sygus_stats.h" #include "theory/quantifiers/sygus_sampler.h" +#include "theory/rewriter.h" namespace cvc5 { namespace theory { @@ -33,7 +34,7 @@ SygusEnumeratorCallback::SygusEnumeratorCallback(Node e, SygusStatistics* s) bool SygusEnumeratorCallback::addTerm(Node n, std::unordered_set<Node>& bterms) { Node bn = datatypes::utils::sygusToBuiltin(n); - Node bnr = d_extr.extendedRewrite(bn); + Node bnr = Rewriter::callExtendedRewrite(bn); if (d_stats != nullptr) { ++(d_stats->d_enumTermsRewrite); diff --git a/src/theory/quantifiers/sygus/sygus_enumerator_callback.h b/src/theory/quantifiers/sygus/sygus_enumerator_callback.h index 5ed28b309..8689d876f 100644 --- a/src/theory/quantifiers/sygus/sygus_enumerator_callback.h +++ b/src/theory/quantifiers/sygus/sygus_enumerator_callback.h @@ -74,8 +74,6 @@ class SygusEnumeratorCallback Node d_enum; /** The type of enum */ TypeNode d_tn; - /** extended rewriter */ - ExtendedRewriter d_extr; /** pointer to the statistics */ SygusStatistics* d_stats; }; diff --git a/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp b/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp index 0ef1e7f17..7af1ef45b 100644 --- a/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp +++ b/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp @@ -180,7 +180,7 @@ void SygusEvalUnfold::registerModelValue(Node a, Node conj = nm->mkNode(DT_SYGUS_EVAL, eval_children); eval_children[0] = vn; Node eval_fun = nm->mkNode(DT_SYGUS_EVAL, eval_children); - res = d_tds->evaluateWithUnfolding(eval_fun); + res = d_tds->rewriteNode(eval_fun); Trace("sygus-eval-unfold") << "Evaluate with unfolding returns " << res << std::endl; esit.init(conj, n, res); @@ -324,13 +324,6 @@ Node SygusEvalUnfold::unfold(Node en, return ret; } -Node SygusEvalUnfold::unfold(Node en) -{ - std::map<Node, Node> vtm; - std::vector<Node> exp; - return unfold(en, vtm, exp, false, false); -} - } // namespace quantifiers } // namespace theory } // namespace cvc5 diff --git a/src/theory/quantifiers/sygus/sygus_eval_unfold.h b/src/theory/quantifiers/sygus/sygus_eval_unfold.h index bb181996a..c30d4dae7 100644 --- a/src/theory/quantifiers/sygus/sygus_eval_unfold.h +++ b/src/theory/quantifiers/sygus/sygus_eval_unfold.h @@ -122,11 +122,6 @@ class SygusEvalUnfold std::vector<Node>& exp, bool track_exp = true, bool doRec = false); - /** - * Same as above, but without explanation tracking. This is used for concrete - * evaluation heads - */ - Node unfold(Node en); private: /** sygus term database associated with this utility */ diff --git a/src/theory/quantifiers/sygus/sygus_grammar_red.cpp b/src/theory/quantifiers/sygus/sygus_grammar_red.cpp index a51fcce25..fd84f0c0a 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_red.cpp +++ b/src/theory/quantifiers/sygus/sygus_grammar_red.cpp @@ -21,6 +21,7 @@ #include "options/quantifiers_options.h" #include "theory/quantifiers/sygus/term_database_sygus.h" #include "theory/quantifiers/term_util.h" +#include "theory/rewriter.h" using namespace std; using namespace cvc5::kind; @@ -147,7 +148,7 @@ void SygusRedundantCons::getGenericList(TermDbSygus* tds, if (index == dt[c].getNumArgs()) { Node gt = tds->mkGeneric(dt, c, pre); - gt = tds->getExtRewriter()->extendedRewrite(gt); + gt = Rewriter::callExtendedRewrite(gt); terms.push_back(gt); return; } diff --git a/src/theory/quantifiers/sygus/sygus_invariance.cpp b/src/theory/quantifiers/sygus/sygus_invariance.cpp index cb7e2b84e..8048330e4 100644 --- a/src/theory/quantifiers/sygus/sygus_invariance.cpp +++ b/src/theory/quantifiers/sygus/sygus_invariance.cpp @@ -49,11 +49,6 @@ void EvalSygusInvarianceTest::init(Node conj, Node var, Node res) d_result = res; } -Node EvalSygusInvarianceTest::doEvaluateWithUnfolding(TermDbSygus* tds, Node n) -{ - return tds->evaluateWithUnfolding(n, d_visited); -} - bool EvalSygusInvarianceTest::invariant(TermDbSygus* tds, Node nvn, Node x) { TNode tnvn = nvn; @@ -61,7 +56,7 @@ bool EvalSygusInvarianceTest::invariant(TermDbSygus* tds, Node nvn, Node x) for (const Node& c : d_terms) { Node conj_subs = c.substitute(d_var, tnvn, cache); - Node conj_subs_unfold = doEvaluateWithUnfolding(tds, conj_subs); + Node conj_subs_unfold = tds->rewriteNode(conj_subs); Trace("sygus-cref-eval2-debug") << " ...check unfolding : " << conj_subs_unfold << std::endl; Trace("sygus-cref-eval2-debug") @@ -111,7 +106,7 @@ bool EquivSygusInvarianceTest::invariant(TermDbSygus* tds, Node nvn, Node x) { TypeNode tn = nvn.getType(); Node nbv = tds->sygusToBuiltin(nvn, tn); - Node nbvr = tds->getExtRewriter()->extendedRewrite(nbv); + Node nbvr = Rewriter::callExtendedRewrite(nbv); Trace("sygus-sb-mexp-debug") << " min-exp check : " << nbv << " -> " << nbvr << std::endl; bool exc_arg = false; @@ -181,7 +176,7 @@ bool DivByZeroSygusInvarianceTest::invariant(TermDbSygus* tds, Node nvn, Node x) { TypeNode tn = nvn.getType(); Node nbv = tds->sygusToBuiltin(nvn, tn); - Node nbvr = tds->getExtRewriter()->extendedRewrite(nbv); + Node nbvr = Rewriter::callExtendedRewrite(nbv); if (tds->involvesDivByZero(nbvr)) { Trace("sygus-sb-mexp") << "sb-min-exp : " << tds->sygusToBuiltin(nvn) @@ -212,7 +207,7 @@ bool NegContainsSygusInvarianceTest::invariant(TermDbSygus* tds, { TypeNode tn = nvn.getType(); Node nbv = tds->sygusToBuiltin(nvn, tn); - Node nbvr = tds->getExtRewriter()->extendedRewrite(nbv); + Node nbvr = Rewriter::callExtendedRewrite(nbv); // if for any of the examples, it is not contained, then we can exclude for (unsigned i = 0; i < d_neg_con_indices.size(); i++) { diff --git a/src/theory/quantifiers/sygus/sygus_invariance.h b/src/theory/quantifiers/sygus/sygus_invariance.h index ca5f057b1..afb59bf73 100644 --- a/src/theory/quantifiers/sygus/sygus_invariance.h +++ b/src/theory/quantifiers/sygus/sygus_invariance.h @@ -111,9 +111,6 @@ class EvalSygusInvarianceTest : public SygusInvarianceTest */ void init(Node conj, Node var, Node res); - /** do evaluate with unfolding, using the cache of this class */ - Node doEvaluateWithUnfolding(TermDbSygus* tds, Node n); - protected: /** does d_terms{ d_var -> nvn } still rewrite to d_result? */ bool invariant(TermDbSygus* tds, Node nvn, Node x) override; @@ -137,8 +134,6 @@ class EvalSygusInvarianceTest : public SygusInvarianceTest * disjunctively, i.e. if one child test succeeds, the overall test succeeds. */ bool d_is_conjunctive; - /** cache of n -> the simplified form of eval( n ) */ - std::unordered_map<Node, Node> d_visited; }; /** EquivSygusInvarianceTest diff --git a/src/theory/quantifiers/sygus/sygus_module.cpp b/src/theory/quantifiers/sygus/sygus_module.cpp index 8272c6418..1840f0eb1 100644 --- a/src/theory/quantifiers/sygus/sygus_module.cpp +++ b/src/theory/quantifiers/sygus/sygus_module.cpp @@ -21,11 +21,12 @@ namespace cvc5 { namespace theory { namespace quantifiers { -SygusModule::SygusModule(QuantifiersState& qs, +SygusModule::SygusModule(Env& env, + QuantifiersState& qs, QuantifiersInferenceManager& qim, TermDbSygus* tds, SynthConjecture* p) - : EnvObj(qs.getEnv()), d_qstate(qs), d_qim(qim), d_tds(tds), d_parent(p) + : EnvObj(env), 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 8070fe009..8ee1fc9b4 100644 --- a/src/theory/quantifiers/sygus/sygus_module.h +++ b/src/theory/quantifiers/sygus/sygus_module.h @@ -53,7 +53,8 @@ class QuantifiersInferenceManager; class SygusModule : protected EnvObj { public: - SygusModule(QuantifiersState& qs, + SygusModule(Env& env, + QuantifiersState& qs, QuantifiersInferenceManager& qim, TermDbSygus* tds, SynthConjecture* p); diff --git a/src/theory/quantifiers/sygus/sygus_pbe.cpp b/src/theory/quantifiers/sygus/sygus_pbe.cpp index 7601e2117..453ac5c18 100644 --- a/src/theory/quantifiers/sygus/sygus_pbe.cpp +++ b/src/theory/quantifiers/sygus/sygus_pbe.cpp @@ -30,11 +30,12 @@ namespace cvc5 { namespace theory { namespace quantifiers { -SygusPbe::SygusPbe(QuantifiersState& qs, +SygusPbe::SygusPbe(Env& env, + QuantifiersState& qs, QuantifiersInferenceManager& qim, TermDbSygus* tds, SynthConjecture* p) - : SygusModule(qs, qim, tds, p) + : SygusModule(env, qs, qim, tds, p) { d_true = NodeManager::currentNM()->mkConst(true); d_false = NodeManager::currentNM()->mkConst(false); @@ -131,7 +132,7 @@ bool SygusPbe::initialize(Node conj, // Apply extended rewriting on the lemma. This helps utilities like // SygusEnumerator more easily recognize the shape of this lemma, e.g. // ( ~is-ite(x) or ( ~is-ite(x) ^ P ) ) --> ~is-ite(x). - lem = d_tds->getExtRewriter()->extendedRewrite(lem); + lem = extendedRewrite(lem); Trace("sygus-pbe") << " static redundant op lemma : " << lem << std::endl; // Register as a symmetry breaking lemma with the term database. diff --git a/src/theory/quantifiers/sygus/sygus_pbe.h b/src/theory/quantifiers/sygus/sygus_pbe.h index 867764617..e55479e18 100644 --- a/src/theory/quantifiers/sygus/sygus_pbe.h +++ b/src/theory/quantifiers/sygus/sygus_pbe.h @@ -18,6 +18,7 @@ #ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_PBE_H #define CVC5__THEORY__QUANTIFIERS__SYGUS_PBE_H +#include "smt/env_obj.h" #include "theory/quantifiers/sygus/sygus_module.h" namespace cvc5 { @@ -86,7 +87,8 @@ class SynthConjecture; class SygusPbe : public SygusModule { public: - SygusPbe(QuantifiersState& qs, + SygusPbe(Env& env, + QuantifiersState& qs, QuantifiersInferenceManager& qim, TermDbSygus* tds, SynthConjecture* p); diff --git a/src/theory/quantifiers/sygus/sygus_repair_const.cpp b/src/theory/quantifiers/sygus/sygus_repair_const.cpp index bcd826799..b7611784d 100644 --- a/src/theory/quantifiers/sygus/sygus_repair_const.cpp +++ b/src/theory/quantifiers/sygus/sygus_repair_const.cpp @@ -444,7 +444,7 @@ Node SygusRepairConst::getFoQuery(Node body, Trace("sygus-repair-const-debug") << " ...got : " << body << std::endl; Trace("sygus-repair-const") << " Unfold the specification..." << std::endl; - body = d_tds->evaluateWithUnfolding(body); + body = d_tds->rewriteNode(body); Trace("sygus-repair-const-debug") << " ...got : " << body << std::endl; Trace("sygus-repair-const") << " Introduce first-order vars..." << std::endl; diff --git a/src/theory/quantifiers/sygus/sygus_unif_io.cpp b/src/theory/quantifiers/sygus/sygus_unif_io.cpp index 9626f7af4..3fb80f917 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_io.cpp +++ b/src/theory/quantifiers/sygus/sygus_unif_io.cpp @@ -569,7 +569,7 @@ void SygusUnifIo::notifyEnumeration(Node e, Node v, std::vector<Node>& lemmas) std::vector<Node> base_results; TypeNode xtn = e.getType(); Node bv = d_tds->sygusToBuiltin(v, xtn); - bv = d_tds->getExtRewriter()->extendedRewrite(bv); + bv = extendedRewrite(bv); Trace("sygus-sui-enum") << "PBE Compute Examples for " << bv << std::endl; // compte the results (should be cached) ExampleEvalCache* eec = d_parent->getExampleEvalCache(e); diff --git a/src/theory/quantifiers/sygus/sygus_unif_strat.cpp b/src/theory/quantifiers/sygus/sygus_unif_strat.cpp index 10db1ef9e..6b023075b 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_strat.cpp +++ b/src/theory/quantifiers/sygus/sygus_unif_strat.cpp @@ -264,7 +264,7 @@ void SygusUnifStrategy::buildStrategyGraph(TypeNode tn, NodeRole nrole) Node eut = nm->mkNode(DT_SYGUS_EVAL, echildren); Trace("sygus-unif-debug2") << " Test evaluation of " << eut << "..." << std::endl; - eut = d_tds->getEvalUnfold()->unfold(eut); + eut = d_tds->rewriteNode(eut); Trace("sygus-unif-debug2") << " ...got " << eut; Trace("sygus-unif-debug2") << ", type : " << eut.getType() << std::endl; diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp index 3e7095c12..da021227a 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.cpp +++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp @@ -45,29 +45,31 @@ namespace cvc5 { namespace theory { namespace quantifiers { -SynthConjecture::SynthConjecture(QuantifiersState& qs, +SynthConjecture::SynthConjecture(Env& env, + QuantifiersState& qs, QuantifiersInferenceManager& qim, QuantifiersRegistry& qr, TermRegistry& tr, SygusStatistics& s) - : d_qstate(qs), + : EnvObj(env), + d_qstate(qs), d_qim(qim), d_qreg(qr), d_treg(tr), d_stats(s), d_tds(tr.getTermDatabaseSygus()), - d_verify(qs.options(), qs.getLogicInfo(), d_tds), + d_verify(options(), qs.getLogicInfo(), d_tds), d_hasSolution(false), - d_ceg_si(new CegSingleInv(qs.getEnv(), tr, s)), + d_ceg_si(new CegSingleInv(env, tr, s)), d_templInfer(new SygusTemplateInfer), d_ceg_proc(new SynthConjectureProcess), d_ceg_gc(new CegGrammarConstructor(d_tds, this)), - d_sygus_rconst(new SygusRepairConst(qs.getEnv(), d_tds)), + d_sygus_rconst(new SygusRepairConst(env, d_tds)), d_exampleInfer(new ExampleInfer(d_tds)), - 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(qs, qim, d_tds, this)), + d_ceg_pbe(new SygusPbe(env, qs, qim, d_tds, this)), + d_ceg_cegis(new Cegis(env, qs, qim, d_tds, this)), + d_ceg_cegisUnif(new CegisUnif(env, qs, qim, d_tds, this)), + d_sygus_ccore(new CegisCoreConnective(env, qs, qim, d_tds, this)), d_master(nullptr), d_set_ce_sk_vars(false), d_repair_index(0), @@ -513,7 +515,7 @@ bool SynthConjecture::doCheck() { if (printDebug) { - const Options& sopts = d_qstate.options(); + const Options& sopts = options(); std::ostream& out = *sopts.base.out; out << "(sygus-candidate "; Assert(d_quant[0].getNumChildren() == candidate_values.size()); @@ -609,8 +611,7 @@ 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; - Env& env = d_qstate.getEnv(); - Result r = checkWithSubsolver(sc, env.getOptions(), env.getLogicInfo()); + Result r = checkWithSubsolver(sc, options(), logicInfo()); Trace("cegqi-debug") << "...got side condition : " << r << std::endl; if (r == Result::UNSAT) { @@ -763,8 +764,8 @@ EnumValueManager* SynthConjecture::getEnumValueManagerFor(Node e) Node f = d_tds->getSynthFunForEnumerator(e); bool hasExamples = (d_exampleInfer->hasExamples(f) && d_exampleInfer->getNumExamples(f) != 0); - d_enumManager[e].reset( - new EnumValueManager(e, d_qstate, d_qim, d_treg, d_stats, hasExamples)); + d_enumManager[e].reset(new EnumValueManager( + d_env, d_qstate, d_qim, d_treg, d_stats, e, hasExamples)); EnumValueManager* eman = d_enumManager[e].get(); // set up the examples if (hasExamples) @@ -800,8 +801,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 - const Options& sopts = d_qstate.options(); - printSynthSolutionInternal(*sopts.base.out); + printSynthSolutionInternal(*options().base.out); excludeCurrentSolution(enums, values); } @@ -885,7 +885,7 @@ void SynthConjecture::printSynthSolutionInternal(std::ostream& out) d_exprm.find(prog); if (its == d_exprm.end()) { - d_exprm[prog].reset(new ExpressionMinerManager(d_qstate.getEnv())); + d_exprm[prog].reset(new ExpressionMinerManager(d_env)); ExpressionMinerManager* emm = d_exprm[prog].get(); emm->initializeSygus( d_tds, d_candidates[i], options::sygusSamples(), true); diff --git a/src/theory/quantifiers/sygus/synth_conjecture.h b/src/theory/quantifiers/sygus/synth_conjecture.h index 9cc488fd2..d7635c816 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.h +++ b/src/theory/quantifiers/sygus/synth_conjecture.h @@ -21,6 +21,7 @@ #include <memory> +#include "smt/env_obj.h" #include "theory/quantifiers/expr_miner_manager.h" #include "theory/quantifiers/sygus/ce_guided_single_inv.h" #include "theory/quantifiers/sygus/cegis.h" @@ -51,10 +52,11 @@ class EnumValueManager; * determines which approach and optimizations are applicable to the * conjecture, and has interfaces for implementing them. */ -class SynthConjecture +class SynthConjecture : protected EnvObj { public: - SynthConjecture(QuantifiersState& qs, + SynthConjecture(Env& env, + QuantifiersState& qs, QuantifiersInferenceManager& qim, QuantifiersRegistry& qr, TermRegistry& tr, diff --git a/src/theory/quantifiers/sygus/synth_engine.cpp b/src/theory/quantifiers/sygus/synth_engine.cpp index cdcbeb85d..454442351 100644 --- a/src/theory/quantifiers/sygus/synth_engine.cpp +++ b/src/theory/quantifiers/sygus/synth_engine.cpp @@ -26,14 +26,15 @@ namespace cvc5 { namespace theory { namespace quantifiers { -SynthEngine::SynthEngine(QuantifiersState& qs, +SynthEngine::SynthEngine(Env& env, + QuantifiersState& qs, QuantifiersInferenceManager& qim, QuantifiersRegistry& qr, TermRegistry& tr) - : QuantifiersModule(qs, qim, qr, tr), d_conj(nullptr), d_sqp(qs.getEnv()) + : QuantifiersModule(env, qs, qim, qr, tr), d_conj(nullptr), d_sqp(env) { d_conjs.push_back(std::unique_ptr<SynthConjecture>( - new SynthConjecture(qs, qim, qr, tr, d_statistics))); + new SynthConjecture(env, qs, qim, qr, tr, d_statistics))); d_conj = d_conjs.back().get(); } @@ -153,8 +154,8 @@ void SynthEngine::assignConjecture(Node q) // allocate a new synthesis conjecture if not assigned if (d_conjs.back()->isAssigned()) { - d_conjs.push_back(std::unique_ptr<SynthConjecture>( - new SynthConjecture(d_qstate, d_qim, d_qreg, d_treg, d_statistics))); + d_conjs.push_back(std::unique_ptr<SynthConjecture>(new SynthConjecture( + d_env, d_qstate, d_qim, d_qreg, d_treg, d_statistics))); } d_conjs.back()->assign(q); } diff --git a/src/theory/quantifiers/sygus/synth_engine.h b/src/theory/quantifiers/sygus/synth_engine.h index d37df4e28..c623d9c0f 100644 --- a/src/theory/quantifiers/sygus/synth_engine.h +++ b/src/theory/quantifiers/sygus/synth_engine.h @@ -34,7 +34,8 @@ class SynthEngine : public QuantifiersModule typedef context::CDHashMap<Node, bool> NodeBoolMap; public: - SynthEngine(QuantifiersState& qs, + SynthEngine(Env& env, + QuantifiersState& qs, QuantifiersInferenceManager& qim, QuantifiersRegistry& qr, TermRegistry& tr); diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp index 3b0ea3312..035db433e 100644 --- a/src/theory/quantifiers/sygus/term_database_sygus.cpp +++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp @@ -51,10 +51,10 @@ std::ostream& operator<<(std::ostream& os, EnumeratorRole r) return os; } -TermDbSygus::TermDbSygus(QuantifiersState& qs) - : d_qstate(qs), +TermDbSygus::TermDbSygus(Env& env, QuantifiersState& qs) + : EnvObj(env), + d_qstate(qs), d_syexp(new SygusExplain(this)), - d_ext_rw(new ExtendedRewriter(true)), d_eval(new Evaluator), d_funDefEval(new FunDefEvaluator), d_eval_unfold(new SygusEvalUnfold(this)) @@ -739,7 +739,15 @@ SygusTypeInfo& TermDbSygus::getTypeInfo(TypeNode tn) Node TermDbSygus::rewriteNode(Node n) const { - Node res = Rewriter::rewrite(n); + Node res; + if (options().quantifiers.sygusExtRew) + { + res = extendedRewrite(n); + } + else + { + res = rewrite(n); + } if (res.isConst()) { // constant, we are done @@ -1001,59 +1009,6 @@ Node TermDbSygus::evaluateBuiltin(TypeNode tn, return rewriteNode(res); } -Node TermDbSygus::evaluateWithUnfolding(Node n, - std::unordered_map<Node, Node>& visited) -{ - std::unordered_map<Node, Node>::iterator it = visited.find(n); - if( it==visited.end() ){ - Node ret = n; - while (ret.getKind() == DT_SYGUS_EVAL - && ret[0].getKind() == APPLY_CONSTRUCTOR) - { - if (ret == n && ret[0].isConst()) - { - // use rewriting, possibly involving recursive functions - ret = rewriteNode(ret); - } - else - { - ret = d_eval_unfold->unfold(ret); - } - } - if( ret.getNumChildren()>0 ){ - std::vector< Node > children; - if( ret.getMetaKind() == kind::metakind::PARAMETERIZED ){ - children.push_back( ret.getOperator() ); - } - bool childChanged = false; - for( unsigned i=0; i<ret.getNumChildren(); i++ ){ - Node nc = evaluateWithUnfolding(ret[i], visited); - childChanged = childChanged || nc!=ret[i]; - children.push_back( nc ); - } - if( childChanged ){ - ret = NodeManager::currentNM()->mkNode( ret.getKind(), children ); - } - if (options::sygusExtRew()) - { - ret = getExtRewriter()->extendedRewrite(ret); - } - // use rewriting, possibly involving recursive functions - ret = rewriteNode(ret); - } - visited[n] = ret; - return ret; - }else{ - return it->second; - } -} - -Node TermDbSygus::evaluateWithUnfolding(Node n) -{ - std::unordered_map<Node, Node> visited; - return evaluateWithUnfolding(n, visited); -} - bool TermDbSygus::isEvaluationPoint(Node n) const { if (n.getKind() != DT_SYGUS_EVAL) diff --git a/src/theory/quantifiers/sygus/term_database_sygus.h b/src/theory/quantifiers/sygus/term_database_sygus.h index 80411b258..7b05c70e4 100644 --- a/src/theory/quantifiers/sygus/term_database_sygus.h +++ b/src/theory/quantifiers/sygus/term_database_sygus.h @@ -21,6 +21,7 @@ #include <unordered_set> #include "expr/dtype.h" +#include "smt/env_obj.h" #include "theory/evaluator.h" #include "theory/quantifiers/extended_rewrite.h" #include "theory/quantifiers/fun_def_evaluator.h" @@ -53,9 +54,10 @@ enum EnumeratorRole std::ostream& operator<<(std::ostream& os, EnumeratorRole r); // TODO :issue #1235 split and document this class -class TermDbSygus { +class TermDbSygus : protected EnvObj +{ public: - TermDbSygus(QuantifiersState& qs); + TermDbSygus(Env& env, QuantifiersState& qs); ~TermDbSygus() {} /** Finish init, which sets the inference manager */ void finishInit(QuantifiersInferenceManager* qim); @@ -78,8 +80,6 @@ class TermDbSygus { //------------------------------utilities /** get the explanation utility */ SygusExplain* getExplain() { return d_syexp.get(); } - /** get the extended rewrite utility */ - ExtendedRewriter* getExtRewriter() { return d_ext_rw.get(); } /** get the evaluator */ Evaluator* getEvaluator() { return d_eval.get(); } /** (recursive) function evaluator utility */ @@ -271,21 +271,6 @@ class TermDbSygus { Node bn, const std::vector<Node>& args, bool tryEval = true); - /** evaluate with unfolding - * - * n is any term that may involve sygus evaluation functions. This function - * returns the result of unfolding the evaluation functions within n and - * rewriting the result. For example, if eval_A is the evaluation function - * for the datatype: - * A -> C_0 | C_1 | C_x | C_+( C_A, C_A ) - * corresponding to grammar: - * A -> 0 | 1 | x | A + A - * then calling this function on eval( C_+( x, 1 ), 4 ) = y returns 5 = y. - * The node returned by this function is in (extended) rewritten form. - */ - Node evaluateWithUnfolding(Node n); - /** same as above, but with a cache of visited nodes */ - Node evaluateWithUnfolding(Node n, std::unordered_map<Node, Node>& visited); /** is evaluation point? * * Returns true if n is of the form eval( x, c1...cn ) for some variable x @@ -324,8 +309,6 @@ class TermDbSygus { //------------------------------utilities /** sygus explanation */ std::unique_ptr<SygusExplain> d_syexp; - /** extended rewriter */ - std::unique_ptr<ExtendedRewriter> d_ext_rw; /** evaluator */ std::unique_ptr<Evaluator> d_eval; /** (recursive) function evaluator utility */ @@ -461,7 +444,6 @@ class TermDbSygus { /** get anchor */ static Node getAnchor( Node n ); static unsigned getAnchorDepth( Node n ); - }; } // namespace quantifiers |