LCOV - code coverage report
Current view: top level - data/source/detail/rewrite - strategy.cpp (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 101 102 99.0 %
Date: 2020-02-29 00:53:40 Functions: 10 10 100.0 %
Legend: Lines: hit not hit

          Line data    Source code
       1             : // Author(s): Muck van Weerdenburg, 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             : #include "mcrl2/data/detail/rewrite/strategy_rule.h"
      11             : #include "mcrl2/data/detail/rewrite/jitty_jittyc.h"
      12             : 
      13             : using namespace mcrl2::data;
      14             : 
      15             : namespace
      16             : {
      17             : 
      18             : /// \brief
      19     9375753 : class dependencies_rewrite_rule_pair
      20             : {
      21             :   public:
      22     1338887 :     dependencies_rewrite_rule_pair(std::set<std::size_t>& dependencies, const data_equation& eq)
      23     1338887 :      : m_dependencies(dependencies), m_equation(eq)
      24     1338887 :     {}
      25             : 
      26     2148686 :     const std::set<std::size_t>& dependencies() const
      27             :     {
      28     2148686 :       return m_dependencies;
      29             :     }
      30             : 
      31     1338887 :     const data_equation& equation() const
      32             :     {
      33     1338887 :       return m_equation;
      34             :     }
      35             : 
      36             :   protected:
      37             :     std::set<std::size_t> m_dependencies;
      38             :     data_equation m_equation;
      39             : };
      40             : 
      41             : }
      42             : 
      43             : namespace mcrl2
      44             : {
      45             : namespace data
      46             : {
      47             : namespace detail
      48             : {
      49             : 
      50      224004 : strategy create_strategy(data_equation_list rules)
      51             : {
      52      448008 :   std::vector<strategy_rule> strat;
      53             : 
      54      448008 :   std::vector<bool> used;
      55             : 
      56      224004 :   std::size_t arity = 0;
      57      224004 :   std::size_t max_number_of_variables = 0;
      58     1546508 :   while (!rules.empty())
      59             :   {
      60     1322504 :     data_equation_list l;
      61     1322504 :     std::vector<dependencies_rewrite_rule_pair> m;
      62             : 
      63     1322504 :     std::vector<int> args(arity,-1);
      64             : 
      65     2304430 :     for (const data_equation& this_rule: rules)
      66             :     {
      67     1643178 :       max_number_of_variables=std::max(this_rule.variables().size(),max_number_of_variables);
      68     1643178 :       const data_expression& this_rule_lhs = this_rule.lhs();
      69     1643178 :       if ((is_function_symbol(this_rule_lhs)?1:detail::recursive_number_of_args(this_rule_lhs)+1) == arity + 1)
      70             :       {
      71      529088 :         const data_expression& cond = this_rule.condition();
      72     1058176 :         atermpp::term_list<variable_list> vars = { get_free_vars(cond) };
      73             : 
      74     1058176 :         std::vector < bool> bs(arity,false);
      75             : 
      76     1643178 :         for (std::size_t i = 0; i < arity; i++)
      77             :         {
      78     2228180 :           const data_expression this_rule_lhs_iplus1_arg=detail::get_argument_of_higher_order_term(atermpp::down_cast<application>(this_rule_lhs),i);
      79     1114090 :           if (!is_variable(this_rule_lhs_iplus1_arg))
      80             :           {
      81      541395 :             bs[i] = true;
      82     1082790 :             const variable_list evars = get_free_vars(this_rule_lhs_iplus1_arg);
      83      939126 :             for (variable_list::const_iterator v=evars.begin(); v!=evars.end(); ++v)
      84             :             {
      85      397731 :               int j=0;
      86      397731 :               const atermpp::term_list <variable_list>& next_vars=vars.tail();
      87      607649 :               for (atermpp::term_list <variable_list>::const_iterator o=next_vars.begin(); o!=next_vars.end(); ++o)
      88             :               {
      89      209918 :                 if (std::find(o->begin(),o->end(),*v) != o->end())
      90             :                 {
      91        7244 :                   bs[j] = true;
      92             :                 }
      93      209918 :                 j++;
      94             :               }
      95             :             }
      96      541395 :             vars=push_back(vars,get_free_vars(this_rule_lhs_iplus1_arg));
      97             :           }
      98             :           else
      99             :           {
     100      572695 :             int j = -1;
     101      572695 :             bool b = false;
     102     1623477 :             for (atermpp::term_list <variable_list>::const_iterator o=vars.begin(); o!=vars.end(); ++o)
     103             :             {
     104     1050782 :               if (std::find(o->begin(),o->end(),variable(this_rule_lhs_iplus1_arg)) != o->end())
     105             :               {
     106      106246 :                 if (j >= 0)
     107             :                 {
     108       64302 :                   bs[j] = true;
     109             :                 }
     110      106246 :                 b = true;
     111             :               }
     112     1050782 :               j++;
     113             :             }
     114      572695 :             if (b)
     115             :             {
     116      105461 :               bs[i] = true;
     117             :             }
     118      572695 :             vars=push_back(vars,get_free_vars(this_rule_lhs_iplus1_arg));
     119             :           }
     120             :         }
     121             : 
     122     1058176 :         double_variable_traverser<data::variable_traverser> lhs_doubles;
     123     1058176 :         double_variable_traverser<data::variable_traverser> rhs_doubles;
     124     1058176 :         std::set<variable> condition_vars = find_free_variables(this_rule.condition());
     125      529088 :         lhs_doubles.apply(this_rule.lhs());
     126      529088 :         rhs_doubles.apply(this_rule.rhs());
     127             : 
     128     1058176 :         std::set<std::size_t> deps;
     129     1643178 :         for (std::size_t i = 0; i < arity; i++)
     130             :         {
     131     1114090 :           if (i>=used.size())
     132             :           {
     133      437248 :             used.resize(i+1,false);
     134             :           }
     135             :           // Check whether argument i is a variable that occurs more than once in
     136             :           // the left or right hand side, or occurs in the condition. It is not clear whether it is
     137             :           // useful to check that it occurs in the condition, but this is what the jittyc rewriter also does.
     138     1114090 :           const data_expression& arg_i = get_argument_of_higher_order_term(atermpp::down_cast<application>(this_rule.lhs()), i);
     139     2633437 :           if ((bs[i] ||
     140     1215771 :                (is_variable(arg_i) && (lhs_doubles.result().count(atermpp::down_cast<variable>(arg_i)) > 0 ||
     141      810514 :                                        condition_vars.count(atermpp::down_cast<variable>(arg_i)) > 0 ||
     142     1519347 :                                        rhs_doubles.result().count(atermpp::down_cast<variable>(arg_i)) > 0))
     143     1863537 :               ) && !used[i])
     144             :           {
     145      746299 :             deps.insert(i);
     146      746299 :             args[i] += 1;
     147             :           }
     148             :         }
     149             : 
     150      529088 :         m.push_back(dependencies_rewrite_rule_pair(deps,this_rule));
     151             :       }
     152             :       else
     153             :       {
     154     1114090 :         l.push_front(this_rule);
     155             :       }
     156             :     }
     157             : 
     158     1295178 :     while (!m.empty())
     159             :     {
     160      859796 :       std::vector<dependencies_rewrite_rule_pair> m2;
     161     1881720 :       for (const dependencies_rewrite_rule_pair& p: m)
     162             :       {
     163     1338887 :         if (p.dependencies().empty())
     164             :         {
     165     1058176 :           const data_equation rule = p.equation();
     166      529088 :           strat.push_back(strategy_rule(rule));
     167             :         }
     168             :         else
     169             :         {
     170      809799 :           m2.push_back(p);
     171             :         }
     172             :       }
     173      542833 :       m = m2;
     174             : 
     175      542833 :       if (m.empty())
     176             :       {
     177      225870 :         break;
     178             :       }
     179             : 
     180      316963 :       int max = -1;
     181      316963 :       std::size_t maxidx = 0;
     182             : 
     183     1020568 :       for (std::size_t i = 0; i < arity; i++)
     184             :       {
     185      703605 :         assert(i < static_cast<std::size_t>(1) << (8 * sizeof(int) - 1));
     186      703605 :         if (args[i] > max)
     187             :         {
     188      329197 :           maxidx = i+1;
     189      329197 :           max = args[i];
     190             :         }
     191             :       }
     192             : 
     193      316963 :       if (maxidx > 0)
     194             :       {
     195      316963 :         args[maxidx-1] = -1;
     196      316963 :         if (maxidx>used.size())
     197             :         {
     198           0 :           used.resize(maxidx,false);
     199             :         }
     200      316963 :         used[maxidx-1] = true;
     201             : 
     202      316963 :         const std::size_t k(maxidx-1);
     203      316963 :         strat.push_back(strategy_rule(k));
     204      316963 :         m2.clear();
     205     1126762 :         for (const dependencies_rewrite_rule_pair& p: m)
     206             :         {
     207     1619598 :           const data_equation eq=p.equation();
     208     1619598 :           std::set<std::size_t> dependencies=p.dependencies();
     209      809799 :           dependencies.erase(k);
     210      809799 :           m2.push_back(dependencies_rewrite_rule_pair(dependencies,eq));
     211             :         }
     212      316963 :         m = m2;
     213             :       }
     214             :     }
     215             : 
     216      661252 :     rules = reverse(l);
     217      661252 :     arity++;
     218             :   }
     219             : 
     220      448008 :   return strategy(max_number_of_variables, atermpp::term_list<data::detail::strategy_rule>(strat.begin(), strat.end()));
     221             : }
     222             : 
     223             : } // namespace detail
     224             : } // namespace data
     225         366 : } // namespace mcrl2

Generated by: LCOV version 1.13