Fixed incorrect type of modulo expression with integer inputs

src/storm/storage/expressions/Expression.cpp

@@ -285,7 +285,7 @@ namespace storm {
         
         Expression operator%(Expression const& first, Expression const& second) {
             assertSameManager(first.getBaseExpression(), second.getBaseExpression());
-            return Expression(std::shared_ptr<BaseExpression>(new BinaryNumericalFunctionExpression(first.getBaseExpression().getManager(), first.getType().power(second.getType()), first.getBaseExpressionPointer(), second.getBaseExpressionPointer(), BinaryNumericalFunctionExpression::OperatorType::Modulo)));
+            return Expression(std::shared_ptr<BaseExpression>(new BinaryNumericalFunctionExpression(first.getBaseExpression().getManager(), first.getType().modulo(second.getType()), first.getBaseExpressionPointer(), second.getBaseExpressionPointer(), BinaryNumericalFunctionExpression::OperatorType::Modulo)));
         }
         
         Expression operator&&(Expression const& first, Expression const& second) {
@@ -452,7 +452,7 @@ namespace storm {
         }
 
         Expression modulo(Expression const& first, Expression const& second) {
-            return Expression(std::shared_ptr<BaseExpression>(new BinaryNumericalFunctionExpression(first.getBaseExpression().getManager(), first.getType().minimumMaximum(second.getType()), first.getBaseExpressionPointer(), second.getBaseExpressionPointer(), BinaryNumericalFunctionExpression::OperatorType::Modulo)));
+            return Expression(std::shared_ptr<BaseExpression>(new BinaryNumericalFunctionExpression(first.getBaseExpression().getManager(), first.getType().modulo(second.getType()), first.getBaseExpressionPointer(), second.getBaseExpressionPointer(), BinaryNumericalFunctionExpression::OperatorType::Modulo)));
         }
         
         Expression apply(std::vector<storm::expressions::Expression> const& expressions, std::function<Expression (Expression const&, Expression const&)> const& function) {

src/storm/storage/expressions/Type.cpp

@@ -214,6 +214,11 @@ namespace storm {
             STORM_LOG_THROW(!this->isBitVectorType() && !other.isBitVectorType(), storm::exceptions::InvalidTypeException, "Operator requires non-bitvector operands.");
             return std::max(*this, other);
         }
+
+        Type Type::modulo(Type const& other) const {
+            STORM_LOG_THROW(this->isNumericalType() && other.isNumericalType(), storm::exceptions::InvalidTypeException, "Operator requires numerical operands.");
+            return std::max(*this, other);
+        }
         
         Type Type::power(Type const& other, bool allowIntegerType) const {
             STORM_LOG_THROW(this->isNumericalType() && other.isNumericalType(), storm::exceptions::InvalidTypeException, "Operator requires numerical operands.");

src/storm/storage/expressions/Type.h

@@ -115,6 +115,7 @@ namespace storm {
             Type plusMinusTimes(Type const& other) const;
             Type minus() const;
             Type divide(Type const& other) const;
+            Type modulo(Type const& other) const;
             Type power(Type const& other, bool allowIntegerType = false) const;
             Type logicalConnective(Type const& other) const;
             Type logicalConnective() const;

src/test/storm/storage/ExpressionTest.cpp

@@ -209,6 +209,26 @@ TEST(Expression, OperatorTest) {
     EXPECT_TRUE(tempExpression.hasBooleanType());
     ASSERT_NO_THROW(tempExpression = intVarExpression <= rationalVarExpression);
     EXPECT_TRUE(tempExpression.hasBooleanType());
+
+    STORM_SILENT_ASSERT_THROW(tempExpression = trueExpression % piExpression, storm::exceptions::InvalidTypeException);
+    ASSERT_NO_THROW(tempExpression = threeExpression % threeExpression);
+    EXPECT_TRUE(tempExpression.hasIntegerType());
+    ASSERT_NO_THROW(tempExpression = threeExpression % piExpression);
+    EXPECT_TRUE(tempExpression.hasRationalType());
+    ASSERT_NO_THROW(tempExpression = piExpression % threeExpression);
+    EXPECT_TRUE(tempExpression.hasRationalType());
+    ASSERT_NO_THROW(tempExpression = piExpression % piExpression);
+    EXPECT_TRUE(tempExpression.hasRationalType());
+
+    STORM_SILENT_ASSERT_THROW(tempExpression = storm::expressions::modulo(trueExpression, piExpression), storm::exceptions::InvalidTypeException);
+    ASSERT_NO_THROW(tempExpression = storm::expressions::modulo(threeExpression, threeExpression));
+    EXPECT_TRUE(tempExpression.hasIntegerType());
+    ASSERT_NO_THROW(tempExpression = storm::expressions::modulo(threeExpression, piExpression));
+    EXPECT_TRUE(tempExpression.hasRationalType());
+    ASSERT_NO_THROW(tempExpression = storm::expressions::modulo(piExpression, threeExpression));
+    EXPECT_TRUE(tempExpression.hasRationalType());
+    ASSERT_NO_THROW(tempExpression = storm::expressions::modulo(piExpression, piExpression));
+    EXPECT_TRUE(tempExpression.hasRationalType());
     
     STORM_SILENT_ASSERT_THROW(tempExpression = storm::expressions::minimum(trueExpression, piExpression), storm::exceptions::InvalidTypeException);
     ASSERT_NO_THROW(tempExpression = storm::expressions::minimum(threeExpression, threeExpression));
@@ -260,7 +280,6 @@ TEST(Expression, OperatorTest) {
     ASSERT_NO_THROW(tempExpression = storm::expressions::pow(intVarExpression, rationalVarExpression));
     EXPECT_TRUE(tempExpression.hasRationalType());
 
-    STORM_SILENT_ASSERT_THROW(tempExpression = storm::expressions::modulo(trueExpression, piExpression), storm::exceptions::InvalidTypeException);
     ASSERT_NO_THROW(tempExpression = storm::expressions::maximum(threeExpression, threeExpression));
     EXPECT_TRUE(tempExpression.hasIntegerType());
 }