diff options
Diffstat (limited to 'src/theory/builtin')
-rw-r--r-- | src/theory/builtin/theory_builtin_type_rules.h | 10 |
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"); } } |