From 0d43a5592327bfefa5984676d160ff59171b740f Mon Sep 17 00:00:00 2001 From: Johannes Lehmann Date: Wed, 9 Jun 2021 16:32:27 +0200 Subject: [PATCH] Fixed incorrect type of modulo expression with integer inputs --- src/storm/storage/expressions/Expression.cpp | 4 ++-- src/storm/storage/expressions/Type.cpp | 5 +++++ src/storm/storage/expressions/Type.h | 1 + src/test/storm/storage/ExpressionTest.cpp | 21 +++++++++++++++++++- 4 files changed, 28 insertions(+), 3 deletions(-) diff --git a/src/storm/storage/expressions/Expression.cpp b/src/storm/storage/expressions/Expression.cpp index 6c5646c5f..b922f3ce5 100644 --- a/src/storm/storage/expressions/Expression.cpp +++ b/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(new BinaryNumericalFunctionExpression(first.getBaseExpression().getManager(), first.getType().power(second.getType()), first.getBaseExpressionPointer(), second.getBaseExpressionPointer(), BinaryNumericalFunctionExpression::OperatorType::Modulo))); + return Expression(std::shared_ptr(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(new BinaryNumericalFunctionExpression(first.getBaseExpression().getManager(), first.getType().minimumMaximum(second.getType()), first.getBaseExpressionPointer(), second.getBaseExpressionPointer(), BinaryNumericalFunctionExpression::OperatorType::Modulo))); + return Expression(std::shared_ptr(new BinaryNumericalFunctionExpression(first.getBaseExpression().getManager(), first.getType().modulo(second.getType()), first.getBaseExpressionPointer(), second.getBaseExpressionPointer(), BinaryNumericalFunctionExpression::OperatorType::Modulo))); } Expression apply(std::vector const& expressions, std::function const& function) { diff --git a/src/storm/storage/expressions/Type.cpp b/src/storm/storage/expressions/Type.cpp index 31882116b..67a968316 100644 --- a/src/storm/storage/expressions/Type.cpp +++ b/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."); diff --git a/src/storm/storage/expressions/Type.h b/src/storm/storage/expressions/Type.h index b5cba7fab..535d16733 100644 --- a/src/storm/storage/expressions/Type.h +++ b/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; diff --git a/src/test/storm/storage/ExpressionTest.cpp b/src/test/storm/storage/ExpressionTest.cpp index b61d549d5..1a50d3acb 100644 --- a/src/test/storm/storage/ExpressionTest.cpp +++ b/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()); }