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

10 files changed, 250 insertions, 17 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 */