From ca4f71c3c3c0da881e0bb9b93dbbb2bb3fe49c46 Mon Sep 17 00:00:00 2001 From: Mathias Preiner Date: Mon, 7 Dec 2020 19:15:14 -0800 Subject: [PATCH] Add support for BV proofs with the simple bitblasting solver. (#5603) --- src/CMakeLists.txt | 4 + src/expr/proof_rule.cpp | 3 + src/expr/proof_rule.h | 17 +- src/theory/bv/bitblast/simple_bitblaster.cpp | 148 +++++++++++++ src/theory/bv/bitblast/simple_bitblaster.h | 77 +++++++ src/theory/bv/bv_solver_simple.cpp | 210 +++---------------- src/theory/bv/bv_solver_simple.h | 14 +- src/theory/bv/proof_checker.cpp | 53 +++++ src/theory/bv/proof_checker.h | 50 +++++ src/theory/bv/theory_bv.cpp | 2 +- 10 files changed, 397 insertions(+), 181 deletions(-) create mode 100644 src/theory/bv/bitblast/simple_bitblaster.cpp create mode 100644 src/theory/bv/bitblast/simple_bitblaster.h create mode 100644 src/theory/bv/proof_checker.cpp create mode 100644 src/theory/bv/proof_checker.h diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 3da032021..4657449f8 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -498,6 +498,8 @@ libcvc4_add_sources( 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 @@ -518,6 +520,8 @@ libcvc4_add_sources( 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 diff --git a/src/expr/proof_rule.cpp b/src/expr/proof_rule.cpp index 885c36131..130eff0f5 100644 --- a/src/expr/proof_rule.cpp +++ b/src/expr/proof_rule.cpp @@ -115,6 +115,9 @@ const char* toString(PfRule id) 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"; diff --git a/src/expr/proof_rule.h b/src/expr/proof_rule.h index f00ef8367..ada10cb9f 100644 --- a/src/expr/proof_rule.h +++ b/src/expr/proof_rule.h @@ -677,7 +677,22 @@ enum class PfRule : uint32_t // --------------------- // 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))) diff --git a/src/theory/bv/bitblast/simple_bitblaster.cpp b/src/theory/bv/bitblast/simple_bitblaster.cpp new file mode 100644 index 000000000..36e115e5e --- /dev/null +++ b/src/theory/bv/bitblast/simple_bitblaster.cpp @@ -0,0 +1,148 @@ +/********************* */ +/*! \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(), 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& 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 diff --git a/src/theory/bv/bitblast/simple_bitblaster.h b/src/theory/bv/bitblast/simple_bitblaster.h new file mode 100644 index 000000000..8a625b5e1 --- /dev/null +++ b/src/theory/bv/bitblast/simple_bitblaster.h @@ -0,0 +1,77 @@ +/********************* */ +/*! \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 +{ + 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; + + /** Collect model values for all relevant terms given in 'relevantTerms'. */ + bool collectModelValues(TheoryModel* m, const std::set& 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 d_bbAtoms; + /** Theory state. */ + TheoryState* d_state; +}; + +} // namespace bv +} // namespace theory +} // namespace CVC4 + +#endif diff --git a/src/theory/bv/bv_solver_simple.cpp b/src/theory/bv/bv_solver_simple.cpp index 153d85df5..98fce24be 100644 --- a/src/theory/bv/bv_solver_simple.cpp +++ b/src/theory/bv/bv_solver_simple.cpp @@ -16,7 +16,6 @@ #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" @@ -25,176 +24,6 @@ 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 -{ - 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; - - /** Collect model values for all relevant terms given in 'relevantTerms'. */ - bool collectModelValues(TheoryModel* m, const std::set& 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 d_bbAtoms; - /** Theory state. */ - TheoryState& d_state; -}; - -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, 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& 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 { @@ -237,9 +66,18 @@ void collectBVAtoms(TNode n, std::unordered_set& atoms) } // 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) @@ -249,9 +87,19 @@ 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( @@ -272,7 +120,17 @@ 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 bv_atoms; collectBVAtoms(n, bv_atoms); diff --git a/src/theory/bv/bv_solver_simple.h b/src/theory/bv/bv_solver_simple.h index d4010cb95..17066e536 100644 --- a/src/theory/bv/bv_solver_simple.h +++ b/src/theory/bv/bv_solver_simple.h @@ -21,15 +21,16 @@ #include +#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 @@ -40,7 +41,9 @@ class BBSimple; class BVSolverSimple : public BVSolver { public: - BVSolverSimple(TheoryState& state, TheoryInferenceManager& inferMgr); + BVSolverSimple(TheoryState* state, + TheoryInferenceManager& inferMgr, + ProofNodeManager* pnm); ~BVSolverSimple() = default; void preRegisterTerm(TNode n) override {} @@ -71,6 +74,11 @@ class BVSolverSimple : public BVSolver /** Bit-blaster used to bit-blast atoms/terms. */ std::unique_ptr d_bitblaster; + + /** Proof generator that manages proofs for lemmas generated by this class. */ + std::unique_ptr d_epg; + + BVProofRuleChecker d_bvProofChecker; }; } // namespace bv diff --git a/src/theory/bv/proof_checker.cpp b/src/theory/bv/proof_checker.cpp new file mode 100644 index 000000000..395930824 --- /dev/null +++ b/src/theory/bv/proof_checker.cpp @@ -0,0 +1,53 @@ +/********************* */ +/*! \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& children, + const std::vector& 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 diff --git a/src/theory/bv/proof_checker.h b/src/theory/bv/proof_checker.h new file mode 100644 index 000000000..1923b50c1 --- /dev/null +++ b/src/theory/bv/proof_checker.h @@ -0,0 +1,50 @@ +/********************* */ +/*! \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& children, + const std::vector& args) override; +}; + +} // namespace bv +} // namespace theory +} // namespace CVC4 + +#endif /* CVC4__THEORY__BV__PROOF_CHECKER_H */ diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index 7285b6768..fd91d0346 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -47,7 +47,7 @@ TheoryBV::TheoryBV(context::Context* c, 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; -- 2.30.2