This commit adds TypeNode::leastCommonTypeNode(). The special case for arithmetic in TypeNode::operator==() has been removed. A number of faulty type checking checks were switched to use isSubtypeOf. The resolves bug #339

3 files changed, 159 insertions, 7 deletions

diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 2bcf5e18c..00fe6baa8 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -573,9 +573,6 @@ public:
   /** Get the (singleton) type for reals. */
   inline TypeNode realType();
 
-  /** Get the (singleton) type for pseudobooleans. */
-  inline TypeNode pseudobooleanType();
-
   /** Get the (singleton) type for strings. */
   inline TypeNode stringType();
 
diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp
index 3f5c3a032..7b093d11a 100644
--- a/src/expr/type_node.cpp
+++ b/src/expr/type_node.cpp
@@ -181,4 +181,140 @@ bool TypeNode::isParameterInstantiatedDatatype(unsigned n) const {
   return TypeNode::fromType(dt.getParameter(n)) != (*this)[n + 1];
 }
 
+TypeNode TypeNode::leastCommonTypeNode(TypeNode t0, TypeNode t1){
+  Assert( NodeManager::currentNM() != NULL,
+          "There is no current CVC4::NodeManager associated to this thread.\n"
+          "Perhaps a public-facing function is missing a NodeManagerScope ?" );
+
+  Assert(!t0.isNull());
+  Assert(!t1.isNull());
+
+  if(EXPECT_TRUE(t0 == t1)){
+    return t0;
+  }else{ // 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 NodeManager::currentNM()->realType(); // RealType
+        }else{
+          return TypeNode(); //null type
+        }
+      case REAL_TYPE:
+        if(t1.isReal()){
+          return t0; // RealType
+        }else{
+          return TypeNode(); // null type
+        }
+      default:
+        if(t1.isPredicateSubtype() && t1.getSubtypeBaseType().isSubtypeOf(t0)){
+          return t0; // t0 is a constant type
+        }else{
+          return TypeNode(); // null type
+        }
+      }
+    }else if(t1.getKind() == kind::TYPE_CONSTANT){
+      return leastCommonTypeNode(t1, t0); //decrease the number of special cases
+    }else{
+      // t0 != t1 &&
+      // t0.getKind() == kind::TYPE_CONSTANT &&
+      // t1.getKind() == kind::TYPE_CONSTANT
+      switch(t0.getKind()){
+      case kind::ARRAY_TYPE:
+      case kind::BITVECTOR_TYPE:
+      case kind::SORT_TYPE:
+      case kind::PARAMETRIC_DATATYPE:
+      case kind::CONSTRUCTOR_TYPE:
+      case kind::SELECTOR_TYPE:
+      case kind::TESTER_TYPE:
+        if(t1.isPredicateSubtype() && t1.getSubtypeBaseType().isSubtypeOf(t0)){
+          return t0;
+        }else{
+          return TypeNode();
+        }
+      case kind::FUNCTION_TYPE:
+        return TypeNode(); // Not sure if this is right
+      case kind::TUPLE_TYPE:
+        Unimplemented();
+        return TypeNode(); // Not sure if this is right
+      case kind::SUBTYPE_TYPE:
+        if(t1.isPredicateSubtype()){
+          // This is the case where both t0 and t1 are predicate subtypes.
+          return leastCommonPredicateSubtype(t0, t1);
+        }else{ //t0 is a predicate subtype and t1 is not
+          return leastCommonTypeNode(t1, t0); //decrease the number of special cases
+        }
+      case kind::SUBRANGE_TYPE:
+        if(t1.isSubrange()){
+          const SubrangeBounds& t0SR= t0.getSubrangeBounds();
+          const SubrangeBounds& t1SR = t1.getSubrangeBounds();
+          if(SubrangeBounds::joinIsBounded(t0SR, t1SR)){
+            SubrangeBounds j = SubrangeBounds::join(t0SR, t1SR);
+            return NodeManager::currentNM()->mkSubrangeType(j);
+          }else{
+            return NodeManager::currentNM()->integerType();
+          }
+        }else if(t1.isPredicateSubtype()){
+          //t0 is a subrange
+          //t1 is not a subrange
+          //t1 is a predicate subtype
+          if(t1.isInteger()){
+            return NodeManager::currentNM()->integerType();
+          }else if(t1.isReal()){
+            return NodeManager::currentNM()->realType();
+          }else{
+            return TypeNode();
+          }
+        }else{
+          //t0 is a subrange
+          //t1 is not a subrange
+          // t1 is not a type constant && is not a predicate subtype
+          // t1 cannot be real subtype or integer.
+          Assert(t1.isReal());
+          Assert(t1.isInteger());
+          return TypeNode();
+        }
+      default:
+        Unimplemented();
+        return TypeNode();
+      }
+    }
+  }
+}
+
+TypeNode TypeNode::leastCommonPredicateSubtype(TypeNode t0, TypeNode t1){
+  Assert(t0.isPredicateSubtype());
+  Assert(t1.isPredicateSubtype());
+
+  std::vector<TypeNode> t0stack;
+  t0stack.push_back(t0);
+  while(t0stack.back().isPredicateSubtype()){
+    t0stack.push_back(t0stack.back().getSubtypeBaseType());
+  }
+  std::vector<TypeNode> t1stack;
+  t1stack.push_back(t1);
+  while(t1stack.back().isPredicateSubtype()){
+    t1stack.push_back(t1stack.back().getSubtypeBaseType());
+  }
+
+  Assert(!t0stack.empty());
+  Assert(!t1stack.empty());
+
+  if(t0stack.back() == t1stack.back()){
+    TypeNode mostGeneral = t1stack.back();
+    t0stack.pop_back(); t1stack.pop_back();
+    while(!t0stack.empty() && t1stack.empty() && t0stack.back() == t1stack.back()){
+      mostGeneral = t0stack.back();
+      t0stack.pop_back(); t1stack.pop_back();
+    }
+    return mostGeneral;
+  }else{
+    return leastCommonTypeNode(t0stack.back(), t1stack.back());
+  }
+}
+
 }/* CVC4 namespace */
diff --git a/src/expr/type_node.h b/src/expr/type_node.h
index 25b5e4bb3..482da2814 100644
--- a/src/expr/type_node.h
+++ b/src/expr/type_node.h
@@ -159,9 +159,7 @@ public:
    * @return true if expressions are equal, false otherwise
    */
   bool operator==(const TypeNode& typeNode) const {
-    return
-      d_nv == typeNode.d_nv ||
-      (typeNode.isReal() && this->isReal());
+    return d_nv == typeNode.d_nv;
   }
 
   /**
@@ -595,9 +593,25 @@ public:
   /** Is this a kind type (i.e., the type of a type)? */
   bool isKind() const;
 
+
+  /**
+   * Returns the leastUpperBound in the extended type lattice of the two types.
+   * If this is \top, i.e. there is no inhabited type that contains both,
+   * a TypeNode such that isNull() is true is returned.
+   *
+   * For more information see: http://church.cims.nyu.edu/wiki/Cvc4_Type_Lattice
+   */
+  static TypeNode leastCommonTypeNode(TypeNode t0, TypeNode t1);
+
 private:
 
   /**
+   * Returns the leastUpperBound in the extended type lattice of two
+   * predicate subtypes.
+   */
+  static TypeNode leastCommonPredicateSubtype(TypeNode t0, TypeNode t1);
+
+  /**
    * Indents the given stream a given amount of spaces.
    *
    * @param out the stream to indent
@@ -940,7 +954,12 @@ inline unsigned TypeNode::getBitVectorSize() const {
 
 inline const SubrangeBounds& TypeNode::getSubrangeBounds() const {
   Assert(isSubrange());
-  return getConst<SubrangeBounds>();
+  if(getKind() == kind::SUBRANGE_TYPE){
+    return getConst<SubrangeBounds>();
+  }else{
+    Assert(isPredicateSubtype());
+    return getSubtypeBaseType().getSubrangeBounds();
+  }
 }
 
 #ifdef CVC4_DEBUG