LCOV - code coverage report
Current view: top level - data/include/mcrl2/data/detail - data_utility.h (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 38 53 71.7 %
Date: 2020-02-21 00:44:40 Functions: 13 14 92.9 %
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/data_utility.h
      10             : /// \brief Add your file description here.
      11             : 
      12             : #ifndef MCRL2_DATA_DETAIL_DATA_UTILITY_H
      13             : #define MCRL2_DATA_DETAIL_DATA_UTILITY_H
      14             : 
      15             : #include "mcrl2/data/alias.h"
      16             : #include "mcrl2/data/assignment.h"
      17             : #include "mcrl2/data/detail/data_functional.h"
      18             : #include "mcrl2/data/standard_utility.h"
      19             : #include "mcrl2/utilities/detail/container_utility.h"
      20             : 
      21             : namespace mcrl2
      22             : {
      23             : 
      24             : namespace data
      25             : {
      26             : 
      27             : namespace detail
      28             : {
      29             : 
      30             : /// \brief Returns the sorts of a sequence of parameters.
      31             : template <typename Container>
      32       10889 : data::sort_expression_list parameter_sorts(const Container& parameters)
      33             : {
      34       21778 :   data::sort_expression_list sorts;
      35       20380 :   for (auto const& param: parameters)
      36             :   {
      37        9491 :     sorts.push_front(param.sort());
      38             :   }
      39       21778 :   return atermpp::reverse(sorts);
      40             : }
      41             : 
      42             : /// \brief Returns true if the names of the given variables are unique.
      43             : /// \param variables A sequence of data variables
      44             : /// \return True if the names of the given variables are unique.
      45             : template <class VariableContainer>
      46             : inline
      47        1281 : bool unique_names(const VariableContainer& variables)
      48             : {
      49        2562 :   std::set<core::identifier_string> variable_names;
      50        2661 :   for (auto const& var: variables)
      51             :   {
      52        1380 :     variable_names.insert(var.name());
      53             :   }
      54        2562 :   return variable_names.size() == variables.size();
      55             : }
      56             : 
      57             : /// \brief Returns true if the left hand sides of assignments are contained in variables.
      58             : /// \param assignments A sequence of assignments to data variables
      59             : /// \param variables A sequence of data variables
      60             : /// \return True if the left hand sides of assignments are contained in variables.
      61             : inline
      62         102 : bool check_assignment_variables(assignment_list const& assignments, variable_list const& variables)
      63             : {
      64             :         using utilities::detail::contains;
      65             : 
      66         204 :   std::set<variable> v(variables.begin(), variables.end());
      67         432 :   for (const assignment& a: assignments)
      68             :   {
      69         330 :     if (!contains(v, a.lhs()))
      70             :     {
      71           0 :       return false;
      72             :     }
      73             :   }
      74         102 :   return true;
      75             : }
      76             : 
      77             : /// \brief Returns true if the domain sorts and the codomain sort of the given sort s are contained in sorts.
      78             : /// \param s A sort expression
      79             : /// \param sorts A set of sort expressions
      80             : /// \return True if the sort is contained in <tt>sorts</tt>
      81             : template <typename SortContainer>
      82       21417 : inline bool check_sort(const sort_expression& s, const SortContainer& sorts)
      83             : {
      84             :   using utilities::detail::remove_if;
      85             : 
      86       42834 :   std::set<sort_expression> s_sorts = data::find_sort_expressions(s);
      87       77323 :   remove_if(s_sorts, [](const sort_expression& x) { return !is_function_sort(x); });
      88       42033 :   for (const sort_expression& sort: s_sorts)
      89             :   {
      90       20616 :     if (std::find(sorts.begin(), sorts.end(), sort) == sorts.end())
      91             :     {
      92             :       // sort *i is not well-typed, a system defined sort or an alias
      93       13736 :       if (!(is_system_defined(sort)) && is_alias(sort))
      94             :       {
      95           0 :         alias sort_alias(sort);
      96             : 
      97           0 :         if (std::find(sorts.begin(), sorts.end(), sort_alias.name()) == sorts.end())
      98             :         {
      99             :           // sort_alias.reference() is a basic, structured or container sort
     100           0 :           const sort_expression& sort_reference(sort_alias.reference());
     101             : 
     102           0 :           if (std::find(sorts.begin(), sorts.end(), sort_reference) == sorts.end())
     103             :           {
     104             :             // sort_reference is structured or container sort
     105           0 :             if (is_structured_sort(sort_reference))
     106             :             {
     107           0 :               assert(false);
     108             :             }
     109           0 :             else if (is_container_sort(sort_reference))
     110             :             {
     111           0 :               if (std::find(sorts.begin(), sorts.end(), container_sort(sort_reference).element_sort()) == sorts.end())
     112             :               {
     113           0 :                 return false;
     114             :               }
     115             :             }
     116             :             else
     117             :             {
     118           0 :               assert(false);
     119             :             }
     120             :           }
     121             :         }
     122             :       }
     123             :     }
     124             :   }
     125             : 
     126       21417 :   return true;
     127             : }
     128             : 
     129             : /// \brief Returns true if the domain sorts and the range sort of the sorts in the sequence [first, last)
     130             : /// are contained in sorts.
     131             : /// \param first Start of a sequence of sorts
     132             : /// \param last End of a sequence of sorts
     133             : /// \param sorts A set of sort expressions
     134             : /// \return True if the sequence of sorts is contained in <tt>sorts</tt>
     135             : template <typename Iterator, typename SortContainer>
     136        1077 : bool check_sorts(Iterator first, Iterator last, const SortContainer& sorts)
     137             : {
     138        5340 :   for (Iterator i = first; i != last; ++i)
     139             :   {
     140        4263 :     if (!check_sort(*i, sorts))
     141             :     {
     142           0 :       return false;
     143             :     }
     144             :   }
     145        1077 :   return true;
     146             : }
     147             : 
     148             : /// \brief Returns true if the domain sorts and the range sort of the given variables are contained in sorts.
     149             : /// \param variables A container with data variables
     150             : /// \param sorts A set of sort expressions
     151             : /// \return True if the domain sorts and the range sort of the given variables are contained in sorts.
     152             : template <typename VariableContainer, typename SortContainer>
     153         171 : bool check_variable_sorts(const VariableContainer& variables, const SortContainer& sorts)
     154             : {
     155         502 :   for (typename VariableContainer::const_iterator i = variables.begin(); i != variables.end(); ++i)
     156             :   {
     157         331 :     if (!check_sort(i->sort(), sorts))
     158             :     {
     159           0 :       return false;
     160             :     }
     161             :   }
     162         171 :   return true;
     163             : }
     164             : 
     165             : /// \brief Returns true if names of the given variables are not contained in names.
     166             : /// \param variables A sequence of data variables
     167             : /// \param names A set of strings
     168             : /// \return True if names of the given variables are not contained in names.
     169             : inline
     170         102 : bool check_variable_names(variable_list const& variables, const std::set<core::identifier_string>& names)
     171             : {
     172             :   using utilities::detail::contains;
     173             : 
     174         149 :   for (const variable& v: variables)
     175             :   {
     176          47 :     if (contains(names, v.name()))
     177             :     {
     178           0 :       return false;
     179             :     }
     180             :   }
     181         102 :   return true;
     182             : }
     183             : 
     184             : /// \brief Returns true if the domain sorts and range sort of the given functions are contained in sorts.
     185             : /// \param range A sequence of data operations
     186             : /// \param sorts A set of sort expressions
     187             : /// \return True if the domain sorts and range sort of the given functions are contained in sorts.
     188             : template < typename Container, typename SortContainer >
     189             : inline
     190         280 : bool check_data_spec_sorts(const Container& container, const SortContainer& sorts)
     191             : {
     192       16889 :   for (typename Container::const_iterator i = container.begin(); i != container.end(); ++i)
     193             :   {
     194       16609 :     if (!check_sort(i->sort(), sorts))
     195             :     {
     196           0 :       return false;
     197             :     }
     198             :   }
     199         280 :   return true;
     200             : }
     201             : 
     202             : } // namespace detail
     203             : 
     204             : } // namespace data
     205             : 
     206             : } // namespace mcrl2
     207             : 
     208             : #endif // MCRL2_DATA_DETAIL_DATA_UTILITY_H

Generated by: LCOV version 1.13