From: Andrew Reynolds Date: Sun, 18 Oct 2020 22:17:37 +0000 (-0500) Subject: (proof-new) More features for SMT proof post-processor (#5246) X-Git-Tag: cvc5-1.0.0~2700 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d4a23ab31a6f811dc4a9c3f24acb9a325fcb6d5a;p=cvc5.git (proof-new) More features for SMT proof post-processor (#5246) This updates the SMT proof postprocessor with additional stats. It also adds the feature to handle conjunctions as substitution, e.g. a child proof concluding (and (= x t) (= y s)) is interpreted as a substitution for x, y, whereas previously we insisted they must be provided separately. --- diff --git a/src/smt/proof_post_processor.cpp b/src/smt/proof_post_processor.cpp index 0d5578734..0c2f8ccf8 100644 --- a/src/smt/proof_post_processor.cpp +++ b/src/smt/proof_post_processor.cpp @@ -376,6 +376,7 @@ Node ProofPostprocessCallback::expandMacros(PfRule id, } else if (id == PfRule::SUBS) { + NodeManager* nm = NodeManager::currentNM(); // Notice that a naive way to reconstruct SUBS is to do a term conversion // proof for each substitution. // The proof of f(a) * { a -> g(b) } * { b -> c } = f(g(c)) is: @@ -400,21 +401,41 @@ Node ProofPostprocessCallback::expandMacros(PfRule id, builtin::BuiltinProofRuleChecker::getMethodId(args[1], ids); } std::vector> pfs; - std::vector vvec; - std::vector svec; + std::vector vsList; + std::vector ssList; + std::vector fromList; std::vector pgs; + // first, compute the entire substitution for (size_t i = 0, nchild = children.size(); i < nchild; i++) + { + // get the substitution + builtin::BuiltinProofRuleChecker::getSubstitutionFor( + children[i], vsList, ssList, fromList, ids); + // ensure proofs for each formula in fromList + if (children[i].getKind() == AND && ids == MethodId::SB_DEFAULT) + { + for (size_t j = 0, nchildi = children[i].getNumChildren(); j < nchildi; + j++) + { + Node nodej = nm->mkConst(Rational(j)); + cdp->addStep( + children[i][j], PfRule::AND_ELIM, {children[i]}, {nodej}); + } + } + } + std::vector vvec; + std::vector svec; + for (size_t i = 0, nvs = vsList.size(); i < nvs; i++) { // Note we process in forward order, since later substitution should be // applied to earlier ones, and the last child of a SUBS is processed // first. - // get the substitution - TNode var, subs; - builtin::BuiltinProofRuleChecker::getSubstitution( - children[i], var, subs, ids); + TNode var = vsList[i]; + TNode subs = ssList[i]; + TNode childFrom = fromList[i]; Trace("smt-proof-pp-debug") - << "...process " << var << " -> " << subs << " (" << children[i] - << ", " << ids << ")" << std::endl; + << "...process " << var << " -> " << subs << " (" << childFrom << ", " + << ids << ")" << std::endl; // apply the current substitution to the range if (!vvec.empty()) { @@ -429,7 +450,13 @@ Node ProofPostprocessCallback::expandMacros(PfRule id, std::shared_ptr pf = std::make_shared(d_pnm); pfs.push_back(pf); // prove the updated substitution - TConvProofGenerator tcg(d_pnm, nullptr, TConvPolicy::ONCE); + TConvProofGenerator tcg(d_pnm, + nullptr, + TConvPolicy::ONCE, + TConvCachePolicy::NEVER, + "nested_SUBS_TConvProofGenerator", + nullptr, + true); // add previous rewrite steps for (unsigned j = 0, nvars = vvec.size(); j < nvars; j++) { @@ -442,11 +469,11 @@ Node ProofPostprocessCallback::expandMacros(PfRule id, Assert(pfn != nullptr); // add the proof pf->addProof(pfn); - // get proof for children[i] from cdp - pfn = cdp->getProofFor(children[i]); + // get proof for childFrom from cdp + pfn = cdp->getProofFor(childFrom); pf->addProof(pfn); // ensure we have a proof of var = subs - Node veqs = addProofForSubsStep(var, subs, children[i], pf.get()); + Node veqs = addProofForSubsStep(var, subs, childFrom, pf.get()); // transitivity pf->addStep(var.eqNode(ss), PfRule::TRANS, {veqs, seqss}, {}); // add to the substitution @@ -458,9 +485,9 @@ Node ProofPostprocessCallback::expandMacros(PfRule id, } // 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[i] as a Boolean assignment (e.g. - // children[i] = true if we are using MethodId::SB_LITERAL). - addProofForSubsStep(var, subs, children[i], cdp); + // uses the assumption childFrom as a Boolean assignment (e.g. + // childFrom = true if we are using MethodId::SB_LITERAL). + addProofForSubsStep(var, subs, childFrom, cdp); vvec.push_back(var); svec.push_back(subs); pgs.push_back(cdp); @@ -470,7 +497,13 @@ Node ProofPostprocessCallback::expandMacros(PfRule id, if (ts != t) { // should be implied by the substitution now - TConvProofGenerator tcpg(d_pnm, nullptr, TConvPolicy::ONCE); + TConvProofGenerator tcpg(d_pnm, + nullptr, + TConvPolicy::ONCE, + TConvCachePolicy::NEVER, + "SUBS_TConvProofGenerator", + nullptr, + true); for (unsigned j = 0, nvars = vvec.size(); j < nvars; j++) { // not necessarily closed, so we pass false to addRewriteStep. @@ -523,7 +556,14 @@ Node ProofPostprocessCallback::expandMacros(PfRule id, std::shared_ptr pfn = trn.toProofNode(); if (pfn == nullptr) { + Trace("smt-proof-pp-debug") + << "Use TRUST_REWRITE for " << eq << std::endl; // did not have a proof of rewriting, probably isExtEq is true + if (isExtEq) + { + // don't update + return Node::null(); + } cdp->addStep(eq, PfRule::TRUST_REWRITE, {}, {eq}); } else @@ -644,23 +684,30 @@ ProofPostprocessFinalCallback::ProofPostprocessFinalCallback( ProofNodeManager* pnm) : d_ruleCount("finalProof::ruleCount"), d_totalRuleCount("finalProof::totalRuleCount", 0), + d_minPedanticLevel("finalProof::minPedanticLevel", 10), + d_numFinalProofs("finalProofs::numFinalProofs", 0), d_pnm(pnm), d_pedanticFailure(false) { smtStatisticsRegistry()->registerStat(&d_ruleCount); smtStatisticsRegistry()->registerStat(&d_totalRuleCount); + smtStatisticsRegistry()->registerStat(&d_minPedanticLevel); + smtStatisticsRegistry()->registerStat(&d_numFinalProofs); } ProofPostprocessFinalCallback::~ProofPostprocessFinalCallback() { smtStatisticsRegistry()->unregisterStat(&d_ruleCount); smtStatisticsRegistry()->unregisterStat(&d_totalRuleCount); + smtStatisticsRegistry()->unregisterStat(&d_minPedanticLevel); + smtStatisticsRegistry()->unregisterStat(&d_numFinalProofs); } void ProofPostprocessFinalCallback::initializeUpdate() { d_pedanticFailure = false; d_pedanticFailureOut.str(""); + ++d_numFinalProofs; } bool ProofPostprocessFinalCallback::shouldUpdate(std::shared_ptr pn, @@ -687,6 +734,11 @@ bool ProofPostprocessFinalCallback::shouldUpdate(std::shared_ptr pn, } } } + uint32_t plevel = d_pnm->getChecker()->getPedanticLevel(r); + if (plevel != 0) + { + d_minPedanticLevel.minAssign(plevel); + } // record stats for the rule d_ruleCount << r; ++d_totalRuleCount; diff --git a/src/smt/proof_post_processor.h b/src/smt/proof_post_processor.h index d7186ea74..3c0d4fbaa 100644 --- a/src/smt/proof_post_processor.h +++ b/src/smt/proof_post_processor.h @@ -173,6 +173,10 @@ class ProofPostprocessFinalCallback : public ProofNodeUpdaterCallback HistogramStat d_ruleCount; /** Total number of postprocessed rule applications */ IntStat d_totalRuleCount; + /** The minimum pedantic level of any rule encountered */ + IntStat d_minPedanticLevel; + /** The total number of final proofs */ + IntStat d_numFinalProofs; /** Proof node manager (used for pedantic checking) */ ProofNodeManager* d_pnm; /** Was there a pedantic failure? */ @@ -198,6 +202,7 @@ class ProofPostproccess void process(std::shared_ptr pf); /** set eliminate rule */ void setEliminateRule(PfRule rule); + private: /** The proof node manager */ ProofNodeManager* d_pnm; diff --git a/src/theory/builtin/proof_checker.cpp b/src/theory/builtin/proof_checker.cpp index 8824859d4..6fc4671ee 100644 --- a/src/theory/builtin/proof_checker.cpp +++ b/src/theory/builtin/proof_checker.cpp @@ -69,11 +69,11 @@ void BuiltinProofRuleChecker::registerTo(ProofChecker* pc) pc->registerChecker(PfRule::REMOVE_TERM_FORMULA_AXIOM, this); // trusted rules pc->registerTrustedChecker(PfRule::THEORY_LEMMA, this, 1); - pc->registerTrustedChecker(PfRule::PREPROCESS, this, 2); - pc->registerTrustedChecker(PfRule::PREPROCESS_LEMMA, this, 2); - pc->registerTrustedChecker(PfRule::THEORY_PREPROCESS, this, 2); - pc->registerTrustedChecker(PfRule::THEORY_PREPROCESS_LEMMA, this, 2); - pc->registerTrustedChecker(PfRule::WITNESS_AXIOM, this, 2); + pc->registerTrustedChecker(PfRule::PREPROCESS, this, 3); + pc->registerTrustedChecker(PfRule::PREPROCESS_LEMMA, this, 3); + pc->registerTrustedChecker(PfRule::THEORY_PREPROCESS, this, 3); + pc->registerTrustedChecker(PfRule::THEORY_PREPROCESS_LEMMA, this, 3); + pc->registerTrustedChecker(PfRule::WITNESS_AXIOM, this, 3); pc->registerTrustedChecker(PfRule::TRUST_REWRITE, this, 1); pc->registerTrustedChecker(PfRule::TRUST_SUBS, this, 1); } @@ -117,10 +117,10 @@ Node BuiltinProofRuleChecker::applyRewrite(Node n, MethodId idr) return n; } -bool BuiltinProofRuleChecker::getSubstitution(Node exp, - TNode& var, - TNode& subs, - MethodId ids) +bool BuiltinProofRuleChecker::getSubstitutionForLit(Node exp, + TNode& var, + TNode& subs, + MethodId ids) { if (ids == MethodId::SB_DEFAULT) { @@ -152,17 +152,57 @@ bool BuiltinProofRuleChecker::getSubstitution(Node exp, return true; } +bool BuiltinProofRuleChecker::getSubstitutionFor(Node exp, + std::vector& vars, + std::vector& subs, + std::vector& from, + MethodId ids) +{ + TNode v; + TNode s; + if (exp.getKind() == AND && ids == MethodId::SB_DEFAULT) + { + for (const Node& ec : exp) + { + // non-recursive, do not use nested AND + if (!getSubstitutionForLit(ec, v, s, ids)) + { + return false; + } + vars.push_back(v); + subs.push_back(s); + from.push_back(ec); + } + return true; + } + bool ret = getSubstitutionForLit(exp, v, s, ids); + vars.push_back(v); + subs.push_back(s); + from.push_back(exp); + return ret; +} + Node BuiltinProofRuleChecker::applySubstitution(Node n, Node exp, MethodId ids) { - TNode var, subs; - if (!getSubstitution(exp, var, subs, ids)) + std::vector vars; + std::vector subs; + std::vector from; + if (!getSubstitutionFor(exp, vars, subs, from, ids)) { return Node::null(); } - Trace("builtin-pfcheck-debug") - << "applySubstitution (" << ids << "): " << var << " -> " << subs - << " (from " << exp << ")" << std::endl; - return n.substitute(var, subs); + Node ns = n; + // apply substitution one at a time, in reverse order + for (size_t i = 0, nvars = vars.size(); i < nvars; i++) + { + TNode v = vars[nvars - 1 - i]; + TNode s = subs[nvars - 1 - i]; + Trace("builtin-pfcheck-debug") + << "applySubstitution (" << ids << "): " << v << " -> " << s + << " (from " << exp << ")" << std::endl; + ns = ns.substitute(v, s); + } + return ns; } Node BuiltinProofRuleChecker::applySubstitution(Node n, @@ -212,6 +252,7 @@ Node BuiltinProofRuleChecker::checkInternal(PfRule id, } else if (id == PfRule::SCOPE) { + NodeManager * nm = NodeManager::currentNM(); Assert(children.size() == 1); if (args.empty()) { @@ -224,7 +265,7 @@ Node BuiltinProofRuleChecker::checkInternal(PfRule id, { return ant.notNode(); } - return NodeManager::currentNM()->mkNode(IMPLIES, ant, children[0]); + return nm->mkNode(IMPLIES, ant, children[0]); } else if (id == PfRule::SUBS) { @@ -270,7 +311,7 @@ Node BuiltinProofRuleChecker::checkInternal(PfRule id, { return Node::null(); } - Node res = applySubstitutionRewrite(args[0], children, idr); + Node res = applySubstitutionRewrite(args[0], children, ids, idr); return args[0].eqNode(res); } else if (id == PfRule::MACRO_SR_PRED_INTRO) diff --git a/src/theory/builtin/proof_checker.h b/src/theory/builtin/proof_checker.h index d1c3309c3..66b04de45 100644 --- a/src/theory/builtin/proof_checker.h +++ b/src/theory/builtin/proof_checker.h @@ -84,13 +84,27 @@ class BuiltinProofRuleChecker : public ProofRuleChecker */ Node applyRewrite(Node n, MethodId idr = MethodId::RW_REWRITE); /** - * Get substitution. Updates vars/subs to the substitution specified by - * exp for the substitution method ids. + * Get substitution for literal exp. Updates vars/subs to the substitution + * specified by exp for the substitution method ids. */ - static bool getSubstitution(Node exp, - TNode& var, - TNode& subs, - MethodId ids = MethodId::SB_DEFAULT); + static bool getSubstitutionForLit(Node exp, + TNode& var, + TNode& subs, + MethodId ids = MethodId::SB_DEFAULT); + /** + * Get substitution for formula exp. Adds to vars/subs to the substitution + * specified by exp for the substitution method ids, which may be multiple + * substitutions if exp is of kind AND and ids is SB_DEFAULT (note the other + * substitution types always interpret applications of AND as a formula). + * The vector "from" are the literals from exp that each substitution in + * vars/subs are based on. For example, if exp is (and (= x t) (= y s)), then + * vars = { x, y }, subs = { t, s }, from = { (= x y), (= y s) }. + */ + static bool getSubstitutionFor(Node exp, + std::vector& vars, + std::vector& subs, + std::vector& from, + MethodId ids = MethodId::SB_DEFAULT); /** * Apply substitution on n in skolem form. This encapsulates the exact