Eliminate even more static uses of rewrite (#8044)

diff --git a/src/theory/quantifiers/sygus/cegis_core_connective.cpp b/src/theory/quantifiers/sygus/cegis_core_connective.cpp
index bfc688db7397142a42c1f34f1ab19641ce4368a1..5a5ae074b06bbfe4df9ea7acc88fbbbcd102f277 100644 (file)
--- a/src/theory/quantifiers/sygus/cegis_core_connective.cpp
+++ b/src/theory/quantifiers/sygus/cegis_core_connective.cpp
@@ -563,6 +563,7 @@ bool CegisCoreConnective::Component::addToAsserts(CegisCoreConnective* p,
 Result CegisCoreConnective::checkSat(Node n, std::vector<Node>& mvs) const
 {
   Trace("sygus-ccore-debug") << "...check-sat " << n << "..." << std::endl;
+  n = rewrite(n);
   Result r = checkWithSubsolver(n, d_vars, mvs, options(), logicInfo());
   Trace("sygus-ccore-debug") << "...got " << r << std::endl;
   return r;

diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp
index 2a1258082c38b60c6589f262f6bd5d32c611608a..3760cffb6fd08649aee59e2e53ed1a1f62a48382 100644 (file)
--- a/src/theory/quantifiers/sygus/synth_conjecture.cpp
+++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp
@@ -604,6 +604,7 @@ bool SynthConjecture::checkSideCondition(const std::vector<Node>& cvals) const
     }
     Trace("sygus-engine") << "Check side condition..." << std::endl;
     Trace("cegqi-debug") << "Check side condition : " << sc << std::endl;
+    sc = rewrite(sc);
     Result r = checkWithSubsolver(sc, options(), logicInfo());
     Trace("cegqi-debug") << "...got side condition : " << r << std::endl;
     if (r == Result::UNSAT)

diff --git a/src/theory/quantifiers/sygus/synth_verify.cpp b/src/theory/quantifiers/sygus/synth_verify.cpp
index 41b63cc533adc25b28b27d8ffe96532107442d17..8b6e24a1fe200c2765d84e3e1006851f0ab3e412 100644 (file)
--- a/src/theory/quantifiers/sygus/synth_verify.cpp
+++ b/src/theory/quantifiers/sygus/synth_verify.cpp
@@ -109,6 +109,7 @@ Result SynthVerify::verify(Node query,
     }
   }
   Trace("sygus-engine") << "  *** Verify with subcall..." << std::endl;
+  query = rewrite(query);
   Result r = checkWithSubsolver(query, vars, mvs, d_subOptions, d_subLogicInfo);
   Trace("sygus-engine") << "  ...got " << r << std::endl;
   if (r.asSatisfiabilityResult().isSat() == Result::SAT)

diff --git a/src/theory/smt_engine_subsolver.cpp b/src/theory/smt_engine_subsolver.cpp
index 3e4a69dc9e441d87876ce287cc2694da6fb7ec39..c41f7895e5719052a42c0c76fea6b1df76bb6ccf 100644 (file)
--- a/src/theory/smt_engine_subsolver.cpp
+++ b/src/theory/smt_engine_subsolver.cpp
@@ -20,7 +20,6 @@
 #include "smt/env.h"
 #include "smt/solver_engine.h"
 #include "smt/solver_engine_scope.h"
-#include "theory/rewriter.h"
 
 namespace cvc5 {
 namespace theory {
@@ -28,7 +27,6 @@ namespace theory {
 // optimization: try to rewrite to constant
 Result quickCheck(Node& query)
 {
-  query = theory::Rewriter::rewrite(query);
   if (query.isConst())
   {
     if (!query.getConst<bool>())

diff --git a/src/theory/uf/theory_uf_rewriter.cpp b/src/theory/uf/theory_uf_rewriter.cpp
index ba00c316fed14ab058ddf82996329a29d6b5bd55..b331d22c4f003475a8f187ab1929c8e7b2829644 100644 (file)
--- a/src/theory/uf/theory_uf_rewriter.cpp
+++ b/src/theory/uf/theory_uf_rewriter.cpp
@@ -126,13 +126,13 @@ RewriteResponse TheoryUfRewriter::postRewrite(TNode node)
       // been introduced
       if (d_isHigherOrder)
       {
-        Node arg = Rewriter::rewrite(node[1]);
+        Node arg = node[1];
         Node var = node[0][0][0];
         new_body = expr::substituteCaptureAvoiding(new_body, var, arg);
       }
       else
       {
-        TNode arg = Rewriter::rewrite(node[1]);
+        TNode arg = node[1];
         TNode var = node[0][0][0];
         new_body = new_body.substitute(var, arg);
       }