some fixes for Mac OS

diff --git a/src/options/options_template.cpp b/src/options/options_template.cpp
index 2df69b5d344ccefcb78124f20746402b4437f2ec..9b9b711ad6c6c628e7b624e758bbbc0e7521f9d2 100644 (file)
--- a/src/options/options_template.cpp
+++ b/src/options/options_template.cpp
@@ -33,10 +33,11 @@
 #include "util/configuration.h"
 #include "util/exception.h"
 #include "util/language.h"
+#include "util/tls.h"
 
 ${include_all_option_headers}
 
-#line 40 "${template}"
+#line 41 "${template}"
 
 #include "util/output.h"
 #include "options/options_holder.h"
@@ -45,7 +46,7 @@ ${include_all_option_headers}
 
 ${option_handler_includes}
 
-#line 49 "${template}"
+#line 50 "${template}"
 
 using namespace CVC4;
 using namespace CVC4::options;
@@ -182,7 +183,7 @@ void runBoolPredicates(T, std::string option, bool b, SmtEngine* smt) {
 
 ${all_custom_handlers}
 
-#line 186 "${template}"
+#line 187 "${template}"
 
 #ifdef CVC4_DEBUG
 #  define USE_EARLY_TYPE_CHECKING_BY_DEFAULT true
@@ -212,18 +213,18 @@ options::OptionsHolder::OptionsHolder() : ${all_modules_defaults}
 {
 }
 
-#line 216 "${template}"
+#line 217 "${template}"
 
 static const std::string mostCommonOptionsDescription = "\
 Most commonly-used CVC4 options:${common_documentation}";
 
-#line 221 "${template}"
+#line 222 "${template}"
 
 static const std::string optionsDescription = mostCommonOptionsDescription + "\n\
 \n\
 Additional CVC4 options:${remaining_documentation}";
 
-#line 227 "${template}"
+#line 228 "${template}"
 
 static const std::string languageDescription = "\
 Languages currently supported as arguments to the -L / --lang option:\n\
@@ -287,7 +288,7 @@ static struct option cmdlineOptions[] = {${all_modules_long_options}
   { NULL, no_argument, NULL, '\0' }
 };/* cmdlineOptions */
 
-#line 291 "${template}"
+#line 292 "${template}"
 
 static void preemptGetopt(int& argc, char**& argv, const char* opt) {
   const size_t maxoptlen = 128;
@@ -320,10 +321,10 @@ namespace options {
 
 /** Set a given Options* as "current" just for a particular scope. */
 class OptionsGuard {
-  Options** d_field;
+  CVC4_THREADLOCAL_TYPE(Options*)* d_field;
   Options* d_old;
 public:
-  OptionsGuard(Options** field, Options* opts) :
+  OptionsGuard(CVC4_THREADLOCAL_TYPE(Options*)* field, Options* opts) :
     d_field(field),
     d_old(*field) {
     *field = opts;
@@ -414,7 +415,7 @@ int Options::parseOptions(int argc, char* main_argv[]) throw(OptionException) {
     switch(c) {
 ${all_modules_option_handlers}
 
-#line 418 "${template}"
+#line 419 "${template}"
 
     case ':':
       // This can be a long or short option, and the way to get at the

diff --git a/src/theory/arith/type_enumerator.h b/src/theory/arith/type_enumerator.h
index 3561e3c7b4fb6d1983a9d6f91af75902bb446751..e62baa2f679a3f593ec1b230a17b0a4d20758a30 100644 (file)
--- a/src/theory/arith/type_enumerator.h
+++ b/src/theory/arith/type_enumerator.h
@@ -37,7 +37,7 @@ class RationalEnumerator : public TypeEnumeratorBase<RationalEnumerator> {
 public:
 
   RationalEnumerator(TypeNode type) throw(AssertionException) :
-    TypeEnumeratorBase(type),
+    TypeEnumeratorBase<RationalEnumerator>(type),
     d_rat(0) {
     Assert(type.getKind() == kind::TYPE_CONSTANT &&
            type.getConst<TypeConstant>() == REAL_TYPE);
@@ -80,7 +80,7 @@ class IntegerEnumerator : public TypeEnumeratorBase<IntegerEnumerator> {
 public:
 
   IntegerEnumerator(TypeNode type) throw(AssertionException) :
-    TypeEnumeratorBase(type),
+    TypeEnumeratorBase<IntegerEnumerator>(type),
     d_int(0) {
     Assert(type.getKind() == kind::TYPE_CONSTANT &&
            type.getConst<TypeConstant>() == INTEGER_TYPE);

diff --git a/src/theory/arrays/type_enumerator.h b/src/theory/arrays/type_enumerator.h
index adea9a9e844c041cf1b072c1c973cdc921f5b75f..e613fc6678f9b9fb73554cc6caa31577e33da2bc 100644 (file)
--- a/src/theory/arrays/type_enumerator.h
+++ b/src/theory/arrays/type_enumerator.h
@@ -36,7 +36,7 @@ class ArrayEnumerator : public TypeEnumeratorBase<ArrayEnumerator> {
 public:
 
   ArrayEnumerator(TypeNode type) throw(AssertionException) :
-    TypeEnumeratorBase(type),
+    TypeEnumeratorBase<ArrayEnumerator>(type),
     d_index(TypeEnumerator(type.getArrayIndexType())),
     d_constituent(TypeEnumerator(type.getArrayConstituentType())) {
   }

diff --git a/src/theory/booleans/type_enumerator.h b/src/theory/booleans/type_enumerator.h
index 36fb6d855dca39d59bf0f61012fc2c34cd8b314e..c83e79d75f940fe7cef9988815e8bdedb6b0fc80 100644 (file)
--- a/src/theory/booleans/type_enumerator.h
+++ b/src/theory/booleans/type_enumerator.h
@@ -35,7 +35,7 @@ class BooleanEnumerator : public TypeEnumeratorBase<BooleanEnumerator> {
 public:
 
   BooleanEnumerator(TypeNode type) :
-    TypeEnumeratorBase(type),
+    TypeEnumeratorBase<BooleanEnumerator>(type),
     d_value(FALSE) {
     Assert(type.getKind() == kind::TYPE_CONSTANT &&
            type.getConst<TypeConstant>() == BOOLEAN_TYPE);

diff --git a/src/theory/builtin/type_enumerator.h b/src/theory/builtin/type_enumerator.h
index 4893c21007cb5c21241fe529573a04aad2772e20..c94ec73222aa8e7725ff2b7676cc5720ee47dd4c 100644 (file)
--- a/src/theory/builtin/type_enumerator.h
+++ b/src/theory/builtin/type_enumerator.h
@@ -37,7 +37,7 @@ class UninterpretedSortEnumerator : public TypeEnumeratorBase<UninterpretedSortE
 public:
 
   UninterpretedSortEnumerator(TypeNode type) throw(AssertionException) :
-    TypeEnumeratorBase(type),
+    TypeEnumeratorBase<UninterpretedSortEnumerator>(type),
     d_count(0) {
     Assert(type.getKind() == kind::SORT_TYPE);
   }

diff --git a/src/theory/bv/type_enumerator.h b/src/theory/bv/type_enumerator.h
index 01d431303b6fddf40886e736a774d557f3a85abb..746e77a0019f1ff22eb2a07e27830d199a3f3692 100644 (file)
--- a/src/theory/bv/type_enumerator.h
+++ b/src/theory/bv/type_enumerator.h
@@ -38,7 +38,7 @@ class BitVectorEnumerator : public TypeEnumeratorBase<BitVectorEnumerator> {
 public:
 
   BitVectorEnumerator(TypeNode type) throw(AssertionException) :
-    TypeEnumeratorBase(type),
+    TypeEnumeratorBase<BitVectorEnumerator>(type),
     d_size(type.getBitVectorSize()),
     d_bits(0) {
   }

diff --git a/src/theory/datatypes/type_enumerator.h b/src/theory/datatypes/type_enumerator.h
index 76d49ecee48ea9ed0b6a9c511f5b9432173b803b..1776bf4cea72597d216e1df70e91d508a83c14ce 100644 (file)
--- a/src/theory/datatypes/type_enumerator.h
+++ b/src/theory/datatypes/type_enumerator.h
@@ -62,7 +62,7 @@ class DatatypesEnumerator : public TypeEnumeratorBase<DatatypesEnumerator> {
 public:
 
   DatatypesEnumerator(TypeNode type) throw() :
-    TypeEnumeratorBase(type),
+    TypeEnumeratorBase<DatatypesEnumerator>(type),
     d_datatype(DatatypeType(type.toType()).getDatatype()),
     d_ctor(0),
     d_zeroCtor(0),

diff --git a/src/util/tls.h.in b/src/util/tls.h.in
index e77d256dcfbe82fc86bcb9f2ad0aca21830f63de..df53cae36741d629900b317005e4d1daf0359c2e 100644 (file)
--- a/src/util/tls.h.in
+++ b/src/util/tls.h.in
@@ -33,10 +33,12 @@
 #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 {