Storm 1.10.0.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
CoreSettings.cpp
Go to the documentation of this file.
2
10
12
16
17namespace storm {
18namespace settings {
19namespace modules {
20
21const std::string CoreSettings::moduleName = "core";
22const std::string CoreSettings::eqSolverOptionName = "eqsolver";
23const std::string CoreSettings::lpSolverOptionName = "lpsolver";
24const std::string CoreSettings::smtSolverOptionName = "smtsolver";
25const std::string CoreSettings::statisticsOptionName = "statistics";
26const std::string CoreSettings::statisticsOptionShortName = "stats";
27const std::string CoreSettings::engineOptionName = "engine";
28const std::string CoreSettings::engineOptionShortName = "e";
29const std::string CoreSettings::ddLibraryOptionName = "ddlib";
30
32 // TODO: We currently never set Gurobi as a default LP solver as
33 // its availability is depending on the license, which may be confusing.
34 // We track this item in #issue 680.
35#if defined STORM_HAVE_GLPK
36 return "glpk";
37#elif defined STORM_HAVE_SOPLEX
38 return "soplex"
39#else
40 return "z3";
41#endif
42}
43
44CoreSettings::CoreSettings() : ModuleSettings(moduleName), engine(storm::utility::Engine::Sparse) {
45 std::vector<std::string> engines;
46 for (auto e : storm::utility::getEngines()) {
48 }
49 engines.push_back("portfolio"); // for backwards compatibility
50
51 this->addOption(storm::settings::OptionBuilder(moduleName, engineOptionName, false, "Sets which engine is used for model building and model checking.")
52 .setShortName(engineOptionShortName)
53 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the engine to use.")
55 .setDefaultValueString("sparse")
56 .build())
57 .build());
58
59 std::vector<std::string> linearEquationSolver = {"gmm++", "native", "eigen", "elimination", "topological", "acyclic"};
60 this->addOption(
61 storm::settings::OptionBuilder(moduleName, eqSolverOptionName, false, "Sets which solver is preferred for solving systems of linear equations.")
62 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the solver to prefer.")
64 .setDefaultValueString("topological")
65 .build())
66 .build());
67
68 std::vector<std::string> ddLibraries = {"cudd", "sylvan"};
69 this->addOption(storm::settings::OptionBuilder(moduleName, ddLibraryOptionName, false, "Sets which library is preferred for decision-diagram operations.")
70 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the library to prefer.")
72 .setDefaultValueString("sylvan")
73 .build())
74 .build());
75
76 std::vector<std::string> lpSolvers = {"gurobi", "glpk", "z3", "soplex"};
77 this->addOption(storm::settings::OptionBuilder(moduleName, lpSolverOptionName, false, "Sets which LP solver is preferred.")
78 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of an LP solver.")
81 .build())
82 .build());
83
84 std::vector<std::string> smtSolvers = {"z3", "mathsat"};
85 this->addOption(storm::settings::OptionBuilder(moduleName, smtSolverOptionName, false, "Sets which SMT solver is preferred.")
86 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of an SMT solver.")
89 .build())
90 .build());
91 this->addOption(storm::settings::OptionBuilder(moduleName, statisticsOptionName, false, "Sets whether to display statistics if available.")
92 .setShortName(statisticsOptionShortName)
93 .build());
94}
95
96storm::solver::EquationSolverType CoreSettings::getEquationSolver() const {
97 std::string equationSolverName = this->getOption(eqSolverOptionName).getArgumentByName("name").getValueAsString();
98 if (equationSolverName == "gmm++") {
99 return storm::solver::EquationSolverType::Gmmxx;
100 } else if (equationSolverName == "native") {
101 return storm::solver::EquationSolverType::Native;
102 } else if (equationSolverName == "eigen") {
103 return storm::solver::EquationSolverType::Eigen;
104 } else if (equationSolverName == "elimination") {
105 return storm::solver::EquationSolverType::Elimination;
106 } else if (equationSolverName == "topological") {
107 return storm::solver::EquationSolverType::Topological;
108 } else if (equationSolverName == "acyclic") {
109 return storm::solver::EquationSolverType::Acyclic;
110 }
111 STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown equation solver '" << equationSolverName << "'.");
112}
113
115 return this->getOption(eqSolverOptionName).getHasOptionBeenSet();
116}
117
119 return !this->getOption(eqSolverOptionName).getHasOptionBeenSet() || this->getOption(eqSolverOptionName).getArgumentByName("name").wasSetFromDefaultValue();
120}
121
122storm::solver::LpSolverType CoreSettings::getLpSolver() const {
123 std::string lpSolverName = this->getOption(lpSolverOptionName).getArgumentByName("name").getValueAsString();
124 if (lpSolverName == "gurobi") {
125 return storm::solver::LpSolverType::Gurobi;
126 } else if (lpSolverName == "glpk") {
127 return storm::solver::LpSolverType::Glpk;
128 } else if (lpSolverName == "z3") {
129 return storm::solver::LpSolverType::Z3;
130 } else if (lpSolverName == "soplex") {
131 return storm::solver::LpSolverType::Soplex;
132 }
133 STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown LP solver '" << lpSolverName << "'.");
134}
135
137 return !this->getOption(lpSolverOptionName).getHasOptionBeenSet() || this->getOption(lpSolverOptionName).getArgumentByName("name").wasSetFromDefaultValue();
138}
139
140storm::solver::SmtSolverType CoreSettings::getSmtSolver() const {
141 std::string smtSolverName = this->getOption(smtSolverOptionName).getArgumentByName("name").getValueAsString();
142 if (smtSolverName == "z3") {
143 return storm::solver::SmtSolverType::Z3;
144 } else if (smtSolverName == "mathsat") {
145 return storm::solver::SmtSolverType::Mathsat;
146 }
147 STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown SMT solver '" << smtSolverName << "'.");
148}
149
151 std::string ddLibraryAsString = this->getOption(ddLibraryOptionName).getArgumentByName("name").getValueAsString();
152 if (ddLibraryAsString == "sylvan") {
154 } else {
156 }
157}
158
160 return !this->getOption(ddLibraryOptionName).getArgumentByName("name").getHasBeenSet() ||
161 this->getOption(ddLibraryOptionName).getArgumentByName("name").wasSetFromDefaultValue();
162}
163
165 return this->getOption(statisticsOptionName).getHasOptionBeenSet();
166}
167
169 return engine;
170}
171
175
177 // Finalize engine.
178 std::string engineStr = this->getOption(engineOptionName).getArgumentByName("name").getValueAsString();
180 STORM_LOG_THROW(engine != storm::utility::Engine::Unknown, storm::exceptions::IllegalArgumentValueException, "Unknown engine '" << engineStr << "'.");
181}
182
184 return true;
185}
186
187} // namespace modules
188} // namespace settings
189} // namespace storm
virtual std::string getValueAsString() const =0
Retrieves the value of this argument as a string.
virtual bool getHasBeenSet() const
Retrieves whether the argument has been set.
virtual bool wasSetFromDefaultValue() const =0
static ArgumentBuilder createStringArgument(std::string const &name, std::string const &description)
Creates a string argument with the given parameters.
static std::shared_ptr< ArgumentValidator< std::string > > createMultipleChoiceValidator(std::vector< std::string > const &choices)
This class provides the interface to create an option...
ArgumentBase const & getArgumentByName(std::string const &argumentName) const
Returns a reference to the argument with the specified long name.
Definition Option.cpp:79
bool getHasOptionBeenSet() const
Retrieves whether the option has been set.
Definition Option.cpp:125
storm::solver::LpSolverType getLpSolver() const
Retrieves the selected LP solver.
storm::dd::DdType getDdLibraryType() const
Retrieves the selected library for DD-related operations.
bool isShowStatisticsSet() const
Retrieves whether statistics are to be shown.
storm::solver::EquationSolverType getEquationSolver() const
Retrieves the selected equation solver.
bool isEquationSolverSetFromDefaultValue() const
Retrieves whether the equation solver has been set from its default value.
bool isEquationSolverSet() const
Retrieves whether a equation solver has been set.
CoreSettings()
Creates a new set of core settings.
bool isLpSolverSetFromDefaultValue() const
Retrieves whether the lp solver has been set from its default value.
void finalize() override
Prepares the modules for further usage, should be called at the end of the initialization,...
void setEngine(storm::utility::Engine const &engine)
Sets the engine for further usage.
bool check() const override
Checks whether the settings are consistent.
storm::solver::SmtSolverType getSmtSolver() const
Retrieves the selected SMT solver.
bool isDdLibraryTypeSetFromDefaultValue() const
Retrieves whether the selected DD library is set from its default value.
static const std::string moduleName
storm::utility::Engine getEngine() const
Retrieves the selected engine.
This is the base class of the settings for a particular module.
void addOption(std::shared_ptr< Option > const &option)
Adds and registers the given option.
Option & getOption(std::string const &longName)
Retrieves the option with the given long name.
#define STORM_LOG_THROW(cond, exception, message)
Definition macros.h:30
std::string getDefaultLpSolverAsString()
SettingsType const & getModule()
Get module.
Engine
An enumeration of all engines.
Definition Engine.h:31
std::string toString(Engine const &engine)
Returns a string representation of the given engine.
Definition Engine.cpp:41
std::vector< Engine > getEngines()
Returns a list of all available engines (excluding Unknown)
Definition Engine.cpp:33
Engine engineFromString(std::string const &engineStr)
Parses the string representation of an engine and returns the corresponding engine.
Definition Engine.cpp:70
LabParser.cpp.
Definition cli.cpp:18