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 : 1722 : LfscProofPostprocessCallback::LfscProofPostprocessCallback(
32 : 1722 : Env& env, LfscNodeConverter& ltp)
33 : : : EnvObj(env),
34 : 1722 : d_pc(env.getProofNodeManager()->getChecker()),
35 : 1722 : d_tproc(ltp),
36 : 3444 : d_numIgnoredScopes(0)
37 : : {
38 : 1722 : }
39 : :
40 : 1722 : void LfscProofPostprocessCallback::initializeUpdate()
41 : : {
42 : 1722 : d_numIgnoredScopes = 0;
43 : 1722 : }
44 : :
45 : 3772437 : bool LfscProofPostprocessCallback::shouldUpdate(
46 : : std::shared_ptr<ProofNode> pn,
47 : : CVC5_UNUSED const std::vector<Node>& fa,
48 : : CVC5_UNUSED bool& continueUpdate)
49 : : {
50 : 3772437 : return pn->getRule() != ProofRule::LFSC_RULE;
51 : : }
52 : :
53 : 2262012 : 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 [ + - ]: 4524024 : Trace("lfsc-pp") << "LfscProofPostprocessCallback::update: " << id
61 : 2262012 : << std::endl;
62 [ + - ]: 2262012 : Trace("lfsc-pp-debug") << "...proves " << res << std::endl;
63 : 2262012 : NodeManager* nm = nodeManager();
64 [ - + ][ - + ]: 2262012 : Assert(id != ProofRule::LFSC_RULE);
[ - - ]
65 : :
66 [ + + ][ + + ]: 2262012 : switch (id)
[ + + ][ + + ]
[ + + ][ + + ]
67 : : {
68 : 142377 : case ProofRule::ASSUME:
69 : : {
70 [ + + ]: 142377 : if (d_defs.find(res) != d_defs.cend())
71 : : {
72 : 301 : addLfscRule(cdp, res, children, LfscRule::DEFINITION, args);
73 : 301 : return true;
74 : : }
75 : 142076 : return false;
76 : : }
77 : : break;
78 : 45804 : 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 [ + + ]: 45804 : if (d_numIgnoredScopes < 2)
85 : : {
86 : : // The arguments of the outer scope are definitions.
87 [ + + ]: 3444 : if (d_numIgnoredScopes == 0)
88 : : {
89 [ + + ]: 2280 : for (const Node& arg : args)
90 : : {
91 : 558 : 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 : 558 : d_tproc.convert(arg);
102 : : }
103 : : }
104 : 3444 : d_numIgnoredScopes++;
105 : : // Note that we do not want to modify the top-most SCOPEs.
106 : 3444 : return false;
107 : : }
108 [ - + ][ - + ]: 42360 : Assert(children.size() == 1);
[ - - ]
109 : : // (SCOPE P :args (F1 ... Fn))
110 : : // becomes
111 : : // (scope _ _ (\ X1 ... (scope _ _ (\ Xn P)) ... ))
112 : 42360 : Node curr = children[0];
113 [ + + ]: 249575 : for (size_t i = 0, nargs = args.size(); i < nargs; i++)
114 : : {
115 : 207215 : 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 : 207215 : Node fconc = mkDummyPredicate(nm);
119 : 621645 : addLfscRule(cdp, fconc, {curr}, LfscRule::LAMBDA, {args[ii]});
120 : : // we use a chained implication (=> F1 ... (=> Fn C)) which avoids
121 : : // aliasing.
122 : 414430 : Node next = nm->mkNode(Kind::OR, args[ii].notNode(), curr);
123 : 621645 : addLfscRule(cdp, next, {fconc}, LfscRule::SCOPE, {args[ii]});
124 : 207215 : curr = next;
125 : 207215 : }
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 [ + + ]: 42360 : 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 : 18534 : 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 : 99279 : addLfscRule(cdp, res, {curr}, LfscRule::PROCESS_SCOPE, {children[0]});
142 : : }
143 : 42360 : }
144 : 42360 : break;
145 : 98035 : case ProofRule::CHAIN_RESOLUTION:
146 : : {
147 : : // turn into binary resolution
148 : 98035 : Node cur = children[0];
149 [ + + ]: 564644 : for (size_t i = 1, size = children.size(); i < size; i++)
150 : : {
151 : 1866436 : std::vector<Node> newChildren{cur, children[i]};
152 : 1866436 : std::vector<Node> newArgs{args[0][i - 1], args[1][i - 1]};
153 : 466609 : cur = d_pc->checkDebug(ProofRule::RESOLUTION, newChildren, newArgs);
154 : 466609 : cdp->addStep(cur, ProofRule::RESOLUTION, newChildren, newArgs);
155 : 466609 : }
156 : 98035 : }
157 : 98035 : break;
158 : 55969 : case ProofRule::SYMM:
159 : : {
160 [ + + ]: 55969 : if (res.getKind() != Kind::NOT)
161 : : {
162 : : // no need to convert (positive) equality symmetry
163 : 55589 : return false;
164 : : }
165 : : // must use alternate SYMM rule for disequality
166 : 760 : addLfscRule(cdp, res, {children[0]}, LfscRule::NEG_SYMM, {});
167 : : }
168 : 380 : break;
169 : 234519 : case ProofRule::TRANS:
170 : : {
171 [ + + ]: 234519 : if (children.size() <= 2)
172 : : {
173 : : // no need to change
174 : 212835 : return false;
175 : : }
176 : : // turn into binary
177 : 21684 : Node cur = children[0];
178 : 21684 : std::unordered_set<Node> processed;
179 : 21684 : processed.insert(children.begin(), children.end());
180 [ + + ]: 92088 : for (size_t i = 1, size = children.size(); i < size; i++)
181 : : {
182 : 281616 : std::vector<Node> newChildren{cur, children[i]};
183 : 70404 : cur = d_pc->checkDebug(ProofRule::TRANS, newChildren, {});
184 [ + + ]: 70404 : if (processed.find(cur) != processed.end())
185 : : {
186 : 14 : continue;
187 : : }
188 : 70390 : processed.insert(cur);
189 : 70390 : cdp->addStep(cur, ProofRule::TRANS, newChildren, {});
190 [ + + ]: 70404 : }
191 : 21684 : }
192 : 21684 : break;
193 : 258867 : case ProofRule::CONG:
194 : : case ProofRule::NARY_CONG:
195 : : {
196 [ - + ][ - + ]: 258867 : Assert(res.getKind() == Kind::EQUAL);
[ - - ]
197 [ - + ][ - + ]: 258867 : Assert(res[0].getOperator() == res[1].getOperator());
[ - - ]
198 [ + - ]: 517734 : Trace("lfsc-pp-cong") << "Processing congruence for " << res << " "
199 [ - + ][ - - ]: 258867 : << res[0].getKind() << std::endl;
200 : : // different for closures
201 [ + + ]: 258867 : if (res[0].isClosure())
202 : : {
203 [ - + ]: 4204 : if (res[0][0] != res[1][0])
204 : : {
205 : : // cannot convert congruence with different variables currently
206 : 0 : return false;
207 : : }
208 : 4204 : Node cop = d_tproc.getOperatorOfClosure(res[0]);
209 : 4204 : Node pcop = d_tproc.getOperatorOfClosure(res[0], false, true);
210 [ + - ]: 4204 : Trace("lfsc-pp-qcong") << "Operator for closure " << cop << std::endl;
211 : : // start with base case body = body'
212 : 4204 : Node curL = children[0][0];
213 : 4204 : Node curR = children[0][1];
214 : 4204 : Node currEq = children[0];
215 [ + - ]: 4204 : Trace("lfsc-pp-qcong") << "Base congruence " << currEq << std::endl;
216 [ + + ]: 12776 : for (size_t i = 0, nvars = res[0][0].getNumChildren(); i < nvars; i++)
217 : : {
218 : 8572 : size_t ii = (nvars - 1) - i;
219 [ + - ]: 8572 : Trace("lfsc-pp-qcong") << "Process child " << i << std::endl;
220 : : // CONG rules for each variable
221 : 17144 : 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 [ + + ]: 17144 : Node vop = d_tproc.getOperatorOfBoundVar(ii == 0 ? cop : pcop, v);
225 : 8572 : Node vopEq = vop.eqNode(vop);
226 : 17144 : cdp->addStep(vopEq, ProofRule::REFL, {}, {vop});
227 : 8572 : Node nextEq;
228 [ + + ]: 8572 : if (i + 1 == nvars)
229 : : {
230 : : // if we are at the end, we prove the final equality
231 : 4204 : nextEq = res;
232 : : }
233 : : else
234 : : {
235 : 4368 : curL = nm->mkNode(Kind::HO_APPLY, vop, curL);
236 : 4368 : curR = nm->mkNode(Kind::HO_APPLY, vop, curR);
237 : 4368 : nextEq = curL.eqNode(curR);
238 : : }
239 [ + + ][ - - ]: 25716 : addLfscRule(cdp, nextEq, {vopEq, currEq}, LfscRule::CONG, {});
240 : 8572 : currEq = nextEq;
241 : 8572 : }
242 : 4204 : return true;
243 : 4204 : }
244 : 254663 : Kind k = res[0].getKind();
245 [ - + ]: 254663 : 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 : 254663 : Node op = d_tproc.getOperatorOfTerm(res[0]);
256 [ + - ]: 509326 : Trace("lfsc-pp-cong") << "Processing cong for op " << op << " "
257 [ - + ][ - - ]: 254663 : << op.getType() << std::endl;
258 [ - + ][ - + ]: 254663 : Assert(!op.isNull());
[ - - ]
259 : : // initial base step is REFL
260 : 254663 : Node opEq = op.eqNode(op);
261 : 509326 : cdp->addStep(opEq, ProofRule::REFL, {}, {op});
262 : 254663 : size_t nchildren = children.size();
263 : 509326 : 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 [ + + ]: 399169 : bool isNary = NodeManager::isNAryKind(k) && k != Kind::APPLY_CONSTRUCTOR
271 [ + + ][ + + ]: 399169 : && k != Kind::APPLY_UF;
272 [ + + ][ + + ]: 254663 : 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 : 79227 : Node currEq;
278 [ + - ]: 79227 : if (!nullTerm.isNull())
279 : : {
280 : 79227 : 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 : 158454 : 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 [ + + ]: 384246 : for (size_t i = 0; i < nchildren; i++)
291 : : {
292 : 305019 : size_t ii = (nchildren - 1) - i;
293 [ + - ]: 305019 : Trace("lfsc-pp-cong") << "Process child " << ii << std::endl;
294 : 305019 : 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 [ + + ][ + + ]: 305019 : if (k == Kind::BITVECTOR_CONCAT || k == Kind::ADD || k == Kind::MULT
[ + + ]
298 [ + + ]: 235345 : || k == Kind::NONLINEAR_MULT)
299 : : {
300 : : // we get the operator of the next argument concatenated with the
301 : : // current accumulated remainder.
302 : 140522 : Node currApp = nm->mkNode(k, children[ii][0], currEq[0]);
303 : 70261 : uop = d_tproc.getOperatorOfTerm(currApp);
304 : 70261 : }
305 [ + - ][ - - ]: 610038 : Trace("lfsc-pp-cong") << "Apply " << uop << " to " << children[ii][0]
306 [ - + ][ - + ]: 305019 : << " and " << children[ii][1] << std::endl;
[ - - ]
307 : : Node argAppEq =
308 : 610038 : nm->mkNode(Kind::HO_APPLY, uop, children[ii][0])
309 : 610038 : .eqNode(nm->mkNode(Kind::HO_APPLY, uop, children[ii][1]));
310 [ + + ][ - - ]: 915057 : addLfscRule(cdp, argAppEq, {opEq, children[ii]}, LfscRule::CONG, {});
311 : : // now, congruence to the current equality
312 : 305019 : Node nextEq;
313 [ + + ]: 305019 : if (ii == 0)
314 : : {
315 : : // use final conclusion
316 : 79227 : nextEq = res;
317 : : }
318 : : else
319 : : {
320 : : // otherwise continue to apply
321 : : nextEq =
322 : 451584 : nm->mkNode(Kind::HO_APPLY, argAppEq[0], currEq[0])
323 : 225792 : .eqNode(nm->mkNode(Kind::HO_APPLY, argAppEq[1], currEq[1]));
324 : : }
325 [ + + ][ - - ]: 915057 : addLfscRule(cdp, nextEq, {argAppEq, currEq}, LfscRule::CONG, {});
326 : 305019 : currEq = nextEq;
327 : 305019 : }
328 : 79227 : }
329 : : else
330 : : {
331 : : // non n-ary kinds do not have null terminators
332 [ - + ][ - + ]: 175436 : Assert(nullTerm.isNull());
[ - - ]
333 : 175436 : updateCong(res, children, cdp, op);
334 : : }
335 : 254663 : }
336 : 254663 : 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 : 31253 : case ProofRule::AND_INTRO:
344 : : {
345 : 31253 : Node cur = d_tproc.getNullTerminator(nm, Kind::AND);
346 : 31253 : size_t nchildren = children.size();
347 [ + + ]: 129106 : for (size_t j = 0; j < nchildren; j++)
348 : : {
349 : 97853 : size_t jj = (nchildren - 1) - j;
350 : : // conclude the final conclusion if we are finished
351 : 164453 : Node next = jj == 0 ? res : nm->mkNode(Kind::AND, children[jj], cur);
352 [ + + ]: 97853 : if (j == 0)
353 : : {
354 : 62506 : addLfscRule(cdp, next, {children[jj]}, LfscRule::AND_INTRO1, {});
355 : : }
356 : : else
357 : : {
358 [ + + ][ - - ]: 199800 : addLfscRule(cdp, next, {children[jj], cur}, LfscRule::AND_INTRO2, {});
359 : : }
360 : 97853 : cur = next;
361 : 97853 : }
362 : 31253 : }
363 : 31253 : break;
364 : 5282 : case ProofRule::ARITH_SUM_UB:
365 : : {
366 : : // proof of null terminator base 0 = 0
367 : 10564 : Node zero = d_tproc.getNullTerminator(nm, Kind::ADD, res[0].getType());
368 : 5282 : Node cur = zero.eqNode(zero);
369 : 10564 : cdp->addStep(cur, ProofRule::REFL, {}, {zero});
370 [ + + ]: 32839 : for (size_t i = 0, size = children.size(); i < size; i++)
371 : : {
372 : 27557 : size_t ii = (children.size() - 1) - i;
373 : 110228 : std::vector<Node> newChildren{children[ii], cur};
374 [ + + ]: 27557 : if (ii == 0)
375 : : {
376 : : // final rule must be the real conclusion
377 : 5282 : addLfscRule(cdp, res, newChildren, LfscRule::ARITH_SUM_UB, {});
378 : : }
379 : : else
380 : : {
381 : : // rules build an n-ary chain of + on both sides
382 : 22275 : cur = d_pc->checkDebug(ProofRule::ARITH_SUM_UB, newChildren, {});
383 : 22275 : addLfscRule(cdp, cur, newChildren, LfscRule::ARITH_SUM_UB, {});
384 : : }
385 : 27557 : }
386 : 5282 : }
387 : 5282 : break;
388 : 1373 : case ProofRule::INSTANTIATE:
389 : : {
390 : 1373 : Node q = children[0];
391 [ - + ][ - + ]: 1373 : Assert(q.getKind() == Kind::FORALL);
[ - - ]
392 : 1373 : std::vector<Node> terms;
393 : 2746 : std::vector<Node> qvars(q[0].begin(), q[0].end());
394 : 1373 : Node conc = q;
395 [ + + ]: 4878 : for (size_t i = 0, nvars = q[0].getNumChildren(); i < nvars; i++)
396 : : {
397 [ - + ][ - + ]: 3505 : Assert(conc.getKind() == Kind::FORALL);
[ - - ]
398 : 3505 : Node prevConc = conc;
399 [ + + ]: 3505 : if (i + 1 == nvars)
400 : : {
401 : 1373 : conc = res;
402 : : }
403 : : else
404 : : {
405 [ - + ][ - + ]: 2132 : Assert(i + 1 < qvars.size());
[ - - ]
406 : 2132 : std::vector<Node> qvarsNew(qvars.begin() + i + 1, qvars.end());
407 [ - + ][ - + ]: 2132 : Assert(!qvarsNew.empty());
[ - - ]
408 [ - + ][ - + ]: 8528 : AssertEqual(qvars[i].getType(), args[0][i].getType());
[ - - ]
409 : 2132 : std::vector<Node> qchildren;
410 : 2132 : TNode v = qvars[i];
411 : 2132 : TNode subs = args[0][i];
412 : 2132 : qchildren.push_back(nm->mkNode(Kind::BOUND_VAR_LIST, qvarsNew));
413 : 2132 : qchildren.push_back(conc[1].substitute(v, subs));
414 : 2132 : conc = nm->mkNode(Kind::FORALL, qchildren);
415 : 2132 : }
416 : 10515 : addLfscRule(cdp, conc, {prevConc}, LfscRule::INSTANTIATE, {args[0][i]});
417 : 3505 : }
418 : 1373 : }
419 : 1373 : 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 : 1387899 : default: return false; break;
441 : : }
442 [ - + ][ - + ]: 455418 : AlwaysAssert(cdp->getProofFor(res)->getRule() != ProofRule::ASSUME);
[ - - ]
443 : 455418 : return true;
444 : : }
445 : :
446 : 175824 : void LfscProofPostprocessCallback::updateCong(Node res,
447 : : const std::vector<Node>& children,
448 : : CDProof* cdp,
449 : : Node startOp)
450 : : {
451 : 175824 : Node currEq;
452 : 175824 : size_t i = 0;
453 : 175824 : size_t nchildren = children.size();
454 [ + + ]: 175824 : if (!startOp.isNull())
455 : : {
456 : : // start with reflexive equality on operator
457 : 175436 : 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 : 175824 : Node curL = currEq[0];
466 : 175824 : Node curR = currEq[1];
467 : 175824 : NodeManager* nm = nodeManager();
468 [ + + ]: 490877 : for (; i < nchildren; i++)
469 : : {
470 : : // CONG rules for each child
471 : 315053 : Node nextEq;
472 [ + + ]: 315053 : if (i + 1 == nchildren)
473 : : {
474 : : // if we are at the end, we prove the final equality
475 : 175824 : nextEq = res;
476 : : }
477 : : else
478 : : {
479 : 139229 : curL = nm->mkNode(Kind::HO_APPLY, curL, children[i][0]);
480 : 139229 : curR = nm->mkNode(Kind::HO_APPLY, curR, children[i][1]);
481 : 139229 : nextEq = curL.eqNode(curR);
482 : : }
483 [ + + ][ - - ]: 945159 : addLfscRule(cdp, nextEq, {currEq, children[i]}, LfscRule::CONG, {});
484 : 315053 : currEq = nextEq;
485 : 315053 : }
486 : 175824 : }
487 : :
488 : 1520049 : 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 : 1520049 : std::vector<Node> largs;
496 : 1520049 : largs.push_back(mkLfscRuleNode(nodeManager(), lr));
497 : 1520049 : largs.push_back(conc);
498 : 1520049 : largs.insert(largs.end(), args.begin(), args.end());
499 : 1520049 : cdp->addStep(conc, ProofRule::LFSC_RULE, children, largs);
500 : 1520049 : }
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 : 207215 : Node LfscProofPostprocessCallback::mkDummyPredicate(NodeManager* nm)
525 : : {
526 : 414430 : return NodeManager::mkBoundVar(nm->booleanType());
527 : : }
528 : :
529 : 1722 : LfscProofPostprocess::LfscProofPostprocess(Env& env, LfscNodeConverter& ltp)
530 : 1722 : : EnvObj(env), d_cb(new proof::LfscProofPostprocessCallback(env, ltp))
531 : : {
532 : 1722 : }
533 : :
534 : 1722 : void LfscProofPostprocess::process(std::shared_ptr<ProofNode> pf)
535 : : {
536 : 1722 : d_cb->initializeUpdate();
537 : : // do not automatically add symmetry steps, since this leads to
538 : : // non-termination for example on policy_variable.smt2
539 : 1722 : ProofNodeUpdater updater(d_env, *(d_cb.get()), false, false);
540 : 1722 : updater.process(pf);
541 : 1722 : }
542 : :
543 : : } // namespace proof
544 : : } // namespace cvc5::internal
|
