automatically switching solvers if soundness is enforced

src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp

@@ -256,7 +256,7 @@ namespace storm {
                         // Initialize the x vector with the hint (if available) or with 1 for each element.
                         // This is the initial guess for the iterative solvers.
                         std::vector<ValueType> x;
-                        if(hint.isExplicitModelCheckerHint() && hint.template asExplicitModelCheckerHint<ValueType>().hasResultHint()) {
+                        if (hint.isExplicitModelCheckerHint() && hint.template asExplicitModelCheckerHint<ValueType>().hasResultHint()) {
                             x = storm::utility::vector::filterVector(hint.template asExplicitModelCheckerHint<ValueType>().getResultHint(), maybeStates);
                         } else {
                             x = std::vector<ValueType>(submatrix.getColumnCount(), storm::utility::one<ValueType>());

src/storm/solver/LinearEquationSolver.cpp

@@ -11,6 +11,7 @@
 
 #include "storm/settings/SettingsManager.h"
 #include "storm/settings/modules/CoreSettings.h"
+#include "storm/settings/modules/GeneralSettings.h"
 
 #include "storm/utility/macros.h"
 #include "storm/exceptions/NotSupportedException.h"
@@ -190,9 +191,36 @@ namespace storm {
             return this->create()->getRequirements();
         }
         
+        template<typename ValueType>
+        GeneralLinearEquationSolverFactory<ValueType>::GeneralLinearEquationSolverFactory() {
+            auto const& coreSettings = storm::settings::getModule<storm::settings::modules::CoreSettings>();
+            auto const& generalSettings = storm::settings::getModule<storm::settings::modules::GeneralSettings>();
+            
+            EquationSolverType actualEquationSolver = coreSettings.getEquationSolver();
+            if (generalSettings.isSoundSet()) {
+                if (coreSettings.isEquationSolverSetFromDefaultValue()) {
+                    STORM_LOG_WARN_COND(actualEquationSolver == EquationSolverType::Native, "Switching to native equation solver to guarantee soundness. To select other solvers, please explicitly specify a solver.");
+                } else {
+                    STORM_LOG_WARN_COND(actualEquationSolver == EquationSolverType::Native, "Switching to native equation solver from explicitly selected solver '" << storm::solver::toString(actualEquationSolver) << "' to guarantee soundness.");
+                }
+                actualEquationSolver = EquationSolverType::Native;
+            }
+            
+            setEquationSolverType(actualEquationSolver);
+        }
+        
+        template<typename ValueType>
+        GeneralLinearEquationSolverFactory<ValueType>::GeneralLinearEquationSolverFactory(EquationSolverType const& equationSolver) {
+            setEquationSolverType(equationSolver);
+        }
+        
+        template<typename ValueType>
+        void GeneralLinearEquationSolverFactory<ValueType>::setEquationSolverType(EquationSolverType const& equationSolver) {
+            this->equationSolver = equationSolver;
+        }
+        
         template<typename ValueType>
         std::unique_ptr<LinearEquationSolver<ValueType>> GeneralLinearEquationSolverFactory<ValueType>::create() const {
-            EquationSolverType equationSolver = storm::settings::getModule<storm::settings::modules::CoreSettings>().getEquationSolver();
             switch (equationSolver) {
                 case EquationSolverType::Gmmxx: return std::make_unique<GmmxxLinearEquationSolver<ValueType>>();
                 case EquationSolverType::Native: return std::make_unique<NativeLinearEquationSolver<ValueType>>();

src/storm/solver/LinearEquationSolver.h

@@ -215,6 +215,8 @@ namespace storm {
             storm::utility::VectorHelper<ValueType> vectorHelper;
         };
         
+        enum class EquationSolverType;
+        
         template<typename ValueType>
         class LinearEquationSolverFactory {
         public:
@@ -260,11 +262,23 @@ namespace storm {
         template<typename ValueType>
         class GeneralLinearEquationSolverFactory : public LinearEquationSolverFactory<ValueType> {
         public:
+            GeneralLinearEquationSolverFactory();
+            GeneralLinearEquationSolverFactory(EquationSolverType const& equationSolver);
+            
             using LinearEquationSolverFactory<ValueType>::create;
 
             virtual std::unique_ptr<LinearEquationSolver<ValueType>> create() const override;
 
             virtual std::unique_ptr<LinearEquationSolverFactory<ValueType>> clone() const override;
+            
+        private:
+            /*!
+             * Sets the equation solver type.
+             */
+            void setEquationSolverType(EquationSolverType const& equationSolver);
+            
+            // The equation solver type.
+            EquationSolverType equationSolver;
         };
 
 #ifdef STORM_HAVE_CARL