Storm 1.11.1.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
NativeLinearEquationSolver.h
Go to the documentation of this file.
1#ifndef STORM_SOLVER_NATIVELINEAREQUATIONSOLVER_H_
2#define STORM_SOLVER_NATIVELINEAREQUATIONSOLVER_H_
3
4#include <ostream>
5
7
12
14
15namespace storm {
16
17class Environment;
18
19namespace solver {
20
24template<typename ValueType>
26 public:
30
31 virtual void setMatrix(storm::storage::SparseMatrix<ValueType> const& A) override;
32 virtual void setMatrix(storm::storage::SparseMatrix<ValueType>&& A) override;
33
35 virtual LinearEquationSolverRequirements getRequirements(Environment const& env) const override;
36
37 virtual void clearCache() const override;
38
39 protected:
40 virtual bool internalSolveEquations(storm::Environment const& env, std::vector<ValueType>& x, std::vector<ValueType> const& b) const override;
41
42 private:
43 struct PowerIterationResult {
44 PowerIterationResult(uint64_t iterations, SolverStatus status) : iterations(iterations), status(status) {
45 // Intentionally left empty.
46 }
47
48 uint64_t iterations;
49 SolverStatus status;
50 };
51
52 template<typename ValueTypePrime>
54
55 PowerIterationResult performPowerIteration(Environment const& env, std::vector<ValueType>*& currentX, std::vector<ValueType>*& newX,
56 std::vector<ValueType> const& b, ValueType const& precision, bool relative, SolverGuarantee const& guarantee,
57 uint64_t currentIterations, uint64_t maxIterations,
58 storm::solver::MultiplicationStyle const& multiplicationStyle) const;
59
60 virtual uint64_t getMatrixRowCount() const override;
61 virtual uint64_t getMatrixColumnCount() const override;
62
63 NativeLinearEquationSolverMethod getMethod(Environment const& env, bool isExactMode) const;
64
65 virtual bool solveEquationsSOR(storm::Environment const& env, std::vector<ValueType>& x, std::vector<ValueType> const& b, ValueType const& omega) const;
66 virtual bool solveEquationsJacobi(storm::Environment const& env, std::vector<ValueType>& x, std::vector<ValueType> const& b) const;
67 virtual bool solveEquationsWalkerChae(storm::Environment const& env, std::vector<ValueType>& x, std::vector<ValueType> const& b) const;
68 virtual bool solveEquationsPower(storm::Environment const& env, std::vector<ValueType>& x, std::vector<ValueType> const& b) const;
69 virtual bool solveEquationsSoundValueIteration(storm::Environment const& env, std::vector<ValueType>& x, std::vector<ValueType> const& b) const;
70 virtual bool solveEquationsOptimisticValueIteration(storm::Environment const& env, std::vector<ValueType>& x, std::vector<ValueType> const& b) const;
71 virtual bool solveEquationsGuessingValueIteration(storm::Environment const& env, std::vector<ValueType>& x, std::vector<ValueType> const& b) const;
72 virtual bool solveEquationsIntervalIteration(storm::Environment const& env, std::vector<ValueType>& x, std::vector<ValueType> const& b) const;
73 virtual bool solveEquationsRationalSearch(storm::Environment const& env, std::vector<ValueType>& x, std::vector<ValueType> const& b) const;
74
75 void setUpViOperator() const;
76
77 // If the solver takes posession of the matrix, we store the moved matrix in this member, so it gets deleted
78 // when the solver is destructed.
79 std::unique_ptr<storm::storage::SparseMatrix<ValueType>> localA;
80
81 // A pointer to the original sparse matrix given to this solver. If the solver takes posession of the matrix
82 // the pointer refers to localA.
84
85 mutable std::shared_ptr<storm::solver::helper::ValueIterationOperator<ValueType, true>> viOperator;
86
87 // An object to dispatch all multiplication operations.
88 mutable std::unique_ptr<Multiplier<ValueType>> multiplier;
89
90 struct JacobiDecomposition {
91 JacobiDecomposition(Environment const& env, storm::storage::SparseMatrix<ValueType> const& A);
92
94 std::vector<ValueType> DVector;
95 std::unique_ptr<storm::solver::Multiplier<ValueType>> multiplier;
96 };
97 mutable std::unique_ptr<JacobiDecomposition> jacobiDecomposition;
98
99 struct WalkerChaeData {
100 WalkerChaeData(Environment const& env, storm::storage::SparseMatrix<ValueType> const& originalMatrix, std::vector<ValueType> const& originalB);
101
102 void computeWalkerChaeMatrix(storm::storage::SparseMatrix<ValueType> const& originalMatrix);
103 void computeNewB(std::vector<ValueType> const& originalB);
104 void precomputeAuxiliaryData();
105
107 std::vector<ValueType> b;
108 ValueType t;
109 std::unique_ptr<storm::solver::Multiplier<ValueType>> multiplier;
110
111 // Auxiliary data.
112 std::vector<ValueType> columnSums;
113 std::vector<ValueType> newX;
114 };
115 mutable std::unique_ptr<WalkerChaeData> walkerChaeData;
116};
117
118template<typename ValueType>
120 public:
122
123 virtual std::unique_ptr<storm::solver::LinearEquationSolver<ValueType>> create(Environment const& env) const override;
124
125 virtual std::unique_ptr<LinearEquationSolverFactory<ValueType>> clone() const override;
126};
127} // namespace solver
128} // namespace storm
129
130#endif /* STORM_SOLVER_NATIVELINEAREQUATIONSOLVER_H_ */
An interface that represents an abstract linear equation solver.
virtual std::unique_ptr< storm::solver::LinearEquationSolver< ValueType > > create(Environment const &env) const override
Creates an equation solver with the current settings, but without a matrix.
virtual std::unique_ptr< LinearEquationSolverFactory< ValueType > > clone() const override
Creates a copy of this factory.
A class that uses storm's native matrix operations to implement the LinearEquationSolver interface.
virtual LinearEquationSolverProblemFormat getEquationProblemFormat(storm::Environment const &env) const override
Retrieves the format in which this solver expects to solve equations.
virtual bool internalSolveEquations(storm::Environment const &env, std::vector< ValueType > &x, std::vector< ValueType > const &b) const override
virtual void setMatrix(storm::storage::SparseMatrix< ValueType > const &A) override
virtual LinearEquationSolverRequirements getRequirements(Environment const &env) const override
Retrieves the requirements of the solver under the current settings.
A class that holds a possibly non-square matrix in the compressed row storage format.