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¶

void apply(T &result, const action_formulas::exists &x)¶

void apply(T &result, const action_formulas::forall &x)¶

void apply(T &result, const data::data_expression &x)¶

void apply(T &result, const exists &x)

void apply(T &result, const forall &x)

void apply(T &result, const mu &x)¶

void apply(T &result, const nu &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_)¶