mcrl2::lps::detail::pattern_match_unfolder Class Reference

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

#include <lpsparunfoldlib.h>

Public Member Functions
	pattern_match_unfolder (unfold_data_manager &datamgr)
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	can_unfold (const data::data_expression &x)
std::vector< std::size_t >	pattern_matching_args (const data::function_symbol &f)
bool	matches_only_known_sorts (const data::function_symbol &f)
	Determines whether f pattern matches on argument arg.
template<class T >
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.

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)

Private Attributes
unfold_data_manager &	m_datamgr
data::representative_generator	m_repgen
std::map< data::function_symbol, bool >	m_is_pattern_matching
std::map< data::function_symbol, data::data_equation >	m_new_eqns

Detailed Description

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

Definition at line 276 of file lpsparunfoldlib.h.

Constructor & Destructor Documentation

pattern_match_unfolder()

mcrl2::lps::detail::pattern_match_unfolder::pattern_match_unfolder ( unfold_data_manager &  datamgr )

inline

Definition at line 341 of file lpsparunfoldlib.h.

Member Function Documentation

can_unfold()

bool mcrl2::lps::detail::pattern_match_unfolder::can_unfold ( const data::data_expression &  x )

inline

Definition at line 378 of file lpsparunfoldlib.h.

find_equations()

const data::data_equation_vector mcrl2::lps::detail::pattern_match_unfolder::find_equations ( const data::function_symbol &  f )

inlineprivate

Finds all rewriting equations for f.

Definition at line 285 of file lpsparunfoldlib.h.

is_constructor()

bool mcrl2::lps::detail::pattern_match_unfolder::is_constructor ( const data::function_symbol &  f )

inline

Definition at line 346 of file lpsparunfoldlib.h.

is_det_or_pi()

bool mcrl2::lps::detail::pattern_match_unfolder::is_det_or_pi ( const data::application &  expr ) const

inline

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).

Definition at line 353 of file lpsparunfoldlib.h.

is_pattern_matching()

bool mcrl2::lps::detail::pattern_match_unfolder::is_pattern_matching ( const data::function_symbol &  f )

inlineprivate

Checks whether f is defined by pattern matching.

Definition at line 299 of file lpsparunfoldlib.h.

matches_only_known_sorts()

bool mcrl2::lps::detail::pattern_match_unfolder::matches_only_known_sorts ( const data::function_symbol &  f )

inline

Determines whether f pattern matches on argument arg.

Precondition

this->can_unfold(f)

Definition at line 432 of file lpsparunfoldlib.h.

operator()()

template<class T >

void mcrl2::lps::detail::pattern_match_unfolder::operator() ( T &  result, const data::application &  x  )

inline

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

Precondition

this->can_unfold(x)

Definition at line 454 of file lpsparunfoldlib.h.

pattern_matching_args()

std::vector< std::size_t > mcrl2::lps::detail::pattern_match_unfolder::pattern_matching_args ( const data::function_symbol &  f )

inline

Definition at line 405 of file lpsparunfoldlib.h.

unfolded_expr()

data::data_expression mcrl2::lps::detail::pattern_match_unfolder::unfolded_expr ( const data::function_symbol &  f, const data::data_expression_vector &  args  )

inlineprivate

Definition at line 313 of file lpsparunfoldlib.h.

Member Data Documentation

m_datamgr

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

private

Definition at line 279 of file lpsparunfoldlib.h.

m_is_pattern_matching

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

private

Definition at line 281 of file lpsparunfoldlib.h.

m_new_eqns

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

private

Definition at line 282 of file lpsparunfoldlib.h.

m_repgen

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

private

Definition at line 280 of file lpsparunfoldlib.h.

---

The documentation for this class was generated from the following file:

• lps/include/mcrl2/lps/lpsparunfoldlib.h