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

5 files changed, 22 insertions, 16 deletions

diff --git a/src/theory/arith/theory_arith_type_rules.h b/src/theory/arith/theory_arith_type_rules.h
index 69c98a255..af358b00d 100644
--- a/src/theory/arith/theory_arith_type_rules.h
+++ b/src/theory/arith/theory_arith_type_rules.h
@@ -59,7 +59,7 @@ public:
         }
       }
       if( check ) {
-        if(childType != integerType && childType != realType) {
+        if(!childType.isReal()) {
           throw TypeCheckingExceptionPrivate(n, "expecting an arithmetic subterm");
         }
       }
@@ -73,14 +73,13 @@ public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
       throw (TypeCheckingExceptionPrivate, AssertionException) {
     if( check ) {
-      TypeNode integerType = nodeManager->integerType();
-      TypeNode realType = nodeManager->realType();
       TypeNode lhsType = n[0].getType(check);
-      if (lhsType != integerType && lhsType != realType) {
+      if (!lhsType.isReal()) {
+        std::cout << lhsType << " : " << n[0] << std::endl;
         throw TypeCheckingExceptionPrivate(n, "expecting an arithmetic term on the left-hand-side");
       }
       TypeNode rhsType = n[1].getType(check);
-      if (rhsType != integerType && rhsType != realType) {
+      if (!rhsType.isReal()) {
         throw TypeCheckingExceptionPrivate(n, "expecting an arithmetic term on the right-hand-side");
       }
     }
diff --git a/src/theory/booleans/theory_bool_type_rules.h b/src/theory/booleans/theory_bool_type_rules.h
index 3b30b9f59..ff6b99d77 100644
--- a/src/theory/booleans/theory_bool_type_rules.h
+++ b/src/theory/booleans/theory_bool_type_rules.h
@@ -50,14 +50,16 @@ class IteTypeRule {
   public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
       throw (TypeCheckingExceptionPrivate, AssertionException) {
-    TypeNode iteType = n[1].getType(check);
+    TypeNode thenType = n[1].getType(check);
+    TypeNode elseType = n[2].getType(check);
+    TypeNode iteType = TypeNode::leastCommonTypeNode(thenType, elseType);
     if( check ) {
       TypeNode booleanType = nodeManager->booleanType();
       if (n[0].getType(check) != booleanType) {
         throw TypeCheckingExceptionPrivate(n, "condition of ITE is not Boolean");
       }
-      if (iteType != n[2].getType(check)) {
-        throw TypeCheckingExceptionPrivate(n, "both branches of the ITE must be of the same type");
+      if (iteType.isNull()) {
+        throw TypeCheckingExceptionPrivate(n, "both branches of the ITE must be a subtype of a common type.");
       }
     }
     return iteType;
diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h
index 706196f8b..52d0defd1 100644
--- a/src/theory/builtin/theory_builtin_type_rules.h
+++ b/src/theory/builtin/theory_builtin_type_rules.h
@@ -79,10 +79,10 @@ class EqualityTypeRule {
       TypeNode lhsType = n[0].getType(check);
       TypeNode rhsType = n[1].getType(check);
 
-      if ( lhsType != rhsType ) {
+      if ( TypeNode::leastCommonTypeNode(lhsType, rhsType).isNull() ) {
         std::stringstream ss;
         ss << Expr::setlanguage(language::toOutputLanguage(Options::current()->inputLanguage));
-        ss << "Types do not match in equation:" << std::endl;
+        ss << "Subtypes must have a common type:" << std::endl;
         ss << "Equation: " << n << std::endl;
         ss << "Type 1: " << lhsType << std::endl;
         ss << "Type 2: " << rhsType << std::endl;
@@ -105,9 +105,11 @@ public:
     if( check ) {
       TNode::iterator child_it = n.begin();
       TNode::iterator child_it_end = n.end();
-      TypeNode firstType = (*child_it).getType(check);
+      TypeNode joinType = (*child_it).getType(check);
       for (++child_it; child_it != child_it_end; ++child_it) {
-        if ((*child_it).getType() != firstType) {
+        TypeNode currentType = (*child_it).getType();
+        joinType = TypeNode::leastCommonTypeNode(joinType, currentType);
+        if (joinType.isNull()) {
           throw TypeCheckingExceptionPrivate(n, "Not all arguments are of the same type");
         }
       }
diff --git a/src/theory/datatypes/theory_datatypes_type_rules.h b/src/theory/datatypes/theory_datatypes_type_rules.h
index 347bc16b3..d8d40154a 100644
--- a/src/theory/datatypes/theory_datatypes_type_rules.h
+++ b/src/theory/datatypes/theory_datatypes_type_rules.h
@@ -71,7 +71,8 @@ struct DatatypeConstructorTypeRule {
         for(; child_it != child_it_end; ++child_it, ++tchild_it) {
           TypeNode childType = (*child_it).getType(check);
           Debug("typecheck-idt") << "typecheck cons arg: " << childType << " " << (*tchild_it) << std::endl;
-          if(childType != *tchild_it) {
+          TypeNode argumentType = *tchild_it;
+          if(!childType.isSubtypeOf(argumentType)) {
             throw TypeCheckingExceptionPrivate(n, "bad type for constructor argument");
           }
         }
diff --git a/src/theory/uf/theory_uf_type_rules.h b/src/theory/uf/theory_uf_type_rules.h
index 9b622bc15..3d7e51746 100644
--- a/src/theory/uf/theory_uf_type_rules.h
+++ b/src/theory/uf/theory_uf_type_rules.h
@@ -42,13 +42,15 @@ public:
       TNode::iterator argument_it_end = n.end();
       TypeNode::iterator argument_type_it = fType.begin();
       for(; argument_it != argument_it_end; ++argument_it, ++argument_type_it) {
-        if((*argument_it).getType() != *argument_type_it) {
+        TypeNode currentArgument = (*argument_it).getType();
+        TypeNode currentArgumentType = *argument_type_it;
+        if(!currentArgument.isSubtypeOf(currentArgumentType)) {
           std::stringstream ss;
           ss << Expr::setlanguage(language::toOutputLanguage(Options::current()->inputLanguage))
-             << "argument types do not match the function type:\n"
+             << "argument types is not a subtype of the function's argument type:\n"
              << "argument:  " << *argument_it << "\n"
              << "has type:  " << (*argument_it).getType() << "\n"
-             << "not equal: " << *argument_type_it;
+             << "not subtype: " << *argument_type_it;
           throw TypeCheckingExceptionPrivate(n, ss.str());
         }
       }