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 Trace("smt-proof-pp-debug") << "...get proof" << std::endl
;
84 Assert(d_pppg
!= nullptr);
85 // get proof from preprocess proof generator
86 pfn
= d_pppg
->getProofFor(f
);
87 Trace("smt-proof-pp-debug") << "...finished get proof" << std::endl
;
88 // print for debugging
91 Trace("smt-proof-pp-debug")
92 << "...no proof, possibly an input assumption" << std::endl
;
96 Assert(pfn
->getResult() == f
);
97 if (Trace
.isOn("smt-proof-pp"))
100 << "=== Connect proof for preprocessing: " << f
<< std::endl
;
101 Trace("smt-proof-pp") << *pfn
.get() << std::endl
;
104 d_assumpToProof
[f
] = pfn
;
106 if (pfn
== nullptr || pfn
->getRule() == PfRule::ASSUME
)
108 Trace("smt-proof-pp-debug") << "...do not add proof" << std::endl
;
112 Trace("smt-proof-pp-debug") << "...add proof" << std::endl
;
117 Node ret
= expandMacros(id
, children
, args
, cdp
);
118 Trace("smt-proof-pp-debug") << "...expanded = " << !ret
.isNull() << std::endl
;
119 return !ret
.isNull();
122 bool ProofPostprocessCallback::updateInternal(Node res
,
124 const std::vector
<Node
>& children
,
125 const std::vector
<Node
>& args
,
128 bool continueUpdate
= true;
129 return update(res
, id
, children
, args
, cdp
, continueUpdate
);
132 Node
ProofPostprocessCallback::expandMacros(PfRule id
,
133 const std::vector
<Node
>& children
,
134 const std::vector
<Node
>& args
,
137 if (d_elimRules
.find(id
) == d_elimRules
.end())
143 if (id
== PfRule::MACRO_SR_EQ_INTRO
)
146 // (SUBS <children> :args args[0:1])
147 // (REWRITE :args <t.substitute(x1,t1). ... .substitute(xn,tn)> args[2]))
148 std::vector
<Node
> tchildren
;
151 if (!children
.empty())
153 std::vector
<Node
> sargs
;
155 MethodId sid
= MethodId::SB_DEFAULT
;
156 if (args
.size() >= 2)
158 if (builtin::BuiltinProofRuleChecker::getMethodId(args
[1], sid
))
160 sargs
.push_back(args
[1]);
164 builtin::BuiltinProofRuleChecker::applySubstitution(t
, children
, sid
);
165 Trace("smt-proof-pp-debug")
166 << "...eq intro subs equality is " << t
<< " == " << ts
<< ", from "
170 Node eq
= t
.eqNode(ts
);
171 // apply SUBS proof rule if necessary
172 if (!updateInternal(eq
, PfRule::SUBS
, children
, sargs
, cdp
))
174 // if we specified that we did not want to eliminate, add as step
175 cdp
->addStep(eq
, PfRule::SUBS
, children
, sargs
);
177 tchildren
.push_back(eq
);
185 std::vector
<Node
> rargs
;
187 MethodId rid
= MethodId::RW_REWRITE
;
188 if (args
.size() >= 3)
190 if (builtin::BuiltinProofRuleChecker::getMethodId(args
[2], rid
))
192 rargs
.push_back(args
[2]);
195 builtin::BuiltinProofRuleChecker
* builtinPfC
=
196 static_cast<builtin::BuiltinProofRuleChecker
*>(
197 d_pnm
->getChecker()->getCheckerFor(PfRule::MACRO_SR_EQ_INTRO
));
198 Node tr
= builtinPfC
->applyRewrite(ts
, rid
);
199 Trace("smt-proof-pp-debug")
200 << "...eq intro rewrite equality is " << ts
<< " == " << tr
<< ", from "
204 Node eq
= ts
.eqNode(tr
);
205 // apply REWRITE proof rule
206 if (!updateInternal(eq
, PfRule::REWRITE
, {}, rargs
, cdp
))
208 // if not elimianted, add as step
209 cdp
->addStep(eq
, PfRule::REWRITE
, {}, rargs
);
211 tchildren
.push_back(eq
);
215 // typically not necessary, but done to be robust
216 cdp
->addStep(t
.eqNode(tr
), PfRule::REFL
, {}, {t
});
219 // must add TRANS if two step
220 return addProofForTrans(tchildren
, cdp
);
222 else if (id
== PfRule::MACRO_SR_PRED_INTRO
)
224 std::vector
<Node
> tchildren
;
225 std::vector
<Node
> sargs
= args
;
226 // take into account witness form, if necessary
227 bool reqWitness
= d_wfpm
.requiresWitnessFormIntro(args
[0]);
228 Trace("smt-proof-pp-debug")
229 << "...pred intro reqWitness=" << reqWitness
<< std::endl
;
232 // (MACRO_SR_EQ_INTRO <children> :args (t args[1:]))
233 // ... proof of apply_SR(t) = toWitness(apply_SR(t)) ...
234 // (MACRO_SR_EQ_INTRO {} {toWitness(apply_SR(t))})
236 // Notice this is an optimized, one sided version of the expansion of
237 // MACRO_SR_PRED_TRANSFORM below.
238 // We call the expandMacros method on MACRO_SR_EQ_INTRO, where notice
239 // that this rule application is immediately expanded in the recursive
240 // call and not added to the proof.
241 Node conc
= expandMacros(PfRule::MACRO_SR_EQ_INTRO
, children
, sargs
, cdp
);
242 Trace("smt-proof-pp-debug")
243 << "...pred intro conclusion is " << conc
<< std::endl
;
244 Assert(!conc
.isNull());
245 Assert(conc
.getKind() == EQUAL
);
246 Assert(conc
[0] == args
[0]);
247 tchildren
.push_back(conc
);
250 Node weq
= addProofForWitnessForm(conc
[1], cdp
);
251 Trace("smt-proof-pp-debug") << "...weq is " << weq
<< std::endl
;
252 if (addToTransChildren(weq
, tchildren
))
254 // toWitness(apply_SR(t)) = apply_SR(toWitness(apply_SR(t)))
255 // rewrite again, don't need substitution. Also we always use the
256 // default rewriter, due to the definition of MACRO_SR_PRED_INTRO.
257 Node weqr
= expandMacros(PfRule::MACRO_SR_EQ_INTRO
, {}, {weq
[1]}, cdp
);
258 addToTransChildren(weqr
, tchildren
);
261 // apply transitivity if necessary
262 Node eq
= addProofForTrans(tchildren
, cdp
);
263 Assert(!eq
.isNull());
264 Assert(eq
.getKind() == EQUAL
);
265 Assert(eq
[0] == args
[0]);
266 Assert(eq
[1] == d_true
);
268 cdp
->addStep(eq
[0], PfRule::TRUE_ELIM
, {eq
}, {});
271 else if (id
== PfRule::MACRO_SR_PRED_ELIM
)
275 // (MACRO_SR_EQ_INTRO children[1:] :args children[0] ++ args))
276 std::vector
<Node
> schildren(children
.begin() + 1, children
.end());
277 std::vector
<Node
> srargs
;
278 srargs
.push_back(children
[0]);
279 srargs
.insert(srargs
.end(), args
.begin(), args
.end());
280 Node conc
= expandMacros(PfRule::MACRO_SR_EQ_INTRO
, schildren
, srargs
, cdp
);
281 Assert(!conc
.isNull());
282 Assert(conc
.getKind() == EQUAL
);
283 Assert(conc
[0] == children
[0]);
284 // apply equality resolve
285 cdp
->addStep(conc
[1], PfRule::EQ_RESOLVE
, {children
[0], conc
}, {});
288 else if (id
== PfRule::MACRO_SR_PRED_TRANSFORM
)
293 // (MACRO_SR_EQ_INTRO children[1:] :args (children[0] args[1:]))
294 // ... proof of c = wc
295 // (MACRO_SR_EQ_INTRO {} wc)
297 // (MACRO_SR_EQ_INTRO children[1:] :args <args>)
298 // ... proof of a = wa
299 // (MACRO_SR_EQ_INTRO {} wa))))
301 // wa = toWitness(apply_SR(args[0])) and
302 // wc = toWitness(apply_SR(children[0])).
303 Trace("smt-proof-pp-debug")
304 << "Transform " << children
[0] << " == " << args
[0] << std::endl
;
305 if (CDProof::isSame(children
[0], args
[0]))
307 Trace("smt-proof-pp-debug") << "...nothing to do" << std::endl
;
311 std::vector
<Node
> tchildren
;
312 std::vector
<Node
> schildren(children
.begin() + 1, children
.end());
313 std::vector
<Node
> sargs
= args
;
314 // first, compute if we need
315 bool reqWitness
= d_wfpm
.requiresWitnessFormTransform(children
[0], args
[0]);
316 Trace("smt-proof-pp-debug") << "...reqWitness=" << reqWitness
<< std::endl
;
317 // convert both sides, in three steps, take symmetry of second chain
318 for (unsigned r
= 0; r
< 2; r
++)
320 std::vector
<Node
> tchildrenr
;
321 // first rewrite children[0], then args[0]
322 sargs
[0] = r
== 0 ? children
[0] : args
[0];
324 Node eq
= expandMacros(PfRule::MACRO_SR_EQ_INTRO
, schildren
, sargs
, cdp
);
325 Trace("smt-proof-pp-debug")
326 << "transform subs_rewrite (" << r
<< "): " << eq
<< std::endl
;
327 Assert(!eq
.isNull() && eq
.getKind() == EQUAL
&& eq
[0] == sargs
[0]);
328 addToTransChildren(eq
, tchildrenr
);
329 // apply_SR(t) = toWitness(apply_SR(t))
332 Node weq
= addProofForWitnessForm(eq
[1], cdp
);
333 Trace("smt-proof-pp-debug")
334 << "transform toWitness (" << r
<< "): " << weq
<< std::endl
;
335 if (addToTransChildren(weq
, tchildrenr
))
337 // toWitness(apply_SR(t)) = apply_SR(toWitness(apply_SR(t)))
338 // rewrite again, don't need substitution. Also, we always use the
339 // default rewriter, due to the definition of MACRO_SR_PRED_TRANSFORM.
341 expandMacros(PfRule::MACRO_SR_EQ_INTRO
, {}, {weq
[1]}, cdp
);
342 Trace("smt-proof-pp-debug") << "transform rewrite_witness (" << r
343 << "): " << weqr
<< std::endl
;
344 addToTransChildren(weqr
, tchildrenr
);
347 Trace("smt-proof-pp-debug")
348 << "transform connect (" << r
<< ")" << std::endl
;
349 // add to overall chain
352 // add the current chain to the overall chain
353 tchildren
.insert(tchildren
.end(), tchildrenr
.begin(), tchildrenr
.end());
357 // add the current chain to cdp
358 Node eqr
= addProofForTrans(tchildrenr
, cdp
);
361 Trace("smt-proof-pp-debug") << "transform connect sym " << tchildren
362 << " " << eqr
<< std::endl
;
363 // take symmetry of above and add it to the overall chain
364 addToTransChildren(eqr
, tchildren
, true);
367 Trace("smt-proof-pp-debug")
368 << "transform finish (" << r
<< ")" << std::endl
;
371 // apply transitivity if necessary
372 Node eq
= addProofForTrans(tchildren
, cdp
);
374 cdp
->addStep(args
[0], PfRule::EQ_RESOLVE
, {children
[0], eq
}, {});
377 else if (id
== PfRule::SUBS
)
379 // Notice that a naive way to reconstruct SUBS is to do a term conversion
380 // proof for each substitution.
381 // The proof of f(a) * { a -> g(b) } * { b -> c } = f(g(c)) is:
382 // TRANS( CONG{f}( a=g(b) ), CONG{f}( CONG{g}( b=c ) ) )
383 // Notice that more optimal proofs are possible that do a single traversal
384 // over t. This is done by applying later substitutions to the range of
385 // previous substitutions, until a final simultaneous substitution is
386 // applied to t. For instance, in the above example, we first prove:
388 // by applying the second substitution { b -> c } to the range of the first,
389 // giving us a proof of g(b)=g(c). We then construct the updated proof
391 // TRANS( a=g(b), CONG{g}( b=c ) )
392 // We then apply the substitution { a -> g(c), b -> c } to f(a), to obtain:
393 // CONG{f}( TRANS( a=g(b), CONG{g}( b=c ) ) )
394 // which notice is more compact than the proof above.
396 // get the kind of substitution
397 MethodId ids
= MethodId::SB_DEFAULT
;
398 if (args
.size() >= 2)
400 builtin::BuiltinProofRuleChecker::getMethodId(args
[1], ids
);
402 std::vector
<std::shared_ptr
<CDProof
>> pfs
;
403 std::vector
<Node
> vvec
;
404 std::vector
<Node
> svec
;
405 std::vector
<ProofGenerator
*> pgs
;
406 for (size_t i
= 0, nchild
= children
.size(); i
< nchild
; i
++)
408 // Note we process in forward order, since later substitution should be
409 // applied to earlier ones, and the last child of a SUBS is processed
411 // get the substitution
413 builtin::BuiltinProofRuleChecker::getSubstitution(
414 children
[i
], var
, subs
, ids
);
415 Trace("smt-proof-pp-debug")
416 << "...process " << var
<< " -> " << subs
<< " (" << children
[i
]
417 << ", " << ids
<< ")" << std::endl
;
418 // apply the current substitution to the range
422 subs
.substitute(vvec
.begin(), vvec
.end(), svec
.begin(), svec
.end());
425 Trace("smt-proof-pp-debug")
426 << "......updated to " << var
<< " -> " << ss
427 << " based on previous substitution" << std::endl
;
428 // make the proof for the tranitivity step
429 std::shared_ptr
<CDProof
> pf
= std::make_shared
<CDProof
>(d_pnm
);
431 // prove the updated substitution
432 TConvProofGenerator
tcg(d_pnm
, nullptr, TConvPolicy::ONCE
);
433 // add previous rewrite steps
434 for (unsigned j
= 0, nvars
= vvec
.size(); j
< nvars
; j
++)
436 // not necessarily closed, so we pass false to addRewriteStep.
437 tcg
.addRewriteStep(vvec
[j
], svec
[j
], pgs
[j
], false);
439 // get the proof for the update to the current substitution
440 Node seqss
= subs
.eqNode(ss
);
441 std::shared_ptr
<ProofNode
> pfn
= tcg
.getProofFor(seqss
);
442 Assert(pfn
!= nullptr);
445 // get proof for children[i] from cdp
446 pfn
= cdp
->getProofFor(children
[i
]);
448 // ensure we have a proof of var = subs
449 Node veqs
= addProofForSubsStep(var
, subs
, children
[i
], pf
.get());
451 pf
->addStep(var
.eqNode(ss
), PfRule::TRANS
, {veqs
, seqss
}, {});
452 // add to the substitution
455 pgs
.push_back(pf
.get());
459 // Just use equality from CDProof, but ensure we have a proof in cdp.
460 // This may involve a TRUE_INTRO/FALSE_INTRO if the substitution step
461 // uses the assumption children[i] as a Boolean assignment (e.g.
462 // children[i] = true if we are using MethodId::SB_LITERAL).
463 addProofForSubsStep(var
, subs
, children
[i
], cdp
);
465 svec
.push_back(subs
);
468 Node ts
= t
.substitute(vvec
.begin(), vvec
.end(), svec
.begin(), svec
.end());
469 Node eq
= t
.eqNode(ts
);
472 // should be implied by the substitution now
473 TConvProofGenerator
tcpg(d_pnm
, nullptr, TConvPolicy::ONCE
);
474 for (unsigned j
= 0, nvars
= vvec
.size(); j
< nvars
; j
++)
476 // not necessarily closed, so we pass false to addRewriteStep.
477 tcpg
.addRewriteStep(vvec
[j
], svec
[j
], pgs
[j
], false);
479 // add the proof constructed by the term conversion utility
480 std::shared_ptr
<ProofNode
> pfn
= tcpg
.getProofFor(eq
);
481 // should give a proof, if not, then tcpg does not agree with the
483 Assert(pfn
!= nullptr);
486 cdp
->addStep(eq
, PfRule::TRUST_SUBS
, {}, {eq
});
495 // should not be necessary typically
496 cdp
->addStep(eq
, PfRule::REFL
, {}, {t
});
500 else if (id
== PfRule::REWRITE
)
502 // get the kind of rewrite
503 MethodId idr
= MethodId::RW_REWRITE
;
504 if (args
.size() >= 2)
506 builtin::BuiltinProofRuleChecker::getMethodId(args
[1], idr
);
508 builtin::BuiltinProofRuleChecker
* builtinPfC
=
509 static_cast<builtin::BuiltinProofRuleChecker
*>(
510 d_pnm
->getChecker()->getCheckerFor(PfRule::REWRITE
));
511 Node ret
= builtinPfC
->applyRewrite(args
[0], idr
);
512 Node eq
= args
[0].eqNode(ret
);
513 if (idr
== MethodId::RW_REWRITE
|| idr
== MethodId::RW_REWRITE_EQ_EXT
)
515 // rewrites from theory::Rewriter
516 // automatically expand THEORY_REWRITE as well here if set
518 (d_elimRules
.find(PfRule::THEORY_REWRITE
) != d_elimRules
.end());
519 bool isExtEq
= (idr
== MethodId::RW_REWRITE_EQ_EXT
);
520 // use rewrite with proof interface
521 Rewriter
* rr
= d_smte
->getRewriter();
522 TrustNode trn
= rr
->rewriteWithProof(args
[0], elimTR
, isExtEq
);
523 std::shared_ptr
<ProofNode
> pfn
= trn
.toProofNode();
526 // did not have a proof of rewriting, probably isExtEq is true
527 cdp
->addStep(eq
, PfRule::TRUST_REWRITE
, {}, {eq
});
533 Assert(trn
.getNode() == ret
)
534 << "Unexpected rewrite " << args
[0] << std::endl
535 << "Got: " << trn
.getNode() << std::endl
536 << "Expected: " << ret
;
538 else if (idr
== MethodId::RW_EVALUATE
)
540 // change to evaluate, which is never eliminated
541 cdp
->addStep(eq
, PfRule::EVALUATE
, {}, {args
[0]});
545 // don't know how to eliminate
550 // should not be necessary typically
551 cdp
->addStep(eq
, PfRule::REFL
, {}, {args
[0]});
556 // TRUST, PREPROCESS, THEORY_LEMMA, THEORY_PREPROCESS?
561 Node
ProofPostprocessCallback::addProofForWitnessForm(Node t
, CDProof
* cdp
)
563 Node tw
= SkolemManager::getWitnessForm(t
);
564 Node eq
= t
.eqNode(tw
);
567 // not necessary, add REFL step
568 cdp
->addStep(eq
, PfRule::REFL
, {}, {t
});
571 std::shared_ptr
<ProofNode
> pn
= d_wfpm
.getProofFor(eq
);
579 Assert(false) << "ProofPostprocessCallback::addProofForWitnessForm: failed "
580 "to add proof for witness form of "
586 Node
ProofPostprocessCallback::addProofForTrans(
587 const std::vector
<Node
>& tchildren
, CDProof
* cdp
)
589 size_t tsize
= tchildren
.size();
592 Node lhs
= tchildren
[0][0];
593 Node rhs
= tchildren
[tsize
- 1][1];
594 Node eq
= lhs
.eqNode(rhs
);
595 cdp
->addStep(eq
, PfRule::TRANS
, tchildren
, {});
605 Node
ProofPostprocessCallback::addProofForSubsStep(Node var
,
610 // ensure we have a proof of var = subs
611 Node veqs
= var
.eqNode(subs
);
614 // should be true intro or false intro
615 Assert(subs
.isConst());
618 subs
.getConst
<bool>() ? PfRule::TRUE_INTRO
: PfRule::FALSE_INTRO
,
625 bool ProofPostprocessCallback::addToTransChildren(Node eq
,
626 std::vector
<Node
>& tchildren
,
629 Assert(!eq
.isNull());
630 Assert(eq
.getKind() == kind::EQUAL
);
635 Node equ
= isSymm
? eq
[1].eqNode(eq
[0]) : eq
;
636 Assert(tchildren
.empty()
637 || (tchildren
[tchildren
.size() - 1].getKind() == kind::EQUAL
638 && tchildren
[tchildren
.size() - 1][1] == equ
[0]));
639 tchildren
.push_back(equ
);
643 ProofPostprocessFinalCallback::ProofPostprocessFinalCallback(
644 ProofNodeManager
* pnm
)
645 : d_ruleCount("finalProof::ruleCount"),
646 d_totalRuleCount("finalProof::totalRuleCount", 0),
648 d_pedanticFailure(false)
650 smtStatisticsRegistry()->registerStat(&d_ruleCount
);
651 smtStatisticsRegistry()->registerStat(&d_totalRuleCount
);
654 ProofPostprocessFinalCallback::~ProofPostprocessFinalCallback()
656 smtStatisticsRegistry()->unregisterStat(&d_ruleCount
);
657 smtStatisticsRegistry()->unregisterStat(&d_totalRuleCount
);
660 void ProofPostprocessFinalCallback::initializeUpdate()
662 d_pedanticFailure
= false;
663 d_pedanticFailureOut
.str("");
666 bool ProofPostprocessFinalCallback::shouldUpdate(std::shared_ptr
<ProofNode
> pn
,
667 bool& continueUpdate
)
669 PfRule r
= pn
->getRule();
670 if (Trace
.isOn("final-pf-hole"))
672 if (r
== PfRule::THEORY_REWRITE
)
674 Trace("final-pf-hole") << "hole: " << r
<< " : " << pn
->getResult()
678 // if not doing eager pedantic checking, fail if below threshold
679 if (!options::proofNewPedanticEager())
681 if (!d_pedanticFailure
)
683 Assert(d_pedanticFailureOut
.str().empty());
684 if (d_pnm
->getChecker()->isPedanticFailure(r
, d_pedanticFailureOut
))
686 d_pedanticFailure
= true;
690 // record stats for the rule
696 bool ProofPostprocessFinalCallback::wasPedanticFailure(std::ostream
& out
) const
698 if (d_pedanticFailure
)
700 out
<< d_pedanticFailureOut
.str();
706 ProofPostproccess::ProofPostproccess(ProofNodeManager
* pnm
,
708 ProofGenerator
* pppg
)
710 d_cb(pnm
, smte
, pppg
),
711 d_updater(d_pnm
, d_cb
),
713 d_finalizer(d_pnm
, d_finalCb
)
717 ProofPostproccess::~ProofPostproccess() {}
719 void ProofPostproccess::process(std::shared_ptr
<ProofNode
> pf
)
721 // Initialize the callback, which computes necessary static information about
722 // how to process, including how to process assumptions in pf.
723 d_cb
.initializeUpdate();
725 d_updater
.process(pf
);
726 // take stats and check pedantic
727 d_finalCb
.initializeUpdate();
728 d_finalizer
.process(pf
);
730 std::stringstream serr
;
731 bool wasPedanticFailure
= d_finalCb
.wasPedanticFailure(serr
);
732 if (wasPedanticFailure
)
734 AlwaysAssert(!wasPedanticFailure
)
735 << "ProofPostproccess::process: pedantic failure:" << std::endl
740 void ProofPostproccess::setEliminateRule(PfRule rule
)
742 d_cb
.setEliminateRule(rule
);