Tuesday end-of-day commit.

Expected performance impact outside of datatypes/CVC parser is
negligible.

* CVC language LAMBDA, functional LET, type LET, precedence fixes,
  bitvectors, and arrays, with partial parsing support also for
  quantifiers, tuples, subranges, subtypes, and records
* support for complex recursive DATATYPE selectors, e.g.
    tree = node(children:ARRAY INT OF tree) | leaf(data:INT)
  these are complicated because they have to be left unresolved
  at parse time and dealt with in a second pass.
* bugfix for Exprs/Types that occurred when setting them to null
  (not Nodes/TypeNodes, just Exprs/Types).
* Cleanup/code review items

15 files changed, 311 insertions, 65 deletions

diff --git a/src/expr/declaration_scope.cpp b/src/expr/declaration_scope.cpp
index 09aa3ed9f..cfcc62335 100644
--- a/src/expr/declaration_scope.cpp
+++ b/src/expr/declaration_scope.cpp
@@ -2,10 +2,10 @@
 /*! \file declaration_scope.cpp
  ** \verbatim
  ** Original author: cconway
- ** Major contributors: none
- ** Minor contributors (to current version): dejan, mdeters
+ ** Major contributors: mdeters
+ ** 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
@@ -174,4 +174,8 @@ void DeclarationScope::pushScope() throw() {
   d_context->push();
 }
 
-} // namespace CVC4
+size_t DeclarationScope::getLevel() const throw() {
+  return d_context->getLevel();
+}
+
+}/* CVC4 namespace */
diff --git a/src/expr/declaration_scope.h b/src/expr/declaration_scope.h
index 17140c850..6d89f5f4e 100644
--- a/src/expr/declaration_scope.h
+++ b/src/expr/declaration_scope.h
@@ -2,10 +2,10 @@
 /*! \file declaration_scope.h
  ** \verbatim
  ** Original author: cconway
- ** Major contributors: none
- ** Minor contributors (to current version): dejan, mdeters
+ ** Major contributors: 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
@@ -49,7 +49,7 @@ class CVC4_PUBLIC ScopeException : public Exception {
  */
 class CVC4_PUBLIC DeclarationScope {
   /** The context manager for the scope maps. */
-  context::Context *d_context;
+  context::Context* d_context;
 
   /** A map for expressions. */
   context::CDMap<std::string, Expr, StringHashFunction> *d_exprMap;
@@ -180,6 +180,9 @@ public:
   /** Push a scope level. */
   void pushScope() throw();
 
+  /** Get the current level of this declaration scope. */
+  size_t getLevel() const throw();
+
 };/* class DeclarationScope */
 
 }/* CVC4 namespace */
diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index 870c77383..b116a4671 100644
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -475,47 +475,137 @@ ArrayType ExprManager::mkArrayType(Type indexType, Type constituentType) const {
 }
 
 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;
+  // Not worth a special implementation; this doesn't need to be fast
+  // code anyway..
+  vector<Datatype> datatypes;
+  datatypes.push_back(datatype);
+  vector<DatatypeType> result = mkMutualDatatypeTypes(datatypes);
+  Assert(result.size() == 1);
+  return result.front();
 }
 
-std::vector<DatatypeType> ExprManager::mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes) {
+std::vector<DatatypeType>
+ExprManager::mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes) {
+  return mkMutualDatatypeTypes(datatypes, set<SortType>());
+}
+
+std::vector<DatatypeType>
+ExprManager::mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes,
+                                   const std::set<SortType>& unresolvedTypes) {
   NodeManagerScope nms(d_nodeManager);
-  std::map<std::string, DatatypeType> resolutions;
+  std::map<std::string, DatatypeType> nameResolutions;
   std::vector<DatatypeType> dtts;
-  for(std::vector<Datatype>::const_iterator i = datatypes.begin(), i_end = datatypes.end();
+
+  // First do some sanity checks, set up the final Type to be used for
+  // each datatype, and set up the "named resolutions" used to handle
+  // simple self- and mutual-recursion, for example in the definition
+  // "nat = succ(pred:nat) | zero", a named resolution can handle the
+  // pred selector.
+  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(),
+    CheckArgument(nameResolutions.find((*i).getName()) == nameResolutions.end(),
                   datatypes,
-                  "cannot construct two datatypes at the same time with the same name `%s'",
+                  "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));
+    nameResolutions.insert(std::make_pair((*i).getName(), dtt));
     dtts.push_back(dtt);
   }
-  for(std::vector<DatatypeType>::iterator i = dtts.begin(), i_end = dtts.end();
+
+  // Second, set up the type substitution map for complex type
+  // resolution (e.g. if "list" is the type we're defining, and it has
+  // a selector of type "ARRAY INT OF list", this can't be taken care
+  // of using the named resolutions that we set up above.  A
+  // preliminary array type was set up, and now needs to have "list"
+  // substituted in it for the correct type.
+  //
+  // @TODO get rid of named resolutions altogether and handle
+  // everything with these resolutions?
+  std::vector<Type> placeholders;// to hold the "unresolved placeholders"
+  std::vector<Type> replacements;// to hold our final, resolved types
+  for(std::set<SortType>::const_iterator i = unresolvedTypes.begin(),
+        i_end = unresolvedTypes.end();
+      i != i_end;
+      ++i) {
+    std::string name = (*i).getName();
+    std::map<std::string, DatatypeType>::const_iterator resolver =
+      nameResolutions.find(name);
+    CheckArgument(resolver != nameResolutions.end(),
+                  unresolvedTypes,
+                  "cannot resolve type `%s'; it's not among "
+                  "the datatypes being defined", name.c_str());
+    // We will instruct the Datatype to substitute "*i" (the
+    // unresolved SortType used as a placeholder in complex types)
+    // with "(*resolver).second" (the DatatypeType we created in the
+    // first step, above).
+    placeholders.push_back(*i);
+    replacements.push_back((*resolver).second);
+  }
+
+  // Lastly, perform the final resolutions and checks.
+  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);
+      const_cast<Datatype&>(dt).resolve(this, nameResolutions,
+                                        placeholders, replacements);
     }
+
+    // Now run some checks, including a check to make sure that no
+    // selector is function-valued.
+    checkResolvedDatatype(*i);
   }
+
   return dtts;
 }
 
+void ExprManager::checkResolvedDatatype(DatatypeType dtt) const {
+  const Datatype& dt = dtt.getDatatype();
+
+  AssertArgument(dt.isResolved(), dtt, "datatype should have been resolved");
+
+  // for all constructors...
+  for(Datatype::const_iterator i = dt.begin(), i_end = dt.end();
+      i != i_end;
+      ++i) {
+    const Datatype::Constructor& c = *i;
+    Type testerType CVC4_UNUSED = c.getTester().getType();
+    Assert(c.isResolved() &&
+           testerType.isTester() &&
+           TesterType(testerType).getDomain() == dtt &&
+           TesterType(testerType).getRangeType() == booleanType(),
+           "malformed tester in datatype post-resolution");
+    Type ctorType CVC4_UNUSED = c.getConstructor().getType();
+    Assert(ctorType.isConstructor() &&
+           ConstructorType(ctorType).getArity() == c.getNumArgs() &&
+           ConstructorType(ctorType).getReturnType() == dtt,
+           "malformed constructor in datatype post-resolution");
+    // for all selectors...
+    for(Datatype::Constructor::const_iterator j = c.begin(), j_end = c.end();
+        j != j_end;
+        ++j) {
+      const Datatype::Constructor::Arg& a = *j;
+      Type selectorType = a.getSelector().getType();
+      Assert(a.isResolved() &&
+             selectorType.isSelector() &&
+             SelectorType(selectorType).getDomain() == dtt,
+             "malformed selector in datatype post-resolution");
+      // This next one's a "hard" check, performed in non-debug builds
+      // as well; the other ones should all be guaranteed by the
+      // CVC4::Datatype class, but this actually needs to be checked.
+      AlwaysAssert(!SelectorType(selectorType).getRangeType().d_typeNode->isFunctionLike(),
+                   "cannot put function-like things in datatypes");
+    }
+  }
+}
+
 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)));
diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h
index 31ce7855a..b7f376811 100644
--- a/src/expr/expr_manager_template.h
+++ b/src/expr/expr_manager_template.h
@@ -72,6 +72,11 @@ private:
   context::Context* getContext() const;
 
   /**
+   * Check some things about a newly-created DatatypeType.
+   */
+  void checkResolvedDatatype(DatatypeType dtt) const;
+
+  /**
    * SmtEngine will use all the internals, so it will grab the
    * NodeManager.
    */
@@ -319,7 +324,41 @@ public:
    * Make a set of types representing the given datatypes, which may be
    * mutually recursive.
    */
-  std::vector<DatatypeType> mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes);
+  std::vector<DatatypeType>
+  mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes);
+
+  /**
+   * Make a set of types representing the given datatypes, which may
+   * be mutually recursive.  unresolvedTypes is a set of SortTypes
+   * that were used as placeholders in the Datatypes for the Datatypes
+   * of the same name.  This is just a more complicated version of the
+   * above mkMutualDatatypeTypes() function, but is required to handle
+   * complex types.
+   *
+   * For example, unresolvedTypes might contain the single sort "list"
+   * (with that name reported from SortType::getName()).  The
+   * datatypes list might have the single datatype
+   *
+   *   DATATYPE
+   *     list = cons(car:ARRAY INT OF list, cdr:list) | nil;
+   *   END;
+   *
+   * To represent the Type of the array, the user had to create a
+   * placeholder type (an uninterpreted sort) to stand for "list" in
+   * the type of "car".  It is this placeholder sort that should be
+   * passed in unresolvedTypes.  If the datatype was of the simpler
+   * form:
+   *
+   *   DATATYPE
+   *     list = cons(car:list, cdr:list) | nil;
+   *   END;
+   *
+   * then no complicated Type needs to be created, and the above,
+   * simpler form of mkMutualDatatypeTypes() is enough.
+   */
+  std::vector<DatatypeType>
+  mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes,
+                        const std::set<SortType>& unresolvedTypes);
 
   /**
    * Make a type representing a constructor with the given parameterization.
diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp
index f6d346630..51a734757 100644
--- a/src/expr/expr_template.cpp
+++ b/src/expr/expr_template.cpp
@@ -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
@@ -117,10 +117,24 @@ Expr& Expr::operator=(const Expr& e) {
   Assert(d_node != NULL, "Unexpected NULL expression pointer!");
   Assert(e.d_node != NULL, "Unexpected NULL expression pointer!");
 
-  ExprManagerScope ems(*this);
-  *d_node = *e.d_node;
-  d_exprManager = e.d_exprManager;
+  if(this != &e) {
+    if(d_exprManager == e.d_exprManager) {
+      ExprManagerScope ems(*this);
+      *d_node = *e.d_node;
+    } else {
+      // This happens more than you think---every time you set to or
+      // from the null Expr.  It's tricky because each node manager
+      // must be in play at the right time.
+
+      ExprManagerScope ems1(*this);
+      *d_node = Node::null();
 
+      ExprManagerScope ems2(e);
+      *d_node = *e.d_node;
+
+      d_exprManager = e.d_exprManager;
+    }
+  }
   return *this;
 }
 
diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h
index 489564d5f..c45cc9b99 100644
--- a/src/expr/expr_template.h
+++ b/src/expr/expr_template.h
@@ -754,7 +754,7 @@ public:
 
 ${getConst_instantiations}
 
-#line 682 "${template}"
+#line 758 "${template}"
 
 namespace expr {
 
diff --git a/src/expr/kind_template.h b/src/expr/kind_template.h
index 932ec31c8..6b9787f6c 100644
--- a/src/expr/kind_template.h
+++ b/src/expr/kind_template.h
@@ -2,10 +2,10 @@
 /*! \file kind_template.h
  ** \verbatim
  ** Original author: mdeters
- ** Major contributors: none
+ ** Major contributors: 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
@@ -95,7 +95,7 @@ struct KindHashStrategy {
  * The enumeration for the built-in atomic types.
  */
 enum TypeConstant {
-  ${type_constant_list}
+${type_constant_list}
   LAST_TYPE
 };/* enum TypeConstant */
 
@@ -110,7 +110,7 @@ struct TypeConstantHashStrategy {
 
 inline std::ostream& operator<<(std::ostream& out, TypeConstant typeConstant) {
   switch(typeConstant) {
-  ${type_constant_descriptions}
+${type_constant_descriptions}
   default:
     out << "UNKNOWN_TYPE_CONSTANT";
     break;
@@ -121,13 +121,13 @@ inline std::ostream& operator<<(std::ostream& out, TypeConstant typeConstant) {
 namespace theory {
 
 enum TheoryId {
-  ${theory_enum}
+${theory_enum}
   THEORY_LAST
 };
 
 inline std::ostream& operator<<(std::ostream& out, TheoryId theoryId) {
   switch(theoryId) {
-  ${theory_descriptions}
+${theory_descriptions}
   default:
     out << "UNKNOWN_THEORY";
     break;
@@ -136,18 +136,18 @@ inline std::ostream& operator<<(std::ostream& out, TheoryId theoryId) {
 }
 
 inline TheoryId kindToTheoryId(::CVC4::Kind k) {
-  switch (k) {
-    ${kind_to_theory_id}
+  switch(k) {
+${kind_to_theory_id}
   default:
-    Unreachable();
+    Unhandled(k);
   }
 }
 
 inline TheoryId typeConstantToTheoryId(::CVC4::TypeConstant typeConstant) {
-  switch (typeConstant) {
-    ${type_constant_to_theory_id}
+  switch(typeConstant) {
+${type_constant_to_theory_id}
   default:
-    Unreachable();
+    Unhandled(typeConstant);
   }
 }
 
diff --git a/src/expr/mkkind b/src/expr/mkkind
index f7f6ba836..fa80894b2 100755
--- a/src/expr/mkkind
+++ b/src/expr/mkkind
@@ -73,9 +73,9 @@ function theory {
   fi
 
   theory_id="$1"
-  theory_enum="$1,
-  ${theory_enum}"
-  theory_descriptions="${theory_descriptions}    case ${theory_id}: out << \"${theory_id}\"; break;
+  theory_enum="${theory_enum}  $1,
+"
+  theory_descriptions="${theory_descriptions}  case ${theory_id}: out << \"${theory_id}\"; break;
 "
 }
 
@@ -144,11 +144,11 @@ function register_sort {
   id=$1
   comment=$2
 
-  type_constant_list="${type_constant_list}   ${id}, /**< ${comment} */
+  type_constant_list="${type_constant_list}  ${id}, /**< ${comment} */
 "
-  type_constant_descriptions="${type_constant_descriptions}   case $id:  out << \"${comment}\"; break;
+  type_constant_descriptions="${type_constant_descriptions}  case $id:  out << \"${comment}\"; break;
 "
-  type_constant_to_theory_id="${type_constant_to_theory_id}   case $id: return $theory_id; break;
+  type_constant_to_theory_id="${type_constant_to_theory_id}  case $id: return $theory_id; break;
 "
 }
 
@@ -161,7 +161,7 @@ function register_kind {
 "
   kind_printers="${kind_printers}  case $r: out << \"$r\"; break;
 "
-  kind_to_theory_id="${kind_to_theory_id}   case kind::$r: return $theory_id; break;
+  kind_to_theory_id="${kind_to_theory_id}  case kind::$r: return $theory_id; break;
 "
 }
 
diff --git a/src/expr/node.h b/src/expr/node.h
index d3775cb3f..6fe1e7d0e 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -720,7 +720,7 @@ public:
   }
 
   /**
-   * Converst this node into a string representation and sends it to the
+   * Converts this node into a string representation and sends it to the
    * given stream
    *
    * @param out the stream to serialize this node to
@@ -790,6 +790,7 @@ public:
 
 /**
  * Serializes a given node to the given stream.
+ *
  * @param out the output stream to use
  * @param n the node to output to the stream
  * @return the stream
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index 9449594e3..716e2a3b3 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -519,18 +519,26 @@ TypeNode NodeManager::getType(TNode n, bool check)
   return typeNode;
 }
 
-TypeNode NodeManager::mkConstructorType(const Datatype::Constructor& constructor, TypeNode range) {
+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];
+    TypeNode selectorType = *(*i).getSelector().getType().d_typeNode;
+    Debug("datatypes") << selectorType << std::endl;
+    TypeNode sort = selectorType[1];
+
+    // should be guaranteed here already, but just in case
+    Assert(!sort.isFunctionLike());
+
     Debug("datatypes") << "ctor sort: " << sort << std::endl;
     sorts.push_back(sort);
   }
   Debug("datatypes") << "ctor range: " << range << std::endl;
+  CheckArgument(!range.isFunctionLike(), range,
+                "cannot create higher-order function types");
   sorts.push_back(range);
   return mkTypeNode(kind::CONSTRUCTOR_TYPE, sorts);
 }
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 94b7e5c40..9974df6ca 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -799,6 +799,8 @@ NodeManager::mkFunctionType(const std::vector<TypeNode>& sorts) {
   Assert(sorts.size() >= 2);
   std::vector<TypeNode> sortNodes;
   for (unsigned i = 0; i < sorts.size(); ++ i) {
+    CheckArgument(!sorts[i].isFunctionLike(), sorts,
+                  "cannot create higher-order function types");
     sortNodes.push_back(sorts[i]);
   }
   return mkTypeNode(kind::FUNCTION_TYPE, sortNodes);
@@ -809,6 +811,8 @@ NodeManager::mkPredicateType(const std::vector<TypeNode>& sorts) {
   Assert(sorts.size() >= 1);
   std::vector<TypeNode> sortNodes;
   for (unsigned i = 0; i < sorts.size(); ++ i) {
+    CheckArgument(!sorts[i].isFunctionLike(), sorts,
+                  "cannot create higher-order function types");
     sortNodes.push_back(sorts[i]);
   }
   sortNodes.push_back(booleanType());
@@ -819,6 +823,10 @@ inline TypeNode NodeManager::mkTupleType(const std::vector<TypeNode>& types) {
   Assert(types.size() >= 2);
   std::vector<TypeNode> typeNodes;
   for (unsigned i = 0; i < types.size(); ++ i) {
+    /* FIXME when congruence closure no longer abuses tuples
+    CheckArgument(!types[i].isFunctionLike(), types,
+                  "cannot put function-like types in tuples");
+    */
     typeNodes.push_back(types[i]);
   }
   return mkTypeNode(kind::TUPLE_TYPE, typeNodes);
@@ -830,14 +838,24 @@ inline TypeNode NodeManager::mkBitVectorType(unsigned size) {
 
 inline TypeNode NodeManager::mkArrayType(TypeNode indexType,
                                          TypeNode constituentType) {
+  CheckArgument(!indexType.isFunctionLike(), domain,
+                "cannot index arrays by a function-like type");
+  CheckArgument(!constituentType.isFunctionLike(), domain,
+                "cannot store function-like types in arrays");
   return mkTypeNode(kind::ARRAY_TYPE, indexType, constituentType);
 }
 
 inline TypeNode NodeManager::mkSelectorType(TypeNode domain, TypeNode range) {
+  CheckArgument(!domain.isFunctionLike(), domain,
+                "cannot create higher-order function types");
+  CheckArgument(!range.isFunctionLike(), range,
+                "cannot create higher-order function types");
   return mkTypeNode(kind::SELECTOR_TYPE, domain, range);
 }
 
 inline TypeNode NodeManager::mkTesterType(TypeNode domain) {
+  CheckArgument(!domain.isFunctionLike(), domain,
+                "cannot create higher-order function types");
   return mkTypeNode(kind::TESTER_TYPE, domain );
 }
 
diff --git a/src/expr/type.cpp b/src/expr/type.cpp
index 6dd9c5cec..4ea425aa7 100644
--- a/src/expr/type.cpp
+++ b/src/expr/type.cpp
@@ -69,10 +69,26 @@ bool Type::isNull() const {
 }
 
 Type& Type::operator=(const Type& t) {
-  NodeManagerScope nms(t.d_nodeManager);
+  Assert(d_typeNode != NULL, "Unexpected NULL typenode pointer!");
+  Assert(t.d_typeNode != NULL, "Unexpected NULL typenode pointer!");
+
   if(this != &t) {
-    *d_typeNode = *t.d_typeNode;
-    d_nodeManager = t.d_nodeManager;
+    if(d_nodeManager == t.d_nodeManager) {
+      NodeManagerScope nms(d_nodeManager);
+      *d_typeNode = *t.d_typeNode;
+    } else {
+      // This happens more than you think---every time you set to or
+      // from the null Type.  It's tricky because each node manager
+      // must be in play at the right time.
+
+      NodeManagerScope nms1(d_nodeManager);
+      *d_typeNode = TypeNode::null();
+
+      NodeManagerScope nms2(t.d_nodeManager);
+      *d_typeNode = *t.d_typeNode;
+
+      d_nodeManager = t.d_nodeManager;
+    }
   }
   return *this;
 }
@@ -85,6 +101,10 @@ bool Type::operator!=(const Type& t) const {
   return *d_typeNode != *t.d_typeNode;
 }
 
+bool Type::operator<(const Type& t) const {
+  return *d_typeNode < *t.d_typeNode;
+}
+
 Type Type::substitute(const Type& type, const Type& replacement) const {
   NodeManagerScope nms(d_nodeManager);
   return makeType(d_typeNode->substitute(*type.d_typeNode,
@@ -468,6 +488,22 @@ Type ConstructorType::getReturnType() const {
   return makeType(d_typeNode->getConstructorReturnType());
 }
 
+size_t ConstructorType::getArity() const {
+  return d_typeNode->getNumChildren() - 1;
+}
+
+std::vector<Type> ConstructorType::getArgTypes() const {
+  NodeManagerScope nms(d_nodeManager);
+  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));
+  }
+  return args;
+}
+
 const Datatype& DatatypeType::getDatatype() const {
   return d_typeNode->getConst<Datatype>();
 }
diff --git a/src/expr/type.h b/src/expr/type.h
index 3b476ddf5..290bb360a 100644
--- a/src/expr/type.h
+++ b/src/expr/type.h
@@ -174,6 +174,11 @@ public:
   bool operator!=(const Type& t) const;
 
   /**
+   * An ordering on Types so they can be stored in maps, etc.
+   */
+  bool operator<(const Type& t) const;
+
+  /**
    * Is this the Boolean type?
    * @return true if the type is a Boolean type
    */
@@ -533,6 +538,12 @@ public:
   /** Get the return type */
   Type getReturnType() const;
 
+  /** Get the argument types */
+  std::vector<Type> getArgTypes() const;
+
+  /** Get the number of constructor arguments */
+  size_t getArity() const;
+
 };/* class ConstructorType */
 
 
diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp
index 7549af895..0b22fdf0f 100644
--- a/src/expr/type_node.cpp
+++ b/src/expr/type_node.cpp
@@ -2,8 +2,8 @@
 /*! \file type_node.cpp
  ** \verbatim
  ** Original author: dejan
- ** Major contributors: mdeters
- ** Minor contributors (to current version): taking
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
@@ -85,6 +85,14 @@ bool TypeNode::isFunction() const {
   return getKind() == kind::FUNCTION_TYPE;
 }
 
+bool TypeNode::isFunctionLike() const {
+  return
+    getKind() == kind::FUNCTION_TYPE ||
+    getKind() == kind::CONSTRUCTOR_TYPE ||
+    getKind() == kind::SELECTOR_TYPE ||
+    getKind() == kind::TESTER_TYPE;
+}
+
 bool TypeNode::isPredicate() const {
   return isFunction() && getRangeType().isBoolean();
 }
diff --git a/src/expr/type_node.h b/src/expr/type_node.h
index 049173867..c04bef0c7 100644
--- a/src/expr/type_node.h
+++ b/src/expr/type_node.h
@@ -371,6 +371,19 @@ public:
   bool isFunction() const;
 
   /**
+   * Is this a function-LIKE type?  Function-like things
+   * (e.g. datatype selectors) that aren't actually functions ARE
+   * considered functions, here.  The main point is that this is used
+   * to avoid anything higher-order: anything function-like cannot be
+   * the argument or return value for anything else function-like.
+   *
+   * Arrays are explicitly *not* function-like for the purposes of
+   * this test.  However, functions still cannot contain anything
+   * function-like.
+   */
+  bool isFunctionLike() const;
+
+  /**
    * Get the argument types of a function, datatype constructor,
    * datatype selector, or datatype tester.
    */
@@ -383,9 +396,9 @@ public:
   TypeNode getRangeType() const;
 
   /**
-   * Is this a predicate type?
-   * NOTE: all predicate types are also function types (so datatype
-   * testers are not considered "predicates" for the purpose of this function).
+   * Is this a predicate type?  NOTE: all predicate types are also
+   * function types (so datatype testers are NOT considered
+   * "predicates" for the purpose of this function).
    */
   bool isPredicate() const;
 
@@ -451,7 +464,8 @@ private:
 inline std::ostream& operator<<(std::ostream& out, const TypeNode& n) {
   n.toStream(out,
              Node::setdepth::getDepth(out),
-             Node::printtypes::getPrintTypes(out));
+             Node::printtypes::getPrintTypes(out),
+             Node::setlanguage::getLanguage(out));
   return out;
 }