From f0378363bbea5f82c2c7dadbd403510db949ff6f Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Mon, 10 May 2021 09:57:20 +0200 Subject: [PATCH] ConstantsComparator: reduced code duplications, fixed a potentially div by 0, and silenced a warning ConstantsComparator: The old code used `abs(x-y)/abs(x+y)<= epsilon` when comparing two numbers for equality (modulo relative precision). This is weird when x and y have different signs and potentially even causes a div by 0 whenever x=-y. Moreover the templating was awkward, causing a lot of code duplications and a Warning with clang. Distribution[WithReward]: replaced forward declarations of ConstantsComparator by actual includes as the forward declarations caused some ambiguity regarding the template parameters. --- src/storm/storage/Distribution.h | 6 +- src/storm/storage/DistributionWithReward.h | 7 +- src/storm/utility/ConstantsComparator.cpp | 201 +++++++-------------- src/storm/utility/ConstantsComparator.h | 117 +++--------- 4 files changed, 100 insertions(+), 231 deletions(-) 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/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