Class to manage the bounds of a variable. More...

#include <VariableBounds.h>

Inheritance diagram for smtrat::vb::VariableBounds< T >:

Collaboration diagram for smtrat::vb::VariableBounds< T >:

[legend]

Public Types
typedef std::map< ConstraintT, const Bound< T > * >	ConstraintBoundMap
	A map from Constraint pointers to Bound pointers. More...

typedef carl::FastMap< carl::Variable, Variable< T > * >	VariableMap
	A hash-map from arithmetic variables to variables managing the bounds. More...

Public Member Functions
	VariableBounds ()
	Constructs a variable bounds manager. More...

	~VariableBounds ()
	Destructs a variable bounds manager. More...

void	clear ()

bool	empty () const

bool	addBound (const ConstraintT &_constraint, const T &_origin)
	Updates the variable bounds by the given constraint. More...

bool	addBound (const FormulaT &_formula, const T &_origin)

unsigned	removeBound (const ConstraintT &_constraint, const T &_origin)
	Removes all effects the given constraint has on the variable bounds. More...

unsigned	removeBound (const FormulaT &_formula, const T &_origin)

unsigned	removeBound (const ConstraintT &_constraint, const T &_origin, carl::Variable *&_changedVariable)
	Removes all effects the given constraint has on the variable bounds. More...

const EvalRationalIntervalMap &	getEvalIntervalMap () const
	Creates an evalintervalmap corresponding to the variable bounds. More...

const RationalInterval &	getInterval (const carl::Variable &_var) const
	Creates an interval corresponding to the variable bounds of the given variable. More...

RationalInterval	getInterval (carl::Monomial::Arg _mon) const
	Creates an interval corresponding to the bounds of the given monomial. More...

RationalInterval	getInterval (const TermT &_term) const
	Creates an interval corresponding to the bounds of the given term. More...

const smtrat::EvalDoubleIntervalMap &	getIntervalMap () const
	Creates an interval map corresponding to the variable bounds. More...

const carl::Interval< double > &	getDoubleInterval (const carl::Variable &_var) const
	Creates a double interval corresponding to the variable bounds of the given variable. More...

std::vector< T >	getOriginsOfBounds (const carl::Variable &_var) const

std::set< T >	getOriginSetOfBounds (const carl::Variable &_var) const

std::vector< T >	getOriginsOfBounds (const carl::Variables &_variables) const

std::set< T >	getOriginSetOfBounds (const carl::Variables &_variables) const

std::vector< T >	getOriginsOfBounds () const
	Collect the origins to the supremums and infimums of all variables. More...

std::set< T >	getOriginSetOfBounds () const

std::vector< std::pair< std::vector< ConstraintT >, ConstraintT > >	getBoundDeductions () const

void	print (std::ostream &_out=std::cout, const std::string _init="", bool _printAllBounds=false) const
	Prints the variable bounds. More...

bool	isConflicting () const

std::set< T >	getConflict () const

Private Attributes
Variable< T > *	mpConflictingVariable
	A pointer to one of the conflicting variables (its supremum is smaller than its infimum) or NULL if there is no conflict. More...

VariableMap *	mpVariableMap
	A mapping from arithmetic variables to the variable objects storing the bounds. More...

ConstraintBoundMap *	mpConstraintBoundMap
	A mapping from constraint pointer to the corresponding bounds. More...

EvalRationalIntervalMap	mEvalIntervalMap
	The stored exact interval map representing the currently tightest bounds. More...

EvalDoubleIntervalMap	mDoubleIntervalMap
	The stored double interval map representing the currently tightest bounds. More...

ConstraintsT	mNonBoundConstraints
	Stores the constraints which cannot be used to infer a bound for a variable. More...

std::unordered_set< std::vector< ConstraintT > >	mBoundDeductions
	Stores deductions which this variable bounds manager has detected. More...

Detailed Description

template<typename T>
class smtrat::vb::VariableBounds< T >

Class to manage the bounds of a variable.

Definition at line 356 of file VariableBounds.h.

Member Typedef Documentation

◆ ConstraintBoundMap

template<typename T >

typedef std::map<ConstraintT,const Bound<T>*> smtrat::vb::VariableBounds< T >::ConstraintBoundMap

A map from Constraint pointers to Bound pointers.

Definition at line 360 of file VariableBounds.h.

◆ VariableMap

template<typename T >

typedef carl::FastMap<carl::Variable, Variable<T>*> smtrat::vb::VariableBounds< T >::VariableMap

A hash-map from arithmetic variables to variables managing the bounds.

Definition at line 362 of file VariableBounds.h.

Constructor & Destructor Documentation

◆ VariableBounds()

template<typename T >

smtrat::vb::VariableBounds< T >::VariableBounds ( )

Constructs a variable bounds manager.

◆ ~VariableBounds()

template<typename T >

smtrat::vb::VariableBounds< T >::~VariableBounds ( )

Destructs a variable bounds manager.

Member Function Documentation

◆ addBound() [1/2]

template<typename T >

bool smtrat::vb::VariableBounds< T >::addBound	(	const ConstraintT &	_constraint,
		const T &	_origin
	)

Updates the variable bounds by the given constraint.

Parameters

_constraint	The constraint to consider.
_origin	The origin of the given constraint.

Returns: true, if the variable bounds have been changed; false, otherwise.

Here is the caller graph for this function:

◆ addBound() [2/2]

template<typename T >

bool smtrat::vb::VariableBounds< T >::addBound	(	const FormulaT &	_formula,
		const T &	_origin
	)

◆ clear()

template<typename T >

void smtrat::vb::VariableBounds< T >::clear ( )

Here is the caller graph for this function:

◆ empty()

template<typename T >

bool smtrat::vb::VariableBounds< T >::empty ( ) const

inline

Definition at line 393 of file VariableBounds.h.

◆ getBoundDeductions()

template<typename T >

std::vector<std::pair<std::vector<ConstraintT>, ConstraintT> > smtrat::vb::VariableBounds< T >::getBoundDeductions ( ) const

Returns: The deductions which this variable bounds manager has detected.

◆ getConflict()

template<typename T >

std::set<T> smtrat::vb::VariableBounds< T >::getConflict ( ) const

inline

Returns: The origins which cause the conflict. This method can only be called, if there is a conflict.

Definition at line 518 of file VariableBounds.h.

Here is the call graph for this function:

◆ getDoubleInterval()

template<typename T >

const carl::Interval<double>& smtrat::vb::VariableBounds< T >::getDoubleInterval ( const carl::Variable & _var ) const

Creates a double interval corresponding to the variable bounds of the given variable.

Parameters

_var	The variable to compute the variable bounds as double interval for.

Returns: The variable bounds as a double interval.

Here is the caller graph for this function:

◆ getEvalIntervalMap()

template<typename T >

const EvalRationalIntervalMap& smtrat::vb::VariableBounds< T >::getEvalIntervalMap ( ) const

Creates an evalintervalmap corresponding to the variable bounds.

Returns: The variable bounds as an evalintervalmap.

Here is the caller graph for this function:

◆ getInterval() [1/3]

template<typename T >

RationalInterval smtrat::vb::VariableBounds< T >::getInterval ( carl::Monomial::Arg _mon ) const

Creates an interval corresponding to the bounds of the given monomial.

Parameters

_mon	The monomial to compute the bounds as interval for.

Returns: The monomial bounds as an interval.

◆ getInterval() [2/3]

template<typename T >

const RationalInterval& smtrat::vb::VariableBounds< T >::getInterval ( const carl::Variable & _var ) const

Creates an interval corresponding to the variable bounds of the given variable.

Parameters

_var	The variable to compute the variable bounds as interval for.

Returns: The variable bounds as an interval.

Here is the caller graph for this function:

◆ getInterval() [3/3]

template<typename T >

RationalInterval smtrat::vb::VariableBounds< T >::getInterval ( const TermT & _term ) const

Creates an interval corresponding to the bounds of the given term.

Parameters

_term The term to compute the bounds as interval for.

Returns: The term bounds as an interval.

◆ getIntervalMap()

template<typename T >

const smtrat::EvalDoubleIntervalMap& smtrat::vb::VariableBounds< T >::getIntervalMap ( ) const

Creates an interval map corresponding to the variable bounds.

Returns: The variable bounds as an interval map.

Here is the caller graph for this function:

◆ getOriginSetOfBounds() [1/3]

template<typename T >

std::set<T> smtrat::vb::VariableBounds< T >::getOriginSetOfBounds ( ) const

◆ getOriginSetOfBounds() [2/3]

template<typename T >

std::set<T> smtrat::vb::VariableBounds< T >::getOriginSetOfBounds ( const carl::Variable & _var ) const

◆ getOriginSetOfBounds() [3/3]

template<typename T >

std::set<T> smtrat::vb::VariableBounds< T >::getOriginSetOfBounds ( const carl::Variables & _variables ) const

◆ getOriginsOfBounds() [1/3]

template<typename T >

std::vector<T> smtrat::vb::VariableBounds< T >::getOriginsOfBounds ( ) const

Collect the origins to the supremums and infimums of all variables.

Returns: A set of origins corresponding to the supremums and infimums of all variables.

◆ getOriginsOfBounds() [2/3]

template<typename T >

std::vector<T> smtrat::vb::VariableBounds< T >::getOriginsOfBounds ( const carl::Variable & _var ) const

Parameters

_var	The variable to get origins of the bounds for.

Returns: The origin constraints of the supremum and infimum of the given variable.

Here is the caller graph for this function:

◆ getOriginsOfBounds() [3/3]

template<typename T >

std::vector<T> smtrat::vb::VariableBounds< T >::getOriginsOfBounds ( const carl::Variables & _variables ) const

Parameters

_variables The variables to get origins of the bounds for.

Returns: The origin constraints of the supremum and infimum of the given variables.

◆ isConflicting()

template<typename T >

bool smtrat::vb::VariableBounds< T >::isConflicting ( ) const

inline

Returns: true, if there is a conflicting variable; false, otherwise.

Definition at line 510 of file VariableBounds.h.

Here is the caller graph for this function:

◆ print()

template<typename T >

void smtrat::vb::VariableBounds< T >::print	(	std::ostream &	_out = `std::cout`,
		const std::string	_init = `""`,
		bool	_printAllBounds = `false`
	)		const

Prints the variable bounds.

Parameters

_out	The output stream to print on.
_init	A string which is displayed at the beginning of every row.
_printAllBounds	A flag that indicates whether to print also the bounds of each variable (=true).

Here is the caller graph for this function:

◆ removeBound() [1/3]

template<typename T >

unsigned smtrat::vb::VariableBounds< T >::removeBound	(	const ConstraintT &	_constraint,
		const T &	_origin
	)

Removes all effects the given constraint has on the variable bounds.

Parameters

_constraint	The constraint, which effects shall be undone for the variable bounds.
_origin	The origin of the given constraint.

Returns: 2, if the variables supremum or infimum have been changed; 1, if the constraint was a (not the strictest) bound; 0, otherwise.

Here is the caller graph for this function:

◆ removeBound() [2/3]

template<typename T >

unsigned smtrat::vb::VariableBounds< T >::removeBound	(	const ConstraintT &	_constraint,
		const T &	_origin,
		carl::Variable *&	_changedVariable
	)

Removes all effects the given constraint has on the variable bounds.

Parameters

_constraint	The constraint, which effects shall be undone for the variable bounds.
_origin	The origin of the given constraint.
_changedVariable	The variable whose interval domain has been changed, if the return value is 2.

Returns: 2, if the variables supremum or infimum have been changed; 1, if the constraint was a (not the strictest) bound; 0, otherwise.

◆ removeBound() [3/3]

template<typename T >

unsigned smtrat::vb::VariableBounds< T >::removeBound	(	const FormulaT &	_formula,
		const T &	_origin
	)

Field Documentation

◆ mBoundDeductions

template<typename T >

std::unordered_set<std::vector<ConstraintT> > smtrat::vb::VariableBounds< T >::mBoundDeductions

mutableprivate

Stores deductions which this variable bounds manager has detected.

Definition at line 380 of file VariableBounds.h.

◆ mDoubleIntervalMap

template<typename T >

EvalDoubleIntervalMap smtrat::vb::VariableBounds< T >::mDoubleIntervalMap

mutableprivate

The stored double interval map representing the currently tightest bounds.

Note, that it is updated on demand.

Definition at line 376 of file VariableBounds.h.

◆ mEvalIntervalMap

template<typename T >

EvalRationalIntervalMap smtrat::vb::VariableBounds< T >::mEvalIntervalMap

mutableprivate

The stored exact interval map representing the currently tightest bounds.

Note, that it is updated on demand.

Definition at line 373 of file VariableBounds.h.

◆ mNonBoundConstraints

template<typename T >

ConstraintsT smtrat::vb::VariableBounds< T >::mNonBoundConstraints

private

Stores the constraints which cannot be used to infer a bound for a variable.

Definition at line 378 of file VariableBounds.h.

◆ mpConflictingVariable

template<typename T >

Variable<T>* smtrat::vb::VariableBounds< T >::mpConflictingVariable

private

A pointer to one of the conflicting variables (its supremum is smaller than its infimum) or NULL if there is no conflict.

Definition at line 366 of file VariableBounds.h.

◆ mpConstraintBoundMap

template<typename T >

ConstraintBoundMap* smtrat::vb::VariableBounds< T >::mpConstraintBoundMap

private

A mapping from constraint pointer to the corresponding bounds.

Definition at line 370 of file VariableBounds.h.

◆ mpVariableMap

template<typename T >

VariableMap* smtrat::vb::VariableBounds< T >::mpVariableMap

private

A mapping from arithmetic variables to the variable objects storing the bounds.

Definition at line 368 of file VariableBounds.h.

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

smtrat-variablebounds/VariableBounds.h

Public Types

Public Member Functions

Private Attributes

Detailed Description

template<typename T> class smtrat::vb::VariableBounds< T >

Member Typedef Documentation

◆ ConstraintBoundMap

◆ VariableMap

Constructor & Destructor Documentation

◆ VariableBounds()

◆ ~VariableBounds()

Member Function Documentation

◆ addBound() [1/2]

◆ addBound() [2/2]

◆ clear()

◆ empty()

◆ getBoundDeductions()

◆ getConflict()

◆ getDoubleInterval()

◆ getEvalIntervalMap()

◆ getInterval() [1/3]

◆ getInterval() [2/3]

◆ getInterval() [3/3]

◆ getIntervalMap()

◆ getOriginSetOfBounds() [1/3]

◆ getOriginSetOfBounds() [2/3]

◆ getOriginSetOfBounds() [3/3]

◆ getOriginsOfBounds() [1/3]

◆ getOriginsOfBounds() [2/3]

◆ getOriginsOfBounds() [3/3]

◆ isConflicting()

◆ print()

◆ removeBound() [1/3]

◆ removeBound() [2/3]

◆ removeBound() [3/3]

Field Documentation

◆ mBoundDeductions

◆ mDoubleIntervalMap

◆ mEvalIntervalMap

◆ mNonBoundConstraints

◆ mpConflictingVariable

◆ mpConstraintBoundMap

◆ mpVariableMap

template<typename T>
class smtrat::vb::VariableBounds< T >