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 18ccf7aca71e3274f1552e8510848c527d359e92..b5984a0a01dc55049a4519fbb45258e81e24be6b 100644 (file)
--- 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 aa9674bda64b23d8136e59b5bef80e009e833691..321ad1717e0e8ed18f0763fb08b3b7f61b926a7c 100644 (file)
--- a/src/theory/quantifiers/quantifiers_preprocess.cpp
+++ b/src/theory/quantifiers/quantifiers_preprocess.cpp
@@ -77,7 +77,7 @@ Node QuantifiersPreprocess::computePrenexAgg(
     std::unordered_set<Node> argsSet;
     std::unordered_set<Node> 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 10c0a315bca4705194c5c4ecafea5f1f9b5afe53..a66a2021da095f9141b83ecafb20294d564b4490 100644 (file)
--- 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<Node> children;

diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h
index 8b3cbb5224f499b0892ca69bf7a4d9d440275688..d1e02b75d693dea060a2d8a0fbae3e07c94ba960 100644 (file)
--- 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 bcd6ea561c50a0cd37a348081951457c1009d930..10e70d76a2b5b4a2e11367186234b80fa10ea8b3 100644 (file)
--- 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<Node> varsTmp;
     std::vector<Node> 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 03e6479478ec64afe320e8a3f9db7093a52ed93c..d726d6db91712cb49c7f1ab24281b4fc88cf6e16 100644 (file)
--- 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 361d90dcd974401b219d33581445c5e99abcc4ba..c3d58624499d925ab9a33cb6f7e1e1b1432f65c4 100644 (file)
--- 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 d90af4a31ef062709e009e0857019d7ffb272001..5e5597f5605314cc490223afee730c4abc2591f3 100644 (file)
--- 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 8d5ca9923153ada07e3c43a11922ff30584d779e..1f85e88d0c48b8806a6a704f86fb6d6ff9fb1476 100644 (file)
--- 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<Node>{
@@ -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));
   }
 }