projects
/
cvc5.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
|
inline
| side by side (parent:
c90b1b6
)
some fixes for Mac OS
author
Morgan Deters
<mdeters@gmail.com>
Wed, 1 Aug 2012 02:25:39 +0000
(
02:25
+0000)
committer
Morgan Deters
<mdeters@gmail.com>
Wed, 1 Aug 2012 02:25:39 +0000
(
02:25
+0000)
src/options/options_template.cpp
patch
|
blob
|
history
src/theory/arith/type_enumerator.h
patch
|
blob
|
history
src/theory/arrays/type_enumerator.h
patch
|
blob
|
history
src/theory/booleans/type_enumerator.h
patch
|
blob
|
history
src/theory/builtin/type_enumerator.h
patch
|
blob
|
history
src/theory/bv/type_enumerator.h
patch
|
blob
|
history
src/theory/datatypes/type_enumerator.h
patch
|
blob
|
history
src/util/tls.h.in
patch
|
blob
|
history
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/configuration.h"
#include "util/exception.h"
#include "util/language.h"
+#include "util/tls.h"
${include_all_option_headers}
${include_all_option_headers}
-#line 4
0
"${template}"
+#line 4
1
"${template}"
#include "util/output.h"
#include "options/options_holder.h"
#include "util/output.h"
#include "options/options_holder.h"
@@
-45,7
+46,7
@@
${include_all_option_headers}
${option_handler_includes}
${option_handler_includes}
-#line
49
"${template}"
+#line
50
"${template}"
using namespace CVC4;
using namespace CVC4::options;
using namespace CVC4;
using namespace CVC4::options;
@@
-182,7
+183,7
@@
void runBoolPredicates(T, std::string option, bool b, SmtEngine* smt) {
${all_custom_handlers}
${all_custom_handlers}
-#line 18
6
"${template}"
+#line 18
7
"${template}"
#ifdef CVC4_DEBUG
# define USE_EARLY_TYPE_CHECKING_BY_DEFAULT true
#ifdef CVC4_DEBUG
# define USE_EARLY_TYPE_CHECKING_BY_DEFAULT true
@@
-212,18
+213,18
@@
options::OptionsHolder::OptionsHolder() : ${all_modules_defaults}
{
}
{
}
-#line 21
6
"${template}"
+#line 21
7
"${template}"
static const std::string mostCommonOptionsDescription = "\
Most commonly-used CVC4 options:${common_documentation}";
static const std::string mostCommonOptionsDescription = "\
Most commonly-used CVC4 options:${common_documentation}";
-#line 22
1
"${template}"
+#line 22
2
"${template}"
static const std::string optionsDescription = mostCommonOptionsDescription + "\n\
\n\
Additional CVC4 options:${remaining_documentation}";
static const std::string optionsDescription = mostCommonOptionsDescription + "\n\
\n\
Additional CVC4 options:${remaining_documentation}";
-#line 22
7
"${template}"
+#line 22
8
"${template}"
static const std::string languageDescription = "\
Languages currently supported as arguments to the -L / --lang option:\n\
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 */
{ NULL, no_argument, NULL, '\0' }
};/* cmdlineOptions */
-#line 29
1
"${template}"
+#line 29
2
"${template}"
static void preemptGetopt(int& argc, char**& argv, const char* opt) {
const size_t maxoptlen = 128;
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 {
/** 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:
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;
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}
switch(c) {
${all_modules_option_handlers}
-#line 41
8
"${template}"
+#line 41
9
"${template}"
case ':':
// This can be a long or short option, and the way to get at the
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) :
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);
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) :
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);
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) :
public:
ArrayEnumerator(TypeNode type) throw(AssertionException) :
- TypeEnumeratorBase(type),
+ TypeEnumeratorBase
<ArrayEnumerator>
(type),
d_index(TypeEnumerator(type.getArrayIndexType())),
d_constituent(TypeEnumerator(type.getArrayConstituentType())) {
}
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) :
public:
BooleanEnumerator(TypeNode type) :
- TypeEnumeratorBase(type),
+ TypeEnumeratorBase
<BooleanEnumerator>
(type),
d_value(FALSE) {
Assert(type.getKind() == kind::TYPE_CONSTANT &&
type.getConst<TypeConstant>() == BOOLEAN_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) :
public:
UninterpretedSortEnumerator(TypeNode type) throw(AssertionException) :
- TypeEnumeratorBase(type),
+ TypeEnumeratorBase
<UninterpretedSortEnumerator>
(type),
d_count(0) {
Assert(type.getKind() == kind::SORT_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) :
public:
BitVectorEnumerator(TypeNode type) throw(AssertionException) :
- TypeEnumeratorBase(type),
+ TypeEnumeratorBase
<BitVectorEnumerator>
(type),
d_size(type.getBitVectorSize()),
d_bits(0) {
}
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() :
public:
DatatypesEnumerator(TypeNode type) throw() :
- TypeEnumeratorBase(type),
+ TypeEnumeratorBase
<DatatypesEnumerator>
(type),
d_datatype(DatatypeType(type.toType()).getDatatype()),
d_ctor(0),
d_zeroCtor(0),
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
#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 >
#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 {
namespace CVC4 {