Line data Source code
1 : // Author(s): Jeroen Keiren, Jeroen van der Wulp, Jan Friso Groote
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/data_specification.h
10 : /// \brief The class data_specification.
11 :
12 : #ifndef MCRL2_DATA_DATA_SPECIFICATION_H
13 : #define MCRL2_DATA_DATA_SPECIFICATION_H
14 :
15 : #include "mcrl2/data/detail/data_functional.h"
16 : #include "mcrl2/data/sort_specification.h"
17 :
18 : namespace mcrl2
19 : {
20 :
21 : namespace data
22 : {
23 :
24 : // template function overloads
25 : data_expression normalize_sorts(const data_expression& x, const data::sort_specification& sortspec);
26 : variable_list normalize_sorts(const variable_list& x, const data::sort_specification& sortspec);
27 : data::data_equation normalize_sorts(const data::data_equation& x, const data::sort_specification& sortspec);
28 : data_equation_list normalize_sorts(const data_equation_list& x, const data::sort_specification& sortspec);
29 : void normalize_sorts(data_equation_vector& x, const data::sort_specification& sortspec);
30 :
31 : // prototype
32 : class data_specification;
33 :
34 : std::string pp(const data::data_specification& x);
35 :
36 : /// \brief Test for a data specification expression
37 : /// \param x A term
38 : /// \return True if \a x is a data specification expression
39 : inline
40 : bool is_data_specification(const atermpp::aterm_appl& x)
41 : {
42 : return x.function() == core::detail::function_symbols::DataSpec;
43 : }
44 :
45 : /// \brief data specification.
46 :
47 : class data_specification: public sort_specification
48 : {
49 : public:
50 : typedef std::map<function_symbol,std::pair<std::function<data_expression(const data_expression&)>, std::string> > implementation_map;
51 :
52 : private:
53 :
54 : /// \cond INTERNAL_DOCS
55 : /// \brief Cached constructors by target sort
56 : struct target_sort_to_function_map
57 : {
58 : bool _outdated;
59 : std::map<sort_expression, std::vector<function_symbol> > _mapping;
60 :
61 61702 : target_sort_to_function_map()
62 61702 : : _outdated(true)
63 61702 : {}
64 :
65 : /// \brief Groups functions according to their target sorts.
66 : /// \param [in,out] c container in which the functions are stored grouped by target sort.
67 : /// \param [in] functions a container with function symbols
68 : template <typename Container>
69 781 : void group_functions_by_target_sort(std::map<sort_expression, std::vector<function_symbol> >& c, const Container& functions)
70 : {
71 12069 : for (const function_symbol& f: functions)
72 : {
73 11288 : const sort_expression s=f.sort();
74 11288 : const sort_expression& index_sort = s.target_sort();
75 11288 : if(c.find(index_sort) == c.end() || std::find(c[index_sort].begin(), c[index_sort].end(), f) == c[index_sort].end())
76 : {
77 : // Insert the constructors, such that those with the smallest number of elements occur first.
78 : // As there are in general only few constructors, this linear insertion should not take too much time.
79 11288 : std::vector<function_symbol>& relevant_rhs = c[index_sort]; // .push_back(f);
80 11288 : const std::size_t f_arity=(is_function_sort(s)?atermpp::down_cast<function_sort>(s).size():0);
81 : std::vector<function_symbol>::iterator i=
82 11288 : std::find_if(relevant_rhs.begin(),
83 : relevant_rhs.end(),
84 192514 : [f_arity](const function_symbol& g)
85 96257 : { const std::size_t g_arity=(is_function_sort(g.sort())?
86 91817 : atermpp::down_cast<function_sort>(g.sort()).size():0);
87 96257 : return f_arity<g_arity;
88 : });
89 11288 : relevant_rhs.insert(i,f);
90 : }
91 : }
92 781 : }
93 :
94 : template <typename FunctionContainer>
95 26694 : void reset(const FunctionContainer& c)
96 : {
97 26694 : if(_outdated)
98 : {
99 781 : _mapping.clear();
100 781 : group_functions_by_target_sort(_mapping, c);
101 781 : _outdated = false;
102 : }
103 26694 : }
104 :
105 20808 : void expire()
106 : {
107 20808 : _outdated = true;
108 20808 : }
109 :
110 26694 : std::map<sort_expression, std::vector<function_symbol> >&mapping()
111 : {
112 26694 : assert(!_outdated);
113 26694 : return _mapping;
114 : }
115 : };
116 :
117 : ///\brief Builds a specification from aterm
118 : void build_from_aterm(const atermpp::aterm_appl& term);
119 : /// \endcond
120 :
121 : protected:
122 :
123 : /// \brief A mapping of sort expressions to the constructors corresponding to that sort.
124 : function_symbol_vector m_user_defined_constructors;
125 :
126 : /// \brief The mappings of the specification.
127 : function_symbol_vector m_user_defined_mappings;
128 :
129 : /// \brief The equations of the specification.
130 : data_equation_vector m_user_defined_equations;
131 :
132 : /// \brief Set containing all constructors, including the system defined ones.
133 : /// The types in these constructors are normalised.
134 : mutable function_symbol_vector m_normalised_constructors;
135 :
136 : /// \brief Cache normalised constructors grouped by target sort.
137 : mutable target_sort_to_function_map m_grouped_normalised_constructors;
138 :
139 : /// \brief Set containing system defined all mappings, including the system defined ones.
140 : /// The types in these mappings are normalised.
141 : mutable function_symbol_vector m_normalised_mappings;
142 :
143 : /// \brief Cache normalised mappings grouped by target sort.
144 : mutable target_sort_to_function_map m_grouped_normalised_mappings;
145 : //
146 : /// \brief Table containing all equations, including the system defined ones.
147 : /// The sorts in these equations are normalised.
148 : /// \details The normalised equations are a set as the number of equations
149 : /// can become large, in which case removing duplicates while inserting equations can be
150 : /// very time consuming.
151 : mutable std::set<data_equation> m_normalised_equations;
152 :
153 : /// \brief A map that for function symbols gives how it can be implemented.
154 : /// \details For each function symbol there is a function : application -> data_expression that
155 : /// when applied to a term in normal form with the function symbol as head symbol
156 : /// returns a function that can be applied to calculate this term.
157 : /// Furthermore, it provides the name of a function that when applied to the
158 : /// number of arguments that the function expects can be used to rewrite the term.
159 : /// This last string can be used for code generation.
160 : mutable implementation_map m_cpp_implemented_functions;
161 :
162 :
163 :
164 14856 : void data_is_not_necessarily_normalised_anymore() const
165 : {
166 14856 : m_normalised_data_is_up_to_date=false;
167 14856 : }
168 :
169 : protected:
170 :
171 : /// \brief Adds a constructor to this specification, and marks it as
172 : /// system defined.
173 : ///
174 : /// \param[in] f A function symbol.
175 : /// \pre f does not yet occur in this specification.
176 : /// \post is_system_defined(f) == true
177 : /// \note this operation does not invalidate iterators of constructors_const_range
178 : inline
179 82123 : void add_normalised_constructor(const function_symbol& f) const
180 : {
181 82123 : function_symbol g(normalize_sorts(f, *this));
182 82123 : if (std::find(m_normalised_constructors.begin(),m_normalised_constructors.end(),g)==m_normalised_constructors.end()) // not found
183 : {
184 81295 : m_normalised_constructors.push_back(g);
185 : }
186 82123 : }
187 :
188 : /// \brief Adds a mapping to this specification, and marks it as system
189 : /// defined.
190 : ///
191 : /// \param[in] f A function symbol.
192 : /// \pre f does not yet occur in this specification.
193 : /// \post is_system_defined(f) == true
194 : /// \note this operation does not invalidate iterators of mappings_const_range
195 1179922 : void add_normalised_mapping(const function_symbol& f) const
196 : {
197 1179922 : function_symbol g(normalize_sorts(f, *this));
198 1179922 : if (std::find(m_normalised_mappings.begin(),m_normalised_mappings.end(),g)==m_normalised_mappings.end()) // not found
199 : {
200 1145333 : m_normalised_mappings.push_back(g);
201 : }
202 1179922 : }
203 :
204 : /// \brief Adds an equation to this specification, and marks it as system
205 : /// defined.
206 : ///
207 : /// \param[in] e An equation.
208 : /// \pre e does not yet occur in this specification.
209 : /// \post is_system_defined(f) == true
210 : /// \note this operation does not invalidate iterators of equations_const_range
211 2726559 : void add_normalised_equation(const data_equation& e) const
212 : {
213 2726559 : m_normalised_equations.insert(normalize_sorts(e,*this));
214 2726559 : }
215 :
216 : template < class Iterator >
217 72131 : void add_normalised_constructors(Iterator begin, Iterator end) const
218 : {
219 154107 : for(Iterator i=begin; i!=end; ++i)
220 : {
221 81976 : data_specification::add_normalised_constructor(*i);
222 : }
223 72131 : }
224 :
225 : template < class Iterator >
226 72131 : void add_normalised_mappings(Iterator begin, Iterator end) const
227 : {
228 1250054 : for(Iterator i=begin; i!=end; ++i)
229 : {
230 1177923 : data_specification::add_normalised_mapping(*i);
231 : }
232 72131 : }
233 :
234 : template < class Iterator >
235 72131 : void add_normalised_equations(Iterator begin, Iterator end) const
236 : {
237 2795428 : for(Iterator i=begin; i!=end; ++i)
238 : {
239 2723297 : data_specification::add_normalised_equation(*i);
240 : }
241 72131 : }
242 :
243 72131 : void add_normalised_cpp_implemented_functions(const implementation_map& c) const
244 : {
245 : typedef std::pair < function_symbol, std::pair<std::function<data_expression(const data_expression&)>, std::string> > map_result_type;
246 86115 : for(const map_result_type f: c)
247 : {
248 13984 : const function_symbol g(normalize_sorts(f.first,*this));
249 13984 : m_cpp_implemented_functions[g]=f.second;
250 13984 : }
251 72131 : }
252 :
253 : /// \brief Adds constructors, mappings and equations for a structured sort
254 : /// to this specification, and marks them as system defined.
255 : ///
256 : /// \param[in] sort A sort expression that is representing the structured sort.
257 : /// \param[out] constructors To this set the new constructors are added.
258 : /// \param[out] mappings New mappings are added to this set.
259 : /// \param[out] equations New equations for the structured sort are added to this set.
260 : /// \param[in] skip_equations This boolean indicates whether equations are added.
261 :
262 3496 : void insert_mappings_constructors_for_structured_sort(
263 : const structured_sort& sort,
264 : std::set < function_symbol >& constructors,
265 : std::set < function_symbol >& mappings,
266 : std::set < data_equation >& equations,
267 : const bool skip_equations) const
268 : {
269 3496 : const structured_sort& s_sort(sort);
270 3496 : function_symbol_vector f(s_sort.constructor_functions(sort));
271 3496 : constructors.insert(f.begin(),f.end());
272 3496 : f = s_sort.projection_functions(sort);
273 3496 : mappings.insert(f.begin(),f.end());
274 3496 : f = s_sort.recogniser_functions(sort);
275 3496 : mappings.insert(f.begin(),f.end());
276 3496 : f = s_sort.comparison_functions(sort);
277 3496 : mappings.insert(f.begin(),f.end());
278 :
279 3496 : if (!skip_equations)
280 : {
281 3496 : data_equation_vector e(s_sort.constructor_equations(sort));
282 3496 : equations.insert(e.begin(),e.end());
283 3496 : e = s_sort.projection_equations(sort);
284 3496 : equations.insert(e.begin(),e.end());
285 3496 : e = s_sort.recogniser_equations(sort);
286 3496 : equations.insert(e.begin(),e.end());
287 3496 : e = s_sort.comparison_equations(sort);
288 3496 : equations.insert(e.begin(),e.end());
289 3496 : }
290 3496 : }
291 :
292 72141 : void add_standard_mappings_and_equations(
293 : const sort_expression& sort,
294 : std::set < function_symbol >& mappings,
295 : std::set < data_equation >& equations,
296 : const bool skip_equations) const
297 : {
298 72141 : function_symbol_vector f(standard_generate_functions_code(sort));
299 72141 : mappings.insert(f.begin(), f.end());
300 :
301 72141 : if (!skip_equations)
302 : {
303 72131 : const data_equation_vector eq(standard_generate_equations_code(sort));
304 72131 : equations.insert(eq.begin(), eq.end());
305 72131 : }
306 72141 : }
307 :
308 : public:
309 :
310 : ///\brief Default constructor. Generate a data specification that contains
311 : /// only booleans and positive numbers.
312 30776 : data_specification()
313 30776 : {
314 30776 : }
315 :
316 : ///\brief Constructor from an aterm.
317 : /// \param[in] t a term adhering to the internal format.
318 3 : data_specification(const atermpp::aterm_appl& t)
319 3 : {
320 3 : build_from_aterm(t);
321 3 : }
322 :
323 : ///\brief Constructor from its members.
324 : data_specification(const basic_sort_vector& sorts,
325 : const alias_vector& aliases,
326 : const function_symbol_vector& constructors,
327 : const function_symbol_vector& user_defined_mappings,
328 : const data_equation_vector& user_defined_equations);
329 :
330 : /// \brief Gets all constructors including those that are system defined.
331 : /// \details The time complexity is the same as for sorts().
332 : /// \return All constructors in this specification, including those for
333 : /// structured sorts.
334 : inline
335 35548 : const function_symbol_vector& constructors() const
336 : {
337 35548 : normalise_data_specification_if_required();
338 35548 : return m_normalised_constructors;
339 : }
340 :
341 : /// \brief Gets the constructors defined by the user, excluding those that
342 : /// are system defined.
343 : /// \details The time complexity for this operation is constant.
344 : inline
345 10381 : const function_symbol_vector& user_defined_constructors() const
346 : {
347 10381 : return m_user_defined_constructors;
348 : }
349 :
350 : /// \brief Gets all constructors of a sort including those that are system defined.
351 : ///
352 : /// \details The time complexity is the same as for sorts().
353 : /// \param[in] s A sort expression.
354 : /// \return The constructors for sort s in this specification.
355 : inline
356 26624 : const function_symbol_vector& constructors(const sort_expression& s, const bool do_not_normalize=false) const
357 : {
358 26624 : normalise_data_specification_if_required();
359 26624 : m_grouped_normalised_constructors.reset(constructors());
360 26624 : if (do_not_normalize)
361 : {
362 2749 : assert(normalize_sorts(s,*this)==s);
363 2749 : return m_grouped_normalised_constructors.mapping()[s];
364 : }
365 23875 : return m_grouped_normalised_constructors.mapping()[normalize_sorts(s,*this)];
366 : }
367 :
368 : /// \brief Gets all mappings in this specification including those that are system defined.
369 : ///
370 : /// \brief The time complexity is the same as for sorts().
371 : /// \return All mappings in this specification, including recognisers and
372 : /// projection functions from structured sorts.
373 : inline
374 6158 : const function_symbol_vector& mappings() const
375 : {
376 6158 : normalise_data_specification_if_required();
377 6158 : return m_normalised_mappings;
378 : }
379 :
380 : /// \brief Gets all user defined mappings in this specification.
381 : ///
382 : /// \brief The time complexity is constant.
383 : /// \return All mappings in this specification, including recognisers and
384 : /// projection functions from structured sorts.
385 : inline
386 10403 : const function_symbol_vector& user_defined_mappings() const
387 : {
388 10403 : return m_user_defined_mappings;
389 : }
390 :
391 : /// \brief Gets all mappings of a sort including those that are system defined
392 : ///
393 : /// \param[in] s A sort expression.
394 : /// \return All mappings in this specification, for which s occurs as a
395 : /// right-hand side of the mapping's sort.
396 : inline
397 70 : const function_symbol_vector& mappings(const sort_expression& s) const
398 : {
399 70 : normalise_data_specification_if_required();
400 70 : m_grouped_normalised_mappings.reset(mappings());
401 70 : return m_grouped_normalised_mappings.mapping()[normalize_sorts(s, *this)];
402 : }
403 :
404 : /// \brief Gets all equations in this specification including those that are system defined
405 : ///
406 : /// \details The time complexity of this operation is the same as that for sort().
407 : /// \return All equations in this specification, including those for
408 : /// structured sorts.
409 : inline
410 2898 : const std::set<data_equation>& equations() const
411 : {
412 2898 : normalise_data_specification_if_required();
413 2898 : return m_normalised_equations;
414 : }
415 :
416 : /// \brief Gets all equations in this specification including those that are system defined
417 : ///
418 : /// \details The time complexity of this operation is the same as that for sort().
419 : /// \return All equations in this specification, including those for
420 : /// structured sorts.
421 : inline
422 278596 : const implementation_map& cpp_implemented_functions() const
423 : {
424 278596 : normalise_data_specification_if_required();
425 278596 : return m_cpp_implemented_functions;
426 : }
427 :
428 : /// \brief Gets all user defined equations.
429 : ///
430 : /// \details The time complexity of this operation is constant.
431 : /// \return All equations in this specification, including those for
432 : /// structured sorts.
433 : inline
434 1175 : const data_equation_vector& user_defined_equations() const
435 : {
436 1175 : return m_user_defined_equations;
437 : }
438 :
439 : // A variant that allows to replace the user defined equations.
440 : inline
441 9126 : data_equation_vector& user_defined_equations()
442 : {
443 9126 : data_is_not_necessarily_normalised_anymore();
444 9126 : return m_user_defined_equations;
445 : }
446 :
447 : /// \brief Adds a constructor to this specification
448 : ///
449 : /// \param[in] f A function symbol.
450 : /// \pre a mapping f does not yet occur in this specification.
451 : /// \note this operation does not invalidate iterators of constructors_const_range
452 137 : void add_constructor(const function_symbol& f)
453 : {
454 137 : if (std::find(m_user_defined_constructors.begin(),m_user_defined_constructors.end(),f)==m_user_defined_constructors.end())
455 : {
456 134 : m_user_defined_constructors.push_back(f);
457 134 : import_system_defined_sort(f.sort());
458 134 : data_is_not_necessarily_normalised_anymore();
459 : }
460 137 : }
461 :
462 : /// \brief Adds a mapping to this specification
463 : ///
464 : /// \param[in] f A function symbol.
465 : /// \pre a constructor f does not yet occur in this specification.
466 : /// \note this operation does not invalidate iterators of mappings_const_range
467 1671 : void add_mapping(const function_symbol& f)
468 : {
469 1671 : if (std::find(m_user_defined_mappings.begin(),m_user_defined_mappings.end(),f)==m_user_defined_mappings.end())
470 : {
471 1668 : m_user_defined_mappings.push_back(f);
472 1668 : import_system_defined_sort(f.sort());
473 1668 : data_is_not_necessarily_normalised_anymore();
474 : }
475 1671 : }
476 :
477 : /// \brief Adds an equation to this specification
478 : ///
479 : /// \param[in] e An equation.
480 : /// \pre e does not yet occur in this specification.
481 : /// \note this operation does not invalidate iterators of equations_const_range
482 2224 : void add_equation(const data_equation& e)
483 : {
484 2224 : if(std::find(m_user_defined_equations.begin(),m_user_defined_equations.end(),e)==m_user_defined_equations.end())
485 : {
486 2220 : m_user_defined_equations.push_back(e);
487 2220 : import_system_defined_sorts(find_sort_expressions(e));
488 2220 : data_is_not_necessarily_normalised_anymore();
489 : }
490 2224 : }
491 :
492 : /// \brief Translate user notation within the equations of the data specification.
493 : /// \details This function replaces explicit numbers, lists, sets and bags by their counterpart
494 : /// in the data types. This function is to be invoked after type checking.
495 1708 : void translate_user_notation()
496 : {
497 2237 : for(data_equation& e: m_user_defined_equations)
498 : {
499 529 : e = data::translate_user_notation(e);
500 : }
501 1708 : data_is_not_necessarily_normalised_anymore();
502 1708 : }
503 :
504 : private:
505 :
506 : ///\brief Puts the constructors, functions and equations in normalised form in
507 : /// de data type.
508 : ///\details See the function normalise_sorts on arbitrary objects for a more detailed description.
509 : /// All sorts in the constructors, mappings and equations are normalised.
510 10404 : void add_data_types_for_sorts() const
511 : {
512 : // Normalise the sorts of the constructors.
513 10404 : m_normalised_constructors.clear();
514 10404 : m_normalised_mappings.clear();
515 10404 : m_normalised_equations.clear();
516 10404 : m_cpp_implemented_functions.clear();
517 :
518 78302 : for (const sort_expression& sort: sorts())
519 : {
520 67898 : import_data_type_for_system_defined_sort(sort);
521 : }
522 :
523 14637 : for (const alias& a: user_defined_aliases())
524 : {
525 4233 : import_data_type_for_system_defined_sort(a.reference());
526 : }
527 :
528 :
529 : // Normalise the constructors.
530 10551 : for (const function_symbol& f: m_user_defined_constructors)
531 : {
532 147 : add_normalised_constructor(f);
533 : }
534 :
535 : // Normalise the sorts of the mappings.
536 12403 : for (const function_symbol& f: m_user_defined_mappings)
537 : {
538 1999 : add_normalised_mapping(f);
539 : }
540 :
541 : // Normalise the sorts of the expressions and variables in equations.
542 13666 : for (const data_equation& eq: m_user_defined_equations)
543 : {
544 3262 : add_normalised_equation(data::translate_user_notation(eq)); // in due time (after 2025) this translate user notation can be removed.
545 : }
546 10404 : }
547 :
548 : /// \brief
549 : /// \details
550 374051 : void normalise_data_specification_if_required() const
551 : {
552 374051 : if (!m_normalised_data_is_up_to_date)
553 : {
554 10404 : m_normalised_data_is_up_to_date=true;
555 10404 : m_grouped_normalised_constructors.expire();
556 10404 : m_grouped_normalised_mappings.expire();
557 10404 : add_data_types_for_sorts();
558 : }
559 374051 : }
560 :
561 : ///\brief Adds the system defined sorts to the sets with constructors, mappings, and equations for
562 : // a given sort. If the boolean skip_equations is true, no equations are added.
563 : void find_associated_system_defined_data_types_for_a_sort(
564 : const sort_expression& sort,
565 : std::set < function_symbol >& constructors,
566 : std::set < function_symbol >& mappings,
567 : std::set < data_equation >& equations,
568 : implementation_map& cpp_implemented_functions,
569 : const bool skip_equations=false) const;
570 :
571 : ///\brief Adds the system defined sorts in a sequence.
572 : /// The second argument is used to check which sorts are added, to prevent
573 : /// useless repetitions of additions of sorts.
574 : /// The function normalise_sorts imports for the given sort_expression sort all sorts, constructors,
575 : /// mappings and equations that belong to this sort to the `normalised' sets in this
576 : /// data type. E.g. for the sort Nat of natural numbers, it is required that Pos
577 : /// (positive numbers) are defined.
578 72131 : void import_data_type_for_system_defined_sort(const sort_expression& sort) const
579 : {
580 72131 : std::set < function_symbol > constructors;
581 72131 : std::set < function_symbol > mappings;
582 72131 : std::set < data_equation > equations;
583 72131 : implementation_map cpp_function_symbols;
584 72131 : find_associated_system_defined_data_types_for_a_sort(sort, constructors, mappings, equations, cpp_function_symbols);
585 :
586 : // add normalised constructors, mappings and equations
587 72131 : add_normalised_constructors(constructors.begin(), constructors.end());
588 72131 : add_normalised_mappings(mappings.begin(), mappings.end());
589 72131 : add_normalised_equations(equations.begin(), equations.end());
590 72131 : add_normalised_cpp_implemented_functions(cpp_function_symbols);
591 72131 : }
592 :
593 : public:
594 :
595 : /// \brief This function provides a sample of all system defined sorts, constructors and mappings
596 : /// that contains at least one specimen of each sort and function symbol. Because types
597 : /// can be parameterised not all function symbols for all types are provided.
598 : /// \details The sorts, constructors and mappings for the following types are added:
599 : /// Bool, Pos, Int, Nat, Real, List(Pos), FSet(Pos), FBag(Pos), Set(Pos), Bag(Pos).
600 : /// How to deal with struct...
601 : void get_system_defined_sorts_constructors_and_mappings(
602 : std::set < sort_expression >& sorts,
603 : std::set < function_symbol >& constructors,
604 : std::set <function_symbol >& mappings) const;
605 :
606 : /// \brief Removes constructor from specification.
607 : ///
608 : /// Note that this does not remove equations containing the constructor.
609 : /// \param[in] f A constructor.
610 : /// \pre f occurs in the specification as constructor.
611 : /// \post f does not occur as constructor.
612 : /// \note this operation does not invalidate iterators of constructors_const_range,
613 : /// only if they point to the element that is removed
614 3 : void remove_constructor(const function_symbol& f)
615 : {
616 3 : detail::remove(m_normalised_constructors, normalize_sorts(f,*this));
617 3 : detail::remove(m_user_defined_constructors, f);
618 3 : }
619 :
620 : /// \brief Removes mapping from specification.
621 : ///
622 : /// Note that this does not remove equations in which the mapping occurs.
623 : /// \param[in] f A function.
624 : /// \post f does not occur as constructor.
625 : /// \note this operation does not invalidate iterators of mappings_const_range,
626 : /// only if they point to the element that is removed
627 2 : void remove_mapping(const function_symbol& f)
628 : {
629 2 : detail::remove(m_normalised_mappings, normalize_sorts(f,*this));
630 2 : detail::remove(m_user_defined_mappings, f);
631 2 : }
632 :
633 : /// \brief Removes equation from specification.
634 : ///
635 : /// \param[in] e An equation.
636 : /// \post e is removed from this specification.
637 : /// \note this operation does not invalidate iterators of equations_const_range,
638 : /// only if they point to the element that is removed
639 2 : void remove_equation(const data_equation& e)
640 : {
641 2 : const data_equation e1=data::translate_user_notation(e); // in due time (after 2025) this translate user notation could possibly be removed.
642 : // as it stands this function is not used.
643 2 : detail::remove(m_normalised_equations, normalize_sorts(e1,*this));
644 2 : detail::remove(m_user_defined_equations, e);
645 2 : }
646 :
647 : /// \brief Checks whether two sort expressions represent the same sort
648 : ///
649 : /// \param[in] s1 A sort expression
650 : /// \param[in] s2 A sort expression
651 24143 : bool equal_sorts(sort_expression const& s1, sort_expression const& s2) const
652 : {
653 24143 : normalise_data_specification_if_required();
654 24143 : const sort_expression normalised_sort1=normalize_sorts(s1,*this);
655 24143 : const sort_expression normalised_sort2=normalize_sorts(s2,*this);
656 48286 : return (normalised_sort1 == normalised_sort2);
657 24143 : }
658 :
659 : /// \brief Checks whether a sort is certainly finite.
660 : ///
661 : /// \param[in] s A sort expression
662 : /// \return true if s can be determined to be finite,
663 : /// false otherwise.
664 : bool is_certainly_finite(const sort_expression& s) const;
665 :
666 : /// \brief Checks whether a sort is a constructor sort
667 : ///
668 : /// \param[in] s A sort expression
669 : /// \return true if s is a constructor sort
670 : bool is_constructor_sort(const sort_expression& s) const
671 : {
672 : normalise_data_specification_if_required();
673 : const sort_expression normalised_sort=normalize_sorts(s,*this);
674 : return !is_function_sort(normalised_sort) && !constructors(normalised_sort).empty();
675 : }
676 :
677 : /// \brief Returns true if
678 : /// <ul>
679 : /// <li>the domain and range sorts of constructors are contained in the list of sorts</li>
680 : /// <li>the domain and range sorts of mappings are contained in the list of sorts</li>
681 : /// </ul>
682 : /// \return True if the data specification is well typed.
683 : bool is_well_typed() const;
684 :
685 7 : bool operator==(const data_specification& other) const
686 : {
687 7 : normalise_data_specification_if_required();
688 7 : other.normalise_data_specification_if_required();
689 : return
690 7 : sort_specification::operator==(other) &&
691 7 : m_normalised_constructors == other.m_normalised_constructors &&
692 21 : m_normalised_mappings == other.m_normalised_mappings &&
693 14 : m_normalised_equations == other.m_normalised_equations;
694 : }
695 :
696 : }; // class data_specification
697 :
698 : //--- start generated class data_specification ---//
699 : // prototype declaration
700 : std::string pp(const data_specification& x);
701 :
702 : /// \\brief Outputs the object to a stream
703 : /// \\param out An output stream
704 : /// \\param x Object x
705 : /// \\return The output stream
706 : inline
707 0 : std::ostream& operator<<(std::ostream& out, const data_specification& x)
708 : {
709 0 : return out << data::pp(x);
710 : }
711 : //--- end generated class data_specification ---//
712 :
713 : /// \brief Merges two data specifications into one.
714 : /// \details It is assumed that the two specs can be merged. I.e.
715 : /// that the second is a safe extension of the first.
716 : /// \param[in] spec1 One of the input specifications.
717 : /// \param[in] spec2 The second input specification.
718 : /// \return A specification that is merged.
719 12 : inline data_specification operator +(data_specification spec1, const data_specification& spec2)
720 : {
721 12 : for(const basic_sort& bsort: spec2.user_defined_sorts())
722 : {
723 0 : spec1.add_sort(bsort);
724 : }
725 :
726 80 : for(const sort_expression& sort: spec2.context_sorts())
727 : {
728 68 : spec1.add_context_sort(sort);
729 : }
730 :
731 16 : for(const alias& a: spec2.user_defined_aliases())
732 : {
733 4 : spec1.add_alias(a);
734 : }
735 :
736 12 : for(const function_symbol& f: spec2.user_defined_constructors())
737 : {
738 0 : spec1.add_constructor(f);
739 : }
740 :
741 13 : for(const function_symbol& f: spec2.user_defined_mappings())
742 : {
743 1 : spec1.add_mapping(f);
744 : }
745 :
746 13 : for(const data_equation& e: spec2.user_defined_equations())
747 : {
748 1 : spec1.add_equation(e);
749 : }
750 :
751 12 : return spec1;
752 : }
753 :
754 : /// \brief Finds a mapping in a data specification.
755 : /// \param data A data specification
756 : /// \param s A string
757 : /// \return The found mapping
758 :
759 : inline
760 10 : function_symbol find_mapping(data_specification const& data, std::string const& s)
761 : {
762 10 : const function_symbol_vector& r(data.mappings());
763 10 : function_symbol_vector::const_iterator i = std::find_if(r.begin(), r.end(), detail::function_symbol_has_name(s));
764 20 : return (i == r.end()) ? function_symbol() : *i;
765 : }
766 :
767 : /// \brief Finds a constructor in a data specification.
768 : /// \param data A data specification
769 : /// \param s A string
770 : /// \return The found constructor
771 :
772 : inline
773 : function_symbol find_constructor(data_specification const& data, std::string const& s)
774 : {
775 : const function_symbol_vector& r(data.constructors());
776 : function_symbol_vector::const_iterator i = std::find_if(r.begin(), r.end(), detail::function_symbol_has_name(s));
777 : return (i == r.end()) ? function_symbol() : *i;
778 : }
779 :
780 : /// \brief Finds a sort in a data specification.
781 : /// \param data A data specification
782 : /// \param s A string
783 : /// \return The found sort
784 :
785 : inline
786 : sort_expression find_sort(data_specification const& data, std::string const& s)
787 : {
788 : const std::set<sort_expression>& r(data.sorts());
789 : const std::set<sort_expression>::const_iterator i = std::find_if(r.begin(), r.end(), detail::sort_has_name(s));
790 : return (i == r.end()) ? sort_expression() : *i;
791 : }
792 :
793 : /// \brief Gets all equations with a data expression as head
794 : /// on one of its sides.
795 : ///
796 : /// \param[in] specification A data specification.
797 : /// \param[in] d A data expression.
798 : /// \return All equations with d as head in one of its sides.
799 :
800 : inline
801 1 : data_equation_vector find_equations(data_specification const& specification, const data_expression& d)
802 : {
803 1 : data_equation_vector result;
804 130 : for (const data_equation& eq: specification.equations())
805 : {
806 129 : if (eq.lhs() == d || eq.rhs() == d)
807 : {
808 1 : result.push_back(eq);
809 : }
810 128 : else if (is_application(eq.lhs()))
811 : {
812 128 : if (atermpp::down_cast<application>(eq.lhs()).head() == d)
813 : {
814 1 : result.push_back(eq);
815 : }
816 : }
817 0 : else if (is_application(eq.rhs()))
818 : {
819 0 : if (atermpp::down_cast<application>(eq.rhs()).head() == d)
820 : {
821 0 : result.push_back(eq);
822 : }
823 : }
824 : }
825 1 : return result;
826 0 : }
827 :
828 :
829 :
830 : /// \brief Order the variables in a variable list such that enumeration over these variables becomes more efficient.
831 : // \detail This routine is experimental, and may benefit from further investigation. The rule of thumb that is
832 : // now used is that first variables of enumerated types are put in the variable list. These are sorts with
833 : // constructors that have no arguments, typically resulting from declarations such as sort Enum = struct e1 | e2 | e3.
834 : // The variables with the largest number of elements are put in front.
835 : // Subsequently, the other data types with a finite number of elements are listed, in arbitrary sequence. At the
836 : // end all other variables are put in an arbitrary sequence.
837 : /// \param[in] l A list of variables that are to be sorted.
838 : /// \param[in] data_spec A data specification containing the constructors that are used to determine efficiency.
839 : /// \return The same list of variables but ordered in such a way that
840 :
841 :
842 576 : inline variable_list order_variables_to_optimise_enumeration(const variable_list& l, const data_specification& data_spec)
843 : {
844 : // Put variables with enumerated types with the largest number of elements in front.
845 : // Put variables of finite types as second.
846 : // Finally put the other variables in the list.
847 576 : std::map < std::size_t,variable_list> vars_of_enumerated_type;
848 576 : variable_list vars_of_finite_type;
849 576 : variable_list rest_vars;
850 875 : for(const variable& v: l)
851 : {
852 299 : if (data_spec.is_certainly_finite(v.sort()))
853 : {
854 250 : bool is_enumerated_type=true;
855 704 : for(const function_symbol& f: data_spec.constructors(v.sort()))
856 : {
857 466 : if (is_function_sort(f.sort()) && function_sort(f.sort()).domain().size()>0)
858 : {
859 12 : is_enumerated_type=false;
860 12 : break;
861 : }
862 : }
863 250 : if (is_enumerated_type)
864 : {
865 238 : vars_of_enumerated_type[data_spec.constructors(v.sort()).size()].push_front(v);
866 : }
867 : else
868 : {
869 12 : vars_of_finite_type.push_front(v);
870 : }
871 : }
872 : else
873 : {
874 : // variable *i has no finite type
875 49 : rest_vars.push_front(v);
876 : }
877 : }
878 :
879 : // Accumulate the result in rest_vars
880 576 : rest_vars=vars_of_finite_type + rest_vars;
881 809 : for(std::map <std::size_t,variable_list>::const_reverse_iterator k=vars_of_enumerated_type.rbegin(); k!=vars_of_enumerated_type.rend(); ++k)
882 : {
883 233 : rest_vars = k->second + rest_vars;
884 : }
885 1152 : return rest_vars;
886 576 : }
887 :
888 : /// \brief Returns the names of functions and mappings that occur in a data specification.
889 : /// \param[in] dataspec A data specification
890 : inline
891 528 : std::set<core::identifier_string> function_and_mapping_identifiers(const data_specification& dataspec)
892 : {
893 528 : std::set<core::identifier_string> result;
894 4816 : for (const function_symbol& f: dataspec.constructors())
895 : {
896 4288 : result.insert(f.name());
897 : }
898 65438 : for (const function_symbol& f: dataspec.mappings())
899 : {
900 64910 : result.insert(f.name());
901 : }
902 528 : return result;
903 0 : }
904 :
905 : } // namespace data
906 :
907 : } // namespace mcrl2
908 :
909 : #endif // MCRL2_DATA_DATA_SPECIFICATION_H
|
