|
|
|
@ -35,19 +35,19 @@ namespace storm { |
|
|
|
namespace storm { |
|
|
|
namespace storage { |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
// Forward declare matrix class. |
|
|
|
template<typename T> |
|
|
|
class SparseMatrix; |
|
|
|
|
|
|
|
|
|
|
|
typedef uint_fast64_t SparseMatrixIndexType; |
|
|
|
|
|
|
|
|
|
|
|
template<typename IndexType, typename ValueType> |
|
|
|
class MatrixEntry { |
|
|
|
public: |
|
|
|
typedef IndexType index_type; |
|
|
|
typedef ValueType value_type; |
|
|
|
|
|
|
|
|
|
|
|
/*! |
|
|
|
* Constructs a matrix entry with the given column and value. |
|
|
|
* |
|
|
|
@ -55,14 +55,14 @@ namespace storm { |
|
|
|
* @param value The value of the matrix entry. |
|
|
|
*/ |
|
|
|
MatrixEntry(index_type column, value_type value); |
|
|
|
|
|
|
|
|
|
|
|
/*! |
|
|
|
* Move-constructs the matrix entry fro the given column-value pair. |
|
|
|
* |
|
|
|
* @param pair The column-value pair from which to move-construct the matrix entry. |
|
|
|
*/ |
|
|
|
MatrixEntry(std::pair<index_type, value_type>&& pair); |
|
|
|
|
|
|
|
|
|
|
|
MatrixEntry() = default; |
|
|
|
MatrixEntry(MatrixEntry const& other) = default; |
|
|
|
MatrixEntry& operator=(MatrixEntry const& other) = default; |
|
|
|
@ -70,59 +70,59 @@ namespace storm { |
|
|
|
MatrixEntry(MatrixEntry&& other) = default; |
|
|
|
MatrixEntry& operator=(MatrixEntry&& other) = default; |
|
|
|
#endif |
|
|
|
|
|
|
|
|
|
|
|
/*! |
|
|
|
* Retrieves the column of the matrix entry. |
|
|
|
* |
|
|
|
* @return The column of the matrix entry. |
|
|
|
*/ |
|
|
|
index_type const& getColumn() const; |
|
|
|
|
|
|
|
|
|
|
|
/*! |
|
|
|
* Sets the column of the current entry. |
|
|
|
* |
|
|
|
* @param column The column to set for this entry. |
|
|
|
*/ |
|
|
|
void setColumn(index_type const& column); |
|
|
|
|
|
|
|
|
|
|
|
/*! |
|
|
|
* Retrieves the value of the matrix entry. |
|
|
|
* |
|
|
|
* @return The value of the matrix entry. |
|
|
|
*/ |
|
|
|
value_type const& getValue() const; |
|
|
|
|
|
|
|
|
|
|
|
/*! |
|
|
|
* Sets the value of the entry in the matrix. |
|
|
|
* |
|
|
|
* @param value The value that is to be set for this entry. |
|
|
|
*/ |
|
|
|
void setValue(value_type const& value); |
|
|
|
|
|
|
|
|
|
|
|
/*! |
|
|
|
* Retrieves a pair of column and value that characterizes this entry. |
|
|
|
* |
|
|
|
* @return A column-value pair that characterizes this entry. |
|
|
|
*/ |
|
|
|
std::pair<index_type, value_type> const& getColumnValuePair() const; |
|
|
|
|
|
|
|
|
|
|
|
/*! |
|
|
|
* Multiplies the entry with the given factor and returns the result. |
|
|
|
* |
|
|
|
* @param factor The factor with which to multiply the entry. |
|
|
|
*/ |
|
|
|
MatrixEntry operator*(value_type factor) const; |
|
|
|
|
|
|
|
|
|
|
|
bool operator==(MatrixEntry const& other) const; |
|
|
|
bool operator!=(MatrixEntry const& other) const; |
|
|
|
|
|
|
|
|
|
|
|
template<typename IndexTypePrime, typename ValueTypePrime> |
|
|
|
friend std::ostream& operator<<(std::ostream& out, MatrixEntry<IndexTypePrime, ValueTypePrime> const& entry); |
|
|
|
private: |
|
|
|
// The actual matrix entry. |
|
|
|
std::pair<index_type, value_type> entry; |
|
|
|
}; |
|
|
|
|
|
|
|
|
|
|
|
/*! |
|
|
|
* Computes the hash value of a matrix entry. |
|
|
|
*/ |
|
|
|
@ -133,7 +133,7 @@ namespace storm { |
|
|
|
boost::hash_combine(seed, matrixEntry.getValue()); |
|
|
|
return seed; |
|
|
|
} |
|
|
|
|
|
|
|
|
|
|
|
/*! |
|
|
|
* A class that can be used to build a sparse matrix by adding value by value. |
|
|
|
*/ |
|
|
|
@ -142,7 +142,7 @@ namespace storm { |
|
|
|
public: |
|
|
|
typedef SparseMatrixIndexType index_type; |
|
|
|
typedef ValueType value_type; |
|
|
|
|
|
|
|
|
|
|
|
/*! |
|
|
|
* Constructs a sparse matrix builder producing a matrix with the given number of rows, columns and entries. |
|
|
|
* The number of rows, columns and entries is reserved upon creation. If more rows/columns or entries are |
|
|
|
@ -159,7 +159,7 @@ namespace storm { |
|
|
|
* has a custom row grouping. |
|
|
|
*/ |
|
|
|
SparseMatrixBuilder(index_type rows = 0, index_type columns = 0, index_type entries = 0, bool forceDimensions = true, bool hasCustomRowGrouping = false, index_type rowGroups = 0); |
|
|
|
|
|
|
|
|
|
|
|
/*! |
|
|
|
* Moves the contents of the given matrix into the matrix builder so that its contents can be modified again. |
|
|
|
* This is, for example, useful if rows need to be added to the matrix. |
|
|
|
@ -167,7 +167,7 @@ namespace storm { |
|
|
|
* @param matrix The matrix that is to be made editable again. |
|
|
|
*/ |
|
|
|
SparseMatrixBuilder(SparseMatrix<ValueType>&& matrix); |
|
|
|
|
|
|
|
|
|
|
|
/*! |
|
|
|
* Sets the matrix entry at the given row and column to the given value. After all entries have been added, |
|
|
|
* a call to finalize(false) is mandatory. |
|
|
|
@ -182,7 +182,7 @@ namespace storm { |
|
|
|
* @param value The value that is to be set at the specified row and column. |
|
|
|
*/ |
|
|
|
void addNextValue(index_type row, index_type column, value_type const& value); |
|
|
|
|
|
|
|
|
|
|
|
/*! |
|
|
|
* Starts a new row group in the matrix. Note that this needs to be called before any entries in the new row |
|
|
|
* group are added. |
|
|
|
@ -190,7 +190,7 @@ namespace storm { |
|
|
|
* @param startingRow The starting row of the new row group. |
|
|
|
*/ |
|
|
|
void newRowGroup(index_type startingRow); |
|
|
|
|
|
|
|
|
|
|
|
/* |
|
|
|
* Finalizes the sparse matrix to indicate that initialization process has been completed and the matrix |
|
|
|
* may now be used. This must be called after all entries have been added to the matrix via addNextValue. |
|
|
|
@ -211,10 +211,10 @@ namespace storm { |
|
|
|
* groups added this way will be empty. |
|
|
|
*/ |
|
|
|
SparseMatrix<value_type> build(index_type overriddenRowCount = 0, index_type overriddenColumnCount = 0, index_type overriddenRowGroupCount = 0); |
|
|
|
|
|
|
|
|
|
|
|
/*! |
|
|
|
* Retrieves the most recently used row. |
|
|
|
* |
|
|
|
* |
|
|
|
* @return The most recently used row. |
|
|
|
*/ |
|
|
|
index_type getLastRow() const; |
|
|
|
@ -232,7 +232,7 @@ namespace storm { |
|
|
|
* @return The most recently used row. |
|
|
|
*/ |
|
|
|
index_type getLastColumn() const; |
|
|
|
|
|
|
|
|
|
|
|
/*! |
|
|
|
* Replaces all columns with id > offset according to replacements. |
|
|
|
* Every state with id offset+i is replaced by the id in replacements[i]. |
|
|
|
@ -242,7 +242,7 @@ namespace storm { |
|
|
|
* @param offset Offset to add to each id in vector index. |
|
|
|
*/ |
|
|
|
void replaceColumns(std::vector<index_type> const& replacements, index_type offset); |
|
|
|
|
|
|
|
|
|
|
|
/*! |
|
|
|
* Makes sure that a diagonal entry will be inserted at the given row. |
|
|
|
* All other entries of this row must be set immediately after calling this (without setting values at other rows in between) |
|
|
|
@ -251,72 +251,72 @@ namespace storm { |
|
|
|
* If addNextValue is called on the given row and the diagonal column, we take the sum of the two values provided to addDiagonalEntry and addNextValue |
|
|
|
*/ |
|
|
|
void addDiagonalEntry(index_type row, ValueType const& value); |
|
|
|
|
|
|
|
|
|
|
|
private: |
|
|
|
// A flag indicating whether a row count was set upon construction. |
|
|
|
bool initialRowCountSet; |
|
|
|
|
|
|
|
|
|
|
|
// The row count that was initially set (if any). |
|
|
|
index_type initialRowCount; |
|
|
|
|
|
|
|
|
|
|
|
// A flag indicating whether a column count was set upon construction. |
|
|
|
bool initialColumnCountSet; |
|
|
|
|
|
|
|
// The column count that was initially set (if any). |
|
|
|
index_type initialColumnCount; |
|
|
|
|
|
|
|
|
|
|
|
// A flag indicating whether an entry count was set upon construction. |
|
|
|
bool initialEntryCountSet; |
|
|
|
|
|
|
|
|
|
|
|
// The number of entries in the matrix. |
|
|
|
index_type initialEntryCount; |
|
|
|
|
|
|
|
|
|
|
|
// A flag indicating whether the initially given dimensions are to be enforced on the resulting matrix. |
|
|
|
bool forceInitialDimensions; |
|
|
|
|
|
|
|
|
|
|
|
// A flag indicating whether the builder is to construct a custom row grouping for the matrix. |
|
|
|
bool hasCustomRowGrouping; |
|
|
|
|
|
|
|
|
|
|
|
// A flag indicating whether the number of row groups was set upon construction. |
|
|
|
bool initialRowGroupCountSet; |
|
|
|
|
|
|
|
|
|
|
|
// The number of row groups in the matrix. |
|
|
|
index_type initialRowGroupCount; |
|
|
|
|
|
|
|
|
|
|
|
// The vector that stores the row-group indices (if they are non-trivial). |
|
|
|
boost::optional<std::vector<index_type>> rowGroupIndices; |
|
|
|
|
|
|
|
|
|
|
|
// The storage for the columns and values of all entries in the matrix. |
|
|
|
std::vector<MatrixEntry<index_type, value_type>> columnsAndValues; |
|
|
|
|
|
|
|
|
|
|
|
// A vector containing the indices at which each given row begins. This index is to be interpreted as an |
|
|
|
// index in the valueStorage and the columnIndications vectors. Put differently, the values of the entries |
|
|
|
// in row i are valueStorage[rowIndications[i]] to valueStorage[rowIndications[i + 1]] where the last |
|
|
|
// entry is not included anymore. |
|
|
|
std::vector<index_type> rowIndications; |
|
|
|
|
|
|
|
|
|
|
|
// Stores the current number of entries in the matrix. This is used for inserting an entry into a matrix |
|
|
|
// with preallocated storage. |
|
|
|
index_type currentEntryCount; |
|
|
|
|
|
|
|
|
|
|
|
// Stores the row of the last entry in the matrix. This is used for correctly inserting an entry into a |
|
|
|
// matrix. |
|
|
|
index_type lastRow; |
|
|
|
|
|
|
|
|
|
|
|
// Stores the column of the currently last entry in the matrix. This is used for correctly inserting an |
|
|
|
// entry into a matrix. |
|
|
|
index_type lastColumn; |
|
|
|
|
|
|
|
|
|
|
|
// Stores the highest column at which an entry was inserted into the matrix. |
|
|
|
index_type highestColumn; |
|
|
|
|
|
|
|
|
|
|
|
// Stores the currently active row group. This is used for correctly constructing the row grouping of the |
|
|
|
// matrix. |
|
|
|
index_type currentRowGroupCount; |
|
|
|
|
|
|
|
|
|
|
|
boost::optional<ValueType> pendingDiagonalEntry; |
|
|
|
}; |
|
|
|
|
|
|
|
|
|
|
|
/*! |
|
|
|
* A class that holds a possibly non-square matrix in the compressed row storage format. That is, it is supposed |
|
|
|
* to store non-zero entries only, but zeros may be explicitly stored if necessary for certain operations. |
|
|
|
@ -340,12 +340,12 @@ namespace storm { |
|
|
|
friend class storm::adapters::StormAdapter; |
|
|
|
friend class storm::solver::TopologicalCudaValueIterationMinMaxLinearEquationSolver<ValueType>; |
|
|
|
friend class SparseMatrixBuilder<ValueType>; |
|
|
|
|
|
|
|
|
|
|
|
typedef SparseMatrixIndexType index_type; |
|
|
|
typedef ValueType value_type; |
|
|
|
typedef typename std::vector<MatrixEntry<index_type, value_type>>::iterator iterator; |
|
|
|
typedef typename std::vector<MatrixEntry<index_type, value_type>>::const_iterator const_iterator; |
|
|
|
|
|
|
|
|
|
|
|
/*! |
|
|
|
* This class represents a number of consecutive rows of the matrix. |
|
|
|
*/ |
|
|
|
@ -359,32 +359,32 @@ namespace storm { |
|
|
|
* @param entryCount The number of entrys in the rows. |
|
|
|
*/ |
|
|
|
rows(iterator begin, index_type entryCount); |
|
|
|
|
|
|
|
|
|
|
|
/*! |
|
|
|
* Retrieves an iterator that points to the beginning of the rows. |
|
|
|
* |
|
|
|
* @return An iterator that points to the beginning of the rows. |
|
|
|
*/ |
|
|
|
iterator begin(); |
|
|
|
|
|
|
|
|
|
|
|
/*! |
|
|
|
* Retrieves an iterator that points past the last entry of the rows. |
|
|
|
* |
|
|
|
* @return An iterator that points past the last entry of the rows. |
|
|
|
*/ |
|
|
|
iterator end(); |
|
|
|
|
|
|
|
|
|
|
|
/*! |
|
|
|
* Retrieves the number of entries in the rows. |
|
|
|
* |
|
|
|
* @return The number of entries in the rows. |
|
|
|
*/ |
|
|
|
index_type getNumberOfEntries() const; |
|
|
|
|
|
|
|
|
|
|
|
private: |
|
|
|
// The pointer to the columnd and value of the first entry. |
|
|
|
iterator beginIterator; |
|
|
|
|
|
|
|
|
|
|
|
// The number of non-zero entries in the rows. |
|
|
|
index_type entryCount; |
|
|
|
}; |
|
|
|
@ -402,55 +402,55 @@ namespace storm { |
|
|
|
* @param entryCount The number of entrys in the rows. |
|
|
|
*/ |
|
|
|
const_rows(const_iterator begin, index_type entryCount); |
|
|
|
|
|
|
|
|
|
|
|
/*! |
|
|
|
* Retrieves an iterator that points to the beginning of the rows. |
|
|
|
* |
|
|
|
* @return An iterator that points to the beginning of the rows. |
|
|
|
*/ |
|
|
|
const_iterator begin() const; |
|
|
|
|
|
|
|
|
|
|
|
/*! |
|
|
|
* Retrieves an iterator that points past the last entry of the rows. |
|
|
|
* |
|
|
|
* @return An iterator that points past the last entry of the rows. |
|
|
|
*/ |
|
|
|
const_iterator end() const; |
|
|
|
|
|
|
|
|
|
|
|
/*! |
|
|
|
* Retrieves the number of entries in the rows. |
|
|
|
* |
|
|
|
* @return The number of entries in the rows. |
|
|
|
*/ |
|
|
|
index_type getNumberOfEntries() const; |
|
|
|
|
|
|
|
|
|
|
|
private: |
|
|
|
// The pointer to the column and value of the first entry. |
|
|
|
const_iterator beginIterator; |
|
|
|
|
|
|
|
|
|
|
|
// The number of non-zero entries in the rows. |
|
|
|
index_type entryCount; |
|
|
|
}; |
|
|
|
|
|
|
|
|
|
|
|
/*! |
|
|
|
* An enum representing the internal state of the matrix. After creation, the matrix is UNINITIALIZED. |
|
|
|
* Only after a call to finalize(), the status of the matrix is set to INITIALIZED and the matrix can be |
|
|
|
* used. |
|
|
|
*/ |
|
|
|
enum MatrixStatus { UNINITIALIZED, INITIALIZED }; |
|
|
|
|
|
|
|
|
|
|
|
/*! |
|
|
|
* Constructs an empty sparse matrix. |
|
|
|
*/ |
|
|
|
SparseMatrix(); |
|
|
|
|
|
|
|
|
|
|
|
/*! |
|
|
|
* Constructs a sparse matrix by performing a deep-copy of the given matrix. |
|
|
|
* |
|
|
|
* @param other The matrix from which to copy the content. |
|
|
|
*/ |
|
|
|
SparseMatrix(SparseMatrix<value_type> const& other); |
|
|
|
|
|
|
|
|
|
|
|
/*! |
|
|
|
* Constructs a sparse matrix by performing a deep-copy of the given matrix. |
|
|
|
* |
|
|
|
@ -459,14 +459,14 @@ namespace storm { |
|
|
|
* exist in the original matrix, they are inserted and set to value zero. |
|
|
|
*/ |
|
|
|
SparseMatrix(SparseMatrix<value_type> const& other, bool insertDiagonalElements); |
|
|
|
|
|
|
|
|
|
|
|
/*! |
|
|
|
* Constructs a sparse matrix by moving the contents of the given matrix to the newly created one. |
|
|
|
* |
|
|
|
* @param other The matrix from which to move the content. |
|
|
|
*/ |
|
|
|
SparseMatrix(SparseMatrix<value_type>&& other); |
|
|
|
|
|
|
|
|
|
|
|
/*! |
|
|
|
* Constructs a sparse matrix by copying the given contents. |
|
|
|
* |
|
|
|
@ -476,7 +476,7 @@ namespace storm { |
|
|
|
* @param rowGroupIndices The vector representing the row groups in the matrix. |
|
|
|
*/ |
|
|
|
SparseMatrix(index_type columnCount, std::vector<index_type> const& rowIndications, std::vector<MatrixEntry<index_type, value_type>> const& columnsAndValues, boost::optional<std::vector<index_type>> const& rowGroupIndices); |
|
|
|
|
|
|
|
|
|
|
|
/*! |
|
|
|
* Constructs a sparse matrix by moving the given contents. |
|
|
|
* |
|
|
|
@ -493,14 +493,14 @@ namespace storm { |
|
|
|
* @param other The matrix from which to copy-assign. |
|
|
|
*/ |
|
|
|
SparseMatrix<value_type>& operator=(SparseMatrix<value_type> const& other); |
|
|
|
|
|
|
|
|
|
|
|
/*! |
|
|
|
* Assigns the contents of the given matrix to the current one by moving its contents. |
|
|
|
* |
|
|
|
* @param other The matrix from which to move to contents. |
|
|
|
*/ |
|
|
|
SparseMatrix<value_type>& operator=(SparseMatrix<value_type>&& other); |
|
|
|
|
|
|
|
|
|
|
|
/*! |
|
|
|
* Determines whether the current and the given matrix are semantically equal. |
|
|
|
* |
|
|
|
@ -508,28 +508,28 @@ namespace storm { |
|
|
|
* @return True iff the given matrix is semantically equal to the current one. |
|
|
|
*/ |
|
|
|
bool operator==(SparseMatrix<value_type> const& other) const; |
|
|
|
|
|
|
|
|
|
|
|
/*! |
|
|
|
* Returns the number of rows of the matrix. |
|
|
|
* |
|
|
|
* @return The number of rows of the matrix. |
|
|
|
*/ |
|
|
|
index_type getRowCount() const; |
|
|
|
|
|
|
|
|
|
|
|
/*! |
|
|
|
* Returns the number of columns of the matrix. |
|
|
|
* |
|
|
|
* @return The number of columns of the matrix. |
|
|
|
*/ |
|
|
|
index_type getColumnCount() const; |
|
|
|
|
|
|
|
|
|
|
|
/*! |
|
|
|
* Returns the number of entries in the matrix. |
|
|
|
* |
|
|
|
* @return The number of entries in the matrix. |
|
|
|
*/ |
|
|
|
index_type getEntryCount() const; |
|
|
|
|
|
|
|
|
|
|
|
/*! |
|
|
|
* Returns the number of entries in the given row group of the matrix. |
|
|
|
* |
|
|
|
@ -550,7 +550,7 @@ namespace storm { |
|
|
|
* Recompute the nonzero entry count |
|
|
|
*/ |
|
|
|
void updateNonzeroEntryCount() const; |
|
|
|
|
|
|
|
|
|
|
|
/*! |
|
|
|
* Recomputes the number of columns and the number of non-zero entries. |
|
|
|
*/ |
|
|
|
@ -562,14 +562,14 @@ namespace storm { |
|
|
|
* @param difference Difference between old and new nonzero entry count. |
|
|
|
*/ |
|
|
|
void updateNonzeroEntryCount(std::make_signed<index_type>::type difference); |
|
|
|
|
|
|
|
|
|
|
|
/*! |
|
|
|
* Returns the number of row groups in the matrix. |
|
|
|
* |
|
|
|
* @return The number of row groups in the matrix. |
|
|
|
*/ |
|
|
|
index_type getRowGroupCount() const; |
|
|
|
|
|
|
|
|
|
|
|
/*! |
|
|
|
* Returns the size of the given row group. |
|
|
|
* |
|
|
|
@ -577,31 +577,31 @@ namespace storm { |
|
|
|
* @return The number of rows that belong to the given row group. |
|
|
|
*/ |
|
|
|
index_type getRowGroupSize(index_type group) const; |
|
|
|
|
|
|
|
|
|
|
|
/*! |
|
|
|
* Returns the size of the largest row group of the matrix |
|
|
|
*/ |
|
|
|
index_type getSizeOfLargestRowGroup() const; |
|
|
|
|
|
|
|
|
|
|
|
/*! |
|
|
|
* Returns the total number of rows that are in one of the specified row groups. |
|
|
|
*/ |
|
|
|
index_type getNumRowsInRowGroups(storm::storage::BitVector const& groupConstraint) const; |
|
|
|
|
|
|
|
|
|
|
|
/*! |
|
|
|
* Returns the grouping of rows of this matrix. |
|
|
|
* |
|
|
|
* @return The grouping of rows of this matrix. |
|
|
|
*/ |
|
|
|
std::vector<index_type> const& getRowGroupIndices() const; |
|
|
|
|
|
|
|
|
|
|
|
/*! |
|
|
|
* Swaps the grouping of rows of this matrix. |
|
|
|
* |
|
|
|
* @return The old grouping of rows of this matrix. |
|
|
|
*/ |
|
|
|
std::vector<index_type> swapRowGroupIndices(std::vector<index_type>&& newRowGrouping); |
|
|
|
|
|
|
|
|
|
|
|
/*! |
|
|
|
* Sets the row grouping to the given one. |
|
|
|
* @note It is assumed that the new row grouping is non-trivial. |
|
|
|
@ -609,14 +609,14 @@ namespace storm { |
|
|
|
* @param newRowGroupIndices The new row group indices. |
|
|
|
*/ |
|
|
|
void setRowGroupIndices(std::vector<index_type> const& newRowGroupIndices); |
|
|
|
|
|
|
|
|
|
|
|
/*! |
|
|
|
* Retrieves whether the matrix has a trivial row grouping. |
|
|
|
* |
|
|
|
* @return True iff the matrix has a trivial row grouping. |
|
|
|
*/ |
|
|
|
bool hasTrivialRowGrouping() const; |
|
|
|
|
|
|
|
|
|
|
|
/*! |
|
|
|
* Makes the row grouping of this matrix trivial. |
|
|
|
* Has no effect when the row grouping is already trivial. |
|
|
|
@ -630,7 +630,7 @@ namespace storm { |
|
|
|
* @return a bit vector that is true at position i iff the row group of row i is selected. |
|
|
|
*/ |
|
|
|
storm::storage::BitVector getRowFilter(storm::storage::BitVector const& groupConstraint) const; |
|
|
|
|
|
|
|
|
|
|
|
/*! |
|
|
|
* Returns the indices of all rows that |
|
|
|
* * are in a selected group and |
|
|
|
@ -641,7 +641,7 @@ namespace storm { |
|
|
|
* @return a bit vector that is true at position i iff row i satisfies the constraints. |
|
|
|
*/ |
|
|
|
storm::storage::BitVector getRowFilter(storm::storage::BitVector const& groupConstraint, storm::storage::BitVector const& columnConstraints) const; |
|
|
|
|
|
|
|
|
|
|
|
/*! |
|
|
|
* Returns the indices of all row groups selected by the row constraints |
|
|
|
* |
|
|
|
@ -650,21 +650,21 @@ namespace storm { |
|
|
|
* @return a bit vector that is true at position i iff row i satisfies the constraints. |
|
|
|
*/ |
|
|
|
storm::storage::BitVector getRowGroupFilter(storm::storage::BitVector const& rowConstraint, bool setIfForAllRowsInGroup) const; |
|
|
|
|
|
|
|
|
|
|
|
/*! |
|
|
|
* This function makes the given rows absorbing. |
|
|
|
* |
|
|
|
* @param rows A bit vector indicating which rows are to be made absorbing. |
|
|
|
*/ |
|
|
|
void makeRowsAbsorbing(storm::storage::BitVector const& rows); |
|
|
|
|
|
|
|
|
|
|
|
/*! |
|
|
|
* This function makes the groups of rows given by the bit vector absorbing. |
|
|
|
* |
|
|
|
* @param rowGroupConstraint A bit vector indicating which row groups to make absorbing. |
|
|
|
*/ |
|
|
|
void makeRowGroupsAbsorbing(storm::storage::BitVector const& rowGroupConstraint); |
|
|
|
|
|
|
|
|
|
|
|
/*! |
|
|
|
* This function makes the given row Dirac. This means that all entries will be set to 0 except the one |
|
|
|
* at the specified column, which is set to 1 instead. |
|
|
|
@ -673,14 +673,14 @@ namespace storm { |
|
|
|
* @param column The index of the column whose value is to be set to 1. |
|
|
|
*/ |
|
|
|
void makeRowDirac(index_type row, index_type column); |
|
|
|
|
|
|
|
|
|
|
|
/* |
|
|
|
* Sums the entries in all rows. |
|
|
|
* |
|
|
|
* @return The vector of sums of the entries in the respective rows. |
|
|
|
*/ |
|
|
|
std::vector<ValueType> getRowSumVector() const; |
|
|
|
|
|
|
|
|
|
|
|
/* |
|
|
|
* Sums the entries in the given row and columns. |
|
|
|
* |
|
|
|
@ -689,7 +689,7 @@ namespace storm { |
|
|
|
* @return The sum of the entries in the given row and columns. |
|
|
|
*/ |
|
|
|
value_type getConstrainedRowSum(index_type row, storm::storage::BitVector const& columns) const; |
|
|
|
|
|
|
|
|
|
|
|
/*! |
|
|
|
* Computes a vector whose i-th entry is the sum of the entries in the i-th selected row where only those |
|
|
|
* entries are added that are in selected columns. |
|
|
|
@ -700,7 +700,7 @@ namespace storm { |
|
|
|
* @return A vector whose elements are the sums of the selected columns in each row. |
|
|
|
*/ |
|
|
|
std::vector<value_type> getConstrainedRowSumVector(storm::storage::BitVector const& rowConstraint, storm::storage::BitVector const& columnConstraint) const; |
|
|
|
|
|
|
|
|
|
|
|
/*! |
|
|
|
* Computes a vector whose entries represent the sums of selected columns for all rows in selected row |
|
|
|
* groups. |
|
|
|
@ -711,7 +711,7 @@ namespace storm { |
|
|
|
* groups. |
|
|
|
*/ |
|
|
|
std::vector<value_type> getConstrainedRowGroupSumVector(storm::storage::BitVector const& rowGroupConstraint, storm::storage::BitVector const& columnConstraint) const; |
|
|
|
|
|
|
|
|
|
|
|
/*! |
|
|
|
* Creates a submatrix of the current matrix by dropping all rows and columns whose bits are not |
|
|
|
* set to one in the given bit vector. |
|
|
|
@ -728,10 +728,10 @@ namespace storm { |
|
|
|
* by the constraints are kept and all others are dropped. |
|
|
|
*/ |
|
|
|
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; |
|
|
|
|
|
|
|
|
|
|
|
/*! |
|
|
|
* Restrict rows in grouped rows matrix. Ensures that the number of groups stays the same. |
|
|
|
* |
|
|
|
* Restrict rows in grouped rows matrix. Ensures that the number of groups stays the same. |
|
|
|
* |
|
|
|
* @param rowsToKeep A bit vector indicating which rows to keep. |
|
|
|
* @param allowEmptyRowGroups if set to true, the result can potentially have empty row groups. |
|
|
|
* Otherwise, it is asserted that there are no empty row groups. |
|
|
|
@ -757,7 +757,7 @@ namespace storm { |
|
|
|
* @param rowFilter the selected rows |
|
|
|
*/ |
|
|
|
SparseMatrix filterEntries(storm::storage::BitVector const& rowFilter) const; |
|
|
|
|
|
|
|
|
|
|
|
/*! |
|
|
|
* Removes all zero entries from this. |
|
|
|
*/ |
|
|
|
@ -770,19 +770,19 @@ namespace storm { |
|
|
|
* @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; |
|
|
|
|
|
|
|
|
|
|
|
/** |
|
|
|
* Swaps the two rows. |
|
|
|
* @param row1 Index of first row |
|
|
|
* @param row2 Index of second row |
|
|
|
*/ |
|
|
|
void swapRows(index_type const& row1, index_type const& row2); |
|
|
|
|
|
|
|
|
|
|
|
/*! |
|
|
|
* Selects exactly one row from each row group of this matrix and returns the resulting matrix. |
|
|
|
* |
|
|
|
@ -791,7 +791,7 @@ namespace storm { |
|
|
|
* @return A submatrix of the current matrix by selecting one row out of each row group. |
|
|
|
*/ |
|
|
|
SparseMatrix selectRowsFromRowGroups(std::vector<index_type> const& rowGroupToRowIndexMapping, bool insertDiagonalEntries = true) const; |
|
|
|
|
|
|
|
|
|
|
|
/*! |
|
|
|
* Selects the rows that are given by the sequence of row indices, allowing to select rows arbitrarily often and with an arbitrary order |
|
|
|
* The resulting matrix will have a trivial row grouping. |
|
|
|
@ -802,7 +802,7 @@ namespace storm { |
|
|
|
* @return A matrix which rows are selected from this matrix according to the given index sequence |
|
|
|
*/ |
|
|
|
SparseMatrix selectRowsFromRowIndexSequence(std::vector<index_type> const& rowIndexSequence, bool insertDiagonalEntries = true) const; |
|
|
|
|
|
|
|
|
|
|
|
/*! |
|
|
|
* Transposes the matrix. |
|
|
|
* |
|
|
|
@ -812,7 +812,7 @@ namespace storm { |
|
|
|
* @return A sparse matrix that represents the transpose of this matrix. |
|
|
|
*/ |
|
|
|
storm::storage::SparseMatrix<value_type> transpose(bool joinGroups = false, bool keepZeros = false) const; |
|
|
|
|
|
|
|
|
|
|
|
/*! |
|
|
|
* Transposes the matrix w.r.t. the selected rows. |
|
|
|
* This is equivalent to selectRowsFromRowGroups(rowGroupChoices, false).transpose(false, keepZeros) but avoids creating one intermediate matrix. |
|
|
|
@ -822,7 +822,7 @@ namespace storm { |
|
|
|
* |
|
|
|
*/ |
|
|
|
SparseMatrix<ValueType> transposeSelectedRowsFromRowGroups(std::vector<uint_fast64_t> const& rowGroupChoices, bool keepZeros = false) const; |
|
|
|
|
|
|
|
|
|
|
|
/*! |
|
|
|
* Transforms the matrix into an equation system. That is, it transforms the matrix A into a matrix (1-A). |
|
|
|
*/ |
|
|
|
@ -833,24 +833,24 @@ namespace storm { |
|
|
|
* Requires the matrix to contain each diagonal entry and to be square. |
|
|
|
*/ |
|
|
|
void invertDiagonal(); |
|
|
|
|
|
|
|
|
|
|
|
/*! |
|
|
|
* Negates (w.r.t. addition) all entries that are not on the diagonal. |
|
|
|
*/ |
|
|
|
void negateAllNonDiagonalEntries(); |
|
|
|
|
|
|
|
|
|
|
|
/*! |
|
|
|
* Sets all diagonal elements to zero. |
|
|
|
*/ |
|
|
|
void deleteDiagonalEntries(); |
|
|
|
|
|
|
|
|
|
|
|
/*! |
|
|
|
* Calculates the Jacobi decomposition of this sparse matrix. For this operation, the matrix must be square. |
|
|
|
* |
|
|
|
* @return A pair (L+U, D^-1) containing the matrix L+U and the inverted diagonal D^-1 (as a vector). |
|
|
|
*/ |
|
|
|
std::pair<storm::storage::SparseMatrix<value_type>, std::vector<value_type>> getJacobiDecomposition() const; |
|
|
|
|
|
|
|
|
|
|
|
/*! |
|
|
|
* Performs a pointwise multiplication of the entries in the given row of this matrix and the entries of |
|
|
|
* the given row of the other matrix and returns the sum. |
|
|
|
@ -862,8 +862,8 @@ namespace storm { |
|
|
|
*/ |
|
|
|
template<typename OtherValueType, typename ResultValueType = OtherValueType> |
|
|
|
ResultValueType getPointwiseProductRowSum(storm::storage::SparseMatrix<OtherValueType> const& otherMatrix, index_type const& row) const; |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
/*! |
|
|
|
* Performs a pointwise matrix multiplication of the matrix with the given matrix and returns a vector |
|
|
|
* containing the sum of the entries in each row of the resulting matrix. |
|
|
|
@ -876,7 +876,7 @@ namespace storm { |
|
|
|
*/ |
|
|
|
template<typename OtherValueType, typename ResultValueType = OtherValueType> |
|
|
|
std::vector<ResultValueType> getPointwiseProductRowSumVector(storm::storage::SparseMatrix<OtherValueType> const& otherMatrix) const; |
|
|
|
|
|
|
|
|
|
|
|
/*! |
|
|
|
* Multiplies the matrix with the given vector and writes the result to the given result vector. |
|
|
|
* |
|
|
|
@ -886,13 +886,13 @@ namespace storm { |
|
|
|
* @return The product of the matrix and the given vector as the content of the given result vector. |
|
|
|
*/ |
|
|
|
void multiplyWithVector(std::vector<value_type> const& vector, std::vector<value_type>& result, std::vector<value_type> const* summand = nullptr) const; |
|
|
|
|
|
|
|
|
|
|
|
void multiplyWithVectorForward(std::vector<value_type> const& vector, std::vector<value_type>& result, std::vector<value_type> const* summand = nullptr) const; |
|
|
|
void multiplyWithVectorBackward(std::vector<value_type> const& vector, std::vector<value_type>& result, std::vector<value_type> const* summand = nullptr) const; |
|
|
|
#ifdef STORM_HAVE_INTELTBB |
|
|
|
void multiplyWithVectorParallel(std::vector<value_type> const& vector, std::vector<value_type>& result, std::vector<value_type> const* summand = nullptr) const; |
|
|
|
#endif |
|
|
|
|
|
|
|
|
|
|
|
/*! |
|
|
|
* Multiplies the matrix with the given vector, reduces it according to the given direction and and writes |
|
|
|
* the result to the given result vector. |
|
|
|
@ -907,19 +907,19 @@ namespace storm { |
|
|
|
* the 'new' choice has a value strictly better (wrt. to the optimization direction) value. |
|
|
|
* @return The resulting vector the content of the given result vector. |
|
|
|
*/ |
|
|
|
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<uint_fast64_t>* choices, storm::storage::BitVector* dirOverride = nullptr) const; |
|
|
|
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<uint_fast64_t>* choices, storm::storage::BitVector const* dirOverride = nullptr) const; |
|
|
|
|
|
|
|
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<uint_fast64_t>* choices, storm::storage::BitVector* dirOverride = nullptr) const; |
|
|
|
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<uint_fast64_t>* choices, storm::storage::BitVector const* dirOverride = nullptr) const; |
|
|
|
template<typename Compare, bool directionOverridden> |
|
|
|
void multiplyAndReduceForward(std::vector<uint64_t> const& rowGroupIndices, std::vector<ValueType> const& vector, std::vector<ValueType> const* summand, std::vector<ValueType>& result, std::vector<uint_fast64_t>* choices, storm::storage::BitVector* dirOverride = nullptr) const; |
|
|
|
void multiplyAndReduceForward(std::vector<uint64_t> const& rowGroupIndices, std::vector<ValueType> const& vector, std::vector<ValueType> const* summand, std::vector<ValueType>& result, std::vector<uint_fast64_t>* choices, storm::storage::BitVector const* dirOverride = nullptr) const; |
|
|
|
|
|
|
|
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<uint_fast64_t>* choices, storm::storage::BitVector* dirOverride = nullptr) const; |
|
|
|
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<uint_fast64_t>* choices, storm::storage::BitVector const* dirOverride = nullptr) const; |
|
|
|
template<typename Compare, bool directionOverridden> |
|
|
|
void multiplyAndReduceBackward(std::vector<uint64_t> const& rowGroupIndices, std::vector<ValueType> const& vector, std::vector<ValueType> const* b, std::vector<ValueType>& result, std::vector<uint_fast64_t>* choices, storm::storage::BitVector* dirOverride = nullptr) const; |
|
|
|
void multiplyAndReduceBackward(std::vector<uint64_t> const& rowGroupIndices, std::vector<ValueType> const& vector, std::vector<ValueType> const* b, std::vector<ValueType>& result, std::vector<uint_fast64_t>* choices, storm::storage::BitVector const* dirOverride = nullptr) const; |
|
|
|
#ifdef STORM_HAVE_INTELTBB |
|
|
|
void multiplyAndReduceParallel(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<uint_fast64_t>* choices, storm::storage::BitVector* dirOverride = nullptr) const; |
|
|
|
void multiplyAndReduceParallel(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<uint_fast64_t>* choices, storm::storage::BitVector const* dirOverride = nullptr) const; |
|
|
|
template<typename Compare, bool directionOverridden> |
|
|
|
void multiplyAndReduceParallel(std::vector<uint64_t> const& rowGroupIndices, std::vector<ValueType> const& vector, std::vector<ValueType> const* b, std::vector<ValueType>& result, std::vector<uint_fast64_t>* choices, storm::storage::BitVector* dirOverride = nullptr) const; |
|
|
|
void multiplyAndReduceParallel(std::vector<uint64_t> const& rowGroupIndices, std::vector<ValueType> const& vector, std::vector<ValueType> const* b, std::vector<ValueType>& result, std::vector<uint_fast64_t>* choices, storm::storage::BitVector const* dirOverride = nullptr) const; |
|
|
|
#endif |
|
|
|
|
|
|
|
/*! |
|
|
|
@ -937,11 +937,11 @@ namespace storm { |
|
|
|
* @param vector The vector with which the matrix is to be multiplied. This vector is interpreted as being |
|
|
|
* a row vector. |
|
|
|
* @param result The vector that is supposed to hold the result of the multiplication after the operation. |
|
|
|
* @return The product of the matrix and the given vector as the content of the given result vector. The |
|
|
|
* @return The product of the matrix and the given vector as the content of the given result vector. The |
|
|
|
* result is to be interpreted as a row vector. |
|
|
|
*/ |
|
|
|
void multiplyVectorWithMatrix(std::vector<value_type> const& vector, std::vector<value_type>& result) const; |
|
|
|
|
|
|
|
|
|
|
|
/*! |
|
|
|
* Scales each row of the matrix, i.e., multiplies each element in row i with factors[i] |
|
|
|
* |
|
|
|
@ -955,7 +955,7 @@ namespace storm { |
|
|
|
* @param divisors The divisors with which each row is divided. |
|
|
|
*/ |
|
|
|
void divideRowsInPlace(std::vector<value_type> const& divisors); |
|
|
|
|
|
|
|
|
|
|
|
/*! |
|
|
|
* Performs one step of the successive over-relaxation technique. |
|
|
|
* |
|
|
|
@ -975,7 +975,7 @@ namespace storm { |
|
|
|
* @param result The vector to which to write the result. |
|
|
|
*/ |
|
|
|
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; |
|
|
|
|
|
|
|
|
|
|
|
/*! |
|
|
|
* Computes the sum of the entries in a given row. |
|
|
|
* |
|
|
|
@ -983,21 +983,21 @@ namespace storm { |
|
|
|
* @return The sum of the selected row. |
|
|
|
*/ |
|
|
|
value_type getRowSum(index_type row) const; |
|
|
|
|
|
|
|
|
|
|
|
/*! |
|
|
|
* Returns the number of non-constant entries |
|
|
|
*/ |
|
|
|
index_type getNonconstantEntryCount() const; |
|
|
|
|
|
|
|
|
|
|
|
/*! |
|
|
|
* Returns the number of rowGroups that contain a non-constant value |
|
|
|
*/ |
|
|
|
index_type getNonconstantRowGroupCount() const; |
|
|
|
|
|
|
|
|
|
|
|
/*! |
|
|
|
* Checks for each row whether it sums to one. |
|
|
|
*/ |
|
|
|
bool isProbabilistic() const; |
|
|
|
bool isProbabilistic() const; |
|
|
|
/*! |
|
|
|
* Checks if the current matrix is a submatrix of the given matrix, where a matrix A is called a submatrix |
|
|
|
* of B if B has no entries in position where A has none. Additionally, the matrices must be of equal size. |
|
|
|
@ -1007,10 +1007,10 @@ namespace storm { |
|
|
|
*/ |
|
|
|
template<typename OtherValueType> |
|
|
|
bool isSubmatrixOf(SparseMatrix<OtherValueType> const& matrix) const; |
|
|
|
|
|
|
|
|
|
|
|
// Returns true if the matrix is the identity matrix |
|
|
|
bool isIdentityMatrix() const; |
|
|
|
|
|
|
|
|
|
|
|
template<typename TPrime> |
|
|
|
friend std::ostream& operator<<(std::ostream& out, SparseMatrix<TPrime> const& matrix); |
|
|
|
|
|
|
|
@ -1018,7 +1018,7 @@ namespace storm { |
|
|
|
* Returns a string describing the dimensions of the matrix. |
|
|
|
*/ |
|
|
|
std::string getDimensionsAsString() const; |
|
|
|
|
|
|
|
|
|
|
|
/*! |
|
|
|
* Prints the matrix in a dense format, as also used by e.g. Matlab. |
|
|
|
* Notice that the format does not support multiple rows in a rowgroup. |
|
|
|
@ -1026,14 +1026,14 @@ namespace storm { |
|
|
|
* @out The stream to output to. |
|
|
|
*/ |
|
|
|
void printAsMatlabMatrix(std::ostream& out) const; |
|
|
|
|
|
|
|
|
|
|
|
/*! |
|
|
|
* Calculates a hash value over all values contained in the matrix. |
|
|
|
* |
|
|
|
* @return size_t A hash value for this matrix. |
|
|
|
*/ |
|
|
|
std::size_t hash() const; |
|
|
|
|
|
|
|
|
|
|
|
/*! |
|
|
|
* Returns an object representing the consecutive rows given by the parameters. |
|
|
|
* |
|
|
|
@ -1067,7 +1067,7 @@ namespace storm { |
|
|
|
* @return An object representing the given row. |
|
|
|
*/ |
|
|
|
rows getRow(index_type row); |
|
|
|
|
|
|
|
|
|
|
|
/*! |
|
|
|
* Returns an object representing the offset'th row in the rowgroup |
|
|
|
* @param rowGroup the row group |
|
|
|
@ -1075,7 +1075,7 @@ namespace storm { |
|
|
|
* @return An object representing the given row. |
|
|
|
*/ |
|
|
|
const_rows getRow(index_type rowGroup, index_type offset) const; |
|
|
|
|
|
|
|
|
|
|
|
/*! |
|
|
|
* Returns an object representing the offset'th row in the rowgroup |
|
|
|
* @param rowGroup the row group |
|
|
|
@ -1083,7 +1083,7 @@ namespace storm { |
|
|
|
* @return An object representing the given row. |
|
|
|
*/ |
|
|
|
rows getRow(index_type rowGroup, index_type offset); |
|
|
|
|
|
|
|
|
|
|
|
/*! |
|
|
|
* Returns an object representing the given row group. |
|
|
|
* |
|
|
|
@ -1091,7 +1091,7 @@ namespace storm { |
|
|
|
* @return An object representing the given row group. |
|
|
|
*/ |
|
|
|
const_rows getRowGroup(index_type rowGroup) const; |
|
|
|
|
|
|
|
|
|
|
|
/*! |
|
|
|
* Returns an object representing the given row group. |
|
|
|
* |
|
|
|
@ -1099,7 +1099,7 @@ namespace storm { |
|
|
|
* @return An object representing the given row group. |
|
|
|
*/ |
|
|
|
rows getRowGroup(index_type rowGroup); |
|
|
|
|
|
|
|
|
|
|
|
/*! |
|
|
|
* Retrieves an iterator that points to the beginning of the given row. |
|
|
|
* |
|
|
|
@ -1107,7 +1107,7 @@ namespace storm { |
|
|
|
* @return An iterator that points to the beginning of the given row. |
|
|
|
*/ |
|
|
|
const_iterator begin(index_type row = 0) const; |
|
|
|
|
|
|
|
|
|
|
|
/*! |
|
|
|
* Retrieves an iterator that points to the beginning of the given row. |
|
|
|
* |
|
|
|
@ -1115,7 +1115,7 @@ namespace storm { |
|
|
|
* @return An iterator that points to the beginning of the given row. |
|
|
|
*/ |
|
|
|
iterator begin(index_type row = 0); |
|
|
|
|
|
|
|
|
|
|
|
/*! |
|
|
|
* Retrieves an iterator that points past the end of the given row. |
|
|
|
* |
|
|
|
@ -1138,14 +1138,14 @@ namespace storm { |
|
|
|
* @return An iterator that points past the end of the last row of the matrix. |
|
|
|
*/ |
|
|
|
const_iterator end() const; |
|
|
|
|
|
|
|
|
|
|
|
/*! |
|
|
|
* Retrieves an iterator that points past the end of the last row of the matrix. |
|
|
|
* |
|
|
|
* @return An iterator that points past the end of the last row of the matrix. |
|
|
|
*/ |
|
|
|
iterator end(); |
|
|
|
|
|
|
|
|
|
|
|
/*! |
|
|
|
* Returns a copy of the matrix with the chosen internal data type |
|
|
|
*/ |
|
|
|
@ -1163,7 +1163,7 @@ namespace storm { |
|
|
|
|
|
|
|
return SparseMatrix<NewValueType>(columnCount, std::move(newRowIndications), std::move(newColumnsAndValues), std::move(newRowGroupIndices)); |
|
|
|
} |
|
|
|
|
|
|
|
|
|
|
|
private: |
|
|
|
/*! |
|
|
|
* Creates a submatrix of the current matrix by keeping only row groups and columns in the given row group |
|
|
|
@ -1178,39 +1178,39 @@ namespace storm { |
|
|
|
* given by the row group constraint are kept and all others are dropped. |
|
|
|
*/ |
|
|
|
SparseMatrix getSubmatrix(storm::storage::BitVector const& rowGroupConstraint, storm::storage::BitVector const& columnConstraint, std::vector<index_type> const& rowGroupIndices, bool insertDiagonalEntries = false, storm::storage::BitVector const& makeZeroColumns = storm::storage::BitVector()) const; |
|
|
|
|
|
|
|
|
|
|
|
// The number of rows of the matrix. |
|
|
|
index_type rowCount; |
|
|
|
|
|
|
|
|
|
|
|
// The number of columns of the matrix. |
|
|
|
mutable index_type columnCount; |
|
|
|
|
|
|
|
|
|
|
|
// The number of entries in the matrix. |
|
|
|
index_type entryCount; |
|
|
|
|
|
|
|
|
|
|
|
// The number of nonzero entries in the matrix. |
|
|
|
mutable index_type nonzeroEntryCount; |
|
|
|
|
|
|
|
|
|
|
|
// The storage for the columns and values of all entries in the matrix. |
|
|
|
std::vector<MatrixEntry<index_type, value_type>> columnsAndValues; |
|
|
|
|
|
|
|
|
|
|
|
// A vector containing the indices at which each given row begins. This index is to be interpreted as an |
|
|
|
// index in the valueStorage and the columnIndications vectors. Put differently, the values of the entries |
|
|
|
// in row i are valueStorage[rowIndications[i]] to valueStorage[rowIndications[i + 1]] where the last |
|
|
|
// entry is not included anymore. |
|
|
|
std::vector<index_type> rowIndications; |
|
|
|
|
|
|
|
|
|
|
|
// A flag indicating whether the matrix has a trivial row grouping. Note that this may be true and yet |
|
|
|
// there may be row group indices, because they were requested from the outside. |
|
|
|
bool trivialRowGrouping; |
|
|
|
|
|
|
|
|
|
|
|
// A vector indicating the row groups of the matrix. This needs to be mutible in case we create it on-the-fly. |
|
|
|
mutable boost::optional<std::vector<index_type>> rowGroupIndices; |
|
|
|
}; |
|
|
|
|
|
|
|
|
|
|
|
#ifdef STORM_HAVE_CARL |
|
|
|
std::set<storm::RationalFunctionVariable> getVariables(SparseMatrix<storm::RationalFunction> const& matrix); |
|
|
|
#endif |
|
|
|
|
|
|
|
|
|
|
|
} // namespace storage |
|
|
|
} // namespace storm |
