Storm
A Modern Probabilistic Model Checker
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
storm::solver::SoplexLpSolver< ValueType, RawMode > Class Template Reference

#include <SoplexLpSolver.h>

Inheritance diagram for storm::solver::SoplexLpSolver< ValueType, RawMode >:
Collaboration diagram for storm::solver::SoplexLpSolver< ValueType, RawMode >:

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
 
- Public Types inherited from storm::solver::LpSolver< ValueType, RawMode >
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

 SoplexLpSolver (std::string const &name, OptimizationDirection const &optDir)
 Constructs a solver with the given name and model sense.
 
 SoplexLpSolver (std::string const &name)
 Constructs a solver with the given name.
 
 SoplexLpSolver (OptimizationDirection const &optDir=OptimizationDirection::Minimize)
 Constructs a solver without a name and the given model sense.
 
 SoplexLpSolver (SoplexLpSolver< ValueType > const &other)
 Creates a (deep) copy of this solver.
 
virtual ~SoplexLpSolver ()
 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 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()
 
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.
 
- Public Member Functions inherited from storm::solver::LpSolver< ValueType, RawMode >
 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

- Protected Member Functions inherited from storm::solver::LpSolver< ValueType, RawMode >
storm::expressions::Variable declareOrGetExpressionVariable (std::string const &name, VariableType const &type)
 
- Protected Attributes inherited from storm::solver::LpSolver< ValueType, RawMode >
std::shared_ptr< storm::expressions::ExpressionManagermanager
 
bool currentModelHasBeenOptimized
 

Detailed Description

template<typename ValueType, bool RawMode = false>
class storm::solver::SoplexLpSolver< ValueType, RawMode >

Definition at line 16 of file SoplexLpSolver.h.

Member Typedef Documentation

◆ Constant

template<typename ValueType , bool RawMode = false>
using storm::solver::SoplexLpSolver< ValueType, RawMode >::Constant = typename LpSolver<ValueType, RawMode>::Constant

Definition at line 20 of file SoplexLpSolver.h.

◆ Constraint

template<typename ValueType , bool RawMode = false>
using storm::solver::SoplexLpSolver< ValueType, RawMode >::Constraint = typename LpSolver<ValueType, RawMode>::Constraint

Definition at line 21 of file SoplexLpSolver.h.

◆ Variable

template<typename ValueType , bool RawMode = false>
using storm::solver::SoplexLpSolver< ValueType, RawMode >::Variable = typename LpSolver<ValueType, RawMode>::Variable

Definition at line 19 of file SoplexLpSolver.h.

◆ VariableType

template<typename ValueType , bool RawMode = false>
using storm::solver::SoplexLpSolver< ValueType, RawMode >::VariableType = typename LpSolver<ValueType, RawMode>::VariableType

Definition at line 18 of file SoplexLpSolver.h.

Constructor & Destructor Documentation

◆ SoplexLpSolver() [1/4]

template<typename ValueType , bool RawMode>
storm::solver::SoplexLpSolver< ValueType, RawMode >::SoplexLpSolver ( std::string const &  name,
OptimizationDirection const &  optDir 
)

Constructs a solver with the given name and model sense.

Parameters
nameThe name of the LP problem.
modelSenseA value indicating whether the value of the objective function is to be minimized or maximized.

Definition at line 300 of file SoplexLpSolver.cpp.

◆ SoplexLpSolver() [2/4]

template<typename ValueType , bool RawMode>
storm::solver::SoplexLpSolver< ValueType, RawMode >::SoplexLpSolver ( 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.

Parameters
nameThe name of the LP problem.

Definition at line 306 of file SoplexLpSolver.cpp.

◆ SoplexLpSolver() [3/4]

template<typename ValueType , bool RawMode>
storm::solver::SoplexLpSolver< ValueType, RawMode >::SoplexLpSolver ( OptimizationDirection const &  optDir = OptimizationDirection::Minimize)

Constructs a solver without a name and the given model sense.

Parameters
modelSenseA value indicating whether the value of the objective function is to be minimized or maximized.

Definition at line 312 of file SoplexLpSolver.cpp.

◆ SoplexLpSolver() [4/4]

template<typename ValueType , bool RawMode = false>
storm::solver::SoplexLpSolver< ValueType, RawMode >::SoplexLpSolver ( SoplexLpSolver< ValueType > const &  other)

Creates a (deep) copy of this solver.

Parameters
other

◆ ~SoplexLpSolver()

template<typename ValueType , bool RawMode>
storm::solver::SoplexLpSolver< ValueType, RawMode >::~SoplexLpSolver ( )
virtual

Destructs a solver by freeing the pointers to Gurobi's structures.

Definition at line 318 of file SoplexLpSolver.cpp.

Member Function Documentation

◆ addConstraint()

template<typename ValueType , bool RawMode>
void storm::solver::SoplexLpSolver< ValueType, RawMode >::addConstraint ( std::string const &  name,
Constraint const &  constraint 
)
overridevirtual

Adds a the given constraint to the LP problem.

Parameters
nameThe name of the constraint. If empty, the constraint has no name.
constraintAn 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 335 of file SoplexLpSolver.cpp.

◆ addIndicatorConstraint()

template<typename ValueType , bool RawMode>
void storm::solver::SoplexLpSolver< ValueType, RawMode >::addIndicatorConstraint ( std::string const &  name,
Variable  indicatorVariable,
bool  indicatorValue,
Constraint const &  constraint 
)
overridevirtual

Adds the given indicator constraint to the LP problem: "If indicatorVariable == indicatorValue, then constraint".

Parameters
nameThe name of the constraint. If empty, the constraint has no name.
indicatorVariablemust be a registered binary
indicatorValue
constraintAn 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 341 of file SoplexLpSolver.cpp.

◆ addVariable()

template<typename ValueType , bool RawMode>
SoplexLpSolver< ValueType, RawMode >::Variable storm::solver::SoplexLpSolver< ValueType, RawMode >::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 
)
overridevirtual

Registers a variable of the given type.

Note
In RawMode this returns a variable index. Variable indices are assigned consecutively starting at 0, i.e. the n'th variable has index (n-1).
Parameters
nameThe name of the variable.
typeThe type of the variable
lowerBoundThe optional lower bound
upperBoundThe optional upper bound
objectiveFunctionCoefficientThe 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 321 of file SoplexLpSolver.cpp.

◆ getBinaryValue()

template<typename ValueType , bool RawMode>
bool storm::solver::SoplexLpSolver< ValueType, RawMode >::getBinaryValue ( Variable const &  variable) const
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.

Parameters
variableThe variable whose integer value (in the optimal solution) to retrieve.
Returns
The value of the binary variable in the optimal solution.

Implements storm::solver::LpSolver< ValueType, RawMode >.

Definition at line 407 of file SoplexLpSolver.cpp.

◆ getContinuousValue()

template<typename ValueType , bool RawMode>
ValueType storm::solver::SoplexLpSolver< ValueType, RawMode >::getContinuousValue ( Variable const &  variable) const
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.

Parameters
variableThe variable whose integer value (in the optimal solution) to retrieve.
Returns
The value of the continuous variable in the optimal solution.

Implements storm::solver::LpSolver< ValueType, RawMode >.

Definition at line 371 of file SoplexLpSolver.cpp.

◆ getIntegerValue()

template<typename ValueType , bool RawMode>
int_fast64_t storm::solver::SoplexLpSolver< ValueType, RawMode >::getIntegerValue ( Variable const &  variable) const
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.

Parameters
variableThe variable whose integer value (in the optimal solution) to retrieve.
Returns
The value of the integer variable in the optimal solution.

Implements storm::solver::LpSolver< ValueType, RawMode >.

Definition at line 402 of file SoplexLpSolver.cpp.

◆ getMILPGap()

template<typename ValueType , bool RawMode>
ValueType storm::solver::SoplexLpSolver< ValueType, RawMode >::getMILPGap ( bool  relative) const
overridevirtual

Returns the obtained gap after a call to optimize()

Implements storm::solver::LpSolver< ValueType, RawMode >.

Definition at line 417 of file SoplexLpSolver.cpp.

◆ getObjectiveValue()

template<typename ValueType , bool RawMode>
ValueType storm::solver::SoplexLpSolver< ValueType, RawMode >::getObjectiveValue ( ) const
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.

Returns
The value of the objective function in the optimal solution.

Implements storm::solver::LpSolver< ValueType, RawMode >.

Definition at line 377 of file SoplexLpSolver.cpp.

◆ isInfeasible()

template<typename ValueType , bool RawMode>
bool storm::solver::SoplexLpSolver< ValueType, RawMode >::isInfeasible ( ) const
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.

Returns
True if the model was optimized and found to be infeasible.

Implements storm::solver::LpSolver< ValueType, RawMode >.

Definition at line 353 of file SoplexLpSolver.cpp.

◆ isOptimal()

template<typename ValueType , bool RawMode>
bool storm::solver::SoplexLpSolver< ValueType, RawMode >::isOptimal ( ) const
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.

Returns
True if the model was optimized and found to be neither infeasible nor unbounded.

Implements storm::solver::LpSolver< ValueType, RawMode >.

Definition at line 365 of file SoplexLpSolver.cpp.

◆ isUnbounded()

template<typename ValueType , bool RawMode>
bool storm::solver::SoplexLpSolver< ValueType, RawMode >::isUnbounded ( ) const
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.

Returns
True if the model was optimized and found to be unbounded.

Implements storm::solver::LpSolver< ValueType, RawMode >.

Definition at line 359 of file SoplexLpSolver.cpp.

◆ optimize()

template<typename ValueType , bool RawMode>
void storm::solver::SoplexLpSolver< ValueType, RawMode >::optimize ( ) const
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 347 of file SoplexLpSolver.cpp.

◆ pop()

template<typename ValueType , bool RawMode>
void storm::solver::SoplexLpSolver< ValueType, RawMode >::pop ( )
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 395 of file SoplexLpSolver.cpp.

◆ push()

template<typename ValueType , bool RawMode>
void storm::solver::SoplexLpSolver< ValueType, RawMode >::push ( )
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 389 of file SoplexLpSolver.cpp.

◆ setMaximalMILPGap()

template<typename ValueType , bool RawMode>
void storm::solver::SoplexLpSolver< ValueType, RawMode >::setMaximalMILPGap ( ValueType const &  gap,
bool  relative 
)
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 412 of file SoplexLpSolver.cpp.

◆ update()

template<typename ValueType , bool RawMode>
void storm::solver::SoplexLpSolver< ValueType, RawMode >::update ( ) const
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 329 of file SoplexLpSolver.cpp.

◆ writeModelToFile()

template<typename ValueType , bool RawMode>
void storm::solver::SoplexLpSolver< ValueType, RawMode >::writeModelToFile ( std::string const &  filename) const
overridevirtual

Writes the current LP problem to the given file.

Parameters
filenameThe file to which to write the string representation of the LP.

Implements storm::solver::LpSolver< ValueType, RawMode >.

Definition at line 383 of file SoplexLpSolver.cpp.


The documentation for this class was generated from the following files: