diff options
author | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-07-27 20:54:33 +0000 |
---|---|---|
committer | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-07-27 20:54:33 +0000 |
commit | 2564d8730f768a8305325d4b6cc08211d8a3281d (patch) | |
tree | 56abf63023e3ffdadde2e7747dd2db7661962664 /src/theory/uf | |
parent | 62ec86743289b26241d69b1701d4b3f547ee2bed (diff) |
Adding optional 'check' parameter to getType() methods
Diffstat (limited to 'src/theory/uf')
-rw-r--r-- | src/theory/uf/theory_uf_type_rules.h | 26 |
1 files changed, 16 insertions, 10 deletions
diff --git a/src/theory/uf/theory_uf_type_rules.h b/src/theory/uf/theory_uf_type_rules.h index f09a44d50..38018112a 100644 --- a/src/theory/uf/theory_uf_type_rules.h +++ b/src/theory/uf/theory_uf_type_rules.h @@ -27,20 +27,26 @@ namespace uf { class UfTypeRule { public: - inline static TypeNode computeType(NodeManager* nodeManager, TNode n) + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) throw (TypeCheckingExceptionPrivate) { TNode f = n.getOperator(); - TypeNode fType = f.getType(); - if (n.getNumChildren() != fType.getNumChildren() - 1) { - throw TypeCheckingExceptionPrivate(n, "number of arguments does not match the function type"); + TypeNode fType = f.getType(check); + if( !fType.isFunction() ) { + throw TypeCheckingExceptionPrivate(n, "operator does not have function type"); } - TNode::iterator argument_it = n.begin(); - TNode::iterator argument_it_end = n.end(); - TypeNode::iterator argument_type_it = fType.begin(); - for(; argument_it != argument_it_end; ++argument_it) - if((*argument_it).getType() != *argument_type_it) { - throw TypeCheckingExceptionPrivate(n, "argument types do not match the function type"); + if( check ) { + if (n.getNumChildren() != fType.getNumChildren() - 1) { + throw TypeCheckingExceptionPrivate(n, "number of arguments does not match the function type"); } + TNode::iterator argument_it = n.begin(); + TNode::iterator argument_it_end = n.end(); + TypeNode::iterator argument_type_it = fType.begin(); + for(; argument_it != argument_it_end; ++argument_it) { + if((*argument_it).getType() != *argument_type_it) { + throw TypeCheckingExceptionPrivate(n, "argument types do not match the function type"); + } + } + } return fType.getRangeType(); } };/* class UfTypeRule */ |