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/detail/split_finite_variables.h
      10             : /// \brief add your file description here.
      11             : 
      12             : #ifndef MCRL2_DATA_DETAIL_SPLIT_FINITE_VARIABLES_H
      13             : #define MCRL2_DATA_DETAIL_SPLIT_FINITE_VARIABLES_H
      14             : 
      15             : #include "mcrl2/data/data_specification.h"
      16             : 
      17             : namespace mcrl2 {
      18             : 
      19             : namespace data {
      20             : 
      21             : namespace detail {
      22             : 
      23             : /// \brief Splits the variables in a subset with finite sort, with infinite sort and those that are not used according to a filter. 
      24             : /// \param variables A sequence of data variables.
      25             : /// \param data A data specification.
      26             : /// \param finite_variables A sequence of data variables.
      27             : /// \param infinite_variables A sequence of data variables.
      28             : /// \param unused A sequence of data variables that do not pass the filter.
      29             : /// \param FILTER A predicate that indicates whether a variable is used. 
      30             : template<typename FILTER>
      31             : inline
      32           3 : void split_finite_variables(data::variable_list variables, 
      33             :                             const data::data_specification& data, 
      34             :                             data::variable_list& finite_variables, 
      35             :                             data::variable_list& infinite_variables,
      36             :                             data::variable_list& unused,
      37             :                             const FILTER filter)
      38             : {
      39           7 :   for (data::variable_list::const_reverse_iterator i = variables.rbegin(); i!=variables.rend(); i++)
      40             :   {
      41           4 :     if (!filter(*i))
      42             :     {
      43           0 :       unused.push_front(*i);
      44             :     }
      45           4 :     else if (data.is_certainly_finite(i->sort()))
      46             :     {
      47           1 :       finite_variables.push_front(*i);
      48             :     }
      49             :     else
      50             :     {
      51           3 :       infinite_variables.push_front(*i);
      52             :     }
      53             :   }
      54           3 : }
      55             : 
      56             : /// \brief Splits a list of variables in those that are enumerable, non enumerable and not used, according to a filter.
      57             : /// \param variables A sequence of data variables.
      58             : /// \param data A data specification.
      59             : /// \param rewr A data rewriter to determine which elements are enumerable.
      60             : /// \param finite_variables A sequence of data variables.
      61             : /// \param infinite_variables A sequence of data variables.
      62             : /// \param unused A sequence of data variables that do not pass the filter.
      63             : /// \param FILTER A predicate that indicates whether a variable is used. 
      64             : template <typename Rewriter, typename FILTER>
      65             : inline
      66        2592 : void split_enumerable_variables(data::variable_list variables, 
      67             :                                 const data::data_specification& data, 
      68             :                                 const Rewriter& rewr, 
      69             :                                 data::variable_list& enumerable_variables, 
      70             :                                 data::variable_list& non_enumerable_variables,
      71             :                                 data::variable_list& unused,
      72             :                                 const FILTER filter)
      73             : {
      74        5190 :   for (data::variable_list::const_reverse_iterator i = variables.rbegin(); i!=variables.rend(); i++)
      75             :   {
      76        2598 :     if (!filter(*i))
      77             :     {
      78        1519 :       unused.push_front(*i);
      79             :     }
      80        1079 :     else if (is_enumerable(data, rewr, i->sort()))
      81             :     {
      82        1079 :       enumerable_variables.push_front(*i);
      83             :     }
      84             :     else
      85             :     {
      86           0 :       non_enumerable_variables.push_front(*i);
      87             :     }
      88             :   }
      89        2592 : }
      90             : 
      91             : /* /// \brief Computes the subset with variables of finite sort and infinite.
      92             : // TODO: this should be done more efficiently, by avoiding aterm lists
      93             : /// \param variables A sequence of data variables
      94             : /// \param data A data specification
      95             : /// \param finite_variables A sequence of data variables
      96             : /// \param infinite_variables A sequence of data variables
      97             : inline
      98             : void split_finite_variables(data::variable_list variables, 
      99             :                             const data::data_specification& data, 
     100             :                             data::variable_list& finite_variables, 
     101             :                             data::variable_list& infinite_variables)
     102             : {
     103             :   for (data::variable_list::const_reverse_iterator i = variables.rbegin(); i!=variables.rend(); i++)
     104             :   {
     105             :     if (data.is_certainly_finite(i->sort()))
     106             :     {
     107             :       finite_variables.push_front(*i);
     108             :     }
     109             :     else
     110             :     {
     111             :       infinite_variables.push_front(*i);
     112             :     }
     113             :   }
     114             : }
     115             : 
     116             : template <typename Rewriter>
     117             : inline
     118             : void split_enumerable_variables(data::variable_list variables, 
     119             :                                 const data::data_specification& data, 
     120             :                                 const Rewriter& rewr, 
     121             :                                 data::variable_list& enumerable_variables, 
     122             :                                 data::variable_list& non_enumerable_variables)
     123             : {
     124             :   for (data::variable_list::const_reverse_iterator i = variables.rbegin(); i!=variables.rend(); i++)
     125             :   {
     126             :     if (is_enumerable(data, rewr, i->sort()))
     127             :     {
     128             :       enumerable_variables.push_front(*i);
     129             :     }
     130             :     else
     131             :     {
     132             :       non_enumerable_variables.push_front(*i);
     133             :     }
     134             :   }
     135             : } */
     136             : 
     137             : } // namespace detail
     138             : 
     139             : } // namespace data
     140             : 
     141             : } // namespace mcrl2
     142             : 
     143             : #endif // MCRL2_DATA_DETAIL_SPLIT_FINITE_VARIABLES_H