diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-02-15 13:02:02 -0600 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-02-15 13:02:02 -0600 |
commit | 62b673a6b8444c14c169a984dd6e3fc8f685851e (patch) | |
tree | f0703edec34e3512dac340ce0059cba6368d7dd8 /src/expr | |
parent | 7acc2844df65ab6fdbf8166653c71eaa26d4d151 (diff) |
Eliminate most of the internal representation infrastructure for tuples and records, replace with datatypes throughout, update cvc printer for tuples/records. Minor changes to API for records and tuples.
Diffstat (limited to 'src/expr')
-rw-r--r-- | src/expr/datatype.cpp | 8 | ||||
-rw-r--r-- | src/expr/datatype.h | 31 | ||||
-rw-r--r-- | src/expr/expr_manager_template.cpp | 9 | ||||
-rw-r--r-- | src/expr/expr_manager_template.h | 4 | ||||
-rw-r--r-- | src/expr/node_manager.cpp | 123 | ||||
-rw-r--r-- | src/expr/node_manager.h | 24 | ||||
-rw-r--r-- | src/expr/type.cpp | 54 | ||||
-rw-r--r-- | src/expr/type.h | 45 | ||||
-rw-r--r-- | src/expr/type_node.cpp | 51 | ||||
-rw-r--r-- | src/expr/type_node.h | 19 |
10 files changed, 161 insertions, 207 deletions
diff --git a/src/expr/datatype.cpp b/src/expr/datatype.cpp index b9870afb4..32c0bb6dd 100644 --- a/src/expr/datatype.cpp +++ b/src/expr/datatype.cpp @@ -151,6 +151,13 @@ void Datatype::setSygus( Type st, Expr bvl, bool allow_const, bool allow_all ){ d_sygus_allow_all = allow_all; } +void Datatype::setTuple() { + d_isTuple = true; +} + +void Datatype::setRecord() { + d_isRecord = true; +} Cardinality Datatype::getCardinality() const throw(IllegalArgumentException) { PrettyCheckArgument(isResolved(), this, "this datatype is not yet resolved"); @@ -663,7 +670,6 @@ void DatatypeConstructor::setSygus( Expr op, Expr let_body, std::vector< Expr >& d_sygus_num_let_input_args = num_let_input_args; } - void DatatypeConstructor::addArg(std::string selectorName, Type selectorType) { // We don't want to introduce a new data member, because eventually // we're going to be a constant stuffed inside a node. So we stow diff --git a/src/expr/datatype.h b/src/expr/datatype.h index 5f80c54f7..625fbb5d4 100644 --- a/src/expr/datatype.h +++ b/src/expr/datatype.h @@ -237,9 +237,6 @@ public: */ DatatypeConstructor(std::string name, std::string tester); - /** set sygus */ - void setSygus( Expr op, Expr let_body, std::vector< Expr >& let_args, unsigned num_let_input_argus ); - /** * Add an argument (i.e., a data field) of the given name and type * to this Datatype constructor. Selector names need not be unique; @@ -382,6 +379,8 @@ public: bool involvesExternalType() const; bool involvesUninterpretedType() const; + /** set sygus */ + void setSygus( Expr op, Expr let_body, std::vector< Expr >& let_args, unsigned num_let_input_argus ); };/* class DatatypeConstructor */ /** @@ -473,6 +472,8 @@ private: std::string d_name; std::vector<Type> d_params; bool d_isCo; + bool d_isTuple; + bool d_isRecord; std::vector<DatatypeConstructor> d_constructors; bool d_resolved; Type d_self; @@ -565,6 +566,12 @@ public: */ void setSygus( Type st, Expr bvl, bool allow_const, bool allow_all ); + /** set tuple */ + void setTuple(); + + /** set tuple */ + void setRecord(); + /** Get the name of this Datatype. */ inline std::string getName() const throw(); @@ -589,6 +596,12 @@ public: /** is this a sygus datatype? */ inline bool isSygus() const; + /** is this a tuple datatype? */ + inline bool isTuple() const; + + /** is this a record datatype? */ + inline bool isRecord() const; + /** * Return the cardinality of this datatype (the sum of the * cardinalities of its constructors). The Datatype must be @@ -757,6 +770,8 @@ inline Datatype::Datatype(std::string name, bool isCo) : d_name(name), d_params(), d_isCo(isCo), + d_isTuple(false), + d_isRecord(false), d_constructors(), d_resolved(false), d_self(), @@ -771,6 +786,8 @@ inline Datatype::Datatype(std::string name, const std::vector<Type>& params, boo d_name(name), d_params(params), d_isCo(isCo), + d_isTuple(false), + d_isRecord(false), d_constructors(), d_resolved(false), d_self(), @@ -819,6 +836,14 @@ inline bool Datatype::isSygus() const { return !d_sygus_type.isNull(); } +inline bool Datatype::isTuple() const { + return d_isTuple; +} + +inline bool Datatype::isRecord() const { + return d_isRecord; +} + inline bool Datatype::operator!=(const Datatype& other) const throw() { return !(*this == other); } diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp index 0b9557cc8..ce7a92b48 100644 --- a/src/expr/expr_manager_template.cpp +++ b/src/expr/expr_manager_template.cpp @@ -20,6 +20,7 @@ #include "expr/node_manager.h" #include "expr/variable_type_map.h" +#include "expr/node_manager_attributes.h" #include "options/options.h" #include "util/statistics_registry.h" @@ -596,18 +597,18 @@ FunctionType ExprManager::mkPredicateType(const std::vector<Type>& sorts) { return FunctionType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkPredicateType(sortNodes)))); } -TupleType ExprManager::mkTupleType(const std::vector<Type>& types) { +DatatypeType ExprManager::mkTupleType(const std::vector<Type>& types) { NodeManagerScope nms(d_nodeManager); std::vector<TypeNode> typeNodes; for (unsigned i = 0, i_end = types.size(); i < i_end; ++ i) { typeNodes.push_back(*types[i].d_typeNode); } - return TupleType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkTupleType(typeNodes)))); + return DatatypeType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkTupleType(typeNodes)))); } -RecordType ExprManager::mkRecordType(const Record& rec) { +DatatypeType ExprManager::mkRecordType(const Record& rec) { NodeManagerScope nms(d_nodeManager); - return RecordType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkRecordType(rec)))); + return DatatypeType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkRecordType(rec)))); } SExprType ExprManager::mkSExprType(const std::vector<Type>& types) { diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h index e65cfc358..37ef128f4 100644 --- a/src/expr/expr_manager_template.h +++ b/src/expr/expr_manager_template.h @@ -341,12 +341,12 @@ public: * <code>types[0..types.size()-1]</code>. <code>types</code> must * have at least one element. */ - TupleType mkTupleType(const std::vector<Type>& types); + DatatypeType mkTupleType(const std::vector<Type>& types); /** * Make a record type with types from the rec parameter. */ - RecordType mkRecordType(const Record& rec); + DatatypeType mkRecordType(const Record& rec); /** * Make a symbolic expressiontype with types from diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index e52776fce..e6e44928d 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -461,79 +461,66 @@ TypeNode NodeManager::mkSubrangeType(const SubrangeBounds& bounds) return TypeNode(mkTypeConst(bounds)); } -TypeNode NodeManager::getDatatypeForTupleRecord(TypeNode t) { - Assert(t.isTuple() || t.isRecord()); - - //AJR: not sure why .getBaseType() was used in two cases below, - // disabling this, which is necessary to fix bug 605/667, - // which involves records of INT which were mapped to records of REAL below. - TypeNode tOrig = t; - if(t.isTuple()) { - vector<TypeNode> v; - bool changed = false; - for(size_t i = 0; i < t.getNumChildren(); ++i) { - TypeNode tn = t[i]; - TypeNode base; - if(tn.isTuple() || tn.isRecord()) { - base = getDatatypeForTupleRecord(tn); - } else { - base = tn;//.getBaseType(); - } - changed = changed || (tn != base); - v.push_back(base); - } - if(changed) { - t = mkTupleType(v); - } - } else { - const Record& r = t.getRecord(); - std::vector< std::pair<std::string, Type> > v; - bool changed = false; - const Record::FieldVector& fields = r.getFields(); - for(Record::FieldVector::const_iterator i = fields.begin(); i != fields.end(); ++i) { - Type tn = (*i).second; - Type base; - if(tn.isTuple() || tn.isRecord()) { - base = getDatatypeForTupleRecord(TypeNode::fromType(tn)).toType(); - } else { - base = tn;//.getBaseType(); - } - changed = changed || (tn != base); - v.push_back(std::make_pair((*i).first, base)); - } - if(changed) { - t = mkRecordType(Record(v)); +TypeNode NodeManager::mkTupleType(const std::vector<TypeNode>& types) { + std::vector< TypeNode > ts; + Debug("tuprec-debug") << "Make tuple type : "; + for (unsigned i = 0; i < types.size(); ++ i) { + CheckArgument(!types[i].isFunctionLike(), types, "cannot put function-like types in tuples"); + ts.push_back( types[i] ); + Debug("tuprec-debug") << types[i] << " "; + } + Debug("tuprec-debug") << std::endl; + //index based on function type + TypeNode tindex; + if( types.empty() ){ + //do nothing (will index on null type) + }else if( types.size()==1 ){ + tindex = types[0]; + }else{ + TypeNode tt = ts.back(); + ts.pop_back(); + tindex = mkFunctionType( ts, tt ); + ts.push_back( tt ); + } + TypeNode& dtt = d_tupleAndRecordTypes[tindex]; + if(dtt.isNull()) { + Datatype dt("__cvc4_tuple"); + dt.setTuple(); + DatatypeConstructor c("__cvc4_tuple_ctor"); + for (unsigned i = 0; i < ts.size(); ++ i) { + std::stringstream ss; + ss << "__cvc4_tuple_stor_" << i; + c.addArg(ss.str().c_str(), ts[i].toType()); } + dt.addConstructor(c); + dtt = TypeNode::fromType(toExprManager()->mkDatatypeType(dt)); + dtt.setAttribute(DatatypeTupleAttr(), tindex); + Debug("tuprec-debug") << "Return type : " << dtt << std::endl; + }else{ + Debug("tuprec-debug") << "Return cached type : " << dtt << std::endl; } + Assert(!dtt.isNull()); + return dtt; +} - // if the type doesn't have an associated datatype, then make one for it - TypeNode& dtt = d_tupleAndRecordTypes[t]; +TypeNode NodeManager::mkRecordType(const Record& rec) { + //index based on type constant + TypeNode tindex = mkTypeConst(rec); + TypeNode& dtt = d_tupleAndRecordTypes[tindex]; if(dtt.isNull()) { - if(t.isTuple()) { - Datatype dt("__cvc4_tuple"); - DatatypeConstructor c("__cvc4_tuple_ctor"); - for(TypeNode::const_iterator i = t.begin(); i != t.end(); ++i) { - c.addArg("__cvc4_tuple_stor", (*i).toType()); - } - dt.addConstructor(c); - dtt = TypeNode::fromType(toExprManager()->mkDatatypeType(dt)); - Debug("tuprec") << "REWROTE " << t << " to " << dtt << std::endl; - dtt.setAttribute(DatatypeTupleAttr(), tOrig); - } else { - const Record& rec = t.getRecord(); - const Record::FieldVector& fields = rec.getFields(); - Datatype dt("__cvc4_record"); - DatatypeConstructor c("__cvc4_record_ctor"); - for(Record::FieldVector::const_iterator i = fields.begin(); i != fields.end(); ++i) { - c.addArg((*i).first, (*i).second); - } - dt.addConstructor(c); - dtt = TypeNode::fromType(toExprManager()->mkDatatypeType(dt)); - Debug("tuprec") << "REWROTE " << t << " to " << dtt << std::endl; - dtt.setAttribute(DatatypeRecordAttr(), tOrig); + const Record::FieldVector& fields = rec.getFields(); + Datatype dt("__cvc4_record"); + dt.setRecord(); + DatatypeConstructor c("__cvc4_record_ctor"); + for(Record::FieldVector::const_iterator i = fields.begin(); i != fields.end(); ++i) { + c.addArg((*i).first, (*i).second); } - } else { - Debug("tuprec") << "REUSING cached " << t << ": " << dtt << std::endl; + dt.addConstructor(c); + dtt = TypeNode::fromType(toExprManager()->mkDatatypeType(dt)); + dtt.setAttribute(DatatypeRecordAttr(), tindex); + Debug("tuprec-debug") << "Return type : " << dtt << std::endl; + }else{ + Debug("tuprec-debug") << "Return cached type : " << dtt << std::endl; } Assert(!dtt.isNull()); return dtt; diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 1ae9f1e8e..45c9afbde 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -756,7 +756,7 @@ public: * @param types a vector of types * @returns the tuple type (types[0], ..., types[n]) */ - inline TypeNode mkTupleType(const std::vector<TypeNode>& types); + TypeNode mkTupleType(const std::vector<TypeNode>& types); /** * Make a record type with the description from rec. @@ -764,7 +764,7 @@ public: * @param rec a description of the record * @returns the record type */ - inline TypeNode mkRecordType(const Record& rec); + TypeNode mkRecordType(const Record& rec); /** * Make a symbolic expression type with types from @@ -839,12 +839,6 @@ public: throw(TypeCheckingExceptionPrivate); /** - * Given a tuple or record type, get the internal datatype used for - * it. Makes the DatatypeType if necessary. - */ - TypeNode getDatatypeForTupleRecord(TypeNode tupleRecordType); - - /** * Get the type for the given node and optionally do type checking. * * Initial type computation will be near-constant time if @@ -1063,20 +1057,6 @@ NodeManager::mkPredicateType(const std::vector<TypeNode>& sorts) { return mkTypeNode(kind::FUNCTION_TYPE, sortNodes); } -inline TypeNode NodeManager::mkTupleType(const std::vector<TypeNode>& types) { - std::vector<TypeNode> typeNodes; - for (unsigned i = 0; i < types.size(); ++ i) { - CheckArgument(!types[i].isFunctionLike(), types, - "cannot put function-like types in tuples"); - typeNodes.push_back(types[i]); - } - return mkTypeNode(kind::TUPLE_TYPE, typeNodes); -} - -inline TypeNode NodeManager::mkRecordType(const Record& rec) { - return mkTypeConst(rec); -} - inline TypeNode NodeManager::mkSExprType(const std::vector<TypeNode>& types) { std::vector<TypeNode> typeNodes; for (unsigned i = 0; i < types.size(); ++ i) { diff --git a/src/expr/type.cpp b/src/expr/type.cpp index 99d04d658..6a8e6609c 100644 --- a/src/expr/type.cpp +++ b/src/expr/type.cpp @@ -292,6 +292,29 @@ 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); @@ -358,27 +381,6 @@ Type FunctionType::getRangeType() const { return makeType(d_typeNode->getRangeType()); } -size_t TupleType::getLength() const { - return d_typeNode->getTupleLength(); -} - -vector<Type> TupleType::getTypes() const { - NodeManagerScope nms(d_nodeManager); - vector<Type> types; - vector<TypeNode> typeNodes = d_typeNode->getTupleTypes(); - vector<TypeNode>::iterator it = typeNodes.begin(); - vector<TypeNode>::iterator it_end = typeNodes.end(); - for(; it != it_end; ++ it) { - types.push_back(makeType(*it)); - } - return types; -} - -const Record& RecordType::getRecord() const { - NodeManagerScope nms(d_nodeManager); - return d_typeNode->getRecord(); -} - vector<Type> SExprType::getTypes() const { NodeManagerScope nms(d_nodeManager); vector<Type> types; @@ -488,16 +490,6 @@ FunctionType::FunctionType(const Type& t) throw(IllegalArgumentException) PrettyCheckArgument(isNull() || isFunction(), this); } -TupleType::TupleType(const Type& t) throw(IllegalArgumentException) - : Type(t) { - PrettyCheckArgument(isNull() || isTuple(), this); -} - -RecordType::RecordType(const Type& t) throw(IllegalArgumentException) - : Type(t) { - PrettyCheckArgument(isNull() || isRecord(), this); -} - SExprType::SExprType(const Type& t) throw(IllegalArgumentException) : Type(t) { PrettyCheckArgument(isNull() || isSExpr(), this); diff --git a/src/expr/type.h b/src/expr/type.h index 0f2118c44..b7ea14f78 100644 --- a/src/expr/type.h +++ b/src/expr/type.h @@ -56,8 +56,6 @@ class ConstructorType; class SelectorType; class TesterType; class FunctionType; -class TupleType; -class RecordType; class SExprType; class SortType; class SortConstructorType; @@ -302,6 +300,15 @@ public: */ bool isRecord() const; + /** Get the length of a tuple type */ + size_t getTupleLength() const; + + /** Get the constituent types of a tuple type */ + std::vector<Type> getTupleTypes() const; + + /** Get the description of the record type */ + const Record& getRecord() const; + /** * Is this a symbolic expression type? * @return true if the type is a symbolic expression type @@ -459,39 +466,7 @@ public: };/* class FunctionType */ /** - * Class encapsulating a tuple type. - */ -class CVC4_PUBLIC TupleType : public Type { - -public: - - /** Construct from the base type */ - TupleType(const Type& type = Type()) throw(IllegalArgumentException); - - /** Get the length of the tuple. The same as getTypes().size(). */ - size_t getLength() const; - - /** Get the constituent types */ - std::vector<Type> getTypes() const; - -};/* class TupleType */ - -/** - * Class encapsulating a record type. - */ -class CVC4_PUBLIC RecordType : public Type { - -public: - - /** Construct from the base type */ - RecordType(const Type& type = Type()) throw(IllegalArgumentException); - - /** Get the constituent types */ - const Record& getRecord() const; -};/* class RecordType */ - -/** - * Class encapsulating a tuple type. + * Class encapsulating a sexpr type. */ class CVC4_PUBLIC SExprType : public Type { diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp index ea185f98b..755b16e46 100644 --- a/src/expr/type_node.cpp +++ b/src/expr/type_node.cpp @@ -94,9 +94,6 @@ bool TypeNode::isSubtypeOf(TypeNode t) const { } } if(isTuple() || isRecord()) { - if(t == NodeManager::currentNM()->getDatatypeForTupleRecord(*this)) { - return true; - } if(isTuple() != t.isTuple() || isRecord() != t.isRecord()) { return false; } @@ -111,8 +108,8 @@ bool TypeNode::isSubtypeOf(TypeNode t) const { } } } else { - const Record& r1 = getConst<Record>(); - const Record& r2 = t.getConst<Record>(); + const Record& r1 = getRecord(); + const Record& r2 = t.getRecord(); if(r1.getNumFields() != r2.getNumFields()) { return false; } @@ -166,12 +163,8 @@ bool TypeNode::isComparableTo(TypeNode t) const { if(isSubtypeOf(NodeManager::currentNM()->realType())) { return t.isSubtypeOf(NodeManager::currentNM()->realType()); } - if(t.isDatatype() && (isTuple() || isRecord())) { + if(isTuple() || isRecord()) { if(t.isTuple() || t.isRecord()) { - if(NodeManager::currentNM()->getDatatypeForTupleRecord(t) == - NodeManager::currentNM()->getDatatypeForTupleRecord(*this)) { - return true; - } if(isTuple() != t.isTuple() || isRecord() != t.isRecord()) { return false; } @@ -186,8 +179,8 @@ bool TypeNode::isComparableTo(TypeNode t) const { } } } else { - const Record& r1 = getConst<Record>(); - const Record& r2 = t.getConst<Record>(); + const Record& r1 = getRecord(); + const Record& r2 = t.getRecord(); if(r1.getNumFields() != r2.getNumFields()) { return false; } @@ -202,12 +195,7 @@ bool TypeNode::isComparableTo(TypeNode t) const { } } return true; - } else { - return t == NodeManager::currentNM()->getDatatypeForTupleRecord(*this); } - } else if(isDatatype() && (t.isTuple() || t.isRecord())) { - Assert(!isTuple() && !isRecord());// should have been handled above - return *this == NodeManager::currentNM()->getDatatypeForTupleRecord(t); } else if(isParametricDatatype() && t.isParametricDatatype()) { Assert(getKind() == kind::PARAMETRIC_DATATYPE); Assert(t.getKind() == kind::PARAMETRIC_DATATYPE); @@ -244,8 +232,6 @@ TypeNode TypeNode::getBaseType() const { TypeNode realt = NodeManager::currentNM()->realType(); if (isSubtypeOf(realt)) { return realt; - } else if (isTuple() || isRecord()) { - return NodeManager::currentNM()->getDatatypeForTupleRecord(*this); } else if (isPredicateSubtype()) { return getSubtypeParentType().getBaseType(); } else if (isParametricDatatype()) { @@ -282,23 +268,40 @@ std::vector<TypeNode> TypeNode::getParamTypes() const { return params; } + +/** Is this a tuple type? */ +bool TypeNode::isTuple() const { + return ( getKind() == kind::DATATYPE_TYPE && hasAttribute(expr::DatatypeTupleAttr()) ) || + ( isPredicateSubtype() && getSubtypeParentType().isTuple() ); +} + +/** Is this a record type? */ +bool TypeNode::isRecord() const { + return ( getKind() == kind::DATATYPE_TYPE && hasAttribute(expr::DatatypeRecordAttr()) ) || + ( isPredicateSubtype() && getSubtypeParentType().isRecord() ); +} + size_t TypeNode::getTupleLength() const { Assert(isTuple()); - return getNumChildren(); + const Datatype& dt = getConst<Datatype>(); + Assert(dt.getNumConstructors()==1); + return dt[0].getNumArgs(); } vector<TypeNode> TypeNode::getTupleTypes() const { Assert(isTuple()); + const Datatype& dt = getConst<Datatype>(); + Assert(dt.getNumConstructors()==1); vector<TypeNode> types; - for(unsigned i = 0, i_end = getNumChildren(); i < i_end; ++i) { - types.push_back((*this)[i]); + for(unsigned i = 0; i < dt[0].getNumArgs(); ++i) { + types.push_back(TypeNode::fromType(((SelectorType)dt[0][i].getSelector().getType()).getRangeType())); } return types; } const Record& TypeNode::getRecord() const { Assert(isRecord()); - return getConst<Record>(); + return getAttribute(expr::DatatypeRecordAttr()).getConst<Record>(); } vector<TypeNode> TypeNode::getSExprTypes() const { @@ -446,6 +449,7 @@ TypeNode TypeNode::leastCommonTypeNode(TypeNode t0, TypeNode t1){ Assert(t1.isInteger()); return TypeNode(); } +/* case kind::TUPLE_TYPE: { // if the other == this one, we returned already, above if(t0.getBaseType() == t1) { @@ -495,6 +499,7 @@ TypeNode TypeNode::leastCommonTypeNode(TypeNode t0, TypeNode t1){ // if we make it here, we constructed the least common type return NodeManager::currentNM()->mkRecordType(Record(fields)); } +*/ case kind::DATATYPE_TYPE: // t1 might be a subtype tuple or record if(t1.getBaseType() == t0) { diff --git a/src/expr/type_node.h b/src/expr/type_node.h index 59f602f09..4c48cc3ca 100644 --- a/src/expr/type_node.h +++ b/src/expr/type_node.h @@ -929,18 +929,6 @@ inline TypeNode TypeNode::getRangeType() const { return (*this)[getNumChildren() - 1]; } -/** Is this a tuple type? */ -inline bool TypeNode::isTuple() const { - return getKind() == kind::TUPLE_TYPE || - ( isPredicateSubtype() && getSubtypeParentType().isTuple() ); -} - -/** Is this a record type? */ -inline bool TypeNode::isRecord() const { - return getKind() == kind::RECORD_TYPE || - ( isPredicateSubtype() && getSubtypeParentType().isRecord() ); -} - /** Is this a symbolic expression type? */ inline bool TypeNode::isSExpr() const { return getKind() == kind::SEXPR_TYPE || @@ -973,7 +961,6 @@ inline bool TypeNode::isBitVector() const { /** Is this a datatype type */ inline bool TypeNode::isDatatype() const { return getKind() == kind::DATATYPE_TYPE || - getKind() == kind::TUPLE_TYPE || getKind() == kind::RECORD_TYPE || ( isPredicateSubtype() && getSubtypeParentType().isDatatype() ); } @@ -1027,11 +1014,7 @@ inline bool TypeNode::isBitVector(unsigned size) const { /** Get the datatype specification from a datatype type */ inline const Datatype& TypeNode::getDatatype() const { Assert(isDatatype()); - if(getKind() == kind::DATATYPE_TYPE) { - return getConst<Datatype>(); - } else { - return NodeManager::currentNM()->getDatatypeForTupleRecord(*this).getConst<Datatype>(); - } + return getConst<Datatype>(); } /** Get the exponent size of this floating-point type */ |