carl  24.04
Computer ARithmetic Library
Public Member Functions | Static Public Member Functions | Private Member Functions | Private Attributes | Friends
carl::BVConstraint Class Reference

#include <BVConstraint.h>

Collaboration diagram for carl::BVConstraint:
Collaboration graph
[legend]

Public Member Functions

const BVTerm & lhs () const
 
const BVTerm & rhs () const
 
BVCompareRelation relation () const
 
std::size_t id () const
 
std::size_t hash () const
 
std::size_t complexity () const
 
void gatherBVVariables (std::set< BVVariable > &vars) const
 
void gatherVariables (carlVariables &vars) const
 
bool is_constant () const
 
bool isAlwaysConsistent () const
 
bool isAlwaysInconsistent () const
 

Static Public Member Functions

static BVConstraint create (bool _consistent=true)
 
static BVConstraint create (const BVCompareRelation &_relation, const BVTerm &_lhs, const BVTerm &_rhs)
 

Private Member Functions

 BVConstraint (bool _consistent=true)
 
 BVConstraint (const BVCompareRelation &_relation, const BVTerm &_lhs, const BVTerm &_rhs)
 Constructs the constraint: _lhs _relation _rhs. More...
 

Private Attributes

BVCompareRelation mRelation
 The relation for comparing left- and right-hand side. More...
 
BVTerm mLhs
 The left-hand side of the (in)equality. More...
 
BVTerm mRhs
 The right-hand size of the (in)equality. More...
 
std::size_t mHash = 0
 The hash value. More...
 
std::size_t mId = 0
 The unique id. More...
 

Friends

class BVConstraintPool
 

Detailed Description

Definition at line 16 of file BVConstraint.h.

Constructor & Destructor Documentation

◆ BVConstraint() [1/2]

carl::BVConstraint::BVConstraint ( bool  _consistent = true)
inlineexplicitprivate

Definition at line 31 of file BVConstraint.h.

◆ BVConstraint() [2/2]

carl::BVConstraint::BVConstraint ( const BVCompareRelation &  _relation,
const BVTerm &  _lhs,
const BVTerm &  _rhs 
)
inlineprivate

Constructs the constraint: _lhs _relation _rhs.

Parameters
_lhsThe bit-vector term to be used as left-hand side of the constraint.
_rhsThe bit-vector term to be used as right-hand side of the constraint.
_relationThe relation symbol to be used for the constraint.

Definition at line 40 of file BVConstraint.h.

Here is the call graph for this function:

Member Function Documentation

◆ complexity()

std::size_t carl::BVConstraint::complexity ( ) const
inline
Returns
An approximation of the complexity of this bit vector constraint.

Definition at line 90 of file BVConstraint.h.

Here is the call graph for this function:

◆ create() [1/2]

BVConstraint carl::BVConstraint::create ( bool  _consistent = true)
static

Definition at line 10 of file BVConstraint.cpp.

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

◆ create() [2/2]

BVConstraint carl::BVConstraint::create ( const BVCompareRelation &  _relation,
const BVTerm &  _lhs,
const BVTerm &  _rhs 
)
static

Definition at line 14 of file BVConstraint.cpp.

Here is the call graph for this function:

◆ gatherBVVariables()

void carl::BVConstraint::gatherBVVariables ( std::set< BVVariable > &  vars) const
inline

Definition at line 94 of file BVConstraint.h.

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

◆ gatherVariables()

void carl::BVConstraint::gatherVariables ( carlVariables &  vars) const
inline

Definition at line 99 of file BVConstraint.h.

Here is the call graph for this function:

◆ hash()

std::size_t carl::BVConstraint::hash ( ) const
inline
Returns
A hash value for this constraint.

Definition at line 83 of file BVConstraint.h.

Here is the caller graph for this function:

◆ id()

std::size_t carl::BVConstraint::id ( ) const
inline
Returns
The unique id of this constraint.

Definition at line 76 of file BVConstraint.h.

Here is the caller graph for this function:

◆ is_constant()

bool carl::BVConstraint::is_constant ( ) const
inline

Definition at line 107 of file BVConstraint.h.

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

◆ isAlwaysConsistent()

bool carl::BVConstraint::isAlwaysConsistent ( ) const
inline

Definition at line 111 of file BVConstraint.h.

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

◆ isAlwaysInconsistent()

bool carl::BVConstraint::isAlwaysInconsistent ( ) const
inline

Definition at line 115 of file BVConstraint.h.

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

◆ lhs()

const BVTerm& carl::BVConstraint::lhs ( ) const
inline
Returns
The bit-vector term being the left-hand side of this constraint.

Definition at line 55 of file BVConstraint.h.

Here is the caller graph for this function:

◆ relation()

BVCompareRelation carl::BVConstraint::relation ( ) const
inline
Returns
The relation symbol of this constraint.

Definition at line 69 of file BVConstraint.h.

Here is the caller graph for this function:

◆ rhs()

const BVTerm& carl::BVConstraint::rhs ( ) const
inline
Returns
The bit-vector term being the right-hand side of this constraint.

Definition at line 62 of file BVConstraint.h.

Here is the caller graph for this function:

Friends And Related Function Documentation

◆ BVConstraintPool

friend class BVConstraintPool
friend

Definition at line 17 of file BVConstraint.h.

Field Documentation

◆ mHash

std::size_t carl::BVConstraint::mHash = 0
private

The hash value.

Definition at line 27 of file BVConstraint.h.

◆ mId

std::size_t carl::BVConstraint::mId = 0
private

The unique id.

Definition at line 29 of file BVConstraint.h.

◆ mLhs

BVTerm carl::BVConstraint::mLhs
private

The left-hand side of the (in)equality.

Definition at line 23 of file BVConstraint.h.

◆ mRelation

BVCompareRelation carl::BVConstraint::mRelation
private

The relation for comparing left- and right-hand side.

Definition at line 21 of file BVConstraint.h.

◆ mRhs

BVTerm carl::BVConstraint::mRhs
private

The right-hand size of the (in)equality.

Definition at line 25 of file BVConstraint.h.

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