Merge from nonclausal-simplification-v2 branch:

* Preprocessing-time, non-clausal, Boolean simplification round to
  support "quasi-non-linear rewrites" as discussed at last few meetings.

* --simplification=none is the default for now, but we'll probably
  change that to --simplification=incremental.  --simplification=batch
  is also a possibility.  See --simplification=help for details.

* RecursionBreaker<T> now uses a hash set for the seen trail.
* Fixes to TLS stuff to support that.
* Fixes to theory and SmtEngine documentation.
* Fixes to stream indentation.
* Other miscellaneous stuff.

1 files changed, 7 insertions, 5 deletions

diff --git a/src/util/recursion_breaker.h b/src/util/recursion_breaker.h
index 6f82eec5c..6573e9b64 100644
--- a/src/util/recursion_breaker.h
+++ b/src/util/recursion_breaker.h
@@ -79,10 +79,9 @@
 
 namespace CVC4 {
 
-template <class T>
+template <class T, class Hasher = std::hash<T> >
 class RecursionBreaker {
-  //typedef std::hash_set<T> Set;
-  typedef std::set<T> Set;
+  typedef std::hash_set<T, Hasher> Set;
   typedef std::map<std::string, Set> Map;
   static CVC4_THREADLOCAL(Map*) s_maps;
 
@@ -92,6 +91,7 @@ class RecursionBreaker {
   bool d_recursion;
 
 public:
+  /** Mark that item has been seen for tag. */
   RecursionBreaker(std::string tag, const T& item) :
     d_tag(tag),
     d_item(item) {
@@ -107,6 +107,7 @@ public:
     }
   }
 
+  /** Clean up the seen trail. */
   ~RecursionBreaker() {
     Assert(s_maps->find(d_tag) != s_maps->end());
     if(!d_recursion) {
@@ -119,14 +120,15 @@ public:
     }
   }
 
+  /** Return true iff recursion has been detected. */
   bool isRecursion() const throw() {
     return d_recursion;
   }
 
 };/* class RecursionBreaker<T> */
 
-template <class T>
-CVC4_THREADLOCAL(typename RecursionBreaker<T>::Map*) RecursionBreaker<T>::s_maps;
+template <class T, class Hasher>
+CVC4_THREADLOCAL(typename RecursionBreaker<T, Hasher>::Map*) RecursionBreaker<T, Hasher>::s_maps;
 
 }/* CVC4 namespace */