diff options
author | Clark Barrett <barrett@cs.nyu.edu> | 2012-11-08 12:21:43 +0000 |
---|---|---|
committer | Clark Barrett <barrett@cs.nyu.edu> | 2012-11-08 12:21:43 +0000 |
commit | 8115182a602848ee7d233b0e4f197289be4fef3c (patch) | |
tree | 44431b965151e3ed236a6484f695d4c50b36fd22 | |
parent | 182f242b6d7a9af3410d4930c98b177c26a8f58b (diff) |
Added getBaseType - Morgan please check
-rw-r--r-- | src/expr/type_node.cpp | 11 | ||||
-rw-r--r-- | src/expr/type_node.h | 3 |
2 files changed, 14 insertions, 0 deletions
diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp index b93ec80c2..80f7f8c76 100644 --- a/src/expr/type_node.cpp +++ b/src/expr/type_node.cpp @@ -119,6 +119,17 @@ TypeNode TypeNode::getSubtypeBaseType() const { return getSubtypePredicate().getType().getArgTypes()[0]; } +TypeNode TypeNode::getBaseType() const { + TypeNode realt = NodeManager::currentNM()->realType(); + if (isSubtypeOf(realt)) { + return realt; + } + else if (isPredicateSubtype()) { + return getSubtypeBaseType(); + } + return *this; +} + std::vector<TypeNode> TypeNode::getArgTypes() const { vector<TypeNode> args; if(isTester()) { diff --git a/src/expr/type_node.h b/src/expr/type_node.h index 88fc70cdc..5f399a855 100644 --- a/src/expr/type_node.h +++ b/src/expr/type_node.h @@ -590,6 +590,9 @@ public: /** Get the base type of this subtype */ TypeNode getSubtypeBaseType() const; + /** Get the most general base type of the type */ + TypeNode getBaseType() const; + /** Is this a subrange */ bool isSubrange() const; |