3#include "storm-config.h"
25template<
typename ValueType>
30template<
typename ValueType>
35template<
typename ValueType>
37 std::vector<ValueType>
const* b, std::vector<ValueType>& result, std::vector<uint_fast64_t>* choices)
const {
38 multiplyAndReduce(env, dir, this->matrix.getRowGroupIndices(), x, b, result, choices);
41template<
typename ValueType>
43 std::vector<ValueType>
const* b, std::vector<uint_fast64_t>* choices,
bool backwards)
const {
44 multiplyAndReduceGaussSeidel(env, dir, this->matrix.getRowGroupIndices(), x, b, choices, backwards);
47template<
typename ValueType>
52 for (uint64_t i = 0; i < n; ++i) {
54 multiply(env, x, b, x);
56 STORM_LOG_WARN(
"Aborting after " << i <<
" of " << n <<
" multiplications.");
62template<
typename ValueType>
64 std::vector<ValueType>
const* b, uint64_t n)
const {
68 for (uint64_t i = 0; i < n; ++i) {
69 multiplyAndReduce(env, dir, x, b, x);
71 STORM_LOG_WARN(
"Aborting after " << i <<
" of " << n <<
" multiplications");
77template<
typename ValueType>
80 if (this->cachedVector) {
81 this->cachedVector->resize(size);
83 this->cachedVector = std::make_unique<std::vector<ValueType>>(size);
85 return *this->cachedVector;
88template<
typename ValueType>
93 if (type == MultiplierType::ViOperator && (std::is_same_v<ValueType, storm::RationalFunction> || std::is_same_v<ValueType, storm::Interval>)) {
94 STORM_LOG_INFO(
"Switching multiplier type from 'vioperator' to 'native' because the given ValueType is not supported by the VI Operator multiplier.");
95 type = MultiplierType::Native;
99 case MultiplierType::ViOperator:
100 if constexpr (std::is_same_v<ValueType, storm::RationalFunction> || std::is_same_v<ValueType, storm::Interval>) {
101 throw storm::exceptions::NotImplementedException() <<
"VI Operator multiplier not supported with given value type.";
104 return std::make_unique<ViOperatorMultiplier<ValueType, true>>(matrix);
106 return std::make_unique<ViOperatorMultiplier<ValueType, false>>(matrix);
108 case MultiplierType::Native:
109 return std::make_unique<NativeMultiplier<ValueType>>(matrix);
111 STORM_LOG_THROW(
false, storm::exceptions::IllegalArgumentException,
"Unknown MultiplierType");
SolverEnvironment & solver()
storm::solver::MultiplierType const & getType() const
MultiplierEnvironment & multiplier()
std::unique_ptr< Multiplier< ValueType > > create(Environment const &env, storm::storage::SparseMatrix< ValueType > const &matrix)
std::vector< ValueType > & provideCachedVector(uint64_t size) const
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...
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.
Multiplier(storm::storage::SparseMatrix< ValueType > const &matrix)
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...
A class that holds a possibly non-square matrix in the compressed row storage format.
bool hasTrivialRowGrouping() const
Retrieves whether the matrix has a trivial row grouping.
A class that provides convenience operations to display run times.
bool updateProgress(uint64_t count)
Updates the progress to the current count and prints it if the delay passed.
void setMaxCount(uint64_t maxCount)
Sets the maximal possible count.
void startNewMeasurement(uint64_t startCount)
Starts a new measurement, dropping all progress information collected so far.
#define STORM_LOG_INFO(message)
#define STORM_LOG_WARN(message)
#define STORM_LOG_THROW(cond, exception, message)
bool isTerminate()
Check whether the program should terminate (due to some abort signal).