From d7bb2484436a55c6b2df08bcae7549809e3ad264 Mon Sep 17 00:00:00 2001 From: Mathias Preiner Date: Wed, 14 Jul 2021 19:19:12 -0700 Subject: [PATCH] bv: Rename BBSimple to NodeBitblaster. (#6891) --- src/CMakeLists.txt | 4 +- ...ple_bitblaster.cpp => node_bitblaster.cpp} | 37 ++++++++++--------- ...{simple_bitblaster.h => node_bitblaster.h} | 12 +++--- src/theory/bv/bitblast/proof_bitblaster.cpp | 2 +- src/theory/bv/bitblast/proof_bitblaster.h | 6 +-- src/theory/bv/bv_solver_bitblast.cpp | 6 +-- src/theory/bv/bv_solver_bitblast.h | 4 +- src/theory/bv/proof_checker.h | 1 - 8 files changed, 36 insertions(+), 36 deletions(-) rename src/theory/bv/bitblast/{simple_bitblaster.cpp => node_bitblaster.cpp} (76%) rename src/theory/bv/bitblast/{simple_bitblaster.h => node_bitblaster.h} (90%) 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 similarity index 76% rename from src/theory/bv/bitblast/simple_bitblaster.cpp rename to 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(), d_state(s) {} +NodeBitblaster::NodeBitblaster(TheoryState* s) : TBitblaster(), 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& termSet) +void NodeBitblaster::computeRelevantTerms(std::set& termSet) { Assert(options::bitblastMode() == options::BitblastMode::EAGER); for (const auto& var : d_variables) @@ -139,8 +140,8 @@ void BBSimple::computeRelevantTerms(std::set& termSet) } } -bool BBSimple::collectModelValues(TheoryModel* m, - const std::set& relevantTerms) +bool NodeBitblaster::collectModelValues(TheoryModel* m, + const std::set& 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 similarity index 90% rename from src/theory/bv/bitblast/simple_bitblaster.h rename to 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 +class NodeBitblaster : public TBitblaster { using Bits = std::vector; 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 d_bb; + std::unique_ptr 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 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 d_modelCache; /** Bit-blaster used to bit-blast atoms/terms. */ - std::unique_ptr d_bitblaster; + std::unique_ptr d_bitblaster; /** Used for initializing `d_cnfStream`. */ std::unique_ptr 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 { -- 2.30.2