Storm
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
GlpkLpSolver.cpp
Go to the documentation of this file.
2
3#include <cmath>
4#include <iostream>
5
7
13
17
23
26
27namespace storm {
28namespace solver {
29
30#ifdef STORM_HAVE_GLPK
31template<typename ValueType, bool RawMode>
33 : LpSolver<ValueType, RawMode>(optDir),
34 lp(nullptr),
35 variableToIndexMap(),
36 modelContainsIntegerVariables(false),
37 isInfeasibleFlag(false),
38 isUnboundedFlag(false) {
39 // Create the LP problem for glpk.
40 lp = glp_create_prob();
41
42 // Set its name and model sense.
43 glp_set_prob_name(lp, name.c_str());
44
45 // Set whether the glpk output shall be printed to the command line.
48 ? GLP_ON
49 : GLP_OFF);
50
51 // Set the maximal allowed MILP gap to its default value
52 glp_iocp* defaultParameters = new glp_iocp();
53 glp_init_iocp(defaultParameters);
54 this->maxMILPGap = defaultParameters->mip_gap;
55 this->maxMILPGapRelative = true;
56}
57
58#else
59
60template<typename ValueType, bool RawMode>
62 // Throw nothing in a constructor.
63}
64#endif
65
66template<typename ValueType, bool RawMode>
68 // Intentionally left empty.
69}
70
71template<typename ValueType, bool RawMode>
75
76template<typename ValueType, bool RawMode>
78 // Intentionally left empty.
79}
80
81template<typename ValueType, bool RawMode>
83#ifdef STORM_HAVE_GLPK
84 // Dispose of all objects allocated dynamically by glpk.
85 glp_delete_prob(this->lp);
86 glp_free_env();
87#endif
88}
89
90template<typename ValueType, bool RawMode>
92#ifdef STORM_HAVE_GLPK
93 switch (type) {
95 return GLP_CV;
97 return GLP_IV;
99 return GLP_BV;
100 }
101 STORM_LOG_ASSERT(false, "Unexpected variable type.");
102 return -1;
103#else
104 throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for GLPK. Yet, a method was called that "
105 "requires this support. Please choose a version with GLPK support.";
106#endif
107}
108
109template<typename ValueType, bool RawMode>
111 std::optional<ValueType> const& lowerBound,
112 std::optional<ValueType> const& upperBound,
113 ValueType objectiveFunctionCoefficient) {
114#ifdef STORM_HAVE_GLPK
115 Variable resultVar;
116 if constexpr (RawMode) {
117 resultVar = variableToIndexMap.size();
118 } else {
119 resultVar = this->declareOrGetExpressionVariable(name, type);
120 // Assert whether the variable does not exist yet.
121 // Due to incremental usage (push(), pop()), a variable might be declared in the manager but not in the lp model.
122 STORM_LOG_ASSERT(variableToIndexMap.count(resultVar) == 0, "Variable " << resultVar.getName() << " exists already in the model.");
123 }
124
125 int boundType;
126 if (lowerBound.has_value()) {
127 boundType = upperBound.has_value() ? GLP_DB : GLP_LO;
128 } else {
129 boundType = upperBound.has_value() ? GLP_UP : GLP_FR;
130 }
131
132 if (type == VariableType::Integer || type == VariableType::Binary) {
133 this->modelContainsIntegerVariables = true;
134 }
135
136 // Create the variable in glpk.
137 int variableIndex = glp_add_cols(this->lp, 1);
138 glp_set_col_name(this->lp, variableIndex, name.c_str());
139 glp_set_col_bnds(lp, variableIndex, boundType, lowerBound.has_value() ? storm::utility::convertNumber<double>(*lowerBound) : 0.0,
140 upperBound.has_value() ? storm::utility::convertNumber<double>(*upperBound) : 0.0);
141 glp_set_col_kind(this->lp, variableIndex, getGlpkType<ValueType, RawMode>(type));
142 glp_set_obj_coef(this->lp, variableIndex, storm::utility::convertNumber<double>(objectiveFunctionCoefficient));
143
144 if constexpr (RawMode) {
145 this->variableToIndexMap.push_back(variableIndex);
146 } else {
147 this->variableToIndexMap.emplace(resultVar, variableIndex);
148 if (!incrementalData.empty()) {
149 incrementalData.back().variables.push_back(resultVar);
150 }
151 }
152
153 return resultVar;
154#else
155 throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for GLPK. Yet, a method was called that "
156 "requires this support. Please choose a version with GLPK support.";
157#endif
158}
159
160template<typename ValueType, bool RawMode>
162 // Intentionally left empty.
163}
164
165template<typename ValueType, bool RawMode>
166void GlpkLpSolver<ValueType, RawMode>::addConstraint(std::string const& name, Constraint const& constraint) {
167#ifdef STORM_HAVE_GLPK
168 // Add the row that will represent this constraint.
169 int constraintIndex = glp_add_rows(this->lp, 1);
170 glp_set_row_name(this->lp, constraintIndex, name.c_str());
171
172 // Extract constraint data
173 double rhs;
175 // glpk uses 1-based indexing (wtf!?)...
176 std::vector<int> variableIndices(1, -1);
177 std::vector<double> coefficients(1, 0.0);
178 if constexpr (RawMode) {
179 rhs = storm::utility::convertNumber<double>(constraint.rhs);
180 relationType = constraint.relationType;
181 variableIndices.reserve(constraint.lhsVariableIndices.size() + 1);
182 for (auto const& var : constraint.lhsVariableIndices) {
183 variableIndices.push_back(this->variableToIndexMap.at(var));
184 }
185 coefficients.reserve(constraint.lhsCoefficients.size() + 1);
186 for (auto const& coef : constraint.lhsCoefficients) {
187 coefficients.push_back(storm::utility::convertNumber<double>(coef));
188 }
189 } else {
190 STORM_LOG_THROW(constraint.getManager() == this->getManager(), storm::exceptions::InvalidArgumentException,
191 "Constraint was not built over the proper variables.");
192 STORM_LOG_THROW(constraint.isRelationalExpression(), storm::exceptions::InvalidArgumentException, "Illegal constraint is not a relational expression.");
193
198 leftCoefficients.separateVariablesFromConstantPart(rightCoefficients);
199 rhs = rightCoefficients.getConstantPart();
200 relationType = constraint.getBaseExpression().asBinaryRelationExpression().getRelationType();
201 int len = std::distance(leftCoefficients.begin(), leftCoefficients.end());
202 variableIndices.reserve(len + 1);
203 coefficients.reserve(len + 1);
204 for (auto const& variableCoefficientPair : leftCoefficients) {
205 auto variableIndexPair = this->variableToIndexMap.find(variableCoefficientPair.first);
206 variableIndices.push_back(variableIndexPair->second);
207 coefficients.push_back(variableCoefficientPair.second);
208 }
209 }
210
211 // Determine the type of the constraint and add it properly.
212 switch (relationType) {
214 glp_set_row_bnds(this->lp, constraintIndex, GLP_UP, 0,
216 break;
218 glp_set_row_bnds(this->lp, constraintIndex, GLP_UP, 0, rhs);
219 break;
221 glp_set_row_bnds(this->lp, constraintIndex, GLP_LO,
223 break;
225 glp_set_row_bnds(this->lp, constraintIndex, GLP_LO, rhs, 0);
226 break;
228 glp_set_row_bnds(this->lp, constraintIndex, GLP_FX, rhs, rhs);
229 break;
230 default:
231 STORM_LOG_ASSERT(false, "Illegal operator in LP solver constraint.");
232 }
233
234 // Add the constraints
235 glp_set_mat_row(this->lp, constraintIndex, variableIndices.size() - 1, variableIndices.data(), coefficients.data());
236
237 this->currentModelHasBeenOptimized = false;
238#else
239 throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for GLPK. Yet, a method was called that "
240 "requires this support. Please choose a version with GLPK support.";
241#endif
242}
243
244template<typename ValueType, bool RawMode>
246 STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Indicator constraints are not supported for GLPK.");
247}
248
249#ifdef STORM_HAVE_GLPK
250// Method used within the MIP solver to terminate early
251void callback(glp_tree* t, void* info) {
252 auto& mipgap = *static_cast<std::pair<double, bool>*>(info);
253 double actualRelativeGap = glp_ios_mip_gap(t);
254 double factor = storm::utility::one<double>();
255 if (!mipgap.second) {
256 // Compute absolute gap
257 factor = storm::utility::abs(glp_mip_obj_val(glp_ios_get_prob(t))) + DBL_EPSILON;
258 assert(factor >= 0.0);
259 }
260 if (actualRelativeGap * factor <= mipgap.first) {
261 // Terminate early
262 mipgap.first = actualRelativeGap;
263 mipgap.second = true; // The gap is relative.
264 glp_ios_terminate(t);
265 }
266}
267#endif
268
269template<typename ValueType, bool RawMode>
271#ifdef STORM_HAVE_GLPK
272 // First, reset the flags.
273 this->isInfeasibleFlag = false;
274 this->isUnboundedFlag = false;
275
276 // Start by setting the model sense.
277 glp_set_obj_dir(this->lp, this->getOptimizationDirection() == OptimizationDirection::Minimize ? GLP_MIN : GLP_MAX);
278
279 int error = 0;
280 if (this->modelContainsIntegerVariables) {
281 glp_iocp* parameters = new glp_iocp();
282 glp_init_iocp(parameters);
283 parameters->tol_int = storm::settings::getModule<storm::settings::modules::GlpkSettings>().getIntegerTolerance();
284 this->isInfeasibleFlag = false;
286 parameters->presolve = GLP_ON;
287 } else {
288 // Without presolving, we solve the relaxed model first. This is required because
289 // glp_intopt requires that either presolving is enabled or an optimal initial basis is provided.
290 error = glp_simplex(this->lp, nullptr);
291 STORM_LOG_THROW(error == 0, storm::exceptions::InvalidStateException, "Unable to optimize relaxed glpk model (" << error << ").");
292 // If the relaxed model is already not feasible, we don't have to solve the actual model.
293 if (glp_get_status(this->lp) == GLP_INFEAS || glp_get_status(this->lp) == GLP_NOFEAS) {
294 this->isInfeasibleFlag = true;
295 }
296 // If the relaxed model is unbounded, there could still be no feasible integer solution.
297 // However, since we can not provide an optimal initial basis, we will need to enable presolving
298 if (glp_get_status(this->lp) == GLP_UNBND) {
299 parameters->presolve = GLP_ON;
300 } else {
301 parameters->presolve = GLP_OFF;
302 }
303 }
304 if (!this->isInfeasibleFlag) {
305 // Check whether we allow sub-optimal solutions via a non-zero MIP gap.
306 // parameters->mip_gap = this->maxMILPGap; (only works for relative values. Also, we need to obtain the actual gap anyway.
307 std::pair<double, bool> mipgap(this->maxMILPGap, this->maxMILPGapRelative);
308 if (!storm::utility::isZero(this->maxMILPGap)) {
309 parameters->cb_func = &callback;
310 parameters->cb_info = &mipgap;
311 }
312
313 // Invoke mip solving
314 error = glp_intopt(this->lp, parameters);
315 int status = glp_mip_status(this->lp);
316 delete parameters;
317
318 // mipgap.first has been set to the achieved mipgap (either within the callback function or because it has been set to this->maxMILPGap)
319 this->actualRelativeMILPGap = mipgap.first;
320
321 // In case the error is caused by an infeasible problem, we do not want to view this as an error and
322 // reset the error code.
323 if (error == GLP_ENOPFS || status == GLP_NOFEAS) {
324 this->isInfeasibleFlag = true;
325 error = 0;
326 } else if (error == GLP_ENODFS) {
327 this->isUnboundedFlag = true;
328 error = 0;
329 } else if (error == GLP_ESTOP) {
330 // Early termination due to achieved MIP Gap. That's fine.
331 error = 0;
332 } else if (error == GLP_EBOUND) {
333 throw storm::exceptions::InvalidStateException()
334 << "The bounds of some variables are illegal. Note that glpk only accepts integer bounds for integer variables.";
335 }
336 }
337 } else {
338 error = glp_simplex(this->lp, nullptr);
339 }
340
341 STORM_LOG_THROW(error == 0, storm::exceptions::InvalidStateException, "Unable to optimize glpk model (" << error << ").");
342 this->currentModelHasBeenOptimized = true;
343#else
344 throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for GLPK. Yet, a method was called that "
345 "requires this support. Please choose a version with GLPK support.";
346#endif
347}
348
349template<typename ValueType, bool RawMode>
351#ifdef STORM_HAVE_GLPK
352 if (!this->currentModelHasBeenOptimized) {
353 throw storm::exceptions::InvalidStateException() << "Illegal call to GlpkLpSolver::isInfeasible: model has not been optimized.";
354 }
355
356 if (this->modelContainsIntegerVariables) {
357 return isInfeasibleFlag;
358 } else {
359 return glp_get_status(this->lp) == GLP_INFEAS || glp_get_status(this->lp) == GLP_NOFEAS;
360 }
361#else
362 throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for GLPK. Yet, a method was called that "
363 "requires this support. Please choose a version with GLPK support.";
364#endif
365}
366
367template<typename ValueType, bool RawMode>
369#ifdef STORM_HAVE_GLPK
370 if (!this->currentModelHasBeenOptimized) {
371 throw storm::exceptions::InvalidStateException() << "Illegal call to GlpkLpSolver::isUnbounded: model has not been optimized.";
372 }
373
374 if (this->modelContainsIntegerVariables) {
375 return isUnboundedFlag;
376 } else {
377 return glp_get_status(this->lp) == GLP_UNBND;
378 }
379#else
380 throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for GLPK. Yet, a method was called that "
381 "requires this support. Please choose a version with GLPK support.";
382#endif
383}
384
385template<typename ValueType, bool RawMode>
387 if (!this->currentModelHasBeenOptimized) {
388 return false;
389 }
390
391 return !isInfeasible() && !isUnbounded();
392}
393
394template<typename ValueType, bool RawMode>
396#ifdef STORM_HAVE_GLPK
397 if (!this->isOptimal()) {
398 STORM_LOG_THROW(!this->isInfeasible(), storm::exceptions::InvalidAccessException, "Unable to get glpk solution from infeasible model.");
399 STORM_LOG_THROW(!this->isUnbounded(), storm::exceptions::InvalidAccessException, "Unable to get glpk solution from unbounded model.");
400 STORM_LOG_THROW(false, storm::exceptions::InvalidAccessException, "Unable to get glpk solution from unoptimized model.");
401 }
402
403 int variableIndex = variableToIndexMap.at(variable);
404
405 double value = 0;
406 if (this->modelContainsIntegerVariables) {
407 value = glp_mip_col_val(this->lp, static_cast<int>(variableIndex));
408 } else {
409 value = glp_get_col_prim(this->lp, static_cast<int>(variableIndex));
410 }
411 return storm::utility::convertNumber<ValueType>(value);
412#else
413 throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for GLPK. Yet, a method was called that "
414 "requires this support. Please choose a version with GLPK support.";
415#endif
416}
417
418template<typename ValueType, bool RawMode>
420#ifdef STORM_HAVE_GLPK
421 if (!this->isOptimal()) {
422 STORM_LOG_THROW(!this->isInfeasible(), storm::exceptions::InvalidAccessException, "Unable to get glpk solution from infeasible model.");
423 STORM_LOG_THROW(!this->isUnbounded(), storm::exceptions::InvalidAccessException, "Unable to get glpk solution from unbounded model.");
424 STORM_LOG_THROW(false, storm::exceptions::InvalidAccessException, "Unable to get glpk solution from unoptimized model.");
425 }
426
427 int variableIndex = variableToIndexMap.at(variable);
428
429 double value = 0;
430 if (this->modelContainsIntegerVariables) {
431 value = glp_mip_col_val(this->lp, variableIndex);
432 } else {
433 value = glp_get_col_prim(this->lp, variableIndex);
434 }
435
436 double roundedValue = std::round(value);
437 double diff = std::abs(roundedValue - value);
439 "Illegal value for integer variable in GLPK solution (" << value << "). Difference to nearest int is " << diff);
440 return static_cast<int_fast64_t>(roundedValue);
441#else
442 throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for GLPK. Yet, a method was called that "
443 "requires this support. Please choose a version with GLPK support.";
444#endif
445}
446
447template<typename ValueType, bool RawMode>
449#ifdef STORM_HAVE_GLPK
450 if (!this->isOptimal()) {
451 STORM_LOG_THROW(!this->isInfeasible(), storm::exceptions::InvalidAccessException, "Unable to get glpk solution from infeasible model.");
452 STORM_LOG_THROW(!this->isUnbounded(), storm::exceptions::InvalidAccessException, "Unable to get glpk solution from unbounded model.");
453 STORM_LOG_THROW(false, storm::exceptions::InvalidAccessException, "Unable to get glpk solution from unoptimized model.");
454 }
455
456 int variableIndex = variableToIndexMap.at(variable);
457
458 double value = 0;
459 if (this->modelContainsIntegerVariables) {
460 value = glp_mip_col_val(this->lp, variableIndex);
461 } else {
462 value = glp_get_col_prim(this->lp, variableIndex);
463 }
464
465 if (value > 0.5) {
467 "Illegal value for binary variable in GLPK solution (" << value << ").");
468 return true;
469 } else {
471 "Illegal value for binary variable in GLPK solution (" << value << ").");
472 return false;
473 }
474
475 return static_cast<bool>(value);
476#else
477 throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for GLPK. Yet, a method was called that "
478 "requires this support. Please choose a version with GLPK support.";
479#endif
480}
481
482template<typename ValueType, bool RawMode>
484#ifdef STORM_HAVE_GLPK
485 if (!this->isOptimal()) {
486 STORM_LOG_THROW(!this->isInfeasible(), storm::exceptions::InvalidAccessException, "Unable to get glpk solution from infeasible model.");
487 STORM_LOG_THROW(!this->isUnbounded(), storm::exceptions::InvalidAccessException, "Unable to get glpk solution from unbounded model.");
488 STORM_LOG_THROW(false, storm::exceptions::InvalidAccessException, "Unable to get glpk solution from unoptimized model.");
489 }
490
491 double value = 0;
492 if (this->modelContainsIntegerVariables) {
493 value = glp_mip_obj_val(this->lp);
494 } else {
495 value = glp_get_obj_val(this->lp);
496 }
497
498 return storm::utility::convertNumber<ValueType>(value);
499#else
500 throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for GLPK. Yet, a method was called that "
501 "requires this support. Please choose a version with GLPK support.";
502#endif
503}
504
505template<typename ValueType, bool RawMode>
506void GlpkLpSolver<ValueType, RawMode>::writeModelToFile(std::string const& filename) const {
507#ifdef STORM_HAVE_GLPK
508 glp_write_lp(this->lp, 0, filename.c_str());
509#else
510 throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for GLPK. Yet, a method was called that "
511 "requires this support. Please choose a version with GLPK support.";
512#endif
513}
514
515template<typename ValueType, bool RawMode>
517#ifdef STORM_HAVE_GLPK
518 if constexpr (RawMode) {
519 STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Incremental LP solving not supported in raw mode");
520 } else {
521 IncrementalLevel lvl;
522 lvl.firstConstraintIndex = glp_get_num_rows(this->lp) + 1;
523 incrementalData.push_back(lvl);
524 }
525#else
526 throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for GLPK. Yet, a method was called that "
527 "requires this support. Please choose a version with GLPK support.";
528#endif
529}
530
531template<typename ValueType, bool RawMode>
533#ifdef STORM_HAVE_GLPK
534 if constexpr (RawMode) {
535 STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Incremental LP solving not supported in raw mode");
536 } else {
537 if (incrementalData.empty()) {
538 STORM_LOG_ERROR("Tried to pop from a solver without pushing before.");
539 } else {
540 IncrementalLevel const& lvl = incrementalData.back();
541 // Since glpk uses 1-based indexing, we need to prepend an additional index
542 std::vector<int> indicesToBeRemoved = storm::utility::vector::buildVectorForRange(lvl.firstConstraintIndex - 1, glp_get_num_rows(this->lp) + 1);
543 if (indicesToBeRemoved.size() > 1) {
544 glp_del_rows(this->lp, indicesToBeRemoved.size() - 1, indicesToBeRemoved.data());
545 }
546 indicesToBeRemoved.clear();
547
548 if (!lvl.variables.empty()) {
549 int firstIndex = -1;
550 bool first = true;
551 for (auto const& var : lvl.variables) {
552 if (first) {
553 auto it = variableToIndexMap.find(var);
554 firstIndex = it->second;
555 variableToIndexMap.erase(it);
556 first = false;
557 } else {
558 variableToIndexMap.erase(var);
559 }
560 }
561 // Since glpk uses 1-based indexing, we need to prepend an additional index
562 std::vector<int> indicesToBeRemoved = storm::utility::vector::buildVectorForRange(firstIndex - 1, glp_get_num_cols(this->lp) + 1);
563 glp_del_cols(this->lp, indicesToBeRemoved.size() - 1, indicesToBeRemoved.data());
564 }
565 incrementalData.pop_back();
566 update();
567 // Check whether we need to adapt the current basis (i.e. the number of basic variables does not equal the number of constraints)
568 int n = glp_get_num_rows(lp);
569 int m = glp_get_num_cols(lp);
570 int nb(0), mb(0);
571 for (int i = 1; i <= n; ++i) {
572 if (glp_get_row_stat(lp, i) == GLP_BS) {
573 ++nb;
574 }
575 }
576 for (int j = 1; j <= m; ++j) {
577 if (glp_get_col_stat(lp, j) == GLP_BS) {
578 ++mb;
579 }
580 }
581 if (n != (nb + mb)) {
582 glp_std_basis(this->lp);
583 }
584 }
585 }
586#else
587 throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for GLPK. Yet, a method was called that "
588 "requires this support. Please choose a version with GLPK support.";
589#endif
590}
591
592template<typename ValueType, bool RawMode>
593void GlpkLpSolver<ValueType, RawMode>::setMaximalMILPGap(ValueType const& gap, bool relative) {
594 this->maxMILPGap = storm::utility::convertNumber<double>(gap);
595 this->maxMILPGapRelative = relative;
596}
597
598template<typename ValueType, bool RawMode>
599ValueType GlpkLpSolver<ValueType, RawMode>::getMILPGap(bool relative) const {
600 STORM_LOG_ASSERT(this->isOptimal(), "Asked for the MILP gap although there is no (bounded) solution.");
601 if (relative) {
602 return storm::utility::convertNumber<ValueType>(this->actualRelativeMILPGap);
603 } else {
604 return storm::utility::abs<ValueType>(storm::utility::convertNumber<ValueType>(this->actualRelativeMILPGap) * getObjectiveValue());
605 }
606}
607
608template class GlpkLpSolver<double, true>;
609template class GlpkLpSolver<double, false>;
612
613} // namespace solver
614} // namespace storm
VariableCoefficients getLinearCoefficients(Expression const &expression)
Computes the (double) coefficients of all identifiers appearing in the expression if the expression w...
A class that implements the LpSolver interface using glpk as the background solver.
virtual bool getBinaryValue(Variable const &name) const override
Retrieves the value of the binary variable with the given name.
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.
virtual ValueType getContinuousValue(Variable const &name) const override
Retrieves the value of the continuous variable with the given name.
virtual int_fast64_t getIntegerValue(Variable const &name) const override
Retrieves the value of the integer variable with the given name.
GlpkLpSolver()
Constructs a solver without a name.
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.
virtual bool isOptimal() const override
Retrieves whether the model was found to be optimal, i.e.
virtual void writeModelToFile(std::string const &filename) const override
Writes the current LP problem to the given file.
virtual bool isInfeasible() const override
Retrieves whether the model was found to be infeasible.
virtual void pop() override
Pops a backtracking point from the solver's stack.
typename LpSolver< ValueType, RawMode >::Constraint Constraint
virtual ValueType getObjectiveValue() const override
Retrieves the value of the objective function.
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 void update() const override
Updates the model to make the variables that have been declared since the last call to update usable.
virtual ValueType getMILPGap(bool relative) const override
Returns the obtained gap after a call to optimize()
virtual ~GlpkLpSolver()
Destructs a solver by freeing the pointers to glpk's structures.
typename LpSolver< ValueType, RawMode >::VariableType VariableType
virtual bool isUnbounded() const override
Retrieves whether the model was found to be infeasible.
virtual void optimize() const override
Optimizes the LP problem previously constructed.
typename LpSolver< ValueType, RawMode >::Variable Variable
#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.
int getGlpkType(typename GlpkLpSolver< ValueType, RawMode >::VariableType const &type)
std::vector< T > buildVectorForRange(T min, T max)
Constructs a vector [min, min+1, ...., max-1].
Definition vector.h:134
bool isZero(ValueType const &a)
Definition constants.cpp:41
ValueType abs(ValueType const &number)
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