diff options
| -rw-r--r-- | src/expr/proof_rule.cpp | 2 | ||||
| -rw-r--r-- | src/expr/proof_rule.h | 33 | ||||
| -rw-r--r-- | src/smt/proof_post_processor.cpp | 183 | ||||
| -rw-r--r-- | src/smt/proof_post_processor.h | 15 | ||||
| -rw-r--r-- | src/theory/builtin/proof_checker.cpp | 5 |
5 files changed, 157 insertions, 81 deletions
diff --git a/src/expr/proof_rule.cpp b/src/expr/proof_rule.cpp index 0fea387b5..a6ecd9bcb 100644 --- a/src/expr/proof_rule.cpp +++ b/src/expr/proof_rule.cpp @@ -41,6 +41,8 @@ const char* toString(PfRule id) case PfRule::THEORY_PREPROCESS: return "THEORY_PREPROCESS"; case PfRule::THEORY_PREPROCESS_LEMMA: return "THEORY_PREPROCESS_LEMMA"; case PfRule::WITNESS_AXIOM: return "WITNESS_AXIOM"; + case PfRule::TRUST_REWRITE: return "TRUST_REWRITE"; + case PfRule::TRUST_SUBS: return "TRUST_SUBS"; //================================================= Boolean rules case PfRule::RESOLUTION: return "RESOLUTION"; case PfRule::CHAIN_RESOLUTION: return "CHAIN_RESOLUTION"; diff --git a/src/expr/proof_rule.h b/src/expr/proof_rule.h index 9324f68c2..1583bdc3d 100644 --- a/src/expr/proof_rule.h +++ b/src/expr/proof_rule.h @@ -129,14 +129,21 @@ enum class PfRule : uint32_t // --------------------------------------------------------------- // Conclusion: F // where - // Rewriter{idr}(toWitness(F)*sigma{ids}(Fn)*...*sigma{ids}(F1)) == true + // Rewriter{idr}(F*sigma{ids}(Fn)*...*sigma{ids}(F1)) == true // where ids and idr are method identifiers. // - // Notice that we apply rewriting on the witness form of F, meaning that this + // More generally, this rule also holds when: + // Rewriter::rewrite(toWitness(F')) == true + // where F' is the result of the left hand side of the equality above. Here, + // notice that we apply rewriting on the witness form of F', meaning that this // rule may conclude an F whose Skolem form is justified by the definition of - // its (fresh) Skolem variables. Furthermore, notice that the rewriting and - // substitution is applied only within the side condition, meaning the - // rewritten form of the witness form of F does not escape this rule. + // its (fresh) Skolem variables. For example, this rule may justify the + // conclusion (= k t) where k is the purification Skolem for t, whose + // witness form is (witness ((x T)) (= x t)). + // + // Furthermore, notice that the rewriting and substitution is applied only + // within the side condition, meaning the rewritten form of the witness form + // of F does not escape this rule. MACRO_SR_PRED_INTRO, // ======== Substitution + Rewriting predicate elimination // @@ -165,11 +172,13 @@ enum class PfRule : uint32_t // ---------------------------------------- // Conclusion: G // where - // Rewriter{idr}(toWitness(F)*sigma{ids}(Fn)*...*sigma{ids}(F1)) == - // Rewriter{idr}(toWitness(G)*sigma{ids}(Fn)*...*sigma{ids}(F1)) + // Rewriter{idr}(F*sigma{ids}(Fn)*...*sigma{ids}(F1)) == + // Rewriter{idr}(G*sigma{ids}(Fn)*...*sigma{ids}(F1)) // - // Notice that we apply rewriting on the witness form of F and G, similar to - // MACRO_SR_PRED_INTRO. + // More generally, this rule also holds when: + // Rewriter::rewrite(toWitness(F')) == Rewriter::rewrite(toWitness(G')) + // where F' and G' are the result of each side of the equation above. Here, + // witness forms are used in a similar manner to MACRO_SR_PRED_INTRO above. MACRO_SR_PRED_TRANSFORM, //================================================= Processing rules @@ -224,6 +233,12 @@ enum class PfRule : uint32_t // where F is an existential (exists ((x T)) (P x)) used for introducing // a witness term (witness ((x T)) (P x)). WITNESS_AXIOM, + // where F is an equality (= t t') that holds by a form of rewriting that + // could not be replayed. + TRUST_REWRITE, + // where F is an equality (= t t') that holds by a form of substitution that + // could not be replayed. + TRUST_SUBS, //================================================= Boolean rules // ======== Resolution diff --git a/src/smt/proof_post_processor.cpp b/src/smt/proof_post_processor.cpp index 306035516..0d5578734 100644 --- a/src/smt/proof_post_processor.cpp +++ b/src/smt/proof_post_processor.cpp @@ -80,9 +80,11 @@ bool ProofPostprocessCallback::update(Node res, } else { + Trace("smt-proof-pp-debug") << "...get proof" << std::endl; Assert(d_pppg != nullptr); // get proof from preprocess proof generator pfn = d_pppg->getProofFor(f); + Trace("smt-proof-pp-debug") << "...finished get proof" << std::endl; // print for debugging if (pfn == nullptr) { @@ -101,11 +103,13 @@ bool ProofPostprocessCallback::update(Node res, } d_assumpToProof[f] = pfn; } - if (pfn == nullptr) + if (pfn == nullptr || pfn->getRule() == PfRule::ASSUME) { + Trace("smt-proof-pp-debug") << "...do not add proof" << std::endl; // no update return false; } + Trace("smt-proof-pp-debug") << "...add proof" << std::endl; // connect the proof cdp->addProof(pfn); return true; @@ -158,13 +162,16 @@ Node ProofPostprocessCallback::expandMacros(PfRule id, } ts = builtin::BuiltinProofRuleChecker::applySubstitution(t, children, sid); + Trace("smt-proof-pp-debug") + << "...eq intro subs equality is " << t << " == " << ts << ", from " + << sid << std::endl; if (ts != t) { Node eq = t.eqNode(ts); // apply SUBS proof rule if necessary if (!updateInternal(eq, PfRule::SUBS, children, sargs, cdp)) { - // if not elimianted, add as step + // if we specified that we did not want to eliminate, add as step cdp->addStep(eq, PfRule::SUBS, children, sargs); } tchildren.push_back(eq); @@ -189,6 +196,9 @@ Node ProofPostprocessCallback::expandMacros(PfRule id, static_cast<builtin::BuiltinProofRuleChecker*>( d_pnm->getChecker()->getCheckerFor(PfRule::MACRO_SR_EQ_INTRO)); Node tr = builtinPfC->applyRewrite(ts, rid); + Trace("smt-proof-pp-debug") + << "...eq intro rewrite equality is " << ts << " == " << tr << ", from " + << rid << std::endl; if (ts != tr) { Node eq = ts.eqNode(tr); @@ -214,66 +224,79 @@ Node ProofPostprocessCallback::expandMacros(PfRule id, std::vector<Node> tchildren; std::vector<Node> sargs = args; // take into account witness form, if necessary - if (d_wfpm.requiresWitnessFormIntro(args[0])) - { - Node weq = addProofForWitnessForm(args[0], cdp); - tchildren.push_back(weq); - // replace the first argument - sargs[0] = weq[1]; - } + bool reqWitness = d_wfpm.requiresWitnessFormIntro(args[0]); + Trace("smt-proof-pp-debug") + << "...pred intro reqWitness=" << reqWitness << std::endl; // (TRUE_ELIM // (TRANS - // ... proof of t = toWitness(t) ... - // (MACRO_SR_EQ_INTRO <children> :args (toWitness(t) args[1:])))) + // (MACRO_SR_EQ_INTRO <children> :args (t args[1:])) + // ... proof of apply_SR(t) = toWitness(apply_SR(t)) ... + // (MACRO_SR_EQ_INTRO {} {toWitness(apply_SR(t))}) + // )) + // Notice this is an optimized, one sided version of the expansion of + // MACRO_SR_PRED_TRANSFORM below. // We call the expandMacros method on MACRO_SR_EQ_INTRO, where notice // that this rule application is immediately expanded in the recursive // call and not added to the proof. Node conc = expandMacros(PfRule::MACRO_SR_EQ_INTRO, children, sargs, cdp); + Trace("smt-proof-pp-debug") + << "...pred intro conclusion is " << conc << std::endl; + Assert(!conc.isNull()); + Assert(conc.getKind() == EQUAL); + Assert(conc[0] == args[0]); tchildren.push_back(conc); - Assert(!conc.isNull() && conc.getKind() == EQUAL && conc[0] == sargs[0] - && conc[1] == d_true); - // transitivity if necessary + if (reqWitness) + { + Node weq = addProofForWitnessForm(conc[1], cdp); + Trace("smt-proof-pp-debug") << "...weq is " << weq << std::endl; + if (addToTransChildren(weq, tchildren)) + { + // toWitness(apply_SR(t)) = apply_SR(toWitness(apply_SR(t))) + // rewrite again, don't need substitution. Also we always use the + // default rewriter, due to the definition of MACRO_SR_PRED_INTRO. + Node weqr = expandMacros(PfRule::MACRO_SR_EQ_INTRO, {}, {weq[1]}, cdp); + addToTransChildren(weqr, tchildren); + } + } + // apply transitivity if necessary Node eq = addProofForTrans(tchildren, cdp); + Assert(!eq.isNull()); + Assert(eq.getKind() == EQUAL); + Assert(eq[0] == args[0]); + Assert(eq[1] == d_true); cdp->addStep(eq[0], PfRule::TRUE_ELIM, {eq}, {}); - Assert(eq[0] == args[0]); return eq[0]; } else if (id == PfRule::MACRO_SR_PRED_ELIM) { - // (TRUE_ELIM - // (TRANS - // (SYMM (MACRO_SR_EQ_INTRO children[1:] :args children[0] ++ args)) - // (TRUE_INTRO children[0]))) + // (EQ_RESOLVE + // children[0] + // (MACRO_SR_EQ_INTRO children[1:] :args children[0] ++ args)) std::vector<Node> schildren(children.begin() + 1, children.end()); std::vector<Node> srargs; srargs.push_back(children[0]); srargs.insert(srargs.end(), args.begin(), args.end()); Node conc = expandMacros(PfRule::MACRO_SR_EQ_INTRO, schildren, srargs, cdp); - Assert(!conc.isNull() && conc.getKind() == EQUAL && conc[0] == children[0]); - - Node eq1 = children[0].eqNode(d_true); - cdp->addStep(eq1, PfRule::TRUE_INTRO, {children[0]}, {}); - - Node concSym = conc[1].eqNode(conc[0]); - Node eq2 = conc[1].eqNode(d_true); - cdp->addStep(eq2, PfRule::TRANS, {concSym, eq1}, {}); - - cdp->addStep(conc[1], PfRule::TRUE_ELIM, {eq2}, {}); + Assert(!conc.isNull()); + Assert(conc.getKind() == EQUAL); + Assert(conc[0] == children[0]); + // apply equality resolve + cdp->addStep(conc[1], PfRule::EQ_RESOLVE, {children[0], conc}, {}); return conc[1]; } else if (id == PfRule::MACRO_SR_PRED_TRANSFORM) { - // (TRUE_ELIM - // (TRANS - // (MACRO_SR_EQ_INTRO children[1:] :args <args>) - // ... proof of a = wa - // (MACRO_SR_EQ_INTRO {} wa) - // (SYMM + // (EQ_RESOLVE + // children[0] + // (TRANS // (MACRO_SR_EQ_INTRO children[1:] :args (children[0] args[1:])) // ... proof of c = wc - // (MACRO_SR_EQ_INTRO {} wc)) - // (TRUE_INTRO children[0]))) + // (MACRO_SR_EQ_INTRO {} wc) + // (SYMM + // (MACRO_SR_EQ_INTRO children[1:] :args <args>) + // ... proof of a = wa + // (MACRO_SR_EQ_INTRO {} wa)))) // where // wa = toWitness(apply_SR(args[0])) and // wc = toWitness(apply_SR(children[0])). @@ -281,6 +304,7 @@ Node ProofPostprocessCallback::expandMacros(PfRule id, << "Transform " << children[0] << " == " << args[0] << std::endl; if (CDProof::isSame(children[0], args[0])) { + Trace("smt-proof-pp-debug") << "...nothing to do" << std::endl; // nothing to do return children[0]; } @@ -289,12 +313,13 @@ Node ProofPostprocessCallback::expandMacros(PfRule id, std::vector<Node> sargs = args; // first, compute if we need bool reqWitness = d_wfpm.requiresWitnessFormTransform(children[0], args[0]); + Trace("smt-proof-pp-debug") << "...reqWitness=" << reqWitness << std::endl; // convert both sides, in three steps, take symmetry of second chain for (unsigned r = 0; r < 2; r++) { std::vector<Node> tchildrenr; - // first rewrite args[0], then children[0] - sargs[0] = r == 0 ? args[0] : children[0]; + // first rewrite children[0], then args[0] + sargs[0] = r == 0 ? children[0] : args[0]; // t = apply_SR(t) Node eq = expandMacros(PfRule::MACRO_SR_EQ_INTRO, schildren, sargs, cdp); Trace("smt-proof-pp-debug") @@ -309,10 +334,11 @@ Node ProofPostprocessCallback::expandMacros(PfRule id, << "transform toWitness (" << r << "): " << weq << std::endl; if (addToTransChildren(weq, tchildrenr)) { - sargs[0] = weq[1]; // toWitness(apply_SR(t)) = apply_SR(toWitness(apply_SR(t))) - // rewrite again, don't need substitution - Node weqr = expandMacros(PfRule::MACRO_SR_EQ_INTRO, {}, sargs, cdp); + // rewrite again, don't need substitution. Also, we always use the + // default rewriter, due to the definition of MACRO_SR_PRED_TRANSFORM. + Node weqr = + expandMacros(PfRule::MACRO_SR_EQ_INTRO, {}, {weq[1]}, cdp); Trace("smt-proof-pp-debug") << "transform rewrite_witness (" << r << "): " << weqr << std::endl; addToTransChildren(weqr, tchildrenr); @@ -332,6 +358,8 @@ Node ProofPostprocessCallback::expandMacros(PfRule id, Node eqr = addProofForTrans(tchildrenr, cdp); if (!eqr.isNull()) { + Trace("smt-proof-pp-debug") << "transform connect sym " << tchildren + << " " << eqr << std::endl; // take symmetry of above and add it to the overall chain addToTransChildren(eqr, tchildren, true); } @@ -340,16 +368,10 @@ Node ProofPostprocessCallback::expandMacros(PfRule id, << "transform finish (" << r << ")" << std::endl; } - // children[0] = true - Node eq3 = children[0].eqNode(d_true); - Trace("smt-proof-pp-debug") << "transform true_intro: " << eq3 << std::endl; - cdp->addStep(eq3, PfRule::TRUE_INTRO, {children[0]}, {}); - addToTransChildren(eq3, tchildren); - // apply transitivity if necessary Node eq = addProofForTrans(tchildren, cdp); - cdp->addStep(args[0], PfRule::TRUE_ELIM, {eq}, {}); + cdp->addStep(args[0], PfRule::EQ_RESOLVE, {children[0], eq}, {}); return args[0]; } else if (id == PfRule::SUBS) @@ -383,12 +405,16 @@ Node ProofPostprocessCallback::expandMacros(PfRule id, std::vector<ProofGenerator*> pgs; for (size_t i = 0, nchild = children.size(); i < nchild; i++) { - // process in reverse order - size_t index = nchild - (i + 1); + // 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[index], var, subs, ids); + children[i], var, subs, ids); + Trace("smt-proof-pp-debug") + << "...process " << var << " -> " << subs << " (" << children[i] + << ", " << ids << ")" << std::endl; // apply the current substitution to the range if (!vvec.empty()) { @@ -396,6 +422,9 @@ Node ProofPostprocessCallback::expandMacros(PfRule id, subs.substitute(vvec.begin(), vvec.end(), svec.begin(), svec.end()); if (ss != subs) { + Trace("smt-proof-pp-debug") + << "......updated to " << var << " -> " << ss + << " based on previous substitution" << std::endl; // make the proof for the tranitivity step std::shared_ptr<CDProof> pf = std::make_shared<CDProof>(d_pnm); pfs.push_back(pf); @@ -404,7 +433,8 @@ Node ProofPostprocessCallback::expandMacros(PfRule id, // add previous rewrite steps for (unsigned j = 0, nvars = vvec.size(); j < nvars; j++) { - tcg.addRewriteStep(vvec[j], svec[j], pgs[j]); + // not necessarily closed, so we pass false to addRewriteStep. + tcg.addRewriteStep(vvec[j], svec[j], pgs[j], false); } // get the proof for the update to the current substitution Node seqss = subs.eqNode(ss); @@ -416,7 +446,7 @@ Node ProofPostprocessCallback::expandMacros(PfRule id, pfn = cdp->getProofFor(children[i]); pf->addProof(pfn); // ensure we have a proof of var = subs - Node veqs = addProofForSubsStep(var, subs, children[index], pf.get()); + Node veqs = addProofForSubsStep(var, subs, children[i], pf.get()); // transitivity pf->addStep(var.eqNode(ss), PfRule::TRANS, {veqs, seqss}, {}); // add to the substitution @@ -428,9 +458,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[index] as a Boolean assignment (e.g. - // children[index] = true if we are using MethodId::SB_LITERAL). - addProofForSubsStep(var, subs, children[index], cdp); + // 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); vvec.push_back(var); svec.push_back(subs); pgs.push_back(cdp); @@ -443,14 +473,19 @@ Node ProofPostprocessCallback::expandMacros(PfRule id, TConvProofGenerator tcpg(d_pnm, nullptr, TConvPolicy::ONCE); for (unsigned j = 0, nvars = vvec.size(); j < nvars; j++) { - tcpg.addRewriteStep(vvec[j], svec[j], pgs[j]); + // not necessarily closed, so we pass false to addRewriteStep. + tcpg.addRewriteStep(vvec[j], svec[j], pgs[j], false); } // add the proof constructed by the term conversion utility std::shared_ptr<ProofNode> pfn = tcpg.getProofFor(eq); // should give a proof, if not, then tcpg does not agree with the // substitution. Assert(pfn != nullptr); - if (pfn != nullptr) + if (pfn == nullptr) + { + cdp->addStep(eq, PfRule::TRUST_SUBS, {}, {eq}); + } + else { cdp->addProof(pfn); } @@ -485,10 +520,20 @@ Node ProofPostprocessCallback::expandMacros(PfRule id, // use rewrite with proof interface Rewriter* rr = d_smte->getRewriter(); TrustNode trn = rr->rewriteWithProof(args[0], elimTR, isExtEq); - std::shared_ptr<ProofNode> pfn = - trn.getGenerator()->getProofFor(trn.getProven()); - cdp->addProof(pfn); - Assert(trn.getNode() == ret); + std::shared_ptr<ProofNode> pfn = trn.toProofNode(); + if (pfn == nullptr) + { + // did not have a proof of rewriting, probably isExtEq is true + cdp->addStep(eq, PfRule::TRUST_REWRITE, {}, {eq}); + } + else + { + cdp->addProof(pfn); + } + Assert(trn.getNode() == ret) + << "Unexpected rewrite " << args[0] << std::endl + << "Got: " << trn.getNode() << std::endl + << "Expected: " << ret; } else if (idr == MethodId::RW_EVALUATE) { @@ -661,7 +706,11 @@ bool ProofPostprocessFinalCallback::wasPedanticFailure(std::ostream& out) const ProofPostproccess::ProofPostproccess(ProofNodeManager* pnm, SmtEngine* smte, ProofGenerator* pppg) - : d_cb(pnm, smte, pppg), d_finalCb(pnm), d_pnm(pnm) + : d_pnm(pnm), + d_cb(pnm, smte, pppg), + d_updater(d_pnm, d_cb), + d_finalCb(pnm), + d_finalizer(d_pnm, d_finalCb) { } @@ -673,12 +722,10 @@ void ProofPostproccess::process(std::shared_ptr<ProofNode> pf) // how to process, including how to process assumptions in pf. d_cb.initializeUpdate(); // now, process - ProofNodeUpdater updater(d_pnm, d_cb); - updater.process(pf); + d_updater.process(pf); // take stats and check pedantic d_finalCb.initializeUpdate(); - ProofNodeUpdater finalizer(d_pnm, d_finalCb); - finalizer.process(pf); + d_finalizer.process(pf); std::stringstream serr; bool wasPedanticFailure = d_finalCb.wasPedanticFailure(serr); diff --git a/src/smt/proof_post_processor.h b/src/smt/proof_post_processor.h index b65519c6d..d7186ea74 100644 --- a/src/smt/proof_post_processor.h +++ b/src/smt/proof_post_processor.h @@ -198,14 +198,23 @@ class ProofPostproccess void process(std::shared_ptr<ProofNode> pf); /** set eliminate rule */ void setEliminateRule(PfRule rule); - private: + /** The proof node manager */ + ProofNodeManager* d_pnm; /** The post process callback */ ProofPostprocessCallback d_cb; + /** + * The updater, which is responsible for expanding macros in the final proof + * and connecting preprocessed assumptions to input assumptions. + */ + ProofNodeUpdater d_updater; /** The post process callback for finalization */ ProofPostprocessFinalCallback d_finalCb; - /** The proof node manager */ - ProofNodeManager* d_pnm; + /** + * The finalizer, which is responsible for taking stats and checking for + * (lazy) pedantic failures. + */ + ProofNodeUpdater d_finalizer; }; } // namespace smt diff --git a/src/theory/builtin/proof_checker.cpp b/src/theory/builtin/proof_checker.cpp index 2fb8f611c..1a30f4449 100644 --- a/src/theory/builtin/proof_checker.cpp +++ b/src/theory/builtin/proof_checker.cpp @@ -74,6 +74,8 @@ void BuiltinProofRuleChecker::registerTo(ProofChecker* pc) 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::TRUST_REWRITE, this, 1); + pc->registerTrustedChecker(PfRule::TRUST_SUBS, this, 1); } Node BuiltinProofRuleChecker::applySubstitutionRewrite( @@ -352,7 +354,8 @@ Node BuiltinProofRuleChecker::checkInternal(PfRule id, } else if (id == PfRule::PREPROCESS || id == PfRule::THEORY_PREPROCESS || id == PfRule::WITNESS_AXIOM || id == PfRule::THEORY_LEMMA - || id == PfRule::PREPROCESS_LEMMA || id == PfRule::THEORY_REWRITE) + || id == PfRule::PREPROCESS_LEMMA || id == PfRule::THEORY_REWRITE + || id == PfRule::TRUST_REWRITE || id == PfRule::TRUST_SUBS) { // "trusted" rules Assert(children.empty()); |