diff --git a/src/storm/storage/expressions/UnaryNumericalFunctionExpression.cpp b/src/storm/storage/expressions/UnaryNumericalFunctionExpression.cpp index 770c7b9f1..1b4b5d0da 100644 --- a/src/storm/storage/expressions/UnaryNumericalFunctionExpression.cpp +++ b/src/storm/storage/expressions/UnaryNumericalFunctionExpression.cpp @@ -40,6 +40,7 @@ namespace storm { int_fast64_t result = this->getOperand()->evaluateAsInt(valuation); return -result; } else { + // TODO: this should evaluate the operand as a rational. double result = this->getOperand()->evaluateAsDouble(valuation); switch (this->getOperatorType()) { case OperatorType::Floor: return static_cast(std::floor(result)); break; @@ -67,39 +68,36 @@ namespace storm { std::shared_ptr operandSimplified = this->getOperand()->simplify(); if (operandSimplified->isLiteral()) { - boost::variant operandEvaluation; if (operandSimplified->hasIntegerType()) { - operandEvaluation = operandSimplified->evaluateAsInt(); - } else { - operandEvaluation = operandSimplified->evaluateAsRational(); - } - - bool rationalToInteger = this->getOperatorType() == OperatorType::Floor || this->getOperatorType() == OperatorType::Ceil; - if (operandSimplified->hasIntegerType()) { - int_fast64_t value = 0; + int_fast64_t value = operandSimplified->evaluateAsInt(); switch (this->getOperatorType()) { - case OperatorType::Minus: value = -boost::get(operandEvaluation); break; - case OperatorType::Floor: value = std::floor(boost::get(operandEvaluation)); break; - case OperatorType::Ceil: value = std::ceil(boost::get(operandEvaluation)); break; - } - return std::shared_ptr(new IntegerLiteralExpression(this->getManager(), value)); - } else if (rationalToInteger) { - int_fast64_t value = 0; - switch (this->getOperatorType()) { - case OperatorType::Floor: value = storm::utility::convertNumber(storm::RationalNumber(carl::floor(boost::get(operandEvaluation)))); break; - case OperatorType::Ceil: value = storm::utility::convertNumber(storm::RationalNumber(carl::ceil(boost::get(operandEvaluation)))); break; - default: - STORM_LOG_ASSERT(false, "Unexpected rational to integer conversion."); + case OperatorType::Minus: value = -value; break; + // Nothing to be done for the other cases: + // case OperatorType::Floor: + // case OperatorType::Ceil: } return std::shared_ptr(new IntegerLiteralExpression(this->getManager(), value)); } else { - storm::RationalNumber value = storm::utility::zero(); + storm::RationalNumber value = operandSimplified->evaluateAsRational(); + bool convertToInteger = false; switch (this->getOperatorType()) { - case OperatorType::Minus: value = -boost::get(operandEvaluation); break; - case OperatorType::Floor: value = carl::floor(boost::get(operandEvaluation)); break; - case OperatorType::Ceil: value = carl::ceil(boost::get(operandEvaluation)); break; + case OperatorType::Minus: + value = -value; + break; + case OperatorType::Floor: + value = storm::utility::floor(value); + convertToInteger = true; + break; + case OperatorType::Ceil: + value = storm::utility::ceil(value); + convertToInteger = true; + break; + } + if (convertToInteger) { + return std::shared_ptr(new IntegerLiteralExpression(this->getManager(), storm::utility::convertNumber(value))); + } else { + return std::shared_ptr(new RationalLiteralExpression(this->getManager(), value)); } - return std::shared_ptr(new RationalLiteralExpression(this->getManager(), value)); } }