}
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)
{
}
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;
}
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);
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);
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])).
<< "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];
}
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")
<< "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);
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);
}
<< "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)
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())
{
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);
// 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);
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
}
// 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);
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);
}
// 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)
{
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)
{
}
// 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);
projects / cvc5.git / commitdiff