12#ifndef MCRL2_PBES_FIND_EQUALITIES_H
13#define MCRL2_PBES_FIND_EQUALITIES_H
20namespace pbes_system {
24template <
template <
class>
class Traverser,
class Derived>
38 return static_cast<Derived&
>(*this);
44 auto const& right =
top();
52 auto const& right =
top();
60 auto const& right =
top();
110 return f.
top().equalities.assignments;
120 return f.
top().inequalities.assignments;
void swap(unprotected_aterm_core &t) noexcept
Swaps this term with its argument.
\brief The and operator for pbes expressions
\brief The existential quantification operator for pbes expressions
const data::variable_list & variables() const
\brief The universal quantification operator for pbes expressions
const data::variable_list & variables() const
\brief The implication operator for pbes expressions
\brief The not operator for pbes expressions
\brief The or operator for pbes expressions
\brief A propositional variable instantiation
add your file description here.
std::map< data::variable, std::set< data::data_expression > > find_equalities(const pbes_expression &x)
std::map< data::variable, std::set< data::data_expression > > find_inequalities(const pbes_expression &x)
A class that takes a linear process specification and checks all tau-summands of that LPS for conflue...
add your file description here.
find_equalities_expression & below_top()
find_equalities_expression pop()
void push(const find_equalities_expression &x)
void leave(const data::variable &x)
void apply(const data::application &x)
find_equalities_expression & top()
std::vector< find_equalities_expression > expression_stack
pbes_system::detail::find_equalities_traverser< pbes_system::data_expression_traverser, find_equalities_traverser_inst > super
find_equalities_expression & below_top()
find_equalities_expression pop()
void push(const find_equalities_expression &x)
data::detail::find_equalities_traverser< Traverser, Derived > super
void apply(const propositional_variable_instantiation &)
void leave(const forall &x)
find_equalities_expression & top()
void leave(const exists &x)
add your file description here.