bv: Use EnvObj::rewrite() and EnvObj::options() in NodeBitblaster. (#7172)

This PR is based on #7171

diff --git a/src/smt/proof_post_processor.cpp b/src/smt/proof_post_processor.cpp
index f5d0e8ee813885686abadc832f430354092cea58..4bb875f7214463fc46943d69947b0979ccf0a4da 100644 (file)
--- a/src/smt/proof_post_processor.cpp
+++ b/src/smt/proof_post_processor.cpp
@@ -1105,7 +1105,7 @@ Node ProofPostprocessCallback::expandMacros(PfRule id,
   }
   else if (id == PfRule::BV_BITBLAST)
   {
-    bv::BBProof bb(nullptr, d_pnm, true);
+    bv::BBProof bb(d_env, nullptr, d_pnm, true);
     Node eq = args[0];
     Assert(eq.getKind() == EQUAL);
     bb.bbAtom(eq[0]);

diff --git a/src/theory/bv/bitblast/node_bitblaster.cpp b/src/theory/bv/bitblast/node_bitblaster.cpp
index fcfa056153381b4e8c89cd2a7d587b9465a9fda0..9f738634cd2a38f99ecd0a6c47d2908afb00eb47 100644 (file)
--- a/src/theory/bv/bitblast/node_bitblaster.cpp
+++ b/src/theory/bv/bitblast/node_bitblaster.cpp
@@ -22,7 +22,8 @@ namespace cvc5 {
 namespace theory {
 namespace bv {
 
-NodeBitblaster::NodeBitblaster(TheoryState* s) : TBitblaster<Node>(), d_state(s)
+NodeBitblaster::NodeBitblaster(Env& env, TheoryState* s)
+    : TBitblaster<Node>(), EnvObj(env), d_state(s)
 {
 }
 
@@ -35,14 +36,14 @@ void NodeBitblaster::bbAtom(TNode node)
     return;
   }
 
-  Node normalized = Rewriter::rewrite(node);
+  Node normalized = rewrite(node);
   Node atom_bb =
       normalized.getKind() != kind::CONST_BOOLEAN
               && normalized.getKind() != kind::BITVECTOR_BITOF
           ? d_atomBBStrategies[normalized.getKind()](normalized, this)
           : normalized;
 
-  storeBBAtom(node, Rewriter::rewrite(atom_bb));
+  storeBBAtom(node, rewrite(atom_bb));
 }
 
 void NodeBitblaster::storeBBAtom(TNode atom, Node atom_bb)
@@ -133,7 +134,7 @@ Node NodeBitblaster::getModelFromSatSolver(TNode a, bool fullModel)
 
 void NodeBitblaster::computeRelevantTerms(std::set<Node>& termSet)
 {
-  Assert(options::bitblastMode() == options::BitblastMode::EAGER);
+  Assert(options().bv.bitblastMode == options::BitblastMode::EAGER);
   for (const auto& var : d_variables)
   {
     termSet.insert(var);

diff --git a/src/theory/bv/bitblast/node_bitblaster.h b/src/theory/bv/bitblast/node_bitblaster.h
index 9b3bdda07c6df0a29d55531da913dbff135528da..94b9d638b663945ff9ccbff5887934f82dc21415 100644 (file)
--- a/src/theory/bv/bitblast/node_bitblaster.h
+++ b/src/theory/bv/bitblast/node_bitblaster.h
@@ -28,12 +28,12 @@ namespace bv {
  *
  * Implements the bare minimum to bit-blast bit-vector atoms/terms.
  */
-class NodeBitblaster : public TBitblaster<Node>
+class NodeBitblaster : public TBitblaster<Node>, protected EnvObj
 {
   using Bits = std::vector<Node>;
 
  public:
-  NodeBitblaster(TheoryState* state);
+  NodeBitblaster(Env& env, TheoryState* state);
   ~NodeBitblaster() = default;
 
   /** Bit-blast term 'node' and return bit-blasted 'bits'. */

diff --git a/src/theory/bv/bitblast/proof_bitblaster.cpp b/src/theory/bv/bitblast/proof_bitblaster.cpp
index 43618974b80307f8ba8a75910edfcd31e0306a07..bef23c0b5f523e154e9f420d0784ae3a46ea084e 100644 (file)
--- a/src/theory/bv/bitblast/proof_bitblaster.cpp
+++ b/src/theory/bv/bitblast/proof_bitblaster.cpp
@@ -23,8 +23,12 @@ namespace cvc5 {
 namespace theory {
 namespace bv {
 
-BBProof::BBProof(TheoryState* state, ProofNodeManager* pnm, bool fineGrained)
-    : d_bb(new NodeBitblaster(state)),
+BBProof::BBProof(Env& env,
+                 TheoryState* state,
+                 ProofNodeManager* pnm,
+                 bool fineGrained)
+    : EnvObj(env),
+      d_bb(new NodeBitblaster(env, state)),
       d_pnm(pnm),
       d_tcontext(new TheoryLeafTermContext(theory::THEORY_BV)),
       d_tcpg(pnm ? new TConvProofGenerator(

diff --git a/src/theory/bv/bitblast/proof_bitblaster.h b/src/theory/bv/bitblast/proof_bitblaster.h
index bc99d27bff93f328ce28fe70b8d8cf6a2ccfe671..be150a0e83c340b127d27305023b2233371b4d18 100644 (file)
--- a/src/theory/bv/bitblast/proof_bitblaster.h
+++ b/src/theory/bv/bitblast/proof_bitblaster.h
@@ -27,12 +27,15 @@ class TConvProofGenerator;
 namespace theory {
 namespace bv {
 
-class BBProof
+class BBProof : protected EnvObj
 {
   using Bits = std::vector<Node>;
 
  public:
-  BBProof(TheoryState* state, ProofNodeManager* pnm, bool fineGrained);
+  BBProof(Env& env,
+          TheoryState* state,
+          ProofNodeManager* pnm,
+          bool fineGrained);
   ~BBProof();
 
   /** Bit-blast atom 'node'. */

diff --git a/src/theory/bv/bv_solver_bitblast.cpp b/src/theory/bv/bv_solver_bitblast.cpp
index 9d316e91e66118dc32595146bb7ce779129386bc..bb9cdb011e2a15f0328ff00a13dbd6c6928fc7b6 100644 (file)
--- a/src/theory/bv/bv_solver_bitblast.cpp
+++ b/src/theory/bv/bv_solver_bitblast.cpp
@@ -113,7 +113,7 @@ BVSolverBitblast::BVSolverBitblast(Env& env,
                                    TheoryInferenceManager& inferMgr,
                                    ProofNodeManager* pnm)
     : BVSolver(env, *s, inferMgr),
-      d_bitblaster(new NodeBitblaster(s)),
+      d_bitblaster(new NodeBitblaster(env, s)),
       d_bbRegistrar(new BBRegistrar(d_bitblaster.get())),
       d_nullContext(new context::Context()),
       d_bbFacts(s->getSatContext()),

diff --git a/src/theory/bv/bv_solver_bitblast_internal.cpp b/src/theory/bv/bv_solver_bitblast_internal.cpp
index 71a29f472f264b23baa6da71cc419f757364a8b3..490ba325c80ed836da04d524f96078d6100e7c2f 100644 (file)
--- a/src/theory/bv/bv_solver_bitblast_internal.cpp
+++ b/src/theory/bv/bv_solver_bitblast_internal.cpp
@@ -74,7 +74,7 @@ BVSolverBitblastInternal::BVSolverBitblastInternal(
     ProofNodeManager* pnm)
     : BVSolver(env, *s, inferMgr),
       d_pnm(pnm),
-      d_bitblaster(new BBProof(s, pnm, false))
+      d_bitblaster(new BBProof(env, s, pnm, false))
 {
 }