Require Swig 3 (#2283)

Removes some hacks due to Swig 2's incomplete C++11 support and adds
checks for version 3 at configuration time as well as in swig.h

diff --git a/config/bindings.m4 b/config/bindings.m4
index 5941d81cdbf9babe536727f1fc200a72cc88f2d4..bc7c0e2b85622f70cafd7b87dfd4f6e6fb845c38 100644 (file)
--- a/config/bindings.m4
+++ b/config/bindings.m4
@@ -58,7 +58,7 @@ else
     AC_MSG_CHECKING([compatibility with version of swig])
     cat > conftest.c << _CVC4EOF
 %module conftest
-#if !defined(SWIG_VERSION) || SWIG_VERSION < 0x020000
+#if !defined(SWIG_VERSION) || SWIG_VERSION < 0x030000
 #error bad version
 #endif
 _CVC4EOF
@@ -66,7 +66,7 @@ _CVC4EOF
       AC_MSG_RESULT([compatible version])
     else
       AC_MSG_RESULT([incompatible version])
-      AC_MSG_WARN([swig version 2.0.0 or later is required to build native API bindings])
+      AC_MSG_WARN([swig version 3.0.0 or later is required to build native API bindings])
       SWIG=
       echo '===Failed swig input was:' >&AS_MESSAGE_LOG_FD
       cat conftest.c >&AS_MESSAGE_LOG_FD

diff --git a/src/base/Makefile.am b/src/base/Makefile.am
index 7dd6f47e5c5c6a0d03850166b66a85f86066cdfc..3619b226e53e682e8ad7ca1a3686bf13b1765188 100644 (file)
--- a/src/base/Makefile.am
+++ b/src/base/Makefile.am
@@ -28,8 +28,7 @@ libbase_la_SOURCES = \
        listener.h \
        modal_exception.h \
        output.cpp \
-       output.h \
-       tls.h
+       output.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

diff --git a/src/base/cvc4_assert.cpp b/src/base/cvc4_assert.cpp
index 1e92670b4fbfc13a35d22525300cf8c25ae86ff3..3af6a9909ec5b6ac29fdd6a70d2e4c4f727c46fb 100644 (file)
--- a/src/base/cvc4_assert.cpp
+++ b/src/base/cvc4_assert.cpp
@@ -20,14 +20,13 @@
 
 #include "base/cvc4_assert.h"
 #include "base/output.h"
-#include "base/tls.h"
 
 using namespace std;
 
 namespace CVC4 {
 
 #ifdef CVC4_DEBUG
-//CVC4_THREAD_LOCAL const char* s_debugLastException = NULL;
+//thread_local const char* s_debugLastException = NULL;
 #endif /* CVC4_DEBUG */
 
 
@@ -141,7 +140,7 @@ void AssertionException::construct(const char* header, const char* extra,
  */
 void debugAssertionFailed(const AssertionException& thisException,
                           const char* propagatingException) {
-  static CVC4_THREAD_LOCAL bool alreadyFired = false;
+  static thread_local bool alreadyFired = false;
 
   if(__builtin_expect( ( !std::uncaught_exception() ), true ) || alreadyFired) {
     throw thisException;

diff --git a/src/base/exception.cpp b/src/base/exception.cpp
index 0a651f773d04aecc304b2d640f676062d12dbf3f..831220a2b55ed1604d00fb17d1222bdfa36a5539 100644 (file)
--- a/src/base/exception.cpp
+++ b/src/base/exception.cpp
@@ -28,7 +28,7 @@ using namespace std;
 
 namespace CVC4 {
 
-CVC4_THREAD_LOCAL LastExceptionBuffer* LastExceptionBuffer::s_currentBuffer = NULL;
+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 983a5957215f9d0af63171f1e6e8154b0d5a47ef..54f6aa92df115eb6b741e35d0a93066522f90ccd 100644 (file)
--- a/src/base/exception.h
+++ b/src/base/exception.h
@@ -27,8 +27,6 @@
 #include <stdexcept>
 #include <string>
 
-#include "base/tls.h"
-
 namespace CVC4 {
 
 class CVC4_PUBLIC Exception : public std::exception {
@@ -163,7 +161,7 @@ private:
 
   char* d_contents;
 
-  static CVC4_THREAD_LOCAL LastExceptionBuffer* s_currentBuffer;
+  static thread_local LastExceptionBuffer* s_currentBuffer;
 }; /* class LastExceptionBuffer */
 
 }/* CVC4 namespace */

diff --git a/src/base/tls.h b/src/base/tls.h
deleted file mode 100644 (file)
index d80d66d..0000000
--- a/src/base/tls.h
+++ /dev/null
@@ -1,31 +0,0 @@
-/*********************                                                        */
-/*! \file tls.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Andres Noetzli
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 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/bindings/swig.h b/src/bindings/swig.h
index 76a64a75f14e3f3835fdafb6bdfa5023cf5e7c3a..5316eef12d607ac70bc88590f789c0f82e14fa5b 100644 (file)
--- a/src/bindings/swig.h
+++ b/src/bindings/swig.h
@@ -21,12 +21,11 @@
 #  error This file should only be included when generating swig interfaces.
 #endif /* SWIG */
 
-#if !defined(SWIG_VERSION) || SWIG_VERSION < 0x020000
-#  error CVC4 bindings require swig version 2.0.0 or later, sorry.
+#if !defined(SWIG_VERSION) || SWIG_VERSION < 0x030000
+#  error CVC4 bindings require swig version 3.0.0 or later, sorry.
 #endif /* SWIG_VERSION */
 
 %import "cvc4_public.h"
-%import "base/tls.h"
 
 // swig doesn't like GCC attributes
 #define __attribute__(x)

diff --git a/src/cvc4.i b/src/cvc4.i
index bc5f5fdfec4924fc55c812cb4b36f3eadf9e5878..c0112c9b0e753c3bf3db5a8fd67999781c25ccb5 100644 (file)
--- a/src/cvc4.i
+++ b/src/cvc4.i
@@ -1,11 +1,3 @@
-// We safely ignore some C++11 keywords that older versions of SWIG cannot
-// handle.
-#if SWIG_VERSION < 0x030000
-%define final %enddef
-%define override %enddef
-%define noexcept %enddef
-#endif
-
 %import "bindings/swig.h"
 
 %include "stdint.i"

diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index 74701cf11b2b79ae4b0eba78ed647385607c9003..a40d1511bc01599f9243b2d2eff18ae67c5858fa 100644 (file)
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -37,7 +37,7 @@ using namespace CVC4::expr;
 
 namespace CVC4 {
 
-CVC4_THREAD_LOCAL NodeManager* NodeManager::s_current = NULL;
+thread_local NodeManager* NodeManager::s_current = NULL;
 
 namespace {
 

diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index f7f3fb1449cb4efd57549be69d01fe26df2f5e2a..8bbf905a969e3b39cc0511c4010ada78c773c2b6 100644 (file)
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -32,7 +32,6 @@
 #include <string>
 #include <unordered_set>
 
-#include "base/tls.h"
 #include "expr/kind.h"
 #include "expr/metakind.h"
 #include "expr/node_value.h"
@@ -101,7 +100,7 @@ class NodeManager {
                              expr::NodeValueIDHashFunction,
                              expr::NodeValueIDEquality> NodeValueIDSet;
 
-  static CVC4_THREAD_LOCAL NodeManager* s_current;
+  static 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 816b40daaa81afcc12c9a46e4144402f81ab4b74..f97b037eb29610ab68583179374f12cb2a698ccb 100644 (file)
--- a/src/main/driver_unified.cpp
+++ b/src/main/driver_unified.cpp
@@ -26,7 +26,6 @@
 // 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"
@@ -56,7 +55,7 @@ using namespace CVC4::main;
 namespace CVC4 {
   namespace main {
     /** Global options variable */
-    CVC4_THREAD_LOCAL Options* pOptions;
+    thread_local Options* pOptions;
 
     /** Full argv[0] */
     const char *progPath;

diff --git a/src/main/interactive_shell.cpp b/src/main/interactive_shell.cpp
index f1220b961c20f873a3a40c1f0fd23e4d03d3012f..2cec42fbf9e2023cbc342d5a5a0174c7824d228b 100644 (file)
--- a/src/main/interactive_shell.cpp
+++ b/src/main/interactive_shell.cpp
@@ -37,7 +37,6 @@
 #  endif /* HAVE_EXT_STDIO_FILEBUF_H */
 #endif /* HAVE_LIBREADLINE */
 
-#include "base/tls.h"
 #include "base/output.h"
 #include "options/language.h"
 #include "options/options.h"
@@ -384,8 +383,8 @@ struct StringPrefix2Less {
 };/* struct StringPrefix2Less */
 
 char* commandGenerator(const char* text, int state) {
-  static CVC4_THREAD_LOCAL const std::string* rlCommand;
-  static CVC4_THREAD_LOCAL set<string>::const_iterator* rlDeclaration;
+  static thread_local const std::string* rlCommand;
+  static thread_local set<string>::const_iterator* rlDeclaration;
 
   const std::string* i = lower_bound(commandsBegin, commandsEnd, text, StringPrefix2Less());
   const std::string* j = upper_bound(commandsBegin, commandsEnd, text, StringPrefix1Less());

diff --git a/src/main/main.h b/src/main/main.h
index 57c00ffc03b3a9a7dfa62ab0a459c93af4bc5846..ee5341b87fb20eea8e6d78e97b0c552bfeca5562 100644 (file)
--- a/src/main/main.h
+++ b/src/main/main.h
@@ -17,7 +17,6 @@
 #include <exception>
 #include <string>
 
-#include "base/tls.h"
 #include "base/exception.h"
 #include "cvc4autoconfig.h"
 #include "expr/expr_manager.h"
@@ -54,7 +53,7 @@ extern CVC4::TimerStat* pTotalTime;
 extern bool segvSpin;
 
 /** A pointer to the options in play */
-extern CVC4_THREAD_LOCAL Options* pOptions;
+extern thread_local Options* pOptions;
 
 /** Initialize the driver.  Sets signal handlers for SIGINT and SIGSEGV.
  * This can throw a CVC4::Exception.

diff --git a/src/options/options.h b/src/options/options.h
index 16210e1a3501439b16a1308d17b63ff3a45a480a..474fe3a4beba86755b5290b25bb890f215116e76 100644 (file)
--- a/src/options/options.h
+++ b/src/options/options.h
@@ -26,7 +26,6 @@
 
 #include "base/listener.h"
 #include "base/modal_exception.h"
-#include "base/tls.h"
 #include "options/argument_extender.h"
 #include "options/language.h"
 #include "options/option_exception.h"
@@ -47,7 +46,7 @@ class CVC4_PUBLIC Options {
   options::OptionsHandler* d_handler;
 
   /** The current Options in effect */
-  static CVC4_THREAD_LOCAL Options* s_current;
+  static thread_local Options* s_current;
 
   /** Listeners for options::forceLogicString being set. */
   ListenerCollection d_forceLogicListeners;

diff --git a/src/options/options_template.cpp b/src/options/options_template.cpp
index d2ccd37ca2bb687e97ce3c3727cc5ce54484c083..609713ce8c2c67ad8aa9d101bba3fe93ecd4a290 100644 (file)
--- a/src/options/options_template.cpp
+++ b/src/options/options_template.cpp
@@ -48,7 +48,6 @@ extern int optreset;
 #include <sstream>
 #include <limits>
 
-#include "base/tls.h"
 #include "base/cvc4_assert.h"
 #include "base/exception.h"
 #include "base/output.h"
@@ -73,7 +72,7 @@ using namespace CVC4::options;
 
 namespace CVC4 {
 
-CVC4_THREAD_LOCAL Options* Options::s_current = NULL;
+thread_local Options* Options::s_current = NULL;
 
 
 

diff --git a/src/smt/smt_engine_scope.cpp b/src/smt/smt_engine_scope.cpp
index 288a07bde832bfd4dfe2d913f7891ac6e13cdec2..a4a0967b2ba791ccc75a33dd08726ead03f04b48 100644 (file)
--- a/src/smt/smt_engine_scope.cpp
+++ b/src/smt/smt_engine_scope.cpp
@@ -17,7 +17,6 @@
 
 #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 +26,7 @@
 namespace CVC4 {
 namespace smt {
 
-CVC4_THREAD_LOCAL SmtEngine* s_smtEngine_current = NULL;
+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 0517e9d2c63dc42a7a6ff1a9759fb47c65a36e23..31a436f818b680fa41e630d00ee7d5899bd3bd6c 100644 (file)
--- a/src/smt_util/node_visitor.h
+++ b/src/smt_util/node_visitor.h
@@ -20,7 +20,6 @@
 
 #include <vector>
 
-#include "base/tls.h"
 #include "expr/node.h"
 
 namespace CVC4 {
@@ -33,7 +32,7 @@ template<typename Visitor>
 class NodeVisitor {
 
   /** For re-entry checking */
-  static CVC4_THREAD_LOCAL bool s_inRun;
+  static thread_local bool s_inRun;
 
   /**
    * Guard against NodeVisitor<> being re-entrant.
@@ -116,6 +115,6 @@ public:
 };/* class NodeVisitor<> */
 
 template <typename Visitor>
-CVC4_THREAD_LOCAL bool NodeVisitor<Visitor>::s_inRun = false;
+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 1f855b1dda999b0244e7350b00183dd0cbf62f4b..c2b95890ad6d7f6b451552d5a5f174cfd972d19f 100644 (file)
--- a/src/theory/arith/dual_simplex.cpp
+++ b/src/theory/arith/dual_simplex.cpp
@@ -17,7 +17,6 @@
 #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"
@@ -63,7 +62,7 @@ DualSimplexDecisionProcedure::Statistics::~Statistics(){
 Result::Sat DualSimplexDecisionProcedure::dualFindModel(bool exactResult){
   Assert(d_conflictVariables.empty());
 
-  static CVC4_THREAD_LOCAL unsigned int instance = 0;
+  static 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 198c22e77da5e12a6d4e4e82d7baf16f651f7ebd..07c6b1691cb954c127e7682cdf9ad02e18f0ee86 100644 (file)
--- a/src/theory/arith/fc_simplex.cpp
+++ b/src/theory/arith/fc_simplex.cpp
@@ -17,7 +17,6 @@
 #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"
@@ -92,7 +91,7 @@ Result::Sat FCSimplexDecisionProcedure::findModel(bool exactResult){
   Assert(d_sgnDisagreements.empty());
 
   d_pivots = 0;
-  static CVC4_THREAD_LOCAL unsigned int instance = 0;
+  static 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 43ea513842d1118da60800e02658538cda2d9bfd..31301df612e951eb8621fcf84f13b74b51d40b91 100644 (file)
--- a/src/theory/arith/soi_simplex.cpp
+++ b/src/theory/arith/soi_simplex.cpp
@@ -19,7 +19,6 @@
 #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"
@@ -104,7 +103,7 @@ Result::Sat SumOfInfeasibilitiesSPD::findModel(bool exactResult){
   Assert(d_sgnDisagreements.empty());
 
   d_pivots = 0;
-  static CVC4_THREAD_LOCAL unsigned int instance = 0;
+  static 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 ad0ce2e8654fe3213cc1060d36feed1eb9b87cd4..6db246b8bbb8eb540c41d5546497b6afd15ef917 100644 (file)
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -24,7 +24,6 @@
 #include <vector>
 
 #include "base/output.h"
-#include "base/tls.h"
 #include "context/cdhashset.h"
 #include "context/cdinsert_hashmap.h"
 #include "context/cdlist.h"
@@ -4400,7 +4399,7 @@ void TheoryArithPrivate::presolve(){
 
   if(Debug.isOn("paranoid:check_tableau")){ d_linEq.debugCheckTableau(); }
 
-  static CVC4_THREAD_LOCAL unsigned callCount = 0;
+  static 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/bv/bitblast/aig_bitblaster.cpp b/src/theory/bv/bitblast/aig_bitblaster.cpp
index f2417deb6a2aa99395d410b6c54d7415a3a57693..b06062cf414b2f36de7a65359f9ac6f19cee68d1 100644 (file)
--- a/src/theory/bv/bitblast/aig_bitblaster.cpp
+++ b/src/theory/bv/bitblast/aig_bitblaster.cpp
@@ -116,7 +116,7 @@ Abc_Obj_t* mkIte<Abc_Obj_t*>(Abc_Obj_t* cond, Abc_Obj_t* a, Abc_Obj_t* b) {
   return Abc_AigMux(AigBitblaster::currentAigM(), cond, a, b); 
 }
 
-CVC4_THREAD_LOCAL Abc_Ntk_t* AigBitblaster::s_abcAigNetwork = nullptr;
+thread_local Abc_Ntk_t* AigBitblaster::s_abcAigNetwork = nullptr;
 
 Abc_Ntk_t* AigBitblaster::currentAigNtk() {
   if (!AigBitblaster::s_abcAigNetwork) {

diff --git a/src/theory/bv/bitblast/aig_bitblaster.h b/src/theory/bv/bitblast/aig_bitblaster.h
index bd624bf92788d66705bf1cb9f747bff212205d15..6d21b69e6036c731a5e74b4206546bd3c2a379f1 100644 (file)
--- a/src/theory/bv/bitblast/aig_bitblaster.h
+++ b/src/theory/bv/bitblast/aig_bitblaster.h
@@ -21,8 +21,6 @@
 
 #include "theory/bv/bitblast/bitblaster.h"
 
-#include "base/tls.h"
-
 class Abc_Obj_t_;
 typedef Abc_Obj_t_ Abc_Obj_t;
 
@@ -57,7 +55,7 @@ class AigBitblaster : public TBitblaster<Abc_Obj_t*>
   typedef std::unordered_map<TNode, Abc_Obj_t*, TNodeHashFunction> TNodeAigMap;
   typedef std::unordered_map<Node, Abc_Obj_t*, NodeHashFunction> NodeAigMap;
 
-  static CVC4_THREAD_LOCAL Abc_Ntk_t* s_abcAigNetwork;
+  static thread_local Abc_Ntk_t* s_abcAigNetwork;
   std::unique_ptr<context::Context> d_nullContext;
   std::unique_ptr<prop::SatSolver> d_satSolver;
   TNodeAigMap d_aigCache;

diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp
index 8b5d34cf4cb87ff047d96c0ad1e2a607d9218258..2c9ccf46aa7730433456c3871498f80fbce88933 100644 (file)
--- a/src/theory/bv/theory_bv_rewriter.cpp
+++ b/src/theory/bv/theory_bv_rewriter.cpp
@@ -30,8 +30,8 @@ using namespace CVC4::theory;
 using namespace CVC4::theory::bv;
 
 
-// CVC4_THREAD_LOCAL AllRewriteRules* TheoryBVRewriter::s_allRules = NULL;
-// CVC4_THREAD_LOCAL TimerStat* TheoryBVRewriter::d_rewriteTimer = NULL;
+// thread_local AllRewriteRules* TheoryBVRewriter::s_allRules = NULL;
+// thread_local TimerStat* TheoryBVRewriter::d_rewriteTimer = NULL;
 RewriteFunction TheoryBVRewriter::d_rewriteTable[kind::LAST_KIND]; 
 void TheoryBVRewriter::init() {
    // s_allRules = new AllRewriteRules;

diff --git a/src/theory/rewriter.cpp b/src/theory/rewriter.cpp
index 6319e11968b6665aec9e83a183271a5d53891968..58f4832c0f9643434f88b6ffecb20fa2e558851c 100644 (file)
--- a/src/theory/rewriter.cpp
+++ b/src/theory/rewriter.cpp
@@ -35,7 +35,7 @@ static TheoryId theoryOf(TNode node) {
 }
 
 #ifdef CVC4_ASSERTIONS
-static CVC4_THREAD_LOCAL std::unordered_set<Node, NodeHashFunction>* s_rewriteStack = NULL;
+static thread_local std::unordered_set<Node, NodeHashFunction>* s_rewriteStack = NULL;
 #endif /* CVC4_ASSERTIONS */
 
 class RewriterInitializer {

diff --git a/src/util/random.h b/src/util/random.h
index 031ef06b7303abd87df1b590e5d2a3864f7fb629..480271c03ec906916d8b15a95be9ee6fb6c86081 100644 (file)
--- a/src/util/random.h
+++ b/src/util/random.h
@@ -21,8 +21,6 @@
 #ifndef __CVC4__UTIL__RANDOM_H
 #define __CVC4__UTIL__RANDOM_H
 
-#include "base/tls.h"
-
 namespace CVC4 {
 
 class Random
@@ -33,7 +31,7 @@ class Random
   /* Get current RNG (singleton).  */
   static Random& getRandom()
   {
-    static CVC4_THREAD_LOCAL Random s_current(0);
+    static thread_local Random s_current(0);
     return s_current;
   }