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 : : * The HoElim preprocessing pass.
11 : : *
12 : : * Eliminates higher-order constraints.
13 : : */
14 : :
15 : : #include "preprocessing/passes/ho_elim.h"
16 : :
17 : : #include <sstream>
18 : :
19 : : #include "expr/node_algorithm.h"
20 : : #include "expr/skolem_manager.h"
21 : : #include "options/quantifiers_options.h"
22 : : #include "preprocessing/assertion_pipeline.h"
23 : : #include "preprocessing/preprocessing_pass_context.h"
24 : : #include "theory/rewriter.h"
25 : : #include "theory/uf/function_const.h"
26 : : #include "theory/uf/theory_uf_rewriter.h"
27 : :
28 : : using namespace cvc5::internal::kind;
29 : :
30 : : namespace cvc5::internal {
31 : : namespace preprocessing {
32 : : namespace passes {
33 : :
34 : 28740 : HoElim::HoElim(PreprocessingPassContext* preprocContext)
35 : 28740 : : PreprocessingPass(preprocContext, "ho-elim")
36 : : {
37 : 28740 : d_hoElimSc = nodeManager()->mkSortConstructor("@ho-elim-sort", 1);
38 : 28740 : }
39 : :
40 : 8078 : Node HoElim::eliminateLambdaComplete(Node n, std::map<Node, Node>& newLambda)
41 : : {
42 : 8078 : NodeManager* nm = nodeManager();
43 : 8078 : std::unordered_map<Node, Node>::iterator it;
44 : 8078 : std::vector<Node> visit;
45 : 8078 : TNode cur;
46 : 8078 : visit.push_back(n);
47 : : do
48 : : {
49 : 170965 : cur = visit.back();
50 : 170965 : visit.pop_back();
51 : 170965 : it = d_visited.find(cur);
52 : :
53 [ + + ]: 170965 : if (it == d_visited.end())
54 : : {
55 : 65176 : Node lam = theory::uf::FunctionConst::toLambda(cur);
56 [ + + ]: 65176 : if (!lam.isNull())
57 : : {
58 [ + - ]: 734 : Trace("ho-elim-ll") << "Lambda lift: " << lam << std::endl;
59 : : // must also get free variables in lambda
60 : 734 : std::vector<Node> lvars;
61 : 734 : std::vector<TypeNode> ftypes;
62 : 734 : std::unordered_set<Node> fvs;
63 : 734 : expr::getFreeVariables(lam, fvs);
64 : 734 : std::vector<Node> nvars;
65 : 734 : std::vector<Node> vars;
66 : 734 : Node sbd = lam[1];
67 [ + + ]: 734 : if (!fvs.empty())
68 : : {
69 [ + - ]: 1356 : Trace("ho-elim-ll")
70 : 678 : << "Has " << fvs.size() << " free variables" << std::endl;
71 [ + + ]: 1914 : for (const Node& v : fvs)
72 : : {
73 : 1236 : TypeNode vt = v.getType();
74 : 1236 : ftypes.push_back(vt);
75 : 1236 : Node vs = NodeManager::mkBoundVar(vt);
76 : 1236 : vars.push_back(v);
77 : 1236 : nvars.push_back(vs);
78 : 1236 : lvars.push_back(vs);
79 : 1236 : }
80 : 1356 : sbd = sbd.substitute(
81 : 678 : vars.begin(), vars.end(), nvars.begin(), nvars.end());
82 : : }
83 [ + + ]: 1504 : for (const Node& bv : lam[0])
84 : : {
85 : 770 : TypeNode bvt = bv.getType();
86 : 770 : ftypes.push_back(bvt);
87 : 770 : lvars.push_back(bv);
88 : 1504 : }
89 : 734 : Node nlambda = lam;
90 [ + + ]: 734 : if (!fvs.empty())
91 : : {
92 : 2034 : nlambda = nm->mkNode(
93 : 2034 : Kind::LAMBDA, nm->mkNode(Kind::BOUND_VAR_LIST, lvars), sbd);
94 [ + - ]: 1356 : Trace("ho-elim-ll")
95 : 678 : << "...new lambda definition: " << nlambda << std::endl;
96 : : }
97 : 734 : TypeNode rangeType = lam.getType().getRangeType();
98 : 734 : TypeNode nft = nm->mkFunctionType(ftypes, rangeType);
99 : 1468 : Node nf = NodeManager::mkDummySkolem("ll", nft);
100 [ + - ]: 1468 : Trace("ho-elim-ll")
101 : 734 : << "...introduce: " << nf << " of type " << nft << std::endl;
102 : 734 : newLambda[nf] = nlambda;
103 [ - + ][ - + ]: 2202 : AssertEqual(nf.getType(), nlambda.getType());
[ - - ]
104 [ + + ]: 734 : if (!vars.empty())
105 : : {
106 [ + + ]: 1914 : for (const Node& v : vars)
107 : : {
108 : 1236 : nf = nm->mkNode(Kind::HO_APPLY, nf, v);
109 : : }
110 [ + - ]: 678 : Trace("ho-elim-ll") << "...partial application: " << nf << std::endl;
111 : : }
112 : 734 : d_visited[cur] = nf;
113 [ + - ][ - - ]: 1468 : Trace("ho-elim-ll") << "...return types : " << nf.getType() << " "
114 [ - + ][ - + ]: 734 : << cur.getType() << std::endl;
[ - - ]
115 [ - + ][ - + ]: 2202 : AssertEqual(nf.getType(), cur.getType());
[ - - ]
116 : 734 : }
117 : : else
118 : : {
119 : 64442 : d_visited[cur] = Node::null();
120 : 64442 : visit.push_back(cur);
121 [ + + ]: 162887 : for (const Node& cn : cur)
122 : : {
123 : 98445 : visit.push_back(cn);
124 : 98445 : }
125 : : }
126 : 65176 : }
127 [ + + ]: 105789 : else if (it->second.isNull())
128 : : {
129 : 64442 : Node ret = cur;
130 : 64442 : bool childChanged = false;
131 : 64442 : std::vector<Node> children;
132 [ + + ]: 64442 : if (cur.getMetaKind() == metakind::PARAMETERIZED)
133 : : {
134 : 12488 : children.push_back(cur.getOperator());
135 : : }
136 [ + + ]: 162887 : for (const Node& cn : cur)
137 : : {
138 : 98445 : it = d_visited.find(cn);
139 [ - + ][ - + ]: 98445 : Assert(it != d_visited.end());
[ - - ]
140 [ - + ][ - + ]: 98445 : Assert(!it->second.isNull());
[ - - ]
141 [ + + ][ + + ]: 98445 : childChanged = childChanged || cn != it->second;
142 : 98445 : children.push_back(it->second);
143 : 98445 : }
144 [ + + ]: 64442 : if (childChanged)
145 : : {
146 : 7933 : ret = nm->mkNode(cur.getKind(), children);
147 : : }
148 : 64442 : d_visited[cur] = ret;
149 : 64442 : }
150 [ + + ]: 170965 : } while (!visit.empty());
151 [ - + ][ - + ]: 8078 : Assert(d_visited.find(n) != d_visited.end());
[ - - ]
152 [ - + ][ - + ]: 8078 : Assert(!d_visited.find(n)->second.isNull());
[ - - ]
153 : 16156 : return d_visited[n];
154 : 8078 : }
155 : :
156 : 908 : Node HoElim::reconstructHoFunction(Node n, TypeNode tn)
157 : : {
158 [ - + ][ - + ]: 908 : Assert(tn.isFunction());
[ - - ]
159 : 908 : NodeManager* nm = nodeManager();
160 : 908 : std::vector<Node> args;
161 : 908 : Node curr = n;
162 : 908 : TypeNode ctn = tn;
163 [ + + ]: 2779 : while (ctn.isFunction())
164 : : {
165 : 1871 : std::vector<TypeNode> argTypes = ctn.getArgTypes();
166 [ - + ][ - + ]: 1871 : Assert(!argTypes.empty());
[ - - ]
167 : 1871 : TypeNode argType = argTypes[0];
168 : 1871 : Node v = NodeManager::mkBoundVar(argType);
169 : 1871 : args.push_back(v);
170 : 1871 : TypeNode nextType = ctn.getRangeType();
171 [ + + ]: 1871 : if (argTypes.size() > 1)
172 : : {
173 : 963 : std::vector<TypeNode> remArgTypes;
174 : 2889 : remArgTypes.insert(
175 : 1926 : remArgTypes.end(), argTypes.begin() + 1, argTypes.end());
176 : 963 : nextType = nm->mkFunctionType(remArgTypes, nextType);
177 : 963 : }
178 : : // Use ctnSort, argTypeSort, and nextTypeSort to ensure deterministic node
179 : : // ID assignments
180 : 1871 : TypeNode ctnSort = getUSort(ctn);
181 : 1871 : TypeNode argTypeSort = getUSort(argType);
182 : 1871 : TypeNode nextTypeSort = getUSort(nextType);
183 : 7484 : curr = nm->mkNode(Kind::APPLY_UF,
184 : 3742 : getHoApplyUf(ctnSort, argTypeSort, nextTypeSort),
185 : : curr,
186 : 1871 : v);
187 : 1871 : ctn = nextType;
188 : 1871 : }
189 : 1816 : return nm->mkNode(Kind::LAMBDA, nm->mkNode(Kind::BOUND_VAR_LIST, args), curr);
190 : 908 : }
191 : :
192 : 8139 : Node HoElim::eliminateHo(Node n)
193 : : {
194 [ + - ]: 8139 : Trace("ho-elim-assert") << "Ho-elim assertion: " << n << std::endl;
195 : 8139 : NodeManager* nm = nodeManager();
196 : 8139 : std::unordered_map<Node, Node>::iterator it;
197 : 8139 : std::map<Node, Node> preReplace;
198 : 8139 : std::map<Node, Node>::iterator itr;
199 : 8139 : std::vector<TNode> visit;
200 : 8139 : TNode cur;
201 : 8139 : visit.push_back(n);
202 : : do
203 : : {
204 : 200871 : cur = visit.back();
205 : 200871 : visit.pop_back();
206 : 200871 : it = d_visited.find(cur);
207 [ + - ]: 200871 : Trace("ho-elim-visit") << "Process: " << cur << std::endl;
208 : :
209 [ + + ]: 200871 : if (it == d_visited.end())
210 : : {
211 : 74904 : TypeNode tn = cur.getType();
212 : : // lambdas are already eliminated by now if hoElim
213 [ + + ][ + - ]: 74904 : Assert(!options().quantifiers.hoElim || cur.getKind() != Kind::LAMBDA);
[ - + ][ - + ]
[ - - ]
214 [ + + ]: 74904 : if (tn.isFunction())
215 : : {
216 : 31074 : d_funTypes.insert(tn);
217 : : }
218 [ + + ]: 105978 : bool isFunLeaf = tn.isFunction() && cur.getNumChildren() == 0
219 [ + - ]: 10899 : && cur.getMetaKind() != metakind::PARAMETERIZED
220 [ + + ][ + - ]: 105978 : && cur.getKind() != Kind::LAMBDA;
221 [ + + ][ + + ]: 74904 : if (cur.isVar() || (options().quantifiers.hoElim && isFunLeaf))
[ - + ][ + + ]
222 : : {
223 : 14457 : Node ret = cur;
224 [ + + ][ + + ]: 14457 : if (options().quantifiers.hoElim && tn.isFunction())
[ + + ]
225 : : {
226 : 10864 : TypeNode ut = getUSort(tn);
227 [ + + ]: 10864 : if (cur.getKind() == Kind::BOUND_VARIABLE)
228 : : {
229 : 9222 : ret = NodeManager::mkBoundVar(ut);
230 : : }
231 : : else
232 : : {
233 : 1642 : ret = NodeManager::mkDummySkolem("k", ut);
234 : : }
235 : : // must get the ho apply to ensure extensionality is applied
236 : 10864 : Node hoa = getHoApplyUf(tn);
237 [ + - ]: 10864 : Trace("ho-elim-visit") << "Hoa is " << hoa << std::endl;
238 : 10864 : }
239 : 14457 : d_visited[cur] = ret;
240 : 14457 : }
241 : : else
242 : : {
243 : 60447 : d_visited[cur] = Node::null();
244 [ + + ][ + + ]: 60447 : if (cur.getKind() == Kind::APPLY_UF && options().quantifiers.hoElim)
[ + + ]
245 : : {
246 : 12520 : Node op = cur.getOperator();
247 : : // convert apply uf with variable arguments eagerly to ho apply
248 : : // chains, so they are processed uniformly.
249 : 12520 : visit.push_back(cur);
250 : 12520 : Node newCur = theory::uf::TheoryUfRewriter::getHoApplyForApplyUf(cur);
251 : 12520 : preReplace[cur] = newCur;
252 : 12520 : cur = newCur;
253 : 12520 : d_visited[cur] = Node::null();
254 : 12520 : }
255 : 60447 : visit.push_back(cur);
256 [ + + ]: 180212 : for (const Node& cn : cur)
257 : : {
258 : 119765 : visit.push_back(cn);
259 : 119765 : }
260 : : }
261 : 74904 : }
262 [ + + ]: 125967 : else if (it->second.isNull())
263 : : {
264 : 72967 : Node ret = cur;
265 : 72967 : itr = preReplace.find(cur);
266 [ + + ]: 72967 : if (itr != preReplace.end())
267 : : {
268 [ + - ]: 25040 : Trace("ho-elim-visit")
269 : 12520 : << "return (pre-repl): " << d_visited[itr->second] << std::endl;
270 : 12520 : d_visited[cur] = d_visited[itr->second];
271 : : }
272 : : else
273 : : {
274 : 60447 : bool childChanged = false;
275 : 60447 : std::vector<Node> children;
276 : 60447 : std::vector<TypeNode> childrent;
277 : 60447 : bool typeChanged = false;
278 [ + + ]: 180212 : for (const Node& cn : ret)
279 : : {
280 : 119765 : it = d_visited.find(cn);
281 [ - + ][ - + ]: 119765 : Assert(it != d_visited.end());
[ - - ]
282 [ - + ][ - + ]: 119765 : Assert(!it->second.isNull());
[ - - ]
283 [ + + ][ + + ]: 119765 : childChanged = childChanged || cn != it->second;
284 : 119765 : children.push_back(it->second);
285 : 119765 : TypeNode ct = it->second.getType();
286 : 119765 : childrent.push_back(ct);
287 [ + + ][ + + ]: 119765 : typeChanged = typeChanged || ct != cn.getType();
[ + + ][ - - ]
288 : 119765 : }
289 [ + + ]: 60447 : if (ret.getMetaKind() == metakind::PARAMETERIZED)
290 : : {
291 : : // child of an argument changed type, must change type
292 : 70 : Node op = ret.getOperator();
293 : 70 : Node retOp = op;
294 [ + - ]: 140 : Trace("ho-elim-visit")
295 : 0 : << "Process op " << op << ", typeChanged = " << typeChanged
296 : 70 : << std::endl;
297 [ - + ]: 70 : if (typeChanged)
298 : : {
299 : : std::unordered_map<TNode, Node>::iterator ito =
300 : 0 : d_visited_op.find(op);
301 [ - - ]: 0 : if (ito == d_visited_op.end())
302 : : {
303 : 0 : Assert(!childrent.empty());
304 : 0 : TypeNode newFType = nm->mkFunctionType(childrent, cur.getType());
305 : 0 : retOp = NodeManager::mkDummySkolem("rf", newFType);
306 : 0 : d_visited_op[op] = retOp;
307 : 0 : }
308 : : else
309 : : {
310 : 0 : retOp = ito->second;
311 : : }
312 : : }
313 : 70 : children.insert(children.begin(), retOp);
314 : 70 : }
315 : : // process ho apply
316 [ + + ][ + - ]: 60447 : if (ret.getKind() == Kind::HO_APPLY && options().quantifiers.hoElim)
[ + + ]
317 : : {
318 : 32942 : TypeNode tnr = ret.getType();
319 : 32942 : tnr = getUSort(tnr);
320 : : // Use child0Type and child1Type to ensure deterministic node ID
321 : : // assignments
322 : 32942 : TypeNode child0Type = children[0].getType();
323 : 32942 : TypeNode child1Type = children[1].getType();
324 : 65884 : Node hoa = getHoApplyUf(child0Type, child1Type, tnr);
325 : 32942 : std::vector<Node> hchildren;
326 : 32942 : hchildren.push_back(hoa);
327 : 32942 : hchildren.push_back(children[0]);
328 : 32942 : hchildren.push_back(children[1]);
329 : 32942 : ret = nm->mkNode(Kind::APPLY_UF, hchildren);
330 : 32942 : }
331 [ + + ]: 27505 : else if (childChanged)
332 : : {
333 : 25623 : ret = nm->mkNode(ret.getKind(), children);
334 : : }
335 [ + - ]: 60447 : Trace("ho-elim-visit") << "return (pre-repl): " << ret << std::endl;
336 : 60447 : d_visited[cur] = ret;
337 : 60447 : }
338 : 72967 : }
339 [ + + ]: 200871 : } while (!visit.empty());
340 [ - + ][ - + ]: 8139 : Assert(d_visited.find(n) != d_visited.end());
[ - - ]
341 [ - + ][ - + ]: 8139 : Assert(!d_visited.find(n)->second.isNull());
[ - - ]
342 [ + - ]: 8139 : Trace("ho-elim-assert") << "...got : " << d_visited[n] << std::endl;
343 : 16278 : return d_visited[n];
344 : 8139 : }
345 : :
346 : 1671 : PreprocessingPassResult HoElim::applyInternal(
347 : : AssertionPipeline* assertionsToPreprocess)
348 : : {
349 : : // this preprocessing pass is only applicable if we are eliminating
350 : : // higher-order, or are adding the store axiom
351 [ + + ][ + + ]: 1671 : if (!options().quantifiers.hoElim && !options().quantifiers.hoElimStoreAx)
[ + + ]
352 : : {
353 : 1612 : return PreprocessingPassResult::NO_CONFLICT;
354 : : }
355 : 59 : d_inputFunSymbols.clear();
356 : 59 : std::unordered_set<TNode> visited;
357 : 59 : std::vector<TNode> visit;
358 [ + + ]: 7464 : for (size_t i = 0, size = assertionsToPreprocess->size(); i < size; ++i)
359 : : {
360 : 7405 : visit.push_back((*assertionsToPreprocess)[i]);
361 : : }
362 [ + + ]: 112344 : while (!visit.empty())
363 : : {
364 : 112285 : TNode cur = visit.back();
365 : 112285 : visit.pop_back();
366 [ + + ]: 112285 : if (visited.find(cur) != visited.end())
367 : : {
368 : 51369 : continue;
369 : : }
370 : 60916 : visited.insert(cur);
371 [ + + ][ - - ]: 81640 : bool isInputFunSymbol = cur.getType().isFunction() && cur.isVar()
372 [ + + ]: 8936 : && cur.getKind() != Kind::BOUND_VARIABLE
373 [ + + ][ + - ]: 81640 : && !cur.isSkolem();
[ + - ]
374 [ + + ]: 60916 : if (isInputFunSymbol)
375 : : {
376 : 915 : d_inputFunSymbols.insert(cur);
377 : : }
378 [ + + ]: 60916 : if (cur.getKind() == Kind::APPLY_UF)
379 : : {
380 : 11704 : visit.push_back(cur.getOperator());
381 : : }
382 [ - + ]: 49212 : else if (cur.getMetaKind() == metakind::PARAMETERIZED)
383 : : {
384 : 0 : visit.push_back(cur.getOperator());
385 : : }
386 [ + + ]: 154092 : for (const Node& cn : cur)
387 : : {
388 : 93176 : visit.push_back(cn);
389 : 93176 : }
390 [ + + ]: 112285 : }
391 : : // step [1]: apply lambda lifting to eliminate all lambdas
392 : 59 : NodeManager* nm = nodeManager();
393 : 59 : std::vector<Node> axioms;
394 [ + + ]: 59 : if (options().quantifiers.hoElim)
395 : : {
396 : 45 : std::map<Node, Node> newLambda;
397 [ + + ]: 7389 : for (size_t i = 0, size = assertionsToPreprocess->size(); i < size; ++i)
398 : : {
399 : 7344 : Node prev = (*assertionsToPreprocess)[i];
400 : 7344 : Node res = eliminateLambdaComplete(prev, newLambda);
401 [ + + ]: 7344 : if (res != prev)
402 : : {
403 : 1761 : assertionsToPreprocess->replace(
404 : : i, res, nullptr, TrustId::PREPROCESS_HO_ELIM);
405 : 1761 : assertionsToPreprocess->ensureRewritten(i);
406 [ - + ][ - + ]: 1761 : Assert(!expr::hasFreeVar((*assertionsToPreprocess)[i]));
[ - - ]
407 : : }
408 : 7344 : }
409 : : // do lambda lifting on new lambda definitions
410 : : // this will do fixed point to eliminate lambdas within lambda lifting
411 : : // axioms.
412 [ + + ]: 52 : while (!newLambda.empty())
413 : : {
414 : 7 : std::map<Node, Node> lproc = newLambda;
415 : 7 : newLambda.clear();
416 [ + + ]: 741 : for (const std::pair<const Node, Node>& l : lproc)
417 : : {
418 : 734 : Node lambda = l.second;
419 : 734 : std::vector<Node> vars;
420 : 734 : std::vector<Node> nvars;
421 [ + + ]: 2740 : for (const Node& v : lambda[0])
422 : : {
423 : 2006 : Node bv = NodeManager::mkBoundVar(v.getType());
424 : 2006 : vars.push_back(v);
425 : 2006 : nvars.push_back(bv);
426 : 2740 : }
427 : :
428 : : Node bd = lambda[1].substitute(
429 : 734 : vars.begin(), vars.end(), nvars.begin(), nvars.end());
430 : 734 : Node bvl = nm->mkNode(Kind::BOUND_VAR_LIST, nvars);
431 : :
432 : 734 : nvars.insert(nvars.begin(), l.first);
433 : 734 : Node curr = nm->mkNode(Kind::APPLY_UF, nvars);
434 : :
435 : 1468 : Node llfax = nm->mkNode(Kind::FORALL, bvl, curr.eqNode(bd));
436 [ + - ]: 1468 : Trace("ho-elim-ax") << "Lambda lifting axiom (pre-elim) " << llfax
437 : 734 : << " for " << lambda << std::endl;
438 [ - + ][ - + ]: 734 : Assert(!expr::hasFreeVar(llfax));
[ - - ]
439 : 734 : Node llfaxe = eliminateLambdaComplete(llfax, newLambda);
440 [ + - ]: 1468 : Trace("ho-elim-ax") << "Lambda lifting axiom " << llfaxe << " for "
441 : 734 : << lambda << std::endl;
442 : 734 : axioms.push_back(llfaxe);
443 : 734 : }
444 : 7 : }
445 : :
446 : 45 : d_visited.clear();
447 : : // add lambda lifting axioms as a conjunction to the first assertion
448 [ + + ]: 45 : if (!axioms.empty())
449 : : {
450 [ + + ]: 741 : for (const Node& ax : axioms)
451 : : {
452 : 734 : Node axr = rewrite(ax);
453 [ - + ][ - + ]: 734 : Assert(!expr::hasFreeVar(axr));
[ - - ]
454 : 734 : assertionsToPreprocess->push_back(
455 : : axr, false, nullptr, TrustId::PREPROCESS_HO_ELIM_LEMMA);
456 : 734 : }
457 : : }
458 : 45 : axioms.clear();
459 : 45 : }
460 : :
461 : : // step [2]: eliminate all higher-order constraints
462 [ + + ]: 8198 : for (unsigned i = 0, size = assertionsToPreprocess->size(); i < size; ++i)
463 : : {
464 : 8139 : Node prev = (*assertionsToPreprocess)[i];
465 : 8139 : Node res = eliminateHo(prev);
466 [ + + ]: 8139 : if (res != prev)
467 : : {
468 : 6978 : assertionsToPreprocess->replace(
469 : : i, res, nullptr, TrustId::PREPROCESS_HO_ELIM);
470 : 6978 : assertionsToPreprocess->ensureRewritten(i);
471 [ - + ][ - + ]: 6978 : Assert(!expr::hasFreeVar((*assertionsToPreprocess)[i]));
[ - - ]
472 : : }
473 : 8139 : }
474 : : // step [2b]: record model reconstruction substitutions for original
475 : : // function-typed symbols. These are used to reconstruct values for the
476 : : // original input symbols from the HO encoding introduced by this pass.
477 [ + + ]: 59 : if (options().quantifiers.hoElim)
478 : : {
479 [ + + ]: 953 : for (const Node& orig : d_inputFunSymbols)
480 : : {
481 : 908 : auto itv = d_visited.find(orig);
482 [ + - ]: 1816 : if (itv == d_visited.end() || itv->second.isNull()
483 [ + - ][ - + ]: 2724 : || !orig.getType().isFunction())
[ + - ][ - + ]
[ - - ]
484 : : {
485 : 0 : continue;
486 : : }
487 : 1816 : Node recon = reconstructHoFunction(itv->second, orig.getType());
488 : 908 : d_preprocContext->addSubstitution(orig, recon);
489 : 908 : }
490 : : }
491 : :
492 : : // extensionality: process all function types
493 [ + + ]: 1248 : for (const TypeNode& ftn : d_funTypes)
494 : : {
495 [ + + ]: 1189 : if (options().quantifiers.hoElim)
496 : : {
497 : 1175 : Node h = getHoApplyUf(ftn);
498 [ + - ]: 1175 : Trace("ho-elim-ax") << "Make extensionality for " << h << std::endl;
499 : 1175 : TypeNode ft = h.getType();
500 : 1175 : TypeNode uf = getUSort(ft[0]);
501 : 1175 : TypeNode ut = getUSort(ft[1]);
502 : : // extensionality
503 : 2350 : Node x = NodeManager::mkBoundVar("x", uf);
504 : 2350 : Node y = NodeManager::mkBoundVar("y", uf);
505 : 2350 : Node z = NodeManager::mkBoundVar("z", ut);
506 : 2350 : Node eq = nm->mkNode(Kind::APPLY_UF, h, x, z)
507 : 2350 : .eqNode(nm->mkNode(Kind::APPLY_UF, h, y, z));
508 : : Node antec =
509 : 2350 : nm->mkNode(Kind::FORALL, nm->mkNode(Kind::BOUND_VAR_LIST, z), eq);
510 : 1175 : Node conc = x.eqNode(y);
511 : 3525 : Node ax = nm->mkNode(Kind::FORALL,
512 : 2350 : {nm->mkNode(Kind::BOUND_VAR_LIST, x, y),
513 : 2350 : nm->mkNode(Kind::OR, antec.negate(), conc)});
514 : 1175 : axioms.push_back(ax);
515 [ + - ]: 1175 : Trace("ho-elim-ax") << "...ext axiom : " << ax << std::endl;
516 : : // Make the "store" axiom, which asserts for every function, there
517 : : // exists another function that acts like the "store" operator for
518 : : // arrays, e.g. it is the same function with one I/O pair updated.
519 : : // Without this axiom, the translation is model unsound.
520 [ + - ]: 1175 : if (options().quantifiers.hoElimStoreAx)
521 : : {
522 : 2350 : Node u = NodeManager::mkBoundVar("u", uf);
523 : 2350 : Node v = NodeManager::mkBoundVar("v", uf);
524 : 2350 : Node i = NodeManager::mkBoundVar("i", ut);
525 : 2350 : Node ii = NodeManager::mkBoundVar("ii", ut);
526 : 2350 : Node huii = nm->mkNode(Kind::APPLY_UF, h, u, ii);
527 : 2350 : Node e = NodeManager::mkBoundVar("e", huii.getType());
528 : 3525 : Node store = nm->mkNode(
529 : : Kind::FORALL,
530 : 2350 : {nm->mkNode(Kind::BOUND_VAR_LIST, u, e, i),
531 : 7050 : nm->mkNode(
532 : : Kind::EXISTS,
533 : 2350 : {nm->mkNode(Kind::BOUND_VAR_LIST, v),
534 : 7050 : nm->mkNode(Kind::FORALL,
535 : 2350 : {nm->mkNode(Kind::BOUND_VAR_LIST, ii),
536 : 2350 : nm->mkNode(Kind::APPLY_UF, h, v, ii)
537 : 4700 : .eqNode(nm->mkNode(
538 : 5875 : Kind::ITE, ii.eqNode(i), e, huii))})})});
539 : 1175 : axioms.push_back(store);
540 [ + - ]: 1175 : Trace("ho-elim-ax") << "...store axiom : " << store << std::endl;
541 : 1175 : }
542 : 1175 : }
543 [ + - ]: 14 : else if (options().quantifiers.hoElimStoreAx)
544 : : {
545 : 28 : Node u = NodeManager::mkBoundVar("u", ftn);
546 : 28 : Node v = NodeManager::mkBoundVar("v", ftn);
547 : 14 : std::vector<TypeNode> argTypes = ftn.getArgTypes();
548 : 28 : Node i = NodeManager::mkBoundVar("i", argTypes[0]);
549 : 28 : Node ii = NodeManager::mkBoundVar("ii", argTypes[0]);
550 : 28 : Node huii = nm->mkNode(Kind::HO_APPLY, u, ii);
551 : 28 : Node e = NodeManager::mkBoundVar("e", huii.getType());
552 : 42 : Node store = nm->mkNode(
553 : : Kind::FORALL,
554 : 28 : {nm->mkNode(Kind::BOUND_VAR_LIST, u, e, i),
555 : 84 : nm->mkNode(
556 : : Kind::EXISTS,
557 : 28 : {nm->mkNode(Kind::BOUND_VAR_LIST, v),
558 : 84 : nm->mkNode(Kind::FORALL,
559 : 28 : {nm->mkNode(Kind::BOUND_VAR_LIST, ii),
560 : 28 : nm->mkNode(Kind::HO_APPLY, v, ii)
561 : 56 : .eqNode(nm->mkNode(
562 : 70 : Kind::ITE, ii.eqNode(i), e, huii))})})});
563 : 14 : axioms.push_back(store);
564 [ + - ]: 28 : Trace("ho-elim-ax") << "...store (ho_apply) axiom : " << store
565 : 14 : << std::endl;
566 : 14 : }
567 : : }
568 : : // add new axioms as a conjunction to the first assertion
569 [ + - ]: 59 : if (!axioms.empty())
570 : : {
571 [ + + ]: 2423 : for (const Node& ax : axioms)
572 : : {
573 : 2364 : Node axr = rewrite(ax);
574 [ - + ][ - + ]: 2364 : Assert(!expr::hasFreeVar(axr));
[ - - ]
575 : 2364 : assertionsToPreprocess->push_back(
576 : : axr, false, nullptr, TrustId::PREPROCESS_HO_ELIM_LEMMA);
577 : 2364 : }
578 : : }
579 : :
580 : 59 : return PreprocessingPassResult::NO_CONFLICT;
581 : 59 : }
582 : :
583 : 12039 : Node HoElim::getHoApplyUf(TypeNode tn)
584 : : {
585 : 12039 : TypeNode tnu = getUSort(tn);
586 : 12039 : TypeNode rangeType = tn.getRangeType();
587 : 12039 : std::vector<TypeNode> argTypes = tn.getArgTypes();
588 : 12039 : TypeNode tna = getUSort(argTypes[0]);
589 : :
590 : 12039 : TypeNode tr = rangeType;
591 [ + + ]: 12039 : if (argTypes.size() > 1)
592 : : {
593 : 3171 : std::vector<TypeNode> remArgTypes;
594 : 3171 : remArgTypes.insert(remArgTypes.end(), argTypes.begin() + 1, argTypes.end());
595 : 3171 : tr = nodeManager()->mkFunctionType(remArgTypes, tr);
596 : 3171 : }
597 : 12039 : TypeNode tnr = getUSort(tr);
598 : :
599 : 24078 : return getHoApplyUf(tnu, tna, tnr);
600 : 12039 : }
601 : :
602 : 46852 : Node HoElim::getHoApplyUf(TypeNode tnf, TypeNode tna, TypeNode tnr)
603 : : {
604 : 46852 : std::map<TypeNode, Node>::iterator it = d_hoApplyUf.find(tnf);
605 [ + + ]: 46852 : if (it == d_hoApplyUf.end())
606 : : {
607 : 1175 : NodeManager* nm = nodeManager();
608 : :
609 : 1175 : std::vector<TypeNode> hoTypeArgs;
610 : 1175 : hoTypeArgs.push_back(tnf);
611 : 1175 : hoTypeArgs.push_back(tna);
612 : 1175 : TypeNode tnh = nm->mkFunctionType(hoTypeArgs, tnr);
613 : 2350 : Node k = NodeManager::mkDummySkolem("ho", tnh);
614 : 1175 : d_hoApplyUf[tnf] = k;
615 : 1175 : return k;
616 : 1175 : }
617 : 45677 : return it->second;
618 : : }
619 : :
620 : 89930 : TypeNode HoElim::getUSort(TypeNode tn)
621 : : {
622 [ + + ]: 89930 : if (!tn.isFunction())
623 : : {
624 : 34365 : return tn;
625 : : }
626 : 55565 : std::map<TypeNode, TypeNode>::iterator it = d_ftypeMap.find(tn);
627 [ + + ]: 55565 : if (it == d_ftypeMap.end())
628 : : {
629 : : // flatten function arguments
630 : 1932 : std::vector<TypeNode> argTypes = tn.getArgTypes();
631 : 1932 : TypeNode rangeType = tn.getRangeType();
632 : 1932 : bool typeChanged = false;
633 [ + + ]: 6366 : for (unsigned i = 0; i < argTypes.size(); i++)
634 : : {
635 [ + + ]: 4434 : if (argTypes[i].isFunction())
636 : : {
637 : 1287 : argTypes[i] = getUSort(argTypes[i]);
638 : 1287 : typeChanged = true;
639 : : }
640 : : }
641 : 1932 : TypeNode s;
642 [ + + ]: 1932 : if (typeChanged)
643 : : {
644 : 757 : TypeNode ntn = nodeManager()->mkFunctionType(argTypes, rangeType);
645 : 757 : s = getUSort(ntn);
646 : 757 : }
647 : : else
648 : : {
649 : : // make the uninterpreted sort, given by (ho-elim-sort tn)
650 : 2350 : s = nodeManager()->mkSort(d_hoElimSc, {tn});
651 : : }
652 : 1932 : d_ftypeMap[tn] = s;
653 : 1932 : return s;
654 : 1932 : }
655 : 53633 : return it->second;
656 : : }
657 : :
658 : : } // namespace passes
659 : : } // namespace preprocessing
660 : : } // namespace cvc5::internal
|
