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/detail/free_variable_visitor.h
      10             : /// \brief Add your file description here.
      11             : 
      12             : #ifndef MCRL2_PBES_DETAIL_FIND_FREE_VARIABLES_H
      13             : #define MCRL2_PBES_DETAIL_FIND_FREE_VARIABLES_H
      14             : 
      15             : #include "mcrl2/pbes/traverser.h"
      16             : 
      17             : namespace mcrl2
      18             : {
      19             : 
      20             : namespace pbes_system
      21             : {
      22             : 
      23             : namespace detail
      24             : {
      25             : 
      26             : struct find_free_variables_traverser: public pbes_expression_traverser<find_free_variables_traverser>
      27             : {
      28             :   typedef pbes_expression_traverser<find_free_variables_traverser> super;
      29             :   using super::enter;
      30             :   using super::leave;
      31             :   using super::apply;
      32             : 
      33             :   data::variable_list bound_variables;
      34             :   std::vector<data::variable_list> quantifier_stack;
      35             :   std::set<data::variable> result;
      36             :   bool search_propositional_variables;
      37             : 
      38             :   find_free_variables_traverser(bool search_propositional_variables_ = true)
      39             :     : search_propositional_variables(search_propositional_variables_)
      40             :   {}
      41             : 
      42           2 :   find_free_variables_traverser(const data::variable_list& bound_variables_, bool search_propositional_variables_ = true)
      43           2 :     : bound_variables(bound_variables_), search_propositional_variables(search_propositional_variables_)
      44           2 :   {}
      45             : 
      46             :   /// \brief Returns true if v is an element of bound_variables or quantifier_stack
      47             :   /// \param v A data variable
      48             :   /// \return True if v is an element of bound_variables or quantifier_stack
      49          23 :   bool is_bound(const data::variable& v) const
      50             :   {
      51          23 :     if (std::find(bound_variables.begin(), bound_variables.end(), v) != bound_variables.end())
      52             :     {
      53           0 :       return true;
      54             :     }
      55          36 :     for (const data::variable_list& vars: quantifier_stack)
      56             :     {
      57          16 :       if (std::find(vars.begin(), vars.end(), v) != vars.end())
      58             :       {
      59           3 :         return true;
      60             :       }
      61             :     }
      62          20 :     return false;
      63             :   }
      64             : 
      65             :   /// \brief Pushes v on the stack of quantifier variables
      66             :   /// \param v A sequence of data variables
      67           6 :   void push(const data::variable_list& v)
      68             :   {
      69           6 :     quantifier_stack.push_back(v);
      70           6 :   }
      71             : 
      72             :   /// \brief Pops the stack of quantifier variables
      73           6 :   void pop()
      74             :   {
      75           6 :     quantifier_stack.pop_back();
      76           6 :   }
      77             : 
      78           6 :   void enter(const forall& x)
      79             :   {
      80           6 :     push(x.variables());
      81           6 :   }
      82             : 
      83           6 :   void leave(const forall&)
      84             :   {
      85           6 :     pop();
      86           6 :   }
      87             : 
      88           0 :   void enter(const exists& x)
      89             :   {
      90           0 :     push(x.variables());
      91           0 :   }
      92             : 
      93           0 :   void leave(const exists&)
      94             :   {
      95           0 :     pop();
      96           0 :   }
      97             : 
      98             :   void enter(const propositional_variable& x)
      99             :   {
     100             :     if (search_propositional_variables)
     101             :     {
     102             :       for (const data::variable& v: data::find_free_variables(x.parameters()))
     103             :       {
     104             :         if (!is_bound(v))
     105             :         {
     106             :           result.insert(v);
     107             :         }
     108             :       }
     109             :     }
     110             :   }
     111             : 
     112          11 :   void enter(const data::data_expression& x)
     113             :   {
     114          34 :     for (const data::variable& v: data::find_free_variables(x))
     115             :     {
     116          23 :       if (!is_bound(v))
     117             :       {
     118          20 :         result.insert(v);
     119             :       }
     120          11 :     }
     121          11 :   }
     122             : };
     123             : 
     124             : inline
     125           2 : std::set<data::variable> find_free_variables(const pbes_expression& x, const data::variable_list& bound_variables = data::variable_list(), bool search_propositional_variables = true)
     126             : {
     127           2 :   find_free_variables_traverser f(bound_variables, search_propositional_variables);
     128           2 :   f.apply(x);
     129           4 :   return f.result;
     130           2 : }
     131             : 
     132             : } // namespace detail
     133             : 
     134             : } // namespace pbes_system
     135             : 
     136             : } // namespace mcrl2
     137             : 
     138             : #endif // MCRL2_PBES_DETAIL_FIND_FREE_VARIABLES_H