diff --git a/src/storage/SparseMatrix.cpp b/src/storage/SparseMatrix.cpp index c43dc77d9..d38b0a838 100644 --- a/src/storage/SparseMatrix.cpp +++ b/src/storage/SparseMatrix.cpp @@ -22,6 +22,8 @@ #include "src/utility/macros.h" +#include + namespace storm { namespace storage { @@ -267,66 +269,37 @@ namespace storm { } template - bool SparseMatrixBuilder::replaceColumns(std::vector const& replacements, index_type offset) { - bool changed = false; + void SparseMatrixBuilder::replaceColumns(std::vector const& replacements, index_type offset) { index_type maxColumn = 0; - for (auto& elem : columnsAndValues) { - if (elem.getColumn() >= offset) { - elem.setColumn(replacements[elem.getColumn() - offset]); - changed = true; - } - maxColumn = std::max(maxColumn, elem.getColumn()); - } - STORM_LOG_ASSERT(changed || highestColumn == maxColumn, "Incorrect maximal column."); - highestColumn = maxColumn; - STORM_LOG_ASSERT(changed || lastColumn == columnsAndValues[columnsAndValues.size() - 1].getColumn(), "Incorrect last column."); - lastColumn = columnsAndValues[columnsAndValues.size() - 1].getColumn(); - - if (changed) { - fixColumns(); - } - return changed; - } - template - void SparseMatrixBuilder::fixColumns() { - // Sort columns per row - typename SparseMatrix::index_type endGroups; - typename SparseMatrix::index_type endRows; - - if (hasCustomRowGrouping) { - for (index_type group = 0; group < rowGroupIndices.get().size(); ++group) { - endGroups = group < rowGroupIndices.get().size()-1 ? rowGroupIndices.get()[group+1] : rowIndications.size(); - for (index_type i = rowGroupIndices.get()[group]; i < endGroups; ++i) { - endRows = i < rowIndications.size()-1 ? rowIndications[i+1] : columnsAndValues.size(); - // Sort the row - std::sort(columnsAndValues.begin() + rowIndications[i], columnsAndValues.begin() + endRows, - [](MatrixEntry const& a, MatrixEntry const& b) { - return a.getColumn() < b.getColumn(); - }); - // Assert no equal elements - STORM_LOG_ASSERT(std::is_sorted(columnsAndValues.begin() + rowIndications[i], columnsAndValues.begin() + endRows, - [](MatrixEntry const& a, MatrixEntry const& b) { - return a.getColumn() <= b.getColumn(); - }), "Columns not sorted."); + for (index_type row = 0; row < rowIndications.size(); ++row) { + bool changed = false; + auto startRow = std::next(columnsAndValues.begin(), rowIndications[row]); + auto endRow = row < rowIndications.size()-1 ? std::next(columnsAndValues.begin(), rowIndications[row+1]) : columnsAndValues.end(); + for (auto entry = startRow; entry != endRow; ++entry) { + if (entry->getColumn() >= offset) { + // Change column + entry->setColumn(replacements[entry->getColumn() - offset]); + changed = true; } + maxColumn = std::max(maxColumn, entry->getColumn()); } - } else { - for (index_type i = 0; i < rowIndications.size(); ++i) { - endRows = i < rowIndications.size()-1 ? rowIndications[i+1] : columnsAndValues.size(); - // Sort the row - std::sort(columnsAndValues.begin() + rowIndications[i], columnsAndValues.begin() + endRows, + if (changed) { + // Sort columns in row + std::sort(startRow, endRow, [](MatrixEntry const& a, MatrixEntry const& b) { return a.getColumn() < b.getColumn(); }); // Assert no equal elements - STORM_LOG_ASSERT(std::is_sorted(columnsAndValues.begin() + rowIndications[i], columnsAndValues.begin() + endRows, - [](MatrixEntry const& a, MatrixEntry const& b) { - return a.getColumn() <= b.getColumn(); - }), "Columns not sorted."); + STORM_LOG_ASSERT(std::is_sorted(startRow, endRow, + [](MatrixEntry const& a, MatrixEntry const& b) { + return a.getColumn() < b.getColumn(); + }), "Columns not sorted."); } - } + + highestColumn = maxColumn; + lastColumn = columnsAndValues[columnsAndValues.size() - 1].getColumn(); } template diff --git a/src/storage/SparseMatrix.h b/src/storage/SparseMatrix.h index c170d43a9..5d9f48fe9 100644 --- a/src/storage/SparseMatrix.h +++ b/src/storage/SparseMatrix.h @@ -230,9 +230,8 @@ namespace storm { * * @param replacements Mapping indicating the replacements from offset+i -> value of i. * @param offset Offset to add to each id in vector index. - * @return True if replacement took place, False if nothing changed. */ - bool replaceColumns(std::vector const& replacements, index_type offset); + void replaceColumns(std::vector const& replacements, index_type offset); private: // A flag indicating whether a row count was set upon construction. @@ -295,11 +294,6 @@ namespace storm { // Stores the currently active row group. This is used for correctly constructing the row grouping of the // matrix. index_type currentRowGroup; - - /*! - * Fixes the matrix by sorting the columns to gain increasing order again. - */ - void fixColumns(); }; /*!