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 : 1750 : LfscProofPostprocessCallback::LfscProofPostprocessCallback(
32 : 1750 : Env& env, LfscNodeConverter& ltp)
33 : : : EnvObj(env),
34 : 1750 : d_pc(env.getProofNodeManager()->getChecker()),
35 : 1750 : d_tproc(ltp),
36 : 3500 : d_numIgnoredScopes(0)
37 : : {
38 : 1750 : }
39 : :
40 : 1750 : void LfscProofPostprocessCallback::initializeUpdate()
41 : : {
42 : 1750 : d_numIgnoredScopes = 0;
43 : 1750 : }
44 : :
45 : 3853378 : bool LfscProofPostprocessCallback::shouldUpdate(
46 : : std::shared_ptr<ProofNode> pn,
47 : : CVC5_UNUSED const std::vector<Node>& fa,
48 : : CVC5_UNUSED bool& continueUpdate)
49 : : {
50 : 3853378 : return pn->getRule() != ProofRule::LFSC_RULE;
51 : : }
52 : :
53 : 2314943 : 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 [ + - ]: 4629886 : Trace("lfsc-pp") << "LfscProofPostprocessCallback::update: " << id
61 : 2314943 : << std::endl;
62 [ + - ]: 2314943 : Trace("lfsc-pp-debug") << "...proves " << res << std::endl;
63 : 2314943 : NodeManager* nm = nodeManager();
64 [ - + ][ - + ]: 2314943 : Assert(id != ProofRule::LFSC_RULE);
[ - - ]
65 : :
66 [ + + ][ + + ]: 2314943 : switch (id)
[ + + ][ + + ]
[ + + ][ + + ]
67 : : {
68 : 145582 : case ProofRule::ASSUME:
69 : : {
70 [ + + ]: 145582 : if (d_defs.find(res) != d_defs.cend())
71 : : {
72 : 302 : addLfscRule(cdp, res, children, LfscRule::DEFINITION, args);
73 : 302 : return true;
74 : : }
75 : 145280 : return false;
76 : : }
77 : : break;
78 : 46670 : 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 [ + + ]: 46670 : if (d_numIgnoredScopes < 2)
85 : : {
86 : : // The arguments of the outer scope are definitions.
87 [ + + ]: 3500 : if (d_numIgnoredScopes == 0)
88 : : {
89 [ + + ]: 2309 : 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 : 3500 : d_numIgnoredScopes++;
105 : : // Note that we do not want to modify the top-most SCOPEs.
106 : 3500 : return false;
107 : : }
108 [ - + ][ - + ]: 43170 : Assert(children.size() == 1);
[ - - ]
109 : : // (SCOPE P :args (F1 ... Fn))
110 : : // becomes
111 : : // (scope _ _ (\ X1 ... (scope _ _ (\ Xn P)) ... ))
112 : 43170 : Node curr = children[0];
113 [ + + ]: 255523 : for (size_t i = 0, nargs = args.size(); i < nargs; i++)
114 : : {
115 : 212353 : 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 : 212353 : Node fconc = mkDummyPredicate(nm);
119 : 637059 : addLfscRule(cdp, fconc, {curr}, LfscRule::LAMBDA, {args[ii]});
120 : : // we use a chained implication (=> F1 ... (=> Fn C)) which avoids
121 : : // aliasing.
122 : 424706 : Node next = nm->mkNode(Kind::OR, args[ii].notNode(), curr);
123 : 637059 : addLfscRule(cdp, next, {fconc}, LfscRule::SCOPE, {args[ii]});
124 : 212353 : curr = next;
125 : 212353 : }
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 [ + + ]: 43170 : 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 : 18672 : 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 : 101502 : addLfscRule(cdp, res, {curr}, LfscRule::PROCESS_SCOPE, {children[0]});
142 : : }
143 : 43170 : }
144 : 43170 : break;
145 : 103147 : case ProofRule::CHAIN_RESOLUTION:
146 : : {
147 : : // turn into binary resolution
148 : 103147 : Node cur = children[0];
149 [ + + ]: 580620 : for (size_t i = 1, size = children.size(); i < size; i++)
150 : : {
151 : 1909892 : std::vector<Node> newChildren{cur, children[i]};
152 : 1909892 : std::vector<Node> newArgs{args[0][i - 1], args[1][i - 1]};
153 : 477473 : cur = d_pc->checkDebug(ProofRule::RESOLUTION, newChildren, newArgs);
154 : 477473 : cdp->addStep(cur, ProofRule::RESOLUTION, newChildren, newArgs);
155 : 477473 : }
156 : 103147 : }
157 : 103147 : break;
158 : 57538 : case ProofRule::SYMM:
159 : : {
160 [ + + ]: 57538 : if (res.getKind() != Kind::NOT)
161 : : {
162 : : // no need to convert (positive) equality symmetry
163 : 57154 : return false;
164 : : }
165 : : // must use alternate SYMM rule for disequality
166 : 768 : addLfscRule(cdp, res, {children[0]}, LfscRule::NEG_SYMM, {});
167 : : }
168 : 384 : break;
169 : 242817 : case ProofRule::TRANS:
170 : : {
171 [ + + ]: 242817 : if (children.size() <= 2)
172 : : {
173 : : // no need to change
174 : 219946 : return false;
175 : : }
176 : : // turn into binary
177 : 22871 : Node cur = children[0];
178 : 22871 : std::unordered_set<Node> processed;
179 : 22871 : processed.insert(children.begin(), children.end());
180 [ + + ]: 97511 : for (size_t i = 1, size = children.size(); i < size; i++)
181 : : {
182 : 298560 : std::vector<Node> newChildren{cur, children[i]};
183 : 74640 : cur = d_pc->checkDebug(ProofRule::TRANS, newChildren, {});
184 [ + + ]: 74640 : if (processed.find(cur) != processed.end())
185 : : {
186 : 13 : continue;
187 : : }
188 : 74627 : processed.insert(cur);
189 : 74627 : cdp->addStep(cur, ProofRule::TRANS, newChildren, {});
190 [ + + ]: 74640 : }
191 : 22871 : }
192 : 22871 : break;
193 : 263305 : case ProofRule::CONG:
194 : : case ProofRule::NARY_CONG:
195 : : {
196 [ - + ][ - + ]: 263305 : Assert(res.getKind() == Kind::EQUAL);
[ - - ]
197 [ - + ][ - + ]: 263305 : Assert(res[0].getOperator() == res[1].getOperator());
[ - - ]
198 [ + - ]: 526610 : Trace("lfsc-pp-cong") << "Processing congruence for " << res << " "
199 [ - + ][ - - ]: 263305 : << res[0].getKind() << std::endl;
200 : : // different for closures
201 [ + + ]: 263305 : if (res[0].isClosure())
202 : : {
203 [ - + ]: 4214 : if (res[0][0] != res[1][0])
204 : : {
205 : : // cannot convert congruence with different variables currently
206 : 0 : return false;
207 : : }
208 : 4214 : Node cop = d_tproc.getOperatorOfClosure(res[0]);
209 : 4214 : Node pcop = d_tproc.getOperatorOfClosure(res[0], false, true);
210 [ + - ]: 4214 : Trace("lfsc-pp-qcong") << "Operator for closure " << cop << std::endl;
211 : : // start with base case body = body'
212 : 4214 : Node curL = children[0][0];
213 : 4214 : Node curR = children[0][1];
214 : 4214 : Node currEq = children[0];
215 [ + - ]: 4214 : Trace("lfsc-pp-qcong") << "Base congruence " << currEq << std::endl;
216 [ + + ]: 12804 : for (size_t i = 0, nvars = res[0][0].getNumChildren(); i < nvars; i++)
217 : : {
218 : 8590 : size_t ii = (nvars - 1) - i;
219 [ + - ]: 8590 : Trace("lfsc-pp-qcong") << "Process child " << i << std::endl;
220 : : // CONG rules for each variable
221 : 17180 : 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 [ + + ]: 17180 : Node vop = d_tproc.getOperatorOfBoundVar(ii == 0 ? cop : pcop, v);
225 : 8590 : Node vopEq = vop.eqNode(vop);
226 : 17180 : cdp->addStep(vopEq, ProofRule::REFL, {}, {vop});
227 : 8590 : Node nextEq;
228 [ + + ]: 8590 : if (i + 1 == nvars)
229 : : {
230 : : // if we are at the end, we prove the final equality
231 : 4214 : nextEq = res;
232 : : }
233 : : else
234 : : {
235 : 4376 : curL = nm->mkNode(Kind::HO_APPLY, vop, curL);
236 : 4376 : curR = nm->mkNode(Kind::HO_APPLY, vop, curR);
237 : 4376 : nextEq = curL.eqNode(curR);
238 : : }
239 [ + + ][ - - ]: 25770 : addLfscRule(cdp, nextEq, {vopEq, currEq}, LfscRule::CONG, {});
240 : 8590 : currEq = nextEq;
241 : 8590 : }
242 : 4214 : return true;
243 : 4214 : }
244 : 259091 : Kind k = res[0].getKind();
245 [ - + ]: 259091 : 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 : 259091 : Node op = d_tproc.getOperatorOfTerm(res[0]);
256 [ + - ]: 518182 : Trace("lfsc-pp-cong") << "Processing cong for op " << op << " "
257 [ - + ][ - - ]: 259091 : << op.getType() << std::endl;
258 [ - + ][ - + ]: 259091 : Assert(!op.isNull());
[ - - ]
259 : : // initial base step is REFL
260 : 259091 : Node opEq = op.eqNode(op);
261 : 518182 : cdp->addStep(opEq, ProofRule::REFL, {}, {op});
262 : 259091 : size_t nchildren = children.size();
263 : 518182 : 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 [ + + ]: 406902 : bool isNary = NodeManager::isNAryKind(k) && k != Kind::APPLY_CONSTRUCTOR
271 [ + + ][ + + ]: 406902 : && k != Kind::APPLY_UF;
272 [ + + ][ + + ]: 259091 : 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 : 80701 : Node currEq;
278 [ + - ]: 80701 : if (!nullTerm.isNull())
279 : : {
280 : 80701 : 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 : 161402 : 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 [ + + ]: 389938 : for (size_t i = 0; i < nchildren; i++)
291 : : {
292 : 309237 : size_t ii = (nchildren - 1) - i;
293 [ + - ]: 309237 : Trace("lfsc-pp-cong") << "Process child " << ii << std::endl;
294 : 309237 : 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 [ + + ][ + + ]: 309237 : if (k == Kind::BITVECTOR_CONCAT || k == Kind::ADD || k == Kind::MULT
[ + + ]
298 [ + + ]: 238542 : || k == Kind::NONLINEAR_MULT)
299 : : {
300 : : // we get the operator of the next argument concatenated with the
301 : : // current accumulated remainder.
302 : 142596 : Node currApp = nm->mkNode(k, children[ii][0], currEq[0]);
303 : 71298 : uop = d_tproc.getOperatorOfTerm(currApp);
304 : 71298 : }
305 [ + - ][ - - ]: 618474 : Trace("lfsc-pp-cong") << "Apply " << uop << " to " << children[ii][0]
306 [ - + ][ - + ]: 309237 : << " and " << children[ii][1] << std::endl;
[ - - ]
307 : : Node argAppEq =
308 : 618474 : nm->mkNode(Kind::HO_APPLY, uop, children[ii][0])
309 : 618474 : .eqNode(nm->mkNode(Kind::HO_APPLY, uop, children[ii][1]));
310 [ + + ][ - - ]: 927711 : addLfscRule(cdp, argAppEq, {opEq, children[ii]}, LfscRule::CONG, {});
311 : : // now, congruence to the current equality
312 : 309237 : Node nextEq;
313 [ + + ]: 309237 : if (ii == 0)
314 : : {
315 : : // use final conclusion
316 : 80701 : nextEq = res;
317 : : }
318 : : else
319 : : {
320 : : // otherwise continue to apply
321 : : nextEq =
322 : 457072 : nm->mkNode(Kind::HO_APPLY, argAppEq[0], currEq[0])
323 : 228536 : .eqNode(nm->mkNode(Kind::HO_APPLY, argAppEq[1], currEq[1]));
324 : : }
325 [ + + ][ - - ]: 927711 : addLfscRule(cdp, nextEq, {argAppEq, currEq}, LfscRule::CONG, {});
326 : 309237 : currEq = nextEq;
327 : 309237 : }
328 : 80701 : }
329 : : else
330 : : {
331 : : // non n-ary kinds do not have null terminators
332 [ - + ][ - + ]: 178390 : Assert(nullTerm.isNull());
[ - - ]
333 : 178390 : updateCong(res, children, cdp, op);
334 : : }
335 : 259091 : }
336 : 259091 : 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 : 31716 : case ProofRule::AND_INTRO:
344 : : {
345 : 31716 : Node cur = d_tproc.getNullTerminator(nm, Kind::AND);
346 : 31716 : size_t nchildren = children.size();
347 [ + + ]: 132270 : for (size_t j = 0; j < nchildren; j++)
348 : : {
349 : 100554 : size_t jj = (nchildren - 1) - j;
350 : : // conclude the final conclusion if we are finished
351 : 169392 : Node next = jj == 0 ? res : nm->mkNode(Kind::AND, children[jj], cur);
352 [ + + ]: 100554 : if (j == 0)
353 : : {
354 : 63432 : addLfscRule(cdp, next, {children[jj]}, LfscRule::AND_INTRO1, {});
355 : : }
356 : : else
357 : : {
358 [ + + ][ - - ]: 206514 : addLfscRule(cdp, next, {children[jj], cur}, LfscRule::AND_INTRO2, {});
359 : : }
360 : 100554 : cur = next;
361 : 100554 : }
362 : 31716 : }
363 : 31716 : break;
364 : 5311 : case ProofRule::ARITH_SUM_UB:
365 : : {
366 : : // proof of null terminator base 0 = 0
367 : 10622 : Node zero = d_tproc.getNullTerminator(nm, Kind::ADD, res[0].getType());
368 : 5311 : Node cur = zero.eqNode(zero);
369 : 10622 : cdp->addStep(cur, ProofRule::REFL, {}, {zero});
370 [ + + ]: 33059 : for (size_t i = 0, size = children.size(); i < size; i++)
371 : : {
372 : 27748 : size_t ii = (children.size() - 1) - i;
373 : 110992 : std::vector<Node> newChildren{children[ii], cur};
374 [ + + ]: 27748 : if (ii == 0)
375 : : {
376 : : // final rule must be the real conclusion
377 : 5311 : addLfscRule(cdp, res, newChildren, LfscRule::ARITH_SUM_UB, {});
378 : : }
379 : : else
380 : : {
381 : : // rules build an n-ary chain of + on both sides
382 : 22437 : cur = d_pc->checkDebug(ProofRule::ARITH_SUM_UB, newChildren, {});
383 : 22437 : addLfscRule(cdp, cur, newChildren, LfscRule::ARITH_SUM_UB, {});
384 : : }
385 : 27748 : }
386 : 5311 : }
387 : 5311 : break;
388 : 1401 : case ProofRule::INSTANTIATE:
389 : : {
390 : 1401 : Node q = children[0];
391 [ - + ][ - + ]: 1401 : Assert(q.getKind() == Kind::FORALL);
[ - - ]
392 : 1401 : std::vector<Node> terms;
393 : 2802 : std::vector<Node> qvars(q[0].begin(), q[0].end());
394 : 1401 : Node conc = q;
395 [ + + ]: 5021 : for (size_t i = 0, nvars = q[0].getNumChildren(); i < nvars; i++)
396 : : {
397 [ - + ][ - + ]: 3620 : Assert(conc.getKind() == Kind::FORALL);
[ - - ]
398 : 3620 : Node prevConc = conc;
399 [ + + ]: 3620 : if (i + 1 == nvars)
400 : : {
401 : 1401 : conc = res;
402 : : }
403 : : else
404 : : {
405 [ - + ][ - + ]: 2219 : Assert(i + 1 < qvars.size());
[ - - ]
406 : 2219 : std::vector<Node> qvarsNew(qvars.begin() + i + 1, qvars.end());
407 [ - + ][ - + ]: 2219 : Assert(!qvarsNew.empty());
[ - - ]
408 [ - + ][ - + ]: 8876 : AssertEqual(qvars[i].getType(), args[0][i].getType());
[ - - ]
409 : 2219 : std::vector<Node> qchildren;
410 : 2219 : TNode v = qvars[i];
411 : 2219 : TNode subs = args[0][i];
412 : 2219 : qchildren.push_back(nm->mkNode(Kind::BOUND_VAR_LIST, qvarsNew));
413 : 2219 : qchildren.push_back(conc[1].substitute(v, subs));
414 : 2219 : conc = nm->mkNode(Kind::FORALL, qchildren);
415 : 2219 : }
416 : 10860 : addLfscRule(cdp, conc, {prevConc}, LfscRule::INSTANTIATE, {args[0][i]});
417 : 3620 : }
418 : 1401 : }
419 : 1401 : break;
420 : 234 : case ProofRule::THEORY_REWRITE:
421 : : {
422 [ - + ][ - + ]: 234 : Assert(args.size() >= 2);
[ - - ]
423 : : ProofRewriteRule idr;
424 [ - + ]: 234 : if (!rewriter::getRewriteRule(args[0], idr))
425 : : {
426 : 234 : return false;
427 : : }
428 [ - + ]: 234 : 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 : 234 : return false;
437 : : }
438 : : }
439 : 0 : break;
440 : 1416834 : default: return false; break;
441 : : }
442 [ - + ][ - + ]: 467479 : AlwaysAssert(cdp->getProofFor(res)->getRule() != ProofRule::ASSUME);
[ - - ]
443 : 467479 : return true;
444 : : }
445 : :
446 : 178778 : void LfscProofPostprocessCallback::updateCong(Node res,
447 : : const std::vector<Node>& children,
448 : : CDProof* cdp,
449 : : Node startOp)
450 : : {
451 : 178778 : Node currEq;
452 : 178778 : size_t i = 0;
453 : 178778 : size_t nchildren = children.size();
454 [ + + ]: 178778 : if (!startOp.isNull())
455 : : {
456 : : // start with reflexive equality on operator
457 : 178390 : 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 : 178778 : Node curL = currEq[0];
466 : 178778 : Node curR = currEq[1];
467 : 178778 : NodeManager* nm = nodeManager();
468 [ + + ]: 499472 : for (; i < nchildren; i++)
469 : : {
470 : : // CONG rules for each child
471 : 320694 : Node nextEq;
472 [ + + ]: 320694 : if (i + 1 == nchildren)
473 : : {
474 : : // if we are at the end, we prove the final equality
475 : 178778 : nextEq = res;
476 : : }
477 : : else
478 : : {
479 : 141916 : curL = nm->mkNode(Kind::HO_APPLY, curL, children[i][0]);
480 : 141916 : curR = nm->mkNode(Kind::HO_APPLY, curR, children[i][1]);
481 : 141916 : nextEq = curL.eqNode(curR);
482 : : }
483 [ + + ][ - - ]: 962082 : addLfscRule(cdp, nextEq, {currEq, children[i]}, LfscRule::CONG, {});
484 : 320694 : currEq = nextEq;
485 : 320694 : }
486 : 178778 : }
487 : :
488 : 1548242 : 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 : 1548242 : std::vector<Node> largs;
496 : 1548242 : largs.push_back(mkLfscRuleNode(nodeManager(), lr));
497 : 1548242 : largs.push_back(conc);
498 : 1548242 : largs.insert(largs.end(), args.begin(), args.end());
499 : 1548242 : cdp->addStep(conc, ProofRule::LFSC_RULE, children, largs);
500 : 1548242 : }
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 : 212353 : Node LfscProofPostprocessCallback::mkDummyPredicate(NodeManager* nm)
525 : : {
526 : 424706 : return NodeManager::mkBoundVar(nm->booleanType());
527 : : }
528 : :
529 : 1750 : LfscProofPostprocess::LfscProofPostprocess(Env& env, LfscNodeConverter& ltp)
530 : 1750 : : EnvObj(env), d_cb(new proof::LfscProofPostprocessCallback(env, ltp))
531 : : {
532 : 1750 : }
533 : :
534 : 1750 : void LfscProofPostprocess::process(std::shared_ptr<ProofNode> pf)
535 : : {
536 : 1750 : d_cb->initializeUpdate();
537 : : // do not automatically add symmetry steps, since this leads to
538 : : // non-termination for example on policy_variable.smt2
539 : 1750 : ProofNodeUpdater updater(d_env, *(d_cb.get()), false, false);
540 : 1750 : updater.process(pf);
541 : 1750 : }
542 : :
543 : : } // namespace proof
544 : : } // namespace cvc5::internal
|
