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

26 files changed, 30 insertions, 90 deletions

diff --git a/config/bindings.m4 b/config/bindings.m4
index 5941d81cd..bc7c0e2b8 100644
--- 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 7dd6f47e5..3619b226e 100644
--- 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 1e92670b4..3af6a9909 100644
--- 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 0a651f773..831220a2b 100644
--- 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 983a59572..54f6aa92d 100644
--- 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
index d80d66d30..000000000
--- 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 76a64a75f..5316eef12 100644
--- 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 bc5f5fdfe..c0112c9b0 100644
--- 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 74701cf11..a40d1511b 100644
--- 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 f7f3fb144..8bbf905a9 100644
--- 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 816b40daa..f97b037eb 100644
--- 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 f1220b961..2cec42fbf 100644
--- 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 57c00ffc0..ee5341b87 100644
--- 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 16210e1a3..474fe3a4b 100644
--- 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 d2ccd37ca..609713ce8 100644
--- 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 288a07bde..a4a0967b2 100644
--- 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 0517e9d2c..31a436f81 100644
--- 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 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;
diff --git a/src/theory/bv/bitblast/aig_bitblaster.cpp b/src/theory/bv/bitblast/aig_bitblaster.cpp
index f2417deb6..b06062cf4 100644
--- 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 bd624bf92..6d21b69e6 100644
--- 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 8b5d34cf4..2c9ccf46a 100644
--- 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 6319e1196..58f4832c0 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_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 031ef06b7..480271c03 100644
--- 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;
   }