The interface for the term library. Provides the storage of of all classes of terms. More...

#include <aterm_pool.h>

Inheritance diagram for atermpp::detail::aterm_pool:

Public Member Functions
	aterm_pool ()

	~aterm_pool ()

function_symbol	create_function_symbol (const std::string &name, const std::size_t arity, const bool check_for_registered_functions=false)
	Creates a function symbol pair (name, arity).

function_symbol	create_function_symbol (std::string &&name, const std::size_t arity, const bool check_for_registered_functions=false)
	Creates a function symbol pair (name, arity).

void	register_thread_aterm_pool (thread_aterm_pool_interface &pool)
	Register a thread specific aterm pool.

void	remove_thread_aterm_pool (thread_aterm_pool_interface &pool)
	Remove thread specific aterm pool.

std::size_t	capacity () const noexcept
	The number of terms that can be stored without resizing.

std::size_t	size () const

void	print_performance_statistics () const
	Prints various performance statistics for the term pool.

aterm &	empty_list () noexcept

const function_symbol &	as_int () noexcept

const function_symbol &	as_list () noexcept

const function_symbol &	as_empty_list () noexcept

void	add_deletion_hook (function_symbol sym, term_callback callback)
	Add a callback that is triggered whenever a term with the given function symbol is destroyed.

void	enable_garbage_collection (bool enable)
	Enable garbage collection when passing true and disable otherwise.

function_symbol_pool &	get_symbol_pool ()

Public Member Functions inherited from mcrl2::utilities::noncopyable
	noncopyable ()=default

	noncopyable (const noncopyable &)=delete

noncopyable &	operator= (const noncopyable &)=delete

Private Member Functions
void	collect (mcrl2::utilities::shared_mutex &mutex)
	Force garbage collection on all storages.

void	created_term (bool allow_collect, mcrl2::utilities::shared_mutex &mutex)
	Triggers garbage collection and resizing when conditions are met.

void	collect_impl (mcrl2::utilities::shared_mutex &mutex)
	Collect garbage on all storages.

bool	create_int (aterm &term, std::size_t val)
	Creates a integral term with the given value.

bool	create_term (aterm &term, const function_symbol &sym)
	Creates a term with the given function symbol.

template<class ... Terms>
bool	create_appl (aterm &term, const function_symbol &sym, const Terms &... arguments)
	Creates a function application with the given function symbol and arguments.

template<typename ForwardIterator >
bool	create_appl_dynamic (aterm &term, const function_symbol &sym, ForwardIterator begin, ForwardIterator end)
	Creates a function application with the given function symbol and the arguments as provided by the given iterator. This function assumes that the arity of the function symbol is equal to the number of elements in the iterator.

template<typename InputIterator , typename ATermConverter >
bool	create_appl_dynamic (aterm &term, const function_symbol &sym, ATermConverter convert_to_aterm, InputIterator begin, InputIterator end)
	Creates a function application with the given function symbol and the arguments as provided by the given iterator. This function assumes that the arity of the function symbol is equal to the number of elements in the iterator.

void	resize_if_needed (mcrl2::utilities::shared_mutex &shared)
	Resizes all storages if necessary.

mcrl2::utilities::shared_mutex &	shared_mutex ()

std::size_t	protection_set_size () const

Private Attributes
std::vector< thread_aterm_pool_interface * >	m_thread_pools
	The set of local aterm pools.

function_symbol_pool	m_function_symbol_pool
	Storage for the function symbols.

integer_term_storage	m_int_storage
	Storage for integral terms.

std::tuple< term_storage, function_application_storage< 1 >, function_application_storage< 2 >, function_application_storage< 3 >, function_application_storage< 4 >, function_application_storage< 5 >, function_application_storage< 6 >, function_application_storage< 7 > >	m_appl_storage
	Storage for function applications with a fixed number of arguments.

arbitrary_function_application_storage	m_appl_dynamic_storage
	Storage for term_appl with a dynamic number of arguments larger than 7.

std::atomic< long >	m_count_until_collection = 0
	Track the number of terms destroyed and reduce the freelist.

std::atomic< long >	m_count_until_resize = 0

std::atomic< bool >	m_enable_garbage_collection = EnableGarbageCollection

mcrl2::utilities::shared_mutex	m_shared_mutex
	Garbage collection is enabled.

aterm_core	m_empty_list
	Represents an empty list.

Friends
class	thread_aterm_pool

Detailed Description

The interface for the term library. Provides the storage of of all classes of terms.

Internally uses different storage objects to store specific classes of terms. For a given term creation it can decide what storage to use at run-time using its function symbol.

Definition at line 81 of file aterm_pool.h.

Constructor & Destructor Documentation

◆ aterm_pool()

atermpp::detail::aterm_pool::aterm_pool ( )

inline

Definition at line 24 of file aterm_pool_implementation.h.

◆ ~aterm_pool()

atermpp::detail::aterm_pool::~aterm_pool ( )

inline

Member Function Documentation

◆ add_deletion_hook()

void atermpp::detail::aterm_pool::add_deletion_hook	(	function_symbol	sym,
		term_callback	callback
	)

inline

Add a callback that is triggered whenever a term with the given function symbol is destroyed.

Definition at line 50 of file aterm_pool_implementation.h.

◆ as_empty_list()

const function_symbol & atermpp::detail::aterm_pool::as_empty_list ( )

inlinenoexcept

Returns: The function symbol used by the term indicating the empty list.

Definition at line 124 of file aterm_pool.h.

◆ as_int()

const function_symbol & atermpp::detail::aterm_pool::as_int ( )

inlinenoexcept

Returns: The function symbol used by integral terms.

Definition at line 118 of file aterm_pool.h.

◆ as_list()

const function_symbol & atermpp::detail::aterm_pool::as_list ( )

inlinenoexcept

Returns: The function symbol used by the list constructor.

Definition at line 121 of file aterm_pool.h.

◆ capacity()

std::size_t atermpp::detail::aterm_pool::capacity ( ) const

inlinenoexcept

The number of terms that can be stored without resizing.

Definition at line 139 of file aterm_pool_implementation.h.

◆ collect()

void atermpp::detail::aterm_pool::collect ( mcrl2::utilities::shared_mutex & mutex )

inlineprivate

Force garbage collection on all storages.

threadsafe

Definition at line 94 of file aterm_pool_implementation.h.

◆ collect_impl()

void atermpp::detail::aterm_pool::collect_impl ( mcrl2::utilities::shared_mutex & mutex )

inlineprivate

Collect garbage on all storages.

threadsafe

Definition at line 199 of file aterm_pool_implementation.h.

◆ create_appl()

template<class ... Terms>

bool atermpp::detail::aterm_pool::create_appl	(	aterm &	term,
		const function_symbol &	sym,
		const Terms &...	arguments
	)

inlineprivate

Creates a function application with the given function symbol and arguments.

Definition at line 303 of file aterm_pool_implementation.h.

◆ create_appl_dynamic() [1/2]

template<typename InputIterator , typename ATermConverter >

bool atermpp::detail::aterm_pool::create_appl_dynamic	(	aterm &	term,
		const function_symbol &	sym,
		ATermConverter	convert_to_aterm,
		InputIterator	begin,
		InputIterator	end
	)

private

Creates a function application with the given function symbol and the arguments as provided by the given iterator. This function assumes that the arity of the function symbol is equal to the number of elements in the iterator.

Definition at line 349 of file aterm_pool_implementation.h.

◆ create_appl_dynamic() [2/2]

template<typename ForwardIterator >

bool atermpp::detail::aterm_pool::create_appl_dynamic	(	aterm &	term,
		const function_symbol &	sym,
		ForwardIterator	begin,
		ForwardIterator	end
	)

private

Creates a function application with the given function symbol and the arguments as provided by the given iterator. This function assumes that the arity of the function symbol is equal to the number of elements in the iterator.

Definition at line 318 of file aterm_pool_implementation.h.

◆ create_function_symbol() [1/2]

function_symbol atermpp::detail::aterm_pool::create_function_symbol	(	const std::string &	name,
		const std::size_t	arity,
		const bool	check_for_registered_functions = `false`
	)

inline

Creates a function symbol pair (name, arity).

See also: function_symbol_pool.

Definition at line 282 of file aterm_pool_implementation.h.

◆ create_function_symbol() [2/2]

function_symbol atermpp::detail::aterm_pool::create_function_symbol	(	std::string &&	name,
		const std::size_t	arity,
		const bool	check_for_registered_functions = `false`
	)

inline

Creates a function symbol pair (name, arity).

See also: function_symbol_pool.

Definition at line 287 of file aterm_pool_implementation.h.

◆ create_int()

bool atermpp::detail::aterm_pool::create_int	(	aterm &	term,
		std::size_t	val
	)

inlineprivate

Creates a integral term with the given value.

Definition at line 292 of file aterm_pool_implementation.h.

◆ create_term()

bool atermpp::detail::aterm_pool::create_term	(	aterm &	term,
		const function_symbol &	sym
	)

inlineprivate

Creates a term with the given function symbol.

Definition at line 297 of file aterm_pool_implementation.h.

◆ created_term()

void atermpp::detail::aterm_pool::created_term	(	bool	allow_collect,
		mcrl2::utilities::shared_mutex &	mutex
	)

inlineprivate

Triggers garbage collection and resizing when conditions are met.

Parameters

allow_collect	Actually perform the garbage collection instead of only updating the counters.
mutex	The shared mutex that should be used for locking if necessary.

threadsafe

Definition at line 171 of file aterm_pool_implementation.h.

◆ empty_list()

aterm & atermpp::detail::aterm_pool::empty_list ( )

inlinenoexcept

Returns: A global term that indicates the empty list.

Definition at line 115 of file aterm_pool.h.

◆ enable_garbage_collection()

void atermpp::detail::aterm_pool::enable_garbage_collection ( bool enable )

inline

Enable garbage collection when passing true and disable otherwise.

Definition at line 130 of file aterm_pool.h.

◆ get_symbol_pool()

function_symbol_pool & atermpp::detail::aterm_pool::get_symbol_pool ( )

inline

Definition at line 132 of file aterm_pool.h.

◆ print_performance_statistics()

void atermpp::detail::aterm_pool::print_performance_statistics ( ) const

inline

Prints various performance statistics for the term pool.

Definition at line 118 of file aterm_pool_implementation.h.

◆ protection_set_size()

std::size_t atermpp::detail::aterm_pool::protection_set_size ( ) const

inlineprivate

Returns: The total number of term variables residing in the protection sets.

Definition at line 419 of file aterm_pool_implementation.h.

◆ register_thread_aterm_pool()

void atermpp::detail::aterm_pool::register_thread_aterm_pool ( thread_aterm_pool_interface & pool )

inline

Register a thread specific aterm pool.

threadsafe

Definition at line 100 of file aterm_pool_implementation.h.

◆ remove_thread_aterm_pool()

void atermpp::detail::aterm_pool::remove_thread_aterm_pool ( thread_aterm_pool_interface & pool )

inline

Remove thread specific aterm pool.

threadsafe

Definition at line 106 of file aterm_pool_implementation.h.

◆ resize_if_needed()

void atermpp::detail::aterm_pool::resize_if_needed ( mcrl2::utilities::shared_mutex & shared )

inlineprivate

Resizes all storages if necessary.

threadsafe

Definition at line 379 of file aterm_pool_implementation.h.

◆ shared_mutex()

mcrl2::utilities::shared_mutex & atermpp::detail::aterm_pool::shared_mutex ( )

inlineprivate

Definition at line 183 of file aterm_pool.h.

◆ size()

std::size_t atermpp::detail::aterm_pool::size ( ) const

inline

Returns: The total number of terms residing in the pool.

Definition at line 154 of file aterm_pool_implementation.h.

Friends And Related Symbol Documentation

◆ thread_aterm_pool

friend class thread_aterm_pool

friend

Definition at line 87 of file aterm_pool.h.

Member Data Documentation

◆ m_appl_dynamic_storage

arbitrary_function_application_storage atermpp::detail::aterm_pool::m_appl_dynamic_storage

private

Storage for term_appl with a dynamic number of arguments larger than 7.

Definition at line 210 of file aterm_pool.h.

◆ m_appl_storage

std::tuple< term_storage, function_application_storage<1>, function_application_storage<2>, function_application_storage<3>, function_application_storage<4>, function_application_storage<5>, function_application_storage<6>, function_application_storage<7> > atermpp::detail::aterm_pool::m_appl_storage

private

Storage for function applications with a fixed number of arguments.

Definition at line 207 of file aterm_pool.h.

◆ m_count_until_collection

std::atomic<long> atermpp::detail::aterm_pool::m_count_until_collection = 0

private

Track the number of terms destroyed and reduce the freelist.

Definition at line 213 of file aterm_pool.h.

◆ m_count_until_resize

std::atomic<long> atermpp::detail::aterm_pool::m_count_until_resize = 0

private

Definition at line 214 of file aterm_pool.h.

◆ m_empty_list

aterm_core atermpp::detail::aterm_pool::m_empty_list

private

Represents an empty list.

Definition at line 222 of file aterm_pool.h.

◆ m_enable_garbage_collection

std::atomic<bool> atermpp::detail::aterm_pool::m_enable_garbage_collection = EnableGarbageCollection

private

Definition at line 216 of file aterm_pool.h.

◆ m_function_symbol_pool

function_symbol_pool atermpp::detail::aterm_pool::m_function_symbol_pool

private

Storage for the function symbols.

Definition at line 192 of file aterm_pool.h.

◆ m_int_storage

integer_term_storage atermpp::detail::aterm_pool::m_int_storage

private

Storage for integral terms.

Definition at line 195 of file aterm_pool.h.

◆ m_shared_mutex

mcrl2::utilities::shared_mutex atermpp::detail::aterm_pool::m_shared_mutex

private

Garbage collection is enabled.

All the shared mutexes.

Definition at line 219 of file aterm_pool.h.

◆ m_thread_pools

std::vector<thread_aterm_pool_interface* > atermpp::detail::aterm_pool::m_thread_pools

private

The set of local aterm pools.

Definition at line 189 of file aterm_pool.h.

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

atermpp/include/mcrl2/atermpp/detail/aterm_pool.h
atermpp/include/mcrl2/atermpp/detail/aterm_pool_implementation.h

Public Member Functions

Private Member Functions

Private Attributes

Friends

Detailed Description

Constructor & Destructor Documentation

◆ aterm_pool()

◆ ~aterm_pool()

Member Function Documentation

◆ add_deletion_hook()

◆ as_empty_list()

◆ as_int()

◆ as_list()

◆ capacity()

◆ collect()

◆ collect_impl()

◆ create_appl()

◆ create_appl_dynamic() [1/2]

◆ create_appl_dynamic() [2/2]

◆ create_function_symbol() [1/2]

◆ create_function_symbol() [2/2]

◆ create_int()

◆ create_term()

◆ created_term()

◆ empty_list()

◆ enable_garbage_collection()

◆ get_symbol_pool()

◆ print_performance_statistics()

◆ protection_set_size()

◆ register_thread_aterm_pool()

◆ remove_thread_aterm_pool()

◆ resize_if_needed()

◆ shared_mutex()

◆ size()

Friends And Related Symbol Documentation

◆ thread_aterm_pool

Member Data Documentation

◆ m_appl_dynamic_storage

◆ m_appl_storage

◆ m_count_until_collection

◆ m_count_until_resize

◆ m_empty_list

◆ m_enable_garbage_collection

◆ m_function_symbol_pool

◆ m_int_storage

◆ m_shared_mutex

◆ m_thread_pools