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 bcf0cd6c1a2a0b3a27402c5c5b50bd9ee87e084c..e64c202b41d65d77bc4d0f845dbecf26b5ca1dab 100644 (file)
--- 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 b3180b958fdcc0a471fcd8d59dece9b0cfdce82f..f8a5f48fe8f32241b6c66a1c5c296810dbcb98e3 100644 (file)
--- 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 80f7f8c7626eac2fe0fed0999ce34d1a54b17214..ae870b1c25c8f38d7f28b49676fa927eadeb19b0 100644 (file)
--- 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 5f399a8554a1ee9d4ebec5c0dd7f18dcda0cf85b..fc142191d5e212c4cb142e3c4a8259f634b8fb0d 100644 (file)
--- 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 195e37154246bd8c20bd5acbe1daf5d95100ad6c..9cc5058cce004bde16a2b799aa1b7a846905b192 100644 (file)
--- 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>());

diff --git a/test/unit/expr/type_node_white.h b/test/unit/expr/type_node_white.h
index 7d5ac3f51760e5c6d61565a61b9fa3bf830600dc..86f0b192ddc0b012b6f148c72143e7267d449d0f 100644 (file)
--- 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 */