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/uf | |
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/uf')
-rw-r--r-- | src/theory/uf/theory_uf_type_rules.h | 8 |
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()); } } |