Storm 1.10.0.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
NativeMultiplier.cpp
Go to the documentation of this file.
1#include "NativeMultiplier.h"
2
3#include "storm-config.h"
4
10
11namespace storm {
12namespace solver {
13
14template<typename ValueType>
16 // Intentionally left empty.
17}
18
19template<typename ValueType>
20void NativeMultiplier<ValueType>::multiply(Environment const& env, std::vector<ValueType> const& x, std::vector<ValueType> const* b,
21 std::vector<ValueType>& result) const {
22 std::vector<ValueType>* target = &result;
23 if (&x == &result) {
24 target = &this->provideCachedVector(x.size());
25 }
26 multAdd(x, b, *target);
27 if (&x == &result) {
28 std::swap(result, *target);
29 }
30}
31
32template<typename ValueType>
33void NativeMultiplier<ValueType>::multiplyGaussSeidel(Environment const& env, std::vector<ValueType>& x, std::vector<ValueType> const* b,
34 bool backwards) const {
35 if (backwards) {
36 this->matrix.multiplyWithVectorBackward(x, x, b);
37 } else {
38 this->matrix.multiplyWithVectorForward(x, x, b);
39 }
40}
41
42template<typename ValueType>
43void NativeMultiplier<ValueType>::multiplyAndReduce(Environment const& env, OptimizationDirection const& dir, std::vector<uint64_t> const& rowGroupIndices,
44 std::vector<ValueType> const& x, std::vector<ValueType> const* b, std::vector<ValueType>& result,
45 std::vector<uint_fast64_t>* choices) const {
46 std::vector<ValueType>* target = &result;
47 if (&x == &result) {
48 target = &this->provideCachedVector(x.size());
49 }
50 multAddReduce(dir, rowGroupIndices, x, b, *target, choices);
51 if (&x == &result) {
52 std::swap(result, *target);
53 }
54}
55
56template<typename ValueType>
58 std::vector<uint64_t> const& rowGroupIndices, std::vector<ValueType>& x,
59 std::vector<ValueType> const* b, std::vector<uint_fast64_t>* choices, bool backwards) const {
60 if (backwards) {
61 this->matrix.multiplyAndReduceBackward(dir, rowGroupIndices, x, b, x, choices);
62 } else {
63 this->matrix.multiplyAndReduceForward(dir, rowGroupIndices, x, b, x, choices);
64 }
65}
66
67template<typename ValueType>
68void NativeMultiplier<ValueType>::multiplyRow(uint64_t const& rowIndex, std::vector<ValueType> const& x, ValueType& value) const {
69 for (auto const& entry : this->matrix.getRow(rowIndex)) {
70 value += entry.getValue() * x[entry.getColumn()];
71 }
72}
73
74template<typename ValueType>
75void NativeMultiplier<ValueType>::multiplyRow2(uint64_t const& rowIndex, std::vector<ValueType> const& x1, ValueType& val1, std::vector<ValueType> const& x2,
76 ValueType& val2) const {
77 for (auto const& entry : this->matrix.getRow(rowIndex)) {
78 val1 += entry.getValue() * x1[entry.getColumn()];
79 val2 += entry.getValue() * x2[entry.getColumn()];
80 }
81}
82
83template<typename ValueType>
84void NativeMultiplier<ValueType>::multAdd(std::vector<ValueType> const& x, std::vector<ValueType> const* b, std::vector<ValueType>& result) const {
85 this->matrix.multiplyWithVector(x, result, b);
86}
87
88template<typename ValueType>
89void NativeMultiplier<ValueType>::multAddReduce(storm::solver::OptimizationDirection const& dir, std::vector<uint64_t> const& rowGroupIndices,
90 std::vector<ValueType> const& x, std::vector<ValueType> const* b, std::vector<ValueType>& result,
91 std::vector<uint64_t>* choices) const {
92 this->matrix.multiplyAndReduce(dir, rowGroupIndices, x, b, result, choices);
93}
94
95template class NativeMultiplier<double>;
96template class NativeMultiplier<storm::RationalNumber>;
97template class NativeMultiplier<storm::RationalFunction>;
98template class NativeMultiplier<storm::Interval>;
99
100} // namespace solver
101} // namespace storm
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 override
void multiplyRow(uint64_t const &rowIndex, std::vector< ValueType > const &x, ValueType &value) const
Multiplies the row with the given index with x and adds the result to the provided value.
NativeMultiplier(storm::storage::SparseMatrix< ValueType > const &matrix)
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 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 override
virtual void multiplyGaussSeidel(Environment const &env, std::vector< ValueType > &x, std::vector< ValueType > const *b, bool backwards=true) const override
Performs a matrix-vector multiplication in gauss-seidel style.
virtual void multiply(Environment const &env, std::vector< ValueType > const &x, std::vector< ValueType > const *b, std::vector< ValueType > &result) const override
Performs a matrix-vector multiplication x' = A*x + b.
A class that holds a possibly non-square matrix in the compressed row storage format.
LabParser.cpp.
Definition cli.cpp:18