diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-07-14 16:15:28 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-07-14 21:15:28 +0000 |
commit | 54eac4f9781d9c07446453697128c4bd036c110d (patch) | |
tree | fd9323eb448cd2d45f4d49df72daf09aacb68d96 /src | |
parent | a7d01e2f8f0e2ff5d2af30aa6b97e5e16758997e (diff) |
Fix for context on input proof generator (#6873)
The preprocess proof generator uses a dummy CDProof to mark input assertions that do not need justification. This CDProof should be user-context dependent to avoid rare cases where an input assertion was the symmetric equality of another, it was previously context independent.
This also refactors the debugging traces in this class.
Diffstat (limited to 'src')
-rw-r--r-- | src/smt/preprocess_proof_generator.cpp | 37 |
1 files changed, 25 insertions, 12 deletions
diff --git a/src/smt/preprocess_proof_generator.cpp b/src/smt/preprocess_proof_generator.cpp index 12a802f14..5511800a1 100644 --- a/src/smt/preprocess_proof_generator.cpp +++ b/src/smt/preprocess_proof_generator.cpp @@ -36,7 +36,7 @@ PreprocessProofGenerator::PreprocessProofGenerator(ProofNodeManager* pnm, d_ctx(c ? c : &d_context), d_src(d_ctx), d_helperProofs(pnm, d_ctx), - d_inputPf(pnm, nullptr), + d_inputPf(pnm, c, "InputProof"), d_name(name), d_ra(ra), d_rpp(rpp) @@ -50,12 +50,18 @@ void PreprocessProofGenerator::notifyInput(Node n) void PreprocessProofGenerator::notifyNewAssert(Node n, ProofGenerator* pg) { + if (n.isConst() && n.getConst<bool>()) + { + // ignore true assertions + return; + } Trace("smt-proof-pp-debug") - << "PreprocessProofGenerator::notifyNewAssert: " << n << std::endl; + << "PreprocessProofGenerator::notifyNewAssert: " << identify() << " " << n + << " from " << (pg == nullptr ? "null" : pg->identify()) << std::endl; if (d_src.find(n) == d_src.end()) { // if no proof generator provided for (non-true) assertion - if (pg == nullptr && (!n.isConst() || !n.getConst<bool>())) + if (pg == nullptr) { checkEagerPedantic(d_ra); } @@ -95,8 +101,7 @@ void PreprocessProofGenerator::notifyTrustedPreprocessed(TrustNode tnp) Assert(tnp.getKind() == TrustNodeKind::REWRITE); Node np = tnp.getNode(); Trace("smt-proof-pp-debug") - << "PreprocessProofGenerator::notifyPreprocessed: " << tnp.getProven() - << std::endl; + << "PreprocessProofGenerator::notifyPreprocessed: " << tnp << std::endl; if (d_src.find(np) == d_src.end()) { if (tnp.getGenerator() == nullptr) @@ -113,17 +118,19 @@ void PreprocessProofGenerator::notifyTrustedPreprocessed(TrustNode tnp) std::shared_ptr<ProofNode> PreprocessProofGenerator::getProofFor(Node f) { + Trace("smt-pppg") << "PreprocessProofGenerator::getProofFor: (" << d_name + << ") input " << f << std::endl; NodeTrustNodeMap::iterator it = d_src.find(f); if (it == d_src.end()) { + Trace("smt-pppg") << "...no proof for " << identify() << " " << f + << std::endl; // could be an assumption, return nullptr return nullptr; } // make CDProof to construct the proof below CDProof cdp(d_pnm); - Trace("smt-pppg") << "PreprocessProofGenerator::getProofFor: (" << d_name - << ") input " << f << std::endl; Node curr = f; std::vector<Node> transChildren; std::unordered_set<Node> processed; @@ -150,27 +157,30 @@ std::shared_ptr<ProofNode> PreprocessProofGenerator::getProofFor(Node f) bool proofStepProcessed = false; // if a generator for the step was provided, it is stored in the proof - Trace("smt-pppg") << "...get provided proof" << std::endl; + Trace("smt-pppg-debug") + << "...get provided proof " << (*it).second << std::endl; std::shared_ptr<ProofNode> pfr = (*it).second.toProofNode(); if (pfr != nullptr) { - Trace("smt-pppg") << "...add provided" << std::endl; + Trace("smt-pppg-debug") << "...add provided " << *pfr << std::endl; Assert(pfr->getResult() == proven); cdp.addProof(pfr); proofStepProcessed = true; } - Trace("smt-pppg") << "...update" << std::endl; + Trace("smt-pppg-debug") << "...update" << std::endl; TrustNodeKind tnk = (*it).second.getKind(); if (tnk == TrustNodeKind::REWRITE) { - Trace("smt-pppg") << "...rewritten from " << proven[0] << std::endl; + Trace("smt-pppg-debug") + << "...rewritten from " << proven[0] << std::endl; Assert(proven.getKind() == kind::EQUAL); if (!proofStepProcessed) { // maybe its just a simple rewrite? if (proven[1] == theory::Rewriter::rewrite(proven[0])) { + Trace("smt-pppg-debug") << "...add simple rewrite" << std::endl; cdp.addStep(proven, PfRule::REWRITE, {}, {proven[0]}); proofStepProcessed = true; } @@ -180,6 +190,7 @@ std::shared_ptr<ProofNode> PreprocessProofGenerator::getProofFor(Node f) curr = proven[0]; success = true; // find the next node + Trace("smt-pppg") << "...continue " << curr << std::endl; it = d_src.find(curr); } else @@ -190,7 +201,9 @@ std::shared_ptr<ProofNode> PreprocessProofGenerator::getProofFor(Node f) if (!proofStepProcessed) { - Trace("smt-pppg") << "...add missing step" << std::endl; + Trace("smt-pppg-debug") + << "...justify missing step with " + << (tnk == TrustNodeKind::LEMMA ? d_ra : d_rpp) << std::endl; // add trusted step, the rule depends on the kind of trust node cdp.addStep( proven, tnk == TrustNodeKind::LEMMA ? d_ra : d_rpp, {}, {proven}); |