31template<
typename ValueType,
bool RawMode>
36 modelContainsIntegerVariables(false),
37 isInfeasibleFlag(false),
38 isUnboundedFlag(false) {
40 lp = glp_create_prob();
43 glp_set_prob_name(lp, name.c_str());
52 glp_iocp* defaultParameters =
new glp_iocp();
53 glp_init_iocp(defaultParameters);
54 this->maxMILPGap = defaultParameters->mip_gap;
55 this->maxMILPGapRelative =
true;
58template<
typename ValueType,
bool RawMode>
63template<
typename ValueType,
bool RawMode>
68template<
typename ValueType,
bool RawMode>
69GlpkLpSolver<ValueType, RawMode>::GlpkLpSolver(OptimizationDirection
const& optDir) : GlpkLpSolver(
"", optDir) {
73template<
typename ValueType,
bool RawMode>
74GlpkLpSolver<ValueType, RawMode>::~GlpkLpSolver() {
76 glp_delete_prob(this->lp);
80template<
typename ValueType,
bool RawMode>
81int getGlpkType(
typename GlpkLpSolver<ValueType, RawMode>::VariableType
const& type) {
83 case GlpkLpSolver<ValueType, RawMode>::VariableType::Continuous:
85 case GlpkLpSolver<ValueType, RawMode>::VariableType::Integer:
87 case GlpkLpSolver<ValueType, RawMode>::VariableType::Binary:
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) {
100 if constexpr (RawMode) {
101 resultVar = variableToIndexMap.size();
103 resultVar = this->declareOrGetExpressionVariable(name, type);
106 STORM_LOG_ASSERT(variableToIndexMap.count(resultVar) == 0,
"Variable " << resultVar.getName() <<
" exists already in the model.");
110 if (lowerBound.has_value()) {
111 boundType = upperBound.has_value() ? GLP_DB : GLP_LO;
113 boundType = upperBound.has_value() ? GLP_UP : GLP_FR;
116 if (type == VariableType::Integer || type == VariableType::Binary) {
117 this->modelContainsIntegerVariables =
true;
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,
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));
128 if constexpr (RawMode) {
129 this->variableToIndexMap.push_back(variableIndex);
131 this->variableToIndexMap.emplace(resultVar, variableIndex);
132 if (!incrementalData.empty()) {
133 incrementalData.back().variables.push_back(resultVar);
140template<
typename ValueType,
bool RawMode>
141void GlpkLpSolver<ValueType, RawMode>::update()
const {
145template<
typename ValueType,
bool RawMode>
146void GlpkLpSolver<ValueType, RawMode>::addConstraint(std::string
const& name, Constraint
const& constraint) {
148 int constraintIndex = glp_add_rows(this->lp, 1);
149 glp_set_row_name(this->lp, constraintIndex, name.c_str());
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));
164 coefficients.reserve(constraint.lhsCoefficients.size() + 1);
165 for (
auto const& coef : constraint.lhsCoefficients) {
166 coefficients.push_back(storm::utility::convertNumber<double>(coef));
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.");
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);
191 switch (relationType) {
193 glp_set_row_bnds(this->lp, constraintIndex, GLP_UP, 0,
197 glp_set_row_bnds(this->lp, constraintIndex, GLP_UP, 0, rhs);
200 glp_set_row_bnds(this->lp, constraintIndex, GLP_LO,
204 glp_set_row_bnds(this->lp, constraintIndex, GLP_LO, rhs, 0);
207 glp_set_row_bnds(this->lp, constraintIndex, GLP_FX, rhs, rhs);
214 glp_set_mat_row(this->lp, constraintIndex, variableIndices.size() - 1, variableIndices.data(), coefficients.data());
216 this->currentModelHasBeenOptimized =
false;
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.");
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) {
232 assert(factor >= 0.0);
234 if (actualRelativeGap * factor <= mipgap.first) {
236 mipgap.first = actualRelativeGap;
237 mipgap.second =
true;
238 glp_ios_terminate(t);
242template<
typename ValueType,
bool RawMode>
243void GlpkLpSolver<ValueType, RawMode>::optimize()
const {
245 this->isInfeasibleFlag =
false;
246 this->isUnboundedFlag =
false;
249 glp_set_obj_dir(this->lp, this->getOptimizationDirection() == OptimizationDirection::Minimize ? GLP_MIN : GLP_MAX);
252 if (this->modelContainsIntegerVariables) {
253 glp_iocp* parameters =
new glp_iocp();
254 glp_init_iocp(parameters);
256 this->isInfeasibleFlag =
false;
258 parameters->presolve = GLP_ON;
262 error = glp_simplex(this->lp,
nullptr);
263 STORM_LOG_THROW(error == 0, storm::exceptions::InvalidStateException,
"Unable to optimize relaxed glpk model (" << error <<
").");
265 if (glp_get_status(this->lp) == GLP_INFEAS || glp_get_status(this->lp) == GLP_NOFEAS) {
266 this->isInfeasibleFlag =
true;
270 if (glp_get_status(this->lp) == GLP_UNBND) {
271 parameters->presolve = GLP_ON;
273 parameters->presolve = GLP_OFF;
276 if (!this->isInfeasibleFlag) {
279 std::pair<double, bool> mipgap(this->maxMILPGap, this->maxMILPGapRelative);
281 parameters->cb_func = &callback;
282 parameters->cb_info = &mipgap;
286 error = glp_intopt(this->lp, parameters);
287 int status = glp_mip_status(this->lp);
291 this->actualRelativeMILPGap = mipgap.first;
295 if (error == GLP_ENOPFS || status == GLP_NOFEAS) {
296 this->isInfeasibleFlag =
true;
298 }
else if (error == GLP_ENODFS) {
299 this->isUnboundedFlag =
true;
301 }
else if (error == GLP_ESTOP) {
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.";
310 error = glp_simplex(this->lp,
nullptr);
313 STORM_LOG_THROW(error == 0, storm::exceptions::InvalidStateException,
"Unable to optimize glpk model (" << error <<
").");
314 this->currentModelHasBeenOptimized =
true;
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.";
323 if (this->modelContainsIntegerVariables) {
324 return isInfeasibleFlag;
326 return glp_get_status(this->lp) == GLP_INFEAS || glp_get_status(this->lp) == GLP_NOFEAS;
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.";
336 if (this->modelContainsIntegerVariables) {
337 return isUnboundedFlag;
339 return glp_get_status(this->lp) == GLP_UNBND;
343template<
typename ValueType,
bool RawMode>
344bool GlpkLpSolver<ValueType, RawMode>::isOptimal()
const {
345 if (!this->currentModelHasBeenOptimized) {
349 return !isInfeasible() && !isUnbounded();
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.");
360 int variableIndex = variableToIndexMap.at(variable);
363 if (this->modelContainsIntegerVariables) {
364 value = glp_mip_col_val(this->lp,
static_cast<int>(variableIndex));
366 value = glp_get_col_prim(this->lp,
static_cast<int>(variableIndex));
368 return storm::utility::convertNumber<ValueType>(value);
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.");
379 int variableIndex = variableToIndexMap.at(variable);
382 if (this->modelContainsIntegerVariables) {
383 value = glp_mip_col_val(this->lp, variableIndex);
385 value = glp_get_col_prim(this->lp, variableIndex);
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);
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.");
403 int variableIndex = variableToIndexMap.at(variable);
406 if (this->modelContainsIntegerVariables) {
407 value = glp_mip_col_val(this->lp, variableIndex);
409 value = glp_get_col_prim(this->lp, variableIndex);
414 "Illegal value for binary variable in GLPK solution (" << value <<
").");
418 "Illegal value for binary variable in GLPK solution (" << value <<
").");
422 return static_cast<bool>(value);
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.");
434 if (this->modelContainsIntegerVariables) {
435 value = glp_mip_obj_val(this->lp);
437 value = glp_get_obj_val(this->lp);
440 return storm::utility::convertNumber<ValueType>(value);
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());
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");
453 IncrementalLevel lvl;
454 lvl.firstConstraintIndex = glp_get_num_rows(this->lp) + 1;
455 incrementalData.push_back(lvl);
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");
464 if (incrementalData.empty()) {
467 IncrementalLevel
const& lvl = incrementalData.back();
470 if (indicesToBeRemoved.size() > 1) {
471 glp_del_rows(this->lp, indicesToBeRemoved.size() - 1, indicesToBeRemoved.data());
473 indicesToBeRemoved.clear();
475 if (!lvl.variables.empty()) {
478 for (
auto const& var : lvl.variables) {
480 auto it = variableToIndexMap.find(var);
481 firstIndex = it->second;
482 variableToIndexMap.erase(it);
485 variableToIndexMap.erase(var);
490 glp_del_cols(this->lp, indicesToBeRemoved.size() - 1, indicesToBeRemoved.data());
492 incrementalData.pop_back();
495 int n = glp_get_num_rows(lp);
496 int m = glp_get_num_cols(lp);
498 for (
int i = 1;
i <= n; ++
i) {
499 if (glp_get_row_stat(lp, i) == GLP_BS) {
503 for (
int j = 1; j <= m; ++j) {
504 if (glp_get_col_stat(lp, j) == GLP_BS) {
508 if (n != (nb + mb)) {
509 glp_std_basis(this->lp);
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;
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.");
525 return storm::utility::convertNumber<ValueType>(this->actualRelativeMILPGap);
527 return storm::utility::abs<ValueType>(storm::utility::convertNumber<ValueType>(this->actualRelativeMILPGap) * getObjectiveValue());
531template class GlpkLpSolver<double, true>;
532template class GlpkLpSolver<double, false>;
533template class GlpkLpSolver<storm::RationalNumber, true>;
534template class GlpkLpSolver<storm::RationalNumber, false>;
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)
#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.
SettingsType const & getModule()
Get module.
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