13#ifdef MCRL2_ENABLE_JITTYC
15#define NAME "rewr_jittyc"
27#ifdef MCRL2_DISPLAY_REWRITE_STATISTICS
50class bracket_level_data
53 const std::size_t MCRL2_BRACKET_NESTING_LEVEL=250;
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;
61 : bracket_nesting_level(0)
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)
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);
88 for(
const variable& v: abstr.variables())
90 intermediate_result.erase(v);
92 result.insert(intermediate_result.begin(), intermediate_result.end());
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())
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);
108 result.insert(intermediate_result.begin(), intermediate_result.end());
116 const application& appl = down_cast<application>(e);
121 for(std::size_t i=0; i<arity; i++)
131 result.insert(variables_in_arg.begin(), variables_in_arg.end());
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)
143 find_variables_in_the_scope_of_main_function_symbol_in_a_complex_subexpression_helper(f, arg, result);
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)
156 std::set <variable> result;
157 find_variables_in_the_scope_of_main_function_symbol_in_a_complex_subexpression_helper(f, e, result);
164static std::vector<bool> dep_vars(
const data_equation& eqn)
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());
175 for (std::size_t i = 0; i < result.size(); ++i)
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)
195 std::size_t max_arity = 0;
199 max_arity = std::max(max_arity, arity);
215static bool arity_is_allowed(
const sort_expression& s,
const std::size_t a)
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);
230void RewriterCompilingJitty::term2seq(
const data_expression& t,
match_tree_list& s, std::size_t *var_cnt,
const bool omit_head)
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));
242 s.push_front(match_tree_F(f,dummy,dummy));
243 s.push_front(match_tree_D(dummy,0));
250 match_tree store = match_tree_S(v,dummy);
252 if (std::find(s.begin(),s.end(),store) != s.end())
254 s.push_front(match_tree_M(v,dummy,dummy));
265 const application ta(t);
266 std::size_t arity = ta.size();
270 term2seq(ta.head(),s,var_cnt,omit_head);
271 s.push_front(match_tree_N(dummy,0));
281 for (
const data_expression& u: ta)
283 term2seq(u,s,var_cnt,
false);
286 s.push_front(match_tree_N(dummy,0));
293 s.push_front(match_tree_D(dummy,0));
303match_tree_list RewriterCompilingJitty::create_sequence(
const data_equation& rule, std::size_t* var_cnt)
305 const data_expression lhs_inner = rule.lhs();
306 const data_expression cond = rule.condition();
307 const data_expression rslt = rule.rhs();
312 const application lhs_innera(lhs_inner);
313 std::size_t lhs_arity = lhs_innera.size();
317 term2seq(lhs_innera.head(),rseq,var_cnt,
true);
318 rseq.push_front(match_tree_N(dummy,0));
324 term2seq(*i,rseq,var_cnt,
false);
327 rseq.push_front(match_tree_N(dummy,0));
334 rseq.push_front(match_tree_Re(rslt,get_used_vars(rslt)));
338 rseq.push_front(match_tree_CRe(cond,rslt, get_used_vars(cond), get_used_vars(rslt)));
359 l.push_front(e.tail());
361 else if (e.front().isN())
363 h.push_front(e.tail());
365 else if (e.front().isRe())
367 r = match_tree_Re(e.front());
371 cr.push_front(e.front());
376 result.push_front(h);
386 if (e.front().isD() || e.front().isN())
390 else if (e.front().isS())
392 pars.Slist.push_front(e);
394 else if (e.front().isMe())
396 pars.Mlist.push_front(e);
398 else if (e.front().isF())
400 pars.Flist.push_front(e);
402 else if (e.front().isMachineNumber())
404 pars.Flist.push_front(e);
406 else if (e.front().isRe())
412 cr.push_front(e.front());
416 pars.stack = add_to_stack(pars.stack,l,r,cr);
419static variable createFreshVar(
const sort_expression& sort, std::size_t* i)
426 const variable& new_val,
427 const std::size_t num,
428 const mutable_map_substitution<>& substs)
436 const match_tree_M headM(head);
437 if (headM.match_variable()==old)
439 assert(headM.true_tree()==dummy);
440 assert(headM.false_tree()==dummy);
441 head = match_tree_Me(new_val,num);
444 else if (
head.isCRe())
446 const match_tree_CRe headCRe(head);
449 for (; !l.empty(); l=l.tail())
457 m.push_front(l.front());
460 l = headCRe.variables_result();
462 for (; !l.empty(); l=l.tail())
470 n.push_front(l.front());
476 else if (
head.isRe())
478 const match_tree_Re& headRe(head);
481 for (; !l.empty(); l=l.tail())
489 m.push_front(l.front());
494 result.push_back(head);
499static std::vector < std::size_t> treevars_usedcnt;
503 for (
const variable_or_number& v: l)
507 treevars_usedcnt[down_cast<aterm_int>(v).value()]++;
512match_tree RewriterCompilingJitty::build_tree(build_pars pars, std::size_t i)
514 if (!pars.Slist.empty())
520 const variable v = createFreshVar(match_tree_S(pars.Slist.front().front()).target_variable().sort(),&i);
521 treevars_usedcnt[k] = 0;
523 for (; !pars.Slist.empty(); pars.Slist=pars.Slist.tail())
527 mutable_map_substitution<>
sigma;
528 sigma[match_tree_S(e.front()).target_variable()]=v;
530 match_tree_S(e.front()).target_variable(),
535 l.push_front(e.front());
536 m.push_front(e.tail());
543 pars.stack = add_to_stack(pars.stack,m,r,readies);
547 match_tree tree = build_tree(pars,i);
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);
560 inc_usedcnt(r.variables());
561 ret = match_tree_R(r.result());
564 if ((treevars_usedcnt[k] > 0) || ((k == 0) && ret.isR()))
566 return match_tree_S(v,ret);
573 else if (!pars.Mlist.empty())
575 match_tree_Me M(pars.Mlist.front().front());
579 for (; !pars.Mlist.empty(); pars.Mlist=pars.Mlist.tail())
581 if (M==pars.Mlist.front().front())
587 m.push_front(pars.Mlist.front());
592 match_tree true_tree,false_tree;
598 false_tree = build_tree(pars,i);
602 pars.stack = newstack;
603 true_tree = build_tree(pars,i);
604 for (; !readies.empty(); readies=readies.tail())
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);
614 inc_usedcnt(r.variables());
615 true_tree = match_tree_R(r.result());
618 if (true_tree==false_tree)
624 treevars_usedcnt[M.variable_index()]++;
625 return match_tree_M(M.match_variable(),true_tree,false_tree);
628 else if (!pars.Flist.empty())
631 match_tree true_tree,false_tree;
636 for (; !pars.Flist.empty(); pars.Flist=pars.Flist.tail())
638 if (pars.Flist.front().front()==F.front())
640 newupstack.
push_front(pars.Flist.front().tail());
644 l.push_front(pars.Flist.front());
649 false_tree = build_tree(pars,i);
651 pars.upstack = newupstack;
652 true_tree = build_tree(pars,i);
654 if (true_tree==false_tree)
658 else if (F.front().isF())
660 return match_tree_F(match_tree_F(F.front()).function(),true_tree,false_tree);
664 assert(F.front().isMachineNumber());
665 return match_tree_MachineNumber(match_tree_MachineNumber(F.front()).number(),true_tree,false_tree);
668 else if (!pars.upstack.empty())
678 add_to_build_pars(pars,l,r,readies);
683 match_tree t = build_tree(pars,i);
685 for (; !readies.empty(); readies=readies.tail())
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);
697 inc_usedcnt(r.variables());
698 return match_tree_R(r.result());
703 if (pars.stack.front().empty())
705 if (pars.stack.tail().empty())
707 return match_tree_X();
711 pars.stack = pars.stack.tail();
712 return match_tree_D(build_tree(pars,i),0);
721 pars.stack = pars.stack.tail();
723 add_to_build_pars(pars,l,r,readies);
728 tree = build_tree(pars,i);
729 for (; !readies.empty(); readies=readies.tail())
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);
739 inc_usedcnt(r.variables());
740 tree = match_tree_R(r.result());
743 return match_tree_N(tree,0);
760 std::size_t total_rule_vars = 0;
761 for (
const data_equation& e: rules)
763 rule_seqs.
push_front(create_sequence(e,&total_rule_vars));
766 build_pars init_pars;
770 add_to_build_pars(init_pars,rule_seqs,r,readies);
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())
778 match_tree_CRe u(readies.front());
779 tree = match_tree_C(u.condition(), match_tree_R(u.result()), tree);
784 tree = match_tree_R(r.result());
810sort_list_vector RewriterCompilingJitty::get_residual_sorts(
const sort_expression& s1, std::size_t actual_arity, std::size_t requested_arity)
812 sort_expression s=s1;
813 sort_list_vector result;
814 while (requested_arity>0)
816 const function_sort fs(s);
819 result.push_back(fs.domain());
820 assert(fs.domain().size()<=requested_arity);
821 requested_arity=requested_arity-fs.domain().size();
825 assert(fs.domain().size()<=actual_arity);
826 actual_arity=actual_arity-fs.domain().size();
827 requested_arity=requested_arity-fs.domain().size();
838bool RewriterCompilingJitty::lift_rewrite_rule_to_right_arity(data_equation& e,
const std::size_t requested_arity)
840 data_expression lhs=e.lhs();
841 data_expression rhs=e.rhs();
847 throw mcrl2::runtime_error(
"Equation " +
pp(e) +
" does not start with a function symbol in its left hand side.");
851 if (arity_is_allowed(f.sort(),requested_arity) && actual_arity<=requested_arity)
853 if (actual_arity<requested_arity)
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)
862 variable v=variable(jitty_rewriter.identifier_generator()(),*s);
863 var_vec.push_back(v);
866 lhs=application(lhs,var_vec.begin(),var_vec.end());
867 rhs=application(rhs,var_vec.begin(),var_vec.end());
876 e=data_equation(vars,e.condition(),lhs,rhs);
882 typedef std::list<std::size_t> dep_list_t;
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)
891 rule_deps.push_front(std::make_pair(eq, dep_list_t()));
892 dep_list_t& deps = rule_deps.front().second;
894 const std::vector<bool> is_dependent_arg = dep_vars(eq);
895 for (std::size_t i = 0; i < is_dependent_arg.size(); i++)
898 if (is_dependent_arg[i])
902 arg_use_count[i] += 1;
909 while (!rule_deps.empty())
912 for (std::list<std::pair<data_equation, dep_list_t> >::iterator it = rule_deps.begin(); it != rule_deps.end(); )
914 if (it->second.empty())
916 lift_rewrite_rule_to_right_arity(it->first, arity);
917 no_deps.push_front(it->first);
918 it = rule_deps.erase(it);
927 if (!no_deps.empty())
929 strat.push_front(create_tree(no_deps));
934 std::size_t maxidx = 0;
935 for (std::size_t i = 0; i < arity; i++)
937 if (arg_use_count[i] >
max)
940 max = arg_use_count[i];
945 assert(rule_deps.empty() ||
max > 0);
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)
953 it->second.remove(maxidx);
960void RewriterCompilingJitty::extend_nfs(nfs_array& nfs,
const function_symbol& opid, std::size_t arity)
969 while (!strat.empty() && strat.front().isA())
971 nfs.at(match_tree_A(strat.front()).variable_index()) =
true;
972 strat = strat.tail();
976class rewr_function_spec
980 const std::size_t m_arity;
981 const bool m_delayed;
984 rewr_function_spec(
function_symbol fs, std::size_t arity,
const bool delayed)
985 : m_fs(fs), m_arity(arity), m_delayed(delayed)
988 bool operator<(
const rewr_function_spec& other)
const
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);
1000 std::size_t arity()
const
1005 bool delayed()
const
1010 bool operator==(
const rewr_function_spec& other)
const
1012 return m_fs == other.m_fs && m_arity == other.m_arity && m_delayed==other.m_delayed;
1015 std::string
name()
const
1017 std::stringstream
name;
1028class RewriterCompilingJitty::ImplementTree
1034 std::size_t m_indent;
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; }
1043 std::ostream&
operator<<(std::ostream& stream,
const padding& p)
1045 for (std::size_t i = p.m_indent; i != 0; --i)
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;
1057 std::vector<bool> m_used;
1058 std::vector<int> m_stack;
1060 std::size_t m_locvar_counter=0;
1074 for (data_equation_list::const_iterator it = l.begin(); it != l.end(); ++it)
1091 const std::string appl_function(std::size_t arity)
1097 return "make_application";
1101 const std::string rewr_function_name(
const function_symbol& f, std::size_t arity)
1103 rewr_function_spec spec(f, arity,
false);
1104 if (m_rewr_functions_implemented.insert(spec).second)
1106 m_rewr_functions.push(spec);
1112 const std::string delayed_rewr_function_name(
const function_symbol& f, std::size_t arity)
1114 rewr_function_spec spec(f, arity,
true);
1115 if (m_rewr_functions_implemented.insert(spec).second)
1117 m_rewr_functions.push(spec);
1119 rewr_function_name(f,arity);
1128 void calc_inner_term_variable(std::ostream& s,
1129 const std::string& target_for_output,
1131 const bool require_normal_form,
1132 std::ostream& result_type,
1133 const std::map<variable,std::string>& type_of_code_variables)
1135 const std::string variable_name = v.name();
1138 if (variable_name[0] ==
'@')
1140 assert(type_of_code_variables.count(v)>0);
1141 if (require_normal_form)
1143 if (type_of_code_variables.at(v)==
"data_expression")
1145 if (target_for_output.empty())
1147 s << variable_name.substr(1);
1151 s << m_padding << target_for_output <<
".assign(" << variable_name.substr(1)
1152 <<
", *this_rewriter->m_thread_aterm_pool);\n";
1157 if (target_for_output.empty())
1159 s <<
"local_rewrite(" << variable_name.substr(1) <<
")";
1163 s << m_padding <<
"local_rewrite(" << target_for_output <<
", " << variable_name.substr(1) <<
");\n";
1166 result_type <<
"data_expression";
1170 assert(target_for_output.empty());
1171 s << variable_name.substr(1);
1172 if (type_of_code_variables.at(v)==
"data_expression")
1174 result_type <<
"data_expression";
1178 assert(variable_name.substr(0,5)==
"@var_");
1179 result_type << type_of_code_variables.at(v);
1186 std::string bound_variable_name=m_rewriter.bound_variable_stems_from_whr_clause(v);
1187 if (!bound_variable_name.empty())
1189 if (target_for_output.empty())
1191 s << bound_variable_name;
1192 result_type <<
"data_expression";
1196 s << m_padding << target_for_output <<
".assign(" << bound_variable_name <<
", *this_rewriter->m_thread_aterm_pool);\n";
1197 result_type <<
"data_expression";
1203 if (target_for_output.empty())
1205 s <<
"static_cast<const data_expression&>(this_rewriter->bound_variable_get(" << m_rewriter.bound_variable_index(v) <<
"))";
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";
1214 result_type <<
"data_expression";
1220 void calc_inner_term_abstraction(
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)
1229 assert(!target_for_output.empty());
1230 std::string binder_constructor;
1234 binder_constructor =
"lambda_binder";
1239 binder_constructor =
"forall_binder";
1245 binder_constructor =
"exists_binder";
1249 m_rewriter.bound_variables_index_declare(a.variables());
1250 if (require_normal_form)
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";
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();
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() <<
">";
1275 m_rewriter.bound_variables_index_undeclare(a.variables());
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)
1286 for(
const assignment& a: w.assignments())
1288 std::string where_var=
"where_var" + std::to_string(m_locvar_counter++);
1289 m_rewriter.bound_variable_index_declare(a.lhs(),where_var);
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");
1297 calc_inner_term(s, target_for_output, w.body(), startarg, require_normal_form, result_type, type_of_code_variables);
1299 for(
const assignment& a: w.assignments())
1301 m_rewriter.bound_variable_index_undeclare(a.lhs());
1305 bool calc_inner_term_appl_function(std::ostream& s,
1306 const std::string& target_for_output,
1307 const application& a,
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)
1316 assert(!target_for_output.empty());
1318 nfs_array args_nfs(arity);
1319 args_nfs.fill(
false);
1320 if (require_normal_form)
1324 m_rewriter.extend_nfs(args_nfs, head, arity);
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);
1335 if (require_normal_form)
1337 result_type <<
"data_expression";
1338 s << m_padding << rewr_function_name(head, arity) <<
"(" << target_for_output <<
", ";
1342 s << m_padding << delayed_rewr_function_name(head, arity);
1343 result_type << delayed_rewr_function_name(head, arity);
1346 s <<
"<" << types_for_arguments.str() <<
"> ";
1347 result_type <<
"<" << types_for_arguments.str() <<
">";
1349 s << target_for_output <<
"(";
1351 s << code_for_arguments.str();
1352 s << (code_for_arguments.str().empty()?
"":
", ") <<
"this_rewriter);\n";
1354 return require_normal_form;
1357 bool calc_inner_term_appl_lambda_abstraction(
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)
1369 assert(a.size() > 0);
1374 assert(!target_for_output.empty());
1375 const std::size_t arity = a.size();
1377 if (require_normal_form)
1380 args_nfs.fill(
true);
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);
1389 types_for_arguments <<
", ";
1391 std::stringstream arguments;
1392 calc_inner_terms(s, arguments, a, startarg, args_nfs,types_for_arguments, type_of_code_variables);
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";
1398 result_type <<
"data_expression";
1399 return require_normal_form;
1404 nfs_array args_nfs(arity);
1405 args_nfs.fill(
true);
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);
1414 types_for_arguments <<
", ";
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;
1425 void write_application_to_stream_in_normal_form(
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)
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;
1438 std::stringstream
head;
1439 std::stringstream arguments;
1443 std::string headlocvar;
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);
1452 for(
const data_expression& t: a)
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");
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";
1473 s << m_padding << appl_function(arity) <<
"(" << target_for_output <<
"," << headlocvar << arguments.str() <<
");\n";
1475 s <<
"/* REWRITE TO NORMALFORM ???? */\n";
1478 std::string delayed_application(
const std::size_t arity)
1480 m_delayed_application_functions.insert(arity);
1481 std::stringstream s;
1482 s <<
"delayed_application" << arity;
1486 void write_delayed_application_to_stream_in_normal_form(
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)
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;
1504 calc_inner_term(code_string,
"", down_cast<variable>(a.head()), startarg,
true, result_types, type_of_code_variables);
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);
1515 for(
const data_expression& t: a)
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);
1524 std::string result_type_str = delayed_application(arity) +
"<" + result_types.str() +
">";
1525 result_type << result_type_str;
1527 s << m_padding << result_type_str <<
" " << target_for_output <<
"(";
1528 s << code_string.str();
1529 s <<
", this_rewriter);\n";
1533 bool calc_inner_term_appl_variable
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)
1543 assert(!target_for_output.empty());
1544 if (require_normal_form)
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";
1554 write_delayed_application_to_stream_in_normal_form(s,target_for_output,a,startarg, result_type, type_of_code_variables);
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)
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);
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);
1579 return calc_inner_term_appl_variable(s, target_for_output, a, startarg, require_normal_form, result_type, type_of_code_variables);
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)
1603 if (target_for_output.empty())
1605 RewriterCompilingJitty::substitution_type
sigma;
1606 s << m_rewriter.m_nf_cache->insert(m_rewriter.jitty_rewriter(t,
sigma));
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))
1616 result_type <<
"data_expression";
1624 calc_inner_term_variable(s, target_for_output, down_cast<variable>(t), require_normal_form, result_type, type_of_code_variables);
1629 calc_inner_term_abstraction(s, target_for_output, down_cast<abstraction>(t), startarg, require_normal_form, result_type, type_of_code_variables);
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);
1639 calc_inner_term_application(s, target_for_output, down_cast<application>(t), startarg, require_normal_form, result_type, type_of_code_variables);
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)
1660 argument_types <<
", ";
1662 std::stringstream argument_string;
1663 std::stringstream argument_type;
1664 assert(i<rewr.size());
1669 argument_type, type_of_code_variables);
1671 arguments << argument_string.str();
1672 argument_types << argument_type.str();
1678 std::string locvar =
"inner_arg"+std::to_string(m_locvar_counter++);
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();
1685 arguments << locvar;
1686 argument_types << argument_type.str();
1690 std::string locvar =
"inner_arg"+std::to_string(m_locvar_counter++);
1692 argument_type, type_of_code_variables);
1693 s << argument_string.str();
1695 arguments << locvar;
1696 argument_types << argument_type.str();
1711 void implement_tree(std::ostream& m_stream,
1712 const match_tree& tree,
1713 std::size_t cur_arg,
1717 const std::size_t arity,
1719 bracket_level_data& brackets,
1720 std::stack<std::string>& auxiliary_code_fragments,
1721 std::map<variable,std::string>& type_of_code_variables)
1727 if (brackets.bracket_nesting_level>brackets.MCRL2_BRACKET_NESTING_LEVEL)
1729 static std::size_t auxiliary_method_name_index=0;
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";
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"
1744 <<
" std::size_t old_stack_size=this_rewriter->m_rewrite_stack.stack_size();\n";
1746 auxiliary_method_name_index++;
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"
1755 m_padding.restore(old_indent);
1756 auxiliary_code_fragments.push(s.str());
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);
1764 else if (tree.isM())
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);
1768 else if (tree.isF())
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);
1772 else if (tree.isMachineNumber())
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);
1776 else if (tree.isD())
1778 implement_treeD(m_stream, atermpp::down_cast<match_tree_D>(tree), level, cnt, arity, opid, brackets, auxiliary_code_fragments, type_of_code_variables);
1780 else if (tree.isN())
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);
1784 else if (tree.isC())
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);
1788 else if (tree.isR())
1790 implement_treeR(m_stream, atermpp::down_cast<match_tree_R>(tree), cur_arg, level, type_of_code_variables);
1795 assert(tree.isA() || tree.isX() || tree.isMe());
1802 const aterm m_matchterm;
1805 matches(
const aterm& matchterm)
1806 : m_matchterm(matchterm)
1811 return t==m_matchterm;
1815 void implement_treeS(
1816 std::ostream& m_stream,
1817 const match_tree_S& tree,
1818 std::size_t cur_arg,
1822 const std::size_t arity,
1824 bracket_level_data& brackets,
1825 std::stack<std::string>& auxiliary_code_fragments,
1826 std::map<variable,std::string>& type_of_code_variables)
1828 const match_tree_S& treeS(tree);
1829 bool reset_current_data_parameters=
false;
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;
1840 if (m_used[cur_arg])
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";
1845 type_of_code_variables[treeS.target_variable()]=
"data_expression";
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);
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 <<
"]"
1860 type_of_code_variables[treeS.target_variable()]=
"data_expression";
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)
1866 brackets.current_data_parameters.pop();
1867 brackets.current_data_arguments.pop();
1871 void implement_treeM(
1872 std::ostream& m_stream,
1873 const match_tree_M& tree,
1874 std::size_t cur_arg,
1878 const std::size_t arity,
1880 bracket_level_data& brackets,
1881 std::stack<std::string>& auxiliary_code_fragments,
1882 std::map<variable,std::string>& type_of_code_variables)
1884 m_stream << m_padding <<
"if (" << std::string(tree.match_variable().name()).c_str() + 1 <<
" == ";
1887 m_stream <<
"arg" << cur_arg;
1891 m_stream << (level == 1 ?
"arg" :
"t") << parent <<
"[" << cur_arg <<
"]";
1893 m_stream <<
") // M\n" << m_padding
1895 brackets.bracket_nesting_level++;
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
1904 brackets.bracket_nesting_level++;
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
1913 void implement_treeF(
1914 std::ostream& m_stream,
1915 const match_tree_F& tree,
1916 std::size_t cur_arg,
1920 const std::size_t arity,
1922 bracket_level_data& brackets,
1923 std::stack<std::string>& auxiliary_code_fragments,
1924 std::map<variable,std::string>& type_of_code_variables)
1926 bool reset_current_data_parameters=
false;
1928 m_stream << m_padding;
1929 brackets.bracket_nesting_level++;
1934 m_stream <<
"if (uint_address(arg" << cur_arg <<
") == " <<
func <<
") // F1\n" << m_padding
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
1946 const char* arg_or_t = level == 1 ?
"arg" :
"t";
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";
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";
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));
1967 reset_current_data_parameters=
true;
1969 m_stack.push_back(cur_arg);
1970 m_stack.push_back(parent);
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)
1975 brackets.current_data_parameters.pop();
1976 brackets.current_data_arguments.pop();
1978 m_padding.unindent();
1981 m_stream << m_padding
1982 <<
"}\n" << m_padding
1983 <<
"else\n" << m_padding
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
1990 brackets.bracket_nesting_level--;
1994 void implement_treeMachineNumber(
1995 std::ostream& m_stream,
1996 const match_tree_MachineNumber& tree,
1997 std::size_t cur_arg,
2001 const std::size_t arity,
2003 bracket_level_data& brackets,
2004 std::stack<std::string>& auxiliary_code_fragments,
2005 std::map<variable,std::string>& type_of_code_variables)
2007 bool reset_current_data_parameters=
false;
2009 m_stream << m_padding;
2010 brackets.bracket_nesting_level++;
2015 m_stream <<
"if (uint_address(arg" << cur_arg <<
") == " <<
number <<
") // MachineNumber (I)\n" << m_padding
2028 const char* arg_or_t = level == 1 ?
"arg" :
"t";
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";
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));
2051 reset_current_data_parameters=
true;
2053 m_stack.push_back(cur_arg);
2054 m_stack.push_back(parent);
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)
2059 brackets.current_data_parameters.pop();
2060 brackets.current_data_arguments.pop();
2062 m_padding.unindent();
2065 m_stream << m_padding
2066 <<
"}\n" << m_padding
2067 <<
"else\n" << m_padding
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
2074 brackets.bracket_nesting_level--;
2078 void implement_treeD(
2079 std::ostream& m_stream,
2080 const match_tree_D& tree,
2083 const std::size_t arity,
2085 bracket_level_data& brackets,
2086 std::stack<std::string>& auxiliary_code_fragments,
2087 std::map<variable,std::string>& type_of_code_variables)
2089 int i = m_stack.back();
2091 int j = m_stack.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);
2098 void implement_treeN(
2099 std::ostream& m_stream,
2100 const match_tree_N& tree,
2101 std::size_t cur_arg,
2105 const std::size_t arity,
2107 bracket_level_data& brackets,
2108 std::stack<std::string>& auxiliary_code_fragments,
2109 std::map<variable,std::string>& type_of_code_variables)
2111 implement_tree(m_stream, tree.subtree(), cur_arg + 1, parent, level, cnt, arity, opid, brackets, auxiliary_code_fragments, type_of_code_variables);
2114 void implement_treeC(
2115 std::ostream& m_stream,
2116 const match_tree_C& tree,
2117 std::size_t cur_arg,
2121 const std::size_t arity,
2123 bracket_level_data& brackets,
2124 std::stack<std::string>& auxiliary_code_fragments,
2125 std::map<variable,std::string>& type_of_code_variables)
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
2133 brackets.bracket_nesting_level++;
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();
2138 m_stream << m_padding
2139 <<
"}\n" << m_padding
2140 <<
"else\n" << m_padding
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();
2147 m_stream << m_padding
2149 brackets.bracket_nesting_level--;
2152 void implement_treeR(
2153 std::ostream& m_stream,
2154 const match_tree_R& tree,
2155 std::size_t cur_arg,
2157 const std::map<variable,std::string>& type_of_code_variables)
2161 cur_arg = m_stack[2 * level - 1];
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";
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)
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
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);
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;
2193 return tree.false_tree();
2196 void implement_treeR(
2197 std::ostream& m_stream,
2198 const match_tree_R& tree,
2200 const std::map<variable,std::string>& type_of_code_variables)
2202 std::stringstream result_type_string;
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";
2213 calc_inner_term(m_stream,
"result", tree.result(), 0,
true, result_type_string, type_of_code_variables);
2215 << m_padding <<
"this_rewriter->m_rewrite_stack.reset_stack_size(old_stack_size);\n"
2216 << m_padding <<
"return; // R2b\n";
2221 ImplementTree(RewriterCompilingJitty& rewr, function_symbol_vector&
function_symbols)
2222 : m_rewriter(rewr), m_padding(2)
2226 const std::size_t max_arity =
getArity(*it);
2227 for (std::size_t arity = 0; arity <= max_arity; ++arity)
2229 if (arity_is_allowed(it->sort(), arity))
2232 static_cast<void>(rewr_function_name(*it, arity));
2238 const std::set<rewr_function_spec>& implemented_rewrs()
2240 return m_rewr_functions_implemented;
2248 void implement_tree(
2249 std::ostream& m_stream,
2251 const std::size_t arity,
2253 bracket_level_data& brackets,
2254 std::stack<std::string>& auxiliary_code_fragments,
2255 std::map<variable,std::string>& type_of_code_variables)
2268 tree = implement_treeC(m_stream, down_cast<match_tree_C>(tree),brackets, type_of_code_variables);
2274 implement_treeR(m_stream, down_cast<match_tree_R>(tree), arity, type_of_code_variables);
2278 implement_tree(m_stream, tree, 0, 0, 0, 0, arity, opid, brackets, auxiliary_code_fragments, type_of_code_variables);
2284 m_padding.unindent();
2285 m_stream << m_padding <<
"}\n";
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)
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;
2302 for (std::size_t i = 0; i < domain_size; ++i)
2304 ss <<
", [&](data_expression& r){ local_rewrite(r, arg_not_nf" << used_arguments + i <<
"); }";
2308 used_arguments += domain_size;
2309 if (used_arguments<arity)
2311 return ss.str() + implement_body_of_cplusplus_defined_function(arity,
2314 down_cast<function_sort>(s.codomain()),
2323 void implement_a_cplusplus_defined_function(
2324 std::ostream& m_stream,
2325 const std::string& target_for_output,
2328 const data_specification& data_spec)
2330 m_stream << m_padding <<
"// Implement function " << opid <<
" by calling a user defined rewrite function.\n";
2337 const std::string cplusplus_function_name = data_spec.cpp_implemented_functions().find(opid)->second.second;
2343 if (target_for_output.empty())
2353 std::stringstream ss1;
2354 m_stream << m_padding << cplusplus_function_name <<
"(" << target_for_output;
2358 ss1 <<
", local_rewrite(arg_not_nf" << i <<
")";
2362 m_stream << m_padding << ss1.str() <<
";\n";
2366 m_stream << m_padding <<
"data_expression& local_store1=this_rewriter->m_rewrite_stack.new_stack_position<data_expression>();\n";
2367 std::stringstream ss;
2369 m_stream << m_padding << cplusplus_function_name <<
"(local_store1";
2373 m_stream <<
", local_rewrite(arg_not_nf" << i <<
")";
2377 m_stream << m_padding <<
"data_expression& local_store=this_rewriter->m_rewrite_stack.new_stack_position<data_expression>();\n";
2380 std::string result=
"local_store";
2381 m_stream << implement_body_of_cplusplus_defined_function(
2385 down_cast<function_sort>(down_cast<function_sort>(opid.sort()).codomain()),
2387 assert(used_arguments == arity);
2391 if (target_for_output.empty())
2393 m_stream << m_padding <<
"data_expression result1; // TODO: optimize\n"
2394 << m_padding <<
"rewrite_aux<true>(result1, " << result <<
",this_rewriter);\n";
2398 m_stream << m_padding <<
"rewrite_aux<true>(" << target_for_output <<
", " << result <<
",this_rewriter);\n";
2402 void implement_strategy(
2403 std::ostream& m_stream,
2404 match_tree_list strat,
2407 bracket_level_data& brackets,
2408 std::stack<std::string>& auxiliary_code_fragments,
2409 const data_specification& data_spec)
2412 if (data_spec.cpp_implemented_functions().find(opid)!=data_spec.cpp_implemented_functions().end() &&
2415 implement_a_cplusplus_defined_function(m_stream,
"result", arity, opid, data_spec);
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);
2422 std::map<variable,std::string> type_of_code_variables;
2423 while (!strat.empty())
2425 m_stream << m_padding <<
"// " << strat.front() <<
"\n";
2426 if (strat.front().isA())
2428 std::size_t
arg = match_tree_A(strat.front()).variable_index();
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";
2442 if (!added_new_parameters_in_brackets)
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());
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);
2453 m_stream << m_padding <<
"// Considering argument " <<
arg <<
"\n";
2457 m_stream << m_padding <<
"{\n";
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";
2463 strat = strat.tail();
2465 rewr_function_finish(m_stream, arity, opid);
2466 if (added_new_parameters_in_brackets)
2468 brackets.current_data_parameters.pop();
2469 brackets.current_data_arguments.pop();
2471 m_stream << m_padding <<
"this_rewriter->m_rewrite_stack.reset_stack_size(old_stack_size);\n";
2474 std::string get_heads(
const sort_expression& s,
const std::string& base_string,
const std::size_t number_of_arguments)
2476 std::stringstream ss;
2479 const function_sort fs(s);
2480 ss <<
"down_cast<application>(" << get_heads(fs.codomain(),base_string,number_of_arguments-fs.domain().size()) <<
".head())";
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)
2499 while (index >= s.domain().size())
2502 index -= s.domain().size();
2503 number_of_arguments -= s.domain().size();
2504 s = down_cast<function_sort>(s.codomain());
2506 m_stream << get_heads(s.codomain(), base_string, number_of_arguments - s.domain().size()) <<
"[" << index <<
"]";
2509 void generate_delayed_application_functions(std::ostream& ss)
2511 for(std::size_t arity: m_delayed_application_functions)
2514 ss << m_padding <<
"template < class HEAD";
2515 for (std::size_t i = 0; i < arity; ++i)
2517 ss <<
", class DATA_EXPR" << i;
2521 ss << m_padding <<
"class delayed_application" << arity <<
"\n"
2522 << m_padding <<
"{\n";
2524 ss << m_padding <<
"protected:\n";
2527 ss << m_padding <<
"const HEAD& m_head;\n";
2528 for (std::size_t i = 0; i < arity; ++i)
2530 ss << m_padding <<
"const DATA_EXPR" << i <<
"& m_arg" << i <<
";\n";
2532 ss << m_padding <<
"RewriterCompilingJitty* this_rewriter;\n\n";
2533 m_padding.unindent();
2534 ss << m_padding <<
"public:\n";
2537 ss << m_padding <<
"delayed_application" << arity <<
"(const HEAD& head";
2538 for (std::size_t i = 0; i < arity; ++i)
2540 ss <<
", const DATA_EXPR" << i <<
"& arg" << i;
2542 ss <<
", RewriterCompilingJitty* tr)\n";
2543 ss << m_padding <<
" : m_head(head)";
2545 for (std::size_t i = 0; i < arity; ++i)
2547 ss <<
", m_arg" << i <<
"(arg" << i <<
")";
2549 ss <<
", this_rewriter(tr)\n" << m_padding <<
"{}\n\n";
2551 ss << m_padding <<
"data_expression& normal_form() const\n";
2552 ss << m_padding <<
"{\n";
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); }";
2561 for (std::size_t i = 0; i < arity; ++i)
2563 ss <<
", [&](data_expression& r){ local_rewrite(r, m_arg" << i <<
"); }";
2566 ss << m_padding <<
"rewrite_with_arguments_in_normal_form(local_store, local_store, this_rewriter);\n"
2567 << m_padding <<
"return local_store;\n";
2569 m_padding.unindent();
2570 ss << m_padding <<
"}\n\n";
2572 ss << m_padding <<
"void normal_form(data_expression& result) const\n";
2573 ss << m_padding <<
"{\n";
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)
2579 ss <<
", [&](data_expression& result){ local_rewrite(result, m_arg" << i <<
"); }";
2582 ss << m_padding <<
"rewrite_with_arguments_in_normal_form(result, result, this_rewriter);\n";
2584 m_padding.unindent();
2585 ss << m_padding <<
"}\n\n";
2586 m_padding.unindent();
2587 m_padding.unindent();
2588 ss << m_padding <<
"};\n\n";
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)
2600 m_stream << m_padding <<
"result = " <<
head <<
";\n";
2604 sort_expression current_sort=s;
2605 std::size_t used_arguments=0;
2606 while (used_arguments<arity)
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();
2613 m_stream << m_padding << appl_function(domain_size) <<
"(result, ";
2614 if (used_arguments>0)
2616 m_stream <<
"result";
2623 for (std::size_t i = 0; i < domain_size; ++i)
2625 if (m_used[used_arguments + i])
2627 m_stream <<
", arg" << used_arguments + i;
2631 m_stream <<
", [&](data_expression& result){ local_rewrite(result, arg_not_nf" << used_arguments + i <<
"); }";
2635 used_arguments += domain_size;
2637 assert(used_arguments==arity);
2641 void rewr_function_finish(std::ostream& m_stream, std::size_t arity,
const data::function_symbol& opid)
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";
2652 std::stringstream ss;
2653 ss <<
"this_rewriter->normal_forms_for_constants["
2656 rewr_function_finish_term(m_stream, arity, ss.str(), down_cast<function_sort>(opid.
sort()));
2660 void rewr_function_signature(std::ostream& m_stream, std::size_t index, std::size_t arity, bracket_level_data& brackets)
2665 m_stream << m_padding <<
"template < ";
2666 std::stringstream s;
2667 for (std::size_t i = 0; i < arity; ++i)
2670 s << (i == 0 ?
"" :
", ")
2671 <<
"class DATA_EXPR" << i;
2673 m_stream << s.str() <<
">\n";
2674 brackets.current_template_parameters = s.str();
2676 m_stream << m_padding <<
"static inline void"
2677 <<
" rewr_" << index <<
"_" << arity <<
"(data_expression& result";
2679 std::stringstream arguments;
2680 std::stringstream parameters;
2681 for (std::size_t i = 0; i < arity; ++i)
2683 parameters <<
", const DATA_EXPR" << i <<
"& arg_not_nf"
2685 arguments << (i == 0 ?
"" :
", ") <<
"arg_not_nf" << i;
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());
2692 void rewr_function_implementation(
2693 std::ostream& m_stream,
2696 match_tree_list strategy,
2697 const data_specification& data_spec)
2700 bracket_level_data brackets;
2701 std::stack<std::string> auxiliary_code_fragments;
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";
2710 implement_strategy(m_stream, strategy, arity,
func, brackets, auxiliary_code_fragments,data_spec);
2712 m_stream << m_padding <<
"return;\n";
2713 m_padding.unindent();
2714 m_stream << m_padding <<
"}\n\n";
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)
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)";
2729 m_stream <<
", this_rewriter); }\n\n";
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)
2739 get_recursive_argument(m_stream, down_cast<function_sort>(
func.sort()), i,
"t", arity);
2741 m_stream <<
", this_rewriter); }\n\n";
2744 while (!auxiliary_code_fragments.empty())
2746 m_stream << auxiliary_code_fragments.top();
2747 auxiliary_code_fragments.pop();
2752 void generate_delayed_normal_form_generating_function(std::ostream& m_stream,
const data::function_symbol&
func, std::size_t arity)
2755 m_stream << m_padding <<
"// [" << index <<
"] " <<
func <<
": " <<
func.sort() <<
"\n";
2758 m_stream << m_padding <<
"template < ";
2759 for (std::size_t i = 0; i < arity; ++i)
2761 m_stream << (i == 0 ?
"" :
", ")
2762 <<
"class DATA_EXPR" << i;
2766 m_stream << m_padding <<
"class delayed_rewr_" << index <<
"_" << arity <<
"\n";
2767 m_stream << m_padding <<
"{\n";
2769 m_stream << m_padding <<
"protected:\n";
2771 for(std::size_t i = 0; i < arity; ++i)
2773 m_stream << m_padding <<
"const DATA_EXPR" << i <<
"& m_t" << i <<
";\n";
2775 m_stream << m_padding <<
"RewriterCompilingJitty* this_rewriter;\n";
2776 m_padding.unindent();
2777 m_stream << m_padding <<
"public:\n";
2779 m_stream << m_padding <<
"delayed_rewr_" << index <<
"_" << arity <<
"(";
2780 for(std::size_t i = 0; i < arity; ++i)
2782 m_stream << (i==0?
"":
", ") <<
"const DATA_EXPR" << i <<
"& t" << i;
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)
2788 m_stream << (i==0?
"":
", ") <<
"m_t" << i <<
"(t" << i <<
")";
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"
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)
2801 m_stream <<
", m_t" << i;
2804 m_stream << (arity==0?
"":
", ") <<
"this_rewriter);\n"
2805 << m_padding <<
" return local_store;\n"
2806 << m_padding <<
"}\n";
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)
2813 m_stream <<
", m_t" << i;
2816 m_stream << (arity==0?
"":
", ") <<
"this_rewriter);\n"
2817 << m_padding <<
"}\n";
2819 m_padding.unindent();
2820 m_padding.unindent();
2821 m_stream << m_padding <<
"};\n";
2822 m_stream << m_padding <<
"\n";
2825 void generate_rewr_functions(std::ostream& m_stream,
const data_specification& data_spec)
2827 while (!m_rewr_functions.empty())
2829 rewr_function_spec spec = m_rewr_functions.top();
2830 m_rewr_functions.pop();
2833 generate_delayed_normal_form_generating_function(m_stream, spec.fs(), spec.arity());
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);
2844void RewriterCompilingJitty::CleanupRewriteSystem()
2847 if (so_rewr_cleanup !=
nullptr)
2860static std::string generate_cpp_filename(std::size_t unique)
2862 const char* env_dir = std::getenv(
"MCRL2_COMPILEDIR");
2863 std::ostringstream filename;
2864 std::string filedir;
2868 if (*filedir.rbegin() !=
'/')
2870 filedir.append(
"/");
2877 time_t now = time(
nullptr);
2878 struct tm tstruct = *localtime(&now);
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;
2887 filename << filedir <<
"jittyc_" << getpid() <<
"_" << (unique % 100000000) <<
"_" << unique_time <<
".cpp";
2888 return filename.str();
2898template <
class Filter>
2901 for (function_symbol_vector::const_iterator it = source.begin(); it != source.end(); ++it)
2905 dest.push_back(*it);
2910void RewriterCompilingJitty::generate_code(
const std::string& filename)
2912 std::ofstream cpp_file(filename);
2913 std::stringstream rewr_code;
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()));
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);
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);
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";
2939 cpp_file <<
"namespace {\n"
2940 "// Anonymous namespace so the compiler uses internal linkage for the generated\n"
2941 "// rewrite code.\n"
2943 "struct rewr_functions\n"
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"
2951 " return t.normal_form();\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"
2960 " t.normal_form(result);\n"
2963 " static const data_expression& local_rewrite(const data_expression& t)\n"
2968 " static void local_rewrite(data_expression& result, const data_expression& t)\n"
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);
2980 code_generator.generate_delayed_application_functions(cpp_file);
2982 cpp_file << rewr_code.str();
2984 cpp_file <<
"void set_the_precompiled_rewrite_functions_in_a_lookup_table(RewriterCompilingJitty* this_rewriter)\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"
2990 <<
" f = nullptr;\n"
2992 cpp_file <<
" for(rewriter_function& f: this_rewriter->functions_when_arguments_are_in_normal_form)\n"
2994 <<
" f = nullptr;\n"
2998 RewriterCompilingJitty::substitution_type
sigma;
2999 normal_forms_for_constants.clear();
3000 for (
const rewr_function_spec& f: code_generator.implemented_rewrs())
3007 cpp_file <<
" this_rewriter->functions_when_arguments_are_not_in_normal_form[this_rewriter->arity_bound * "
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 * "
3013 <<
" + " << f.
arity() <<
"] = rewr_functions::"
3014 << f.
name() <<
"_term_arg_in_normal_form;\n";
3018 if (index>=normal_forms_for_constants.size())
3020 normal_forms_for_constants.resize(index+1);
3022 normal_forms_for_constants[index]=jitty_rewriter(f.fs(),
sigma);
3032void RewriterCompilingJitty::BuildRewriteSystem()
3034 CleanupRewriteSystem();
3045 std::string compile_script;
3046 const char* env_compile_script = std::getenv(
"MCRL2_COMPILEREWRITER");
3047 if (env_compile_script !=
nullptr)
3049 compile_script = env_compile_script;
3057 compile_script =
"mcrl2compilerewriter";
3060 rewriter_so = std::shared_ptr<uncompiled_library>(
new uncompiled_library(compile_script));
3062 mCRL2log(verbose) <<
"using '" << compile_script <<
"' to compile rewriter." << std::endl;
3065 jittyc_eqns.clear();
3066 for(std::set < data_equation >::const_iterator it = rewrite_rules.begin(); it != rewrite_rules.end(); ++it)
3068 jittyc_eqns[down_cast<function_symbol>(
get_nested_head(it->lhs()))].push_front(*it);
3071 std::string cpp_file = generate_cpp_filename(
reinterpret_cast<std::size_t
>(
this));
3072 generate_code(cpp_file);
3074 mCRL2log(verbose) <<
"generated " << cpp_file <<
" in " << time.
time() <<
"ms, compiling..." << std::endl;
3079 rewriter_so->compile(cpp_file);
3081 catch(std::runtime_error& e)
3083 rewriter_so->leave_files();
3087 mCRL2log(verbose) <<
"compiled in " << time.
time() <<
"ms, loading rewriter..." << std::endl;
3089 bool (*
init)(rewriter_interface*, RewriterCompilingJitty* this_rewriter);
3093 typedef bool rewrite_function_type(rewriter_interface*, RewriterCompilingJitty*);
3094 init =
reinterpret_cast<rewrite_function_type*
>(rewriter_so->proc_address(
"init"));
3096 catch(std::runtime_error& e)
3098 rewriter_so->leave_files();
3099#ifndef MCRL2_DISABLE_JITTYC_VERSION_CHECK
3105 if (logger::get_reporting_level()<debug)
3109 rewriter_so->cleanup();
3111 catch (std::runtime_error&
error)
3118 if (!
init(&interface,
this))
3120#ifndef MCRL2_DISABLE_JITTYC_VERSION_CHECK
3124 so_rewr_cleanup = interface.rewrite_cleanup;
3125 so_rewr = interface.rewrite_external;
3127 mCRL2log(verbose) << interface.status << std::endl;
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())
3137 thread_initialise();
3138 assert(m_nf_cache->empty());
3139 so_rewr_cleanup =
nullptr;
3141 rewriting_in_progress =
false;
3144 rewrite_rules.clear();
3146 for (
const data_equation& e: data_spec.equations())
3148 if (data_equation_selector(e))
3150 const data_equation rule=e;
3154 if (rewrite_rules.insert(rule).second)
3160 catch (std::runtime_error&
error)
3167 BuildRewriteSystem();
3170RewriterCompilingJitty::~RewriterCompilingJitty()
3172 CleanupRewriteSystem();
3175void RewriterCompilingJitty::rewrite(
3176 data_expression& result,
3177 const data_expression& term,
3178 substitution_type&
sigma)
3180#ifdef MCRL2_DISPLAY_REWRITE_STATISTICS
3181 data::detail::increment_rewrite_count();
3185 substitution_type *saved_sigma=global_sigma;
3186 global_sigma=&
sigma;
3187 if (rewriting_in_progress)
3189 so_rewr(result,term,
this);
3193 rewriting_in_progress=
true;
3196 so_rewr(result,term,
this);
3198 catch (recalculate_term_as_stack_is_too_small&)
3201 rewriting_in_progress=
false;
3204 m_rewrite_stack.reserve_more_space();
3208 rewriting_in_progress=
false;
3209 assert(m_rewrite_stack.stack_size()==0);
3212 global_sigma=saved_sigma;
3216data_expression RewriterCompilingJitty::rewrite(
3217 const data_expression& term,
3218 substitution_type&
sigma)
3220 data_expression result;
3227 return jitty_compiling;
bool operator==(const ParityGameVertex &a, const ParityGameVertex &b)
functions to get the executable's basename.
An integer term stores a single std::size_t value. It carries no arguments.
const function_symbol & function() const
Returns the function symbol belonging to an aterm.
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.
const Term & front() const
Returns the first element of the list.
term_list_iterator< Term > const_iterator
Const iterator used to iterate through an term_list.
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.
const sort_expression & sort() const
Standard exception class for reporting runtime errors.
Implements a simple stopwatch that starts on construction.
void reset()
Reset the stopwatch to count from this moment onwards.
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)
#define mCRL2log(LEVEL)
mCRL2log(LEVEL) provides the stream used to log.
_aterm * address(const unprotected_aterm_core &t)
The main namespace for the aterm++ library.
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.
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...
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
atermpp::term_list< match_tree_list > match_tree_list_list
atermpp::term_list< variable_or_number > variable_or_number_list
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
atermpp::term_list< match_tree_list_list > match_tree_list_list_list
std::size_t getArity(const data::function_symbol &op)
std::size_t get_direct_arity(const data::function_symbol &op)
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.
const function_symbol & true_()
Constructor for function symbol true.
function_symbol empty(const sort_expression &s)
Constructor for function symbol {:}.
function_symbol head(const sort_expression &s)
Constructor for function symbol head.
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
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)
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.
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...
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.