theory/bv/bitblast/eager_bitblaster.h
theory/bv/bitblast/lazy_bitblaster.cpp
theory/bv/bitblast/lazy_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
theory/bv/bv_subtheory_core.h
theory/bv/bv_subtheory_inequality.cpp
theory/bv/bv_subtheory_inequality.h
+ theory/bv/proof_checker.cpp
+ theory/bv/proof_checker.h
theory/bv/slicer.cpp
theory/bv/slicer.h
theory/bv/theory_bv.cpp
case PfRule::ARRAYS_READ_OVER_WRITE_1: return "ARRAYS_READ_OVER_WRITE_1";
case PfRule::ARRAYS_EXT: return "ARRAYS_EXT";
case PfRule::ARRAYS_TRUST: return "ARRAYS_TRUST";
+ //================================================= Bit-Vector rules
+ case PfRule::BV_BITBLAST: return "BV_BITBLAST";
+ case PfRule::BV_EAGER_ATOM: return "BV_EAGER_ATOM";
//================================================= Datatype rules
case PfRule::DT_UNIF: return "DT_UNIF";
case PfRule::DT_INST: return "DT_INST";
// ---------------------
// Conclusion: F
ARRAYS_TRUST,
-
+
+ //================================================= Bit-Vector rules
+ // ======== Bitblast
+ // Children: none
+ // Arguments: (t)
+ // ---------------------
+ // Conclusion: (= t bitblast(t))
+ BV_BITBLAST,
+ // ======== Eager Atom
+ // Children: none
+ // Arguments: (F)
+ // ---------------------
+ // Conclusion: (= F F[0])
+ // where F is of kind BITVECTOR_EAGER_ATOM
+ BV_EAGER_ATOM,
+
//================================================= Datatype rules
// ======== Unification
// Children: (P:(= (C t1 ... tn) (C s1 ... sn)))
--- /dev/null
+/********************* */
+/*! \file simple_bitblaster.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Mathias Preiner
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 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.\endverbatim
+ **
+ ** \brief Bitblaster for simple BV solver.
+ **
+ **/
+#include "theory/bv/bitblast/simple_bitblaster.h"
+
+#include "theory/theory_model.h"
+
+namespace CVC4 {
+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, 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 atom) const
+{
+ return d_bbAtoms.find(atom) != 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);
+}
+
+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;
+}
+
+} // namespace bv
+} // namespace theory
+} // namespace CVC4
--- /dev/null
+/********************* */
+/*! \file simple_bitblaster.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Mathias Preiner
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 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.\endverbatim
+ **
+ ** \brief Bitblaster for simple BV solver.
+ **
+ **/
+#include "cvc4_private.h"
+
+#ifndef CVC4__THEORY__BV__BITBLAST_SIMPLE_BITBLASTER_H
+#define CVC4__THEORY__BV__BITBLAST_SIMPLE_BITBLASTER_H
+
+#include "theory/bv/bitblast/lazy_bitblaster.h"
+
+namespace CVC4 {
+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;
+
+ /** Collect model values for all relevant terms given in 'relevantTerms'. */
+ bool collectModelValues(TheoryModel* m, const std::set<Node>& relevantTerms);
+
+ prop::SatSolver* getSatSolver() override { Unreachable(); }
+
+ 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, NodeHashFunction> d_bbAtoms;
+ /** Theory state. */
+ TheoryState* d_state;
+};
+
+} // namespace bv
+} // namespace theory
+} // namespace CVC4
+
+#endif
#include "theory/bv/bv_solver_simple.h"
-#include "theory/bv/bitblast/lazy_bitblaster.h"
#include "theory/bv/theory_bv.h"
#include "theory/bv/theory_bv_utils.h"
#include "theory/theory_model.h"
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;
-
- /** Collect model values for all relevant terms given in 'relevantTerms'. */
- bool collectModelValues(TheoryModel* m, const std::set<Node>& relevantTerms);
-
- prop::SatSolver* getSatSolver() override { Unreachable(); }
-
- 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, NodeHashFunction> d_bbAtoms;
- /** Theory state. */
- TheoryState& d_state;
-};
-
-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, 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 atom) const
-{
- return d_bbAtoms.find(atom) != 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);
-}
-
-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;
-}
-
/* -------------------------------------------------------------------------- */
namespace {
} // namespace
-BVSolverSimple::BVSolverSimple(TheoryState& s, TheoryInferenceManager& inferMgr)
- : BVSolver(s, inferMgr), d_bitblaster(new BBSimple(s))
+BVSolverSimple::BVSolverSimple(TheoryState* s,
+ TheoryInferenceManager& inferMgr,
+ ProofNodeManager* pnm)
+ : BVSolver(*s, inferMgr),
+ d_bitblaster(new BBSimple(s)),
+ d_epg(pnm ? new EagerProofGenerator(pnm, s->getUserContext(), "")
+ : nullptr)
{
+ if (pnm != nullptr)
+ {
+ d_bvProofChecker.registerTo(pnm->getChecker());
+ }
}
void BVSolverSimple::addBBLemma(TNode fact)
d_bitblaster->bbAtom(fact);
}
NodeManager* nm = NodeManager::currentNM();
- Node atom_bb = Rewriter::rewrite(d_bitblaster->getStoredBBAtom(fact));
+
+ Node atom_bb = d_bitblaster->getStoredBBAtom(fact);
Node lemma = nm->mkNode(kind::EQUAL, fact, atom_bb);
- d_inferManager.lemma(lemma);
+
+ if (d_epg == nullptr)
+ {
+ d_inferManager.lemma(lemma);
+ }
+ else
+ {
+ TrustNode tlem = d_epg->mkTrustNode(lemma, PfRule::BV_BITBLAST, {}, {fact});
+ d_inferManager.trustedLemma(tlem);
+ }
}
bool BVSolverSimple::preNotifyFact(
NodeManager* nm = NodeManager::currentNM();
Node lemma = nm->mkNode(kind::EQUAL, fact, n);
- d_inferManager.lemma(lemma);
+
+ if (d_epg == nullptr)
+ {
+ d_inferManager.lemma(lemma);
+ }
+ else
+ {
+ TrustNode tlem =
+ d_epg->mkTrustNode(lemma, PfRule::BV_EAGER_ATOM, {}, {fact});
+ d_inferManager.trustedLemma(tlem);
+ }
std::unordered_set<Node, NodeHashFunction> bv_atoms;
collectBVAtoms(n, bv_atoms);
#include <unordered_map>
+#include "theory/bv/bitblast/simple_bitblaster.h"
#include "theory/bv/bv_solver.h"
+#include "theory/bv/proof_checker.h"
+#include "theory/eager_proof_generator.h"
namespace CVC4 {
namespace theory {
namespace bv {
-class BBSimple;
-
/**
* Simple bit-blasting solver that sends bit-blasting lemmas directly to the
* internal MiniSat. It is also ablo to handle atoms of kind
class BVSolverSimple : public BVSolver
{
public:
- BVSolverSimple(TheoryState& state, TheoryInferenceManager& inferMgr);
+ BVSolverSimple(TheoryState* state,
+ TheoryInferenceManager& inferMgr,
+ ProofNodeManager* pnm);
~BVSolverSimple() = default;
void preRegisterTerm(TNode n) override {}
/** Bit-blaster used to bit-blast atoms/terms. */
std::unique_ptr<BBSimple> d_bitblaster;
+
+ /** Proof generator that manages proofs for lemmas generated by this class. */
+ std::unique_ptr<EagerProofGenerator> d_epg;
+
+ BVProofRuleChecker d_bvProofChecker;
};
} // namespace bv
--- /dev/null
+/********************* */
+/*! \file proof_checker.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Mathias Preiner
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 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.\endverbatim
+ **
+ ** \brief Implementation of bit-vectors proof checker
+ **/
+
+#include "theory/bv/proof_checker.h"
+
+namespace CVC4 {
+namespace theory {
+namespace bv {
+
+void BVProofRuleChecker::registerTo(ProofChecker* pc)
+{
+ pc->registerChecker(PfRule::BV_BITBLAST, this);
+ pc->registerChecker(PfRule::BV_EAGER_ATOM, this);
+}
+
+Node BVProofRuleChecker::checkInternal(PfRule id,
+ const std::vector<Node>& children,
+ const std::vector<Node>& args)
+{
+ if (id == PfRule::BV_BITBLAST)
+ {
+ BBSimple bb(nullptr);
+ Assert(children.empty());
+ Assert(args.size() == 1);
+ bb.bbAtom(args[0]);
+ Node n = bb.getStoredBBAtom(args[0]);
+ return args[0].eqNode(n);
+ }
+ else if (id == PfRule::BV_EAGER_ATOM)
+ {
+ Assert(children.empty());
+ Assert(args.size() == 1);
+ Assert(args[0].getKind() == kind::BITVECTOR_EAGER_ATOM);
+ return args[0].eqNode(args[0][0]);
+ }
+ // no rule
+ return Node::null();
+}
+
+} // namespace bv
+} // namespace theory
+} // namespace CVC4
--- /dev/null
+/********************* */
+/*! \file proof_checker.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Mathias Preiner
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 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.\endverbatim
+ **
+ ** \brief Bit-Vector proof checker utility
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__THEORY__BV__PROOF_CHECKER_H
+#define CVC4__THEORY__BV__PROOF_CHECKER_H
+
+#include "expr/node.h"
+#include "expr/proof_checker.h"
+#include "expr/proof_node.h"
+#include "theory/bv/bitblast/simple_bitblaster.h"
+
+namespace CVC4 {
+namespace theory {
+namespace bv {
+
+/** The proof checker for bit-vectors. */
+class BVProofRuleChecker : public ProofRuleChecker
+{
+ public:
+ BVProofRuleChecker() = default;
+ ~BVProofRuleChecker() = default;
+
+ /** Register all rules owned by this rule checker into pc. */
+ void registerTo(ProofChecker* pc) override;
+
+ protected:
+ /** Return the conclusion of the given proof step, or null if it is invalid */
+ Node checkInternal(PfRule id,
+ const std::vector<Node>& children,
+ const std::vector<Node>& args) override;
+};
+
+} // namespace bv
+} // namespace theory
+} // namespace CVC4
+
+#endif /* CVC4__THEORY__BV__PROOF_CHECKER_H */
default:
AlwaysAssert(options::bvSolver() == options::BVSolver::SIMPLE);
- d_internal.reset(new BVSolverSimple(d_state, d_inferMgr));
+ d_internal.reset(new BVSolverSimple(&d_state, d_inferMgr, pnm));
}
d_theoryState = &d_state;
d_inferManager = &d_inferMgr;
projects / cvc5.git / commitdiff