Branch data Line data Source code
1 : : /******************************************************************************
2 : : * This file is part of the cvc5 project.
3 : : *
4 : : * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
5 : : * in the top-level source directory and their institutional affiliations.
6 : : * All rights reserved. See the file COPYING in the top-level source
7 : : * directory for licensing information.
8 : : * ****************************************************************************
9 : : *
10 : : * Implementation of module for processing proof nodes.
11 : : */
12 : :
13 : : #include "smt/proof_post_processor.h"
14 : :
15 : : #include "expr/skolem_manager.h"
16 : : #include "options/base_options.h"
17 : : #include "options/proof_options.h"
18 : : #include "preprocessing/assertion_pipeline.h"
19 : : #include "proof/proof_node_algorithm.h"
20 : : #include "proof/proof_node_manager.h"
21 : : #include "proof/resolution_proofs_util.h"
22 : : #include "proof/subtype_elim_proof_converter.h"
23 : : #include "theory/arith/arith_proof_utilities.h"
24 : : #include "theory/arith/arith_utilities.h"
25 : : #include "theory/builtin/proof_checker.h"
26 : : #include "theory/bv/bitblast/bitblast_proof_generator.h"
27 : : #include "theory/bv/bitblast/proof_bitblaster.h"
28 : : #include "theory/rewriter.h"
29 : : #include "theory/strings/infer_proof_cons.h"
30 : : #include "theory/theory.h"
31 : : #include "util/rational.h"
32 : :
33 : : using namespace cvc5::internal::kind;
34 : : using namespace cvc5::internal::theory;
35 : :
36 : : namespace cvc5::internal {
37 : : namespace smt {
38 : :
39 : 18896 : ProofPostprocessCallback::ProofPostprocessCallback(Env& env,
40 : 18896 : bool updateScopedAssumptions)
41 : : : EnvObj(env),
42 : 18896 : d_pc(nullptr),
43 : 18896 : d_pppg(nullptr),
44 : 18896 : d_wfpm(env),
45 : 18896 : d_macroExpand(statisticsRegistry().registerHistogram<ProofRule>(
46 : : "ProofPostprocessCallback::macroExpandCount")),
47 : 56688 : d_updateScopedAssumptions(updateScopedAssumptions)
48 : : {
49 : 18896 : d_true = nodeManager()->mkConst(true);
50 : 18896 : }
51 : :
52 : 13591 : void ProofPostprocessCallback::initializeUpdate(ProofGenerator* pppg)
53 : : {
54 : 13591 : d_pppg = pppg;
55 : 13591 : d_assumpToProof.clear();
56 : 13591 : d_wfAssumptions.clear();
57 : 13591 : d_pc = d_env.getProofNodeManager()->getChecker();
58 : 13591 : }
59 : :
60 : 103525 : void ProofPostprocessCallback::setEliminateRule(ProofRule rule)
61 : : {
62 : 103525 : d_elimRules.insert(rule);
63 : 103525 : }
64 : :
65 : 7522291 : bool ProofPostprocessCallback::shouldUpdate(std::shared_ptr<ProofNode> pn,
66 : : const std::vector<Node>& fa,
67 : : bool& continueUpdate)
68 : : {
69 : 7522291 : ProofRule id = pn->getRule();
70 [ + + ]: 7522291 : if (shouldExpand(id))
71 : : {
72 : 406041 : return true;
73 : : }
74 : : // other than elimination rules, we always update assumptions as long as
75 : : // d_updateScopedAssumptions is true or they are *not* in scope, i.e., not in
76 : : // fa
77 [ + + ]: 7116250 : if (id != ProofRule::ASSUME)
78 : : {
79 : 5902732 : return false;
80 : : }
81 : 2427036 : if (!d_updateScopedAssumptions
82 [ + + ][ + + ]: 1213518 : && std::find(fa.begin(), fa.end(), pn->getResult()) != fa.end())
[ + + ][ + + ]
[ - - ]
83 : : {
84 [ + - ]: 325008 : Trace("smt-proof-pp-debug")
85 [ - + ][ - - ]: 162504 : << "... not updating in-scope assumption " << pn->getResult() << "\n";
86 : 162504 : return false;
87 : : }
88 : 1051014 : return true;
89 : : }
90 : :
91 : 7039490 : bool ProofPostprocessCallback::shouldUpdatePost(std::shared_ptr<ProofNode> pn,
92 : : const std::vector<Node>& fa)
93 : : {
94 : 7039490 : return false;
95 : : }
96 : :
97 : 1760993 : bool ProofPostprocessCallback::update(Node res,
98 : : ProofRule id,
99 : : const std::vector<Node>& children,
100 : : const std::vector<Node>& args,
101 : : CDProof* cdp,
102 : : bool& continueUpdate)
103 : : {
104 [ + - ]: 3521986 : Trace("smt-proof-pp-debug") << "- Post process " << id << " " << children
105 : 1760993 : << " / " << args << std::endl;
106 : :
107 [ + + ]: 1760993 : if (id == ProofRule::ASSUME)
108 : : {
109 : : // we cache based on the assumption node, not the proof node, since there
110 : : // may be multiple occurrences of the same node.
111 : 1051014 : Node f = args[0];
112 : 1051014 : std::shared_ptr<ProofNode> pfn;
113 : : std::map<Node, std::shared_ptr<ProofNode>>::iterator it =
114 : 1051014 : d_assumpToProof.find(f);
115 [ + + ]: 1051014 : if (it != d_assumpToProof.end())
116 : : {
117 [ + - ]: 895731 : Trace("smt-proof-pp-debug") << "...already computed" << std::endl;
118 : 895731 : pfn = it->second;
119 : : }
120 : : else
121 : : {
122 [ + - ]: 155283 : Trace("smt-proof-pp-debug") << "...get proof" << std::endl;
123 [ - + ][ - + ]: 155283 : Assert(d_pppg != nullptr);
[ - - ]
124 : : // get proof from preprocess proof generator
125 : 155283 : pfn = d_pppg->getProofFor(f);
126 [ + - ]: 155283 : Trace("smt-proof-pp-debug") << "...finished get proof" << std::endl;
127 : : // print for debugging
128 [ + + ]: 155283 : if (pfn == nullptr)
129 : : {
130 [ + - ]: 132036 : Trace("smt-proof-pp-debug")
131 : 66018 : << "...no proof, possibly an input assumption" << std::endl;
132 : : }
133 : : else
134 : : {
135 [ - + ][ - + ]: 89265 : Assert(pfn->getResult() == f);
[ - - ]
136 [ - + ]: 89265 : if (TraceIsOn("smt-proof-pp"))
137 : : {
138 [ - - ]: 0 : Trace("smt-proof-pp")
139 : 0 : << "=== Connect proof for preprocessing: " << f << std::endl;
140 [ - - ]: 0 : Trace("smt-proof-pp") << *pfn.get() << std::endl;
141 : : }
142 : : }
143 : 155283 : d_assumpToProof[f] = pfn;
144 : : }
145 [ + + ][ + + ]: 1051014 : if (pfn == nullptr || pfn->getRule() == ProofRule::ASSUME)
[ + + ]
146 : : {
147 [ + - ]: 993544 : Trace("smt-proof-pp-debug") << "...do not add proof" << std::endl;
148 : : // no update
149 : 993544 : return false;
150 : : }
151 [ + - ]: 57470 : Trace("smt-proof-pp-debug") << "...add proof" << std::endl;
152 : : // connect the proof
153 : 57470 : cdp->addProof(pfn);
154 : 57470 : return true;
155 : 1051014 : }
156 : 709979 : Node ret = expandMacros(id, children, args, cdp, res);
157 [ + - ]: 709979 : Trace("smt-proof-pp-debug") << "...expanded = " << !ret.isNull() << std::endl;
158 : 709979 : return !ret.isNull();
159 : 709979 : }
160 : :
161 : 303938 : bool ProofPostprocessCallback::updateInternal(Node res,
162 : : ProofRule id,
163 : : const std::vector<Node>& children,
164 : : const std::vector<Node>& args,
165 : : CDProof* cdp)
166 : : {
167 : 303938 : bool continueUpdate = true;
168 : 303938 : return update(res, id, children, args, cdp, continueUpdate);
169 : : }
170 : :
171 : 8671744 : bool ProofPostprocessCallback::shouldExpand(ProofRule id) const
172 : : {
173 : 8671744 : return d_elimRules.find(id) != d_elimRules.end();
174 : : }
175 : :
176 : 1149453 : Node ProofPostprocessCallback::expandMacros(ProofRule id,
177 : : const std::vector<Node>& children,
178 : : const std::vector<Node>& args,
179 : : CDProof* cdp,
180 : : Node res)
181 : : {
182 [ - + ]: 1149453 : if (!shouldExpand(id))
183 : : {
184 : : // not eliminated
185 : 0 : return Node::null();
186 : : }
187 : 1149453 : d_macroExpand << id;
188 [ + - ]: 1149453 : Trace("smt-proof-pp-debug") << "Expand macro " << id << std::endl;
189 [ + + ]: 1149453 : if (id == ProofRule::TRUST)
190 : : {
191 : : TrustId tid;
192 : 19811 : getTrustId(args[0], tid);
193 : : // maybe we can show it rewrites to true based on rewriting
194 : : // modulo original forms (MACRO_SR_PRED_INTRO).
195 : 19811 : TheoryProofStepBuffer psb(d_pc);
196 [ + + ]: 19811 : if (psb.applyPredIntro(
197 : : res, {}, MethodId::SB_DEFAULT, MethodId::SBA_SEQUENTIAL))
198 : : {
199 : 975 : cdp->addSteps(psb);
200 : 975 : return res;
201 : : }
202 : 18836 : return Node::null();
203 : 19811 : }
204 : : // macro elimination
205 [ + + ]: 1129642 : if (id == ProofRule::MACRO_SR_EQ_INTRO)
206 : : {
207 : : // (TRANS
208 : : // (SUBS <children> :args args[0:1])
209 : : // (REWRITE :args <t.substitute(x1,t1). ... .substitute(xn,tn)> args[2]))
210 : 467107 : std::vector<Node> tchildren;
211 : 467107 : Node t = args[0];
212 : 467107 : Node ts;
213 [ + + ]: 467107 : if (!children.empty())
214 : : {
215 : 24756 : std::vector<Node> sargs;
216 : 24756 : sargs.push_back(t);
217 : 24756 : MethodId ids = MethodId::SB_DEFAULT;
218 [ + + ]: 24756 : if (args.size() >= 2)
219 : : {
220 [ + - ]: 9692 : if (getMethodId(args[1], ids))
221 : : {
222 : 9692 : sargs.push_back(args[1]);
223 : : }
224 : : }
225 : 24756 : MethodId ida = MethodId::SBA_SEQUENTIAL;
226 [ + + ]: 24756 : if (args.size() >= 3)
227 : : {
228 [ + - ]: 9518 : if (getMethodId(args[2], ida))
229 : : {
230 : 9518 : sargs.push_back(args[2]);
231 : : }
232 : : }
233 : 49512 : ts = builtin::BuiltinProofRuleChecker::applySubstitution(
234 : 24756 : t, children, ids, ida);
235 [ + - ]: 49512 : Trace("smt-proof-pp-debug")
236 : 0 : << "...eq intro subs equality is " << t << " == " << ts << ", from "
237 : 24756 : << ids << " " << ida << std::endl;
238 [ + + ]: 24756 : if (ts != t)
239 : : {
240 : 17329 : Node eq = t.eqNode(ts);
241 : : // apply SUBS proof rule if necessary
242 [ - + ]: 17329 : if (!updateInternal(eq, ProofRule::SUBS, children, sargs, cdp))
243 : : {
244 : : // if we specified that we did not want to eliminate, add as step
245 : 0 : cdp->addStep(eq, ProofRule::SUBS, children, sargs);
246 : : }
247 : 17329 : tchildren.push_back(eq);
248 : 17329 : }
249 : 24756 : }
250 : : else
251 : : {
252 : : // no substitute
253 : 442351 : ts = t;
254 : : }
255 : 467107 : std::vector<Node> rargs;
256 : 467107 : rargs.push_back(ts);
257 : 467107 : MethodId idr = MethodId::RW_REWRITE;
258 [ + + ]: 467107 : if (args.size() >= 4)
259 : : {
260 [ + - ]: 2774 : if (getMethodId(args[3], idr))
261 : : {
262 : 2774 : rargs.push_back(args[3]);
263 : : }
264 : : }
265 : 467107 : Node tr = d_env.rewriteViaMethod(ts, idr);
266 [ + - ]: 934214 : Trace("smt-proof-pp-debug")
267 : 0 : << "...eq intro rewrite equality is " << ts << " == " << tr << ", from "
268 : 467107 : << idr << std::endl;
269 [ + + ]: 467107 : if (ts != tr)
270 : : {
271 : 286609 : Node eq = ts.eqNode(tr);
272 : : // apply REWRITE proof rule
273 [ - + ]: 286609 : if (!updateInternal(eq, ProofRule::MACRO_REWRITE, {}, rargs, cdp))
274 : : {
275 : : // if not elimianted, add as step
276 : 0 : cdp->addStep(eq, ProofRule::MACRO_REWRITE, {}, rargs);
277 : : }
278 : 286609 : tchildren.push_back(eq);
279 : 286609 : }
280 [ + + ]: 467107 : if (t == tr)
281 : : {
282 : : // typically not necessary, but done to be robust
283 : 352946 : cdp->addStep(t.eqNode(tr), ProofRule::REFL, {}, {t});
284 : 176473 : return t.eqNode(tr);
285 : : }
286 : : // must add TRANS if two step
287 : 290634 : return addProofForTrans(tchildren, cdp);
288 : 467107 : }
289 [ + + ]: 662535 : else if (id == ProofRule::MACRO_SR_PRED_INTRO)
290 : : {
291 : 42723 : std::vector<Node> tchildren;
292 : 42723 : std::vector<Node> sargs = args;
293 : 42723 : MethodId idr = MethodId::RW_REWRITE;
294 [ + + ]: 42723 : if (args.size() >= 4)
295 : : {
296 : 1723 : getMethodId(args[3], idr);
297 : : }
298 : : // take into account witness form, if necessary
299 : 42723 : WitnessReq reqw = d_wfpm.requiresWitnessFormIntro(args[0], idr);
300 [ + - ]: 42723 : Trace("smt-proof-pp-debug") << "...pred intro reqw=" << reqw << std::endl;
301 : : // (TRUE_ELIM
302 : : // (TRANS
303 : : // (MACRO_SR_EQ_INTRO <children> :args (t args[1:]))
304 : : // ... proof of apply_SR(t) = toWitness(apply_SR(t)) ...
305 : : // (MACRO_SR_EQ_INTRO {} {toWitness(apply_SR(t))})
306 : : // ))
307 : : // Notice this is an optimized, one sided version of the expansion of
308 : : // MACRO_SR_PRED_TRANSFORM below.
309 : : // We call the expandMacros method on MACRO_SR_EQ_INTRO, where notice
310 : : // that this rule application is immediately expanded in the recursive
311 : : // call and not added to the proof.
312 : : Node conc =
313 : 42723 : addExpandStep(ProofRule::MACRO_SR_EQ_INTRO, children, sargs, cdp);
314 [ + - ]: 85446 : Trace("smt-proof-pp-debug")
315 : 42723 : << "...pred intro conclusion is " << conc << std::endl;
316 [ - + ][ - + ]: 42723 : Assert(!conc.isNull());
[ - - ]
317 [ - + ][ - + ]: 42723 : Assert(conc.getKind() == Kind::EQUAL);
[ - - ]
318 [ - + ][ - + ]: 42723 : Assert(conc[0] == args[0]);
[ - - ]
319 : 42723 : addToTransChildren(conc, tchildren);
320 : 42723 : Node wc = conc[1];
321 [ + + ][ + + ]: 42723 : if (reqw == WitnessReq::WITNESS || reqw == WitnessReq::WITNESS_AND_REWRITE)
322 : : {
323 : 11778 : Node weq = addProofForWitnessForm(conc[1], cdp);
324 [ + - ]: 11778 : Trace("smt-proof-pp-debug") << "...weq is " << weq << std::endl;
325 : : // note this may be reflexive
326 : 11778 : addToTransChildren(weq, tchildren);
327 : 11778 : wc = weq[1];
328 : 11778 : }
329 [ + - ][ + + ]: 42723 : if (reqw == WitnessReq::REWRITE || reqw == WitnessReq::WITNESS_AND_REWRITE)
330 : : {
331 : : // toWitness(apply_SR(t)) = apply_SR(toWitness(apply_SR(t)))
332 : : // rewrite again, don't need substitution. Also we always use the
333 : : // default rewriter, due to the definition of MACRO_SR_PRED_INTRO.
334 : 35127 : Node weqr = addExpandStep(ProofRule::MACRO_SR_EQ_INTRO, {}, {wc}, cdp);
335 : 11709 : addToTransChildren(weqr, tchildren);
336 : 11709 : }
337 [ + + ]: 42723 : if (tchildren.empty())
338 : : {
339 : : // if trivial corner case, go back and add conc (which must be reflexive,
340 : : // since we already tried to add it via addToTransChildren).
341 : 80 : tchildren.push_back(conc);
342 : : }
343 : : // apply transitivity if necessary
344 : 42723 : Node eq = addProofForTrans(tchildren, cdp);
345 [ - + ][ - + ]: 42723 : Assert(!eq.isNull());
[ - - ]
346 [ - + ][ - + ]: 42723 : Assert(eq.getKind() == Kind::EQUAL);
[ - - ]
347 [ - + ][ - + ]: 42723 : Assert(eq[0] == args[0]);
[ - - ]
348 [ - + ][ - + ]: 42723 : Assert(eq[1] == d_true);
[ - - ]
349 : :
350 : 85446 : cdp->addStep(eq[0], ProofRule::TRUE_ELIM, {eq}, {});
351 : 42723 : return eq[0];
352 : 42723 : }
353 [ + + ]: 619812 : else if (id == ProofRule::MACRO_SR_PRED_ELIM)
354 : : {
355 : : // (EQ_RESOLVE
356 : : // children[0]
357 : : // (MACRO_SR_EQ_INTRO children[1:] :args children[0] ++ args))
358 : 11418 : std::vector<Node> schildren(children.begin() + 1, children.end());
359 : 11418 : std::vector<Node> srargs;
360 : 11418 : srargs.push_back(children[0]);
361 : 11418 : srargs.insert(srargs.end(), args.begin(), args.end());
362 : : Node conc =
363 : 11418 : addExpandStep(ProofRule::MACRO_SR_EQ_INTRO, schildren, srargs, cdp);
364 [ - + ][ - + ]: 11418 : Assert(!conc.isNull());
[ - - ]
365 [ - + ][ - + ]: 11418 : Assert(conc.getKind() == Kind::EQUAL);
[ - - ]
366 [ - + ][ - + ]: 11418 : Assert(conc[0] == children[0]);
[ - - ]
367 : : // apply equality resolve
368 [ + + ][ - - ]: 34254 : cdp->addStep(conc[1], ProofRule::EQ_RESOLVE, {children[0], conc}, {});
369 : 11418 : return conc[1];
370 : 11418 : }
371 [ + + ]: 608394 : else if (id == ProofRule::MACRO_SR_PRED_TRANSFORM)
372 : : {
373 : : // (EQ_RESOLVE
374 : : // children[0]
375 : : // (TRANS
376 : : // (MACRO_SR_EQ_INTRO children[1:] :args (children[0] args[1:]))
377 : : // ... proof of c = wc
378 : : // (MACRO_SR_EQ_INTRO {} wc)
379 : : // (SYMM
380 : : // (MACRO_SR_EQ_INTRO children[1:] :args <args>)
381 : : // ... proof of a = wa
382 : : // (MACRO_SR_EQ_INTRO {} wa))))
383 : : // where
384 : : // wa = toWitness(apply_SR(args[0])) and
385 : : // wc = toWitness(apply_SR(children[0])).
386 [ + - ]: 373198 : Trace("smt-proof-pp-debug")
387 : 186599 : << "Transform " << children[0] << " == " << args[0] << std::endl;
388 [ + + ]: 186599 : if (CDProof::isSame(children[0], args[0]))
389 : : {
390 [ + - ]: 3834 : Trace("smt-proof-pp-debug") << "...nothing to do" << std::endl;
391 : : // nothing to do
392 : 3834 : return children[0];
393 : : }
394 : 182765 : std::vector<Node> tchildren;
395 : 182765 : std::vector<Node> schildren(children.begin() + 1, children.end());
396 : 182765 : std::vector<Node> sargs = args;
397 : : // first, compute if we need
398 : 182765 : MethodId idr = MethodId::RW_REWRITE;
399 [ + + ]: 182765 : if (args.size() >= 4)
400 : : {
401 : 139 : getMethodId(args[3], idr);
402 : : }
403 : : WitnessReq reqw =
404 : 182765 : d_wfpm.requiresWitnessFormTransform(children[0], args[0], idr);
405 [ + - ]: 182765 : Trace("smt-proof-pp-debug") << "...reqw=" << reqw << std::endl;
406 : : // convert both sides, in three steps, take symmetry of second chain
407 [ + + ]: 548295 : for (unsigned r = 0; r < 2; r++)
408 : : {
409 : 365530 : std::vector<Node> tchildrenr;
410 : : // first rewrite children[0], then args[0]
411 [ + + ]: 365530 : sargs[0] = r == 0 ? children[0] : args[0];
412 : : // t = apply_SR(t)
413 : : Node eq =
414 : 365530 : expandMacros(ProofRule::MACRO_SR_EQ_INTRO, schildren, sargs, cdp);
415 [ + - ]: 731060 : Trace("smt-proof-pp-debug")
416 : 365530 : << "transform subs_rewrite (" << r << "): " << eq << std::endl;
417 : 365530 : Assert(!eq.isNull() && eq.getKind() == Kind::EQUAL && eq[0] == sargs[0]);
418 : 365530 : addToTransChildren(eq, tchildrenr);
419 : : // apply_SR(t) = toWitness(apply_SR(t))
420 : 365530 : Node wc = eq[1];
421 [ + + ]: 365530 : if (reqw == WitnessReq::WITNESS
422 [ + + ]: 359374 : || reqw == WitnessReq::WITNESS_AND_REWRITE)
423 : : {
424 : 14140 : Node weq = addProofForWitnessForm(eq[1], cdp);
425 [ + - ]: 28280 : Trace("smt-proof-pp-debug")
426 : 14140 : << "transform toWitness (" << r << "): " << weq << std::endl;
427 : : // note this may be reflexive
428 : 14140 : addToTransChildren(weq, tchildrenr);
429 : 14140 : wc = weq[1];
430 : 14140 : }
431 [ + + ]: 365530 : if (reqw == WitnessReq::REWRITE
432 [ + + ]: 365420 : || reqw == WitnessReq::WITNESS_AND_REWRITE)
433 : : {
434 : : // toWitness(apply_SR(t)) = apply_SR(toWitness(apply_SR(t)))
435 : : // rewrite again, don't need substitution. Also, we always use the
436 : : // default rewriter, due to the definition of MACRO_SR_PRED_TRANSFORM.
437 : 24282 : Node weqr = addExpandStep(ProofRule::MACRO_SR_EQ_INTRO, {}, {wc}, cdp);
438 [ + - ]: 16188 : Trace("smt-proof-pp-debug")
439 : 8094 : << "transform rewrite_witness (" << r << "): " << weqr << std::endl;
440 : 8094 : addToTransChildren(weqr, tchildrenr);
441 : 8094 : }
442 [ + - ]: 731060 : Trace("smt-proof-pp-debug")
443 : 365530 : << "transform connect (" << r << ")" << std::endl;
444 : : // add to overall chain
445 [ + + ]: 365530 : if (r == 0)
446 : : {
447 : : // add the current chain to the overall chain
448 : 182765 : tchildren.insert(tchildren.end(), tchildrenr.begin(), tchildrenr.end());
449 : : }
450 : : else
451 : : {
452 : : // add the current chain to cdp
453 : 182765 : Node eqr = addProofForTrans(tchildrenr, cdp);
454 [ + + ]: 182765 : if (!eqr.isNull())
455 : : {
456 [ + - ]: 257488 : Trace("smt-proof-pp-debug") << "transform connect sym " << tchildren
457 : 128744 : << " " << eqr << std::endl;
458 : : // take symmetry of above and add it to the overall chain
459 : 128744 : addToTransChildren(eqr, tchildren, true);
460 : : }
461 : 182765 : }
462 [ + - ]: 731060 : Trace("smt-proof-pp-debug")
463 : 365530 : << "transform finish (" << r << ")" << std::endl;
464 : 365530 : }
465 : : // apply transitivity if necessary
466 : 182765 : Node eq = addProofForTrans(tchildren, cdp);
467 [ + - ][ - + ]: 182765 : if (eq.isNull() || eq[1] != args[0])
[ + - ][ - + ]
[ - - ]
468 : : {
469 : 0 : DebugUnhandled() << "Failed proof for MACRO_SR_PRED_TRANSFORM";
470 : : Trace("smt-proof-pp-debug")
471 : : << "Failed transitivity from " << tchildren << std::endl;
472 : : return Node::null();
473 : : }
474 [ + + ][ - - ]: 548295 : cdp->addStep(eq[1], ProofRule::EQ_RESOLVE, {children[0], eq}, {});
475 : 182765 : return args[0];
476 : 182765 : }
477 [ + + ]: 421795 : else if (id == ProofRule::CHAIN_M_RESOLUTION)
478 : : {
479 : 40618 : ProofNodeManager* pnm = d_env.getProofNodeManager();
480 : : // first generate the naive chain_resolution
481 [ - + ][ - + ]: 40618 : Assert(args.size() == 3);
[ - - ]
482 : 40618 : std::vector<Node> pols(args[1].begin(), args[1].end());
483 : 40618 : std::vector<Node> lits(args[2].begin(), args[2].end());
484 [ - + ][ - + ]: 40618 : Assert(lits.size() == pols.size());
[ - - ]
485 [ - + ][ - + ]: 40618 : Assert(pols.size() == children.size() - 1);
[ - - ]
486 : 40618 : NodeManager* nm = nodeManager();
487 : 40618 : std::vector<Node> chainResArgs(args.begin() + 1, args.end());
488 : 40618 : Node chainConclusion = d_pc->checkDebug(
489 : 40618 : ProofRule::CHAIN_RESOLUTION, children, chainResArgs, Node::null(), "");
490 [ + - ]: 40618 : Trace("smt-proof-pp-debug") << "Original conclusion: " << args[0] << "\n";
491 [ + - ]: 81236 : Trace("smt-proof-pp-debug")
492 : 40618 : << "chainRes conclusion: " << chainConclusion << "\n";
493 [ + - ]: 81236 : Trace("crowding-lits")
494 : 40618 : << "Original conclusion and chainRes conclusion differ\n";
495 : : // There are n cases:
496 : : // - if the conclusion is the same, just replace
497 : : // - if they have the same literals but in different quantity, add a
498 : : // FACTORING step
499 : : // - if the order is not the same, add a REORDERING step
500 : : // - if there are literals in chainConclusion that are not in the original
501 : : // conclusion, we need to transform the CHAIN_M_RESOLUTION into a series
502 : : // of CHAIN_RESOLUTION + FACTORING steps, so that we explicitly eliminate
503 : : // all these "crowding" literals. We do this via FACTORING so we avoid
504 : : // adding an exponential number of premises, which would happen if we just
505 : : // repeated in the premises the clauses needed for eliminating crowding
506 : : // literals, which could themselves add crowding literals.
507 [ + + ]: 40618 : if (chainConclusion == args[0])
508 : : {
509 [ + - ]: 17183 : Trace("smt-proof-pp-debug") << "..same conclusion, DONE.\n";
510 [ + - ]: 17183 : Trace("crowding-lits") << "..same conclusion, DONE.\n";
511 : 17183 : cdp->addStep(
512 : : chainConclusion, ProofRule::CHAIN_RESOLUTION, children, chainResArgs);
513 : 17183 : return chainConclusion;
514 : : }
515 : 23435 : size_t initProofSize = cdp->getNumProofNodes();
516 : : // If we got here, then chainConclusion is NECESSARILY an OR node
517 [ - + ][ - + ]: 23435 : Assert(chainConclusion.getKind() == Kind::OR);
[ - - ]
518 : : // get the literals in the chain conclusion
519 : 23435 : std::vector<Node> chainConclusionLits{chainConclusion.begin(),
520 : 23435 : chainConclusion.end()};
521 : 23435 : std::set<Node> chainConclusionLitsSet{chainConclusion.begin(),
522 : 23435 : chainConclusion.end()};
523 [ + - ]: 46870 : Trace("smt-proof-pp-debug2")
524 : 23435 : << "..chainConclusionLits: " << chainConclusionLits << "\n";
525 [ + - ]: 46870 : Trace("smt-proof-pp-debug2")
526 : 23435 : << "..chainConclusionLitsSet: " << chainConclusionLitsSet << "\n";
527 : 23435 : std::vector<Node> conclusionLits;
528 : : // is args[0] a singleton clause? Yes if it's not an OR node. One might also
529 : : // think that it is a singleton if args[0] occurs in chainConclusionLitsSet.
530 : : // However it's not possible to know this only looking at the sets. For
531 : : // example with
532 : : //
533 : : // args[0] : (or b c)
534 : : // chairConclusionLitsSet : {b, c, (or b c)}
535 : : //
536 : : // we have that if args[0] occurs in the set but as a crowding literal, then
537 : : // args[0] is *not* a singleton clause. But if b and c were crowding
538 : : // literals, then args[0] would be a singleton clause. Since our intention
539 : : // is to determine who are the crowding literals exactly based on whether
540 : : // args[0] is a singleton or not, we must determine in another way whether
541 : : // args[0] is a singleton.
542 : : //
543 : : // Thus we rely on the standard utility to determine if args[0] is singleton
544 : : // based on the premises and arguments of the resolution
545 : 23435 : std::vector<Node> chainResArgsOrig;
546 : : // the proof utilities below expect to interleave literals and polarities
547 [ + + ]: 557757 : for (size_t i = 0, nsteps = args[1].getNumChildren(); i < nsteps; i++)
548 : : {
549 : 534322 : chainResArgsOrig.push_back(args[1][i]);
550 : 534322 : chainResArgsOrig.push_back(args[2][i]);
551 : : }
552 [ + + ]: 23435 : if (proof::isSingletonClause(args[0], children, chainResArgsOrig))
553 : : {
554 : 1058 : conclusionLits.push_back(args[0]);
555 : : }
556 : : else
557 : : {
558 [ - + ][ - + ]: 22377 : Assert(args[0].getKind() == Kind::OR);
[ - - ]
559 : 67131 : conclusionLits.insert(
560 : 89508 : conclusionLits.end(), args[0].begin(), args[0].end());
561 : : }
562 : 23435 : std::set<Node> conclusionLitsSet{conclusionLits.begin(),
563 : 23435 : conclusionLits.end()};
564 : : // If the sets are different, there are "crowding" literals, i.e. literals
565 : : // that were removed by implicit multi-usage of premises in the resolution
566 : : // chain.
567 [ + + ]: 23435 : if (chainConclusionLitsSet != conclusionLitsSet)
568 : : {
569 : 20549 : chainResArgsOrig.insert(chainResArgsOrig.begin(), args[0]);
570 [ + - ]: 20549 : Trace("smt-proof-pp-debug") << "..need to eliminate crowding lits.\n";
571 [ + - ]: 20549 : Trace("crowding-lits") << "..need to eliminate crowding lits.\n";
572 [ + - ]: 20549 : Trace("crowding-lits") << "..premises: " << children << "\n";
573 [ + - ]: 20549 : Trace("crowding-lits") << "..args: " << chainResArgsOrig << "\n";
574 : : chainConclusion =
575 : 20549 : proof::eliminateCrowdingLits(nm,
576 : 20549 : d_env.getOptions().proof.optResReconSize,
577 : : chainConclusionLits,
578 : : conclusionLits,
579 : : children,
580 : : chainResArgsOrig,
581 : : cdp,
582 : 20549 : pnm);
583 : : // update vector of lits. Note that the set is no longer used, so we don't
584 : : // need to update it
585 : : //
586 : : // We need again to check whether chainConclusion is a singleton
587 : : // clause. As above, it's a singleton if it's in the original
588 : : // chainConclusionLitsSet.
589 : 20549 : chainConclusionLits.clear();
590 [ - + ]: 20549 : if (chainConclusionLitsSet.count(chainConclusion))
591 : : {
592 : 0 : chainConclusionLits.push_back(chainConclusion);
593 : : }
594 : : else
595 : : {
596 [ - + ][ - + ]: 20549 : Assert(chainConclusion.getKind() == Kind::OR);
[ - - ]
597 : 20549 : chainConclusionLits.insert(chainConclusionLits.end(),
598 : : chainConclusion.begin(),
599 : : chainConclusion.end());
600 : : }
601 : : }
602 : : else
603 : : {
604 [ + - ]: 2886 : Trace("smt-proof-pp-debug") << "..add chainRes step directly.\n";
605 : 2886 : cdp->addStep(
606 : : chainConclusion, ProofRule::CHAIN_RESOLUTION, children, chainResArgs);
607 : : }
608 [ + - ]: 46870 : Trace("smt-proof-pp-debug")
609 : 23435 : << "Conclusion after chain_res/elimCrowd: " << chainConclusion << "\n";
610 [ + - ]: 46870 : Trace("smt-proof-pp-debug")
611 : 23435 : << "Conclusion lits: " << chainConclusionLits << "\n";
612 : : // Placeholder for running conclusion
613 : 23435 : Node n = chainConclusion;
614 : : // factoring
615 [ + + ]: 23435 : if (chainConclusionLits.size() != conclusionLits.size())
616 : : {
617 [ + - ]: 22554 : Trace("smt-proof-pp-debug") << "..add factoring step.\n";
618 : : // We build it rather than taking conclusionLits because the order may be
619 : : // different
620 : 22554 : std::vector<Node> factoredLits;
621 : 22554 : std::unordered_set<TNode> clauseSet;
622 [ + + ]: 766936 : for (size_t i = 0, size = chainConclusionLits.size(); i < size; ++i)
623 : : {
624 [ + + ]: 744382 : if (clauseSet.count(chainConclusionLits[i]))
625 : : {
626 : 326736 : continue;
627 : : }
628 : 417646 : factoredLits.push_back(n[i]);
629 : 417646 : clauseSet.insert(n[i]);
630 : : }
631 : 22554 : Node factored = factoredLits.empty() ? nm->mkConst(false)
632 : 22554 : : factoredLits.size() == 1
633 : 1058 : ? factoredLits[0]
634 [ - + ][ + + ]: 46166 : : nm->mkNode(Kind::OR, factoredLits);
635 : 45108 : cdp->addStep(factored, ProofRule::FACTORING, {n}, {});
636 : 22554 : n = factored;
637 : 22554 : }
638 : : // either same node or n as a clause
639 [ + + ][ + - ]: 23435 : Assert(n == args[0] || n.getKind() == Kind::OR);
[ - + ][ - + ]
[ - - ]
640 : : // reordering
641 [ + + ]: 23435 : if (n != args[0])
642 : : {
643 [ + - ]: 20264 : Trace("smt-proof-pp-debug") << "..add reordering step.\n";
644 : 60792 : cdp->addStep(args[0], ProofRule::REORDERING, {n}, {args[0]});
645 : : }
646 [ + - ]: 46870 : Trace("crowding-lits") << "Number of added proof nodes: "
647 : 23435 : << cdp->getNumProofNodes() - initProofSize << "\n";
648 : 23435 : return args[0];
649 : 40618 : }
650 [ + + ]: 381177 : else if (id == ProofRule::SUBS)
651 : : {
652 : 17361 : NodeManager* nm = nodeManager();
653 : : // Notice that a naive way to reconstruct SUBS is to do a term conversion
654 : : // proof for each substitution.
655 : : // The proof of f(a) * { a -> g(b) } * { b -> c } = f(g(c)) is:
656 : : // TRANS( CONG{f}( a=g(b) ), CONG{f}( CONG{g}( b=c ) ) )
657 : : // Notice that more optimal proofs are possible that do a single traversal
658 : : // over t. This is done by applying later substitutions to the range of
659 : : // previous substitutions, until a final simultaneous substitution is
660 : : // applied to t. For instance, in the above example, we first prove:
661 : : // CONG{g}( b = c )
662 : : // by applying the second substitution { b -> c } to the range of the first,
663 : : // giving us a proof of g(b)=g(c). We then construct the updated proof
664 : : // by tranitivity:
665 : : // TRANS( a=g(b), CONG{g}( b=c ) )
666 : : // We then apply the substitution { a -> g(c), b -> c } to f(a), to obtain:
667 : : // CONG{f}( TRANS( a=g(b), CONG{g}( b=c ) ) )
668 : : // which notice is more compact than the proof above.
669 : 17361 : Node t = args[0];
670 : : // get the kind of substitution
671 : 17361 : MethodId ids = MethodId::SB_DEFAULT;
672 [ + + ]: 17361 : if (args.size() >= 2)
673 : : {
674 : 9235 : getMethodId(args[1], ids);
675 : : }
676 : 17361 : MethodId ida = MethodId::SBA_SEQUENTIAL;
677 [ + + ]: 17361 : if (args.size() >= 3)
678 : : {
679 : 9061 : getMethodId(args[2], ida);
680 : : }
681 [ + - ]: 34722 : Trace("smt-proof-pp-debug")
682 : 17361 : << "Expand SUBS " << ids << " " << ida << std::endl;
683 : 17361 : std::vector<std::shared_ptr<CDProof>> pfs;
684 : 17361 : std::vector<TNode> vsList;
685 : 17361 : std::vector<TNode> ssList;
686 : 17361 : std::vector<TNode> fromList;
687 : 17361 : std::vector<ProofGenerator*> pgs;
688 : : // first, compute the entire substitution
689 [ + + ]: 35627 : for (size_t i = 0, nchild = children.size(); i < nchild; i++)
690 : : {
691 : : // get the substitution
692 : 18266 : builtin::BuiltinProofRuleChecker::getSubstitutionFor(
693 : 18266 : children[i], vsList, ssList, fromList, ids);
694 : : // ensure proofs for each formula in fromList
695 [ + + ][ + - ]: 18266 : if (children[i].getKind() == Kind::AND && ids == MethodId::SB_DEFAULT)
[ + + ]
696 : : {
697 [ + + ]: 1070521 : for (size_t j = 0, nchildi = children[i].getNumChildren(); j < nchildi;
698 : : j++)
699 : : {
700 : 1062945 : Node nodej = nm->mkConstInt(Rational(j));
701 : 5314725 : cdp->addStep(
702 : 2125890 : children[i][j], ProofRule::AND_ELIM, {children[i]}, {nodej});
703 : 1062945 : }
704 : : }
705 : : }
706 : 17361 : std::vector<Node> vvec;
707 : 17361 : std::vector<Node> svec;
708 [ + + ]: 1090996 : for (size_t i = 0, nvs = vsList.size(); i < nvs; i++)
709 : : {
710 : : // Note we process in forward order, since later substitution should be
711 : : // applied to earlier ones, and the last child of a SUBS is processed
712 : : // first.
713 : 1073635 : TNode var = vsList[i];
714 : 1073635 : TNode subs = ssList[i];
715 : 1073635 : TNode childFrom = fromList[i];
716 [ + - ]: 2147270 : Trace("smt-proof-pp-debug")
717 : 0 : << "...process " << var << " -> " << subs << " (" << childFrom << ", "
718 : 1073635 : << ids << ")" << std::endl;
719 : : // apply the current substitution to the range
720 [ + + ][ + + ]: 1073635 : if (!vvec.empty() && ida == MethodId::SBA_SEQUENTIAL)
[ + + ]
721 : : {
722 : : Node ss =
723 : 905 : subs.substitute(vvec.begin(), vvec.end(), svec.begin(), svec.end());
724 [ + + ]: 905 : if (ss != subs)
725 : : {
726 [ + - ]: 664 : Trace("smt-proof-pp-debug")
727 : 0 : << "......updated to " << var << " -> " << ss
728 : 332 : << " based on previous substitution" << std::endl;
729 : : // make the proof for the tranitivity step
730 : 332 : std::shared_ptr<CDProof> pf = std::make_shared<CDProof>(d_env);
731 : 332 : pfs.push_back(pf);
732 : : // prove the updated substitution
733 : : TConvProofGenerator tcg(d_env,
734 : : nullptr,
735 : : TConvPolicy::ONCE,
736 : : TConvCachePolicy::NEVER,
737 : : "nested_SUBS_TConvProofGenerator",
738 : : nullptr,
739 : 664 : true);
740 : : // add previous rewrite steps
741 [ + + ]: 2140 : for (unsigned j = 0, nvars = vvec.size(); j < nvars; j++)
742 : : {
743 : : // substitutions are pre-rewrites
744 : 1808 : tcg.addRewriteStep(vvec[j], svec[j], pgs[j], true);
745 : : }
746 : : // get the proof for the update to the current substitution
747 : 332 : Node seqss = subs.eqNode(ss);
748 : 332 : std::shared_ptr<ProofNode> pfn = tcg.getProofFor(seqss);
749 [ - + ][ - + ]: 332 : Assert(pfn != nullptr);
[ - - ]
750 : : // add the proof
751 : 332 : pf->addProof(pfn);
752 : : // get proof for childFrom from cdp
753 : 332 : pfn = cdp->getProofFor(childFrom);
754 : 332 : pf->addProof(pfn);
755 : : // ensure we have a proof of var = subs
756 : 664 : Node veqs = addProofForSubsStep(var, subs, childFrom, pf.get());
757 : : // transitivity
758 [ + + ][ - - ]: 996 : pf->addStep(var.eqNode(ss), ProofRule::TRANS, {veqs, seqss}, {});
759 : : // add to the substitution
760 : 332 : vvec.push_back(var);
761 : 332 : svec.push_back(ss);
762 [ + - ]: 332 : pgs.push_back(pf.get());
763 : 332 : continue;
764 : 332 : }
765 [ + + ]: 905 : }
766 : : // Just use equality from CDProof, but ensure we have a proof in cdp.
767 : : // This may involve a TRUE_INTRO/FALSE_INTRO if the substitution step
768 : : // uses the assumption childFrom as a Boolean assignment (e.g.
769 : : // childFrom = true if we are using MethodId::SB_LITERAL).
770 : 1073303 : addProofForSubsStep(var, subs, childFrom, cdp);
771 : 1073303 : vvec.push_back(var);
772 : 1073303 : svec.push_back(subs);
773 [ + - ]: 1073303 : pgs.push_back(cdp);
774 [ + + ][ + + ]: 1074299 : }
[ + + ]
775 : : // should be implied by the substitution now
776 : 17361 : TConvPolicy tcpolicy = ida == MethodId::SBA_FIXPOINT ? TConvPolicy::FIXPOINT
777 : : : TConvPolicy::ONCE;
778 : : TConvProofGenerator tcpg(d_env,
779 : : nullptr,
780 : : tcpolicy,
781 : : TConvCachePolicy::NEVER,
782 : : "SUBS_TConvProofGenerator",
783 : : nullptr,
784 : 34722 : true);
785 [ + + ]: 1090996 : for (unsigned j = 0, nvars = vvec.size(); j < nvars; j++)
786 : : {
787 : : // substitutions are pre-rewrites
788 : 1073635 : tcpg.addRewriteStep(vvec[j], svec[j], pgs[j], true);
789 [ + + ]: 1073635 : if (ida == MethodId::SBA_FIXPOINT)
790 : : {
791 : : // fixed point substitutions are also post-rewrites
792 : 1064394 : tcpg.addRewriteStep(vvec[j], svec[j], pgs[j], false);
793 : : }
794 : : }
795 : : // add the proof constructed by the term conversion utility
796 : 17361 : std::shared_ptr<ProofNode> pfn = tcpg.getProofForRewriting(t);
797 : 17361 : Node eq = pfn->getResult();
798 : : Node ts = builtin::BuiltinProofRuleChecker::applySubstitution(
799 : 17361 : t, children, ids, ida);
800 : 17361 : Node eqq = t.eqNode(ts);
801 : : // should have the same conclusion, if not, then tcpg does not agree with
802 : : // the substitution.
803 [ - + ]: 17361 : if (eq != eqq)
804 : : {
805 : : // this can happen in very rare cases where e.g. x -> a; f(x) -> b
806 : : // and t*{x -> a} = t*{x -> a}*{f(x) -> b} != t*{x -> a, f(x) -> b}
807 [ - - ][ - - ]: 0 : if (ida == MethodId::SBA_SEQUENTIAL && vsList.size() > 1)
[ - - ]
808 : : {
809 [ - - ]: 0 : Trace("smt-proof-pp-debug")
810 : 0 : << "resort to sequential reconstruction" << std::endl;
811 : : // just do the naive sequential reconstruction,
812 : : // (SUBS F1 ... Fn t) ---> (TRANS (SUBS F1 t) ... (SUBS Fn tn))
813 : 0 : Node curr = t;
814 : 0 : std::vector<Node> transChildren;
815 [ - - ]: 0 : for (size_t i = 0, nvs = vsList.size(); i < nvs; i++)
816 : : {
817 : 0 : size_t ii = nvs - 1 - i;
818 : 0 : TNode var = vsList[ii];
819 : 0 : TNode subs = ssList[ii];
820 : 0 : Node next = curr.substitute(var, subs);
821 [ - - ]: 0 : if (next != curr)
822 : : {
823 : 0 : Node eqo = curr.eqNode(next);
824 : 0 : transChildren.push_back(eqo);
825 : : // ensure the proof for the substitution exists
826 : 0 : addProofForSubsStep(var, subs, fromList[ii], cdp);
827 : : // do the single step SUBS on curr with the default arguments
828 : 0 : cdp->addStep(eqo, ProofRule::SUBS, {var.eqNode(subs)}, {curr});
829 : 0 : curr = next;
830 : 0 : }
831 : 0 : }
832 : 0 : Assert(curr == ts);
833 : 0 : cdp->addStep(eqq, ProofRule::TRANS, transChildren, {});
834 : 0 : }
835 : : else
836 : : {
837 [ - - ]: 0 : Trace("smt-proof-pp-debug")
838 : 0 : << "resort to TRUST_SUBS" << std::endl
839 : 0 : << eq << std::endl
840 : 0 : << eqq << std::endl
841 : 0 : << "from " << children << " applied to " << t << std::endl;
842 : 0 : cdp->addTrustedStep(eqq, TrustId::SUBS_NO_ELABORATE, children, {});
843 : : }
844 : : }
845 : : else
846 : : {
847 : 17361 : cdp->addProof(pfn);
848 : : }
849 : 17361 : return eqq;
850 : 17361 : }
851 [ + + ]: 363816 : else if (id == ProofRule::MACRO_REWRITE)
852 : : {
853 : : // get the kind of rewrite
854 : 316698 : MethodId idr = MethodId::RW_REWRITE;
855 : 316698 : TheoryId theoryId = d_env.theoryOf(args[0]);
856 [ + + ]: 316698 : if (args.size() >= 2)
857 : : {
858 : 4584 : getMethodId(args[1], idr);
859 : : }
860 : 316698 : Rewriter* rr = d_env.getRewriter();
861 : 316698 : Node ret = d_env.rewriteViaMethod(args[0], idr);
862 : 316698 : Node eq = args[0].eqNode(ret);
863 [ + + ][ + + ]: 316698 : if (idr == MethodId::RW_REWRITE || idr == MethodId::RW_REWRITE_EQ_EXT)
864 : : {
865 : : // rewrites from theory::Rewriter
866 : 314786 : bool isExtEq = (idr == MethodId::RW_REWRITE_EQ_EXT);
867 : : // use rewrite with proof interface
868 : 314786 : TrustNode trn = rr->rewriteWithProof(args[0], isExtEq);
869 : 314786 : std::shared_ptr<ProofNode> pfn = trn.toProofNode();
870 [ + + ]: 314786 : if (pfn == nullptr)
871 : : {
872 [ + - ]: 1712 : Trace("smt-proof-pp-debug")
873 : 856 : << "Use TRUST_REWRITE for " << eq << std::endl;
874 : : // did not have a proof of rewriting, probably isExtEq is true
875 [ + - ]: 856 : if (isExtEq)
876 : : {
877 : : // update to TRUST_THEORY_REWRITE with idr
878 [ - + ][ - + ]: 856 : Assert(args.size() >= 1);
[ - - ]
879 : : Node tid = builtin::BuiltinProofRuleChecker::mkTheoryIdNode(
880 : 856 : nodeManager(), theoryId);
881 [ + + ][ - - ]: 4280 : cdp->addStep(
882 : 856 : eq, ProofRule::TRUST_THEORY_REWRITE, {}, {eq, tid, args[1]});
883 : 856 : }
884 : : else
885 : : {
886 : : // this should never be applied
887 : 0 : cdp->addTrustedStep(eq, TrustId::REWRITE_NO_ELABORATE, {}, {});
888 : : }
889 : : }
890 : : else
891 : : {
892 : 313930 : cdp->addProof(pfn);
893 : : }
894 : 629572 : Assert(trn.getNode() == ret)
895 [ - + ][ - - ]: 314786 : << "Unexpected rewrite " << args[0] << std::endl
896 : 314786 : << "Got: " << trn.getNode() << std::endl
897 : 0 : << "Expected: " << ret;
898 : 314786 : }
899 [ - + ]: 1912 : else if (idr == MethodId::RW_EVALUATE)
900 : : {
901 : : // change to evaluate, which is never eliminated
902 : 0 : cdp->addStep(eq, ProofRule::EVALUATE, {}, {args[0]});
903 : : }
904 : : else
905 : : {
906 : 1912 : Node retCurr = args[0];
907 : 1912 : std::vector<Node> transEq;
908 : : // try to reconstruct the (extended) rewrite
909 : : // first, use the standard rewriter followed by the extended equality
910 : : // rewriter
911 [ + + ]: 2254 : for (size_t i = 0; i < 2; i++)
912 : : {
913 [ + + ][ + + ]: 2190 : if (i == 1 && retCurr.getKind() != Kind::EQUAL)
[ + + ]
914 : : {
915 : 1848 : break;
916 : : }
917 : 2150 : MethodId midi =
918 [ + + ]: 2150 : i == 0 ? MethodId::RW_REWRITE : MethodId::RW_REWRITE_EQ_EXT;
919 : 2150 : Node retDef = d_env.rewriteViaMethod(retCurr, midi);
920 [ + + ]: 2150 : if (retDef != retCurr)
921 : : {
922 : : // will expand this as a default rewrite if needed
923 : 2006 : Node eqd = retCurr.eqNode(retDef);
924 : 2006 : Node mid = mkMethodId(nodeManager(), midi);
925 [ + + ][ - - ]: 6018 : cdp->addStep(eqd, ProofRule::MACRO_REWRITE, {}, {retCurr, mid});
926 : 2006 : transEq.push_back(eqd);
927 : 2006 : }
928 : 2150 : retCurr = retDef;
929 [ + + ]: 2150 : if (retCurr == ret)
930 : : {
931 : : // already successful
932 : 1808 : break;
933 : : }
934 [ + + ]: 2150 : }
935 [ + + ]: 1912 : if (retCurr != ret)
936 : : {
937 : : // We were unable to show it via ordinary rewriting, so we insert
938 : : // a trusted step. This cannot be TRUST_THEORY_REWRITE since it is
939 : : // not an ordinary theory rewrite.
940 : 104 : Node eqp = retCurr.eqNode(ret);
941 : 104 : cdp->addTrustedStep(eqp, TrustId::EXT_THEORY_REWRITE, {}, {});
942 : 104 : transEq.push_back(eqp);
943 : 104 : }
944 [ + + ]: 1912 : if (transEq.size() > 1)
945 : : {
946 : : // put together with transitivity
947 : 194 : cdp->addStep(eq, ProofRule::TRANS, transEq, {});
948 : : }
949 : 1912 : }
950 [ - + ]: 316698 : if (args[0] == ret)
951 : : {
952 : : // should not be necessary typically
953 : 0 : cdp->addStep(eq, ProofRule::REFL, {}, {args[0]});
954 : : }
955 : 316698 : return eq;
956 : 316698 : }
957 [ + + ]: 47118 : else if (id == ProofRule::MACRO_ARITH_SCALE_SUM_UB)
958 : : {
959 : : Node sumBounds =
960 : 30672 : theory::arith::expandMacroSumUb(nodeManager(), children, args, cdp);
961 [ - + ][ - + ]: 30672 : Assert(!sumBounds.isNull());
[ - - ]
962 [ + - ][ + - ]: 30672 : Assert(res.isNull() || sumBounds == res);
[ - + ][ - + ]
[ - - ]
963 : 30672 : return sumBounds;
964 : 30672 : }
965 [ + + ]: 16446 : else if (id == ProofRule::MACRO_STRING_INFERENCE)
966 : : {
967 : : // get the arguments
968 : 9151 : Node conc;
969 : : InferenceId iid;
970 : : bool isRev;
971 : 9151 : std::vector<Node> exp;
972 [ + - ]: 9151 : if (theory::strings::InferProofCons::unpackArgs(
973 : : args, conc, iid, isRev, exp))
974 : : {
975 [ + - ]: 9151 : if (theory::strings::InferProofCons::convert(
976 : : d_env, iid, isRev, conc, exp, cdp))
977 : : {
978 : 9151 : return conc;
979 : : }
980 : : }
981 [ - + ][ - + ]: 18302 : }
982 [ + - ]: 7295 : else if (id == ProofRule::MACRO_BV_BITBLAST)
983 : : {
984 : 7295 : bv::BBProof bb(d_env, nullptr, true);
985 : 7295 : Node eq = args[0];
986 [ - + ][ - + ]: 7295 : Assert(eq.getKind() == Kind::EQUAL);
[ - - ]
987 : 7295 : bb.bbAtom(eq[0]);
988 : 14590 : Node bbAtom = bb.getStoredBBAtom(eq[0]);
989 : 7295 : bb.getProofGenerator()->addProofTo(eq[0].eqNode(bbAtom), cdp);
990 : 7295 : return eq;
991 : 7295 : }
992 : 0 : return Node::null();
993 : : }
994 : :
995 : 73944 : Node ProofPostprocessCallback::addExpandStep(ProofRule id,
996 : : const std::vector<Node>& children,
997 : : const std::vector<Node>& args,
998 : : CDProof* cdp)
999 : : {
1000 : : // For now, this is a (locally) recursive call to expand macros; alternatively
1001 : : // we could add the step to cdp and allow the proof node updater to call us
1002 : : // again. This has the advantage that it may be possible to do more aggressive
1003 : : // merging, e.g. if a subproof in expanded call was duplicated in multiple
1004 : : // expansions, at the cost of generating more intermediate proof nodes. At
1005 : : // the moment, this is not worthwhile.
1006 : 73944 : return expandMacros(id, children, args, cdp);
1007 : : }
1008 : :
1009 : 25918 : Node ProofPostprocessCallback::addProofForWitnessForm(Node t, CDProof* cdp)
1010 : : {
1011 : 25918 : Node tw = SkolemManager::getOriginalForm(t);
1012 : 25918 : Node eq = t.eqNode(tw);
1013 [ + + ]: 25918 : if (t == tw)
1014 : : {
1015 : : // not necessary, add REFL step
1016 : 2560 : cdp->addStep(eq, ProofRule::REFL, {}, {t});
1017 : 1280 : return eq;
1018 : : }
1019 : 24638 : std::shared_ptr<ProofNode> pn = d_wfpm.getProofFor(eq);
1020 [ + - ]: 24638 : if (pn != nullptr)
1021 : : {
1022 : : // add the proof
1023 : 24638 : cdp->addProof(pn);
1024 : : }
1025 : : else
1026 : : {
1027 : 0 : DebugUnhandled() << "ProofPostprocessCallback::addProofForWitnessForm: failed "
1028 : 0 : "to add proof for witness form of "
1029 : : << t;
1030 : : }
1031 : 24638 : return eq;
1032 : 25918 : }
1033 : :
1034 : 698887 : Node ProofPostprocessCallback::addProofForTrans(
1035 : : const std::vector<Node>& tchildren, CDProof* cdp)
1036 : : {
1037 : 698887 : size_t tsize = tchildren.size();
1038 [ + + ]: 698887 : if (tsize > 1)
1039 : : {
1040 : 48870 : Node lhs = tchildren[0][0];
1041 : 48870 : Node rhs = tchildren[tsize - 1][1];
1042 : 48870 : Node eq = lhs.eqNode(rhs);
1043 : 48870 : cdp->addStep(eq, ProofRule::TRANS, tchildren, {});
1044 : 48870 : return eq;
1045 : 48870 : }
1046 [ + + ]: 650017 : else if (tsize == 1)
1047 : : {
1048 : 595996 : return tchildren[0];
1049 : : }
1050 : 54021 : return Node::null();
1051 : : }
1052 : :
1053 : 1073635 : Node ProofPostprocessCallback::addProofForSubsStep(Node var,
1054 : : Node subs,
1055 : : Node assump,
1056 : : CDProof* cdp)
1057 : : {
1058 : : // ensure we have a proof of var = subs
1059 : 1073635 : Node veqs = var.eqNode(subs);
1060 [ + + ]: 1073635 : if (veqs != assump)
1061 : : {
1062 : : // should be true intro or false intro
1063 [ - + ][ - + ]: 174 : Assert(subs.isConst());
[ - - ]
1064 : 522 : cdp->addStep(
1065 : : veqs,
1066 [ + - ]: 174 : subs.getConst<bool>() ? ProofRule::TRUE_INTRO : ProofRule::FALSE_INTRO,
1067 : : {assump},
1068 : : {});
1069 : : }
1070 : 1073635 : return veqs;
1071 : 0 : }
1072 : :
1073 : 582718 : bool ProofPostprocessCallback::addToTransChildren(Node eq,
1074 : : std::vector<Node>& tchildren,
1075 : : bool isSymm)
1076 : : {
1077 [ - + ][ - + ]: 582718 : Assert(!eq.isNull());
[ - - ]
1078 [ - + ][ - + ]: 582718 : Assert(eq.getKind() == Kind::EQUAL);
[ - - ]
1079 [ + + ]: 582718 : if (eq[0] == eq[1])
1080 : : {
1081 : 177762 : return false;
1082 : : }
1083 : 533691 : Node equ = isSymm ? eq[1].eqNode(eq[0]) : eq;
1084 : 404956 : Assert(tchildren.empty()
1085 : : || (tchildren[tchildren.size() - 1].getKind() == Kind::EQUAL
1086 : : && tchildren[tchildren.size() - 1][1] == equ[0]));
1087 : 404956 : tchildren.push_back(equ);
1088 : 404956 : return true;
1089 : 404956 : }
1090 : :
1091 : 18896 : ProofPostprocess::ProofPostprocess(Env& env,
1092 : : rewriter::RewriteDb* rdb,
1093 : 18896 : bool updateScopedAssumptions)
1094 : : : EnvObj(env),
1095 : 18896 : d_cb(env, updateScopedAssumptions),
1096 : 18896 : d_elimTrustedRules(false),
1097 : : // the update merges subproofs if proofPpMerge is true
1098 : 18896 : d_updater(env, d_cb, options().proof.proofPpMerge)
1099 : : {
1100 [ + + ]: 18896 : if (rdb != nullptr)
1101 : : {
1102 : 6655 : d_ppdsl.reset(new ProofPostprocessDsl(env, rdb));
1103 : : }
1104 : 18896 : }
1105 : :
1106 : 37764 : ProofPostprocess::~ProofPostprocess() {}
1107 : :
1108 : 13591 : void ProofPostprocess::process(std::shared_ptr<ProofNode> pf,
1109 : : ProofGenerator* pppg)
1110 : : {
1111 : : // Initialize the callback, which computes necessary static information about
1112 : : // how to process, including how to process assumptions in pf.
1113 : 13591 : d_cb.initializeUpdate(pppg);
1114 : : // now, process
1115 : 13591 : d_updater.process(pf);
1116 : :
1117 : : // eliminate subtypes if option is specified
1118 [ + - ]: 13591 : if (options().proof.proofElimSubtypes)
1119 : : {
1120 : 13591 : SubtypeElimConverterCallback secc(d_env);
1121 : 13591 : ProofNodeConverter subtypeConvert(d_env, secc);
1122 : 13591 : std::shared_ptr<ProofNode> pfc = subtypeConvert.process(pf);
1123 [ - + ][ - + ]: 13591 : AlwaysAssert(pfc != nullptr);
[ - - ]
1124 : : // now update
1125 : 13591 : d_env.getProofNodeManager()->updateNode(pf.get(), pfc.get());
1126 : 13591 : }
1127 [ + + ][ + - ]: 13591 : if (d_elimTrustedRules && d_ppdsl != nullptr)
[ + + ]
1128 : : {
1129 : : // go back and find the (possibly new) trusted steps
1130 : 5618 : std::vector<std::shared_ptr<ProofNode>> tproofs;
1131 : : std::unordered_set<ProofRule> trustRules{ProofRule::TRUST,
1132 : 5618 : ProofRule::TRUST_THEORY_REWRITE};
1133 : 5618 : expr::getSubproofRules(pf, trustRules, tproofs);
1134 : 5618 : d_ppdsl->reconstruct(tproofs);
1135 : 5618 : }
1136 : 13591 : }
1137 : :
1138 : 103525 : void ProofPostprocess::setEliminateRule(ProofRule rule)
1139 : : {
1140 : 103525 : d_cb.setEliminateRule(rule);
1141 : 103525 : }
1142 : :
1143 : 6655 : void ProofPostprocess::setEliminateAllTrustedRules()
1144 : : {
1145 : 6655 : d_elimTrustedRules = true;
1146 : 6655 : }
1147 : :
1148 : 10173 : void ProofPostprocess::setAssertions(const std::vector<Node>& assertions,
1149 : : bool doDebug)
1150 : : {
1151 : 10173 : d_updater.setFreeAssumptions(assertions, doDebug);
1152 : 10173 : }
1153 : :
1154 : : } // namespace smt
1155 : : } // namespace cvc5::internal
|
