carl  24.04
Computer ARithmetic Library
Public Member Functions | Static Public Member Functions | Private Types | Private Attributes
carl::BVConstraintPool Class Reference

#include <BVConstraintPool.h>

Inheritance diagram for carl::BVConstraintPool:
Inheritance graph
[legend]
Collaboration diagram for carl::BVConstraintPool:
Collaboration graph
[legend]

Public Member Functions

ConstConstraintPtr create (bool _consistent=true)
 
ConstConstraintPtr create (const BVCompareRelation &_relation, const BVTerm &_lhs, const BVTerm &_rhs)
 
void assignId (ConstraintPtr _constraint, std::size_t _id) override
 Assigns a unique id to the generated element. More...
 
void print () const
 
std::pair< typename FastPointerSet< BVConstraint >::iterator, bool > insert (ElementPtr _element, bool _assertFreshness=false)
 Inserts the given element into the pool, if it does not yet occur in there. More...
 
ConstElementPtr add (ElementPtr _element)
 Adds the given element to the pool, if it does not yet occur in there. More...
 

Static Public Member Functions

static BVConstraintPool & getInstance ()
 Returns the single instance of this class by reference. More...
 

Private Types

using Constraint = BVConstraint
 
using ConstraintPtr = Constraint *
 
using ConstConstraintPtr = const Constraint *
 
using ElementPtr = BVConstraint *
 
using ConstElementPtr = const BVConstraint *
 

Private Attributes

friend Singleton< BVConstraintPool >
 
unsigned mIdAllocator
 id allocator More...
 
FastPointerSet< BVConstraint > mPool
 The formula pool. More...
 
std::mutex mMutexPool
 Mutex to avoid multiple access to the pool. More...
 

Detailed Description

Definition at line 17 of file BVConstraintPool.h.

Member Typedef Documentation

◆ ConstConstraintPtr

using carl::BVConstraintPool::ConstConstraintPtr = const Constraint*
private

Definition at line 23 of file BVConstraintPool.h.

◆ ConstElementPtr

using carl::Pool< BVConstraint >::ConstElementPtr = const BVConstraint *
privateinherited

Definition at line 25 of file Pool.h.

◆ Constraint

using carl::BVConstraintPool::Constraint = BVConstraint
private

Definition at line 21 of file BVConstraintPool.h.

◆ ConstraintPtr

using carl::BVConstraintPool::ConstraintPtr = Constraint*
private

Definition at line 22 of file BVConstraintPool.h.

◆ ElementPtr

using carl::Pool< BVConstraint >::ElementPtr = BVConstraint *
privateinherited

Definition at line 24 of file Pool.h.

Member Function Documentation

◆ add()

ConstElementPtr carl::Pool< BVConstraint >::add ( ElementPtr  _element)
inlineinherited

Adds the given element to the pool, if it does not yet occur in there.

Note, that this method uses the allocator which is locked before calling.

Parameters
_elementThe element to add to the pool.
Returns
The given element, if it did not yet occur in the pool; The equivalent element already occurring in the pool, otherwise.

Definition at line 113 of file Pool.h.

◆ assignId()

void carl::BVConstraintPool::assignId ( ConstraintPtr  ,
std::size_t   
)
overridevirtual

Assigns a unique id to the generated element.

Note that this method serves as a callback for subclasses. The actual assignment of the id is done there.

Parameters
_elementThe element for which to add the id.
_idA unique id.

Reimplemented from carl::Pool< BVConstraint >.

Definition at line 62 of file BVConstraintPool.cpp.

◆ create() [1/2]

BVConstraintPool::ConstConstraintPtr carl::BVConstraintPool::create ( bool  _consistent = true)

Definition at line 12 of file BVConstraintPool.cpp.

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

◆ create() [2/2]

BVConstraintPool::ConstConstraintPtr carl::BVConstraintPool::create ( const BVCompareRelation &  _relation,
const BVTerm &  _lhs,
const BVTerm &  _rhs 
)

Definition at line 17 of file BVConstraintPool.cpp.

Here is the call graph for this function:

◆ getInstance()

static BVConstraintPool & carl::Singleton< BVConstraintPool >::getInstance ( )
inlinestaticinherited

Returns the single instance of this class by reference.

If there is no instance yet, a new one is created.

Definition at line 45 of file Singleton.h.

◆ insert()

std::pair<typename FastPointerSet<BVConstraint >::iterator, bool> carl::Pool< BVConstraint >::insert ( ElementPtr  _element,
bool  _assertFreshness = false 
)
inlineinherited

Inserts the given element into the pool, if it does not yet occur in there.

Parameters
_elementThe element to add to the pool.
_assertFreshnessWhen true, an assertion fails if the element is not fresh (i.e., if it already occurs in the pool).
Returns
The position of the given element in the pool and true, if it did not yet occur in the pool; The position of the equivalent element in the pool and false, otherwise.

Definition at line 89 of file Pool.h.

◆ print()

void carl::Pool< BVConstraint >::print ( ) const
inlineinherited

Definition at line 72 of file Pool.h.

Field Documentation

◆ mIdAllocator

unsigned carl::Pool< BVConstraint >::mIdAllocator
privateinherited

id allocator

Definition at line 31 of file Pool.h.

◆ mMutexPool

std::mutex carl::Pool< BVConstraint >::mMutexPool
mutableprivateinherited

Mutex to avoid multiple access to the pool.

Definition at line 35 of file Pool.h.

◆ mPool

FastPointerSet<BVConstraint > carl::Pool< BVConstraint >::mPool
privateinherited

The formula pool.

Definition at line 33 of file Pool.h.

◆ Singleton< BVConstraintPool >

friend carl::BVConstraintPool::Singleton< BVConstraintPool >
private

Definition at line 19 of file BVConstraintPool.h.

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