Remove subtyping for sets (#5205)

Removed subtyping for sets in type_node.h

Fixes #4502, fixes #4631.

1 files changed, 8 insertions, 23 deletions

diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp
index cbfb57747..659b1eef2 100644
--- a/src/expr/type_node.cpp
+++ b/src/expr/type_node.cpp
@@ -318,9 +318,6 @@ bool TypeNode::isSubtypeOf(TypeNode t) const {
       return false;
     }
   }
-  if(isSet() && t.isSet()) {
-    return getSetElementType().isSubtypeOf(t.getSetElementType());
-  }
   if (isFunction() && t.isFunction())
   {
     if (!isComparableTo(t))
@@ -342,9 +339,6 @@ bool TypeNode::isComparableTo(TypeNode t) const {
   if(isSubtypeOf(NodeManager::currentNM()->realType())) {
     return t.isSubtypeOf(NodeManager::currentNM()->realType());
   }
-  if(isSet() && t.isSet()) {
-    return getSetElementType().isComparableTo(t.getSetElementType());
-  }
   if (isFunction() && t.isFunction())
   {
     // comparable if they have a common type node
@@ -583,24 +577,15 @@ TypeNode TypeNode::commonTypeNode(TypeNode t0, TypeNode t1, bool isLeast) {
     case kind::SEQUENCE_TYPE: return TypeNode();
     case kind::SET_TYPE:
     {
-      // take the least common subtype of element types
-      TypeNode elementType;
-      if (t1.isSet()
-          && !(elementType = commonTypeNode(t0[0], t1[0], isLeast)).isNull())
-      {
-        return NodeManager::currentNM()->mkSetType(elementType);
-      }
-      else
-      {
-        return TypeNode();
-      }
+      // we don't support subtyping for sets
+      return TypeNode(); // return null type
     }
-  case kind::SEXPR_TYPE:
-    Unimplemented()
-        << "haven't implemented leastCommonType for symbolic expressions yet";
-  default:
-    Unimplemented() << "don't have a commonType for types `" << t0 << "' and `"
-                    << t1 << "'";
+    case kind::SEXPR_TYPE:
+      Unimplemented()
+          << "haven't implemented leastCommonType for symbolic expressions yet";
+    default:
+      Unimplemented() << "don't have a commonType for types `" << t0
+                      << "' and `" << t1 << "'";
   }
 }