QSopt_ex is an exact LP solver written in C. More...

#include <QsoptexTheorySolver.h>

Inheritance diagram for dlinear::QsoptexTheorySolver:

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.

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.

virtual void	Reset ()
	Reset the linear problem.

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.

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

void	EnableQsxRow (int qsx_row)
	Enable the `qsx_row` row for the LP solver.

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

void	DisableQsxRows ()
	Disable all disabled qsx rows from the LP solver.

void	SetRowCoeff (const Formula &formula, int qsx_row)
	Parse a `formula` and set the correct coefficients of decisional variables in the `qsx_row` row.

void	SetQsxVarCoeff (int qsx_row, const Variable &var, const mpq_class &value)
	Set the coefficient of `var` on the `qsx_row` row.

void	SetQsxVarObjCoeff (const Variable &var, const mpq_class &value)
	Set the objective coefficient of `var` to `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
std::vector< mpq_class >	qsx_rhs_
	Right-hand side of the constraints.

std::vector< LpRowSense >	qsx_sense_
	Sense of the constraints.

qsopt_ex::MpqArray	ray_
	Ray of the last infeasible solution.

qsopt_ex::MpqArray	x_
	Solution vector.

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.

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

QSopt_ex is an exact LP solver written in C.

It uses the technique of precision boosting to efficiently solve LPs exactly.

Definition at line 30 of file QsoptexTheorySolver.h.

Member Function Documentation

◆ AddLiterals()

void dlinear::QsoptexTheorySolver::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 49 of file QsoptexTheorySolver.cpp.

◆ AddVariable()

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

overridevirtual

Add a variable (column) to the theory solver.

Parameters

var	variable to add

Implements dlinear::TheorySolver.

Definition at line 35 of file QsoptexTheorySolver.cpp.

◆ Consolidate()

void dlinear::QsoptexTheorySolver::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 55 of file QsoptexTheorySolver.cpp.

◆ DisableQsxRows()

void dlinear::QsoptexTheorySolver::DisableQsxRows ( )

protected

Disable all disabled qsx 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 292 of file QsoptexTheorySolver.cpp.

◆ EnableQsxRow() [1/2]

void dlinear::QsoptexTheorySolver::EnableQsxRow ( int qsx_row )

protected

Enable the qsx_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

qsx_row index of the row to enable

Definition at line 301 of file QsoptexTheorySolver.cpp.

◆ EnableQsxRow() [2/2]

virtual void dlinear::QsoptexTheorySolver::EnableQsxRow	(	int	qsx_row,
		bool	truth )

protectedpure virtual

Enable the qsx_row row for the LP solver.

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

Parameters

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

Implemented in dlinear::DeltaQsoptexTheorySolver.

◆ EnableQsxVarBound()

void dlinear::QsoptexTheorySolver::EnableQsxVarBound ( )

protected

Set the bounds of the variables in the LP solver.

Definition at line 199 of file QsoptexTheorySolver.cpp.

◆ SetQsxVarCoeff()

void dlinear::QsoptexTheorySolver::SetQsxVarCoeff	(	int	qsx_row,
		const Variable &	var,
		const mpq_class &	value )

protected

Set the coefficient of var on the qsx_row row.

Parameters

qsx_row	row to update with the coefficient
var	variable to set the coefficient for
value	value to set the coefficient to

Definition at line 209 of file QsoptexTheorySolver.cpp.

◆ SetQsxVarObjCoeff()

void dlinear::QsoptexTheorySolver::SetQsxVarObjCoeff	(	const Variable &	var,
		const mpq_class &	value )

protected

Set the objective coefficient of var to value.

Parameters

var	variable to set the objective coefficient for
value	value of the objective coefficient

Definition at line 223 of file QsoptexTheorySolver.cpp.

◆ SetRowCoeff()

void dlinear::QsoptexTheorySolver::SetRowCoeff	(	const Formula &	formula,
		int	qsx_row )

protected

Parse a formula and set the correct coefficients of decisional variables in the qsx_row row.

It will store the rhs term in qsx_rhs_ and update the qsx_row with the parsed coefficients.

Parameters

formula	symbolic formula representing the row
qsx_row	index of the row to update

Definition at line 139 of file QsoptexTheorySolver.cpp.

◆ UpdateExplanation()

void dlinear::QsoptexTheorySolver::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 251 of file QsoptexTheorySolver.cpp.

◆ UpdateModelBounds()

void dlinear::QsoptexTheorySolver::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 84 of file QsoptexTheorySolver.cpp.

◆ UpdateModelSolution()

void dlinear::QsoptexTheorySolver::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 74 of file QsoptexTheorySolver.cpp.

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

dlinear/solver/QsoptexTheorySolver.h
dlinear/solver/QsoptexTheorySolver.cpp

Public Member Functions

Protected Member Functions

Protected Attributes

Additional Inherited Members

Detailed Description

Member Function Documentation

◆ AddLiterals()

◆ AddVariable()

◆ Consolidate()

◆ DisableQsxRows()

◆ EnableQsxRow() [1/2]

◆ EnableQsxRow() [2/2]

◆ EnableQsxVarBound()

◆ SetQsxVarCoeff()

◆ SetQsxVarObjCoeff()

◆ SetRowCoeff()

◆ UpdateExplanation()

◆ UpdateModelBounds()

◆ UpdateModelSolution()