Storm
A Modern Probabilistic Model Checker
|
A class that implements the LpSolver interface using Gurobi. More...
#include <GurobiLpSolver.h>
Public Types | |
using | VariableType = typename LpSolver< ValueType, RawMode >::VariableType |
using | Variable = typename LpSolver< ValueType, RawMode >::Variable |
using | Constant = typename LpSolver< ValueType, RawMode >::Constant |
using | Constraint = typename LpSolver< ValueType, RawMode >::Constraint |
![]() | |
enum class | VariableType { Continuous , Integer , Binary } |
Enumerates the different types of variables. More... | |
using | Variable = std::conditional_t< RawMode, typename RawLpConstraint< ValueType >::VariableIndexType, storm::expressions::Variable > |
using | Constant = std::conditional_t< RawMode, ValueType, storm::expressions::Expression > |
using | Constraint = std::conditional_t< RawMode, RawLpConstraint< ValueType >, storm::expressions::Expression > |
Public Member Functions | |
GurobiLpSolver (std::shared_ptr< GurobiEnvironment > const &environment, std::string const &name, OptimizationDirection const &optDir) | |
Constructs a solver with the given name and model sense. | |
GurobiLpSolver (std::shared_ptr< GurobiEnvironment > const &environment, std::string const &name) | |
Constructs a solver with the given name. | |
GurobiLpSolver (std::shared_ptr< GurobiEnvironment > const &environment, OptimizationDirection const &optDir) | |
Constructs a solver without a name and the given model sense. | |
GurobiLpSolver (std::shared_ptr< GurobiEnvironment > const &environment) | |
Constructs a solver without a name. | |
GurobiLpSolver (GurobiLpSolver< ValueType > const &other) | |
Creates a (deep) copy of this solver. | |
virtual | ~GurobiLpSolver () |
Destructs a solver by freeing the pointers to Gurobi's structures. | |
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 void | update () const override |
Updates the model to make the variables that have been declared since the last call to update usable. | |
virtual void | addConstraint (std::string const &name, Constraint const &constraint) override |
Adds a the given constraint to the LP problem. | |
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, then constraint". | |
virtual void | optimize () const override |
Optimizes the LP problem previously constructed. | |
virtual bool | isInfeasible () const override |
Retrieves whether the model was found to be infeasible. | |
virtual bool | isUnbounded () const override |
Retrieves whether the model was found to be infeasible. | |
virtual bool | isOptimal () const override |
Retrieves whether the model was found to be optimal, i.e. | |
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 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. | |
virtual void | writeModelToFile (std::string const &filename) const override |
Writes the current LP problem to the given file. | |
virtual void | push () override |
Pushes a backtracking point on the solver's stack. | |
virtual void | pop () override |
Pops a backtracking point from the solver's stack. | |
virtual void | setMaximalMILPGap (ValueType const &gap, bool relative) override |
Specifies the maximum difference between lower- and upper objective bounds that triggers termination. | |
virtual ValueType | getMILPGap (bool relative) const override |
Returns the obtained gap after a call to optimize() | |
void | setMaximalSolutionCount (uint64_t value) |
uint64_t | getSolutionCount () const |
ValueType | getContinuousValue (Variable const &name, uint64_t const &solutionIndex) const |
int_fast64_t | getIntegerValue (Variable const &name, uint64_t const &solutionIndex) const |
bool | getBinaryValue (Variable const &name, uint64_t const &solutionIndex) const |
ValueType | getObjectiveValue (uint64_t solutionIndex) const |
![]() | |
LpSolver () | |
Creates an empty LP solver. | |
LpSolver (OptimizationDirection const &optDir) | |
Creates an empty LP solver with the given model sense. | |
virtual | ~LpSolver ()=default |
Variable | addBoundedContinuousVariable (std::string const &name, ValueType lowerBound, ValueType upperBound, ValueType objectiveFunctionCoefficient=0) |
Registers an upper- and lower-bounded continuous variable, i.e. | |
Variable | addLowerBoundedContinuousVariable (std::string const &name, ValueType lowerBound, ValueType objectiveFunctionCoefficient=0) |
Registers a lower-bounded continuous variable, i.e. | |
Variable | addUpperBoundedContinuousVariable (std::string const &name, ValueType upperBound, ValueType objectiveFunctionCoefficient=0) |
Registers an upper-bounded continuous variable, i.e. | |
Variable | addUnboundedContinuousVariable (std::string const &name, ValueType objectiveFunctionCoefficient=0) |
Registers a unbounded continuous variable, i.e. | |
Variable | addContinuousVariable (std::string const &name, std::optional< ValueType > const &lowerBound=std::nullopt, std::optional< ValueType > const &upperBound=std::nullopt, ValueType objectiveFunctionCoefficient=0) |
Registers a continuous variable, i.e. | |
Variable | addBoundedIntegerVariable (std::string const &name, ValueType lowerBound, ValueType upperBound, ValueType objectiveFunctionCoefficient=0) |
Registers an upper- and lower-bounded integer variable, i.e. | |
Variable | addLowerBoundedIntegerVariable (std::string const &name, ValueType lowerBound, ValueType objectiveFunctionCoefficient=0) |
Registers a lower-bounded integer variable, i.e. | |
Variable | addUpperBoundedIntegerVariable (std::string const &name, ValueType upperBound, ValueType objectiveFunctionCoefficient=0) |
Registers an upper-bounded integer variable, i.e. | |
Variable | addUnboundedIntegerVariable (std::string const &name, ValueType objectiveFunctionCoefficient=0) |
Registers an unbounded integer variable, i.e. | |
Variable | addIntegerVariable (std::string const &name, std::optional< ValueType > const &lowerBound=std::nullopt, std::optional< ValueType > const &upperBound=std::nullopt, ValueType objectiveFunctionCoefficient=0) |
Registers an integer variable, i.e. | |
Variable | addBinaryVariable (std::string const &name, ValueType objectiveFunctionCoefficient=0) |
Registers a boolean variable, i.e. | |
Constant | getConstant (ValueType value) const |
Retrieves an expression that characterizes the given constant value. | |
void | setOptimizationDirection (OptimizationDirection const &optimizationDirection) |
Sets whether the objective function of this model is to be minimized or maximized. | |
OptimizationDirection | getOptimizationDirection () const |
Retrieves whether the objective function of this model is to be minimized or maximized. | |
storm::expressions::ExpressionManager const & | getManager () const |
Retrieves the manager for the variables created for this solver. | |
Additional Inherited Members | |
![]() | |
storm::expressions::Variable | declareOrGetExpressionVariable (std::string const &name, VariableType const &type) |
![]() | |
std::shared_ptr< storm::expressions::ExpressionManager > | manager |
bool | currentModelHasBeenOptimized |
A class that implements the LpSolver interface using Gurobi.
Definition at line 46 of file GurobiLpSolver.h.
using storm::solver::GurobiLpSolver< ValueType, RawMode >::Constant = typename LpSolver<ValueType, RawMode>::Constant |
Definition at line 50 of file GurobiLpSolver.h.
using storm::solver::GurobiLpSolver< ValueType, RawMode >::Constraint = typename LpSolver<ValueType, RawMode>::Constraint |
Definition at line 51 of file GurobiLpSolver.h.
using storm::solver::GurobiLpSolver< ValueType, RawMode >::Variable = typename LpSolver<ValueType, RawMode>::Variable |
Definition at line 49 of file GurobiLpSolver.h.
using storm::solver::GurobiLpSolver< ValueType, RawMode >::VariableType = typename LpSolver<ValueType, RawMode>::VariableType |
Definition at line 48 of file GurobiLpSolver.h.
storm::solver::GurobiLpSolver< ValueType, RawMode >::GurobiLpSolver | ( | std::shared_ptr< GurobiEnvironment > const & | environment, |
std::string const & | name, | ||
OptimizationDirection const & | optDir | ||
) |
Constructs a solver with the given name and model sense.
name | The name of the LP problem. |
modelSense | A value indicating whether the value of the objective function is to be minimized or maximized. |
Definition at line 749 of file GurobiLpSolver.cpp.
storm::solver::GurobiLpSolver< ValueType, RawMode >::GurobiLpSolver | ( | std::shared_ptr< GurobiEnvironment > const & | environment, |
std::string const & | name | ||
) |
Constructs a solver with the given name.
By default the objective function is assumed to be minimized, but this may be altered later using a call to setModelSense.
name | The name of the LP problem. |
Definition at line 755 of file GurobiLpSolver.cpp.
storm::solver::GurobiLpSolver< ValueType, RawMode >::GurobiLpSolver | ( | std::shared_ptr< GurobiEnvironment > const & | environment, |
OptimizationDirection const & | optDir | ||
) |
Constructs a solver without a name and the given model sense.
modelSense | A value indicating whether the value of the objective function is to be minimized or maximized. |
Definition at line 761 of file GurobiLpSolver.cpp.
storm::solver::GurobiLpSolver< ValueType, RawMode >::GurobiLpSolver | ( | std::shared_ptr< GurobiEnvironment > const & | environment | ) |
Constructs a solver without a name.
By default the objective function is assumed to be minimized, but this may be altered later using a call to setModelSense.
Definition at line 767 of file GurobiLpSolver.cpp.
storm::solver::GurobiLpSolver< ValueType, RawMode >::GurobiLpSolver | ( | GurobiLpSolver< ValueType > const & | other | ) |
Creates a (deep) copy of this solver.
other |
|
virtual |
Destructs a solver by freeing the pointers to Gurobi's structures.
Definition at line 773 of file GurobiLpSolver.cpp.
|
overridevirtual |
Adds a the given constraint to the LP problem.
name | The name of the constraint. If empty, the constraint has no name. |
constraint | An expression that represents the constraint. The given constraint must be a linear (in)equality over the registered variables. |
Implements storm::solver::LpSolver< ValueType, RawMode >.
Definition at line 790 of file GurobiLpSolver.cpp.
|
overridevirtual |
Adds the given indicator constraint to the LP problem: "If indicatorVariable == indicatorValue, then constraint".
name | The name of the constraint. If empty, the constraint has no name. |
indicatorVariable | must be a registered binary |
indicatorValue | |
constraint | An expression that represents the constraint. The given constraint must be a linear (in)equality over the registered variables. |
Implements storm::solver::LpSolver< ValueType, RawMode >.
Definition at line 796 of file GurobiLpSolver.cpp.
|
overridevirtual |
Registers a variable of the given type.
name | The name of the variable. |
type | The type of the variable |
lowerBound | The optional lower bound |
upperBound | The optional upper bound |
objectiveFunctionCoefficient | The coefficient with which the variable appears in the objective function. If omitted (or set to zero), the variable is irrelevant for the objective value. |
Implements storm::solver::LpSolver< ValueType, RawMode >.
Definition at line 776 of file GurobiLpSolver.cpp.
|
overridevirtual |
Retrieves the value of the binary variable with the given name.
Note that this may only be called, if the model was found to be optimal, i.e. iff isOptimal() returns true.
variable | The variable whose integer value (in the optimal solution) to retrieve. |
Implements storm::solver::LpSolver< ValueType, RawMode >.
Definition at line 838 of file GurobiLpSolver.cpp.
bool storm::solver::GurobiLpSolver< ValueType, RawMode >::getBinaryValue | ( | Variable const & | name, |
uint64_t const & | solutionIndex | ||
) | const |
Definition at line 892 of file GurobiLpSolver.cpp.
|
overridevirtual |
Retrieves the value of the continuous variable with the given name.
Note that this may only be called, if the model was found to be optimal, i.e. iff isOptimal() returns true.
variable | The variable whose integer value (in the optimal solution) to retrieve. |
Implements storm::solver::LpSolver< ValueType, RawMode >.
Definition at line 826 of file GurobiLpSolver.cpp.
ValueType storm::solver::GurobiLpSolver< ValueType, RawMode >::getContinuousValue | ( | Variable const & | name, |
uint64_t const & | solutionIndex | ||
) | const |
Definition at line 880 of file GurobiLpSolver.cpp.
|
overridevirtual |
Retrieves the value of the integer variable with the given name.
Note that this may only be called, if the model was found to be optimal, i.e. iff isOptimal() returns true.
variable | The variable whose integer value (in the optimal solution) to retrieve. |
Implements storm::solver::LpSolver< ValueType, RawMode >.
Definition at line 832 of file GurobiLpSolver.cpp.
int_fast64_t storm::solver::GurobiLpSolver< ValueType, RawMode >::getIntegerValue | ( | Variable const & | name, |
uint64_t const & | solutionIndex | ||
) | const |
Definition at line 886 of file GurobiLpSolver.cpp.
|
overridevirtual |
Returns the obtained gap after a call to optimize()
Implements storm::solver::LpSolver< ValueType, RawMode >.
Definition at line 910 of file GurobiLpSolver.cpp.
|
overridevirtual |
Retrieves the value of the objective function.
Note that this may only be called, if the model was found to be optimal, i.e. iff isOptimal() returns true.
Implements storm::solver::LpSolver< ValueType, RawMode >.
Definition at line 844 of file GurobiLpSolver.cpp.
ValueType storm::solver::GurobiLpSolver< ValueType, RawMode >::getObjectiveValue | ( | uint64_t | solutionIndex | ) | const |
Definition at line 898 of file GurobiLpSolver.cpp.
uint64_t storm::solver::GurobiLpSolver< ValueType, RawMode >::getSolutionCount | ( | ) | const |
Definition at line 874 of file GurobiLpSolver.cpp.
|
overridevirtual |
Retrieves whether the model was found to be infeasible.
This can only be called after the model has been optimized and not modified afterwards. Otherwise, an exception is thrown.
Implements storm::solver::LpSolver< ValueType, RawMode >.
Definition at line 808 of file GurobiLpSolver.cpp.
|
overridevirtual |
Retrieves whether the model was found to be optimal, i.e.
neither infeasible nor unbounded. This can only be called after the model has been optimized and not modified afterwards. Otherwise, an exception is thrown.
Implements storm::solver::LpSolver< ValueType, RawMode >.
Definition at line 820 of file GurobiLpSolver.cpp.
|
overridevirtual |
Retrieves whether the model was found to be infeasible.
This can only be called after the model has been optimized and not modified afterwards. Otherwise, an exception is thrown.
Implements storm::solver::LpSolver< ValueType, RawMode >.
Definition at line 814 of file GurobiLpSolver.cpp.
|
overridevirtual |
Optimizes the LP problem previously constructed.
Afterwards, the methods isInfeasible, isUnbounded and isOptimal can be used to query the optimality status.
Implements storm::solver::LpSolver< ValueType, RawMode >.
Definition at line 802 of file GurobiLpSolver.cpp.
|
overridevirtual |
Pops a backtracking point from the solver's stack.
This deletes all assertions from the solver's stack that were added after the last call to push().
Implements storm::solver::LpSolver< ValueType, RawMode >.
Definition at line 862 of file GurobiLpSolver.cpp.
|
overridevirtual |
Pushes a backtracking point on the solver's stack.
A following call to pop() deletes exactly those assertions from the solver's stack that were added after this call.
Implements storm::solver::LpSolver< ValueType, RawMode >.
Definition at line 856 of file GurobiLpSolver.cpp.
|
overridevirtual |
Specifies the maximum difference between lower- and upper objective bounds that triggers termination.
That means a solution is considered optimal if upperBound - lowerBound < gap * (relative ? |upperBound| : 1). Only relevant for programs with integer/boolean variables.
Implements storm::solver::LpSolver< ValueType, RawMode >.
Definition at line 904 of file GurobiLpSolver.cpp.
void storm::solver::GurobiLpSolver< ValueType, RawMode >::setMaximalSolutionCount | ( | uint64_t | value | ) |
Definition at line 868 of file GurobiLpSolver.cpp.
|
overridevirtual |
Updates the model to make the variables that have been declared since the last call to update
usable.
Implements storm::solver::LpSolver< ValueType, RawMode >.
Definition at line 784 of file GurobiLpSolver.cpp.
|
overridevirtual |
Writes the current LP problem to the given file.
filename | The file to which to write the string representation of the LP. |
Implements storm::solver::LpSolver< ValueType, RawMode >.
Definition at line 850 of file GurobiLpSolver.cpp.