23template<
typename ValueType,
bool RawMode>
29 modelContainsIntegerVariables(false),
30 integerTolerance(glpkSettings.getIntegerTolerance()),
31 milpPresolverEnabled(glpkSettings.isMILPPresolverEnabled()),
32 isInfeasibleFlag(false),
33 isUnboundedFlag(false) {
35 lp = glp_create_prob();
38 glp_set_prob_name(lp, name.c_str());
41 glp_term_out(debug || glpkSettings.
isOutputSet() ? GLP_ON : GLP_OFF);
44 glp_iocp* defaultParameters =
new glp_iocp();
45 glp_init_iocp(defaultParameters);
46 this->maxMILPGap = defaultParameters->mip_gap;
47 this->maxMILPGapRelative =
true;
52template<
typename ValueType,
bool RawMode>
58template<
typename ValueType,
bool RawMode>
64template<
typename ValueType,
bool RawMode>
70template<
typename ValueType,
bool RawMode>
76template<
typename ValueType,
bool RawMode>
80 glp_delete_prob(this->lp);
85template<
typename ValueType,
bool RawMode>
100 "This version of storm was compiled without support for GLPK. Yet, a method was called that requires this support. Please choose a "
101 "version with GLPK support.");
105template<
typename ValueType,
bool RawMode>
107 std::optional<ValueType>
const& lowerBound,
108 std::optional<ValueType>
const& upperBound,
109 ValueType objectiveFunctionCoefficient) {
110#ifdef STORM_HAVE_GLPK
112 if constexpr (RawMode) {
113 resultVar = variableToIndexMap.size();
118 STORM_LOG_ASSERT(variableToIndexMap.count(resultVar) == 0,
"Variable " << resultVar.getName() <<
" exists already in the model.");
122 if (lowerBound.has_value()) {
123 boundType = upperBound.has_value() ? GLP_DB : GLP_LO;
125 boundType = upperBound.has_value() ? GLP_UP : GLP_FR;
128 if (type == VariableType::Integer || type == VariableType::Binary) {
129 this->modelContainsIntegerVariables =
true;
133 int variableIndex = glp_add_cols(this->lp, 1);
134 glp_set_col_name(this->lp, variableIndex, name.c_str());
140 if constexpr (RawMode) {
141 this->variableToIndexMap.push_back(variableIndex);
143 this->variableToIndexMap.emplace(resultVar, variableIndex);
144 if (!incrementalData.empty()) {
145 incrementalData.back().variables.push_back(resultVar);
152 "This version of storm was compiled without support for GLPK. Yet, a method was called that requires this support. Please choose a "
153 "version with GLPK support.");
157template<
typename ValueType,
bool RawMode>
162template<
typename ValueType,
bool RawMode>
164#ifdef STORM_HAVE_GLPK
166 int constraintIndex = glp_add_rows(this->lp, 1);
167 glp_set_row_name(this->lp, constraintIndex, name.c_str());
173 std::vector<int> variableIndices(1, -1);
174 std::vector<double> coefficients(1, 0.0);
175 if constexpr (RawMode) {
177 relationType = constraint.relationType;
178 variableIndices.reserve(constraint.lhsVariableIndices.size() + 1);
179 for (
auto const& var : constraint.lhsVariableIndices) {
180 variableIndices.push_back(this->variableToIndexMap.at(var));
182 coefficients.reserve(constraint.lhsCoefficients.size() + 1);
183 for (
auto const& coef : constraint.lhsCoefficients) {
187 STORM_LOG_THROW(constraint.getManager() == this->getManager(), storm::exceptions::InvalidArgumentException,
188 "Constraint was not built over the proper variables.");
189 STORM_LOG_THROW(constraint.isRelationalExpression(), storm::exceptions::InvalidArgumentException,
"Illegal constraint is not a relational expression.");
197 relationType = constraint.getBaseExpression().asBinaryRelationExpression().getRelationType();
198 int len = std::distance(leftCoefficients.
begin(), leftCoefficients.
end());
199 variableIndices.reserve(len + 1);
200 coefficients.reserve(len + 1);
201 for (
auto const& variableCoefficientPair : leftCoefficients) {
202 auto variableIndexPair = this->variableToIndexMap.find(variableCoefficientPair.first);
203 variableIndices.push_back(variableIndexPair->second);
204 coefficients.push_back(variableCoefficientPair.second);
209 switch (relationType) {
211 glp_set_row_bnds(this->lp, constraintIndex, GLP_UP, 0, rhs - this->integerTolerance);
214 glp_set_row_bnds(this->lp, constraintIndex, GLP_UP, 0, rhs);
217 glp_set_row_bnds(this->lp, constraintIndex, GLP_LO, rhs + this->integerTolerance, 0);
220 glp_set_row_bnds(this->lp, constraintIndex, GLP_LO, rhs, 0);
223 glp_set_row_bnds(this->lp, constraintIndex, GLP_FX, rhs, rhs);
230 glp_set_mat_row(this->lp, constraintIndex, variableIndices.size() - 1, variableIndices.data(), coefficients.data());
235 "This version of storm was compiled without support for GLPK. Yet, a method was called that requires this support. Please choose a "
236 "version with GLPK support.");
240template<
typename ValueType,
bool RawMode>
242 STORM_LOG_THROW(
false, storm::exceptions::NotSupportedException,
"Indicator constraints are not supported for GLPK.");
245#ifdef STORM_HAVE_GLPK
247void callback(glp_tree* t,
void* info) {
248 auto& mipgap = *
static_cast<std::pair<double, bool>*
>(info);
249 double actualRelativeGap = glp_ios_mip_gap(t);
251 if (!mipgap.second) {
256 if (actualRelativeGap * factor <= mipgap.first) {
258 mipgap.first = actualRelativeGap;
259 mipgap.second =
true;
260 glp_ios_terminate(t);
265template<
typename ValueType,
bool RawMode>
267#ifdef STORM_HAVE_GLPK
269 this->isInfeasibleFlag =
false;
270 this->isUnboundedFlag =
false;
276 if (this->modelContainsIntegerVariables) {
277 glp_iocp* parameters =
new glp_iocp();
278 glp_init_iocp(parameters);
279 parameters->tol_int = this->integerTolerance;
280 this->isInfeasibleFlag =
false;
281 if (this->milpPresolverEnabled) {
282 parameters->presolve = GLP_ON;
286 error = glp_simplex(this->lp,
nullptr);
287 STORM_LOG_THROW(error == 0, storm::exceptions::InvalidStateException,
"Unable to optimize relaxed glpk model (" << error <<
").");
289 if (glp_get_status(this->lp) == GLP_INFEAS || glp_get_status(this->lp) == GLP_NOFEAS) {
290 this->isInfeasibleFlag =
true;
294 if (glp_get_status(this->lp) == GLP_UNBND) {
295 parameters->presolve = GLP_ON;
297 parameters->presolve = GLP_OFF;
300 if (!this->isInfeasibleFlag) {
303 std::pair<double, bool> mipgap(this->maxMILPGap, this->maxMILPGapRelative);
305 parameters->cb_func = &callback;
306 parameters->cb_info = &mipgap;
310 error = glp_intopt(this->lp, parameters);
311 int status = glp_mip_status(this->lp);
315 this->actualRelativeMILPGap = mipgap.first;
319 if (error == GLP_ENOPFS || status == GLP_NOFEAS) {
320 this->isInfeasibleFlag =
true;
322 }
else if (error == GLP_ENODFS) {
323 this->isUnboundedFlag =
true;
325 }
else if (error == GLP_ESTOP) {
328 }
else if (error == GLP_EBOUND) {
330 "The bounds of some variables are illegal. Note that glpk only accepts integer bounds for integer variables.");
334 error = glp_simplex(this->lp,
nullptr);
337 STORM_LOG_THROW(error == 0, storm::exceptions::InvalidStateException,
"Unable to optimize glpk model (" << error <<
").");
341 "This version of storm was compiled without support for GLPK. Yet, a method was called that requires this support. Please choose a "
342 "version with GLPK support.");
346template<
typename ValueType,
bool RawMode>
348#ifdef STORM_HAVE_GLPK
350 "Illegal call to GlpkLpSolver::isInfeasible: model has not been optimized.");
352 if (this->modelContainsIntegerVariables) {
353 return isInfeasibleFlag;
355 return glp_get_status(this->lp) == GLP_INFEAS || glp_get_status(this->lp) == GLP_NOFEAS;
359 "This version of storm was compiled without support for GLPK. Yet, a method was called that requires this support. Please choose a "
360 "version with GLPK support.");
364template<
typename ValueType,
bool RawMode>
366#ifdef STORM_HAVE_GLPK
368 "Illegal call to GlpkLpSolver::isUnbounded: model has not been optimized.");
370 if (this->modelContainsIntegerVariables) {
371 return isUnboundedFlag;
373 return glp_get_status(this->lp) == GLP_UNBND;
377 "This version of storm was compiled without support for GLPK. Yet, a method was called that requires this support. Please choose a "
378 "version with GLPK support.");
382template<
typename ValueType,
bool RawMode>
391template<
typename ValueType,
bool RawMode>
393#ifdef STORM_HAVE_GLPK
395 STORM_LOG_THROW(!this->
isInfeasible(), storm::exceptions::InvalidAccessException,
"Unable to get glpk solution from infeasible model.");
396 STORM_LOG_THROW(!this->
isUnbounded(), storm::exceptions::InvalidAccessException,
"Unable to get glpk solution from unbounded model.");
397 STORM_LOG_THROW(
false, storm::exceptions::InvalidAccessException,
"Unable to get glpk solution from unoptimized model.");
400 int variableIndex = variableToIndexMap.at(variable);
403 if (this->modelContainsIntegerVariables) {
404 value = glp_mip_col_val(this->lp,
static_cast<int>(variableIndex));
406 value = glp_get_col_prim(this->lp,
static_cast<int>(variableIndex));
411 "This version of storm was compiled without support for GLPK. Yet, a method was called that requires this support. Please choose a "
412 "version with GLPK support.");
416template<
typename ValueType,
bool RawMode>
418#ifdef STORM_HAVE_GLPK
420 STORM_LOG_THROW(!this->
isInfeasible(), storm::exceptions::InvalidAccessException,
"Unable to get glpk solution from infeasible model.");
421 STORM_LOG_THROW(!this->
isUnbounded(), storm::exceptions::InvalidAccessException,
"Unable to get glpk solution from unbounded model.");
422 STORM_LOG_THROW(
false, storm::exceptions::InvalidAccessException,
"Unable to get glpk solution from unoptimized model.");
425 int variableIndex = variableToIndexMap.at(variable);
428 if (this->modelContainsIntegerVariables) {
429 value = glp_mip_col_val(this->lp, variableIndex);
431 value = glp_get_col_prim(this->lp, variableIndex);
434 double roundedValue = std::round(value);
435 double diff = std::abs(roundedValue - value);
437 "Illegal value for integer variable in GLPK solution (" << value <<
"). Difference to nearest int is " << diff);
438 return static_cast<int_fast64_t
>(roundedValue);
441 "This version of storm was compiled without support for GLPK. Yet, a method was called that requires this support. Please choose a "
442 "version with GLPK support.");
446template<
typename ValueType,
bool RawMode>
448#ifdef STORM_HAVE_GLPK
450 STORM_LOG_THROW(!this->
isInfeasible(), storm::exceptions::InvalidAccessException,
"Unable to get glpk solution from infeasible model.");
451 STORM_LOG_THROW(!this->
isUnbounded(), storm::exceptions::InvalidAccessException,
"Unable to get glpk solution from unbounded model.");
452 STORM_LOG_THROW(
false, storm::exceptions::InvalidAccessException,
"Unable to get glpk solution from unoptimized model.");
455 int variableIndex = variableToIndexMap.at(variable);
458 if (this->modelContainsIntegerVariables) {
459 value = glp_mip_col_val(this->lp, variableIndex);
461 value = glp_get_col_prim(this->lp, variableIndex);
465 STORM_LOG_ERROR_COND(std::abs(value - 1.0) <= this->integerTolerance,
"Illegal value for binary variable in GLPK solution (" << value <<
").");
468 STORM_LOG_ERROR_COND(std::abs(value) <= this->integerTolerance,
"Illegal value for binary variable in GLPK solution (" << value <<
").");
472 return static_cast<bool>(value);
475 "This version of storm was compiled without support for GLPK. Yet, a method was called that requires this support. Please choose a "
476 "version with GLPK support.");
480template<
typename ValueType,
bool RawMode>
482#ifdef STORM_HAVE_GLPK
484 STORM_LOG_THROW(!this->
isInfeasible(), storm::exceptions::InvalidAccessException,
"Unable to get glpk solution from infeasible model.");
485 STORM_LOG_THROW(!this->
isUnbounded(), storm::exceptions::InvalidAccessException,
"Unable to get glpk solution from unbounded model.");
486 STORM_LOG_THROW(
false, storm::exceptions::InvalidAccessException,
"Unable to get glpk solution from unoptimized model.");
490 if (this->modelContainsIntegerVariables) {
491 value = glp_mip_obj_val(this->lp);
493 value = glp_get_obj_val(this->lp);
499 "This version of storm was compiled without support for GLPK. Yet, a method was called that requires this support. Please choose a "
500 "version with GLPK support.");
504template<
typename ValueType,
bool RawMode>
506#ifdef STORM_HAVE_GLPK
507 glp_write_lp(this->lp,
nullptr, filename.c_str());
510 "This version of storm was compiled without support for GLPK. Yet, a method was called that requires this support. Please choose a "
511 "version with GLPK support.");
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.");
521 IncrementalLevel lvl;
522 lvl.firstConstraintIndex = glp_get_num_rows(this->lp) + 1;
523 incrementalData.push_back(lvl);
527 "This version of storm was compiled without support for GLPK. Yet, a method was called that requires this support. Please choose a "
528 "version with GLPK support.");
532template<
typename ValueType,
bool RawMode>
534#ifdef STORM_HAVE_GLPK
535 if constexpr (RawMode) {
536 STORM_LOG_THROW(
false, storm::exceptions::InvalidOperationException,
"Incremental LP solving not supported in raw mode.");
538 if (incrementalData.empty()) {
541 IncrementalLevel
const& lvl = incrementalData.back();
544 if (indicesToBeRemoved.size() > 1) {
545 glp_del_rows(this->lp, indicesToBeRemoved.size() - 1, indicesToBeRemoved.data());
547 indicesToBeRemoved.clear();
549 if (!lvl.variables.empty()) {
552 for (
auto const& var : lvl.variables) {
554 auto it = variableToIndexMap.find(var);
555 firstIndex = it->second;
556 variableToIndexMap.erase(it);
559 variableToIndexMap.erase(var);
564 glp_del_cols(this->lp, indicesToBeRemoved.size() - 1, indicesToBeRemoved.data());
566 incrementalData.pop_back();
569 int n = glp_get_num_rows(lp);
570 int m = glp_get_num_cols(lp);
572 for (
int i = 1; i <= n; ++i) {
573 if (glp_get_row_stat(lp, i) == GLP_BS) {
577 for (
int j = 1; j <= m; ++j) {
578 if (glp_get_col_stat(lp, j) == GLP_BS) {
582 if (n != (nb + mb)) {
583 glp_std_basis(this->lp);
589 "This version of storm was compiled without support for GLPK. Yet, a method was called that requires this support. Please choose a "
590 "version with GLPK support.");
594template<
typename ValueType,
bool RawMode>
597 this->maxMILPGapRelative = relative;
600template<
typename ValueType,
bool RawMode>
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.
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
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.
GlpkLpSolver(storm::GlpkSolverEnvironment const &glpkSettings, bool debug, std::string const &name, OptimizationDirection const &optDir)
Constructs a solver with the given name and model sense.
typename LpSolver< ValueType, RawMode >::Variable Variable
An interface that captures the functionality of an LP solver.
bool currentModelHasBeenOptimized
OptimizationDirection getOptimizationDirection() const
storm::expressions::Variable declareOrGetExpressionVariable(std::string const &name, VariableType const &type)
#define STORM_LOG_ERROR(message)
#define STORM_LOG_ASSERT(cond, message)
#define STORM_LOG_ERROR_COND(cond, message)
#define STORM_LOG_THROW(cond, exception, message)
SFTBDDChecker::ValueType ValueType
RelationType
An enum type specifying the different relations applicable.
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].
bool isZero(ValueType const &a)
ValueType abs(ValueType const &number)
TargetType convertNumber(SourceType const &number)
std::map< storm::expressions::Variable, double >::const_iterator end() const
void separateVariablesFromConstantPart(VariableCoefficients &rhs)
Brings all variables of the right-hand side coefficients to the left-hand side by negating them and m...
std::map< storm::expressions::Variable, double >::const_iterator begin() const
double getConstantPart() const