From 6d445e38af9560f5889457ef3bec8edee9d258c4 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Tue, 17 Apr 2018 15:04:42 +0200
Subject: [PATCH] fixes github issue #18
---
.../UnaryNumericalFunctionExpression.cpp | 10 ++++++++++
src/storm/utility/constants.cpp | 14 ++++++++++++--
2 files changed, 22 insertions(+), 2 deletions(-)
diff --git a/src/storm/storage/expressions/UnaryNumericalFunctionExpression.cpp b/src/storm/storage/expressions/UnaryNumericalFunctionExpression.cpp
index 3ed20d7b6..770c7b9f1 100644
--- a/src/storm/storage/expressions/UnaryNumericalFunctionExpression.cpp
+++ b/src/storm/storage/expressions/UnaryNumericalFunctionExpression.cpp
@@ -74,6 +74,7 @@ namespace storm {
operandEvaluation = operandSimplified->evaluateAsRational();
}
+ bool rationalToInteger = this->getOperatorType() == OperatorType::Floor || this->getOperatorType() == OperatorType::Ceil;
if (operandSimplified->hasIntegerType()) {
int_fast64_t value = 0;
switch (this->getOperatorType()) {
@@ -82,6 +83,15 @@ namespace storm {
case OperatorType::Ceil: value = std::ceil(boost::get<int_fast64_t>(operandEvaluation)); break;
}
return std::shared_ptr<BaseExpression>(new IntegerLiteralExpression(this->getManager(), value));
+ } else if (rationalToInteger) {
+ int_fast64_t value = 0;
+ switch (this->getOperatorType()) {
+ case OperatorType::Floor: value = storm::utility::convertNumber<int_fast64_t>(storm::RationalNumber(carl::floor(boost::get<storm::RationalNumber>(operandEvaluation)))); break;
+ case OperatorType::Ceil: value = storm::utility::convertNumber<int_fast64_t>(storm::RationalNumber(carl::ceil(boost::get<storm::RationalNumber>(operandEvaluation)))); break;
+ default:
+ STORM_LOG_ASSERT(false, "Unexpected rational to integer conversion.");
+ }
+ return std::shared_ptr<BaseExpression>(new IntegerLiteralExpression(this->getManager(), value));
} else {
storm::RationalNumber value = storm::utility::zero<storm::RationalNumber>();
switch (this->getOperatorType()) {
diff --git a/src/storm/utility/constants.cpp b/src/storm/utility/constants.cpp
index 6086f1bf9..6c0d1c814 100644
--- a/src/storm/utility/constants.cpp
+++ b/src/storm/utility/constants.cpp
@@ -324,7 +324,12 @@ namespace storm {
uint_fast64_t convertNumber(ClnRationalNumber const& number) {
return carl::toInt<carl::uint>(number);
}
-
+
+ template<>
+ int_fast64_t convertNumber(ClnRationalNumber const& number) {
+ return carl::toInt<carl::sint>(number);
+ }
+
template<>
ClnRationalNumber convertNumber(double const& number) {
return carl::rationalize<ClnRationalNumber>(number);
@@ -516,7 +521,12 @@ namespace storm {
uint_fast64_t convertNumber(GmpRationalNumber const& number){
return carl::toInt<carl::uint>(number);
}
-
+
+ template<>
+ int_fast64_t convertNumber(GmpRationalNumber const& number){
+ return carl::toInt<carl::sint>(number);
+ }
+
template<>
GmpRationalNumber convertNumber(double const& number){
return carl::rationalize<GmpRationalNumber>(number);