Remove subtyping for sets (#5205)

Removed subtyping for sets in type_node.h

Fixes #4502, fixes #4631.

11 files changed, 54 insertions, 119 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 << "'";
   }
 }
 
diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index 18df43e9f..db2f3f22f 100644
--- a/src/theory/sets/theory_sets_private.cpp
+++ b/src/theory/sets/theory_sets_private.cpp
@@ -361,8 +361,6 @@ void TheorySetsPrivate::fullEffortCheck()
         Trace("sets-mem") << std::endl;
       }
     }
-    // check subtypes
-    checkSubtypes();
     d_im.doPendingLemmas();
     if (d_im.hasSent())
     {
@@ -418,49 +416,6 @@ void TheorySetsPrivate::fullEffortCheck()
                 << std::endl;
 }
 
-void TheorySetsPrivate::checkSubtypes()
-{
-  Trace("sets") << "TheorySetsPrivate: check Subtypes..." << std::endl;
-  const std::vector<Node>& sec = d_state.getSetsEqClasses();
-  for (const Node& s : sec)
-  {
-    TypeNode mct = d_most_common_type[s];
-    Assert(!mct.isNull());
-    const std::map<Node, Node>& smems = d_state.getMembers(s);
-    if (!smems.empty())
-    {
-      for (const std::pair<const Node, Node>& it2 : smems)
-      {
-        Trace("sets") << "  check subtype " << it2.first << " " << it2.second
-                      << std::endl;
-        Trace("sets") << "    types : " << it2.first.getType() << " " << mct
-                      << std::endl;
-        if (!it2.first.getType().isSubtypeOf(mct))
-        {
-          Node mctt = d_most_common_type_term[s];
-          Assert(!mctt.isNull());
-          Trace("sets") << "    most common type term is " << mctt << std::endl;
-          std::vector<Node> exp;
-          exp.push_back(it2.second);
-          Assert(d_state.areEqual(mctt, it2.second[1]));
-          exp.push_back(mctt.eqNode(it2.second[1]));
-          Node tc_k = d_treg.getTypeConstraintSkolem(it2.first, mct);
-          if (!tc_k.isNull())
-          {
-            Node etc = tc_k.eqNode(it2.first);
-            d_im.assertInference(etc, exp, "subtype-clash");
-            if (d_state.isInConflict())
-            {
-              return;
-            }
-          }
-        }
-      }
-    }
-  }
-  Trace("sets") << "TheorySetsPrivate: finished." << std::endl;
-}
-
 void TheorySetsPrivate::checkDownwardsClosure()
 {
   Trace("sets") << "TheorySetsPrivate: check downwards closure..." << std::endl;
diff --git a/src/theory/sets/theory_sets_private.h b/src/theory/sets/theory_sets_private.h
index 5ac40515a..8247d4940 100644
--- a/src/theory/sets/theory_sets_private.h
+++ b/src/theory/sets/theory_sets_private.h
@@ -62,19 +62,6 @@ class TheorySetsPrivate {
    */
   void fullEffortReset();
   /**
-   * This ensures that subtype constraints are met for all set terms. In
-   * particular, for a set equivalence class E, let Set(T) be the most
-   * common type among the types of terms in that class. In other words,
-   * if E contains two terms of Set(Int) and Set(Real), then Set(Int) is the
-   * most common type. Then, for each membership x in S where S is a set in
-   * this equivalence class, we ensure x has type T by asserting:
-   *   x = k
-   * for a fresh constant k of type T. This is done only if the type of x is not
-   * a subtype of Int (e.g. if x is of type Real). We call k the "type
-   * constraint skolem for x of type Int".
-   */
-  void checkSubtypes();
-  /**
    * This implements an inference schema based on the "downwards closure" of
    * set membership. This roughly corresponds to the rules UNION DOWN I and II,
    * INTER DOWN I and II from Bansal et al IJCAR 2016, as well as rules for set
diff --git a/src/theory/sets/theory_sets_type_rules.h b/src/theory/sets/theory_sets_type_rules.h
index 20e5e57e2..c5e86f10c 100644
--- a/src/theory/sets/theory_sets_type_rules.h
+++ b/src/theory/sets/theory_sets_type_rules.h
@@ -84,33 +84,26 @@ struct SubsetTypeRule {
   }
 };/* struct SetSubsetTypeRule */
 
-struct MemberTypeRule {
-  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+struct MemberTypeRule
+{
+  inline static TypeNode computeType(NodeManager* nodeManager,
+                                     TNode n,
+                                     bool check)
   {
     Assert(n.getKind() == kind::MEMBER);
     TypeNode setType = n[1].getType(check);
-    if( check ) {
-      if(!setType.isSet()) {
-        throw TypeCheckingExceptionPrivate(n, "checking for membership in a non-set");
+    if (check)
+    {
+      if (!setType.isSet())
+      {
+        throw TypeCheckingExceptionPrivate(
+            n, "checking for membership in a non-set");
       }
       TypeNode elementType = n[0].getType(check);
-      // TODO : still need to be flexible here due to situations like:
-      //
-      // T : (Set Int)
-      // S : (Set Real)
-      // (= (as T (Set Real)) S)
-      // (member 0.5 S)
-      // ...where (member 0.5 T) is inferred
-      //
-      // or
-      //
-      // S : (Set Real)
-      // (not (member 0.5 s))
-      // (member 0.0 s)
-      // ...find model M where M( s ) = { 0 }, check model will generate (not (member 0.5 (singleton 0)))
-      //      
-      if(!elementType.isComparableTo(setType.getSetElementType())) {
-      //if(!elementType.isSubtypeOf(setType.getSetElementType())) {     //FIXME:typing
+      // e.g. (member 1 (singleton 1.0)) is true whereas
+      // (member 1.0 (singleton 1)) throws a typing error
+      if (!elementType.isSubtypeOf(setType.getSetElementType()))
+      {
         std::stringstream ss;
         ss << "member operating on sets of different types:\n"
            << "child type:  " << elementType << "\n"
@@ -121,7 +114,7 @@ struct MemberTypeRule {
     }
     return nodeManager->booleanType();
   }
-};/* struct MemberTypeRule */
+}; /* struct MemberTypeRule */
 
 struct SingletonTypeRule
 {
diff --git a/test/regress/regress0/sets/int-real-univ-unsat.smt2 b/test/regress/regress0/sets/int-real-univ-unsat.smt2
index 56f7e8c5e..19b5850fa 100644
--- a/test/regress/regress0/sets/int-real-univ-unsat.smt2
+++ b/test/regress/regress0/sets/int-real-univ-unsat.smt2
@@ -1,13 +1,13 @@
 ; COMMAND-LINE: --sets-ext
-; EXPECT: unsat
+; EXPECT: sat
 (set-logic ALL)
-(set-info :status unsat)
+(set-info :status sat)
 
 (declare-fun a () (Set Real))
 
 (declare-fun x () Real)
 
-(assert (= (as univset (Set Real)) (as univset (Set Int))))
+(assert (= (as univset (Set Real)) (as univset (Set Real))))
 
 (assert (member x a))
 
diff --git a/test/regress/regress0/sets/int-real-univ.smt2 b/test/regress/regress0/sets/int-real-univ.smt2
index afe20b92f..e7d79bbf6 100644
--- a/test/regress/regress0/sets/int-real-univ.smt2
+++ b/test/regress/regress0/sets/int-real-univ.smt2
@@ -7,7 +7,7 @@
 
 (declare-fun x () Real)
 
-(assert (= (as univset (Set Real)) (as univset (Set Int))))
+(assert (= (as univset (Set Real)) (as univset (Set Real))))
 
 (assert (member x a))
 
diff --git a/test/regress/regress0/sets/sets-of-sets-subtypes.smt2 b/test/regress/regress0/sets/sets-of-sets-subtypes.smt2
index 86a1d93b4..e8c98e09c 100644
--- a/test/regress/regress0/sets/sets-of-sets-subtypes.smt2
+++ b/test/regress/regress0/sets/sets-of-sets-subtypes.smt2
@@ -1,10 +1,10 @@
 (set-logic QF_LIRAFS)
-(set-info :status unsat)
+(set-info :status sat)
 
 (declare-fun s () (Set (Set Real)))
-(declare-fun t () (Set (Set Int)))
+(declare-fun t () (Set (Set Real)))
 
-(declare-fun x () (Set Int))
+(declare-fun x () (Set Real))
 (declare-fun y () (Set Real))
 
 (assert (member 0.5 y))
diff --git a/test/regress/regress0/sets/sets-poly-nonint.smt2 b/test/regress/regress0/sets/sets-poly-nonint.smt2
index a0e883ace..58ff563bc 100644
--- a/test/regress/regress0/sets/sets-poly-nonint.smt2
+++ b/test/regress/regress0/sets/sets-poly-nonint.smt2
@@ -1,6 +1,6 @@
 (set-logic QF_UFLIRAFS)
-(set-info :status unsat)
-(declare-fun s () (Set Int))
+(set-info :status sat)
+(declare-fun s () (Set Real))
 (declare-fun t () (Set Real))
 (declare-fun r () (Set Real))
 (declare-fun u () (Set Real))
diff --git a/test/unit/api/python/test_sort.py b/test/unit/api/python/test_sort.py
index 12fec6c91..cff92ca8d 100644
--- a/test/unit/api/python/test_sort.py
+++ b/test/unit/api/python/test_sort.py
@@ -347,6 +347,9 @@ def testSortSubtyping():
 
     setSortI = solver.mkSetSort(intSort)
     setSortR = solver.mkSetSort(realSort)
-    # we support subtyping for sets
-    assert setSortI.isSubsortOf(setSortR)
-    assert setSortR.isComparableTo(setSortI)
+    # we don't support subtyping for sets
+    assert not setSortI.isComparableTo(setSortR)
+    assert not setSortI.isSubsortOf(setSortR)
+    assert not setSortR.isComparableTo(setSortI)
+    assert not setSortR.isSubsortOf(setSortI)
+
diff --git a/test/unit/api/sort_black.h b/test/unit/api/sort_black.h
index 32108bf84..53563f833 100644
--- a/test/unit/api/sort_black.h
+++ b/test/unit/api/sort_black.h
@@ -372,7 +372,9 @@ void SortBlack::testSortSubtyping()
 
   Sort setSortI = d_solver.mkSetSort(intSort);
   Sort setSortR = d_solver.mkSetSort(realSort);
-  // we support subtyping for sets
-  TS_ASSERT(setSortI.isSubsortOf(setSortR));
-  TS_ASSERT(setSortR.isComparableTo(setSortI));
+  // we don't support subtyping for sets
+  TS_ASSERT(!setSortI.isComparableTo(setSortR));
+  TS_ASSERT(!setSortI.isSubsortOf(setSortR));
+  TS_ASSERT(!setSortR.isComparableTo(setSortI));
+  TS_ASSERT(!setSortR.isSubsortOf(setSortI));
 }
diff --git a/test/unit/theory/theory_sets_type_rules_white.h b/test/unit/theory/theory_sets_type_rules_white.h
index 06f5608c8..c098ca9b8 100644
--- a/test/unit/theory/theory_sets_type_rules_white.h
+++ b/test/unit/theory/theory_sets_type_rules_white.h
@@ -41,6 +41,16 @@ class SetsTypeRuleWhite : public CxxTest::TestSuite
     d_em.reset();
   }
 
+  void testIsisComparableTo()
+  {
+    TypeNode setRealType = d_nm->mkSetType(d_nm->realType());
+    TypeNode setIntType = d_nm->mkSetType(d_nm->integerType());
+    TS_ASSERT(!setIntType.isComparableTo(setRealType));
+    TS_ASSERT(!setIntType.isSubtypeOf(setRealType));
+    TS_ASSERT(!setRealType.isComparableTo(setIntType));
+    TS_ASSERT(!setRealType.isComparableTo(setIntType));
+  }
+
   void testSingletonTerm()
   {
     Sort realSort = d_slv->getRealSort();