1 /********************* */
2 /*! \file proof_post_processor.cpp
4 ** Top contributors (to current version):
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
8 ** in the top-level source directory and their institutional affiliations.
9 ** All rights reserved. See the file COPYING in the top-level source
10 ** directory for licensing information.\endverbatim
12 ** \brief Implementation of module for processing proof nodes
15 #include "smt/proof_post_processor.h"
17 #include "expr/skolem_manager.h"
18 #include "options/smt_options.h"
19 #include "preprocessing/assertion_pipeline.h"
20 #include "smt/smt_engine.h"
21 #include "smt/smt_statistics_registry.h"
22 #include "theory/builtin/proof_checker.h"
23 #include "theory/rewriter.h"
25 using namespace CVC4::kind
;
26 using namespace CVC4::theory
;
31 ProofPostprocessCallback::ProofPostprocessCallback(ProofNodeManager
* pnm
,
34 : d_pnm(pnm
), d_smte(smte
), d_pppg(pppg
), d_wfpm(pnm
)
36 d_true
= NodeManager::currentNM()->mkConst(true);
37 // always check whether to update ASSUME
38 d_elimRules
.insert(PfRule::ASSUME
);
41 void ProofPostprocessCallback::initializeUpdate()
43 d_assumpToProof
.clear();
44 d_wfAssumptions
.clear();
47 void ProofPostprocessCallback::setEliminateRule(PfRule rule
)
49 d_elimRules
.insert(rule
);
52 bool ProofPostprocessCallback::shouldUpdate(std::shared_ptr
<ProofNode
> pn
,
55 return d_elimRules
.find(pn
->getRule()) != d_elimRules
.end();
58 bool ProofPostprocessCallback::update(Node res
,
60 const std::vector
<Node
>& children
,
61 const std::vector
<Node
>& args
,
65 Trace("smt-proof-pp-debug") << "- Post process " << id
<< " " << children
66 << " / " << args
<< std::endl
;
68 if (id
== PfRule::ASSUME
)
70 // we cache based on the assumption node, not the proof node, since there
71 // may be multiple occurrences of the same node.
73 std::shared_ptr
<ProofNode
> pfn
;
74 std::map
<Node
, std::shared_ptr
<ProofNode
>>::iterator it
=
75 d_assumpToProof
.find(f
);
76 if (it
!= d_assumpToProof
.end())
78 Trace("smt-proof-pp-debug") << "...already computed" << std::endl
;
83 Assert(d_pppg
!= nullptr);
84 // get proof from preprocess proof generator
85 pfn
= d_pppg
->getProofFor(f
);
86 // print for debugging
89 Trace("smt-proof-pp-debug")
90 << "...no proof, possibly an input assumption" << std::endl
;
94 Assert(pfn
->getResult() == f
);
95 if (Trace
.isOn("smt-proof-pp"))
98 << "=== Connect proof for preprocessing: " << f
<< std::endl
;
99 Trace("smt-proof-pp") << *pfn
.get() << std::endl
;
102 d_assumpToProof
[f
] = pfn
;
113 Node ret
= expandMacros(id
, children
, args
, cdp
);
114 Trace("smt-proof-pp-debug") << "...expanded = " << !ret
.isNull() << std::endl
;
115 return !ret
.isNull();
118 bool ProofPostprocessCallback::updateInternal(Node res
,
120 const std::vector
<Node
>& children
,
121 const std::vector
<Node
>& args
,
124 bool continueUpdate
= true;
125 return update(res
, id
, children
, args
, cdp
, continueUpdate
);
128 Node
ProofPostprocessCallback::expandMacros(PfRule id
,
129 const std::vector
<Node
>& children
,
130 const std::vector
<Node
>& args
,
133 if (d_elimRules
.find(id
) == d_elimRules
.end())
139 if (id
== PfRule::MACRO_SR_EQ_INTRO
)
142 // (SUBS <children> :args args[0:1])
143 // (REWRITE :args <t.substitute(x1,t1). ... .substitute(xn,tn)> args[2]))
144 std::vector
<Node
> tchildren
;
147 if (!children
.empty())
149 std::vector
<Node
> sargs
;
151 MethodId sid
= MethodId::SB_DEFAULT
;
152 if (args
.size() >= 2)
154 if (builtin::BuiltinProofRuleChecker::getMethodId(args
[1], sid
))
156 sargs
.push_back(args
[1]);
160 builtin::BuiltinProofRuleChecker::applySubstitution(t
, children
, sid
);
163 Node eq
= t
.eqNode(ts
);
164 // apply SUBS proof rule if necessary
165 if (!updateInternal(eq
, PfRule::SUBS
, children
, sargs
, cdp
))
167 // if not elimianted, add as step
168 cdp
->addStep(eq
, PfRule::SUBS
, children
, sargs
);
170 tchildren
.push_back(eq
);
178 std::vector
<Node
> rargs
;
180 MethodId rid
= MethodId::RW_REWRITE
;
181 if (args
.size() >= 3)
183 if (builtin::BuiltinProofRuleChecker::getMethodId(args
[2], rid
))
185 rargs
.push_back(args
[2]);
188 builtin::BuiltinProofRuleChecker
* builtinPfC
=
189 static_cast<builtin::BuiltinProofRuleChecker
*>(
190 d_pnm
->getChecker()->getCheckerFor(PfRule::MACRO_SR_EQ_INTRO
));
191 Node tr
= builtinPfC
->applyRewrite(ts
, rid
);
194 Node eq
= ts
.eqNode(tr
);
195 // apply REWRITE proof rule
196 if (!updateInternal(eq
, PfRule::REWRITE
, {}, rargs
, cdp
))
198 // if not elimianted, add as step
199 cdp
->addStep(eq
, PfRule::REWRITE
, {}, rargs
);
201 tchildren
.push_back(eq
);
205 // typically not necessary, but done to be robust
206 cdp
->addStep(t
.eqNode(tr
), PfRule::REFL
, {}, {t
});
209 // must add TRANS if two step
210 return addProofForTrans(tchildren
, cdp
);
212 else if (id
== PfRule::MACRO_SR_PRED_INTRO
)
214 std::vector
<Node
> tchildren
;
215 std::vector
<Node
> sargs
= args
;
216 // take into account witness form, if necessary
217 if (d_wfpm
.requiresWitnessFormIntro(args
[0]))
219 Node weq
= addProofForWitnessForm(args
[0], cdp
);
220 tchildren
.push_back(weq
);
221 // replace the first argument
226 // ... proof of t = toWitness(t) ...
227 // (MACRO_SR_EQ_INTRO <children> :args (toWitness(t) args[1:]))))
228 // We call the expandMacros method on MACRO_SR_EQ_INTRO, where notice
229 // that this rule application is immediately expanded in the recursive
230 // call and not added to the proof.
231 Node conc
= expandMacros(PfRule::MACRO_SR_EQ_INTRO
, children
, sargs
, cdp
);
232 tchildren
.push_back(conc
);
233 Assert(!conc
.isNull() && conc
.getKind() == EQUAL
&& conc
[0] == sargs
[0]
234 && conc
[1] == d_true
);
235 // transitivity if necessary
236 Node eq
= addProofForTrans(tchildren
, cdp
);
238 cdp
->addStep(eq
[0], PfRule::TRUE_ELIM
, {eq
}, {});
239 Assert(eq
[0] == args
[0]);
242 else if (id
== PfRule::MACRO_SR_PRED_ELIM
)
246 // (SYMM (MACRO_SR_EQ_INTRO children[1:] :args children[0] ++ args))
247 // (TRUE_INTRO children[0])))
248 std::vector
<Node
> schildren(children
.begin() + 1, children
.end());
249 std::vector
<Node
> srargs
;
250 srargs
.push_back(children
[0]);
251 srargs
.insert(srargs
.end(), args
.begin(), args
.end());
252 Node conc
= expandMacros(PfRule::MACRO_SR_EQ_INTRO
, schildren
, srargs
, cdp
);
253 Assert(!conc
.isNull() && conc
.getKind() == EQUAL
&& conc
[0] == children
[0]);
255 Node eq1
= children
[0].eqNode(d_true
);
256 cdp
->addStep(eq1
, PfRule::TRUE_INTRO
, {children
[0]}, {});
258 Node concSym
= conc
[1].eqNode(conc
[0]);
259 Node eq2
= conc
[1].eqNode(d_true
);
260 cdp
->addStep(eq2
, PfRule::TRANS
, {concSym
, eq1
}, {});
262 cdp
->addStep(conc
[1], PfRule::TRUE_ELIM
, {eq2
}, {});
265 else if (id
== PfRule::MACRO_SR_PRED_TRANSFORM
)
269 // (MACRO_SR_EQ_INTRO children[1:] :args <args>)
270 // ... proof of a = wa
271 // (MACRO_SR_EQ_INTRO {} wa)
273 // (MACRO_SR_EQ_INTRO children[1:] :args (children[0] args[1:]))
274 // ... proof of c = wc
275 // (MACRO_SR_EQ_INTRO {} wc))
276 // (TRUE_INTRO children[0])))
278 // wa = toWitness(apply_SR(args[0])) and
279 // wc = toWitness(apply_SR(children[0])).
280 Trace("smt-proof-pp-debug")
281 << "Transform " << children
[0] << " == " << args
[0] << std::endl
;
282 if (CDProof::isSame(children
[0], args
[0]))
287 std::vector
<Node
> tchildren
;
288 std::vector
<Node
> schildren(children
.begin() + 1, children
.end());
289 std::vector
<Node
> sargs
= args
;
290 // first, compute if we need
291 bool reqWitness
= d_wfpm
.requiresWitnessFormTransform(children
[0], args
[0]);
292 // convert both sides, in three steps, take symmetry of second chain
293 for (unsigned r
= 0; r
< 2; r
++)
295 std::vector
<Node
> tchildrenr
;
296 // first rewrite args[0], then children[0]
297 sargs
[0] = r
== 0 ? args
[0] : children
[0];
299 Node eq
= expandMacros(PfRule::MACRO_SR_EQ_INTRO
, schildren
, sargs
, cdp
);
300 Trace("smt-proof-pp-debug")
301 << "transform subs_rewrite (" << r
<< "): " << eq
<< std::endl
;
302 Assert(!eq
.isNull() && eq
.getKind() == EQUAL
&& eq
[0] == sargs
[0]);
303 addToTransChildren(eq
, tchildrenr
);
304 // apply_SR(t) = toWitness(apply_SR(t))
307 Node weq
= addProofForWitnessForm(eq
[1], cdp
);
308 Trace("smt-proof-pp-debug")
309 << "transform toWitness (" << r
<< "): " << weq
<< std::endl
;
310 if (addToTransChildren(weq
, tchildrenr
))
313 // toWitness(apply_SR(t)) = apply_SR(toWitness(apply_SR(t)))
314 // rewrite again, don't need substitution
315 Node weqr
= expandMacros(PfRule::MACRO_SR_EQ_INTRO
, {}, sargs
, cdp
);
316 Trace("smt-proof-pp-debug") << "transform rewrite_witness (" << r
317 << "): " << weqr
<< std::endl
;
318 addToTransChildren(weqr
, tchildrenr
);
321 Trace("smt-proof-pp-debug")
322 << "transform connect (" << r
<< ")" << std::endl
;
323 // add to overall chain
326 // add the current chain to the overall chain
327 tchildren
.insert(tchildren
.end(), tchildrenr
.begin(), tchildrenr
.end());
331 // add the current chain to cdp
332 Node eqr
= addProofForTrans(tchildrenr
, cdp
);
335 // take symmetry of above and add it to the overall chain
336 addToTransChildren(eqr
, tchildren
, true);
339 Trace("smt-proof-pp-debug")
340 << "transform finish (" << r
<< ")" << std::endl
;
343 // children[0] = true
344 Node eq3
= children
[0].eqNode(d_true
);
345 Trace("smt-proof-pp-debug") << "transform true_intro: " << eq3
<< std::endl
;
346 cdp
->addStep(eq3
, PfRule::TRUE_INTRO
, {children
[0]}, {});
347 addToTransChildren(eq3
, tchildren
);
349 // apply transitivity if necessary
350 Node eq
= addProofForTrans(tchildren
, cdp
);
352 cdp
->addStep(args
[0], PfRule::TRUE_ELIM
, {eq
}, {});
355 else if (id
== PfRule::SUBS
)
357 // Notice that a naive way to reconstruct SUBS is to do a term conversion
358 // proof for each substitution.
359 // The proof of f(a) * { a -> g(b) } * { b -> c } = f(g(c)) is:
360 // TRANS( CONG{f}( a=g(b) ), CONG{f}( CONG{g}( b=c ) ) )
361 // Notice that more optimal proofs are possible that do a single traversal
362 // over t. This is done by applying later substitutions to the range of
363 // previous substitutions, until a final simultaneous substitution is
364 // applied to t. For instance, in the above example, we first prove:
366 // by applying the second substitution { b -> c } to the range of the first,
367 // giving us a proof of g(b)=g(c). We then construct the updated proof
369 // TRANS( a=g(b), CONG{g}( b=c ) )
370 // We then apply the substitution { a -> g(c), b -> c } to f(a), to obtain:
371 // CONG{f}( TRANS( a=g(b), CONG{g}( b=c ) ) )
372 // which notice is more compact than the proof above.
374 // get the kind of substitution
375 MethodId ids
= MethodId::SB_DEFAULT
;
376 if (args
.size() >= 2)
378 builtin::BuiltinProofRuleChecker::getMethodId(args
[1], ids
);
380 std::vector
<std::shared_ptr
<CDProof
>> pfs
;
381 std::vector
<Node
> vvec
;
382 std::vector
<Node
> svec
;
383 std::vector
<ProofGenerator
*> pgs
;
384 for (size_t i
= 0, nchild
= children
.size(); i
< nchild
; i
++)
386 // process in reverse order
387 size_t index
= nchild
- (i
+ 1);
388 // get the substitution
390 builtin::BuiltinProofRuleChecker::getSubstitution(
391 children
[index
], var
, subs
, ids
);
392 // apply the current substitution to the range
396 subs
.substitute(vvec
.begin(), vvec
.end(), svec
.begin(), svec
.end());
399 // make the proof for the tranitivity step
400 std::shared_ptr
<CDProof
> pf
= std::make_shared
<CDProof
>(d_pnm
);
402 // prove the updated substitution
403 TConvProofGenerator
tcg(d_pnm
, nullptr, TConvPolicy::ONCE
);
404 // add previous rewrite steps
405 for (unsigned j
= 0, nvars
= vvec
.size(); j
< nvars
; j
++)
407 tcg
.addRewriteStep(vvec
[j
], svec
[j
], pgs
[j
]);
409 // get the proof for the update to the current substitution
410 Node seqss
= subs
.eqNode(ss
);
411 std::shared_ptr
<ProofNode
> pfn
= tcg
.getProofFor(seqss
);
412 Assert(pfn
!= nullptr);
415 // get proof for children[i] from cdp
416 pfn
= cdp
->getProofFor(children
[i
]);
418 // ensure we have a proof of var = subs
419 Node veqs
= addProofForSubsStep(var
, subs
, children
[index
], pf
.get());
421 pf
->addStep(var
.eqNode(ss
), PfRule::TRANS
, {veqs
, seqss
}, {});
422 // add to the substitution
425 pgs
.push_back(pf
.get());
429 // Just use equality from CDProof, but ensure we have a proof in cdp.
430 // This may involve a TRUE_INTRO/FALSE_INTRO if the substitution step
431 // uses the assumption children[index] as a Boolean assignment (e.g.
432 // children[index] = true if we are using MethodId::SB_LITERAL).
433 addProofForSubsStep(var
, subs
, children
[index
], cdp
);
435 svec
.push_back(subs
);
438 Node ts
= t
.substitute(vvec
.begin(), vvec
.end(), svec
.begin(), svec
.end());
439 Node eq
= t
.eqNode(ts
);
442 // should be implied by the substitution now
443 TConvProofGenerator
tcpg(d_pnm
, nullptr, TConvPolicy::ONCE
);
444 for (unsigned j
= 0, nvars
= vvec
.size(); j
< nvars
; j
++)
446 tcpg
.addRewriteStep(vvec
[j
], svec
[j
], pgs
[j
]);
448 // add the proof constructed by the term conversion utility
449 std::shared_ptr
<ProofNode
> pfn
= tcpg
.getProofFor(eq
);
450 // should give a proof, if not, then tcpg does not agree with the
452 Assert(pfn
!= nullptr);
460 // should not be necessary typically
461 cdp
->addStep(eq
, PfRule::REFL
, {}, {t
});
465 else if (id
== PfRule::REWRITE
)
467 // get the kind of rewrite
468 MethodId idr
= MethodId::RW_REWRITE
;
469 if (args
.size() >= 2)
471 builtin::BuiltinProofRuleChecker::getMethodId(args
[1], idr
);
473 builtin::BuiltinProofRuleChecker
* builtinPfC
=
474 static_cast<builtin::BuiltinProofRuleChecker
*>(
475 d_pnm
->getChecker()->getCheckerFor(PfRule::REWRITE
));
476 Node ret
= builtinPfC
->applyRewrite(args
[0], idr
);
477 Node eq
= args
[0].eqNode(ret
);
478 if (idr
== MethodId::RW_REWRITE
|| idr
== MethodId::RW_REWRITE_EQ_EXT
)
480 // rewrites from theory::Rewriter
481 // automatically expand THEORY_REWRITE as well here if set
483 (d_elimRules
.find(PfRule::THEORY_REWRITE
) != d_elimRules
.end());
484 bool isExtEq
= (idr
== MethodId::RW_REWRITE_EQ_EXT
);
485 // use rewrite with proof interface
486 Rewriter
* rr
= d_smte
->getRewriter();
487 TrustNode trn
= rr
->rewriteWithProof(args
[0], elimTR
, isExtEq
);
488 std::shared_ptr
<ProofNode
> pfn
=
489 trn
.getGenerator()->getProofFor(trn
.getProven());
491 Assert(trn
.getNode() == ret
);
493 else if (idr
== MethodId::RW_EVALUATE
)
495 // change to evaluate, which is never eliminated
496 cdp
->addStep(eq
, PfRule::EVALUATE
, {}, {args
[0]});
500 // don't know how to eliminate
505 // should not be necessary typically
506 cdp
->addStep(eq
, PfRule::REFL
, {}, {args
[0]});
511 // TRUST, PREPROCESS, THEORY_LEMMA, THEORY_PREPROCESS?
516 Node
ProofPostprocessCallback::addProofForWitnessForm(Node t
, CDProof
* cdp
)
518 Node tw
= SkolemManager::getWitnessForm(t
);
519 Node eq
= t
.eqNode(tw
);
522 // not necessary, add REFL step
523 cdp
->addStep(eq
, PfRule::REFL
, {}, {t
});
526 std::shared_ptr
<ProofNode
> pn
= d_wfpm
.getProofFor(eq
);
534 Assert(false) << "ProofPostprocessCallback::addProofForWitnessForm: failed "
535 "to add proof for witness form of "
541 Node
ProofPostprocessCallback::addProofForTrans(
542 const std::vector
<Node
>& tchildren
, CDProof
* cdp
)
544 size_t tsize
= tchildren
.size();
547 Node lhs
= tchildren
[0][0];
548 Node rhs
= tchildren
[tsize
- 1][1];
549 Node eq
= lhs
.eqNode(rhs
);
550 cdp
->addStep(eq
, PfRule::TRANS
, tchildren
, {});
560 Node
ProofPostprocessCallback::addProofForSubsStep(Node var
,
565 // ensure we have a proof of var = subs
566 Node veqs
= var
.eqNode(subs
);
569 // should be true intro or false intro
570 Assert(subs
.isConst());
573 subs
.getConst
<bool>() ? PfRule::TRUE_INTRO
: PfRule::FALSE_INTRO
,
580 bool ProofPostprocessCallback::addToTransChildren(Node eq
,
581 std::vector
<Node
>& tchildren
,
584 Assert(!eq
.isNull());
585 Assert(eq
.getKind() == kind::EQUAL
);
590 Node equ
= isSymm
? eq
[1].eqNode(eq
[0]) : eq
;
591 Assert(tchildren
.empty()
592 || (tchildren
[tchildren
.size() - 1].getKind() == kind::EQUAL
593 && tchildren
[tchildren
.size() - 1][1] == equ
[0]));
594 tchildren
.push_back(equ
);
598 ProofPostprocessFinalCallback::ProofPostprocessFinalCallback(
599 ProofNodeManager
* pnm
)
600 : d_ruleCount("finalProof::ruleCount"),
601 d_totalRuleCount("finalProof::totalRuleCount", 0),
603 d_pedanticFailure(false)
605 smtStatisticsRegistry()->registerStat(&d_ruleCount
);
606 smtStatisticsRegistry()->registerStat(&d_totalRuleCount
);
609 ProofPostprocessFinalCallback::~ProofPostprocessFinalCallback()
611 smtStatisticsRegistry()->unregisterStat(&d_ruleCount
);
612 smtStatisticsRegistry()->unregisterStat(&d_totalRuleCount
);
615 void ProofPostprocessFinalCallback::initializeUpdate()
617 d_pedanticFailure
= false;
618 d_pedanticFailureOut
.str("");
621 bool ProofPostprocessFinalCallback::shouldUpdate(std::shared_ptr
<ProofNode
> pn
,
622 bool& continueUpdate
)
624 PfRule r
= pn
->getRule();
625 if (Trace
.isOn("final-pf-hole"))
627 if (r
== PfRule::THEORY_REWRITE
)
629 Trace("final-pf-hole") << "hole: " << r
<< " : " << pn
->getResult()
633 // if not doing eager pedantic checking, fail if below threshold
634 if (!options::proofNewPedanticEager())
636 if (!d_pedanticFailure
)
638 Assert(d_pedanticFailureOut
.str().empty());
639 if (d_pnm
->getChecker()->isPedanticFailure(r
, d_pedanticFailureOut
))
641 d_pedanticFailure
= true;
645 // record stats for the rule
651 bool ProofPostprocessFinalCallback::wasPedanticFailure(std::ostream
& out
) const
653 if (d_pedanticFailure
)
655 out
<< d_pedanticFailureOut
.str();
661 ProofPostproccess::ProofPostproccess(ProofNodeManager
* pnm
,
663 ProofGenerator
* pppg
)
664 : d_cb(pnm
, smte
, pppg
), d_finalCb(pnm
), d_pnm(pnm
)
668 ProofPostproccess::~ProofPostproccess() {}
670 void ProofPostproccess::process(std::shared_ptr
<ProofNode
> pf
)
672 // Initialize the callback, which computes necessary static information about
673 // how to process, including how to process assumptions in pf.
674 d_cb
.initializeUpdate();
676 ProofNodeUpdater
updater(d_pnm
, d_cb
);
678 // take stats and check pedantic
679 d_finalCb
.initializeUpdate();
680 ProofNodeUpdater
finalizer(d_pnm
, d_finalCb
);
681 finalizer
.process(pf
);
683 std::stringstream serr
;
684 bool wasPedanticFailure
= d_finalCb
.wasPedanticFailure(serr
);
685 if (wasPedanticFailure
)
687 AlwaysAssert(!wasPedanticFailure
)
688 << "ProofPostproccess::process: pedantic failure:" << std::endl
693 void ProofPostproccess::setEliminateRule(PfRule rule
)
695 d_cb
.setEliminateRule(rule
);