Storm
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
storm::solver::Multiplier< ValueType > Class Template Referenceabstract

#include <Multiplier.h>

Inheritance diagram for storm::solver::Multiplier< ValueType >:

Public Member Functions

 Multiplier (storm::storage::SparseMatrix< ValueType > const &matrix)
 
virtual ~Multiplier ()=default
 
virtual void clearCache () const
 
virtual void multiply (Environment const &env, std::vector< ValueType > const &x, std::vector< ValueType > const *b, std::vector< ValueType > &result) const =0
 Performs a matrix-vector multiplication x' = A*x + b.
 
virtual void multiplyGaussSeidel (Environment const &env, std::vector< ValueType > &x, std::vector< ValueType > const *b, bool backwards=true) const =0
 Performs a matrix-vector multiplication in gauss-seidel style.
 
void multiplyAndReduce (Environment const &env, OptimizationDirection const &dir, std::vector< ValueType > const &x, std::vector< ValueType > const *b, std::vector< ValueType > &result, std::vector< uint_fast64_t > *choices=nullptr) const
 Performs a matrix-vector multiplication x' = A*x + b and then minimizes/maximizes over the row groups so that the resulting vector has the size of number of row groups of A.
 
virtual void multiplyAndReduce (Environment const &env, OptimizationDirection const &dir, std::vector< uint64_t > const &rowGroupIndices, std::vector< ValueType > const &x, std::vector< ValueType > const *b, std::vector< ValueType > &result, std::vector< uint_fast64_t > *choices=nullptr) const =0
 
void multiplyAndReduceGaussSeidel (Environment const &env, OptimizationDirection const &dir, std::vector< ValueType > &x, std::vector< ValueType > const *b, std::vector< uint_fast64_t > *choices=nullptr, bool backwards=true) const
 Performs a matrix-vector multiplication in gauss-seidel style and then minimizes/maximizes over the row groups so that the resulting vector has the size of number of row groups of A.
 
virtual void multiplyAndReduceGaussSeidel (Environment const &env, OptimizationDirection const &dir, std::vector< uint64_t > const &rowGroupIndices, std::vector< ValueType > &x, std::vector< ValueType > const *b, std::vector< uint_fast64_t > *choices=nullptr, bool backwards=true) const =0
 
void repeatedMultiply (Environment const &env, std::vector< ValueType > &x, std::vector< ValueType > const *b, uint64_t n) const
 Performs repeated matrix-vector multiplication, using x[0] = x and x[i + 1] = A*x[i] + b.
 
void repeatedMultiplyAndReduce (Environment const &env, OptimizationDirection const &dir, std::vector< ValueType > &x, std::vector< ValueType > const *b, uint64_t n) const
 Performs repeated matrix-vector multiplication x' = A*x + b and then minimizes/maximizes over the row groups so that the resulting vector has the size of number of row groups of A.
 
virtual void multiplyRow (uint64_t const &rowIndex, std::vector< ValueType > const &x, ValueType &value) const =0
 Multiplies the row with the given index with x and adds the result to the provided value.
 
virtual void multiplyRow2 (uint64_t const &rowIndex, std::vector< ValueType > const &x1, ValueType &val1, std::vector< ValueType > const &x2, ValueType &val2) const
 Multiplies the row with the given index with x1 and x2 and adds the given offset o1 and o2, respectively.
 

Protected Attributes

std::unique_ptr< std::vector< ValueType > > cachedVector
 
storm::storage::SparseMatrix< ValueType > const & matrix
 

Detailed Description

template<typename ValueType>
class storm::solver::Multiplier< ValueType >

Definition at line 21 of file Multiplier.h.

Constructor & Destructor Documentation

◆ Multiplier()

template<typename ValueType >
storm::solver::Multiplier< ValueType >::Multiplier ( storm::storage::SparseMatrix< ValueType > const &  matrix)

Definition at line 25 of file Multiplier.cpp.

◆ ~Multiplier()

template<typename ValueType >
virtual storm::solver::Multiplier< ValueType >::~Multiplier ( )
virtualdefault

Member Function Documentation

◆ clearCache()

template<typename ValueType >
void storm::solver::Multiplier< ValueType >::clearCache ( ) const
virtual

Reimplemented in storm::solver::GmmxxMultiplier< ValueType >.

Definition at line 30 of file Multiplier.cpp.

◆ multiply()

template<typename ValueType >
virtual void storm::solver::Multiplier< ValueType >::multiply ( Environment const &  env,
std::vector< ValueType > const &  x,
std::vector< ValueType > const *  b,
std::vector< ValueType > &  result 
) const
pure virtual

Performs a matrix-vector multiplication x' = A*x + b.

Parameters
xThe input vector with which to multiply the matrix. Its length must be equal to the number of columns of A.
bIf non-null, this vector is added after the multiplication. If given, its length must be equal to the number of rows of A.
resultThe target vector into which to write the multiplication result. Its length must be equal to the number of rows of A. Can be the same as the x vector.

Implemented in storm::solver::GmmxxMultiplier< ValueType >, and storm::solver::NativeMultiplier< ValueType >.

◆ multiplyAndReduce() [1/2]

template<typename ValueType >
virtual void storm::solver::Multiplier< ValueType >::multiplyAndReduce ( Environment const &  env,
OptimizationDirection const &  dir,
std::vector< uint64_t > const &  rowGroupIndices,
std::vector< ValueType > const &  x,
std::vector< ValueType > const *  b,
std::vector< ValueType > &  result,
std::vector< uint_fast64_t > *  choices = nullptr 
) const
pure virtual

◆ multiplyAndReduce() [2/2]

template<typename ValueType >
void storm::solver::Multiplier< ValueType >::multiplyAndReduce ( Environment const &  env,
OptimizationDirection const &  dir,
std::vector< ValueType > const &  x,
std::vector< ValueType > const *  b,
std::vector< ValueType > &  result,
std::vector< uint_fast64_t > *  choices = nullptr 
) const

Performs a matrix-vector multiplication x' = A*x + b and then minimizes/maximizes over the row groups so that the resulting vector has the size of number of row groups of A.

Parameters
dirThe direction for the reduction step.
rowGroupIndicesA vector storing the row groups over which to reduce.
xThe input vector with which to multiply the matrix. Its length must be equal to the number of columns of A.
bIf non-null, this vector is added after the multiplication. If given, its length must be equal to the number of rows of A.
resultThe target vector into which to write the multiplication result. Its length must be equal to the number of rows of A. Can be the same as the x vector.
choicesIf given, the choices made in the reduction process are written to this vector.

Definition at line 35 of file Multiplier.cpp.

◆ multiplyAndReduceGaussSeidel() [1/2]

template<typename ValueType >
virtual void storm::solver::Multiplier< ValueType >::multiplyAndReduceGaussSeidel ( Environment const &  env,
OptimizationDirection const &  dir,
std::vector< uint64_t > const &  rowGroupIndices,
std::vector< ValueType > &  x,
std::vector< ValueType > const *  b,
std::vector< uint_fast64_t > *  choices = nullptr,
bool  backwards = true 
) const
pure virtual

◆ multiplyAndReduceGaussSeidel() [2/2]

template<typename ValueType >
void storm::solver::Multiplier< ValueType >::multiplyAndReduceGaussSeidel ( Environment const &  env,
OptimizationDirection const &  dir,
std::vector< ValueType > &  x,
std::vector< ValueType > const *  b,
std::vector< uint_fast64_t > *  choices = nullptr,
bool  backwards = true 
) const

Performs a matrix-vector multiplication in gauss-seidel style and then minimizes/maximizes over the row groups so that the resulting vector has the size of number of row groups of A.

Parameters
dirThe direction for the reduction step.
rowGroupIndicesA vector storing the row groups over which to reduce.
xThe input/output vector with which to multiply the matrix. Its length must be equal to the number of columns of A.
bIf non-null, this vector is added after the multiplication. If given, its length must be equal to the number of rows of A.
resultThe target vector into which to write the multiplication result. Its length must be equal to the number of rows of A. Can be the same as the x vector.
choicesIf given, the choices made in the reduction process are written to this vector.
backwardsif true, the iterations will be performed beginning from the last rowgroup and ending at the first rowgroup.

Definition at line 41 of file Multiplier.cpp.

◆ multiplyGaussSeidel()

template<typename ValueType >
virtual void storm::solver::Multiplier< ValueType >::multiplyGaussSeidel ( Environment const &  env,
std::vector< ValueType > &  x,
std::vector< ValueType > const *  b,
bool  backwards = true 
) const
pure virtual

Performs a matrix-vector multiplication in gauss-seidel style.

Parameters
xThe input/output vector with which to multiply the matrix. Its length must be equal to the number of columns of A.
bIf non-null, this vector is added after the multiplication. If given, its length must be equal to the number of rows of A.
backwardsif true, the iterations will be performed beginning from the last row and ending at the first row.

Implemented in storm::solver::GmmxxMultiplier< ValueType >, and storm::solver::NativeMultiplier< ValueType >.

◆ multiplyRow()

template<typename ValueType >
virtual void storm::solver::Multiplier< ValueType >::multiplyRow ( uint64_t const &  rowIndex,
std::vector< ValueType > const &  x,
ValueType &  value 
) const
pure virtual

Multiplies the row with the given index with x and adds the result to the provided value.

Parameters
rowIndexThe index of the considered row
xThe input vector with which the row is multiplied
valueThe multiplication result is added to this value. It shall not reffer to a value in x or in the Matrix.

Implemented in storm::solver::GmmxxMultiplier< ValueType >, and storm::solver::NativeMultiplier< ValueType >.

◆ multiplyRow2()

template<typename ValueType >
void storm::solver::Multiplier< ValueType >::multiplyRow2 ( uint64_t const &  rowIndex,
std::vector< ValueType > const &  x1,
ValueType &  val1,
std::vector< ValueType > const &  x2,
ValueType &  val2 
) const
virtual

Multiplies the row with the given index with x1 and x2 and adds the given offset o1 and o2, respectively.

Parameters
rowIndexThe index of the considered row
x1The first input vector with which the row is multiplied.
val1The first multiplication result is added to this value. It shall not reffer to a value in x or in the Matrix.
x2The second input vector with which the row is multiplied.
val2The second multiplication result is added to this value. It shall not reffer to a value in x or in the Matrix.

Reimplemented in storm::solver::NativeMultiplier< ValueType >.

Definition at line 77 of file Multiplier.cpp.

◆ repeatedMultiply()

template<typename ValueType >
void storm::solver::Multiplier< ValueType >::repeatedMultiply ( Environment const &  env,
std::vector< ValueType > &  x,
std::vector< ValueType > const *  b,
uint64_t  n 
) const

Performs repeated matrix-vector multiplication, using x[0] = x and x[i + 1] = A*x[i] + b.

After performing the necessary multiplications, the result is written to the input vector x. Note that the matrix A has to be given upon construction time of the solver object.

Parameters
xThe initial vector with which to perform matrix-vector multiplication. Its length must be equal to the number of columns of A.
bIf non-null, this vector is added after each multiplication. If given, its length must be equal to the number of rows of A.
nThe number of times to perform the multiplication.

Definition at line 47 of file Multiplier.cpp.

◆ repeatedMultiplyAndReduce()

template<typename ValueType >
void storm::solver::Multiplier< ValueType >::repeatedMultiplyAndReduce ( Environment const &  env,
OptimizationDirection const &  dir,
std::vector< ValueType > &  x,
std::vector< ValueType > const *  b,
uint64_t  n 
) const

Performs repeated matrix-vector multiplication x' = A*x + b and then minimizes/maximizes over the row groups so that the resulting vector has the size of number of row groups of A.

Parameters
dirThe direction for the reduction step.
xThe input vector with which to multiply the matrix. Its length must be equal to the number of columns of A.
bIf non-null, this vector is added after the multiplication. If given, its length must be equal to the number of rows of A.
resultThe target vector into which to write the multiplication result. Its length must be equal to the number of rows of A.
nThe number of times to perform the multiplication.

Definition at line 62 of file Multiplier.cpp.

Member Data Documentation

◆ cachedVector

template<typename ValueType >
std::unique_ptr<std::vector<ValueType> > storm::solver::Multiplier< ValueType >::cachedVector
mutableprotected

Definition at line 145 of file Multiplier.h.

◆ matrix

template<typename ValueType >
storm::storage::SparseMatrix<ValueType> const& storm::solver::Multiplier< ValueType >::matrix
protected

Definition at line 146 of file Multiplier.h.


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