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
58template<typename ValueType, bool RawMode>
59GlpkLpSolver<ValueType, RawMode>::GlpkLpSolver(std::string const& name) : GlpkLpSolver(name, OptimizationDirection::Minimize) {
60 // Intentionally left empty.
61}
62
63template<typename ValueType, bool RawMode>
64GlpkLpSolver<ValueType, RawMode>::GlpkLpSolver() : GlpkLpSolver("", OptimizationDirection::Minimize) {
65 // Intentionally left empty.
66}
67
68template<typename ValueType, bool RawMode>
69GlpkLpSolver<ValueType, RawMode>::GlpkLpSolver(OptimizationDirection const& optDir) : GlpkLpSolver("", optDir) {
70 // Intentionally left empty.
71}
72
73template<typename ValueType, bool RawMode>
74GlpkLpSolver<ValueType, RawMode>::~GlpkLpSolver() {
75 // Dispose of all objects allocated dynamically by glpk.
76 glp_delete_prob(this->lp);
77 glp_free_env();
78}
79
80template<typename ValueType, bool RawMode>
81int getGlpkType(typename GlpkLpSolver<ValueType, RawMode>::VariableType const& type) {
82 switch (type) {
83 case GlpkLpSolver<ValueType, RawMode>::VariableType::Continuous:
84 return GLP_CV;
85 case GlpkLpSolver<ValueType, RawMode>::VariableType::Integer:
86 return GLP_IV;
87 case GlpkLpSolver<ValueType, RawMode>::VariableType::Binary:
88 return GLP_BV;
89 }
90 STORM_LOG_ASSERT(false, "Unexpected variable type.");
91 return -1;
92}
93
94template<typename ValueType, bool RawMode>
95typename GlpkLpSolver<ValueType, RawMode>::Variable GlpkLpSolver<ValueType, RawMode>::addVariable(std::string const& name, VariableType const& type,
96 std::optional<ValueType> const& lowerBound,
97 std::optional<ValueType> const& upperBound,
98 ValueType objectiveFunctionCoefficient) {
99 Variable resultVar;
100 if constexpr (RawMode) {
101 resultVar = variableToIndexMap.size();
102 } else {
103 resultVar = this->declareOrGetExpressionVariable(name, type);
104 // Assert whether the variable does not exist yet.
105 // Due to incremental usage (push(), pop()), a variable might be declared in the manager but not in the lp model.
106 STORM_LOG_ASSERT(variableToIndexMap.count(resultVar) == 0, "Variable " << resultVar.getName() << " exists already in the model.");
107 }
108
109 int boundType;
110 if (lowerBound.has_value()) {
111 boundType = upperBound.has_value() ? GLP_DB : GLP_LO;
112 } else {
113 boundType = upperBound.has_value() ? GLP_UP : GLP_FR;
114 }
115
116 if (type == VariableType::Integer || type == VariableType::Binary) {
117 this->modelContainsIntegerVariables = true;
118 }
119
120 // Create the variable in glpk.
121 int variableIndex = glp_add_cols(this->lp, 1);
122 glp_set_col_name(this->lp, variableIndex, name.c_str());
123 glp_set_col_bnds(lp, variableIndex, boundType, lowerBound.has_value() ? storm::utility::convertNumber<double>(*lowerBound) : 0.0,
124 upperBound.has_value() ? storm::utility::convertNumber<double>(*upperBound) : 0.0);
125 glp_set_col_kind(this->lp, variableIndex, getGlpkType<ValueType, RawMode>(type));
126 glp_set_obj_coef(this->lp, variableIndex, storm::utility::convertNumber<double>(objectiveFunctionCoefficient));
127
128 if constexpr (RawMode) {
129 this->variableToIndexMap.push_back(variableIndex);
130 } else {
131 this->variableToIndexMap.emplace(resultVar, variableIndex);
132 if (!incrementalData.empty()) {
133 incrementalData.back().variables.push_back(resultVar);
134 }
135 }
136
137 return resultVar;
138}
139
140template<typename ValueType, bool RawMode>
141void GlpkLpSolver<ValueType, RawMode>::update() const {
142 // Intentionally left empty.
143}
144
145template<typename ValueType, bool RawMode>
146void GlpkLpSolver<ValueType, RawMode>::addConstraint(std::string const& name, Constraint const& constraint) {
147 // Add the row that will represent this constraint.
148 int constraintIndex = glp_add_rows(this->lp, 1);
149 glp_set_row_name(this->lp, constraintIndex, name.c_str());
150
151 // Extract constraint data
152 double rhs;
154 // glpk uses 1-based indexing (wtf!?)...
155 std::vector<int> variableIndices(1, -1);
156 std::vector<double> coefficients(1, 0.0);
157 if constexpr (RawMode) {
158 rhs = storm::utility::convertNumber<double>(constraint.rhs);
159 relationType = constraint.relationType;
160 variableIndices.reserve(constraint.lhsVariableIndices.size() + 1);
161 for (auto const& var : constraint.lhsVariableIndices) {
162 variableIndices.push_back(this->variableToIndexMap.at(var));
163 }
164 coefficients.reserve(constraint.lhsCoefficients.size() + 1);
165 for (auto const& coef : constraint.lhsCoefficients) {
166 coefficients.push_back(storm::utility::convertNumber<double>(coef));
167 }
168 } else {
169 STORM_LOG_THROW(constraint.getManager() == this->getManager(), storm::exceptions::InvalidArgumentException,
170 "Constraint was not built over the proper variables.");
171 STORM_LOG_THROW(constraint.isRelationalExpression(), storm::exceptions::InvalidArgumentException, "Illegal constraint is not a relational expression.");
172
177 leftCoefficients.separateVariablesFromConstantPart(rightCoefficients);
178 rhs = rightCoefficients.getConstantPart();
179 relationType = constraint.getBaseExpression().asBinaryRelationExpression().getRelationType();
180 int len = std::distance(leftCoefficients.begin(), leftCoefficients.end());
181 variableIndices.reserve(len + 1);
182 coefficients.reserve(len + 1);
183 for (auto const& variableCoefficientPair : leftCoefficients) {
184 auto variableIndexPair = this->variableToIndexMap.find(variableCoefficientPair.first);
185 variableIndices.push_back(variableIndexPair->second);
186 coefficients.push_back(variableCoefficientPair.second);
187 }
188 }
189
190 // Determine the type of the constraint and add it properly.
191 switch (relationType) {
193 glp_set_row_bnds(this->lp, constraintIndex, GLP_UP, 0,
195 break;
197 glp_set_row_bnds(this->lp, constraintIndex, GLP_UP, 0, rhs);
198 break;
200 glp_set_row_bnds(this->lp, constraintIndex, GLP_LO,
202 break;
204 glp_set_row_bnds(this->lp, constraintIndex, GLP_LO, rhs, 0);
205 break;
207 glp_set_row_bnds(this->lp, constraintIndex, GLP_FX, rhs, rhs);
208 break;
209 default:
210 STORM_LOG_ASSERT(false, "Illegal operator in LP solver constraint.");
211 }
212
213 // Add the constraints
214 glp_set_mat_row(this->lp, constraintIndex, variableIndices.size() - 1, variableIndices.data(), coefficients.data());
215
216 this->currentModelHasBeenOptimized = false;
217}
218
219template<typename ValueType, bool RawMode>
220void GlpkLpSolver<ValueType, RawMode>::addIndicatorConstraint(std::string const&, Variable, bool, Constraint const&) {
221 STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Indicator Constraints not supported for SoPlex.");
222}
223
224// Method used within the MIP solver to terminate early
225void callback(glp_tree* t, void* info) {
226 auto& mipgap = *static_cast<std::pair<double, bool>*>(info);
227 double actualRelativeGap = glp_ios_mip_gap(t);
228 double factor = storm::utility::one<double>();
229 if (!mipgap.second) {
230 // Compute absolute gap
231 factor = storm::utility::abs(glp_mip_obj_val(glp_ios_get_prob(t))) + DBL_EPSILON;
232 assert(factor >= 0.0);
233 }
234 if (actualRelativeGap * factor <= mipgap.first) {
235 // Terminate early
236 mipgap.first = actualRelativeGap;
237 mipgap.second = true; // The gap is relative.
238 glp_ios_terminate(t);
239 }
240}
241
242template<typename ValueType, bool RawMode>
243void GlpkLpSolver<ValueType, RawMode>::optimize() const {
244 // First, reset the flags.
245 this->isInfeasibleFlag = false;
246 this->isUnboundedFlag = false;
247
248 // Start by setting the model sense.
249 glp_set_obj_dir(this->lp, this->getOptimizationDirection() == OptimizationDirection::Minimize ? GLP_MIN : GLP_MAX);
250
251 int error = 0;
252 if (this->modelContainsIntegerVariables) {
253 glp_iocp* parameters = new glp_iocp();
254 glp_init_iocp(parameters);
255 parameters->tol_int = storm::settings::getModule<storm::settings::modules::GlpkSettings>().getIntegerTolerance();
256 this->isInfeasibleFlag = false;
258 parameters->presolve = GLP_ON;
259 } else {
260 // Without presolving, we solve the relaxed model first. This is required because
261 // glp_intopt requires that either presolving is enabled or an optimal initial basis is provided.
262 error = glp_simplex(this->lp, nullptr);
263 STORM_LOG_THROW(error == 0, storm::exceptions::InvalidStateException, "Unable to optimize relaxed glpk model (" << error << ").");
264 // If the relaxed model is already not feasible, we don't have to solve the actual model.
265 if (glp_get_status(this->lp) == GLP_INFEAS || glp_get_status(this->lp) == GLP_NOFEAS) {
266 this->isInfeasibleFlag = true;
267 }
268 // If the relaxed model is unbounded, there could still be no feasible integer solution.
269 // However, since we can not provide an optimal initial basis, we will need to enable presolving
270 if (glp_get_status(this->lp) == GLP_UNBND) {
271 parameters->presolve = GLP_ON;
272 } else {
273 parameters->presolve = GLP_OFF;
274 }
275 }
276 if (!this->isInfeasibleFlag) {
277 // Check whether we allow sub-optimal solutions via a non-zero MIP gap.
278 // parameters->mip_gap = this->maxMILPGap; (only works for relative values. Also, we need to obtain the actual gap anyway.
279 std::pair<double, bool> mipgap(this->maxMILPGap, this->maxMILPGapRelative);
280 if (!storm::utility::isZero(this->maxMILPGap)) {
281 parameters->cb_func = &callback;
282 parameters->cb_info = &mipgap;
283 }
284
285 // Invoke mip solving
286 error = glp_intopt(this->lp, parameters);
287 int status = glp_mip_status(this->lp);
288 delete parameters;
289
290 // mipgap.first has been set to the achieved mipgap (either within the callback function or because it has been set to this->maxMILPGap)
291 this->actualRelativeMILPGap = mipgap.first;
292
293 // In case the error is caused by an infeasible problem, we do not want to view this as an error and
294 // reset the error code.
295 if (error == GLP_ENOPFS || status == GLP_NOFEAS) {
296 this->isInfeasibleFlag = true;
297 error = 0;
298 } else if (error == GLP_ENODFS) {
299 this->isUnboundedFlag = true;
300 error = 0;
301 } else if (error == GLP_ESTOP) {
302 // Early termination due to achieved MIP Gap. That's fine.
303 error = 0;
304 } else if (error == GLP_EBOUND) {
305 throw storm::exceptions::InvalidStateException()
306 << "The bounds of some variables are illegal. Note that glpk only accepts integer bounds for integer variables.";
307 }
308 }
309 } else {
310 error = glp_simplex(this->lp, nullptr);
311 }
312
313 STORM_LOG_THROW(error == 0, storm::exceptions::InvalidStateException, "Unable to optimize glpk model (" << error << ").");
314 this->currentModelHasBeenOptimized = true;
315}
316
317template<typename ValueType, bool RawMode>
318bool GlpkLpSolver<ValueType, RawMode>::isInfeasible() const {
319 if (!this->currentModelHasBeenOptimized) {
320 throw storm::exceptions::InvalidStateException() << "Illegal call to GlpkLpSolver::isInfeasible: model has not been optimized.";
321 }
322
323 if (this->modelContainsIntegerVariables) {
324 return isInfeasibleFlag;
325 } else {
326 return glp_get_status(this->lp) == GLP_INFEAS || glp_get_status(this->lp) == GLP_NOFEAS;
327 }
328}
329
330template<typename ValueType, bool RawMode>
331bool GlpkLpSolver<ValueType, RawMode>::isUnbounded() const {
332 if (!this->currentModelHasBeenOptimized) {
333 throw storm::exceptions::InvalidStateException() << "Illegal call to GlpkLpSolver::isUnbounded: model has not been optimized.";
334 }
335
336 if (this->modelContainsIntegerVariables) {
337 return isUnboundedFlag;
338 } else {
339 return glp_get_status(this->lp) == GLP_UNBND;
340 }
341}
342
343template<typename ValueType, bool RawMode>
344bool GlpkLpSolver<ValueType, RawMode>::isOptimal() const {
345 if (!this->currentModelHasBeenOptimized) {
346 return false;
347 }
348
349 return !isInfeasible() && !isUnbounded();
350}
351
352template<typename ValueType, bool RawMode>
353ValueType GlpkLpSolver<ValueType, RawMode>::getContinuousValue(Variable const& variable) const {
354 if (!this->isOptimal()) {
355 STORM_LOG_THROW(!this->isInfeasible(), storm::exceptions::InvalidAccessException, "Unable to get glpk solution from infeasible model.");
356 STORM_LOG_THROW(!this->isUnbounded(), storm::exceptions::InvalidAccessException, "Unable to get glpk solution from unbounded model.");
357 STORM_LOG_THROW(false, storm::exceptions::InvalidAccessException, "Unable to get glpk solution from unoptimized model.");
358 }
359
360 int variableIndex = variableToIndexMap.at(variable);
361
362 double value = 0;
363 if (this->modelContainsIntegerVariables) {
364 value = glp_mip_col_val(this->lp, static_cast<int>(variableIndex));
365 } else {
366 value = glp_get_col_prim(this->lp, static_cast<int>(variableIndex));
367 }
368 return storm::utility::convertNumber<ValueType>(value);
369}
370
371template<typename ValueType, bool RawMode>
372int_fast64_t GlpkLpSolver<ValueType, RawMode>::getIntegerValue(Variable const& variable) const {
373 if (!this->isOptimal()) {
374 STORM_LOG_THROW(!this->isInfeasible(), storm::exceptions::InvalidAccessException, "Unable to get glpk solution from infeasible model.");
375 STORM_LOG_THROW(!this->isUnbounded(), storm::exceptions::InvalidAccessException, "Unable to get glpk solution from unbounded model.");
376 STORM_LOG_THROW(false, storm::exceptions::InvalidAccessException, "Unable to get glpk solution from unoptimized model.");
377 }
378
379 int variableIndex = variableToIndexMap.at(variable);
380
381 double value = 0;
382 if (this->modelContainsIntegerVariables) {
383 value = glp_mip_col_val(this->lp, variableIndex);
384 } else {
385 value = glp_get_col_prim(this->lp, variableIndex);
386 }
387
388 double roundedValue = std::round(value);
389 double diff = std::abs(roundedValue - value);
391 "Illegal value for integer variable in GLPK solution (" << value << "). Difference to nearest int is " << diff);
392 return static_cast<int_fast64_t>(roundedValue);
393}
394
395template<typename ValueType, bool RawMode>
396bool GlpkLpSolver<ValueType, RawMode>::getBinaryValue(Variable const& variable) const {
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, variableIndex);
408 } else {
409 value = glp_get_col_prim(this->lp, variableIndex);
410 }
411
412 if (value > 0.5) {
414 "Illegal value for binary variable in GLPK solution (" << value << ").");
415 return true;
416 } else {
418 "Illegal value for binary variable in GLPK solution (" << value << ").");
419 return false;
420 }
421
422 return static_cast<bool>(value);
423}
424
425template<typename ValueType, bool RawMode>
426ValueType GlpkLpSolver<ValueType, RawMode>::getObjectiveValue() const {
427 if (!this->isOptimal()) {
428 STORM_LOG_THROW(!this->isInfeasible(), storm::exceptions::InvalidAccessException, "Unable to get glpk solution from infeasible model.");
429 STORM_LOG_THROW(!this->isUnbounded(), storm::exceptions::InvalidAccessException, "Unable to get glpk solution from unbounded model.");
430 STORM_LOG_THROW(false, storm::exceptions::InvalidAccessException, "Unable to get glpk solution from unoptimized model.");
431 }
432
433 double value = 0;
434 if (this->modelContainsIntegerVariables) {
435 value = glp_mip_obj_val(this->lp);
436 } else {
437 value = glp_get_obj_val(this->lp);
438 }
439
440 return storm::utility::convertNumber<ValueType>(value);
441}
442
443template<typename ValueType, bool RawMode>
444void GlpkLpSolver<ValueType, RawMode>::writeModelToFile(std::string const& filename) const {
445 glp_write_lp(this->lp, 0, filename.c_str());
446}
447
448template<typename ValueType, bool RawMode>
449void GlpkLpSolver<ValueType, RawMode>::push() {
450 if constexpr (RawMode) {
451 STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Incremental LP solving not supported in raw mode");
452 } else {
453 IncrementalLevel lvl;
454 lvl.firstConstraintIndex = glp_get_num_rows(this->lp) + 1;
455 incrementalData.push_back(lvl);
456 }
457}
458
459template<typename ValueType, bool RawMode>
460void GlpkLpSolver<ValueType, RawMode>::pop() {
461 if constexpr (RawMode) {
462 STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Incremental LP solving not supported in raw mode");
463 } else {
464 if (incrementalData.empty()) {
465 STORM_LOG_ERROR("Tried to pop from a solver without pushing before.");
466 } else {
467 IncrementalLevel const& lvl = incrementalData.back();
468 // Since glpk uses 1-based indexing, we need to prepend an additional index
469 std::vector<int> indicesToBeRemoved = storm::utility::vector::buildVectorForRange(lvl.firstConstraintIndex - 1, glp_get_num_rows(this->lp) + 1);
470 if (indicesToBeRemoved.size() > 1) {
471 glp_del_rows(this->lp, indicesToBeRemoved.size() - 1, indicesToBeRemoved.data());
472 }
473 indicesToBeRemoved.clear();
474
475 if (!lvl.variables.empty()) {
476 int firstIndex = -1;
477 bool first = true;
478 for (auto const& var : lvl.variables) {
479 if (first) {
480 auto it = variableToIndexMap.find(var);
481 firstIndex = it->second;
482 variableToIndexMap.erase(it);
483 first = false;
484 } else {
485 variableToIndexMap.erase(var);
486 }
487 }
488 // Since glpk uses 1-based indexing, we need to prepend an additional index
489 std::vector<int> indicesToBeRemoved = storm::utility::vector::buildVectorForRange(firstIndex - 1, glp_get_num_cols(this->lp) + 1);
490 glp_del_cols(this->lp, indicesToBeRemoved.size() - 1, indicesToBeRemoved.data());
491 }
492 incrementalData.pop_back();
493 update();
494 // Check whether we need to adapt the current basis (i.e. the number of basic variables does not equal the number of constraints)
495 int n = glp_get_num_rows(lp);
496 int m = glp_get_num_cols(lp);
497 int nb(0), mb(0);
498 for (int i = 1; i <= n; ++i) {
499 if (glp_get_row_stat(lp, i) == GLP_BS) {
500 ++nb;
501 }
502 }
503 for (int j = 1; j <= m; ++j) {
504 if (glp_get_col_stat(lp, j) == GLP_BS) {
505 ++mb;
506 }
507 }
508 if (n != (nb + mb)) {
509 glp_std_basis(this->lp);
510 }
511 }
512 }
513}
514
515template<typename ValueType, bool RawMode>
516void GlpkLpSolver<ValueType, RawMode>::setMaximalMILPGap(ValueType const& gap, bool relative) {
517 this->maxMILPGap = storm::utility::convertNumber<double>(gap);
518 this->maxMILPGapRelative = relative;
519}
520
521template<typename ValueType, bool RawMode>
522ValueType GlpkLpSolver<ValueType, RawMode>::getMILPGap(bool relative) const {
523 STORM_LOG_ASSERT(this->isOptimal(), "Asked for the MILP gap although there is no (bounded) solution.");
524 if (relative) {
525 return storm::utility::convertNumber<ValueType>(this->actualRelativeMILPGap);
526 } else {
527 return storm::utility::abs<ValueType>(storm::utility::convertNumber<ValueType>(this->actualRelativeMILPGap) * getObjectiveValue());
528 }
529}
530
531template class GlpkLpSolver<double, true>;
532template class GlpkLpSolver<double, false>;
533template class GlpkLpSolver<storm::RationalNumber, true>;
534template class GlpkLpSolver<storm::RationalNumber, false>;
535#endif
536} // namespace solver
537} // namespace storm
VariableCoefficients getLinearCoefficients(Expression const &expression)
Computes the (double) coefficients of all identifiers appearing in the expression if the expression w...
#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::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)
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