Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Andrew Reynolds, Aina Niemetz, Amalee Wilson
4 : : *
5 : : * This file is part of the cvc5 project.
6 : : *
7 : : * Copyright (c) 2009-2025 by the authors listed in the file AUTHORS
8 : : * in the top-level source directory and their institutional affiliations.
9 : : * All rights reserved. See the file COPYING in the top-level source
10 : : * directory for licensing information.
11 : : * ****************************************************************************
12 : : *
13 : : * Implementation of skolem manager class.
14 : : */
15 : :
16 : : #include "expr/skolem_manager.h"
17 : :
18 : : #include <sstream>
19 : :
20 : : #include "expr/attribute.h"
21 : : #include "expr/bound_var_manager.h"
22 : : #include "expr/node_algorithm.h"
23 : : #include "expr/node_manager_attributes.h"
24 : : #include "expr/sort_to_term.h"
25 : : #include "util/rational.h"
26 : : #include "util/string.h"
27 : :
28 : : using namespace cvc5::internal::kind;
29 : :
30 : : namespace cvc5::internal {
31 : :
32 : : struct OriginalFormAttributeId
33 : : {
34 : : };
35 : : typedef expr::Attribute<OriginalFormAttributeId, Node> OriginalFormAttribute;
36 : :
37 : : struct UnpurifiedFormAttributeId
38 : : {
39 : : };
40 : : typedef expr::Attribute<UnpurifiedFormAttributeId, Node> UnpurifiedFormAttribute;
41 : :
42 : 28728 : SkolemManager::SkolemManager() : d_skolemCounter(0) {}
43 : :
44 : 368749 : Node SkolemManager::mkPurifySkolem(Node t)
45 : : {
46 : 368749 : SkolemManager* skm = t.getNodeManager()->getSkolemManager();
47 : : // We do not recursively compute the original form of t here
48 : 368749 : Node k = skm->mkSkolemFunction(SkolemId::PURIFY, {t});
49 [ + - ]: 368749 : Trace("sk-manager-skolem") << "skolem: " << k << " purify " << t << std::endl;
50 : 368749 : return k;
51 : : }
52 : :
53 : 374488 : Node SkolemManager::mkSkolemFunction(SkolemId id, Node cacheVal)
54 : : {
55 : 748976 : std::vector<Node> cvals;
56 [ + + ]: 374488 : if (!cacheVal.isNull())
57 : : {
58 [ - + ]: 371394 : if (cacheVal.getKind() == Kind::SEXPR)
59 : : {
60 : 0 : cvals.insert(cvals.end(), cacheVal.begin(), cacheVal.end());
61 : : }
62 : : else
63 : : {
64 : 371394 : cvals.push_back(cacheVal);
65 : : }
66 : : }
67 : 748976 : return mkSkolemFunction(id, cvals);
68 : : }
69 : :
70 : 413711 : Node SkolemManager::mkSkolemFunction(SkolemId id,
71 : : const std::vector<Node>& cacheVals)
72 : : {
73 : 413711 : TypeNode ctn = getTypeFor(id, cacheVals);
74 [ - + ][ - + ]: 413711 : Assert(!ctn.isNull());
[ - - ]
75 : 827422 : return mkSkolemFunctionTyped(id, ctn, cacheVals);
76 : : }
77 : :
78 : 164999 : Node SkolemManager::mkInternalSkolemFunction(InternalSkolemId id,
79 : : TypeNode tn,
80 : : const std::vector<Node>& cacheVals)
81 : : {
82 : 164999 : NodeManager* nm = NodeManager::currentNM();
83 : 164999 : std::vector<Node> cvals;
84 : 164999 : cvals.push_back(nm->mkConstInt(Rational(static_cast<uint32_t>(id))));
85 : 164999 : cvals.insert(cvals.end(), cacheVals.begin(), cacheVals.end());
86 : 329998 : return mkSkolemFunctionTyped(SkolemId::INTERNAL, tn, cvals);
87 : : }
88 : :
89 : 45 : bool SkolemManager::isCommutativeSkolemId(SkolemId id)
90 : : {
91 [ + + ]: 45 : switch (id)
92 : : {
93 : 30 : case cvc5::SkolemId::ARRAY_DEQ_DIFF:
94 : : case cvc5::SkolemId::BAGS_DEQ_DIFF:
95 : : case cvc5::SkolemId::SETS_DEQ_DIFF:
96 : 30 : case cvc5::SkolemId::STRINGS_DEQ_DIFF: return true;
97 : 15 : default: break;
98 : : }
99 : 15 : return false;
100 : : }
101 : :
102 : 578710 : Node SkolemManager::mkSkolemFunctionTyped(SkolemId id,
103 : : TypeNode tn,
104 : : Node cacheVal)
105 : : {
106 : 1157420 : std::tuple<SkolemId, TypeNode, Node> key(id, tn, cacheVal);
107 : : std::map<std::tuple<SkolemId, TypeNode, Node>, Node>::iterator it =
108 : 578710 : d_skolemFuns.find(key);
109 [ + + ]: 578710 : if (it == d_skolemFuns.end())
110 : : {
111 : : // We use @ as a prefix, which follows the SMT-LIB standard indicating
112 : : // internal symbols starting with @ or . are reserved for internal use.
113 : : //
114 : 275980 : std::stringstream ss;
115 : : // Print internal skolems by the internal identifier, otherwise all would
116 : : // be @INTERNAL_*.
117 [ + + ]: 137990 : if (id == SkolemId::INTERNAL)
118 : : {
119 [ + + ]: 14540 : Node cval = cacheVal.getKind() == Kind::SEXPR ? cacheVal[0] : cacheVal;
120 [ - + ][ - + ]: 7270 : Assert(cval.getKind() == Kind::CONST_INTEGER);
[ - - ]
121 : 7270 : Rational r = cval.getConst<Rational>();
122 : 14540 : Assert(r.sgn() >= 0 && r.getNumerator().fitsUnsignedInt());
123 : 7270 : ss << "@"
124 : 7270 : << static_cast<InternalSkolemId>(r.getNumerator().toUnsignedInt());
125 : : }
126 : : else
127 : : {
128 : 130720 : ss << "@" << id;
129 : : }
130 : 275980 : Node k = mkSkolemNode(Kind::SKOLEM, ss.str(), tn);
131 [ + + ]: 137990 : if (id == SkolemId::PURIFY)
132 : : {
133 [ - + ][ - + ]: 106210 : Assert(cacheVal.getType() == tn);
[ - - ]
134 : : // set unpurified form attribute for k
135 : : UnpurifiedFormAttribute ufa;
136 : 106210 : k.setAttribute(ufa, cacheVal);
137 : : // the original form of k can be computed by calling getOriginalForm, but
138 : : // it is not computed here
139 : : }
140 : 137990 : d_skolemFuns[key] = k;
141 : 137990 : d_skolemFunMap[k] = key;
142 [ + - ]: 275980 : Trace("sk-manager-skolem") << "mkSkolemFunction(" << id << ", " << cacheVal
143 : 137990 : << ") returns " << k << std::endl;
144 : 137990 : return k;
145 : : }
146 : 440720 : return it->second;
147 : : }
148 : :
149 : 578710 : Node SkolemManager::mkSkolemFunctionTyped(SkolemId id,
150 : : TypeNode tn,
151 : : const std::vector<Node>& cacheVals)
152 : : {
153 : 578710 : Node cacheVal;
154 : : // use null node if cacheVals is empty
155 [ + + ]: 578710 : if (!cacheVals.empty())
156 : : {
157 : 575609 : cacheVal = cacheVals.size() == 1
158 [ + + ]: 1151220 : ? cacheVals[0]
159 : 575609 : : NodeManager::currentNM()->mkNode(Kind::SEXPR, cacheVals);
160 : : }
161 : 1157420 : return mkSkolemFunctionTyped(id, tn, cacheVal);
162 : : }
163 : :
164 : 0 : bool SkolemManager::isSkolemFunction(TNode k)
165 : : {
166 : 0 : return k.getKind() == Kind::SKOLEM;
167 : : }
168 : :
169 : 1190040 : bool SkolemManager::isSkolemFunction(TNode k,
170 : : SkolemId& id,
171 : : Node& cacheVal)
172 : : {
173 : 1190040 : SkolemManager* skm = k.getNodeManager()->getSkolemManager();
174 [ + + ]: 1190040 : if (k.getKind() != Kind::SKOLEM)
175 : : {
176 : 1167740 : return false;
177 : : }
178 : : std::map<Node, std::tuple<SkolemId, TypeNode, Node>>::const_iterator it =
179 : 22298 : skm->d_skolemFunMap.find(k);
180 [ - + ][ - + ]: 22298 : Assert(it != skm->d_skolemFunMap.end());
[ - - ]
181 : 22298 : id = std::get<0>(it->second);
182 : 22298 : cacheVal = std::get<2>(it->second);
183 : 22298 : return true;
184 : : }
185 : :
186 : 20208 : SkolemId SkolemManager::getId(TNode k) const
187 : : {
188 : : SkolemId id;
189 : 40416 : Node cacheVal;
190 [ + + ]: 20208 : if (isSkolemFunction(k, id, cacheVal))
191 : : {
192 : 127 : return id;
193 : : }
194 : 20081 : return SkolemId::NONE;
195 : : }
196 : :
197 : 15 : std::vector<Node> SkolemManager::getIndices(TNode k) const
198 : : {
199 : 15 : std::vector<Node> vec;
200 : : SkolemId id;
201 : 30 : Node cacheVal;
202 [ + - ]: 15 : if (isSkolemFunction(k, id, cacheVal))
203 : : {
204 [ + - ]: 15 : if (!cacheVal.isNull())
205 : : {
206 [ + - ]: 15 : if (cacheVal.getKind() == Kind::SEXPR)
207 : : {
208 : 15 : vec.insert(vec.end(), cacheVal.begin(), cacheVal.end());
209 : : }
210 : : else
211 : : {
212 : 0 : vec.push_back(cacheVal);
213 : : }
214 : : }
215 : : }
216 : 30 : return vec;
217 : : }
218 : :
219 : 1141300 : InternalSkolemId SkolemManager::getInternalId(TNode k) const
220 : : {
221 : : SkolemId id;
222 : 2282590 : Node cacheVal;
223 : : // if its an internal skolem
224 [ + + ][ + + ]: 1141300 : if (isSkolemFunction(k, id, cacheVal) && id == SkolemId::INTERNAL)
[ + - ][ + + ]
[ - - ]
225 : : {
226 [ - + ][ - + ]: 801 : Assert(!cacheVal.isNull());
[ - - ]
227 [ + + ]: 1602 : Node cval = cacheVal.getKind() == Kind::SEXPR ? cacheVal[0] : cacheVal;
228 [ - + ][ - + ]: 801 : Assert(cval.getKind() == Kind::CONST_INTEGER);
[ - - ]
229 : 801 : Rational r = cval.getConst<Rational>();
230 : 1602 : Assert(r.sgn() >= 0 && r.getNumerator().fitsUnsignedInt());
231 : 801 : return static_cast<InternalSkolemId>(r.getNumerator().toUnsignedInt());
232 : : }
233 : 1140490 : return InternalSkolemId::NONE;
234 : : }
235 : :
236 : 514698 : Node SkolemManager::mkDummySkolem(const std::string& prefix,
237 : : const TypeNode& type,
238 : : const std::string& comment,
239 : : SkolemFlags flags)
240 : : {
241 : 514698 : return mkSkolemNode(Kind::DUMMY_SKOLEM, prefix, type, flags);
242 : : }
243 : :
244 : 232 : bool SkolemManager::isAbstractValue(TNode n) const
245 : : {
246 : 232 : return (getInternalId(n) == InternalSkolemId::ABSTRACT_VALUE);
247 : : }
248 : :
249 : 1354810 : Node SkolemManager::getOriginalForm(Node n)
250 : : {
251 [ - + ]: 1354810 : if (n.isNull())
252 : : {
253 : 0 : return n;
254 : : }
255 [ + - ]: 2709630 : Trace("sk-manager-debug")
256 : 1354810 : << "SkolemManager::getOriginalForm " << n << std::endl;
257 : : OriginalFormAttribute ofa;
258 : : UnpurifiedFormAttribute ufa;
259 : 1354810 : NodeManager* nm = NodeManager::currentNM();
260 : 2709630 : std::unordered_set<TNode> visited;
261 : 1354810 : std::unordered_set<TNode>::iterator it;
262 : 2709630 : std::vector<TNode> visit;
263 : 2709630 : TNode cur;
264 : 1354810 : visit.push_back(n);
265 : 1263050 : do
266 : : {
267 : 2617860 : cur = visit.back();
268 [ + + ]: 2617860 : if (cur.hasAttribute(ofa))
269 : : {
270 : 1704490 : visit.pop_back();
271 : 2236250 : continue;
272 : : }
273 [ + + ]: 913378 : else if (cur.hasAttribute(ufa))
274 : : {
275 : : // if it has an unpurified form, compute the original form of it
276 : 172244 : Node ucur = cur.getAttribute(ufa);
277 [ + + ]: 86122 : if (ucur.hasAttribute(ofa))
278 : : {
279 : : // Already computed, set. This always happens after cur is visited
280 : : // again after computing the original form of its unpurified form.
281 : 94878 : Node ucuro = ucur.getAttribute(ofa);
282 : 47439 : cur.setAttribute(ofa, ucuro);
283 : 47439 : visit.pop_back();
284 : : }
285 : : else
286 : : {
287 : : // visit ucur then visit cur again
288 : 38683 : visit.push_back(ucur);
289 : : }
290 : 86122 : continue;
291 : : }
292 [ + + ]: 827256 : else if (cur.getNumChildren() == 0)
293 : : {
294 : 64026 : cur.setAttribute(ofa, cur);
295 : 64026 : visit.pop_back();
296 : 64026 : continue;
297 : : }
298 : 763230 : it = visited.find(cur);
299 [ + + ]: 763230 : if (it == visited.end())
300 : : {
301 : 381615 : visited.insert(cur);
302 [ + + ]: 381615 : if (cur.getMetaKind() == metakind::PARAMETERIZED)
303 : : {
304 : 15790 : visit.push_back(cur.getOperator());
305 : : }
306 : 381615 : visit.insert(visit.end(), cur.begin(), cur.end());
307 : 381615 : continue;
308 : : }
309 : 381615 : visit.pop_back();
310 : 763230 : Node ret = cur;
311 : 381615 : bool childChanged = false;
312 : 763230 : std::vector<Node> children;
313 [ + + ]: 381615 : if (cur.getMetaKind() == metakind::PARAMETERIZED)
314 : : {
315 : 31580 : const Node& oon = cur.getOperator().getAttribute(ofa);
316 [ - + ][ - + ]: 15790 : Assert(!oon.isNull());
[ - - ]
317 [ + - ][ + + ]: 15790 : childChanged = childChanged || cur.getOperator() != oon;
[ + - ][ - - ]
318 : 15790 : children.push_back(oon);
319 : : }
320 [ + + ]: 1169900 : for (const Node& cn : cur)
321 : : {
322 : 1576560 : const Node& ocn = cn.getAttribute(ofa);
323 [ - + ][ - + ]: 788281 : Assert(!ocn.isNull());
[ - - ]
324 [ + + ][ + + ]: 788281 : childChanged = childChanged || cn != ocn;
325 : 788281 : children.push_back(ocn);
326 : : }
327 [ + + ]: 381615 : if (childChanged)
328 : : {
329 : 163166 : ret = nm->mkNode(cur.getKind(), children);
330 : : }
331 : 381615 : cur.setAttribute(ofa, ret);
332 : :
333 [ + + ]: 2617860 : } while (!visit.empty());
334 : 2709630 : const Node& on = n.getAttribute(ofa);
335 [ + - ]: 1354810 : Trace("sk-manager-debug") << "..return " << on << std::endl;
336 : 1354810 : return on;
337 : : }
338 : :
339 : 286540 : Node SkolemManager::getUnpurifiedForm(Node k)
340 : : {
341 : : UnpurifiedFormAttribute ufa;
342 [ + + ]: 286540 : if (k.hasAttribute(ufa))
343 : : {
344 : 183605 : return k.getAttribute(ufa);
345 : : }
346 : 102935 : return k;
347 : : }
348 : :
349 : 652688 : Node SkolemManager::mkSkolemNode(Kind k,
350 : : const std::string& prefix,
351 : : const TypeNode& type,
352 : : SkolemFlags flags)
353 : : {
354 : 652688 : NodeManager* nm = NodeManager::currentNM();
355 : 652688 : Node n = NodeBuilder(nm, k);
356 : 652688 : if ((flags & SkolemFlags::SKOLEM_EXACT_NAME)
357 [ + + ]: 652688 : == SkolemFlags::SKOLEM_EXACT_NAME)
358 : : {
359 : 415577 : n.setAttribute(expr::VarNameAttr(), prefix);
360 : : }
361 : : else
362 : : {
363 : 237111 : std::stringstream name;
364 : 237111 : name << prefix << '_' << ++d_skolemCounter;
365 : 237111 : n.setAttribute(expr::VarNameAttr(), name.str());
366 : : }
367 : 652688 : n.setAttribute(expr::TypeAttr(), type);
368 : 652688 : n.setAttribute(expr::TypeCheckedAttr(), true);
369 : 652688 : return n;
370 : : }
371 : :
372 : 413711 : TypeNode SkolemManager::getTypeFor(SkolemId id,
373 : : const std::vector<Node>& cacheVals)
374 : : {
375 : 413711 : NodeManager* nm = NodeManager::currentNM();
376 [ + + ][ + + ]: 413711 : switch (id)
[ + + ][ + + ]
[ + + ][ + - ]
[ - + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ - ]
377 : : {
378 : : // Type(cacheVals[0]), i.e skolems that return same type as first argument
379 : 369009 : case SkolemId::PURIFY:
380 : : case SkolemId::TRANSCENDENTAL_PURIFY:
381 [ - + ][ - + ]: 369009 : Assert(cacheVals.size() > 0);
[ - - ]
382 : 369009 : return cacheVals[0].getType();
383 : : break;
384 : 835 : case SkolemId::GROUND_TERM:
385 : : case SkolemId::ARITH_VTS_INFINITY:
386 : : case SkolemId::ARITH_VTS_INFINITY_FREE:
387 : : {
388 [ - + ][ - + ]: 835 : Assert(cacheVals[0].getKind() == Kind::SORT_TO_TERM);
[ - - ]
389 : 835 : return cacheVals[0].getConst<SortToTerm>().getType();
390 : : }
391 : : // real -> real function
392 : 951 : case SkolemId::DIV_BY_ZERO:
393 : : {
394 : 1902 : TypeNode rtype = nm->realType();
395 : 951 : return nm->mkFunctionType(rtype, rtype);
396 : : }
397 : : // real skolems
398 : 859 : case SkolemId::TRANSCENDENTAL_PURIFY_ARG:
399 : : case SkolemId::TRANSCENDENTAL_SINE_PHASE_SHIFT:
400 : : case SkolemId::ARITH_VTS_DELTA:
401 : 859 : case SkolemId::ARITH_VTS_DELTA_FREE: return nm->realType();
402 : : // int -> int function
403 : 1785 : case SkolemId::INT_DIV_BY_ZERO:
404 : : case SkolemId::MOD_BY_ZERO:
405 : : case SkolemId::STRINGS_OCCUR_INDEX:
406 : : case SkolemId::STRINGS_OCCUR_INDEX_RE:
407 : : case SkolemId::STRINGS_OCCUR_LEN_RE:
408 : : case SkolemId::STRINGS_STOI_RESULT:
409 : : case SkolemId::STRINGS_ITOS_RESULT:
410 : : case SkolemId::BAGS_MAP_SUM:
411 : : case SkolemId::BAGS_CARD_COMBINE:
412 : : {
413 : 3570 : TypeNode itype = nm->integerType();
414 : 1785 : return nm->mkFunctionType(itype, itype);
415 : : }
416 : 662 : case SkolemId::BV_EMPTY:
417 : : {
418 : 662 : return nm->mkBitVectorType(0);
419 : : }
420 : : // int -> Type(args[0])
421 : 170 : case SkolemId::STRINGS_REPLACE_ALL_RESULT:
422 : : {
423 [ - + ][ - + ]: 170 : Assert(cacheVals.size() > 0);
[ - - ]
424 : 170 : TypeNode itype = nm->integerType();
425 : 340 : return nm->mkFunctionType(itype, cacheVals[0].getType());
426 : : }
427 : : // integer skolems
428 : 1278 : case SkolemId::STRINGS_NUM_OCCUR:
429 : : case SkolemId::STRINGS_NUM_OCCUR_RE:
430 : : case SkolemId::STRINGS_DEQ_DIFF:
431 : : case SkolemId::STRINGS_STOI_NON_DIGIT:
432 : : case SkolemId::BAGS_FOLD_CARD:
433 : : case SkolemId::SETS_FOLD_CARD:
434 : : case SkolemId::BAGS_DISTINCT_ELEMENTS_SIZE:
435 : 1278 : case SkolemId::BAGS_MAP_INDEX: return nm->integerType();
436 : : // string skolems
437 : 2823 : case SkolemId::RE_FIRST_MATCH_PRE:
438 : : case SkolemId::RE_FIRST_MATCH:
439 : : case SkolemId::RE_FIRST_MATCH_POST:
440 : 2823 : case SkolemId::RE_UNFOLD_POS_COMPONENT: return nm->stringType();
441 : 4052 : case SkolemId::ARRAY_DEQ_DIFF:
442 : : {
443 [ - + ][ - + ]: 4052 : Assert(cacheVals.size() == 2);
[ - - ]
444 : 8104 : TypeNode atype = cacheVals[0].getType();
445 [ - + ][ - + ]: 4052 : Assert(atype.isArray());
[ - - ]
446 : 4052 : return atype.getArrayIndexType();
447 : : }
448 : 12835 : case SkolemId::QUANTIFIERS_SKOLEMIZE:
449 : : {
450 [ - + ][ - + ]: 12835 : Assert(cacheVals.size() == 2);
[ - - ]
451 [ - + ][ - + ]: 12835 : Assert(cacheVals[0].getKind() == Kind::FORALL);
[ - - ]
452 [ - + ][ - + ]: 12835 : Assert(cacheVals[1].getKind() == Kind::CONST_INTEGER);
[ - - ]
453 : 12835 : const Rational& r = cacheVals[1].getConst<Rational>();
454 [ - + ][ - + ]: 12835 : Assert(r.getNumerator().fitsUnsignedInt());
[ - - ]
455 : 12835 : size_t i = r.getNumerator().toUnsignedInt();
456 [ - + ][ - + ]: 12835 : Assert(i < cacheVals[0][0].getNumChildren());
[ - - ]
457 : 12835 : return cacheVals[0][0][i].getType();
458 : : }
459 : : break;
460 : 0 : case SkolemId::WITNESS_STRING_LENGTH:
461 : : {
462 : 0 : Assert(cacheVals.size() == 3);
463 : 0 : Assert(cacheVals[0].getKind() == Kind::SORT_TO_TERM);
464 : 0 : Assert(cacheVals[1].getKind() == Kind::CONST_INTEGER);
465 : 0 : Assert(cacheVals[2].getKind() == Kind::CONST_INTEGER);
466 : 0 : TypeNode t = cacheVals[0].getConst<SortToTerm>().getType();
467 : 0 : return t;
468 : : }
469 : : break;
470 : 0 : case SkolemId::WITNESS_INV_CONDITION:
471 : : {
472 : 0 : Assert(cacheVals.size() == 1);
473 : 0 : Assert(cacheVals[0].getKind() == Kind::EXISTS);
474 : 0 : Assert(cacheVals[0][0].getNumChildren() == 1);
475 : 0 : return cacheVals[0][0][0].getType();
476 : : }
477 : : break;
478 : : // skolems that return the set element type
479 : 5858 : case SkolemId::BAGS_DEQ_DIFF:
480 : : case SkolemId::SETS_DEQ_DIFF:
481 : : {
482 [ - + ][ - + ]: 5858 : Assert(cacheVals.size() > 0);
[ - - ]
483 : 11716 : TypeNode stype = cacheVals[0].getType();
484 [ - + ][ - + ]: 5858 : Assert(stype.getNumChildren() == 1);
[ - - ]
485 : 5858 : return stype[0];
486 : : }
487 : : // skolems that return the set to set element type
488 : 285 : case SkolemId::BAGS_CHOOSE:
489 : : case SkolemId::SETS_CHOOSE:
490 : : {
491 [ - + ][ - + ]: 285 : Assert(cacheVals.size() > 0);
[ - - ]
492 : 285 : TypeNode stype = cacheVals[0].getType();
493 [ - + ][ - + ]: 285 : Assert(stype.getNumChildren() == 1);
[ - - ]
494 : 285 : return nm->mkFunctionType(stype, stype[0]);
495 : : }
496 : 1019 : case SkolemId::TABLES_GROUP_PART:
497 : : case SkolemId::RELATIONS_GROUP_PART:
498 : : {
499 [ - + ][ - + ]: 1019 : Assert(cacheVals.size() > 0);
[ - - ]
500 : 1019 : TypeNode stype = cacheVals[0].getType();
501 [ - + ][ - + ]: 1019 : Assert(stype.getNumChildren() == 1);
[ - - ]
502 : 1019 : stype = stype[0];
503 [ - + ][ - + ]: 1019 : Assert(stype.getNumChildren() == 1);
[ - - ]
504 : 1019 : return nm->mkFunctionType(stype[0], stype);
505 : : }
506 : : // skolems that return the set element of set element type
507 : 211 : case SkolemId::TABLES_GROUP_PART_ELEMENT:
508 : : case SkolemId::RELATIONS_GROUP_PART_ELEMENT:
509 : : {
510 [ - + ][ - + ]: 211 : Assert(cacheVals.size() > 0);
[ - - ]
511 : 422 : TypeNode stype = cacheVals[0].getType();
512 [ - + ][ - + ]: 211 : Assert(stype.getNumChildren() == 1);
[ - - ]
513 : 211 : stype = stype[0];
514 [ - + ][ - + ]: 211 : Assert(stype.getNumChildren() == 1);
[ - - ]
515 : 211 : return stype[0];
516 : : }
517 : 96 : case SkolemId::SETS_MAP_DOWN_ELEMENT:
518 : : {
519 [ + - ][ + - ]: 192 : Assert(cacheVals.size() == 2 && cacheVals[0].getKind() == Kind::SET_MAP);
[ - + ][ - - ]
520 : 192 : TypeNode stype = cacheVals[0][1].getType();
521 [ - + ][ - + ]: 96 : Assert(stype.isSet());
[ - - ]
522 : 96 : return stype.getSetElementType();
523 : : }
524 : 48 : case SkolemId::BAGS_FOLD_UNION_DISJOINT:
525 : : case SkolemId::SETS_FOLD_UNION:
526 : : case SkolemId::BAGS_DISTINCT_ELEMENTS_UNION_DISJOINT:
527 : : {
528 [ - + ][ - + ]: 48 : Assert(cacheVals.size() > 0);
[ - - ]
529 : 48 : TypeNode itype = nm->integerType();
530 : 96 : return nm->mkFunctionType(itype, cacheVals[0].getType());
531 : : }
532 : 84 : case SkolemId::BAGS_DISTINCT_ELEMENTS:
533 : : case SkolemId::BAGS_FOLD_ELEMENTS:
534 : : case SkolemId::SETS_FOLD_ELEMENTS:
535 : : {
536 [ - + ][ - + ]: 84 : Assert(cacheVals.size() > 0);
[ - - ]
537 : 168 : TypeNode itype = nm->integerType();
538 : 168 : TypeNode collectionType = cacheVals[0].getType();
539 [ - + ][ - + ]: 84 : Assert(collectionType.getNumChildren() == 1);
[ - - ]
540 : 168 : TypeNode elementType = collectionType[0];
541 : 84 : return nm->mkFunctionType(itype, elementType);
542 : : }
543 : 14 : case SkolemId::BAGS_FOLD_COMBINE:
544 : : case SkolemId::SETS_FOLD_COMBINE:
545 : : {
546 [ - + ][ - + ]: 14 : Assert(cacheVals.size() == 3);
[ - - ]
547 : 14 : TypeNode itype = nm->integerType();
548 : 28 : return nm->mkFunctionType(itype, cacheVals[1].getType());
549 : : }
550 : 11 : case SkolemId::BAGS_MAP_PREIMAGE_INJECTIVE:
551 : : {
552 [ - + ][ - + ]: 11 : Assert (cacheVals[0].getType().isFunction());
[ - - ]
553 : 22 : return cacheVals[0].getType().getArgTypes()[0];
554 : : }
555 : 2521 : case SkolemId::SHARED_SELECTOR:
556 : : {
557 [ - + ][ - + ]: 2521 : Assert(cacheVals.size() == 3);
[ - - ]
558 [ - + ][ - + ]: 2521 : Assert(cacheVals[0].getKind() == Kind::SORT_TO_TERM);
[ - - ]
559 [ - + ][ - + ]: 2521 : Assert(cacheVals[1].getKind() == Kind::SORT_TO_TERM);
[ - - ]
560 : 5042 : TypeNode dtt = cacheVals[0].getConst<SortToTerm>().getType();
561 : 2521 : TypeNode t = cacheVals[1].getConst<SortToTerm>().getType();
562 : 2521 : return nm->mkSelectorType(dtt, t);
563 : : }
564 : 8160 : case SkolemId::HO_DEQ_DIFF:
565 : : {
566 : 8160 : const Rational& r = cacheVals[2].getConst<Rational>();
567 [ - + ][ - + ]: 8160 : Assert(r.getNumerator().fitsUnsignedInt());
[ - - ]
568 : 8160 : size_t i = r.getNumerator().toUnsignedInt();
569 [ - + ][ - + ]: 8160 : Assert(cacheVals[0].getType().isFunction());
[ - - ]
570 : 16320 : std::vector<TypeNode> argTypes = cacheVals[0].getType().getArgTypes();
571 [ - + ][ - + ]: 8160 : Assert(i < argTypes.size());
[ - - ]
572 : 8160 : return argTypes[i];
573 : : }
574 : : // fp skolems
575 : 12 : case SkolemId::FP_MIN_ZERO:
576 : : case SkolemId::FP_MAX_ZERO:
577 : : {
578 [ - + ][ - + ]: 12 : Assert(cacheVals.size() == 1);
[ - - ]
579 [ - + ][ - + ]: 12 : Assert(cacheVals[0].getKind() == Kind::SORT_TO_TERM);
[ - - ]
580 : 12 : TypeNode type = cacheVals[0].getConst<SortToTerm>().getType();
581 [ - + ][ - + ]: 12 : Assert(type.isFloatingPoint());
[ - - ]
582 [ + + ][ - - ]: 36 : return nm->mkFunctionType({type, type}, nm->mkBitVectorType(1));
583 : : }
584 : 31 : case SkolemId::FP_TO_SBV:
585 : : case SkolemId::FP_TO_UBV:
586 : : {
587 [ - + ][ - + ]: 31 : Assert(cacheVals.size() == 2);
[ - - ]
588 [ - + ][ - + ]: 31 : Assert(cacheVals[0].getKind() == Kind::SORT_TO_TERM);
[ - - ]
589 : 62 : TypeNode fptype = cacheVals[0].getConst<SortToTerm>().getType();
590 [ - + ][ - + ]: 31 : Assert(fptype.isFloatingPoint());
[ - - ]
591 [ - + ][ - + ]: 31 : Assert(cacheVals[1].getKind() == Kind::SORT_TO_TERM);
[ - - ]
592 : 31 : TypeNode bvtype = cacheVals[1].getConst<SortToTerm>().getType();
593 [ - + ][ - + ]: 31 : Assert(bvtype.isBitVector());
[ - - ]
594 [ + + ][ - - ]: 93 : return nm->mkFunctionType({nm->roundingModeType(), fptype}, bvtype);
595 : : }
596 : 18 : case SkolemId::FP_TO_REAL:
597 : : {
598 [ - + ][ - + ]: 18 : Assert(cacheVals.size() == 1);
[ - - ]
599 [ - + ][ - + ]: 18 : Assert(cacheVals[0].getKind() == Kind::SORT_TO_TERM);
[ - - ]
600 : 18 : TypeNode type = cacheVals[0].getConst<SortToTerm>().getType();
601 [ - + ][ - + ]: 18 : Assert(type.isFloatingPoint());
[ - - ]
602 : 36 : return nm->mkFunctionType({type}, nm->realType());
603 : : }
604 : 84 : case SkolemId::BV_TO_INT_UF:
605 : : {
606 [ - + ][ - + ]: 84 : Assert(cacheVals.size() == 1);
[ - - ]
607 : : // fetch the original function
608 : 168 : Node bvUF = cacheVals[0];
609 [ - + ][ - + ]: 84 : Assert(cacheVals[0].getType().isFunction());
[ - - ]
610 : : // old and new types of domain and result
611 : 168 : TypeNode tn = bvUF.getType();
612 : 168 : TypeNode bvRange = tn.getRangeType();
613 : 168 : std::vector<TypeNode> bvDomain = tn.getArgTypes();
614 : 168 : std::vector<TypeNode> intDomain;
615 : :
616 : : // if the original range is a bit-vector sort,
617 : : // the new range should be an integer sort.
618 : : // Otherwise, we keep the original range.
619 : : // Similarly for the domain sorts.
620 [ + + ]: 168 : TypeNode intRange = bvRange.isBitVector() ? nm->integerType() : bvRange;
621 [ + + ]: 197 : for (const TypeNode& d : bvDomain)
622 : : {
623 [ + + ]: 113 : intDomain.push_back(d.isBitVector() ? nm->integerType() : d);
624 : : }
625 : 84 : return nm->mkFunctionType(intDomain, intRange);
626 : : }
627 : : //
628 : 0 : default: break;
629 : : }
630 : 0 : return TypeNode();
631 : : }
632 : :
633 : 86 : size_t SkolemManager::getNumIndicesForSkolemId(SkolemId id) const
634 : : {
635 [ + - ][ + - ]: 86 : switch (id)
[ + - ]
636 : : {
637 : : // Number of skolem indices: 0
638 : 14 : case SkolemId::BV_EMPTY:
639 : : case SkolemId::DIV_BY_ZERO:
640 : : case SkolemId::INT_DIV_BY_ZERO:
641 : 14 : case SkolemId::MOD_BY_ZERO: return 0;
642 : :
643 : : // Number of skolem indices: 1
644 : 0 : case SkolemId::PURIFY:
645 : : case SkolemId::GROUND_TERM:
646 : : case SkolemId::TRANSCENDENTAL_PURIFY:
647 : : case SkolemId::TRANSCENDENTAL_PURIFY_ARG:
648 : : case SkolemId::TRANSCENDENTAL_SINE_PHASE_SHIFT:
649 : : case SkolemId::STRINGS_REPLACE_ALL_RESULT:
650 : : case SkolemId::STRINGS_ITOS_RESULT:
651 : : case SkolemId::STRINGS_STOI_RESULT:
652 : : case SkolemId::STRINGS_STOI_NON_DIGIT:
653 : : case SkolemId::BAGS_CARD_COMBINE:
654 : : case SkolemId::BAGS_DISTINCT_ELEMENTS_UNION_DISJOINT:
655 : : case SkolemId::BAGS_FOLD_CARD:
656 : : case SkolemId::BAGS_FOLD_ELEMENTS:
657 : : case SkolemId::BAGS_FOLD_UNION_DISJOINT:
658 : : case SkolemId::BAGS_CHOOSE:
659 : : case SkolemId::BAGS_DISTINCT_ELEMENTS:
660 : : case SkolemId::BAGS_DISTINCT_ELEMENTS_SIZE:
661 : : case SkolemId::TABLES_GROUP_PART:
662 : : case SkolemId::RELATIONS_GROUP_PART:
663 : : case SkolemId::SETS_CHOOSE:
664 : : case SkolemId::SETS_FOLD_CARD:
665 : : case SkolemId::SETS_FOLD_ELEMENTS:
666 : : case SkolemId::SETS_FOLD_UNION:
667 : : case SkolemId::FP_MIN_ZERO:
668 : : case SkolemId::FP_MAX_ZERO:
669 : : case SkolemId::BV_TO_INT_UF:
670 : 0 : case SkolemId::FP_TO_REAL: return 1;
671 : :
672 : : // Number of skolem indices: 2
673 : 68 : case SkolemId::ARRAY_DEQ_DIFF:
674 : : case SkolemId::QUANTIFIERS_SKOLEMIZE:
675 : : case SkolemId::STRINGS_NUM_OCCUR:
676 : : case SkolemId::STRINGS_OCCUR_INDEX:
677 : : case SkolemId::STRINGS_NUM_OCCUR_RE:
678 : : case SkolemId::STRINGS_OCCUR_INDEX_RE:
679 : : case SkolemId::STRINGS_OCCUR_LEN_RE:
680 : : case SkolemId::STRINGS_DEQ_DIFF:
681 : : case SkolemId::RE_FIRST_MATCH_PRE:
682 : : case SkolemId::RE_FIRST_MATCH:
683 : : case SkolemId::RE_FIRST_MATCH_POST:
684 : : case SkolemId::BAGS_DEQ_DIFF:
685 : : case SkolemId::TABLES_GROUP_PART_ELEMENT:
686 : : case SkolemId::RELATIONS_GROUP_PART_ELEMENT:
687 : : case SkolemId::SETS_DEQ_DIFF:
688 : : case SkolemId::SETS_MAP_DOWN_ELEMENT:
689 : : case SkolemId::FP_TO_SBV:
690 : 68 : case SkolemId::FP_TO_UBV: return 2;
691 : :
692 : : // Number of skolem indices: 3
693 : 0 : case SkolemId::SHARED_SELECTOR:
694 : : case SkolemId::RE_UNFOLD_POS_COMPONENT:
695 : : case SkolemId::BAGS_FOLD_COMBINE:
696 : : case SkolemId::BAGS_MAP_PREIMAGE_INJECTIVE:
697 : : case SkolemId::BAGS_MAP_SUM:
698 : 0 : case SkolemId::SETS_FOLD_COMBINE: return 3;
699 : :
700 : : // Number of skolem indices: 5
701 : 4 : case SkolemId::BAGS_MAP_INDEX: return 5;
702 : :
703 : 0 : default: Unimplemented() << "Unknown skolem kind " << id; break;
704 : : }
705 : : }
706 : :
707 : : } // namespace cvc5::internal
|
