SMT-RAT  24.02
Toolbox for Strategic and Parallel Satisfiability-Modulo-Theories Solving
Public Member Functions | Private Member Functions | Private Attributes | Friends
smtrat::icp::IcpVariable Class Reference

#include <IcpVariable.h>

Collaboration diagram for smtrat::icp::IcpVariable:
Collaboration graph
[legend]

Public Member Functions

 IcpVariable (carl::Variable::Arg _var, bool _original, ModuleInput::iterator _defaultPosition, EvalDoubleIntervalMap::iterator _intervalPos, const LRAVariable *_lraVar=NULL)
 
 ~IcpVariable ()
 
carl::Variable::Arg var () const
 
ContractionCandidates & candidates ()
 
const LRAVariable * lraVar () const
 
void addCandidate (ContractionCandidate *_candidate)
 
void addCandidates (const ContractionCandidates &_candidates)
 
void addOriginalConstraint (const FormulaT &_constraint)
 
void removeOriginalConstraint (const FormulaT &_constraint)
 
void setLraVar (const LRAVariable *_lraVar)
 
void print (std::ostream &_out=std::cout, bool _withContractionCandidates=false) const
 
bool isActive () const
 
void incrementActivity ()
 
void decrementActivity ()
 
bool is_linear ()
 
EvalDoubleIntervalMap::const_iterator intervalPosition () const
 
const DoubleInterval & interval () const
 
void setInterval (const DoubleInterval &_interval)
 
void setUnmodified ()
 
void setExternalUnmodified ()
 
void setExternalModified ()
 
void setInternalUnmodified ()
 
Updated isInternalUpdated () const
 
Updated isExternalUpdated () const
 
const smtrat::FormulaT & internalLeftBound () const
 
const smtrat::FormulaT & internalRightBound () const
 
ModuleInput::iterator externalLeftBound () const
 
ModuleInput::iterator externalRightBound () const
 
void setInternalLeftBound (const smtrat::FormulaT &_left)
 
void setInternalRightBound (const smtrat::FormulaT &_right)
 
void setExternalLeftBound (ModuleInput::iterator _left)
 
void setExternalRightBound (ModuleInput::iterator _right)
 
Updated isInternalBoundsSet () const
 
bool isOriginal () const
 
bool operator< (IcpVariable const &rhs) const
 

Private Member Functions

 IcpVariable ()
 

Private Attributes

carl::Variable mVar
 
bool mOriginal
 
ContractionCandidates mCandidates
 
FormulaSetT mOriginalConstraints
 
const LRAVariable * mLraVar
 
unsigned mActivity
 
bool mLinear
 
EvalDoubleIntervalMap::iterator mIntervalPos
 
std::pair< Updated, Updated > mBoundsSet
 
std::pair< Updated, Updated > mUpdated
 
smtrat::FormulaT mInternalLeftBound
 
smtrat::FormulaT mInternalRightBound
 
ModuleInput::iterator mExternalLeftBound
 
ModuleInput::iterator mExternalRightBound
 
ModuleInput::iterator mDefaultPosition
 

Friends

std::ostream & operator<< (std::ostream &os, const IcpVariable &_var)
 

Detailed Description

Definition at line 35 of file IcpVariable.h.

Constructor & Destructor Documentation

◆ IcpVariable() [1/2]

smtrat::icp::IcpVariable::IcpVariable ( )
private

◆ IcpVariable() [2/2]

smtrat::icp::IcpVariable::IcpVariable ( carl::Variable::Arg  _var,
bool  _original,
ModuleInput::iterator  _defaultPosition,
EvalDoubleIntervalMap::iterator  _intervalPos,
const LRAVariable *  _lraVar = NULL 
)
inline

Definition at line 68 of file IcpVariable.h.

◆ ~IcpVariable()

smtrat::icp::IcpVariable::~IcpVariable ( )
inline

Definition at line 89 of file IcpVariable.h.

Member Function Documentation

◆ addCandidate()

void smtrat::icp::IcpVariable::addCandidate ( ContractionCandidate *  _candidate)
inline

Definition at line 111 of file IcpVariable.h.

Here is the call graph for this function:

◆ addCandidates()

void smtrat::icp::IcpVariable::addCandidates ( const ContractionCandidates &  _candidates)
inline

Definition at line 121 of file IcpVariable.h.

◆ addOriginalConstraint()

void smtrat::icp::IcpVariable::addOriginalConstraint ( const FormulaT &  _constraint)
inline

Definition at line 132 of file IcpVariable.h.

Here is the call graph for this function:

◆ candidates()

ContractionCandidates& smtrat::icp::IcpVariable::candidates ( )
inline

Definition at line 101 of file IcpVariable.h.

◆ decrementActivity()

void smtrat::icp::IcpVariable::decrementActivity ( )
inline

Definition at line 181 of file IcpVariable.h.

◆ externalLeftBound()

ModuleInput::iterator smtrat::icp::IcpVariable::externalLeftBound ( ) const
inline

Definition at line 257 of file IcpVariable.h.

◆ externalRightBound()

ModuleInput::iterator smtrat::icp::IcpVariable::externalRightBound ( ) const
inline

Definition at line 262 of file IcpVariable.h.

◆ incrementActivity()

void smtrat::icp::IcpVariable::incrementActivity ( )
inline

Definition at line 176 of file IcpVariable.h.

◆ internalLeftBound()

const smtrat::FormulaT& smtrat::icp::IcpVariable::internalLeftBound ( ) const
inline

Definition at line 247 of file IcpVariable.h.

◆ internalRightBound()

const smtrat::FormulaT& smtrat::icp::IcpVariable::internalRightBound ( ) const
inline

Definition at line 252 of file IcpVariable.h.

◆ interval()

const DoubleInterval& smtrat::icp::IcpVariable::interval ( ) const
inline

Definition at line 197 of file IcpVariable.h.

◆ intervalPosition()

EvalDoubleIntervalMap::const_iterator smtrat::icp::IcpVariable::intervalPosition ( ) const
inline

Definition at line 192 of file IcpVariable.h.

◆ is_linear()

bool smtrat::icp::IcpVariable::is_linear ( )
inline

Definition at line 187 of file IcpVariable.h.

Here is the caller graph for this function:

◆ isActive()

bool smtrat::icp::IcpVariable::isActive ( ) const
inline

Definition at line 171 of file IcpVariable.h.

Here is the call graph for this function:

◆ isExternalUpdated()

Updated smtrat::icp::IcpVariable::isExternalUpdated ( ) const
inline

Definition at line 242 of file IcpVariable.h.

◆ isInternalBoundsSet()

Updated smtrat::icp::IcpVariable::isInternalBoundsSet ( ) const
inline

Definition at line 287 of file IcpVariable.h.

◆ isInternalUpdated()

Updated smtrat::icp::IcpVariable::isInternalUpdated ( ) const
inline

Definition at line 237 of file IcpVariable.h.

◆ isOriginal()

bool smtrat::icp::IcpVariable::isOriginal ( ) const
inline

Definition at line 298 of file IcpVariable.h.

Here is the caller graph for this function:

◆ lraVar()

const LRAVariable* smtrat::icp::IcpVariable::lraVar ( ) const
inline

Definition at line 106 of file IcpVariable.h.

◆ operator<()

bool smtrat::icp::IcpVariable::operator< ( IcpVariable const &  rhs) const
inline

Definition at line 303 of file IcpVariable.h.

Here is the call graph for this function:

◆ print()

void smtrat::icp::IcpVariable::print ( std::ostream &  _out = std::cout,
bool  _withContractionCandidates = false 
) const
inline

Definition at line 151 of file IcpVariable.h.

Here is the call graph for this function:

◆ removeOriginalConstraint()

void smtrat::icp::IcpVariable::removeOriginalConstraint ( const FormulaT &  _constraint)
inline

Definition at line 138 of file IcpVariable.h.

Here is the call graph for this function:

◆ setExternalLeftBound()

void smtrat::icp::IcpVariable::setExternalLeftBound ( ModuleInput::iterator  _left)
inline

Definition at line 277 of file IcpVariable.h.

◆ setExternalModified()

void smtrat::icp::IcpVariable::setExternalModified ( )
inline

Definition at line 227 of file IcpVariable.h.

◆ setExternalRightBound()

void smtrat::icp::IcpVariable::setExternalRightBound ( ModuleInput::iterator  _right)
inline

Definition at line 282 of file IcpVariable.h.

◆ setExternalUnmodified()

void smtrat::icp::IcpVariable::setExternalUnmodified ( )
inline

Definition at line 222 of file IcpVariable.h.

◆ setInternalLeftBound()

void smtrat::icp::IcpVariable::setInternalLeftBound ( const smtrat::FormulaT &  _left)
inline

Definition at line 267 of file IcpVariable.h.

◆ setInternalRightBound()

void smtrat::icp::IcpVariable::setInternalRightBound ( const smtrat::FormulaT &  _right)
inline

Definition at line 272 of file IcpVariable.h.

◆ setInternalUnmodified()

void smtrat::icp::IcpVariable::setInternalUnmodified ( )
inline

Definition at line 232 of file IcpVariable.h.

◆ setInterval()

void smtrat::icp::IcpVariable::setInterval ( const DoubleInterval &  _interval)
inline

Definition at line 202 of file IcpVariable.h.

◆ setLraVar()

void smtrat::icp::IcpVariable::setLraVar ( const LRAVariable *  _lraVar)
inline

Definition at line 144 of file IcpVariable.h.

◆ setUnmodified()

void smtrat::icp::IcpVariable::setUnmodified ( )
inline

Definition at line 217 of file IcpVariable.h.

◆ var()

carl::Variable::Arg smtrat::icp::IcpVariable::var ( ) const
inline

Definition at line 96 of file IcpVariable.h.

Here is the caller graph for this function:

Friends And Related Function Documentation

◆ operator<<

std::ostream& operator<< ( std::ostream &  os,
const IcpVariable &  _var 
)
friend

Definition at line 308 of file IcpVariable.h.

Field Documentation

◆ mActivity

unsigned smtrat::icp::IcpVariable::mActivity
private

Definition at line 47 of file IcpVariable.h.

◆ mBoundsSet

std::pair<Updated,Updated> smtrat::icp::IcpVariable::mBoundsSet
private

Definition at line 52 of file IcpVariable.h.

◆ mCandidates

ContractionCandidates smtrat::icp::IcpVariable::mCandidates
private

Definition at line 44 of file IcpVariable.h.

◆ mDefaultPosition

ModuleInput::iterator smtrat::icp::IcpVariable::mDefaultPosition
private

Definition at line 58 of file IcpVariable.h.

◆ mExternalLeftBound

ModuleInput::iterator smtrat::icp::IcpVariable::mExternalLeftBound
private

Definition at line 56 of file IcpVariable.h.

◆ mExternalRightBound

ModuleInput::iterator smtrat::icp::IcpVariable::mExternalRightBound
private

Definition at line 57 of file IcpVariable.h.

◆ mInternalLeftBound

smtrat::FormulaT smtrat::icp::IcpVariable::mInternalLeftBound
private

Definition at line 54 of file IcpVariable.h.

◆ mInternalRightBound

smtrat::FormulaT smtrat::icp::IcpVariable::mInternalRightBound
private

Definition at line 55 of file IcpVariable.h.

◆ mIntervalPos

EvalDoubleIntervalMap::iterator smtrat::icp::IcpVariable::mIntervalPos
private

Definition at line 49 of file IcpVariable.h.

◆ mLinear

bool smtrat::icp::IcpVariable::mLinear
private

Definition at line 48 of file IcpVariable.h.

◆ mLraVar

const LRAVariable* smtrat::icp::IcpVariable::mLraVar
private

Definition at line 46 of file IcpVariable.h.

◆ mOriginal

bool smtrat::icp::IcpVariable::mOriginal
private

Definition at line 43 of file IcpVariable.h.

◆ mOriginalConstraints

FormulaSetT smtrat::icp::IcpVariable::mOriginalConstraints
private

Definition at line 45 of file IcpVariable.h.

◆ mUpdated

std::pair<Updated,Updated> smtrat::icp::IcpVariable::mUpdated
private

Definition at line 53 of file IcpVariable.h.

◆ mVar

carl::Variable smtrat::icp::IcpVariable::mVar
private

Definition at line 42 of file IcpVariable.h.

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