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
--- /dev/null
+/******************************************************************************
+ * 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<Node>(), 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<Node>& termSet)
+{
+ Assert(options::bitblastMode() == options::BitblastMode::EAGER);
+ for (const auto& var : d_variables)
+ {
+ termSet.insert(var);
+ }
+}
+
+bool NodeBitblaster::collectModelValues(TheoryModel* m,
+ const std::set<Node>& 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
--- /dev/null
+/******************************************************************************
+ * 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<Node>
+{
+ using Bits = std::vector<Node>;
+
+ 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<Node>& termSet);
+ /** Collect model values for all relevant terms given in 'relevantTerms'. */
+ bool collectModelValues(TheoryModel* m, const std::set<Node>& 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<Node, Node> d_bbAtoms;
+ /** Theory state. */
+ TheoryState* d_state;
+};
+
+} // namespace bv
+} // namespace theory
+} // namespace cvc5
+
+#endif
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(
* 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"
#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 {
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. */
+++ /dev/null
-/******************************************************************************
- * 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<Node>(), 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<Node>& termSet)
-{
- Assert(options::bitblastMode() == options::BitblastMode::EAGER);
- for (const auto& var : d_variables)
- {
- termSet.insert(var);
- }
-}
-
-bool BBSimple::collectModelValues(TheoryModel* m,
- const std::set<Node>& 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
+++ /dev/null
-/******************************************************************************
- * 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<Node>
-{
- using Bits = std::vector<Node>;
-
- 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<Node>& termSet);
- /** Collect model values for all relevant terms given in 'relevantTerms'. */
- bool collectModelValues(TheoryModel* m, const std::set<Node>& 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<Node, Node> d_bbAtoms;
- /** Theory state. */
- TheoryState* d_state;
-};
-
-} // namespace bv
-} // namespace theory
-} // namespace cvc5
-
-#endif
class BBRegistrar : public prop::Registrar
{
public:
- BBRegistrar(BBSimple* bb) : d_bitblaster(bb) {}
+ BBRegistrar(NodeBitblaster* bb) : d_bitblaster(bb) {}
void preRegister(Node n) override
{
private:
/** The bitblaster used. */
- BBSimple* d_bitblaster;
+ NodeBitblaster* d_bitblaster;
/** Stores bit-vector atoms encounterd on preRegister(). */
std::unordered_set<TNode> d_registeredAtoms;
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()),
#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"
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;
#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 {
projects / cvc5.git / commitdiff