Eliminate more static calls to Rewriter::rewrite (#7740)

diff --git a/src/preprocessing/passes/apply_substs.cpp b/src/preprocessing/passes/apply_substs.cpp
index 99bded47a412d70f40487cac22a814d7bdca7847..82122fa7fafc459f6aba33d14729b2a63b5eea27 100644 (file)
--- a/src/preprocessing/passes/apply_substs.cpp
+++ b/src/preprocessing/passes/apply_substs.cpp
@@ -21,7 +21,7 @@
 #include "context/cdo.h"
 #include "preprocessing/assertion_pipeline.h"
 #include "preprocessing/preprocessing_pass_context.h"
-#include "theory/rewriter.h"
+#include "smt/env.h"
 #include "theory/substitutions.h"
 
 namespace cvc5 {
@@ -55,7 +55,8 @@ PreprocessingPassResult ApplySubsts::applyInternal(
                           << std::endl;
     d_preprocContext->spendResource(Resource::PreprocessStep);
     assertionsToPreprocess->replaceTrusted(
-        i, tlsm.applyTrusted((*assertionsToPreprocess)[i]));
+        i,
+        tlsm.applyTrusted((*assertionsToPreprocess)[i], d_env.getRewriter()));
     Trace("apply-substs") << "  got " << (*assertionsToPreprocess)[i]
                           << std::endl;
   }

diff --git a/src/preprocessing/passes/non_clausal_simp.cpp b/src/preprocessing/passes/non_clausal_simp.cpp
index 4bf29157efbe8a247045215ed7dd344aeeec301b..247a8b72ef5f5062f56ee17aff1800b8adc5b62e 100644 (file)
--- a/src/preprocessing/passes/non_clausal_simp.cpp
+++ b/src/preprocessing/passes/non_clausal_simp.cpp
@@ -120,6 +120,7 @@ PreprocessingPassResult NonClausalSimp::applyInternal(
       << " learned literals." << std::endl;
   // No conflict, go through the literals and solve them
   context::Context* u = userContext();
+  Rewriter* rw = d_env.getRewriter();
   TrustSubstitutionMap& ttls = d_preprocContext->getTopLevelSubstitutions();
   CVC5_UNUSED SubstitutionMap& top_level_substs = ttls.get();
   // constant propagations
@@ -228,7 +229,7 @@ PreprocessingPassResult NonClausalSimp::applyInternal(
             c = learnedLiteral[1];
           }
           Assert(!t.isConst());
-          Assert(cps.apply(t, true) == t);
+          Assert(rewrite(cps.apply(t)) == t);
           Assert(top_level_substs.apply(t) == t);
           Assert(nss.apply(t) == t);
           // also add to learned literal
@@ -293,7 +294,7 @@ PreprocessingPassResult NonClausalSimp::applyInternal(
   for (size_t i = 0, size = assertionsToPreprocess->size(); i < size; ++i)
   {
     Node assertion = (*assertionsToPreprocess)[i];
-    TrustNode assertionNew = newSubstitutions->applyTrusted(assertion);
+    TrustNode assertionNew = newSubstitutions->applyTrusted(assertion, rw);
     Trace("non-clausal-simplify") << "assertion = " << assertion << std::endl;
     if (!assertionNew.isNull())
     {
@@ -305,7 +306,7 @@ PreprocessingPassResult NonClausalSimp::applyInternal(
     }
     for (;;)
     {
-      assertionNew = constantPropagations->applyTrusted(assertion);
+      assertionNew = constantPropagations->applyTrusted(assertion, rw);
       if (assertionNew.isNull())
       {
         break;
@@ -340,7 +341,7 @@ PreprocessingPassResult NonClausalSimp::applyInternal(
       if (d_preprocContext->getSymsInAssertions().contains(lhs))
       {
         // if it has, the substitution becomes an assertion
-        TrustNode trhs = newSubstitutions->applyTrusted(lhs);
+        TrustNode trhs = newSubstitutions->applyTrusted(lhs, rw);
         Assert(!trhs.isNull());
         Trace("non-clausal-simplify")
             << "substitute: will notify SAT layer of substitution: "
@@ -446,10 +447,11 @@ Node NonClausalSimp::processLearnedLit(Node lit,
                                        theory::TrustSubstitutionMap* subs,
                                        theory::TrustSubstitutionMap* cp)
 {
+  Rewriter* rw = d_env.getRewriter();
   TrustNode tlit;
   if (subs != nullptr)
   {
-    tlit = subs->applyTrusted(lit);
+    tlit = subs->applyTrusted(lit, rw);
     if (!tlit.isNull())
     {
       lit = processRewrittenLearnedLit(tlit);
@@ -462,7 +464,7 @@ Node NonClausalSimp::processLearnedLit(Node lit,
   {
     for (;;)
     {
-      tlit = cp->applyTrusted(lit);
+      tlit = cp->applyTrusted(lit, rw);
       if (tlit.isNull())
       {
         break;

diff --git a/src/smt/abduction_solver.cpp b/src/smt/abduction_solver.cpp
index ce11c57187afdb38dc6213c3ed2a188963be8f4a..063ffe09b0e177eb326bbc4d70f2fd51ffe1b541 100644 (file)
--- a/src/smt/abduction_solver.cpp
+++ b/src/smt/abduction_solver.cpp
@@ -50,6 +50,7 @@ bool AbductionSolver::getAbduct(const std::vector<Node>& axioms,
   std::vector<Node> asserts(axioms.begin(), axioms.end());
   // must expand definitions
   Node conjn = d_env.getTopLevelSubstitutions().apply(goal);
+  conjn = rewrite(conjn);
   // now negate
   conjn = conjn.negate();
   d_abdConj = conjn;

diff --git a/src/smt/check_models.cpp b/src/smt/check_models.cpp
index 7d546eae73afb79332a52b219d5d4efa498a151d..f3393caae3afc406d9115c3af3a2fceac4708828 100644 (file)
--- a/src/smt/check_models.cpp
+++ b/src/smt/check_models.cpp
@@ -71,7 +71,7 @@ void CheckModels::checkModel(TheoryModel* m,
     // evaluate e.g. divide-by-zero. This is intentional since the evaluation
     // is not trustworthy, since the UF introduced by expanding definitions may
     // not be properly constrained.
-    Node n = sm.apply(assertion, false);
+    Node n = sm.apply(assertion);
     verbose(1) << "SolverEngine::checkModel(): -- substitutes to " << n
                << std::endl;
 

diff --git a/src/smt/interpolation_solver.cpp b/src/smt/interpolation_solver.cpp
index 36f8e2a8d5820e60db3f3d07cf695dd5b958a0fd..20be53e85c16a3f0aaba48fe4a5129060fd1d6ea 100644 (file)
--- a/src/smt/interpolation_solver.cpp
+++ b/src/smt/interpolation_solver.cpp
@@ -51,6 +51,7 @@ bool InterpolationSolver::getInterpol(const std::vector<Node>& axioms,
                           << std::endl;
   // must expand definitions
   Node conjn = d_env.getTopLevelSubstitutions().apply(conj);
+  conjn = rewrite(conjn);
   std::string name("__internal_interpol");
 
   quantifiers::SygusInterpol interpolSolver(d_env);

diff --git a/src/smt/preprocessor.cpp b/src/smt/preprocessor.cpp
index 41653b6ee6bd102b8817431e6d376b6e024b43b6..0fdb569c82c07a0a7907f9a2b5b628552d4cd18e 100644 (file)
--- a/src/smt/preprocessor.cpp
+++ b/src/smt/preprocessor.cpp
@@ -125,8 +125,8 @@ Node Preprocessor::expandDefinitions(const Node& node,
     // Ensure node is type-checked at this point.
     n.getType(true);
   }
-  // we apply substitutions here, before expanding definitions
-  n = d_env.getTopLevelSubstitutions().apply(n, false);
+  // apply substitutions here (without rewriting), before expanding definitions
+  n = d_env.getTopLevelSubstitutions().apply(n);
   // now call expand definitions
   n = d_exDefs.expandDefinitions(n, cache);
   return n;

diff --git a/src/smt/solver_engine.cpp b/src/smt/solver_engine.cpp
index 2cf4862a9d67b49e96c710f4876e2e49c0d1da76..52fdaf74b2bbf27dbe46b98e9cca63148df39875 100644 (file)
--- a/src/smt/solver_engine.cpp
+++ b/src/smt/solver_engine.cpp
@@ -1386,7 +1386,7 @@ void SolverEngine::checkUnsatCore()
   theory::TrustSubstitutionMap& tls = d_env->getTopLevelSubstitutions();
   for (UnsatCore::iterator i = core.begin(); i != core.end(); ++i)
   {
-    Node assertionAfterExpansion = tls.apply(*i, false);
+    Node assertionAfterExpansion = tls.apply(*i);
     d_env->verbose(1) << "SolverEngine::checkUnsatCore(): pushing core member "
                       << *i << ", expanded to " << assertionAfterExpansion
                       << std::endl;

diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
index 65ad79e299291cbee4d46271828c6800f560aa02..e08f892181bd53d64eaac7ae9604ab0036aa3652 100644 (file)
--- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
+++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
@@ -56,7 +56,7 @@ InstStrategyCegqi::InstStrategyCegqi(Env& env,
       d_cbqi_set_quant_inactive(false),
       d_incomplete_check(false),
       d_added_cbqi_lemma(userContext()),
-      d_vtsCache(new VtsTermCache(qim)),
+      d_vtsCache(new VtsTermCache(env, qim)),
       d_bv_invert(nullptr),
       d_small_const_multiplier(NodeManager::currentNM()->mkConst(
           CONST_RATIONAL, Rational(1) / Rational(1000000))),

diff --git a/src/theory/quantifiers/cegqi/vts_term_cache.cpp b/src/theory/quantifiers/cegqi/vts_term_cache.cpp
index 37ded9b7f69101d75514562c782ffaa6c085e2ce..f405da34573d73c1a27c9877bb2d9018f08559b3 100644 (file)
--- a/src/theory/quantifiers/cegqi/vts_term_cache.cpp
+++ b/src/theory/quantifiers/cegqi/vts_term_cache.cpp
@@ -28,7 +28,8 @@ namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
-VtsTermCache::VtsTermCache(QuantifiersInferenceManager& qim) : d_qim(qim)
+VtsTermCache::VtsTermCache(Env& env, QuantifiersInferenceManager& qim)
+    : EnvObj(env), d_qim(qim)
 {
   d_zero = NodeManager::currentNM()->mkConst(CONST_RATIONAL, Rational(0));
 }
@@ -155,7 +156,7 @@ Node VtsTermCache::rewriteVtsSymbols(Node n)
                            subs_lhs.end(),
                            subs_rhs.begin(),
                            subs_rhs.end());
-          n = Rewriter::rewrite(n);
+          n = rewrite(n);
           // may have cancelled
           if (!expr::hasSubterm(n, rew_vts_inf))
           {

diff --git a/src/theory/quantifiers/cegqi/vts_term_cache.h b/src/theory/quantifiers/cegqi/vts_term_cache.h
index d3a6558cf3cfa45faa29e4750db4f46d8fdb09d5..60c8f28f3a1ef89594feea336b4a6c6c6ef5db20 100644 (file)
--- a/src/theory/quantifiers/cegqi/vts_term_cache.h
+++ b/src/theory/quantifiers/cegqi/vts_term_cache.h
@@ -19,8 +19,10 @@
 #define CVC5__THEORY__QUANTIFIERS__CEGQI__VTS_TERM_CACHE_H
 
 #include <map>
+
 #include "expr/attribute.h"
 #include "expr/node.h"
+#include "smt/env_obj.h"
 
 namespace cvc5 {
 namespace theory {
@@ -68,10 +70,10 @@ class QuantifiersInferenceManager;
  * that combine instantiating quantified formulas with nested quantifiers
  * with terms containing virtual terms.
  */
-class VtsTermCache
+class VtsTermCache : protected EnvObj
 {
  public:
-  VtsTermCache(QuantifiersInferenceManager& qim);
+  VtsTermCache(Env& env, QuantifiersInferenceManager& qim);
   ~VtsTermCache() {}
   /**
    * Get vts delta. The argument isFree indicates if we are getting the

diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index c38d0aa91128f8df236d1ef5947d159619f1dfdc..ba10a2efcc0f3fd3fe4411c6ab77d4169fdd3a44 100644 (file)
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -443,7 +443,7 @@ Node QuantifiersRewriter::computeProcessTerms(Node body,
     {
       Node r = computeProcessTerms2(fbody, cache, new_vars, new_conds);
       Assert(new_vars.size() == h.getNumChildren());
-      return Rewriter::rewrite(NodeManager::currentNM()->mkNode(EQUAL, h, r));
+      return NodeManager::currentNM()->mkNode(EQUAL, h, r);
     }
     // It can happen that we can't infer the shape of the function definition,
     // for example: forall xy. f( x, y ) = 1 + f( x, y ), this is rewritten to
@@ -1028,12 +1028,11 @@ bool QuantifiersRewriter::getVarElimInternal(Node body,
                                              std::vector<Node>& subs) const
 {
   Kind nk = n.getKind();
-  if (nk == NOT)
+  while (nk == NOT)
   {
     n = n[0];
     pol = !pol;
     nk = n.getKind();
-    Assert(nk != NOT);
   }
   if ((nk == AND && pol) || (nk == OR && !pol))
   {
@@ -1326,7 +1325,6 @@ Node QuantifiersRewriter::computeVarElimination(Node body,
       // remake with eliminated nodes
       body =
           body.substitute(vars.begin(), vars.end(), subs.begin(), subs.end());
-      body = Rewriter::rewrite(body);
       if (!qa.d_ipl.isNull())
       {
         qa.d_ipl = qa.d_ipl.substitute(

diff --git a/src/theory/quantifiers/single_inv_partition.cpp b/src/theory/quantifiers/single_inv_partition.cpp
index 73bcad535ba11d1f050b8ced4589136de877f6fa..2725e182645181337d2019928a506d08984ed713 100644 (file)
--- a/src/theory/quantifiers/single_inv_partition.cpp
+++ b/src/theory/quantifiers/single_inv_partition.cpp
@@ -19,7 +19,6 @@
 #include "expr/node_algorithm.h"
 #include "expr/skolem_manager.h"
 #include "theory/quantifiers/term_util.h"
-#include "theory/rewriter.h"
 
 using namespace cvc5;
 using namespace cvc5::kind;
@@ -336,7 +335,6 @@ bool SingleInvocationPartition::init(std::vector<Node>& funcs,
         cr = cr.substitute(
             termsNs.begin(), termsNs.end(), subsNs.begin(), subsNs.end());
       }
-      cr = Rewriter::rewrite(cr);
       Trace("si-prt") << ".....got si=" << singleInvocation
                       << ", result : " << cr << std::endl;
       d_conjuncts[2].push_back(cr);
@@ -349,7 +347,6 @@ bool SingleInvocationPartition::init(std::vector<Node>& funcs,
         Assert(si_terms.size() == si_subs.size());
         cr = cr.substitute(
             si_terms.begin(), si_terms.end(), si_subs.begin(), si_subs.end());
-        cr = Rewriter::rewrite(cr);
         Trace("si-prt") << ".....si version=" << cr << std::endl;
         d_conjuncts[0].push_back(cr);
       }

diff --git a/src/theory/quantifiers/skolemize.cpp b/src/theory/quantifiers/skolemize.cpp
index 4dea0dc22fe5b10f055f30cacf04a0c4a9d84c8d..f116b2f3cb6099fe9eaaf0a3b2650ac53b074083 100644 (file)
--- a/src/theory/quantifiers/skolemize.cpp
+++ b/src/theory/quantifiers/skolemize.cpp
@@ -309,7 +309,6 @@ Node Skolemize::mkSkolemizedBody(Node f,
     {
       Node bvl = nm->mkNode(BOUND_VAR_LIST, rem_ind_vars);
       nret = nm->mkNode(FORALL, bvl, nret);
-      nret = Rewriter::rewrite(nret);
       sub = nret;
       sub_vars.insert(
           sub_vars.end(), ind_var_indicies.begin() + 1, ind_var_indicies.end());

diff --git a/src/theory/quantifiers/sygus/sygus_abduct.cpp b/src/theory/quantifiers/sygus/sygus_abduct.cpp
index fc7e7a1b9881deeb8f38fc066fe69e7a09f2fc15..3da55ff50833cb73801c98b85d341b95b2292413 100644 (file)
--- a/src/theory/quantifiers/sygus/sygus_abduct.cpp
+++ b/src/theory/quantifiers/sygus/sygus_abduct.cpp
@@ -28,7 +28,6 @@
 #include "theory/quantifiers/sygus/sygus_grammar_cons.h"
 #include "theory/quantifiers/sygus/sygus_utils.h"
 #include "theory/quantifiers/term_util.h"
-#include "theory/rewriter.h"
 
 using namespace std;
 using namespace cvc5::kind;
@@ -184,8 +183,6 @@ Node SygusAbduct::mkAbductionConjecture(const std::string& name,
   res = SygusUtils::mkSygusConjecture({abd}, res, {instAttr});
   Trace("sygus-abduct-debug") << "...finish" << std::endl;
 
-  res = theory::Rewriter::rewrite(res);
-
   Trace("sygus-abduct") << "Generate: " << res << std::endl;
 
   return res;

diff --git a/src/theory/substitutions.cpp b/src/theory/substitutions.cpp
index 70e3deb63b89221ed24448f362e02b5646520838..f910944817b2f9ae72adddc334407b7ed9649115 100644 (file)
--- a/src/theory/substitutions.cpp
+++ b/src/theory/substitutions.cpp
@@ -184,8 +184,8 @@ void SubstitutionMap::addSubstitutions(SubstitutionMap& subMap, bool invalidateC
   }
 }
 
-Node SubstitutionMap::apply(TNode t, bool doRewrite) {
-
+Node SubstitutionMap::apply(TNode t, Rewriter* r)
+{
   Debug("substitution") << "SubstitutionMap::apply(" << t << ")" << endl;
 
   // Setup the cache
@@ -199,9 +199,9 @@ Node SubstitutionMap::apply(TNode t, bool doRewrite) {
   Node result = internalSubstitute(t, d_substitutionCache);
   Debug("substitution") << "SubstitutionMap::apply(" << t << ") => " << result << endl;
 
-  if (doRewrite)
+  if (r != nullptr)
   {
-    result = Rewriter::rewrite(result);
+    result = r->rewrite(result);
   }
 
   return result;

diff --git a/src/theory/substitutions.h b/src/theory/substitutions.h
index 1de636fb3e9cd12b974ee1aeb5383f2422465a03..7a3afcb1188ad18c379bab767ca6b02a9aec3864 100644 (file)
--- a/src/theory/substitutions.h
+++ b/src/theory/substitutions.h
@@ -32,6 +32,8 @@
 namespace cvc5 {
 namespace theory {
 
+class Rewriter;
+
 /**
  * The type for the Substitutions mapping output by
  * Theory::simplify(), TheoryEngine::simplify(), and
@@ -125,16 +127,17 @@ class SubstitutionMap
   }
 
   /**
-   * Apply the substitutions to the node.
+   * Apply the substitutions to the node, optionally rewrite if a non-null
+   * Rewriter pointer is passed.
    */
-  Node apply(TNode t, bool doRewrite = false);
+  Node apply(TNode t, Rewriter* r = nullptr);
 
   /**
    * Apply the substitutions to the node.
    */
-  Node apply(TNode t, bool doRewrite = false) const
+  Node apply(TNode t, Rewriter* r = nullptr) const
   {
-    return const_cast<SubstitutionMap*>(this)->apply(t, doRewrite);
+    return const_cast<SubstitutionMap*>(this)->apply(t, r);
   }
 
   iterator begin() { return d_substitutions.begin(); }

diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp
index 0796831163a3337b489cca7dc05c24224cdd8827..33ec5b23bb34aba85cf9398b61b5886172986d4f 100644 (file)
--- a/src/theory/theory_model.cpp
+++ b/src/theory/theory_model.cpp
@@ -135,6 +135,7 @@ Node TheoryModel::getValue(TNode n) const
 {
   //apply substitutions
   Node nn = d_env.getTopLevelSubstitutions().apply(n);
+  nn = rewrite(nn);
   Debug("model-getvalue-debug") << "[model-getvalue] getValue : substitute " << n << " to " << nn << std::endl;
   //get value in model
   nn = getModelValue(nn);

diff --git a/src/theory/trust_substitutions.cpp b/src/theory/trust_substitutions.cpp
index c732650959384abe3937c0c1865dbc0bc0cd3ca1..ea87829a9ffc0debe096d17d34b57e41008313aa 100644 (file)
--- a/src/theory/trust_substitutions.cpp
+++ b/src/theory/trust_substitutions.cpp
@@ -145,11 +145,11 @@ void TrustSubstitutionMap::addSubstitutions(TrustSubstitutionMap& t)
   }
 }
 
-TrustNode TrustSubstitutionMap::applyTrusted(Node n, bool doRewrite)
+TrustNode TrustSubstitutionMap::applyTrusted(Node n, Rewriter* r)
 {
   Trace("trust-subs") << "TrustSubstitutionMap::addSubstitution: apply " << n
                       << std::endl;
-  Node ns = d_subs.apply(n, doRewrite);
+  Node ns = d_subs.apply(n, r);
   Trace("trust-subs") << "...subs " << ns << std::endl;
   if (n == ns)
   {
@@ -172,9 +172,9 @@ TrustNode TrustSubstitutionMap::applyTrusted(Node n, bool doRewrite)
   return TrustNode::mkTrustRewrite(n, ns, this);
 }
 
-Node TrustSubstitutionMap::apply(Node n, bool doRewrite)
+Node TrustSubstitutionMap::apply(Node n, Rewriter* r)
 {
-  return d_subs.apply(n, doRewrite);
+  return d_subs.apply(n, r);
 }
 
 std::shared_ptr<ProofNode> TrustSubstitutionMap::getProofFor(Node eq)

diff --git a/src/theory/trust_substitutions.h b/src/theory/trust_substitutions.h
index cc08c870d35d0a22afcdc22bab1000bb9fe0b55b..abcf039ba013027475d085096bd15504bde0b4fe 100644 (file)
--- a/src/theory/trust_substitutions.h
+++ b/src/theory/trust_substitutions.h
@@ -87,11 +87,12 @@ class TrustSubstitutionMap : public ProofGenerator
   /**
    * Apply substitutions in this class to node n. Returns a trust node
    * proving n = n*sigma, where the proof generator is provided by this class
-   * (when proofs are enabled).
+   * (when proofs are enabled). If a non-null rewriter is provided, the result
+   * of the substitution is rewritten.
    */
-  TrustNode applyTrusted(Node n, bool doRewrite = true);
+  TrustNode applyTrusted(Node n, Rewriter* r = nullptr);
   /** Same as above, without proofs */
-  Node apply(Node n, bool doRewrite = true);
+  Node apply(Node n, Rewriter* r = nullptr);
 
   /** Get the proof for formula f */
   std::shared_ptr<ProofNode> getProofFor(Node f) override;