summaryrefslogtreecommitdiff
path: root/src/theory/arith
diff options
context:
space:
mode:
authorAndres Noetzli <andres.noetzli@gmail.com>2018-08-07 23:24:07 -0700
committerGitHub <noreply@github.com>2018-08-07 23:24:07 -0700
commit047e75b485ad16a729083c210ba4064943d2e7c5 (patch)
treecbd0ac11a061cb6da426e44bd6684f6115fecc88 /src/theory/arith
parent95e9918607ed879347bb250ecbaa3c5c557d71b4 (diff)
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
Diffstat (limited to 'src/theory/arith')
-rw-r--r--src/theory/arith/dual_simplex.cpp3
-rw-r--r--src/theory/arith/fc_simplex.cpp3
-rw-r--r--src/theory/arith/soi_simplex.cpp3
-rw-r--r--src/theory/arith/theory_arith_private.cpp3
4 files changed, 4 insertions, 8 deletions
diff --git a/src/theory/arith/dual_simplex.cpp b/src/theory/arith/dual_simplex.cpp
index 1f855b1dd..c2b95890a 100644
--- 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 198c22e77..07c6b1691 100644
--- 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 43ea51384..31301df61 100644
--- 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 ad0ce2e86..6db246b8b 100644
--- 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;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback