mcrl2/pbes/quantifier_propagate.h

Include file:

#include "mcrl2/pbes/quantifier_propagate.h"

Classes

Functions

void mcrl2::pbes_system::quantifier_propagate(pbes &p)
pbes mcrl2::pbes_system::quantifier_propagate(const pbes &p)

Functions

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)
pbes_expression mcrl2::pbes_system::detail::quantifier_propagate(const pbes_expression &x)
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)