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.

1 files changed, 20 insertions, 3 deletions

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()) {