mCRL2
Loading...
Searching...
No Matches
Public Types | Public Member Functions | Public Attributes | List of all members
mcrl2::state_formulas::detail::state_formula_data_variable_name_clash_resolver Class Reference

#include <resolve_name_clashes.h>

Inheritance diagram for mcrl2::state_formulas::detail::state_formula_data_variable_name_clash_resolver:
mcrl2::state_formulas::data_expression_builder< state_formula_data_variable_name_clash_resolver > mcrl2::state_formulas::add_data_expressions< Builder, Derived >

Public Types

using super = state_formulas::data_expression_builder< state_formula_data_variable_name_clash_resolver >
 
- Public Types inherited from mcrl2::state_formulas::add_data_expressions< Builder, Derived >
using super = Builder< Derived >
 

Public Member Functions

 state_formula_data_variable_name_clash_resolver (data::set_identifier_generator &generator_)
 
void insert (const data::variable &v)
 
void erase (const data::variable &v)
 
data::assignment_list apply_assignments (const data::assignment_list &x)
 
data::variable_list apply_variables (const data::variable_list &x)
 
template<class T >
void apply (T &result, const mu &x)
 
template<class T >
void apply (T &result, const nu &x)
 
template<class T >
void apply (T &result, const forall &x)
 
template<class T >
void apply (T &result, const exists &x)
 
template<class T >
void apply (T &result, const action_formulas::forall &x)
 
template<class T >
void apply (T &result, const action_formulas::exists &x)
 
template<class T >
void apply (T &result, const data::data_expression &x)
 
- Public Member Functions inherited from mcrl2::state_formulas::add_data_expressions< Builder, Derived >
template<class T >
void apply (T &result, const state_formulas::true_ &x)
 
template<class T >
void apply (T &result, const state_formulas::false_ &x)
 
template<class T >
void apply (T &result, const state_formulas::not_ &x)
 
template<class T >
void apply (T &result, const state_formulas::minus &x)
 
template<class T >
void apply (T &result, const state_formulas::and_ &x)
 
template<class T >
void apply (T &result, const state_formulas::or_ &x)
 
template<class T >
void apply (T &result, const state_formulas::imp &x)
 
template<class T >
void apply (T &result, const state_formulas::plus &x)
 
template<class T >
void apply (T &result, const state_formulas::const_multiply &x)
 
template<class T >
void apply (T &result, const state_formulas::const_multiply_alt &x)
 
template<class T >
void apply (T &result, const state_formulas::forall &x)
 
template<class T >
void apply (T &result, const state_formulas::exists &x)
 
template<class T >
void apply (T &result, const state_formulas::infimum &x)
 
template<class T >
void apply (T &result, const state_formulas::supremum &x)
 
template<class T >
void apply (T &result, const state_formulas::sum &x)
 
template<class T >
void apply (T &result, const state_formulas::must &x)
 
template<class T >
void apply (T &result, const state_formulas::may &x)
 
template<class T >
void apply (T &result, const state_formulas::yaled &x)
 
template<class T >
void apply (T &result, const state_formulas::yaled_timed &x)
 
template<class T >
void apply (T &result, const state_formulas::delay &x)
 
template<class T >
void apply (T &result, const state_formulas::delay_timed &x)
 
template<class T >
void apply (T &result, const state_formulas::variable &x)
 
template<class T >
void apply (T &result, const state_formulas::nu &x)
 
template<class T >
void apply (T &result, const state_formulas::mu &x)
 
void update (state_formulas::state_formula_specification &x)
 
template<class T >
void apply (T &result, const state_formulas::state_formula &x)
 

Public Attributes

data::set_identifier_generator & generator
 
std::multiset< data::variable > bound_variables
 
std::map< data::variable, std::vector< data::variable > > substitutions
 

Detailed Description

Definition at line 143 of file resolve_name_clashes.h.

Member Typedef Documentation

◆ super

using mcrl2::state_formulas::detail::state_formula_data_variable_name_clash_resolver::super = state_formulas::data_expression_builder<state_formula_data_variable_name_clash_resolver>

Definition at line 146 of file resolve_name_clashes.h.

Constructor & Destructor Documentation

◆ state_formula_data_variable_name_clash_resolver()

mcrl2::state_formulas::detail::state_formula_data_variable_name_clash_resolver::state_formula_data_variable_name_clash_resolver ( data::set_identifier_generator &  generator_)
inlineexplicit

Definition at line 156 of file resolve_name_clashes.h.

Member Function Documentation

◆ apply() [1/7]

template<class T >
void mcrl2::state_formulas::detail::state_formula_data_variable_name_clash_resolver::apply ( T &  result,
const action_formulas::exists &  x 
)
inline

Definition at line 286 of file resolve_name_clashes.h.

◆ apply() [2/7]

template<class T >
void mcrl2::state_formulas::detail::state_formula_data_variable_name_clash_resolver::apply ( T &  result,
const action_formulas::forall &  x 
)
inline

Definition at line 270 of file resolve_name_clashes.h.

◆ apply() [3/7]

template<class T >
void mcrl2::state_formulas::detail::state_formula_data_variable_name_clash_resolver::apply ( T &  result,
const data::data_expression &  x 
)
inline

Definition at line 302 of file resolve_name_clashes.h.

◆ apply() [4/7]

template<class T >
void mcrl2::state_formulas::detail::state_formula_data_variable_name_clash_resolver::apply ( T &  result,
const exists &  x 
)
inline

Definition at line 255 of file resolve_name_clashes.h.

◆ apply() [5/7]

template<class T >
void mcrl2::state_formulas::detail::state_formula_data_variable_name_clash_resolver::apply ( T &  result,
const forall &  x 
)
inline

Definition at line 240 of file resolve_name_clashes.h.

◆ apply() [6/7]

template<class T >
void mcrl2::state_formulas::detail::state_formula_data_variable_name_clash_resolver::apply ( T &  result,
const mu &  x 
)
inline

Definition at line 210 of file resolve_name_clashes.h.

◆ apply() [7/7]

template<class T >
void mcrl2::state_formulas::detail::state_formula_data_variable_name_clash_resolver::apply ( T &  result,
const nu &  x 
)
inline

Definition at line 225 of file resolve_name_clashes.h.

◆ apply_assignments()

data::assignment_list mcrl2::state_formulas::detail::state_formula_data_variable_name_clash_resolver::apply_assignments ( const data::assignment_list &  x)
inline

Definition at line 187 of file resolve_name_clashes.h.

◆ apply_variables()

data::variable_list mcrl2::state_formulas::detail::state_formula_data_variable_name_clash_resolver::apply_variables ( const data::variable_list &  x)
inline

Definition at line 198 of file resolve_name_clashes.h.

◆ erase()

void mcrl2::state_formulas::detail::state_formula_data_variable_name_clash_resolver::erase ( const data::variable &  v)
inline

Definition at line 169 of file resolve_name_clashes.h.

◆ insert()

void mcrl2::state_formulas::detail::state_formula_data_variable_name_clash_resolver::insert ( const data::variable &  v)
inline

Definition at line 160 of file resolve_name_clashes.h.

Member Data Documentation

◆ bound_variables

std::multiset<data::variable> mcrl2::state_formulas::detail::state_formula_data_variable_name_clash_resolver::bound_variables

Definition at line 153 of file resolve_name_clashes.h.

◆ generator

data::set_identifier_generator& mcrl2::state_formulas::detail::state_formula_data_variable_name_clash_resolver::generator

Definition at line 152 of file resolve_name_clashes.h.

◆ substitutions

std::map<data::variable, std::vector<data::variable> > mcrl2::state_formulas::detail::state_formula_data_variable_name_clash_resolver::substitutions

Definition at line 154 of file resolve_name_clashes.h.

The documentation for this class was generated from the following file: