Monday tasks:

* new "well-foundedness" type property (like cardinality) specified in
  Theory kinds files; specifies well-foundedness and a ground term

* well-foundedness / finite checks in Datatypes now superseded by type
  system isFinite(), isWellFounded(), mkGroundTerm().

* new "RecursionBreaker" template class, a convenient class that keeps
  a "seen" trail without you having to pass it around (which is
  difficult in cases of mutual recursion) of the idea of passing
  around a "seen" trail

27 files changed, 969 insertions, 55 deletions

diff --git a/src/expr/expr_manager_scope.h b/src/expr/expr_manager_scope.h
index c1da288a4..7a5bdbfb4 100644
--- a/src/expr/expr_manager_scope.h
+++ b/src/expr/expr_manager_scope.h
@@ -5,7 +5,7 @@
  ** 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
@@ -56,6 +56,11 @@ public:
           ? NodeManager::currentNM()
           : e.getExprManager()->getNodeManager()) {
   }
+  inline ExprManagerScope(const Type& t) :
+    d_nms(t.getExprManager() == NULL
+          ? NodeManager::currentNM()
+          : t.getExprManager()->getNodeManager()) {
+  }
   inline ExprManagerScope(const ExprManager& exprManager) :
     d_nms(exprManager.getNodeManager()) {
   }
diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index b116a4671..f0c90ebdb 100644
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -585,7 +585,7 @@ void ExprManager::checkResolvedDatatype(DatatypeType dtt) const {
     Type ctorType CVC4_UNUSED = c.getConstructor().getType();
     Assert(ctorType.isConstructor() &&
            ConstructorType(ctorType).getArity() == c.getNumArgs() &&
-           ConstructorType(ctorType).getReturnType() == dtt,
+           ConstructorType(ctorType).getRangeType() == dtt,
            "malformed constructor in datatype post-resolution");
     // for all selectors...
     for(Datatype::Constructor::const_iterator j = c.begin(), j_end = c.end();
diff --git a/src/expr/mkexpr b/src/expr/mkexpr
index a7302da26..479ef6d11 100755
--- a/src/expr/mkexpr
+++ b/src/expr/mkexpr
@@ -108,7 +108,7 @@ function endtheory {
 }
 
 function sort {
-  # sort TYPE cardinality ["comment"]
+  # sort TYPE cardinality [well-founded ground-term header | not-well-founded] ["comment"]
   lineno=${BASH_LINENO[0]}
   check_theory_seen
 }
@@ -119,6 +119,12 @@ function cardinality {
   check_theory_seen
 }
 
+function well-founded {
+  # well-founded TYPE wellfoundedness-computer [header]
+  lineno=${BASH_LINENO[0]}
+  check_theory_seen
+}
+
 function variable {
   # variable K ["comment"]
   lineno=${BASH_LINENO[0]}
diff --git a/src/expr/mkkind b/src/expr/mkkind
index 08d874c79..47d02863e 100755
--- a/src/expr/mkkind
+++ b/src/expr/mkkind
@@ -63,7 +63,11 @@ type_constant_list=
 type_constant_to_theory_id=
 type_cardinalities=
 type_constant_cardinalities=
-type_cardinalities_includes=
+type_wellfoundednesses=
+type_constant_wellfoundednesses=
+type_groundterms=
+type_constant_groundterms=
+type_properties_includes=
 
 seen_theory=false
 seen_theory_builtin=false
@@ -121,10 +125,24 @@ function rewriter {
 }
 
 function sort {
-  # sort TYPE cardinality ["comment"]
+  # sort TYPE cardinality [well-founded ground-term header | not-well-founded] ["comment"]
   lineno=${BASH_LINENO[0]}
   check_theory_seen
-  register_sort "$1" "$2" "$3"
+  if [ "$3" = well-founded ]; then
+    wf=true
+    groundterm="$4"
+    header="$5"
+    comment="$6"
+  elif [ "$3" = not-well-founded ]; then
+    wf=false
+    groundterm=
+    header=
+    comment="$4"
+  else
+    echo "$kf:$lineno: expected third argument to be \"well-founded\" or \"not-well-founded\"" >&2
+    exit 1
+  fi
+  register_sort "$1" "$2" "$wf" "$groundterm" "$header" "$comment"
 }
 
 function cardinality {
@@ -134,6 +152,13 @@ function cardinality {
   register_cardinality "$1" "$2" "$3"
 }
 
+function well-founded {
+  # well-founded TYPE wellfoundedness-computer groundterm-computer [header]
+  lineno=${BASH_LINENO[0]}
+  check_theory_seen
+  register_wellfoundedness "$1" "$2" "$3" "$4"
+}
+
 function variable {
   # variable K ["comment"]
 
@@ -173,7 +198,10 @@ function constant {
 function register_sort {
   id=$1
   cardinality=$2
-  comment=$3
+  wellfoundedness=$3
+  groundterm=$4
+  header=$5
+  comment=$6
 
   type_constant_list="${type_constant_list}  ${id}, /**< ${comment} */
 "
@@ -184,6 +212,23 @@ function register_sort {
   type_constant_cardinalities="${type_constant_cardinalities}#line $lineno \"$kf\"
   case $id: return Cardinality($cardinality);
 "
+  type_constant_wellfoundednesses="${type_constant_wellfoundednesses}#line $lineno \"$kf\"
+  case $id: return $wellfoundedness;
+"
+  if [ -n "$groundterm" ]; then
+    type_constant_groundterms="${type_constant_groundterms}#line $lineno \"$kf\"
+  case $id: return $groundterm;
+"
+    if [ -n "$header" ]; then
+      type_properties_includes="${type_properties_includes}#line $lineno \"$kf\"
+#include \"$header\"
+"
+    fi
+  else
+    type_constant_groundterms="${type_constant_groundterms}#line $lineno \"$kf\"
+  case $id: Unhandled(tc);
+"
+  fi
 }
 
 function register_cardinality {
@@ -195,7 +240,46 @@ function register_cardinality {
   case $id: return $cardinality_computer;
 "
   if [ -n "$header" ]; then
-    type_cardinalities_includes="${type_cardinalities_includes}#line $lineno \"$kf\"
+    type_properties_includes="${type_properties_includes}#line $lineno \"$kf\"
+#include \"$header\"
+"
+  fi
+}
+
+function register_wellfoundedness {
+  id=$1
+  wellfoundedness_computer=$(sed 's,%TYPE%,typeNode,g' <<<"$2")
+  groundterm_computer=$(sed 's,%TYPE%,typeNode,g' <<<"$3")
+  header=$4
+
+  # "false" is a special well-foundedness computer that doesn't
+  # require an associated groundterm-computer; anything else does
+  if [ "$wellfoundedness_computer" != false ]; then
+    if [ -z "$groundterm_computer" ]; then
+      echo "$kf:$lineno: ground-term computer missing in command \"well-founded\"" >&2
+      exit 1
+    fi
+  else
+    if [ -n "$groundterm_computer" ]; then
+      echo "$kf:$lineno: ground-term computer specified for not-well-founded type" >&2
+      exit 1
+    fi
+  fi
+
+  type_wellfoundednesses="${type_wellfoundednesses}#line $lineno \"$kf\"
+  case $id: return $wellfoundedness_computer;
+"
+  if [ -n "$groundterm_computer" ]; then
+    type_groundterms="${type_groundterms}#line $lineno \"$kf\"
+  case $id: return $groundterm_computer;
+"
+  else
+    type_groundterms="${type_groundterms}#line $lineno \"$kf\"
+  case $id: Unhandled(typeNode);
+"
+  fi
+  if [ -n "$header" ]; then
+    type_properties_includes="${type_properties_includes}#line $lineno \"$kf\"
 #include \"$header\"
 "
   fi
@@ -272,7 +356,11 @@ for var in \
     type_constant_to_theory_id \
     type_cardinalities \
     type_constant_cardinalities \
-    type_cardinalities_includes \
+    type_wellfoundednesses \
+    type_constant_wellfoundednesses \
+    type_groundterms \
+    type_constant_groundterms \
+    type_properties_includes \
     theory_descriptions \
     template \
     ; do
diff --git a/src/expr/mkmetakind b/src/expr/mkmetakind
index 00599c5a0..46a69dee5 100755
--- a/src/expr/mkmetakind
+++ b/src/expr/mkmetakind
@@ -100,7 +100,7 @@ function rewriter {
 }
 
 function sort {
-  # sort TYPE cardinality ["comment"]
+  # sort TYPE cardinality [well-founded ground-term header | not-well-founded] ["comment"]
   lineno=${BASH_LINENO[0]}
   check_theory_seen
 }
@@ -111,6 +111,12 @@ function cardinality {
   check_theory_seen
 }
 
+function well-founded {
+  # well-founded TYPE wellfoundedness-computer [header]
+  lineno=${BASH_LINENO[0]}
+  check_theory_seen
+}
+
 function variable {
   # variable K ["comment"]
 
diff --git a/src/expr/type.cpp b/src/expr/type.cpp
index 27a3f9da7..0df385a29 100644
--- a/src/expr/type.cpp
+++ b/src/expr/type.cpp
@@ -73,6 +73,16 @@ Cardinality Type::getCardinality() const {
   return d_typeNode->getCardinality();
 }
 
+bool Type::isWellFounded() const {
+  NodeManagerScope nms(d_nodeManager);
+  return d_typeNode->isWellFounded();
+}
+
+Expr Type::mkGroundTerm() const {
+  NodeManagerScope nms(d_nodeManager);
+  return d_typeNode->mkGroundTerm().toExpr();
+}
+
 Type& Type::operator=(const Type& t) {
   Assert(d_typeNode != NULL, "Unexpected NULL typenode pointer!");
   Assert(t.d_typeNode != NULL, "Unexpected NULL typenode pointer!");
@@ -489,8 +499,8 @@ Type ArrayType::getConstituentType() const {
   return makeType(d_typeNode->getArrayConstituentType());
 }
 
-Type ConstructorType::getReturnType() const {
-  return makeType(d_typeNode->getConstructorReturnType());
+DatatypeType ConstructorType::getRangeType() const {
+  return DatatypeType(makeType(d_typeNode->getConstructorRangeType()));
 }
 
 size_t ConstructorType::getArity() const {
diff --git a/src/expr/type.h b/src/expr/type.h
index 89cb994e7..682e5fbcd 100644
--- a/src/expr/type.h
+++ b/src/expr/type.h
@@ -33,6 +33,7 @@ namespace CVC4 {
 
 class NodeManager;
 class ExprManager;
+class Expr;
 class TypeNode;
 
 class SmtEngine;
@@ -143,6 +144,18 @@ public:
   Cardinality getCardinality() const;
 
   /**
+   * Is this a well-founded type?  (I.e., do there exist ground
+   * terms?)
+   */
+  bool isWellFounded() const;
+
+  /**
+   * Construct and return a ground term for this Type.  Throws an
+   * exception if this type is not well-founded.
+   */
+  Expr mkGroundTerm() const;
+
+  /**
    * Substitution of Types.
    */
   Type substitute(const Type& type, const Type& replacement) const;
@@ -541,8 +554,8 @@ public:
   /** Construct from the base type */
   ConstructorType(const Type& type) throw(AssertionException);
 
-  /** Get the return type */
-  Type getReturnType() const;
+  /** Get the range type */
+  DatatypeType getRangeType() const;
 
   /** Get the argument types */
   std::vector<Type> getArgTypes() const;
diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp
index e48a92321..7b0adaa95 100644
--- a/src/expr/type_node.cpp
+++ b/src/expr/type_node.cpp
@@ -51,6 +51,14 @@ Cardinality TypeNode::getCardinality() const {
   return kind::getCardinality(*this);
 }
 
+bool TypeNode::isWellFounded() const {
+  return kind::isWellFounded(*this);
+}
+
+Node TypeNode::mkGroundTerm() const {
+  return kind::mkGroundTerm(*this);
+}
+
 bool TypeNode::isBoolean() const {
   return getKind() == kind::TYPE_CONSTANT &&
     getConst<TypeConstant>() == BOOLEAN_TYPE;
@@ -81,7 +89,7 @@ TypeNode TypeNode::getArrayConstituentType() const {
   return (*this)[1];
 }
 
-TypeNode TypeNode::getConstructorReturnType() const {
+TypeNode TypeNode::getConstructorRangeType() const {
   Assert(isConstructor());
   return (*this)[getNumChildren()-1];
 }
diff --git a/src/expr/type_node.h b/src/expr/type_node.h
index f51d7a9ba..b9fea939e 100644
--- a/src/expr/type_node.h
+++ b/src/expr/type_node.h
@@ -344,12 +344,39 @@ public:
   }
 
   /**
+   * Convert this TypeNode into a Type using the currently-in-scope
+   * manager.
+   */
+  inline Type toType();
+
+  /**
+   * Convert a Type into a TypeNode.
+   */
+  inline static TypeNode fromType(const Type& t);
+
+  /**
    * Returns the cardinality of this type.
    *
    * @return a finite or infinite cardinality
    */
   Cardinality getCardinality() const;
 
+  /**
+   * Returns whether this type is well-founded.  A type is
+   * well-founded if there exist ground terms.
+   *
+   * @return true iff the type is well-founded
+   */
+  bool isWellFounded() const;
+
+  /**
+   * Construct and return a ground term of this type.  If the type is
+   * not well founded, this function throws an exception.
+   *
+   * @return a ground term of the type
+   */
+  Node mkGroundTerm() const;
+
   /** Is this the Boolean type? */
   bool isBoolean() const;
 
@@ -369,7 +396,7 @@ public:
   TypeNode getArrayConstituentType() const;
 
   /** Get the return type (for constructor types) */
-  TypeNode getConstructorReturnType() const;
+  TypeNode getConstructorRangeType() const;
 
   /**
    * Is this a function type?  Function-like things (e.g. datatype
@@ -492,6 +519,14 @@ struct TypeNodeHashFunction {
 
 namespace CVC4 {
 
+inline Type TypeNode::toType() {
+  return NodeManager::currentNM()->toType(*this);
+}
+
+inline TypeNode TypeNode::fromType(const Type& t) {
+  return NodeManager::fromType(t);
+}
+
 template <class Iterator1, class Iterator2>
 TypeNode TypeNode::substitute(Iterator1 typesBegin,
                               Iterator1 typesEnd,
diff --git a/src/expr/type_properties_template.h b/src/expr/type_properties_template.h
index b6fd644c8..28aa2f884 100644
--- a/src/expr/type_properties_template.h
+++ b/src/expr/type_properties_template.h
@@ -31,7 +31,7 @@
 
 #include <sstream>
 
-${type_cardinalities_includes}
+${type_properties_includes}
 
 #line 37 "${template}"
 
@@ -81,6 +81,68 @@ ${type_cardinalities}
   }
 }/* getCardinality(TypeNode) */
 
+inline bool isWellFounded(TypeConstant tc) {
+  switch(tc) {
+${type_constant_wellfoundednesses}
+#line 88 "${template}"
+  default: {
+    std::stringstream ss;
+    ss << "No well-foundedness status known for type constant: " << tc;
+    InternalError(ss.str());
+  }
+  }
+}/* isWellFounded(TypeConstant) */
+
+inline bool isWellFounded(TypeNode typeNode) {
+  AssertArgument(!typeNode.isNull(), typeNode);
+  switch(Kind k = typeNode.getKind()) {
+  case TYPE_CONSTANT:
+    return isWellFounded(typeNode.getConst<TypeConstant>());
+${type_wellfoundednesses}
+#line 103 "${template}"
+  default: {
+    std::stringstream ss;
+    ss << Expr::setlanguage(language::toOutputLanguage
+                            ( Options::current()->inputLanguage ));
+    ss << "A theory kinds file did not provide a well-foundedness "
+       << "or well-foundedness computer for type:\n" << typeNode
+       << "\nof kind " << k;
+    InternalError(ss.str());
+  }
+  }
+}/* isWellFounded(TypeNode) */
+
+inline Node mkGroundTerm(TypeConstant tc) {
+  switch(tc) {
+${type_constant_groundterms}
+#line 119 "${template}"
+  default: {
+    std::stringstream ss;
+    ss << "No ground term known for type constant: " << tc;
+    InternalError(ss.str());
+  }
+  }
+}/* mkGroundTerm(TypeConstant) */
+
+inline Node mkGroundTerm(TypeNode typeNode) {
+  AssertArgument(!typeNode.isNull(), typeNode);
+  switch(Kind k = typeNode.getKind()) {
+  case TYPE_CONSTANT:
+    return mkGroundTerm(typeNode.getConst<TypeConstant>());
+${type_groundterms}
+#line 134 "${template}"
+  default: {
+    std::stringstream ss;
+    ss << Expr::setlanguage(language::toOutputLanguage
+                            ( Options::current()->inputLanguage ));
+    ss << "A theory kinds file did not provide a ground term "
+       << "or ground term computer for type:\n" << typeNode
+       << "\nof kind " << k;
+    InternalError(ss.str());
+  }
+  }
+}/* mkGroundTerm(TypeNode) */
+
 }/* CVC4::kind namespace */
 }/* CVC4 namespace */
 
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index f98d60702..45c697d0b 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -508,7 +508,7 @@ void SmtEnginePrivate::addFormula(SmtEngine& smt, TNode n)
     // process without any error notice.
     stringstream ss;
     ss << Expr::setlanguage(language::toOutputLanguage(Options::current()->inputLanguage))
-       << "A bad expression was produced.  Original exception follows:\n"
+       << "A bad expression was produced internally.  Original exception follows:\n"
        << tcep;
     InternalError(ss.str().c_str());
   }
diff --git a/src/theory/arith/kinds b/src/theory/arith/kinds
index a0fc71ab4..1871e897a 100644
--- a/src/theory/arith/kinds
+++ b/src/theory/arith/kinds
@@ -18,8 +18,18 @@ operator MINUS 2 "arithmetic binary subtraction operator"
 operator UMINUS 1 "arithmetic unary negation"
 operator DIVISION 2 "arithmetic division"
 
-sort REAL_TYPE Cardinality::REALS "Real type"
-sort INTEGER_TYPE Cardinality::INTEGERS "Integer type"
+sort REAL_TYPE \
+    Cardinality::REALS \
+    well-founded \
+        "NodeManager::currentNM()->mkConst(Rational(0))" \
+        "expr/node_manager.h" \
+    "Real type"
+sort INTEGER_TYPE \
+    Cardinality::INTEGERS \
+    well-founded \
+        "NodeManager::currentNM()->mkConst(Integer(0))" \
+        "expr/node_manager.h" \
+    "Integer type"
 
 constant CONST_RATIONAL \
     ::CVC4::Rational \
diff --git a/src/theory/arrays/kinds b/src/theory/arrays/kinds
index 533145dc2..4c68fb5cb 100644
--- a/src/theory/arrays/kinds
+++ b/src/theory/arrays/kinds
@@ -15,6 +15,7 @@ operator ARRAY_TYPE 2 "array type"
 cardinality ARRAY_TYPE \
     "::CVC4::theory::arrays::CardinalityComputer::computeCardinality(%TYPE%)" \
     "theory/arrays/theory_arrays_type_rules.h"
+well-founded ARRAY_TYPE false
 
 # select a i  is  a[i]
 operator SELECT 2 "array select"
diff --git a/src/theory/booleans/kinds b/src/theory/booleans/kinds
index ce7c9111a..d540d57f5 100644
--- a/src/theory/booleans/kinds
+++ b/src/theory/booleans/kinds
@@ -10,7 +10,12 @@ properties finite
 
 rewriter ::CVC4::theory::booleans::TheoryBoolRewriter "theory/booleans/theory_bool_rewriter.h"
 
-sort BOOLEAN_TYPE 2 "Boolean type"
+sort BOOLEAN_TYPE \
+    2 \
+    well-founded \
+        "NodeManager::currentNM()->mkConst(false)" \
+        "expr/node_manager.h" \
+    "Boolean type"
 
 constant CONST_BOOLEAN \
     bool \
@@ -26,4 +31,4 @@ operator OR 2: "logical or"
 operator XOR 2 "exclusive or"
 operator ITE 3 "if-then-else"
 
-endtheory
\ No newline at end of file
+endtheory
diff --git a/src/theory/builtin/kinds b/src/theory/builtin/kinds
index a170ba145..f5195e256 100644
--- a/src/theory/builtin/kinds
+++ b/src/theory/builtin/kinds
@@ -122,7 +122,7 @@
 #     For consistency, constants taking a non-void payload should
 #     start with "CONST_", but this is not enforced.
 #
-#   sort K cardinality ["comment"]
+#   sort K cardinality [well-founded ground-term header | not-well-founded] ["comment"]
 #
 #     This creates a kind K that represents a sort (a "type constant").
 #     These kinds of types are "atomic" types; if you need to describe
@@ -138,6 +138,13 @@
 #     cardinality as the integers, or Cardinality::REALS if the sort
 #     has the same cardinality as the reals.
 #
+#     If the sort is well-founded (i.e., there exist ground terms),
+#     then the argument should be the string "well-founded"; if not,
+#     it should be the string "not-well-founded".  If well-founded,
+#     two extra arguments immediately follow---a C++ expression that
+#     constructs a ground term (as a Node), and the header that must
+#     be #included for that expression to compile.
+#
 #     For consistency, sorts should end with "_TYPE", but this is not
 #     enforced.
 #
@@ -168,6 +175,15 @@
 #           ::CVC4::theory::foo::TheoryFoo::CardinalityComputer(%TYPE%) \
 #           "theory/foo/theory_foo_type_rules.h"
 #
+#   well-founded K wellfoundedness-computer ground-term-computer [header]
+#
+#     Analogous to the "cardinality" command above, the well-founded
+#     command provides a well-foundedness computer for the type.  A
+#     ground term computer is required unless the
+#     wellfoundedness-computer is the constant "false".  The ground
+#     term computer should return a Node, and it should return the
+#     same Node each time for a given type (although usually it's only
+#     ever called once anyway since the result is cached).
 #
 #
 # Lines may be broken with a backslash between arguments; for example:
@@ -207,7 +223,10 @@ properties stable-infinite
 # Rewriter responisble for all the terms of the theory
 rewriter ::CVC4::theory::builtin::TheoryBuiltinRewriter "theory/builtin/theory_builtin_rewriter.h"
 
-sort BUILTIN_OPERATOR_TYPE Cardinality::INTEGERS "Built in type for built in operators"
+sort BUILTIN_OPERATOR_TYPE \
+    Cardinality::INTEGERS \
+    not-well-founded \
+    "Built in type for built in operators"
 
 # A kind representing "inlined" operators defined with OPERATOR
 # Conceptually, (EQUAL a b) is actually an (APPLY EQUAL a b), but it's
@@ -235,11 +254,16 @@ constant TYPE_CONSTANT \
     "basic types"
 operator FUNCTION_TYPE 2: "function type"
 cardinality FUNCTION_TYPE \
-    "::CVC4::theory::builtin::FunctionCardinality::computeCardinality(%TYPE%)" \
+    "::CVC4::theory::builtin::FunctionProperties::computeCardinality(%TYPE%)" \
     "theory/builtin/theory_builtin_type_rules.h"
+well-founded FUNCTION_TYPE false
 operator TUPLE_TYPE 2: "tuple type"
 cardinality TUPLE_TYPE \
-    "::CVC4::theory::builtin::TupleCardinality::computeCardinality(%TYPE%)" \
+    "::CVC4::theory::builtin::TupleProperties::computeCardinality(%TYPE%)" \
+    "theory/builtin/theory_builtin_type_rules.h"
+well-founded TUPLE_TYPE \
+    "::CVC4::theory::builtin::TupleProperties::isWellFounded(%TYPE%)" \
+    "::CVC4::theory::builtin::TupleProperties::mkGroundTerm(%TYPE%)" \
     "theory/builtin/theory_builtin_type_rules.h"
 
 endtheory
diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h
index bebfca9ab..cffc95ab2 100644
--- a/src/theory/builtin/theory_builtin_type_rules.h
+++ b/src/theory/builtin/theory_builtin_type_rules.h
@@ -128,10 +128,13 @@ public:
   }
 };/* class TupleTypeRule */
 
-class FunctionCardinality {
+class FunctionProperties {
 public:
   inline static Cardinality computeCardinality(TypeNode type) {
-    Assert(type.getKind() == kind::FUNCTION_TYPE);
+    // Don't assert this; allow other theories to use this cardinality
+    // computation.
+    //
+    // Assert(type.getKind() == kind::FUNCTION_TYPE);
 
     Cardinality argsCard(1);
     // get the largest cardinality of function arguments/return type
@@ -143,12 +146,15 @@ public:
 
     return valueCard ^ argsCard;
   }
-};/* class FuctionCardinality */
+};/* class FuctionProperties */
 
-class TupleCardinality {
+class TupleProperties {
 public:
   inline static Cardinality computeCardinality(TypeNode type) {
-    Assert(type.getKind() == kind::TUPLE_TYPE);
+    // Don't assert this; allow other theories to use this cardinality
+    // computation.
+    //
+    // Assert(type.getKind() == kind::TUPLE_TYPE);
 
     Cardinality card(1);
     for(TypeNode::iterator i = type.begin(),
@@ -160,7 +166,39 @@ public:
 
     return card;
   }
-};/* class TupleCardinality */
+
+  inline static bool isWellFounded(TypeNode type) {
+    // Don't assert this; allow other theories to use this
+    // wellfoundedness computation.
+    //
+    // Assert(type.getKind() == kind::TUPLE_TYPE);
+
+    for(TypeNode::iterator i = type.begin(),
+          i_end = type.end();
+        i != i_end;
+        ++i) {
+      if(! (*i).isWellFounded()) {
+        return false;
+      }
+    }
+
+    return true;
+  }
+
+  inline static Node mkGroundTerm(TypeNode type) {
+    Assert(type.getKind() == kind::TUPLE_TYPE);
+
+    std::vector<Node> children;
+    for(TypeNode::iterator i = type.begin(),
+          i_end = type.end();
+        i != i_end;
+        ++i) {
+      children.push_back((*i).mkGroundTerm());
+    }
+
+    return NodeManager::currentNM()->mkNode(kind::TUPLE, children);
+  }
+};/* class TupleProperties */
 
 }/* CVC4::theory::builtin namespace */
 }/* CVC4::theory namespace */
diff --git a/src/theory/datatypes/kinds b/src/theory/datatypes/kinds
index 8cac2da62..37a65a2b0 100644
--- a/src/theory/datatypes/kinds
+++ b/src/theory/datatypes/kinds
@@ -12,12 +12,27 @@ rewriter ::CVC4::theory::datatypes::DatatypesRewriter "theory/datatypes/datatype
 
 # constructor type has a list of selector types followed by a return type
 operator CONSTRUCTOR_TYPE 1: "constructor"
+cardinality CONSTRUCTOR_TYPE \
+    "::CVC4::theory::datatypes::ConstructorProperties::computeCardinality(%TYPE%)" \
+    "theory/datatypes/theory_datatypes_type_rules.h"
+well-founded CONSTRUCTOR_TYPE \
+    "::CVC4::theory::datatypes::ConstructorProperties::isWellFounded(%TYPE%)" \
+    "::CVC4::theory::datatypes::ConstructorProperties::mkGroundTerm(%TYPE%)" \
+    "theory/datatypes/theory_datatypes_type_rules.h"
 
 # selector type has domain type and a range type
 operator SELECTOR_TYPE 2 "selector"
+# can re-use function cardinality
+cardinality SELECTOR_TYPE \
+    "::CVC4::theory::builtin::FunctionProperties::computeCardinality(%TYPE%)" \
+    "theory/builtin/theory_builtin_type_rules.h"
 
 # tester type has a constructor type
 operator TESTER_TYPE 1 "tester"
+# can re-use function cardinality
+cardinality TESTER_TYPE \
+    "::CVC4::theory::builtin::FunctionProperties::computeCardinality(%TYPE%)" \
+    "theory/builtin/theory_builtin_type_rules.h"
 
 parameterized APPLY_CONSTRUCTOR CONSTRUCTOR_TYPE 0: "constructor application"
 
@@ -30,5 +45,12 @@ constant DATATYPE_TYPE \
     "::CVC4::DatatypeHashStrategy" \
     "util/datatype.h" \
     "datatype type"
+cardinality DATATYPE_TYPE \
+    "%TYPE%.getConst<Datatype>().getCardinality()" \
+    "util/datatype.h"
+well-founded DATATYPE_TYPE \
+    "%TYPE%.getConst<Datatype>().isWellFounded()" \
+    "%TYPE%.getConst<Datatype>().mkGroundTerm()" \
+    "util/datatype.h"
 
 endtheory
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index 5e813b125..ee6f175dd 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -66,7 +66,7 @@ void TheoryDatatypes::checkFiniteWellFounded() {
     vector<Node>::iterator itc;
     // for each datatype...
     for( it = d_cons.begin(); it != d_cons.end(); ++it ) {
-      d_distinguishTerms[it->first] = Node::null();
+      //d_distinguishTerms[it->first] = Node::null();
       d_finite[it->first] = false;
       d_wellFounded[it->first] = false;
       // for each ctor of that datatype...
@@ -137,15 +137,15 @@ void TheoryDatatypes::checkFiniteWellFounded() {
               for( int c=0; c<(int)ct.getNumChildren()-1; c++ ) {
                 TypeNode ts = ct[c];
                 if( ts.isDatatype() ) {
-                  children.push_back( d_distinguishTerms[ts] );
+                  //children.push_back( d_distinguishTerms[ts] );
                 } else {
                   //fix?  this should be a ground term
                   children.push_back( nm->mkVar( ts ) );
                 }
               }
-              Node dgt = nm->mkNode( APPLY_CONSTRUCTOR, children );
-              Debug("datatypes-finite") << "set distinguished ground term " << t << " to " << dgt << endl;
-              d_distinguishTerms[t] = dgt;
+              //Node dgt = nm->mkNode( APPLY_CONSTRUCTOR, children );
+              //Debug("datatypes-finite") << "set distinguished ground term " << t << " to " << dgt << endl;
+              //d_distinguishTerms[t] = dgt;
             }
           }
         }
@@ -882,8 +882,8 @@ Node TheoryDatatypes::collapseSelector( TNode t, bool useContext ) {
       } else {
         Debug("datatypes") << "Applied selector " << t << " to wrong constructor " << endl;
         Debug("datatypes") << "Return distinguished term ";
-        Debug("datatypes") << d_distinguishTerms[ selType[1] ] << " of type " << selType[1] << endl;
-        retNode = d_distinguishTerms[ selType[1] ];
+        Debug("datatypes") << selType[1].mkGroundTerm() << " of type " << selType[1] << endl;
+        retNode = selType[1].mkGroundTerm();
       }
       if( useContext ) {
         Node neq = NodeManager::currentNM()->mkNode( EQUAL, retNode, t );
@@ -900,7 +900,7 @@ Node TheoryDatatypes::collapseSelector( TNode t, bool useContext ) {
         checkTester( tester, false );
         if( !d_conflict.isNull() ) {
           Debug("datatypes") << "Applied selector " << t << " to provably wrong constructor." << endl;
-          retNode = d_distinguishTerms[ selType[1] ];
+          retNode = selType[1].mkGroundTerm();
 
           Node neq = NodeManager::currentNM()->mkNode( EQUAL, retNode, t );
           NodeBuilder<> nb(kind::AND);
diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h
index 36d1b3311..c3b9a0baf 100644
--- a/src/theory/datatypes/theory_datatypes.h
+++ b/src/theory/datatypes/theory_datatypes.h
@@ -56,7 +56,7 @@ private:
   /** map from selectors to the constructors they are for */
   std::map<Node, Node > d_sel_cons;
   /**  the distinguished ground term for each type */
-  std::map<TypeNode, Node > d_distinguishTerms;
+  //std::map<TypeNode, Node > d_distinguishTerms;
   /** finite datatypes/constructor */
   std::map< TypeNode, bool > d_finite;
   std::map< Node, bool > d_cons_finite;
diff --git a/src/theory/datatypes/theory_datatypes_type_rules.h b/src/theory/datatypes/theory_datatypes_type_rules.h
index 1fd24cf53..bc1581f14 100644
--- a/src/theory/datatypes/theory_datatypes_type_rules.h
+++ b/src/theory/datatypes/theory_datatypes_type_rules.h
@@ -22,9 +22,18 @@
 #define __CVC4__THEORY__DATATYPES__THEORY_DATATYPES_TYPE_RULES_H
 
 namespace CVC4 {
+
+namespace expr {
+  namespace attr {
+    struct DatatypeConstructorTypeGroundTermTag {};
+  }/* CVC4::expr::attr namespace */
+}/* CVC4::expr namespace */
+
 namespace theory {
 namespace datatypes {
 
+typedef expr::Attribute<expr::attr::DatatypeConstructorTypeGroundTermTag, Node> GroundTermAttr;
+
 struct DatatypeConstructorTypeRule {
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
     throw(TypeCheckingExceptionPrivate) {
@@ -47,7 +56,7 @@ struct DatatypeConstructorTypeRule {
         }
       }
     }
-    return consType.getConstructorReturnType();
+    return consType.getConstructorRangeType();
   }
 };/* struct DatatypeConstructorTypeRule */
 
@@ -91,6 +100,61 @@ struct DatatypeTesterTypeRule {
   }
 };/* struct DatatypeSelectorTypeRule */
 
+struct ConstructorProperties {
+  inline static Cardinality computeCardinality(TypeNode type) {
+    // Constructors aren't exactly functions, they're like
+    // parameterized ground terms.  So the cardinality is more like
+    // that of a tuple than that of a function.
+    AssertArgument(type.isConstructor(), type);
+    Cardinality c = 1;
+    for(unsigned i = 0, i_end = type.getNumChildren(); i < i_end - 1; ++i) {
+      c *= type[i].getCardinality();
+    }
+    return c;
+  }
+
+  inline static bool isWellFounded(TypeNode type) {
+    // Constructors aren't exactly functions, they're like
+    // parameterized ground terms.  So the wellfoundedness is more
+    // like that of a tuple than that of a function.
+    AssertArgument(type.isConstructor(), type);
+    for(unsigned i = 0, i_end = type.getNumChildren(); i < i_end - 1; ++i) {
+      if(!type[i].isWellFounded()) {
+        return false;
+      }
+    }
+    return true;
+  }
+
+  inline static Node mkGroundTerm(TypeNode type) {
+    AssertArgument(type.isConstructor(), type);
+
+    // is this already in the cache ?
+    Node groundTerm = type.getAttribute(GroundTermAttr());
+    if(!groundTerm.isNull()) {
+      return groundTerm;
+    }
+
+    // This is a bit tricky; Constructors have a unique index within
+    // their datatype, but Constructor *types* do not; multiple
+    // Constructors within the same Datatype could share the same
+    // type.  So we scan through the datatype to find one that
+    // matches.
+    const Datatype& dt = type[type.getNumChildren() - 1].getConst<Datatype>();
+    for(Datatype::const_iterator i = dt.begin(),
+          i_end = dt.end();
+        i != i_end;
+        ++i) {
+      if(TypeNode::fromType((*i).getConstructor().getType()) == type) {
+        groundTerm = Node::fromExpr((*i).mkGroundTerm());
+        type.setAttribute(GroundTermAttr(), groundTerm);
+        return groundTerm;
+      }
+    }
+
+    InternalError("couldn't find a matching constructor?!");
+  }
+};/* struct ConstructorProperties */
 
 }/* CVC4::theory::datatypes namespace */
 }/* CVC4::theory namespace */
diff --git a/src/theory/mkrewriter b/src/theory/mkrewriter
index 78fc39984..ec659d0bb 100755
--- a/src/theory/mkrewriter
+++ b/src/theory/mkrewriter
@@ -125,7 +125,7 @@ function rewriter {
 }
 
 function sort {
-  # sort TYPE cardinality ["comment"]
+  # sort TYPE cardinality [well-founded ground-term header | not-well-founded] ["comment"]
   lineno=${BASH_LINENO[0]}
   check_theory_seen
 }
@@ -136,6 +136,12 @@ function cardinality {
   check_theory_seen
 }
 
+function well-founded {
+  # well-founded TYPE wellfoundedness-computer [header]
+  lineno=${BASH_LINENO[0]}
+  check_theory_seen
+}
+
 function variable {
   # variable K ["comment"]
   lineno=${BASH_LINENO[0]}
diff --git a/src/theory/mktheorytraits b/src/theory/mktheorytraits
index 9672fc871..2056c6306 100755
--- a/src/theory/mktheorytraits
+++ b/src/theory/mktheorytraits
@@ -197,10 +197,14 @@ function properties {
 }
 
 function sort {
-  # sort TYPE cardinality ["comment"]
+  # sort TYPE cardinality [well-founded ground-term header | not-well-founded] ["comment"]
   lineno=${BASH_LINENO[0]}
   check_theory_seen
-  register_sort "$1" "$2" "$3"
+  if [ "$3" = well-founded ]; then
+    register_sort "$1" "$2" "$6"
+  else
+    register_sort "$1" "$2" "$4"
+  fi
 }
 
 function cardinality {
@@ -209,6 +213,12 @@ function cardinality {
   check_theory_seen
 }
 
+function well-founded {
+  # well-founded TYPE wellfoundedness-computer [header]
+  lineno=${BASH_LINENO[0]}
+  check_theory_seen
+}
+
 function variable {
   # variable K ["comment"]
   lineno=${BASH_LINENO[0]}
diff --git a/src/theory/uf/kinds b/src/theory/uf/kinds
index d7f542038..9498fa6fb 100644
--- a/src/theory/uf/kinds
+++ b/src/theory/uf/kinds
@@ -13,7 +13,10 @@ rewriter ::CVC4::theory::uf::TheoryUfRewriter "theory/uf/theory_uf_rewriter.h"
 
 # Justified because we can have an unbounded-but-finite number of
 # sorts.  Assuming we have |Z| is probably ok for now..
-sort KIND_TYPE Cardinality::INTEGERS "Uninterpreted Sort"
+sort KIND_TYPE \
+    Cardinality::INTEGERS \
+    not-well-founded \
+    "Uninterpreted Sort"
 
 parameterized APPLY_UF VARIABLE 1: "uninterpreted function application"
 
@@ -23,5 +26,6 @@ parameterized SORT_TYPE SORT_TAG 0: "sort type"
 # enough (for now) ?  Once we support quantifiers, maybe reconsider
 # this..
 cardinality SORT_TYPE "Cardinality(Cardinality::INTEGERS)"
+well-founded SORT_TYPE false
 
 endtheory
diff --git a/src/util/Makefile.am b/src/util/Makefile.am
index a6ff0ea40..27b9e42d2 100644
--- a/src/util/Makefile.am
+++ b/src/util/Makefile.am
@@ -47,6 +47,7 @@ libutil_la_SOURCES = \
 	language.h \
 	language.cpp \
 	triple.h \
+	recursion_breaker.h \
 	subrange_bound.h \
 	cardinality.h \
 	cardinality.cpp \
diff --git a/src/util/datatype.cpp b/src/util/datatype.cpp
index afd5af703..20d63995f 100644
--- a/src/util/datatype.cpp
+++ b/src/util/datatype.cpp
@@ -23,7 +23,10 @@
 #include "util/datatype.h"
 #include "expr/type.h"
 #include "expr/expr_manager.h"
+#include "expr/expr_manager_scope.h"
+#include "expr/node_manager.h"
 #include "expr/node.h"
+#include "util/recursion_breaker.h"
 
 using namespace std;
 
@@ -32,10 +35,20 @@ namespace CVC4 {
 namespace expr {
   namespace attr {
     struct DatatypeIndexTag {};
-  }
-}
+    struct DatatypeFiniteTag {};
+    struct DatatypeWellFoundedTag {};
+    struct DatatypeFiniteComputedTag {};
+    struct DatatypeWellFoundedComputedTag {};
+    struct DatatypeGroundTermTag {};
+  }/* CVC4::expr::attr namespace */
+}/* CVC4::expr namespace */
 
 typedef expr::Attribute<expr::attr::DatatypeIndexTag, uint64_t> DatatypeIndexAttr;
+typedef expr::Attribute<expr::attr::DatatypeFiniteTag, bool> DatatypeFiniteAttr;
+typedef expr::Attribute<expr::attr::DatatypeWellFoundedTag, bool> DatatypeWellFoundedAttr;
+typedef expr::Attribute<expr::attr::DatatypeFiniteComputedTag, bool> DatatypeFiniteComputedAttr;
+typedef expr::Attribute<expr::attr::DatatypeWellFoundedComputedTag, bool> DatatypeWellFoundedComputedAttr;
+typedef expr::Attribute<expr::attr::DatatypeGroundTermTag, Node> DatatypeGroundTermAttr;
 
 const Datatype& Datatype::datatypeOf(Expr item) {
   TypeNode t = Node::fromExpr(item).getType();
@@ -73,6 +86,7 @@ void Datatype::resolve(ExprManager* em,
                 "Datatype::resolve(): resolutions doesn't contain me!");
   AssertArgument(placeholders.size() == replacements.size(), placeholders,
                 "placeholders and replacements must be the same size");
+  CheckArgument(getNumConstructors() > 0, *this, "cannot resolve a Datatype that has no constructors");
   DatatypeType self = (*resolutions.find(d_name)).second;
   AssertArgument(&self.getDatatype() == this, "Datatype::resolve(): resolutions doesn't contain me!");
   d_resolved = true;
@@ -83,6 +97,7 @@ void Datatype::resolve(ExprManager* em,
     Node::fromExpr((*i).d_constructor).setAttribute(DatatypeIndexAttr(), index);
     Node::fromExpr((*i).d_tester).setAttribute(DatatypeIndexAttr(), index++);
   }
+  d_self = self;
   Assert(index == getNumConstructors());
 }
 
@@ -92,6 +107,166 @@ void Datatype::addConstructor(const Constructor& c) {
   d_constructors.push_back(c);
 }
 
+Cardinality Datatype::getCardinality() const throw(AssertionException) {
+  CheckArgument(isResolved(), this, "this datatype is not yet resolved");
+  RecursionBreaker<const Datatype*> breaker(__PRETTY_FUNCTION__, this);
+  if(breaker.isRecursion()) {
+    return Cardinality::INTEGERS;
+  }
+  Cardinality c = 0;
+  for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) {
+    c += (*i).getCardinality();
+  }
+  return c;
+}
+
+bool Datatype::isFinite() const throw(AssertionException) {
+  CheckArgument(isResolved(), this, "this datatype is not yet resolved");
+
+  // we're using some internals, so we have to set up this library context
+  ExprManagerScope ems(d_self);
+
+  TypeNode self = TypeNode::fromType(d_self);
+
+  // is this already in the cache ?
+  if(self.getAttribute(DatatypeFiniteComputedAttr())) {
+    return self.getAttribute(DatatypeFiniteAttr());
+  }
+
+  Cardinality c = 0;
+  for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) {
+    if(! (*i).isFinite()) {
+      self.setAttribute(DatatypeFiniteComputedAttr(), true);
+      self.setAttribute(DatatypeFiniteAttr(), false);
+      return false;
+    }
+  }
+  self.setAttribute(DatatypeFiniteComputedAttr(), true);
+  self.setAttribute(DatatypeFiniteAttr(), true);
+  return true;
+}
+
+bool Datatype::isWellFounded() const throw(AssertionException) {
+  CheckArgument(isResolved(), this, "this datatype is not yet resolved");
+
+  // we're using some internals, so we have to set up this library context
+  ExprManagerScope ems(d_self);
+
+  TypeNode self = TypeNode::fromType(d_self);
+
+  // is this already in the cache ?
+  if(self.getAttribute(DatatypeWellFoundedComputedAttr())) {
+    return self.getAttribute(DatatypeWellFoundedAttr());
+  }
+
+  RecursionBreaker<const Datatype*> breaker(__PRETTY_FUNCTION__, this);
+  if(breaker.isRecursion()) {
+    // This *path* is cyclic, so may not be well-founded.  The
+    // datatype itself might still be well-founded, though (we'll find
+    // the well-foundedness along another path).
+    return false;
+  }
+
+  for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) {
+    if((*i).isWellFounded()) {
+      self.setAttribute(DatatypeWellFoundedComputedAttr(), true);
+      self.setAttribute(DatatypeWellFoundedAttr(), true);
+      return true;
+    }
+  }
+
+  self.setAttribute(DatatypeWellFoundedComputedAttr(), true);
+  self.setAttribute(DatatypeWellFoundedAttr(), false);
+  return false;
+}
+
+Expr Datatype::mkGroundTerm() const throw(AssertionException) {
+  CheckArgument(isResolved(), this, "this datatype is not yet resolved");
+
+  // we're using some internals, so we have to set up this library context
+  ExprManagerScope ems(d_self);
+
+  TypeNode self = TypeNode::fromType(d_self);
+
+  // is this already in the cache ?
+  Expr groundTerm = self.getAttribute(DatatypeGroundTermAttr()).toExpr();
+  if(!groundTerm.isNull()) {
+    Debug("datatypes") << "\nin cache: " << d_self << " => " << groundTerm << std::endl;
+    return groundTerm;
+  } else {
+    Debug("datatypes") << "\nNOT in cache: " << d_self << std::endl;
+  }
+
+  // look for a nullary ctor and use that
+  for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) {
+    // prefer the nullary constructor
+    if((*i).getNumArgs() == 0) {
+      groundTerm = (*i).getConstructor().getExprManager()->mkExpr(kind::APPLY_CONSTRUCTOR, (*i).getConstructor());
+      self.setAttribute(DatatypeGroundTermAttr(), groundTerm);
+      Debug("datatypes") << "constructed nullary: " << getName() << " => " << groundTerm << std::endl;
+      return groundTerm;
+    }
+  }
+
+  // No ctors are nullary, but we can't just use the first ctor
+  // because that might recurse!  In fact, since this datatype is
+  // well-founded by assumption, we know that at least one constructor
+  // doesn't contain a self-reference.  We search for that one and use
+  // it to construct the ground term, as that is often a simpler
+  // ground term (e.g. in a tree datatype, something like "(leaf 0)"
+  // is simpler than "(node (leaf 0) (leaf 0))".
+  //
+  // Of course this check doesn't always work, if the self-reference
+  // is through other Datatypes (or other non-Datatype types), but it
+  // does simplify a common case.  It requires a bit of extra work,
+  // but since we cache the results of these, it only happens once,
+  // ever, per Datatype.
+  //
+  // If the datatype is not actually well-founded, something below
+  // will throw an exception.
+  for(const_iterator i = begin(), i_end = end();
+      i != i_end;
+      ++i) {
+    Constructor::const_iterator j = (*i).begin(), j_end = (*i).end();
+    for(; j != j_end; ++j) {
+      SelectorType stype((*j).getSelector().getType());
+      if(stype.getDomain() == stype.getRangeType()) {
+        Debug("datatypes") << "self-reference, skip " << getName() << "::" << (*i).getName() << std::endl;
+        // the constructor contains a direct self-reference
+        break;
+      }
+    }
+
+    if(j == j_end && (*i).isWellFounded()) {
+      groundTerm = (*i).mkGroundTerm();
+      // Constructor::mkGroundTerm() doesn't ever return null when
+      // called from the outside.  But in recursive invocations, it
+      // can: say you have dt = a(one:dt) | b(two:INT), and you ask
+      // the "a" constructor for a ground term.  It asks "dt" for a
+      // ground term, which in turn asks the "a" constructor for a
+      // ground term!  Thus, even though "a" is a well-founded
+      // constructor, it cannot construct a ground-term by itself.  We
+      // have to skip past it, and we do that with a
+      // RecursionBreaker<> in Constructor::mkGroundTerm().  In the
+      // case of recursion, it returns null.
+      if(!groundTerm.isNull()) {
+        // we found a ground-term-constructing constructor!
+        self.setAttribute(DatatypeGroundTermAttr(), groundTerm);
+        Debug("datatypes") << "constructed: " << getName() << " => " << groundTerm << std::endl;
+        return groundTerm;
+      }
+    }
+  }
+  // if we get all the way here, we aren't well-founded
+  CheckArgument(false, *this, "this datatype is not well-founded, cannot construct a ground term!");
+}
+
+DatatypeType Datatype::getDatatypeType() const throw(AssertionException) {
+  CheckArgument(isResolved(), *this, "Datatype must be resolved to get its DatatypeType");
+  Assert(!d_self.isNull());
+  return DatatypeType(d_self);
+}
+
 bool Datatype::operator==(const Datatype& other) const throw() {
   // two datatypes are == iff the name is the same and they have
   // exactly matching constructors (in the same order)
@@ -279,15 +454,131 @@ std::string Datatype::Constructor::getName() const throw() {
 }
 
 Expr Datatype::Constructor::getConstructor() const {
-  CheckArgument(isResolved(), this, "this datatype constructor not yet resolved");
+  CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
   return d_constructor;
 }
 
 Expr Datatype::Constructor::getTester() const {
-  CheckArgument(isResolved(), this, "this datatype constructor not yet resolved");
+  CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
   return d_tester;
 }
 
+Cardinality Datatype::Constructor::getCardinality() const throw(AssertionException) {
+  CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
+
+  Cardinality c = 1;
+
+  for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) {
+    c *= SelectorType((*i).getSelector().getType()).getRangeType().getCardinality();
+  }
+
+  return c;
+}
+
+bool Datatype::Constructor::isFinite() const throw(AssertionException) {
+  CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
+
+  // we're using some internals, so we have to set up this library context
+  ExprManagerScope ems(d_constructor);
+
+  TNode self = Node::fromExpr(d_constructor);
+
+  // is this already in the cache ?
+  if(self.getAttribute(DatatypeFiniteComputedAttr())) {
+    return self.getAttribute(DatatypeFiniteAttr());
+  }
+
+  for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) {
+    if(! SelectorType((*i).getSelector().getType()).getRangeType().getCardinality().isFinite()) {
+      self.setAttribute(DatatypeFiniteComputedAttr(), true);
+      self.setAttribute(DatatypeFiniteAttr(), false);
+      return false;
+    }
+  }
+
+  self.setAttribute(DatatypeFiniteComputedAttr(), true);
+  self.setAttribute(DatatypeFiniteAttr(), true);
+  return true;
+}
+
+bool Datatype::Constructor::isWellFounded() const throw(AssertionException) {
+  CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
+
+  // we're using some internals, so we have to set up this library context
+  ExprManagerScope ems(d_constructor);
+
+  TNode self = Node::fromExpr(d_constructor);
+
+  // is this already in the cache ?
+  if(self.getAttribute(DatatypeWellFoundedComputedAttr())) {
+    return self.getAttribute(DatatypeWellFoundedAttr());
+  }
+
+  RecursionBreaker<const Datatype::Constructor*> breaker(__PRETTY_FUNCTION__, this);
+  if(breaker.isRecursion()) {
+    // This *path* is cyclic, sso may not be well-founded.  The
+    // constructor itself might still be well-founded, though (we'll
+    // find the well-foundedness along another path).
+    return false;
+  }
+
+  for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) {
+    if(! SelectorType((*i).getSelector().getType()).getRangeType().isWellFounded()) {
+      /* FIXME - we can't cache a negative result here, because a
+         Datatype might tell us it's not well founded along this
+         *path*, due to recursion, when it really is well-founded.
+         This should be fixed by creating private functions to do the
+         recursion here, and leaving the (public-facing)
+         isWellFounded() call as the base of that recursion.  Then we
+         can distinguish the cases.
+      */
+      /*
+      self.setAttribute(DatatypeWellFoundedComputedAttr(), true);
+      self.setAttribute(DatatypeWellFoundedAttr(), false);
+      */
+      return false;
+    }
+  }
+
+  self.setAttribute(DatatypeWellFoundedComputedAttr(), true);
+  self.setAttribute(DatatypeWellFoundedAttr(), true);
+  return true;
+}
+
+Expr Datatype::Constructor::mkGroundTerm() const throw(AssertionException) {
+  CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
+
+  // we're using some internals, so we have to set up this library context
+  ExprManagerScope ems(d_constructor);
+
+  TNode self = Node::fromExpr(d_constructor);
+
+  // is this already in the cache ?
+  Expr groundTerm = self.getAttribute(DatatypeGroundTermAttr()).toExpr();
+  if(!groundTerm.isNull()) {
+    return groundTerm;
+  }
+
+  RecursionBreaker<const Datatype::Constructor*> breaker(__PRETTY_FUNCTION__, this);
+  if(breaker.isRecursion()) {
+    // Recursive path, we should skip and go to the next constructor;
+    // see lengthy comments in Datatype::mkGroundTerm().
+    return Expr();
+  }
+
+  std::vector<Expr> groundTerms;
+  groundTerms.push_back(getConstructor());
+
+  // for each selector, get a ground term
+  for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) {
+    groundTerms.push_back(SelectorType((*i).getSelector().getType()).getRangeType().mkGroundTerm());
+  }
+
+  groundTerm = getConstructor().getExprManager()->mkExpr(kind::APPLY_CONSTRUCTOR, groundTerms);
+  self.setAttribute(DatatypeGroundTermAttr(), groundTerm);
+  return groundTerm;
+}
+
 const Datatype::Constructor::Arg& Datatype::Constructor::operator[](size_t index) const {
   CheckArgument(index < getNumArgs(), index, "index out of bounds");
   return d_args[index];
@@ -346,7 +637,7 @@ std::ostream& operator<<(std::ostream& os, const Datatype& dt) {
   // These datatype things are recursive!  Be very careful not to
   // print an infinite chain of them.
   long& printNameOnly = os.iword(s_printDatatypeNamesOnly);
-  Debug("datatypes") << "printNameOnly is " << printNameOnly << std::endl;
+  Debug("datatypes-output") << "printNameOnly is " << printNameOnly << std::endl;
   if(printNameOnly) {
     return os << dt.getName();
   }
@@ -360,7 +651,7 @@ std::ostream& operator<<(std::ostream& os, const Datatype& dt) {
   } scope(printNameOnly, 1);
   // when scope is destructed, the value pops back
 
-  Debug("datatypes") << "printNameOnly is now " << printNameOnly << std::endl;
+  Debug("datatypes-output") << "printNameOnly is now " << printNameOnly << std::endl;
 
   // can only output datatypes in the CVC4 native language
   Expr::setlanguage::Scope ls(os, language::output::LANG_CVC4);
diff --git a/src/util/datatype.h b/src/util/datatype.h
index 74bff1843..df7dd1814 100644
--- a/src/util/datatype.h
+++ b/src/util/datatype.h
@@ -99,8 +99,17 @@ public:
  */
 class CVC4_PUBLIC Datatype {
 public:
-  static const Datatype& datatypeOf(Expr item);
-  static size_t indexOf(Expr item);
+  /**
+   * Get the datatype of a constructor, selector, or tester operator.
+   */
+  static const Datatype& datatypeOf(Expr item) CVC4_PUBLIC;
+
+  /**
+   * Get the index of a constructor or tester in its datatype, or the
+   * index of a selector in its constructor.  (Zero is always the
+   * first index.)
+   */
+  static size_t indexOf(Expr item) CVC4_PUBLIC;
 
   /**
    * A holder type (used in calls to Datatype::Constructor::addArg())
@@ -244,6 +253,33 @@ public:
     inline size_t getNumArgs() const throw();
 
     /**
+     * Return the cardinality of this constructor (the product of the
+     * cardinalities of its arguments).
+     */
+    Cardinality getCardinality() const throw(AssertionException);
+
+    /**
+     * Return true iff this constructor is finite (it is nullary or
+     * each of its argument types are finite).  This function can
+     * only be called for resolved constructors.
+     */
+    bool isFinite() const throw(AssertionException);
+
+    /**
+     * Return true iff this constructor is well-founded (there exist
+     * ground terms).  The constructor must be resolved or an
+     * exception is thrown.
+     */
+    bool isWellFounded() const throw(AssertionException);
+
+    /**
+     * Construct and return a ground term of this constructor.  The
+     * constructor must be both resolved and well-founded, or else an
+     * exception is thrown.
+     */
+    Expr mkGroundTerm() const throw(AssertionException);
+
+    /**
      * Returns true iff this Datatype constructor has already been
      * resolved.
      */
@@ -272,6 +308,7 @@ private:
   std::string d_name;
   std::vector<Constructor> d_constructors;
   bool d_resolved;
+  Type d_self;
 
   /**
    * Datatypes refer to themselves, recursively, and we have a
@@ -303,6 +340,40 @@ public:
   inline size_t getNumConstructors() const throw();
 
   /**
+   * Return the cardinality of this datatype (the sum of the
+   * cardinalities of its constructors).  The Datatype must be
+   * resolved.
+   */
+  Cardinality getCardinality() const throw(AssertionException);
+
+  /**
+   * Return  true iff this  Datatype is  finite (all  constructors are
+   * finite,  i.e., there  are finitely  many ground  terms).   If the
+   * datatype is  not well-founded, this function  returns false.  The
+   * Datatype must be resolved or an exception is thrown.
+   */
+  bool isFinite() const throw(AssertionException);
+
+  /**
+   * Return true iff this datatype is well-founded (there exist ground
+   * terms).  The Datatype must be resolved or an exception is thrown.
+   */
+  bool isWellFounded() const throw(AssertionException);
+
+  /**
+   * Construct and return a ground term of this Datatype.  The
+   * Datatype must be both resolved and well-founded, or else an
+   * exception is thrown.
+   */
+  Expr mkGroundTerm() const throw(AssertionException);
+
+  /**
+   * Get the DatatypeType associated to this Datatype.  Can only be
+   * called post-resolution.
+   */
+  DatatypeType getDatatypeType() const throw(AssertionException);
+
+  /**
    * Return true iff the two Datatypes are the same.
    *
    * We need == for mkConst(Datatype) to properly work---since if the
@@ -372,7 +443,8 @@ inline std::string Datatype::UnresolvedType::getName() const throw() {
 inline Datatype::Datatype(std::string name) :
   d_name(name),
   d_constructors(),
-  d_resolved(false) {
+  d_resolved(false),
+  d_self() {
 }
 
 inline std::string Datatype::getName() const throw() {
diff --git a/src/util/recursion_breaker.h b/src/util/recursion_breaker.h
new file mode 100644
index 000000000..6f82eec5c
--- /dev/null
+++ b/src/util/recursion_breaker.h
@@ -0,0 +1,133 @@
+/*********************                                                        */
+/*! \file recursion_breaker.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, 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
+ ** information.\endverbatim
+ **
+ ** \brief A utility class to help with detecting recursion in a
+ ** computation
+ **
+ ** A utility class to help with detecting recursion in a computation.
+ ** A breadcrumb trail is left, and a function can query the breaker
+ ** to see if recursion has occurred.  For example:
+ **
+ **   int foo(int x) {
+ **     RecursionBreaker<int> breaker("foo", x);
+ **     if(breaker.isRecursion()) {
+ **       ++d_count;
+ **       return 0;
+ **     }
+ **     int xfactor = x * x;
+ **     if(x > 0) {
+ **       xfactor = -xfactor;
+ **     }
+ **     int y = foo(11 * x + xfactor);
+ **     int z = y < 0 ? y : x * y;
+ **     cout << "x == " << x << ", y == " << y << " ==> " << z << endl;
+ **     return z;
+ **   }
+ **
+ ** Recursion occurs after a while in this example, and the recursion
+ ** is broken by the RecursionBreaker.
+ **
+ ** RecursionBreaker is really just a thread-local set of "what has
+ ** been seen."  The above example is trivial, easily fixed by
+ ** allocating such a set at the base of the recursion, and passing a
+ ** reference to it to each invocation.  But other cases of
+ ** nontrivial, mutual recursion exist that aren't so easily broken,
+ ** and that's what the RecursionBreaker is for.  See
+ ** Datatype::getCardinality(), for example.  A Datatype's cardinality
+ ** depends on the cardinalities of the types it references---but
+ ** these, in turn can reference the original datatype in a cyclic
+ ** fashion.  Where that happens, we need to break the recursion.
+ **
+ ** Several RecursionBreakers can be used at once; each is identified
+ ** by the string tag in its constructor.  If a single function is
+ ** involved in the detection of recursion, a good choice is to use
+ ** __FUNCTION__:
+ **
+ **   RecursionBreaker<Foo*>(__FUNCTION__, this) breaker;
+ **
+ ** Of course, if you're using GNU, you might prefer
+ ** __PRETTY_FUNCTION__, since it's robust to overloading, namespaces,
+ ** and containing classes.  But neither is a good choice if two
+ ** functions need to access the same RecursionBreaker mechanism.
+ **
+ ** For non-primitive datatypes, it might be a good idea to use a
+ ** pointer type to instantiate RecursionBreaker<>, for example with
+ ** RecursionBreaker<Foo*>.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__RECURSION_BREAKER_H
+#define __CVC4__RECURSION_BREAKER_H
+
+#include <string>
+#include <map>
+#include <ext/hash_set>
+#include "util/hash.h"
+#include "util/tls.h"
+#include "util/Assert.h"
+
+namespace CVC4 {
+
+template <class T>
+class RecursionBreaker {
+  //typedef std::hash_set<T> Set;
+  typedef std::set<T> Set;
+  typedef std::map<std::string, Set> Map;
+  static CVC4_THREADLOCAL(Map*) s_maps;
+
+  std::string d_tag;
+  const T& d_item;
+  bool d_firstToTag;
+  bool d_recursion;
+
+public:
+  RecursionBreaker(std::string tag, const T& item) :
+    d_tag(tag),
+    d_item(item) {
+    if(s_maps == NULL) {
+      s_maps = new Map();
+    }
+    d_firstToTag = s_maps->find(tag) == s_maps->end();
+    Set& set = (*s_maps)[tag];
+    d_recursion = (set.find(item) != set.end());
+    Assert(!d_recursion || !d_firstToTag);
+    if(!d_recursion) {
+      set.insert(item);
+    }
+  }
+
+  ~RecursionBreaker() {
+    Assert(s_maps->find(d_tag) != s_maps->end());
+    if(!d_recursion) {
+      (*s_maps)[d_tag].erase(d_item);
+    }
+    if(d_firstToTag) {
+      Assert((*s_maps)[d_tag].empty());
+      s_maps->erase(d_tag);
+      Assert(s_maps->find(d_tag) == s_maps->end());
+    }
+  }
+
+  bool isRecursion() const throw() {
+    return d_recursion;
+  }
+
+};/* class RecursionBreaker<T> */
+
+template <class T>
+CVC4_THREADLOCAL(typename RecursionBreaker<T>::Map*) RecursionBreaker<T>::s_maps;
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__RECURSION_BREAKER_H */