From 8d61d9a6deea7adc0ac7eb47634141717e873468 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 27 May 2022 12:58:30 -0500 Subject: [PATCH] Eliminate static options access in BV inverter (#8829) --- src/theory/quantifiers/bv_inverter.cpp | 7 +++++-- src/theory/quantifiers/bv_inverter.h | 7 ++++++- .../quantifiers/cegqi/ceg_bv_instantiator.cpp | 2 +- .../quantifiers/cegqi/ceg_bv_instantiator.h | 4 +++- .../quantifiers/cegqi/ceg_instantiator.cpp | 2 +- .../quantifiers/cegqi/inst_strategy_cegqi.cpp | 2 +- .../quantifiers/quantifiers_rewriter.cpp | 10 +++++----- src/theory/quantifiers/quantifiers_rewriter.h | 18 ++++++++---------- 8 files changed, 30 insertions(+), 22 deletions(-) diff --git a/src/theory/quantifiers/bv_inverter.cpp b/src/theory/quantifiers/bv_inverter.cpp index 043587410..168afe2b6 100644 --- a/src/theory/quantifiers/bv_inverter.cpp +++ b/src/theory/quantifiers/bv_inverter.cpp @@ -31,7 +31,10 @@ namespace cvc5::internal { namespace theory { namespace quantifiers { -BvInverter::BvInverter(Rewriter* r) : d_rewriter(r) {} +BvInverter::BvInverter(const Options& opts, Rewriter* r) + : d_opts(opts), d_rewriter(r) +{ +} /*---------------------------------------------------------------------------*/ @@ -342,7 +345,7 @@ Node BvInverter::solveBvLit(Node sv, } else if (k == BITVECTOR_CONCAT) { - if (litk == EQUAL && options::cegqiBvConcInv()) + if (litk == EQUAL && d_opts.quantifiers.cegqiBvConcInv) { /* Compute inverse for s1 o x, x o s2, s1 o x o s2 * (while disregarding that invertibility depends on si) diff --git a/src/theory/quantifiers/bv_inverter.h b/src/theory/quantifiers/bv_inverter.h index d17b58fab..bd313a4c4 100644 --- a/src/theory/quantifiers/bv_inverter.h +++ b/src/theory/quantifiers/bv_inverter.h @@ -26,6 +26,9 @@ #include "expr/node.h" namespace cvc5::internal { + +class Options; + namespace theory { class Rewriter; @@ -53,7 +56,7 @@ class BvInverterQuery class BvInverter { public: - BvInverter(Rewriter* r = nullptr); + BvInverter(const Options& opts, Rewriter* r = nullptr); ~BvInverter() {} /** get dummy fresh variable of type tn, used as argument for sv */ Node getSolveVariable(TypeNode tn); @@ -125,6 +128,8 @@ class BvInverter * to this call is null. */ Node getInversionNode(Node cond, TypeNode tn, BvInverterQuery* m); + /** Reference to options */ + const Options& d_opts; /** (Optional) rewriter used as helper in getInversionNode */ Rewriter* d_rewriter; /** Dummy variables for each type */ diff --git a/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp index f0be34902..5607c0447 100644 --- a/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp +++ b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp @@ -643,7 +643,7 @@ void BvInstantiatorPreprocess::registerCounterexampleLemma( // new lemmas std::vector new_lems; - if (options::cegqiBvRmExtract()) + if (d_opts.quantifiers.cegqiBvRmExtract) { NodeManager* nm = NodeManager::currentNM(); SkolemManager* sm = nm->getSkolemManager(); diff --git a/src/theory/quantifiers/cegqi/ceg_bv_instantiator.h b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.h index be990899a..b116a01b5 100644 --- a/src/theory/quantifiers/cegqi/ceg_bv_instantiator.h +++ b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.h @@ -167,7 +167,7 @@ class BvInstantiator : public Instantiator class BvInstantiatorPreprocess : public InstantiatorPreprocess { public: - BvInstantiatorPreprocess() {} + BvInstantiatorPreprocess(const Options& opts) : d_opts(opts) {} ~BvInstantiatorPreprocess() override {} /** register counterexample lemma * @@ -208,6 +208,8 @@ class BvInstantiatorPreprocess : public InstantiatorPreprocess void collectExtracts(Node lem, std::map>& extract_map, std::unordered_set& visited); + /** Reference to options */ + const Options& d_opts; }; } // namespace quantifiers diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp index 750c07e5d..0295d5317 100644 --- a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp +++ b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp @@ -554,7 +554,7 @@ void CegInstantiator::registerTheoryId(TheoryId tid) // setup any theory-specific preprocessors here if (tid == THEORY_BV) { - d_tipp[tid] = new BvInstantiatorPreprocess; + d_tipp[tid] = new BvInstantiatorPreprocess(d_env.getOptions()); } d_tids.push_back(tid); } diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp index e290b0f67..109805702 100644 --- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp +++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp @@ -66,7 +66,7 @@ InstStrategyCegqi::InstStrategyCegqi(Env& env, if (options().quantifiers.cegqiBv) { // if doing instantiation for BV, need the inverter class - d_bv_invert.reset(new BvInverter(env.getRewriter())); + d_bv_invert.reset(new BvInverter(env.getOptions(), env.getRewriter())); } if (options().quantifiers.cegqiNestedQE) { diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index 55ed145cf..37626015c 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -840,7 +840,7 @@ bool QuantifiersRewriter::isVarElim(Node v, Node s) Node QuantifiersRewriter::getVarElimEq(Node lit, const std::vector& args, - Node& var) + Node& var) const { Assert(lit.getKind() == EQUAL); Node slv; @@ -862,7 +862,7 @@ Node QuantifiersRewriter::getVarElimEq(Node lit, Node QuantifiersRewriter::getVarElimEqReal(Node lit, const std::vector& args, - Node& var) + Node& var) const { // for arithmetic, solve the equality std::map msum; @@ -896,7 +896,7 @@ Node QuantifiersRewriter::getVarElimEqReal(Node lit, Node QuantifiersRewriter::getVarElimEqBv(Node lit, const std::vector& args, - Node& var) + Node& var) const { if (TraceIsOn("quant-velim-bv")) { @@ -914,7 +914,7 @@ Node QuantifiersRewriter::getVarElimEqBv(Node lit, std::vector active_args; computeArgVec(args, active_args, lit); - BvInverter binv; + BvInverter binv(d_opts); for (const Node& cvar : active_args) { // solve for the variable on this path using the inverter @@ -947,7 +947,7 @@ Node QuantifiersRewriter::getVarElimEqBv(Node lit, Node QuantifiersRewriter::getVarElimEqString(Node lit, const std::vector& args, - Node& var) + Node& var) const { Assert(lit.getKind() == EQUAL); NodeManager* nm = NodeManager::currentNM(); diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h index 7263ece48..abaebfbaf 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.h +++ b/src/theory/quantifiers/quantifiers_rewriter.h @@ -101,31 +101,29 @@ class QuantifiersRewriter : public TheoryRewriter /** * Get variable eliminate for an equality based on theory-specific reasoning. */ - static Node getVarElimEq(Node lit, const std::vector& args, Node& var); + Node getVarElimEq(Node lit, const std::vector& args, Node& var) const; /** variable eliminate for real equalities * * If this returns a non-null value ret, then var is updated to a member of * args, lit is equivalent to ( var = ret ). */ - static Node getVarElimEqReal(Node lit, - const std::vector& args, - Node& var); + Node getVarElimEqReal(Node lit, + const std::vector& args, + Node& var) const; /** variable eliminate for bit-vector equalities * * If this returns a non-null value ret, then var is updated to a member of * args, lit is equivalent to ( var = ret ). */ - static Node getVarElimEqBv(Node lit, - const std::vector& args, - Node& var); + Node getVarElimEqBv(Node lit, const std::vector& args, Node& var) const; /** variable eliminate for string equalities * * If this returns a non-null value ret, then var is updated to a member of * args, lit is equivalent to ( var = ret ). */ - static Node getVarElimEqString(Node lit, - const std::vector& args, - Node& var); + Node getVarElimEqString(Node lit, + const std::vector& args, + Node& var) const; /** get variable elimination * * If there exists an n with some polarity in body, and entails a literal that -- 2.30.2