Visitor for determining if within the scope of a quantifier there are quantifier variables of free variables with the same name. More...
#include <is_well_typed.h>
Public Types | |
| using | super = pbes_expression_traverser< has_quantifier_name_clashes_traverser > |
 Public Types inherited from mcrl2::pbes_system::add_traverser_pbes_expressions< Traverser, Derived > | |
| using | super = Traverser< Derived > |
Public Member Functions | |
| bool | is_in_quantifier_stack (const core::identifier_string &name) const |
| Returns true if the quantifier_stack contains a data variable with the given name. | |
| void | push (const data::variable_list &variables) |
| Adds variables to the quantifier stack, and adds replacements for the name clashes to replacements. | |
| void | pop () |
| Pops the quantifier stack. | |
| void | enter (const forall &x) |
| void | leave (const forall &) |
| void | enter (const exists &x) |
| void | leave (const exists &) |
| Public Member Functions inherited from mcrl2::pbes_system::add_traverser_pbes_expressions< Traverser, Derived > | |
| void | apply (const pbes_system::pbes_equation &x) |
| void | apply (const pbes_system::pbes &x) |
| void | apply (const pbes_system::propositional_variable_instantiation &x) |
| void | apply (const pbes_system::not_ &x) |
| void | apply (const pbes_system::and_ &x) |
| void | apply (const pbes_system::or_ &x) |
| void | apply (const pbes_system::imp &x) |
| void | apply (const pbes_system::forall &x) |
| void | apply (const pbes_system::exists &x) |
| void | apply (const pbes_system::pbes_expression &x) |
Public Attributes | |
| std::vector< data::variable_list > | quantifier_stack |
| bool | result = false |
| data::variable | name_clash |
Detailed Description
Visitor for determining if within the scope of a quantifier there are quantifier variables of free variables with the same name.
Definition at line 56 of file is_well_typed.h.
Member Typedef Documentation
◆ super
| using mcrl2::pbes_system::detail::has_quantifier_name_clashes_traverser::super = pbes_expression_traverser<has_quantifier_name_clashes_traverser> |
Definition at line 58 of file is_well_typed.h.
Member Function Documentation
◆ enter() [1/2]
|
inline |
Definition at line 127 of file is_well_typed.h.
◆ enter() [2/2]
|
inline |
Definition at line 117 of file is_well_typed.h.
◆ is_in_quantifier_stack()
|
inline |
Returns true if the quantifier_stack contains a data variable with the given name.
- Parameters
-
name A
- Returns
- True if the quantifier_stack contains a data variable with the given name
Definition at line 70 of file is_well_typed.h.
◆ leave() [1/2]
|
inline |
Definition at line 132 of file is_well_typed.h.
◆ leave() [2/2]
|
inline |
Definition at line 122 of file is_well_typed.h.
◆ pop()
|
inline |
Pops the quantifier stack.
Definition at line 108 of file is_well_typed.h.
◆ push()
|
inline |
Adds variables to the quantifier stack, and adds replacements for the name clashes to replacements.
- Parameters
-
variables A sequence of data variables
- Returns
- The number of replacements that were added.
Definition at line 89 of file is_well_typed.h.
Member Data Documentation
◆ name_clash
| data::variable mcrl2::pbes_system::detail::has_quantifier_name_clashes_traverser::name_clash |
Definition at line 65 of file is_well_typed.h.
◆ quantifier_stack
| std::vector<data::variable_list> mcrl2::pbes_system::detail::has_quantifier_name_clashes_traverser::quantifier_stack |
Definition at line 63 of file is_well_typed.h.
◆ result
| bool mcrl2::pbes_system::detail::has_quantifier_name_clashes_traverser::result = false |
Definition at line 64 of file is_well_typed.h.
The documentation for this struct was generated from the following file:
- pbes/include/mcrl2/pbes/detail/is_well_typed.h
