SoPlex is an exact LP solver written in C++. More...

#include <SoplexTheorySolver.h>

Inheritance diagram for dlinear::SoplexTheorySolver:

Public Member Functions
void	AddVariable (const Variable &var) override
	Add a variable (column) to the theory solver.

void	AddLiterals () override
	Add a vector of literals to the theory solver.

void	Consolidate (const Box &box) override
	Consolidate the solver.

void	Reset () override
	Reset the linear problem.

Public Member Functions inherited from dlinear::TheorySolver
	TheorySolver (const PredicateAbstractor &predicate_abstractor, const std::string &class_name="TheorySolver")
	Construct a new Theory Solver object.

virtual void	AddLiteral (const Variable &formula_var, const Formula &formula)=0
	Add a Literal to the theory solver.

virtual Explanations	PreprocessFixedLiterals (const LiteralSet &fixed_literals)
	Add the fixed literals to the theory solver.

Explanations	EnableLiterals (std::span< const Literal > theory_literals)
	Activate the literals that have previously been added to the theory solver.

virtual Explanations	EnableLiteral (const Literal &lit)=0
	Activate the literal that had previously been added to the theory solver.

const Box &	model () const
	Get read-only access to the model that satisfies all the constraints of the TheorySolver.

const Config &	config () const
	Get read-only access to the configuration of the TheorySolver.

const PredicateAbstractor &	predicate_abstractor () const
	Get read-only access to the predicate abstractor of the TheorySolver.

const std::map< Variable::Id, int > &	var_to_theory_col () const
	Get read-only access to the map of variables to the theory columns of the TheorySolver.

const std::vector< Variable > &	theory_col_to_var () const
	Get read-only access to the map of theory columns to the variables of the TheorySolver.

const std::map< Variable::Id, int > &	lit_to_theory_row () const
	Get read-only access to the map of literals to the theory rows of the TheorySolver.

const std::vector< Literal > &	theory_row_to_lit () const
	Get read-only access to the map of theory rows to the literals of the TheorySolver.

const BoundVectorMap &	theory_bounds () const
	Get read-only access to the bounds of each theory variable of the TheorySolver.

const BoundVectorMap &	fixed_theory_bounds () const
	Get read-only access to the fixed bounds of each theory variable of the TheorySolver.

const BoundPreprocessor &	preprocessor () const
	Get read-only access to the bound preprocessor of the TheorySolver.

BoundPreprocessor &	m_preprocessor ()
	Get read-write access to the bound preprocessor of the TheorySolver.

const BoundPreprocessor &	fixed_preprocessor () const
	Get read-only access to the fixed bound preprocessor of the TheorySolver.

BoundPreprocessor &	m_fixed_preprocessor ()
	Get read-write access to the fixed bound preprocessor of the TheorySolver.

std::size_t	theory_row_count () const
	Get read-only access to the number of rows of the TheorySolver.

std::size_t	theory_col_count () const
	Get read-only access to the number of columns of the TheorySolver.

std::set< Literal >	enabled_literals () const
	Get read-only access to the vector of enabled literals of the TheorySolver.

SatResult	CheckSat (const Box &box, mpq_class *actual_precision, std::set< LiteralSet > &explanations)
	Check the satisfiability of the theory.

virtual SatResult	CheckSatCore (mpq_class *actual_precision, std::set< LiteralSet > &explanations)=0
	Check the satisfiability of the theory.

const IterationStats &	stats () const
	Get the statistics of the theory solver.

Protected Member Functions
void	UpdateModelBounds () override
	Update each variable in the model with the bounds passed to the theory solver.

void	UpdateModelSolution () override
	Update the model with the solution obtained from the LP solver.

void	UpdateExplanation (LiteralSet &explanation) override
	Use the result from the theory solver to update the explanation with the conflict that has been detected.

virtual void	EnableSpxVarBound ()
	Set the bounds of the variables in the LP solver.

void	EnableSpxRow (int spx_row)
	Enable the `spx_row` row for the LP solver.

virtual void	EnableSpxRow (int spx_row, bool truth)=0
	Enable the `spx_row` row for the LP solver.

void	DisableSpxRows ()
	Disable all disabled spx rows from the LP solver.

soplex::DSVectorRational	ParseRowCoeff (const Formula &formula)
	Parse a `formula` and return the vector of coefficients to apply to the decisional variables.

void	SetSPXVarCoeff (soplex::DSVectorRational &coeffs, const Variable &var, const mpq_class &value) const
	Set the coefficients to apply to `var` on a specific row.

void	GetSpxInfeasibilityRay (soplex::VectorRational &farkas_ray)
	Get the infeasibility ray of the LP problem.

void	GetSpxInfeasibilityRay (soplex::VectorRational &farkas_ray, std::vector< BoundViolationType > &bounds_ray)
	Get the infeasibility rays of the LP problem.

std::vector< std::pair< int, soplex::Rational > >	GetActiveRows ()
	Get all active rows in the current solution.

std::vector< std::pair< int, soplex::Rational > >	GetActiveRows (const std::vector< int > &spx_rows)
	Get active rows in the current solution among the rows in `spx_rows`.

std::optional< soplex::Rational >	IsRowActive (int spx_row)
	Check if the `spx_row` is active.

bool	IsRowActive (int spx_row, const soplex::Rational &value)
	Check if the `spx_row` is active with value `value`.

Protected Member Functions inherited from dlinear::TheorySolver
void	UpdateExplanations (Explanations &explanations)
	Use the result from the theory solver to update the explanations with the conflict that has been detected.

Protected Attributes
soplex::SoPlex	spx_
	SoPlex exact LP solver.

soplex::LPColSetRational	spx_cols_
	Columns of the LP problem.

soplex::LPRowSetRational	spx_rows_
	Rows of the LP problem.

std::vector< mpq_class >	spx_rhs_
	Right-hand side of the rows.

std::vector< LpRowSense >	spx_sense_
	Sense of the rows.

Protected Attributes inherited from dlinear::TheorySolver
const Config &	config_
	Configuration of the theory solver.

bool	is_consolidated_
	Whether the solver has been consolidated.

const PredicateAbstractor &	predicate_abstractor_
	Predicate abstractor used to create the theory solver.

std::map< Variable::Id, int >	var_to_theory_col_
	Variable ⇔ theory column.

std::vector< Variable >	theory_col_to_var_
	Theory column ⇔ Variable.

std::map< Variable::Id, int >	lit_to_theory_row_
	Literal ⇔ theory row.

std::vector< Literal >	theory_row_to_lit_
	Theory row ⇔ Literal The row is the constraint used by the theory solver.

std::vector< bool >	theory_rows_state_
	Whether each theory row is enabled or not.

BoundPreprocessor	fixed_preprocessor_
	Preprocessor for the bounds. Only computed on fixed literal theories.

BoundPreprocessor	preprocessor_
	Preprocessor for the bounds.

Box	model_
	Model produced by the theory solver.

IterationStats	stats_
	Statistics of the theory solver.

Static Protected Attributes
static mpq_class	infinity_ {soplex::infinity}
	Positive infinity.

static mpq_class	ninfinity_ {-soplex::infinity}
	Negative infinity.

Additional Inherited Members
Public Types inherited from dlinear::TheorySolver
using	Bound = std::tuple<const Variable &, LpColBound, const mpq_class &>
	Bound on the variable.

using	Violation = BoundIterator
	Bound iterator over some violated bounds.

using	Explanations = std::set<LiteralSet>
	Set of explanations of the conflict.

Protected Types inherited from dlinear::TheorySolver
enum class	BoundViolationType { NO_BOUND_VIOLATION , LOWER_BOUND_VIOLATION , UPPER_BOUND_VIOLATION }
	Enum used to describe how the bounds on a variable participate in the infeasibility result of an LP problem. More...

Detailed Description

SoPlex is an exact LP solver written in C++.

It uses a mixture of techniques, from iterative refinement to precision boosting, in order to efficiently solve LPs exactly.

Definition at line 34 of file SoplexTheorySolver.h.

Member Function Documentation

◆ AddLiterals()

void dlinear::SoplexTheorySolver::AddLiterals ( )

overridevirtual

Add a vector of literals to the theory solver.

Each literal is formed by a variable that corresponds to a theory formula inside the PredicateAbstractor

Reimplemented from dlinear::TheorySolver.

Definition at line 52 of file SoplexTheorySolver.cpp.

◆ AddVariable()

void dlinear::SoplexTheorySolver::AddVariable ( const Variable & var )

overridevirtual

Add a variable (column) to the theory solver.

Parameters

var	variable to add

Implements dlinear::TheorySolver.

Definition at line 61 of file SoplexTheorySolver.cpp.

◆ Consolidate()

void dlinear::SoplexTheorySolver::Consolidate ( const Box & box )

overridevirtual

Consolidate the solver.

This method must be called after all the literals have been added to the solver and before calling any other method. Once the solver has been consolidated, no more literals can be added to it. A previously added literal can be enabled using the EnableLiteral method and disabled with Reset.

Note: A solver can be consolidated only once. If you need to change the variables or constraints, you must create a new theory solver.

Parameters

box	box with the bounds for the variables

Reimplemented from dlinear::TheorySolver.

Definition at line 219 of file SoplexTheorySolver.cpp.

◆ DisableSpxRows()

void dlinear::SoplexTheorySolver::DisableSpxRows ( )

protected

Disable all disabled spx rows from the LP solver.

Whether a row is disabled or not is determined by the theory_row_state_ field, where a true value means the row is enabled and a false value means the row is disabled.

Definition at line 317 of file SoplexTheorySolver.cpp.

◆ EnableSpxRow() [1/2]

void dlinear::SoplexTheorySolver::EnableSpxRow ( int spx_row )

protected

Enable the spx_row row for the LP solver.

The truth value and the free variables are collected from the state of the solver.

Precondition: The row's coefficients must have been set correctly before calling this function; The row's truth value must have been updated correctly; The row's free variables must have been updated correctly

Parameters

spx_row index of the row to enable

Definition at line 332 of file SoplexTheorySolver.cpp.

◆ EnableSpxRow() [2/2]

virtual void dlinear::SoplexTheorySolver::EnableSpxRow	(	int	spx_row,
		bool	truth )

protectedpure virtual

Enable the spx_row row for the LP solver.

Precondition: The row's coefficients must have been set correctly before calling this function

Parameters

spx_row	index of the row to enable
truth	truth value of the row

Implemented in dlinear::CompleteSoplexTheorySolver, dlinear::DeltaSoplexTheorySolver, and dlinear::NNSoplexTheorySolver.

◆ EnableSpxVarBound()

void dlinear::SoplexTheorySolver::EnableSpxVarBound ( )

protectedvirtual

Set the bounds of the variables in the LP solver.

Reimplemented in dlinear::CompleteSoplexTheorySolver.

Definition at line 323 of file SoplexTheorySolver.cpp.

◆ GetActiveRows() [1/2]

std::vector< std::pair< int, Rational > > dlinear::SoplexTheorySolver::GetActiveRows ( )

protected

Get all active rows in the current solution.

An active row is a row where the sum of the coefficients times the current solution is equal to either the lower or upper bound of the row.

Note: The problem must be feasible and a solution must have been found before calling this function.

Returns: vector of active rows with their value

Definition at line 76 of file SoplexTheorySolver.cpp.

◆ GetActiveRows() [2/2]

std::vector< std::pair< int, soplex::Rational > > dlinear::SoplexTheorySolver::GetActiveRows ( const std::vector< int > & spx_rows )

protected

Get active rows in the current solution among the rows in spx_rows.

An active row is a row where the sum of the coefficients times the current solution is equal to either the lower or upper bound of the row.

Note: The problem must be feasible and a solution must have been found before calling this function.

Parameters

spx_rows rows to check

Returns: vector of active rows among spx_rows with their value

Definition at line 90 of file SoplexTheorySolver.cpp.

◆ GetSpxInfeasibilityRay() [1/2]

void dlinear::SoplexTheorySolver::GetSpxInfeasibilityRay ( soplex::VectorRational & farkas_ray )

protected

Get the infeasibility ray of the LP problem.

This will return the Farkas ray, which can be used to find the infeasible core. The infeasible constraints will have the same indexes as the non-zero elements in the Farkas ray.

Note: The infeasible core is not guaranteed to be minimal

Precondition: The LP problem must be infeasible; farkas_ray.size() == num_rows

Parameters

[out] farkas_ray Farkas ray

Definition at line 188 of file SoplexTheorySolver.cpp.

◆ GetSpxInfeasibilityRay() [2/2]

void dlinear::SoplexTheorySolver::GetSpxInfeasibilityRay	(	soplex::VectorRational &	farkas_ray,
		std::vector< BoundViolationType > &	bounds_ray )

protected

Get the infeasibility rays of the LP problem.

This will return the Farkas ray and use it to compute the bounds ray. Combinind both it is possible to to find an even more precise infeasible core. The infeasible constraints will have the same indexes as the non-zero elements in the Farkas ray. Furthermore, given the Farkas ray \(y\), we get an infeasible linear inequality \(y^T A x \le y^T b\). Therefore, even setting \(x_i\) to the bound that minimises \(y^T A x\), that minimum is still \(> y^T b\), but tells which bound to include in the explanation.

Note: The infeasible core is not guaranteed to be minimal

Precondition: The LP problem must be infeasible; farkas_ray.size() == num_rows; bounds_ray.size() == num_cols - 1; All the element in bounds_ray must be BoundViolationType::NO_BOUND_VIOLATION

Parameters

[out]	farkas_ray	Farkas ray
[out]	bounds_ray	information about the bounds that are violated

Definition at line 195 of file SoplexTheorySolver.cpp.

◆ IsRowActive() [1/2]

std::optional< Rational > dlinear::SoplexTheorySolver::IsRowActive ( int spx_row )

protected

Check if the spx_row is active.

An active row is a row where the sum of the coefficients times the current solution is equal to either the lower or upper bound of the row.

Note: The problem must be feasible and a solution must have been found before calling this function.

Parameters

spx_row row to check

Returns: the value of the row if it is active; std::nullopt if the row is not active

Definition at line 104 of file SoplexTheorySolver.cpp.

◆ IsRowActive() [2/2]

bool dlinear::SoplexTheorySolver::IsRowActive	(	int	spx_row,
		const soplex::Rational &	value )

protected

Check if the spx_row is active with value value.

An active row is a row where the sum of the coefficients times the current solution is equal to either the lower or upper bound of the row. The value must be equal to value for the row to be considered active in this case.

Note: The problem must be feasible and a solution must have been found before calling this function.

Parameters

spx_row	row to check
value	value the row must be equal to in order to be considered active

Returns: true if the row is active with value value; false if the row is not active or if the value is not equal to value

◆ ParseRowCoeff()

soplex::DSVectorRational dlinear::SoplexTheorySolver::ParseRowCoeff ( const Formula & formula )

protected

Parse a formula and return the vector of coefficients to apply to the decisional variables.

It will store the rhs term in spx_rhs_ and create a vector of coefficients for the row.

Parameters

formula symbolic formula representing the row

Returns: vector of coefficients to apply to the decisional variables in the row

Definition at line 126 of file SoplexTheorySolver.cpp.

◆ Reset()

void dlinear::SoplexTheorySolver::Reset ( )

overridevirtual

Reset the linear problem.

All constraints' state will be set to disabled and the bounds for each variable will be cleared.

Note: The variables and constraints themselves will not be modified. If you need to change them, you must create a new theory solver.

Reimplemented from dlinear::TheorySolver.

Definition at line 244 of file SoplexTheorySolver.cpp.

◆ SetSPXVarCoeff()

void dlinear::SoplexTheorySolver::SetSPXVarCoeff	(	soplex::DSVectorRational &	coeffs,
		const Variable &	var,
		const mpq_class &	value ) const

protected

Set the coefficients to apply to var on a specific row.

Parameters

coeffs	vector of coefficients to apply to the decisional variables
var	variable to set the coefficients for
value	value to set the coefficients to

Definition at line 165 of file SoplexTheorySolver.cpp.

◆ UpdateExplanation()

void dlinear::SoplexTheorySolver::UpdateExplanation ( LiteralSet & explanation )

overrideprotectedvirtual

Use the result from the theory solver to update the explanation with the conflict that has been detected.

This will allow the SAT solver to find a new assignment without the conflict.

Warning: The explanation will be cleared before adding the conflicting literals

Parameters

explanation set conflicting clauses to be updated

Implements dlinear::TheorySolver.

Definition at line 290 of file SoplexTheorySolver.cpp.

◆ UpdateModelBounds()

void dlinear::SoplexTheorySolver::UpdateModelBounds ( )

overrideprotectedvirtual

Update each variable in the model with the bounds passed to the theory solver.

Note: there is no check in place on whether the bounds are inverted or the constraints satisfied.

Implements dlinear::TheorySolver.

Definition at line 266 of file SoplexTheorySolver.cpp.

◆ UpdateModelSolution()

void dlinear::SoplexTheorySolver::UpdateModelSolution ( )

overrideprotectedvirtual

Update the model with the solution obtained from the LP solver.

The model with show an assignment that satisfies all the theory literals.

Precondition: the lp solver must have found a feasible solution

Implements dlinear::TheorySolver.

Definition at line 251 of file SoplexTheorySolver.cpp.

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

dlinear/solver/SoplexTheorySolver.h
dlinear/solver/SoplexTheorySolver.cpp

Public Member Functions

Protected Member Functions

Protected Attributes

Static Protected Attributes

Additional Inherited Members

Detailed Description

Member Function Documentation

◆ AddLiterals()

◆ AddVariable()

◆ Consolidate()

◆ DisableSpxRows()

◆ EnableSpxRow() [1/2]

◆ EnableSpxRow() [2/2]

◆ EnableSpxVarBound()

◆ GetActiveRows() [1/2]

◆ GetActiveRows() [2/2]

◆ GetSpxInfeasibilityRay() [1/2]

◆ GetSpxInfeasibilityRay() [2/2]

◆ IsRowActive() [1/2]

◆ IsRowActive() [2/2]

◆ ParseRowCoeff()

◆ Reset()

◆ SetSPXVarCoeff()

◆ UpdateExplanation()

◆ UpdateModelBounds()

◆ UpdateModelSolution()