17template<storm::dd::DdType DdType,
typename ValueType>
22template<storm::dd::DdType DdType,
typename ValueType>
25 std::set<storm::expressions::Variable>
const& columnMetaVariables,
26 std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>>
const& rowColumnMetaVariablePairs)
31template<storm::dd::DdType DdType,
typename ValueType>
34 std::set<storm::expressions::Variable>
const& columnMetaVariables,
35 std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>>
const& rowColumnMetaVariablePairs)
40template<storm::dd::DdType DdType,
typename ValueType>
47 if (method != NativeLinearEquationSolverMethod::RationalSearch) {
49 method = NativeLinearEquationSolverMethod::RationalSearch;
52 "' as the solution technique to guarantee exact results. If you want to override this, please explicitly specify a different method.");
54 STORM_LOG_WARN(
"The selected solution method does not guarantee exact results.");
58 if (method != NativeLinearEquationSolverMethod::Power && method != NativeLinearEquationSolverMethod::RationalSearch &&
59 method != NativeLinearEquationSolverMethod::Jacobi) {
60 method = NativeLinearEquationSolverMethod::Jacobi;
61 STORM_LOG_INFO(
"The selected solution method is not supported in the dd engine. Falling back to '" +
toString(method) +
"'.");
68template<storm::dd::DdType DdType,
typename ValueType>
72 switch (getMethod(env, std::is_same<ValueType, storm::RationalNumber>::value)) {
73 case NativeLinearEquationSolverMethod::Jacobi:
74 return solveEquationsJacobi(env, x, b);
75 case NativeLinearEquationSolverMethod::Power:
76 return solveEquationsPower(env, x, b);
77 case NativeLinearEquationSolverMethod::RationalSearch:
78 return solveEquationsRationalSearch(env, x, b);
80 STORM_LOG_THROW(
false, storm::exceptions::NotSupportedException,
"The selected solution technique is not supported.");
85template<storm::dd::DdType DdType,
typename ValueType>
94 STORM_LOG_INFO(
"Solving symbolic linear equation system with NativeLinearEquationSolver (jacobi)");
98 diagonal &= this->allRows;
109 uint_fast64_t iterationCount = 0;
110 bool converged =
false;
112 while (!converged && iterationCount < maxIter) {
126 STORM_LOG_INFO(
"Iterative solver (jacobi) converged in " << iterationCount <<
" iterations.");
128 STORM_LOG_WARN(
"Iterative solver (jacobi) did not converge in " << iterationCount <<
" iterations.");
134template<storm::dd::DdType DdType,
typename ValueType>
135typename SymbolicNativeLinearEquationSolver<DdType, ValueType>::PowerIterationResult
138 bool relativeTerminationCriterion, uint64_t maximalIterations)
const {
141 uint_fast64_t iterations = 0;
158 return PowerIterationResult(status, iterations, currentX);
161template<storm::dd::DdType DdType,
typename ValueType>
165 STORM_LOG_INFO(
"Solving symbolic linear equation system with NativeLinearEquationSolver (power)");
166 ValueType precision = storm::utility::convertNumber<ValueType>(env.solver().native().getPrecision());
167 PowerIterationResult result =
168 performPowerIteration(x, b, precision, env.solver().native().getRelativeTerminationCriterion(), env.solver().native().getMaximalNumberOfIterations());
171 STORM_LOG_INFO(
"Iterative solver (power iteration) converged in " << result.iterations <<
" iterations.");
173 STORM_LOG_WARN(
"Iterative solver (power iteration) did not converge in " << result.iterations <<
" iterations.");
176 return result.values;
179template<storm::dd::DdType DdType,
typename ValueType>
189template<storm::dd::DdType DdType,
typename ValueType>
190template<
typename RationalType,
typename ImpreciseType>
196 for (uint64_t p = 1; p <= precision; ++p) {
199 isSolution = rationalSolver.isSolutionFixedPoint(sharpenedX, rationalB);
208template<storm::dd::DdType DdType,
typename ValueType>
209template<
typename RationalType,
typename ImpreciseType>
211 Environment
const& env, SymbolicNativeLinearEquationSolver<DdType, RationalType>
const& rationalSolver,
219 uint64_t overallIterations = 0;
220 uint64_t powerIterationInvocations = 0;
221 ValueType precision = storm::utility::convertNumber<ValueType>(env.solver().native().getPrecision());
222 uint64_t maxIter = env.solver().native().getMaximalNumberOfIterations();
223 bool relative = env.solver().native().getRelativeTerminationCriterion();
226 typename SymbolicNativeLinearEquationSolver<DdType, ImpreciseType>::PowerIterationResult result = impreciseSolver.performPowerIteration(
227 currentX, b, storm::utility::convertNumber<ImpreciseType, ValueType>(precision), relative, maxIter - overallIterations);
229 ++powerIterationInvocations;
230 STORM_LOG_TRACE(
"Completed " << powerIterationInvocations <<
" power iteration invocations, the last one with precision " << precision
231 <<
" completed in " << result.iterations <<
" iterations.");
234 overallIterations += result.iterations;
238 storm::utility::convertNumber<uint64_t>(
storm::utility::ceil(storm::utility::log10<ValueType>(storm::utility::one<ValueType>() / precision)));
240 bool isSolution =
false;
241 sharpenedX = sharpen<RationalType, ImpreciseType>(p, rationalSolver, result.values, rationalB, isSolution);
246 currentX = result.values;
247 precision /= storm::utility::convertNumber<ValueType, uint64_t>(10);
259 STORM_LOG_INFO(
"Iterative solver (rational search) converged in " << overallIterations <<
" iterations.");
261 STORM_LOG_WARN(
"Iterative solver (rational search) did not converge in " << overallIterations <<
" iterations.");
267template<storm::dd::DdType DdType,
typename ValueType>
268template<
typename ImpreciseType>
272 return solveEquationsRationalSearchHelper<ValueType, ValueType>(env, *
this, *
this, b, this->getLowerBoundsVector(), b);
275template<storm::dd::DdType DdType,
typename ValueType>
276template<
typename ImpreciseType>
281 SymbolicNativeLinearEquationSolver<DdType, storm::RationalNumber> rationalSolver(this->A.template toValueType<storm::RationalNumber>(), this->allRows,
282 this->rowMetaVariables, this->columnMetaVariables,
283 this->rowColumnMetaVariablePairs);
286 solveEquationsRationalSearchHelper<storm::RationalNumber, ImpreciseType>(env, rationalSolver, *
this, rationalB, this->getLowerBoundsVector(), b);
287 return rationalResult.template toValueType<ValueType>();
290template<storm::dd::DdType DdType,
typename ValueType>
291template<
typename ImpreciseType>
299 impreciseX = this->getLowerBoundsVector().template toValueType<ImpreciseType>();
301 SymbolicNativeLinearEquationSolver<DdType, ImpreciseType> impreciseSolver(
302 this->A.template toValueType<ImpreciseType>(), this->allRows, this->rowMetaVariables, this->columnMetaVariables, this->rowColumnMetaVariablePairs);
304 rationalResult = solveEquationsRationalSearchHelper<ValueType, ImpreciseType>(env, *
this, impreciseSolver, b, impreciseX, impreciseB);
305 }
catch (storm::exceptions::PrecisionExceededException
const& e) {
306 STORM_LOG_WARN(
"Precision of value type was exceeded, trying to recover by switching to rational arithmetic.");
309 rationalResult = solveEquationsRationalSearchHelper<ValueType, ValueType>(env, *
this, *
this, b, impreciseX.template toValueType<ValueType>(), b);
311 return rationalResult.template toValueType<ValueType>();
314template<storm::dd::DdType DdType,
typename ValueType>
317 STORM_LOG_INFO(
"Solving symbolic linear equation system with NativeLinearEquationSolver (rational search)");
318 return solveEquationsRationalSearchHelper<double>(env, x, b);
321template<storm::dd::DdType DdType,
typename ValueType>
323 auto method = getMethod(env, std::is_same<ValueType, storm::RationalNumber>::value);
324 if (method == NativeLinearEquationSolverMethod::Jacobi) {
330template<storm::dd::DdType DdType,
typename ValueType>
333 auto method = getMethod(env, std::is_same<ValueType, storm::RationalNumber>::value);
334 if (method == NativeLinearEquationSolverMethod::RationalSearch) {
340template<storm::dd::DdType DdType,
typename ValueType>
343 return std::make_unique<SymbolicNativeLinearEquationSolver<DdType, ValueType>>();
SolverEnvironment & solver()
storm::RationalNumber const & getPrecision() const
uint64_t const & getMaximalNumberOfIterations() const
bool const & isMethodSetFromDefault() const
bool const & getRelativeTerminationCriterion() const
storm::solver::NativeLinearEquationSolverMethod const & getMethod() const
NativeSolverEnvironment & native()
bool isForceSoundness() const
Add< LibraryType, ValueType > swapVariables(std::vector< std::pair< storm::expressions::Variable, storm::expressions::Variable > > const &metaVariablePairs) const
Swaps the given pairs of meta variables in the ADD.
Add< LibraryType, storm::RationalNumber > sharpenKwekMehlhorn(uint64_t precision) const
Retrieves the function that sharpens all values in the current ADD with the Kwek-Mehlhorn algorithm.
Add< LibraryType, ValueType > multiplyMatrix(Add< LibraryType, ValueType > const &otherMatrix, std::set< storm::expressions::Variable > const &summationMetaVariables) const
Multiplies the current ADD (representing a matrix) with the given matrix by summing over the given me...
bool equalModuloPrecision(Add< LibraryType, ValueType > const &other, ValueType const &precision, bool relative=true) const
Checks whether the current and the given ADD represent the same function modulo some given precision.
Bdd< LibraryType > ite(Bdd< LibraryType > const &thenBdd, Bdd< LibraryType > const &elseBdd) const
Performs an if-then-else with the given operands, i.e.
DdManager< LibraryType > & getDdManager() const
Retrieves the manager that is responsible for this DD.
LinearEquationSolverRequirements & requireLowerBounds(bool critical=true)
An interface that represents an abstract symbolic linear equation solver.
void setMatrix(storm::dd::Add< DdType, ValueType > const &newA)
virtual std::unique_ptr< storm::solver::SymbolicLinearEquationSolver< DdType, ValueType > > create(Environment const &env) const override
An interface that represents an abstract symbolic linear equation solver.
virtual LinearEquationSolverRequirements getRequirements(Environment const &env) const override
Retrieves the requirements of the solver under the current settings.
virtual storm::dd::Add< DdType, ValueType > solveEquations(Environment const &env, storm::dd::Add< DdType, ValueType > const &x, storm::dd::Add< DdType, ValueType > const &b) const override
Solves the equation system A*x = b.
friend class SymbolicNativeLinearEquationSolver
virtual LinearEquationSolverProblemFormat getEquationProblemFormat(Environment const &env) const override
Retrieves the format in which this solver expects to solve equations.
#define STORM_LOG_INFO(message)
#define STORM_LOG_WARN(message)
#define STORM_LOG_TRACE(message)
#define STORM_LOG_THROW(cond, exception, message)
#define STORM_LOG_WARN_COND_DEBUG(cond, message)
SFTBDDChecker::ValueType ValueType
LinearEquationSolverProblemFormat
std::string toString(GurobiSolverMethod const &method)
Yields a string representation of the GurobiSolverMethod.
@ MaximalIterationsExceeded
storm::dd::Bdd< Type > getRowColumnDiagonal(storm::dd::DdManager< Type > const &ddManager, std::vector< std::pair< storm::expressions::Variable, storm::expressions::Variable > > const &rowColumnMetaVariablePairs)
bool isTerminate()
Check whether the program should terminate (due to some abort signal).
ValueType ceil(ValueType const &number)