Storm 1.13.0.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
Multiplier.h
Go to the documentation of this file.
1#pragma once
2
3#include <memory>
4#include <vector>
5
9
10namespace storm {
11
12class Environment;
13
14namespace storage {
15template<typename ValueType>
16class SparseMatrix;
17}
18
19namespace solver {
20
21template<typename ValueType, typename SolutionType = ValueType>
23 public:
25
26 virtual ~Multiplier() = default;
27
28 /*
29 * Clears the currently cached data of this multiplier in order to free some memory.
30 */
31 virtual void clearCache() const;
32
43 virtual void multiply(Environment const& env, std::vector<SolutionType> const& x, std::vector<ValueType> const* b,
44 std::vector<SolutionType>& result) const = 0;
45
55 virtual void multiplyGaussSeidel(Environment const& env, std::vector<SolutionType>& x, std::vector<ValueType> const* b, bool backwards = true) const = 0;
56
72 void multiplyAndReduce(Environment const& env, OptimizationDirection const& dir, std::vector<SolutionType> const& x, std::vector<ValueType> const* b,
73 std::vector<SolutionType>& result, UncertaintyResolutionMode const& uncertaintyResolutionMode = UncertaintyResolutionMode::Unset,
74 std::vector<uint_fast64_t>* choices = nullptr) const;
75 virtual void multiplyAndReduce(Environment const& env, OptimizationDirection const& dir, std::vector<uint64_t> const& rowGroupIndices,
76 std::vector<SolutionType> const& x, std::vector<ValueType> const* b, std::vector<SolutionType>& result,
77 UncertaintyResolutionMode const& uncertaintyResolutionMode = UncertaintyResolutionMode::Unset,
78 std::vector<uint_fast64_t>* choices = nullptr) const = 0;
79
95 void multiplyAndReduceGaussSeidel(Environment const& env, OptimizationDirection const& dir, std::vector<SolutionType>& x, std::vector<ValueType> const* b,
96 std::vector<uint_fast64_t>* choices = nullptr, bool backwards = true) const;
97 virtual void multiplyAndReduceGaussSeidel(Environment const& env, OptimizationDirection const& dir, std::vector<uint64_t> const& rowGroupIndices,
98 std::vector<SolutionType>& x, std::vector<ValueType> const* b, std::vector<uint_fast64_t>* choices = nullptr,
99 bool backwards = true) const = 0;
100
112 void repeatedMultiply(Environment const& env, std::vector<SolutionType>& x, std::vector<ValueType> const* b, uint64_t n) const;
113
128 void repeatedMultiplyAndReduce(Environment const& env, OptimizationDirection const& dir, std::vector<SolutionType>& x, std::vector<ValueType> const* b,
129 uint64_t n, UncertaintyResolutionMode const& uncertaintyResolutionMode = UncertaintyResolutionMode::Unset) const;
142 void repeatedMultiplyWithFactor(Environment const& env, std::vector<SolutionType>& x, std::vector<ValueType> const* b, uint64_t n,
143 SolutionType factor) const;
144
160 void repeatedMultiplyAndReduceWithFactor(Environment const& env, OptimizationDirection const& dir, std::vector<SolutionType>& x,
161 std::vector<ValueType> const* b, uint64_t n, SolutionType factor,
162 UncertaintyResolutionMode const& uncertaintyResolutionMode = UncertaintyResolutionMode::Unset) const;
163
164 protected:
165 std::vector<SolutionType>& provideCachedVector(uint64_t size) const;
166
167 mutable std::unique_ptr<std::vector<SolutionType>> cachedVector;
169};
170
171template<typename ValueType, typename SolutionType = ValueType>
173 public:
174 MultiplierFactory() = default;
176
177 std::unique_ptr<Multiplier<ValueType, SolutionType>> create(Environment const& env, storm::storage::SparseMatrix<ValueType> const& matrix);
178};
179
180} // namespace solver
181} // namespace storm
std::unique_ptr< Multiplier< ValueType, SolutionType > > create(Environment const &env, storm::storage::SparseMatrix< ValueType > const &matrix)
virtual void multiplyAndReduce(Environment const &env, OptimizationDirection const &dir, std::vector< uint64_t > const &rowGroupIndices, std::vector< SolutionType > const &x, std::vector< ValueType > const *b, std::vector< SolutionType > &result, UncertaintyResolutionMode const &uncertaintyResolutionMode=UncertaintyResolutionMode::Unset, std::vector< uint_fast64_t > *choices=nullptr) const =0
Multiplier(storm::storage::SparseMatrix< ValueType > const &matrix)
void repeatedMultiplyWithFactor(Environment const &env, std::vector< SolutionType > &x, std::vector< ValueType > const *b, uint64_t n, SolutionType factor) const
Performs repeated matrix-vector multiplication x' = A*(factor * x) + b.
void multiplyAndReduce(Environment const &env, OptimizationDirection const &dir, std::vector< SolutionType > const &x, std::vector< ValueType > const *b, std::vector< SolutionType > &result, UncertaintyResolutionMode const &uncertaintyResolutionMode=UncertaintyResolutionMode::Unset, 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...
std::unique_ptr< std::vector< SolutionType > > cachedVector
Definition Multiplier.h:167
void repeatedMultiply(Environment const &env, std::vector< SolutionType > &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.
virtual ~Multiplier()=default
void repeatedMultiplyAndReduceWithFactor(Environment const &env, OptimizationDirection const &dir, std::vector< SolutionType > &x, std::vector< ValueType > const *b, uint64_t n, SolutionType factor, UncertaintyResolutionMode const &uncertaintyResolutionMode=UncertaintyResolutionMode::Unset) const
Performs repeated matrix-vector multiplication x' = A*(factor * x) + b, minimizes/maximizes over the ...
void multiplyAndReduceGaussSeidel(Environment const &env, OptimizationDirection const &dir, std::vector< SolutionType > &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...
virtual void multiplyGaussSeidel(Environment const &env, std::vector< SolutionType > &x, std::vector< ValueType > const *b, bool backwards=true) const =0
Performs a matrix-vector multiplication in gauss-seidel style.
std::vector< SolutionType > & provideCachedVector(uint64_t size) const
virtual void clearCache() const
storm::storage::SparseMatrix< ValueType > const & matrix
Definition Multiplier.h:168
virtual void multiplyAndReduceGaussSeidel(Environment const &env, OptimizationDirection const &dir, std::vector< uint64_t > const &rowGroupIndices, std::vector< SolutionType > &x, std::vector< ValueType > const *b, std::vector< uint_fast64_t > *choices=nullptr, bool backwards=true) const =0
virtual void multiply(Environment const &env, std::vector< SolutionType > const &x, std::vector< ValueType > const *b, std::vector< SolutionType > &result) const =0
Performs a matrix-vector multiplication x' = A*x + b.
void repeatedMultiplyAndReduce(Environment const &env, OptimizationDirection const &dir, std::vector< SolutionType > &x, std::vector< ValueType > const *b, uint64_t n, UncertaintyResolutionMode const &uncertaintyResolutionMode=UncertaintyResolutionMode::Unset) const
Performs repeated matrix-vector multiplication x' = A*x + b and then minimizes/maximizes over the row...
A class that holds a possibly non-square matrix in the compressed row storage format.