cvc4-1.3
tls.h
Go to the documentation of this file.
1 /********************* */
20 #include "cvc4_public.h"
21 
22 #ifndef __CVC4__TLS_H
23 #define __CVC4__TLS_H
24 
25 // A bit obnoxious: we have to take varargs to support multi-argument
26 // template types in the threadlocals.
27 // E.g. "CVC4_THREADLOCAL(hash_set<type, hasher>*)" fails otherwise,
28 // due to the embedded comma.
29 #if 1
30 # define CVC4_THREADLOCAL(__type...) __thread __type
31 # define CVC4_THREADLOCAL_PUBLIC(__type...) __thread CVC4_PUBLIC __type
32 # define CVC4_THREADLOCAL_TYPE(__type...) __type
33 #else
34 # include <pthread.h>
35 # define CVC4_THREADLOCAL(__type...) ::CVC4::ThreadLocal< __type >
36 # define CVC4_THREADLOCAL_PUBLIC(__type...) CVC4_PUBLIC ::CVC4::ThreadLocal< __type >
37 # define CVC4_THREADLOCAL_TYPE(__type...) ::CVC4::ThreadLocal< __type >
38 
39 namespace CVC4 {
40 
41 template <class T, bool small>
42 class ThreadLocalImpl;
43 
44 template <class T>
45 class ThreadLocalImpl<T, true> {
46  pthread_key_t d_key;
47 
48  static void cleanup(void*) {
49  }
50 
51 public:
52  ThreadLocalImpl() {
53  pthread_key_create(&d_key, ThreadLocalImpl::cleanup);
54  }
55 
56  ThreadLocalImpl(const T& t) {
57  pthread_key_create(&d_key, ThreadLocalImpl::cleanup);
58  pthread_setspecific(d_key, const_cast<void*>(reinterpret_cast<const void*>(t)));
59  }
60 
61  ThreadLocalImpl(const ThreadLocalImpl& tl) {
62  pthread_key_create(&d_key, ThreadLocalImpl::cleanup);
63  pthread_setspecific(d_key, const_cast<void*>(reinterpret_cast<const void*>(static_cast<const T&>(tl))));
64  }
65 
66  ThreadLocalImpl& operator=(const T& t) {
67  pthread_setspecific(d_key, const_cast<void*>(reinterpret_cast<const void*>(t)));
68  return *this;
69  }
70  ThreadLocalImpl& operator=(const ThreadLocalImpl& tl) {
71  pthread_setspecific(d_key, const_cast<void*>(reinterpret_cast<const void*>(static_cast<const T&>(tl))));
72  return *this;
73  }
74 
75  operator T() const {
76  return static_cast<T>(reinterpret_cast<size_t>(pthread_getspecific(d_key)));
77  }
78 };/* class ThreadLocalImpl<T, true> */
79 
80 template <class T>
81 class ThreadLocalImpl<T*, true> {
82  pthread_key_t d_key;
83 
84  static void cleanup(void*) {
85  }
86 
87 public:
88  ThreadLocalImpl() {
89  pthread_key_create(&d_key, ThreadLocalImpl::cleanup);
90  }
91 
92  ThreadLocalImpl(const T* t) {
93  pthread_key_create(&d_key, ThreadLocalImpl::cleanup);
94  pthread_setspecific(d_key, const_cast<void*>(reinterpret_cast<const void*>(t)));
95  }
96 
97  ThreadLocalImpl(const ThreadLocalImpl& tl) {
98  pthread_key_create(&d_key, ThreadLocalImpl::cleanup);
99  pthread_setspecific(d_key, const_cast<void*>(reinterpret_cast<const void*>(static_cast<const T*>(tl))));
100  }
101 
102  ThreadLocalImpl& operator=(const T* t) {
103  pthread_setspecific(d_key, const_cast<void*>(reinterpret_cast<const void*>(t)));
104  return *this;
105  }
106  ThreadLocalImpl& operator=(const ThreadLocalImpl& tl) {
107  pthread_setspecific(d_key, const_cast<void*>(reinterpret_cast<const void*>(static_cast<const T*>(tl))));
108  return *this;
109  }
110 
111  operator T*() const {
112  return static_cast<T*>(pthread_getspecific(d_key));
113  }
114 
115  T operator*() {
116  return *static_cast<T*>(pthread_getspecific(d_key));
117  }
118  T* operator->() {
119  return static_cast<T*>(pthread_getspecific(d_key));
120  }
121 };/* class ThreadLocalImpl<T*, true> */
122 
123 template <class T>
124 class ThreadLocalImpl<T, false> {
125 };/* class ThreadLocalImpl<T, false> */
126 
127 template <class T>
128 class ThreadLocal : public ThreadLocalImpl<T, sizeof(T) <= sizeof(void*)> {
129  typedef ThreadLocalImpl<T, sizeof(T) <= sizeof(void*)> super;
130 
131 public:
132  ThreadLocal() : super() {}
133  ThreadLocal(const T& t) : super(t) {}
134  ThreadLocal(const ThreadLocal<T>& tl) : super(tl) {}
135 
136  ThreadLocal<T>& operator=(const T& t) {
137  return static_cast< ThreadLocal<T>& >(super::operator=(t));
138  }
139  ThreadLocal<T>& operator=(const ThreadLocal<T>& tl) {
140  return static_cast< ThreadLocal<T>& >(super::operator=(tl));
141  }
142 };/* class ThreadLocal<T> */
143 
144 template <class T>
145 class ThreadLocal<T*> : public ThreadLocalImpl<T*, sizeof(T*) <= sizeof(void*)> {
146  typedef ThreadLocalImpl<T*, sizeof(T*) <= sizeof(void*)> super;
147 
148 public:
149  ThreadLocal() : super() {}
150  ThreadLocal(T* t) : super(t) {}
151  ThreadLocal(const ThreadLocal<T*>& tl) : super(tl) {}
152 
153  ThreadLocal<T*>& operator=(T* t) {
154  return static_cast< ThreadLocal<T*>& >(super::operator=(t));
155  }
156  ThreadLocal<T*>& operator=(const ThreadLocal<T*>& tl) {
157  return static_cast< ThreadLocal<T*>& >(super::operator=(tl));
158  }
159  // special operators for pointers
160  T& operator*() {
161  return *static_cast<T*>(*this);
162  }
163  const T& operator*() const {
164  return *static_cast<const T*>(*this);
165  }
166  T* operator->() {
167  return static_cast<T*>(*this);
168  }
169  const T* operator->() const {
170  return static_cast<const T*>(*this);
171  }
172  T* operator++() {
173  T* p = *this;
174  *this = ++p;
175  return p;
176  }
177  T* operator++(int) {
178  T* p = *this;
179  *this = p + 1;
180  return p;
181  }
182  T* operator--() {
183  T* p = *this;
184  *this = --p;
185  return p;
186  }
187  T* operator--(int) {
188  T* p = *this;
189  *this = p - 1;
190  return p;
191  }
192 };/* class ThreadLocal<T*> */
193 
194 }/* CVC4 namespace */
195 
196 #endif /* 1 */
197 
198 #endif /* __CVC4__TLS_H */
This is CVC4 release version For build and installation please see the INSTALL file included with this distribution This first official release of CVC4 is the result of more than three years of efforts by researchers at New York University and The University of Iowa The project leaders are Clark please refer to the AUTHORS file in the source distribution CVC4 is a tool for determining the satisfiability of a first order formula modulo a first order CVC CVC3 but does not directly incorporate code from any previous version CVC4 is intended to be an open and extensible SMT engine It can be used as a stand alone tool or as a library It has been designed to increase the performance and reduce the memory overhead of its predecessors It is written entirely in C and is released under a free software see the INSTALL file that comes with this distribution We recommend that you visit our CVC4 tutorials online please write to the cvc users cs nyu edu mailing list *if you need to report a bug with CVC4
Definition: README:39
Macros that should be defined everywhere during the building of the libraries and driver binary...