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 : #define NAME std::string("rewr_jitty")
11 :
12 : #include "mcrl2/data/detail/rewrite/jitty.h"
13 : #include "mcrl2/data/detail/rewrite/jitty_jittyc.h"
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 : // The function below is intended to remove the auxiliary function this_term_is_in_normal_form from a term
36 : // such that it can for instance be pretty printed.
37 :
38 2912077 : data_expression RewriterJitty::remove_normal_form_function(const data_expression& t)
39 : {
40 2912077 : if (is_variable(t))
41 : {
42 378708 : return t;
43 : }
44 :
45 2533369 : if (is_function_symbol(t))
46 : {
47 1737298 : assert(t!=this_term_is_in_normal_form());
48 1737298 : return t;
49 : }
50 :
51 796071 : if (is_application(t))
52 : {
53 790791 : const application& ta=atermpp::down_cast<application>(t);
54 790791 : if (ta.head()==this_term_is_in_normal_form())
55 : {
56 0 : assert(ta.size()==1);
57 0 : return ta[0];
58 : }
59 :
60 3069357 : return application(ta.head(), ta.begin(), ta.end(), [&](const data_expression& t){ return remove_normal_form_function(t); });
61 : }
62 :
63 :
64 5280 : if (is_where_clause(t))
65 : {
66 0 : const where_clause& t1=atermpp::down_cast<where_clause>(t);
67 0 : const assignment_expression_list& assignments=t1.declarations();
68 0 : const data_expression& body=t1.body();
69 :
70 0 : assignment_vector new_assignments;
71 0 : for(const assignment_expression& ae: assignments)
72 : {
73 0 : const assignment& assignment_expr = atermpp::down_cast<assignment>(ae);
74 0 : new_assignments.push_back(assignment(assignment_expr.lhs(), remove_normal_form_function(assignment_expr.rhs())));
75 : }
76 0 : return where_clause(remove_normal_form_function(body),assignment_list(new_assignments.begin(),new_assignments.end()));
77 0 : }
78 :
79 5280 : assert(is_abstraction(t));
80 :
81 5280 : const abstraction& t1=atermpp::down_cast<abstraction>(t);
82 5280 : const binder_type& binder=t1.binding_operator();
83 5280 : const variable_list& bound_variables=t1.variables();
84 5280 : const data_expression& body=t1.body();
85 :
86 5280 : return abstraction(binder, bound_variables, remove_normal_form_function(body));
87 : }
88 :
89 : class jitty_argument_rewriter
90 : {
91 : protected:
92 : mutable_indexed_substitution<>& m_sigma;
93 : RewriterJitty& m_r;
94 : public:
95 10 : jitty_argument_rewriter(mutable_indexed_substitution<>& sigma, RewriterJitty& r)
96 10 : : m_sigma(sigma), m_r(r)
97 10 : {}
98 :
99 32 : void operator()(data_expression& result, const data_expression& t)
100 : {
101 32 : m_r.rewrite_aux(result, t, m_sigma);
102 32 : }
103 : };
104 :
105 : class dependencies_rewrite_rule_pair
106 : {
107 : protected:
108 : std::set<std::size_t> m_dependencies;
109 : data_equation m_equation;
110 :
111 : public:
112 : dependencies_rewrite_rule_pair(std::set<std::size_t>& dependencies, const data_equation& eq)
113 : : m_dependencies(dependencies), m_equation(eq)
114 : {}
115 :
116 : const std::set<std::size_t>& dependencies() const
117 : {
118 : return m_dependencies;
119 : }
120 :
121 : const data_equation equation() const
122 : {
123 : return m_equation;
124 : }
125 : };
126 :
127 :
128 :
129 :
130 :
131 2124110 : void RewriterJitty::make_jitty_strat_sufficiently_larger(const std::size_t i)
132 : {
133 2124110 : if (i>=jitty_strat.size())
134 : {
135 73923 : jitty_strat.resize(i+1);
136 : }
137 2124110 : }
138 :
139 1801 : void RewriterJitty::rebuild_strategy(const data_specification& data_spec, const mcrl2::data::used_data_equation_selector& equation_selector)
140 : {
141 1801 : jitty_strat.clear();
142 1801 : function_symbol_vector function_symbols=data_spec.constructors();
143 1801 : function_symbols.insert(function_symbols.end(), data_spec.mappings().begin(), data_spec.mappings().end());
144 276572 : for(const function_symbol& f: function_symbols)
145 : {
146 274771 : if (equation_selector(f))
147 : {
148 273423 : const std::size_t i=atermpp::detail::index_traits<data::function_symbol, function_symbol_key_type, 2>::index(f);
149 273423 : make_jitty_strat_sufficiently_larger(i);
150 273423 : std::map< function_symbol, data_equation_list >::const_iterator j=jitty_eqns.find(f);
151 273423 : jitty_strat[i] =
152 273423 : (j==jitty_eqns.end()
153 1070182 : ?create_strategy(f,data_equation_list(), data_spec)
154 796759 : :create_strategy(f,reverse(j->second), data_spec));
155 : }
156 : }
157 :
158 1801 : }
159 :
160 :
161 1801 : RewriterJitty::RewriterJitty(
162 : const data_specification& data_spec,
163 1801 : const mcrl2::data::used_data_equation_selector& equation_selector):
164 : Rewriter(data_spec,equation_selector),
165 1801 : this_term_is_in_normal_form_symbol(
166 3602 : std::string("Rewritten@@term"),
167 5403 : function_sort({ untyped_sort() },untyped_sort())),
168 3602 : rewriting_in_progress(false)
169 : {
170 1801 : thread_initialise();
171 587692 : for (const data_equation& eq: data_spec.equations())
172 : {
173 585891 : if (equation_selector(eq))
174 : {
175 : try
176 : {
177 582881 : CheckRewriteRule(eq);
178 : }
179 0 : catch (std::runtime_error& e)
180 : {
181 0 : mCRL2log(warning) << e.what() << std::endl;
182 0 : continue;
183 0 : }
184 :
185 582881 : const function_symbol& lhs_head_index=atermpp::down_cast<function_symbol>(get_nested_head(eq.lhs()));
186 :
187 582881 : data_equation_list n;
188 582881 : std::map< function_symbol, data_equation_list >::iterator it = jitty_eqns.find(lhs_head_index);
189 582881 : if (it != jitty_eqns.end())
190 : {
191 332968 : n = it->second;
192 : }
193 582881 : n.push_front(eq);
194 582881 : jitty_eqns[lhs_head_index] = n;
195 582881 : }
196 : }
197 :
198 1801 : rebuild_strategy(data_spec, equation_selector);
199 1801 : }
200 :
201 3597 : RewriterJitty::~RewriterJitty()
202 : {
203 3597 : }
204 :
205 1304878 : void RewriterJitty::subst_values(
206 : data_expression& result,
207 : const jitty_assignments_for_a_rewrite_rule& assignments,
208 : const data_expression& t,
209 : data::enumerator_identifier_generator& generator) // This generator is used for the generation of fresh variable names.
210 : {
211 1304878 : if (is_function_symbol(t))
212 : {
213 : // result=t; The following is more efficient as it avoids a call to thread local variables. Should be removed in due time.
214 525472 : result.assign(t, *m_thread_aterm_pool);
215 525472 : return;
216 : }
217 779406 : else if (is_variable(t))
218 : {
219 812235 : for (std::size_t i=0; i<assignments.size; i++)
220 : {
221 811195 : if (t==assignments.assignment[i].var)
222 : {
223 434024 : if (assignments.assignment[i].variable_is_a_normal_form)
224 : {
225 : // Variables that are in normal form get a tag that they are in normal form.
226 324982 : make_application(result,this_term_is_in_normal_form(),assignments.assignment[i].term);
227 324982 : return;
228 : }
229 : // result=assignments.assignment[i].term;
230 109042 : result.assign(assignments.assignment[i].term,
231 109042 : *m_thread_aterm_pool);
232 109042 : return;
233 : }
234 : }
235 : // result=t;
236 1040 : result.assign(t, *m_thread_aterm_pool);
237 1040 : return;
238 : }
239 344342 : else if (is_abstraction(t))
240 : {
241 457 : const abstraction& t1=atermpp::down_cast<abstraction>(t);
242 457 : const binder_type& binder=t1.binding_operator();
243 457 : const variable_list& bound_variables=t1.variables();
244 : // Check that variables in the left and right hand sides of equations do not clash with bound variables.
245 457 : std::set<variable> variables_in_substitution;
246 1436 : for(std::size_t i=0; i<assignments.size; ++i)
247 : {
248 979 : std::set<variable> s=find_free_variables(assignments.assignment[i].term);
249 979 : variables_in_substitution.insert(s.begin(),s.end());
250 979 : variables_in_substitution.insert(assignments.assignment[i].var);
251 979 : }
252 :
253 457 : variable_vector new_variables;
254 457 : mutable_map_substitution<> sigma;
255 457 : bool sigma_trivial=true;
256 920 : for(const variable& v: bound_variables)
257 : {
258 463 : if (variables_in_substitution.count(v)>0)
259 : {
260 : // Replace v in the list and in the body by a new variable name.
261 1 : const variable fresh_variable(generator(),v.sort());
262 1 : new_variables.push_back(fresh_variable);
263 1 : sigma[v]=fresh_variable;
264 1 : sigma_trivial=false;
265 1 : }
266 : else
267 : {
268 462 : new_variables.push_back(v);
269 : }
270 : }
271 457 : subst_values(result,
272 : assignments,
273 914 : (sigma_trivial?t1.body():replace_variables(t1.body(),sigma)),
274 : generator);
275 914 : result=abstraction(binder,
276 914 : variable_list(new_variables.begin(),new_variables.end()),
277 457 : result);
278 457 : return;
279 457 : }
280 343885 : else if (is_where_clause(t))
281 : {
282 44 : const where_clause& t1=atermpp::down_cast<where_clause>(t);
283 44 : const assignment_expression_list& local_assignments=t1.declarations();
284 44 : const data_expression& body=t1.body();
285 :
286 : #ifndef NDEBUG
287 : // Check that variables in right hand sides of equations do not clash with bound variables.
288 124 : for(std::size_t i=0; i<assignments.size; ++i)
289 : {
290 160 : for(const assignment_expression& a: local_assignments)
291 : {
292 80 : assert(a[0]!= assignments.assignment[i].var);
293 : }
294 : }
295 : #endif
296 :
297 44 : assignment_vector new_assignments;
298 :
299 88 : for(const assignment_expression& a: local_assignments)
300 : {
301 44 : const assignment& assignment_expr = atermpp::down_cast<assignment>(a);
302 44 : subst_values(result,assignments,assignment_expr.rhs(),generator);
303 44 : new_assignments.push_back(assignment(assignment_expr.lhs(),result));
304 : }
305 44 : subst_values(result,assignments,body,generator),
306 44 : result=where_clause(result, assignment_list(new_assignments.begin(),new_assignments.end()));
307 44 : return;
308 44 : }
309 : else
310 : {
311 343841 : const application& t1 = atermpp::down_cast<application>(t);
312 343841 : make_application(result,
313 : t1.head(),
314 343841 : t1.begin(),
315 687682 : t1.end(),
316 933141 : [&](data_expression& result, const data_expression& t) -> void
317 933141 : { subst_values(result,assignments,t,generator); return;});
318 : }
319 : }
320 :
321 : // Match term t with the lhs p of an equation.
322 4691347 : static bool match_jitty(
323 : const data_expression& t,
324 : const data_expression& p,
325 : jitty_assignments_for_a_rewrite_rule& assignments,
326 : const bool term_context_guarantees_normal_form)
327 : {
328 4691347 : if (is_function_symbol(p))
329 : {
330 1748891 : return p==t;
331 : }
332 2942456 : else if (is_variable(p))
333 : {
334 :
335 1968949 : for (std::size_t i=0; i<assignments.size; i++)
336 : {
337 751724 : if (p==assignments.assignment[i].var)
338 : {
339 257827 : return t==assignments.assignment[i].term;
340 : }
341 : }
342 :
343 1217225 : new (&assignments.assignment[assignments.size])
344 : jitty_variable_assignment_for_a_rewrite_rule(
345 1217225 : atermpp::down_cast<variable>(p),
346 : t,
347 1217225 : term_context_guarantees_normal_form);
348 1217225 : assignments.size++;
349 1217225 : return true;
350 : }
351 : else
352 : {
353 1467404 : if (is_function_symbol(t) || is_variable(t) || is_abstraction(t) || is_where_clause(t))
354 : {
355 996029 : return false;
356 : }
357 : // p and t must be applications.
358 471375 : assert(term_context_guarantees_normal_form); // If the argument must match an expression it must be a normal form.
359 :
360 471375 : const application& pa=atermpp::down_cast<application>(p);
361 471375 : const application& ta=atermpp::down_cast<application>(t);
362 471375 : if (pa.size()!=ta.size()) // are p and t applications of the same arity?
363 : {
364 125925 : return false;
365 : }
366 :
367 :
368 345450 : if (!match_jitty(ta.head(),
369 : pa.head(),assignments,true))
370 : {
371 40394 : return false;
372 : }
373 :
374 787331 : for (std::size_t i=0; i<pa.size(); i++)
375 : {
376 499620 : if (!match_jitty(ta[i], pa[i],assignments,true))
377 : {
378 17345 : return false;
379 : }
380 : }
381 :
382 287711 : return true;
383 : }
384 : }
385 :
386 :
387 : // This function applies the rewrite_cpp_code on a higher order term t with op as head symbol for
388 : // which the code in rewrite_cpp_code must be applied.
389 : template <class ITERATOR>
390 24 : void RewriterJitty::apply_cpp_code_to_higher_order_term(
391 : data_expression& result,
392 : const application& t,
393 : const std::function<data_expression(const data_expression&)> rewrite_cpp_code,
394 : ITERATOR begin,
395 : ITERATOR end,
396 : substitution_type& sigma)
397 : {
398 24 : if (is_function_symbol(t.head()))
399 : {
400 12 : make_application(result, t.head(), begin, end);
401 12 : result=rewrite_cpp_code(result);
402 12 : return;
403 : }
404 :
405 12 : const application& ta=atermpp::down_cast<application>(t.head());
406 12 : std::size_t n_args=recursive_number_of_args(ta);
407 12 : apply_cpp_code_to_higher_order_term(result,ta,rewrite_cpp_code,begin,begin+n_args,sigma);
408 12 : const data_expression rewrite_result=result; /* TODO Optimize */
409 12 : rewrite_aux(result,application(rewrite_result,
410 : begin+n_args,
411 : end,
412 24 : [&](const data_expression& t){ return application(this_term_is_in_normal_form(),t); } ),
413 : sigma);
414 12 : }
415 :
416 :
417 : /// \brief Rewrite a term with a given substitution and put the rewritten term in result.
418 2619903 : void RewriterJitty::rewrite_aux(
419 : data_expression& result,
420 : const data_expression& term,
421 : substitution_type& sigma)
422 : {
423 2619903 : if (is_application(term))
424 : {
425 1412101 : const application& terma=atermpp::down_cast<application>(term);
426 1412101 : if (terma.head()==this_term_is_in_normal_form())
427 : {
428 283211 : assert(terma.size()==1);
429 283211 : assert(remove_normal_form_function(terma[0])==terma[0]);
430 : // result=terma[0]; the following is more efficient.
431 283211 : result.assign(terma[0], *m_thread_aterm_pool);
432 283211 : return;
433 : }
434 :
435 : // The variable term has the shape appl(t,t1,...,tn);
436 :
437 : // First check whether t has the shape appl(appl...appl(f,u1,...,un)(...)(...) where f is a function symbol.
438 : // In this case rewrite that function symbol. This is an optimisation. If this does not apply t is rewritten,
439 : // including all its subterms. But this is costly, as not all subterms will be rewritten again
440 : // in rewrite_aux_function_symbol.
441 :
442 1128890 : const data_expression& head=get_nested_head(term);
443 :
444 1128890 : if (is_function_symbol(head) && head!=this_term_is_in_normal_form())
445 : {
446 : // return rewrite_aux_function_symbol(atermpp::down_cast<function_symbol>(head),term,sigma);
447 1126118 : rewrite_aux_function_symbol(result, atermpp::down_cast<function_symbol>(head),terma,sigma);
448 1126080 : return;
449 : }
450 :
451 2772 : const application& tapp=atermpp::down_cast<application>(term);
452 :
453 : // const data_expression t = rewrite_aux(tapp.head(),sigma);
454 2772 : m_rewrite_stack.increase(2);
455 :
456 2772 : const std::size_t t = 0; // Index of variable t in the stack.
457 2772 : rewrite_aux(m_rewrite_stack.element(t,2),tapp.head(),sigma);
458 :
459 : // Here t has the shape f(u1,....,un)(u1',...,um')....: f applied several times to arguments,
460 : // x(u1,....,un)(u1',...,um')....: x applied several times to arguments, or
461 : // binder x1,...,xn.t' where the binder is a lambda, exists or forall.
462 :
463 2772 : const std::size_t head1 = 1; // Index of variable head1 in the stack.
464 2772 : m_rewrite_stack.element(head1,2) = get_nested_head(m_rewrite_stack.element(t,2));
465 2772 : if (is_function_symbol(m_rewrite_stack.element(head1,2)))
466 : {
467 : // In this case t (is top of the rewrite stack) has the shape f(u1...un)(u1'...um').... where all u1,...,un,u1',...,um' are normal formas.
468 : // In the invocation of rewrite_aux_function_symbol these terms are rewritten to normalform again.
469 352 : make_application(result, m_rewrite_stack.element(t,2) , tapp.begin(), tapp.end());
470 704 : rewrite_aux_function_symbol(m_rewrite_stack.element(t,2),
471 352 : atermpp::down_cast<function_symbol>(m_rewrite_stack.element(head1,2)),
472 : atermpp::down_cast<application>(result),
473 : sigma);
474 352 : result=m_rewrite_stack.element(t,2);
475 352 : m_rewrite_stack.decrease(2);
476 352 : return;
477 : }
478 2420 : else if (is_variable(m_rewrite_stack.element(head1,2)))
479 : {
480 : // return appl(t,t1,...,tn) where t1,...,tn still need to be rewritten.
481 10 : jitty_argument_rewriter r(sigma,*this);
482 10 : const bool do_not_rewrite_head=false;
483 10 : make_application(result, m_rewrite_stack.element(t,2) , tapp.begin(), tapp.end(), r, do_not_rewrite_head); // Replacing r by a lambda term requires 16 more bytes on the stack.
484 10 : m_rewrite_stack.decrease(2);
485 10 : return;
486 : }
487 2410 : assert(is_abstraction(m_rewrite_stack.top()));
488 2410 : const abstraction& ta=atermpp::down_cast<abstraction>(m_rewrite_stack.element(t,2) );
489 2410 : const binder_type& binder(ta.binding_operator());
490 2410 : if (is_lambda_binder(binder))
491 : {
492 2410 : rewrite_lambda_application(result,ta,tapp,sigma);
493 2410 : m_rewrite_stack.decrease(2);
494 2410 : return;
495 : }
496 0 : if (is_exists_binder(binder))
497 : {
498 0 : assert(term.size()==1);
499 0 : existential_quantifier_enumeration(result,ta,sigma);
500 0 : m_rewrite_stack.decrease(2);
501 0 : return;
502 : }
503 0 : assert(is_forall_binder(binder));
504 0 : assert(term.size()==1);
505 0 : universal_quantifier_enumeration(result,ta,sigma);
506 0 : m_rewrite_stack.decrease(2);
507 0 : return;
508 : }
509 : // Here term does not have the shape appl(t1,...,tn)
510 1207802 : if (is_function_symbol(term))
511 : {
512 724218 : assert(term!=this_term_is_in_normal_form());
513 724218 : rewrite_aux_const_function_symbol(result,atermpp::down_cast<const function_symbol>(term),sigma);
514 724218 : return;
515 : }
516 483584 : if (is_variable(term))
517 : {
518 480920 : sigma.apply(atermpp::down_cast<variable>(term),result, *m_thread_aterm_pool);
519 480920 : return;
520 : }
521 2664 : if (is_where_clause(term))
522 : {
523 45 : const where_clause& w = atermpp::down_cast<where_clause>(term);
524 45 : rewrite_where(result,w,sigma);
525 45 : return;
526 : }
527 :
528 : {
529 2619 : const abstraction& ta=atermpp::down_cast<abstraction>(term);
530 2619 : if (is_exists(ta))
531 : {
532 335 : existential_quantifier_enumeration(result,ta,sigma);
533 335 : return;
534 : }
535 2284 : if (is_forall(ta))
536 : {
537 451 : universal_quantifier_enumeration(result,ta,sigma);
538 451 : return;
539 : }
540 1833 : assert(is_lambda(ta));
541 1833 : rewrite_single_lambda(result,ta.variables(),ta.body(),false,sigma);
542 1833 : return;
543 : }
544 : }
545 :
546 1126470 : void RewriterJitty::rewrite_aux_function_symbol(
547 : data_expression& result,
548 : const function_symbol& op,
549 : const application& term,
550 : substitution_type& sigma)
551 : {
552 : // The first term is function symbol; apply the necessary rewrite rules using a jitty strategy.
553 1126470 : assert(is_function_sort(op.sort()));
554 :
555 1126470 : const std::size_t arity=detail::recursive_number_of_args(term);
556 1126470 : assert(arity>0);
557 : // data_expression* rewritten = MCRL2_SPECIFIC_STACK_ALLOCATOR(data_expression, arity);
558 1126470 : m_rewrite_stack.increase(arity+1);
559 1126469 : bool* rewritten_defined = MCRL2_SPECIFIC_STACK_ALLOCATOR(bool, arity);
560 :
561 3203943 : for(std::size_t i=0; i<arity; ++i)
562 : {
563 2077474 : rewritten_defined[i]=false;
564 : }
565 :
566 1126469 : const std::size_t op_value=atermpp::detail::index_traits<data::function_symbol,function_symbol_key_type, 2>::index(op);
567 1126469 : make_jitty_strat_sufficiently_larger(op_value);
568 1126469 : const strategy& strat=jitty_strat[op_value];
569 :
570 1126469 : if (!strat.rules().empty())
571 : {
572 : jitty_assignments_for_a_rewrite_rule assignments(
573 716056 : MCRL2_SPECIFIC_STACK_ALLOCATOR(jitty_variable_assignment_for_a_rewrite_rule, strat.number_of_variables()));
574 :
575 4454202 : for (const strategy_rule& rule : strat.rules())
576 : {
577 4089647 : if (rule.is_rewrite_index())
578 : {
579 1203328 : const std::size_t i = rule.rewrite_index();
580 1203328 : if (i < arity)
581 : {
582 1203112 : assert(!rewritten_defined[i]||i==0);
583 1203112 : if (!rewritten_defined[i])
584 : {
585 : // new (&rewritten[i]) data_expression(rewrite_aux(detail::get_argument_of_higher_order_term(term,i),sigma));
586 1203112 : rewrite_aux(m_rewrite_stack.element(i,arity+1),detail::get_argument_of_higher_order_term(term,i),sigma);
587 :
588 1203097 : rewritten_defined[i]=true;
589 : }
590 : // assert(rewritten[i].defined());
591 1203097 : assert(m_rewrite_stack.element(i,arity+1).defined());
592 : }
593 : else
594 : {
595 216 : break;
596 : }
597 : }
598 2886319 : else if (rule.is_cpp_code())
599 : {
600 : // Here it is assumed that precompiled code only works on the exact right number of arguments and
601 : // precompiled functions are not used in a higher order fashion. Maybe this requires an explicit check.
602 320 : assert(arity>0);
603 320 : if (term.head()==op)
604 : {
605 : // application rewriteable_term(op, &rewritten[0], &rewritten[arity]);
606 308 : assert(m_rewrite_stack.stack_size()>=arity+1);
607 : application rewriteable_term(op, m_rewrite_stack.stack_iterator(0,arity+1),
608 308 : m_rewrite_stack.stack_iterator(arity,arity+1)); /* TODO Optimize */
609 308 : result=rule.rewrite_cpp_code()(rewriteable_term);
610 308 : m_rewrite_stack.decrease(arity+1);
611 308 : return;
612 308 : }
613 : else
614 : {
615 : // Guarantee that all higher order arguments are in normal form. Maybe this had to be done in the strategy for higher
616 : // order terms.
617 60 : for(std::size_t i=0; i<recursive_number_of_args(term); i++)
618 : {
619 48 : if (!rewritten_defined[i])
620 : {
621 : // new (&rewritten[i]) data_expression(rewrite_aux(detail::get_argument_of_higher_order_term(term,i),sigma));
622 12 : rewrite_aux(m_rewrite_stack.element(i,arity+1),detail::get_argument_of_higher_order_term(term,i),sigma);
623 12 : rewritten_defined[i]=true;
624 : }
625 : }
626 : // return apply_cpp_code_to_higher_order_term(term, rule.rewrite_cpp_code(), &rewritten[0], &rewritten[arity], sigma);
627 24 : apply_cpp_code_to_higher_order_term(
628 : result,
629 : term,
630 24 : rule.rewrite_cpp_code(),
631 : m_rewrite_stack.stack_iterator(0,arity+1),
632 : m_rewrite_stack.stack_iterator(arity,arity+1), sigma);
633 12 : m_rewrite_stack.decrease(arity+1);
634 12 : return;
635 : }
636 : }
637 : else
638 : {
639 2885999 : const data_equation& rule1=rule.equation();
640 2885999 : const data_expression& lhs=rule1.lhs();
641 2885999 : std::size_t rule_arity = (is_function_symbol(lhs)?0:detail::recursive_number_of_args(lhs));
642 :
643 2885999 : if (rule_arity > arity)
644 : {
645 0 : break;
646 : }
647 :
648 2885999 : assert(assignments.size==0);
649 :
650 2885999 : bool matches = true;
651 4214157 : for (std::size_t i=0; i<rule_arity; i++)
652 : {
653 3846277 : assert(i<arity);
654 7692554 : if (!match_jitty(rewritten_defined[i]?
655 3614501 : m_rewrite_stack.element(i,arity+1):
656 231776 : detail::get_argument_of_higher_order_term(term,i),
657 : detail::get_argument_of_higher_order_term(atermpp::down_cast<application>(lhs),i),
658 3846277 : assignments,rewritten_defined[i]))
659 : {
660 2518119 : matches = false;
661 2518119 : break;
662 : }
663 : }
664 2885999 : if (matches)
665 : {
666 367880 : bool condition_of_this_rule=false;
667 367880 : if (rule1.condition()==sort_bool::true_())
668 : {
669 347638 : condition_of_this_rule=true;
670 : }
671 : else
672 : {
673 20242 : subst_values(m_rewrite_stack.top(),assignments,rule1.condition(),m_generator);
674 20242 : rewrite_aux(result, m_rewrite_stack.top(), sigma);
675 20242 : if (result==sort_bool::true_())
676 : {
677 3312 : condition_of_this_rule=true;
678 : }
679 : }
680 367880 : if (condition_of_this_rule)
681 : {
682 350950 : const data_expression& rhs=rule1.rhs();
683 :
684 350950 : if (arity == rule_arity)
685 : {
686 : // const data_expression result=rewrite_aux(subst_values(assignments,rhs,m_generator),sigma);
687 350909 : subst_values(m_rewrite_stack.top(),assignments,rhs,m_generator);
688 350909 : rewrite_aux(result, m_rewrite_stack.top(),sigma);
689 350887 : m_rewrite_stack.decrease(arity+1);
690 350887 : return;
691 : }
692 : else
693 : {
694 41 : assert(arity>rule_arity);
695 : // There are more arguments than those that have been rewritten.
696 : // Get those, put them in rewritten.
697 :
698 82 : for(std::size_t i=rule_arity; i<arity; ++i)
699 : {
700 41 : m_rewrite_stack.set_element(i,arity+1,detail::get_argument_of_higher_order_term(term,i));
701 41 : rewritten_defined[i]=true;
702 : }
703 :
704 41 : subst_values(m_rewrite_stack.top(),assignments,rhs,m_generator);
705 41 : std::size_t i = rule_arity;
706 41 : sort_expression sort = detail::residual_sort(op.sort(),i);
707 82 : while (is_function_sort(sort) && (i < arity))
708 : {
709 41 : const function_sort& fsort = atermpp::down_cast<function_sort>(sort);
710 41 : const std::size_t end=i+fsort.domain().size();
711 41 : assert(end-1<arity);
712 : // result = application(result,&rewritten[0]+i,&rewritten[0]+end);
713 41 : assert(m_rewrite_stack.stack_size()+i>=arity+1);
714 41 : assert(end<arity+1);
715 41 : assert(end>=i);
716 :
717 41 : make_application(m_rewrite_stack.top(),m_rewrite_stack.top(),
718 : m_rewrite_stack.stack_iterator(i,arity+1),
719 : m_rewrite_stack.stack_iterator(end,arity+1));
720 41 : i=end;
721 41 : sort = fsort.codomain();
722 : }
723 :
724 41 : rewrite_aux(result,m_rewrite_stack.top(),sigma);
725 41 : m_rewrite_stack.decrease(arity+1);
726 41 : return;
727 41 : }
728 : }
729 :
730 : }
731 2535049 : assignments.size=0;
732 : }
733 : }
734 : }
735 :
736 : // No rewrite rule is applicable. Rewrite the not yet rewritten arguments.
737 : // As we rewrite all, we do not record anymore whether terms are rewritten.
738 :
739 2172872 : for (std::size_t i=0; i<arity; i++)
740 : {
741 1397688 : if (!rewritten_defined[i])
742 : {
743 : // new (&rewritten[i]) data_expression(rewrite_aux(detail::get_argument_of_higher_order_term(term,i),sigma));
744 697714 : rewrite_aux(m_rewrite_stack.element(i,arity+1),detail::get_argument_of_higher_order_term(term,i),sigma);
745 : }
746 : }
747 :
748 : // The while loop must always be iterated once. Therefore, the initial traversal is put before the
749 : // main loop.
750 775184 : const function_sort& fsort=atermpp::down_cast<function_sort>(op.sort());
751 775184 : const std::size_t end=fsort.domain().size();
752 :
753 775184 : make_application(result,op,m_rewrite_stack.stack_iterator(0,arity+1), m_rewrite_stack.stack_iterator(end,arity+1));
754 775184 : std::size_t i=end;
755 775184 : const sort_expression* sort = &fsort.codomain();
756 775263 : while (i<arity && is_function_sort(*sort))
757 : {
758 79 : const function_sort& fsort=atermpp::down_cast<function_sort>(*sort);
759 79 : const std::size_t end=i+fsort.domain().size();
760 79 : assert(m_rewrite_stack.stack_size()+i>=arity+1);
761 79 : assert(end<arity+1);
762 79 : assert(end>=i);
763 79 : make_application(result,result,m_rewrite_stack.stack_iterator(i,arity+1), m_rewrite_stack.stack_iterator(end,arity+1));
764 79 : i=end;
765 79 : sort = &fsort.codomain();
766 : }
767 :
768 775184 : m_rewrite_stack.decrease(arity+1);
769 775184 : return;
770 : }
771 :
772 724218 : void RewriterJitty::rewrite_aux_const_function_symbol(
773 : data_expression& result,
774 : const function_symbol& op,
775 : substitution_type& sigma)
776 : {
777 : // This is special code to rewrite a function symbol. Note that the function symbol can be higher order,
778 : // e.g., it can be a function symbol f for which a rewrite rule f(n)=... exists.
779 :
780 724218 : const std::size_t op_value=atermpp::detail::index_traits<data::function_symbol,function_symbol_key_type, 2>::index(op);
781 724218 : make_jitty_strat_sufficiently_larger(op_value);
782 :
783 : // Cache the rhs's as they are rewritten very often.
784 724218 : if (rhs_for_constants_cache.size()<=op_value)
785 : {
786 3133 : rhs_for_constants_cache.resize(op_value+1);
787 : }
788 724218 : const data_expression& cached_rhs = rhs_for_constants_cache[op_value];
789 724218 : if (!cached_rhs.is_default_data_expression())
790 : {
791 : // result=cached_rhs;
792 : /* result.assign(cached_rhs,
793 : this->m_busy_flag,
794 : this->m_forbidden_flag,
795 : *this->m_creation_depth); */
796 718306 : result.assign(cached_rhs, *m_thread_aterm_pool);
797 718306 : return;
798 : }
799 :
800 5912 : const strategy& strat=jitty_strat[op_value];
801 :
802 5912 : for (const strategy_rule& rule : strat.rules())
803 : {
804 504 : if (rule.is_rewrite_index())
805 : {
806 : // In this case a standalone function symbol is rewritten, which could have arguments.
807 : // It is not needed to rewrite the arguments.
808 239 : break;
809 : }
810 265 : else if (rule.is_cpp_code())
811 : {
812 0 : result=rule.rewrite_cpp_code()(op); /* TODO Optimize */
813 0 : rhs_for_constants_cache[op_value]=result;
814 36 : return;
815 : }
816 : else
817 : {
818 265 : const data_equation& rule1=rule.equation();
819 265 : const data_expression& lhs=rule1.lhs();
820 265 : std::size_t rule_arity = (is_function_symbol(lhs)?0:detail::recursive_number_of_args(lhs));
821 :
822 265 : if (rule_arity > 0)
823 : {
824 229 : break;
825 : }
826 :
827 36 : if (rule1.condition()==sort_bool::true_())
828 : {
829 36 : rewrite_aux(result,rule1.rhs(),sigma);
830 36 : rhs_for_constants_cache[op_value]=result;
831 36 : return;
832 : }
833 0 : rewrite_aux(result,rule1.condition(),sigma);
834 0 : if (result==sort_bool::true_())
835 : {
836 0 : rewrite_aux(result,rule1.rhs(),sigma);
837 0 : rhs_for_constants_cache[op_value]=result;
838 0 : return;
839 : }
840 : }
841 : }
842 :
843 5876 : rhs_for_constants_cache[op_value]=op;
844 5876 : result=op;
845 5876 : return;
846 : }
847 :
848 345021 : void RewriterJitty::rewrite(
849 : data_expression& result,
850 : const data_expression& term,
851 : substitution_type& sigma)
852 : {
853 : #ifdef MCRL2_DISPLAY_REWRITE_STATISTICS
854 : data::detail::increment_rewrite_count();
855 : #endif
856 345021 : if (rewriting_in_progress)
857 : {
858 79546 : rewrite_aux(result, term, sigma);
859 : }
860 : else
861 : {
862 265475 : assert(m_rewrite_stack.stack_size()==0);
863 265475 : rewriting_in_progress=true;
864 : try
865 : {
866 265475 : rewrite_aux(result, term, sigma);
867 : }
868 1 : catch (recalculate_term_as_stack_is_too_small&)
869 : {
870 1 : rewriting_in_progress=false; // Restart rewriting, due to a stack overflow.
871 : // The stack is a vector, and it may be relocated in memory when
872 : // resized. References to the stack loose their validity.
873 1 : m_rewrite_stack.reserve_more_space();
874 1 : rewrite(result,term,sigma);
875 1 : return;
876 1 : }
877 265474 : rewriting_in_progress=false;
878 265474 : assert(m_rewrite_stack.stack_size()==0);
879 : }
880 :
881 345020 : assert(remove_normal_form_function(result)==result);
882 345020 : return;
883 : }
884 :
885 78812 : data_expression RewriterJitty::rewrite(
886 : const data_expression& term,
887 : substitution_type& sigma)
888 : {
889 78812 : data_expression result;
890 78812 : rewrite(result, term, sigma);
891 78812 : return result;
892 0 : }
893 :
894 :
895 0 : rewrite_strategy RewriterJitty::getStrategy()
896 : {
897 0 : return jitty;
898 : }
899 : }
900 : }
901 : }
|
