Storm
A Modern Probabilistic Model Checker
|
#include <Multiplier.h>
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 |
Definition at line 21 of file Multiplier.h.
storm::solver::Multiplier< ValueType >::Multiplier | ( | storm::storage::SparseMatrix< ValueType > const & | matrix | ) |
Definition at line 25 of file Multiplier.cpp.
|
virtualdefault |
|
virtual |
Reimplemented in storm::solver::GmmxxMultiplier< ValueType >.
Definition at line 30 of file Multiplier.cpp.
|
pure virtual |
Performs a matrix-vector multiplication x' = A*x + b.
x | The input vector with which to multiply the matrix. Its length must be equal to the number of columns of A. |
b | If non-null, this vector is added after the multiplication. If given, its length must be equal to the number of rows of A. |
result | The 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 >.
|
pure virtual |
Implemented in storm::solver::GmmxxMultiplier< ValueType >, and storm::solver::NativeMultiplier< 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.
dir | The direction for the reduction step. |
rowGroupIndices | A vector storing the row groups over which to reduce. |
x | The input vector with which to multiply the matrix. Its length must be equal to the number of columns of A. |
b | If non-null, this vector is added after the multiplication. If given, its length must be equal to the number of rows of A. |
result | The 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. |
choices | If given, the choices made in the reduction process are written to this vector. |
Definition at line 35 of file Multiplier.cpp.
|
pure virtual |
Implemented in storm::solver::GmmxxMultiplier< ValueType >, and storm::solver::NativeMultiplier< 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.
dir | The direction for the reduction step. |
rowGroupIndices | A vector storing the row groups over which to reduce. |
x | The input/output vector with which to multiply the matrix. Its length must be equal to the number of columns of A. |
b | If non-null, this vector is added after the multiplication. If given, its length must be equal to the number of rows of A. |
result | The 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. |
choices | If given, the choices made in the reduction process are written to this vector. |
backwards | if 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.
|
pure virtual |
Performs a matrix-vector multiplication in gauss-seidel style.
x | The input/output vector with which to multiply the matrix. Its length must be equal to the number of columns of A. |
b | If non-null, this vector is added after the multiplication. If given, its length must be equal to the number of rows of A. |
backwards | if 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 >.
|
pure virtual |
Multiplies the row with the given index with x and adds the result to the provided value.
rowIndex | The index of the considered row |
x | The input vector with which the row is multiplied |
value | The 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 >.
|
virtual |
Multiplies the row with the given index with x1 and x2 and adds the given offset o1 and o2, respectively.
rowIndex | The index of the considered row |
x1 | The first input vector with which the row is multiplied. |
val1 | The first multiplication result is added to this value. It shall not reffer to a value in x or in the Matrix. |
x2 | The second input vector with which the row is multiplied. |
val2 | The 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.
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.
x | The initial vector with which to perform matrix-vector multiplication. Its length must be equal to the number of columns of A. |
b | If non-null, this vector is added after each multiplication. If given, its length must be equal to the number of rows of A. |
n | The number of times to perform the multiplication. |
Definition at line 47 of file Multiplier.cpp.
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.
dir | The direction for the reduction step. |
x | The input vector with which to multiply the matrix. Its length must be equal to the number of columns of A. |
b | If non-null, this vector is added after the multiplication. If given, its length must be equal to the number of rows of A. |
result | The target vector into which to write the multiplication result. Its length must be equal to the number of rows of A. |
n | The number of times to perform the multiplication. |
Definition at line 62 of file Multiplier.cpp.
|
mutableprotected |
Definition at line 145 of file Multiplier.h.
|
protected |
Definition at line 146 of file Multiplier.h.