9#ifndef MCRL2_DATA_UNFOLD_PATTERN_MATCHING_H
10#define MCRL2_DATA_UNFOLD_PATTERN_MATCHING_H
60 rule(
const std::map<data_expression, data_expression>& mc,
89 return atermpp::down_cast<function_symbol>(expr);
93 const application& expr_appl = atermpp::down_cast<application>(expr);
96 return atermpp::down_cast<function_symbol>(expr_appl.
head());
118 if (rules.size() == 0)
120 return representative;
124 for (
const rule& r: rules)
126 std::map<variable, data_expression> substitution_map;
127 for (
const auto& [var_expr, pattern]: r.match_criteria)
130 substitution_map[atermpp::down_cast<variable>(pattern)] = var_expr;
143 result =
lazy::if_(condition, rhs, result);
153template <
typename StructInfo>
157 const std::vector<rule>& rules,
185 NONE, INCOMPLETE, PARTIAL, FULL
187 MatchType matching_type = MatchType::NONE;
190 for (
const auto& [var_expr, _]: rules[0].match_criteria)
192 bool variable_seen =
false;
193 std::set<function_symbol> constructors_seen;
194 for (
const rule& r: rules)
199 variable_seen =
true;
206 assert(ssf.is_constructor(fs));
207 constructors_seen.insert(fs);
211 MatchType new_matching_type;
212 if (constructors_seen.empty())
215 new_matching_type = MatchType::NONE;
217 else if (variable_seen)
221 new_matching_type = MatchType::PARTIAL;
223 else if (constructors_seen.size() != ssf.get_constructors(var_expr.sort()).size())
228 new_matching_type = MatchType::INCOMPLETE;
234 new_matching_type = MatchType::FULL;
237 if (new_matching_type > matching_type)
239 matching_target = var_expr;
240 matching_type = new_matching_type;
242 if (matching_type == MatchType::FULL)
248 if (matching_type == MatchType::NONE)
259 const auto& match_constructors = ssf.get_constructors(matching_target.
sort());
260 std::map<function_symbol, std::vector<rule> > constructor_rules;
261 for (
const rule& r: rules)
277 const application& pattern_appl = atermpp::down_cast<application>(pattern);
278 parameters.insert(parameters.end(), pattern_appl.
begin(), pattern_appl.
end());
286 if (!parameters.empty() && std::none_of(subexpr.begin(), subexpr.end(), [](
const data_expression& e) { return is_abstraction(e); }))
292 for (std::size_t j = 0; j < parameters.size(); j++)
294 function_symbol projection_function = ssf.get_projection_funcs(constructor)[j];
298 constructor_rules[constructor].push_back(
rule);
315 rule rule(r.match_criteria, rhs, condition, r.variables);
319 for (
const variable& v: r.variables)
327 std::size_t index = 0;
331 function_symbol projection_function = ssf.get_projection_funcs(f)[index];
338 constructor_rules[f].push_back(
rule);
348 for (
const auto& f: match_constructors)
350 rhs.push_back(
construct_rhs(ssf, gen, constructor_rules[f], sort));
352 return ssf.create_cases(matching_target, rhs);
362template <
typename StructInfo>
369 subexpressions.erase(rewrite_rule.
lhs());
375 bool all_pattern = std::all_of(subexpressions.begin(), subexpressions.end(), [&ssf](
const data_expression& expr) {
378 (is_function_symbol(expr) && ssf.is_constructor(atermpp::down_cast<function_symbol>(expr))) ||
379 (is_application(expr) && is_function_symbol(atermpp::down_cast<application>(expr).head()) &&
380 ssf.is_constructor(function_symbol(atermpp::down_cast<application>(expr).head())));
386 if (std::all_of(subexpressions.begin(), subexpressions.end(), [](
const data_expression& x){ return is_variable(x); }))
393 std::set<variable> variable_set;
394 std::multiset<variable> variable_multiset;
397 return variable_set.size() == variable_multiset.size();
436template <
typename StructInfo>
452 temp_par.push_back(
variable(id_gen(
"x"), s));
455 variable_list new_parameters(temp_par.begin(), temp_par.end());
458 std::vector<detail::rule> rules;
463 std::map<data_expression, data_expression> match_criteria;
466 const application& lhs_appl = atermpp::down_cast<application>(eq.lhs());
468 assert(lhs_appl.
head() == mapping);
469 assert(new_parameters.
size() == lhs_appl.
size());
473 auto mappar_it = new_parameters.
begin();
474 auto lhspar_it = lhs_appl.
begin();
475 while(mappar_it != new_parameters.
end())
477 match_criteria[*mappar_it] = *lhspar_it;
478 ++mappar_it, ++lhspar_it;
481 assert(lhspar_it == lhs_appl.
end());
484 detail::rule rule(match_criteria, eq.rhs(), eq.condition(), eq.variables());
485 rules.push_back(rule);
487#ifdef MCRL2_ENABLE_MACHINENUMBERS
490 assert(rules.size() != 0);
size_type size() const
Returns the size of the term_list.
const_iterator end() const
Returns a const_iterator pointing to the end of the term_list.
const_iterator begin() const
Returns a const_iterator pointing to the beginning of the term_list.
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.
const data_expression & lhs() const
sort_expression sort() const
Returns the sort of the data expression.
const sort_expression_list & domain() const
const sort_expression & sort() const
Components for generating an arbitrary element of a sort.
Identifier generator that stores the identifiers of the context in a set. Using the operator()() and ...
void add_identifier(const core::identifier_string &s) override
Adds the identifier s to the context.
const sort_expression & target_sort() const
Returns the target sort of this expression.
Join and split functions for data expressions.
add your file description here.
static RewriterCompilingJitty::substitution_type & sigma(RewriterCompilingJitty *this_rewriter)
add your file description here.
std::string print_map(const MapContainer &v, const std::string &message="")
Creates a string representation of a map.
std::string print_list(const Container &v, const std::string &message="", bool print_index=false, bool boundary_spaces=true)
Creates a string representation of a container.
data_expression construct_rhs(StructInfo &ssf, representative_generator &gen, const std::vector< rule > &rules, const sort_expression &sort)
For a list of rules with equal left hand sides of match_criteria, construct a right hand side.
data_expression construct_condition_rhs(const std::vector< rule > &rules, const data_expression &representative)
For a list of rules with equal left hand sides of match_criteria and only variables in the right hand...
std::ostream & operator<<(std::ostream &os, smt_solver_type s)
standard conversion from solvert type to stream
function_symbol get_top_fs(const data_expression &expr)
Get the top level function symbol f if expr is of the shape f or f(t1,...,tn)
data_expression if_(const data_expression &cond, const data_expression &then, const data_expression &else_)
Returns an expression equivalent to if(cond,then,else_)
const basic_sort & bool_()
Constructor for sort expression Bool.
bool is_most_significant_digit_function_symbol(const atermpp::aterm &e)
Recogniser for function @most_significant_digit.
Namespace for all data library functionality.
std::set< data::variable > find_all_variables(const data::data_expression &x)
std::vector< data_equation > data_equation_vector
\brief vector of data_equations
std::vector< variable > variable_vector
\brief vector of variables
std::vector< data_expression > data_expression_vector
\brief vector of data_expressions
void replace_data_expressions(T &x, const Substitution &sigma, bool innermost, typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
bool is_function_symbol(const atermpp::aterm &x)
Returns true if the term t is a function symbol.
bool is_pattern_matching_rule(StructInfo &ssf, const data_equation &rewrite_rule)
Check whether the given rewrite rule can be classified as a pattern matching rule.
void find_data_expressions(const T &x, OutputIterator o)
Returns all data expressions that occur in an object.
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.
bool is_application(const atermpp::aterm &x)
Returns true if the term t is an application.
data_equation unfold_pattern_matching(const function_symbol &mapping, const data_equation_vector &rewrite_rules, StructInfo &ssf, representative_generator &gen, set_identifier_generator &id_gen)
This converts a collection of rewrite rules for a give function symbol into a one-rule specification ...
bool is_variable(const atermpp::aterm &x)
Returns true if the term t is a variable.
bool contains(const atermpp::indexed_set< Key, ThreadSafe, Hash, Equals, Allocator, KeyTable > &c, const typename atermpp::indexed_set< Key, ThreadSafe, Hash, Equals, Allocator, KeyTable >::key_type &v, const std::size_t thread_index=0)
Component for generating representatives of sorts.
A rule describes a partially pattern-matched rewrite rule.
std::map< data_expression, data_expression > match_criteria
rule(const std::map< data_expression, data_expression > &mc, const data_expression &r, const data_expression &c, const variable_list &v)
data_expression condition
Generic substitution function. The substitution is stored as a mapping of variables to expressions.
Substitution that maps a single variable to a data expression.