Facade class that hides the underlying LP solver used by delpi. More...

#include <LpSolver.h>

Inheritance diagram for delpi::LpSolver:

Public Types
using	SolveCallback
	Callback invoked by the LP solver when a solution (or delta solution) is found.
using	PartialSolveCallback
	Callback invoked by the LP solver when a solution (or delta solution) is found.

Public Member Functions
	LpSolver (mpq_class ninfinity, mpq_class infinity, Config config={}, const std::string &class_name="LpSolver")
	Construct a new LpSolver object with the given config.
bool	Parse ()
	Parse the input file or stdin based on the Config parameters.
bool	ParseFile (const std::string &filename)
	Parse the file with the given filename.
bool	ParseString (const std::string &string)
	Parse the given string as input.
bool	ParseStream (std::istream &stream, const std::string &stream_name="(stdin)")
	Parse the given stream as input.
const std::unordered_map< std::string, std::string > &	info () const
	@getter{information stored in the LP solver}
std::unordered_map< Variable, mpq_class >	model (const std::vector< mpq_class > &x) const
	Get a mapping between the variables and their values in the solution vector x.
const mpq_class &	solution (const Variable var) const
	Get the value of var in the solution vector.
const Variable &	var (const int column) const
	Shorthand notation to get the real variable linked with column column.
virtual Column	column (int column_idx) const =0
	Get the column at the given column_idx index.
virtual Row	row (int row_idx) const =0
	Get the row at the given row_idx index.
virtual void	ReserveColumns (int size)
	Reserve space for the given number of columns and rows.
virtual void	ReserveRows (int size)
	Reserve space for the given number of rows.
const std::string &	GetInfo (const std::string &key) const
	Retrieve the information stored under the given key.
void	SetInfo (const std::string &key, const std::string &value)
	Set the information stored under the given key to the given value.
void	SetOption (const std::string &key, const std::string &value)
	Set the option identified by the given key to the given value.
virtual void	AddColumns (const std::span< Column > &columns)
	Add a vector of columns to the LP problem.
ColumnIndex	AddColumn (const Column &column)
	Add a new column to the LP problem.
ColumnIndex	AddColumn (const Variable &var)
	Add a new unbounded column corresponding to the variable var to the LP problem.
ColumnIndex	AddColumn (const Variable &var, const mpq_class &obj)
	Add a new column to the LP problem setting the objective coefficient of var to the given obj.
ColumnIndex	AddColumn (const Variable &var, const mpq_class &lb, const mpq_class &ub)
	Add a new bounded column to the LP problem, ensuring that the variable var is in the range \( [lb, ub] \).
virtual ColumnIndex	AddColumn (const Variable &var, const mpq_class &obj, const mpq_class &lb, const mpq_class &ub)=0
	Add a new bounded column to the LP problem, ensuring that the variable var is in the range \( [lb, ub] \) and has the objective coefficient obj.
virtual void	AddRows (const std::span< Row > &rows)
	Add a vector of rows to the LP problem.
RowIndex	AddRow (const Row &row)
	Add a new row to the LP problem with the given row.
virtual RowIndex	AddRow (const std::vector< std::pair< Variable, mpq_class > > &addends, const mpq_class &lb, const mpq_class &ub)=0
	Add a new row to the LP problem with the given addends bounded by lb and ub.
RowIndex	AddRow (const Formula &formula)
	Add a new row to the LP problem with the given formula.
RowIndex	AddRow (const Expression &lhs, FormulaKind sense, const mpq_class &rhs)
	Add a new row to the LP problem with the given lhs linear expression, sense and rhs.
virtual RowIndex	AddRow (const Expression::Addends &lhs, FormulaKind sense, const mpq_class &rhs)=0
	Add a new row to the LP problem with the given lhs linear summation, sense and rhs.
virtual void	SetCoefficient (RowIndex row, ColumnIndex column, const mpq_class &value)=0
	Set the coefficient of the row constraint to apply at the column decisional variable.
void	SetObjective (const Expression &objective)
	Set the objective coefficients of the LP problem to the given objective.
void	SetObjective (const std::unordered_map< int, mpq_class > &objective)
	Set the objective coefficients of the LP problem to the given objective.
void	SetObjective (const std::vector< mpq_class > &objective)
	Set the objective coefficients of the LP problem to the given objective.
void	SetObjective (const Variable &var, const mpq_class &value)
	The the objective coefficient of the column corresponding to the give var to the given value.
virtual void	SetObjective (int column, const mpq_class &value)=0
	The the objective coefficient of the given column to the given value.
virtual void	SetBound (Variable var, const mpq_class &lb, const mpq_class &ub)=0
	Set the bounds of a var in the LP problem to the given lb and ub.
LpResult	Solve ()
	Optimise the LP problem with the given delta.
void	Maximise (const Expression &objective_function)
	Set the objective_function to maximise while being subject to all the constraints.
template<TypedIterable< std::pair< const Variable, mpq_class > > T>
void	Maximise (const T &objective_function)
	Set the objective_function to maximise while being subject to all the constraints.
void	Minimise (const Expression &objective_function)
	Set the objective_function to minimise while being subject to all the constraints.
template<TypedIterable< std::pair< const Variable, mpq_class > > T>
void	Minimise (const T &objective_function)
	Set the objective_function to maximise while being subject to all the constraints.
void	ResetObjective ()
	Set all coefficients in the objective function to zero.
bool	CheckAgainstExpected (LpResult result) const
	Check whether the result obtained by the solver is compatible with the one collected from the file.
bool	Verify () const
	Verify that the current solution_ satisfies all the constraints in the LpSolver.

Protected Member Functions
void	EnsureSense (bool is_min)
	Make sure the LP solvers are aware of the sense of the LP problem (minimisation or maximisation).
virtual void	EnsureSenseCore ()=0
	Make sure the LP solvers are aware of the sense of the LP problem (minimisation or maximisation).
virtual LpResult	SolveCore ()=0
	Internal method that optimises the LP problem with the given delta.
bool	SetSimpleBoundInsteadOfAddRow (const std::vector< Expression::Addend > &addends, const mpq_class &lb, const mpq_class &ub)
	Check whether the row that is about to be added is a simple bound.

Protected Attributes
Config	config_
	Configuration to use.
LpStats	stats_
	Statistics of the solver.
std::unordered_map< std::string, std::string >	info_
	Generic information map. Generally collected from the file.
std::unordered_map< Variable, int >	var_to_col_
	Theory column ⇔ Variable.
std::vector< Variable >	col_to_var_
	Literal ⇔ lp row.
std::vector< mpq_class >	solution_
	Solution vector.
std::vector< mpq_class >	dual_solution_
	Dual solution vector.
mpq_class	obj_lb_
	Lower bound on the objective value, if any.
mpq_class	obj_ub_
	Upper bound on the objective value, if any.
SolveCallback	solve_cb_
	Callback to call after solving the LP problem.
PartialSolveCallback	partial_solve_cb_
	Callback to call after solving the LP problem with a partial solution.
bool	is_min_
	Whether this is a minimization or maximization LP problem.
mpq_class	ninfinity_
	Negative infinity threshold value.
mpq_class	infinity_
	Infinity threshold value.

Detailed Description

Facade class that hides the underlying LP solver used by delpi.

It provides a common interface to interact with any number of LP solvers, implemented as subclasses. An LP problem is defined as

\[\begin{array}{} & \max & c^T x \newline & \text{subject to} & A x \le b \newline & & l \le x \le u \end{array} \]

where \( x \) is the vector of real variables, \( c \) is the vector of objective coefficients, \( A \) is the matrix of coefficients of the constraints, \( b \) is the right-hand side of the constraints, \( l \) is the vector of lower bounds, and \( u \) is the vector of upper bounds.

If the problem is feasible, the solution vector \( x \) and the objective value are made available. Otherwise, the Farekas ray \( y \) is used to create the linear inequality \( (y^T A) x \le y^T b \), which is infeasible over the local bounds. In other words, even setting each element of \( x \) to the bound that minimise \( (y^A) x \), its value is still greater than \( y^T b \).

The usual workflow is as follows:

For each real variable in the SMT problem, add a linked column with AddColumn
For each symbolic formula in the SMT problem, add a linked row with AddRow
Optimise the LP problem with Solve
- If the problem is feasible, the solution is stored in solution_ and dual_solution_
- If the problem is infeasible, the Farekas ray is stored in dual_solution_

Definition at line 60 of file LpSolver.h.

Member Typedef Documentation

◆ PartialSolveCallback

using delpi::LpSolver::PartialSolveCallback

Initial value:

 
std::function<bool(const LpSolver& lp_solver, LpResult result, const std::vector<mpq_class>& x,
                   const std::vector<mpq_class>& y, const mpq_class& obj_lb, const mpq_class& obj_ub)>

Callback invoked by the LP solver when a solution (or delta solution) is found.

Parameters

lp_solver	LP solver that invoked the callback
result	result of the LP solver
x	solution vector
y	dual solution vector
obj_lb	lower bound of the objective
obj_ub	upper bound of the objective
diff	difference between the lower and upper bounds
delta	delta value
precision	precision (bits) used to obtain the solution

Returns: true if the solver should continue; false if the solver should stop

Definition at line 94 of file LpSolver.h.

◆ SolveCallback

using delpi::LpSolver::SolveCallback

Initial value:

 
std::function<void(const LpSolver& lp_solver, LpResult result, const std::vector<mpq_class>& x,
                   const std::vector<mpq_class>& y, const mpq_class& obj_lb, const mpq_class& obj_ub)>

Callback invoked by the LP solver when a solution (or delta solution) is found.

Parameters

lp_solver	LP solver that invoked the callback
result	result of the LP solver
x	solution vector
y	dual solution vector
obj_lb	lower bound of the objective
obj_ub	upper bound of the objective
delta	delta value
precision	precision (bits) used to obtain the solution

Returns: true if the solver should continue; false if the solver should stop

Definition at line 77 of file LpSolver.h.

Constructor & Destructor Documentation

◆ LpSolver()

delpi::LpSolver::LpSolver	(	mpq_class	ninfinity,
		mpq_class	infinity,
		Config	config = {},
		const std::string &	class_name = "LpSolver" )

Construct a new LpSolver object with the given config.

Parameters

ninfinity	negative infinity threshold value
infinity	infinity threshold value
config	configuration to use
class_name	name of the class

Definition at line 41 of file LpSolver.cpp.

Member Function Documentation

◆ AddColumn() [1/5]

LpSolver::ColumnIndex delpi::LpSolver::AddColumn ( const Column & column )

Add a new column to the LP problem.

Not indicating a column.lb or column.ub will result in an unbounded variable in that direction.

Warning: The objective coefficient is set with respect to a minimisation problem.

Parameters

column column to add to the LP problem

Returns: index of the last column added

Definition at line 88 of file LpSolver.cpp.

◆ AddColumn() [2/5]

LpSolver::ColumnIndex delpi::LpSolver::AddColumn ( const Variable & var )

Add a new unbounded column corresponding to the variable var to the LP problem.

Parameters

var	variable to add to the LP problem

Returns: index of the last column added

Definition at line 92 of file LpSolver.cpp.

◆ AddColumn() [3/5]

LpSolver::ColumnIndex delpi::LpSolver::AddColumn	(	const Variable &	var,
		const mpq_class &	lb,
		const mpq_class &	ub )

Add a new bounded column to the LP problem, ensuring that the variable var is in the range \( [lb, ub] \).

Parameters

var	variable to add to the LP problem
lb	lower bound of the column
ub	upper bound of the column

Returns: index of the last column added

Definition at line 102 of file LpSolver.cpp.

◆ AddColumn() [4/5]

LpSolver::ColumnIndex delpi::LpSolver::AddColumn	(	const Variable &	var,
		const mpq_class &	obj )

Add a new column to the LP problem setting the objective coefficient of var to the given obj.

Warning: The objective coefficient is set with respect to a minimisation problem.

Parameters

var	variable to add to the LP problem
obj	coefficient of the variable in the objective function for minimisation

Returns: index of the last column added

Definition at line 97 of file LpSolver.cpp.

◆ AddColumn() [5/5]

virtual ColumnIndex delpi::LpSolver::AddColumn	(	const Variable &	var,
		const mpq_class &	obj,
		const mpq_class &	lb,
		const mpq_class &	ub )

pure virtual

Add a new bounded column to the LP problem, ensuring that the variable var is in the range \( [lb, ub] \) and has the objective coefficient obj.

Warning: The objective coefficient is set with respect to a minimisation problem.

Parameters

var	variable to add to the LP problem
obj	objective coefficient of the column
lb	lower bound of the column
ub	upper bound of the column

Returns: index of the last column added

Implemented in delpi::DelpiLpSolver, delpi::QsoptexLpSolver, and delpi::SoplexLpSolver.

◆ AddColumns()

void delpi::LpSolver::AddColumns ( const std::span< Column > & columns )

virtual

Add a vector of columns to the LP problem.

Warning: The objective coefficient is set with respect to a minimisation problem.

Parameters

columns vector of columns to add to the LP problem

See also: AddColumn(const Column&)

Definition at line 218 of file LpSolver.cpp.

◆ AddRow() [1/5]

LpSolver::RowIndex delpi::LpSolver::AddRow	(	const Expression &	lhs,
		FormulaKind	sense,
		const mpq_class &	rhs )

Add a new row to the LP problem with the given lhs linear expression, sense and rhs.

The resulting row will be in the shape

\[lhs \text{ sense } rhs \]

where \( lhs \) is a linear expression, \( \text{ sense } \in \\{ \le, =, \ge \\} \) and \( rhs \) is a constant.

Parameters

lhs	linear expression on the left-hand side of the row
sense	sense of the row (i.e. \( \le, =, \ge \))
rhs	constant on the right-hand side of the row

Definition at line 118 of file LpSolver.cpp.

◆ AddRow() [2/5]

virtual RowIndex delpi::LpSolver::AddRow	(	const Expression::Addends &	lhs,
		FormulaKind	sense,
		const mpq_class &	rhs )

pure virtual

Add a new row to the LP problem with the given lhs linear summation, sense and rhs.

The resulting row will be in the shape

\[lhs \text{ sense } rhs \]

where \( lhs \) is a linear expression, \( \text{ sense } \in \\{ \le, =, \ge \\} \) and \( rhs \) is a constant.

Parameters

lhs	linear summation on the left-hand side of the row
sense	sense of the row (i.e. <=, =, >=)
rhs	right-hand side of the row

Implemented in delpi::DelpiLpSolver, delpi::QsoptexLpSolver, and delpi::SoplexLpSolver.

◆ AddRow() [3/5]

LpSolver::RowIndex delpi::LpSolver::AddRow ( const Formula & formula )

Add a new row to the LP problem with the given formula.

Parameters

formula symbolic formula representing a constraint to add as a row

Definition at line 115 of file LpSolver.cpp.

◆ AddRow() [4/5]

LpSolver::RowIndex delpi::LpSolver::AddRow ( const Row & row )

Add a new row to the LP problem with the given row.

Not indicating a row.lb or row.ub will result in an unbounded row in that direction. If row.lb and row.ub are equal, a single equality constraint is added. Otherwise, a pair of inequality constraints may be added, depending on the underlying solver implementation.

Parameters

row	structure of the row to add

Returns: index of the last row added

Definition at line 112 of file LpSolver.cpp.

◆ AddRow() [5/5]

virtual RowIndex delpi::LpSolver::AddRow	(	const std::vector< std::pair< Variable, mpq_class > > &	addends,
		const mpq_class &	lb,
		const mpq_class &	ub )

pure virtual

Add a new row to the LP problem with the given addends bounded by lb and ub.

If lb and ub are equal, a single equality constraint is added. Otherwise, a pair of inequality constraints may be added, depending on the underlying solver implementation.

Parameters

addends	vector of pairs (Variable, coeff) that represent the linear summation of the row
lb	lower bound of the row
ub	upper bound of the row

Returns: index of the last row added

◆ AddRows()

void delpi::LpSolver::AddRows ( const std::span< Row > & rows )

virtual

Add a vector of rows to the LP problem.

Parameters

rows	vector of rows to add to the LP problem

See also: AddRow(const Row&)

Definition at line 108 of file LpSolver.cpp.

◆ CheckAgainstExpected()

bool delpi::LpSolver::CheckAgainstExpected ( LpResult result ) const

nodiscard

Check whether the result obtained by the solver is compatible with the one collected from the file.

Parameters

result result obtained by the solver

Returns: true if the result obtained by the solver is compatible with the one collected from the file; false if the result obtained by the solver is incompatible with the one collected from the file

Definition at line 243 of file LpSolver.cpp.

◆ column()

virtual Column delpi::LpSolver::column ( int column_idx ) const

nodiscardpure virtual

Get the column at the given column_idx index.

Parameters

column_idx index of the column to get

Returns: column structure

Implemented in delpi::DelpiLpSolver, delpi::QsoptexLpSolver, and delpi::SoplexLpSolver.

◆ EnsureSense()

void delpi::LpSolver::EnsureSense ( bool is_min )

protected

Make sure the LP solvers are aware of the sense of the LP problem (minimisation or maximisation).

Parameters

is_min new sense

Definition at line 271 of file LpSolver.cpp.

◆ GetInfo()

const std::string & delpi::LpSolver::GetInfo ( const std::string & key ) const

Retrieve the information stored under the given key.

Parameters

key	key of the information to get

Returns: information stored under the given key

Definition at line 164 of file LpSolver.cpp.

◆ Maximise() [1/2]

void delpi::LpSolver::Maximise ( const Expression & objective_function )

Set the objective_function to maximise while being subject to all the constraints.

The objective function coefficients will overwrite the current ones, if any.

Warning: The objective coefficient of variables not appearing in the objective_function is not altered.

Parameters

objective_function expression to maximise}

Definition at line 217 of file LpSolver.cpp.

◆ Maximise() [2/2]

template<TypedIterable< std::pair< const Variable, mpq_class > > T>

void delpi::LpSolver::Maximise ( const T & objective_function )

Set the objective_function to maximise while being subject to all the constraints.

The objective function coefficients will overwrite the current ones, if any.

Template Parameters

T	iterable of pairs (Variable, mpq_class) representing the objective function

Warning: The objective coefficient of variables not appearing in the objective_function is not altered.

Parameters

objective_function expression to maximise}

Definition at line 224 of file LpSolver.cpp.

◆ Minimise() [1/2]

void delpi::LpSolver::Minimise ( const Expression & objective_function )

Set the objective_function to minimise while being subject to all the constraints.

The objective function coefficients will overwrite the current ones, if any.

Warning: The objective coefficient of variables not appearing in the objective_function is not altered.

Parameters

objective_function expression to minimise

Definition at line 230 of file LpSolver.cpp.

◆ Minimise() [2/2]

template<TypedIterable< std::pair< const Variable, mpq_class > > T>

void delpi::LpSolver::Minimise ( const T & objective_function )

Set the objective_function to maximise while being subject to all the constraints.

The objective function coefficients will overwrite the current ones, if any.

Template Parameters

T	iterable of pairs (Variable, mpq_class) representing the objective function

Warning: The objective coefficient of variables not appearing in the objective_function is not altered.

Parameters

objective_function expression to maximise}

Definition at line 232 of file LpSolver.cpp.

◆ model()

std::unordered_map< Variable, mpq_class > delpi::LpSolver::model ( const std::vector< mpq_class > & x ) const

nodiscard

Get a mapping between the variables and their values in the solution vector x.

Parameters

x	solution vector

Returns: mapping between the variables and their values

Definition at line 79 of file LpSolver.cpp.

◆ Parse()

bool delpi::LpSolver::Parse ( )

Parse the input file or stdin based on the Config parameters.

All variables, constraints, bounds and objective are added to the LP solver.

Returns: true if the parsing was successful; false if the parsing failed

Definition at line 19 of file parser.cpp.

◆ ParseFile()

bool delpi::LpSolver::ParseFile ( const std::string & filename )

Parse the file with the given filename.

All variables, constraints, bounds and objective are added to the LP solver.

Parameters

filename path to the file to parse

Returns: true if the parsing was successful; false if the parsing failed

Definition at line 20 of file parser.cpp.

◆ ParseStream()

bool delpi::LpSolver::ParseStream	(	std::istream &	stream,
		const std::string &	stream_name = "(stdin)" )

Parse the given stream as input.

All variables, constraints, bounds and objective are added to the LP solver.

Parameters

stream	stream to parse
stream_name	name of the stream

Returns: true if the parsing was successful; false if the parsing failed

Definition at line 25 of file parser.cpp.

◆ ParseString()

bool delpi::LpSolver::ParseString ( const std::string & string )

Parse the given string as input.

All variables, constraints, bounds and objective are added to the LP solver.

Parameters

string string to parse

Returns: true if the parsing was successful; false if the parsing failed

Definition at line 32 of file parser.cpp.

◆ ReserveColumns()

void delpi::LpSolver::ReserveColumns ( int size )

virtual

Reserve space for the given number of columns and rows.

Can speed up the addition of columns if the guess is close to the actual number.

Parameters

size	number of columns to reserve

Reimplemented in delpi::DelpiLpSolver, and delpi::SoplexLpSolver.

Definition at line 159 of file LpSolver.cpp.

◆ ReserveRows()

void delpi::LpSolver::ReserveRows ( int size )

virtual

Reserve space for the given number of rows.

Can speed up the addition of rows if the guess is close to the actual number.

Parameters

size	number of rows to reserve

Reimplemented in delpi::DelpiLpSolver, and delpi::SoplexLpSolver.

Definition at line 162 of file LpSolver.cpp.

◆ row()

virtual Row delpi::LpSolver::row ( int row_idx ) const

nodiscardpure virtual

Get the row at the given row_idx index.

Parameters

row_idx index of the row to get

Returns: row structure

Implemented in delpi::DelpiLpSolver, delpi::QsoptexLpSolver, and delpi::SoplexLpSolver.

◆ SetBound()

virtual void delpi::LpSolver::SetBound	(	Variable	var,
		const mpq_class &	lb,
		const mpq_class &	ub )

pure virtual

Set the bounds of a var in the LP problem to the given lb and ub.

Parameters

var	variable to be bounded
lb	lower bound
ub	upper bound

Implemented in delpi::DelpiLpSolver, delpi::QsoptexLpSolver, and delpi::SoplexLpSolver.

◆ SetCoefficient()

virtual void delpi::LpSolver::SetCoefficient	(	RowIndex	row,
		ColumnIndex	column,
		const mpq_class &	value )

pure virtual

Set the coefficient of the row constraint to apply at the column decisional variable.

Parameters

row	row of the constraint
column	column containing the decisional variable to set the coefficient for
value	new value of the coefficient

Implemented in delpi::DelpiLpSolver, delpi::QsoptexLpSolver, and delpi::SoplexLpSolver.

◆ SetInfo()

void delpi::LpSolver::SetInfo	(	const std::string &	key,
		const std::string &	value )

Set the information stored under the given key to the given value.

Parameters

key	key of the information to set
value	value to set the information to set

Definition at line 165 of file LpSolver.cpp.

◆ SetObjective() [1/5]

void delpi::LpSolver::SetObjective ( const Expression & objective )

Set the objective coefficients of the LP problem to the given objective.

Parameters

objective expression of the objective coefficients

Definition at line 191 of file LpSolver.cpp.

◆ SetObjective() [2/5]

void delpi::LpSolver::SetObjective ( const std::unordered_map< int, mpq_class > & objective )

Set the objective coefficients of the LP problem to the given objective.

Parameters

objective map from column index to objective coefficient

Definition at line 195 of file LpSolver.cpp.

◆ SetObjective() [3/5]

void delpi::LpSolver::SetObjective ( const std::vector< mpq_class > & objective )

Set the objective coefficients of the LP problem to the given objective.

Parameters

objective

Definition at line 199 of file LpSolver.cpp.

◆ SetObjective() [4/5]

void delpi::LpSolver::SetObjective	(	const Variable &	var,
		const mpq_class &	value )

The the objective coefficient of the column corresponding to the give var to the given value.

Parameters

var	variable to set the objective for
value	new objective coefficient for the column

Definition at line 215 of file LpSolver.cpp.

◆ SetObjective() [5/5]

virtual void delpi::LpSolver::SetObjective	(	int	column,
		const mpq_class &	value )

pure virtual

The the objective coefficient of the given column to the given value.

Parameters

column	column to set the objective for
value	new objective coefficient for the column

Implemented in delpi::DelpiLpSolver, delpi::QsoptexLpSolver, and delpi::SoplexLpSolver.

◆ SetOption()

void delpi::LpSolver::SetOption	(	const std::string &	key,
		const std::string &	value )

Set the option identified by the given key to the given value.

The options will modify the Config of the LP solver. Boolean parameters will be set to true if the value is "yes", "true", "1", or "on" (case-insensitive) and false otherwise. Available options are:

:csv (bool): whether to output in CSV format
:silent (bool): whether to output nothing
:with-timings (bool): whether to output timings
:delta (double): delta parameter of the solver
:continuous-output (bool): whether to output continuously (at each delta-satisfying point)
:verbosity (int): verbosity level
:simplex-verbosity (int): verbosity level of the simplex solver
:produce-models (bool): whether to produce models
:timeout (int): timeout in milliseconds

Note that the spacing before the '*' is mandatory.

* @set-option :delta 0.505
* @set-option :produce-models false
ENDATA

Note: Parameters set from the command line will have precedence over the ones set in the input file.

Parameters

key	key of the option to set
value	value of the option

Definition at line 166 of file LpSolver.cpp.

◆ SetSimpleBoundInsteadOfAddRow()

bool delpi::LpSolver::SetSimpleBoundInsteadOfAddRow	(	const std::vector< Expression::Addend > &	addends,
		const mpq_class &	lb,
		const mpq_class &	ub )

protected

Check whether the row that is about to be added is a simple bound.

If that is the case, the LP solver should add a simple bound instead of a row. A simple bound is a constraint of the form \( l \le c \cdot x \le u \), where \( l \) and \( u \) are the lower and upper bounds of the variable \( x \) and \( c \) is a constant. Any other constraint should be added as a proper row.

Parameters

addends	linear summation of the row. If it only contains a single variable, it is a simple bound
lb	lower bound of the row
ub	upper bound of the row

Returns: true if the LP solver has added a simple bound instead of a row; false if the LP solver should add proper row

Definition at line 275 of file LpSolver.cpp.

◆ solution()

const mpq_class & delpi::LpSolver::solution ( const Variable var ) const

inlinenodiscard

Get the value of var in the solution vector.

Parameters

var	variable to get the value for

Returns: solution value of the variable

Definition at line 198 of file LpSolver.h.

◆ Solve()

LpResult delpi::LpSolver::Solve ( )

Optimise the LP problem with the given delta.

The result of the computation will be stored in solution_ and dual_solution_ if the problem is feasible. If store_solution is false, the solution will not be stored, but the LpResult will still be returned. The actual delta will be returned in the delta parameter.

Returns: OPTIMAL if an optimal solution has been found and the return value of delta is \( = 0 \); DELTA_OPTIMAL if an delta-optimal solution has been found and the return value of delta \(\ge 0 \); UNBOUNDED if the problem is unbounded; INFEASIBLE if the problem is infeasible; ERROR if an error occurred

Definition at line 203 of file LpSolver.cpp.

◆ SolveCore()

virtual LpResult delpi::LpSolver::SolveCore ( )

protectedpure virtual

Internal method that optimises the LP problem with the given delta.

Returns: OPTIMAL if an optimal solution has been found and the return value of delta is \( = 0 \); DELTA_OPTIMAL if a delta-optimal solution has been found and the return value of delta \(\ge 0 \); UNBOUNDED if the problem is unbounded; INFEASIBLE if the problem is infeasible; ERROR if an error occurred

Implemented in delpi::DelpiLpSolver, delpi::QsoptexLpSolver, and delpi::SoplexLpSolver.

◆ var()

const Variable & delpi::LpSolver::var ( const int column ) const

inlinenodiscard

Shorthand notation to get the real variable linked with column column.

Parameters

column index of the column the real variable is linked to

Returns: corresponding real variable

Definition at line 205 of file LpSolver.h.

◆ Verify()

bool delpi::LpSolver::Verify ( ) const

Verify that the current solution_ satisfies all the constraints in the LpSolver.

Returns: true if the current solution_ verifies all the constraints; false if at least one constraint is violated by the current solution_.

Definition at line 261 of file LpSolver.cpp.

Member Data Documentation

◆ col_to_var_

std::vector<Variable> delpi::LpSolver::col_to_var_

protected

Literal ⇔ lp row.

The literal is the one created by the PredicateAbstractor The row is the constraint used by the lp solver.

Definition at line 540 of file LpSolver.h.

◆ var_to_col_

std::unordered_map<Variable, int> delpi::LpSolver::var_to_col_

protected

Theory column ⇔ Variable.

The column is the one used by the lp solver. The Variable is the one created by the PredicateAbstractor

Definition at line 537 of file LpSolver.h.

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

delpi/solver/LpSolver.h
delpi/parser/parser.cpp
delpi/solver/LpSolver.cpp

Public Types

Public Member Functions

Protected Member Functions

Protected Attributes

Detailed Description

Member Typedef Documentation

◆ PartialSolveCallback

◆ SolveCallback

Constructor & Destructor Documentation

◆ LpSolver()

Member Function Documentation

◆ AddColumn() [1/5]

◆ AddColumn() [2/5]

◆ AddColumn() [3/5]

◆ AddColumn() [4/5]

◆ AddColumn() [5/5]

◆ AddColumns()

◆ AddRow() [1/5]

◆ AddRow() [2/5]

◆ AddRow() [3/5]

◆ AddRow() [4/5]

◆ AddRow() [5/5]

◆ AddRows()

◆ CheckAgainstExpected()

◆ column()

◆ EnsureSense()

◆ GetInfo()

◆ Maximise() [1/2]

◆ Maximise() [2/2]

◆ Minimise() [1/2]

◆ Minimise() [2/2]

◆ model()

◆ Parse()

◆ ParseFile()

◆ ParseStream()

◆ ParseString()

◆ ReserveColumns()

◆ ReserveRows()

◆ row()

◆ SetBound()

◆ SetCoefficient()

◆ SetInfo()

◆ SetObjective() [1/5]

◆ SetObjective() [2/5]

◆ SetObjective() [3/5]

◆ SetObjective() [4/5]

◆ SetObjective() [5/5]

◆ SetOption()

◆ SetSimpleBoundInsteadOfAddRow()

◆ solution()

◆ Solve()

◆ SolveCore()

◆ var()

◆ Verify()

Member Data Documentation

◆ col_to_var_

◆ var_to_col_