bv: Remove remaining Rewriter::rewrite calls. (#7545)

diff --git a/src/theory/bv/bitblast/bitblast_proof_generator.cpp b/src/theory/bv/bitblast/bitblast_proof_generator.cpp
index 57435f65153884a1eb4872a716dd62abbaf21871..c05243e8cfcc7433d97ae596b50e4d0272b0f0a4 100644 (file)
--- a/src/theory/bv/bitblast/bitblast_proof_generator.cpp
+++ b/src/theory/bv/bitblast/bitblast_proof_generator.cpp
@@ -21,9 +21,10 @@ namespace cvc5 {
 namespace theory {
 namespace bv {
 
-BitblastProofGenerator::BitblastProofGenerator(ProofNodeManager* pnm,
+BitblastProofGenerator::BitblastProofGenerator(Env& env,
+                                               ProofNodeManager* pnm,
                                                TConvProofGenerator* tcpg)
-    : d_pnm(pnm), d_tcpg(tcpg)
+    : EnvObj(env), d_pnm(pnm), d_tcpg(tcpg)
 {
 }
 
@@ -78,7 +79,7 @@ std::shared_ptr<ProofNode> BitblastProofGenerator::getProofFor(Node eq)
      * sub-terms and recording these bit-blast steps in the conversion proof.
      */
 
-    Node rwt = Rewriter::rewrite(t);
+    Node rwt = rewrite(t);
 
     std::vector<Node> transSteps;
 
@@ -94,7 +95,7 @@ std::shared_ptr<ProofNode> BitblastProofGenerator::getProofFor(Node eq)
     transSteps.push_back(rwt.eqNode(bbt));
 
     // Record post-rewrite of bit-blasted term.
-    Node rwbbt = Rewriter::rewrite(bbt);
+    Node rwbbt = rewrite(bbt);
     if (bbt != rwbbt)
     {
       cdp.addStep(bbt.eqNode(rwbbt), PfRule::REWRITE, {}, {bbt});

diff --git a/src/theory/bv/bitblast/bitblast_proof_generator.h b/src/theory/bv/bitblast/bitblast_proof_generator.h
index 114bf474982d344e1ce668454922a05aa6b059f4..a0627010abc817b2bbdc8692f0378fe92b98a3fd 100644 (file)
--- a/src/theory/bv/bitblast/bitblast_proof_generator.h
+++ b/src/theory/bv/bitblast/bitblast_proof_generator.h
@@ -19,6 +19,7 @@
 
 #include "proof/proof_generator.h"
 #include "proof/proof_node_manager.h"
+#include "smt/env_obj.h"
 
 namespace cvc5 {
 
@@ -28,10 +29,12 @@ namespace theory {
 namespace bv {
 
 /** Proof generator fot bit-blast proofs. */
-class BitblastProofGenerator : public ProofGenerator
+class BitblastProofGenerator : public ProofGenerator, protected EnvObj
 {
  public:
-  BitblastProofGenerator(ProofNodeManager* pnm, TConvProofGenerator* tcpg);
+  BitblastProofGenerator(Env& env,
+                         ProofNodeManager* pnm,
+                         TConvProofGenerator* tcpg);
   ~BitblastProofGenerator(){};
 
   /**

diff --git a/src/theory/bv/bitblast/bitblaster.h b/src/theory/bv/bitblast/bitblaster.h
index ef75bd5f8a5519fcfa80090556bb86ba8d53b3f8..fddf6c51ea8cbd84f9318dba0883a7883dfbf59d 100644 (file)
--- a/src/theory/bv/bitblast/bitblaster.h
+++ b/src/theory/bv/bitblast/bitblaster.h
@@ -199,58 +199,6 @@ void TBitblaster<T>::invalidateModelCache()
   d_modelCache.clear();
 }
 
-template <class T>
-Node TBitblaster<T>::getTermModel(TNode node, bool fullModel)
-{
-  if (d_modelCache.find(node) != d_modelCache.end()) return d_modelCache[node];
-
-  if (node.isConst()) return node;
-
-  Node value = getModelFromSatSolver(node, false);
-  if (!value.isNull())
-  {
-    Debug("bv-equality-status")
-        << "TLazyBitblaster::getTermModel from SatSolver" << node << " => "
-        << value << "\n";
-    d_modelCache[node] = value;
-    Assert(value.isConst());
-    return value;
-  }
-
-  if (Theory::isLeafOf(node, theory::THEORY_BV))
-  {
-    // if it is a leaf may ask for fullModel
-    value = getModelFromSatSolver(node, true);
-    Debug("bv-equality-status") << "TLazyBitblaster::getTermModel from VarValue"
-                                << node << " => " << value << "\n";
-    Assert((fullModel && !value.isNull() && value.isConst()) || !fullModel);
-    if (!value.isNull())
-    {
-      d_modelCache[node] = value;
-    }
-    return value;
-  }
-  Assert(node.getType().isBitVector());
-
-  NodeBuilder nb(node.getKind());
-  if (node.getMetaKind() == kind::metakind::PARAMETERIZED)
-  {
-    nb << node.getOperator();
-  }
-
-  for (unsigned i = 0; i < node.getNumChildren(); ++i)
-  {
-    nb << getTermModel(node[i], fullModel);
-  }
-  value = nb;
-  value = Rewriter::rewrite(value);
-  Assert(value.isConst());
-  d_modelCache[node] = value;
-  Debug("bv-term-model") << "TLazyBitblaster::getTermModel Building Value"
-                         << node << " => " << value << "\n";
-  return value;
-}
-
 }  // namespace bv
 }  // namespace theory
 }  // namespace cvc5

diff --git a/src/theory/bv/bitblast/proof_bitblaster.cpp b/src/theory/bv/bitblast/proof_bitblaster.cpp
index 6119e9d7c3488de6206424d65df77be18176679a..d8f327b29ed747d23129ca148dfcd27531b060bb 100644 (file)
--- a/src/theory/bv/bitblast/proof_bitblaster.cpp
+++ b/src/theory/bv/bitblast/proof_bitblaster.cpp
@@ -45,7 +45,8 @@ BBProof::BBProof(Env& env,
                  d_tcontext.get(),
                  false)
                  : nullptr),
-      d_bbpg(pnm ? new BitblastProofGenerator(pnm, d_tcpg.get()) : nullptr),
+      d_bbpg(pnm ? new BitblastProofGenerator(env, pnm, d_tcpg.get())
+                 : nullptr),
       d_recordFineGrainedProofs(fineGrained)
 {
 }
@@ -75,7 +76,7 @@ void BBProof::bbAtom(TNode node)
     NodeManager* nm = NodeManager::currentNM();
 
     // post-rewrite atom
-    Node rwNode = Rewriter::rewrite(node);
+    Node rwNode = rewrite(node);
 
     // Post-order traversal of `rwNode` to make sure that all subterms are
     // bit-blasted and recorded.

diff --git a/src/theory/bv/theory_bv_rewrite_rules_normalization.h b/src/theory/bv/theory_bv_rewrite_rules_normalization.h
index 5ead8a215bafac18ef1ac3a5b5c0349ee2eae84e..d73497adf97851c99c9a7d1562a69cece9c83b18 100644 (file)
--- a/src/theory/bv/theory_bv_rewrite_rules_normalization.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_normalization.h
@@ -844,15 +844,9 @@ inline Node RewriteRule<SolveEq>::apply(TNode node)
 
   if (newLeft < newRight)
   {
-    Assert((newRight == left && newLeft == right)
-           || Rewriter::rewrite(newRight) != left
-           || Rewriter::rewrite(newLeft) != right);
     return newRight.eqNode(newLeft);
   }
 
-  Assert((newLeft == left && newRight == right)
-         || Rewriter::rewrite(newLeft) != left
-         || Rewriter::rewrite(newRight) != right);
   return newLeft.eqNode(newRight);
 }