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

30 files changed, 956 insertions, 337 deletions

diff --git a/src/context/cdmap.h b/src/context/cdmap.h
index 76c05fd4d..1e7e931da 100644
--- a/src/context/cdmap.h
+++ b/src/context/cdmap.h
@@ -92,20 +92,19 @@
 #ifndef __CVC4__CONTEXT__CDMAP_H
 #define __CVC4__CONTEXT__CDMAP_H
 
-#include "context/context.h"
-#include "util/Assert.h"
-
 #include <vector>
 #include <iterator>
 #include <ext/hash_map>
 
+#include "context/context.h"
+#include "util/Assert.h"
+#include "context/cdmap_forward.h"
+
 namespace CVC4 {
 namespace context {
 
 // Auxiliary class: almost the same as CDO (see cdo.h)
 
-template <class Key, class Data, class HashFcn = __gnu_cxx::hash<Key> > class CDMap;
-
 template <class Key, class Data, class HashFcn = __gnu_cxx::hash<Key> >
 class CDOmap : public ContextObj {
   friend class CDMap<Key, Data, HashFcn>;
diff --git a/src/context/cdmap_forward.h b/src/context/cdmap_forward.h
new file mode 100644
index 000000000..1024f0b54
--- /dev/null
+++ b/src/context/cdmap_forward.h
@@ -0,0 +1,42 @@
+/*********************                                                        */
+/*! \file cdmap_forward.h
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief This is a forward declaration header to declare the CDMap<>
+ ** template
+ **
+ ** This is a forward declaration header to declare the CDMap<>
+ ** template.  It's useful if you want to forward-declare CDMap<>
+ ** without including the full cdmap.h header, for example, in a
+ ** public header context.
+ **
+ ** For CDMap<> in particular, it's difficult to forward-declare it
+ ** yourself, becase it has a default template argument.
+ **/
+
+#include "cvc4_public.h"
+
+#ifndef __CVC4__CONTEXT__CDMAP_FORWARD_H
+#define __CVC4__CONTEXT__CDMAP_FORWARD_H
+
+namespace __gnu_cxx {
+  template <class Key> class hash;
+}/* __gnu_cxx namespace */
+
+namespace CVC4 {
+  namespace context {
+    template <class Key, class Data, class HashFcn = __gnu_cxx::hash<Key> >
+    class CDMap;
+  }/* CVC4::context namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__CONTEXT__CDMAP_FORWARD_H */
diff --git a/src/context/cdset.h b/src/context/cdset.h
index 7032f76ba..47848c26f 100644
--- a/src/context/cdset.h
+++ b/src/context/cdset.h
@@ -34,6 +34,23 @@ class CDSet : protected CDMap<V, V, HashFcn> {
 
 public:
 
+  // ensure these are publicly accessible
+  static void* operator new(size_t size, bool b) {
+    return ContextObj::operator new(size, b);
+  }
+
+  static void operator delete(void* pMem, bool b) {
+    return ContextObj::operator delete(pMem, b);
+  }
+
+  void deleteSelf() {
+    this->ContextObj::deleteSelf();
+  }
+
+  static void operator delete(void* pMem) {
+    AlwaysAssert(false, "It is not allowed to delete a ContextObj this way!");
+  }
+
   CDSet(Context* context) :
     super(context) {
   }
diff --git a/src/expr/Makefile.am b/src/expr/Makefile.am
index 5f2453898..50ce4141e 100644
--- a/src/expr/Makefile.am
+++ b/src/expr/Makefile.am
@@ -26,7 +26,8 @@ libexpr_la_SOURCES = \
 	command.cpp \
 	declaration_scope.h \
 	declaration_scope.cpp \
-	expr_manager_scope.h 
+	expr_manager_scope.h \
+	sort.h
 nodist_libexpr_la_SOURCES = \
 	kind.h \
 	metakind.h \
diff --git a/src/expr/declaration_scope.cpp b/src/expr/declaration_scope.cpp
index edc4c5fa8..bd128267a 100644
--- a/src/expr/declaration_scope.cpp
+++ b/src/expr/declaration_scope.cpp
@@ -11,69 +11,162 @@
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
- ** \brief Convenience class for scoping variable and type declarations (implementation).
+ ** \brief Convenience class for scoping variable and type
+ ** declarations (implementation).
  **
- ** Convenience class for scoping variable and type declarations (implementation)
+ ** Convenience class for scoping variable and type declarations
+ ** (implementation).
  **/
 
-#include "declaration_scope.h"
-#include "expr.h"
-#include "type.h"
-
+#include "expr/declaration_scope.h"
+#include "expr/expr.h"
+#include "expr/type.h"
 #include "context/cdmap.h"
+#include "context/cdset.h"
 #include "context/context.h"
 
 #include <string>
+#include <utility>
 
-namespace CVC4 {
+using namespace CVC4;
+using namespace CVC4::context;
+using namespace std;
 
-using namespace context;
+namespace CVC4 {
 
 DeclarationScope::DeclarationScope() :
-  d_context(new Context()),
-  d_exprMap(new (true) CDMap<std::string,Expr,StringHashFunction>(d_context)),
-  d_typeMap(new (true) CDMap<std::string,Type,StringHashFunction>(d_context)) {
+  d_context(new Context),
+  d_exprMap(new(true) CDMap<std::string, Expr, StringHashFunction>(d_context)),
+  d_typeMap(new(true) CDMap<std::string, pair<vector<Type>, Type>, StringHashFunction>(d_context)),
+  d_functions(new(true) CDSet<Expr, ExprHashFunction>(d_context)) {
 }
 
 DeclarationScope::~DeclarationScope() {
   d_exprMap->deleteSelf();
   d_typeMap->deleteSelf();
+  d_functions->deleteSelf();
   delete d_context;
 }
 
-void DeclarationScope::bind(const std::string& name, const Expr& obj) throw () {
-  d_exprMap->insert(name,obj);
+void DeclarationScope::bind(const std::string& name, Expr obj) throw() {
+  d_exprMap->insert(name, obj);
 }
 
-bool DeclarationScope::isBound(const std::string& name) const throw () {
+void DeclarationScope::bindDefinedFunction(const std::string& name, Expr obj) throw() {
+  d_exprMap->insert(name, obj);
+  d_functions->insert(obj);
+}
+
+bool DeclarationScope::isBound(const std::string& name) const throw() {
   return d_exprMap->find(name) != d_exprMap->end();
 }
 
-Expr DeclarationScope::lookup(const std::string& name) const throw () {
+bool DeclarationScope::isBoundDefinedFunction(const std::string& name) const throw() {
+  CDMap<std::string, Expr, StringHashFunction>::iterator found =
+    d_exprMap->find(name);
+  return found != d_exprMap->end() && d_functions->contains((*found).second);
+}
+
+Expr DeclarationScope::lookup(const std::string& name) const throw(AssertionException) {
   return (*d_exprMap->find(name)).second;
 }
 
-void DeclarationScope::bindType(const std::string& name, const Type& t) throw () {
-  d_typeMap->insert(name,t);
+void DeclarationScope::bindType(const std::string& name, Type t) throw() {
+  d_typeMap->insert(name, make_pair(vector<Type>(), t));
 }
 
-bool DeclarationScope::isBoundType(const std::string& name) const throw () {
+void DeclarationScope::bindType(const std::string& name,
+                                const vector<Type>& params,
+                                Type t) throw() {
+  if(Debug.isOn("sort")) {
+    Debug("sort") << "bindType(" << name << ", [";
+    if(params.size() > 0) {
+      copy( params.begin(), params.end() - 1,
+            ostream_iterator<Type>(Debug("sort"), ", ") );
+      Debug("sort") << params.back();
+    }
+    Debug("sort") << "], " << t << ")" << endl;
+  }
+  d_typeMap->insert(name, make_pair(params, t));
+}
+
+bool DeclarationScope::isBoundType(const std::string& name) const throw() {
   return d_typeMap->find(name) != d_typeMap->end();
 }
 
-Type DeclarationScope::lookupType(const std::string& name) const throw () {
-  return (*d_typeMap->find(name)).second;
+Type DeclarationScope::lookupType(const std::string& name) const throw(AssertionException) {
+  pair<vector<Type>, Type> p = (*d_typeMap->find(name)).second;
+  Assert(p.first.size() == 0,
+         "type constructor arity is wrong: "
+         "`%s' requires %u parameters but was provided 0",
+         name.c_str(), p.first.size());
+  return p.second;
 }
 
+Type DeclarationScope::lookupType(const std::string& name,
+                                  const vector<Type>& params) const throw(AssertionException) {
+  pair<vector<Type>, Type> p = (*d_typeMap->find(name)).second;
+  Assert(p.first.size() == params.size(),
+         "type constructor arity is wrong: "
+         "`%s' requires %u parameters but was provided %u",
+         name.c_str(), p.first.size(), params.size());
+  if(p.first.size() == 0) {
+    Assert(p.second.isSort());
+    return p.second;
+  }
+  if(p.second.isSortConstructor()) {
+    if(Debug.isOn("sort")) {
+      Debug("sort") << "instantiating using a sort constructor" << endl;
+      Debug("sort") << "have formals [";
+      copy( p.first.begin(), p.first.end() - 1,
+            ostream_iterator<Type>(Debug("sort"), ", ") );
+      Debug("sort") << p.first.back() << "]" << endl
+                    << "parameters   [";
+      copy( params.begin(), params.end() - 1,
+            ostream_iterator<Type>(Debug("sort"), ", ") );
+      Debug("sort") << params.back() << "]" << endl
+                    << "type ctor    " << name << endl
+                    << "type is      " << p.second << endl;
+    }
+
+    Type instantiation =
+      SortConstructorType(p.second).instantiate(params);
+
+    Debug("sort") << "instance is  " << instantiation << endl;
+
+    return instantiation;
+  } else {
+    Assert(p.second.isSort());
+    if(Debug.isOn("sort")) {
+      Debug("sort") << "instantiating using a sort substitution" << endl;
+      Debug("sort") << "have formals [";
+      copy( p.first.begin(), p.first.end() - 1,
+            ostream_iterator<Type>(Debug("sort"), ", ") );
+      Debug("sort") << p.first.back() << "]" << endl
+                    << "parameters   [";
+      copy( params.begin(), params.end() - 1,
+            ostream_iterator<Type>(Debug("sort"), ", ") );
+      Debug("sort") << params.back() << "]" << endl
+                    << "type ctor    " << name << endl
+                    << "type is      " << p.second << endl;
+    }
+
+    Type instantiation = p.second.substitute(p.first, params);
+
+    Debug("sort") << "instance is  " << instantiation << endl;
+
+    return instantiation;
+  }
+}
 
-void DeclarationScope::popScope() throw (ScopeException) {
+void DeclarationScope::popScope() throw(ScopeException) {
   if( d_context->getLevel() == 0 ) {
     throw ScopeException();
   }
   d_context->pop();
 }
 
-void DeclarationScope::pushScope() throw () {
+void DeclarationScope::pushScope() throw() {
   d_context->push();
 }
 
diff --git a/src/expr/declaration_scope.h b/src/expr/declaration_scope.h
index 74869bae7..a402a9139 100644
--- a/src/expr/declaration_scope.h
+++ b/src/expr/declaration_scope.h
@@ -19,6 +19,8 @@
 #ifndef DECLARATION_SCOPE_H
 #define DECLARATION_SCOPE_H
 
+#include <vector>
+#include <utility>
 #include <ext/hash_map>
 
 #include "expr/expr.h"
@@ -29,16 +31,17 @@ namespace CVC4 {
 class Type;
 
 namespace context {
+  class Context;
 
-class Context;
+  template <class Key, class Data, class HashFcn>
+  class CDMap;
 
-template <class Key, class Data, class HashFcn>
-class CDMap;
-
-} //namespace context
+  template <class V, class HashFcn>
+  class CDSet;
+}/* CVC4::context namespace */
 
 class CVC4_PUBLIC ScopeException : public Exception {
-};
+};/* class ScopeException */
 
 /**
  * A convenience class for handling scoped declarations. Implements the usual
@@ -50,10 +53,13 @@ class CVC4_PUBLIC DeclarationScope {
   context::Context *d_context;
 
   /** A map for expressions. */
-  context::CDMap<std::string,Expr,StringHashFunction> *d_exprMap;
+  context::CDMap<std::string, Expr, StringHashFunction> *d_exprMap;
 
   /** A map for types. */
-  context::CDMap<std::string,Type,StringHashFunction> *d_typeMap;
+  context::CDMap<std::string, std::pair<std::vector<Type>, Type>, StringHashFunction> *d_typeMap;
+
+  /** A set of defined functions. */
+  context::CDSet<Expr, ExprHashFunction> *d_functions;
 
 public:
   /** Create a declaration scope. */
@@ -62,68 +68,119 @@ public:
   /** Destroy a declaration scope. */
   ~DeclarationScope();
 
-  /** Bind an expression to a name in the current scope level.
-   * If <code>name</code> is already bound in the current level, then the
+  /**
+   * Bind an expression to a name in the current scope level.  If
+   * <code>name</code> is already bound in the current level, then the
    * binding is replaced. If <code>name</code> is bound in a previous
-   * level, then the binding is "covered" by this one until the current
-   * scope is popped.
+   * level, then the binding is "covered" by this one until the
+   * current scope is popped.
    *
    * @param name an identifier
    * @param obj the expression to bind to <code>name</code>
    */
-  void bind(const std::string& name, const Expr& obj) throw ();
-
-  /** Bind a type to a name in the current scope.
-   * If <code>name</code> is already bound to a type in the current level,
-   * then the binding is replaced. If <code>name</code> is bound in a
-   * previous level, then the binding is "covered" by this one until the
-   * current scope is popped.
+  void bind(const std::string& name, Expr obj) throw();
+
+  /**
+   * Bind a type to a name in the current scope.  If <code>name</code>
+   * is already bound to a type in the current level, then the binding
+   * is replaced. If <code>name</code> is bound in a previous level,
+   * then the binding is "covered" by this one until the current scope
+   * is popped.
+   *
+   * @param name an identifier
+   * @param t the type to bind to <code>name</code>
+   */
+  void bindDefinedFunction(const std::string& name, Expr obj) throw();
+
+  /**
+   * Bind a type to a name in the current scope.  If <code>name</code>
+   * is already bound to a type in the current level, then the binding
+   * is replaced. If <code>name</code> is bound in a previous level,
+   * then the binding is "covered" by this one until the current scope
+   * is popped.
+   *
+   * @param name an identifier
+   * @param t the type to bind to <code>name</code>
+   */
+  void bindType(const std::string& name, Type t) throw();
+
+  /**
+   * Bind a type to a name in the current scope.  If <code>name</code>
+   * is already bound to a type or type constructor in the current
+   * level, then the binding is replaced. If <code>name</code> is
+   * bound in a previous level, then the binding is "covered" by this
+   * one until the current scope is popped.
    *
    * @param name an identifier
    * @param t the type to bind to <code>name</code>
    */
-  void bindType(const std::string& name, const Type& t) throw ();
+  void bindType(const std::string& name,
+                const std::vector<Type>& params,
+                Type t) throw();
 
-  /** Check whether a name is bound to an expression.
+  /**
+   * Check whether a name is bound to an expression with either bind()
+   * or bindDefinedFunction().
    *
    * @param name the identifier to check.
    * @returns true iff name is bound in the current scope.
    */
-  bool isBound(const std::string& name) const throw ();
+  bool isBound(const std::string& name) const throw();
+
+  /**
+   * Check whether a name was bound to a function with bindDefinedFunction().
+   */
+  bool isBoundDefinedFunction(const std::string& name) const throw();
 
-  /** Check whether a name is bound to a type.
+  /**
+   * Check whether a name is bound to a type (or type constructor).
    *
    * @param name the identifier to check.
    * @returns true iff name is bound to a type in the current scope.
    */
-  bool isBoundType(const std::string& name) const throw ();
+  bool isBoundType(const std::string& name) const throw();
 
-  /** Lookup a bound expression.
+  /**
+   * Lookup a bound expression.
    *
    * @param name the identifier to lookup
    * @returns the expression bound to <code>name</code> in the current scope.
    */
-  Expr lookup(const std::string& name) const throw ();
+  Expr lookup(const std::string& name) const throw(AssertionException);
 
-  /** Lookup a bound type.
+  /**
+   * Lookup a bound type.
    *
-   * @param name the identifier to lookup
+   * @param name the type identifier to lookup
    * @returns the type bound to <code>name</code> in the current scope.
    */
-  Type lookupType(const std::string& name) const throw ();
+  Type lookupType(const std::string& name) const throw(AssertionException);
 
-  /** Pop a scope level. Deletes all bindings since the last call to
+  /**
+   * Lookup a bound parameterized type.
+   *
+   * @param name the type-constructor identifier to lookup
+   * @param params the types to use to parameterize the type
+   * @returns the type bound to <code>name(<i>params</i>)</code> in
+   * the current scope.
+   */
+  Type lookupType(const std::string& name,
+                  const std::vector<Type>& params) const throw(AssertionException);
+
+  /**
+   * Pop a scope level. Deletes all bindings since the last call to
    * <code>pushScope</code>. Calls to <code>pushScope</code> and
    * <code>popScope</code> must be "properly nested." I.e., a call to
    * <code>popScope</code> is only legal if the number of prior calls to
    * <code>pushScope</code> on this <code>DeclarationScope</code> is strictly
    * greater than then number of prior calls to <code>popScope</code>. */
-  void popScope() throw (ScopeException);
+  void popScope() throw(ScopeException);
 
   /** Push a scope level. */
-  void pushScope() throw ();
+  void pushScope() throw();
+
 };/* class DeclarationScope */
 
-}/* namespace CVC4 */
+}/* CVC4 namespace */
 
 #endif /* DECLARATION_SCOPE_H */
diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index 56b89c125..55b59d13c 100644
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -88,11 +88,11 @@ Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2) {
                 minArity(kind), maxArity(kind), n);
   NodeManagerScope nms(d_nodeManager);
   try {
-    return Expr(this, d_nodeManager->mkNodePtr(kind, 
+    return Expr(this, d_nodeManager->mkNodePtr(kind,
                                                child1.getNode(),
                                                child2.getNode()));
   } catch (const TypeCheckingExceptionPrivate& e) {
-    throw TypeCheckingException(Expr(this, new Node(e.getNode())), 
+    throw TypeCheckingException(Expr(this, new Node(e.getNode())),
                                 e.getMessage());
   }
 }
@@ -107,12 +107,12 @@ Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2,
                 minArity(kind), maxArity(kind), n);
   NodeManagerScope nms(d_nodeManager);
   try {
-    return Expr(this, d_nodeManager->mkNodePtr(kind, 
-                                               child1.getNode(), 
-                                               child2.getNode(), 
+    return Expr(this, d_nodeManager->mkNodePtr(kind,
+                                               child1.getNode(),
+                                               child2.getNode(),
                                                child3.getNode()));
   } catch (const TypeCheckingExceptionPrivate& e) {
-    throw TypeCheckingException(Expr(this, new Node(e.getNode())), 
+    throw TypeCheckingException(Expr(this, new Node(e.getNode())),
                                 e.getMessage());
   }
 }
@@ -127,13 +127,13 @@ Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2,
                 minArity(kind), maxArity(kind), n);
   NodeManagerScope nms(d_nodeManager);
   try {
-    return Expr(this, d_nodeManager->mkNodePtr(kind, 
+    return Expr(this, d_nodeManager->mkNodePtr(kind,
                                                child1.getNode(),
-                                               child2.getNode(), 
+                                               child2.getNode(),
                                                child3.getNode(),
                                                child4.getNode()));
   } catch (const TypeCheckingExceptionPrivate& e) {
-    throw TypeCheckingException(Expr(this, new Node(e.getNode())), 
+    throw TypeCheckingException(Expr(this, new Node(e.getNode())),
                                 e.getMessage());
   }
 }
@@ -149,14 +149,14 @@ Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2,
                 minArity(kind), maxArity(kind), n);
   NodeManagerScope nms(d_nodeManager);
   try {
-    return Expr(this, d_nodeManager->mkNodePtr(kind, 
+    return Expr(this, d_nodeManager->mkNodePtr(kind,
                                                child1.getNode(),
-                                               child2.getNode(), 
+                                               child2.getNode(),
                                                child3.getNode(),
                                                child4.getNode(),
                                                child5.getNode()));
   } catch (const TypeCheckingExceptionPrivate& e) {
-    throw TypeCheckingException(Expr(this, new Node(e.getNode())), 
+    throw TypeCheckingException(Expr(this, new Node(e.getNode())),
                                 e.getMessage());
   }
 }
@@ -181,7 +181,7 @@ Expr ExprManager::mkExpr(Kind kind, const std::vector<Expr>& children) {
   try {
     return Expr(this, d_nodeManager->mkNodePtr(kind, nodes));
   } catch (const TypeCheckingExceptionPrivate& e) {
-    throw TypeCheckingException(Expr(this, new Node(e.getNode())), 
+    throw TypeCheckingException(Expr(this, new Node(e.getNode())),
                                 e.getMessage());
   }
 }
@@ -219,8 +219,8 @@ FunctionType ExprManager::mkFunctionType(const Type& domain, const Type& range)
 
 /** Make a function type with input types from argTypes. */
 FunctionType ExprManager::mkFunctionType(const std::vector<Type>& argTypes, const Type& range) {
-  Assert( argTypes.size() >= 1 );
   NodeManagerScope nms(d_nodeManager);
+  Assert( argTypes.size() >= 1 );
   std::vector<TypeNode> argTypeNodes;
   for (unsigned i = 0, i_end = argTypes.size(); i < i_end; ++ i) {
     argTypeNodes.push_back(*argTypes[i].d_typeNode);
@@ -229,8 +229,8 @@ FunctionType ExprManager::mkFunctionType(const std::vector<Type>& argTypes, cons
 }
 
 FunctionType ExprManager::mkFunctionType(const std::vector<Type>& sorts) {
-  Assert( sorts.size() >= 2 );
   NodeManagerScope nms(d_nodeManager);
+  Assert( sorts.size() >= 2 );
   std::vector<TypeNode> sortNodes;
   for (unsigned i = 0, i_end = sorts.size(); i < i_end; ++ i) {
      sortNodes.push_back(*sorts[i].d_typeNode);
@@ -239,8 +239,8 @@ FunctionType ExprManager::mkFunctionType(const std::vector<Type>& sorts) {
 }
 
 FunctionType ExprManager::mkPredicateType(const std::vector<Type>& sorts) {
-  Assert( sorts.size() >= 1 );
   NodeManagerScope nms(d_nodeManager);
+  Assert( sorts.size() >= 1 );
   std::vector<TypeNode> sortNodes;
   for (unsigned i = 0, i_end = sorts.size(); i < i_end; ++ i) {
      sortNodes.push_back(*sorts[i].d_typeNode);
@@ -249,8 +249,8 @@ FunctionType ExprManager::mkPredicateType(const std::vector<Type>& sorts) {
 }
 
 TupleType ExprManager::mkTupleType(const std::vector<Type>& types) {
-  Assert( types.size() >= 2 );
   NodeManagerScope nms(d_nodeManager);
+  Assert( types.size() >= 2 );
   std::vector<TypeNode> typeNodes;
   for (unsigned i = 0, i_end = types.size(); i < i_end; ++ i) {
      typeNodes.push_back(*types[i].d_typeNode);
@@ -268,9 +268,16 @@ ArrayType ExprManager::mkArrayType(Type indexType, Type constituentType) const {
   return Type(d_nodeManager, new TypeNode(d_nodeManager->mkArrayType(*indexType.d_typeNode, *constituentType.d_typeNode)));
 }
 
-SortType ExprManager::mkSort(const std::string& name, size_t arity) const {
+SortType ExprManager::mkSort(const std::string& name) const {
+  NodeManagerScope nms(d_nodeManager);
+  return Type(d_nodeManager, new TypeNode(d_nodeManager->mkSort(name)));
+}
+
+SortConstructorType ExprManager::mkSortConstructor(const std::string& name,
+                                                   size_t arity) const {
   NodeManagerScope nms(d_nodeManager);
-  return Type(d_nodeManager, new TypeNode(d_nodeManager->mkSort(name, arity)));
+  return Type(d_nodeManager,
+              new TypeNode(d_nodeManager->mkSortConstructor(name, arity)));
 }
 
 /**
@@ -295,7 +302,7 @@ SortType ExprManager::mkSort(const std::string& name, size_t arity) const {
  * amount of checking required to return a valid result.
  *
  * @param n the Expr for which we want a type
- * @param check whether we should check the type as we compute it 
+ * @param check whether we should check the type as we compute it
  * (default: false)
  */
 Type ExprManager::getType(const Expr& e, bool check) throw (TypeCheckingException) {
@@ -333,7 +340,7 @@ Expr ExprManager::mkAssociative(Kind kind,
   /* If the number of children is within bounds, then there's nothing to do. */
   if( numChildren <= max ) {
     return mkExpr(kind,children);
-  } 
+  }
 
   std::vector<Expr>::const_iterator it = children.begin() ;
   std::vector<Expr>::const_iterator end = children.end() ;
@@ -379,7 +386,7 @@ Expr ExprManager::mkAssociative(Kind kind,
 
   /* It would be really weird if this happened (it would require
    * min > 2, for one thing), but let's make sure. */
-  AlwaysAssert( newChildren.size() >= min, 
+  AlwaysAssert( newChildren.size() >= min,
                 "Too few new children in mkAssociative" );
 
   return Expr(this, d_nodeManager->mkNodePtr(kind,newChildren) );
diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h
index 316a9b7b1..92d039bd3 100644
--- a/src/expr/expr_manager_template.h
+++ b/src/expr/expr_manager_template.h
@@ -173,7 +173,8 @@ public:
   template <class T>
   Expr mkConst(const T&);
 
-  /** Create an Expr by applying an associative operator to the children.
+  /**
+   * Create an Expr by applying an associative operator to the children.
    * If <code>children.size()</code> is greater than the max arity for
    * <code>kind</code>, then the expression will be broken up into
    * suitably-sized chunks, taking advantage of the associativity of
@@ -224,8 +225,16 @@ public:
   /** Make the type of arrays with the given parameterization */
   ArrayType mkArrayType(Type indexType, Type constituentType) const;
 
-  /** Make a new sort with the given name and arity. */
-  SortType mkSort(const std::string& name, size_t arity = 0) const;
+  /** Make a new sort with the given name. */
+  SortType mkSort(const std::string& name) const;
+
+  /** Make a new sort from a constructor */
+  SortType mkSort(SortConstructorType constructor,
+                  const std::vector<TypeNode>& children) const;
+
+  /** Make a sort constructor from a name and arity */
+  SortConstructorType mkSortConstructor(const std::string& name,
+                                        size_t arity) const;
 
   /** Get the type of an expression */
   Type getType(const Expr& e, bool check = false)
diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp
index 83d5dc47f..803808b0f 100644
--- a/src/expr/expr_template.cpp
+++ b/src/expr/expr_template.cpp
@@ -151,6 +151,12 @@ bool Expr::operator>(const Expr& e) const {
   return *d_node > *e.d_node;
 }
 
+unsigned Expr::getId() const {
+  ExprManagerScope ems(*this);
+  Assert(d_node != NULL, "Unexpected NULL expression pointer!");
+  return d_node->getId();
+}
+
 Kind Expr::getKind() const {
   ExprManagerScope ems(*this);
   Assert(d_node != NULL, "Unexpected NULL expression pointer!");
diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h
index fee8e70db..8fab13b37 100644
--- a/src/expr/expr_template.h
+++ b/src/expr/expr_template.h
@@ -75,6 +75,7 @@ public:
 
   /**
    * Get the Expr that caused the type-checking to fail.
+   *
    * @return the expr
    */
   Expr getExpression() const;
@@ -103,6 +104,7 @@ protected:
 
   /**
    * Constructor for internal purposes.
+   *
    * @param em the expression manager that handles this expression
    * @param node the actual expression node pointer
    */
@@ -115,6 +117,7 @@ public:
 
   /**
    * Copy constructor, makes a copy of a given expression
+   *
    * @param e the expression to copy
    */
   Expr(const Expr& e);
@@ -134,6 +137,7 @@ public:
    * Assignment operator, makes a copy of the given expression. If the
    * expression managers of the two expressions differ, the expression of
    * the given expression will be used.
+   *
    * @param e the expression to assign
    * @return the reference to this expression after assignment
    */
@@ -142,13 +146,15 @@ public:
   /**
    * Syntactic comparison operator. Returns true if expressions belong to the
    * same expression manager and are syntactically identical.
+   *
    * @param e the expression to compare to
    * @return true if expressions are syntactically the same, false otherwise
    */
   bool operator==(const Expr& e) const;
 
   /**
-   * Syntactic dis-equality operator.
+   * Syntactic disequality operator.
+   *
    * @param e the expression to compare to
    * @return true if expressions differ syntactically, false otherwise
    */
@@ -160,6 +166,7 @@ public:
    * ordering than all the expressions created later. Null expression is the
    * smallest element of the ordering. The behavior of the operator is
    * undefined if the expressions come from two different expression managers.
+   *
    * @param e the expression to compare to
    * @return true if this expression is smaller than the given one
    */
@@ -171,6 +178,7 @@ public:
    * ordering than all the expressions created later. Null expression is the
    * smallest element of the ordering. The behavior of the operator is
    * undefined if the expressions come from two different expression managers.
+   *
    * @param e the expression to compare to
    * @return true if this expression is greater than the given one
    */
@@ -182,6 +190,7 @@ public:
    * ordering than all the expressions created later. Null expression is the
    * smallest element of the ordering. The behavior of the operator is
    * undefined if the expressions come from two different expression managers.
+   *
    * @param e the expression to compare to
    * @return true if this expression is smaller or equal to the given one
    */
@@ -193,25 +202,37 @@ public:
    * ordering than all the expressions created later. Null expression is the
    * smallest element of the ordering. The behavior of the operator is
    * undefined if the expressions come from two different expression managers.
+   *
    * @param e the expression to compare to
    * @return true if this expression is greater or equal to the given one
    */
   bool operator>=(const Expr& e) const { return !(*this < e); }
 
   /**
+   * Get the ID of this expression (used for the comparison operators).
+   *
+   * @return an identifier uniquely identifying the value this
+   * expression holds.
+   */
+  unsigned getId() const;
+
+  /**
    * Returns the kind of the expression (AND, PLUS ...).
+   *
    * @return the kind of the expression
    */
   Kind getKind() const;
 
   /**
    * Returns the number of children of this expression.
+   *
    * @return the number of children
    */
   size_t getNumChildren() const;
 
   /**
    * Returns the i'th child of this expression.
+   *
    * @param i the index of the child to retrieve
    * @return the child
    */
@@ -219,12 +240,14 @@ public:
 
   /**
    * Check if this is an expression that has an operator.
+   *
    * @return true if this expression has an operator
    */
   bool hasOperator() const;
 
   /**
    * Get the operator of this expression.
+   *
    * @throws IllegalArgumentException if it has no operator
    * @return the operator of this expression
    */
@@ -599,6 +622,13 @@ inline std::ostream& operator<<(std::ostream& out, ExprPrintTypes pt) {
 
 }/* CVC4::expr namespace */
 
+// for hash_maps, hash_sets..
+struct ExprHashFunction {
+  size_t operator()(CVC4::Expr e) const {
+    return (size_t) e.getId();
+  }
+};/* struct ExprHashFunction */
+
 }/* CVC4 namespace */
 
 #endif /* __CVC4__EXPR_H */
diff --git a/src/expr/mkmetakind b/src/expr/mkmetakind
index 89e2861d6..aaecff800 100755
--- a/src/expr/mkmetakind
+++ b/src/expr/mkmetakind
@@ -227,7 +227,7 @@ function register_metakind {
     exit 1
   fi
 
-  if [ $mk = OPERATOR -o $mk = PARAMETERIZED ]; then
+  if [ $mk = OPERATOR ] || [ $mk = PARAMETERIZED -a "$k" != SORT_TYPE ]; then
     if [ $lb = 0 ]; then
       echo "$kf:$lineno: error in range \`$nc' for \`$k': $mk-kinded kinds must always take at least one child" >&2
       exit 1
diff --git a/src/expr/node.cpp b/src/expr/node.cpp
index 6b689034a..d9933689d 100644
--- a/src/expr/node.cpp
+++ b/src/expr/node.cpp
@@ -25,17 +25,18 @@ using namespace std;
 
 namespace CVC4 {
 
-TypeCheckingExceptionPrivate::TypeCheckingExceptionPrivate(TNode node, std::string message)
-: Exception(message), d_node(new Node(node))
-{
+TypeCheckingExceptionPrivate::TypeCheckingExceptionPrivate(TNode node,
+                                                           string message) :
+  Exception(message),
+  d_node(new Node(node)) {
 }
 
 TypeCheckingExceptionPrivate::~TypeCheckingExceptionPrivate() throw () {
   delete d_node;
 }
 
-std::string TypeCheckingExceptionPrivate::toString() const {
-  std::stringstream ss;
+string TypeCheckingExceptionPrivate::toString() const {
+  stringstream ss;
   ss << "Error type-checking " << d_node << ": " << d_msg;
   return ss.str();
 }
diff --git a/src/expr/node.h b/src/expr/node.h
index b5f6307ed..67d46a977 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -342,11 +342,14 @@ public:
   /**
    * Returns a node representing the operator of this expression.
    * If this is an APPLY, then the operator will be a functional term.
-   * Otherwise, it will be a node with kind BUILTIN
+   * Otherwise, it will be a node with kind BUILTIN.
    */
   NodeTemplate<true> getOperator() const;
 
-  /** Returns true if the node has an operator (i.e., it's not a variable or a constant). */
+  /**
+   * Returns true if the node has an operator (i.e., it's not a
+   * variable or a constant).
+   */
   inline bool hasOperator() const;
 
   /**
@@ -721,14 +724,14 @@ struct NodeHashFunction {
   size_t operator()(const CVC4::Node& node) const {
     return (size_t) node.getId();
   }
-};
+};/* struct NodeHashFunction */
 
 // for hash_maps, hash_sets..
 struct TNodeHashFunction {
   size_t operator()(CVC4::TNode node) const {
     return (size_t) node.getId();
   }
-};
+};/* struct TNodeHashFunction */
 
 template <bool ref_count>
 inline size_t NodeTemplate<ref_count>::getNumChildren() const {
@@ -976,7 +979,7 @@ NodeTemplate<ref_count>::printAst(std::ostream& out, int indent) const {
 /**
  * Returns a node representing the operator of this expression.
  * If this is an APPLY, then the operator will be a functional term.
- * Otherwise, it will be a node with kind BUILTIN
+ * Otherwise, it will be a node with kind BUILTIN.
  */
 template <bool ref_count>
 NodeTemplate<true> NodeTemplate<ref_count>::getOperator() const {
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index 942906fbd..4653ee95f 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -198,6 +198,9 @@ TypeNode NodeManager::getType(TNode n, bool check)
     case kind::SORT_TYPE:
       typeNode = kindType();
       break;
+    case kind::APPLY:
+      typeNode = CVC4::theory::builtin::ApplyTypeRule::computeType(this, n, check);
+      break;
     case kind::EQUAL:
       typeNode = CVC4::theory::builtin::EqualityTypeRule::computeType(this, n, check);
       break;
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index ca93473db..c0f489d7a 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -48,9 +48,11 @@ namespace expr {
 // TODO: hide this attribute behind a NodeManager interface.
 namespace attr {
   struct VarNameTag {};
+  struct SortArityTag {};
 }/* CVC4::expr::attr namespace */
 
 typedef expr::Attribute<attr::VarNameTag, std::string> VarNameAttr;
+typedef expr::Attribute<attr::SortArityTag, uint64_t> SortArityAttr;
 
 }/* CVC4::expr namespace */
 
@@ -508,7 +510,14 @@ public:
   inline TypeNode mkSort();
 
   /** Make a new sort with the given name and arity. */
-  inline TypeNode mkSort(const std::string& name, size_t arity = 0);
+  inline TypeNode mkSort(const std::string& name);
+
+  /** Make a new sort with the given name and arity. */
+  inline TypeNode mkSort(TypeNode constructor,
+                         const std::vector<TypeNode>& children);
+
+  /** Make a new sort with the given name and arity. */
+  inline TypeNode mkSortConstructor(const std::string& name, size_t arity);
 
   /**
    * Get the type for the given node and optionally do type checking.
@@ -762,16 +771,55 @@ inline bool NodeManager::hasOperator(Kind k) {
 }
 
 inline TypeNode NodeManager::mkSort() {
-  return NodeBuilder<0>(this, kind::SORT_TYPE).constructTypeNode();
+  NodeBuilder<1> nb(this, kind::SORT_TYPE);
+  Node sortTag = NodeBuilder<0>(this, kind::SORT_TAG);
+  nb << sortTag;
+  return nb.constructTypeNode();
 }
 
-inline TypeNode NodeManager::mkSort(const std::string& name, size_t arity) {
-  Assert(arity == 0, "parameterized sorts not yet supported.");
+inline TypeNode NodeManager::mkSort(const std::string& name) {
   TypeNode type = mkSort();
   type.setAttribute(expr::VarNameAttr(), name);
   return type;
 }
 
+inline TypeNode NodeManager::mkSort(TypeNode constructor,
+                                    const std::vector<TypeNode>& children) {
+  Assert(constructor.getKind() == kind::SORT_TYPE &&
+         constructor.getNumChildren() == 0,
+         "expected a sort constructor");
+  Assert(children.size() > 0, "expected non-zero # of children");
+  uint64_t arity;
+  std::string name;
+  bool hasArityAttribute =
+    getAttribute(constructor.d_nv, expr::SortArityAttr(), arity);
+  Assert(hasArityAttribute, "expected a sort constructor");
+  bool hasNameAttribute =
+    getAttribute(constructor.d_nv, expr::VarNameAttr(), name);
+  Assert(hasNameAttribute, "expected a sort constructor");
+  Assert(arity == children.size(),
+         "arity mismatch in application of sort constructor");
+  NodeBuilder<> nb(this, kind::SORT_TYPE);
+  Node sortTag = Node(constructor.d_nv->d_children[0]);
+  nb << sortTag;
+  nb.append(children);
+  TypeNode type = nb.constructTypeNode();
+  type.setAttribute(expr::VarNameAttr(), name);
+  return type;
+}
+
+inline TypeNode NodeManager::mkSortConstructor(const std::string& name,
+                                               size_t arity) {
+  Assert(arity > 0);
+  NodeBuilder<> nb(this, kind::SORT_TYPE);
+  Node sortTag = NodeBuilder<0>(this, kind::SORT_TAG);
+  nb << sortTag;
+  TypeNode type = nb.constructTypeNode();
+  type.setAttribute(expr::VarNameAttr(), name);
+  type.setAttribute(expr::SortArityAttr(), arity);
+  return type;
+}
+
 inline Node NodeManager::mkNode(Kind kind, TNode child1) {
   NodeBuilder<1> nb(this, kind);
   nb << child1;
@@ -832,7 +880,7 @@ inline Node NodeManager::mkNode(Kind kind, TNode child1, TNode child2,
 }
 
 inline Node* NodeManager::mkNodePtr(Kind kind, TNode child1, TNode child2,
-                                TNode child3, TNode child4, TNode child5) {
+                                    TNode child3, TNode child4, TNode child5) {
   NodeBuilder<5> nb(this, kind);
   nb << child1 << child2 << child3 << child4 << child5;
   return nb.constructNodePtr();
diff --git a/src/expr/type.cpp b/src/expr/type.cpp
index 43325d6cc..05b69f6f4 100644
--- a/src/expr/type.cpp
+++ b/src/expr/type.cpp
@@ -11,21 +11,25 @@
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
- ** \brief Implementation of expression types .
+ ** \brief Implementation of expression types
  **
- ** Implementation of expression types 
+ ** Implementation of expression types.
  **/
 
+#include <iostream>
 #include <string>
+#include <vector>
 
 #include "expr/node_manager.h"
 #include "expr/type.h"
 #include "expr/type_node.h"
 #include "util/Assert.h"
 
+using namespace std;
+
 namespace CVC4 {
 
-std::ostream& operator<<(std::ostream& out, const Type& e) {
+ostream& operator<<(ostream& out, const Type& e) {
   e.toStream(out);
   return out;
 }
@@ -34,8 +38,8 @@ Type Type::makeType(const TypeNode& typeNode) const {
   return Type(d_nodeManager, new TypeNode(typeNode));
 }
 
-Type::Type(NodeManager* nm, TypeNode* node)
-: d_typeNode(node),
+Type::Type(NodeManager* nm, TypeNode* node) :
+  d_typeNode(node),
   d_nodeManager(nm) {
 }
 
@@ -44,22 +48,20 @@ Type::~Type() {
   delete d_typeNode;
 }
 
-Type::Type()
-: d_typeNode(new TypeNode()),
-  d_nodeManager(NULL)
-{
+Type::Type() :
+  d_typeNode(new TypeNode),
+  d_nodeManager(NULL) {
 }
 
-Type::Type(uintptr_t n)
-: d_typeNode(new TypeNode()),
+Type::Type(uintptr_t n) :
+  d_typeNode(new TypeNode),
   d_nodeManager(NULL) {
   AlwaysAssert(n == 0);
 }
 
-Type::Type(const Type& t)
-: d_typeNode(new TypeNode(*t.d_typeNode)),
-  d_nodeManager(t.d_nodeManager)
-{
+Type::Type(const Type& t) :
+  d_typeNode(new TypeNode(*t.d_typeNode)),
+  d_nodeManager(t.d_nodeManager) {
 }
 
 bool Type::isNull() const {
@@ -68,7 +70,7 @@ bool Type::isNull() const {
 
 Type& Type::operator=(const Type& t) {
   NodeManagerScope nms(d_nodeManager);
-  if (this != &t) {
+  if(this != &t) {
     *d_typeNode = *t.d_typeNode;
     d_nodeManager = t.d_nodeManager;
   }
@@ -83,7 +85,36 @@ bool Type::operator!=(const Type& t) const {
   return *d_typeNode != *t.d_typeNode;
 }
 
-void Type::toStream(std::ostream& out) const {
+Type Type::substitute(const Type& type, const Type& replacement) const {
+  NodeManagerScope nms(d_nodeManager);
+  return makeType(d_typeNode->substitute(*type.d_typeNode,
+                                         *replacement.d_typeNode));
+}
+
+Type Type::substitute(const vector<Type>& types,
+                      const vector<Type>& replacements) const {
+  NodeManagerScope nms(d_nodeManager);
+
+  vector<TypeNode> typesNodes, replacementsNodes;
+
+  for(vector<Type>::const_iterator i = types.begin(),
+        iend = types.end();
+      i != iend;
+      ++i) {
+    typesNodes.push_back(*(*i).d_typeNode);
+  }
+
+  for(vector<Type>::const_iterator i = replacements.begin(),
+        iend = replacements.end();
+      i != iend;
+      ++i) {
+    replacementsNodes.push_back(*(*i).d_typeNode);
+  }
+
+  return makeType(d_typeNode->substitute(typesNodes, replacementsNodes));
+}
+
+void Type::toStream(ostream& out) const {
   NodeManagerScope nms(d_nodeManager);
   out << *d_typeNode;
   return;
@@ -96,7 +127,7 @@ bool Type::isBoolean() const {
 }
 
 /** Cast to a Boolean type */
-Type::operator BooleanType() const throw (AssertionException) {
+Type::operator BooleanType() const throw(AssertionException) {
   NodeManagerScope nms(d_nodeManager);
   Assert(isBoolean());
   return BooleanType(*this);
@@ -109,7 +140,7 @@ bool Type::isInteger() const {
 }
 
 /** Cast to a integer type */
-Type::operator IntegerType() const throw (AssertionException) {
+Type::operator IntegerType() const throw(AssertionException) {
   NodeManagerScope nms(d_nodeManager);
   Assert(isInteger());
   return IntegerType(*this);
@@ -122,7 +153,7 @@ bool Type::isReal() const {
 }
 
 /** Cast to a real type */
-Type::operator RealType() const throw (AssertionException) {
+Type::operator RealType() const throw(AssertionException) {
   NodeManagerScope nms(d_nodeManager);
   Assert(isReal());
   return RealType(*this);
@@ -135,7 +166,7 @@ bool Type::isBitVector() const {
 }
 
 /** Cast to a bit-vector type */
-Type::operator BitVectorType() const throw (AssertionException) {
+Type::operator BitVectorType() const throw(AssertionException) {
   NodeManagerScope nms(d_nodeManager);
   Assert(isBitVector());
   return BitVectorType(*this);
@@ -157,7 +188,7 @@ bool Type::isPredicate() const {
 }
 
 /** Cast to a function type */
-Type::operator FunctionType() const throw (AssertionException) {
+Type::operator FunctionType() const throw(AssertionException) {
   NodeManagerScope nms(d_nodeManager);
   Assert(isFunction());
   return FunctionType(*this);
@@ -170,7 +201,7 @@ bool Type::isTuple() const {
 }
 
 /** Cast to a tuple type */
-Type::operator TupleType() const throw (AssertionException) {
+Type::operator TupleType() const throw(AssertionException) {
   NodeManagerScope nms(d_nodeManager);
   Assert(isTuple());
   return TupleType(*this);
@@ -183,7 +214,7 @@ bool Type::isArray() const {
 }
 
 /** Cast to an array type */
-Type::operator ArrayType() const throw (AssertionException) {
+Type::operator ArrayType() const throw(AssertionException) {
   NodeManagerScope nms(d_nodeManager);
   return ArrayType(*this);
 }
@@ -195,12 +226,25 @@ bool Type::isSort() const {
 }
 
 /** Cast to a sort type */
-Type::operator SortType() const throw (AssertionException) {
+Type::operator SortType() const throw(AssertionException) {
   NodeManagerScope nms(d_nodeManager);
   Assert(isSort());
   return SortType(*this);
 }
 
+/** Is this a sort constructor kind */
+bool Type::isSortConstructor() const {
+  NodeManagerScope nms(d_nodeManager);
+  return d_typeNode->isSortConstructor();
+}
+
+/** Cast to a sort type */
+Type::operator SortConstructorType() const throw(AssertionException) {
+  NodeManagerScope nms(d_nodeManager);
+  Assert(isSortConstructor());
+  return SortConstructorType(*this);
+}
+
 /** Is this a kind type (i.e., the type of a type)? */
 bool Type::isKind() const {
   NodeManagerScope nms(d_nodeManager);
@@ -208,18 +252,18 @@ bool Type::isKind() const {
 }
 
 /** Cast to a kind type */
-Type::operator KindType() const throw (AssertionException) {
+Type::operator KindType() const throw(AssertionException) {
   NodeManagerScope nms(d_nodeManager);
   Assert(isKind());
   return KindType(*this);
 }
 
-std::vector<Type> FunctionType::getArgTypes() const {
+vector<Type> FunctionType::getArgTypes() const {
   NodeManagerScope nms(d_nodeManager);
-  std::vector<Type> args;
-  std::vector<TypeNode> argNodes = d_typeNode->getArgTypes();
-  std::vector<TypeNode>::iterator it = argNodes.begin();
-  std::vector<TypeNode>::iterator it_end = argNodes.end();
+  vector<Type> args;
+  vector<TypeNode> argNodes = d_typeNode->getArgTypes();
+  vector<TypeNode>::iterator it = argNodes.begin();
+  vector<TypeNode>::iterator it_end = argNodes.end();
   for(; it != it_end; ++ it) {
     args.push_back(makeType(*it));
   }
@@ -232,77 +276,96 @@ Type FunctionType::getRangeType() const {
   return makeType(d_typeNode->getRangeType());
 }
 
-std::vector<Type> TupleType::getTypes() const {
+vector<Type> TupleType::getTypes() const {
   NodeManagerScope nms(d_nodeManager);
-  std::vector<Type> types;
-  std::vector<TypeNode> typeNodes = d_typeNode->getTupleTypes();
-  std::vector<TypeNode>::iterator it = typeNodes.begin();
-  std::vector<TypeNode>::iterator it_end = typeNodes.end();
+  vector<Type> types;
+  vector<TypeNode> typeNodes = d_typeNode->getTupleTypes();
+  vector<TypeNode>::iterator it = typeNodes.begin();
+  vector<TypeNode>::iterator it_end = typeNodes.end();
   for(; it != it_end; ++ it) {
     types.push_back(makeType(*it));
   }
   return types;
 }
 
-std::string SortType::getName() const {
+string SortType::getName() const {
   NodeManagerScope nms(d_nodeManager);
   return d_typeNode->getAttribute(expr::VarNameAttr());
 }
 
-BooleanType::BooleanType(const Type& t) throw (AssertionException)
-: Type(t)
-{
+string SortConstructorType::getName() const {
+  NodeManagerScope nms(d_nodeManager);
+  return d_typeNode->getAttribute(expr::VarNameAttr());
+}
+
+size_t SortConstructorType::getArity() const {
+  NodeManagerScope nms(d_nodeManager);
+  return d_typeNode->getAttribute(expr::SortArityAttr());
+}
+
+SortType SortConstructorType::instantiate(const vector<Type>& params) const {
+  NodeManagerScope nms(d_nodeManager);
+  vector<TypeNode> paramsNodes;
+  for(vector<Type>::const_iterator i = params.begin(),
+        iend = params.end();
+      i != iend;
+      ++i) {
+    paramsNodes.push_back(*getTypeNode(*i));
+  }
+  return SortType(makeType(d_nodeManager->mkSort(*d_typeNode, paramsNodes)));
+}
+
+BooleanType::BooleanType(const Type& t) throw(AssertionException) :
+  Type(t) {
   Assert(isBoolean());
 }
 
-IntegerType::IntegerType(const Type& t) throw (AssertionException)
-: Type(t)
-{
+IntegerType::IntegerType(const Type& t) throw(AssertionException) :
+  Type(t) {
   Assert(isInteger());
 }
 
-RealType::RealType(const Type& t) throw (AssertionException)
-: Type(t)
-{
+RealType::RealType(const Type& t) throw(AssertionException) :
+  Type(t) {
   Assert(isReal());
 }
 
-BitVectorType::BitVectorType(const Type& t) throw (AssertionException)
-: Type(t)
-{
+BitVectorType::BitVectorType(const Type& t) throw(AssertionException) :
+  Type(t) {
   Assert(isBitVector());
 }
 
-FunctionType::FunctionType(const Type& t) throw (AssertionException)
-: Type(t)
-{
+FunctionType::FunctionType(const Type& t) throw(AssertionException) :
+  Type(t) {
   Assert(isFunction());
 }
 
-TupleType::TupleType(const Type& t) throw (AssertionException)
-: Type(t)
-{
+TupleType::TupleType(const Type& t) throw(AssertionException) :
+  Type(t) {
   Assert(isTuple());
 }
 
-ArrayType::ArrayType(const Type& t) throw (AssertionException)
-: Type(t)
-{
+ArrayType::ArrayType(const Type& t) throw(AssertionException) :
+  Type(t) {
   Assert(isArray());
 }
 
-KindType::KindType(const Type& t) throw (AssertionException)
-: Type(t)
-{
+KindType::KindType(const Type& t) throw(AssertionException) :
+  Type(t) {
   Assert(isKind());
 }
 
-SortType::SortType(const Type& t) throw (AssertionException)
-: Type(t)
-{
+SortType::SortType(const Type& t) throw(AssertionException) :
+  Type(t) {
   Assert(isSort());
 }
 
+SortConstructorType::SortConstructorType(const Type& t)
+  throw(AssertionException) :
+  Type(t) {
+  Assert(isSortConstructor());
+}
+
 unsigned BitVectorType::getSize() const {
   return d_typeNode->getBitVectorSize();
 }
diff --git a/src/expr/type.h b/src/expr/type.h
index 3e3fbd368..57ec3bf5c 100644
--- a/src/expr/type.h
+++ b/src/expr/type.h
@@ -46,6 +46,7 @@ class FunctionType;
 class TupleType;
 class KindType;
 class SortType;
+class SortConstructorType;
 class Type;
 
 /** Strategy for hashing Types */
@@ -85,6 +86,9 @@ protected:
    */
   Type(NodeManager* em, TypeNode* typeNode);
 
+  /** Accessor for derived classes */
+  static TypeNode* getTypeNode(const Type& t) { return t.d_typeNode; }
+
 public:
 
   /**
@@ -114,6 +118,17 @@ public:
   bool isNull() const;
 
   /**
+   * Substitution of Types.
+   */
+  Type substitute(const Type& type, const Type& replacement) const;
+
+  /**
+   * Simultaneous substitution of Types.
+   */
+  Type substitute(const std::vector<Type>& types,
+                  const std::vector<Type>& replacements) const;
+
+  /**
    * Assignment operator.
    * @param t the type to assign to this type
    * @return this type after assignment.
@@ -144,7 +159,7 @@ public:
    * Cast this type to a Boolean type
    * @return the BooleanType
    */
-  operator BooleanType() const throw (AssertionException);
+  operator BooleanType() const throw(AssertionException);
 
   /**
    * Is this the integer type?
@@ -156,7 +171,7 @@ public:
    * Cast this type to a integer type
    * @return the IntegerType
    */
-  operator IntegerType() const throw (AssertionException);
+  operator IntegerType() const throw(AssertionException);
 
   /**
    * Is this the real type?
@@ -168,7 +183,7 @@ public:
    * Cast this type to a real type
    * @return the RealType
    */
-  operator RealType() const throw (AssertionException);
+  operator RealType() const throw(AssertionException);
 
   /**
    * Is this the bit-vector type?
@@ -180,7 +195,7 @@ public:
    * Cast this type to a bit-vector type
    * @return the BitVectorType
    */
-  operator BitVectorType() const throw (AssertionException);
+  operator BitVectorType() const throw(AssertionException);
 
   /**
    * Is this a function type?
@@ -199,7 +214,7 @@ public:
    * Cast this type to a function type
    * @return the FunctionType
    */
-  operator FunctionType() const throw (AssertionException);
+  operator FunctionType() const throw(AssertionException);
 
   /**
    * Is this a tuple type?
@@ -211,7 +226,7 @@ public:
    * Cast this type to a tuple type
    * @return the TupleType
    */
-  operator TupleType() const throw (AssertionException);
+  operator TupleType() const throw(AssertionException);
 
   /**
    * Is this an array type?
@@ -223,7 +238,7 @@ public:
    * Cast this type to an array type
    * @return the ArrayType
    */
-  operator ArrayType() const throw (AssertionException);
+  operator ArrayType() const throw(AssertionException);
 
   /**
    * Is this a sort kind?
@@ -233,9 +248,21 @@ public:
 
   /**
    * Cast this type to a sort type
-   * @return the function Type
+   * @return the sort type
+   */
+  operator SortType() const throw(AssertionException);
+
+  /**
+   * Is this a sort constructor kind?
+   * @return true if this is a sort constructor kind
+   */
+  bool isSortConstructor() const;
+
+  /**
+   * Cast this type to a sort constructor type
+   * @return the sort constructor type
    */
-  operator SortType() const throw (AssertionException);
+  operator SortConstructorType() const throw(AssertionException);
 
   /**
    * Is this a kind type (i.e., the type of a type)?
@@ -247,7 +274,7 @@ public:
    * Cast to a kind type
    * @return the kind type
    */
-  operator KindType() const throw (AssertionException);
+  operator KindType() const throw(AssertionException);
 
   /**
    * Outputs a string representation of this type to the stream.
@@ -264,7 +291,7 @@ class CVC4_PUBLIC BooleanType : public Type {
 public:
 
   /** Construct from the base type */
-  BooleanType(const Type& type) throw (AssertionException);
+  BooleanType(const Type& type) throw(AssertionException);
 };
 
 /**
@@ -275,7 +302,7 @@ class CVC4_PUBLIC IntegerType : public Type {
 public:
 
   /** Construct from the base type */
-  IntegerType(const Type& type) throw (AssertionException);
+  IntegerType(const Type& type) throw(AssertionException);
 };
 
 /**
@@ -286,7 +313,7 @@ class CVC4_PUBLIC RealType : public Type {
 public:
 
   /** Construct from the base type */
-  RealType(const Type& type) throw (AssertionException);
+  RealType(const Type& type) throw(AssertionException);
 };
 
 
@@ -298,7 +325,7 @@ class CVC4_PUBLIC FunctionType : public Type {
 public:
 
   /** Construct from the base type */
-  FunctionType(const Type& type) throw (AssertionException);
+  FunctionType(const Type& type) throw(AssertionException);
 
   /** Get the argument types */
   std::vector<Type> getArgTypes() const;
@@ -315,7 +342,7 @@ class CVC4_PUBLIC TupleType : public Type {
 public:
 
   /** Construct from the base type */
-  TupleType(const Type& type) throw (AssertionException);
+  TupleType(const Type& type) throw(AssertionException);
 
   /** Get the constituent types */
   std::vector<Type> getTypes() const;
@@ -329,7 +356,7 @@ class CVC4_PUBLIC ArrayType : public Type {
 public:
 
   /** Construct from the base type */
-  ArrayType(const Type& type) throw (AssertionException);
+  ArrayType(const Type& type) throw(AssertionException);
 
   /** Get the index type */
   Type getIndexType() const;
@@ -346,13 +373,33 @@ class CVC4_PUBLIC SortType : public Type {
 public:
 
   /** Construct from the base type */
-  SortType(const Type& type) throw (AssertionException);
+  SortType(const Type& type) throw(AssertionException);
 
   /** Get the name of the sort */
   std::string getName() const;
 };
 
 /**
+ * Class encapsulating a user-defined sort constructor.
+ */
+class CVC4_PUBLIC SortConstructorType : public Type {
+
+public:
+
+  /** Construct from the base type */
+  SortConstructorType(const Type& type) throw(AssertionException);
+
+  /** Get the name of the sort constructor */
+  std::string getName() const;
+
+  /** Get the arity of the sort constructor */
+  size_t getArity() const;
+
+  /** Instantiate a sort using this sort constructor */
+  SortType instantiate(const std::vector<Type>& params) const;
+};
+
+/**
  * Class encapsulating the kind type (the type of types).
  */
 class CVC4_PUBLIC KindType : public Type {
@@ -360,7 +407,7 @@ class CVC4_PUBLIC KindType : public Type {
 public:
 
   /** Construct from the base type */
-  KindType(const Type& type) throw (AssertionException);
+  KindType(const Type& type) throw(AssertionException);
 };
 
 
@@ -372,7 +419,7 @@ class CVC4_PUBLIC BitVectorType : public Type {
 public:
 
   /** Construct from the base type */
-  BitVectorType(const Type& type) throw (AssertionException);
+  BitVectorType(const Type& type) throw(AssertionException);
 
   /**
    * Returns the size of the bit-vector type.
@@ -384,7 +431,7 @@ public:
 /**
  * Output operator for types
  * @param out the stream to output to
- * @param e the type to output
+ * @param t the type to output
  * @return the stream
  */
 std::ostream& operator<<(std::ostream& out, const Type& t) CVC4_PUBLIC;
diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp
index 94213d941..a55c05c5a 100644
--- a/src/expr/type_node.cpp
+++ b/src/expr/type_node.cpp
@@ -16,23 +16,67 @@
  ** Reference-counted encapsulation of a pointer to node information.
  **/
 
+#include <vector>
+
 #include "expr/type_node.h"
 
+using namespace std;
+
 namespace CVC4 {
 
-TypeNode TypeNode::s_null(&expr::NodeValue::s_null);
+TypeNode TypeNode::s_null( &expr::NodeValue::s_null );
+
+TypeNode TypeNode::substitute(const TypeNode& type,
+                              const TypeNode& replacement) const {
+  NodeBuilder<> nb(getKind());
+  if(getMetaKind() == kind::metakind::PARAMETERIZED) {
+    // push the operator
+    nb << TypeNode(d_nv->d_children[0]);
+  }
+  for(TypeNode::iterator i = begin(), iend = end(); i != iend; ++i) {
+    if(*i == type) {
+      nb << replacement;
+    } else {
+      (*i).substitute(type, replacement);
+    }
+  }
+  return nb.constructTypeNode();
+}
+
+TypeNode TypeNode::substitute(const vector<TypeNode>& types,
+                              const vector<TypeNode>& replacements) const {
+  vector<TypeNode>::const_iterator j = find(types.begin(), types.end(), *this);
+  if(j != types.end()) {
+    return replacements[j - types.begin()];
+  } else if(getNumChildren() == 0) {
+    return *this;
+  } else {
+    NodeBuilder<> nb(getKind());
+    if(getMetaKind() == kind::metakind::PARAMETERIZED) {
+      // push the operator
+      nb << TypeNode(d_nv->d_children[0]);
+    }
+    for(TypeNode::iterator i = begin(), iend = end(); i != iend; ++i) {
+      nb << (*i).substitute(types, replacements);
+    }
+    return nb.constructTypeNode();
+  }
+}
 
 bool TypeNode::isBoolean() const {
-  return getKind() == kind::TYPE_CONSTANT && getConst<TypeConstant>() == BOOLEAN_TYPE;
+  return getKind() == kind::TYPE_CONSTANT &&
+    getConst<TypeConstant>() == BOOLEAN_TYPE;
 }
 
 bool TypeNode::isInteger() const {
-  return getKind() == kind::TYPE_CONSTANT && getConst<TypeConstant>() == INTEGER_TYPE;
+  return getKind() == kind::TYPE_CONSTANT &&
+    getConst<TypeConstant>() == INTEGER_TYPE;
 }
 
 bool TypeNode::isReal() const {
   return getKind() == kind::TYPE_CONSTANT
-    && (getConst<TypeConstant>() == REAL_TYPE || getConst<TypeConstant>() == INTEGER_TYPE);
+    && ( getConst<TypeConstant>() == REAL_TYPE ||
+         getConst<TypeConstant>() == INTEGER_TYPE );
 }
 
 bool TypeNode::isArray() const {
@@ -60,10 +104,10 @@ bool TypeNode::isPredicate() const {
   return isFunction() && getRangeType().isBoolean();
 }
 
-std::vector<TypeNode> TypeNode::getArgTypes() const {
+vector<TypeNode> TypeNode::getArgTypes() const {
   Assert(isFunction());
-  std::vector<TypeNode> args;
-  for (unsigned i = 0, i_end = getNumChildren() - 1; i < i_end; ++i) {
+  vector<TypeNode> args;
+  for(unsigned i = 0, i_end = getNumChildren() - 1; i < i_end; ++i) {
     args.push_back((*this)[i]);
   }
   return args;
@@ -80,10 +124,10 @@ bool TypeNode::isTuple() const {
 }
 
 /** Is this a tuple type? */
-std::vector<TypeNode> TypeNode::getTupleTypes() const {
+vector<TypeNode> TypeNode::getTupleTypes() const {
   Assert(isTuple());
-  std::vector<TypeNode> types;
-  for (unsigned i = 0, i_end = getNumChildren(); i < i_end; ++i) {
+  vector<TypeNode> types;
+  for(unsigned i = 0, i_end = getNumChildren(); i < i_end; ++i) {
     types.push_back((*this)[i]);
   }
   return types;
@@ -91,12 +135,18 @@ std::vector<TypeNode> TypeNode::getTupleTypes() const {
 
 /** Is this a sort kind */
 bool TypeNode::isSort() const {
-  return getKind() == kind::SORT_TYPE;
+  return getKind() == kind::SORT_TYPE && !hasAttribute(expr::SortArityAttr());
+}
+
+/** Is this a sort constructor kind */
+bool TypeNode::isSortConstructor() const {
+  return getKind() == kind::SORT_TYPE && hasAttribute(expr::SortArityAttr());
 }
 
 /** Is this a kind type (i.e., the type of a type)? */
 bool TypeNode::isKind() const {
-  return getKind() == kind::TYPE_CONSTANT && getConst<TypeConstant>() == KIND_TYPE;
+  return getKind() == kind::TYPE_CONSTANT &&
+    getConst<TypeConstant>() == KIND_TYPE;
 }
 
 /** Is this a bit-vector type */
@@ -106,7 +156,8 @@ bool TypeNode::isBitVector() const {
 
 /** Is this a bit-vector type of size <code>size</code> */
 bool TypeNode::isBitVector(unsigned size) const {
-  return getKind() == kind::BITVECTOR_TYPE && getConst<BitVectorSize>() == size;
+  return getKind() == kind::BITVECTOR_TYPE &&
+    getConst<BitVectorSize>() == size;
 }
 
 /** Get the size of this bit-vector type */
diff --git a/src/expr/type_node.h b/src/expr/type_node.h
index 30359495f..6780b08f7 100644
--- a/src/expr/type_node.h
+++ b/src/expr/type_node.h
@@ -70,9 +70,9 @@ class TypeNode {
   friend class NodeBuilder;
 
   /**
-   * Assigns the expression value and does reference counting. No assumptions
-   * are made on the expression, and should only be used if we know what we
-   * are doing.
+   * Assigns the expression value and does reference counting. No
+   * assumptions are made on the expression, and should only be used
+   * if we know what we are doing.
    *
    * @param ev the expression value to assign
    */
@@ -87,21 +87,23 @@ public:
   TypeNode(const TypeNode& node);
 
   /**
+   * Destructor. If ref_count is true it will decrement the reference count
+   * and, if zero, collect the NodeValue.
+   */
+  ~TypeNode() throw(AssertionException);
+
+  /**
    * Assignment operator for nodes, copies the relevant information from node
    * to this node.
+   *
    * @param node the node to copy
    * @return reference to this node
    */
   TypeNode& operator=(const TypeNode& typeNode);
 
   /**
-   * Destructor. If ref_count is true it will decrement the reference count
-   * and, if zero, collect the NodeValue.
-   */
-  ~TypeNode() throw(AssertionException);
-
-  /**
    * Return the null node.
+   *
    * @return the null node
    */
   static TypeNode null() {
@@ -109,18 +111,31 @@ public:
   }
 
   /**
+   * Substitution of TypeNodes.
+   */
+  TypeNode substitute(const TypeNode& type, const TypeNode& replacement) const;
+
+  /**
+   * Simultaneous substitution of TypeNodes.
+   */
+  TypeNode substitute(const std::vector<TypeNode>& types,
+                      const std::vector<TypeNode>& replacements) const;
+
+  /**
    * Structural comparison operator for expressions.
+   *
    * @param typeNode the type node to compare to
    * @return true if expressions are equal, false otherwise
    */
   bool operator==(const TypeNode& typeNode) const {
     return
-      d_nv == typeNode.d_nv
-      || (typeNode.isReal() && this->isReal());
+      d_nv == typeNode.d_nv ||
+      (typeNode.isReal() && this->isReal());
   }
 
   /**
    * Structural comparison operator for expressions.
+   *
    * @param typeNode the type node to compare to
    * @return true if expressions are equal, false otherwise
    */
@@ -131,6 +146,7 @@ public:
   /**
    * We compare by expression ids so, keeping things deterministic and having
    * that subexpressions have to be smaller than the enclosing expressions.
+   *
    * @param node the node to compare to
    * @return true if this expression is smaller
    */
@@ -140,23 +156,26 @@ public:
 
   /**
    * Returns the i-th child of this node.
+   *
    * @param i the index of the child
    * @return the node representing the i-th child
    */
-  TypeNode operator[](int i) const {
+  inline TypeNode operator[](int i) const {
     return TypeNode(d_nv->getChild(i));
   }
 
   /**
    * Returns the unique id of this node
+   *
    * @return the id
    */
-  unsigned getId() const {
+  inline unsigned getId() const {
     return d_nv->getId();
   }
 
   /**
    * Returns the kind of this type node.
+   *
    * @return the kind
    */
   inline Kind getKind() const {
@@ -165,6 +184,7 @@ public:
 
   /**
    * Returns the metakind of this type node.
+   *
    * @return the metakind
    */
   inline kind::MetaKind getMetaKind() const {
@@ -173,6 +193,7 @@ public:
 
   /**
    * Returns the number of children this node has.
+   *
    * @return the number of children
    */
   inline size_t getNumChildren() const;
@@ -185,11 +206,13 @@ public:
 
   /**
    * Returns the value of the given attribute that this has been attached.
+   *
    * @param attKind the kind of the attribute
    * @return the value of the attribute
    */
   template <class AttrKind>
-  inline typename AttrKind::value_type getAttribute(const AttrKind& attKind) const;
+  inline typename AttrKind::value_type
+  getAttribute(const AttrKind& attKind) const;
 
   // Note that there are two, distinct hasAttribute() declarations for
   // a reason (rather than using a pointer-valued argument with a
@@ -197,9 +220,11 @@ public:
   // hasAttribute() implementations.
 
   /**
-   * Returns true if this node has been associated an attribute of given kind.
-   * Additionaly, if a pointer to the value_kind is give, and the attribute
-   * value has been set for this node, it will be returned.
+   * Returns true if this node has been associated an attribute of
+   * given kind.  Additionally, if a pointer to the value_kind is
+   * give, and the attribute value has been set for this node, it will
+   * be returned.
+   *
    * @param attKind the kind of the attribute
    * @return true if this node has the requested attribute
    */
@@ -210,6 +235,7 @@ public:
    * Returns true if this node has been associated an attribute of given kind.
    * Additionaly, if a pointer to the value_kind is give, and the attribute
    * value has been set for this node, it will be returned.
+   *
    * @param attKind the kind of the attribute
    * @param value where to store the value if it exists
    * @return true if this node has the requested attribute
@@ -220,6 +246,7 @@ public:
 
   /**
    * Sets the given attribute of this node to the given value.
+   *
    * @param attKind the kind of the atribute
    * @param value the value to set the attribute to
    */
@@ -234,6 +261,7 @@ public:
 
   /**
    * Returns the iterator pointing to the first child.
+   *
    * @return the iterator
    */
   inline iterator begin() {
@@ -241,8 +269,9 @@ public:
   }
 
   /**
-   * Returns the iterator pointing to the end of the children (one beyond the
-   * last one.
+   * Returns the iterator pointing to the end of the children (one
+   * beyond the last one.
+   *
    * @return the end of the children iterator.
    */
   inline iterator end() {
@@ -251,6 +280,7 @@ public:
 
   /**
    * Returns the const_iterator pointing to the first child.
+   *
    * @return the const_iterator
    */
   inline const_iterator begin() const {
@@ -258,8 +288,9 @@ public:
   }
 
   /**
-   * Returns the const_iterator pointing to the end of the children (one
-   * beyond the last one.
+   * Returns the const_iterator pointing to the end of the children
+   * (one beyond the last one.
+   *
    * @return the end of the children const_iterator.
    */
   inline const_iterator end() const {
@@ -267,8 +298,9 @@ public:
   }
 
   /**
-   * Converts this node into a string representation.
-   * @return the string representation of this node.
+   * Converts this type into a string representation.
+   *
+   * @return the string representation of this type.
    */
   inline std::string toString() const {
     return d_nv->toString();
@@ -277,6 +309,7 @@ public:
   /**
    * Converst this node into a string representation and sends it to the
    * given stream
+   *
    * @param out the sream to serialise this node to
    */
   inline void toStream(std::ostream& out, int toDepth = -1,
@@ -286,6 +319,7 @@ public:
 
   /**
    * Very basic pretty printer for Node.
+   *
    * @param o output stream to print to.
    * @param indent number of spaces to indent the formula by.
    */
@@ -293,6 +327,7 @@ public:
 
   /**
    * Returns true if this type is a null type.
+   *
    * @return true if null
    */
   bool isNull() const {
@@ -350,6 +385,9 @@ public:
   /** Is this a sort kind */
   bool isSort() const;
 
+  /** Is this a sort constructor kind */
+  bool isSortConstructor() const;
+
   /** Is this a kind type (i.e., the type of a type)? */
   bool isKind() const;
 
@@ -357,6 +395,7 @@ private:
 
   /**
    * Indents the given stream a given amount of spaces.
+   *
    * @param out the stream to indent
    * @param indent the numer of spaces
    */
@@ -370,6 +409,7 @@ private:
 
 /**
  * Serializes a given node to the given stream.
+ *
  * @param out the output stream to use
  * @param node the node to output to the stream
  * @return the changed stream.
@@ -383,7 +423,7 @@ inline std::ostream& operator<<(std::ostream& out, const TypeNode& n) {
 
 // for hash_maps, hash_sets..
 struct TypeNodeHashStrategy {
-  static inline size_t hash(const CVC4::TypeNode& node) {
+  static inline size_t hash(const TypeNode& node) {
     return (size_t) node.getId();
   }
 };/* struct TypeNodeHashStrategy */
@@ -429,7 +469,8 @@ inline void TypeNode::assignNodeValue(expr::NodeValue* ev) {
 
 inline TypeNode& TypeNode::operator=(const TypeNode& typeNode) {
   Assert(d_nv != NULL, "Expecting a non-NULL expression value!");
-  Assert(typeNode.d_nv != NULL, "Expecting a non-NULL expression value on RHS!");
+  Assert(typeNode.d_nv != NULL,
+         "Expecting a non-NULL expression value on RHS!");
   if(EXPECT_TRUE( d_nv != typeNode.d_nv )) {
     d_nv->dec();
     d_nv = typeNode.d_nv;
diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index 39f61c16d..297a2d804 100644
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -66,11 +66,15 @@ Expr Parser::getVariable(const std::string& name) {
   return getSymbol(name, SYM_VARIABLE);
 }
 
+Expr Parser::getFunction(const std::string& name) {
+  return getSymbol(name, SYM_VARIABLE);
+}
+
 Type
 Parser::getType(const std::string& var_name,
                      SymbolType type) {
   Assert( isDeclared(var_name, type) );
-  Type t = getSymbol(var_name,type).getType();
+  Type t = getSymbol(var_name, type).getType();
   return t;
 }
 
@@ -83,8 +87,7 @@ Type Parser::getSort(const std::string& name) {
 Type Parser::getSort(const std::string& name,
                      const std::vector<Type>& params) {
   Assert( isDeclared(name, SYM_SORT) );
-  Type t = d_declScope.lookupType(name);
-  Warning() << "FIXME use params to realize parameterized sort\n";
+  Type t = d_declScope.lookupType(name, params);
   return t;
 }
 
@@ -98,6 +101,11 @@ bool Parser::isFunction(const std::string& name) {
   return isDeclared(name, SYM_VARIABLE) && getType(name).isFunction();
 }
 
+/* Returns true if name is bound to a defined function. */
+bool Parser::isDefinedFunction(const std::string& name) {
+  return isFunction(name) && d_declScope.isBoundDefinedFunction(name);
+}
+
 /* Returns true if name is bound to a function returning boolean. */
 bool Parser::isPredicate(const std::string& name) {
   return isDeclared(name, SYM_VARIABLE) && getType(name).isPredicate();
@@ -105,32 +113,54 @@ bool Parser::isPredicate(const std::string& name) {
 
 Expr
 Parser::mkVar(const std::string& name, const Type& type) {
-  Debug("parser") << "mkVar(" << name << "," << type << ")" << std::endl;
+  Debug("parser") << "mkVar(" << name << ", " << type << ")" << std::endl;
   Expr expr = d_exprManager->mkVar(name, type);
-  defineVar(name,expr);
+  defineVar(name, expr);
+  return expr;
+}
+
+Expr
+Parser::mkFunction(const std::string& name, const Type& type) {
+  Debug("parser") << "mkVar(" << name << ", " << type << ")" << std::endl;
+  Expr expr = d_exprManager->mkVar(name, type);
+  defineFunction(name, expr);
   return expr;
 }
 
 const std::vector<Expr>
 Parser::mkVars(const std::vector<std::string> names,
-                    const Type& type) {
+               const Type& type) {
   std::vector<Expr> vars;
   for(unsigned i = 0; i < names.size(); ++i) {
-    vars.push_back(mkVar(names[i],type));
+    vars.push_back(mkVar(names[i], type));
   }
   return vars;
 }
 
 void
 Parser::defineVar(const std::string& name, const Expr& val) {
-  d_declScope.bind(name,val);
-  Assert(isDeclared(name));
+  d_declScope.bind(name, val);
+  Assert( isDeclared(name) );
+}
+
+void
+Parser::defineFunction(const std::string& name, const Expr& val) {
+  d_declScope.bindDefinedFunction(name, val);
+  Assert( isDeclared(name) );
 }
 
 void
 Parser::defineType(const std::string& name, const Type& type) {
-  d_declScope.bindType(name,type);
-  Assert( isDeclared(name, SYM_SORT) ) ;
+  d_declScope.bindType(name, type);
+  Assert( isDeclared(name, SYM_SORT) );
+}
+
+void
+Parser::defineType(const std::string& name,
+                   const std::vector<Type>& params,
+                   const Type& type) {
+  d_declScope.bindType(name, params, type);
+  Assert( isDeclared(name, SYM_SORT) );
 }
 
 void
@@ -139,20 +169,30 @@ Parser::defineParameterizedType(const std::string& name,
                                 const Type& type) {
   if(Debug.isOn("parser")) {
     Debug("parser") << "defineParameterizedType(" << name << ", " << params.size() << ", [";
-    copy(params.begin(), params.end() - 1,
-         ostream_iterator<Type>(Debug("parser"), ", ") );
-    Debug("parser") << params.back();
+    if(params.size() > 0) {
+      copy(params.begin(), params.end() - 1,
+           ostream_iterator<Type>(Debug("parser"), ", ") );
+      Debug("parser") << params.back();
+    }
     Debug("parser") << "], " << type << ")" << std::endl;
   }
-  Warning("defineSort unimplemented\n");
-  defineType(name,type);
+  defineType(name, params, type);
+}
+
+Type
+Parser::mkSort(const std::string& name) {
+  Debug("parser") << "newSort(" << name << ")" << std::endl;
+  Type type = d_exprManager->mkSort(name);
+  defineType(name, type);
+  return type;
 }
 
 Type
-Parser::mkSort(const std::string& name, size_t arity) {
-  Debug("parser") << "newSort(" << name << ", " << arity << ")" << std::endl;
-  Type type = d_exprManager->mkSort(name, arity);
-  defineType(name,type);
+Parser::mkSortConstructor(const std::string& name, size_t arity) {
+  Debug("parser") << "newSortConstructor(" << name << ", " << arity << ")"
+                  << std::endl;
+  Type type = d_exprManager->mkSortConstructor(name, arity);
+  defineType(name, vector<Type>(arity), type);
   return type;
 }
 
@@ -239,7 +279,7 @@ void Parser::checkOperator(Kind kind, unsigned int numArgs) throw (ParserExcepti
   if( d_strictMode && d_logicOperators.find(kind) == d_logicOperators.end() ) {
     parseError( "Operator is not defined in the current logic: " + kindToString(kind) );
   }
-  checkArity(kind,numArgs);
+  checkArity(kind, numArgs);
 }
 
 void Parser::addOperator(Kind kind) {
diff --git a/src/parser/parser.h b/src/parser/parser.h
index 0faf9bebf..1c492c843 100644
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -186,26 +186,21 @@ public:
 
   bool strictModeEnabled() { return d_strictMode; }
 
-  /** Get the name of the input file. */
-/*
-  inline const std::string getFilename() {
-    return d_filename;
-  }
-*/
-
   /**
-   * Sets the logic for the current benchmark. Declares any logic symbols.
+   * Returns a variable, given a name.
    *
-   * @param name the name of the logic (e.g., QF_UF, AUFLIA)
+   * @param name the name of the variable
+   * @return the variable expression
    */
-//  void setLogic(const std::string& name);
+  Expr getVariable(const std::string& name);
 
   /**
-   * Returns a variable, given a name and a type.
+   * Returns a function, given a name.
+   *
    * @param var_name the name of the variable
    * @return the variable expression
    */
-  Expr getVariable(const std::string& var_name);
+  Expr getFunction(const std::string& name);
 
   /**
    * Returns a sort, given a name.
@@ -213,7 +208,7 @@ public:
   Type getSort(const std::string& sort_name);
 
   /**
-   * Returns a sort, given a name and args.
+   * Returns a (parameterized) sort, given a name and args.
    */
   Type getSort(const std::string& sort_name,
                const std::vector<Type>& params);
@@ -240,7 +235,8 @@ public:
   /**
    * Checks whether the given name is bound to a function.
    * @param name the name to check
-   * @throws ParserException if checks are enabled and name is not bound to a function
+   * @throws ParserException if checks are enabled and name is not
+   * bound to a function
    */
   void checkFunction(const std::string& name) throw (ParserException);
 
@@ -248,23 +244,26 @@ public:
    * Check that <code>kind</code> can accept <code>numArgs</code> arguments.
    * @param kind the built-in operator to check
    * @param numArgs the number of actual arguments
-   * @throws ParserException if checks are enabled and the operator <code>kind</code> cannot be
-   * applied to <code>numArgs</code> arguments.
+   * @throws ParserException if checks are enabled and the operator
+   * <code>kind</code> cannot be applied to <code>numArgs</code>
+   * arguments.
    */
   void checkArity(Kind kind, unsigned int numArgs) throw (ParserException);
 
-  /** Check that <code>kind</code> is a legal operator in the current logic and
-   * that it can accept <code>numArgs</code> arguments.
+  /**
+   * Check that <code>kind</code> is a legal operator in the current
+   * logic and that it can accept <code>numArgs</code> arguments.
    *
    * @param kind the built-in operator to check
    * @param numArgs the number of actual arguments
-   * @throws ParserException if the parser mode is strict and the operator <code>kind</kind>
-   * has not been enabled
+   * @throws ParserException if the parser mode is strict and the
+   * operator <code>kind</kind> has not been enabled
    */
   void checkOperator(Kind kind, unsigned int numArgs) throw (ParserException);
 
   /**
    * Returns the type for the variable with the given name.
+   *
    * @param var_name the symbol to lookup
    * @param type the (namespace) type of the symbol
    */
@@ -274,27 +273,41 @@ public:
   Expr mkVar(const std::string& name, const Type& type);
 
   /**
-   * Create a set of new CVC4 variable expressions of the given
-   * type.
+   * Create a set of new CVC4 variable expressions of the given type.
    */
   const std::vector<Expr>
   mkVars(const std::vector<std::string> names, const Type& type);
 
+  /** Create a new CVC4 function expression of the given type. */
+  Expr mkFunction(const std::string& name, const Type& type);
+
   /** Create a new variable definition (e.g., from a let binding). */
   void defineVar(const std::string& name, const Expr& val);
 
+  /** Create a new function definition (e.g., from a define-fun). */
+  void defineFunction(const std::string& name, const Expr& val);
+
   /** Create a new type definition. */
   void defineType(const std::string& name, const Type& type);
 
+  /** Create a new (parameterized) type definition. */
+  void defineType(const std::string& name,
+                  const std::vector<Type>& params, const Type& type);
+
   /** Create a new type definition (e.g., from an SMT-LIBv2 define-sort). */
   void defineParameterizedType(const std::string& name,
                                const std::vector<Type>& params,
                                const Type& type);
 
   /**
-   * Creates a new sort with the given name and arity.
+   * Creates a new sort with the given name.
+   */
+  Type mkSort(const std::string& name);
+
+  /**
+   * Creates a new sort constructor with the given name and arity.
    */
-  Type mkSort(const std::string& name, size_t arity = 0);
+  Type mkSortConstructor(const std::string& name, size_t arity);
 
   /**
    * Creates new sorts with the given names (all of arity 0).
@@ -314,6 +327,9 @@ public:
   /** Is the symbol bound to a function? */
   bool isFunction(const std::string& name);
 
+  /** Is the symbol bound to a defined function? */
+  bool isDefinedFunction(const std::string& name);
+
   /** Is the symbol bound to a predicate? */
   bool isPredicate(const std::string& name);
 
diff --git a/src/parser/smt/smt.cpp b/src/parser/smt/smt.cpp
index da352c226..7ff738dd7 100644
--- a/src/parser/smt/smt.cpp
+++ b/src/parser/smt/smt.cpp
@@ -85,8 +85,8 @@ void Smt::addTheory(Theory theory) {
   case THEORY_ARRAYS_EX: {
     Type indexType = mkSort("Index");
     Type elementType = mkSort("Element");
-    
-    defineType("Array",getExprManager()->mkArrayType(indexType,elementType));
+
+    defineType("Array", getExprManager()->mkArrayType(indexType,elementType));
 
     addOperator(kind::SELECT);
     addOperator(kind::STORE);
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 4c742adfc..9ad8c3177 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -19,8 +19,8 @@
 grammar Smt2;
 
 options {
-  language = 'C';                  // C output for antlr
-//  defaultErrorHandler = false;      // Skip the default error handling, just break with exceptions
+  language = 'C'; // C output for antlr
+  //defaultErrorHandler = false; // Skip the default error handling, just break with exceptions
   k = 2;
 }
 
@@ -162,8 +162,15 @@ command returns [CVC4::Command* cmd]
     DECLARE_SORT_TOK symbol[name,CHECK_UNDECLARED,SYM_SORT] n=INTEGER_LITERAL
     { Debug("parser") << "declare sort: '" << name
                       << "' arity=" << n << std::endl;
-      PARSER_STATE->mkSort(name, AntlrInput::tokenToUnsigned(n));
-      $cmd = new DeclarationCommand(name,EXPR_MANAGER->kindType()); }
+      unsigned arity = AntlrInput::tokenToUnsigned(n);
+      if(arity == 0) {
+        PARSER_STATE->mkSort(name);
+        $cmd = new DeclarationCommand(name, EXPR_MANAGER->kindType());
+      } else {
+        PARSER_STATE->mkSortConstructor(name, arity);
+        $cmd = new DeclarationCommand(name, EXPR_MANAGER->kindType());
+      }
+    }
   | /* sort definition */
     DEFINE_SORT_TOK symbol[name,CHECK_UNDECLARED,SYM_SORT]
     LPAREN_TOK symbolList[names,CHECK_NONE,SYM_SORT] RPAREN_TOK
@@ -223,8 +230,8 @@ command returns [CVC4::Command* cmd]
       // declare the name down here (while parsing term, signature
       // must not be extended with the name itself; no recursion
       // permitted)
-      PARSER_STATE->mkVar(name, t);
-      $cmd = new DefineFunctionCommand(name,sortedVars,t,expr);
+      PARSER_STATE->mkFunction(name, t);
+      $cmd = new DefineFunctionCommand(name, sortedVars, t, expr);
     }
   | /* value query */
     GET_VALUE_TOK LPAREN_TOK termList[terms,expr] RPAREN_TOK
@@ -315,22 +322,18 @@ term[CVC4::Expr& expr]
 
   | /* A non-built-in function application */
     LPAREN_TOK
-    functionSymbol[expr]
-    { args.push_back(expr); }
+    functionName[name,CHECK_DECLARED]
+    { args.push_back(Expr()); }
     termList[args,expr] RPAREN_TOK
-    // TODO: check arity
-    { expr = MK_EXPR(CVC4::kind::APPLY_UF,args); }
-
-  // | /* An ite expression */
-  //   LPAREN_TOK ITE_TOK
-  //   term[expr]
-  //   { args.push_back(expr); }
-  //   term[expr]
-  //   { args.push_back(expr); }
-  //   term[expr]
-  //   { args.push_back(expr); }
-  //   RPAREN_TOK
-  //   { expr = MK_EXPR(CVC4::kind::ITE, args); }
+    { PARSER_STATE->checkFunction(name);
+      const bool isDefinedFunction =
+        PARSER_STATE->isDefinedFunction(name);
+      expr = isDefinedFunction ?
+        PARSER_STATE->getFunction(name) :
+        PARSER_STATE->getVariable(name);
+      args[0] = expr;
+      // TODO: check arity
+      expr = MK_EXPR(isDefinedFunction ? CVC4::kind::APPLY : CVC4::kind::APPLY_UF, args); }
 
   | /* a let binding */
     LPAREN_TOK LET_TOK LPAREN_TOK
@@ -479,7 +482,7 @@ sortSymbol[CVC4::Type& t]
         }
         t = EXPR_MANAGER->mkArrayType( args[0], args[1] );
       } else {
-        PARSER_STATE->parseError("Unhandled parameterized type.");
+        t = PARSER_STATE->getSort(name, args);
       }
     }
   ;
@@ -516,9 +519,7 @@ symbol[std::string& id,
 
 // Base SMT-LIB tokens
 ASSERT_TOK : 'assert';
-//CATEGORY_TOK : ':category';
 CHECKSAT_TOK : 'check-sat';
-//DIFFICULTY_TOK : ':difficulty';
 DECLARE_FUN_TOK : 'declare-fun';
 DECLARE_SORT_TOK : 'declare-sort';
 DEFINE_FUN_TOK : 'define-fun';
@@ -526,23 +527,15 @@ DEFINE_SORT_TOK : 'define-sort';
 GET_VALUE_TOK : 'get-value';
 GET_ASSERTIONS_TOK : 'get-assertions';
 EXIT_TOK : 'exit';
-//FALSE_TOK : 'false';
 ITE_TOK : 'ite';
 LET_TOK : 'let';
 LPAREN_TOK : '(';
-//NOTES_TOK : ':notes';
 RPAREN_TOK : ')';
-//SAT_TOK : 'sat';
 SET_LOGIC_TOK : 'set-logic';
 SET_INFO_TOK : 'set-info';
+GET_INFO_TOK : 'get-info';
 SET_OPTION_TOK : 'set-option';
 GET_OPTION_TOK : 'get-option';
-//SMT_VERSION_TOK : ':smt-lib-version';
-//SOURCE_TOK : ':source';
-//STATUS_TOK : ':status';
-//TRUE_TOK : 'true';
-//UNKNOWN_TOK : 'unknown';
-//UNSAT_TOK : 'unsat';
 
 // operators (NOTE: theory symbols go here)
 AMPERSAND_TOK     : '&';
@@ -605,15 +598,18 @@ WHITESPACE
   ;
 
 /**
- * Matches an integer constant from the input (non-empty sequence of digits, with
- * no leading zeroes).
+ * Matches an integer constant from the input (non-empty sequence of
+ * digits, with no leading zeroes).
  */
 INTEGER_LITERAL
   : NUMERAL
   ;
 
-/** Match an integer constant. In non-strict mode, this is any sequence of
- * digits. In strict mode, non-zero integers can't have leading zeroes. */
+/**
+ * Match an integer constant. In non-strict mode, this is any sequence
+ * of digits. In strict mode, non-zero integers can't have leading
+ * zeroes.
+ */
 fragment NUMERAL
 @init {
   char *start = (char*) GETCHARINDEX();
@@ -631,8 +627,8 @@ fragment NUMERAL
   ;
 
 /**
-  * Matches a decimal constant from the input.
-  */
+ * Matches a decimal constant from the input.
+ */
 DECIMAL_LITERAL
   : NUMERAL '.' DIGIT+
   ;
@@ -684,7 +680,8 @@ fragment DIGIT : '0'..'9';
 
 fragment HEX_DIGIT : DIGIT | 'a'..'f' | 'A'..'F';
 
-/** Matches the characters that may appear in a "symbol" (i.e., an identifier)
+/**
+ * Matches the characters that may appear in a "symbol" (i.e., an identifier)
  */
 fragment SYMBOL_CHAR
   : '+' | '-' | '/' | '*' | '=' | '%' | '?' | '!' | '.' | '$' | '_' | '~'
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index c4eceeb24..be4abb8ab 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -94,8 +94,10 @@ SmtEngine::SmtEngine(ExprManager* em, const Options* opts) throw () :
                                 d_theoryEngine, d_context);
   d_theoryEngine->setPropEngine(d_propEngine);
 
+  d_functions = new(true) FunctionMap(d_context);
+
   if(d_options->interactive) {
-    d_assertionList = new(true) CDList<Expr>(d_context);
+    d_assertionList = new(true) AssertionList(d_context);
   }
 }
 
@@ -110,7 +112,11 @@ SmtEngine::~SmtEngine() {
 
   shutdown();
 
-  ::delete d_assertionList;
+  if(d_assertionList != NULL) {
+    d_assertionList->deleteSelf();
+  }
+
+  d_functions->deleteSelf();
 
   delete d_theoryEngine;
   delete d_propEngine;
@@ -145,7 +151,7 @@ void SmtEngine::defineFunction(const string& name,
                                Type type,
                                Expr formula) {
   NodeManagerScope nms(d_nodeManager);
-  Unimplemented();
+  d_functions->insert(name, make_pair(make_pair(args, type), formula));
 }
 
 Node SmtEnginePrivate::preprocess(SmtEngine& smt, TNode n) {
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 56e38af7a..97772273d 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -25,9 +25,11 @@
 
 #include "expr/expr.h"
 #include "expr/expr_manager.h"
+#include "context/cdmap_forward.h"
 #include "util/result.h"
 #include "util/model.h"
 #include "util/sexpr.h"
+#include "util/hash.h"
 #include "smt/noninteractive_exception.h"
 #include "smt/bad_option.h"
 
@@ -69,36 +71,39 @@ namespace smt {
 class CVC4_PUBLIC SmtEngine {
 private:
 
+  /** A name/type pair, used for signatures */
+  typedef std::pair<std::string, Type> TypedArg;
+  /** A vector of typed formals, and a return type */
+  typedef std::pair<std::vector<TypedArg>, Type> FunctionSignature;
+  /** The type of our internal map of defined functions */
+  typedef context::CDMap<std::string, std::pair<FunctionSignature, Expr>,
+    StringHashFunction>
+    FunctionMap;
+
+  /** The type of our internal assertion list */
+  typedef context::CDList<Expr> AssertionList;
+
   /** Our Context */
   context::Context* d_context;
-
   /** Our expression manager */
   ExprManager* d_exprManager;
-
   /** Out internal expression/node manager */
   NodeManager* d_nodeManager;
-
   /** User-level options */
   const Options* d_options;
-
   /** The decision engine */
   DecisionEngine* d_decisionEngine;
-
   /** The decision engine */
   TheoryEngine* d_theoryEngine;
-
   /** The propositional engine */
   prop::PropEngine* d_propEngine;
-
+  /** An index of our defined functions */
+  FunctionMap* d_functions;
   /**
-   * The assertion list, before any conversion, for supporting
+   * The assertion list (before any conversion) for supporting
    * getAssertions().  Only maintained if in interactive mode.
    */
-  context::CDList<Expr>* d_assertionList;
-
-  // preprocess() and addFormula() used to be housed here; they are
-  // now in an SmtEnginePrivate class.  See the comment in
-  // smt_engine.cpp.
+  AssertionList* d_assertionList;
 
   /**
    * This is called by the destructor, just before destroying the
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"
diff --git a/src/util/hash.h b/src/util/hash.h
index 2ce2d2941..cca60ce76 100644
--- a/src/util/hash.h
+++ b/src/util/hash.h
@@ -17,6 +17,8 @@
  ** \todo document this file
  **/
 
+#include "cvc4_public.h"
+
 #ifndef __CVC4__HASH_H
 #define __CVC4__HASH_H