multiplier settings and environment

src/storm/environment/SubEnvironment.cpp

@@ -4,6 +4,7 @@
 #include "storm/environment/solver/GmmxxSolverEnvironment.h"
 #include "storm/environment/solver/NativeSolverEnvironment.h"
 #include "storm/environment/solver/MinMaxSolverEnvironment.h"
+#include "storm/environment/solver/MultiplierEnvironment.h"
 #include "storm/environment/solver/GameSolverEnvironment.h"
 #include "storm/environment/solver/TopologicalSolverEnvironment.h"
 
@@ -40,6 +41,7 @@ namespace storm {
     template class SubEnvironment<GmmxxSolverEnvironment>;
     template class SubEnvironment<NativeSolverEnvironment>;
     template class SubEnvironment<MinMaxSolverEnvironment>;
+    template class SubEnvironment<MultiplierEnvironment>;
     template class SubEnvironment<GameSolverEnvironment>;
     template class SubEnvironment<TopologicalSolverEnvironment>;
     

src/storm/environment/solver/MultiplierEnvironment.cpp

@@ -0,0 +1,33 @@
+#include "storm/environment/solver/MultiplierEnvironment.h"
+
+#include "storm/settings/SettingsManager.h"
+#include "storm/settings/modules/MultiplierSettings.h"
+#include "storm/utility/constants.h"
+#include "storm/utility/macros.h"
+
+namespace storm {
+    
+    MultiplierEnvironment::MultiplierEnvironment() {
+        auto const& multiplierSettings = storm::settings::getModule<storm::settings::modules::MultiplierSettings>();
+        type = multiplierSettings.getMultiplierType();
+        typeSetFromDefault = multiplierSettings.isMultiplierTypeSetFromDefaultValue();
+    }
+    
+    MultiplierEnvironment::~MultiplierEnvironment() {
+        // Intentionally left empty
+    }
+    
+    storm::solver::MultiplierType const& MultiplierEnvironment::getType() const {
+        return type;
+    }
+    
+    bool const& MultiplierEnvironment::isTypeSetFromDefault() const {
+        return typeSetFromDefault;
+    }
+    
+    void MultiplierEnvironment::setType(storm::solver::MultiplierType value, bool isSetFromDefault) {
+        type = value;
+        typeSetFromDefault = isSetFromDefault;
+    }
+    
+}

src/storm/environment/solver/MultiplierEnvironment.h

@@ -0,0 +1,23 @@
+#pragma once
+
+#include "storm/environment/solver/SolverEnvironment.h"
+#include "storm/solver/SolverSelectionOptions.h"
+
+namespace storm {
+    
+    class MultiplierEnvironment {
+    public:
+        
+        MultiplierEnvironment();
+        ~MultiplierEnvironment();
+        
+        storm::solver::MultiplierType const& getType() const;
+        bool const& isTypeSetFromDefault() const;
+        void setType(storm::solver::MultiplierType value, bool isSetFromDefault = false);
+        
+    private:
+        storm::solver::MultiplierType type;
+        bool typeSetFromDefault;
+    };
+}
+

src/storm/environment/solver/SolverEnvironment.cpp

@@ -1,6 +1,7 @@
 #include "storm/environment/solver/SolverEnvironment.h"
 
 #include "storm/environment/solver/MinMaxSolverEnvironment.h"
+#include "storm/environment/solver/MultiplierEnvironment.h"
 #include "storm/environment/solver/EigenSolverEnvironment.h"
 #include "storm/environment/solver/GmmxxSolverEnvironment.h"
 #include "storm/environment/solver/NativeSolverEnvironment.h"
@@ -36,6 +37,14 @@ namespace storm {
         return minMaxSolverEnvironment.get();
     }
     
+    MultiplierEnvironment& SolverEnvironment::multiplier() {
+        return multiplierEnvironment.get();
+    }
+    
+    MultiplierEnvironment const& SolverEnvironment::multiplier() const {
+        return multiplierEnvironment.get();
+    }
+    
     EigenSolverEnvironment& SolverEnvironment::eigen() {
         return eigenSolverEnvironment.get();
     }

src/storm/environment/solver/SolverEnvironment.h

@@ -15,6 +15,7 @@ namespace storm {
     class GmmxxSolverEnvironment;
     class NativeSolverEnvironment;
     class MinMaxSolverEnvironment;
+    class MultiplierEnvironment;
     class GameSolverEnvironment;
     class TopologicalSolverEnvironment;
     
@@ -32,6 +33,8 @@ namespace storm {
         NativeSolverEnvironment const& native() const;
         MinMaxSolverEnvironment& minMax();
         MinMaxSolverEnvironment const& minMax() const;
+        MultiplierEnvironment& multiplier();
+        MultiplierEnvironment const& multiplier() const;
         GameSolverEnvironment& game();
         GameSolverEnvironment const& game() const;
         TopologicalSolverEnvironment& topological();
@@ -54,6 +57,7 @@ namespace storm {
         SubEnvironment<GameSolverEnvironment> gameSolverEnvironment;
         SubEnvironment<TopologicalSolverEnvironment> topologicalSolverEnvironment;
         SubEnvironment<MinMaxSolverEnvironment> minMaxSolverEnvironment;
+        SubEnvironment<MultiplierEnvironment> multiplierEnvironment;
       
         storm::solver::EquationSolverType linearEquationSolverType;
         bool linearEquationSolverTypeSetFromDefault;

src/storm/settings/SettingsManager.cpp

@@ -38,6 +38,7 @@
 #include "storm/settings/modules/JaniExportSettings.h"
 #include "storm/settings/modules/JitBuilderSettings.h"
 #include "storm/settings/modules/MultiObjectiveSettings.h"
+#include "storm/settings/modules/MultiplierSettings.h"
 #include "storm/utility/macros.h"
 #include "storm/utility/file.h"
 #include "storm/settings/Option.h"
@@ -550,6 +551,7 @@ namespace storm {
             storm::settings::addModule<storm::settings::modules::JaniExportSettings>();
             storm::settings::addModule<storm::settings::modules::JitBuilderSettings>();
             storm::settings::addModule<storm::settings::modules::MultiObjectiveSettings>();
+            storm::settings::addModule<storm::settings::modules::MultiplierSettings>();
         }
 
     }

src/storm/settings/modules/MultiplierSettings.cpp

@@ -0,0 +1,40 @@
+#include "storm/settings/modules/MultiplierSettings.h"
+
+#include "storm/settings/Option.h"
+#include "storm/settings/ArgumentBuilder.h"
+#include "storm/settings/OptionBuilder.h"
+
+#include "storm/utility/macros.h"
+#include "storm/exceptions/IllegalArgumentValueException.h"
+
+namespace storm {
+    namespace settings {
+        namespace modules {
+            
+            const std::string MultiplierSettings::moduleName = "multiplier";
+            const std::string MultiplierSettings::multiplierTypeOptionName = "type";
+
+            MultiplierSettings::MultiplierSettings() : ModuleSettings(moduleName) {
+                std::vector<std::string> multiplierTypes = {"native", "gmmxx"};
+                this->addOption(storm::settings::OptionBuilder(moduleName, multiplierTypeOptionName, true, "Sets which type of multiplier is preferred.")
+                                .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of a multiplier.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(multiplierTypes)).setDefaultValueString("gmmxx").build()).build());
+                
+            }
+            
+            storm::solver::MultiplierType MultiplierSettings::getMultiplierType() const {
+                std::string type = this->getOption(multiplierTypeOptionName).getArgumentByName("name").getValueAsString();
+                if (type == "native") {
+                    return storm::solver::MultiplierType::Native;
+                } else if (type == "gmmxx") {
+                    return storm::solver::MultiplierType::Gmmxx;
+                }
+                
+                STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown multiplier type '" << type << "'.");
+            }
+            
+            bool MultiplierSettings::isMultiplierTypeSetFromDefaultValue() const {
+                return !this->getOption(multiplierTypeOptionName).getArgumentByName("name").getHasBeenSet() || this->getOption(multiplierTypeOptionName).getArgumentByName("name").wasSetFromDefaultValue();
+            }
+        }
+    }
+}

src/storm/settings/modules/MultiplierSettings.h

@@ -0,0 +1,34 @@
+#pragma once
+
+#include "storm-config.h"
+#include "storm/settings/modules/ModuleSettings.h"
+
+#include "storm/solver/SolverSelectionOptions.h"
+#include "storm/solver/MultiplicationStyle.h"
+
+namespace storm {
+    namespace settings {
+        namespace modules {
+            
+            /*!
+             * This class represents the multiplier settings.
+             */
+            class MultiplierSettings : public ModuleSettings {
+            public:
+                
+                MultiplierSettings();
+              
+                storm::solver::MultiplierType getMultiplierType() const;
+                
+                bool isMultiplierTypeSetFromDefaultValue() const;
+                
+                // The name of the module.
+                static const std::string moduleName;
+                
+            private:
+                static const std::string multiplierTypeOptionName;
+            };
+            
+        }
+    }
+}