From: Andrew Reynolds Date: Tue, 21 Dec 2021 17:03:24 +0000 (-0600) Subject: Eliminate remaining calls to callExtendedRewrite (#7839) X-Git-Tag: cvc5-1.0.0~624 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=2b7bebc38a48a0bd600b2cd9b2dae7328a3c5d3f;p=cvc5.git Eliminate remaining calls to callExtendedRewrite (#7839) --- diff --git a/src/theory/arith/nl/cad/cdcac.cpp b/src/theory/arith/nl/cad/cdcac.cpp index 18ccf7aca..b5984a0a0 100644 --- a/src/theory/arith/nl/cad/cdcac.cpp +++ b/src/theory/arith/nl/cad/cdcac.cpp @@ -251,7 +251,8 @@ PolyVector requiredCoefficientsLazard(const poly::Polynomial& p, PolyVector requiredCoefficientsLazardModified( const poly::Polynomial& p, const poly::Assignment& assignment, - VariableMapper& vm) + VariableMapper& vm, + Rewriter* rewriter) { PolyVector res; auto lc = poly::leading_coefficient(p); @@ -274,8 +275,8 @@ PolyVector requiredCoefficientsLazardModified( Kind::EQUAL, nl::as_cvc_polynomial(coeff, vm), zero)); } // if phi is false (i.e. p can not vanish) - Node rewritten = Rewriter::callExtendedRewrite( - NodeManager::currentNM()->mkAnd(conditions)); + Node rewritten = + rewriter->extendedRewrite(NodeManager::currentNM()->mkAnd(conditions)); if (rewritten.isConst()) { Assert(rewritten.getKind() == Kind::CONST_BOOLEAN); @@ -301,7 +302,7 @@ PolyVector CDCAC::requiredCoefficients(const poly::Polynomial& p) Trace("cdcac::projection") << "LMod: " << requiredCoefficientsLazardModified( - p, d_assignment, d_constraints.varMapper()) + p, d_assignment, d_constraints.varMapper(), d_env.getRewriter()) << std::endl; Trace("cdcac::projection") << "Original: " << requiredCoefficientsOriginal(p, d_assignment) @@ -315,7 +316,7 @@ PolyVector CDCAC::requiredCoefficients(const poly::Polynomial& p) return requiredCoefficientsLazard(p, d_assignment); case options::NlCadProjectionMode::LAZARDMOD: return requiredCoefficientsLazardModified( - p, d_assignment, d_constraints.varMapper()); + p, d_assignment, d_constraints.varMapper(), d_env.getRewriter()); default: Assert(false); return requiredCoefficientsOriginal(p, d_assignment); diff --git a/src/theory/quantifiers/quantifiers_preprocess.cpp b/src/theory/quantifiers/quantifiers_preprocess.cpp index aa9674bda..321ad1717 100644 --- a/src/theory/quantifiers/quantifiers_preprocess.cpp +++ b/src/theory/quantifiers/quantifiers_preprocess.cpp @@ -77,7 +77,7 @@ Node QuantifiersPreprocess::computePrenexAgg( std::unordered_set argsSet; std::unordered_set nargsSet; Node q; - QuantifiersRewriter qrew(options()); + QuantifiersRewriter qrew(d_env.getRewriter(), options()); Node nn = qrew.computePrenex(q, n, argsSet, nargsSet, true, true); Assert(n != nn || argsSet.empty()); Assert(n != nn || nargsSet.empty()); diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index 10c0a315b..a66a2021d 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -90,7 +90,10 @@ std::ostream& operator<<(std::ostream& out, RewriteStep s) return out; } -QuantifiersRewriter::QuantifiersRewriter(const Options& opts) : d_opts(opts) {} +QuantifiersRewriter::QuantifiersRewriter(Rewriter* r, const Options& opts) + : d_rewriter(r), d_opts(opts) +{ +} bool QuantifiersRewriter::isLiteral( Node n ){ switch( n.getKind() ){ @@ -550,7 +553,8 @@ Node QuantifiersRewriter::computeProcessTerms2( return ret; } -Node QuantifiersRewriter::computeExtendedRewrite(Node q, const QAttributes& qa) +Node QuantifiersRewriter::computeExtendedRewrite(TNode q, + const QAttributes& qa) const { // do not apply to recursive functions if (qa.isFunDef()) @@ -559,7 +563,7 @@ Node QuantifiersRewriter::computeExtendedRewrite(Node q, const QAttributes& qa) } Node body = q[1]; // apply extended rewriter - Node bodyr = Rewriter::callExtendedRewrite(body); + Node bodyr = d_rewriter->extendedRewrite(body); if (body != bodyr) { std::vector children; diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h index 8b3cbb522..d1e02b75d 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.h +++ b/src/theory/quantifiers/quantifiers_rewriter.h @@ -26,6 +26,9 @@ namespace cvc5 { class Options; namespace theory { + +class Rewriter; + namespace quantifiers { struct QAttributes; @@ -63,7 +66,7 @@ std::ostream& operator<<(std::ostream& out, RewriteStep s); class QuantifiersRewriter : public TheoryRewriter { public: - QuantifiersRewriter(const Options& opts); + QuantifiersRewriter(Rewriter* r, const Options& opts); /** Pre-rewrite n */ RewriteResponse preRewrite(TNode in) override; /** Post-rewrite n */ @@ -295,7 +298,7 @@ class QuantifiersRewriter : public TheoryRewriter * This returns the result of applying the extended rewriter on the body * of quantified formula q with attributes qa. */ - static Node computeExtendedRewrite(Node q, const QAttributes& qa); + Node computeExtendedRewrite(TNode q, const QAttributes& qa) const; //------------------------------------- end extended rewrite /** * Return true if we should do operation computeOption on quantified formula @@ -308,6 +311,8 @@ class QuantifiersRewriter : public TheoryRewriter Node computeOperation(Node q, RewriteStep computeOption, QAttributes& qa) const; + /** Pointer to rewriter, used for computeExtendedRewrite above */ + Rewriter* d_rewriter; /** Reference to the options */ const Options& d_opts; }; /* class QuantifiersRewriter */ diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp index bcd6ea561..10e70d76a 100644 --- a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp +++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp @@ -508,7 +508,7 @@ bool CegSingleInv::solveTrivial(Node q) std::vector varsTmp; std::vector subsTmp; - QuantifiersRewriter qrew(options()); + QuantifiersRewriter qrew(d_env.getRewriter(), options()); qrew.getVarElim(body, args, varsTmp, subsTmp); // if we eliminated a variable, update body and reprocess if (!varsTmp.empty()) diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp index 03e647947..d726d6db9 100644 --- a/src/theory/quantifiers/theory_quantifiers.cpp +++ b/src/theory/quantifiers/theory_quantifiers.cpp @@ -34,7 +34,7 @@ TheoryQuantifiers::TheoryQuantifiers(Env& env, OutputChannel& out, Valuation valuation) : Theory(THEORY_QUANTIFIERS, env, out, valuation), - d_rewriter(env.getOptions()), + d_rewriter(env.getRewriter(), options()), d_qstate(env, valuation, logicInfo()), d_qreg(env), d_treg(env, d_qstate, d_qreg), diff --git a/src/theory/rewriter.cpp b/src/theory/rewriter.cpp index 361d90dcd..c3d586244 100644 --- a/src/theory/rewriter.cpp +++ b/src/theory/rewriter.cpp @@ -96,11 +96,6 @@ Node Rewriter::rewrite(TNode node) { return getInstance()->rewriteTo(theoryOf(node), node); } -Node Rewriter::callExtendedRewrite(TNode node, bool aggr) -{ - return getInstance()->extendedRewrite(node, aggr); -} - Node Rewriter::extendedRewrite(TNode node, bool aggr) { quantifiers::ExtendedRewriter er(*this, aggr); diff --git a/src/theory/rewriter.h b/src/theory/rewriter.h index d90af4a31..5e5597f56 100644 --- a/src/theory/rewriter.h +++ b/src/theory/rewriter.h @@ -46,10 +46,6 @@ class Rewriter { * use on the node. */ static Node rewrite(TNode node); - /** - * !!! Temporary until static access to rewriter is eliminated. - */ - static Node callExtendedRewrite(TNode node, bool aggr = true); /** * Rewrites the equality node using theoryOf() to determine which rewriter to diff --git a/test/unit/theory/theory_arith_cad_white.cpp b/test/unit/theory/theory_arith_cad_white.cpp index 8d5ca9923..1f85e88d0 100644 --- a/test/unit/theory/theory_arith_cad_white.cpp +++ b/test/unit/theory/theory_arith_cad_white.cpp @@ -182,6 +182,7 @@ poly::Polynomial up_to_poly(const poly::UPolynomial& p, poly::Variable var) TEST_F(TestTheoryWhiteArithCAD, lazard_simp) { + Rewriter* rewriter = d_slvEngine->getRewriter(); Node a = d_nodeManager->mkVar(*d_realType); Node c = d_nodeManager->mkVar(*d_realType); Node orig = d_nodeManager->mkAnd(std::vector{ @@ -196,11 +197,11 @@ TEST_F(TestTheoryWhiteArithCAD, lazard_simp) d_nodeManager->mkConst(CONST_RATIONAL, d_zero))}); { - Node rewritten = Rewriter::rewrite(orig); + Node rewritten = rewriter->rewrite(orig); EXPECT_NE(rewritten, d_nodeManager->mkConst(false)); } { - Node rewritten = Rewriter::callExtendedRewrite(orig); + Node rewritten = rewriter->extendedRewrite(orig); EXPECT_EQ(rewritten, d_nodeManager->mkConst(false)); } }