Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Andrew Reynolds, Abdalrhman Mohamed, Aina Niemetz
4 : : *
5 : : * This file is part of the cvc5 project.
6 : : *
7 : : * Copyright (c) 2009-2024 by the authors listed in the file AUTHORS
8 : : * in the top-level source directory and their institutional affiliations.
9 : : * All rights reserved. See the file COPYING in the top-level source
10 : : * directory for licensing information.
11 : : * ****************************************************************************
12 : : *
13 : : * Implementation of the Lfsc post processor
14 : : */
15 : :
16 : : #include "proof/lfsc/lfsc_post_processor.h"
17 : :
18 : : #include "options/proof_options.h"
19 : : #include "proof/lazy_proof.h"
20 : : #include "proof/lfsc/lfsc_printer.h"
21 : : #include "proof/proof_checker.h"
22 : : #include "proof/proof_node_algorithm.h"
23 : : #include "proof/proof_node_manager.h"
24 : : #include "proof/proof_node_updater.h"
25 : : #include "rewriter/rewrites.h"
26 : : #include "smt/env.h"
27 : : #include "theory/strings/theory_strings_utils.h"
28 : :
29 : : using namespace cvc5::internal::kind;
30 : :
31 : : namespace cvc5::internal {
32 : : namespace proof {
33 : :
34 : 1417 : LfscProofPostprocessCallback::LfscProofPostprocessCallback(
35 : 1417 : Env& env, LfscNodeConverter& ltp)
36 : : : EnvObj(env),
37 : 1417 : d_pc(env.getProofNodeManager()->getChecker()),
38 : : d_tproc(ltp),
39 : 2834 : d_numIgnoredScopes(0)
40 : : {
41 : 1417 : }
42 : :
43 : 1417 : void LfscProofPostprocessCallback::initializeUpdate() { d_numIgnoredScopes = 0; }
44 : :
45 : 3229340 : bool LfscProofPostprocessCallback::shouldUpdate(std::shared_ptr<ProofNode> pn,
46 : : const std::vector<Node>& fa,
47 : : bool& continueUpdate)
48 : : {
49 : 3229340 : return pn->getRule() != ProofRule::LFSC_RULE;
50 : : }
51 : :
52 : 1927630 : bool LfscProofPostprocessCallback::update(Node res,
53 : : ProofRule id,
54 : : const std::vector<Node>& children,
55 : : const std::vector<Node>& args,
56 : : CDProof* cdp,
57 : : bool& continueUpdate)
58 : : {
59 [ + - ]: 3855260 : Trace("lfsc-pp") << "LfscProofPostprocessCallback::update: " << id
60 : 1927630 : << std::endl;
61 [ + - ]: 1927630 : Trace("lfsc-pp-debug") << "...proves " << res << std::endl;
62 : 1927630 : NodeManager* nm = nodeManager();
63 [ - + ][ - + ]: 1927630 : Assert(id != ProofRule::LFSC_RULE);
[ - - ]
64 : :
65 [ + + ][ + + ]: 1927630 : switch (id)
[ + + ][ + + ]
[ + + ][ + + ]
[ + ]
66 : : {
67 : 117567 : case ProofRule::ASSUME:
68 : : {
69 [ + + ]: 117567 : if (d_defs.find(res) != d_defs.cend())
70 : : {
71 : 230 : addLfscRule(cdp, res, children, LfscRule::DEFINITION, args);
72 : 230 : return true;
73 : : }
74 : 117337 : return false;
75 : : }
76 : : break;
77 : 37302 : case ProofRule::SCOPE:
78 : : {
79 : : // On the first two calls to update, the proof node is the outermost
80 : : // scopes of the proof. These scopes should not be printed in the LFSC
81 : : // proof. Instead, the LFSC proof printer will print the proper scopes
82 : : // around the proof, which e.g. involves an LFSC "check" command.
83 [ + + ]: 37302 : if (d_numIgnoredScopes < 2)
84 : : {
85 : : // The arguments of the outer scope are definitions.
86 [ + + ]: 2834 : if (d_numIgnoredScopes == 0)
87 : : {
88 [ + + ]: 1909 : for (const Node& arg : args)
89 : : {
90 : 492 : d_defs.insert(arg);
91 : : // Notes:
92 : : // - Some declarations only appear inside definitions and don't show
93 : : // up in assertions. To ensure that those declarations are printed,
94 : : // we need to process the definitions.
95 : : // - We process the definitions here before the rest of the proof to
96 : : // keep the indices of bound variables consistant between different
97 : : // queries that share the same definitions (e.g., incremental mode).
98 : : // Otherwise, bound variables will be assigned indices according to
99 : : // the order in which they appear in the proof.
100 : 492 : d_tproc.convert(arg);
101 : : }
102 : : }
103 : 2834 : d_numIgnoredScopes++;
104 : : // Note that we do not want to modify the top-most SCOPEs.
105 : 2834 : return false;
106 : : }
107 [ - + ][ - + ]: 34468 : Assert(children.size() == 1);
[ - - ]
108 : : // (SCOPE P :args (F1 ... Fn))
109 : : // becomes
110 : : // (scope _ _ (\ X1 ... (scope _ _ (\ Xn P)) ... ))
111 : 68936 : Node curr = children[0];
112 [ + + ]: 213085 : for (size_t i = 0, nargs = args.size(); i < nargs; i++)
113 : : {
114 : 178617 : size_t ii = (nargs - 1) - i;
115 : : // Use a dummy conclusion for what LAMBDA proves, since there is no
116 : : // FOL representation for its type.
117 : 357234 : Node fconc = mkDummyPredicate(nm);
118 : 535851 : addLfscRule(cdp, fconc, {curr}, LfscRule::LAMBDA, {args[ii]});
119 : : // we use a chained implication (=> F1 ... (=> Fn C)) which avoids
120 : : // aliasing.
121 : 535851 : Node next = nm->mkNode(Kind::OR, args[ii].notNode(), curr);
122 : 535851 : addLfscRule(cdp, next, {fconc}, LfscRule::SCOPE, {args[ii]});
123 : 178617 : curr = next;
124 : : }
125 : : // In LFSC, we have now proved:
126 : : // (or (not F1) (or (not F2) ... (or (not Fn) C) ... ))
127 : : // We now must convert this to one of two cases
128 [ + + ]: 34468 : if (res.getKind() == Kind::NOT)
129 : : {
130 : : // we have C = false,
131 : : // convert to (not (and F1 (and F2 ... (and Fn true) ... )))
132 : : // this also handles the case where the conclusion is simply F1,
133 : : // when n=1.
134 : 13796 : addLfscRule(cdp, res, {curr}, LfscRule::NOT_AND_REV, {});
135 : : }
136 : : else
137 : : {
138 : : // we have that C != false
139 : : // convert to (=> (and F1 (and F2 ... (and Fn true) ... )) C)
140 : 82710 : addLfscRule(cdp, res, {curr}, LfscRule::PROCESS_SCOPE, {children[0]});
141 : : }
142 : : }
143 : 34468 : break;
144 : 85236 : case ProofRule::CHAIN_RESOLUTION:
145 : : {
146 : : // turn into binary resolution
147 : 170472 : Node cur = children[0];
148 [ + + ]: 454464 : for (size_t i = 1, size = children.size(); i < size; i++)
149 : : {
150 : 1846140 : std::vector<Node> newChildren{cur, children[i]};
151 : 1476910 : std::vector<Node> newArgs{args[0][i - 1], args[1][i - 1]};
152 : 369228 : cur = d_pc->checkDebug(ProofRule::RESOLUTION, newChildren, newArgs);
153 : 369228 : cdp->addStep(cur, ProofRule::RESOLUTION, newChildren, newArgs);
154 : : }
155 : : }
156 : 85236 : break;
157 : 101260 : case ProofRule::SYMM:
158 : : {
159 [ + + ]: 101260 : if (res.getKind() != Kind::NOT)
160 : : {
161 : : // no need to convert (positive) equality symmetry
162 : 100996 : return false;
163 : : }
164 : : // must use alternate SYMM rule for disequality
165 : 528 : addLfscRule(cdp, res, {children[0]}, LfscRule::NEG_SYMM, {});
166 : : }
167 : 264 : break;
168 : 211222 : case ProofRule::TRANS:
169 : : {
170 [ + + ]: 211222 : if (children.size() <= 2)
171 : : {
172 : : // no need to change
173 : 189175 : return false;
174 : : }
175 : : // turn into binary
176 : 44094 : Node cur = children[0];
177 : 44094 : std::unordered_set<Node> processed;
178 : 22047 : processed.insert(children.begin(), children.end());
179 [ + + ]: 92863 : for (size_t i = 1, size = children.size(); i < size; i++)
180 : : {
181 : 283264 : std::vector<Node> newChildren{cur, children[i]};
182 : 70816 : cur = d_pc->checkDebug(ProofRule::TRANS, newChildren, {});
183 [ + + ]: 70816 : if (processed.find(cur) != processed.end())
184 : : {
185 : 1432 : continue;
186 : : }
187 : 69384 : processed.insert(cur);
188 : 69384 : cdp->addStep(cur, ProofRule::TRANS, newChildren, {});
189 : : }
190 : : }
191 : 22047 : break;
192 : 223207 : case ProofRule::CONG:
193 : : case ProofRule::NARY_CONG:
194 : : {
195 [ - + ][ - + ]: 223207 : Assert(res.getKind() == Kind::EQUAL);
[ - - ]
196 [ - + ][ - + ]: 223207 : Assert(res[0].getOperator() == res[1].getOperator());
[ - - ]
197 [ + - ]: 446414 : Trace("lfsc-pp-cong") << "Processing congruence for " << res << " "
198 [ - + ][ - - ]: 223207 : << res[0].getKind() << std::endl;
199 : : // different for closures
200 [ + + ]: 223207 : if (res[0].isClosure())
201 : : {
202 [ - + ]: 2326 : if (res[0][0] != res[1][0])
203 : : {
204 : : // cannot convert congruence with different variables currently
205 : 0 : return false;
206 : : }
207 : 4652 : Node cop = d_tproc.getOperatorOfClosure(res[0]);
208 : 4652 : Node pcop = d_tproc.getOperatorOfClosure(res[0], false, true);
209 [ + - ]: 2326 : Trace("lfsc-pp-qcong") << "Operator for closure " << cop << std::endl;
210 : : // start with base case body = body'
211 : 4652 : Node curL = children[0][0];
212 : 4652 : Node curR = children[0][1];
213 : 2326 : Node currEq = children[0];
214 [ + - ]: 2326 : Trace("lfsc-pp-qcong") << "Base congruence " << currEq << std::endl;
215 [ + + ]: 7552 : for (size_t i = 0, nvars = res[0][0].getNumChildren(); i < nvars; i++)
216 : : {
217 : 5226 : size_t ii = (nvars - 1) - i;
218 [ + - ]: 5226 : Trace("lfsc-pp-qcong") << "Process child " << i << std::endl;
219 : : // CONG rules for each variable
220 : 15678 : Node v = res[0][0][ii];
221 : : // Use partial version for each argument except the last one. This
222 : : // avoids type errors in internal representation of LFSC terms.
223 [ + + ]: 15678 : Node vop = d_tproc.getOperatorOfBoundVar(ii == 0 ? cop : pcop, v);
224 : 10452 : Node vopEq = vop.eqNode(vop);
225 : 10452 : cdp->addStep(vopEq, ProofRule::REFL, {}, {vop});
226 : 10452 : Node nextEq;
227 [ + + ]: 5226 : if (i + 1 == nvars)
228 : : {
229 : : // if we are at the end, we prove the final equality
230 : 2326 : nextEq = res;
231 : : }
232 : : else
233 : : {
234 : 2900 : curL = nm->mkNode(Kind::HO_APPLY, vop, curL);
235 : 2900 : curR = nm->mkNode(Kind::HO_APPLY, vop, curR);
236 : 2900 : nextEq = curL.eqNode(curR);
237 : : }
238 [ + + ][ - - ]: 15678 : addLfscRule(cdp, nextEq, {vopEq, currEq}, LfscRule::CONG, {});
239 : 5226 : currEq = nextEq;
240 : : }
241 : 2326 : return true;
242 : : }
243 : 220881 : Kind k = res[0].getKind();
244 [ - + ]: 220881 : if (k == Kind::HO_APPLY)
245 : : {
246 : : // HO_APPLY congruence is a single application of LFSC congruence
247 : 0 : addLfscRule(cdp, res, children, LfscRule::CONG, {});
248 : 0 : return true;
249 : : }
250 : : // We are proving f(t1, ..., tn) = f(s1, ..., sn), nested.
251 : : // First, get the operator, which will be used for printing the base
252 : : // REFL step. Notice this may be for interpreted or uninterpreted
253 : : // function symbols.
254 : 441762 : Node op = d_tproc.getOperatorOfTerm(res[0]);
255 [ + - ]: 441762 : Trace("lfsc-pp-cong") << "Processing cong for op " << op << " "
256 [ - + ][ - - ]: 220881 : << op.getType() << std::endl;
257 [ - + ][ - + ]: 220881 : Assert(!op.isNull());
[ - - ]
258 : : // initial base step is REFL
259 : 441762 : Node opEq = op.eqNode(op);
260 : 441762 : cdp->addStep(opEq, ProofRule::REFL, {}, {op});
261 : 220881 : size_t nchildren = children.size();
262 : 662643 : Node nullTerm = d_tproc.getNullTerminator(k, res[0].getType());
263 : : // Are we doing congruence of an n-ary operator? If so, notice that op
264 : : // is a binary operator and we must apply congruence in a special way.
265 : : // Note we use the first block of code if we have more than 2 children,
266 : : // or if we have a null terminator.
267 : : // special case: constructors and apply uf are not treated as n-ary; these
268 : : // symbols have function types that expect n arguments.
269 [ + + ]: 345567 : bool isNary = NodeManager::isNAryKind(k) && k != Kind::APPLY_CONSTRUCTOR
270 [ + + ][ + + ]: 345567 : && k != Kind::APPLY_UF;
271 [ + + ][ + + ]: 220881 : if (isNary && (nchildren > 2 || !nullTerm.isNull()))
[ + + ][ + + ]
272 : : {
273 : : // get the null terminator for the kind, which may mean we are doing
274 : : // a special kind of congruence for n-ary kinds whose base is a REFL
275 : : // step for the null terminator.
276 : 120364 : Node currEq;
277 [ + - ]: 60182 : if (!nullTerm.isNull())
278 : : {
279 : 60182 : currEq = nullTerm.eqNode(nullTerm);
280 : : // if we have a null terminator, we do a final REFL step to add
281 : : // the null terminator to both sides.
282 : 120364 : cdp->addStep(currEq, ProofRule::REFL, {}, {nullTerm});
283 : : }
284 : : else
285 : : {
286 : : // Otherwise, start with the last argument.
287 : 0 : currEq = children[nchildren - 1];
288 : : }
289 [ + + ]: 321044 : for (size_t i = 0; i < nchildren; i++)
290 : : {
291 : 260862 : size_t ii = (nchildren - 1) - i;
292 [ + - ]: 260862 : Trace("lfsc-pp-cong") << "Process child " << ii << std::endl;
293 : 521724 : Node uop = op;
294 : : // special case: applications of the following kinds in the chain may
295 : : // have a different type, so remake the operator here.
296 [ + + ][ + + ]: 260862 : if (k == Kind::BITVECTOR_CONCAT || k == Kind::ADD || k == Kind::MULT
[ + + ]
297 [ + + ]: 203046 : || k == Kind::NONLINEAR_MULT)
298 : : {
299 : : // we get the operator of the next argument concatenated with the
300 : : // current accumulated remainder.
301 : 116006 : Node currApp = nm->mkNode(k, children[ii][0], currEq[0]);
302 : 58003 : uop = d_tproc.getOperatorOfTerm(currApp);
303 : : }
304 [ + - ][ - - ]: 521724 : Trace("lfsc-pp-cong") << "Apply " << uop << " to " << children[ii][0]
305 [ - + ][ - + ]: 260862 : << " and " << children[ii][1] << std::endl;
[ - - ]
306 : : Node argAppEq =
307 : 521724 : nm->mkNode(Kind::HO_APPLY, uop, children[ii][0])
308 : 782586 : .eqNode(nm->mkNode(Kind::HO_APPLY, uop, children[ii][1]));
309 [ + + ][ - - ]: 782586 : addLfscRule(cdp, argAppEq, {opEq, children[ii]}, LfscRule::CONG, {});
310 : : // now, congruence to the current equality
311 : 521724 : Node nextEq;
312 [ + + ]: 260862 : if (ii == 0)
313 : : {
314 : : // use final conclusion
315 : 60182 : nextEq = res;
316 : : }
317 : : else
318 : : {
319 : : // otherwise continue to apply
320 : : nextEq =
321 : 401360 : nm->mkNode(Kind::HO_APPLY, argAppEq[0], currEq[0])
322 : 200680 : .eqNode(nm->mkNode(Kind::HO_APPLY, argAppEq[1], currEq[1]));
323 : : }
324 [ + + ][ - - ]: 782586 : addLfscRule(cdp, nextEq, {argAppEq, currEq}, LfscRule::CONG, {});
325 : 260862 : currEq = nextEq;
326 : : }
327 : : }
328 : : else
329 : : {
330 : : // non n-ary kinds do not have null terminators
331 [ - + ][ - + ]: 160699 : Assert(nullTerm.isNull());
[ - - ]
332 : 160699 : updateCong(res, children, cdp, op);
333 : : }
334 : : }
335 : 220881 : break;
336 : 284 : case ProofRule::HO_CONG:
337 : : {
338 : : // converted to chain of CONG, with no base operator
339 : 284 : updateCong(res, children, cdp, Node::null());
340 : : }
341 : 284 : break;
342 : 24472 : case ProofRule::AND_INTRO:
343 : : {
344 : 48944 : Node cur = d_tproc.getNullTerminator(Kind::AND);
345 : 24472 : size_t nchildren = children.size();
346 [ + + ]: 103227 : for (size_t j = 0; j < nchildren; j++)
347 : : {
348 : 78755 : size_t jj = (nchildren - 1) - j;
349 : : // conclude the final conclusion if we are finished
350 : 211793 : Node next = jj == 0 ? res : nm->mkNode(Kind::AND, children[jj], cur);
351 [ + + ]: 78755 : if (j == 0)
352 : : {
353 : 48944 : addLfscRule(cdp, next, {children[jj]}, LfscRule::AND_INTRO1, {});
354 : : }
355 : : else
356 : : {
357 [ + + ][ - - ]: 162849 : addLfscRule(cdp, next, {children[jj], cur}, LfscRule::AND_INTRO2, {});
358 : : }
359 : 78755 : cur = next;
360 : : }
361 : : }
362 : 24472 : break;
363 : 4008 : case ProofRule::ARITH_SUM_UB:
364 : : {
365 : : // proof of null terminator base 0 = 0
366 : 12024 : Node zero = d_tproc.getNullTerminator(Kind::ADD, res[0].getType());
367 : 8016 : Node cur = zero.eqNode(zero);
368 : 8016 : cdp->addStep(cur, ProofRule::REFL, {}, {zero});
369 [ + + ]: 24726 : for (size_t i = 0, size = children.size(); i < size; i++)
370 : : {
371 : 20718 : size_t ii = (children.size() - 1) - i;
372 : 103590 : std::vector<Node> newChildren{children[ii], cur};
373 [ + + ]: 20718 : if (ii == 0)
374 : : {
375 : : // final rule must be the real conclusion
376 : 4008 : addLfscRule(cdp, res, newChildren, LfscRule::ARITH_SUM_UB, {});
377 : : }
378 : : else
379 : : {
380 : : // rules build an n-ary chain of + on both sides
381 : 16710 : cur = d_pc->checkDebug(ProofRule::ARITH_SUM_UB, newChildren, {});
382 : 16710 : addLfscRule(cdp, cur, newChildren, LfscRule::ARITH_SUM_UB, {});
383 : : }
384 : : }
385 : : }
386 : 4008 : break;
387 : 17 : case ProofRule::CONCAT_CONFLICT:
388 : : {
389 [ + - ]: 17 : if (children.size() == 1)
390 : : {
391 : : // no need to change
392 : 17 : return false;
393 : : }
394 : 0 : Assert(children.size() == 2);
395 : 0 : Assert(children[0].getKind() == Kind::EQUAL);
396 : 0 : Assert(children[0][0].getType().isSequence());
397 : : // must use the sequences version of the rule
398 : 0 : Node falsen = nm->mkConst(false);
399 : 0 : addLfscRule(cdp, falsen, children, LfscRule::CONCAT_CONFLICT_DEQ, args);
400 : : }
401 : 0 : break;
402 : 1092 : case ProofRule::INSTANTIATE:
403 : : {
404 : 2184 : Node q = children[0];
405 [ - + ][ - + ]: 1092 : Assert(q.getKind() == Kind::FORALL);
[ - - ]
406 : 2184 : std::vector<Node> terms;
407 : 3276 : std::vector<Node> qvars(q[0].begin(), q[0].end());
408 : 2184 : Node conc = q;
409 [ + + ]: 4172 : for (size_t i = 0, nvars = q[0].getNumChildren(); i < nvars; i++)
410 : : {
411 [ - + ][ - + ]: 3080 : Assert(conc.getKind() == Kind::FORALL);
[ - - ]
412 : 3080 : Node prevConc = conc;
413 [ + + ]: 3080 : if (i + 1 == nvars)
414 : : {
415 : 1092 : conc = res;
416 : : }
417 : : else
418 : : {
419 [ - + ][ - + ]: 1988 : Assert(i + 1 < qvars.size());
[ - - ]
420 : 3976 : std::vector<Node> qvarsNew(qvars.begin() + i + 1, qvars.end());
421 [ - + ][ - + ]: 1988 : Assert(!qvarsNew.empty());
[ - - ]
422 [ - + ][ - + ]: 1988 : Assert(qvars[i].getType() == args[0][i].getType());
[ - - ]
423 : 3976 : std::vector<Node> qchildren;
424 : 3976 : TNode v = qvars[i];
425 : 1988 : TNode subs = args[0][i];
426 : 1988 : qchildren.push_back(nm->mkNode(Kind::BOUND_VAR_LIST, qvarsNew));
427 : 1988 : qchildren.push_back(conc[1].substitute(v, subs));
428 : 1988 : conc = nm->mkNode(Kind::FORALL, qchildren);
429 : : }
430 : 9240 : addLfscRule(cdp, conc, {prevConc}, LfscRule::INSTANTIATE, {args[0][i]});
431 : : }
432 : : }
433 : 1092 : break;
434 : 126 : case ProofRule::THEORY_REWRITE:
435 : : {
436 [ - + ][ - + ]: 126 : Assert(args.size() >= 2);
[ - - ]
437 : : ProofRewriteRule idr;
438 [ - + ]: 126 : if (!rewriter::getRewriteRule(args[0], idr))
439 : : {
440 : 126 : return false;
441 : : }
442 [ - + ]: 126 : if (idr == ProofRewriteRule::BETA_REDUCE)
443 : : {
444 : : // get the term to beta-reduce
445 : 0 : Node termToReduce = nm->mkNode(Kind::APPLY_UF, args[1][0]);
446 : 0 : addLfscRule(cdp, res, {}, LfscRule::BETA_REDUCE, {termToReduce});
447 : : }
448 : : else
449 : : {
450 : 126 : return false;
451 : : }
452 : : }
453 : 0 : break;
454 : 1121840 : default: return false; break;
455 : : }
456 [ - + ][ - + ]: 392752 : AlwaysAssert(cdp->getProofFor(res)->getRule() != ProofRule::ASSUME);
[ - - ]
457 : 392752 : return true;
458 : : }
459 : :
460 : 160983 : void LfscProofPostprocessCallback::updateCong(Node res,
461 : : const std::vector<Node>& children,
462 : : CDProof* cdp,
463 : : Node startOp)
464 : : {
465 : 321966 : Node currEq;
466 : 160983 : size_t i = 0;
467 : 160983 : size_t nchildren = children.size();
468 [ + + ]: 160983 : if (!startOp.isNull())
469 : : {
470 : : // start with reflexive equality on operator
471 : 160699 : currEq = startOp.eqNode(startOp);
472 : : }
473 : : else
474 : : {
475 : : // first child specifies (higher-order) operator equality
476 : 284 : currEq = children[0];
477 : 284 : i++;
478 : : }
479 : 321966 : Node curL = currEq[0];
480 : 321966 : Node curR = currEq[1];
481 : 160983 : NodeManager* nm = nodeManager();
482 [ + + ]: 447588 : for (; i < nchildren; i++)
483 : : {
484 : : // CONG rules for each child
485 : 573210 : Node nextEq;
486 [ + + ]: 286605 : if (i + 1 == nchildren)
487 : : {
488 : : // if we are at the end, we prove the final equality
489 : 160983 : nextEq = res;
490 : : }
491 : : else
492 : : {
493 : 125622 : curL = nm->mkNode(Kind::HO_APPLY, curL, children[i][0]);
494 : 125622 : curR = nm->mkNode(Kind::HO_APPLY, curR, children[i][1]);
495 : 125622 : nextEq = curL.eqNode(curR);
496 : : }
497 [ + + ][ - - ]: 859815 : addLfscRule(cdp, nextEq, {currEq, children[i]}, LfscRule::CONG, {});
498 : 286605 : currEq = nextEq;
499 : : }
500 : 160983 : }
501 : :
502 : 1308300 : void LfscProofPostprocessCallback::addLfscRule(
503 : : CDProof* cdp,
504 : : Node conc,
505 : : const std::vector<Node>& children,
506 : : LfscRule lr,
507 : : const std::vector<Node>& args)
508 : : {
509 : 1308300 : std::vector<Node> largs;
510 : 1308300 : largs.push_back(mkLfscRuleNode(nodeManager(), lr));
511 : 1308300 : largs.push_back(conc);
512 : 1308300 : largs.insert(largs.end(), args.begin(), args.end());
513 : 1308300 : cdp->addStep(conc, ProofRule::LFSC_RULE, children, largs);
514 : 1308300 : }
515 : :
516 : 0 : Node LfscProofPostprocessCallback::mkChain(Kind k,
517 : : const std::vector<Node>& children)
518 : : {
519 : 0 : Assert(!children.empty());
520 : 0 : NodeManager* nm = nodeManager();
521 : 0 : size_t nchildren = children.size();
522 : 0 : size_t i = 0;
523 : : // do we have a null terminator? If so, we start with it.
524 : 0 : Node ret = d_tproc.getNullTerminator(k, children[0].getType());
525 [ - - ]: 0 : if (ret.isNull())
526 : : {
527 : 0 : ret = children[nchildren - 1];
528 : 0 : i = 1;
529 : : }
530 [ - - ]: 0 : while (i < nchildren)
531 : : {
532 : 0 : ret = nm->mkNode(k, children[(nchildren - 1) - i], ret);
533 : 0 : i++;
534 : : }
535 : 0 : return ret;
536 : : }
537 : :
538 : 178617 : Node LfscProofPostprocessCallback::mkDummyPredicate(NodeManager* nm)
539 : : {
540 : 357234 : return nm->mkBoundVar(nm->booleanType());
541 : : }
542 : :
543 : 1417 : LfscProofPostprocess::LfscProofPostprocess(Env& env, LfscNodeConverter& ltp)
544 : 1417 : : EnvObj(env), d_cb(new proof::LfscProofPostprocessCallback(env, ltp))
545 : : {
546 : 1417 : }
547 : :
548 : 1417 : void LfscProofPostprocess::process(std::shared_ptr<ProofNode> pf)
549 : : {
550 : 1417 : d_cb->initializeUpdate();
551 : : // do not automatically add symmetry steps, since this leads to
552 : : // non-termination for example on policy_variable.smt2
553 : 1417 : ProofNodeUpdater updater(d_env, *(d_cb.get()), false, false);
554 : 1417 : updater.process(pf);
555 : 1417 : }
556 : :
557 : : } // namespace proof
558 : : } // namespace cvc5::internal
|
