LCOV - code coverage report
Current view: top level - data/include/mcrl2/data/detail/rewrite - jitty_jittyc.h (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 72 79 91.1 %
Date: 2020-09-16 00:45:56 Functions: 11 13 84.6 %
Legend: Lines: hit not hit

          Line data    Source code
       1             : // Author(s): Jan Friso Groote
       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             : 
      10             : #ifndef MCRL2_DATA_DETAIL_REWRITE_JITTY_JITTYC_H
      11             : #define MCRL2_DATA_DETAIL_REWRITE_JITTY_JITTYC_H
      12             : 
      13             : #include "mcrl2/data/detail/rewrite.h"
      14             : 
      15             : namespace mcrl2
      16             : {
      17             : namespace data
      18             : {
      19             : namespace detail
      20             : {
      21             : 
      22             : template <template <class> class Traverser>
      23     2132084 : struct double_variable_traverser : public Traverser<double_variable_traverser<Traverser> >
      24             : {
      25             :   typedef Traverser<double_variable_traverser<Traverser> > super;
      26             :   using super::enter;
      27             :   using super::leave;
      28             :   using super::apply;
      29             : 
      30             :   std::set<variable> m_seen;
      31             :   std::set<variable> m_doubles;
      32             : 
      33     1779112 :   void apply(const variable& v)
      34             :   {
      35     1779112 :     if (!m_seen.insert(v).second)
      36             :     {
      37      200724 :       m_doubles.insert(v);
      38             :     }
      39     1779112 :   }
      40             : 
      41      816146 :   const std::set<variable>& result()
      42             :   {
      43      816146 :     return m_doubles;
      44             :   }
      45             : };
      46             : 
      47             : 
      48     2191946 : inline variable_list get_free_vars(const data_expression& a)
      49             : {
      50     4383892 :   const std::set<variable> s = find_free_variables(a);
      51     4383892 :   return variable_list(s.begin(), s.end());
      52             : }
      53             : 
      54          31 : inline sort_expression residual_sort(const sort_expression& s, std::size_t no_of_initial_arguments)
      55             : {
      56             :   // Remove no_of_initial_arguments sort from sort s.
      57             : 
      58          31 :   sort_expression result=s;
      59         101 :   while (no_of_initial_arguments > 0)
      60             :   {
      61          35 :     assert(is_function_sort(result));
      62          35 :     const function_sort& sf = atermpp::down_cast<function_sort>(result);
      63          35 :     assert(sf.domain().size()<=no_of_initial_arguments);
      64          35 :     no_of_initial_arguments=no_of_initial_arguments-sf.domain().size();
      65          35 :     result=sf.codomain();
      66             :   }
      67             : 
      68          31 :   return result;
      69             : }
      70             : 
      71             : // This function returns <b, arg_i> where arg_i is the i-th argument of the application t and
      72             : // b is a boolean that indicates whether this argument exists. 
      73             : // TODO: use the optional class of c++17 when it can be used. The current solution is somewhat ugly. 
      74             : // This function yields a pointer to argument_i if it exists. If not it yields the nullptr;
      75       61113 : inline const data_expression* get_argument_of_higher_order_term_helper(const application& t, std::size_t& i)
      76             : {
      77             :   // t has the shape t application(....)
      78       61113 :   if (!is_application(t.head()))
      79             :   {
      80       30238 :     const std::size_t arity = t.size();
      81       30238 :     if (arity>i)
      82             :     {
      83       22327 :       return &t[i];
      84             :     }
      85             :     // arity <=i
      86        7911 :     i=i-arity;
      87        7911 :     return nullptr;
      88             :   }
      89       30875 :   const data_expression* p=get_argument_of_higher_order_term_helper(atermpp::down_cast<application>(t.head()),i);
      90       30875 :   if (p!=nullptr)
      91             :   {
      92       22736 :     return p;
      93             :   }
      94        8139 :   const std::size_t arity = t.size();
      95        8139 :   if (arity>i)
      96             :   {
      97        7911 :     return &t[i];
      98             :   }
      99             :   // arity <=i
     100         228 :   i=i-arity;
     101         228 :   return nullptr;
     102             : }
     103             : 
     104             : // This function returns the i-th argument t_i. NOTE: The first argument has index 1.
     105             : // t is an applicatoin of the shape application(application(...application(f,t1,...tn),tn+1....),tm...).
     106             : // i must be a valid index of an argument. 
     107    15489628 : inline const data_expression& get_argument_of_higher_order_term(const application& t, std::size_t i)
     108             : {
     109             :   // This first case applies to the majority of cases. Therefore this cheap check is done first, before
     110             :   // going into a recursive algorithm. Furthermore checking that t is a function_symbol, etc. is cheaper
     111             :   // than checking that t is not an application by !is_application(t.head()). 
     112    15489628 :   const data_expression& head=t.head();
     113    31009494 :   if (is_function_symbol(head) ||
     114       60476 :       is_variable(head) ||
     115    15550104 :       is_where_clause(head) ||
     116       30238 :       is_abstraction(head))
     117             :   {
     118    15459390 :     assert(t.size()>i);
     119    15459390 :     return t[i];
     120             :   }
     121             : 
     122       30238 :   const data_expression* p=get_argument_of_higher_order_term_helper(t,i);
     123       30238 :   assert(p!=nullptr);
     124       30238 :   return *p;
     125             : }
     126             : 
     127    21342840 : inline std::size_t recursive_number_of_args(const data_expression& t)
     128             : {
     129             :   // Checking these cases is together more efficient than
     130             :   // checking whether t is an application. 
     131    53366256 :   if (is_function_symbol(t) ||
     132    21361004 :       is_variable(t) ||
     133    42703696 :       is_where_clause(t) ||
     134    10680428 :       is_abstraction(t))
     135             :   {
     136    10662412 :     return 0;
     137             :   }
     138             :  
     139    10680428 :   assert(is_application(t));
     140             :   
     141    10680428 :   const application& ta = atermpp::down_cast<application>(t);
     142    10680428 :   return ta.size()+recursive_number_of_args(ta.head());
     143             : }
     144             : 
     145             : // Return the head symbol, nested within applications.
     146             : // This helper function is used to allow inlining of the function
     147             : // get_nested_head.
     148        6278 : inline const data_expression& get_nested_head_helper(const application& t)
     149             : {
     150        6278 :   if (is_application(t.head()))
     151             :   {
     152          83 :     return get_nested_head_helper(atermpp::down_cast<application>(t.head()));
     153             :   }
     154             : 
     155        6195 :   return t.head();
     156             : }
     157             : 
     158             : // Return the head symbol, nested within applications.
     159     3164642 : inline const data_expression& get_nested_head(const data_expression& t)
     160             : {
     161     9493035 :   if (is_function_symbol(t) ||
     162     6327482 :       is_variable(t) ||
     163     9492104 :       is_where_clause(t) ||
     164     3163731 :       is_abstraction(t))
     165             :   {
     166        5643 :     return t;
     167             :   }
     168             : 
     169     3158999 :   const application& ta = atermpp::down_cast<application>(t);
     170     3158999 :   const data_expression& head=ta.head();
     171             : 
     172     6327705 :   if (is_function_symbol(head) ||
     173       15929 :       is_variable(head) ||
     174     3171443 :       is_where_clause(head) ||
     175        6222 :       is_abstraction(head))
     176             :   {
     177     3152804 :     return head;
     178             :   }
     179        6195 :   return get_nested_head_helper(atermpp::down_cast<application>(head));
     180             : }
     181             : 
     182             : // Replace the recursively nested head symbol in t by head.
     183           0 : inline const data_expression replace_nested_head(const data_expression& t, const data_expression& head)
     184             : {
     185           0 :   if (is_application(t))
     186             :   {
     187           0 :     const application& ta = atermpp::down_cast<application>(t);
     188           0 :     return application(replace_nested_head(ta.head(),head),ta.begin(),ta.end());
     189             :   }
     190             : 
     191           0 :   return head;
     192             : }
     193             : 
     194             : template <class ARGUMENT_REWRITER>
     195           0 : inline const data_expression rewrite_all_arguments(const application& t, const ARGUMENT_REWRITER rewriter)
     196             : {
     197           0 :   return application(t.head(),t.begin(),t.end(),rewriter);
     198             : } 
     199             : 
     200             : }
     201             : }
     202             : }
     203             : 
     204             : #endif // REWRITE_JITTY_JITTYC_COMMON_H

Generated by: LCOV version 1.13