diff --git a/src/storm/solver/GmmxxMultiplier.cpp b/src/storm/solver/GmmxxMultiplier.cpp index e36ce7e74..e28e1ceae 100644 --- a/src/storm/solver/GmmxxMultiplier.cpp +++ b/src/storm/solver/GmmxxMultiplier.cpp @@ -88,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, storm::storage::BitVector* dirOverride) 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 const* dirOverride) const { initialize(); std::vector* target = &result; if (&x == &result) { @@ -110,7 +110,7 @@ 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, storm::storage::BitVector* dirOverride, 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 const* dirOverride, bool backwards) const { initialize(); multAddReduceHelper(dir, rowGroupIndices, x, b, x, choices, dirOverride, backwards); } @@ -135,7 +135,7 @@ 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, storm::storage::BitVector* dirOverride, 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 const* dirOverride, bool backwards) const { bool isOverridden = (dirOverride && !dirOverride->empty()) ? true : false; if (dir == storm::OptimizationDirection::Minimize) { if(isOverridden) { @@ -170,7 +170,7 @@ 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, storm::storage::BitVector* dirOverride) const { + void GmmxxMultiplier::multAddReduceHelper(std::vector const& rowGroupIndices, std::vector const& x, std::vector const* b, std::vector& result, std::vector* choices, storm::storage::BitVector const* dirOverride) const { Compare compare; typedef std::vector VectorType; typedef gmm::csr_matrix MatrixType; @@ -304,7 +304,7 @@ 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, storm::storage::BitVector* dirOverride) const { + void GmmxxMultiplier::multAddReduceHelper(std::vector const& rowGroupIndices, std::vector const& x, std::vector const* b, std::vector& result, std::vector* choices, storm::storage::BitVector const* dirOverride) const { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Operation not supported for this data type."); } @@ -330,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, storm::storage::BitVector* dirOverride = nullptr) : rowGroupIndices(rowGroupIndices), matrix(matrix), x(x), b(b), result(result), choices(choices), dirOverride(dirOverride) { + 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 const* dirOverride = nullptr) : rowGroupIndices(rowGroupIndices), matrix(matrix), x(x), b(b), result(result), choices(choices), dirOverride(dirOverride) { // Intentionally left empty. } @@ -429,12 +429,12 @@ namespace storm { std::vector const* b; std::vector& result; std::vector* choices; - boost::optional dirOverride = boost::none; + boost::optional const 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, storm::storage::BitVector* dirOverride) 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 const* 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, dirOverride)); @@ -448,7 +448,7 @@ namespace storm { } 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, storm::storage::BitVector* dirOverride) 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 const* 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 77050f8aa..b3f65d282 100644 --- a/src/storm/solver/GmmxxMultiplier.h +++ b/src/storm/solver/GmmxxMultiplier.h @@ -25,8 +25,8 @@ namespace storm { 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, 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 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 const* 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 const* 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; @@ -37,11 +37,11 @@ namespace storm { 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, 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; + 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 const* 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 const* 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; + void multAddReduceHelper(std::vector const& rowGroupIndices, std::vector const& x, std::vector const* b, std::vector& result, std::vector* choices = nullptr, storm::storage::BitVector const* dirOverride = nullptr) const; mutable gmm::csr_matrix gmmMatrix; }; diff --git a/src/storm/solver/Multiplier.cpp b/src/storm/solver/Multiplier.cpp index a0533b06d..97eb22bb8 100644 --- a/src/storm/solver/Multiplier.cpp +++ b/src/storm/solver/Multiplier.cpp @@ -30,12 +30,12 @@ namespace storm { } template - void Multiplier::multiplyAndReduce(Environment const& env, OptimizationDirection const& dir, std::vector const& x, std::vector const* b, std::vector& result, std::vector* choices, storm::storage::BitVector* dirOverride) const { + void Multiplier::multiplyAndReduce(Environment const& env, OptimizationDirection const& dir, std::vector const& x, std::vector const* b, std::vector& result, std::vector* choices, storm::storage::BitVector const* dirOverride) const { multiplyAndReduce(env, dir, this->matrix.getRowGroupIndices(), x, b, result, choices, dirOverride); } template - void Multiplier::multiplyAndReduceGaussSeidel(Environment const& env, OptimizationDirection const& dir, std::vector& x, std::vector const* b, std::vector* choices, storm::storage::BitVector* dirOverride, bool backwards) const { + void Multiplier::multiplyAndReduceGaussSeidel(Environment const& env, OptimizationDirection const& dir, std::vector& x, std::vector const* b, std::vector* choices, storm::storage::BitVector const* dirOverride, bool backwards) const { multiplyAndReduceGaussSeidel(env, dir, this->matrix.getRowGroupIndices(), x, b, choices, dirOverride, backwards); } @@ -55,7 +55,7 @@ namespace storm { } template - void Multiplier::repeatedMultiplyAndReduce(Environment const& env, OptimizationDirection const& dir, std::vector& x, std::vector const* b, uint64_t n, storm::storage::BitVector* dirOverride) const { + void Multiplier::repeatedMultiplyAndReduce(Environment const& env, OptimizationDirection const& dir, std::vector& x, std::vector const* b, uint64_t n, storm::storage::BitVector const* dirOverride) const { storm::utility::ProgressMeasurement progress("multiplications"); progress.setMaxCount(n); progress.startNewMeasurement(0); diff --git a/src/storm/solver/Multiplier.h b/src/storm/solver/Multiplier.h index 7662d355c..4127a6625 100644 --- a/src/storm/solver/Multiplier.h +++ b/src/storm/solver/Multiplier.h @@ -70,8 +70,8 @@ namespace storm { * to the number of rows of A. Can be the same as the x vector. * @param choices If given, the choices made in the reduction process are written to this vector. */ - void multiplyAndReduce(Environment const& env, OptimizationDirection const& dir, std::vector const& x, std::vector const* b, std::vector& result, std::vector* choices = nullptr, storm::storage::BitVector* dirOverride = nullptr) const; - 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 = 0; + void multiplyAndReduce(Environment const& env, OptimizationDirection const& dir, std::vector const& x, std::vector const* b, std::vector& result, std::vector* choices = nullptr, storm::storage::BitVector const* dirOverride = nullptr) const; + 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 const* dirOverride = nullptr) const = 0; /*! * Performs a matrix-vector multiplication in gauss-seidel style and then minimizes/maximizes over the row groups @@ -88,8 +88,8 @@ namespace storm { * @param choices If given, the choices made in the reduction process are written to this vector. * @param backwards if true, the iterations will be performed beginning from the last rowgroup and ending at the first rowgroup. */ - void multiplyAndReduceGaussSeidel(Environment const& env, OptimizationDirection const& dir, std::vector& x, std::vector const* b, std::vector* choices = nullptr, storm::storage::BitVector* dirOverride = nullptr, bool backwards = true) const; - 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 = 0; + void multiplyAndReduceGaussSeidel(Environment const& env, OptimizationDirection const& dir, std::vector& x, std::vector const* b, std::vector* choices = nullptr, storm::storage::BitVector const* dirOverride = nullptr, bool backwards = true) const; + 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 const* dirOverride = nullptr, bool backwards = true) const = 0; /*! * Performs repeated matrix-vector multiplication, using x[0] = x and x[i + 1] = A*x[i] + b. After @@ -117,7 +117,7 @@ namespace storm { * to the number of rows of A. * @param n The number of times to perform the multiplication. */ - void repeatedMultiplyAndReduce(Environment const& env, OptimizationDirection const& dir, std::vector& x, std::vector const* b, uint64_t n, storm::storage::BitVector* dirOverride = nullptr) const; + void repeatedMultiplyAndReduce(Environment const& env, OptimizationDirection const& dir, std::vector& x, std::vector const* b, uint64_t n, storm::storage::BitVector const* dirOverride = nullptr) const; /*! * Multiplies the row with the given index with x and adds the result to the provided value diff --git a/src/storm/solver/NativeMultiplier.cpp b/src/storm/solver/NativeMultiplier.cpp index 26dad0b22..17df1faa3 100644 --- a/src/storm/solver/NativeMultiplier.cpp +++ b/src/storm/solver/NativeMultiplier.cpp @@ -16,12 +16,12 @@ namespace storm { namespace solver { - + template NativeMultiplier::NativeMultiplier(storm::storage::SparseMatrix const& matrix) : Multiplier(matrix) { // Intentionally left empty. } - + template bool NativeMultiplier::parallelize(Environment const& env) const { #ifdef STORM_HAVE_INTELTBB @@ -30,7 +30,7 @@ namespace storm { return false; #endif } - + template void NativeMultiplier::multiply(Environment const& env, std::vector const& x, std::vector const* b, std::vector& result) const { std::vector* target = &result; @@ -51,7 +51,7 @@ namespace storm { std::swap(result, *this->cachedVector); } } - + template void NativeMultiplier::multiplyGaussSeidel(Environment const& env, std::vector& x, std::vector const* b, bool backwards) const { if (backwards) { @@ -62,7 +62,7 @@ namespace storm { } template - void NativeMultiplier::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 { + void NativeMultiplier::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 const* dirOverride) const { std::vector* target = &result; if (&x == &result) { if (this->cachedVector) { @@ -83,7 +83,7 @@ namespace storm { } template - void NativeMultiplier::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 { + void NativeMultiplier::multiplyAndReduceGaussSeidel(Environment const& env, OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector& x, std::vector const* b, std::vector* choices, storm::storage::BitVector const* dirOverride, bool backwards) const { if (backwards) { this->matrix.multiplyAndReduceBackward(dir, rowGroupIndices, x, b, x, choices, dirOverride); } else { @@ -112,7 +112,7 @@ namespace storm { } template - void NativeMultiplier::multAddReduce(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 { + void NativeMultiplier::multAddReduce(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 const* dirOverride) const { this->matrix.multiplyAndReduce(dir, rowGroupIndices, x, b, result, choices, dirOverride); } @@ -127,7 +127,7 @@ namespace storm { } template - void NativeMultiplier::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 { + void NativeMultiplier::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 const* dirOverride) const { #ifdef STORM_HAVE_INTELTBB this->matrix.multiplyAndReduceParallel(dir, rowGroupIndices, x, b, result, choices, dirOverride); #else @@ -141,6 +141,6 @@ namespace storm { template class NativeMultiplier; template class NativeMultiplier; #endif - + } } diff --git a/src/storm/solver/NativeMultiplier.h b/src/storm/solver/NativeMultiplier.h index 62ae47d07..532ec2cc9 100644 --- a/src/storm/solver/NativeMultiplier.h +++ b/src/storm/solver/NativeMultiplier.h @@ -20,8 +20,8 @@ namespace storm { 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, 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 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 const* 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 const* dirOverride = nullptr, bool backwards = true) const override; virtual void multiplyRow(uint64_t const& rowIndex, std::vector const& x, ValueType& value) const override; virtual void multiplyRow2(uint64_t const& rowIndex, std::vector const& x1, ValueType& val1, std::vector const& x2, ValueType& val2) const override; @@ -30,10 +30,10 @@ namespace storm { void multAdd(std::vector const& x, std::vector const* b, std::vector& result) const; - void multAddReduce(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 multAddReduce(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 const* dirOverride = nullptr) 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, storm::storage::BitVector* dirOverride = 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 const* dirOverride = nullptr) const; }; diff --git a/src/storm/storage/SparseMatrix.cpp b/src/storm/storage/SparseMatrix.cpp index 84b8fa306..7f2e7e1d6 100644 --- a/src/storm/storage/SparseMatrix.cpp +++ b/src/storm/storage/SparseMatrix.cpp @@ -1753,7 +1753,7 @@ namespace storm { #endif template - void SparseMatrix::multiplyAndReduceForward(OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& vector, std::vector const* summand, std::vector& result, std::vector* choices, storm::storage::BitVector* dirOverride) const { + void SparseMatrix::multiplyAndReduceForward(OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& vector, std::vector const* summand, std::vector& result, std::vector* choices, storm::storage::BitVector const* dirOverride) const { if(dirOverride && !dirOverride->empty()) { if (dir == OptimizationDirection::Minimize) { multiplyAndReduceForward, true>(rowGroupIndices, vector, summand, result, choices, dirOverride); @@ -1771,7 +1771,7 @@ namespace storm { template template - void SparseMatrix::multiplyAndReduceForward(std::vector const& rowGroupIndices, std::vector const& vector, std::vector const* summand, std::vector& result, std::vector* choices, storm::storage::BitVector* dirOverride) const { + void SparseMatrix::multiplyAndReduceForward(std::vector const& rowGroupIndices, std::vector const& vector, std::vector const* summand, std::vector& result, std::vector* choices, storm::storage::BitVector const* dirOverride) const { Compare compare; auto elementIt = this->begin(); auto rowGroupIt = rowGroupIndices.begin(); @@ -1862,13 +1862,13 @@ namespace storm { #ifdef STORM_HAVE_CARL template<> - void SparseMatrix::multiplyAndReduceForward(OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& vector, std::vector const* b, std::vector& result, std::vector* choices, storm::storage::BitVector* dirOverride) const { + void SparseMatrix::multiplyAndReduceForward(OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& vector, std::vector const* b, std::vector& result, std::vector* choices, storm::storage::BitVector const* dirOverride) const { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "This operation is not supported."); } #endif template - void SparseMatrix::multiplyAndReduceBackward(OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& vector, std::vector const* summand, std::vector& result, std::vector* choices, storm::storage::BitVector* dirOverride) const { + void SparseMatrix::multiplyAndReduceBackward(OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& vector, std::vector const* summand, std::vector& result, std::vector* choices, storm::storage::BitVector const* dirOverride) const { if(dirOverride && !dirOverride->empty()) { if (dir == storm::OptimizationDirection::Minimize) { multiplyAndReduceBackward, true>(rowGroupIndices, vector, summand, result, choices, dirOverride); @@ -1886,7 +1886,7 @@ namespace storm { template template - void SparseMatrix::multiplyAndReduceBackward(std::vector const& rowGroupIndices, std::vector const& vector, std::vector const* summand, std::vector& result, std::vector* choices, storm::storage::BitVector* dirOverride) const { + void SparseMatrix::multiplyAndReduceBackward(std::vector const& rowGroupIndices, std::vector const& vector, std::vector const* summand, std::vector& result, std::vector* choices, storm::storage::BitVector const* dirOverride) const { Compare compare; auto elementIt = this->end() - 1; auto rowGroupIt = rowGroupIndices.end() - 2; @@ -1972,7 +1972,7 @@ namespace storm { #ifdef STORM_HAVE_CARL template<> - void SparseMatrix::multiplyAndReduceBackward(OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& vector, std::vector const* b, std::vector& result, std::vector* choices, storm::storage::BitVector* dirOverride) const { + void SparseMatrix::multiplyAndReduceBackward(OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& vector, std::vector const* b, std::vector& result, std::vector* choices, storm::storage::BitVector const* dirOverride) const { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "This operation is not supported."); } #endif @@ -1985,7 +1985,7 @@ namespace storm { typedef typename storm::storage::SparseMatrix::value_type value_type; typedef typename storm::storage::SparseMatrix::const_iterator const_iterator; - TbbMultAddReduceFunctor(std::vector const& rowGroupIndices, std::vector> const& columnsAndEntries, std::vector const& rowIndications, std::vector const& x, std::vector& result, std::vector const* summand, std::vector* choices, storm::storage::BitVector* dirOverride = nullptr) : rowGroupIndices(rowGroupIndices), columnsAndEntries(columnsAndEntries), rowIndications(rowIndications), x(x), result(result), summand(summand), choices(choices), dirOverride(dirOverride) { + TbbMultAddReduceFunctor(std::vector const& rowGroupIndices, std::vector> const& columnsAndEntries, std::vector const& rowIndications, std::vector const& x, std::vector& result, std::vector const* summand, std::vector* choices, storm::storage::BitVector const* dirOverride = nullptr) : rowGroupIndices(rowGroupIndices), columnsAndEntries(columnsAndEntries), rowIndications(rowIndications), x(x), result(result), summand(summand), choices(choices), dirOverride(dirOverride) { // Intentionally left empty. } @@ -2092,7 +2092,7 @@ namespace storm { }; template - void SparseMatrix::multiplyAndReduceParallel(OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& vector, std::vector const* summand, std::vector& result, std::vector* choices, storm::storage::BitVector* dirOverride) const { + void SparseMatrix::multiplyAndReduceParallel(OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& vector, std::vector const* summand, std::vector& result, std::vector* choices, storm::storage::BitVector const* dirOverride) const { if(dirOverride && !dirOverride->empty()) { if (dir == storm::OptimizationDirection::Minimize) { tbb::parallel_for(tbb::blocked_range(0, rowGroupIndices.size() - 1, 100), TbbMultAddReduceFunctor, true>(rowGroupIndices, columnsAndValues, rowIndications, vector, result, summand, choices, dirOverride)); @@ -2110,14 +2110,14 @@ namespace storm { #ifdef STORM_HAVE_CARL template<> - void SparseMatrix::multiplyAndReduceParallel(OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& vector, std::vector const* summand, std::vector& result, std::vector* choices, storm::storage::BitVector* dirOverride) const { + void SparseMatrix::multiplyAndReduceParallel(OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& vector, std::vector const* summand, std::vector& result, std::vector* choices, storm::storage::BitVector const* dirOverride) const { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "This operation is not supported."); } #endif #endif template - void SparseMatrix::multiplyAndReduce(OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& vector, std::vector const* summand, std::vector& result, std::vector* choices, storm::storage::BitVector* dirOverride) const { + void SparseMatrix::multiplyAndReduce(OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& vector, std::vector const* summand, std::vector& result, std::vector* choices, storm::storage::BitVector const* dirOverride) const { // If the vector and the result are aliases, we need and temporary vector. std::vector* target; diff --git a/src/storm/storage/SparseMatrix.h b/src/storm/storage/SparseMatrix.h index 8346e5554..0043f5c01 100644 --- a/src/storm/storage/SparseMatrix.h +++ b/src/storm/storage/SparseMatrix.h @@ -35,19 +35,19 @@ namespace storm { namespace storm { namespace storage { - + // Forward declare matrix class. template class SparseMatrix; - + typedef uint_fast64_t SparseMatrixIndexType; - + template class MatrixEntry { public: typedef IndexType index_type; typedef ValueType value_type; - + /*! * Constructs a matrix entry with the given column and value. * @@ -55,14 +55,14 @@ namespace storm { * @param value The value of the matrix entry. */ MatrixEntry(index_type column, value_type value); - + /*! * Move-constructs the matrix entry fro the given column-value pair. * * @param pair The column-value pair from which to move-construct the matrix entry. */ MatrixEntry(std::pair&& pair); - + MatrixEntry() = default; MatrixEntry(MatrixEntry const& other) = default; MatrixEntry& operator=(MatrixEntry const& other) = default; @@ -70,59 +70,59 @@ namespace storm { MatrixEntry(MatrixEntry&& other) = default; MatrixEntry& operator=(MatrixEntry&& other) = default; #endif - + /*! * Retrieves the column of the matrix entry. * * @return The column of the matrix entry. */ index_type const& getColumn() const; - + /*! * Sets the column of the current entry. * * @param column The column to set for this entry. */ void setColumn(index_type const& column); - + /*! * Retrieves the value of the matrix entry. * * @return The value of the matrix entry. */ value_type const& getValue() const; - + /*! * Sets the value of the entry in the matrix. * * @param value The value that is to be set for this entry. */ void setValue(value_type const& value); - + /*! * Retrieves a pair of column and value that characterizes this entry. * * @return A column-value pair that characterizes this entry. */ std::pair const& getColumnValuePair() const; - + /*! * Multiplies the entry with the given factor and returns the result. * * @param factor The factor with which to multiply the entry. */ MatrixEntry operator*(value_type factor) const; - + bool operator==(MatrixEntry const& other) const; bool operator!=(MatrixEntry const& other) const; - + template friend std::ostream& operator<<(std::ostream& out, MatrixEntry const& entry); private: // The actual matrix entry. std::pair entry; }; - + /*! * Computes the hash value of a matrix entry. */ @@ -133,7 +133,7 @@ namespace storm { boost::hash_combine(seed, matrixEntry.getValue()); return seed; } - + /*! * A class that can be used to build a sparse matrix by adding value by value. */ @@ -142,7 +142,7 @@ namespace storm { public: typedef SparseMatrixIndexType index_type; typedef ValueType value_type; - + /*! * Constructs a sparse matrix builder producing a matrix with the given number of rows, columns and entries. * The number of rows, columns and entries is reserved upon creation. If more rows/columns or entries are @@ -159,7 +159,7 @@ namespace storm { * has a custom row grouping. */ SparseMatrixBuilder(index_type rows = 0, index_type columns = 0, index_type entries = 0, bool forceDimensions = true, bool hasCustomRowGrouping = false, index_type rowGroups = 0); - + /*! * Moves the contents of the given matrix into the matrix builder so that its contents can be modified again. * This is, for example, useful if rows need to be added to the matrix. @@ -167,7 +167,7 @@ namespace storm { * @param matrix The matrix that is to be made editable again. */ SparseMatrixBuilder(SparseMatrix&& matrix); - + /*! * Sets the matrix entry at the given row and column to the given value. After all entries have been added, * a call to finalize(false) is mandatory. @@ -182,7 +182,7 @@ namespace storm { * @param value The value that is to be set at the specified row and column. */ void addNextValue(index_type row, index_type column, value_type const& value); - + /*! * Starts a new row group in the matrix. Note that this needs to be called before any entries in the new row * group are added. @@ -190,7 +190,7 @@ namespace storm { * @param startingRow The starting row of the new row group. */ void newRowGroup(index_type startingRow); - + /* * Finalizes the sparse matrix to indicate that initialization process has been completed and the matrix * may now be used. This must be called after all entries have been added to the matrix via addNextValue. @@ -211,10 +211,10 @@ namespace storm { * groups added this way will be empty. */ SparseMatrix build(index_type overriddenRowCount = 0, index_type overriddenColumnCount = 0, index_type overriddenRowGroupCount = 0); - + /*! * Retrieves the most recently used row. - * + * * @return The most recently used row. */ index_type getLastRow() const; @@ -232,7 +232,7 @@ namespace storm { * @return The most recently used row. */ index_type getLastColumn() const; - + /*! * Replaces all columns with id > offset according to replacements. * Every state with id offset+i is replaced by the id in replacements[i]. @@ -242,7 +242,7 @@ namespace storm { * @param offset Offset to add to each id in vector index. */ void replaceColumns(std::vector const& replacements, index_type offset); - + /*! * Makes sure that a diagonal entry will be inserted at the given row. * All other entries of this row must be set immediately after calling this (without setting values at other rows in between) @@ -251,72 +251,72 @@ namespace storm { * If addNextValue is called on the given row and the diagonal column, we take the sum of the two values provided to addDiagonalEntry and addNextValue */ void addDiagonalEntry(index_type row, ValueType const& value); - + private: // A flag indicating whether a row count was set upon construction. bool initialRowCountSet; - + // The row count that was initially set (if any). index_type initialRowCount; - + // A flag indicating whether a column count was set upon construction. bool initialColumnCountSet; // The column count that was initially set (if any). index_type initialColumnCount; - + // A flag indicating whether an entry count was set upon construction. bool initialEntryCountSet; - + // The number of entries in the matrix. index_type initialEntryCount; - + // A flag indicating whether the initially given dimensions are to be enforced on the resulting matrix. bool forceInitialDimensions; - + // A flag indicating whether the builder is to construct a custom row grouping for the matrix. bool hasCustomRowGrouping; - + // A flag indicating whether the number of row groups was set upon construction. bool initialRowGroupCountSet; - + // The number of row groups in the matrix. index_type initialRowGroupCount; - + // The vector that stores the row-group indices (if they are non-trivial). boost::optional> rowGroupIndices; - + // The storage for the columns and values of all entries in the matrix. std::vector> columnsAndValues; - + // A vector containing the indices at which each given row begins. This index is to be interpreted as an // index in the valueStorage and the columnIndications vectors. Put differently, the values of the entries // in row i are valueStorage[rowIndications[i]] to valueStorage[rowIndications[i + 1]] where the last // entry is not included anymore. std::vector rowIndications; - + // Stores the current number of entries in the matrix. This is used for inserting an entry into a matrix // with preallocated storage. index_type currentEntryCount; - + // Stores the row of the last entry in the matrix. This is used for correctly inserting an entry into a // matrix. index_type lastRow; - + // Stores the column of the currently last entry in the matrix. This is used for correctly inserting an // entry into a matrix. index_type lastColumn; - + // Stores the highest column at which an entry was inserted into the matrix. index_type highestColumn; - + // Stores the currently active row group. This is used for correctly constructing the row grouping of the // matrix. index_type currentRowGroupCount; - + boost::optional pendingDiagonalEntry; }; - + /*! * A class that holds a possibly non-square matrix in the compressed row storage format. That is, it is supposed * to store non-zero entries only, but zeros may be explicitly stored if necessary for certain operations. @@ -340,12 +340,12 @@ namespace storm { friend class storm::adapters::StormAdapter; friend class storm::solver::TopologicalCudaValueIterationMinMaxLinearEquationSolver; friend class SparseMatrixBuilder; - + typedef SparseMatrixIndexType index_type; typedef ValueType value_type; typedef typename std::vector>::iterator iterator; typedef typename std::vector>::const_iterator const_iterator; - + /*! * This class represents a number of consecutive rows of the matrix. */ @@ -359,32 +359,32 @@ namespace storm { * @param entryCount The number of entrys in the rows. */ rows(iterator begin, index_type entryCount); - + /*! * Retrieves an iterator that points to the beginning of the rows. * * @return An iterator that points to the beginning of the rows. */ iterator begin(); - + /*! * Retrieves an iterator that points past the last entry of the rows. * * @return An iterator that points past the last entry of the rows. */ iterator end(); - + /*! * Retrieves the number of entries in the rows. * * @return The number of entries in the rows. */ index_type getNumberOfEntries() const; - + private: // The pointer to the columnd and value of the first entry. iterator beginIterator; - + // The number of non-zero entries in the rows. index_type entryCount; }; @@ -402,55 +402,55 @@ namespace storm { * @param entryCount The number of entrys in the rows. */ const_rows(const_iterator begin, index_type entryCount); - + /*! * Retrieves an iterator that points to the beginning of the rows. * * @return An iterator that points to the beginning of the rows. */ const_iterator begin() const; - + /*! * Retrieves an iterator that points past the last entry of the rows. * * @return An iterator that points past the last entry of the rows. */ const_iterator end() const; - + /*! * Retrieves the number of entries in the rows. * * @return The number of entries in the rows. */ index_type getNumberOfEntries() const; - + private: // The pointer to the column and value of the first entry. const_iterator beginIterator; - + // The number of non-zero entries in the rows. index_type entryCount; }; - + /*! * An enum representing the internal state of the matrix. After creation, the matrix is UNINITIALIZED. * Only after a call to finalize(), the status of the matrix is set to INITIALIZED and the matrix can be * used. */ enum MatrixStatus { UNINITIALIZED, INITIALIZED }; - + /*! * Constructs an empty sparse matrix. */ SparseMatrix(); - + /*! * Constructs a sparse matrix by performing a deep-copy of the given matrix. * * @param other The matrix from which to copy the content. */ SparseMatrix(SparseMatrix const& other); - + /*! * Constructs a sparse matrix by performing a deep-copy of the given matrix. * @@ -459,14 +459,14 @@ namespace storm { * exist in the original matrix, they are inserted and set to value zero. */ SparseMatrix(SparseMatrix const& other, bool insertDiagonalElements); - + /*! * Constructs a sparse matrix by moving the contents of the given matrix to the newly created one. * * @param other The matrix from which to move the content. */ SparseMatrix(SparseMatrix&& other); - + /*! * Constructs a sparse matrix by copying the given contents. * @@ -476,7 +476,7 @@ namespace storm { * @param rowGroupIndices The vector representing the row groups in the matrix. */ SparseMatrix(index_type columnCount, std::vector const& rowIndications, std::vector> const& columnsAndValues, boost::optional> const& rowGroupIndices); - + /*! * Constructs a sparse matrix by moving the given contents. * @@ -493,14 +493,14 @@ namespace storm { * @param other The matrix from which to copy-assign. */ SparseMatrix& operator=(SparseMatrix const& other); - + /*! * Assigns the contents of the given matrix to the current one by moving its contents. * * @param other The matrix from which to move to contents. */ SparseMatrix& operator=(SparseMatrix&& other); - + /*! * Determines whether the current and the given matrix are semantically equal. * @@ -508,28 +508,28 @@ namespace storm { * @return True iff the given matrix is semantically equal to the current one. */ bool operator==(SparseMatrix const& other) const; - + /*! * Returns the number of rows of the matrix. * * @return The number of rows of the matrix. */ index_type getRowCount() const; - + /*! * Returns the number of columns of the matrix. * * @return The number of columns of the matrix. */ index_type getColumnCount() const; - + /*! * Returns the number of entries in the matrix. * * @return The number of entries in the matrix. */ index_type getEntryCount() const; - + /*! * Returns the number of entries in the given row group of the matrix. * @@ -550,7 +550,7 @@ namespace storm { * Recompute the nonzero entry count */ void updateNonzeroEntryCount() const; - + /*! * Recomputes the number of columns and the number of non-zero entries. */ @@ -562,14 +562,14 @@ namespace storm { * @param difference Difference between old and new nonzero entry count. */ void updateNonzeroEntryCount(std::make_signed::type difference); - + /*! * Returns the number of row groups in the matrix. * * @return The number of row groups in the matrix. */ index_type getRowGroupCount() const; - + /*! * Returns the size of the given row group. * @@ -577,31 +577,31 @@ namespace storm { * @return The number of rows that belong to the given row group. */ index_type getRowGroupSize(index_type group) const; - + /*! * Returns the size of the largest row group of the matrix */ index_type getSizeOfLargestRowGroup() const; - + /*! * Returns the total number of rows that are in one of the specified row groups. */ index_type getNumRowsInRowGroups(storm::storage::BitVector const& groupConstraint) const; - + /*! * Returns the grouping of rows of this matrix. * * @return The grouping of rows of this matrix. */ std::vector const& getRowGroupIndices() const; - + /*! * Swaps the grouping of rows of this matrix. * * @return The old grouping of rows of this matrix. */ std::vector swapRowGroupIndices(std::vector&& newRowGrouping); - + /*! * Sets the row grouping to the given one. * @note It is assumed that the new row grouping is non-trivial. @@ -609,14 +609,14 @@ namespace storm { * @param newRowGroupIndices The new row group indices. */ void setRowGroupIndices(std::vector const& newRowGroupIndices); - + /*! * Retrieves whether the matrix has a trivial row grouping. * * @return True iff the matrix has a trivial row grouping. */ bool hasTrivialRowGrouping() const; - + /*! * Makes the row grouping of this matrix trivial. * Has no effect when the row grouping is already trivial. @@ -630,7 +630,7 @@ namespace storm { * @return a bit vector that is true at position i iff the row group of row i is selected. */ storm::storage::BitVector getRowFilter(storm::storage::BitVector const& groupConstraint) const; - + /*! * Returns the indices of all rows that * * are in a selected group and @@ -641,7 +641,7 @@ namespace storm { * @return a bit vector that is true at position i iff row i satisfies the constraints. */ storm::storage::BitVector getRowFilter(storm::storage::BitVector const& groupConstraint, storm::storage::BitVector const& columnConstraints) const; - + /*! * Returns the indices of all row groups selected by the row constraints * @@ -650,21 +650,21 @@ namespace storm { * @return a bit vector that is true at position i iff row i satisfies the constraints. */ storm::storage::BitVector getRowGroupFilter(storm::storage::BitVector const& rowConstraint, bool setIfForAllRowsInGroup) const; - + /*! * This function makes the given rows absorbing. * * @param rows A bit vector indicating which rows are to be made absorbing. */ void makeRowsAbsorbing(storm::storage::BitVector const& rows); - + /*! * This function makes the groups of rows given by the bit vector absorbing. * * @param rowGroupConstraint A bit vector indicating which row groups to make absorbing. */ void makeRowGroupsAbsorbing(storm::storage::BitVector const& rowGroupConstraint); - + /*! * This function makes the given row Dirac. This means that all entries will be set to 0 except the one * at the specified column, which is set to 1 instead. @@ -673,14 +673,14 @@ namespace storm { * @param column The index of the column whose value is to be set to 1. */ void makeRowDirac(index_type row, index_type column); - + /* * Sums the entries in all rows. * * @return The vector of sums of the entries in the respective rows. */ std::vector getRowSumVector() const; - + /* * Sums the entries in the given row and columns. * @@ -689,7 +689,7 @@ namespace storm { * @return The sum of the entries in the given row and columns. */ value_type getConstrainedRowSum(index_type row, storm::storage::BitVector const& columns) const; - + /*! * Computes a vector whose i-th entry is the sum of the entries in the i-th selected row where only those * entries are added that are in selected columns. @@ -700,7 +700,7 @@ namespace storm { * @return A vector whose elements are the sums of the selected columns in each row. */ std::vector getConstrainedRowSumVector(storm::storage::BitVector const& rowConstraint, storm::storage::BitVector const& columnConstraint) const; - + /*! * Computes a vector whose entries represent the sums of selected columns for all rows in selected row * groups. @@ -711,7 +711,7 @@ namespace storm { * groups. */ std::vector getConstrainedRowGroupSumVector(storm::storage::BitVector const& rowGroupConstraint, storm::storage::BitVector const& columnConstraint) const; - + /*! * Creates a submatrix of the current matrix by dropping all rows and columns whose bits are not * set to one in the given bit vector. @@ -728,10 +728,10 @@ namespace storm { * by the constraints are kept and all others are dropped. */ SparseMatrix getSubmatrix(bool useGroups, storm::storage::BitVector const& rowConstraint, storm::storage::BitVector const& columnConstraint, bool insertDiagonalEntries = false, storm::storage::BitVector const& makeZeroColumns = storm::storage::BitVector()) const; - + /*! - * Restrict rows in grouped rows matrix. Ensures that the number of groups stays the same. - * + * Restrict rows in grouped rows matrix. Ensures that the number of groups stays the same. + * * @param rowsToKeep A bit vector indicating which rows to keep. * @param allowEmptyRowGroups if set to true, the result can potentially have empty row groups. * Otherwise, it is asserted that there are no empty row groups. @@ -757,7 +757,7 @@ namespace storm { * @param rowFilter the selected rows */ SparseMatrix filterEntries(storm::storage::BitVector const& rowFilter) const; - + /*! * Removes all zero entries from this. */ @@ -770,19 +770,19 @@ namespace storm { * @return True if the rows have identical entries. */ bool compareRows(index_type i1, index_type i2) const; - + /*! * Finds duplicate rows in a rowgroup. */ BitVector duplicateRowsInRowgroups() const; - + /** * Swaps the two rows. * @param row1 Index of first row * @param row2 Index of second row */ void swapRows(index_type const& row1, index_type const& row2); - + /*! * Selects exactly one row from each row group of this matrix and returns the resulting matrix. * @@ -791,7 +791,7 @@ namespace storm { * @return A submatrix of the current matrix by selecting one row out of each row group. */ SparseMatrix selectRowsFromRowGroups(std::vector const& rowGroupToRowIndexMapping, bool insertDiagonalEntries = true) const; - + /*! * Selects the rows that are given by the sequence of row indices, allowing to select rows arbitrarily often and with an arbitrary order * The resulting matrix will have a trivial row grouping. @@ -802,7 +802,7 @@ namespace storm { * @return A matrix which rows are selected from this matrix according to the given index sequence */ SparseMatrix selectRowsFromRowIndexSequence(std::vector const& rowIndexSequence, bool insertDiagonalEntries = true) const; - + /*! * Transposes the matrix. * @@ -812,7 +812,7 @@ namespace storm { * @return A sparse matrix that represents the transpose of this matrix. */ storm::storage::SparseMatrix transpose(bool joinGroups = false, bool keepZeros = false) const; - + /*! * Transposes the matrix w.r.t. the selected rows. * This is equivalent to selectRowsFromRowGroups(rowGroupChoices, false).transpose(false, keepZeros) but avoids creating one intermediate matrix. @@ -822,7 +822,7 @@ namespace storm { * */ SparseMatrix transposeSelectedRowsFromRowGroups(std::vector const& rowGroupChoices, bool keepZeros = false) const; - + /*! * Transforms the matrix into an equation system. That is, it transforms the matrix A into a matrix (1-A). */ @@ -833,24 +833,24 @@ namespace storm { * Requires the matrix to contain each diagonal entry and to be square. */ void invertDiagonal(); - + /*! * Negates (w.r.t. addition) all entries that are not on the diagonal. */ void negateAllNonDiagonalEntries(); - + /*! * Sets all diagonal elements to zero. */ void deleteDiagonalEntries(); - + /*! * Calculates the Jacobi decomposition of this sparse matrix. For this operation, the matrix must be square. * * @return A pair (L+U, D^-1) containing the matrix L+U and the inverted diagonal D^-1 (as a vector). */ std::pair, std::vector> getJacobiDecomposition() const; - + /*! * Performs a pointwise multiplication of the entries in the given row of this matrix and the entries of * the given row of the other matrix and returns the sum. @@ -862,8 +862,8 @@ namespace storm { */ template ResultValueType getPointwiseProductRowSum(storm::storage::SparseMatrix const& otherMatrix, index_type const& row) const; - - + + /*! * Performs a pointwise matrix multiplication of the matrix with the given matrix and returns a vector * containing the sum of the entries in each row of the resulting matrix. @@ -876,7 +876,7 @@ namespace storm { */ template std::vector getPointwiseProductRowSumVector(storm::storage::SparseMatrix const& otherMatrix) const; - + /*! * Multiplies the matrix with the given vector and writes the result to the given result vector. * @@ -886,13 +886,13 @@ namespace storm { * @return The product of the matrix and the given vector as the content of the given result vector. */ void multiplyWithVector(std::vector const& vector, std::vector& result, std::vector const* summand = nullptr) const; - + void multiplyWithVectorForward(std::vector const& vector, std::vector& result, std::vector const* summand = nullptr) const; void multiplyWithVectorBackward(std::vector const& vector, std::vector& result, std::vector const* summand = nullptr) const; #ifdef STORM_HAVE_INTELTBB void multiplyWithVectorParallel(std::vector const& vector, std::vector& result, std::vector const* summand = nullptr) const; #endif - + /*! * Multiplies the matrix with the given vector, reduces it according to the given direction and and writes * the result to the given result vector. @@ -907,19 +907,19 @@ namespace storm { * the 'new' choice has a value strictly better (wrt. to the optimization direction) value. * @return The resulting vector the content of the given result vector. */ - void multiplyAndReduce(storm::solver::OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& vector, std::vector const* summand, std::vector& result, std::vector* choices, storm::storage::BitVector* dirOverride = nullptr) const; + void multiplyAndReduce(storm::solver::OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& vector, std::vector const* summand, std::vector& result, std::vector* choices, storm::storage::BitVector const* dirOverride = nullptr) const; - void multiplyAndReduceForward(storm::solver::OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& vector, std::vector const* b, std::vector& result, std::vector* choices, storm::storage::BitVector* dirOverride = nullptr) const; + void multiplyAndReduceForward(storm::solver::OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& vector, std::vector const* b, std::vector& result, std::vector* choices, storm::storage::BitVector const* dirOverride = nullptr) const; template - void multiplyAndReduceForward(std::vector const& rowGroupIndices, std::vector const& vector, std::vector const* summand, std::vector& result, std::vector* choices, storm::storage::BitVector* dirOverride = nullptr) const; + void multiplyAndReduceForward(std::vector const& rowGroupIndices, std::vector const& vector, std::vector const* summand, std::vector& result, std::vector* choices, storm::storage::BitVector const* dirOverride = nullptr) const; - void multiplyAndReduceBackward(storm::solver::OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& vector, std::vector const* b, std::vector& result, std::vector* choices, storm::storage::BitVector* dirOverride = nullptr) const; + void multiplyAndReduceBackward(storm::solver::OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& vector, std::vector const* b, std::vector& result, std::vector* choices, storm::storage::BitVector const* dirOverride = nullptr) const; template - void multiplyAndReduceBackward(std::vector const& rowGroupIndices, std::vector const& vector, std::vector const* b, std::vector& result, std::vector* choices, storm::storage::BitVector* dirOverride = nullptr) const; + void multiplyAndReduceBackward(std::vector const& rowGroupIndices, std::vector const& vector, std::vector const* b, std::vector& result, std::vector* choices, storm::storage::BitVector const* dirOverride = nullptr) const; #ifdef STORM_HAVE_INTELTBB - void multiplyAndReduceParallel(storm::solver::OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& vector, std::vector const* b, std::vector& result, std::vector* choices, storm::storage::BitVector* dirOverride = nullptr) const; + void multiplyAndReduceParallel(storm::solver::OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& vector, std::vector const* b, std::vector& result, std::vector* choices, storm::storage::BitVector const* dirOverride = nullptr) const; template - void multiplyAndReduceParallel(std::vector const& rowGroupIndices, std::vector const& vector, std::vector const* b, std::vector& result, std::vector* choices, storm::storage::BitVector* dirOverride = nullptr) const; + void multiplyAndReduceParallel(std::vector const& rowGroupIndices, std::vector const& vector, std::vector const* b, std::vector& result, std::vector* choices, storm::storage::BitVector const* dirOverride = nullptr) const; #endif /*! @@ -937,11 +937,11 @@ namespace storm { * @param vector The vector with which the matrix is to be multiplied. This vector is interpreted as being * a row vector. * @param result The vector that is supposed to hold the result of the multiplication after the operation. - * @return The product of the matrix and the given vector as the content of the given result vector. The + * @return The product of the matrix and the given vector as the content of the given result vector. The * result is to be interpreted as a row vector. */ void multiplyVectorWithMatrix(std::vector const& vector, std::vector& result) const; - + /*! * Scales each row of the matrix, i.e., multiplies each element in row i with factors[i] * @@ -955,7 +955,7 @@ namespace storm { * @param divisors The divisors with which each row is divided. */ void divideRowsInPlace(std::vector const& divisors); - + /*! * Performs one step of the successive over-relaxation technique. * @@ -975,7 +975,7 @@ namespace storm { * @param result The vector to which to write the result. */ void performWalkerChaeStep(std::vector const& x, std::vector const& columnSums, std::vector const& b, std::vector const& ax, std::vector& result) const; - + /*! * Computes the sum of the entries in a given row. * @@ -983,21 +983,21 @@ namespace storm { * @return The sum of the selected row. */ value_type getRowSum(index_type row) const; - + /*! * Returns the number of non-constant entries */ index_type getNonconstantEntryCount() const; - + /*! * Returns the number of rowGroups that contain a non-constant value */ index_type getNonconstantRowGroupCount() const; - + /*! * Checks for each row whether it sums to one. */ - bool isProbabilistic() const; + bool isProbabilistic() const; /*! * Checks if the current matrix is a submatrix of the given matrix, where a matrix A is called a submatrix * of B if B has no entries in position where A has none. Additionally, the matrices must be of equal size. @@ -1007,10 +1007,10 @@ namespace storm { */ template bool isSubmatrixOf(SparseMatrix const& matrix) const; - + // Returns true if the matrix is the identity matrix bool isIdentityMatrix() const; - + template friend std::ostream& operator<<(std::ostream& out, SparseMatrix const& matrix); @@ -1018,7 +1018,7 @@ namespace storm { * Returns a string describing the dimensions of the matrix. */ std::string getDimensionsAsString() const; - + /*! * Prints the matrix in a dense format, as also used by e.g. Matlab. * Notice that the format does not support multiple rows in a rowgroup. @@ -1026,14 +1026,14 @@ namespace storm { * @out The stream to output to. */ void printAsMatlabMatrix(std::ostream& out) const; - + /*! * Calculates a hash value over all values contained in the matrix. * * @return size_t A hash value for this matrix. */ std::size_t hash() const; - + /*! * Returns an object representing the consecutive rows given by the parameters. * @@ -1067,7 +1067,7 @@ namespace storm { * @return An object representing the given row. */ rows getRow(index_type row); - + /*! * Returns an object representing the offset'th row in the rowgroup * @param rowGroup the row group @@ -1075,7 +1075,7 @@ namespace storm { * @return An object representing the given row. */ const_rows getRow(index_type rowGroup, index_type offset) const; - + /*! * Returns an object representing the offset'th row in the rowgroup * @param rowGroup the row group @@ -1083,7 +1083,7 @@ namespace storm { * @return An object representing the given row. */ rows getRow(index_type rowGroup, index_type offset); - + /*! * Returns an object representing the given row group. * @@ -1091,7 +1091,7 @@ namespace storm { * @return An object representing the given row group. */ const_rows getRowGroup(index_type rowGroup) const; - + /*! * Returns an object representing the given row group. * @@ -1099,7 +1099,7 @@ namespace storm { * @return An object representing the given row group. */ rows getRowGroup(index_type rowGroup); - + /*! * Retrieves an iterator that points to the beginning of the given row. * @@ -1107,7 +1107,7 @@ namespace storm { * @return An iterator that points to the beginning of the given row. */ const_iterator begin(index_type row = 0) const; - + /*! * Retrieves an iterator that points to the beginning of the given row. * @@ -1115,7 +1115,7 @@ namespace storm { * @return An iterator that points to the beginning of the given row. */ iterator begin(index_type row = 0); - + /*! * Retrieves an iterator that points past the end of the given row. * @@ -1138,14 +1138,14 @@ namespace storm { * @return An iterator that points past the end of the last row of the matrix. */ const_iterator end() const; - + /*! * Retrieves an iterator that points past the end of the last row of the matrix. * * @return An iterator that points past the end of the last row of the matrix. */ iterator end(); - + /*! * Returns a copy of the matrix with the chosen internal data type */ @@ -1163,7 +1163,7 @@ namespace storm { return SparseMatrix(columnCount, std::move(newRowIndications), std::move(newColumnsAndValues), std::move(newRowGroupIndices)); } - + private: /*! * Creates a submatrix of the current matrix by keeping only row groups and columns in the given row group @@ -1178,39 +1178,39 @@ namespace storm { * given by the row group constraint are kept and all others are dropped. */ SparseMatrix getSubmatrix(storm::storage::BitVector const& rowGroupConstraint, storm::storage::BitVector const& columnConstraint, std::vector const& rowGroupIndices, bool insertDiagonalEntries = false, storm::storage::BitVector const& makeZeroColumns = storm::storage::BitVector()) const; - + // The number of rows of the matrix. index_type rowCount; - + // The number of columns of the matrix. mutable index_type columnCount; - + // The number of entries in the matrix. index_type entryCount; - + // The number of nonzero entries in the matrix. mutable index_type nonzeroEntryCount; - + // The storage for the columns and values of all entries in the matrix. std::vector> columnsAndValues; - + // A vector containing the indices at which each given row begins. This index is to be interpreted as an // index in the valueStorage and the columnIndications vectors. Put differently, the values of the entries // in row i are valueStorage[rowIndications[i]] to valueStorage[rowIndications[i + 1]] where the last // entry is not included anymore. std::vector rowIndications; - + // A flag indicating whether the matrix has a trivial row grouping. Note that this may be true and yet // there may be row group indices, because they were requested from the outside. bool trivialRowGrouping; - + // A vector indicating the row groups of the matrix. This needs to be mutible in case we create it on-the-fly. mutable boost::optional> rowGroupIndices; }; - + #ifdef STORM_HAVE_CARL std::set getVariables(SparseMatrix const& matrix); #endif - + } // namespace storage } // namespace storm