declare-sort, define-sort working but not thoroughly tested; define-fun half working (just need to decide where to expand)

2 files changed, 35 insertions, 2 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) {