diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2017-08-30 20:55:27 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2017-08-30 20:55:27 -0700 |
commit | 546d795470ca7c30fc62fe9b6c7b8e5838e1eed4 (patch) | |
tree | 443f7101c4246b684ce21a04704d769eb2db15ad /src | |
parent | d7dadde871ae4775748695b0b7f9deee49576c0a (diff) |
Use thread_local instead of compiler extensions (#210)
C++11 introduced the thread_local keyword, so we don't need to use
non-standard extensions or our custom pthread extension anymore.
The behavior was previously introduced as a workaround in commit
753a072c542c1c254d7c6adbf10e091ba585ede5. This commit
introduces the macro CVC4_THREAD_LOCAL that can be used to
declare variables as thread local. For Swig, this macro is defined to
be empty.
Diffstat (limited to 'src')
-rw-r--r-- | src/Makefile.am | 2 | ||||
-rw-r--r-- | src/base/Makefile.am | 16 | ||||
-rw-r--r-- | src/base/cvc4_assert.cpp | 5 | ||||
-rw-r--r-- | src/base/cvc4_assert.h | 1 | ||||
-rw-r--r-- | src/base/exception.cpp | 2 | ||||
-rw-r--r-- | src/base/exception.h | 2 | ||||
-rw-r--r-- | src/base/tls.h | 31 | ||||
-rw-r--r-- | src/base/tls.h.in | 198 | ||||
-rw-r--r-- | src/bindings/swig.h | 10 | ||||
-rw-r--r-- | src/expr/node_manager.cpp | 3 | ||||
-rw-r--r-- | src/expr/node_manager.h | 2 | ||||
-rw-r--r-- | src/main/driver_unified.cpp | 3 | ||||
-rw-r--r-- | src/main/main.h | 4 | ||||
-rw-r--r-- | src/main/util.cpp | 1 | ||||
-rw-r--r-- | src/options/options.h | 4 | ||||
-rw-r--r-- | src/options/options_public_functions.cpp | 1 | ||||
-rw-r--r-- | src/options/options_template.cpp | 8 | ||||
-rw-r--r-- | src/smt/smt_engine_scope.cpp | 3 | ||||
-rw-r--r-- | src/smt_util/node_visitor.h | 7 | ||||
-rw-r--r-- | src/theory/arith/dual_simplex.cpp | 3 | ||||
-rw-r--r-- | src/theory/arith/fc_simplex.cpp | 3 | ||||
-rw-r--r-- | src/theory/arith/soi_simplex.cpp | 3 | ||||
-rw-r--r-- | src/theory/arith/theory_arith_private.cpp | 5 | ||||
-rw-r--r-- | src/theory/rewriter.cpp | 2 |
24 files changed, 70 insertions, 249 deletions
diff --git a/src/Makefile.am b/src/Makefile.am index 916733016..974f599e4 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -620,7 +620,6 @@ install-data-local: (echo include/cvc4.h; \ echo include/cvc4_public.h; \ echo include/cvc4parser_public.h; \ - echo base/tls.h; \ echo util/integer.h; \ echo util/rational.h; \ find * -name '*.h' | \ @@ -653,7 +652,6 @@ uninstall-local: -(echo include/cvc4.h; \ echo include/cvc4_public.h; \ echo include/cvc4parser_public.h; \ - echo base/tls.h; \ echo util/integer.h; \ echo util/rational.h; \ find * -name '*.h' | \ diff --git a/src/base/Makefile.am b/src/base/Makefile.am index 491baaa90..5537bbbdd 100644 --- a/src/base/Makefile.am +++ b/src/base/Makefile.am @@ -5,7 +5,7 @@ AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN) noinst_LTLIBRARIES = libbase.la -# Do not list built sources (like tls.h) here! +# Do not list built sources here! # Rather, list them under BUILT_SOURCES, and their .in versions under # EXTRA_DIST. Otherwise, they're packaged up in the tarball, which is # no good---they belong in the configured builds/ directory. If they @@ -26,17 +26,14 @@ libbase_la_SOURCES = \ listener.h \ modal_exception.h \ output.cpp \ - output.h - - -BUILT_SOURCES = \ + output.h \ tls.h # listing {Debug,Trace}_tags too ensures that make doesn't auto-remove it # after building (if it does, we don't get the "cached" effect with # the .tmp files below, and we have to re-compile and re-link each # time, even when there are no changes). -BUILT_SOURCES += \ +BUILT_SOURCES = \ Debug_tags.h \ Debug_tags \ Trace_tags.h \ @@ -55,12 +52,7 @@ EXTRA_DIST = \ exception.i \ mktagheaders \ mktags \ - modal_exception.i \ - tls.h.in - -DISTCLEANFILES = \ - tls.h.tmp \ - tls.h + modal_exception.i %_tags.h: %_tags mktagheaders $(AM_V_at)chmod +x @srcdir@/mktagheaders diff --git a/src/base/cvc4_assert.cpp b/src/base/cvc4_assert.cpp index c122667f3..f342f5562 100644 --- a/src/base/cvc4_assert.cpp +++ b/src/base/cvc4_assert.cpp @@ -20,13 +20,14 @@ #include "base/cvc4_assert.h" #include "base/output.h" +#include "base/tls.h" using namespace std; namespace CVC4 { #ifdef CVC4_DEBUG -//CVC4_THREADLOCAL(const char*) s_debugLastException = NULL; +//CVC4_THREAD_LOCAL const char* s_debugLastException = NULL; #endif /* CVC4_DEBUG */ @@ -140,7 +141,7 @@ void AssertionException::construct(const char* header, const char* extra, */ void debugAssertionFailed(const AssertionException& thisException, const char* propagatingException) { - static CVC4_THREADLOCAL(bool) alreadyFired = false; + static CVC4_THREAD_LOCAL bool alreadyFired = false; if(__builtin_expect( ( !std::uncaught_exception() ), true ) || alreadyFired) { throw thisException; diff --git a/src/base/cvc4_assert.h b/src/base/cvc4_assert.h index d4942f47c..bb4d57170 100644 --- a/src/base/cvc4_assert.h +++ b/src/base/cvc4_assert.h @@ -26,7 +26,6 @@ #include <string> #include "base/exception.h" -#include "base/tls.h" // output.h not strictly needed for this header, but it _is_ needed to // actually _use_ anything in this header, so let's include it. diff --git a/src/base/exception.cpp b/src/base/exception.cpp index 7df050726..990ae77c6 100644 --- a/src/base/exception.cpp +++ b/src/base/exception.cpp @@ -28,7 +28,7 @@ using namespace std; namespace CVC4 { -CVC4_THREADLOCAL(LastExceptionBuffer*) LastExceptionBuffer::s_currentBuffer = NULL; +CVC4_THREAD_LOCAL LastExceptionBuffer* LastExceptionBuffer::s_currentBuffer = NULL; LastExceptionBuffer::LastExceptionBuffer() : d_contents(NULL) {} diff --git a/src/base/exception.h b/src/base/exception.h index 1ce2ae757..01a054b19 100644 --- a/src/base/exception.h +++ b/src/base/exception.h @@ -160,7 +160,7 @@ private: char* d_contents; - static CVC4_THREADLOCAL(LastExceptionBuffer*) s_currentBuffer; + static CVC4_THREAD_LOCAL LastExceptionBuffer* s_currentBuffer; }; /* class LastExceptionBuffer */ }/* CVC4 namespace */ diff --git a/src/base/tls.h b/src/base/tls.h new file mode 100644 index 000000000..a60b0d8f9 --- /dev/null +++ b/src/base/tls.h @@ -0,0 +1,31 @@ +/********************* */ +/*! \file tls.h + ** \verbatim + ** Top contributors (to current version): + ** Andres Noetzli + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Definiton of CVC4_THREAD_LOCAL + ** + ** This header defines CVC4_THREAD_LOCAL, which should be used instead of + ** thread_local because it is not supported by all build types (e.g. Swig). + **/ + +#include "cvc4_public.h" + +#ifndef __CVC4__BASE__TLS_H +#define __CVC4__BASE__TLS_H + +#if SWIG && (!defined(SWIG_VERSION) || SWIG_VERSION < 0x030000) +// SWIG versions older than 3.0 do not support thread_local, so just redefine +// CVC4_THREAD_LOCAL to be empty for those versions. +#define CVC4_THREAD_LOCAL +#else +#define CVC4_THREAD_LOCAL thread_local +#endif + +#endif /* __CVC4__BASE__TLS_H */ diff --git a/src/base/tls.h.in b/src/base/tls.h.in deleted file mode 100644 index c66aef767..000000000 --- a/src/base/tls.h.in +++ /dev/null @@ -1,198 +0,0 @@ -/********************* */ -/*! \file tls.h.in - ** \verbatim - ** Top contributors (to current version): - ** Morgan Deters, ACSYS, Paul Meng - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Header to define CVC4_THREAD whether or not TLS is - ** supported by the compiler/runtime platform - ** - ** Header to define CVC4_THREAD whether or not TLS is supported by - ** the compiler/runtime platform. If not, an implementation based on - ** pthread_getspecific() / pthread_setspecific() is given. - **/ - -#include "cvc4_public.h" - -#ifndef __CVC4__TLS_H -#define __CVC4__TLS_H - -// 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(__type...) __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(__type...) ::CVC4::ThreadLocal< __type > - -namespace CVC4 { - -template <class T, bool small> -class ThreadLocalImpl; - -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>(reinterpret_cast<size_t>(pthread_getspecific(d_key))); - } -};/* 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> */ - -template <class T> -class ThreadLocal : public ThreadLocalImpl<T, sizeof(T) <= sizeof(void*)> { - typedef ThreadLocalImpl<T, sizeof(T) <= sizeof(void*)> super; - -public: - ThreadLocal() : super() {} - ThreadLocal(const T& t) : super(t) {} - ThreadLocal(const ThreadLocal<T>& tl) : super(tl) {} - - ThreadLocal<T>& operator=(const T& t) { - return static_cast< ThreadLocal<T>& >(super::operator=(t)); - } - ThreadLocal<T>& operator=(const ThreadLocal<T>& tl) { - return static_cast< ThreadLocal<T>& >(super::operator=(tl)); - } -};/* class ThreadLocal<T> */ - -template <class T> -class ThreadLocal<T*> : public ThreadLocalImpl<T*, sizeof(T*) <= sizeof(void*)> { - typedef ThreadLocalImpl<T*, sizeof(T*) <= sizeof(void*)> super; - -public: - ThreadLocal() : super() {} - ThreadLocal(T* t) : super(t) {} - ThreadLocal(const ThreadLocal<T*>& tl) : super(tl) {} - - ThreadLocal<T*>& operator=(T* t) { - return static_cast< ThreadLocal<T*>& >(super::operator=(t)); - } - ThreadLocal<T*>& operator=(const ThreadLocal<T*>& tl) { - return static_cast< ThreadLocal<T*>& >(super::operator=(tl)); - } - // special operators for pointers - T& operator*() { - return *static_cast<T*>(*this); - } - const T& operator*() const { - return *static_cast<const T*>(*this); - } - T* operator->() { - return static_cast<T*>(*this); - } - const T* operator->() const { - return static_cast<const T*>(*this); - } - T* operator++() { - T* p = *this; - *this = ++p; - return p; - } - T* operator++(int) { - T* p = *this; - *this = p + 1; - return p; - } - T* operator--() { - T* p = *this; - *this = --p; - return p; - } - T* operator--(int) { - T* p = *this; - *this = p - 1; - return p; - } -};/* class ThreadLocal<T*> */ - -}/* CVC4 namespace */ - -#endif /* @CVC4_TLS_SUPPORTED@ */ - -#endif /* __CVC4__TLS_H */ diff --git a/src/bindings/swig.h b/src/bindings/swig.h index f73ddd9bb..053cb7172 100644 --- a/src/bindings/swig.h +++ b/src/bindings/swig.h @@ -26,15 +26,9 @@ #endif /* SWIG_VERSION */ %import "cvc4_public.h" -#warning "Working around a SWIG segfault in C++ template parsing." -//%import "base/tls.h" -#define CVC4_THREADLOCAL(__type...) __type -#define CVC4_THREADLOCAL_PUBLIC(__type...) CVC4_PUBLIC __type -#define CVC4_THREADLOCAL_TYPE(__type...) __type +%import "base/tls.h" -// swig doesn't like the __thread storage class... -#define __thread -// ...or GCC attributes +// swig doesn't like GCC attributes #define __attribute__(x) #endif /* __CVC4__BINDINGS__SWIG_H */ diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index e440261cb..33f057274 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -23,7 +23,6 @@ #include "base/cvc4_assert.h" #include "base/listener.h" -#include "base/tls.h" #include "expr/attribute.h" #include "expr/node_manager_attributes.h" #include "expr/node_manager_listeners.h" @@ -38,7 +37,7 @@ using namespace CVC4::expr; namespace CVC4 { -CVC4_THREADLOCAL(NodeManager*) NodeManager::s_current = NULL; +CVC4_THREAD_LOCAL NodeManager* NodeManager::s_current = NULL; namespace { diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index fab5d4688..b1b0bc974 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -101,7 +101,7 @@ class NodeManager { expr::NodeValueIDHashFunction, expr::NodeValueIDEquality> NodeValueIDSet; - static CVC4_THREADLOCAL(NodeManager*) s_current; + static CVC4_THREAD_LOCAL NodeManager* s_current; Options* d_options; StatisticsRegistry* d_statisticsRegistry; diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp index 2a9202898..cad662d90 100644 --- a/src/main/driver_unified.cpp +++ b/src/main/driver_unified.cpp @@ -26,6 +26,7 @@ // This must come before PORTFOLIO_BUILD. #include "cvc4autoconfig.h" +#include "base/tls.h" #include "base/configuration.h" #include "base/output.h" #include "expr/expr_iomanip.h" @@ -55,7 +56,7 @@ using namespace CVC4::main; namespace CVC4 { namespace main { /** Global options variable */ - CVC4_THREADLOCAL(Options*) pOptions; + CVC4_THREAD_LOCAL Options* pOptions; /** Full argv[0] */ const char *progPath; diff --git a/src/main/main.h b/src/main/main.h index dcb5c2a0a..8a5d0971e 100644 --- a/src/main/main.h +++ b/src/main/main.h @@ -17,8 +17,8 @@ #include <exception> #include <string> -#include "base/exception.h" #include "base/tls.h" +#include "base/exception.h" #include "cvc4autoconfig.h" #include "expr/expr_manager.h" #include "options/options.h" @@ -54,7 +54,7 @@ extern CVC4::TimerStat* pTotalTime; extern bool segvSpin; /** A pointer to the options in play */ -extern CVC4_THREADLOCAL(Options*) pOptions; +extern CVC4_THREAD_LOCAL Options* pOptions; /** Initialize the driver. Sets signal handlers for SIGINT and SIGSEGV. */ void cvc4_init() throw(Exception); diff --git a/src/main/util.cpp b/src/main/util.cpp index e08628848..110fc2c67 100644 --- a/src/main/util.cpp +++ b/src/main/util.cpp @@ -33,7 +33,6 @@ #endif /* __WIN32__ */ #include "base/exception.h" -#include "base/tls.h" #include "cvc4autoconfig.h" #include "main/command_executor.h" #include "main/main.h" diff --git a/src/options/options.h b/src/options/options.h index 6b2bfedad..f93663095 100644 --- a/src/options/options.h +++ b/src/options/options.h @@ -29,8 +29,8 @@ #include "base/tls.h" #include "options/argument_extender.h" #include "options/language.h" -#include "options/printer_modes.h" #include "options/option_exception.h" +#include "options/printer_modes.h" namespace CVC4 { @@ -47,7 +47,7 @@ class CVC4_PUBLIC Options { options::OptionsHandler* d_handler; /** The current Options in effect */ - static CVC4_THREADLOCAL(Options*) s_current; + static CVC4_THREAD_LOCAL Options* s_current; /** Listeners for options::forceLogicString being set. */ ListenerCollection d_forceLogicListeners; diff --git a/src/options/options_public_functions.cpp b/src/options/options_public_functions.cpp index 54fbd3c81..7d71c267a 100644 --- a/src/options/options_public_functions.cpp +++ b/src/options/options_public_functions.cpp @@ -25,7 +25,6 @@ #include "base/listener.h" #include "base/modal_exception.h" -#include "base/tls.h" #include "options/base_options.h" #include "options/language.h" #include "options/main_options.h" diff --git a/src/options/options_template.cpp b/src/options/options_template.cpp index bc97e6028..a48b22625 100644 --- a/src/options/options_template.cpp +++ b/src/options/options_template.cpp @@ -48,10 +48,10 @@ extern int optreset; #include <sstream> #include <limits> +#include "base/tls.h" #include "base/cvc4_assert.h" #include "base/exception.h" #include "base/output.h" -#include "base/tls.h" #include "options/argument_extender.h" #include "options/argument_extender_implementation.h" #include "options/didyoumean.h" @@ -75,7 +75,7 @@ using namespace CVC4::options; namespace CVC4 { -CVC4_THREADLOCAL(Options*) Options::s_current = NULL; +CVC4_THREAD_LOCAL Options* Options::s_current = NULL; @@ -532,10 +532,10 @@ namespace options { /** Set a given Options* as "current" just for a particular scope. */ class OptionsGuard { - CVC4_THREADLOCAL_TYPE(Options*)* d_field; + Options** d_field; Options* d_old; public: - OptionsGuard(CVC4_THREADLOCAL_TYPE(Options*)* field, Options* opts) : + OptionsGuard(Options** field, Options* opts) : d_field(field), d_old(*field) { *field = opts; diff --git a/src/smt/smt_engine_scope.cpp b/src/smt/smt_engine_scope.cpp index 6c360cdc9..d5fb87dbc 100644 --- a/src/smt/smt_engine_scope.cpp +++ b/src/smt/smt_engine_scope.cpp @@ -17,6 +17,7 @@ #include "smt/smt_engine_scope.h" +#include "base/tls.h" #include "base/configuration_private.h" #include "base/cvc4_assert.h" #include "base/output.h" @@ -27,7 +28,7 @@ namespace CVC4 { namespace smt { -CVC4_THREADLOCAL(SmtEngine*) s_smtEngine_current = NULL; +CVC4_THREAD_LOCAL SmtEngine* s_smtEngine_current = NULL; SmtEngine* currentSmtEngine() { Assert(s_smtEngine_current != NULL); diff --git a/src/smt_util/node_visitor.h b/src/smt_util/node_visitor.h index 8c02af82d..ffd05c83f 100644 --- a/src/smt_util/node_visitor.h +++ b/src/smt_util/node_visitor.h @@ -20,6 +20,7 @@ #include <vector> +#include "base/tls.h" #include "expr/node.h" namespace CVC4 { @@ -32,7 +33,7 @@ template<typename Visitor> class NodeVisitor { /** For re-entry checking */ - static CVC4_THREADLOCAL(bool) s_inRun; + static CVC4_THREAD_LOCAL bool s_inRun; /** * Guard against NodeVisitor<> being re-entrant. @@ -73,7 +74,7 @@ public: */ static typename Visitor::return_type run(Visitor& visitor, TNode node) { - GuardReentry<CVC4_THREADLOCAL_TYPE(bool)> guard(s_inRun); + GuardReentry<bool> guard(s_inRun); // Notify of a start visitor.start(node); @@ -115,6 +116,6 @@ public: };/* class NodeVisitor<> */ template <typename Visitor> -CVC4_THREADLOCAL(bool) NodeVisitor<Visitor>::s_inRun = false; +CVC4_THREAD_LOCAL bool NodeVisitor<Visitor>::s_inRun = false; }/* CVC4 namespace */ diff --git a/src/theory/arith/dual_simplex.cpp b/src/theory/arith/dual_simplex.cpp index a40db89a7..ccab94221 100644 --- a/src/theory/arith/dual_simplex.cpp +++ b/src/theory/arith/dual_simplex.cpp @@ -17,6 +17,7 @@ #include "theory/arith/dual_simplex.h" #include "base/output.h" +#include "base/tls.h" #include "options/arith_options.h" #include "smt/smt_statistics_registry.h" #include "theory/arith/constraint.h" @@ -62,7 +63,7 @@ DualSimplexDecisionProcedure::Statistics::~Statistics(){ Result::Sat DualSimplexDecisionProcedure::dualFindModel(bool exactResult){ Assert(d_conflictVariables.empty()); - static CVC4_THREADLOCAL(unsigned int) instance = 0; + static CVC4_THREAD_LOCAL unsigned int instance = 0; instance = instance + 1; d_pivots = 0; diff --git a/src/theory/arith/fc_simplex.cpp b/src/theory/arith/fc_simplex.cpp index 59bb35293..db40f3580 100644 --- a/src/theory/arith/fc_simplex.cpp +++ b/src/theory/arith/fc_simplex.cpp @@ -17,6 +17,7 @@ #include "theory/arith/fc_simplex.h" #include "base/output.h" +#include "base/tls.h" #include "options/arith_options.h" #include "smt/smt_statistics_registry.h" #include "theory/arith/constraint.h" @@ -91,7 +92,7 @@ Result::Sat FCSimplexDecisionProcedure::findModel(bool exactResult){ Assert(d_sgnDisagreements.empty()); d_pivots = 0; - static CVC4_THREADLOCAL(unsigned int) instance = 0; + static CVC4_THREAD_LOCAL unsigned int instance = 0; instance = instance + 1; static const bool verbose = false; diff --git a/src/theory/arith/soi_simplex.cpp b/src/theory/arith/soi_simplex.cpp index b2f7b08b5..60c7ed56f 100644 --- a/src/theory/arith/soi_simplex.cpp +++ b/src/theory/arith/soi_simplex.cpp @@ -19,6 +19,7 @@ #include <algorithm> #include "base/output.h" +#include "base/tls.h" #include "options/arith_options.h" #include "smt/smt_statistics_registry.h" #include "theory/arith/constraint.h" @@ -103,7 +104,7 @@ Result::Sat SumOfInfeasibilitiesSPD::findModel(bool exactResult){ Assert(d_sgnDisagreements.empty()); d_pivots = 0; - static CVC4_THREADLOCAL(unsigned int) instance = 0; + static CVC4_THREAD_LOCAL unsigned int instance = 0; instance = instance + 1; static const bool verbose = false; diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index ab5a19858..a3e2d8ee4 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -24,6 +24,7 @@ #include <vector> #include "base/output.h" +#include "base/tls.h" #include "context/cdhashset.h" #include "context/cdinsert_hashmap.h" #include "context/cdlist.h" @@ -56,12 +57,12 @@ #include "theory/arith/linear_equality.h" #include "theory/arith/matrix.h" #include "theory/arith/matrix.h" +#include "theory/arith/nonlinear_extension.h" #include "theory/arith/normal_form.h" #include "theory/arith/partial_model.h" #include "theory/arith/partial_model.h" #include "theory/arith/simplex.h" #include "theory/arith/theory_arith.h" -#include "theory/arith/nonlinear_extension.h" #include "theory/ite_utilities.h" #include "theory/quantifiers/bounded_integers.h" #include "theory/rewriter.h" @@ -4389,7 +4390,7 @@ void TheoryArithPrivate::presolve(){ if(Debug.isOn("paranoid:check_tableau")){ d_linEq.debugCheckTableau(); } - static CVC4_THREADLOCAL(unsigned) callCount = 0; + static CVC4_THREAD_LOCAL unsigned callCount = 0; if(Debug.isOn("arith::presolve")) { Debug("arith::presolve") << "TheoryArithPrivate::presolve #" << callCount << endl; callCount = callCount + 1; diff --git a/src/theory/rewriter.cpp b/src/theory/rewriter.cpp index 0c20c48a4..fe58f658d 100644 --- a/src/theory/rewriter.cpp +++ b/src/theory/rewriter.cpp @@ -35,7 +35,7 @@ static TheoryId theoryOf(TNode node) { } #ifdef CVC4_ASSERTIONS -static CVC4_THREADLOCAL(std::unordered_set<Node, NodeHashFunction>*) s_rewriteStack = NULL; +static CVC4_THREAD_LOCAL std::unordered_set<Node, NodeHashFunction>* s_rewriteStack = NULL; #endif /* CVC4_ASSERTIONS */ class RewriterInitializer { |