ArrayStoreAll infrastructure

3 files changed, 26 insertions, 5 deletions

diff --git a/src/expr/type.cpp b/src/expr/type.cpp
index df222b684..bd8e29a44 100644
--- a/src/expr/type.cpp
+++ b/src/expr/type.cpp
@@ -77,6 +77,16 @@ Expr Type::mkGroundTerm() const {
   return d_typeNode->mkGroundTerm().toExpr();
 }
 
+bool Type::isSubtypeOf(Type t) const {
+  NodeManagerScope nms(d_nodeManager);
+  return d_typeNode->isSubtypeOf(*t.d_typeNode);
+}
+
+bool Type::isComparableTo(Type t) const {
+  NodeManagerScope nms(d_nodeManager);
+  return d_typeNode->isComparableTo(*t.d_typeNode);
+}
+
 Type& Type::operator=(const Type& t) {
   Assert(d_typeNode != NULL, "Unexpected NULL typenode pointer!");
   Assert(t.d_typeNode != NULL, "Unexpected NULL typenode pointer!");
diff --git a/src/expr/type.h b/src/expr/type.h
index a813aec02..bd6a6a298 100644
--- a/src/expr/type.h
+++ b/src/expr/type.h
@@ -145,8 +145,7 @@ public:
   Cardinality getCardinality() const;
 
   /**
-   * Is this a well-founded type?  (I.e., do there exist ground
-   * terms?)
+   * Is this a well-founded type?
    */
   bool isWellFounded() const;
 
@@ -157,6 +156,17 @@ public:
   Expr mkGroundTerm() const;
 
   /**
+   * Is this type a subtype of the given type?
+   */
+  bool isSubtypeOf(Type t) const;
+
+  /**
+   * Is this type comparable to the given type (i.e., do they share
+   * a common ancestor in the subtype tree)?
+   */
+  bool isComparableTo(Type t) const;
+
+  /**
    * Substitution of Types.
    */
   Type substitute(const Type& type, const Type& replacement) const;
diff --git a/src/expr/type_node.h b/src/expr/type_node.h
index bfbedde88..83bbb25a7 100644
--- a/src/expr/type_node.h
+++ b/src/expr/type_node.h
@@ -430,8 +430,7 @@ public:
   Cardinality getCardinality() const;
 
   /**
-   * Returns whether this type is well-founded.  A type is
-   * well-founded if there exist ground terms.
+   * Returns whether this type is well-founded.
    *
    * @return true iff the type is well-founded
    */
@@ -445,7 +444,9 @@ public:
    */
   Node mkGroundTerm() const;
 
-  /** Is this type a subtype of the given type? */
+  /**
+   * Is this type a subtype of the given type?
+   */
   bool isSubtypeOf(TypeNode t) const;
 
   /**