support for SMT-LIBv2 :named attributes, and attributes in general; zero-ary define-fun; several set-info, set-option, get-option, get-info improvementss

2 files changed, 18 insertions, 12 deletions

diff --git a/src/theory/builtin/kinds b/src/theory/builtin/kinds
index 47ee8cbfc..ad442fc2f 100644
--- a/src/theory/builtin/kinds
+++ b/src/theory/builtin/kinds
@@ -119,7 +119,7 @@ constant BUILTIN \
     "The kind of nodes representing built-in operators"
 
 variable FUNCTION "function"
-parameterized APPLY FUNCTION 1: "defined function application"
+parameterized APPLY FUNCTION 0: "defined function application"
 
 operator EQUAL 2 "equality"
 operator DISTINCT 2: "disequality"
diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h
index aee147eff..ec98e61d2 100644
--- a/src/theory/builtin/theory_builtin_type_rules.h
+++ b/src/theory/builtin/theory_builtin_type_rules.h
@@ -37,23 +37,29 @@ class ApplyTypeRule {
     throw (TypeCheckingExceptionPrivate) {
     TNode f = n.getOperator();
     TypeNode fType = f.getType(check);
-    if( !fType.isFunction() ) {
+    if( !fType.isFunction() && n.getNumChildren() > 0 ) {
       throw TypeCheckingExceptionPrivate(n, "operator does not have 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");
+      if(fType.isFunction()) {
+        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");
+          }
+        }
+      } else {
+        if( n.getNumChildren() > 0 ) {
+          throw TypeCheckingExceptionPrivate(n, "number of arguments does not match the function type");
         }
       }
     }
-    return fType.getRangeType();
+    return fType.isFunction() ? fType.getRangeType() : fType;
   }
 };/* class ApplyTypeRule */