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, 5 insertions, 3 deletions

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