Storm 1.12.0.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
SparseMatrix.cpp
Go to the documentation of this file.
2
3#include <iterator>
4
20
21namespace storm {
22namespace storage {
23
24template<typename IndexType, typename ValueType>
25MatrixEntry<IndexType, ValueType>::MatrixEntry(IndexType column, ValueType value) : entry(column, value) {
26 // Intentionally left empty.
27}
28
29template<typename IndexType, typename ValueType>
30MatrixEntry<IndexType, ValueType>::MatrixEntry(std::pair<IndexType, ValueType>&& pair) : entry(std::move(pair)) {
31 // Intentionally left empty.
32}
33
34template<typename IndexType, typename ValueType>
36 return this->entry.first;
37}
38
39template<typename IndexType, typename ValueType>
40void MatrixEntry<IndexType, ValueType>::setColumn(IndexType const& column) {
41 this->entry.first = column;
42}
43
44template<typename IndexType, typename ValueType>
46 return this->entry.second;
47}
48
49template<typename IndexType, typename ValueType>
50void MatrixEntry<IndexType, ValueType>::setValue(ValueType const& value) {
51 this->entry.second = value;
52}
53
54template<typename IndexType, typename ValueType>
55std::pair<IndexType, ValueType> const& MatrixEntry<IndexType, ValueType>::getColumnValuePair() const {
56 return this->entry;
57}
58
59template<typename IndexType, typename ValueType>
61 return MatrixEntry(this->getColumn(), this->getValue() * factor);
62}
63
64template<typename IndexType, typename ValueType>
66 return this->entry.first == other.entry.first && this->entry.second == other.entry.second;
67}
68
69template<typename IndexType, typename ValueType>
71 return !(*this == other);
72}
73
74template<typename IndexTypePrime, typename ValueTypePrime>
75std::ostream& operator<<(std::ostream& out, MatrixEntry<IndexTypePrime, ValueTypePrime> const& entry) {
76 out << "(" << entry.getColumn() << ", " << entry.getValue() << ")";
77 return out;
78}
79
80template<typename ValueType>
81SparseMatrixBuilder<ValueType>::SparseMatrixBuilder(index_type rows, index_type columns, index_type entries, bool forceDimensions, bool hasCustomRowGrouping,
82 index_type rowGroups)
83 : initialRowCountSet(rows != 0),
84 initialRowCount(rows),
85 initialColumnCountSet(columns != 0),
86 initialColumnCount(columns),
87 initialEntryCountSet(entries != 0),
88 initialEntryCount(entries),
89 forceInitialDimensions(forceDimensions),
90 hasCustomRowGrouping(hasCustomRowGrouping),
91 initialRowGroupCountSet(rowGroups != 0),
92 initialRowGroupCount(rowGroups),
93 rowGroupIndices(),
94 columnsAndValues(),
95 rowIndications(),
96 currentEntryCount(0),
97 lastRow(0),
98 lastColumn(0),
99 highestColumn(0),
100 currentRowGroupCount(0) {
101 // Prepare the internal storage.
102 if (initialRowCountSet) {
103 rowIndications.reserve(initialRowCount + 1);
104 }
105 if (initialEntryCountSet) {
106 columnsAndValues.reserve(initialEntryCount);
107 }
108 if (hasCustomRowGrouping) {
109 rowGroupIndices = std::vector<index_type>();
110 }
111 if (initialRowGroupCountSet && hasCustomRowGrouping) {
112 rowGroupIndices.get().reserve(initialRowGroupCount + 1);
113 }
114 rowIndications.push_back(0);
115}
116
117template<typename ValueType>
119 : initialRowCountSet(false),
120 initialRowCount(0),
121 initialColumnCountSet(false),
122 initialColumnCount(0),
123 initialEntryCountSet(false),
124 initialEntryCount(0),
125 forceInitialDimensions(false),
126 hasCustomRowGrouping(!matrix.trivialRowGrouping),
127 initialRowGroupCountSet(false),
128 initialRowGroupCount(0),
129 rowGroupIndices(),
130 columnsAndValues(std::move(matrix.columnsAndValues)),
131 rowIndications(std::move(matrix.rowIndications)),
132 currentEntryCount(matrix.entryCount),
133 currentRowGroupCount() {
134 lastRow = matrix.rowCount == 0 ? 0 : matrix.rowCount - 1;
135 lastColumn = columnsAndValues.empty() ? 0 : columnsAndValues.back().getColumn();
136 highestColumn = matrix.getColumnCount() == 0 ? 0 : matrix.getColumnCount() - 1;
137
138 // If the matrix has a custom row grouping, we move it and remove the last element to make it 'open' again.
139 if (hasCustomRowGrouping) {
140 rowGroupIndices = std::move(matrix.rowGroupIndices);
141 if (!rowGroupIndices->empty()) {
142 rowGroupIndices.get().pop_back();
143 }
144 currentRowGroupCount = rowGroupIndices->empty() ? 0 : rowGroupIndices.get().size() - 1;
145 }
146
147 // Likewise, we need to 'open' the row indications again.
148 if (!rowIndications.empty()) {
149 rowIndications.pop_back();
150 }
151}
152
153template<typename ValueType>
154void SparseMatrixBuilder<ValueType>::addNextValue(index_type row, index_type column, ValueType const& value) {
155 // Check that we did not move backwards wrt. the row.
156 STORM_LOG_THROW(row >= lastRow, storm::exceptions::InvalidArgumentException,
157 "Adding an element in row " << row << ", but an element in row " << lastRow << " has already been added.");
158 STORM_LOG_ASSERT(columnsAndValues.size() == currentEntryCount, "Unexpected size of columnsAndValues vector.");
159
160 // Check if a diagonal entry shall be inserted before
161 if (pendingDiagonalEntry) {
162 index_type diagColumn = hasCustomRowGrouping ? currentRowGroupCount - 1 : lastRow;
163 if (row > lastRow || column >= diagColumn) {
164 ValueType diagValue = std::move(pendingDiagonalEntry.get());
165 pendingDiagonalEntry = boost::none;
166 // Add the pending diagonal value now
167 if (row == lastRow && column == diagColumn) {
168 // The currently added value coincides with the diagonal entry!
169 // We add up the values and repeat this call.
170 addNextValue(row, column, diagValue + value);
171 // We return here because the above call already did all the work.
172 return;
173 } else {
174 addNextValue(lastRow, diagColumn, diagValue);
175 }
176 }
177 }
178
179 // If the element is in the same row, but was not inserted in the correct order, we need to fix the row after
180 // the insertion.
181 bool fixCurrentRow = row == lastRow && column < lastColumn;
182 // If the element is in the same row and column as the previous entry, we add them up...
183 // unless there is no entry in this row yet, which might happen either for the very first entry or when only a diagonal value has been added
184 if (row == lastRow && column == lastColumn && rowIndications.back() < currentEntryCount) {
185 columnsAndValues.back().setValue(columnsAndValues.back().getValue() + value);
186 } else {
187 // If we switched to another row, we have to adjust the missing entries in the row indices vector.
188 if (row != lastRow) {
189 // Otherwise, we need to push the correct values to the vectors, which might trigger reallocations.
190 assert(rowIndications.size() == lastRow + 1);
191 rowIndications.resize(row + 1, currentEntryCount);
192 lastRow = row;
193 }
194
195 lastColumn = column;
196
197 // Finally, set the element and increase the current size.
198 columnsAndValues.emplace_back(column, value);
199 highestColumn = std::max(highestColumn, column);
200 ++currentEntryCount;
201
202 // If we need to fix the row, do so now.
203 if (fixCurrentRow) {
204 // TODO we fix this row directly after the out-of-order insertion, but the code does not exploit that fact.
205 STORM_LOG_TRACE("Fix row " << row << " as column " << column << " is added out-of-order.");
206 // First, we sort according to columns.
207 std::sort(columnsAndValues.begin() + rowIndications.back(), columnsAndValues.end(),
209 return a.getColumn() < b.getColumn();
210 });
211
212 auto insertIt = columnsAndValues.begin() + rowIndications.back();
213 uint64_t elementsToRemove = 0;
214 for (auto it = insertIt + 1; it != columnsAndValues.end(); ++it) {
215 // Iterate over all entries in this last row and detect duplicates.
216 if (it->getColumn() == insertIt->getColumn()) {
217 // This entry is a duplicate of the column. Update the previous entry.
218 insertIt->setValue(insertIt->getValue() + it->getValue());
219 elementsToRemove++;
220 } else {
221 insertIt = it;
222 }
223 }
224 // Then, we eliminate those duplicate entries.
225 // We cast the result of std::unique to void to silence a warning issued due to a [[nodiscard]] attribute
226 static_cast<void>(std::unique(columnsAndValues.begin() + rowIndications.back(), columnsAndValues.end(),
228 storm::storage::MatrixEntry<index_type, ValueType> const& b) { return a.getColumn() == b.getColumn(); }));
229
230 if (elementsToRemove > 0) {
231 STORM_LOG_WARN("Unordered insertion into matrix builder caused duplicate entries.");
232 currentEntryCount -= elementsToRemove;
233 columnsAndValues.resize(columnsAndValues.size() - elementsToRemove);
234 }
235 lastColumn = columnsAndValues.back().getColumn();
236 }
237 }
238
239 // In case we did not expect this value, we throw an exception.
240 if (forceInitialDimensions) {
241 STORM_LOG_THROW(!initialRowCountSet || lastRow < initialRowCount, storm::exceptions::OutOfRangeException,
242 "Cannot insert value at illegal row " << lastRow << ".");
243 STORM_LOG_THROW(!initialColumnCountSet || lastColumn < initialColumnCount, storm::exceptions::OutOfRangeException,
244 "Cannot insert value at illegal column " << lastColumn << ".");
245 STORM_LOG_THROW(!initialEntryCountSet || currentEntryCount <= initialEntryCount, storm::exceptions::OutOfRangeException,
246 "Too many entries in matrix, expected only " << initialEntryCount << ".");
247 }
248}
249
250template<typename ValueType>
252 STORM_LOG_THROW(hasCustomRowGrouping, storm::exceptions::InvalidStateException, "Matrix was not created to have a custom row grouping.");
253 STORM_LOG_THROW(startingRow >= lastRow, storm::exceptions::InvalidStateException, "Illegal row group with negative size.");
254
255 // If there still is a pending diagonal entry, we need to add it now (otherwise, the correct diagonal column will be unclear)
256 if (pendingDiagonalEntry) {
257 STORM_LOG_ASSERT(currentRowGroupCount > 0, "Diagonal entry was set before opening the first row group.");
258 index_type diagColumn = currentRowGroupCount - 1;
259 ValueType diagValue = std::move(pendingDiagonalEntry.get());
260 pendingDiagonalEntry = boost::none; // clear now, so addNextValue works properly
261 addNextValue(lastRow, diagColumn, diagValue);
262 }
263
264 rowGroupIndices.get().push_back(startingRow);
265 ++currentRowGroupCount;
266
267 // Handle the case where the previous row group ends with one or more empty rows
268 if (lastRow + 1 < startingRow) {
269 // Close all rows from the most recent one to the starting row.
270 assert(rowIndications.size() == lastRow + 1);
271 rowIndications.resize(startingRow, currentEntryCount);
272 // Reset the most recently seen row/column to allow for proper insertion of the following elements.
273 lastRow = startingRow - 1;
274 lastColumn = 0;
275 }
276}
277
278template<typename ValueType>
280 index_type overriddenRowGroupCount) {
281 // If there still is a pending diagonal entry, we need to add it now
282 if (pendingDiagonalEntry) {
283 index_type diagColumn = hasCustomRowGrouping ? currentRowGroupCount - 1 : lastRow;
284 ValueType diagValue = std::move(pendingDiagonalEntry.get());
285 pendingDiagonalEntry = boost::none; // clear now, so addNextValue works properly
286 addNextValue(lastRow, diagColumn, diagValue);
287 }
288
289 bool hasEntries = currentEntryCount != 0;
290
291 uint_fast64_t rowCount = hasEntries ? lastRow + 1 : 0;
292
293 // If the last row group was empty, we need to add one more to the row count, because otherwise this empty row is not counted.
294 if (hasCustomRowGrouping) {
295 if (lastRow < rowGroupIndices->back()) {
296 ++rowCount;
297 }
298 }
299
300 if (initialRowCountSet && forceInitialDimensions) {
301 STORM_LOG_THROW(rowCount <= initialRowCount, storm::exceptions::InvalidStateException,
302 "Expected not more than " << initialRowCount << " rows, but got " << rowCount << ".");
303 rowCount = std::max(rowCount, initialRowCount);
304 }
305
306 rowCount = std::max(rowCount, overriddenRowCount);
307
308 // If the current row count was overridden, we may need to add empty rows.
309 for (index_type i = lastRow + 1; i < rowCount; ++i) {
310 rowIndications.push_back(currentEntryCount);
311 }
312
313 // We put a sentinel element at the last position of the row indices array. This eases iteration work,
314 // as now the indices of row i are always between rowIndications[i] and rowIndications[i + 1], also for
315 // the first and last row.
316 if (rowCount > 0) {
317 rowIndications.push_back(currentEntryCount);
318 }
319 STORM_LOG_ASSERT(rowCount == rowIndications.size() - 1,
320 "Wrong sizes of row indications vector: (Rowcount) " << rowCount << " != " << (rowIndications.size() - 1) << " (Vector).");
321 uint_fast64_t columnCount = hasEntries ? highestColumn + 1 : 0;
322 if (initialColumnCountSet && forceInitialDimensions) {
323 STORM_LOG_THROW(columnCount <= initialColumnCount, storm::exceptions::InvalidStateException,
324 "Expected not more than " << initialColumnCount << " columns, but got " << columnCount << ".");
325 columnCount = std::max(columnCount, initialColumnCount);
326 }
327 columnCount = std::max(columnCount, overriddenColumnCount);
328
329 uint_fast64_t entryCount = currentEntryCount;
330 if (initialEntryCountSet && forceInitialDimensions) {
331 STORM_LOG_THROW(entryCount == initialEntryCount, storm::exceptions::InvalidStateException,
332 "Expected " << initialEntryCount << " entries, but got " << entryCount << ".");
333 }
334
335 // Check whether row groups are missing some entries.
336 if (hasCustomRowGrouping) {
337 uint_fast64_t rowGroupCount = currentRowGroupCount;
338 if (initialRowGroupCountSet && forceInitialDimensions) {
339 STORM_LOG_THROW(rowGroupCount <= initialRowGroupCount, storm::exceptions::InvalidStateException,
340 "Expected not more than " << initialRowGroupCount << " row groups, but got " << rowGroupCount << ".");
341 rowGroupCount = std::max(rowGroupCount, initialRowGroupCount);
342 }
343 rowGroupCount = std::max(rowGroupCount, overriddenRowGroupCount);
344
345 for (index_type i = currentRowGroupCount; i <= rowGroupCount; ++i) {
346 rowGroupIndices.get().push_back(rowCount);
347 }
348 }
349
350 return SparseMatrix<ValueType>(columnCount, std::move(rowIndications), std::move(columnsAndValues), std::move(rowGroupIndices));
351}
352
353template<typename ValueType>
357
358template<typename ValueType>
360 if (this->hasCustomRowGrouping) {
361 return currentRowGroupCount;
362 } else {
363 return getLastRow() + 1;
364 }
365}
366
367template<typename ValueType>
369 return lastColumn;
370}
371
372// Debug method for printing the current matrix
373template<typename ValueType>
374void print(std::vector<typename SparseMatrix<ValueType>::index_type> const& rowGroupIndices,
375 std::vector<MatrixEntry<typename SparseMatrix<ValueType>::index_type, typename SparseMatrix<ValueType>::value_type>> const& columnsAndValues,
376 std::vector<typename SparseMatrix<ValueType>::index_type> const& rowIndications) {
377 typename SparseMatrix<ValueType>::index_type endGroups;
379 // Iterate over all row groups.
380 for (typename SparseMatrix<ValueType>::index_type group = 0; group < rowGroupIndices.size(); ++group) {
381 std::cout << "\t---- group " << group << "/" << (rowGroupIndices.size() - 1) << " ---- \n";
382 endGroups = group < rowGroupIndices.size() - 1 ? rowGroupIndices[group + 1] : rowIndications.size();
383 // Iterate over all rows in a row group
384 for (typename SparseMatrix<ValueType>::index_type i = rowGroupIndices[group]; i < endGroups; ++i) {
385 endRows = i < rowIndications.size() - 1 ? rowIndications[i + 1] : columnsAndValues.size();
386 // Print the actual row.
387 std::cout << "Row " << i << " (" << rowIndications[i] << " - " << endRows << ")" << ": ";
388 for (typename SparseMatrix<ValueType>::index_type pos = rowIndications[i]; pos < endRows; ++pos) {
389 std::cout << "(" << columnsAndValues[pos].getColumn() << ": " << columnsAndValues[pos].getValue() << ") ";
390 }
391 std::cout << '\n';
392 }
393 }
394}
395
396template<typename ValueType>
397void SparseMatrixBuilder<ValueType>::replaceColumns(std::vector<index_type> const& replacements, index_type offset) {
398 index_type maxColumn = 0;
399
400 for (index_type row = 0; row < rowIndications.size(); ++row) {
401 bool changed = false;
402 auto startRow = std::next(columnsAndValues.begin(), rowIndications[row]);
403 auto endRow = row < rowIndications.size() - 1 ? std::next(columnsAndValues.begin(), rowIndications[row + 1]) : columnsAndValues.end();
404 for (auto entry = startRow; entry != endRow; ++entry) {
405 if (entry->getColumn() >= offset) {
406 // Change column
407 entry->setColumn(replacements[entry->getColumn() - offset]);
408 changed = true;
409 }
410 maxColumn = std::max(maxColumn, entry->getColumn());
412 if (changed) {
413 // Sort columns in row
414 std::sort(startRow, endRow,
416 // Assert no equal elements
417 STORM_LOG_ASSERT(std::is_sorted(startRow, endRow,
419 return a.getColumn() < b.getColumn();
420 }),
421 "Columns not sorted.");
422 }
423 }
424
425 highestColumn = maxColumn;
426 lastColumn = columnsAndValues.empty() ? 0 : columnsAndValues.back().getColumn();
427}
428
429template<typename ValueType>
431 STORM_LOG_THROW(row >= lastRow, storm::exceptions::InvalidArgumentException,
432 "Adding a diagonal element in row " << row << ", but an element in row " << lastRow << " has already been added.");
433 if (pendingDiagonalEntry) {
434 if (row == lastRow) {
435 // Add the two diagonal entries, nothing else to be done.
436 pendingDiagonalEntry.get() += value;
437 return;
438 } else {
439 // add the pending entry
440 index_type column = hasCustomRowGrouping ? currentRowGroupCount - 1 : lastRow;
441 ValueType diagValue = std::move(pendingDiagonalEntry.get());
442 pendingDiagonalEntry = boost::none; // clear now, so addNextValue works properly
443 addNextValue(lastRow, column, diagValue);
444 }
446 pendingDiagonalEntry = value;
447 if (lastRow != row) {
448 assert(rowIndications.size() == lastRow + 1);
449 rowIndications.resize(row + 1, currentEntryCount);
450 lastRow = row;
451 lastColumn = 0;
452 }
453}
455template<typename ValueType>
456SparseMatrix<ValueType>::rows::rows(iterator begin, index_type entryCount) : beginIterator(begin), entryCount(entryCount) {
457 // Intentionally left empty.
458}
459
460template<typename ValueType>
464
465template<typename ValueType>
467 return beginIterator + entryCount;
468}
469
470template<typename ValueType>
474
475template<typename ValueType>
476SparseMatrix<ValueType>::const_rows::const_rows(const_iterator begin, index_type entryCount) : beginIterator(begin), entryCount(entryCount) {
477 // Intentionally left empty.
478}
479
480template<typename ValueType>
482 return beginIterator;
483}
484
485template<typename ValueType>
487 return beginIterator + entryCount;
488}
489
490template<typename ValueType>
494
495template<typename ValueType>
497 : rowCount(0), columnCount(0), entryCount(0), nonzeroEntryCount(0), columnsAndValues(), rowIndications(), rowGroupIndices() {
498 // Intentionally left empty.
499}
500
501template<typename ValueType>
503 : rowCount(other.rowCount),
504 columnCount(other.columnCount),
505 entryCount(other.entryCount),
506 nonzeroEntryCount(other.nonzeroEntryCount),
507 columnsAndValues(other.columnsAndValues),
508 rowIndications(other.rowIndications),
509 trivialRowGrouping(other.trivialRowGrouping),
510 rowGroupIndices(other.rowGroupIndices) {
511 // Intentionally left empty.
513
514template<typename ValueType>
515SparseMatrix<ValueType>::SparseMatrix(SparseMatrix<value_type> const& other, bool insertDiagonalElements) {
516 storm::storage::BitVector rowConstraint(other.getRowCount(), true);
517 storm::storage::BitVector columnConstraint(other.getColumnCount(), true);
518 *this = other.getSubmatrix(false, rowConstraint, columnConstraint, insertDiagonalElements);
520
521template<typename ValueType>
523 : rowCount(other.rowCount),
524 columnCount(other.columnCount),
525 entryCount(other.entryCount),
526 nonzeroEntryCount(other.nonzeroEntryCount),
527 columnsAndValues(std::move(other.columnsAndValues)),
528 rowIndications(std::move(other.rowIndications)),
529 trivialRowGrouping(other.trivialRowGrouping),
530 rowGroupIndices(std::move(other.rowGroupIndices)) {
531 // Now update the source matrix
532 other.rowCount = 0;
533 other.columnCount = 0;
534 other.entryCount = 0;
535}
536
537template<typename ValueType>
538SparseMatrix<ValueType>::SparseMatrix(index_type columnCount, std::vector<index_type> const& rowIndications,
539 std::vector<MatrixEntry<index_type, ValueType>> const& columnsAndValues,
540 boost::optional<std::vector<index_type>> const& rowGroupIndices)
541 : rowCount(rowIndications.size() - 1),
542 columnCount(columnCount),
543 entryCount(columnsAndValues.size()),
544 nonzeroEntryCount(0),
545 columnsAndValues(columnsAndValues),
546 rowIndications(rowIndications),
547 trivialRowGrouping(!rowGroupIndices),
548 rowGroupIndices(rowGroupIndices) {
550}
551
552template<typename ValueType>
553SparseMatrix<ValueType>::SparseMatrix(index_type columnCount, std::vector<index_type>&& rowIndications,
554 std::vector<MatrixEntry<index_type, ValueType>>&& columnsAndValues,
555 boost::optional<std::vector<index_type>>&& rowGroupIndices)
556 : columnCount(columnCount),
557 nonzeroEntryCount(0),
558 columnsAndValues(std::move(columnsAndValues)),
559 rowIndications(std::move(rowIndications)),
560 rowGroupIndices(std::move(rowGroupIndices)) {
561 // Initialize some variables here which depend on other variables
562 // This way we are more robust against different initialization orders
563 this->rowCount = this->rowIndications.size() - 1;
564 this->entryCount = this->columnsAndValues.size();
565 this->trivialRowGrouping = !this->rowGroupIndices;
567}
568
569template<typename ValueType>
571 // Only perform assignment if source and target are not the same.
572 if (this != &other) {
573 rowCount = other.rowCount;
574 columnCount = other.columnCount;
575 entryCount = other.entryCount;
576 nonzeroEntryCount = other.nonzeroEntryCount;
577
578 columnsAndValues = other.columnsAndValues;
579 rowIndications = other.rowIndications;
580 rowGroupIndices = other.rowGroupIndices;
581 trivialRowGrouping = other.trivialRowGrouping;
582 }
583 return *this;
585
586template<typename ValueType>
588 // Only perform assignment if source and target are not the same.
589 if (this != &other) {
590 rowCount = other.rowCount;
591 columnCount = other.columnCount;
592 entryCount = other.entryCount;
593 nonzeroEntryCount = other.nonzeroEntryCount;
594
595 columnsAndValues = std::move(other.columnsAndValues);
596 rowIndications = std::move(other.rowIndications);
597 rowGroupIndices = std::move(other.rowGroupIndices);
598 trivialRowGrouping = other.trivialRowGrouping;
599 }
600 return *this;
602
603template<typename ValueType>
605 if (this == &other) {
606 return true;
607 }
609 bool equalityResult = true;
610
611 equalityResult &= this->getRowCount() == other.getRowCount();
612 if (!equalityResult) {
613 return false;
614 }
615 equalityResult &= this->getColumnCount() == other.getColumnCount();
616 if (!equalityResult) {
617 return false;
618 }
619 if (!this->hasTrivialRowGrouping() && !other.hasTrivialRowGrouping()) {
620 equalityResult &= this->getRowGroupIndices() == other.getRowGroupIndices();
621 } else {
622 equalityResult &= this->hasTrivialRowGrouping() && other.hasTrivialRowGrouping();
624 if (!equalityResult) {
625 return false;
626 }
627
628 // For the actual contents, we need to do a little bit more work, because we want to ignore elements that
629 // are set to zero, please they may be represented implicitly in the other matrix.
630 for (index_type row = 0; row < this->getRowCount(); ++row) {
631 for (const_iterator it1 = this->begin(row), ite1 = this->end(row), it2 = other.begin(row), ite2 = other.end(row); it1 != ite1 && it2 != ite2;
632 ++it1, ++it2) {
633 // Skip over all zero entries in both matrices.
634 while (it1 != ite1 && storm::utility::isZero(it1->getValue())) {
635 ++it1;
636 }
637 while (it2 != ite2 && storm::utility::isZero(it2->getValue())) {
638 ++it2;
639 }
640 if ((it1 == ite1) || (it2 == ite2)) {
641 equalityResult = (it1 == ite1) ^ (it2 == ite2);
642 break;
643 } else {
644 if (it1->getColumn() != it2->getColumn() || it1->getValue() != it2->getValue()) {
645 equalityResult = false;
646 break;
647 }
648 }
650 if (!equalityResult) {
651 return false;
652 }
653 }
654
655 return equalityResult;
656}
657
658template<typename ValueType>
662
663template<typename ValueType>
667
668template<typename ValueType>
672
673template<typename ValueType>
675 index_type result = 0;
676 if (!this->hasTrivialRowGrouping()) {
677 for (auto row : this->getRowGroupIndices(group)) {
678 result += (this->rowIndications[row + 1] - this->rowIndications[row]);
679 }
680 } else {
681 result += (this->rowIndications[group + 1] - this->rowIndications[group]);
682 }
683 return result;
684}
685
686template<typename ValueType>
688 return nonzeroEntryCount;
689}
690
691template<typename ValueType>
693 this->nonzeroEntryCount = 0;
694 for (auto const& element : *this) {
695 if (element.getValue() != storm::utility::zero<ValueType>()) {
696 ++this->nonzeroEntryCount;
697 }
698 }
699}
700
701template<typename ValueType>
702void SparseMatrix<ValueType>::updateNonzeroEntryCount(std::make_signed<index_type>::type difference) {
703 this->nonzeroEntryCount += difference;
705
706template<typename ValueType>
708 this->nonzeroEntryCount = 0;
709 this->columnCount = 0;
710 for (auto const& element : *this) {
711 if (element.getValue() != storm::utility::zero<ValueType>()) {
712 ++this->nonzeroEntryCount;
713 this->columnCount = std::max(element.getColumn() + 1, this->columnCount);
714 }
716}
717
718template<typename ValueType>
720 if (!this->hasTrivialRowGrouping()) {
721 return rowGroupIndices.get().size() - 1;
722 } else {
723 return rowCount;
724 }
725}
727template<typename ValueType>
731
732template<typename ValueType>
734 if (this->hasTrivialRowGrouping()) {
735 return 1;
736 }
737 index_type res = 0;
738 index_type previousGroupStart = 0;
739 for (auto const& i : rowGroupIndices.get()) {
740 res = std::max(res, i - previousGroupStart);
741 previousGroupStart = i;
742 }
743 return res;
745
746template<typename ValueType>
748 if (this->hasTrivialRowGrouping()) {
749 return groupConstraint.getNumberOfSetBits();
750 }
751 index_type numRows = 0;
752 index_type rowGroupIndex = groupConstraint.getNextSetIndex(0);
753 while (rowGroupIndex < this->getRowGroupCount()) {
754 index_type start = this->getRowGroupIndices()[rowGroupIndex];
755 rowGroupIndex = groupConstraint.getNextUnsetIndex(rowGroupIndex + 1);
756 index_type end = this->getRowGroupIndices()[rowGroupIndex];
757 // All rows with index in [start,end) are selected.
758 numRows += end - start;
759 rowGroupIndex = groupConstraint.getNextSetIndex(rowGroupIndex + 1);
760 }
761 return numRows;
762}
763
764template<typename ValueType>
765std::vector<typename SparseMatrix<ValueType>::index_type> const& SparseMatrix<ValueType>::getRowGroupIndices() const {
766 // If there is no current row grouping, we need to create it.
767 if (!this->rowGroupIndices) {
768 STORM_LOG_ASSERT(trivialRowGrouping, "Only trivial row-groupings can be constructed on-the-fly.");
769 this->rowGroupIndices = storm::utility::vector::buildVectorForRange(static_cast<index_type>(0), this->getRowGroupCount() + 1);
770 }
771 return rowGroupIndices.get();
772}
773
774template<typename ValueType>
775std::vector<typename SparseMatrix<ValueType>::index_type> const& SparseMatrix<ValueType>::getRowIndices() const {
776 return rowIndications;
777}
778
779template<typename ValueType>
780boost::integer_range<typename SparseMatrix<ValueType>::index_type> SparseMatrix<ValueType>::getRowGroupIndices(index_type group) const {
781 STORM_LOG_ASSERT(group < this->getRowGroupCount(),
782 "Invalid row group index:" << group << ". Only " << this->getRowGroupCount() << " row groups available.");
783 if (this->rowGroupIndices) {
784 return boost::irange(rowGroupIndices.get()[group], rowGroupIndices.get()[group + 1]);
785 } else {
786 return boost::irange(group, group + 1);
787 }
789
790template<typename ValueType>
791std::vector<typename SparseMatrix<ValueType>::index_type> SparseMatrix<ValueType>::swapRowGroupIndices(std::vector<index_type>&& newRowGrouping) {
792 std::vector<index_type> result;
793 if (this->rowGroupIndices) {
794 result = std::move(rowGroupIndices.get());
795 rowGroupIndices = std::move(newRowGrouping);
797 return result;
798}
799
800template<typename ValueType>
801void SparseMatrix<ValueType>::setRowGroupIndices(std::vector<index_type> const& newRowGroupIndices) {
802 trivialRowGrouping = false;
803 rowGroupIndices = newRowGroupIndices;
804}
805
806template<typename ValueType>
808 return trivialRowGrouping;
809}
810
811template<typename ValueType>
813 if (trivialRowGrouping) {
815 !rowGroupIndices || rowGroupIndices.get() == storm::utility::vector::buildVectorForRange(static_cast<index_type>(0), this->getRowGroupCount() + 1),
816 "Row grouping is supposed to be trivial but actually it is not.");
817 } else {
818 trivialRowGrouping = true;
819 rowGroupIndices = boost::none;
820 }
821}
822
823template<typename ValueType>
825 storm::storage::BitVector res(this->getRowCount(), false);
826 for (auto group : groupConstraint) {
827 res.setMultiple(getRowGroupIndices()[group], getRowGroupSize(group));
829 return res;
830}
831
832template<typename ValueType>
834 storm::storage::BitVector const& columnConstraint) const {
835 storm::storage::BitVector result(this->getRowCount(), false);
836 for (auto group : groupConstraint) {
837 for (auto row : this->getRowGroupIndices(group)) {
838 bool choiceSatisfiesColumnConstraint = true;
839 for (auto const& entry : this->getRow(row)) {
840 if (!columnConstraint.get(entry.getColumn())) {
841 choiceSatisfiesColumnConstraint = false;
842 break;
843 }
844 }
845 if (choiceSatisfiesColumnConstraint) {
846 result.set(row, true);
847 }
849 }
850 return result;
851}
852
853template<typename ValueType>
855 STORM_LOG_ASSERT(!this->hasTrivialRowGrouping(), "Tried to get a row group filter but this matrix does not have row groups");
856 storm::storage::BitVector result(this->getRowGroupCount(), false);
857 auto const& groupIndices = this->getRowGroupIndices();
858 if (setIfForAllRowsInGroup) {
859 for (uint64_t group = 0; group < this->getRowGroupCount(); ++group) {
860 if (rowConstraint.getNextUnsetIndex(groupIndices[group]) >= groupIndices[group + 1]) {
861 // All rows within this group are set
862 result.set(group, true);
863 }
865 } else {
866 for (uint64_t group = 0; group < this->getRowGroupCount(); ++group) {
867 if (rowConstraint.getNextSetIndex(groupIndices[group]) < groupIndices[group + 1]) {
868 // Some row is set
869 result.set(group, true);
870 }
872 }
873 return result;
874}
875
876template<typename ValueType>
878 // First transform ALL rows without dropping zero entries, then drop zero entries once
879 // This prevents iteration over the whole matrix every time an entry is set to zero.
880 for (auto row : rows) {
881 makeRowDirac(row, row, false);
882 }
883 if (dropZeroEntries) {
884 this->dropZeroEntries();
885 }
886}
887
888template<typename ValueType>
890 // First transform ALL rows without dropping zero entries, then drop zero entries once.
891 // This prevents iteration over the whole matrix every time an entry is set to zero.
892 if (!this->hasTrivialRowGrouping()) {
893 for (auto rowGroup : rowGroupConstraint) {
894 for (index_type row = this->getRowGroupIndices()[rowGroup]; row < this->getRowGroupIndices()[rowGroup + 1]; ++row) {
895 makeRowDirac(row, rowGroup, false);
896 }
897 }
898 } else {
899 for (auto rowGroup : rowGroupConstraint) {
900 makeRowDirac(rowGroup, rowGroup, false);
901 }
902 }
904 this->dropZeroEntries();
905 }
906}
907
908template<typename ValueType>
910 iterator columnValuePtr = this->begin(row);
911 iterator columnValuePtrEnd = this->end(row);
912
913 // If the row has no elements in it, we cannot make it absorbing, because we would need to move all elements
914 // in the vector of nonzeros otherwise.
915 if (columnValuePtr >= columnValuePtrEnd) {
916 throw storm::exceptions::InvalidStateException()
917 << "Illegal call to SparseMatrix::makeRowDirac: cannot make row " << row << " absorbing, because there is no entry in this row.";
918 }
919 iterator lastColumnValuePtr = this->end(row) - 1;
920
921 // If there is at least one entry in this row, we can set it to one, modify its column value to the
922 // one given by the parameter and set all subsequent elements of this row to zero.
923 // However, we want to preserve that column indices within a row are ascending, so we pick an entry that is close to the desired column index
924 while (columnValuePtr->getColumn() < column && columnValuePtr != lastColumnValuePtr) {
925 if (!storm::utility::isZero(columnValuePtr->getValue())) {
926 --this->nonzeroEntryCount;
927 }
928 columnValuePtr->setValue(storm::utility::zero<ValueType>());
929 ++columnValuePtr;
930 }
931 // At this point, we have found the first entry whose column is >= the desired column (or the last entry of the row, if no such column exist)
932 if (storm::utility::isZero(columnValuePtr->getValue())) {
933 ++this->nonzeroEntryCount;
935 columnValuePtr->setValue(storm::utility::one<ValueType>());
936 columnValuePtr->setColumn(column);
937 for (++columnValuePtr; columnValuePtr != columnValuePtrEnd; ++columnValuePtr) {
938 if (!storm::utility::isZero(columnValuePtr->getValue())) {
939 --this->nonzeroEntryCount;
940 }
941 columnValuePtr->setValue(storm::utility::zero<ValueType>());
942 }
943 if (dropZeroEntries) {
945 }
946}
947
948template<typename ValueType>
950 const_iterator end1 = this->end(i1);
951 const_iterator end2 = this->end(i2);
952 const_iterator it1 = this->begin(i1);
953 const_iterator it2 = this->begin(i2);
954 for (; it1 != end1 && it2 != end2; ++it1, ++it2) {
955 if (*it1 != *it2) {
956 return false;
957 }
959 if (it1 == end1 && it2 == end2) {
960 return true;
961 }
962 return false;
963}
964
965template<typename ValueType>
967 BitVector bv(this->getRowCount());
968 for (size_t rowgroup = 0; rowgroup < this->getRowGroupCount(); ++rowgroup) {
969 for (size_t row1 = this->getRowGroupIndices().at(rowgroup); row1 < this->getRowGroupIndices().at(rowgroup + 1); ++row1) {
970 for (size_t row2 = row1; row2 < this->getRowGroupIndices().at(rowgroup + 1); ++row2) {
971 if (compareRows(row1, row2)) {
972 bv.set(row2);
973 }
974 }
975 }
977 return bv;
978}
979
980template<typename ValueType>
982 if (row1 == row2) {
983 return;
984 }
985
986 // Get the index of the row that has more / less entries than the other.
987 index_type largerRow = getRow(row1).getNumberOfEntries() > getRow(row2).getNumberOfEntries() ? row1 : row2;
988 index_type smallerRow = largerRow == row1 ? row2 : row1;
989 index_type rowSizeDifference = getRow(largerRow).getNumberOfEntries() - getRow(smallerRow).getNumberOfEntries();
990
991 // Save contents of larger row.
992 auto copyRow = getRow(largerRow);
993 std::vector<MatrixEntry<index_type, value_type>> largerRowContents(copyRow.begin(), copyRow.end());
994
995 if (largerRow < smallerRow) {
996 auto writeIt = getRows(largerRow, smallerRow + 1).begin();
997
998 // Write smaller row to its new position.
999 for (auto& smallerRowEntry : getRow(smallerRow)) {
1000 *writeIt = std::move(smallerRowEntry);
1001 ++writeIt;
1002 }
1004 // Write the intermediate rows into their correct position.
1005 if (!storm::utility::isZero(rowSizeDifference)) {
1006 for (auto& intermediateRowEntry : getRows(largerRow + 1, smallerRow)) {
1007 *writeIt = std::move(intermediateRowEntry);
1008 ++writeIt;
1009 }
1010 } else {
1011 // skip the intermediate rows
1012 writeIt = getRow(smallerRow).begin();
1013 }
1014
1015 // Write the larger row to its new position.
1016 for (auto& largerRowEntry : largerRowContents) {
1017 *writeIt = std::move(largerRowEntry);
1018 ++writeIt;
1019 }
1020
1021 STORM_LOG_ASSERT(writeIt == getRow(smallerRow).end(), "Unexpected position of write iterator.");
1023 // Update the row indications to account for the shift of indices at where the rows now start.
1024 if (!storm::utility::isZero(rowSizeDifference)) {
1025 for (index_type row = largerRow + 1; row <= smallerRow; ++row) {
1026 rowIndications[row] -= rowSizeDifference;
1027 }
1028 }
1029 } else {
1030 auto writeIt = getRows(smallerRow, largerRow + 1).end() - 1;
1032 // Write smaller row to its new position
1033 auto copyRow = getRow(smallerRow);
1034 for (auto smallerRowEntryIt = copyRow.end() - 1; smallerRowEntryIt != copyRow.begin() - 1; --smallerRowEntryIt) {
1035 *writeIt = std::move(*smallerRowEntryIt);
1036 --writeIt;
1037 }
1038
1039 // Write the intermediate rows into their correct position.
1040 if (!storm::utility::isZero(rowSizeDifference)) {
1041 for (auto intermediateRowEntryIt = getRows(smallerRow + 1, largerRow).end() - 1;
1042 intermediateRowEntryIt != getRows(smallerRow + 1, largerRow).begin() - 1; --intermediateRowEntryIt) {
1043 *writeIt = std::move(*intermediateRowEntryIt);
1044 --writeIt;
1045 }
1046 } else {
1047 // skip the intermediate rows
1048 writeIt = getRow(smallerRow).end() - 1;
1050
1051 // Write the larger row to its new position.
1052 for (auto largerRowEntryIt = largerRowContents.rbegin(); largerRowEntryIt != largerRowContents.rend(); ++largerRowEntryIt) {
1053 *writeIt = std::move(*largerRowEntryIt);
1054 --writeIt;
1055 }
1056
1057 STORM_LOG_ASSERT(writeIt == getRow(smallerRow).begin() - 1, "Unexpected position of write iterator.");
1058
1059 // Update row indications.
1060 // Update the row indications to account for the shift of indices at where the rows now start.
1061 if (!storm::utility::isZero(rowSizeDifference)) {
1062 for (index_type row = smallerRow + 1; row <= largerRow; ++row) {
1063 rowIndications[row] += rowSizeDifference;
1064 }
1066 }
1067}
1068
1069template<typename ValueType>
1070std::vector<ValueType> SparseMatrix<ValueType>::getRowSumVector() const {
1071 std::vector<ValueType> result(this->getRowCount());
1073 index_type row = 0;
1074 for (auto resultIt = result.begin(), resultIte = result.end(); resultIt != resultIte; ++resultIt, ++row) {
1075 *resultIt = getRowSum(row);
1076 }
1077
1078 return result;
1079}
1080
1081template<typename ValueType>
1083 ValueType result = storm::utility::zero<ValueType>();
1084 for (const_iterator it = this->begin(row), ite = this->end(row); it != ite; ++it) {
1085 if (constraint.get(it->getColumn())) {
1086 result += it->getValue();
1087 }
1088 }
1089 return result;
1091
1092template<typename ValueType>
1094 storm::storage::BitVector const& columnConstraint) const {
1095 std::vector<ValueType> result(rowConstraint.getNumberOfSetBits());
1096 index_type currentRowCount = 0;
1097 for (auto row : rowConstraint) {
1098 result[currentRowCount++] = getConstrainedRowSum(row, columnConstraint);
1099 }
1100 return result;
1101}
1102
1103template<typename ValueType>
1105 storm::storage::BitVector const& columnConstraint) const {
1106 std::vector<ValueType> result;
1107 result.reserve(this->getNumRowsInRowGroups(rowGroupConstraint));
1108 if (!this->hasTrivialRowGrouping()) {
1109 for (auto rowGroup : rowGroupConstraint) {
1110 for (index_type row = this->getRowGroupIndices()[rowGroup]; row < this->getRowGroupIndices()[rowGroup + 1]; ++row) {
1111 result.push_back(getConstrainedRowSum(row, columnConstraint));
1112 }
1113 }
1114 } else {
1115 for (auto rowGroup : rowGroupConstraint) {
1116 result.push_back(getConstrainedRowSum(rowGroup, columnConstraint));
1117 }
1118 }
1119 return result;
1120}
1121
1122template<typename ValueType>
1124 storm::storage::BitVector const& columnConstraint, bool insertDiagonalElements,
1125 storm::storage::BitVector const& makeZeroColumns) const {
1126 if (useGroups) {
1127 return getSubmatrix(rowConstraint, columnConstraint, this->getRowGroupIndices(), insertDiagonalElements, makeZeroColumns);
1128 } else {
1129 // Create a fake row grouping to reduce this to a call to a more general method.
1130 std::vector<index_type> fakeRowGroupIndices(rowCount + 1);
1131 index_type i = 0;
1132 for (std::vector<index_type>::iterator it = fakeRowGroupIndices.begin(); it != fakeRowGroupIndices.end(); ++it, ++i) {
1133 *it = i;
1134 }
1135 auto res = getSubmatrix(rowConstraint, columnConstraint, fakeRowGroupIndices, insertDiagonalElements, makeZeroColumns);
1136
1137 // Create a new row grouping that reflects the new sizes of the row groups if the current matrix has a
1138 // non trivial row-grouping.
1139 if (!this->hasTrivialRowGrouping()) {
1140 std::vector<index_type> newRowGroupIndices;
1141 newRowGroupIndices.push_back(0);
1142 auto selectedRowIt = rowConstraint.begin();
1143
1144 // For this, we need to count how many rows were preserved in every group.
1145 for (index_type group = 0; group < this->getRowGroupCount(); ++group) {
1146 index_type newRowCount = 0;
1147 while (*selectedRowIt < this->getRowGroupIndices()[group + 1]) {
1148 ++selectedRowIt;
1149 ++newRowCount;
1150 }
1151 if (newRowCount > 0) {
1152 newRowGroupIndices.push_back(newRowGroupIndices.back() + newRowCount);
1153 }
1155
1156 res.trivialRowGrouping = false;
1157 res.rowGroupIndices = newRowGroupIndices;
1158 }
1159
1160 return res;
1162}
1163
1164template<typename ValueType>
1165SparseMatrix<ValueType> SparseMatrix<ValueType>::getSubmatrix(storm::storage::BitVector const& rowGroupConstraint,
1166 storm::storage::BitVector const& columnConstraint, std::vector<index_type> const& rowGroupIndices,
1167 bool insertDiagonalEntries, storm::storage::BitVector const& makeZeroColumns) const {
1168 STORM_LOG_THROW(!rowGroupConstraint.empty() && !columnConstraint.empty(), storm::exceptions::InvalidArgumentException, "Cannot build empty submatrix.");
1169 index_type submatrixColumnCount = columnConstraint.getNumberOfSetBits();
1170
1171 // Start by creating a temporary vector that stores for each index whose bit is set to true the number of
1172 // bits that were set before that particular index.
1173 std::vector<index_type> columnBitsSetBeforeIndex = columnConstraint.getNumberOfSetBitsBeforeIndices();
1174 std::unique_ptr<std::vector<index_type>> tmp;
1175 if (rowGroupConstraint != columnConstraint) {
1176 tmp = std::make_unique<std::vector<index_type>>(rowGroupConstraint.getNumberOfSetBitsBeforeIndices());
1177 }
1178 std::vector<index_type> const& rowBitsSetBeforeIndex = tmp ? *tmp : columnBitsSetBeforeIndex;
1179
1180 // Then, we need to determine the number of entries and the number of rows of the submatrix.
1181 index_type subEntries = 0;
1182 index_type subRows = 0;
1183 index_type rowGroupCount = 0;
1184 for (auto index : rowGroupConstraint) {
1185 subRows += rowGroupIndices[index + 1] - rowGroupIndices[index];
1186 for (index_type i = rowGroupIndices[index]; i < rowGroupIndices[index + 1]; ++i) {
1187 bool foundDiagonalElement = false;
1188
1189 for (const_iterator it = this->begin(i), ite = this->end(i); it != ite; ++it) {
1190 if (columnConstraint.get(it->getColumn()) && (makeZeroColumns.size() == 0 || !makeZeroColumns.get(it->getColumn()))) {
1191 ++subEntries;
1192
1193 if (columnBitsSetBeforeIndex[it->getColumn()] == rowBitsSetBeforeIndex[index]) {
1194 foundDiagonalElement = true;
1195 }
1196 }
1197 }
1199 // If requested, we need to reserve one entry more for inserting the diagonal zero entry.
1200 if (insertDiagonalEntries && !foundDiagonalElement && rowGroupCount < submatrixColumnCount) {
1201 ++subEntries;
1202 }
1203 }
1204 ++rowGroupCount;
1205 }
1206
1207 // Create and initialize resulting matrix.
1208 SparseMatrixBuilder<ValueType> matrixBuilder(subRows, submatrixColumnCount, subEntries, true, !this->hasTrivialRowGrouping());
1209
1210 // Copy over selected entries.
1211 rowGroupCount = 0;
1212 index_type rowCount = 0;
1213 subEntries = 0;
1214 for (auto index : rowGroupConstraint) {
1215 if (!this->hasTrivialRowGrouping()) {
1216 matrixBuilder.newRowGroup(rowCount);
1217 }
1218 for (index_type i = rowGroupIndices[index]; i < rowGroupIndices[index + 1]; ++i) {
1219 bool insertedDiagonalElement = false;
1220
1221 for (const_iterator it = this->begin(i), ite = this->end(i); it != ite; ++it) {
1222 if (columnConstraint.get(it->getColumn()) && (makeZeroColumns.size() == 0 || !makeZeroColumns.get(it->getColumn()))) {
1223 if (columnBitsSetBeforeIndex[it->getColumn()] == rowBitsSetBeforeIndex[index]) {
1224 insertedDiagonalElement = true;
1225 } else if (insertDiagonalEntries && !insertedDiagonalElement && columnBitsSetBeforeIndex[it->getColumn()] > rowBitsSetBeforeIndex[index]) {
1226 matrixBuilder.addNextValue(rowCount, rowGroupCount, storm::utility::zero<ValueType>());
1227 insertedDiagonalElement = true;
1228 }
1229 ++subEntries;
1230 matrixBuilder.addNextValue(rowCount, columnBitsSetBeforeIndex[it->getColumn()], it->getValue());
1231 }
1232 }
1233 if (insertDiagonalEntries && !insertedDiagonalElement && rowGroupCount < submatrixColumnCount) {
1234 matrixBuilder.addNextValue(rowCount, rowGroupCount, storm::utility::zero<ValueType>());
1235 }
1236 ++rowCount;
1237 }
1238 ++rowGroupCount;
1239 }
1240
1241 return matrixBuilder.build();
1242}
1243
1244template<typename ValueType>
1246 STORM_LOG_ASSERT(rowsToKeep.size() == this->getRowCount(), "Dimensions mismatch.");
1247
1248 // Count the number of entries of the resulting matrix
1249 index_type entryCount = 0;
1250 for (auto row : rowsToKeep) {
1251 entryCount += this->getRow(row).getNumberOfEntries();
1252 }
1253
1254 // Get the smallest row group index such that all row groups with at least this index are empty.
1255 index_type firstTrailingEmptyRowGroup = this->getRowGroupCount();
1256 for (auto groupIndexIt = this->getRowGroupIndices().rbegin() + 1; groupIndexIt != this->getRowGroupIndices().rend(); ++groupIndexIt) {
1257 if (rowsToKeep.getNextSetIndex(*groupIndexIt) != rowsToKeep.size()) {
1258 break;
1259 }
1260 --firstTrailingEmptyRowGroup;
1261 }
1262 STORM_LOG_THROW(allowEmptyRowGroups || firstTrailingEmptyRowGroup == this->getRowGroupCount(), storm::exceptions::InvalidArgumentException,
1263 "Empty rows are not allowed, but row group " << firstTrailingEmptyRowGroup << " is empty.");
1264
1265 // build the matrix. The row grouping will always be considered as nontrivial.
1266 SparseMatrixBuilder<ValueType> builder(rowsToKeep.getNumberOfSetBits(), this->getColumnCount(), entryCount, true, true, this->getRowGroupCount());
1267 index_type newRow = 0;
1268 for (index_type rowGroup = 0; rowGroup < firstTrailingEmptyRowGroup; ++rowGroup) {
1269 // Add a new row group
1270 builder.newRowGroup(newRow);
1271 bool rowGroupEmpty = true;
1272 for (index_type row = rowsToKeep.getNextSetIndex(this->getRowGroupIndices()[rowGroup]); row < this->getRowGroupIndices()[rowGroup + 1];
1273 row = rowsToKeep.getNextSetIndex(row + 1)) {
1274 rowGroupEmpty = false;
1275 for (auto const& entry : this->getRow(row)) {
1276 builder.addNextValue(newRow, entry.getColumn(), entry.getValue());
1277 }
1278 ++newRow;
1279 }
1280 STORM_LOG_THROW(allowEmptyRowGroups || !rowGroupEmpty, storm::exceptions::InvalidArgumentException,
1281 "Empty rows are not allowed, but row group " << rowGroup << " is empty.");
1282 }
1283
1284 // The all remaining row groups will be empty. Note that it is not allowed to call builder.addNewGroup(...) if there are no more rows afterwards.
1285 SparseMatrix<ValueType> res = builder.build();
1286 return res;
1287}
1288
1289template<typename ValueType>
1291 // Count the number of entries in the resulting matrix.
1292 index_type entryCount = 0;
1293 for (auto row : rowFilter) {
1294 entryCount += getRow(row).getNumberOfEntries();
1295 }
1296
1297 // Build the resulting matrix.
1299 for (auto row : rowFilter) {
1300 for (auto const& entry : getRow(row)) {
1301 builder.addNextValue(row, entry.getColumn(), entry.getValue());
1302 }
1303 }
1304 SparseMatrix<ValueType> result = builder.build();
1305
1306 // Add a row grouping if necessary.
1307 if (!hasTrivialRowGrouping()) {
1309 }
1310 return result;
1311}
1312
1313template<typename ValueType>
1318 for (index_type row = 0; row < getRowCount(); ++row) {
1319 for (auto const& entry : getRow(row)) {
1320 if (!storm::utility::isZero(entry.getValue())) {
1321 builder.addNextValue(row, entry.getColumn(), entry.getValue());
1322 }
1323 }
1324 }
1325 SparseMatrix<ValueType> result = builder.build();
1326 // Add a row grouping if necessary.
1327 if (!hasTrivialRowGrouping()) {
1329 }
1330 *this = std::move(result);
1331 }
1332}
1333
1334template<typename ValueType>
1335SparseMatrix<ValueType> SparseMatrix<ValueType>::selectRowsFromRowGroups(std::vector<index_type> const& rowGroupToRowIndexMapping,
1336 bool insertDiagonalEntries) const {
1337 // First, we need to count how many non-zero entries the resulting matrix will have and reserve space for
1338 // diagonal entries if requested.
1339 index_type subEntries = 0;
1340 for (index_type rowGroupIndex = 0, rowGroupIndexEnd = rowGroupToRowIndexMapping.size(); rowGroupIndex < rowGroupIndexEnd; ++rowGroupIndex) {
1341 // Determine which row we need to select from the current row group.
1342 STORM_LOG_ASSERT(rowGroupToRowIndexMapping[rowGroupIndex] < this->getRowGroupSize(rowGroupIndex),
1343 "Cannot point to row offset " << rowGroupToRowIndexMapping[rowGroupIndex] << " for rowGroup " << rowGroupIndex << " which starts at "
1344 << this->getRowGroupIndices()[rowGroupIndex] << " and ends at "
1345 << this->getRowGroupIndices()[rowGroupIndex + 1] << ".");
1346 index_type rowToCopy = this->getRowGroupIndices()[rowGroupIndex] + rowGroupToRowIndexMapping[rowGroupIndex];
1347
1348 // Iterate through that row and count the number of slots we have to reserve for copying.
1349 bool foundDiagonalElement = false;
1350 for (const_iterator it = this->begin(rowToCopy), ite = this->end(rowToCopy); it != ite; ++it) {
1351 if (it->getColumn() == rowGroupIndex) {
1352 foundDiagonalElement = true;
1353 }
1354 ++subEntries;
1355 }
1356 if (insertDiagonalEntries && !foundDiagonalElement) {
1357 ++subEntries;
1358 }
1359 }
1360
1361 // Now create the matrix to be returned with the appropriate size.
1362 SparseMatrixBuilder<ValueType> matrixBuilder(rowGroupIndices.get().size() - 1, columnCount, subEntries);
1363
1364 // Copy over the selected lines from the source matrix.
1365 for (index_type rowGroupIndex = 0, rowGroupIndexEnd = rowGroupToRowIndexMapping.size(); rowGroupIndex < rowGroupIndexEnd; ++rowGroupIndex) {
1366 // Determine which row we need to select from the current row group.
1367 index_type rowToCopy = this->getRowGroupIndices()[rowGroupIndex] + rowGroupToRowIndexMapping[rowGroupIndex];
1368
1369 // Iterate through that row and copy the entries. This also inserts a zero element on the diagonal if
1370 // there is no entry yet.
1371 bool insertedDiagonalElement = false;
1372 for (const_iterator it = this->begin(rowToCopy), ite = this->end(rowToCopy); it != ite; ++it) {
1373 if (it->getColumn() == rowGroupIndex) {
1374 insertedDiagonalElement = true;
1375 } else if (insertDiagonalEntries && !insertedDiagonalElement && it->getColumn() > rowGroupIndex) {
1376 matrixBuilder.addNextValue(rowGroupIndex, rowGroupIndex, storm::utility::zero<ValueType>());
1377 insertedDiagonalElement = true;
1378 }
1379 matrixBuilder.addNextValue(rowGroupIndex, it->getColumn(), it->getValue());
1380 }
1381 if (insertDiagonalEntries && !insertedDiagonalElement) {
1382 matrixBuilder.addNextValue(rowGroupIndex, rowGroupIndex, storm::utility::zero<ValueType>());
1383 }
1384 }
1385
1386 // Finalize created matrix and return result.
1387 return matrixBuilder.build();
1388}
1389
1390template<typename ValueType>
1392 bool insertDiagonalEntries) const {
1393 // First, we need to count how many non-zero entries the resulting matrix will have and reserve space for
1394 // diagonal entries if requested.
1395 index_type newEntries = 0;
1396 for (index_type row = 0, rowEnd = rowIndexSequence.size(); row < rowEnd; ++row) {
1397 bool foundDiagonalElement = false;
1398 for (const_iterator it = this->begin(rowIndexSequence[row]), ite = this->end(rowIndexSequence[row]); it != ite; ++it) {
1399 if (it->getColumn() == row) {
1400 foundDiagonalElement = true;
1401 }
1402 ++newEntries;
1403 }
1404 if (insertDiagonalEntries && !foundDiagonalElement) {
1405 ++newEntries;
1406 }
1407 }
1408
1409 // Now create the matrix to be returned with the appropriate size.
1410 SparseMatrixBuilder<ValueType> matrixBuilder(rowIndexSequence.size(), columnCount, newEntries);
1411
1412 // Copy over the selected rows from the source matrix.
1413 for (index_type row = 0, rowEnd = rowIndexSequence.size(); row < rowEnd; ++row) {
1414 bool insertedDiagonalElement = false;
1415 for (const_iterator it = this->begin(rowIndexSequence[row]), ite = this->end(rowIndexSequence[row]); it != ite; ++it) {
1416 if (it->getColumn() == row) {
1417 insertedDiagonalElement = true;
1418 } else if (insertDiagonalEntries && !insertedDiagonalElement && it->getColumn() > row) {
1419 matrixBuilder.addNextValue(row, row, storm::utility::zero<ValueType>());
1420 insertedDiagonalElement = true;
1421 }
1422 matrixBuilder.addNextValue(row, it->getColumn(), it->getValue());
1423 }
1424 if (insertDiagonalEntries && !insertedDiagonalElement) {
1425 matrixBuilder.addNextValue(row, row, storm::utility::zero<ValueType>());
1426 }
1427 }
1428
1429 // Finally create matrix and return result.
1430 return matrixBuilder.build();
1431}
1432
1433template<typename ValueType>
1434SparseMatrix<ValueType> SparseMatrix<ValueType>::permuteRows(std::vector<index_type> const& inversePermutation) const {
1435 // Now create the matrix to be returned with the appropriate size.
1436 // The entry size is only adequate if this is indeed a permutation.
1437 SparseMatrixBuilder<ValueType> matrixBuilder(inversePermutation.size(), columnCount, entryCount);
1438
1439 // Copy over the selected rows from the source matrix.
1440
1441 for (index_type writeTo = 0; writeTo < inversePermutation.size(); ++writeTo) {
1442 index_type const& readFrom = inversePermutation[writeTo];
1443 auto row = this->getRow(readFrom);
1444 for (auto const& entry : row) {
1445 matrixBuilder.addNextValue(writeTo, entry.getColumn(), entry.getValue());
1446 }
1447 }
1448 // Finally create matrix and return result.
1449 auto result = matrixBuilder.build();
1450 if (this->rowGroupIndices) {
1451 result.setRowGroupIndices(this->rowGroupIndices.get());
1452 }
1453 return result;
1454}
1455
1456template<typename ValueType>
1457SparseMatrix<ValueType> SparseMatrix<ValueType>::permuteRowGroupsAndColumns(std::vector<index_type> const& inverseRowGroupPermutation,
1458 std::vector<index_type> const& columnPermutation) const {
1459 STORM_LOG_ASSERT(storm::utility::permutation::isValidPermutation(inverseRowGroupPermutation), "Row group permutation is not a permutation.");
1460 STORM_LOG_ASSERT(storm::utility::permutation::isValidPermutation(columnPermutation), "Column permutation is not a permutation.");
1461 index_type const rowCount = getRowCount();
1463 auto oldGroupIt = inverseRowGroupPermutation.cbegin();
1464 index_type newRowIndex = 0;
1465 while (newRowIndex < rowCount) {
1466 if (!hasTrivialRowGrouping()) {
1467 matrixBuilder.newRowGroup(newRowIndex);
1468 }
1469 for (auto oldRowIndex : getRowGroupIndices(*oldGroupIt)) {
1470 for (auto const& oldEntry : getRow(oldRowIndex)) {
1471 matrixBuilder.addNextValue(newRowIndex, columnPermutation[oldEntry.getColumn()], oldEntry.getValue());
1472 }
1473 ++newRowIndex;
1474 }
1475 ++oldGroupIt;
1476 }
1477 return matrixBuilder.build();
1478}
1479
1480template<typename ValueType>
1481SparseMatrix<ValueType> SparseMatrix<ValueType>::transpose(bool joinGroups, bool keepZeros) const {
1482 index_type rowCount = this->getColumnCount();
1483 index_type columnCount = joinGroups ? this->getRowGroupCount() : this->getRowCount();
1484 index_type entryCount;
1485 if (keepZeros) {
1486 entryCount = this->getEntryCount();
1487 } else {
1489 entryCount = this->getNonzeroEntryCount();
1490 }
1491
1492 std::vector<index_type> rowIndications(rowCount + 1);
1493 std::vector<MatrixEntry<index_type, ValueType>> columnsAndValues(entryCount);
1494
1495 // First, we need to count how many entries each column has.
1496 for (index_type group = 0; group < columnCount; ++group) {
1497 for (auto const& transition : joinGroups ? this->getRowGroup(group) : this->getRow(group)) {
1498 if (transition.getValue() != storm::utility::zero<ValueType>() || keepZeros) {
1499 ++rowIndications[transition.getColumn() + 1];
1500 }
1501 }
1502 }
1503
1504 // Now compute the accumulated offsets.
1505 for (index_type i = 1; i < rowCount + 1; ++i) {
1506 rowIndications[i] = rowIndications[i - 1] + rowIndications[i];
1507 }
1508
1509 // Create an array that stores the index for the next value to be added for
1510 // each row in the transposed matrix. Initially this corresponds to the previously
1511 // computed accumulated offsets.
1512 std::vector<index_type> nextIndices = rowIndications;
1513
1514 // Now we are ready to actually fill in the values of the transposed matrix.
1515 for (index_type group = 0; group < columnCount; ++group) {
1516 for (auto const& transition : joinGroups ? this->getRowGroup(group) : this->getRow(group)) {
1517 if (transition.getValue() != storm::utility::zero<ValueType>() || keepZeros) {
1518 columnsAndValues[nextIndices[transition.getColumn()]] = std::make_pair(group, transition.getValue());
1519 nextIndices[transition.getColumn()]++;
1520 }
1521 }
1522 }
1523
1524 storm::storage::SparseMatrix<ValueType> transposedMatrix(columnCount, std::move(rowIndications), std::move(columnsAndValues), boost::none);
1525
1526 return transposedMatrix;
1527}
1528
1529template<typename ValueType>
1530SparseMatrix<ValueType> SparseMatrix<ValueType>::transposeSelectedRowsFromRowGroups(std::vector<uint64_t> const& rowGroupChoices, bool keepZeros) const {
1531 index_type rowCount = this->getColumnCount();
1532 index_type columnCount = this->getRowGroupCount();
1533
1534 // Get the overall entry count as well as the number of entries of each column
1535 index_type entryCount = 0;
1536 std::vector<index_type> rowIndications(columnCount + 1);
1537 auto rowGroupChoiceIt = rowGroupChoices.begin();
1538 for (index_type rowGroup = 0; rowGroup < columnCount; ++rowGroup, ++rowGroupChoiceIt) {
1539 for (auto const& entry : this->getRow(rowGroup, *rowGroupChoiceIt)) {
1540 if (keepZeros || !storm::utility::isZero(entry.getValue())) {
1541 ++entryCount;
1542 ++rowIndications[entry.getColumn() + 1];
1543 }
1544 }
1545 }
1546
1547 // Now compute the accumulated offsets.
1548 for (index_type i = 1; i < rowCount + 1; ++i) {
1549 rowIndications[i] = rowIndications[i - 1] + rowIndications[i];
1550 }
1551
1552 std::vector<MatrixEntry<index_type, ValueType>> columnsAndValues(entryCount);
1553
1554 // Create an array that stores the index for the next value to be added for
1555 // each row in the transposed matrix. Initially this corresponds to the previously
1556 // computed accumulated offsets.
1557 std::vector<index_type> nextIndices = rowIndications;
1558
1559 // Now we are ready to actually fill in the values of the transposed matrix.
1560 rowGroupChoiceIt = rowGroupChoices.begin();
1561 for (index_type rowGroup = 0; rowGroup < columnCount; ++rowGroup, ++rowGroupChoiceIt) {
1562 for (auto const& entry : this->getRow(rowGroup, *rowGroupChoiceIt)) {
1563 if (keepZeros || !storm::utility::isZero(entry.getValue())) {
1564 columnsAndValues[nextIndices[entry.getColumn()]] = std::make_pair(rowGroup, entry.getValue());
1565 ++nextIndices[entry.getColumn()];
1566 }
1567 }
1568 }
1569
1570 return storm::storage::SparseMatrix<ValueType>(std::move(columnCount), std::move(rowIndications), std::move(columnsAndValues), boost::none);
1571}
1572
1573template<typename ValueType>
1578
1579template<typename ValueType>
1581 // Now iterate over all row groups and set the diagonal elements to the inverted value.
1582 // If there is a row without the diagonal element, an exception is thrown.
1583 ValueType one = storm::utility::one<ValueType>();
1584 ValueType zero = storm::utility::zero<ValueType>();
1585 bool foundDiagonalElement = false;
1586 for (index_type group = 0; group < this->getRowGroupCount(); ++group) {
1587 for (auto& entry : this->getRowGroup(group)) {
1588 if (entry.getColumn() == group) {
1589 if (entry.getValue() == one) {
1590 --this->nonzeroEntryCount;
1591 entry.setValue(zero);
1592 } else if (entry.getValue() == zero) {
1593 ++this->nonzeroEntryCount;
1594 entry.setValue(one);
1595 } else {
1596 entry.setValue(one - entry.getValue());
1597 }
1598 foundDiagonalElement = true;
1599 }
1600 }
1601
1602 // Throw an exception if a row did not have an element on the diagonal.
1603 if (!foundDiagonalElement) {
1604 throw storm::exceptions::InvalidArgumentException() << "Illegal call to SparseMatrix::invertDiagonal: matrix is missing diagonal entries.";
1605 }
1606 }
1607}
1608
1609template<typename ValueType>
1611 // Iterate over all row groups and negate all the elements that are not on the diagonal.
1612 for (index_type group = 0; group < this->getRowGroupCount(); ++group) {
1613 for (auto& entry : this->getRowGroup(group)) {
1614 if (entry.getColumn() != group) {
1615 entry.setValue(-entry.getValue());
1616 }
1617 }
1618 }
1619}
1620
1621template<typename ValueType>
1623 // Iterate over all rows and negate all the elements that are not on the diagonal.
1624 for (index_type group = 0; group < this->getRowGroupCount(); ++group) {
1625 for (auto& entry : this->getRowGroup(group)) {
1626 if (entry.getColumn() == group) {
1627 --this->nonzeroEntryCount;
1628 entry.setValue(storm::utility::zero<ValueType>());
1629 }
1630 }
1631 }
1632 if (dropZeroEntries) {
1633 this->dropZeroEntries();
1634 }
1635}
1636
1637template<typename ValueType>
1638typename std::pair<storm::storage::SparseMatrix<ValueType>, std::vector<ValueType>> SparseMatrix<ValueType>::getJacobiDecomposition() const {
1639 STORM_LOG_THROW(this->getRowCount() == this->getColumnCount(), storm::exceptions::InvalidArgumentException,
1640 "Canno compute Jacobi decomposition of non-square matrix.");
1641
1642 // Prepare the resulting data structures.
1643 SparseMatrixBuilder<ValueType> luBuilder(this->getRowCount(), this->getColumnCount());
1644 std::vector<ValueType> invertedDiagonal(rowCount);
1645
1646 // Copy entries to the appropriate matrices.
1647 for (index_type rowNumber = 0; rowNumber < rowCount; ++rowNumber) {
1648 for (const_iterator it = this->begin(rowNumber), ite = this->end(rowNumber); it != ite; ++it) {
1649 if (it->getColumn() == rowNumber) {
1650 invertedDiagonal[rowNumber] = storm::utility::one<ValueType>() / it->getValue();
1651 } else {
1652 luBuilder.addNextValue(rowNumber, it->getColumn(), it->getValue());
1653 }
1654 }
1655 }
1656
1657 return std::make_pair(luBuilder.build(), std::move(invertedDiagonal));
1658}
1659
1660template<>
1661typename std::pair<storm::storage::SparseMatrix<Interval>, std::vector<Interval>> SparseMatrix<Interval>::getJacobiDecomposition() const {
1662 STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This operation is not supported.");
1663}
1664
1665template<>
1666typename std::pair<storm::storage::SparseMatrix<RationalFunction>, std::vector<RationalFunction>> SparseMatrix<RationalFunction>::getJacobiDecomposition()
1667 const {
1668 STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This operation is not supported.");
1669}
1670
1671template<typename ValueType>
1672template<typename OtherValueType, typename ResultValueType>
1674 index_type const& row) const {
1679
1680 ResultValueType result = storm::utility::zero<ResultValueType>();
1681 for (; it1 != ite1 && it2 != ite2; ++it1) {
1682 if (it1->getColumn() < it2->getColumn()) {
1683 continue;
1684 } else {
1685 // If the precondition of this method (i.e. that the given matrix is a submatrix
1686 // of the current one) was fulfilled, we know now that the two elements are in
1687 // the same column, so we can multiply and add them to the row sum vector.
1688 STORM_LOG_ASSERT(it1->getColumn() == it2->getColumn(), "The given matrix is not a submatrix of this one.");
1689 result += it2->getValue() * OtherValueType(it1->getValue());
1690 ++it2;
1691 }
1692 }
1693 return result;
1694}
1695
1696template<typename ValueType>
1697template<typename OtherValueType, typename ResultValueType>
1699 std::vector<ResultValueType> result;
1700 result.reserve(rowCount);
1701 for (index_type row = 0; row < rowCount && row < otherMatrix.getRowCount(); ++row) {
1702 result.push_back(getPointwiseProductRowSum<OtherValueType, ResultValueType>(otherMatrix, row));
1703 }
1704 return result;
1705}
1706
1707template<typename ValueType>
1708void SparseMatrix<ValueType>::multiplyWithVector(std::vector<ValueType> const& vector, std::vector<ValueType>& result,
1709 std::vector<value_type> const* summand) const {
1710 // If the vector and the result are aliases and this is not set to be allowed, we need and temporary vector.
1711 std::vector<ValueType>* target;
1712 std::vector<ValueType> temporary;
1713 if (&vector == &result) {
1714 STORM_LOG_WARN("Vectors are aliased. Using temporary, which is potentially slow.");
1715 temporary = std::vector<ValueType>(vector.size());
1716 target = &temporary;
1717 } else {
1718 target = &result;
1719 }
1720
1721 this->multiplyWithVectorForward(vector, *target, summand);
1722
1723 if (target == &temporary) {
1724 std::swap(result, *target);
1725 }
1726}
1727
1728template<typename ValueType>
1729void SparseMatrix<ValueType>::multiplyWithVectorForward(std::vector<ValueType> const& vector, std::vector<ValueType>& result,
1730 std::vector<value_type> const* summand) const {
1731 const_iterator it = this->begin();
1732 const_iterator ite;
1733 std::vector<index_type>::const_iterator rowIterator = rowIndications.begin();
1734 typename std::vector<ValueType>::iterator resultIterator = result.begin();
1735 typename std::vector<ValueType>::iterator resultIteratorEnd = result.end();
1736 typename std::vector<ValueType>::const_iterator summandIterator;
1737 if (summand) {
1738 summandIterator = summand->begin();
1739 }
1740
1741 for (; resultIterator != resultIteratorEnd; ++rowIterator, ++resultIterator, ++summandIterator) {
1742 ValueType newValue;
1743 if (summand) {
1744 newValue = *summandIterator;
1745 } else {
1746 newValue = storm::utility::zero<ValueType>();
1747 }
1748
1749 for (ite = this->begin() + *(rowIterator + 1); it != ite; ++it) {
1750 newValue += it->getValue() * vector[it->getColumn()];
1751 }
1752
1753 *resultIterator = newValue;
1754 }
1755}
1756
1757template<typename ValueType>
1758void SparseMatrix<ValueType>::multiplyWithVectorBackward(std::vector<ValueType> const& vector, std::vector<ValueType>& result,
1759 std::vector<value_type> const* summand) const {
1760 const_iterator it = this->end() - 1;
1761 const_iterator ite;
1762 std::vector<index_type>::const_iterator rowIterator = rowIndications.end() - 2;
1763 typename std::vector<ValueType>::iterator resultIterator = result.end() - 1;
1764 typename std::vector<ValueType>::iterator resultIteratorEnd = result.begin() - 1;
1765 typename std::vector<ValueType>::const_iterator summandIterator;
1766 if (summand) {
1767 summandIterator = summand->end() - 1;
1768 }
1769
1770 for (; resultIterator != resultIteratorEnd; --rowIterator, --resultIterator, --summandIterator) {
1771 ValueType newValue;
1772 if (summand) {
1773 newValue = *summandIterator;
1774 } else {
1775 newValue = storm::utility::zero<ValueType>();
1776 }
1777
1778 for (ite = this->begin() + *rowIterator - 1; it != ite; --it) {
1779 newValue += (it->getValue() * vector[it->getColumn()]);
1780 }
1781
1782 *resultIterator = newValue;
1783 }
1784}
1785
1786template<typename ValueType>
1787ValueType SparseMatrix<ValueType>::multiplyRowWithVector(index_type row, std::vector<ValueType> const& vector) const {
1788 ValueType result = storm::utility::zero<ValueType>();
1789
1790 for (auto const& entry : this->getRow(row)) {
1791 result += entry.getValue() * vector[entry.getColumn()];
1792 }
1793 return result;
1794}
1795
1796template<typename ValueType>
1797void SparseMatrix<ValueType>::performSuccessiveOverRelaxationStep(ValueType omega, std::vector<ValueType>& x, std::vector<ValueType> const& b) const {
1798 const_iterator it = this->end() - 1;
1799 const_iterator ite;
1800 std::vector<index_type>::const_iterator rowIterator = rowIndications.end() - 2;
1801 typename std::vector<ValueType>::const_iterator bIt = b.end() - 1;
1802 typename std::vector<ValueType>::iterator resultIterator = x.end() - 1;
1803 typename std::vector<ValueType>::iterator resultIteratorEnd = x.begin() - 1;
1804
1805 index_type currentRow = getRowCount();
1806 for (; resultIterator != resultIteratorEnd; --rowIterator, --resultIterator, --bIt) {
1807 --currentRow;
1808 ValueType tmpValue = storm::utility::zero<ValueType>();
1809 ValueType diagonalElement = storm::utility::zero<ValueType>();
1810
1811 for (ite = this->begin() + *rowIterator - 1; it != ite; --it) {
1812 if (it->getColumn() != currentRow) {
1813 tmpValue += it->getValue() * x[it->getColumn()];
1814 } else {
1815 diagonalElement += it->getValue();
1816 }
1817 }
1818 assert(!storm::utility::isZero(diagonalElement));
1819 *resultIterator = ((storm::utility::one<ValueType>() - omega) * *resultIterator) + (omega / diagonalElement) * (*bIt - tmpValue);
1820 }
1821}
1822
1823template<>
1824void SparseMatrix<Interval>::performSuccessiveOverRelaxationStep(Interval, std::vector<Interval>&, std::vector<Interval> const&) const {
1825 STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "This operation is not supported.");
1826}
1827
1828template<typename ValueType>
1829void SparseMatrix<ValueType>::performWalkerChaeStep(std::vector<ValueType> const& x, std::vector<ValueType> const& columnSums, std::vector<ValueType> const& b,
1830 std::vector<ValueType> const& ax, std::vector<ValueType>& result) const {
1831 const_iterator it = this->begin();
1832 const_iterator ite;
1833 std::vector<index_type>::const_iterator rowIterator = rowIndications.begin();
1834
1835 // Clear all previous entries.
1836 ValueType zero = storm::utility::zero<ValueType>();
1837 for (auto& entry : result) {
1838 entry = zero;
1839 }
1840
1841 for (index_type row = 0; row < rowCount; ++row, ++rowIterator) {
1842 for (ite = this->begin() + *(rowIterator + 1); it != ite; ++it) {
1843 result[it->getColumn()] += it->getValue() * (b[row] / ax[row]);
1844 }
1845 }
1846
1847 auto xIterator = x.begin();
1848 auto sumsIterator = columnSums.begin();
1849 for (auto& entry : result) {
1850 entry *= *xIterator / *sumsIterator;
1851 ++xIterator;
1852 ++sumsIterator;
1853 }
1854}
1855
1856template<>
1857void SparseMatrix<Interval>::performWalkerChaeStep(std::vector<Interval> const& x, std::vector<Interval> const& rowSums, std::vector<Interval> const& b,
1858 std::vector<Interval> const& ax, std::vector<Interval>& result) const {
1859 STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "This operation is not supported.");
1860}
1861
1862template<typename ValueType>
1863void SparseMatrix<ValueType>::multiplyAndReduceForward(OptimizationDirection const& dir, std::vector<uint64_t> const& rowGroupIndices,
1864 std::vector<ValueType> const& vector, std::vector<ValueType> const* summand,
1865 std::vector<ValueType>& result, std::vector<uint64_t>* choices) const {
1866 if (dir == OptimizationDirection::Minimize) {
1867 multiplyAndReduceForward<storm::utility::ElementLess<ValueType>>(rowGroupIndices, vector, summand, result, choices);
1868 } else {
1869 multiplyAndReduceForward<storm::utility::ElementGreater<ValueType>>(rowGroupIndices, vector, summand, result, choices);
1870 }
1871}
1872
1873template<typename ValueType>
1874template<typename Compare>
1875void SparseMatrix<ValueType>::multiplyAndReduceForward(std::vector<uint64_t> const& rowGroupIndices, std::vector<ValueType> const& vector,
1876 std::vector<ValueType> const* summand, std::vector<ValueType>& result,
1877 std::vector<uint64_t>* choices) const {
1878 Compare compare;
1879 auto elementIt = this->begin();
1880 auto rowGroupIt = rowGroupIndices.begin();
1881 auto rowIt = rowIndications.begin();
1882 typename std::vector<ValueType>::const_iterator summandIt;
1883 if (summand) {
1884 summandIt = summand->begin();
1885 }
1886 typename std::vector<uint64_t>::iterator choiceIt;
1887 if (choices) {
1888 choiceIt = choices->begin();
1889 }
1890
1891 // Variables for correctly tracking choices (only update if new choice is strictly better).
1892 ValueType oldSelectedChoiceValue;
1893 uint64_t selectedChoice;
1894
1895 uint64_t currentRow = 0;
1896 for (auto resultIt = result.begin(), resultIte = result.end(); resultIt != resultIte; ++resultIt, ++choiceIt, ++rowGroupIt) {
1897 ValueType currentValue = storm::utility::zero<ValueType>();
1898
1899 // Only multiply and reduce if there is at least one row in the group.
1900 if (*rowGroupIt < *(rowGroupIt + 1)) {
1901 if (summand) {
1902 currentValue = *summandIt;
1903 ++summandIt;
1904 }
1905
1906 for (auto elementIte = this->begin() + *(rowIt + 1); elementIt != elementIte; ++elementIt) {
1907 currentValue += elementIt->getValue() * vector[elementIt->getColumn()];
1908 }
1909
1910 if (choices) {
1911 selectedChoice = 0;
1912 if (*choiceIt == 0) {
1913 oldSelectedChoiceValue = currentValue;
1914 }
1915 }
1916
1917 ++rowIt;
1918 ++currentRow;
1919
1920 for (; currentRow < *(rowGroupIt + 1); ++rowIt, ++currentRow) {
1921 ValueType newValue = summand ? *summandIt : storm::utility::zero<ValueType>();
1922 for (auto elementIte = this->begin() + *(rowIt + 1); elementIt != elementIte; ++elementIt) {
1923 newValue += elementIt->getValue() * vector[elementIt->getColumn()];
1924 }
1925
1926 if (choices && currentRow == *choiceIt + *rowGroupIt) {
1927 oldSelectedChoiceValue = newValue;
1928 }
1929
1930 if (compare(newValue, currentValue)) {
1931 currentValue = newValue;
1932 if (choices) {
1933 selectedChoice = currentRow - *rowGroupIt;
1934 }
1935 }
1936 if (summand) {
1937 ++summandIt;
1938 }
1939 }
1940
1941 // Finally write value to target vector.
1942 *resultIt = currentValue;
1943 if (choices && compare(currentValue, oldSelectedChoiceValue)) {
1944 *choiceIt = selectedChoice;
1945 }
1946 }
1947 }
1948}
1949
1950template<>
1951void SparseMatrix<storm::RationalFunction>::multiplyAndReduceForward(OptimizationDirection const& dir, std::vector<uint64_t> const& rowGroupIndices,
1952 std::vector<storm::RationalFunction> const& vector,
1953 std::vector<storm::RationalFunction> const* b,
1954 std::vector<storm::RationalFunction>& result, std::vector<uint64_t>* choices) const {
1955 STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "This operation is not supported.");
1956}
1957
1958template<typename ValueType>
1959void SparseMatrix<ValueType>::multiplyAndReduceBackward(OptimizationDirection const& dir, std::vector<uint64_t> const& rowGroupIndices,
1960 std::vector<ValueType> const& vector, std::vector<ValueType> const* summand,
1961 std::vector<ValueType>& result, std::vector<uint64_t>* choices) const {
1962 if (dir == storm::OptimizationDirection::Minimize) {
1963 multiplyAndReduceBackward<storm::utility::ElementLess<ValueType>>(rowGroupIndices, vector, summand, result, choices);
1964 } else {
1965 multiplyAndReduceBackward<storm::utility::ElementGreater<ValueType>>(rowGroupIndices, vector, summand, result, choices);
1966 }
1967}
1968
1969template<typename ValueType>
1970template<typename Compare>
1971void SparseMatrix<ValueType>::multiplyAndReduceBackward(std::vector<uint64_t> const& rowGroupIndices, std::vector<ValueType> const& vector,
1972 std::vector<ValueType> const* summand, std::vector<ValueType>& result,
1973 std::vector<uint64_t>* choices) const {
1974 Compare compare;
1975 auto elementIt = this->end() - 1;
1976 auto rowGroupIt = rowGroupIndices.end() - 2;
1977 auto rowIt = rowIndications.end() - 2;
1978 typename std::vector<ValueType>::const_iterator summandIt;
1979 if (summand) {
1980 summandIt = summand->end() - 1;
1981 }
1982 typename std::vector<uint64_t>::iterator choiceIt;
1983 if (choices) {
1984 choiceIt = choices->end() - 1;
1985 }
1986
1987 // Variables for correctly tracking choices (only update if new choice is strictly better).
1988 ValueType oldSelectedChoiceValue;
1989 uint64_t selectedChoice;
1990
1991 uint64_t currentRow = this->getRowCount() - 1;
1992 for (auto resultIt = result.end() - 1, resultIte = result.begin() - 1; resultIt != resultIte; --resultIt, --choiceIt, --rowGroupIt) {
1993 ValueType currentValue = storm::utility::zero<ValueType>();
1994
1995 // Only multiply and reduce if there is at least one row in the group.
1996 if (*rowGroupIt < *(rowGroupIt + 1)) {
1997 if (summand) {
1998 currentValue = *summandIt;
1999 --summandIt;
2000 }
2001
2002 for (auto elementIte = this->begin() + *rowIt - 1; elementIt != elementIte; --elementIt) {
2003 currentValue += elementIt->getValue() * vector[elementIt->getColumn()];
2004 }
2005 if (choices) {
2006 selectedChoice = currentRow - *rowGroupIt;
2007 if (*choiceIt == selectedChoice) {
2008 oldSelectedChoiceValue = currentValue;
2009 }
2010 }
2011 --rowIt;
2012 --currentRow;
2013
2014 for (uint64_t i = *rowGroupIt + 1, end = *(rowGroupIt + 1); i < end; --rowIt, --currentRow, ++i, --summandIt) {
2015 ValueType newValue = summand ? *summandIt : storm::utility::zero<ValueType>();
2016 for (auto elementIte = this->begin() + *rowIt - 1; elementIt != elementIte; --elementIt) {
2017 newValue += elementIt->getValue() * vector[elementIt->getColumn()];
2018 }
2019
2020 if (choices && currentRow == *choiceIt + *rowGroupIt) {
2021 oldSelectedChoiceValue = newValue;
2022 }
2023
2024 if (compare(newValue, currentValue)) {
2025 currentValue = newValue;
2026 if (choices) {
2027 selectedChoice = currentRow - *rowGroupIt;
2028 }
2029 }
2030 }
2031
2032 // Finally write value to target vector.
2033 *resultIt = currentValue;
2034 if (choices && compare(currentValue, oldSelectedChoiceValue)) {
2035 *choiceIt = selectedChoice;
2036 }
2037 }
2038 }
2039}
2040
2041template<>
2042void SparseMatrix<storm::RationalFunction>::multiplyAndReduceBackward(OptimizationDirection const& dir, std::vector<uint64_t> const& rowGroupIndices,
2043 std::vector<storm::RationalFunction> const& vector,
2044 std::vector<storm::RationalFunction> const* b,
2045 std::vector<storm::RationalFunction>& result, std::vector<uint64_t>* choices) const {
2046 STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "This operation is not supported.");
2047}
2048
2049template<typename ValueType>
2050void SparseMatrix<ValueType>::multiplyAndReduce(OptimizationDirection const& dir, std::vector<uint64_t> const& rowGroupIndices,
2051 std::vector<ValueType> const& vector, std::vector<ValueType> const* summand, std::vector<ValueType>& result,
2052 std::vector<uint64_t>* choices) const {
2053 // If the vector and the result are aliases, we need and temporary vector.
2054 std::vector<ValueType>* target;
2055 std::vector<ValueType> temporary;
2056 if (&vector == &result) {
2057 STORM_LOG_WARN("Vectors are aliased but are not allowed to be. Using temporary, which is potentially slow.");
2058 temporary = std::vector<ValueType>(vector.size());
2059 target = &temporary;
2060 } else {
2061 target = &result;
2062 }
2063
2064 this->multiplyAndReduceForward(dir, rowGroupIndices, vector, summand, *target, choices);
2065
2066 if (target == &temporary) {
2067 std::swap(temporary, result);
2068 }
2069}
2070
2071template<typename ValueType>
2072void SparseMatrix<ValueType>::multiplyVectorWithMatrix(std::vector<value_type> const& vector, std::vector<value_type>& result) const {
2073 const_iterator it = this->begin();
2074 const_iterator ite;
2075 std::vector<index_type>::const_iterator rowIterator = rowIndications.begin();
2076 std::vector<index_type>::const_iterator rowIteratorEnd = rowIndications.end();
2077
2078 index_type currentRow = 0;
2079 for (; rowIterator != rowIteratorEnd - 1; ++rowIterator) {
2080 for (ite = this->begin() + *(rowIterator + 1); it != ite; ++it) {
2081 result[it->getColumn()] += it->getValue() * vector[currentRow];
2082 }
2083 ++currentRow;
2084 }
2085}
2086
2087template<typename ValueType>
2088void SparseMatrix<ValueType>::scaleRowsInPlace(std::vector<ValueType> const& factors) {
2089 STORM_LOG_ASSERT(factors.size() == this->getRowCount(), "Can not scale rows: Number of rows and number of scaling factors do not match.");
2090 index_type row = 0;
2091 for (auto const& factor : factors) {
2092 for (auto& entry : getRow(row)) {
2093 entry.setValue(entry.getValue() * factor);
2094 }
2095 ++row;
2096 }
2097}
2098
2099template<typename ValueType>
2100void SparseMatrix<ValueType>::divideRowsInPlace(std::vector<ValueType> const& divisors) {
2101 STORM_LOG_ASSERT(divisors.size() == this->getRowCount(), "Can not divide rows: Number of rows and number of divisors do not match.");
2102 index_type row = 0;
2103 for (auto const& divisor : divisors) {
2104 STORM_LOG_ASSERT(!storm::utility::isZero(divisor), "Can not divide row " << row << " by 0.");
2105 for (auto& entry : getRow(row)) {
2106 entry.setValue(entry.getValue() / divisor);
2107 }
2108 ++row;
2109 }
2110}
2111
2112template<>
2113void SparseMatrix<Interval>::divideRowsInPlace(std::vector<Interval> const&) {
2114 STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This operation is not supported.");
2115}
2116
2117template<typename ValueType>
2119 return const_rows(this->columnsAndValues.begin() + this->rowIndications[startRow], this->rowIndications[endRow] - this->rowIndications[startRow]);
2120}
2121
2122template<typename ValueType>
2124 return rows(this->columnsAndValues.begin() + this->rowIndications[startRow], this->rowIndications[endRow] - this->rowIndications[startRow]);
2125}
2126
2127template<typename ValueType>
2129 return getRows(row, row + 1);
2130}
2131
2132template<typename ValueType>
2136
2137template<typename ValueType>
2139 STORM_LOG_ASSERT(rowGroup < this->getRowGroupCount(), "Row group is out-of-bounds.");
2140 STORM_LOG_ASSERT(offset < this->getRowGroupSize(rowGroup), "Row offset in row-group is out-of-bounds.");
2141 if (!this->hasTrivialRowGrouping()) {
2142 return getRow(this->getRowGroupIndices()[rowGroup] + offset);
2143 } else {
2144 return getRow(this->getRowGroupIndices()[rowGroup] + offset);
2145 }
2146}
2147
2148template<typename ValueType>
2150 STORM_LOG_ASSERT(rowGroup < this->getRowGroupCount(), "Row group is out-of-bounds.");
2151 STORM_LOG_ASSERT(offset < this->getRowGroupSize(rowGroup), "Row offset in row-group is out-of-bounds.");
2152 if (!this->hasTrivialRowGrouping()) {
2153 return getRow(this->getRowGroupIndices()[rowGroup] + offset);
2154 } else {
2155 STORM_LOG_ASSERT(offset == 0, "Invalid offset.");
2156 return getRow(rowGroup + offset);
2157 }
2158}
2159
2160template<typename ValueType>
2162 STORM_LOG_ASSERT(rowGroup < this->getRowGroupCount(), "Row group is out-of-bounds.");
2163 if (!this->hasTrivialRowGrouping()) {
2164 return getRows(this->getRowGroupIndices()[rowGroup], this->getRowGroupIndices()[rowGroup + 1]);
2165 } else {
2166 return getRows(rowGroup, rowGroup + 1);
2167 }
2168}
2169
2170template<typename ValueType>
2172 STORM_LOG_ASSERT(rowGroup < this->getRowGroupCount(), "Row group is out-of-bounds.");
2173 if (!this->hasTrivialRowGrouping()) {
2174 return getRows(this->getRowGroupIndices()[rowGroup], this->getRowGroupIndices()[rowGroup + 1]);
2175 } else {
2176 return getRows(rowGroup, rowGroup + 1);
2177 }
2178}
2179
2180template<typename ValueType>
2182 STORM_LOG_ASSERT(row < this->getRowCount(), "Row " << row << " exceeds row count " << this->getRowCount() << ".");
2183 return this->columnsAndValues.begin() + this->rowIndications[row];
2184}
2185
2186template<typename ValueType>
2188 STORM_LOG_ASSERT(row < this->getRowCount(), "Row " << row << " exceeds row count " << this->getRowCount() << ".");
2189 return this->columnsAndValues.begin() + this->rowIndications[row];
2190}
2191
2192template<typename ValueType>
2194 return this->columnsAndValues.begin();
2195}
2196
2197template<typename ValueType>
2199 return this->columnsAndValues.begin();
2200}
2201
2202template<typename ValueType>
2204 STORM_LOG_ASSERT(row < this->getRowCount(), "Row " << row << " exceeds row count " << this->getRowCount() << ".");
2205 return this->columnsAndValues.begin() + this->rowIndications[row + 1];
2206}
2207
2208template<typename ValueType>
2210 STORM_LOG_ASSERT(row < this->getRowCount(), "Row " << row << " exceeds row count " << this->getRowCount() << ".");
2211 return this->columnsAndValues.begin() + this->rowIndications[row + 1];
2212}
2213
2214template<typename ValueType>
2216 return this->columnsAndValues.begin() + this->rowIndications[rowCount];
2217}
2218
2219template<typename ValueType>
2221 return this->columnsAndValues.begin() + this->rowIndications[rowCount];
2222}
2223
2224template<typename ValueType>
2226 ValueType sum = storm::utility::zero<ValueType>();
2227 for (const_iterator it = this->begin(row), ite = this->end(row); it != ite; ++it) {
2228 sum += it->getValue();
2229 }
2230 return sum;
2231}
2232
2233template<typename ValueType>
2235 index_type nonConstEntries = 0;
2236 for (auto const& entry : *this) {
2237 if (!storm::utility::isConstant(entry.getValue())) {
2238 ++nonConstEntries;
2239 }
2240 }
2241 return nonConstEntries;
2242}
2243
2244template<typename ValueType>
2246 index_type nonConstRowGroups = 0;
2247 for (index_type rowGroup = 0; rowGroup < this->getRowGroupCount(); ++rowGroup) {
2248 for (auto const& entry : this->getRowGroup(rowGroup)) {
2249 if (!storm::utility::isConstant(entry.getValue())) {
2250 ++nonConstRowGroups;
2251 break;
2252 }
2253 }
2254 }
2255 return nonConstRowGroups;
2256}
2257
2258template<typename ValueType>
2260 using BaseType =
2261 std::conditional_t<std::is_same_v<ValueType, storm::RationalFunction>, storm::RationalFunctionCoefficient, storm::IntervalBaseType<ValueType>>;
2262 auto toBaseType = [](ValueType const& value) {
2263 if constexpr (std::is_same_v<ValueType, BaseType>) {
2264 return value;
2265 } else {
2266 return storm::utility::convertNumber<BaseType>(value);
2267 }
2268 };
2269 STORM_LOG_ASSERT(storm::utility::isConstant(tolerance), "Expected constant tolerance. Got " << tolerance);
2270 BaseType const zeroMinusTolerance = storm::utility::zero<BaseType>() - toBaseType(tolerance);
2271 BaseType const onePlusTolerance = storm::utility::one<BaseType>() + toBaseType(tolerance);
2272 BaseType const oneMinusTolerance = storm::utility::one<BaseType>() - toBaseType(tolerance);
2273
2274 auto isContained = [&toBaseType](ValueType const& value, BaseType const& lower, BaseType const& upper) {
2275 // surpress unused lambda capture warning for toBaseType in case it is not needed for the given ValueType.
2276 (void)toBaseType;
2277 if constexpr (storm::IsIntervalType<ValueType>) {
2278 // check if the interval contains some value in [lower,upper]
2279 return value.lower() <= upper && value.upper() >= lower;
2280 } else if constexpr (std::is_same_v<ValueType, storm::RationalFunction>) {
2281 // for rational functions, we only perform a check if the value is constant.
2282 if (storm::utility::isConstant(value)) {
2283 auto const constValue = toBaseType(value);
2284 return constValue <= upper && constValue >= lower;
2285 }
2286 return true;
2287 } else {
2288 // in all other cases, we expect the value to be constant
2289 STORM_LOG_ASSERT(storm::utility::isConstant(value), "Expected constant value. Got " << value);
2290 return value <= upper && value >= lower;
2291 }
2292 };
2293
2294 auto toString = [](ValueType const& value) {
2295 std::stringstream s;
2296 s << value;
2297 return s.str();
2298 };
2299
2300 for (index_type row = 0; row < this->rowCount; ++row) {
2301 auto rowSum = storm::utility::zero<ValueType>();
2302 for (auto const& entry : getRow(row)) {
2303 if (!isContained(entry.getValue(), zeroMinusTolerance, onePlusTolerance)) {
2304 if (reason) {
2305 *reason = "Entry in row " + std::to_string(row) + " is not a probability: " + toString(entry.getValue());
2306 }
2307 return false;
2308 }
2309 rowSum += entry.getValue();
2310 }
2311 if (!isContained(rowSum, oneMinusTolerance, onePlusTolerance)) {
2312 if (reason) {
2313 // print sum-1 to ensure that the reason is informative even if the sum is very close to one.
2314 *reason = "Sum of entries in row " + std::to_string(row) + " is not one: sum-1=" + toString(rowSum - storm::utility::one<ValueType>());
2315 }
2316 return false;
2317 }
2318 }
2319 return true;
2320}
2321
2322template<typename ValueType>
2324 for (auto const& entry : *this) {
2325 if (!storm::utility::isPositive(entry.getValue())) {
2326 return false;
2327 }
2328 }
2329 return true;
2330}
2331
2332template<typename ValueType>
2333template<typename OtherValueType>
2335 // Check for matching sizes.
2336 if (this->getRowCount() != matrix.getRowCount())
2337 return false;
2338 if (this->getColumnCount() != matrix.getColumnCount())
2339 return false;
2340 if (this->hasTrivialRowGrouping() && !matrix.hasTrivialRowGrouping())
2341 return false;
2342 if (!this->hasTrivialRowGrouping() && matrix.hasTrivialRowGrouping())
2343 return false;
2344 if (!this->hasTrivialRowGrouping() && !matrix.hasTrivialRowGrouping() && this->getRowGroupIndices() != matrix.getRowGroupIndices())
2345 return false;
2346 if (this->getRowGroupIndices() != matrix.getRowGroupIndices())
2347 return false;
2348
2349 // Check the subset property for all rows individually.
2350 for (index_type row = 0; row < this->getRowCount(); ++row) {
2351 auto it2 = matrix.begin(row);
2352 auto ite2 = matrix.end(row);
2353 for (const_iterator it1 = this->begin(row), ite1 = this->end(row); it1 != ite1; ++it1) {
2354 // Skip over all entries of the other matrix that are before the current entry in the current matrix.
2355 while (it2 != ite2 && it2->getColumn() < it1->getColumn()) {
2356 ++it2;
2357 }
2358 if (it2 == ite2 || it1->getColumn() != it2->getColumn()) {
2359 return false;
2360 }
2361 }
2362 }
2363 return true;
2364}
2365
2366template<typename ValueType>
2368 if (this->getRowCount() != this->getColumnCount()) {
2369 return false;
2370 }
2371 if (this->getNonzeroEntryCount() != this->getRowCount()) {
2372 return false;
2373 }
2374 for (uint64_t row = 0; row < this->getRowCount(); ++row) {
2375 bool rowHasEntry = false;
2376 for (auto const& entry : this->getRow(row)) {
2377 if (entry.getColumn() == row) {
2378 if (!storm::utility::isOne(entry.getValue())) {
2379 return false;
2380 }
2381 rowHasEntry = true;
2382 } else {
2383 if (!storm::utility::isZero(entry.getValue())) {
2384 return false;
2385 }
2386 }
2387 }
2388 if (!rowHasEntry) {
2389 return false;
2390 }
2391 }
2392 return true;
2393}
2394
2395template<typename ValueType>
2397 std::string result =
2398 std::to_string(getRowCount()) + "x" + std::to_string(getColumnCount()) + " matrix (" + std::to_string(getNonzeroEntryCount()) + " non-zeroes";
2399 if (!hasTrivialRowGrouping()) {
2400 result += ", " + std::to_string(getRowGroupCount()) + " groups";
2401 }
2402 result += ")";
2403 return result;
2404}
2405
2406template<typename ValueType>
2407std::ostream& operator<<(std::ostream& out, SparseMatrix<ValueType> const& matrix) {
2408 // Print column numbers in header.
2409 out << "\t\t";
2410 for (typename SparseMatrix<ValueType>::index_type i = 0; i < matrix.getColumnCount(); ++i) {
2411 out << i << "\t";
2412 }
2413 out << '\n';
2414
2415 // Iterate over all row groups.
2416 for (typename SparseMatrix<ValueType>::index_type group = 0; group < matrix.getRowGroupCount(); ++group) {
2417 out << "\t---- group " << group << "/" << (matrix.getRowGroupCount() - 1) << " ---- \n";
2418 typename SparseMatrix<ValueType>::index_type start = matrix.hasTrivialRowGrouping() ? group : matrix.getRowGroupIndices()[group];
2419 typename SparseMatrix<ValueType>::index_type end = matrix.hasTrivialRowGrouping() ? group + 1 : matrix.getRowGroupIndices()[group + 1];
2420
2421 for (typename SparseMatrix<ValueType>::index_type i = start; i < end; ++i) {
2422 typename SparseMatrix<ValueType>::index_type nextIndex = matrix.rowIndications[i];
2423
2424 // Print the actual row.
2425 out << i << "\t(\t";
2426 typename SparseMatrix<ValueType>::index_type currentRealIndex = 0;
2427 while (currentRealIndex < matrix.columnCount) {
2428 if (nextIndex < matrix.rowIndications[i + 1] && currentRealIndex == matrix.columnsAndValues[nextIndex].getColumn()) {
2429 out << matrix.columnsAndValues[nextIndex].getValue() << "\t";
2430 ++nextIndex;
2431 } else {
2432 out << "0\t";
2433 }
2434 ++currentRealIndex;
2435 }
2436 out << "\t)\t" << i << '\n';
2437 }
2438 }
2439
2440 // Print column numbers in footer.
2441 out << "\t\t";
2442 for (typename SparseMatrix<ValueType>::index_type i = 0; i < matrix.getColumnCount(); ++i) {
2443 out << i << "\t";
2444 }
2445 out << '\n';
2446
2447 return out;
2448}
2449
2450template<typename ValueType>
2452 // Iterate over all row groups.
2453 for (typename SparseMatrix<ValueType>::index_type group = 0; group < this->getRowGroupCount(); ++group) {
2454 STORM_LOG_ASSERT(this->getRowGroupSize(group) == 1, "Incorrect row group size.");
2455 for (typename SparseMatrix<ValueType>::index_type i = this->getRowGroupIndices()[group]; i < this->getRowGroupIndices()[group + 1]; ++i) {
2456 typename SparseMatrix<ValueType>::index_type nextIndex = this->rowIndications[i];
2457
2458 // Print the actual row.
2459 out << i << "\t(";
2460 typename SparseMatrix<ValueType>::index_type currentRealIndex = 0;
2461 while (currentRealIndex < this->columnCount) {
2462 if (nextIndex < this->rowIndications[i + 1] && currentRealIndex == this->columnsAndValues[nextIndex].getColumn()) {
2463 out << this->columnsAndValues[nextIndex].getValue() << " ";
2464 ++nextIndex;
2465 } else {
2466 out << "0 ";
2467 }
2468 ++currentRealIndex;
2469 }
2470 out << ";\n";
2471 }
2472 }
2473}
2474
2475template<typename ValueType>
2477 std::size_t result = 0;
2478
2479 boost::hash_combine(result, this->getRowCount());
2480 boost::hash_combine(result, this->getColumnCount());
2481 boost::hash_combine(result, this->getEntryCount());
2482 boost::hash_combine(result, boost::hash_range(columnsAndValues.begin(), columnsAndValues.end()));
2483 boost::hash_combine(result, boost::hash_range(rowIndications.begin(), rowIndications.end()));
2484 if (!this->hasTrivialRowGrouping()) {
2485 boost::hash_combine(result, boost::hash_range(rowGroupIndices.get().begin(), rowGroupIndices.get().end()));
2486 }
2487
2488 return result;
2489}
2490
2491// Explicitly instantiate the entry, builder and the matrix.
2492// double
2494template std::ostream& operator<<(std::ostream& out, MatrixEntry<typename SparseMatrix<double>::index_type, double> const& entry);
2495template class SparseMatrixBuilder<double>;
2496template class SparseMatrix<double>;
2497template std::ostream& operator<<(std::ostream& out, SparseMatrix<double> const& matrix);
2499 typename SparseMatrix<double>::index_type const& row) const;
2500template std::vector<double> SparseMatrix<double>::getPointwiseProductRowSumVector(storm::storage::SparseMatrix<double> const& otherMatrix) const;
2501template bool SparseMatrix<double>::isSubmatrixOf(SparseMatrix<double> const& matrix) const;
2502
2503template class MatrixEntry<uint32_t, double>;
2504template std::ostream& operator<<(std::ostream& out, MatrixEntry<uint32_t, double> const& entry);
2505
2506// int
2508template std::ostream& operator<<(std::ostream& out, MatrixEntry<typename SparseMatrix<int>::index_type, int> const& entry);
2509template class SparseMatrixBuilder<int>;
2510template class SparseMatrix<int>;
2511template std::ostream& operator<<(std::ostream& out, SparseMatrix<int> const& matrix);
2512template bool SparseMatrix<int>::isSubmatrixOf(SparseMatrix<int> const& matrix) const;
2513
2514// state_type
2516template std::ostream& operator<<(
2520template std::ostream& operator<<(std::ostream& out, SparseMatrix<storm::storage::sparse::state_type> const& matrix);
2522
2523// Rational Numbers
2524
2525#if defined(STORM_HAVE_CLN)
2527template std::ostream& operator<<(std::ostream& out, MatrixEntry<typename SparseMatrix<ClnRationalNumber>::index_type, ClnRationalNumber> const& entry);
2529template class SparseMatrix<ClnRationalNumber>;
2530template std::ostream& operator<<(std::ostream& out, SparseMatrix<ClnRationalNumber> const& matrix);
2533template std::vector<storm::ClnRationalNumber> SparseMatrix<ClnRationalNumber>::getPointwiseProductRowSumVector(
2536#endif
2537
2538#if defined(STORM_HAVE_GMP)
2540template std::ostream& operator<<(std::ostream& out, MatrixEntry<typename SparseMatrix<GmpRationalNumber>::index_type, GmpRationalNumber> const& entry);
2542template class SparseMatrix<GmpRationalNumber>;
2543template std::ostream& operator<<(std::ostream& out, SparseMatrix<GmpRationalNumber> const& matrix);
2546template std::vector<storm::GmpRationalNumber> SparseMatrix<GmpRationalNumber>::getPointwiseProductRowSumVector(
2549#endif
2550
2551// Rational Function
2553template std::ostream& operator<<(std::ostream& out, MatrixEntry<typename SparseMatrix<RationalFunction>::index_type, RationalFunction> const& entry);
2555template class SparseMatrix<RationalFunction>;
2556template std::ostream& operator<<(std::ostream& out, SparseMatrix<RationalFunction> const& matrix);
2560 typename SparseMatrix<storm::RationalFunction>::index_type const& row) const;
2562 typename SparseMatrix<storm::RationalFunction>::index_type const& row) const;
2563template std::vector<storm::RationalFunction> SparseMatrix<RationalFunction>::getPointwiseProductRowSumVector(
2565template std::vector<storm::RationalFunction> SparseMatrix<double>::getPointwiseProductRowSumVector(
2567template std::vector<storm::RationalFunction> SparseMatrix<int>::getPointwiseProductRowSumVector(
2570
2571// Intervals
2572template std::vector<storm::Interval> SparseMatrix<double>::getPointwiseProductRowSumVector(
2573 storm::storage::SparseMatrix<storm::Interval> const& otherMatrix) const;
2575template std::ostream& operator<<(std::ostream& out, MatrixEntry<typename SparseMatrix<Interval>::index_type, Interval> const& entry);
2576template class SparseMatrixBuilder<Interval>;
2577template class SparseMatrix<Interval>;
2578template std::ostream& operator<<(std::ostream& out, SparseMatrix<Interval> const& matrix);
2579template std::vector<storm::Interval> SparseMatrix<Interval>::getPointwiseProductRowSumVector(
2580 storm::storage::SparseMatrix<storm::Interval> const& otherMatrix) const;
2582
2584
2585} // namespace storage
2586} // 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
void setMultiple(uint64_t bitIndex, uint64_t nrOfBits, bool newValue=true)
Sets multiple bits to the given value.
uint64_t getNextSetIndex(uint64_t startingIndex) const
Retrieves the index of the bit that is the next bit set to true in the bit vector.
std::vector< uint64_t > getNumberOfSetBitsBeforeIndices() const
Retrieves a vector that holds at position i the number of bits set before index i.
bool empty() const
Retrieves whether no bits are set to true in this bit vector.
uint64_t getNumberOfSetBits() const
Returns the number of bits that are set to true in this bit vector.
uint64_t getNextUnsetIndex(uint64_t startingIndex) const
Retrieves the index of the bit that is the next bit set to false in the bit vector.
void set(uint64_t index, bool value=true)
Sets the given truth value at the given index.
const_iterator begin() const
Returns an iterator to the indices of the set bits in the bit vector.
size_t size() const
Retrieves the number of bits this bit vector can store.
bool get(uint64_t index) const
Retrieves the truth value of the bit at the given index and performs a bound check.
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.
void setColumn(index_type const &column)
Sets the column of the current entry.
MatrixEntry()=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.
ValueType value_type
bool operator==(MatrixEntry const &other) const
This class represents a number of consecutive rows of the matrix.
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.
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.
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.
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.
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].
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.
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.
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.
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.
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
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.
friend class SparseMatrixBuilder< ValueType >
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.
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 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.
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.
std::vector< index_type > const & getRowIndices() const
Returns the entry indices within the given row.
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.
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...
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.
#define STORM_LOG_WARN(message)
Definition logging.h:25
#define STORM_LOG_TRACE(message)
Definition logging.h:12
#define STORM_LOG_ASSERT(cond, message)
Definition macros.h:11
#define STORM_LOG_THROW(cond, exception, message)
Definition macros.h:30
Expression ite(Expression const &condition, Expression const &thenExpression, Expression const &elseExpression)
std::string toString(PomdpMemoryPattern const &pattern)
void print(std::vector< typename SparseMatrix< ValueType >::index_type > const &rowGroupIndices, std::vector< MatrixEntry< typename SparseMatrix< ValueType >::index_type, typename SparseMatrix< ValueType >::value_type > > const &columnsAndValues, std::vector< typename SparseMatrix< ValueType >::index_type > const &rowIndications)
bool isValidPermutation(std::vector< index_type > const &permutation)
Returns true if the given vector is a permutation of the numbers 0, 1, ..., n-1 for n = permutation....
std::vector< T > buildVectorForRange(T min, T max)
Constructs a vector [min, min+1, ...., max-1].
Definition vector.h:129
bool isPositive(ValueType const &a)
Definition constants.cpp:64
bool isOne(ValueType const &a)
Definition constants.cpp:34
bool isConstant(ValueType const &)
bool isZero(ValueType const &a)
Definition constants.cpp:39
typename detail::IntervalMetaProgrammingHelper< ValueType >::BaseType IntervalBaseType
Helper to access the type in which interval boundaries are stored.