From: Morgan Deters Date: Thu, 8 Nov 2012 21:53:14 +0000 (+0000) Subject: Review of trunk r4525 (TypeNode::getBaseType()): X-Git-Tag: cvc5-1.0.0~7639 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=72d6f5d9eb6c28a417b00524eff51ea38e37d985;p=cvc5.git 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.) --- 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 @@ -163,6 +163,11 @@ public: */ bool isComparableTo(Type t) const; + /** + * Get the most general base type of this type. + */ + Type getBaseType() const; + /** * Substitution of Types. */ @@ -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()); } -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 t0stack; t0stack.push_back(t0); while(t0stack.back().isPredicateSubtype()){ - t0stack.push_back(t0stack.back().getSubtypeBaseType()); + t0stack.push_back(t0stack.back().getSubtypeParentType()); } std::vector 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() == BOOLEAN_TYPE ) || - ( isPredicateSubtype() && getSubtypeBaseType().isBoolean() ); + ( isPredicateSubtype() && getSubtypeParentType().isBoolean() ); } inline bool TypeNode::isInteger() const { return ( getKind() == kind::TYPE_CONSTANT && getConst() == INTEGER_TYPE ) || isSubrange() || - ( isPredicateSubtype() && getSubtypeBaseType().isInteger() ); + ( isPredicateSubtype() && getSubtypeParentType().isInteger() ); } inline bool TypeNode::isReal() const { return ( getKind() == kind::TYPE_CONSTANT && getConst() == 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() == 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(); }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()); diff --git a/test/unit/expr/type_node_white.h b/test/unit/expr/type_node_white.h index 7d5ac3f51..86f0b192d 100644 --- a/test/unit/expr/type_node_white.h +++ b/test/unit/expr/type_node_white.h @@ -53,7 +53,7 @@ public: delete d_em; } - void testIsComparableTo() { + void testSubtypes() { TypeNode realType = d_nm->realType(); TypeNode integerType = d_nm->realType(); TypeNode booleanType = d_nm->booleanType(); @@ -125,6 +125,16 @@ public: TS_ASSERT( not predicateSubtype.isComparableTo(bvType) ); TS_ASSERT( predicateSubtype.isComparableTo(subrangeType) ); TS_ASSERT( predicateSubtype.isComparableTo(predicateSubtype) ); + + TS_ASSERT(realType.getBaseType() == realType); + TS_ASSERT(integerType.getBaseType() == realType); + TS_ASSERT(booleanType.getBaseType() == booleanType); + TS_ASSERT(arrayType.getBaseType() == arrayType); + TS_ASSERT(bvType.getBaseType() == bvType); + TS_ASSERT(subrangeType.getBaseType() == realType); + TS_ASSERT(predicateSubtype.getBaseType() == realType); + + TS_ASSERT(predicateSubtype.getSubtypeParentType() == integerType); } };/* TypeNodeWhite */