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(ProofNode
* pn
)
54 return d_elimRules
.find(pn
->getRule()) != d_elimRules
.end();
57 bool ProofPostprocessCallback::update(Node res
,
59 const std::vector
<Node
>& children
,
60 const std::vector
<Node
>& args
,
64 Trace("smt-proof-pp-debug") << "- Post process " << id
<< " " << children
65 << " / " << args
<< std::endl
;
67 if (id
== PfRule::ASSUME
)
69 // we cache based on the assumption node, not the proof node, since there
70 // may be multiple occurrences of the same node.
72 std::shared_ptr
<ProofNode
> pfn
;
73 std::map
<Node
, std::shared_ptr
<ProofNode
>>::iterator it
=
74 d_assumpToProof
.find(f
);
75 if (it
!= d_assumpToProof
.end())
77 Trace("smt-proof-pp-debug") << "...already computed" << std::endl
;
82 Assert(d_pppg
!= nullptr);
83 // get proof from preprocess proof generator
84 pfn
= d_pppg
->getProofFor(f
);
85 // print for debugging
88 Trace("smt-proof-pp-debug")
89 << "...no proof, possibly an input assumption" << std::endl
;
93 Assert(pfn
->getResult() == f
);
94 if (Trace
.isOn("smt-proof-pp"))
97 << "=== Connect proof for preprocessing: " << f
<< std::endl
;
98 Trace("smt-proof-pp") << *pfn
.get() << std::endl
;
101 d_assumpToProof
[f
] = pfn
;
112 Node ret
= expandMacros(id
, children
, args
, cdp
);
113 Trace("smt-proof-pp-debug") << "...expanded = " << !ret
.isNull() << std::endl
;
114 return !ret
.isNull();
117 bool ProofPostprocessCallback::updateInternal(Node res
,
119 const std::vector
<Node
>& children
,
120 const std::vector
<Node
>& args
,
123 bool continueUpdate
= true;
124 return update(res
, id
, children
, args
, cdp
, continueUpdate
);
127 Node
ProofPostprocessCallback::expandMacros(PfRule id
,
128 const std::vector
<Node
>& children
,
129 const std::vector
<Node
>& args
,
132 if (d_elimRules
.find(id
) == d_elimRules
.end())
138 if (id
== PfRule::MACRO_SR_EQ_INTRO
)
141 // (SUBS <children> :args args[0:1])
142 // (REWRITE :args <t.substitute(x1,t1). ... .substitute(xn,tn)> args[2]))
143 std::vector
<Node
> tchildren
;
146 if (!children
.empty())
148 std::vector
<Node
> sargs
;
150 MethodId sid
= MethodId::SB_DEFAULT
;
151 if (args
.size() >= 2)
153 if (builtin::BuiltinProofRuleChecker::getMethodId(args
[1], sid
))
155 sargs
.push_back(args
[1]);
159 builtin::BuiltinProofRuleChecker::applySubstitution(t
, children
, sid
);
162 Node eq
= t
.eqNode(ts
);
163 // apply SUBS proof rule if necessary
164 if (!updateInternal(eq
, PfRule::SUBS
, children
, sargs
, cdp
))
166 // if not elimianted, add as step
167 cdp
->addStep(eq
, PfRule::SUBS
, children
, sargs
);
169 tchildren
.push_back(eq
);
177 std::vector
<Node
> rargs
;
179 MethodId rid
= MethodId::RW_REWRITE
;
180 if (args
.size() >= 3)
182 if (builtin::BuiltinProofRuleChecker::getMethodId(args
[2], rid
))
184 rargs
.push_back(args
[2]);
187 builtin::BuiltinProofRuleChecker
* builtinPfC
=
188 static_cast<builtin::BuiltinProofRuleChecker
*>(
189 d_pnm
->getChecker()->getCheckerFor(PfRule::MACRO_SR_EQ_INTRO
));
190 Node tr
= builtinPfC
->applyRewrite(ts
, rid
);
193 Node eq
= ts
.eqNode(tr
);
194 // apply REWRITE proof rule
195 if (!updateInternal(eq
, PfRule::REWRITE
, {}, rargs
, cdp
))
197 // if not elimianted, add as step
198 cdp
->addStep(eq
, PfRule::REWRITE
, {}, rargs
);
200 tchildren
.push_back(eq
);
204 // typically not necessary, but done to be robust
205 cdp
->addStep(t
.eqNode(tr
), PfRule::REFL
, {}, {t
});
208 // must add TRANS if two step
209 return addProofForTrans(tchildren
, cdp
);
211 else if (id
== PfRule::MACRO_SR_PRED_INTRO
)
213 std::vector
<Node
> tchildren
;
214 std::vector
<Node
> sargs
= args
;
215 // take into account witness form, if necessary
216 if (d_wfpm
.requiresWitnessFormIntro(args
[0]))
218 Node weq
= addProofForWitnessForm(args
[0], cdp
);
219 tchildren
.push_back(weq
);
220 // replace the first argument
225 // ... proof of t = toWitness(t) ...
226 // (MACRO_SR_EQ_INTRO <children> :args (toWitness(t) args[1:]))))
227 // We call the expandMacros method on MACRO_SR_EQ_INTRO, where notice
228 // that this rule application is immediately expanded in the recursive
229 // call and not added to the proof.
230 Node conc
= expandMacros(PfRule::MACRO_SR_EQ_INTRO
, children
, sargs
, cdp
);
231 tchildren
.push_back(conc
);
232 Assert(!conc
.isNull() && conc
.getKind() == EQUAL
&& conc
[0] == sargs
[0]
233 && conc
[1] == d_true
);
234 // transitivity if necessary
235 Node eq
= addProofForTrans(tchildren
, cdp
);
237 cdp
->addStep(eq
[0], PfRule::TRUE_ELIM
, {eq
}, {});
238 Assert(eq
[0] == args
[0]);
241 else if (id
== PfRule::MACRO_SR_PRED_ELIM
)
245 // (SYMM (MACRO_SR_EQ_INTRO children[1:] :args children[0] ++ args))
246 // (TRUE_INTRO children[0])))
247 std::vector
<Node
> schildren(children
.begin() + 1, children
.end());
248 std::vector
<Node
> srargs
;
249 srargs
.push_back(children
[0]);
250 srargs
.insert(srargs
.end(), args
.begin(), args
.end());
251 Node conc
= expandMacros(PfRule::MACRO_SR_EQ_INTRO
, schildren
, srargs
, cdp
);
252 Assert(!conc
.isNull() && conc
.getKind() == EQUAL
&& conc
[0] == children
[0]);
254 Node eq1
= children
[0].eqNode(d_true
);
255 cdp
->addStep(eq1
, PfRule::TRUE_INTRO
, {children
[0]}, {});
257 Node concSym
= conc
[1].eqNode(conc
[0]);
258 Node eq2
= conc
[1].eqNode(d_true
);
259 cdp
->addStep(eq2
, PfRule::TRANS
, {concSym
, eq1
}, {});
261 cdp
->addStep(conc
[1], PfRule::TRUE_ELIM
, {eq2
}, {});
264 else if (id
== PfRule::MACRO_SR_PRED_TRANSFORM
)
268 // (MACRO_SR_EQ_INTRO children[1:] :args <args>)
269 // ... proof of a = wa
270 // (MACRO_SR_EQ_INTRO {} wa)
272 // (MACRO_SR_EQ_INTRO children[1:] :args (children[0] args[1:]))
273 // ... proof of c = wc
274 // (MACRO_SR_EQ_INTRO {} wc))
275 // (TRUE_INTRO children[0])))
277 // wa = toWitness(apply_SR(args[0])) and
278 // wc = toWitness(apply_SR(children[0])).
279 Trace("smt-proof-pp-debug")
280 << "Transform " << children
[0] << " == " << args
[0] << std::endl
;
281 if (CDProof::isSame(children
[0], args
[0]))
286 std::vector
<Node
> tchildren
;
287 std::vector
<Node
> schildren(children
.begin() + 1, children
.end());
288 std::vector
<Node
> sargs
= args
;
289 // first, compute if we need
290 bool reqWitness
= d_wfpm
.requiresWitnessFormTransform(children
[0], args
[0]);
291 // convert both sides, in three steps, take symmetry of second chain
292 for (unsigned r
= 0; r
< 2; r
++)
294 std::vector
<Node
> tchildrenr
;
295 // first rewrite args[0], then children[0]
296 sargs
[0] = r
== 0 ? args
[0] : children
[0];
298 Node eq
= expandMacros(PfRule::MACRO_SR_EQ_INTRO
, schildren
, sargs
, cdp
);
299 Trace("smt-proof-pp-debug")
300 << "transform subs_rewrite (" << r
<< "): " << eq
<< std::endl
;
301 Assert(!eq
.isNull() && eq
.getKind() == EQUAL
&& eq
[0] == sargs
[0]);
302 addToTransChildren(eq
, tchildrenr
);
303 // apply_SR(t) = toWitness(apply_SR(t))
306 Node weq
= addProofForWitnessForm(eq
[1], cdp
);
307 Trace("smt-proof-pp-debug")
308 << "transform toWitness (" << r
<< "): " << weq
<< std::endl
;
309 if (addToTransChildren(weq
, tchildrenr
))
312 // toWitness(apply_SR(t)) = apply_SR(toWitness(apply_SR(t)))
313 // rewrite again, don't need substitution
314 Node weqr
= expandMacros(PfRule::MACRO_SR_EQ_INTRO
, {}, sargs
, cdp
);
315 Trace("smt-proof-pp-debug") << "transform rewrite_witness (" << r
316 << "): " << weqr
<< std::endl
;
317 addToTransChildren(weqr
, tchildrenr
);
320 Trace("smt-proof-pp-debug")
321 << "transform connect (" << r
<< ")" << std::endl
;
322 // add to overall chain
325 // add the current chain to the overall chain
326 tchildren
.insert(tchildren
.end(), tchildrenr
.begin(), tchildrenr
.end());
330 // add the current chain to cdp
331 Node eqr
= addProofForTrans(tchildrenr
, cdp
);
334 // take symmetry of above and add it to the overall chain
335 addToTransChildren(eqr
, tchildren
, true);
338 Trace("smt-proof-pp-debug")
339 << "transform finish (" << r
<< ")" << std::endl
;
342 // children[0] = true
343 Node eq3
= children
[0].eqNode(d_true
);
344 Trace("smt-proof-pp-debug") << "transform true_intro: " << eq3
<< std::endl
;
345 cdp
->addStep(eq3
, PfRule::TRUE_INTRO
, {children
[0]}, {});
346 addToTransChildren(eq3
, tchildren
);
348 // apply transitivity if necessary
349 Node eq
= addProofForTrans(tchildren
, cdp
);
351 cdp
->addStep(args
[0], PfRule::TRUE_ELIM
, {eq
}, {});
354 else if (id
== PfRule::SUBS
)
356 // Notice that a naive way to reconstruct SUBS is to do a term conversion
357 // proof for each substitution.
358 // The proof of f(a) * { a -> g(b) } * { b -> c } = f(g(c)) is:
359 // TRANS( CONG{f}( a=g(b) ), CONG{f}( CONG{g}( b=c ) ) )
360 // Notice that more optimal proofs are possible that do a single traversal
361 // over t. This is done by applying later substitutions to the range of
362 // previous substitutions, until a final simultaneous substitution is
363 // applied to t. For instance, in the above example, we first prove:
365 // by applying the second substitution { b -> c } to the range of the first,
366 // giving us a proof of g(b)=g(c). We then construct the updated proof
368 // TRANS( a=g(b), CONG{g}( b=c ) )
369 // We then apply the substitution { a -> g(c), b -> c } to f(a), to obtain:
370 // CONG{f}( TRANS( a=g(b), CONG{g}( b=c ) ) )
371 // which notice is more compact than the proof above.
373 // get the kind of substitution
374 MethodId ids
= MethodId::SB_DEFAULT
;
375 if (args
.size() >= 2)
377 builtin::BuiltinProofRuleChecker::getMethodId(args
[1], ids
);
379 std::vector
<std::shared_ptr
<CDProof
>> pfs
;
380 std::vector
<Node
> vvec
;
381 std::vector
<Node
> svec
;
382 std::vector
<ProofGenerator
*> pgs
;
383 for (size_t i
= 0, nchild
= children
.size(); i
< nchild
; i
++)
385 // process in reverse order
386 size_t index
= nchild
- (i
+ 1);
387 // get the substitution
389 builtin::BuiltinProofRuleChecker::getSubstitution(
390 children
[index
], var
, subs
, ids
);
391 // apply the current substitution to the range
395 subs
.substitute(vvec
.begin(), vvec
.end(), svec
.begin(), svec
.end());
398 // make the proof for the tranitivity step
399 std::shared_ptr
<CDProof
> pf
= std::make_shared
<CDProof
>(d_pnm
);
401 // prove the updated substitution
402 TConvProofGenerator
tcg(d_pnm
, nullptr, TConvPolicy::ONCE
);
403 // add previous rewrite steps
404 for (unsigned j
= 0, nvars
= vvec
.size(); j
< nvars
; j
++)
406 tcg
.addRewriteStep(vvec
[j
], svec
[j
], pgs
[j
]);
408 // get the proof for the update to the current substitution
409 Node seqss
= subs
.eqNode(ss
);
410 std::shared_ptr
<ProofNode
> pfn
= tcg
.getProofFor(seqss
);
411 Assert(pfn
!= nullptr);
414 // get proof for children[i] from cdp
415 pfn
= cdp
->getProofFor(children
[i
]);
417 // ensure we have a proof of var = subs
418 Node veqs
= addProofForSubsStep(var
, subs
, children
[index
], pf
.get());
420 pf
->addStep(var
.eqNode(ss
), PfRule::TRANS
, {veqs
, seqss
}, {});
421 // add to the substitution
424 pgs
.push_back(pf
.get());
428 // Just use equality from CDProof, but ensure we have a proof in cdp.
429 // This may involve a TRUE_INTRO/FALSE_INTRO if the substitution step
430 // uses the assumption children[index] as a Boolean assignment (e.g.
431 // children[index] = true if we are using MethodId::SB_LITERAL).
432 addProofForSubsStep(var
, subs
, children
[index
], cdp
);
434 svec
.push_back(subs
);
437 Node ts
= t
.substitute(vvec
.begin(), vvec
.end(), svec
.begin(), svec
.end());
438 Node eq
= t
.eqNode(ts
);
441 // should be implied by the substitution now
442 TConvProofGenerator
tcpg(d_pnm
, nullptr, TConvPolicy::ONCE
);
443 for (unsigned j
= 0, nvars
= vvec
.size(); j
< nvars
; j
++)
445 tcpg
.addRewriteStep(vvec
[j
], svec
[j
], pgs
[j
]);
447 // add the proof constructed by the term conversion utility
448 std::shared_ptr
<ProofNode
> pfn
= tcpg
.getProofFor(eq
);
449 // should give a proof, if not, then tcpg does not agree with the
451 Assert(pfn
!= nullptr);
459 // should not be necessary typically
460 cdp
->addStep(eq
, PfRule::REFL
, {}, {t
});
464 else if (id
== PfRule::REWRITE
)
466 // get the kind of rewrite
467 MethodId idr
= MethodId::RW_REWRITE
;
468 if (args
.size() >= 2)
470 builtin::BuiltinProofRuleChecker::getMethodId(args
[1], idr
);
472 builtin::BuiltinProofRuleChecker
* builtinPfC
=
473 static_cast<builtin::BuiltinProofRuleChecker
*>(
474 d_pnm
->getChecker()->getCheckerFor(PfRule::REWRITE
));
475 Node ret
= builtinPfC
->applyRewrite(args
[0], idr
);
476 Node eq
= args
[0].eqNode(ret
);
477 if (idr
== MethodId::RW_REWRITE
|| idr
== MethodId::RW_REWRITE_EQ_EXT
)
479 // rewrites from theory::Rewriter
480 // automatically expand THEORY_REWRITE as well here if set
482 (d_elimRules
.find(PfRule::THEORY_REWRITE
) != d_elimRules
.end());
483 bool isExtEq
= (idr
== MethodId::RW_REWRITE_EQ_EXT
);
484 // use rewrite with proof interface
485 Rewriter
* rr
= d_smte
->getRewriter();
486 TrustNode trn
= rr
->rewriteWithProof(args
[0], elimTR
, isExtEq
);
487 std::shared_ptr
<ProofNode
> pfn
=
488 trn
.getGenerator()->getProofFor(trn
.getProven());
490 Assert(trn
.getNode() == ret
);
492 else if (idr
== MethodId::RW_EVALUATE
)
494 // change to evaluate, which is never eliminated
495 cdp
->addStep(eq
, PfRule::EVALUATE
, {}, {args
[0]});
499 // don't know how to eliminate
504 // should not be necessary typically
505 cdp
->addStep(eq
, PfRule::REFL
, {}, {args
[0]});
510 // TRUST, PREPROCESS, THEORY_LEMMA, THEORY_PREPROCESS?
515 Node
ProofPostprocessCallback::addProofForWitnessForm(Node t
, CDProof
* cdp
)
517 Node tw
= SkolemManager::getWitnessForm(t
);
518 Node eq
= t
.eqNode(tw
);
521 // not necessary, add REFL step
522 cdp
->addStep(eq
, PfRule::REFL
, {}, {t
});
525 std::shared_ptr
<ProofNode
> pn
= d_wfpm
.getProofFor(eq
);
533 Assert(false) << "ProofPostprocessCallback::addProofForWitnessForm: failed "
534 "to add proof for witness form of "
540 Node
ProofPostprocessCallback::addProofForTrans(
541 const std::vector
<Node
>& tchildren
, CDProof
* cdp
)
543 size_t tsize
= tchildren
.size();
546 Node lhs
= tchildren
[0][0];
547 Node rhs
= tchildren
[tsize
- 1][1];
548 Node eq
= lhs
.eqNode(rhs
);
549 cdp
->addStep(eq
, PfRule::TRANS
, tchildren
, {});
559 Node
ProofPostprocessCallback::addProofForSubsStep(Node var
,
564 // ensure we have a proof of var = subs
565 Node veqs
= var
.eqNode(subs
);
568 // should be true intro or false intro
569 Assert(subs
.isConst());
572 subs
.getConst
<bool>() ? PfRule::TRUE_INTRO
: PfRule::FALSE_INTRO
,
579 bool ProofPostprocessCallback::addToTransChildren(Node eq
,
580 std::vector
<Node
>& tchildren
,
583 Assert(!eq
.isNull());
584 Assert(eq
.getKind() == kind::EQUAL
);
589 Node equ
= isSymm
? eq
[1].eqNode(eq
[0]) : eq
;
590 Assert(tchildren
.empty()
591 || (tchildren
[tchildren
.size() - 1].getKind() == kind::EQUAL
592 && tchildren
[tchildren
.size() - 1][1] == equ
[0]));
593 tchildren
.push_back(equ
);
597 ProofPostprocessFinalCallback::ProofPostprocessFinalCallback(
598 ProofNodeManager
* pnm
)
599 : d_ruleCount("finalProof::ruleCount"),
600 d_totalRuleCount("finalProof::totalRuleCount", 0),
602 d_pedanticFailure(false)
604 smtStatisticsRegistry()->registerStat(&d_ruleCount
);
605 smtStatisticsRegistry()->registerStat(&d_totalRuleCount
);
608 ProofPostprocessFinalCallback::~ProofPostprocessFinalCallback()
610 smtStatisticsRegistry()->unregisterStat(&d_ruleCount
);
611 smtStatisticsRegistry()->unregisterStat(&d_totalRuleCount
);
614 void ProofPostprocessFinalCallback::initializeUpdate()
616 d_pedanticFailure
= false;
617 d_pedanticFailureOut
.str("");
620 bool ProofPostprocessFinalCallback::shouldUpdate(ProofNode
* pn
)
622 PfRule r
= pn
->getRule();
623 if (Trace
.isOn("final-pf-hole"))
625 if (r
== PfRule::THEORY_REWRITE
)
627 Trace("final-pf-hole") << "hole: " << r
<< " : " << pn
->getResult()
631 // if not doing eager pedantic checking, fail if below threshold
632 if (!options::proofNewPedanticEager())
634 if (!d_pedanticFailure
)
636 Assert(d_pedanticFailureOut
.str().empty());
637 if (d_pnm
->getChecker()->isPedanticFailure(r
, d_pedanticFailureOut
))
639 d_pedanticFailure
= true;
643 // record stats for the rule
649 bool ProofPostprocessFinalCallback::wasPedanticFailure(std::ostream
& out
) const
651 if (d_pedanticFailure
)
653 out
<< d_pedanticFailureOut
.str();
659 ProofPostproccess::ProofPostproccess(ProofNodeManager
* pnm
,
661 ProofGenerator
* pppg
)
662 : d_cb(pnm
, smte
, pppg
), d_finalCb(pnm
), d_pnm(pnm
)
666 ProofPostproccess::~ProofPostproccess() {}
668 void ProofPostproccess::process(std::shared_ptr
<ProofNode
> pf
)
670 // Initialize the callback, which computes necessary static information about
671 // how to process, including how to process assumptions in pf.
672 d_cb
.initializeUpdate();
674 ProofNodeUpdater
updater(d_pnm
, d_cb
);
676 // take stats and check pedantic
677 d_finalCb
.initializeUpdate();
678 ProofNodeUpdater
finalizer(d_pnm
, d_finalCb
);
679 finalizer
.process(pf
);
681 std::stringstream serr
;
682 bool wasPedanticFailure
= d_finalCb
.wasPedanticFailure(serr
);
683 if (wasPedanticFailure
)
685 AlwaysAssert(!wasPedanticFailure
)
686 << "ProofPostproccess::process: pedantic failure:" << std::endl
691 void ProofPostproccess::setEliminateRule(PfRule rule
)
693 d_cb
.setEliminateRule(rule
);