An interface that captures the functionality of an LP solver. More...

#include <LpSolver.h>

Inheritance diagram for storm::solver::LpSolver< ValueType, RawMode >:

[legend]

Public Types
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
	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.

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)=0
	Registers a variable of the given type.

Constant	getConstant (ValueType value) const
	Retrieves an expression that characterizes the given constant value.

virtual void	update () const =0
	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)=0
	Adds a the given constraint to the LP problem.

virtual void	addIndicatorConstraint (std::string const &name, Variable indicatorVariable, bool indicatorValue, Constraint const &constraint)=0
	Adds the given indicator constraint to the LP problem: "If indicatorVariable == indicatorValue, then constraint".

virtual void	optimize () const =0
	Optimizes the LP problem previously constructed.

virtual bool	isInfeasible () const =0
	Retrieves whether the model was found to be infeasible.

virtual bool	isUnbounded () const =0
	Retrieves whether the model was found to be infeasible.

virtual bool	isOptimal () const =0
	Retrieves whether the model was found to be optimal, i.e.

virtual int_fast64_t	getIntegerValue (Variable const &variable) const =0
	Retrieves the value of the integer variable with the given name.

virtual bool	getBinaryValue (Variable const &variable) const =0
	Retrieves the value of the binary variable with the given name.

virtual ValueType	getContinuousValue (Variable const &variable) const =0
	Retrieves the value of the continuous variable with the given name.

virtual ValueType	getObjectiveValue () const =0
	Retrieves the value of the objective function.

virtual void	writeModelToFile (std::string const &filename) const =0
	Writes the current LP problem to the given file.

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.

virtual void	push ()=0
	Pushes a backtracking point on the solver's stack.

virtual void	pop ()=0
	Pops a backtracking point from the solver's stack.

virtual void	setMaximalMILPGap (ValueType const &gap, bool relative)=0
	Specifies the maximum difference between lower- and upper objective bounds that triggers termination.

virtual ValueType	getMILPGap (bool relative) const =0
	Returns the obtained gap after a call to optimize()

Protected Member Functions
storm::expressions::Variable	declareOrGetExpressionVariable (std::string const &name, VariableType const &type)

Protected Attributes
std::shared_ptr< storm::expressions::ExpressionManager >	manager

bool	currentModelHasBeenOptimized

Detailed Description

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

An interface that captures the functionality of an LP solver.

Template Parameters

RawMode If set, variables are given as indices and constraints as RawConstraints. This avoids overhead introduced by storm::expression's

Definition at line 51 of file LpSolver.h.

Member Typedef Documentation

◆ Constant

template<typename ValueType , bool RawMode = false>

using storm::solver::LpSolver< ValueType, RawMode >::Constant = std::conditional_t<RawMode, ValueType, storm::expressions::Expression>

Definition at line 54 of file LpSolver.h.

◆ Constraint

template<typename ValueType , bool RawMode = false>

using storm::solver::LpSolver< ValueType, RawMode >::Constraint = std::conditional_t<RawMode, RawLpConstraint<ValueType>, storm::expressions::Expression>

Definition at line 55 of file LpSolver.h.

◆ Variable

template<typename ValueType , bool RawMode = false>

using storm::solver::LpSolver< ValueType, RawMode >::Variable = std::conditional_t<RawMode, typename RawLpConstraint<ValueType>::VariableIndexType, storm::expressions::Variable>

Definition at line 53 of file LpSolver.h.

Member Enumeration Documentation

◆ VariableType

template<typename ValueType , bool RawMode = false>

enum class storm::solver::LpSolver::VariableType

strong

Enumerates the different types of variables.

Enumerator
Continuous
Integer
Binary

Definition at line 60 of file LpSolver.h.

Constructor & Destructor Documentation

◆ LpSolver() [1/2]

template<typename ValueType , bool RawMode>

storm::solver::LpSolver< ValueType, RawMode >::LpSolver ( )

Creates an empty LP solver.

By default the objective function is assumed to be minimized.

Definition at line 26 of file LpSolver.cpp.

◆ LpSolver() [2/2]

template<typename ValueType , bool RawMode>

storm::solver::LpSolver< ValueType, RawMode >::LpSolver ( OptimizationDirection const & optDir )

Creates an empty LP solver with the given model sense.

Parameters

optDir A value indicating whether the objective function of this model is to be minimized or maximized.

Definition at line 32 of file LpSolver.cpp.

◆ ~LpSolver()

template<typename ValueType , bool RawMode = false>

virtual storm::solver::LpSolver< ValueType, RawMode >::~LpSolver ( )

virtualdefault

Member Function Documentation

◆ addBinaryVariable()

template<typename ValueType , bool RawMode>

LpSolver< ValueType, RawMode >::Variable storm::solver::LpSolver< ValueType, RawMode >::addBinaryVariable	(	std::string const &	name,
		ValueType	objectiveFunctionCoefficient = `0`
	)

Registers a boolean variable, i.e.

a variable that may be either 0 or 1.

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

name	The name of the variable.
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.

Definition at line 103 of file LpSolver.cpp.

◆ addBoundedContinuousVariable()

template<typename ValueType , bool RawMode>

LpSolver< ValueType, RawMode >::Variable storm::solver::LpSolver< ValueType, RawMode >::addBoundedContinuousVariable	(	std::string const &	name,
		ValueType	lowerBound,
		ValueType	upperBound,
		ValueType	objectiveFunctionCoefficient = `0`
	)

Registers an upper- and lower-bounded continuous variable, i.e.

a variable that may take all real values within its bounds.

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

name	The name of the variable.
lowerBound	The lower bound of the variable.
upperBound	The upper bound of the variable.
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.

Definition at line 38 of file LpSolver.cpp.

◆ addBoundedIntegerVariable()

template<typename ValueType , bool RawMode>

LpSolver< ValueType, RawMode >::Variable storm::solver::LpSolver< ValueType, RawMode >::addBoundedIntegerVariable	(	std::string const &	name,
		ValueType	lowerBound,
		ValueType	upperBound,
		ValueType	objectiveFunctionCoefficient = `0`
	)

Registers an upper- and lower-bounded integer variable, i.e.

a variable that may take all integer values within its bounds.

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

name	The name of the variable.
lowerBound	The lower bound of the variable.
upperBound	The upper bound of the variable.
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.

Definition at line 71 of file LpSolver.cpp.

◆ addConstraint()

template<typename ValueType , bool RawMode = false>

virtual void storm::solver::LpSolver< ValueType, RawMode >::addConstraint	(	std::string const &	name,
		Constraint const &	constraint
	)

pure virtual

Adds a the given constraint to the LP problem.

Parameters

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.

Implemented in storm::solver::GurobiLpSolver< ValueType, RawMode >, storm::solver::SoplexLpSolver< ValueType, RawMode >, and storm::solver::Z3LpSolver< ValueType, RawMode >.

◆ addContinuousVariable()

template<typename ValueType , bool RawMode>

LpSolver< ValueType, RawMode >::Variable storm::solver::LpSolver< ValueType, RawMode >::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.

a variable that may take all real values within its bounds (if given).

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

name	The name of the variable.
lowerBound	The lower bound of the variable (unbounded if not given).
upperBound	The upper bound of the variable (unbounded if not given).
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.

Definition at line 63 of file LpSolver.cpp.

◆ addIndicatorConstraint()

template<typename ValueType , bool RawMode = false>

virtual void storm::solver::LpSolver< ValueType, RawMode >::addIndicatorConstraint	(	std::string const &	name,
		Variable	indicatorVariable,
		bool	indicatorValue,
		Constraint const &	constraint
	)

pure virtual

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

Parameters

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.

Implemented in storm::solver::GurobiLpSolver< ValueType, RawMode >, storm::solver::SoplexLpSolver< ValueType, RawMode >, and storm::solver::Z3LpSolver< ValueType, RawMode >.

◆ addIntegerVariable()

template<typename ValueType , bool RawMode>

LpSolver< ValueType, RawMode >::Variable storm::solver::LpSolver< ValueType, RawMode >::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.

a variable that may take all integer values within its bounds (if given).

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

name	The name of the variable.
lowerBound	The lower bound of the variable.
upperBound	The upper bound of the variable.
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.

Definition at line 96 of file LpSolver.cpp.

◆ addLowerBoundedContinuousVariable()

template<typename ValueType , bool RawMode>

LpSolver< ValueType, RawMode >::Variable storm::solver::LpSolver< ValueType, RawMode >::addLowerBoundedContinuousVariable	(	std::string const &	name,
		ValueType	lowerBound,
		ValueType	objectiveFunctionCoefficient = `0`
	)

Registers a lower-bounded continuous variable, i.e.

a variable that may take all real values up to its lower bound.

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

name	The name of the variable.
lowerBound	The lower bound of the variable.
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.

Definition at line 45 of file LpSolver.cpp.

◆ addLowerBoundedIntegerVariable()

template<typename ValueType , bool RawMode>

LpSolver< ValueType, RawMode >::Variable storm::solver::LpSolver< ValueType, RawMode >::addLowerBoundedIntegerVariable	(	std::string const &	name,
		ValueType	lowerBound,
		ValueType	objectiveFunctionCoefficient = `0`
	)

Registers a lower-bounded integer variable, i.e.

a variable that may take all integer values up to its lower bound.

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

name	The name of the variable.
lowerBound	The lower bound of the variable.
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.

Definition at line 78 of file LpSolver.cpp.

◆ addUnboundedContinuousVariable()

template<typename ValueType , bool RawMode>

LpSolver< ValueType, RawMode >::Variable storm::solver::LpSolver< ValueType, RawMode >::addUnboundedContinuousVariable	(	std::string const &	name,
		ValueType	objectiveFunctionCoefficient = `0`
	)

Registers a unbounded continuous variable, i.e.

a variable that may take all real values.

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

name	The name of the variable.
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.

Definition at line 57 of file LpSolver.cpp.

◆ addUnboundedIntegerVariable()

template<typename ValueType , bool RawMode>

LpSolver< ValueType, RawMode >::Variable storm::solver::LpSolver< ValueType, RawMode >::addUnboundedIntegerVariable	(	std::string const &	name,
		ValueType	objectiveFunctionCoefficient = `0`
	)

Registers an unbounded integer variable, i.e.

a variable that may take all integer values.

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

name	The name of the variable.
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.

Definition at line 90 of file LpSolver.cpp.

◆ addUpperBoundedContinuousVariable()

template<typename ValueType , bool RawMode>

LpSolver< ValueType, RawMode >::Variable storm::solver::LpSolver< ValueType, RawMode >::addUpperBoundedContinuousVariable	(	std::string const &	name,
		ValueType	upperBound,
		ValueType	objectiveFunctionCoefficient = `0`
	)

Registers an upper-bounded continuous variable, i.e.

a variable that may take all real values up to its upper bound.

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

name	The name of the variable.
upperBound	The upper bound of the variable.
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.

Definition at line 51 of file LpSolver.cpp.

◆ addUpperBoundedIntegerVariable()

template<typename ValueType , bool RawMode>

LpSolver< ValueType, RawMode >::Variable storm::solver::LpSolver< ValueType, RawMode >::addUpperBoundedIntegerVariable	(	std::string const &	name,
		ValueType	upperBound,
		ValueType	objectiveFunctionCoefficient = `0`
	)

Registers an upper-bounded integer variable, i.e.

a variable that may take all integer values up to its lower bound.

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

name	The name of the variable.
upperBound	The upper bound of the variable.
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.

Definition at line 84 of file LpSolver.cpp.

◆ addVariable()

template<typename ValueType , bool RawMode = false>

virtual Variable storm::solver::LpSolver< 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`
	)

pure virtual

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

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.

Implemented in storm::solver::GurobiLpSolver< ValueType, RawMode >, storm::solver::SoplexLpSolver< ValueType, RawMode >, and storm::solver::Z3LpSolver< ValueType, RawMode >.

◆ declareOrGetExpressionVariable()

template<typename ValueType , bool RawMode>

storm::expressions::Variable storm::solver::LpSolver< ValueType, RawMode >::declareOrGetExpressionVariable	(	std::string const &	name,
		VariableType const &	type
	)

protected

Definition at line 137 of file LpSolver.cpp.

◆ getBinaryValue()

template<typename ValueType , bool RawMode = false>

virtual bool storm::solver::LpSolver< ValueType, RawMode >::getBinaryValue ( Variable const & variable ) const

pure virtual

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

variable The variable whose integer value (in the optimal solution) to retrieve.

Returns: The value of the binary variable in the optimal solution.

Implemented in storm::solver::GurobiLpSolver< ValueType, RawMode >, storm::solver::SoplexLpSolver< ValueType, RawMode >, and storm::solver::Z3LpSolver< ValueType, RawMode >.

◆ getConstant()

template<typename ValueType , bool RawMode>

LpSolver< ValueType, RawMode >::Constant storm::solver::LpSolver< ValueType, RawMode >::getConstant ( ValueType value ) const

Retrieves an expression that characterizes the given constant value.

In RawMode, this just returns the given value

Parameters

value The value of the constant.

Returns: The resulting expression.

Definition at line 109 of file LpSolver.cpp.

◆ getContinuousValue()

template<typename ValueType , bool RawMode = false>

virtual ValueType storm::solver::LpSolver< ValueType, RawMode >::getContinuousValue ( Variable const & variable ) const

pure virtual

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

variable The variable whose integer value (in the optimal solution) to retrieve.

Returns: The value of the continuous variable in the optimal solution.

Implemented in storm::solver::GurobiLpSolver< ValueType, RawMode >, storm::solver::SoplexLpSolver< ValueType, RawMode >, and storm::solver::Z3LpSolver< ValueType, RawMode >.

◆ getIntegerValue()

template<typename ValueType , bool RawMode = false>

virtual int_fast64_t storm::solver::LpSolver< ValueType, RawMode >::getIntegerValue ( Variable const & variable ) const

pure virtual

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

variable The variable whose integer value (in the optimal solution) to retrieve.

Returns: The value of the integer variable in the optimal solution.

Implemented in storm::solver::GurobiLpSolver< ValueType, RawMode >, storm::solver::SoplexLpSolver< ValueType, RawMode >, and storm::solver::Z3LpSolver< ValueType, RawMode >.

◆ getManager()

template<typename ValueType , bool RawMode>

storm::expressions::ExpressionManager const & storm::solver::LpSolver< ValueType, RawMode >::getManager ( ) const

Retrieves the manager for the variables created for this solver.

Returns: The manager for the variables created for this solver.

Definition at line 131 of file LpSolver.cpp.

◆ getMILPGap()

template<typename ValueType , bool RawMode = false>

virtual ValueType storm::solver::LpSolver< ValueType, RawMode >::getMILPGap ( bool relative ) const

pure virtual

Returns the obtained gap after a call to optimize()

Implemented in storm::solver::GlpkLpSolver, storm::solver::GlpkLpSolver, storm::solver::GurobiLpSolver< ValueType, RawMode >, storm::solver::SoplexLpSolver< ValueType, RawMode >, and storm::solver::Z3LpSolver< ValueType, RawMode >.

◆ getObjectiveValue()

template<typename ValueType , bool RawMode = false>

virtual ValueType storm::solver::LpSolver< ValueType, RawMode >::getObjectiveValue ( ) const

pure virtual

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.

Implemented in storm::solver::GlpkLpSolver, storm::solver::GurobiLpSolver< ValueType, RawMode >, storm::solver::SoplexLpSolver< ValueType, RawMode >, and storm::solver::Z3LpSolver< ValueType, RawMode >.

◆ getOptimizationDirection()

template<typename ValueType , bool RawMode>

OptimizationDirection storm::solver::LpSolver< ValueType, RawMode >::getOptimizationDirection ( ) const

Retrieves whether the objective function of this model is to be minimized or maximized.

Returns: A value indicating whether the objective function of this model is to be minimized or maximized.

Definition at line 126 of file LpSolver.cpp.

◆ isInfeasible()

template<typename ValueType , bool RawMode = false>

virtual bool storm::solver::LpSolver< ValueType, RawMode >::isInfeasible ( ) const

pure virtual

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.

Implemented in storm::solver::GlpkLpSolver, storm::solver::GurobiLpSolver< ValueType, RawMode >, storm::solver::SoplexLpSolver< ValueType, RawMode >, and storm::solver::Z3LpSolver< ValueType, RawMode >.

◆ isOptimal()

template<typename ValueType , bool RawMode = false>

virtual bool storm::solver::LpSolver< ValueType, RawMode >::isOptimal ( ) const

pure virtual

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.

Implemented in storm::solver::GlpkLpSolver, storm::solver::GurobiLpSolver< ValueType, RawMode >, storm::solver::SoplexLpSolver< ValueType, RawMode >, and storm::solver::Z3LpSolver< ValueType, RawMode >.

◆ isUnbounded()

template<typename ValueType , bool RawMode = false>

virtual bool storm::solver::LpSolver< ValueType, RawMode >::isUnbounded ( ) const

pure virtual

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.

Implemented in storm::solver::GlpkLpSolver, storm::solver::GurobiLpSolver< ValueType, RawMode >, storm::solver::SoplexLpSolver< ValueType, RawMode >, and storm::solver::Z3LpSolver< ValueType, RawMode >.

◆ optimize()

template<typename ValueType , bool RawMode = false>

virtual void storm::solver::LpSolver< ValueType, RawMode >::optimize ( ) const

pure virtual

Optimizes the LP problem previously constructed.

Afterwards, the methods isInfeasible, isUnbounded and isOptimal can be used to query the optimality status.

Implemented in storm::solver::GlpkLpSolver, storm::solver::GurobiLpSolver< ValueType, RawMode >, storm::solver::SoplexLpSolver< ValueType, RawMode >, and storm::solver::Z3LpSolver< ValueType, RawMode >.

◆ pop()

template<typename ValueType , bool RawMode = false>

virtual void storm::solver::LpSolver< ValueType, RawMode >::pop ( )

pure virtual

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().

Implemented in storm::solver::GlpkLpSolver, storm::solver::GurobiLpSolver< ValueType, RawMode >, storm::solver::SoplexLpSolver< ValueType, RawMode >, and storm::solver::Z3LpSolver< ValueType, RawMode >.

◆ push()

template<typename ValueType , bool RawMode = false>

virtual void storm::solver::LpSolver< ValueType, RawMode >::push ( )

pure virtual

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.

Implemented in storm::solver::GlpkLpSolver, storm::solver::GurobiLpSolver< ValueType, RawMode >, storm::solver::SoplexLpSolver< ValueType, RawMode >, and storm::solver::Z3LpSolver< ValueType, RawMode >.

◆ setMaximalMILPGap()

template<typename ValueType , bool RawMode = false>

virtual void storm::solver::LpSolver< ValueType, RawMode >::setMaximalMILPGap	(	ValueType const &	gap,
		bool	relative
	)

pure virtual

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.

Implemented in storm::solver::GurobiLpSolver< ValueType, RawMode >, storm::solver::SoplexLpSolver< ValueType, RawMode >, and storm::solver::Z3LpSolver< ValueType, RawMode >.

◆ setOptimizationDirection()

template<typename ValueType , bool RawMode>

void storm::solver::LpSolver< ValueType, RawMode >::setOptimizationDirection ( OptimizationDirection const & optimizationDirection )

Sets whether the objective function of this model is to be minimized or maximized.

Parameters

modelSense The model sense to use.

Definition at line 118 of file LpSolver.cpp.

◆ update()

template<typename ValueType , bool RawMode = false>

virtual void storm::solver::LpSolver< ValueType, RawMode >::update ( ) const

pure virtual

Updates the model to make the variables that have been declared since the last call to update usable.

Implemented in storm::solver::GlpkLpSolver, storm::solver::GurobiLpSolver< ValueType, RawMode >, storm::solver::SoplexLpSolver< ValueType, RawMode >, and storm::solver::Z3LpSolver< ValueType, RawMode >.

◆ writeModelToFile()

template<typename ValueType , bool RawMode = false>

virtual void storm::solver::LpSolver< ValueType, RawMode >::writeModelToFile ( std::string const & filename ) const

pure virtual

Writes the current LP problem to the given file.

Parameters

filename The file to which to write the string representation of the LP.

Implemented in storm::solver::GlpkLpSolver, storm::solver::GurobiLpSolver< ValueType, RawMode >, storm::solver::SoplexLpSolver< ValueType, RawMode >, and storm::solver::Z3LpSolver< ValueType, RawMode >.

Member Data Documentation

◆ currentModelHasBeenOptimized

template<typename ValueType , bool RawMode = false>

bool storm::solver::LpSolver< ValueType, RawMode >::currentModelHasBeenOptimized

mutableprotected

Definition at line 394 of file LpSolver.h.

◆ manager

template<typename ValueType , bool RawMode = false>

std::shared_ptr<storm::expressions::ExpressionManager> storm::solver::LpSolver< ValueType, RawMode >::manager

protected

Definition at line 391 of file LpSolver.h.

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

src/storm/solver/LpSolver.h
src/storm/solver/LpSolver.cpp

Public Types

Public Member Functions

Protected Member Functions

Protected Attributes

Detailed Description

Member Typedef Documentation

◆ Constant

◆ Constraint

◆ Variable

Member Enumeration Documentation

◆ VariableType

Constructor & Destructor Documentation

◆ LpSolver() [1/2]

◆ LpSolver() [2/2]

◆ ~LpSolver()

Member Function Documentation

◆ addBinaryVariable()

◆ addBoundedContinuousVariable()

◆ addBoundedIntegerVariable()

◆ addConstraint()

◆ addContinuousVariable()

◆ addIndicatorConstraint()

◆ addIntegerVariable()

◆ addLowerBoundedContinuousVariable()

◆ addLowerBoundedIntegerVariable()

◆ addUnboundedContinuousVariable()

◆ addUnboundedIntegerVariable()

◆ addUpperBoundedContinuousVariable()

◆ addUpperBoundedIntegerVariable()

◆ addVariable()

◆ declareOrGetExpressionVariable()

◆ getBinaryValue()

◆ getConstant()

◆ getContinuousValue()

◆ getIntegerValue()

◆ getManager()

◆ getMILPGap()

◆ getObjectiveValue()

◆ getOptimizationDirection()

◆ isInfeasible()

◆ isOptimal()

◆ isUnbounded()

◆ optimize()

◆ pop()

◆ push()

◆ setMaximalMILPGap()

◆ setOptimizationDirection()

◆ update()

◆ writeModelToFile()

Member Data Documentation

◆ currentModelHasBeenOptimized

◆ manager