1 /******************************************************************************
2 * Top contributors (to current version):
3 * Andrew Reynolds, Haniel Barbosa, Aina Niemetz
5 * This file is part of the cvc5 project.
7 * Copyright (c) 2009-2021 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.
11 * ****************************************************************************
13 * Implementation of module for processing proof nodes.
16 #include "smt/proof_post_processor.h"
18 #include "expr/skolem_manager.h"
19 #include "options/proof_options.h"
20 #include "preprocessing/assertion_pipeline.h"
21 #include "proof/proof_node_manager.h"
22 #include "smt/smt_engine.h"
23 #include "theory/arith/arith_utilities.h"
24 #include "theory/builtin/proof_checker.h"
25 #include "theory/bv/bitblast/proof_bitblaster.h"
26 #include "theory/rewriter.h"
27 #include "theory/strings/infer_proof_cons.h"
28 #include "theory/theory.h"
29 #include "util/rational.h"
31 using namespace cvc5::kind
;
32 using namespace cvc5::theory
;
37 ProofPostprocessCallback::ProofPostprocessCallback(Env
& env
,
39 rewriter::RewriteDb
* rdb
,
40 bool updateScopedAssumptions
)
42 d_pnm(env
.getProofNodeManager()),
44 d_wfpm(env
.getProofNodeManager()),
45 d_updateScopedAssumptions(updateScopedAssumptions
)
47 d_true
= NodeManager::currentNM()->mkConst(true);
50 void ProofPostprocessCallback::initializeUpdate()
52 d_assumpToProof
.clear();
53 d_wfAssumptions
.clear();
56 void ProofPostprocessCallback::setEliminateRule(PfRule rule
)
58 d_elimRules
.insert(rule
);
61 bool ProofPostprocessCallback::shouldUpdate(std::shared_ptr
<ProofNode
> pn
,
62 const std::vector
<Node
>& fa
,
65 PfRule id
= pn
->getRule();
66 if (d_elimRules
.find(id
) != d_elimRules
.end())
70 // other than elimination rules, we always update assumptions as long as
71 // d_updateScopedAssumptions is true or they are *not* in scope, i.e., not in
73 if (id
!= PfRule::ASSUME
74 || (!d_updateScopedAssumptions
75 && std::find(fa
.begin(), fa
.end(), pn
->getResult()) != fa
.end()))
77 Trace("smt-proof-pp-debug")
78 << "... not updating in-scope assumption " << pn
->getResult() << "\n";
84 bool ProofPostprocessCallback::update(Node res
,
86 const std::vector
<Node
>& children
,
87 const std::vector
<Node
>& args
,
91 Trace("smt-proof-pp-debug") << "- Post process " << id
<< " " << children
92 << " / " << args
<< std::endl
;
94 if (id
== PfRule::ASSUME
)
96 // we cache based on the assumption node, not the proof node, since there
97 // may be multiple occurrences of the same node.
99 std::shared_ptr
<ProofNode
> pfn
;
100 std::map
<Node
, std::shared_ptr
<ProofNode
>>::iterator it
=
101 d_assumpToProof
.find(f
);
102 if (it
!= d_assumpToProof
.end())
104 Trace("smt-proof-pp-debug") << "...already computed" << std::endl
;
109 Trace("smt-proof-pp-debug") << "...get proof" << std::endl
;
110 Assert(d_pppg
!= nullptr);
111 // get proof from preprocess proof generator
112 pfn
= d_pppg
->getProofFor(f
);
113 Trace("smt-proof-pp-debug") << "...finished get proof" << std::endl
;
114 // print for debugging
117 Trace("smt-proof-pp-debug")
118 << "...no proof, possibly an input assumption" << std::endl
;
122 Assert(pfn
->getResult() == f
);
123 if (Trace
.isOn("smt-proof-pp"))
125 Trace("smt-proof-pp")
126 << "=== Connect proof for preprocessing: " << f
<< std::endl
;
127 Trace("smt-proof-pp") << *pfn
.get() << std::endl
;
130 d_assumpToProof
[f
] = pfn
;
132 if (pfn
== nullptr || pfn
->getRule() == PfRule::ASSUME
)
134 Trace("smt-proof-pp-debug") << "...do not add proof" << std::endl
;
138 Trace("smt-proof-pp-debug") << "...add proof" << std::endl
;
143 Node ret
= expandMacros(id
, children
, args
, cdp
);
144 Trace("smt-proof-pp-debug") << "...expanded = " << !ret
.isNull() << std::endl
;
145 return !ret
.isNull();
148 bool ProofPostprocessCallback::updateInternal(Node res
,
150 const std::vector
<Node
>& children
,
151 const std::vector
<Node
>& args
,
154 bool continueUpdate
= true;
155 return update(res
, id
, children
, args
, cdp
, continueUpdate
);
158 Node
ProofPostprocessCallback::eliminateCrowdingLits(
159 const std::vector
<Node
>& clauseLits
,
160 const std::vector
<Node
>& targetClauseLits
,
161 const std::vector
<Node
>& children
,
162 const std::vector
<Node
>& args
,
165 Trace("smt-proof-pp-debug2") << push
;
166 NodeManager
* nm
= NodeManager::currentNM();
167 Node trueNode
= nm
->mkConst(true);
168 // get crowding lits and the position of the last clause that includes
169 // them. The factoring step must be added after the last inclusion and before
171 std::unordered_set
<TNode
> crowding
;
172 std::vector
<std::pair
<Node
, size_t>> lastInclusion
;
173 // positions of eliminators of crowding literals, which are the positions of
174 // the clauses that eliminate crowding literals *after* their last inclusion
175 std::vector
<size_t> eliminators
;
176 for (size_t i
= 0, size
= clauseLits
.size(); i
< size
; ++i
)
178 if (!crowding
.count(clauseLits
[i
])
180 targetClauseLits
.begin(), targetClauseLits
.end(), clauseLits
[i
])
181 == targetClauseLits
.end())
183 Node crowdLit
= clauseLits
[i
];
184 crowding
.insert(crowdLit
);
185 Trace("smt-proof-pp-debug2") << "crowding lit " << crowdLit
<< "\n";
186 // found crowding lit, now get its last inclusion position, which is the
187 // position of the last resolution link that introduces the crowding
188 // literal. Note that this position has to be *before* the last link, as a
189 // link *after* the last inclusion must eliminate the crowding literal.
191 for (j
= children
.size() - 1; j
> 0; --j
)
193 // notice that only non-singleton clauses may be introducing the
194 // crowding literal, so we only care about non-singleton OR nodes. We
195 // check then against the kind and whether the whole OR node occurs as a
196 // pivot of the respective resolution
197 if (children
[j
- 1].getKind() != kind::OR
)
201 uint64_t pivotIndex
= 2 * (j
- 1);
202 if (args
[pivotIndex
] == children
[j
- 1]
203 || args
[pivotIndex
].notNode() == children
[j
- 1])
207 if (std::find(children
[j
- 1].begin(), children
[j
- 1].end(), crowdLit
)
208 != children
[j
- 1].end())
214 lastInclusion
.emplace_back(crowdLit
, j
- 1);
216 Trace("smt-proof-pp-debug2") << "last inc " << j
- 1 << "\n";
217 // get elimination position, starting from the following link as the last
218 // inclusion one. The result is the last (in the chain, but first from
219 // this point on) resolution link that eliminates the crowding literal. A
220 // literal l is eliminated by a link if it contains a literal l' with
221 // opposite polarity to l.
222 for (; j
< children
.size(); ++j
)
224 bool posFirst
= args
[(2 * j
) - 1] == trueNode
;
225 Node pivot
= args
[(2 * j
)];
226 Trace("smt-proof-pp-debug2")
227 << "\tcheck w/ args " << posFirst
<< " / " << pivot
<< "\n";
228 // To eliminate the crowding literal (crowdLit), the clause must contain
229 // it with opposite polarity. There are three successful cases,
230 // according to the pivot and its sign
232 // - crowdLit is the same as the pivot and posFirst is true, which means
233 // that the clause contains its negation and eliminates it
235 // - crowdLit is the negation of the pivot and posFirst is false, so the
236 // clause contains the node whose negation is crowdLit. Note that this
237 // case may either be crowdLit.notNode() == pivot or crowdLit ==
239 if ((crowdLit
== pivot
&& posFirst
)
240 || (crowdLit
.notNode() == pivot
&& !posFirst
)
241 || (pivot
.notNode() == crowdLit
&& !posFirst
))
243 Trace("smt-proof-pp-debug2") << "\t\tfound it!\n";
244 eliminators
.push_back(j
);
248 AlwaysAssert(j
< children
.size());
251 Assert(!lastInclusion
.empty());
252 // order map so that we process crowding literals in the order of the clauses
253 // that last introduce them
254 auto cmp
= [](std::pair
<Node
, size_t>& a
, std::pair
<Node
, size_t>& b
) {
255 return a
.second
< b
.second
;
257 std::sort(lastInclusion
.begin(), lastInclusion
.end(), cmp
);
259 std::sort(eliminators
.begin(), eliminators
.end());
260 if (Trace
.isOn("smt-proof-pp-debug"))
262 Trace("smt-proof-pp-debug") << "crowding lits last inclusion:\n";
263 for (const auto& pair
: lastInclusion
)
265 Trace("smt-proof-pp-debug")
266 << "\t- [" << pair
.second
<< "] : " << pair
.first
<< "\n";
268 Trace("smt-proof-pp-debug") << "eliminators:";
269 for (size_t elim
: eliminators
)
271 Trace("smt-proof-pp-debug") << " " << elim
;
273 Trace("smt-proof-pp-debug") << "\n";
275 // TODO (cvc4-wishues/issues/77): implement also simpler version and compare
277 // We now start to break the chain, one step at a time. Naively this breaking
278 // down would be one resolution/factoring to each crowding literal, but we can
279 // merge some of the cases. Effectively we do the following:
282 // lastClause children[start] ... children[end]
283 // ---------------------------------------------- CHAIN_RES
285 // ----------- FACTORING
286 // lastClause' children[start'] ... children[end']
287 // -------------------------------------------------------------- CHAIN_RES
291 // lastClause_0 = children[0]
293 // end_0 = eliminators[0] - 1
294 // start_i+1 = nextGuardedElimPos - 1
296 // The important point is how end_i+1 is computed. It is based on what we call
297 // the "nextGuardedElimPos", i.e., the next elimination position that requires
298 // removal of duplicates. The intuition is that a factoring step may eliminate
299 // the duplicates of crowding literals l1 and l2. If the last inclusion of l2
300 // is before the elimination of l1, then we can go ahead and also perform the
301 // elimination of l2 without another factoring. However if another literal l3
302 // has its last inclusion after the elimination of l2, then the elimination of
303 // l3 is the next guarded elimination.
305 // To do the above computation then we determine, after a resolution/factoring
306 // step, the first crowded literal to have its last inclusion after "end". The
307 // first elimination position to be bigger than the position of that crowded
308 // literal is the next guarded elimination position.
310 Node lastClause
= children
[0];
311 std::vector
<Node
> childrenRes
;
312 std::vector
<Node
> childrenResArgs
;
314 size_t nextGuardedElimPos
= eliminators
[0];
317 size_t start
= lastElim
+ 1;
318 size_t end
= nextGuardedElimPos
- 1;
319 Trace("smt-proof-pp-debug2")
320 << "res with:\n\tlastClause: " << lastClause
<< "\n\tstart: " << start
321 << "\n\tend: " << end
<< "\n";
322 childrenRes
.push_back(lastClause
);
323 // note that the interval of insert is exclusive in the end, so we add 1
324 childrenRes
.insert(childrenRes
.end(),
325 children
.begin() + start
,
326 children
.begin() + end
+ 1);
327 childrenResArgs
.insert(childrenResArgs
.end(),
328 args
.begin() + (2 * start
) - 1,
329 args
.begin() + (2 * end
) + 1);
330 Trace("smt-proof-pp-debug2") << "res children: " << childrenRes
<< "\n";
331 Trace("smt-proof-pp-debug2") << "res args: " << childrenResArgs
<< "\n";
332 resPlaceHolder
= d_pnm
->getChecker()->checkDebug(PfRule::CHAIN_RESOLUTION
,
337 Trace("smt-proof-pp-debug2")
338 << "resPlaceHorder: " << resPlaceHolder
<< "\n";
340 resPlaceHolder
, PfRule::CHAIN_RESOLUTION
, childrenRes
, childrenResArgs
);
341 // I need to add factoring if end < children.size(). Otherwise, this is
342 // to be handled by the caller
343 if (end
< children
.size() - 1)
345 lastClause
= d_pnm
->getChecker()->checkDebug(
346 PfRule::FACTORING
, {resPlaceHolder
}, {}, Node::null(), "");
347 if (!lastClause
.isNull())
349 cdp
->addStep(lastClause
, PfRule::FACTORING
, {resPlaceHolder
}, {});
353 lastClause
= resPlaceHolder
;
355 Trace("smt-proof-pp-debug2") << "lastClause: " << lastClause
<< "\n";
359 lastClause
= resPlaceHolder
;
362 // update for next round
364 childrenResArgs
.clear();
367 // find the position of the last inclusion of the next crowded literal
368 size_t nextCrowdedInclusionPos
= lastInclusion
.size();
369 for (size_t i
= 0, size
= lastInclusion
.size(); i
< size
; ++i
)
371 if (lastInclusion
[i
].second
> lastElim
)
373 nextCrowdedInclusionPos
= i
;
377 Trace("smt-proof-pp-debug2")
378 << "nextCrowdedInclusion/Pos: "
379 << lastInclusion
[nextCrowdedInclusionPos
].second
<< "/"
380 << nextCrowdedInclusionPos
<< "\n";
381 // if there is none, then the remaining literals will be used in the next
383 if (nextCrowdedInclusionPos
== lastInclusion
.size())
385 nextGuardedElimPos
= children
.size();
389 nextGuardedElimPos
= children
.size();
390 for (size_t i
= 0, size
= eliminators
.size(); i
< size
; ++i
)
392 // nextGuardedElimPos is the largest element of
393 // eliminators bigger the next crowded literal's last inclusion
394 if (eliminators
[i
] > lastInclusion
[nextCrowdedInclusionPos
].second
)
396 nextGuardedElimPos
= eliminators
[i
];
400 Assert(nextGuardedElimPos
< children
.size());
402 Trace("smt-proof-pp-debug2")
403 << "nextGuardedElimPos: " << nextGuardedElimPos
<< "\n";
405 Trace("smt-proof-pp-debug2") << pop
;
409 Node
ProofPostprocessCallback::expandMacros(PfRule id
,
410 const std::vector
<Node
>& children
,
411 const std::vector
<Node
>& args
,
414 if (d_elimRules
.find(id
) == d_elimRules
.end())
420 if (id
== PfRule::MACRO_SR_EQ_INTRO
)
423 // (SUBS <children> :args args[0:1])
424 // (REWRITE :args <t.substitute(x1,t1). ... .substitute(xn,tn)> args[2]))
425 std::vector
<Node
> tchildren
;
428 if (!children
.empty())
430 std::vector
<Node
> sargs
;
432 MethodId ids
= MethodId::SB_DEFAULT
;
433 if (args
.size() >= 2)
435 if (getMethodId(args
[1], ids
))
437 sargs
.push_back(args
[1]);
440 MethodId ida
= MethodId::SBA_SEQUENTIAL
;
441 if (args
.size() >= 3)
443 if (getMethodId(args
[2], ida
))
445 sargs
.push_back(args
[2]);
448 ts
= builtin::BuiltinProofRuleChecker::applySubstitution(
449 t
, children
, ids
, ida
);
450 Trace("smt-proof-pp-debug")
451 << "...eq intro subs equality is " << t
<< " == " << ts
<< ", from "
452 << ids
<< " " << ida
<< std::endl
;
455 Node eq
= t
.eqNode(ts
);
456 // apply SUBS proof rule if necessary
457 if (!updateInternal(eq
, PfRule::SUBS
, children
, sargs
, cdp
))
459 // if we specified that we did not want to eliminate, add as step
460 cdp
->addStep(eq
, PfRule::SUBS
, children
, sargs
);
462 tchildren
.push_back(eq
);
470 std::vector
<Node
> rargs
;
472 MethodId idr
= MethodId::RW_REWRITE
;
473 if (args
.size() >= 4)
475 if (getMethodId(args
[3], idr
))
477 rargs
.push_back(args
[3]);
480 Rewriter
* rr
= d_env
.getRewriter();
481 Node tr
= rr
->rewriteViaMethod(ts
, idr
);
482 Trace("smt-proof-pp-debug")
483 << "...eq intro rewrite equality is " << ts
<< " == " << tr
<< ", from "
487 Node eq
= ts
.eqNode(tr
);
488 // apply REWRITE proof rule
489 if (!updateInternal(eq
, PfRule::REWRITE
, {}, rargs
, cdp
))
491 // if not elimianted, add as step
492 cdp
->addStep(eq
, PfRule::REWRITE
, {}, rargs
);
494 tchildren
.push_back(eq
);
498 // typically not necessary, but done to be robust
499 cdp
->addStep(t
.eqNode(tr
), PfRule::REFL
, {}, {t
});
502 // must add TRANS if two step
503 return addProofForTrans(tchildren
, cdp
);
505 else if (id
== PfRule::MACRO_SR_PRED_INTRO
)
507 std::vector
<Node
> tchildren
;
508 std::vector
<Node
> sargs
= args
;
509 // take into account witness form, if necessary
510 bool reqWitness
= d_wfpm
.requiresWitnessFormIntro(args
[0]);
511 Trace("smt-proof-pp-debug")
512 << "...pred intro reqWitness=" << reqWitness
<< std::endl
;
515 // (MACRO_SR_EQ_INTRO <children> :args (t args[1:]))
516 // ... proof of apply_SR(t) = toWitness(apply_SR(t)) ...
517 // (MACRO_SR_EQ_INTRO {} {toWitness(apply_SR(t))})
519 // Notice this is an optimized, one sided version of the expansion of
520 // MACRO_SR_PRED_TRANSFORM below.
521 // We call the expandMacros method on MACRO_SR_EQ_INTRO, where notice
522 // that this rule application is immediately expanded in the recursive
523 // call and not added to the proof.
524 Node conc
= expandMacros(PfRule::MACRO_SR_EQ_INTRO
, children
, sargs
, cdp
);
525 Trace("smt-proof-pp-debug")
526 << "...pred intro conclusion is " << conc
<< std::endl
;
527 Assert(!conc
.isNull());
528 Assert(conc
.getKind() == EQUAL
);
529 Assert(conc
[0] == args
[0]);
530 tchildren
.push_back(conc
);
533 Node weq
= addProofForWitnessForm(conc
[1], cdp
);
534 Trace("smt-proof-pp-debug") << "...weq is " << weq
<< std::endl
;
535 if (addToTransChildren(weq
, tchildren
))
537 // toWitness(apply_SR(t)) = apply_SR(toWitness(apply_SR(t)))
538 // rewrite again, don't need substitution. Also we always use the
539 // default rewriter, due to the definition of MACRO_SR_PRED_INTRO.
540 Node weqr
= expandMacros(PfRule::MACRO_SR_EQ_INTRO
, {}, {weq
[1]}, cdp
);
541 addToTransChildren(weqr
, tchildren
);
544 // apply transitivity if necessary
545 Node eq
= addProofForTrans(tchildren
, cdp
);
546 Assert(!eq
.isNull());
547 Assert(eq
.getKind() == EQUAL
);
548 Assert(eq
[0] == args
[0]);
549 Assert(eq
[1] == d_true
);
551 cdp
->addStep(eq
[0], PfRule::TRUE_ELIM
, {eq
}, {});
554 else if (id
== PfRule::MACRO_SR_PRED_ELIM
)
558 // (MACRO_SR_EQ_INTRO children[1:] :args children[0] ++ args))
559 std::vector
<Node
> schildren(children
.begin() + 1, children
.end());
560 std::vector
<Node
> srargs
;
561 srargs
.push_back(children
[0]);
562 srargs
.insert(srargs
.end(), args
.begin(), args
.end());
563 Node conc
= expandMacros(PfRule::MACRO_SR_EQ_INTRO
, schildren
, srargs
, cdp
);
564 Assert(!conc
.isNull());
565 Assert(conc
.getKind() == EQUAL
);
566 Assert(conc
[0] == children
[0]);
567 // apply equality resolve
568 cdp
->addStep(conc
[1], PfRule::EQ_RESOLVE
, {children
[0], conc
}, {});
571 else if (id
== PfRule::MACRO_SR_PRED_TRANSFORM
)
576 // (MACRO_SR_EQ_INTRO children[1:] :args (children[0] args[1:]))
577 // ... proof of c = wc
578 // (MACRO_SR_EQ_INTRO {} wc)
580 // (MACRO_SR_EQ_INTRO children[1:] :args <args>)
581 // ... proof of a = wa
582 // (MACRO_SR_EQ_INTRO {} wa))))
584 // wa = toWitness(apply_SR(args[0])) and
585 // wc = toWitness(apply_SR(children[0])).
586 Trace("smt-proof-pp-debug")
587 << "Transform " << children
[0] << " == " << args
[0] << std::endl
;
588 if (CDProof::isSame(children
[0], args
[0]))
590 Trace("smt-proof-pp-debug") << "...nothing to do" << std::endl
;
594 std::vector
<Node
> tchildren
;
595 std::vector
<Node
> schildren(children
.begin() + 1, children
.end());
596 std::vector
<Node
> sargs
= args
;
597 // first, compute if we need
598 bool reqWitness
= d_wfpm
.requiresWitnessFormTransform(children
[0], args
[0]);
599 Trace("smt-proof-pp-debug") << "...reqWitness=" << reqWitness
<< std::endl
;
600 // convert both sides, in three steps, take symmetry of second chain
601 for (unsigned r
= 0; r
< 2; r
++)
603 std::vector
<Node
> tchildrenr
;
604 // first rewrite children[0], then args[0]
605 sargs
[0] = r
== 0 ? children
[0] : args
[0];
607 Node eq
= expandMacros(PfRule::MACRO_SR_EQ_INTRO
, schildren
, sargs
, cdp
);
608 Trace("smt-proof-pp-debug")
609 << "transform subs_rewrite (" << r
<< "): " << eq
<< std::endl
;
610 Assert(!eq
.isNull() && eq
.getKind() == EQUAL
&& eq
[0] == sargs
[0]);
611 addToTransChildren(eq
, tchildrenr
);
612 // apply_SR(t) = toWitness(apply_SR(t))
615 Node weq
= addProofForWitnessForm(eq
[1], cdp
);
616 Trace("smt-proof-pp-debug")
617 << "transform toWitness (" << r
<< "): " << weq
<< std::endl
;
618 if (addToTransChildren(weq
, tchildrenr
))
620 // toWitness(apply_SR(t)) = apply_SR(toWitness(apply_SR(t)))
621 // rewrite again, don't need substitution. Also, we always use the
622 // default rewriter, due to the definition of MACRO_SR_PRED_TRANSFORM.
624 expandMacros(PfRule::MACRO_SR_EQ_INTRO
, {}, {weq
[1]}, cdp
);
625 Trace("smt-proof-pp-debug") << "transform rewrite_witness (" << r
626 << "): " << weqr
<< std::endl
;
627 addToTransChildren(weqr
, tchildrenr
);
630 Trace("smt-proof-pp-debug")
631 << "transform connect (" << r
<< ")" << std::endl
;
632 // add to overall chain
635 // add the current chain to the overall chain
636 tchildren
.insert(tchildren
.end(), tchildrenr
.begin(), tchildrenr
.end());
640 // add the current chain to cdp
641 Node eqr
= addProofForTrans(tchildrenr
, cdp
);
644 Trace("smt-proof-pp-debug") << "transform connect sym " << tchildren
645 << " " << eqr
<< std::endl
;
646 // take symmetry of above and add it to the overall chain
647 addToTransChildren(eqr
, tchildren
, true);
650 Trace("smt-proof-pp-debug")
651 << "transform finish (" << r
<< ")" << std::endl
;
654 // apply transitivity if necessary
655 Node eq
= addProofForTrans(tchildren
, cdp
);
657 cdp
->addStep(args
[0], PfRule::EQ_RESOLVE
, {children
[0], eq
}, {});
660 else if (id
== PfRule::MACRO_RESOLUTION
661 || id
== PfRule::MACRO_RESOLUTION_TRUST
)
663 // first generate the naive chain_resolution
664 std::vector
<Node
> chainResArgs
{args
.begin() + 1, args
.end()};
665 Node chainConclusion
= d_pnm
->getChecker()->checkDebug(
666 PfRule::CHAIN_RESOLUTION
, children
, chainResArgs
, Node::null(), "");
667 Trace("smt-proof-pp-debug") << "Original conclusion: " << args
[0] << "\n";
668 Trace("smt-proof-pp-debug")
669 << "chainRes conclusion: " << chainConclusion
<< "\n";
670 // There are n cases:
671 // - if the conclusion is the same, just replace
672 // - if they have the same literals but in different quantity, add a
674 // - if the order is not the same, add a REORDERING step
675 // - if there are literals in chainConclusion that are not in the original
676 // conclusion, we need to transform the MACRO_RESOLUTION into a series of
677 // CHAIN_RESOLUTION + FACTORING steps, so that we explicitly eliminate all
678 // these "crowding" literals. We do this via FACTORING so we avoid adding
679 // an exponential number of premises, which would happen if we just
680 // repeated in the premises the clauses needed for eliminating crowding
681 // literals, which could themselves add crowding literals.
682 if (chainConclusion
== args
[0])
685 chainConclusion
, PfRule::CHAIN_RESOLUTION
, children
, chainResArgs
);
686 return chainConclusion
;
688 NodeManager
* nm
= NodeManager::currentNM();
689 // If we got here, then chainConclusion is NECESSARILY an OR node
690 Assert(chainConclusion
.getKind() == kind::OR
);
691 // get the literals in the chain conclusion
692 std::vector
<Node
> chainConclusionLits
{chainConclusion
.begin(),
693 chainConclusion
.end()};
694 std::set
<Node
> chainConclusionLitsSet
{chainConclusion
.begin(),
695 chainConclusion
.end()};
696 // is args[0] a singleton clause? If it's not an OR node, then yes.
697 // Otherwise, it's only a singleton if it occurs in chainConclusionLitsSet
698 std::vector
<Node
> conclusionLits
;
699 // whether conclusion is singleton
700 if (chainConclusionLitsSet
.count(args
[0]))
702 conclusionLits
.push_back(args
[0]);
706 Assert(args
[0].getKind() == kind::OR
);
707 conclusionLits
.insert(
708 conclusionLits
.end(), args
[0].begin(), args
[0].end());
710 std::set
<Node
> conclusionLitsSet
{conclusionLits
.begin(),
711 conclusionLits
.end()};
712 // If the sets are different, there are "crowding" literals, i.e. literals
713 // that were removed by implicit multi-usage of premises in the resolution
715 if (chainConclusionLitsSet
!= conclusionLitsSet
)
717 chainConclusion
= eliminateCrowdingLits(
718 chainConclusionLits
, conclusionLits
, children
, args
, cdp
);
719 // update vector of lits. Note that the set is no longer used, so we don't
722 // We need again to check whether chainConclusion is a singleton
723 // clause. As above, it's a singleton if it's in the original
724 // chainConclusionLitsSet.
725 chainConclusionLits
.clear();
726 if (chainConclusionLitsSet
.count(chainConclusion
))
728 chainConclusionLits
.push_back(chainConclusion
);
732 Assert(chainConclusion
.getKind() == kind::OR
);
733 chainConclusionLits
.insert(chainConclusionLits
.end(),
734 chainConclusion
.begin(),
735 chainConclusion
.end());
741 chainConclusion
, PfRule::CHAIN_RESOLUTION
, children
, chainResArgs
);
743 Trace("smt-proof-pp-debug")
744 << "Conclusion after chain_res/elimCrowd: " << chainConclusion
<< "\n";
745 Trace("smt-proof-pp-debug")
746 << "Conclusion lits: " << chainConclusionLits
<< "\n";
747 // Placeholder for running conclusion
748 Node n
= chainConclusion
;
750 if (chainConclusionLits
.size() != conclusionLits
.size())
752 // We build it rather than taking conclusionLits because the order may be
754 std::vector
<Node
> factoredLits
;
755 std::unordered_set
<TNode
> clauseSet
;
756 for (size_t i
= 0, size
= chainConclusionLits
.size(); i
< size
; ++i
)
758 if (clauseSet
.count(chainConclusionLits
[i
]))
762 factoredLits
.push_back(n
[i
]);
763 clauseSet
.insert(n
[i
]);
765 Node factored
= factoredLits
.empty()
767 : factoredLits
.size() == 1
769 : nm
->mkNode(kind::OR
, factoredLits
);
770 cdp
->addStep(factored
, PfRule::FACTORING
, {n
}, {});
773 // either same node or n as a clause
774 Assert(n
== args
[0] || n
.getKind() == kind::OR
);
778 cdp
->addStep(args
[0], PfRule::REORDERING
, {n
}, {args
[0]});
782 else if (id
== PfRule::SUBS
)
784 NodeManager
* nm
= NodeManager::currentNM();
785 // Notice that a naive way to reconstruct SUBS is to do a term conversion
786 // proof for each substitution.
787 // The proof of f(a) * { a -> g(b) } * { b -> c } = f(g(c)) is:
788 // TRANS( CONG{f}( a=g(b) ), CONG{f}( CONG{g}( b=c ) ) )
789 // Notice that more optimal proofs are possible that do a single traversal
790 // over t. This is done by applying later substitutions to the range of
791 // previous substitutions, until a final simultaneous substitution is
792 // applied to t. For instance, in the above example, we first prove:
794 // by applying the second substitution { b -> c } to the range of the first,
795 // giving us a proof of g(b)=g(c). We then construct the updated proof
797 // TRANS( a=g(b), CONG{g}( b=c ) )
798 // We then apply the substitution { a -> g(c), b -> c } to f(a), to obtain:
799 // CONG{f}( TRANS( a=g(b), CONG{g}( b=c ) ) )
800 // which notice is more compact than the proof above.
802 // get the kind of substitution
803 MethodId ids
= MethodId::SB_DEFAULT
;
804 if (args
.size() >= 2)
806 getMethodId(args
[1], ids
);
808 MethodId ida
= MethodId::SBA_SEQUENTIAL
;
809 if (args
.size() >= 3)
811 getMethodId(args
[2], ida
);
813 std::vector
<std::shared_ptr
<CDProof
>> pfs
;
814 std::vector
<TNode
> vsList
;
815 std::vector
<TNode
> ssList
;
816 std::vector
<TNode
> fromList
;
817 std::vector
<ProofGenerator
*> pgs
;
818 // first, compute the entire substitution
819 for (size_t i
= 0, nchild
= children
.size(); i
< nchild
; i
++)
821 // get the substitution
822 builtin::BuiltinProofRuleChecker::getSubstitutionFor(
823 children
[i
], vsList
, ssList
, fromList
, ids
);
824 // ensure proofs for each formula in fromList
825 if (children
[i
].getKind() == AND
&& ids
== MethodId::SB_DEFAULT
)
827 for (size_t j
= 0, nchildi
= children
[i
].getNumChildren(); j
< nchildi
;
830 Node nodej
= nm
->mkConst(Rational(j
));
832 children
[i
][j
], PfRule::AND_ELIM
, {children
[i
]}, {nodej
});
836 std::vector
<Node
> vvec
;
837 std::vector
<Node
> svec
;
838 for (size_t i
= 0, nvs
= vsList
.size(); i
< nvs
; i
++)
840 // Note we process in forward order, since later substitution should be
841 // applied to earlier ones, and the last child of a SUBS is processed
843 TNode var
= vsList
[i
];
844 TNode subs
= ssList
[i
];
845 TNode childFrom
= fromList
[i
];
846 Trace("smt-proof-pp-debug")
847 << "...process " << var
<< " -> " << subs
<< " (" << childFrom
<< ", "
848 << ids
<< ")" << std::endl
;
849 // apply the current substitution to the range
850 if (!vvec
.empty() && ida
== MethodId::SBA_SEQUENTIAL
)
853 subs
.substitute(vvec
.begin(), vvec
.end(), svec
.begin(), svec
.end());
856 Trace("smt-proof-pp-debug")
857 << "......updated to " << var
<< " -> " << ss
858 << " based on previous substitution" << std::endl
;
859 // make the proof for the tranitivity step
860 std::shared_ptr
<CDProof
> pf
= std::make_shared
<CDProof
>(d_pnm
);
862 // prove the updated substitution
863 TConvProofGenerator
tcg(d_pnm
,
866 TConvCachePolicy::NEVER
,
867 "nested_SUBS_TConvProofGenerator",
870 // add previous rewrite steps
871 for (unsigned j
= 0, nvars
= vvec
.size(); j
< nvars
; j
++)
873 // substitutions are pre-rewrites
874 tcg
.addRewriteStep(vvec
[j
], svec
[j
], pgs
[j
], true);
876 // get the proof for the update to the current substitution
877 Node seqss
= subs
.eqNode(ss
);
878 std::shared_ptr
<ProofNode
> pfn
= tcg
.getProofFor(seqss
);
879 Assert(pfn
!= nullptr);
882 // get proof for childFrom from cdp
883 pfn
= cdp
->getProofFor(childFrom
);
885 // ensure we have a proof of var = subs
886 Node veqs
= addProofForSubsStep(var
, subs
, childFrom
, pf
.get());
888 pf
->addStep(var
.eqNode(ss
), PfRule::TRANS
, {veqs
, seqss
}, {});
889 // add to the substitution
892 pgs
.push_back(pf
.get());
896 // Just use equality from CDProof, but ensure we have a proof in cdp.
897 // This may involve a TRUE_INTRO/FALSE_INTRO if the substitution step
898 // uses the assumption childFrom as a Boolean assignment (e.g.
899 // childFrom = true if we are using MethodId::SB_LITERAL).
900 addProofForSubsStep(var
, subs
, childFrom
, cdp
);
902 svec
.push_back(subs
);
905 // should be implied by the substitution now
906 TConvPolicy tcpolicy
= ida
== MethodId::SBA_FIXPOINT
? TConvPolicy::FIXPOINT
908 TConvProofGenerator
tcpg(d_pnm
,
911 TConvCachePolicy::NEVER
,
912 "SUBS_TConvProofGenerator",
915 for (unsigned j
= 0, nvars
= vvec
.size(); j
< nvars
; j
++)
917 // substitutions are pre-rewrites
918 tcpg
.addRewriteStep(vvec
[j
], svec
[j
], pgs
[j
], true);
920 // add the proof constructed by the term conversion utility
921 std::shared_ptr
<ProofNode
> pfn
= tcpg
.getProofForRewriting(t
);
922 Node eq
= pfn
->getResult();
923 Node ts
= builtin::BuiltinProofRuleChecker::applySubstitution(
924 t
, children
, ids
, ida
);
925 Node eqq
= t
.eqNode(ts
);
930 // should give a proof, if not, then tcpg does not agree with the
934 Warning() << "resort to TRUST_SUBS" << std::endl
937 << "from " << children
<< " applied to " << t
<< std::endl
;
938 cdp
->addStep(eqq
, PfRule::TRUST_SUBS
, {}, {eqq
});
946 else if (id
== PfRule::REWRITE
)
948 // get the kind of rewrite
949 MethodId idr
= MethodId::RW_REWRITE
;
950 TheoryId theoryId
= Theory::theoryOf(args
[0]);
951 if (args
.size() >= 2)
953 getMethodId(args
[1], idr
);
955 Rewriter
* rr
= d_env
.getRewriter();
956 Node ret
= rr
->rewriteViaMethod(args
[0], idr
);
957 Node eq
= args
[0].eqNode(ret
);
958 if (idr
== MethodId::RW_REWRITE
|| idr
== MethodId::RW_REWRITE_EQ_EXT
)
960 // rewrites from theory::Rewriter
961 bool isExtEq
= (idr
== MethodId::RW_REWRITE_EQ_EXT
);
962 // use rewrite with proof interface
963 TrustNode trn
= rr
->rewriteWithProof(args
[0], isExtEq
);
964 std::shared_ptr
<ProofNode
> pfn
= trn
.toProofNode();
967 Trace("smt-proof-pp-debug")
968 << "Use TRUST_REWRITE for " << eq
<< std::endl
;
969 // did not have a proof of rewriting, probably isExtEq is true
972 // update to THEORY_REWRITE with idr
973 Assert(args
.size() >= 1);
974 Node tid
= builtin::BuiltinProofRuleChecker::mkTheoryIdNode(theoryId
);
975 cdp
->addStep(eq
, PfRule::THEORY_REWRITE
, {}, {eq
, tid
, args
[1]});
979 // this should never be applied
980 cdp
->addStep(eq
, PfRule::TRUST_REWRITE
, {}, {eq
});
987 Assert(trn
.getNode() == ret
)
988 << "Unexpected rewrite " << args
[0] << std::endl
989 << "Got: " << trn
.getNode() << std::endl
990 << "Expected: " << ret
;
992 else if (idr
== MethodId::RW_EVALUATE
)
994 // change to evaluate, which is never eliminated
995 cdp
->addStep(eq
, PfRule::EVALUATE
, {}, {args
[0]});
999 // try to reconstruct as a standalone rewrite
1000 std::vector
<Node
> targs
;
1001 targs
.push_back(eq
);
1003 builtin::BuiltinProofRuleChecker::mkTheoryIdNode(theoryId
));
1004 // in this case, must be a non-standard rewrite kind
1005 Assert(args
.size() >= 2);
1006 targs
.push_back(args
[1]);
1007 Node eqp
= expandMacros(PfRule::THEORY_REWRITE
, {}, targs
, cdp
);
1010 // don't know how to eliminate
1011 return Node::null();
1016 // should not be necessary typically
1017 cdp
->addStep(eq
, PfRule::REFL
, {}, {args
[0]});
1021 else if (id
== PfRule::THEORY_REWRITE
)
1023 Assert(!args
.empty());
1025 Assert(eq
.getKind() == EQUAL
);
1026 // try to replay theory rewrite
1027 // first, check that maybe its just an evaluation step
1028 ProofChecker
* pc
= d_pnm
->getChecker();
1030 pc
->checkDebug(PfRule::EVALUATE
, {}, {eq
[0]}, eq
, "smt-proof-pp-debug");
1031 if (!ceval
.isNull() && ceval
== eq
)
1033 cdp
->addStep(eq
, PfRule::EVALUATE
, {}, {eq
[0]});
1036 // otherwise no update
1037 Trace("final-pf-hole") << "hole: " << id
<< " : " << eq
<< std::endl
;
1039 else if (id
== PfRule::MACRO_ARITH_SCALE_SUM_UB
)
1041 Debug("macro::arith") << "Expand MACRO_ARITH_SCALE_SUM_UB" << std::endl
;
1042 if (Debug
.isOn("macro::arith"))
1044 for (const auto& child
: children
)
1046 Debug("macro::arith") << " child: " << child
<< std::endl
;
1048 Debug("macro::arith") << " args: " << args
<< std::endl
;
1050 Assert(args
.size() == children
.size());
1051 NodeManager
* nm
= NodeManager::currentNM();
1052 ProofStepBuffer steps
{d_pnm
->getChecker()};
1054 // Scale all children, accumulating
1055 std::vector
<Node
> scaledRels
;
1056 for (size_t i
= 0; i
< children
.size(); ++i
)
1058 TNode child
= children
[i
];
1059 TNode scalar
= args
[i
];
1060 bool isPos
= scalar
.getConst
<Rational
>() > 0;
1062 nm
->mkNode(isPos
? GT
: LT
, scalar
, nm
->mkConst(Rational(0)));
1063 // (= scalarCmp true)
1064 Node scalarCmpOrTrue
= steps
.tryStep(PfRule::EVALUATE
, {}, {scalarCmp
});
1065 Assert(!scalarCmpOrTrue
.isNull());
1067 steps
.addStep(PfRule::TRUE_ELIM
, {scalarCmpOrTrue
}, {}, scalarCmp
);
1068 // (and scalarCmp relation)
1069 Node scalarCmpAndRel
=
1070 steps
.tryStep(PfRule::AND_INTRO
, {scalarCmp
, child
}, {});
1071 Assert(!scalarCmpAndRel
.isNull());
1072 // (=> (and scalarCmp relation) scaled)
1074 steps
.tryStep(isPos
? PfRule::ARITH_MULT_POS
: PfRule::ARITH_MULT_NEG
,
1077 Assert(!impl
.isNull());
1080 steps
.tryStep(PfRule::MODUS_PONENS
, {scalarCmpAndRel
, impl
}, {});
1081 Assert(!scaled
.isNull());
1082 scaledRels
.emplace_back(scaled
);
1085 Node sumBounds
= steps
.tryStep(PfRule::ARITH_SUM_UB
, scaledRels
, {});
1086 cdp
->addSteps(steps
);
1087 Debug("macro::arith") << "Expansion done. Proved: " << sumBounds
1091 else if (id
== PfRule::STRING_INFERENCE
)
1093 // get the arguments
1097 std::vector
<Node
> exp
;
1098 if (strings::InferProofCons::unpackArgs(args
, conc
, iid
, isRev
, exp
))
1100 if (strings::InferProofCons::addProofTo(cdp
, conc
, iid
, isRev
, exp
))
1106 else if (id
== PfRule::BV_BITBLAST
)
1108 bv::BBProof
bb(nullptr, d_pnm
, true);
1110 Assert(eq
.getKind() == EQUAL
);
1112 Node bbAtom
= bb
.getStoredBBAtom(eq
[0]);
1113 bb
.getProofGenerator()->addProofTo(eq
[0].eqNode(bbAtom
), cdp
);
1117 // TRUST, PREPROCESS, THEORY_LEMMA, THEORY_PREPROCESS?
1119 return Node::null();
1122 Node
ProofPostprocessCallback::addProofForWitnessForm(Node t
, CDProof
* cdp
)
1124 Node tw
= SkolemManager::getOriginalForm(t
);
1125 Node eq
= t
.eqNode(tw
);
1128 // not necessary, add REFL step
1129 cdp
->addStep(eq
, PfRule::REFL
, {}, {t
});
1132 std::shared_ptr
<ProofNode
> pn
= d_wfpm
.getProofFor(eq
);
1140 Assert(false) << "ProofPostprocessCallback::addProofForWitnessForm: failed "
1141 "to add proof for witness form of "
1147 Node
ProofPostprocessCallback::addProofForTrans(
1148 const std::vector
<Node
>& tchildren
, CDProof
* cdp
)
1150 size_t tsize
= tchildren
.size();
1153 Node lhs
= tchildren
[0][0];
1154 Node rhs
= tchildren
[tsize
- 1][1];
1155 Node eq
= lhs
.eqNode(rhs
);
1156 cdp
->addStep(eq
, PfRule::TRANS
, tchildren
, {});
1159 else if (tsize
== 1)
1161 return tchildren
[0];
1163 return Node::null();
1166 Node
ProofPostprocessCallback::addProofForSubsStep(Node var
,
1171 // ensure we have a proof of var = subs
1172 Node veqs
= var
.eqNode(subs
);
1175 // should be true intro or false intro
1176 Assert(subs
.isConst());
1179 subs
.getConst
<bool>() ? PfRule::TRUE_INTRO
: PfRule::FALSE_INTRO
,
1186 bool ProofPostprocessCallback::addToTransChildren(Node eq
,
1187 std::vector
<Node
>& tchildren
,
1190 Assert(!eq
.isNull());
1191 Assert(eq
.getKind() == kind::EQUAL
);
1196 Node equ
= isSymm
? eq
[1].eqNode(eq
[0]) : eq
;
1197 Assert(tchildren
.empty()
1198 || (tchildren
[tchildren
.size() - 1].getKind() == kind::EQUAL
1199 && tchildren
[tchildren
.size() - 1][1] == equ
[0]));
1200 tchildren
.push_back(equ
);
1204 ProofPostproccess::ProofPostproccess(Env
& env
,
1205 ProofGenerator
* pppg
,
1206 rewriter::RewriteDb
* rdb
,
1207 bool updateScopedAssumptions
)
1208 : d_cb(env
, pppg
, rdb
, updateScopedAssumptions
),
1209 // the update merges subproofs
1210 d_updater(env
.getProofNodeManager(), d_cb
, options::proofPpMerge()),
1211 d_finalCb(env
.getProofNodeManager()),
1212 d_finalizer(env
.getProofNodeManager(), d_finalCb
)
1216 ProofPostproccess::~ProofPostproccess() {}
1218 void ProofPostproccess::process(std::shared_ptr
<ProofNode
> pf
)
1220 // Initialize the callback, which computes necessary static information about
1221 // how to process, including how to process assumptions in pf.
1222 d_cb
.initializeUpdate();
1224 d_updater
.process(pf
);
1225 // take stats and check pedantic
1226 d_finalCb
.initializeUpdate();
1227 d_finalizer
.process(pf
);
1229 std::stringstream serr
;
1230 bool wasPedanticFailure
= d_finalCb
.wasPedanticFailure(serr
);
1231 if (wasPedanticFailure
)
1233 AlwaysAssert(!wasPedanticFailure
)
1234 << "ProofPostproccess::process: pedantic failure:" << std::endl
1239 void ProofPostproccess::setEliminateRule(PfRule rule
)
1241 d_cb
.setEliminateRule(rule
);