Storm
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
6
8
12
14
15namespace storm {
16namespace solver {
17
18template<typename ValueType>
20 // Intentionally left empty.
21}
22
23template<typename ValueType>
25 return false;
26}
27
28template<typename ValueType>
29void NativeMultiplier<ValueType>::multiply(Environment const& env, std::vector<ValueType> const& x, std::vector<ValueType> const* b,
30 std::vector<ValueType>& result) const {
31 std::vector<ValueType>* target = &result;
32 if (&x == &result) {
33 if (this->cachedVector) {
34 this->cachedVector->resize(x.size());
35 } else {
36 this->cachedVector = std::make_unique<std::vector<ValueType>>(x.size());
37 }
38 target = this->cachedVector.get();
39 }
40 if (parallelize(env)) {
41 multAddParallel(x, b, *target);
42 } else {
43 multAdd(x, b, *target);
44 }
45 if (&x == &result) {
46 std::swap(result, *this->cachedVector);
47 }
48}
49
50template<typename ValueType>
51void NativeMultiplier<ValueType>::multiplyGaussSeidel(Environment const& env, std::vector<ValueType>& x, std::vector<ValueType> const* b,
52 bool backwards) const {
53 if (backwards) {
54 this->matrix.multiplyWithVectorBackward(x, x, b);
55 } else {
56 this->matrix.multiplyWithVectorForward(x, x, b);
57 }
58}
59
60template<typename ValueType>
61void NativeMultiplier<ValueType>::multiplyAndReduce(Environment const& env, OptimizationDirection const& dir, std::vector<uint64_t> const& rowGroupIndices,
62 std::vector<ValueType> const& x, std::vector<ValueType> const* b, std::vector<ValueType>& result,
63 std::vector<uint_fast64_t>* choices) const {
64 std::vector<ValueType>* target = &result;
65 if (&x == &result) {
66 if (this->cachedVector) {
67 this->cachedVector->resize(x.size());
68 } else {
69 this->cachedVector = std::make_unique<std::vector<ValueType>>(x.size());
70 }
71 target = this->cachedVector.get();
72 }
73 if (parallelize(env)) {
74 multAddReduceParallel(dir, rowGroupIndices, x, b, *target, choices);
75 } else {
76 multAddReduce(dir, rowGroupIndices, x, b, *target, choices);
77 }
78 if (&x == &result) {
79 std::swap(result, *this->cachedVector);
80 }
81}
82
83template<typename ValueType>
85 std::vector<uint64_t> const& rowGroupIndices, std::vector<ValueType>& x,
86 std::vector<ValueType> const* b, std::vector<uint_fast64_t>* choices, bool backwards) const {
87 if (backwards) {
88 this->matrix.multiplyAndReduceBackward(dir, rowGroupIndices, x, b, x, choices);
89 } else {
90 this->matrix.multiplyAndReduceForward(dir, rowGroupIndices, x, b, x, choices);
91 }
92}
93
94template<typename ValueType>
95void NativeMultiplier<ValueType>::multiplyRow(uint64_t const& rowIndex, std::vector<ValueType> const& x, ValueType& value) const {
96 for (auto const& entry : this->matrix.getRow(rowIndex)) {
97 value += entry.getValue() * x[entry.getColumn()];
98 }
99}
100
101template<typename ValueType>
102void NativeMultiplier<ValueType>::multiplyRow2(uint64_t const& rowIndex, std::vector<ValueType> const& x1, ValueType& val1, std::vector<ValueType> const& x2,
103 ValueType& val2) const {
104 for (auto const& entry : this->matrix.getRow(rowIndex)) {
105 val1 += entry.getValue() * x1[entry.getColumn()];
106 val2 += entry.getValue() * x2[entry.getColumn()];
107 }
108}
109
110template<typename ValueType>
111void NativeMultiplier<ValueType>::multAdd(std::vector<ValueType> const& x, std::vector<ValueType> const* b, std::vector<ValueType>& result) const {
112 this->matrix.multiplyWithVector(x, result, b);
113}
114
115template<typename ValueType>
116void NativeMultiplier<ValueType>::multAddReduce(storm::solver::OptimizationDirection const& dir, std::vector<uint64_t> const& rowGroupIndices,
117 std::vector<ValueType> const& x, std::vector<ValueType> const* b, std::vector<ValueType>& result,
118 std::vector<uint64_t>* choices) const {
119 this->matrix.multiplyAndReduce(dir, rowGroupIndices, x, b, result, choices);
120}
121
122template<typename ValueType>
123void NativeMultiplier<ValueType>::multAddParallel(std::vector<ValueType> const& x, std::vector<ValueType> const* b, std::vector<ValueType>& result) const {
124#ifdef STORM_HAVE_INTELTBB
125 this->matrix.multiplyWithVectorParallel(x, result, b);
126#else
127 STORM_LOG_WARN("Storm was built without support for Intel TBB, defaulting to sequential version.");
128 multAdd(x, b, result);
129#endif
130}
131
132template<typename ValueType>
133void NativeMultiplier<ValueType>::multAddReduceParallel(storm::solver::OptimizationDirection const& dir, std::vector<uint64_t> const& rowGroupIndices,
134 std::vector<ValueType> const& x, std::vector<ValueType> const* b, std::vector<ValueType>& result,
135 std::vector<uint64_t>* choices) const {
136#ifdef STORM_HAVE_INTELTBB
137 this->matrix.multiplyAndReduceParallel(dir, rowGroupIndices, x, b, result, choices);
138#else
139 STORM_LOG_WARN("Storm was built without support for Intel TBB, defaulting to sequential version.");
140 multAddReduce(dir, rowGroupIndices, x, b, result, choices);
141#endif
142}
143
144template class NativeMultiplier<double>;
145template class NativeMultiplier<storm::RationalNumber>;
146template class NativeMultiplier<storm::RationalFunction>;
147template class NativeMultiplier<storm::Interval>;
148
149} // namespace solver
150} // 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
virtual void multiplyRow2(uint64_t const &rowIndex, std::vector< ValueType > const &x1, ValueType &val1, std::vector< ValueType > const &x2, ValueType &val2) const override
Multiplies the row with the given index with x1 and x2 and adds the given offset o1 and o2,...
NativeMultiplier(storm::storage::SparseMatrix< ValueType > const &matrix)
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 multiplyRow(uint64_t const &rowIndex, std::vector< ValueType > const &x, ValueType &value) const override
Multiplies the row with the given index with x and adds the result to the provided value.
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.
#define STORM_LOG_WARN(message)
Definition logging.h:30
LabParser.cpp.
Definition cli.cpp:18