SMT-RAT  24.02
Toolbox for Strategic and Parallel Satisfiability-Modulo-Theories Solving
Public Member Functions | Private Attributes
smtrat::lra::Variable< T1, T2 > Class Template Reference

#include <Variable.h>

Inheritance diagram for smtrat::lra::Variable< T1, T2 >:
Inheritance graph
[legend]
Collaboration diagram for smtrat::lra::Variable< T1, T2 >:
Collaboration graph
[legend]

Public Member Functions

 Variable (size_t _position, const typename Poly::PolyType *_expression, ModuleInput::iterator _defaultBoundPosition, bool _isInteger, size_t _id)
 
 Variable (typename std::list< std::list< std::pair< Variable< T1, T2 > *, T2 >>>::iterator _positionInNonActives, const typename Poly::PolyType *_expression, ModuleInput::iterator _defaultBoundPosition, bool _isInteger, size_t _id)
 
virtual ~Variable ()
 
const Value< T1 > & assignment () const
 
Value< T1 > & rAssignment ()
 
void storeAssignment ()
 
const Value< T1 > & lastConsistentAssignment () const
 
void setBasic (bool _basic)
 
bool isBasic () const
 
bool isOriginal () const
 
bool is_integer () const
 
bool hasBound () const
 
bool involvesEquation () const
 
EntryID startEntry () const
 
EntryID & rStartEntry ()
 
size_t size () const
 
size_t & rSize ()
 
double conflictActivity () const
 
void setSupremum (const Bound< T1, T2 > *_supremum)
 
const Bound< T1, T2 > * pSupremum () const
 
const Bound< T1, T2 > & supremum () const
 
void setInfimum (const Bound< T1, T2 > *_infimum)
 
const Bound< T1, T2 > * pInfimum () const
 
const Bound< T1, T2 > & infimum () const
 
size_t position () const
 
size_t id () const
 
void setPosition (size_t _position)
 
bool isConflicting () const
 
std::list< std::list< std::pair< Variable< T1, T2 > *, T2 > > >::iterator positionInNonActives () const
 
void setPositionInNonActives (typename std::list< std::list< std::pair< Variable< T1, T2 > *, T2 >>>::iterator _positionInNonActives)
 
size_t rLowerBoundsSize ()
 
size_t rUpperBoundsSize ()
 
const Bound< T1, T2 >::BoundSet & upperbounds () const
 
const Bound< T1, T2 >::BoundSet & lowerbounds () const
 
Bound< T1, T2 >::BoundSet & rUpperbounds ()
 
Bound< T1, T2 >::BoundSet & rLowerbounds ()
 
size_t & rPosition ()
 
const Poly::PolyType * pExpression () const
 
const Poly::PolyType & expression () const
 
const T2 & factor () const
 
T2 & rFactor ()
 
unsigned isSatisfiedBy (const RationalAssignment &_ass) const
 
FormulaT inConflictWith (const RationalAssignment &_ass) const
 
void updateConflictActivity ()
 
std::pair< const Bound< T1, T2 > *, bool > addUpperBound (Value< T1 > *const _val, ModuleInput::iterator _position, const FormulaT &_constraint, bool _deduced=false)
 
std::pair< const Bound< T1, T2 > *, bool > addLowerBound (Value< T1 > *const _val, ModuleInput::iterator _position, const FormulaT &_constraint, bool _deduced=false)
 
std::pair< const Bound< T1, T2 > *, bool > addEqualBound (Value< T1 > *const _val, ModuleInput::iterator _position, const FormulaT &_constraint)
 
void removeBound (const Bound< T1, T2 > *_bound)
 
bool deactivateBound (const Bound< T1, T2 > *bound, ModuleInput::iterator _position)
 
RationalInterval getVariableBounds () const
 
FormulasT getDefiningOrigins () const
 
bool operator< (const Variable &_variable) const
 
bool operator> (const Variable &_variable) const
 
bool operator== (const Variable &_variable) const
 
bool operator!= (const Variable &_variable) const
 
void print (std::ostream &_out=std::cout) const
 
void printAllBounds (std::ostream &_out=std::cout, const std::string _init="") const
 

Private Attributes

bool mBasic
 
bool mOriginal
 
bool mInteger
 
EntryID mStartEntry
 
size_t mSize
 
double mConflictActivity
 
size_t mPosition
 
std::list< std::list< std::pair< Variable< T1, T2 > *, T2 > > >::iterator mPositionInNonActives
 
size_t mId
 
Bound< T1, T2 >::BoundSet mUpperbounds
 
Bound< T1, T2 >::BoundSet mLowerbounds
 
const Bound< T1, T2 > * mpSupremum
 
const Bound< T1, T2 > * mpInfimum
 
const Poly::PolyType * mExpression
 
Value< T1 > mAssignment
 
Value< T1 > mLastConsistentAssignment
 
T2 mFactor
 

Detailed Description

template<typename T1, typename T2>
class smtrat::lra::Variable< T1, T2 >

Definition at line 28 of file Variable.h.

Constructor & Destructor Documentation

◆ Variable() [1/2]

template<typename T1 , typename T2 >
smtrat::lra::Variable< T1, T2 >::Variable ( size_t  _position,
const typename Poly::PolyType *  _expression,
ModuleInput::iterator  _defaultBoundPosition,
bool  _isInteger,
size_t  _id 
)
Parameters
_position
_expression
_defaultBoundPosition
_isInteger
_id

◆ Variable() [2/2]

template<typename T1 , typename T2 >
smtrat::lra::Variable< T1, T2 >::Variable ( typename std::list< std::list< std::pair< Variable< T1, T2 > *, T2 >>>::iterator  _positionInNonActives,
const typename Poly::PolyType *  _expression,
ModuleInput::iterator  _defaultBoundPosition,
bool  _isInteger,
size_t  _id 
)
Parameters
_positionInNonActives
_expression
_defaultBoundPosition
_isInteger
_id

◆ ~Variable()

template<typename T1 , typename T2 >
virtual smtrat::lra::Variable< T1, T2 >::~Variable ( )
virtual

Member Function Documentation

◆ addEqualBound()

template<typename T1 , typename T2 >
std::pair<const Bound<T1, T2>*, bool> smtrat::lra::Variable< T1, T2 >::addEqualBound ( Value< T1 > *const  _val,
ModuleInput::iterator  _position,
const FormulaT &  _constraint 
)
Parameters
_val
_position
_constraint
Returns

◆ addLowerBound()

template<typename T1 , typename T2 >
std::pair<const Bound<T1, T2>*, bool> smtrat::lra::Variable< T1, T2 >::addLowerBound ( Value< T1 > *const  _val,
ModuleInput::iterator  _position,
const FormulaT &  _constraint,
bool  _deduced = false 
)
Parameters
_val
_position
_constraint
_deduced
Returns

◆ addUpperBound()

template<typename T1 , typename T2 >
std::pair<const Bound<T1, T2>*, bool> smtrat::lra::Variable< T1, T2 >::addUpperBound ( Value< T1 > *const  _val,
ModuleInput::iterator  _position,
const FormulaT &  _constraint,
bool  _deduced = false 
)
Parameters
_val
_position
_constraint
_deduced
Returns

◆ assignment()

template<typename T1 , typename T2 >
const Value<T1>& smtrat::lra::Variable< T1, T2 >::assignment ( ) const
inline
Returns

Definition at line 97 of file Variable.h.

◆ conflictActivity()

template<typename T1 , typename T2 >
double smtrat::lra::Variable< T1, T2 >::conflictActivity ( ) const
inline
Returns

Definition at line 210 of file Variable.h.

◆ deactivateBound()

template<typename T1 , typename T2 >
bool smtrat::lra::Variable< T1, T2 >::deactivateBound ( const Bound< T1, T2 > *  bound,
ModuleInput::iterator  _position 
)
Parameters
bound
_position
Returns

◆ expression()

template<typename T1 , typename T2 >
const Poly::PolyType& smtrat::lra::Variable< T1, T2 >::expression ( ) const
inline
Returns

Definition at line 391 of file Variable.h.

◆ factor()

template<typename T1 , typename T2 >
const T2& smtrat::lra::Variable< T1, T2 >::factor ( ) const
inline
Returns

Definition at line 400 of file Variable.h.

Here is the caller graph for this function:

◆ getDefiningOrigins()

template<typename T1 , typename T2 >
FormulasT smtrat::lra::Variable< T1, T2 >::getDefiningOrigins ( ) const
Returns

◆ getVariableBounds()

template<typename T1 , typename T2 >
RationalInterval smtrat::lra::Variable< T1, T2 >::getVariableBounds ( ) const
Returns

◆ hasBound()

template<typename T1 , typename T2 >
bool smtrat::lra::Variable< T1, T2 >::hasBound ( ) const
inline
Returns

Definition at line 162 of file Variable.h.

◆ id()

template<typename T1 , typename T2 >
size_t smtrat::lra::Variable< T1, T2 >::id ( ) const
inline

Definition at line 288 of file Variable.h.

Here is the caller graph for this function:

◆ inConflictWith()

template<typename T1 , typename T2 >
FormulaT smtrat::lra::Variable< T1, T2 >::inConflictWith ( const RationalAssignment &  _ass) const
inline
Parameters
_ass
Returns

Definition at line 446 of file Variable.h.

Here is the call graph for this function:

◆ infimum()

template<typename T1 , typename T2 >
const Bound<T1, T2>& smtrat::lra::Variable< T1, T2 >::infimum ( ) const
inline
Returns

Definition at line 274 of file Variable.h.

◆ involvesEquation()

template<typename T1 , typename T2 >
bool smtrat::lra::Variable< T1, T2 >::involvesEquation ( ) const
inline
Returns

Definition at line 170 of file Variable.h.

◆ is_integer()

template<typename T1 , typename T2 >
bool smtrat::lra::Variable< T1, T2 >::is_integer ( ) const
inline
Returns

Definition at line 154 of file Variable.h.

◆ isBasic()

template<typename T1 , typename T2 >
bool smtrat::lra::Variable< T1, T2 >::isBasic ( ) const
inline
Returns

Definition at line 138 of file Variable.h.

◆ isConflicting()

template<typename T1 , typename T2 >
bool smtrat::lra::Variable< T1, T2 >::isConflicting ( ) const
inline

Definition at line 301 of file Variable.h.

◆ isOriginal()

template<typename T1 , typename T2 >
bool smtrat::lra::Variable< T1, T2 >::isOriginal ( ) const
inline
Returns

Definition at line 146 of file Variable.h.

Here is the caller graph for this function:

◆ isSatisfiedBy()

template<typename T1 , typename T2 >
unsigned smtrat::lra::Variable< T1, T2 >::isSatisfiedBy ( const RationalAssignment &  _ass) const
inline
Parameters
_ass
Returns

Definition at line 419 of file Variable.h.

Here is the call graph for this function:

◆ lastConsistentAssignment()

template<typename T1 , typename T2 >
const Value<T1>& smtrat::lra::Variable< T1, T2 >::lastConsistentAssignment ( ) const
inline
Returns

Definition at line 121 of file Variable.h.

◆ lowerbounds()

template<typename T1 , typename T2 >
const Bound<T1, T2>::BoundSet& smtrat::lra::Variable< T1, T2 >::lowerbounds ( ) const
inline
Returns

Definition at line 351 of file Variable.h.

◆ operator!=()

template<typename T1 , typename T2 >
bool smtrat::lra::Variable< T1, T2 >::operator!= ( const Variable< T1, T2 > &  _variable) const
inline

Definition at line 596 of file Variable.h.

◆ operator<()

template<typename T1 , typename T2 >
bool smtrat::lra::Variable< T1, T2 >::operator< ( const Variable< T1, T2 > &  _variable) const
inline
Parameters
_bound
Returns

Definition at line 579 of file Variable.h.

Here is the call graph for this function:

◆ operator==()

template<typename T1 , typename T2 >
bool smtrat::lra::Variable< T1, T2 >::operator== ( const Variable< T1, T2 > &  _variable) const
inline

Definition at line 591 of file Variable.h.

Here is the call graph for this function:

◆ operator>()

template<typename T1 , typename T2 >
bool smtrat::lra::Variable< T1, T2 >::operator> ( const Variable< T1, T2 > &  _variable) const
inline

Definition at line 586 of file Variable.h.

◆ pExpression()

template<typename T1 , typename T2 >
const Poly::PolyType* smtrat::lra::Variable< T1, T2 >::pExpression ( ) const
inline
Returns

Definition at line 383 of file Variable.h.

◆ pInfimum()

template<typename T1 , typename T2 >
const Bound<T1, T2>* smtrat::lra::Variable< T1, T2 >::pInfimum ( ) const
inline
Returns

Definition at line 265 of file Variable.h.

◆ position()

template<typename T1 , typename T2 >
size_t smtrat::lra::Variable< T1, T2 >::position ( ) const
inline
Returns

Definition at line 283 of file Variable.h.

◆ positionInNonActives()

template<typename T1 , typename T2 >
std::list<std::list<std::pair<Variable<T1,T2>*,T2> > >::iterator smtrat::lra::Variable< T1, T2 >::positionInNonActives ( ) const
inline
Returns

Definition at line 309 of file Variable.h.

Here is the caller graph for this function:

◆ print()

template<typename T1 , typename T2 >
void smtrat::lra::Variable< T1, T2 >::print ( std::ostream &  _out = std::cout) const
Parameters
_out
Here is the caller graph for this function:

◆ printAllBounds()

template<typename T1 , typename T2 >
void smtrat::lra::Variable< T1, T2 >::printAllBounds ( std::ostream &  _out = std::cout,
const std::string  _init = "" 
) const
Parameters
_out
_init

◆ pSupremum()

template<typename T1 , typename T2 >
const Bound<T1, T2>* smtrat::lra::Variable< T1, T2 >::pSupremum ( ) const
inline
Returns

Definition at line 232 of file Variable.h.

◆ rAssignment()

template<typename T1 , typename T2 >
Value<T1>& smtrat::lra::Variable< T1, T2 >::rAssignment ( )
inline
Returns

Definition at line 105 of file Variable.h.

◆ removeBound()

template<typename T1 , typename T2 >
void smtrat::lra::Variable< T1, T2 >::removeBound ( const Bound< T1, T2 > *  _bound)
Parameters
_bound

◆ rFactor()

template<typename T1 , typename T2 >
T2& smtrat::lra::Variable< T1, T2 >::rFactor ( )
inline
Returns

Definition at line 408 of file Variable.h.

◆ rLowerbounds()

template<typename T1 , typename T2 >
Bound<T1, T2>::BoundSet& smtrat::lra::Variable< T1, T2 >::rLowerbounds ( )
inline
Returns

Definition at line 367 of file Variable.h.

◆ rLowerBoundsSize()

template<typename T1 , typename T2 >
size_t smtrat::lra::Variable< T1, T2 >::rLowerBoundsSize ( )
inline
Returns

Definition at line 327 of file Variable.h.

◆ rPosition()

template<typename T1 , typename T2 >
size_t& smtrat::lra::Variable< T1, T2 >::rPosition ( )
inline
Returns

Definition at line 375 of file Variable.h.

◆ rSize()

template<typename T1 , typename T2 >
size_t& smtrat::lra::Variable< T1, T2 >::rSize ( )
inline
Returns

Definition at line 202 of file Variable.h.

◆ rStartEntry()

template<typename T1 , typename T2 >
EntryID& smtrat::lra::Variable< T1, T2 >::rStartEntry ( )
inline
Returns

Definition at line 186 of file Variable.h.

◆ rUpperbounds()

template<typename T1 , typename T2 >
Bound<T1, T2>::BoundSet& smtrat::lra::Variable< T1, T2 >::rUpperbounds ( )
inline
Returns

Definition at line 359 of file Variable.h.

◆ rUpperBoundsSize()

template<typename T1 , typename T2 >
size_t smtrat::lra::Variable< T1, T2 >::rUpperBoundsSize ( )
inline
Returns

Definition at line 335 of file Variable.h.

◆ setBasic()

template<typename T1 , typename T2 >
void smtrat::lra::Variable< T1, T2 >::setBasic ( bool  _basic)
inline
Parameters
_basic

Definition at line 130 of file Variable.h.

◆ setInfimum()

template<typename T1 , typename T2 >
void smtrat::lra::Variable< T1, T2 >::setInfimum ( const Bound< T1, T2 > *  _infimum)
inline
Parameters
_infimum

Definition at line 251 of file Variable.h.

Here is the call graph for this function:

◆ setPosition()

template<typename T1 , typename T2 >
void smtrat::lra::Variable< T1, T2 >::setPosition ( size_t  _position)
inline
Parameters
_position

Definition at line 296 of file Variable.h.

◆ setPositionInNonActives()

template<typename T1 , typename T2 >
void smtrat::lra::Variable< T1, T2 >::setPositionInNonActives ( typename std::list< std::list< std::pair< Variable< T1, T2 > *, T2 >>>::iterator  _positionInNonActives)
inline
Parameters
_positionInNonActives

Definition at line 318 of file Variable.h.

Here is the call graph for this function:

◆ setSupremum()

template<typename T1 , typename T2 >
void smtrat::lra::Variable< T1, T2 >::setSupremum ( const Bound< T1, T2 > *  _supremum)
inline
Parameters
_supremum

Definition at line 219 of file Variable.h.

Here is the call graph for this function:

◆ size()

template<typename T1 , typename T2 >
size_t smtrat::lra::Variable< T1, T2 >::size ( ) const
inline
Returns

Definition at line 194 of file Variable.h.

◆ startEntry()

template<typename T1 , typename T2 >
EntryID smtrat::lra::Variable< T1, T2 >::startEntry ( ) const
inline
Returns

Definition at line 178 of file Variable.h.

◆ storeAssignment()

template<typename T1 , typename T2 >
void smtrat::lra::Variable< T1, T2 >::storeAssignment ( )
inline

Definition at line 113 of file Variable.h.

◆ supremum()

template<typename T1 , typename T2 >
const Bound<T1, T2>& smtrat::lra::Variable< T1, T2 >::supremum ( ) const
inline
Returns

Definition at line 241 of file Variable.h.

◆ updateConflictActivity()

template<typename T1 , typename T2 >
void smtrat::lra::Variable< T1, T2 >::updateConflictActivity ( )
inline

Definition at line 478 of file Variable.h.

Here is the caller graph for this function:

◆ upperbounds()

template<typename T1 , typename T2 >
const Bound<T1, T2>::BoundSet& smtrat::lra::Variable< T1, T2 >::upperbounds ( ) const
inline
Returns

Definition at line 343 of file Variable.h.

Field Documentation

◆ mAssignment

template<typename T1 , typename T2 >
Value<T1> smtrat::lra::Variable< T1, T2 >::mAssignment
private

Definition at line 60 of file Variable.h.

◆ mBasic

template<typename T1 , typename T2 >
bool smtrat::lra::Variable< T1, T2 >::mBasic
private

Definition at line 32 of file Variable.h.

◆ mConflictActivity

template<typename T1 , typename T2 >
double smtrat::lra::Variable< T1, T2 >::mConflictActivity
private

Definition at line 42 of file Variable.h.

◆ mExpression

template<typename T1 , typename T2 >
const Poly::PolyType* smtrat::lra::Variable< T1, T2 >::mExpression
private

Definition at line 58 of file Variable.h.

◆ mFactor

template<typename T1 , typename T2 >
T2 smtrat::lra::Variable< T1, T2 >::mFactor
private

Definition at line 65 of file Variable.h.

◆ mId

template<typename T1 , typename T2 >
size_t smtrat::lra::Variable< T1, T2 >::mId
private

Definition at line 48 of file Variable.h.

◆ mInteger

template<typename T1 , typename T2 >
bool smtrat::lra::Variable< T1, T2 >::mInteger
private

Definition at line 36 of file Variable.h.

◆ mLastConsistentAssignment

template<typename T1 , typename T2 >
Value<T1> smtrat::lra::Variable< T1, T2 >::mLastConsistentAssignment
private

Definition at line 62 of file Variable.h.

◆ mLowerbounds

template<typename T1 , typename T2 >
Bound<T1, T2>::BoundSet smtrat::lra::Variable< T1, T2 >::mLowerbounds
private

Definition at line 52 of file Variable.h.

◆ mOriginal

template<typename T1 , typename T2 >
bool smtrat::lra::Variable< T1, T2 >::mOriginal
private

Definition at line 34 of file Variable.h.

◆ mpInfimum

template<typename T1 , typename T2 >
const Bound<T1, T2>* smtrat::lra::Variable< T1, T2 >::mpInfimum
private

Definition at line 56 of file Variable.h.

◆ mPosition

template<typename T1 , typename T2 >
size_t smtrat::lra::Variable< T1, T2 >::mPosition
private

Definition at line 44 of file Variable.h.

◆ mPositionInNonActives

template<typename T1 , typename T2 >
std::list<std::list<std::pair<Variable<T1,T2>*,T2> > >::iterator smtrat::lra::Variable< T1, T2 >::mPositionInNonActives
private

Definition at line 46 of file Variable.h.

◆ mpSupremum

template<typename T1 , typename T2 >
const Bound<T1, T2>* smtrat::lra::Variable< T1, T2 >::mpSupremum
private

Definition at line 54 of file Variable.h.

◆ mSize

template<typename T1 , typename T2 >
size_t smtrat::lra::Variable< T1, T2 >::mSize
private

Definition at line 40 of file Variable.h.

◆ mStartEntry

template<typename T1 , typename T2 >
EntryID smtrat::lra::Variable< T1, T2 >::mStartEntry
private

Definition at line 38 of file Variable.h.

◆ mUpperbounds

template<typename T1 , typename T2 >
Bound<T1, T2>::BoundSet smtrat::lra::Variable< T1, T2 >::mUpperbounds
private

Definition at line 50 of file Variable.h.

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