#include "storm/solver/EigenLinearEquationSolver.h" #include "storm/adapters/EigenAdapter.h" #include "storm/environment/solver/EigenSolverEnvironment.h" #include "storm/utility/vector.h" #include "storm/utility/macros.h" #include "storm/exceptions/InvalidSettingsException.h" namespace storm { namespace solver { template EigenLinearEquationSolver::EigenLinearEquationSolver() { // Intentionally left empty. } template EigenLinearEquationSolver::EigenLinearEquationSolver(storm::storage::SparseMatrix const& A) { this->setMatrix(A); } template EigenLinearEquationSolver::EigenLinearEquationSolver(storm::storage::SparseMatrix&& A) { this->setMatrix(std::move(A)); } template void EigenLinearEquationSolver::setMatrix(storm::storage::SparseMatrix const& A) { eigenA = storm::adapters::EigenAdapter::toEigenSparseMatrix(A); this->clearCache(); } template void EigenLinearEquationSolver::setMatrix(storm::storage::SparseMatrix&& A) { // Take ownership of the matrix so it is destroyed after we have translated it to Eigen's format. storm::storage::SparseMatrix localA(std::move(A)); this->setMatrix(localA); this->clearCache(); } template EigenLinearEquationSolverMethod EigenLinearEquationSolver::getMethod(Environment const& env, bool isExactMode) const { // Adjust the method if none was specified and we are using rational numbers. auto method = env.solver().eigen().getMethod(); if (isExactMode && method != EigenLinearEquationSolverMethod::SparseLU) { if (env.solver().eigen().isMethodSetFromDefault()) { STORM_LOG_INFO("Selecting 'SparseLU' as the solution technique to guarantee exact results."); } else { STORM_LOG_WARN("The selected solution method does not guarantee exact results. Falling back to SparseLU."); } method = EigenLinearEquationSolverMethod::SparseLU; } else if (env.solver().isForceSoundness() && method != EigenLinearEquationSolverMethod::SparseLU) { if (env.solver().eigen().isMethodSetFromDefault()) { STORM_LOG_INFO("Selecting 'SparseLU' as the solution technique to guarantee sound results. If you want to override this, please explicitly specify a different method."); method = EigenLinearEquationSolverMethod::SparseLU; } else { STORM_LOG_WARN("The selected solution method does not guarantee sound results."); } } return method; } #ifdef STORM_HAVE_CARL // Specialization for storm::RationalNumber template<> bool EigenLinearEquationSolver::internalSolveEquations(Environment const& env, std::vector& x, std::vector const& b) const { auto solutionMethod = getMethod(env, true); STORM_LOG_WARN_COND(solutionMethod == EigenLinearEquationSolverMethod::SparseLU, "Switching method to SparseLU."); STORM_LOG_INFO("Solving linear equation system (" << x.size() << " rows) with with rational numbers using LU factorization (Eigen library)."); // Map the input vectors to Eigen's format. auto eigenX = Eigen::Matrix::Map(x.data(), x.size()); auto eigenB = Eigen::Matrix::Map(b.data(), b.size()); Eigen::SparseLU, Eigen::COLAMDOrdering> solver; solver.compute(*eigenA); solver._solve_impl(eigenB, eigenX); return solver.info() == Eigen::ComputationInfo::Success; } // Specialization for storm::RationalFunction template<> bool EigenLinearEquationSolver::internalSolveEquations(Environment const& env, std::vector& x, std::vector const& b) const { auto solutionMethod = getMethod(env, true); STORM_LOG_WARN_COND(solutionMethod == EigenLinearEquationSolverMethod::SparseLU, "Switching method to SparseLU."); STORM_LOG_INFO("Solving linear equation system (" << x.size() << " rows) with rational functions using LU factorization (Eigen library)."); // Map the input vectors to Eigen's format. auto eigenX = Eigen::Matrix::Map(x.data(), x.size()); auto eigenB = Eigen::Matrix::Map(b.data(), b.size()); Eigen::SparseLU, Eigen::COLAMDOrdering> solver; solver.compute(*eigenA); solver._solve_impl(eigenB, eigenX); return solver.info() == Eigen::ComputationInfo::Success; } #endif template bool EigenLinearEquationSolver::internalSolveEquations(Environment const& env, std::vector& x, std::vector const& b) const { // Map the input vectors to Eigen's format. auto eigenX = Eigen::Matrix::Map(x.data(), x.size()); auto eigenB = Eigen::Matrix::Map(b.data(), b.size()); auto solutionMethod = getMethod(env, env.solver().isForceExact()); if (solutionMethod == EigenLinearEquationSolverMethod::SparseLU) { STORM_LOG_INFO("Solving linear equation system (" << x.size() << " rows) with sparse LU factorization (Eigen library)."); Eigen::SparseLU, Eigen::COLAMDOrdering> solver; solver.compute(*this->eigenA); solver._solve_impl(eigenB, eigenX); } else { bool converged = false; uint64_t numberOfIterations = 0; Eigen::Index maxIter = std::numeric_limits::max(); if (env.solver().eigen().getMaximalNumberOfIterations() < static_cast(maxIter)) { maxIter = env.solver().eigen().getMaximalNumberOfIterations(); } uint64_t restartThreshold = env.solver().eigen().getRestartThreshold(); ValueType precision = storm::utility::convertNumber(env.solver().eigen().getPrecision()); EigenLinearEquationSolverPreconditioner preconditioner = env.solver().eigen().getPreconditioner(); if (solutionMethod == EigenLinearEquationSolverMethod::Bicgstab) { if (preconditioner == EigenLinearEquationSolverPreconditioner::Ilu) { STORM_LOG_INFO("Solving linear equation system (" << x.size() << " rows) with BiCGSTAB with Ilu preconditioner (Eigen library)."); Eigen::BiCGSTAB, Eigen::IncompleteLUT> solver; solver.compute(*this->eigenA); solver.setTolerance(precision); solver.setMaxIterations(maxIter); eigenX = solver.solveWithGuess(eigenB, eigenX); converged = solver.info() == Eigen::ComputationInfo::Success; numberOfIterations = solver.iterations(); } else if (preconditioner == EigenLinearEquationSolverPreconditioner::Diagonal) { STORM_LOG_INFO("Solving linear equation system (" << x.size() << " rows) with BiCGSTAB with Diagonal preconditioner (Eigen library)."); Eigen::BiCGSTAB, Eigen::DiagonalPreconditioner> solver; solver.setTolerance(precision); solver.setMaxIterations(maxIter); solver.compute(*this->eigenA); eigenX = solver.solveWithGuess(eigenB, eigenX); converged = solver.info() == Eigen::ComputationInfo::Success; numberOfIterations = solver.iterations(); } else { STORM_LOG_INFO("Solving linear equation system (" << x.size() << " rows) with BiCGSTAB with identity preconditioner (Eigen library)."); Eigen::BiCGSTAB, Eigen::IdentityPreconditioner> solver; solver.setTolerance(precision); solver.setMaxIterations(maxIter); solver.compute(*this->eigenA); eigenX = solver.solveWithGuess(eigenB, eigenX); numberOfIterations = solver.iterations(); converged = solver.info() == Eigen::ComputationInfo::Success; } } else if (solutionMethod == EigenLinearEquationSolverMethod::DGmres) { if (preconditioner == EigenLinearEquationSolverPreconditioner::Ilu) { STORM_LOG_INFO("Solving linear equation system (" << x.size() << " rows) with DGMRES with Ilu preconditioner (Eigen library)."); Eigen::DGMRES, Eigen::IncompleteLUT> solver; solver.setTolerance(precision); solver.setMaxIterations(maxIter); solver.set_restart(restartThreshold); solver.compute(*this->eigenA); eigenX = solver.solveWithGuess(eigenB, eigenX); converged = solver.info() == Eigen::ComputationInfo::Success; numberOfIterations = solver.iterations(); } else if (preconditioner == EigenLinearEquationSolverPreconditioner::Diagonal) { STORM_LOG_INFO("Solving linear equation system (" << x.size() << " rows) with DGMRES with Diagonal preconditioner (Eigen library)."); Eigen::DGMRES, Eigen::DiagonalPreconditioner> solver; solver.setTolerance(precision); solver.setMaxIterations(maxIter); solver.set_restart(restartThreshold); solver.compute(*this->eigenA); eigenX = solver.solveWithGuess(eigenB, eigenX); converged = solver.info() == Eigen::ComputationInfo::Success; numberOfIterations = solver.iterations(); } else { STORM_LOG_INFO("Solving linear equation system (" << x.size() << " rows) with DGMRES with identity preconditioner (Eigen library)."); Eigen::DGMRES, Eigen::IdentityPreconditioner> solver; solver.setTolerance(precision); solver.setMaxIterations(maxIter); solver.set_restart(restartThreshold); solver.compute(*this->eigenA); eigenX = solver.solveWithGuess(eigenB, eigenX); converged = solver.info() == Eigen::ComputationInfo::Success; numberOfIterations = solver.iterations(); } } else if (solutionMethod == EigenLinearEquationSolverMethod::Gmres) { if (preconditioner == EigenLinearEquationSolverPreconditioner::Ilu) { STORM_LOG_INFO("Solving linear equation system (" << x.size() << " rows) with GMRES with Ilu preconditioner (Eigen library)."); Eigen::GMRES, Eigen::IncompleteLUT> solver; solver.setTolerance(precision); solver.setMaxIterations(maxIter); solver.set_restart(restartThreshold); solver.compute(*this->eigenA); eigenX = solver.solveWithGuess(eigenB, eigenX); converged = solver.info() == Eigen::ComputationInfo::Success; numberOfIterations = solver.iterations(); } else if (preconditioner == EigenLinearEquationSolverPreconditioner::Diagonal) { STORM_LOG_INFO("Solving linear equation system (" << x.size() << " rows) with GMRES with Diagonal preconditioner (Eigen library)."); Eigen::GMRES, Eigen::DiagonalPreconditioner> solver; solver.setTolerance(precision); solver.setMaxIterations(maxIter); solver.set_restart(restartThreshold); solver.compute(*this->eigenA); eigenX = solver.solveWithGuess(eigenB, eigenX); converged = solver.info() == Eigen::ComputationInfo::Success; numberOfIterations = solver.iterations(); } else { STORM_LOG_INFO("Solving linear equation system (" << x.size() << " rows) with GMRES with identity preconditioner (Eigen library)."); Eigen::GMRES, Eigen::IdentityPreconditioner> solver; solver.setTolerance(precision); solver.setMaxIterations(maxIter); solver.set_restart(restartThreshold); solver.compute(*this->eigenA); eigenX = solver.solveWithGuess(eigenB, eigenX); converged = solver.info() == Eigen::ComputationInfo::Success; numberOfIterations = solver.iterations(); } } // Make sure that all results conform to the (global) bounds. storm::utility::vector::clip(x, this->lowerBound, this->upperBound); // Check if the solver converged and issue a warning otherwise. if (converged) { STORM_LOG_INFO("Iterative solver converged after " << numberOfIterations << " iterations."); return true; } else { STORM_LOG_WARN("Iterative solver did not converge."); return false; } } return true; } template LinearEquationSolverProblemFormat EigenLinearEquationSolver::getEquationProblemFormat(Environment const&) const { return LinearEquationSolverProblemFormat::EquationSystem; } template uint64_t EigenLinearEquationSolver::getMatrixRowCount() const { return eigenA->rows(); } template uint64_t EigenLinearEquationSolver::getMatrixColumnCount() const { return eigenA->cols(); } template std::unique_ptr> EigenLinearEquationSolverFactory::create(Environment const&) const { return std::make_unique>(); } template std::unique_ptr> EigenLinearEquationSolverFactory::clone() const { return std::make_unique>(*this); } template class EigenLinearEquationSolver; template class EigenLinearEquationSolverFactory; #ifdef STORM_HAVE_CARL template class EigenLinearEquationSolver; template class EigenLinearEquationSolver; template class EigenLinearEquationSolverFactory; template class EigenLinearEquationSolverFactory; #endif } }