bv: Rename BBSimple to NodeBitblaster. (#6891)

8 files changed, 36 insertions, 36 deletions

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 015f00f8f..95b6f401e 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -576,10 +576,10 @@ libcvc5_add_sources(
   theory/bv/bitblast/eager_bitblaster.h
   theory/bv/bitblast/lazy_bitblaster.cpp
   theory/bv/bitblast/lazy_bitblaster.h
+  theory/bv/bitblast/node_bitblaster.cpp
+  theory/bv/bitblast/node_bitblaster.h
   theory/bv/bitblast/proof_bitblaster.cpp
   theory/bv/bitblast/proof_bitblaster.h
-  theory/bv/bitblast/simple_bitblaster.cpp
-  theory/bv/bitblast/simple_bitblaster.h
   theory/bv/bv_eager_solver.cpp
   theory/bv/bv_eager_solver.h
   theory/bv/bv_inequality_graph.cpp
diff --git a/src/theory/bv/bitblast/simple_bitblaster.cpp b/src/theory/bv/bitblast/node_bitblaster.cpp
index 357a54b1a..fcfa05615 100644
--- a/src/theory/bv/bitblast/simple_bitblaster.cpp
+++ b/src/theory/bv/bitblast/node_bitblaster.cpp
@@ -10,22 +10,23 @@
  * directory for licensing information.
  * ****************************************************************************
  *
- * Bitblaster for simple BV solver.
- *
+ * Bitblaster used to bitblast to Boolean Nodes.
  */
-#include "theory/bv/bitblast/simple_bitblaster.h"
+#include "theory/bv/bitblast/node_bitblaster.h"
 
+#include "options/bv_options.h"
 #include "theory/theory_model.h"
 #include "theory/theory_state.h"
-#include "options/bv_options.h"
 
 namespace cvc5 {
 namespace theory {
 namespace bv {
 
-BBSimple::BBSimple(TheoryState* s) : TBitblaster<Node>(), d_state(s) {}
+NodeBitblaster::NodeBitblaster(TheoryState* s) : TBitblaster<Node>(), d_state(s)
+{
+}
 
-void BBSimple::bbAtom(TNode node)
+void NodeBitblaster::bbAtom(TNode node)
 {
   node = node.getKind() == kind::NOT ? node[0] : node;
 
@@ -44,17 +45,17 @@ void BBSimple::bbAtom(TNode node)
   storeBBAtom(node, Rewriter::rewrite(atom_bb));
 }
 
-void BBSimple::storeBBAtom(TNode atom, Node atom_bb)
+void NodeBitblaster::storeBBAtom(TNode atom, Node atom_bb)
 {
   d_bbAtoms.emplace(atom, atom_bb);
 }
 
-void BBSimple::storeBBTerm(TNode node, const Bits& bits)
+void NodeBitblaster::storeBBTerm(TNode node, const Bits& bits)
 {
   d_termCache.emplace(node, bits);
 }
 
-bool BBSimple::hasBBAtom(TNode lit) const
+bool NodeBitblaster::hasBBAtom(TNode lit) const
 {
   if (lit.getKind() == kind::NOT)
   {
@@ -63,7 +64,7 @@ bool BBSimple::hasBBAtom(TNode lit) const
   return d_bbAtoms.find(lit) != d_bbAtoms.end();
 }
 
-void BBSimple::makeVariable(TNode var, Bits& bits)
+void NodeBitblaster::makeVariable(TNode var, Bits& bits)
 {
   Assert(bits.size() == 0);
   for (unsigned i = 0; i < utils::getSize(var); ++i)
@@ -73,9 +74,9 @@ void BBSimple::makeVariable(TNode var, Bits& bits)
   d_variables.insert(var);
 }
 
-Node BBSimple::getBBAtom(TNode node) const { return node; }
+Node NodeBitblaster::getBBAtom(TNode node) const { return node; }
 
-void BBSimple::bbTerm(TNode node, Bits& bits)
+void NodeBitblaster::bbTerm(TNode node, Bits& bits)
 {
   Assert(node.getType().isBitVector());
   if (hasBBTerm(node))
@@ -88,7 +89,7 @@ void BBSimple::bbTerm(TNode node, Bits& bits)
   storeBBTerm(node, bits);
 }
 
-Node BBSimple::getStoredBBAtom(TNode node)
+Node NodeBitblaster::getStoredBBAtom(TNode node)
 {
   bool negated = false;
   if (node.getKind() == kind::NOT)
@@ -102,7 +103,7 @@ Node BBSimple::getStoredBBAtom(TNode node)
   return negated ? atom_bb.negate() : atom_bb;
 }
 
-Node BBSimple::getModelFromSatSolver(TNode a, bool fullModel)
+Node NodeBitblaster::getModelFromSatSolver(TNode a, bool fullModel)
 {
   if (!hasBBTerm(a))
   {
@@ -130,7 +131,7 @@ Node BBSimple::getModelFromSatSolver(TNode a, bool fullModel)
   return utils::mkConst(bits.size(), value);
 }
 
-void BBSimple::computeRelevantTerms(std::set<Node>& termSet)
+void NodeBitblaster::computeRelevantTerms(std::set<Node>& termSet)
 {
   Assert(options::bitblastMode() == options::BitblastMode::EAGER);
   for (const auto& var : d_variables)
@@ -139,8 +140,8 @@ void BBSimple::computeRelevantTerms(std::set<Node>& termSet)
   }
 }
 
-bool BBSimple::collectModelValues(TheoryModel* m,
-                                  const std::set<Node>& relevantTerms)
+bool NodeBitblaster::collectModelValues(TheoryModel* m,
+                                        const std::set<Node>& relevantTerms)
 {
   for (const auto& var : relevantTerms)
   {
@@ -159,7 +160,7 @@ bool BBSimple::collectModelValues(TheoryModel* m,
   return true;
 }
 
-bool BBSimple::isVariable(TNode node)
+bool NodeBitblaster::isVariable(TNode node)
 {
   return d_variables.find(node) != d_variables.end();
 }
diff --git a/src/theory/bv/bitblast/simple_bitblaster.h b/src/theory/bv/bitblast/node_bitblaster.h
index ec0899145..9b3bdda07 100644
--- a/src/theory/bv/bitblast/simple_bitblaster.h
+++ b/src/theory/bv/bitblast/node_bitblaster.h
@@ -10,12 +10,12 @@
  * directory for licensing information.
  * ****************************************************************************
  *
- * Bitblaster for simple BV solver.
+ * Bitblaster used to bitblast to Boolean Nodes.
  */
 #include "cvc5_private.h"
 
-#ifndef CVC5__THEORY__BV__BITBLAST_SIMPLE_BITBLASTER_H
-#define CVC5__THEORY__BV__BITBLAST_SIMPLE_BITBLASTER_H
+#ifndef CVC5__THEORY__BV__BITBLAST_NODE_BITBLASTER_H
+#define CVC5__THEORY__BV__BITBLAST_NODE_BITBLASTER_H
 
 #include "theory/bv/bitblast/bitblaster.h"
 
@@ -28,13 +28,13 @@ namespace bv {
  *
  * Implements the bare minimum to bit-blast bit-vector atoms/terms.
  */
-class BBSimple : public TBitblaster<Node>
+class NodeBitblaster : public TBitblaster<Node>
 {
   using Bits = std::vector<Node>;
 
  public:
-  BBSimple(TheoryState* state);
-  ~BBSimple() = default;
+  NodeBitblaster(TheoryState* state);
+  ~NodeBitblaster() = default;
 
   /** Bit-blast term 'node' and return bit-blasted 'bits'. */
   void bbTerm(TNode node, Bits& bits) override;
diff --git a/src/theory/bv/bitblast/proof_bitblaster.cpp b/src/theory/bv/bitblast/proof_bitblaster.cpp
index 9d4de1387..f714ffda9 100644
--- a/src/theory/bv/bitblast/proof_bitblaster.cpp
+++ b/src/theory/bv/bitblast/proof_bitblaster.cpp
@@ -24,7 +24,7 @@ namespace theory {
 namespace bv {
 
 BBProof::BBProof(TheoryState* state, ProofNodeManager* pnm, bool fineGrained)
-    : d_bb(new BBSimple(state)),
+    : d_bb(new NodeBitblaster(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 17be4204c..f6aa71f21 100644
--- a/src/theory/bv/bitblast/proof_bitblaster.h
+++ b/src/theory/bv/bitblast/proof_bitblaster.h
@@ -10,7 +10,7 @@
  * directory for licensing information.
  * ****************************************************************************
  *
- * A bit-blaster wrapper around BBSimple for proof logging.
+ * A bit-blaster wrapper around NodeBitblaster for proof logging.
  */
 #include "cvc5_private.h"
 
@@ -18,7 +18,7 @@
 #define CVC5__THEORY__BV__BITBLAST__PROOF_BITBLASTER_H
 
 #include "expr/term_context.h"
-#include "theory/bv/bitblast/simple_bitblaster.h"
+#include "theory/bv/bitblast/node_bitblaster.h"
 
 namespace cvc5 {
 
@@ -53,7 +53,7 @@ class BBProof
   bool isProofsEnabled() const;
 
   /** The associated simple bit-blaster. */
-  std::unique_ptr<BBSimple> d_bb;
+  std::unique_ptr<NodeBitblaster> d_bb;
   /** The associated proof node manager. */
   ProofNodeManager* d_pnm;
   /** Term context for d_tcpg to not rewrite below BV leafs. */
diff --git a/src/theory/bv/bv_solver_bitblast.cpp b/src/theory/bv/bv_solver_bitblast.cpp
index 613ba47bf..5b70fb3a2 100644
--- a/src/theory/bv/bv_solver_bitblast.cpp
+++ b/src/theory/bv/bv_solver_bitblast.cpp
@@ -78,7 +78,7 @@ class NotifyResetAssertions : public context::ContextNotifyObj
 class BBRegistrar : public prop::Registrar
 {
  public:
-  BBRegistrar(BBSimple* bb) : d_bitblaster(bb) {}
+  BBRegistrar(NodeBitblaster* bb) : d_bitblaster(bb) {}
 
   void preRegister(Node n) override
   {
@@ -102,7 +102,7 @@ class BBRegistrar : public prop::Registrar
 
  private:
   /** The bitblaster used. */
-  BBSimple* d_bitblaster;
+  NodeBitblaster* d_bitblaster;
 
   /** Stores bit-vector atoms encounterd on preRegister(). */
   std::unordered_set<TNode> d_registeredAtoms;
@@ -112,7 +112,7 @@ BVSolverBitblast::BVSolverBitblast(TheoryState* s,
                                    TheoryInferenceManager& inferMgr,
                                    ProofNodeManager* pnm)
     : BVSolver(*s, inferMgr),
-      d_bitblaster(new BBSimple(s)),
+      d_bitblaster(new NodeBitblaster(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.h b/src/theory/bv/bv_solver_bitblast.h
index 1fb721deb..87f3f25cd 100644
--- a/src/theory/bv/bv_solver_bitblast.h
+++ b/src/theory/bv/bv_solver_bitblast.h
@@ -24,7 +24,7 @@
 #include "proof/eager_proof_generator.h"
 #include "prop/cnf_stream.h"
 #include "prop/sat_solver.h"
-#include "theory/bv/bitblast/simple_bitblaster.h"
+#include "theory/bv/bitblast/node_bitblaster.h"
 #include "theory/bv/bv_solver.h"
 #include "theory/bv/proof_checker.h"
 
@@ -106,7 +106,7 @@ class BVSolverBitblast : public BVSolver
   std::unordered_map<Node, Node> d_modelCache;
 
   /** Bit-blaster used to bit-blast atoms/terms. */
-  std::unique_ptr<BBSimple> d_bitblaster;
+  std::unique_ptr<NodeBitblaster> d_bitblaster;
 
   /** Used for initializing `d_cnfStream`. */
   std::unique_ptr<BBRegistrar> d_bbRegistrar;
diff --git a/src/theory/bv/proof_checker.h b/src/theory/bv/proof_checker.h
index c89dd359c..9d34e9a88 100644
--- a/src/theory/bv/proof_checker.h
+++ b/src/theory/bv/proof_checker.h
@@ -21,7 +21,6 @@
 #include "expr/node.h"
 #include "proof/proof_checker.h"
 #include "proof/proof_node.h"
-#include "theory/bv/bitblast/simple_bitblaster.h"
 
 namespace cvc5 {
 namespace theory {