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

Stores a bound, which could be an upper "<= b" or a lower bound ">= b" for a bound value b. More...

#include <Bound.h>

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

Data Structures

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

Public Types

enum  Type { LOWER , UPPER , EQUAL }
 The type of the bound: LOWER = ">=", UPPER = "<=", EQUAL "==". More...
 
typedef carl::PointerSet< Bound< T1, T2 > > BoundSet
 A set of pointer to bounds. More...
 

Public Member Functions

 Bound ()=delete
 
 Bound (const Value< T1 > *const _limit, Variable< T1, T2 > *const _var, Type _type, const FormulaT &_constraint, Bound< T1, T2 >::Info *_boundInfo=NULL, bool _deduced=false)
 
 ~Bound ()
 
bool operator> (const Value< T1 > &_value) const
 
bool operator== (const Value< T1 > &_value) const
 
bool operator< (const Value< T1 > &_value) const
 
bool operator< (const Bound &_bound) const
 
bool operator> (const Bound &_bound) const
 
bool operator== (const T1 &_a) const
 
bool operator> (const T1 &_a) const
 
bool operator< (const T1 &_a) const
 
bool operator>= (const T1 &_a) const
 
bool operator<= (const T1 &_a) const
 
const std::string toString () const
 
void print (bool _withOrigins=false, std::ostream &_out=std::cout, bool _printTypebool=false) const
 
bool deduced () const
 
bool markedAsDeleted () const
 
void markAsDeleted () const
 
void unmarkAsDeleted () const
 
const Value< T1 > & limit () const
 
const Value< T1 > * pLimit () const
 
bool isInfinite () const
 
Variable< T1, T2 > * pVariable () const
 
const Variable< T1, T2 > & variable () const
 
Type type () const
 
bool isWeak () const
 
bool isUpperBound () const
 
bool isLowerBound () const
 
const FormulaT & asConstraint () const
 
bool hasNeqRepresentation () const
 
const FormulaT & neqRepresentation () const
 
void setNeqRepresentation (const FormulaT &_constraint) const
 
void resetNeqRepresentation () const
 
void boundExists () const
 
void setComplement (const Bound< T1, T2 > *_complement) const
 
bool exists () const
 
const std::shared_ptr< std::vector< FormulaT > > & pOrigins () const
 
const std::vector< FormulaT > & origins () const
 
bool isActive () const
 
bool isComplementActive () const
 
bool isUnassigned () const
 
Info * pInfo () const
 
bool isSatisfied (const T1 &_delta) const
 
bool operator>= (const Value< T1 > &v) const
 
bool operator<= (const Value< T1 > &v) const
 

Private Attributes

bool mDeduced
 
bool mMarkedAsDeleted
 
Type mType
 
const Value< T1 > * mLimit
 
Variable< T1, T2 > *const mVar
 
FormulaT mAsConstraint
 
std::shared_ptr< std::vector< FormulaT > > mpOrigins
 
Info * mpInfo
 

Friends

template<typename T3 , typename T4 >
std::ostream & operator<< (std::ostream &_ostream, const Bound< T3, T4 > &_bound)
 

Detailed Description

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

Stores a bound, which could be an upper "<= b" or a lower bound ">= b" for a bound value b.

In the case that "<= b" and ">= b" hold this bound is a so called equal bound represented by "==b".

Definition at line 32 of file Bound.h.

Member Typedef Documentation

◆ BoundSet

template<typename T1 , typename T2 >
typedef carl::PointerSet<Bound<T1, T2> > smtrat::lra::Bound< T1, T2 >::BoundSet

A set of pointer to bounds.

Definition at line 39 of file Bound.h.

Member Enumeration Documentation

◆ Type

template<typename T1 , typename T2 >
enum smtrat::lra::Bound::Type

The type of the bound: LOWER = ">=", UPPER = "<=", EQUAL "==".

Enumerator
LOWER 
UPPER 
EQUAL 

Definition at line 36 of file Bound.h.

Constructor & Destructor Documentation

◆ Bound() [1/2]

template<typename T1 , typename T2 >
smtrat::lra::Bound< T1, T2 >::Bound ( )
delete

◆ Bound() [2/2]

template<typename T1 , typename T2 >
smtrat::lra::Bound< T1, T2 >::Bound ( const Value< T1 > *const  _limit,
Variable< T1, T2 > *const  _var,
Type  _type,
const FormulaT &  _constraint,
Bound< T1, T2 >::Info *  _boundInfo = NULL,
bool  _deduced = false 
)
Parameters
_limit
_var
_type
_constraint
_boundInfo
_deduced

◆ ~Bound()

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

Member Function Documentation

◆ asConstraint()

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

Definition at line 319 of file Bound.h.

◆ boundExists()

template<typename T1 , typename T2 >
void smtrat::lra::Bound< T1, T2 >::boundExists ( ) const
inline

Definition at line 361 of file Bound.h.

◆ deduced()

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

Definition at line 215 of file Bound.h.

◆ exists()

template<typename T1 , typename T2 >
bool smtrat::lra::Bound< T1, T2 >::exists ( ) const
inline

Definition at line 377 of file Bound.h.

Here is the caller graph for this function:

◆ hasNeqRepresentation()

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

Definition at line 327 of file Bound.h.

◆ isActive()

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

Definition at line 401 of file Bound.h.

Here is the caller graph for this function:

◆ isComplementActive()

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

Definition at line 409 of file Bound.h.

Here is the caller graph for this function:

◆ isInfinite()

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

Definition at line 263 of file Bound.h.

Here is the caller graph for this function:

◆ isLowerBound()

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

Definition at line 311 of file Bound.h.

◆ isSatisfied()

template<typename T1 , typename T2 >
bool smtrat::lra::Bound< T1, T2 >::isSatisfied ( const T1 &  _delta) const
inline

Definition at line 427 of file Bound.h.

Here is the call graph for this function:

◆ isUnassigned()

template<typename T1 , typename T2 >
bool smtrat::lra::Bound< T1, T2 >::isUnassigned ( ) const
inline

Definition at line 414 of file Bound.h.

Here is the call graph for this function:

◆ isUpperBound()

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

Definition at line 303 of file Bound.h.

◆ isWeak()

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

Definition at line 295 of file Bound.h.

Here is the call graph for this function:
Here is the caller graph for this function:

◆ limit()

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

Definition at line 247 of file Bound.h.

Here is the caller graph for this function:

◆ markAsDeleted()

template<typename T1 , typename T2 >
void smtrat::lra::Bound< T1, T2 >::markAsDeleted ( ) const
inline
Returns

Definition at line 231 of file Bound.h.

◆ markedAsDeleted()

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

Definition at line 223 of file Bound.h.

◆ neqRepresentation()

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

Definition at line 335 of file Bound.h.

◆ operator<() [1/3]

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

◆ operator<() [2/3]

template<typename T1 , typename T2 >
bool smtrat::lra::Bound< T1, T2 >::operator< ( const T1 &  _a) const
Parameters
_a
Returns

◆ operator<() [3/3]

template<typename T1 , typename T2 >
bool smtrat::lra::Bound< T1, T2 >::operator< ( const Value< T1 > &  _value) const
Parameters
_value
Returns

◆ operator<=() [1/2]

template<typename T1 , typename T2 >
bool smtrat::lra::Bound< T1, T2 >::operator<= ( const T1 &  _a) const
Parameters
_a
Returns

◆ operator<=() [2/2]

template<typename T1 , typename T2 >
bool smtrat::lra::Bound< T1, T2 >::operator<= ( const Value< T1 > &  v) const
inline
Returns

Definition at line 465 of file Bound.h.

◆ operator==() [1/2]

template<typename T1 , typename T2 >
bool smtrat::lra::Bound< T1, T2 >::operator== ( const T1 &  _a) const
Parameters
_a
Returns

◆ operator==() [2/2]

template<typename T1 , typename T2 >
bool smtrat::lra::Bound< T1, T2 >::operator== ( const Value< T1 > &  _value) const
Parameters
_value
Returns

◆ operator>() [1/3]

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

◆ operator>() [2/3]

template<typename T1 , typename T2 >
bool smtrat::lra::Bound< T1, T2 >::operator> ( const T1 &  _a) const
Parameters
_a
Returns

◆ operator>() [3/3]

template<typename T1 , typename T2 >
bool smtrat::lra::Bound< T1, T2 >::operator> ( const Value< T1 > &  _value) const
Parameters
_value
Returns

◆ operator>=() [1/2]

template<typename T1 , typename T2 >
bool smtrat::lra::Bound< T1, T2 >::operator>= ( const T1 &  _a) const
Parameters
_a
Returns

◆ operator>=() [2/2]

template<typename T1 , typename T2 >
bool smtrat::lra::Bound< T1, T2 >::operator>= ( const Value< T1 > &  v) const
inline
Returns

Definition at line 457 of file Bound.h.

◆ origins()

template<typename T1 , typename T2 >
const std::vector<FormulaT>& smtrat::lra::Bound< T1, T2 >::origins ( ) const
inline
Returns

Definition at line 393 of file Bound.h.

◆ pInfo()

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

Definition at line 422 of file Bound.h.

Here is the caller graph for this function:

◆ pLimit()

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

Definition at line 255 of file Bound.h.

◆ pOrigins()

template<typename T1 , typename T2 >
const std::shared_ptr<std::vector<FormulaT> >& smtrat::lra::Bound< T1, T2 >::pOrigins ( ) const
inline
Returns

Definition at line 385 of file Bound.h.

◆ print()

template<typename T1 , typename T2 >
void smtrat::lra::Bound< T1, T2 >::print ( bool  _withOrigins = false,
std::ostream &  _out = std::cout,
bool  _printTypebool = false 
) const
Parameters
_withOrigins
_out
_printTypebool

◆ pVariable()

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

Definition at line 271 of file Bound.h.

◆ resetNeqRepresentation()

template<typename T1 , typename T2 >
void smtrat::lra::Bound< T1, T2 >::resetNeqRepresentation ( ) const
inline

Definition at line 353 of file Bound.h.

◆ setComplement()

template<typename T1 , typename T2 >
void smtrat::lra::Bound< T1, T2 >::setComplement ( const Bound< T1, T2 > *  _complement) const
inline

Definition at line 369 of file Bound.h.

◆ setNeqRepresentation()

template<typename T1 , typename T2 >
void smtrat::lra::Bound< T1, T2 >::setNeqRepresentation ( const FormulaT &  _constraint) const
inline
Parameters
_constraint

Definition at line 344 of file Bound.h.

◆ toString()

template<typename T1 , typename T2 >
const std::string smtrat::lra::Bound< T1, T2 >::toString ( ) const
Returns

◆ type()

template<typename T1 , typename T2 >
Type smtrat::lra::Bound< T1, T2 >::type ( ) const
inline
Returns

Definition at line 287 of file Bound.h.

◆ unmarkAsDeleted()

template<typename T1 , typename T2 >
void smtrat::lra::Bound< T1, T2 >::unmarkAsDeleted ( ) const
inline
Returns

Definition at line 239 of file Bound.h.

◆ variable()

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

Definition at line 279 of file Bound.h.

Here is the caller graph for this function:

Friends And Related Function Documentation

◆ operator<<

template<typename T1 , typename T2 >
template<typename T3 , typename T4 >
std::ostream& operator<< ( std::ostream &  _ostream,
const Bound< T3, T4 > &  _bound 
)
friend
Parameters
_withOrigins
_out
_printTypebool

Field Documentation

◆ mAsConstraint

template<typename T1 , typename T2 >
FormulaT smtrat::lra::Bound< T1, T2 >::mAsConstraint
private

Definition at line 88 of file Bound.h.

◆ mDeduced

template<typename T1 , typename T2 >
bool smtrat::lra::Bound< T1, T2 >::mDeduced
private

Definition at line 78 of file Bound.h.

◆ mLimit

template<typename T1 , typename T2 >
const Value<T1>* smtrat::lra::Bound< T1, T2 >::mLimit
private

Definition at line 84 of file Bound.h.

◆ mMarkedAsDeleted

template<typename T1 , typename T2 >
bool smtrat::lra::Bound< T1, T2 >::mMarkedAsDeleted
mutableprivate

Definition at line 80 of file Bound.h.

◆ mpInfo

template<typename T1 , typename T2 >
Info* smtrat::lra::Bound< T1, T2 >::mpInfo
private

Definition at line 92 of file Bound.h.

◆ mpOrigins

template<typename T1 , typename T2 >
std::shared_ptr<std::vector<FormulaT> > smtrat::lra::Bound< T1, T2 >::mpOrigins
private

Definition at line 90 of file Bound.h.

◆ mType

template<typename T1 , typename T2 >
Type smtrat::lra::Bound< T1, T2 >::mType
private

Definition at line 82 of file Bound.h.

◆ mVar

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

Definition at line 86 of file Bound.h.

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