Storm 1.10.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
51 MatrixEntry(index_type column, value_type value);
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#ifndef WINDOWS
64 MatrixEntry(MatrixEntry&& other) = default;
65 MatrixEntry& operator=(MatrixEntry&& other) = default;
66#endif
67
73 index_type const& getColumn() const;
74
80 void setColumn(index_type const& column);
81
87 value_type const& getValue() const;
88
94 void setValue(value_type const& value);
95
101 std::pair<index_type, value_type> const& getColumnValuePair() const;
102
108 MatrixEntry operator*(value_type factor) const;
109
110 bool operator==(MatrixEntry const& other) const;
111 bool operator!=(MatrixEntry const& other) const;
112
113 template<typename IndexTypePrime, typename ValueTypePrime>
114 friend std::ostream& operator<<(std::ostream& out, MatrixEntry<IndexTypePrime, ValueTypePrime> const& entry);
115
116 private:
117 // The actual matrix entry.
118 std::pair<index_type, value_type> entry;
119};
120
124template<typename IndexType, typename ValueType>
125std::size_t hash_value(MatrixEntry<IndexType, ValueType> const& matrixEntry) {
126 std::size_t seed = 0;
127 boost::hash_combine(seed, matrixEntry.getColumn());
128 boost::hash_combine(seed, matrixEntry.getValue());
129 return seed;
130}
131
135template<typename ValueType>
137 public:
139 typedef ValueType value_type;
140
156 SparseMatrixBuilder(index_type rows = 0, index_type columns = 0, index_type entries = 0, bool forceDimensions = true, bool hasCustomRowGrouping = false,
157 index_type rowGroups = 0);
158
166
180 void addNextValue(index_type row, index_type column, value_type const& value);
181
188 void newRowGroup(index_type startingRow);
189
190 /*
191 * Finalizes the sparse matrix to indicate that initialization process has been completed and the matrix
192 * may now be used. This must be called after all entries have been added to the matrix via addNextValue.
193 *
194 * @param overriddenRowCount If this is set to a value that is greater than the current number of rows,
195 * this will cause the finalize method to add empty rows at the end of the matrix until the given row count
196 * has been matched. Note that this will *not* override the row count that has been given upon construction
197 * (if any), but will only take effect if the matrix has been created without the number of rows given.
198 * @param overriddenColumnCount If this is set to a value that is greater than the current number of columns,
199 * this will cause the finalize method to set the number of columns to the given value. Note that this will
200 * *not* override the column count that has been given upon construction (if any), but will only take effect
201 * if the matrix has been created without the number of columns given. By construction, the matrix will have
202 * no entries in the columns that have been added this way.
203 * @param overriddenRowGroupCount If this is set to a value that is greater than the current number of row
204 * groups, this will cause the method to set the number of row groups to the given value. Note that this will
205 * *not* override the row group count that has been given upon construction (if any), but will only take
206 * effect if the matrix has been created without the number of row groups given. By construction, the row
207 * groups added this way will be empty.
208 */
209 SparseMatrix<value_type> build(index_type overriddenRowCount = 0, index_type overriddenColumnCount = 0, index_type overriddenRowGroupCount = 0);
210
216 index_type getLastRow() const;
217
224
231
240 void replaceColumns(std::vector<index_type> const& replacements, index_type offset);
241
249 void addDiagonalEntry(index_type row, ValueType const& value);
250
251 private:
252 // A flag indicating whether a row count was set upon construction.
253 bool initialRowCountSet;
254
255 // The row count that was initially set (if any).
256 index_type initialRowCount;
257
258 // A flag indicating whether a column count was set upon construction.
259 bool initialColumnCountSet;
260
261 // The column count that was initially set (if any).
262 index_type initialColumnCount;
263
264 // A flag indicating whether an entry count was set upon construction.
265 bool initialEntryCountSet;
266
267 // The number of entries in the matrix.
268 index_type initialEntryCount;
269
270 // A flag indicating whether the initially given dimensions are to be enforced on the resulting matrix.
271 bool forceInitialDimensions;
272
273 // A flag indicating whether the builder is to construct a custom row grouping for the matrix.
274 bool hasCustomRowGrouping;
275
276 // A flag indicating whether the number of row groups was set upon construction.
277 bool initialRowGroupCountSet;
278
279 // The number of row groups in the matrix.
280 index_type initialRowGroupCount;
281
282 // The vector that stores the row-group indices (if they are non-trivial).
283 boost::optional<std::vector<index_type>> rowGroupIndices;
284
285 // The storage for the columns and values of all entries in the matrix.
286 std::vector<MatrixEntry<index_type, value_type>> columnsAndValues;
287
288 // A vector containing the indices at which each given row begins. This index is to be interpreted as an
289 // index in the valueStorage and the columnIndications vectors. Put differently, the values of the entries
290 // in row i are valueStorage[rowIndications[i]] to valueStorage[rowIndications[i + 1]] where the last
291 // entry is not included anymore.
292 std::vector<index_type> rowIndications;
293
294 // Stores the current number of entries in the matrix. This is used for inserting an entry into a matrix
295 // with preallocated storage.
296 index_type currentEntryCount;
297
298 // Stores the row of the last entry in the matrix. This is used for correctly inserting an entry into a
299 // matrix.
300 index_type lastRow;
301
302 // Stores the column of the currently last entry in the matrix. This is used for correctly inserting an
303 // entry into a matrix.
304 index_type lastColumn;
305
306 // Stores the highest column at which an entry was inserted into the matrix.
307 index_type highestColumn;
308
309 // Stores the currently active row group. This is used for correctly constructing the row grouping of the
310 // matrix.
311 index_type currentRowGroupCount;
312
313 boost::optional<ValueType> pendingDiagonalEntry;
314};
315
330template<typename ValueType>
332 public:
333 // Declare adapter classes as friends to use internal data.
334 friend class storm::adapters::GmmxxAdapter<ValueType>;
337 friend class SparseMatrixBuilder<ValueType>;
338
340 typedef ValueType value_type;
341 typedef typename std::vector<MatrixEntry<index_type, value_type>>::iterator iterator;
342 typedef typename std::vector<MatrixEntry<index_type, value_type>>::const_iterator const_iterator;
343
347 class rows {
348 public:
356 rows(iterator begin, index_type entryCount);
357
363 iterator begin();
364
370 iterator end();
371
378
379 private:
380 // The pointer to the columnd and value of the first entry.
381 iterator beginIterator;
382
383 // The number of non-zero entries in the rows.
384 index_type entryCount;
385 };
386
391 public:
400
406 const_iterator begin() const;
407
413 const_iterator end() const;
414
421
422 private:
423 // The pointer to the column and value of the first entry.
424 const_iterator beginIterator;
425
426 // The number of non-zero entries in the rows.
427 index_type entryCount;
428 };
429
436
440 SparseMatrix();
441
448
456 SparseMatrix(SparseMatrix<value_type> const& other, bool insertDiagonalElements);
457
464
473 SparseMatrix(index_type columnCount, std::vector<index_type> const& rowIndications,
474 std::vector<MatrixEntry<index_type, value_type>> const& columnsAndValues, boost::optional<std::vector<index_type>> const& rowGroupIndices);
475
484 SparseMatrix(index_type columnCount, std::vector<index_type>&& rowIndications, std::vector<MatrixEntry<index_type, value_type>>&& columnsAndValues,
485 boost::optional<std::vector<index_type>>&& rowGroupIndices);
486
493
500
507 bool operator==(SparseMatrix<value_type> const& other) const;
508
514 index_type getRowCount() const;
515
522
529
536
545
549 void updateNonzeroEntryCount() const;
550
554 void updateDimensions() const;
555
561 void updateNonzeroEntryCount(std::make_signed<index_type>::type difference);
562
569
577
582
586 index_type getNumRowsInRowGroups(storm::storage::BitVector const& groupConstraint) const;
587
593 std::vector<index_type> const& getRowGroupIndices() const;
594
598 boost::integer_range<index_type> getRowGroupIndices(index_type group) const;
599
605 std::vector<index_type> swapRowGroupIndices(std::vector<index_type>&& newRowGrouping);
606
613 void setRowGroupIndices(std::vector<index_type> const& newRowGroupIndices);
614
620 bool hasTrivialRowGrouping() const;
621
627
636
646 storm::storage::BitVector getRowFilter(storm::storage::BitVector const& groupConstraint, storm::storage::BitVector const& columnConstraints) const;
647
656 storm::storage::BitVector getRowGroupFilter(storm::storage::BitVector const& rowConstraint, bool setIfForAllRowsInGroup) const;
657
665 void makeRowsAbsorbing(storm::storage::BitVector const& rows, bool dropZeroEntries = false);
666
674 void makeRowGroupsAbsorbing(storm::storage::BitVector const& rowGroupConstraint, bool dropZeroEntries = false);
675
685 void makeRowDirac(index_type row, index_type column, bool dropZeroEntries = false);
686
692 std::vector<ValueType> getRowSumVector() const;
693
702
712 std::vector<value_type> getConstrainedRowSumVector(storm::storage::BitVector const& rowConstraint, storm::storage::BitVector const& columnConstraint) const;
713
723 std::vector<value_type> getConstrainedRowGroupSumVector(storm::storage::BitVector const& rowGroupConstraint,
724 storm::storage::BitVector const& columnConstraint) const;
725
741 SparseMatrix getSubmatrix(bool useGroups, storm::storage::BitVector const& rowConstraint, storm::storage::BitVector const& columnConstraint,
742 bool insertDiagonalEntries = false, storm::storage::BitVector const& makeZeroColumns = storm::storage::BitVector()) const;
743
754 SparseMatrix restrictRows(storm::storage::BitVector const& rowsToKeep, bool allowEmptyRowGroups = false) const;
755
762 SparseMatrix permuteRows(std::vector<index_type> const& inversePermutation) const;
763
771 SparseMatrix permuteRowGroupsAndColumns(std::vector<index_type> const& inverseRowGroupPermutation, std::vector<index_type> const& columnPermutation) const;
772
781
785 void dropZeroEntries();
786
793 bool compareRows(index_type i1, index_type i2) const;
794
799
805 void swapRows(index_type const& row1, index_type const& row2);
806
814 SparseMatrix selectRowsFromRowGroups(std::vector<index_type> const& rowGroupToRowIndexMapping, bool insertDiagonalEntries = true) const;
815
825 SparseMatrix selectRowsFromRowIndexSequence(std::vector<index_type> const& rowIndexSequence, bool insertDiagonalEntries = true) const;
826
835 storm::storage::SparseMatrix<value_type> transpose(bool joinGroups = false, bool keepZeros = false) const;
836
845 SparseMatrix<ValueType> transposeSelectedRowsFromRowGroups(std::vector<uint64_t> const& rowGroupChoices, bool keepZeros = false) const;
846
851
856 void invertDiagonal();
857
862
868 void deleteDiagonalEntries(bool dropZeroEntries = false);
869
875 std::pair<storm::storage::SparseMatrix<value_type>, std::vector<value_type>> getJacobiDecomposition() const;
876
886 template<typename OtherValueType, typename ResultValueType = OtherValueType>
887 ResultValueType getPointwiseProductRowSum(storm::storage::SparseMatrix<OtherValueType> const& otherMatrix, index_type const& row) const;
888
899 template<typename OtherValueType, typename ResultValueType = OtherValueType>
900 std::vector<ResultValueType> getPointwiseProductRowSumVector(storm::storage::SparseMatrix<OtherValueType> const& otherMatrix) const;
901
910 void multiplyWithVector(std::vector<value_type> const& vector, std::vector<value_type>& result, std::vector<value_type> const* summand = nullptr) const;
911
912 void multiplyWithVectorForward(std::vector<value_type> const& vector, std::vector<value_type>& result,
913 std::vector<value_type> const* summand = nullptr) const;
914 void multiplyWithVectorBackward(std::vector<value_type> const& vector, std::vector<value_type>& result,
915 std::vector<value_type> const* summand = nullptr) const;
916
931 void multiplyAndReduce(storm::solver::OptimizationDirection const& dir, std::vector<uint64_t> const& rowGroupIndices, std::vector<ValueType> const& vector,
932 std::vector<ValueType> const* summand, std::vector<ValueType>& result, std::vector<uint64_t>* choices) const;
933
934 void multiplyAndReduceForward(storm::solver::OptimizationDirection const& dir, std::vector<uint64_t> const& rowGroupIndices,
935 std::vector<ValueType> const& vector, std::vector<ValueType> const* b, std::vector<ValueType>& result,
936 std::vector<uint64_t>* choices) const;
937 template<typename Compare>
938 void multiplyAndReduceForward(std::vector<uint64_t> const& rowGroupIndices, std::vector<ValueType> const& vector, std::vector<ValueType> const* summand,
939 std::vector<ValueType>& result, std::vector<uint64_t>* choices) const;
940
941 void multiplyAndReduceBackward(storm::solver::OptimizationDirection const& dir, std::vector<uint64_t> const& rowGroupIndices,
942 std::vector<ValueType> const& vector, std::vector<ValueType> const* b, std::vector<ValueType>& result,
943 std::vector<uint64_t>* choices) const;
944 template<typename Compare>
945 void multiplyAndReduceBackward(std::vector<uint64_t> const& rowGroupIndices, std::vector<ValueType> const& vector, std::vector<ValueType> const* b,
946 std::vector<ValueType>& result, std::vector<uint64_t>* choices) const;
947
955 value_type multiplyRowWithVector(index_type row, std::vector<value_type> const& vector) const;
956
966 void multiplyVectorWithMatrix(std::vector<value_type> const& vector, std::vector<value_type>& result) const;
967
973 void scaleRowsInPlace(std::vector<value_type> const& factors);
974
980 void divideRowsInPlace(std::vector<value_type> const& divisors);
981
989 void performSuccessiveOverRelaxationStep(ValueType omega, std::vector<ValueType>& x, std::vector<ValueType> const& b) const;
990
1000 void performWalkerChaeStep(std::vector<ValueType> const& x, std::vector<ValueType> const& columnSums, std::vector<ValueType> const& b,
1001 std::vector<ValueType> const& ax, std::vector<ValueType>& result) const;
1002
1009 value_type getRowSum(index_type row) const;
1010
1015
1020
1024 bool isProbabilistic() const;
1025
1029 bool hasOnlyPositiveEntries() const;
1030
1038 template<typename OtherValueType>
1039 bool isSubmatrixOf(SparseMatrix<OtherValueType> const& matrix) const;
1040
1041 // Returns true if the matrix is the identity matrix
1042 bool isIdentityMatrix() const;
1043
1044 template<typename TPrime>
1045 friend std::ostream& operator<<(std::ostream& out, SparseMatrix<TPrime> const& matrix);
1046
1050 std::string getDimensionsAsString() const;
1051
1058 void printAsMatlabMatrix(std::ostream& out) const;
1059
1065 std::size_t hash() const;
1066
1074 const_rows getRows(index_type startRow, index_type endRow) const;
1075
1083 rows getRows(index_type startRow, index_type endRow);
1084
1091 const_rows getRow(index_type row) const;
1092
1099 rows getRow(index_type row);
1100
1107 const_rows getRow(index_type rowGroup, index_type offset) const;
1108
1115 rows getRow(index_type rowGroup, index_type offset);
1116
1123 const_rows getRowGroup(index_type rowGroup) const;
1124
1131 rows getRowGroup(index_type rowGroup);
1132
1139 const_iterator begin(index_type row) const;
1140
1148
1154 const_iterator begin() const;
1155
1161 iterator begin();
1162
1169 const_iterator end(index_type row) const;
1170
1177 iterator end(index_type row);
1178
1184 const_iterator end() const;
1185
1191 iterator end();
1192
1196 template<typename NewValueType>
1198 std::vector<MatrixEntry<SparseMatrix::index_type, NewValueType>> newColumnsAndValues;
1199 std::vector<SparseMatrix::index_type> newRowIndications(rowIndications);
1200 boost::optional<std::vector<SparseMatrix::index_type>> newRowGroupIndices(rowGroupIndices);
1201
1202 newColumnsAndValues.resize(columnsAndValues.size());
1203 std::transform(
1204 columnsAndValues.begin(), columnsAndValues.end(), newColumnsAndValues.begin(), [](MatrixEntry<SparseMatrix::index_type, ValueType> const& a) {
1205 return MatrixEntry<SparseMatrix::index_type, NewValueType>(a.getColumn(), storm::utility::convertNumber<NewValueType, ValueType>(a.getValue()));
1206 });
1207
1208 return SparseMatrix<NewValueType>(columnCount, std::move(newRowIndications), std::move(newColumnsAndValues), std::move(newRowGroupIndices));
1209 }
1210
1211 private:
1224 SparseMatrix getSubmatrix(storm::storage::BitVector const& rowGroupConstraint, storm::storage::BitVector const& columnConstraint,
1225 std::vector<index_type> const& rowGroupIndices, bool insertDiagonalEntries = false,
1226 storm::storage::BitVector const& makeZeroColumns = storm::storage::BitVector()) const;
1227
1228 // The number of rows of the matrix.
1229 index_type rowCount;
1230
1231 // The number of columns of the matrix.
1232 mutable index_type columnCount;
1233
1234 // The number of entries in the matrix.
1235 index_type entryCount;
1236
1237 // The number of nonzero entries in the matrix.
1238 mutable index_type nonzeroEntryCount;
1239
1240 // The storage for the columns and values of all entries in the matrix.
1241 std::vector<MatrixEntry<index_type, value_type>> columnsAndValues;
1242
1243 // A vector containing the indices at which each given row begins. This index is to be interpreted as an
1244 // index in the valueStorage and the columnIndications vectors. Put differently, the values of the entries
1245 // in row i are valueStorage[rowIndications[i]] to valueStorage[rowIndications[i + 1]] where the last
1246 // entry is not included anymore.
1247 std::vector<index_type> rowIndications;
1248
1249 // A flag indicating whether the matrix has a trivial row grouping. Note that this may be true and yet
1250 // there may be row group indices, because they were requested from the outside.
1251 bool trivialRowGrouping;
1252
1253 // A vector indicating the row groups of the matrix. This needs to be mutible in case we create it on-the-fly.
1254 mutable boost::optional<std::vector<index_type>> rowGroupIndices;
1255};
1256
1257} // namespace storage
1258} // namespace storm
A bit vector that is internally represented as a vector of 64-bit values.
Definition BitVector.h:18
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
This class represents a number of consecutive rows of the matrix.
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.
This class represents a number of consecutive rows of the matrix.
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.
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.
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.
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.
SparseMatrix< value_type > build(index_type overriddenRowCount=0, index_type overriddenColumnCount=0, index_type overriddenRowGroupCount=0)
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].
void convertToEquationSystem()
Transforms the matrix into an equation system.
SparseMatrix()
Constructs an empty sparse matrix.
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.
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.
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.
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 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.
bool isProbabilistic() const
Checks for each row whether it sums to one.
void multiplyWithVectorBackward(std::vector< value_type > const &vector, std::vector< value_type > &result, std::vector< value_type > const *summand=nullptr) const
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.
void updateDimensions() const
Recomputes the number of columns and the number of non-zero entries.
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.
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.
friend class storm::adapters::StormAdapter
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.
MatrixStatus
An enum representing the internal state of the matrix.
SparseMatrix< ValueType > transposeSelectedRowsFromRowGroups(std::vector< uint64_t > const &rowGroupChoices, bool keepZeros=false) const
Transposes the matrix w.r.t.
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.
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.
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.
void dropZeroEntries()
Removes all zero entries from this.
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...
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...
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.
void deleteDiagonalEntries(bool dropZeroEntries=false)
Sets all diagonal elements to zero.
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...
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
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.
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].
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 ...
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
LabParser.cpp.
Definition cli.cpp:18