diff options
Diffstat (limited to 'src/theory/bv/bitblast/proof_bitblaster.cpp')
-rw-r--r-- | src/theory/bv/bitblast/proof_bitblaster.cpp | 31 |
1 files changed, 22 insertions, 9 deletions
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 <unordered_set> -#include "options/proof_options.h" #include "proof/conv_proof_generator.h" #include "theory/theory_model.h" @@ -68,10 +67,23 @@ std::unordered_map<Kind, PfRule, kind::KindHashFunction> {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<TNode> 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 |