diff --git a/src/storm/builder/ExplicitModelBuilder.h b/src/storm/builder/ExplicitModelBuilder.h index f33b37ba3..cb537eb52 100644 --- a/src/storm/builder/ExplicitModelBuilder.h +++ b/src/storm/builder/ExplicitModelBuilder.h @@ -32,9 +32,6 @@ #include "storm/generator/VariableInformation.h" namespace storm { - namespace utility { - template class ConstantsComparator; - } namespace builder { diff --git a/src/storm/storage/Distribution.h b/src/storm/storage/Distribution.h index c3ac58dcc..761aa214f 100644 --- a/src/storm/storage/Distribution.h +++ b/src/storm/storage/Distribution.h @@ -6,12 +6,10 @@ #include #include "storm/storage/sparse/StateType.h" +#include "storm/utility/ConstantsComparator.h" namespace storm { - namespace utility { - template - class ConstantsComparator; - } + namespace storage { diff --git a/src/storm/storage/DistributionWithReward.h b/src/storm/storage/DistributionWithReward.h index d830b89e2..43c4e8bf7 100644 --- a/src/storm/storage/DistributionWithReward.h +++ b/src/storm/storage/DistributionWithReward.h @@ -3,13 +3,10 @@ #include "storm/storage/Distribution.h" #include "storm/utility/constants.h" +#include "storm/utility/ConstantsComparator.h" namespace storm { - namespace utility { - template - class ConstantsComparator; - } - + namespace storage { template diff --git a/src/storm/storage/bisimulation/BisimulationDecomposition.h b/src/storm/storage/bisimulation/BisimulationDecomposition.h index 7e8d871fa..14b32ecd0 100644 --- a/src/storm/storage/bisimulation/BisimulationDecomposition.h +++ b/src/storm/storage/bisimulation/BisimulationDecomposition.h @@ -16,10 +16,6 @@ #include "storm/utility/ConstantsComparator.h" namespace storm { - namespace utility { - template class ConstantsComparator; - } - namespace logic { class Formula; } diff --git a/src/storm/storage/bisimulation/DeterministicModelBisimulationDecomposition.h b/src/storm/storage/bisimulation/DeterministicModelBisimulationDecomposition.h index 0605474bb..be296af9e 100644 --- a/src/storm/storage/bisimulation/DeterministicModelBisimulationDecomposition.h +++ b/src/storm/storage/bisimulation/DeterministicModelBisimulationDecomposition.h @@ -5,10 +5,6 @@ #include "storm/storage/bisimulation/DeterministicBlockData.h" namespace storm { - namespace utility { - template class ConstantsComparator; - } - namespace storage { /*! diff --git a/src/storm/storage/bisimulation/NondeterministicModelBisimulationDecomposition.h b/src/storm/storage/bisimulation/NondeterministicModelBisimulationDecomposition.h index f42415c49..3afc68b54 100644 --- a/src/storm/storage/bisimulation/NondeterministicModelBisimulationDecomposition.h +++ b/src/storm/storage/bisimulation/NondeterministicModelBisimulationDecomposition.h @@ -7,10 +7,6 @@ #include "storm/storage/DistributionWithReward.h" namespace storm { - namespace utility { - template class ConstantsComparator; - } - namespace storage { /*! diff --git a/src/storm/utility/ConstantsComparator.cpp b/src/storm/utility/ConstantsComparator.cpp index a7f9b9609..382847f4b 100644 --- a/src/storm/utility/ConstantsComparator.cpp +++ b/src/storm/utility/ConstantsComparator.cpp @@ -1,160 +1,99 @@ #include "storm/utility/ConstantsComparator.h" -#include -#include #include "storm/storage/sparse/StateType.h" -#include "storm/utility/constants.h" #include "storm/settings/SettingsManager.h" #include "storm/settings/modules/GeneralSettings.h" +#include "storm/utility/NumberTraits.h" +#include "storm/utility/constants.h" namespace storm { namespace utility { - template - bool ConstantsComparator::isOne(ValueType const& value) const { - return storm::utility::isOne(value); + + template + bool ConstantsComparator::isOne(ValueType const& value) const { + return isEqual(value, storm::utility::one()); } - - template - bool ConstantsComparator::isZero(ValueType const& value) const { - return storm::utility::isZero(value); + + template + bool ConstantsComparator::isZero(ValueType const& value) const { + return isEqual(value, storm::utility::zero()); } - - template - bool ConstantsComparator::isEqual(ValueType const& value1, ValueType const& value2) const { + + template + bool ConstantsComparator::isEqual(ValueType const& value1, ValueType const& value2) const { return value1 == value2; } - - template - bool ConstantsComparator::isConstant(ValueType const& value) const { + + template + bool ConstantsComparator::isConstant(ValueType const& value) const { return storm::utility::isConstant(value); } - template - bool ConstantsComparator::isInfinity(ValueType const&) const { - return false; - } - - template - bool ConstantsComparator::isLess(ValueType const& value1, ValueType const& value2) const { + template + bool ConstantsComparator::isLess(ValueType const& value1, ValueType const& value2) const { return value1 < value2; } - - ConstantsComparator::ConstantsComparator() : precision(static_cast(storm::settings::getModule().getPrecision())) { - // Intentionally left empty. - } - - ConstantsComparator::ConstantsComparator(float precision) : precision(precision) { - // Intentionally left empty. - } - - bool ConstantsComparator::isOne(float const& value) const { - return std::abs(value - one()) <= precision; - } - - bool ConstantsComparator::isZero(float const& value) const { - return std::abs(value) <= precision; - } - - bool ConstantsComparator::isEqual(float const& value1, float const& value2) const { - return std::abs(value1 - value2) <= precision; - } - - bool ConstantsComparator::isConstant(float const&) const { - return true; - } - - bool ConstantsComparator::isInfinity(float const& value) const { - return value == storm::utility::infinity(); - } - - bool ConstantsComparator::isLess(float const& value1, float const& value2) const { - return std::abs(value1 - value2) < precision; - } - - ConstantsComparator::ConstantsComparator() : precision(storm::settings::getModule().getPrecision()), relative(false) { - // Intentionally left empty. - } - - ConstantsComparator::ConstantsComparator(double precision, bool relative) : precision(precision), relative(relative) { - // Intentionally left empty. - } - - bool ConstantsComparator::isOne(double const& value) const { - return std::abs(value - one()) <= precision; - } - - bool ConstantsComparator::isZero(double const& value) const { - return std::abs(value) <= precision; - } - - bool ConstantsComparator::isInfinity(double const& value) const { - return value == infinity(); - } - - bool ConstantsComparator::isEqual(double const& value1, double const& value2) const { - if (relative) { - return value1 == value2 || std::abs(value1 - value2)/std::abs(value1 + value2) <= precision; - } else { - return std::abs(value1 - value2) <= precision; - } - } - - bool ConstantsComparator::isConstant(double const&) const { - return true; - } - - bool ConstantsComparator::isLess(double const& value1, double const& value2) const { - return value1 < value2 - precision; - } - - ConstantsComparator::ConstantsComparator() : precision(storm::utility::zero()), relative(false) { - // Intentionally left empty. + + template + ConstantsComparator>::ConstantsComparator() + : ConstantsComparator( + storm::NumberTraits::IsExact + ? storm::utility::zero() + : storm::utility::convertNumber(storm::settings::getModule().getPrecision())) { + // Intentionally left empty } - - ConstantsComparator::ConstantsComparator(storm::RationalNumber precision, bool relative) : precision(precision), relative(relative) { - // Intentionally left empty. + + template + ConstantsComparator>::ConstantsComparator(ValueType const& precision, bool const& relative) + : precision(precision), relative(relative) { + // Intentionally left empty } - - bool ConstantsComparator::isOne(storm::RationalNumber const& value) const { - if (storm::utility::isZero(precision)) { - return storm::utility::isOne(value); - } - return storm::utility::abs(storm::RationalNumber(value - one())) <= precision; + + template + bool ConstantsComparator>::isOne(ValueType const& value) const { + return isEqual(value, storm::utility::one()); } - - bool ConstantsComparator::isZero(storm::RationalNumber const& value) const { - if (storm::utility::isZero(precision)) { - return storm::utility::isZero(value); - } - return storm::utility::abs(value) <= precision; + + template + bool ConstantsComparator>::isZero(ValueType const& value) const { + return isEqual(value, storm::utility::zero()); } - - bool ConstantsComparator::isEqual(storm::RationalNumber const& value1, storm::RationalNumber const& value2) const { - if (storm::utility::isZero(precision)) { - return value1 == value2; - } - - if (relative) { - return value1 == value2 || storm::utility::abs(storm::RationalNumber(value1 - value2))/storm::utility::abs(storm::RationalNumber(value1 + value2)) <= precision; + + template + bool ConstantsComparator>::isEqual(ValueType const& value1, ValueType const& value2) const { + if (value1 == value2) { + return true; + } else if (storm::utility::isZero(precision)) { + return false; } else { - return storm::utility::abs(storm::RationalNumber(value1 - value2)) <= precision; + ValueType absDiff = storm::utility::abs(value1 - value2); + if (relative) { + return absDiff <= precision * (storm::utility::abs(value1) + storm::utility::abs(value2)); + } else { + return absDiff <= precision; + } } } - - bool ConstantsComparator::isConstant(storm::RationalNumber const&) const { - return true; + + template + bool ConstantsComparator>::isConstant(ValueType const& value) const { + return storm::utility::isConstant(value); } - - bool ConstantsComparator::isInfinity(storm::RationalNumber const&) const { - return false; + + template + bool ConstantsComparator>::isInfinity(ValueType const& value) const { + return storm::utility::isInfinity(value); } - - bool ConstantsComparator::isLess(storm::RationalNumber const& value1, storm::RationalNumber const& value2) const { + + template + bool ConstantsComparator>::isLess(ValueType const& value1, ValueType const& value2) const { return value1 < value2 - precision; } - + // Explicit instantiations. + template class ConstantsComparator; + template class ConstantsComparator; template class ConstantsComparator; template class ConstantsComparator; @@ -162,14 +101,14 @@ namespace storm { #if defined(STORM_HAVE_CLN) template class ConstantsComparator; #endif - + #if defined(STORM_HAVE_GMP) template class ConstantsComparator; #endif - + template class ConstantsComparator; template class ConstantsComparator; template class ConstantsComparator; #endif - } -} + } // namespace utility +} // namespace storm diff --git a/src/storm/utility/ConstantsComparator.h b/src/storm/utility/ConstantsComparator.h index 99f7cd625..b38d2a288 100644 --- a/src/storm/utility/ConstantsComparator.h +++ b/src/storm/utility/ConstantsComparator.h @@ -1,108 +1,43 @@ -#ifndef STORM_UTILITY_CONSTANTSCOMPARATOR_H_ -#define STORM_UTILITY_CONSTANTSCOMPARATOR_H_ +#pragma once -#include "storm/adapters/RationalFunctionAdapter.h" +#include +#include "storm/adapters/RationalNumberAdapter.h" namespace storm { namespace utility { + // A class that can be used for comparing constants. - template + template class ConstantsComparator { - public: - // This needs to be in here, otherwise the template specializations are not used properly. + public: ConstantsComparator() = default; - bool isOne(ValueType const& value) const; - bool isZero(ValueType const& value) const; - bool isEqual(ValueType const& value1, ValueType const& value2) const; - bool isConstant(ValueType const& value) const; - - bool isInfinity(ValueType const& value) const; - bool isLess(ValueType const& value1, ValueType const& value2) const; }; - - // For floats we specialize this class and consider the comparison modulo some predefined precision. - template<> - class ConstantsComparator { - public: - ConstantsComparator(); - - ConstantsComparator(float precision); - - bool isOne(float const& value) const; - - bool isZero(float const& value) const; - - bool isEqual(float const& value1, float const& value2) const; - - bool isConstant(float const& value) const; - - bool isInfinity(float const& value) const; - bool isLess(float const& value1, float const& value2) const; - - private: - // The precision used for comparisons. - float precision; - }; - - // For doubles we specialize this class and consider the comparison modulo some predefined precision. - template<> - class ConstantsComparator { - public: - ConstantsComparator(); - - ConstantsComparator(double precision, bool relative = false); - - bool isOne(double const& value) const; - - bool isZero(double const& value) const; - - bool isInfinity(double const& value) const; - - bool isEqual(double const& value1, double const& value2) const; - - bool isConstant(double const& value) const; - - bool isLess(double const& value1, double const& value2) const; - - private: - // The precision used for comparisons. - double precision; - - // Whether to use relative comparison for equality. - bool relative; - }; - - // For rational numbers we specialize this class and consider the comparison modulo some predefined precision. - template<> - class ConstantsComparator { - public: + // Specialization for numbers where there can be a precision + template + using ConstantsComparatorEnablePrecision = + typename std::enable_if_t::value || std::is_same::value>; + + template + class ConstantsComparator> { + public: ConstantsComparator(); - - ConstantsComparator(storm::RationalNumber precision, bool relative); - - bool isOne(storm::RationalNumber const& value) const; - - bool isZero(storm::RationalNumber const& value) const; - - bool isEqual(storm::RationalNumber const& value1, storm::RationalNumber const& value2) const; - - bool isConstant(storm::RationalNumber const& value) const; - - bool isInfinity(storm::RationalNumber const& value) const; - - bool isLess(storm::RationalNumber const& value1, storm::RationalNumber const& value2) const; - - private: - storm::RationalNumber precision; + ConstantsComparator(ValueType const& precision, bool const& relative = false); + bool isOne(ValueType const& value) const; + bool isZero(ValueType const& value) const; + bool isEqual(ValueType const& value1, ValueType const& value2) const; + bool isConstant(ValueType const& value) const; + bool isInfinity(ValueType const& value) const; + bool isLess(ValueType const& value1, ValueType const& value2) const; + + private: + ValueType precision; bool relative; }; - } -} - -#endif /* STORM_UTILITY_CONSTANTSCOMPARATOR_H_ */ + } // namespace utility +} // namespace storm