From dd1d53046c4e4a4a860090881912a8f195fba389 Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Tue, 7 May 2019 09:58:20 +0200 Subject: [PATCH 1/3] utility/constants.cpp: Fixing unknown 'isnan' --- src/storm/utility/constants.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/storm/utility/constants.cpp b/src/storm/utility/constants.cpp index 050955956..b1944c267 100644 --- a/src/storm/utility/constants.cpp +++ b/src/storm/utility/constants.cpp @@ -52,7 +52,7 @@ namespace storm { template<> bool isNan(double const& value) { - return isnan(value); + return std::isnan(value); } bool isAlmostZero(double const& a) { From fe658ee78700c5b184c44e7a74058f0bdc8e8a53 Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Tue, 7 May 2019 10:36:58 +0200 Subject: [PATCH 2/3] Reverting the previous fix since the jit builder wasn't happy about the carl/formula/Formula.h include. --- src/storm/adapters/RationalFunctionAdapter.h | 23 -------------------- src/storm/analysis/GraphConditions.h | 3 ++- 2 files changed, 2 insertions(+), 24 deletions(-) diff --git a/src/storm/adapters/RationalFunctionAdapter.h b/src/storm/adapters/RationalFunctionAdapter.h index e41869b5b..f403103f5 100644 --- a/src/storm/adapters/RationalFunctionAdapter.h +++ b/src/storm/adapters/RationalFunctionAdapter.h @@ -9,27 +9,6 @@ #include #include -// Some header files on macOS (included via INTEL TBB) might #define TRUE and FALSE, which in carl/formula/Formula.h are used as FormulaTypes. -// Hence, we temporarily #undef these: -#ifdef TRUE -#define STORM_TEMP_TRUE TRUE -#undef TRUE -#endif -#ifdef FALSE -#define STORM_TEMP_FALSE FALSE -#undef FALSE -#endif -#include -// Restore TRUE / FALSE macros. -#ifdef STORM_TEMP_TRUE -#define TRUE STORM_TEMP_TRUE -#undef STORM_TEMP_TRUE -#endif -#ifdef STORM_TEMP_FALSE -#define FALSE STORM_TEMP_FALSE -#undef STORM_TEMP_FALSE -#endif - namespace carl { // Define hash values for all polynomials and rational function. template @@ -78,7 +57,5 @@ namespace storm { typedef carl::RationalFunction RationalFunction; typedef carl::Interval Interval; - - typedef carl::Formula RationalFunctionConstraint; } diff --git a/src/storm/analysis/GraphConditions.h b/src/storm/analysis/GraphConditions.h index f9f119fc1..00c0d5101 100644 --- a/src/storm/analysis/GraphConditions.h +++ b/src/storm/analysis/GraphConditions.h @@ -4,6 +4,7 @@ #include #include "storm/adapters/RationalFunctionAdapter.h" #include "storm/models/sparse/Dtmc.h" +#include namespace storm { namespace analysis { @@ -16,7 +17,7 @@ namespace storm { template struct ConstraintType::value>::type> { - typedef storm::RationalFunctionConstraint val; + typedef carl::Formula val; }; /** From 3a11a4b3eb8377a1316e47af3d4219f0edeaaf56 Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Tue, 7 May 2019 10:37:59 +0200 Subject: [PATCH 3/3] Introducing a TBB adapter that #undefs TRUE and FALSE. --- .../3rdparty/gmm-5.2/include/gmm/gmm_blas.h | 2 +- src/storm-cli-utilities/cli.cpp | 5 ++- src/storm/adapters/IntelTbbAdapter.h | 32 +++++++++++++++++++ src/storm/settings/modules/CoreSettings.cpp | 1 + src/storm/solver/GmmxxMultiplier.cpp | 1 + src/storm/solver/NativeMultiplier.cpp | 1 + src/storm/storage/SparseMatrix.cpp | 7 ---- src/storm/storage/SparseMatrix.h | 1 + src/storm/utility/VectorHelper.cpp | 3 +- src/storm/utility/vector.h | 6 +--- 10 files changed, 41 insertions(+), 18 deletions(-) create mode 100644 src/storm/adapters/IntelTbbAdapter.h diff --git a/resources/3rdparty/gmm-5.2/include/gmm/gmm_blas.h b/resources/3rdparty/gmm-5.2/include/gmm/gmm_blas.h index 19e58f755..4fbe070d3 100644 --- a/resources/3rdparty/gmm-5.2/include/gmm/gmm_blas.h +++ b/resources/3rdparty/gmm-5.2/include/gmm/gmm_blas.h @@ -44,7 +44,7 @@ #ifdef STORM_HAVE_INTELTBB #include // This fixes a potential dependency ordering problem between GMM and TBB -#include "tbb/tbb.h" +#include "storm/adapters/IntelTbbAdapter.h" #include #endif diff --git a/src/storm-cli-utilities/cli.cpp b/src/storm-cli-utilities/cli.cpp index e79971cbc..e4a929445 100644 --- a/src/storm-cli-utilities/cli.cpp +++ b/src/storm-cli-utilities/cli.cpp @@ -17,9 +17,8 @@ // Includes for the linked libraries and versions header. -#ifdef STORM_HAVE_INTELTBB -# include "tbb/tbb_stddef.h" -#endif +#include "storm/adapters/IntelTbbAdapter.h" + #ifdef STORM_HAVE_GLPK # include "glpk.h" #endif diff --git a/src/storm/adapters/IntelTbbAdapter.h b/src/storm/adapters/IntelTbbAdapter.h new file mode 100644 index 000000000..fb4d7eb72 --- /dev/null +++ b/src/storm/adapters/IntelTbbAdapter.h @@ -0,0 +1,32 @@ +#pragma once + +// To detect whether the usage of TBB is possible, this include is neccessary +#include "storm-config.h" + + +/* On macOS, TBB includes the header + * /Library/Developer/CommandLineTools/SDKs/MacOSX10.14.sdk/usr/include/mach/boolean.h + * which #defines macros TRUE and FALSE. Since these also occur as identifiers, we #undef them after including TBB. + * We still issue a warning in case these macros have been defined before. +*/ + +#ifdef TRUE +#warning "Undefining previously defined macro 'TRUE'." +#endif + +#ifdef FALSE +#warning "Undefining previously defined macro 'FALSE'." +#endif + +#ifdef STORM_HAVE_INTELTBB +#include "tbb/tbb.h" +#include "tbb/tbb_stddef.h" +#endif + +#ifdef TRUE +#undef TRUE +#endif + +#ifdef FALSE +#undef FALSE +#endif diff --git a/src/storm/settings/modules/CoreSettings.cpp b/src/storm/settings/modules/CoreSettings.cpp index 3925012e3..baf474d1c 100644 --- a/src/storm/settings/modules/CoreSettings.cpp +++ b/src/storm/settings/modules/CoreSettings.cpp @@ -9,6 +9,7 @@ #include "storm/solver/SolverSelectionOptions.h" #include "storm/storage/dd/DdType.h" +#include "storm/adapters/IntelTbbAdapter.h" #include "storm/utility/macros.h" #include "storm/exceptions/IllegalArgumentValueException.h" diff --git a/src/storm/solver/GmmxxMultiplier.cpp b/src/storm/solver/GmmxxMultiplier.cpp index 95abf61fb..59d71af8e 100644 --- a/src/storm/solver/GmmxxMultiplier.cpp +++ b/src/storm/solver/GmmxxMultiplier.cpp @@ -2,6 +2,7 @@ #include "storm/adapters/RationalNumberAdapter.h" #include "storm/adapters/RationalFunctionAdapter.h" +#include "storm/adapters/IntelTbbAdapter.h" #include "storm/storage/SparseMatrix.h" #include "storm/settings/SettingsManager.h" #include "storm/settings/modules/CoreSettings.h" diff --git a/src/storm/solver/NativeMultiplier.cpp b/src/storm/solver/NativeMultiplier.cpp index 7dd2457df..b8c6c3549 100644 --- a/src/storm/solver/NativeMultiplier.cpp +++ b/src/storm/solver/NativeMultiplier.cpp @@ -10,6 +10,7 @@ #include "storm/adapters/RationalNumberAdapter.h" #include "storm/adapters/RationalFunctionAdapter.h" +#include "storm/adapters/IntelTbbAdapter.h" #include "storm/utility/macros.h" diff --git a/src/storm/storage/SparseMatrix.cpp b/src/storm/storage/SparseMatrix.cpp index 2ca0c823c..cdeaaf9a2 100644 --- a/src/storm/storage/SparseMatrix.cpp +++ b/src/storm/storage/SparseMatrix.cpp @@ -1,12 +1,5 @@ #include -// To detect whether the usage of TBB is possible, this include is neccessary -#include "storm-config.h" - -#ifdef STORM_HAVE_INTELTBB -#include "tbb/tbb.h" -#endif - #include "storm/storage/sparse/StateType.h" #include "storm/storage/SparseMatrix.h" #include "storm/adapters/RationalFunctionAdapter.h" diff --git a/src/storm/storage/SparseMatrix.h b/src/storm/storage/SparseMatrix.h index d33eda907..dbdd4086d 100644 --- a/src/storm/storage/SparseMatrix.h +++ b/src/storm/storage/SparseMatrix.h @@ -16,6 +16,7 @@ #include "storm/utility/macros.h" #include "storm/utility/constants.h" #include "storm/adapters/RationalFunctionAdapter.h" +#include "storm/adapters/IntelTbbAdapter.h" // Forward declaration for adapter classes. namespace storm { diff --git a/src/storm/utility/VectorHelper.cpp b/src/storm/utility/VectorHelper.cpp index ca40c8844..352910dd1 100644 --- a/src/storm/utility/VectorHelper.cpp +++ b/src/storm/utility/VectorHelper.cpp @@ -5,8 +5,7 @@ #include "storm/adapters/RationalNumberAdapter.h" #include "storm/adapters/RationalFunctionAdapter.h" - -#include "storm-config.h" +#include "storm/adapters/IntelTbbAdapter.h" #include "storm/utility/vector.h" diff --git a/src/storm/utility/vector.h b/src/storm/utility/vector.h index 153f74a36..82d698dde 100644 --- a/src/storm/utility/vector.h +++ b/src/storm/utility/vector.h @@ -1,16 +1,12 @@ #ifndef STORM_UTILITY_VECTOR_H_ #define STORM_UTILITY_VECTOR_H_ -#include "storm-config.h" -#ifdef STORM_HAVE_INTELTBB -#include "tbb/tbb.h" -#endif - #include #include #include #include #include +#include #include