diff --git a/resources/3rdparty/sylvan/src/storm_wrapper.cpp b/resources/3rdparty/sylvan/src/storm_wrapper.cpp index 6d12a0825..5bfe580de 100644 --- a/resources/3rdparty/sylvan/src/storm_wrapper.cpp +++ b/resources/3rdparty/sylvan/src/storm_wrapper.cpp @@ -227,8 +227,11 @@ storm_rational_number_ptr storm_rational_number_mod(storm_rational_number_ptr a, storm::RationalNumber const& srn_a = *(storm::RationalNumber const*)a; storm::RationalNumber const& srn_b = *(storm::RationalNumber const*)b; - - throw storm::exceptions::InvalidOperationException() << "Modulo not supported for rational numbers."; + if (carl::isInteger(srn_a) && carl::isInteger(srn_b)) { + storm::RationalNumber* result_srn = new storm::RationalNumber(carl::mod(carl::getNum(srn_a), carl::getNum(srn_b))); + return (storm_rational_number_ptr)result_srn; + } + throw storm::exceptions::InvalidOperationException() << "Modulo not supported for rational, non-integer numbers."; } storm_rational_number_ptr storm_rational_number_min(storm_rational_number_ptr a, storm_rational_number_ptr b) { diff --git a/resources/3rdparty/sylvan/src/sylvan_obj_mtbdd_storm.hpp b/resources/3rdparty/sylvan/src/sylvan_obj_mtbdd_storm.hpp index d41976f5f..fc4ccf420 100644 --- a/resources/3rdparty/sylvan/src/sylvan_obj_mtbdd_storm.hpp +++ b/resources/3rdparty/sylvan/src/sylvan_obj_mtbdd_storm.hpp @@ -53,6 +53,7 @@ Mtbdd DivideRN(const Mtbdd &other) const; Mtbdd FloorRN() const; Mtbdd CeilRN() const; Mtbdd PowRN(const Mtbdd& other) const; +Mtbdd ModRN(const Mtbdd& other) const; Mtbdd MinimumRN() const; Mtbdd MaximumRN() const; diff --git a/resources/3rdparty/sylvan/src/sylvan_obj_storm.cpp b/resources/3rdparty/sylvan/src/sylvan_obj_storm.cpp index 0420d112c..c622637cf 100644 --- a/resources/3rdparty/sylvan/src/sylvan_obj_storm.cpp +++ b/resources/3rdparty/sylvan/src/sylvan_obj_storm.cpp @@ -315,6 +315,12 @@ Mtbdd::PowRN(const Mtbdd& other) const { return sylvan_storm_rational_number_pow(mtbdd, other.mtbdd); } +Mtbdd +Mtbdd::ModRN(const Mtbdd& other) const { + LACE_ME; + return sylvan_storm_rational_number_mod(mtbdd, other.mtbdd); +} + Mtbdd Mtbdd::MinimumRN() const { LACE_ME; diff --git a/src/storm/storage/dd/sylvan/InternalSylvanAdd.cpp b/src/storm/storage/dd/sylvan/InternalSylvanAdd.cpp index 5a3cdc954..a7c33d59e 100644 --- a/src/storm/storage/dd/sylvan/InternalSylvanAdd.cpp +++ b/src/storm/storage/dd/sylvan/InternalSylvanAdd.cpp @@ -328,8 +328,8 @@ namespace storm { } template<> - InternalAdd InternalAdd::mod(InternalAdd const&) const { - STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Operation (mod) not supported by rational numbers."); + InternalAdd InternalAdd::mod(InternalAdd const& other) const { + return InternalAdd(ddManager, this->sylvanMtbdd.ModRN(other.sylvanMtbdd)); } #ifdef STORM_HAVE_CARL