4 files changed, 44 insertions, 9 deletions
diff --git a/src/theory/builtin/kinds b/src/theory/builtin/kinds
index d3b9d12fb..47ee8cbfc 100644
--- a/src/theory/builtin/kinds
+++ b/src/theory/builtin/kinds
@@ -112,8 +112,14 @@ theory builtin ::CVC4::theory::builtin::TheoryBuiltin "theory_builtin.h"
 # Conceptually, (EQUAL a b) is actually an (APPLY EQUAL a b), but it's
 # not stored that way.  If you ask for the operator of (EQUAL a b),
 # you'll get a special, singleton (BUILTIN EQUAL) Node.
-constant BUILTIN ::CVC4::Kind ::CVC4::kind::KindHashStrategy \
-    "expr/kind.h" "The kind of nodes representing built-in operators"
+constant BUILTIN \
+    ::CVC4::Kind \
+    ::CVC4::kind::KindHashStrategy \
+    "expr/kind.h" \
+    "The kind of nodes representing built-in operators"
+
+variable FUNCTION "function"
+parameterized APPLY FUNCTION 1: "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 2ff92e788..aee147eff 100644
--- a/src/theory/builtin/theory_builtin_type_rules.h
+++ b/src/theory/builtin/theory_builtin_type_rules.h
@@ -31,6 +31,33 @@ namespace CVC4 {
 namespace theory {
 namespace builtin {
 
+class ApplyTypeRule {
+  public:
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+    throw (TypeCheckingExceptionPrivate) {
+    TNode f = n.getOperator();
+    TypeNode fType = f.getType(check);
+    if( !fType.isFunction() ) {
+      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");
+        }
+      }
+    }
+    return fType.getRangeType();
+  }
+};/* class ApplyTypeRule */
+
+
 class EqualityTypeRule {
   public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) throw (TypeCheckingExceptionPrivate) {
diff --git a/src/theory/bv/kinds b/src/theory/bv/kinds
index cc6fe0c20..e7374284e 100644
--- a/src/theory/bv/kinds
+++ b/src/theory/bv/kinds
@@ -17,11 +17,11 @@ constant CONST_BITVECTOR \
     ::CVC4::BitVectorHashStrategy \
     "util/bitvector.h" \
     "a fixed-width bit-vector constant"
-    
+
 operator BITVECTOR_CONCAT 2: "bit-vector concatenation"
 operator BITVECTOR_AND 2 "bitwise and"
-operator BITVECTOR_OR 2 "bitwise or"      
-operator BITVECTOR_XOR 2 "bitwise xor"      
+operator BITVECTOR_OR 2 "bitwise or"
+operator BITVECTOR_XOR 2 "bitwise xor"
 operator BITVECTOR_NOT 2 "bitwise not"
 operator BITVECTOR_NAND 2 "bitwise nand"
 operator BITVECTOR_NOR 2 "bitwise nor"
@@ -31,8 +31,8 @@ operator BITVECTOR_MULT 2 "bit-vector multiplication"
 operator BITVECTOR_PLUS 2 "bit-vector addition"
 operator BITVECTOR_SUB 2 "bit-vector subtraction"
 operator BITVECTOR_NEG 1 "bit-vector unary negation"
-operator BITVECTOR_UDIV 2 "bit-vector unsigned division, truncating towards 0 (undefined if divisor is 0)"    
-operator BITVECTOR_UREM 2 "bit-vector unsigned remainder from truncating division (undefined if divisor is 0)"    
+operator BITVECTOR_UDIV 2 "bit-vector unsigned division, truncating towards 0 (undefined if divisor is 0)"
+operator BITVECTOR_UREM 2 "bit-vector unsigned remainder from truncating division (undefined if divisor is 0)"
 operator BITVECTOR_SDIV 2 "bit-vector 2's complement signed division"
 operator BITVECTOR_SREM 2 "bit-vector 2's complement signed remainder (sign follows dividend)"
 operator BITVECTOR_SMOD 2 "bit-vector 2's complement signed remainder (sign follows divisor)"
@@ -83,7 +83,7 @@ constant BITVECTOR_ROTATE_RIGHT_OP \
 	"::CVC4::UnsignedHashStrategy< ::CVC4::BitVectorRotateRight >" \
 	"util/bitvector.h" \
 	"operator for the bit-vector rotate right"
-	
+
 parameterized BITVECTOR_EXTRACT BITVECTOR_EXTRACT_OP 1 "bit-vector extract"
 parameterized BITVECTOR_REPEAT BITVECTOR_REPEAT_OP 1 "bit-vector repeat"
 parameterized BITVECTOR_ZERO_EXTEND BITVECTOR_ZERO_EXTEND_OP 1 "bit-vector zero-extend"
diff --git a/src/theory/uf/kinds b/src/theory/uf/kinds
index 13cd5e91b..8cd6aec70 100644
--- a/src/theory/uf/kinds
+++ b/src/theory/uf/kinds
@@ -7,4 +7,6 @@
 theory ::CVC4::theory::uf::TheoryUF "theory_uf.h"
 
 parameterized APPLY_UF VARIABLE 1: "uninterpreted function application"
-variable SORT_TYPE "sort type"
+
+variable SORT_TAG "sort tag"
+parameterized SORT_TYPE SORT_TAG 0: "sort type"