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/data/detail/test_rewriters.h
10 : /// \brief Functions for testing a rewriter
11 :
12 : #ifndef MCRL2_DATA_DETAIL_TEST_REWRITERS_H
13 : #define MCRL2_DATA_DETAIL_TEST_REWRITERS_H
14 :
15 : #include "mcrl2/data/builder.h"
16 : #include "mcrl2/data/detail/print_utility.h"
17 : #include "mcrl2/data/join.h"
18 : #include "mcrl2/data/optimized_boolean_operators.h"
19 : #include "mcrl2/data/parse.h"
20 : #include "mcrl2/utilities/detail/test_operation.h"
21 :
22 : namespace mcrl2 {
23 :
24 : namespace data {
25 :
26 : namespace detail {
27 :
28 : // Normalizes conjunctions and disjunctions.
29 : template <typename Derived>
30 : struct normalize_and_or_builder: public data_expression_builder<Derived>
31 : {
32 : typedef data_expression_builder<Derived> super;
33 : using super::enter;
34 : using super::leave;
35 : using super::update;
36 : using super::apply;
37 :
38 : /// \brief Splits a disjunction into a sequence of operands
39 : /// Given a data expression of the form p1 || p2 || .... || pn, this will yield a
40 : /// set of the form { p1, p2, ..., pn }, assuming that pi does not have a || as main
41 : /// function symbol.
42 : /// \param expr A data expression
43 : /// \return A sequence of operands
44 10 : std::multiset<data_expression> split_or(const data_expression& expr)
45 : {
46 10 : std::multiset<data_expression> result;
47 10 : utilities::detail::split(expr, std::insert_iterator<std::multiset<data_expression> >(result, result.begin()), sort_bool::is_or_application, data::binary_left1, data::binary_right1);
48 10 : return result;
49 0 : }
50 :
51 : /// \brief Splits a conjunction into a sequence of operands
52 : /// Given a data expression of the form p1 && p2 && .... && pn, this will yield a
53 : /// set of the form { p1, p2, ..., pn }, assuming that pi does not have a && as main
54 : /// function symbol.
55 : /// \param expr A data expression
56 : /// \return A sequence of operands
57 12 : std::multiset<data_expression> split_and(const data_expression& expr)
58 : {
59 12 : std::multiset<data_expression> result;
60 12 : utilities::detail::split(expr, std::insert_iterator<std::multiset<data_expression> >(result, result.begin()), sort_bool::is_and_application, data::binary_left1, data::binary_right1);
61 12 : return result;
62 0 : }
63 :
64 : template<class T>
65 66 : void apply(T& result, const application& x)
66 : {
67 66 : data_expression y;
68 66 : super::apply(y, x);
69 66 : if (sort_bool::is_and_application(y))
70 : {
71 12 : std::multiset<data_expression> s = split_and(y);
72 12 : result = data::join_and(s.begin(), s.end());
73 12 : return;
74 12 : }
75 54 : else if (sort_bool::is_or_application(y))
76 : {
77 10 : std::multiset<data_expression> s = split_or(y);
78 10 : result = data::join_or(s.begin(), s.end());
79 10 : return;
80 10 : }
81 44 : result = y;
82 66 : }
83 : };
84 :
85 : template <typename T>
86 28 : T normalize_and_or(const T& x,
87 : typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value>::type* = nullptr
88 : )
89 : {
90 28 : T result;
91 28 : core::make_apply_builder<normalize_and_or_builder>().apply(result, x);
92 28 : return result;
93 0 : }
94 :
95 : template <typename T>
96 : void normalize_and_or(T& x,
97 : typename std::enable_if< !std::is_base_of< atermpp::aterm, T >::value>::type* = 0
98 : )
99 : {
100 : core::make_apply_builder<normalize_and_or_builder>().update(x);
101 : }
102 :
103 : // Normalizes equalities.
104 : template <typename Derived>
105 : struct normalize_equality_builder: public data_expression_builder<Derived>
106 : {
107 : typedef data_expression_builder<Derived> super;
108 : using super::enter;
109 : using super::leave;
110 : using super::apply;
111 :
112 : template<class T>
113 14 : void apply(T& result, const application& x)
114 : {
115 14 : data_expression y;
116 14 : super::apply(y, x);
117 14 : if (data::is_equal_to_application(y))
118 : {
119 8 : const data_expression& left = data::binary_left1(y);
120 8 : const data_expression& right = data::binary_right1(y);
121 8 : if (left < right)
122 : {
123 4 : result = data::equal_to(left, right);
124 4 : return;
125 : }
126 : else
127 : {
128 4 : result = data::equal_to(right, left);
129 4 : return;
130 : }
131 : }
132 6 : else if (data::is_not_equal_to_application(y))
133 : {
134 0 : const data_expression& left = data::binary_left1(y);
135 0 : const data_expression& right = data::binary_right1(y);
136 0 : if (left < right)
137 : {
138 0 : result = data::not_equal_to(left, right);
139 0 : return;
140 : }
141 : else
142 : {
143 0 : result = data::not_equal_to(right, left);
144 0 : return;
145 : }
146 : }
147 6 : result = y;
148 14 : }
149 : };
150 :
151 : template <typename T>
152 2 : T normalize_equality(const T& x,
153 : typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value>::type* = nullptr
154 : )
155 : {
156 2 : T result;
157 2 : core::make_apply_builder<normalize_equality_builder>().apply(result, x);
158 2 : return result;
159 0 : }
160 :
161 : template <typename T>
162 : void normalize_equality(T& x,
163 : typename std::enable_if< !std::is_base_of< atermpp::aterm, T >::value>::type* = 0
164 : )
165 : {
166 : core::make_apply_builder<normalize_equality_builder>().update(x);
167 : }
168 :
169 : // normalize operator
170 : template <typename Function>
171 : struct normalizer
172 : {
173 : const Function& f;
174 :
175 26 : normalizer(const Function& f0)
176 26 : : f(f0)
177 26 : {}
178 :
179 26 : data_expression operator()(const data_expression& t) const
180 : {
181 26 : return detail::normalize_and_or(f(t));
182 : }
183 : };
184 :
185 : // utility function for creating a normalizer
186 : template <typename Function>
187 26 : normalizer<Function> N(const Function& f)
188 : {
189 26 : return normalizer<Function>(f);
190 : }
191 :
192 : inline
193 13 : std::string VARIABLE_SPECIFICATION()
194 : {
195 : return
196 : " b: Bool; \n"
197 : " b1: Bool; \n"
198 : " b2: Bool; \n"
199 : " b3: Bool; \n"
200 : " \n"
201 : " n: Nat; \n"
202 : " n1: Nat; \n"
203 : " n2: Nat; \n"
204 : " n3: Nat; \n"
205 : " \n"
206 : " p: Pos; \n"
207 : " p1: Pos; \n"
208 : " p2: Pos; \n"
209 13 : " p3: Pos; \n"
210 : ;
211 : }
212 :
213 : class parser
214 : {
215 : protected:
216 : std::string m_var_decl;
217 : std::string m_data_spec;
218 :
219 : public:
220 :
221 13 : parser(const std::string& var_decl = VARIABLE_SPECIFICATION(), const std::string& data_spec = "")
222 13 : : m_var_decl(var_decl),
223 13 : m_data_spec(data_spec)
224 13 : {}
225 :
226 26 : data_expression operator()(const std::string& expr)
227 : {
228 52 : return parse_data_expression(expr, parse_variables(m_var_decl), parse_data_specification(m_data_spec));
229 : }
230 : };
231 :
232 : template <typename Rewriter1, typename Rewriter2>
233 13 : void test_rewriters(Rewriter1 R1, Rewriter2 R2, std::string expr1, std::string expr2, const std::string& var_decl = VARIABLE_SPECIFICATION(), const std::string& data_spec = "")
234 : {
235 39 : utilities::detail::test_operation(
236 : expr1,
237 : expr2,
238 26 : parser(var_decl, data_spec),
239 : std::equal_to<data_expression>(),
240 : R1,
241 : "R1",
242 : R2,
243 : "R2"
244 : );
245 13 : }
246 :
247 : inline
248 13 : data_expression I(const data_expression& x)
249 : {
250 13 : return x;
251 : }
252 :
253 : } // namespace detail
254 :
255 : } // namespace data
256 :
257 : } // namespace mcrl2
258 :
259 : #endif // MCRL2_DATA_DETAIL_TEST_REWRITERS_H
260 :
|