renamed double literal to rational literal

Former-commit-id: 7bafe79eed

src/adapters/AddExpressionAdapter.cpp

@@ -194,7 +194,7 @@ namespace storm {
         }
         
         template<storm::dd::DdType Type, typename ValueType>
-        boost::any AddExpressionAdapter<Type, ValueType>::visit(storm::expressions::DoubleLiteralExpression const& expression) {
+        boost::any AddExpressionAdapter<Type, ValueType>::visit(storm::expressions::RationalLiteralExpression const& expression) {
             return ddManager->getConstant(static_cast<ValueType>(expression.getValueAsDouble()));
         }
         

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.

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

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

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;
             

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;

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<storm::expressions::OperatorType> 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;

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<int_fast64_t>(std::pow(firstOperandEvaluation, secondOperandEvaluation)); break;
                         case OperatorType::Divide: STORM_LOG_THROW(false, storm::exceptions::InvalidStateException, "Unable to simplify division."); break;
                     }
-                    return std::shared_ptr<BaseExpression>(new DoubleLiteralExpression(this->getManager(), newValue));
+                    return std::shared_ptr<BaseExpression>(new RationalLiteralExpression(this->getManager(), newValue));
                 }
             }
             

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<storm::RationalNumber>(value)) {
+        RationalLiteralExpression::RationalLiteralExpression(ExpressionManager const& manager, double value) : BaseExpression(manager, manager.getRationalType()), value(storm::utility::convertNumber<storm::RationalNumber>(value)) {
             // Intentionally left empty.
         }
         
-        DoubleLiteralExpression::DoubleLiteralExpression(ExpressionManager const& manager, std::string const& valueAsString) : BaseExpression(manager, manager.getRationalType()), value(storm::utility::convertNumber<storm::RationalNumber>(valueAsString)) {
+        RationalLiteralExpression::RationalLiteralExpression(ExpressionManager const& manager, std::string const& valueAsString) : BaseExpression(manager, manager.getRationalType()), value(storm::utility::convertNumber<storm::RationalNumber>(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<storm::expressions::Variable>& variables) const {
+        void RationalLiteralExpression::gatherVariables(std::set<storm::expressions::Variable>& variables) const {
             return;
 		}
         
-        std::shared_ptr<BaseExpression const> DoubleLiteralExpression::simplify() const {
+        std::shared_ptr<BaseExpression const> 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<double>(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();
         }
     }

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_ */
+#endif /* STORM_STORAGE_EXPRESSIONS_RationalLiteralExpression_H_ */

src/storage/expressions/ExpressionManager.cpp

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

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

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"

src/storage/expressions/LinearCoefficientVisitor.cpp

@@ -151,7 +151,7 @@ namespace storm {
             return VariableCoefficients(static_cast<double>(expression.getValue()));
         }
         
-        boost::any LinearCoefficientVisitor::visit(DoubleLiteralExpression const& expression) {
+        boost::any LinearCoefficientVisitor::visit(RationalLiteralExpression const& expression) {
             return VariableCoefficients(expression.getValueAsDouble());
         }
     }

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

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

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

src/storage/expressions/SubstitutionVisitor.cpp

@@ -116,7 +116,7 @@ namespace storm {
         }
         
 		template<typename MapType>
-        boost::any SubstitutionVisitor<MapType>::visit(DoubleLiteralExpression const& expression) {
+        boost::any SubstitutionVisitor<MapType>::visit(RationalLiteralExpression const& expression) {
             return expression.getSharedPointer();
         }
         

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.

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

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;

src/storage/expressions/ToRationalFunctionVisitor.cpp

@@ -93,7 +93,7 @@ namespace storm {
         }
         
         template<typename RationalFunctionType>
-        boost::any ToRationalFunctionVisitor<RationalFunctionType>::visit(DoubleLiteralExpression const& expression) {
+        boost::any ToRationalFunctionVisitor<RationalFunctionType>::visit(RationalLiteralExpression const& expression) {
             return storm::utility::convertNumber<storm::RationalFunction>(expression.getValue());
         }
 

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<typename TP = typename RationalFunctionType::PolyType, carl::EnableIf<carl::needs_cache<TP>> = carl::dummy>

src/storage/expressions/ToRationalNumberVisitor.cpp

@@ -97,7 +97,7 @@ namespace storm {
         }
         
         template<typename RationalNumberType>
-        boost::any ToRationalNumberVisitor<RationalNumberType>::visit(DoubleLiteralExpression const& expression) {
+        boost::any ToRationalNumberVisitor<RationalNumberType>::visit(RationalLiteralExpression const& expression) {
 #ifdef STORM_HAVE_CARL
             return expression.getValue();
 #else

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

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<double>(operandEvaluation)); break;
                         case OperatorType::Ceil: value = std::ceil(boost::get<double>(operandEvaluation)); break;
                     }
-                    return std::shared_ptr<BaseExpression>(new DoubleLiteralExpression(this->getManager(), value));
+                    return std::shared_ptr<BaseExpression>(new RationalLiteralExpression(this->getManager(), value));
                 }
             }