11
12
13
14
15
16
18#ifndef MCRL2_UTILITIES_HASH_UTILITY_H
19#define MCRL2_UTILITIES_HASH_UTILITY_H
25namespace mcrl2::utilities::detail
31 return h1 ^ (h2 + 0x9e3779b9 + (h1<<6) + (h1>>2));
41 return hash_number + (seed << 1) + (seed >> 1);
67template <
class X,
class Y>
86template <
class X,
class Y>
87struct hash<
std::pair < X, Y > >
atermpp::aterm create_nested_function(const std::string &function_name, const std::string &leaf_name, std::size_t number_of_arguments, std::size_t depth)
Create a nested function application f_depth. Where f_0 = c and f_i = f(f_i-1,...,...
atermpp::aterm create_nested_function(const std::string &function_name, const std::string &leaf_name, std::size_t depth)
Create a nested function application f_depth. Where f_0 = c and f_i = f(f_i-1,...,...
void benchmark_threads(std::size_t number_of_threads, F f)
Run the given function f on number_of_threads threads (including the main thread) and report the elap...
The aterm_core base class that provides protection of the underlying shared terms.
aterm_core & operator=(aterm_core &&other) noexcept
Move assignment operator.
~aterm_core() noexcept
Standard destructor.
aterm_core & operator=(const aterm_core &other) noexcept
Assignment operator.
aterm_core(const aterm_core &other) noexcept
Copy constructor.
aterm_core(aterm_core &&other) noexcept
Move constructor.
aterm_core() noexcept
Default constructor.
aterm_core & assign(const aterm_core &other, detail::thread_aterm_pool &pool) noexcept
Assignment operator, to be used if busy and forbidden flags are explicitly available.
aterm_core & unprotected_assign(const aterm_core &other) noexcept
Assignment operator, to be used when the busy flags do not need to be set.
aterm_core(const detail::_aterm *t) noexcept
Constructor based on an internal term data structure. This is not for public use.
aterm(aterm &&other) noexcept=default
aterm()
Default constructor.
aterm & operator=(const aterm &other) noexcept=default
aterm(const aterm &other) noexcept=default
This class has user-declared copy constructor so declare default copy and move operators.
aterm(detail::_term_appl *t)
Constructor.
aterm & operator=(aterm &&other) noexcept=default
aterm(const function_symbol &sym, ForwardIterator begin, ForwardIterator end)
Constructor that provides an aterm based on a function symbol and forward iterator providing the argu...
This class allocates _aterm_appl objects where the size is based on the arity of the function symbol.
T * allocate_args(const function_symbol &symbol, unprotected_aterm_core *)
Allocates space for an _aterm_appl where the arity is given by the function symbol.
T * allocate_args(const function_symbol &symbol, ForwardIterator, ForwardIterator)
Allocates space for an _aterm_appl where the arity is given by the function symbol.
std::allocator< char > m_packed_allocator
static constexpr std::size_t term_appl_size(std::size_t arity)
void destroy(T *element)
Specialize destroy for _aterm_appl to only destroy the function symbol. The reference count for the a...
constexpr std::size_t capacity() const
void deallocate(T *element, std::size_t)
constexpr bool has_free_slots() const noexcept
constexpr std::size_t consolidate() const noexcept
void construct(T *element, const function_symbol &symbol, ForwardIterator begin, ForwardIterator end)
Constructs an _aterm_appl with arguments taken from begin, the arity is given by the function symbol.
This class stores a term followed by N arguments. Where N should be equal to the arity of the functio...
_aterm_appl(const function_symbol &symbol, Iterator it, Iterator end, bool)
constructs a term application with the given symbol and its arguments from the iterator.
_aterm_appl(const function_symbol &sym, const Terms &... arguments)
Constructs a term application with the given symbol and arguments.
_aterm_appl(const function_symbol &sym, std::array< unprotected_aterm_core, N > arguments)
Constructs a term application with the given symbol and arguments.
std::array< unprotected_aterm_core, N > m_arguments
operator _aterm_appl< 1 > &()
Convert any known number of arguments aterm<N> to the default _aterm_appl.
_aterm_appl(const function_symbol &sym, Iterator it, Iterator end)
constructs a term application with the given symbol and an iterator where the number of elements is e...
const aterm_core & arg(std::size_t index) const
The underlying integer term that actually carries the integer data.
std::size_t value() const noexcept
_aterm_int(std::size_t value)
Constructs the underlying term from a given value.
This is the class to which an aterm points.
bool is_marked() const
Check if the term is already marked.
_aterm(const function_symbol &symbol)
Create a term from a function symbol.
function_symbol m_function_symbol
const function_symbol & function() const noexcept
void mark() const
Mark this term to be garbage collected.
void unmark() const
Remove the mark from a term.
Stores the data for a function symbol (name, arity) pair.
const std::size_t m_arity
const std::string & name() const noexcept
bool operator==(const _function_symbol &f) const noexcept
std::size_t arity() const noexcept
This class provides for all types of term storage. It also provides garbage collection via its mark a...
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 gi...
constexpr bool is_dynamic_storage() const
std::vector< callback_pair > m_deletion_hooks
This array stores creation, resp deletion, hooks for function symbols.
void print_performance_stats(const char *identifier) const
Prints various performance statistics for this storage.
bool create_appl(aterm &term, const function_symbol &sym, const Terms &... arguments)
Creates a function application with the given function symbol and arguments.
bool create_int(aterm &term, std::size_t value)
Creates a integral term with the given value.
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 gi...
void resize_if_needed()
Resizes the hash table if necessary.
bool verify_sweep()
Check that all arguments of a term application are marked properly.
unordered_set m_term_set
This is the set of term pointers to keep the terms unique.
aterm_pool_storage(aterm_pool &pool)
std::size_t m_erasedBlocks
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.
aterm_pool & m_pool
The pool that this storage belongs to.
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 gi...
std::size_t capacity() const noexcept
bool emplace(aterm_core &term, Args &&... args)
Inserts a term constructed by the given arguments, checks for existing term.
iterator destroy(iterator it)
Removes an element from the unordered set and deallocates it.
void call_deletion_hook(unprotected_aterm_core term)
Calls the deletion hook attached to the function symbol of this term.
aterm_pool_storage(const aterm_pool_storage &other)
A fake copy constructor to fix the issues with GCC 4 and 5.
mcrl2::utilities::cache_metric m_term_metric
Count the number of times a term has been found in or is added to the set.
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 gi...
bool verify_term(const _aterm &term)
Verify that the given term was constructed properly.
bool verify_mark()
Check that all arguments of a term application are marked properly.
bool create_term(aterm &term, const function_symbol &sym)
Creates a term with the given function symbol.
bool resize_is_needed() const
Check whether resizing the hash table is needed.
void sweep()
sweep Destroys all terms that are not reachable. Requires that mark() was called first.
The interface for the term library. Provides the storage of of all classes of terms.
const function_symbol & as_int() noexcept
void enable_resize(bool enable)
Enable automatic hash table resizing when passing true and disable otherwise.
bool create_appl(aterm &term, const function_symbol &sym, const Terms &... arguments)
Creates a function application with the given function symbol and arguments.
std::atomic< bool > m_enable_garbage_collection
function_symbol create_function_symbol(const std::string &name, std::size_t arity, bool check_for_registered_functions=false)
Creates a function symbol pair (name, arity).
function_symbol create_function_symbol(std::string &&name, std::size_t arity, bool check_for_registered_functions=false)
Creates a function symbol pair (name, arity).
void remove_thread_aterm_pool(thread_aterm_pool_interface &pool)
Remove thread specific aterm pool.
std::vector< thread_aterm_pool_interface * > m_thread_pools
The set of local aterm pools.
bool create_int(aterm &term, std::size_t val)
Creates a integral term with the given value.
function_symbol_pool m_function_symbol_pool
Storage for the function symbols.
void collect_impl(mcrl2::utilities::shared_mutex &mutex)
Collect garbage on all storages.
bool resize_is_needed(mcrl2::utilities::shared_mutex &shared) const
Resizes all storages if necessary.
arbitrary_function_application_storage m_appl_dynamic_storage
Storage for term_appl with a dynamic number of arguments larger than 7.
const function_symbol & as_empty_list() noexcept
const function_symbol & as_list() noexcept
aterm_core m_empty_list
Represents an empty list.
void print_performance_statistics() const
Prints various performance statistics for the term pool.
std::atomic< long > m_count_until_collection
Track the number of terms destroyed and reduce the freelist.
void register_thread_aterm_pool(thread_aterm_pool_interface &pool)
Register a thread specific aterm pool.
bool create_term(aterm &term, const function_symbol &sym)
Creates a term with the given function symbol.
std::size_t protection_set_size() const
void collect(mcrl2::utilities::shared_mutex &mutex)
Force garbage collection on all storages.
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 gi...
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 gi...
aterm & empty_list() noexcept
mcrl2::utilities::shared_mutex m_shared_mutex
Automatic hash table resizing is enabled.
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.
function_symbol_pool & get_symbol_pool()
integer_term_storage m_int_storage
Storage for integral terms.
std::atomic< bool > m_enable_resize
Garbage collection is enabled.
void created_term(mcrl2::utilities::shared_mutex &mutex, long &count_until_check)
Triggers garbage collection and resizing when conditions are met.
void resize_if_needed(mcrl2::utilities::shared_mutex &shared)
Resizes all storages if necessary.
void enable_garbage_collection(bool enable)
Enable garbage collection when passing true and disable otherwise.
std::size_t capacity() const noexcept
The number of terms that can be stored without resizing.
This class stores a set of function symbols.
void mark()
Mark the terms created by this thread to prevent them being garbage collected.
std::function< void()> m_mark_function
std::function< void()> m_print_function
std::size_t protection_set_size() const
thread_aterm_pool_interface(aterm_pool &pool, std::function< void()> mark_function, std::function< void()> print_function, std::function< std::size_t()> protection_set_size_function)
void print_local_performance_statistics() const
Print performance statistics for data stored for this thread.
std::function< std::size_t()> m_protection_set_size_function
~thread_aterm_pool_interface()
std::stack< std::reference_wrapper< _aterm > > m_todo
A reusable todo stack.
void swap(function_symbol &f) noexcept
Swap this function with its argument.
bool operator!=(const function_symbol &f) const
Inequality test.
function_symbol & operator=(const function_symbol &other) noexcept=default
function_symbol(function_symbol &&other) noexcept=default
bool operator>=(const function_symbol &f) const
Comparison operation.
bool operator==(const function_symbol &f) const
Equality test.
function_symbol(detail::_function_symbol::ref &&f)
Constructor for internal use only.
bool operator<(const function_symbol &f) const
Comparison operation.
function_symbol(const function_symbol &other) noexcept=default
This class has non-trivial destructor so declare default copy and move operators.
void destroy()
Calls the function symbol pool to free our used memory.
function_symbol & operator=(function_symbol &&other) noexcept=default
std::size_t arity() const
Return the arity (number of arguments) of the function symbol (function_symbol).
detail::_function_symbol::ref m_function_symbol
The shared reference to the underlying function symbol.
const std::string & name() const
Return the name of the function_symbol.
bool operator>(const function_symbol &f) const
Comparison operation.
function_symbol()=default
bool operator<=(const function_symbol &f) const
Comparison operation.
term_appl_iterator operator++(int)
Postfix increment.
bool operator==(const term_appl_iterator &other) const
Equality of iterators.
term_appl_iterator operator-(ptrdiff_t n) const
Decrease by a constant value.
term_appl_iterator & operator--()
Prefix decrement.
ptrdiff_t operator-(const term_appl_iterator &other) const
The negative distance from this to the other iterator.
term_appl_iterator & operator++()
Prefix increment.
term_appl_iterator & operator-=(difference_type n)
Decrease the iterator with n steps.
const Term & operator[](difference_type n) const
The dereference operator.
term_appl_iterator operator+(ptrdiff_t n) const
Increase by a constant value.
friend term_appl_iterator< Derived > detail::aterm_appl_iterator_cast(term_appl_iterator< Base > a)
term_appl_iterator operator--(int)
Post decrement an iterator.
const Term * operator->() const
Dereference the current iterator.
term_appl_iterator & operator+=(difference_type n)
Increase the iterator with n steps.
const Term & operator*() const
The dereference operator.
term_appl_iterator(const Term *t)
Constructor.
ptrdiff_t distance_to(const term_appl_iterator &other) const
Provide the distance to the other iterator.
A unordered_map class in which aterms can be stored.
An unprotected term does not change the reference count of the shared term when it is copied or moved...
bool type_is_list() const noexcept
Dynamic check whether the term is an aterm_list.
void swap(unprotected_aterm_core &t) noexcept
Swaps this term with its argument.
bool operator==(const unprotected_aterm_core &t) const
Comparison operator.
unprotected_aterm_core() noexcept
Default constuctor.
bool type_is_appl() const noexcept
Dynamic check whether the term is an aterm.
bool defined() const
Returns true if this term is not equal to the term assigned by the default constructor of aterms,...
friend detail::_aterm * detail::address(const unprotected_aterm_core &t)
const detail::_aterm * m_term
const function_symbol & function() const
Yields the function symbol in an aterm.
bool type_is_int() const noexcept
Dynamic check whether the term is an aterm_int.
unprotected_aterm_core(const detail::_aterm *term) noexcept
Constructor.
Inherit from this class to prevent it from being copyable.
noncopyable & operator=(const noncopyable &)=delete
noncopyable & operator=(noncopyable &&)=default
noncopyable(const noncopyable &)=delete
noncopyable(noncopyable &&)=default
Stores a reference count that can be incremented and decremented.
SizeType m_reference_count
static void count_reference_count_changes()
Increment the number of reference count changes.
shared_reference_counted()
std::size_t reference_count() const
Obtain the reference count.
void increment_reference_count() const
Increment the reference count by one.
static std::atomic< std::size_t > & reference_count_changes()
Obtain the number of times that this reference count has changed.
void decrement_reference_count() const
Decrement the reference count by one.
A reference counted reference to a shared_reference_counted object.
bool operator==(const shared_reference< T > &other) const noexcept
Address equality operator.
shared_reference< T > & operator=(shared_reference< T > &&other) noexcept
Move assignment constructor.
T * operator->() const noexcept
bool defined() const
Check whether the shared_reference has a valid reference.
T & operator*() const noexcept
bool tagged() const noexcept
shared_reference() noexcept
The default constructor.
utilities::tagged_pointer< T > m_reference
shared_reference< T > & operator=(const shared_reference< T > &other) noexcept
Copy assignment constructor.
shared_reference(shared_reference< T > &&other) noexcept
Move constructor.
shared_reference(const shared_reference< T > &other) noexcept
Copy constructor.
shared_reference(T *reference) noexcept
Takes ownership of the passed reference, which means that its reference count is incremented.
void swap(shared_reference< T > &other) noexcept
Swaps *this with the other shared reference.
A pointer storage object that uses a least significant bit as a mark. Can be used by objects that are...
const T * operator->() const
bool operator==(const tagged_pointer &other) const
bool operator==(std::nullptr_t) const
void untag() const
Remove the tag.
void swap(tagged_pointer< T > &other) noexcept
const T & operator*() const
void tag() const
Apply a tag to the pointer that can be checked with tagged().
tagged_pointer & operator=(std::nullptr_t)
std::conditional_t< detail::GlobalThreadSafe, detail::atomic_wrapper< T * >, T * > m_pointer
Implements a simple stopwatch that starts on construction.
static constexpr bool EnableGarbageCollection
Enable garbage collection.
static constexpr bool EnableHashtableMetrics
Enable to print hashtable collision, size and number of buckets.
aterm_pool & g_term_pool()
obtain a reference to the global aterm pool.
void debug_print(std::ostream &o, const _aterm *t, std::size_t d=3)
bool equal_args(const _aterm_appl< 8 > &term, const Tp &... t)
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.
static constexpr bool EnableCreationMetrics
Enable to obtain the percentage of terms found compared to allocated.
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 vari...
function_symbol g_as_empty_list
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...
std::size_t combine(const std::size_t hnr, const unprotected_aterm_core &term)
Auxiliary function to combine hnr with aterms.
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.
function_symbol g_as_list
static constexpr bool EnableGarbageCollectionMetrics
Enable to print garbage collection statistics.
void start_gc_stress_thread()
Spawns a dedicated background thread that continuously triggers garbage collection.
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...
aterm_pool & g_aterm_pool_instance()
A reference to the global term pool storage.
static constexpr bool EnableAggressiveGarbageCollection
Performs garbage collection intensively for testing purposes.
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 ...
function_symbol g_as_int
These function symbols are used to indicate integer, list and empty list terms.
std::size_t combine_args(std::size_t seed, const Tp &... t)
static constexpr bool EnableBlockAllocator
Enable the block allocator for terms.
static std::size_t xorshift(const std::size_t n, const std::size_t i)
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.
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.
static constexpr bool EnableVariableRegistrationMetrics
Keep track of the number of variables registered.
std::array< std::byte, sizeof(aterm_pool)> g_aterm_pool_storage
Storage for a global term pool that is not initialized.
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 mark_term(const _aterm &root, std::stack< std::reference_wrapper< _aterm > > &todo)
Marks a term and recursively all arguments that are not reachable.
static constexpr bool EnableGCStressThread
Spawns a dedicated background thread that continuously triggers garbage collection.
constexpr std::size_t DynamicNumberOfArguments
Indicates that the number of arguments is not known at compile time.
The main namespace for the aterm++ library.
std::string pp(const atermpp::aterm &t)
Transform an aterm to an ascii string.
void add_deletion_hook(const function_symbol &, term_callback)
Check for reasonably sized aterm (32 bits, 4 bytes) This check might break on perfectly valid archite...
void make_term_appl(Term &target, const function_symbol &sym, ForwardIterator begin, ForwardIterator end)
Constructor an aterm in a variable based on a function symbol and an forward iterator providing the a...
std::size_t hash_combine(const std::size_t h1, const std::size_t h2)
static constexpr bool GlobalThreadSafe
Enables thread safety for the whole toolset.
std::size_t hash_combine_cheap(const std::size_t seed, const std::size_t hash_number)
Auxiliary function to combine seed with a hash number.
T * tag(const T *p)
Applies a tag to a pointer.
T * pointer(const detail::atomic_wrapper< T * > &p)
T * tag(const detail::atomic_wrapper< T * > &p)
constexpr bool is_iterable_v
static constexpr bool EnableReferenceCountMetrics
Enable to count the number of reference count changes.
bool tagged(const detail::atomic_wrapper< T * > &p)
constexpr bool is_iterator_v
void swap(atermpp::aterm &t1, atermpp::aterm &t2) noexcept
Swaps two term_applss.
void swap(mcrl2::utilities::shared_reference< T > &a, mcrl2::utilities::shared_reference< T > &b) noexcept
void swap(atermpp::unprotected_aterm_core &t1, atermpp::unprotected_aterm_core &t2) noexcept
Swaps two aterms.
int main(int argc, char *argv[])
bool operator()(const _aterm &term, const function_symbol &symbol, const Args &... args) const noexcept
bool operator()(const _aterm &term, const function_symbol &symbol, std::array< unprotected_aterm_core, N > key) const noexcept
Returns true iff first and second are value-equivalent.
bool operator()(const _aterm &first, const _aterm &second) const noexcept
bool operator()(const _aterm &term, const function_symbol &symbol) const noexcept
bool operator()(const _aterm &term, const function_symbol &symbol, unprotected_aterm_core *arguments) const noexcept
Computes the hash of the given term.
std::size_t operator()(const function_symbol &symbol, const Args &... args) const noexcept
std::size_t operator()(const function_symbol &symbol, std::array< unprotected_aterm_core, N > key) const noexcept
Computes the hash of the given term.
std::size_t operator()(const function_symbol &symbol) const noexcept
std::size_t operator()(const _aterm &term) const noexcept
Implementation.
std::size_t operator()(const function_symbol &symbol, unprotected_aterm_core *arguments) const noexcept
Returns true iff the given term(s) or value are equivalent.
bool operator()(const _aterm_int &term, std::size_t value) const noexcept
bool operator()(const _aterm_int &first, const _aterm_int &second) const noexcept
Computes the hash of the integral term arguments.
std::size_t operator()(const _aterm_int &term) const noexcept
std::size_t operator()(std::size_t value) const noexcept
void operator()(Term &result, const Term &t) const
const Term & operator()(const Term &t) const
Term & operator()(Term &t) const
True iff the given function symbols are equal to eachother or to the given key.
bool operator()(const _function_symbol &first, const _function_symbol &second) const noexcept
Computes the hash for given function symbol objects and for the function_symbol_key.
std::size_t operator()(const _function_symbol &symbol) const noexcept
atomic_wrapper & operator=(const atomic_wrapper< T > &other)
atomic_wrapper(const atomic_wrapper< T > &other)
atomic_wrapper(const T t)
Checks whether condition holds for all types passed as variadic template.
static constexpr size_t arity
A typetrait that is std::true_type iff std::begin() and std::end() can be called on type T.
A typetrait that is std::true_type iff the given type has the iterator traits.
std::size_t operator()(const atermpp::aterm &t) const
std::size_t operator()(const atermpp::aterm_core &t) const
std::size_t operator()(const atermpp::detail::_aterm *term) const
std::size_t operator()(const atermpp::detail::_function_symbol &f) const
std::size_t operator()(const atermpp::function_symbol &f) const
std::size_t operator()(const atermpp::unprotected_aterm_core &term) const
std::size_t operator()(const mcrl2::utilities::tagged_pointer< T > &p) const
std::size_t operator()(const std::pair< X, Y > &p) const
std::size_t operator()(const std::vector< X > &v) const