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