10#define NAME std::string("rewr_jitty")
15#include <boost/config.hpp>
20#ifdef MCRL2_DISPLAY_REWRITE_STATISTICS
58 const application& ta=atermpp::down_cast<application>(t);
71 const where_clause& t1=atermpp::down_cast<where_clause>(t);
78 const assignment& assignment_expr = atermpp::down_cast<assignment>(ae);
86 const abstraction& t1=atermpp::down_cast<abstraction>(t);
151 if (equation_selector(f))
155 std::map< function_symbol, data_equation_list >::const_iterator j=
jitty_eqns.find(f);
169 Rewriter(data_spec,equation_selector),
170 this_term_is_in_normal_form_symbol(
171 std::string(
"Rewritten@@term"),
173 rewriting_in_progress(
false)
178 if (equation_selector(eq))
184 catch (std::runtime_error& e)
190 const function_symbol& lhs_head_index=atermpp::down_cast<function_symbol>(
get_nested_head(eq.lhs()));
193 std::map< function_symbol, data_equation_list >::iterator it = jitty_eqns.find(lhs_head_index);
194 if (it != jitty_eqns.end())
199 jitty_eqns[lhs_head_index] = n;
203 rebuild_strategy(data_spec, equation_selector);
214 std::set<variable> variables_in_substitution;
215 for(std::size_t i=0; i<assignments.
size; ++i)
218 variables_in_substitution.insert(s.begin(),s.end());
219 variables_in_substitution.insert(assignments.
assignment[i].
var);
221 return variables_in_substitution;
243 for (std::size_t i=0; i<assignments.
size; i++)
265 const abstraction& t1=atermpp::down_cast<abstraction>(t);
279 bool sigma_trivial=
true;
280 for(
const variable& v: bound_variables)
282 if (variables_in_substitution.count(v)>0)
285 const variable fresh_variable(generator(),v.sort());
286 new_variables.push_back(fresh_variable);
287 sigma[v]=fresh_variable;
292 new_variables.push_back(v);
306 const where_clause& t1=atermpp::down_cast<where_clause>(t);
315 bool sigma_trivial=
true;
319 const assignment& assignment_expr = atermpp::down_cast<assignment>(a);
322 if (variables_in_substitution.count(v)>0)
326 new_assignments.push_back(
assignment(fresh_variable,result));
327 sigma[v]=fresh_variable;
332 new_assignments.push_back(
assignment(v,result));
344 const application& t1 = atermpp::down_cast<application>(t);
350 { subst_values(result,assignments,t,generator); return;});
359 const bool term_context_guarantees_normal_form)
372 for (std::size_t i=0; i<assignments.
size; i++)
382 atermpp::down_cast<variable>(p),
384 term_context_guarantees_normal_form);
395 assert(term_context_guarantees_normal_form);
397 const application& pa=atermpp::down_cast<application>(p);
398 const application& ta=atermpp::down_cast<application>(t);
406 pa.
head(),assignments,
true))
411 for (std::size_t i=0; i<pa.
size(); i++)
426template <
class ITERATOR>
439 rewrite_cpp_code(result, intermediate);
480 const where_clause& w = atermpp::down_cast<where_clause>(term);
487 const abstraction& ta=atermpp::down_cast<abstraction>(term);
506 const application& terma=atermpp::down_cast<application>(term);
509 assert(terma.
size()==1);
532 const application& tapp=atermpp::down_cast<application>(term);
537 const std::size_t t = 0;
544 const std::size_t head1 = 1;
553 atermpp::down_cast<application>(result),
563 const bool do_not_rewrite_head=
false;
579 assert(term.
size()==1);
585 assert(term.
size()==1);
604 bool* rewritten_defined = MCRL2_SPECIFIC_STACK_ALLOCATOR(
bool, arity);
606 for(std::size_t i=0; i<arity; ++i)
608 rewritten_defined[i]=
false;
615 if (!strat.
rules().empty())
622 if (
rule.is_rewrite_index())
624 const std::size_t i =
rule.rewrite_index();
627 assert(!rewritten_defined[i]||i==0);
628 if (!rewritten_defined[i])
633 rewritten_defined[i]=
true;
643 else if (
rule.is_cpp_code())
654 rule.rewrite_cpp_code()(result, rewriteable_term);
664 if (!rewritten_defined[i])
668 rewritten_defined[i]=
true;
675 rule.rewrite_cpp_code(),
688 if (rule_arity > arity)
693 assert(assignments.
size==0);
696 for (std::size_t i=0; i<rule_arity; i++)
703 assignments,rewritten_defined[i]))
711 bool condition_of_this_rule=
false;
714 condition_of_this_rule=
true;
722 condition_of_this_rule=
true;
725 if (condition_of_this_rule)
729 if (arity == rule_arity)
739 assert(arity>rule_arity);
743 for(std::size_t i=rule_arity; i<arity; ++i)
746 rewritten_defined[i]=
true;
750 std::size_t i = rule_arity;
754 const function_sort& fsort = atermpp::down_cast<function_sort>(sort);
755 const std::size_t end=i+fsort.
domain().
size();
784 for (std::size_t i=0; i<arity; i++)
786 if (!rewritten_defined[i])
803 const function_sort& fsort=atermpp::down_cast<function_sort>(*sort);
804 const std::size_t end=i+fsort.
domain().
size();
849 if (
rule.is_rewrite_index())
855 else if (
rule.is_cpp_code())
857 rule.rewrite_cpp_code()(result, op);
898#ifdef MCRL2_DISPLAY_REWRITE_STATISTICS
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.
size_type size() const
Returns the size of the term_list.
bool defined() const
Returns true if this term is not equal to the term assigned by the default constructor of aterms,...
An abstraction expression.
const variable_list & variables() const
const data_expression & body() const
const binder_type & binding_operator() const
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.
\brief Assignment expression
\brief Assignment of a data expression to a variable
const data_expression & rhs() const
const variable & lhs() const
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.
class rewrite_stack m_rewrite_stack
void rewrite_aux_const_function_symbol(data_expression &result, const function_symbol &op, substitution_type &sigma)
data_expression rewrite(const data_expression &term, substitution_type &sigma)
Rewrite an mCRL2 data term.
RewriterJitty(const data_specification &data_spec, const used_data_equation_selector &)
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.
strategy create_strategy(const function_symbol &f, const data_equation_list &rules1, const data_specification &data_spec)
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)
const function_symbol & this_term_is_in_normal_form()
void subst_values(data_expression &result, const jitty_assignments_for_a_rewrite_rule &assignments, const data_expression &t, data::enumerator_identifier_generator &generator)
void rewrite_aux_function_symbol(data_expression &result, const function_symbol &op, const application &term, substitution_type &sigma)
data_expression remove_normal_form_function(const data_expression &t)
atermpp::detail::thread_aterm_pool * m_thread_aterm_pool
void rebuild_strategy(const data_specification &data_spec, const mcrl2::data::used_data_equation_selector &equation_selector)
std::vector< strategy > jitty_strat
std::map< function_symbol, data_equation_list > jitty_eqns
bool rewriting_in_progress
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.
std::vector< data_expression > rhs_for_constants_cache
Rewriter interface class.
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.
void rewrite_where(data_expression &result, const where_clause &term, substitution_type &sigma)
void existential_quantifier_enumeration(data_expression &result, const abstraction &t, substitution_type &sigma)
void universal_quantifier_enumeration(data_expression &result, const abstraction &t, substitution_type &sigma)
void rewrite_single_lambda(data_expression &result, const variable_list &vl, const data_expression &body, const bool body_in_normal_form, substitution_type &sigma)
enumerator_identifier_generator m_generator
std::set< std::size_t > m_dependencies
const std::set< std::size_t > & dependencies() const
const data_equation equation() const
dependencies_rewrite_rule_pair(std::set< std::size_t > &dependencies, const data_equation &eq)
jitty_argument_rewriter(mutable_indexed_substitution<> &sigma, RewriterJitty &r)
mutable_indexed_substitution & m_sigma
void operator()(data_expression &result, const data_expression &t)
void reserve_more_space()
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)
std::size_t stack_size() const
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.
const sort_expression & codomain() const
const sort_expression_list & domain() const
const sort_expression & sort() const
Generic substitution function.
Generic substitution function. The substitution is stored as a mapping of variables to expressions....
\brief Unknown sort expression
Component for selecting a subset of equations that are actually used in an encompassing specification...
const sort_expression & sort() const
\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.
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...
void increment_rewrite_count()
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)
std::set< variable > bound_variables_in_substitution(const jitty_assignments_for_a_rewrite_rule &assignments)
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.
std::vector< assignment > assignment_vector
\brief vector of assignments
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_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)
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
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)
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.
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 index(const Variable &x)
Returns the index of the variable.
jitty_variable_assignment_for_a_rewrite_rule * assignment
bool variable_is_a_normal_form
const data_expression & term
A rule describes a partially pattern-matched rewrite rule.