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

This PR is based on #7171

4 files changed, 18 insertions, 10 deletions

diff --git a/src/theory/bv/bitblast/node_bitblaster.cpp b/src/theory/bv/bitblast/node_bitblaster.cpp
index fcfa05615..9f738634c 100644
--- 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 9b3bdda07..94b9d638b 100644
--- 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 43618974b..bef23c0b5 100644
--- 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 bc99d27bf..be150a0e8 100644
--- 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'. */