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