diff options
Diffstat (limited to 'src/smt/preprocess_proof_generator.cpp')
| -rw-r--r-- | src/smt/preprocess_proof_generator.cpp | 117 |
1 files changed, 89 insertions, 28 deletions
diff --git a/src/smt/preprocess_proof_generator.cpp b/src/smt/preprocess_proof_generator.cpp index 5c7ed0356..1739a4e7d 100644 --- a/src/smt/preprocess_proof_generator.cpp +++ b/src/smt/preprocess_proof_generator.cpp @@ -21,15 +21,24 @@ namespace CVC4 { namespace smt { -PreprocessProofGenerator::PreprocessProofGenerator(ProofNodeManager* pnm) - : d_pnm(pnm) +PreprocessProofGenerator::PreprocessProofGenerator(context::UserContext* u, + ProofNodeManager* pnm) + : d_pnm(pnm), d_src(u), d_helperProofs(u) { } void PreprocessProofGenerator::notifyNewAssert(Node n, ProofGenerator* pg) { - Trace("smt-proof-pp-debug") << "- notifyNewAssert: " << n << std::endl; - d_src[n] = theory::TrustNode::mkTrustLemma(n, pg); + Trace("smt-proof-pp-debug") + << "PreprocessProofGenerator::notifyNewAssert: " << n << std::endl; + if (d_src.find(n) == d_src.end()) + { + d_src[n] = theory::TrustNode::mkTrustLemma(n, pg); + } + else + { + Trace("smt-proof-pp-debug") << "...already proven" << std::endl; + } } void PreprocessProofGenerator::notifyPreprocessed(Node n, @@ -40,14 +49,22 @@ void PreprocessProofGenerator::notifyPreprocessed(Node n, if (n != np) { Trace("smt-proof-pp-debug") - << "- notifyPreprocessed: " << n << "..." << np << std::endl; - d_src[np] = theory::TrustNode::mkTrustRewrite(n, np, pg); + << "PreprocessProofGenerator::notifyPreprocessed: " << n << "..." << np + << std::endl; + if (d_src.find(np) == d_src.end()) + { + d_src[np] = theory::TrustNode::mkTrustRewrite(n, np, pg); + } + else + { + Trace("smt-proof-pp-debug") << "...already proven" << std::endl; + } } } std::shared_ptr<ProofNode> PreprocessProofGenerator::getProofFor(Node f) { - std::map<Node, theory::TrustNode>::iterator it = d_src.find(f); + NodeTrustNodeMap::iterator it = d_src.find(f); if (it == d_src.end()) { // could be an assumption, return nullptr @@ -56,67 +73,102 @@ std::shared_ptr<ProofNode> PreprocessProofGenerator::getProofFor(Node f) // make CDProof to construct the proof below CDProof cdp(d_pnm); + Trace("smt-pppg") << "PreprocessProofGenerator::getProofFor: input " << f + << std::endl; Node curr = f; std::vector<Node> transChildren; + std::unordered_set<Node, NodeHashFunction> processed; bool success; + // we connect the proof of f to its source via the map d_src until we + // discover that its source is a preprocessing lemma (a lemma stored in d_src) + // or otherwise it is assumed to be an input assumption. do { success = false; if (it != d_src.end()) { - Assert(it->second.getNode() == curr); + Assert((*it).second.getNode() == curr); + // get the proven node + Node proven = (*it).second.getProven(); + Assert(!proven.isNull()); + Trace("smt-pppg") << "...process proven " << proven << std::endl; + if (processed.find(proven) != processed.end()) + { + Unhandled() << "Cyclic steps in preprocess proof generator"; + continue; + } + processed.insert(proven); bool proofStepProcessed = false; - std::shared_ptr<ProofNode> pfr = it->second.toProofNode(); + + // if a generator for the step was provided, it is stored in the proof + Trace("smt-pppg") << "...get provided proof" << std::endl; + std::shared_ptr<ProofNode> pfr = (*it).second.toProofNode(); if (pfr != nullptr) { - Assert(pfr->getResult() == it->second.getProven()); + Trace("smt-pppg") << "...add provided" << std::endl; + Assert(pfr->getResult() == proven); cdp.addProof(pfr); proofStepProcessed = true; } - if (it->second.getKind() == theory::TrustNodeKind::REWRITE) + Trace("smt-pppg") << "...update" << std::endl; + theory::TrustNodeKind tnk = (*it).second.getKind(); + if (tnk == theory::TrustNodeKind::REWRITE) { - Node eq = it->second.getProven(); - Assert(eq.getKind() == kind::EQUAL); + Trace("smt-pppg") << "...rewritten from " << proven[0] << std::endl; + Assert(proven.getKind() == kind::EQUAL); if (!proofStepProcessed) { // maybe its just a simple rewrite? - if (eq[1] == theory::Rewriter::rewrite(eq[0])) + if (proven[1] == theory::Rewriter::rewrite(proven[0])) { - cdp.addStep(eq, PfRule::REWRITE, {}, {eq[0]}); + cdp.addStep(proven, PfRule::REWRITE, {}, {proven[0]}); proofStepProcessed = true; } } - transChildren.push_back(eq); + transChildren.push_back(proven); // continue with source - curr = eq[0]; + curr = proven[0]; success = true; // find the next node it = d_src.find(curr); } else { - Assert(it->second.getKind() == theory::TrustNodeKind::LEMMA); + Trace("smt-pppg") << "...lemma" << std::endl; + Assert(tnk == theory::TrustNodeKind::LEMMA); } if (!proofStepProcessed) { - // add trusted step - Node proven = it->second.getProven(); - cdp.addStep(proven, PfRule::PREPROCESS, {}, {proven}); + Trace("smt-pppg") << "...add missing step" << std::endl; + // add trusted step, the rule depends on the kind of trust node + cdp.addStep(proven, + tnk == theory::TrustNodeKind::LEMMA + ? PfRule::PREPROCESS_LEMMA + : PfRule::PREPROCESS, + {}, + {proven}); } } } while (success); - Assert(curr != f); - // prove ( curr == f ) - Node fullRewrite = curr.eqNode(f); - if (transChildren.size() >= 2) + // prove ( curr == f ), which is not necessary if they are the same + // modulo symmetry. + if (!CDProof::isSame(f, curr)) { - cdp.addStep(fullRewrite, PfRule::TRANS, transChildren, {}); + Node fullRewrite = curr.eqNode(f); + if (transChildren.size() >= 2) + { + Trace("smt-pppg") << "...apply trans to get " << fullRewrite << std::endl; + std::reverse(transChildren.begin(), transChildren.end()); + cdp.addStep(fullRewrite, PfRule::TRANS, transChildren, {}); + } + Trace("smt-pppg") << "...eq_resolve to prove" << std::endl; + // prove f + cdp.addStep(f, PfRule::EQ_RESOLVE, {curr, fullRewrite}, {}); + Trace("smt-pppg") << "...finished" << std::endl; } - // prove f - cdp.addStep(f, PfRule::EQ_RESOLVE, {curr, fullRewrite}, {}); // overall, proof is: // --------- from proof generator ---------- from proof generator @@ -130,6 +182,15 @@ std::shared_ptr<ProofNode> PreprocessProofGenerator::getProofFor(Node f) return cdp.getProofFor(f); } +ProofNodeManager* PreprocessProofGenerator::getManager() { return d_pnm; } + +LazyCDProof* PreprocessProofGenerator::allocateHelperProof() +{ + std::shared_ptr<LazyCDProof> helperPf = std::make_shared<LazyCDProof>(d_pnm); + d_helperProofs.push_back(helperPf); + return helperPf.get(); +} + std::string PreprocessProofGenerator::identify() const { return "PreprocessProofGenerator"; |