Line data Source code
1 : // Author(s): Jeroen Keiren, 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 : //
9 : /// \file mcrl2/data/structured_sort.h
10 : /// \brief The class structured_sort.
11 :
12 : #ifndef MCRL2_DATA_STRUCTURED_SORT_H
13 : #define MCRL2_DATA_STRUCTURED_SORT_H
14 :
15 : #include "mcrl2/data/set_identifier_generator.h"
16 : #include "mcrl2/data/standard_numbers_utility.h"
17 : #include "mcrl2/data/structured_sort_constructor.h"
18 :
19 : namespace mcrl2
20 : {
21 :
22 : namespace data
23 : {
24 :
25 : /// \cond INTERNAL_DOCS
26 : // declare for friendship
27 : namespace sort_fset
28 : {
29 : function_symbol_vector fset_generate_constructors_code(const sort_expression&);
30 : function_symbol_vector fset_generate_functions_code(const sort_expression&);
31 : data_equation_vector fset_generate_equations_code(const sort_expression&);
32 : } // namespace sort_fset
33 :
34 : // declare for friendship
35 : namespace sort_fbag
36 : {
37 : function_symbol_vector fbag_generate_constructors_code(const sort_expression&);
38 : function_symbol_vector fbag_generate_functions_code(const sort_expression&);
39 : data_equation_vector fbag_generate_equations_code(const sort_expression&);
40 : } // namespace sort_fbag
41 : /// \endcond
42 :
43 : /// \brief structured sort.
44 : ///
45 : /// A structured sort is a sort with the following structure:
46 : /// struct c1(pr1,1:S1,1, ..., pr1,k1:S1,k1)?is_c1
47 : /// | ...
48 : /// | cn(prn,1:Sn,1, ..., prn,kn:Sn,kn)?is_cn
49 : /// in this:
50 : /// * c1, ..., cn are called constructors.
51 : /// * pri,j are the projection functions (or constructor arguments).
52 : /// * is_ci are the recognisers.
53 : //--- start generated class structured_sort ---//
54 : /// \\brief A structured sort
55 : class structured_sort: public sort_expression
56 : {
57 : public:
58 : /// \\brief Default constructor.
59 : structured_sort()
60 : : sort_expression(core::detail::default_values::SortStruct)
61 : {}
62 :
63 : /// \\brief Constructor.
64 : /// \\param term A term
65 18584 : explicit structured_sort(const atermpp::aterm& term)
66 18584 : : sort_expression(term)
67 : {
68 18584 : assert(core::detail::check_term_SortStruct(*this));
69 18584 : }
70 :
71 : /// \\brief Constructor.
72 4468 : explicit structured_sort(const structured_sort_constructor_list& constructors)
73 4468 : : sort_expression(atermpp::aterm_appl(core::detail::function_symbol_SortStruct(), constructors))
74 4468 : {}
75 :
76 : /// \\brief Constructor.
77 : template <typename Container>
78 21115 : structured_sort(const Container& constructors, typename atermpp::enable_if_container<Container, structured_sort_constructor>::type* = nullptr)
79 21115 : : sort_expression(atermpp::aterm_appl(core::detail::function_symbol_SortStruct(), structured_sort_constructor_list(constructors.begin(), constructors.end())))
80 21115 : {}
81 :
82 : /// Move semantics
83 0 : structured_sort(const structured_sort&) noexcept = default;
84 : structured_sort(structured_sort&&) noexcept = default;
85 : structured_sort& operator=(const structured_sort&) noexcept = default;
86 : structured_sort& operator=(structured_sort&&) noexcept = default;
87 :
88 69021 : const structured_sort_constructor_list& constructors() const
89 : {
90 69021 : return atermpp::down_cast<structured_sort_constructor_list>((*this)[0]);
91 : }
92 : //--- start user section structured_sort ---//
93 :
94 : friend class data_specification;
95 : friend class sort_specification;
96 :
97 : private:
98 :
99 : friend function_symbol_vector sort_fset::fset_generate_constructors_code(const sort_expression&);
100 : friend function_symbol_vector sort_fset::fset_generate_functions_code(const sort_expression&);
101 : friend data_equation_vector sort_fset::fset_generate_equations_code(const sort_expression&);
102 : friend function_symbol_vector sort_fbag::fbag_generate_constructors_code(const sort_expression&);
103 : friend function_symbol_vector sort_fbag::fbag_generate_functions_code(const sort_expression&);
104 : friend data_equation_vector sort_fbag::fbag_generate_equations_code(const sort_expression&);
105 :
106 : static bool has_recogniser(structured_sort_constructor const& s)
107 : {
108 : return !s.recogniser().empty();
109 : }
110 :
111 17534 : function_symbol to_pos_function(const sort_expression& s) const
112 : {
113 35068 : function_symbol to_pos_function_("@to_pos", make_function_sort_(s, sort_pos::pos()));
114 17534 : return to_pos_function_;
115 : }
116 :
117 17534 : function_symbol equal_arguments_function(const sort_expression& s) const
118 : {
119 35068 : function_symbol equal_arguments_function_("@equal_arguments", make_function_sort_(s, s, sort_bool::bool_()));
120 17534 : return equal_arguments_function_;
121 : }
122 :
123 14038 : function_symbol smaller_arguments_function(const sort_expression& s) const
124 : {
125 28076 : function_symbol smaller_arguments_function_("@less_arguments", make_function_sort_(s, s, sort_bool::bool_()));
126 14038 : return smaller_arguments_function_;
127 : }
128 :
129 14038 : function_symbol smaller_equal_arguments_function(const sort_expression& s) const
130 : {
131 28076 : function_symbol smaller_equal_arguments_function_("@less_equal_arguments", make_function_sort_(s, s, sort_bool::bool_()));
132 14038 : return smaller_equal_arguments_function_;
133 : }
134 :
135 7628 : function_symbol_vector constructor_functions(const sort_expression& s) const
136 : {
137 7628 : function_symbol_vector result;
138 22910 : for (const auto & i : constructors())
139 : {
140 15282 : result.push_back(i.constructor_function(s));
141 : }
142 7628 : return result;
143 0 : }
144 :
145 3496 : function_symbol_vector comparison_functions(const sort_expression& s) const
146 : {
147 3496 : function_symbol_vector result;
148 3496 : result.push_back(to_pos_function(s));
149 3496 : result.push_back(equal_arguments_function(s));
150 3496 : result.push_back(smaller_arguments_function(s));
151 3496 : result.push_back(smaller_equal_arguments_function(s));
152 3496 : return result;
153 0 : }
154 :
155 3496 : function_symbol_vector projection_functions(const sort_expression& s) const
156 : {
157 3496 : function_symbol_vector result;
158 10542 : for (const structured_sort_constructor& i: constructors())
159 : {
160 7046 : function_symbol_vector projections(i.projection_functions(s));
161 :
162 8776 : for (function_symbol_vector::const_iterator j = projections.begin(); j != projections.end(); ++j)
163 : {
164 1730 : result.push_back(*j);
165 : }
166 7046 : }
167 3496 : return result;
168 0 : }
169 :
170 3496 : function_symbol_vector recogniser_functions(const sort_expression& s) const
171 : {
172 3496 : function_symbol_vector result;
173 10542 : for (const structured_sort_constructor& i: constructors())
174 : {
175 7046 : if (i.recogniser() != core::empty_identifier_string())
176 : {
177 808 : result.push_back(i.recogniser_function(s));
178 : }
179 : }
180 3496 : return result;
181 0 : }
182 :
183 :
184 3496 : data_equation_vector comparison_equations(const sort_expression& s) const
185 : {
186 3496 : data_equation_vector result;
187 :
188 : // First add an equation "equal_arguments(v,v)=true", as it is sometimes useful.
189 6992 : variable v("v",s);
190 6992 : result.push_back(data_equation({ v }, sort_bool::true_(),application(equal_arguments_function(s),v,v),sort_bool::true_()));
191 :
192 : // give every constructor an index.
193 3496 : std::size_t index = 1;
194 10542 : for(structured_sort_constructor_list::const_iterator i = constructors().begin(); i != constructors().end(); ++i, ++index)
195 : {
196 : // constructor does not take arguments
197 7046 : if (i->arguments().empty())
198 : {
199 5951 : result.push_back(data_equation(to_pos_function(s)(i->constructor_function(s)), sort_pos::pos(index)));
200 5951 : result.push_back(data_equation(equal_arguments_function(s)(i->constructor_function(s),i->constructor_function(s)), sort_bool::true_()));
201 5951 : result.push_back(data_equation(smaller_arguments_function(s)(i->constructor_function(s),i->constructor_function(s)), sort_bool::false_()));
202 5951 : result.push_back(data_equation(smaller_equal_arguments_function(s)(i->constructor_function(s),i->constructor_function(s)), sort_bool::true_()));
203 : }
204 : else
205 : {
206 1095 : set_identifier_generator generator;
207 :
208 1095 : std::vector< variable > variables1;
209 1095 : std::vector< variable > variables2;
210 3030 : for (const structured_sort_constructor_argument& k: i->arguments())
211 : {
212 1935 : variables1.push_back(variable(generator("v"), k.sort()));
213 1935 : variables2.push_back(variable(generator("w"), k.sort()));
214 : }
215 1095 : application instance1(i->constructor_function(s), variables1);
216 1095 : application instance2(i->constructor_function(s), variables2);
217 :
218 1095 : result.push_back(data_equation(variables1, sort_bool::true_(), to_pos_function(s)(instance1), sort_pos::pos(index)));
219 :
220 : // constructors are the same, generate right hand sides of equal_arguments_function, etc.
221 1095 : variable_vector::const_reverse_iterator end(variables1.rend());
222 1095 : variable_vector::const_reverse_iterator k(variables1.rbegin());
223 1095 : variable_vector::const_reverse_iterator l(variables2.rbegin());
224 :
225 1095 : data_expression right_equal = equal_to(*k, *l);
226 1095 : data_expression right_smaller = less(*k, *l);
227 1095 : data_expression right_smaller_equal = less_equal(*k, *l);
228 :
229 1935 : for (++l, ++k; k != end; ++l, ++k)
230 : {
231 : // Constructors have one or more arguments:
232 : // - rhs for c(x0,...,xn) == c(y0,..,yn):
233 : // x0 == y0 && ... && xn == yn
234 840 : right_equal = sort_bool::and_(equal_to(*k, *l), right_equal);
235 : // - rhs for c(x0,...,xn) < c(y0,..,yn):
236 : // x0 < y0 , when n = 0
237 : // x0 < y0 || (x0 == y0 && x1 < y1) , when n = 1
238 : // x0 < y0 || (x0 == y0 && (x1 < y1 || (x1 == y1 && x2 < y2))) , when n = 2
239 : // etcetera
240 1680 : right_smaller = sort_bool::or_(less(*k, *l),
241 2520 : sort_bool::and_(equal_to(*k, *l), right_smaller));
242 : // - rhs for c(x0,...,xn) <= c(y0,..,yn):
243 : // x0 <= y0 , when n = 0
244 : // x0 < y0 || (x0 == y0 && x1 <= y1) , when n = 1
245 : // x0 < y0 || (x0 == y0 && (x1 < y1 || (x1 == y1 && x2 <= y2))), when n = 2
246 : // etcetera
247 1680 : right_smaller_equal = sort_bool::or_(less(*k, *l),
248 2520 : sort_bool::and_(equal_to(*k, *l), right_smaller_equal));
249 : }
250 :
251 1095 : application left_equal = application(equal_arguments_function(s), instance1, instance2);
252 1095 : application left_smaller = application(smaller_arguments_function(s), instance1, instance2);
253 1095 : application left_smaller_equal = application(smaller_equal_arguments_function(s), instance1, instance2);
254 1095 : variables1.insert(variables1.end(),variables2.begin(),variables2.end());
255 1095 : result.push_back(data_equation(variables1, sort_bool::true_(),left_equal, right_equal));
256 1095 : result.push_back(data_equation(variables1, sort_bool::true_(),left_smaller, right_smaller));
257 1095 : result.push_back(data_equation(variables1, sort_bool::true_(),left_smaller_equal, right_smaller_equal));
258 1095 : }
259 : }
260 6992 : return result;
261 3496 : }
262 :
263 3496 : data_equation_vector constructor_equations(const sort_expression& s) const
264 : {
265 3496 : data_equation_vector result;
266 :
267 6992 : variable x("x", s);
268 6992 : variable y("y", s);
269 10488 : variable_list xy = { x, y };
270 3496 : application to_pos_x = application(to_pos_function(s), x);
271 3496 : application to_pos_y = application(to_pos_function(s), y);
272 3496 : application equal_arguments_xy = application(equal_arguments_function(s), x, y);
273 3496 : application smaller_arguments_xy = application(smaller_arguments_function(s), x, y);
274 3496 : application smaller_equal_arguments_xy = application(smaller_equal_arguments_function(s), x, y);
275 3496 : result.push_back(data_equation(xy, equal_to(to_pos_x, to_pos_y), equal_to(x,y), equal_arguments_xy));
276 3496 : result.push_back(data_equation(xy, not_equal_to(to_pos_x, to_pos_y), equal_to(x,y), sort_bool::false_()));
277 3496 : result.push_back(data_equation(xy, less(to_pos_x, to_pos_y), less(x,y), sort_bool::true_()));
278 3496 : result.push_back(data_equation(xy, equal_to(to_pos_x, to_pos_y), less(x,y), smaller_arguments_xy));
279 3496 : result.push_back(data_equation(xy, greater(to_pos_x, to_pos_y), less(x,y), sort_bool::false_()));
280 3496 : result.push_back(data_equation(xy, less(to_pos_x, to_pos_y), less_equal(x,y), sort_bool::true_()));
281 3496 : result.push_back(data_equation(xy, equal_to(to_pos_x, to_pos_y), less_equal(x,y), smaller_equal_arguments_xy));
282 3496 : result.push_back(data_equation(xy, greater(to_pos_x, to_pos_y), less_equal(x,y), sort_bool::false_()));
283 : // (JK) The following encoding of the equations would be more desirable; however,
284 : // rewriting fails if we use this.
285 : /*
286 : result.push_back(data_equation(xy, sort_bool::true_(), equal_to(x,y), sort_bool::and_(equal_to(to_pos_x, to_pos_y), equal_arguments_xy)));
287 : result.push_back(data_equation(xy, sort_bool::true_(), less(x,y), sort_bool::or_(less(to_pos_x, to_pos_y), sort_bool::and_(equal_to(to_pos_x, to_pos_y), smaller_arguments_xy))));
288 : result.push_back(data_equation(xy, sort_bool::true_(), less_equal(x,y), sort_bool::or_(less(to_pos_x, to_pos_y), sort_bool::and_(equal_to(to_pos_x, to_pos_y), smaller_equal_arguments_xy))));
289 : */
290 6992 : return result;
291 3496 : }
292 :
293 3496 : data_equation_vector projection_equations(const sort_expression& s) const
294 : {
295 3496 : data_equation_vector result;
296 :
297 10542 : for (const auto & i : constructors())
298 : {
299 7046 : if (!i.arguments().empty())
300 : {
301 1095 : structured_sort_constructor_argument_list arguments(i.arguments());
302 :
303 1095 : set_identifier_generator generator;
304 :
305 1095 : std::vector< variable > variables;
306 :
307 : // Create variables for equation
308 3030 : for (const auto & argument : arguments)
309 : {
310 1935 : variables.push_back(variable(generator("v"), argument.sort()));
311 : }
312 :
313 1095 : std::vector< variable >::const_iterator v = variables.begin();
314 :
315 3030 : for (structured_sort_constructor_argument_list::const_iterator j(arguments.begin()); j != arguments.end(); ++j, ++v)
316 : {
317 1935 : if (j->name() != core::empty_identifier_string())
318 : {
319 3460 : application lhs(function_symbol(j->name(), make_function_sort_(s, j->sort()))
320 3460 : (application(i.constructor_function(s), variables)));
321 :
322 1730 : result.push_back(data_equation(variables, lhs, *v));
323 1730 : }
324 : }
325 1095 : }
326 : }
327 :
328 3496 : return result;
329 0 : }
330 :
331 3496 : data_equation_vector recogniser_equations(const sort_expression& s) const
332 : {
333 3496 : data_equation_vector result;
334 :
335 3496 : structured_sort_constructor_list cl(constructors());
336 :
337 10542 : for (structured_sort_constructor_list::const_iterator i = cl.begin(); i != cl.end(); ++i)
338 : {
339 28068 : for (const auto & j : cl)
340 : {
341 21022 : if (j.recogniser() != core::empty_identifier_string())
342 : {
343 1653 : data_expression right = (*i == j) ? sort_bool::true_() : sort_bool::false_();
344 :
345 1653 : if (i->arguments().empty())
346 : {
347 698 : result.push_back(data_equation(j.recogniser_function(s)(i->constructor_function(s)), right));
348 : }
349 : else
350 : {
351 :
352 955 : set_identifier_generator generator;
353 :
354 955 : structured_sort_constructor_argument_list arguments(i->arguments());
355 :
356 : // Create variables for equation
357 955 : variable_vector variables;
358 :
359 2743 : for (const auto & argument : arguments)
360 : {
361 1788 : variables.push_back(variable(generator("v"), argument.sort()));
362 : }
363 :
364 1910 : result.push_back(data_equation(variables, j.recogniser_function(s)(
365 1910 : application(i->constructor_function(s), variables)), right));
366 955 : }
367 1653 : }
368 : }
369 : }
370 :
371 6992 : return result;
372 3496 : }
373 :
374 : public:
375 : /// \brief Returns the constructor functions of this sort, such that the
376 : /// result can be used by the rewriter
377 874 : function_symbol_vector constructor_functions() const
378 : {
379 874 : return constructor_functions(*this);
380 : }
381 :
382 : /// \brief Returns the additional functions of this sort, used to implement
383 : /// its comparison operators
384 : function_symbol_vector comparison_functions() const
385 : {
386 : return comparison_functions(*this);
387 : }
388 :
389 : /// \brief Returns the projection functions of this sort, such that the
390 : /// result can be used by the rewriter
391 : function_symbol_vector projection_functions() const
392 : {
393 : return projection_functions(*this);
394 : }
395 :
396 :
397 : /// \brief Returns the recogniser functions of this sort, such that the
398 : /// result can be used by the rewriter
399 : function_symbol_vector recogniser_functions() const
400 : {
401 : return recogniser_functions(*this);
402 : }
403 :
404 : /// \brief Returns the equations for ==, < and <= for this sort, such that the
405 : /// result can be used by the rewriter internally
406 : data_equation_vector constructor_equations() const
407 : {
408 : return constructor_equations(*this);
409 : }
410 :
411 : /// \brief Returns the equations for the functions used to implement comparison
412 : /// operators on this sort.
413 : /// Needed to do proper rewriting
414 : data_equation_vector comparison_equations() const
415 : {
416 : return comparison_equations(*this);
417 : }
418 :
419 : /// \brief Generate equations for the projection functions of this sort
420 : /// \return A vector of equations for the projection functions of this sort.
421 : data_equation_vector projection_equations() const
422 : {
423 : return projection_equations(*this);
424 : }
425 :
426 : /// \brief Generate equations for the recognisers of this sort, assuming
427 : /// that this sort is referred to with s.
428 : /// \return A vector of equations for the recognisers of this sort.
429 : data_equation_vector recogniser_equations() const
430 : {
431 : return recogniser_equations(*this);
432 : }
433 : //--- end user section structured_sort ---//
434 : };
435 :
436 : /// \\brief Make_structured_sort constructs a new term into a given address.
437 : /// \\ \param t The reference into which the new structured_sort is constructed.
438 : template <class... ARGUMENTS>
439 6191 : inline void make_structured_sort(atermpp::aterm_appl& t, const ARGUMENTS&... args)
440 : {
441 6191 : atermpp::make_term_appl(t, core::detail::function_symbol_SortStruct(), args...);
442 6191 : }
443 :
444 : /// \\brief list of structured_sorts
445 : typedef atermpp::term_list<structured_sort> structured_sort_list;
446 :
447 : /// \\brief vector of structured_sorts
448 : typedef std::vector<structured_sort> structured_sort_vector;
449 :
450 : // prototype declaration
451 : std::string pp(const structured_sort& x);
452 :
453 : /// \\brief Outputs the object to a stream
454 : /// \\param out An output stream
455 : /// \\param x Object x
456 : /// \\return The output stream
457 : inline
458 0 : std::ostream& operator<<(std::ostream& out, const structured_sort& x)
459 : {
460 0 : return out << data::pp(x);
461 : }
462 :
463 : /// \\brief swap overload
464 : inline void swap(structured_sort& t1, structured_sort& t2)
465 : {
466 : t1.swap(t2);
467 : }
468 : //--- end generated class structured_sort ---//
469 :
470 : } // namespace data
471 :
472 : } // namespace mcrl2
473 :
474 : #endif // MCRL2_DATA_STRUCTURED_SORT_H
475 :
|
