24template<
typename IndexType,
typename ValueType>
29template<
typename IndexType,
typename ValueType>
34template<
typename IndexType,
typename ValueType>
36 return this->entry.first;
39template<
typename IndexType,
typename ValueType>
41 this->entry.first = column;
44template<
typename IndexType,
typename ValueType>
46 return this->entry.second;
49template<
typename IndexType,
typename ValueType>
51 this->entry.second = value;
54template<
typename IndexType,
typename ValueType>
59template<
typename IndexType,
typename ValueType>
61 return MatrixEntry(this->getColumn(), this->getValue() * factor);
64template<
typename IndexType,
typename ValueType>
66 return this->entry.first == other.entry.first && this->entry.second == other.entry.second;
69template<
typename IndexType,
typename ValueType>
71 return !(*
this == other);
74template<
typename IndexTypePrime,
typename ValueTypePrime>
80template<
typename ValueType>
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),
100 currentRowGroupCount(0) {
102 if (initialRowCountSet) {
103 rowIndications.reserve(initialRowCount + 1);
105 if (initialEntryCountSet) {
106 columnsAndValues.reserve(initialEntryCount);
108 if (hasCustomRowGrouping) {
109 rowGroupIndices = std::vector<index_type>();
111 if (initialRowGroupCountSet && hasCustomRowGrouping) {
112 rowGroupIndices.get().reserve(initialRowGroupCount + 1);
114 rowIndications.push_back(0);
117template<
typename ValueType>
119 : initialRowCountSet(false),
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),
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;
139 if (hasCustomRowGrouping) {
140 rowGroupIndices = std::move(matrix.rowGroupIndices);
141 if (!rowGroupIndices->empty()) {
142 rowGroupIndices.get().pop_back();
144 currentRowGroupCount = rowGroupIndices->empty() ? 0 : rowGroupIndices.get().size() - 1;
148 if (!rowIndications.empty()) {
149 rowIndications.pop_back();
153template<
typename ValueType>
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.");
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;
167 if (row == lastRow && column == diagColumn) {
170 addNextValue(row, column, diagValue + value);
174 addNextValue(lastRow, diagColumn, diagValue);
181 bool fixCurrentRow = row == lastRow && column < lastColumn;
184 if (row == lastRow && column == lastColumn && rowIndications.back() < currentEntryCount) {
185 columnsAndValues.back().setValue(columnsAndValues.back().getValue() + value);
188 if (row != lastRow) {
190 assert(rowIndications.size() == lastRow + 1);
191 rowIndications.resize(row + 1, currentEntryCount);
198 columnsAndValues.emplace_back(column, value);
199 highestColumn = std::max(highestColumn, column);
205 STORM_LOG_TRACE(
"Fix row " << row <<
" as column " << column <<
" is added out-of-order.");
207 std::sort(columnsAndValues.begin() + rowIndications.back(), columnsAndValues.end(),
209 return a.getColumn() < b.getColumn();
212 auto insertIt = columnsAndValues.begin() + rowIndications.back();
213 uint64_t elementsToRemove = 0;
214 for (
auto it = insertIt + 1; it != columnsAndValues.end(); ++it) {
216 if (it->getColumn() == insertIt->getColumn()) {
218 insertIt->setValue(insertIt->getValue() + it->getValue());
226 static_cast<void>(std::unique(columnsAndValues.begin() + rowIndications.back(), columnsAndValues.end(),
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);
235 lastColumn = columnsAndValues.back().getColumn();
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 <<
".");
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.");
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;
261 addNextValue(lastRow, diagColumn, diagValue);
264 rowGroupIndices.get().push_back(startingRow);
265 ++currentRowGroupCount;
268 if (lastRow + 1 < startingRow) {
270 assert(rowIndications.size() == lastRow + 1);
271 rowIndications.resize(startingRow, currentEntryCount);
273 lastRow = startingRow - 1;
278template<
typename ValueType>
282 if (pendingDiagonalEntry) {
283 index_type diagColumn = hasCustomRowGrouping ? currentRowGroupCount - 1 : lastRow;
284 ValueType diagValue = std::move(pendingDiagonalEntry.get());
285 pendingDiagonalEntry = boost::none;
286 addNextValue(lastRow, diagColumn, diagValue);
289 bool hasEntries = currentEntryCount != 0;
291 uint_fast64_t rowCount = hasEntries ? lastRow + 1 : 0;
294 if (hasCustomRowGrouping) {
295 if (lastRow < rowGroupIndices->back()) {
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);
306 rowCount = std::max(rowCount, overriddenRowCount);
310 rowIndications.push_back(currentEntryCount);
317 rowIndications.push_back(currentEntryCount);
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);
327 columnCount = std::max(columnCount, overriddenColumnCount);
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 <<
".");
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);
343 rowGroupCount = std::max(rowGroupCount, overriddenRowGroupCount);
345 for (
index_type i = currentRowGroupCount;
i <= rowGroupCount; ++
i) {
346 rowGroupIndices.get().push_back(rowCount);
350 return SparseMatrix<ValueType>(columnCount, std::move(rowIndications), std::move(columnsAndValues), std::move(rowGroupIndices));
353template<
typename ValueType>
358template<
typename ValueType>
360 if (this->hasCustomRowGrouping) {
361 return currentRowGroupCount;
363 return getLastRow() + 1;
367template<
typename ValueType>
373template<
typename ValueType>
381 std::cout <<
"\t---- group " << group <<
"/" << (rowGroupIndices.size() - 1) <<
" ---- \n";
382 endGroups = group < rowGroupIndices.size() - 1 ? rowGroupIndices[group + 1] : rowIndications.size();
385 endRows =
i < rowIndications.size() - 1 ? rowIndications[
i + 1] : columnsAndValues.size();
387 std::cout <<
"Row " <<
i <<
" (" << rowIndications[
i] <<
" - " << endRows <<
")" <<
": ";
389 std::cout <<
"(" << columnsAndValues[pos].getColumn() <<
": " << columnsAndValues[pos].getValue() <<
") ";
396template<
typename ValueType>
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) {
407 entry->setColumn(replacements[entry->getColumn() - offset]);
410 maxColumn = std::max(maxColumn, entry->getColumn());
414 std::sort(startRow, endRow,
421 "Columns not sorted.");
425 highestColumn = maxColumn;
426 lastColumn = columnsAndValues.empty() ? 0 : columnsAndValues.back().getColumn();
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) {
436 pendingDiagonalEntry.get() += value;
440 index_type column = hasCustomRowGrouping ? currentRowGroupCount - 1 : lastRow;
441 ValueType diagValue = std::move(pendingDiagonalEntry.get());
442 pendingDiagonalEntry = boost::none;
443 addNextValue(lastRow, column, diagValue);
446 pendingDiagonalEntry = value;
447 if (lastRow != row) {
448 assert(rowIndications.size() == lastRow + 1);
449 rowIndications.resize(row + 1, currentEntryCount);
455template<
typename ValueType>
460template<
typename ValueType>
462 return beginIterator;
465template<
typename ValueType>
467 return beginIterator + entryCount;
470template<
typename ValueType>
472 return this->entryCount;
475template<
typename ValueType>
480template<
typename ValueType>
482 return beginIterator;
485template<
typename ValueType>
487 return beginIterator + entryCount;
490template<
typename ValueType>
492 return this->entryCount;
495template<
typename ValueType>
497 : rowCount(0), columnCount(0), entryCount(0), nonzeroEntryCount(0), columnsAndValues(), rowIndications(), rowGroupIndices() {
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) {
514template<
typename ValueType>
518 *
this = other.
getSubmatrix(
false, rowConstraint, columnConstraint, insertDiagonalElements);
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)) {
533 other.columnCount = 0;
534 other.entryCount = 0;
537template<
typename ValueType>
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) {
552template<
typename ValueType>
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)) {
563 this->rowCount = this->rowIndications.size() - 1;
564 this->entryCount = this->columnsAndValues.size();
565 this->trivialRowGrouping = !this->rowGroupIndices;
569template<
typename ValueType>
572 if (
this != &other) {
573 rowCount = other.rowCount;
574 columnCount = other.columnCount;
575 entryCount = other.entryCount;
576 nonzeroEntryCount = other.nonzeroEntryCount;
578 columnsAndValues = other.columnsAndValues;
579 rowIndications = other.rowIndications;
580 rowGroupIndices = other.rowGroupIndices;
581 trivialRowGrouping = other.trivialRowGrouping;
586template<
typename ValueType>
589 if (
this != &other) {
590 rowCount = other.rowCount;
591 columnCount = other.columnCount;
592 entryCount = other.entryCount;
593 nonzeroEntryCount = other.nonzeroEntryCount;
595 columnsAndValues = std::move(other.columnsAndValues);
596 rowIndications = std::move(other.rowIndications);
597 rowGroupIndices = std::move(other.rowGroupIndices);
598 trivialRowGrouping = other.trivialRowGrouping;
603template<
typename ValueType>
605 if (
this == &other) {
609 bool equalityResult =
true;
612 if (!equalityResult) {
616 if (!equalityResult) {
624 if (!equalityResult) {
640 if ((it1 == ite1) || (it2 == ite2)) {
641 equalityResult = (it1 == ite1) ^ (it2 == ite2);
644 if (it1->getColumn() != it2->getColumn() || it1->getValue() != it2->getValue()) {
645 equalityResult =
false;
650 if (!equalityResult) {
655 return equalityResult;
658template<
typename ValueType>
663template<
typename ValueType>
668template<
typename ValueType>
673template<
typename ValueType>
678 result += (this->rowIndications[row + 1] - this->rowIndications[row]);
681 result += (this->rowIndications[group + 1] - this->rowIndications[group]);
686template<
typename ValueType>
688 return nonzeroEntryCount;
691template<
typename ValueType>
693 this->nonzeroEntryCount = 0;
694 for (
auto const& element : *
this) {
695 if (element.getValue() != storm::utility::zero<ValueType>()) {
696 ++this->nonzeroEntryCount;
701template<
typename ValueType>
703 this->nonzeroEntryCount += difference;
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);
718template<
typename ValueType>
721 return rowGroupIndices.get().size() - 1;
727template<
typename ValueType>
732template<
typename ValueType>
739 for (
auto const&
i : rowGroupIndices.get()) {
740 res = std::max(res,
i - previousGroupStart);
741 previousGroupStart =
i;
746template<
typename ValueType>
758 numRows +=
end - start;
764template<
typename ValueType>
767 if (!this->rowGroupIndices) {
768 STORM_LOG_ASSERT(trivialRowGrouping,
"Only trivial row-groupings can be constructed on-the-fly.");
771 return rowGroupIndices.get();
774template<
typename ValueType>
776 return rowIndications;
779template<
typename ValueType>
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]);
786 return boost::irange(group, group + 1);
790template<
typename ValueType>
792 std::vector<index_type> result;
793 if (this->rowGroupIndices) {
794 result = std::move(rowGroupIndices.get());
795 rowGroupIndices = std::move(newRowGrouping);
800template<
typename ValueType>
802 trivialRowGrouping =
false;
803 rowGroupIndices = newRowGroupIndices;
806template<
typename ValueType>
808 return trivialRowGrouping;
811template<
typename ValueType>
813 if (trivialRowGrouping) {
816 "Row grouping is supposed to be trivial but actually it is not.");
818 trivialRowGrouping =
true;
819 rowGroupIndices = boost::none;
823template<
typename ValueType>
826 for (
auto group : groupConstraint) {
832template<
typename ValueType>
836 for (
auto group : groupConstraint) {
838 bool choiceSatisfiesColumnConstraint =
true;
839 for (
auto const& entry : this->
getRow(row)) {
840 if (!columnConstraint.
get(entry.getColumn())) {
841 choiceSatisfiesColumnConstraint =
false;
845 if (choiceSatisfiesColumnConstraint) {
846 result.
set(row,
true);
853template<
typename ValueType>
858 if (setIfForAllRowsInGroup) {
860 if (rowConstraint.
getNextUnsetIndex(groupIndices[group]) >= groupIndices[group + 1]) {
862 result.
set(group,
true);
867 if (rowConstraint.
getNextSetIndex(groupIndices[group]) < groupIndices[group + 1]) {
869 result.
set(group,
true);
876template<
typename ValueType>
880 for (
auto row : rows) {
888template<
typename ValueType>
893 for (
auto rowGroup : rowGroupConstraint) {
899 for (
auto rowGroup : rowGroupConstraint) {
908template<
typename ValueType>
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.";
924 while (columnValuePtr->getColumn() < column && columnValuePtr != lastColumnValuePtr) {
926 --this->nonzeroEntryCount;
928 columnValuePtr->setValue(storm::utility::zero<ValueType>());
933 ++this->nonzeroEntryCount;
935 columnValuePtr->setValue(storm::utility::one<ValueType>());
936 columnValuePtr->setColumn(column);
937 for (++columnValuePtr; columnValuePtr != columnValuePtrEnd; ++columnValuePtr) {
939 --this->nonzeroEntryCount;
941 columnValuePtr->setValue(storm::utility::zero<ValueType>());
948template<
typename ValueType>
954 for (; it1 != end1 && it2 != end2; ++it1, ++it2) {
959 if (it1 == end1 && it2 == end2) {
965template<
typename ValueType>
968 for (
size_t rowgroup = 0; rowgroup < this->
getRowGroupCount(); ++rowgroup) {
970 for (
size_t row2 = row1; row2 < this->
getRowGroupIndices().at(rowgroup + 1); ++row2) {
980template<
typename ValueType>
988 index_type smallerRow = largerRow == row1 ? row2 : row1;
993 std::vector<MatrixEntry<index_type, value_type>> largerRowContents(copyRow.begin(), copyRow.end());
995 if (largerRow < smallerRow) {
996 auto writeIt =
getRows(largerRow, smallerRow + 1).
begin();
999 for (
auto& smallerRowEntry :
getRow(smallerRow)) {
1000 *writeIt = std::move(smallerRowEntry);
1006 for (
auto& intermediateRowEntry :
getRows(largerRow + 1, smallerRow)) {
1007 *writeIt = std::move(intermediateRowEntry);
1016 for (
auto& largerRowEntry : largerRowContents) {
1017 *writeIt = std::move(largerRowEntry);
1025 for (
index_type row = largerRow + 1; row <= smallerRow; ++row) {
1026 rowIndications[row] -= rowSizeDifference;
1030 auto writeIt =
getRows(smallerRow, largerRow + 1).
end() - 1;
1033 auto copyRow =
getRow(smallerRow);
1034 for (
auto smallerRowEntryIt = copyRow.end() - 1; smallerRowEntryIt != copyRow.begin() - 1; --smallerRowEntryIt) {
1035 *writeIt = std::move(*smallerRowEntryIt);
1041 for (
auto intermediateRowEntryIt =
getRows(smallerRow + 1, largerRow).
end() - 1;
1042 intermediateRowEntryIt !=
getRows(smallerRow + 1, largerRow).
begin() - 1; --intermediateRowEntryIt) {
1043 *writeIt = std::move(*intermediateRowEntryIt);
1052 for (
auto largerRowEntryIt = largerRowContents.rbegin(); largerRowEntryIt != largerRowContents.rend(); ++largerRowEntryIt) {
1053 *writeIt = std::move(*largerRowEntryIt);
1062 for (
index_type row = smallerRow + 1; row <= largerRow; ++row) {
1063 rowIndications[row] += rowSizeDifference;
1069template<
typename ValueType>
1071 std::vector<ValueType> result(this->
getRowCount());
1074 for (
auto resultIt = result.begin(), resultIte = result.end(); resultIt != resultIte; ++resultIt, ++row) {
1081template<
typename ValueType>
1083 ValueType result = storm::utility::zero<ValueType>();
1085 if (constraint.
get(it->getColumn())) {
1086 result += it->getValue();
1092template<
typename ValueType>
1097 for (
auto row : rowConstraint) {
1103template<
typename ValueType>
1106 std::vector<ValueType> result;
1109 for (
auto rowGroup : rowGroupConstraint) {
1115 for (
auto rowGroup : rowGroupConstraint) {
1122template<
typename ValueType>
1130 std::vector<index_type> fakeRowGroupIndices(rowCount + 1);
1132 for (std::vector<index_type>::iterator it = fakeRowGroupIndices.begin(); it != fakeRowGroupIndices.end(); ++it, ++
i) {
1135 auto res =
getSubmatrix(rowConstraint, columnConstraint, fakeRowGroupIndices, insertDiagonalElements, makeZeroColumns);
1140 std::vector<index_type> newRowGroupIndices;
1141 newRowGroupIndices.push_back(0);
1142 auto selectedRowIt = rowConstraint.
begin();
1151 if (newRowCount > 0) {
1152 newRowGroupIndices.push_back(newRowGroupIndices.back() + newRowCount);
1156 res.trivialRowGrouping =
false;
1157 res.rowGroupIndices = newRowGroupIndices;
1164template<
typename ValueType>
1168 STORM_LOG_THROW(!rowGroupConstraint.
empty() && !columnConstraint.
empty(), storm::exceptions::InvalidArgumentException,
"Cannot build empty submatrix.");
1174 std::unique_ptr<std::vector<index_type>> tmp;
1175 if (rowGroupConstraint != columnConstraint) {
1178 std::vector<index_type>
const& rowBitsSetBeforeIndex = tmp ? *tmp : columnBitsSetBeforeIndex;
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;
1190 if (columnConstraint.
get(it->getColumn()) && (makeZeroColumns.
size() == 0 || !makeZeroColumns.
get(it->getColumn()))) {
1193 if (columnBitsSetBeforeIndex[it->getColumn()] == rowBitsSetBeforeIndex[index]) {
1194 foundDiagonalElement =
true;
1200 if (insertDiagonalEntries && !foundDiagonalElement && rowGroupCount < submatrixColumnCount) {
1214 for (
auto index : rowGroupConstraint) {
1216 matrixBuilder.newRowGroup(rowCount);
1218 for (
index_type i = rowGroupIndices[index];
i < rowGroupIndices[index + 1]; ++
i) {
1219 bool insertedDiagonalElement =
false;
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;
1230 matrixBuilder.addNextValue(rowCount, columnBitsSetBeforeIndex[it->getColumn()], it->getValue());
1233 if (insertDiagonalEntries && !insertedDiagonalElement && rowGroupCount < submatrixColumnCount) {
1234 matrixBuilder.addNextValue(rowCount, rowGroupCount, storm::utility::zero<ValueType>());
1241 return matrixBuilder.build();
1244template<
typename ValueType>
1250 for (
auto row : rowsToKeep) {
1260 --firstTrailingEmptyRowGroup;
1263 "Empty rows are not allowed, but row group " << firstTrailingEmptyRowGroup <<
" is empty.");
1268 for (
index_type rowGroup = 0; rowGroup < firstTrailingEmptyRowGroup; ++rowGroup) {
1271 bool rowGroupEmpty =
true;
1274 rowGroupEmpty =
false;
1275 for (
auto const& entry : this->
getRow(row)) {
1276 builder.
addNextValue(newRow, entry.getColumn(), entry.getValue());
1280 STORM_LOG_THROW(allowEmptyRowGroups || !rowGroupEmpty, storm::exceptions::InvalidArgumentException,
1281 "Empty rows are not allowed, but row group " << rowGroup <<
" is empty.");
1289template<
typename ValueType>
1293 for (
auto row : rowFilter) {
1299 for (
auto row : rowFilter) {
1300 for (
auto const& entry :
getRow(row)) {
1301 builder.
addNextValue(row, entry.getColumn(), entry.getValue());
1313template<
typename ValueType>
1319 for (
auto const& entry :
getRow(row)) {
1321 builder.
addNextValue(row, entry.getColumn(), entry.getValue());
1330 *
this = std::move(result);
1334template<
typename ValueType>
1336 bool insertDiagonalEntries)
const {
1340 for (
index_type rowGroupIndex = 0, rowGroupIndexEnd = rowGroupToRowIndexMapping.size(); rowGroupIndex < rowGroupIndexEnd; ++rowGroupIndex) {
1343 "Cannot point to row offset " << rowGroupToRowIndexMapping[rowGroupIndex] <<
" for rowGroup " << rowGroupIndex <<
" which starts at "
1349 bool foundDiagonalElement =
false;
1351 if (it->getColumn() == rowGroupIndex) {
1352 foundDiagonalElement =
true;
1356 if (insertDiagonalEntries && !foundDiagonalElement) {
1365 for (
index_type rowGroupIndex = 0, rowGroupIndexEnd = rowGroupToRowIndexMapping.size(); rowGroupIndex < rowGroupIndexEnd; ++rowGroupIndex) {
1371 bool insertedDiagonalElement =
false;
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;
1379 matrixBuilder.
addNextValue(rowGroupIndex, it->getColumn(), it->getValue());
1381 if (insertDiagonalEntries && !insertedDiagonalElement) {
1382 matrixBuilder.
addNextValue(rowGroupIndex, rowGroupIndex, storm::utility::zero<ValueType>());
1387 return matrixBuilder.
build();
1390template<
typename ValueType>
1392 bool insertDiagonalEntries)
const {
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;
1404 if (insertDiagonalEntries && !foundDiagonalElement) {
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;
1422 matrixBuilder.
addNextValue(row, it->getColumn(), it->getValue());
1424 if (insertDiagonalEntries && !insertedDiagonalElement) {
1425 matrixBuilder.
addNextValue(row, row, storm::utility::zero<ValueType>());
1430 return matrixBuilder.
build();
1433template<
typename ValueType>
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());
1449 auto result = matrixBuilder.
build();
1450 if (this->rowGroupIndices) {
1451 result.setRowGroupIndices(this->rowGroupIndices.get());
1456template<
typename ValueType>
1458 std::vector<index_type>
const& columnPermutation)
const {
1463 auto oldGroupIt = inverseRowGroupPermutation.cbegin();
1465 while (newRowIndex < rowCount) {
1470 for (
auto const& oldEntry :
getRow(oldRowIndex)) {
1471 matrixBuilder.
addNextValue(newRowIndex, columnPermutation[oldEntry.getColumn()], oldEntry.getValue());
1477 return matrixBuilder.
build();
1480template<
typename ValueType>
1492 std::vector<index_type> rowIndications(rowCount + 1);
1493 std::vector<MatrixEntry<index_type, ValueType>> columnsAndValues(entryCount);
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];
1506 rowIndications[
i] = rowIndications[
i - 1] + rowIndications[
i];
1512 std::vector<index_type> nextIndices = rowIndications;
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()]++;
1526 return transposedMatrix;
1529template<
typename ValueType>
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)) {
1542 ++rowIndications[entry.getColumn() + 1];
1549 rowIndications[
i] = rowIndications[
i - 1] + rowIndications[
i];
1552 std::vector<MatrixEntry<index_type, ValueType>> columnsAndValues(entryCount);
1557 std::vector<index_type> nextIndices = rowIndications;
1560 rowGroupChoiceIt = rowGroupChoices.begin();
1561 for (
index_type rowGroup = 0; rowGroup < columnCount; ++rowGroup, ++rowGroupChoiceIt) {
1562 for (
auto const& entry : this->
getRow(rowGroup, *rowGroupChoiceIt)) {
1564 columnsAndValues[nextIndices[entry.getColumn()]] = std::make_pair(rowGroup, entry.getValue());
1565 ++nextIndices[entry.getColumn()];
1573template<
typename ValueType>
1579template<
typename ValueType>
1583 ValueType one = storm::utility::one<ValueType>();
1584 ValueType zero = storm::utility::zero<ValueType>();
1585 bool foundDiagonalElement =
false;
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);
1596 entry.setValue(one - entry.getValue());
1598 foundDiagonalElement =
true;
1603 if (!foundDiagonalElement) {
1604 throw storm::exceptions::InvalidArgumentException() <<
"Illegal call to SparseMatrix::invertDiagonal: matrix is missing diagonal entries.";
1609template<
typename ValueType>
1614 if (entry.getColumn() != group) {
1615 entry.setValue(-entry.getValue());
1621template<
typename ValueType>
1626 if (entry.getColumn() == group) {
1627 --this->nonzeroEntryCount;
1628 entry.setValue(storm::utility::zero<ValueType>());
1637template<
typename ValueType>
1640 "Canno compute Jacobi decomposition of non-square matrix.");
1644 std::vector<ValueType> invertedDiagonal(rowCount);
1647 for (
index_type rowNumber = 0; rowNumber < rowCount; ++rowNumber) {
1649 if (it->getColumn() == rowNumber) {
1650 invertedDiagonal[rowNumber] = storm::utility::one<ValueType>() / it->getValue();
1652 luBuilder.
addNextValue(rowNumber, it->getColumn(), it->getValue());
1657 return std::make_pair(luBuilder.
build(), std::move(invertedDiagonal));
1662 STORM_LOG_THROW(
false, storm::exceptions::NotImplementedException,
"This operation is not supported.");
1668 STORM_LOG_THROW(
false, storm::exceptions::NotImplementedException,
"This operation is not supported.");
1671template<
typename ValueType>
1672template<
typename OtherValueType,
typename ResultValueType>
1680 ResultValueType result = storm::utility::zero<ResultValueType>();
1681 for (; it1 != ite1 && it2 != ite2; ++it1) {
1682 if (it1->getColumn() < it2->getColumn()) {
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());
1696template<
typename ValueType>
1697template<
typename OtherValueType,
typename ResultValueType>
1699 std::vector<ResultValueType> result;
1700 result.reserve(rowCount);
1702 result.push_back(getPointwiseProductRowSum<OtherValueType, ResultValueType>(otherMatrix, row));
1707template<
typename ValueType>
1709 std::vector<value_type>
const* summand)
const {
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;
1723 if (target == &temporary) {
1724 std::swap(result, *target);
1728template<
typename ValueType>
1730 std::vector<value_type>
const* summand)
const {
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;
1738 summandIterator = summand->begin();
1741 for (; resultIterator != resultIteratorEnd; ++rowIterator, ++resultIterator, ++summandIterator) {
1744 newValue = *summandIterator;
1746 newValue = storm::utility::zero<ValueType>();
1749 for (ite = this->
begin() + *(rowIterator + 1); it != ite; ++it) {
1750 newValue += it->getValue() * vector[it->getColumn()];
1753 *resultIterator = newValue;
1757template<
typename ValueType>
1759 std::vector<value_type>
const* summand)
const {
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;
1767 summandIterator = summand->end() - 1;
1770 for (; resultIterator != resultIteratorEnd; --rowIterator, --resultIterator, --summandIterator) {
1773 newValue = *summandIterator;
1775 newValue = storm::utility::zero<ValueType>();
1778 for (ite = this->
begin() + *rowIterator - 1; it != ite; --it) {
1779 newValue += (it->getValue() * vector[it->getColumn()]);
1782 *resultIterator = newValue;
1786template<
typename ValueType>
1788 ValueType result = storm::utility::zero<ValueType>();
1790 for (
auto const& entry : this->
getRow(row)) {
1791 result += entry.getValue() * vector[entry.getColumn()];
1796template<
typename ValueType>
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;
1806 for (; resultIterator != resultIteratorEnd; --rowIterator, --resultIterator, --bIt) {
1808 ValueType tmpValue = storm::utility::zero<ValueType>();
1809 ValueType diagonalElement = storm::utility::zero<ValueType>();
1811 for (ite = this->
begin() + *rowIterator - 1; it != ite; --it) {
1812 if (it->getColumn() != currentRow) {
1813 tmpValue += it->getValue() * x[it->getColumn()];
1815 diagonalElement += it->getValue();
1819 *resultIterator = ((storm::utility::one<ValueType>() - omega) * *resultIterator) + (omega / diagonalElement) * (*bIt - tmpValue);
1825 STORM_LOG_THROW(
false, storm::exceptions::NotSupportedException,
"This operation is not supported.");
1828template<
typename ValueType>
1830 std::vector<ValueType>
const& ax, std::vector<ValueType>& result)
const {
1833 std::vector<index_type>::const_iterator rowIterator = rowIndications.begin();
1836 ValueType zero = storm::utility::zero<ValueType>();
1837 for (
auto& entry : result) {
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]);
1847 auto xIterator = x.begin();
1848 auto sumsIterator = columnSums.begin();
1849 for (
auto& entry : result) {
1850 entry *= *xIterator / *sumsIterator;
1858 std::vector<Interval>
const& ax, std::vector<Interval>& result)
const {
1859 STORM_LOG_THROW(
false, storm::exceptions::NotSupportedException,
"This operation is not supported.");
1862template<
typename ValueType>
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);
1869 multiplyAndReduceForward<storm::utility::ElementGreater<ValueType>>(rowGroupIndices, vector, summand, result, choices);
1873template<
typename ValueType>
1874template<
typename Compare>
1876 std::vector<ValueType>
const* summand, std::vector<ValueType>& result,
1877 std::vector<uint64_t>* choices)
const {
1879 auto elementIt = this->
begin();
1880 auto rowGroupIt = rowGroupIndices.begin();
1881 auto rowIt = rowIndications.begin();
1882 typename std::vector<ValueType>::const_iterator summandIt;
1884 summandIt = summand->begin();
1886 typename std::vector<uint64_t>::iterator choiceIt;
1888 choiceIt = choices->begin();
1892 ValueType oldSelectedChoiceValue;
1893 uint64_t selectedChoice;
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>();
1900 if (*rowGroupIt < *(rowGroupIt + 1)) {
1902 currentValue = *summandIt;
1906 for (
auto elementIte = this->
begin() + *(rowIt + 1); elementIt != elementIte; ++elementIt) {
1907 currentValue += elementIt->getValue() * vector[elementIt->getColumn()];
1912 if (*choiceIt == 0) {
1913 oldSelectedChoiceValue = currentValue;
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()];
1926 if (choices && currentRow == *choiceIt + *rowGroupIt) {
1927 oldSelectedChoiceValue = newValue;
1930 if (compare(newValue, currentValue)) {
1931 currentValue = newValue;
1933 selectedChoice = currentRow - *rowGroupIt;
1942 *resultIt = currentValue;
1943 if (choices && compare(currentValue, oldSelectedChoiceValue)) {
1944 *choiceIt = selectedChoice;
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.");
1958template<
typename ValueType>
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);
1965 multiplyAndReduceBackward<storm::utility::ElementGreater<ValueType>>(rowGroupIndices, vector, summand, result, choices);
1969template<
typename ValueType>
1970template<
typename Compare>
1972 std::vector<ValueType>
const* summand, std::vector<ValueType>& result,
1973 std::vector<uint64_t>* choices)
const {
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;
1980 summandIt = summand->end() - 1;
1982 typename std::vector<uint64_t>::iterator choiceIt;
1984 choiceIt = choices->end() - 1;
1988 ValueType oldSelectedChoiceValue;
1989 uint64_t selectedChoice;
1992 for (
auto resultIt = result.end() - 1, resultIte = result.begin() - 1; resultIt != resultIte; --resultIt, --choiceIt, --rowGroupIt) {
1993 ValueType currentValue = storm::utility::zero<ValueType>();
1996 if (*rowGroupIt < *(rowGroupIt + 1)) {
1998 currentValue = *summandIt;
2002 for (
auto elementIte = this->
begin() + *rowIt - 1; elementIt != elementIte; --elementIt) {
2003 currentValue += elementIt->getValue() * vector[elementIt->getColumn()];
2006 selectedChoice = currentRow - *rowGroupIt;
2007 if (*choiceIt == selectedChoice) {
2008 oldSelectedChoiceValue = currentValue;
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()];
2020 if (choices && currentRow == *choiceIt + *rowGroupIt) {
2021 oldSelectedChoiceValue = newValue;
2024 if (compare(newValue, currentValue)) {
2025 currentValue = newValue;
2027 selectedChoice = currentRow - *rowGroupIt;
2033 *resultIt = currentValue;
2034 if (choices && compare(currentValue, oldSelectedChoiceValue)) {
2035 *choiceIt = selectedChoice;
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.");
2049template<
typename ValueType>
2051 std::vector<ValueType>
const& vector, std::vector<ValueType>
const* summand, std::vector<ValueType>& result,
2052 std::vector<uint64_t>* choices)
const {
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;
2066 if (target == &temporary) {
2067 std::swap(temporary, result);
2071template<
typename ValueType>
2075 std::vector<index_type>::const_iterator rowIterator = rowIndications.begin();
2076 std::vector<index_type>::const_iterator rowIteratorEnd = rowIndications.end();
2079 for (; rowIterator != rowIteratorEnd - 1; ++rowIterator) {
2080 for (ite = this->
begin() + *(rowIterator + 1); it != ite; ++it) {
2081 result[it->getColumn()] += it->getValue() * vector[currentRow];
2087template<
typename ValueType>
2089 STORM_LOG_ASSERT(factors.size() == this->getRowCount(),
"Can not scale rows: Number of rows and number of scaling factors do not match.");
2091 for (
auto const& factor : factors) {
2092 for (
auto& entry :
getRow(row)) {
2093 entry.setValue(entry.getValue() * factor);
2099template<
typename ValueType>
2101 STORM_LOG_ASSERT(divisors.size() == this->getRowCount(),
"Can not divide rows: Number of rows and number of divisors do not match.");
2103 for (
auto const& divisor : divisors) {
2105 for (
auto& entry :
getRow(row)) {
2106 entry.setValue(entry.getValue() / divisor);
2114 STORM_LOG_THROW(
false, storm::exceptions::NotImplementedException,
"This operation is not supported.");
2117template<
typename ValueType>
2119 return const_rows(this->columnsAndValues.begin() + this->rowIndications[startRow], this->rowIndications[endRow] - this->rowIndications[startRow]);
2122template<
typename ValueType>
2124 return rows(this->columnsAndValues.begin() + this->rowIndications[startRow], this->rowIndications[endRow] - this->rowIndications[startRow]);
2127template<
typename ValueType>
2132template<
typename ValueType>
2137template<
typename ValueType>
2148template<
typename ValueType>
2156 return getRow(rowGroup + offset);
2160template<
typename ValueType>
2166 return getRows(rowGroup, rowGroup + 1);
2170template<
typename ValueType>
2176 return getRows(rowGroup, rowGroup + 1);
2180template<
typename ValueType>
2183 return this->columnsAndValues.begin() + this->rowIndications[row];
2186template<
typename ValueType>
2189 return this->columnsAndValues.begin() + this->rowIndications[row];
2192template<
typename ValueType>
2194 return this->columnsAndValues.begin();
2197template<
typename ValueType>
2199 return this->columnsAndValues.begin();
2202template<
typename ValueType>
2205 return this->columnsAndValues.begin() + this->rowIndications[row + 1];
2208template<
typename ValueType>
2211 return this->columnsAndValues.begin() + this->rowIndications[row + 1];
2214template<
typename ValueType>
2216 return this->columnsAndValues.begin() + this->rowIndications[rowCount];
2219template<
typename ValueType>
2221 return this->columnsAndValues.begin() + this->rowIndications[rowCount];
2224template<
typename ValueType>
2226 ValueType sum = storm::utility::zero<ValueType>();
2228 sum += it->getValue();
2233template<
typename ValueType>
2236 for (
auto const& entry : *
this) {
2241 return nonConstEntries;
2244template<
typename ValueType>
2248 for (
auto const& entry : this->
getRowGroup(rowGroup)) {
2250 ++nonConstRowGroups;
2255 return nonConstRowGroups;
2258template<
typename ValueType>
2262 auto toBaseType = [](ValueType
const& value) {
2263 if constexpr (std::is_same_v<ValueType, BaseType>) {
2266 return storm::utility::convertNumber<BaseType>(value);
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);
2274 auto isContained = [&toBaseType](ValueType
const& value, BaseType
const& lower, BaseType
const& upper) {
2277 if constexpr (storm::IsIntervalType<ValueType>) {
2279 return value.lower() <= upper && value.upper() >= lower;
2280 }
else if constexpr (std::is_same_v<ValueType, storm::RationalFunction>) {
2283 auto const constValue = toBaseType(value);
2284 return constValue <= upper && constValue >= lower;
2290 return value <= upper && value >= lower;
2294 auto toString = [](ValueType
const& value) {
2295 std::stringstream s;
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)) {
2305 *reason =
"Entry in row " + std::to_string(row) +
" is not a probability: " +
toString(entry.getValue());
2309 rowSum += entry.getValue();
2311 if (!isContained(rowSum, oneMinusTolerance, onePlusTolerance)) {
2314 *reason =
"Sum of entries in row " + std::to_string(row) +
" is not one: sum-1=" +
toString(rowSum - storm::utility::one<ValueType>());
2322template<
typename ValueType>
2324 for (
auto const& entry : *
this) {
2332template<
typename ValueType>
2333template<
typename OtherValueType>
2351 auto it2 = matrix.
begin(row);
2352 auto ite2 = matrix.
end(row);
2355 while (it2 != ite2 && it2->getColumn() < it1->getColumn()) {
2358 if (it2 == ite2 || it1->getColumn() != it2->getColumn()) {
2366template<
typename ValueType>
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) {
2395template<
typename ValueType>
2397 std::string result =
2406template<
typename ValueType>
2417 out <<
"\t---- group " << group <<
"/" << (matrix.
getRowGroupCount() - 1) <<
" ---- \n";
2425 out <<
i <<
"\t(\t";
2427 while (currentRealIndex < matrix.columnCount) {
2428 if (nextIndex < matrix.rowIndications[
i + 1] && currentRealIndex == matrix.columnsAndValues[nextIndex].getColumn()) {
2429 out << matrix.columnsAndValues[nextIndex].getValue() <<
"\t";
2436 out <<
"\t)\t" <<
i <<
'\n';
2450template<
typename ValueType>
2461 while (currentRealIndex < this->columnCount) {
2462 if (nextIndex < this->rowIndications[
i + 1] && currentRealIndex == this->columnsAndValues[nextIndex].getColumn()) {
2463 out << this->columnsAndValues[nextIndex].getValue() <<
" ";
2475template<
typename ValueType>
2477 std::size_t result = 0;
2482 boost::hash_combine(result, boost::hash_range(columnsAndValues.begin(), columnsAndValues.end()));
2483 boost::hash_combine(result, boost::hash_range(rowIndications.begin(), rowIndications.end()));
2485 boost::hash_combine(result, boost::hash_range(rowGroupIndices.get().begin(), rowGroupIndices.get().end()));
2525#if defined(STORM_HAVE_CLN)
2538#if defined(STORM_HAVE_GMP)
Helper class that optionally holds a reference to an object of type T.
A bit vector that is internally represented as a vector of 64-bit values.
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.
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.
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.
SparseMatrixIndexType index_type
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
bool isIdentityMatrix() const
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)
#define STORM_LOG_TRACE(message)
#define STORM_LOG_ASSERT(cond, message)
#define STORM_LOG_THROW(cond, exception, message)
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].
bool isPositive(ValueType const &a)
bool isOne(ValueType const &a)
bool isConstant(ValueType const &)
bool isZero(ValueType const &a)
typename detail::IntervalMetaProgrammingHelper< ValueType >::BaseType IntervalBaseType
Helper to access the type in which interval boundaries are stored.