Line data Source code
1 : // Author(s): Jan Friso Groote, 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_DETAIL_ATERM_LIST_IMPLEMENTATION_H
11 : #define MCRL2_ATERMPP_DETAIL_ATERM_LIST_IMPLEMENTATION_H
12 : #pragma once
13 :
14 : #include <type_traits>
15 : #include "mcrl2/atermpp/aterm_appl.h"
16 : #include "mcrl2/atermpp/aterm_list.h"
17 :
18 : #include "mcrl2/utilities/exception.h"
19 : #include "mcrl2/utilities/workarounds.h"
20 :
21 : namespace atermpp
22 : {
23 :
24 : constexpr std::size_t LengthOfShortList = 10000; /// \brief The length of a short list. If lists
25 : /// are short the stack can be used for temporary data.
26 : /// Otherwise the heap must be used to avoid stack overflow.
27 : /// The chosen value is rather arbitrary.
28 :
29 : template <class Term>
30 68091736 : void term_list<Term>::push_front(const Term& el)
31 : {
32 68091736 : detail::g_thread_term_pool().create_appl<Term>(*this, detail::g_term_pool().as_list(), el, *this);
33 68091736 : }
34 :
35 : template <class Term>
36 : template<typename ...Args>
37 : void term_list<Term>::emplace_front(Args&&... arguments)
38 : {
39 : detail::g_thread_term_pool().create_appl(*this, detail::g_term_pool().as_list(), Term(std::forward<Args>(arguments)...), *this);
40 : }
41 :
42 : template <typename Term>
43 : inline
44 1281315 : term_list<Term> push_back(const term_list<Term>& l, const Term& el)
45 : {
46 : typedef typename term_list<Term>::const_iterator const_iterator;
47 :
48 1281315 : const std::size_t len = l.size();
49 :
50 : // The resulting list
51 1281315 : term_list<Term> result;
52 1281315 : result.push_front(el);
53 :
54 1281315 : if (len < LengthOfShortList)
55 : {
56 : // The list is short, use the stack for temporal storage.
57 1281315 : const_iterator* buffer = MCRL2_SPECIFIC_STACK_ALLOCATOR(const_iterator, len);
58 :
59 : // Collect all elements of list in buffer.
60 1281315 : std::size_t j=0;
61 3380351 : for (const_iterator i = l.begin(); i != l.end(); ++i, ++j)
62 : {
63 2099036 : buffer[j]=i;
64 : }
65 :
66 : // Insert elements at the front of the list.
67 3380351 : while (j>0)
68 : {
69 2099036 : j=j-1;
70 2099036 : result.push_front(*buffer[j]);
71 : }
72 : }
73 : else
74 : {
75 : // The list is long. Use the heap to store intermediate data.
76 0 : std::vector<Term> buffer;
77 0 : buffer.reserve(len);
78 :
79 0 : for (const Term& t: l)
80 : {
81 0 : buffer.push_back(t);
82 : }
83 :
84 : // Insert elements at the front of the list
85 0 : for (typename std::vector<Term>::reverse_iterator i=buffer.rbegin(); i!=buffer.rend(); ++i)
86 : {
87 0 : result.push_front(*i);
88 : }
89 0 : }
90 :
91 1281315 : return result;
92 0 : }
93 :
94 : template <typename Term>
95 : inline
96 : void make_reverse(term_list<Term>& result, const term_list<Term>& l)
97 : {
98 : make_term_list<Term>(result);
99 : for(const Term& t: l)
100 : {
101 : result.push_front(t);
102 : }
103 : }
104 :
105 : template <typename Term>
106 : inline
107 1478964 : term_list<Term> reverse(const term_list<Term>& l)
108 : {
109 1478964 : if (l.size()<2)
110 : {
111 861369 : return l;
112 : }
113 617595 : term_list<Term> result;
114 3181014 : for(const Term& t: l)
115 : {
116 1945824 : result.push_front(t);
117 : }
118 617595 : return result;
119 617595 : }
120 :
121 : template <typename Term>
122 : inline
123 384 : term_list<Term> sort_list(const term_list<Term>& l,
124 : const std::function<bool(const Term&, const Term&)>& ordering
125 : /* = [](const Term& t1, const Term& t2){ return t1<t2;}*/ )
126 : {
127 384 : const std::size_t len = l.size();
128 384 : if (len<=1)
129 : {
130 160 : return l;
131 : }
132 :
133 : // The resulting list
134 224 : term_list<Term> result;
135 :
136 224 : if (len < LengthOfShortList)
137 : {
138 : // The list is short, use the stack for temporal storage.
139 224 : Term* buffer = MCRL2_SPECIFIC_STACK_ALLOCATOR(Term, len);
140 :
141 : // Collect all elements of list in buffer.
142 224 : std::size_t j=0;
143 908 : for (const Term& t: l)
144 : {
145 460 : new (buffer+j) Term(t); // A mcrl2 stack allocator does not handle construction by default.
146 460 : ++j;
147 : }
148 :
149 224 : std::sort(buffer, buffer+len, ordering);
150 :
151 : // Insert elements at the front of the list.
152 684 : while (j>0)
153 : {
154 460 : j=j-1;
155 460 : result.push_front(buffer[j]);
156 460 : buffer[j].~Term(); // Explicitly call the destructor, as an mCRL2 stack allocator does not do that itself. .
157 : }
158 : }
159 : else
160 : {
161 : // The list is long. Use the heap to store intermediate data.
162 0 : std::vector<Term> buffer;
163 0 : buffer.reserve(len);
164 :
165 0 : for (const Term& t: l)
166 : {
167 0 : buffer.push_back(t);
168 : }
169 :
170 : // Sort using a standard algorithm.
171 0 : std::sort(buffer.begin(), buffer.end(), ordering);
172 :
173 : // Insert elements at the front of the list
174 0 : for (typename std::vector<Term>::reverse_iterator i=buffer.rbegin(); i!=buffer.rend(); ++i)
175 : {
176 0 : result.push_front(*i);
177 : }
178 0 : }
179 224 : return result;
180 224 : }
181 :
182 :
183 : template <typename Term>
184 : inline
185 0 : term_list<Term> remove_one_element(const term_list<Term>& list, const Term& t)
186 : {
187 : typedef typename term_list<Term>::const_iterator const_iterator;
188 :
189 0 : std::size_t len=0;
190 0 : const_iterator i = list.begin();
191 0 : for( ; i!=list.end(); ++i, ++len)
192 : {
193 0 : if (*i==t)
194 : {
195 0 : break;
196 : }
197 : }
198 :
199 0 : if (i==list.end())
200 : {
201 : // Term t not found in list.
202 0 : return list;
203 : }
204 :
205 0 : const_iterator* buffer = MCRL2_SPECIFIC_STACK_ALLOCATOR(const_iterator, len);
206 :
207 0 : term_list<Term> result = list;
208 0 : std::size_t k=0;
209 0 : for(const_iterator j = list.begin(); j != i; ++j, ++k)
210 : {
211 0 : buffer[k]=j;
212 0 : result.pop_front();
213 : }
214 0 : assert(len==k);
215 0 : assert(result.front()==t);
216 0 : result.pop_front(); // skip the element.
217 :
218 0 : while (k>0)
219 : {
220 0 : k=k-1;
221 0 : result.push_front(*buffer[k]);
222 : }
223 :
224 0 : return result;
225 0 : }
226 :
227 :
228 : template <typename Term1, typename Term2>
229 : inline
230 : typename std::conditional<std::is_convertible<Term2,Term1>::value,term_list<Term1>,term_list<Term2>>::type
231 856699 : operator+(const term_list<Term1>& l, const term_list<Term2>& m)
232 : {
233 : static_assert(std::is_convertible< Term1, Term2 >::value ||
234 : std::is_convertible< Term2, Term1 >::value,
235 : "Concatenated lists must be of convertible types. ");
236 : static_assert(sizeof(Term1) == sizeof(aterm),
237 : "aterm cast cannot be applied types derived from aterms where extra fields are added. ");
238 : static_assert(sizeof(Term2) == sizeof(aterm),
239 : "aterm cast cannot be applied types derived from aterms where extra fields are added. ");
240 : typedef typename std::conditional<std::is_convertible<Term2,Term1>::value,Term1,Term2>::type ResultType;
241 : typedef typename term_list<Term1>::const_iterator const_iterator;
242 :
243 856699 : if (m.empty())
244 : {
245 34127 : return reinterpret_cast<const term_list<ResultType>&>(l);
246 : }
247 :
248 822572 : std::size_t len = l.size();
249 :
250 822572 : if (len == 0)
251 : {
252 451193 : return reinterpret_cast<const term_list<ResultType>&>(m);
253 : }
254 :
255 371379 : term_list<ResultType> result = reinterpret_cast<const term_list<ResultType>&>(m);
256 371379 : if (len < LengthOfShortList)
257 : {
258 : // The length is short. Use the stack for temporary storage.
259 371379 : const_iterator* buffer = MCRL2_SPECIFIC_STACK_ALLOCATOR(const_iterator, len);
260 :
261 371379 : std::size_t j=0;
262 1899745 : for (const_iterator i = l.begin(); i != l.end(); ++i, ++j)
263 : {
264 1528366 : buffer[j]=i;
265 : }
266 371379 : assert(j==len);
267 :
268 : // Insert elements at the front of the list
269 1899745 : while (j>0)
270 : {
271 1528366 : j=j-1;
272 1528366 : result.push_front(*buffer[j]);
273 : }
274 : }
275 : else
276 : {
277 : // The length of l is very long. Use the heap for temporary storage.
278 0 : std::vector<ResultType> buffer;
279 0 : buffer.reserve(len);
280 :
281 0 : for (const Term1& t: l)
282 : {
283 0 : buffer.push_back(t);
284 : }
285 :
286 : // Insert elements at the front of the list
287 0 : for(typename std::vector<ResultType>::const_reverse_iterator i=buffer.rbegin(); i!=buffer.rend(); ++i)
288 : {
289 0 : result.push_front(*i);
290 : }
291 0 : }
292 371379 : return result;
293 371379 : }
294 :
295 :
296 : namespace detail
297 : {
298 : template <class Term, class Iter, class ATermConverter, class ATermFilter>
299 1 : inline void make_list_backward(term_list<Term>& result, Iter first, Iter last, ATermConverter convert_to_aterm, ATermFilter aterm_filter)
300 : {
301 : static_assert(std::is_base_of<aterm, Term>::value,"Term must be derived from an aterm");
302 : static_assert(sizeof(Term)==sizeof(aterm),"Term derived from an aterm must not have extra fields");
303 :
304 1 : Term t;
305 6 : while (first != last)
306 : {
307 5 : --last;
308 5 : t = convert_to_aterm(*last);
309 5 : if (aterm_filter(t))
310 : {
311 3 : result.push_front(t);
312 : }
313 : }
314 1 : }
315 :
316 : template <class Term, class Iter, class ATermConverter, class ATermFilter>
317 1 : inline aterm make_list_backward(Iter first, Iter last, ATermConverter convert_to_aterm, ATermFilter aterm_filter)
318 : {
319 1 : term_list<Term> result_list;
320 1 : make_list_backward<Term, Iter, ATermConverter, ATermFilter>(result_list, first, last, convert_to_aterm, aterm_filter);
321 2 : return mcrl2::workaround::return_std_move(result_list);
322 1 : }
323 :
324 : template <class Term, class Iter, class ATermConverter>
325 26188699 : inline void make_list_backward(term_list<Term>& result, Iter first, Iter last, ATermConverter convert_to_aterm)
326 : {
327 : static_assert(std::is_base_of<aterm, Term>::value,"Term must be derived from an aterm");
328 : static_assert(sizeof(Term)==sizeof(aterm),"Term derived from an aterm must not have extra fields");
329 :
330 69256237 : while (first != last)
331 : {
332 43067538 : --last;
333 43067538 : result.push_front(convert_to_aterm(*last));
334 : }
335 26188699 : }
336 :
337 : template <class Term, class Iter, class ATermConverter>
338 26188699 : inline aterm make_list_backward(Iter first, Iter last, ATermConverter convert_to_aterm)
339 : {
340 26188699 : term_list<Term> result_list;
341 26188699 : make_list_backward<Term, Iter, ATermConverter>(result_list, first, last, convert_to_aterm);
342 52377398 : return mcrl2::workaround::return_std_move(result_list);
343 26188699 : }
344 :
345 : // See the note at make_list_backwards for why there are two almost similar version of make_list_forward.
346 : // The resulting list is put in result.
347 : template <class Term, class Iter, class ATermConverter, class ATermFilter>
348 14 : inline void make_list_forward(term_list<Term>& result, Iter first, Iter last, ATermConverter convert_to_aterm, ATermFilter aterm_filter)
349 : {
350 : static_assert(std::is_base_of<aterm, Term>::value,"Term must be derived from an aterm");
351 : static_assert(sizeof(Term)==sizeof(aterm),"Term derived from an aterm must not have extra fields");
352 :
353 :
354 14 : const std::size_t len = std::distance(first,last);
355 14 : if (len < LengthOfShortList) // If the list is sufficiently short, use the stack.
356 : {
357 14 : Term* buffer = MCRL2_SPECIFIC_STACK_ALLOCATOR(Term, len);
358 14 : Term *const buffer_begin=buffer;
359 14 : Term* i=buffer_begin;
360 17 : for(; first != last; ++first)
361 : {
362 3 : const Term t = convert_to_aterm(*first);
363 3 : if (aterm_filter(t))
364 : {
365 : // Placement new; The buffer is not properly initialised.
366 2 : new (i) Term(t);
367 2 : ++i;
368 : }
369 : }
370 :
371 : // Construct the list using the temporary array of elements.
372 16 : for( ; i != buffer_begin; )
373 : {
374 2 : --i;
375 2 : result.push_front(*i);
376 2 : (*i).~Term(); // Destroy the elements in the buffer explicitly.
377 : }
378 : }
379 : else
380 : {
381 : // The list is long. Therefore use the heap for temporary storage.
382 0 : std::vector<Term> buffer;
383 0 : buffer.reserve(len);
384 0 : for(; first != last; ++first)
385 : {
386 0 : const Term t = convert_to_aterm(*first);
387 0 : if (aterm_filter(t))
388 : {
389 : // Placement new; The buffer is not properly initialised.
390 0 : buffer.push_back(t);
391 : }
392 : }
393 :
394 : // Construct the list using the temporary array of elements.
395 0 : for(typename std::vector<Term>::const_reverse_iterator i = buffer.rbegin(); i != buffer.rend(); ++i)
396 : {
397 0 : result.push_front(*i);
398 : }
399 0 : }
400 14 : }
401 :
402 : template <class Term, class Iter, class ATermConverter, class ATermFilter>
403 14 : inline aterm make_list_forward(Iter first, Iter last, ATermConverter convert_to_aterm, ATermFilter aterm_filter)
404 : {
405 14 : term_list<Term> result_list;
406 14 : make_list_forward<Term, Iter, ATermConverter, ATermFilter>(result_list, first, last, convert_to_aterm, aterm_filter);
407 28 : return mcrl2::workaround::return_std_move(result_list);
408 14 : }
409 :
410 : template < class Term, typename ForwardTraversalIterator, class Transformer >
411 9483355 : void make_list_forward_helper(term_list<Term>& result, ForwardTraversalIterator& p, const ForwardTraversalIterator last, Transformer transformer)
412 : {
413 9483355 : assert(p!=last);
414 18966710 : make_term_appl(result,
415 9483355 : detail::g_term_pool().as_list(),
416 18966710 : [&transformer, &p](Term& result)
417 : {
418 : if constexpr (mcrl2::utilities::is_applicable2<Transformer, Term&, const Term&>::value)
419 : {
420 9458782 : transformer(reinterpret_cast<Term&>(result), *(p++));
421 : }
422 : else
423 : {
424 24573 : reinterpret_cast<Term&>(result)=transformer(*(p++));
425 : }
426 : },
427 9483355 : [&transformer, &p, last](term_list<Term>& result)
428 : {
429 9483355 : if (p==last)
430 : {
431 5110542 : make_term_list(reinterpret_cast<term_list<Term>& >(result));
432 : }
433 : else
434 : {
435 4372813 : make_list_forward_helper(reinterpret_cast<term_list<Term>& >(result), p, last, transformer);
436 : }
437 : });
438 9483355 : }
439 :
440 : template <class Term, class Iter, class ATermConverter>
441 5454056 : inline void make_list_forward(term_list<Term>& result, Iter first, Iter last, ATermConverter convert_aterm)
442 : {
443 : static_assert(std::is_base_of<aterm, Term>::value,"Term must be derived from an aterm");
444 : static_assert(sizeof(Term)==sizeof(aterm),"Term derived from an aterm must not have extra fields");
445 :
446 5454056 : const std::size_t len = std::distance(first,last);
447 5454056 : if (first==last)
448 : {
449 343514 : make_term_list(result); // Put the empty list in result.
450 343514 : return;
451 : }
452 5110542 : else if (len < LengthOfShortList) // If the list is sufficiently short, use the stack.
453 : {
454 5110542 : make_list_forward_helper(result, first, last, convert_aterm);
455 : }
456 : else
457 : {
458 : // The list is very long. Reserve memory on the heap.
459 0 : std::vector<Term> buffer;
460 0 : buffer.reserve(len);
461 0 : for(; first != last; ++first)
462 : {
463 : if constexpr (mcrl2::utilities::is_applicable2<ATermConverter, Term&, const Term>::value)
464 : {
465 0 : buffer.emplace_back();
466 0 : convert_aterm(buffer.back(), *first);
467 : }
468 : else
469 : {
470 0 : buffer.emplace_back(convert_aterm(*first));
471 : }
472 :
473 : }
474 :
475 0 : for(typename std::vector<Term>::const_reverse_iterator i = buffer.rbegin(); i != buffer.rend(); ++i)
476 : {
477 0 : result.push_front(*i);
478 : }
479 0 : }
480 : }
481 :
482 : template <class Term, class Iter, class ATermConverter>
483 2581760 : inline aterm make_list_forward(Iter first, Iter last, ATermConverter convert_to_aterm)
484 : {
485 2581760 : term_list<Term> result_list;
486 2581760 : make_list_forward<Term,Iter,ATermConverter>(result_list, first, last, convert_to_aterm);
487 5163520 : return mcrl2::workaround::return_std_move(result_list);
488 2581760 : }
489 : } // detail
490 :
491 :
492 :
493 : } // namespace atermpp
494 :
495 : #endif // MCRL2_ATERMPP_DETAIL_ATERM_LIST_IMPLEMENTATION_H
|
