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, 51 insertions, 4 deletions

diff --git a/src/util/tls.h.in b/src/util/tls.h.in
index c2892d11c..fc0b6932b 100644
--- a/src/util/tls.h.in
+++ b/src/util/tls.h.in
@@ -26,13 +26,17 @@
 
 #line 28 "@srcdir@/tls.h.in"
 
+// A bit obnoxious: we have to take varargs to support multi-argument
+// template types in the threadlocals.
+// E.g. "CVC4_THREADLOCAL(hash_set<type, hasher>*)" fails otherwise,
+// due to the embedded comma.
 #if @CVC4_TLS_SUPPORTED@
-#  define CVC4_THREADLOCAL(__type) @CVC4_TLS@ __type
-#  define CVC4_THREADLOCAL_PUBLIC(__type) @CVC4_TLS@ CVC4_PUBLIC __type
+#  define CVC4_THREADLOCAL(__type...) @CVC4_TLS@ __type
+#  define CVC4_THREADLOCAL_PUBLIC(__type...) @CVC4_TLS@ CVC4_PUBLIC __type
 #else
 #  include <pthread.h>
-#  define CVC4_THREADLOCAL(__type) ::CVC4::ThreadLocal< __type >
-#  define CVC4_THREADLOCAL_PUBLIC(__type) CVC4_PUBLIC ::CVC4::ThreadLocal< __type >
+#  define CVC4_THREADLOCAL(__type...) ::CVC4::ThreadLocal< __type >
+#  define CVC4_THREADLOCAL_PUBLIC(__type...) CVC4_PUBLIC ::CVC4::ThreadLocal< __type >
 
 namespace CVC4 {
 
@@ -76,6 +80,49 @@ public:
 };/* class ThreadLocalImpl<T, true> */
 
 template <class T>
+class ThreadLocalImpl<T*, true> {
+  pthread_key_t d_key;
+
+  static void cleanup(void*) {
+  }
+
+public:
+  ThreadLocalImpl() {
+    pthread_key_create(&d_key, ThreadLocalImpl::cleanup);
+  }
+
+  ThreadLocalImpl(const T* t) {
+    pthread_key_create(&d_key, ThreadLocalImpl::cleanup);
+    pthread_setspecific(d_key, const_cast<void*>(reinterpret_cast<const void*>(t)));
+  }
+
+  ThreadLocalImpl(const ThreadLocalImpl& tl) {
+    pthread_key_create(&d_key, ThreadLocalImpl::cleanup);
+    pthread_setspecific(d_key, const_cast<void*>(reinterpret_cast<const void*>(static_cast<const T*>(tl))));
+  }
+
+  ThreadLocalImpl& operator=(const T* t) {
+    pthread_setspecific(d_key, const_cast<void*>(reinterpret_cast<const void*>(t)));
+    return *this;
+  }
+  ThreadLocalImpl& operator=(const ThreadLocalImpl& tl) {
+    pthread_setspecific(d_key, const_cast<void*>(reinterpret_cast<const void*>(static_cast<const T*>(tl))));
+    return *this;
+  }
+
+  operator T*() const {
+    return static_cast<T*>(pthread_getspecific(d_key));
+  }
+
+  T operator*() {
+    return *static_cast<T*>(pthread_getspecific(d_key));
+  }
+  T* operator->() {
+    return static_cast<T*>(pthread_getspecific(d_key));
+  }
+};/* class ThreadLocalImpl<T*, true> */
+
+template <class T>
 class ThreadLocalImpl<T, false> {
 };/* class ThreadLocalImpl<T, false> */