Remove many static calls to rewrite (#7580)

This is the result of a global replace Rewriter::rewrite( -> rewrite( + patching the results.

It makes several classes into EnvObj. Many calls to Rewriter::rewrite remain (that are embedded in classes that should not be EnvObj).

1 files changed, 8 insertions, 7 deletions

diff --git a/src/theory/strings/extf_solver.cpp b/src/theory/strings/extf_solver.cpp
index 2de9bda96..6e2f60c6d 100644
--- a/src/theory/strings/extf_solver.cpp
+++ b/src/theory/strings/extf_solver.cpp
@@ -209,7 +209,8 @@ bool ExtfSolver::doReduction(int effort, Node n)
         << "Reduction_" << effort << " lemma : " << nnlem << std::endl;
     Trace("strings-red-lemma") << "...from " << n << std::endl;
     Trace("strings-red-lemma")
-        << "Reduction_" << effort << " rewritten : " << Rewriter::rewrite(nnlem) << std::endl;
+        << "Reduction_" << effort << " rewritten : " << rewrite(nnlem)
+        << std::endl;
     d_im.sendInference(d_emptyVec, nnlem, InferenceId::STRINGS_REDUCTION, false, true);
     Trace("strings-extf-debug")
         << "  resolve extf : " << n << " based on reduction." << std::endl;
@@ -297,7 +298,7 @@ void ExtfSolver::checkExtfEval(int effort)
           << ", exp " << exp << std::endl;
       einfo.d_exp.insert(einfo.d_exp.end(), exp.begin(), exp.end());
       // inference is rewriting the substituted node
-      Node nrc = Rewriter::rewrite(sn);
+      Node nrc = rewrite(sn);
       // if rewrites to a constant, then do the inference and mark as reduced
       if (nrc.isConst())
       {
@@ -332,7 +333,7 @@ void ExtfSolver::checkExtfEval(int effort)
           {
             Trace("strings-extf-debug")
                 << "  rewrite " << nrs << "..." << std::endl;
-            Node nrsr = Rewriter::rewrite(nrs);
+            Node nrsr = rewrite(nrs);
             // ensure the symbolic form is not rewritable
             if (nrsr != nrs)
             {
@@ -544,7 +545,7 @@ void ExtfSolver::checkExtfInference(Node n,
         {
           children[index] = nrc;
           Node conc = nm->mkNode(STRING_CONTAINS, children);
-          conc = Rewriter::rewrite(pol ? conc : conc.negate());
+          conc = rewrite(pol ? conc : conc.negate());
           // check if it already (does not) hold
           if (d_state.hasTerm(conc))
           {
@@ -605,7 +606,7 @@ void ExtfSolver::checkExtfInference(Node n,
           Node onr = d_extfInfoTmp[nr[0]].d_ctn[opol][i];
           Node concOrig =
               nm->mkNode(STRING_CONTAINS, pol ? nr[1] : onr, pol ? onr : nr[1]);
-          Node conc = Rewriter::rewrite(concOrig);
+          Node conc = rewrite(concOrig);
           // For termination concerns, we only do the inference if the contains
           // does not rewrite (and thus does not introduce new terms).
           if (conc == concOrig)
@@ -654,7 +655,7 @@ void ExtfSolver::checkExtfInference(Node n,
   // If it's not a predicate, see if we can solve the equality n = c, where c
   // is the constant that extended term n is equal to.
   Node inferEq = nr.eqNode(in.d_const);
-  Node inferEqr = Rewriter::rewrite(inferEq);
+  Node inferEqr = rewrite(inferEq);
   Node inferEqrr = inferEqr;
   if (inferEqr.getKind() == EQUAL)
   {
@@ -663,7 +664,7 @@ void ExtfSolver::checkExtfInference(Node n,
   }
   if (inferEqrr != inferEqr)
   {
-    inferEqrr = Rewriter::rewrite(inferEqrr);
+    inferEqrr = rewrite(inferEqrr);
     Trace("strings-extf-infer")
         << "checkExtfInference: " << inferEq << " ...reduces to " << inferEqrr
         << " with explanation " << in.d_exp << std::endl;