diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-11-08 21:53:14 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-11-08 21:53:14 +0000 |
commit | 72d6f5d9eb6c28a417b00524eff51ea38e37d985 (patch) | |
tree | 2a7633872b9dc78fba3bbdd510a360435c4def39 /src | |
parent | b3470b5e0b7a664443b9f835db5dd86fb1487866 (diff) |
Review of trunk r4525 (TypeNode::getBaseType()):
* fixed TypeNode::getBaseType() for predicate subtypes
* added Type::getBaseType() for public interface
* added unit testing
To avoid confusion, also:
* renamed PredicateType::getBaseType() to "getParentType()"
* renamed TypeNode::getSubtypeBaseType() to "getSubtypeParentType()"
(this commit was certified error- and warning-free by the test-and-commit script.)
Diffstat (limited to 'src')
-rw-r--r-- | src/expr/type.cpp | 9 | ||||
-rw-r--r-- | src/expr/type.h | 12 | ||||
-rw-r--r-- | src/expr/type_node.cpp | 19 | ||||
-rw-r--r-- | src/expr/type_node.h | 31 | ||||
-rw-r--r-- | src/theory/theory.h | 2 |
5 files changed, 44 insertions, 29 deletions
diff --git a/src/expr/type.cpp b/src/expr/type.cpp index bcf0cd6c1..e64c202b4 100644 --- a/src/expr/type.cpp +++ b/src/expr/type.cpp @@ -85,6 +85,11 @@ bool Type::isComparableTo(Type t) const { return d_typeNode->isComparableTo(*t.d_typeNode); } +Type Type::getBaseType() const { + NodeManagerScope nms(d_nodeManager); + return d_typeNode->getBaseType().toType(); +} + Type& Type::operator=(const Type& t) { CheckArgument(d_typeNode != NULL, this, "Unexpected NULL typenode pointer!"); CheckArgument(t.d_typeNode != NULL, t, "Unexpected NULL typenode pointer!"); @@ -699,9 +704,9 @@ Expr PredicateSubtype::getPredicate() const { return d_typeNode->getSubtypePredicate().toExpr(); } -Type PredicateSubtype::getBaseType() const { +Type PredicateSubtype::getParentType() const { NodeManagerScope nms(d_nodeManager); - return d_typeNode->getSubtypeBaseType().toType(); + return d_typeNode->getSubtypeParentType().toType(); } SubrangeBounds SubrangeType::getSubrangeBounds() const { diff --git a/src/expr/type.h b/src/expr/type.h index b3180b958..f8a5f48fe 100644 --- a/src/expr/type.h +++ b/src/expr/type.h @@ -164,6 +164,11 @@ public: bool isComparableTo(Type t) const; /** + * Get the most general base type of this type. + */ + Type getBaseType() const; + + /** * Substitution of Types. */ Type substitute(const Type& type, const Type& replacement) const; @@ -609,8 +614,11 @@ public: /** Get the LAMBDA defining this predicate subtype */ Expr getPredicate() const; - /** Get the base type of this predicate subtype */ - Type getBaseType() const; + /** + * Get the parent type of this predicate subtype; note that this + * could be another predicate subtype. + */ + Type getParentType() const; };/* class PredicateSubtype */ diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp index 80f7f8c76..ae870b1c2 100644 --- a/src/expr/type_node.cpp +++ b/src/expr/type_node.cpp @@ -91,7 +91,7 @@ bool TypeNode::isSubtypeOf(TypeNode t) const { } } if(isPredicateSubtype()) { - return getSubtypeBaseType().isSubtypeOf(t); + return getSubtypeParentType().isSubtypeOf(t); } return false; } @@ -104,7 +104,7 @@ bool TypeNode::isComparableTo(TypeNode t) const { return t.isSubtypeOf(NodeManager::currentNM()->realType()); } if(isPredicateSubtype()) { - return t.isComparableTo(getSubtypeBaseType()); + return t.isComparableTo(getSubtypeParentType()); } return false; } @@ -114,7 +114,7 @@ Node TypeNode::getSubtypePredicate() const { return Node::fromExpr(getConst<Predicate>()); } -TypeNode TypeNode::getSubtypeBaseType() const { +TypeNode TypeNode::getSubtypeParentType() const { Assert(isPredicateSubtype()); return getSubtypePredicate().getType().getArgTypes()[0]; } @@ -123,9 +123,8 @@ TypeNode TypeNode::getBaseType() const { TypeNode realt = NodeManager::currentNM()->realType(); if (isSubtypeOf(realt)) { return realt; - } - else if (isPredicateSubtype()) { - return getSubtypeBaseType(); + } else if (isPredicateSubtype()) { + return getSubtypeParentType().getBaseType(); } return *this; } @@ -228,7 +227,7 @@ TypeNode TypeNode::leastCommonTypeNode(TypeNode t0, TypeNode t1){ return TypeNode(); // null type } default: - if(t1.isPredicateSubtype() && t1.getSubtypeBaseType().isSubtypeOf(t0)){ + if(t1.isPredicateSubtype() && t1.getSubtypeParentType().isSubtypeOf(t0)){ return t0; // t0 is a constant type }else{ return TypeNode(); // null type @@ -248,7 +247,7 @@ TypeNode TypeNode::leastCommonTypeNode(TypeNode t0, TypeNode t1){ case kind::CONSTRUCTOR_TYPE: case kind::SELECTOR_TYPE: case kind::TESTER_TYPE: - if(t1.isPredicateSubtype() && t1.getSubtypeBaseType().isSubtypeOf(t0)){ + if(t1.isPredicateSubtype() && t1.getSubtypeParentType().isSubtypeOf(t0)){ return t0; }else{ return TypeNode(); @@ -316,12 +315,12 @@ TypeNode TypeNode::leastCommonPredicateSubtype(TypeNode t0, TypeNode t1){ std::vector<TypeNode> t0stack; t0stack.push_back(t0); while(t0stack.back().isPredicateSubtype()){ - t0stack.push_back(t0stack.back().getSubtypeBaseType()); + t0stack.push_back(t0stack.back().getSubtypeParentType()); } std::vector<TypeNode> t1stack; t1stack.push_back(t1); while(t1stack.back().isPredicateSubtype()){ - t1stack.push_back(t1stack.back().getSubtypeBaseType()); + t1stack.push_back(t1stack.back().getSubtypeParentType()); } Assert(!t0stack.empty()); diff --git a/src/expr/type_node.h b/src/expr/type_node.h index 5f399a855..fc142191d 100644 --- a/src/expr/type_node.h +++ b/src/expr/type_node.h @@ -587,8 +587,11 @@ public: /** Get the predicate defining this subtype */ Node getSubtypePredicate() const; - /** Get the base type of this subtype */ - TypeNode getSubtypeBaseType() const; + /** + * Get the parent type of this subtype; note that it could be + * another subtype. + */ + TypeNode getSubtypeParentType() const; /** Get the most general base type of the type */ TypeNode getBaseType() const; @@ -805,21 +808,21 @@ inline void TypeNode::printAst(std::ostream& out, int indent) const { inline bool TypeNode::isBoolean() const { return ( getKind() == kind::TYPE_CONSTANT && getConst<TypeConstant>() == BOOLEAN_TYPE ) || - ( isPredicateSubtype() && getSubtypeBaseType().isBoolean() ); + ( isPredicateSubtype() && getSubtypeParentType().isBoolean() ); } inline bool TypeNode::isInteger() const { return ( getKind() == kind::TYPE_CONSTANT && getConst<TypeConstant>() == INTEGER_TYPE ) || isSubrange() || - ( isPredicateSubtype() && getSubtypeBaseType().isInteger() ); + ( isPredicateSubtype() && getSubtypeParentType().isInteger() ); } inline bool TypeNode::isReal() const { return ( getKind() == kind::TYPE_CONSTANT && getConst<TypeConstant>() == REAL_TYPE ) || isInteger() || - ( isPredicateSubtype() && getSubtypeBaseType().isReal() ); + ( isPredicateSubtype() && getSubtypeParentType().isReal() ); } inline bool TypeNode::isString() const { @@ -877,19 +880,19 @@ inline TypeNode TypeNode::getRangeType() const { /** Is this a tuple type? */ inline bool TypeNode::isTuple() const { return getKind() == kind::TUPLE_TYPE || - ( isPredicateSubtype() && getSubtypeBaseType().isTuple() ); + ( isPredicateSubtype() && getSubtypeParentType().isTuple() ); } /** Is this a symbolic expression type? */ inline bool TypeNode::isSExpr() const { return getKind() == kind::SEXPR_TYPE || - ( isPredicateSubtype() && getSubtypeBaseType().isSExpr() ); + ( isPredicateSubtype() && getSubtypeParentType().isSExpr() ); } /** Is this a sort kind */ inline bool TypeNode::isSort() const { return ( getKind() == kind::SORT_TYPE && !hasAttribute(expr::SortArityAttr()) ) || - ( isPredicateSubtype() && getSubtypeBaseType().isSort() ); + ( isPredicateSubtype() && getSubtypeParentType().isSort() ); } /** Is this a sort constructor kind */ @@ -905,25 +908,25 @@ inline bool TypeNode::isPredicateSubtype() const { /** Is this a subrange type */ inline bool TypeNode::isSubrange() const { return getKind() == kind::SUBRANGE_TYPE || - ( isPredicateSubtype() && getSubtypeBaseType().isSubrange() ); + ( isPredicateSubtype() && getSubtypeParentType().isSubrange() ); } /** Is this a bit-vector type */ inline bool TypeNode::isBitVector() const { return getKind() == kind::BITVECTOR_TYPE || - ( isPredicateSubtype() && getSubtypeBaseType().isBitVector() ); + ( isPredicateSubtype() && getSubtypeParentType().isBitVector() ); } /** Is this a datatype type */ inline bool TypeNode::isDatatype() const { return getKind() == kind::DATATYPE_TYPE || - ( isPredicateSubtype() && getSubtypeBaseType().isDatatype() ); + ( isPredicateSubtype() && getSubtypeParentType().isDatatype() ); } /** Is this a parametric datatype type */ inline bool TypeNode::isParametricDatatype() const { return getKind() == kind::PARAMETRIC_DATATYPE || - ( isPredicateSubtype() && getSubtypeBaseType().isParametricDatatype() ); + ( isPredicateSubtype() && getSubtypeParentType().isParametricDatatype() ); } /** Is this a constructor type */ @@ -945,7 +948,7 @@ inline bool TypeNode::isTester() const { inline bool TypeNode::isBitVector(unsigned size) const { return ( getKind() == kind::BITVECTOR_TYPE && getConst<BitVectorSize>() == size ) || - ( isPredicateSubtype() && getSubtypeBaseType().isBitVector(size) ); + ( isPredicateSubtype() && getSubtypeParentType().isBitVector(size) ); } /** Get the size of this bit-vector type */ @@ -960,7 +963,7 @@ inline const SubrangeBounds& TypeNode::getSubrangeBounds() const { return getConst<SubrangeBounds>(); }else{ Assert(isPredicateSubtype()); - return getSubtypeBaseType().getSubrangeBounds(); + return getSubtypeParentType().getSubrangeBounds(); } } diff --git a/src/theory/theory.h b/src/theory/theory.h index 195e37154..9cc5058cc 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -308,7 +308,7 @@ public: Trace("theory::internal") << "theoryOf(" << typeNode << ")" << std::endl; TheoryId id; while (typeNode.isPredicateSubtype()) { - typeNode = typeNode.getSubtypeBaseType(); + typeNode = typeNode.getSubtypeParentType(); } if (typeNode.getKind() == kind::TYPE_CONSTANT) { id = typeConstantToTheoryId(typeNode.getConst<TypeConstant>()); |