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

3 files changed, 325 insertions, 10 deletions

diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am
index f50cc32db..691f33406 100644
--- a/test/unit/Makefile.am
+++ b/test/unit/Makefile.am
@@ -48,6 +48,7 @@ UNIT_TESTS = \
 	util/boolean_simplification_black \
 	util/subrange_bound_white \
 	util/cardinality_public \
+	util/recursion_breaker_black \
 	main/interactive_shell_black
 
 export VERBOSE = 1
diff --git a/test/unit/util/datatype_black.h b/test/unit/util/datatype_black.h
index 991d71364..1ac4caaec 100644
--- a/test/unit/util/datatype_black.h
+++ b/test/unit/util/datatype_black.h
@@ -35,12 +35,54 @@ public:
 
   void setUp() {
     d_em = new ExprManager();
+    Debug.on("datatypes");
+    Debug.on("groundterms");
   }
 
   void tearDown() {
     delete d_em;
   }
 
+  void testEnumeration() {
+    Datatype colors("colors");
+
+    Datatype::Constructor yellow("yellow", "is_yellow");
+    Datatype::Constructor blue("blue", "is_blue");
+    Datatype::Constructor green("green", "is_green");
+    Datatype::Constructor red("red", "is_red");
+
+    colors.addConstructor(yellow);
+    colors.addConstructor(blue);
+    colors.addConstructor(green);
+    colors.addConstructor(red);
+
+    Debug("datatypes") << colors << std::endl;
+    DatatypeType colorsType = d_em->mkDatatypeType(colors);
+    Debug("datatypes") << colorsType << std::endl;
+
+    Expr ctor = colorsType.getDatatype()[1].getConstructor();
+    Expr apply = d_em->mkExpr(kind::APPLY_CONSTRUCTOR, ctor);
+    Debug("datatypes") << apply << std::endl;
+
+    TS_ASSERT(colorsType.getDatatype().isFinite());
+    TS_ASSERT(colorsType.getDatatype().getCardinality() == 4);
+    TS_ASSERT(ctor.getType().getCardinality() == 1);
+    TS_ASSERT(colorsType.getDatatype().isWellFounded());
+    Debug("groundterms") << "ground term of " << colorsType.getDatatype().getName() << endl
+                         << "  is " << colorsType.mkGroundTerm() << endl;
+    TS_ASSERT(colorsType.mkGroundTerm().getType() == colorsType);
+    // all ctors should be well-founded too
+    for(Datatype::const_iterator i = colorsType.getDatatype().begin(),
+          i_end = colorsType.getDatatype().end();
+        i != i_end;
+        ++i) {
+      TS_ASSERT((*i).isWellFounded());
+      Debug("groundterms") << "ground term of " << *i << endl
+                           << "  is " << (*i).mkGroundTerm() << endl;
+      TS_ASSERT((*i).mkGroundTerm().getType() == colorsType);
+    }
+  }
+
   void testNat() {
     Datatype nat("nat");
 
@@ -51,13 +93,31 @@ public:
     Datatype::Constructor zero("zero", "is_zero");
     nat.addConstructor(zero);
 
-    cout << nat << std::endl;
+    Debug("datatypes") << nat << std::endl;
     DatatypeType natType = d_em->mkDatatypeType(nat);
-    cout << natType << std::endl;
+    Debug("datatypes") << natType << std::endl;
 
     Expr ctor = natType.getDatatype()[1].getConstructor();
     Expr apply = d_em->mkExpr(kind::APPLY_CONSTRUCTOR, ctor);
-    cout << apply << std::endl;
+    Debug("datatypes") << apply << std::endl;
+
+    TS_ASSERT(! natType.getDatatype().isFinite());
+    TS_ASSERT(natType.getDatatype().getCardinality() == Cardinality::INTEGERS);
+    TS_ASSERT(natType.getDatatype().isWellFounded());
+    Debug("groundterms") << "ground term of " << natType.getDatatype().getName() << endl
+                         << "  is " << natType.mkGroundTerm() << endl;
+    TS_ASSERT(natType.mkGroundTerm().getType() == natType);
+    // all ctors should be well-founded too
+    for(Datatype::const_iterator i = natType.getDatatype().begin(),
+          i_end = natType.getDatatype().end();
+        i != i_end;
+        ++i) {
+      Debug("datatypes") << "checking " << (*i).getName() << endl;
+      TS_ASSERT((*i).isWellFounded());
+      Debug("groundterms") << "ground term of " << *i << endl
+                           << "  is " << (*i).mkGroundTerm() << endl;
+      TS_ASSERT((*i).mkGroundTerm().getType() == natType);
+    }
   }
 
   void testTree() {
@@ -73,12 +133,29 @@ public:
     leaf.addArg("leaf", integerType);
     tree.addConstructor(leaf);
 
-    cout << tree << std::endl;
+    Debug("datatypes") << tree << std::endl;
     DatatypeType treeType = d_em->mkDatatypeType(tree);
-    cout << treeType << std::endl;
+    Debug("datatypes") << treeType << std::endl;
+
+    TS_ASSERT(! treeType.getDatatype().isFinite());
+    TS_ASSERT(treeType.getDatatype().getCardinality() == Cardinality::INTEGERS);
+    TS_ASSERT(treeType.getDatatype().isWellFounded());
+    Debug("groundterms") << "ground term of " << treeType.getDatatype().getName() << endl
+                         << "  is " << treeType.mkGroundTerm() << endl;
+    TS_ASSERT(treeType.mkGroundTerm().getType() == treeType);
+    // all ctors should be well-founded too
+    for(Datatype::const_iterator i = treeType.getDatatype().begin(),
+          i_end = treeType.getDatatype().end();
+        i != i_end;
+        ++i) {
+      TS_ASSERT((*i).isWellFounded());
+      Debug("groundterms") << "ground term of " << *i << endl
+                           << "  is " << (*i).mkGroundTerm() << endl;
+      TS_ASSERT((*i).mkGroundTerm().getType() == treeType);
+    }
   }
 
-  void testList() {
+  void testListInt() {
     Datatype list("list");
     Type integerType = d_em->integerType();
 
@@ -90,9 +167,94 @@ public:
     Datatype::Constructor nil("nil", "is_nil");
     list.addConstructor(nil);
 
-    cout << list << std::endl;
+    Debug("datatypes") << list << std::endl;
+    DatatypeType listType = d_em->mkDatatypeType(list);
+    Debug("datatypes") << listType << std::endl;
+
+    TS_ASSERT(! listType.getDatatype().isFinite());
+    TS_ASSERT(listType.getDatatype().getCardinality() == Cardinality::INTEGERS);
+    TS_ASSERT(listType.getDatatype().isWellFounded());
+    Debug("groundterms") << "ground term of " << listType.getDatatype().getName() << endl
+                         << "  is " << listType.mkGroundTerm() << endl;
+    TS_ASSERT(listType.mkGroundTerm().getType() == listType);
+    // all ctors should be well-founded too
+    for(Datatype::const_iterator i = listType.getDatatype().begin(),
+          i_end = listType.getDatatype().end();
+        i != i_end;
+        ++i) {
+      TS_ASSERT((*i).isWellFounded());
+      Debug("groundterms") << "ground term of " << *i << endl
+                           << "  is " << (*i).mkGroundTerm() << endl;
+      TS_ASSERT((*i).mkGroundTerm().getType() == listType);
+    }
+  }
+
+  void testListReal() {
+    Datatype list("list");
+    Type realType = d_em->realType();
+
+    Datatype::Constructor cons("cons", "is_cons");
+    cons.addArg("car", realType);
+    cons.addArg("cdr", Datatype::SelfType());
+    list.addConstructor(cons);
+
+    Datatype::Constructor nil("nil", "is_nil");
+    list.addConstructor(nil);
+
+    Debug("datatypes") << list << std::endl;
     DatatypeType listType = d_em->mkDatatypeType(list);
-    cout << listType << std::endl;
+    Debug("datatypes") << listType << std::endl;
+
+    TS_ASSERT(! listType.getDatatype().isFinite());
+    TS_ASSERT(listType.getDatatype().getCardinality() == Cardinality::REALS);
+    TS_ASSERT(listType.getDatatype().isWellFounded());
+    Debug("groundterms") << "ground term of " << listType.getDatatype().getName() << endl
+                         << "  is " << listType.mkGroundTerm() << endl;
+    TS_ASSERT(listType.mkGroundTerm().getType() == listType);
+    // all ctors should be well-founded too
+    for(Datatype::const_iterator i = listType.getDatatype().begin(),
+          i_end = listType.getDatatype().end();
+        i != i_end;
+        ++i) {
+      TS_ASSERT((*i).isWellFounded());
+      Debug("groundterms") << "ground term of " << *i << endl
+                           << "  is " << (*i).mkGroundTerm() << endl;
+      TS_ASSERT((*i).mkGroundTerm().getType() == listType);
+    }
+  }
+
+  void testListBoolean() {
+    Datatype list("list");
+    Type booleanType = d_em->booleanType();
+
+    Datatype::Constructor cons("cons", "is_cons");
+    cons.addArg("car", booleanType);
+    cons.addArg("cdr", Datatype::SelfType());
+    list.addConstructor(cons);
+
+    Datatype::Constructor nil("nil", "is_nil");
+    list.addConstructor(nil);
+
+    Debug("datatypes") << list << std::endl;
+    DatatypeType listType = d_em->mkDatatypeType(list);
+    Debug("datatypes") << listType << std::endl;
+
+    TS_ASSERT(! listType.getDatatype().isFinite());
+    TS_ASSERT(listType.getDatatype().getCardinality() == Cardinality::INTEGERS);
+    TS_ASSERT(listType.getDatatype().isWellFounded());
+    Debug("groundterms") << "ground term of " << listType.getDatatype().getName() << endl
+                         << "  is " << listType.mkGroundTerm() << endl;
+    TS_ASSERT(listType.mkGroundTerm().getType() == listType);
+    // all ctors should be well-founded too
+    for(Datatype::const_iterator i = listType.getDatatype().begin(),
+          i_end = listType.getDatatype().end();
+        i != i_end;
+        ++i) {
+      TS_ASSERT((*i).isWellFounded());
+      Debug("groundterms") << "ground term of " << *i << endl
+                           << "  is " << (*i).mkGroundTerm() << endl;
+      TS_ASSERT((*i).mkGroundTerm().getType() == listType);
+    }
   }
 
   void testMutualListTrees() {
@@ -114,7 +276,7 @@ public:
     leaf.addArg("leaf", Datatype::UnresolvedType("list"));
     tree.addConstructor(leaf);
 
-    cout << tree << std::endl;
+    Debug("datatypes") << tree << std::endl;
 
     Datatype list("list");
     Datatype::Constructor cons("cons", "is_cons");
@@ -125,7 +287,7 @@ public:
     Datatype::Constructor nil("nil", "is_nil");
     list.addConstructor(nil);
 
-    cout << list << std::endl;
+    Debug("datatypes") << list << std::endl;
 
     TS_ASSERT(! tree.isResolved());
     TS_ASSERT(! node.isResolved());
@@ -142,6 +304,40 @@ public:
     TS_ASSERT(dtts[0].getDatatype().isResolved());
     TS_ASSERT(dtts[1].getDatatype().isResolved());
 
+    TS_ASSERT(! dtts[0].getDatatype().isFinite());
+    TS_ASSERT(dtts[0].getDatatype().getCardinality() == Cardinality::INTEGERS);
+    TS_ASSERT(dtts[0].getDatatype().isWellFounded());
+    Debug("groundterms") << "ground term of " << dtts[0].getDatatype().getName() << endl
+                         << "  is " << dtts[0].mkGroundTerm() << endl;
+    TS_ASSERT(dtts[0].mkGroundTerm().getType() == dtts[0]);
+    // all ctors should be well-founded too
+    for(Datatype::const_iterator i = dtts[0].getDatatype().begin(),
+          i_end = dtts[0].getDatatype().end();
+        i != i_end;
+        ++i) {
+      TS_ASSERT((*i).isWellFounded());
+      Debug("groundterms") << "ground term of " << *i << endl
+                           << "  is " << (*i).mkGroundTerm() << endl;
+      TS_ASSERT((*i).mkGroundTerm().getType() == dtts[0]);
+    }
+
+    TS_ASSERT(! dtts[1].getDatatype().isFinite());
+    TS_ASSERT(dtts[1].getDatatype().getCardinality() == Cardinality::INTEGERS);
+    TS_ASSERT(dtts[1].getDatatype().isWellFounded());
+    Debug("groundterms") << "ground term of " << dtts[1].getDatatype().getName() << endl
+                         << "  is " << dtts[1].mkGroundTerm() << endl;
+    TS_ASSERT(dtts[1].mkGroundTerm().getType() == dtts[1]);
+    // all ctors should be well-founded too
+    for(Datatype::const_iterator i = dtts[1].getDatatype().begin(),
+          i_end = dtts[1].getDatatype().end();
+        i != i_end;
+        ++i) {
+      TS_ASSERT((*i).isWellFounded());
+      Debug("groundterms") << "ground term of " << *i << endl
+                           << "  is " << (*i).mkGroundTerm() << endl;
+      TS_ASSERT((*i).mkGroundTerm().getType() == dtts[1]);
+    }
+
     // add another constructor to list datatype resulting in an
     // "otherNil-list"
     Datatype::Constructor otherNil("otherNil", "is_otherNil");
@@ -155,6 +351,67 @@ public:
 
     // tree is also different because it's a tree of otherNil-lists
     TS_ASSERT_DIFFERS(dtts[0], dtts2[0]);
+
+    TS_ASSERT(! dtts2[0].getDatatype().isFinite());
+    TS_ASSERT(dtts2[0].getDatatype().getCardinality() == Cardinality::INTEGERS);
+    TS_ASSERT(dtts2[0].getDatatype().isWellFounded());
+    Debug("groundterms") << "ground term of " << dtts2[0].getDatatype().getName() << endl
+                         << "  is " << dtts2[0].mkGroundTerm() << endl;
+    TS_ASSERT(dtts2[0].mkGroundTerm().getType() == dtts2[0]);
+    // all ctors should be well-founded too
+    for(Datatype::const_iterator i = dtts2[0].getDatatype().begin(),
+          i_end = dtts2[0].getDatatype().end();
+        i != i_end;
+        ++i) {
+      TS_ASSERT((*i).isWellFounded());
+      Debug("groundterms") << "ground term of " << *i << endl
+                           << "  is " << (*i).mkGroundTerm() << endl;
+      TS_ASSERT((*i).mkGroundTerm().getType() == dtts2[0]);
+    }
+
+    TS_ASSERT(! dtts2[1].getDatatype().isFinite());
+    TS_ASSERT(dtts2[1].getDatatype().getCardinality() == Cardinality::INTEGERS);
+    TS_ASSERT(dtts2[1].getDatatype().isWellFounded());
+    Debug("groundterms") << "ground term of " << dtts2[1].getDatatype().getName() << endl
+                         << "  is " << dtts2[1].mkGroundTerm() << endl;
+    TS_ASSERT(dtts2[1].mkGroundTerm().getType() == dtts2[1]);
+    // all ctors should be well-founded too
+    for(Datatype::const_iterator i = dtts2[1].getDatatype().begin(),
+          i_end = dtts2[1].getDatatype().end();
+        i != i_end;
+        ++i) {
+      TS_ASSERT((*i).isWellFounded());
+      Debug("groundterms") << "ground term of " << *i << endl
+                           << "  is " << (*i).mkGroundTerm() << endl;
+      TS_ASSERT((*i).mkGroundTerm().getType() == dtts2[1]);
+    }
+  }
+
+  void testNotSoWellFounded() {
+    Datatype tree("tree");
+
+    Datatype::Constructor node("node", "is_node");
+    node.addArg("left", Datatype::SelfType());
+    node.addArg("right", Datatype::SelfType());
+    tree.addConstructor(node);
+
+    Debug("datatypes") << tree << std::endl;
+    DatatypeType treeType = d_em->mkDatatypeType(tree);
+    Debug("datatypes") << treeType << std::endl;
+
+    TS_ASSERT(! treeType.getDatatype().isFinite());
+    TS_ASSERT(treeType.getDatatype().getCardinality() == Cardinality::INTEGERS);
+    TS_ASSERT(! treeType.getDatatype().isWellFounded());
+    TS_ASSERT_THROWS_ANYTHING( treeType.mkGroundTerm() );
+    TS_ASSERT_THROWS_ANYTHING( treeType.getDatatype().mkGroundTerm() );
+    // all ctors should be not-well-founded either
+    for(Datatype::const_iterator i = treeType.getDatatype().begin(),
+          i_end = treeType.getDatatype().end();
+        i != i_end;
+        ++i) {
+      TS_ASSERT(! (*i).isWellFounded());
+      TS_ASSERT_THROWS_ANYTHING( (*i).mkGroundTerm() );
+    }
   }
 
 };/* class DatatypeBlack */
diff --git a/test/unit/util/recursion_breaker_black.h b/test/unit/util/recursion_breaker_black.h
new file mode 100644
index 000000000..41e498919
--- /dev/null
+++ b/test/unit/util/recursion_breaker_black.h
@@ -0,0 +1,57 @@
+/*********************                                                        */
+/*! \file recursion_breaker_black.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 Black-box testing of RecursionBreaker<T>
+ **
+ ** Black-box testing of RecursionBreaker<T>.
+ **/
+
+#include <iostream>
+#include <string>
+
+#include "util/recursion_breaker.h"
+
+using namespace CVC4;
+using namespace std;
+
+class RecursionBreakerBlack : public CxxTest::TestSuite {
+  int d_count;
+
+public:
+
+  void setUp() {
+    d_count = 0;
+  }
+
+  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;
+  }
+
+  void testFoo() {
+    foo(5);
+    TS_ASSERT( d_count == 1 );
+  }
+
+};/* class RecursionBreakerBlack */