LCOV - code coverage report
Current view: top level - data/source/detail/rewrite - jitty.cpp (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 273 296 92.2 %
Date: 2020-02-28 00:44:21 Functions: 19 20 95.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/jitty.h"
      11             : #include "mcrl2/data/detail/rewrite/jitty_jittyc.h"
      12             : 
      13             : #define NAME std::string("rewr_jitty")
      14             : 
      15             : #include <boost/config.hpp>
      16             : 
      17             : #include "mcrl2/data/substitutions/mutable_map_substitution.h"
      18             : #include "mcrl2/data/replace.h"
      19             : 
      20             : #ifdef MCRL2_DISPLAY_REWRITE_STATISTICS
      21             : #include "mcrl2/data/detail/rewrite_statistics.h"
      22             : #endif
      23             : 
      24             : using namespace mcrl2::log;
      25             : using namespace mcrl2::core;
      26             : using namespace mcrl2::core::detail;
      27             : 
      28             : namespace mcrl2
      29             : {
      30             : namespace data
      31             : {
      32             : namespace detail
      33             : {
      34             : 
      35             : 
      36             : typedef atermpp::detail::_aterm* unprotected_variable;           // Variable that is not protected (so a copy should exist at some other place)
      37             : typedef atermpp::detail::_aterm* unprotected_data_expression;    // Idem, but now a data expression.
      38             : 
      39             : struct jitty_variable_assignment_for_a_rewrite_rule
      40             : {
      41             :   unprotected_variable var;
      42             :   unprotected_data_expression term;
      43             :   bool variable_is_a_normal_form;
      44             : };
      45             : 
      46             : struct jitty_assignments_for_a_rewrite_rule
      47             : {
      48             :   std::size_t size;
      49             :   jitty_variable_assignment_for_a_rewrite_rule* assignment;
      50             : 
      51      907215 :   jitty_assignments_for_a_rewrite_rule(jitty_variable_assignment_for_a_rewrite_rule* a)
      52      907215 :    : size(0),
      53      907215 :      assignment(a)
      54      907215 :   {}
      55             : 
      56             : };
      57             : 
      58             : 
      59             : // The function symbol below is used to administrate that a term is in normal form. It is put around a term.
      60             : // Terms with this auxiliary function symbol cannot be printed using the pretty printer for data expressions.
      61             : 
      62             : 
      63     9137631 : static const function_symbol& this_term_is_in_normal_form()
      64             : {
      65             :   static const function_symbol this_term_is_in_normal_form(
      66         112 :                          std::string("Rewritten@@term"),
      67     9137743 :                          function_sort({ untyped_sort() },untyped_sort()));
      68     9137631 :   return this_term_is_in_normal_form;
      69             : }
      70             : 
      71             : // The function below is intended to remove the auxiliary function this_term_is_in_normal_form from a term
      72             : // such that it can for instance be pretty printed.
      73             : 
      74     3449444 : data_expression remove_normal_form_function(const data_expression& t)
      75             : {
      76     3449444 :   if (is_variable(t))
      77             :   {
      78      130892 :     return t;
      79             :   }
      80             : 
      81     3318552 :   if (is_function_symbol(t))
      82             :   {
      83     2419743 :     assert(t!=this_term_is_in_normal_form());
      84     2419743 :     return t;
      85             :   }
      86             : 
      87      898809 :   if (is_application(t))
      88             :   {
      89      888952 :     const application& ta=atermpp::down_cast<application>(t);
      90      888952 :     if (ta.head()==this_term_is_in_normal_form())
      91             :     {
      92           0 :       assert(ta.size()==1);
      93           0 :       return ta[0];
      94             :     }
      95             : 
      96      888952 :     return application(remove_normal_form_function(ta.head()),ta.begin(),ta.end(),remove_normal_form_function);
      97             :   }
      98             : 
      99             : 
     100        9857 :   if (is_where_clause(t))
     101             :   {
     102           0 :     const where_clause& t1=atermpp::down_cast<where_clause>(t);
     103           0 :     const assignment_expression_list& assignments=t1.declarations();
     104           0 :     const data_expression& body=t1.body();
     105             : 
     106           0 :     assignment_vector new_assignments;
     107           0 :     for(const assignment_expression& ae: assignments)
     108             :     {
     109           0 :       const assignment& assignment_expr = atermpp::down_cast<assignment>(ae);
     110           0 :       new_assignments.push_back(assignment(assignment_expr.lhs(), remove_normal_form_function(assignment_expr.rhs())));
     111             :     }
     112           0 :     return where_clause(remove_normal_form_function(body),assignment_list(new_assignments.begin(),new_assignments.end()));
     113             :   }
     114             : 
     115        9857 :   assert(is_abstraction(t));
     116             : 
     117        9857 :   const abstraction& t1=atermpp::down_cast<abstraction>(t);
     118        9857 :   const binder_type& binder=t1.binding_operator();
     119        9857 :   const variable_list& bound_variables=t1.variables();
     120        9857 :   const data_expression& body=t1.body();
     121             : 
     122        9857 :   return abstraction(binder, bound_variables, remove_normal_form_function(body));
     123             : }
     124             : 
     125             : class jitty_argument_rewriter
     126             : {
     127             :   protected:
     128             :     mutable_indexed_substitution<>& m_sigma;
     129             :     RewriterJitty& m_r;
     130             :   public:
     131          20 :     jitty_argument_rewriter(mutable_indexed_substitution<>& sigma, RewriterJitty& r)
     132          20 :      : m_sigma(sigma), m_r(r)
     133          20 :     {}
     134             : 
     135          44 :   data_expression operator()(const data_expression& t)
     136             :   {
     137          44 :     return m_r.rewrite(t, m_sigma);
     138             :   }
     139             : };
     140             : 
     141             : 
     142     2652716 : void RewriterJitty::make_jitty_strat_sufficiently_larger(const std::size_t i)
     143             : {
     144     2652716 :   if (i>=jitty_strat.size())
     145             :   {
     146      223497 :     jitty_strat.resize(i+1);
     147             :   }
     148     2652716 : }
     149             : 
     150        1920 : void RewriterJitty::rebuild_strategy()
     151             : {
     152        1920 :   jitty_strat.clear();
     153      225924 :   for(std::map< function_symbol, data_equation_list >::const_iterator l=jitty_eqns.begin(); l!=jitty_eqns.end(); ++l)
     154             :   {
     155      224004 :     const std::size_t i=core::index_traits<data::function_symbol, function_symbol_key_type, 2>::index(l->first);
     156      224004 :     make_jitty_strat_sufficiently_larger(i);
     157      224004 :     jitty_strat[i] = create_strategy(reverse(l->second));
     158             :   }
     159        1920 : }
     160             : 
     161        1920 : RewriterJitty::RewriterJitty(
     162             :            const data_specification& data_spec,
     163        1920 :            const mcrl2::data::used_data_equation_selector& equation_selector):
     164        1920 :         Rewriter(data_spec,equation_selector)
     165             : {
     166      561146 :   for (const data_equation& eq: data_spec.equations())
     167             :   {
     168      559226 :     if (equation_selector(eq))
     169             :     {
     170             :       try
     171             :       {
     172      529088 :         CheckRewriteRule(eq);
     173             :       }
     174           0 :       catch (std::runtime_error& e)
     175             :       {
     176           0 :         mCRL2log(warning) << e.what() << std::endl;
     177           0 :         continue;
     178             :       }
     179             : 
     180      529088 :       const function_symbol& lhs_head_index=atermpp::down_cast<function_symbol>(get_nested_head(eq.lhs()));
     181             : 
     182     1058176 :       data_equation_list n;
     183      529088 :       std::map< function_symbol, data_equation_list >::iterator it = jitty_eqns.find(lhs_head_index);
     184      529088 :       if (it != jitty_eqns.end())
     185             :       {
     186      305084 :         n = it->second;
     187             :       }
     188      529088 :       n.push_front(eq);
     189      529088 :       jitty_eqns[lhs_head_index] = n;
     190             :     }
     191             :   }
     192             : 
     193        1920 :   rebuild_strategy();
     194        1920 : }
     195             : 
     196        3836 : RewriterJitty::~RewriterJitty()
     197             : {
     198        3836 : }
     199             : 
     200     3549518 : static data_expression subst_values(
     201             :             const jitty_assignments_for_a_rewrite_rule& assignments,
     202             :             const data_expression& t,
     203             :             data::enumerator_identifier_generator& generator) // This generator is used for the generation of fresh variable names.
     204             : {
     205     3549518 :   if (is_function_symbol(t))
     206             :   {
     207     1343910 :     return t;
     208             :   }
     209     2205608 :   else if (is_variable(t))
     210             :   {
     211     2119507 :     for (std::size_t i=0; i<assignments.size; i++)
     212             :     {
     213     2117653 :       if (atermpp::detail::address(t)==assignments.assignment[i].var)
     214             :       {
     215     1176499 :         if (assignments.assignment[i].variable_is_a_normal_form)
     216             :         {
     217             :           // Variables that are in normal form get a tag that they are in normal form.
     218      916936 :           return application(this_term_is_in_normal_form(),atermpp::down_cast<data_expression>(atermpp::aterm(assignments.assignment[i].term)));  
     219             :         }
     220      259563 :         return atermpp::down_cast<data_expression>(atermpp::aterm(assignments.assignment[i].term));
     221             :       }
     222             :     }
     223        1854 :     return t;
     224             :   }
     225     1027255 :   else if (is_abstraction(t))
     226             :   {
     227         852 :     const abstraction& t1=atermpp::down_cast<abstraction>(t);
     228         852 :     const binder_type& binder=t1.binding_operator();
     229         852 :     const variable_list& bound_variables=t1.variables();
     230             :     // Check that variables in the left and right hand sides of equations do not clash with bound variables.
     231        1704 :     std::set<variable> variables_in_substitution;
     232        2645 :     for(std::size_t i=0; i<assignments.size; ++i)
     233             :     {
     234        3586 :       std::set<variable> s=find_free_variables(atermpp::down_cast<data_expression>(atermpp::aterm(assignments.assignment[i].term)));
     235        1793 :       variables_in_substitution.insert(s.begin(),s.end());
     236        1793 :       variables_in_substitution.insert(atermpp::down_cast<variable>(atermpp::aterm(assignments.assignment[i].var)));
     237             :     }
     238             : 
     239        1704 :     variable_vector new_variables;
     240        1704 :     mutable_map_substitution<> sigma;
     241         852 :     bool sigma_trivial=true;
     242        1710 :     for(const variable& v: bound_variables)
     243             :     {
     244         858 :       if (variables_in_substitution.count(v)>0)
     245             :       {
     246             :         // Replace v in the list and in the body by a new variable name.
     247           2 :         const variable fresh_variable(generator(),v.sort());
     248           1 :         new_variables.push_back(fresh_variable);
     249           1 :         sigma[v]=fresh_variable;
     250           1 :         sigma_trivial=false;
     251             :       }
     252             :       else
     253             :       {
     254         857 :         new_variables.push_back(v);
     255             :       }
     256             :     }
     257        1704 :     return abstraction(binder,
     258        1704 :                        variable_list(new_variables.begin(),new_variables.end()),
     259        1704 :                        subst_values(assignments,
     260        1704 :                                     (sigma_trivial?t1.body():replace_variables(t1.body(),sigma)),
     261         852 :                                     generator));
     262             :   }
     263     1026403 :   else if (is_where_clause(t))
     264             :   {
     265          44 :     const where_clause& t1=atermpp::down_cast<where_clause>(t);
     266          44 :     const assignment_expression_list& local_assignments=t1.declarations();
     267          44 :     const data_expression& body=t1.body();
     268             : 
     269             : #ifndef NDEBUG
     270             :     // Check that variables in right hand sides of equations do not clash with bound variables.
     271         124 :     for(std::size_t i=0; i<assignments.size; ++i)
     272             :     {
     273         160 :       for(const assignment_expression& a: local_assignments)
     274             :       {
     275          80 :         assert(a[0]!= atermpp::aterm(assignments.assignment[i].var));
     276             :       }
     277             :     }
     278             : #endif
     279             : 
     280          88 :     assignment_vector new_assignments;
     281             : 
     282          88 :     for(const assignment_expression& a: local_assignments)
     283             :     {
     284          44 :       const assignment& assignment_expr = atermpp::down_cast<assignment>(a);
     285          44 :       new_assignments.push_back(assignment(assignment_expr.lhs(), subst_values(assignments,assignment_expr.rhs(),generator)));
     286             :     }
     287          44 :     return where_clause(subst_values(assignments,body,generator),assignment_list(new_assignments.begin(),new_assignments.end()));
     288             :   }
     289             :   else
     290             :   {
     291     1026359 :     const application& t1 = atermpp::down_cast<application>(t);
     292     3079077 :     return application(subst_values(assignments,
     293             :                                     t1.head(),
     294             :                                     generator),
     295     2052718 :                        t1.begin(),
     296     2052718 :                        t1.end(),
     297     2733835 :                        [&](const data_expression& t){ return subst_values(assignments,t,generator);});
     298             :   }
     299             : }
     300             : 
     301             : // Match term t with the lhs p of an equation.
     302     5209053 : static bool match_jitty(
     303             :                     const data_expression& t,
     304             :                     const data_expression& p,
     305             :                     jitty_assignments_for_a_rewrite_rule& assignments,
     306             :                     const bool term_context_guarantees_normal_form)
     307             : {
     308     5209053 :   if (is_function_symbol(p))
     309             :   {
     310     1975635 :     return p==t;
     311             :   }
     312     3233418 :   else if (is_variable(p))
     313             :   {
     314             : 
     315     2883625 :     for (std::size_t i=0; i<assignments.size; i++)
     316             :     {
     317     1127634 :       if (atermpp::detail::address(p)==assignments.assignment[i].var)
     318             :       {
     319      131619 :         return atermpp::detail::address(t)==assignments.assignment[i].term;
     320             :       }
     321             :     }
     322             : 
     323     1755991 :     assignments.assignment[assignments.size].var=atermpp::detail::address(p);
     324     1755991 :     assignments.assignment[assignments.size].term=atermpp::detail::address(t);
     325     1755991 :     assignments.assignment[assignments.size].variable_is_a_normal_form=term_context_guarantees_normal_form;
     326     1755991 :     assignments.size++;
     327     1755991 :     return true;
     328             :   }
     329             :   else
     330             :   {
     331     1345808 :     if (is_function_symbol(t) || is_variable(t) || is_abstraction(t) || is_where_clause(t))
     332             :     {
     333      492133 :       return false;
     334             :     }
     335             :     // p and t must be applications.
     336      853675 :     assert(term_context_guarantees_normal_form); // If the argument must match an expression it must be a normal form.
     337             : 
     338      853675 :     const application& pa=atermpp::down_cast<application>(p);
     339      853675 :     const application& ta=atermpp::down_cast<application>(t);
     340      853675 :     if (pa.size()!=ta.size()) // are p and t applications of the same arity?
     341             :     {
     342       43561 :       return false;
     343             :     }
     344             : 
     345             : 
     346      810114 :     if (!match_jitty(ta.head(),
     347             :                      pa.head(),assignments,true))
     348             :     {
     349       28111 :       return false;
     350             :     }
     351             : 
     352     1855904 :     for (std::size_t i=0; i<pa.size(); i++)
     353             :     {
     354     1093323 :       if (!match_jitty(ta[i], pa[i],assignments,true))
     355             :       {
     356       19422 :         return false;
     357             :       }
     358             :     }
     359             : 
     360      762581 :     return true;
     361             :   }
     362             : }
     363             : 
     364     3588388 : data_expression RewriterJitty::rewrite_aux(
     365             :                       const data_expression& term,
     366             :                       substitution_type& sigma)
     367             : {
     368     3588388 :   if (is_application(term))
     369             :   {
     370     2481715 :     const application& terma=atermpp::down_cast<application>(term);
     371     2481715 :     if (terma.head()==this_term_is_in_normal_form())
     372             :     {
     373      825160 :       assert(terma.size()==1);
     374      825160 :       assert(remove_normal_form_function(terma[0])==terma[0]);
     375      825160 :       return terma[0];
     376             :     }
     377             : 
     378             :     // The variable term has the shape appl(t,t1,...,tn);
     379             :   
     380             :     // First check whether t has the shape appl(appl...appl(f,u1,...,un)(...)(...) where f is a function symbol.
     381             :     // In this case rewrite that function symbol. This is an optimisation. If this does not apply t is rewritten,
     382             :     // including all its subterms. But this is costly, as not all subterms will be rewritten again
     383             :     // in rewrite_aux_function_symbol.
     384             :   
     385     1656555 :     const data_expression& head=get_nested_head(term);
     386             :   
     387     1656555 :     if (is_function_symbol(head) && head!=this_term_is_in_normal_form())
     388             :     {
     389     1650856 :       return rewrite_aux_function_symbol(atermpp::down_cast<function_symbol>(head),term,sigma);
     390             :     }
     391             :   
     392        5699 :     const application& tapp=atermpp::down_cast<application>(term);
     393             :     
     394       11398 :     const data_expression& t = rewrite_aux(tapp.head(),sigma);
     395             :     // Here t has the shape f(u1,....,un)(u1',...,um')....: f applied several times to arguments,
     396             :     // x(u1,....,un)(u1',...,um')....: x applied several times to arguments, or
     397             :     // binder x1,...,xn.t' where the binder is a lambda, exists or forall.
     398             :   
     399        5699 :     const data_expression& head1 = get_nested_head(t);
     400        5699 :     if (is_function_symbol(head1))
     401             :     {
     402             :       // In this case t has the shape f(u1...un)(u1'...um')....  where all u1,...,un,u1',...,um' are normal formas.
     403             :       // In the invocation of rewrite_aux_function_symbol these terms are rewritten to normalform again.
     404        1894 :       const data_expression& result=application(t,tapp.begin(), tapp.end()); 
     405         947 :       return rewrite_aux_function_symbol(atermpp::down_cast<function_symbol>(head1),result,sigma);
     406             :     }
     407        4752 :     else if (is_variable(head1))
     408             :     {
     409             :       // return appl(t,t1,...,tn) where t1,...,tn still need to be rewritten.
     410          20 :       jitty_argument_rewriter r(sigma,*this);
     411          20 :       return application(t,tapp.begin(),tapp.end(),r); // Replacing r by a lambda term requires 16 more bytes on the stack. 
     412             :     }
     413        4732 :     assert(is_abstraction(t));
     414        4732 :     const abstraction& ta=atermpp::down_cast<abstraction>(t);
     415        4732 :     const binder_type& binder(ta.binding_operator());
     416        4732 :     if (is_lambda_binder(binder))
     417             :     {
     418        4732 :       return rewrite_lambda_application(t,tapp,sigma);
     419             :     }
     420           0 :     if (is_exists_binder(binder))
     421             :     {
     422           0 :       assert(term.size()==1);
     423           0 :       return existential_quantifier_enumeration(t,sigma);
     424             :     }
     425           0 :     assert(is_forall_binder(binder));
     426           0 :     assert(term.size()==1);
     427           0 :     return universal_quantifier_enumeration(head1,sigma);
     428             :   }
     429             :   // Here term does not have the shape appl(t1,...,tn)
     430     1106673 :   if (is_function_symbol(term))
     431             :   {
     432      776909 :     assert(term!=this_term_is_in_normal_form());
     433      776909 :     return rewrite_aux_const_function_symbol(atermpp::down_cast<const function_symbol>(term),sigma);
     434             :   }
     435      329764 :   if (is_variable(term))
     436             :   {
     437      325229 :     return sigma(atermpp::down_cast<variable>(term));
     438             :   }
     439        4535 :   if (is_where_clause(term))
     440             :   {
     441          45 :     const where_clause& w = atermpp::down_cast<where_clause>(term);
     442          45 :     return rewrite_where(w,sigma);
     443             :   }
     444             : 
     445             :   { 
     446        4490 :     assert(is_abstraction(term));
     447        8980 :     const abstraction& ta(term);
     448        4490 :     if (is_exists(ta))
     449             :     {
     450          95 :       return existential_quantifier_enumeration(ta,sigma);
     451             :     }
     452        4395 :     if (is_forall(ta))
     453             :     {
     454         846 :       return universal_quantifier_enumeration(ta,sigma);
     455             :     }
     456        3549 :     assert(is_lambda(ta));
     457        3549 :     return rewrite_single_lambda(ta.variables(),ta.body(),false,sigma);
     458             :   }
     459             : }
     460             : 
     461     1651803 : data_expression RewriterJitty::rewrite_aux_function_symbol(
     462             :                       const function_symbol& op,
     463             :                       const data_expression& term,
     464             :                       substitution_type& sigma)
     465             : {
     466             :   // The first term is function symbol; apply the necessary rewrite rules using a jitty strategy.
     467             : 
     468     1651803 :   const std::size_t arity=(is_function_symbol(term)?0:detail::recursive_number_of_args(term));
     469             : 
     470     1651803 :   data_expression* rewritten = MCRL2_SPECIFIC_STACK_ALLOCATOR(data_expression, arity);
     471     1651803 :   bool* rewritten_defined = MCRL2_SPECIFIC_STACK_ALLOCATOR(bool, arity);
     472             : 
     473     4468959 :   for(std::size_t i=0; i<arity; ++i)
     474             :   {
     475     2817156 :     rewritten_defined[i]=false;
     476             :   }
     477             : 
     478     1651803 :   const std::size_t op_value=core::index_traits<data::function_symbol,function_symbol_key_type, 2>::index(op);
     479     1651803 :   make_jitty_strat_sufficiently_larger(op_value);
     480     1651803 :   const strategy& strat=jitty_strat[op_value];
     481             : 
     482     1651803 :   if (!strat.rules().empty())
     483             :   {
     484      907215 :     jitty_assignments_for_a_rewrite_rule assignments(MCRL2_SPECIFIC_STACK_ALLOCATOR(jitty_variable_assignment_for_a_rewrite_rule, strat.number_of_variables()));
     485             : 
     486     3656163 :     for (const strategy_rule& rule : strat.rules())
     487             :     {
     488     3548806 :       if (rule.is_rewrite_index())
     489             :       {
     490     1425095 :         const std::size_t i = rule.rewrite_index();
     491     1425095 :         if (i < arity)
     492             :         {
     493     1424897 :           assert(!rewritten_defined[i]||i==0);
     494     1424897 :           if (!rewritten_defined[i])
     495             :           {
     496     1424897 :             new (&rewritten[i]) data_expression(rewrite_aux(detail::get_argument_of_higher_order_term(atermpp::down_cast<application>(term),i),sigma));
     497     1424897 :             rewritten_defined[i]=true;
     498             :           }
     499     1424897 :           assert(rewritten[i].defined());
     500             :         }
     501             :         else
     502             :         {
     503         198 :           break;
     504             :         }
     505             :       }
     506             :       else
     507             :       {
     508     2123711 :         const data_equation& rule1=rule.equation();
     509     2123711 :         const data_expression& lhs=rule1.lhs();
     510     2123711 :         std::size_t rule_arity = (is_function_symbol(lhs)?0:detail::recursive_number_of_args(lhs));
     511             : 
     512     2123711 :         if (rule_arity > arity)
     513             :         {
     514           0 :           break;
     515             :         }
     516             : 
     517     2123711 :         assert(assignments.size==0);
     518             : 
     519     2123711 :         bool matches = true;
     520     4114571 :         for (std::size_t i=0; i<rule_arity; i++)
     521             :         {
     522     3305616 :           assert(i<arity);
     523     3305616 :           if (!match_jitty(rewritten_defined[i]?rewritten[i]:detail::get_argument_of_higher_order_term(atermpp::down_cast<application>(term),i),
     524             :                            detail::get_argument_of_higher_order_term(atermpp::down_cast<application>(lhs),i),
     525     3305616 :                            assignments,rewritten_defined[i]))
     526             :           {
     527     1314756 :             matches = false;
     528     1314756 :             break;
     529             :           }
     530             :         }
     531     2123711 :         if (matches)
     532             :         {
     533     1648076 :           if (rule1.condition()==sort_bool::true_() || rewrite_aux(
     534      839121 :                    subst_values(assignments,rule1.condition(),m_generator),sigma)==sort_bool::true_())
     535             :           {
     536      799660 :             const data_expression& rhs=rule1.rhs();
     537             : 
     538      799660 :             if (arity == rule_arity)
     539             :             {
     540     1599258 :               const data_expression& result=rewrite_aux(subst_values(assignments,rhs,m_generator),sigma);
     541     2389819 :               for (std::size_t i=0; i<arity; i++)
     542             :               {
     543     1590190 :                 if (rewritten_defined[i])
     544             :                 {
     545     1211346 :                   rewritten[i].~data_expression();
     546             :                 }
     547             :               }
     548      799629 :               return result;
     549             :             }
     550             :             else
     551             :             {
     552             : 
     553          31 :               assert(arity>rule_arity);
     554             :               // There are more arguments than those that have been rewritten.
     555             :               // Get those, put them in rewritten.
     556             : 
     557          62 :               data_expression result=subst_values(assignments,rhs,m_generator);
     558             : 
     559          62 :               for(std::size_t i=rule_arity; i<arity; ++i)
     560             :               {
     561          31 :                 if (rewritten_defined[i])
     562             :                 {
     563           0 :                   rewritten[i]=detail::get_argument_of_higher_order_term(atermpp::down_cast<application>(term),i);
     564             :                 }
     565             :                 else
     566             :                 {
     567          31 :                   new (&rewritten[i]) data_expression(detail::get_argument_of_higher_order_term(atermpp::down_cast<application>(term),i));
     568          31 :                   rewritten_defined[i]=true;
     569             :                 }
     570             :               }
     571          31 :               std::size_t i = rule_arity;
     572          62 :               sort_expression sort = detail::residual_sort(op.sort(),i);
     573          93 :               while (is_function_sort(sort) && (i < arity))
     574             :               {
     575          31 :                 const function_sort& fsort =  atermpp::down_cast<function_sort>(sort);
     576          31 :                 const std::size_t end=i+fsort.domain().size();
     577          31 :                 assert(end-1<arity);
     578          31 :                 result = application(result,&rewritten[0]+i,&rewritten[0]+end);
     579          31 :                 i=end;
     580          31 :                 sort = fsort.codomain();
     581             :               }
     582             : 
     583         116 :               for (std::size_t i=0; i<arity; ++i)
     584             :               {
     585          85 :                 if (rewritten_defined[i])
     586             :                 {
     587          31 :                   rewritten[i].~data_expression();
     588             :                 }
     589             :               }
     590          31 :               return rewrite_aux(result,sigma);
     591             :             }
     592             :           }
     593             :         }
     594     1324051 :         assignments.size=0;
     595             :       }
     596             :     }
     597             :   }
     598             : 
     599             :   // No rewrite rule is applicable. Rewrite the not yet rewritten arguments.
     600             :   // As we rewrite all, we do not record anymore whether terms are rewritten.
     601             : 
     602     2079024 :   for (std::size_t i=0; i<arity; i++)
     603             :   {
     604     1226881 :     if (!rewritten_defined[i])
     605             :     {
     606     1013330 :       new (&rewritten[i]) data_expression(rewrite_aux(detail::get_argument_of_higher_order_term(atermpp::down_cast<application>(term),i),sigma));
     607             :     }
     608             :   }
     609             : 
     610             :   //Construct this potential higher order term.
     611     1704286 :   data_expression result=op;
     612      852143 :   std::size_t i = 0;
     613     1704286 :   sort_expression sort = op.sort();
     614     2556663 :   while (is_function_sort(sort) && (i < arity))
     615             :   {
     616      852260 :     const function_sort& fsort=atermpp::down_cast<function_sort>(sort);
     617      852260 :     const std::size_t end=i+fsort.domain().size();
     618      852260 :     assert(end-1<arity);
     619      852260 :     result = application(result,&rewritten[0]+i,&rewritten[0]+end);
     620      852260 :     i=end;
     621      852260 :     sort = fsort.codomain();
     622             :   }
     623             : 
     624     2079024 :   for (std::size_t i=0; i<arity; i++)
     625             :   {
     626     1226881 :     rewritten[i].~data_expression();
     627             :   } 
     628      852143 :   return result; 
     629             : }
     630             : 
     631      776909 : data_expression RewriterJitty::rewrite_aux_const_function_symbol(
     632             :                       const function_symbol& op,
     633             :                       substitution_type& sigma)
     634             : {
     635             :   // This is special code to rewrite a function symbol. Note that the function symbol can be higher order,
     636             :   // e.g., it can be a function symbol f for which a rewrite rule f(n)=... exists. 
     637             : 
     638      776909 :   const std::size_t op_value=core::index_traits<data::function_symbol,function_symbol_key_type, 2>::index(op);
     639      776909 :   make_jitty_strat_sufficiently_larger(op_value);
     640      776909 :   const strategy& strat=jitty_strat[op_value];
     641             : 
     642      776909 :   for (const strategy_rule& rule : strat.rules())
     643             :   {
     644         928 :     if (rule.is_rewrite_index())
     645             :     {
     646         162 :       break;
     647             :     }
     648             :     else
     649             :     {
     650         766 :       const data_equation& rule1=rule.equation();
     651         766 :       const data_expression& lhs=rule1.lhs();
     652         766 :       std::size_t rule_arity = (is_function_symbol(lhs)?0:detail::recursive_number_of_args(lhs));
     653             : 
     654         766 :       if (rule_arity > 0)
     655             :       {
     656         685 :         break;
     657             :       }
     658             : 
     659          81 :       if (rule1.condition()==sort_bool::true_() || rewrite_aux(rule1.condition(),sigma)==sort_bool::true_())
     660             :       {
     661         162 :         return rewrite_aux(rule1.rhs(),sigma);
     662             :       }
     663             :     }
     664             :   }
     665             : 
     666      776828 :   return op; 
     667             : }
     668             : 
     669             : 
     670      329638 : data_expression RewriterJitty::rewrite(
     671             :      const data_expression& term,
     672             :      substitution_type& sigma)
     673             : {
     674             : #ifdef MCRL2_DISPLAY_REWRITE_STATISTICS
     675             :   data::detail::increment_rewrite_count();
     676             : #endif
     677      659276 :   const data_expression& t=rewrite_aux(term, sigma);
     678      329638 :   assert(remove_normal_form_function(t)==t);
     679      659276 :   return t;
     680             : }
     681             : 
     682           0 : rewrite_strategy RewriterJitty::getStrategy()
     683             : {
     684           0 :   return jitty;
     685             : }
     686             : }
     687             : }
     688         366 : }

Generated by: LCOV version 1.13