From 978f295178a2e70e16aca2ce2b951cc9afe2be40 Mon Sep 17 00:00:00 2001
From: Mathias Preiner <mathias.preiner@gmail.com>
Date: Fri, 10 Sep 2021 10:58:35 -0700
Subject: [PATCH] bv: Use EnvObj::rewrite() and EnvObj::options() in
 NodeBitblaster. (#7172)

This PR is based on #7171
---
 src/smt/proof_post_processor.cpp              | 2 +-
 src/theory/bv/bitblast/node_bitblaster.cpp    | 9 +++++----
 src/theory/bv/bitblast/node_bitblaster.h      | 4 ++--
 src/theory/bv/bitblast/proof_bitblaster.cpp   | 8 ++++++--
 src/theory/bv/bitblast/proof_bitblaster.h     | 7 +++++--
 src/theory/bv/bv_solver_bitblast.cpp          | 2 +-
 src/theory/bv/bv_solver_bitblast_internal.cpp | 2 +-
 7 files changed, 21 insertions(+), 13 deletions(-)

diff --git a/src/smt/proof_post_processor.cpp b/src/smt/proof_post_processor.cpp
index f5d0e8ee8..4bb875f72 100644
--- 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 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'. */
diff --git a/src/theory/bv/bv_solver_bitblast.cpp b/src/theory/bv/bv_solver_bitblast.cpp
index 9d316e91e..bb9cdb011 100644
--- 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 71a29f472..490ba325c 100644
--- 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))
 {
 }
 
-- 
2.30.2