Line data Source code
1 : // Author(s): Muck van Weerdenburg
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 : /// \file jittyc.cpp
10 :
11 : #include "mcrl2/data/detail/rewrite.h" // Required for MCRL2_JITTTYC_AVAILABLE.
12 :
13 : #ifdef MCRL2_ENABLE_JITTYC
14 :
15 : #define NAME "rewr_jittyc"
16 :
17 : #include <unistd.h>
18 : #include <sys/stat.h>
19 : #include "mcrl2/utilities/basename.h"
20 : #include "mcrl2/utilities/stopwatch.h"
21 : #include "mcrl2/atermpp/algorithm.h"
22 : #include "mcrl2/atermpp/detail/aterm_list_implementation.h"
23 : #include "mcrl2/data/detail/rewrite/jittyc.h"
24 : #include "mcrl2/data/detail/rewrite/jitty_jittyc.h"
25 : #include "mcrl2/data/replace.h"
26 :
27 : #ifdef MCRL2_DISPLAY_REWRITE_STATISTICS
28 : #include "mcrl2/data/detail/rewrite_statistics.h"
29 : #endif
30 :
31 : using namespace mcrl2::core;
32 : using namespace mcrl2::core::detail;
33 : using namespace atermpp;
34 : using namespace mcrl2::log;
35 :
36 : namespace mcrl2
37 : {
38 : namespace data
39 : {
40 : namespace detail
41 : {
42 :
43 : // Some compilers can only deal with a limited number of nested curly brackets.
44 : // This limit can be increased by using -fbracket-depth=C where C is a new constant
45 : // value. By default this value C often appears to be 256. But not all compilers
46 : // recognize -fbracket-depth=C, making its use unreliable and therefore not advisable.
47 : // In order to generate the these auxiliary code fragments, we need to recall
48 : // what the template and data parameters of the current process are.
49 :
50 : class bracket_level_data
51 : {
52 : public:
53 : const std::size_t MCRL2_BRACKET_NESTING_LEVEL=250; // Some compilers limit the nesting to 256 brackets.
54 : // This guarantees that we will not use more.
55 : std::size_t bracket_nesting_level;
56 : std::string current_template_parameters;
57 : std::stack< std::string > current_data_parameters;
58 : std::stack< std::string > current_data_arguments;
59 :
60 897 : bracket_level_data()
61 897 : : bracket_nesting_level(0)
62 897 : {}
63 : };
64 :
65 : /// This function returns the variables that occur in a complex subexpression within f.
66 : /// For instance in f(n+1,m) it returns {n}. In m+f(n1+1,n2) it returns {n1}.
67 : /// The effect is that such variables n, and n1, must be in normalform, before evaluation.
68 : /// This is required for the template structure of the compiling rewriter.
69 5444 : static void find_variables_in_the_scope_of_main_function_symbol_in_a_complex_subexpression_helper(
70 : const data_expression& f,
71 : const data_expression& e,
72 : std::set <variable>& result)
73 : {
74 5444 : if (is_function_symbol(e))
75 : {
76 2267 : return;
77 : }
78 3177 : else if (is_variable(e))
79 : {
80 1818 : return;
81 : }
82 1359 : else if (is_abstraction(e))
83 : {
84 44 : const abstraction& abstr = down_cast<abstraction>(e);
85 44 : std::set<variable> intermediate_result;
86 44 : find_variables_in_the_scope_of_main_function_symbol_in_a_complex_subexpression_helper(f, abstr.body(), intermediate_result);
87 : // Remove the bound variables.
88 122 : for(const variable& v: abstr.variables())
89 : {
90 78 : intermediate_result.erase(v);
91 : }
92 44 : result.insert(intermediate_result.begin(), intermediate_result.end());
93 :
94 44 : return;
95 44 : }
96 1315 : else if (is_where_clause(e))
97 : {
98 0 : const where_clause& where = down_cast<where_clause>(e);
99 0 : std::set<variable> intermediate_result;
100 0 : find_variables_in_the_scope_of_main_function_symbol_in_a_complex_subexpression_helper(f, where.body(), intermediate_result);
101 0 : result.insert(intermediate_result.begin(), intermediate_result.end());
102 0 : for(const assignment_expression& ass: where.declarations())
103 : {
104 0 : const assignment& ass1= atermpp::down_cast<assignment>(ass);
105 0 : intermediate_result.erase(ass1.lhs());
106 0 : find_variables_in_the_scope_of_main_function_symbol_in_a_complex_subexpression_helper(f, ass1.rhs(), intermediate_result);
107 : }
108 0 : result.insert(intermediate_result.begin(), intermediate_result.end());
109 :
110 0 : return;
111 0 : }
112 : else
113 : {
114 1315 : assert(is_application(e));
115 : // e has the shape application(head,t1,...,tn)
116 1315 : const application& appl = down_cast<application>(e);
117 1315 : const std::size_t arity = recursive_number_of_args(appl);
118 :
119 1315 : if (get_nested_head(e)==f)
120 : {
121 1049 : for(std::size_t i=0; i<arity; i++)
122 : {
123 692 : const data_expression arg=get_argument_of_higher_order_term(appl, i);
124 692 : if (is_variable(arg))
125 : {
126 : // if the argument is a single variable, it is ignored.
127 : }
128 : else
129 : {
130 180 : std::set<variable> variables_in_arg=find_free_variables(arg);
131 180 : result.insert(variables_in_arg.begin(), variables_in_arg.end());
132 180 : }
133 692 : }
134 :
135 : }
136 : else
137 : {
138 : // Traverse all subexpressions for occurrences of variables.
139 958 : const data_expression& head = appl.head();
140 958 : find_variables_in_the_scope_of_main_function_symbol_in_a_complex_subexpression_helper(f, head, result);
141 2732 : for(const data_expression& arg: appl)
142 : {
143 1774 : find_variables_in_the_scope_of_main_function_symbol_in_a_complex_subexpression_helper(f, arg, result);
144 : }
145 : }
146 : }
147 :
148 1315 : return;
149 : }
150 :
151 :
152 2668 : static std::set<variable> find_variables_in_the_scope_of_main_function_symbol_in_a_complex_subexpression(
153 : const data_expression& f,
154 : const data_expression& e)
155 : {
156 2668 : std::set <variable> result;
157 2668 : find_variables_in_the_scope_of_main_function_symbol_in_a_complex_subexpression_helper(f, e, result);
158 2668 : return result;
159 0 : }
160 :
161 :
162 : typedef atermpp::term_list<variable_list> variable_list_list;
163 :
164 2668 : static std::vector<bool> dep_vars(const data_equation& eqn)
165 : {
166 2668 : std::vector<bool> result(recursive_number_of_args(eqn.lhs()), true);
167 2668 : std::set<variable> condition_vars = find_free_variables(eqn.condition());
168 : std::set<variable> variables_in_the_scope_of_main_function_symbol_in_a_complex_subexpression =
169 2668 : find_variables_in_the_scope_of_main_function_symbol_in_a_complex_subexpression(get_nested_head(eqn.lhs()),eqn.rhs());
170 2668 : double_variable_traverser<data::variable_traverser> lhs_doubles;
171 2668 : double_variable_traverser<data::variable_traverser> rhs_doubles;
172 2668 : lhs_doubles.apply(eqn.lhs());
173 2668 : rhs_doubles.apply(eqn.rhs());
174 :
175 8035 : for (std::size_t i = 0; i < result.size(); ++i)
176 : {
177 5367 : const data_expression& arg_i = get_argument_of_higher_order_term(atermpp::down_cast<application>(eqn.lhs()), i);
178 5367 : if (is_variable(arg_i))
179 : {
180 2462 : const variable& v = down_cast<variable>(arg_i);
181 2462 : if (condition_vars.count(v) == 0 &&
182 2298 : lhs_doubles.result().count(v) == 0 &&
183 6120 : rhs_doubles.result().count(v) == 0 &&
184 1360 : variables_in_the_scope_of_main_function_symbol_in_a_complex_subexpression.count(v) == 0)
185 : {
186 1360 : result[i] = false;
187 : }
188 : }
189 : }
190 5336 : return result;
191 2668 : }
192 :
193 10 : static std::size_t calc_max_arity(const function_symbol_vector& symbols)
194 : {
195 10 : std::size_t max_arity = 0;
196 825 : for (const function_symbol& f: symbols)
197 : {
198 815 : std::size_t arity = getArity(f);
199 815 : max_arity = std::max(max_arity, arity);
200 : }
201 :
202 10 : return max_arity;
203 : }
204 :
205 :
206 : ///
207 : /// \brief arity_is_allowed yields true if the function indicated by the function index can
208 : /// legitemately be used with a arguments. A function f:D1x...xDn->D can be used with 0 and
209 : /// n arguments. A function f:(D1x...xDn)->(E1x...Em)->F can be used with 0, n, and n+m
210 : /// arguments.
211 : /// \param s A function sort
212 : /// \param a The desired number of arguments
213 : /// \return A boolean indicating whether a term of sort s applied to a arguments is a valid term.
214 : ///
215 7405 : static bool arity_is_allowed(const sort_expression& s, const std::size_t a)
216 : {
217 7405 : if (a == 0)
218 : {
219 3565 : return true;
220 : }
221 3840 : if (is_function_sort(s))
222 : {
223 3840 : const function_sort& fs = atermpp::down_cast<function_sort>(s);
224 3840 : std::size_t n = fs.domain().size();
225 3840 : return n <= a && arity_is_allowed(fs.codomain(), a - n);
226 : }
227 0 : return false;
228 : }
229 :
230 8418 : void RewriterCompilingJitty::term2seq(const data_expression& t, match_tree_list& s, std::size_t *var_cnt, const bool omit_head)
231 : {
232 8418 : if (is_function_symbol(t))
233 : {
234 1683 : const function_symbol f(t);
235 1683 : s.push_front(match_tree_F(f,dummy,dummy));
236 1683 : s.push_front(match_tree_D(dummy,0));
237 1683 : return;
238 1683 : }
239 :
240 6735 : if (is_variable(t))
241 : {
242 4992 : const variable v(t);
243 4992 : match_tree store = match_tree_S(v,dummy);
244 :
245 4992 : if (std::find(s.begin(),s.end(),store) != s.end())
246 : {
247 524 : s.push_front(match_tree_M(v,dummy,dummy));
248 : }
249 : else
250 : {
251 4468 : (*var_cnt)++;
252 4468 : s.push_front(store);
253 : }
254 4992 : return;
255 4992 : }
256 :
257 1743 : assert(is_application(t));
258 1743 : const application ta(t);
259 1743 : std::size_t arity = ta.size();
260 :
261 1743 : if (is_application(ta.head()))
262 : {
263 0 : term2seq(ta.head(),s,var_cnt,omit_head);
264 0 : s.push_front(match_tree_N(dummy,0));
265 : }
266 1743 : else if (!omit_head)
267 : {
268 : {
269 1591 : s.push_front(match_tree_F(function_symbol(ta.head()),dummy,dummy));
270 : }
271 : }
272 :
273 1743 : std::size_t j=1;
274 4856 : for (const data_expression& u: ta)
275 : {
276 3113 : term2seq(u,s,var_cnt,false);
277 3113 : if (j<arity)
278 : {
279 1370 : s.push_front(match_tree_N(dummy,0));
280 : }
281 3113 : ++j;
282 : }
283 :
284 1743 : if (!omit_head)
285 : {
286 1591 : s.push_front(match_tree_D(dummy,0));
287 : }
288 1743 : }
289 :
290 2756 : static variable_or_number_list get_used_vars(const data_expression& t)
291 : {
292 2756 : std::set <variable> vars = find_free_variables(t);
293 5512 : return variable_or_number_list(vars.begin(),vars.end());
294 2756 : }
295 :
296 2668 : match_tree_list RewriterCompilingJitty::create_sequence(const data_equation& rule, std::size_t* var_cnt)
297 : {
298 2668 : const data_expression lhs_inner = rule.lhs();
299 2668 : const data_expression cond = rule.condition();
300 2668 : const data_expression rslt = rule.rhs();
301 2668 : match_tree_list rseq;
302 :
303 2668 : if (!is_function_symbol(lhs_inner))
304 : {
305 2668 : const application lhs_innera(lhs_inner);
306 2668 : std::size_t lhs_arity = lhs_innera.size();
307 :
308 2668 : if (is_application(lhs_innera.head()))
309 : {
310 152 : term2seq(lhs_innera.head(),rseq,var_cnt,true);
311 152 : rseq.push_front(match_tree_N(dummy,0));
312 : }
313 :
314 2668 : std::size_t j=1;
315 7821 : for (application::const_iterator i=lhs_innera.begin(); i!=lhs_innera.end(); ++i,++j)
316 : {
317 5153 : term2seq(*i,rseq,var_cnt,false);
318 5153 : if (j<lhs_arity)
319 : {
320 2485 : rseq.push_front(match_tree_N(dummy,0));
321 : }
322 : }
323 2668 : }
324 :
325 2668 : if (cond==sort_bool::true_())
326 : {
327 2580 : rseq.push_front(match_tree_Re(rslt,get_used_vars(rslt)));
328 : }
329 : else
330 : {
331 88 : rseq.push_front(match_tree_CRe(cond,rslt, get_used_vars(cond), get_used_vars(rslt)));
332 : }
333 :
334 5336 : return reverse(rseq);
335 2668 : }
336 :
337 :
338 34020 : static match_tree_list_list_list add_to_stack(const match_tree_list_list_list& stack, const match_tree_list_list& seqs, match_tree_Re& r, match_tree_list& cr)
339 : {
340 34020 : if (stack.empty())
341 : {
342 13290 : return stack;
343 : }
344 :
345 20730 : match_tree_list_list l;
346 20730 : match_tree_list_list h = stack.front();
347 :
348 34195 : for (const match_tree_list& e: seqs)
349 : {
350 13465 : if (e.front().isD())
351 : {
352 4680 : l.push_front(e.tail());
353 : }
354 8785 : else if (e.front().isN())
355 : {
356 4815 : h.push_front(e.tail());
357 : }
358 3970 : else if (e.front().isRe())
359 : {
360 3870 : r = match_tree_Re(e.front());
361 : }
362 : else
363 : {
364 100 : cr.push_front(e.front());
365 : }
366 : }
367 :
368 20730 : match_tree_list_list_list result=add_to_stack(stack.tail(),l,r,cr);
369 20730 : result.push_front(h);
370 20730 : return result;
371 20730 : }
372 :
373 7879 : static void add_to_build_pars(build_pars& pars, const match_tree_list_list& seqs, match_tree_Re& r, match_tree_list& cr)
374 : {
375 7879 : match_tree_list_list l;
376 :
377 20468 : for (const match_tree_list& e: seqs)
378 : {
379 12589 : if (e.front().isD() || e.front().isN())
380 : {
381 2031 : l.push_front(e);
382 : }
383 10558 : else if (e.front().isS())
384 : {
385 5556 : pars.Slist.push_front(e);
386 : }
387 5002 : else if (e.front().isMe()) // M should not appear at the head of a seq
388 : {
389 1198 : pars.Mlist.push_front(e);
390 : }
391 3804 : else if (e.front().isF())
392 : {
393 3804 : pars.Flist.push_front(e);
394 : }
395 0 : else if (e.front().isRe())
396 : {
397 0 : r = e.front();
398 : }
399 : else
400 : {
401 0 : cr.push_front(e.front());
402 : }
403 : }
404 :
405 7879 : pars.stack = add_to_stack(pars.stack,l,r,cr);
406 7879 : }
407 :
408 4213 : static variable createFreshVar(const sort_expression& sort, std::size_t* i)
409 : {
410 8426 : return data::variable("@var_" + std::to_string((*i)++), sort);
411 : }
412 :
413 5556 : match_tree_list RewriterCompilingJitty::subst_var(const match_tree_list& l,
414 : const variable& old,
415 : const variable& new_val,
416 : const std::size_t num,
417 : const mutable_map_substitution<>& substs)
418 : {
419 5556 : match_tree_vector result;
420 32949 : for(match_tree_list::const_iterator i=l.begin(); i!=l.end(); ++i)
421 : {
422 27393 : match_tree head=*i;
423 27393 : if (head.isM())
424 : {
425 674 : const match_tree_M headM(head);
426 674 : if (headM.match_variable()==old)
427 : {
428 532 : assert(headM.true_tree()==dummy);
429 532 : assert(headM.false_tree()==dummy);
430 532 : head = match_tree_Me(new_val,num);
431 : }
432 674 : }
433 26719 : else if (head.isCRe())
434 : {
435 244 : const match_tree_CRe headCRe(head);
436 244 : variable_or_number_list l = headCRe.variables_condition(); // This is a list with variables and aterm_ints.
437 244 : variable_or_number_list m ; // Idem.
438 702 : for (; !l.empty(); l=l.tail())
439 : {
440 458 : if (l.front()==old)
441 : {
442 172 : m.push_front(atermpp::aterm_int(num));
443 : }
444 : else
445 : {
446 286 : m.push_front(l.front());
447 : }
448 : }
449 244 : l = headCRe.variables_result();
450 244 : variable_or_number_list n;
451 786 : for (; !l.empty(); l=l.tail())
452 : {
453 542 : if (l.front()==old)
454 : {
455 146 : n.push_front(atermpp::aterm_int(num));
456 : }
457 : else
458 : {
459 396 : n.push_front(l.front());
460 : }
461 : }
462 488 : head = match_tree_CRe(replace_variables_capture_avoiding(headCRe.condition(),substs),
463 732 : replace_variables_capture_avoiding(headCRe.result(),substs),m, n);
464 244 : }
465 26475 : else if (head.isRe())
466 : {
467 5312 : const match_tree_Re& headRe(head);
468 5312 : variable_or_number_list l = headRe.variables();
469 5312 : variable_or_number_list m ;
470 14108 : for (; !l.empty(); l=l.tail())
471 : {
472 8796 : if (l.front()==old)
473 : {
474 3292 : m.push_front(atermpp::aterm_int(num));
475 : }
476 : else
477 : {
478 5504 : m.push_front(l.front());
479 : }
480 : }
481 5312 : head = match_tree_Re(replace_variables_capture_avoiding(headRe.result(),substs),m);
482 5312 : }
483 27393 : result.push_back(head);
484 27393 : }
485 11112 : return match_tree_list(result.begin(),result.end());
486 5556 : }
487 :
488 : static std::vector < std::size_t> treevars_usedcnt;
489 :
490 3900 : static void inc_usedcnt(const variable_or_number_list& l)
491 : {
492 7634 : for (const variable_or_number& v: l)
493 : {
494 3734 : if (v.type_is_int())
495 : {
496 3734 : treevars_usedcnt[down_cast<aterm_int>(v).value()]++;
497 : }
498 : }
499 3900 : }
500 :
501 19036 : match_tree RewriterCompilingJitty::build_tree(build_pars pars, std::size_t i)
502 : {
503 19036 : if (!pars.Slist.empty())
504 : {
505 4213 : match_tree_list l;
506 4213 : match_tree_list_list m;
507 :
508 4213 : std::size_t k = i;
509 4213 : const variable v = createFreshVar(match_tree_S(pars.Slist.front().front()).target_variable().sort(),&i);
510 4213 : treevars_usedcnt[k] = 0;
511 :
512 9769 : for (; !pars.Slist.empty(); pars.Slist=pars.Slist.tail())
513 : {
514 5556 : match_tree_list e = pars.Slist.front();
515 :
516 5556 : mutable_map_substitution<> sigma;
517 5556 : sigma[match_tree_S(e.front()).target_variable()]=v;
518 11112 : e = subst_var(e,
519 11112 : match_tree_S(e.front()).target_variable(),
520 : v,
521 : k,
522 5556 : sigma);
523 :
524 5556 : l.push_front(e.front());
525 5556 : m.push_front(e.tail());
526 5556 : }
527 :
528 4213 : match_tree_Re r;
529 4213 : match_tree ret;
530 4213 : match_tree_list readies;
531 :
532 4213 : pars.stack = add_to_stack(pars.stack,m,r,readies);
533 :
534 4213 : if (!r.is_defined())
535 : {
536 2219 : match_tree tree = build_tree(pars,i);
537 2311 : for (match_tree_list::const_iterator i=readies.begin(); i!=readies.end(); ++i)
538 : {
539 92 : match_tree_CRe t(*i);
540 92 : inc_usedcnt(t.variables_condition());
541 92 : inc_usedcnt(t.variables_result());
542 92 : tree = match_tree_C(t.condition(),match_tree_R(t.result()),tree);
543 92 : }
544 2219 : ret = tree;
545 2219 : }
546 : else
547 : {
548 :
549 1994 : inc_usedcnt(r.variables());
550 1994 : ret = match_tree_R(r.result());
551 : }
552 :
553 4213 : if ((treevars_usedcnt[k] > 0) || ((k == 0) && ret.isR()))
554 : {
555 3217 : return match_tree_S(v,ret);
556 : }
557 : else
558 : {
559 996 : return ret;
560 : }
561 4213 : }
562 14823 : else if (!pars.Mlist.empty())
563 : {
564 1198 : match_tree_Me M(pars.Mlist.front().front());
565 :
566 1198 : match_tree_list_list l;
567 1198 : match_tree_list_list m;
568 2396 : for (; !pars.Mlist.empty(); pars.Mlist=pars.Mlist.tail())
569 : {
570 1198 : if (M==pars.Mlist.front().front())
571 : {
572 1198 : l.push_front(pars.Mlist.front().tail());
573 : }
574 : else
575 : {
576 0 : m.push_front(pars.Mlist.front());
577 : }
578 : }
579 1198 : pars.Mlist = m;
580 :
581 1198 : match_tree true_tree,false_tree;
582 1198 : match_tree_Re r ;
583 1198 : match_tree_list readies;
584 :
585 1198 : match_tree_list_list_list newstack = add_to_stack(pars.stack,l,r,readies);
586 :
587 1198 : false_tree = build_tree(pars,i);
588 :
589 1198 : if (!r.is_defined())
590 : {
591 279 : pars.stack = newstack;
592 279 : true_tree = build_tree(pars,i);
593 279 : for (; !readies.empty(); readies=readies.tail())
594 : {
595 0 : match_tree_CRe t(readies.front());
596 0 : inc_usedcnt(t.variables_condition());
597 0 : inc_usedcnt(t.variables_result());
598 0 : true_tree = match_tree_C(t.condition(), match_tree_R(t.result()),true_tree);
599 0 : }
600 : }
601 : else
602 : {
603 919 : inc_usedcnt(r.variables());
604 919 : true_tree = match_tree_R(r.result());
605 : }
606 :
607 1198 : if (true_tree==false_tree)
608 : {
609 0 : return true_tree;
610 : }
611 : else
612 : {
613 1198 : treevars_usedcnt[M.variable_index()]++;
614 1198 : return match_tree_M(M.match_variable(),true_tree,false_tree);
615 : }
616 1198 : }
617 13625 : else if (!pars.Flist.empty())
618 : {
619 3214 : match_tree_list F = pars.Flist.front();
620 3214 : match_tree true_tree,false_tree;
621 :
622 3214 : match_tree_list_list newupstack = pars.upstack;
623 3214 : match_tree_list_list l;
624 :
625 9518 : for (; !pars.Flist.empty(); pars.Flist=pars.Flist.tail())
626 : {
627 6304 : if (pars.Flist.front().front()==F.front())
628 : {
629 3958 : newupstack.push_front(pars.Flist.front().tail());
630 : }
631 : else
632 : {
633 2346 : l.push_front(pars.Flist.front());
634 : }
635 : }
636 :
637 3214 : pars.Flist = l;
638 3214 : false_tree = build_tree(pars,i);
639 3214 : pars.Flist = match_tree_list_list();
640 3214 : pars.upstack = newupstack;
641 3214 : true_tree = build_tree(pars,i);
642 :
643 3214 : if (true_tree==false_tree)
644 : {
645 0 : return true_tree;
646 : }
647 : else
648 : {
649 3214 : return match_tree_F(match_tree_F(F.front()).function(),true_tree,false_tree);
650 : }
651 3214 : }
652 10411 : else if (!pars.upstack.empty())
653 : {
654 3214 : match_tree_list_list l;
655 :
656 3214 : match_tree_Re r;
657 3214 : match_tree_list readies;
658 :
659 3214 : pars.stack.push_front(match_tree_list_list());
660 3214 : l = pars.upstack;
661 3214 : pars.upstack = match_tree_list_list();
662 3214 : add_to_build_pars(pars,l,r,readies);
663 :
664 :
665 3214 : if (!r.is_defined())
666 : {
667 2411 : match_tree t = build_tree(pars,i);
668 :
669 2411 : for (; !readies.empty(); readies=readies.tail())
670 : {
671 0 : match_tree_CRe u(readies.front());
672 0 : inc_usedcnt(u.variables_condition());
673 0 : inc_usedcnt(u.variables_result());
674 0 : t = match_tree_C(u.condition(), match_tree_R(u.result()),t);
675 0 : }
676 :
677 2411 : return t;
678 2411 : }
679 : else
680 : {
681 803 : inc_usedcnt(r.variables());
682 803 : return match_tree_R(r.result());
683 : }
684 3214 : }
685 : else
686 : {
687 7197 : if (pars.stack.front().empty())
688 : {
689 3612 : if (pars.stack.tail().empty())
690 : {
691 1776 : return match_tree_X();
692 : }
693 : else
694 : {
695 1836 : pars.stack = pars.stack.tail();
696 1836 : return match_tree_D(build_tree(pars,i),0);
697 : }
698 : }
699 : else
700 : {
701 3585 : match_tree_list_list l = pars.stack.front();
702 3585 : match_tree_Re r ;
703 3585 : match_tree_list readies;
704 :
705 3585 : pars.stack = pars.stack.tail();
706 3585 : pars.stack.push_front(match_tree_list_list());
707 3585 : add_to_build_pars(pars,l,r,readies);
708 :
709 3585 : match_tree tree;
710 3585 : if (!r.is_defined())
711 : {
712 3585 : tree = build_tree(pars,i);
713 3585 : for (; !readies.empty(); readies=readies.tail())
714 : {
715 0 : match_tree_CRe t(readies.front());
716 0 : inc_usedcnt(t.variables_condition());
717 0 : inc_usedcnt(t.variables_result());
718 0 : tree = match_tree_C(t.condition(), match_tree_R(t.result()),tree);
719 0 : }
720 : }
721 : else
722 : {
723 0 : inc_usedcnt(r.variables());
724 0 : tree = match_tree_R(r.result());
725 : }
726 :
727 3585 : return match_tree_N(tree,0);
728 3585 : }
729 : }
730 : }
731 :
732 1080 : match_tree RewriterCompilingJitty::create_tree(const data_equation_list& rules)
733 : // Create a match tree for OpId int2term[opid].
734 : //
735 : // Pre: rules is a list of rewrite rules for some function symbol f.
736 : // Ret: A match tree for function symbol f.
737 : {
738 : // Create sequences representing the trees for each rewrite rule and
739 : // store the total number of variables used in these sequences.
740 : // (The total number of variables in all sequences should be an upper
741 : // bound for the number of variable in the final tree.)
742 :
743 1080 : match_tree_list_list rule_seqs;
744 1080 : std::size_t total_rule_vars = 0;
745 3748 : for (const data_equation& e: rules)
746 : {
747 2668 : rule_seqs.push_front(create_sequence(e,&total_rule_vars));
748 : }
749 : // Generate initial parameters for built_tree
750 1080 : build_pars init_pars;
751 1080 : match_tree_Re r;
752 1080 : match_tree_list readies;
753 :
754 1080 : add_to_build_pars(init_pars,rule_seqs,r,readies);
755 1080 : match_tree tree;
756 1080 : if (!r.is_defined())
757 : {
758 1080 : treevars_usedcnt=std::vector < std::size_t> (total_rule_vars);
759 1080 : tree = build_tree(init_pars,0);
760 1080 : for (; !readies.empty(); readies=readies.tail())
761 : {
762 0 : match_tree_CRe u(readies.front());
763 0 : tree = match_tree_C(u.condition(), match_tree_R(u.result()), tree);
764 0 : }
765 : }
766 : else
767 : {
768 0 : tree = match_tree_R(r.result());
769 : }
770 2160 : return tree;
771 1080 : }
772 :
773 : // This function assigns a unique index to variable v and stores
774 : // v at this position in the vector rewriter_bound_variables. This is
775 : // used in the compiling rewriter to obtain this variable again.
776 : // Note that the static variable variable_indices is not cleared
777 : // during several runs, as generally the variables bound in rewrite
778 : // rules do not change.
779 156 : std::size_t RewriterCompilingJitty::bound_variable_index(const variable& v)
780 : {
781 156 : if (variable_indices0.count(v)>0)
782 : {
783 108 : return variable_indices0[v];
784 : }
785 48 : const std::size_t index_for_v=rewriter_bound_variables.size();
786 48 : variable_indices0[v]=index_for_v;
787 48 : rewriter_bound_variables.push_back(v);
788 48 : return index_for_v;
789 : }
790 :
791 : // This function assigns a unique index to variable list vl and stores
792 : // vl at this position in the vector rewriter_binding_variable_lists. This is
793 : // used in the compiling rewriter to obtain this variable again.
794 : // Note that the static variable variable_indices is not cleared
795 : // during several runs, as generally the variables bound in rewrite
796 : // rules do not change.
797 44 : std::size_t RewriterCompilingJitty::binding_variable_list_index(const variable_list& vl)
798 : {
799 44 : if (variable_list_indices1.count(vl)>0)
800 : {
801 5 : return variable_list_indices1[vl];
802 : }
803 39 : const std::size_t index_for_vl=rewriter_binding_variable_lists.size();
804 39 : variable_list_indices1[vl]=index_for_vl;
805 39 : rewriter_binding_variable_lists.push_back(vl);
806 39 : return index_for_vl;
807 : }
808 :
809 : // Put the sorts with indices between actual arity and requested arity in a vector.
810 140 : sort_list_vector RewriterCompilingJitty::get_residual_sorts(const sort_expression& s1, std::size_t actual_arity, std::size_t requested_arity)
811 : {
812 140 : sort_expression s=s1;
813 140 : sort_list_vector result;
814 420 : while (requested_arity>0)
815 : {
816 280 : const function_sort fs(s);
817 280 : if (actual_arity==0)
818 : {
819 140 : result.push_back(fs.domain());
820 140 : assert(fs.domain().size()<=requested_arity);
821 140 : requested_arity=requested_arity-fs.domain().size();
822 : }
823 : else
824 : {
825 140 : assert(fs.domain().size()<=actual_arity);
826 140 : actual_arity=actual_arity-fs.domain().size();
827 140 : requested_arity=requested_arity-fs.domain().size();
828 : }
829 280 : s=fs.codomain();
830 280 : }
831 280 : return result;
832 140 : }
833 :
834 : /// Rewrite the equation e such that it has exactly a arguments.
835 : /// If the rewrite rule has too many arguments, false is returned, otherwise
836 : /// additional arguments are added.
837 :
838 2668 : bool RewriterCompilingJitty::lift_rewrite_rule_to_right_arity(data_equation& e, const std::size_t requested_arity)
839 : {
840 2668 : data_expression lhs=e.lhs();
841 2668 : data_expression rhs=e.rhs();
842 2668 : variable_list vars=e.variables();
843 :
844 2668 : const data_expression& f=get_nested_head(lhs);
845 2668 : if (!is_function_symbol(f))
846 : {
847 0 : throw mcrl2::runtime_error("Equation " + pp(e) + " does not start with a function symbol in its left hand side.");
848 : }
849 :
850 2668 : std::size_t actual_arity=recursive_number_of_args(lhs);
851 2668 : if (arity_is_allowed(f.sort(),requested_arity) && actual_arity<=requested_arity)
852 : {
853 2668 : if (actual_arity<requested_arity)
854 : {
855 : // Supplement the lhs and rhs with requested_arity-actual_arity extra variables.
856 140 : sort_list_vector requested_sorts=get_residual_sorts(f.sort(),actual_arity,requested_arity);
857 280 : for(sort_list_vector::const_iterator sl=requested_sorts.begin(); sl!=requested_sorts.end(); ++sl)
858 : {
859 140 : variable_vector var_vec;
860 382 : for(sort_expression_list::const_iterator s=sl->begin(); s!=sl->end(); ++s)
861 : {
862 242 : variable v=variable(jitty_rewriter.identifier_generator()(),*s); // Find a new name for a variable that is temporarily in use.
863 242 : var_vec.push_back(v);
864 242 : vars.push_front(v);
865 242 : }
866 140 : lhs=application(lhs,var_vec.begin(),var_vec.end());
867 140 : rhs=application(rhs,var_vec.begin(),var_vec.end());
868 140 : }
869 140 : }
870 : }
871 : else
872 : {
873 0 : return false; // This is not an allowed arity, or the actual number of arguments is larger than the requested number.
874 : }
875 :
876 2668 : e=data_equation(vars,e.condition(),lhs,rhs);
877 2668 : return true;
878 2668 : }
879 :
880 1249 : match_tree_list RewriterCompilingJitty::create_strategy(const data_equation_list& rules, const std::size_t arity)
881 : {
882 : typedef std::list<std::size_t> dep_list_t;
883 1249 : match_tree_list strat;
884 : // Maintain dependency count (i.e. the number of rules that depend on a given argument)
885 1249 : std::vector<std::size_t> arg_use_count(arity, 0);
886 1249 : std::list<std::pair<data_equation, dep_list_t> > rule_deps;
887 4857 : for (const data_equation& eq: rules)
888 : {
889 3608 : if (recursive_number_of_args(eq.lhs()) <= arity)
890 : {
891 2668 : rule_deps.push_front(std::make_pair(eq, dep_list_t()));
892 2668 : dep_list_t& deps = rule_deps.front().second;
893 :
894 2668 : const std::vector<bool> is_dependent_arg = dep_vars(eq);
895 8035 : for (std::size_t i = 0; i < is_dependent_arg.size(); i++)
896 : {
897 : // Only if needed and not already rewritten
898 5367 : if (is_dependent_arg[i])
899 : {
900 4007 : deps.push_back(i);
901 : // Increase dependency count
902 4007 : arg_use_count[i] += 1;
903 : }
904 : }
905 2668 : }
906 : }
907 :
908 : // Process all rules with their dependencies
909 3322 : while (!rule_deps.empty())
910 : {
911 2073 : data_equation_list no_deps;
912 9026 : for (std::list<std::pair<data_equation, dep_list_t> >::iterator it = rule_deps.begin(); it != rule_deps.end(); )
913 : {
914 6953 : if (it->second.empty())
915 : {
916 2668 : lift_rewrite_rule_to_right_arity(it->first, arity);
917 2668 : no_deps.push_front(it->first);
918 2668 : it = rule_deps.erase(it);
919 : }
920 : else
921 : {
922 4285 : ++it;
923 : }
924 : }
925 :
926 : // Create and add tree of collected rules
927 2073 : if (!no_deps.empty())
928 : {
929 1080 : strat.push_front(create_tree(no_deps));
930 : }
931 :
932 : // Figure out which argument is most useful to rewrite
933 2073 : std::size_t max = 0;
934 2073 : std::size_t maxidx = 0;
935 6817 : for (std::size_t i = 0; i < arity; i++)
936 : {
937 4744 : if (arg_use_count[i] > max)
938 : {
939 1321 : maxidx = i;
940 1321 : max = arg_use_count[i];
941 : }
942 : }
943 :
944 : // If there is a maximum, add it to the strategy and remove it from the dependency lists
945 2073 : assert(rule_deps.empty() || max > 0);
946 2073 : if (max > 0)
947 : {
948 1288 : assert(!rule_deps.empty());
949 1288 : arg_use_count[maxidx] = 0;
950 1288 : strat.push_front(match_tree_A(maxidx));
951 5573 : for (std::list<std::pair<data_equation, dep_list_t> >::iterator it = rule_deps.begin(); it != rule_deps.end(); ++it)
952 : {
953 4285 : it->second.remove(maxidx);
954 : }
955 : }
956 2073 : }
957 2498 : return reverse(strat);
958 1249 : }
959 :
960 459 : void RewriterCompilingJitty::extend_nfs(nfs_array& nfs, const function_symbol& opid, std::size_t arity)
961 : {
962 459 : data_equation_list eqns = jittyc_eqns[opid];
963 459 : if (eqns.empty())
964 : {
965 107 : nfs.fill(true);
966 107 : return;
967 : }
968 352 : match_tree_list strat = create_strategy(eqns,arity);
969 814 : while (!strat.empty() && strat.front().isA())
970 : {
971 462 : nfs.at(match_tree_A(strat.front()).variable_index()) = true;
972 462 : strat = strat.tail();
973 : }
974 459 : }
975 :
976 : class rewr_function_spec
977 : {
978 : protected:
979 : const function_symbol m_fs;
980 : const std::size_t m_arity;
981 : const bool m_delayed;
982 :
983 : public:
984 3052 : rewr_function_spec(function_symbol fs, std::size_t arity, const bool delayed)
985 3052 : : m_fs(fs), m_arity(arity), m_delayed(delayed)
986 3052 : { }
987 :
988 30239 : bool operator<(const rewr_function_spec& other) const
989 : {
990 49967 : return m_fs < other.m_fs ||
991 67171 : (m_fs == other.m_fs && m_arity < other.m_arity) ||
992 57988 : (m_fs == other.m_fs && m_arity == other.m_arity && m_delayed<other.m_delayed);
993 : }
994 :
995 3259 : function_symbol fs() const
996 : {
997 3259 : return m_fs;
998 : }
999 :
1000 3733 : std::size_t arity() const
1001 : {
1002 3733 : return m_arity;
1003 : }
1004 :
1005 2050 : bool delayed() const
1006 : {
1007 2050 : return m_delayed;
1008 : }
1009 :
1010 : bool operator==(const rewr_function_spec& other) const
1011 : {
1012 : return m_fs == other.m_fs && m_arity == other.m_arity && m_delayed==other.m_delayed;
1013 : }
1014 :
1015 3966 : std::string name() const
1016 : {
1017 3966 : std::stringstream name;
1018 3966 : if (m_delayed)
1019 : {
1020 848 : name << "delayed_";
1021 : }
1022 3966 : name << "rewr_" << atermpp::detail::index_traits<data::function_symbol,function_symbol_key_type, 2>::index(m_fs)
1023 3966 : << "_" << m_arity;
1024 7932 : return name.str();
1025 3966 : }
1026 : };
1027 :
1028 : class RewriterCompilingJitty::ImplementTree
1029 : {
1030 : private:
1031 : class padding
1032 : {
1033 : private:
1034 : std::size_t m_indent;
1035 : public:
1036 5 : padding(std::size_t indent) : m_indent(indent) { }
1037 4537 : void indent() { m_indent += 2; }
1038 4537 : void unindent() { m_indent -= 2; }
1039 0 : std::size_t reset() { std::size_t old = m_indent; m_indent = 4; return old; }
1040 0 : void restore(const std::size_t i){ m_indent = i; }
1041 :
1042 : friend
1043 33104 : std::ostream& operator<<(std::ostream& stream, const padding& p)
1044 : {
1045 228392 : for (std::size_t i = p.m_indent; i != 0; --i)
1046 : {
1047 195288 : stream << ' ';
1048 : }
1049 33104 : return stream;
1050 : }
1051 : };
1052 :
1053 : RewriterCompilingJitty& m_rewriter;
1054 : std::stack<rewr_function_spec> m_rewr_functions;
1055 : std::set<rewr_function_spec> m_rewr_functions_implemented;
1056 : std::set<std::size_t>m_delayed_application_functions; // Recalls the arities of the required functions 'delayed_application';
1057 : std::vector<bool> m_used;
1058 : std::vector<int> m_stack;
1059 : padding m_padding;
1060 : // variable_or_number_list m_nnfvars;
1061 :
1062 : ///
1063 : /// \brief opid_is_nf establishes whether a function symbol is always in normal form.
1064 : /// this is the case when there are no rewrite rules for the symbol.
1065 : /// \param opid The symbol to investigate.
1066 : /// \param num_args The arity of the function symbol.
1067 : /// \return true if the function symbol is always in normal form, false otherwise.
1068 : ///
1069 : bool opid_is_nf(const function_symbol& opid, std::size_t num_args)
1070 : {
1071 : data_equation_list l = m_rewriter.jittyc_eqns[opid];
1072 : for (data_equation_list::const_iterator it = l.begin(); it != l.end(); ++it)
1073 : {
1074 : if (recursive_number_of_args(it->lhs()) <= num_args)
1075 : {
1076 : return false;
1077 : }
1078 : }
1079 : return true;
1080 : }
1081 :
1082 : /// \brief appl_function returns the name of a function that can construct a data::application of
1083 : /// arity `arity`.
1084 : /// \param arity the arity of the application that is to be constructed with the function.
1085 : /// \return the name of a function/constructor that creates an application (either of 'pass_on',
1086 : /// 'application' or 'make_term_with_many_arguments').
1087 : ///
1088 : static inline
1089 661 : const std::string appl_function(std::size_t arity)
1090 : {
1091 661 : if (arity == 0)
1092 : {
1093 0 : return "pass_on"; // This is to avoid confusion with atermpp::aterm_appl on a function symbol and two iterators.
1094 : }
1095 661 : return "make_application";
1096 : }
1097 :
1098 : inline
1099 2204 : const std::string rewr_function_name(const function_symbol& f, std::size_t arity)
1100 : {
1101 2204 : rewr_function_spec spec(f, arity, false);
1102 2204 : if (m_rewr_functions_implemented.insert(spec).second)
1103 : {
1104 897 : m_rewr_functions.push(spec);
1105 : }
1106 4408 : return spec.name();
1107 2204 : }
1108 :
1109 : inline
1110 848 : const std::string delayed_rewr_function_name(const function_symbol& f, std::size_t arity)
1111 : {
1112 848 : rewr_function_spec spec(f, arity, true);
1113 848 : if (m_rewr_functions_implemented.insert(spec).second)
1114 : {
1115 128 : m_rewr_functions.push(spec);
1116 : }
1117 848 : rewr_function_name(f,arity); // Also declare the non delayed function.
1118 1696 : return spec.name();
1119 848 : }
1120 :
1121 : /*
1122 : * calc_inner_term helper methods
1123 : *
1124 : */
1125 :
1126 1955 : void calc_inner_term_variable(std::ostream& s,
1127 : const std::string& target_for_output,
1128 : const variable& v,
1129 : const bool require_normal_form,
1130 : std::ostream& result_type,
1131 : const std::map<variable,std::string>& type_of_code_variables)
1132 : {
1133 1955 : const std::string variable_name = v.name();
1134 : // Remove the initial @ if it is present in the variable name, because then it is a variable introduced
1135 : // by this rewriter.
1136 1955 : if (variable_name[0] == '@')
1137 : {
1138 1799 : assert(type_of_code_variables.count(v)>0); // We know the type of the variable at hand.
1139 1799 : if (require_normal_form)
1140 : {
1141 765 : if (type_of_code_variables.at(v)=="data_expression")
1142 : {
1143 185 : if (target_for_output.empty())
1144 : {
1145 82 : s << variable_name.substr(1);
1146 : }
1147 : else
1148 : {
1149 206 : s << m_padding << target_for_output << ".assign(" << variable_name.substr(1)
1150 103 : << ", *this_rewriter->m_thread_aterm_pool);\n";
1151 : }
1152 : }
1153 : else
1154 : {
1155 580 : if (target_for_output.empty())
1156 : {
1157 412 : s << "local_rewrite(" << variable_name.substr(1) << ")";
1158 : }
1159 : else
1160 : {
1161 168 : s << m_padding << "local_rewrite(" << target_for_output << ", " << variable_name.substr(1) << ");\n";
1162 : }
1163 : }
1164 765 : result_type << "data_expression";
1165 : }
1166 : else // No normal form is required.
1167 : {
1168 1034 : assert(target_for_output.empty());
1169 1034 : s << variable_name.substr(1);
1170 1034 : if (type_of_code_variables.at(v)=="data_expression")
1171 : {
1172 771 : result_type << "data_expression";
1173 : }
1174 : else
1175 : {
1176 263 : assert(variable_name.substr(0,5)=="@var_");
1177 263 : result_type << type_of_code_variables.at(v);
1178 : }
1179 : }
1180 1799 : return;
1181 : }
1182 : else
1183 : {
1184 156 : if (target_for_output.empty())
1185 : {
1186 156 : s << "static_cast<const data_expression&>(this_rewriter->bound_variable_get(" << m_rewriter.bound_variable_index(v) << "))";
1187 : }
1188 : else
1189 : {
1190 : // s << m_padding << target_for_output << " = " <<
1191 : // "static_cast<const data_expression&>(this_rewriter->bound_variable_get(" << m_rewriter.bound_variable_index(v) << "))\n";
1192 0 : s << m_padding << target_for_output << ".assign("
1193 0 : << "static_cast<const data_expression&>(this_rewriter->bound_variable_get(" << m_rewriter.bound_variable_index(v) << ")), "
1194 0 : << "this_rewriter), *this_rewriter->m_thread_aterm_pool);\n";
1195 : }
1196 156 : result_type << "data_expression";
1197 156 : return;
1198 : }
1199 1955 : }
1200 :
1201 44 : void calc_inner_term_abstraction(
1202 : std::ostream& s,
1203 : const std::string& target_for_output,
1204 : const abstraction& a,
1205 : const std::size_t startarg,
1206 : const bool require_normal_form,
1207 : std::ostream& result_type,
1208 : const std::map<variable,std::string>& type_of_code_variables)
1209 : {
1210 44 : std::string binder_constructor;
1211 44 : std::string rewriter_function;
1212 44 : if (is_lambda_binder(a.binding_operator()))
1213 : {
1214 0 : binder_constructor = "lambda_binder";
1215 0 : rewriter_function = "rewrite_single_lambda";
1216 : }
1217 : else
1218 44 : if (is_forall_binder(a.binding_operator()))
1219 : {
1220 44 : binder_constructor = "forall_binder";
1221 44 : rewriter_function = "universal_quantifier_enumeration";
1222 : }
1223 : else
1224 : {
1225 0 : assert(is_exists_binder(a.binding_operator()));
1226 0 : binder_constructor = "exists_binder";
1227 0 : rewriter_function = "existential_quantifier_enumeration";
1228 : }
1229 44 : if (require_normal_form)
1230 : {
1231 44 : if (target_for_output.empty())
1232 : {
1233 0 : std::stringstream argument;
1234 0 : calc_inner_term(argument, "", a.body(), startarg, true, result_type, type_of_code_variables);
1235 : s << "this_rewriter->" << rewriter_function << "(" <<
1236 0 : "this_rewriter->binding_variable_list_get(" << m_rewriter.binding_variable_list_index(a.variables()) << "), ";
1237 0 : s << argument.str() << ", true, sigma(this_rewriter))";
1238 0 : result_type << "data_expression";
1239 0 : return;
1240 0 : }
1241 : else
1242 : {
1243 44 : calc_inner_term(s, target_for_output, a.body(), startarg, true, result_type, type_of_code_variables);
1244 44 : s << m_padding << "this_rewriter->" << rewriter_function << "(" << target_for_output <<
1245 44 : ", this_rewriter->binding_variable_list_get(" << m_rewriter.binding_variable_list_index(a.variables()) << "), ";
1246 44 : s << target_for_output << ", true, sigma(this_rewriter));\n";
1247 44 : result_type << "data_expression";
1248 44 : return;
1249 : }
1250 : }
1251 : else
1252 : {
1253 0 : std::stringstream argument_type;
1254 0 : std::stringstream argument_string;
1255 0 : calc_inner_term(argument_string, "", a.body(), startarg, false, argument_type, type_of_code_variables);
1256 0 : s << "delayed_abstraction<" << argument_type.str() << ">(" << binder_constructor << "(), "
1257 0 : "this_rewriter->binding_variable_list_get(" << m_rewriter.binding_variable_list_index(a.variables()) << "), ";
1258 0 : s << argument_string.str() << ", this_rewriter)";
1259 0 : result_type << "delayed_abstraction<" << argument_type.str() << ">";
1260 0 : return;
1261 0 : }
1262 44 : }
1263 :
1264 0 : void calc_inner_term_where_clause(std::ostream& s,
1265 : const std::string& target_for_output,
1266 : const where_clause& w,
1267 : const std::size_t startarg,
1268 : const bool require_normal_form,
1269 : std::ostream& result_type,
1270 : const std::map<variable,std::string>& type_of_code_variables)
1271 : {
1272 0 : if (require_normal_form) // TODO Take into account that some arguments are already in normal form.
1273 : {
1274 0 : if (target_for_output.empty())
1275 : {
1276 0 : s << "this_rewriter->rewrite_where(";
1277 : }
1278 : else
1279 : {
1280 0 : s << m_padding << "this_rewriter->rewrite_where(" << target_for_output << ", ";
1281 : }
1282 0 : result_type << "data_expression";
1283 : }
1284 : else
1285 : {
1286 0 : s << "term_not_in_normal_form(";
1287 0 : result_type << "term_not_in_normal_form";
1288 : }
1289 : // A rewritten result is expected.
1290 0 : std::stringstream temp_result_type;
1291 0 : s << "where_clause(";
1292 0 : calc_inner_term(s, "", w.body(), startarg, true, temp_result_type, type_of_code_variables);
1293 0 : s << ",";
1294 0 : for(std::size_t i = w.assignments().size(); i > 0; --i)
1295 : {
1296 0 : s << "jittyc_local_push_front(";
1297 : }
1298 0 : s << "assignment_expression_list()";
1299 0 : for(assignment_list::const_iterator i = w.assignments().begin(); i != w.assignments().end(); ++i)
1300 : {
1301 0 : s << ", assignment(this_rewriter->bound_variable_get(" << m_rewriter.bound_variable_index(i->lhs()) << "), ";
1302 0 : calc_inner_term(s, "", i->rhs(), startarg, true, temp_result_type, type_of_code_variables);
1303 0 : s << "))";
1304 : }
1305 0 : s << ")";
1306 0 : if (require_normal_form)
1307 : {
1308 0 : s << ", sigma(this_rewriter))";
1309 : }
1310 : else
1311 : {
1312 0 : s << ", this_rewriter)";
1313 : }
1314 0 : if (!target_for_output.empty())
1315 : {
1316 0 : s << ";\n";
1317 : }
1318 0 : }
1319 :
1320 883 : bool calc_inner_term_appl_function(std::ostream& s,
1321 : const std::string& target_for_output,
1322 : const application& a,
1323 : const function_symbol& head,
1324 : const std::size_t startarg,
1325 : const bool require_normal_form,
1326 : std::ostream& result_type,
1327 : const std::map<variable,std::string>& type_of_code_variables)
1328 : {
1329 883 : const std::size_t arity = recursive_number_of_args(a);
1330 :
1331 883 : assert(arity > 0);
1332 883 : nfs_array args_nfs(arity);
1333 883 : if (require_normal_form)
1334 : {
1335 : // Take care that arguments that need to be rewritten,
1336 : // are rewritten immediately.
1337 459 : m_rewriter.extend_nfs(args_nfs, head, arity);
1338 : }
1339 :
1340 : // First calculate the code to be generated for the arguments.
1341 : // This provides the information which arguments are certainly in normal
1342 : // form, which can be used to optimise the result.
1343 :
1344 883 : std::stringstream code_for_arguments;
1345 883 : std::stringstream types_for_arguments;
1346 883 : args_nfs.fill(false);
1347 883 : calc_inner_terms(code_for_arguments, a, startarg, args_nfs, types_for_arguments, type_of_code_variables);
1348 :
1349 883 : if (require_normal_form)
1350 : {
1351 459 : if (target_for_output.empty())
1352 : {
1353 0 : result_type << "data_expression";
1354 0 : s << delayed_rewr_function_name(head, arity) << "(";
1355 : }
1356 : else
1357 : {
1358 459 : result_type << "data_expression";
1359 459 : s << m_padding << rewr_function_name(head, arity) << "(" << target_for_output << ", ";
1360 : }
1361 : }
1362 : else
1363 : {
1364 424 : s << delayed_rewr_function_name(head, arity);
1365 424 : result_type << delayed_rewr_function_name(head, arity);
1366 424 : if (arity>0)
1367 : {
1368 424 : s << "<" << types_for_arguments.str() << ">";
1369 424 : result_type << "<" << types_for_arguments.str() << ">";
1370 : }
1371 424 : s << "(";
1372 : }
1373 883 : s << code_for_arguments.str();
1374 883 : s << (code_for_arguments.str().empty()?"":", ") << "this_rewriter)";
1375 :
1376 883 : if (require_normal_form)
1377 : {
1378 459 : if (target_for_output.empty())
1379 : {
1380 0 : s << ".normal_form()";
1381 : }
1382 : else
1383 : {
1384 459 : s << ";\n";
1385 : }
1386 : }
1387 :
1388 883 : return require_normal_form;
1389 883 : }
1390 :
1391 0 : bool calc_inner_term_appl_lambda_abstraction(
1392 : std::ostream& s,
1393 : const std::string& target_for_output,
1394 : const application& a,
1395 : const abstraction& head,
1396 : const std::size_t startarg,
1397 : const bool require_normal_form,
1398 : std::ostream& result_type,
1399 : const std::map<variable,std::string>& type_of_code_variables)
1400 : {
1401 0 : assert(a.size() > 0); // TODO Take care that the application of this lambda is done without unnecessary rewriting.
1402 : // The problem is that the function rewrite_lambda_application rewrites all its arguments.
1403 : // This should be lifted to a templated function. Furthermore, in the not rewritten variant,
1404 : // all arguments are also rewritten to normal form, to guarantee that they are of sort dataexpression.
1405 0 : assert(is_lambda_binder(head.binding_operator()));
1406 0 : const std::size_t arity = a.size();
1407 :
1408 0 : if (require_normal_form)
1409 : {
1410 0 : nfs_array args_nfs(recursive_number_of_args(a));
1411 0 : args_nfs.fill(true);
1412 :
1413 0 : s << m_padding << appl_function(arity) << "(" + target_for_output + ",";
1414 0 : std::stringstream types_for_arguments;
1415 0 : calc_inner_term(s, "", head, startarg, true, types_for_arguments, type_of_code_variables);
1416 0 : s << ", ";
1417 0 : if (arity>0)
1418 : {
1419 0 : types_for_arguments << ", ";
1420 : }
1421 0 : calc_inner_terms(s, a, startarg, args_nfs,types_for_arguments, type_of_code_variables);
1422 0 : s << ");\n";
1423 0 : s << m_padding << "this_rewriter->rewrite_lambda_application(" << target_for_output << ", " << target_for_output;
1424 0 : result_type << "data_expression";
1425 :
1426 0 : s << ", sigma(this_rewriter));\n";
1427 0 : return require_normal_form;
1428 0 : }
1429 : else
1430 : {
1431 : // !require_normal_form
1432 0 : nfs_array args_nfs(arity);
1433 0 : args_nfs.fill(true);
1434 :
1435 0 : s << m_padding << appl_function(arity) << "(" << target_for_output;
1436 0 : std::stringstream types_for_arguments;
1437 0 : calc_inner_term(s, target_for_output, head, startarg, true, types_for_arguments, type_of_code_variables);
1438 0 : s << ", ";
1439 0 : if (arity>0)
1440 : {
1441 0 : types_for_arguments << ", ";
1442 : }
1443 0 : calc_inner_terms(s, a, startarg, args_nfs,types_for_arguments, type_of_code_variables);
1444 0 : s << ");\n";
1445 0 : s << m_padding << target_for_output << "= term_not_in_normalform(" << target_for_output << ");\n";
1446 0 : result_type << "term_not_in_normalform";
1447 0 : return require_normal_form;
1448 0 : }
1449 : }
1450 :
1451 136 : void write_application_to_stream_in_normal_form(
1452 : std::ostream& s,
1453 : const std::string& target_for_output,
1454 : const application& a,
1455 : const std::size_t startarg,
1456 : const std::map<variable,std::string>& type_of_code_variables)
1457 : {
1458 : // the application is either application(variable,t1,..,tn) or application(application(...),t1,..,tn).
1459 :
1460 136 : const std::size_t arity = a.size();
1461 136 : nfs_array rewr_args(arity);
1462 136 : rewr_args.fill(true);
1463 136 : std::stringstream dummy_result_type; // As we rewrite to normal forms, these are always data_expressions.
1464 :
1465 136 : if (target_for_output.empty())
1466 : {
1467 0 : if (is_variable(a.head()))
1468 : {
1469 0 : s << "application(";
1470 0 : calc_inner_term(s, "", down_cast<variable>(a.head()), startarg, true, dummy_result_type, type_of_code_variables);
1471 : }
1472 : else
1473 : {
1474 0 : assert(is_application(a.head()));
1475 0 : s << "application(";
1476 0 : write_application_to_stream_in_normal_form(s,"",down_cast<application>(a.head()),startarg, type_of_code_variables);
1477 : }
1478 0 : for(const data_expression& t: a)
1479 : {
1480 0 : s << ", ";
1481 :
1482 0 : calc_inner_term(s, "", t, startarg, rewr_args, dummy_result_type, type_of_code_variables);
1483 : }
1484 0 : s << ")";
1485 : }
1486 : else
1487 : {
1488 136 : if (is_variable(a.head()))
1489 : {
1490 136 : s << m_padding << appl_function(arity) << "(" << target_for_output << ",";
1491 136 : calc_inner_term(s, "", down_cast<variable>(a.head()), startarg, true, dummy_result_type, type_of_code_variables);
1492 : }
1493 : else
1494 : {
1495 0 : assert(is_application(a.head()));
1496 0 : write_application_to_stream_in_normal_form(s,target_for_output,down_cast<application>(a.head()),startarg, type_of_code_variables);
1497 0 : s << m_padding << appl_function(arity) << "(" << target_for_output << "," << target_for_output;
1498 0 : std::stringstream dummy_result_type; // As we rewrite to normal forms, these are always data_expressions.
1499 0 : }
1500 374 : for(const data_expression& t: a)
1501 : {
1502 238 : s << ", ";
1503 :
1504 238 : calc_inner_term(s, "", t, startarg, rewr_args, dummy_result_type, type_of_code_variables);
1505 : }
1506 136 : s << ");\n";
1507 : }
1508 136 : }
1509 :
1510 104 : std::string delayed_application(const std::size_t arity)
1511 : {
1512 104 : m_delayed_application_functions.insert(arity);
1513 104 : std::stringstream s;
1514 104 : s << "delayed_application" << arity;
1515 208 : return s.str();
1516 104 : }
1517 :
1518 104 : void write_delayed_application_to_stream_in_normal_form(
1519 : std::ostream& s,
1520 : const application& a,
1521 : const std::size_t startarg,
1522 : std::ostream& result_type,
1523 : const std::map<variable,std::string>& type_of_code_variables)
1524 : {
1525 : // the application is either application(variable,t1,..,tn) or application(application(...),t1,..,tn).
1526 :
1527 104 : const std::size_t arity = a.size();
1528 104 : nfs_array rewr_args(arity);
1529 104 : rewr_args.fill(true);
1530 104 : std::stringstream code_string;
1531 104 : std::stringstream result_types;
1532 :
1533 104 : if (is_variable(a.head()))
1534 : {
1535 104 : calc_inner_term(code_string, "", down_cast<variable>(a.head()), startarg, true, result_types, type_of_code_variables);
1536 : }
1537 : else
1538 : {
1539 0 : assert(is_application(a.head()));
1540 0 : write_delayed_application_to_stream_in_normal_form(code_string,down_cast<application>(a.head()),startarg, result_types, type_of_code_variables);
1541 : }
1542 :
1543 276 : for(const data_expression& t: a)
1544 : {
1545 172 : result_types << ",";
1546 172 : code_string << ", ";
1547 172 : calc_inner_term(code_string, "", t, startarg, true, result_types, type_of_code_variables);
1548 : }
1549 :
1550 104 : s << delayed_application(arity) << "<" << result_types.str() << ">(";
1551 104 : s << code_string.str();
1552 104 : s << ", this_rewriter)";
1553 :
1554 104 : result_type << "delayed_application" << arity << "<" << result_types.str() << ">";
1555 104 : }
1556 :
1557 240 : bool calc_inner_term_appl_variable
1558 : (std::ostream& s,
1559 : const std::string& target_for_output,
1560 : const application& a,
1561 : const std::size_t startarg,
1562 : const bool require_normal_form,
1563 : std::ostream& result_type,
1564 : const std::map<variable,std::string>& type_of_code_variables)
1565 : {
1566 240 : if (require_normal_form)
1567 : {
1568 136 : result_type << "data_expression";
1569 136 : if (target_for_output.empty())
1570 : {
1571 0 : s << "rewrite_with_arguments_in_normal_form(";
1572 0 : write_application_to_stream_in_normal_form(s,"",a,startarg, type_of_code_variables);
1573 0 : s << ", this_rewriter)";
1574 : }
1575 : else
1576 : {
1577 136 : write_application_to_stream_in_normal_form(s,target_for_output,a,startarg, type_of_code_variables);
1578 136 : s << m_padding << "rewrite_with_arguments_in_normal_form(" << target_for_output << ", "
1579 136 : << target_for_output << ", this_rewriter);\n";
1580 : }
1581 136 : return true;
1582 : }
1583 :
1584 : // Generate an application which is rewritten when it is needed.
1585 104 : write_delayed_application_to_stream_in_normal_form(s,a,startarg, result_type, type_of_code_variables);
1586 104 : return false;
1587 : }
1588 :
1589 1123 : bool calc_inner_term_application(std::ostream& s,
1590 : const std::string& target_for_output,
1591 : const application& a,
1592 : const std::size_t startarg,
1593 : const bool require_normal_form,
1594 : std::ostream& result_type,
1595 : const std::map<variable,std::string>& type_of_code_variables)
1596 : {
1597 1123 : const data_expression head=get_nested_head(a);
1598 :
1599 1123 : if (is_function_symbol(head)) // Determine whether the topmost symbol is a function symbol.
1600 : {
1601 883 : return calc_inner_term_appl_function(s, target_for_output, a, down_cast<function_symbol>(head), startarg, require_normal_form, result_type, type_of_code_variables);
1602 : }
1603 :
1604 240 : if (is_abstraction(head)) // Here we must consider the case where head is an abstraction, and hence it must be a lambda abstraction.
1605 : {
1606 0 : return calc_inner_term_appl_lambda_abstraction(s, target_for_output, a, down_cast<abstraction>(head), startarg, require_normal_form, result_type, type_of_code_variables);
1607 : }
1608 :
1609 240 : assert(is_variable(head)); // Here we must consider the case where head is a variable.
1610 240 : return calc_inner_term_appl_variable(s, target_for_output, a, startarg, require_normal_form, result_type, type_of_code_variables);
1611 1123 : }
1612 :
1613 : ///
1614 : /// \brief calc_inner_term generates C++ code that reconstructs data expression t.
1615 : /// \param s is the stream to write the generated code to.
1616 : /// \param target_for_output is a reference expression to which the output must be assigned, or in case of the empty string,
1617 : // it is the result of the expression.
1618 : /// \param t is the data expression to be reconstructed in the generated code.
1619 : /// \param startarg gives the index of the position of t in the surrounding application (0 for head position, 1 for first argument, etc.)
1620 : /// \param require_normal_form indicates whether the reconstructed data expression should be rewritten to normal form.
1621 : /// \param type_of_code_variables gives the type of the variables used in the generated C++ code. data_expression means is in normal form.
1622 : /// \return True if the result is in normal form, false otherwise.
1623 : ///
1624 3608 : void calc_inner_term(std::ostream& s,
1625 : const std::string& target_for_output,
1626 : const data_expression& t,
1627 : const std::size_t startarg,
1628 : const bool require_normal_form,
1629 : std::ostream& result_type,
1630 : const std::map<variable,std::string>& type_of_code_variables)
1631 : {
1632 3608 : if (find_free_variables(t).empty())
1633 : {
1634 486 : if (target_for_output.empty())
1635 : {
1636 43 : RewriterCompilingJitty::substitution_type sigma;
1637 43 : s << m_rewriter.m_nf_cache->insert(m_rewriter.jitty_rewriter(t,sigma));
1638 43 : }
1639 : else
1640 : {
1641 443 : RewriterCompilingJitty::substitution_type sigma;
1642 443 : s << m_padding << target_for_output
1643 : << ".unprotected_assign<false>("
1644 886 : << m_rewriter.m_nf_cache->insert(m_rewriter.jitty_rewriter(t,sigma))
1645 886 : << ");\n";
1646 443 : }
1647 486 : result_type << "data_expression";
1648 486 : return;
1649 : }
1650 3122 : assert(!is_function_symbol(t)); // This will never be reached, as it is dealt with in the if clause above.
1651 :
1652 3122 : if (is_variable(t))
1653 : {
1654 1955 : calc_inner_term_variable(s, target_for_output, down_cast<variable>(t), require_normal_form, result_type, type_of_code_variables);
1655 1955 : return;
1656 : }
1657 1167 : if (is_abstraction(t))
1658 : {
1659 44 : calc_inner_term_abstraction(s, target_for_output, down_cast<abstraction>(t), startarg, require_normal_form, result_type, type_of_code_variables);
1660 44 : return;
1661 : }
1662 1123 : if (is_where_clause(t))
1663 : {
1664 0 : calc_inner_term_where_clause(s, target_for_output, down_cast<where_clause>(t), startarg, require_normal_form, result_type, type_of_code_variables);
1665 0 : return;
1666 : }
1667 :
1668 1123 : assert(is_application(t));
1669 1123 : calc_inner_term_application(s, target_for_output, down_cast<application>(t), startarg, require_normal_form, result_type, type_of_code_variables);
1670 : }
1671 :
1672 : ///
1673 : /// \brief calc_inner_terms calls calc_inner_term on all arguments of t, passing the corresponding
1674 : /// bools in the rewr array as the rewr parameter. Returns the booleans returned by those
1675 : /// calls as a vector.
1676 : ///
1677 883 : void calc_inner_terms(std::ostream& s,
1678 : const application& appl,
1679 : const std::size_t startarg,
1680 : const nfs_array& rewr, /// A Boolean would be enough. TODO:
1681 : std::ostream& argument_types,
1682 : const std::map<variable,std::string>& type_of_code_variables)
1683 : {
1684 2488 : for(std::size_t i=0; i<recursive_number_of_args(appl); ++i)
1685 : {
1686 1605 : if (i > 0)
1687 : {
1688 722 : s << ", ";
1689 722 : argument_types << ", ";
1690 : }
1691 1605 : std::stringstream argument_string;
1692 1605 : std::stringstream argument_type;
1693 1605 : assert(i<rewr.size());
1694 1605 : calc_inner_term(argument_string, "", get_argument_of_higher_order_term(appl,i), startarg + i, rewr.at(i),
1695 : argument_type, type_of_code_variables);
1696 1605 : s << argument_string.str();
1697 1605 : argument_types << argument_type.str();
1698 1605 : }
1699 883 : }
1700 :
1701 : /*
1702 : * implement_tree helper methods.
1703 : * type_of_code_variables gives a mapping from the variables used in the generated code.
1704 : * if it is "data_expression" then it is a normal form. Otherwise it is a template type, which
1705 : * may or may not be a normal form.
1706 : *
1707 : */
1708 :
1709 7028 : void implement_tree(std::ostream& m_stream,
1710 : const match_tree& tree,
1711 : std::size_t cur_arg,
1712 : std::size_t parent,
1713 : std::size_t level,
1714 : std::size_t cnt,
1715 : const std::size_t arity,
1716 : const function_symbol& opid,
1717 : bracket_level_data& brackets,
1718 : std::stack<std::string>& auxiliary_code_fragments,
1719 : std::map<variable,std::string>& type_of_code_variables)
1720 : {
1721 : /* Some c++ compilers cannot deal with more than 256 nestings of curly braces ({...}).
1722 : If too many curly braces are generated, a new method is generated, with as only purpose
1723 : to avoid too many brackets. The resulting code fragments are stored in auxiliary_code_fragments.
1724 : */
1725 7028 : if (brackets.bracket_nesting_level>brackets.MCRL2_BRACKET_NESTING_LEVEL)
1726 : {
1727 : static std::size_t auxiliary_method_name_index=0;
1728 :
1729 0 : m_stream << m_padding
1730 0 : << "auxiliary_function_to_reduce_bracket_nesting" << auxiliary_method_name_index << "(result, "
1731 0 : << brackets.current_data_arguments.top() << ",this_rewriter);\n";
1732 0 : m_stream << m_padding
1733 0 : << "if (!result.is_default_data_expression()) { return; }\n";
1734 :
1735 0 : const std::size_t old_indent=m_padding.reset();
1736 0 : std::stringstream s;
1737 0 : s << " template < " << brackets.current_template_parameters << ">\n"
1738 0 : << " static inline void auxiliary_function_to_reduce_bracket_nesting" << auxiliary_method_name_index
1739 : << "(data_expression& result"
1740 0 : << brackets.current_data_parameters.top() << (brackets.current_data_parameters.top().empty()?"":", ") << "RewriterCompilingJitty* this_rewriter)\n"
1741 : << " {\n"
1742 0 : << " std::size_t old_stack_size=this_rewriter->m_rewrite_stack.stack_size();\n";
1743 :
1744 0 : auxiliary_method_name_index++;
1745 :
1746 0 : std::size_t old_bracket_nesting_level=brackets.bracket_nesting_level;
1747 0 : brackets.bracket_nesting_level=0;
1748 0 : implement_tree(s,tree,cur_arg,parent,level,cnt,arity, opid, brackets,auxiliary_code_fragments, type_of_code_variables);
1749 0 : brackets.bracket_nesting_level=old_bracket_nesting_level;
1750 : s << " make_data_expression(result); return; // This indicates that no result has been calculated;\n"
1751 : << " }\n"
1752 0 : << "\n";
1753 0 : m_padding.restore(old_indent);
1754 0 : auxiliary_code_fragments.push(s.str());
1755 0 : return;
1756 0 : }
1757 :
1758 7028 : if (tree.isS())
1759 : {
1760 1527 : implement_treeS(m_stream,atermpp::down_cast<match_tree_S>(tree), cur_arg, parent, level, cnt, arity, opid, brackets, auxiliary_code_fragments, type_of_code_variables);
1761 : }
1762 5501 : else if (tree.isM())
1763 : {
1764 368 : implement_treeM(m_stream,atermpp::down_cast<match_tree_M>(tree), cur_arg, parent, level, cnt, arity, opid, brackets, auxiliary_code_fragments, type_of_code_variables);
1765 : }
1766 5133 : else if (tree.isF())
1767 : {
1768 852 : implement_treeF(m_stream, atermpp::down_cast<match_tree_F>(tree), cur_arg, parent, level, cnt, arity, opid, brackets, auxiliary_code_fragments, type_of_code_variables);
1769 : }
1770 4281 : else if (tree.isD())
1771 : {
1772 584 : implement_treeD(m_stream, atermpp::down_cast<match_tree_D>(tree), level, cnt, arity, opid, brackets, auxiliary_code_fragments, type_of_code_variables);
1773 : }
1774 3697 : else if (tree.isN())
1775 : {
1776 1721 : implement_treeN(m_stream, atermpp::down_cast<match_tree_N>(tree), cur_arg, parent, level, cnt, arity, opid, brackets,auxiliary_code_fragments, type_of_code_variables);
1777 : }
1778 1976 : else if (tree.isC())
1779 : {
1780 58 : implement_treeC(m_stream, atermpp::down_cast<match_tree_C>(tree), cur_arg, parent, level, cnt, arity, opid, brackets, auxiliary_code_fragments, type_of_code_variables);
1781 : }
1782 1918 : else if (tree.isR())
1783 : {
1784 1251 : implement_treeR(m_stream, atermpp::down_cast<match_tree_R>(tree), cur_arg, level, type_of_code_variables);
1785 : }
1786 : else
1787 : {
1788 : // These are the only remaining case, where we do not have to do anything.
1789 667 : assert(tree.isA() || tree.isX() || tree.isMe());
1790 : }
1791 : }
1792 :
1793 : class matches
1794 : {
1795 : protected:
1796 : const aterm m_matchterm;
1797 :
1798 : public:
1799 1527 : matches(const aterm& matchterm)
1800 1527 : : m_matchterm(matchterm)
1801 1527 : {}
1802 :
1803 39845 : bool operator ()(const atermpp::aterm& t) const
1804 : {
1805 39845 : return t==m_matchterm;
1806 : }
1807 : };
1808 :
1809 1527 : void implement_treeS(
1810 : std::ostream& m_stream,
1811 : const match_tree_S& tree,
1812 : std::size_t cur_arg,
1813 : std::size_t parent,
1814 : std::size_t level,
1815 : std::size_t cnt,
1816 : const std::size_t arity,
1817 : const function_symbol& opid,
1818 : bracket_level_data& brackets,
1819 : std::stack<std::string>& auxiliary_code_fragments,
1820 : std::map<variable,std::string>& type_of_code_variables)
1821 : {
1822 1527 : const match_tree_S& treeS(tree);
1823 1527 : bool reset_current_data_parameters=false;
1824 1527 : if (atermpp::find_if(treeS.subtree(),matches(treeS.target_variable()))!=aterm_appl()) // treeS.target_variable occurs in treeS.subtree
1825 : {
1826 1503 : const std::string parameters = brackets.current_data_parameters.top();
1827 1503 : brackets.current_data_parameters.push(parameters + (parameters.empty()?"":", ") + "const data_expression& " + (std::string(treeS.target_variable().name()).c_str() + 1));
1828 1503 : const std::string arguments = brackets.current_data_arguments.top();
1829 1503 : brackets.current_data_arguments.push(arguments + (arguments.empty()?"":", ") + (std::string(treeS.target_variable().name()).c_str() + 1));
1830 1503 : reset_current_data_parameters=true;
1831 :
1832 1503 : if (level == 0)
1833 : {
1834 1171 : if (m_used[cur_arg])
1835 : {
1836 330 : m_stream << m_padding << "const data_expression& " << std::string(treeS.target_variable().name()).c_str() + 1 << " = ";
1837 330 : m_stream << "arg" << cur_arg << "; // S1a\n";
1838 :
1839 330 : type_of_code_variables[treeS.target_variable()]="data_expression";
1840 : }
1841 : else
1842 : {
1843 841 : m_stream << m_padding << "const DATA_EXPR" << cur_arg <<"& " << std::string(treeS.target_variable().name()).c_str() + 1 << " = ";
1844 841 : m_stream << "arg_not_nf" << cur_arg << "; // S1b\n";
1845 841 : type_of_code_variables[treeS.target_variable()]="DATA_EXPR" + std::to_string(cur_arg);
1846 : }
1847 : }
1848 : else
1849 : {
1850 332 : m_stream << m_padding << "const data_expression& " << std::string(treeS.target_variable().name()).c_str() + 1 << " = ";
1851 : m_stream << "down_cast<data_expression>("
1852 332 : << (level == 1 ? "arg" : "t") << parent << "[" << cur_arg << "]"
1853 332 : << "); // S2\n";
1854 332 : type_of_code_variables[treeS.target_variable()]="data_expression";
1855 : }
1856 1503 : }
1857 1527 : implement_tree(m_stream, tree.subtree(), cur_arg, parent, level, cnt, arity, opid, brackets, auxiliary_code_fragments, type_of_code_variables);
1858 1527 : if (reset_current_data_parameters)
1859 : {
1860 1503 : brackets.current_data_parameters.pop();
1861 1503 : brackets.current_data_arguments.pop();
1862 : }
1863 1527 : }
1864 :
1865 368 : void implement_treeM(
1866 : std::ostream& m_stream,
1867 : const match_tree_M& tree,
1868 : std::size_t cur_arg,
1869 : std::size_t parent,
1870 : std::size_t level,
1871 : std::size_t cnt,
1872 : const std::size_t arity,
1873 : const function_symbol& opid,
1874 : bracket_level_data& brackets,
1875 : std::stack<std::string>& auxiliary_code_fragments,
1876 : std::map<variable,std::string>& type_of_code_variables)
1877 : {
1878 368 : m_stream << m_padding << "if (" << std::string(tree.match_variable().name()).c_str() + 1 << " == ";
1879 368 : if (level == 0)
1880 : {
1881 335 : m_stream << "arg" << cur_arg;
1882 : }
1883 : else
1884 : {
1885 33 : m_stream << (level == 1 ? "arg" : "t") << parent << "[" << cur_arg << "]";
1886 : }
1887 368 : m_stream << ") // M\n" << m_padding
1888 368 : << "{\n";
1889 368 : brackets.bracket_nesting_level++;
1890 368 : m_padding.indent();
1891 368 : implement_tree(m_stream, tree.true_tree(), cur_arg, parent, level, cnt, arity, opid, brackets, auxiliary_code_fragments, type_of_code_variables);
1892 368 : m_padding.unindent();
1893 368 : brackets.bracket_nesting_level--;
1894 368 : m_stream << m_padding
1895 368 : << "}\n" << m_padding
1896 368 : << "else\n" << m_padding
1897 368 : << "{\n";
1898 368 : brackets.bracket_nesting_level++;
1899 368 : m_padding.indent();
1900 368 : implement_tree(m_stream, tree.false_tree(), cur_arg, parent, level, cnt, arity, opid, brackets, auxiliary_code_fragments, type_of_code_variables);
1901 368 : m_padding.unindent();
1902 368 : brackets.bracket_nesting_level--;
1903 368 : m_stream << m_padding
1904 368 : << "}\n";
1905 368 : }
1906 :
1907 852 : void implement_treeF(
1908 : std::ostream& m_stream,
1909 : const match_tree_F& tree,
1910 : std::size_t cur_arg,
1911 : std::size_t parent,
1912 : std::size_t level,
1913 : std::size_t cnt,
1914 : const std::size_t arity,
1915 : const function_symbol& opid,
1916 : bracket_level_data& brackets,
1917 : std::stack<std::string>& auxiliary_code_fragments,
1918 : std::map<variable,std::string>& type_of_code_variables)
1919 : {
1920 852 : bool reset_current_data_parameters=false;
1921 852 : const void* func = (void*)(atermpp::detail::address(tree.function()));
1922 852 : m_stream << m_padding;
1923 852 : brackets.bracket_nesting_level++;
1924 852 : if (level == 0)
1925 : {
1926 740 : if (!is_function_sort(tree.function().sort()))
1927 : {
1928 519 : m_stream << "if (uint_address(arg" << cur_arg << ") == " << func << ") // F1\n" << m_padding
1929 519 : << "{\n";
1930 : }
1931 : else
1932 : {
1933 221 : m_stream << "if (uint_address((is_function_symbol(arg" << cur_arg << ") ? arg" << cur_arg << " : arg" << cur_arg << "[0])) == "
1934 221 : << func << ") // F1\n" << m_padding
1935 221 : << "{\n";
1936 : }
1937 : }
1938 : else
1939 : {
1940 112 : const char* arg_or_t = level == 1 ? "arg" : "t";
1941 112 : if (!is_function_sort(tree.function().sort()))
1942 : {
1943 105 : m_stream << "if (uint_address(" << arg_or_t << parent << "[" << cur_arg << "]) == "
1944 105 : << func << ") // F2a " << tree.function().name() << "\n" << m_padding
1945 105 : << "{\n" << m_padding
1946 105 : << " const data_expression& t" << cnt << " = down_cast<data_expression>(" << arg_or_t << parent << "[" << cur_arg << "]);\n";
1947 : }
1948 : else
1949 : {
1950 7 : m_stream << "if (is_application_no_check(down_cast<data_expression>(" << arg_or_t << parent << "[" << cur_arg << "])) && "
1951 7 : << "uint_address(down_cast<data_expression>(" << arg_or_t << parent << "[" << cur_arg << "])[0]) == "
1952 7 : << func << ") // F2b " << tree.function().name() << "\n" << m_padding
1953 7 : << "{\n" << m_padding
1954 7 : << " const data_expression& t" << cnt << " = down_cast<data_expression>(" << arg_or_t << parent << "[" << cur_arg << "]);\n";
1955 : }
1956 112 : const std::string parameters = brackets.current_data_parameters.top();
1957 112 : brackets.current_data_parameters.push(parameters + (parameters.empty()?"":", ") + "const data_expression& t" + std::to_string(cnt));
1958 112 : const std::string arguments = brackets.current_data_arguments.top();
1959 112 : brackets.current_data_arguments.push(arguments + (arguments.empty()?"t":", t") + std::to_string(cnt));
1960 :
1961 112 : reset_current_data_parameters=true;
1962 112 : }
1963 852 : m_stack.push_back(cur_arg);
1964 852 : m_stack.push_back(parent);
1965 852 : m_padding.indent();
1966 852 : implement_tree(m_stream, tree.true_tree(), 1, level == 0 ? cur_arg : cnt, level + 1, cnt + 1, arity, opid, brackets, auxiliary_code_fragments, type_of_code_variables);
1967 852 : if (reset_current_data_parameters)
1968 : {
1969 112 : brackets.current_data_parameters.pop();
1970 112 : brackets.current_data_arguments.pop();
1971 : }
1972 852 : m_padding.unindent();
1973 852 : m_stack.pop_back();
1974 852 : m_stack.pop_back();
1975 852 : m_stream << m_padding
1976 852 : << "}\n" << m_padding
1977 852 : << "else\n" << m_padding
1978 852 : << "{\n";
1979 852 : m_padding.indent();
1980 852 : implement_tree(m_stream, tree.false_tree(), cur_arg, parent, level, cnt, arity, opid, brackets, auxiliary_code_fragments, type_of_code_variables);
1981 852 : m_padding.unindent();
1982 852 : m_stream << m_padding
1983 852 : << "}\n";
1984 852 : brackets.bracket_nesting_level--;
1985 852 : }
1986 :
1987 584 : void implement_treeD(
1988 : std::ostream& m_stream,
1989 : const match_tree_D& tree,
1990 : std::size_t level,
1991 : std::size_t cnt,
1992 : const std::size_t arity,
1993 : const function_symbol& opid,
1994 : bracket_level_data& brackets,
1995 : std::stack<std::string>& auxiliary_code_fragments,
1996 : std::map<variable,std::string>& type_of_code_variables)
1997 : {
1998 584 : int i = m_stack.back();
1999 584 : m_stack.pop_back();
2000 584 : int j = m_stack.back();
2001 584 : m_stack.pop_back();
2002 584 : implement_tree(m_stream, tree.subtree(), j, i, level - 1, cnt, arity, opid, brackets, auxiliary_code_fragments, type_of_code_variables);
2003 584 : m_stack.push_back(j);
2004 584 : m_stack.push_back(i);
2005 584 : }
2006 :
2007 1721 : void implement_treeN(
2008 : std::ostream& m_stream,
2009 : const match_tree_N& tree,
2010 : std::size_t cur_arg,
2011 : std::size_t parent,
2012 : std::size_t level,
2013 : std::size_t cnt,
2014 : const std::size_t arity,
2015 : const function_symbol& opid,
2016 : bracket_level_data& brackets,
2017 : std::stack<std::string>& auxiliary_code_fragments,
2018 : std::map<variable,std::string>& type_of_code_variables)
2019 : {
2020 1721 : implement_tree(m_stream, tree.subtree(), cur_arg + 1, parent, level, cnt, arity, opid, brackets, auxiliary_code_fragments, type_of_code_variables);
2021 1721 : }
2022 :
2023 58 : void implement_treeC(
2024 : std::ostream& m_stream,
2025 : const match_tree_C& tree,
2026 : std::size_t cur_arg,
2027 : std::size_t parent,
2028 : std::size_t level,
2029 : std::size_t cnt,
2030 : const std::size_t arity,
2031 : const function_symbol& opid,
2032 : bracket_level_data& brackets,
2033 : std::stack<std::string>& auxiliary_code_fragments,
2034 : std::map<variable,std::string>& type_of_code_variables)
2035 : {
2036 58 : std::stringstream result_type_string;
2037 58 : calc_inner_term(m_stream, "result", tree.condition(), 0, true, result_type_string, type_of_code_variables);
2038 58 : m_stream << m_padding
2039 58 : << "if (result == sort_bool::true_()) // C\n" << m_padding
2040 58 : << "{\n";
2041 :
2042 58 : brackets.bracket_nesting_level++;
2043 58 : m_padding.indent();
2044 58 : implement_tree(m_stream, tree.true_tree(), cur_arg, parent, level, cnt, arity, opid, brackets, auxiliary_code_fragments, type_of_code_variables);
2045 58 : m_padding.unindent();
2046 :
2047 58 : m_stream << m_padding
2048 58 : << "}\n" << m_padding
2049 58 : << "else\n" << m_padding
2050 58 : << "{\n";
2051 :
2052 58 : m_padding.indent();
2053 58 : implement_tree(m_stream, tree.false_tree(), cur_arg, parent, level, cnt, arity, opid, brackets, auxiliary_code_fragments, type_of_code_variables);
2054 58 : m_padding.unindent();
2055 :
2056 58 : m_stream << m_padding
2057 58 : << "}\n";
2058 58 : brackets.bracket_nesting_level--;
2059 58 : }
2060 :
2061 1251 : void implement_treeR(
2062 : std::ostream& m_stream,
2063 : const match_tree_R& tree,
2064 : std::size_t cur_arg,
2065 : std::size_t level,
2066 : const std::map<variable,std::string>& type_of_code_variables)
2067 : {
2068 1251 : if (level > 0)
2069 : {
2070 399 : cur_arg = m_stack[2 * level - 1];
2071 : }
2072 :
2073 1251 : std::stringstream result_type_string;
2074 1251 : calc_inner_term(m_stream, "result", tree.result(), cur_arg + 1, true, result_type_string, type_of_code_variables);
2075 1251 : m_stream << m_padding << "this_rewriter->m_rewrite_stack.reset_stack_size(old_stack_size);\n"
2076 1251 : << m_padding << "return; // R1 " << tree.result() << "\n";
2077 1251 : }
2078 :
2079 0 : const match_tree& implement_treeC(
2080 : std::ostream& m_stream,
2081 : const match_tree_C& tree,
2082 : bracket_level_data& brackets,
2083 : const std::map<variable,std::string>& type_of_code_variables)
2084 : {
2085 0 : std::stringstream result_type_string;
2086 0 : assert(tree.true_tree().isR());
2087 0 : calc_inner_term(m_stream, "result", tree.condition(), 0, true, result_type_string, type_of_code_variables);
2088 0 : m_stream << ";\n" << m_padding
2089 0 : << "if (result == sort_bool::true_()) // C\n" << m_padding
2090 0 : << "{\n";
2091 0 : brackets.bracket_nesting_level++;
2092 0 : calc_inner_term(m_stream, "result", match_tree_R(tree.true_tree()).result(), 0, true, result_type_string, type_of_code_variables);
2093 0 : m_stream << ";\n"
2094 0 : << m_padding << "this_rewriter->m_rewrite_stack.reset_stack_size(old_stack_size);\n"
2095 0 : << m_padding << "return ";
2096 0 : brackets.bracket_nesting_level--;
2097 0 : m_stream << ";\n" << m_padding
2098 0 : << "}\n" << m_padding
2099 0 : << "else\n" << m_padding
2100 0 : << "{\n" << m_padding;
2101 0 : m_padding.indent();
2102 0 : return tree.false_tree();
2103 0 : }
2104 :
2105 0 : void implement_treeR(
2106 : std::ostream& m_stream,
2107 : const match_tree_R& tree,
2108 : std::size_t arity,
2109 : const std::map<variable,std::string>& type_of_code_variables)
2110 : {
2111 0 : std::stringstream result_type_string;
2112 0 : if (arity == 0)
2113 : {
2114 0 : calc_inner_term(m_stream, "result", tree.result(), 0, true, result_type_string, type_of_code_variables);
2115 0 : m_stream << ";\n" << m_padding
2116 0 : << m_padding << "this_rewriter->m_rewrite_stack.reset_stack_size(old_stack_size);\n"
2117 0 : << m_padding << "return; // R2a\n";
2118 : }
2119 : else
2120 : {
2121 : // arity>0
2122 0 : calc_inner_term(m_stream, "result", tree.result(), 0, true, result_type_string, type_of_code_variables);
2123 0 : m_stream << ";\n"
2124 0 : << m_padding << "this_rewriter->m_rewrite_stack.reset_stack_size(old_stack_size);\n"
2125 0 : << m_padding << "return; // R2b\n";
2126 : }
2127 0 : }
2128 :
2129 : public:
2130 5 : ImplementTree(RewriterCompilingJitty& rewr, function_symbol_vector& function_symbols)
2131 5 : : m_rewriter(rewr), m_padding(2)
2132 : {
2133 445 : for (function_symbol_vector::const_iterator it = function_symbols.begin(); it != function_symbols.end(); ++it)
2134 : {
2135 440 : const std::size_t max_arity = getArity(*it);
2136 1816 : for (std::size_t arity = 0; arity <= max_arity; ++arity)
2137 : {
2138 1376 : if (arity_is_allowed(it->sort(), arity))
2139 : {
2140 : // Register this <symbol, arity, nfs> tuple as a function that needs to be generated
2141 897 : static_cast<void>(rewr_function_name(*it, arity));
2142 : }
2143 : }
2144 : }
2145 5 : }
2146 :
2147 5 : const std::set<rewr_function_spec>& implemented_rewrs()
2148 : {
2149 5 : return m_rewr_functions_implemented;
2150 : }
2151 :
2152 : ///
2153 : /// \brief implement_tree
2154 : /// \param tree
2155 : /// \param arity
2156 : ///
2157 640 : void implement_tree(
2158 : std::ostream& m_stream,
2159 : match_tree tree,
2160 : const std::size_t arity,
2161 : const function_symbol& opid,
2162 : bracket_level_data& brackets,
2163 : std::stack<std::string>& auxiliary_code_fragments,
2164 : std::map<variable,std::string>& type_of_code_variables)
2165 : {
2166 : /* for (std::size_t i = 0; i < arity; ++i)
2167 : {
2168 : if (!m_used[i])
2169 : {
2170 : m_nnfvars.push_front(atermpp::aterm_int(i));
2171 : }
2172 : } */
2173 :
2174 640 : std::size_t l = 0;
2175 640 : while (tree.isC())
2176 : {
2177 0 : tree = implement_treeC(m_stream, down_cast<match_tree_C>(tree),brackets, type_of_code_variables);
2178 0 : l++;
2179 : }
2180 :
2181 640 : if (tree.isR())
2182 : {
2183 0 : implement_treeR(m_stream, down_cast<match_tree_R>(tree), arity, type_of_code_variables);
2184 : }
2185 : else
2186 : {
2187 640 : implement_tree(m_stream, tree, 0, 0, 0, 0, arity, opid, brackets, auxiliary_code_fragments, type_of_code_variables);
2188 : }
2189 :
2190 : // Close braces opened by implement_tree(std ostream&, onst match_tree_C&)
2191 640 : while (0 < l--)
2192 : {
2193 0 : m_padding.unindent();
2194 0 : m_stream << m_padding << "}\n";
2195 : }
2196 640 : }
2197 :
2198 2 : std::string implement_body_of_cplusplus_defined_function(
2199 : const std::size_t arity,
2200 : const std::string& target_for_output,
2201 : const std::string& head,
2202 : const function_sort& s,
2203 : std::size_t& used_arguments)
2204 : {
2205 : // In this case opid is used in a higher order fashion.
2206 2 : assert(!target_for_output.empty());
2207 2 : const std::size_t domain_size = s.domain().size();
2208 2 : std::stringstream ss;
2209 2 : ss << m_padding << appl_function(domain_size) << "(" << target_for_output << "," << head;
2210 :
2211 4 : for (std::size_t i = 0; i < domain_size; ++i)
2212 : {
2213 2 : ss << ", [&](data_expression& r){ local_rewrite(r, arg_not_nf" << used_arguments + i << "); }";
2214 : }
2215 2 : ss << ");\n";
2216 :
2217 2 : used_arguments += domain_size;
2218 2 : if (used_arguments<arity)
2219 : {
2220 0 : return ss.str() + implement_body_of_cplusplus_defined_function(arity,
2221 : target_for_output,
2222 : target_for_output,
2223 : down_cast<function_sort>(s.codomain()),
2224 0 : used_arguments);
2225 : }
2226 : else
2227 : {
2228 2 : return ss.str();
2229 : }
2230 2 : };
2231 :
2232 6 : void implement_a_cplusplus_defined_function(
2233 : std::ostream& m_stream,
2234 : const std::string& target_for_output,
2235 : std::size_t arity,
2236 : const function_symbol& opid,
2237 : const data_specification& data_spec)
2238 : {
2239 6 : m_stream << m_padding << "// Implement function " << opid << " by calling a user defined rewrite function.\n";
2240 :
2241 : /* m_stream << m_padding << "stack_increment++;\n"
2242 : << m_padding << "this_rewriter->m_rewrite_stack.increase(1);\n"
2243 : << m_padding << "data_expression& local_store=this_rewriter->m_rewrite_stack.top();\n"; */
2244 :
2245 6 : m_stream << m_padding << "data_expression& local_store=this_rewriter->m_rewrite_stack.new_stack_position();\n";
2246 :
2247 6 : const std::string cplusplus_function_name = data_spec.cpp_implemented_functions().find(opid)->second.second;
2248 :
2249 : // First calculate the core function, which may be surrounded by extra applications.
2250 6 : std::stringstream ss;
2251 6 : ss << cplusplus_function_name << "(";
2252 :
2253 20 : for(size_t i=0; i<get_direct_arity(opid); ++i)
2254 : {
2255 14 : ss << (i>0?",":"");
2256 14 : ss << "local_rewrite(arg_not_nf" << i << ")";
2257 : }
2258 6 : ss << ")";
2259 :
2260 6 : if (arity==get_direct_arity(opid))
2261 : {
2262 4 : if (target_for_output.empty())
2263 : {
2264 0 : m_stream << ss.str();
2265 : }
2266 : else
2267 : {
2268 : // m_stream << m_padding << target_for_output << " = " << ss.str() << ";\n";
2269 8 : m_stream << m_padding << target_for_output << ".assign(" << ss.str()
2270 4 : << ", *this_rewriter->m_thread_aterm_pool);\n";
2271 : }
2272 4 : return;
2273 : }
2274 : // else it is a higher order function, and it must be surrounded by "application"s.
2275 2 : assert(arity>get_direct_arity(opid));
2276 2 : std::size_t used_arguments = get_direct_arity(opid);
2277 2 : std::string result="local_store";
2278 8 : m_stream << m_padding << implement_body_of_cplusplus_defined_function(
2279 : arity,
2280 : result,
2281 4 : ss.str(),
2282 2 : down_cast<function_sort>(down_cast<function_sort>(opid.sort()).codomain()),
2283 2 : used_arguments) << ";\n";
2284 2 : assert(used_arguments == arity);
2285 :
2286 : // If there applications surrounding the term, it may not be a normalform anymore, but its arguments
2287 : // are in normal form. That is why rewrite_aux has as second argument true.
2288 2 : if (target_for_output.empty())
2289 : {
2290 0 : m_stream << m_padding << "data_expression result1; // TODO: optimize\n"
2291 0 : << m_padding << "rewrite_aux<true>(result1, " << result << ",this_rewriter);\n";
2292 : }
2293 : else
2294 : {
2295 2 : m_stream << m_padding << "rewrite_aux<true>(" << target_for_output << ", " << result << ",this_rewriter);\n";
2296 : }
2297 10 : }
2298 :
2299 897 : void implement_strategy(
2300 : std::ostream& m_stream,
2301 : match_tree_list strat,
2302 : std::size_t arity,
2303 : const function_symbol& opid,
2304 : bracket_level_data& brackets,
2305 : std::stack<std::string>& auxiliary_code_fragments,
2306 : const data_specification& data_spec)
2307 : {
2308 : // First check whether this is a predefined function with the right arity.
2309 907 : if (data_spec.cpp_implemented_functions().find(opid)!=data_spec.cpp_implemented_functions().end() &&
2310 10 : arity>=get_direct_arity(opid))
2311 : {
2312 6 : implement_a_cplusplus_defined_function(m_stream, "result", arity, opid, data_spec);
2313 6 : return;
2314 : }
2315 891 : bool added_new_parameters_in_brackets=false;
2316 891 : m_used=nfs_array(arity); // This vector maintains which arguments are in normal form.
2317 : // m_nnfvars=variable_or_number_list();
2318 891 : std::map<variable,std::string> type_of_code_variables;
2319 2253 : while (!strat.empty())
2320 : {
2321 1362 : m_stream << m_padding << "// " << strat.front() << "\n";
2322 1362 : if (strat.front().isA())
2323 : {
2324 722 : std::size_t arg = match_tree_A(strat.front()).variable_index();
2325 722 : if (!m_used[arg])
2326 : {
2327 : // m_stream << m_padding << "const data_expression& arg" << arg << " = local_rewrite(arg_not_nf" << arg << ");\n";
2328 : /* m_stream << m_padding << "data_expression& arg" << arg << " = this_rewriter->m_rewrite_stack.new_stack_position();\n"
2329 : << m_padding << "local_rewrite(arg" << arg << ", arg_not_nf" << arg << ");\n"; */
2330 :
2331 722 : m_stream << m_padding << "data_expression& arg" << arg
2332 722 : << "(std::is_convertible<DATA_EXPR" << arg << ", const data_expression&>::value?(const_cast<data_expression&>(reinterpret_cast<const data_expression&>(arg_not_nf" << arg << "))):this_rewriter->m_rewrite_stack.new_stack_position());\n"
2333 722 : << m_padding << "if constexpr (!std::is_convertible<DATA_EXPR" << arg << ", const data_expression&>::value)\n"
2334 722 : << m_padding << "{\n"
2335 722 : << m_padding << " local_rewrite(arg" << arg << ", arg_not_nf" << arg << ");\n"
2336 722 : << m_padding << "}\n";
2337 722 : m_used[arg] = true;
2338 722 : if (!added_new_parameters_in_brackets)
2339 : {
2340 319 : added_new_parameters_in_brackets=true;
2341 319 : brackets.current_data_parameters.push(brackets.current_data_parameters.top());
2342 319 : brackets.current_data_arguments.push(brackets.current_data_arguments.top());
2343 : }
2344 722 : const std::string& parameters=brackets.current_data_parameters.top();
2345 722 : brackets.current_data_parameters.top()=parameters + (parameters.empty()?"":", ") + "const data_expression& arg" + std::to_string(arg);
2346 722 : const std::string arguments = brackets.current_data_arguments.top();
2347 722 : brackets.current_data_arguments.top()=arguments + (arguments.empty()?"":", ") + "arg" + std::to_string(arg);
2348 722 : }
2349 722 : m_stream << m_padding << "// Considering argument " << arg << "\n";
2350 : }
2351 : else
2352 : {
2353 640 : m_stream << m_padding << "{\n";
2354 640 : m_padding.indent();
2355 640 : implement_tree(m_stream, strat.front(), arity, opid, brackets, auxiliary_code_fragments, type_of_code_variables);
2356 640 : m_padding.unindent();
2357 640 : m_stream << m_padding << "}\n";
2358 : }
2359 1362 : strat = strat.tail();
2360 : }
2361 891 : rewr_function_finish(m_stream, arity, opid);
2362 891 : if (added_new_parameters_in_brackets)
2363 : {
2364 319 : brackets.current_data_parameters.pop();
2365 319 : brackets.current_data_arguments.pop();
2366 : }
2367 891 : }
2368 :
2369 2472 : std::string get_heads(const sort_expression& s, const std::string& base_string, const std::size_t number_of_arguments)
2370 : {
2371 2472 : std::stringstream ss;
2372 2472 : if (is_function_sort(s) && number_of_arguments>0)
2373 : {
2374 300 : const function_sort fs(s);
2375 300 : ss << "down_cast<application>(" << get_heads(fs.codomain(),base_string,number_of_arguments-fs.domain().size()) << ".head())";
2376 300 : return ss.str();
2377 300 : }
2378 2172 : return base_string;
2379 2472 : }
2380 :
2381 : ///
2382 : /// \brief get_recursive_argument provides the index-th argument of an expression provided in
2383 : /// base_string, given that its head symbol has type s and there are number_of_arguments
2384 : /// arguments. Example: if f:D->E->F and index is 0, base_string is "t", base_string is
2385 : /// set to "atermpp::down_cast<application>(t[0])[0]
2386 : /// \param s
2387 : /// \param index
2388 : /// \param base_string
2389 : /// \param number_of_arguments
2390 : /// \return
2391 : ///
2392 2172 : void get_recursive_argument(std::ostream& m_stream, function_sort s, std::size_t index, const std::string& base_string, std::size_t number_of_arguments)
2393 : {
2394 2340 : while (index >= s.domain().size())
2395 : {
2396 168 : assert(is_function_sort(s.codomain()));
2397 168 : index -= s.domain().size();
2398 168 : number_of_arguments -= s.domain().size();
2399 168 : s = down_cast<function_sort>(s.codomain());
2400 : }
2401 2172 : m_stream << get_heads(s.codomain(), base_string, number_of_arguments - s.domain().size()) << "[" << index << "]";
2402 2172 : }
2403 :
2404 5 : void generate_delayed_application_functions(std::ostream& ss)
2405 : {
2406 17 : for(std::size_t arity: m_delayed_application_functions)
2407 : {
2408 12 : assert(arity>0);
2409 12 : ss << m_padding << "template < class HEAD";
2410 33 : for (std::size_t i = 0; i < arity; ++i)
2411 : {
2412 21 : ss << ", class DATA_EXPR" << i;
2413 : }
2414 12 : ss << " >\n";
2415 :
2416 12 : ss << m_padding << "class delayed_application" << arity << "\n"
2417 12 : << m_padding << "{\n";
2418 12 : m_padding.indent();
2419 12 : ss << m_padding << "protected:\n";
2420 12 : m_padding.indent();
2421 :
2422 12 : ss << m_padding << "const HEAD& m_head;\n";
2423 33 : for (std::size_t i = 0; i < arity; ++i)
2424 : {
2425 21 : ss << m_padding << "const DATA_EXPR" << i << "& m_arg" << i << ";\n";
2426 : }
2427 12 : ss << m_padding << "RewriterCompilingJitty* this_rewriter;\n\n";
2428 12 : m_padding.unindent();
2429 12 : ss << m_padding << "public:\n";
2430 12 : m_padding.indent();
2431 :
2432 12 : ss << m_padding << "delayed_application" << arity << "(const HEAD& head";
2433 33 : for (std::size_t i = 0; i < arity; ++i)
2434 : {
2435 21 : ss << ", const DATA_EXPR" << i << "& arg" << i;
2436 : }
2437 12 : ss << ", RewriterCompilingJitty* tr)\n";
2438 12 : ss << m_padding << " : m_head(head)";
2439 :
2440 33 : for (std::size_t i = 0; i < arity; ++i)
2441 : {
2442 21 : ss << ", m_arg" << i << "(arg" << i << ")";
2443 : }
2444 12 : ss << ", this_rewriter(tr)\n" << m_padding << "{}\n\n";
2445 :
2446 12 : ss << m_padding << "data_expression& normal_form() const\n";
2447 12 : ss << m_padding << "{\n";
2448 12 : m_padding.indent();
2449 :
2450 12 : ss << m_padding << "data_expression& local_store=this_rewriter->m_rewrite_stack.new_stack_position();\n"
2451 12 : << m_padding << appl_function(arity) << "(local_store, [&](data_expression& r){ local_rewrite(r, m_head); }";
2452 : /* ss << m_padding << "this_rewriter->m_rewrite_stack.increase(1);\n"
2453 : << m_padding << "data_expression& local_store=this_rewriter->m_rewrite_stack.top();\n"
2454 : << m_padding << "stack_increment++;\n"
2455 : << m_padding << appl_function(arity) << "(local_store, [&](data_expression& r){ local_rewrite(r, m_head); }"; */
2456 33 : for (std::size_t i = 0; i < arity; ++i)
2457 : {
2458 21 : ss << ", [&](data_expression& r){ local_rewrite(r, m_arg" << i << "); }";
2459 : }
2460 12 : ss << ");\n";
2461 12 : ss << m_padding << "rewrite_with_arguments_in_normal_form(local_store, local_store, this_rewriter);\n"
2462 12 : << m_padding << "return local_store;\n";
2463 :
2464 12 : m_padding.unindent();
2465 12 : ss << m_padding << "}\n\n";
2466 :
2467 12 : ss << m_padding << "void normal_form(data_expression& result) const\n";
2468 12 : ss << m_padding << "{\n";
2469 12 : m_padding.indent();
2470 :
2471 12 : ss << m_padding << appl_function(arity) << "(result, [&](data_expression& result){ local_rewrite(result, m_head); }";
2472 33 : for (std::size_t i = 0; i < arity; ++i)
2473 : {
2474 21 : ss << ", [&](data_expression& result){ local_rewrite(result, m_arg" << i << "); }";
2475 : }
2476 12 : ss << ");\n";
2477 12 : ss << m_padding << "rewrite_with_arguments_in_normal_form(result, result, this_rewriter);\n";
2478 :
2479 12 : m_padding.unindent();
2480 12 : ss << m_padding << "}\n\n";
2481 12 : m_padding.unindent();
2482 12 : m_padding.unindent();
2483 12 : ss << m_padding << "};\n\n";
2484 : }
2485 :
2486 5 : }
2487 :
2488 451 : void rewr_function_finish_term(std::ostream& m_stream,
2489 : const std::size_t arity,
2490 : const std::string& head,
2491 : const function_sort& s)
2492 : {
2493 451 : if (arity == 0)
2494 : {
2495 0 : m_stream << m_padding << "result = " << head << ";\n";
2496 0 : return;
2497 : }
2498 :
2499 451 : sort_expression current_sort=s;
2500 451 : std::size_t used_arguments=0;
2501 950 : while (used_arguments<arity)
2502 : {
2503 499 : assert(is_function_sort(current_sort)); // otherwise used_arguments == arity == 0, excluded above.
2504 499 : const function_sort& fs = atermpp::down_cast<function_sort>(current_sort);
2505 499 : const std::size_t domain_size = fs.domain().size();
2506 499 : current_sort = fs.codomain();
2507 :
2508 499 : m_stream << m_padding << appl_function(domain_size) << "(result, ";
2509 499 : if (used_arguments>0)
2510 : {
2511 48 : m_stream << "result";
2512 : }
2513 : else
2514 : {
2515 451 : m_stream << head;
2516 : }
2517 :
2518 1569 : for (std::size_t i = 0; i < domain_size; ++i)
2519 : {
2520 1070 : if (m_used[used_arguments + i])
2521 : {
2522 722 : m_stream << ", arg" << used_arguments + i;
2523 : }
2524 : else
2525 : {
2526 348 : m_stream << ", [&](data_expression& result){ local_rewrite(result, arg_not_nf" << used_arguments + i << "); }";
2527 : }
2528 : }
2529 499 : m_stream << ");\n";
2530 499 : used_arguments += domain_size;
2531 : }
2532 451 : assert(used_arguments==arity);
2533 451 : }
2534 :
2535 :
2536 891 : void rewr_function_finish(std::ostream& m_stream, std::size_t arity, const data::function_symbol& opid)
2537 : {
2538 : // Note that arity is the total arity, of all function symbols.
2539 891 : if (arity == 0)
2540 : {
2541 440 : m_stream << m_padding << "result.unprotected_assign<false>(";
2542 440 : RewriterCompilingJitty::substitution_type sigma;
2543 440 : m_stream << m_rewriter.m_nf_cache->insert(m_rewriter.jitty_rewriter(opid,sigma)) << ");\n";
2544 440 : }
2545 : else
2546 : {
2547 451 : std::stringstream ss;
2548 451 : ss << "this_rewriter->normal_forms_for_constants["
2549 451 : << atermpp::detail::index_traits<data::function_symbol, function_symbol_key_type, 2>::index(opid)
2550 451 : << "]";
2551 451 : rewr_function_finish_term(m_stream, arity, ss.str(), down_cast<function_sort>(opid.sort()));
2552 451 : }
2553 891 : }
2554 :
2555 897 : void rewr_function_signature(std::ostream& m_stream, std::size_t index, std::size_t arity, bracket_level_data& brackets)
2556 : {
2557 : // Constant function symbols (a == 0) can be passed by reference
2558 897 : if (arity>0)
2559 : {
2560 457 : m_stream << m_padding << "template < ";
2561 457 : std::stringstream s;
2562 1543 : for (std::size_t i = 0; i < arity; ++i)
2563 : {
2564 :
2565 : s << (i == 0 ? "" : ", ")
2566 1086 : << "class DATA_EXPR" << i;
2567 : }
2568 457 : m_stream << s.str() << ">\n";
2569 457 : brackets.current_template_parameters = s.str();
2570 457 : }
2571 897 : m_stream << m_padding << "static inline void"
2572 897 : << " rewr_" << index << "_" << arity << "(data_expression& result";
2573 :
2574 897 : std::stringstream arguments;
2575 897 : std::stringstream parameters;
2576 1983 : for (std::size_t i = 0; i < arity; ++i)
2577 : {
2578 1086 : parameters << ", const DATA_EXPR" << i << "& arg_not_nf"
2579 1086 : << i;
2580 1086 : arguments << (i == 0 ? "" : ", ") << "arg_not_nf" << i;
2581 : }
2582 897 : m_stream << parameters.str() << ", RewriterCompilingJitty* this_rewriter)\n";
2583 897 : brackets.current_data_arguments.push(arguments.str());
2584 897 : brackets.current_data_parameters.push(parameters.str());
2585 897 : }
2586 :
2587 897 : void rewr_function_implementation(
2588 : std::ostream& m_stream,
2589 : const data::function_symbol& func,
2590 : std::size_t arity,
2591 : match_tree_list strategy,
2592 : const data_specification& data_spec)
2593 :
2594 : {
2595 897 : bracket_level_data brackets;
2596 897 : std::stack<std::string> auxiliary_code_fragments;
2597 :
2598 897 : std::size_t index = atermpp::detail::index_traits<data::function_symbol, function_symbol_key_type, 2>::index(func);
2599 897 : m_stream << m_padding << "// [" << index << "] " << func << ": " << func.sort() << "\n";
2600 897 : rewr_function_signature(m_stream, index, arity, brackets);
2601 897 : m_stream << m_padding << "{\n"
2602 897 : << m_padding << " mcrl2::utilities::mcrl2_unused(this_rewriter); // Suppress warning\n"
2603 897 : << m_padding << " std::size_t old_stack_size=this_rewriter->m_rewrite_stack.stack_size();\n";
2604 897 : m_padding.indent();
2605 897 : implement_strategy(m_stream, strategy, arity, func, brackets, auxiliary_code_fragments,data_spec);
2606 897 : m_stream << m_padding << "this_rewriter->m_rewrite_stack.reset_stack_size(old_stack_size);\n"
2607 897 : << m_padding << "return;\n";
2608 897 : m_padding.unindent();
2609 897 : m_stream << m_padding << "}\n\n";
2610 :
2611 897 : if (arity>0)
2612 : {
2613 457 : m_stream << m_padding <<
2614 457 : "static inline void rewr_" << index << "_" << arity << "_term"
2615 : "(data_expression& result, const application&" << (arity == 0 ? "" : " t") << ", RewriterCompilingJitty* this_rewriter) "
2616 457 : "{ rewr_" << index << "_" << arity << "(result";
2617 1543 : for(std::size_t i = 0; i < arity; ++i)
2618 : {
2619 1086 : assert(is_function_sort(func.sort()));
2620 1086 : m_stream << ", term_not_in_normal_form(";
2621 1086 : get_recursive_argument(m_stream, down_cast<function_sort>(func.sort()), i, "t", arity);
2622 1086 : m_stream << ", this_rewriter)";
2623 : }
2624 457 : m_stream << ", this_rewriter); }\n\n";
2625 :
2626 457 : m_stream << m_padding <<
2627 457 : "static inline void rewr_" << index << "_" << arity << "_term_arg_in_normal_form"
2628 : "(data_expression& result, const application&" << (arity == 0 ? "" : " t") << ", RewriterCompilingJitty* this_rewriter) "
2629 457 : "{ rewr_" << index << "_" << arity << "(result";
2630 1543 : for(std::size_t i = 0; i < arity; ++i)
2631 : {
2632 1086 : assert(is_function_sort(func.sort()));
2633 1086 : m_stream << ", ";
2634 1086 : get_recursive_argument(m_stream, down_cast<function_sort>(func.sort()), i, "t", arity);
2635 : }
2636 457 : m_stream << ", this_rewriter); }\n\n";
2637 : }
2638 :
2639 897 : while (!auxiliary_code_fragments.empty())
2640 : {
2641 0 : m_stream << auxiliary_code_fragments.top();
2642 0 : auxiliary_code_fragments.pop();
2643 : }
2644 897 : m_stream << "\n";
2645 897 : }
2646 :
2647 128 : void generate_delayed_normal_form_generating_function(std::ostream& m_stream, const data::function_symbol& func, std::size_t arity)
2648 : {
2649 128 : std::size_t index = atermpp::detail::index_traits<data::function_symbol, function_symbol_key_type, 2>::index(func);
2650 128 : m_stream << m_padding << "// [" << index << "] " << func << ": " << func.sort() << "\n";
2651 128 : if (arity>0)
2652 : {
2653 128 : m_stream << m_padding << "template < ";
2654 363 : for (std::size_t i = 0; i < arity; ++i)
2655 : {
2656 : m_stream << (i == 0 ? "" : ", ")
2657 235 : << "class DATA_EXPR" << i;
2658 : }
2659 128 : m_stream << ">\n";
2660 : }
2661 128 : m_stream << m_padding << "class delayed_rewr_" << index << "_" << arity << "\n";
2662 128 : m_stream << m_padding << "{\n";
2663 128 : m_padding.indent();
2664 128 : m_stream << m_padding << "protected:\n";
2665 128 : m_padding.indent();
2666 363 : for(std::size_t i = 0; i < arity; ++i)
2667 : {
2668 235 : m_stream << m_padding << "const DATA_EXPR" << i << "& m_t" << i << ";\n";
2669 : }
2670 128 : m_stream << m_padding << "RewriterCompilingJitty* this_rewriter;\n";
2671 128 : m_padding.unindent();
2672 128 : m_stream << m_padding << "public:\n";
2673 128 : m_padding.indent();
2674 128 : m_stream << m_padding << "delayed_rewr_" << index << "_" << arity << "(";
2675 363 : for(std::size_t i = 0; i < arity; ++i)
2676 : {
2677 235 : m_stream << (i==0?"":", ") << "const DATA_EXPR" << i << "& t" << i;
2678 : }
2679 128 : m_stream << (arity == 0 ? "" : ", ") << "RewriterCompilingJitty* tr)\n";
2680 128 : m_stream << m_padding << (arity==0?"":" : ");
2681 363 : for(std::size_t i = 0; i < arity; ++i)
2682 : {
2683 235 : m_stream << (i==0?"":", ") << "m_t" << i << "(t" << i << ")";
2684 : }
2685 : m_stream << (arity==0?"":", ") << "this_rewriter(tr)"
2686 128 : << (arity==0?"":"\n") << m_padding << "{}\n\n"
2687 128 : << m_padding << "data_expression& normal_form() const\n"
2688 128 : << m_padding << "{\n"
2689 : /* << m_padding << " this_rewriter->m_rewrite_stack.increase(1);\n"
2690 : << m_padding << " data_expression& local_store=this_rewriter->m_rewrite_stack.top();\n"
2691 : << m_padding << " stack_increment++;\n" */
2692 128 : << m_padding << " data_expression& local_store=this_rewriter->m_rewrite_stack.new_stack_position();\n"
2693 128 : << m_padding << " rewr_" << index << "_" << arity << "(local_store";
2694 363 : for(std::size_t i = 0; i < arity; ++i)
2695 : {
2696 235 : m_stream << ", m_t" << i;
2697 : }
2698 :
2699 128 : m_stream << (arity==0?"":", ") << "this_rewriter);\n"
2700 128 : << m_padding << " return local_store;\n"
2701 128 : << m_padding << "}\n";
2702 :
2703 128 : m_stream << m_padding << "void normal_form(data_expression& result) const\n"
2704 128 : << m_padding << "{\n"
2705 128 : << m_padding << " rewr_" << index << "_" << arity << "(result";
2706 363 : for(std::size_t i = 0; i < arity; ++i)
2707 : {
2708 235 : m_stream << ", m_t" << i;
2709 : }
2710 :
2711 128 : m_stream << (arity==0?"":", ") << "this_rewriter);\n"
2712 128 : << m_padding << "}\n";
2713 :
2714 128 : m_padding.unindent();
2715 128 : m_padding.unindent();
2716 128 : m_stream << m_padding << "};\n";
2717 128 : m_stream << m_padding << "\n";
2718 128 : }
2719 :
2720 5 : void generate_rewr_functions(std::ostream& m_stream, const data_specification& data_spec)
2721 : {
2722 1030 : while (!m_rewr_functions.empty())
2723 : {
2724 1025 : rewr_function_spec spec = m_rewr_functions.top();
2725 1025 : m_rewr_functions.pop();
2726 1025 : if (spec.delayed())
2727 : {
2728 128 : generate_delayed_normal_form_generating_function(m_stream, spec.fs(), spec.arity());
2729 : }
2730 : else
2731 : {
2732 897 : const match_tree_list strategy = m_rewriter.create_strategy(m_rewriter.jittyc_eqns[spec.fs()], spec.arity());
2733 897 : rewr_function_implementation(m_stream, spec.fs(), spec.arity(), strategy, data_spec);
2734 897 : }
2735 1025 : }
2736 5 : }
2737 : };
2738 :
2739 10 : void RewriterCompilingJitty::CleanupRewriteSystem()
2740 : {
2741 : // m_nf_cache.clear();
2742 10 : if (so_rewr_cleanup != nullptr)
2743 : {
2744 5 : so_rewr_cleanup();
2745 : }
2746 10 : }
2747 :
2748 : ///
2749 : /// \brief generate_cpp_filename creates a filename that is hopefully unique enough not to cause
2750 : /// name clashes when more than one instance of the compiling rewriter run at the same
2751 : /// time.
2752 : /// \param unique A number that will be incorporated into the filename.
2753 : /// \return A filename that should be used to store the generated C++ code in.
2754 : ///
2755 5 : static std::string generate_cpp_filename(std::size_t unique)
2756 : {
2757 5 : const char* env_dir = std::getenv("MCRL2_COMPILEDIR");
2758 5 : std::ostringstream filename;
2759 5 : std::string filedir;
2760 5 : if (env_dir)
2761 : {
2762 0 : filedir = env_dir;
2763 0 : if (*filedir.rbegin() != '/')
2764 : {
2765 0 : filedir.append("/");
2766 : }
2767 : }
2768 : else
2769 : {
2770 5 : filedir = "./";
2771 : }
2772 5 : time_t now = time(nullptr);
2773 5 : struct tm tstruct = *localtime(&now);
2774 :
2775 : // The static_cast<std::size_t> is required, as the calculation does not fit into a 32 bit int, yielding a negative number.
2776 5 : std::size_t unique_time = ((((static_cast<std::size_t>(tstruct.tm_year)*12+tstruct.tm_mon)*31+tstruct.tm_mday)*24+
2777 5 : tstruct.tm_hour)*60+tstruct.tm_min)*60 + tstruct.tm_sec;
2778 : // the name below must be unique. If two .cpp files have the same name, loading the second
2779 : // may effectively load the first. The pid of the current process and the this pointer in
2780 : // unique could lead to duplicate filenames, as happened in September 2021. A time tag has
2781 : // been added to guarantee further uniqueness.
2782 5 : filename << filedir << "jittyc_" << getpid() << "_" << (unique % 100000000) << "_" << unique_time << ".cpp";
2783 10 : return filename.str();
2784 5 : }
2785 :
2786 : ///
2787 : /// \brief filter_function_symbols selects the function symbols from source for which filter
2788 : /// returns true, and copies them to dest.
2789 : /// \param source The input list.
2790 : /// \param dest The output list.
2791 : /// \param filter A functor of type bool(const function_symbol&)
2792 : ///
2793 : template <class Filter>
2794 10 : void filter_function_symbols(const function_symbol_vector& source, function_symbol_vector& dest, Filter filter)
2795 : {
2796 825 : for (function_symbol_vector::const_iterator it = source.begin(); it != source.end(); ++it)
2797 : {
2798 815 : if (filter(*it))
2799 : {
2800 440 : dest.push_back(*it);
2801 : }
2802 : }
2803 10 : }
2804 :
2805 5 : void RewriterCompilingJitty::generate_code(const std::string& filename)
2806 : {
2807 5 : std::ofstream cpp_file(filename);
2808 5 : std::stringstream rewr_code;
2809 : // arity_bound is one larger than the maximal arity.
2810 5 : arity_bound = 1+std::max(calc_max_arity(m_data_specification_for_enumeration.constructors()),
2811 5 : calc_max_arity(m_data_specification_for_enumeration.mappings()));
2812 :
2813 : // - Store all used function symbols in a vector
2814 5 : std::vector<function_symbol> function_symbols;
2815 5 : filter_function_symbols(m_data_specification_for_enumeration.constructors(), function_symbols, data_equation_selector);
2816 5 : filter_function_symbols(m_data_specification_for_enumeration.mappings(), function_symbols, data_equation_selector);
2817 :
2818 :
2819 : // The rewrite functions are first stored in a separate buffer (rewrite_functions),
2820 : // because during the generation process, new function symbols are created. This
2821 : // affects the value that the macro INDEX_BOUND should have before loading
2822 : // jittycpreamble.h.
2823 5 : ImplementTree code_generator(*this, function_symbols);
2824 :
2825 5 : index_bound = atermpp::detail::index_traits<data::function_symbol, function_symbol_key_type, 2>::max_index() + 1;
2826 :
2827 5 : functions_when_arguments_are_not_in_normal_form = std::vector<rewriter_function>(arity_bound * index_bound);
2828 5 : functions_when_arguments_are_in_normal_form = std::vector<rewriter_function>(arity_bound * index_bound);
2829 :
2830 5 : cpp_file << "#define INDEX_BOUND__ " << index_bound << "// These values are not used anymore.\n"
2831 5 : "#define ARITY_BOUND__ " << arity_bound << "// These values are not used anymore.\n";
2832 5 : cpp_file << "#include \"mcrl2/data/detail/rewrite/jittycpreamble.h\"\n";
2833 :
2834 : cpp_file << "namespace {\n"
2835 : "// Anonymous namespace so the compiler uses internal linkage for the generated\n"
2836 : "// rewrite code.\n"
2837 : "\n"
2838 : "struct rewr_functions\n"
2839 : "{\n"
2840 :
2841 : " // A rewrite_term is a term that may or may not be in normal form. If the method\n"
2842 : " // normal_form is invoked, it will calculate a normal form for itself as efficiently as possible.\n"
2843 : " template <class REWRITE_TERM>\n"
2844 : " static data_expression& local_rewrite(const REWRITE_TERM& t)\n"
2845 : " {\n"
2846 : " return t.normal_form();\n"
2847 : " }\n"
2848 : "\n"
2849 : " // A rewrite_term is a term that may or may not be in normal form. If the method\n"
2850 : " // normal_form is invoked, it will calculate a normal form for itself as efficiently as possible.\n"
2851 : " template <class REWRITE_TERM>\n"
2852 : " static void local_rewrite(data_expression& result,\n"
2853 : " const REWRITE_TERM& t) \n"
2854 : " {\n"
2855 : " t.normal_form(result);\n"
2856 : " }\n"
2857 : "\n"
2858 : " static const data_expression& local_rewrite(const data_expression& t)\n"
2859 : " {\n"
2860 : " return t;\n"
2861 : " }\n"
2862 : "\n"
2863 : " static void local_rewrite(data_expression& result, const data_expression& t)\n"
2864 : " {\n"
2865 : " result=t;\n"
2866 : " }\n"
2867 5 : "\n";
2868 :
2869 : rewr_code << " // We're declaring static members in a struct rather than simple functions in\n"
2870 5 : " // the global scope, so that we don't have to worry about forward declarations.\n";
2871 5 : code_generator.generate_rewr_functions(rewr_code,m_data_specification_for_enumeration);
2872 : rewr_code << "};\n"
2873 5 : "} // namespace\n";
2874 :
2875 5 : code_generator.generate_delayed_application_functions(cpp_file);
2876 :
2877 5 : cpp_file << rewr_code.str();
2878 :
2879 : cpp_file << "void set_the_precompiled_rewrite_functions_in_a_lookup_table(RewriterCompilingJitty* this_rewriter)\n"
2880 5 : "{\n";
2881 5 : cpp_file << " assert(&this_rewriter->functions_when_arguments_are_not_in_normal_form == (void *)" << &functions_when_arguments_are_not_in_normal_form << "); // Check that this table matches the one rewriter is actually using.\n";
2882 5 : cpp_file << " assert(&this_rewriter->functions_when_arguments_are_in_normal_form == (void *)" << &functions_when_arguments_are_in_normal_form << "); // Check that this table matches the one rewriter is actually using.\n";
2883 : cpp_file << " for(rewriter_function& f: this_rewriter->functions_when_arguments_are_not_in_normal_form)\n"
2884 : << " {\n"
2885 : << " f = nullptr;\n"
2886 5 : << " }\n";
2887 : cpp_file << " for(rewriter_function& f: this_rewriter->functions_when_arguments_are_in_normal_form)\n"
2888 : << " {\n"
2889 : << " f = nullptr;\n"
2890 5 : << " }\n";
2891 :
2892 : // Fill tables with the rewrite functions
2893 5 : RewriterCompilingJitty::substitution_type sigma;
2894 5 : normal_forms_for_constants.clear();
2895 1030 : for (const rewr_function_spec& f: code_generator.implemented_rewrs())
2896 : {
2897 1025 : if (!f.delayed())
2898 : {
2899 897 : std::size_t index = atermpp::detail::index_traits<data::function_symbol, function_symbol_key_type, 2>::index(f.fs());
2900 897 : if (f.arity()>0)
2901 : {
2902 457 : cpp_file << " this_rewriter->functions_when_arguments_are_not_in_normal_form[this_rewriter->arity_bound * "
2903 457 : << index
2904 457 : << " + " << f.arity() << "] = rewr_functions::"
2905 457 : << f.name() << "_term;\n";
2906 457 : cpp_file << " this_rewriter->functions_when_arguments_are_in_normal_form[this_rewriter->arity_bound * "
2907 457 : << index
2908 457 : << " + " << f.arity() << "] = rewr_functions::"
2909 457 : << f.name() << "_term_arg_in_normal_form;\n";
2910 : }
2911 : else
2912 : {
2913 440 : if (index>=normal_forms_for_constants.size())
2914 : {
2915 440 : normal_forms_for_constants.resize(index+1);
2916 : }
2917 440 : normal_forms_for_constants[index]=jitty_rewriter(f.fs(),sigma);
2918 : }
2919 : }
2920 : }
2921 :
2922 :
2923 5 : cpp_file << "}\n";
2924 5 : cpp_file.close();
2925 5 : }
2926 :
2927 5 : void RewriterCompilingJitty::BuildRewriteSystem()
2928 : {
2929 5 : CleanupRewriteSystem();
2930 :
2931 : // Try to find out from environment which compile script to use.
2932 : // If not set, choose one of the following two:
2933 : // * if "mcrl2compilerewriter" is in the same directory as the executable,
2934 : // this is the version we favour. This is especially needed for single
2935 : // bundle applications on MacOSX. Furthermore, it is the more foolproof
2936 : // approach on other platforms.
2937 : // * by default, fall back to the system provided mcrl2compilerewriter script.
2938 : // in this case, we rely on the script being available in the user's
2939 : // $PATH environment variable.
2940 5 : std::string compile_script;
2941 5 : const char* env_compile_script = std::getenv("MCRL2_COMPILEREWRITER");
2942 5 : if (env_compile_script != nullptr)
2943 : {
2944 5 : compile_script = env_compile_script;
2945 : }
2946 0 : else if(mcrl2::utilities::file_exists(mcrl2::utilities::get_executable_basename() + "/mcrl2compilerewriter"))
2947 : {
2948 0 : compile_script = mcrl2::utilities::get_executable_basename() + "/mcrl2compilerewriter";
2949 : }
2950 : else
2951 : {
2952 0 : compile_script = "mcrl2compilerewriter";
2953 : }
2954 :
2955 5 : rewriter_so = std::shared_ptr<uncompiled_library>(new uncompiled_library(compile_script));
2956 :
2957 5 : mCRL2log(verbose) << "using '" << compile_script << "' to compile rewriter." << std::endl;
2958 5 : stopwatch time;
2959 :
2960 5 : jittyc_eqns.clear();
2961 933 : for(std::set < data_equation >::const_iterator it = rewrite_rules.begin(); it != rewrite_rules.end(); ++it)
2962 : {
2963 928 : jittyc_eqns[down_cast<function_symbol>(get_nested_head(it->lhs()))].push_front(*it);
2964 : }
2965 :
2966 5 : std::string cpp_file = generate_cpp_filename(reinterpret_cast<std::size_t>(this));
2967 5 : generate_code(cpp_file);
2968 :
2969 5 : mCRL2log(verbose) << "generated " << cpp_file << " in " << time.time() << "ms, compiling..." << std::endl;
2970 5 : time.reset();
2971 :
2972 : try
2973 : {
2974 5 : rewriter_so->compile(cpp_file);
2975 : }
2976 0 : catch(std::runtime_error& e)
2977 : {
2978 0 : rewriter_so->leave_files();
2979 0 : throw mcrl2::runtime_error(std::string("Could not compile rewriter: ") + e.what());
2980 0 : }
2981 :
2982 5 : mCRL2log(verbose) << "compiled in " << time.time() << "ms, loading rewriter..." << std::endl;
2983 :
2984 : bool (*init)(rewriter_interface*, RewriterCompilingJitty* this_rewriter);
2985 5 : rewriter_interface interface = { mcrl2::utilities::get_toolset_version(), "Unknown error when loading rewriter.", this, nullptr, nullptr };
2986 : try
2987 : {
2988 : typedef bool rewrite_function_type(rewriter_interface*, RewriterCompilingJitty*);
2989 5 : init = reinterpret_cast<rewrite_function_type*>(rewriter_so->proc_address("init"));
2990 : }
2991 0 : catch(std::runtime_error& e)
2992 : {
2993 0 : rewriter_so->leave_files();
2994 : #ifndef MCRL2_DISABLE_JITTYC_VERSION_CHECK
2995 0 : throw mcrl2::runtime_error(std::string("Could not load rewriter: ") + e.what());
2996 : #endif
2997 0 : }
2998 :
2999 : #ifdef NDEBUG // In non debug mode clear compiled files directly after loading.
3000 : if (logger::get_reporting_level()<debug) // leave the files in debug mode.
3001 : {
3002 : try
3003 : {
3004 : rewriter_so->cleanup();
3005 : }
3006 : catch (std::runtime_error& error)
3007 : {
3008 : mCRL2log(mcrl2::log::error) << "Could not cleanup temporary files: " << error.what() << std::endl;
3009 : }
3010 : }
3011 : #endif
3012 :
3013 5 : if (!init(&interface,this))
3014 : {
3015 : #ifndef MCRL2_DISABLE_JITTYC_VERSION_CHECK
3016 0 : throw mcrl2::runtime_error(std::string("Could not load rewriter: ") + interface.status);
3017 : #endif
3018 : }
3019 5 : so_rewr_cleanup = interface.rewrite_cleanup;
3020 5 : so_rewr = interface.rewrite_external;
3021 :
3022 5 : mCRL2log(verbose) << interface.status << std::endl;
3023 5 : }
3024 :
3025 5 : RewriterCompilingJitty::RewriterCompilingJitty(
3026 : const data_specification& data_spec,
3027 5 : const used_data_equation_selector& equation_selector)
3028 : : Rewriter(data_spec,equation_selector),
3029 5 : jitty_rewriter(data_spec,equation_selector),
3030 10 : m_nf_cache(new normal_form_cache())
3031 : {
3032 5 : thread_initialise();
3033 5 : assert(m_nf_cache->empty());
3034 5 : so_rewr_cleanup = nullptr;
3035 5 : so_rewr = nullptr;
3036 5 : rewriting_in_progress = false;
3037 :
3038 5 : made_files = false;
3039 5 : rewrite_rules.clear();
3040 :
3041 1652 : for (const data_equation& e: data_spec.equations())
3042 : {
3043 1647 : if (data_equation_selector(e))
3044 : {
3045 928 : const data_equation rule=e;
3046 : try
3047 : {
3048 928 : CheckRewriteRule(rule);
3049 928 : if (rewrite_rules.insert(rule).second)
3050 : {
3051 : // The equation has been added as a rewrite rule, otherwise the equation was already present.
3052 : // data_equation_selector.add_function_symbols(rule.lhs());
3053 : }
3054 : }
3055 0 : catch (std::runtime_error& error)
3056 : {
3057 0 : mCRL2log(warning) << error.what() << std::endl;
3058 0 : }
3059 928 : }
3060 : }
3061 :
3062 5 : BuildRewriteSystem();
3063 5 : }
3064 :
3065 15 : RewriterCompilingJitty::~RewriterCompilingJitty()
3066 : {
3067 5 : CleanupRewriteSystem();
3068 10 : }
3069 :
3070 6175 : void RewriterCompilingJitty::rewrite(
3071 : data_expression& result,
3072 : const data_expression& term,
3073 : substitution_type& sigma)
3074 : {
3075 : #ifdef MCRL2_DISPLAY_REWRITE_STATISTICS
3076 : data::detail::increment_rewrite_count();
3077 : #endif
3078 : // Save global sigma and restore it afterwards, as rewriting might be recursive with different
3079 : // substitutions, due to the enumerator.
3080 : // std::cerr << "REWRITE " << term << "\n";
3081 6175 : substitution_type *saved_sigma=global_sigma;
3082 6175 : global_sigma=σ
3083 6175 : if (rewriting_in_progress)
3084 : {
3085 0 : so_rewr(result,term, this);
3086 : }
3087 : else
3088 : {
3089 6175 : rewriting_in_progress=true;
3090 : try
3091 : {
3092 6175 : so_rewr(result,term, this);
3093 : }
3094 0 : catch (recalculate_term_as_stack_is_too_small&)
3095 : {
3096 0 : assert(!atermpp::detail::g_thread_term_pool().is_shared_locked());
3097 0 : rewriting_in_progress=false; // Restart rewriting, due to a stack overflow.
3098 : // The stack is a vector, and it may be relocated in memory when
3099 : // resized. References to the stack loose their validity.
3100 0 : m_rewrite_stack.reserve_more_space();
3101 0 : rewrite(result,term,sigma);
3102 : // std::cerr << "REWRITE " << term << " --> " << result << "\n";
3103 0 : return;
3104 0 : }
3105 6175 : rewriting_in_progress=false;
3106 6175 : assert(m_rewrite_stack.stack_size()==0);
3107 : }
3108 :
3109 6175 : global_sigma=saved_sigma;
3110 : // std::cerr << "REWRITE " << term << " --> " << result << "\n";
3111 6175 : return;
3112 : }
3113 :
3114 0 : data_expression RewriterCompilingJitty::rewrite(
3115 : const data_expression& term,
3116 : substitution_type& sigma)
3117 : {
3118 : // std::cerr << "REWRITE " << term << "\n";
3119 0 : data_expression result;
3120 0 : rewrite(result, term, sigma);
3121 : // std::cerr << "REWRITE " << term << " --> " << result << "\n";
3122 0 : return result;
3123 0 : }
3124 :
3125 0 : rewrite_strategy RewriterCompilingJitty::getStrategy()
3126 : {
3127 0 : return jitty_compiling;
3128 : }
3129 :
3130 : }
3131 : }
3132 : }
3133 :
3134 : #endif
|
