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/find.h
      10             : /// \brief Search functions of the data library.
      11             : 
      12             : #ifndef MCRL2_LPS_FIND_H
      13             : #define MCRL2_LPS_FIND_H
      14             : 
      15             : #include "mcrl2/lps/add_binding.h"
      16             : #include "mcrl2/lps/traverser.h"
      17             : #include "mcrl2/process/find.h"
      18             : 
      19             : namespace mcrl2
      20             : {
      21             : 
      22             : namespace lps
      23             : {
      24             : 
      25             : //--- start generated lps find code ---//
      26             : /// \\brief Returns all variables that occur in an object
      27             : /// \\param[in] x an object containing variables
      28             : /// \\param[in,out] o an output iterator to which all variables occurring in x are written.
      29             : /// \\return All variables that occur in the term x
      30             : template <typename T, typename OutputIterator>
      31         172 : void find_all_variables(const T& x, OutputIterator o)
      32             : {
      33         172 :   data::detail::make_find_all_variables_traverser<lps::variable_traverser>(o).apply(x);
      34         172 : }
      35             : 
      36             : /// \\brief Returns all variables that occur in an object
      37             : /// \\param[in] x an object containing variables
      38             : /// \\return All variables that occur in the object x
      39             : template <typename T>
      40         172 : std::set<data::variable> find_all_variables(const T& x)
      41             : {
      42         172 :   std::set<data::variable> result;
      43         172 :   lps::find_all_variables(x, std::inserter(result, result.end()));
      44         172 :   return result;
      45           0 : }
      46             : 
      47             : /// \\brief Returns all variables that occur in an object
      48             : /// \\param[in] x an object containing variables
      49             : /// \\param[in,out] o an output iterator to which all variables occurring in x are added.
      50             : /// \\return All free variables that occur in the object x
      51             : template <typename T, typename OutputIterator>
      52       16826 : void find_free_variables(const T& x, OutputIterator o)
      53             : {
      54       16826 :   data::detail::make_find_free_variables_traverser<lps::data_expression_traverser, lps::add_data_variable_traverser_binding>(o).apply(x);
      55       16826 : }
      56             : 
      57             : /// \\brief Returns all variables that occur in an object
      58             : /// \\param[in] x an object containing variables
      59             : /// \\param[in,out] o an output iterator to which all variables occurring in x are written.
      60             : /// \\param[in] bound a container of variables
      61             : /// \\return All free variables that occur in the object x
      62             : template <typename T, typename OutputIterator, typename VariableContainer>
      63             : void find_free_variables_with_bound(const T& x, OutputIterator o, const VariableContainer& bound)
      64             : {
      65             :   data::detail::make_find_free_variables_traverser<lps::data_expression_traverser, lps::add_data_variable_traverser_binding>(o, bound).apply(x);
      66             : }
      67             : 
      68             : /// \\brief Returns all variables that occur in an object
      69             : /// \\param[in] x an object containing variables
      70             : /// \\return All free variables that occur in the object x
      71             : template <typename T>
      72       16780 : std::set<data::variable> find_free_variables(const T& x)
      73             : {
      74       16780 :   std::set<data::variable> result;
      75       16780 :   lps::find_free_variables(x, std::inserter(result, result.end()));
      76       16780 :   return result;
      77           0 : }
      78             : 
      79             : /// \\brief Returns all variables that occur in an object
      80             : /// \\param[in] x an object containing variables
      81             : /// \\param[in] bound a bound a container of variables
      82             : /// \\return All free variables that occur in the object x
      83             : template <typename T, typename VariableContainer>
      84             : std::set<data::variable> find_free_variables_with_bound(const T& x, VariableContainer const& bound)
      85             : {
      86             :   std::set<data::variable> result;
      87             :   lps::find_free_variables_with_bound(x, std::inserter(result, result.end()), bound);
      88             :   return result;
      89             : }
      90             : 
      91             : /// \\brief Returns all identifiers that occur in an object
      92             : /// \\param[in] x an object containing identifiers
      93             : /// \\param[in,out] o an output iterator to which all identifiers occurring in x are written.
      94             : /// \\return All identifiers that occur in the term x
      95             : template <typename T, typename OutputIterator>
      96        2022 : void find_identifiers(const T& x, OutputIterator o)
      97             : {
      98        2022 :   data::detail::make_find_identifiers_traverser<lps::identifier_string_traverser>(o).apply(x);
      99        2022 : }
     100             : 
     101             : /// \\brief Returns all identifiers that occur in an object
     102             : /// \\param[in] x an object containing identifiers
     103             : /// \\return All identifiers that occur in the object x
     104             : template <typename T>
     105        2022 : std::set<core::identifier_string> find_identifiers(const T& x)
     106             : {
     107        2022 :   std::set<core::identifier_string> result;
     108        2022 :   lps::find_identifiers(x, std::inserter(result, result.end()));
     109        2022 :   return result;
     110           0 : }
     111             : 
     112             : /// \\brief Returns all sort expressions that occur in an object
     113             : /// \\param[in] x an object containing sort expressions
     114             : /// \\param[in,out] o an output iterator to which all sort expressions occurring in x are written.
     115             : /// \\return All sort expressions that occur in the term x
     116             : template <typename T, typename OutputIterator>
     117        2782 : void find_sort_expressions(const T& x, OutputIterator o)
     118             : {
     119        2782 :   data::detail::make_find_sort_expressions_traverser<lps::sort_expression_traverser>(o).apply(x);
     120        2782 : }
     121             : 
     122             : /// \\brief Returns all sort expressions that occur in an object
     123             : /// \\param[in] x an object containing sort expressions
     124             : /// \\return All sort expressions that occur in the object x
     125             : template <typename T>
     126        2781 : std::set<data::sort_expression> find_sort_expressions(const T& x)
     127             : {
     128        2781 :   std::set<data::sort_expression> result;
     129        2781 :   lps::find_sort_expressions(x, std::inserter(result, result.end()));
     130        2781 :   return result;
     131           0 : }
     132             : 
     133             : /// \\brief Returns all function symbols that occur in an object
     134             : /// \\param[in] x an object containing function symbols
     135             : /// \\param[in,out] o an output iterator to which all function symbols occurring in x are written.
     136             : /// \\return All function symbols that occur in the term x
     137             : template <typename T, typename OutputIterator>
     138           0 : void find_function_symbols(const T& x, OutputIterator o)
     139             : {
     140           0 :   data::detail::make_find_function_symbols_traverser<lps::data_expression_traverser>(o).apply(x);
     141           0 : }
     142             : 
     143             : /// \\brief Returns all function symbols that occur in an object
     144             : /// \\param[in] x an object containing function symbols
     145             : /// \\return All function symbols that occur in the object x
     146             : template <typename T>
     147           0 : std::set<data::function_symbol> find_function_symbols(const T& x)
     148             : {
     149           0 :   std::set<data::function_symbol> result;
     150           0 :   lps::find_function_symbols(x, std::inserter(result, result.end()));
     151           0 :   return result;
     152           0 : }
     153             : //--- end generated lps find code ---//
     154             : 
     155             : /// \brief Returns true if the term has a given free variable as subterm.
     156             : /// \param[in] x an expression
     157             : /// \param[in] v a variable
     158             : /// \return True if v occurs free in x.
     159             : template <typename T>
     160           3 : bool search_free_variable(const T& x, const data::variable& v)
     161             : {
     162           3 :   data::detail::search_free_variable_traverser<lps::data_expression_traverser, lps::add_data_variable_traverser_binding> f(v);
     163           3 :   f.apply(x);
     164           3 :   return f.found;
     165           3 : }
     166             : 
     167             : /// \brief Returns all action labels that occur in an object
     168             : /// \param[in] x an object containing action labels
     169             : /// \param[in,out] o an output iterator to which all action labels occurring in x are written.
     170             : /// \return All action labels that occur in the term x
     171             : template <typename T, typename OutputIterator>
     172           0 : void find_action_labels(const T& x, OutputIterator o)
     173             : {
     174           0 :   process::detail::make_find_action_labels_traverser<lps::action_label_traverser>(o).apply(x);
     175           0 : }
     176             : 
     177             : /// \brief Returns all action labels that occur in an object
     178             : /// \param[in] x an object containing action labels
     179             : /// \return All action labels that occur in the object x
     180             : template <typename T>
     181           0 : std::set<process::action_label> find_action_labels(const T& x)
     182             : {
     183           0 :   std::set<process::action_label> result;
     184           0 :   lps::find_action_labels(x, std::inserter(result, result.end()));
     185           0 :   return result;
     186           0 : }
     187             : 
     188             : } // namespace lps
     189             : 
     190             : } // namespace mcrl2
     191             : 
     192             : #endif