From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 20 Oct 2021 21:07:09 +0000 (-0500)
Subject: Eliminate last static calls to rewriter from smt layer (#7355)
X-Git-Tag: cvc5-1.0.0~1035
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=09c6f9514b993c78c662ff6d3f46acce97286068;p=cvc5.git

Eliminate last static calls to rewriter from smt layer (#7355)
---

diff --git a/src/proof/proof_node_manager.cpp b/src/proof/proof_node_manager.cpp
index a3ef944e0..8b4b332a1 100644
--- a/src/proof/proof_node_manager.cpp
+++ b/src/proof/proof_node_manager.cpp
@@ -28,7 +28,8 @@ using namespace cvc5::kind;
 
 namespace cvc5 {
 
-ProofNodeManager::ProofNodeManager(ProofChecker* pc) : d_checker(pc)
+ProofNodeManager::ProofNodeManager(theory::Rewriter* rr, ProofChecker* pc)
+    : d_rewriter(rr), d_checker(pc)
 {
   d_true = NodeManager::currentNM()->mkConst(true);
   // we always allocate a proof checker, regardless of the proof checking mode
@@ -160,14 +161,14 @@ std::shared_ptr<ProofNode> ProofNodeManager::mkScope(
         computedAcr = true;
         for (const Node& acc : ac)
         {
-          Node accr = theory::Rewriter::rewrite(acc);
+          Node accr = d_rewriter->rewrite(acc);
           if (accr != acc)
           {
             acr[accr] = acc;
           }
         }
       }
-      Node ar = theory::Rewriter::rewrite(a);
+      Node ar = d_rewriter->rewrite(a);
       std::unordered_map<Node, Node>::iterator itr = acr.find(ar);
       if (itr != acr.end())
       {
diff --git a/src/proof/proof_node_manager.h b/src/proof/proof_node_manager.h
index 928aabb76..533f6d173 100644
--- a/src/proof/proof_node_manager.h
+++ b/src/proof/proof_node_manager.h
@@ -28,6 +28,10 @@ namespace cvc5 {
 class ProofChecker;
 class ProofNode;
 
+namespace theory {
+class Rewriter;
+}
+
 /**
  * A manager for proof node objects. This is a trusted interface for creating
  * and updating ProofNode objects.
@@ -54,7 +58,7 @@ class ProofNode;
 class ProofNodeManager
 {
  public:
-  ProofNodeManager(ProofChecker* pc = nullptr);
+  ProofNodeManager(theory::Rewriter* rr, ProofChecker* pc = nullptr);
   ~ProofNodeManager() {}
   /**
    * This constructs a ProofNode with the given arguments. The expected
@@ -184,6 +188,8 @@ class ProofNodeManager
   static ProofNode* cancelDoubleSymm(ProofNode* pn);
 
  private:
+  /** The rewriter */
+  theory::Rewriter* d_rewriter;
   /** The (optional) proof checker */
   ProofChecker* d_checker;
   /** the true node */
diff --git a/src/smt/check_models.cpp b/src/smt/check_models.cpp
index f148d1018..36d107429 100644
--- a/src/smt/check_models.cpp
+++ b/src/smt/check_models.cpp
@@ -31,8 +31,7 @@ using namespace cvc5::theory;
 namespace cvc5 {
 namespace smt {
 
-CheckModels::CheckModels(Env& e) : d_env(e) {}
-CheckModels::~CheckModels() {}
+CheckModels::CheckModels(Env& e) : EnvObj(e) {}
 
 void CheckModels::checkModel(TheoryModel* m,
                              const context::CDList<Node>& al,
@@ -71,7 +70,7 @@ void CheckModels::checkModel(TheoryModel* m,
     Notice() << "SolverEngine::checkModel(): -- substitutes to " << n
              << std::endl;
 
-    n = Rewriter::rewrite(n);
+    n = rewrite(n);
     Notice() << "SolverEngine::checkModel(): -- rewrites to " << n << std::endl;
 
     // We look up the value before simplifying. If n contains quantifiers,
diff --git a/src/smt/check_models.h b/src/smt/check_models.h
index d785b53d5..2b3447010 100644
--- a/src/smt/check_models.h
+++ b/src/smt/check_models.h
@@ -20,11 +20,10 @@
 
 #include "context/cdlist.h"
 #include "expr/node.h"
+#include "smt/env_obj.h"
 
 namespace cvc5 {
 
-class Env;
-
 namespace theory {
 class TheoryModel;
 }
@@ -34,11 +33,10 @@ namespace smt {
 /**
  * This utility is responsible for checking the current model.
  */
-class CheckModels
+class CheckModels : protected EnvObj
 {
  public:
   CheckModels(Env& e);
-  ~CheckModels();
   /**
    * Check model m against the current set of input assertions al.
    *
@@ -48,10 +46,6 @@ class CheckModels
   void checkModel(theory::TheoryModel* m,
                   const context::CDList<Node>& al,
                   bool hardFailure);
-
- private:
-  /** Reference to the environment */
-  Env& d_env;
 };
 
 }  // namespace smt
diff --git a/src/smt/model_blocker.cpp b/src/smt/model_blocker.cpp
index cbc388331..e8c1ff07f 100644
--- a/src/smt/model_blocker.cpp
+++ b/src/smt/model_blocker.cpp
@@ -25,6 +25,8 @@ using namespace cvc5::kind;
 
 namespace cvc5 {
 
+ModelBlocker::ModelBlocker(Env& e) : EnvObj(e) {}
+
 Node ModelBlocker::getModelBlocker(const std::vector<Node>& assertions,
                                    theory::TheoryModel* m,
                                    options::BlockModelsMode mode,
diff --git a/src/smt/model_blocker.h b/src/smt/model_blocker.h
index 42219e220..5e41de6a3 100644
--- a/src/smt/model_blocker.h
+++ b/src/smt/model_blocker.h
@@ -22,6 +22,7 @@
 
 #include "expr/node.h"
 #include "options/smt_options.h"
+#include "smt/env_obj.h"
 
 namespace cvc5 {
 
@@ -32,9 +33,10 @@ class TheoryModel;
 /**
  * A utility for blocking the current model.
  */
-class ModelBlocker
+class ModelBlocker : protected EnvObj
 {
  public:
+  ModelBlocker(Env& e);
   /** get model blocker
    *
    * This returns a disjunction of literals ~L1 V ... V ~Ln with the following
@@ -63,7 +65,7 @@ class ModelBlocker
    * our input. In other words, we do not return ~(x < 0) V ~(w < 0) since the
    * left disjunct is always false.
    */
-  static Node getModelBlocker(
+  Node getModelBlocker(
       const std::vector<Node>& assertions,
       theory::TheoryModel* m,
       options::BlockModelsMode mode,
diff --git a/src/smt/preprocessor.cpp b/src/smt/preprocessor.cpp
index 4b16b9391..3aed58b30 100644
--- a/src/smt/preprocessor.cpp
+++ b/src/smt/preprocessor.cpp
@@ -150,7 +150,7 @@ Node Preprocessor::simplify(const Node& node)
     d_env.getPrinter().toStreamCmdSimplify(d_env.getDumpOut(), node);
   }
   Node ret = expandDefinitions(node);
-  ret = theory::Rewriter::rewrite(ret);
+  ret = rewrite(ret);
   return ret;
 }
 
diff --git a/src/smt/proof_manager.cpp b/src/smt/proof_manager.cpp
index 2e08ab2df..4b4291075 100644
--- a/src/smt/proof_manager.cpp
+++ b/src/smt/proof_manager.cpp
@@ -41,7 +41,7 @@ PfManager::PfManager(Env& env)
       d_pchecker(new ProofChecker(
           options().proof.proofCheck == options::ProofCheckMode::EAGER,
           options().proof.proofPedantic)),
-      d_pnm(new ProofNodeManager(d_pchecker.get())),
+      d_pnm(new ProofNodeManager(env.getRewriter(), d_pchecker.get())),
       d_pppg(new PreprocessProofGenerator(
           d_pnm.get(), env.getUserContext(), "smt::PreprocessProofGenerator")),
       d_pfpp(nullptr),
diff --git a/src/smt/proof_post_processor.cpp b/src/smt/proof_post_processor.cpp
index a547c4362..04a36c1c0 100644
--- a/src/smt/proof_post_processor.cpp
+++ b/src/smt/proof_post_processor.cpp
@@ -42,7 +42,7 @@ ProofPostprocessCallback::ProofPostprocessCallback(Env& env,
     : d_env(env),
       d_pnm(env.getProofNodeManager()),
       d_pppg(pppg),
-      d_wfpm(env.getProofNodeManager()),
+      d_wfpm(env),
       d_updateScopedAssumptions(updateScopedAssumptions)
 {
   d_true = NodeManager::currentNM()->mkConst(true);
diff --git a/src/smt/solver_engine.cpp b/src/smt/solver_engine.cpp
index e928dcade..fc6ec3915 100644
--- a/src/smt/solver_engine.cpp
+++ b/src/smt/solver_engine.cpp
@@ -1081,7 +1081,7 @@ Node SolverEngine::getValue(const Node& ex) const
   // AJR : necessary?
   if (!n.getType().isFunction())
   {
-    n = Rewriter::rewrite(n);
+    n = d_env->getRewriter()->rewrite(n);
   }
 
   Trace("smt") << "--- getting value of " << n << endl;
@@ -1224,7 +1224,8 @@ Result SolverEngine::blockModel()
 
   // get expanded assertions
   std::vector<Node> eassertsProc = getExpandedAssertions();
-  Node eblocker = ModelBlocker::getModelBlocker(
+  ModelBlocker mb(*d_env.get());
+  Node eblocker = mb.getModelBlocker(
       eassertsProc, m, d_env->getOptions().smt.blockModelsMode);
   Trace("smt") << "Block formula: " << eblocker << std::endl;
   return assertFormula(eblocker);
@@ -1247,7 +1248,8 @@ Result SolverEngine::blockModelValues(const std::vector<Node>& exprs)
   // get expanded assertions
   std::vector<Node> eassertsProc = getExpandedAssertions();
   // we always do block model values mode here
-  Node eblocker = ModelBlocker::getModelBlocker(
+  ModelBlocker mb(*d_env.get());
+  Node eblocker = mb.getModelBlocker(
       eassertsProc, m, options::BlockModelsMode::VALUES, exprs);
   return assertFormula(eblocker);
 }
diff --git a/src/smt/sygus_solver.cpp b/src/smt/sygus_solver.cpp
index 2a1d4e6c6..5db9804c6 100644
--- a/src/smt/sygus_solver.cpp
+++ b/src/smt/sygus_solver.cpp
@@ -377,7 +377,7 @@ void SygusSolver::checkSynthSolution(Assertions& as)
       // problem are rewritten to true. If this is not the case, then the
       // assertions module of the subsolver will complain about assertions
       // with free variables.
-      Node ar = theory::Rewriter::rewrite(a);
+      Node ar = rewrite(a);
       solChecker->assertFormula(ar);
     }
     Result r = solChecker->checkSat();
diff --git a/src/smt/witness_form.cpp b/src/smt/witness_form.cpp
index 8e998b9cf..16d297495 100644
--- a/src/smt/witness_form.cpp
+++ b/src/smt/witness_form.cpp
@@ -16,21 +16,27 @@
 #include "smt/witness_form.h"
 
 #include "expr/skolem_manager.h"
+#include "smt/env.h"
 #include "theory/rewriter.h"
 
 namespace cvc5 {
 namespace smt {
 
-WitnessFormGenerator::WitnessFormGenerator(ProofNodeManager* pnm)
-    : d_tcpg(pnm,
+WitnessFormGenerator::WitnessFormGenerator(Env& env)
+    : d_rewriter(env.getRewriter()),
+      d_tcpg(env.getProofNodeManager(),
              nullptr,
              TConvPolicy::FIXPOINT,
              TConvCachePolicy::NEVER,
              "WfGenerator::TConvProofGenerator",
              nullptr,
              true),
-      d_wintroPf(pnm, nullptr, nullptr, "WfGenerator::LazyCDProof"),
-      d_pskPf(pnm, nullptr, "WfGenerator::PurifySkolemProof")
+      d_wintroPf(env.getProofNodeManager(),
+                 nullptr,
+                 nullptr,
+                 "WfGenerator::LazyCDProof"),
+      d_pskPf(
+          env.getProofNodeManager(), nullptr, "WfGenerator::PurifySkolemProof")
 {
 }
 
@@ -114,12 +120,12 @@ Node WitnessFormGenerator::convertToWitnessForm(Node t)
 
 bool WitnessFormGenerator::requiresWitnessFormTransform(Node t, Node s) const
 {
-  return theory::Rewriter::rewrite(t) != theory::Rewriter::rewrite(s);
+  return d_rewriter->rewrite(t) != d_rewriter->rewrite(s);
 }
 
 bool WitnessFormGenerator::requiresWitnessFormIntro(Node t) const
 {
-  Node tr = theory::Rewriter::rewrite(t);
+  Node tr = d_rewriter->rewrite(t);
   return !tr.isConst() || !tr.getConst<bool>();
 }
 
diff --git a/src/smt/witness_form.h b/src/smt/witness_form.h
index 8522d41f0..06d60c1ed 100644
--- a/src/smt/witness_form.h
+++ b/src/smt/witness_form.h
@@ -25,6 +25,13 @@
 #include "proof/proof_generator.h"
 
 namespace cvc5 {
+
+class Env;
+
+namespace theory {
+class Rewriter;
+}
+
 namespace smt {
 
 /**
@@ -37,7 +44,7 @@ namespace smt {
 class WitnessFormGenerator : public ProofGenerator
 {
  public:
-  WitnessFormGenerator(ProofNodeManager* pnm);
+  WitnessFormGenerator(Env& env);
   ~WitnessFormGenerator() {}
   /**
    * Get proof for, which expects an equality of the form t = toWitness(t).
@@ -85,6 +92,8 @@ class WitnessFormGenerator : public ProofGenerator
    * Return a proof generator that can prove the given axiom exists.
    */
   ProofGenerator* convertExistsInternal(Node exists);
+  /** The rewriter we are using */
+  theory::Rewriter* d_rewriter;
   /** The term conversion proof generator */
   TConvProofGenerator d_tcpg;
   /** The nodes we have already added rewrite steps for in d_tcpg */