From 4f5abe126235843cf17e83c7e1e29c91225573ca Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 13 Oct 2020 22:23:38 -0500 Subject: [PATCH] (proof-new) Generalize preprocess proof generator (#5245) This class is of general use, not just as the overall maintainer of proofs of preprocessing, but also locally within preprocessing passes. This generalizes the interface slightly and also does some minor cleaning. --- src/smt/preprocess_proof_generator.cpp | 68 ++++++++++++++++---------- src/smt/preprocess_proof_generator.h | 33 ++++++++++--- src/smt/proof_manager.cpp | 3 +- 3 files changed, 70 insertions(+), 34 deletions(-) diff --git a/src/smt/preprocess_proof_generator.cpp b/src/smt/preprocess_proof_generator.cpp index 1739a4e7d..7bd10e0b0 100644 --- a/src/smt/preprocess_proof_generator.cpp +++ b/src/smt/preprocess_proof_generator.cpp @@ -21,9 +21,13 @@ namespace CVC4 { namespace smt { -PreprocessProofGenerator::PreprocessProofGenerator(context::UserContext* u, - ProofNodeManager* pnm) - : d_pnm(pnm), d_src(u), d_helperProofs(u) +PreprocessProofGenerator::PreprocessProofGenerator(ProofNodeManager* pnm, + context::Context* c, + std::string name) + : d_pnm(pnm), + d_src(c ? c : &d_context), + d_helperProofs(pnm, c ? c : &d_context), + d_name(name) { } @@ -41,24 +45,43 @@ void PreprocessProofGenerator::notifyNewAssert(Node n, ProofGenerator* pg) } } +void PreprocessProofGenerator::notifyNewTrustedAssert(theory::TrustNode tn) +{ + notifyNewAssert(tn.getProven(), tn.getGenerator()); +} + void PreprocessProofGenerator::notifyPreprocessed(Node n, Node np, ProofGenerator* pg) { - // only keep if indeed it rewrote - if (n != np) + // only do anything if indeed it rewrote + if (n == np) { - Trace("smt-proof-pp-debug") - << "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; - } + return; + } + // call the trusted version + notifyTrustedPreprocessed(theory::TrustNode::mkTrustRewrite(n, np, pg)); +} + +void PreprocessProofGenerator::notifyTrustedPreprocessed(theory::TrustNode tnp) +{ + if (tnp.isNull()) + { + // no rewrite, nothing to do + return; + } + Assert(tnp.getKind() == theory::TrustNodeKind::REWRITE); + Node np = tnp.getNode(); + Trace("smt-proof-pp-debug") + << "PreprocessProofGenerator::notifyPreprocessed: " << tnp.getProven() + << std::endl; + if (d_src.find(np) == d_src.end()) + { + d_src[np] = tnp; + } + else + { + Trace("smt-proof-pp-debug") << "...already proven" << std::endl; } } @@ -73,8 +96,8 @@ std::shared_ptr PreprocessProofGenerator::getProofFor(Node f) // make CDProof to construct the proof below CDProof cdp(d_pnm); - Trace("smt-pppg") << "PreprocessProofGenerator::getProofFor: input " << f - << std::endl; + Trace("smt-pppg") << "PreprocessProofGenerator::getProofFor: (" << d_name + << ") input " << f << std::endl; Node curr = f; std::vector transChildren; std::unordered_set processed; @@ -186,15 +209,10 @@ ProofNodeManager* PreprocessProofGenerator::getManager() { return d_pnm; } LazyCDProof* PreprocessProofGenerator::allocateHelperProof() { - std::shared_ptr helperPf = std::make_shared(d_pnm); - d_helperProofs.push_back(helperPf); - return helperPf.get(); + return d_helperProofs.allocateProof(); } -std::string PreprocessProofGenerator::identify() const -{ - return "PreprocessProofGenerator"; -} +std::string PreprocessProofGenerator::identify() const { return d_name; } } // namespace smt } // namespace CVC4 diff --git a/src/smt/preprocess_proof_generator.h b/src/smt/preprocess_proof_generator.h index b71187188..e5a9d17f7 100644 --- a/src/smt/preprocess_proof_generator.h +++ b/src/smt/preprocess_proof_generator.h @@ -22,6 +22,7 @@ #include "context/cdhashmap.h" #include "context/cdlist.h" #include "expr/lazy_proof.h" +#include "expr/lazy_proof_set.h" #include "expr/proof_generator.h" #include "expr/proof_node_manager.h" #include "theory/eager_proof_generator.h" @@ -31,10 +32,18 @@ namespace CVC4 { namespace smt { /** - * A proof generator storing proofs of preprocessing. This has two main - * interfaces during solving: + * This is a proof generator that manages proofs for a set of formulas that + * may be replaced over time. This set of formulas is implicit; formulas that + * are not notified as assertions to this class are treated as assumptions. + * + * The main use case of this proof generator is for proofs of preprocessing, + * although it can be used in other scenarios where proofs for an evolving set + * of formulas is maintained. In the remainder of the description here, we + * describe its role as a proof generator for proofs of preprocessing. + * + * This class has two main interfaces during solving: * (1) notifyNewAssert, for assertions that are not part of the input and are - * added by preprocessing passes, + * added to the assertion pipeline by preprocessing passes, * (2) notifyPreprocessed, which is called when a preprocessing pass rewrites * an assertion into another. * Notice that input assertions do not need to be provided to this class. @@ -49,17 +58,23 @@ class PreprocessProofGenerator : public ProofGenerator NodeTrustNodeMap; public: - PreprocessProofGenerator(context::UserContext* u, ProofNodeManager* pnm); + PreprocessProofGenerator(ProofNodeManager* pnm, + context::Context* c = nullptr, + std::string name = "PreprocessProofGenerator"); ~PreprocessProofGenerator() {} /** * Notify that n is a new assertion, where pg can provide a proof of n. */ void notifyNewAssert(Node n, ProofGenerator* pg); + /** Notify a new assertion, trust node version. */ + void notifyNewTrustedAssert(theory::TrustNode tn); /** * Notify that n was replaced by np due to preprocessing, where pg can * provide a proof of the equality n=np. */ void notifyPreprocessed(Node n, Node np, ProofGenerator* pg); + /** Notify preprocessed, trust node version */ + void notifyTrustedPreprocessed(theory::TrustNode tnp); /** * Get proof for f, which returns a proof based on proving an equality based * on transitivity of preprocessing steps, and then using the original @@ -72,17 +87,17 @@ class PreprocessProofGenerator : public ProofGenerator 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 + * remains alive in the 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 */ ProofNodeManager* d_pnm; + /** A dummy context used by this class if none is provided */ + context::Context d_context; /** * The trust node that was the source of each node constructed during * preprocessing. For each n, d_src[n] is a trust node whose node is n. This @@ -92,7 +107,9 @@ class PreprocessProofGenerator : public ProofGenerator */ NodeTrustNodeMap d_src; /** A context-dependent list of LazyCDProof, allocated for conjoin steps */ - context::CDList > d_helperProofs; + LazyCDProofSet d_helperProofs; + /** Name for debugging */ + std::string d_name; }; } // namespace smt diff --git a/src/smt/proof_manager.cpp b/src/smt/proof_manager.cpp index df7b6bf4d..685032136 100644 --- a/src/smt/proof_manager.cpp +++ b/src/smt/proof_manager.cpp @@ -25,7 +25,8 @@ namespace smt { PfManager::PfManager(context::UserContext* u, SmtEngine* smte) : d_pchecker(new ProofChecker(options::proofNewPedantic())), d_pnm(new ProofNodeManager(d_pchecker.get())), - d_pppg(new PreprocessProofGenerator(u, d_pnm.get())), + d_pppg(new PreprocessProofGenerator( + d_pnm.get(), u, "smt::PreprocessProofGenerator")), d_pfpp(new ProofPostproccess(d_pnm.get(), smte, d_pppg.get())), d_finalProof(nullptr) { -- 2.30.2