rewrite.cpp File Reference

Go to the source code of this file.

Classes
struct	mcrl2::data::detail::is_a_variable

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
static bool	mcrl2::data::detail::occur_check (const variable &v, const atermpp::aterm &e)
std::shared_ptr< detail::Rewriter >	mcrl2::data::detail::createRewriter (const data_specification &DataSpec, const used_data_equation_selector &equations_selector, const rewrite_strategy Strategy=jitty)
	Create a rewriter.
static void	mcrl2::data::detail::check_vars (const data_expression &expr, const std::set< variable > &vars, std::set< variable > &used_vars)
static void	mcrl2::data::detail::check_vars (application::const_iterator begin, const application::const_iterator &end, const std::set< variable > &vars, std::set< variable > &used_vars)
static void	mcrl2::data::detail::checkPattern (const data_expression &p)
static void	mcrl2::data::detail::checkPattern (application::const_iterator begin, const application::const_iterator &end)
void	mcrl2::data::detail::CheckRewriteRule (const data_equation &data_eqn)
	Check that an mCRL2 data equation is a valid rewrite rule. If not, an runtime_error is thrown indicating the problem.
bool	mcrl2::data::detail::isValidRewriteRule (const data_equation &data_eqn)
	Check whether or not an mCRL2 data equation is a valid rewrite rule.