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