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"
24 #include "theory/theory.h"
26 using namespace CVC4::kind
;
27 using namespace CVC4::theory
;
32 ProofPostprocessCallback::ProofPostprocessCallback(ProofNodeManager
* pnm
,
35 : d_pnm(pnm
), d_smte(smte
), d_pppg(pppg
), d_wfpm(pnm
)
37 d_true
= NodeManager::currentNM()->mkConst(true);
38 // always check whether to update ASSUME
39 d_elimRules
.insert(PfRule::ASSUME
);
42 void ProofPostprocessCallback::initializeUpdate()
44 d_assumpToProof
.clear();
45 d_wfAssumptions
.clear();
48 void ProofPostprocessCallback::setEliminateRule(PfRule rule
)
50 d_elimRules
.insert(rule
);
53 bool ProofPostprocessCallback::shouldUpdate(std::shared_ptr
<ProofNode
> pn
,
56 return d_elimRules
.find(pn
->getRule()) != d_elimRules
.end();
59 bool ProofPostprocessCallback::update(Node res
,
61 const std::vector
<Node
>& children
,
62 const std::vector
<Node
>& args
,
66 Trace("smt-proof-pp-debug") << "- Post process " << id
<< " " << children
67 << " / " << args
<< std::endl
;
69 if (id
== PfRule::ASSUME
)
71 // we cache based on the assumption node, not the proof node, since there
72 // may be multiple occurrences of the same node.
74 std::shared_ptr
<ProofNode
> pfn
;
75 std::map
<Node
, std::shared_ptr
<ProofNode
>>::iterator it
=
76 d_assumpToProof
.find(f
);
77 if (it
!= d_assumpToProof
.end())
79 Trace("smt-proof-pp-debug") << "...already computed" << std::endl
;
84 Trace("smt-proof-pp-debug") << "...get proof" << std::endl
;
85 Assert(d_pppg
!= nullptr);
86 // get proof from preprocess proof generator
87 pfn
= d_pppg
->getProofFor(f
);
88 Trace("smt-proof-pp-debug") << "...finished get proof" << std::endl
;
89 // print for debugging
92 Trace("smt-proof-pp-debug")
93 << "...no proof, possibly an input assumption" << std::endl
;
97 Assert(pfn
->getResult() == f
);
98 if (Trace
.isOn("smt-proof-pp"))
100 Trace("smt-proof-pp")
101 << "=== Connect proof for preprocessing: " << f
<< std::endl
;
102 Trace("smt-proof-pp") << *pfn
.get() << std::endl
;
105 d_assumpToProof
[f
] = pfn
;
107 if (pfn
== nullptr || pfn
->getRule() == PfRule::ASSUME
)
109 Trace("smt-proof-pp-debug") << "...do not add proof" << std::endl
;
113 Trace("smt-proof-pp-debug") << "...add proof" << std::endl
;
118 Node ret
= expandMacros(id
, children
, args
, cdp
);
119 Trace("smt-proof-pp-debug") << "...expanded = " << !ret
.isNull() << std::endl
;
120 return !ret
.isNull();
123 bool ProofPostprocessCallback::updateInternal(Node res
,
125 const std::vector
<Node
>& children
,
126 const std::vector
<Node
>& args
,
129 bool continueUpdate
= true;
130 return update(res
, id
, children
, args
, cdp
, continueUpdate
);
133 Node
ProofPostprocessCallback::expandMacros(PfRule id
,
134 const std::vector
<Node
>& children
,
135 const std::vector
<Node
>& args
,
138 if (d_elimRules
.find(id
) == d_elimRules
.end())
144 if (id
== PfRule::MACRO_SR_EQ_INTRO
)
147 // (SUBS <children> :args args[0:1])
148 // (REWRITE :args <t.substitute(x1,t1). ... .substitute(xn,tn)> args[2]))
149 std::vector
<Node
> tchildren
;
152 if (!children
.empty())
154 std::vector
<Node
> sargs
;
156 MethodId sid
= MethodId::SB_DEFAULT
;
157 if (args
.size() >= 2)
159 if (builtin::BuiltinProofRuleChecker::getMethodId(args
[1], sid
))
161 sargs
.push_back(args
[1]);
165 builtin::BuiltinProofRuleChecker::applySubstitution(t
, children
, sid
);
166 Trace("smt-proof-pp-debug")
167 << "...eq intro subs equality is " << t
<< " == " << ts
<< ", from "
171 Node eq
= t
.eqNode(ts
);
172 // apply SUBS proof rule if necessary
173 if (!updateInternal(eq
, PfRule::SUBS
, children
, sargs
, cdp
))
175 // if we specified that we did not want to eliminate, add as step
176 cdp
->addStep(eq
, PfRule::SUBS
, children
, sargs
);
178 tchildren
.push_back(eq
);
186 std::vector
<Node
> rargs
;
188 MethodId rid
= MethodId::RW_REWRITE
;
189 if (args
.size() >= 3)
191 if (builtin::BuiltinProofRuleChecker::getMethodId(args
[2], rid
))
193 rargs
.push_back(args
[2]);
196 builtin::BuiltinProofRuleChecker
* builtinPfC
=
197 static_cast<builtin::BuiltinProofRuleChecker
*>(
198 d_pnm
->getChecker()->getCheckerFor(PfRule::MACRO_SR_EQ_INTRO
));
199 Node tr
= builtinPfC
->applyRewrite(ts
, rid
);
200 Trace("smt-proof-pp-debug")
201 << "...eq intro rewrite equality is " << ts
<< " == " << tr
<< ", from "
205 Node eq
= ts
.eqNode(tr
);
206 // apply REWRITE proof rule
207 if (!updateInternal(eq
, PfRule::REWRITE
, {}, rargs
, cdp
))
209 // if not elimianted, add as step
210 cdp
->addStep(eq
, PfRule::REWRITE
, {}, rargs
);
212 tchildren
.push_back(eq
);
216 // typically not necessary, but done to be robust
217 cdp
->addStep(t
.eqNode(tr
), PfRule::REFL
, {}, {t
});
220 // must add TRANS if two step
221 return addProofForTrans(tchildren
, cdp
);
223 else if (id
== PfRule::MACRO_SR_PRED_INTRO
)
225 std::vector
<Node
> tchildren
;
226 std::vector
<Node
> sargs
= args
;
227 // take into account witness form, if necessary
228 bool reqWitness
= d_wfpm
.requiresWitnessFormIntro(args
[0]);
229 Trace("smt-proof-pp-debug")
230 << "...pred intro reqWitness=" << reqWitness
<< std::endl
;
233 // (MACRO_SR_EQ_INTRO <children> :args (t args[1:]))
234 // ... proof of apply_SR(t) = toWitness(apply_SR(t)) ...
235 // (MACRO_SR_EQ_INTRO {} {toWitness(apply_SR(t))})
237 // Notice this is an optimized, one sided version of the expansion of
238 // MACRO_SR_PRED_TRANSFORM below.
239 // We call the expandMacros method on MACRO_SR_EQ_INTRO, where notice
240 // that this rule application is immediately expanded in the recursive
241 // call and not added to the proof.
242 Node conc
= expandMacros(PfRule::MACRO_SR_EQ_INTRO
, children
, sargs
, cdp
);
243 Trace("smt-proof-pp-debug")
244 << "...pred intro conclusion is " << conc
<< std::endl
;
245 Assert(!conc
.isNull());
246 Assert(conc
.getKind() == EQUAL
);
247 Assert(conc
[0] == args
[0]);
248 tchildren
.push_back(conc
);
251 Node weq
= addProofForWitnessForm(conc
[1], cdp
);
252 Trace("smt-proof-pp-debug") << "...weq is " << weq
<< std::endl
;
253 if (addToTransChildren(weq
, tchildren
))
255 // toWitness(apply_SR(t)) = apply_SR(toWitness(apply_SR(t)))
256 // rewrite again, don't need substitution. Also we always use the
257 // default rewriter, due to the definition of MACRO_SR_PRED_INTRO.
258 Node weqr
= expandMacros(PfRule::MACRO_SR_EQ_INTRO
, {}, {weq
[1]}, cdp
);
259 addToTransChildren(weqr
, tchildren
);
262 // apply transitivity if necessary
263 Node eq
= addProofForTrans(tchildren
, cdp
);
264 Assert(!eq
.isNull());
265 Assert(eq
.getKind() == EQUAL
);
266 Assert(eq
[0] == args
[0]);
267 Assert(eq
[1] == d_true
);
269 cdp
->addStep(eq
[0], PfRule::TRUE_ELIM
, {eq
}, {});
272 else if (id
== PfRule::MACRO_SR_PRED_ELIM
)
276 // (MACRO_SR_EQ_INTRO children[1:] :args children[0] ++ args))
277 std::vector
<Node
> schildren(children
.begin() + 1, children
.end());
278 std::vector
<Node
> srargs
;
279 srargs
.push_back(children
[0]);
280 srargs
.insert(srargs
.end(), args
.begin(), args
.end());
281 Node conc
= expandMacros(PfRule::MACRO_SR_EQ_INTRO
, schildren
, srargs
, cdp
);
282 Assert(!conc
.isNull());
283 Assert(conc
.getKind() == EQUAL
);
284 Assert(conc
[0] == children
[0]);
285 // apply equality resolve
286 cdp
->addStep(conc
[1], PfRule::EQ_RESOLVE
, {children
[0], conc
}, {});
289 else if (id
== PfRule::MACRO_SR_PRED_TRANSFORM
)
294 // (MACRO_SR_EQ_INTRO children[1:] :args (children[0] args[1:]))
295 // ... proof of c = wc
296 // (MACRO_SR_EQ_INTRO {} wc)
298 // (MACRO_SR_EQ_INTRO children[1:] :args <args>)
299 // ... proof of a = wa
300 // (MACRO_SR_EQ_INTRO {} wa))))
302 // wa = toWitness(apply_SR(args[0])) and
303 // wc = toWitness(apply_SR(children[0])).
304 Trace("smt-proof-pp-debug")
305 << "Transform " << children
[0] << " == " << args
[0] << std::endl
;
306 if (CDProof::isSame(children
[0], args
[0]))
308 Trace("smt-proof-pp-debug") << "...nothing to do" << std::endl
;
312 std::vector
<Node
> tchildren
;
313 std::vector
<Node
> schildren(children
.begin() + 1, children
.end());
314 std::vector
<Node
> sargs
= args
;
315 // first, compute if we need
316 bool reqWitness
= d_wfpm
.requiresWitnessFormTransform(children
[0], args
[0]);
317 Trace("smt-proof-pp-debug") << "...reqWitness=" << reqWitness
<< std::endl
;
318 // convert both sides, in three steps, take symmetry of second chain
319 for (unsigned r
= 0; r
< 2; r
++)
321 std::vector
<Node
> tchildrenr
;
322 // first rewrite children[0], then args[0]
323 sargs
[0] = r
== 0 ? children
[0] : args
[0];
325 Node eq
= expandMacros(PfRule::MACRO_SR_EQ_INTRO
, schildren
, sargs
, cdp
);
326 Trace("smt-proof-pp-debug")
327 << "transform subs_rewrite (" << r
<< "): " << eq
<< std::endl
;
328 Assert(!eq
.isNull() && eq
.getKind() == EQUAL
&& eq
[0] == sargs
[0]);
329 addToTransChildren(eq
, tchildrenr
);
330 // apply_SR(t) = toWitness(apply_SR(t))
333 Node weq
= addProofForWitnessForm(eq
[1], cdp
);
334 Trace("smt-proof-pp-debug")
335 << "transform toWitness (" << r
<< "): " << weq
<< std::endl
;
336 if (addToTransChildren(weq
, tchildrenr
))
338 // toWitness(apply_SR(t)) = apply_SR(toWitness(apply_SR(t)))
339 // rewrite again, don't need substitution. Also, we always use the
340 // default rewriter, due to the definition of MACRO_SR_PRED_TRANSFORM.
342 expandMacros(PfRule::MACRO_SR_EQ_INTRO
, {}, {weq
[1]}, cdp
);
343 Trace("smt-proof-pp-debug") << "transform rewrite_witness (" << r
344 << "): " << weqr
<< std::endl
;
345 addToTransChildren(weqr
, tchildrenr
);
348 Trace("smt-proof-pp-debug")
349 << "transform connect (" << r
<< ")" << std::endl
;
350 // add to overall chain
353 // add the current chain to the overall chain
354 tchildren
.insert(tchildren
.end(), tchildrenr
.begin(), tchildrenr
.end());
358 // add the current chain to cdp
359 Node eqr
= addProofForTrans(tchildrenr
, cdp
);
362 Trace("smt-proof-pp-debug") << "transform connect sym " << tchildren
363 << " " << eqr
<< std::endl
;
364 // take symmetry of above and add it to the overall chain
365 addToTransChildren(eqr
, tchildren
, true);
368 Trace("smt-proof-pp-debug")
369 << "transform finish (" << r
<< ")" << std::endl
;
372 // apply transitivity if necessary
373 Node eq
= addProofForTrans(tchildren
, cdp
);
375 cdp
->addStep(args
[0], PfRule::EQ_RESOLVE
, {children
[0], eq
}, {});
378 else if (id
== PfRule::SUBS
)
380 NodeManager
* nm
= NodeManager::currentNM();
381 // Notice that a naive way to reconstruct SUBS is to do a term conversion
382 // proof for each substitution.
383 // The proof of f(a) * { a -> g(b) } * { b -> c } = f(g(c)) is:
384 // TRANS( CONG{f}( a=g(b) ), CONG{f}( CONG{g}( b=c ) ) )
385 // Notice that more optimal proofs are possible that do a single traversal
386 // over t. This is done by applying later substitutions to the range of
387 // previous substitutions, until a final simultaneous substitution is
388 // applied to t. For instance, in the above example, we first prove:
390 // by applying the second substitution { b -> c } to the range of the first,
391 // giving us a proof of g(b)=g(c). We then construct the updated proof
393 // TRANS( a=g(b), CONG{g}( b=c ) )
394 // We then apply the substitution { a -> g(c), b -> c } to f(a), to obtain:
395 // CONG{f}( TRANS( a=g(b), CONG{g}( b=c ) ) )
396 // which notice is more compact than the proof above.
398 // get the kind of substitution
399 MethodId ids
= MethodId::SB_DEFAULT
;
400 if (args
.size() >= 2)
402 builtin::BuiltinProofRuleChecker::getMethodId(args
[1], ids
);
404 std::vector
<std::shared_ptr
<CDProof
>> pfs
;
405 std::vector
<TNode
> vsList
;
406 std::vector
<TNode
> ssList
;
407 std::vector
<TNode
> fromList
;
408 std::vector
<ProofGenerator
*> pgs
;
409 // first, compute the entire substitution
410 for (size_t i
= 0, nchild
= children
.size(); i
< nchild
; i
++)
412 // get the substitution
413 builtin::BuiltinProofRuleChecker::getSubstitutionFor(
414 children
[i
], vsList
, ssList
, fromList
, ids
);
415 // ensure proofs for each formula in fromList
416 if (children
[i
].getKind() == AND
&& ids
== MethodId::SB_DEFAULT
)
418 for (size_t j
= 0, nchildi
= children
[i
].getNumChildren(); j
< nchildi
;
421 Node nodej
= nm
->mkConst(Rational(j
));
423 children
[i
][j
], PfRule::AND_ELIM
, {children
[i
]}, {nodej
});
427 std::vector
<Node
> vvec
;
428 std::vector
<Node
> svec
;
429 for (size_t i
= 0, nvs
= vsList
.size(); i
< nvs
; i
++)
431 // Note we process in forward order, since later substitution should be
432 // applied to earlier ones, and the last child of a SUBS is processed
434 TNode var
= vsList
[i
];
435 TNode subs
= ssList
[i
];
436 TNode childFrom
= fromList
[i
];
437 Trace("smt-proof-pp-debug")
438 << "...process " << var
<< " -> " << subs
<< " (" << childFrom
<< ", "
439 << ids
<< ")" << std::endl
;
440 // apply the current substitution to the range
444 subs
.substitute(vvec
.begin(), vvec
.end(), svec
.begin(), svec
.end());
447 Trace("smt-proof-pp-debug")
448 << "......updated to " << var
<< " -> " << ss
449 << " based on previous substitution" << std::endl
;
450 // make the proof for the tranitivity step
451 std::shared_ptr
<CDProof
> pf
= std::make_shared
<CDProof
>(d_pnm
);
453 // prove the updated substitution
454 TConvProofGenerator
tcg(d_pnm
,
457 TConvCachePolicy::NEVER
,
458 "nested_SUBS_TConvProofGenerator",
461 // add previous rewrite steps
462 for (unsigned j
= 0, nvars
= vvec
.size(); j
< nvars
; j
++)
464 tcg
.addRewriteStep(vvec
[j
], svec
[j
], pgs
[j
]);
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 tcpg
.addRewriteStep(vvec
[j
], svec
[j
], pgs
[j
]);
511 // add the proof constructed by the term conversion utility
512 std::shared_ptr
<ProofNode
> pfn
= tcpg
.getProofFor(eq
);
513 // should give a proof, if not, then tcpg does not agree with the
515 Assert(pfn
!= nullptr);
518 cdp
->addStep(eq
, PfRule::TRUST_SUBS
, {}, {eq
});
527 // should not be necessary typically
528 cdp
->addStep(eq
, PfRule::REFL
, {}, {t
});
532 else if (id
== PfRule::REWRITE
)
534 // get the kind of rewrite
535 MethodId idr
= MethodId::RW_REWRITE
;
536 if (args
.size() >= 2)
538 builtin::BuiltinProofRuleChecker::getMethodId(args
[1], idr
);
540 builtin::BuiltinProofRuleChecker
* builtinPfC
=
541 static_cast<builtin::BuiltinProofRuleChecker
*>(
542 d_pnm
->getChecker()->getCheckerFor(PfRule::REWRITE
));
543 Node ret
= builtinPfC
->applyRewrite(args
[0], idr
);
544 Node eq
= args
[0].eqNode(ret
);
545 if (idr
== MethodId::RW_REWRITE
|| idr
== MethodId::RW_REWRITE_EQ_EXT
)
547 // rewrites from theory::Rewriter
548 bool isExtEq
= (idr
== MethodId::RW_REWRITE_EQ_EXT
);
549 // use rewrite with proof interface
550 Rewriter
* rr
= d_smte
->getRewriter();
551 TrustNode trn
= rr
->rewriteWithProof(args
[0], isExtEq
);
552 std::shared_ptr
<ProofNode
> pfn
= trn
.toProofNode();
555 Trace("smt-proof-pp-debug")
556 << "Use TRUST_REWRITE for " << eq
<< std::endl
;
557 // did not have a proof of rewriting, probably isExtEq is true
560 // update to THEORY_REWRITE with idr
561 Assert(args
.size() >= 1);
562 TheoryId theoryId
= Theory::theoryOf(args
[0].getType());
563 Node tid
= builtin::BuiltinProofRuleChecker::mkTheoryIdNode(theoryId
);
564 cdp
->addStep(eq
, PfRule::THEORY_REWRITE
, {}, {eq
, tid
, args
[1]});
568 // this should never be applied
569 cdp
->addStep(eq
, PfRule::TRUST_REWRITE
, {}, {eq
});
576 Assert(trn
.getNode() == ret
)
577 << "Unexpected rewrite " << args
[0] << std::endl
578 << "Got: " << trn
.getNode() << std::endl
579 << "Expected: " << ret
;
581 else if (idr
== MethodId::RW_EVALUATE
)
583 // change to evaluate, which is never eliminated
584 cdp
->addStep(eq
, PfRule::EVALUATE
, {}, {args
[0]});
588 // don't know how to eliminate
593 // should not be necessary typically
594 cdp
->addStep(eq
, PfRule::REFL
, {}, {args
[0]});
598 else if (id
== PfRule::THEORY_REWRITE
)
600 Assert(!args
.empty());
602 Assert(eq
.getKind() == EQUAL
);
603 // try to replay theory rewrite
604 // first, check that maybe its just an evaluation step
605 ProofChecker
* pc
= d_pnm
->getChecker();
607 pc
->checkDebug(PfRule::EVALUATE
, {}, {eq
[0]}, eq
, "smt-proof-pp-debug");
608 if (!ceval
.isNull() && ceval
== eq
)
610 cdp
->addStep(eq
, PfRule::EVALUATE
, {}, {eq
[0]});
613 // otherwise no update
614 Trace("final-pf-hole") << "hole: " << id
<< " : " << eq
<< std::endl
;
617 // TRUST, PREPROCESS, THEORY_LEMMA, THEORY_PREPROCESS?
622 Node
ProofPostprocessCallback::addProofForWitnessForm(Node t
, CDProof
* cdp
)
624 Node tw
= SkolemManager::getWitnessForm(t
);
625 Node eq
= t
.eqNode(tw
);
628 // not necessary, add REFL step
629 cdp
->addStep(eq
, PfRule::REFL
, {}, {t
});
632 std::shared_ptr
<ProofNode
> pn
= d_wfpm
.getProofFor(eq
);
640 Assert(false) << "ProofPostprocessCallback::addProofForWitnessForm: failed "
641 "to add proof for witness form of "
647 Node
ProofPostprocessCallback::addProofForTrans(
648 const std::vector
<Node
>& tchildren
, CDProof
* cdp
)
650 size_t tsize
= tchildren
.size();
653 Node lhs
= tchildren
[0][0];
654 Node rhs
= tchildren
[tsize
- 1][1];
655 Node eq
= lhs
.eqNode(rhs
);
656 cdp
->addStep(eq
, PfRule::TRANS
, tchildren
, {});
666 Node
ProofPostprocessCallback::addProofForSubsStep(Node var
,
671 // ensure we have a proof of var = subs
672 Node veqs
= var
.eqNode(subs
);
675 // should be true intro or false intro
676 Assert(subs
.isConst());
679 subs
.getConst
<bool>() ? PfRule::TRUE_INTRO
: PfRule::FALSE_INTRO
,
686 bool ProofPostprocessCallback::addToTransChildren(Node eq
,
687 std::vector
<Node
>& tchildren
,
690 Assert(!eq
.isNull());
691 Assert(eq
.getKind() == kind::EQUAL
);
696 Node equ
= isSymm
? eq
[1].eqNode(eq
[0]) : eq
;
697 Assert(tchildren
.empty()
698 || (tchildren
[tchildren
.size() - 1].getKind() == kind::EQUAL
699 && tchildren
[tchildren
.size() - 1][1] == equ
[0]));
700 tchildren
.push_back(equ
);
704 ProofPostprocessFinalCallback::ProofPostprocessFinalCallback(
705 ProofNodeManager
* pnm
)
706 : d_ruleCount("finalProof::ruleCount"),
707 d_totalRuleCount("finalProof::totalRuleCount", 0),
708 d_minPedanticLevel("finalProof::minPedanticLevel", 10),
709 d_numFinalProofs("finalProofs::numFinalProofs", 0),
711 d_pedanticFailure(false)
713 smtStatisticsRegistry()->registerStat(&d_ruleCount
);
714 smtStatisticsRegistry()->registerStat(&d_totalRuleCount
);
715 smtStatisticsRegistry()->registerStat(&d_minPedanticLevel
);
716 smtStatisticsRegistry()->registerStat(&d_numFinalProofs
);
719 ProofPostprocessFinalCallback::~ProofPostprocessFinalCallback()
721 smtStatisticsRegistry()->unregisterStat(&d_ruleCount
);
722 smtStatisticsRegistry()->unregisterStat(&d_totalRuleCount
);
723 smtStatisticsRegistry()->unregisterStat(&d_minPedanticLevel
);
724 smtStatisticsRegistry()->unregisterStat(&d_numFinalProofs
);
727 void ProofPostprocessFinalCallback::initializeUpdate()
729 d_pedanticFailure
= false;
730 d_pedanticFailureOut
.str("");
734 bool ProofPostprocessFinalCallback::shouldUpdate(std::shared_ptr
<ProofNode
> pn
,
735 bool& continueUpdate
)
737 PfRule r
= pn
->getRule();
738 // if not doing eager pedantic checking, fail if below threshold
739 if (!options::proofNewPedanticEager())
741 if (!d_pedanticFailure
)
743 Assert(d_pedanticFailureOut
.str().empty());
744 if (d_pnm
->getChecker()->isPedanticFailure(r
, d_pedanticFailureOut
))
746 d_pedanticFailure
= true;
750 uint32_t plevel
= d_pnm
->getChecker()->getPedanticLevel(r
);
753 d_minPedanticLevel
.minAssign(plevel
);
755 // record stats for the rule
761 bool ProofPostprocessFinalCallback::wasPedanticFailure(std::ostream
& out
) const
763 if (d_pedanticFailure
)
765 out
<< d_pedanticFailureOut
.str();
771 ProofPostproccess::ProofPostproccess(ProofNodeManager
* pnm
,
773 ProofGenerator
* pppg
)
775 d_cb(pnm
, smte
, pppg
),
776 // the update merges subproofs
777 d_updater(d_pnm
, d_cb
, true),
779 d_finalizer(d_pnm
, d_finalCb
)
783 ProofPostproccess::~ProofPostproccess() {}
785 void ProofPostproccess::process(std::shared_ptr
<ProofNode
> pf
)
787 // Initialize the callback, which computes necessary static information about
788 // how to process, including how to process assumptions in pf.
789 d_cb
.initializeUpdate();
791 d_updater
.process(pf
);
792 // take stats and check pedantic
793 d_finalCb
.initializeUpdate();
794 d_finalizer
.process(pf
);
796 std::stringstream serr
;
797 bool wasPedanticFailure
= d_finalCb
.wasPedanticFailure(serr
);
798 if (wasPedanticFailure
)
800 AlwaysAssert(!wasPedanticFailure
)
801 << "ProofPostproccess::process: pedantic failure:" << std::endl
806 void ProofPostproccess::setEliminateRule(PfRule rule
)
808 d_cb
.setEliminateRule(rule
);