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

1 files changed, 57 insertions, 0 deletions

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 */