mcrl2::state_formulas::detail::state_formula_data_variable_name_clash_resolver

Include file:

#include "mcrl2/modal_formula/resolve_name_clashes.h
class mcrl2::state_formulas::detail::state_formula_data_variable_name_clash_resolver

Public types

type mcrl2::state_formulas::detail::state_formula_data_variable_name_clash_resolver::super

typedef for state_formulas::data_expression_builder< state_formula_data_variable_name_clash_resolver >

Public attributes

std::multiset<data::variable> mcrl2::state_formulas::detail::state_formula_data_variable_name_clash_resolver::bound_variables
data::set_identifier_generator &mcrl2::state_formulas::detail::state_formula_data_variable_name_clash_resolver::generator
std::map<data::variable, std::vector<data::variable>> mcrl2::state_formulas::detail::state_formula_data_variable_name_clash_resolver::substitutions

Public member functions

state_formula apply(const mu &x)
state_formula apply(const nu &x)
state_formula apply(const forall &x)
state_formula apply(const exists &x)
data::data_expression apply(const data::data_expression &x)
data::assignment_list apply_assignments(const data::assignment_list &x)
data::variable_list apply_variables(const data::variable_list &x)
void erase(const data::variable &v)
void insert(const data::variable &v)
state_formula_data_variable_name_clash_resolver(data::set_identifier_generator &generator_)