This class uses some basic algebraic operations to preprocess the constraints and identify violations before invoking the solver. More...

#include <BoundPreprocessor.h>

Public Member Functions
	BoundPreprocessor (const PredicateAbstractor &predicate_abstractor)
	Construct a new Bound Preprocessor object using the `predicate_abstractor`.

void	AddVariable (const Variable &var)
	Add a theory variable to the preprocessor.

std::set< LiteralSet >	EnableLiterals (const std::vector< Literal > &enabled_literals)
	Preprocess all the `enabled_literals`.

void	EnableLiterals (const std::vector< Literal > &enabled_literals, std::set< LiteralSet > &explanation)
	Preprocess all the `enabled_literals`.

std::set< LiteralSet >	EnableLiteral (const Literal &lit)
	Enable the literal `lit`.

void	EnableLiteral (const Literal &lit, std::set< LiteralSet > &explanations)
	Enable the literal `lit`.

Explanations	Process ()
	Process all enabled literals.

void	Process (Explanations &explanations)
	Process all enabled literals.

Explanations	Process (const LiteralSet &enabled_literals)
	Process the enabled literals `enabled_literals`.

void	Process (const LiteralSet &enabled_literals, Explanations &explanations)
	Process the enabled literals `enabled_literals`.

void	GetActiveExplanation (const Variable &var, LiteralSet &explanation)
	Get the active explanation for the variable `var`.

void	SetInfinityBounds (const Variable &var, const mpq_class &lb, const mpq_class &ub)
	Set the lower and upper infinity bounds (`lb`, ub) of the variable `var`.

void	Clear ()
	Clear the preprocessor.

void	Clear (const BoundPreprocessor &fixed_preprocessor)
	Clear the preprocessor using the `fixed_preprocessor`.

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

const BoundVectorMap &	theory_bounds () const
	Get read-only access to the bounds of the variables in the LP solver of the BoundPreprocessor.

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

const Environment &	env () const
	Get read-only access to the propagated environment containing the variable's values of the BoundPreprocessor.

const IterationStats &	stats () const
	Get read-only access to the statistics of the BoundPreprocessor.

bool	PropagateEqPolynomial (const Literal &lit, const Variable &var_to_propagate, Explanations &explanations)
	Propagate the bounds of the variables in the given formula.

bool	PropagateBoundsPolynomial (const Literal &lit, const Variable &var_to_propagate, Explanations &explanations)
	Propagate the bounds of the variables in the given formula.

Static Public Member Functions
static bool	IsSimpleBound (const Formula &formula)
	Check whether the formula is a simple relational bound.

static bool	IsEqualTo (const Formula &formula, bool truth=true)
	Check whether the formula is a simple relational bound with an equality operator ( \( a = b \)).

static bool	IsNotEqualTo (const Formula &formula, bool truth=true)
	Check whether the formula is a simple relational bound with a non-equality operator ( \( a \neq b \)).

static bool	IsGreaterThan (const Formula &formula, bool truth=true)
	Check whether the formula is a simple relational bound with a greater than operator ( \( a > b \)).

static bool	IsLessThan (const Formula &formula, bool truth=true)
	Check whether the formula is a simple relational bound with a less than operator ( \( a < b \)).

static bool	IsGreaterThanOrEqualTo (const Formula &formula, bool truth=true)
	Check whether the formula is a simple relational bound with a less than or equal to operator ( \( a \ge b \)).

static bool	IsLessThanOrEqualTo (const Formula &formula, bool truth=true)
	Check whether the formula is a simple relational bound with a less than or equal to operator ( \( a \le b \)).

Protected Member Functions
mpq_class	ExtractEqBoundCoefficient (const Formula &formula) const
	Given a formula of the form \( ax = by \), with \( a, b \in \mathbb{R} \) being constants, extract the coefficient \( c \coloneqq cx = y \).

const mpq_class *	StoreTemporaryMpq (const mpq_class &value)
	Vector used to store the mpq_class elements obtained from more complex constraints.

Private Attributes
std::list< mpq_class >	temporary_mpq_vector_
	Vector used to store temporary mpq values obtained from more complex constraints.

const Config &	config_
	Configuration of the preprocessor.

const PredicateAbstractor &	predicate_abstractor_
	Predicate abstractor used to get the constraints from the literals.

BoundVectorMap	theory_bounds_
	Theory bounds for each theory variable.

Environment	env_
	Environment storing the values of all the variables with a fixed value.

IterationStats	stats_
	Statistics of the preprocessing.

Detailed Description

This class uses some basic algebraic operations to preprocess the constraints and identify violations before invoking the solver.

Definition at line 37 of file BoundPreprocessor.h.

Constructor & Destructor Documentation

◆ BoundPreprocessor()

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

explicit

Construct a new Bound Preprocessor object using the predicate_abstractor.

Parameters

predicate_abstractor predicate abstractor containing the map between the variables and the literals

Definition at line 90 of file BoundPreprocessor.cpp.

Member Function Documentation

◆ AddVariable()

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

Add a theory variable to the preprocessor.

It will create a new entry in the theory_bounds_ map.

Parameters

var	theory variable to add

Definition at line 95 of file BoundPreprocessor.cpp.

◆ Clear() [1/2]

void dlinear::BoundPreprocessor::Clear ( )

Clear the preprocessor.

It will clear the environment, the theory bounds, and the enabled literals.

Definition at line 196 of file BoundPreprocessor.cpp.

◆ Clear() [2/2]

void dlinear::BoundPreprocessor::Clear ( const BoundPreprocessor & fixed_preprocessor )

Clear the preprocessor using the fixed_preprocessor.

It will clear the environment, the theory bounds, and the enabled literals by copying the values from the fixed_preprocessor.

Parameters

fixed_preprocessor preprocessor to use as a reference

Definition at line 202 of file BoundPreprocessor.cpp.

◆ config()

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

inlinenodiscard

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

Returns: configuration of the BoundPreprocessor

Definition at line 176 of file BoundPreprocessor.h.

◆ EnableLiteral() [1/2]

std::set< LiteralSet > dlinear::BoundPreprocessor::EnableLiteral ( const Literal & lit )

Enable the literal lit.

It will enable the literal and propagate the bounds. If a conflict is detected, it will return the set of explanations. Enabled literals are cached and will not be enabled again in the future.

Parameters

lit	literal to enable

Returns: set of explanations from the enabled literal if a conflict is detected; empty set if no conflict is detected

Definition at line 114 of file BoundPreprocessor.cpp.

◆ EnableLiteral() [2/2]

void dlinear::BoundPreprocessor::EnableLiteral	(	const Literal &	lit,
		std::set< LiteralSet > &	explanations )

Enable the literal lit.

It will enable the literal and propagate the bounds. If a conflict is detected, it will return the set of explanations. Enabled literals are cached and will not be enabled again in the future.

Parameters

	lit	literal to enable
[out]	explanations	set of explanations from the enabled literal if a conflict is detected

Definition at line 119 of file BoundPreprocessor.cpp.

◆ EnableLiterals() [1/2]

std::set< LiteralSet > dlinear::BoundPreprocessor::EnableLiterals ( const std::vector< Literal > & enabled_literals )

Preprocess all the enabled_literals.

It will enable the literals and propagate the bounds. If a conflict is detected, it will return the set of explanations. Enabled literals are cached and will not be enabled again in the future.

Parameters

enabled_literals literals to enable

Returns: set of explanations from the enabled literals if a conflict is detected; empty set if no conflict is detected

Definition at line 101 of file BoundPreprocessor.cpp.

◆ EnableLiterals() [2/2]

void dlinear::BoundPreprocessor::EnableLiterals	(	const std::vector< Literal > &	enabled_literals,
		std::set< LiteralSet > &	explanation )

Preprocess all the enabled_literals.

It will enable the literals and propagate the bounds. If a conflict is detected, it will return the set of explanations. Enabled literals are cached and will not be enabled again in the future.

Parameters

	enabled_literals	literals to enable
[out]	explanations	set of explanations from the enabled literals if a conflict is detected

Definition at line 106 of file BoundPreprocessor.cpp.

◆ env()

const Environment & dlinear::BoundPreprocessor::env ( ) const

inlinenodiscard

Get read-only access to the propagated environment containing the variable's values of the BoundPreprocessor.

Returns: propagated environment containing the variable's values of the BoundPreprocessor

Definition at line 182 of file BoundPreprocessor.h.

◆ ExtractEqBoundCoefficient()

mpq_class dlinear::BoundPreprocessor::ExtractEqBoundCoefficient ( const Formula & formula ) const

protected

Given a formula of the form \( ax = by \), with \( a, b \in \mathbb{R} \) being constants, extract the coefficient \( c \coloneqq cx = y \).

Variables enjoy total ordering between them. The leftmost variable is always the smallest.

Parameters

formula the formula to extract the coefficient from

Returns: the coefficient \( c \)

Definition at line 651 of file BoundPreprocessor.cpp.

◆ GetActiveExplanation()

void dlinear::BoundPreprocessor::GetActiveExplanation	(	const Variable &	var,
		LiteralSet &	explanation )

Get the active explanation for the variable var.

It will return the explanation for the variable var, justifying the active bounds.

Parameters

	var	variable to get the explanation for
[out]	explanation	explanation for the variable `var`

Definition at line 146 of file BoundPreprocessor.cpp.

◆ IsEqualTo()

bool dlinear::BoundPreprocessor::IsEqualTo	(	const Formula &	formula,
		bool	truth = true )

static

Check whether the formula is a simple relational bound with an equality operator ( \( a = b \)).

Parameters

formula	symbolic formula to check
truth	whether to consider the formula as it is (true) or to invert it (false)

Returns: true if the formula respects the condition; false if the formula does not respect the condition

See also: IsSimpleBound for more information about simple relational bounds

Definition at line 714 of file BoundPreprocessor.cpp.

◆ IsGreaterThan()

bool dlinear::BoundPreprocessor::IsGreaterThan	(	const Formula &	formula,
		bool	truth = true )

static

Check whether the formula is a simple relational bound with a greater than operator ( \( a > b \)).

Parameters

formula	symbolic formula to check
truth	whether to consider the formula as it is (true) or to invert it (false)

Returns: true if the formula respects the condition; false if the formula does not respect the condition

See also: IsSimpleBound for more information about simple relational bounds

Definition at line 722 of file BoundPreprocessor.cpp.

◆ IsGreaterThanOrEqualTo()

bool dlinear::BoundPreprocessor::IsGreaterThanOrEqualTo	(	const Formula &	formula,
		bool	truth = true )

static

Check whether the formula is a simple relational bound with a less than or equal to operator ( \( a \ge b \)).

Parameters

formula	symbolic formula to check
truth	whether to consider the formula as it is (true) or to invert it (false)

Returns: true if the formula respects the condition; false if the formula does not respect the condition

See also: IsSimpleBound for more information about simple relational bounds

Definition at line 730 of file BoundPreprocessor.cpp.

◆ IsLessThan()

bool dlinear::BoundPreprocessor::IsLessThan	(	const Formula &	formula,
		bool	truth = true )

static

Check whether the formula is a simple relational bound with a less than operator ( \( a < b \)).

Parameters

formula	symbolic formula to check
truth	whether to consider the formula as it is (true) or to invert it (false)

Returns: true if the formula respects the condition; false if the formula does not respect the condition

See also: IsSimpleBound for more information about simple relational bounds

Definition at line 726 of file BoundPreprocessor.cpp.

◆ IsLessThanOrEqualTo()

bool dlinear::BoundPreprocessor::IsLessThanOrEqualTo	(	const Formula &	formula,
		bool	truth = true )

static

Check whether the formula is a simple relational bound with a less than or equal to operator ( \( a \le b \)).

Parameters

formula	symbolic formula to check
truth	whether to consider the formula as it is (true) or to invert it (false)

Returns: true if the formula respects the condition; false if the formula does not respect the condition

See also: IsSimpleBound for more information about simple relational bounds

Definition at line 734 of file BoundPreprocessor.cpp.

◆ IsNotEqualTo()

bool dlinear::BoundPreprocessor::IsNotEqualTo	(	const Formula &	formula,
		bool	truth = true )

static

Check whether the formula is a simple relational bound with a non-equality operator ( \( a \neq b \)).

Parameters

formula	symbolic formula to check
truth	whether to consider the formula as it is (true) or to invert it (false)

Returns: true if the formula respects the condition; false if the formula does not respect the condition

See also: IsSimpleBound for more information about simple relational bounds

Definition at line 718 of file BoundPreprocessor.cpp.

◆ IsSimpleBound()

bool dlinear::BoundPreprocessor::IsSimpleBound ( const Formula & formula )

static

Check whether the formula is a simple relational bound.

A simple relational bound is a formula in the form:

\[ a \leq b \\ a < b \\ a \geq b \\ a > b \\ a = b \\ a \neq b \\ \]

Where \( a \) is a variable and \( b \) is a constant or vice versa.

Parameters

formula symbolic formula to check

Returns: true if the formula is a simple relational bound; false if the formula is not a simple relational bound

Definition at line 702 of file BoundPreprocessor.cpp.

◆ predicate_abstractor()

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

inlinenodiscard

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

Returns: predicate abstractor of the BoundPreprocessor

Definition at line 180 of file BoundPreprocessor.h.

◆ Process() [1/4]

BoundPreprocessor::Explanations dlinear::BoundPreprocessor::Process ( )

Process all enabled literals.

It will process the enabled literals and propagate the bounds. The bounds are propagated based on the BoundPropagationType and the formulae will be evaluated. If a conflict is detected, it will return the set of explanations.

Returns: set of explanations from the enabled literals if a conflict is detected; empty set if no conflict is detected

Definition at line 151 of file BoundPreprocessor.cpp.

◆ Process() [2/4]

BoundPreprocessor::Explanations dlinear::BoundPreprocessor::Process ( const LiteralSet & enabled_literals )

Process the enabled literals enabled_literals.

It will process the enabled literals and propagate the bounds. The bounds are propagated based on the BoundPropagationType and the formulae will be evaluated. If a conflict is detected, it will return the set of explanations.

Parameters

enabled_literals literals to enable

Returns: set of explanations from the enabled literals if a conflict is detected; empty set if no conflict is detected

Definition at line 157 of file BoundPreprocessor.cpp.

◆ Process() [3/4]

void dlinear::BoundPreprocessor::Process	(	const LiteralSet &	enabled_literals,
		Explanations &	explanations )

Process the enabled literals enabled_literals.

It will process the enabled literals and propagate the bounds. The bounds are propagated based on the BoundPropagationType and the formulae will be evaluated. If a conflict is detected, it will return the set of explanations.

Parameters

	enabled_literals	literals to enable
[out]	explanations	set of explanations from the enabled literals if a conflict is detected

Definition at line 162 of file BoundPreprocessor.cpp.

◆ Process() [4/4]

void dlinear::BoundPreprocessor::Process ( Explanations & explanations )

Process all enabled literals.

It will process the enabled literals and propagate the bounds. The bounds are propagated based on the BoundPropagationType and the formulae will be evaluated. If a conflict is detected, it will return the set of explanations.

Parameters

[out] explanations set of explanations from the enabled literals if a conflict is detected

Definition at line 156 of file BoundPreprocessor.cpp.

◆ PropagateBoundsPolynomial()

bool dlinear::BoundPreprocessor::PropagateBoundsPolynomial	(	const Literal &	lit,
		const Variable &	var_to_propagate,
		Explanations &	explanations )

Propagate the bounds of the variables in the given formula.

It only works for formulas of the form \( \sum_{i = 1}^n a_i x_i \bowtie c \) where the values \( a_i, c \in \mathbb{R} \) are known, \( \bowtie \in \{<, \le, =, \ge, >\} \), and all but exactly one variable among the \( x_i \) are bounded. Their values will be used to assign the value to the last unknown variable, and a dependency edge will be added to the graph. If the new assignment is incompatible with the current one, a conflict is found.

Precondition: the formula is of the form \( \sum_{i = 1}^n a_i x_i \bowtie c \); all but exactly one of the variables are bounded

Parameters

lit	theory literal corresponding to the formula to propagate
var_to_propagate	the variable to propagate
explanations	the explanations to be updated if a conflict is found

Returns: true if the propagation was successful; false if a conflict was detected

Definition at line 292 of file BoundPreprocessor.cpp.

◆ PropagateEqPolynomial()

bool dlinear::BoundPreprocessor::PropagateEqPolynomial	(	const Literal &	lit,
		const Variable &	var_to_propagate,
		Explanations &	explanations )

Propagate the bounds of the variables in the given formula.

It only works for formulas of the form \( \sum_{i = 1}^n a_i x_i = c \) where the values \( a_i, c \in \mathbb{R} \) are known, and all but exactly one variable among the \( x_i \) have a value assigned in the env_. Their values will be used to assign the value to the last unknown variable. The explanation will be added to the bound vector. If the new assignment is incompatible with the current one, a conflict is found.

Precondition: the formula is of the form \( \sum_{i = 1}^n a_i x_i = c \); all but exactly one of the variables have a value assigned in the env_

Parameters

lit	theory literal corresponding to the formula to propagate
var_to_propagate	the variable to propagate
explanations	the explanations to be updated if a conflict is found

Returns: true if the propagation was successful; false if a conflict was detected

Definition at line 209 of file BoundPreprocessor.cpp.

◆ SetInfinityBounds()

void dlinear::BoundPreprocessor::SetInfinityBounds	(	const Variable &	var,
		const mpq_class &	lb,
		const mpq_class &	ub )

Set the lower and upper infinity bounds (lb, ub) of the variable var.

All bounds currently assigned to var will be removed.

Parameters

var	variable to fix the bounds for
lb	lower infinity bound
ub	upper infinity bound

Definition at line 192 of file BoundPreprocessor.cpp.

◆ stats()

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

inlinenodiscard

Get read-only access to the statistics of the BoundPreprocessor.

Returns: statistics of the BoundPreprocessor

Definition at line 184 of file BoundPreprocessor.h.

◆ theory_bounds()

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

inlinenodiscard

Get read-only access to the bounds of the variables in the LP solver of the BoundPreprocessor.

Returns: bounds of the variables in the LP solver of the BoundPreprocessor

Definition at line 178 of file BoundPreprocessor.h.

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

dlinear/solver/BoundPreprocessor.h
dlinear/solver/BoundPreprocessor.cpp

Public Member Functions

Static Public Member Functions

Protected Member Functions

Private Attributes

Detailed Description

Constructor & Destructor Documentation

◆ BoundPreprocessor()

Member Function Documentation

◆ AddVariable()

◆ Clear() [1/2]

◆ Clear() [2/2]

◆ config()

◆ EnableLiteral() [1/2]

◆ EnableLiteral() [2/2]

◆ EnableLiterals() [1/2]

◆ EnableLiterals() [2/2]

◆ env()

◆ ExtractEqBoundCoefficient()

◆ GetActiveExplanation()

◆ IsEqualTo()

◆ IsGreaterThan()

◆ IsGreaterThanOrEqualTo()

◆ IsLessThan()

◆ IsLessThanOrEqualTo()

◆ IsNotEqualTo()

◆ IsSimpleBound()

◆ predicate_abstractor()

◆ Process() [1/4]

◆ Process() [2/4]

◆ Process() [3/4]

◆ Process() [4/4]

◆ PropagateBoundsPolynomial()

◆ PropagateEqPolynomial()

◆ SetInfinityBounds()

◆ stats()

◆ theory_bounds()