Storm 1.14.0.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
SparseMatrix.h
Go to the documentation of this file.
1#pragma once
2
3#include <algorithm>
4#include <cstdint>
5#include <iosfwd>
6#include <iterator>
7#include <vector>
8
9#include <boost/functional/hash.hpp>
10#include <boost/optional.hpp>
11#include <boost/range/irange.hpp>
12
16
19
20// Forward declaration for adapter classes.
21namespace storm {
22namespace adapters {
23template<typename ValueType>
25class EigenAdapter;
26class StormAdapter;
27} // namespace adapters
28} // namespace storm
29
30namespace storm {
31namespace storage {
32
33// Forward declare matrix class.
34template<typename T>
35class SparseMatrix;
36
38
39template<typename IndexType, typename ValueType>
41 public:
42 typedef IndexType index_type;
43 typedef ValueType value_type;
44
52
58 MatrixEntry(std::pair<index_type, value_type>&& pair);
59
60 MatrixEntry() = default;
61 MatrixEntry(MatrixEntry const& other) = default;
62 MatrixEntry& operator=(MatrixEntry const& other) = default;
63 MatrixEntry(MatrixEntry&& other) = default;
64 MatrixEntry& operator=(MatrixEntry&& other) = default;
65
71 index_type const& getColumn() const;
72
78 void setColumn(index_type const& column);
79
85 value_type const& getValue() const;
86
92 void setValue(value_type const& value);
93
99 std::pair<index_type, value_type> const& getColumnValuePair() const;
100
107
108 bool operator==(MatrixEntry const& other) const;
109 bool operator!=(MatrixEntry const& other) const;
110
111 template<typename IndexTypePrime, typename ValueTypePrime>
112 friend std::ostream& operator<<(std::ostream& out, MatrixEntry<IndexTypePrime, ValueTypePrime> const& entry);
113
114 private:
115 // The actual matrix entry.
116 std::pair<index_type, value_type> entry;
117};
118
122template<typename IndexType, typename ValueType>
123std::size_t hash_value(MatrixEntry<IndexType, ValueType> const& matrixEntry) {
124 std::size_t seed = 0;
125 boost::hash_combine(seed, matrixEntry.getColumn());
126 boost::hash_combine(seed, matrixEntry.getValue());
127 return seed;
128}
129
133template<typename ValueType>
135 public:
137 typedef ValueType value_type;
138
150
166 SparseMatrixBuilder(index_type rows = 0, index_type columns = 0, index_type entries = 0, bool forceDimensions = true, bool hasCustomRowGrouping = false,
167 index_type rowGroups = 0);
168
176
192 void addNextValue(index_type row, index_type column, value_type const& value);
193
203
210
217 void newRowGroup(index_type startingRow);
218
219 /*
220 * Finalizes the sparse matrix to indicate that initialization process has been completed and the matrix
221 * may now be used. This must be called after all entries have been added to the matrix via addNextValue.
222 *
223 * @param overriddenRowCount If this is set to a nonzero value, the resulting matrix will have exactly this many rows.
224 * If there are fewer rows than that, empty rows are added at the end of the matrix. If rows beyond that
225 * count were already added, an exception is thrown. Note that this will *not* override the row count that has
226 * been given upon construction (if any).
227 * @param overriddenColumnCount If this is set to a nonzero value, the resulting matrix will have exactly this many
228 * columns. By construction, the matrix will have no entries in the columns that have been added this way.
229 * If entries beyond that column count were already added, an exception is thrown. Note that this will *not*
230 * override the column count that has been given upon construction (if any).
231 * @param overriddenRowGroupCount If this is set to a nonzero value, the resulting matrix will have exactly this
232 * many row groups. The row groups added this way are empty. If more row groups were already started, an
233 * exception is thrown. Note that this will *not* override the row group count that has been given upon
234 * construction (if any).
235 */
236 SparseMatrix<value_type> build(index_type overriddenRowCount = 0, index_type overriddenColumnCount = 0, index_type overriddenRowGroupCount = 0);
237
243 index_type getLastRow() const;
244
251
258
267 void replaceColumns(std::vector<index_type> const& replacements, index_type offset);
268
277 void addDiagonalEntry(index_type row, ValueType const& value);
278
279 private:
280 // A flag indicating whether a row count was set upon construction.
281 bool initialRowCountSet;
282
283 // The row count that was initially set (if any).
284 index_type initialRowCount;
285
286 // A flag indicating whether a column count was set upon construction.
287 bool initialColumnCountSet;
288
289 // The column count that was initially set (if any).
290 index_type initialColumnCount;
291
292 // A flag indicating whether an entry count was set upon construction.
293 bool initialEntryCountSet;
294
295 // The number of entries in the matrix.
296 index_type initialEntryCount;
297
298 // A flag indicating whether the initially given dimensions are to be enforced on the resulting matrix.
299 bool forceInitialDimensions;
300
301 // A flag indicating whether the builder is to construct a custom row grouping for the matrix.
302 bool hasCustomRowGrouping;
303
304 // A flag indicating whether the number of row groups was set upon construction.
305 bool initialRowGroupCountSet;
306
307 // The number of row groups in the matrix.
308 index_type initialRowGroupCount;
309
310 // The vector that stores the row-group indices (if they are non-trivial).
311 boost::optional<std::vector<index_type>> rowGroupIndices;
312
313 // The storage for the columns and values of all entries in the matrix.
314 std::vector<MatrixEntry<index_type, value_type>> columnsAndValues;
315
316 // A vector containing the indices at which each given row begins. This index is to be interpreted as an
317 // index in the valueStorage and the columnIndications vectors. Put differently, the values of the entries
318 // in row i are valueStorage[rowIndications[i]] to valueStorage[rowIndications[i + 1]] where the last
319 // entry is not included anymore.
320 std::vector<index_type> rowIndications;
321
322 // Stores the current number of entries in the matrix. This is used for inserting an entry into a matrix
323 // with preallocated storage.
324 index_type currentEntryCount;
325
326 // Stores the row of the last entry in the matrix. This is used for correctly inserting an entry into a
327 // matrix.
328 index_type lastRow;
329
330 // Stores the column of the currently last entry in the matrix. This is used for correctly inserting an
331 // entry into a matrix.
332 index_type lastColumn;
333
334 // Stores the highest column at which an entry was inserted into the matrix.
335 index_type highestColumn;
336
337 // Stores the currently active row group. This is used for correctly constructing the row grouping of the
338 // matrix.
339 index_type currentRowGroupCount;
340
341 boost::optional<ValueType> pendingDiagonalEntry;
342
343 // Specifies how multiple values for the same row and column are combined.
345};
346
361template<typename ValueType>
363 public:
364 // Declare adapter classes as friends to use internal data.
365 friend class storm::adapters::GmmxxAdapter<ValueType>;
367 friend class storm::adapters::StormAdapter;
368 friend class SparseMatrixBuilder<ValueType>;
369
371 typedef ValueType value_type;
372 typedef typename std::vector<MatrixEntry<index_type, value_type>>::iterator iterator;
373 typedef typename std::vector<MatrixEntry<index_type, value_type>>::const_iterator const_iterator;
374
378 class rows {
379 public:
387 rows(iterator begin, index_type entryCount);
388
394 iterator begin();
395
401 iterator end();
402
409
410 private:
411 // The pointer to the columnd and value of the first entry.
412 iterator beginIterator;
413
414 // The number of non-zero entries in the rows.
415 index_type entryCount;
416 };
417
422 public:
431
437 const_iterator begin() const;
438
444 const_iterator end() const;
445
452
453 private:
454 // The pointer to the column and value of the first entry.
455 const_iterator beginIterator;
456
457 // The number of non-zero entries in the rows.
458 index_type entryCount;
459 };
460
467
472
479
487 SparseMatrix(SparseMatrix<value_type> const& other, bool insertDiagonalElements);
488
495
504 SparseMatrix(index_type columnCount, std::vector<index_type> const& rowIndications,
505 std::vector<MatrixEntry<index_type, value_type>> const& columnsAndValues, boost::optional<std::vector<index_type>> const& rowGroupIndices);
506
515 SparseMatrix(index_type columnCount, std::vector<index_type>&& rowIndications, std::vector<MatrixEntry<index_type, value_type>>&& columnsAndValues,
516 boost::optional<std::vector<index_type>>&& rowGroupIndices);
517
524
531
538 bool operator==(SparseMatrix<value_type> const& other) const;
539
546
553
560
567
574
583
588
592 void updateDimensions() const;
593
599 void updateNonzeroEntryCount(std::make_signed<index_type>::type difference);
600
607
615
620
625
631 std::vector<index_type> const& getRowGroupIndices() const;
632
636 boost::integer_range<index_type> getRowGroupIndices(index_type group) const;
637
641 std::vector<index_type> const& getRowIndices() const;
642
648 std::vector<index_type> swapRowGroupIndices(std::vector<index_type>&& newRowGrouping);
649
656 void setRowGroupIndices(std::vector<index_type> const& newRowGroupIndices);
657
664
670
679
689 storm::storage::BitVector getRowFilter(storm::storage::BitVector const& groupConstraint, storm::storage::BitVector const& columnConstraints) const;
690
699 storm::storage::BitVector getRowGroupFilter(storm::storage::BitVector const& rowConstraint, bool setIfForAllRowsInGroup) const;
700
709
717 void makeRowGroupsAbsorbing(storm::storage::BitVector const& rowGroupConstraint, bool dropZeroEntries = false);
718
728 void makeRowDirac(index_type row, index_type column, bool dropZeroEntries = false);
729
735 std::vector<ValueType> getRowSumVector() const;
736
745
755 std::vector<value_type> getConstrainedRowSumVector(storm::storage::BitVector const& rowConstraint, storm::storage::BitVector const& columnConstraint) const;
756
766 std::vector<value_type> getConstrainedRowGroupSumVector(storm::storage::BitVector const& rowGroupConstraint,
767 storm::storage::BitVector const& columnConstraint) const;
768
784 SparseMatrix getSubmatrix(bool useGroups, storm::storage::BitVector const& rowConstraint, storm::storage::BitVector const& columnConstraint,
785 bool insertDiagonalEntries = false, storm::storage::BitVector const& makeZeroColumns = storm::storage::BitVector()) const;
786
797 SparseMatrix restrictRows(storm::storage::BitVector const& rowsToKeep, bool allowEmptyRowGroups = false) const;
798
805 SparseMatrix permuteRows(std::vector<index_type> const& inversePermutation) const;
806
814 SparseMatrix permuteRowGroupsAndColumns(std::vector<index_type> const& inverseRowGroupPermutation, std::vector<index_type> const& columnPermutation) const;
815
824
829
837
842
848 void swapRows(index_type const& row1, index_type const& row2);
849
857 SparseMatrix selectRowsFromRowGroups(std::vector<index_type> const& rowGroupToRowIndexMapping, bool insertDiagonalEntries = true) const;
858
868 SparseMatrix selectRowsFromRowIndexSequence(std::vector<index_type> const& rowIndexSequence, bool insertDiagonalEntries = true) const;
869
878 storm::storage::SparseMatrix<value_type> transpose(bool joinGroups = false, bool keepZeros = false) const;
879
888 SparseMatrix<ValueType> transposeSelectedRowsFromRowGroups(std::vector<uint64_t> const& rowGroupChoices, bool keepZeros = false) const;
889
894
900
905
912
918 std::pair<storm::storage::SparseMatrix<value_type>, std::vector<value_type>> getJacobiDecomposition() const;
919
929 template<typename OtherValueType, typename ResultValueType = OtherValueType>
930 ResultValueType getPointwiseProductRowSum(storm::storage::SparseMatrix<OtherValueType> const& otherMatrix, index_type const& row) const;
931
942 template<typename OtherValueType, typename ResultValueType = OtherValueType>
943 std::vector<ResultValueType> getPointwiseProductRowSumVector(storm::storage::SparseMatrix<OtherValueType> const& otherMatrix) const;
944
953 void multiplyWithVector(std::vector<value_type> const& vector, std::vector<value_type>& result, std::vector<value_type> const* summand = nullptr) const;
954
955 void multiplyWithVectorForward(std::vector<value_type> const& vector, std::vector<value_type>& result,
956 std::vector<value_type> const* summand = nullptr) const;
957 void multiplyWithVectorBackward(std::vector<value_type> const& vector, std::vector<value_type>& result,
958 std::vector<value_type> const* summand = nullptr) const;
959
974 void multiplyAndReduce(storm::solver::OptimizationDirection const& dir, std::vector<uint64_t> const& rowGroupIndices, std::vector<ValueType> const& vector,
975 std::vector<ValueType> const* summand, std::vector<ValueType>& result, std::vector<uint64_t>* choices) const;
976
977 void multiplyAndReduceForward(storm::solver::OptimizationDirection const& dir, std::vector<uint64_t> const& rowGroupIndices,
978 std::vector<ValueType> const& vector, std::vector<ValueType> const* b, std::vector<ValueType>& result,
979 std::vector<uint64_t>* choices) const;
980 template<typename Compare>
981 void multiplyAndReduceForward(std::vector<uint64_t> const& rowGroupIndices, std::vector<ValueType> const& vector, std::vector<ValueType> const* summand,
982 std::vector<ValueType>& result, std::vector<uint64_t>* choices) const;
983
984 void multiplyAndReduceBackward(storm::solver::OptimizationDirection const& dir, std::vector<uint64_t> const& rowGroupIndices,
985 std::vector<ValueType> const& vector, std::vector<ValueType> const* b, std::vector<ValueType>& result,
986 std::vector<uint64_t>* choices) const;
987 template<typename Compare>
988 void multiplyAndReduceBackward(std::vector<uint64_t> const& rowGroupIndices, std::vector<ValueType> const& vector, std::vector<ValueType> const* b,
989 std::vector<ValueType>& result, std::vector<uint64_t>* choices) const;
990
998 value_type multiplyRowWithVector(index_type row, std::vector<value_type> const& vector) const;
999
1009 void multiplyVectorWithMatrix(std::vector<value_type> const& vector, std::vector<value_type>& result) const;
1010
1016 void scaleRowsInPlace(std::vector<value_type> const& factors);
1017
1023 void divideRowsInPlace(std::vector<value_type> const& divisors);
1024
1032 void performSuccessiveOverRelaxationStep(ValueType omega, std::vector<ValueType>& x, std::vector<ValueType> const& b) const;
1033
1043 void performWalkerChaeStep(std::vector<ValueType> const& x, std::vector<ValueType> const& columnSums, std::vector<ValueType> const& b,
1044 std::vector<ValueType> const& ax, std::vector<ValueType>& result) const;
1045
1053
1058
1063
1071 bool isProbabilistic(ValueType const& tolerance, storm::OptionalRef<std::string> reason = {}) const;
1072
1077
1088
1096 template<typename OtherValueType>
1098
1099 // Returns true if the matrix is the identity matrix
1100 bool isIdentityMatrix() const;
1101
1102 template<typename TPrime>
1103 friend std::ostream& operator<<(std::ostream& out, SparseMatrix<TPrime> const& matrix);
1104
1108 std::string getDimensionsAsString() const;
1109
1116 void printAsMatlabMatrix(std::ostream& out) const;
1117
1123 std::size_t hash() const;
1124
1132 const_rows getRows(index_type startRow, index_type endRow) const;
1133
1141 rows getRows(index_type startRow, index_type endRow);
1142
1149 const_rows getRow(index_type row) const;
1150
1158
1165 const_rows getRow(index_type rowGroup, index_type offset) const;
1166
1173 rows getRow(index_type rowGroup, index_type offset);
1174
1181 const_rows getRowGroup(index_type rowGroup) const;
1182
1189 rows getRowGroup(index_type rowGroup);
1190
1198
1206
1213
1220
1228
1236
1243
1250
1254 template<typename NewValueType>
1256 std::vector<MatrixEntry<SparseMatrix::index_type, NewValueType>> newColumnsAndValues;
1257 std::vector<SparseMatrix::index_type> newRowIndications(rowIndications);
1258 boost::optional<std::vector<SparseMatrix::index_type>> newRowGroupIndices(rowGroupIndices);
1259
1260 newColumnsAndValues.resize(columnsAndValues.size());
1261 std::transform(
1262 columnsAndValues.begin(), columnsAndValues.end(), newColumnsAndValues.begin(), [](MatrixEntry<SparseMatrix::index_type, ValueType> const& a) {
1263 return MatrixEntry<SparseMatrix::index_type, NewValueType>(a.getColumn(), storm::utility::convertNumber<NewValueType, ValueType>(a.getValue()));
1264 });
1265
1266 return SparseMatrix<NewValueType>(columnCount, std::move(newRowIndications), std::move(newColumnsAndValues), std::move(newRowGroupIndices));
1267 }
1268
1269 private:
1270 // The number of rows of the matrix.
1271 index_type rowCount;
1272
1273 // The number of columns of the matrix.
1274 mutable index_type columnCount;
1275
1276 // The number of entries in the matrix.
1277 index_type entryCount;
1278
1279 // The number of nonzero entries in the matrix.
1280 mutable index_type nonzeroEntryCount;
1281
1282 // The storage for the columns and values of all entries in the matrix.
1283 std::vector<MatrixEntry<index_type, value_type>> columnsAndValues;
1284
1285 // A vector containing the indices at which each given row begins. This index is to be interpreted as an
1286 // index in the valueStorage and the columnIndications vectors. Put differently, the values of the entries
1287 // in row i are valueStorage[rowIndications[i]] to valueStorage[rowIndications[i + 1]] where the last
1288 // entry is not included anymore.
1289 std::vector<index_type> rowIndications;
1290
1291 // A flag indicating whether the matrix has a trivial row grouping. Note that this may be true and yet
1292 // there may be row group indices, because they were requested from the outside.
1293 bool trivialRowGrouping;
1294
1295 // A vector indicating the row groups of the matrix. This needs to be mutible in case we create it on-the-fly.
1296 mutable boost::optional<std::vector<index_type>> rowGroupIndices;
1297};
1298
1299} // namespace storage
1300} // namespace storm
Helper class that optionally holds a reference to an object of type T.
Definition OptionalRef.h:48
A bit vector that is internally represented as a vector of 64-bit values.
Definition BitVector.h:16
MatrixEntry(index_type column, value_type value)
Constructs a matrix entry with the given column and value.
MatrixEntry operator*(value_type factor) const
Multiplies the entry with the given factor and returns the result.
value_type const & getValue() const
Retrieves the value of the matrix entry.
std::pair< index_type, value_type > const & getColumnValuePair() const
Retrieves a pair of column and value that characterizes this entry.
MatrixEntry(MatrixEntry &&other)=default
void setColumn(index_type const &column)
Sets the column of the current entry.
MatrixEntry()=default
MatrixEntry(MatrixEntry const &other)=default
index_type const & getColumn() const
Retrieves the column of the matrix entry.
bool operator!=(MatrixEntry const &other) const
void setValue(value_type const &value)
Sets the value of the entry in the matrix.
MatrixEntry & operator=(MatrixEntry &&other)=default
MatrixEntry & operator=(MatrixEntry const &other)=default
ValueType value_type
IndexType index_type
friend std::ostream & operator<<(std::ostream &out, MatrixEntry< IndexTypePrime, ValueTypePrime > const &entry)
bool operator==(MatrixEntry const &other) const
MatrixEntry(std::pair< index_type, value_type > &&pair)
Move-constructs the matrix entry fro the given column-value pair.
const_rows(const_iterator begin, index_type entryCount)
Constructs an object that represents the rows defined by the value of the first entry,...
const_iterator end() const
Retrieves an iterator that points past the last entry of the rows.
index_type getNumberOfEntries() const
Retrieves the number of entries in the rows.
const_iterator begin() const
Retrieves an iterator that points to the beginning of the rows.
iterator end()
Retrieves an iterator that points past the last entry of the rows.
iterator begin()
Retrieves an iterator that points to the beginning of the rows.
index_type getNumberOfEntries() const
Retrieves the number of entries in the rows.
rows(iterator begin, index_type entryCount)
Constructs an object that represents the rows defined by the value of the first entry,...
A class that can be used to build a sparse matrix by adding value by value.
index_type getCurrentRowGroupCount() const
Retrieves the current row group count.
AccumulationMode
Specifies how values that are added for the same row and column are combined.
@ ExpectNone
There must not be multiple values for the same row and column.
@ ExpectSame
All values added for the same row and column must be equal. The (single) entry keeps this value.
index_type getLastRow() const
Retrieves the most recently used row.
void addNextValue(index_type row, index_type column, value_type const &value)
Sets the matrix entry at the given row and column to the given value.
void replaceColumns(std::vector< index_type > const &replacements, index_type offset)
Replaces all columns with id > offset according to replacements.
SparseMatrixBuilder(index_type rows=0, index_type columns=0, index_type entries=0, bool forceDimensions=true, bool hasCustomRowGrouping=false, index_type rowGroups=0)
Constructs a sparse matrix builder producing a matrix with the given number of rows,...
void newRowGroup(index_type startingRow)
Starts a new row group in the matrix.
index_type getLastColumn() const
Retrieves the most recently used row.
void addDiagonalEntry(index_type row, ValueType const &value)
Makes sure that a diagonal entry will be inserted at the given row.
void setAccumulationMode(AccumulationMode mode)
Sets how values that are added for the same row and column are combined.
SparseMatrix< value_type > build(index_type overriddenRowCount=0, index_type overriddenColumnCount=0, index_type overriddenRowGroupCount=0)
AccumulationMode getAccumulationMode() const
Retrieves how values that are added for the same row and column are combined.
A class that holds a possibly non-square matrix in the compressed row storage format.
void divideRowsInPlace(std::vector< value_type > const &divisors)
Divides each row of the matrix, i.e., divides each element in row i with divisors[i].
ResultValueType getPointwiseProductRowSum(storm::storage::SparseMatrix< OtherValueType > const &otherMatrix, index_type const &row) const
Performs a pointwise multiplication of the entries in the given row of this matrix and the entries of...
void convertToEquationSystem()
Transforms the matrix into an equation system.
SparseMatrix()
Constructs an empty sparse matrix.
rows getRow(index_type row)
Returns an object representing the given row.
void swapRows(index_type const &row1, index_type const &row2)
Swaps the two rows.
bool operator==(SparseMatrix< value_type > const &other) const
Determines whether the current and the given matrix are semantically equal.
const_rows getRow(index_type row) const
Returns an object representing the given row.
storm::storage::BitVector getRowFilter(storm::storage::BitVector const &groupConstraint, storm::storage::BitVector const &columnConstraints) const
Returns the indices of all rows that.
index_type getSizeOfLargestRowGroup() const
Returns the size of the largest row group of the matrix.
SparseMatrix selectRowsFromRowGroups(std::vector< index_type > const &rowGroupToRowIndexMapping, bool insertDiagonalEntries=true) const
Selects exactly one row from each row group of this matrix and returns the resulting matrix.
void multiplyWithVectorForward(std::vector< value_type > const &vector, std::vector< value_type > &result, std::vector< value_type > const *summand=nullptr) const
index_type getEntryCount() const
Returns the number of entries in the matrix.
bool isProbabilistic(ValueType const &tolerance, storm::OptionalRef< std::string > reason={}) const
Checks for each row whether (i) each entry is between zero and one and (ii) all entries sum to one.
SparseMatrix(index_type columnCount, std::vector< index_type > &&rowIndications, std::vector< MatrixEntry< index_type, value_type > > &&columnsAndValues, boost::optional< std::vector< index_type > > &&rowGroupIndices)
Constructs a sparse matrix by moving the given contents.
const_rows getRows(index_type startRow, index_type endRow) const
Returns an object representing the consecutive rows given by the parameters.
index_type getNonconstantEntryCount() const
Returns the number of non-constant entries.
void multiplyVectorWithMatrix(std::vector< value_type > const &vector, std::vector< value_type > &result) const
Multiplies the vector to the matrix from the left and writes the result to the given result vector.
void multiplyAndReduceBackward(storm::solver::OptimizationDirection const &dir, std::vector< uint64_t > const &rowGroupIndices, std::vector< ValueType > const &vector, std::vector< ValueType > const *b, std::vector< ValueType > &result, std::vector< uint64_t > *choices) const
index_type getNumRowsInRowGroups(storm::storage::BitVector const &groupConstraint) const
Returns the total number of rows that are in one of the specified row groups.
void makeRowsAbsorbing(storm::storage::BitVector const &rows, bool dropZeroEntries=false)
This function makes the given rows absorbing.
rows getRows(index_type startRow, index_type endRow)
Returns an object representing the consecutive rows given by the parameters.
void multiplyAndReduceBackward(std::vector< uint64_t > const &rowGroupIndices, std::vector< ValueType > const &vector, std::vector< ValueType > const *b, std::vector< ValueType > &result, std::vector< uint64_t > *choices) const
SparseMatrix(SparseMatrix< value_type > const &other)
Constructs a sparse matrix by performing a deep-copy of the given matrix.
void multiplyWithVector(std::vector< value_type > const &vector, std::vector< value_type > &result, std::vector< value_type > const *summand=nullptr) const
Multiplies the matrix with the given vector and writes the result to the given result vector.
void updateNonzeroEntryCount() const
Recompute the nonzero entry count.
void multiplyWithVectorBackward(std::vector< value_type > const &vector, std::vector< value_type > &result, std::vector< value_type > const *summand=nullptr) const
boost::integer_range< index_type > getRowGroupIndices(index_type group) const
Returns the row indices within the given group.
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
Creates a submatrix of the current matrix by dropping all rows and columns whose bits are not set to ...
void performWalkerChaeStep(std::vector< ValueType > const &x, std::vector< ValueType > const &columnSums, std::vector< ValueType > const &b, std::vector< ValueType > const &ax, std::vector< ValueType > &result) const
Performs one step of the Walker-Chae technique.
SparseMatrix(SparseMatrix< value_type > &&other)
Constructs a sparse matrix by moving the contents of the given matrix to the newly created one.
void updateDimensions() const
Recomputes the number of columns and the number of non-zero entries.
const_iterator begin(index_type row) const
Retrieves an iterator that points to the beginning of the given row.
void printAsMatlabMatrix(std::ostream &out) const
Prints the matrix in a dense format, as also used by e.g.
void performSuccessiveOverRelaxationStep(ValueType omega, std::vector< ValueType > &x, std::vector< ValueType > const &b) const
Performs one step of the successive over-relaxation technique.
SparseMatrix(index_type columnCount, std::vector< index_type > const &rowIndications, std::vector< MatrixEntry< index_type, value_type > > const &columnsAndValues, boost::optional< std::vector< index_type > > const &rowGroupIndices)
Constructs a sparse matrix by copying the given contents.
std::vector< value_type > getConstrainedRowSumVector(storm::storage::BitVector const &rowConstraint, storm::storage::BitVector const &columnConstraint) const
Computes a vector whose i-th entry is the sum of the entries in the i-th selected row where only thos...
BitVector duplicateRowsInRowgroups() const
Finds duplicate rows in a rowgroup.
bool compareRows(index_type i1, index_type i2) const
Compares two rows.
const_rows getRowGroup(index_type rowGroup) const
Returns an object representing the given row group.
SparseMatrix permuteRows(std::vector< index_type > const &inversePermutation) const
Permute rows of the matrix according to the vector.
void setRowGroupIndices(std::vector< index_type > const &newRowGroupIndices)
Sets the row grouping to the given one.
void negateAllNonDiagonalEntries()
Negates (w.r.t.
const_iterator begin() const
Retrieves an iterator that points to the beginning of the first row of the matrix.
std::vector< index_type > swapRowGroupIndices(std::vector< index_type > &&newRowGrouping)
Swaps the grouping of rows of this matrix.
SparseMatrix restrictRows(storm::storage::BitVector const &rowsToKeep, bool allowEmptyRowGroups=false) const
Restrict rows in grouped rows matrix.
std::vector< ValueType > getRowSumVector() const
Sums the entries in all rows.
SparseMatrix< NewValueType > toValueType() const
Returns a copy of the matrix with the chosen internal data type.
value_type multiplyRowWithVector(index_type row, std::vector< value_type > const &vector) const
Multiplies a single row of the matrix with the given vector and returns the result.
SparseMatrix< ValueType > transposeSelectedRowsFromRowGroups(std::vector< uint64_t > const &rowGroupChoices, bool keepZeros=false) const
Transposes the matrix w.r.t.
iterator begin()
Retrieves an iterator that points to the beginning of the first row of the matrix.
std::vector< index_type > const & getRowIndices() const
Returns the entry indices within the given row.
index_type getRowEntryCount(index_type const row) const
Returns the number of entries in the given row of the matrix.
void multiplyAndReduceForward(storm::solver::OptimizationDirection const &dir, std::vector< uint64_t > const &rowGroupIndices, std::vector< ValueType > const &vector, std::vector< ValueType > const *b, std::vector< ValueType > &result, std::vector< uint64_t > *choices) const
value_type getRowSum(index_type row) const
Computes the sum of the entries in a given row.
const_iterator end(index_type row) const
Retrieves an iterator that points past the end of the given row.
SparseMatrix permuteRowGroupsAndColumns(std::vector< index_type > const &inverseRowGroupPermutation, std::vector< index_type > const &columnPermutation) const
Permutes row groups and columns of the matrix according to the given permutations.
iterator begin(index_type row)
Retrieves an iterator that points to the beginning of the given row.
void multiplyAndReduce(storm::solver::OptimizationDirection const &dir, std::vector< uint64_t > const &rowGroupIndices, std::vector< ValueType > const &vector, std::vector< ValueType > const *summand, std::vector< ValueType > &result, std::vector< uint64_t > *choices) const
Multiplies the matrix with the given vector, reduces it according to the given direction and and writ...
index_type getRowGroupCount() const
Returns the number of row groups in the matrix.
const_rows getRow(index_type rowGroup, index_type offset) const
Returns an object representing the offset'th row in the rowgroup.
bool isSubmatrixOf(SparseMatrix< OtherValueType > const &matrix) const
Checks if the current matrix is a submatrix of the given matrix, where a matrix A is called a submatr...
SparseMatrix< value_type > & operator=(SparseMatrix< value_type > const &other)
Assigns the contents of the given matrix to the current one by deep-copying its contents.
void makeRowGroupsAbsorbing(storm::storage::BitVector const &rowGroupConstraint, bool dropZeroEntries=false)
This function makes the groups of rows given by the bit vector absorbing.
std::string getDimensionsAsString() const
Returns a string describing the dimensions of the matrix.
index_type getColumnCount() const
Returns the number of columns of the matrix.
std::pair< storm::storage::SparseMatrix< value_type >, std::vector< value_type > > getJacobiDecomposition() const
Calculates the Jacobi decomposition of this sparse matrix.
void makeRowDirac(index_type row, index_type column, bool dropZeroEntries=false)
This function makes the given row Dirac.
std::vector< MatrixEntry< index_type, value_type > >::const_iterator const_iterator
value_type getConstrainedRowSum(index_type row, storm::storage::BitVector const &columns) const
Sums the entries in the given row and columns.
SparseMatrix(SparseMatrix< value_type > const &other, bool insertDiagonalElements)
Constructs a sparse matrix by performing a deep-copy of the given matrix.
rows getRow(index_type rowGroup, index_type offset)
Returns an object representing the offset'th row in the rowgroup.
std::vector< ResultValueType > getPointwiseProductRowSumVector(storm::storage::SparseMatrix< OtherValueType > const &otherMatrix) const
Performs a pointwise matrix multiplication of the matrix with the given matrix and returns a vector c...
void deleteDiagonalEntries(bool dropZeroEntries=false)
Sets all diagonal elements to zero.
rows getRowGroup(index_type rowGroup)
Returns an object representing the given row group.
SparseMatrix< value_type > & operator=(SparseMatrix< value_type > &&other)
Assigns the contents of the given matrix to the current one by moving its contents.
bool hasTrivialRowGrouping() const
Retrieves whether the matrix has a trivial row grouping.
void invertDiagonal()
Inverts all entries on the diagonal, i.e.
storm::storage::BitVector getRowGroupFilter(storm::storage::BitVector const &rowConstraint, bool setIfForAllRowsInGroup) const
Returns the indices of all row groups selected by the row constraints.
void makeRowGroupingTrivial()
Makes the row grouping of this matrix trivial.
SparseMatrix selectRowsFromRowIndexSequence(std::vector< index_type > const &rowIndexSequence, bool insertDiagonalEntries=true) const
Selects the rows that are given by the sequence of row indices, allowing to select rows arbitrarily o...
bool isProbabilisticGraphPreserving() const
Checks whether the support graph of the matrix is preserved by every way of resolving the uncertainty...
std::size_t hash() const
Calculates a hash value over all values contained in the matrix.
std::vector< index_type > const & getRowGroupIndices() const
Returns the grouping of rows of this matrix.
std::vector< MatrixEntry< index_type, value_type > >::iterator iterator
iterator end()
Retrieves an iterator that points past the end of the last row of the matrix.
index_type getRowGroupSize(index_type group) const
Returns the size of the given row group.
std::vector< value_type > getConstrainedRowGroupSumVector(storm::storage::BitVector const &rowGroupConstraint, storm::storage::BitVector const &columnConstraint) const
Computes a vector whose entries represent the sums of selected columns for all rows in selected row g...
storm::storage::SparseMatrix< value_type > transpose(bool joinGroups=false, bool keepZeros=false) const
Transposes the matrix.
bool hasOnlyPositiveEntries() const
Checks whether each present entry is strictly positive (omitted entries are not considered).
friend std::ostream & operator<<(std::ostream &out, SparseMatrix< TPrime > const &matrix)
index_type getRowCount() const
Returns the number of rows of the matrix.
void updateNonzeroEntryCount(std::make_signed< index_type >::type difference)
Change the nonzero entry count by the provided value.
SparseMatrixIndexType index_type
index_type getNonzeroEntryCount() const
Returns the cached number of nonzero entries in the matrix.
const_iterator end() const
Retrieves an iterator that points past the end of the last row of the matrix.
index_type getNonconstantRowGroupCount() const
Returns the number of rowGroups that contain a non-constant value.
void scaleRowsInPlace(std::vector< value_type > const &factors)
Scales each row of the matrix, i.e., multiplies each element in row i with factors[i].
iterator end(index_type row)
Retrieves an iterator that points past the end of the given row.
index_type getRowGroupEntryCount(index_type const group) const
Returns the number of entries in the given row group of the matrix.
storm::storage::BitVector getRowFilter(storm::storage::BitVector const &groupConstraint) const
Returns a bitvector representing the set of rows, with all indices set that correspond to one of the ...
void multiplyAndReduceForward(std::vector< uint64_t > const &rowGroupIndices, std::vector< ValueType > const &vector, std::vector< ValueType > const *summand, std::vector< ValueType > &result, std::vector< uint64_t > *choices) const
SparseMatrix filterEntries(storm::storage::BitVector const &rowFilter) const
Returns a copy of this matrix that only considers entries in the selected rows.
std::size_t hash_value(MatrixEntry< IndexType, ValueType > const &matrixEntry)
Computes the hash value of a matrix entry.
storm::storage::sparse::state_type SparseMatrixIndexType