smtrat::lra::Bound< T1, T2 >::Info Struct Reference

Stores some additional information for a bound. More...

#include <Bound.h>

Public Member Functions
	Info (ModuleInput::iterator _position)

Data Fields
int	updated
	A value to store the information whether this bounds constraint has already been processed (=0), must be processed (>0) or must be removed from consideration (<0). More...
ModuleInput::iterator	position
	The position of this bounds constraint in a formula, if it has been processed already. More...
FormulaT	neqRepresentation
	If this bound corresponds to a constraint being p<0 or p>0 for a polynomial p, we store here the constraint p!=0. More...
bool	exists
	A flag which is only false, if this bound has been created for a constraint having != as relation symbol, i.e. More...
const Bound< T1, T2 > *	complement

Detailed Description

template<typename T1, typename T2>
struct smtrat::lra::Bound< T1, T2 >::Info

Stores some additional information for a bound.

Definition at line 44 of file Bound.h.

Constructor & Destructor Documentation

Info()

template<typename T1 , typename T2 >

smtrat::lra::Bound< T1, T2 >::Info::Info ( ModuleInput::iterator  _position )

inline

Definition at line 66 of file Bound.h.

Field Documentation

complement

template<typename T1 , typename T2 >

const Bound<T1, T2>* smtrat::lra::Bound< T1, T2 >::Info::complement

Definition at line 64 of file Bound.h.

exists

template<typename T1 , typename T2 >

bool smtrat::lra::Bound< T1, T2 >::Info::exists

A flag which is only false, if this bound has been created for a constraint having != as relation symbol, i.e.

p!=0, and not yet for the constraint p<0 or p>0.

Definition at line 62 of file Bound.h.

neqRepresentation

template<typename T1 , typename T2 >

FormulaT smtrat::lra::Bound< T1, T2 >::Info::neqRepresentation

If this bound corresponds to a constraint being p<0 or p>0 for a polynomial p, we store here the constraint p!=0.

Definition at line 57 of file Bound.h.

position

template<typename T1 , typename T2 >

ModuleInput::iterator smtrat::lra::Bound< T1, T2 >::Info::position

The position of this bounds constraint in a formula, if it has been processed already.

Otherwise it points to the end of a formula.

Definition at line 55 of file Bound.h.

updated

template<typename T1 , typename T2 >

int smtrat::lra::Bound< T1, T2 >::Info::updated

A value to store the information whether this bounds constraint has already been processed (=0), must be processed (>0) or must be removed from consideration (<0).

Definition at line 50 of file Bound.h.

---

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

• smtrat-modules/LRAModule/tableau/Bound.h