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