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 |
9859 |
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 |
16805 |
Cardinality TypeNode::getCardinality() const { |
71 |
16805 |
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 |
7658641 |
CardinalityClass TypeNode::getCardinalityClass() |
82 |
|
{ |
83 |
|
// check it is already cached |
84 |
7658641 |
if (hasAttribute(TypeCardinalityClassAttr())) |
85 |
|
{ |
86 |
|
return static_cast<CardinalityClass>( |
87 |
7642619 |
getAttribute(TypeCardinalityClassAttr())); |
88 |
|
} |
89 |
16022 |
CardinalityClass ret = CardinalityClass::INFINITE; |
90 |
16022 |
if (isSort()) |
91 |
|
{ |
92 |
1908 |
ret = CardinalityClass::INTERPRETED_ONE; |
93 |
|
} |
94 |
42065 |
else if (isBoolean() || isBitVector() || isFloatingPoint() |
95 |
23241 |
|| isRoundingMode()) |
96 |
|
{ |
97 |
5015 |
ret = CardinalityClass::FINITE; |
98 |
|
} |
99 |
9099 |
else if (isString() || isRegExp() || isSequence() || isReal() || isBag()) |
100 |
|
{ |
101 |
4849 |
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 |
4250 |
setAttribute(TypeCardinalityClassAttr(), static_cast<uint64_t>(ret)); |
109 |
|
|
110 |
4250 |
if (isDatatype()) |
111 |
|
{ |
112 |
4598 |
TypeNode tn = *this; |
113 |
2299 |
const DType& dt = getDType(); |
114 |
2299 |
ret = dt.getCardinalityClass(tn); |
115 |
|
} |
116 |
1951 |
else if (isArray()) |
117 |
|
{ |
118 |
521 |
ret = getArrayConstituentType().getCardinalityClass(); |
119 |
521 |
if (ret == CardinalityClass::FINITE |
120 |
261 |
|| ret == CardinalityClass::INTERPRETED_FINITE) |
121 |
|
{ |
122 |
260 |
CardinalityClass cci = getArrayIndexType().getCardinalityClass(); |
123 |
|
// arrays with both finite element types, we take the max with its |
124 |
|
// index type. |
125 |
260 |
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 |
1430 |
else if (isSet()) |
131 |
|
{ |
132 |
942 |
CardinalityClass cc = getSetElementType().getCardinalityClass(); |
133 |
942 |
if (cc == CardinalityClass::ONE) |
134 |
|
{ |
135 |
|
// 1 -> 2 |
136 |
19 |
ret = CardinalityClass::FINITE; |
137 |
|
} |
138 |
923 |
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 |
923 |
ret = cc; |
147 |
|
} |
148 |
|
} |
149 |
488 |
else if (isFunction()) |
150 |
|
{ |
151 |
485 |
ret = getRangeType().getCardinalityClass(); |
152 |
485 |
if (ret == CardinalityClass::FINITE |
153 |
341 |
|| ret == CardinalityClass::INTERPRETED_FINITE) |
154 |
|
{ |
155 |
|
// we may have a larger cardinality class based on the |
156 |
|
// arguments of the function |
157 |
288 |
std::vector<TypeNode> argTypes = getArgTypes(); |
158 |
369 |
for (size_t i = 0, nargs = argTypes.size(); i < nargs; i++) |
159 |
|
{ |
160 |
225 |
CardinalityClass cca = argTypes[i].getCardinalityClass(); |
161 |
225 |
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 |
3 |
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 |
3 |
ret = CardinalityClass::ONE; |
175 |
|
// we may have a larger cardinality class based on the |
176 |
|
// arguments of the constructor |
177 |
6 |
std::vector<TypeNode> argTypes = getArgTypes(); |
178 |
7 |
for (size_t i = 0, nargs = argTypes.size(); i < nargs; i++) |
179 |
|
{ |
180 |
4 |
CardinalityClass cca = argTypes[i].getCardinalityClass(); |
181 |
4 |
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 |
16022 |
setAttribute(TypeCardinalityClassAttr(), static_cast<uint64_t>(ret)); |
191 |
16022 |
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 |
84946 |
bool TypeNode::isClosedEnumerable() |
206 |
|
{ |
207 |
|
// check it is already cached |
208 |
84946 |
if (!getAttribute(IsClosedEnumerableComputedAttr())) |
209 |
|
{ |
210 |
2331 |
bool ret = true; |
211 |
2331 |
if (isArray() || isSort() || isCodatatype() || isFunction() || isRegExp()) |
212 |
|
{ |
213 |
505 |
ret = false; |
214 |
|
} |
215 |
1826 |
else if (isSet()) |
216 |
|
{ |
217 |
9 |
ret = getSetElementType().isClosedEnumerable(); |
218 |
|
} |
219 |
1817 |
else if (isSequence()) |
220 |
|
{ |
221 |
|
ret = getSequenceElementType().isClosedEnumerable(); |
222 |
|
} |
223 |
1817 |
else if (isDatatype()) |
224 |
|
{ |
225 |
|
// avoid infinite loops: initially set to true |
226 |
418 |
setAttribute(IsClosedEnumerableAttr(), ret); |
227 |
418 |
setAttribute(IsClosedEnumerableComputedAttr(), true); |
228 |
836 |
TypeNode tn = *this; |
229 |
418 |
const DType& dt = getDType(); |
230 |
1021 |
for (uint32_t i = 0, ncons = dt.getNumConstructors(); i < ncons; i++) |
231 |
|
{ |
232 |
1424 |
for (uint32_t j = 0, nargs = dt[i].getNumArgs(); j < nargs; j++) |
233 |
|
{ |
234 |
1443 |
TypeNode ctn = dt[i][j].getRangeType(); |
235 |
821 |
if (tn != ctn && !ctn.isClosedEnumerable()) |
236 |
|
{ |
237 |
199 |
ret = false; |
238 |
199 |
break; |
239 |
|
} |
240 |
|
} |
241 |
802 |
if (!ret) |
242 |
|
{ |
243 |
199 |
break; |
244 |
|
} |
245 |
|
} |
246 |
|
} |
247 |
2331 |
setAttribute(IsClosedEnumerableAttr(), ret); |
248 |
2331 |
setAttribute(IsClosedEnumerableComputedAttr(), true); |
249 |
2331 |
return ret; |
250 |
|
} |
251 |
82615 |
return getAttribute(IsClosedEnumerableAttr()); |
252 |
|
} |
253 |
|
|
254 |
992270 |
bool TypeNode::isFirstClass() const |
255 |
|
{ |
256 |
1984540 |
return getKind() != kind::CONSTRUCTOR_TYPE && getKind() != kind::SELECTOR_TYPE |
257 |
992270 |
&& getKind() != kind::TESTER_TYPE && getKind() != kind::UPDATER_TYPE |
258 |
2974871 |
&& (getKind() != kind::TYPE_CONSTANT |
259 |
321054 |
|| (getConst<TypeConstant>() != REGEXP_TYPE |
260 |
1311385 |
&& getConst<TypeConstant>() != SEXPR_TYPE)); |
261 |
|
} |
262 |
|
|
263 |
|
bool TypeNode::isWellFounded() const { |
264 |
|
return kind::isWellFounded(*this); |
265 |
|
} |
266 |
|
|
267 |
116425 |
Node TypeNode::mkGroundTerm() const { |
268 |
116425 |
return kind::mkGroundTerm(*this); |
269 |
|
} |
270 |
|
|
271 |
117472 |
Node TypeNode::mkGroundValue() const |
272 |
|
{ |
273 |
234944 |
theory::TypeEnumerator te(*this); |
274 |
234944 |
return *te; |
275 |
|
} |
276 |
|
|
277 |
4852143 |
bool TypeNode::isStringLike() const { return isString() || isSequence(); } |
278 |
|
|
279 |
9536342 |
bool TypeNode::isSubtypeOf(TypeNode t) const { |
280 |
9536342 |
if(*this == t) { |
281 |
8935143 |
return true; |
282 |
|
} |
283 |
601199 |
if(getKind() == kind::TYPE_CONSTANT) { |
284 |
223425 |
switch(getConst<TypeConstant>()) { |
285 |
169546 |
case INTEGER_TYPE: |
286 |
169546 |
return t.getKind() == kind::TYPE_CONSTANT && t.getConst<TypeConstant>() == REAL_TYPE; |
287 |
53879 |
default: |
288 |
53879 |
return false; |
289 |
|
} |
290 |
|
} |
291 |
377774 |
if (isFunction() && t.isFunction()) |
292 |
|
{ |
293 |
3 |
if (!isComparableTo(t)) |
294 |
|
{ |
295 |
|
// incomparable, not subtype |
296 |
|
return false; |
297 |
|
} |
298 |
3 |
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 |
377771 |
return false; |
303 |
|
} |
304 |
|
|
305 |
6517601 |
bool TypeNode::isComparableTo(TypeNode t) const { |
306 |
6517601 |
if(*this == t) { |
307 |
6498724 |
return true; |
308 |
|
} |
309 |
18877 |
if(isSubtypeOf(NodeManager::currentNM()->realType())) { |
310 |
16637 |
return t.isSubtypeOf(NodeManager::currentNM()->realType()); |
311 |
|
} |
312 |
2240 |
if (isFunction() && t.isFunction()) |
313 |
|
{ |
314 |
|
// comparable if they have a common type node |
315 |
5 |
return !leastCommonTypeNode(*this, t).isNull(); |
316 |
|
} |
317 |
2235 |
return false; |
318 |
|
} |
319 |
|
|
320 |
40 |
TypeNode TypeNode::getTesterDomainType() const |
321 |
|
{ |
322 |
40 |
Assert(isTester()); |
323 |
40 |
return (*this)[0]; |
324 |
|
} |
325 |
|
|
326 |
7266 |
TypeNode TypeNode::getSequenceElementType() const |
327 |
|
{ |
328 |
7266 |
Assert(isSequence()); |
329 |
7266 |
return (*this)[0]; |
330 |
|
} |
331 |
|
|
332 |
584627 |
TypeNode TypeNode::getBaseType() const { |
333 |
1169254 |
TypeNode realt = NodeManager::currentNM()->realType(); |
334 |
584627 |
if (isSubtypeOf(realt)) { |
335 |
159753 |
return realt; |
336 |
424874 |
} 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 |
423951 |
return *this; |
344 |
|
} |
345 |
|
|
346 |
12368 |
std::vector<TypeNode> TypeNode::getArgTypes() const { |
347 |
12368 |
vector<TypeNode> args; |
348 |
12368 |
if(isTester()) { |
349 |
|
Assert(getNumChildren() == 1); |
350 |
|
args.push_back((*this)[0]); |
351 |
|
} else { |
352 |
12368 |
Assert(isFunction() || isConstructor() || isSelector()); |
353 |
33228 |
for(unsigned i = 0, i_end = getNumChildren() - 1; i < i_end; ++i) { |
354 |
20860 |
args.push_back((*this)[i]); |
355 |
|
} |
356 |
|
} |
357 |
12368 |
return args; |
358 |
|
} |
359 |
|
|
360 |
3604 |
std::vector<TypeNode> TypeNode::getParamTypes() const { |
361 |
3604 |
vector<TypeNode> params; |
362 |
3604 |
Assert(isParametricDatatype()); |
363 |
9251 |
for(unsigned i = 1, i_end = getNumChildren(); i < i_end; ++i) { |
364 |
5647 |
params.push_back((*this)[i]); |
365 |
|
} |
366 |
3604 |
return params; |
367 |
|
} |
368 |
|
|
369 |
120948 |
bool TypeNode::isTuple() const |
370 |
|
{ |
371 |
120948 |
return (getKind() == kind::DATATYPE_TYPE && getDType().isTuple()); |
372 |
|
} |
373 |
|
|
374 |
194 |
bool TypeNode::isRecord() const |
375 |
|
{ |
376 |
194 |
return (getKind() == kind::DATATYPE_TYPE && getDType().isRecord()); |
377 |
|
} |
378 |
|
|
379 |
36282 |
size_t TypeNode::getTupleLength() const { |
380 |
36282 |
Assert(isTuple()); |
381 |
36282 |
const DType& dt = getDType(); |
382 |
36282 |
Assert(dt.getNumConstructors() == 1); |
383 |
36282 |
return dt[0].getNumArgs(); |
384 |
|
} |
385 |
|
|
386 |
15664 |
vector<TypeNode> TypeNode::getTupleTypes() const { |
387 |
15664 |
Assert(isTuple()); |
388 |
15664 |
const DType& dt = getDType(); |
389 |
15664 |
Assert(dt.getNumConstructors() == 1); |
390 |
15664 |
vector<TypeNode> types; |
391 |
47175 |
for(unsigned i = 0; i < dt[0].getNumArgs(); ++i) { |
392 |
31511 |
types.push_back(dt[0][i].getRangeType()); |
393 |
|
} |
394 |
15664 |
return types; |
395 |
|
} |
396 |
|
|
397 |
|
/** Is this an instantiated datatype type */ |
398 |
1440 |
bool TypeNode::isInstantiatedDatatype() const { |
399 |
1440 |
if(getKind() == kind::DATATYPE_TYPE) { |
400 |
897 |
return true; |
401 |
|
} |
402 |
543 |
if(getKind() != kind::PARAMETRIC_DATATYPE) { |
403 |
|
return false; |
404 |
|
} |
405 |
543 |
const DType& dt = (*this)[0].getDType(); |
406 |
543 |
unsigned n = dt.getNumParameters(); |
407 |
543 |
Assert(n < getNumChildren()); |
408 |
1248 |
for(unsigned i = 0; i < n; ++i) { |
409 |
705 |
if (dt.getParameter(i) == (*this)[i + 1]) |
410 |
|
{ |
411 |
|
return false; |
412 |
|
} |
413 |
|
} |
414 |
543 |
return true; |
415 |
|
} |
416 |
|
|
417 |
1508 |
TypeNode TypeNode::instantiateParametricDatatype( |
418 |
|
const std::vector<TypeNode>& params) const |
419 |
|
{ |
420 |
1508 |
AssertArgument(getKind() == kind::PARAMETRIC_DATATYPE, *this); |
421 |
1508 |
AssertArgument(params.size() == getNumChildren() - 1, *this); |
422 |
1508 |
NodeManager* nm = NodeManager::currentNM(); |
423 |
3016 |
TypeNode cons = nm->mkTypeConst((*this)[0].getConst<DatatypeIndexConstant>()); |
424 |
3016 |
std::vector<TypeNode> paramsNodes; |
425 |
1508 |
paramsNodes.push_back(cons); |
426 |
3318 |
for (const TypeNode& t : params) |
427 |
|
{ |
428 |
1810 |
paramsNodes.push_back(t); |
429 |
|
} |
430 |
3016 |
return nm->mkTypeNode(kind::PARAMETRIC_DATATYPE, paramsNodes); |
431 |
|
} |
432 |
|
|
433 |
54 |
uint64_t TypeNode::getSortConstructorArity() const |
434 |
|
{ |
435 |
54 |
Assert(isSortConstructor() && hasAttribute(expr::SortArityAttr())); |
436 |
54 |
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 |
50 |
TypeNode TypeNode::instantiateSortConstructor( |
446 |
|
const std::vector<TypeNode>& params) const |
447 |
|
{ |
448 |
50 |
Assert(isSortConstructor()); |
449 |
50 |
return NodeManager::currentNM()->mkSort(*this, params); |
450 |
|
} |
451 |
|
|
452 |
|
/** Is this an instantiated datatype parameter */ |
453 |
5438 |
bool TypeNode::isParameterInstantiatedDatatype(unsigned n) const { |
454 |
5438 |
AssertArgument(getKind() == kind::PARAMETRIC_DATATYPE, *this); |
455 |
5438 |
const DType& dt = (*this)[0].getDType(); |
456 |
5438 |
AssertArgument(n < dt.getNumParameters(), *this); |
457 |
5438 |
return dt.getParameter(n) != (*this)[n + 1]; |
458 |
|
} |
459 |
|
|
460 |
6866839 |
TypeNode TypeNode::leastCommonTypeNode(TypeNode t0, TypeNode t1){ |
461 |
6866839 |
return commonTypeNode( t0, t1, true ); |
462 |
|
} |
463 |
|
|
464 |
141126 |
TypeNode TypeNode::mostCommonTypeNode(TypeNode t0, TypeNode t1){ |
465 |
141126 |
return commonTypeNode( t0, t1, false ); |
466 |
|
} |
467 |
|
|
468 |
7007993 |
TypeNode TypeNode::commonTypeNode(TypeNode t0, TypeNode t1, bool isLeast) { |
469 |
7007993 |
Assert(NodeManager::currentNM() != NULL) |
470 |
|
<< "There is no current cvc5::NodeManager associated to this thread.\n" |
471 |
|
"Perhaps a public-facing function is missing a NodeManagerScope ?"; |
472 |
|
|
473 |
7007993 |
Assert(!t0.isNull()); |
474 |
7007993 |
Assert(!t1.isNull()); |
475 |
|
|
476 |
7007993 |
if(__builtin_expect( (t0 == t1), true )) { |
477 |
6957231 |
return t0; |
478 |
|
} |
479 |
|
|
480 |
|
// t0 != t1 && |
481 |
50762 |
if(t0.getKind() == kind::TYPE_CONSTANT) { |
482 |
50704 |
switch(t0.getConst<TypeConstant>()) { |
483 |
15170 |
case INTEGER_TYPE: |
484 |
15170 |
if(t1.isInteger()) { |
485 |
|
// t0 == IntegerType && t1.isInteger() |
486 |
|
return t0; //IntegerType |
487 |
15170 |
} else if(t1.isReal()) { |
488 |
|
// t0 == IntegerType && t1.isReal() && !t1.isInteger() |
489 |
15138 |
return isLeast ? t1 : t0; // RealType |
490 |
|
} else { |
491 |
32 |
return TypeNode(); // null type |
492 |
|
} |
493 |
35474 |
case REAL_TYPE: |
494 |
35474 |
if(t1.isReal()) { |
495 |
35474 |
return isLeast ? t0 : t1; // RealType |
496 |
|
} else { |
497 |
|
return TypeNode(); // null type |
498 |
|
} |
499 |
60 |
default: |
500 |
60 |
return TypeNode(); // null type |
501 |
|
} |
502 |
58 |
} else if(t1.getKind() == kind::TYPE_CONSTANT) { |
503 |
22 |
return commonTypeNode(t1, t0, isLeast); // decrease the number of special cases |
504 |
|
} |
505 |
|
|
506 |
|
// t0 != t1 && |
507 |
|
// t0.getKind() == kind::TYPE_CONSTANT && |
508 |
|
// t1.getKind() == kind::TYPE_CONSTANT |
509 |
36 |
switch(t0.getKind()) { |
510 |
12 |
case kind::FUNCTION_TYPE: |
511 |
|
{ |
512 |
12 |
if (t1.getKind() != kind::FUNCTION_TYPE) |
513 |
|
{ |
514 |
4 |
return TypeNode(); |
515 |
|
} |
516 |
|
// must have equal arguments |
517 |
16 |
std::vector<TypeNode> t0a = t0.getArgTypes(); |
518 |
16 |
std::vector<TypeNode> t1a = t1.getArgTypes(); |
519 |
8 |
if (t0a.size() != t1a.size()) |
520 |
|
{ |
521 |
|
// different arities |
522 |
|
return TypeNode(); |
523 |
|
} |
524 |
15 |
for (unsigned i = 0, nargs = t0a.size(); i < nargs; i++) |
525 |
|
{ |
526 |
9 |
if (t0a[i] != t1a[i]) |
527 |
|
{ |
528 |
|
// an argument is different |
529 |
2 |
return TypeNode(); |
530 |
|
} |
531 |
|
} |
532 |
12 |
TypeNode t0r = t0.getRangeType(); |
533 |
12 |
TypeNode t1r = t1.getRangeType(); |
534 |
12 |
TypeNode tr = commonTypeNode(t0r, t1r, isLeast); |
535 |
12 |
std::vector<TypeNode> ftypes; |
536 |
6 |
ftypes.insert(ftypes.end(), t0a.begin(), t0a.end()); |
537 |
6 |
ftypes.push_back(tr); |
538 |
6 |
return NodeManager::currentNM()->mkFunctionType(ftypes); |
539 |
|
} |
540 |
|
break; |
541 |
24 |
case kind::BITVECTOR_TYPE: |
542 |
|
case kind::FLOATINGPOINT_TYPE: |
543 |
|
case kind::SORT_TYPE: |
544 |
|
case kind::CONSTRUCTOR_TYPE: |
545 |
|
case kind::SELECTOR_TYPE: |
546 |
|
case kind::TESTER_TYPE: |
547 |
|
case kind::ARRAY_TYPE: |
548 |
|
case kind::DATATYPE_TYPE: |
549 |
|
case kind::PARAMETRIC_DATATYPE: |
550 |
|
case kind::SEQUENCE_TYPE: |
551 |
|
case kind::SET_TYPE: |
552 |
|
case kind::BAG_TYPE: |
553 |
|
{ |
554 |
|
// we don't support subtyping except for built in types Int and Real. |
555 |
24 |
return TypeNode(); // return null type |
556 |
|
} |
557 |
|
default: |
558 |
|
Unimplemented() << "don't have a commonType for types `" << t0 |
559 |
|
<< "' and `" << t1 << "'"; |
560 |
|
} |
561 |
|
} |
562 |
|
|
563 |
|
Node TypeNode::getEnsureTypeCondition( Node n, TypeNode tn ) { |
564 |
|
TypeNode ntn = n.getType(); |
565 |
|
Assert(ntn.isComparableTo(tn)); |
566 |
|
if( !ntn.isSubtypeOf( tn ) ){ |
567 |
|
if( tn.isInteger() ){ |
568 |
|
if( tn.isSubtypeOf( ntn ) ){ |
569 |
|
return NodeManager::currentNM()->mkNode( kind::IS_INTEGER, n ); |
570 |
|
} |
571 |
|
}else if( tn.isDatatype() && ntn.isDatatype() ){ |
572 |
|
if( tn.isTuple() && ntn.isTuple() ){ |
573 |
|
const DType& dt1 = tn.getDType(); |
574 |
|
const DType& dt2 = ntn.getDType(); |
575 |
|
NodeManager* nm = NodeManager::currentNM(); |
576 |
|
if( dt1[0].getNumArgs()==dt2[0].getNumArgs() ){ |
577 |
|
std::vector< Node > conds; |
578 |
|
for( unsigned i=0; i<dt2[0].getNumArgs(); i++ ){ |
579 |
|
Node s = nm->mkNode( |
580 |
|
kind::APPLY_SELECTOR_TOTAL, dt2[0][i].getSelector(), n); |
581 |
|
Node etc = getEnsureTypeCondition(s, dt1[0][i].getRangeType()); |
582 |
|
if( etc.isNull() ){ |
583 |
|
return Node::null(); |
584 |
|
}else{ |
585 |
|
conds.push_back( etc ); |
586 |
|
} |
587 |
|
} |
588 |
|
if( conds.empty() ){ |
589 |
|
return nm->mkConst(true); |
590 |
|
}else if( conds.size()==1 ){ |
591 |
|
return conds[0]; |
592 |
|
}else{ |
593 |
|
return nm->mkNode(kind::AND, conds); |
594 |
|
} |
595 |
|
} |
596 |
|
} |
597 |
|
} |
598 |
|
return Node::null(); |
599 |
|
}else{ |
600 |
|
return NodeManager::currentNM()->mkConst( true ); |
601 |
|
} |
602 |
|
} |
603 |
|
|
604 |
|
/** Is this a sort kind */ |
605 |
1582343 |
bool TypeNode::isSort() const { |
606 |
1582343 |
return ( getKind() == kind::SORT_TYPE && !hasAttribute(expr::SortArityAttr()) ); |
607 |
|
} |
608 |
|
|
609 |
|
/** Is this a sort constructor kind */ |
610 |
1463 |
bool TypeNode::isSortConstructor() const { |
611 |
1463 |
return getKind() == kind::SORT_TYPE && hasAttribute(expr::SortArityAttr()); |
612 |
|
} |
613 |
|
|
614 |
125243 |
bool TypeNode::isFloatingPoint() const |
615 |
|
{ |
616 |
125243 |
return getKind() == kind::FLOATINGPOINT_TYPE; |
617 |
|
} |
618 |
|
|
619 |
7742113 |
bool TypeNode::isBitVector() const { return getKind() == kind::BITVECTOR_TYPE; } |
620 |
|
|
621 |
7413431 |
bool TypeNode::isDatatype() const |
622 |
|
{ |
623 |
7413431 |
return getKind() == kind::DATATYPE_TYPE |
624 |
7413431 |
|| getKind() == kind::PARAMETRIC_DATATYPE; |
625 |
|
} |
626 |
|
|
627 |
896530 |
bool TypeNode::isParametricDatatype() const |
628 |
|
{ |
629 |
896530 |
return getKind() == kind::PARAMETRIC_DATATYPE; |
630 |
|
} |
631 |
|
|
632 |
7560014 |
bool TypeNode::isConstructor() const |
633 |
|
{ |
634 |
7560014 |
return getKind() == kind::CONSTRUCTOR_TYPE; |
635 |
|
} |
636 |
|
|
637 |
1284219 |
bool TypeNode::isSelector() const { return getKind() == kind::SELECTOR_TYPE; } |
638 |
|
|
639 |
2130072 |
bool TypeNode::isTester() const { return getKind() == kind::TESTER_TYPE; } |
640 |
|
|
641 |
70 |
bool TypeNode::isUpdater() const { return getKind() == kind::UPDATER_TYPE; } |
642 |
|
|
643 |
500373 |
bool TypeNode::isCodatatype() const |
644 |
|
{ |
645 |
500373 |
if (isDatatype()) |
646 |
|
{ |
647 |
498961 |
return getDType().isCodatatype(); |
648 |
|
} |
649 |
1412 |
return false; |
650 |
|
} |
651 |
|
|
652 |
8542 |
bool TypeNode::isSygusDatatype() const |
653 |
|
{ |
654 |
8542 |
if (isDatatype()) |
655 |
|
{ |
656 |
8070 |
return getDType().isSygus(); |
657 |
|
} |
658 |
472 |
return false; |
659 |
|
} |
660 |
|
|
661 |
2039 |
std::string TypeNode::toString() const { |
662 |
4078 |
std::stringstream ss; |
663 |
|
Language outlang = |
664 |
2039 |
(this == &s_null) ? Language::LANG_AUTO : options::outputLanguage(); |
665 |
2039 |
d_nv->toStream(ss, -1, 0, outlang); |
666 |
4078 |
return ss.str(); |
667 |
|
} |
668 |
|
|
669 |
4360814 |
const DType& TypeNode::getDType() const |
670 |
|
{ |
671 |
4360814 |
if (getKind() == kind::DATATYPE_TYPE) |
672 |
|
{ |
673 |
4339178 |
DatatypeIndexConstant dic = getConst<DatatypeIndexConstant>(); |
674 |
4339178 |
return NodeManager::currentNM()->getDTypeForIndex(dic.getIndex()); |
675 |
|
} |
676 |
21636 |
Assert(getKind() == kind::PARAMETRIC_DATATYPE); |
677 |
21636 |
return (*this)[0].getDType(); |
678 |
|
} |
679 |
|
|
680 |
48969 |
bool TypeNode::isBag() const |
681 |
|
{ |
682 |
48969 |
return getKind() == kind::BAG_TYPE; |
683 |
|
} |
684 |
|
|
685 |
3517 |
TypeNode TypeNode::getBagElementType() const |
686 |
|
{ |
687 |
3517 |
Assert(isBag()); |
688 |
3517 |
return (*this)[0]; |
689 |
|
} |
690 |
|
|
691 |
1935 |
bool TypeNode::isBitVector(unsigned size) const |
692 |
|
{ |
693 |
1935 |
return (getKind() == kind::BITVECTOR_TYPE |
694 |
1935 |
&& getConst<BitVectorSize>() == size); |
695 |
|
} |
696 |
|
|
697 |
3553254 |
uint32_t TypeNode::getBitVectorSize() const |
698 |
|
{ |
699 |
3553254 |
Assert(isBitVector()); |
700 |
3553254 |
return getConst<BitVectorSize>(); |
701 |
|
} |
702 |
|
|
703 |
|
} // namespace cvc5 |
704 |
|
|
705 |
|
namespace std { |
706 |
|
|
707 |
2917565 |
size_t hash<cvc5::TypeNode>::operator()(const cvc5::TypeNode& tn) const |
708 |
|
{ |
709 |
2917565 |
return tn.getId(); |
710 |
|
} |
711 |
|
|
712 |
29577 |
} // namespace std |