diff options
author | Morgan Deters <mdeters@gmail.com> | 2011-05-05 22:23:50 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2011-05-05 22:23:50 +0000 |
commit | fef0f8190fc7e5f3b88b33e7574b7df1e629e80f (patch) | |
tree | dfdda739bf5008096860e19f6b9275fb2a257960 /src/util/recursion_breaker.h | |
parent | 90d8205a86b698c2548108ca4db124fe9c3f738a (diff) |
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.
Diffstat (limited to 'src/util/recursion_breaker.h')
-rw-r--r-- | src/util/recursion_breaker.h | 12 |
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 */ |