Namespaces
namespace	anonymous_namespace{gc_stress_thread.cpp}

Classes
class	_aterm
	This is the class to which an aterm points. More...

class	_aterm_appl
	This class stores a term followed by N arguments. Where N should be equal to the arity of the function symbol. These arguments do have room reserved for them during the creation of the _aterm_appl. More...

class	_aterm_appl_allocator
	This class allocates _aterm_appl objects where the size is based on the arity of the function symbol. More...

class	_aterm_int
	The underlying integer term that actually carries the integer data. More...

class	_function_symbol
	Stores the data for a function symbol (name, arity) pair. More...

class	_term_list

class	aterm_allocator

class	aterm_container
	Provides safe storage of unprotected_aterm_core instances in a container by marking them during garbage collection. More...

struct	aterm_equals
	Returns true iff first and second are value-equivalent. More...

struct	aterm_equals_finite

struct	aterm_hasher
	Computes the hash of the given term. More...

struct	aterm_hasher_finite
	Computes the hash of the given term. More...

struct	aterm_int_equals
	Returns true iff the given term(s) or value are equivalent. More...

struct	aterm_int_hasher
	Computes the hash of the integral term arguments. More...

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

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

struct	bottom_up_replace_aterm_builder

struct	cached_bottom_up_replace_aterm_builder

struct	do_not_convert_term

struct	found_term_exception

struct	function_symbol_equals
	True iff the given function symbols are equal to eachother or to the given key. More...

struct	function_symbol_hasher
	Computes the hash for given function symbol objects and for the function_symbol_key. More...

class	function_symbol_pool
	This class stores a set of function symbols. More...

class	generic_aterm_container

struct	index_traits
	For several variable types in mCRL2 an implicit mapping of these variables to integers is available. This is done for efficiency reasons. Examples are: More...

struct	is_container_impl

struct	is_container_impl< std::list< T > >

struct	is_container_impl< std::multiset< T > >

struct	is_container_impl< std::set< T > >

struct	is_container_impl< std::vector< T > >

struct	is_markable_aterm
	Type trait to detect markable_aterm instantiations. More...

struct	is_markable_aterm< markable_aterm< T > >

struct	is_set_impl

struct	is_set_impl< std::multiset< T > >

struct	is_set_impl< std::set< T > >

struct	iterator_value

struct	iterator_value< std::back_insert_iterator< Container > >

struct	iterator_value< std::front_insert_iterator< Container > >

struct	iterator_value< std::insert_iterator< Container > >

struct	lazy_check_value_type

struct	lazy_check_value_type< true, Container, ValueType >

struct	markable_aterm
	Wrapper for user-defined types that provide their own mark() implementation. More...

struct	markable_aterm< std::pair< F, S > >
	Wrapper for std::pair — recursively marks both elements. More...

struct	markable_aterm< std::vector< T, Alloc > >
	Wrapper for std::vector — recursively marks all elements. More...

struct	markable_aterm< T >
	Wrapper for fundamental types (int, bool, etc.) — mark is a no-op. More...

struct	partial_replace_aterm_builder

struct	replace_aterm_builder

class	thread_aterm_pool
	This is a thread's specific access to the global aterm pool which ensures that garbage collection and hash table resizing can proceed. More...

class	thread_aterm_pool_interface
	A thread specific aterm pool that provides a local interface to the global term pool. Ensures that terms created by this thread are protected during garbage collection. More...

Concepts
concept	Markable
	Concept for types that support GC marking.

Typedefs
template<typename ... Terms>
using	are_terms = mcrl2::utilities::forall< std::is_convertible< Terms, unprotected_aterm_core >... >
	Can be used to check whether all elements in the parameter pack are derived from aterms.

template<typename Term >
using	is_term_or_function = std::disjunction< std::is_convertible< Term, unprotected_aterm_core >, std::disjunction< mcrl2::utilities::is_applicable< Term, unprotected_aterm_core & >, mcrl2::utilities::is_constant_function_yielding< Term, unprotected_aterm_core > > >

template<typename ... Terms>
using	are_terms_or_functions = mcrl2::utilities::forall< is_term_or_function< Terms >... >

using	integer_term_storage = aterm_pool_storage< _aterm_int, aterm_int_hasher, aterm_int_equals, 0 >
	Define several specializations of the term pool storage objects.

using	term_storage = aterm_pool_storage< _aterm, aterm_hasher_finite< 0 >, aterm_equals_finite< 0 >, 0 >

using	arbitrary_function_application_storage = aterm_pool_storage< _aterm_appl< 1 >, aterm_hasher< DynamicNumberOfArguments >, aterm_equals< DynamicNumberOfArguments >, DynamicNumberOfArguments >

template<std::size_t N>
using	function_application_storage = aterm_pool_storage< _aterm_appl< N >, aterm_hasher_finite< N >, aterm_equals_finite< N >, N >

template<typename T >
using	markable_t = std::conditional_t< is_markable_aterm< std::decay_t< T > >::value, T, markable_aterm< T > >
	Returns T if T is already a `markable_aterm<U>`, otherwise `markable_aterm<T>`.

template<typename T >
using	reference_aterm = markable_aterm< T >
	Backward-compatible alias for markable_aterm.

using	_term_appl = _aterm_appl<>
	A default instantiation for the underlying term application.

Functions
thread_aterm_pool &	g_thread_term_pool ()
	A reference to the thread local term pool storage.

mcrl2::utilities::shared_guard	lock_shared_aterm_pool ()
	Acquires a shared lock on the global thread aterm pool.

aterm_pool &	g_aterm_pool_instance ()
	A reference to the global term pool storage.

template<bool lazy = false>
aterm_pool &	g_term_pool ()
	obtain a reference to the global aterm pool.

void	start_gc_stress_thread ()
	Spawns a dedicated background thread that continuously triggers garbage collection.

void	stop_gc_stress_thread ()
	Stop the background GC stress thread if it is running.

template<template< class > class Builder, class ReplaceFunction >
replace_aterm_builder< Builder, ReplaceFunction >	make_replace_aterm_builder (ReplaceFunction f)

template<template< class > class Builder, class ReplaceFunction >
partial_replace_aterm_builder< Builder, ReplaceFunction >	make_partial_replace_aterm_builder (ReplaceFunction f)

template<template< class > class Builder, class ReplaceFunction >
bottom_up_replace_aterm_builder< Builder, ReplaceFunction >	make_bottom_up_replace_aterm_builder (ReplaceFunction f)

template<template< class > class Builder, class ReplaceFunction >
cached_bottom_up_replace_aterm_builder< Builder, ReplaceFunction >	make_cached_bottom_up_replace_aterm_builder (ReplaceFunction f, std::unordered_map< aterm, aterm > &cache)

template<typename Function >
aterm	appl_apply (const aterm &a, const Function f)
	Applies the function f to all children of a.

template<typename UnaryFunction >
UnaryFunction	for_each_impl (aterm t, UnaryFunction op)
	Implements the for_each algorithm.

template<typename MatchPredicate >
bool	find_if_impl (const aterm &t, MatchPredicate match, aterm &output)
	Implements the find_if algorithm If the term t is found, it is stored in output and true is returned.

template<typename MatchPredicate , typename OutputIterator >
void	find_all_if_impl (const aterm &t, MatchPredicate op, OutputIterator &destBegin)
	Implements the find_all_if algorithm.

template<typename MatchPredicate , typename StopPredicate >
aterm	partial_find_if_impl (const aterm &t, MatchPredicate match, StopPredicate stop)
	Implements the partial_find_if_impl algorithm.

template<typename MatchPredicate , typename StopPredicate , typename OutputIterator >
void	partial_find_all_if_impl (const aterm &t, MatchPredicate match, StopPredicate stop, OutputIterator &destBegin)
	Implements the partial_find_all_if algorithm.

_aterm *	address (const unprotected_aterm_core &t)

template<IsATerm Derived, IsATerm Base> requires std::is_base_of_v<aterm, Base> && std::is_base_of_v<aterm, Derived>
term_appl_iterator< Derived >	aterm_appl_iterator_cast (term_appl_iterator< Base > a)
	This function can be used to translate an term_appl_iterator of one sort into another.

void	debug_print (std::ostream &o, const _aterm *t, std::size_t d=3)

template<typename Term , typename Iter , typename ATermConverter >
term_list< Term >	make_list_backward (Iter first, Iter last, ATermConverter convert_to_aterm)
	Constructs a list starting from first to last. The iterators are traversed backwards and each element is converted using the TermConverter.

template<class Term , class Iter , class ATermConverter >
void	make_list_backward (term_list< Term > &result, Iter first, Iter last, ATermConverter convert_to_aterm)
	Constructs a list starting from first to last where the result is put in result.

template<typename Term , typename Iter , typename ATermConverter , typename ATermFilter >
term_list< Term >	make_list_backward (Iter first, Iter last, ATermConverter convert_to_aterm, ATermFilter aterm_filter)
	Constructs a list starting from first to last. The iterators are traversed backwards and each element is converted using the TermConverter and inserted whenever TermFilter yields true for the converted element.

template<class Term , class Iter , class ATermConverter , class ATermFilter >
void	make_list_backward (term_list< Term > &result, Iter first, Iter last, ATermConverter convert_to_aterm, ATermFilter aterm_filter)
	Construct a list iterating from the last to the first element. Result is put in the variable result.

template<typename Term , class Iter , class ATermConverter >
term_list< Term >	make_list_forward (Iter first, Iter last, ATermConverter convert_to_aterm)
	Constructs a list starting from first to last. Each element is converted using the TermConverter.

template<typename Term , class Iter , class ATermConverter >
void	make_list_forward (term_list< Term > &result, Iter first, Iter last, ATermConverter convert_to_aterm)
	Constructs a list starting from first to last. Each element is converted using the TermConverter.

template<typename Term , class Iter , class ATermConverter , class ATermFilter >
term_list< Term >	make_list_forward (Iter first, Iter last, ATermConverter convert_to_aterm, ATermFilter aterm_filter)
	Constructs a list starting from first to last. Each element is converted using the TermConverter and inserted whenever TermFilter yields true for the converted element.

template<class Term , class Iter , class ATermConverter , class ATermFilter >
void	make_list_forward (term_list< Term > &result, Iter first, Iter last, ATermConverter convert_to_aterm, ATermFilter aterm_filter)
	Constructs a list traversing the iterator from first to last, putting the result in place in the variable result.

template<class Term , typename ForwardTraversalIterator , class Transformer >
void	make_list_forward_helper (term_list< Term > &result, ForwardTraversalIterator &p, const ForwardTraversalIterator last, Transformer transformer)

std::size_t	combine (const std::size_t hnr, const unprotected_aterm_core &term)
	Auxiliary function to combine hnr with aterms.

template<std::size_t I = 0, typename... Tp> requires (I < sizeof...(Tp))
std::size_t	combine_args (std::size_t seed, const Tp &... t)

static std::size_t	xorshift (const std::size_t n, const std::size_t i)

template<std::size_t I = 0, typename... Tp> requires (I < sizeof...(Tp))
bool	equal_args (const _aterm_appl< 8 > &term, const Tp &... t)

void	mark_term (const _aterm &root, std::stack< std::reference_wrapper< _aterm > > &todo)
	Marks a term and recursively all arguments that are not reachable.

template<std::size_t N, typename InputIterator , typename TermConverter > requires (mcrl2::utilities::is_iterator<InputIterator>::value && std::is_convertible_v<std::invoke_result_t<TermConverter, typename InputIterator::value_type>, aterm>)
std::array< unprotected_aterm_core, N >	construct_arguments (InputIterator it, InputIterator end, TermConverter converter)
	Construct the proxy where its arguments are given by applying the converter to each element in the iterator.

template<std::size_t N, typename InputIterator , typename TermConverter > requires (mcrl2::utilities::is_iterator<InputIterator>::value && std::is_same_v< std::invoke_result_t<TermConverter, typename InputIterator::value_type&, typename InputIterator::value_type>, void>)
std::array< unprotected_aterm_core, N >	construct_arguments (InputIterator it, InputIterator end, TermConverter converter)
	Construct the proxy where its arguments are given by applying the converter to each element in the iterator.

template<std::size_t N, std::size_t I>
void	store_in_argument_array_ (std::array< unprotected_aterm_core, N > &)

template<std::size_t N, std::size_t I, class FUNCTION_OR_TERM_TYPE , typename... Args>
void	store_in_argument_array_ (std::array< unprotected_aterm_core, N > &argument_array, const FUNCTION_OR_TERM_TYPE &function_or_term, const Args &... args)

template<std::size_t N, typename... Args>
void	store_in_argument_array (std::array< unprotected_aterm_core, N > &argument_array, const Args &... args)

template<typename Variable , typename KeyType >
atermpp::unordered_map< KeyType, std::size_t > &	variable_index_map ()

template<typename Variable , typename KeyType >
std::stack< std::size_t > &	variable_map_free_numbers ()

template<typename Variable , typename KeyType >
mcrl2::utilities::mutex &	variable_mutex ()

template<typename Variable , typename KeyType >
std::size_t &	variable_map_max_index ()

Variables
thread_aterm_pool *	g_main_thread_pool = nullptr
	Pointer to the main thread's pool; set on its first access and used by ~thread_aterm_pool to transfer orphaned protection-set entries when a worker thread exits.

std::array< std::byte, sizeof(aterm_pool)>	g_aterm_pool_storage = {}
	Storage for a global term pool that is not initialized.

static constexpr bool	EnableGarbageCollection = true
	Enable garbage collection.

static constexpr bool	EnableBlockAllocator = true
	Enable the block allocator for terms.

static constexpr bool	EnableGarbageCollectionMetrics = false
	Enable to print garbage collection statistics.

static constexpr bool	EnableAggressiveGarbageCollection = false
	Performs garbage collection intensively for testing purposes.

static constexpr bool	EnableGCStressThread = false
	Spawns a dedicated background thread that continuously triggers garbage collection.

static constexpr bool	EnableHashtableMetrics = false
	Enable to print hashtable collision, size and number of buckets.

static constexpr bool	EnableCreationMetrics = false
	Enable to obtain the percentage of terms found compared to allocated.

static constexpr bool	EnableVariableRegistrationMetrics = false
	Keep track of the number of variables registered.

constexpr std::size_t	DynamicNumberOfArguments = std::numeric_limits<std::size_t>::max()
	Indicates that the number of arguments is not known at compile time.

function_symbol	g_as_int
	These function symbols are used to indicate integer, list and empty list terms.

function_symbol	g_as_list

function_symbol	g_as_empty_list

Typedef Documentation

◆ _term_appl

using atermpp::detail::_term_appl = typedef _aterm_appl<>

A default instantiation for the underlying term application.

Definition at line 106 of file aterm.h.

◆ arbitrary_function_application_storage

using atermpp::detail::arbitrary_function_application_storage = typedef aterm_pool_storage<_aterm_appl<1>, aterm_hasher<DynamicNumberOfArguments>, aterm_equals<DynamicNumberOfArguments>, DynamicNumberOfArguments>

Definition at line 27 of file aterm_pool.h.

◆ are_terms

template<typename ... Terms>

using atermpp::detail::are_terms = typedef mcrl2::utilities::forall<std::is_convertible<Terms, unprotected_aterm_core>...>

Can be used to check whether all elements in the parameter pack are derived from aterms.

Definition at line 33 of file aterm_core.h.

◆ are_terms_or_functions

template<typename ... Terms>

using atermpp::detail::are_terms_or_functions = typedef mcrl2::utilities::forall<is_term_or_function<Terms>...>

Definition at line 44 of file aterm_core.h.

◆ function_application_storage

template<std::size_t N>

using atermpp::detail::function_application_storage = typedef aterm_pool_storage<_aterm_appl<N>, aterm_hasher_finite<N>, aterm_equals_finite<N>, N>

Definition at line 33 of file aterm_pool.h.

◆ integer_term_storage

using atermpp::detail::integer_term_storage = typedef aterm_pool_storage<_aterm_int, aterm_int_hasher, aterm_int_equals, 0>

Define several specializations of the term pool storage objects.

Definition at line 25 of file aterm_pool.h.

◆ is_term_or_function

template<typename Term >

using atermpp::detail::is_term_or_function = typedef std::disjunction<std::is_convertible<Term, unprotected_aterm_core>, std::disjunction<mcrl2::utilities::is_applicable<Term, unprotected_aterm_core&>, mcrl2::utilities::is_constant_function_yielding<Term, unprotected_aterm_core> > >

Check whether all arguments of a parameter pack are terms, constant functions yielding a term or a function putting a term in a result parameter.

Definition at line 39 of file aterm_core.h.

◆ markable_t

template<typename T >

using atermpp::detail::markable_t = typedef std::conditional_t<is_markable_aterm<std::decay_t<T> >::value, T, markable_aterm<T> >

Returns T if T is already a markable_aterm<U>, otherwise markable_aterm<T>.

Prevents double-wrapping when T is already a markable_aterm.

Definition at line 103 of file aterm_container.h.

◆ reference_aterm

template<typename T >

using atermpp::detail::reference_aterm = typedef markable_aterm<T>

Backward-compatible alias for markable_aterm.

Definition at line 407 of file aterm_container.h.

◆ term_storage

using atermpp::detail::term_storage = typedef aterm_pool_storage<_aterm, aterm_hasher_finite<0>, aterm_equals_finite<0>, 0>

Definition at line 26 of file aterm_pool.h.

Function Documentation

◆ address()

_aterm * atermpp::detail::address ( const unprotected_aterm_core & t )

inline

Returns: A pointer to the underlying aterm_core.

Definition at line 208 of file aterm_core.h.

◆ appl_apply()

template<typename Function >

aterm atermpp::detail::appl_apply	(	const aterm &	a,
		const Function	f
	)

Applies the function f to all children of a.

Parameters

a	A term
f	A function on terms

Returns: The transformed term

Definition at line 24 of file algorithm_impl.h.

◆ aterm_appl_iterator_cast()

template<IsATerm Derived, IsATerm Base>
requires std::is_base_of_v<aterm, Base> && std::is_base_of_v<aterm, Derived>

term_appl_iterator< Derived > atermpp::detail::aterm_appl_iterator_cast ( term_appl_iterator< Base > a )

This function can be used to translate an term_appl_iterator of one sort into another.

Definition at line 177 of file aterm_appl_iterator.h.

◆ combine()

std::size_t atermpp::detail::combine	(	const std::size_t	hnr,
		const unprotected_aterm_core &	term
	)

inline

Auxiliary function to combine hnr with aterms.

Definition at line 160 of file aterm_hash.h.

◆ combine_args()

template<std::size_t I = 0, typename... Tp>
requires (I < sizeof...(Tp))

std::size_t atermpp::detail::combine_args	(	std::size_t	seed,
		const Tp &...	t
	)

Definition at line 254 of file aterm_hash.h.

◆ construct_arguments() [1/2]

template<std::size_t N, typename InputIterator , typename TermConverter >
requires (mcrl2::utilities::is_iterator<InputIterator>::value && std::is_convertible_v<std::invoke_result_t<TermConverter, typename InputIterator::value_type>, aterm>)

std::array< unprotected_aterm_core, N > atermpp::detail::construct_arguments	(	InputIterator	it,
		InputIterator	end,
		TermConverter	converter
	)

inline

Construct the proxy where its arguments are given by applying the converter to each element in the iterator.

Definition at line 29 of file aterm_pool_storage_implementation.h.

◆ construct_arguments() [2/2]

template<std::size_t N, typename InputIterator , typename TermConverter >
requires (mcrl2::utilities::is_iterator<InputIterator>::value && std::is_same_v< std::invoke_result_t<TermConverter, typename InputIterator::value_type&, typename InputIterator::value_type>, void>)

std::array< unprotected_aterm_core, N > atermpp::detail::construct_arguments	(	InputIterator	it,
		InputIterator	end,
		TermConverter	converter
	)

inline

Construct the proxy where its arguments are given by applying the converter to each element in the iterator.

Definition at line 53 of file aterm_pool_storage_implementation.h.

◆ debug_print()

void atermpp::detail::debug_print	(	std::ostream &	o,
		const _aterm *	t,
		std::size_t	d = `3`
	)

inline

◆ equal_args()

template<std::size_t I = 0, typename... Tp>
requires (I < sizeof...(Tp))

bool atermpp::detail::equal_args	(	const _aterm_appl< 8 > &	term,
		const Tp &...	t
	)

Definition at line 383 of file aterm_hash.h.

◆ find_all_if_impl()

template<typename MatchPredicate , typename OutputIterator >

void atermpp::detail::find_all_if_impl	(	const aterm &	t,
		MatchPredicate	op,
		OutputIterator &	destBegin
	)

Implements the find_all_if algorithm.

Parameters

t	A term
op	A predicate function on terms
destBegin	The beginning of a range to where the results are written

Definition at line 138 of file algorithm_impl.h.

◆ find_if_impl()

template<typename MatchPredicate >

bool atermpp::detail::find_if_impl	(	const aterm &	t,
		MatchPredicate	match,
		aterm &	output
	)

Implements the find_if algorithm If the term t is found, it is stored in output and true is returned.

Parameters

t	A term
match	A predicate function on terms
output	The variable to store the match in

Returns: true if a match was found, false otherwise

Definition at line 102 of file algorithm_impl.h.

◆ for_each_impl()

template<typename UnaryFunction >

UnaryFunction atermpp::detail::for_each_impl	(	aterm	t,
		UnaryFunction	op
	)

Implements the for_each algorithm.

Parameters

t	A term
op	A unary function on terms

Returns: The result of the algorithm

Definition at line 72 of file algorithm_impl.h.

◆ g_aterm_pool_instance()

aterm_pool & atermpp::detail::g_aterm_pool_instance ( )

inline

A reference to the global term pool storage.

Implemented as a function to avoid a static initialisation order dependency on g_aterm_pool_storage. The returned reference merely reinterprets the address of the storage array, which is a link-time constant.

Definition at line 32 of file global_aterm_pool.h.

◆ g_term_pool()

template<bool lazy = false>

aterm_pool & atermpp::detail::g_term_pool ( )

inline

obtain a reference to the global aterm pool.

provides lazy initialization which should be used when instantiating global terms and function symbols.

Definition at line 41 of file global_aterm_pool.h.

◆ g_thread_term_pool()

thread_aterm_pool & atermpp::detail::g_thread_term_pool ( )

A reference to the thread local term pool storage.

Definition at line 40 of file aterm_implementation.cpp.

◆ lock_shared_aterm_pool()

mcrl2::utilities::shared_guard atermpp::detail::lock_shared_aterm_pool ( )

Acquires a shared lock on the global thread aterm pool.

This free function is declared here but defined in aterm_implementation.cpp, where thread_aterm_pool is a complete type. It allows reference_aterm::operator= below to be defined inline, which is required to work around an MSVC limitation regarding out-of-line definitions of members of constrained partial specializations, without this header needing the complete definition of thread_aterm_pool, which Clang requires when the body is inline.

Definition at line 58 of file aterm_implementation.cpp.

◆ make_bottom_up_replace_aterm_builder()

template<template< class > class Builder, class ReplaceFunction >

bottom_up_replace_aterm_builder< Builder, ReplaceFunction > atermpp::detail::make_bottom_up_replace_aterm_builder ( ReplaceFunction f )

Definition at line 126 of file algorithm.h.

◆ make_cached_bottom_up_replace_aterm_builder()

template<template< class > class Builder, class ReplaceFunction >

cached_bottom_up_replace_aterm_builder< Builder, ReplaceFunction > atermpp::detail::make_cached_bottom_up_replace_aterm_builder	(	ReplaceFunction	f,
		std::unordered_map< aterm, aterm > &	cache
	)

Definition at line 165 of file algorithm.h.

◆ make_list_backward() [1/4]

template<typename Term , typename Iter , typename ATermConverter >

term_list< Term > atermpp::detail::make_list_backward	(	Iter	first,
		Iter	last,
		ATermConverter	convert_to_aterm
	)

inline

Constructs a list starting from first to last. The iterators are traversed backwards and each element is converted using the TermConverter.

The functions make_list_backward and make_list_forward with three and four arguments are almost the same. The reason for this is that there is a 5% loss of speed of the toolset when merging these two functions. This is caused by storing and protecting the intermediate value of the converted aterm. See Term t = convert_to_aterm(...).

Definition at line 514 of file aterm_list_implementation.h.

◆ make_list_backward() [2/4]

template<typename Term , typename Iter , typename ATermConverter , typename ATermFilter >

term_list< Term > atermpp::detail::make_list_backward	(	Iter	first,
		Iter	last,
		ATermConverter	convert_to_aterm,
		ATermFilter	aterm_filter
	)

inline

Constructs a list starting from first to last. The iterators are traversed backwards and each element is converted using the TermConverter and inserted whenever TermFilter yields true for the converted element.

Definition at line 493 of file aterm_list_implementation.h.

◆ make_list_backward() [3/4]

template<class Term , class Iter , class ATermConverter >

void atermpp::detail::make_list_backward	(	term_list< Term > &	result,
		Iter	first,
		Iter	last,
		ATermConverter	convert_to_aterm
	)

inline

Constructs a list starting from first to last where the result is put in result.

Constructs a list starting from the first iterator element to the last. The result is put into the variable result.

Definition at line 501 of file aterm_list_implementation.h.

◆ make_list_backward() [4/4]

template<class Term , class Iter , class ATermConverter , class ATermFilter >

void atermpp::detail::make_list_backward	(	term_list< Term > &	result,
		Iter	first,
		Iter	last,
		ATermConverter	convert_to_aterm,
		ATermFilter	aterm_filter
	)

inline

Construct a list iterating from the last to the first element. Result is put in the variable result.

Definition at line 475 of file aterm_list_implementation.h.

◆ make_list_forward() [1/4]

template<typename Term , class Iter , class ATermConverter >

term_list< Term > atermpp::detail::make_list_forward	(	Iter	first,
		Iter	last,
		ATermConverter	convert_to_aterm
	)

inline

Constructs a list starting from first to last. Each element is converted using the TermConverter.

Definition at line 660 of file aterm_list_implementation.h.

◆ make_list_forward() [2/4]

template<typename Term , class Iter , class ATermConverter , class ATermFilter >

term_list< Term > atermpp::detail::make_list_forward	(	Iter	first,
		Iter	last,
		ATermConverter	convert_to_aterm,
		ATermFilter	aterm_filter
	)

inline

Constructs a list starting from first to last. Each element is converted using the TermConverter and inserted whenever TermFilter yields true for the converted element.

Will first store the converted elements in an array and then insert them into the list.

Definition at line 579 of file aterm_list_implementation.h.

◆ make_list_forward() [3/4]

template<typename Term , class Iter , class ATermConverter >

void atermpp::detail::make_list_forward	(	term_list< Term > &	result,
		Iter	first,
		Iter	last,
		ATermConverter	convert_to_aterm
	)

inline

Constructs a list starting from first to last. Each element is converted using the TermConverter.

Definition at line 617 of file aterm_list_implementation.h.

◆ make_list_forward() [4/4]

template<class Term , class Iter , class ATermConverter , class ATermFilter >

void atermpp::detail::make_list_forward	(	term_list< Term > &	result,
		Iter	first,
		Iter	last,
		ATermConverter	convert_to_aterm,
		ATermFilter	aterm_filter
	)

inline

Constructs a list traversing the iterator from first to last, putting the result in place in the variable result.

Definition at line 524 of file aterm_list_implementation.h.

◆ make_list_forward_helper()

template<class Term , typename ForwardTraversalIterator , class Transformer >

void atermpp::detail::make_list_forward_helper	(	term_list< Term > &	result,
		ForwardTraversalIterator &	p,
		const ForwardTraversalIterator	last,
		Transformer	transformer
	)

Definition at line 587 of file aterm_list_implementation.h.

◆ make_partial_replace_aterm_builder()

template<template< class > class Builder, class ReplaceFunction >

partial_replace_aterm_builder< Builder, ReplaceFunction > atermpp::detail::make_partial_replace_aterm_builder ( ReplaceFunction f )

Definition at line 95 of file algorithm.h.

◆ make_replace_aterm_builder()

template<template< class > class Builder, class ReplaceFunction >

replace_aterm_builder< Builder, ReplaceFunction > atermpp::detail::make_replace_aterm_builder ( ReplaceFunction f )

Definition at line 58 of file algorithm.h.

◆ mark_term()

void atermpp::detail::mark_term	(	const _aterm &	root,
		std::stack< std::reference_wrapper< _aterm > > &	todo
	)

inline

Marks a term and recursively all arguments that are not reachable.

Definition at line 73 of file aterm_pool_storage_implementation.h.

◆ partial_find_all_if_impl()

template<typename MatchPredicate , typename StopPredicate , typename OutputIterator >

void atermpp::detail::partial_find_all_if_impl	(	const aterm &	t,
		MatchPredicate	match,
		StopPredicate	stop,
		OutputIterator &	destBegin
	)

Implements the partial_find_all_if algorithm.

Parameters

t	A term
match	A predicate function on terms
stop	A predicate function on terms
destBegin	The beginning of a range to where the results are written

Definition at line 217 of file algorithm_impl.h.

◆ partial_find_if_impl()

template<typename MatchPredicate , typename StopPredicate >

aterm atermpp::detail::partial_find_if_impl	(	const aterm &	t,
		MatchPredicate	match,
		StopPredicate	stop
	)

Implements the partial_find_if_impl algorithm.

Parameters

t	A term
match	A predicate function on terms
stop	A predicate function on terms

Definition at line 174 of file algorithm_impl.h.

◆ start_gc_stress_thread()

void atermpp::detail::start_gc_stress_thread ( )

Spawns a dedicated background thread that continuously triggers garbage collection.

Only has effect when EnableGCStressThread is set and MCRL2_ENABLE_MULTITHREADING is defined. Useful for stress-testing the thread safety of the term pool under concurrent GC pressure. The thread is stopped automatically at program exit.

Definition at line 31 of file gc_stress_thread.cpp.

◆ stop_gc_stress_thread()

void atermpp::detail::stop_gc_stress_thread ( )

Stop the background GC stress thread if it is running.

Definition at line 49 of file gc_stress_thread.cpp.

◆ store_in_argument_array()

template<std::size_t N, typename... Args>

void atermpp::detail::store_in_argument_array	(	std::array< unprotected_aterm_core, N > &	argument_array,
		const Args &...	args
	)

Definition at line 176 of file aterm_pool_storage_implementation.h.

◆ store_in_argument_array_() [1/2]

template<std::size_t N, std::size_t I>

void atermpp::detail::store_in_argument_array_ ( std::array< unprotected_aterm_core, N > & )

Definition at line 146 of file aterm_pool_storage_implementation.h.

◆ store_in_argument_array_() [2/2]

template<std::size_t N, std::size_t I, class FUNCTION_OR_TERM_TYPE , typename... Args>

void atermpp::detail::store_in_argument_array_	(	std::array< unprotected_aterm_core, N > &	argument_array,
		const FUNCTION_OR_TERM_TYPE &	function_or_term,
		const Args &...	args
	)

Definition at line 152 of file aterm_pool_storage_implementation.h.

◆ variable_index_map()

template<typename Variable , typename KeyType >

atermpp::unordered_map< KeyType, std::size_t > & atermpp::detail::variable_index_map ( )

Definition at line 26 of file index_traits.h.

◆ variable_map_free_numbers()

template<typename Variable , typename KeyType >

std::stack< std::size_t > & atermpp::detail::variable_map_free_numbers ( )

Definition at line 33 of file index_traits.h.

◆ variable_map_max_index()

template<typename Variable , typename KeyType >

std::size_t & atermpp::detail::variable_map_max_index ( )

Definition at line 48 of file index_traits.h.

◆ variable_mutex()

template<typename Variable , typename KeyType >

mcrl2::utilities::mutex & atermpp::detail::variable_mutex ( )

Definition at line 40 of file index_traits.h.

◆ xorshift()

static std::size_t atermpp::detail::xorshift	(	const std::size_t	n,
		const std::size_t	i
	)

inlinestatic

Definition at line 277 of file aterm_hash.h.

Variable Documentation

◆ DynamicNumberOfArguments

constexpr std::size_t atermpp::detail::DynamicNumberOfArguments = std::numeric_limits<std::size_t>::max()

constexpr

Indicates that the number of arguments is not known at compile time.

Definition at line 77 of file aterm_hash.h.

◆ EnableAggressiveGarbageCollection

constexpr bool atermpp::detail::EnableAggressiveGarbageCollection = false

staticconstexpr

Performs garbage collection intensively for testing purposes.

Definition at line 28 of file aterm_configuration.h.

◆ EnableBlockAllocator

constexpr bool atermpp::detail::EnableBlockAllocator = true

staticconstexpr

Enable the block allocator for terms.

Definition at line 22 of file aterm_configuration.h.

◆ EnableCreationMetrics

constexpr bool atermpp::detail::EnableCreationMetrics = false

staticconstexpr

Enable to obtain the percentage of terms found compared to allocated.

Definition at line 39 of file aterm_configuration.h.

◆ EnableGarbageCollection

constexpr bool atermpp::detail::EnableGarbageCollection = true

staticconstexpr

Enable garbage collection.

Definition at line 19 of file aterm_configuration.h.

◆ EnableGarbageCollectionMetrics

constexpr bool atermpp::detail::EnableGarbageCollectionMetrics = false

staticconstexpr

Enable to print garbage collection statistics.

Definition at line 25 of file aterm_configuration.h.

◆ EnableGCStressThread

constexpr bool atermpp::detail::EnableGCStressThread = false

staticconstexpr

Spawns a dedicated background thread that continuously triggers garbage collection.

Only has effect when MCRL2_ENABLE_MULTITHREADING is defined. Useful for stress-testing the thread safety of the term pool under concurrent GC pressure.

Definition at line 33 of file aterm_configuration.h.

◆ EnableHashtableMetrics

constexpr bool atermpp::detail::EnableHashtableMetrics = false

staticconstexpr

Enable to print hashtable collision, size and number of buckets.

Definition at line 36 of file aterm_configuration.h.

◆ EnableVariableRegistrationMetrics

constexpr bool atermpp::detail::EnableVariableRegistrationMetrics = false

staticconstexpr

Keep track of the number of variables registered.

Definition at line 42 of file aterm_configuration.h.

◆ g_as_empty_list

function_symbol atermpp::detail::g_as_empty_list

extern

◆ g_as_int

function_symbol atermpp::detail::g_as_int

extern

These function symbols are used to indicate integer, list and empty list terms.

They are copied from the function_symbol_pool so that type_is_{int|list|appl} can be defined in the header.

◆ g_as_list

function_symbol atermpp::detail::g_as_list

extern

◆ g_aterm_pool_storage

std::array< std::byte, sizeof(aterm_pool)> atermpp::detail::g_aterm_pool_storage = {}

extern

Storage for a global term pool that is not initialized.

Definition of the extern global term pool.

Definition at line 73 of file aterm_implementation.cpp.

◆ g_main_thread_pool

thread_aterm_pool * atermpp::detail::g_main_thread_pool = nullptr

Pointer to the main thread's pool; set on its first access and used by ~thread_aterm_pool to transfer orphaned protection-set entries when a worker thread exits.

Definition at line 37 of file aterm_implementation.cpp.

Namespaces

Classes

Concepts

Typedefs

Functions

Variables

Typedef Documentation

◆ _term_appl

◆ arbitrary_function_application_storage

◆ are_terms

◆ are_terms_or_functions

◆ function_application_storage

◆ integer_term_storage

◆ is_term_or_function

◆ markable_t

◆ reference_aterm

◆ term_storage

Function Documentation

◆ address()

◆ appl_apply()

◆ aterm_appl_iterator_cast()

◆ combine()

◆ combine_args()

◆ construct_arguments() [1/2]

◆ construct_arguments() [2/2]

◆ debug_print()

◆ equal_args()

◆ find_all_if_impl()

◆ find_if_impl()

◆ for_each_impl()

◆ g_aterm_pool_instance()

◆ g_term_pool()

◆ g_thread_term_pool()

◆ lock_shared_aterm_pool()

◆ make_bottom_up_replace_aterm_builder()

◆ make_cached_bottom_up_replace_aterm_builder()

◆ make_list_backward() [1/4]

◆ make_list_backward() [2/4]

◆ make_list_backward() [3/4]

◆ make_list_backward() [4/4]

◆ make_list_forward() [1/4]

◆ make_list_forward() [2/4]

◆ make_list_forward() [3/4]

◆ make_list_forward() [4/4]

◆ make_list_forward_helper()

◆ make_partial_replace_aterm_builder()

◆ make_replace_aterm_builder()

◆ mark_term()

◆ partial_find_all_if_impl()

◆ partial_find_if_impl()

◆ start_gc_stress_thread()

◆ stop_gc_stress_thread()

◆ store_in_argument_array()

◆ store_in_argument_array_() [1/2]

◆ store_in_argument_array_() [2/2]

◆ variable_index_map()

◆ variable_map_free_numbers()

◆ variable_map_max_index()

◆ variable_mutex()

◆ xorshift()

Variable Documentation

◆ DynamicNumberOfArguments

◆ EnableAggressiveGarbageCollection

◆ EnableBlockAllocator

◆ EnableCreationMetrics

◆ EnableGarbageCollection

◆ EnableGarbageCollectionMetrics

◆ EnableGCStressThread

◆ EnableHashtableMetrics

◆ EnableVariableRegistrationMetrics

◆ g_as_empty_list

◆ g_as_int

◆ g_as_list

◆ g_aterm_pool_storage

◆ g_main_thread_pool