From: Andrew Reynolds Date: Fri, 28 Aug 2020 18:48:40 +0000 (-0500) Subject: (proof-new) Add the SMT proof post processor (#4913) X-Git-Tag: cvc5-1.0.0~2943 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d1bb100d75aca76fdeb7a18b6c044035029ffe17;p=cvc5.git (proof-new) Add the SMT proof post processor (#4913) This PR adds the proof post-processor, which is the final authority on putting together the overall proof. It additionally implements lazy pedantic failures and statistics. This PR also corrects a subtle bug in the elimination of SUBS which requires a TRUE_INTRO/FALSE_INTRO in certain cases. --- diff --git a/src/smt/proof_post_processor.cpp b/src/smt/proof_post_processor.cpp index 5046dee92..197cdd4b7 100644 --- a/src/smt/proof_post_processor.cpp +++ b/src/smt/proof_post_processor.cpp @@ -404,17 +404,8 @@ Node ProofPostprocessCallback::expandMacros(PfRule id, pfn = cdp->getProofFor(children[i]); pf->addProof(pfn); // ensure we have a proof of var = subs - Node veqs = var.eqNode(subs); - if (veqs != children[index]) - { - // should be true intro or false intro - Assert(subs.isConst()); - pf->addStep(veqs, - subs.getConst() ? PfRule::TRUE_INTRO - : PfRule::FALSE_INTRO, - {children[index]}, - {}); - } + Node veqs = addProofForSubsStep(var, subs, children[index], pf.get()); + // transitivity pf->addStep(var.eqNode(ss), PfRule::TRANS, {veqs, seqss}, {}); // add to the substitution vvec.push_back(var); @@ -423,7 +414,11 @@ Node ProofPostprocessCallback::expandMacros(PfRule id, continue; } } - // just use equality from CDProof + // Just use equality from CDProof, but ensure we have a proof in cdp. + // This may involve a TRUE_INTRO/FALSE_INTRO if the substitution step + // uses the assumption children[index] as a Boolean assignment (e.g. + // children[index] = true if we are using MethodId::SB_LITERAL). + addProofForSubsStep(var, subs, children[index], cdp); vvec.push_back(var); svec.push_back(subs); pgs.push_back(cdp); @@ -550,6 +545,26 @@ Node ProofPostprocessCallback::addProofForTrans( return Node::null(); } +Node ProofPostprocessCallback::addProofForSubsStep(Node var, + Node subs, + Node assump, + CDProof* cdp) +{ + // ensure we have a proof of var = subs + Node veqs = var.eqNode(subs); + if (veqs != assump) + { + // should be true intro or false intro + Assert(subs.isConst()); + cdp->addStep( + veqs, + subs.getConst() ? PfRule::TRUE_INTRO : PfRule::FALSE_INTRO, + {assump}, + {}); + } + return veqs; +} + bool ProofPostprocessCallback::addToTransChildren(Node eq, std::vector& tchildren, bool isSymm) @@ -568,5 +583,104 @@ bool ProofPostprocessCallback::addToTransChildren(Node eq, return true; } +ProofPostprocessFinalCallback::ProofPostprocessFinalCallback( + ProofNodeManager* pnm) + : d_ruleCount("finalProof::ruleCount"), + d_totalRuleCount("finalProof::totalRuleCount", 0), + d_pnm(pnm), + d_pedanticFailure(false) +{ + smtStatisticsRegistry()->registerStat(&d_ruleCount); + smtStatisticsRegistry()->registerStat(&d_totalRuleCount); +} + +ProofPostprocessFinalCallback::~ProofPostprocessFinalCallback() +{ + smtStatisticsRegistry()->unregisterStat(&d_ruleCount); + smtStatisticsRegistry()->unregisterStat(&d_totalRuleCount); +} + +void ProofPostprocessFinalCallback::initializeUpdate() +{ + d_pedanticFailure = false; + d_pedanticFailureOut.str(""); +} + +bool ProofPostprocessFinalCallback::shouldUpdate(ProofNode* pn) +{ + PfRule r = pn->getRule(); + if (Trace.isOn("final-pf-hole")) + { + if (r == PfRule::THEORY_REWRITE) + { + Trace("final-pf-hole") << "hole: " << r << " : " << pn->getResult() + << std::endl; + } + } + // if not doing eager pedantic checking, fail if below threshold + if (!options::proofNewPedanticEager()) + { + if (!d_pedanticFailure) + { + Assert(d_pedanticFailureOut.str().empty()); + if (d_pnm->getChecker()->isPedanticFailure(r, d_pedanticFailureOut)) + { + d_pedanticFailure = true; + } + } + } + // record stats for the rule + d_ruleCount << r; + ++d_totalRuleCount; + return false; +} + +bool ProofPostprocessFinalCallback::wasPedanticFailure(std::ostream& out) const +{ + if (d_pedanticFailure) + { + out << d_pedanticFailureOut.str(); + return true; + } + return false; +} + +ProofPostproccess::ProofPostproccess(ProofNodeManager* pnm, + SmtEngine* smte, + ProofGenerator* pppg) + : d_cb(pnm, smte, pppg), d_finalCb(pnm), d_pnm(pnm) +{ +} + +ProofPostproccess::~ProofPostproccess() {} + +void ProofPostproccess::process(std::shared_ptr pf) +{ + // Initialize the callback, which computes necessary static information about + // how to process, including how to process assumptions in pf. + d_cb.initializeUpdate(); + // now, process + ProofNodeUpdater updater(d_pnm, d_cb); + updater.process(pf); + // take stats and check pedantic + d_finalCb.initializeUpdate(); + ProofNodeUpdater finalizer(d_pnm, d_finalCb); + finalizer.process(pf); + + std::stringstream serr; + bool wasPedanticFailure = d_finalCb.wasPedanticFailure(serr); + if (wasPedanticFailure) + { + AlwaysAssert(!wasPedanticFailure) + << "ProofPostproccess::process: pedantic failure:" << std::endl + << serr.str(); + } +} + +void ProofPostproccess::setEliminateRule(PfRule rule) +{ + d_cb.setEliminateRule(rule); +} + } // namespace smt } // namespace CVC4 diff --git a/src/smt/proof_post_processor.h b/src/smt/proof_post_processor.h index 8dc540701..6c75af5ce 100644 --- a/src/smt/proof_post_processor.h +++ b/src/smt/proof_post_processor.h @@ -119,12 +119,82 @@ class ProofPostprocessCallback : public ProofNodeUpdaterCallback * @return The conclusion of the TRANS step. */ Node addProofForTrans(const std::vector& tchildren, CDProof* cdp); + /** + * Add proof for substitution step. Some substitutions are derived based + * on viewing a formula as a Boolean assignment (see MethodId::SB_LITERAL for + * example). This method ensures that the proof of var == subs exists + * in cdp, where var, subs were derived from BuiltinProofRuleChecker's + * getSubstitution method. + * + * @param var The variable of the substitution + * @param subs The substituted term + * @param assump The formula the substitution was derived from + * @param cdp The proof to add to + * @return var == subs, the conclusion of the substitution step. + */ + Node addProofForSubsStep(Node var, Node subs, Node assump, CDProof* cdp); /** Add eq (or its symmetry) to transivity children, if not reflexive */ bool addToTransChildren(Node eq, std::vector& tchildren, bool isSymm = false); }; +/** Final callback class, for stats and pedantic checking */ +class ProofPostprocessFinalCallback : public ProofNodeUpdaterCallback +{ + public: + ProofPostprocessFinalCallback(ProofNodeManager* pnm); + ~ProofPostprocessFinalCallback(); + /** + * Initialize, called once for each new ProofNode to process. This initializes + * static information to be used by successive calls to update. + */ + void initializeUpdate(); + /** Should proof pn be updated? Returns false, adds to stats. */ + bool shouldUpdate(ProofNode* pn) override; + /** was pedantic failure */ + bool wasPedanticFailure(std::ostream& out) const; + + private: + /** Counts number of postprocessed proof nodes for each kind of proof rule */ + HistogramStat d_ruleCount; + /** Total number of postprocessed rule applications */ + IntStat d_totalRuleCount; + /** Proof node manager (used for pedantic checking) */ + ProofNodeManager* d_pnm; + /** Was there a pedantic failure? */ + bool d_pedanticFailure; + /** The pedantic failure string for debugging */ + std::stringstream d_pedanticFailureOut; +}; + +/** + * The proof postprocessor module. This postprocesses the final proof + * produced by an SmtEngine. Its main two tasks are to: + * (1) Connect proofs of preprocessing, + * (2) Expand macro PfRule applications. + */ +class ProofPostproccess +{ + public: + ProofPostproccess(ProofNodeManager* pnm, + SmtEngine* smte, + ProofGenerator* pppg); + ~ProofPostproccess(); + /** post-process */ + void process(std::shared_ptr pf); + /** set eliminate rule */ + void setEliminateRule(PfRule rule); + + private: + /** The post process callback */ + ProofPostprocessCallback d_cb; + /** The post process callback for finalization */ + ProofPostprocessFinalCallback d_finalCb; + /** The proof node manager */ + ProofNodeManager* d_pnm; +}; + } // namespace smt } // namespace CVC4