mCRL2
Loading...
Searching...
No Matches
standard_container_utility.h
Go to the documentation of this file.
1// Author(s): Jeroen van der Wulp
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//
11
12#ifndef MCRL2_DATA_STANDARD_CONTAINER_UTILITY_H
13#define MCRL2_DATA_STANDARD_CONTAINER_UTILITY_H
14
16
17#include "mcrl2/data/bag.h"
18#include "mcrl2/data/list.h"
19
20namespace mcrl2
21{
22
23namespace data
24{
25
26namespace sort_list
27{
29//
34template < typename Sequence >
35inline
37 Sequence const& range,
39{
40 data_expression list_expression(empty(s));
41 std::vector< data_expression > elements(range.begin(), range.end());
42
43 for (std::vector< data_expression >::reverse_iterator i = elements.rbegin(); i != elements.rend(); ++i)
44 {
45 list_expression = sort_list::cons_(s, *i, list_expression);
46 }
47
48 return static_cast< application >(list_expression);
49}
50
53inline
55{
58}
59
63inline
65{
67 return list_enumeration;
68}
69
73inline
75{
76 if (is_function_symbol(e))
77 {
79 }
80 return false;
81}
82
90template <typename Sequence>
91inline
93 Sequence const& range,
95{
96 if (range.empty())
97 {
98 return list_enumeration(s);
99 }
100 else
101 {
102 sort_expression_vector v(range.size(), range.begin()->sort());
103
104 return application(list_enumeration(function_sort(v,s)), range);
105 }
106}
107
112inline
114{
115 if (range.empty())
116 {
117 return list_enumeration(s);
118 }
119 else
120 {
121 sort_expression_vector v(range.size(), range.begin()->sort());
122
123 return application(list_enumeration(function_sort(v,s)), range);
124 }
125}
126
131inline
133{
134 if (is_application(e))
135 {
137 }
138 return false;
139}
140} // namespace sort_list
141
142namespace sort_set
143{
146inline
148{
151}
152
156inline
158{
160 return set_enumeration;
161}
162
166inline
168{
169 if (is_function_symbol(e))
170 {
172 }
173 return false;
174}
175
183template <typename Sequence>
184inline
186 Sequence const& range,
188{
189 if (range.empty())
190 {
192 }
193 else
194 {
195 sort_expression_vector v(range.size(), range.begin()->sort());
196
198 }
199}
200
205inline
207 data_expression_list const& range)
208{
209 if (range.empty())
210 {
212 }
213 else
214 {
215 sort_expression_vector v(range.size(), range.begin()->sort());
216
218 }
219}
220
225inline
227{
228 if (is_application(e))
229 {
231 }
232 return false;
233}
234} // namespace sort_set
235
236namespace sort_fset
237{
238
240//
245template < typename Sequence >
246inline
248 Sequence const& range,
250{
251 data_expression fset_expression(sort_fset::empty(s));
252
253 // We process the elements in reverse order to have a resulting enumeration
254 // in the same order as the input
255 for (typename Sequence::const_reverse_iterator i = range.rbegin(); i != range.rend(); ++i)
256 {
257 fset_expression = sort_fset::insert(s, *i, fset_expression);
258 }
259
260 return static_cast< application >(fset_expression);
261}
262
264//
267inline
269 const data_expression_list& range)
270{
271 return fset(s, data_expression_vector(range.begin(),range.end()));
272}
273
274} // namespace sort_fset
275
276namespace sort_bag
277{
280inline
282{
285}
286
290inline
292{
294 return bag_enumeration;
295}
296
300inline
302{
303 if (is_function_symbol(e))
304 {
306 }
307 return false;
308}
309
317template <typename Sequence>
318inline
320 Sequence const& range,
322{
323 if (range.empty())
324 {
326 }
327 else
328 {
329 assert(range.size() % 2 == 0);
330 sort_expression t(range.begin()->sort());
331
333
334 for (std::size_t i = 0; i < range.size() / 2; ++i)
335 {
336 v.push_back(t);
337 v.push_back(sort_nat::nat());
338 }
339
341 }
342}
343
348inline
350 data_expression_list const& range)
351{
352 if (range.empty())
353 {
355 }
356 else
357 {
358 assert(range.size() % 2 == 0);
359 sort_expression t(range.begin()->sort());
361
362 for (std::size_t i = 0; i < range.size() / 2; ++i)
363 {
364 v.push_back(t);
365 v.push_back(sort_nat::nat());
366 }
367
369 }
370}
371
376inline
378{
379 if (is_application(e))
380 {
382 }
383 return false;
384}
385
386} // namespace sort_bag
387
388namespace sort_fbag
389{
396template < typename Sequence >
397inline
398application fbag(const sort_expression& s, Sequence const& range,
400{
401 data_expression fbag_expression(sort_fbag::empty(s));
402
403 // The sequence contains element, count, ...
404 // As we process the list in reverse, we have count, element, ...
405 // We process the elements in reverse order to have a resulting enumeration
406 // in the same order as the input
407 for (typename Sequence::const_reverse_iterator i = range.rbegin(); i != range.rend(); ++i, ++i)
408 {
409 fbag_expression = sort_fbag::cinsert(s, *std::next(i, 1), *i, fbag_expression);
410 }
411
412 return static_cast< application >(fbag_expression);
413}
414
419inline
421{
422 return fbag(s, data_expression_vector(range.begin(),range.end()));
423}
424} // namespace sort_fbag
425
426} // namespace data
427
428} // namespace mcrl2
429
430#endif
431
The standard sort bag.
Term containing a string.
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_iterator begin() const
Returns a const_iterator pointing to the beginning of the term_list.
Definition aterm_list.h:275
bool empty() const
Returns true if the list's size is 0.
Definition aterm_list.h:268
An application of a data expression to a number of arguments.
\brief A function sort
\brief A function symbol
const core::identifier_string & name() const
\brief A sort expression
The standard sort list.
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.
atermpp::aterm_string identifier_string
String type of the LPS library. Identifier strings are represented internally as ATerms.
bool is_bag_enumeration_application(const atermpp::aterm &e)
Recogniser for application of bag_enumeration.
core::identifier_string const & bag_enumeration_name()
Generate identifier bag_enumeration.
function_symbol bag_enumeration(const sort_expression &s)
Constructor for function symbol bag_enumeration.
bool is_bag_enumeration_function_symbol(const atermpp::aterm &e)
Recogniser for function bag_enumeration.
container_sort fbag(const sort_expression &s)
Constructor for sort expression FBag(S)
Definition fbag1.h:43
function_symbol empty(const sort_expression &s)
Constructor for function symbol {:}.
Definition fbag1.h:77
function_symbol cinsert(const sort_expression &s)
Constructor for function symbol @fbag_cinsert.
Definition fbag1.h:277
function_symbol insert(const sort_expression &s)
Constructor for function symbol @fset_insert.
Definition fset1.h:107
function_symbol empty(const sort_expression &s)
Constructor for function symbol {}.
Definition fset1.h:75
container_sort fset(const sort_expression &s)
Constructor for sort expression FSet(S)
Definition fset1.h:41
bool is_list_enumeration_application(const atermpp::aterm &e)
Recogniser for application of list_enumeration.
function_symbol empty(const sort_expression &s)
Constructor for function symbol [].
Definition list1.h:76
function_symbol head(const sort_expression &s)
Constructor for function symbol head.
Definition list1.h:526
function_symbol list_enumeration(const sort_expression &s)
Constructor for function symbol list_enumeration.
container_sort list(const sort_expression &s)
Constructor for sort expression List(S)
Definition list1.h:42
core::identifier_string const & list_enumeration_name()
Generate identifier list_enumeration.
function_symbol cons_(const sort_expression &s)
Constructor for function symbol |>.
Definition list1.h:108
bool is_list_enumeration_function_symbol(const atermpp::aterm &e)
Recogniser for function list_enumeration.
const basic_sort & nat()
Constructor for sort expression Nat.
Definition nat1.h:46
core::identifier_string const & set_enumeration_name()
Generate identifier set_enumeration.
function_symbol set_enumeration(const sort_expression &s)
Constructor for function symbol set_enumeration.
bool is_set_enumeration_application(const atermpp::aterm &e)
Recogniser for application of set_enumeration.
bool is_set_enumeration_function_symbol(const atermpp::aterm &e)
Recogniser for function set_enumeration.
std::vector< sort_expression > sort_expression_vector
\brief vector of sort_expressions
std::vector< data_expression > data_expression_vector
\brief vector of data_expressions
bool is_function_symbol(const atermpp::aterm &x)
Returns true if the term t is a function symbol.
bool is_application(const atermpp::aterm &x)
Returns true if the term t is an application.
A class that takes a linear process specification and checks all tau-summands of that LPS for conflue...
Definition indexed_set.h:72
Generic join and split functions.