Storm
A Modern Probabilistic Model Checker
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
Multiplier.h
Go to the documentation of this file.
1#pragma once
2
3#include <memory>
4#include <vector>
5
8
9namespace storm {
10
11class Environment;
12
13namespace storage {
14template<typename ValueType>
15class SparseMatrix;
16}
17
18namespace solver {
19
20template<typename ValueType>
22 public:
24
25 virtual ~Multiplier() = default;
26
27 /*
28 * Clears the currently cached data of this multiplier in order to free some memory.
29 */
30 virtual void clearCache() const;
31
42 virtual void multiply(Environment const& env, std::vector<ValueType> const& x, std::vector<ValueType> const* b, std::vector<ValueType>& result) const = 0;
43
53 virtual void multiplyGaussSeidel(Environment const& env, std::vector<ValueType>& x, std::vector<ValueType> const* b, bool backwards = true) const = 0;
54
69 void multiplyAndReduce(Environment const& env, OptimizationDirection const& dir, std::vector<ValueType> const& x, std::vector<ValueType> const* b,
70 std::vector<ValueType>& result, std::vector<uint_fast64_t>* choices = nullptr) const;
71 virtual void multiplyAndReduce(Environment const& env, OptimizationDirection const& dir, std::vector<uint64_t> const& rowGroupIndices,
72 std::vector<ValueType> const& x, std::vector<ValueType> const* b, std::vector<ValueType>& result,
73 std::vector<uint_fast64_t>* choices = nullptr) const = 0;
74
90 void multiplyAndReduceGaussSeidel(Environment const& env, OptimizationDirection const& dir, std::vector<ValueType>& x, std::vector<ValueType> const* b,
91 std::vector<uint_fast64_t>* choices = nullptr, bool backwards = true) const;
92 virtual void multiplyAndReduceGaussSeidel(Environment const& env, OptimizationDirection const& dir, std::vector<uint64_t> const& rowGroupIndices,
93 std::vector<ValueType>& x, std::vector<ValueType> const* b, std::vector<uint_fast64_t>* choices = nullptr,
94 bool backwards = true) const = 0;
95
107 void repeatedMultiply(Environment const& env, std::vector<ValueType>& x, std::vector<ValueType> const* b, uint64_t n) const;
108
122 void repeatedMultiplyAndReduce(Environment const& env, OptimizationDirection const& dir, std::vector<ValueType>& x, std::vector<ValueType> const* b,
123 uint64_t n) const;
124
131 virtual void multiplyRow(uint64_t const& rowIndex, std::vector<ValueType> const& x, ValueType& value) const = 0;
132
141 virtual void multiplyRow2(uint64_t const& rowIndex, std::vector<ValueType> const& x1, ValueType& val1, std::vector<ValueType> const& x2,
142 ValueType& val2) const;
143
144 protected:
145 mutable std::unique_ptr<std::vector<ValueType>> cachedVector;
147};
148
149template<typename ValueType>
151 public:
152 MultiplierFactory() = default;
154
155 std::unique_ptr<Multiplier<ValueType>> create(Environment const& env, storm::storage::SparseMatrix<ValueType> const& matrix);
156};
157
158} // namespace solver
159} // namespace storm
std::unique_ptr< Multiplier< ValueType > > create(Environment const &env, storm::storage::SparseMatrix< ValueType > const &matrix)
virtual void clearCache() const
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 r...
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...
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 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,...
virtual ~Multiplier()=default
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
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 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.
std::unique_ptr< std::vector< ValueType > > cachedVector
Definition Multiplier.h:145
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 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...
storm::storage::SparseMatrix< ValueType > const & matrix
Definition Multiplier.h:146
A class that holds a possibly non-square matrix in the compressed row storage format.
LabParser.cpp.
Definition cli.cpp:18