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, 133 insertions, 0 deletions

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