Eliminate use of subtypes from remainder of type rules (#8756)

This PR should be added before the minor release that advertises our policy change for subtyping.

diff --git a/src/expr/type_matcher.cpp b/src/expr/type_matcher.cpp
index bfcce31d79ebc8c4c41c40a99caa64bac6670cc4..c5257b7e16f54be3d622d8273f4ed87b9f559139 100644 (file)
--- a/src/expr/type_matcher.cpp
+++ b/src/expr/type_matcher.cpp
@@ -75,15 +75,13 @@ bool TypeMatcher::doMatching(TypeNode pattern, TypeNode tn)
     if (!d_match[index].isNull())
     {
       Trace("typecheck-idt")
-          << "check subtype " << tn << " " << d_match[index] << std::endl;
-      TypeNode tnn = TypeNode::leastCommonTypeNode(tn, d_match[index]);
-      // recognize subtype relation
-      if (!tnn.isNull())
+          << "check types " << tn << " " << d_match[index] << std::endl;
+      if (tn != d_match[index])
       {
-        d_match[index] = tnn;
-        return true;
+        return false;
       }
-      return false;
+      d_match[index] = tn;
+      return true;
     }
     d_match[index] = tn;
     return true;

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 8f879916f90e093b9b1d9f82c96da208012bfa30..49e0ed5256ef09bd5d5faed8d1e4c01a2eb6968c 100644 (file)
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -94,7 +94,7 @@ static void toStreamRational(std::ostream& out,
   }
   else
   {
-    Assert (isReal);
+    Assert(isReal);
     out << "(/ ";
     if (neg)
     {

diff --git a/src/theory/arith/theory_arith_type_rules.cpp b/src/theory/arith/theory_arith_type_rules.cpp
index b709e2d6a4fc0d78222a6b89996489087223dd0f..b60a9b8b83001554381b8a4863e403d8ed4e0a77 100644 (file)
--- a/src/theory/arith/theory_arith_type_rules.cpp
+++ b/src/theory/arith/theory_arith_type_rules.cpp
@@ -110,18 +110,12 @@ TypeNode ArithRelationTypeRule::computeType(NodeManager* nodeManager,
   if (check)
   {
     Assert(n.getNumChildren() == 2);
-    TypeNode t1 = n[0].getType(check);
-    if (!t1.isRealOrInt())
+    if (!n[0].getType(check).isRealOrInt()
+        || !n[1].getType(check).isRealOrInt())
     {
       throw TypeCheckingExceptionPrivate(
           n, "expecting an arithmetic term for arithmetic relation");
     }
-    TypeNode t2 = n[1].getType(check);
-    if (!t1.isComparableTo(t2))
-    {
-      throw TypeCheckingExceptionPrivate(
-          n, "expecting arithmetic terms of comparable type");
-    }
   }
   return nodeManager->booleanType();
 }

diff --git a/src/theory/arrays/theory_arrays_type_rules.cpp b/src/theory/arrays/theory_arrays_type_rules.cpp
index a5ec7e15cf1bb855e0e1d11c3ffa6ea0c057a5b6..14987fbfe209f4f6d41e804f9215d25966eb0759 100644 (file)
--- a/src/theory/arrays/theory_arrays_type_rules.cpp
+++ b/src/theory/arrays/theory_arrays_type_rules.cpp
@@ -40,7 +40,7 @@ TypeNode ArraySelectTypeRule::computeType(NodeManager* nodeManager,
                                          "array select operating on non-array");
     }
     TypeNode indexType = n[1].getType(check);
-    if (!indexType.isSubtypeOf(arrayType.getArrayIndexType()))
+    if (indexType != arrayType.getArrayIndexType())
     {
       throw TypeCheckingExceptionPrivate(
           n, "array select not indexed with correct type for array");
@@ -197,13 +197,13 @@ TypeNode ArrayTableFunTypeRule::computeType(NodeManager* nodeManager,
                                          "array table fun arg 1 is non-array");
     }
     TypeNode indexType = n[2].getType(check);
-    if (!indexType.isComparableTo(arrayType.getArrayIndexType()))
+    if (indexType != arrayType.getArrayIndexType())
     {
       throw TypeCheckingExceptionPrivate(
           n, "array table fun arg 2 does not match type of array");
     }
     indexType = n[3].getType(check);
-    if (!indexType.isComparableTo(arrayType.getArrayIndexType()))
+    if (indexType != arrayType.getArrayIndexType())
     {
       throw TypeCheckingExceptionPrivate(
           n, "array table fun arg 3 does not match type of array");

diff --git a/src/theory/bags/theory_bags_type_rules.cpp b/src/theory/bags/theory_bags_type_rules.cpp
index 5ca0f081538a008b416c379b69ab38f79f0982a0..4e3da85f50218e1b9b338f74d12f4b1fd438ccfe 100644 (file)
--- a/src/theory/bags/theory_bags_type_rules.cpp
+++ b/src/theory/bags/theory_bags_type_rules.cpp
@@ -88,11 +88,8 @@ TypeNode SubBagTypeRule::computeType(NodeManager* nodeManager,
     TypeNode secondBagType = n[1].getType(check);
     if (secondBagType != bagType)
     {
-      if (!bagType.isComparableTo(secondBagType))
-      {
-        throw TypeCheckingExceptionPrivate(
-            n, "BAG_SUBBAG operating on bags of different types");
-      }
+      throw TypeCheckingExceptionPrivate(
+          n, "BAG_SUBBAG operating on bags of different types");
     }
   }
   return nodeManager->booleanType();
@@ -114,12 +111,12 @@ TypeNode CountTypeRule::computeType(NodeManager* nodeManager,
     TypeNode elementType = n[0].getType(check);
     // e.g. (bag.count 1 (bag (BagMakeOp Real) 1.0 3))) is 3 whereas
     // (bag.count 1.0 (bag (BagMakeOp Int) 1 3)) throws a typing error
-    if (!elementType.isSubtypeOf(bagType.getBagElementType()))
+    if (elementType != bagType.getBagElementType())
     {
       std::stringstream ss;
       ss << "member operating on bags of different types:\n"
          << "child type:  " << elementType << "\n"
-         << "not subtype: " << bagType.getBagElementType() << "\n"
+         << "not type: " << bagType.getBagElementType() << "\n"
          << "in term : " << n;
       throw TypeCheckingExceptionPrivate(n, ss.str());
     }
@@ -143,12 +140,12 @@ TypeNode MemberTypeRule::computeType(NodeManager* nodeManager,
     TypeNode elementType = n[0].getType(check);
     // e.g. (bag.member 1 (bag 1.0 1)) is true whereas
     // (bag.member 1.0 (bag 1 1)) throws a typing error
-    if (!elementType.isSubtypeOf(bagType.getBagElementType()))
+    if (elementType != bagType.getBagElementType())
     {
       std::stringstream ss;
       ss << "member operating on bags of different types:\n"
          << "child type:  " << elementType << "\n"
-         << "not subtype: " << bagType.getBagElementType() << "\n"
+         << "not type: " << bagType.getBagElementType() << "\n"
          << "in term : " << n;
       throw TypeCheckingExceptionPrivate(n, ss.str());
     }
@@ -201,11 +198,11 @@ TypeNode BagMakeTypeRule::computeType(NodeManager* nm, TNode n, bool check)
     TypeNode actualElementType = n[0].getType(check);
     // the type of the element should be a subtype of the type of the operator
     // e.g. (bag (bag_op Real) 1 1) where 1 is an Int
-    if (!actualElementType.isSubtypeOf(expectedElementType))
+    if (actualElementType != expectedElementType)
     {
       std::stringstream ss;
       ss << "The type '" << actualElementType
-         << "' of the element is not a subtype of '" << expectedElementType
+         << "' of the element is not type of '" << expectedElementType
          << "' in term : " << n;
       throw TypeCheckingExceptionPrivate(n, ss.str());
     }
@@ -486,9 +483,8 @@ TypeNode BagPartitionTypeRule::computeType(NodeManager* nodeManager,
     }
     std::vector<TypeNode> argTypes = functionType.getArgTypes();
     TypeNode rangeType = functionType.getRangeType();
-    if (!(argTypes.size() == 2 && elementType.isSubtypeOf(argTypes[0])
-          && elementType.isSubtypeOf(argTypes[1])
-          && rangeType == nm->booleanType()))
+    if (!(argTypes.size() == 2 && elementType == argTypes[0]
+          && elementType == argTypes[1] && rangeType == nm->booleanType()))
     {
       std::stringstream ss;
       ss << "Operator " << n.getKind() << " expects a function of type  (-> "

diff --git a/src/theory/datatypes/theory_datatypes_type_rules.cpp b/src/theory/datatypes/theory_datatypes_type_rules.cpp
index 94aebbc63eef660256b3638b6b15f333d7da6bde..1a8c622257f7698ef1711105ff0aa34127d22181 100644 (file)
--- a/src/theory/datatypes/theory_datatypes_type_rules.cpp
+++ b/src/theory/datatypes/theory_datatypes_type_rules.cpp
@@ -87,12 +87,12 @@ TypeNode DatatypeConstructorTypeRule::computeType(NodeManager* nodeManager,
         Trace("typecheck-idt") << "typecheck cons arg: " << childType << " "
                                << (*tchild_it) << std::endl;
         TypeNode argumentType = *tchild_it;
-        if (!childType.isSubtypeOf(argumentType))
+        if (childType != argumentType)
         {
           std::stringstream ss;
           ss << "bad type for constructor argument:\n"
              << "child type:  " << childType << "\n"
-             << "not subtype: " << argumentType << "\n"
+             << "not type: " << argumentType << "\n"
              << "in term : " << n;
           throw TypeCheckingExceptionPrivate(n, ss.str());
         }
@@ -161,7 +161,7 @@ TypeNode DatatypeSelectorTypeRule::computeType(NodeManager* nodeManager,
       Trace("typecheck-idt") << "typecheck sel: " << n << std::endl;
       Trace("typecheck-idt") << "sel type: " << selType << std::endl;
       TypeNode childType = n[0].getType(check);
-      if (!selType[0].isComparableTo(childType))
+      if (selType[0] != childType)
       {
         Trace("typecheck-idt") << "ERROR: " << selType[0].getKind() << " "
                                << childType.getKind() << std::endl;
@@ -203,7 +203,7 @@ TypeNode DatatypeTesterTypeRule::computeType(NodeManager* nodeManager,
     {
       Trace("typecheck-idt") << "typecheck test: " << n << std::endl;
       Trace("typecheck-idt") << "test type: " << testType << std::endl;
-      if (!testType[0].isComparableTo(childType))
+      if (testType[0] != childType)
       {
         throw TypeCheckingExceptionPrivate(n, "bad type for tester argument");
       }
@@ -238,12 +238,9 @@ TypeNode DatatypeUpdateTypeRule::computeType(NodeManager* nodeManager,
               "matching failed for update argument of parameterized datatype");
         }
       }
-      else
+      else if (targ != childType)
       {
-        if (!targ.isComparableTo(childType))
-        {
-          throw TypeCheckingExceptionPrivate(n, "bad type for update argument");
-        }
+        throw TypeCheckingExceptionPrivate(n, "bad type for update argument");
       }
     }
   }
@@ -368,7 +365,7 @@ TypeNode DtSygusEvalTypeRule::computeType(NodeManager* nodeManager,
     {
       TypeNode vtype = svl[i].getType(check);
       TypeNode atype = n[i + 1].getType(check);
-      if (!vtype.isComparableTo(atype))
+      if (vtype != atype)
       {
         throw TypeCheckingExceptionPrivate(
             n,
@@ -464,14 +461,10 @@ TypeNode MatchTypeRule::computeType(NodeManager* nodeManager,
     {
       retType = currType;
     }
-    else
+    else if (retType != currType)
     {
-      retType = TypeNode::leastCommonTypeNode(retType, currType);
-      if (retType.isNull())
-      {
-        throw TypeCheckingExceptionPrivate(
-            n, "incomparable types in match case list");
-      }
+      throw TypeCheckingExceptionPrivate(
+          n, "incomparable types in match case list");
     }
   }
   // it is mandatory to check this here to ensure the match is exhaustive

diff --git a/src/theory/sets/theory_sets_type_rules.cpp b/src/theory/sets/theory_sets_type_rules.cpp
index f97f7c7fcf69840a179c92392a41b8a94d726621..fe10f303a881e603d26721cf3b6daf32efc761ce 100644 (file)
--- a/src/theory/sets/theory_sets_type_rules.cpp
+++ b/src/theory/sets/theory_sets_type_rules.cpp
@@ -78,11 +78,8 @@ TypeNode SubsetTypeRule::computeType(NodeManager* nodeManager,
     TypeNode secondSetType = n[1].getType(check);
     if (secondSetType != setType)
     {
-      if (!setType.isComparableTo(secondSetType))
-      {
-        throw TypeCheckingExceptionPrivate(
-            n, "set subset operating on sets of different types");
-      }
+      throw TypeCheckingExceptionPrivate(
+          n, "set subset operating on sets of different types");
     }
   }
   return nodeManager->booleanType();
@@ -104,12 +101,12 @@ TypeNode MemberTypeRule::computeType(NodeManager* nodeManager,
     TypeNode elementType = n[0].getType(check);
     // e.g. (member 1 (singleton 1.0)) is true whereas
     // (member 1.0 (singleton 1)) throws a typing error
-    if (!elementType.isSubtypeOf(setType.getSetElementType()))
+    if (elementType != setType.getSetElementType())
     {
       std::stringstream ss;
       ss << "member operating on sets of different types:\n"
          << "child type:  " << elementType << "\n"
-         << "not subtype: " << setType.getSetElementType() << "\n"
+         << "not type: " << setType.getSetElementType() << "\n"
          << "in term : " << n;
       throw TypeCheckingExceptionPrivate(n, ss.str());
     }
@@ -129,13 +126,12 @@ TypeNode SingletonTypeRule::computeType(NodeManager* nodeManager,
   if (check)
   {
     TypeNode type2 = n[0].getType(check);
-    TypeNode leastCommonType = TypeNode::leastCommonTypeNode(type1, type2);
     // the type of the element should be a subtype of the type of the operator
     // e.g. (set.singleton (SetSingletonOp Real) 1) where 1 is an Int
-    if (leastCommonType.isNull() || leastCommonType != type1)
+    if (type1 != type2)
     {
       std::stringstream ss;
-      ss << "The type '" << type2 << "' of the element is not a subtype of '"
+      ss << "The type '" << type2 << "' of the element is not a type of '"
          << type1 << "' in term : " << n;
       throw TypeCheckingExceptionPrivate(n, ss.str());
     }

diff --git a/src/theory/strings/theory_strings_type_rules.cpp b/src/theory/strings/theory_strings_type_rules.cpp
index 5e47283a4b9af1964a7c98cba2d341bba7cbf927..01adb7e3ad756df00eb429e07aa914e1671d164c 100644 (file)
--- a/src/theory/strings/theory_strings_type_rules.cpp
+++ b/src/theory/strings/theory_strings_type_rules.cpp
@@ -336,10 +336,10 @@ TypeNode SeqUnitTypeRule::computeType(NodeManager* nodeManager,
     TypeNode argType = n[0].getType(check);
     // the type of the element should be a subtype of the type of the operator
     // e.g. (seq.unit (SeqUnitOp Real) 1) where 1 is an Int
-    if (!argType.isSubtypeOf(otype))
+    if (argType != otype)
     {
       std::stringstream ss;
-      ss << "The type '" << argType << "' of the element is not a subtype of '"
+      ss << "The type '" << argType << "' of the element is not the type of '"
          << otype << "' in term : " << n;
       throw TypeCheckingExceptionPrivate(n, ss.str());
     }

diff --git a/src/theory/uf/theory_uf_type_rules.cpp b/src/theory/uf/theory_uf_type_rules.cpp
index 84a54025f9a4d3160bd357d8d33c18b33cb8bfd3..9a0a66a3fcf26ca0094d860c740241b4aea49a3d 100644 (file)
--- a/src/theory/uf/theory_uf_type_rules.cpp
+++ b/src/theory/uf/theory_uf_type_rules.cpp
@@ -131,7 +131,7 @@ TypeNode HoApplyTypeRule::computeType(NodeManager* nodeManager,
   if (check)
   {
     TypeNode aType = n[1].getType(check);
-    if (!aType.isSubtypeOf(fType[0]))
+    if (aType != fType[0])
     {
       throw TypeCheckingExceptionPrivate(
           n, "argument does not match function type");