Storm
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
GlpkLpSolver.h
Go to the documentation of this file.
1#pragma once
2
3#include <map>
6
7#include "storm-config.h"
8
9#ifdef STORM_HAVE_GLPK
10#include <glpk.h>
11#endif
12
13namespace storm {
14namespace solver {
18template<typename ValueType, bool RawMode = false>
19class GlpkLpSolver : public LpSolver<ValueType, RawMode> {
20 public:
25
33 GlpkLpSolver(std::string const& name, OptimizationDirection const& optDir);
34
41 GlpkLpSolver(std::string const& name);
42
50
56
60 virtual ~GlpkLpSolver();
61
62 virtual Variable addVariable(std::string const& name, VariableType const& type, std::optional<ValueType> const& lowerBound = std::nullopt,
63 std::optional<ValueType> const& upperBound = std::nullopt, ValueType objectiveFunctionCoefficient = 0) override;
64
65 // Methods to incorporate recent changes.
66 virtual void update() const override;
67
68 // Methods to add constraints
69 virtual void addConstraint(std::string const& name, Constraint const& constraint) override;
70 virtual void addIndicatorConstraint(std::string const& name, Variable indicatorVariable, bool indicatorValue, Constraint const& constraint) override;
71
72 // Methods to optimize and retrieve optimality status.
73 virtual void optimize() const override;
74 virtual bool isInfeasible() const override;
75 virtual bool isUnbounded() const override;
76 virtual bool isOptimal() const override;
77
78 // Methods to retrieve values of variables and the objective function in the optimal solutions.
79 virtual ValueType getContinuousValue(Variable const& name) const override;
80 virtual int_fast64_t getIntegerValue(Variable const& name) const override;
81 virtual bool getBinaryValue(Variable const& name) const override;
82 virtual ValueType getObjectiveValue() const override;
83
84 // Methods to print the LP problem to a file.
85 virtual void writeModelToFile(std::string const& filename) const override;
86
87 virtual void push() override;
88 virtual void pop() override;
89
90 virtual void setMaximalMILPGap(ValueType const& gap, bool relative) override;
91 virtual ValueType getMILPGap(bool relative) const override;
92
93 private:
94#ifdef STORM_HAVE_GLPK
95 // The glpk LP problem.
96 glp_prob* lp;
97#endif
98
99 // A mapping from variables to their indices.
100 std::conditional_t<RawMode, std::vector<int>, std::map<storm::expressions::Variable, int>> variableToIndexMap;
101
102 // A flag storing whether the model is an LP or an MILP.
103 bool modelContainsIntegerVariables;
104
105 // Flags that store whether the MILP was found to be infeasible or unbounded.
106 mutable bool isInfeasibleFlag;
107 mutable bool isUnboundedFlag;
108
109 mutable double maxMILPGap;
110 mutable bool maxMILPGapRelative;
111 mutable double actualRelativeMILPGap;
112
113 struct IncrementalLevel {
114 std::vector<Variable> variables;
115 int firstConstraintIndex;
116 };
117 std::vector<IncrementalLevel> incrementalData;
118};
119
120} // namespace solver
121} // namespace storm
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
typename LpSolver< ValueType, RawMode >::Constant Constant
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
An interface that captures the functionality of an LP solver.
Definition LpSolver.h:51
std::conditional_t< RawMode, RawLpConstraint< ValueType >, storm::expressions::Expression > Constraint
Definition LpSolver.h:55
std::conditional_t< RawMode, ValueType, storm::expressions::Expression > Constant
Definition LpSolver.h:54
std::conditional_t< RawMode, typename RawLpConstraint< ValueType >::VariableIndexType, storm::expressions::Variable > Variable
Definition LpSolver.h:53
VariableType
Enumerates the different types of variables.
Definition LpSolver.h:60
LabParser.cpp.
Definition cli.cpp:18