unfold_pattern_matching.h File Reference

Go to the source code of this file.

Classes
struct	mcrl2::data::detail::rule
	A rule describes a partially pattern-matched rewrite rule. More...

Namespaces
namespace	mcrl2
	A class that takes a linear process specification and checks all tau-summands of that LPS for confluence.
namespace	mcrl2::data
	Namespace for all data library functionality.
namespace	mcrl2::data::detail

Functions
std::ostream &	mcrl2::data::detail::operator<< (std::ostream &out, const rule &r)
function_symbol	mcrl2::data::detail::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	mcrl2::data::detail::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 sides of match_criteria, construct a right hand side based on the conditions and right hand sides of the rules.
template<typename StructInfo >
data_expression	mcrl2::data::detail::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.
template<typename StructInfo >
bool	mcrl2::data::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.
template<typename StructInfo >
data_equation	mcrl2::data::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 of the function, using recogniser and projection functions to implement pattern matching.