Base class for theory solvers. More...

#include <TheorySolver.h>

Inheritance diagram for dlinear::TheorySolver:

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

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

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

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.

virtual void	AddVariable (const Variable &var)=0
	Add a variable (column) 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	Consolidate (const Box &box)
	Consolidate the solver.

virtual void	Reset ()
	Reset the linear problem.

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

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

Protected Member Functions
virtual void	UpdateModelSolution ()=0
	Update the model with the solution obtained from the LP solver.

virtual void	UpdateModelBounds ()=0
	Update each variable in the model with the bounds passed to the theory solver.

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

void	UpdateExplanations (Explanations &explanations)
	Use the result from the theory solver to update the explanations with the conflict that has been detected.

Protected Attributes
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.

Detailed Description

Base class for theory solvers.

Theory solvers pick up the literals assignments from the SAT solver and check whether the assignment is satisfiable within the theory. If that is not the case, they will produce an explanation to guide the SAT solver and find a new assignment. This class has to be inherited and implemented by the specific theory solvers.

Definition at line 37 of file TheorySolver.h.

Member Enumeration Documentation

◆ BoundViolationType

enum class dlinear::TheorySolver::BoundViolationType

strongprotected

Enum used to describe how the bounds on a variable participate in the infeasibility result of an LP problem.

Enumerator
NO_BOUND_VIOLATION	The bounds of the variable have no role in the infeasibility.
LOWER_BOUND_VIOLATION	The lower bound is involved in the infeasibility.

Definition at line 207 of file TheorySolver.h.

Constructor & Destructor Documentation

◆ TheorySolver()

dlinear::TheorySolver::TheorySolver	(	const PredicateAbstractor &	predicate_abstractor,
		const std::string &	class_name = "TheorySolver" )

explicit

Construct a new Theory Solver object.

The predicate_abstractor is shared between the theory solver and the SAT solver, in order to have a common understanding of the literals. The class_name is used to identify the theory solver in the logs.

Note: The predicate abstractor will share its configuration with the theory solver.

Parameters

class_name	name of the subclass of the theory solver used
predicate_abstractor	predicate abstractor linking boolean literals to theory literals. It is shared between the theory solver and the SAT solver

Definition at line 13 of file TheorySolver.cpp.

Member Function Documentation

◆ AddLiteral()

virtual void dlinear::TheorySolver::AddLiteral	(	const Variable &	formula_var,
		const Formula &	formula )

pure virtual

Add a Literal to the theory solver.

A Literal is formed by a variable that corresponds to a theory formula inside the PredicateAbstractor and the formula itself

Parameters

formula_var	boolean variable that corresponds to the theory formula
formula	symbolic formula that represents the theory formula

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

◆ AddLiterals()

void dlinear::TheorySolver::AddLiterals ( )

virtual

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 in dlinear::QsoptexTheorySolver, and dlinear::SoplexTheorySolver.

Definition at line 35 of file TheorySolver.cpp.

◆ AddVariable()

virtual void dlinear::TheorySolver::AddVariable ( const Variable & var )

pure virtual

Add a variable (column) to the theory solver.

Parameters

var	variable to add

Implemented in dlinear::CompleteSoplexTheorySolver, dlinear::QsoptexTheorySolver, and dlinear::SoplexTheorySolver.

◆ CheckSat()

SatResult dlinear::TheorySolver::CheckSat	(	const Box &	box,
		mpq_class *	actual_precision,
		std::set< LiteralSet > &	explanations )

Check the satisfiability of the theory.

Run the internal LP solver to check whether the underlying linear programming problem is feasible. If it is, SAT will be returned, along with the actual precision required to obtain that result. Otherwise, UNSAT will be returned, along with an explanation of the conflict. In that case, the precision will remain the same as the one passed as input.

Parameters

	box	current box with the bounds for the variables, including the boolean ones
[in,out]	actual_precision	desired precision. It will be updated with the actual precision if SAT is returned
[out]	explanations	set of sets of literals that explain the conflict if UNSAT is returned

Returns: SAT if the problem is feasible, along with the actual precision required to obtain that result and the model; UNSAT if the problem is infeasible, along with an explanation of the conflict

Definition at line 121 of file TheorySolver.cpp.

◆ CheckSatCore()

virtual SatResult dlinear::TheorySolver::CheckSatCore	(	mpq_class *	actual_precision,
		std::set< LiteralSet > &	explanations )

pure virtual

Check the satisfiability of the theory.

Called by CheckSat. Run the internal LP solver to check whether the underlying linear programming problem is feasible. If it is, SAT will be returned, along with the actual precision required to obtain that result. Otherwise, UNSAT will be returned, along with an explanation of the conflict. In that case, the precision will remain the same as the one passed as input.

Parameters

[in,out]	actual_precision	desired precision. It will be updated with the actual precision if SAT is returned
[out]	explanations	set of sets of literals that explain the conflict if UNSAT is returned

Returns: SAT if the problem is feasible, along with the actual precision required to obtain that result and the model; UNSAT if the problem is infeasible, along with an explanation of the conflict

Implemented in dlinear::NNSoplexTheorySolver.

◆ config()

const Config & dlinear::TheorySolver::config ( ) const

inlinenodiscard

Get read-only access to the configuration of the TheorySolver.

Returns: configuration of the TheorySolver

Definition at line 112 of file TheorySolver.h.

◆ Consolidate()

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

virtual

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 in dlinear::CompleteSoplexTheorySolver, dlinear::NNSoplexTheorySolver, dlinear::QsoptexTheorySolver, and dlinear::SoplexTheorySolver.

Definition at line 72 of file TheorySolver.cpp.

◆ enabled_literals()

std::set< Literal > dlinear::TheorySolver::enabled_literals ( ) const

nodiscard

Get read-only access to the vector of enabled literals of the TheorySolver.

Returns: vector of enabled literals of the TheorySolver

Definition at line 23 of file TheorySolver.cpp.

◆ EnableLiteral()

virtual Explanations dlinear::TheorySolver::EnableLiteral ( const Literal & lit )

pure virtual

Activate the literal that had previously been added to the theory solver.

If the literal is a row inside the TheorySolver, then the the corresponding constraint is activated by giving it the proper values.

If the literal is a simple bound on the variable (column), some additional checks are made. Theory solvers struggle to handle problems with inverted bounds. It is convenient to have a method that checks them beforehand. If at least a bound is inverted, the problem is UNSAT, since it is impossible to satisfy the constraint. An explanation is produced and returned to the SAT solver.

Parameters

lit	literal to activate

Returns: an explanation with the literals that correspond to the conflicting bounds; an empty optional if no conflicts are detected at this step

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

◆ EnableLiterals()

TheorySolver::Explanations dlinear::TheorySolver::EnableLiterals ( std::span< const Literal > theory_literals )

Activate the literals that have previously been added to the theory solver.

Parameters

theory_literals vector of literals to be activated

Returns: a set of explanations with the literals that correspond to the conflicting bounds

Definition at line 54 of file TheorySolver.cpp.

◆ fixed_preprocessor()

const BoundPreprocessor & dlinear::TheorySolver::fixed_preprocessor ( ) const

inlinenodiscard

Get read-only access to the fixed bound preprocessor of the TheorySolver.

Returns: fixed bound preprocessor of the TheorySolver

Definition at line 132 of file TheorySolver.h.

◆ fixed_theory_bounds()

const BoundVectorMap & dlinear::TheorySolver::fixed_theory_bounds ( ) const

inlinenodiscard

Get read-only access to the fixed bounds of each theory variable of the TheorySolver.

Returns: fixed bounds of each theory variable of the TheorySolver

Definition at line 126 of file TheorySolver.h.

◆ lit_to_theory_row()

const std::map< Variable::Id, int > & dlinear::TheorySolver::lit_to_theory_row ( ) const

inlinenodiscard

Get read-only access to the map of literals to the theory rows of the TheorySolver.

Returns: map of literals to the theory rows of the TheorySolver

Definition at line 120 of file TheorySolver.h.

◆ m_fixed_preprocessor()

BoundPreprocessor & dlinear::TheorySolver::m_fixed_preprocessor ( )

inlinenodiscard

Get read-write access to the fixed bound preprocessor of the TheorySolver.

Returns: fixed bound preprocessor of the TheorySolver

Definition at line 134 of file TheorySolver.h.

◆ m_preprocessor()

BoundPreprocessor & dlinear::TheorySolver::m_preprocessor ( )

inlinenodiscard

Get read-write access to the bound preprocessor of the TheorySolver.

Returns: bound preprocessor of the TheorySolver

Definition at line 130 of file TheorySolver.h.

◆ model()

const Box & dlinear::TheorySolver::model ( ) const

nodiscard

Get read-only access to the model that satisfies all the constraints of the TheorySolver.

Returns: model that satisfies all the constraints of the TheorySolver

Definition at line 22 of file TheorySolver.cpp.

◆ predicate_abstractor()

const PredicateAbstractor & dlinear::TheorySolver::predicate_abstractor ( ) const

inlinenodiscard

Get read-only access to the predicate abstractor of the TheorySolver.

Returns: predicate abstractor of the TheorySolver

Definition at line 114 of file TheorySolver.h.

◆ PreprocessFixedLiterals()

TheorySolver::Explanations dlinear::TheorySolver::PreprocessFixedLiterals ( const LiteralSet & fixed_literals )

virtual

Add the fixed literals to the theory solver.

This means that, for the model to be sat, these literals will never change their assignment. This allows for slight optimizations (e.g. their bound can be computed once, at the beginning of the run instead of at each iteration)

Parameters

fixed_literals set of fixed literals

Definition at line 40 of file TheorySolver.cpp.

◆ preprocessor()

const BoundPreprocessor & dlinear::TheorySolver::preprocessor ( ) const

inlinenodiscard

Get read-only access to the bound preprocessor of the TheorySolver.

Returns: bound preprocessor of the TheorySolver

Definition at line 128 of file TheorySolver.h.

◆ Reset()

void dlinear::TheorySolver::Reset ( )

virtual

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 in dlinear::CompleteSoplexTheorySolver, dlinear::NNSoplexTheorySolver, and dlinear::SoplexTheorySolver.

Definition at line 79 of file TheorySolver.cpp.

◆ stats()

const IterationStats & dlinear::TheorySolver::stats ( ) const

inlinenodiscard

Get the statistics of the theory solver.

Returns: statistics of the theory solver

Definition at line 199 of file TheorySolver.h.

◆ theory_bounds()

const BoundVectorMap & dlinear::TheorySolver::theory_bounds ( ) const

inlinenodiscard

Get read-only access to the bounds of each theory variable of the TheorySolver.

Returns: bounds of each theory variable of the TheorySolver

Definition at line 124 of file TheorySolver.h.

◆ theory_col_count()

std::size_t dlinear::TheorySolver::theory_col_count ( ) const

inlinenodiscard

Get read-only access to the number of columns of the TheorySolver.

Returns: number of columns of the TheorySolver

Definition at line 138 of file TheorySolver.h.

◆ theory_col_to_var()

const std::vector< Variable > & dlinear::TheorySolver::theory_col_to_var ( ) const

inlinenodiscard

Get read-only access to the map of theory columns to the variables of the TheorySolver.

Returns: map of theory columns to the variables of the TheorySolver

Definition at line 118 of file TheorySolver.h.

◆ theory_row_count()

std::size_t dlinear::TheorySolver::theory_row_count ( ) const

inlinenodiscard

Get read-only access to the number of rows of the TheorySolver.

Returns: number of rows of the TheorySolver

Definition at line 136 of file TheorySolver.h.

◆ theory_row_to_lit()

const std::vector< Literal > & dlinear::TheorySolver::theory_row_to_lit ( ) const

inlinenodiscard

Get read-only access to the map of theory rows to the literals of the TheorySolver.

Returns: map of theory rows to the literals of the TheorySolver

Definition at line 122 of file TheorySolver.h.

◆ UpdateExplanation()

virtual void dlinear::TheorySolver::UpdateExplanation ( LiteralSet & explanation )

protectedpure virtual

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

Implemented in dlinear::QsoptexTheorySolver, and dlinear::SoplexTheorySolver.

◆ UpdateExplanations()

void dlinear::TheorySolver::UpdateExplanations ( Explanations & explanations )

protected

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

A new explanations will be added to the current set of explanations. This will allow the SAT solver to find a new assignment without the conflict.

Parameters

explanations set of explanations the new conflicting clauses will be added to

Definition at line 65 of file TheorySolver.cpp.

◆ UpdateModelBounds()

virtual void dlinear::TheorySolver::UpdateModelBounds ( )

protectedpure virtual

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.

Implemented in dlinear::QsoptexTheorySolver, and dlinear::SoplexTheorySolver.

◆ UpdateModelSolution()

virtual void dlinear::TheorySolver::UpdateModelSolution ( )

protectedpure virtual

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

Implemented in dlinear::QsoptexTheorySolver, and dlinear::SoplexTheorySolver.

◆ var_to_theory_col()

const std::map< Variable::Id, int > & dlinear::TheorySolver::var_to_theory_col ( ) const

inlinenodiscard

Get read-only access to the map of variables to the theory columns of the TheorySolver.

Returns: map of variables to the theory columns of the TheorySolver

Definition at line 116 of file TheorySolver.h.

Member Data Documentation

◆ is_consolidated_

bool dlinear::TheorySolver::is_consolidated_

protected

Whether the solver has been consolidated.

This method must be called after all the literals have been added to the solver.

Definition at line 247 of file TheorySolver.h.

◆ lit_to_theory_row_

std::map<Variable::Id, int> dlinear::TheorySolver::lit_to_theory_row_

protected

Literal ⇔ theory row.

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

Definition at line 258 of file TheorySolver.h.

◆ preprocessor_

BoundPreprocessor dlinear::TheorySolver::preprocessor_

protected

Preprocessor for the bounds.

Propagates the bounds through simple expressions to produce a precise explanation of the conflict without invoking the LP solver.

Definition at line 270 of file TheorySolver.h.

◆ theory_col_to_var_

std::vector<Variable> dlinear::TheorySolver::theory_col_to_var_

protected

Theory column ⇔ Variable.

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

Definition at line 255 of file TheorySolver.h.

◆ theory_row_to_lit_

std::vector<Literal> dlinear::TheorySolver::theory_row_to_lit_

protected

Theory row ⇔ Literal The row is the constraint used by the theory solver.

The literal is the one created by the PredicateAbstractor. It may not contain simple bounds

Definition at line 261 of file TheorySolver.h.

◆ theory_rows_state_

std::vector<bool> dlinear::TheorySolver::theory_rows_state_

protected

Whether each theory row is enabled or not.

It also verifies that the bounds are consistent every time a new one is added.

Definition at line 265 of file TheorySolver.h.

◆ var_to_theory_col_

std::map<Variable::Id, int> dlinear::TheorySolver::var_to_theory_col_

protected

Variable ⇔ theory column.

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

Definition at line 252 of file TheorySolver.h.

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

dlinear/solver/TheorySolver.h
dlinear/solver/TheorySolver.cpp

Public Types

Public Member Functions

Protected Types

Protected Member Functions

Protected Attributes

Detailed Description

Member Enumeration Documentation

◆ BoundViolationType

Constructor & Destructor Documentation

◆ TheorySolver()

Member Function Documentation

◆ AddLiteral()

◆ AddLiterals()

◆ AddVariable()

◆ CheckSat()

◆ CheckSatCore()

◆ config()

◆ Consolidate()

◆ enabled_literals()

◆ EnableLiteral()

◆ EnableLiterals()

◆ fixed_preprocessor()

◆ fixed_theory_bounds()

◆ lit_to_theory_row()

◆ m_fixed_preprocessor()

◆ m_preprocessor()

◆ model()

◆ predicate_abstractor()

◆ PreprocessFixedLiterals()

◆ preprocessor()

◆ Reset()

◆ stats()

◆ theory_bounds()

◆ theory_col_count()

◆ theory_col_to_var()

◆ theory_row_count()

◆ theory_row_to_lit()

◆ UpdateExplanation()

◆ UpdateExplanations()

◆ UpdateModelBounds()

◆ UpdateModelSolution()

◆ var_to_theory_col()

Member Data Documentation

◆ is_consolidated_

◆ lit_to_theory_row_

◆ preprocessor_

◆ theory_col_to_var_

◆ theory_row_to_lit_

◆ theory_rows_state_

◆ var_to_theory_col_