diff --git a/src/storm/storage/expressions/BinaryNumericalFunctionExpression.cpp b/src/storm/storage/expressions/BinaryNumericalFunctionExpression.cpp index 5524ca52d..3d2e09153 100644 --- a/src/storm/storage/expressions/BinaryNumericalFunctionExpression.cpp +++ b/src/storm/storage/expressions/BinaryNumericalFunctionExpression.cpp @@ -1,6 +1,7 @@ #include #include +#include "storm/adapters/NumberAdapter.h" #include "storm/storage/expressions/BinaryNumericalFunctionExpression.h" #include "storm/storage/expressions/IntegerLiteralExpression.h" #include "storm/storage/expressions/RationalLiteralExpression.h" @@ -90,16 +91,21 @@ namespace storm { } return std::shared_ptr(new IntegerLiteralExpression(this->getManager(), newValue)); } else if (this->hasRationalType()) { - double firstOperandEvaluation = firstOperandSimplified->evaluateAsDouble(); - double secondOperandEvaluation = secondOperandSimplified->evaluateAsDouble(); - double newValue = 0; + storm::RationalNumber firstOperandEvaluation = firstOperandSimplified->evaluateAsRational(); + storm::RationalNumber secondOperandEvaluation = secondOperandSimplified->evaluateAsRational(); + storm::RationalNumber newValue = 0; switch (this->getOperatorType()) { case OperatorType::Plus: newValue = firstOperandEvaluation + secondOperandEvaluation; break; case OperatorType::Minus: newValue = firstOperandEvaluation - secondOperandEvaluation; break; case OperatorType::Times: newValue = firstOperandEvaluation * secondOperandEvaluation; break; case OperatorType::Min: newValue = std::min(firstOperandEvaluation, secondOperandEvaluation); break; case OperatorType::Max: newValue = std::max(firstOperandEvaluation, secondOperandEvaluation); break; - case OperatorType::Power: newValue = std::pow(firstOperandEvaluation, secondOperandEvaluation); break; + case OperatorType::Power: { + STORM_LOG_THROW(carl::isInteger(secondOperandEvaluation), storm::exceptions::InvalidStateException, "Can not simplify pow() with fractional exponent."); + std::size_t exponent = carl::toInt(secondOperandEvaluation); + newValue = carl::pow(firstOperandEvaluation, exponent); + break; + } case OperatorType::Divide: STORM_LOG_THROW(false, storm::exceptions::InvalidStateException, "Unable to simplify division."); break; } return std::shared_ptr(new RationalLiteralExpression(this->getManager(), newValue)); diff --git a/src/storm/storage/expressions/BinaryRelationExpression.cpp b/src/storm/storage/expressions/BinaryRelationExpression.cpp index 7602fbf3c..a610802e8 100644 --- a/src/storm/storage/expressions/BinaryRelationExpression.cpp +++ b/src/storm/storage/expressions/BinaryRelationExpression.cpp @@ -4,6 +4,7 @@ #include "storm/storage/expressions/BooleanLiteralExpression.h" #include "storm/utility/macros.h" +#include "storm/utility/constants.h" #include "storm/exceptions/InvalidTypeException.h" #include "storm/storage/expressions/ExpressionVisitor.h" @@ -48,28 +49,28 @@ namespace storm { std::shared_ptr secondOperandSimplified = this->getSecondOperand()->simplify(); if (firstOperandSimplified->isLiteral() && secondOperandSimplified->isLiteral()) { - boost::variant firstOperandEvaluation; - boost::variant secondOperandEvaluation; - + storm::RationalNumber firstOperandEvaluation; + storm::RationalNumber secondOperandEvaluation; + if (firstOperandSimplified->hasIntegerType()) { - firstOperandEvaluation = firstOperandSimplified->evaluateAsInt(); + firstOperandEvaluation = storm::utility::convertNumber(firstOperandSimplified->evaluateAsInt()); } else { - firstOperandEvaluation = firstOperandSimplified->evaluateAsDouble(); + firstOperandEvaluation = firstOperandSimplified->evaluateAsRational(); } if (secondOperandSimplified->hasIntegerType()) { - secondOperandEvaluation = secondOperandSimplified->evaluateAsInt(); + secondOperandEvaluation = storm::utility::convertNumber(secondOperandSimplified->evaluateAsInt()); } else { - secondOperandEvaluation = secondOperandSimplified->evaluateAsDouble(); + secondOperandEvaluation = secondOperandSimplified->evaluateAsRational(); } - + bool truthValue = false; switch (this->getRelationType()) { - case RelationType::Equal: truthValue = (firstOperandSimplified->hasIntegerType() ? boost::get(firstOperandEvaluation) : boost::get(firstOperandEvaluation)) == (secondOperandSimplified->hasIntegerType() ? boost::get(secondOperandEvaluation) : boost::get(secondOperandEvaluation)); break; - case RelationType::NotEqual: truthValue = (firstOperandSimplified->hasIntegerType() ? boost::get(firstOperandEvaluation) : boost::get(firstOperandEvaluation)) != (secondOperandSimplified->hasIntegerType() ? boost::get(secondOperandEvaluation) : boost::get(secondOperandEvaluation)); break; - case RelationType::Greater: truthValue = (firstOperandSimplified->hasIntegerType() ? boost::get(firstOperandEvaluation) : boost::get(firstOperandEvaluation)) > (secondOperandSimplified->hasIntegerType() ? boost::get(secondOperandEvaluation) : boost::get(secondOperandEvaluation)); break; - case RelationType::GreaterOrEqual: truthValue = (firstOperandSimplified->hasIntegerType() ? boost::get(firstOperandEvaluation) : boost::get(firstOperandEvaluation)) >= (secondOperandSimplified->hasIntegerType() ? boost::get(secondOperandEvaluation) : boost::get(secondOperandEvaluation)); break; - case RelationType::Less: truthValue = (firstOperandSimplified->hasIntegerType() ? boost::get(firstOperandEvaluation) : boost::get(firstOperandEvaluation)) < (secondOperandSimplified->hasIntegerType() ? boost::get(secondOperandEvaluation) : boost::get(secondOperandEvaluation)); break; - case RelationType::LessOrEqual: truthValue = (firstOperandSimplified->hasIntegerType() ? boost::get(firstOperandEvaluation) : boost::get(firstOperandEvaluation)) <= (secondOperandSimplified->hasIntegerType() ? boost::get(secondOperandEvaluation) : boost::get(secondOperandEvaluation)); break; + case RelationType::Equal: truthValue = firstOperandEvaluation == secondOperandEvaluation; break; + case RelationType::NotEqual: truthValue = firstOperandEvaluation != secondOperandEvaluation; break; + case RelationType::Greater: truthValue = firstOperandEvaluation > secondOperandEvaluation; break; + case RelationType::GreaterOrEqual: truthValue = firstOperandEvaluation >= secondOperandEvaluation; break; + case RelationType::Less: truthValue = firstOperandEvaluation < secondOperandEvaluation; break; + case RelationType::LessOrEqual: truthValue = firstOperandEvaluation <= secondOperandEvaluation; break; } return std::shared_ptr(new BooleanLiteralExpression(this->getManager(), truthValue)); } diff --git a/src/storm/storage/expressions/UnaryNumericalFunctionExpression.cpp b/src/storm/storage/expressions/UnaryNumericalFunctionExpression.cpp index 2382e1399..9fc2c5639 100644 --- a/src/storm/storage/expressions/UnaryNumericalFunctionExpression.cpp +++ b/src/storm/storage/expressions/UnaryNumericalFunctionExpression.cpp @@ -2,11 +2,13 @@ #include +#include "storm/adapters/NumberAdapter.h" #include "storm/storage/expressions/UnaryNumericalFunctionExpression.h" #include "storm/storage/expressions/IntegerLiteralExpression.h" #include "storm/storage/expressions/RationalLiteralExpression.h" #include "ExpressionVisitor.h" #include "storm/utility/macros.h" +#include "storm/utility/constants.h" #include "storm/exceptions/InvalidTypeException.h" #include "storm/exceptions/InvalidOperationException.h" @@ -65,14 +67,13 @@ namespace storm { std::shared_ptr operandSimplified = this->getOperand()->simplify(); if (operandSimplified->isLiteral()) { - boost::variant operandEvaluation; + boost::variant operandEvaluation; if (operandSimplified->hasIntegerType()) { operandEvaluation = operandSimplified->evaluateAsInt(); } else { - operandEvaluation = operandSimplified->evaluateAsDouble(); + operandEvaluation = operandSimplified->evaluateAsRational(); } - boost::variant result; if (operandSimplified->hasIntegerType()) { int_fast64_t value = 0; switch (this->getOperatorType()) { @@ -82,11 +83,11 @@ namespace storm { } return std::shared_ptr(new IntegerLiteralExpression(this->getManager(), value)); } else { - double value = 0; + storm::RationalNumber value = storm::utility::zero(); 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; + 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; } return std::shared_ptr(new RationalLiteralExpression(this->getManager(), value)); }