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/dtype_cons.h" |
20 |
|
#include "expr/node_manager_attributes.h" |
21 |
|
#include "expr/type_properties.h" |
22 |
|
#include "options/base_options.h" |
23 |
|
#include "options/quantifiers_options.h" |
24 |
|
#include "theory/type_enumerator.h" |
25 |
|
|
26 |
|
using namespace std; |
27 |
|
|
28 |
|
namespace cvc5 { |
29 |
|
|
30 |
9398 |
TypeNode TypeNode::s_null( &expr::NodeValue::null() ); |
31 |
|
|
32 |
2 |
TypeNode TypeNode::substitute( |
33 |
|
const TypeNode& type, |
34 |
|
const TypeNode& replacement, |
35 |
|
std::unordered_map<TypeNode, TypeNode>& cache) const |
36 |
|
{ |
37 |
|
// in cache? |
38 |
2 |
std::unordered_map<TypeNode, TypeNode>::const_iterator i = cache.find(*this); |
39 |
2 |
if(i != cache.end()) { |
40 |
|
return (*i).second; |
41 |
|
} |
42 |
|
|
43 |
|
// otherwise compute |
44 |
4 |
NodeBuilder nb(getKind()); |
45 |
2 |
if(getMetaKind() == kind::metakind::PARAMETERIZED) { |
46 |
|
// push the operator |
47 |
|
nb << TypeNode(d_nv->d_children[0]); |
48 |
|
} |
49 |
6 |
for (TypeNode::const_iterator j = begin(), iend = end(); j != iend; ++j) |
50 |
|
{ |
51 |
4 |
if (*j == type) |
52 |
|
{ |
53 |
4 |
nb << replacement; |
54 |
|
} |
55 |
|
else |
56 |
|
{ |
57 |
|
(*j).substitute(type, replacement); |
58 |
|
} |
59 |
|
} |
60 |
|
|
61 |
|
// put in cache |
62 |
4 |
TypeNode tn = nb.constructTypeNode(); |
63 |
2 |
cache[*this] = tn; |
64 |
2 |
return tn; |
65 |
|
} |
66 |
|
|
67 |
16586 |
Cardinality TypeNode::getCardinality() const { |
68 |
16586 |
return kind::getCardinality(*this); |
69 |
|
} |
70 |
|
|
71 |
|
/** Attribute true for types that have cardinality one */ |
72 |
|
struct TypeCardinalityClassTag |
73 |
|
{ |
74 |
|
}; |
75 |
|
typedef expr::Attribute<TypeCardinalityClassTag, uint64_t> |
76 |
|
TypeCardinalityClassAttr; |
77 |
|
|
78 |
7022670 |
CardinalityClass TypeNode::getCardinalityClass() |
79 |
|
{ |
80 |
|
// check it is already cached |
81 |
7022670 |
if (hasAttribute(TypeCardinalityClassAttr())) |
82 |
|
{ |
83 |
|
return static_cast<CardinalityClass>( |
84 |
7007252 |
getAttribute(TypeCardinalityClassAttr())); |
85 |
|
} |
86 |
15418 |
CardinalityClass ret = CardinalityClass::INFINITE; |
87 |
15418 |
if (isSort()) |
88 |
|
{ |
89 |
2003 |
ret = CardinalityClass::INTERPRETED_ONE; |
90 |
|
} |
91 |
39997 |
else if (isBoolean() || isBitVector() || isFloatingPoint() |
92 |
21993 |
|| isRoundingMode()) |
93 |
|
{ |
94 |
4860 |
ret = CardinalityClass::FINITE; |
95 |
|
} |
96 |
8555 |
else if (isString() || isRegExp() || isSequence() || isReal() || isBag()) |
97 |
|
{ |
98 |
4519 |
ret = CardinalityClass::INFINITE; |
99 |
|
} |
100 |
|
else |
101 |
|
{ |
102 |
|
// recursive case (this may be a parametric sort), we assume infinite for |
103 |
|
// the moment here to prevent infinite loops, which may occur when |
104 |
|
// computing the cardinality of datatype types with foreign types |
105 |
4036 |
setAttribute(TypeCardinalityClassAttr(), static_cast<uint64_t>(ret)); |
106 |
|
|
107 |
4036 |
if (isDatatype()) |
108 |
|
{ |
109 |
4284 |
TypeNode tn = *this; |
110 |
2142 |
const DType& dt = getDType(); |
111 |
2142 |
ret = dt.getCardinalityClass(tn); |
112 |
|
} |
113 |
1894 |
else if (isArray()) |
114 |
|
{ |
115 |
474 |
ret = getArrayConstituentType().getCardinalityClass(); |
116 |
474 |
if (ret == CardinalityClass::FINITE |
117 |
229 |
|| ret == CardinalityClass::INTERPRETED_FINITE) |
118 |
|
{ |
119 |
245 |
CardinalityClass cci = getArrayIndexType().getCardinalityClass(); |
120 |
|
// arrays with both finite element types, we take the max with its |
121 |
|
// index type. |
122 |
245 |
ret = maxCardinalityClass(ret, cci); |
123 |
|
} |
124 |
|
// else, array types whose element type is INFINITE, ONE, or |
125 |
|
// INTERPRETED_ONE have the same cardinality class as their range. |
126 |
|
} |
127 |
1420 |
else if (isSet()) |
128 |
|
{ |
129 |
933 |
CardinalityClass cc = getSetElementType().getCardinalityClass(); |
130 |
933 |
if (cc == CardinalityClass::ONE) |
131 |
|
{ |
132 |
|
// 1 -> 2 |
133 |
19 |
ret = CardinalityClass::FINITE; |
134 |
|
} |
135 |
914 |
else if (ret == CardinalityClass::INTERPRETED_ONE) |
136 |
|
{ |
137 |
|
// maybe 1 -> maybe finite |
138 |
|
ret = CardinalityClass::INTERPRETED_FINITE; |
139 |
|
} |
140 |
|
else |
141 |
|
{ |
142 |
|
// finite or infinite is unchanged |
143 |
914 |
ret = cc; |
144 |
|
} |
145 |
|
} |
146 |
487 |
else if (isFunction()) |
147 |
|
{ |
148 |
485 |
ret = getRangeType().getCardinalityClass(); |
149 |
485 |
if (ret == CardinalityClass::FINITE |
150 |
345 |
|| ret == CardinalityClass::INTERPRETED_FINITE) |
151 |
|
{ |
152 |
|
// we may have a larger cardinality class based on the |
153 |
|
// arguments of the function |
154 |
280 |
std::vector<TypeNode> argTypes = getArgTypes(); |
155 |
359 |
for (size_t i = 0, nargs = argTypes.size(); i < nargs; i++) |
156 |
|
{ |
157 |
219 |
CardinalityClass cca = argTypes[i].getCardinalityClass(); |
158 |
219 |
ret = maxCardinalityClass(ret, cca); |
159 |
|
} |
160 |
|
} |
161 |
|
// else, function types whose range type is INFINITE, ONE, or |
162 |
|
// INTERPRETED_ONE have the same cardinality class as their range. |
163 |
|
} |
164 |
2 |
else if (isConstructor()) |
165 |
|
{ |
166 |
|
// notice that we require computing the cardinality class of the |
167 |
|
// constructor type, which is equivalent to asking how many |
168 |
|
// constructor applications of the given constructor exist. This |
169 |
|
// is used in several places in the decision procedure for datatypes. |
170 |
|
// The cardinality starts with one. |
171 |
2 |
ret = CardinalityClass::ONE; |
172 |
|
// we may have a larger cardinality class based on the |
173 |
|
// arguments of the constructor |
174 |
4 |
std::vector<TypeNode> argTypes = getArgTypes(); |
175 |
4 |
for (size_t i = 0, nargs = argTypes.size(); i < nargs; i++) |
176 |
|
{ |
177 |
2 |
CardinalityClass cca = argTypes[i].getCardinalityClass(); |
178 |
2 |
ret = maxCardinalityClass(ret, cca); |
179 |
|
} |
180 |
|
} |
181 |
|
else |
182 |
|
{ |
183 |
|
// all types we care about should be handled above |
184 |
|
Assert(false); |
185 |
|
} |
186 |
|
} |
187 |
15418 |
setAttribute(TypeCardinalityClassAttr(), static_cast<uint64_t>(ret)); |
188 |
15418 |
return ret; |
189 |
|
} |
190 |
|
|
191 |
|
/** Attribute true for types that are closed enumerable */ |
192 |
|
struct IsClosedEnumerableTag |
193 |
|
{ |
194 |
|
}; |
195 |
|
struct IsClosedEnumerableComputedTag |
196 |
|
{ |
197 |
|
}; |
198 |
|
typedef expr::Attribute<IsClosedEnumerableTag, bool> IsClosedEnumerableAttr; |
199 |
|
typedef expr::Attribute<IsClosedEnumerableComputedTag, bool> |
200 |
|
IsClosedEnumerableComputedAttr; |
201 |
|
|
202 |
81726 |
bool TypeNode::isClosedEnumerable() |
203 |
|
{ |
204 |
|
// check it is already cached |
205 |
81726 |
if (!getAttribute(IsClosedEnumerableComputedAttr())) |
206 |
|
{ |
207 |
2176 |
bool ret = true; |
208 |
2176 |
if (isArray() || isSort() || isCodatatype() || isFunction()) |
209 |
|
{ |
210 |
511 |
ret = false; |
211 |
|
} |
212 |
1665 |
else if (isSet()) |
213 |
|
{ |
214 |
9 |
ret = getSetElementType().isClosedEnumerable(); |
215 |
|
} |
216 |
1656 |
else if (isSequence()) |
217 |
|
{ |
218 |
3 |
ret = getSequenceElementType().isClosedEnumerable(); |
219 |
|
} |
220 |
1653 |
else if (isDatatype()) |
221 |
|
{ |
222 |
|
// avoid infinite loops: initially set to true |
223 |
337 |
setAttribute(IsClosedEnumerableAttr(), ret); |
224 |
337 |
setAttribute(IsClosedEnumerableComputedAttr(), true); |
225 |
674 |
TypeNode tn = *this; |
226 |
337 |
const DType& dt = getDType(); |
227 |
833 |
for (uint32_t i = 0, ncons = dt.getNumConstructors(); i < ncons; i++) |
228 |
|
{ |
229 |
1213 |
for (uint32_t j = 0, nargs = dt[i].getNumArgs(); j < nargs; j++) |
230 |
|
{ |
231 |
1271 |
TypeNode ctn = dt[i][j].getRangeType(); |
232 |
717 |
if (tn != ctn && !ctn.isClosedEnumerable()) |
233 |
|
{ |
234 |
163 |
ret = false; |
235 |
163 |
break; |
236 |
|
} |
237 |
|
} |
238 |
659 |
if (!ret) |
239 |
|
{ |
240 |
163 |
break; |
241 |
|
} |
242 |
|
} |
243 |
|
} |
244 |
2176 |
setAttribute(IsClosedEnumerableAttr(), ret); |
245 |
2176 |
setAttribute(IsClosedEnumerableComputedAttr(), true); |
246 |
2176 |
return ret; |
247 |
|
} |
248 |
79550 |
return getAttribute(IsClosedEnumerableAttr()); |
249 |
|
} |
250 |
|
|
251 |
1029548 |
bool TypeNode::isFirstClass() const |
252 |
|
{ |
253 |
2059096 |
return getKind() != kind::CONSTRUCTOR_TYPE && getKind() != kind::SELECTOR_TYPE |
254 |
1029548 |
&& getKind() != kind::TESTER_TYPE && getKind() != kind::UPDATER_TYPE |
255 |
3087740 |
&& (getKind() != kind::TYPE_CONSTANT |
256 |
325782 |
|| (getConst<TypeConstant>() != REGEXP_TYPE |
257 |
1354426 |
&& getConst<TypeConstant>() != SEXPR_TYPE)); |
258 |
|
} |
259 |
|
|
260 |
|
bool TypeNode::isWellFounded() const { |
261 |
|
return kind::isWellFounded(*this); |
262 |
|
} |
263 |
|
|
264 |
90889 |
Node TypeNode::mkGroundTerm() const { |
265 |
90889 |
return kind::mkGroundTerm(*this); |
266 |
|
} |
267 |
|
|
268 |
91509 |
Node TypeNode::mkGroundValue() const |
269 |
|
{ |
270 |
183018 |
theory::TypeEnumerator te(*this); |
271 |
183018 |
return *te; |
272 |
|
} |
273 |
|
|
274 |
2833701 |
bool TypeNode::isStringLike() const { return isString() || isSequence(); } |
275 |
|
|
276 |
9536062 |
bool TypeNode::isSubtypeOf(TypeNode t) const { |
277 |
9536062 |
if(*this == t) { |
278 |
8862182 |
return true; |
279 |
|
} |
280 |
673880 |
if(getKind() == kind::TYPE_CONSTANT) { |
281 |
185250 |
switch(getConst<TypeConstant>()) { |
282 |
139015 |
case INTEGER_TYPE: |
283 |
139015 |
return t.getKind() == kind::TYPE_CONSTANT && t.getConst<TypeConstant>() == REAL_TYPE; |
284 |
46235 |
default: |
285 |
46235 |
return false; |
286 |
|
} |
287 |
|
} |
288 |
488630 |
if (isFunction() && t.isFunction()) |
289 |
|
{ |
290 |
|
if (!isComparableTo(t)) |
291 |
|
{ |
292 |
|
// incomparable, not subtype |
293 |
|
return false; |
294 |
|
} |
295 |
|
return getRangeType().isSubtypeOf(t.getRangeType()); |
296 |
|
} |
297 |
|
// this should only return true for types T1, T2 where we handle equalities between T1 and T2 |
298 |
|
// (more cases go here, if we want to support such cases) |
299 |
488630 |
return false; |
300 |
|
} |
301 |
|
|
302 |
7296183 |
bool TypeNode::isComparableTo(TypeNode t) const { |
303 |
7296183 |
if(*this == t) { |
304 |
7278846 |
return true; |
305 |
|
} |
306 |
17337 |
if(isSubtypeOf(NodeManager::currentNM()->realType())) { |
307 |
15094 |
return t.isSubtypeOf(NodeManager::currentNM()->realType()); |
308 |
|
} |
309 |
2243 |
if (isFunction() && t.isFunction()) |
310 |
|
{ |
311 |
|
// comparable if they have a common type node |
312 |
2 |
return !leastCommonTypeNode(*this, t).isNull(); |
313 |
|
} |
314 |
2241 |
return false; |
315 |
|
} |
316 |
|
|
317 |
14 |
TypeNode TypeNode::getTesterDomainType() const |
318 |
|
{ |
319 |
14 |
Assert(isTester()); |
320 |
14 |
return (*this)[0]; |
321 |
|
} |
322 |
|
|
323 |
10278 |
TypeNode TypeNode::getSequenceElementType() const |
324 |
|
{ |
325 |
10278 |
Assert(isSequence()); |
326 |
10278 |
return (*this)[0]; |
327 |
|
} |
328 |
|
|
329 |
661267 |
TypeNode TypeNode::getBaseType() const { |
330 |
1322534 |
TypeNode realt = NodeManager::currentNM()->realType(); |
331 |
661267 |
if (isSubtypeOf(realt)) { |
332 |
133394 |
return realt; |
333 |
527873 |
} else if (isParametricDatatype()) { |
334 |
1920 |
std::vector<TypeNode> v; |
335 |
2135 |
for(size_t i = 1; i < getNumChildren(); ++i) { |
336 |
1175 |
v.push_back((*this)[i].getBaseType()); |
337 |
|
} |
338 |
960 |
return (*this)[0].getDType().getTypeNode().instantiateParametricDatatype(v); |
339 |
|
} |
340 |
526913 |
return *this; |
341 |
|
} |
342 |
|
|
343 |
11999 |
std::vector<TypeNode> TypeNode::getArgTypes() const { |
344 |
11999 |
vector<TypeNode> args; |
345 |
11999 |
if(isTester()) { |
346 |
|
Assert(getNumChildren() == 1); |
347 |
|
args.push_back((*this)[0]); |
348 |
|
} else { |
349 |
11999 |
Assert(isFunction() || isConstructor() || isSelector()); |
350 |
31892 |
for(unsigned i = 0, i_end = getNumChildren() - 1; i < i_end; ++i) { |
351 |
19893 |
args.push_back((*this)[i]); |
352 |
|
} |
353 |
|
} |
354 |
11999 |
return args; |
355 |
|
} |
356 |
|
|
357 |
2070 |
std::vector<TypeNode> TypeNode::getParamTypes() const { |
358 |
2070 |
vector<TypeNode> params; |
359 |
2070 |
Assert(isParametricDatatype()); |
360 |
4660 |
for(unsigned i = 1, i_end = getNumChildren(); i < i_end; ++i) { |
361 |
2590 |
params.push_back((*this)[i]); |
362 |
|
} |
363 |
2070 |
return params; |
364 |
|
} |
365 |
|
|
366 |
120352 |
bool TypeNode::isTuple() const |
367 |
|
{ |
368 |
120352 |
return (getKind() == kind::DATATYPE_TYPE && getDType().isTuple()); |
369 |
|
} |
370 |
|
|
371 |
194 |
bool TypeNode::isRecord() const |
372 |
|
{ |
373 |
194 |
return (getKind() == kind::DATATYPE_TYPE && getDType().isRecord()); |
374 |
|
} |
375 |
|
|
376 |
36130 |
size_t TypeNode::getTupleLength() const { |
377 |
36130 |
Assert(isTuple()); |
378 |
36130 |
const DType& dt = getDType(); |
379 |
36130 |
Assert(dt.getNumConstructors() == 1); |
380 |
36130 |
return dt[0].getNumArgs(); |
381 |
|
} |
382 |
|
|
383 |
15747 |
vector<TypeNode> TypeNode::getTupleTypes() const { |
384 |
15747 |
Assert(isTuple()); |
385 |
15747 |
const DType& dt = getDType(); |
386 |
15747 |
Assert(dt.getNumConstructors() == 1); |
387 |
15747 |
vector<TypeNode> types; |
388 |
47356 |
for(unsigned i = 0; i < dt[0].getNumArgs(); ++i) { |
389 |
31609 |
types.push_back(dt[0][i].getRangeType()); |
390 |
|
} |
391 |
15747 |
return types; |
392 |
|
} |
393 |
|
|
394 |
|
/** Is this an instantiated datatype type */ |
395 |
1163 |
bool TypeNode::isInstantiatedDatatype() const { |
396 |
1163 |
if(getKind() == kind::DATATYPE_TYPE) { |
397 |
629 |
return true; |
398 |
|
} |
399 |
534 |
if(getKind() != kind::PARAMETRIC_DATATYPE) { |
400 |
|
return false; |
401 |
|
} |
402 |
534 |
const DType& dt = (*this)[0].getDType(); |
403 |
534 |
unsigned n = dt.getNumParameters(); |
404 |
534 |
Assert(n < getNumChildren()); |
405 |
1260 |
for(unsigned i = 0; i < n; ++i) { |
406 |
726 |
if (dt.getParameter(i) == (*this)[i + 1]) |
407 |
|
{ |
408 |
|
return false; |
409 |
|
} |
410 |
|
} |
411 |
534 |
return true; |
412 |
|
} |
413 |
|
|
414 |
1619 |
TypeNode TypeNode::instantiateParametricDatatype( |
415 |
|
const std::vector<TypeNode>& params) const |
416 |
|
{ |
417 |
1619 |
AssertArgument(getKind() == kind::PARAMETRIC_DATATYPE, *this); |
418 |
1619 |
AssertArgument(params.size() == getNumChildren() - 1, *this); |
419 |
1619 |
NodeManager* nm = NodeManager::currentNM(); |
420 |
3238 |
TypeNode cons = nm->mkTypeConst((*this)[0].getConst<DatatypeIndexConstant>()); |
421 |
3238 |
std::vector<TypeNode> paramsNodes; |
422 |
1619 |
paramsNodes.push_back(cons); |
423 |
3636 |
for (const TypeNode& t : params) |
424 |
|
{ |
425 |
2017 |
paramsNodes.push_back(t); |
426 |
|
} |
427 |
3238 |
return nm->mkTypeNode(kind::PARAMETRIC_DATATYPE, paramsNodes); |
428 |
|
} |
429 |
|
|
430 |
54 |
uint64_t TypeNode::getSortConstructorArity() const |
431 |
|
{ |
432 |
54 |
Assert(isSortConstructor() && hasAttribute(expr::SortArityAttr())); |
433 |
54 |
return getAttribute(expr::SortArityAttr()); |
434 |
|
} |
435 |
|
|
436 |
4 |
std::string TypeNode::getName() const |
437 |
|
{ |
438 |
4 |
Assert(isSort() || isSortConstructor()); |
439 |
4 |
return getAttribute(expr::VarNameAttr()); |
440 |
|
} |
441 |
|
|
442 |
50 |
TypeNode TypeNode::instantiateSortConstructor( |
443 |
|
const std::vector<TypeNode>& params) const |
444 |
|
{ |
445 |
50 |
Assert(isSortConstructor()); |
446 |
50 |
return NodeManager::currentNM()->mkSort(*this, params); |
447 |
|
} |
448 |
|
|
449 |
|
/** Is this an instantiated datatype parameter */ |
450 |
2383 |
bool TypeNode::isParameterInstantiatedDatatype(unsigned n) const { |
451 |
2383 |
AssertArgument(getKind() == kind::PARAMETRIC_DATATYPE, *this); |
452 |
2383 |
const DType& dt = (*this)[0].getDType(); |
453 |
2383 |
AssertArgument(n < dt.getNumParameters(), *this); |
454 |
2383 |
return dt.getParameter(n) != (*this)[n + 1]; |
455 |
|
} |
456 |
|
|
457 |
6108533 |
TypeNode TypeNode::leastCommonTypeNode(TypeNode t0, TypeNode t1){ |
458 |
6108533 |
return commonTypeNode( t0, t1, true ); |
459 |
|
} |
460 |
|
|
461 |
139681 |
TypeNode TypeNode::mostCommonTypeNode(TypeNode t0, TypeNode t1){ |
462 |
139681 |
return commonTypeNode( t0, t1, false ); |
463 |
|
} |
464 |
|
|
465 |
6248239 |
TypeNode TypeNode::commonTypeNode(TypeNode t0, TypeNode t1, bool isLeast) { |
466 |
6248239 |
Assert(NodeManager::currentNM() != NULL) |
467 |
|
<< "There is no current cvc5::NodeManager associated to this thread.\n" |
468 |
|
"Perhaps a public-facing function is missing a NodeManagerScope ?"; |
469 |
|
|
470 |
6248239 |
Assert(!t0.isNull()); |
471 |
6248239 |
Assert(!t1.isNull()); |
472 |
|
|
473 |
6248239 |
if(__builtin_expect( (t0 == t1), true )) { |
474 |
6200608 |
return t0; |
475 |
|
} |
476 |
|
|
477 |
|
// t0 != t1 && |
478 |
47631 |
if(t0.getKind() == kind::TYPE_CONSTANT) { |
479 |
47576 |
switch(t0.getConst<TypeConstant>()) { |
480 |
13916 |
case INTEGER_TYPE: |
481 |
13916 |
if(t1.isInteger()) { |
482 |
|
// t0 == IntegerType && t1.isInteger() |
483 |
|
return t0; //IntegerType |
484 |
13916 |
} else if(t1.isReal()) { |
485 |
|
// t0 == IntegerType && t1.isReal() && !t1.isInteger() |
486 |
13884 |
return isLeast ? t1 : t0; // RealType |
487 |
|
} else { |
488 |
32 |
return TypeNode(); // null type |
489 |
|
} |
490 |
33600 |
case REAL_TYPE: |
491 |
33600 |
if(t1.isReal()) { |
492 |
33600 |
return isLeast ? t0 : t1; // RealType |
493 |
|
} else { |
494 |
|
return TypeNode(); // null type |
495 |
|
} |
496 |
60 |
default: |
497 |
60 |
return TypeNode(); // null type |
498 |
|
} |
499 |
55 |
} else if(t1.getKind() == kind::TYPE_CONSTANT) { |
500 |
22 |
return commonTypeNode(t1, t0, isLeast); // decrease the number of special cases |
501 |
|
} |
502 |
|
|
503 |
|
// t0 != t1 && |
504 |
|
// t0.getKind() == kind::TYPE_CONSTANT && |
505 |
|
// t1.getKind() == kind::TYPE_CONSTANT |
506 |
33 |
switch(t0.getKind()) { |
507 |
9 |
case kind::FUNCTION_TYPE: |
508 |
|
{ |
509 |
9 |
if (t1.getKind() != kind::FUNCTION_TYPE) |
510 |
|
{ |
511 |
4 |
return TypeNode(); |
512 |
|
} |
513 |
|
// must have equal arguments |
514 |
10 |
std::vector<TypeNode> t0a = t0.getArgTypes(); |
515 |
10 |
std::vector<TypeNode> t1a = t1.getArgTypes(); |
516 |
5 |
if (t0a.size() != t1a.size()) |
517 |
|
{ |
518 |
|
// different arities |
519 |
|
return TypeNode(); |
520 |
|
} |
521 |
8 |
for (unsigned i = 0, nargs = t0a.size(); i < nargs; i++) |
522 |
|
{ |
523 |
5 |
if (t0a[i] != t1a[i]) |
524 |
|
{ |
525 |
|
// an argument is different |
526 |
2 |
return TypeNode(); |
527 |
|
} |
528 |
|
} |
529 |
6 |
TypeNode t0r = t0.getRangeType(); |
530 |
6 |
TypeNode t1r = t1.getRangeType(); |
531 |
6 |
TypeNode tr = commonTypeNode(t0r, t1r, isLeast); |
532 |
6 |
std::vector<TypeNode> ftypes; |
533 |
3 |
ftypes.insert(ftypes.end(), t0a.begin(), t0a.end()); |
534 |
3 |
ftypes.push_back(tr); |
535 |
3 |
return NodeManager::currentNM()->mkFunctionType(ftypes); |
536 |
|
} |
537 |
|
break; |
538 |
24 |
case kind::BITVECTOR_TYPE: |
539 |
|
case kind::FLOATINGPOINT_TYPE: |
540 |
|
case kind::SORT_TYPE: |
541 |
|
case kind::CONSTRUCTOR_TYPE: |
542 |
|
case kind::SELECTOR_TYPE: |
543 |
|
case kind::TESTER_TYPE: |
544 |
|
case kind::ARRAY_TYPE: |
545 |
|
case kind::DATATYPE_TYPE: |
546 |
|
case kind::PARAMETRIC_DATATYPE: |
547 |
|
case kind::SEQUENCE_TYPE: |
548 |
|
case kind::SET_TYPE: |
549 |
|
case kind::BAG_TYPE: |
550 |
|
{ |
551 |
|
// we don't support subtyping except for built in types Int and Real. |
552 |
24 |
return TypeNode(); // return null type |
553 |
|
} |
554 |
|
default: |
555 |
|
Unimplemented() << "don't have a commonType for types `" << t0 |
556 |
|
<< "' and `" << t1 << "'"; |
557 |
|
} |
558 |
|
} |
559 |
|
|
560 |
|
Node TypeNode::getEnsureTypeCondition( Node n, TypeNode tn ) { |
561 |
|
TypeNode ntn = n.getType(); |
562 |
|
Assert(ntn.isComparableTo(tn)); |
563 |
|
if( !ntn.isSubtypeOf( tn ) ){ |
564 |
|
if( tn.isInteger() ){ |
565 |
|
if( tn.isSubtypeOf( ntn ) ){ |
566 |
|
return NodeManager::currentNM()->mkNode( kind::IS_INTEGER, n ); |
567 |
|
} |
568 |
|
}else if( tn.isDatatype() && ntn.isDatatype() ){ |
569 |
|
if( tn.isTuple() && ntn.isTuple() ){ |
570 |
|
const DType& dt1 = tn.getDType(); |
571 |
|
const DType& dt2 = ntn.getDType(); |
572 |
|
NodeManager* nm = NodeManager::currentNM(); |
573 |
|
if( dt1[0].getNumArgs()==dt2[0].getNumArgs() ){ |
574 |
|
std::vector< Node > conds; |
575 |
|
for( unsigned i=0; i<dt2[0].getNumArgs(); i++ ){ |
576 |
|
Node s = nm->mkNode( |
577 |
|
kind::APPLY_SELECTOR_TOTAL, dt2[0][i].getSelector(), n); |
578 |
|
Node etc = getEnsureTypeCondition(s, dt1[0][i].getRangeType()); |
579 |
|
if( etc.isNull() ){ |
580 |
|
return Node::null(); |
581 |
|
}else{ |
582 |
|
conds.push_back( etc ); |
583 |
|
} |
584 |
|
} |
585 |
|
if( conds.empty() ){ |
586 |
|
return nm->mkConst(true); |
587 |
|
}else if( conds.size()==1 ){ |
588 |
|
return conds[0]; |
589 |
|
}else{ |
590 |
|
return nm->mkNode(kind::AND, conds); |
591 |
|
} |
592 |
|
} |
593 |
|
} |
594 |
|
} |
595 |
|
return Node::null(); |
596 |
|
}else{ |
597 |
|
return NodeManager::currentNM()->mkConst( true ); |
598 |
|
} |
599 |
|
} |
600 |
|
|
601 |
|
/** Is this a sort kind */ |
602 |
1821451 |
bool TypeNode::isSort() const { |
603 |
1821451 |
return ( getKind() == kind::SORT_TYPE && !hasAttribute(expr::SortArityAttr()) ); |
604 |
|
} |
605 |
|
|
606 |
|
/** Is this a sort constructor kind */ |
607 |
1461 |
bool TypeNode::isSortConstructor() const { |
608 |
1461 |
return getKind() == kind::SORT_TYPE && hasAttribute(expr::SortArityAttr()); |
609 |
|
} |
610 |
|
|
611 |
81141 |
bool TypeNode::isFloatingPoint() const |
612 |
|
{ |
613 |
81141 |
return getKind() == kind::FLOATINGPOINT_TYPE; |
614 |
|
} |
615 |
|
|
616 |
11399509 |
bool TypeNode::isBitVector() const { return getKind() == kind::BITVECTOR_TYPE; } |
617 |
|
|
618 |
7341213 |
bool TypeNode::isDatatype() const |
619 |
|
{ |
620 |
7341213 |
return getKind() == kind::DATATYPE_TYPE |
621 |
7341213 |
|| getKind() == kind::PARAMETRIC_DATATYPE; |
622 |
|
} |
623 |
|
|
624 |
1002376 |
bool TypeNode::isParametricDatatype() const |
625 |
|
{ |
626 |
1002376 |
return getKind() == kind::PARAMETRIC_DATATYPE; |
627 |
|
} |
628 |
|
|
629 |
6880917 |
bool TypeNode::isConstructor() const |
630 |
|
{ |
631 |
6880917 |
return getKind() == kind::CONSTRUCTOR_TYPE; |
632 |
|
} |
633 |
|
|
634 |
1493536 |
bool TypeNode::isSelector() const { return getKind() == kind::SELECTOR_TYPE; } |
635 |
|
|
636 |
1678342 |
bool TypeNode::isTester() const { return getKind() == kind::TESTER_TYPE; } |
637 |
|
|
638 |
70 |
bool TypeNode::isUpdater() const { return getKind() == kind::UPDATER_TYPE; } |
639 |
|
|
640 |
576632 |
bool TypeNode::isCodatatype() const |
641 |
|
{ |
642 |
576632 |
if (isDatatype()) |
643 |
|
{ |
644 |
575279 |
return getDType().isCodatatype(); |
645 |
|
} |
646 |
1353 |
return false; |
647 |
|
} |
648 |
|
|
649 |
4068 |
bool TypeNode::isSygusDatatype() const |
650 |
|
{ |
651 |
4068 |
if (isDatatype()) |
652 |
|
{ |
653 |
3612 |
return getDType().isSygus(); |
654 |
|
} |
655 |
456 |
return false; |
656 |
|
} |
657 |
|
|
658 |
3397 |
std::string TypeNode::toString() const { |
659 |
6794 |
std::stringstream ss; |
660 |
3397 |
OutputLanguage outlang = (this == &s_null) ? language::output::LANG_AUTO : options::outputLanguage(); |
661 |
3397 |
d_nv->toStream(ss, -1, 0, outlang); |
662 |
6794 |
return ss.str(); |
663 |
|
} |
664 |
|
|
665 |
4586729 |
const DType& TypeNode::getDType() const |
666 |
|
{ |
667 |
4586729 |
if (getKind() == kind::DATATYPE_TYPE) |
668 |
|
{ |
669 |
4565901 |
DatatypeIndexConstant dic = getConst<DatatypeIndexConstant>(); |
670 |
4565901 |
return NodeManager::currentNM()->getDTypeForIndex(dic.getIndex()); |
671 |
|
} |
672 |
20828 |
Assert(getKind() == kind::PARAMETRIC_DATATYPE); |
673 |
20828 |
return (*this)[0].getDType(); |
674 |
|
} |
675 |
|
|
676 |
38923 |
bool TypeNode::isBag() const |
677 |
|
{ |
678 |
38923 |
return getKind() == kind::BAG_TYPE; |
679 |
|
} |
680 |
|
|
681 |
3238 |
TypeNode TypeNode::getBagElementType() const |
682 |
|
{ |
683 |
3238 |
Assert(isBag()); |
684 |
3238 |
return (*this)[0]; |
685 |
|
} |
686 |
|
|
687 |
|
} // namespace cvc5 |
688 |
|
|
689 |
|
namespace std { |
690 |
|
|
691 |
3039545 |
size_t hash<cvc5::TypeNode>::operator()(const cvc5::TypeNode& tn) const |
692 |
|
{ |
693 |
3039545 |
return tn.getId(); |
694 |
|
} |
695 |
|
|
696 |
28194 |
} // namespace std |