Storm
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
GurobiLpSolver.h
Go to the documentation of this file.
1#ifndef STORM_SOLVER_GUROBILPSOLVER
2#define STORM_SOLVER_GUROBILPSOLVER
3
4#include <map>
5#include <optional>
7// To detect whether the usage of Gurobi is possible, this include is neccessary.
8#include "storm-config.h"
9
10#ifdef STORM_HAVE_GUROBI
11extern "C" {
12#include "gurobi_c.h"
13
14int __stdcall GRBislp(GRBenv**, const char*, const char*, const char*, const char*);
15}
16#endif
17
18namespace storm {
19namespace solver {
20
22 public:
23 GurobiEnvironment() = default;
26 virtual ~GurobiEnvironment();
30 void initialize();
31 void setOutput(bool set = false);
32#ifdef STORM_HAVE_GUROBI
33 GRBenv* operator*();
34#endif
35 private:
36 bool initialized = false;
37#ifdef STORM_HAVE_GUROBI
38 GRBenv* env = nullptr;
39#endif
40};
41
45template<typename ValueType, bool RawMode = false>
46class GurobiLpSolver : public LpSolver<ValueType, RawMode> {
47 public:
52
60 GurobiLpSolver(std::shared_ptr<GurobiEnvironment> const& environment, std::string const& name, OptimizationDirection const& optDir);
61
68 GurobiLpSolver(std::shared_ptr<GurobiEnvironment> const& environment, std::string const& name);
69
76 GurobiLpSolver(std::shared_ptr<GurobiEnvironment> const& environment, OptimizationDirection const& optDir);
77
82 GurobiLpSolver(std::shared_ptr<GurobiEnvironment> const& environment);
83
89
93 virtual ~GurobiLpSolver();
94
95 // Methods to add variables.
96 virtual Variable addVariable(std::string const& name, VariableType const& type, std::optional<ValueType> const& lowerBound = std::nullopt,
97 std::optional<ValueType> const& upperBound = std::nullopt, ValueType objectiveFunctionCoefficient = 0) override;
98
99 // Methods to incorporate recent changes.
100 virtual void update() const override;
101
102 // Methods to add constraints
103 virtual void addConstraint(std::string const& name, Constraint const& constraint) override;
104 virtual void addIndicatorConstraint(std::string const& name, Variable indicatorVariable, bool indicatorValue, Constraint const& constraint) override;
105
106 // Methods to optimize and retrieve optimality status.
107 virtual void optimize() const override;
108 virtual bool isInfeasible() const override;
109 virtual bool isUnbounded() const override;
110 virtual bool isOptimal() const override;
111
112 // Methods to retrieve values of variables and the objective function in the optimal solutions.
113 virtual ValueType getContinuousValue(Variable const& name) const override;
114 virtual int_fast64_t getIntegerValue(Variable const& name) const override;
115 virtual bool getBinaryValue(Variable const& name) const override;
116 virtual ValueType getObjectiveValue() const override;
117 // Methods to print the LP problem to a file.
118 virtual void writeModelToFile(std::string const& filename) const override;
119
120 virtual void push() override;
121 virtual void pop() override;
122
123 virtual void setMaximalMILPGap(ValueType const& gap, bool relative) override;
124 virtual ValueType getMILPGap(bool relative) const override;
125
126 // Methods to retrieve values of sub-optimal solutions found along the way.
127 void setMaximalSolutionCount(uint64_t value); // How many solutions will be stored (at max)
128 uint64_t getSolutionCount() const; // How many solutions have been found
129 ValueType getContinuousValue(Variable const& name, uint64_t const& solutionIndex) const;
130 int_fast64_t getIntegerValue(Variable const& name, uint64_t const& solutionIndex) const;
131 bool getBinaryValue(Variable const& name, uint64_t const& solutionIndex) const;
132 ValueType getObjectiveValue(uint64_t solutionIndex) const;
133
134 private:
135#ifdef STORM_HAVE_GUROBI
136 // The Gurobi model.
137 GRBmodel* model;
138#endif
139
140 std::shared_ptr<GurobiEnvironment> environment;
141
142 // The index of the next variable.
143 int nextVariableIndex;
144
145 // A mapping from variables to their indices.
146 std::map<storm::expressions::Variable, int> variableToIndexMap;
147
148 struct IncrementalLevel {
149 std::vector<storm::expressions::Variable> variables;
150 // Gurobi considers a different set of indices for linear constraints and general constraints.
151 // The term "general constraints" is used by Gurobi to refer to "non-standard" constraints, e.g., indicator constraint.
152 int firstConstraintIndex;
153 int firstGenConstraintIndex;
154 };
155 std::vector<IncrementalLevel> incrementalData;
156};
157
159
165std::string toString(GurobiSolverMethod const& method);
166std::optional<GurobiSolverMethod> gurobiSolverMethodFromString(std::string const&);
167std::vector<GurobiSolverMethod> getGurobiSolverMethods();
168
169} // namespace solver
170} // namespace storm
171
172#endif /* STORM_SOLVER_GUROBILPSOLVER */
GurobiEnvironment(GurobiEnvironment const &)=delete
GurobiEnvironment & operator=(GurobiEnvironment const &)=delete
void initialize()
Sets some properties of the Gurobi environment according to parameters given by the options.
A class that implements the LpSolver interface using Gurobi.
virtual ~GurobiLpSolver()
Destructs a solver by freeing the pointers to Gurobi's structures.
GurobiLpSolver(GurobiLpSolver< ValueType > const &other)
Creates a (deep) copy of this solver.
virtual bool isInfeasible() const override
Retrieves whether the model was found to be infeasible.
virtual int_fast64_t getIntegerValue(Variable const &name) const override
Retrieves the value of the integer variable with the given name.
virtual bool isUnbounded() const override
Retrieves whether the model was found to be infeasible.
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.
void setMaximalSolutionCount(uint64_t value)
typename LpSolver< ValueType, RawMode >::VariableType VariableType
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 ValueType getContinuousValue(Variable const &name) const override
Retrieves the value of the continuous variable with the given name.
virtual bool getBinaryValue(Variable const &name) const override
Retrieves the value of the binary variable with the given name.
virtual ValueType getObjectiveValue() const override
Retrieves the value of the objective function.
typename LpSolver< ValueType, RawMode >::Constant Constant
virtual void pop() override
Pops a backtracking point from the solver's stack.
virtual void writeModelToFile(std::string const &filename) const override
Writes the current LP problem to the given file.
typename LpSolver< ValueType, RawMode >::Variable Variable
virtual void optimize() const override
Optimizes the LP problem previously constructed.
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.
typename LpSolver< ValueType, RawMode >::Constraint Constraint
virtual ValueType getMILPGap(bool relative) const override
Returns the obtained gap after a call to optimize()
virtual bool isOptimal() const override
Retrieves whether the model was found to be optimal, i.e.
virtual void update() const override
Updates the model to make the variables that have been declared since the last call to update usable.
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
std::string toString(GurobiSolverMethod const &method)
Yields a string representation of the GurobiSolverMethod.
std::optional< GurobiSolverMethod > gurobiSolverMethodFromString(std::string const &method)
std::vector< GurobiSolverMethod > getGurobiSolverMethods()
LabParser.cpp.
Definition cli.cpp:18