Storm 1.14.0.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
GmmxxLinearEquationSolver.cpp
Go to the documentation of this file.
2
3#include <utility>
4
12
13namespace storm {
14namespace solver {
15
16template<typename ValueType>
20
21template<typename ValueType>
25
26template<typename ValueType>
30
31template<typename ValueType>
33#ifdef STORM_HAVE_GMM
35 clearCache();
36#else
37 STORM_LOG_THROW(false, storm::exceptions::MissingLibraryException,
38 "This version of storm was compiled without support for GMM. Yet, a method was called that requires this support.");
39#endif
40}
41
42template<typename ValueType>
44#ifdef STORM_HAVE_GMM
46 clearCache();
47#else
48 STORM_LOG_THROW(false, storm::exceptions::MissingLibraryException,
49 "This version of storm was compiled without support for GMM. Yet, a method was called that requires this support.");
50#endif
51}
52
53template<typename ValueType>
54GmmxxLinearEquationSolverMethod GmmxxLinearEquationSolver<ValueType>::getMethod(Environment const& env) const {
55 STORM_LOG_ERROR_COND(!env.solver().isForceSoundness(), "This linear equation solver does not support sound computations. Using unsound methods now...");
56 STORM_LOG_ERROR_COND(!env.solver().isForceExact(), "This linear equation solver does not support exact computations. Using unsound methods now...");
57 return env.solver().gmmxx().getMethod();
58}
59
60template<typename ValueType>
61bool GmmxxLinearEquationSolver<ValueType>::internalSolveEquations(Environment const& env, std::vector<ValueType>& x, std::vector<ValueType> const& b) const {
62#ifdef STORM_HAVE_GMM
63 auto method = getMethod(env);
64 auto preconditioner = env.solver().gmmxx().getPreconditioner();
65
66 STORM_LOG_INFO("Solving linear equation system (" << x.size() << " rows) with Gmmxx linear equation solver with method '" << toString(method)
67 << "' and preconditioner '" << toString(preconditioner) << "'.");
68
69 if (method == GmmxxLinearEquationSolverMethod::Bicgstab || method == GmmxxLinearEquationSolverMethod::Qmr ||
70 method == GmmxxLinearEquationSolverMethod::Gmres) {
71 // Make sure that the requested preconditioner is available
72 if (preconditioner == GmmxxLinearEquationSolverPreconditioner::Ilu && !iluPreconditioner) {
73 iluPreconditioner = std::make_unique<gmm::ilu_precond<gmm::csr_matrix<ValueType>>>(*gmmxxA);
74 } else if (preconditioner == GmmxxLinearEquationSolverPreconditioner::Diagonal) {
75 diagonalPreconditioner = std::make_unique<gmm::diagonal_precond<gmm::csr_matrix<ValueType>>>(*gmmxxA);
76 }
77
78 // Prepare an iteration object that determines the accuracy and the maximum number of iterations.
79 gmm::size_type maxIter = std::numeric_limits<gmm::size_type>::max();
80 if (env.solver().gmmxx().getMaximalNumberOfIterations() < static_cast<uint64_t>(maxIter)) {
81 maxIter = env.solver().gmmxx().getMaximalNumberOfIterations();
82 }
83 gmm::iteration iter(storm::utility::convertNumber<ValueType>(env.solver().gmmxx().getPrecision()), 0, maxIter);
84 iter.set_callback([](const gmm::iteration& iteration) -> void {
85 STORM_LOG_THROW(!storm::utility::resources::isTerminate(), storm::exceptions::AbortException,
86 "Gmm++ (externally) aborted after " << iteration.get_iteration() << " iterations.");
87 });
88
89 // We use throwing an exception to abort within Gmm++
90 try {
91 // Invoke gmm with the corresponding settings
92 if (method == GmmxxLinearEquationSolverMethod::Bicgstab) {
93 if (preconditioner == GmmxxLinearEquationSolverPreconditioner::Ilu) {
94 gmm::bicgstab(*gmmxxA, x, b, *iluPreconditioner, iter);
95 } else if (preconditioner == GmmxxLinearEquationSolverPreconditioner::Diagonal) {
96 gmm::bicgstab(*gmmxxA, x, b, *diagonalPreconditioner, iter);
97 } else if (preconditioner == GmmxxLinearEquationSolverPreconditioner::None) {
98 gmm::bicgstab(*gmmxxA, x, b, gmm::identity_matrix(), iter);
99 }
100 } else if (method == GmmxxLinearEquationSolverMethod::Qmr) {
101 if (preconditioner == GmmxxLinearEquationSolverPreconditioner::Ilu) {
102 gmm::qmr(*gmmxxA, x, b, *iluPreconditioner, iter);
103 } else if (preconditioner == GmmxxLinearEquationSolverPreconditioner::Diagonal) {
104 gmm::qmr(*gmmxxA, x, b, *diagonalPreconditioner, iter);
105 } else if (preconditioner == GmmxxLinearEquationSolverPreconditioner::None) {
106 gmm::qmr(*gmmxxA, x, b, gmm::identity_matrix(), iter);
107 }
108 } else if (method == GmmxxLinearEquationSolverMethod::Gmres) {
109 if (preconditioner == GmmxxLinearEquationSolverPreconditioner::Ilu) {
110 gmm::gmres(*gmmxxA, x, b, *iluPreconditioner, env.solver().gmmxx().getRestartThreshold(), iter);
111 } else if (preconditioner == GmmxxLinearEquationSolverPreconditioner::Diagonal) {
112 gmm::gmres(*gmmxxA, x, b, *diagonalPreconditioner, env.solver().gmmxx().getRestartThreshold(), iter);
113 } else if (preconditioner == GmmxxLinearEquationSolverPreconditioner::None) {
114 gmm::gmres(*gmmxxA, x, b, gmm::identity_matrix(), env.solver().gmmxx().getRestartThreshold(), iter);
115 }
116 }
117 } catch (storm::exceptions::AbortException const&) {
118 // Do nothing
119 STORM_LOG_WARN("Gmm++ (externally) aborted.");
120 }
121
122 if (!this->isCachingEnabled()) {
123 clearCache();
124 }
125
126 // Make sure that all results conform to the bounds.
128
129 // Check if the solver converged and issue a warning otherwise.
130 if (iter.converged()) {
131 STORM_LOG_INFO("Iterative solver converged after " << iter.get_iteration() << " iteration(s).");
132 return true;
133 } else {
134 STORM_LOG_WARN("Iterative solver did not converge within " << iter.get_iteration() << " iteration(s).");
135 return false;
136 }
137 }
138
139 STORM_LOG_ERROR("Selected method is not available");
140 return false;
141#else
142 STORM_LOG_THROW(false, storm::exceptions::MissingLibraryException,
143 "This version of storm was compiled without support for GMM. Yet, a method was called that requires this support.");
144#endif
145}
146
147template<typename ValueType>
151
152template<typename ValueType>
154#ifdef STORM_HAVE_GMM
155 iluPreconditioner.reset();
156 diagonalPreconditioner.reset();
158#else
159 STORM_LOG_THROW(false, storm::exceptions::MissingLibraryException,
160 "This version of storm was compiled without support for GMM. Yet, a method was called that requires this support.");
161#endif
162}
163
164template<typename ValueType>
165uint64_t GmmxxLinearEquationSolver<ValueType>::getMatrixRowCount() const {
166#ifdef STORM_HAVE_GMM
167 return gmmxxA->nr;
168#else
169 STORM_LOG_THROW(false, storm::exceptions::MissingLibraryException,
170 "This version of storm was compiled without support for GMM. Yet, a method was called that requires this support.");
171#endif
172}
173
174template<typename ValueType>
175uint64_t GmmxxLinearEquationSolver<ValueType>::getMatrixColumnCount() const {
176#ifdef STORM_HAVE_GMM
177 return gmmxxA->nc;
178#else
179 STORM_LOG_THROW(false, storm::exceptions::MissingLibraryException,
180 "This version of storm was compiled without support for GMM. Yet, a method was called that requires this support.");
181#endif
182}
183
184template<typename ValueType>
185std::unique_ptr<storm::solver::LinearEquationSolver<ValueType>> GmmxxLinearEquationSolverFactory<ValueType>::create(Environment const& env) const {
186 return std::make_unique<storm::solver::GmmxxLinearEquationSolver<ValueType>>();
187}
188
189template<typename ValueType>
190std::unique_ptr<LinearEquationSolverFactory<ValueType>> GmmxxLinearEquationSolverFactory<ValueType>::clone() const {
191 return std::make_unique<GmmxxLinearEquationSolverFactory<ValueType>>(*this);
192}
193
194// Explicitly instantiate the solver.
197
198} // namespace solver
199} // namespace storm
SolverEnvironment & solver()
storm::RationalNumber const & getPrecision() const
uint64_t const & getMaximalNumberOfIterations() const
storm::solver::GmmxxLinearEquationSolverMethod const & getMethod() const
uint64_t const & getRestartThreshold() const
storm::solver::GmmxxLinearEquationSolverPreconditioner const & getPreconditioner() const
GmmxxSolverEnvironment & gmmxx()
virtual std::unique_ptr< LinearEquationSolverFactory< ValueType > > clone() const override
Creates a copy of this factory.
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.
A class that uses the gmm++ library to implement the LinearEquationSolver interface.
virtual bool internalSolveEquations(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 LinearEquationSolverProblemFormat getEquationProblemFormat(Environment const &env) const override
Retrieves the format in which this solver expects to solve equations.
bool isCachingEnabled() const
Retrieves whether some of the generated data during solver calls should be cached.
A class that holds a possibly non-square matrix in the compressed row storage format.
#define STORM_LOG_INFO(message)
Definition logging.h:27
#define STORM_LOG_WARN(message)
Definition logging.h:28
#define STORM_LOG_ERROR(message)
Definition logging.h:29
#define STORM_LOG_ERROR_COND(cond, message)
Definition macros.h:50
#define STORM_LOG_THROW(cond, exception, message)
Definition macros.h:28
std::string toString(GurobiSolverMethod const &method)
Yields a string representation of the GurobiSolverMethod.
bool isTerminate()
Check whether the program should terminate (due to some abort signal).
void clip(std::vector< ValueType > &x, boost::optional< ValueType > const &lowerBound, boost::optional< ValueType > const &upperBound)
Takes the input vector and ensures that all entries conform to the bounds.
Definition vector.h:888
TargetType convertNumber(SourceType const &number)