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/tls.h.in | |
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/tls.h.in')
-rw-r--r-- | src/util/tls.h.in | 55 |
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> */ |