From 7063928d2fd6ad771d78c485fcbe7a5fecf64fda Mon Sep 17 00:00:00 2001 From: Stefan Pranger Date: Fri, 29 Jan 2021 19:16:54 +0100 Subject: [PATCH] refactored gmm opt dir overrides --- src/storm/solver/GmmxxMultiplier.cpp | 130 ++++++++++++++++++--------- src/storm/solver/GmmxxMultiplier.h | 32 +++---- 2 files changed, 107 insertions(+), 55 deletions(-) diff --git a/src/storm/solver/GmmxxMultiplier.cpp b/src/storm/solver/GmmxxMultiplier.cpp index 66ae1249a..e36ce7e74 100644 --- a/src/storm/solver/GmmxxMultiplier.cpp +++ b/src/storm/solver/GmmxxMultiplier.cpp @@ -11,6 +11,7 @@ #include "storm/utility/constants.h" #include "storm/exceptions/NotSupportedException.h" +#include "storm/exceptions/InternalException.h" #include "storm/utility/macros.h" @@ -87,7 +88,7 @@ namespace storm { } template - void GmmxxMultiplier::multiplyAndReduce(Environment const& env, OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& x, std::vector const* b, std::vector& result, std::vector* choices) const { + void GmmxxMultiplier::multiplyAndReduce(Environment const& env, OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& x, std::vector const* b, std::vector& result, std::vector* choices, storm::storage::BitVector* dirOverride) const { initialize(); std::vector* target = &result; if (&x == &result) { @@ -99,9 +100,9 @@ namespace storm { target = this->cachedVector.get(); } if (parallelize(env)) { - multAddReduceParallel(dir, rowGroupIndices, x, b, *target, choices); + multAddReduceParallel(dir, rowGroupIndices, x, b, *target, choices, dirOverride); } else { - multAddReduceHelper(dir, rowGroupIndices, x, b, *target, choices, false); + multAddReduceHelper(dir, rowGroupIndices, x, b, *target, choices, dirOverride, false); } if (&x == &result) { std::swap(result, *this->cachedVector); @@ -109,9 +110,9 @@ namespace storm { } template - void GmmxxMultiplier::multiplyAndReduceGaussSeidel(Environment const& env, OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector& x, std::vector const* b, std::vector* choices, bool backwards) const { + void GmmxxMultiplier::multiplyAndReduceGaussSeidel(Environment const& env, OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector& x, std::vector const* b, std::vector* choices, storm::storage::BitVector* dirOverride, bool backwards) const { initialize(); - multAddReduceHelper(dir, rowGroupIndices, x, b, x, choices, backwards); + multAddReduceHelper(dir, rowGroupIndices, x, b, x, choices, dirOverride, backwards); } template @@ -134,25 +135,42 @@ namespace storm { } template - void GmmxxMultiplier::multAddReduceHelper(OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& x, std::vector const* b, std::vector& result, std::vector* choices, bool backwards) const { + void GmmxxMultiplier::multAddReduceHelper(OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& x, std::vector const* b, std::vector& result, std::vector* choices, storm::storage::BitVector* dirOverride, bool backwards) const { + bool isOverridden = (dirOverride && !dirOverride->empty()) ? true : false; if (dir == storm::OptimizationDirection::Minimize) { - if (backwards) { - multAddReduceHelper, true>(rowGroupIndices, x, b, result, choices); + if(isOverridden) { + if (backwards) { + multAddReduceHelper, true, true>(rowGroupIndices, x, b, result, choices, dirOverride); + } else { + multAddReduceHelper, false, true>(rowGroupIndices, x, b, result, choices, dirOverride); + } } else { - multAddReduceHelper, false>(rowGroupIndices, x, b, result, choices); + if (backwards) { + multAddReduceHelper, true, false>(rowGroupIndices, x, b, result, choices); + } else { + multAddReduceHelper, false, false>(rowGroupIndices, x, b, result, choices); + } } } else { - if (backwards) { - multAddReduceHelper, true>(rowGroupIndices, x, b, result, choices); + if(isOverridden) { + if (backwards) { + multAddReduceHelper, true, true>(rowGroupIndices, x, b, result, choices, dirOverride); + } else { + multAddReduceHelper, false, true>(rowGroupIndices, x, b, result, choices, dirOverride); + } } else { - multAddReduceHelper, false>(rowGroupIndices, x, b, result, choices); + if (backwards) { + multAddReduceHelper, true, false>(rowGroupIndices, x, b, result, choices); + } else { + multAddReduceHelper, false, false>(rowGroupIndices, x, b, result, choices); + } } } } template - template - void GmmxxMultiplier::multAddReduceHelper(std::vector const& rowGroupIndices, std::vector const& x, std::vector const* b, std::vector& result, std::vector* choices) const { + template + void GmmxxMultiplier::multAddReduceHelper(std::vector const& rowGroupIndices, std::vector const& x, std::vector const* b, std::vector& result, std::vector* choices, storm::storage::BitVector* dirOverride) const { Compare compare; typedef std::vector VectorType; typedef gmm::csr_matrix MatrixType; @@ -169,11 +187,6 @@ namespace storm { choice_it = backwards ? choices->end() - 1 : choices->begin(); } - boost::optional optimizationDirectionOverride; - if(this->getOptimizationDirectionOverride().is_initialized()) { - optimizationDirectionOverride = this->getOptimizationDirectionOverride(); - } - // Variables for correctly tracking choices (only update if new choice is strictly better). ValueType oldSelectedChoiceValue; uint64_t selectedChoice; @@ -228,12 +241,22 @@ namespace storm { } //std::cout << newValue << ", "; //STORM_LOG_DEBUG(std::setprecision(3) << vect_sp(gmm::linalg_traits::row(itr), x) << " + " << *add_it << "; "); - if(this->isOverridden(currentRowGroup) ? compare(currentValue, newValue) : compare(newValue, currentValue)) { - currentValue = newValue; - if (choices) { - selectedChoice = currentRow - *row_group_it; + if(!directionOverridden) { + if(compare(newValue, currentValue)) { + currentValue = newValue; + if (choices) { + selectedChoice = currentRow - *row_group_it; + } + choiceforprintout = currentRow - *row_group_it; + } + } else { + if(dirOverride->get(currentRowGroup) ? compare(currentValue, newValue) : compare(newValue, currentValue)) { + currentValue = newValue; + if (choices) { + selectedChoice = currentRow - *row_group_it; + } + choiceforprintout = currentRow - *row_group_it; } - choiceforprintout = currentRow - *row_group_it; } // move row-based iterators to the next row if (backwards) { @@ -251,8 +274,14 @@ namespace storm { // Finally write value to target vector. *target_it = currentValue; if(choices) { - if(this->isOverridden(currentRowGroup) ? compare(oldSelectedChoiceValue, currentValue) : compare(currentValue, oldSelectedChoiceValue) ) { - *choice_it = selectedChoice; + if(!directionOverridden) { + if(compare(currentValue, oldSelectedChoiceValue) ) { + *choice_it = selectedChoice; + } + } else { + if(dirOverride->get(currentRowGroup) ? compare(oldSelectedChoiceValue, currentValue) : compare(currentValue, oldSelectedChoiceValue) ) { + *choice_it = selectedChoice; + } } } } @@ -274,8 +303,8 @@ namespace storm { } template<> - template - void GmmxxMultiplier::multAddReduceHelper(std::vector const& rowGroupIndices, std::vector const& x, std::vector const* b, std::vector& result, std::vector* choices) const { + template + void GmmxxMultiplier::multAddReduceHelper(std::vector const& rowGroupIndices, std::vector const& x, std::vector const* b, std::vector& result, std::vector* choices, storm::storage::BitVector* dirOverride) const { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Operation not supported for this data type."); } @@ -301,7 +330,7 @@ namespace storm { template class TbbMultAddReduceFunctor { public: - TbbMultAddReduceFunctor(std::vector const& rowGroupIndices, gmm::csr_matrix const& matrix, std::vector const& x, std::vector const* b, std::vector& result, std::vector* choices) : rowGroupIndices(rowGroupIndices), matrix(matrix), x(x), b(b), result(result), choices(choices) { + TbbMultAddReduceFunctor(std::vector const& rowGroupIndices, gmm::csr_matrix const& matrix, std::vector const& x, std::vector const* b, std::vector& result, std::vector* choices, storm::storage::BitVector* dirOverride = nullptr) : rowGroupIndices(rowGroupIndices), matrix(matrix), x(x), b(b), result(result), choices(choices), dirOverride(dirOverride) { // Intentionally left empty. } @@ -321,6 +350,10 @@ namespace storm { if (choices) { choiceIt = choices->begin() + range.begin(); } + bool dirOverridden = false; + if(dirOverride && !dirOverride.get()->empty()) { + dirOverridden = true; + } auto resultIt = result.begin() + range.begin(); @@ -355,19 +388,35 @@ namespace storm { ValueType newValue = b ? *bIt : storm::utility::zero(); newValue += vect_sp(gmm::linalg_traits::row(itr), x); - if (compare(newValue, currentValue)) { - currentValue = newValue; - if (choices) { - selectedChoice = currentRow - *groupIt; + if(!dirOverridden) { + if (compare(newValue, currentValue)) { + currentValue = newValue; + if (choices) { + selectedChoice = currentRow - *groupIt; + } + } + } else { + if (dirOverride.get()->get(*groupIt) ? compare(currentValue, newValue) : compare(newValue, currentValue)) { + currentValue = newValue; + if (choices) { + selectedChoice = currentRow - *groupIt; + } } + } } } // Finally write value to target vector. *resultIt = currentValue; - if (choices && compare(currentValue, oldSelectedChoiceValue)) { - *choiceIt = selectedChoice; + if(!dirOverridden) { + if (choices && compare(currentValue, oldSelectedChoiceValue)) { + *choiceIt = selectedChoice; + } + } else { + if (choices && dirOverride.get()->get(*groupIt) ? compare(oldSelectedChoiceValue, currentValue) : compare(currentValue, oldSelectedChoiceValue)) { + *choiceIt = selectedChoice; + } } } } @@ -380,25 +429,26 @@ namespace storm { std::vector const* b; std::vector& result; std::vector* choices; + boost::optional dirOverride = boost::none; }; #endif template - void GmmxxMultiplier::multAddReduceParallel(storm::solver::OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& x, std::vector const* b, std::vector& result, std::vector* choices) const { + void GmmxxMultiplier::multAddReduceParallel(storm::solver::OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& x, std::vector const* b, std::vector& result, std::vector* choices, storm::storage::BitVector* dirOverride) const { #ifdef STORM_HAVE_INTELTBB if (dir == storm::OptimizationDirection::Minimize) { - tbb::parallel_for(tbb::blocked_range(0, rowGroupIndices.size() - 1, 100), TbbMultAddReduceFunctor>(rowGroupIndices, this->gmmMatrix, x, b, result, choices)); + tbb::parallel_for(tbb::blocked_range(0, rowGroupIndices.size() - 1, 100), TbbMultAddReduceFunctor>(rowGroupIndices, this->gmmMatrix, x, b, result, choices, dirOverride)); } else { - tbb::parallel_for(tbb::blocked_range(0, rowGroupIndices.size() - 1, 100), TbbMultAddReduceFunctor>(rowGroupIndices, this->gmmMatrix, x, b, result, choices)); + tbb::parallel_for(tbb::blocked_range(0, rowGroupIndices.size() - 1, 100), TbbMultAddReduceFunctor>(rowGroupIndices, this->gmmMatrix, x, b, result, choices, dirOverride)); } #else STORM_LOG_WARN("Storm was built without support for Intel TBB, defaulting to sequential version."); - multAddReduceHelper(dir, rowGroupIndices, x, b, result, choices); + multAddReduceHelper(dir, rowGroupIndices, x, b, result, choices, dirOverride); #endif } template<> - void GmmxxMultiplier::multAddReduceParallel(storm::solver::OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& x, std::vector const* b, std::vector& result, std::vector* choices) const { + void GmmxxMultiplier::multAddReduceParallel(storm::solver::OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& x, std::vector const* b, std::vector& result, std::vector* choices, storm::storage::BitVector* dirOverride) const { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "This operation is not supported."); } diff --git a/src/storm/solver/GmmxxMultiplier.h b/src/storm/solver/GmmxxMultiplier.h index f0394770b..77050f8aa 100644 --- a/src/storm/solver/GmmxxMultiplier.h +++ b/src/storm/solver/GmmxxMultiplier.h @@ -2,47 +2,49 @@ #include "storm/solver/Multiplier.h" +#include "storm/storage/BitVector.h" + #include "storm/adapters/GmmxxAdapter.h" #include "storm-config.h" namespace storm { - + namespace storage { template class SparseMatrix; } - + namespace solver { - + template class GmmxxMultiplier : public Multiplier { public: GmmxxMultiplier(storm::storage::SparseMatrix const& matrix); virtual ~GmmxxMultiplier() = default; - + virtual void multiply(Environment const& env, std::vector const& x, std::vector const* b, std::vector& result) const override; virtual void multiplyGaussSeidel(Environment const& env, std::vector& x, std::vector const* b, bool backwards = true) const override; - virtual void multiplyAndReduce(Environment const& env, OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& x, std::vector const* b, std::vector& result, std::vector* choices = nullptr) const override; - virtual void multiplyAndReduceGaussSeidel(Environment const& env, OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector& x, std::vector const* b, std::vector* choices = nullptr, bool backwards = true) const override; + virtual void multiplyAndReduce(Environment const& env, OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& x, std::vector const* b, std::vector& result, std::vector* choices = nullptr, storm::storage::BitVector* dirOverride = nullptr) const override; + virtual void multiplyAndReduceGaussSeidel(Environment const& env, OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector& x, std::vector const* b, std::vector* choices = nullptr, storm::storage::BitVector* dirOverride = nullptr, bool backwards = true) const override; virtual void multiplyRow(uint64_t const& rowIndex, std::vector const& x, ValueType& value) const override; virtual void clearCache() const override; - + private: void initialize() const; - + bool parallelize(Environment const& env) const; - + void multAdd(std::vector const& x, std::vector const* b, std::vector& result) const; void multAddParallel(std::vector const& x, std::vector const* b, std::vector& result) const; - void multAddReduceParallel(storm::solver::OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& x, std::vector const* b, std::vector& result, std::vector* choices = nullptr) const; - void multAddReduceHelper(storm::solver::OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& x, std::vector const* b, std::vector& result, std::vector* choices = nullptr, bool backwards = true) const; - - template - void multAddReduceHelper(std::vector const& rowGroupIndices, std::vector const& x, std::vector const* b, std::vector& result, std::vector* choices = nullptr) const; + void multAddReduceParallel(storm::solver::OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& x, std::vector const* b, std::vector& result, std::vector* choices = nullptr, storm::storage::BitVector* dirOverride = nullptr) const; + void multAddReduceHelper(storm::solver::OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& x, std::vector const* b, std::vector& result, std::vector* choices = nullptr, storm::storage::BitVector* dirOverride = nullptr, bool backwards = true) const; + + template + void multAddReduceHelper(std::vector const& rowGroupIndices, std::vector const& x, std::vector const* b, std::vector& result, std::vector* choices = nullptr, storm::storage::BitVector* dirOverride = nullptr) const; mutable gmm::csr_matrix gmmMatrix; }; - + } }