From c8d9ec553509b2c8178ed41fdef21b84a0cb0af2 Mon Sep 17 00:00:00 2001 From: sjunges Date: Mon, 4 Apr 2016 15:43:43 +0200 Subject: [PATCH] update sparse matrix with duplicate row detection within rowgroups Former-commit-id: 282803c02f0dd59e9f55b107ee3f1d2b2ec7788f --- src/storage/SparseMatrix.cpp | 43 ++++++++++++++++++++++++++++++++++++ src/storage/SparseMatrix.h | 15 +++++++++++++ 2 files changed, 58 insertions(+) diff --git a/src/storage/SparseMatrix.cpp b/src/storage/SparseMatrix.cpp index 3dbabf854..abd490330 100644 --- a/src/storage/SparseMatrix.cpp +++ b/src/storage/SparseMatrix.cpp @@ -65,6 +65,17 @@ namespace storm { return MatrixEntry(this->getColumn(), this->getValue() * factor); } + + template + bool MatrixEntry::operator==(MatrixEntry const& other) const { + return this->entry.first == other.entry.first && this->entry.second == other.entry.second; + } + + template + bool MatrixEntry::operator!=(MatrixEntry const& other) const { + return !(*this == other); + } + template std::ostream& operator<<(std::ostream& out, MatrixEntry const& entry) { out << "(" << entry.getColumn() << ", " << entry.getValue() << ")"; @@ -487,6 +498,38 @@ namespace storm { } } + template + bool SparseMatrix::compareRows(index_type i1, index_type i2) const { + const_iterator end1 = this->end(i1); + const_iterator end2 = this->end(i2); + const_iterator it1 = this->begin(i1); + const_iterator it2 = this->begin(i2); + for(;it1 != end1 && it2 != end2; ++it1, ++it2 ) { + if(*it1 != *it2) { + return false; + } + } + if(it1 == end1 && it2 == end2) { + return true; + } + return false; + } + + template + BitVector SparseMatrix::duplicateRowsInRowgroups() const { + BitVector bv(this->getRowCount()); + for(size_t rowgroup = 0; rowgroup < this->getRowGroupCount(); ++rowgroup) { + for(size_t row1 = this->getRowGroupIndices().at(rowgroup); row1 < this->getRowGroupIndices().at(rowgroup+1); ++row1) { + for(size_t row2 = row1; row2 < this->getRowGroupIndices().at(rowgroup+1); ++row2) { + if(compareRows(row1, row2)) { + bv.set(row2); + } + } + } + } + return bv; + } + template ValueType SparseMatrix::getConstrainedRowSum(index_type row, storm::storage::BitVector const& constraint) const { ValueType result = storm::utility::zero(); diff --git a/src/storage/SparseMatrix.h b/src/storage/SparseMatrix.h index f9d9916c4..0df4bea36 100644 --- a/src/storage/SparseMatrix.h +++ b/src/storage/SparseMatrix.h @@ -107,6 +107,9 @@ namespace storm { */ MatrixEntry operator*(value_type factor) const; + bool operator==(MatrixEntry const& other) const; + bool operator!=(MatrixEntry const& other) const; + template friend std::ostream& operator<<(std::ostream& out, MatrixEntry const& entry); private: @@ -628,6 +631,18 @@ namespace storm { */ SparseMatrix restrictRows(storm::storage::BitVector const& rowsToKeep) const; + /** + * Compares two rows. + * @param i1 Index of first row + * @param i2 Index of second row + * @return True if the rows have identical entries. + */ + bool compareRows(index_type i1, index_type i2) const; + /*! + * Finds duplicate rows in a rowgroup. + */ + BitVector duplicateRowsInRowgroups() const; + /*! * Selects exactly one row from each row group of this matrix and returns the resulting matrix. *