Line data Source code
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 :
13 : #include "mcrl2/atermpp/detail/aterm_hash.h"
14 : #include "mcrl2/utilities/cache_metric.h"
15 : #include "mcrl2/utilities/unordered_set.h"
16 :
17 : #include <stack>
18 : #include <utility>
19 :
20 : namespace atermpp
21 : {
22 : namespace detail
23 : {
24 :
25 : // Forward declaration
26 : class aterm_pool;
27 :
28 : /// \brief Marks a term and recursively all arguments that are not reachable.
29 : inline void mark_term(const _aterm& root, std::stack<std::reference_wrapper<_aterm>>& todo);
30 :
31 : /// \brief This class provides for all types of term storage. It also
32 : /// provides garbage collection via its mark and sweep functions.
33 : /// \details Internally a hash set is used to ensure that the created terms are unique.
34 : template<typename Element,
35 : typename Hash = aterm_hasher<>,
36 : typename Equals = aterm_equals<>,
37 : std::size_t N = DynamicNumberOfArguments>
38 : class aterm_pool_storage : private mcrl2::utilities::noncopyable
39 : {
40 : public:
41 : using unordered_set = mcrl2::utilities::unordered_set<
42 : Element,
43 : Hash,
44 : Equals,
45 : typename std::conditional_t<N == DynamicNumberOfArguments,
46 : atermpp::detail::_aterm_appl_allocator<>,
47 : typename std::conditional_t<EnableBlockAllocator,
48 : mcrl2::utilities::block_allocator<Element, 1024, mcrl2::utilities::detail::GlobalThreadSafe>,
49 : std::allocator<Element>>
50 : >,
51 : mcrl2::utilities::detail::GlobalThreadSafe,
52 : false>;
53 : using iterator = typename unordered_set::iterator;
54 : using const_iterator = typename unordered_set::const_iterator;
55 :
56 : /// \brief The local pool is a friend class so it can mark terms.
57 : friend class aterm_pool;
58 :
59 : aterm_pool_storage(aterm_pool& pool);
60 :
61 : /// \brief Add a callback that is triggered whenever a term with the given function symbol is destroyed.
62 : void add_deletion_hook(function_symbol sym, term_callback callback);
63 :
64 11 : /// \returns The total number of terms that can be stored without resizing.
65 1942 : std::size_t capacity() const noexcept { return m_term_set.capacity(); }
66 :
67 : /// \brief Creates a integral term with the given value.
68 : bool create_int(aterm& term, std::size_t value);
69 :
70 : /// \brief Creates a term with the given function symbol.
71 : bool create_term(aterm& term, const function_symbol& sym);
72 :
73 : /// \brief Creates a function application with the given function symbol and arguments.
74 : template<class ...Terms>
75 : bool create_appl(aterm& term, const function_symbol& sym, const Terms&... arguments);
76 :
77 : /// \brief Creates a function application with the given function symbol and the arguments
78 : /// as provided by the given iterator. This function assumes that the arity of the
79 : /// function symbol is equal to N and that the iterator has exactly N elements.
80 : template<typename ForwardIterator>
81 : bool create_appl_iterator(aterm& term,
82 : const function_symbol& sym,
83 : ForwardIterator begin,
84 : ForwardIterator end);
85 :
86 : /// \brief Creates a function application with the given function symbol and the arguments
87 : /// as provided by the given iterator. This function assumes that the arity of the
88 : /// function symbol is equal to N and that the iterator has exactly N elements.
89 : template<typename InputIterator,
90 : typename TermConverter>
91 : bool create_appl_iterator(aterm& term,
92 : const function_symbol& sym,
93 : TermConverter converter,
94 : InputIterator begin,
95 : InputIterator end);
96 :
97 : /// \brief Creates a function application with the given function symbol and the arguments
98 : /// as provided by the given iterator.
99 : template<typename ForwardIterator>
100 : bool create_appl_dynamic(aterm& term,
101 : const function_symbol& sym,
102 : ForwardIterator begin,
103 : ForwardIterator end);
104 :
105 : /// \brief Creates a function application with the given function symbol and the arguments
106 : /// as provided by the given iterator, but the converter is applied to each argument.
107 : template<typename InputIterator,
108 : typename TermConverter,
109 : typename std::enable_if<!std::is_convertible<
110 : typename std::invoke_result<TermConverter, typename InputIterator::value_type>::type,
111 : aterm>::value, void>::type* = nullptr>
112 : bool create_appl_dynamic(aterm& term,
113 : const function_symbol& sym,
114 : TermConverter converter,
115 : InputIterator begin,
116 : InputIterator end);
117 :
118 : /// \brief Creates a function application with the given function symbol and the arguments
119 : /// as provided by the given iterator, but the converter is applied to each argument.
120 : template<typename InputIterator,
121 : typename TermConverter,
122 : typename std::enable_if<std::is_convertible<
123 : typename std::invoke_result<TermConverter, typename InputIterator::value_type>::type,
124 : aterm>::value, void>::type* = nullptr>
125 : bool create_appl_dynamic(aterm& term,
126 : const function_symbol& sym,
127 : TermConverter converter,
128 : InputIterator begin,
129 : InputIterator end);
130 :
131 : /// \brief Creates a function application with the given function symbol and the arguments
132 : /// as provided by the given iterator, but the converter is applied to each argument.
133 : template<typename InputIterator,
134 : typename TermConverter,
135 : typename std::enable_if<std::is_same<
136 : typename std::invoke_result<TermConverter,
137 : typename InputIterator::value_type&,
138 : typename InputIterator::value_type>::type,
139 : void>::value, void>::type* = nullptr>
140 : bool create_appl_dynamic(aterm& term,
141 : const function_symbol& sym,
142 : TermConverter converter,
143 : InputIterator begin,
144 : InputIterator end);
145 :
146 :
147 : /// \brief Prints various performance statistics for this storage.
148 : /// \param identifier A string to identify the printed message for this storage.
149 : void print_performance_stats(const char* identifier) const;
150 :
151 : /// \brief sweep Destroys all terms that are not reachable. Requires that
152 : /// mark() was called first.
153 : void sweep();
154 :
155 : /// \brief Resizes the hash table if necessary.
156 : void resize_if_needed();
157 :
158 0 : /// \returns The number of terms stored in this storage.
159 20300 : std::size_t size() const { return m_term_set.size(); }
160 :
161 : /// \brief A fake copy constructor to fix the issues with GCC 4 and 5.
162 : aterm_pool_storage(const aterm_pool_storage& other) :
163 : m_pool(other.m_pool),
164 : m_term_set(std::move(other.m_term_set))
165 : {}
166 :
167 : /// \brief Check that all arguments of a term application are marked properly.
168 : bool verify_mark();
169 :
170 : /// \brief Check that all arguments of a term application are marked properly.
171 : bool verify_sweep();
172 :
173 : private:
174 : using callback_pair = std::pair<function_symbol, term_callback>;
175 :
176 : /// \brief Calls the deletion hook attached to the function symbol of this term.
177 : /// \threadsafe
178 : void call_deletion_hook(unprotected_aterm term);
179 :
180 : /// \brief Removes an element from the unordered set and deallocates it.
181 : iterator destroy(iterator it);
182 :
183 : /// \brief Inserts a term constructed by the given arguments, checks for existing term.
184 : template<typename ...Args>
185 : bool emplace(aterm& term, Args&&... args);
186 :
187 : /// \returns True if and only if this term storage can store term applications with a dynamic
188 : /// number of arguments.
189 : constexpr bool is_dynamic_storage() const;
190 :
191 : /// \brief Verify that the given term was constructed properly.
192 : template<std::size_t Arity = N>
193 : bool verify_term(const _aterm& term);
194 :
195 : /// The pool that this storage belongs to.
196 : aterm_pool& m_pool;
197 :
198 : /// This is the set of term pointers to keep the terms unique.
199 : unordered_set m_term_set;
200 :
201 : /// This array stores creation, resp deletion, hooks for function symbols.
202 : // std::vector<callback_pair> m_creation_hooks; Not needed anymore.
203 : std::vector<callback_pair> m_deletion_hooks;
204 :
205 : /// A reusable todo stack.
206 : std::stack<std::reference_wrapper<_aterm>> todo;
207 :
208 : // Various performance statistics.
209 :
210 : mcrl2::utilities::cache_metric m_term_metric; ///< Count the number of times a term has been found in or is added to the set.
211 : std::size_t m_erasedBlocks = 0; /// The number of blocks that have been erased in the block allocator.
212 : };
213 :
214 : } // namespace detail
215 : } // namespace atermpp
216 :
217 :
218 : #endif // ATERMPP_DETAIL_ATERM_POOL_STORAGE_H
|
