From 5faebdff8682c1490051f3ee9454b19c55f482da Mon Sep 17 00:00:00 2001 From: sjunges Date: Tue, 19 Jul 2016 11:46:22 +0200 Subject: [PATCH] constants in header Former-commit-id: 281e4908734c5f65f371db11161c064223a4b166 --- CMakeLists.txt | 2 +- src/builder/ExplicitDFTModelBuilder.cpp | 2 +- src/utility/constants.cpp | 520 ++++++++++++------------ src/utility/constants.h | 195 +++++++-- src/utility/storm.h | 2 +- src/utility/vector.h | 7 +- 6 files changed, 436 insertions(+), 292 deletions(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index 0c564cf61..0f5eb9612 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -364,7 +364,7 @@ find_package(CLN QUIET) set(STORM_USE_CLN_NUMBERS OFF) if(CLN_FOUND) set(STORM_HAVE_CLN ON) - set(STORM_USE_CLN_NUMBERS ON) + set(STORM_USE_CLN_NUMBERS OFF) message(STATUS "StoRM - Linking with CLN ${CLN_VERSION_STRING}") include_directories("${CLN_INCLUDE_DIR}") list(APPEND STORM_LINK_LIBRARIES ${CLN_LIBRARIES}) diff --git a/src/builder/ExplicitDFTModelBuilder.cpp b/src/builder/ExplicitDFTModelBuilder.cpp index 4fb6131df..25b96b9cd 100644 --- a/src/builder/ExplicitDFTModelBuilder.cpp +++ b/src/builder/ExplicitDFTModelBuilder.cpp @@ -2,7 +2,7 @@ #include #include #include -#include +#include "src/utility/vector.h" #include #include diff --git a/src/utility/constants.cpp b/src/utility/constants.cpp index 4821d1b94..00b6e1154 100644 --- a/src/utility/constants.cpp +++ b/src/utility/constants.cpp @@ -1,168 +1,168 @@ -#include "src/utility/constants.h" - -#include "src/storage/sparse/StateType.h" +//#include "src/utility/constants.h" +// +//#include "src/storage/sparse/StateType.h" #include "src/storage/SparseMatrix.h" -#include "src/settings/SettingsManager.h" -#include "src/settings/modules/GeneralSettings.h" - -#include "src/adapters/CarlAdapter.h" - +//#include "src/settings/SettingsManager.h" +//#include "src/settings/modules/GeneralSettings.h" +// +//#include "src/adapters/CarlAdapter.h" +// namespace storm { namespace utility { - - template - ValueType one() { - return ValueType(1); - } - - template - ValueType zero() { - return ValueType(0); - } - - template - ValueType infinity() { - return std::numeric_limits::infinity(); - } - - template - bool isOne(ValueType const& a) { - return a == one(); - } - - template - bool isZero(ValueType const& a) { - return a == zero(); - } - - template - bool isConstant(ValueType const& a) { - return true; - } - - template<> - bool isOne(storm::RationalNumber const& a) { - return carl::isOne(a); - } - - template<> - bool isZero(storm::RationalNumber const& a) { - return carl::isZero(a); - } - - template<> - storm::RationalNumber infinity() { - // FIXME: this should be treated more properly. - return storm::RationalNumber(-1); - } - - template<> - bool isOne(storm::RationalFunction const& a) { - return a.isOne(); - } - - template<> - bool isZero(storm::RationalFunction const& a) { - return a.isZero(); - } - - template<> - bool isConstant(storm::RationalFunction const& a) { - return a.isConstant(); - } - - template<> - bool isOne(storm::Polynomial const& a) { - return a.isOne(); - } - - template<> - bool isZero(storm::Polynomial const& a) { - return a.isZero(); - } - - template<> - bool isConstant(storm::Polynomial const& a) { - return a.isConstant(); - } - - template<> - storm::RationalFunction infinity() { - // FIXME: this should be treated more properly. - return storm::RationalFunction(-1.0); - } - - template - ValueType pow(ValueType const& value, uint_fast64_t exponent) { - return std::pow(value, exponent); - } - - template - ValueType simplify(ValueType value) { - // In the general case, we don't do anything here, but merely return the value. If something else is - // supposed to happen here, the templated function can be specialized for this particular type. - return value; - } - - template<> - double convertNumber(double const& number){ - return number; - } - - template - ValueType abs(ValueType const& number) { - return std::fabs(number); - } - - template<> - RationalFunction& simplify(RationalFunction& value); - - template<> - RationalFunction&& simplify(RationalFunction&& value); - - template<> - RationalFunction pow(RationalFunction const& value, uint_fast64_t exponent) { - return carl::pow(value, exponent); - } - - template<> - RationalFunction simplify(RationalFunction value) { - value.simplify(); - return value; - } - - template<> - RationalFunction& simplify(RationalFunction& value) { - value.simplify(); - return value; - } - - template<> - RationalFunction&& simplify(RationalFunction&& value) { - value.simplify(); - return std::move(value); - } - - template<> - double convertNumber(RationalNumber const& number){ - return carl::toDouble(number); - } - - template<> - RationalNumber convertNumber(double const& number){ - return carl::rationalize(number); - } - - template<> - RationalFunction convertNumber(double const& number){ - return RationalFunction(carl::rationalize(number)); - } - - template<> - storm::RationalNumber abs(storm::RationalNumber const& number) { - return carl::abs(number); - } +// template +// ValueType one() { +// return ValueType(1); +// } +// +// template +// ValueType zero() { +// return ValueType(0); +// } +// +// template +// ValueType infinity() { +// return std::numeric_limits::infinity(); +// } +// +// template +// bool isOne(ValueType const& a) { +// return a == one(); +// } +// +// template +// bool isZero(ValueType const& a) { +// return a == zero(); +// } +// +// template +// bool isConstant(ValueType const& a) { +// return true; +// } +// +// template<> +// bool isOne(storm::RationalNumber const& a) { +// return carl::isOne(a); +// } +// +// template<> +// bool isZero(storm::RationalNumber const& a) { +// return carl::isZero(a); +// } +// +// template<> +// storm::RationalNumber infinity() { +// // FIXME: this should be treated more properly. +// return storm::RationalNumber(-1); +// } +// +// template<> +// bool isOne(storm::RationalFunction const& a) { +// return a.isOne(); +// } +// +// template<> +// bool isZero(storm::RationalFunction const& a) { +// return a.isZero(); +// } +// +// template<> +// bool isConstant(storm::RationalFunction const& a) { +// return a.isConstant(); +// } +// +// template<> +// bool isOne(storm::Polynomial const& a) { +// return a.isOne(); +// } +// +// template<> +// bool isZero(storm::Polynomial const& a) { +// return a.isZero(); +// } +// +// template<> +// bool isConstant(storm::Polynomial const& a) { +// return a.isConstant(); +// } +// +// template<> +// storm::RationalFunction infinity() { +// // FIXME: this should be treated more properly. +// return storm::RationalFunction(-1.0); +// } +// +// template +// ValueType pow(ValueType const& value, uint_fast64_t exponent) { +// return std::pow(value, exponent); +// } +// +// template +// ValueType simplify(ValueType value) { +// // In the general case, we don't do anything here, but merely return the value. If something else is +// // supposed to happen here, the templated function can be specialized for this particular type. +// return value; +// } +// +// template<> +// double convertNumber(double const& number){ +// return number; +// } +// +// template +// ValueType abs(ValueType const& number) { +// return carl::abs(number); +// } +// +// template<> +// RationalFunction& simplify(RationalFunction& value); +// +// template<> +// RationalFunction&& simplify(RationalFunction&& value); +// +// template<> +// RationalFunction pow(RationalFunction const& value, uint_fast64_t exponent) { +// return carl::pow(value, exponent); +// } +// +// template<> +// RationalFunction simplify(RationalFunction value) { +// value.simplify(); +// return value; +// } +// +// template<> +// RationalFunction& simplify(RationalFunction& value) { +// value.simplify(); +// return value; +// } +// +// template<> +// RationalFunction&& simplify(RationalFunction&& value) { +// value.simplify(); +// return std::move(value); +// } +// +// template<> +// double convertNumber(RationalNumber const& number){ +// return carl::toDouble(number); +// } +// +// template<> +// RationalNumber convertNumber(double const& number){ +// return carl::rationalize(number); +// } +// +// template<> +// RationalFunction convertNumber(double const& number){ +// return RationalFunction(carl::rationalize(number)); +// } +//// +//// template<> +//// storm::RationalNumber abs(storm::RationalNumber const& number) { +//// return carl::abs(number); +//// } +// template storm::storage::MatrixEntry simplify(storm::storage::MatrixEntry matrixEntry) { simplify(matrixEntry.getValue()); @@ -180,127 +180,127 @@ namespace storm { simplify(matrixEntry.getValue()); return std::move(matrixEntry); } - - // Explicit instantiations. - template bool isOne(double const& value); - template bool isZero(double const& value); - template bool isConstant(double const& value); - - template double one(); - template double zero(); - template double infinity(); - - template double pow(double const& value, uint_fast64_t exponent); - - template double simplify(double value); +// +// // Explicit instantiations. +// template bool isOne(double const& value); +// template bool isZero(double const& value); +// template bool isConstant(double const& value); +// +// template double one(); +// template double zero(); +// template double infinity(); +// +// template double pow(double const& value, uint_fast64_t exponent); +// +// template double simplify(double value); template storm::storage::MatrixEntry simplify(storm::storage::MatrixEntry matrixEntry); template storm::storage::MatrixEntry& simplify(storm::storage::MatrixEntry& matrixEntry); template storm::storage::MatrixEntry&& simplify(storm::storage::MatrixEntry&& matrixEntry); - - template double abs(double const& number); - - template bool isOne(float const& value); - template bool isZero(float const& value); - template bool isConstant(float const& value); - - template float one(); - template float zero(); - template float infinity(); - - template float pow(float const& value, uint_fast64_t exponent); - - template float simplify(float value); +// +// template double abs(double const& number); +// +// template bool isOne(float const& value); +// template bool isZero(float const& value); +// template bool isConstant(float const& value); +// +// template float one(); +// template float zero(); +// template float infinity(); +// +// template float pow(float const& value, uint_fast64_t exponent); +// +// template float simplify(float value); template storm::storage::MatrixEntry simplify(storm::storage::MatrixEntry matrixEntry); template storm::storage::MatrixEntry& simplify(storm::storage::MatrixEntry& matrixEntry); template storm::storage::MatrixEntry&& simplify(storm::storage::MatrixEntry&& matrixEntry); - - template bool isOne(int const& value); - template bool isZero(int const& value); - template bool isConstant(int const& value); - - template int one(); - template int zero(); - template int infinity(); - - template int pow(int const& value, uint_fast64_t exponent); - - template int simplify(int value); - + +// template bool isOne(int const& value); +// template bool isZero(int const& value); +// template bool isConstant(int const& value); +// +// template int one(); +// template int zero(); +// template int infinity(); +// +// template int pow(int const& value, uint_fast64_t exponent); +// +// template int simplify(int value); + template storm::storage::MatrixEntry simplify(storm::storage::MatrixEntry matrixEntry); template storm::storage::MatrixEntry& simplify(storm::storage::MatrixEntry& matrixEntry); template storm::storage::MatrixEntry&& simplify(storm::storage::MatrixEntry&& matrixEntry); - template bool isOne(storm::storage::sparse::state_type const& value); - template bool isZero(storm::storage::sparse::state_type const& value); - template bool isConstant(storm::storage::sparse::state_type const& value); - - template uint32_t one(); - template uint32_t zero(); - template uint32_t infinity(); - - template storm::storage::sparse::state_type one(); - template storm::storage::sparse::state_type zero(); - template storm::storage::sparse::state_type infinity(); - - template storm::storage::sparse::state_type pow(storm::storage::sparse::state_type const& value, uint_fast64_t exponent); - - template storm::storage::sparse::state_type simplify(storm::storage::sparse::state_type value); - +// template bool isOne(storm::storage::sparse::state_type const& value); +// template bool isZero(storm::storage::sparse::state_type const& value); +// template bool isConstant(storm::storage::sparse::state_type const& value); +// +// template uint32_t one(); +// template uint32_t zero(); +// template uint32_t infinity(); +// +// template storm::storage::sparse::state_type one(); +// template storm::storage::sparse::state_type zero(); +// template storm::storage::sparse::state_type infinity(); +// +// template storm::storage::sparse::state_type pow(storm::storage::sparse::state_type const& value, uint_fast64_t exponent); +// +// template storm::storage::sparse::state_type simplify(storm::storage::sparse::state_type value); +// template storm::storage::MatrixEntry simplify(storm::storage::MatrixEntry matrixEntry); template storm::storage::MatrixEntry& simplify(storm::storage::MatrixEntry& matrixEntry); template storm::storage::MatrixEntry&& simplify(storm::storage::MatrixEntry&& matrixEntry); - - // Instantiations for rational number. - template bool isOne(storm::RationalNumber const& value); - template bool isZero(storm::RationalNumber const& value); - template bool isConstant(storm::RationalNumber const& value); - - template storm::RationalNumber one(); - template storm::RationalNumber zero(); - template storm::RationalNumber infinity(); - - template double convertNumber(storm::RationalNumber const& number); - template storm::RationalNumber convertNumber(double const& number); - - template storm::RationalNumber abs(storm::RationalNumber const& number); - -// template storm::RationalNumber pow(storm::RationalNumber const& value, uint_fast64_t exponent); - - template storm::RationalNumber simplify(storm::RationalNumber value); +// +// // Instantiations for rational number. +// template bool isOne(storm::RationalNumber const& value); +// template bool isZero(storm::RationalNumber const& value); +// template bool isConstant(storm::RationalNumber const& value); +// +// template storm::RationalNumber one(); +// template storm::RationalNumber zero(); +// template storm::RationalNumber infinity(); +// +// template double convertNumber(storm::RationalNumber const& number); +// template storm::RationalNumber convertNumber(double const& number); +// +// template storm::RationalNumber abs(storm::RationalNumber const& number); +// +//// template storm::RationalNumber pow(storm::RationalNumber const& value, uint_fast64_t exponent); +// +// template storm::RationalNumber simplify(storm::RationalNumber value); template storm::storage::MatrixEntry simplify(storm::storage::MatrixEntry matrixEntry); template storm::storage::MatrixEntry& simplify(storm::storage::MatrixEntry& matrixEntry); template storm::storage::MatrixEntry&& simplify(storm::storage::MatrixEntry&& matrixEntry); - + #ifdef STORM_HAVE_CARL - template bool isOne(RationalFunction const& value); - template bool isZero(RationalFunction const& value); - template bool isConstant(RationalFunction const& value); - - template RationalFunction one(); - template RationalFunction zero(); - template storm::RationalFunction infinity(); - - template RationalFunction pow(RationalFunction const& value, uint_fast64_t exponent); - template RationalFunction simplify(RationalFunction value); - template RationalFunction& simplify(RationalFunction& value); - template RationalFunction&& simplify(RationalFunction&& value); - - template Polynomial one(); - template Polynomial zero(); - - template bool isOne(Interval const& value); - template bool isZero(Interval const& value); - template bool isConstant(Interval const& value); - - template Interval one(); - template Interval zero(); - +// template bool isOne(RationalFunction const& value); +// template bool isZero(RationalFunction const& value); +// template bool isConstant(RationalFunction const& value); +// +// template RationalFunction one(); +// template RationalFunction zero(); +// template storm::RationalFunction infinity(); +// +// template RationalFunction pow(RationalFunction const& value, uint_fast64_t exponent); +// template RationalFunction simplify(RationalFunction value); +// template RationalFunction& simplify(RationalFunction& value); +// template RationalFunction&& simplify(RationalFunction&& value); +// +// template Polynomial one(); +// template Polynomial zero(); +// +// template bool isOne(Interval const& value); +// template bool isZero(Interval const& value); +// template bool isConstant(Interval const& value); +// +// template Interval one(); +// template Interval zero(); + template storm::storage::MatrixEntry simplify(storm::storage::MatrixEntry matrixEntry); template storm::storage::MatrixEntry& simplify(storm::storage::MatrixEntry& matrixEntry); template storm::storage::MatrixEntry&& simplify(storm::storage::MatrixEntry&& matrixEntry); #endif - +// } } diff --git a/src/utility/constants.h b/src/utility/constants.h index 4ec4e7539..7f97acdb4 100644 --- a/src/utility/constants.h +++ b/src/utility/constants.h @@ -11,6 +11,11 @@ #include #include +#include "src/storage/sparse/StateType.h" +#include "src/settings/SettingsManager.h" +#include "src/settings/modules/GeneralSettings.h" + +#include "src/adapters/CarlAdapter.h" namespace storm { @@ -20,42 +25,182 @@ namespace storm { } namespace utility { - + template - ValueType one(); - + ValueType one() { + return ValueType(1); + } + template - ValueType zero(); - + ValueType zero() { + return ValueType(0); + } + template - ValueType infinity(); - + ValueType infinity() { + return std::numeric_limits::infinity(); + } + template - bool isOne(ValueType const& a); - + bool isOne(ValueType const& a) { + return a == one(); + } + template - bool isZero(ValueType const& a); - + bool isZero(ValueType const& a) { + return a == zero(); + } + template - bool isConstant(ValueType const& a); - + bool isConstant(ValueType const& a) { + return true; + } + + template<> + bool isOne(storm::RationalNumber const& a) { + return carl::isOne(a); + } + + template<> + bool isZero(storm::RationalNumber const& a) { + return carl::isZero(a); + } + + template<> + storm::RationalNumber infinity() { + // FIXME: this should be treated more properly. + return storm::RationalNumber(-1); + } + + template<> + bool isOne(storm::RationalFunction const& a) { + return a.isOne(); + } + + template<> + bool isZero(storm::RationalFunction const& a) { + return a.isZero(); + } + + template<> + bool isConstant(storm::RationalFunction const& a) { + return a.isConstant(); + } + + template<> + bool isOne(storm::Polynomial const& a) { + return a.isOne(); + } + + template<> + bool isZero(storm::Polynomial const& a) { + return a.isZero(); + } + + template<> + bool isConstant(storm::Polynomial const& a) { + return a.isConstant(); + } + + template<> + storm::RationalFunction infinity() { + // FIXME: this should be treated more properly. + return storm::RationalFunction(-1.0); + } + template - ValueType pow(ValueType const& value, uint_fast64_t exponent); - + ValueType pow(ValueType const& value, uint_fast64_t exponent) { + return std::pow(value, exponent); + } + template - ValueType simplify(ValueType value); - - template - storm::storage::MatrixEntry& simplify(storm::storage::MatrixEntry& matrixEntry); + ValueType simplify(ValueType value) { + // In the general case, we don't do anything here, but merely return the value. If something else is + // supposed to happen here, the templated function can be specialized for this particular type. + return value; + } - template - storm::storage::MatrixEntry&& simplify(storm::storage::MatrixEntry&& matrixEntry); - - template + template TargetType convertNumber(SourceType const& number); - + + template<> + double convertNumber(double const& number){ + return number; + } + template - ValueType abs(ValueType const& number); + ValueType abs(ValueType const& number) { + return carl::abs(number); + } + + template<> + RationalFunction& simplify(RationalFunction& value); + + template<> + RationalFunction&& simplify(RationalFunction&& value); + + template<> + RationalFunction pow(RationalFunction const& value, uint_fast64_t exponent) { + return carl::pow(value, exponent); + } + + template<> + RationalFunction simplify(RationalFunction value) { + value.simplify(); + return value; + } + + template<> + RationalFunction& simplify(RationalFunction& value) { + value.simplify(); + return value; + } + + template<> + RationalFunction&& simplify(RationalFunction&& value) { + value.simplify(); + return std::move(value); + } + + template<> + double convertNumber(RationalNumber const& number){ + return carl::toDouble(number); + } + + template<> + RationalNumber convertNumber(double const& number){ + return carl::rationalize(number); + } + + template<> + RationalFunction convertNumber(double const& number){ + return RationalFunction(carl::rationalize(number)); + } +// +// template<> +// storm::RationalNumber abs(storm::RationalNumber const& number) { +// return carl::abs(number); +// } + + template + storm::storage::MatrixEntry simplify(storm::storage::MatrixEntry matrixEntry) { + simplify(matrixEntry.getValue()); + return matrixEntry; + } + + template + storm::storage::MatrixEntry& simplify(storm::storage::MatrixEntry& matrixEntry) { + simplify(matrixEntry.getValue()); + return matrixEntry; + } + + template + storm::storage::MatrixEntry&& simplify(storm::storage::MatrixEntry&& matrixEntry) { + simplify(matrixEntry.getValue()); + return std::move(matrixEntry); + } + + } } diff --git a/src/utility/storm.h b/src/utility/storm.h index 49ef4bf04..6dd9dc526 100644 --- a/src/utility/storm.h +++ b/src/utility/storm.h @@ -243,7 +243,7 @@ namespace storm { case storm::settings::modules::CoreSettings::Engine::Sparse: { std::shared_ptr> sparseModel = model->template as>(); STORM_LOG_THROW(sparseModel != nullptr, storm::exceptions::InvalidArgumentException, "Sparse engine requires a sparse input model"); - return verifySparseModel(sparseModel, formula, onlyInitialStatesRelevant); + return (sparseModel, formula, onlyInitialStatesRelevant); } case storm::settings::modules::CoreSettings::Engine::Hybrid: { std::shared_ptr> ddModel = model->template as>(); diff --git a/src/utility/vector.h b/src/utility/vector.h index 6faf88c7c..e22564f08 100644 --- a/src/utility/vector.h +++ b/src/utility/vector.h @@ -12,7 +12,6 @@ #include #include "src/storage/BitVector.h" -#include "src/utility/constants.h" #include "src/utility/macros.h" #include "src/solver/OptimizationDirection.h" @@ -588,7 +587,7 @@ namespace storm { * @return True iff the elements are considered equal. */ template - bool equalModuloPrecision(T const& val1, T const& val2, T precision, bool relativeError = true) { + bool equalModuloPrecision(T const& val1, T const& val2, T const& precision, bool relativeError = true) { if (relativeError) { if (val2 == 0) { return (storm::utility::abs(val1) <= precision); @@ -612,7 +611,7 @@ namespace storm { * @param relativeError If set, the difference between the vectors is computed relative to the value or in absolute terms. */ template - bool equalModuloPrecision(std::vector const& vectorLeft, std::vector const& vectorRight, T precision, bool relativeError) { + bool equalModuloPrecision(std::vector const& vectorLeft, std::vector const& vectorRight, T const& precision, bool relativeError) { STORM_LOG_ASSERT(vectorLeft.size() == vectorRight.size(), "Lengths of vectors does not match."); for (uint_fast64_t i = 0; i < vectorLeft.size(); ++i) { @@ -636,7 +635,7 @@ namespace storm { * @param relativeError If set, the difference between the vectors is computed relative to the value or in absolute terms. */ template - bool equalModuloPrecision(std::vector const& vectorLeft, std::vector const& vectorRight, std::vector const& positions, T precision, bool relativeError) { + bool equalModuloPrecision(std::vector const& vectorLeft, std::vector const& vectorRight, std::vector const& positions, T const& precision, bool relativeError) { STORM_LOG_ASSERT(vectorLeft.size() == vectorRight.size(), "Lengths of vectors does not match."); for (uint_fast64_t position : positions) {