From 3bfdead7da2143fd801fa632165a986b2631ad3d Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 19 Oct 2020 12:01:33 -0500 Subject: [PATCH] (proof-new) Updates to assertions pipeline and preprocess generator (#5300) This updates and improves assertions pipeline and preprocess generator so that they avoid cyclic proofs and have better infrastructure for catching pedantic failures. This is in preparation for making the non-clausal-simplification pass proof producing. --- src/preprocessing/assertion_pipeline.cpp | 73 ++++++++++++++++-------- src/preprocessing/assertion_pipeline.h | 5 +- src/smt/preprocess_proof_generator.cpp | 44 ++++++++++++-- src/smt/preprocess_proof_generator.h | 31 +++++++++- 4 files changed, 122 insertions(+), 31 deletions(-) diff --git a/src/preprocessing/assertion_pipeline.cpp b/src/preprocessing/assertion_pipeline.cpp index 4529ad5e1..78c459cb7 100644 --- a/src/preprocessing/assertion_pipeline.cpp +++ b/src/preprocessing/assertion_pipeline.cpp @@ -62,6 +62,8 @@ void AssertionPipeline::push_back(Node n, Assert(d_assumptionsStart + d_numAssumptions == d_nodes.size() - 1); d_numAssumptions++; } + Trace("assert-pipeline") << "Assertions: ...new assertion " << n + << ", isInput=" << isInput << std::endl; if (isProofEnabled()) { if (!isInput) @@ -71,7 +73,9 @@ void AssertionPipeline::push_back(Node n, } else { - Trace("smt-pppg") << "...input assertion " << n << std::endl; + Assert(pgen == nullptr); + // n is an input assertion, whose proof should be ASSUME. + d_pppg->notifyInput(n); } } } @@ -90,8 +94,8 @@ void AssertionPipeline::replace(size_t i, Node n, ProofGenerator* pgen) // no change, skip return; } - Trace("smt-pppg-repl") << "Replace " << d_nodes[i] << " with " << n - << std::endl; + Trace("assert-pipeline") << "Assertions: Replace " << d_nodes[i] << " with " + << n << std::endl; if (options::unsatCores()) { ProofManager::currentPM()->addDependence(n, d_nodes[i]); @@ -111,6 +115,7 @@ void AssertionPipeline::replaceTrusted(size_t i, theory::TrustNode trn) return; } Assert(trn.getKind() == theory::TrustNodeKind::REWRITE); + Assert(trn.getProven()[0] == d_nodes[i]); replace(i, trn.getNode(), trn.getGenerator()); } @@ -145,6 +150,10 @@ void AssertionPipeline::conjoin(size_t i, Node n, ProofGenerator* pg) NodeManager* nm = NodeManager::currentNM(); Node newConj = nm->mkNode(kind::AND, d_nodes[i], n); Node newConjr = theory::Rewriter::rewrite(newConj); + Trace("assert-pipeline") << "Assertions: conjoin " << n << " to " + << d_nodes[i] << std::endl; + Trace("assert-pipeline-debug") << "conjoin " << n << " to " << d_nodes[i] + << ", got " << newConjr << std::endl; if (newConjr == d_nodes[i]) { // trivial, skip @@ -152,29 +161,45 @@ void AssertionPipeline::conjoin(size_t i, Node n, ProofGenerator* pg) } if (isProofEnabled()) { - // ---------- from pppg --------- from pg - // d_nodes[i] n - // -------------------------------- AND_INTRO - // d_nodes[i] ^ n - // -------------------------------- MACRO_SR_PRED_TRANSFORM - // rewrite( d_nodes[i] ^ n ) - // allocate a fresh proof which will act as the proof generator - LazyCDProof* lcp = d_pppg->allocateHelperProof(); - lcp->addLazyStep(d_nodes[i], d_pppg, false); - lcp->addLazyStep( - n, pg, false, "AssertionPipeline::conjoin", false, PfRule::PREPROCESS); - lcp->addStep(newConj, PfRule::AND_INTRO, {d_nodes[i], n}, {}); - if (newConjr != newConj) + if (newConjr == n) { - lcp->addStep( - newConjr, PfRule::MACRO_SR_PRED_TRANSFORM, {newConj}, {newConjr}); + // don't care about the previous proof and can simply plug in the + // proof from pg if the resulting assertion is the same as n. + d_pppg->notifyNewAssert(newConjr, pg); + } + else + { + // ---------- from pppg --------- from pg + // d_nodes[i] n + // -------------------------------- AND_INTRO + // d_nodes[i] ^ n + // -------------------------------- MACRO_SR_PRED_TRANSFORM + // rewrite( d_nodes[i] ^ n ) + // allocate a fresh proof which will act as the proof generator + LazyCDProof* lcp = d_pppg->allocateHelperProof(); + lcp->addLazyStep(n, pg, false); + if (d_nodes[i].isConst() && d_nodes[i].getConst()) + { + // skip the AND_INTRO if the previous d_nodes[i] was true + newConj = n; + } + else + { + lcp->addLazyStep(d_nodes[i], d_pppg); + lcp->addStep(newConj, PfRule::AND_INTRO, {d_nodes[i], n}, {}); + } + if (newConjr != newConj) + { + lcp->addStep( + newConjr, PfRule::MACRO_SR_PRED_TRANSFORM, {newConj}, {newConjr}); + } + // Notice we have constructed a proof of a new assertion, where d_pppg + // is referenced in the lazy proof above. If alternatively we had + // constructed a proof of d_nodes[i] = rewrite( d_nodes[i] ^ n ), we would + // have used notifyPreprocessed. However, it is simpler to make the + // above proof. + d_pppg->notifyNewAssert(newConjr, lcp); } - // Notice we have constructed a proof of a new assertion, where d_pppg - // is referenced in the lazy proof above. If alternatively we had - // constructed a proof of d_nodes[i] = rewrite( d_nodes[i] ^ n ), we would - // have used notifyPreprocessed. However, it is simpler to make the - // above proof. - d_pppg->notifyNewAssert(newConjr, lcp); } if (options::unsatCores()) { diff --git a/src/preprocessing/assertion_pipeline.h b/src/preprocessing/assertion_pipeline.h index 5c50903c5..75f370450 100644 --- a/src/preprocessing/assertion_pipeline.h +++ b/src/preprocessing/assertion_pipeline.h @@ -88,7 +88,10 @@ class AssertionPipeline * where d_nodes[i] is the assertion at position i prior to this call. */ void replace(size_t i, Node n, ProofGenerator* pg = nullptr); - /** Same as above, with TrustNode */ + /** + * Same as above, with TrustNode trn, which is of kind REWRITE and proves + * d_nodes[i] = n for some n. + */ void replaceTrusted(size_t i, theory::TrustNode trn); IteSkolemMap& getIteSkolemMap() { return d_iteSkolemMap; } diff --git a/src/smt/preprocess_proof_generator.cpp b/src/smt/preprocess_proof_generator.cpp index 7bd10e0b0..465e7a471 100644 --- a/src/smt/preprocess_proof_generator.cpp +++ b/src/smt/preprocess_proof_generator.cpp @@ -16,6 +16,7 @@ #include "smt/preprocess_proof_generator.h" #include "expr/proof.h" +#include "options/smt_options.h" #include "theory/rewriter.h" namespace CVC4 { @@ -23,20 +24,35 @@ namespace smt { PreprocessProofGenerator::PreprocessProofGenerator(ProofNodeManager* pnm, context::Context* c, - std::string name) + std::string name, + PfRule ra, + PfRule rpp) : d_pnm(pnm), d_src(c ? c : &d_context), d_helperProofs(pnm, c ? c : &d_context), - d_name(name) + d_inputPf(pnm, nullptr), + d_name(name), + d_ra(ra), + d_rpp(rpp) { } +void PreprocessProofGenerator::notifyInput(Node n) +{ + notifyNewAssert(n, &d_inputPf); +} + void PreprocessProofGenerator::notifyNewAssert(Node n, ProofGenerator* pg) { Trace("smt-proof-pp-debug") << "PreprocessProofGenerator::notifyNewAssert: " << n << 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())) + { + checkEagerPedantic(d_ra); + } d_src[n] = theory::TrustNode::mkTrustLemma(n, pg); } else @@ -77,6 +93,10 @@ void PreprocessProofGenerator::notifyTrustedPreprocessed(theory::TrustNode tnp) << std::endl; if (d_src.find(np) == d_src.end()) { + if (tnp.getGenerator() == nullptr) + { + checkEagerPedantic(d_rpp); + } d_src[np] = tnp; } else @@ -167,9 +187,7 @@ std::shared_ptr PreprocessProofGenerator::getProofFor(Node f) 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, + tnk == theory::TrustNodeKind::LEMMA ? d_ra : d_rpp, {}, {proven}); } @@ -214,5 +232,21 @@ LazyCDProof* PreprocessProofGenerator::allocateHelperProof() std::string PreprocessProofGenerator::identify() const { return d_name; } +void PreprocessProofGenerator::checkEagerPedantic(PfRule r) +{ + if (options::proofNewEagerChecking()) + { + // catch a pedantic failure now, which otherwise would not be + // triggered since we are doing lazy proof generation + ProofChecker* pc = d_pnm->getChecker(); + std::stringstream serr; + if (pc->isPedanticFailure(r, serr)) + { + Unhandled() << "PreprocessProofGenerator::checkEagerPedantic: " + << serr.str(); + } + } +} + } // namespace smt } // namespace CVC4 diff --git a/src/smt/preprocess_proof_generator.h b/src/smt/preprocess_proof_generator.h index e5a9d17f7..a0c090ad7 100644 --- a/src/smt/preprocess_proof_generator.h +++ b/src/smt/preprocess_proof_generator.h @@ -58,10 +58,25 @@ class PreprocessProofGenerator : public ProofGenerator NodeTrustNodeMap; public: + /** + * @param pnm The proof node manager + * @param c The context this class depends on + * @param name The name of this generator (for debugging) + * @param ra The proof rule to use when no generator is provided for new + * assertions + * @param rpp The proof rule to use when no generator is provided for + * preprocessing steps. + */ PreprocessProofGenerator(ProofNodeManager* pnm, context::Context* c = nullptr, - std::string name = "PreprocessProofGenerator"); + std::string name = "PreprocessProofGenerator", + PfRule ra = PfRule::PREPROCESS_LEMMA, + PfRule rpp = PfRule::PREPROCESS); ~PreprocessProofGenerator() {} + /** + * Notify that n is an input (its proof is ASSUME). + */ + void notifyInput(Node n); /** * Notify that n is a new assertion, where pg can provide a proof of n. */ @@ -94,6 +109,11 @@ class PreprocessProofGenerator : public ProofGenerator LazyCDProof* allocateHelperProof(); private: + /** + * Possibly check pedantic failure for null proof generator provided + * to this class. + */ + void checkEagerPedantic(PfRule r); /** The proof node manager */ ProofNodeManager* d_pnm; /** A dummy context used by this class if none is provided */ @@ -108,8 +128,17 @@ class PreprocessProofGenerator : public ProofGenerator NodeTrustNodeMap d_src; /** A context-dependent list of LazyCDProof, allocated for conjoin steps */ LazyCDProofSet d_helperProofs; + /** + * A cd proof for input assertions, this is an empty proof that intentionally + * returns (ASSUME f) for all f. + */ + CDProof d_inputPf; /** Name for debugging */ std::string d_name; + /** The trust rule for new assertions with no provided proof generator */ + PfRule d_ra; + /** The trust rule for rewrites with no provided proof generator */ + PfRule d_rpp; }; } // namespace smt -- 2.30.2