diff --git a/src/adapters/AddExpressionAdapter.cpp b/src/adapters/AddExpressionAdapter.cpp index 7a22c8f8f..2f0dc7190 100644 --- a/src/adapters/AddExpressionAdapter.cpp +++ b/src/adapters/AddExpressionAdapter.cpp @@ -194,7 +194,7 @@ namespace storm { } template - boost::any AddExpressionAdapter::visit(storm::expressions::DoubleLiteralExpression const& expression) { + boost::any AddExpressionAdapter::visit(storm::expressions::RationalLiteralExpression const& expression) { return ddManager->getConstant(static_cast(expression.getValueAsDouble())); } diff --git a/src/adapters/AddExpressionAdapter.h b/src/adapters/AddExpressionAdapter.h index 89d825d96..dfb13a315 100644 --- a/src/adapters/AddExpressionAdapter.h +++ b/src/adapters/AddExpressionAdapter.h @@ -31,7 +31,7 @@ namespace storm { virtual boost::any visit(storm::expressions::UnaryNumericalFunctionExpression const& expression) override; virtual boost::any visit(storm::expressions::BooleanLiteralExpression const& expression) override; virtual boost::any visit(storm::expressions::IntegerLiteralExpression const& expression) override; - virtual boost::any visit(storm::expressions::DoubleLiteralExpression const& expression) override; + virtual boost::any visit(storm::expressions::RationalLiteralExpression const& expression) override; private: // The manager responsible for the DDs built by this adapter. diff --git a/src/adapters/MathsatExpressionAdapter.h b/src/adapters/MathsatExpressionAdapter.h index db5bf9b69..77b39cc68 100644 --- a/src/adapters/MathsatExpressionAdapter.h +++ b/src/adapters/MathsatExpressionAdapter.h @@ -171,7 +171,7 @@ namespace storm { return expression.getValue() ? msat_make_true(env) : msat_make_false(env); } - virtual boost::any visit(expressions::DoubleLiteralExpression const& expression) override { + virtual boost::any visit(expressions::RationalLiteralExpression const& expression) override { return msat_make_number(env, std::to_string(expression.getValueAsDouble()).c_str()); } diff --git a/src/adapters/Z3ExpressionAdapter.cpp b/src/adapters/Z3ExpressionAdapter.cpp index 60b4e8e1c..6f4efc178 100644 --- a/src/adapters/Z3ExpressionAdapter.cpp +++ b/src/adapters/Z3ExpressionAdapter.cpp @@ -208,7 +208,7 @@ namespace storm { return context.bool_val(expression.getValue()); } - boost::any Z3ExpressionAdapter::visit(storm::expressions::DoubleLiteralExpression const& expression) { + boost::any Z3ExpressionAdapter::visit(storm::expressions::RationalLiteralExpression const& expression) { std::stringstream fractionStream; fractionStream << expression.getValue(); return context.real_val(fractionStream.str().c_str()); diff --git a/src/adapters/Z3ExpressionAdapter.h b/src/adapters/Z3ExpressionAdapter.h index 4fc60c8a5..2735f5713 100644 --- a/src/adapters/Z3ExpressionAdapter.h +++ b/src/adapters/Z3ExpressionAdapter.h @@ -63,7 +63,7 @@ namespace storm { virtual boost::any visit(storm::expressions::BooleanLiteralExpression const& expression) override; - virtual boost::any visit(storm::expressions::DoubleLiteralExpression const& expression) override; + virtual boost::any visit(storm::expressions::RationalLiteralExpression const& expression) override; virtual boost::any visit(storm::expressions::IntegerLiteralExpression const& expression) override; diff --git a/src/parser/ExpressionParser.cpp b/src/parser/ExpressionParser.cpp index d556d799a..3054f2fe0 100644 --- a/src/parser/ExpressionParser.cpp +++ b/src/parser/ExpressionParser.cpp @@ -61,7 +61,7 @@ namespace storm { identifierExpression = identifier[qi::_val = phoenix::bind(&ExpressionParser::getIdentifierExpression, phoenix::ref(*this), qi::_1, allowBacktracking, qi::_pass)]; identifierExpression.name("identifier expression"); - literalExpression = trueFalse_[qi::_val = qi::_1] | rationalLiteral_[qi::_val = phoenix::bind(&ExpressionParser::createDoubleLiteralExpression, phoenix::ref(*this), qi::_1, qi::_pass)] | qi::int_[qi::_val = phoenix::bind(&ExpressionParser::createIntegerLiteralExpression, phoenix::ref(*this), qi::_1, qi::_pass)]; + literalExpression = trueFalse_[qi::_val = qi::_1] | rationalLiteral_[qi::_val = phoenix::bind(&ExpressionParser::createRationalLiteralExpression, phoenix::ref(*this), qi::_1, qi::_pass)] | qi::int_[qi::_val = phoenix::bind(&ExpressionParser::createIntegerLiteralExpression, phoenix::ref(*this), qi::_1, qi::_pass)]; literalExpression.name("literal expression"); atomicExpression = floorCeilExpression | prefixPowerExpression | minMaxExpression | (qi::lit("(") >> expression >> qi::lit(")")) | literalExpression | identifierExpression; @@ -323,7 +323,7 @@ namespace storm { return manager->boolean(false); } - storm::expressions::Expression ExpressionParser::createDoubleLiteralExpression(storm::RationalNumber const& value, bool& pass) const { + storm::expressions::Expression ExpressionParser::createRationalLiteralExpression(storm::RationalNumber const& value, bool& pass) const { // If we are not supposed to accept double expressions, we reject it by setting pass to false. if (!this->acceptDoubleLiterals) { pass = false; diff --git a/src/parser/ExpressionParser.h b/src/parser/ExpressionParser.h index c728e0b84..077be8db2 100644 --- a/src/parser/ExpressionParser.h +++ b/src/parser/ExpressionParser.h @@ -260,7 +260,7 @@ namespace storm { storm::expressions::Expression createMultExpression(storm::expressions::Expression const& e1, storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e2, bool& pass) const; storm::expressions::Expression createPowerExpression(storm::expressions::Expression const& e1, storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e2, bool& pass) const; storm::expressions::Expression createUnaryExpression(boost::optional const& operatorType, storm::expressions::Expression const& e1, bool& pass) const; - storm::expressions::Expression createDoubleLiteralExpression(storm::RationalNumber const& value, bool& pass) const; + storm::expressions::Expression createRationalLiteralExpression(storm::RationalNumber const& value, bool& pass) const; storm::expressions::Expression createIntegerLiteralExpression(int value, bool& pass) const; storm::expressions::Expression createMinimumMaximumExpression(storm::expressions::Expression const& e1, storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e2, bool& pass) const; storm::expressions::Expression createFloorCeilExpression(storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e1, bool& pass) const; diff --git a/src/storage/expressions/BinaryNumericalFunctionExpression.cpp b/src/storage/expressions/BinaryNumericalFunctionExpression.cpp index 95a326de1..7c4367952 100644 --- a/src/storage/expressions/BinaryNumericalFunctionExpression.cpp +++ b/src/storage/expressions/BinaryNumericalFunctionExpression.cpp @@ -3,7 +3,7 @@ #include "src/storage/expressions/BinaryNumericalFunctionExpression.h" #include "src/storage/expressions/IntegerLiteralExpression.h" -#include "src/storage/expressions/DoubleLiteralExpression.h" +#include "src/storage/expressions/RationalLiteralExpression.h" #include "src/storage/expressions/ExpressionVisitor.h" #include "src/utility/macros.h" #include "src/exceptions/InvalidTypeException.h" @@ -102,7 +102,7 @@ namespace storm { case OperatorType::Power: newValue = static_cast(std::pow(firstOperandEvaluation, secondOperandEvaluation)); break; case OperatorType::Divide: STORM_LOG_THROW(false, storm::exceptions::InvalidStateException, "Unable to simplify division."); break; } - return std::shared_ptr(new DoubleLiteralExpression(this->getManager(), newValue)); + return std::shared_ptr(new RationalLiteralExpression(this->getManager(), newValue)); } } diff --git a/src/storage/expressions/DoubleLiteralExpression.cpp b/src/storage/expressions/DoubleLiteralExpression.cpp index 86a2ba889..3fa226a8a 100644 --- a/src/storage/expressions/DoubleLiteralExpression.cpp +++ b/src/storage/expressions/DoubleLiteralExpression.cpp @@ -1,4 +1,4 @@ -#include "src/storage/expressions/DoubleLiteralExpression.h" +#include "src/storage/expressions/RationalLiteralExpression.h" #include "src/storage/expressions/ExpressionManager.h" #include "src/storage/expressions/ExpressionVisitor.h" @@ -6,47 +6,47 @@ namespace storm { namespace expressions { - DoubleLiteralExpression::DoubleLiteralExpression(ExpressionManager const& manager, double value) : BaseExpression(manager, manager.getRationalType()), value(storm::utility::convertNumber(value)) { + RationalLiteralExpression::RationalLiteralExpression(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)) { + RationalLiteralExpression::RationalLiteralExpression(ExpressionManager const& manager, std::string const& valueAsString) : BaseExpression(manager, manager.getRationalType()), value(storm::utility::convertNumber(valueAsString)) { // Intentionally left empty. } - DoubleLiteralExpression::DoubleLiteralExpression(ExpressionManager const& manager, storm::RationalNumber const& value) : BaseExpression(manager, manager.getRationalType()), value(value) { + RationalLiteralExpression::RationalLiteralExpression(ExpressionManager const& manager, storm::RationalNumber const& value) : BaseExpression(manager, manager.getRationalType()), value(value) { // Intentionally left empty. } - double DoubleLiteralExpression::evaluateAsDouble(Valuation const* valuation) const { + double RationalLiteralExpression::evaluateAsDouble(Valuation const* valuation) const { return this->getValueAsDouble(); } - bool DoubleLiteralExpression::isLiteral() const { + bool RationalLiteralExpression::isLiteral() const { return true; } - void DoubleLiteralExpression::gatherVariables(std::set& variables) const { + void RationalLiteralExpression::gatherVariables(std::set& variables) const { return; } - std::shared_ptr DoubleLiteralExpression::simplify() const { + std::shared_ptr RationalLiteralExpression::simplify() const { return this->shared_from_this(); } - boost::any DoubleLiteralExpression::accept(ExpressionVisitor& visitor) const { + boost::any RationalLiteralExpression::accept(ExpressionVisitor& visitor) const { return visitor.visit(*this); } - double DoubleLiteralExpression::getValueAsDouble() const { + double RationalLiteralExpression::getValueAsDouble() const { return storm::utility::convertNumber(this->value); } - storm::RationalNumber DoubleLiteralExpression::getValue() const { + storm::RationalNumber RationalLiteralExpression::getValue() const { return this->value; } - void DoubleLiteralExpression::printToStream(std::ostream& stream) const { + void RationalLiteralExpression::printToStream(std::ostream& stream) const { stream << this->getValue(); } } diff --git a/src/storage/expressions/DoubleLiteralExpression.h b/src/storage/expressions/DoubleLiteralExpression.h index 1b6aa28b3..4eff900b2 100644 --- a/src/storage/expressions/DoubleLiteralExpression.h +++ b/src/storage/expressions/DoubleLiteralExpression.h @@ -1,5 +1,5 @@ -#ifndef STORM_STORAGE_EXPRESSIONS_DOUBLELITERALEXPRESSION_H_ -#define STORM_STORAGE_EXPRESSIONS_DOUBLELITERALEXPRESSION_H_ +#ifndef STORM_STORAGE_EXPRESSIONS_RationalLiteralExpression_H_ +#define STORM_STORAGE_EXPRESSIONS_RationalLiteralExpression_H_ #include "src/storage/expressions/BaseExpression.h" #include "src/utility/OsDetection.h" @@ -8,7 +8,7 @@ namespace storm { namespace expressions { - class DoubleLiteralExpression : public BaseExpression { + class RationalLiteralExpression : public BaseExpression { public: /*! * Creates an double literal expression with the given value. @@ -16,7 +16,7 @@ namespace storm { * @param manager The manager responsible for this expression. * @param value The value of the double literal. */ - DoubleLiteralExpression(ExpressionManager const& manager, double value); + RationalLiteralExpression(ExpressionManager const& manager, double value); /*! * Creates an double literal expression with the value given as a string. @@ -24,7 +24,7 @@ namespace storm { * @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); + RationalLiteralExpression(ExpressionManager const& manager, std::string const& valueAsString); /*! * Creates an double literal expression with the rational value. @@ -32,16 +32,16 @@ namespace storm { * @param manager The manager responsible for this expression. * @param value The rational number that is the value of this literal expression. */ - DoubleLiteralExpression(ExpressionManager const& manager, storm::RationalNumber const& value); + RationalLiteralExpression(ExpressionManager const& manager, storm::RationalNumber const& value); // Instantiate constructors and assignments with their default implementations. - DoubleLiteralExpression(DoubleLiteralExpression const& other) = default; - DoubleLiteralExpression& operator=(DoubleLiteralExpression const& other) = delete; + RationalLiteralExpression(RationalLiteralExpression const& other) = default; + RationalLiteralExpression& operator=(RationalLiteralExpression const& other) = delete; #ifndef WINDOWS - DoubleLiteralExpression(DoubleLiteralExpression&&) = default; - DoubleLiteralExpression& operator=(DoubleLiteralExpression&&) = delete; + RationalLiteralExpression(RationalLiteralExpression&&) = default; + RationalLiteralExpression& operator=(RationalLiteralExpression&&) = delete; #endif - virtual ~DoubleLiteralExpression() = default; + virtual ~RationalLiteralExpression() = default; // Override base class methods. virtual double evaluateAsDouble(Valuation const* valuation = nullptr) const override; @@ -75,4 +75,4 @@ namespace storm { } } -#endif /* STORM_STORAGE_EXPRESSIONS_DOUBLELITERALEXPRESSION_H_ */ \ No newline at end of file +#endif /* STORM_STORAGE_EXPRESSIONS_RationalLiteralExpression_H_ */ \ No newline at end of file diff --git a/src/storage/expressions/ExpressionManager.cpp b/src/storage/expressions/ExpressionManager.cpp index a92d908f3..ed51f76ee 100644 --- a/src/storage/expressions/ExpressionManager.cpp +++ b/src/storage/expressions/ExpressionManager.cpp @@ -65,11 +65,11 @@ namespace storm { } Expression ExpressionManager::rational(double value) const { - return Expression(std::shared_ptr(new DoubleLiteralExpression(*this, value))); + return Expression(std::shared_ptr(new RationalLiteralExpression(*this, value))); } Expression ExpressionManager::rational(storm::RationalNumber const& value) const { - return Expression(std::shared_ptr(new DoubleLiteralExpression(*this, value))); + return Expression(std::shared_ptr(new RationalLiteralExpression(*this, value))); } bool ExpressionManager::operator==(ExpressionManager const& other) const { diff --git a/src/storage/expressions/ExpressionVisitor.h b/src/storage/expressions/ExpressionVisitor.h index 5fdb486c2..1abafc2a6 100644 --- a/src/storage/expressions/ExpressionVisitor.h +++ b/src/storage/expressions/ExpressionVisitor.h @@ -15,7 +15,7 @@ namespace storm { class UnaryNumericalFunctionExpression; class BooleanLiteralExpression; class IntegerLiteralExpression; - class DoubleLiteralExpression; + class RationalLiteralExpression; class ExpressionVisitor { public: @@ -28,7 +28,7 @@ namespace storm { virtual boost::any visit(UnaryNumericalFunctionExpression const& expression) = 0; virtual boost::any visit(BooleanLiteralExpression const& expression) = 0; virtual boost::any visit(IntegerLiteralExpression const& expression) = 0; - virtual boost::any visit(DoubleLiteralExpression const& expression) = 0; + virtual boost::any visit(RationalLiteralExpression const& expression) = 0; }; } } diff --git a/src/storage/expressions/Expressions.h b/src/storage/expressions/Expressions.h index d670c29e3..655cc4aab 100644 --- a/src/storage/expressions/Expressions.h +++ b/src/storage/expressions/Expressions.h @@ -4,7 +4,7 @@ #include "src/storage/expressions/BinaryRelationExpression.h" #include "src/storage/expressions/BooleanLiteralExpression.h" #include "src/storage/expressions/IntegerLiteralExpression.h" -#include "src/storage/expressions/DoubleLiteralExpression.h" +#include "src/storage/expressions/RationalLiteralExpression.h" #include "src/storage/expressions/UnaryBooleanFunctionExpression.h" #include "src/storage/expressions/UnaryNumericalFunctionExpression.h" #include "src/storage/expressions/VariableExpression.h" diff --git a/src/storage/expressions/LinearCoefficientVisitor.cpp b/src/storage/expressions/LinearCoefficientVisitor.cpp index 3d881c25e..dc9a909f9 100644 --- a/src/storage/expressions/LinearCoefficientVisitor.cpp +++ b/src/storage/expressions/LinearCoefficientVisitor.cpp @@ -151,7 +151,7 @@ namespace storm { return VariableCoefficients(static_cast(expression.getValue())); } - boost::any LinearCoefficientVisitor::visit(DoubleLiteralExpression const& expression) { + boost::any LinearCoefficientVisitor::visit(RationalLiteralExpression const& expression) { return VariableCoefficients(expression.getValueAsDouble()); } } diff --git a/src/storage/expressions/LinearCoefficientVisitor.h b/src/storage/expressions/LinearCoefficientVisitor.h index b48c53d09..dea1bfc2e 100644 --- a/src/storage/expressions/LinearCoefficientVisitor.h +++ b/src/storage/expressions/LinearCoefficientVisitor.h @@ -75,7 +75,7 @@ namespace storm { virtual boost::any visit(UnaryNumericalFunctionExpression const& expression) override; virtual boost::any visit(BooleanLiteralExpression const& expression) override; virtual boost::any visit(IntegerLiteralExpression const& expression) override; - virtual boost::any visit(DoubleLiteralExpression const& expression) override; + virtual boost::any visit(RationalLiteralExpression const& expression) override; }; } } diff --git a/src/storage/expressions/LinearityCheckVisitor.cpp b/src/storage/expressions/LinearityCheckVisitor.cpp index 35e1e5c76..7a33a501a 100644 --- a/src/storage/expressions/LinearityCheckVisitor.cpp +++ b/src/storage/expressions/LinearityCheckVisitor.cpp @@ -85,7 +85,7 @@ namespace storm { return LinearityStatus::LinearWithoutVariables; } - boost::any LinearityCheckVisitor::visit(DoubleLiteralExpression const& expression) { + boost::any LinearityCheckVisitor::visit(RationalLiteralExpression const& expression) { return LinearityStatus::LinearWithoutVariables; } } diff --git a/src/storage/expressions/LinearityCheckVisitor.h b/src/storage/expressions/LinearityCheckVisitor.h index 2df8f8084..6bb35b7e8 100644 --- a/src/storage/expressions/LinearityCheckVisitor.h +++ b/src/storage/expressions/LinearityCheckVisitor.h @@ -29,7 +29,7 @@ namespace storm { virtual boost::any visit(UnaryNumericalFunctionExpression const& expression) override; virtual boost::any visit(BooleanLiteralExpression const& expression) override; virtual boost::any visit(IntegerLiteralExpression const& expression) override; - virtual boost::any visit(DoubleLiteralExpression const& expression) override; + virtual boost::any visit(RationalLiteralExpression const& expression) override; private: enum class LinearityStatus { NonLinear, LinearContainsVariables, LinearWithoutVariables }; diff --git a/src/storage/expressions/SubstitutionVisitor.cpp b/src/storage/expressions/SubstitutionVisitor.cpp index c736de156..1490e6f59 100644 --- a/src/storage/expressions/SubstitutionVisitor.cpp +++ b/src/storage/expressions/SubstitutionVisitor.cpp @@ -116,7 +116,7 @@ namespace storm { } template - boost::any SubstitutionVisitor::visit(DoubleLiteralExpression const& expression) { + boost::any SubstitutionVisitor::visit(RationalLiteralExpression const& expression) { return expression.getSharedPointer(); } diff --git a/src/storage/expressions/SubstitutionVisitor.h b/src/storage/expressions/SubstitutionVisitor.h index 343521335..5f1a93cb2 100644 --- a/src/storage/expressions/SubstitutionVisitor.h +++ b/src/storage/expressions/SubstitutionVisitor.h @@ -37,7 +37,7 @@ namespace storm { virtual boost::any visit(UnaryNumericalFunctionExpression const& expression) override; virtual boost::any visit(BooleanLiteralExpression const& expression) override; virtual boost::any visit(IntegerLiteralExpression const& expression) override; - virtual boost::any visit(DoubleLiteralExpression const& expression) override; + virtual boost::any visit(RationalLiteralExpression const& expression) override; private: // A mapping of variables to expressions with which they shall be replaced. diff --git a/src/storage/expressions/ToExprtkStringVisitor.cpp b/src/storage/expressions/ToExprtkStringVisitor.cpp index 51d9c1f34..1492aeae5 100644 --- a/src/storage/expressions/ToExprtkStringVisitor.cpp +++ b/src/storage/expressions/ToExprtkStringVisitor.cpp @@ -212,7 +212,7 @@ namespace storm { return boost::any(); } - boost::any ToExprtkStringVisitor::visit(DoubleLiteralExpression const& expression) { + boost::any ToExprtkStringVisitor::visit(RationalLiteralExpression const& expression) { stream << expression.getValue(); return boost::any(); } diff --git a/src/storage/expressions/ToExprtkStringVisitor.h b/src/storage/expressions/ToExprtkStringVisitor.h index 6c285ff28..d68da589d 100644 --- a/src/storage/expressions/ToExprtkStringVisitor.h +++ b/src/storage/expressions/ToExprtkStringVisitor.h @@ -25,7 +25,7 @@ namespace storm { virtual boost::any visit(UnaryNumericalFunctionExpression const& expression) override; virtual boost::any visit(BooleanLiteralExpression const& expression) override; virtual boost::any visit(IntegerLiteralExpression const& expression) override; - virtual boost::any visit(DoubleLiteralExpression const& expression) override; + virtual boost::any visit(RationalLiteralExpression const& expression) override; private: std::stringstream stream; diff --git a/src/storage/expressions/ToRationalFunctionVisitor.cpp b/src/storage/expressions/ToRationalFunctionVisitor.cpp index 533fa1f1f..60fecc08c 100644 --- a/src/storage/expressions/ToRationalFunctionVisitor.cpp +++ b/src/storage/expressions/ToRationalFunctionVisitor.cpp @@ -93,7 +93,7 @@ namespace storm { } template - boost::any ToRationalFunctionVisitor::visit(DoubleLiteralExpression const& expression) { + boost::any ToRationalFunctionVisitor::visit(RationalLiteralExpression const& expression) { return storm::utility::convertNumber(expression.getValue()); } diff --git a/src/storage/expressions/ToRationalFunctionVisitor.h b/src/storage/expressions/ToRationalFunctionVisitor.h index 12603f44e..1cda5028f 100644 --- a/src/storage/expressions/ToRationalFunctionVisitor.h +++ b/src/storage/expressions/ToRationalFunctionVisitor.h @@ -27,7 +27,7 @@ namespace storm { virtual boost::any visit(UnaryNumericalFunctionExpression const& expression) override; virtual boost::any visit(BooleanLiteralExpression const& expression) override; virtual boost::any visit(IntegerLiteralExpression const& expression) override; - virtual boost::any visit(DoubleLiteralExpression const& expression) override; + virtual boost::any visit(RationalLiteralExpression const& expression) override; private: template> = carl::dummy> diff --git a/src/storage/expressions/ToRationalNumberVisitor.cpp b/src/storage/expressions/ToRationalNumberVisitor.cpp index 44194cb4b..1b7319927 100644 --- a/src/storage/expressions/ToRationalNumberVisitor.cpp +++ b/src/storage/expressions/ToRationalNumberVisitor.cpp @@ -97,7 +97,7 @@ namespace storm { } template - boost::any ToRationalNumberVisitor::visit(DoubleLiteralExpression const& expression) { + boost::any ToRationalNumberVisitor::visit(RationalLiteralExpression const& expression) { #ifdef STORM_HAVE_CARL return expression.getValue(); #else diff --git a/src/storage/expressions/ToRationalNumberVisitor.h b/src/storage/expressions/ToRationalNumberVisitor.h index 2254931f6..3d53b8a87 100644 --- a/src/storage/expressions/ToRationalNumberVisitor.h +++ b/src/storage/expressions/ToRationalNumberVisitor.h @@ -25,7 +25,7 @@ namespace storm { virtual boost::any visit(UnaryNumericalFunctionExpression const& expression) override; virtual boost::any visit(BooleanLiteralExpression const& expression) override; virtual boost::any visit(IntegerLiteralExpression const& expression) override; - virtual boost::any visit(DoubleLiteralExpression const& expression) override; + virtual boost::any visit(RationalLiteralExpression const& expression) override; }; } } diff --git a/src/storage/expressions/UnaryNumericalFunctionExpression.cpp b/src/storage/expressions/UnaryNumericalFunctionExpression.cpp index fa7cad7e3..f5178fb6f 100644 --- a/src/storage/expressions/UnaryNumericalFunctionExpression.cpp +++ b/src/storage/expressions/UnaryNumericalFunctionExpression.cpp @@ -4,7 +4,7 @@ #include "src/storage/expressions/UnaryNumericalFunctionExpression.h" #include "src/storage/expressions/IntegerLiteralExpression.h" -#include "src/storage/expressions/DoubleLiteralExpression.h" +#include "src/storage/expressions/RationalLiteralExpression.h" #include "ExpressionVisitor.h" #include "src/utility/macros.h" #include "src/exceptions/InvalidTypeException.h" @@ -87,7 +87,7 @@ namespace storm { 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 DoubleLiteralExpression(this->getManager(), value)); + return std::shared_ptr(new RationalLiteralExpression(this->getManager(), value)); } }