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