Added support for modulo operators when building symbolic models in exact mode.

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) {

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;
 

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;

src/storm/storage/dd/sylvan/InternalSylvanAdd.cpp

@@ -328,8 +328,8 @@ namespace storm {
         }
 
         template<>
-        InternalAdd<DdType::Sylvan, storm::RationalNumber> InternalAdd<DdType::Sylvan, storm::RationalNumber>::mod(InternalAdd<DdType::Sylvan, storm::RationalNumber> const&) const {
-            STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Operation (mod) not supported by rational numbers.");
+        InternalAdd<DdType::Sylvan, storm::RationalNumber> InternalAdd<DdType::Sylvan, storm::RationalNumber>::mod(InternalAdd<DdType::Sylvan, storm::RationalNumber> const& other) const {
+            return InternalAdd<DdType::Sylvan, storm::RationalNumber>(ddManager, this->sylvanMtbdd.ModRN(other.sylvanMtbdd));
         }
 
 #ifdef STORM_HAVE_CARL