Remove more static calls to rewrite (#8025)

diff --git a/src/preprocessing/assertion_pipeline.cpp b/src/preprocessing/assertion_pipeline.cpp
index 778931f7059fdffcb46db40d77a813111a32497a..5c43a01688f569e016a6c3a26783dfc635dcfae6 100644 (file)
--- a/src/preprocessing/assertion_pipeline.cpp
+++ b/src/preprocessing/assertion_pipeline.cpp
@@ -21,13 +21,13 @@
 #include "proof/lazy_proof.h"
 #include "smt/preprocess_proof_generator.h"
 #include "theory/builtin/proof_checker.h"
-#include "theory/rewriter.h"
 
 namespace cvc5 {
 namespace preprocessing {
 
-AssertionPipeline::AssertionPipeline()
-    : d_realAssertionsEnd(0),
+AssertionPipeline::AssertionPipeline(Env& env)
+    : EnvObj(env),
+      d_realAssertionsEnd(0),
       d_storeSubstsInAsserts(false),
       d_substsIndex(0),
       d_assumptionsStart(0),
@@ -147,7 +147,7 @@ void AssertionPipeline::conjoin(size_t i, Node n, ProofGenerator* pg)
 {
   NodeManager* nm = NodeManager::currentNM();
   Node newConj = nm->mkNode(kind::AND, d_nodes[i], n);
-  Node newConjr = theory::Rewriter::rewrite(newConj);
+  Node newConjr = rewrite(newConj);
   Trace("assert-pipeline") << "Assertions: conjoin " << n << " to "
                            << d_nodes[i] << std::endl;
   Trace("assert-pipeline-debug") << "conjoin " << n << " to " << d_nodes[i]
@@ -200,7 +200,7 @@ void AssertionPipeline::conjoin(size_t i, Node n, ProofGenerator* pg)
     }
   }
   d_nodes[i] = newConjr;
-  Assert(theory::Rewriter::rewrite(newConjr) == newConjr);
+  Assert(rewrite(newConjr) == newConjr);
 }
 
 }  // namespace preprocessing

diff --git a/src/preprocessing/assertion_pipeline.h b/src/preprocessing/assertion_pipeline.h
index 5c75fba2b7ead957a8f48c891cdd20cb8d4420b4..6c220b756a7450a6d983428a8997617732e15cec 100644 (file)
--- a/src/preprocessing/assertion_pipeline.h
+++ b/src/preprocessing/assertion_pipeline.h
@@ -23,6 +23,7 @@
 
 #include "expr/node.h"
 #include "proof/trust_node.h"
+#include "smt/env_obj.h"
 
 namespace cvc5 {
 
@@ -40,10 +41,10 @@ using IteSkolemMap = std::unordered_map<size_t, Node>;
  * passes. It is assumed that all assertions after d_realAssertionsEnd were
  * generated by ITE removal. Hence, d_iteSkolemMap maps into only these.
  */
-class AssertionPipeline
+class AssertionPipeline : protected EnvObj
 {
  public:
-  AssertionPipeline();
+  AssertionPipeline(Env& env);
 
   size_t size() const { return d_nodes.size(); }
 

diff --git a/src/smt/assertions.cpp b/src/smt/assertions.cpp
index 0191bcb82976270abe0d9c6d6241ef612770c005..136cdaf8cbcd83cfc7a54f8ce5d709c0a01742e8 100644 (file)
--- a/src/smt/assertions.cpp
+++ b/src/smt/assertions.cpp
@@ -42,7 +42,7 @@ Assertions::Assertions(Env& env, AbstractValues& absv)
       d_assertionListDefs(userContext()),
       d_globalDefineFunLemmasIndex(userContext(), 0),
       d_globalNegation(false),
-      d_assertions()
+      d_assertions(env)
 {
 }
 

diff --git a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp
index 51804f0ce4bb1382bcaea58ea13b23b9c15d3cf9..687c69f8f541df0b4f1ccbd7a0ec0b55b9bd5e8c 100644 (file)
--- a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp
+++ b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp
@@ -1176,8 +1176,9 @@ Node SygusUnifRl::DecisionTreeInfo::PointSeparator::computeCond(Node cond,
   {
     return it->second;
   }
+  TermDbSygus* tds = d_dt->d_unif->d_tds;
   TypeNode tn = cond.getType();
-  Node builtin_cond = d_dt->d_unif->d_tds->sygusToBuiltin(cond, tn);
+  Node builtin_cond = tds->sygusToBuiltin(cond, tn);
   // Retrieve evaluation point
   Assert(d_dt->d_unif->d_hd_to_pt.find(hd) != d_dt->d_unif->d_hd_to_pt.end());
   std::vector<Node> pt = d_dt->d_unif->d_hd_to_pt[hd];
@@ -1192,7 +1193,7 @@ Node SygusUnifRl::DecisionTreeInfo::PointSeparator::computeCond(Node cond,
     }
     Trace("sygus-unif-rl-sep") << ")\n";
   }
-  Node res = d_dt->d_unif->d_tds->evaluateBuiltin(tn, builtin_cond, pt);
+  Node res = tds->evaluateBuiltin(tn, builtin_cond, pt);
   Trace("sygus-unif-rl-sep") << "...got res = " << res << "\n";
   // If condition is templated, recompute result accordingly
   Node templ = d_dt->d_template.first;
@@ -1200,7 +1201,7 @@ Node SygusUnifRl::DecisionTreeInfo::PointSeparator::computeCond(Node cond,
   if (!templ.isNull())
   {
     res = templ.substitute(templ_var, res);
-    res = Rewriter::rewrite(res);
+    res = tds->rewriteNode(res);
     Trace("sygus-unif-rl-sep")
         << "...after template res = " << res << std::endl;
   }

diff --git a/src/theory/strings/core_solver.cpp b/src/theory/strings/core_solver.cpp
index 96cbf8848374ac3b47a7aaea938321f09cb3cd77..ee54b0fce100e3e4a9ee4c1ec2b758e20d23a29f 100644 (file)
--- a/src/theory/strings/core_solver.cpp
+++ b/src/theory/strings/core_solver.cpp
@@ -1554,7 +1554,10 @@ void CoreSolver::processSimpleNEq(NormalForm& nfi,
         size_t cIndex = index;
         Node stra = nfc.collectConstantStringAt(cIndex);
         Assert(!stra.isNull());
-        Node strb = nextConstStr;
+        stra = rewrite(stra);
+        Assert(stra.isConst());
+        Node strb = rewrite(nextConstStr);
+        Assert(strb.isConst());
 
         // Since `nc` is non-empty, we use the non-empty overlap
         size_t p = getSufficientNonEmptyOverlap(stra, strb, isRev);

diff --git a/src/theory/strings/normal_form.cpp b/src/theory/strings/normal_form.cpp
index 7a8df9f420202959b785681898771d6f86599601..b2bc8ac5c72c383e7f39c70e08f1700cdd966e99 100644 (file)
--- a/src/theory/strings/normal_form.cpp
+++ b/src/theory/strings/normal_form.cpp
@@ -52,8 +52,7 @@ void NormalForm::reverse()
 
 void NormalForm::splitConstant(unsigned index, Node c1, Node c2)
 {
-  Assert(Rewriter::rewrite(NodeManager::currentNM()->mkNode(
-             STRING_CONCAT, d_isRev ? c2 : c1, d_isRev ? c1 : c2))
+  Assert(Word::mkWordFlatten({d_isRev ? c2 : c1, d_isRev ? c1 : c2})
          == d_nf[index]);
   d_nf.insert(d_nf.begin() + index + 1, c2);
   d_nf[index] = c1;
@@ -152,14 +151,9 @@ Node NormalForm::collectConstantStringAt(size_t& index)
     {
       std::reverse(c.begin(), c.end());
     }
-    Node cc = Rewriter::rewrite(utils::mkConcat(c, c[0].getType()));
-    Assert(cc.isConst());
-    return cc;
-  }
-  else
-  {
-    return Node::null();
+    return utils::mkConcat(c, c[0].getType());
   }
+  return Node::null();
 }
 
 void NormalForm::getExplanationForPrefixEq(NormalForm& nfi,

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index fdc743915c1848318c4efd9f354bc0c2f47b996a..2f8b3b8ce27cd69c907272dcb2a1e2b96d1b5517 100644 (file)
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -433,7 +433,7 @@ bool TheoryStrings::collectModelInfoType(
           argVal = nfe.d_nf[0][0];
         }
         Assert(!argVal.isNull()) << "No value for " << nfe.d_nf[0][0];
-        assignedValue = Rewriter::rewrite(nm->mkNode(SEQ_UNIT, argVal));
+        assignedValue = rewrite(nm->mkNode(SEQ_UNIT, argVal));
         Trace("strings-model")
             << "-> assign via seq.unit: " << assignedValue << std::endl;
       }

diff --git a/src/theory/uf/function_const.cpp b/src/theory/uf/function_const.cpp
index 181cb20ca687f8351fb574313d66140531eb95ac..85fec7cb23bdad6534cab9ab849c71606fc07d67 100644 (file)
--- a/src/theory/uf/function_const.cpp
+++ b/src/theory/uf/function_const.cpp
@@ -173,9 +173,6 @@ Node FunctionConst::getArrayRepresentationForLambdaRec(TNode n,
     {
       Trace("builtin-rewrite-debug2")
           << "  process base : " << curr << std::endl;
-      // curr = Rewriter::rewrite(curr);
-      // Trace("builtin-rewrite-debug2")
-      //     << "  rewriten base : " << curr << std::endl;
       // Complex Boolean return cases, in which
       //  (1) lambda x. (= x v1) v ... becomes
       //      lambda x. (ite (= x v1) true [...])

diff --git a/test/unit/preprocessing/pass_bv_gauss_white.cpp b/test/unit/preprocessing/pass_bv_gauss_white.cpp
index eb462006c6995908e74d118767d8ac45c4cc5ff2..1a36d682bf7bfc85b6ae054396c132bf72936245 100644 (file)
--- a/test/unit/preprocessing/pass_bv_gauss_white.cpp
+++ b/test/unit/preprocessing/pass_bv_gauss_white.cpp
@@ -2409,7 +2409,7 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_unique1)
   Node a = d_nodeManager->mkNode(
       kind::AND, d_nodeManager->mkNode(kind::AND, eq1, eq2), eq3);
 
-  AssertionPipeline apipe;
+  AssertionPipeline apipe(d_slvEngine->getEnv());
   apipe.push_back(a);
   passes::BVGauss bgauss(d_preprocContext.get(), "bv-gauss-unit");
   std::unordered_map<Node, Node> res;
@@ -2496,7 +2496,7 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_unique2)
   Node a = d_nodeManager->mkNode(
       kind::AND, d_nodeManager->mkNode(kind::AND, eq1, eq2), eq3);
 
-  AssertionPipeline apipe;
+  AssertionPipeline apipe(d_slvEngine->getEnv());
   apipe.push_back(a);
   apipe.push_back(eq4);
   apipe.push_back(eq5);
@@ -2548,7 +2548,7 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_partial)
           d_p),
       d_nine);
 
-  AssertionPipeline apipe;
+  AssertionPipeline apipe(d_slvEngine->getEnv());
   apipe.push_back(eq1);
   apipe.push_back(eq2);
   passes::BVGauss bgauss(d_preprocContext.get(), "bv-gauss-unit");