SolverEnvironment: Added the switch `forceExact` to switch to exact solving methods more conveniently.

src/storm/environment/solver/SolverEnvironment.cpp

@@ -23,6 +23,7 @@ namespace storm {
     
     SolverEnvironment::SolverEnvironment() {
         forceSoundness = storm::settings::getModule<storm::settings::modules::GeneralSettings>().isSoundSet();
+        forceExact = storm::settings::getModule<storm::settings::modules::GeneralSettings>().isExactSet();
         linearEquationSolverType = storm::settings::getModule<storm::settings::modules::CoreSettings>().getEquationSolver();
         linearEquationSolverTypeSetFromDefault = storm::settings::getModule<storm::settings::modules::CoreSettings>().isEquationSolverSetFromDefaultValue();
     }
@@ -111,6 +112,14 @@ namespace storm {
         SolverEnvironment::forceSoundness = value;
     }
     
+    bool SolverEnvironment::isForceExact() const {
+        return forceExact;
+    }
+    
+    void SolverEnvironment::setForceExact(bool value) {
+        SolverEnvironment::forceExact = value;
+    }
+    
     storm::solver::EquationSolverType const& SolverEnvironment::getLinearEquationSolverType() const {
         return linearEquationSolverType;
     }

src/storm/environment/solver/SolverEnvironment.h

@@ -48,6 +48,8 @@ namespace storm {
 
         bool isForceSoundness() const;
         void setForceSoundness(bool value);
+        bool isForceExact() const;
+        void setForceExact(bool value);
         
         storm::solver::EquationSolverType const& getLinearEquationSolverType() const;
         void setLinearEquationSolverType(storm::solver::EquationSolverType const& value, bool isSetFromDefault = false);
@@ -70,6 +72,7 @@ namespace storm {
         storm::solver::EquationSolverType linearEquationSolverType;
         bool linearEquationSolverTypeSetFromDefault;
         bool forceSoundness;
+        bool forceExact;
     };
 }
 

src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp

@@ -576,7 +576,7 @@ namespace storm {
                 }
                 
                 storm::solver::LraMethod method = env.solver().lra().getDetLraMethod();
-                if (storm::NumberTraits<ValueType>::IsExact && env.solver().lra().isDetLraMethodSetFromDefault() && method == storm::solver::LraMethod::ValueIteration) {
+                if ((storm::NumberTraits<ValueType>::IsExact || env.solver().isForceExact()) && env.solver().lra().isDetLraMethodSetFromDefault() && method == storm::solver::LraMethod::ValueIteration) {
                     method = storm::solver::LraMethod::GainBiasEquations;
                     STORM_LOG_INFO("Selecting " << storm::solver::toString(method) << " as the solution technique for long-run properties to guarantee exact results. If you want to override this, please explicitly specify a different LRA method.");
                 } else if (env.solver().isForceSoundness() && env.solver().lra().isDetLraMethodSetFromDefault() && method != storm::solver::LraMethod::ValueIteration) {

src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp

@@ -820,7 +820,7 @@ namespace storm {
                 
                 // Solve MEC with the method specified in the settings
                 storm::solver::LraMethod method = env.solver().lra().getNondetLraMethod();
-                if (storm::NumberTraits<ValueType>::IsExact && env.solver().lra().isNondetLraMethodSetFromDefault() && method != storm::solver::LraMethod::LinearProgramming) {
+                if ((storm::NumberTraits<ValueType>::IsExact || env.solver().isForceExact()) && env.solver().lra().isNondetLraMethodSetFromDefault() && method != storm::solver::LraMethod::LinearProgramming) {
                     STORM_LOG_INFO("Selecting 'LP' as the solution technique for long-run properties to guarantee exact results. If you want to override this, please explicitly specify a different LRA method.");
                     method = storm::solver::LraMethod::LinearProgramming;
                 } else if (env.solver().isForceSoundness() && env.solver().lra().isNondetLraMethodSetFromDefault() && method != storm::solver::LraMethod::ValueIteration) {

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

@@ -1477,7 +1477,7 @@ namespace storm {
                 
                 // Solve MEC with the method specified in the settings
                 storm::solver::LraMethod method = env.solver().lra().getNondetLraMethod();
-                if (storm::NumberTraits<ValueType>::IsExact && env.solver().lra().isNondetLraMethodSetFromDefault() && method != storm::solver::LraMethod::LinearProgramming) {
+                if ((storm::NumberTraits<ValueType>::IsExact || env.solver().isForceExact()) && env.solver().lra().isNondetLraMethodSetFromDefault() && method != storm::solver::LraMethod::LinearProgramming) {
                     STORM_LOG_INFO("Selecting 'LP' as the solution technique for long-run properties to guarantee exact results. If you want to override this, please explicitly specify a different LRA method.");
                     method = storm::solver::LraMethod::LinearProgramming;
                 } else if (env.solver().isForceSoundness() && env.solver().lra().isNondetLraMethodSetFromDefault() && method != storm::solver::LraMethod::ValueIteration) {

src/storm/solver/EigenLinearEquationSolver.cpp

@@ -107,7 +107,7 @@ namespace storm {
             auto eigenX = StormEigen::Matrix<ValueType, StormEigen::Dynamic, 1>::Map(x.data(), x.size());
             auto eigenB = StormEigen::Matrix<ValueType, StormEigen::Dynamic, 1>::Map(b.data(), b.size());
 
-            auto solutionMethod = getMethod(env, false);
+            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).");
                 StormEigen::SparseLU<StormEigen::SparseMatrix<ValueType>, StormEigen::COLAMDOrdering<int>> solver;

src/storm/solver/GmmxxLinearEquationSolver.cpp

@@ -46,6 +46,7 @@ namespace storm {
         template<typename ValueType>
         GmmxxLinearEquationSolverMethod GmmxxLinearEquationSolver<ValueType>::getMethod(Environment const& env) const {
             STORM_LOG_ERROR_COND(!env.solver().isForceSoundness(), "This linear equation solver does not support sound computations. Using unsound methods now...");
+            STORM_LOG_ERROR_COND(!env.solver().isForceExact(), "This linear equation solver does not support exact computations. Using unsound methods now...");
             return env.solver().gmmxx().getMethod();
         }
         

src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp

@@ -64,7 +64,7 @@ namespace storm {
         template<typename ValueType>
         bool IterativeMinMaxLinearEquationSolver<ValueType>::internalSolveEquations(Environment const& env, OptimizationDirection dir, std::vector<ValueType>& x, std::vector<ValueType> const& b) const {
             bool result = false;
-            switch (getMethod(env, storm::NumberTraits<ValueType>::IsExact)) {
+            switch (getMethod(env, storm::NumberTraits<ValueType>::IsExact || env.solver().isForceExact())) {
                 case MinMaxMethod::ValueIteration:
                     result = solveEquationsValueIteration(env, dir, x, b);
                     break;
@@ -228,7 +228,7 @@ namespace storm {
 
         template<typename ValueType>
         MinMaxLinearEquationSolverRequirements IterativeMinMaxLinearEquationSolver<ValueType>::getRequirements(Environment const& env, boost::optional<storm::solver::OptimizationDirection> const& direction, bool const& hasInitialScheduler) const {
-            auto method = getMethod(env, storm::NumberTraits<ValueType>::IsExact);
+            auto method = getMethod(env, storm::NumberTraits<ValueType>::IsExact || env.solver().isForceExact());
             
             // Check whether a linear equation solver is needed and potentially start with its requirements
             bool needsLinEqSolver = false;

src/storm/solver/LinearEquationSolver.cpp

@@ -128,8 +128,15 @@ namespace storm {
         std::unique_ptr<LinearEquationSolver<ValueType>> GeneralLinearEquationSolverFactory<ValueType>::create(Environment const& env) const {
             EquationSolverType type = env.solver().getLinearEquationSolverType();
             
-            // Adjust the solver type if none was specified and we want sound computations
-            if (env.solver().isForceSoundness() && type != EquationSolverType::Native && type != EquationSolverType::Eigen && type != EquationSolverType::Elimination && type != EquationSolverType::Topological) {
+            // Adjust the solver type if none was specified and we want sound/exact computations
+            if (env.solver().isForceExact() && type != EquationSolverType::Native && type != EquationSolverType::Eigen && type != EquationSolverType::Elimination && type != EquationSolverType::Topological) {
+                if (env.solver().isLinearEquationSolverTypeSetFromDefaultValue()) {
+                    type = EquationSolverType::Eigen;
+                    STORM_LOG_INFO("Selecting '" + toString(type) + "' as the linear equation solver to guarantee exact results. If you want to override this, please explicitly specify a different solver.");
+                } else {
+                    STORM_LOG_WARN("The selected solver does not yield exact results.");
+                }
+            } else if (env.solver().isForceSoundness() && type != EquationSolverType::Native && type != EquationSolverType::Eigen && type != EquationSolverType::Elimination && type != EquationSolverType::Topological) {
                 if (env.solver().isLinearEquationSolverTypeSetFromDefaultValue()) {
                     type = EquationSolverType::Native;
                     STORM_LOG_INFO("Selecting '" + toString(type) + "' as the linear equation solver to guarantee sound results. If you want to override this, please explicitly specify a different solver.");

src/storm/solver/NativeLinearEquationSolver.cpp

@@ -922,7 +922,7 @@ namespace storm {
         
         template<typename ValueType>
         bool NativeLinearEquationSolver<ValueType>::internalSolveEquations(Environment const& env, std::vector<ValueType>& x, std::vector<ValueType> const& b) const {
-            switch(getMethod(env, storm::NumberTraits<ValueType>::IsExact)) {
+            switch(getMethod(env, storm::NumberTraits<ValueType>::IsExact || env.solver().isForceExact())) {
                 case NativeLinearEquationSolverMethod::SOR:
                     return this->solveEquationsSOR(env, x, b, storm::utility::convertNumber<ValueType>(env.solver().native().getSorOmega()));
                 case NativeLinearEquationSolverMethod::GaussSeidel:
@@ -946,7 +946,7 @@ namespace storm {
         
         template<typename ValueType>
         LinearEquationSolverProblemFormat NativeLinearEquationSolver<ValueType>::getEquationProblemFormat(Environment const& env) const {
-            auto method = getMethod(env, storm::NumberTraits<ValueType>::IsExact);
+            auto method = getMethod(env, storm::NumberTraits<ValueType>::IsExact || env.solver().isForceExact());
             if (method == NativeLinearEquationSolverMethod::Power || method == NativeLinearEquationSolverMethod::SoundValueIteration || method == NativeLinearEquationSolverMethod::RationalSearch || method == NativeLinearEquationSolverMethod::IntervalIteration) {
                 return LinearEquationSolverProblemFormat::FixedPointSystem;
             } else {
@@ -957,7 +957,7 @@ namespace storm {
         template<typename ValueType>
         LinearEquationSolverRequirements NativeLinearEquationSolver<ValueType>::getRequirements(Environment const& env) const {
             LinearEquationSolverRequirements requirements;
-            auto method = getMethod(env, storm::NumberTraits<ValueType>::IsExact);
+            auto method = getMethod(env, storm::NumberTraits<ValueType>::IsExact || env.solver().isForceExact());
             if (method == NativeLinearEquationSolverMethod::IntervalIteration) {
                 requirements.requireBounds();
             } else if (method == NativeLinearEquationSolverMethod::RationalSearch) {

src/storm/solver/StandardGameSolver.cpp

@@ -72,7 +72,7 @@ namespace storm {
         
         template<typename ValueType>
         bool StandardGameSolver<ValueType>::solveGame(Environment const& env, OptimizationDirection player1Dir, OptimizationDirection player2Dir, std::vector<ValueType>& x, std::vector<ValueType> const& b, std::vector<uint64_t>* player1Choices, std::vector<uint64_t>* player2Choices) const {
-            auto method = getMethod(env, std::is_same<ValueType, storm::RationalNumber>::value);
+            auto method = getMethod(env, std::is_same<ValueType, storm::RationalNumber>::value || env.solver().isForceExact());
             STORM_LOG_INFO("Solving stochastic two player game over " << x.size() << " states using " << toString(method) << ".");
             switch (method) {
                 case GameMethod::ValueIteration: