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 NodeManager
* nm
= NodeManager::currentNM();
380 // Notice that a naive way to reconstruct SUBS is to do a term conversion
381 // proof for each substitution.
382 // The proof of f(a) * { a -> g(b) } * { b -> c } = f(g(c)) is:
383 // TRANS( CONG{f}( a=g(b) ), CONG{f}( CONG{g}( b=c ) ) )
384 // Notice that more optimal proofs are possible that do a single traversal
385 // over t. This is done by applying later substitutions to the range of
386 // previous substitutions, until a final simultaneous substitution is
387 // applied to t. For instance, in the above example, we first prove:
389 // by applying the second substitution { b -> c } to the range of the first,
390 // giving us a proof of g(b)=g(c). We then construct the updated proof
392 // TRANS( a=g(b), CONG{g}( b=c ) )
393 // We then apply the substitution { a -> g(c), b -> c } to f(a), to obtain:
394 // CONG{f}( TRANS( a=g(b), CONG{g}( b=c ) ) )
395 // which notice is more compact than the proof above.
397 // get the kind of substitution
398 MethodId ids
= MethodId::SB_DEFAULT
;
399 if (args
.size() >= 2)
401 builtin::BuiltinProofRuleChecker::getMethodId(args
[1], ids
);
403 std::vector
<std::shared_ptr
<CDProof
>> pfs
;
404 std::vector
<TNode
> vsList
;
405 std::vector
<TNode
> ssList
;
406 std::vector
<TNode
> fromList
;
407 std::vector
<ProofGenerator
*> pgs
;
408 // first, compute the entire substitution
409 for (size_t i
= 0, nchild
= children
.size(); i
< nchild
; i
++)
411 // get the substitution
412 builtin::BuiltinProofRuleChecker::getSubstitutionFor(
413 children
[i
], vsList
, ssList
, fromList
, ids
);
414 // ensure proofs for each formula in fromList
415 if (children
[i
].getKind() == AND
&& ids
== MethodId::SB_DEFAULT
)
417 for (size_t j
= 0, nchildi
= children
[i
].getNumChildren(); j
< nchildi
;
420 Node nodej
= nm
->mkConst(Rational(j
));
422 children
[i
][j
], PfRule::AND_ELIM
, {children
[i
]}, {nodej
});
426 std::vector
<Node
> vvec
;
427 std::vector
<Node
> svec
;
428 for (size_t i
= 0, nvs
= vsList
.size(); i
< nvs
; i
++)
430 // Note we process in forward order, since later substitution should be
431 // applied to earlier ones, and the last child of a SUBS is processed
433 TNode var
= vsList
[i
];
434 TNode subs
= ssList
[i
];
435 TNode childFrom
= fromList
[i
];
436 Trace("smt-proof-pp-debug")
437 << "...process " << var
<< " -> " << subs
<< " (" << childFrom
<< ", "
438 << ids
<< ")" << std::endl
;
439 // apply the current substitution to the range
443 subs
.substitute(vvec
.begin(), vvec
.end(), svec
.begin(), svec
.end());
446 Trace("smt-proof-pp-debug")
447 << "......updated to " << var
<< " -> " << ss
448 << " based on previous substitution" << std::endl
;
449 // make the proof for the tranitivity step
450 std::shared_ptr
<CDProof
> pf
= std::make_shared
<CDProof
>(d_pnm
);
452 // prove the updated substitution
453 TConvProofGenerator
tcg(d_pnm
,
456 TConvCachePolicy::NEVER
,
457 "nested_SUBS_TConvProofGenerator",
460 // add previous rewrite steps
461 for (unsigned j
= 0, nvars
= vvec
.size(); j
< nvars
; j
++)
463 // not necessarily closed, so we pass false to addRewriteStep.
464 tcg
.addRewriteStep(vvec
[j
], svec
[j
], pgs
[j
], false);
466 // get the proof for the update to the current substitution
467 Node seqss
= subs
.eqNode(ss
);
468 std::shared_ptr
<ProofNode
> pfn
= tcg
.getProofFor(seqss
);
469 Assert(pfn
!= nullptr);
472 // get proof for childFrom from cdp
473 pfn
= cdp
->getProofFor(childFrom
);
475 // ensure we have a proof of var = subs
476 Node veqs
= addProofForSubsStep(var
, subs
, childFrom
, pf
.get());
478 pf
->addStep(var
.eqNode(ss
), PfRule::TRANS
, {veqs
, seqss
}, {});
479 // add to the substitution
482 pgs
.push_back(pf
.get());
486 // Just use equality from CDProof, but ensure we have a proof in cdp.
487 // This may involve a TRUE_INTRO/FALSE_INTRO if the substitution step
488 // uses the assumption childFrom as a Boolean assignment (e.g.
489 // childFrom = true if we are using MethodId::SB_LITERAL).
490 addProofForSubsStep(var
, subs
, childFrom
, cdp
);
492 svec
.push_back(subs
);
495 Node ts
= t
.substitute(vvec
.begin(), vvec
.end(), svec
.begin(), svec
.end());
496 Node eq
= t
.eqNode(ts
);
499 // should be implied by the substitution now
500 TConvProofGenerator
tcpg(d_pnm
,
503 TConvCachePolicy::NEVER
,
504 "SUBS_TConvProofGenerator",
507 for (unsigned j
= 0, nvars
= vvec
.size(); j
< nvars
; j
++)
509 // not necessarily closed, so we pass false to addRewriteStep.
510 tcpg
.addRewriteStep(vvec
[j
], svec
[j
], pgs
[j
], false);
512 // add the proof constructed by the term conversion utility
513 std::shared_ptr
<ProofNode
> pfn
= tcpg
.getProofFor(eq
);
514 // should give a proof, if not, then tcpg does not agree with the
516 Assert(pfn
!= nullptr);
519 cdp
->addStep(eq
, PfRule::TRUST_SUBS
, {}, {eq
});
528 // should not be necessary typically
529 cdp
->addStep(eq
, PfRule::REFL
, {}, {t
});
533 else if (id
== PfRule::REWRITE
)
535 // get the kind of rewrite
536 MethodId idr
= MethodId::RW_REWRITE
;
537 if (args
.size() >= 2)
539 builtin::BuiltinProofRuleChecker::getMethodId(args
[1], idr
);
541 builtin::BuiltinProofRuleChecker
* builtinPfC
=
542 static_cast<builtin::BuiltinProofRuleChecker
*>(
543 d_pnm
->getChecker()->getCheckerFor(PfRule::REWRITE
));
544 Node ret
= builtinPfC
->applyRewrite(args
[0], idr
);
545 Node eq
= args
[0].eqNode(ret
);
546 if (idr
== MethodId::RW_REWRITE
|| idr
== MethodId::RW_REWRITE_EQ_EXT
)
548 // rewrites from theory::Rewriter
549 // automatically expand THEORY_REWRITE as well here if set
551 (d_elimRules
.find(PfRule::THEORY_REWRITE
) != d_elimRules
.end());
552 bool isExtEq
= (idr
== MethodId::RW_REWRITE_EQ_EXT
);
553 // use rewrite with proof interface
554 Rewriter
* rr
= d_smte
->getRewriter();
555 TrustNode trn
= rr
->rewriteWithProof(args
[0], elimTR
, isExtEq
);
556 std::shared_ptr
<ProofNode
> pfn
= trn
.toProofNode();
559 Trace("smt-proof-pp-debug")
560 << "Use TRUST_REWRITE for " << eq
<< std::endl
;
561 // did not have a proof of rewriting, probably isExtEq is true
567 cdp
->addStep(eq
, PfRule::TRUST_REWRITE
, {}, {eq
});
573 Assert(trn
.getNode() == ret
)
574 << "Unexpected rewrite " << args
[0] << std::endl
575 << "Got: " << trn
.getNode() << std::endl
576 << "Expected: " << ret
;
578 else if (idr
== MethodId::RW_EVALUATE
)
580 // change to evaluate, which is never eliminated
581 cdp
->addStep(eq
, PfRule::EVALUATE
, {}, {args
[0]});
585 // don't know how to eliminate
590 // should not be necessary typically
591 cdp
->addStep(eq
, PfRule::REFL
, {}, {args
[0]});
596 // TRUST, PREPROCESS, THEORY_LEMMA, THEORY_PREPROCESS?
601 Node
ProofPostprocessCallback::addProofForWitnessForm(Node t
, CDProof
* cdp
)
603 Node tw
= SkolemManager::getWitnessForm(t
);
604 Node eq
= t
.eqNode(tw
);
607 // not necessary, add REFL step
608 cdp
->addStep(eq
, PfRule::REFL
, {}, {t
});
611 std::shared_ptr
<ProofNode
> pn
= d_wfpm
.getProofFor(eq
);
619 Assert(false) << "ProofPostprocessCallback::addProofForWitnessForm: failed "
620 "to add proof for witness form of "
626 Node
ProofPostprocessCallback::addProofForTrans(
627 const std::vector
<Node
>& tchildren
, CDProof
* cdp
)
629 size_t tsize
= tchildren
.size();
632 Node lhs
= tchildren
[0][0];
633 Node rhs
= tchildren
[tsize
- 1][1];
634 Node eq
= lhs
.eqNode(rhs
);
635 cdp
->addStep(eq
, PfRule::TRANS
, tchildren
, {});
645 Node
ProofPostprocessCallback::addProofForSubsStep(Node var
,
650 // ensure we have a proof of var = subs
651 Node veqs
= var
.eqNode(subs
);
654 // should be true intro or false intro
655 Assert(subs
.isConst());
658 subs
.getConst
<bool>() ? PfRule::TRUE_INTRO
: PfRule::FALSE_INTRO
,
665 bool ProofPostprocessCallback::addToTransChildren(Node eq
,
666 std::vector
<Node
>& tchildren
,
669 Assert(!eq
.isNull());
670 Assert(eq
.getKind() == kind::EQUAL
);
675 Node equ
= isSymm
? eq
[1].eqNode(eq
[0]) : eq
;
676 Assert(tchildren
.empty()
677 || (tchildren
[tchildren
.size() - 1].getKind() == kind::EQUAL
678 && tchildren
[tchildren
.size() - 1][1] == equ
[0]));
679 tchildren
.push_back(equ
);
683 ProofPostprocessFinalCallback::ProofPostprocessFinalCallback(
684 ProofNodeManager
* pnm
)
685 : d_ruleCount("finalProof::ruleCount"),
686 d_totalRuleCount("finalProof::totalRuleCount", 0),
687 d_minPedanticLevel("finalProof::minPedanticLevel", 10),
688 d_numFinalProofs("finalProofs::numFinalProofs", 0),
690 d_pedanticFailure(false)
692 smtStatisticsRegistry()->registerStat(&d_ruleCount
);
693 smtStatisticsRegistry()->registerStat(&d_totalRuleCount
);
694 smtStatisticsRegistry()->registerStat(&d_minPedanticLevel
);
695 smtStatisticsRegistry()->registerStat(&d_numFinalProofs
);
698 ProofPostprocessFinalCallback::~ProofPostprocessFinalCallback()
700 smtStatisticsRegistry()->unregisterStat(&d_ruleCount
);
701 smtStatisticsRegistry()->unregisterStat(&d_totalRuleCount
);
702 smtStatisticsRegistry()->unregisterStat(&d_minPedanticLevel
);
703 smtStatisticsRegistry()->unregisterStat(&d_numFinalProofs
);
706 void ProofPostprocessFinalCallback::initializeUpdate()
708 d_pedanticFailure
= false;
709 d_pedanticFailureOut
.str("");
713 bool ProofPostprocessFinalCallback::shouldUpdate(std::shared_ptr
<ProofNode
> pn
,
714 bool& continueUpdate
)
716 PfRule r
= pn
->getRule();
717 if (Trace
.isOn("final-pf-hole"))
719 if (r
== PfRule::THEORY_REWRITE
)
721 Trace("final-pf-hole") << "hole: " << r
<< " : " << pn
->getResult()
725 // if not doing eager pedantic checking, fail if below threshold
726 if (!options::proofNewPedanticEager())
728 if (!d_pedanticFailure
)
730 Assert(d_pedanticFailureOut
.str().empty());
731 if (d_pnm
->getChecker()->isPedanticFailure(r
, d_pedanticFailureOut
))
733 d_pedanticFailure
= true;
737 uint32_t plevel
= d_pnm
->getChecker()->getPedanticLevel(r
);
740 d_minPedanticLevel
.minAssign(plevel
);
742 // record stats for the rule
748 bool ProofPostprocessFinalCallback::wasPedanticFailure(std::ostream
& out
) const
750 if (d_pedanticFailure
)
752 out
<< d_pedanticFailureOut
.str();
758 ProofPostproccess::ProofPostproccess(ProofNodeManager
* pnm
,
760 ProofGenerator
* pppg
)
762 d_cb(pnm
, smte
, pppg
),
763 d_updater(d_pnm
, d_cb
),
765 d_finalizer(d_pnm
, d_finalCb
)
769 ProofPostproccess::~ProofPostproccess() {}
771 void ProofPostproccess::process(std::shared_ptr
<ProofNode
> pf
)
773 // Initialize the callback, which computes necessary static information about
774 // how to process, including how to process assumptions in pf.
775 d_cb
.initializeUpdate();
777 d_updater
.process(pf
);
778 // take stats and check pedantic
779 d_finalCb
.initializeUpdate();
780 d_finalizer
.process(pf
);
782 std::stringstream serr
;
783 bool wasPedanticFailure
= d_finalCb
.wasPedanticFailure(serr
);
784 if (wasPedanticFailure
)
786 AlwaysAssert(!wasPedanticFailure
)
787 << "ProofPostproccess::process: pedantic failure:" << std::endl
792 void ProofPostproccess::setEliminateRule(PfRule rule
)
794 d_cb
.setEliminateRule(rule
);