diff options
author | Tim King <taking@cs.nyu.edu> | 2012-05-18 23:48:38 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2012-05-18 23:48:38 +0000 |
commit | ea8139dc7b727bf48bd7b7c6b169d763618a1f2a (patch) | |
tree | 95701608122c2a6e232ee22979e9da757bf4e2dd /src/theory/builtin | |
parent | 3b93d45dab9513195d5604a069423ed13e173f49 (diff) |
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
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"); } } |