Improved simplify a bit.

Former-commit-id: bfdfa5bfbb

src/storage/expressions/BinaryBooleanFunctionExpression.cpp

@@ -22,7 +22,7 @@ namespace storm {
                 case OperatorType::Iff: return storm::expressions::OperatorType::Iff; break;
             }
         }
-                
+        
         bool BinaryBooleanFunctionExpression::evaluateAsBool(Valuation const* valuation) const {
             STORM_LOG_THROW(this->hasBooleanType(), storm::exceptions::InvalidTypeException, "Unable to evaluate expression as boolean.");
             
@@ -40,47 +40,53 @@ namespace storm {
             
             return result;
         }
-                
+        
         std::shared_ptr<BaseExpression const> BinaryBooleanFunctionExpression::simplify() const {
             std::shared_ptr<BaseExpression const> firstOperandSimplified = this->getFirstOperand()->simplify();
             std::shared_ptr<BaseExpression const> secondOperandSimplified = this->getSecondOperand()->simplify();
             
-            switch (this->getOperatorType()) {
-                case OperatorType::And: if (firstOperandSimplified->isTrue()) {
-                    return secondOperandSimplified;
-                } else if (firstOperandSimplified->isFalse()) {
-                    return firstOperandSimplified;
-                } else if (secondOperandSimplified->isTrue()) {
-                    return firstOperandSimplified;
-                } else if (secondOperandSimplified->isFalse()) {
-                    return secondOperandSimplified;
-                }
-                break;
-                case OperatorType::Or: if (firstOperandSimplified->isTrue()) {
-                    return firstOperandSimplified;
-                } else if (firstOperandSimplified->isFalse()) {
-                    return secondOperandSimplified;
-                } else if (secondOperandSimplified->isTrue()) {
-                    return secondOperandSimplified;
-                } else if (secondOperandSimplified->isFalse()) {
-                    return firstOperandSimplified;
-                }
-                break;
-                case OperatorType::Xor: break;
-                case OperatorType::Implies: if (firstOperandSimplified->isTrue()) {
-                    return secondOperandSimplified;
-                } else if (firstOperandSimplified->isFalse()) {
-                    return std::shared_ptr<BaseExpression>(new BooleanLiteralExpression(this->getManager(), true));
-                } else if (secondOperandSimplified->isTrue()) {
-                    return std::shared_ptr<BaseExpression>(new BooleanLiteralExpression(this->getManager(), true));
-                }
-                break;
-                case OperatorType::Iff: if (firstOperandSimplified->isTrue() && secondOperandSimplified->isTrue()) {
-                    return std::shared_ptr<BaseExpression>(new BooleanLiteralExpression(this->getManager(), true));
-                } else if (firstOperandSimplified->isFalse() && secondOperandSimplified->isFalse()) {
-                    return std::shared_ptr<BaseExpression>(new BooleanLiteralExpression(this->getManager(), true));
+            if (firstOperandSimplified->isLiteral() && secondOperandSimplified->isLiteral()) {
+                switch (this->getOperatorType()) {
+                    case OperatorType::And:
+                        if (firstOperandSimplified->isTrue()) {
+                            return secondOperandSimplified;
+                        } else if (firstOperandSimplified->isFalse()) {
+                            return firstOperandSimplified;
+                        } else if (secondOperandSimplified->isTrue()) {
+                            return firstOperandSimplified;
+                        } else if (secondOperandSimplified->isFalse()) {
+                            return secondOperandSimplified;
+                        }
+                        break;
+                    case OperatorType::Or:
+                        if (firstOperandSimplified->isTrue()) {
+                            return firstOperandSimplified;
+                        } else if (firstOperandSimplified->isFalse()) {
+                            return secondOperandSimplified;
+                        } else if (secondOperandSimplified->isTrue()) {
+                            return secondOperandSimplified;
+                        } else if (secondOperandSimplified->isFalse()) {
+                            return firstOperandSimplified;
+                        }
+                        break;
+                    case OperatorType::Xor: break;
+                    case OperatorType::Implies:
+                        if (firstOperandSimplified->isTrue()) {
+                            return secondOperandSimplified;
+                        } else if (firstOperandSimplified->isFalse()) {
+                            return std::shared_ptr<BaseExpression>(new BooleanLiteralExpression(this->getManager(), true));
+                        } else if (secondOperandSimplified->isTrue()) {
+                            return std::shared_ptr<BaseExpression>(new BooleanLiteralExpression(this->getManager(), true));
+                        }
+                        break;
+                    case OperatorType::Iff:
+                        if (firstOperandSimplified->isTrue() && secondOperandSimplified->isTrue()) {
+                            return std::shared_ptr<BaseExpression>(new BooleanLiteralExpression(this->getManager(), true));
+                        } else if (firstOperandSimplified->isFalse() && secondOperandSimplified->isFalse()) {
+                            return std::shared_ptr<BaseExpression>(new BooleanLiteralExpression(this->getManager(), true));
+                        }
+                        break;
                 }
-                break;
             }
             
             // If the two successors remain unchanged, we can return a shared_ptr to this very object.

src/storage/expressions/BinaryNumericalFunctionExpression.cpp

@@ -2,6 +2,8 @@
 #include <cmath>
 
 #include "src/storage/expressions/BinaryNumericalFunctionExpression.h"
+#include "src/storage/expressions/IntegerLiteralExpression.h"
+#include "src/storage/expressions/DoubleLiteralExpression.h"
 #include "src/utility/macros.h"
 #include "src/exceptions/InvalidTypeException.h"
 
@@ -49,12 +51,12 @@ namespace storm {
             double firstOperandEvaluation = this->getFirstOperand()->evaluateAsDouble(valuation);
             double secondOperandEvaluation = this->getSecondOperand()->evaluateAsDouble(valuation);
             switch (this->getOperatorType()) {
-                case OperatorType::Plus: return static_cast<double>(firstOperandEvaluation + secondOperandEvaluation); break;
-                case OperatorType::Minus: return static_cast<double>(firstOperandEvaluation - secondOperandEvaluation); break;
-                case OperatorType::Times: return static_cast<double>(firstOperandEvaluation * secondOperandEvaluation); break;
-                case OperatorType::Divide: return static_cast<double>(firstOperandEvaluation / secondOperandEvaluation); break;
-                case OperatorType::Min: return static_cast<double>(std::min(firstOperandEvaluation, secondOperandEvaluation)); break;
-                case OperatorType::Max: return static_cast<double>(std::max(firstOperandEvaluation, secondOperandEvaluation)); break;
+                case OperatorType::Plus: return firstOperandEvaluation + secondOperandEvaluation; break;
+                case OperatorType::Minus: return firstOperandEvaluation - secondOperandEvaluation; break;
+                case OperatorType::Times: return firstOperandEvaluation * secondOperandEvaluation; break;
+                case OperatorType::Divide: return firstOperandEvaluation / secondOperandEvaluation; break;
+                case OperatorType::Min: return std::min(firstOperandEvaluation, secondOperandEvaluation); break;
+                case OperatorType::Max: return std::max(firstOperandEvaluation, secondOperandEvaluation); break;
                 case OperatorType::Power: return std::pow(firstOperandEvaluation, secondOperandEvaluation); break;
             }
         }
@@ -63,6 +65,38 @@ namespace storm {
             std::shared_ptr<BaseExpression const> firstOperandSimplified = this->getFirstOperand()->simplify();
             std::shared_ptr<BaseExpression const> secondOperandSimplified = this->getSecondOperand()->simplify();
             
+            if (firstOperandSimplified->isLiteral() && secondOperandSimplified->isLiteral()) {
+                if (this->hasIntegerType()) {
+                    int_fast64_t firstOperandEvaluation = firstOperandSimplified->evaluateAsInt();
+                    int_fast64_t secondOperandEvaluation = secondOperandSimplified->evaluateAsInt();
+                    int_fast64_t newValue = 0;
+                    switch (this->getOperatorType()) {
+                        case OperatorType::Plus: newValue = firstOperandEvaluation + secondOperandEvaluation; break;
+                        case OperatorType::Minus: newValue = firstOperandEvaluation - secondOperandEvaluation; break;
+                        case OperatorType::Times: newValue = firstOperandEvaluation * secondOperandEvaluation; break;
+                        case OperatorType::Divide: newValue = firstOperandEvaluation / secondOperandEvaluation; break;
+                        case OperatorType::Min: newValue = std::min(firstOperandEvaluation, secondOperandEvaluation); break;
+                        case OperatorType::Max: newValue = std::max(firstOperandEvaluation, secondOperandEvaluation); break;
+                        case OperatorType::Power: newValue = static_cast<int_fast64_t>(std::pow(firstOperandEvaluation, secondOperandEvaluation)); break;
+                    }
+                    return std::shared_ptr<BaseExpression>(new IntegerLiteralExpression(this->getManager(), newValue));
+                } else if (this->hasRationalType()) {
+                    double firstOperandEvaluation = firstOperandSimplified->evaluateAsDouble();
+                    double secondOperandEvaluation = secondOperandSimplified->evaluateAsDouble();
+                    double newValue = 0;
+                    switch (this->getOperatorType()) {
+                        case OperatorType::Plus: newValue = firstOperandEvaluation + secondOperandEvaluation; break;
+                        case OperatorType::Minus: newValue = firstOperandEvaluation - secondOperandEvaluation; break;
+                        case OperatorType::Times: newValue = firstOperandEvaluation * secondOperandEvaluation; break;
+                        case OperatorType::Divide: newValue = firstOperandEvaluation / secondOperandEvaluation; break;
+                        case OperatorType::Min: newValue = std::min(firstOperandEvaluation, secondOperandEvaluation); break;
+                        case OperatorType::Max: newValue = std::max(firstOperandEvaluation, secondOperandEvaluation); break;
+                        case OperatorType::Power: newValue = static_cast<int_fast64_t>(std::pow(firstOperandEvaluation, secondOperandEvaluation)); break;
+                    }
+                    return std::shared_ptr<BaseExpression>(new DoubleLiteralExpression(this->getManager(), newValue));
+                }
+            }
+            
             if (firstOperandSimplified.get() == this->getFirstOperand().get() && secondOperandSimplified.get() == this->getSecondOperand().get()) {
                 return this->shared_from_this();
             } else {

src/storage/expressions/BinaryRelationExpression.cpp

@@ -1,5 +1,8 @@
 #include "src/storage/expressions/BinaryRelationExpression.h"
 
+#include <boost/variant.hpp>
+
+#include "src/storage/expressions/BooleanLiteralExpression.h"
 #include "src/utility/macros.h"
 #include "src/exceptions/InvalidTypeException.h"
 
@@ -22,7 +25,7 @@ namespace storm {
         
         bool BinaryRelationExpression::evaluateAsBool(Valuation const* valuation) const {
             STORM_LOG_THROW(this->hasBooleanType(), storm::exceptions::InvalidTypeException, "Unable to evaluate expression as boolean.");
-
+            
             double firstOperandEvaluated = this->getFirstOperand()->evaluateAsDouble(valuation);
             double secondOperandEvaluated = this->getSecondOperand()->evaluateAsDouble(valuation);
             switch (this->getRelationType()) {
@@ -39,6 +42,33 @@ namespace storm {
             std::shared_ptr<BaseExpression const> firstOperandSimplified = this->getFirstOperand()->simplify();
             std::shared_ptr<BaseExpression const> secondOperandSimplified = this->getSecondOperand()->simplify();
             
+            if (firstOperandSimplified->isLiteral() && secondOperandSimplified->isLiteral()) {
+                boost::variant<int_fast64_t, double> firstOperandEvaluation;
+                boost::variant<int_fast64_t, double> secondOperandEvaluation;
+                
+                if (firstOperandSimplified->hasIntegerType()) {
+                    firstOperandEvaluation = firstOperandSimplified->evaluateAsInt();
+                } else {
+                    firstOperandEvaluation = firstOperandSimplified->evaluateAsDouble();
+                }
+                if (secondOperandSimplified->hasIntegerType()) {
+                    secondOperandEvaluation = secondOperandSimplified->evaluateAsInt();
+                } else {
+                    secondOperandEvaluation = secondOperandSimplified->evaluateAsDouble();
+                }
+                
+                bool truthValue = false;
+                switch (this->getRelationType()) {
+                    case RelationType::Equal: truthValue = (firstOperandSimplified->hasIntegerType() ? boost::get<int_fast64_t>(firstOperandEvaluation) : boost::get<double>(firstOperandEvaluation)) == (secondOperandSimplified->hasIntegerType() ? boost::get<int_fast64_t>(secondOperandEvaluation) : boost::get<double>(secondOperandEvaluation)); break;
+                    case RelationType::NotEqual: truthValue = (firstOperandSimplified->hasIntegerType() ? boost::get<int_fast64_t>(firstOperandEvaluation) : boost::get<double>(firstOperandEvaluation)) != (secondOperandSimplified->hasIntegerType() ? boost::get<int_fast64_t>(secondOperandEvaluation) : boost::get<double>(secondOperandEvaluation)); break;
+                    case RelationType::Greater: truthValue = (firstOperandSimplified->hasIntegerType() ? boost::get<int_fast64_t>(firstOperandEvaluation) : boost::get<double>(firstOperandEvaluation)) > (secondOperandSimplified->hasIntegerType() ? boost::get<int_fast64_t>(secondOperandEvaluation) : boost::get<double>(secondOperandEvaluation)); break;
+                    case RelationType::GreaterOrEqual: truthValue = (firstOperandSimplified->hasIntegerType() ? boost::get<int_fast64_t>(firstOperandEvaluation) : boost::get<double>(firstOperandEvaluation)) >= (secondOperandSimplified->hasIntegerType() ? boost::get<int_fast64_t>(secondOperandEvaluation) : boost::get<double>(secondOperandEvaluation)); break;
+                    case RelationType::Less: truthValue = (firstOperandSimplified->hasIntegerType() ? boost::get<int_fast64_t>(firstOperandEvaluation) : boost::get<double>(firstOperandEvaluation)) < (secondOperandSimplified->hasIntegerType() ? boost::get<int_fast64_t>(secondOperandEvaluation) : boost::get<double>(secondOperandEvaluation)); break;
+                    case RelationType::LessOrEqual: truthValue = (firstOperandSimplified->hasIntegerType() ? boost::get<int_fast64_t>(firstOperandEvaluation) : boost::get<double>(firstOperandEvaluation)) <= (secondOperandSimplified->hasIntegerType() ? boost::get<int_fast64_t>(secondOperandEvaluation) : boost::get<double>(secondOperandEvaluation)); break;
+                }
+                return std::shared_ptr<BaseExpression>(new BooleanLiteralExpression(this->getManager(), truthValue));
+            }
+            
             if (firstOperandSimplified.get() == this->getFirstOperand().get() && secondOperandSimplified.get() == this->getSecondOperand().get()) {
                 return this->shared_from_this();
             } else {

src/storage/expressions/Expression.cpp

@@ -50,7 +50,7 @@ namespace storm {
             return this->getBaseExpression().evaluateAsDouble(valuation);
         }
         
-        Expression Expression::simplify() {
+        Expression Expression::simplify() const {
             return Expression(this->getBaseExpression().simplify());
         }
         

src/storage/expressions/Expression.h

@@ -115,7 +115,7 @@ namespace storm {
              *
              * @return The simplified expression.
              */
-            Expression simplify();
+            Expression simplify() const;
             
             /*!
              * Retrieves the operator of a function application. This is only legal to call if the expression is

src/storage/expressions/UnaryBooleanFunctionExpression.cpp

@@ -33,7 +33,7 @@ namespace storm {
             switch (this->getOperatorType()) {
                 case OperatorType::Not: if (operandSimplified->isTrue()) {
                     return std::shared_ptr<BaseExpression>(new BooleanLiteralExpression(this->getManager(), false));
-                } else {
+                } else if (operandSimplified->isFalse()) {
                     return std::shared_ptr<BaseExpression>(new BooleanLiteralExpression(this->getManager(), true));
                 }
             }

src/storage/expressions/UnaryNumericalFunctionExpression.cpp

@@ -1,6 +1,10 @@
 #include <cmath>
 
+#include <boost/variant.hpp>
+
 #include "src/storage/expressions/UnaryNumericalFunctionExpression.h"
+#include "src/storage/expressions/IntegerLiteralExpression.h"
+#include "src/storage/expressions/DoubleLiteralExpression.h"
 #include "src/utility/macros.h"
 #include "src/exceptions/InvalidTypeException.h"
 
@@ -47,6 +51,29 @@ namespace storm {
         std::shared_ptr<BaseExpression const> UnaryNumericalFunctionExpression::simplify() const {
             std::shared_ptr<BaseExpression const> operandSimplified = this->getOperand()->simplify();
             
+            if (operandSimplified->isLiteral()) {
+                boost::variant<int_fast64_t, double> operandEvaluation;
+
+                if (operandSimplified->hasIntegerType()) {
+                    operandEvaluation = operandSimplified->evaluateAsInt();
+                } else {
+                    operandEvaluation = operandSimplified->evaluateAsDouble();
+                }
+                
+                boost::variant<int_fast64_t, double> result;
+                switch (this->getOperatorType()) {
+                    case OperatorType::Minus: result = -(operandSimplified->hasIntegerType() ? boost::get<int_fast64_t>(operandEvaluation) : boost::get<double>(operandEvaluation)); break;
+                    case OperatorType::Floor: result = std::floor(operandSimplified->hasIntegerType() ? boost::get<int_fast64_t>(operandEvaluation) : boost::get<double>(operandEvaluation)); break;
+                    case OperatorType::Ceil: result = std::ceil(operandSimplified->hasIntegerType() ? boost::get<int_fast64_t>(operandEvaluation) : boost::get<double>(operandEvaluation)); break;
+                }
+                
+                if (result.type() == typeid(int_fast64_t)) {
+                    return std::shared_ptr<BaseExpression>(new IntegerLiteralExpression(this->getManager(), boost::get<int_fast64_t>(result)));
+                } else {
+                    return std::shared_ptr<BaseExpression>(new DoubleLiteralExpression(this->getManager(), boost::get<double>(result)));
+                }
+            }
+            
             if (operandSimplified.get() == this->getOperand().get()) {
                 return this->shared_from_this();
             } else {

src/storage/prism/Program.cpp

@@ -291,7 +291,7 @@ namespace storm {
                 STORM_LOG_THROW(constant.isDefined(), storm::exceptions::InvalidArgumentException, "Cannot substitute constants in program that contains undefined constants.");
                 
                 // Put the corresponding expression in the substitution.
-                constantSubstitution.emplace(constant.getExpressionVariable(), constant.getExpression());
+                constantSubstitution.emplace(constant.getExpressionVariable(), constant.getExpression().simplify());
                 
                 // If there is at least one more constant to come, we substitute the costants we have so far.
                 if (constantIndex + 1 < newConstants.size()) {