e7775cf7f88dcb3d1abb970822c7cced0bcecb1b
1 /********************* */
2 /*! \file type_node.cpp
4 ** Top contributors (to current version):
5 ** Morgan Deters, Andrew Reynolds, Kshitij Bansal
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2017 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.\endverbatim
12 ** \brief Reference-counted encapsulation of a pointer to node information.
14 ** Reference-counted encapsulation of a pointer to node information.
16 #include "expr/type_node.h"
20 #include "expr/node_manager_attributes.h"
21 #include "expr/type_properties.h"
22 #include "options/base_options.h"
23 #include "options/expr_options.h"
24 #include "options/quantifiers_options.h"
25 #include "options/uf_options.h"
31 TypeNode
TypeNode::s_null( &expr::NodeValue::null() );
33 TypeNode
TypeNode::substitute(const TypeNode
& type
,
34 const TypeNode
& replacement
,
35 std::unordered_map
<TypeNode
, TypeNode
, HashFunction
>& cache
) const {
37 std::unordered_map
<TypeNode
, TypeNode
, HashFunction
>::const_iterator i
= cache
.find(*this);
38 if(i
!= cache
.end()) {
43 NodeBuilder
<> nb(getKind());
44 if(getMetaKind() == kind::metakind::PARAMETERIZED
) {
46 nb
<< TypeNode(d_nv
->d_children
[0]);
48 for(TypeNode::const_iterator i
= begin(),
55 (*i
).substitute(type
, replacement
);
60 TypeNode tn
= nb
.constructTypeNode();
65 Cardinality
TypeNode::getCardinality() const {
66 return kind::getCardinality(*this);
69 bool TypeNode::isInterpretedFinite() const {
70 if( getCardinality().isFinite() ){
73 if( options::finiteModelFind() ){
76 }else if( isDatatype() ){
78 const Datatype
& dt
= getDatatype();
79 return dt
.isInterpretedFinite( tn
.toType() );
80 }else if( isArray() ){
81 return getArrayIndexType().isInterpretedFinite() && getArrayConstituentType().isInterpretedFinite();
83 return getSetElementType().isInterpretedFinite();
85 else if (isFunction())
87 if (!getRangeType().isInterpretedFinite())
91 std::vector
<TypeNode
> argTypes
= getArgTypes();
92 for (unsigned i
= 0, nargs
= argTypes
.size(); i
< nargs
; i
++)
94 if (!argTypes
[i
].isInterpretedFinite())
106 bool TypeNode::isFirstClass() const {
107 return ( getKind() != kind::FUNCTION_TYPE
|| options::ufHo() ) &&
108 getKind() != kind::CONSTRUCTOR_TYPE
&&
109 getKind() != kind::SELECTOR_TYPE
&&
110 getKind() != kind::TESTER_TYPE
&&
111 getKind() != kind::SEXPR_TYPE
&&
112 ( getKind() != kind::TYPE_CONSTANT
||
113 getConst
<TypeConstant
>() != REGEXP_TYPE
);
116 bool TypeNode::isWellFounded() const {
117 return kind::isWellFounded(*this);
120 Node
TypeNode::mkGroundTerm() const {
121 return kind::mkGroundTerm(*this);
124 bool TypeNode::isSubtypeOf(TypeNode t
) const {
128 if(getKind() == kind::TYPE_CONSTANT
) {
129 switch(getConst
<TypeConstant
>()) {
131 return t
.getKind() == kind::TYPE_CONSTANT
&& t
.getConst
<TypeConstant
>() == REAL_TYPE
;
136 if(isSet() && t
.isSet()) {
137 return getSetElementType().isSubtypeOf(t
.getSetElementType());
139 // this should only return true for types T1, T2 where we handle equalities between T1 and T2
140 // (more cases go here, if we want to support such cases)
144 bool TypeNode::isComparableTo(TypeNode t
) const {
148 if(isSubtypeOf(NodeManager::currentNM()->realType())) {
149 return t
.isSubtypeOf(NodeManager::currentNM()->realType());
151 if(isSet() && t
.isSet()) {
152 return getSetElementType().isComparableTo(t
.getSetElementType());
157 TypeNode
TypeNode::getBaseType() const {
158 TypeNode realt
= NodeManager::currentNM()->realType();
159 if (isSubtypeOf(realt
)) {
161 } else if (isParametricDatatype()) {
163 for(size_t i
= 1; i
< getNumChildren(); ++i
) {
164 v
.push_back((*this)[i
].getBaseType().toType());
166 TypeNode tn
= TypeNode::fromType((*this)[0].getDatatype().getDatatypeType(v
));
172 std::vector
<TypeNode
> TypeNode::getArgTypes() const {
173 vector
<TypeNode
> args
;
175 Assert(getNumChildren() == 1);
176 args
.push_back((*this)[0]);
178 Assert(isFunction() || isConstructor() || isSelector());
179 for(unsigned i
= 0, i_end
= getNumChildren() - 1; i
< i_end
; ++i
) {
180 args
.push_back((*this)[i
]);
186 std::vector
<TypeNode
> TypeNode::getParamTypes() const {
187 vector
<TypeNode
> params
;
188 Assert(isParametricDatatype());
189 for(unsigned i
= 1, i_end
= getNumChildren(); i
< i_end
; ++i
) {
190 params
.push_back((*this)[i
]);
196 /** Is this a tuple type? */
197 bool TypeNode::isTuple() const {
198 return ( getKind() == kind::DATATYPE_TYPE
&& getDatatype().isTuple() );
201 /** Is this a record type? */
202 bool TypeNode::isRecord() const {
203 return ( getKind() == kind::DATATYPE_TYPE
&& getDatatype().isRecord() );
206 size_t TypeNode::getTupleLength() const {
208 const Datatype
& dt
= getDatatype();
209 Assert(dt
.getNumConstructors()==1);
210 return dt
[0].getNumArgs();
213 vector
<TypeNode
> TypeNode::getTupleTypes() const {
215 const Datatype
& dt
= getDatatype();
216 Assert(dt
.getNumConstructors()==1);
217 vector
<TypeNode
> types
;
218 for(unsigned i
= 0; i
< dt
[0].getNumArgs(); ++i
) {
219 types
.push_back(TypeNode::fromType(dt
[0][i
].getRangeType()));
224 const Record
& TypeNode::getRecord() const {
226 const Datatype
& dt
= getDatatype();
227 return *(dt
.getRecord());
228 //return getAttribute(expr::DatatypeRecordAttr()).getConst<Record>();
231 vector
<TypeNode
> TypeNode::getSExprTypes() const {
233 vector
<TypeNode
> types
;
234 for(unsigned i
= 0, i_end
= getNumChildren(); i
< i_end
; ++i
) {
235 types
.push_back((*this)[i
]);
240 /** Is this an instantiated datatype type */
241 bool TypeNode::isInstantiatedDatatype() const {
242 if(getKind() == kind::DATATYPE_TYPE
) {
245 if(getKind() != kind::PARAMETRIC_DATATYPE
) {
248 const Datatype
& dt
= (*this)[0].getDatatype();
249 unsigned n
= dt
.getNumParameters();
250 Assert(n
< getNumChildren());
251 for(unsigned i
= 0; i
< n
; ++i
) {
252 if(TypeNode::fromType(dt
.getParameter(i
)) == (*this)[i
+ 1]) {
259 /** Is this an instantiated datatype parameter */
260 bool TypeNode::isParameterInstantiatedDatatype(unsigned n
) const {
261 AssertArgument(getKind() == kind::PARAMETRIC_DATATYPE
, *this);
262 const Datatype
& dt
= (*this)[0].getDatatype();
263 AssertArgument(n
< dt
.getNumParameters(), *this);
264 return TypeNode::fromType(dt
.getParameter(n
)) != (*this)[n
+ 1];
267 TypeNode
TypeNode::leastCommonTypeNode(TypeNode t0
, TypeNode t1
){
268 return commonTypeNode( t0
, t1
, true );
271 TypeNode
TypeNode::mostCommonTypeNode(TypeNode t0
, TypeNode t1
){
272 return commonTypeNode( t0
, t1
, false );
275 TypeNode
TypeNode::commonTypeNode(TypeNode t0
, TypeNode t1
, bool isLeast
) {
276 Assert( NodeManager::currentNM() != NULL
,
277 "There is no current CVC4::NodeManager associated to this thread.\n"
278 "Perhaps a public-facing function is missing a NodeManagerScope ?" );
280 Assert(!t0
.isNull());
281 Assert(!t1
.isNull());
283 if(__builtin_expect( (t0
== t1
), true )) {
288 if(t0
.getKind() == kind::TYPE_CONSTANT
) {
289 switch(t0
.getConst
<TypeConstant
>()) {
292 // t0 == IntegerType && t1.isInteger()
293 return t0
; //IntegerType
294 } else if(t1
.isReal()) {
295 // t0 == IntegerType && t1.isReal() && !t1.isInteger()
296 return isLeast
? t1
: t0
; // RealType
298 return TypeNode(); // null type
302 return isLeast
? t0
: t1
; // RealType
304 return TypeNode(); // null type
307 return TypeNode(); // null type
309 } else if(t1
.getKind() == kind::TYPE_CONSTANT
) {
310 return commonTypeNode(t1
, t0
, isLeast
); // decrease the number of special cases
314 // t0.getKind() == kind::TYPE_CONSTANT &&
315 // t1.getKind() == kind::TYPE_CONSTANT
316 switch(t0
.getKind()) {
317 case kind::BITVECTOR_TYPE
:
318 case kind::SORT_TYPE
:
319 case kind::CONSTRUCTOR_TYPE
:
320 case kind::SELECTOR_TYPE
:
321 case kind::TESTER_TYPE
:
322 case kind::FUNCTION_TYPE
:
323 case kind::ARRAY_TYPE
:
324 case kind::DATATYPE_TYPE
:
325 case kind::PARAMETRIC_DATATYPE
:
327 case kind::SET_TYPE
: {
328 // take the least common subtype of element types
329 TypeNode elementType
;
330 if(t1
.isSet() && !(elementType
= commonTypeNode(t0
[0], t1
[0], isLeast
)).isNull() ) {
331 return NodeManager::currentNM()->mkSetType(elementType
);
336 case kind::SEXPR_TYPE
:
337 Unimplemented("haven't implemented leastCommonType for symbolic expressions yet");
339 Unimplemented("don't have a commonType for types `%s' and `%s'", t0
.toString().c_str(), t1
.toString().c_str());
343 Node
TypeNode::getEnsureTypeCondition( Node n
, TypeNode tn
) {
344 TypeNode ntn
= n
.getType();
345 Assert( ntn
.isComparableTo( tn
) );
346 if( !ntn
.isSubtypeOf( tn
) ){
347 if( tn
.isInteger() ){
348 if( tn
.isSubtypeOf( ntn
) ){
349 return NodeManager::currentNM()->mkNode( kind::IS_INTEGER
, n
);
351 }else if( tn
.isDatatype() && ntn
.isDatatype() ){
352 if( tn
.isTuple() && ntn
.isTuple() ){
353 const Datatype
& dt1
= tn
.getDatatype();
354 const Datatype
& dt2
= ntn
.getDatatype();
355 if( dt1
[0].getNumArgs()==dt2
[0].getNumArgs() ){
356 std::vector
< Node
> conds
;
357 for( unsigned i
=0; i
<dt2
[0].getNumArgs(); i
++ ){
358 Node s
= NodeManager::currentNM()->mkNode( kind::APPLY_SELECTOR_TOTAL
, Node::fromExpr( dt2
[0][i
].getSelector() ), n
);
359 Node etc
= getEnsureTypeCondition( s
, TypeNode::fromType( dt1
[0][i
].getRangeType() ) );
363 conds
.push_back( etc
);
367 return NodeManager::currentNM()->mkConst( true );
368 }else if( conds
.size()==1 ){
371 return NodeManager::currentNM()->mkNode( kind::AND
, conds
);
378 return NodeManager::currentNM()->mkConst( true );
382 /** Is this a sort kind */
383 bool TypeNode::isSort() const {
384 return ( getKind() == kind::SORT_TYPE
&& !hasAttribute(expr::SortArityAttr()) );
387 /** Is this a sort constructor kind */
388 bool TypeNode::isSortConstructor() const {
389 return getKind() == kind::SORT_TYPE
&& hasAttribute(expr::SortArityAttr());
392 std::string
TypeNode::toString() const {
393 std::stringstream ss
;
394 OutputLanguage outlang
= (this == &s_null
) ? language::output::LANG_AUTO
: options::outputLanguage();
395 d_nv
->toStream(ss
, -1, false, 0, outlang
);
400 }/* CVC4 namespace */