1 /********************* */
4 ** Original author: cconway
5 ** Major contributors: dejan, mdeters
6 ** Minor contributors (to current version): 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 Implementation of expression types
16 ** Implementation of expression types.
23 #include "expr/node_manager.h"
24 #include "expr/type.h"
25 #include "expr/type_node.h"
26 #include "util/Assert.h"
32 ostream
& operator<<(ostream
& out
, const Type
& t
) {
33 NodeManagerScope
nms(t
.d_nodeManager
);
34 return out
<< *Type::getTypeNode(t
);
37 Type
Type::makeType(const TypeNode
& typeNode
) const {
38 return Type(d_nodeManager
, new TypeNode(typeNode
));
41 Type::Type(NodeManager
* nm
, TypeNode
* node
) :
47 NodeManagerScope
nms(d_nodeManager
);
52 d_typeNode(new TypeNode
),
56 Type::Type(const Type
& t
) :
57 d_typeNode(new TypeNode(*t
.d_typeNode
)),
58 d_nodeManager(t
.d_nodeManager
) {
61 bool Type::isNull() const {
62 return d_typeNode
->isNull();
65 Cardinality
Type::getCardinality() const {
66 NodeManagerScope
nms(d_nodeManager
);
67 return d_typeNode
->getCardinality();
70 bool Type::isWellFounded() const {
71 NodeManagerScope
nms(d_nodeManager
);
72 return d_typeNode
->isWellFounded();
75 Expr
Type::mkGroundTerm() const {
76 NodeManagerScope
nms(d_nodeManager
);
77 return d_typeNode
->mkGroundTerm().toExpr();
80 Type
& Type::operator=(const Type
& t
) {
81 Assert(d_typeNode
!= NULL
, "Unexpected NULL typenode pointer!");
82 Assert(t
.d_typeNode
!= NULL
, "Unexpected NULL typenode pointer!");
85 if(d_nodeManager
== t
.d_nodeManager
) {
86 NodeManagerScope
nms(d_nodeManager
);
87 *d_typeNode
= *t
.d_typeNode
;
89 // This happens more than you think---every time you set to or
90 // from the null Type. It's tricky because each node manager
91 // must be in play at the right time.
93 NodeManagerScope
nms1(d_nodeManager
);
94 *d_typeNode
= TypeNode::null();
96 NodeManagerScope
nms2(t
.d_nodeManager
);
97 *d_typeNode
= *t
.d_typeNode
;
99 d_nodeManager
= t
.d_nodeManager
;
105 bool Type::operator==(const Type
& t
) const {
106 return *d_typeNode
== *t
.d_typeNode
;
109 bool Type::operator!=(const Type
& t
) const {
110 return *d_typeNode
!= *t
.d_typeNode
;
113 bool Type::operator<(const Type
& t
) const {
114 return *d_typeNode
< *t
.d_typeNode
;
117 bool Type::operator<=(const Type
& t
) const {
118 return *d_typeNode
<= *t
.d_typeNode
;
121 bool Type::operator>(const Type
& t
) const {
122 return *d_typeNode
> *t
.d_typeNode
;
125 bool Type::operator>=(const Type
& t
) const {
126 return *d_typeNode
>= *t
.d_typeNode
;
129 Type
Type::substitute(const Type
& type
, const Type
& replacement
) const {
130 NodeManagerScope
nms(d_nodeManager
);
131 return makeType(d_typeNode
->substitute(*type
.d_typeNode
,
132 *replacement
.d_typeNode
));
135 Type
Type::substitute(const std::vector
<Type
>& types
,
136 const std::vector
<Type
>& replacements
) const {
137 NodeManagerScope
nms(d_nodeManager
);
139 vector
<TypeNode
> typesNodes
, replacementsNodes
;
141 for(vector
<Type
>::const_iterator i
= types
.begin(),
145 typesNodes
.push_back(*(*i
).d_typeNode
);
148 for(vector
<Type
>::const_iterator i
= replacements
.begin(),
149 iend
= replacements
.end();
152 replacementsNodes
.push_back(*(*i
).d_typeNode
);
155 return makeType(d_typeNode
->substitute(typesNodes
.begin(),
157 replacementsNodes
.begin(),
158 replacementsNodes
.end()));
161 ExprManager
* Type::getExprManager() const {
162 return d_nodeManager
->toExprManager();
165 void Type::toStream(std::ostream
& out
) const {
166 NodeManagerScope
nms(d_nodeManager
);
171 string
Type::toString() const {
172 NodeManagerScope
nms(d_nodeManager
);
178 /** Is this the Boolean type? */
179 bool Type::isBoolean() const {
180 NodeManagerScope
nms(d_nodeManager
);
181 return d_typeNode
->isBoolean();
184 /** Cast to a Boolean type */
185 Type::operator BooleanType() const throw(AssertionException
) {
186 NodeManagerScope
nms(d_nodeManager
);
187 Assert(isNull() || isBoolean());
188 return BooleanType(*this);
191 /** Is this the integer type? */
192 bool Type::isInteger() const {
193 NodeManagerScope
nms(d_nodeManager
);
194 return d_typeNode
->isInteger();
197 /** Cast to a integer type */
198 Type::operator IntegerType() const throw(AssertionException
) {
199 NodeManagerScope
nms(d_nodeManager
);
200 Assert(isNull() || isInteger());
201 return IntegerType(*this);
204 /** Is this the real type? */
205 bool Type::isReal() const {
206 NodeManagerScope
nms(d_nodeManager
);
207 return d_typeNode
->isReal();
210 /** Cast to a real type */
211 Type::operator RealType() const throw(AssertionException
) {
212 NodeManagerScope
nms(d_nodeManager
);
213 Assert(isNull() || isReal());
214 return RealType(*this);
217 /** Is this the pseudoboolean type? */
218 bool Type::isPseudoboolean() const {
219 NodeManagerScope
nms(d_nodeManager
);
220 return d_typeNode
->isPseudoboolean();
223 /** Cast to a pseudoboolean type */
224 Type::operator PseudobooleanType() const throw(AssertionException
) {
225 NodeManagerScope
nms(d_nodeManager
);
226 Assert(isNull() || isPseudoboolean());
227 return PseudobooleanType(*this);
230 /** Is this the string type? */
231 bool Type::isString() const {
232 NodeManagerScope
nms(d_nodeManager
);
233 return d_typeNode
->isString();
236 /** Cast to a string type */
237 Type::operator StringType() const throw(AssertionException
) {
238 NodeManagerScope
nms(d_nodeManager
);
239 Assert(isNull() || isString());
240 return StringType(*this);
243 /** Is this the bit-vector type? */
244 bool Type::isBitVector() const {
245 NodeManagerScope
nms(d_nodeManager
);
246 return d_typeNode
->isBitVector();
249 /** Cast to a bit-vector type */
250 Type::operator BitVectorType() const throw(AssertionException
) {
251 NodeManagerScope
nms(d_nodeManager
);
252 Assert(isNull() || isBitVector());
253 return BitVectorType(*this);
256 /** Cast to a Constructor type */
257 Type::operator DatatypeType() const throw(AssertionException
) {
258 NodeManagerScope
nms(d_nodeManager
);
259 Assert(isNull() || isDatatype());
260 return DatatypeType(*this);
263 /** Is this a datatype type? */
264 bool Type::isDatatype() const {
265 NodeManagerScope
nms(d_nodeManager
);
266 return d_typeNode
->isDatatype() || d_typeNode
->isParametricDatatype();
269 /** Cast to a Constructor type */
270 Type::operator ConstructorType() const throw(AssertionException
) {
271 NodeManagerScope
nms(d_nodeManager
);
272 Assert(isNull() || isConstructor());
273 return ConstructorType(*this);
276 /** Is this the Constructor type? */
277 bool Type::isConstructor() const {
278 NodeManagerScope
nms(d_nodeManager
);
279 return d_typeNode
->isConstructor();
282 /** Cast to a Selector type */
283 Type::operator SelectorType() const throw(AssertionException
) {
284 NodeManagerScope
nms(d_nodeManager
);
285 Assert(isNull() || isSelector());
286 return SelectorType(*this);
289 /** Is this the Selector type? */
290 bool Type::isSelector() const {
291 NodeManagerScope
nms(d_nodeManager
);
292 return d_typeNode
->isSelector();
295 /** Cast to a Tester type */
296 Type::operator TesterType() const throw(AssertionException
) {
297 NodeManagerScope
nms(d_nodeManager
);
298 Assert(isNull() || isTester());
299 return TesterType(*this);
302 /** Is this the Tester type? */
303 bool Type::isTester() const {
304 NodeManagerScope
nms(d_nodeManager
);
305 return d_typeNode
->isTester();
308 /** Is this a function type? */
309 bool Type::isFunction() const {
310 NodeManagerScope
nms(d_nodeManager
);
311 return d_typeNode
->isFunction();
315 * Is this a predicate type? NOTE: all predicate types are also
318 bool Type::isPredicate() const {
319 NodeManagerScope
nms(d_nodeManager
);
320 return d_typeNode
->isPredicate();
323 /** Cast to a function type */
324 Type::operator FunctionType() const throw(AssertionException
) {
325 NodeManagerScope
nms(d_nodeManager
);
326 Assert(isNull() || isFunction());
327 return FunctionType(*this);
330 /** Is this a tuple type? */
331 bool Type::isTuple() const {
332 NodeManagerScope
nms(d_nodeManager
);
333 return d_typeNode
->isTuple();
336 /** Cast to a tuple type */
337 Type::operator TupleType() const throw(AssertionException
) {
338 NodeManagerScope
nms(d_nodeManager
);
339 Assert(isNull() || isTuple());
340 return TupleType(*this);
343 /** Is this an array type? */
344 bool Type::isArray() const {
345 NodeManagerScope
nms(d_nodeManager
);
346 return d_typeNode
->isArray();
349 /** Cast to an array type */
350 Type::operator ArrayType() const throw(AssertionException
) {
351 NodeManagerScope
nms(d_nodeManager
);
352 return ArrayType(*this);
355 /** Is this a sort kind */
356 bool Type::isSort() const {
357 NodeManagerScope
nms(d_nodeManager
);
358 return d_typeNode
->isSort();
361 /** Cast to a sort type */
362 Type::operator SortType() const throw(AssertionException
) {
363 NodeManagerScope
nms(d_nodeManager
);
364 Assert(isNull() || isSort());
365 return SortType(*this);
368 /** Is this a sort constructor kind */
369 bool Type::isSortConstructor() const {
370 NodeManagerScope
nms(d_nodeManager
);
371 return d_typeNode
->isSortConstructor();
374 /** Cast to a sort type */
375 Type::operator SortConstructorType() const throw(AssertionException
) {
376 NodeManagerScope
nms(d_nodeManager
);
377 Assert(isNull() || isSortConstructor());
378 return SortConstructorType(*this);
381 /** Is this a kind type (i.e., the type of a type)? */
382 bool Type::isKind() const {
383 NodeManagerScope
nms(d_nodeManager
);
384 return d_typeNode
->isKind();
387 /** Cast to a kind type */
388 Type::operator KindType() const throw(AssertionException
) {
389 NodeManagerScope
nms(d_nodeManager
);
390 Assert(isNull() || isKind());
391 return KindType(*this);
394 vector
<Type
> FunctionType::getArgTypes() const {
395 NodeManagerScope
nms(d_nodeManager
);
397 vector
<TypeNode
> argNodes
= d_typeNode
->getArgTypes();
398 vector
<TypeNode
>::iterator it
= argNodes
.begin();
399 vector
<TypeNode
>::iterator it_end
= argNodes
.end();
400 for(; it
!= it_end
; ++ it
) {
401 args
.push_back(makeType(*it
));
406 Type
FunctionType::getRangeType() const {
407 NodeManagerScope
nms(d_nodeManager
);
408 Assert(isNull() || isFunction());
409 return makeType(d_typeNode
->getRangeType());
412 vector
<Type
> TupleType::getTypes() const {
413 NodeManagerScope
nms(d_nodeManager
);
415 vector
<TypeNode
> typeNodes
= d_typeNode
->getTupleTypes();
416 vector
<TypeNode
>::iterator it
= typeNodes
.begin();
417 vector
<TypeNode
>::iterator it_end
= typeNodes
.end();
418 for(; it
!= it_end
; ++ it
) {
419 types
.push_back(makeType(*it
));
424 string
SortType::getName() const {
425 NodeManagerScope
nms(d_nodeManager
);
426 return d_typeNode
->getAttribute(expr::VarNameAttr());
429 bool SortType::isParameterized() const {
433 /** Get the parameter types */
434 std::vector
<Type
> SortType::getParamTypes() const {
439 string
SortConstructorType::getName() const {
440 NodeManagerScope
nms(d_nodeManager
);
441 return d_typeNode
->getAttribute(expr::VarNameAttr());
444 size_t SortConstructorType::getArity() const {
445 NodeManagerScope
nms(d_nodeManager
);
446 return d_typeNode
->getAttribute(expr::SortArityAttr());
449 SortType
SortConstructorType::instantiate(const std::vector
<Type
>& params
) const {
450 NodeManagerScope
nms(d_nodeManager
);
451 vector
<TypeNode
> paramsNodes
;
452 for(vector
<Type
>::const_iterator i
= params
.begin(),
456 paramsNodes
.push_back(*getTypeNode(*i
));
458 return SortType(makeType(d_nodeManager
->mkSort(*d_typeNode
, paramsNodes
)));
461 BooleanType::BooleanType(const Type
& t
) throw(AssertionException
) :
463 Assert(isNull() || isBoolean());
466 IntegerType::IntegerType(const Type
& t
) throw(AssertionException
) :
468 Assert(isNull() || isInteger());
471 RealType::RealType(const Type
& t
) throw(AssertionException
) :
473 Assert(isNull() || isReal());
476 PseudobooleanType::PseudobooleanType(const Type
& t
) throw(AssertionException
) :
478 Assert(isNull() || isPseudoboolean());
481 StringType::StringType(const Type
& t
) throw(AssertionException
) :
483 Assert(isNull() || isString());
486 BitVectorType::BitVectorType(const Type
& t
) throw(AssertionException
) :
488 Assert(isNull() || isBitVector());
491 DatatypeType::DatatypeType(const Type
& t
) throw(AssertionException
) :
493 Assert(isNull() || isDatatype());
496 ConstructorType::ConstructorType(const Type
& t
) throw(AssertionException
) :
498 Assert(isNull() || isConstructor());
501 SelectorType::SelectorType(const Type
& t
) throw(AssertionException
) :
503 Assert(isNull() || isSelector());
506 TesterType::TesterType(const Type
& t
) throw(AssertionException
) :
508 Assert(isNull() || isTester());
511 FunctionType::FunctionType(const Type
& t
) throw(AssertionException
) :
513 Assert(isNull() || isFunction());
516 TupleType::TupleType(const Type
& t
) throw(AssertionException
) :
518 Assert(isNull() || isTuple());
521 ArrayType::ArrayType(const Type
& t
) throw(AssertionException
) :
523 Assert(isNull() || isArray());
526 KindType::KindType(const Type
& t
) throw(AssertionException
) :
528 Assert(isNull() || isKind());
531 SortType::SortType(const Type
& t
) throw(AssertionException
) :
533 Assert(isNull() || isSort());
536 SortConstructorType::SortConstructorType(const Type
& t
)
537 throw(AssertionException
) :
539 Assert(isNull() || isSortConstructor());
542 unsigned BitVectorType::getSize() const {
543 return d_typeNode
->getBitVectorSize();
546 Type
ArrayType::getIndexType() const {
547 return makeType(d_typeNode
->getArrayIndexType());
550 Type
ArrayType::getConstituentType() const {
551 return makeType(d_typeNode
->getArrayConstituentType());
554 DatatypeType
ConstructorType::getRangeType() const {
555 return DatatypeType(makeType(d_typeNode
->getConstructorRangeType()));
558 size_t ConstructorType::getArity() const {
559 return d_typeNode
->getNumChildren() - 1;
562 std::vector
<Type
> ConstructorType::getArgTypes() const {
563 NodeManagerScope
nms(d_nodeManager
);
565 vector
<TypeNode
> argNodes
= d_typeNode
->getArgTypes();
566 vector
<TypeNode
>::iterator it
= argNodes
.begin();
567 vector
<TypeNode
>::iterator it_end
= argNodes
.end();
568 for(; it
!= it_end
; ++ it
) {
569 args
.push_back(makeType(*it
));
574 const Datatype
& DatatypeType::getDatatype() const {
575 if( d_typeNode
->isParametricDatatype() ) {
576 Assert( (*d_typeNode
)[0].getKind() == kind::DATATYPE_TYPE
);
577 const Datatype
& dt
= (*d_typeNode
)[0].getConst
<Datatype
>();
580 return d_typeNode
->getConst
<Datatype
>();
584 bool DatatypeType::isParametric() const {
585 return d_typeNode
->isParametricDatatype();
588 Expr
DatatypeType::getConstructor(std::string name
) const {
589 return getDatatype().getConstructor(name
);
592 bool DatatypeType::isInstantiated() const {
593 return d_typeNode
->isInstantiatedDatatype();
596 bool DatatypeType::isParameterInstantiated(unsigned n
) const {
597 return d_typeNode
->isParameterInstantiatedDatatype(n
);
600 size_t DatatypeType::getArity() const {
601 NodeManagerScope
nms(d_nodeManager
);
602 return d_typeNode
->getNumChildren() - 1;
605 std::vector
<Type
> DatatypeType::getParamTypes() const {
606 NodeManagerScope
nms(d_nodeManager
);
608 vector
<TypeNode
> paramNodes
= d_typeNode
->getParamTypes();
609 vector
<TypeNode
>::iterator it
= paramNodes
.begin();
610 vector
<TypeNode
>::iterator it_end
= paramNodes
.end();
611 for(; it
!= it_end
; ++it
) {
612 params
.push_back(makeType(*it
));
617 DatatypeType
DatatypeType::instantiate(const std::vector
<Type
>& params
) const {
618 NodeManagerScope
nms(d_nodeManager
);
619 TypeNode cons
= d_nodeManager
->mkTypeConst( getDatatype() );
620 vector
<TypeNode
> paramsNodes
;
621 paramsNodes
.push_back( cons
);
622 for(vector
<Type
>::const_iterator i
= params
.begin(),
626 paramsNodes
.push_back(*getTypeNode(*i
));
628 return DatatypeType(makeType(d_nodeManager
->mkTypeNode(kind::PARAMETRIC_DATATYPE
,paramsNodes
)));
631 DatatypeType
SelectorType::getDomain() const {
632 return DatatypeType(makeType((*d_typeNode
)[0]));
635 Type
SelectorType::getRangeType() const {
636 return makeType((*d_typeNode
)[1]);
639 DatatypeType
TesterType::getDomain() const {
640 return DatatypeType(makeType((*d_typeNode
)[0]));
643 BooleanType
TesterType::getRangeType() const {
644 return BooleanType(makeType(d_nodeManager
->booleanType()));
647 size_t TypeHashFunction::operator()(const Type
& t
) const {
648 return TypeNodeHashFunction()(NodeManager::fromType(t
));
651 }/* CVC4 namespace */