Partial merge from datatypes-merge branch:

1. Defines a new type "DatatypeType", a type-constant that holds a Datatype, describing an inductive data type.
2. CVC language parser supports datatypes.
3. CVC language printer now functional.
4. Minor other cleanups.

No performance impact is expected outside of datatypes.  I'm verifying that that is the case with a cluster job this morning.

14 files changed, 584 insertions, 62 deletions

diff --git a/src/expr/command.cpp b/src/expr/command.cpp
index 7c08293be..bcc96637f 100644
--- a/src/expr/command.cpp
+++ b/src/expr/command.cpp
@@ -2,10 +2,10 @@
 /*! \file command.cpp
  ** \verbatim
  ** Original author: mdeters
- ** Major contributors: dejan
- ** Minor contributors (to current version): none
+ ** Major contributors: none
+ ** Minor contributors (to current version): dejan
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009, 2010, 2011  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
@@ -498,6 +498,35 @@ void GetOptionCommand::toStream(std::ostream& out) const {
   out << "GetOption(" << d_flag << ")";
 }
 
+/* class DatatypeDeclarationCommand */
+
+DatatypeDeclarationCommand::DatatypeDeclarationCommand(const DatatypeType& datatype) :
+  d_datatypes() {
+  d_datatypes.push_back(datatype);
+  Debug("datatypes") << "Create datatype command." << endl;
+}
+
+DatatypeDeclarationCommand::DatatypeDeclarationCommand(const std::vector<DatatypeType>& datatypes) :
+  d_datatypes(datatypes) {
+  Debug("datatypes") << "Create datatype command." << endl;
+}
+
+void DatatypeDeclarationCommand::invoke(SmtEngine* smtEngine) {
+  Debug("datatypes") << "Invoke datatype command." << endl;
+  //smtEngine->addDatatypeDefinitions(d_datatype);
+}
+
+void DatatypeDeclarationCommand::toStream(std::ostream& out) const {
+  out << "DatatypeDeclarationCommand([";
+  for(vector<DatatypeType>::const_iterator i = d_datatypes.begin(),
+        i_end = d_datatypes.end();
+      i != i_end;
+      ++i) {
+    out << *i << ";" << endl;
+  }
+  out << "])";
+}
+
 /* output stream insertion operator for benchmark statuses */
 std::ostream& operator<<(std::ostream& out,
                          BenchmarkStatus status) {
diff --git a/src/expr/command.h b/src/expr/command.h
index fbb48b6b0..585e60eb4 100644
--- a/src/expr/command.h
+++ b/src/expr/command.h
@@ -2,10 +2,10 @@
 /*! \file command.h
  ** \verbatim
  ** Original author: mdeters
- ** Major contributors: cconway, dejan
- ** Minor contributors (to current version): none
+ ** Major contributors: dejan
+ ** Minor contributors (to current version): cconway
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009, 2010, 2011  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
@@ -28,11 +28,13 @@
 #include <sstream>
 #include <string>
 #include <vector>
+#include <map>
 
 #include "expr/expr.h"
 #include "expr/type.h"
 #include "util/result.h"
 #include "util/sexpr.h"
+#include "util/datatype.h"
 
 namespace CVC4 {
 
@@ -264,6 +266,16 @@ public:
   void printResult(std::ostream& out) const;
 };/* class GetOptionCommand */
 
+class CVC4_PUBLIC DatatypeDeclarationCommand : public Command {
+private:
+  std::vector<DatatypeType> d_datatypes;
+public:
+  DatatypeDeclarationCommand(const DatatypeType& datatype);
+  DatatypeDeclarationCommand(const std::vector<DatatypeType>& datatypes);
+  void invoke(SmtEngine* smtEngine);
+  void toStream(std::ostream& out) const;
+};/* class DatatypeDeclarationCommand */
+
 class CVC4_PUBLIC CommandSequence : public Command {
 private:
   /** All the commands to be executed (in sequence) */
diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index 6e8b6c63c..21fc0a4a1 100644
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -2,10 +2,10 @@
 /*! \file expr_manager_template.cpp
  ** \verbatim
  ** Original author: dejan
- ** Major contributors: mdeters, cconway
+ ** Major contributors: cconway, mdeters
  ** 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)
+ ** Copyright (c) 2009, 2010, 2011  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
@@ -22,13 +22,15 @@
 #include "util/options.h"
 #include "util/stats.h"
 
+#include <map>
+
 ${includes}
 
 // This is a hack, but an important one: if there's an error, the
 // compiler directs the user to the template file instead of the
 // generated one.  We don't want the user to modify the generated one,
 // since it'll get overwritten on a later build.
-#line 32 "${template}"
+#line 34 "${template}"
 
 #ifdef CVC4_STATISTICS_ON
   #define INC_STAT(kind) \
@@ -340,6 +342,63 @@ ArrayType ExprManager::mkArrayType(Type indexType, Type constituentType) const {
   return ArrayType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkArrayType(*indexType.d_typeNode, *constituentType.d_typeNode))));
 }
 
+DatatypeType ExprManager::mkDatatypeType(const Datatype& datatype) {
+  NodeManagerScope nms(d_nodeManager);
+  TypeNode* typeNode = new TypeNode(d_nodeManager->mkTypeConst(datatype));
+  Type type(d_nodeManager, typeNode);
+  DatatypeType dtt(type);
+  const Datatype& dt = typeNode->getConst<Datatype>();
+  if(!dt.isResolved()) {
+    std::map<std::string, DatatypeType> resolutions;
+    resolutions.insert(std::make_pair(datatype.getName(), dtt));
+    const_cast<Datatype&>(dt).resolve(this, resolutions);
+  }
+  return dtt;
+}
+
+std::vector<DatatypeType> ExprManager::mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes) {
+  NodeManagerScope nms(d_nodeManager);
+  std::map<std::string, DatatypeType> resolutions;
+  std::vector<DatatypeType> dtts;
+  for(std::vector<Datatype>::const_iterator i = datatypes.begin(), i_end = datatypes.end();
+      i != i_end;
+      ++i) {
+    TypeNode* typeNode = new TypeNode(d_nodeManager->mkTypeConst(*i));
+    Type type(d_nodeManager, typeNode);
+    DatatypeType dtt(type);
+    CheckArgument(resolutions.find((*i).getName()) == resolutions.end(),
+                  datatypes,
+                  "cannot construct two datatypes at the same time with the same name `%s'",
+                  (*i).getName().c_str());
+    resolutions.insert(std::make_pair((*i).getName(), dtt));
+    dtts.push_back(dtt);
+  }
+  for(std::vector<DatatypeType>::iterator i = dtts.begin(), i_end = dtts.end();
+      i != i_end;
+      ++i) {
+    const Datatype& dt = (*i).getDatatype();
+    if(!dt.isResolved()) {
+      const_cast<Datatype&>(dt).resolve(this, resolutions);
+    }
+  }
+  return dtts;
+}
+
+ConstructorType ExprManager::mkConstructorType(const Datatype::Constructor& constructor, Type range) const {
+  NodeManagerScope nms(d_nodeManager);
+  return Type(d_nodeManager, new TypeNode(d_nodeManager->mkConstructorType(constructor, *range.d_typeNode)));
+}
+
+SelectorType ExprManager::mkSelectorType(Type domain, Type range) const {
+  NodeManagerScope nms(d_nodeManager);
+  return Type(d_nodeManager, new TypeNode(d_nodeManager->mkSelectorType(*domain.d_typeNode, *range.d_typeNode)));
+}
+
+TesterType ExprManager::mkTesterType(Type domain) const {
+  NodeManagerScope nms(d_nodeManager);
+  return Type(d_nodeManager, new TypeNode(d_nodeManager->mkTesterType(*domain.d_typeNode)));
+}
+
 SortType ExprManager::mkSort(const std::string& name) const {
   NodeManagerScope nms(d_nodeManager);
   return SortType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkSort(name))));
diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h
index f51d6fa28..415d05878 100644
--- a/src/expr/expr_manager_template.h
+++ b/src/expr/expr_manager_template.h
@@ -5,7 +5,7 @@
  ** Major contributors: mdeters
  ** Minor contributors (to current version): taking, cconway
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009, 2010, 2011  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
@@ -241,20 +241,40 @@ public:
    */
   TupleType mkTupleType(const std::vector<Type>& types);
 
-  /** Make a type representing a bit-vector of the given size */
+  /** Make a type representing a bit-vector of the given size. */
   BitVectorType mkBitVectorType(unsigned size) const;
 
-  /** Make the type of arrays with the given parameterization */
+  /** Make the type of arrays with the given parameterization. */
   ArrayType mkArrayType(Type indexType, Type constituentType) const;
 
+  /** Make a type representing the given datatype. */
+  DatatypeType mkDatatypeType(const Datatype& datatype);
+
+  /**
+   * Make a set of types representing the given datatypes, which may be
+   * mutually recursive.
+   */
+  std::vector<DatatypeType> mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes);
+
+  /**
+   * Make a type representing a constructor with the given parameterization.
+   */
+  ConstructorType mkConstructorType(const Datatype::Constructor& constructor, Type range) const;
+
+  /** Make a type representing a selector with the given parameterization. */
+  SelectorType mkSelectorType(Type domain, Type range) const;
+
+  /** Make a type representing a tester with the given parameterization. */
+  TesterType mkTesterType(Type domain) const;
+
   /** Make a new sort with the given name. */
   SortType mkSort(const std::string& name) const;
 
-  /** Make a new sort from a constructor */
+  /** 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 */
+  /** Make a sort constructor from a name and arity. */
   SortConstructorType mkSortConstructor(const std::string& name,
                                         size_t arity) const;
 
diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h
index 1a9722939..489564d5f 100644
--- a/src/expr/expr_template.h
+++ b/src/expr/expr_template.h
@@ -18,6 +18,13 @@
 
 #include "cvc4_public.h"
 
+// putting the constant-payload #includes up here allows circularity
+// (some of them may require a completely-defined Expr type).  This
+// way, those #includes can forward-declare some stuff to get Expr's
+// getConst<> template instantiations correct, and then #include
+// "expr.h" safely, then go on to completely declare their own stuff.
+${includes}
+
 #ifndef __CVC4__EXPR_H
 #define __CVC4__EXPR_H
 
@@ -28,13 +35,11 @@
 #include "util/exception.h"
 #include "util/language.h"
 
-${includes}
-
 // This is a hack, but an important one: if there's an error, the
 // compiler directs the user to the template file instead of the
 // generated one.  We don't want the user to modify the generated one,
 // since it'll get overwritten on a later build.
-#line 38 "${template}"
+#line 43 "${template}"
 
 namespace CVC4 {
 
@@ -576,6 +581,31 @@ public:
   static inline void setDepth(std::ostream& out, long depth) {
     out.iword(s_iosIndex) = depth;
   }
+
+  /**
+   * Set the expression depth on the output stream for the current
+   * stack scope.  This makes sure the old depth is reset on the stream
+   * after normal OR exceptional exit from the scope, using the RAII
+   * C++ idiom.
+   */
+  class Scope {
+    std::ostream& d_out;
+    long d_oldDepth;
+
+  public:
+
+    inline Scope(std::ostream& out, long depth) :
+      d_out(out),
+      d_oldDepth(ExprSetDepth::getDepth(out)) {
+      ExprSetDepth::setDepth(out, depth);
+    }
+
+    inline ~Scope() {
+      ExprSetDepth::setDepth(d_out, d_oldDepth);
+    }
+
+  };/* class ExprSetDepth::Scope */
+
 };/* class ExprSetDepth */
 
 /**
@@ -621,6 +651,31 @@ public:
   static inline void setPrintTypes(std::ostream& out, bool printTypes) {
     out.iword(s_iosIndex) = printTypes;
   }
+
+  /**
+   * Set the print-types state on the output stream for the current
+   * stack scope.  This makes sure the old state is reset on the
+   * stream after normal OR exceptional exit from the scope, using the
+   * RAII C++ idiom.
+   */
+  class Scope {
+    std::ostream& d_out;
+    bool d_oldPrintTypes;
+
+  public:
+
+    inline Scope(std::ostream& out, bool printTypes) :
+      d_out(out),
+      d_oldPrintTypes(ExprPrintTypes::getPrintTypes(out)) {
+      ExprPrintTypes::setPrintTypes(out, printTypes);
+    }
+
+    inline ~Scope() {
+      ExprPrintTypes::setPrintTypes(d_out, d_oldPrintTypes);
+    }
+
+  };/* class ExprPrintTypes::Scope */
+
 };/* class ExprPrintTypes */
 
 /**
@@ -668,13 +723,38 @@ public:
     // (offset by one to detect whether default has been set yet)
     out.iword(s_iosIndex) = int(l) + 1;
   }
+
+  /**
+   * Set a language on the output stream for the current stack scope.
+   * This makes sure the old language is reset on the stream after
+   * normal OR exceptional exit from the scope, using the RAII C++
+   * idiom.
+   */
+  class Scope {
+    std::ostream& d_out;
+    OutputLanguage d_oldLanguage;
+
+  public:
+
+    inline Scope(std::ostream& out, OutputLanguage language) :
+      d_out(out),
+      d_oldLanguage(ExprSetLanguage::getLanguage(out)) {
+      ExprSetLanguage::setLanguage(out, language);
+    }
+
+    inline ~Scope() {
+      ExprSetLanguage::setLanguage(d_out, d_oldLanguage);
+    }
+
+  };/* class ExprSetLanguage::Scope */
+
 };/* class ExprSetLanguage */
 
 }/* CVC4::expr namespace */
 
 ${getConst_instantiations}
 
-#line 676 "${template}"
+#line 682 "${template}"
 
 namespace expr {
 
diff --git a/src/expr/mkexpr b/src/expr/mkexpr
index 40bf9992c..da2847d84 100755
--- a/src/expr/mkexpr
+++ b/src/expr/mkexpr
@@ -138,25 +138,26 @@ function constant {
   includes="${includes}
 #include \"$4\""
   mkConst_instantiations="${mkConst_instantiations}
-template <>
-Expr ExprManager::mkConst($2 const& val);
+#line $lineno \"$kf\"
+template <> Expr ExprManager::mkConst($2 const& val);
 "
   mkConst_implementations="${mkConst_implementations}
-template <>
-Expr ExprManager::mkConst($2 const& val) {
+#line $lineno \"$kf\"
+template <> Expr ExprManager::mkConst($2 const& val) {
+#line $lineno \"$kf\"
   return Expr(this, new Node(d_nodeManager->mkConst< $2 >(val)));
 }
 "
   getConst_instantiations="${getConst_instantiations}
-template <>
-$2 const & Expr::getConst< $2 >() const;
+#line $lineno \"$kf\"
+template <> $2 const & Expr::getConst< $2 >() const;
 "
   getConst_implementations="${getConst_implementations}
-template <>
-$2 const & Expr::getConst() const {
-  // check even for production builds
-  CheckArgument(getKind() == ::CVC4::kind::$1, *this,
-                \"Improper kind for getConst<$2>()\");
+#line $lineno \"$kf\"
+template <> $2 const & Expr::getConst() const {
+#line $lineno \"$kf\"
+  CheckArgument(getKind() == ::CVC4::kind::$1, *this, \"Improper kind for getConst<$2>()\");
+#line $lineno \"$kf\"
   return d_node->getConst< $2 >();
 }
 "
diff --git a/src/expr/mkkind b/src/expr/mkkind
index 631f73a89..f7f6ba836 100755
--- a/src/expr/mkkind
+++ b/src/expr/mkkind
@@ -74,7 +74,7 @@ function theory {
 
   theory_id="$1"
   theory_enum="$1,
-    ${theory_enum}"
+  ${theory_enum}"
   theory_descriptions="${theory_descriptions}    case ${theory_id}: out << \"${theory_id}\"; break;
 "
 }
diff --git a/src/expr/node.h b/src/expr/node.h
index 2509640e0..d3775cb3f 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -813,7 +813,7 @@ namespace CVC4 {
 
 // for hash_maps, hash_sets..
 struct NodeHashFunction {
-  size_t operator()(const CVC4::Node& node) const {
+  size_t operator()(CVC4::Node node) const {
     return (size_t) node.getId();
   }
 };/* struct NodeHashFunction */
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index 793b701f8..9449594e3 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -2,10 +2,10 @@
 /*! \file node_manager.cpp
  ** \verbatim
  ** Original author: mdeters
- ** Major contributors: cconway, dejan
- ** Minor contributors (to current version): acsys, taking
+ ** Major contributors: cconway
+ ** Minor contributors (to current version): acsys, taking, dejan
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009, 2010, 2011  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
@@ -26,6 +26,7 @@
 #include "theory/arith/theory_arith_type_rules.h"
 #include "theory/arrays/theory_arrays_type_rules.h"
 #include "theory/bv/theory_bv_type_rules.h"
+#include "theory/datatypes/theory_datatypes_type_rules.h"
 
 #include "util/Assert.h"
 #include "util/options.h"
@@ -434,6 +435,15 @@ TypeNode NodeManager::computeType(TNode n, bool check)
   case kind::BITVECTOR_SIGN_EXTEND:
     typeNode = CVC4::theory::bv::BitVectorExtendTypeRule::computeType(this, n, check);
     break;
+  case kind::APPLY_CONSTRUCTOR:
+    typeNode = CVC4::theory::datatypes::DatatypeConstructorTypeRule::computeType(this, n, check);
+    break;
+  case kind::APPLY_SELECTOR:
+    typeNode = CVC4::theory::datatypes::DatatypeSelectorTypeRule::computeType(this, n, check);
+    break;
+  case kind::APPLY_TESTER:
+    typeNode = CVC4::theory::datatypes::DatatypeTesterTypeRule::computeType(this, n, check);
+    break;
   default:
     Debug("getType") << "FAILURE" << std::endl;
     Unhandled(n.getKind());
@@ -509,4 +519,20 @@ TypeNode NodeManager::getType(TNode n, bool check)
   return typeNode;
 }
 
+TypeNode NodeManager::mkConstructorType(const Datatype::Constructor& constructor, TypeNode range) {
+  std::vector<TypeNode> sorts;
+  Debug("datatypes") << "ctor name: " << constructor.getName() << std::endl;
+  for(Datatype::Constructor::const_iterator i = constructor.begin();
+      i != constructor.end();
+      ++i) {
+    Debug("datatypes") << *(*i).getSelector().getType().d_typeNode << std::endl;
+    TypeNode sort = (*(*i).getSelector().getType().d_typeNode)[1];
+    Debug("datatypes") << "ctor sort: " << sort << std::endl;
+    sorts.push_back(sort);
+  }
+  Debug("datatypes") << "ctor range: " << range << std::endl;
+  sorts.push_back(range);
+  return mkTypeNode(kind::CONSTRUCTOR_TYPE, sorts);
+}
+
 }/* CVC4 namespace */
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 1760f48c7..7f7d37a52 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -5,7 +5,7 @@
  ** Major contributors: cconway, dejan
  ** Minor contributors (to current version): acsys, taking
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009, 2010, 2011  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
@@ -55,8 +55,8 @@ namespace attr {
   struct SortArityTag {};
 }/* CVC4::expr::attr namespace */
 
-typedef expr::Attribute<attr::VarNameTag, std::string> VarNameAttr;
-typedef expr::Attribute<attr::SortArityTag, uint64_t> SortArityAttr;
+typedef Attribute<attr::VarNameTag, std::string> VarNameAttr;
+typedef Attribute<attr::SortArityTag, uint64_t> SortArityAttr;
 
 }/* CVC4::expr namespace */
 
@@ -542,6 +542,15 @@ public:
   /** Make the type of arrays with the given parameterization */
   inline TypeNode mkArrayType(TypeNode indexType, TypeNode constituentType);
 
+  /** Make a type representing a constructor with the given parameterization */
+  TypeNode mkConstructorType(const Datatype::Constructor& constructor, TypeNode range);
+
+  /** Make a type representing a selector with the given parameterization */
+  inline TypeNode mkSelectorType(TypeNode domain, TypeNode range);
+
+  /** Make a type representing a tester with given parameterization */
+  inline TypeNode mkTesterType(TypeNode domain);
+
   /** Make a new (anonymous) sort of arity 0. */
   inline TypeNode mkSort();
 
@@ -796,6 +805,14 @@ inline TypeNode NodeManager::mkArrayType(TypeNode indexType,
   return mkTypeNode(kind::ARRAY_TYPE, indexType, constituentType);
 }
 
+inline TypeNode NodeManager::mkSelectorType(TypeNode domain, TypeNode range) {
+  return mkTypeNode(kind::SELECTOR_TYPE, domain, range);
+}
+
+inline TypeNode NodeManager::mkTesterType(TypeNode domain) {
+  return mkTypeNode(kind::TESTER_TYPE, domain );
+}
+
 inline expr::NodeValue* NodeManager::poolLookup(expr::NodeValue* nv) const {
   NodeValuePool::const_iterator find = d_nodeValuePool.find(nv);
   if(find == d_nodeValuePool.end()) {
diff --git a/src/expr/type.cpp b/src/expr/type.cpp
index 78554f61f..6dd9c5cec 100644
--- a/src/expr/type.cpp
+++ b/src/expr/type.cpp
@@ -2,10 +2,10 @@
 /*! \file type.cpp
  ** \verbatim
  ** Original author: cconway
- ** Major contributors: mdeters, dejan
+ ** Major contributors: dejan, mdeters
  ** 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)
+ ** Copyright (c) 2009, 2010, 2011  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
@@ -186,6 +186,58 @@ Type::operator BitVectorType() const throw(AssertionException) {
   return BitVectorType(*this);
 }
 
+/** Cast to a Constructor type */
+Type::operator DatatypeType() const throw(AssertionException) {
+  NodeManagerScope nms(d_nodeManager);
+  Assert(isDatatype());
+  return DatatypeType(*this);
+}
+
+/** Is this the Datatype type? */
+bool Type::isDatatype() const {
+  NodeManagerScope nms(d_nodeManager);
+  return d_typeNode->isDatatype();
+}
+
+/** Cast to a Constructor type */
+Type::operator ConstructorType() const throw(AssertionException) {
+  NodeManagerScope nms(d_nodeManager);
+  Assert(isConstructor());
+  return ConstructorType(*this);
+}
+
+/** Is this the Constructor type? */
+bool Type::isConstructor() const {
+  NodeManagerScope nms(d_nodeManager);
+  return d_typeNode->isConstructor();
+}
+
+/** Cast to a Selector type */
+Type::operator SelectorType() const throw(AssertionException) {
+  NodeManagerScope nms(d_nodeManager);
+  Assert(isSelector());
+  return SelectorType(*this);
+}
+
+/** Is this the Selector type? */
+bool Type::isSelector() const {
+  NodeManagerScope nms(d_nodeManager);
+  return d_typeNode->isSelector();
+}
+
+/** Cast to a Tester type */
+Type::operator TesterType() const throw(AssertionException) {
+  NodeManagerScope nms(d_nodeManager);
+  Assert(isTester());
+  return TesterType(*this);
+}
+
+/** Is this the Tester type? */
+bool Type::isTester() const {
+  NodeManagerScope nms(d_nodeManager);
+  return d_typeNode->isTester();
+}
+
 /** Is this a function type? */
 bool Type::isFunction() const {
   NodeManagerScope nms(d_nodeManager);
@@ -349,6 +401,26 @@ BitVectorType::BitVectorType(const Type& t) throw(AssertionException) :
   Assert(isBitVector());
 }
 
+DatatypeType::DatatypeType(const Type& t) throw(AssertionException) :
+  Type(t) {
+  Assert(isDatatype());
+}
+
+ConstructorType::ConstructorType(const Type& t) throw(AssertionException) :
+  Type(t) {
+  Assert(isConstructor());
+}
+
+SelectorType::SelectorType(const Type& t) throw(AssertionException) :
+  Type(t) {
+  Assert(isSelector());
+}
+
+TesterType::TesterType(const Type& t) throw(AssertionException) :
+  Type(t) {
+  Assert(isTester());
+}
+
 FunctionType::FunctionType(const Type& t) throw(AssertionException) :
   Type(t) {
   Assert(isFunction());
@@ -392,8 +464,32 @@ Type ArrayType::getConstituentType() const {
   return makeType(d_typeNode->getArrayConstituentType());
 }
 
-size_t TypeHashStrategy::hash(const Type& t) {
-  return TypeNodeHashStrategy::hash(*t.d_typeNode);
+Type ConstructorType::getReturnType() const {
+  return makeType(d_typeNode->getConstructorReturnType());
+}
+
+const Datatype& DatatypeType::getDatatype() const {
+  return d_typeNode->getConst<Datatype>();
+}
+
+DatatypeType SelectorType::getDomain() const {
+  return DatatypeType(makeType((*d_typeNode)[0]));
+}
+
+Type SelectorType::getRangeType() const {
+  return makeType((*d_typeNode)[1]);
+}
+
+DatatypeType TesterType::getDomain() const {
+  return DatatypeType(makeType((*d_typeNode)[0]));
+}
+
+BooleanType TesterType::getRangeType() const {
+  return BooleanType(makeType(d_nodeManager->booleanType()));
+}
+
+size_t TypeHashFunction::operator()(const Type& t) {
+  return TypeNodeHashFunction()(NodeManager::fromType(t));
 }
 
 }/* CVC4 namespace */
diff --git a/src/expr/type.h b/src/expr/type.h
index 130aa3122..3b476ddf5 100644
--- a/src/expr/type.h
+++ b/src/expr/type.h
@@ -5,7 +5,7 @@
  ** Major contributors: mdeters, dejan
  ** 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)
+ ** Copyright (c) 2009, 2010, 2011  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
@@ -36,6 +36,8 @@ class TypeNode;
 
 class SmtEngine;
 
+class Datatype;
+
 template <bool ref_count>
 class NodeTemplate;
 
@@ -44,6 +46,10 @@ class IntegerType;
 class RealType;
 class BitVectorType;
 class ArrayType;
+class DatatypeType;
+class ConstructorType;
+class SelectorType;
+class TesterType;
 class FunctionType;
 class TupleType;
 class KindType;
@@ -52,10 +58,10 @@ class SortConstructorType;
 class Type;
 
 /** Strategy for hashing Types */
-struct CVC4_PUBLIC TypeHashStrategy {
+struct CVC4_PUBLIC TypeHashFunction {
   /** Return a hash code for type t */
-  static size_t hash(const CVC4::Type& t);
-};/* struct TypeHashStrategy */
+  size_t operator()(const CVC4::Type& t);
+};/* struct TypeHashFunction */
 
 /**
  * Output operator for types
@@ -259,6 +265,54 @@ public:
   operator ArrayType() const throw(AssertionException);
 
   /**
+   * Is this a datatype type?
+   * @return true if the type is a datatype type
+   */
+  bool isDatatype() const;
+
+  /**
+   * Cast this type to a datatype type
+   * @return the DatatypeType
+   */
+  operator DatatypeType() const throw(AssertionException);
+
+  /**
+   * Is this a constructor type?
+   * @return true if the type is a constructor type
+   */
+  bool isConstructor() const;
+
+  /**
+   * Cast this type to a constructor type
+   * @return the ConstructorType
+   */
+  operator ConstructorType() const throw(AssertionException);
+
+  /**
+   * Is this a selector type?
+   * @return true if the type is a selector type
+   */
+  bool isSelector() const;
+
+  /**
+   * Cast this type to a selector type
+   * @return the SelectorType
+   */
+  operator SelectorType() const throw(AssertionException);
+
+  /**
+   * Is this a tester type?
+   * @return true if the type is a tester type
+   */
+  bool isTester() const;
+
+  /**
+   * Cast this type to a tester type
+   * @return the TesterType
+   */
+  operator TesterType() const throw(AssertionException);
+
+  /**
    * Is this a sort kind?
    * @return true if this is a sort kind
    */
@@ -449,6 +503,78 @@ public:
   unsigned getSize() const;
 };/* class BitVectorType */
 
+
+/**
+ * Class encapsulating the datatype type
+ */
+class CVC4_PUBLIC DatatypeType : public Type {
+
+public:
+
+  /** Construct from the base type */
+  DatatypeType(const Type& type) throw(AssertionException);
+
+  /** Get the underlying datatype */
+  const Datatype& getDatatype() const;
+
+};/* class DatatypeType */
+
+
+/**
+ * Class encapsulating the constructor type
+ */
+class CVC4_PUBLIC ConstructorType : public Type {
+
+public:
+
+  /** Construct from the base type */
+  ConstructorType(const Type& type) throw(AssertionException);
+
+  /** Get the return type */
+  Type getReturnType() const;
+
+};/* class ConstructorType */
+
+
+/**
+ * Class encapsulating the Selector type
+ */
+class CVC4_PUBLIC SelectorType : public Type {
+
+public:
+
+  /** Construct from the base type */
+  SelectorType(const Type& type) throw(AssertionException);
+
+  /** Get the domain type for this selector (the datatype type) */
+  DatatypeType getDomain() const;
+
+  /** Get the range type for this selector (the field type) */
+  Type getRangeType() const;
+
+};/* class SelectorType */
+
+/**
+ * Class encapsulating the Tester type
+ */
+class CVC4_PUBLIC TesterType : public Type {
+
+public:
+
+  /** Construct from the base type */
+  TesterType(const Type& type) throw(AssertionException);
+
+  /** Get the type that this tester tests (the datatype type) */
+  DatatypeType getDomain() const;
+
+  /**
+   * Get the range type for this tester (included for sake of
+   * interface completeness), but doesn't give useful information).
+   */
+  BooleanType getRangeType() const;
+
+};/* class TesterType */
+
 }/* CVC4 namespace */
 
 #endif /* __CVC4__TYPE_H */
diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp
index badc3b72f..7549af895 100644
--- a/src/expr/type_node.cpp
+++ b/src/expr/type_node.cpp
@@ -5,7 +5,7 @@
  ** Major contributors: mdeters
  ** Minor contributors (to current version): taking
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009, 2010, 2011  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
@@ -76,28 +76,38 @@ TypeNode TypeNode::getArrayConstituentType() const {
   return (*this)[1];
 }
 
-/** Is this a function type? */
+TypeNode TypeNode::getConstructorReturnType() const {
+  Assert(isConstructor());
+  return (*this)[getNumChildren()-1];
+}
+
 bool TypeNode::isFunction() const {
   return getKind() == kind::FUNCTION_TYPE;
 }
 
-/** Is this a predicate type? NOTE: all predicate types are also
-    function types. */
 bool TypeNode::isPredicate() const {
   return isFunction() && getRangeType().isBoolean();
 }
 
-vector<TypeNode> TypeNode::getArgTypes() const {
-  Assert(isFunction());
+std::vector<TypeNode> TypeNode::getArgTypes() const {
   vector<TypeNode> args;
-  for(unsigned i = 0, i_end = getNumChildren() - 1; i < i_end; ++i) {
-    args.push_back((*this)[i]);
+  if(isTester()) {
+    Assert(getNumChildren() == 1);
+    args.push_back((*this)[0]);
+  } else {
+    Assert(isFunction() || isConstructor() || isSelector());
+    for(unsigned i = 0, i_end = getNumChildren() - 1; i < i_end; ++i) {
+      args.push_back((*this)[i]);
+    }
   }
   return args;
 }
 
 TypeNode TypeNode::getRangeType() const {
-  Assert(isFunction());
+  if(isTester()) {
+    return NodeManager::currentNM()->booleanType();
+  }
+  Assert(isFunction() || isConstructor() || isSelector());
   return (*this)[getNumChildren()-1];
 }
 
@@ -137,6 +147,26 @@ bool TypeNode::isBitVector() const {
   return getKind() == kind::BITVECTOR_TYPE;
 }
 
+/** Is this a datatype type */
+bool TypeNode::isDatatype() const {
+  return getKind() == kind::DATATYPE_TYPE;
+}
+
+/** Is this a constructor type */
+bool TypeNode::isConstructor() const {
+  return getKind() == kind::CONSTRUCTOR_TYPE;
+}
+
+/** Is this a selector type */
+bool TypeNode::isSelector() const {
+  return getKind() == kind::SELECTOR_TYPE;
+}
+
+/** Is this a tester type */
+bool TypeNode::isTester() const {
+  return getKind() == kind::TESTER_TYPE;
+}
+
 /** Is this a bit-vector type of size <code>size</code> */
 bool TypeNode::isBitVector(unsigned size) const {
   return getKind() == kind::BITVECTOR_TYPE &&
diff --git a/src/expr/type_node.h b/src/expr/type_node.h
index ead85cd19..049173867 100644
--- a/src/expr/type_node.h
+++ b/src/expr/type_node.h
@@ -5,7 +5,7 @@
  ** Major contributors: mdeters
  ** Minor contributors (to current version): taking
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009, 2010, 2011  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
@@ -360,18 +360,32 @@ public:
   /** Get the element type (for array types) */
   TypeNode getArrayConstituentType() const;
 
-  /** Is this a function type? */
+  /** Get the return type (for constructor types) */
+  TypeNode getConstructorReturnType() const;
+
+  /**
+   * Is this a function type?  Function-like things (e.g. datatype
+   * selectors) that aren't actually functions are NOT considered
+   * functions, here.
+   */
   bool isFunction() const;
 
-  /** Get the argument types */
+  /**
+   * Get the argument types of a function, datatype constructor,
+   * datatype selector, or datatype tester.
+   */
   std::vector<TypeNode> getArgTypes() const;
 
-  /** Get the range type (i.e., the type of the result). */
+  /**
+   * Get the range type (i.e., the type of the result) of a function,
+   * datatype constructor, datatype selector, or datatype tester.
+   */
   TypeNode getRangeType() const;
 
   /**
    * Is this a predicate type?
-   * NOTE: all predicate types are also function types.
+   * NOTE: all predicate types are also function types (so datatype
+   * testers are not considered "predicates" for the purpose of this function).
    */
   bool isPredicate() const;
 
@@ -387,6 +401,18 @@ public:
   /** Is this a bit-vector type of size <code>size</code> */
   bool isBitVector(unsigned size) const;
 
+  /** Is this a datatype type */
+  bool isDatatype() const;
+
+  /** Is this a constructor type */
+  bool isConstructor() const;
+
+  /** Is this a selector type */
+  bool isSelector() const;
+
+  /** Is this a tester type */
+  bool isTester() const;
+
   /** Get the size of this bit-vector type */
   unsigned getBitVectorSize() const;
 
@@ -430,11 +456,11 @@ inline std::ostream& operator<<(std::ostream& out, const TypeNode& n) {
 }
 
 // for hash_maps, hash_sets..
-struct TypeNodeHashStrategy {
-  static inline size_t hash(const TypeNode& node) {
+struct TypeNodeHashFunction {
+  size_t operator()(TypeNode node) const {
     return (size_t) node.getId();
   }
-};/* struct TypeNodeHashStrategy */
+};/* struct TypeNodeHashFunction */
 
 }/* CVC4 namespace */