From 50ad99bbbefe6a9ff2ed58995e8305ff0c121abf Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 3 Jun 2022 08:59:59 -0500 Subject: [PATCH] Eliminate static options access from pattern term selector (#8825) Towards eliminating options scopes. --- .../ematching/inst_strategy_e_matching.cpp | 3 +- .../inst_strategy_e_matching_user.cpp | 3 +- .../ematching/pattern_term_selector.cpp | 65 +++++++++++-------- .../ematching/pattern_term_selector.h | 23 ++++--- src/theory/quantifiers/quantifiers_macros.cpp | 11 +++- src/theory/quantifiers/quantifiers_macros.h | 6 +- src/theory/quantifiers/theory_quantifiers.cpp | 2 +- 7 files changed, 71 insertions(+), 42 deletions(-) diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp index 52aa1538f..42c88e040 100644 --- a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp +++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp @@ -414,7 +414,8 @@ bool InstStrategyAutoGenTriggers::generatePatternTerms(Node f) if (patTermsF.empty()) { Node bd = d_qreg.getInstConstantBody(f); - PatternTermSelector pts(f, d_tr_strategy, d_user_no_gen[f], true); + PatternTermSelector pts( + d_env.getOptions(), f, d_tr_strategy, d_user_no_gen[f], true); pts.collect(bd, patTermsF, tinfo); if (ntrivTriggers) { diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.cpp b/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.cpp index ffb8932cc..021c88233 100644 --- a/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.cpp +++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.cpp @@ -122,6 +122,7 @@ void InstStrategyUserPatterns::addUserPattern(Node q, Node pat) Assert(pat.getKind() == INST_PATTERN); // add to generators std::vector nodes; + const Options& opts = d_env.getOptions(); for (const Node& p : pat) { if (std::find(nodes.begin(), nodes.end(), p) != nodes.end()) @@ -129,7 +130,7 @@ void InstStrategyUserPatterns::addUserPattern(Node q, Node pat) // skip duplicate pattern term continue; } - Node pat_use = PatternTermSelector::getIsUsableTrigger(p, q); + Node pat_use = PatternTermSelector::getIsUsableTrigger(opts, p, q); if (pat_use.isNull()) { Trace("trigger-warn") << "User-provided trigger is not usable : " << pat diff --git a/src/theory/quantifiers/ematching/pattern_term_selector.cpp b/src/theory/quantifiers/ematching/pattern_term_selector.cpp index 740d0e903..20f131277 100644 --- a/src/theory/quantifiers/ematching/pattern_term_selector.cpp +++ b/src/theory/quantifiers/ematching/pattern_term_selector.cpp @@ -29,17 +29,22 @@ namespace theory { namespace quantifiers { namespace inst { -PatternTermSelector::PatternTermSelector(Node q, +PatternTermSelector::PatternTermSelector(const Options& opts, + Node q, options::TriggerSelMode tstrt, const std::vector& exc, bool filterInst) - : d_quant(q), d_tstrt(tstrt), d_excluded(exc), d_filterInst(filterInst) + : d_opts(opts), + d_quant(q), + d_tstrt(tstrt), + d_excluded(exc), + d_filterInst(filterInst) { } PatternTermSelector::~PatternTermSelector() {} -bool PatternTermSelector::isUsable(Node n, Node q) +bool PatternTermSelector::isUsable(const Options& opts, Node n, Node q) { if (quantifiers::TermUtil::getInstConstAttr(n) != q) { @@ -49,7 +54,7 @@ bool PatternTermSelector::isUsable(Node n, Node q) { for (const Node& nc : n) { - if (!isUsable(nc, q)) + if (!isUsable(opts, nc, q)) { return false; } @@ -60,7 +65,7 @@ bool PatternTermSelector::isUsable(Node n, Node q) { return true; } - if (options::purifyTriggers()) + if (opts.quantifiers.purifyTriggers) { Node x = getInversionVariable(n); if (!x.isNull()) @@ -71,12 +76,12 @@ bool PatternTermSelector::isUsable(Node n, Node q) return false; } -Node PatternTermSelector::getIsUsableEq(Node q, Node n) +Node PatternTermSelector::getIsUsableEq(const Options& opts, Node q, Node n) { Assert(TriggerTermInfo::isRelationalTrigger(n)); for (size_t i = 0; i < 2; i++) { - if (isUsableEqTerms(q, n[i], n[1 - i])) + if (isUsableEqTerms(opts, q, n[i], n[1 - i])) { if (i == 1 && n.getKind() == EQUAL && !quantifiers::TermUtil::hasInstConstAttr(n[0])) @@ -92,11 +97,14 @@ Node PatternTermSelector::getIsUsableEq(Node q, Node n) return Node::null(); } -bool PatternTermSelector::isUsableEqTerms(Node q, Node n1, Node n2) +bool PatternTermSelector::isUsableEqTerms(const Options& opts, + Node q, + Node n1, + Node n2) { if (n1.getKind() == INST_CONSTANT) { - if (options::relationalTriggers()) + if (opts.quantifiers.relationalTriggers) { Node q1 = quantifiers::TermUtil::getInstConstAttr(n1); if (q1 != q) @@ -119,9 +127,9 @@ bool PatternTermSelector::isUsableEqTerms(Node q, Node n1, Node n2) // when n1 and n2 are swapped } } - else if (isUsableAtomicTrigger(n1, q)) + else if (isUsableAtomicTrigger(opts, n1, q)) { - if (options::relationalTriggers() && n2.getKind() == INST_CONSTANT + if (opts.quantifiers.relationalTriggers && n2.getKind() == INST_CONSTANT && quantifiers::TermUtil::getInstConstAttr(n2) == q && !expr::hasSubterm(n1, n2)) { @@ -137,7 +145,9 @@ bool PatternTermSelector::isUsableEqTerms(Node q, Node n1, Node n2) return false; } -Node PatternTermSelector::getIsUsableTrigger(Node n, Node q) +Node PatternTermSelector::getIsUsableTrigger(const Options& opts, + Node n, + Node q) { bool pol = true; Trace("trigger-debug") << "Is " << n << " a usable trigger?" << std::endl; @@ -153,7 +163,7 @@ Node PatternTermSelector::getIsUsableTrigger(Node n, Node q) } else if (TriggerTermInfo::isRelationalTrigger(n)) { - Node rtr = getIsUsableEq(q, n); + Node rtr = getIsUsableEq(opts, q, n); if (rtr.isNull() && n[0].getType().isRealOrInt()) { // try to solve relation @@ -167,9 +177,9 @@ Node PatternTermSelector::getIsUsableTrigger(Node n, Node q) { if (it->first.getKind() == INST_CONSTANT) { - trySolve = options::relationalTriggers(); + trySolve = opts.quantifiers.relationalTriggers; } - else if (isUsableTrigger(it->first, q)) + else if (isUsableTrigger(opts, it->first, q)) { trySolve = true; } @@ -181,7 +191,7 @@ Node PatternTermSelector::getIsUsableTrigger(Node n, Node q) Node veq; if (ArithMSum::isolate(it->first, m, veq, n.getKind()) != 0) { - rtr = getIsUsableEq(q, veq); + rtr = getIsUsableEq(opts, q, veq); } // either all solves will succeed or all solves will fail break; @@ -204,23 +214,25 @@ Node PatternTermSelector::getIsUsableTrigger(Node n, Node q) Trace("trigger-debug") << n << " usable : " << (quantifiers::TermUtil::getInstConstAttr(n) == q) << " " << TriggerTermInfo::isAtomicTrigger(n) << " " - << isUsable(n, q) << std::endl; - if (isUsableAtomicTrigger(n, q)) + << isUsable(opts, n, q) << std::endl; + if (isUsableAtomicTrigger(opts, n, q)) { return pol ? n : nm->mkNode(EQUAL, n, nm->mkConst(true)).notNode(); } return Node::null(); } -bool PatternTermSelector::isUsableAtomicTrigger(Node n, Node q) +bool PatternTermSelector::isUsableAtomicTrigger(const Options& opts, + Node n, + Node q) { return quantifiers::TermUtil::getInstConstAttr(n) == q - && TriggerTermInfo::isAtomicTrigger(n) && isUsable(n, q); + && TriggerTermInfo::isAtomicTrigger(n) && isUsable(opts, n, q); } -bool PatternTermSelector::isUsableTrigger(Node n, Node q) +bool PatternTermSelector::isUsableTrigger(const Options& opts, Node n, Node q) { - Node nu = getIsUsableTrigger(n, q); + Node nu = getIsUsableTrigger(opts, n, q); return !nu.isNull(); } @@ -271,7 +283,7 @@ void PatternTermSelector::collectTermsInternal( && std::find(d_excluded.begin(), d_excluded.end(), n) == d_excluded.end()) { - nu = getIsUsableTrigger(n, d_quant); + nu = getIsUsableTrigger(d_opts, n, d_quant); if (!nu.isNull() && nu != n) { collectTermsInternal( @@ -301,7 +313,7 @@ void PatternTermSelector::collectTermsInternal( } } Assert(reqEq.isNull() || !quantifiers::TermUtil::hasInstConstAttr(reqEq)); - Assert(isUsableTrigger(nu, d_quant)); + Assert(isUsableTrigger(d_opts, nu, d_quant)); Trace("auto-gen-trigger-debug2") << "...add usable trigger : " << nu << std::endl; tinfo[nu].init(d_quant, nu, hasEPol ? (epol ? 1 : -1) : 0, reqEq); @@ -710,11 +722,12 @@ Node PatternTermSelector::getInversion(Node n, Node x) return Node::null(); } -void PatternTermSelector::getTriggerVariables(Node n, +void PatternTermSelector::getTriggerVariables(const Options& opts, + Node n, Node q, std::vector& tvars) { - PatternTermSelector pts(q, options::TriggerSelMode::ALL); + PatternTermSelector pts(opts, q, options::TriggerSelMode::ALL); std::vector patTerms; std::map tinfo; // collect all patterns from n diff --git a/src/theory/quantifiers/ematching/pattern_term_selector.h b/src/theory/quantifiers/ematching/pattern_term_selector.h index 2a8351618..b04b072e8 100644 --- a/src/theory/quantifiers/ematching/pattern_term_selector.h +++ b/src/theory/quantifiers/ematching/pattern_term_selector.h @@ -38,6 +38,7 @@ class PatternTermSelector { public: /** + * @param opts Reference to the options, which impacts pattern term selection * @param q The quantified formula we are selecting pattern terms for * @param tstrt the selection strategy (see options/quantifiers_mode.h), * @param exc The set of terms we are excluding as pattern terms. @@ -46,7 +47,8 @@ class PatternTermSelector * also returning f(f(x)). This is default true since it helps in practice * to filter trigger instances. */ - PatternTermSelector(Node q, + PatternTermSelector(const Options& opts, + Node q, options::TriggerSelMode tstrt, const std::vector& exc = {}, bool filterInst = true); @@ -73,7 +75,7 @@ class PatternTermSelector * (2) Relational triggers are put into solved form, e.g. * getIsUsableTrigger( (= (+ x a) 5), q ) may return (= x (- 5 a)). */ - static Node getIsUsableTrigger(Node n, Node q); + static Node getIsUsableTrigger(const Options& opts, Node n, Node q); /** get the variable associated with an inversion for n * * A term n with an inversion variable x has the following property : @@ -96,7 +98,10 @@ class PatternTermSelector * This returns the union of all free variables in usable triggers that are * subterms of n. */ - static void getTriggerVariables(Node n, Node q, std::vector& tvars); + static void getTriggerVariables(const Options& opts, + Node n, + Node q, + std::vector& tvars); protected: /** Is n a usable trigger in quantified formula q? @@ -104,21 +109,21 @@ class PatternTermSelector * A usable trigger is one that is matchable and contains free variables only * from q. */ - static bool isUsableTrigger(Node n, Node q); + static bool isUsableTrigger(const Options& opts, Node n, Node q); /** Is n a usable atomic trigger? * * A usable atomic trigger is a term that is both a useable trigger and an * atomic trigger. */ - static bool isUsableAtomicTrigger(Node n, Node q); + static bool isUsableAtomicTrigger(const Options& opts, Node n, Node q); /** is subterm of trigger usable (helper function for isUsableTrigger) */ - static bool isUsable(Node n, Node q); + static bool isUsable(const Options& opts, Node n, Node q); /** returns an equality that is equivalent to the equality eq and * is a usable trigger for q if one exists, otherwise returns Node::null(). */ - static Node getIsUsableEq(Node q, Node eq); + static Node getIsUsableEq(const Options& opts, Node q, Node eq); /** returns whether n1 == n2 is a usable (relational) trigger for q. */ - static bool isUsableEqTerms(Node q, Node n1, Node n2); + static bool isUsableEqTerms(const Options& opts, Node q, Node n1, Node n2); /** Helper for collect, with a fixed strategy for selection and filtering */ void collectInternal(Node n, std::vector& patTerms, @@ -180,6 +185,8 @@ class PatternTermSelector Node n2, const std::vector& fv1, const std::vector& fv2); + /** Reference to options */ + const Options& d_opts; /** The quantified formula this trigger is for. */ Node d_quant; /** The trigger selection strategy */ diff --git a/src/theory/quantifiers/quantifiers_macros.cpp b/src/theory/quantifiers/quantifiers_macros.cpp index e9e55c4c2..c77ef9d25 100644 --- a/src/theory/quantifiers/quantifiers_macros.cpp +++ b/src/theory/quantifiers/quantifiers_macros.cpp @@ -31,7 +31,10 @@ namespace cvc5::internal { namespace theory { namespace quantifiers { -QuantifiersMacros::QuantifiersMacros(QuantifiersRegistry& qr) : d_qreg(qr) {} +QuantifiersMacros::QuantifiersMacros(Env& env, QuantifiersRegistry& qr) + : EnvObj(env), d_qreg(qr) +{ +} Node QuantifiersMacros::solve(Node lit, bool reqGround) { @@ -87,7 +90,8 @@ Node QuantifiersMacros::solve(Node lit, bool reqGround) Trace("macros-debug") << "...does not contain bad (recursive) operator." << std::endl; // must be ground UF term if mode is GROUND_UF - if (options::macrosQuantMode() != options::MacrosQuantMode::GROUND_UF + if (options().quantifiers.macrosQuantMode + != options::MacrosQuantMode::GROUND_UF || preservesTriggerVariables(lit, n_def)) { Trace("macros-debug") @@ -146,7 +150,8 @@ bool QuantifiersMacros::preservesTriggerVariables(Node q, Node n) quantifiers::TermUtil::computeInstConstContainsForQuant(q, icn, var); Trace("macros-debug2") << "Get trigger variables for " << icn << std::endl; std::vector trigger_var; - inst::PatternTermSelector::getTriggerVariables(icn, q, trigger_var); + inst::PatternTermSelector::getTriggerVariables( + d_env.getOptions(), icn, q, trigger_var); Trace("macros-debug2") << "Done." << std::endl; // only if all variables are also trigger variables return trigger_var.size() >= var.size(); diff --git a/src/theory/quantifiers/quantifiers_macros.h b/src/theory/quantifiers/quantifiers_macros.h index 95ebca0e9..edbd71244 100644 --- a/src/theory/quantifiers/quantifiers_macros.h +++ b/src/theory/quantifiers/quantifiers_macros.h @@ -20,7 +20,9 @@ #include #include + #include "expr/node.h" +#include "smt/env_obj.h" namespace cvc5::internal { namespace theory { @@ -33,10 +35,10 @@ class QuantifiersRegistry; * a method for putting quantified formulas in solved form, e.g. * forall x. P(x) ---> P = (lambda x. true) */ -class QuantifiersMacros +class QuantifiersMacros : protected EnvObj { public: - QuantifiersMacros(QuantifiersRegistry& qr); + QuantifiersMacros(Env& env, QuantifiersRegistry& qr); ~QuantifiersMacros() {} /** * Called on quantified formulas lit of the form diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp index d40bf27c0..6a476ec32 100644 --- a/src/theory/quantifiers/theory_quantifiers.cpp +++ b/src/theory/quantifiers/theory_quantifiers.cpp @@ -56,7 +56,7 @@ TheoryQuantifiers::TheoryQuantifiers(Env& env, if (options().quantifiers.macrosQuant) { - d_qmacros.reset(new QuantifiersMacros(d_qreg)); + d_qmacros.reset(new QuantifiersMacros(env, d_qreg)); } } -- 2.30.2