quantifier_propagate.h File Reference

Go to the source code of this file.

Classes
class	mcrl2::pbes_system::detail::quantifier
struct	mcrl2::pbes_system::detail::quantifier_propagate_builder

Namespaces
namespace	mcrl2
namespace	mcrl2::pbes_system
	The main namespace for the PBES library.
namespace	mcrl2::pbes_system::detail

Functions
pbes_expression	mcrl2::pbes_system::detail::quantifier_propagate (const pbes_expression &x)
pbes_expression	mcrl2::pbes_system::detail::make_exists_ (std::set< data::variable > vars, const pbes_expression &expr)
pbes_expression	mcrl2::pbes_system::detail::make_forall_ (std::set< data::variable > vars, const pbes_expression &expr)
pbes_expression	mcrl2::pbes_system::detail::make_quantifier (bool is_forall, const data::variable_list &vars, const pbes_expression &body)
void	mcrl2::pbes_system::detail::quantifier_propagate (std::list< std::pair< core::identifier_string, pbes_equation > > &new_equations, data::set_identifier_generator &id_gen, const quantifier_propagate_builder::equation_map_t eqn_map, pbes_expression &x)
void	mcrl2::pbes_system::quantifier_propagate (pbes &p)
pbes	mcrl2::pbes_system::quantifier_propagate (const pbes &p)