mCRL2
Loading...
Searching...
No Matches
aterm_pool_storage_implementation.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 MCRL2_ATERMPP_ATERM_POOL_STORAGE_IMPLEMENTION_H
11#define MCRL2_ATERMPP_ATERM_POOL_STORAGE_IMPLEMENTION_H
12#pragma once
13
14#include <type_traits>
15#include <cstring>
18
19
20
21namespace atermpp
22{
23namespace detail
24{
25
28template<std::size_t N,
29 typename InputIterator,
30 typename TermConverter,
31 typename std::enable_if<mcrl2::utilities::is_iterator<InputIterator>::value, void>::type* = nullptr,
32 typename std::enable_if<std::is_convertible<
33 typename std::invoke_result<TermConverter, typename InputIterator::value_type>::type,
34 aterm>::value, void>::type* = nullptr>
35inline std::array<unprotected_aterm_core, N> construct_arguments(InputIterator it, InputIterator end, TermConverter converter)
36{
37 // The end is only used for debugging to ensure that the arity and std::distance(it, end) match.
39
40 // Copy the arguments into this array.
41 std::array<unprotected_aterm_core, N> arguments;
42 for (size_t i = 0; i < N; ++i)
43 {
44 assert(it != end);
45 arguments[i] = converter(*it);
46
47 ++it;
48 }
49 assert(it == end);
50
51 return arguments;
52}
53
56template<std::size_t N,
57 typename InputIterator,
58 typename TermConverter,
59 typename std::enable_if<mcrl2::utilities::is_iterator<InputIterator>::value, void>::type* = nullptr,
60 typename std::enable_if<std::is_same<
61 typename std::invoke_result<TermConverter,
62 typename InputIterator::value_type&,
63 typename InputIterator::value_type>::type,
64 void>::value, void>::type* = nullptr>
65inline std::array<unprotected_aterm_core, N> construct_arguments(InputIterator it, InputIterator end, TermConverter converter)
66{
67 // The end is only used for debugging to ensure that the arity and std::distance(it, end) match.
69
70 // Copy the arguments into this array. Doesn't change any reference count, because they are unprotected terms.
71 std::array<unprotected_aterm_core, N> arguments;
72 for (size_t i = 0; i < N; ++i)
73 {
74 assert(it != end);
75 typename InputIterator::value_type& t= *reinterpret_cast<typename InputIterator::value_type*>(&arguments[i]);
76 converter(t, *it);
77 ++it;
78 }
79 assert(it == end);
80
81 return arguments;
82}
83
84void mark_term(const _aterm& root, std::stack<std::reference_wrapper<_aterm>>& todo)
85{
86 if (!root.is_marked())
87 {
88 // Do not use the stack, because this might run out of stack memory for large lists.
89 todo.push(const_cast<_aterm&>(root));
90
91 // Mark the term depth-first to reduce the maximum todo size required.
92 while (!todo.empty())
93 {
94 _aterm& term = todo.top();
95 todo.pop();
96
97 // Each term should be marked.
98 term.mark();
99 // Determine the arity of the function application.
100 const std::size_t arity = term.function().arity();
101 _term_appl& term_appl = static_cast<_term_appl&>(term);
102
103 for (std::size_t i = 0; i < arity; ++i)
104 {
105 // Marks all arguments that are not already (marked as) reachable, because the current
106 // term is reachable and as such its arguments are reachable as well.
107 _aterm& argument = *detail::address(term_appl.arg(i));
108 if (!argument.is_marked())
109 {
110 argument.mark();
111
112 // Add the argument to be explored as well.
113 todo.push(argument);
114 }
115 }
116
117 }
118 }
119}
120
121#define ATERM_POOL_STORAGE_TEMPLATES template<typename Element, typename Hash, typename Equals, std::size_t N>
122#define ATERM_POOL_STORAGE aterm_pool_storage<Element, Hash, Equals, N>
123
125ATERM_POOL_STORAGE::aterm_pool_storage(aterm_pool& pool) :
126 m_pool(pool),
127 m_term_set(1 << 14)
128{}
129
131void ATERM_POOL_STORAGE::add_deletion_hook(function_symbol sym, term_callback callback)
132{
133 for (const auto& hook : m_deletion_hooks)
134 {
136 assert(hook.first != sym);
137 }
138 m_deletion_hooks.emplace_back(sym, callback);
139}
140
142bool ATERM_POOL_STORAGE::create_int(aterm& term, std::size_t value)
143{
144 return emplace(reinterpret_cast<aterm_core&>(term), value); // TODO: remove reinterpret_cast
145}
146
148bool ATERM_POOL_STORAGE::create_term(aterm& term, const function_symbol& symbol)
149{
150 assert(symbol.arity() == 0);
151 return emplace(reinterpret_cast<aterm_core&>(term), symbol); // TODO: remove reinterpret_cast
152}
153
154template <std::size_t N>
155void store_in_argument_array_(std::size_t , std::array<unprotected_aterm_core, N>& )
156{}
157
158template <std::size_t N, class FUNCTION_OR_TERM_TYPE, typename... Args>
159void store_in_argument_array_(std::size_t i,
160 std::array<unprotected_aterm_core, N>& argument_array,
161 FUNCTION_OR_TERM_TYPE& function_or_term,
162 const Args&... args)
163{
164 if constexpr (std::is_convertible<FUNCTION_OR_TERM_TYPE,atermpp::aterm>::value)
165 {
166 argument_array[i]=function_or_term;
167 }
168 // check whether the function_or_term invoked on an empty argument yields an aterm.
170 {
171 argument_array[i]=function_or_term();
172 }
173 // Otherwise function_or_term is supposed to have type void(term& result), putting the term in result.
174 else
175 {
176 // function_or_term(static_cast<Term&>(argument_array[i]));
177
178 typedef mcrl2::utilities::function_traits<decltype(&FUNCTION_OR_TERM_TYPE::operator())> traits;
179 function_or_term(static_cast<typename traits::template arg<0>::type&>(argument_array[i]));
180 }
181 store_in_argument_array_(i+1, argument_array, args...);
182}
183
184template <std::size_t N, typename... Args>
185void store_in_argument_array(std::array<unprotected_aterm_core, N>& argument_array,
186 const Args&... args)
187{
188 store_in_argument_array_(0, argument_array, args...);
189}
190
191
192
194template<class ...Terms>
195bool ATERM_POOL_STORAGE::create_appl(aterm& term, const function_symbol& symbol, const Terms&... arguments)
196{
197 assert(symbol.arity() == sizeof...(arguments));
198 if constexpr (detail::are_terms<Terms...>::value)
199 {
200 return emplace(reinterpret_cast<aterm_core&>(term), symbol, arguments...); // TODO remove reinterpret_cast.
201 }
202 else
203 {
204 std::array<unprotected_aterm_core, N> argument_array;
205
206 // Evaluate the functions or terms and put the result in "argument_array".
207 store_in_argument_array(argument_array, arguments...);
208
209 return emplace(term, symbol, argument_array.begin(), argument_array.end());
210 }
211}
212
214template<typename ForwardIterator>
215bool ATERM_POOL_STORAGE::create_appl_iterator(aterm& term,
216 const function_symbol& symbol,
217 ForwardIterator begin,
218 ForwardIterator end)
219{
220 return emplace(term, symbol, begin, end);
221}
222
224template<typename InputIterator, typename TermConverter>
225bool ATERM_POOL_STORAGE::create_appl_iterator(aterm& term,
226 const function_symbol& symbol,
227 TermConverter converter,
228 InputIterator begin,
229 InputIterator end)
230{
231 std::array<unprotected_aterm_core, N> arguments = construct_arguments<N>(begin, end, converter);
232 return emplace(term, symbol, arguments);
233}
234
236template<typename ForwardIterator>
237bool ATERM_POOL_STORAGE::create_appl_dynamic(aterm& term,
238 const function_symbol& symbol,
239 ForwardIterator begin,
240 ForwardIterator end)
241{
242 return emplace(term, symbol, begin, end);
243}
244
246template<typename InputIterator,
247 typename TermConverter,
248 typename std::enable_if<std::is_convertible<
249 typename std::invoke_result<TermConverter, typename InputIterator::value_type>::type,
250 aterm>::value, void>::type*>
251bool ATERM_POOL_STORAGE::create_appl_dynamic(aterm& term,
252 const function_symbol& symbol,
253 TermConverter converter,
254 InputIterator it,
255 InputIterator end)
256{
257 // The end is only used for debugging to ensure that the arity and std::distance(it, end) match.
259
260 MCRL2_DECLARE_STACK_ARRAY(arguments, unprotected_aterm_core, symbol.arity());
261 for (std::size_t i = 0; i < symbol.arity(); ++i)
262 {
263 assert(it != end);
264 arguments[i] = converter(*it);
265 ++it;
266 }
267 assert(it == end);
268
269 // Find or create a new term and return it.
270 return emplace(term, symbol, arguments.begin(), arguments.end());
271}
272
274template<typename InputIterator,
275 typename TermConverter,
276 typename std::enable_if<std::is_same<
277 typename std::invoke_result<TermConverter,
278 typename InputIterator::value_type&,
279 typename InputIterator::value_type>::type,
280 void>::value, void>::type*>
281bool ATERM_POOL_STORAGE::create_appl_dynamic(aterm& term,
282 const function_symbol& symbol,
283 TermConverter converter,
284 InputIterator it,
285 InputIterator end)
286{
287 // The end is only used for debugging to ensure that the arity and std::distance(it, end) match.
289
290 MCRL2_DECLARE_STACK_ARRAY(arguments, unprotected_aterm_core, symbol.arity());
291 for (std::size_t i = 0; i < symbol.arity(); ++i)
292 {
293 assert(it != end);
294 // The construction below is possible as with protection sets the new term simply
295 // overwrites the object at arguments[i].
296 converter(reinterpret_cast<typename InputIterator::value_type&>(arguments[i]), *it);
297 ++it;
298 }
299 assert(it == end);
300
301 // Find or create a new term and return it.
302 return emplace(term, symbol, arguments.begin(), arguments.end());
303}
304
305
307void ATERM_POOL_STORAGE::print_performance_stats(const char* identifier) const
308{
309 if (EnableHashtableMetrics)
310 {
311 mCRL2log(mcrl2::log::info) << "g_term_pool(" << identifier << ") hashtable:\n";
313 }
314
315 if (EnableGarbageCollectionMetrics && m_erasedBlocks > 0)
316 {
317 mCRL2log(mcrl2::log::info) << "g_term_pool(" << identifier << "): Consolidate removed " << m_erasedBlocks << " blocks.\n";
318 }
319
320 if (EnableCreationMetrics)
321 {
322 mCRL2log(mcrl2::log::info) << "g_term_pool(" << identifier << "): emplace() " << m_term_metric.message() << ".\n";
323 }
324}
325
327void ATERM_POOL_STORAGE::sweep()
328{
329 // Iterate over all terms and removes the ones that are marked.
330 for (auto it = m_term_set.begin(); it != m_term_set.end(); )
331 {
332 const Element& term = *it;
333
334 if (!term.is_marked())
335 {
336 // For constants, i.e., arity zero and integer terms we do not mark, but use their reachability directly.
337 it = destroy(it);
338 }
339 else
340 {
341 // Reset terms that have been marked.
342 term.unmark();
343 ++it;
344 }
345 }
346
347 if constexpr (EnableBlockAllocator)
348 {
349 // Clean up unnecessary blocks.
350 m_erasedBlocks = m_term_set.get_allocator().consolidate();
351 }
352}
353
355void ATERM_POOL_STORAGE::resize_if_needed()
356{
357 m_term_set.rehash_if_needed();
358}
359
361
363void ATERM_POOL_STORAGE::call_deletion_hook(unprotected_aterm_core term)
364{
365 for (const auto& [symbol, callback] : m_deletion_hooks)
366 {
367 if (symbol == term.function())
368 {
369 assert(verify_term(*detail::address(term)));
370 callback(reinterpret_cast<const aterm&>(term)); // TODO Check whether this cast is OK. It was a static cast.
371 }
372 }
373}
374
375
377bool ATERM_POOL_STORAGE::verify_mark()
378{
379 // Check for consistency that if a term is marked then its arguments are as well.
380 for (const Element& term : m_term_set)
381 {
382 if (term.is_marked() && term.function().arity() > 0)
383 {
384 const _term_appl& ta = static_cast<_term_appl&>(const_cast<Element&>(term));
385 for (std::size_t i = 0; i < ta.function().arity(); ++i)
386 {
387 assert(detail::address(ta.arg(i))->is_marked());
388 }
389 }
390 }
391 return true;
392}
393
395bool ATERM_POOL_STORAGE::verify_sweep()
396{
397 // Check that no argument was removed from a reachable term.
398 for (const Element& term : m_term_set)
399 {
400 (void)term;
401 assert(verify_term(term));
402 }
403 return true;
404}
405
407
409typename ATERM_POOL_STORAGE::iterator ATERM_POOL_STORAGE::destroy(iterator it)
410{
411 // Store the term temporarily to be able to deallocate it after removing it from the set.
412 const Element& term = *it;
413
414 // Trigger the deletion hook before the term is actually destroyed.
415 call_deletion_hook(&term);
416
417 // Remove them from the hash table, will also destroy terms with fixed arity.
418 return m_term_set.erase(it);
419}
420
422template<typename ...Args>
423bool ATERM_POOL_STORAGE::emplace(aterm_core& term, Args&&... args)
424{
425 auto [it, added] = m_term_set.emplace(std::forward<Args>(args)...);
426 new (&term) atermpp::unprotected_aterm_core(&*it);
427
428 if (added)
429 {
430 if (EnableCreationMetrics) { m_term_metric.miss(); }
431 }
432 else if (EnableCreationMetrics)
433 {
434 // A term was already found in the set.
435 m_term_metric.hit();
436 }
437
438 return added;
439}
440
442constexpr bool ATERM_POOL_STORAGE::is_dynamic_storage() const
443{
444 return N == DynamicNumberOfArguments;
445}
446
448template<std::size_t Arity>
449bool ATERM_POOL_STORAGE::verify_term(const _aterm& term)
450{
451 // Check that a valid function symbol was used and that its arity belongs to this storage.
452 assert(term.function().defined());
453 assert(Arity == DynamicNumberOfArguments ? true : term.function().arity() == N);
454
455 // Check that all of its arguments are defined.
456 if (term.function().arity() > 0)
457 {
458 const _term_appl& ta = static_cast<const _term_appl&>(term);
459 assert(ta.function().defined());
460 for (std::size_t i = 0; i < ta.function().arity(); ++i)
461 {
462 assert(ta.arg(i).defined());
463 assert(&ta!=detail::address(ta.arg(i)));
464 verify_term<DynamicNumberOfArguments>(*detail::address(ta.arg(i)));
465 }
466 }
467 return true;
468}
469
470#undef ATERM_POOL_STORAGE_TEMPLATES
471#undef ATERM_POOL_STORAGE
472
473} // namespace detail
474} // namespace atermpp
475
476#endif
#define ATERM_POOL_STORAGE_TEMPLATES
The aterm_core base class that provides protection of the underlying shared terms.
Definition aterm_core.h:182
This class stores a term followed by N arguments. Where N should be equal to the arity of the functio...
Definition aterm.h:34
const aterm_core & arg(std::size_t index) const
Definition aterm.h:97
This is the class to which an aterm points.
Definition aterm_core.h:48
bool is_marked() const
Check if the term is already marked.
Definition aterm_core.h:73
const function_symbol & function() const noexcept
Definition aterm_core.h:55
void mark() const
Mark this term to be garbage collected.
Definition aterm_core.h:61
std::size_t arity() const
Return the arity (number of arguments) of the function symbol (function_symbol).
An unprotected term does not change the reference count of the shared term when it is copied or moved...
Definition aterm_core.h:32
a pool allocator class
#define mCRL2log(LEVEL)
mCRL2log(LEVEL) provides the stream used to log.
Definition logger.h:395
_aterm * address(const unprotected_aterm_core &t)
Definition aterm_core.h:239
void store_in_argument_array_(std::size_t, std::array< unprotected_aterm_core, N > &)
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 it...
_aterm_appl<> _term_appl
A default instantiation for the underlying term application.
Definition aterm.h:113
void store_in_argument_array(std::array< unprotected_aterm_core, N > &argument_array, const Args &... args)
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
normalizer< Function > N(const Function &f)
void print_performance_statistics(const T &unordered_set)
Prints various information for unordered_set like data structures.
void mcrl2_unused(T &&...)
Function that can be used to silence unused parameter warnings.
Definition unused.h:20
#define MCRL2_DECLARE_STACK_ARRAY(NAME, TYPE, SIZE)
Declares a stack_array<TYPE> with the specified NAME that stores SIZE elements type TYPE.
Definition stack_array.h:98
Checks whether condition holds for all types passed as variadic template.
Definition type_traits.h:41