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

1 files changed, 6 insertions, 4 deletions

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");
         }
       }