forceBounds option for native solver

src/storm/environment/solver/NativeSolverEnvironment.cpp

@@ -18,6 +18,7 @@ namespace storm {
         STORM_LOG_ASSERT(considerRelativeTerminationCriterion || nativeSettings.getConvergenceCriterion() == storm::settings::modules::NativeEquationSolverSettings::ConvergenceCriterion::Absolute, "Unknown convergence criterion");
         powerMethodMultiplicationStyle = nativeSettings.getPowerMethodMultiplicationStyle();
         sorOmega = storm::utility::convertNumber<storm::RationalNumber>(nativeSettings.getOmega());
+        forceBounds = nativeSettings.isForceBoundsSet();
     }
 
     NativeSolverEnvironment::~NativeSolverEnvironment() {
@@ -77,4 +78,13 @@ namespace storm {
         sorOmega = value;
     }
 
+    bool NativeSolverEnvironment::isForceBoundsSet() const {
+        return forceBounds;
+    }
+    
+    void NativeSolverEnvironment::setForceBounds(bool value) {
+        forceBounds = value;
+    }
+
+    
 }

src/storm/environment/solver/NativeSolverEnvironment.h

@@ -27,6 +27,8 @@ namespace storm {
         void setPowerMethodMultiplicationStyle(storm::solver::MultiplicationStyle value);
         storm::RationalNumber const& getSorOmega() const;
         void setSorOmega(storm::RationalNumber const& value);
+        bool isForceBoundsSet() const;
+        void setForceBounds(bool value);
         
     private:
         storm::solver::NativeLinearEquationSolverMethod method;
@@ -36,6 +38,7 @@ namespace storm {
         bool considerRelativeTerminationCriterion;
         storm::solver::MultiplicationStyle powerMethodMultiplicationStyle;
         storm::RationalNumber sorOmega;
+        bool forceBounds;
     };
 }
 

src/storm/settings/modules/NativeEquationSolverSettings.cpp

@@ -23,6 +23,7 @@ namespace storm {
             const std::string NativeEquationSolverSettings::precisionOptionName = "precision";
             const std::string NativeEquationSolverSettings::absoluteOptionName = "absolute";
             const std::string NativeEquationSolverSettings::powerMethodMultiplicationStyleOptionName = "powmult";
+            const std::string NativeEquationSolverSettings::forceBoundsOptionName = "forcebounds";
 
             NativeEquationSolverSettings::NativeEquationSolverSettings() : ModuleSettings(moduleName) {
                 std::vector<std::string> methods = { "jacobi", "gaussseidel", "sor", "walkerchae", "power", "ratsearch", "qpower" };
@@ -39,6 +40,9 @@ namespace storm {
                 std::vector<std::string> multiplicationStyles = {"gaussseidel", "regular", "gs", "r"};
                 this->addOption(storm::settings::OptionBuilder(moduleName, powerMethodMultiplicationStyleOptionName, false, "Sets which method multiplication style to prefer for the power method.")
                                 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of a multiplication style.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(multiplicationStyles)).setDefaultValueString("gaussseidel").build()).build());
+                                
+                this->addOption(storm::settings::OptionBuilder(moduleName, forceBoundsOptionName, false, "If set, the equation solver always require that a priori bounds for the solution are computed.").build());
+                
             }
             
             bool NativeEquationSolverSettings::isLinearEquationSystemTechniqueSet() const {
@@ -107,6 +111,10 @@ namespace storm {
                 STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown multiplication style '" << multiplicationStyleString << "'.");
             }
             
+            bool NativeEquationSolverSettings::isForceBoundsSet() const {
+                return this->getOption(forceBoundsOptionName).getHasOptionBeenSet();
+            }
+
             bool NativeEquationSolverSettings::check() const {
                 // This list does not include the precision, because this option is shared with other modules.
                 bool optionSet = isLinearEquationSystemTechniqueSet() || isMaximalIterationCountSet() || isConvergenceCriterionSet();

src/storm/settings/modules/NativeEquationSolverSettings.h

@@ -100,6 +100,11 @@ namespace storm {
                  */
                 storm::solver::MultiplicationStyle getPowerMethodMultiplicationStyle() const;
                 
+                /*!
+                 * Retrieves whether the  force bounds option has been set.
+                 */
+                bool isForceBoundsSet() const;
+               
                 bool check() const override;
                 
                 // The name of the module.
@@ -114,6 +119,8 @@ namespace storm {
                 static const std::string precisionOptionName;
                 static const std::string absoluteOptionName;
                 static const std::string powerMethodMultiplicationStyleOptionName;
+                static const std::string forceBoundsOptionName;
+
             };
             
         } // namespace modules

src/storm/solver/NativeLinearEquationSolver.cpp

@@ -1128,6 +1128,10 @@ namespace storm {
         LinearEquationSolverRequirements NativeLinearEquationSolver<ValueType>::getRequirements(Environment const& env, LinearEquationSolverTask const& task) const {
             LinearEquationSolverRequirements requirements;
             if (task != LinearEquationSolverTask::Multiply) {
+                if (env.solver().native().isForceBoundsSet()) {
+                    requirements.requiresLowerBounds();
+                    requirements.requiresUpperBounds();
+                }
                 auto method = getMethod(env, storm::NumberTraits<ValueType>::IsExact);
                 if (method == NativeLinearEquationSolverMethod::Power && env.solver().isForceSoundness()) {
                     requirements.requireBounds();