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