From a05b134c4d7bc73d57f31a55330e543dc6c14f33 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 3 Feb 2022 15:33:56 -0600
Subject: [PATCH] Eliminate even more static uses of rewrite (#8044)

---
 src/theory/quantifiers/sygus/cegis_core_connective.cpp | 1 +
 src/theory/quantifiers/sygus/synth_conjecture.cpp      | 1 +
 src/theory/quantifiers/sygus/synth_verify.cpp          | 1 +
 src/theory/smt_engine_subsolver.cpp                    | 2 --
 src/theory/uf/theory_uf_rewriter.cpp                   | 4 ++--
 5 files changed, 5 insertions(+), 4 deletions(-)

diff --git a/src/theory/quantifiers/sygus/cegis_core_connective.cpp b/src/theory/quantifiers/sygus/cegis_core_connective.cpp
index bfc688db7..5a5ae074b 100644
--- 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 2a1258082..3760cffb6 100644
--- 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 41b63cc53..8b6e24a1f 100644
--- 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 3e4a69dc9..c41f7895e 100644
--- 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 ba00c316f..b331d22c4 100644
--- 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);
       }
-- 
2.30.2