This class provides for all types of term storage. It also provides garbage collection via its mark and sweep functions. More...

#include <aterm_pool_storage.h>

Inheritance diagram for atermpp::detail::aterm_pool_storage< Element, Hash, Equals, N >:

Public Types
using	unordered_set = mcrl2::utilities::unordered_set< Element, Hash, Equals, typename std::conditional_t< N==DynamicNumberOfArguments, atermpp::detail::_aterm_appl_allocator<>, typename std::conditional_t< EnableBlockAllocator, mcrl2::utilities::block_allocator< Element, 1024, mcrl2::utilities::detail::GlobalThreadSafe >, std::allocator< Element > > >, mcrl2::utilities::detail::GlobalThreadSafe, false >

using	iterator = typename unordered_set::iterator

using	const_iterator = typename unordered_set::const_iterator

Public Member Functions
	aterm_pool_storage (aterm_pool &pool)

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.

std::size_t	capacity () const noexcept

bool	create_int (aterm &term, std::size_t value)
	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_iterator (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 N and that the iterator has exactly N elements.

template<typename InputIterator , typename TermConverter >
bool	create_appl_iterator (aterm &term, const function_symbol &sym, TermConverter converter, 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 N and that the iterator has exactly N elements.

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.

template<typename InputIterator , typename TermConverter , typename std::enable_if<!std::is_convertible< typename std::invoke_result< TermConverter, typename InputIterator::value_type >::type, aterm >::value, void >::type * = nullptr>
bool	create_appl_dynamic (aterm &term, const function_symbol &sym, TermConverter converter, InputIterator begin, InputIterator end)
	Creates a function application with the given function symbol and the arguments as provided by the given iterator, but the converter is applied to each argument.

template<typename InputIterator , typename TermConverter , typename std::enable_if< std::is_convertible< typename std::invoke_result< TermConverter, typename InputIterator::value_type >::type, aterm >::value, void >::type * = nullptr>
bool	create_appl_dynamic (aterm &term, const function_symbol &sym, TermConverter converter, InputIterator begin, InputIterator end)
	Creates a function application with the given function symbol and the arguments as provided by the given iterator, but the converter is applied to each argument.

template<typename InputIterator , typename TermConverter , typename std::enable_if< std::is_same< typename std::invoke_result< TermConverter, typename InputIterator::value_type &, typename InputIterator::value_type >::type, void >::value, void >::type * = nullptr>
bool	create_appl_dynamic (aterm &term, const function_symbol &sym, TermConverter converter, InputIterator begin, InputIterator end)
	Creates a function application with the given function symbol and the arguments as provided by the given iterator, but the converter is applied to each argument.

void	print_performance_stats (const char *identifier) const
	Prints various performance statistics for this storage.

void	sweep ()
	sweep Destroys all terms that are not reachable. Requires that mark() was called first.

void	resize_if_needed ()
	Resizes the hash table if necessary.

std::size_t	size () const

	aterm_pool_storage (const aterm_pool_storage &other)
	A fake copy constructor to fix the issues with GCC 4 and 5.

bool	verify_mark ()
	Check that all arguments of a term application are marked properly.

bool	verify_sweep ()
	Check that all arguments of a term application are marked properly.

Private Types
using	callback_pair = std::pair< function_symbol, term_callback >

Private Member Functions
void	call_deletion_hook (unprotected_aterm_core term)
	Calls the deletion hook attached to the function symbol of this term. \threadsafe.

iterator	destroy (iterator it)
	Removes an element from the unordered set and deallocates it.

template<typename ... Args>
bool	emplace (aterm_core &term, Args &&... args)
	Inserts a term constructed by the given arguments, checks for existing term.

constexpr bool	is_dynamic_storage () const

template<std::size_t Arity = N>
bool	verify_term (const _aterm &term)
	Verify that the given term was constructed properly.

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

	noncopyable (const noncopyable &)=delete

noncopyable &	operator= (const noncopyable &)=delete

Private Attributes
aterm_pool &	m_pool
	The pool that this storage belongs to.

unordered_set	m_term_set
	This is the set of term pointers to keep the terms unique.

std::vector< callback_pair >	m_deletion_hooks
	This array stores creation, resp deletion, hooks for function symbols.

std::stack< std::reference_wrapper< _aterm > >	todo
	A reusable todo stack.

mcrl2::utilities::cache_metric	m_term_metric
	Count the number of times a term has been found in or is added to the set.

std::size_t	m_erasedBlocks = 0

Friends
class	aterm_pool
	The local pool is a friend class so it can mark terms.

Detailed Description

template<typename Element, typename Hash = aterm_hasher<>, typename Equals = aterm_equals<>, std::size_t N = DynamicNumberOfArguments>
class atermpp::detail::aterm_pool_storage< Element, Hash, Equals, N >

This class provides for all types of term storage. It also provides garbage collection via its mark and sweep functions.

Internally a hash set is used to ensure that the created terms are unique.

Definition at line 43 of file aterm_pool_storage.h.

Member Typedef Documentation

◆ callback_pair

template<typename Element , typename Hash = aterm_hasher<>, typename Equals = aterm_equals<>, std::size_t N = DynamicNumberOfArguments>

using atermpp::detail::aterm_pool_storage< Element, Hash, Equals, N >::callback_pair = std::pair<function_symbol, term_callback>

private

Definition at line 179 of file aterm_pool_storage.h.

◆ const_iterator

template<typename Element , typename Hash = aterm_hasher<>, typename Equals = aterm_equals<>, std::size_t N = DynamicNumberOfArguments>

using atermpp::detail::aterm_pool_storage< Element, Hash, Equals, N >::const_iterator = typename unordered_set::const_iterator

Definition at line 59 of file aterm_pool_storage.h.

◆ iterator

template<typename Element , typename Hash = aterm_hasher<>, typename Equals = aterm_equals<>, std::size_t N = DynamicNumberOfArguments>

using atermpp::detail::aterm_pool_storage< Element, Hash, Equals, N >::iterator = typename unordered_set::iterator

Definition at line 58 of file aterm_pool_storage.h.

◆ unordered_set

template<typename Element , typename Hash = aterm_hasher<>, typename Equals = aterm_equals<>, std::size_t N = DynamicNumberOfArguments>

using atermpp::detail::aterm_pool_storage< Element, Hash, Equals, N >::unordered_set = mcrl2::utilities::unordered_set< Element, Hash, Equals, typename std::conditional_t<N == DynamicNumberOfArguments, atermpp::detail::_aterm_appl_allocator<>, typename std::conditional_t<EnableBlockAllocator, mcrl2::utilities::block_allocator<Element, 1024, mcrl2::utilities::detail::GlobalThreadSafe>, std::allocator<Element> > >, mcrl2::utilities::detail::GlobalThreadSafe, false>

Definition at line 46 of file aterm_pool_storage.h.

Constructor & Destructor Documentation

◆ aterm_pool_storage() [1/2]

template<typename Element , typename Hash = aterm_hasher<>, typename Equals = aterm_equals<>, std::size_t N = DynamicNumberOfArguments>

atermpp::detail::aterm_pool_storage< Element, Hash, Equals, N >::aterm_pool_storage ( aterm_pool & pool )

◆ aterm_pool_storage() [2/2]

template<typename Element , typename Hash = aterm_hasher<>, typename Equals = aterm_equals<>, std::size_t N = DynamicNumberOfArguments>

atermpp::detail::aterm_pool_storage< Element, Hash, Equals, N >::aterm_pool_storage ( const aterm_pool_storage< Element, Hash, Equals, N > & other )

inline

A fake copy constructor to fix the issues with GCC 4 and 5.

Definition at line 167 of file aterm_pool_storage.h.

Member Function Documentation

◆ add_deletion_hook()

template<typename Element , typename Hash = aterm_hasher<>, typename Equals = aterm_equals<>, std::size_t N = DynamicNumberOfArguments>

void atermpp::detail::aterm_pool_storage< Element, Hash, Equals, N >::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.

◆ call_deletion_hook()

template<typename Element , typename Hash = aterm_hasher<>, typename Equals = aterm_equals<>, std::size_t N = DynamicNumberOfArguments>

void atermpp::detail::aterm_pool_storage< Element, Hash, Equals, N >::call_deletion_hook ( unprotected_aterm_core term )

private

Calls the deletion hook attached to the function symbol of this term. \threadsafe.

◆ capacity()

template<typename Element , typename Hash = aterm_hasher<>, typename Equals = aterm_equals<>, std::size_t N = DynamicNumberOfArguments>

std::size_t atermpp::detail::aterm_pool_storage< Element, Hash, Equals, N >::capacity ( ) const

inlinenoexcept

Returns: The total number of terms that can be stored without resizing.

Definition at line 70 of file aterm_pool_storage.h.

◆ create_appl()

template<typename Element , typename Hash = aterm_hasher<>, typename Equals = aterm_equals<>, std::size_t N = DynamicNumberOfArguments>

template<class ... Terms>

bool atermpp::detail::aterm_pool_storage< Element, Hash, Equals, N >::create_appl	(	aterm &	term,
		const function_symbol &	sym,
		const Terms &...	arguments
	)

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

◆ create_appl_dynamic() [1/4]

template<typename Element , typename Hash = aterm_hasher<>, typename Equals = aterm_equals<>, std::size_t N = DynamicNumberOfArguments>

template<typename ForwardIterator >

bool atermpp::detail::aterm_pool_storage< Element, Hash, Equals, N >::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.

◆ create_appl_dynamic() [2/4]

template<typename Element , typename Hash = aterm_hasher<>, typename Equals = aterm_equals<>, std::size_t N = DynamicNumberOfArguments>

template<typename InputIterator , typename TermConverter , typename std::enable_if<!std::is_convertible< typename std::invoke_result< TermConverter, typename InputIterator::value_type >::type, aterm >::value, void >::type * = nullptr>

bool atermpp::detail::aterm_pool_storage< Element, Hash, Equals, N >::create_appl_dynamic	(	aterm &	term,
		const function_symbol &	sym,
		TermConverter	converter,
		InputIterator	begin,
		InputIterator	end
	)

Creates a function application with the given function symbol and the arguments as provided by the given iterator, but the converter is applied to each argument.

◆ create_appl_dynamic() [3/4]

template<typename Element , typename Hash = aterm_hasher<>, typename Equals = aterm_equals<>, std::size_t N = DynamicNumberOfArguments>

template<typename InputIterator , typename TermConverter , typename std::enable_if< std::is_convertible< typename std::invoke_result< TermConverter, typename InputIterator::value_type >::type, aterm >::value, void >::type * = nullptr>

bool atermpp::detail::aterm_pool_storage< Element, Hash, Equals, N >::create_appl_dynamic	(	aterm &	term,
		const function_symbol &	sym,
		TermConverter	converter,
		InputIterator	begin,
		InputIterator	end
	)

Creates a function application with the given function symbol and the arguments as provided by the given iterator, but the converter is applied to each argument.

◆ create_appl_dynamic() [4/4]

template<typename Element , typename Hash = aterm_hasher<>, typename Equals = aterm_equals<>, std::size_t N = DynamicNumberOfArguments>

template<typename InputIterator , typename TermConverter , typename std::enable_if< std::is_same< typename std::invoke_result< TermConverter, typename InputIterator::value_type &, typename InputIterator::value_type >::type, void >::value, void >::type * = nullptr>

bool atermpp::detail::aterm_pool_storage< Element, Hash, Equals, N >::create_appl_dynamic	(	aterm &	term,
		const function_symbol &	sym,
		TermConverter	converter,
		InputIterator	begin,
		InputIterator	end
	)

Creates a function application with the given function symbol and the arguments as provided by the given iterator, but the converter is applied to each argument.

◆ create_appl_iterator() [1/2]

template<typename Element , typename Hash = aterm_hasher<>, typename Equals = aterm_equals<>, std::size_t N = DynamicNumberOfArguments>

template<typename ForwardIterator >

bool atermpp::detail::aterm_pool_storage< Element, Hash, Equals, N >::create_appl_iterator	(	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 N and that the iterator has exactly N elements.

◆ create_appl_iterator() [2/2]

template<typename Element , typename Hash = aterm_hasher<>, typename Equals = aterm_equals<>, std::size_t N = DynamicNumberOfArguments>

template<typename InputIterator , typename TermConverter >

bool atermpp::detail::aterm_pool_storage< Element, Hash, Equals, N >::create_appl_iterator	(	aterm &	term,
		const function_symbol &	sym,
		TermConverter	converter,
		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 N and that the iterator has exactly N elements.

◆ create_int()

template<typename Element , typename Hash = aterm_hasher<>, typename Equals = aterm_equals<>, std::size_t N = DynamicNumberOfArguments>

bool atermpp::detail::aterm_pool_storage< Element, Hash, Equals, N >::create_int	(	aterm &	term,
		std::size_t	value
	)

Creates a integral term with the given value.

◆ create_term()

template<typename Element , typename Hash = aterm_hasher<>, typename Equals = aterm_equals<>, std::size_t N = DynamicNumberOfArguments>

bool atermpp::detail::aterm_pool_storage< Element, Hash, Equals, N >::create_term	(	aterm &	term,
		const function_symbol &	sym
	)

Creates a term with the given function symbol.

◆ destroy()

template<typename Element , typename Hash = aterm_hasher<>, typename Equals = aterm_equals<>, std::size_t N = DynamicNumberOfArguments>

iterator atermpp::detail::aterm_pool_storage< Element, Hash, Equals, N >::destroy ( iterator it )

private

Removes an element from the unordered set and deallocates it.

◆ emplace()

template<typename Element , typename Hash = aterm_hasher<>, typename Equals = aterm_equals<>, std::size_t N = DynamicNumberOfArguments>

template<typename ... Args>

bool atermpp::detail::aterm_pool_storage< Element, Hash, Equals, N >::emplace	(	aterm_core &	term,
		Args &&...	args
	)

private

Inserts a term constructed by the given arguments, checks for existing term.

◆ is_dynamic_storage()

template<typename Element , typename Hash = aterm_hasher<>, typename Equals = aterm_equals<>, std::size_t N = DynamicNumberOfArguments>

constexpr bool atermpp::detail::aterm_pool_storage< Element, Hash, Equals, N >::is_dynamic_storage ( ) const

constexprprivate

Returns: True if and only if this term storage can store term applications with a dynamic number of arguments.

◆ print_performance_stats()

template<typename Element , typename Hash = aterm_hasher<>, typename Equals = aterm_equals<>, std::size_t N = DynamicNumberOfArguments>

void atermpp::detail::aterm_pool_storage< Element, Hash, Equals, N >::print_performance_stats ( const char * identifier ) const

Prints various performance statistics for this storage.

Parameters

identifier A string to identify the printed message for this storage.

◆ resize_if_needed()

template<typename Element , typename Hash = aterm_hasher<>, typename Equals = aterm_equals<>, std::size_t N = DynamicNumberOfArguments>

void atermpp::detail::aterm_pool_storage< Element, Hash, Equals, N >::resize_if_needed ( )

Resizes the hash table if necessary.

◆ size()

template<typename Element , typename Hash = aterm_hasher<>, typename Equals = aterm_equals<>, std::size_t N = DynamicNumberOfArguments>

std::size_t atermpp::detail::aterm_pool_storage< Element, Hash, Equals, N >::size ( ) const

inline

Returns: The number of terms stored in this storage.

Definition at line 164 of file aterm_pool_storage.h.

◆ sweep()

template<typename Element , typename Hash = aterm_hasher<>, typename Equals = aterm_equals<>, std::size_t N = DynamicNumberOfArguments>

void atermpp::detail::aterm_pool_storage< Element, Hash, Equals, N >::sweep ( )

sweep Destroys all terms that are not reachable. Requires that mark() was called first.

◆ verify_mark()

template<typename Element , typename Hash = aterm_hasher<>, typename Equals = aterm_equals<>, std::size_t N = DynamicNumberOfArguments>

bool atermpp::detail::aterm_pool_storage< Element, Hash, Equals, N >::verify_mark ( )

Check that all arguments of a term application are marked properly.

◆ verify_sweep()

template<typename Element , typename Hash = aterm_hasher<>, typename Equals = aterm_equals<>, std::size_t N = DynamicNumberOfArguments>

bool atermpp::detail::aterm_pool_storage< Element, Hash, Equals, N >::verify_sweep ( )

Check that all arguments of a term application are marked properly.

◆ verify_term()

template<typename Element , typename Hash = aterm_hasher<>, typename Equals = aterm_equals<>, std::size_t N = DynamicNumberOfArguments>

template<std::size_t Arity = N>

bool atermpp::detail::aterm_pool_storage< Element, Hash, Equals, N >::verify_term ( const _aterm & term )

private

Verify that the given term was constructed properly.

Friends And Related Symbol Documentation

◆ aterm_pool

template<typename Element , typename Hash = aterm_hasher<>, typename Equals = aterm_equals<>, std::size_t N = DynamicNumberOfArguments>

friend class aterm_pool

friend

The local pool is a friend class so it can mark terms.

Definition at line 62 of file aterm_pool_storage.h.

Member Data Documentation

◆ m_deletion_hooks

template<typename Element , typename Hash = aterm_hasher<>, typename Equals = aterm_equals<>, std::size_t N = DynamicNumberOfArguments>

std::vector<callback_pair> atermpp::detail::aterm_pool_storage< Element, Hash, Equals, N >::m_deletion_hooks

private

This array stores creation, resp deletion, hooks for function symbols.

Definition at line 208 of file aterm_pool_storage.h.

◆ m_erasedBlocks

template<typename Element , typename Hash = aterm_hasher<>, typename Equals = aterm_equals<>, std::size_t N = DynamicNumberOfArguments>

std::size_t atermpp::detail::aterm_pool_storage< Element, Hash, Equals, N >::m_erasedBlocks = 0

private

Definition at line 216 of file aterm_pool_storage.h.

◆ m_pool

template<typename Element , typename Hash = aterm_hasher<>, typename Equals = aterm_equals<>, std::size_t N = DynamicNumberOfArguments>

aterm_pool& atermpp::detail::aterm_pool_storage< Element, Hash, Equals, N >::m_pool

private

The pool that this storage belongs to.

Definition at line 201 of file aterm_pool_storage.h.

◆ m_term_metric

template<typename Element , typename Hash = aterm_hasher<>, typename Equals = aterm_equals<>, std::size_t N = DynamicNumberOfArguments>

mcrl2::utilities::cache_metric atermpp::detail::aterm_pool_storage< Element, Hash, Equals, N >::m_term_metric

private

Count the number of times a term has been found in or is added to the set.

Definition at line 215 of file aterm_pool_storage.h.

◆ m_term_set

template<typename Element , typename Hash = aterm_hasher<>, typename Equals = aterm_equals<>, std::size_t N = DynamicNumberOfArguments>

unordered_set atermpp::detail::aterm_pool_storage< Element, Hash, Equals, N >::m_term_set

private

This is the set of term pointers to keep the terms unique.

Definition at line 204 of file aterm_pool_storage.h.

◆ todo

template<typename Element , typename Hash = aterm_hasher<>, typename Equals = aterm_equals<>, std::size_t N = DynamicNumberOfArguments>

std::stack<std::reference_wrapper<_aterm> > atermpp::detail::aterm_pool_storage< Element, Hash, Equals, N >::todo

private

A reusable todo stack.

Definition at line 211 of file aterm_pool_storage.h.

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

atermpp/include/mcrl2/atermpp/detail/aterm_pool_storage.h

Public Types

Public Member Functions

Private Types

Private Member Functions

Private Attributes

Friends

Detailed Description

Member Typedef Documentation

◆ callback_pair

◆ const_iterator

◆ iterator

◆ unordered_set

Constructor & Destructor Documentation

◆ aterm_pool_storage() [1/2]

◆ aterm_pool_storage() [2/2]

Member Function Documentation

◆ add_deletion_hook()

◆ call_deletion_hook()

◆ capacity()

◆ create_appl()

◆ create_appl_dynamic() [1/4]

◆ create_appl_dynamic() [2/4]

◆ create_appl_dynamic() [3/4]

◆ create_appl_dynamic() [4/4]

◆ create_appl_iterator() [1/2]

◆ create_appl_iterator() [2/2]

◆ create_int()

◆ create_term()

◆ destroy()

◆ emplace()

◆ is_dynamic_storage()

◆ print_performance_stats()

◆ resize_if_needed()

◆ size()

◆ sweep()

◆ verify_mark()

◆ verify_sweep()

◆ verify_term()

Friends And Related Symbol Documentation

◆ aterm_pool

Member Data Documentation

◆ m_deletion_hooks

◆ m_erasedBlocks

◆ m_pool

◆ m_term_metric

◆ m_term_set

◆ todo