diff --git a/src/storm/modelchecker/multiobjective/constraintbased/SparseCbAchievabilityQuery.cpp b/src/storm/modelchecker/multiobjective/constraintbased/SparseCbAchievabilityQuery.cpp index 5a65bd502..475bab05a 100644 --- a/src/storm/modelchecker/multiobjective/constraintbased/SparseCbAchievabilityQuery.cpp +++ b/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()); storm::expressions::Expression one = this->expressionManager->rational(storm::utility::one()); @@ -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())); + } + 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()); diff --git a/src/storm/modelchecker/prctl/helper/rewardbounded/CostLimitClosure.cpp b/src/storm/modelchecker/prctl/helper/rewardbounded/CostLimitClosure.cpp index 657703b93..2471093d7 100644 --- a/src/storm/modelchecker/prctl/helper/rewardbounded/CostLimitClosure.cpp +++ b/src/storm/modelchecker/prctl/helper/rewardbounded/CostLimitClosure.cpp @@ -1,4 +1,3 @@ -#include #include "storm/modelchecker/prctl/helper/rewardbounded/CostLimitClosure.h" #include "storm/utility/macros.h" #include "storm/exceptions/IllegalArgumentException.h" diff --git a/src/storm/storage/expressions/Expression.cpp b/src/storm/storage/expressions/Expression.cpp index 77d318606..0221628db 100644 --- a/src/storm/storage/expressions/Expression.cpp +++ b/src/storm/storage/expressions/Expression.cpp @@ -436,19 +436,19 @@ namespace storm { } Expression disjunction(std::vector 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 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 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 const& expressions, std::function 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 const& expressions, std::function 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> 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); + } + } } } diff --git a/src/storm/storage/expressions/Expression.h b/src/storm/storage/expressions/Expression.h index e07e1cf1a..f8741440e 100644 --- a/src/storm/storage/expressions/Expression.h +++ b/src/storm/storage/expressions/Expression.h @@ -442,6 +442,7 @@ namespace storm { Expression conjunction(std::vector const& expressions); Expression sum(std::vector const& expressions); Expression apply(std::vector const& expressions, std::function const& function); + Expression applyAssociative(std::vector const& expressions, std::function const& function); } } diff --git a/src/storm/utility/ExpressionHelper.cpp b/src/storm/utility/ExpressionHelper.cpp deleted file mode 100644 index fd99855f8..000000000 --- a/src/storm/utility/ExpressionHelper.cpp +++ /dev/null @@ -1,28 +0,0 @@ -#include "storm/utility/ExpressionHelper.h" -#include "storm/utility/constants.h" - -namespace storm { - namespace utility { - - ExpressionHelper::ExpressionHelper(std::shared_ptr const& expressionManager) : manager(expressionManager) { - // Intentionally left empty - } - - storm::expressions::Expression ExpressionHelper::sum(std::vector&& summands) const { - if (summands.empty()) { - return manager->rational(storm::utility::zero()); - } - 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(); - } - - } -} \ No newline at end of file diff --git a/src/storm/utility/ExpressionHelper.h b/src/storm/utility/ExpressionHelper.h deleted file mode 100644 index 6c171a286..000000000 --- a/src/storm/utility/ExpressionHelper.h +++ /dev/null @@ -1,28 +0,0 @@ -#pragma once - -#include -#include -#include "storm/storage/expressions/Expression.h" -#include "storm/storage/expressions/ExpressionManager.h" - -namespace storm { - namespace utility { - - class ExpressionHelper { - - public: - ExpressionHelper(std::shared_ptr const& expressionManager); - - /*! - * Creates an expression that is the sum over all the given summands. - */ - storm::expressions::Expression sum(std::vector&& summands) const; - - private: - - std::shared_ptr manager; - }; - - - } -} \ No newline at end of file