#include <BVTermPool.h>

Inheritance diagram for carl::BVTermPool:

[legend]

Collaboration diagram for carl::BVTermPool:

[legend]

Public Types
using	Term = BVTermContent

using	TermPtr = Term *

using	ConstTermPtr = const Term *

Public Member Functions
	BVTermPool ()

	BVTermPool (const BVTermPool &)=delete

BVTermPool &	operator= (const BVTermPool &)=delete

ConstTermPtr	create ()

ConstTermPtr	create (BVTermType _type, BVValue &&_value)

ConstTermPtr	create (BVTermType _type, const BVVariable &_variable)

ConstTermPtr	create (BVTermType _type, const BVTerm &_operand, std::size_t _index=0)

ConstTermPtr	create (BVTermType _type, const BVTerm &_first, const BVTerm &_second)

ConstTermPtr	create (BVTermType _type, const BVTerm &_operand, std::size_t _first, std::size_t _last)

void	assignId (TermPtr _term, std::size_t _id) override
	Assigns a unique id to the generated element. More...

void	print () const

std::pair< typename FastPointerSet< BVTermContent >::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 BVTermPool &	getInstance ()
	Returns the single instance of this class by reference. More...

Private Types
using	ElementPtr = BVTermContent *

using	ConstElementPtr = const BVTermContent *

Private Attributes
friend	Singleton< BVTermPool >

ConstTermPtr	mpInvalid

unsigned	mIdAllocator
	id allocator More...

FastPointerSet< BVTermContent >	mPool
	The formula pool. More...

std::mutex	mMutexPool
	Mutex to avoid multiple access to the pool. More...

Detailed Description

Definition at line 13 of file BVTermPool.h.

Member Typedef Documentation

◆ ConstElementPtr

using carl::Pool< BVTermContent >::ConstElementPtr = const BVTermContent *

privateinherited

Definition at line 25 of file Pool.h.

◆ ConstTermPtr

using carl::BVTermPool::ConstTermPtr = const Term*

Definition at line 20 of file BVTermPool.h.

◆ ElementPtr

using carl::Pool< BVTermContent >::ElementPtr = BVTermContent *

privateinherited

Definition at line 24 of file Pool.h.

◆ Term

using carl::BVTermPool::Term = BVTermContent

Definition at line 18 of file BVTermPool.h.

◆ TermPtr

using carl::BVTermPool::TermPtr = Term*

Definition at line 19 of file BVTermPool.h.

Constructor & Destructor Documentation

◆ BVTermPool() [1/2]

carl::BVTermPool::BVTermPool ( )

Definition at line 11 of file BVTermPool.cpp.

◆ BVTermPool() [2/2]

carl::BVTermPool::BVTermPool ( const BVTermPool & )

delete

Member Function Documentation

◆ add()

ConstElementPtr carl::Pool< BVTermContent >::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

_element The 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::BVTermPool::assignId	(	TermPtr	,
		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

_element	The element for which to add the id.
_id	A unique id.

Reimplemented from carl::Pool< BVTermContent >.

Definition at line 176 of file BVTermPool.cpp.

◆ create() [1/6]

BVTermPool::ConstTermPtr carl::BVTermPool::create ( )

Definition at line 16 of file BVTermPool.cpp.

Here is the caller graph for this function: