mcrl2::lps::detail::pattern_match_unfolder

Include file:

#include "mcrl2/lps/lpsparunfoldlib.h

class mcrl2::lps::detail::pattern_match_unfolder

Class for unfolding expressions f(a1,…,an) based on the pattern-matching rewrite rules that define f.

Private attributes

unfold_data_manager &mcrl2::lps::detail::pattern_match_unfolder::m_datamgr

std::map<data::function_symbol, bool> mcrl2::lps::detail::pattern_match_unfolder::m_is_pattern_matching

std::map<data::function_symbol, data::data_equation> mcrl2::lps::detail::pattern_match_unfolder::m_new_eqns

data::representative_generator mcrl2::lps::detail::pattern_match_unfolder::m_repgen

Private member functions

const data::data_equation_vector find_equations(const data::function_symbol &f)

Finds all rewriting equations for f.

bool is_pattern_matching(const data::function_symbol &f)

Checks whether f is defined by pattern matching.

data::data_expression unfolded_expr(const data::function_symbol &f, const data::data_expression_vector &args)

Public member functions

bool can_unfold(const data::data_expression &x)

bool is_constructor(const data::function_symbol &f)

bool is_det_or_pi(const data::application &expr) const

Checks whether expr is of the shape Det(h(a1,…,an)) or pi(h(a1,…,an)), where h is defined by patter matching, and, if so, unfolds h(a1,…,an).

bool matches_only_known_sorts(const data::function_symbol &f)

Determines whether f pattern matches on argument arg.

Pre: this->can_unfold(f)

void operator()(T &result, const data::application &x)

Unfolds expr if it is of the shape h(a1,…,an) and h is defined by pattern matching.

Pre: this->can_unfold(x)

pattern_match_unfolder(unfold_data_manager &datamgr)

std::vector<std::size_t> pattern_matching_args(const data::function_symbol &f)