diff options
Diffstat (limited to 'src/expr/type.cpp')
-rw-r--r-- | src/expr/type.cpp | 46 |
1 files changed, 23 insertions, 23 deletions
diff --git a/src/expr/type.cpp b/src/expr/type.cpp index 6a8e6609c..6b5bdf07c 100644 --- a/src/expr/type.cpp +++ b/src/expr/type.cpp @@ -292,29 +292,6 @@ bool Type::isRecord() const { return d_typeNode->isRecord(); } -/** Get the length of a tuple type */ -size_t Type::getTupleLength() const { - NodeManagerScope nms(d_nodeManager); - return d_typeNode->getTupleLength(); -} - -/** Get the constituent types of a tuple type */ -std::vector<Type> Type::getTupleTypes() const { - NodeManagerScope nms(d_nodeManager); - std::vector< TypeNode > vec = d_typeNode->getTupleTypes(); - std::vector< Type > vect; - for( unsigned i=0; i<vec.size(); i++ ){ - vect.push_back( vec[i].toType() ); - } - return vect; -} - -/** Get the description of the record type */ -const Record& Type::getRecord() const { - NodeManagerScope nms(d_nodeManager); - return d_typeNode->getRecord(); -} - /** Is this a symbolic expression type? */ bool Type::isSExpr() const { NodeManagerScope nms(d_nodeManager); @@ -632,6 +609,29 @@ DatatypeType DatatypeType::instantiate(const std::vector<Type>& params) const { return DatatypeType(makeType(d_nodeManager->mkTypeNode(kind::PARAMETRIC_DATATYPE, paramsNodes))); } +/** Get the length of a tuple type */ +size_t DatatypeType::getTupleLength() const { + NodeManagerScope nms(d_nodeManager); + return d_typeNode->getTupleLength(); +} + +/** Get the constituent types of a tuple type */ +std::vector<Type> DatatypeType::getTupleTypes() const { + NodeManagerScope nms(d_nodeManager); + std::vector< TypeNode > vec = d_typeNode->getTupleTypes(); + std::vector< Type > vect; + for( unsigned i=0; i<vec.size(); i++ ){ + vect.push_back( vec[i].toType() ); + } + return vect; +} + +/** Get the description of the record type */ +const Record& DatatypeType::getRecord() const { + NodeManagerScope nms(d_nodeManager); + return d_typeNode->getRecord(); +} + DatatypeType SelectorType::getDomain() const { return DatatypeType(makeType((*d_typeNode)[0])); } |