Simplify implementation of subtype methods in TypeNode (#8634)

Also deletes unused data that was used for an inference schema involving subtypes in sets.

diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp
index f48f5a320131f72f665f36433433ade8ea2f4aeb..d7b832c701599208f8a4bf63e3edb62c6add4f2a 100644 (file)
--- a/src/expr/type_node.cpp
+++ b/src/expr/type_node.cpp
@@ -284,22 +284,34 @@ bool TypeNode::isSubtypeOf(TypeNode t) const {
   if(*this == t) {
     return true;
   }
-  if(getKind() == kind::TYPE_CONSTANT) {
-    switch(getConst<TypeConstant>()) {
-    case INTEGER_TYPE:
-      return t.getKind() == kind::TYPE_CONSTANT && t.getConst<TypeConstant>() == REAL_TYPE;
-    default:
-      return false;
-    }
+  if (isInteger())
+  {
+    return t.isReal();
   }
   if (isFunction() && t.isFunction())
   {
-    if (!isComparableTo(t))
+    if (!getRangeType().isSubtypeOf(t.getRangeType()))
+    {
+      // range is not subtype, return false
+      return false;
+    }
+    // must have equal arguments
+    std::vector<TypeNode> t0a = getArgTypes();
+    std::vector<TypeNode> t1a = t.getArgTypes();
+    if (t0a.size() != t1a.size())
     {
-      // incomparable, not subtype
+      // different arities
       return false;
     }
-    return getRangeType().isSubtypeOf(t.getRangeType());
+    for (size_t i = 0, nargs = t0a.size(); i < nargs; i++)
+    {
+      if (t0a[i] != t1a[i])
+      {
+        // an argument is different
+        return false;
+      }
+    }
+    return true;
   }
   // this should only return true for types T1, T2 where we handle equalities between T1 and T2
   // (more cases go here, if we want to support such cases)
@@ -307,18 +319,11 @@ bool TypeNode::isSubtypeOf(TypeNode t) const {
 }
 
 bool TypeNode::isComparableTo(TypeNode t) const {
-  if(*this == t) {
-    return true;
-  }
-  if(isSubtypeOf(NodeManager::currentNM()->realType())) {
-    return t.isSubtypeOf(NodeManager::currentNM()->realType());
-  }
-  if (isFunction() && t.isFunction())
+  if (*this == t)
   {
-    // comparable if they have a common type node
-    return !leastCommonTypeNode(*this, t).isNull();
+    return true;
   }
-  return false;
+  return isSubtypeOf(t) || t.isSubtypeOf(*this);
 }
 
 TypeNode TypeNode::getDatatypeTesterDomainType() const
@@ -486,102 +491,19 @@ bool TypeNode::isParameterInstantiatedDatatype(size_t n) const
 }
 
 TypeNode TypeNode::leastCommonTypeNode(TypeNode t0, TypeNode t1){
-  return commonTypeNode( t0, t1, true );
-}
-
-TypeNode TypeNode::mostCommonTypeNode(TypeNode t0, TypeNode t1){
-  return commonTypeNode( t0, t1, false );
-}
-
-TypeNode TypeNode::commonTypeNode(TypeNode t0, TypeNode t1, bool isLeast) {
-  Assert(!t0.isNull());
-  Assert(!t1.isNull());
-
-  if(__builtin_expect( (t0 == t1), true )) {
+  if (t0 == t1)
+  {
     return t0;
   }
-
-  // t0 != t1 &&
-  if(t0.getKind() == kind::TYPE_CONSTANT) {
-    switch(t0.getConst<TypeConstant>()) {
-    case INTEGER_TYPE:
-      if(t1.isInteger()) {
-        // t0 == IntegerType && t1.isInteger()
-        return t0; //IntegerType
-      } else if(t1.isReal()) {
-        // t0 == IntegerType && t1.isReal() && !t1.isInteger()
-        return isLeast ? t1 : t0; // RealType
-      } else {
-        return TypeNode(); // null type
-      }
-    case REAL_TYPE:
-      if(t1.isReal()) {
-        return isLeast ? t0 : t1; // RealType
-      } else {
-        return TypeNode(); // null type
-      }
-    default:
-      return TypeNode(); // null type
-    }
-  } else if(t1.getKind() == kind::TYPE_CONSTANT) {
-    return commonTypeNode(t1, t0, isLeast); // decrease the number of special cases
+  if (t0.isSubtypeOf(t1))
+  {
+    return t1;
   }
-
-  // t0 != t1 &&
-  // t0.getKind() == kind::TYPE_CONSTANT &&
-  // t1.getKind() == kind::TYPE_CONSTANT
-  switch(t0.getKind()) {
-    case kind::FUNCTION_TYPE:
-    {
-      if (t1.getKind() != kind::FUNCTION_TYPE)
-      {
-        return TypeNode();
-      }
-      // must have equal arguments
-      std::vector<TypeNode> t0a = t0.getArgTypes();
-      std::vector<TypeNode> t1a = t1.getArgTypes();
-      if (t0a.size() != t1a.size())
-      {
-        // different arities
-        return TypeNode();
-      }
-      for (unsigned i = 0, nargs = t0a.size(); i < nargs; i++)
-      {
-        if (t0a[i] != t1a[i])
-        {
-          // an argument is different
-          return TypeNode();
-        }
-      }
-      TypeNode t0r = t0.getRangeType();
-      TypeNode t1r = t1.getRangeType();
-      TypeNode tr = commonTypeNode(t0r, t1r, isLeast);
-      std::vector<TypeNode> ftypes;
-      ftypes.insert(ftypes.end(), t0a.begin(), t0a.end());
-      ftypes.push_back(tr);
-      return NodeManager::currentNM()->mkFunctionType(ftypes);
-    }
-    break;
-    case kind::BITVECTOR_TYPE:
-    case kind::FLOATINGPOINT_TYPE:
-    case kind::SORT_TYPE:
-    case kind::CONSTRUCTOR_TYPE:
-    case kind::SELECTOR_TYPE:
-    case kind::TESTER_TYPE:
-    case kind::ARRAY_TYPE:
-    case kind::DATATYPE_TYPE:
-    case kind::PARAMETRIC_DATATYPE:
-    case kind::SEQUENCE_TYPE:
-    case kind::SET_TYPE:
-    case kind::BAG_TYPE:
-    {
-      // we don't support subtyping except for built in types Int and Real.
-      return TypeNode();  // return null type
-    }
-    default:
-      Unimplemented() << "don't have a commonType for types `" << t0
-                      << "' and `" << t1 << "'";
+  else if (t1.isSubtypeOf(t0))
+  {
+    return t0;
   }
+  return TypeNode();
 }
 
 /** Is this a sort kind */

diff --git a/src/expr/type_node.h b/src/expr/type_node.h
index 9e199472943f90990473a83848abaf8e0753b558..314935da8813af0ca4707acd2a633cf76b6e56c8 100644 (file)
--- a/src/expr/type_node.h
+++ b/src/expr/type_node.h
@@ -697,10 +697,8 @@ private:
    * a TypeNode such that isNull() is true is returned.
    */
   static TypeNode leastCommonTypeNode(TypeNode t0, TypeNode t1);
-  static TypeNode mostCommonTypeNode(TypeNode t0, TypeNode t1);
 
 private:
-  static TypeNode commonTypeNode(TypeNode t0, TypeNode t1, bool isLeast);
 
   /**
    * Indents the given stream a given amount of spaces.

diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index ff68f19ecd80305397fb16db5c5042182fdb61f0..6ac904ed0020de0855ad06ae5a4d366a9b75f141 100644 (file)
--- a/src/theory/sets/theory_sets_private.cpp
+++ b/src/theory/sets/theory_sets_private.cpp
@@ -198,8 +198,6 @@ void TheorySetsPrivate::fullEffortReset()
   Assert(d_equalityEngine->consistent());
   d_fullCheckIncomplete = false;
   d_fullCheckIncompleteId = IncompleteId::UNKNOWN;
-  d_most_common_type.clear();
-  d_most_common_type_term.clear();
   d_card_enabled = false;
   d_rels_enabled = false;
   // reset the state object
@@ -227,19 +225,9 @@ void TheorySetsPrivate::fullEffortCheck()
     while (!eqcs_i.isFinished())
     {
       Node eqc = (*eqcs_i);
-      bool isSet = false;
       TypeNode tn = eqc.getType();
       d_state.registerEqc(tn, eqc);
       eqcTypeCount[tn]++;
-      // common type node and term
-      TypeNode tnc;
-      Node tnct;
-      if (tn.isSet())
-      {
-        isSet = true;
-        tnc = tn.getSetElementType();
-        tnct = eqc;
-      }
       Trace("sets-eqc") << "[" << eqc << "] : ";
       eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc, d_equalityEngine);
       while (!eqc_i.isFinished())
@@ -257,18 +245,6 @@ void TheorySetsPrivate::fullEffortCheck()
           }
         }
         TypeNode tnn = n.getType();
-        if (isSet)
-        {
-          Assert(tnn.isSet());
-          TypeNode tnnel = tnn.getSetElementType();
-          tnc = TypeNode::mostCommonTypeNode(tnc, tnnel);
-          Assert(!tnc.isNull());
-          // update the common type term
-          if (tnc == tnnel)
-          {
-            tnct = n;
-          }
-        }
         // register it with the state
         d_state.registerTerm(eqc, tnn, n);
         Kind nk = n.getKind();
@@ -312,12 +288,6 @@ void TheorySetsPrivate::fullEffortCheck()
         }
         ++eqc_i;
       }
-      if (isSet)
-      {
-        Assert(tnct.getType().getSetElementType() == tnc);
-        d_most_common_type[eqc] = tnc;
-        d_most_common_type_term[eqc] = tnct;
-      }
       Trace("sets-eqc") << std::endl;
       ++eqcs_i;
     }

diff --git a/src/theory/sets/theory_sets_private.h b/src/theory/sets/theory_sets_private.h
index bfdf7a5c056e8a4ee292584e891329277012b67e..2a89b793376044df846562f2d34668392f96f695 100644 (file)
--- a/src/theory/sets/theory_sets_private.h
+++ b/src/theory/sets/theory_sets_private.h
@@ -119,8 +119,6 @@ class TheorySetsPrivate : protected EnvObj
   bool d_fullCheckIncomplete;
   /** The reason we set the above flag to true */
   IncompleteId d_fullCheckIncompleteId;
-  std::map< Node, TypeNode > d_most_common_type;
-  std::map< Node, Node > d_most_common_type_term;
 
  public: