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.

4 files changed, 9 insertions, 5 deletions

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;