From 632c9c2e1e7cdfe36aba1287788021261671164f Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Fri, 13 Mar 2020 16:29:58 +0100 Subject: [PATCH] Modified the modernjson library so that it can parse numbers as rationals. --- resources/3rdparty/modernjson/src/json.hpp | 178 +++++++++++++++------ src/storm/adapters/JsonAdapter.h | 9 ++ src/storm/utility/constants.cpp | 6 + 3 files changed, 144 insertions(+), 49 deletions(-) create mode 100644 src/storm/adapters/JsonAdapter.h diff --git a/resources/3rdparty/modernjson/src/json.hpp b/resources/3rdparty/modernjson/src/json.hpp index 1b279a804..e98b57a40 100755 --- a/resources/3rdparty/modernjson/src/json.hpp +++ b/resources/3rdparty/modernjson/src/json.hpp @@ -26,9 +26,19 @@ OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. */ +/* + * This version has been adapted by the Storm developers so that we are able to parse + * floating point numbers using exact arithmetic. The major changes are: + * * A json_value now stores the number_float as a pointer. + * * Conversion operations between number representations are done using storm's utility functions. + */ + #ifndef NLOHMANN_JSON_HPP #define NLOHMANN_JSON_HPP +#include "storm/utility/constants.h" +#include "storm/utility/macros.h" + #include // all_of, for_each, transform #include // array #include // assert @@ -142,6 +152,29 @@ and fractional parts. } }; + + template + void float_to_stream(std::ostream& o, ValueType const& number) { + if (storm::utility::isZero(number)) + { + // special case for zero to get "0.0"/"-0.0" + o << (std::signbit(number) ? "-0.0" : "0.0"); + } + else + { + o << number; + } + } + + template <> + void float_to_stream(std::ostream& o, storm::RationalNumber const& number) { + auto result = storm::utility::to_string(storm::utility::convertNumber(number)); + // Parse the result again to check for accuracy + auto compare = storm::utility::convertNumber(result); + STORM_LOG_WARN_COND(compare == number, "Inaccurate JSON export: During export, the number " << number << " will be rounded to " << result << "."); + o << result; + } + } /*! @@ -826,8 +859,8 @@ Format](http://rfc7159.net/rfc7159) number_integer_t number_integer; /// number (unsigned integer) number_unsigned_t number_unsigned; - /// number (floating-point) - number_float_t number_float; + /// number (floating-point, stored with pointer to save storage) + number_float_t* number_float; /// default constructor (for null values) json_value() = default; @@ -837,8 +870,7 @@ Format](http://rfc7159.net/rfc7159) json_value(number_integer_t v) noexcept : number_integer(v) {} /// constructor for numbers (unsigned) json_value(number_unsigned_t v) noexcept : number_unsigned(v) {} - /// constructor for numbers (floating-point) - json_value(number_float_t v) noexcept : number_float(v) {} + /// constructor for empty values of a given type json_value(value_t t) { @@ -882,7 +914,7 @@ Format](http://rfc7159.net/rfc7159) case value_t::number_float: { - number_float = number_float_t(0.0); + number_float = create(storm::utility::zero()); break; } @@ -893,6 +925,12 @@ Format](http://rfc7159.net/rfc7159) } } + /// constructor for strings + json_value(const number_float_t & value) + { + number_float = create(value); + } + /// constructor for strings json_value(const string_t& value) { @@ -1516,7 +1554,7 @@ Format](http://rfc7159.net/rfc7159) : m_type(value_t::number_float), m_value(val) { // replace infinity and NAN by null - if (not std::isfinite(val)) + if (storm::utility::isInfinity(val)) { m_type = value_t::null; m_value = json_value(); @@ -1880,7 +1918,7 @@ Format](http://rfc7159.net/rfc7159) case value_t::number_float: { - m_value.number_float = first.m_object->m_value.number_float; + m_value = *first.m_object->m_value.number_float; break; } @@ -2024,7 +2062,7 @@ Format](http://rfc7159.net/rfc7159) case value_t::number_float: { - m_value = other.m_value.number_float; + m_value = *other.m_value.number_float; break; } @@ -2131,6 +2169,15 @@ Format](http://rfc7159.net/rfc7159) switch (m_type) { + + case value_t::number_float: + { + AllocatorType alloc; + alloc.destroy(m_value.number_float); + alloc.deallocate(m_value.number_float, 1); + break; + } + case value_t::object: { AllocatorType alloc; @@ -2208,7 +2255,8 @@ Format](http://rfc7159.net/rfc7159) // string->float->string, string->double->string or string->long // double->string; to be safe, we read this value from // std::numeric_limits::digits10 - ss.precision(std::numeric_limits::digits10); + // Note that other libraries need to be able to read this, so we just stick to the standard double precision. + ss.precision(std::numeric_limits::max_digits10 + 2); if (indent >= 0) { @@ -2724,7 +2772,34 @@ Format](http://rfc7159.net/rfc7159) case value_t::number_float: { - return static_cast(m_value.number_float); + static_assert(!std::is_same::value, "why is this int?"); + return storm::utility::convertNumber(*m_value.number_float); + } + + default: + { + throw std::domain_error("type must be number, but is " + type_name()); + } + } + } + + /// get a rational number (explicit) + storm::RationalNumber get_impl(storm::RationalNumber*) const { + switch (m_type) + { + case value_t::number_integer: + { + return storm::utility::convertNumber(m_value.number_integer); + } + + case value_t::number_unsigned: + { + return storm::utility::convertNumber(m_value.number_unsigned); + } + + case value_t::number_float: + { + return storm::utility::convertNumber(*m_value.number_float); } default: @@ -2817,13 +2892,13 @@ Format](http://rfc7159.net/rfc7159) /// get a pointer to the value (floating-point number) number_float_t* get_impl_ptr(number_float_t*) noexcept { - return is_number_float() ? &m_value.number_float : nullptr; + return is_number_float() ? m_value.number_float : nullptr; } /// get a pointer to the value (floating-point number) constexpr const number_float_t* get_impl_ptr(const number_float_t*) const noexcept { - return is_number_float() ? &m_value.number_float : nullptr; + return is_number_float() ? m_value.number_float : nullptr; } /*! @@ -3948,6 +4023,12 @@ Format](http://rfc7159.net/rfc7159) { case value_t::boolean: case value_t::number_float: + if (is_number_float()) { + AllocatorType alloc; + alloc.destroy(m_value.number_float); + alloc.deallocate(m_value.number_float, 1); + m_value.number_float = nullptr; + } case value_t::number_integer: case value_t::number_unsigned: case value_t::string: @@ -4055,6 +4136,12 @@ Format](http://rfc7159.net/rfc7159) { case value_t::boolean: case value_t::number_float: + if (is_number_float()) { + AllocatorType alloc; + alloc.destroy(m_value.number_float); + alloc.deallocate(m_value.number_float, 1); + m_value.number_float = nullptr; + } case value_t::number_integer: case value_t::number_unsigned: case value_t::string: @@ -4834,7 +4921,7 @@ Format](http://rfc7159.net/rfc7159) case value_t::number_float: { - m_value.number_float = 0.0; + *m_value.number_float = storm::utility::zero(); break; } @@ -5494,7 +5581,7 @@ Format](http://rfc7159.net/rfc7159) } case value_t::number_float: { - return lhs.m_value.number_float == rhs.m_value.number_float; + return *lhs.m_value.number_float == *rhs.m_value.number_float; } default: { @@ -5504,19 +5591,19 @@ Format](http://rfc7159.net/rfc7159) } else if (lhs_type == value_t::number_integer and rhs_type == value_t::number_float) { - return static_cast(lhs.m_value.number_integer) == rhs.m_value.number_float; + return storm::utility::convertNumber(lhs.m_value.number_integer) == *rhs.m_value.number_float; } else if (lhs_type == value_t::number_float and rhs_type == value_t::number_integer) { - return lhs.m_value.number_float == static_cast(rhs.m_value.number_integer); + return *lhs.m_value.number_float == storm::utility::convertNumber(rhs.m_value.number_integer); } else if (lhs_type == value_t::number_unsigned and rhs_type == value_t::number_float) { - return static_cast(lhs.m_value.number_unsigned) == rhs.m_value.number_float; + return storm::utility::convertNumber(lhs.m_value.number_unsigned) == *rhs.m_value.number_float; } else if (lhs_type == value_t::number_float and rhs_type == value_t::number_unsigned) { - return lhs.m_value.number_float == static_cast(rhs.m_value.number_unsigned); + return *lhs.m_value.number_float == storm::utility::convertNumber(rhs.m_value.number_unsigned); } else if (lhs_type == value_t::number_unsigned and rhs_type == value_t::number_integer) { @@ -5679,7 +5766,7 @@ Format](http://rfc7159.net/rfc7159) } case value_t::number_float: { - return lhs.m_value.number_float < rhs.m_value.number_float; + return *lhs.m_value.number_float < *rhs.m_value.number_float; } default: { @@ -5689,19 +5776,19 @@ Format](http://rfc7159.net/rfc7159) } else if (lhs_type == value_t::number_integer and rhs_type == value_t::number_float) { - return static_cast(lhs.m_value.number_integer) < rhs.m_value.number_float; + return storm::utility::convertNumber(lhs.m_value.number_integer) < *rhs.m_value.number_float; } else if (lhs_type == value_t::number_float and rhs_type == value_t::number_integer) { - return lhs.m_value.number_float < static_cast(rhs.m_value.number_integer); + return *lhs.m_value.number_float < storm::utility::convertNumber(rhs.m_value.number_integer); } else if (lhs_type == value_t::number_unsigned and rhs_type == value_t::number_float) { - return static_cast(lhs.m_value.number_unsigned) < rhs.m_value.number_float; + return storm::utility::convertNumber(lhs.m_value.number_unsigned) < *rhs.m_value.number_float; } else if (lhs_type == value_t::number_float and rhs_type == value_t::number_unsigned) { - return lhs.m_value.number_float < static_cast(rhs.m_value.number_unsigned); + return *lhs.m_value.number_float < storm::utility::convertNumber(rhs.m_value.number_unsigned); } else if (lhs_type == value_t::number_integer and rhs_type == value_t::number_unsigned) { @@ -6476,15 +6563,7 @@ Format](http://rfc7159.net/rfc7159) case value_t::number_float: { - if (m_value.number_float == 0) - { - // special case for zero to get "0.0"/"-0.0" - o << (std::signbit(m_value.number_float) ? "-0.0" : "0.0"); - } - else - { - o << m_value.number_float; - } + float_to_stream(o, *m_value.number_float); return; } @@ -8972,14 +9051,17 @@ Format](http://rfc7159.net/rfc7159) @param[in] type the @ref number_float_t in use - @param[in,out] endptr recieves a pointer to the first character after - the number - @return the floating point number */ - long double str_to_float_t(long double* /* type */, char** endptr) const + template + FloatValueType str_to_float_t(FloatValueType* /* type */) const { + return storm::utility::convertNumber(std::string(reinterpret_cast(m_start))); + } + + template <> + long double str_to_float_t(long double* /* type */) const { - return std::strtold(reinterpret_cast(m_start), endptr); + return std::strtold(reinterpret_cast(m_start), NULL); } /*! @@ -8992,14 +9074,12 @@ Format](http://rfc7159.net/rfc7159) @param[in] type the @ref number_float_t in use - @param[in,out] endptr recieves a pointer to the first character after - the number - @return the floating point number */ - double str_to_float_t(double* /* type */, char** endptr) const + template <> + double str_to_float_t(double* /* type */) const { - return std::strtod(reinterpret_cast(m_start), endptr); + return std::strtod(reinterpret_cast(m_start), NULL); } /*! @@ -9012,15 +9092,15 @@ Format](http://rfc7159.net/rfc7159) @param[in] type the @ref number_float_t in use - @param[in,out] endptr recieves a pointer to the first character after - the number @return the floating point number */ - float str_to_float_t(float* /* type */, char** endptr) const + template <> + float str_to_float_t(float* /* type */) const { - return std::strtof(reinterpret_cast(m_start), endptr); + return std::strtof(reinterpret_cast(m_start), NULL); } + /*! @brief return number value for number tokens @@ -9120,11 +9200,11 @@ Format](http://rfc7159.net/rfc7159) } else { - // parse with strtod - result.m_value.number_float = str_to_float_t(static_cast(nullptr), NULL); + // parse float + result.m_value = basic_json::json_value(str_to_float_t(static_cast(nullptr))); // replace infinity and NAN by null - if (not std::isfinite(result.m_value.number_float)) + if (storm::utility::isInfinity(*result.m_value.number_float)) { type = value_t::null; result.m_value = basic_json::json_value(); diff --git a/src/storm/adapters/JsonAdapter.h b/src/storm/adapters/JsonAdapter.h new file mode 100644 index 000000000..5cc3e4975 --- /dev/null +++ b/src/storm/adapters/JsonAdapter.h @@ -0,0 +1,9 @@ +#pragma once + +// Modernjson JSON parser +#include "json.hpp" + +namespace storm { + template + using json = nlohmann::basic_json; +} diff --git a/src/storm/utility/constants.cpp b/src/storm/utility/constants.cpp index eeff62ad3..1b2bdff97 100644 --- a/src/storm/utility/constants.cpp +++ b/src/storm/utility/constants.cpp @@ -105,6 +105,11 @@ namespace storm { return std::llround(number); } + template<> + int_fast64_t convertNumber(double const& number){ + return std::llround(number); + } + template<> double convertNumber(uint_fast64_t const& number){ return number; @@ -285,6 +290,7 @@ namespace storm { template std::string to_string(ValueType const& value) { std::stringstream ss; + ss.precision(std::numeric_limits::max_digits10 + 2); ss << value; return ss.str(); }