Line data Source code
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 : //
9 : /// \file mcrl2/pbes/join.h
10 : /// \brief add your file description here.
11 :
12 : #ifndef MCRL2_PBES_JOIN_H
13 : #define MCRL2_PBES_JOIN_H
14 :
15 : #include "mcrl2/pbes/pbes_expression.h"
16 :
17 : namespace mcrl2 {
18 :
19 : namespace pbes_system {
20 :
21 : /// \brief Returns or applied to the sequence of pbes expressions [first, last)
22 : /// \param first Start of a sequence of pbes expressions
23 : /// \param last End of a sequence of of pbes expressions
24 : /// \return Or applied to the sequence of pbes expressions [first, last)
25 : template <typename FwdIt>
26 98 : pbes_expression join_or(FwdIt first, FwdIt last)
27 : {
28 142 : return utilities::detail::join(first, last, [](const pbes_expression& x, const pbes_expression& y) { return or_(x, y); }, false_());
29 : }
30 :
31 : /// \brief Returns and applied to the sequence of pbes expressions [first, last)
32 : /// \param first Start of a sequence of pbes expressions
33 : /// \param last End of a sequence of of pbes expressions
34 : /// \return And applied to the sequence of pbes expressions [first, last)
35 : template <typename FwdIt>
36 114 : pbes_expression join_and(FwdIt first, FwdIt last)
37 : {
38 250 : return utilities::detail::join(first, last, [](const pbes_expression& x, const pbes_expression& y) { return and_(x, y); }, true_());
39 : }
40 :
41 : /// \brief Splits a disjunction into a sequence of operands
42 : /// Given a pbes expression of the form p1 || p2 || .... || pn, this will yield a
43 : /// set of the form { p1, p2, ..., pn }, assuming that pi does not have a || as main
44 : /// function symbol.
45 : /// \param expr A PBES expression
46 : /// \param split_data_expressions if true, both data and pbes disjunctions are
47 : /// split, otherwise only pbes disjunctions are split.
48 : /// \return A sequence of operands
49 : inline
50 508 : std::set<pbes_expression> split_or(const pbes_expression& expr, bool split_data_expressions = false)
51 : {
52 : using namespace accessors;
53 508 : std::set<pbes_expression> result;
54 :
55 508 : if (split_data_expressions)
56 : {
57 0 : utilities::detail::split(expr, std::insert_iterator<std::set<pbes_expression> >(result, result.begin()), is_universal_or, data_left, data_right);
58 : }
59 : else
60 : {
61 508 : utilities::detail::split(expr, std::insert_iterator<std::set<pbes_expression> >(result, result.begin()), is_pbes_or, left, right);
62 : }
63 :
64 508 : return result;
65 0 : }
66 :
67 : /// \brief Splits a conjunction into a sequence of operands
68 : /// Given a pbes expression of the form p1 && p2 && .... && pn, this will yield a
69 : /// set of the form { p1, p2, ..., pn }, assuming that pi does not have a && as main
70 : /// function symbol.
71 : /// \param expr A PBES expression
72 : /// \param split_data_expressions if true, both data and pbes conjunctions are
73 : /// split, otherwise only pbes conjunctions are split.
74 : /// \return A sequence of operands
75 : inline
76 2408 : std::set<pbes_expression> split_and(const pbes_expression& expr, bool split_data_expressions = false)
77 : {
78 : using namespace accessors;
79 2408 : std::set<pbes_expression> result;
80 :
81 2408 : if (split_data_expressions)
82 : {
83 0 : utilities::detail::split(expr, std::insert_iterator<std::set<pbes_expression> >(result, result.begin()), is_universal_and, data_left, data_right);
84 : }
85 : else
86 : {
87 2408 : utilities::detail::split(expr, std::insert_iterator<std::set<pbes_expression> >(result, result.begin()), is_pbes_and, left, right);
88 : }
89 :
90 2408 : return result;
91 0 : }
92 :
93 : /// \brief Returns or applied to the sequence of pbes expressions [first, last)
94 : /// \param first Start of a sequence of pbes expressions
95 : /// \param last End of a sequence of pbes expressions
96 : /// \return Or applied to the sequence of pbes expressions [first, last)
97 : template <typename FwdIt>
98 1660 : inline pbes_expression optimized_join_or(FwdIt first, FwdIt last)
99 : {
100 : return utilities::detail::join(first,
101 : last,
102 2070 : [](const pbes_expression& arg0, const pbes_expression& arg1) -> pbes_expression
103 : {
104 2070 : pbes_expression result;
105 2070 : data::optimized_or(result, arg0, arg1);
106 2070 : return result;
107 0 : },
108 1660 : false_());
109 : }
110 :
111 : /// \brief Returns and applied to the sequence of pbes expressions [first, last)
112 : /// \param first Start of a sequence of pbes expressions
113 : /// \param last End of a sequence of pbes expressions
114 : /// \return And applied to the sequence of pbes expressions [first, last)
115 : template <typename FwdIt>
116 64 : inline pbes_expression optimized_join_and(FwdIt first, FwdIt last)
117 : {
118 : return utilities::detail::join(first,
119 : last,
120 224 : [](const pbes_expression& arg0, const pbes_expression& arg1) -> pbes_expression
121 : {
122 224 : pbes_expression result;
123 224 : data::optimized_and(result, arg0, arg1);
124 224 : return result;
125 0 : },
126 64 : true_());
127 : }
128 :
129 : } // namespace pbes_system
130 :
131 : } // namespace mcrl2
132 :
133 : #endif // MCRL2_PBES_JOIN_H
|
