mCRL2
|
The interface for the term library. Provides the storage of of all classes of terms. More...
#include <aterm_pool.h>
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 |
Friends | |
class | thread_aterm_pool |
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.
|
inline |
Definition at line 24 of file aterm_pool_implementation.h.
|
inline |
|
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.
|
inlinenoexcept |
Definition at line 124 of file aterm_pool.h.
|
inlinenoexcept |
Definition at line 118 of file aterm_pool.h.
|
inlinenoexcept |
Definition at line 121 of file aterm_pool.h.
|
inlinenoexcept |
The number of terms that can be stored without resizing.
Definition at line 139 of file aterm_pool_implementation.h.
|
inlineprivate |
Force garbage collection on all storages.
threadsafe
Definition at line 94 of file aterm_pool_implementation.h.
|
inlineprivate |
Collect garbage on all storages.
threadsafe
Definition at line 199 of file aterm_pool_implementation.h.
|
inlineprivate |
Creates a function application with the given function symbol and arguments.
Definition at line 303 of file aterm_pool_implementation.h.
|
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.
|
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.
|
inline |
Creates a function symbol pair (name, arity).
Definition at line 282 of file aterm_pool_implementation.h.
|
inline |
Creates a function symbol pair (name, arity).
Definition at line 287 of file aterm_pool_implementation.h.
|
inlineprivate |
Creates a integral term with the given value.
Definition at line 292 of file aterm_pool_implementation.h.
|
inlineprivate |
Creates a term with the given function symbol.
Definition at line 297 of file aterm_pool_implementation.h.
|
inlineprivate |
Triggers garbage collection and resizing when conditions are met.
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.
|
inlinenoexcept |
Definition at line 115 of file aterm_pool.h.
|
inline |
Enable garbage collection when passing true and disable otherwise.
Definition at line 130 of file aterm_pool.h.
|
inline |
Definition at line 132 of file aterm_pool.h.
|
inline |
Prints various performance statistics for the term pool.
Definition at line 118 of file aterm_pool_implementation.h.
|
inlineprivate |
Definition at line 419 of file aterm_pool_implementation.h.
|
inline |
Register a thread specific aterm pool.
threadsafe
Definition at line 100 of file aterm_pool_implementation.h.
|
inline |
Remove thread specific aterm pool.
threadsafe
Definition at line 106 of file aterm_pool_implementation.h.
|
inlineprivate |
Resizes all storages if necessary.
threadsafe
Definition at line 379 of file aterm_pool_implementation.h.
|
inlineprivate |
Definition at line 183 of file aterm_pool.h.
|
inline |
Definition at line 154 of file aterm_pool_implementation.h.
|
friend |
Definition at line 87 of file aterm_pool.h.
|
private |
Storage for term_appl with a dynamic number of arguments larger than 7.
Definition at line 210 of file aterm_pool.h.
|
private |
Storage for function applications with a fixed number of arguments.
Definition at line 207 of file aterm_pool.h.
|
private |
Track the number of terms destroyed and reduce the freelist.
Definition at line 213 of file aterm_pool.h.
|
private |
Definition at line 214 of file aterm_pool.h.
|
private |
Represents an empty list.
Definition at line 222 of file aterm_pool.h.
|
private |
Definition at line 216 of file aterm_pool.h.
|
private |
Storage for the function symbols.
Definition at line 192 of file aterm_pool.h.
|
private |
Storage for integral terms.
Definition at line 195 of file aterm_pool.h.
|
private |
|
private |
The set of local aterm pools.
Definition at line 189 of file aterm_pool.h.