1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Andrew Reynolds, Morgan Deters, Tim King |
4 |
|
* |
5 |
|
* This file is part of the cvc5 project. |
6 |
|
* |
7 |
|
* Copyright (c) 2009-2021 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 |
|
* Reference-counted encapsulation of a pointer to node information. |
14 |
|
*/ |
15 |
|
#include "expr/type_node.h" |
16 |
|
|
17 |
|
#include <vector> |
18 |
|
|
19 |
|
#include "expr/datatype_index.h" |
20 |
|
#include "expr/dtype_cons.h" |
21 |
|
#include "expr/node_manager_attributes.h" |
22 |
|
#include "expr/type_properties.h" |
23 |
|
#include "options/base_options.h" |
24 |
|
#include "options/quantifiers_options.h" |
25 |
|
#include "theory/type_enumerator.h" |
26 |
|
#include "util/bitvector.h" |
27 |
|
#include "util/cardinality.h" |
28 |
|
|
29 |
|
using namespace std; |
30 |
|
|
31 |
|
namespace cvc5 { |
32 |
|
|
33 |
10379 |
TypeNode TypeNode::s_null( &expr::NodeValue::null() ); |
34 |
|
|
35 |
2 |
TypeNode TypeNode::substitute( |
36 |
|
const TypeNode& type, |
37 |
|
const TypeNode& replacement, |
38 |
|
std::unordered_map<TypeNode, TypeNode>& cache) const |
39 |
|
{ |
40 |
|
// in cache? |
41 |
2 |
std::unordered_map<TypeNode, TypeNode>::const_iterator i = cache.find(*this); |
42 |
2 |
if(i != cache.end()) { |
43 |
|
return (*i).second; |
44 |
|
} |
45 |
|
|
46 |
|
// otherwise compute |
47 |
4 |
NodeBuilder nb(getKind()); |
48 |
2 |
if(getMetaKind() == kind::metakind::PARAMETERIZED) { |
49 |
|
// push the operator |
50 |
|
nb << TypeNode(d_nv->d_children[0]); |
51 |
|
} |
52 |
6 |
for (TypeNode::const_iterator j = begin(), iend = end(); j != iend; ++j) |
53 |
|
{ |
54 |
4 |
if (*j == type) |
55 |
|
{ |
56 |
4 |
nb << replacement; |
57 |
|
} |
58 |
|
else |
59 |
|
{ |
60 |
|
(*j).substitute(type, replacement); |
61 |
|
} |
62 |
|
} |
63 |
|
|
64 |
|
// put in cache |
65 |
4 |
TypeNode tn = nb.constructTypeNode(); |
66 |
2 |
cache[*this] = tn; |
67 |
2 |
return tn; |
68 |
|
} |
69 |
|
|
70 |
17288 |
Cardinality TypeNode::getCardinality() const { |
71 |
17288 |
return kind::getCardinality(*this); |
72 |
|
} |
73 |
|
|
74 |
|
/** Attribute true for types that have cardinality one */ |
75 |
|
struct TypeCardinalityClassTag |
76 |
|
{ |
77 |
|
}; |
78 |
|
typedef expr::Attribute<TypeCardinalityClassTag, uint64_t> |
79 |
|
TypeCardinalityClassAttr; |
80 |
|
|
81 |
8388165 |
CardinalityClass TypeNode::getCardinalityClass() |
82 |
|
{ |
83 |
|
// check it is already cached |
84 |
8388165 |
if (hasAttribute(TypeCardinalityClassAttr())) |
85 |
|
{ |
86 |
|
return static_cast<CardinalityClass>( |
87 |
8371473 |
getAttribute(TypeCardinalityClassAttr())); |
88 |
|
} |
89 |
16692 |
CardinalityClass ret = CardinalityClass::INFINITE; |
90 |
16692 |
if (isSort()) |
91 |
|
{ |
92 |
1976 |
ret = CardinalityClass::INTERPRETED_ONE; |
93 |
|
} |
94 |
43858 |
else if (isBoolean() || isBitVector() || isFloatingPoint() |
95 |
24801 |
|| isRoundingMode()) |
96 |
|
{ |
97 |
4664 |
ret = CardinalityClass::FINITE; |
98 |
|
} |
99 |
10052 |
else if (isString() || isRegExp() || isSequence() || isReal() || isBag()) |
100 |
|
{ |
101 |
5272 |
ret = CardinalityClass::INFINITE; |
102 |
|
} |
103 |
|
else |
104 |
|
{ |
105 |
|
// recursive case (this may be a parametric sort), we assume infinite for |
106 |
|
// the moment here to prevent infinite loops, which may occur when |
107 |
|
// computing the cardinality of datatype types with foreign types |
108 |
4780 |
setAttribute(TypeCardinalityClassAttr(), static_cast<uint64_t>(ret)); |
109 |
|
|
110 |
4780 |
if (isDatatype()) |
111 |
|
{ |
112 |
5470 |
TypeNode tn = *this; |
113 |
2735 |
const DType& dt = getDType(); |
114 |
2735 |
ret = dt.getCardinalityClass(tn); |
115 |
|
} |
116 |
2045 |
else if (isArray()) |
117 |
|
{ |
118 |
509 |
ret = getArrayConstituentType().getCardinalityClass(); |
119 |
509 |
if (ret == CardinalityClass::FINITE |
120 |
243 |
|| ret == CardinalityClass::INTERPRETED_FINITE) |
121 |
|
{ |
122 |
266 |
CardinalityClass cci = getArrayIndexType().getCardinalityClass(); |
123 |
|
// arrays with both finite element types, we take the max with its |
124 |
|
// index type. |
125 |
266 |
ret = maxCardinalityClass(ret, cci); |
126 |
|
} |
127 |
|
// else, array types whose element type is INFINITE, ONE, or |
128 |
|
// INTERPRETED_ONE have the same cardinality class as their range. |
129 |
|
} |
130 |
1536 |
else if (isSet()) |
131 |
|
{ |
132 |
997 |
CardinalityClass cc = getSetElementType().getCardinalityClass(); |
133 |
997 |
if (cc == CardinalityClass::ONE) |
134 |
|
{ |
135 |
|
// 1 -> 2 |
136 |
19 |
ret = CardinalityClass::FINITE; |
137 |
|
} |
138 |
978 |
else if (ret == CardinalityClass::INTERPRETED_ONE) |
139 |
|
{ |
140 |
|
// maybe 1 -> maybe finite |
141 |
|
ret = CardinalityClass::INTERPRETED_FINITE; |
142 |
|
} |
143 |
|
else |
144 |
|
{ |
145 |
|
// finite or infinite is unchanged |
146 |
978 |
ret = cc; |
147 |
|
} |
148 |
|
} |
149 |
539 |
else if (isFunction()) |
150 |
|
{ |
151 |
534 |
ret = getRangeType().getCardinalityClass(); |
152 |
534 |
if (ret == CardinalityClass::FINITE |
153 |
370 |
|| ret == CardinalityClass::INTERPRETED_FINITE) |
154 |
|
{ |
155 |
|
// we may have a larger cardinality class based on the |
156 |
|
// arguments of the function |
157 |
328 |
std::vector<TypeNode> argTypes = getArgTypes(); |
158 |
430 |
for (size_t i = 0, nargs = argTypes.size(); i < nargs; i++) |
159 |
|
{ |
160 |
266 |
CardinalityClass cca = argTypes[i].getCardinalityClass(); |
161 |
266 |
ret = maxCardinalityClass(ret, cca); |
162 |
|
} |
163 |
|
} |
164 |
|
// else, function types whose range type is INFINITE, ONE, or |
165 |
|
// INTERPRETED_ONE have the same cardinality class as their range. |
166 |
|
} |
167 |
5 |
else if (isConstructor()) |
168 |
|
{ |
169 |
|
// notice that we require computing the cardinality class of the |
170 |
|
// constructor type, which is equivalent to asking how many |
171 |
|
// constructor applications of the given constructor exist. This |
172 |
|
// is used in several places in the decision procedure for datatypes. |
173 |
|
// The cardinality starts with one. |
174 |
5 |
ret = CardinalityClass::ONE; |
175 |
|
// we may have a larger cardinality class based on the |
176 |
|
// arguments of the constructor |
177 |
10 |
std::vector<TypeNode> argTypes = getArgTypes(); |
178 |
11 |
for (size_t i = 0, nargs = argTypes.size(); i < nargs; i++) |
179 |
|
{ |
180 |
6 |
CardinalityClass cca = argTypes[i].getCardinalityClass(); |
181 |
6 |
ret = maxCardinalityClass(ret, cca); |
182 |
|
} |
183 |
|
} |
184 |
|
else |
185 |
|
{ |
186 |
|
// all types we care about should be handled above |
187 |
|
Assert(false); |
188 |
|
} |
189 |
|
} |
190 |
16692 |
setAttribute(TypeCardinalityClassAttr(), static_cast<uint64_t>(ret)); |
191 |
16692 |
return ret; |
192 |
|
} |
193 |
|
|
194 |
|
/** Attribute true for types that are closed enumerable */ |
195 |
|
struct IsClosedEnumerableTag |
196 |
|
{ |
197 |
|
}; |
198 |
|
struct IsClosedEnumerableComputedTag |
199 |
|
{ |
200 |
|
}; |
201 |
|
typedef expr::Attribute<IsClosedEnumerableTag, bool> IsClosedEnumerableAttr; |
202 |
|
typedef expr::Attribute<IsClosedEnumerableComputedTag, bool> |
203 |
|
IsClosedEnumerableComputedAttr; |
204 |
|
|
205 |
86804 |
bool TypeNode::isClosedEnumerable() |
206 |
|
{ |
207 |
|
// check it is already cached |
208 |
86804 |
if (!getAttribute(IsClosedEnumerableComputedAttr())) |
209 |
|
{ |
210 |
2443 |
bool ret = true; |
211 |
2443 |
if (isArray() || isSort() || isCodatatype() || isFunction() || isRegExp()) |
212 |
|
{ |
213 |
549 |
ret = false; |
214 |
|
} |
215 |
1894 |
else if (isSet()) |
216 |
|
{ |
217 |
9 |
ret = getSetElementType().isClosedEnumerable(); |
218 |
|
} |
219 |
1885 |
else if (isSequence()) |
220 |
|
{ |
221 |
3 |
ret = getSequenceElementType().isClosedEnumerable(); |
222 |
|
} |
223 |
1882 |
else if (isDatatype()) |
224 |
|
{ |
225 |
|
// avoid infinite loops: initially set to true |
226 |
451 |
setAttribute(IsClosedEnumerableAttr(), ret); |
227 |
451 |
setAttribute(IsClosedEnumerableComputedAttr(), true); |
228 |
902 |
TypeNode tn = *this; |
229 |
451 |
const DType& dt = getDType(); |
230 |
1102 |
for (uint32_t i = 0, ncons = dt.getNumConstructors(); i < ncons; i++) |
231 |
|
{ |
232 |
1526 |
for (uint32_t j = 0, nargs = dt[i].getNumArgs(); j < nargs; j++) |
233 |
|
{ |
234 |
1546 |
TypeNode ctn = dt[i][j].getRangeType(); |
235 |
875 |
if (tn != ctn && !ctn.isClosedEnumerable()) |
236 |
|
{ |
237 |
204 |
ret = false; |
238 |
204 |
break; |
239 |
|
} |
240 |
|
} |
241 |
855 |
if (!ret) |
242 |
|
{ |
243 |
204 |
break; |
244 |
|
} |
245 |
|
} |
246 |
|
} |
247 |
2443 |
setAttribute(IsClosedEnumerableAttr(), ret); |
248 |
2443 |
setAttribute(IsClosedEnumerableComputedAttr(), true); |
249 |
2443 |
return ret; |
250 |
|
} |
251 |
84361 |
return getAttribute(IsClosedEnumerableAttr()); |
252 |
|
} |
253 |
|
|
254 |
1556097 |
bool TypeNode::isFirstClass() const |
255 |
|
{ |
256 |
3112194 |
return getKind() != kind::CONSTRUCTOR_TYPE && getKind() != kind::SELECTOR_TYPE |
257 |
1556097 |
&& getKind() != kind::TESTER_TYPE && getKind() != kind::UPDATER_TYPE |
258 |
4666305 |
&& (getKind() != kind::TYPE_CONSTANT |
259 |
701876 |
|| (getConst<TypeConstant>() != REGEXP_TYPE |
260 |
2255987 |
&& getConst<TypeConstant>() != SEXPR_TYPE)); |
261 |
|
} |
262 |
|
|
263 |
|
bool TypeNode::isWellFounded() const { |
264 |
|
return kind::isWellFounded(*this); |
265 |
|
} |
266 |
|
|
267 |
196626 |
Node TypeNode::mkGroundTerm() const { |
268 |
196626 |
return kind::mkGroundTerm(*this); |
269 |
|
} |
270 |
|
|
271 |
198389 |
Node TypeNode::mkGroundValue() const |
272 |
|
{ |
273 |
396778 |
theory::TypeEnumerator te(*this); |
274 |
396778 |
return *te; |
275 |
|
} |
276 |
|
|
277 |
6221646 |
bool TypeNode::isStringLike() const { return isString() || isSequence(); } |
278 |
|
|
279 |
10351155 |
bool TypeNode::isSubtypeOf(TypeNode t) const { |
280 |
10351155 |
if(*this == t) { |
281 |
9508122 |
return true; |
282 |
|
} |
283 |
843033 |
if(getKind() == kind::TYPE_CONSTANT) { |
284 |
337717 |
switch(getConst<TypeConstant>()) { |
285 |
265598 |
case INTEGER_TYPE: |
286 |
265598 |
return t.getKind() == kind::TYPE_CONSTANT && t.getConst<TypeConstant>() == REAL_TYPE; |
287 |
72119 |
default: |
288 |
72119 |
return false; |
289 |
|
} |
290 |
|
} |
291 |
505316 |
if (isFunction() && t.isFunction()) |
292 |
|
{ |
293 |
1 |
if (!isComparableTo(t)) |
294 |
|
{ |
295 |
|
// incomparable, not subtype |
296 |
|
return false; |
297 |
|
} |
298 |
1 |
return getRangeType().isSubtypeOf(t.getRangeType()); |
299 |
|
} |
300 |
|
// this should only return true for types T1, T2 where we handle equalities between T1 and T2 |
301 |
|
// (more cases go here, if we want to support such cases) |
302 |
505315 |
return false; |
303 |
|
} |
304 |
|
|
305 |
7564363 |
bool TypeNode::isComparableTo(TypeNode t) const { |
306 |
7564363 |
if(*this == t) { |
307 |
7543049 |
return true; |
308 |
|
} |
309 |
21314 |
if(isSubtypeOf(NodeManager::currentNM()->realType())) { |
310 |
19060 |
return t.isSubtypeOf(NodeManager::currentNM()->realType()); |
311 |
|
} |
312 |
2254 |
if (isFunction() && t.isFunction()) |
313 |
|
{ |
314 |
|
// comparable if they have a common type node |
315 |
3 |
return !leastCommonTypeNode(*this, t).isNull(); |
316 |
|
} |
317 |
2251 |
return false; |
318 |
|
} |
319 |
|
|
320 |
40 |
TypeNode TypeNode::getTesterDomainType() const |
321 |
|
{ |
322 |
40 |
Assert(isTester()); |
323 |
40 |
return (*this)[0]; |
324 |
|
} |
325 |
|
|
326 |
7561 |
TypeNode TypeNode::getSequenceElementType() const |
327 |
|
{ |
328 |
7561 |
Assert(isSequence()); |
329 |
7561 |
return (*this)[0]; |
330 |
|
} |
331 |
|
|
332 |
840374 |
TypeNode TypeNode::getBaseType() const { |
333 |
1680748 |
TypeNode realt = NodeManager::currentNM()->realType(); |
334 |
840374 |
if (isSubtypeOf(realt)) { |
335 |
269726 |
return realt; |
336 |
570648 |
} else if (isParametricDatatype()) { |
337 |
1846 |
std::vector<TypeNode> v; |
338 |
2012 |
for(size_t i = 1; i < getNumChildren(); ++i) { |
339 |
1089 |
v.push_back((*this)[i].getBaseType()); |
340 |
|
} |
341 |
923 |
return (*this)[0].getDType().getTypeNode().instantiateParametricDatatype(v); |
342 |
|
} |
343 |
569725 |
return *this; |
344 |
|
} |
345 |
|
|
346 |
10299 |
std::vector<TypeNode> TypeNode::getArgTypes() const { |
347 |
10299 |
vector<TypeNode> args; |
348 |
10299 |
if(isTester()) { |
349 |
|
Assert(getNumChildren() == 1); |
350 |
|
args.push_back((*this)[0]); |
351 |
|
} else { |
352 |
10299 |
Assert(isFunction() || isConstructor() || isSelector()); |
353 |
27740 |
for(unsigned i = 0, i_end = getNumChildren() - 1; i < i_end; ++i) { |
354 |
17441 |
args.push_back((*this)[i]); |
355 |
|
} |
356 |
|
} |
357 |
10299 |
return args; |
358 |
|
} |
359 |
|
|
360 |
3642 |
std::vector<TypeNode> TypeNode::getParamTypes() const { |
361 |
3642 |
vector<TypeNode> params; |
362 |
3642 |
Assert(isParametricDatatype()); |
363 |
9323 |
for(unsigned i = 1, i_end = getNumChildren(); i < i_end; ++i) { |
364 |
5681 |
params.push_back((*this)[i]); |
365 |
|
} |
366 |
3642 |
return params; |
367 |
|
} |
368 |
|
|
369 |
131804 |
bool TypeNode::isTuple() const |
370 |
|
{ |
371 |
131804 |
return (getKind() == kind::DATATYPE_TYPE && getDType().isTuple()); |
372 |
|
} |
373 |
|
|
374 |
4 |
bool TypeNode::isRecord() const |
375 |
|
{ |
376 |
4 |
return (getKind() == kind::DATATYPE_TYPE && getDType().isRecord()); |
377 |
|
} |
378 |
|
|
379 |
38263 |
size_t TypeNode::getTupleLength() const { |
380 |
38263 |
Assert(isTuple()); |
381 |
38263 |
const DType& dt = getDType(); |
382 |
38263 |
Assert(dt.getNumConstructors() == 1); |
383 |
38263 |
return dt[0].getNumArgs(); |
384 |
|
} |
385 |
|
|
386 |
18434 |
vector<TypeNode> TypeNode::getTupleTypes() const { |
387 |
18434 |
Assert(isTuple()); |
388 |
18434 |
const DType& dt = getDType(); |
389 |
18434 |
Assert(dt.getNumConstructors() == 1); |
390 |
18434 |
vector<TypeNode> types; |
391 |
55471 |
for(unsigned i = 0; i < dt[0].getNumArgs(); ++i) { |
392 |
37037 |
types.push_back(dt[0][i].getRangeType()); |
393 |
|
} |
394 |
18434 |
return types; |
395 |
|
} |
396 |
|
|
397 |
|
/** Is this an instantiated datatype type */ |
398 |
2203 |
bool TypeNode::isInstantiatedDatatype() const { |
399 |
2203 |
if(getKind() == kind::DATATYPE_TYPE) { |
400 |
1662 |
return true; |
401 |
|
} |
402 |
541 |
if(getKind() != kind::PARAMETRIC_DATATYPE) { |
403 |
|
return false; |
404 |
|
} |
405 |
541 |
const DType& dt = (*this)[0].getDType(); |
406 |
541 |
unsigned n = dt.getNumParameters(); |
407 |
541 |
Assert(n < getNumChildren()); |
408 |
1240 |
for(unsigned i = 0; i < n; ++i) { |
409 |
699 |
if (dt.getParameter(i) == (*this)[i + 1]) |
410 |
|
{ |
411 |
|
return false; |
412 |
|
} |
413 |
|
} |
414 |
541 |
return true; |
415 |
|
} |
416 |
|
|
417 |
1522 |
TypeNode TypeNode::instantiateParametricDatatype( |
418 |
|
const std::vector<TypeNode>& params) const |
419 |
|
{ |
420 |
1522 |
AssertArgument(getKind() == kind::PARAMETRIC_DATATYPE, *this); |
421 |
1522 |
AssertArgument(params.size() == getNumChildren() - 1, *this); |
422 |
1522 |
NodeManager* nm = NodeManager::currentNM(); |
423 |
3044 |
TypeNode cons = nm->mkTypeConst((*this)[0].getConst<DatatypeIndexConstant>()); |
424 |
3044 |
std::vector<TypeNode> paramsNodes; |
425 |
1522 |
paramsNodes.push_back(cons); |
426 |
3348 |
for (const TypeNode& t : params) |
427 |
|
{ |
428 |
1826 |
paramsNodes.push_back(t); |
429 |
|
} |
430 |
3044 |
return nm->mkTypeNode(kind::PARAMETRIC_DATATYPE, paramsNodes); |
431 |
|
} |
432 |
|
|
433 |
55 |
uint64_t TypeNode::getSortConstructorArity() const |
434 |
|
{ |
435 |
55 |
Assert(isSortConstructor() && hasAttribute(expr::SortArityAttr())); |
436 |
55 |
return getAttribute(expr::SortArityAttr()); |
437 |
|
} |
438 |
|
|
439 |
4 |
std::string TypeNode::getName() const |
440 |
|
{ |
441 |
4 |
Assert(isSort() || isSortConstructor()); |
442 |
4 |
return getAttribute(expr::VarNameAttr()); |
443 |
|
} |
444 |
|
|
445 |
51 |
TypeNode TypeNode::instantiateSortConstructor( |
446 |
|
const std::vector<TypeNode>& params) const |
447 |
|
{ |
448 |
51 |
Assert(isSortConstructor()); |
449 |
51 |
return NodeManager::currentNM()->mkSort(*this, params); |
450 |
|
} |
451 |
|
|
452 |
|
/** Is this an instantiated datatype parameter */ |
453 |
5465 |
bool TypeNode::isParameterInstantiatedDatatype(unsigned n) const { |
454 |
5465 |
AssertArgument(getKind() == kind::PARAMETRIC_DATATYPE, *this); |
455 |
5465 |
const DType& dt = (*this)[0].getDType(); |
456 |
5465 |
AssertArgument(n < dt.getNumParameters(), *this); |
457 |
5465 |
return dt.getParameter(n) != (*this)[n + 1]; |
458 |
|
} |
459 |
|
|
460 |
7429438 |
TypeNode TypeNode::leastCommonTypeNode(TypeNode t0, TypeNode t1){ |
461 |
7429438 |
return commonTypeNode( t0, t1, true ); |
462 |
|
} |
463 |
|
|
464 |
263221 |
TypeNode TypeNode::mostCommonTypeNode(TypeNode t0, TypeNode t1){ |
465 |
263221 |
return commonTypeNode( t0, t1, false ); |
466 |
|
} |
467 |
|
|
468 |
7692685 |
TypeNode TypeNode::commonTypeNode(TypeNode t0, TypeNode t1, bool isLeast) { |
469 |
7692685 |
Assert(!t0.isNull()); |
470 |
7692685 |
Assert(!t1.isNull()); |
471 |
|
|
472 |
7692685 |
if(__builtin_expect( (t0 == t1), true )) { |
473 |
7636173 |
return t0; |
474 |
|
} |
475 |
|
|
476 |
|
// t0 != t1 && |
477 |
56512 |
if(t0.getKind() == kind::TYPE_CONSTANT) { |
478 |
56456 |
switch(t0.getConst<TypeConstant>()) { |
479 |
16973 |
case INTEGER_TYPE: |
480 |
16973 |
if(t1.isInteger()) { |
481 |
|
// t0 == IntegerType && t1.isInteger() |
482 |
|
return t0; //IntegerType |
483 |
16973 |
} else if(t1.isReal()) { |
484 |
|
// t0 == IntegerType && t1.isReal() && !t1.isInteger() |
485 |
16941 |
return isLeast ? t1 : t0; // RealType |
486 |
|
} else { |
487 |
32 |
return TypeNode(); // null type |
488 |
|
} |
489 |
39423 |
case REAL_TYPE: |
490 |
39423 |
if(t1.isReal()) { |
491 |
39423 |
return isLeast ? t0 : t1; // RealType |
492 |
|
} else { |
493 |
|
return TypeNode(); // null type |
494 |
|
} |
495 |
60 |
default: |
496 |
60 |
return TypeNode(); // null type |
497 |
|
} |
498 |
56 |
} else if(t1.getKind() == kind::TYPE_CONSTANT) { |
499 |
22 |
return commonTypeNode(t1, t0, isLeast); // decrease the number of special cases |
500 |
|
} |
501 |
|
|
502 |
|
// t0 != t1 && |
503 |
|
// t0.getKind() == kind::TYPE_CONSTANT && |
504 |
|
// t1.getKind() == kind::TYPE_CONSTANT |
505 |
34 |
switch(t0.getKind()) { |
506 |
10 |
case kind::FUNCTION_TYPE: |
507 |
|
{ |
508 |
10 |
if (t1.getKind() != kind::FUNCTION_TYPE) |
509 |
|
{ |
510 |
4 |
return TypeNode(); |
511 |
|
} |
512 |
|
// must have equal arguments |
513 |
12 |
std::vector<TypeNode> t0a = t0.getArgTypes(); |
514 |
12 |
std::vector<TypeNode> t1a = t1.getArgTypes(); |
515 |
6 |
if (t0a.size() != t1a.size()) |
516 |
|
{ |
517 |
|
// different arities |
518 |
|
return TypeNode(); |
519 |
|
} |
520 |
10 |
for (unsigned i = 0, nargs = t0a.size(); i < nargs; i++) |
521 |
|
{ |
522 |
6 |
if (t0a[i] != t1a[i]) |
523 |
|
{ |
524 |
|
// an argument is different |
525 |
2 |
return TypeNode(); |
526 |
|
} |
527 |
|
} |
528 |
8 |
TypeNode t0r = t0.getRangeType(); |
529 |
8 |
TypeNode t1r = t1.getRangeType(); |
530 |
8 |
TypeNode tr = commonTypeNode(t0r, t1r, isLeast); |
531 |
8 |
std::vector<TypeNode> ftypes; |
532 |
4 |
ftypes.insert(ftypes.end(), t0a.begin(), t0a.end()); |
533 |
4 |
ftypes.push_back(tr); |
534 |
4 |
return NodeManager::currentNM()->mkFunctionType(ftypes); |
535 |
|
} |
536 |
|
break; |
537 |
24 |
case kind::BITVECTOR_TYPE: |
538 |
|
case kind::FLOATINGPOINT_TYPE: |
539 |
|
case kind::SORT_TYPE: |
540 |
|
case kind::CONSTRUCTOR_TYPE: |
541 |
|
case kind::SELECTOR_TYPE: |
542 |
|
case kind::TESTER_TYPE: |
543 |
|
case kind::ARRAY_TYPE: |
544 |
|
case kind::DATATYPE_TYPE: |
545 |
|
case kind::PARAMETRIC_DATATYPE: |
546 |
|
case kind::SEQUENCE_TYPE: |
547 |
|
case kind::SET_TYPE: |
548 |
|
case kind::BAG_TYPE: |
549 |
|
{ |
550 |
|
// we don't support subtyping except for built in types Int and Real. |
551 |
24 |
return TypeNode(); // return null type |
552 |
|
} |
553 |
|
default: |
554 |
|
Unimplemented() << "don't have a commonType for types `" << t0 |
555 |
|
<< "' and `" << t1 << "'"; |
556 |
|
} |
557 |
|
} |
558 |
|
|
559 |
|
Node TypeNode::getEnsureTypeCondition( Node n, TypeNode tn ) { |
560 |
|
TypeNode ntn = n.getType(); |
561 |
|
Assert(ntn.isComparableTo(tn)); |
562 |
|
if( !ntn.isSubtypeOf( tn ) ){ |
563 |
|
if( tn.isInteger() ){ |
564 |
|
if( tn.isSubtypeOf( ntn ) ){ |
565 |
|
return NodeManager::currentNM()->mkNode( kind::IS_INTEGER, n ); |
566 |
|
} |
567 |
|
}else if( tn.isDatatype() && ntn.isDatatype() ){ |
568 |
|
if( tn.isTuple() && ntn.isTuple() ){ |
569 |
|
const DType& dt1 = tn.getDType(); |
570 |
|
const DType& dt2 = ntn.getDType(); |
571 |
|
NodeManager* nm = NodeManager::currentNM(); |
572 |
|
if( dt1[0].getNumArgs()==dt2[0].getNumArgs() ){ |
573 |
|
std::vector< Node > conds; |
574 |
|
for( unsigned i=0; i<dt2[0].getNumArgs(); i++ ){ |
575 |
|
Node s = nm->mkNode( |
576 |
|
kind::APPLY_SELECTOR_TOTAL, dt2[0][i].getSelector(), n); |
577 |
|
Node etc = getEnsureTypeCondition(s, dt1[0][i].getRangeType()); |
578 |
|
if( etc.isNull() ){ |
579 |
|
return Node::null(); |
580 |
|
}else{ |
581 |
|
conds.push_back( etc ); |
582 |
|
} |
583 |
|
} |
584 |
|
if( conds.empty() ){ |
585 |
|
return nm->mkConst(true); |
586 |
|
}else if( conds.size()==1 ){ |
587 |
|
return conds[0]; |
588 |
|
}else{ |
589 |
|
return nm->mkNode(kind::AND, conds); |
590 |
|
} |
591 |
|
} |
592 |
|
} |
593 |
|
} |
594 |
|
return Node::null(); |
595 |
|
}else{ |
596 |
|
return NodeManager::currentNM()->mkConst( true ); |
597 |
|
} |
598 |
|
} |
599 |
|
|
600 |
|
/** Is this a sort kind */ |
601 |
1610345 |
bool TypeNode::isSort() const { |
602 |
1610345 |
return ( getKind() == kind::SORT_TYPE && !hasAttribute(expr::SortArityAttr()) ); |
603 |
|
} |
604 |
|
|
605 |
|
/** Is this a sort constructor kind */ |
606 |
1453 |
bool TypeNode::isSortConstructor() const { |
607 |
1453 |
return getKind() == kind::SORT_TYPE && hasAttribute(expr::SortArityAttr()); |
608 |
|
} |
609 |
|
|
610 |
168667 |
bool TypeNode::isFloatingPoint() const |
611 |
|
{ |
612 |
168667 |
return getKind() == kind::FLOATINGPOINT_TYPE; |
613 |
|
} |
614 |
|
|
615 |
9826150 |
bool TypeNode::isBitVector() const { return getKind() == kind::BITVECTOR_TYPE; } |
616 |
|
|
617 |
13411480 |
bool TypeNode::isDatatype() const |
618 |
|
{ |
619 |
13411480 |
return getKind() == kind::DATATYPE_TYPE |
620 |
13411480 |
|| getKind() == kind::PARAMETRIC_DATATYPE; |
621 |
|
} |
622 |
|
|
623 |
1221983 |
bool TypeNode::isParametricDatatype() const |
624 |
|
{ |
625 |
1221983 |
return getKind() == kind::PARAMETRIC_DATATYPE; |
626 |
|
} |
627 |
|
|
628 |
8605244 |
bool TypeNode::isConstructor() const |
629 |
|
{ |
630 |
8605244 |
return getKind() == kind::CONSTRUCTOR_TYPE; |
631 |
|
} |
632 |
|
|
633 |
2258595 |
bool TypeNode::isSelector() const { return getKind() == kind::SELECTOR_TYPE; } |
634 |
|
|
635 |
2855149 |
bool TypeNode::isTester() const { return getKind() == kind::TESTER_TYPE; } |
636 |
|
|
637 |
194 |
bool TypeNode::isUpdater() const { return getKind() == kind::UPDATER_TYPE; } |
638 |
|
|
639 |
733632 |
bool TypeNode::isCodatatype() const |
640 |
|
{ |
641 |
733632 |
if (isDatatype()) |
642 |
|
{ |
643 |
732173 |
return getDType().isCodatatype(); |
644 |
|
} |
645 |
1459 |
return false; |
646 |
|
} |
647 |
|
|
648 |
8984 |
bool TypeNode::isSygusDatatype() const |
649 |
|
{ |
650 |
8984 |
if (isDatatype()) |
651 |
|
{ |
652 |
8388 |
return getDType().isSygus(); |
653 |
|
} |
654 |
596 |
return false; |
655 |
|
} |
656 |
|
|
657 |
3362 |
std::string TypeNode::toString() const { |
658 |
6724 |
std::stringstream ss; |
659 |
|
Language outlang = |
660 |
3362 |
(this == &s_null) ? Language::LANG_AUTO : options::outputLanguage(); |
661 |
3362 |
d_nv->toStream(ss, -1, 0, outlang); |
662 |
6724 |
return ss.str(); |
663 |
|
} |
664 |
|
|
665 |
7134021 |
const DType& TypeNode::getDType() const |
666 |
|
{ |
667 |
7134021 |
if (getKind() == kind::DATATYPE_TYPE) |
668 |
|
{ |
669 |
7112173 |
DatatypeIndexConstant dic = getConst<DatatypeIndexConstant>(); |
670 |
7112173 |
return NodeManager::currentNM()->getDTypeForIndex(dic.getIndex()); |
671 |
|
} |
672 |
21848 |
Assert(getKind() == kind::PARAMETRIC_DATATYPE); |
673 |
21848 |
return (*this)[0].getDType(); |
674 |
|
} |
675 |
|
|
676 |
61084 |
bool TypeNode::isBag() const |
677 |
|
{ |
678 |
61084 |
return getKind() == kind::BAG_TYPE; |
679 |
|
} |
680 |
|
|
681 |
5572 |
TypeNode TypeNode::getBagElementType() const |
682 |
|
{ |
683 |
5572 |
Assert(isBag()); |
684 |
5572 |
return (*this)[0]; |
685 |
|
} |
686 |
|
|
687 |
2143 |
bool TypeNode::isBitVector(unsigned size) const |
688 |
|
{ |
689 |
2143 |
return (getKind() == kind::BITVECTOR_TYPE |
690 |
2143 |
&& getConst<BitVectorSize>() == size); |
691 |
|
} |
692 |
|
|
693 |
4458037 |
uint32_t TypeNode::getBitVectorSize() const |
694 |
|
{ |
695 |
4458037 |
Assert(isBitVector()); |
696 |
4458037 |
return getConst<BitVectorSize>(); |
697 |
|
} |
698 |
|
|
699 |
|
} // namespace cvc5 |
700 |
|
|
701 |
|
namespace std { |
702 |
|
|
703 |
3907048 |
size_t hash<cvc5::TypeNode>::operator()(const cvc5::TypeNode& tn) const |
704 |
|
{ |
705 |
3907048 |
return tn.getId(); |
706 |
|
} |
707 |
|
|
708 |
31137 |
} // namespace std |