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