configuration script generated by Autoconf, you may include it under
the same distribution terms that you use for the rest of that program.
-CVC4 incorporates the m4 macro file "ax_tls.m4", excluded from the above
-copyright and downloaded from
-http://www.gnu.org/software/autoconf-archive/ax_tls.html.
-See config/ax_tls.m4. Its copyright:
-
- Copyright (c) 2008 Alan Woodland <ajw05@aber.ac.uk>
- Copyright (c) 2010 Diego Elio Petteno` <flameeyes@gmail.com>
-
- This program is free software: you can redistribute it and/or modify it
- under the terms of the GNU General Public License as published by the
- Free Software Foundation, either version 3 of the License, or (at your
- option) any later version.
-
- This program is distributed in the hope that it will be useful, but
- WITHOUT ANY WARRANTY; without even the implied warranty of
- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General
- Public License for more details.
-
- You should have received a copy of the GNU General Public License along
- with this program. If not, see <http://www.gnu.org/licenses/>.
-
- As a special exception, the respective Autoconf Macro's copyright owner
- gives unlimited permission to copy, distribute and modify the configure
- scripts that are the output of Autoconf when processing the Macro. You
- need not follow the terms of the GNU General Public License when using
- or distributing such scripts, even though portions of the text of the
- Macro appear in them. The GNU General Public License (GPL) does govern
- all other use of the material that constitutes the Autoconf Macro.
-
- This special exception to the GPL applies to versions of the Autoconf
- Macro released by the Autoconf Archive. When you make and distribute a
- modified version of the Autoconf Macro, you may extend this special
- exception to the GPL to apply to your modified version as well.
-
CVC4 incorporates the m4 macro file "boost.m4", excluded from the above
copyright and downloaded from http://github.com/tsuna/boost.m4 .
See config/boost.m4. Its copyright:
+++ /dev/null
-# ===========================================================================
-# http://www.gnu.org/software/autoconf-archive/ax_tls.html
-# ===========================================================================
-#
-# SYNOPSIS
-#
-# AX_TLS([action-if-found], [action-if-not-found])
-#
-# DESCRIPTION
-#
-# Provides a test for the compiler support of thread local storage (TLS)
-# extensions. Defines TLS if it is found. Currently knows about GCC/ICC
-# and MSVC. I think SunPro uses the same as GCC, and Borland apparently
-# supports either.
-#
-# LICENSE
-#
-# Copyright (c) 2008 Alan Woodland <ajw05@aber.ac.uk>
-# Copyright (c) 2010 Diego Elio Petteno` <flameeyes@gmail.com>
-#
-# This program is free software: you can redistribute it and/or modify it
-# under the terms of the GNU General Public License as published by the
-# Free Software Foundation, either version 3 of the License, or (at your
-# option) any later version.
-#
-# This program is distributed in the hope that it will be useful, but
-# WITHOUT ANY WARRANTY; without even the implied warranty of
-# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General
-# Public License for more details.
-#
-# You should have received a copy of the GNU General Public License along
-# with this program. If not, see <http://www.gnu.org/licenses/>.
-#
-# As a special exception, the respective Autoconf Macro's copyright owner
-# gives unlimited permission to copy, distribute and modify the configure
-# scripts that are the output of Autoconf when processing the Macro. You
-# need not follow the terms of the GNU General Public License when using
-# or distributing such scripts, even though portions of the text of the
-# Macro appear in them. The GNU General Public License (GPL) does govern
-# all other use of the material that constitutes the Autoconf Macro.
-#
-# This special exception to the GPL applies to versions of the Autoconf
-# Macro released by the Autoconf Archive. When you make and distribute a
-# modified version of the Autoconf Macro, you may extend this special
-# exception to the GPL to apply to your modified version as well.
-
-#serial 10
-
-AC_DEFUN([AX_TLS], [
- AC_MSG_CHECKING(for thread local storage (TLS) class)
- AC_CACHE_VAL(ac_cv_tls, [
- ax_tls_keywords="__thread __declspec(thread) none"
- for ax_tls_keyword in $ax_tls_keywords; do
- AS_CASE([$ax_tls_keyword],
- [none], [ac_cv_tls=none ; break],
- [AC_TRY_COMPILE(
- [#include <stdlib.h>
- static void
- foo(void) {
- static ] $ax_tls_keyword [ int bar;
- exit(1);
- }],
- [],
- [ac_cv_tls=$ax_tls_keyword ; break],
- ac_cv_tls=none
- )])
- done
- ])
- AC_MSG_RESULT($ac_cv_tls)
-
- AS_IF([test "$ac_cv_tls" != "none"],
- AC_DEFINE_UNQUOTED([TLS], $ac_cv_tls, [If the compiler supports a TLS storage class define it to that here])
- m4_ifnblank([$1], [$1]),
- m4_ifnblank([$2], [$2])
- )
-])
AC_SUBST(CVC4_BUILD_LIBCOMPAT)
AM_CONDITIONAL([CVC4_BUILD_LIBCOMPAT], [test "$CVC4_BUILD_LIBCOMPAT" = yes])
-# Check for availability of TLS support (e.g. __thread storage class)
-AC_MSG_CHECKING([whether to use compiler-supported TLS if available])
-AC_ARG_ENABLE([tls], AS_HELP_STRING([--disable-tls], [don't use compiler-native TLS]))
-if test $cvc4_has_threads = no; then
- # We disable TLS entirely by simply telling the build system that
- # the empty string is the __thread keyword.
- AC_MSG_RESULT([multithreading disabled])
- CVC4_TLS_SUPPORTED=1
- CVC4_TLS=
- CVC4_TLS_explanation='disabled (no multithreading support)'
-else
- if test -z "${enable_tls+set}" || test "$enable_tls" = "yes"; then
- AC_MSG_RESULT([yes])
- AX_TLS([CVC4_TLS=$ac_cv_tls], [CVC4_TLS=])
- else
- AC_MSG_RESULT([no])
- CVC4_TLS=
- fi
- if test -n "$CVC4_TLS"; then
- CVC4_TLS_SUPPORTED=1
- CVC4_TLS_explanation="$CVC4_TLS"
- else
- CVC4_TLS_explanation='pthread_getspecific()'
- CVC4_TLS_SUPPORTED=0
- fi
-fi
-AC_SUBST([CVC4_TLS])
-AC_SUBST([CVC4_TLS_SUPPORTED])
-
# Whether to compile with google profiling tools
cvc4_use_google_perftools=0
AC_ARG_WITH(
fi
fi
-CVC4_CONFIG_FILE_ONLY_IF_CHANGED([src/base/tls.h])
CVC4_CONFIG_FILE_ONLY_IF_CHANGED([src/util/integer.h])
CVC4_CONFIG_FILE_ONLY_IF_CHANGED([src/util/rational.h])
Bindings : $bindings_to_be_built
Multithreaded: $support_multithreaded
-TLS support : $CVC4_TLS_explanation
Portfolio : $with_portfolio
MP library : $mplibrary
(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' | \
-(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' | \
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
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 \
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
#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 */
*/
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;
#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.
namespace CVC4 {
-CVC4_THREADLOCAL(LastExceptionBuffer*) LastExceptionBuffer::s_currentBuffer = NULL;
+CVC4_THREAD_LOCAL LastExceptionBuffer* LastExceptionBuffer::s_currentBuffer = NULL;
LastExceptionBuffer::LastExceptionBuffer() : d_contents(NULL) {}
char* d_contents;
- static CVC4_THREADLOCAL(LastExceptionBuffer*) s_currentBuffer;
+ static CVC4_THREAD_LOCAL LastExceptionBuffer* s_currentBuffer;
}; /* class LastExceptionBuffer */
}/* CVC4 namespace */
--- /dev/null
+/********************* */
+/*! \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 */
+++ /dev/null
-/********************* */
-/*! \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 */
#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 */
#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"
namespace CVC4 {
-CVC4_THREADLOCAL(NodeManager*) NodeManager::s_current = NULL;
+CVC4_THREAD_LOCAL NodeManager* NodeManager::s_current = NULL;
namespace {
expr::NodeValueIDHashFunction,
expr::NodeValueIDEquality> NodeValueIDSet;
- static CVC4_THREADLOCAL(NodeManager*) s_current;
+ static CVC4_THREAD_LOCAL NodeManager* s_current;
Options* d_options;
StatisticsRegistry* d_statisticsRegistry;
// 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"
namespace CVC4 {
namespace main {
/** Global options variable */
- CVC4_THREADLOCAL(Options*) pOptions;
+ CVC4_THREAD_LOCAL Options* pOptions;
/** Full argv[0] */
const char *progPath;
#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"
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);
#endif /* __WIN32__ */
#include "base/exception.h"
-#include "base/tls.h"
#include "cvc4autoconfig.h"
#include "main/command_executor.h"
#include "main/main.h"
#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 {
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;
#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"
#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"
namespace CVC4 {
-CVC4_THREADLOCAL(Options*) Options::s_current = NULL;
+CVC4_THREAD_LOCAL Options* Options::s_current = NULL;
/** 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;
#include "smt/smt_engine_scope.h"
+#include "base/tls.h"
#include "base/configuration_private.h"
#include "base/cvc4_assert.h"
#include "base/output.h"
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);
#include <vector>
+#include "base/tls.h"
#include "expr/node.h"
namespace CVC4 {
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.
*/
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);
};/* class NodeVisitor<> */
template <typename Visitor>
-CVC4_THREADLOCAL(bool) NodeVisitor<Visitor>::s_inRun = false;
+CVC4_THREAD_LOCAL bool NodeVisitor<Visitor>::s_inRun = false;
}/* CVC4 namespace */
#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"
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;
#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"
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;
#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"
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;
#include <vector>
#include "base/output.h"
+#include "base/tls.h"
#include "context/cdhashset.h"
#include "context/cdinsert_hashmap.h"
#include "context/cdlist.h"
#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"
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;
}
#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 {
projects / cvc5.git / commitdiff