mcrl2/pbes/rewriters/quantifiers_inside_rewriter.h

Include file:

#include "mcrl2/pbes/rewriters/quantifiers_inside_rewriter.h"

add your file description here.

Classes

• mcrl2::pbes_system::detail::quantifiers_inside_builder
• mcrl2::pbes_system::detail::quantifiers_inside_exists_builder
• mcrl2::pbes_system::detail::quantifiers_inside_forall_builder
• mcrl2::pbes_system::quantifiers_inside_rewriter

Functions

std::tuple<pbes_expression, pbes_expression> mcrl2::pbes_system::detail::compute_Phi_Psi(const std::vector<pbes_expression> &X, const std::set<data::variable> &V, BinaryOperation op, pbes_expression empty_sequence_result)

pbes_expression quantifiers_inside(const pbes_expression &x)

pbes_expression quantifiers_inside_exists(const std::set<data::variable> &variables, const pbes_expression &x)

pbes_expression quantifiers_inside_forall(const std::set<data::variable> &variables, const pbes_expression &x)