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

#include <function_symbol_pool.h>

Inheritance diagram for atermpp::detail::function_symbol_pool:

Public Member Functions
	function_symbol_pool ()

function_symbol	create (const std::string &name, const std::size_t arity, const bool check_for_registered_functions=false)
	Creates a function symbol pair (name, arity), returns a pointer to an existing element if this pair is already defined.

function_symbol	create (std::string &&name, const std::size_t arity, const bool check_for_registered_functions=false)

void	deregister (const std::string &prefix)
	Restore the index back to index before registering this prefix. \threadsafe.

std::shared_ptr< std::size_t >	register_prefix (const std::string &prefix)

void	resize_if_needed ()
	Resize the function symbol pool if necessary.

std::size_t	get_sufficiently_large_postfix_index (const std::string &prefix) const
	Get an index such that no function symbol with name prefix + returned value and any value above it already exists.

void	sweep ()
	Collect all garbage function symbols.

const function_symbol &	as_int () noexcept

const function_symbol &	as_list () noexcept

const function_symbol &	as_empty_list () noexcept

std::size_t	size () const noexcept

std::size_t	capacity () const noexcept

Private Types
using	unordered_set = mcrl2::utilities::unordered_set< _function_symbol, function_symbol_hasher, function_symbol_equals, typename std::conditional_t< EnableBlockAllocator, mcrl2::utilities::block_allocator< _function_symbol, 1024, mcrl2::utilities::detail::GlobalThreadSafe >, std::allocator< _function_symbol > >, mcrl2::utilities::detail::GlobalThreadSafe, false >

Private Member Functions
void	create_helper (const std::string &name)

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

	noncopyable (const noncopyable &)=delete

noncopyable &	operator= (const noncopyable &)=delete

Private Attributes
unordered_set	m_symbol_set
	Stores the underlying function symbols.

std::map< std::string, std::shared_ptr< std::size_t > >	m_prefix_to_register_function_map
	A map that records a function for each prefix that must be called to set the postfix number to a sufficiently high number if a function symbol with the same prefix string is registered.

mcrl2::utilities::mutex	m_mutex

function_symbol	m_as_int

function_symbol	m_as_list

function_symbol	m_as_empty_list

mcrl2::utilities::cache_metric	m_function_symbol_metrics
	Track the number of function symbols found in or added to the set.

Detailed Description

This class stores a set of function symbols.

Definition at line 24 of file function_symbol_pool.h.

Member Typedef Documentation

◆ unordered_set

using atermpp::detail::function_symbol_pool::unordered_set = mcrl2::utilities::unordered_set< _function_symbol, function_symbol_hasher, function_symbol_equals, typename std::conditional_t<EnableBlockAllocator, mcrl2::utilities::block_allocator<_function_symbol, 1024, mcrl2::utilities::detail::GlobalThreadSafe>, std::allocator<_function_symbol> >, mcrl2::utilities::detail::GlobalThreadSafe, false>

private

Definition at line 74 of file function_symbol_pool.h.

Constructor & Destructor Documentation

◆ function_symbol_pool()

function_symbol_pool::function_symbol_pool ( )

Definition at line 19 of file function_symbol_pool.cpp.

Member Function Documentation

◆ as_empty_list()

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

inlinenoexcept

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

Definition at line 65 of file function_symbol_pool.h.

◆ as_int()

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

inlinenoexcept

Returns: The function symbol used by integral terms.

Definition at line 59 of file function_symbol_pool.h.

◆ as_list()

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

inlinenoexcept

Returns: The function symbol used by the list constructor.

Definition at line 62 of file function_symbol_pool.h.

◆ capacity()

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

inlinenoexcept

Returns: The maximum number of function symbols stored in this pool.

Definition at line 71 of file function_symbol_pool.h.

◆ create() [1/2]

function_symbol function_symbol_pool::create	(	const std::string &	name,
		const std::size_t	arity,
		const bool	check_for_registered_functions = `false`
	)

Creates a function symbol pair (name, arity), returns a pointer to an existing element if this pair is already defined.

Parameters

check_for_registered_functions Check whether there is a registered prefix p such that name equal pn where n is a number. In that case prevent that pn will be generated as a fresh function name. \threadsafe

Definition at line 87 of file function_symbol_pool.cpp.

◆ create() [2/2]

function_symbol function_symbol_pool::create	(	std::string &&	name,
		const std::size_t	arity,
		const bool	check_for_registered_functions = `false`
	)

Definition at line 63 of file function_symbol_pool.cpp.

◆ create_helper()

void function_symbol_pool::create_helper ( const std::string & name )

private

Definition at line 32 of file function_symbol_pool.cpp.

◆ deregister()

void function_symbol_pool::deregister ( const std::string & prefix )

Restore the index back to index before registering this prefix. \threadsafe.

Definition at line 111 of file function_symbol_pool.cpp.

◆ get_sufficiently_large_postfix_index()

std::size_t function_symbol_pool::get_sufficiently_large_postfix_index ( const std::string & prefix ) const

Get an index such that no function symbol with name prefix + returned value and any value above it already exists.

Definition at line 140 of file function_symbol_pool.cpp.

◆ register_prefix()

std::shared_ptr< std::size_t > function_symbol_pool::register_prefix ( const std::string & prefix )

Returns: An index that is always a safe index for the given prefix.

Todo:: These functions are all used by the function_symbol_generator and should probably not be public. \threadsafe

Definition at line 118 of file function_symbol_pool.cpp.

◆ resize_if_needed()

void function_symbol_pool::resize_if_needed ( )

Resize the function symbol pool if necessary.

Definition at line 222 of file function_symbol_pool.cpp.

◆ size()

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

inlinenoexcept

Returns: The number of function symbols stored in this pool.

Definition at line 68 of file function_symbol_pool.h.

◆ sweep()

void function_symbol_pool::sweep ( )

Collect all garbage function symbols.

Definition at line 173 of file function_symbol_pool.cpp.

Member Data Documentation

◆ m_as_empty_list

function_symbol atermpp::detail::function_symbol_pool::m_as_empty_list

private

Definition at line 97 of file function_symbol_pool.h.

◆ m_as_int

function_symbol atermpp::detail::function_symbol_pool::m_as_int

private

Definition at line 95 of file function_symbol_pool.h.

◆ m_as_list

function_symbol atermpp::detail::function_symbol_pool::m_as_list

private

Definition at line 96 of file function_symbol_pool.h.

◆ m_function_symbol_metrics

mcrl2::utilities::cache_metric atermpp::detail::function_symbol_pool::m_function_symbol_metrics

private

Track the number of function symbols found in or added to the set.

Definition at line 100 of file function_symbol_pool.h.

◆ m_mutex

mcrl2::utilities::mutex atermpp::detail::function_symbol_pool::m_mutex

mutableprivate

Definition at line 92 of file function_symbol_pool.h.

◆ m_prefix_to_register_function_map

std::map<std::string, std::shared_ptr<std::size_t> > atermpp::detail::function_symbol_pool::m_prefix_to_register_function_map

private

A map that records a function for each prefix that must be called to set the postfix number to a sufficiently high number if a function symbol with the same prefix string is registered.

Definition at line 90 of file function_symbol_pool.h.

◆ m_symbol_set

unordered_set atermpp::detail::function_symbol_pool::m_symbol_set

private

Stores the underlying function symbols.

Definition at line 85 of file function_symbol_pool.h.

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

atermpp/include/mcrl2/atermpp/detail/function_symbol_pool.h
atermpp/source/function_symbol_pool.cpp

Public Member Functions

Private Types

Private Member Functions

Private Attributes

Detailed Description

Member Typedef Documentation

◆ unordered_set

Constructor & Destructor Documentation

◆ function_symbol_pool()

Member Function Documentation

◆ as_empty_list()

◆ as_int()

◆ as_list()

◆ capacity()

◆ create() [1/2]

◆ create() [2/2]

◆ create_helper()

◆ deregister()

◆ get_sufficiently_large_postfix_index()

◆ register_prefix()

◆ resize_if_needed()

◆ size()

◆ sweep()

Member Data Documentation

◆ m_as_empty_list

◆ m_as_int

◆ m_as_list

◆ m_function_symbol_metrics

◆ m_mutex

◆ m_prefix_to_register_function_map

◆ m_symbol_set