1 /********************* */
2 /*! \file type_node.cpp
4 ** Original author: dejan
5 ** Major contributors: mdeters
6 ** Minor contributors (to current version): taking, ajreynol
7 ** This file is part of the CVC4 prototype.
8 ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
9 ** Courant Institute of Mathematical Sciences
10 ** New York University
11 ** See the file COPYING in the top-level source directory for licensing
12 ** information.\endverbatim
14 ** \brief Reference-counted encapsulation of a pointer to node information.
16 ** Reference-counted encapsulation of a pointer to node information.
21 #include "expr/type_node.h"
22 #include "expr/type_properties.h"
28 TypeNode
TypeNode::s_null( &expr::NodeValue::s_null
);
30 TypeNode
TypeNode::substitute(const TypeNode
& type
,
31 const TypeNode
& replacement
,
32 std::hash_map
<TypeNode
, TypeNode
, HashFunction
>& cache
) const {
34 std::hash_map
<TypeNode
, TypeNode
, HashFunction
>::const_iterator i
= cache
.find(*this);
35 if(i
!= cache
.end()) {
40 NodeBuilder
<> nb(getKind());
41 if(getMetaKind() == kind::metakind::PARAMETERIZED
) {
43 nb
<< TypeNode(d_nv
->d_children
[0]);
45 for(TypeNode::const_iterator i
= begin(),
52 (*i
).substitute(type
, replacement
);
57 TypeNode tn
= nb
.constructTypeNode();
62 Cardinality
TypeNode::getCardinality() const {
63 return kind::getCardinality(*this);
66 bool TypeNode::isWellFounded() const {
67 return kind::isWellFounded(*this);
70 Node
TypeNode::mkGroundTerm() const {
71 return kind::mkGroundTerm(*this);
74 bool TypeNode::isBoolean() const {
75 return getKind() == kind::TYPE_CONSTANT
&&
76 ( getConst
<TypeConstant
>() == BOOLEAN_TYPE
||
77 getConst
<TypeConstant
>() == PSEUDOBOOLEAN_TYPE
);
80 bool TypeNode::isInteger() const {
81 return getKind() == kind::TYPE_CONSTANT
&&
82 ( getConst
<TypeConstant
>() == INTEGER_TYPE
||
83 getConst
<TypeConstant
>() == PSEUDOBOOLEAN_TYPE
);
86 bool TypeNode::isReal() const {
87 return getKind() == kind::TYPE_CONSTANT
&&
88 ( getConst
<TypeConstant
>() == REAL_TYPE
||
89 getConst
<TypeConstant
>() == INTEGER_TYPE
||
90 getConst
<TypeConstant
>() == PSEUDOBOOLEAN_TYPE
);
93 bool TypeNode::isPseudoboolean() const {
94 return getKind() == kind::TYPE_CONSTANT
&&
95 getConst
<TypeConstant
>() == PSEUDOBOOLEAN_TYPE
;
98 bool TypeNode::isString() const {
99 return getKind() == kind::TYPE_CONSTANT
&&
100 getConst
<TypeConstant
>() == STRING_TYPE
;
103 bool TypeNode::isArray() const {
104 return getKind() == kind::ARRAY_TYPE
;
107 TypeNode
TypeNode::getArrayIndexType() const {
112 TypeNode
TypeNode::getArrayConstituentType() const {
117 TypeNode
TypeNode::getConstructorRangeType() const {
118 Assert(isConstructor());
119 return (*this)[getNumChildren()-1];
122 bool TypeNode::isFunction() const {
123 return getKind() == kind::FUNCTION_TYPE
;
126 bool TypeNode::isFunctionLike() const {
128 getKind() == kind::FUNCTION_TYPE
||
129 getKind() == kind::CONSTRUCTOR_TYPE
||
130 getKind() == kind::SELECTOR_TYPE
||
131 getKind() == kind::TESTER_TYPE
;
134 bool TypeNode::isPredicate() const {
135 return isFunction() && getRangeType().isBoolean();
138 std::vector
<TypeNode
> TypeNode::getArgTypes() const {
139 vector
<TypeNode
> args
;
141 Assert(getNumChildren() == 1);
142 args
.push_back((*this)[0]);
144 Assert(isFunction() || isConstructor() || isSelector());
145 for(unsigned i
= 0, i_end
= getNumChildren() - 1; i
< i_end
; ++i
) {
146 args
.push_back((*this)[i
]);
152 std::vector
<TypeNode
> TypeNode::getParamTypes() const {
153 vector
<TypeNode
> params
;
154 Assert(isParametricDatatype());
155 for(unsigned i
= 1, i_end
= getNumChildren(); i
< i_end
; ++i
) {
156 params
.push_back((*this)[i
]);
161 TypeNode
TypeNode::getRangeType() const {
163 return NodeManager::currentNM()->booleanType();
165 Assert(isFunction() || isConstructor() || isSelector());
166 return (*this)[getNumChildren()-1];
169 /** Is this a tuple type? */
170 bool TypeNode::isTuple() const {
171 return getKind() == kind::TUPLE_TYPE
;
174 /** Is this a tuple type? */
175 vector
<TypeNode
> TypeNode::getTupleTypes() const {
177 vector
<TypeNode
> types
;
178 for(unsigned i
= 0, i_end
= getNumChildren(); i
< i_end
; ++i
) {
179 types
.push_back((*this)[i
]);
184 /** Is this a sort kind */
185 bool TypeNode::isSort() const {
186 return getKind() == kind::SORT_TYPE
&& !hasAttribute(expr::SortArityAttr());
189 /** Is this a sort constructor kind */
190 bool TypeNode::isSortConstructor() const {
191 return getKind() == kind::SORT_TYPE
&& hasAttribute(expr::SortArityAttr());
194 /** Is this a kind type (i.e., the type of a type)? */
195 bool TypeNode::isKind() const {
196 return getKind() == kind::TYPE_CONSTANT
&&
197 getConst
<TypeConstant
>() == KIND_TYPE
;
200 /** Is this a bit-vector type */
201 bool TypeNode::isBitVector() const {
202 return getKind() == kind::BITVECTOR_TYPE
;
205 /** Is this a datatype type */
206 bool TypeNode::isDatatype() const {
207 return getKind() == kind::DATATYPE_TYPE
;
210 /** Is this a parametric datatype type */
211 bool TypeNode::isParametricDatatype() const {
212 return getKind() == kind::PARAMETRIC_DATATYPE
;
215 /** Is this an instantiated datatype type */
216 bool TypeNode::isInstantiatedDatatype() const {
217 if(getKind() == kind::DATATYPE_TYPE
) {
220 if(getKind() != kind::PARAMETRIC_DATATYPE
) {
223 const Datatype
& dt
= (*this)[0].getConst
<Datatype
>();
224 unsigned n
= dt
.getNumParameters();
225 Assert(n
< getNumChildren());
226 for(unsigned i
= 0; i
< n
; ++i
) {
227 if(TypeNode::fromType(dt
.getParameter(i
)) == (*this)[i
+ 1]) {
234 /** Is this an instantiated datatype parameter */
235 bool TypeNode::isParameterInstantiatedDatatype(unsigned n
) const {
236 AssertArgument(getKind() == kind::PARAMETRIC_DATATYPE
, *this);
237 const Datatype
& dt
= (*this)[0].getConst
<Datatype
>();
238 AssertArgument(n
< dt
.getNumParameters(), *this);
239 return TypeNode::fromType(dt
.getParameter(n
)) != (*this)[n
+ 1];
242 /** Is this a constructor type */
243 bool TypeNode::isConstructor() const {
244 return getKind() == kind::CONSTRUCTOR_TYPE
;
247 /** Is this a selector type */
248 bool TypeNode::isSelector() const {
249 return getKind() == kind::SELECTOR_TYPE
;
252 /** Is this a tester type */
253 bool TypeNode::isTester() const {
254 return getKind() == kind::TESTER_TYPE
;
257 /** Is this a bit-vector type of size <code>size</code> */
258 bool TypeNode::isBitVector(unsigned size
) const {
259 return getKind() == kind::BITVECTOR_TYPE
&&
260 getConst
<BitVectorSize
>() == size
;
263 /** Get the size of this bit-vector type */
264 unsigned TypeNode::getBitVectorSize() const {
265 Assert(isBitVector());
266 return getConst
<BitVectorSize
>();
269 }/* CVC4 namespace */