summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/smt/proof_manager.cpp1
-rw-r--r--src/smt/proof_post_processor.cpp11
-rw-r--r--src/theory/bv/bitblast/proof_bitblaster.cpp31
-rw-r--r--src/theory/bv/bitblast/proof_bitblaster.h8
-rw-r--r--src/theory/bv/bv_solver_simple.cpp26
-rw-r--r--src/theory/bv/bv_solver_simple.h4
-rw-r--r--src/theory/bv/proof_checker.cpp6
7 files changed, 52 insertions, 35 deletions
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 <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
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<Node>;
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<Node>& relevantTerms);
+ TConvProofGenerator* getProofGenerator();
+
private:
/** Map node kinds to proof rules. */
static std::unordered_map<Kind, PfRule, kind::KindHashFunction>
@@ -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<TConvProofGenerator> d_tcpg;
/** Map bit-vector nodes to bit-blasted nodes. */
std::unordered_map<Node, Node> 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<TConvProofGenerator> d_tcpg;
+ /** Proof node manager. */
+ ProofNodeManager* d_pnm;
/** Bit-blaster used to bit-blast atoms/terms. */
std::unique_ptr<BBProof> 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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback