LCOV - code coverage report
Current view: top level - data/include/mcrl2/data/detail - split_finite_variables.h (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 19 20 95.0 %
Date: 2020-04-01 00:44:46 Functions: 2 2 100.0 %
Legend: Lines: hit not hit

          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 Computes the subset with variables of finite sort and infinite.
      24             : // TODO: this should be done more efficiently, by avoiding aterm lists
      25             : /// \param variables A sequence of data variables
      26             : /// \param data A data specification
      27             : /// \param finite_variables A sequence of data variables
      28             : /// \param infinite_variables A sequence of data variables
      29             : inline
      30           3 : void split_finite_variables(data::variable_list variables, const data::data_specification& data, data::variable_list& finite_variables, data::variable_list& infinite_variables)
      31             : {
      32           6 :   std::vector<data::variable> finite;
      33           6 :   std::vector<data::variable> infinite;
      34           7 :   for (const data::variable& v: variables)
      35             :   {
      36           4 :     if (data.is_certainly_finite(v.sort()))
      37             :     {
      38           1 :       finite.push_back(v);
      39             :     }
      40             :     else
      41             :     {
      42           3 :       infinite.push_back(v);
      43             :     }
      44             :   }
      45           3 :   finite_variables = data::variable_list(finite.begin(), finite.end());
      46           3 :   infinite_variables = data::variable_list(infinite.begin(), infinite.end());
      47           3 : }
      48             : 
      49             : template <typename Rewriter>
      50             : inline
      51        2579 : void split_enumerable_variables(data::variable_list variables, const data::data_specification& data, const Rewriter& rewr, data::variable_list& enumerable_variables, data::variable_list& non_enumerable_variables)
      52             : {
      53        5158 :   std::vector<data::variable> enumerable;
      54        5158 :   std::vector<data::variable> non_enumerable;
      55        5163 :   for (const data::variable& v: variables)
      56             :   {
      57        2584 :     if (is_enumerable(data, rewr, v.sort()))
      58             :     {
      59        2584 :       enumerable.push_back(v);
      60             :     }
      61             :     else
      62             :     {
      63           0 :       non_enumerable.push_back(v);
      64             :     }
      65             :   }
      66        2579 :   enumerable_variables = data::variable_list(enumerable.begin(), enumerable.end());
      67        2579 :   non_enumerable_variables = data::variable_list(non_enumerable.begin(), non_enumerable.end());
      68        2579 : }
      69             : 
      70             : } // namespace detail
      71             : 
      72             : } // namespace data
      73             : 
      74             : } // namespace mcrl2
      75             : 
      76             : #endif // MCRL2_DATA_DETAIL_SPLIT_FINITE_VARIABLES_H

Generated by: LCOV version 1.13