quantifiers_inside_rewriter.h File Reference

Go to the source code of this file.

Classes
struct	mcrl2::data::detail::quantifiers_inside_builder
struct	mcrl2::data::detail::quantifiers_inside_forall_builder
struct	mcrl2::data::detail::quantifiers_inside_exists_builder
struct	mcrl2::data::quantifiers_inside_rewriter

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
data_expression	mcrl2::data::detail::quantifiers_inside (const data_expression &x)
data_expression	mcrl2::data::detail::quantifiers_inside_forall (const std::set< variable > &variables, const data_expression &x)
data_expression	mcrl2::data::detail::quantifiers_inside_exists (const std::set< variable > &variables, const data_expression &x)
std::set< variable >	mcrl2::data::detail::make_variable_set (const variable_list &x)
variable_list	mcrl2::data::detail::make_variable_list (const std::set< variable > &x)
template<typename BinaryOperation >
std::tuple< data_expression, data_expression >	mcrl2::data::detail::compute_Phi_Psi (const std::vector< data_expression > &X, const std::set< variable > &V, BinaryOperation op, data_expression empty_sequence_result)
template<typename T >
void	mcrl2::data::quantifiers_inside_rewrite (T &x, typename std::enable_if< !std::is_base_of< atermpp::aterm, T >::value >::type *=0)
template<typename T >
T	mcrl2::data::quantifiers_inside_rewrite (const T &x, typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *=0)