From: Clark Barrett <barrett@cs.nyu.edu>
Date: Thu, 8 Nov 2012 12:21:43 +0000 (+0000)
Subject: Added getBaseType - Morgan please check
X-Git-Tag: cvc5-1.0.0~7643
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=8115182a602848ee7d233b0e4f197289be4fef3c;p=cvc5.git

Added getBaseType - Morgan please check
---

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;