From: Mathias Preiner Date: Tue, 13 Jul 2021 02:33:08 +0000 (-0700) Subject: bv: Expand bitblast proof steps in the proof post processor. (#6867) X-Git-Tag: cvc5-1.0.0~1500 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=03087213703b8429ed98a30160df8fea22bc25fb;p=cvc5.git bv: Expand bitblast proof steps in the proof post processor. (#6867) This commit changes BV proof logging to record coarse-grained bit-blast steps during solving and expanding these steps on-demand in the proof post processor. --- diff --git a/src/smt/proof_manager.cpp b/src/smt/proof_manager.cpp index eb5d8e7af..2c04b9e76 100644 --- a/src/smt/proof_manager.cpp +++ b/src/smt/proof_manager.cpp @@ -79,6 +79,7 @@ PfManager::PfManager(context::UserContext* u, SmtEngine* smte) d_pfpp->setEliminateRule(PfRule::THEORY_REWRITE); } } + d_pfpp->setEliminateRule(PfRule::BV_BITBLAST); } d_false = NodeManager::currentNM()->mkConst(false); } diff --git a/src/smt/proof_post_processor.cpp b/src/smt/proof_post_processor.cpp index 6498fa84f..ad9a8f844 100644 --- a/src/smt/proof_post_processor.cpp +++ b/src/smt/proof_post_processor.cpp @@ -23,6 +23,7 @@ #include "smt/smt_engine.h" #include "smt/smt_statistics_registry.h" #include "theory/builtin/proof_checker.h" +#include "theory/bv/bitblast/proof_bitblaster.h" #include "theory/rewriter.h" #include "theory/theory.h" #include "util/rational.h" @@ -1080,6 +1081,16 @@ Node ProofPostprocessCallback::expandMacros(PfRule id, << std::endl; return sumBounds; } + else if (id == PfRule::BV_BITBLAST) + { + bv::BBProof bb(nullptr, d_pnm, true); + Node eq = args[0]; + Assert(eq.getKind() == EQUAL); + bb.bbAtom(eq[0]); + Node bbAtom = bb.getStoredBBAtom(eq[0]); + bb.getProofGenerator()->addProofTo(eq[0].eqNode(bbAtom), cdp); + return eq; + } // TRUST, PREPROCESS, THEORY_LEMMA, THEORY_PREPROCESS? diff --git a/src/theory/bv/bitblast/proof_bitblaster.cpp b/src/theory/bv/bitblast/proof_bitblaster.cpp index a55adaace..ea7ba1a13 100644 --- a/src/theory/bv/bitblast/proof_bitblaster.cpp +++ b/src/theory/bv/bitblast/proof_bitblaster.cpp @@ -16,7 +16,6 @@ #include -#include "options/proof_options.h" #include "proof/conv_proof_generator.h" #include "theory/theory_model.h" @@ -68,10 +67,23 @@ std::unordered_map {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(TheoryState* state, ProofNodeManager* pnm, bool fineGrained) + : d_bb(new BBSimple(state)), + d_pnm(pnm), + 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, + "BBProof::TConvProofGenerator", + nullptr, + false) + : nullptr), + d_recordFineGrainedProofs(fineGrained) { } @@ -83,9 +95,7 @@ void BBProof::bbAtom(TNode node) visit.push_back(node); std::unordered_set visited; - bool fproofs = - options::proofGranularityMode() != options::ProofGranularityMode::OFF; - bool fpenabled = isProofsEnabled() && fproofs; + bool fpenabled = isProofsEnabled() && d_recordFineGrainedProofs; NodeManager* nm = NodeManager::currentNM(); @@ -183,7 +193,8 @@ void BBProof::bbAtom(TNode node) visit.pop_back(); } } - if (isProofsEnabled() && !fproofs) + /* Record coarse-grain bit-blast proof step. */ + if (isProofsEnabled() && !d_recordFineGrainedProofs) { Node node_tobv = getStoredBBAtom(node); d_tcpg->addRewriteStep(node, @@ -210,6 +221,8 @@ bool BBProof::collectModelValues(TheoryModel* m, return d_bb->collectModelValues(m, relevantTerms); } +TConvProofGenerator* BBProof::getProofGenerator() { return d_tcpg.get(); } + bool BBProof::isProofsEnabled() const { return d_pnm != nullptr; } } // namespace bv diff --git a/src/theory/bv/bitblast/proof_bitblaster.h b/src/theory/bv/bitblast/proof_bitblaster.h index ef23c05c0..86cbeae81 100644 --- a/src/theory/bv/bitblast/proof_bitblaster.h +++ b/src/theory/bv/bitblast/proof_bitblaster.h @@ -31,7 +31,7 @@ class BBProof using Bits = std::vector; public: - BBProof(TheoryState* state, ProofNodeManager* pnm, TConvProofGenerator* tcpg); + BBProof(TheoryState* state, ProofNodeManager* pnm, bool fineGrained); ~BBProof(); /** Bit-blast atom 'node'. */ @@ -45,6 +45,8 @@ class BBProof /** Collect model values for all relevant terms given in 'relevantTerms'. */ bool collectModelValues(TheoryModel* m, const std::set& relevantTerms); + TConvProofGenerator* getProofGenerator(); + private: /** Map node kinds to proof rules. */ static std::unordered_map @@ -58,9 +60,11 @@ class BBProof /** The associated proof node manager. */ ProofNodeManager* d_pnm; /** The associated term conversion proof generator. */ - TConvProofGenerator* d_tcpg; + std::unique_ptr d_tcpg; /** Map bit-vector nodes to bit-blasted nodes. */ std::unordered_map d_bbMap; + + bool d_recordFineGrainedProofs; }; } // namespace bv diff --git a/src/theory/bv/bv_solver_simple.cpp b/src/theory/bv/bv_solver_simple.cpp index a16bf7eb8..4216fa087 100644 --- a/src/theory/bv/bv_solver_simple.cpp +++ b/src/theory/bv/bv_solver_simple.cpp @@ -70,20 +70,8 @@ BVSolverSimple::BVSolverSimple(TheoryState* s, TheoryInferenceManager& inferMgr, ProofNodeManager* pnm) : BVSolver(*s, inferMgr), - 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())) + d_pnm(pnm), + d_bitblaster(new BBProof(s, pnm, false)) { } @@ -98,13 +86,14 @@ void BVSolverSimple::addBBLemma(TNode fact) Node atom_bb = d_bitblaster->getStoredBBAtom(fact); Node lemma = nm->mkNode(kind::EQUAL, fact, atom_bb); - if (d_tcpg == nullptr) + if (d_pnm == nullptr) { d_im.lemma(lemma, InferenceId::BV_SIMPLE_BITBLAST_LEMMA); } else { - TrustNode tlem = TrustNode::mkTrustLemma(lemma, d_tcpg.get()); + TrustNode tlem = + TrustNode::mkTrustLemma(lemma, d_bitblaster->getProofGenerator()); d_im.trustedLemma(tlem, InferenceId::BV_SIMPLE_BITBLAST_LEMMA); } } @@ -128,13 +117,14 @@ bool BVSolverSimple::preNotifyFact( NodeManager* nm = NodeManager::currentNM(); Node lemma = nm->mkNode(kind::EQUAL, fact, n); - if (d_tcpg == nullptr) + if (d_pnm == nullptr) { d_im.lemma(lemma, InferenceId::BV_SIMPLE_LEMMA); } else { - TrustNode tlem = TrustNode::mkTrustLemma(lemma, d_tcpg.get()); + TrustNode tlem = + TrustNode::mkTrustLemma(lemma, d_bitblaster->getProofGenerator()); 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 2c23189db..0af4f5b89 100644 --- a/src/theory/bv/bv_solver_simple.h +++ b/src/theory/bv/bv_solver_simple.h @@ -67,8 +67,8 @@ class BVSolverSimple : public BVSolver */ void addBBLemma(TNode fact); - /** Proof generator. */ - std::unique_ptr d_tcpg; + /** Proof node manager. */ + ProofNodeManager* d_pnm; /** Bit-blaster used to bit-blast atoms/terms. */ std::unique_ptr d_bitblaster; /** Proof rule checker */ diff --git a/src/theory/bv/proof_checker.cpp b/src/theory/bv/proof_checker.cpp index 93ba9e67f..711e9798c 100644 --- a/src/theory/bv/proof_checker.cpp +++ b/src/theory/bv/proof_checker.cpp @@ -72,12 +72,10 @@ Node BVProofRuleChecker::checkInternal(PfRule id, { 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); + Assert(args[0].getKind() == kind::EQUAL); + return args[0]; } else if (id == PfRule::BV_BITBLAST_CONST || id == PfRule::BV_BITBLAST_VAR || id == PfRule::BV_BITBLAST_EQUAL || id == PfRule::BV_BITBLAST_ULT