From: Mathias Preiner Date: Thu, 15 Jul 2021 02:19:12 +0000 (-0700) Subject: bv: Rename BBSimple to NodeBitblaster. (#6891) X-Git-Tag: cvc5-1.0.0~1483 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d7bb2484436a55c6b2df08bcae7549809e3ad264;p=cvc5.git bv: Rename BBSimple to NodeBitblaster. (#6891) --- 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/node_bitblaster.cpp b/src/theory/bv/bitblast/node_bitblaster.cpp new file mode 100644 index 000000000..fcfa05615 --- /dev/null +++ b/src/theory/bv/bitblast/node_bitblaster.cpp @@ -0,0 +1,170 @@ +/****************************************************************************** + * Top contributors (to current version): + * Mathias Preiner + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Bitblaster used to bitblast to Boolean Nodes. + */ +#include "theory/bv/bitblast/node_bitblaster.h" + +#include "options/bv_options.h" +#include "theory/theory_model.h" +#include "theory/theory_state.h" + +namespace cvc5 { +namespace theory { +namespace bv { + +NodeBitblaster::NodeBitblaster(TheoryState* s) : TBitblaster(), d_state(s) +{ +} + +void NodeBitblaster::bbAtom(TNode node) +{ + node = node.getKind() == kind::NOT ? node[0] : node; + + if (hasBBAtom(node)) + { + return; + } + + Node normalized = Rewriter::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)); +} + +void NodeBitblaster::storeBBAtom(TNode atom, Node atom_bb) +{ + d_bbAtoms.emplace(atom, atom_bb); +} + +void NodeBitblaster::storeBBTerm(TNode node, const Bits& bits) +{ + d_termCache.emplace(node, bits); +} + +bool NodeBitblaster::hasBBAtom(TNode lit) const +{ + if (lit.getKind() == kind::NOT) + { + lit = lit[0]; + } + return d_bbAtoms.find(lit) != d_bbAtoms.end(); +} + +void NodeBitblaster::makeVariable(TNode var, Bits& bits) +{ + Assert(bits.size() == 0); + for (unsigned i = 0; i < utils::getSize(var); ++i) + { + bits.push_back(utils::mkBitOf(var, i)); + } + d_variables.insert(var); +} + +Node NodeBitblaster::getBBAtom(TNode node) const { return node; } + +void NodeBitblaster::bbTerm(TNode node, Bits& bits) +{ + Assert(node.getType().isBitVector()); + if (hasBBTerm(node)) + { + getBBTerm(node, bits); + return; + } + d_termBBStrategies[node.getKind()](node, bits, this); + Assert(bits.size() == utils::getSize(node)); + storeBBTerm(node, bits); +} + +Node NodeBitblaster::getStoredBBAtom(TNode node) +{ + bool negated = false; + if (node.getKind() == kind::NOT) + { + node = node[0]; + negated = true; + } + + Assert(hasBBAtom(node)); + Node atom_bb = d_bbAtoms.at(node); + return negated ? atom_bb.negate() : atom_bb; +} + +Node NodeBitblaster::getModelFromSatSolver(TNode a, bool fullModel) +{ + if (!hasBBTerm(a)) + { + return utils::mkConst(utils::getSize(a), 0u); + } + + bool assignment; + Bits bits; + getBBTerm(a, bits); + Integer value(0); + Integer one(1), zero(0); + for (int i = bits.size() - 1; i >= 0; --i) + { + Integer bit; + if (d_state->hasSatValue(bits[i], assignment)) + { + bit = assignment ? one : zero; + } + else + { + bit = zero; + } + value = value * 2 + bit; + } + return utils::mkConst(bits.size(), value); +} + +void NodeBitblaster::computeRelevantTerms(std::set& termSet) +{ + Assert(options::bitblastMode() == options::BitblastMode::EAGER); + for (const auto& var : d_variables) + { + termSet.insert(var); + } +} + +bool NodeBitblaster::collectModelValues(TheoryModel* m, + const std::set& relevantTerms) +{ + for (const auto& var : relevantTerms) + { + if (d_variables.find(var) == d_variables.end()) continue; + + Node const_value = getModelFromSatSolver(var, true); + Assert(const_value.isNull() || const_value.isConst()); + if (!const_value.isNull()) + { + if (!m->assertEquality(var, const_value, true)) + { + return false; + } + } + } + return true; +} + +bool NodeBitblaster::isVariable(TNode node) +{ + return d_variables.find(node) != d_variables.end(); +} + +} // namespace bv +} // namespace theory +} // namespace cvc5 diff --git a/src/theory/bv/bitblast/node_bitblaster.h b/src/theory/bv/bitblast/node_bitblaster.h new file mode 100644 index 000000000..9b3bdda07 --- /dev/null +++ b/src/theory/bv/bitblast/node_bitblaster.h @@ -0,0 +1,82 @@ +/****************************************************************************** + * Top contributors (to current version): + * Mathias Preiner + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Bitblaster used to bitblast to Boolean Nodes. + */ +#include "cvc5_private.h" + +#ifndef CVC5__THEORY__BV__BITBLAST_NODE_BITBLASTER_H +#define CVC5__THEORY__BV__BITBLAST_NODE_BITBLASTER_H + +#include "theory/bv/bitblast/bitblaster.h" + +namespace cvc5 { +namespace theory { +namespace bv { + +/** + * Implementation of a simple Node-based bit-blaster. + * + * Implements the bare minimum to bit-blast bit-vector atoms/terms. + */ +class NodeBitblaster : public TBitblaster +{ + using Bits = std::vector; + + public: + NodeBitblaster(TheoryState* state); + ~NodeBitblaster() = default; + + /** Bit-blast term 'node' and return bit-blasted 'bits'. */ + void bbTerm(TNode node, Bits& bits) override; + /** Bit-blast atom 'node'. */ + void bbAtom(TNode node) override; + /** Get bit-blasted atom, returns 'atom' itself since it's Boolean. */ + Node getBBAtom(TNode atom) const override; + /** Store Boolean node representing the bit-blasted atom. */ + void storeBBAtom(TNode atom, Node atom_bb) override; + /** Store bits of bit-blasted term. */ + void storeBBTerm(TNode node, const Bits& bits) override; + /** Check if atom was already bit-blasted. */ + bool hasBBAtom(TNode atom) const override; + /** Get bit-blasted node stored for atom. */ + Node getStoredBBAtom(TNode node); + /** Create 'bits' for variable 'var'. */ + void makeVariable(TNode var, Bits& bits) override; + + /** Add d_variables to termSet. */ + void computeRelevantTerms(std::set& termSet); + /** Collect model values for all relevant terms given in 'relevantTerms'. */ + bool collectModelValues(TheoryModel* m, const std::set& relevantTerms); + + prop::SatSolver* getSatSolver() override { Unreachable(); } + + /** Checks whether node is a variable introduced via `makeVariable`.*/ + bool isVariable(TNode node); + + private: + /** Query SAT solver for assignment of node 'a'. */ + Node getModelFromSatSolver(TNode a, bool fullModel) override; + + /** Caches variables for which we already created bits. */ + TNodeSet d_variables; + /** Stores bit-blasted atoms. */ + std::unordered_map d_bbAtoms; + /** Theory state. */ + TheoryState* d_state; +}; + +} // namespace bv +} // namespace theory +} // namespace cvc5 + +#endif 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/bitblast/simple_bitblaster.cpp b/src/theory/bv/bitblast/simple_bitblaster.cpp deleted file mode 100644 index 357a54b1a..000000000 --- a/src/theory/bv/bitblast/simple_bitblaster.cpp +++ /dev/null @@ -1,169 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Mathias Preiner - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - * in the top-level source directory and their institutional affiliations. - * All rights reserved. See the file COPYING in the top-level source - * directory for licensing information. - * **************************************************************************** - * - * Bitblaster for simple BV solver. - * - */ -#include "theory/bv/bitblast/simple_bitblaster.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) {} - -void BBSimple::bbAtom(TNode node) -{ - node = node.getKind() == kind::NOT ? node[0] : node; - - if (hasBBAtom(node)) - { - return; - } - - Node normalized = Rewriter::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)); -} - -void BBSimple::storeBBAtom(TNode atom, Node atom_bb) -{ - d_bbAtoms.emplace(atom, atom_bb); -} - -void BBSimple::storeBBTerm(TNode node, const Bits& bits) -{ - d_termCache.emplace(node, bits); -} - -bool BBSimple::hasBBAtom(TNode lit) const -{ - if (lit.getKind() == kind::NOT) - { - lit = lit[0]; - } - return d_bbAtoms.find(lit) != d_bbAtoms.end(); -} - -void BBSimple::makeVariable(TNode var, Bits& bits) -{ - Assert(bits.size() == 0); - for (unsigned i = 0; i < utils::getSize(var); ++i) - { - bits.push_back(utils::mkBitOf(var, i)); - } - d_variables.insert(var); -} - -Node BBSimple::getBBAtom(TNode node) const { return node; } - -void BBSimple::bbTerm(TNode node, Bits& bits) -{ - Assert(node.getType().isBitVector()); - if (hasBBTerm(node)) - { - getBBTerm(node, bits); - return; - } - d_termBBStrategies[node.getKind()](node, bits, this); - Assert(bits.size() == utils::getSize(node)); - storeBBTerm(node, bits); -} - -Node BBSimple::getStoredBBAtom(TNode node) -{ - bool negated = false; - if (node.getKind() == kind::NOT) - { - node = node[0]; - negated = true; - } - - Assert(hasBBAtom(node)); - Node atom_bb = d_bbAtoms.at(node); - return negated ? atom_bb.negate() : atom_bb; -} - -Node BBSimple::getModelFromSatSolver(TNode a, bool fullModel) -{ - if (!hasBBTerm(a)) - { - return utils::mkConst(utils::getSize(a), 0u); - } - - bool assignment; - Bits bits; - getBBTerm(a, bits); - Integer value(0); - Integer one(1), zero(0); - for (int i = bits.size() - 1; i >= 0; --i) - { - Integer bit; - if (d_state->hasSatValue(bits[i], assignment)) - { - bit = assignment ? one : zero; - } - else - { - bit = zero; - } - value = value * 2 + bit; - } - return utils::mkConst(bits.size(), value); -} - -void BBSimple::computeRelevantTerms(std::set& termSet) -{ - Assert(options::bitblastMode() == options::BitblastMode::EAGER); - for (const auto& var : d_variables) - { - termSet.insert(var); - } -} - -bool BBSimple::collectModelValues(TheoryModel* m, - const std::set& relevantTerms) -{ - for (const auto& var : relevantTerms) - { - if (d_variables.find(var) == d_variables.end()) continue; - - Node const_value = getModelFromSatSolver(var, true); - Assert(const_value.isNull() || const_value.isConst()); - if (!const_value.isNull()) - { - if (!m->assertEquality(var, const_value, true)) - { - return false; - } - } - } - return true; -} - -bool BBSimple::isVariable(TNode node) -{ - return d_variables.find(node) != d_variables.end(); -} - -} // namespace bv -} // namespace theory -} // namespace cvc5 diff --git a/src/theory/bv/bitblast/simple_bitblaster.h b/src/theory/bv/bitblast/simple_bitblaster.h deleted file mode 100644 index ec0899145..000000000 --- a/src/theory/bv/bitblast/simple_bitblaster.h +++ /dev/null @@ -1,82 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Mathias Preiner - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - * in the top-level source directory and their institutional affiliations. - * All rights reserved. See the file COPYING in the top-level source - * directory for licensing information. - * **************************************************************************** - * - * Bitblaster for simple BV solver. - */ -#include "cvc5_private.h" - -#ifndef CVC5__THEORY__BV__BITBLAST_SIMPLE_BITBLASTER_H -#define CVC5__THEORY__BV__BITBLAST_SIMPLE_BITBLASTER_H - -#include "theory/bv/bitblast/bitblaster.h" - -namespace cvc5 { -namespace theory { -namespace bv { - -/** - * Implementation of a simple Node-based bit-blaster. - * - * Implements the bare minimum to bit-blast bit-vector atoms/terms. - */ -class BBSimple : public TBitblaster -{ - using Bits = std::vector; - - public: - BBSimple(TheoryState* state); - ~BBSimple() = default; - - /** Bit-blast term 'node' and return bit-blasted 'bits'. */ - void bbTerm(TNode node, Bits& bits) override; - /** Bit-blast atom 'node'. */ - void bbAtom(TNode node) override; - /** Get bit-blasted atom, returns 'atom' itself since it's Boolean. */ - Node getBBAtom(TNode atom) const override; - /** Store Boolean node representing the bit-blasted atom. */ - void storeBBAtom(TNode atom, Node atom_bb) override; - /** Store bits of bit-blasted term. */ - void storeBBTerm(TNode node, const Bits& bits) override; - /** Check if atom was already bit-blasted. */ - bool hasBBAtom(TNode atom) const override; - /** Get bit-blasted node stored for atom. */ - Node getStoredBBAtom(TNode node); - /** Create 'bits' for variable 'var'. */ - void makeVariable(TNode var, Bits& bits) override; - - /** Add d_variables to termSet. */ - void computeRelevantTerms(std::set& termSet); - /** Collect model values for all relevant terms given in 'relevantTerms'. */ - bool collectModelValues(TheoryModel* m, const std::set& relevantTerms); - - prop::SatSolver* getSatSolver() override { Unreachable(); } - - /** Checks whether node is a variable introduced via `makeVariable`.*/ - bool isVariable(TNode node); - - private: - /** Query SAT solver for assignment of node 'a'. */ - Node getModelFromSatSolver(TNode a, bool fullModel) override; - - /** Caches variables for which we already created bits. */ - TNodeSet d_variables; - /** Stores bit-blasted atoms. */ - std::unordered_map d_bbAtoms; - /** Theory state. */ - TheoryState* d_state; -}; - -} // namespace bv -} // namespace theory -} // namespace cvc5 - -#endif 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 {