diff --git a/src/adapters/AddExpressionAdapter.cpp b/src/adapters/AddExpressionAdapter.cpp index e50620db8..7a22c8f8f 100644 --- a/src/adapters/AddExpressionAdapter.cpp +++ b/src/adapters/AddExpressionAdapter.cpp @@ -195,7 +195,7 @@ namespace storm { template boost::any AddExpressionAdapter::visit(storm::expressions::DoubleLiteralExpression const& expression) { - return ddManager->getConstant(static_cast(expression.getValue())); + return ddManager->getConstant(static_cast(expression.getValueAsDouble())); } // Explicitly instantiate the symbolic expression adapter diff --git a/src/adapters/MathsatExpressionAdapter.h b/src/adapters/MathsatExpressionAdapter.h index 9fec0cf15..db5bf9b69 100644 --- a/src/adapters/MathsatExpressionAdapter.h +++ b/src/adapters/MathsatExpressionAdapter.h @@ -172,7 +172,7 @@ namespace storm { } virtual boost::any visit(expressions::DoubleLiteralExpression const& expression) override { - return msat_make_number(env, std::to_string(expression.getValue()).c_str()); + return msat_make_number(env, std::to_string(expression.getValueAsDouble()).c_str()); } virtual boost::any visit(expressions::IntegerLiteralExpression const& expression) override { diff --git a/src/storage/expressions/DoubleLiteralExpression.cpp b/src/storage/expressions/DoubleLiteralExpression.cpp index cab9fc31b..192d747ee 100644 --- a/src/storage/expressions/DoubleLiteralExpression.cpp +++ b/src/storage/expressions/DoubleLiteralExpression.cpp @@ -2,14 +2,20 @@ #include "src/storage/expressions/ExpressionManager.h" #include "src/storage/expressions/ExpressionVisitor.h" +#include "src/utility/constants.h" + namespace storm { namespace expressions { - DoubleLiteralExpression::DoubleLiteralExpression(ExpressionManager const& manager, double value) : BaseExpression(manager, manager.getRationalType()), value(value) { + DoubleLiteralExpression::DoubleLiteralExpression(ExpressionManager const& manager, double value) : BaseExpression(manager, manager.getRationalType()), value(storm::utility::convertNumber(value)) { + // Intentionally left empty. + } + + DoubleLiteralExpression::DoubleLiteralExpression(ExpressionManager const& manager, std::string const& valueAsString) : BaseExpression(manager, manager.getRationalType()), value(storm::utility::convertNumber(valueAsString)) { // Intentionally left empty. } double DoubleLiteralExpression::evaluateAsDouble(Valuation const* valuation) const { - return this->getValue(); + return this->getValueAsDouble(); } bool DoubleLiteralExpression::isLiteral() const { @@ -28,7 +34,11 @@ namespace storm { return visitor.visit(*this); } - double DoubleLiteralExpression::getValue() const { + double DoubleLiteralExpression::getValueAsDouble() const { + return storm::utility::convertNumber(this->value); + } + + storm::RationalNumber DoubleLiteralExpression::getValue() const { return this->value; } diff --git a/src/storage/expressions/DoubleLiteralExpression.h b/src/storage/expressions/DoubleLiteralExpression.h index 676291a77..6a04f23e3 100644 --- a/src/storage/expressions/DoubleLiteralExpression.h +++ b/src/storage/expressions/DoubleLiteralExpression.h @@ -4,6 +4,8 @@ #include "src/storage/expressions/BaseExpression.h" #include "src/utility/OsDetection.h" +#include "src/adapters/CarlAdapter.h" + namespace storm { namespace expressions { class DoubleLiteralExpression : public BaseExpression { @@ -15,7 +17,15 @@ namespace storm { * @param value The value of the double literal. */ DoubleLiteralExpression(ExpressionManager const& manager, double value); - + + /*! + * Creates an double literal expression with the value given as a string. + * + * @param manager The manager responsible for this expression. + * @param value The string representation of the value of the literal. + */ + DoubleLiteralExpression(ExpressionManager const& manager, std::string const& valueAsString); + // Instantiate constructors and assignments with their default implementations. DoubleLiteralExpression(DoubleLiteralExpression const& other) = default; DoubleLiteralExpression& operator=(DoubleLiteralExpression const& other) = delete; @@ -37,15 +47,22 @@ namespace storm { * * @return The value of the double literal. */ - double getValue() const; + double getValueAsDouble() const; + + /*! + * Retrieves the value of the double literal. + * + * @return The value of the double literal. + */ + storm::RationalNumber getValue() const; protected: // Override base class method. virtual void printToStream(std::ostream& stream) const override; private: - // The value of the double literal. - double value; + // The value of the literal. + storm::RationalNumber value; }; } } diff --git a/src/storage/expressions/LinearCoefficientVisitor.cpp b/src/storage/expressions/LinearCoefficientVisitor.cpp index 8d7f39278..3d881c25e 100644 --- a/src/storage/expressions/LinearCoefficientVisitor.cpp +++ b/src/storage/expressions/LinearCoefficientVisitor.cpp @@ -152,7 +152,7 @@ namespace storm { } boost::any LinearCoefficientVisitor::visit(DoubleLiteralExpression const& expression) { - return VariableCoefficients(expression.getValue()); + return VariableCoefficients(expression.getValueAsDouble()); } } } \ No newline at end of file diff --git a/src/storage/expressions/ToRationalFunctionVisitor.cpp b/src/storage/expressions/ToRationalFunctionVisitor.cpp index 1a3dd0fc3..533fa1f1f 100644 --- a/src/storage/expressions/ToRationalFunctionVisitor.cpp +++ b/src/storage/expressions/ToRationalFunctionVisitor.cpp @@ -2,6 +2,7 @@ #include +#include "src/utility/constants.h" #include "src/utility/macros.h" #include "src/exceptions/InvalidArgumentException.h" @@ -93,7 +94,7 @@ namespace storm { template boost::any ToRationalFunctionVisitor::visit(DoubleLiteralExpression const& expression) { - return RationalFunctionType(carl::rationalize(expression.getValue())); + return storm::utility::convertNumber(expression.getValue()); } template class ToRationalFunctionVisitor; diff --git a/src/storage/expressions/ToRationalNumberVisitor.cpp b/src/storage/expressions/ToRationalNumberVisitor.cpp index 785f36950..44194cb4b 100644 --- a/src/storage/expressions/ToRationalNumberVisitor.cpp +++ b/src/storage/expressions/ToRationalNumberVisitor.cpp @@ -1,6 +1,7 @@ #include "src/storage/expressions/ToRationalNumberVisitor.h" #include "src/utility/macros.h" +#include "src/utility/constants.h" #include "src/exceptions/InvalidArgumentException.h" #include "src/exceptions/NotSupportedException.h" @@ -28,26 +29,36 @@ namespace storm { template boost::any ToRationalNumberVisitor::visit(BinaryNumericalFunctionExpression const& expression) { - RationalNumberType firstOperandAsRationalFunction = boost::any_cast(expression.getFirstOperand()->accept(*this)); - RationalNumberType secondOperandAsRationalFunction = boost::any_cast(expression.getSecondOperand()->accept(*this)); + RationalNumberType firstOperandAsRationalNumber = boost::any_cast(expression.getFirstOperand()->accept(*this)); + RationalNumberType secondOperandAsRationalNumber = boost::any_cast(expression.getSecondOperand()->accept(*this)); switch(expression.getOperatorType()) { case BinaryNumericalFunctionExpression::OperatorType::Plus: - return firstOperandAsRationalFunction + secondOperandAsRationalFunction; + return firstOperandAsRationalNumber + secondOperandAsRationalNumber; break; case BinaryNumericalFunctionExpression::OperatorType::Minus: - return firstOperandAsRationalFunction - secondOperandAsRationalFunction; + return firstOperandAsRationalNumber - secondOperandAsRationalNumber; break; case BinaryNumericalFunctionExpression::OperatorType::Times: - return firstOperandAsRationalFunction * secondOperandAsRationalFunction; + return firstOperandAsRationalNumber * secondOperandAsRationalNumber; break; case BinaryNumericalFunctionExpression::OperatorType::Divide: - return firstOperandAsRationalFunction / secondOperandAsRationalFunction; + return firstOperandAsRationalNumber / secondOperandAsRationalNumber; + break; + case BinaryNumericalFunctionExpression::OperatorType::Min: + return std::min(firstOperandAsRationalNumber, secondOperandAsRationalNumber); + break; + case BinaryNumericalFunctionExpression::OperatorType::Max: + return std::max(firstOperandAsRationalNumber, secondOperandAsRationalNumber); + break; + case BinaryNumericalFunctionExpression::OperatorType::Power: + STORM_LOG_THROW(storm::utility::isInteger(secondOperandAsRationalNumber), storm::exceptions::InvalidArgumentException, "Exponent of power operator must be a positive integer."); + uint_fast64_t exponentAsInteger = storm::utility::convertNumber(secondOperandAsRationalNumber); + return storm::utility::pow(firstOperandAsRationalNumber, exponentAsInteger); break; - default: - STORM_LOG_ASSERT(false, "Illegal operator type."); } // Return a dummy. This point must, however, never be reached. + STORM_LOG_ASSERT(false, "Illegal operator type."); return boost::any(); } @@ -88,7 +99,7 @@ namespace storm { template boost::any ToRationalNumberVisitor::visit(DoubleLiteralExpression const& expression) { #ifdef STORM_HAVE_CARL - return RationalNumberType(carl::rationalize(expression.getValue())); + return expression.getValue(); #else STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Rational numbers are not supported in this build."); #endif diff --git a/src/utility/constants.cpp b/src/utility/constants.cpp index 71d56cd63..2630ed285 100644 --- a/src/utility/constants.cpp +++ b/src/utility/constants.cpp @@ -39,6 +39,23 @@ namespace storm { bool isConstant(ValueType const& a) { return true; } + + template + bool isInteger(ValueType const& number) { + ValueType iPart; + ValueType result = std::modf(number, &iPart); + return result = zero(); + } + + template<> + bool isInteger(int const& number) { + return true; + } + + template<> + bool isInteger(uint_fast64_t const& number) { + return true; + } #ifdef STORM_HAVE_CARL template<> @@ -50,7 +67,6 @@ namespace storm { bool isZero(storm::RationalNumber const& a) { return carl::isZero(a); } - template<> bool isOne(storm::RationalFunction const& a) { @@ -93,6 +109,12 @@ namespace storm { // FIXME: this should be treated more properly. return storm::RationalNumber(-1); } + + template<> + bool isInteger(storm::RationalNumber const& number) { + return carl::isInteger(number); + } + #endif template @@ -102,9 +124,9 @@ namespace storm { template ValueType simplify(ValueType value) { - // In the general case, we don't do anything here, but merely return the value. If something else is - // supposed to happen here, the templated function can be specialized for this particular type. - return value; + // In the general case, we don't do anything here, but merely return the value. If something else is + // supposed to happen here, the templated function can be specialized for this particular type. + return value; } template<> @@ -151,7 +173,12 @@ namespace storm { double convertNumber(RationalNumber const& number){ return carl::toDouble(number); } - + + template<> + uint_fast64_t convertNumber(RationalNumber const& number){ + return carl::toInt(number); + } + template<> RationalNumber convertNumber(double const& number){ return carl::rationalize(number); @@ -167,15 +194,26 @@ namespace storm { return RationalFunction(carl::rationalize(number)); } + template<> + RationalNumber convertNumber(std::string const& number) { + return carl::rationalize(number); + } + template<> RationalFunction convertNumber(RationalNumber const& number) { return RationalFunction(number); } template<> - storm::RationalNumber abs(storm::RationalNumber const& number) { + RationalNumber abs(storm::RationalNumber const& number) { return carl::abs(number); } + + template<> + RationalNumber pow(RationalNumber const& value, uint_fast64_t exponent) { + return carl::pow(value, exponent); + } + #endif template @@ -214,6 +252,7 @@ namespace storm { template storm::storage::MatrixEntry&& simplify(storm::storage::MatrixEntry&& matrixEntry); template double abs(double const& number); + template bool isInteger(double const& number); template bool isOne(float const& value); template bool isZero(float const& value); @@ -224,6 +263,7 @@ namespace storm { template float infinity(); template float pow(float const& value, uint_fast64_t exponent); + template bool isInteger(float const& number); template float simplify(float value); @@ -240,7 +280,8 @@ namespace storm { template int infinity(); template int pow(int const& value, uint_fast64_t exponent); - + template bool isInteger(int const& number); + template int simplify(int value); template storm::storage::MatrixEntry simplify(storm::storage::MatrixEntry matrixEntry); @@ -278,12 +319,14 @@ namespace storm { template storm::RationalNumber infinity(); template double convertNumber(storm::RationalNumber const& number); + template uint_fast64_t convertNumber(storm::RationalNumber const& number); template storm::RationalNumber convertNumber(double const& number); template storm::RationalNumber convertNumber(storm::RationalNumber const& number); - + RationalNumber convertNumber(std::string const& number); + template storm::RationalNumber abs(storm::RationalNumber const& number); -// template storm::RationalNumber pow(storm::RationalNumber const& value, uint_fast64_t exponent); + template storm::RationalNumber pow(storm::RationalNumber const& value, uint_fast64_t exponent); template storm::RationalNumber simplify(storm::RationalNumber value); template storm::storage::MatrixEntry simplify(storm::storage::MatrixEntry matrixEntry); diff --git a/src/utility/constants.h b/src/utility/constants.h index 4ec4e7539..66edb9f46 100644 --- a/src/utility/constants.h +++ b/src/utility/constants.h @@ -56,6 +56,9 @@ namespace storm { template ValueType abs(ValueType const& number); + + template + bool isInteger(ValueType const& number); } }