Storm 1.11.1.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
GurobiLpSolver.cpp
Go to the documentation of this file.
2
3#include <numeric>
4
19
20namespace storm {
21namespace solver {
22
24#ifdef STORM_HAVE_GUROBI
25 if (initialized) {
26 GRBfreeenv(env);
27 }
28#endif
29}
30
31#ifdef STORM_HAVE_GUROBI
32GRBenv* GurobiEnvironment::operator*() {
33 STORM_LOG_ASSERT(initialized, "Gurobi Environment has not been initialized");
34 return env;
35}
36#endif
37
39#ifdef STORM_HAVE_GUROBI
40 // Create the environment.
41 int error = GRBloadenv(&env, "");
42 if (error || env == nullptr) {
43 if (error == 10009) {
44 STORM_LOG_ERROR("Gurobi License Issue. " << GRBgeterrormsg(env) << ", error code " << error << ").");
45 throw storm::exceptions::GurobiLicenseException()
46 << "Could not initialize Gurobi environment (" << GRBgeterrormsg(env) << ", error code " << error << ").";
47 }
48 STORM_LOG_ERROR("Could not initialize Gurobi (" << GRBgeterrormsg(env) << ", error code " << error << ").");
49 throw storm::exceptions::InvalidStateException()
50 << "Could not initialize Gurobi environment (" << GRBgeterrormsg(env) << ", error code " << error << ").";
51 }
52 setOutput(storm::settings::getModule<storm::settings::modules::DebugSettings>().isDebugSet() ||
53 storm::settings::getModule<storm::settings::modules::GurobiSettings>().isOutputSet());
54
55 error = GRBsetintparam(env, "Method", static_cast<int>(storm::settings::getModule<storm::settings::modules::GurobiSettings>().getMethod()));
56 STORM_LOG_THROW(error == 0, storm::exceptions::InvalidStateException,
57 "Unable to set Gurobi Parameter Method (" << GRBgeterrormsg(env) << ", error code " << error << ").");
58
59 // Enable the following line to restrict Gurobi to one thread only.
60 error = GRBsetintparam(env, "Threads", storm::settings::getModule<storm::settings::modules::GurobiSettings>().getNumberOfThreads());
61 STORM_LOG_THROW(error == 0, storm::exceptions::InvalidStateException,
62 "Unable to set Gurobi Parameter Threads (" << GRBgeterrormsg(env) << ", error code " << error << ").");
63
64 error = GRBsetintparam(env, "MIPFocus", storm::settings::getModule<storm::settings::modules::GurobiSettings>().getMIPFocus());
65 STORM_LOG_THROW(error == 0, storm::exceptions::InvalidStateException,
66 "Unable to set Gurobi Parameter MIPFocus (" << GRBgeterrormsg(env) << ", error code " << error << ").");
67
68 error = GRBsetintparam(env, "ConcurrentMIP", storm::settings::getModule<storm::settings::modules::GurobiSettings>().getNumberOfConcurrentMipThreads());
69 STORM_LOG_THROW(error == 0, storm::exceptions::InvalidStateException,
70 "Unable to set Gurobi Parameter ConcurrentMIP (" << GRBgeterrormsg(env) << ", error code " << error << ").");
71
72 // Enable the following line to force Gurobi to be as precise about the binary variables as required by the given precision option.
73 error = GRBsetdblparam(env, "IntFeasTol", storm::settings::getModule<storm::settings::modules::GurobiSettings>().getIntegerTolerance());
74 STORM_LOG_THROW(error == 0, storm::exceptions::InvalidStateException,
75 "Unable to set Gurobi Parameter IntFeasTol (" << GRBgeterrormsg(env) << ", error code " << error << ").");
76#endif
77 initialized = true;
78}
79
81#ifdef STORM_HAVE_GUROBI
82 int error = GRBsetintparam(env, "OutputFlag", set);
83 STORM_LOG_THROW(error == 0, storm::exceptions::InvalidStateException,
84 "Unable to set Gurobi Parameter OutputFlag (" << GRBgeterrormsg(env) << ", error code " << error << ").");
85#else
86 (void)set;
87#endif
88}
89
90#ifdef STORM_HAVE_GUROBI
91
92template<typename ValueType, bool RawMode>
93GurobiLpSolver<ValueType, RawMode>::GurobiLpSolver(std::shared_ptr<GurobiEnvironment> const& environment, std::string const& name,
94 OptimizationDirection const& optDir)
95 : LpSolver<ValueType, RawMode>(optDir), model(nullptr), environment(environment), nextVariableIndex(0) {
96 // Create the model.
97 int error = 0;
98 error = GRBnewmodel(**environment, &model, name.c_str(), 0, nullptr, nullptr, nullptr, nullptr, nullptr);
99 if (error) {
100 STORM_LOG_ERROR("Could not initialize Gurobi model (" << GRBgeterrormsg(**environment) << ", error code " << error << ").");
101 throw storm::exceptions::InvalidStateException()
102 << "Could not initialize Gurobi model (" << GRBgeterrormsg(**environment) << ", error code " << error << ").";
103 }
104}
105
106template<typename ValueType, bool RawMode>
107GurobiLpSolver<ValueType, RawMode>::GurobiLpSolver(std::shared_ptr<GurobiEnvironment> const& environment, std::string const& name)
108 : GurobiLpSolver(environment, name, OptimizationDirection::Minimize) {
109 // Intentionally left empty.
110}
111
112template<typename ValueType, bool RawMode>
113GurobiLpSolver<ValueType, RawMode>::GurobiLpSolver(std::shared_ptr<GurobiEnvironment> const& environment, OptimizationDirection const& optDir)
114 : GurobiLpSolver(environment, "", optDir) {
115 // Intentionally left empty.
116}
117
118template<typename ValueType, bool RawMode>
119GurobiLpSolver<ValueType, RawMode>::GurobiLpSolver(std::shared_ptr<GurobiEnvironment> const& environment)
120 : GurobiLpSolver(environment, "", OptimizationDirection::Minimize) {
121 // Intentionally left empty.
122}
123
124template<typename ValueType, bool RawMode>
126 // Dispose of the objects allocated inside Gurobi.
127 GRBfreemodel(model);
128}
129
130template<typename ValueType, bool RawMode>
132 int error = GRBupdatemodel(model);
133 STORM_LOG_THROW(error == 0, storm::exceptions::InvalidStateException,
134 "Unable to update Gurobi model (" << GRBgeterrormsg(**environment) << ", error code " << error << ").");
135
136 // Since the model changed, we erase the optimality flag.
137 this->currentModelHasBeenOptimized = false;
138}
139
140template<typename ValueType, bool RawMode>
141char getGurobiType(typename GurobiLpSolver<ValueType, RawMode>::VariableType const& type) {
142 switch (type) {
143 case GurobiLpSolver<ValueType, RawMode>::VariableType::Continuous:
144 return GRB_CONTINUOUS;
145 case GurobiLpSolver<ValueType, RawMode>::VariableType::Integer:
146 return GRB_INTEGER;
147 case GurobiLpSolver<ValueType, RawMode>::VariableType::Binary:
148 return GRB_BINARY;
149 }
150 STORM_LOG_ASSERT(false, "Unexpected variable type.");
151 return -1;
152}
153
154template<typename ValueType, bool RawMode>
155typename GurobiLpSolver<ValueType, RawMode>::Variable GurobiLpSolver<ValueType, RawMode>::addVariable(std::string const& name, VariableType const& type,
156 std::optional<ValueType> const& lowerBound,
157 std::optional<ValueType> const& upperBound,
158 ValueType objectiveFunctionCoefficient) {
159 Variable resultVar;
160 if constexpr (RawMode) {
161 resultVar = nextVariableIndex;
162 } else {
163 resultVar = this->declareOrGetExpressionVariable(name, type);
164 // Assert whether the variable does not exist yet.
165 // Due to incremental usage (push(), pop()), a variable might be declared in the manager but not in the lp model.
166 STORM_LOG_ASSERT(variableToIndexMap.count(resultVar) == 0, "Variable " << resultVar.getName() << " exists already in the model.");
167 this->variableToIndexMap.emplace(resultVar, nextVariableIndex);
168 if (!incrementalData.empty()) {
169 incrementalData.back().variables.push_back(resultVar);
170 }
171 }
172 ++nextVariableIndex;
173
174 // Create the actual variable.
175 int error = 0;
176 error = GRBaddvar(model, 0, nullptr, nullptr, storm::utility::convertNumber<double>(objectiveFunctionCoefficient),
177 lowerBound.has_value() ? storm::utility::convertNumber<double>(*lowerBound) : -GRB_INFINITY,
178 upperBound.has_value() ? storm::utility::convertNumber<double>(*upperBound) : GRB_INFINITY, getGurobiType<ValueType, RawMode>(type),
179 name.c_str());
180 STORM_LOG_THROW(error == 0, storm::exceptions::InvalidStateException,
181 "Could not create binary Gurobi variable (" << GRBgeterrormsg(**environment) << ", error code " << error << ").");
182 return resultVar;
183}
184
185struct GurobiConstraint {
186 std::vector<int> variableIndices;
187 std::vector<double> coefficients;
188 char sense;
189 double rhs;
190};
191
192template<typename ValueType, bool RawMode>
193GurobiConstraint createConstraint(typename GurobiLpSolver<ValueType, RawMode>::Constraint const& constraint,
194 std::map<storm::expressions::Variable, int> const& variableToIndexMap) {
195 GurobiConstraint gurobiConstraint;
197 if constexpr (RawMode) {
198 gurobiConstraint.rhs = storm::utility::convertNumber<double>(constraint.rhs);
199 relationType = constraint.relationType;
200 gurobiConstraint.variableIndices.insert(gurobiConstraint.variableIndices.end(), constraint.lhsVariableIndices.begin(),
201 constraint.lhsVariableIndices.end());
202 gurobiConstraint.coefficients.reserve(constraint.lhsCoefficients.size());
203 for (auto const& coef : constraint.lhsCoefficients) {
204 gurobiConstraint.coefficients.push_back(storm::utility::convertNumber<double>(coef));
205 }
206 } else {
207 STORM_LOG_THROW(constraint.isRelationalExpression(), storm::exceptions::InvalidArgumentException, "Illegal constraint is not a relational expression.");
212 leftCoefficients.separateVariablesFromConstantPart(rightCoefficients);
213 gurobiConstraint.rhs = rightCoefficients.getConstantPart();
214 relationType = constraint.getBaseExpression().asBinaryRelationExpression().getRelationType();
215 int len = std::distance(leftCoefficients.begin(), leftCoefficients.end());
216 gurobiConstraint.variableIndices.reserve(len);
217 gurobiConstraint.coefficients.reserve(len);
218 for (auto const& variableCoefficientPair : leftCoefficients) {
219 auto variableIndexPair = variableToIndexMap.find(variableCoefficientPair.first);
220 gurobiConstraint.variableIndices.push_back(variableIndexPair->second);
221 gurobiConstraint.coefficients.push_back(variableCoefficientPair.second);
222 }
223 }
224 // Determine the type of the constraint and add it properly.
225 switch (relationType) {
227 gurobiConstraint.sense = GRB_LESS_EQUAL;
228 gurobiConstraint.rhs -= storm::settings::getModule<storm::settings::modules::GurobiSettings>().getIntegerTolerance();
229 break;
231 gurobiConstraint.sense = GRB_LESS_EQUAL;
232 break;
234 gurobiConstraint.sense = GRB_GREATER_EQUAL;
235 gurobiConstraint.rhs += storm::settings::getModule<storm::settings::modules::GurobiSettings>().getIntegerTolerance();
236 break;
238 gurobiConstraint.sense = GRB_GREATER_EQUAL;
239 break;
241 gurobiConstraint.sense = GRB_EQUAL;
242 break;
243 default:
244 STORM_LOG_ASSERT(false, "Illegal operator in LP solver constraint.");
245 }
246 return gurobiConstraint;
247}
248
249template<typename ValueType, bool RawMode>
250void GurobiLpSolver<ValueType, RawMode>::addConstraint(std::string const& name, Constraint const& constraint) {
251 if constexpr (!RawMode) {
252 STORM_LOG_TRACE("Adding constraint " << name << " to GurobiLpSolver:\n"
253 << "\t" << constraint);
254 STORM_LOG_ASSERT(constraint.getManager() == this->getManager(), "Constraint was not built over the proper variables.");
255 }
256
257 // Extract constraint data
258 auto grbConstr = createConstraint<ValueType, RawMode>(constraint, this->variableToIndexMap);
259 int error = GRBaddconstr(model, grbConstr.variableIndices.size(), grbConstr.variableIndices.data(), grbConstr.coefficients.data(), grbConstr.sense,
260 grbConstr.rhs, name == "" ? nullptr : name.c_str());
261 STORM_LOG_THROW(error == 0, storm::exceptions::InvalidStateException,
262 "Could not assert constraint (" << GRBgeterrormsg(**environment) << ", error code " << error << ").");
263}
264
265template<typename ValueType, bool RawMode>
266void GurobiLpSolver<ValueType, RawMode>::addIndicatorConstraint(std::string const& name, Variable indicatorVariable, bool indicatorValue,
267 Constraint const& constraint) {
268 int indVar;
269 // Extract constraint data
270 if constexpr (RawMode) {
271 indVar = indicatorVariable;
272 } else {
273 STORM_LOG_ASSERT(this->variableToIndexMap.count(indicatorVariable) > 0, "Indicator Variable " << indicatorVariable.getName() << " unknown to solver.");
274 STORM_LOG_ASSERT(indicatorVariable.hasIntegerType(), "Indicator Variable " << indicatorVariable.getName() << " has unexpected type.");
275 STORM_LOG_ASSERT(constraint.getManager() == this->getManager(), "Constraint was not built over the proper variables.");
276 STORM_LOG_TRACE("Adding Indicator constraint " << name << " to GurobiLpSolver:\n"
277 << "\t(" << indicatorVariable.getName() << "==" << indicatorValue << ") implies " << constraint);
278 indVar = this->variableToIndexMap.at(indicatorVariable);
279 }
280 int indVal = indicatorValue ? 1 : 0;
281 auto grbConstr = createConstraint<ValueType, RawMode>(constraint, this->variableToIndexMap);
282 // Gurobi considers indicator constraints as a certain kind of what they call "general constraints".
283 int error = GRBaddgenconstrIndicator(model, name == "" ? nullptr : name.c_str(), indVar, indVal, grbConstr.variableIndices.size(),
284 grbConstr.variableIndices.data(), grbConstr.coefficients.data(), grbConstr.sense, grbConstr.rhs);
285 STORM_LOG_THROW(error == 0, storm::exceptions::InvalidStateException,
286 "Could not assert constraint (" << GRBgeterrormsg(**environment) << ", error code " << error << ").");
287}
288
289template<typename ValueType, bool RawMode>
291 // First incorporate all recent changes.
292 this->update();
293
294 // Set the most recently set model sense.
295 int error = GRBsetintattr(model, "ModelSense", this->getOptimizationDirection() == OptimizationDirection::Minimize ? 1 : -1);
296 STORM_LOG_THROW(error == 0, storm::exceptions::InvalidStateException,
297 "Unable to set Gurobi model sense (" << GRBgeterrormsg(**environment) << ", error code " << error << ").");
298
299 // Then we actually optimize the model.
300 error = GRBoptimize(model);
301 STORM_LOG_THROW(error == 0, storm::exceptions::InvalidStateException,
302 "Unable to optimize Gurobi model (" << GRBgeterrormsg(**environment) << ", error code " << error << ").");
303
304 this->currentModelHasBeenOptimized = true;
305}
306
307template<typename ValueType, bool RawMode>
309 if (!this->currentModelHasBeenOptimized) {
310 throw storm::exceptions::InvalidStateException() << "Illegal call to GurobiLpSolver<ValueType, RawMode>::isInfeasible: model has not been optimized.";
311 }
312
313 int optimalityStatus = 0;
314
315 int error = GRBgetintattr(model, GRB_INT_ATTR_STATUS, &optimalityStatus);
316 STORM_LOG_THROW(error == 0, storm::exceptions::InvalidStateException,
317 "Unable to retrieve optimization status of Gurobi model (" << GRBgeterrormsg(**environment) << ", error code " << error << ").");
318
319 // By default, Gurobi may tell us only that the model is either infeasible or unbounded. To decide which one
320 // it is, we need to perform an extra step.
321 if (optimalityStatus == GRB_INF_OR_UNBD) {
322 error = GRBsetintparam(GRBgetenv(model), GRB_INT_PAR_DUALREDUCTIONS, 0);
323 STORM_LOG_THROW(error == 0, storm::exceptions::InvalidStateException,
324 "Unable to set Gurobi parameter (" << GRBgeterrormsg(**environment) << ", error code " << error << ").");
325
326 this->optimize();
327
328 error = GRBgetintattr(model, GRB_INT_ATTR_STATUS, &optimalityStatus);
329 STORM_LOG_THROW(error == 0, storm::exceptions::InvalidStateException,
330 "Unable to retrieve optimization status of Gurobi model (" << GRBgeterrormsg(**environment) << ", error code " << error << ").");
331
332 error = GRBsetintparam(GRBgetenv(model), GRB_INT_PAR_DUALREDUCTIONS, 1);
333 STORM_LOG_THROW(error == 0, storm::exceptions::InvalidStateException,
334 "Unable to set Gurobi parameter (" << GRBgeterrormsg(**environment) << ", error code " << error << ").");
335 }
336
337 return optimalityStatus == GRB_INFEASIBLE;
338}
339
340template<typename ValueType, bool RawMode>
342 if (!this->currentModelHasBeenOptimized) {
343 throw storm::exceptions::InvalidStateException() << "Illegal call to GurobiLpSolver<ValueType, RawMode>::isUnbounded: model has not been optimized.";
344 }
345
346 int optimalityStatus = 0;
347
348 int error = GRBgetintattr(model, GRB_INT_ATTR_STATUS, &optimalityStatus);
349 STORM_LOG_THROW(error == 0, storm::exceptions::InvalidStateException,
350 "Unable to retrieve optimization status of Gurobi model (" << GRBgeterrormsg(**environment) << ", error code " << error << ").");
351
352 // By default, Gurobi may tell us only that the model is either infeasible or unbounded. To decide which one
353 // it is, we need to perform an extra step.
354 if (optimalityStatus == GRB_INF_OR_UNBD) {
355 error = GRBsetintparam(GRBgetenv(model), GRB_INT_PAR_DUALREDUCTIONS, 0);
356 STORM_LOG_THROW(error == 0, storm::exceptions::InvalidStateException,
357 "Unable to set Gurobi parameter (" << GRBgeterrormsg(**environment) << ", error code " << error << ").");
358
359 this->optimize();
360
361 error = GRBgetintattr(model, GRB_INT_ATTR_STATUS, &optimalityStatus);
362 STORM_LOG_THROW(error == 0, storm::exceptions::InvalidStateException,
363 "Unable to retrieve optimization status of Gurobi model (" << GRBgeterrormsg(**environment) << ", error code " << error << ").");
364
365 error = GRBsetintparam(GRBgetenv(model), GRB_INT_PAR_DUALREDUCTIONS, 1);
366 STORM_LOG_THROW(error == 0, storm::exceptions::InvalidStateException,
367 "Unable to set Gurobi parameter (" << GRBgeterrormsg(**environment) << ", error code " << error << ").");
368 }
369
370 return optimalityStatus == GRB_UNBOUNDED;
371}
372
373template<typename ValueType, bool RawMode>
375 if (!this->currentModelHasBeenOptimized) {
376 return false;
377 }
378 int optimalityStatus = 0;
379
380 int error = GRBgetintattr(model, GRB_INT_ATTR_STATUS, &optimalityStatus);
381 STORM_LOG_THROW(error == 0, storm::exceptions::InvalidStateException,
382 "Unable to retrieve optimization status of Gurobi model (" << GRBgeterrormsg(**environment) << ", error code " << error << ").");
383
384 return optimalityStatus == GRB_OPTIMAL;
385}
386
387template<typename ValueType, bool RawMode>
389 if (!this->isOptimal()) {
390 STORM_LOG_THROW(!this->isInfeasible(), storm::exceptions::InvalidAccessException,
391 "Unable to get Gurobi solution from infeasible model (" << GRBgeterrormsg(**environment) << ").");
392 STORM_LOG_THROW(!this->isUnbounded(), storm::exceptions::InvalidAccessException,
393 "Unable to get Gurobi solution from unbounded model (" << GRBgeterrormsg(**environment) << ").");
394 STORM_LOG_THROW(false, storm::exceptions::InvalidAccessException,
395 "Unable to get Gurobi solution from unoptimized model (" << GRBgeterrormsg(**environment) << ").");
396 }
397
398 int varIndex;
399 if constexpr (RawMode) {
400 varIndex = variable;
401 } else {
402 STORM_LOG_ASSERT(variableToIndexMap.count(variable) != 0, "Accessing value of unknown variable '" << variable.getName() << "'.");
403 varIndex = variableToIndexMap.at(variable);
404 }
405
406 double value = 0;
407 int error = GRBgetdblattrelement(model, GRB_DBL_ATTR_X, varIndex, &value);
408 STORM_LOG_THROW(error == 0, storm::exceptions::InvalidStateException,
409 "Unable to get Gurobi solution (" << GRBgeterrormsg(**environment) << ", error code " << error << ").");
410
411 return storm::utility::convertNumber<ValueType>(value);
412}
413
414template<typename ValueType, bool RawMode>
415int_fast64_t GurobiLpSolver<ValueType, RawMode>::getIntegerValue(Variable const& variable) const {
416 if (!this->isOptimal()) {
417 STORM_LOG_THROW(!this->isInfeasible(), storm::exceptions::InvalidAccessException,
418 "Unable to get Gurobi solution from infeasible model (" << GRBgeterrormsg(**environment) << ").");
419 STORM_LOG_THROW(!this->isUnbounded(), storm::exceptions::InvalidAccessException,
420 "Unable to get Gurobi solution from unbounded model (" << GRBgeterrormsg(**environment) << ").");
421 STORM_LOG_THROW(false, storm::exceptions::InvalidAccessException,
422 "Unable to get Gurobi solution from unoptimized model (" << GRBgeterrormsg(**environment) << ").");
423 }
424
425 int varIndex;
426 if constexpr (RawMode) {
427 varIndex = variable;
428 } else {
429 STORM_LOG_ASSERT(variableToIndexMap.count(variable) != 0, "Accessing value of unknown variable '" << variable.getName() << "'.");
430 varIndex = variableToIndexMap.at(variable);
431 }
432
433 double value = 0;
434 int error = GRBgetdblattrelement(model, GRB_DBL_ATTR_X, varIndex, &value);
435 STORM_LOG_THROW(error == 0, storm::exceptions::InvalidStateException,
436 "Unable to get Gurobi solution (" << GRBgeterrormsg(**environment) << ", error code " << error << ").");
437 double roundedValue = std::round(value);
438 double diff = std::abs(roundedValue - value);
439 STORM_LOG_ERROR_COND(diff <= storm::settings::getModule<storm::settings::modules::GurobiSettings>().getIntegerTolerance(),
440 "Illegal value for integer variable in Gurobi solution (" << value << "). Difference to nearest int is " << diff);
441 return static_cast<int_fast64_t>(roundedValue);
442}
443
444template<typename ValueType, bool RawMode>
445bool GurobiLpSolver<ValueType, RawMode>::getBinaryValue(Variable const& variable) const {
446 if (!this->isOptimal()) {
447 STORM_LOG_THROW(!this->isInfeasible(), storm::exceptions::InvalidAccessException,
448 "Unable to get Gurobi solution from infeasible model (" << GRBgeterrormsg(**environment) << ").");
449 STORM_LOG_THROW(!this->isUnbounded(), storm::exceptions::InvalidAccessException,
450 "Unable to get Gurobi solution from unbounded model (" << GRBgeterrormsg(**environment) << ").");
451 STORM_LOG_THROW(false, storm::exceptions::InvalidAccessException,
452 "Unable to get Gurobi solution from unoptimized model (" << GRBgeterrormsg(**environment) << ").");
453 }
454
455 int varIndex;
456 if constexpr (RawMode) {
457 varIndex = variable;
458 } else {
459 STORM_LOG_ASSERT(variableToIndexMap.count(variable) != 0, "Accessing value of unknown variable '" << variable.getName() << "'.");
460 varIndex = variableToIndexMap.at(variable);
461 }
462
463 double value = 0;
464 int error = GRBgetdblattrelement(model, GRB_DBL_ATTR_X, varIndex, &value);
465 STORM_LOG_THROW(error == 0, storm::exceptions::InvalidStateException,
466 "Unable to get Gurobi solution (" << GRBgeterrormsg(**environment) << ", error code " << error << ").");
467
468 if (value > 0.5) {
469 STORM_LOG_ERROR_COND(std::abs(value - 1.0) <= storm::settings::getModule<storm::settings::modules::GurobiSettings>().getIntegerTolerance(),
470 "Illegal value for binary variable in Gurobi solution (" << value << ").");
471 return true;
472 } else {
473 STORM_LOG_ERROR_COND(std::abs(value) <= storm::settings::getModule<storm::settings::modules::GurobiSettings>().getIntegerTolerance(),
474 "Illegal value for binary variable in Gurobi solution (" << value << ").");
475 return false;
476 }
477}
478
479template<typename ValueType, bool RawMode>
481 if (!this->isOptimal()) {
482 STORM_LOG_THROW(!this->isInfeasible(), storm::exceptions::InvalidAccessException,
483 "Unable to get Gurobi solution from infeasible model (" << GRBgeterrormsg(**environment) << ").");
484 STORM_LOG_THROW(!this->isUnbounded(), storm::exceptions::InvalidAccessException,
485 "Unable to get Gurobi solution from unbounded model (" << GRBgeterrormsg(**environment) << ").");
486 STORM_LOG_THROW(false, storm::exceptions::InvalidAccessException,
487 "Unable to get Gurobi solution from unoptimized model (" << GRBgeterrormsg(**environment) << ").");
488 }
489
490 double value = 0;
491 int error = GRBgetdblattr(model, GRB_DBL_ATTR_OBJVAL, &value);
492 STORM_LOG_THROW(error == 0, storm::exceptions::InvalidStateException,
493 "Unable to get Gurobi solution (" << GRBgeterrormsg(**environment) << ", error code " << error << ").");
494
495 return storm::utility::convertNumber<ValueType>(value);
496}
497
498template<typename ValueType, bool RawMode>
499void GurobiLpSolver<ValueType, RawMode>::writeModelToFile(std::string const& filename) const {
500 int error = GRBwrite(model, filename.c_str());
501 if (error) {
502 STORM_LOG_ERROR("Unable to write Gurobi model (" << GRBgeterrormsg(**environment) << ", error code " << error << ") to file.");
503 throw storm::exceptions::InvalidStateException()
504 << "Unable to write Gurobi model (" << GRBgeterrormsg(**environment) << ", error code " << error << ") to file.";
505 }
506}
507
508template<typename ValueType, bool RawMode>
510 IncrementalLevel lvl;
511 int num;
512 GRBgetintattr(model, GRB_INT_ATTR_NUMCONSTRS, &num);
513 lvl.firstConstraintIndex = num;
514 GRBgetintattr(model, GRB_INT_ATTR_NUMGENCONSTRS, &num);
515 lvl.firstGenConstraintIndex = num;
516 incrementalData.push_back(lvl);
517}
518
519template<typename ValueType, bool RawMode>
521 if (incrementalData.empty()) {
522 STORM_LOG_ERROR("Tried to pop from a solver without pushing before.");
523 } else {
524 IncrementalLevel const& lvl = incrementalData.back();
525 int num;
526 GRBgetintattr(model, GRB_INT_ATTR_NUMCONSTRS, &num);
527 std::vector<int> indicesToBeRemoved = storm::utility::vector::buildVectorForRange(lvl.firstConstraintIndex, num);
528 int error = GRBdelconstrs(model, indicesToBeRemoved.size(), indicesToBeRemoved.data());
529 STORM_LOG_THROW(error == 0, storm::exceptions::InvalidStateException,
530 "Unable to delete constraints (" << GRBgeterrormsg(**environment) << ", error code " << error << ").");
531 GRBgetintattr(model, GRB_INT_ATTR_NUMGENCONSTRS, &num);
532 indicesToBeRemoved = storm::utility::vector::buildVectorForRange(lvl.firstGenConstraintIndex, num);
533 STORM_LOG_THROW(error == 0, storm::exceptions::InvalidStateException,
534 "Unable to delete general constraints (" << GRBgeterrormsg(**environment) << ", error code " << error << ").");
535 indicesToBeRemoved.clear();
536
537 if (!lvl.variables.empty()) {
538 int firstIndex = -1;
539 bool first = true;
540 for (auto const& var : lvl.variables) {
541 if (first) {
542 auto it = variableToIndexMap.find(var);
543 firstIndex = it->second;
544 variableToIndexMap.erase(it);
545 first = false;
546 } else {
547 variableToIndexMap.erase(var);
548 }
549 }
550 std::vector<int> indicesToBeRemoved = storm::utility::vector::buildVectorForRange(firstIndex, nextVariableIndex);
551 error = GRBdelvars(model, indicesToBeRemoved.size(), indicesToBeRemoved.data());
552 STORM_LOG_THROW(error == 0, storm::exceptions::InvalidStateException,
553 "Unable to delete variables (" << GRBgeterrormsg(**environment) << ", error code " << error << ").");
554 nextVariableIndex = firstIndex;
555 }
556 update();
557 // Assert that indices are as expected
558 GRBgetintattr(model, GRB_INT_ATTR_NUMCONSTRS, &num);
559 STORM_LOG_THROW(lvl.firstConstraintIndex == num, storm::exceptions::InvalidStateException, "Unexpected number of constraints after deletion.");
560 GRBgetintattr(model, GRB_INT_ATTR_NUMGENCONSTRS, &num);
561 STORM_LOG_THROW(lvl.firstGenConstraintIndex == num, storm::exceptions::InvalidStateException,
562 "Unexpected number of general constraints after deletion.");
563 GRBgetintattr(model, GRB_INT_ATTR_NUMVARS, &num);
564 STORM_LOG_THROW(nextVariableIndex == num, storm::exceptions::InvalidStateException, "Unexpected number ofvariables after deletion.");
565
566 incrementalData.pop_back();
567 }
568}
569
570template<typename ValueType, bool RawMode>
572 int error = GRBsetintparam(GRBgetenv(model), "PoolSolutions", value);
573 STORM_LOG_THROW(error == 0, storm::exceptions::InvalidStateException,
574 "Unable to set Gurobi Parameter PoolSolutions (" << GRBgeterrormsg(**environment) << ", error code " << error << ").");
575}
576
577template<typename ValueType, bool RawMode>
579 STORM_LOG_THROW(this->currentModelHasBeenOptimized, storm::exceptions::InvalidStateException,
580 "Illegal call to GurobiLpSolver<ValueType, RawMode>::getSolutionCount: model has not been optimized.");
581 int result = -1;
582 int error = GRBgetintattr(model, "SolCount", &result);
583 STORM_LOG_THROW(error == 0 && result >= 0, storm::exceptions::InvalidStateException, "Unable to get solution count or invalid number of solutions.");
584 return result;
585}
586
587template<typename ValueType, bool RawMode>
588ValueType GurobiLpSolver<ValueType, RawMode>::getContinuousValue(Variable const& variable, uint64_t const& solutionIndex) const {
589 if (!this->isOptimal()) {
590 STORM_LOG_THROW(this->currentModelHasBeenOptimized, storm::exceptions::InvalidAccessException,
591 "Unable to get Gurobi solution from unoptimized model (" << GRBgeterrormsg(**environment) << ").");
592 }
593 STORM_LOG_ASSERT(solutionIndex < getSolutionCount(), "Invalid solution index.");
594
595 int varIndex;
596 if constexpr (RawMode) {
597 varIndex = variable;
598 } else {
599 STORM_LOG_THROW(variableToIndexMap.count(variable) != 0, storm::exceptions::InvalidAccessException,
600 "Accessing value of unknown variable '" << variable.getName() << "'.");
601 varIndex = variableToIndexMap.at(variable);
602 }
603
604 double value = 0;
605 int error = GRBsetintparam(GRBgetenv(model), GRB_INT_PAR_SOLUTIONNUMBER, solutionIndex);
606 STORM_LOG_THROW(error == 0, storm::exceptions::InvalidStateException,
607 "Unable to set Gurobi solution index (" << GRBgeterrormsg(**environment) << ", error code " << error << ").");
608 error = GRBgetdblattrelement(model, GRB_DBL_ATTR_Xn, varIndex, &value);
609 STORM_LOG_THROW(error == 0, storm::exceptions::InvalidStateException,
610 "Unable to get Gurobi solution (" << GRBgeterrormsg(**environment) << ", error code " << error << ").");
611
612 return storm::utility::convertNumber<ValueType>(value);
613}
614
615template<typename ValueType, bool RawMode>
616int_fast64_t GurobiLpSolver<ValueType, RawMode>::getIntegerValue(Variable const& variable, uint64_t const& solutionIndex) const {
617 if (!this->isOptimal()) {
618 STORM_LOG_THROW(this->currentModelHasBeenOptimized, storm::exceptions::InvalidAccessException,
619 "Unable to get Gurobi solution from unoptimized model (" << GRBgeterrormsg(**environment) << ").");
620 }
621 STORM_LOG_ASSERT(solutionIndex < getSolutionCount(), "Invalid solution index.");
622
623 int varIndex;
624 if constexpr (RawMode) {
625 varIndex = variable;
626 } else {
627 STORM_LOG_THROW(variableToIndexMap.count(variable) != 0, storm::exceptions::InvalidAccessException,
628 "Accessing value of unknown variable '" << variable.getName() << "'.");
629 varIndex = variableToIndexMap.at(variable);
630 }
631
632 double value = 0;
633 int error = GRBsetintparam(GRBgetenv(model), GRB_INT_PAR_SOLUTIONNUMBER, solutionIndex);
634 STORM_LOG_THROW(error == 0, storm::exceptions::InvalidStateException,
635 "Unable to set Gurobi solution index (" << GRBgeterrormsg(**environment) << ", error code " << error << ").");
636 error = GRBgetdblattrelement(model, GRB_DBL_ATTR_Xn, varIndex, &value);
637 STORM_LOG_THROW(error == 0, storm::exceptions::InvalidStateException,
638 "Unable to get Gurobi solution (" << GRBgeterrormsg(**environment) << ", error code " << error << ").");
639 double roundedValue = std::round(value);
640 double diff = std::abs(roundedValue - value);
641 STORM_LOG_ERROR_COND(diff <= storm::settings::getModule<storm::settings::modules::GurobiSettings>().getIntegerTolerance(),
642 "Illegal value for integer variable in Gurobi solution (" << value << "). Difference to nearest int is " << diff);
643 return static_cast<int_fast64_t>(roundedValue);
644}
645
646template<typename ValueType, bool RawMode>
647bool GurobiLpSolver<ValueType, RawMode>::getBinaryValue(Variable const& variable, uint64_t const& solutionIndex) const {
648 if (!this->isOptimal()) {
649 STORM_LOG_THROW(this->currentModelHasBeenOptimized, storm::exceptions::InvalidAccessException,
650 "Unable to get Gurobi solution from unoptimized model (" << GRBgeterrormsg(**environment) << ").");
651 }
652 STORM_LOG_ASSERT(solutionIndex < getSolutionCount(), "Invalid solution index.");
653
654 int varIndex;
655 if constexpr (RawMode) {
656 varIndex = variable;
657 } else {
658 STORM_LOG_THROW(variableToIndexMap.count(variable) != 0, storm::exceptions::InvalidAccessException,
659 "Accessing value of unknown variable '" << variable.getName() << "'.");
660 varIndex = variableToIndexMap.at(variable);
661 }
662
663 double value = 0;
664 int error = GRBsetintparam(GRBgetenv(model), GRB_INT_PAR_SOLUTIONNUMBER, solutionIndex);
665 STORM_LOG_THROW(error == 0, storm::exceptions::InvalidStateException,
666 "Unable to set Gurobi solution index (" << GRBgeterrormsg(**environment) << ", error code " << error << ").");
667 error = GRBgetdblattrelement(model, GRB_DBL_ATTR_Xn, varIndex, &value);
668 STORM_LOG_THROW(error == 0, storm::exceptions::InvalidStateException,
669 "Unable to get Gurobi solution (" << GRBgeterrormsg(**environment) << ", error code " << error << ").");
670
671 if (value > 0.5) {
672 STORM_LOG_ERROR_COND(std::abs(value - 1) <= storm::settings::getModule<storm::settings::modules::GurobiSettings>().getIntegerTolerance(),
673 "Illegal value for integer variable in Gurobi solution (" << value << ").");
674 return true;
675 } else {
676 STORM_LOG_ERROR_COND(std::abs(value) <= storm::settings::getModule<storm::settings::modules::GurobiSettings>().getIntegerTolerance(),
677 "Illegal value for integer variable in Gurobi solution (" << value << ").");
678 return false;
679 }
680}
681
682template<typename ValueType, bool RawMode>
684 if (!this->isOptimal()) {
685 STORM_LOG_THROW(this->currentModelHasBeenOptimized, storm::exceptions::InvalidAccessException,
686 "Unable to get Gurobi solution from unoptimized model (" << GRBgeterrormsg(**environment) << ").");
687 }
688 STORM_LOG_ASSERT(solutionIndex < getSolutionCount(), "Invalid solution index.");
689
690 double value = 0;
691 int error = GRBsetintparam(GRBgetenv(model), GRB_INT_PAR_SOLUTIONNUMBER, solutionIndex);
692 STORM_LOG_THROW(error == 0, storm::exceptions::InvalidStateException,
693 "Unable to set Gurobi solution index (" << GRBgeterrormsg(**environment) << ", error code " << error << ").");
694 error = GRBgetdblattr(model, GRB_DBL_ATTR_POOLOBJVAL, &value);
695 STORM_LOG_THROW(error == 0, storm::exceptions::InvalidStateException,
696 "Unable to get Gurobi solution (" << GRBgeterrormsg(**environment) << ", error code " << error << ").");
697
698 return storm::utility::convertNumber<ValueType>(value);
699}
700
701template<typename ValueType, bool RawMode>
702void GurobiLpSolver<ValueType, RawMode>::setMaximalMILPGap(ValueType const& gap, bool relative) {
703 int error = -1;
704 if (relative) {
705 error = GRBsetdblparam(GRBgetenv(model), GRB_DBL_PAR_MIPGAP, storm::utility::convertNumber<double>(gap));
706 } else {
707 error = GRBsetdblparam(GRBgetenv(model), GRB_DBL_PAR_MIPGAPABS, storm::utility::convertNumber<double>(gap));
708 }
709 STORM_LOG_THROW(error == 0, storm::exceptions::InvalidStateException,
710 "Unable to set Gurobi MILP GAP (" << GRBgeterrormsg(**environment) << ", error code " << error << ").");
711}
712
713template<typename ValueType, bool RawMode>
715 double relativeGap;
716 int error = GRBgetdblattr(model, GRB_DBL_ATTR_MIPGAP, &relativeGap);
717 STORM_LOG_THROW(error == 0, storm::exceptions::InvalidStateException,
718 "Unable to get Gurobi MILP GAP (" << GRBgeterrormsg(**environment) << ", error code " << error << ").");
719 auto result = storm::utility::convertNumber<ValueType>(relativeGap);
720 if (relative) {
721 return result;
722 } else {
723 return storm::utility::abs<ValueType>(result * getObjectiveValue());
724 }
725}
726
727template<typename ValueType, bool RawMode>
729 int error = GRBsetdblparam(GRBgetenv(model), GRB_DBL_PAR_TIMELIMIT, seconds);
730 timeLimit.emplace(seconds);
731 STORM_LOG_THROW(error == 0, storm::exceptions::InvalidStateException,
732 "Unable to set Gurobi time limit (" << GRBgeterrormsg(**environment) << ", error code " << error << ").");
733}
734
735template<typename ValueType, bool RawMode>
737 STORM_LOG_THROW(timeLimit.has_value(), storm::exceptions::InvalidAccessException, "Unable to get Gurobi time limit because none was specified.");
738 return timeLimit.value();
739}
740
741template<typename ValueType, bool RawMode>
743 return timeLimit.has_value();
744}
745
746template<typename ValueType, bool RawMode>
748 if (!this->currentModelHasBeenOptimized) {
749 return false;
750 }
751 int status = 0;
752
753 int error = GRBgetintattr(model, GRB_INT_ATTR_STATUS, &status);
754 STORM_LOG_THROW(error == 0, storm::exceptions::InvalidStateException,
755 "Unable to retrieve optimization status of Gurobi model (" << GRBgeterrormsg(**environment) << ", error code " << error << ").");
756
757 return status == GRB_TIME_LIMIT;
758}
759
760#else
761template<typename ValueType, bool RawMode>
762GurobiLpSolver<ValueType, RawMode>::GurobiLpSolver(std::shared_ptr<GurobiEnvironment> const&, std::string const&, OptimizationDirection const&) {
763 throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that "
764 "requires this support. Please choose a version of support with Gurobi support.";
765}
766
767template<typename ValueType, bool RawMode>
768GurobiLpSolver<ValueType, RawMode>::GurobiLpSolver(std::shared_ptr<GurobiEnvironment> const&, std::string const&) {
769 throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that "
770 "requires this support. Please choose a version of support with Gurobi support.";
771}
772
773template<typename ValueType, bool RawMode>
774GurobiLpSolver<ValueType, RawMode>::GurobiLpSolver(std::shared_ptr<GurobiEnvironment> const&, OptimizationDirection const&) {
775 throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that "
776 "requires this support. Please choose a version of support with Gurobi support.";
777}
778
779template<typename ValueType, bool RawMode>
780GurobiLpSolver<ValueType, RawMode>::GurobiLpSolver(std::shared_ptr<GurobiEnvironment> const&) {
781 throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that "
782 "requires this support. Please choose a version of support with Gurobi support.";
783}
784
785template<typename ValueType, bool RawMode>
787
788template<typename ValueType, bool RawMode>
790 std::optional<ValueType> const&,
791 std::optional<ValueType> const&, ValueType) {
792 throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that "
793 "requires this support. Please choose a version of support with Gurobi support.";
794}
795
796template<typename ValueType, bool RawMode>
798 throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that "
799 "requires this support. Please choose a version of support with Gurobi support.";
800}
801
802template<typename ValueType, bool RawMode>
804 throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that "
805 "requires this support. Please choose a version of support with Gurobi support.";
806}
807
808template<typename ValueType, bool RawMode>
810 throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that "
811 "requires this support. Please choose a version of support with Gurobi support.";
812}
813
814template<typename ValueType, bool RawMode>
816 throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that "
817 "requires this support. Please choose a version of support with Gurobi support.";
818}
819
820template<typename ValueType, bool RawMode>
822 throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that "
823 "requires this support. Please choose a version of support with Gurobi support.";
824}
825
826template<typename ValueType, bool RawMode>
828 throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that "
829 "requires this support. Please choose a version of support with Gurobi support.";
830}
831
832template<typename ValueType, bool RawMode>
834 throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that "
835 "requires this support. Please choose a version of support with Gurobi support.";
836}
837
838template<typename ValueType, bool RawMode>
840 throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that "
841 "requires this support. Please choose a version of support with Gurobi support.";
842}
843
844template<typename ValueType, bool RawMode>
846 throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that "
847 "requires this support. Please choose a version of support with Gurobi support.";
848}
849
850template<typename ValueType, bool RawMode>
852 throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that "
853 "requires this support. Please choose a version of support with Gurobi support.";
854}
855
856template<typename ValueType, bool RawMode>
858 throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that "
859 "requires this support. Please choose a version of support with Gurobi support.";
860}
861
862template<typename ValueType, bool RawMode>
864 throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that "
865 "requires this support. Please choose a version of support with Gurobi support.";
866}
867
868template<typename ValueType, bool RawMode>
870 throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that "
871 "requires this support. Please choose a version of support with Gurobi support.";
872}
873
874template<typename ValueType, bool RawMode>
876 throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that "
877 "requires this support. Please choose a version of support with Gurobi support.";
878}
879
880template<typename ValueType, bool RawMode>
882 throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that "
883 "requires this support. Please choose a version of storm with Gurobi support.";
884}
885
886template<typename ValueType, bool RawMode>
888 throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that "
889 "requires this support. Please choose a version of storm with Gurobi support.";
890}
891
892template<typename ValueType, bool RawMode>
893ValueType GurobiLpSolver<ValueType, RawMode>::getContinuousValue(Variable const&, uint64_t const&) const {
894 throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that "
895 "requires this support. Please choose a version of storm with Gurobi support.";
896}
897
898template<typename ValueType, bool RawMode>
899int_fast64_t GurobiLpSolver<ValueType, RawMode>::getIntegerValue(Variable const&, uint64_t const&) const {
900 throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that "
901 "requires this support. Please choose a version of storm with Gurobi support.";
902}
903
904template<typename ValueType, bool RawMode>
906 throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that "
907 "requires this support. Please choose a version of storm with Gurobi support.";
908}
909
910template<typename ValueType, bool RawMode>
912 throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that "
913 "requires this support. Please choose a version of storm with Gurobi support.";
914}
915
916template<typename ValueType, bool RawMode>
918 throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that "
919 "requires this support. Please choose a version of storm with Gurobi support.";
920}
921
922template<typename ValueType, bool RawMode>
924 throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that "
925 "requires this support. Please choose a version of storm with Gurobi support.";
926}
927
928template<typename ValueType, bool RawMode>
930 throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that "
931 "requires this support. Please choose a version of storm with Gurobi support.";
932}
933
934template<typename ValueType, bool RawMode>
936 throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that "
937 "requires this support. Please choose a version of storm with Gurobi support.";
938}
939
940template<typename ValueType, bool RawMode>
942 throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that "
943 "requires this support. Please choose a version of storm with Gurobi support.";
944}
945
946template<typename ValueType, bool RawMode>
948 throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that "
949 "requires this support. Please choose a version of storm with Gurobi support.";
950}
951
952#endif
953
954std::string toString(GurobiSolverMethod const& method) {
955 switch (method) {
957 return "auto";
959 return "primal-simplex";
961 return "dual-simplex";
963 return "barrier";
965 return "concurrent";
967 return "deterministic-concurrent";
969 return "deterministic-concurrent-simplex";
970 }
971 STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Unknown solver method");
972}
973
974std::optional<GurobiSolverMethod> gurobiSolverMethodFromString(std::string const& method) {
975 for (auto const& mt : getGurobiSolverMethods()) {
976 if (toString(mt) == method) {
977 return mt;
978 }
979 }
980 return {};
981}
982
987
988template class GurobiLpSolver<double, true>;
989template class GurobiLpSolver<double, false>;
990template class GurobiLpSolver<storm::RationalNumber, true>;
991template class GurobiLpSolver<storm::RationalNumber, false>;
992} // namespace solver
993} // namespace storm
VariableCoefficients getLinearCoefficients(Expression const &expression)
Computes the (double) coefficients of all identifiers appearing in the expression if the expression w...
void initialize()
Sets some properties of the Gurobi environment according to parameters given by the options.
virtual ~GurobiLpSolver()
Destructs a solver by freeing the pointers to Gurobi's structures.
virtual bool isInfeasible() const override
Retrieves whether the model was found to be infeasible.
virtual int_fast64_t getIntegerValue(Variable const &name) const override
Retrieves the value of the integer variable with the given name.
virtual bool isUnbounded() const override
Retrieves whether the model was found to be infeasible.
virtual void setMaximalMILPGap(ValueType const &gap, bool relative) override
Specifies the maximum difference between lower- and upper objective bounds that triggers termination.
virtual void push() override
Pushes a backtracking point on the solver's stack.
void setMaximalSolutionCount(uint64_t value)
typename LpSolver< ValueType, RawMode >::VariableType VariableType
GurobiLpSolver(std::shared_ptr< GurobiEnvironment > const &environment, std::string const &name, OptimizationDirection const &optDir)
Constructs a solver with the given name and model sense.
virtual void addIndicatorConstraint(std::string const &name, Variable indicatorVariable, bool indicatorValue, Constraint const &constraint) override
Adds the given indicator constraint to the LP problem: "If indicatorVariable == indicatorValue,...
virtual void addConstraint(std::string const &name, Constraint const &constraint) override
Adds a the given constraint to the LP problem.
virtual ValueType getContinuousValue(Variable const &name) const override
Retrieves the value of the continuous variable with the given name.
virtual bool getBinaryValue(Variable const &name) const override
Retrieves the value of the binary variable with the given name.
virtual ValueType getObjectiveValue() const override
Retrieves the value of the objective function.
void setTimeLimit(uint64_t seconds)
virtual void pop() override
Pops a backtracking point from the solver's stack.
virtual void writeModelToFile(std::string const &filename) const override
Writes the current LP problem to the given file.
typename LpSolver< ValueType, RawMode >::Variable Variable
virtual void optimize() const override
Optimizes the LP problem previously constructed.
virtual Variable addVariable(std::string const &name, VariableType const &type, std::optional< ValueType > const &lowerBound=std::nullopt, std::optional< ValueType > const &upperBound=std::nullopt, ValueType objectiveFunctionCoefficient=0) override
Registers a variable of the given type.
typename LpSolver< ValueType, RawMode >::Constraint Constraint
virtual ValueType getMILPGap(bool relative) const override
Returns the obtained gap after a call to optimize()
virtual bool isOptimal() const override
Retrieves whether the model was found to be optimal, i.e.
virtual void update() const override
Updates the model to make the variables that have been declared since the last call to update usable.
An interface that captures the functionality of an LP solver.
Definition LpSolver.h:51
#define STORM_LOG_TRACE(message)
Definition logging.h:12
#define STORM_LOG_ERROR(message)
Definition logging.h:26
#define STORM_LOG_ASSERT(cond, message)
Definition macros.h:11
#define STORM_LOG_ERROR_COND(cond, message)
Definition macros.h:52
#define STORM_LOG_THROW(cond, exception, message)
Definition macros.h:30
SFTBDDChecker::ValueType ValueType
RelationType
An enum type specifying the different relations applicable.
std::string toString(GurobiSolverMethod const &method)
Yields a string representation of the GurobiSolverMethod.
std::optional< GurobiSolverMethod > gurobiSolverMethodFromString(std::string const &method)
std::vector< GurobiSolverMethod > getGurobiSolverMethods()
std::vector< T > buildVectorForRange(T min, T max)
Constructs a vector [min, min+1, ...., max-1].
Definition vector.h:129
TargetType convertNumber(SourceType const &number)
std::map< storm::expressions::Variable, double >::const_iterator end() const
void separateVariablesFromConstantPart(VariableCoefficients &rhs)
Brings all variables of the right-hand side coefficients to the left-hand side by negating them and m...
std::map< storm::expressions::Variable, double >::const_iterator begin() const