diff options
Diffstat (limited to 'src/smt')
-rw-r--r-- | src/smt/preprocess_proof_generator.cpp | 117 | ||||
-rw-r--r-- | src/smt/preprocess_proof_generator.h | 24 | ||||
-rw-r--r-- | src/smt/proof_manager.cpp | 4 | ||||
-rw-r--r-- | src/smt/proof_manager.h | 2 | ||||
-rw-r--r-- | src/smt/smt_engine.cpp | 2 |
5 files changed, 115 insertions, 34 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"; diff --git a/src/smt/preprocess_proof_generator.h b/src/smt/preprocess_proof_generator.h index 5319071f0..b71187188 100644 --- a/src/smt/preprocess_proof_generator.h +++ b/src/smt/preprocess_proof_generator.h @@ -19,8 +19,12 @@ #include <map> +#include "context/cdhashmap.h" +#include "context/cdlist.h" +#include "expr/lazy_proof.h" #include "expr/proof_generator.h" #include "expr/proof_node_manager.h" +#include "theory/eager_proof_generator.h" #include "theory/trust_node.h" namespace CVC4 { @@ -41,8 +45,11 @@ namespace smt { */ class PreprocessProofGenerator : public ProofGenerator { + typedef context::CDHashMap<Node, theory::TrustNode, NodeHashFunction> + NodeTrustNodeMap; + public: - PreprocessProofGenerator(ProofNodeManager* pnm); + PreprocessProofGenerator(context::UserContext* u, ProofNodeManager* pnm); ~PreprocessProofGenerator() {} /** * Notify that n is a new assertion, where pg can provide a proof of n. @@ -61,6 +68,17 @@ class PreprocessProofGenerator : public ProofGenerator std::shared_ptr<ProofNode> getProofFor(Node f) override; /** Identify */ std::string identify() const override; + /** Get the proof manager */ + ProofNodeManager* getManager(); + /** + * Allocate a helper proof. This returns a fresh lazy proof object that + * remains alive in this user context. This feature is used to construct + * helper proofs for preprocessing, e.g. to support the skeleton of proofs + * that connect AssertionPipeline::conjoin steps. + * + * Internally, this adds a LazyCDProof to the list d_helperProofs below. + */ + LazyCDProof* allocateHelperProof(); private: /** The proof node manager */ @@ -72,7 +90,9 @@ class PreprocessProofGenerator : public ProofGenerator * (1) A trust node REWRITE proving (n_src = n) for some n_src, or * (2) A trust node LEMMA proving n. */ - std::map<Node, theory::TrustNode> d_src; + NodeTrustNodeMap d_src; + /** A context-dependent list of LazyCDProof, allocated for conjoin steps */ + context::CDList<std::shared_ptr<LazyCDProof> > d_helperProofs; }; } // namespace smt diff --git a/src/smt/proof_manager.cpp b/src/smt/proof_manager.cpp index f51a116b7..df7b6bf4d 100644 --- a/src/smt/proof_manager.cpp +++ b/src/smt/proof_manager.cpp @@ -22,10 +22,10 @@ namespace CVC4 { namespace smt { -PfManager::PfManager(SmtEngine* smte) +PfManager::PfManager(context::UserContext* u, SmtEngine* smte) : d_pchecker(new ProofChecker(options::proofNewPedantic())), d_pnm(new ProofNodeManager(d_pchecker.get())), - d_pppg(new PreprocessProofGenerator(d_pnm.get())), + d_pppg(new PreprocessProofGenerator(u, d_pnm.get())), d_pfpp(new ProofPostproccess(d_pnm.get(), smte, d_pppg.get())), d_finalProof(nullptr) { diff --git a/src/smt/proof_manager.h b/src/smt/proof_manager.h index bda741a05..118b82bec 100644 --- a/src/smt/proof_manager.h +++ b/src/smt/proof_manager.h @@ -41,7 +41,7 @@ class Assertions; class PfManager { public: - PfManager(SmtEngine* smte); + PfManager(context::UserContext* u, SmtEngine* smte); ~PfManager(); /** * Print the proof on the output channel of the current options in scope. diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 3caf03946..755822d2a 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -270,7 +270,7 @@ void SmtEngine::finishInit() ProofNodeManager* pnm = nullptr; if (options::proofNew()) { - d_pfManager.reset(new PfManager(this)); + d_pfManager.reset(new PfManager(getUserContext(), this)); // use this proof node manager pnm = d_pfManager->getProofNodeManager(); // enable proof support in the rewriter |