mCRL2
Loading...
Searching...
No Matches
jitty.cpp
Go to the documentation of this file.
1// Author(s): Muck van Weerdenburg, Jan Friso Groote
2// Copyright: see the accompanying file COPYING or copy at
3// https://github.com/mCRL2org/mCRL2/blob/master/COPYING
4//
5// Distributed under the Boost Software License, Version 1.0.
6// (See accompanying file LICENSE_1_0.txt or copy at
7// http://www.boost.org/LICENSE_1_0.txt)
8//
9
10#define NAME std::string("rewr_jitty")
11
14
15#include <boost/config.hpp>
16
18#include "mcrl2/data/replace.h"
19
20#ifdef MCRL2_DISPLAY_REWRITE_STATISTICS
22#endif
23
24using namespace mcrl2::log;
25using namespace mcrl2::core;
26using namespace mcrl2::core::detail;
27
28namespace mcrl2
29{
30namespace data
31{
32namespace detail
33{
34
35// The function below is intended to remove the auxiliary function this_term_is_in_normal_form from a term
36// such that it can for instance be pretty printed.
37
39{
40 if (is_machine_number(t))
41 {
42 return t;
43 }
44
45 if (is_variable(t))
46 {
47 return t;
48 }
49
50 if (is_function_symbol(t))
51 {
52 assert(t!=this_term_is_in_normal_form());
53 return t;
54 }
55
56 if (is_application(t))
57 {
58 const application& ta=atermpp::down_cast<application>(t);
60 {
61 assert(ta.size()==1);
62 return ta[0];
63 }
64
65 return application(ta.head(), ta.begin(), ta.end(), [&](const data_expression& t){ return remove_normal_form_function(t); });
66 }
67
68
69 if (is_where_clause(t))
70 {
71 const where_clause& t1=atermpp::down_cast<where_clause>(t);
72 const assignment_expression_list& assignments=t1.declarations();
73 const data_expression& body=t1.body();
74
75 assignment_vector new_assignments;
76 for(const assignment_expression& ae: assignments)
77 {
78 const assignment& assignment_expr = atermpp::down_cast<assignment>(ae);
79 new_assignments.push_back(assignment(assignment_expr.lhs(), remove_normal_form_function(assignment_expr.rhs())));
80 }
81 return where_clause(remove_normal_form_function(body),assignment_list(new_assignments.begin(),new_assignments.end()));
82 }
83
84 assert(is_abstraction(t));
85
86 const abstraction& t1=atermpp::down_cast<abstraction>(t);
87 const binder_type& binder=t1.binding_operator();
88 const variable_list& bound_variables=t1.variables();
89 const data_expression& body=t1.body();
90
91 return abstraction(binder, bound_variables, remove_normal_form_function(body));
92}
93
95{
96 protected:
99 public:
101 : m_sigma(sigma), m_r(r)
102 {}
103
105 {
106 m_r.rewrite_aux(result, t, m_sigma);
107 }
108};
109
111{
112 protected:
113 std::set<std::size_t> m_dependencies;
115
116 public:
119 {}
120
121 const std::set<std::size_t>& dependencies() const
122 {
123 return m_dependencies;
124 }
125
127 {
128 return m_equation;
129 }
130};
131
132
133
134
135
137{
138 if (i>=jitty_strat.size())
139 {
140 jitty_strat.resize(i+1);
141 }
142}
143
145{
146 jitty_strat.clear();
148 function_symbols.insert(function_symbols.end(), data_spec.mappings().begin(), data_spec.mappings().end());
149 for(const function_symbol& f: function_symbols)
150 {
151 if (equation_selector(f))
152 {
155 std::map< function_symbol, data_equation_list >::const_iterator j=jitty_eqns.find(f);
156 jitty_strat[i] =
157 (j==jitty_eqns.end()
158 ?create_strategy(f,data_equation_list(), data_spec)
159 :create_strategy(f,reverse(j->second), data_spec));
160 }
161 }
162
163}
164
165
167 const data_specification& data_spec,
168 const mcrl2::data::used_data_equation_selector& equation_selector):
169 Rewriter(data_spec,equation_selector),
170 this_term_is_in_normal_form_symbol(
171 std::string("Rewritten@@term"),
173 rewriting_in_progress(false)
174{
175 thread_initialise();
176 for (const data_equation& eq: data_spec.equations())
177 {
178 if (equation_selector(eq))
179 {
180 try
181 {
183 }
184 catch (std::runtime_error& e)
185 {
186 mCRL2log(warning) << e.what() << std::endl;
187 continue;
188 }
189
190 const function_symbol& lhs_head_index=atermpp::down_cast<function_symbol>(get_nested_head(eq.lhs()));
191
193 std::map< function_symbol, data_equation_list >::iterator it = jitty_eqns.find(lhs_head_index);
194 if (it != jitty_eqns.end())
195 {
196 n = it->second;
197 }
198 n.push_front(eq);
199 jitty_eqns[lhs_head_index] = n;
200 }
201 }
202
203 rebuild_strategy(data_spec, equation_selector);
204}
205
207{
208}
209
210// Find the variables that occur in the lhs and the rhs of the assignments;
211//
213{
214 std::set<variable> variables_in_substitution;
215 for(std::size_t i=0; i<assignments.size; ++i)
216 {
217 std::set<variable> s=find_free_variables(assignments.assignment[i].term);
218 variables_in_substitution.insert(s.begin(),s.end());
219 variables_in_substitution.insert(assignments.assignment[i].var);
220 }
221 return variables_in_substitution;
222}
223
225 data_expression& result,
226 const jitty_assignments_for_a_rewrite_rule& assignments,
227 const data_expression& t,
228 data::enumerator_identifier_generator& generator) // This generator is used for the generation of fresh variable names.
229{
230 if (is_machine_number(t))
231 {
232 result=t;
233 return;
234 }
235 if (is_function_symbol(t))
236 {
237 // result=t; The following is more efficient as it avoids a call to thread local variables. Should be removed in due time.
238 result.assign(t, *m_thread_aterm_pool);
239 return;
240 }
241 else if (is_variable(t))
242 {
243 for (std::size_t i=0; i<assignments.size; i++)
244 {
245 if (t==assignments.assignment[i].var)
246 {
247 if (assignments.assignment[i].variable_is_a_normal_form)
248 {
249 // Variables that are in normal form get a tag that they are in normal form.
251 return;
252 }
253 // result=assignments.assignment[i].term;
254 result.assign(assignments.assignment[i].term,
256 return;
257 }
258 }
259 // result=t;
260 result.assign(t, *m_thread_aterm_pool);
261 return;
262 }
263 else if (is_abstraction(t))
264 {
265 const abstraction& t1=atermpp::down_cast<abstraction>(t);
266 const binder_type& binder=t1.binding_operator();
267 const variable_list& bound_variables=t1.variables();
268 // Check that variables in the left and right hand sides of equations do not clash with bound variables.
269 std::set<variable> variables_in_substitution=bound_variables_in_substitution(assignments);
270 /* for(std::size_t i=0; i<assignments.size; ++i)
271 {
272 std::set<variable> s=find_free_variables(assignments.assignment[i].term);
273 variables_in_substitution.insert(s.begin(),s.end());
274 variables_in_substitution.insert(assignments.assignment[i].var);
275 } */
276
277 variable_vector new_variables;
279 bool sigma_trivial=true;
280 for(const variable& v: bound_variables)
281 {
282 if (variables_in_substitution.count(v)>0)
283 {
284 // Replace v in the list and in the body by a new variable name.
285 const variable fresh_variable(generator(),v.sort());
286 new_variables.push_back(fresh_variable);
287 sigma[v]=fresh_variable;
288 sigma_trivial=false;
289 }
290 else
291 {
292 new_variables.push_back(v);
293 }
294 }
295 subst_values(result,
296 assignments,
297 (sigma_trivial?t1.body():replace_variables(t1.body(),sigma)),
298 generator);
299 result=abstraction(binder,
300 variable_list(new_variables.begin(),new_variables.end()),
301 result);
302 return;
303 }
304 else if (is_where_clause(t))
305 {
306 const where_clause& t1=atermpp::down_cast<where_clause>(t);
307 const assignment_expression_list& local_assignments=t1.declarations();
308 const data_expression& body=t1.body();
309
310 std::set<variable> variables_in_substitution=bound_variables_in_substitution(assignments);
311
312 assignment_vector new_assignments;
313
315 bool sigma_trivial=true;
316
317 for(const assignment_expression& a: local_assignments)
318 {
319 const assignment& assignment_expr = atermpp::down_cast<assignment>(a);
320 const variable& v=assignment_expr.lhs();
321 subst_values(result,assignments,assignment_expr.rhs(),generator);
322 if (variables_in_substitution.count(v)>0)
323 {
324 // Replace variable in the assignment and in the body by a new variable name.
325 const variable fresh_variable(generator(),v.sort());
326 new_assignments.push_back(assignment(fresh_variable,result));
327 sigma[v]=fresh_variable;
328 sigma_trivial=false;
329 }
330 else
331 {
332 new_assignments.push_back(assignment(v,result));
333 }
334 }
335 subst_values(result,
336 assignments,
337 (sigma_trivial?body:replace_variables(body,sigma)),
338 generator),
339 result=where_clause(result, assignment_list(new_assignments.begin(),new_assignments.end()));
340 return;
341 }
342 else
343 {
344 const application& t1 = atermpp::down_cast<application>(t);
345 make_application(result,
346 t1.head(),
347 t1.begin(),
348 t1.end(),
349 [&](data_expression& result, const data_expression& t) -> void
350 { subst_values(result,assignments,t,generator); return;});
351 }
352}
353
354// Match term t with the lhs p of an equation.
355static bool match_jitty(
356 const data_expression& t,
357 const data_expression& p,
359 const bool term_context_guarantees_normal_form)
360{
361 if (is_machine_number(p))
362 {
363 return p==t;
364 }
365 else if (is_function_symbol(p))
366 {
367 return p==t;
368 }
369 else if (is_variable(p))
370 {
371
372 for (std::size_t i=0; i<assignments.size; i++)
373 {
374 if (p==assignments.assignment[i].var)
375 {
376 return t==assignments.assignment[i].term;
377 }
378 }
379
380 new (&assignments.assignment[assignments.size])
382 atermpp::down_cast<variable>(p),
383 t,
384 term_context_guarantees_normal_form);
385 assignments.size++;
386 return true;
387 }
388 else
389 {
391 {
392 return false;
393 }
394 // p and t must be applications.
395 assert(term_context_guarantees_normal_form); // If the argument must match an expression it must be a normal form.
396
397 const application& pa=atermpp::down_cast<application>(p);
398 const application& ta=atermpp::down_cast<application>(t);
399 if (pa.size()!=ta.size()) // are p and t applications of the same arity?
400 {
401 return false;
402 }
403
404
405 if (!match_jitty(ta.head(),
406 pa.head(),assignments,true))
407 {
408 return false;
409 }
410
411 for (std::size_t i=0; i<pa.size(); i++)
412 {
413 if (!match_jitty(ta[i], pa[i],assignments,true))
414 {
415 return false;
416 }
417 }
418
419 return true;
420 }
421}
422
423
424// This function applies the rewrite_cpp_code on a higher order term t with op as head symbol for
425// which the code in rewrite_cpp_code must be applied.
426template <class ITERATOR>
428 data_expression& result,
429 const application& t,
430 const std::function<void(data_expression&, const data_expression&)> rewrite_cpp_code,
431 ITERATOR begin,
432 ITERATOR end,
434{
435 if (is_function_symbol(t.head()))
436 {
437 data_expression intermediate;
438 make_application(intermediate, t.head(), begin, end);
439 rewrite_cpp_code(result, intermediate);
440 return;
441 }
442
443 const application& ta=atermpp::down_cast<application>(t.head());
444 std::size_t n_args=recursive_number_of_args(ta);
445 apply_cpp_code_to_higher_order_term(result,ta,rewrite_cpp_code,begin,begin+n_args,sigma);
446 const data_expression rewrite_result=result; /* TODO Optimize */
447 rewrite_aux(result,application(rewrite_result,
448 begin+n_args,
449 end,
450 [&](const data_expression& t){ return application(this_term_is_in_normal_form(),t); } ),
451 sigma);
452}
453
454
457 data_expression& result,
458 const data_expression& term,
460{
461 if (is_function_symbol(term))
462 {
463 assert(term!=this_term_is_in_normal_form());
464 rewrite_aux_const_function_symbol(result,atermpp::down_cast<const function_symbol>(term),sigma);
465 return;
466 }
467 if (is_variable(term))
468 {
469 sigma.apply(atermpp::down_cast<variable>(term),result, *m_thread_aterm_pool);
470 return;
471 }
472 if (is_machine_number(term))
473 {
474 result=term;
475 return;
476 }
477
478 if (is_where_clause(term))
479 {
480 const where_clause& w = atermpp::down_cast<where_clause>(term);
481 rewrite_where(result,w,sigma);
482 return;
483 }
484
485 if (is_abstraction(term))
486 {
487 const abstraction& ta=atermpp::down_cast<abstraction>(term);
488 if (is_exists(ta))
489 {
491 return;
492 }
493 if (is_forall(ta))
494 {
496 return;
497 }
498 assert(is_lambda(ta));
499 rewrite_single_lambda(result,ta.variables(),ta.body(),false,sigma);
500 return;
501 }
502
503 // Here term must have the shape appl(t1,...,tn)
504 assert(is_application(term));
505 {
506 const application& terma=atermpp::down_cast<application>(term);
507 if (terma.head()==this_term_is_in_normal_form())
508 {
509 assert(terma.size()==1);
510 assert(remove_normal_form_function(terma[0])==terma[0]);
511 // result=terma[0]; the following is more efficient.
512 result.assign(terma[0], *m_thread_aterm_pool);
513 return;
514 }
515
516 // The variable term has the shape appl(t,t1,...,tn);
517
518 // First check whether t has the shape appl(appl...appl(f,u1,...,un)(...)(...) where f is a function symbol.
519 // In this case rewrite that function symbol. This is an optimisation. If this does not apply t is rewritten,
520 // including all its subterms. But this is costly, as not all subterms will be rewritten again
521 // in rewrite_aux_function_symbol.
522
523 const data_expression& head=get_nested_head(term);
524
526 {
527 // return rewrite_aux_function_symbol(atermpp::down_cast<function_symbol>(head),term,sigma);
528 rewrite_aux_function_symbol(result, atermpp::down_cast<function_symbol>(head),terma,sigma);
529 return;
530 }
531
532 const application& tapp=atermpp::down_cast<application>(term);
533
534 // const data_expression t = rewrite_aux(tapp.head(),sigma);
536
537 const std::size_t t = 0; // Index of variable t in the stack.
539
540 // Here t has the shape f(u1,....,un)(u1',...,um')....: f applied several times to arguments,
541 // x(u1,....,un)(u1',...,um')....: x applied several times to arguments, or
542 // binder x1,...,xn.t' where the binder is a lambda, exists or forall.
543
544 const std::size_t head1 = 1; // Index of variable head1 in the stack.
547 {
548 // In this case t (is top of the rewrite stack) has the shape f(u1...un)(u1'...um').... where all u1,...,un,u1',...,um' are normal formas.
549 // In the invocation of rewrite_aux_function_symbol these terms are rewritten to normalform again.
550 make_application(result, m_rewrite_stack.element(t,2) , tapp.begin(), tapp.end());
552 atermpp::down_cast<function_symbol>(m_rewrite_stack.element(head1,2)),
553 atermpp::down_cast<application>(result),
554 sigma);
555 result=m_rewrite_stack.element(t,2);
557 return;
558 }
559 else if (is_variable(m_rewrite_stack.element(head1,2)))
560 {
561 // return appl(t,t1,...,tn) where t1,...,tn still need to be rewritten.
563 const bool do_not_rewrite_head=false;
564 make_application(result, m_rewrite_stack.element(t,2) , tapp.begin(), tapp.end(), r, do_not_rewrite_head); // Replacing r by a lambda term requires 16 more bytes on the stack.
566 return;
567 }
569 const abstraction& ta=atermpp::down_cast<abstraction>(m_rewrite_stack.element(t,2) );
570 const binder_type& binder(ta.binding_operator());
571 if (is_lambda_binder(binder))
572 {
573 rewrite_lambda_application(result,ta,tapp,sigma);
575 return;
576 }
577 if (is_exists_binder(binder))
578 {
579 assert(term.size()==1);
582 return;
583 }
584 assert(is_forall_binder(binder));
585 assert(term.size()==1);
588 return;
589 }
590}
591
593 data_expression& result,
594 const function_symbol& op,
595 const application& term,
597{
598 assert(is_function_sort(op.sort()));
599
600 const std::size_t arity=detail::recursive_number_of_args(term);
601 assert(arity>0);
602 // data_expression* rewritten = MCRL2_SPECIFIC_STACK_ALLOCATOR(data_expression, arity);
603 m_rewrite_stack.increase(arity+1);
604 bool* rewritten_defined = MCRL2_SPECIFIC_STACK_ALLOCATOR(bool, arity);
605
606 for(std::size_t i=0; i<arity; ++i)
607 {
608 rewritten_defined[i]=false;
609 }
610
613 const strategy& strat=jitty_strat[op_value];
614
615 if (!strat.rules().empty())
616 {
618 MCRL2_SPECIFIC_STACK_ALLOCATOR(jitty_variable_assignment_for_a_rewrite_rule, strat.number_of_variables()));
619
620 for (const strategy_rule& rule : strat.rules())
621 {
622 if (rule.is_rewrite_index())
623 {
624 const std::size_t i = rule.rewrite_index();
625 if (i < arity)
626 {
627 assert(!rewritten_defined[i]||i==0);
628 if (!rewritten_defined[i])
629 {
630 // new (&rewritten[i]) data_expression(rewrite_aux(detail::get_argument_of_higher_order_term(term,i),sigma));
632
633 rewritten_defined[i]=true;
634 }
635 // assert(rewritten[i].defined());
636 assert(m_rewrite_stack.element(i,arity+1).defined());
637 }
638 else
639 {
640 break;
641 }
642 }
643 else if (rule.is_cpp_code())
644 {
645 // Here it is assumed that precompiled code only works on the exact right number of arguments and
646 // precompiled functions are not used in a higher order fashion. Maybe this requires an explicit check.
647 assert(arity>0);
648 if (term.head()==op)
649 {
650 // application rewriteable_term(op, &rewritten[0], &rewritten[arity]);
651 assert(m_rewrite_stack.stack_size()>=arity+1);
652 application rewriteable_term(op, m_rewrite_stack.stack_iterator(0,arity+1),
653 m_rewrite_stack.stack_iterator(arity,arity+1)); /* TODO Optimize */
654 rule.rewrite_cpp_code()(result, rewriteable_term);
655 m_rewrite_stack.decrease(arity+1);
656 return;
657 }
658 else
659 {
660 // Guarantee that all higher order arguments are in normal form. Maybe this had to be done in the strategy for higher
661 // order terms.
662 for(std::size_t i=0; i<recursive_number_of_args(term); i++)
663 {
664 if (!rewritten_defined[i])
665 {
666 // new (&rewritten[i]) data_expression(rewrite_aux(detail::get_argument_of_higher_order_term(term,i),sigma));
668 rewritten_defined[i]=true;
669 }
670 }
671 // return apply_cpp_code_to_higher_order_term(term, rule.rewrite_cpp_code(), &rewritten[0], &rewritten[arity], sigma);
673 result,
674 term,
675 rule.rewrite_cpp_code(),
677 m_rewrite_stack.stack_iterator(arity,arity+1), sigma);
678 m_rewrite_stack.decrease(arity+1);
679 return;
680 }
681 }
682 else
683 {
684 const data_equation& rule1=rule.equation();
685 const data_expression& lhs=rule1.lhs();
686 std::size_t rule_arity = (is_function_symbol(lhs)?0:detail::recursive_number_of_args(lhs));
687
688 if (rule_arity > arity)
689 {
690 break;
691 }
692
693 assert(assignments.size==0);
694
695 bool matches = true;
696 for (std::size_t i=0; i<rule_arity; i++)
697 {
698 assert(i<arity);
699 if (!match_jitty(rewritten_defined[i]?
700 m_rewrite_stack.element(i,arity+1):
702 detail::get_argument_of_higher_order_term(atermpp::down_cast<application>(lhs),i),
703 assignments,rewritten_defined[i]))
704 {
705 matches = false;
706 break;
707 }
708 }
709 if (matches)
710 {
711 bool condition_of_this_rule=false;
712 if (rule1.condition()==sort_bool::true_())
713 {
714 condition_of_this_rule=true;
715 }
716 else
717 {
720 if (result==sort_bool::true_())
721 {
722 condition_of_this_rule=true;
723 }
724 }
725 if (condition_of_this_rule)
726 {
727 const data_expression& rhs=rule1.rhs();
728
729 if (arity == rule_arity)
730 {
731 // const data_expression result=rewrite_aux(subst_values(assignments,rhs,m_generator),sigma);
732 subst_values(m_rewrite_stack.top(),assignments,rhs,m_generator);
734 m_rewrite_stack.decrease(arity+1);
735 return;
736 }
737 else
738 {
739 assert(arity>rule_arity);
740 // There are more arguments than those that have been rewritten.
741 // Get those, put them in rewritten.
742
743 for(std::size_t i=rule_arity; i<arity; ++i)
744 {
746 rewritten_defined[i]=true;
747 }
748
749 subst_values(m_rewrite_stack.top(),assignments,rhs,m_generator);
750 std::size_t i = rule_arity;
752 while (is_function_sort(sort) && (i < arity))
753 {
754 const function_sort& fsort = atermpp::down_cast<function_sort>(sort);
755 const std::size_t end=i+fsort.domain().size();
756 assert(end-1<arity);
757 // result = application(result,&rewritten[0]+i,&rewritten[0]+end);
758 assert(m_rewrite_stack.stack_size()+i>=arity+1);
759 assert(end<arity+1);
760 assert(end>=i);
761
764 m_rewrite_stack.stack_iterator(end,arity+1));
765 i=end;
766 sort = fsort.codomain();
767 }
768
770 m_rewrite_stack.decrease(arity+1);
771 return;
772 }
773 }
774
775 }
776 assignments.size=0;
777 }
778 }
779 }
780
781 // No rewrite rule is applicable. Rewrite the not yet rewritten arguments.
782 // As we rewrite all, we do not record anymore whether terms are rewritten.
783
784 for (std::size_t i=0; i<arity; i++)
785 {
786 if (!rewritten_defined[i])
787 {
788 // new (&rewritten[i]) data_expression(rewrite_aux(detail::get_argument_of_higher_order_term(term,i),sigma));
790 }
791 }
792
793 // The while loop must always be iterated once. Therefore, the initial traversal is put before the
794 // main loop.
795 const function_sort& fsort=atermpp::down_cast<function_sort>(op.sort());
796 const std::size_t end=fsort.domain().size();
797
799 std::size_t i=end;
800 const sort_expression* sort = &fsort.codomain();
801 while (i<arity && is_function_sort(*sort))
802 {
803 const function_sort& fsort=atermpp::down_cast<function_sort>(*sort);
804 const std::size_t end=i+fsort.domain().size();
805 assert(m_rewrite_stack.stack_size()+i>=arity+1);
806 assert(end<arity+1);
807 assert(end>=i);
808 make_application(result,result,m_rewrite_stack.stack_iterator(i,arity+1), m_rewrite_stack.stack_iterator(end,arity+1));
809 i=end;
810 sort = &fsort.codomain();
811 }
812
813 m_rewrite_stack.decrease(arity+1);
814 return;
815}
816
818 data_expression& result,
819 const function_symbol& op,
821{
822 // This is special code to rewrite a function symbol. Note that the function symbol can be higher order,
823 // e.g., it can be a function symbol f for which a rewrite rule f(n)=... exists.
824
827
828 // Cache the rhs's as they are rewritten very often.
829 if (rhs_for_constants_cache.size()<=op_value)
830 {
831 rhs_for_constants_cache.resize(op_value+1);
832 }
833 const data_expression& cached_rhs = rhs_for_constants_cache[op_value];
834 if (!cached_rhs.is_default_data_expression())
835 {
836 // result=cached_rhs;
837 /* result.assign(cached_rhs,
838 this->m_busy_flag,
839 this->m_forbidden_flag,
840 *this->m_creation_depth); */
841 result.assign(cached_rhs, *m_thread_aterm_pool);
842 return;
843 }
844
845 const strategy& strat=jitty_strat[op_value];
846
847 for (const strategy_rule& rule : strat.rules())
848 {
849 if (rule.is_rewrite_index())
850 {
851 // In this case a standalone function symbol is rewritten, which could have arguments.
852 // It is not needed to rewrite the arguments.
853 break;
854 }
855 else if (rule.is_cpp_code())
856 {
857 rule.rewrite_cpp_code()(result, op);
858 rhs_for_constants_cache[op_value]=result;
859 return;
860 }
861 else
862 {
863 const data_equation& rule1=rule.equation();
864 const data_expression& lhs=rule1.lhs();
865 std::size_t rule_arity = (is_function_symbol(lhs)?0:detail::recursive_number_of_args(lhs));
866
867 if (rule_arity > 0)
868 {
869 break;
870 }
871
872 if (rule1.condition()==sort_bool::true_())
873 {
874 rewrite_aux(result,rule1.rhs(),sigma);
875 rhs_for_constants_cache[op_value]=result;
876 return;
877 }
878 rewrite_aux(result,rule1.condition(),sigma);
879 if (result==sort_bool::true_())
880 {
881 rewrite_aux(result,rule1.rhs(),sigma);
882 rhs_for_constants_cache[op_value]=result;
883 return;
884 }
885 }
886 }
887
888 rhs_for_constants_cache[op_value]=op;
889 result=op;
890 return;
891}
892
894 data_expression& result,
895 const data_expression& term,
897{
898#ifdef MCRL2_DISPLAY_REWRITE_STATISTICS
900#endif
902 {
903 rewrite_aux(result, term, sigma);
904 }
905 else
906 {
907 assert(m_rewrite_stack.stack_size()==0);
909 try
910 {
911 rewrite_aux(result, term, sigma);
912 }
914 {
915 rewriting_in_progress=false; // Restart rewriting, due to a stack overflow.
916 // The stack is a vector, and it may be relocated in memory when
917 // resized. References to the stack loose their validity.
919 rewrite(result,term,sigma);
920 return;
921 }
923 assert(m_rewrite_stack.stack_size()==0);
924 }
925
926 assert(remove_normal_form_function(result)==result);
927 return;
928}
929
931 const data_expression& term,
933{
934 data_expression result;
935 rewrite(result, term, sigma);
936 return result;
937}
938
939
941{
942 return jitty;
943}
944}
945}
946}
aterm_core & assign(const aterm_core &other, detail::thread_aterm_pool &pool) noexcept
Assignment operator, to be used if busy and forbidden flags are explicitly available.
size_type size() const
Returns the number of arguments of this term.
Definition aterm.h:151
A list of aterm objects.
Definition aterm_list.h:24
size_type size() const
Returns the size of the term_list.
Definition aterm_list.h:256
bool defined() const
Returns true if this term is not equal to the term assigned by the default constructor of aterms,...
Definition aterm_core.h:143
An abstraction expression.
Definition abstraction.h:26
const variable_list & variables() const
Definition abstraction.h:63
const data_expression & body() const
Definition abstraction.h:68
const binder_type & binding_operator() const
Definition abstraction.h:58
An application of a data expression to a number of arguments.
const_iterator end() const
Returns an iterator pointing past the last argument of the application.
const_iterator begin() const
Returns an iterator pointing to the first argument of the application.
const data_expression & head() const
Get the function at the head of this expression.
std::size_t size() const
\brief Assignment expression
Definition assignment.h:27
\brief Assignment of a data expression to a variable
Definition assignment.h:91
const data_expression & rhs() const
Definition assignment.h:122
const variable & lhs() const
Definition assignment.h:117
\brief A data equation
const data_expression & lhs() const
const data_expression & condition() const
const data_expression & rhs() const
bool is_default_data_expression() const
A function to efficiently determine whether a data expression is made by the default constructor.
const function_symbol_vector & constructors() const
Gets all constructors including those that are system defined.
const function_symbol_vector & mappings() const
Gets all mappings in this specification including those that are system defined.
rewrite_strategy getStrategy()
Get rewriter strategy that is used.
Definition jitty.cpp:940
class rewrite_stack m_rewrite_stack
Definition jitty.h:90
void rewrite_aux_const_function_symbol(data_expression &result, const function_symbol &op, substitution_type &sigma)
Definition jitty.cpp:817
data_expression rewrite(const data_expression &term, substitution_type &sigma)
Rewrite an mCRL2 data term.
Definition jitty.cpp:930
RewriterJitty(const data_specification &data_spec, const used_data_equation_selector &)
Definition jitty.cpp:166
void rewrite_aux(data_expression &result, const data_expression &term, substitution_type &sigma)
Rewrite a term with a given substitution and put the rewritten term in result.
Definition jitty.cpp:456
strategy create_strategy(const function_symbol &f, const data_equation_list &rules1, const data_specification &data_spec)
Definition strategy.cpp:242
void apply_cpp_code_to_higher_order_term(data_expression &result, const application &t, const std::function< void(data_expression &, const data_expression &)> rewrite_cpp_code, ITERATOR begin, ITERATOR end, substitution_type &sigma)
Definition jitty.cpp:427
const function_symbol & this_term_is_in_normal_form()
Definition jitty.h:77
void subst_values(data_expression &result, const jitty_assignments_for_a_rewrite_rule &assignments, const data_expression &t, data::enumerator_identifier_generator &generator)
Definition jitty.cpp:224
void rewrite_aux_function_symbol(data_expression &result, const function_symbol &op, const application &term, substitution_type &sigma)
Definition jitty.cpp:592
data_expression remove_normal_form_function(const data_expression &t)
Definition jitty.cpp:38
atermpp::detail::thread_aterm_pool * m_thread_aterm_pool
Definition jitty.h:96
void rebuild_strategy(const data_specification &data_spec, const mcrl2::data::used_data_equation_selector &equation_selector)
Definition jitty.cpp:144
std::vector< strategy > jitty_strat
Definition jitty.h:94
std::map< function_symbol, data_equation_list > jitty_eqns
Definition jitty.h:93
void make_jitty_strat_sufficiently_larger(const std::size_t i)
Auxiliary function to take care that the array jitty_strat is sufficiently large to access element i.
Definition jitty.cpp:136
std::vector< data_expression > rhs_for_constants_cache
Definition jitty.h:92
Rewriter interface class.
Definition rewrite.h:42
void rewrite_lambda_application(data_expression &result, const data_expression &t, substitution_type &sigma)
Rewrite t, assuming that the headsymbol of t, which can be nested, is a lambda term.
Definition rewrite.cpp:214
void rewrite_where(data_expression &result, const where_clause &term, substitution_type &sigma)
Definition rewrite.cpp:70
void existential_quantifier_enumeration(data_expression &result, const abstraction &t, substitution_type &sigma)
Definition rewrite.cpp:334
void universal_quantifier_enumeration(data_expression &result, const abstraction &t, substitution_type &sigma)
Definition rewrite.cpp:362
void rewrite_single_lambda(data_expression &result, const variable_list &vl, const data_expression &body, const bool body_in_normal_form, substitution_type &sigma)
Definition rewrite.cpp:109
enumerator_identifier_generator m_generator
Definition rewrite.h:44
const std::set< std::size_t > & dependencies() const
Definition jitty.cpp:121
dependencies_rewrite_rule_pair(std::set< std::size_t > &dependencies, const data_equation &eq)
Definition jitty.cpp:117
jitty_argument_rewriter(mutable_indexed_substitution<> &sigma, RewriterJitty &r)
Definition jitty.cpp:100
mutable_indexed_substitution & m_sigma
Definition jitty.cpp:97
void operator()(data_expression &result, const data_expression &t)
Definition jitty.cpp:104
void increase(std::size_t distance)
void set_element(std::size_t pos, std::size_t frame_size, const data_expression &d)
data_expression & element(std::size_t pos, std::size_t frame_size)
void decrease(std::size_t distance)
atermpp::vector< data_expression >::const_iterator stack_iterator(std::size_t pos, std::size_t frame_size) const
Is either a rewrite rule to be matched or an index that should be rewritten.
A strategy is a list of rules and the number of variables that occur in it.
std::size_t number_of_variables() const
Provides the maximal number of variables used in the rewrite rules making up this strategy.
const std::vector< strategy_rule > & rules() const
Yield the rules of the strategy.
\brief A function sort
const sort_expression & codomain() const
const sort_expression_list & domain() const
\brief A function symbol
const sort_expression & sort() const
Generic substitution function. The substitution is stored as a mapping of variables to expressions....
\brief A sort expression
\brief Unknown sort expression
Component for selecting a subset of equations that are actually used in an encompassing specification...
Definition selection.h:37
\brief A data variable
Definition variable.h:28
const sort_expression & sort() const
Definition variable.h:43
\brief A where expression
const data_expression & body() const
const assignment_expression_list & declarations() const
add your file description here.
static RewriterCompilingJitty::substitution_type & sigma(RewriterCompilingJitty *this_rewriter)
#define mCRL2log(LEVEL)
mCRL2log(LEVEL) provides the stream used to log.
Definition logger.h:391
add your file description here.
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
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)
static bool match_jitty(const data_expression &t, const data_expression &p, jitty_assignments_for_a_rewrite_rule &assignments, const bool term_context_guarantees_normal_form)
Definition jitty.cpp:355
std::set< variable > bound_variables_in_substitution(const jitty_assignments_for_a_rewrite_rule &assignments)
Definition jitty.cpp:212
sort_expression residual_sort(const sort_expression &s, std::size_t no_of_initial_arguments)
const data_expression & get_nested_head(const data_expression &t)
const function_symbol & true_()
Constructor for function symbol true.
Definition bool.h:77
std::vector< assignment > assignment_vector
\brief vector of assignments
Definition assignment.h:149
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_forall(const atermpp::aterm &x)
Returns true if the term t is a universal quantification.
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
bool is_exists(const atermpp::aterm &x)
Returns true if the term t is an existential quantification.
bool is_function_sort(const atermpp::aterm &x)
Returns true if the term t is a function sort.
atermpp::term_list< assignment > assignment_list
\brief list of assignments
Definition assignment.h:146
bool is_machine_number(const atermpp::aterm &x)
Returns true if the term t is a machine_number.
bool is_lambda(const atermpp::aterm &x)
Returns true if the term t is a lambda abstraction.
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
void replace_variables(T &x, const Substitution &sigma, typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
Definition replace.h:213
bool is_variable(const atermpp::aterm &x)
Returns true if the term t is a variable.
void make_application(atermpp::aterm &result)
Make function for an application.
@ warning
Definition logger.h:34
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 index(const Variable &x)
Returns the index of the variable.
jitty_variable_assignment_for_a_rewrite_rule * assignment
Definition jitty.h:40
A rule describes a partially pattern-matched rewrite rule.