A class that holds a possibly non-square matrix in the compressed row storage format. More...

#include <SparseMatrix.h>

Classes
class	rows
	This class represents a number of consecutive rows of the matrix. More...
class	const_rows
	This class represents a number of consecutive rows of the matrix. More...

Public Types
enum	MatrixStatus { UNINITIALIZED , INITIALIZED }
	An enum representing the internal state of the matrix. More...
typedef SparseMatrixIndexType	index_type
typedef ValueType	value_type
typedef std::vector< MatrixEntry< index_type, value_type > >::iterator	iterator
typedef std::vector< MatrixEntry< index_type, value_type > >::const_iterator	const_iterator

Public Member Functions
	SparseMatrix ()
	Constructs an empty sparse matrix.
	SparseMatrix (SparseMatrix< value_type > const &other)
	Constructs a sparse matrix by performing a deep-copy of the given matrix.
	SparseMatrix (SparseMatrix< value_type > const &other, bool insertDiagonalElements)
	Constructs a sparse matrix by performing a deep-copy of the given matrix.
	SparseMatrix (SparseMatrix< value_type > &&other)
	Constructs a sparse matrix by moving the contents of the given matrix to the newly created one.
	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 copying the given contents.
	SparseMatrix (index_type columnCount, std::vector< index_type > &&rowIndications, std::vector< MatrixEntry< index_type, value_type > > &&columnsAndValues, boost::optional< std::vector< index_type > > &&rowGroupIndices)
	Constructs a sparse matrix by moving the given contents.
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.
SparseMatrix< value_type > &	operator= (SparseMatrix< value_type > &&other)
	Assigns the contents of the given matrix to the current one by moving its contents.
bool	operator== (SparseMatrix< value_type > const &other) const
	Determines whether the current and the given matrix are semantically equal.
index_type	getRowCount () const
	Returns the number of rows of the matrix.
index_type	getColumnCount () const
	Returns the number of columns of the matrix.
index_type	getEntryCount () const
	Returns the number of entries in the matrix.
index_type	getRowGroupEntryCount (index_type const group) const
	Returns the number of entries in the given row group of the matrix.
index_type	getRowEntryCount (index_type const row) const
	Returns the number of entries in the given row of the matrix.
index_type	getNonzeroEntryCount () const
	Returns the cached number of nonzero entries in the matrix.
void	updateNonzeroEntryCount () const
	Recompute the nonzero entry count.
void	updateDimensions () const
	Recomputes the number of columns and the number of non-zero entries.
void	updateNonzeroEntryCount (std::make_signed< index_type >::type difference)
	Change the nonzero entry count by the provided value.
index_type	getRowGroupCount () const
	Returns the number of row groups in the matrix.
index_type	getRowGroupSize (index_type group) const
	Returns the size of the given row group.
index_type	getSizeOfLargestRowGroup () const
	Returns the size of the largest row group of the matrix.
index_type	getNumRowsInRowGroups (storm::storage::BitVector const &groupConstraint) const
	Returns the total number of rows that are in one of the specified row groups.
std::vector< index_type > const &	getRowGroupIndices () const
	Returns the grouping of rows of this matrix.
boost::integer_range< index_type >	getRowGroupIndices (index_type group) const
	Returns the row indices within the given group.
std::vector< index_type > const &	getRowIndices () const
	Returns the entry indices within the given row.
std::vector< index_type >	swapRowGroupIndices (std::vector< index_type > &&newRowGrouping)
	Swaps the grouping of rows of this matrix.
void	setRowGroupIndices (std::vector< index_type > const &newRowGroupIndices)
	Sets the row grouping to the given one.
bool	hasTrivialRowGrouping () const
	Retrieves whether the matrix has a trivial row grouping.
void	makeRowGroupingTrivial ()
	Makes the row grouping of this matrix trivial.
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 selected row groups.
storm::storage::BitVector	getRowFilter (storm::storage::BitVector const &groupConstraint, storm::storage::BitVector const &columnConstraints) const
	Returns the indices of all rows that.
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	makeRowsAbsorbing (storm::storage::BitVector const &rows, bool dropZeroEntries=false)
	This function makes the given rows absorbing.
void	makeRowGroupsAbsorbing (storm::storage::BitVector const &rowGroupConstraint, bool dropZeroEntries=false)
	This function makes the groups of rows given by the bit vector absorbing.
void	makeRowDirac (index_type row, index_type column, bool dropZeroEntries=false)
	This function makes the given row Dirac.
std::vector< ValueType >	getRowSumVector () const
	Sums the entries in all rows.
value_type	getConstrainedRowSum (index_type row, storm::storage::BitVector const &columns) const
	Sums the entries in the given row and columns.
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 those entries are added that are in selected columns.
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 groups.
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 one in the given bit vector.
SparseMatrix	restrictRows (storm::storage::BitVector const &rowsToKeep, bool allowEmptyRowGroups=false) const
	Restrict rows in grouped rows matrix.
SparseMatrix	permuteRows (std::vector< index_type > const &inversePermutation) const
	Permute rows of the matrix according to the vector.
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.
SparseMatrix	filterEntries (storm::storage::BitVector const &rowFilter) const
	Returns a copy of this matrix that only considers entries in the selected rows.
void	dropZeroEntries ()
	Removes all zero entries from this.
bool	compareRows (index_type i1, index_type i2) const
	Compares two rows.
BitVector	duplicateRowsInRowgroups () const
	Finds duplicate rows in a rowgroup.
void	swapRows (index_type const &row1, index_type const &row2)
	Swaps the two rows.
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.
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 often and with an arbitrary order The resulting matrix will have a trivial row grouping.
storm::storage::SparseMatrix< value_type >	transpose (bool joinGroups=false, bool keepZeros=false) const
	Transposes the matrix.
SparseMatrix< ValueType >	transposeSelectedRowsFromRowGroups (std::vector< uint64_t > const &rowGroupChoices, bool keepZeros=false) const
	Transposes the matrix w.r.t.
void	convertToEquationSystem ()
	Transforms the matrix into an equation system.
void	invertDiagonal ()
	Inverts all entries on the diagonal, i.e.
void	negateAllNonDiagonalEntries ()
	Negates (w.r.t.
void	deleteDiagonalEntries (bool dropZeroEntries=false)
	Sets all diagonal elements to zero.
std::pair< storm::storage::SparseMatrix< value_type >, std::vector< value_type > >	getJacobiDecomposition () const
	Calculates the Jacobi decomposition of this sparse matrix.
template<typename OtherValueType, typename ResultValueType = OtherValueType>
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 the given row of the other matrix and returns the sum.
template<typename OtherValueType, typename ResultValueType = OtherValueType>
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 containing the sum of the entries in each row of the resulting matrix.
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	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
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 writes the result to the given result vector.
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
template<typename Compare>
void	multiplyAndReduceForward (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
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
template<typename Compare>
void	multiplyAndReduceBackward (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	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.
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	scaleRowsInPlace (std::vector< value_type > const &factors)
	Scales each row of the matrix, i.e., multiplies each element in row i with factors[i].
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].
void	performSuccessiveOverRelaxationStep (ValueType omega, std::vector< ValueType > &x, std::vector< ValueType > const &b) const
	Performs one step of the successive over-relaxation technique.
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.
value_type	getRowSum (index_type row) const
	Computes the sum of the entries in a given row.
index_type	getNonconstantEntryCount () const
	Returns the number of non-constant entries.
index_type	getNonconstantRowGroupCount () const
	Returns the number of rowGroups that contain a non-constant value.
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.
bool	hasOnlyPositiveEntries () const
	Checks whether each present entry is strictly positive (omitted entries are not considered).
template<typename OtherValueType>
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 submatrix of B if B has no entries in position where A has none.
bool	isIdentityMatrix () const
std::string	getDimensionsAsString () const
	Returns a string describing the dimensions of the matrix.
void	printAsMatlabMatrix (std::ostream &out) const
	Prints the matrix in a dense format, as also used by e.g.
std::size_t	hash () const
	Calculates a hash value over all values contained in the matrix.
const_rows	getRows (index_type startRow, index_type endRow) const
	Returns an object representing the consecutive rows given by the parameters.
rows	getRows (index_type startRow, index_type endRow)
	Returns an object representing the consecutive rows given by the parameters.
const_rows	getRow (index_type row) const
	Returns an object representing the given row.
rows	getRow (index_type row)
	Returns 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.
rows	getRow (index_type rowGroup, index_type offset)
	Returns an object representing the offset'th row in the rowgroup.
const_rows	getRowGroup (index_type rowGroup) const
	Returns an object representing the given row group.
rows	getRowGroup (index_type rowGroup)
	Returns an object representing the given row group.
const_iterator	begin (index_type row) const
	Retrieves an iterator that points to the beginning of the given row.
iterator	begin (index_type row)
	Retrieves an iterator that points to the beginning of the given row.
const_iterator	begin () const
	Retrieves an iterator that points to the beginning of the first row of the matrix.
iterator	begin ()
	Retrieves an iterator that points to the beginning of the first row of the matrix.
const_iterator	end (index_type row) const
	Retrieves an iterator that points past the end of the given row.
iterator	end (index_type row)
	Retrieves an iterator that points past the end of the given row.
const_iterator	end () const
	Retrieves an iterator that points past the end of the last row of the matrix.
iterator	end ()
	Retrieves an iterator that points past the end of the last row of the matrix.
template<typename NewValueType>
SparseMatrix< NewValueType >	toValueType () const
	Returns a copy of the matrix with the chosen internal data type.
std::pair< storm::storage::SparseMatrix< Interval >, std::vector< Interval > >	getJacobiDecomposition () const
std::pair< storm::storage::SparseMatrix< RationalFunction >, std::vector< RationalFunction > >	getJacobiDecomposition () const
void	performSuccessiveOverRelaxationStep (Interval, std::vector< Interval > &, std::vector< Interval > const &) const
void	performWalkerChaeStep (std::vector< Interval > const &x, std::vector< Interval > const &rowSums, std::vector< Interval > const &b, std::vector< Interval > const &ax, std::vector< Interval > &result) const
void	multiplyAndReduceForward (OptimizationDirection const &dir, std::vector< uint64_t > const &rowGroupIndices, std::vector< storm::RationalFunction > const &vector, std::vector< storm::RationalFunction > const b, std::vector< storm::RationalFunction > &result, std::vector< uint64_t > choices) const
void	multiplyAndReduceBackward (OptimizationDirection const &dir, std::vector< uint64_t > const &rowGroupIndices, std::vector< storm::RationalFunction > const &vector, std::vector< storm::RationalFunction > const b, std::vector< storm::RationalFunction > &result, std::vector< uint64_t > choices) const
void	divideRowsInPlace (std::vector< Interval > const &)

Friends
class	storm::adapters::GmmxxAdapter< ValueType >
class	storm::adapters::EigenAdapter
class	storm::adapters::StormAdapter
class	SparseMatrixBuilder< ValueType >
template<typename TPrime>
std::ostream &	operator<< (std::ostream &out, SparseMatrix< TPrime > const &matrix)

Detailed Description

template<typename ValueType>
class storm::storage::SparseMatrix< ValueType >

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. Likewise, the matrix is intended to store one value per column only. However, the functions provided by the matrix are implemented in a way that makes it safe to store several entries per column.

The creation of a matrix can be done in several ways. If the number of rows, columns and entries is known prior to creating the matrix, the matrix can be constructed using this knowledge, which saves reallocations. On the other hand, if either one of these values is not known a priori, the matrix can be constructed as an empty matrix that needs to perform reallocations as more and more entries are inserted in the matrix.

It should be observed that due to the nature of the sparse matrix format, entries can only be inserted in order, i.e. row by row and column by column.

Definition at line 329 of file SparseMatrix.h.

Member Typedef Documentation

◆ const_iterator

template<typename ValueType>

typedef std::vector<MatrixEntry<index_type,value_type>>::const_iterator storm::storage::SparseMatrix< ValueType >::const_iterator

Definition at line 340 of file SparseMatrix.h.

◆ index_type

template<typename ValueType>

typedef SparseMatrixIndexType storm::storage::SparseMatrix< ValueType >::index_type

Definition at line 337 of file SparseMatrix.h.

◆ iterator

template<typename ValueType>

typedef std::vector<MatrixEntry<index_type,value_type>>::iterator storm::storage::SparseMatrix< ValueType >::iterator

Definition at line 339 of file SparseMatrix.h.

◆ value_type

template<typename ValueType>

typedef ValueType storm::storage::SparseMatrix< ValueType >::value_type

Definition at line 338 of file SparseMatrix.h.

Member Enumeration Documentation

◆ MatrixStatus

template<typename ValueType>

enum storm::storage::SparseMatrix::MatrixStatus

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.

Enumerator
UNINITIALIZED
INITIALIZED

Definition at line 433 of file SparseMatrix.h.

Constructor & Destructor Documentation

◆ SparseMatrix() [1/6]

template<typename ValueType>

storm::storage::SparseMatrix< ValueType >::SparseMatrix ( )

Constructs an empty sparse matrix.

Definition at line 497 of file SparseMatrix.cpp.

◆ SparseMatrix() [2/6]

template<typename ValueType>

storm::storage::SparseMatrix< ValueType >::SparseMatrix ( SparseMatrix< value_type > const & other )

Constructs a sparse matrix by performing a deep-copy of the given matrix.

Parameters

other The matrix from which to copy the content.

Definition at line 503 of file SparseMatrix.cpp.

◆ SparseMatrix() [3/6]

template<typename ValueType>

storm::storage::SparseMatrix< ValueType >::SparseMatrix	(	SparseMatrix< value_type > const &	other,
		bool	insertDiagonalElements )

Constructs a sparse matrix by performing a deep-copy of the given matrix.

Parameters

other	The matrix from which to copy the content.
insertDiagonalElements	If set to true, the copy will have all diagonal elements. If they did not exist in the original matrix, they are inserted and set to value zero.

Definition at line 516 of file SparseMatrix.cpp.

◆ SparseMatrix() [4/6]

template<typename ValueType>

storm::storage::SparseMatrix< ValueType >::SparseMatrix ( SparseMatrix< value_type > && other )

Constructs a sparse matrix by moving the contents of the given matrix to the newly created one.

Parameters

other The matrix from which to move the content.

Definition at line 523 of file SparseMatrix.cpp.

◆ SparseMatrix() [5/6]

template<typename ValueType>

storm::storage::SparseMatrix< ValueType >::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 copying the given contents.

Parameters

columnCount	The number of columns of the matrix.
rowIndications	The row indications vector of the matrix to be constructed.
columnsAndValues	The vector containing the columns and values of the entries in the matrix.
rowGroupIndices	The vector representing the row groups in the matrix.

Definition at line 539 of file SparseMatrix.cpp.

◆ SparseMatrix() [6/6]

template<typename ValueType>

storm::storage::SparseMatrix< ValueType >::SparseMatrix	(	index_type	columnCount,
		std::vector< index_type > &&	rowIndications,
		std::vector< MatrixEntry< index_type, value_type > > &&	columnsAndValues,
		boost::optional< std::vector< index_type > > &&	rowGroupIndices )

Constructs a sparse matrix by moving the given contents.

Parameters

columnCount	The number of columns of the matrix.
rowIndications	The row indications vector of the matrix to be constructed.
columnsAndValues	The vector containing the columns and values of the entries in the matrix.
rowGroupIndices	The vector representing the row groups in the matrix.

Definition at line 554 of file SparseMatrix.cpp.

Member Function Documentation

◆ begin() [1/4]

template<typename ValueType>

SparseMatrix< ValueType >::iterator storm::storage::SparseMatrix< ValueType >::begin ( )

Retrieves an iterator that points to the beginning of the first row of the matrix.

Returns: An iterator that points to the beginning of the first row of the matrix.

Definition at line 2202 of file SparseMatrix.cpp.

◆ begin() [2/4]

template<typename ValueType>

SparseMatrix< ValueType >::const_iterator storm::storage::SparseMatrix< ValueType >::begin ( ) const

Retrieves an iterator that points to the beginning of the first row of the matrix.

Returns: An iterator that points to the beginning of the first row of the matrix.

Definition at line 2197 of file SparseMatrix.cpp.

◆ begin() [3/4]

template<typename ValueType>

SparseMatrix< ValueType >::iterator storm::storage::SparseMatrix< ValueType >::begin ( index_type row )

Retrieves an iterator that points to the beginning of the given row.

Parameters

row	The row to the beginning of which the iterator has to point.

Returns: An iterator that points to the beginning of the given row.

Definition at line 2191 of file SparseMatrix.cpp.

◆ begin() [4/4]

template<typename ValueType>

SparseMatrix< ValueType >::const_iterator storm::storage::SparseMatrix< ValueType >::begin ( index_type row ) const

Retrieves an iterator that points to the beginning of the given row.

Parameters

row	The row to the beginning of which the iterator has to point.

Returns: An iterator that points to the beginning of the given row.

Definition at line 2185 of file SparseMatrix.cpp.

◆ compareRows()

template<typename ValueType>

bool storm::storage::SparseMatrix< ValueType >::compareRows	(	index_type	i1,
		index_type	i2 ) const

Compares two rows.

Parameters

i1	Index of first row
i2	Index of second row

Returns: True if the rows have identical entries.

Definition at line 953 of file SparseMatrix.cpp.

◆ convertToEquationSystem()

template<typename ValueType>

void storm::storage::SparseMatrix< ValueType >::convertToEquationSystem ( )

Transforms the matrix into an equation system.

That is, it transforms the matrix A into a matrix (1-A).

Definition at line 1578 of file SparseMatrix.cpp.

◆ deleteDiagonalEntries()

template<typename ValueType>

void storm::storage::SparseMatrix< ValueType >::deleteDiagonalEntries ( bool dropZeroEntries = false )

Sets all diagonal elements to zero.

Parameters

dropZeroEntries if true, zero entries resulting from the transformation are dropped from the matrix after the transformation. Dropping zero entries takes time linear in the number of matrix entries.

Definition at line 1625 of file SparseMatrix.cpp.

◆ divideRowsInPlace() [1/2]

void storm::storage::SparseMatrix< Interval >::divideRowsInPlace ( std::vector< Interval > const & )

Definition at line 2116 of file SparseMatrix.cpp.

◆ divideRowsInPlace() [2/2]

template<typename ValueType>

void storm::storage::SparseMatrix< ValueType >::divideRowsInPlace ( std::vector< value_type > const & divisors )

Divides each row of the matrix, i.e., divides each element in row i with divisors[i].

Parameters

divisors The divisors with which each row is divided.

Definition at line 2103 of file SparseMatrix.cpp.

◆ dropZeroEntries()

template<typename ValueType>

void storm::storage::SparseMatrix< ValueType >::dropZeroEntries ( )

Removes all zero entries from this.

Definition at line 1318 of file SparseMatrix.cpp.

◆ duplicateRowsInRowgroups()

template<typename ValueType>

BitVector storm::storage::SparseMatrix< ValueType >::duplicateRowsInRowgroups ( ) const

Finds duplicate rows in a rowgroup.

Definition at line 970 of file SparseMatrix.cpp.

◆ end() [1/4]

template<typename ValueType>

SparseMatrix< ValueType >::iterator storm::storage::SparseMatrix< ValueType >::end ( )

Retrieves an iterator that points past the end of the last row of the matrix.

Returns: An iterator that points past the end of the last row of the matrix.

Definition at line 2224 of file SparseMatrix.cpp.

◆ end() [2/4]

template<typename ValueType>

SparseMatrix< ValueType >::const_iterator storm::storage::SparseMatrix< ValueType >::end ( ) const

Retrieves an iterator that points past the end of the last row of the matrix.

Returns: An iterator that points past the end of the last row of the matrix.

Definition at line 2219 of file SparseMatrix.cpp.

◆ end() [3/4]

template<typename ValueType>

SparseMatrix< ValueType >::iterator storm::storage::SparseMatrix< ValueType >::end ( index_type row )

Retrieves an iterator that points past the end of the given row.

Parameters

row	The row past the end of which the iterator has to point.

Returns: An iterator that points past the end of the given row.

Definition at line 2213 of file SparseMatrix.cpp.

◆ end() [4/4]

template<typename ValueType>

SparseMatrix< ValueType >::const_iterator storm::storage::SparseMatrix< ValueType >::end ( index_type row ) const

Retrieves an iterator that points past the end of the given row.

Parameters

row	The row past the end of which the iterator has to point.

Returns: An iterator that points past the end of the given row.

Definition at line 2207 of file SparseMatrix.cpp.

◆ filterEntries()

template<typename ValueType>

SparseMatrix< ValueType > storm::storage::SparseMatrix< ValueType >::filterEntries ( storm::storage::BitVector const & rowFilter ) const

Returns a copy of this matrix that only considers entries in the selected rows.

Non-selected rows will not have any entries

Note: does not change the dimensions (row-, column-, and rowGroup count) of this matrix

Parameters

rowFilter the selected rows

Definition at line 1294 of file SparseMatrix.cpp.

◆ getColumnCount()

template<typename ValueType>

SparseMatrix< ValueType >::index_type storm::storage::SparseMatrix< ValueType >::getColumnCount ( ) const

Returns the number of columns of the matrix.

Returns: The number of columns of the matrix.

Definition at line 665 of file SparseMatrix.cpp.

◆ getConstrainedRowGroupSumVector()

template<typename ValueType>

std::vector< ValueType > storm::storage::SparseMatrix< ValueType >::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 groups.

Parameters

rowGroupConstraint	A bit vector that indicates which row groups are to be considered.
columnConstraint	A bit vector that indicates which columns to sum.

Returns: A vector whose entries represent the sums of selected columns for all rows in selected row groups.

Definition at line 1108 of file SparseMatrix.cpp.

◆ getConstrainedRowSum()

template<typename ValueType>

ValueType storm::storage::SparseMatrix< ValueType >::getConstrainedRowSum	(	index_type	row,
		storm::storage::BitVector const &	columns ) const

Sums the entries in the given row and columns.

Parameters

row	The row whose entries to add.
columns	A bit vector that indicates which columns to add.

Returns: The sum of the entries in the given row and columns.

Definition at line 1086 of file SparseMatrix.cpp.

◆ getConstrainedRowSumVector()

template<typename ValueType>

std::vector< ValueType > storm::storage::SparseMatrix< ValueType >::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 those entries are added that are in selected columns.

Parameters

rowConstraint	A bit vector that indicates for which rows to compute the constrained sum.
columnConstraint	A bit vector that indicates which columns to add in the selected rows.

Returns: A vector whose elements are the sums of the selected columns in each row.

Definition at line 1097 of file SparseMatrix.cpp.

◆ getDimensionsAsString()

template<typename ValueType>

std::string storm::storage::SparseMatrix< ValueType >::getDimensionsAsString ( ) const

Returns a string describing the dimensions of the matrix.

Definition at line 2393 of file SparseMatrix.cpp.

◆ getEntryCount()

template<typename ValueType>

SparseMatrix< ValueType >::index_type storm::storage::SparseMatrix< ValueType >::getEntryCount ( ) const

Returns the number of entries in the matrix.

Returns: The number of entries in the matrix.

Definition at line 670 of file SparseMatrix.cpp.

◆ getJacobiDecomposition() [1/3]

std::pair< storm::storage::SparseMatrix< RationalFunction >, std::vector< RationalFunction > > storm::storage::SparseMatrix< RationalFunction >::getJacobiDecomposition ( ) const

Definition at line 1669 of file SparseMatrix.cpp.

◆ getJacobiDecomposition() [2/3]

std::pair< storm::storage::SparseMatrix< Interval >, std::vector< Interval > > storm::storage::SparseMatrix< Interval >::getJacobiDecomposition ( ) const

Definition at line 1664 of file SparseMatrix.cpp.

◆ getJacobiDecomposition() [3/3]

template<typename ValueType>

std::pair< storm::storage::SparseMatrix< ValueType >, std::vector< ValueType > > storm::storage::SparseMatrix< ValueType >::getJacobiDecomposition ( ) const

Calculates the Jacobi decomposition of this sparse matrix.

For this operation, the matrix must be square.

Returns: A pair (L+U, D^-1) containing the matrix L+U and the inverted diagonal D^-1 (as a vector).

Definition at line 1641 of file SparseMatrix.cpp.

◆ getNonconstantEntryCount()

template<typename ValueType>

SparseMatrix< ValueType >::index_type storm::storage::SparseMatrix< ValueType >::getNonconstantEntryCount ( ) const

Returns the number of non-constant entries.

Definition at line 2238 of file SparseMatrix.cpp.

◆ getNonconstantRowGroupCount()

template<typename ValueType>

SparseMatrix< ValueType >::index_type storm::storage::SparseMatrix< ValueType >::getNonconstantRowGroupCount ( ) const

Returns the number of rowGroups that contain a non-constant value.

Definition at line 2249 of file SparseMatrix.cpp.

◆ getNonzeroEntryCount()

template<typename ValueType>

SparseMatrix< ValueType >::index_type storm::storage::SparseMatrix< ValueType >::getNonzeroEntryCount ( ) const

Returns the cached number of nonzero entries in the matrix.

See also: updateNonzeroEntryCount()

Returns: The number of nonzero entries in the matrix.

Definition at line 693 of file SparseMatrix.cpp.

◆ getNumRowsInRowGroups()

template<typename ValueType>

SparseMatrix< ValueType >::index_type storm::storage::SparseMatrix< ValueType >::getNumRowsInRowGroups ( storm::storage::BitVector const & groupConstraint ) const

Returns the total number of rows that are in one of the specified row groups.

Definition at line 753 of file SparseMatrix.cpp.

◆ getPointwiseProductRowSum()

template<typename ValueType>

template<typename OtherValueType, typename ResultValueType>

template storm::RationalFunction storm::storage::SparseMatrix< ValueType >::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 the given row of the other matrix and returns the sum.

Parameters

otherMatrix A reference to the matrix with which to perform the pointwise multiplication. This matrix must be a submatrix of the current matrix in the sense that it may not have entries at indices where there is no entry in the current matrix.

Returns: the sum of the product of the entries in the given row.

Definition at line 1676 of file SparseMatrix.cpp.

◆ getPointwiseProductRowSumVector()

template<typename ValueType>

template<typename OtherValueType, typename ResultValueType>

template std::vector< storm::RationalInterval > storm::storage::SparseMatrix< ValueType >::getPointwiseProductRowSumVector ( storm::storage::SparseMatrix< OtherValueType > const & otherMatrix ) 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.

Parameters

otherMatrix A reference to the matrix with which to perform the pointwise multiplication. This matrix must be a submatrix of the current matrix in the sense that it may not have entries at indices where there is no entry in the current matrix.

Returns: A vector containing the sum of the entries in each row of the matrix resulting from pointwise multiplication of the current matrix with the given matrix.

Definition at line 1701 of file SparseMatrix.cpp.

◆ getRow() [1/4]

template<typename ValueType>

SparseMatrix< ValueType >::rows storm::storage::SparseMatrix< ValueType >::getRow ( index_type row )

Returns an object representing the given row.

Parameters

row	The row to get.

Returns: An object representing the given row.

Definition at line 2136 of file SparseMatrix.cpp.

◆ getRow() [2/4]

template<typename ValueType>

SparseMatrix< ValueType >::const_rows storm::storage::SparseMatrix< ValueType >::getRow ( index_type row ) const

Returns an object representing the given row.

Parameters

row	The row to get.

Returns: An object representing the given row.

Definition at line 2131 of file SparseMatrix.cpp.

◆ getRow() [3/4]

template<typename ValueType>

SparseMatrix< ValueType >::rows storm::storage::SparseMatrix< ValueType >::getRow	(	index_type	rowGroup,
		index_type	offset )

Returns an object representing the offset'th row in the rowgroup.

Parameters

rowGroup	the row group
offset	which row in the group

Returns: An object representing the given row.

Definition at line 2153 of file SparseMatrix.cpp.

◆ getRow() [4/4]

template<typename ValueType>

SparseMatrix< ValueType >::const_rows storm::storage::SparseMatrix< ValueType >::getRow	(	index_type	rowGroup,
		index_type	offset ) const

Returns an object representing the offset'th row in the rowgroup.

Parameters

rowGroup	the row group
offset	which row in the group

Returns: An object representing the given row.

Definition at line 2141 of file SparseMatrix.cpp.

◆ getRowCount()

template<typename ValueType>

SparseMatrix< ValueType >::index_type storm::storage::SparseMatrix< ValueType >::getRowCount ( ) const

Returns the number of rows of the matrix.

Returns: The number of rows of the matrix.

Definition at line 660 of file SparseMatrix.cpp.

◆ getRowEntryCount()

template<typename ValueType>

SparseMatrix< ValueType >::index_type storm::storage::SparseMatrix< ValueType >::getRowEntryCount ( index_type const row ) const

Returns the number of entries in the given row of the matrix.

Parameters

row Which row

Returns: Number of entries

Definition at line 688 of file SparseMatrix.cpp.

◆ getRowFilter() [1/2]

template<typename ValueType>

storm::storage::BitVector storm::storage::SparseMatrix< ValueType >::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 selected row groups.

Parameters

groups the selected row groups

Returns: a bit vector that is true at position i iff the row group of row i is selected.

Definition at line 830 of file SparseMatrix.cpp.

◆ getRowFilter() [2/2]

template<typename ValueType>

storm::storage::BitVector storm::storage::SparseMatrix< ValueType >::getRowFilter	(	storm::storage::BitVector const &	groupConstraint,
		storm::storage::BitVector const &	columnConstraints ) const

Returns the indices of all rows that.

are in a selected group and
only have entries within the selected columns.

Parameters

groupConstraint	the selected groups
columnConstraints	the selected columns

Returns: a bit vector that is true at position i iff row i satisfies the constraints.

Definition at line 839 of file SparseMatrix.cpp.

◆ getRowGroup() [1/2]

template<typename ValueType>

SparseMatrix< ValueType >::rows storm::storage::SparseMatrix< ValueType >::getRowGroup ( index_type rowGroup )

Returns an object representing the given row group.

Parameters

rowGroup The row group to get.

Returns: An object representing the given row group.

Definition at line 2175 of file SparseMatrix.cpp.

◆ getRowGroup() [2/2]

template<typename ValueType>

SparseMatrix< ValueType >::const_rows storm::storage::SparseMatrix< ValueType >::getRowGroup ( index_type rowGroup ) const

Returns an object representing the given row group.

Parameters

rowGroup The row group to get.

Returns: An object representing the given row group.

Definition at line 2165 of file SparseMatrix.cpp.

◆ getRowGroupCount()

template<typename ValueType>

SparseMatrix< ValueType >::index_type storm::storage::SparseMatrix< ValueType >::getRowGroupCount ( ) const

Returns the number of row groups in the matrix.

Returns: The number of row groups in the matrix.

Definition at line 725 of file SparseMatrix.cpp.

◆ getRowGroupEntryCount()

template<typename ValueType>

SparseMatrix< ValueType >::index_type storm::storage::SparseMatrix< ValueType >::getRowGroupEntryCount ( index_type const group ) const

Returns the number of entries in the given row group of the matrix.

Returns: The number of entries in the given row group of the matrix.

Definition at line 675 of file SparseMatrix.cpp.

◆ getRowGroupFilter()

template<typename ValueType>

storm::storage::BitVector storm::storage::SparseMatrix< ValueType >::getRowGroupFilter	(	storm::storage::BitVector const &	rowConstraint,
		bool	setIfForAllRowsInGroup ) const

Returns the indices of all row groups selected by the row constraints.

Parameters

rowConstraint	the selected rows
setIfForAllRowsInGroup	if true, a group is selected if the rowConstraint is true for all rows within that group. If false, a group is selected if the rowConstraint is true for some row within that group

Returns: a bit vector that is true at position i iff row i satisfies the constraints.

Definition at line 860 of file SparseMatrix.cpp.

◆ getRowGroupIndices() [1/2]

template<typename ValueType>

std::vector< typename SparseMatrix< ValueType >::index_type > const & storm::storage::SparseMatrix< ValueType >::getRowGroupIndices ( ) const

Returns the grouping of rows of this matrix.

Returns: The grouping of rows of this matrix.

Definition at line 771 of file SparseMatrix.cpp.

◆ getRowGroupIndices() [2/2]

template<typename ValueType>

boost::integer_range< typename SparseMatrix< ValueType >::index_type > storm::storage::SparseMatrix< ValueType >::getRowGroupIndices ( index_type group ) const

Returns the row indices within the given group.

Definition at line 786 of file SparseMatrix.cpp.

◆ getRowGroupSize()

template<typename ValueType>

SparseMatrix< ValueType >::index_type storm::storage::SparseMatrix< ValueType >::getRowGroupSize ( index_type group ) const

Returns the size of the given row group.

Parameters

group The group whose size to retrieve.

Returns: The number of rows that belong to the given row group.

Definition at line 734 of file SparseMatrix.cpp.

◆ getRowIndices()

template<typename ValueType>

std::vector< typename SparseMatrix< ValueType >::index_type > const & storm::storage::SparseMatrix< ValueType >::getRowIndices ( ) const

Returns the entry indices within the given row.

Definition at line 781 of file SparseMatrix.cpp.

◆ getRows() [1/2]

template<typename ValueType>

SparseMatrix< ValueType >::rows storm::storage::SparseMatrix< ValueType >::getRows	(	index_type	startRow,
		index_type	endRow )

Returns an object representing the consecutive rows given by the parameters.

Parameters

startRow	The starting row.
endRow	The ending row (which is not included in the result).

Returns: An object representing the consecutive rows given by the parameters.

Definition at line 2126 of file SparseMatrix.cpp.

◆ getRows() [2/2]

template<typename ValueType>

SparseMatrix< ValueType >::const_rows storm::storage::SparseMatrix< ValueType >::getRows	(	index_type	startRow,
		index_type	endRow ) const

Returns an object representing the consecutive rows given by the parameters.

Parameters

startRow	The starting row.
endRow	The ending row (which is not included in the result).

Returns: An object representing the consecutive rows given by the parameters.

Definition at line 2121 of file SparseMatrix.cpp.

◆ getRowSum()

template<typename ValueType>

ValueType storm::storage::SparseMatrix< ValueType >::getRowSum ( index_type row ) const

Computes the sum of the entries in a given row.

Parameters

row	The row that is to be summed.

Returns: The sum of the selected row.

Definition at line 2229 of file SparseMatrix.cpp.

◆ getRowSumVector()

template<typename ValueType>

std::vector< ValueType > storm::storage::SparseMatrix< ValueType >::getRowSumVector ( ) const

Sums the entries in all rows.

Returns: The vector of sums of the entries in the respective rows.

Definition at line 1074 of file SparseMatrix.cpp.

◆ getSizeOfLargestRowGroup()

template<typename ValueType>

SparseMatrix< ValueType >::index_type storm::storage::SparseMatrix< ValueType >::getSizeOfLargestRowGroup ( ) const

Returns the size of the largest row group of the matrix.

Definition at line 739 of file SparseMatrix.cpp.

◆ getSubmatrix()

template<typename ValueType>

SparseMatrix< ValueType > storm::storage::SparseMatrix< ValueType >::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 one in the given bit vector.

Parameters

useGroups	If set to true, the constraint for the rows is interpreted as selecting whole row groups. If it is not set, the row constraint is interpreted over the actual rows. Note that empty row groups will be dropped altogether. That is, if no row of a row group is selected or the row group is already empty, the submatrix will not have this row group.
constraint	A bit vector indicating which rows to keep.
columnConstraint	A bit vector indicating which columns to keep.
insertDiagonalEntries	If set to true, the resulting matrix will have zero entries in column i for each row i, if there is no value yet. This can then be used for inserting other values later.

Returns: A matrix corresponding to a submatrix of the current matrix in which only rows and columns given by the constraints are kept and all others are dropped.

Definition at line 1127 of file SparseMatrix.cpp.

◆ hash()

template<typename ValueType>

std::size_t storm::storage::SparseMatrix< ValueType >::hash ( ) const

Calculates a hash value over all values contained in the matrix.

Returns: size_t A hash value for this matrix.

Definition at line 2473 of file SparseMatrix.cpp.

◆ hasOnlyPositiveEntries()

template<typename ValueType>

bool storm::storage::SparseMatrix< ValueType >::hasOnlyPositiveEntries ( ) const

Checks whether each present entry is strictly positive (omitted entries are not considered).

Definition at line 2327 of file SparseMatrix.cpp.

◆ hasTrivialRowGrouping()

template<typename ValueType>

bool storm::storage::SparseMatrix< ValueType >::hasTrivialRowGrouping ( ) const

Retrieves whether the matrix has a trivial row grouping.

Returns: True iff the matrix has a trivial row grouping.

Definition at line 813 of file SparseMatrix.cpp.

◆ invertDiagonal()

template<typename ValueType>

void storm::storage::SparseMatrix< ValueType >::invertDiagonal ( )

Inverts all entries on the diagonal, i.e.

sets the diagonal values to one minus their previous value. Requires the matrix to contain each diagonal entry and to be square.

Definition at line 1584 of file SparseMatrix.cpp.

◆ isIdentityMatrix()

template<typename ValueType>

bool storm::storage::SparseMatrix< ValueType >::isIdentityMatrix ( ) const

Definition at line 2364 of file SparseMatrix.cpp.

◆ isProbabilistic()

template<typename ValueType>

bool storm::storage::SparseMatrix< ValueType >::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.

For interval models, we check if each interval contains a value between zero and one and if the sum contains one. For rational functions, we only do these checks if they are constant, i.e., do not contain any parameter.

Parameters

tolerance	The tolerance used when comparing values to zero and one.
reason	if the matrix is not probabilistic, this string will be filled with a human-readable explanation of why the matrix is not probabilistic.

Definition at line 2263 of file SparseMatrix.cpp.

◆ isSubmatrixOf()

template<typename ValueType>

template<typename OtherValueType>

template bool storm::storage::SparseMatrix< ValueType >::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 submatrix of B if B has no entries in position where A has none.

Additionally, the matrices must be of equal size.

Parameters

matrix The matrix that possibly is a supermatrix of the current matrix.

Returns: True iff the current matrix is a submatrix of the given matrix.

Definition at line 2338 of file SparseMatrix.cpp.

◆ makeRowDirac()

template<typename ValueType>

void storm::storage::SparseMatrix< ValueType >::makeRowDirac	(	index_type	row,
		index_type	column,
		bool	dropZeroEntries = false )

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.

Parameters

row	The row to be made Dirac.
column	The index of the column whose value is to be set to 1.
dropZeroEntries	if true, zero entries resulting from the transformation are dropped from the matrix after the transformation. Dropping zero entries takes time linear in the number of matrix entries.

Definition at line 915 of file SparseMatrix.cpp.

◆ makeRowGroupingTrivial()

template<typename ValueType>

void storm::storage::SparseMatrix< ValueType >::makeRowGroupingTrivial ( )

Makes the row grouping of this matrix trivial.

Has no effect when the row grouping is already trivial.

Definition at line 818 of file SparseMatrix.cpp.

◆ makeRowGroupsAbsorbing()

template<typename ValueType>

void storm::storage::SparseMatrix< ValueType >::makeRowGroupsAbsorbing	(	storm::storage::BitVector const &	rowGroupConstraint,
		bool	dropZeroEntries = false )

This function makes the groups of rows given by the bit vector absorbing.

Parameters

rowGroupConstraint	A bit vector indicating which row groups to make absorbing.
dropZeroEntries	if true, zero entries resulting from the transformation are dropped from the matrix after the transformation. Dropping zero entries takes time linear in the number of matrix entries.

Definition at line 895 of file SparseMatrix.cpp.

◆ makeRowsAbsorbing()

template<typename ValueType>

void storm::storage::SparseMatrix< ValueType >::makeRowsAbsorbing	(	storm::storage::BitVector const &	rows,
		bool	dropZeroEntries = false )

This function makes the given rows absorbing.

Parameters

rows	A bit vector indicating which rows are to be made absorbing.
dropZeroEntries	if true, zero entries resulting from the transformation are dropped from the matrix after the transformation. Dropping zero entries takes time linear in the number of matrix entries.

Definition at line 883 of file SparseMatrix.cpp.

◆ multiplyAndReduce()

template<typename ValueType>

void storm::storage::SparseMatrix< ValueType >::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 writes the result to the given result vector.

Parameters

dir	The optimization direction for the reduction.
rowGroupIndices	The row groups for the reduction
vector	The vector with which to multiply the matrix.
summand	If given, this summand will be added to the result of the multiplication.
result	The vector that is supposed to hold the result of the multiplication after the operation.
choices	If given, the choices made in the reduction process will be written to this vector. Note that if the direction is maximize, the choice for a row group is only updated if the value obtained with the 'new' choice has a value strictly better (wrt. to the optimization direction) value.

Returns: The resulting vector the content of the given result vector.

Definition at line 2053 of file SparseMatrix.cpp.

◆ multiplyAndReduceBackward() [1/3]

void storm::storage::SparseMatrix< storm::RationalFunction >::multiplyAndReduceBackward	(	OptimizationDirection const &	dir,
		std::vector< uint64_t > const &	rowGroupIndices,
		std::vector< storm::RationalFunction > const &	vector,
		std::vector< storm::RationalFunction > const *	b,
		std::vector< storm::RationalFunction > &	result,
		std::vector< uint64_t > *	choices ) const

Definition at line 2045 of file SparseMatrix.cpp.

◆ multiplyAndReduceBackward() [2/3]

template<typename ValueType>

template<typename Compare>

void storm::storage::SparseMatrix< ValueType >::multiplyAndReduceBackward	(	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

Definition at line 1974 of file SparseMatrix.cpp.

◆ multiplyAndReduceBackward() [3/3]

template<typename ValueType>

void storm::storage::SparseMatrix< ValueType >::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

Definition at line 1962 of file SparseMatrix.cpp.

◆ multiplyAndReduceForward() [1/3]

void storm::storage::SparseMatrix< storm::RationalFunction >::multiplyAndReduceForward	(	OptimizationDirection const &	dir,
		std::vector< uint64_t > const &	rowGroupIndices,
		std::vector< storm::RationalFunction > const &	vector,
		std::vector< storm::RationalFunction > const *	b,
		std::vector< storm::RationalFunction > &	result,
		std::vector< uint64_t > *	choices ) const

Definition at line 1954 of file SparseMatrix.cpp.

◆ multiplyAndReduceForward() [2/3]

template<typename ValueType>

template<typename Compare>

void storm::storage::SparseMatrix< ValueType >::multiplyAndReduceForward	(	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

Definition at line 1878 of file SparseMatrix.cpp.

◆ multiplyAndReduceForward() [3/3]

template<typename ValueType>

void storm::storage::SparseMatrix< ValueType >::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

Definition at line 1866 of file SparseMatrix.cpp.

◆ multiplyRowWithVector()

template<typename ValueType>

ValueType storm::storage::SparseMatrix< ValueType >::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.

Parameters

row	The index of the row with which to multiply
vector	The vector with which to multiply the row.

Returns: the result of the multiplication.

Definition at line 1790 of file SparseMatrix.cpp.

◆ multiplyVectorWithMatrix()

template<typename ValueType>

void storm::storage::SparseMatrix< ValueType >::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.

Parameters

vector	The vector with which the matrix is to be multiplied. This vector is interpreted as being a row vector.
result	The vector that is supposed to hold the result of the multiplication after the operation.

Returns: 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.

Definition at line 2075 of file SparseMatrix.cpp.

◆ multiplyWithVector()

template<typename ValueType>

void storm::storage::SparseMatrix< ValueType >::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.

Parameters

vector	The vector with which to multiply the matrix.
result	The vector that is supposed to hold the result of the multiplication after the operation.
summand	If given, this summand will be added to the result of the multiplication.

Returns: The product of the matrix and the given vector as the content of the given result vector.

Definition at line 1711 of file SparseMatrix.cpp.

◆ multiplyWithVectorBackward()

template<typename ValueType>

void storm::storage::SparseMatrix< ValueType >::multiplyWithVectorBackward	(	std::vector< value_type > const &	vector,
		std::vector< value_type > &	result,
		std::vector< value_type > const *	summand = nullptr ) const

Definition at line 1761 of file SparseMatrix.cpp.

◆ multiplyWithVectorForward()

template<typename ValueType>

void storm::storage::SparseMatrix< ValueType >::multiplyWithVectorForward	(	std::vector< value_type > const &	vector,
		std::vector< value_type > &	result,
		std::vector< value_type > const *	summand = nullptr ) const

Definition at line 1732 of file SparseMatrix.cpp.

◆ negateAllNonDiagonalEntries()

template<typename ValueType>

void storm::storage::SparseMatrix< ValueType >::negateAllNonDiagonalEntries ( )

Negates (w.r.t.

addition) all entries that are not on the diagonal.

Definition at line 1613 of file SparseMatrix.cpp.

◆ operator=() [1/2]

template<typename ValueType>

SparseMatrix< ValueType > & storm::storage::SparseMatrix< ValueType >::operator= ( SparseMatrix< value_type > && other )

Assigns the contents of the given matrix to the current one by moving its contents.

Parameters

other The matrix from which to move to contents.

Definition at line 588 of file SparseMatrix.cpp.

◆ operator=() [2/2]

template<typename ValueType>

SparseMatrix< ValueType > & storm::storage::SparseMatrix< ValueType >::operator= ( SparseMatrix< value_type > const & other )

Assigns the contents of the given matrix to the current one by deep-copying its contents.

Parameters

other The matrix from which to copy-assign.

Definition at line 571 of file SparseMatrix.cpp.

◆ operator==()

template<typename ValueType>

bool storm::storage::SparseMatrix< ValueType >::operator== ( SparseMatrix< value_type > const & other ) const

Determines whether the current and the given matrix are semantically equal.

Parameters

other The matrix with which to compare the current matrix.

Returns: True iff the given matrix is semantically equal to the current one.

Definition at line 605 of file SparseMatrix.cpp.

◆ performSuccessiveOverRelaxationStep() [1/2]

void storm::storage::SparseMatrix< Interval >::performSuccessiveOverRelaxationStep	(	Interval	,
		std::vector< Interval > &	,
		std::vector< Interval > const &	) const

Definition at line 1827 of file SparseMatrix.cpp.

◆ performSuccessiveOverRelaxationStep() [2/2]

template<typename ValueType>

void storm::storage::SparseMatrix< ValueType >::performSuccessiveOverRelaxationStep	(	ValueType	omega,
		std::vector< ValueType > &	x,
		std::vector< ValueType > const &	b ) const

Performs one step of the successive over-relaxation technique.

Parameters

omega	The Omega parameter for SOR.
x	The current solution vector. The result will be written to the very same vector.
b	The 'right-hand side' of the problem.

Definition at line 1800 of file SparseMatrix.cpp.

◆ performWalkerChaeStep() [1/2]

void storm::storage::SparseMatrix< Interval >::performWalkerChaeStep	(	std::vector< Interval > const &	x,
		std::vector< Interval > const &	rowSums,
		std::vector< Interval > const &	b,
		std::vector< Interval > const &	ax,
		std::vector< Interval > &	result ) const

Definition at line 1860 of file SparseMatrix.cpp.

◆ performWalkerChaeStep() [2/2]

template<typename ValueType>

void storm::storage::SparseMatrix< ValueType >::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.

Parameters

x	The current solution vector.
columnSums	The sums the individual columns.
b	The 'right-hand side' of the problem.
ax	A vector resulting from multiplying the current matrix with the vector x.
result	The vector to which to write the result.

Definition at line 1832 of file SparseMatrix.cpp.

◆ permuteRowGroupsAndColumns()

template<typename ValueType>

SparseMatrix< ValueType > storm::storage::SparseMatrix< ValueType >::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.

That is, in row group i, write the entries of row group inverseRowGroupPermutation[i] and in column columnPermutation[j], write the entries of column j.

Precondition: inverseRowGroupPermutation and columnPermutation must be permutations (i.e., they must contain each index exactly once).

Note: the permutation for the row groups is inverted while the one for columns is not!

Returns: the permuted matrix.

Definition at line 1461 of file SparseMatrix.cpp.

◆ permuteRows()

template<typename ValueType>

SparseMatrix< ValueType > storm::storage::SparseMatrix< ValueType >::permuteRows ( std::vector< index_type > const & inversePermutation ) const

Permute rows of the matrix according to the vector.

That is, in row i, write the entry of row inversePermutation[i]. Consequently, a single row might actually be written into multiple other rows, and the function application is not necessarily a permutation. Notice that this method does not touch column entries, nor the row grouping.

Definition at line 1438 of file SparseMatrix.cpp.

◆ printAsMatlabMatrix()

template<typename ValueType>

void storm::storage::SparseMatrix< ValueType >::printAsMatlabMatrix ( std::ostream & out ) 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.

@out The stream to output to.

Definition at line 2448 of file SparseMatrix.cpp.

◆ restrictRows()

template<typename ValueType>

SparseMatrix< ValueType > storm::storage::SparseMatrix< ValueType >::restrictRows	(	storm::storage::BitVector const &	rowsToKeep,
		bool	allowEmptyRowGroups = false ) const

Restrict rows in grouped rows matrix.

Ensures that the number of groups stays the same.

Parameters

rowsToKeep	A bit vector indicating which rows to keep.
allowEmptyRowGroups	if set to true, the result can potentially have empty row groups. Otherwise, it is asserted that there are no empty row groups.

Note: The resulting matrix will always have a non-trivial row grouping even if the current one is trivial.

Definition at line 1249 of file SparseMatrix.cpp.

◆ scaleRowsInPlace()

template<typename ValueType>

void storm::storage::SparseMatrix< ValueType >::scaleRowsInPlace ( std::vector< value_type > const & factors )

Scales each row of the matrix, i.e., multiplies each element in row i with factors[i].

Parameters

factors The factors with which each row is scaled.

Definition at line 2091 of file SparseMatrix.cpp.

◆ selectRowsFromRowGroups()

template<typename ValueType>

SparseMatrix< ValueType > storm::storage::SparseMatrix< ValueType >::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.

Parameters

insertDiagonalEntries If set to true, the resulting matrix will have zero entries in column i for each row in row group i. This can then be used for inserting other values later.

Returns: A submatrix of the current matrix by selecting one row out of each row group.

Definition at line 1339 of file SparseMatrix.cpp.

◆ selectRowsFromRowIndexSequence()

template<typename ValueType>

SparseMatrix< ValueType > storm::storage::SparseMatrix< ValueType >::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 often and with an arbitrary order The resulting matrix will have a trivial row grouping.

Parameters

rowIndexSequence	the sequence of row indices which specifies, which rows are contained in the new matrix
insertDiagonalEntries	If set to true, the resulting matrix will have zero entries in column i for each row. This can then be used for inserting other values later.

Returns: A matrix which rows are selected from this matrix according to the given index sequence

Definition at line 1395 of file SparseMatrix.cpp.

◆ setRowGroupIndices()

template<typename ValueType>

void storm::storage::SparseMatrix< ValueType >::setRowGroupIndices ( std::vector< index_type > const & newRowGroupIndices )

Sets the row grouping to the given one.

Note: It is assumed that the new row grouping is non-trivial.

Parameters

newRowGroupIndices The new row group indices.

Definition at line 807 of file SparseMatrix.cpp.

◆ swapRowGroupIndices()

template<typename ValueType>

std::vector< typename SparseMatrix< ValueType >::index_type > storm::storage::SparseMatrix< ValueType >::swapRowGroupIndices ( std::vector< index_type > && newRowGrouping )

Swaps the grouping of rows of this matrix.

Returns: The old grouping of rows of this matrix.

Definition at line 797 of file SparseMatrix.cpp.

◆ swapRows()

template<typename ValueType>

void storm::storage::SparseMatrix< ValueType >::swapRows	(	index_type const &	row1,
		index_type const &	row2 )

Swaps the two rows.

Parameters

row1	Index of first row
row2	Index of second row

Definition at line 985 of file SparseMatrix.cpp.

◆ toValueType()

template<typename ValueType>

template<typename NewValueType>

SparseMatrix< NewValueType > storm::storage::SparseMatrix< ValueType >::toValueType ( ) const

inline

Returns a copy of the matrix with the chosen internal data type.

Definition at line 1211 of file SparseMatrix.h.

◆ transpose()

template<typename ValueType>

SparseMatrix< ValueType > storm::storage::SparseMatrix< ValueType >::transpose	(	bool	joinGroups = false,
		bool	keepZeros = false ) const

Transposes the matrix.

Parameters

joinGroups	A flag indicating whether the row groups are supposed to be treated as single rows.
keepZeros	A flag indicating whether entries with value zero should be kept.

Returns: A sparse matrix that represents the transpose of this matrix.

Definition at line 1485 of file SparseMatrix.cpp.

◆ transposeSelectedRowsFromRowGroups()

template<typename ValueType>

SparseMatrix< ValueType > storm::storage::SparseMatrix< ValueType >::transposeSelectedRowsFromRowGroups	(	std::vector< uint64_t > const &	rowGroupChoices,
		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.

Parameters

rowGroupChoices	A mapping from each row group index to a selected row in this group.
keepZeros	A flag indicating whether entries with value zero should be kept.

Definition at line 1534 of file SparseMatrix.cpp.

◆ updateDimensions()

template<typename ValueType>

void storm::storage::SparseMatrix< ValueType >::updateDimensions ( ) const

Recomputes the number of columns and the number of non-zero entries.

Definition at line 713 of file SparseMatrix.cpp.

◆ updateNonzeroEntryCount() [1/2]

template<typename ValueType>

void storm::storage::SparseMatrix< ValueType >::updateNonzeroEntryCount ( ) const

Recompute the nonzero entry count.

Definition at line 698 of file SparseMatrix.cpp.

◆ updateNonzeroEntryCount() [2/2]

template<typename ValueType>

void storm::storage::SparseMatrix< ValueType >::updateNonzeroEntryCount ( std::make_signed< index_type >::type difference )

Change the nonzero entry count by the provided value.

Parameters

difference Difference between old and new nonzero entry count.

Definition at line 708 of file SparseMatrix.cpp.

◆ operator<<

template<typename ValueType>

template<typename TPrime>

std::ostream & operator<<	(	std::ostream &	out,
		SparseMatrix< TPrime > const &	matrix )

friend

◆ SparseMatrixBuilder< ValueType >

template<typename ValueType>

friend class SparseMatrixBuilder< ValueType >

friend

Definition at line 334 of file SparseMatrix.h.

◆ storm::adapters::EigenAdapter

template<typename ValueType>

friend class storm::adapters::EigenAdapter

friend

Definition at line 333 of file SparseMatrix.h.

◆ storm::adapters::GmmxxAdapter< ValueType >

template<typename ValueType>

friend class storm::adapters::GmmxxAdapter< ValueType >

friend

Definition at line 311 of file SparseMatrix.h.

◆ storm::adapters::StormAdapter

template<typename ValueType>

friend class storm::adapters::StormAdapter

friend

Definition at line 334 of file SparseMatrix.h.

The documentation for this class was generated from the following files:

src/storm-pars/modelchecker/region/monotonicity/OrderBasedMonotonicityBackend.h
src/storm/storage/SparseMatrix.h
src/storm/storage/SparseMatrix.cpp

Classes

Public Types

Public Member Functions

Friends

Detailed Description

Member Typedef Documentation

◆ const_iterator

◆ index_type

◆ iterator

◆ value_type

Member Enumeration Documentation

◆ MatrixStatus

Constructor & Destructor Documentation

◆ SparseMatrix() [1/6]

◆ SparseMatrix() [2/6]

◆ SparseMatrix() [3/6]

◆ SparseMatrix() [4/6]

◆ SparseMatrix() [5/6]

◆ SparseMatrix() [6/6]

Member Function Documentation

◆ begin() [1/4]

◆ begin() [2/4]

◆ begin() [3/4]

◆ begin() [4/4]

◆ compareRows()

◆ convertToEquationSystem()

◆ deleteDiagonalEntries()

◆ divideRowsInPlace() [1/2]

◆ divideRowsInPlace() [2/2]

◆ dropZeroEntries()

◆ duplicateRowsInRowgroups()

◆ end() [1/4]

◆ end() [2/4]

◆ end() [3/4]

◆ end() [4/4]

◆ filterEntries()

◆ getColumnCount()

◆ getConstrainedRowGroupSumVector()

◆ getConstrainedRowSum()

◆ getConstrainedRowSumVector()

◆ getDimensionsAsString()

◆ getEntryCount()

◆ getJacobiDecomposition() [1/3]

◆ getJacobiDecomposition() [2/3]

◆ getJacobiDecomposition() [3/3]

◆ getNonconstantEntryCount()

◆ getNonconstantRowGroupCount()

◆ getNonzeroEntryCount()

◆ getNumRowsInRowGroups()

◆ getPointwiseProductRowSum()

◆ getPointwiseProductRowSumVector()

◆ getRow() [1/4]

◆ getRow() [2/4]

◆ getRow() [3/4]

◆ getRow() [4/4]

◆ getRowCount()

◆ getRowEntryCount()

◆ getRowFilter() [1/2]

◆ getRowFilter() [2/2]

◆ getRowGroup() [1/2]

◆ getRowGroup() [2/2]

◆ getRowGroupCount()

◆ getRowGroupEntryCount()

◆ getRowGroupFilter()

◆ getRowGroupIndices() [1/2]

◆ getRowGroupIndices() [2/2]

◆ getRowGroupSize()

◆ getRowIndices()

◆ getRows() [1/2]

◆ getRows() [2/2]

◆ getRowSum()

◆ getRowSumVector()

◆ getSizeOfLargestRowGroup()

◆ getSubmatrix()

◆ hash()

◆ hasOnlyPositiveEntries()

◆ hasTrivialRowGrouping()

◆ invertDiagonal()

◆ isIdentityMatrix()

◆ isProbabilistic()