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/pbes/find.h
      10             : /// \brief Search functions of the pbes library.
      11             : 
      12             : #ifndef MCRL2_PBES_FIND_H
      13             : #define MCRL2_PBES_FIND_H
      14             : 
      15             : #include "mcrl2/pbes/add_binding.h"
      16             : #include "mcrl2/pbes/traverser.h"
      17             : 
      18             : namespace mcrl2
      19             : {
      20             : 
      21             : namespace pbes_system
      22             : {
      23             : 
      24             : namespace detail
      25             : {
      26             : 
      27             : template <template <class> class Traverser, class OutputIterator>
      28             : struct find_propositional_variables_traverser: public Traverser<find_propositional_variables_traverser<Traverser, OutputIterator> >
      29             : {
      30             :   typedef Traverser<find_propositional_variables_traverser<Traverser, OutputIterator> > super;
      31             :   using super::enter;
      32             :   using super::leave;
      33             :   using super::apply;
      34             : 
      35             :   OutputIterator out;
      36             : 
      37        3812 :   find_propositional_variables_traverser(OutputIterator out_)
      38        3812 :     : out(out_)
      39        3812 :   {}
      40             : 
      41             :   // instead of deriving from a traverser in the data library
      42         748 :   void apply(const data::data_expression&)
      43         748 :   {}
      44             : 
      45        5993 :   void apply(const propositional_variable_instantiation& v)
      46             :   {
      47        5993 :     *out = v;
      48        5993 :   }
      49             : };
      50             : 
      51             : template <template <class> class Traverser, class OutputIterator>
      52             : find_propositional_variables_traverser<Traverser, OutputIterator>
      53        3812 : make_find_propositional_variables_traverser(OutputIterator out)
      54             : {
      55        3812 :   return find_propositional_variables_traverser<Traverser, OutputIterator>(out);
      56             : }
      57             : 
      58             : } // namespace detail
      59             : 
      60             : //--- start generated pbes_system find code ---//
      61             : /// \\brief Returns all variables that occur in an object
      62             : /// \\param[in] x an object containing variables
      63             : /// \\param[in,out] o an output iterator to which all variables occurring in x are written.
      64             : /// \\return All variables that occur in the term x
      65             : template <typename T, typename OutputIterator>
      66           2 : void find_all_variables(const T& x, OutputIterator o)
      67             : {
      68           2 :   data::detail::make_find_all_variables_traverser<pbes_system::variable_traverser>(o).apply(x);
      69           2 : }
      70             : 
      71             : /// \\brief Returns all variables that occur in an object
      72             : /// \\param[in] x an object containing variables
      73             : /// \\return All variables that occur in the object x
      74             : template <typename T>
      75           2 : std::set<data::variable> find_all_variables(const T& x)
      76             : {
      77           2 :   std::set<data::variable> result;
      78           2 :   pbes_system::find_all_variables(x, std::inserter(result, result.end()));
      79           2 :   return result;
      80           0 : }
      81             : 
      82             : /// \\brief Returns all variables that occur in an object
      83             : /// \\param[in] x an object containing variables
      84             : /// \\param[in,out] o an output iterator to which all variables occurring in x are added.
      85             : /// \\return All free variables that occur in the object x
      86             : template <typename T, typename OutputIterator>
      87        4184 : void find_free_variables(const T& x, OutputIterator o)
      88             : {
      89        4184 :   data::detail::make_find_free_variables_traverser<pbes_system::data_expression_traverser, pbes_system::add_data_variable_traverser_binding>(o).apply(x);
      90        4184 : }
      91             : 
      92             : /// \\brief Returns all variables that occur in an object
      93             : /// \\param[in] x an object containing variables
      94             : /// \\param[in,out] o an output iterator to which all variables occurring in x are written.
      95             : /// \\param[in] bound a container of variables
      96             : /// \\return All free variables that occur in the object x
      97             : template <typename T, typename OutputIterator, typename VariableContainer>
      98             : void find_free_variables_with_bound(const T& x, OutputIterator o, const VariableContainer& bound)
      99             : {
     100             :   data::detail::make_find_free_variables_traverser<pbes_system::data_expression_traverser, pbes_system::add_data_variable_traverser_binding>(o, bound).apply(x);
     101             : }
     102             : 
     103             : /// \\brief Returns all variables that occur in an object
     104             : /// \\param[in] x an object containing variables
     105             : /// \\return All free variables that occur in the object x
     106             : template <typename T>
     107        4184 : std::set<data::variable> find_free_variables(const T& x)
     108             : {
     109        4184 :   std::set<data::variable> result;
     110        4184 :   pbes_system::find_free_variables(x, std::inserter(result, result.end()));
     111        4184 :   return result;
     112           0 : }
     113             : 
     114             : /// \\brief Returns all variables that occur in an object
     115             : /// \\param[in] x an object containing variables
     116             : /// \\param[in] bound a bound a container of variables
     117             : /// \\return All free variables that occur in the object x
     118             : template <typename T, typename VariableContainer>
     119             : std::set<data::variable> find_free_variables_with_bound(const T& x, VariableContainer const& bound)
     120             : {
     121             :   std::set<data::variable> result;
     122             :   pbes_system::find_free_variables_with_bound(x, std::inserter(result, result.end()), bound);
     123             :   return result;
     124             : }
     125             : 
     126             : /// \\brief Returns all identifiers that occur in an object
     127             : /// \\param[in] x an object containing identifiers
     128             : /// \\param[in,out] o an output iterator to which all identifiers occurring in x are written.
     129             : /// \\return All identifiers that occur in the term x
     130             : template <typename T, typename OutputIterator>
     131         925 : void find_identifiers(const T& x, OutputIterator o)
     132             : {
     133         925 :   data::detail::make_find_identifiers_traverser<pbes_system::identifier_string_traverser>(o).apply(x);
     134         925 : }
     135             : 
     136             : /// \\brief Returns all identifiers that occur in an object
     137             : /// \\param[in] x an object containing identifiers
     138             : /// \\return All identifiers that occur in the object x
     139             : template <typename T>
     140         925 : std::set<core::identifier_string> find_identifiers(const T& x)
     141             : {
     142         925 :   std::set<core::identifier_string> result;
     143         925 :   pbes_system::find_identifiers(x, std::inserter(result, result.end()));
     144         925 :   return result;
     145           0 : }
     146             : 
     147             : /// \\brief Returns all sort expressions that occur in an object
     148             : /// \\param[in] x an object containing sort expressions
     149             : /// \\param[in,out] o an output iterator to which all sort expressions occurring in x are written.
     150             : /// \\return All sort expressions that occur in the term x
     151             : template <typename T, typename OutputIterator>
     152         622 : void find_sort_expressions(const T& x, OutputIterator o)
     153             : {
     154         622 :   data::detail::make_find_sort_expressions_traverser<pbes_system::sort_expression_traverser>(o).apply(x);
     155         622 : }
     156             : 
     157             : /// \\brief Returns all sort expressions that occur in an object
     158             : /// \\param[in] x an object containing sort expressions
     159             : /// \\return All sort expressions that occur in the object x
     160             : template <typename T>
     161         607 : std::set<data::sort_expression> find_sort_expressions(const T& x)
     162             : {
     163         607 :   std::set<data::sort_expression> result;
     164         607 :   pbes_system::find_sort_expressions(x, std::inserter(result, result.end()));
     165         607 :   return result;
     166           0 : }
     167             : 
     168             : /// \\brief Returns all function symbols that occur in an object
     169             : /// \\param[in] x an object containing function symbols
     170             : /// \\param[in,out] o an output iterator to which all function symbols occurring in x are written.
     171             : /// \\return All function symbols that occur in the term x
     172             : template <typename T, typename OutputIterator>
     173          22 : void find_function_symbols(const T& x, OutputIterator o)
     174             : {
     175          22 :   data::detail::make_find_function_symbols_traverser<pbes_system::data_expression_traverser>(o).apply(x);
     176          22 : }
     177             : 
     178             : /// \\brief Returns all function symbols that occur in an object
     179             : /// \\param[in] x an object containing function symbols
     180             : /// \\return All function symbols that occur in the object x
     181             : template <typename T>
     182          22 : std::set<data::function_symbol> find_function_symbols(const T& x)
     183             : {
     184          22 :   std::set<data::function_symbol> result;
     185          22 :   pbes_system::find_function_symbols(x, std::inserter(result, result.end()));
     186          22 :   return result;
     187           0 : }
     188             : //--- end generated pbes_system find code ---//
     189             : 
     190             : /// \brief Returns all data variables that occur in a range of expressions
     191             : /// \param[in] container a container with expressions
     192             : /// \param[in,out] o an output iterator to which all data variables occurring in t
     193             : ///             are added.
     194             : /// \return All data variables that occur in the term t
     195             : template <typename Container, typename OutputIterator>
     196        3812 : void find_propositional_variable_instantiations(Container const& container, OutputIterator o)
     197             : {
     198        3812 :   pbes_system::detail::make_find_propositional_variables_traverser<pbes_system::pbes_expression_traverser>(o).apply(container);
     199        3812 : }
     200             : 
     201             : /// \brief Returns all data variables that occur in a range of expressions
     202             : /// \param[in] container a container with expressions
     203             : /// \return All data variables that occur in the term t
     204             : template <typename Container>
     205        3808 : std::set<propositional_variable_instantiation> find_propositional_variable_instantiations(Container const& container)
     206             : {
     207        3808 :   std::set<propositional_variable_instantiation> result;
     208        3808 :   pbes_system::find_propositional_variable_instantiations(container, std::inserter(result, result.end()));
     209        3808 :   return result;
     210           0 : }
     211             : 
     212             : /// \brief Returns true if the term has a given variable as subterm.
     213             : /// \param[in] x an expression
     214             : /// \param[in] v a variable
     215             : /// \return True if v occurs in x.
     216             : template <typename T>
     217           0 : bool search_variable(const T& x, const data::variable& v)
     218             : {
     219           0 :   data::detail::search_variable_traverser<pbes_system::variable_traverser> f(v);
     220           0 :   f.apply(x);
     221           0 :   return f.found;
     222             : }
     223             : 
     224             : } // namespace pbes_system
     225             : 
     226             : } // namespace mcrl2
     227             : 
     228             : #endif // MCRL2_PBES_FIND_H