sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

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.
main
Tim Quatmann 4 years ago
parent
c5bbf68eaf
commit
f0378363bb
No known key found for this signature in database GPG Key ID: 6EDE19592731EEC3
4 changed files with 100 additions and 231 deletions
Unified View
  1. 6
      src/storm/storage/Distribution.h
  2. 7
      src/storm/storage/DistributionWithReward.h
  3. 201
      src/storm/utility/ConstantsComparator.cpp
  4. 117
      src/storm/utility/ConstantsComparator.h

6
src/storm/storage/Distribution.h
View File

@ -6,12 +6,10 @@
#include <boost/container/flat_map.hpp> #include <boost/container/flat_map.hpp>
#include "storm/storage/sparse/StateType.h" #include "storm/storage/sparse/StateType.h"
#include "storm/utility/ConstantsComparator.h"
namespace storm { namespace storm {
namespace utility {
template <typename ValueType>
class ConstantsComparator;
}
namespace storage { namespace storage {

7
src/storm/storage/DistributionWithReward.h
View File

@ -3,13 +3,10 @@
#include "storm/storage/Distribution.h" #include "storm/storage/Distribution.h"
#include "storm/utility/constants.h" #include "storm/utility/constants.h"
#include "storm/utility/ConstantsComparator.h"
namespace storm { namespace storm {
namespace utility {
template <typename ValueType>
class ConstantsComparator;
}
namespace storage { namespace storage {
template<typename ValueType, typename StateType = uint32_t> template<typename ValueType, typename StateType = uint32_t>

201
src/storm/utility/ConstantsComparator.cpp
View File

@ -1,160 +1,99 @@
#include "storm/utility/ConstantsComparator.h" #include "storm/utility/ConstantsComparator.h"
#include <cstdlib>
#include <cmath>
#include "storm/storage/sparse/StateType.h" #include "storm/storage/sparse/StateType.h"
#include "storm/utility/constants.h"
#include "storm/settings/SettingsManager.h" #include "storm/settings/SettingsManager.h"
#include "storm/settings/modules/GeneralSettings.h" #include "storm/settings/modules/GeneralSettings.h"
#include "storm/utility/NumberTraits.h"
#include "storm/utility/constants.h"
namespace storm { namespace storm {
namespace utility { namespace utility {
template<typename ValueType> template<typename ValueType, typename Enable>
bool ConstantsComparator<ValueType>::isOne(ValueType const& value) const { bool ConstantsComparator<ValueType, Enable>::isOne(ValueType const& value) const {
return storm::utility::isOne(value); return isEqual(value, storm::utility::one<ValueType>());
} }
template<typename ValueType, typename Enable>
template<typename ValueType> bool ConstantsComparator<ValueType, Enable>::isZero(ValueType const& value) const {
bool ConstantsComparator<ValueType>::isZero(ValueType const& value) const { return isEqual(value, storm::utility::zero<ValueType>());
return storm::utility::isZero(value);
} }
template<typename ValueType, typename Enable>
template<typename ValueType> bool ConstantsComparator<ValueType, Enable>::isEqual(ValueType const& value1, ValueType const& value2) const {
bool ConstantsComparator<ValueType>::isEqual(ValueType const& value1, ValueType const& value2) const {
return value1 == value2; return value1 == value2;
} }
template<typename ValueType, typename Enable>
template<typename ValueType> bool ConstantsComparator<ValueType, Enable>::isConstant(ValueType const& value) const {
bool ConstantsComparator<ValueType>::isConstant(ValueType const& value) const {
return storm::utility::isConstant(value); return storm::utility::isConstant(value);
} }
template<typename ValueType> template<typename ValueType, typename Enable>
bool ConstantsComparator<ValueType>::isInfinity(ValueType const&) const { bool ConstantsComparator<ValueType, Enable>::isLess(ValueType const& value1, ValueType const& value2) const {
return false;
}
template<typename ValueType>
bool ConstantsComparator<ValueType>::isLess(ValueType const& value1, ValueType const& value2) const {
return value1 < value2; return value1 < value2;
} }
template<typename ValueType>
ConstantsComparator<float>::ConstantsComparator() : precision(static_cast<float>(storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision())) { ConstantsComparator<ValueType, ConstantsComparatorEnablePrecision<ValueType>>::ConstantsComparator()
// Intentionally left empty. : ConstantsComparator(
} storm::NumberTraits<ValueType>::IsExact
? storm::utility::zero<ValueType>()
ConstantsComparator<float>::ConstantsComparator(float precision) : precision(precision) { : storm::utility::convertNumber<ValueType>(storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision())) {
// Intentionally left empty. // Intentionally left empty
}
bool ConstantsComparator<float>::isOne(float const& value) const {
return std::abs(value - one<float>()) <= precision;
}
bool ConstantsComparator<float>::isZero(float const& value) const {
return std::abs(value) <= precision;
}
bool ConstantsComparator<float>::isEqual(float const& value1, float const& value2) const {
return std::abs(value1 - value2) <= precision;
}
bool ConstantsComparator<float>::isConstant(float const&) const {
return true;
}
bool ConstantsComparator<float>::isInfinity(float const& value) const {
return value == storm::utility::infinity<float>();
}
bool ConstantsComparator<float>::isLess(float const& value1, float const& value2) const {
return std::abs(value1 - value2) < precision;
}
ConstantsComparator<double>::ConstantsComparator() : precision(storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision()), relative(false) {
// Intentionally left empty.
}
ConstantsComparator<double>::ConstantsComparator(double precision, bool relative) : precision(precision), relative(relative) {
// Intentionally left empty.
}
bool ConstantsComparator<double>::isOne(double const& value) const {
return std::abs(value - one<double>()) <= precision;
}
bool ConstantsComparator<double>::isZero(double const& value) const {
return std::abs(value) <= precision;
}
bool ConstantsComparator<double>::isInfinity(double const& value) const {
return value == infinity<double>();
}
bool ConstantsComparator<double>::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<double>::isConstant(double const&) const {
return true;
}
bool ConstantsComparator<double>::isLess(double const& value1, double const& value2) const {
return value1 < value2 - precision;
}
ConstantsComparator<storm::RationalNumber>::ConstantsComparator() : precision(storm::utility::zero<storm::RationalNumber>()), relative(false) {
// Intentionally left empty.
} }
template<typename ValueType>
ConstantsComparator<storm::RationalNumber>::ConstantsComparator(storm::RationalNumber precision, bool relative) : precision(precision), relative(relative) { ConstantsComparator<ValueType, ConstantsComparatorEnablePrecision<ValueType>>::ConstantsComparator(ValueType const& precision, bool const& relative)
// Intentionally left empty. : precision(precision), relative(relative) {
// Intentionally left empty
} }
template<typename ValueType>
bool ConstantsComparator<storm::RationalNumber>::isOne(storm::RationalNumber const& value) const { bool ConstantsComparator<ValueType, ConstantsComparatorEnablePrecision<ValueType>>::isOne(ValueType const& value) const {
if (storm::utility::isZero(precision)) { return isEqual(value, storm::utility::one<ValueType>());
return storm::utility::isOne(value);
}
return storm::utility::abs(storm::RationalNumber(value - one<storm::RationalNumber>())) <= precision;
} }
template<typename ValueType>
bool ConstantsComparator<storm::RationalNumber>::isZero(storm::RationalNumber const& value) const { bool ConstantsComparator<ValueType, ConstantsComparatorEnablePrecision<ValueType>>::isZero(ValueType const& value) const {
if (storm::utility::isZero(precision)) { return isEqual(value, storm::utility::zero<ValueType>());
return storm::utility::isZero(value);
}
return storm::utility::abs(value) <= precision;
} }
template<typename ValueType>
bool ConstantsComparator<storm::RationalNumber>::isEqual(storm::RationalNumber const& value1, storm::RationalNumber const& value2) const { bool ConstantsComparator<ValueType, ConstantsComparatorEnablePrecision<ValueType>>::isEqual(ValueType const& value1, ValueType const& value2) const {
if (storm::utility::isZero(precision)) { if (value1 == value2) {
return value1 == value2; return true;
} } else if (storm::utility::isZero(precision)) {
return false;
if (relative) {
return value1 == value2 || storm::utility::abs(storm::RationalNumber(value1 - value2))/storm::utility::abs(storm::RationalNumber(value1 + value2)) <= precision;
} else { } else {
return storm::utility::abs(storm::RationalNumber(value1 - value2)) <= precision; ValueType absDiff = storm::utility::abs<ValueType>(value1 - value2);
if (relative) {
return absDiff <= precision * (storm::utility::abs(value1) + storm::utility::abs(value2));
} else {
return absDiff <= precision;
}
} }
} }
template<typename ValueType>
bool ConstantsComparator<storm::RationalNumber>::isConstant(storm::RationalNumber const&) const { bool ConstantsComparator<ValueType, ConstantsComparatorEnablePrecision<ValueType>>::isConstant(ValueType const& value) const {
return true; return storm::utility::isConstant(value);
} }
template<typename ValueType>
bool ConstantsComparator<storm::RationalNumber>::isInfinity(storm::RationalNumber const&) const { bool ConstantsComparator<ValueType, ConstantsComparatorEnablePrecision<ValueType>>::isInfinity(ValueType const& value) const {
return false; return storm::utility::isInfinity(value);
} }
template<typename ValueType>
bool ConstantsComparator<storm::RationalNumber>::isLess(storm::RationalNumber const& value1, storm::RationalNumber const& value2) const { bool ConstantsComparator<ValueType, ConstantsComparatorEnablePrecision<ValueType>>::isLess(ValueType const& value1, ValueType const& value2) const {
return value1 < value2 - precision; return value1 < value2 - precision;
} }
// Explicit instantiations. // Explicit instantiations.
template class ConstantsComparator<double>;
template class ConstantsComparator<float>;
template class ConstantsComparator<int>; template class ConstantsComparator<int>;
template class ConstantsComparator<storm::storage::sparse::state_type>; template class ConstantsComparator<storm::storage::sparse::state_type>;
@ -162,14 +101,14 @@ namespace storm {
#if defined(STORM_HAVE_CLN) #if defined(STORM_HAVE_CLN)
template class ConstantsComparator<ClnRationalNumber>; template class ConstantsComparator<ClnRationalNumber>;
#endif #endif
#if defined(STORM_HAVE_GMP) #if defined(STORM_HAVE_GMP)
template class ConstantsComparator<GmpRationalNumber>; template class ConstantsComparator<GmpRationalNumber>;
#endif #endif
template class ConstantsComparator<RationalFunction>; template class ConstantsComparator<RationalFunction>;
template class ConstantsComparator<Polynomial>; template class ConstantsComparator<Polynomial>;
template class ConstantsComparator<Interval>; template class ConstantsComparator<Interval>;
#endif #endif
} } // namespace utility
} } // namespace storm

117
src/storm/utility/ConstantsComparator.h
View File

@ -1,108 +1,43 @@
#ifndef STORM_UTILITY_CONSTANTSCOMPARATOR_H_ #pragma once
#define STORM_UTILITY_CONSTANTSCOMPARATOR_H_
#include "storm/adapters/RationalFunctionAdapter.h" #include <type_traits>
#include "storm/adapters/RationalNumberAdapter.h"
namespace storm { namespace storm {
namespace utility { namespace utility {
// A class that can be used for comparing constants. // A class that can be used for comparing constants.
template<typename ValueType> template<typename ValueType, typename Enable = void>
class ConstantsComparator { class ConstantsComparator {
public: public:
// This needs to be in here, otherwise the template specializations are not used properly.
ConstantsComparator() = default; ConstantsComparator() = default;
bool isOne(ValueType const& value) const; bool isOne(ValueType const& value) const;
bool isZero(ValueType const& value) const; bool isZero(ValueType const& value) const;
bool isEqual(ValueType const& value1, ValueType const& value2) const; bool isEqual(ValueType const& value1, ValueType const& value2) const;
bool isConstant(ValueType const& value) const; bool isConstant(ValueType const& value) const;
bool isInfinity(ValueType const& value) const;
bool isLess(ValueType const& value1, ValueType const& value2) 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<float> {
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; // Specialization for numbers where there can be a precision
template<typename ValueType>
private: using ConstantsComparatorEnablePrecision =
// The precision used for comparisons. typename std::enable_if_t<std::is_same<ValueType, double>::value || std::is_same<ValueType, storm::RationalNumber>::value>;
float precision; template<typename ValueType>
}; class ConstantsComparator<ValueType, ConstantsComparatorEnablePrecision<ValueType>> {
public:
// For doubles we specialize this class and consider the comparison modulo some predefined precision.
template<>
class ConstantsComparator<double> {
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<storm::RationalNumber> {
public:
ConstantsComparator(); ConstantsComparator();
ConstantsComparator(ValueType const& precision, bool const& relative = false);
ConstantsComparator(storm::RationalNumber precision, bool relative); bool isOne(ValueType const& value) const;
bool isZero(ValueType const& value) const;
bool isOne(storm::RationalNumber const& value) const; bool isEqual(ValueType const& value1, ValueType const& value2) const;
bool isConstant(ValueType const& value) const;
bool isZero(storm::RationalNumber const& value) const; bool isInfinity(ValueType const& value) const;
bool isLess(ValueType const& value1, ValueType const& value2) const;
bool isEqual(storm::RationalNumber const& value1, storm::RationalNumber const& value2) const; private:
ValueType precision;
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;
bool relative; bool relative;
}; };
} } // namespace utility
} } // namespace storm
#endif /* STORM_UTILITY_CONSTANTSCOMPARATOR_H_ */
Write Preview
|||||||
100:0
Loading…
Cancel
Save