From 4e38397c87b4437089b92cd274e65f3d17096d73 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Wed, 1 Aug 2012 02:25:39 +0000 Subject: [PATCH] some fixes for Mac OS --- src/options/options_template.cpp | 21 +++++++++++---------- src/theory/arith/type_enumerator.h | 4 ++-- src/theory/arrays/type_enumerator.h | 2 +- src/theory/booleans/type_enumerator.h | 2 +- src/theory/builtin/type_enumerator.h | 2 +- src/theory/bv/type_enumerator.h | 2 +- src/theory/datatypes/type_enumerator.h | 2 +- src/util/tls.h.in | 2 ++ 8 files changed, 20 insertions(+), 17 deletions(-) diff --git a/src/options/options_template.cpp b/src/options/options_template.cpp index 2df69b5d3..9b9b711ad 100644 --- 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 3561e3c7b..e62baa2f6 100644 --- a/src/theory/arith/type_enumerator.h +++ b/src/theory/arith/type_enumerator.h @@ -37,7 +37,7 @@ class RationalEnumerator : public TypeEnumeratorBase { public: RationalEnumerator(TypeNode type) throw(AssertionException) : - TypeEnumeratorBase(type), + TypeEnumeratorBase(type), d_rat(0) { Assert(type.getKind() == kind::TYPE_CONSTANT && type.getConst() == REAL_TYPE); @@ -80,7 +80,7 @@ class IntegerEnumerator : public TypeEnumeratorBase { public: IntegerEnumerator(TypeNode type) throw(AssertionException) : - TypeEnumeratorBase(type), + TypeEnumeratorBase(type), d_int(0) { Assert(type.getKind() == kind::TYPE_CONSTANT && type.getConst() == INTEGER_TYPE); diff --git a/src/theory/arrays/type_enumerator.h b/src/theory/arrays/type_enumerator.h index adea9a9e8..e613fc667 100644 --- a/src/theory/arrays/type_enumerator.h +++ b/src/theory/arrays/type_enumerator.h @@ -36,7 +36,7 @@ class ArrayEnumerator : public TypeEnumeratorBase { public: ArrayEnumerator(TypeNode type) throw(AssertionException) : - TypeEnumeratorBase(type), + TypeEnumeratorBase(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 36fb6d855..c83e79d75 100644 --- a/src/theory/booleans/type_enumerator.h +++ b/src/theory/booleans/type_enumerator.h @@ -35,7 +35,7 @@ class BooleanEnumerator : public TypeEnumeratorBase { public: BooleanEnumerator(TypeNode type) : - TypeEnumeratorBase(type), + TypeEnumeratorBase(type), d_value(FALSE) { Assert(type.getKind() == kind::TYPE_CONSTANT && type.getConst() == BOOLEAN_TYPE); diff --git a/src/theory/builtin/type_enumerator.h b/src/theory/builtin/type_enumerator.h index 4893c2100..c94ec7322 100644 --- a/src/theory/builtin/type_enumerator.h +++ b/src/theory/builtin/type_enumerator.h @@ -37,7 +37,7 @@ class UninterpretedSortEnumerator : public TypeEnumeratorBase(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 01d431303..746e77a00 100644 --- a/src/theory/bv/type_enumerator.h +++ b/src/theory/bv/type_enumerator.h @@ -38,7 +38,7 @@ class BitVectorEnumerator : public TypeEnumeratorBase { public: BitVectorEnumerator(TypeNode type) throw(AssertionException) : - TypeEnumeratorBase(type), + TypeEnumeratorBase(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 76d49ecee..1776bf4ce 100644 --- a/src/theory/datatypes/type_enumerator.h +++ b/src/theory/datatypes/type_enumerator.h @@ -62,7 +62,7 @@ class DatatypesEnumerator : public TypeEnumeratorBase { public: DatatypesEnumerator(TypeNode type) throw() : - TypeEnumeratorBase(type), + TypeEnumeratorBase(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 e77d256dc..df53cae36 100644 --- 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 # 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 { -- 2.30.2