mCRL2
Loading...
Searching...
No Matches
aterm_list_implementation.h
Go to the documentation of this file.
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.h"
17
20
21namespace atermpp
22{
23
24constexpr std::size_t LengthOfShortList = 10000;
28
29template <class Term>
30void term_list<Term>::push_front(const Term& el)
31{
33}
34
35template <class Term>
36template<typename ...Args>
37void 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
42template <typename Term>
43inline
44term_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 const std::size_t len = l.size();
49
50 // The resulting list
51 term_list<Term> result;
52 result.push_front(el);
53
54 if (len < LengthOfShortList)
55 {
56 // The list is short, use the stack for temporal storage.
57 const_iterator* buffer = MCRL2_SPECIFIC_STACK_ALLOCATOR(const_iterator, len);
58
59 // Collect all elements of list in buffer.
60 std::size_t j=0;
61 for (const_iterator i = l.begin(); i != l.end(); ++i, ++j)
62 {
63 buffer[j]=i;
64 }
65
66 // Insert elements at the front of the list.
67 while (j>0)
68 {
69 j=j-1;
70 result.push_front(*buffer[j]);
71 }
72 }
73 else
74 {
75 // The list is long. Use the heap to store intermediate data.
76 std::vector<Term> buffer;
77 buffer.reserve(len);
78
79 for (const Term& t: l)
80 {
81 buffer.push_back(t);
82 }
83
84 // Insert elements at the front of the list
85 for (typename std::vector<Term>::reverse_iterator i=buffer.rbegin(); i!=buffer.rend(); ++i)
86 {
87 result.push_front(*i);
88 }
89 }
90
91 return result;
92}
93
94template <typename Term>
95inline
97{
98 make_term_list<Term>(result);
99 for(const Term& t: l)
100 {
101 result.push_front(t);
102 }
103}
104
105template <typename Term>
106inline
108{
109 if (l.size()<2)
110 {
111 return l;
112 }
113 term_list<Term> result;
114 for(const Term& t: l)
115 {
116 result.push_front(t);
117 }
118 return result;
119}
120
121template <typename Term>
122inline
124 const std::function<bool(const Term&, const Term&)>& ordering
125 /* = [](const Term& t1, const Term& t2){ return t1<t2;}*/ )
126{
127 const std::size_t len = l.size();
128 if (len<=1)
129 {
130 return l;
131 }
132
133 // The resulting list
134 term_list<Term> result;
135
136 if (len < LengthOfShortList)
137 {
138 // The list is short, use the stack for temporal storage.
139 Term* buffer = MCRL2_SPECIFIC_STACK_ALLOCATOR(Term, len);
140
141 // Collect all elements of list in buffer.
142 std::size_t j=0;
143 for (const Term& t: l)
144 {
145 new (buffer+j) Term(t); // A mcrl2 stack allocator does not handle construction by default.
146 ++j;
147 }
148
149 std::sort(buffer, buffer+len, ordering);
150
151 // Insert elements at the front of the list.
152 while (j>0)
153 {
154 j=j-1;
155 result.push_front(buffer[j]);
156 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 std::vector<Term> buffer;
163 buffer.reserve(len);
164
165 for (const Term& t: l)
166 {
167 buffer.push_back(t);
168 }
169
170 // Sort using a standard algorithm.
171 std::sort(buffer.begin(), buffer.end(), ordering);
172
173 // Insert elements at the front of the list
174 for (typename std::vector<Term>::reverse_iterator i=buffer.rbegin(); i!=buffer.rend(); ++i)
175 {
176 result.push_front(*i);
177 }
178 }
179 return result;
180}
181
182
183template <typename Term>
184inline
186{
187 typedef typename term_list<Term>::const_iterator const_iterator;
188
189 std::size_t len=0;
190 const_iterator i = list.begin();
191 for( ; i!=list.end(); ++i, ++len)
192 {
193 if (*i==t)
194 {
195 break;
196 }
197 }
198
199 if (i==list.end())
200 {
201 // Term t not found in list.
202 return list;
203 }
204
205 const_iterator* buffer = MCRL2_SPECIFIC_STACK_ALLOCATOR(const_iterator, len);
206
207 term_list<Term> result = list;
208 std::size_t k=0;
209 for(const_iterator j = list.begin(); j != i; ++j, ++k)
210 {
211 buffer[k]=j;
212 result.pop_front();
213 }
214 assert(len==k);
215 assert(result.front()==t);
216 result.pop_front(); // skip the element.
217
218 while (k>0)
219 {
220 k=k-1;
221 result.push_front(*buffer[k]);
222 }
223
224 return result;
225}
226
227
228template <typename Term1, typename Term2>
229inline
230typename std::conditional<std::is_convertible<Term2,Term1>::value,term_list<Term1>,term_list<Term2>>::type
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 if (m.empty())
244 {
245 return reinterpret_cast<const term_list<ResultType>&>(l);
247
248 std::size_t len = l.size();
249
250 if (len == 0)
252 return reinterpret_cast<const term_list<ResultType>&>(m);
253 }
254
255 term_list<ResultType> result = reinterpret_cast<const term_list<ResultType>&>(m);
256 if (len < LengthOfShortList)
257 {
258 // The length is short. Use the stack for temporary storage.
259 const_iterator* buffer = MCRL2_SPECIFIC_STACK_ALLOCATOR(const_iterator, len);
260
261 std::size_t j=0;
262 for (const_iterator i = l.begin(); i != l.end(); ++i, ++j)
263 {
264 buffer[j]=i;
265 }
266 assert(j==len);
267
268 // Insert elements at the front of the list
269 while (j>0)
270 {
271 j=j-1;
272 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 std::vector<ResultType> buffer;
279 buffer.reserve(len);
280
281 for (const Term1& t: l)
282 {
283 buffer.push_back(t);
284 }
285
286 // Insert elements at the front of the list
287 for(typename std::vector<ResultType>::const_reverse_iterator i=buffer.rbegin(); i!=buffer.rend(); ++i)
288 {
289 result.push_front(*i);
290 }
291 }
292 return result;
293}
294
295
296namespace detail
297{
298 template <class Term, class Iter, class ATermConverter, class ATermFilter>
299 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 Term t;
305 while (first != last)
306 {
307 --last;
308 t = convert_to_aterm(*last);
309 if (aterm_filter(t))
310 {
311 result.push_front(t);
312 }
313 }
314 }
315
316 template <class Term, class Iter, class ATermConverter, class ATermFilter>
317 inline aterm make_list_backward(Iter first, Iter last, ATermConverter convert_to_aterm, ATermFilter aterm_filter)
318 {
319 term_list<Term> result_list;
320 make_list_backward<Term, Iter, ATermConverter, ATermFilter>(result_list, first, last, convert_to_aterm, aterm_filter);
321 return mcrl2::workaround::return_std_move(result_list);
322 }
323
324 template <class Term, class Iter, class ATermConverter>
325 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 while (first != last)
331 {
332 --last;
333 result.push_front(convert_to_aterm(*last));
334 }
335 }
336
337 template <class Term, class Iter, class ATermConverter>
338 inline aterm make_list_backward(Iter first, Iter last, ATermConverter convert_to_aterm)
339 {
340 term_list<Term> result_list;
341 make_list_backward<Term, Iter, ATermConverter>(result_list, first, last, convert_to_aterm);
342 return mcrl2::workaround::return_std_move(result_list);
343 }
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 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 const std::size_t len = std::distance(first,last);
355 if (len < LengthOfShortList) // If the list is sufficiently short, use the stack.
356 {
357 Term* buffer = MCRL2_SPECIFIC_STACK_ALLOCATOR(Term, len);
358 Term *const buffer_begin=buffer;
359 Term* i=buffer_begin;
360 for(; first != last; ++first)
361 {
362 const Term t = convert_to_aterm(*first);
363 if (aterm_filter(t))
364 {
365 // Placement new; The buffer is not properly initialised.
366 new (i) Term(t);
367 ++i;
368 }
369 }
370
371 // Construct the list using the temporary array of elements.
372 for( ; i != buffer_begin; )
373 {
374 --i;
375 result.push_front(*i);
376 (*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 std::vector<Term> buffer;
383 buffer.reserve(len);
384 for(; first != last; ++first)
385 {
386 const Term t = convert_to_aterm(*first);
387 if (aterm_filter(t))
388 {
389 // Placement new; The buffer is not properly initialised.
390 buffer.push_back(t);
391 }
392 }
393
394 // Construct the list using the temporary array of elements.
395 for(typename std::vector<Term>::const_reverse_iterator i = buffer.rbegin(); i != buffer.rend(); ++i)
396 {
397 result.push_front(*i);
398 }
399 }
400 }
401
402 template <class Term, class Iter, class ATermConverter, class ATermFilter>
403 inline aterm make_list_forward(Iter first, Iter last, ATermConverter convert_to_aterm, ATermFilter aterm_filter)
404 {
405 term_list<Term> result_list;
406 make_list_forward<Term, Iter, ATermConverter, ATermFilter>(result_list, first, last, convert_to_aterm, aterm_filter);
407 return mcrl2::workaround::return_std_move(result_list);
408 }
409
410 template < class Term, typename ForwardTraversalIterator, class Transformer >
411 void make_list_forward_helper(term_list<Term>& result, ForwardTraversalIterator& p, const ForwardTraversalIterator last, Transformer transformer)
412 {
413 assert(p!=last);
414 make_term_appl(result,
415 detail::g_term_pool().as_list(),
416 [&transformer, &p](Term& result)
417 {
419 {
420 transformer(reinterpret_cast<Term&>(result), *(p++));
421 }
422 else
423 {
424 reinterpret_cast<Term&>(result)=transformer(*(p++));
425 }
426 },
427 [&transformer, &p, last](term_list<Term>& result)
428 {
429 if (p==last)
430 {
431 make_term_list(reinterpret_cast<term_list<Term>& >(result));
432 }
433 else
434 {
435 make_list_forward_helper(reinterpret_cast<term_list<Term>& >(result), p, last, transformer);
436 }
437 });
438 }
439
440 template <class Term, class Iter, class ATermConverter>
441 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 const std::size_t len = std::distance(first,last);
447 if (first==last)
448 {
449 make_term_list(result); // Put the empty list in result.
450 return;
451 }
452 else if (len < LengthOfShortList) // If the list is sufficiently short, use the stack.
453 {
454 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 std::vector<Term> buffer;
460 buffer.reserve(len);
461 for(; first != last; ++first)
462 {
464 {
465 buffer.emplace_back();
466 convert_aterm(buffer.back(), *first);
467 }
468 else
469 {
470 buffer.emplace_back(convert_aterm(*first));
471 }
472
473 }
474
475 for(typename std::vector<Term>::const_reverse_iterator i = buffer.rbegin(); i != buffer.rend(); ++i)
476 {
477 result.push_front(*i);
478 }
479 }
480 }
481
482 template <class Term, class Iter, class ATermConverter>
483 inline aterm make_list_forward(Iter first, Iter last, ATermConverter convert_to_aterm)
484 {
485 term_list<Term> result_list;
486 make_list_forward<Term,Iter,ATermConverter>(result_list, first, last, convert_to_aterm);
487 return mcrl2::workaround::return_std_move(result_list);
488 }
489} // detail
490
491
492
493} // namespace atermpp
494
495#endif // MCRL2_ATERMPP_DETAIL_ATERM_LIST_IMPLEMENTATION_H
The term_appl class represents function application.
const_iterator end() const
Returns a const_iterator pointing past the last argument.
Definition aterm.h:172
const_iterator begin() const
Returns an iterator pointing to the first argument.
Definition aterm.h:165
const function_symbol & as_list() noexcept
Definition aterm_pool.h:121
void create_appl(aterm &term, const function_symbol &sym, const Terms &... arguments)
Iterator for term_list.
A list of aterm objects.
Definition aterm_list.h:24
size_type size() const
Returns the size of the term_list.
Definition aterm_list.h:256
const_iterator end() const
Returns a const_iterator pointing to the end of the term_list.
Definition aterm_list.h:282
const Term & front() const
Returns the first element of the list.
Definition aterm_list.h:239
void pop_front()
Removes the first element of the list.
Definition aterm_list.h:232
const_iterator begin() const
Returns a const_iterator pointing to the beginning of the term_list.
Definition aterm_list.h:275
void emplace_front(Args &&... arguments)
Construct and insert a new element at the beginning of the current list.
bool empty() const
Returns true if the list's size is 0.
Definition aterm_list.h:268
void push_front(const Term &el)
Inserts a new element at the beginning of the current list.
Exception classes for use in libraries and tools.
aterm_pool & g_term_pool()
obtain a reference to the global aterm pool.
aterm 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 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.
thread_aterm_pool & g_thread_term_pool()
A reference to the thread local term pool storage.
void make_list_forward_helper(term_list< Term > &result, ForwardTraversalIterator &p, const ForwardTraversalIterator last, Transformer transformer)
The main namespace for the aterm++ library.
Definition algorithm.h:21
term_list< Term > remove_one_element(const term_list< Term > &list, const Term &t)
void make_term_list(term_list< Term > &target)
Make an empty list and put it in target;.
Definition aterm_list.h:314
term_list< Term > sort_list(const term_list< Term > &l, const std::function< bool(const Term &, const Term &)> &ordering=[](const Term &t1, const Term &t2){ return t1< t2;})
Returns the list with the elements sorted according to the <-operator on the addresses of terms.
term_list< Term > reverse(const term_list< Term > &l)
Returns the list with the elements in reversed order.
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...
Definition aterm.h:213
constexpr std::size_t LengthOfShortList
std::conditional< std::is_convertible< Term2, Term1 >::value, term_list< Term1 >, term_list< Term2 > >::type operator+(const term_list< Term1 > &l, const term_list< Term2 > &m)
Returns the concatenation of two lists with convertible element types.
void make_reverse(term_list< Term > &result, const term_list< Term > &l)
term_list< Term > push_back(const term_list< Term > &l, const Term &el)
Appends a new element at the end of the list. Note that the complexity of this function is O(n),...
T && return_std_move(T &t)
This is a workaround for the return by value diagnostic (clang -Wreturn-std-move)....
Definition workarounds.h:24