diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2021-04-22 18:19:05 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-04-23 01:19:05 +0000 |
commit | 55c2f669abe354ffb258a0da89358f8c5366e2c4 (patch) | |
tree | eb4b0e3e29f17cc24a8d57e12c6756d38ed611ef /src/theory | |
parent | a7fe3cbb024d37b0154a779f01651afa8c0bac0b (diff) |
BV: Add proof logging for bit-blasting. (#6373)
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/bv/bitblast/proof_bitblaster.cpp | 133 | ||||
-rw-r--r-- | src/theory/bv/bitblast/proof_bitblaster.h | 21 | ||||
-rw-r--r-- | src/theory/bv/bv_solver_simple.cpp | 27 | ||||
-rw-r--r-- | src/theory/bv/bv_solver_simple.h | 9 | ||||
-rw-r--r-- | src/theory/bv/kinds | 7 | ||||
-rw-r--r-- | src/theory/bv/proof_checker.cpp | 67 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_type_rules.h | 19 |
7 files changed, 266 insertions, 17 deletions
diff --git a/src/theory/bv/bitblast/proof_bitblaster.cpp b/src/theory/bv/bitblast/proof_bitblaster.cpp index 2f6f099a8..09448da8a 100644 --- a/src/theory/bv/bitblast/proof_bitblaster.cpp +++ b/src/theory/bv/bitblast/proof_bitblaster.cpp @@ -16,19 +16,79 @@ #include <unordered_set> +#include "expr/term_conversion_proof_generator.h" +#include "options/proof_options.h" #include "theory/theory_model.h" namespace cvc5 { namespace theory { namespace bv { -BBProof::BBProof(TheoryState* state) : d_bb(new BBSimple(state)) {} +std::unordered_map<Kind, PfRule, kind::KindHashFunction> + BBProof::s_kindToPfRule = { + {kind::CONST_BITVECTOR, PfRule::BV_BITBLAST_CONST}, + {kind::EQUAL, PfRule::BV_BITBLAST_EQUAL}, + {kind::BITVECTOR_ULT, PfRule::BV_BITBLAST_ULT}, + {kind::BITVECTOR_ULE, PfRule::BV_BITBLAST_ULE}, + {kind::BITVECTOR_UGT, PfRule::BV_BITBLAST_UGT}, + {kind::BITVECTOR_UGE, PfRule::BV_BITBLAST_UGE}, + {kind::BITVECTOR_SLT, PfRule::BV_BITBLAST_SLT}, + {kind::BITVECTOR_SLE, PfRule::BV_BITBLAST_SLE}, + {kind::BITVECTOR_SGT, PfRule::BV_BITBLAST_SGT}, + {kind::BITVECTOR_SGE, PfRule::BV_BITBLAST_SGE}, + {kind::BITVECTOR_NOT, PfRule::BV_BITBLAST_NOT}, + {kind::BITVECTOR_CONCAT, PfRule::BV_BITBLAST_CONCAT}, + {kind::BITVECTOR_AND, PfRule::BV_BITBLAST_AND}, + {kind::BITVECTOR_OR, PfRule::BV_BITBLAST_OR}, + {kind::BITVECTOR_XOR, PfRule::BV_BITBLAST_XOR}, + {kind::BITVECTOR_XNOR, PfRule::BV_BITBLAST_XNOR}, + {kind::BITVECTOR_NAND, PfRule::BV_BITBLAST_NAND}, + {kind::BITVECTOR_NOR, PfRule::BV_BITBLAST_NOR}, + {kind::BITVECTOR_COMP, PfRule::BV_BITBLAST_COMP}, + {kind::BITVECTOR_MULT, PfRule::BV_BITBLAST_MULT}, + {kind::BITVECTOR_PLUS, PfRule::BV_BITBLAST_PLUS}, + {kind::BITVECTOR_SUB, PfRule::BV_BITBLAST_SUB}, + {kind::BITVECTOR_NEG, PfRule::BV_BITBLAST_NEG}, + {kind::BITVECTOR_UDIV, PfRule::BV_BITBLAST_UDIV}, + {kind::BITVECTOR_UREM, PfRule::BV_BITBLAST_UREM}, + {kind::BITVECTOR_SDIV, PfRule::BV_BITBLAST_SDIV}, + {kind::BITVECTOR_SREM, PfRule::BV_BITBLAST_SREM}, + {kind::BITVECTOR_SMOD, PfRule::BV_BITBLAST_SMOD}, + {kind::BITVECTOR_SHL, PfRule::BV_BITBLAST_SHL}, + {kind::BITVECTOR_LSHR, PfRule::BV_BITBLAST_LSHR}, + {kind::BITVECTOR_ASHR, PfRule::BV_BITBLAST_ASHR}, + {kind::BITVECTOR_ULTBV, PfRule::BV_BITBLAST_ULTBV}, + {kind::BITVECTOR_SLTBV, PfRule::BV_BITBLAST_SLTBV}, + {kind::BITVECTOR_ITE, PfRule::BV_BITBLAST_ITE}, + {kind::BITVECTOR_EXTRACT, PfRule::BV_BITBLAST_EXTRACT}, + {kind::BITVECTOR_REPEAT, PfRule::BV_BITBLAST_REPEAT}, + {kind::BITVECTOR_ZERO_EXTEND, PfRule::BV_BITBLAST_ZERO_EXTEND}, + {kind::BITVECTOR_SIGN_EXTEND, PfRule::BV_BITBLAST_SIGN_EXTEND}, + {kind::BITVECTOR_ROTATE_RIGHT, PfRule::BV_BITBLAST_ROTATE_RIGHT}, + {kind::BITVECTOR_ROTATE_LEFT, PfRule::BV_BITBLAST_ROTATE_LEFT}, +}; + +BBProof::BBProof(TheoryState* state, + ProofNodeManager* pnm, + TConvProofGenerator* tcpg) + : d_bb(new BBSimple(state)), d_pnm(pnm), d_tcpg(tcpg) +{ +} + +BBProof::~BBProof() {} void BBProof::bbAtom(TNode node) { std::vector<TNode> visit; visit.push_back(node); std::unordered_set<TNode, TNodeHashFunction> visited; + + bool fproofs = + options::proofGranularityMode() != options::ProofGranularityMode::OFF; + bool fpenabled = isProofsEnabled() && fproofs; + + NodeManager* nm = NodeManager::currentNM(); + while (!visit.empty()) { TNode n = visit.back(); @@ -50,22 +110,89 @@ void BBProof::bbAtom(TNode node) { if (Theory::isLeafOf(n, theory::THEORY_BV) && !n.isConst()) { - // unused for now, will be needed for proof logging Bits bits; d_bb->makeVariable(n, bits); + if (fpenabled) + { + Node n_tobv = nm->mkNode(kind::BITVECTOR_BB_TERM, bits); + d_bbMap.emplace(n, n_tobv); + d_tcpg->addRewriteStep(n, + n_tobv, + PfRule::BV_BITBLAST_VAR, + {}, + {n.eqNode(n_tobv)}, + false); + } } else if (n.getType().isBitVector()) { Bits bits; d_bb->bbTerm(n, bits); + Kind kind = n.getKind(); + if (fpenabled) + { + Node n_tobv = nm->mkNode(kind::BITVECTOR_BB_TERM, bits); + d_bbMap.emplace(n, n_tobv); + Node c_tobv; + if (n.isConst()) + { + c_tobv = n; + } + else + { + std::vector<Node> children_tobv; + if (n.getMetaKind() == kind::metakind::PARAMETERIZED) + { + children_tobv.push_back(n.getOperator()); + } + + for (const auto& child : n) + { + children_tobv.push_back(d_bbMap.at(child)); + } + c_tobv = nm->mkNode(kind, children_tobv); + } + d_tcpg->addRewriteStep(c_tobv, + n_tobv, + s_kindToPfRule.at(kind), + {}, + {c_tobv.eqNode(n_tobv)}, + false); + } } else { d_bb->bbAtom(n); + if (fpenabled) + { + Node n_tobv = getStoredBBAtom(n); + std::vector<Node> children_tobv; + for (const auto& child : n) + { + children_tobv.push_back(d_bbMap.at(child)); + } + Node c_tobv = nm->mkNode(n.getKind(), children_tobv); + d_tcpg->addRewriteStep(c_tobv, + n_tobv, + s_kindToPfRule.at(n.getKind()), + {}, + {c_tobv.eqNode(n_tobv)}, + false); + } } visit.pop_back(); } } + if (isProofsEnabled() && !fproofs) + { + Node node_tobv = getStoredBBAtom(node); + d_tcpg->addRewriteStep(node, + node_tobv, + PfRule::BV_BITBLAST, + {}, + {node.eqNode(node_tobv)}, + false); + } } bool BBProof::hasBBAtom(TNode atom) const { return d_bb->hasBBAtom(atom); } @@ -83,6 +210,8 @@ bool BBProof::collectModelValues(TheoryModel* m, return d_bb->collectModelValues(m, relevantTerms); } +bool BBProof::isProofsEnabled() const { return d_pnm != nullptr; } + } // namespace bv } // namespace theory } // namespace cvc5 diff --git a/src/theory/bv/bitblast/proof_bitblaster.h b/src/theory/bv/bitblast/proof_bitblaster.h index bd5232a76..6cd4960fb 100644 --- a/src/theory/bv/bitblast/proof_bitblaster.h +++ b/src/theory/bv/bitblast/proof_bitblaster.h @@ -20,6 +20,9 @@ #include "theory/bv/bitblast/simple_bitblaster.h" namespace cvc5 { + +class TConvProofGenerator; + namespace theory { namespace bv { @@ -28,8 +31,8 @@ class BBProof using Bits = std::vector<Node>; public: - BBProof(TheoryState* state); - ~BBProof() = default; + BBProof(TheoryState* state, ProofNodeManager* pnm, TConvProofGenerator* tcpg); + ~BBProof(); /** Bit-blast atom 'node'. */ void bbAtom(TNode node); @@ -43,7 +46,21 @@ class BBProof bool collectModelValues(TheoryModel* m, const std::set<Node>& relevantTerms); private: + /** Map node kinds to proof rules. */ + static std::unordered_map<Kind, PfRule, kind::KindHashFunction> + s_kindToPfRule; + + /** Return true if proofs are enabled. */ + bool isProofsEnabled() const; + + /** The associated simple bit-blaster. */ std::unique_ptr<BBSimple> d_bb; + /** The associated proof node manager. */ + ProofNodeManager* d_pnm; + /** The associated term conversion proof generator. */ + TConvProofGenerator* d_tcpg; + /** Map bit-vector nodes to bit-blasted nodes. */ + std::unordered_map<Node, Node, NodeHashFunction> d_bbMap; }; } // namespace bv diff --git a/src/theory/bv/bv_solver_simple.cpp b/src/theory/bv/bv_solver_simple.cpp index b3abd6269..52f5d52ac 100644 --- a/src/theory/bv/bv_solver_simple.cpp +++ b/src/theory/bv/bv_solver_simple.cpp @@ -15,6 +15,7 @@ #include "theory/bv/bv_solver_simple.h" +#include "expr/term_conversion_proof_generator.h" #include "theory/bv/theory_bv.h" #include "theory/bv/theory_bv_utils.h" #include "theory/theory_model.h" @@ -69,9 +70,20 @@ BVSolverSimple::BVSolverSimple(TheoryState* s, TheoryInferenceManager& inferMgr, ProofNodeManager* pnm) : BVSolver(*s, inferMgr), - d_bitblaster(new BBProof(s)), - d_epg(pnm ? new EagerProofGenerator(pnm, s->getUserContext(), "") - : nullptr) + d_tcpg(pnm ? new TConvProofGenerator( + pnm, + nullptr, + /* ONCE to visit each term only once, post-order. FIXPOINT + * could lead to infinite loops due to terms being rewritten + * to terms that contain themselves */ + TConvPolicy::ONCE, + /* STATIC to get the same ProofNode for a shared subterm. */ + TConvCachePolicy::STATIC, + "BVSolverSimple::TConvProofGenerator", + nullptr, + false) + : nullptr), + d_bitblaster(new BBProof(s, pnm, d_tcpg.get())) { } @@ -86,13 +98,13 @@ void BVSolverSimple::addBBLemma(TNode fact) Node atom_bb = d_bitblaster->getStoredBBAtom(fact); Node lemma = nm->mkNode(kind::EQUAL, fact, atom_bb); - if (d_epg == nullptr) + if (d_tcpg == nullptr) { d_im.lemma(lemma, InferenceId::BV_SIMPLE_BITBLAST_LEMMA); } else { - TrustNode tlem = d_epg->mkTrustNode(lemma, PfRule::BV_BITBLAST, {}, {fact}); + TrustNode tlem = TrustNode::mkTrustLemma(lemma, d_tcpg.get()); d_im.trustedLemma(tlem, InferenceId::BV_SIMPLE_BITBLAST_LEMMA); } } @@ -116,14 +128,13 @@ bool BVSolverSimple::preNotifyFact( NodeManager* nm = NodeManager::currentNM(); Node lemma = nm->mkNode(kind::EQUAL, fact, n); - if (d_epg == nullptr) + if (d_tcpg == nullptr) { d_im.lemma(lemma, InferenceId::BV_SIMPLE_LEMMA); } else { - TrustNode tlem = - d_epg->mkTrustNode(lemma, PfRule::BV_EAGER_ATOM, {}, {fact}); + TrustNode tlem = TrustNode::mkTrustLemma(lemma, d_tcpg.get()); d_im.trustedLemma(tlem, InferenceId::BV_SIMPLE_LEMMA); } diff --git a/src/theory/bv/bv_solver_simple.h b/src/theory/bv/bv_solver_simple.h index 6994d755d..106a473d9 100644 --- a/src/theory/bv/bv_solver_simple.h +++ b/src/theory/bv/bv_solver_simple.h @@ -21,9 +21,11 @@ #include "theory/bv/bitblast/proof_bitblaster.h" #include "theory/bv/bv_solver.h" #include "theory/bv/proof_checker.h" -#include "theory/eager_proof_generator.h" namespace cvc5 { + +class TConvProofGenerator; + namespace theory { namespace bv { @@ -71,11 +73,10 @@ class BVSolverSimple : public BVSolver */ void addBBLemma(TNode fact); + /** Proof generator. */ + std::unique_ptr<TConvProofGenerator> d_tcpg; /** Bit-blaster used to bit-blast atoms/terms. */ std::unique_ptr<BBProof> d_bitblaster; - - /** Proof generator that manages proofs for lemmas generated by this class. */ - std::unique_ptr<EagerProofGenerator> d_epg; /** Proof rule checker */ BVProofRuleChecker d_checker; }; diff --git a/src/theory/bv/kinds b/src/theory/bv/kinds index 3a1032bc3..c9999d39b 100644 --- a/src/theory/bv/kinds +++ b/src/theory/bv/kinds @@ -38,6 +38,9 @@ well-founded BITVECTOR_TYPE \ ### non-parameterized operator kinds ------------------------------------------ +## conversion to bit-vector from vector of Booleans kind +operator BITVECTOR_BB_TERM 1: "create bit-vector from vector of Booleans" + ## concatentation kind operator BITVECTOR_CONCAT 2: "concatenation of two or more bit-vectors" @@ -61,7 +64,6 @@ operator BITVECTOR_UREM 2 "unsigned remainder from truncating division of two bi operator BITVECTOR_SDIV 2 "2's complement signed division" operator BITVECTOR_SMOD 2 "2's complement signed remainder (sign follows divisor)" operator BITVECTOR_SREM 2 "2's complement signed remainder (sign follows dividend)" -# total division kinds ## shift kinds operator BITVECTOR_ASHR 2 "bit-vector arithmetic shift right (the two bit-vector parameters must have same width)" @@ -158,6 +160,9 @@ parameterized INT_TO_BITVECTOR INT_TO_BITVECTOR_OP 1 "integer conversion to bit- typerule CONST_BITVECTOR ::cvc5::theory::bv::BitVectorConstantTypeRule +## conversion to bit-vector from vector of Booleans kind +typerule BITVECTOR_BB_TERM ::cvc5::theory::bv::BitVectorToBVTypeRule + ## concatentation kind typerule BITVECTOR_CONCAT ::cvc5::theory::bv::BitVectorConcatTypeRule diff --git a/src/theory/bv/proof_checker.cpp b/src/theory/bv/proof_checker.cpp index 57244d9b4..b8ede6386 100644 --- a/src/theory/bv/proof_checker.cpp +++ b/src/theory/bv/proof_checker.cpp @@ -22,6 +22,47 @@ namespace bv { void BVProofRuleChecker::registerTo(ProofChecker* pc) { pc->registerChecker(PfRule::BV_BITBLAST, this); + pc->registerChecker(PfRule::BV_BITBLAST_CONST, this); + pc->registerChecker(PfRule::BV_BITBLAST_VAR, this); + pc->registerChecker(PfRule::BV_BITBLAST_EQUAL, this); + pc->registerChecker(PfRule::BV_BITBLAST_ULT, this); + pc->registerChecker(PfRule::BV_BITBLAST_ULE, this); + pc->registerChecker(PfRule::BV_BITBLAST_UGT, this); + pc->registerChecker(PfRule::BV_BITBLAST_UGE, this); + pc->registerChecker(PfRule::BV_BITBLAST_SLT, this); + pc->registerChecker(PfRule::BV_BITBLAST_SLE, this); + pc->registerChecker(PfRule::BV_BITBLAST_SGT, this); + pc->registerChecker(PfRule::BV_BITBLAST_SGE, this); + pc->registerChecker(PfRule::BV_BITBLAST_NOT, this); + pc->registerChecker(PfRule::BV_BITBLAST_CONCAT, this); + pc->registerChecker(PfRule::BV_BITBLAST_AND, this); + pc->registerChecker(PfRule::BV_BITBLAST_OR, this); + pc->registerChecker(PfRule::BV_BITBLAST_XOR, this); + pc->registerChecker(PfRule::BV_BITBLAST_XNOR, this); + pc->registerChecker(PfRule::BV_BITBLAST_NAND, this); + pc->registerChecker(PfRule::BV_BITBLAST_NOR, this); + pc->registerChecker(PfRule::BV_BITBLAST_COMP, this); + pc->registerChecker(PfRule::BV_BITBLAST_MULT, this); + pc->registerChecker(PfRule::BV_BITBLAST_PLUS, this); + pc->registerChecker(PfRule::BV_BITBLAST_SUB, this); + pc->registerChecker(PfRule::BV_BITBLAST_NEG, this); + pc->registerChecker(PfRule::BV_BITBLAST_UDIV, this); + pc->registerChecker(PfRule::BV_BITBLAST_UREM, this); + pc->registerChecker(PfRule::BV_BITBLAST_SDIV, this); + pc->registerChecker(PfRule::BV_BITBLAST_SREM, this); + pc->registerChecker(PfRule::BV_BITBLAST_SMOD, this); + pc->registerChecker(PfRule::BV_BITBLAST_SHL, this); + pc->registerChecker(PfRule::BV_BITBLAST_LSHR, this); + pc->registerChecker(PfRule::BV_BITBLAST_ASHR, this); + pc->registerChecker(PfRule::BV_BITBLAST_ULTBV, this); + pc->registerChecker(PfRule::BV_BITBLAST_SLTBV, this); + pc->registerChecker(PfRule::BV_BITBLAST_ITE, this); + pc->registerChecker(PfRule::BV_BITBLAST_EXTRACT, this); + pc->registerChecker(PfRule::BV_BITBLAST_REPEAT, this); + pc->registerChecker(PfRule::BV_BITBLAST_ZERO_EXTEND, this); + pc->registerChecker(PfRule::BV_BITBLAST_SIGN_EXTEND, this); + pc->registerChecker(PfRule::BV_BITBLAST_ROTATE_RIGHT, this); + pc->registerChecker(PfRule::BV_BITBLAST_ROTATE_LEFT, this); pc->registerChecker(PfRule::BV_EAGER_ATOM, this); } @@ -38,6 +79,32 @@ Node BVProofRuleChecker::checkInternal(PfRule id, Node n = bb.getStoredBBAtom(args[0]); return args[0].eqNode(n); } + else if (id == PfRule::BV_BITBLAST_CONST || id == PfRule::BV_BITBLAST_VAR + || id == PfRule::BV_BITBLAST_EQUAL || id == PfRule::BV_BITBLAST_ULT + || id == PfRule::BV_BITBLAST_ULE || id == PfRule::BV_BITBLAST_UGT + || id == PfRule::BV_BITBLAST_UGE || id == PfRule::BV_BITBLAST_SLT + || id == PfRule::BV_BITBLAST_SLE || id == PfRule::BV_BITBLAST_SGT + || id == PfRule::BV_BITBLAST_SGE || id == PfRule::BV_BITBLAST_NOT + || id == PfRule::BV_BITBLAST_CONCAT || id == PfRule::BV_BITBLAST_AND + || id == PfRule::BV_BITBLAST_OR || id == PfRule::BV_BITBLAST_XOR + || id == PfRule::BV_BITBLAST_XNOR || id == PfRule::BV_BITBLAST_NAND + || id == PfRule::BV_BITBLAST_NOR || id == PfRule::BV_BITBLAST_COMP + || id == PfRule::BV_BITBLAST_MULT || id == PfRule::BV_BITBLAST_PLUS + || id == PfRule::BV_BITBLAST_SUB || id == PfRule::BV_BITBLAST_NEG + || id == PfRule::BV_BITBLAST_UDIV || id == PfRule::BV_BITBLAST_UREM + || id == PfRule::BV_BITBLAST_SDIV || id == PfRule::BV_BITBLAST_SREM + || id == PfRule::BV_BITBLAST_SMOD || id == PfRule::BV_BITBLAST_SHL + || id == PfRule::BV_BITBLAST_LSHR || id == PfRule::BV_BITBLAST_ASHR + || id == PfRule::BV_BITBLAST_ULTBV || id == PfRule::BV_BITBLAST_SLTBV + || id == PfRule::BV_BITBLAST_ITE || id == PfRule::BV_BITBLAST_EXTRACT + || id == PfRule::BV_BITBLAST_REPEAT + || id == PfRule::BV_BITBLAST_ZERO_EXTEND + || id == PfRule::BV_BITBLAST_SIGN_EXTEND + || id == PfRule::BV_BITBLAST_ROTATE_RIGHT + || id == PfRule::BV_BITBLAST_ROTATE_LEFT) + { + return args[0]; + } else if (id == PfRule::BV_EAGER_ATOM) { Assert(children.empty()); diff --git a/src/theory/bv/theory_bv_type_rules.h b/src/theory/bv/theory_bv_type_rules.h index 6594e9fa7..763617d25 100644 --- a/src/theory/bv/theory_bv_type_rules.h +++ b/src/theory/bv/theory_bv_type_rules.h @@ -81,6 +81,25 @@ class BitVectorConcatTypeRule static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); }; +class BitVectorToBVTypeRule +{ + public: + inline static TypeNode computeType(NodeManager* nodeManager, + TNode n, + bool check) + { + for (const auto& child : n) + { + TypeNode t = child.getType(check); + if (!t.isBoolean()) + { + throw TypeCheckingExceptionPrivate(n, "expecting Boolean terms"); + } + } + return nodeManager->mkBitVectorType(n.getNumChildren()); + } +}; + class BitVectorITETypeRule { public: |