mCRL2
Loading...
Searching...
No Matches
data_sequence_algorithm.h
Go to the documentation of this file.
1// Author(s): Wieger Wesselink
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_DETAIL_DATA_SEQUENCE_ALGORITHM_H
13#define MCRL2_DATA_DETAIL_DATA_SEQUENCE_ALGORITHM_H
14
15#include "mcrl2/data/variable.h"
16
17namespace mcrl2
18{
19
20namespace data
21{
22
23namespace detail
24{
25
30inline
32{
33 if (x == y)
34 {
35 return x;
36 }
37
38 std::vector<variable> result;
39 for (const variable& v: x)
40 {
41 if (std::find(y.begin(), y.end(), v) != y.end())
42 {
43 result.push_back(v);
44 }
45 }
46 return variable_list(result.begin(), result.end());
47}
48
53inline
55{
56 if (x == y)
57 {
58 return variable_list();
59 }
60
61 std::vector<variable> result;
62 for (const variable& v: x)
63 {
64 if (std::find(y.begin(), y.end(), v) == y.end())
65 {
66 result.push_back(v);
67 }
68 }
69 return variable_list(result.begin(), result.end());
70}
71
72} // namespace detail
73
74} // namespace data
75
76} // namespace mcrl2
77
78#endif // MCRL2_DATA_DETAIL_DATA_SEQUENCE_ALGORITHM_H
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
\brief A data variable
Definition variable.h:28
variable_list set_intersection(const variable_list &x, const variable_list &y)
Returns the intersection of two unordered sets, that are stored in ATerm lists.
variable_list set_difference(const variable_list &x, const variable_list &y)
Returns the difference of two unordered sets, that are stored in aterm lists.
atermpp::term_list< variable > variable_list
\brief list of variables
A class that takes a linear process specification and checks all tau-summands of that LPS for conflue...
Definition indexed_set.h:72
The class variable.