Adding optional 'check' parameter to getType() methods

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 */