double literal now stores rational internally

Former-commit-id: c0f089b8ba

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<uint_fast64_t>(exp));
+                } else {
+                    r = acc / storm::utility::pow(storm::RationalNumber(10), static_cast<uint_fast64_t>(-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<char, uint_fast64_t> 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;

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<typename NumberType>
+        struct RationalPolicies : boost::spirit::qi::strict_real_policies<NumberType> {
+            static const bool expect_dot = true;
+            
+            template <typename It, typename Attr>
+            static bool parse_nan(It&, It const&, Attr&) { return false; }
+            template <typename It, typename Attr>
+            static bool parse_inf(It&, It const&, Attr&) { return false; }
+        };
+        
         class ExpressionParser : public qi::grammar<Iterator, storm::expressions::Expression(), Skipper> {
         public:
             /*!
@@ -236,7 +248,7 @@ namespace storm {
             qi::rule<Iterator, std::string(), Skipper> identifier;
             
             // Parser that is used to recognize doubles only (as opposed to Spirit's double_ parser).
-            boost::spirit::qi::real_parser<double, boost::spirit::qi::strict_real_policies<double>> strict_double;
+            boost::spirit::qi::real_parser<storm::RationalNumber, RationalPolicies<storm::RationalNumber>> 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<storm::expressions::OperatorType> 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;

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();
         }

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;

src/storage/expressions/ExpressionManager.cpp

@@ -68,6 +68,10 @@ namespace storm {
             return Expression(std::shared_ptr<BaseExpression>(new DoubleLiteralExpression(*this, value)));
         }
         
+        Expression ExpressionManager::rational(storm::RationalNumber const& value) const {
+            return Expression(std::shared_ptr<BaseExpression>(new DoubleLiteralExpression(*this, value)));
+        }
+        
         bool ExpressionManager::operator==(ExpressionManager const& other) const {
             return this == &other;
         }

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 {
@@ -105,6 +106,14 @@ namespace storm {
              */
             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.
              */