From 7b2a667a9d28b0a81fef0f11116bb9dba652823d Mon Sep 17 00:00:00 2001 From: dehnert Date: Mon, 15 Aug 2016 16:53:56 +0200 Subject: [PATCH] double literal now stores rational internally Former-commit-id: c0f089b8baa1c6bef553889fb708f8a44cae1937 --- src/parser/ExpressionParser.cpp | 32 +++++++++++++++++-- src/parser/ExpressionParser.h | 16 ++++++++-- .../expressions/DoubleLiteralExpression.cpp | 4 +++ .../expressions/DoubleLiteralExpression.h | 8 +++++ src/storage/expressions/ExpressionManager.cpp | 4 +++ src/storage/expressions/ExpressionManager.h | 9 ++++++ 6 files changed, 69 insertions(+), 4 deletions(-) diff --git a/src/parser/ExpressionParser.cpp b/src/parser/ExpressionParser.cpp index 20982bd20..d556d799a 100644 --- a/src/parser/ExpressionParser.cpp +++ b/src/parser/ExpressionParser.cpp @@ -3,6 +3,34 @@ #include "src/exceptions/InvalidTypeException.h" #include "src/exceptions/WrongFormatException.h" +#include "src/utility/constants.h" + +namespace boost { + namespace spirit { + namespace traits { + template<> + bool scale(int exp, storm::RationalNumber& r, storm::RationalNumber acc) { + if (exp >= 0) { + r = acc * storm::utility::pow(storm::RationalNumber(10), static_cast(exp)); + } else { + r = acc / storm::utility::pow(storm::RationalNumber(10), static_cast(-exp)); + } + return true; + } + + template<> + bool is_equal_to_one(storm::RationalNumber const& value) { + return storm::utility::isOne(value); + } + + template<> + storm::RationalNumber negate(bool neg, storm::RationalNumber const& number) { + return neg ? storm::RationalNumber(-number) : number; + } + } + } +} + namespace storm { namespace parser { ExpressionParser::ExpressionParser(storm::expressions::ExpressionManager const& manager, qi::symbols const& invalidIdentifiers_, bool enableErrorHandling, bool allowBacktracking) : ExpressionParser::base_type(expression), orOperator_(), andOperator_(), equalityOperator_(), relationalOperator_(), plusOperator_(), multiplicationOperator_(), infixPowerOperator_(), unaryOperator_(), floorCeilOperator_(), minMaxOperator_(), prefixPowerOperator_(), trueFalse_(manager), manager(manager.getSharedPointer()), createExpressions(false), acceptDoubleLiterals(true), identifiers_(nullptr), invalidIdentifiers_(invalidIdentifiers_) { @@ -33,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] | strict_double[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::createDoubleLiteralExpression, 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; @@ -295,7 +323,7 @@ namespace storm { return manager->boolean(false); } - storm::expressions::Expression ExpressionParser::createDoubleLiteralExpression(double value, bool& pass) const { + storm::expressions::Expression ExpressionParser::createDoubleLiteralExpression(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 66d851707..c728e0b84 100644 --- a/src/parser/ExpressionParser.h +++ b/src/parser/ExpressionParser.h @@ -8,8 +8,20 @@ #include "src/storage/expressions/Expression.h" #include "src/storage/expressions/ExpressionManager.h" +#include "src/adapters/CarlAdapter.h" + namespace storm { namespace parser { + template + struct RationalPolicies : boost::spirit::qi::strict_real_policies { + static const bool expect_dot = true; + + template + static bool parse_nan(It&, It const&, Attr&) { return false; } + template + static bool parse_inf(It&, It const&, Attr&) { return false; } + }; + class ExpressionParser : public qi::grammar { public: /*! @@ -236,7 +248,7 @@ namespace storm { qi::rule identifier; // Parser that is used to recognize doubles only (as opposed to Spirit's double_ parser). - boost::spirit::qi::real_parser> strict_double; + boost::spirit::qi::real_parser> rationalLiteral_; // Helper functions to create expressions. storm::expressions::Expression createIteExpression(storm::expressions::Expression e1, storm::expressions::Expression e2, storm::expressions::Expression e3, bool& pass) const; @@ -248,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(double value, bool& pass) const; + storm::expressions::Expression createDoubleLiteralExpression(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/DoubleLiteralExpression.cpp b/src/storage/expressions/DoubleLiteralExpression.cpp index 192d747ee..86a2ba889 100644 --- a/src/storage/expressions/DoubleLiteralExpression.cpp +++ b/src/storage/expressions/DoubleLiteralExpression.cpp @@ -14,6 +14,10 @@ namespace storm { // Intentionally left empty. } + DoubleLiteralExpression::DoubleLiteralExpression(ExpressionManager const& manager, storm::RationalNumber const& value) : BaseExpression(manager, manager.getRationalType()), value(value) { + // Intentionally left empty. + } + double DoubleLiteralExpression::evaluateAsDouble(Valuation const* valuation) const { return this->getValueAsDouble(); } diff --git a/src/storage/expressions/DoubleLiteralExpression.h b/src/storage/expressions/DoubleLiteralExpression.h index 6a04f23e3..1b6aa28b3 100644 --- a/src/storage/expressions/DoubleLiteralExpression.h +++ b/src/storage/expressions/DoubleLiteralExpression.h @@ -26,6 +26,14 @@ namespace storm { */ DoubleLiteralExpression(ExpressionManager const& manager, std::string const& valueAsString); + /*! + * Creates an double literal expression with the rational value. + * + * @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); + // Instantiate constructors and assignments with their default implementations. DoubleLiteralExpression(DoubleLiteralExpression const& other) = default; DoubleLiteralExpression& operator=(DoubleLiteralExpression const& other) = delete; diff --git a/src/storage/expressions/ExpressionManager.cpp b/src/storage/expressions/ExpressionManager.cpp index d1add4402..a92d908f3 100644 --- a/src/storage/expressions/ExpressionManager.cpp +++ b/src/storage/expressions/ExpressionManager.cpp @@ -68,6 +68,10 @@ namespace storm { return Expression(std::shared_ptr(new DoubleLiteralExpression(*this, value))); } + Expression ExpressionManager::rational(storm::RationalNumber const& value) const { + return Expression(std::shared_ptr(new DoubleLiteralExpression(*this, value))); + } + bool ExpressionManager::operator==(ExpressionManager const& other) const { return this == &other; } diff --git a/src/storage/expressions/ExpressionManager.h b/src/storage/expressions/ExpressionManager.h index 6fee92fd6..f3ec7e76b 100644 --- a/src/storage/expressions/ExpressionManager.h +++ b/src/storage/expressions/ExpressionManager.h @@ -10,6 +10,7 @@ #include "src/storage/expressions/Variable.h" #include "src/storage/expressions/Expression.h" +#include "src/adapters/CarlAdapter.h" #include "src/utility/OsDetection.h" namespace storm { @@ -104,6 +105,14 @@ namespace storm { * @return The resulting expression. */ Expression rational(double value) const; + + /*! + * Creates an expression that characterizes the given rational literal. + * + * @param value The value of the rational literal. + * @return The resulting expression. + */ + Expression rational(storm::RationalNumber const& value) const; /*! * Compares the two expression managers for equality, which holds iff they are the very same object.