Line data Source code
1 : // Author(s): Wieger Wesselink, 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/find.h
10 : /// \brief Search functions of the data library.
11 :
12 : #ifndef MCRL2_DATA_FIND_H
13 : #define MCRL2_DATA_FIND_H
14 :
15 : #include "mcrl2/data/add_binding.h"
16 : #include "mcrl2/data/detail/data_functional.h"
17 : #include "mcrl2/data/traverser.h"
18 :
19 : namespace mcrl2
20 : {
21 :
22 : namespace data
23 : {
24 :
25 : namespace detail
26 : {
27 : /// \cond INTERNAL_DOCS
28 : template <template <class> class Traverser, class OutputIterator>
29 : struct find_identifiers_traverser: public Traverser<find_identifiers_traverser<Traverser, OutputIterator> >
30 : {
31 : typedef Traverser<find_identifiers_traverser<Traverser, OutputIterator> > super;
32 :
33 : using super::enter;
34 : using super::leave;
35 : using super::apply;
36 :
37 : OutputIterator out;
38 :
39 15312 : explicit find_identifiers_traverser(OutputIterator out_)
40 15312 : : out(out_)
41 15312 : {}
42 :
43 9904742 : void apply(const core::identifier_string& v)
44 : {
45 9904742 : *out = v;
46 9904742 : }
47 : };
48 :
49 : template <template <class> class Traverser, class OutputIterator>
50 : find_identifiers_traverser<Traverser, OutputIterator>
51 15312 : make_find_identifiers_traverser(OutputIterator out)
52 : {
53 15312 : return find_identifiers_traverser<Traverser, OutputIterator>(out);
54 : }
55 :
56 : template <template <class> class Traverser, class OutputIterator>
57 : struct find_function_symbols_traverser: public Traverser<find_function_symbols_traverser<Traverser, OutputIterator> >
58 : {
59 : typedef Traverser<find_function_symbols_traverser<Traverser, OutputIterator> > super;
60 : using super::enter;
61 : using super::leave;
62 : using super::apply;
63 :
64 : OutputIterator out;
65 :
66 20649 : explicit find_function_symbols_traverser(OutputIterator out_)
67 20649 : : out(out_)
68 20649 : {}
69 :
70 38320 : void apply(const function_symbol& v)
71 : {
72 38320 : *out = v;
73 38320 : }
74 : };
75 :
76 : template <template <class> class Traverser, class OutputIterator>
77 : find_function_symbols_traverser<Traverser, OutputIterator>
78 20649 : make_find_function_symbols_traverser(OutputIterator out)
79 : {
80 20649 : return find_function_symbols_traverser<Traverser, OutputIterator>(out);
81 : }
82 :
83 : template <template <class> class Traverser, class OutputIterator>
84 : struct find_sort_expressions_traverser: public Traverser<find_sort_expressions_traverser<Traverser, OutputIterator> >
85 : {
86 : typedef Traverser<find_sort_expressions_traverser<Traverser, OutputIterator> > super;
87 : using super::enter;
88 : using super::leave;
89 : using super::apply;
90 :
91 : OutputIterator out;
92 :
93 187942 : explicit find_sort_expressions_traverser(OutputIterator out_)
94 187942 : : out(out_)
95 : {
96 187942 : }
97 :
98 1445638 : void apply(const data::sort_expression& v)
99 : {
100 1445638 : *out = v;
101 :
102 : // also traverse sub-expressions!
103 1445638 : super::apply(v);
104 1445638 : }
105 : };
106 :
107 : template <template <class> class Traverser, class OutputIterator>
108 : find_sort_expressions_traverser<Traverser, OutputIterator>
109 187942 : make_find_sort_expressions_traverser(OutputIterator out)
110 : {
111 187942 : return find_sort_expressions_traverser<Traverser, OutputIterator>(out);
112 : }
113 :
114 : template <template <class> class Traverser, class OutputIterator>
115 : struct find_data_expressions_traverser: public Traverser<find_data_expressions_traverser<Traverser, OutputIterator> >
116 : {
117 : typedef Traverser<find_data_expressions_traverser<Traverser, OutputIterator> > super;
118 : using super::enter;
119 : using super::leave;
120 : using super::apply;
121 :
122 : OutputIterator out;
123 :
124 0 : explicit find_data_expressions_traverser(OutputIterator out_)
125 0 : : out(out_)
126 0 : {}
127 :
128 0 : void apply(const data::data_expression& v)
129 : {
130 0 : *out = v;
131 :
132 : // also traverse sub-expressions!
133 0 : super::apply(v);
134 0 : }
135 : };
136 :
137 : template <template <class> class Traverser, class OutputIterator>
138 : find_data_expressions_traverser<Traverser, OutputIterator>
139 0 : make_find_data_expressions_traverser(OutputIterator out)
140 : {
141 0 : return find_data_expressions_traverser<Traverser, OutputIterator>(out);
142 : }
143 :
144 : template <template <class> class Traverser, class OutputIterator>
145 : struct find_all_variables_traverser: public Traverser<find_all_variables_traverser<Traverser, OutputIterator> >
146 : {
147 : typedef Traverser<find_all_variables_traverser<Traverser, OutputIterator> > super;
148 : using super::enter;
149 : using super::leave;
150 : using super::apply;
151 :
152 : OutputIterator out;
153 :
154 835 : explicit find_all_variables_traverser(OutputIterator out_)
155 835 : : out(out_)
156 835 : {}
157 :
158 4505 : void apply(const variable& v)
159 : {
160 4505 : *out = v;
161 4505 : }
162 : };
163 :
164 : template <template <class> class Traverser, class OutputIterator>
165 : find_all_variables_traverser<Traverser, OutputIterator>
166 835 : make_find_all_variables_traverser(OutputIterator out)
167 : {
168 835 : return find_all_variables_traverser<Traverser, OutputIterator>(out);
169 : }
170 :
171 : template <typename T, typename OutputIterator> void find_free_variables(const T& x, OutputIterator o);
172 :
173 : template <template <class> class Traverser, template <template <class> class, class> class Binder, class OutputIterator>
174 : struct find_free_variables_traverser: public Binder<Traverser, find_free_variables_traverser<Traverser, Binder, OutputIterator> >
175 : {
176 : typedef Binder<Traverser, find_free_variables_traverser<Traverser, Binder, OutputIterator> > super;
177 : using super::enter;
178 : using super::leave;
179 : using super::apply;
180 : using super::is_bound;
181 : using super::bound_variables;
182 : using super::increase_bind_count;
183 :
184 : OutputIterator out;
185 :
186 3116655 : explicit find_free_variables_traverser(OutputIterator out_)
187 3116655 : : out(out_)
188 3116655 : {}
189 :
190 : template <typename VariableContainer>
191 : find_free_variables_traverser(OutputIterator out_, const VariableContainer& v)
192 : : out(out_)
193 : {
194 : increase_bind_count(v);
195 : }
196 :
197 2028833 : void apply(const variable& v)
198 : {
199 2028833 : if (!is_bound(v))
200 : {
201 1977904 : *out = v;
202 : }
203 2028833 : }
204 : };
205 :
206 : template <template <class> class Traverser, template <template <class> class, class> class Binder, class OutputIterator>
207 : find_free_variables_traverser<Traverser, Binder, OutputIterator>
208 3116655 : make_find_free_variables_traverser(OutputIterator out)
209 : {
210 3116655 : return find_free_variables_traverser<Traverser, Binder, OutputIterator>(out);
211 : }
212 :
213 : template <template <class> class Traverser, template <template <class> class, class> class Binder, class OutputIterator, class VariableContainer>
214 : find_free_variables_traverser<Traverser, Binder, OutputIterator>
215 : make_find_free_variables_traverser(OutputIterator out, const VariableContainer& v)
216 : {
217 : return find_free_variables_traverser<Traverser, Binder, OutputIterator>(out, v);
218 : }
219 :
220 : template <template <class> class Traverser>
221 : struct search_variable_traverser: public Traverser<search_variable_traverser<Traverser> >
222 : {
223 : typedef Traverser<search_variable_traverser<Traverser> > super;
224 : using super::enter;
225 : using super::leave;
226 : using super::apply;
227 :
228 : bool found;
229 : const variable& v;
230 :
231 12 : explicit search_variable_traverser(const variable& v_)
232 12 : : found(false), v(v_)
233 12 : {}
234 :
235 36 : void apply(const variable& x)
236 : {
237 36 : if (x == v)
238 : {
239 10 : found = true;
240 : }
241 36 : }
242 : };
243 :
244 : template <template <class> class Traverser>
245 : search_variable_traverser<Traverser>
246 : make_search_variable_traverser(const data::variable& v)
247 : {
248 : return search_variable_traverser<Traverser>(v);
249 : }
250 :
251 : template <template <class> class Traverser, template <template <class> class, class> class Binder>
252 : struct search_free_variable_traverser: public Binder<Traverser, search_free_variable_traverser<Traverser, Binder> >
253 : {
254 : typedef Binder<Traverser, search_free_variable_traverser<Traverser, Binder> > super;
255 : using super::enter;
256 : using super::leave;
257 : using super::apply;
258 : using super::is_bound;
259 : using super::bound_variables;
260 : using super::increase_bind_count;
261 :
262 : bool found;
263 : const data::variable& v;
264 :
265 100446 : explicit search_free_variable_traverser(const data::variable& v_)
266 100446 : : found(false), v(v_)
267 100446 : {}
268 :
269 136785 : void apply(const variable& x)
270 : {
271 136785 : if (v == x && !is_bound(x))
272 : {
273 6159 : found = true;
274 : }
275 136785 : }
276 : };
277 :
278 : template <template <class> class Traverser, template <template <class> class, class> class Binder>
279 : search_free_variable_traverser<Traverser, Binder>
280 : make_search_free_variable_traverser(const data::variable& v)
281 : {
282 : return search_free_variable_traverser<Traverser, Binder>(v);
283 : }
284 : /// \endcond
285 :
286 : } // namespace detail
287 :
288 : //--- start generated data find code ---//
289 : /// \\brief Returns all variables that occur in an object
290 : /// \\param[in] x an object containing variables
291 : /// \\param[in,out] o an output iterator to which all variables occurring in x are written.
292 : /// \\return All variables that occur in the term x
293 : template <typename T, typename OutputIterator>
294 637 : void find_all_variables(const T& x, OutputIterator o)
295 : {
296 637 : data::detail::make_find_all_variables_traverser<data::variable_traverser>(o).apply(x);
297 637 : }
298 :
299 : /// \\brief Returns all variables that occur in an object
300 : /// \\param[in] x an object containing variables
301 : /// \\return All variables that occur in the object x
302 : template <typename T>
303 329 : std::set<data::variable> find_all_variables(const T& x)
304 : {
305 329 : std::set<data::variable> result;
306 329 : data::find_all_variables(x, std::inserter(result, result.end()));
307 329 : return result;
308 0 : }
309 :
310 : /// \\brief Returns all variables that occur in an object
311 : /// \\param[in] x an object containing variables
312 : /// \\param[in,out] o an output iterator to which all variables occurring in x are added.
313 : /// \\return All free variables that occur in the object x
314 : template <typename T, typename OutputIterator>
315 3093826 : void find_free_variables(const T& x, OutputIterator o)
316 : {
317 3093826 : data::detail::make_find_free_variables_traverser<data::data_expression_traverser, data::add_data_variable_traverser_binding>(o).apply(x);
318 3093826 : }
319 :
320 : /// \\brief Returns all variables that occur in an object
321 : /// \\param[in] x an object containing variables
322 : /// \\param[in,out] o an output iterator to which all variables occurring in x are written.
323 : /// \\param[in] bound a container of variables
324 : /// \\return All free variables that occur in the object x
325 : template <typename T, typename OutputIterator, typename VariableContainer>
326 : void find_free_variables_with_bound(const T& x, OutputIterator o, const VariableContainer& bound)
327 : {
328 : data::detail::make_find_free_variables_traverser<data::data_expression_traverser, data::add_data_variable_traverser_binding>(o, bound).apply(x);
329 : }
330 :
331 : /// \\brief Returns all variables that occur in an object
332 : /// \\param[in] x an object containing variables
333 : /// \\return All free variables that occur in the object x
334 : template <typename T>
335 3082539 : std::set<data::variable> find_free_variables(const T& x)
336 : {
337 3082539 : std::set<data::variable> result;
338 3082539 : data::find_free_variables(x, std::inserter(result, result.end()));
339 3082539 : return result;
340 0 : }
341 :
342 : /// \\brief Returns all variables that occur in an object
343 : /// \\param[in] x an object containing variables
344 : /// \\param[in] bound a bound a container of variables
345 : /// \\return All free variables that occur in the object x
346 : template <typename T, typename VariableContainer>
347 : std::set<data::variable> find_free_variables_with_bound(const T& x, VariableContainer const& bound)
348 : {
349 : std::set<data::variable> result;
350 : data::find_free_variables_with_bound(x, std::inserter(result, result.end()), bound);
351 : return result;
352 : }
353 :
354 : /// \\brief Returns all identifiers that occur in an object
355 : /// \\param[in] x an object containing identifiers
356 : /// \\param[in,out] o an output iterator to which all identifiers occurring in x are written.
357 : /// \\return All identifiers that occur in the term x
358 : template <typename T, typename OutputIterator>
359 10781 : void find_identifiers(const T& x, OutputIterator o)
360 : {
361 10781 : data::detail::make_find_identifiers_traverser<data::identifier_string_traverser>(o).apply(x);
362 10781 : }
363 :
364 : /// \\brief Returns all identifiers that occur in an object
365 : /// \\param[in] x an object containing identifiers
366 : /// \\return All identifiers that occur in the object x
367 : template <typename T>
368 10781 : std::set<core::identifier_string> find_identifiers(const T& x)
369 : {
370 10781 : std::set<core::identifier_string> result;
371 10781 : data::find_identifiers(x, std::inserter(result, result.end()));
372 10781 : return result;
373 0 : }
374 :
375 : /// \\brief Returns all sort expressions that occur in an object
376 : /// \\param[in] x an object containing sort expressions
377 : /// \\param[in,out] o an output iterator to which all sort expressions occurring in x are written.
378 : /// \\return All sort expressions that occur in the term x
379 : template <typename T, typename OutputIterator>
380 181705 : void find_sort_expressions(const T& x, OutputIterator o)
381 : {
382 181705 : data::detail::make_find_sort_expressions_traverser<data::sort_expression_traverser>(o).apply(x);
383 181705 : }
384 :
385 : /// \\brief Returns all sort expressions that occur in an object
386 : /// \\param[in] x an object containing sort expressions
387 : /// \\return All sort expressions that occur in the object x
388 : template <typename T>
389 181703 : std::set<data::sort_expression> find_sort_expressions(const T& x)
390 : {
391 181703 : std::set<data::sort_expression> result;
392 181703 : data::find_sort_expressions(x, std::inserter(result, result.end()));
393 181703 : return result;
394 0 : }
395 :
396 : /// \\brief Returns all function symbols that occur in an object
397 : /// \\param[in] x an object containing function symbols
398 : /// \\param[in,out] o an output iterator to which all function symbols occurring in x are written.
399 : /// \\return All function symbols that occur in the term x
400 : template <typename T, typename OutputIterator>
401 276 : void find_function_symbols(const T& x, OutputIterator o)
402 : {
403 276 : data::detail::make_find_function_symbols_traverser<data::data_expression_traverser>(o).apply(x);
404 276 : }
405 :
406 : /// \\brief Returns all function symbols that occur in an object
407 : /// \\param[in] x an object containing function symbols
408 : /// \\return All function symbols that occur in the object x
409 : template <typename T>
410 276 : std::set<data::function_symbol> find_function_symbols(const T& x)
411 : {
412 276 : std::set<data::function_symbol> result;
413 276 : data::find_function_symbols(x, std::inserter(result, result.end()));
414 276 : return result;
415 0 : }
416 : //--- end generated data find code ---//
417 :
418 : /// \brief Returns all data expressions that occur in an object
419 : /// \param[in] x an object containing data expressions
420 : /// \param[in,out] o an output iterator to which all data expressions occurring in x are written.
421 : /// \return All data expressions that occur in the term x
422 : template <typename T, typename OutputIterator>
423 0 : void find_data_expressions(const T& x, OutputIterator o)
424 : {
425 0 : data::detail::make_find_data_expressions_traverser<data::data_expression_traverser>(o).apply(x);
426 0 : }
427 :
428 : /// \brief Returns all data expressions that occur in an object
429 : /// \param[in] x an object containing data expressions
430 : /// \return All data expressions that occur in the object x
431 : template <typename T>
432 0 : std::set<data::data_expression> find_data_expressions(const T& x)
433 : {
434 0 : std::set<data::data_expression> result;
435 0 : data::find_data_expressions(x, std::inserter(result, result.end()));
436 0 : return result;
437 0 : }
438 :
439 : /// \brief Returns true if the term has a given variable as subterm.
440 : /// \param[in] x an expression
441 : /// \param[in] v a variable
442 : /// \return True if v occurs in x.
443 : template <typename T>
444 12 : bool search_variable(const T& x, const variable& v)
445 : {
446 12 : data::detail::search_variable_traverser<data::variable_traverser> f(v);
447 12 : f.apply(x);
448 12 : return f.found;
449 : }
450 :
451 : /// \brief Returns true if the term has a given free variable as subterm.
452 : /// \param[in] x an expression
453 : /// \param[in] v a variable
454 : /// \return True if v occurs free in x.
455 : template <typename T>
456 100443 : bool search_free_variable(const T& x, const variable& v)
457 : {
458 100443 : data::detail::search_free_variable_traverser<data::data_expression_traverser, data::add_data_variable_traverser_binding> f(v);
459 100443 : f.apply(x);
460 100443 : return f.found;
461 100443 : }
462 :
463 : /// \brief Returns true if the term has a given sort expression as subterm.
464 : /// \param[in] container an expression or container of expressions
465 : /// \param[in] s A sort expression
466 : /// \return True if the term has a given sort expression as subterm.
467 : template <typename Container>
468 362 : bool search_sort_expression(Container const& container, const sort_expression& s)
469 : {
470 362 : std::set<data::sort_expression> sort_expressions = data::find_sort_expressions(container);
471 724 : return sort_expressions.find(s) != sort_expressions.end();
472 362 : }
473 :
474 : /// \brief Returns true if the term has a given data expression as subterm.
475 : /// \param[in] container an expression or container of expressions
476 : /// \param[in] s A data expression
477 : /// \return True if the term has a given data expression as subterm.
478 : template <typename Container>
479 : bool search_data_expression(Container const& container, const data_expression& s)
480 : {
481 : std::set<data::data_expression> data_expressions = data::find_data_expressions(container);
482 : return data_expressions.find(s) != data_expressions.end();
483 : }
484 :
485 : } // namespace data
486 :
487 : } // namespace mcrl2
488 :
489 : #endif // MCRL2_DATA_FIND_H
|
