diff --git a/src/storm/environment/SubEnvironment.cpp b/src/storm/environment/SubEnvironment.cpp index 45c833110..f11b2b1bf 100644 --- a/src/storm/environment/SubEnvironment.cpp +++ b/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; template class SubEnvironment; template class SubEnvironment; + template class SubEnvironment; template class SubEnvironment; template class SubEnvironment; diff --git a/src/storm/environment/solver/MultiplierEnvironment.cpp b/src/storm/environment/solver/MultiplierEnvironment.cpp new file mode 100644 index 000000000..85e3bac77 --- /dev/null +++ b/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(); + 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; + } + +} diff --git a/src/storm/environment/solver/MultiplierEnvironment.h b/src/storm/environment/solver/MultiplierEnvironment.h new file mode 100644 index 000000000..d9e35f5fb --- /dev/null +++ b/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; + }; +} + diff --git a/src/storm/environment/solver/SolverEnvironment.cpp b/src/storm/environment/solver/SolverEnvironment.cpp index 5fc371072..42600adbb 100644 --- a/src/storm/environment/solver/SolverEnvironment.cpp +++ b/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(); } diff --git a/src/storm/environment/solver/SolverEnvironment.h b/src/storm/environment/solver/SolverEnvironment.h index 32c3cb648..5e24652e1 100644 --- a/src/storm/environment/solver/SolverEnvironment.h +++ b/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; SubEnvironment topologicalSolverEnvironment; SubEnvironment minMaxSolverEnvironment; + SubEnvironment multiplierEnvironment; storm::solver::EquationSolverType linearEquationSolverType; bool linearEquationSolverTypeSetFromDefault; diff --git a/src/storm/settings/SettingsManager.cpp b/src/storm/settings/SettingsManager.cpp index 8477b221f..fc2b80b35 100644 --- a/src/storm/settings/SettingsManager.cpp +++ b/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::addModule(); storm::settings::addModule(); + storm::settings::addModule(); } } diff --git a/src/storm/settings/modules/MultiplierSettings.cpp b/src/storm/settings/modules/MultiplierSettings.cpp new file mode 100644 index 000000000..d386bbf3a --- /dev/null +++ b/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 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(); + } + } + } +} diff --git a/src/storm/settings/modules/MultiplierSettings.h b/src/storm/settings/modules/MultiplierSettings.h new file mode 100644 index 000000000..ea5bfdd8c --- /dev/null +++ b/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; + }; + + } + } +}