Reducing the nesting when creating a expression::sum(...).

src/storm/modelchecker/multiobjective/constraintbased/SparseCbAchievabilityQuery.cpp

@@ -9,7 +9,6 @@
 #include "storm/utility/vector.h"
 #include "storm/utility/solver.h"
 #include "storm/utility/Stopwatch.h"
-#include "storm/utility/ExpressionHelper.h"
 #include "storm/settings/SettingsManager.h"
 #include "storm/settings/modules/GeneralSettings.h"
 #include "storm/settings/modules/CoreSettings.h"
@@ -82,7 +81,7 @@ namespace storm {
                 uint_fast64_t numStates = this->preprocessedModel->getNumberOfStates();
                 uint_fast64_t numChoices = this->preprocessedModel->getNumberOfChoices();
                 uint_fast64_t numBottomStates = this->reward0EStates.getNumberOfSetBits();
-                
+                STORM_LOG_THROW(numBottomStates > 0, storm::exceptions::UnexpectedException, "No bottom states in the preprocessed model.");
                 storm::expressions::Expression zero = this->expressionManager->rational(storm::utility::zero<ValueType>());
                 storm::expressions::Expression one = this->expressionManager->rational(storm::utility::one<ValueType>());
                 
@@ -106,7 +105,7 @@ namespace storm {
                     solver->add(var.getExpression() >= zero);
                     bottomStateVarsAsExpression.push_back(var.getExpression());
                 }
-                auto bottomStateSum = storm::utility::ExpressionHelper(this->expressionManager).sum(std::move(bottomStateVarsAsExpression));
+                auto bottomStateSum = storm::expressions::sum(bottomStateVarsAsExpression).simplify();
                 solver->add(bottomStateSum == one);
                 
                 // assert that the "incoming" value of each state equals the "outgoing" value
@@ -149,7 +148,10 @@ namespace storm {
                             objectiveValues.push_back(this->expressionManager->rational(rewards[choice]) * expectedChoiceVariables[choice].getExpression());
                         }
                     }
-                    auto objValue = storm::utility::ExpressionHelper(this->expressionManager).sum(std::move(objectiveValues));
+                    if (objectiveValues.empty()) {
+                        objectiveValues.push_back(this->expressionManager->rational(storm::utility::zero<storm::RationalNumber>()));
+                    }
+                    auto objValue = storm::expressions::sum(objectiveValues).simplify();
                     
                     // We need to actually evaluate the threshold as rational number. Otherwise a threshold like '<=16/9' might be considered as 1 due to integer division
                     storm::expressions::Expression threshold = this->expressionManager->rational(obj.formula->getThreshold().evaluateAsRational());

src/storm/modelchecker/prctl/helper/rewardbounded/CostLimitClosure.cpp

@@ -1,4 +1,3 @@
-#include <storm/utility/ExpressionHelper.h>
 #include "storm/modelchecker/prctl/helper/rewardbounded/CostLimitClosure.h"
 #include "storm/utility/macros.h"
 #include "storm/exceptions/IllegalArgumentException.h"

src/storm/storage/expressions/Expression.cpp

@@ -436,19 +436,19 @@ namespace storm {
         }
 
         Expression disjunction(std::vector<storm::expressions::Expression> const& expressions) {
-            return apply(expressions, [] (Expression const& e1, Expression const& e2) { return e1 || e2; });
+            return applyAssociative(expressions, [] (Expression const& e1, Expression const& e2) { return e1 || e2; });
         }
 
         Expression conjunction(std::vector<storm::expressions::Expression> const& expressions) {
-            return apply(expressions, [] (Expression const& e1, Expression const& e2) { return e1 && e2; });
+            return applyAssociative(expressions, [] (Expression const& e1, Expression const& e2) { return e1 && e2; });
         }
         
         Expression sum(std::vector<storm::expressions::Expression> const& expressions) {
-            return apply(expressions, [] (Expression const& e1, Expression const& e2) { return e1 + e2; });
+            return applyAssociative(expressions, [] (Expression const& e1, Expression const& e2) { return e1 + e2; });
         }
         
         Expression apply(std::vector<storm::expressions::Expression> const& expressions, std::function<Expression (Expression const&, Expression const&)> const& function) {
-            STORM_LOG_THROW(!expressions.empty(), storm::exceptions::InvalidArgumentException, "Cannot build disjunction of empty expression list.");
+            STORM_LOG_THROW(!expressions.empty(), storm::exceptions::InvalidArgumentException, "Cannot build function application of empty expression list.");
             auto it = expressions.begin();
             auto ite = expressions.end();
             Expression result = *it;
@@ -460,5 +460,45 @@ namespace storm {
             
             return result;
         }
+        
+        Expression applyAssociative(std::vector<storm::expressions::Expression> const& expressions, std::function<Expression (Expression const&, Expression const&)> const& function) {
+            STORM_LOG_THROW(!expressions.empty(), storm::exceptions::InvalidArgumentException, "Cannot build function application of empty expression list.");
+            
+            // Balance the syntax tree if there are enough operands
+            if (expressions.size() >= 4) {
+                // we treat operands and literals seperately so that a subsequent call to simplify() is more successful (see, e.g., (a + 1) + (b + 1))
+                std::vector<std::vector<storm::expressions::Expression>> operandTypes(2);
+                auto& nonliterals = operandTypes[0];
+                auto& literals = operandTypes[1];
+                for (auto const& expression : expressions) {
+                    if (expression.isLiteral()) {
+                        literals.push_back(expression);
+                    } else {
+                        nonliterals.push_back(expression);
+                    }
+                }
+                
+                for (auto& operands : operandTypes) {
+                    auto opIt = operands.begin();
+                    while (operands.size() > 1) {
+                        if (opIt == operands.end() || opIt == operands.end() - 1) {
+                            opIt = operands.begin();
+                        }
+                        *opIt = function(*opIt, operands.back());
+                        operands.pop_back();
+                        ++opIt;
+                    }
+                }
+                if (nonliterals.empty()) {
+                    return literals.front();
+                } else if (literals.empty()) {
+                    return nonliterals.front();
+                } else {
+                    return function(literals.front(), nonliterals.front());
+                }
+            } else {
+                return apply(expressions, function);
+            }
+        }
     }
 }

src/storm/storage/expressions/Expression.h

@@ -442,6 +442,7 @@ namespace storm {
         Expression conjunction(std::vector<storm::expressions::Expression> const& expressions);
         Expression sum(std::vector<storm::expressions::Expression> const& expressions);
         Expression apply(std::vector<storm::expressions::Expression> const& expressions, std::function<Expression (Expression const&, Expression const&)> const& function);
+        Expression applyAssociative(std::vector<storm::expressions::Expression> const& expressions, std::function<Expression (Expression const&, Expression const&)> const& function);
 
     }
 }

src/storm/utility/ExpressionHelper.cpp

@@ -1,28 +0,0 @@
-#include "storm/utility/ExpressionHelper.h"
-#include "storm/utility/constants.h"
-
-namespace storm {
-    namespace utility {
-        
-        ExpressionHelper::ExpressionHelper(std::shared_ptr<storm::expressions::ExpressionManager> const& expressionManager) : manager(expressionManager) {
-            // Intentionally left empty
-        }
-
-        storm::expressions::Expression ExpressionHelper::sum(std::vector<storm::expressions::Expression>&& summands) const {
-            if (summands.empty()) {
-                return manager->rational(storm::utility::zero<storm::RationalNumber>());
-            }
-            storm::expressions::Expression res = summands.front();
-            bool first = true;
-            for (auto& s : summands) {
-                if (first) {
-                    first = false;
-                } else {
-                    res = res + s;
-                }
-            }
-            return res.simplify().reduceNesting();
-        }
-        
-    }
-}

src/storm/utility/ExpressionHelper.h

@@ -1,28 +0,0 @@
-#pragma once
-
-#include <vector>
-#include <memory>
-#include "storm/storage/expressions/Expression.h"
-#include "storm/storage/expressions/ExpressionManager.h"
-
-namespace storm {
-    namespace utility {
-    
-        class ExpressionHelper {
-
-        public:
-            ExpressionHelper(std::shared_ptr<storm::expressions::ExpressionManager> const& expressionManager);
-            
-            /*!
-             * Creates an expression that is the sum over all the given summands.
-             */
-            storm::expressions::Expression sum(std::vector<storm::expressions::Expression>&& summands) const;
-
-        private:
-            
-            std::shared_ptr<storm::expressions::ExpressionManager> manager;
-        };
-    
-    
-    }
-}