mCRL2
Loading...
Searching...
No Matches
aterm_pool_storage.h
Go to the documentation of this file.
1// Author(s): Maurice Laveaux.
2// Copyright: see the accompanying file COPYING or copy at
3// https://github.com/mCRL2org/mCRL2/blob/master/COPYING
4//
5// Distributed under the Boost Software License, Version 1.0.
6// (See accompanying file LICENSE_1_0.txt or copy at
7// http://www.boost.org/LICENSE_1_0.txt)
8//
9
10#ifndef ATERMPP_DETAIL_ATERM_POOL_STORAGE_H
11#define ATERMPP_DETAIL_ATERM_POOL_STORAGE_H
12
16
17#include <stack>
18#include <utility>
19
20namespace atermpp
21{
22
23typedef void(*term_callback)(const aterm&);
24
25extern void add_deletion_hook(const function_symbol&, term_callback);
26
27namespace detail
28{
29
30// Forward declaration
31class aterm_pool;
32
34inline void mark_term(const _aterm& root, std::stack<std::reference_wrapper<_aterm>>& todo);
35
39template<typename Element,
40 typename Hash = aterm_hasher<>,
41 typename Equals = aterm_equals<>,
42 std::size_t N = DynamicNumberOfArguments>
44{
45public:
47 Element,
48 Hash,
49 Equals,
50 typename std::conditional_t<N == DynamicNumberOfArguments,
52 typename std::conditional_t<EnableBlockAllocator,
54 std::allocator<Element>>
55 >,
57 false>;
60
62 friend class aterm_pool;
63
65
68
70 std::size_t capacity() const noexcept { return m_term_set.capacity(); }
71
73 bool create_int(aterm& term, std::size_t value);
74
76 bool create_term(aterm& term, const function_symbol& sym);
77
79 template<class ...Terms>
80 bool create_appl(aterm& term, const function_symbol& sym, const Terms&... arguments);
81
85 template<typename ForwardIterator>
87 const function_symbol& sym,
88 ForwardIterator begin,
89 ForwardIterator end);
90
94 template<typename InputIterator,
95 typename TermConverter>
97 const function_symbol& sym,
98 TermConverter converter,
99 InputIterator begin,
100 InputIterator end);
101
104 template<typename ForwardIterator>
106 const function_symbol& sym,
107 ForwardIterator begin,
108 ForwardIterator end);
109
112 template<typename InputIterator,
113 typename TermConverter,
114 typename std::enable_if<!std::is_convertible<
115 typename std::invoke_result<TermConverter, typename InputIterator::value_type>::type,
116 aterm>::value, void>::type* = nullptr>
118 const function_symbol& sym,
119 TermConverter converter,
120 InputIterator begin,
121 InputIterator end);
122
125 template<typename InputIterator,
126 typename TermConverter,
127 typename std::enable_if<std::is_convertible<
128 typename std::invoke_result<TermConverter, typename InputIterator::value_type>::type,
129 aterm>::value, void>::type* = nullptr>
131 const function_symbol& sym,
132 TermConverter converter,
133 InputIterator begin,
134 InputIterator end);
135
138 template<typename InputIterator,
139 typename TermConverter,
140 typename std::enable_if<std::is_same<
141 typename std::invoke_result<TermConverter,
142 typename InputIterator::value_type&,
143 typename InputIterator::value_type>::type,
144 void>::value, void>::type* = nullptr>
146 const function_symbol& sym,
147 TermConverter converter,
148 InputIterator begin,
149 InputIterator end);
150
151
154 void print_performance_stats(const char* identifier) const;
155
158 void sweep();
159
162
164 std::size_t size() const { return m_term_set.size(); }
165
168 m_pool(other.m_pool),
169 m_term_set(std::move(other.m_term_set))
170 {}
171
174
177
178private:
179 using callback_pair = std::pair<function_symbol, term_callback>;
180
184
187
189 template<typename ...Args>
190 bool emplace(aterm_core& term, Args&&... args);
191
194 constexpr bool is_dynamic_storage() const;
195
197 template<std::size_t Arity = N>
198 bool verify_term(const _aterm& term);
199
202
205
207 // std::vector<callback_pair> m_creation_hooks; Not needed anymore.
208 std::vector<callback_pair> m_deletion_hooks;
209
211 std::stack<std::reference_wrapper<_aterm>> todo;
212
213 // Various performance statistics.
214
216 std::size_t m_erasedBlocks = 0;
217};
218
219} // namespace detail
220} // namespace atermpp
221
222
223#endif // ATERMPP_DETAIL_ATERM_POOL_STORAGE_H
The aterm_core base class that provides protection of the underlying shared terms.
Definition aterm_core.h:182
This class allocates _aterm_appl objects where the size is based on the arity of the function symbol.
Definition aterm.h:120
This is the class to which an aterm points.
Definition aterm_core.h:48
This class provides for all types of term storage. It also provides garbage collection via its mark a...
typename unordered_set::iterator iterator
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...
std::stack< std::reference_wrapper< _aterm > > todo
A reusable todo stack.
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.
typename unordered_set::const_iterator const_iterator
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.
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...
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...
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.
std::pair< function_symbol, term_callback > callback_pair
void call_deletion_hook(unprotected_aterm_core term)
Calls the deletion hook attached to the function symbol of this term. \threadsafe.
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 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.
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.
Definition aterm_pool.h:82
An unprotected term does not change the reference count of the shared term when it is copied or moved...
Definition aterm_core.h:32
The block allocator provides the allocator interface for the memory pool class. As such is can be use...
A helper class to keep track of the number of hits and misses for cache-like data structures.
Inherit from this class to prevent it from being copyable.
Definition noncopyable.h:21
A unordered_set with a subset of the interface of std::unordered_set that only stores a single pointe...
unordered_set_iterator< bucket_type, true > const_iterator
size_type size() const noexcept
size_type capacity() const noexcept
a pool allocator class
static constexpr bool EnableBlockAllocator
Enable the block allocator for terms.
void mark_term(const _aterm &root, std::stack< std::reference_wrapper< _aterm > > &todo)
Marks a term and recursively all arguments that are not reachable.
constexpr std::size_t DynamicNumberOfArguments
Indicates that the number of arguments is not known at compile time.
Definition aterm_hash.h:68
The main namespace for the aterm++ library.
Definition algorithm.h:21
void(* term_callback)(const aterm &)
Definition aterm.h:194
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...
normalizer< Function > N(const Function &f)
static constexpr bool GlobalThreadSafe
Enables thread safety for the whole toolset.
STL namespace.