mCRL2
Loading...
Searching...
No Matches
find_equalities.h
Go to the documentation of this file.
1// Author(s): Wieger Wesselink
2// Copyright: see the accompanying file COPYING or copy at
3// https://github.com/mCRL2org/mCRL2/blob/master/COPYING
4//
5// Distributed under the Boost Software License, Version 1.0.
6// (See accompanying file LICENSE_1_0.txt or copy at
7// http://www.boost.org/LICENSE_1_0.txt)
8//
11
12#ifndef MCRL2_PBES_FIND_EQUALITIES_H
13#define MCRL2_PBES_FIND_EQUALITIES_H
14
17
18namespace mcrl2 {
19
20namespace pbes_system {
21
22namespace detail {
23
24template <template <class> class Traverser, class Derived>
26{
28 using super::enter;
29 using super::leave;
30 using super::apply;
31 using super::push;
32 using super::pop;
33 using super::top;
34 using super::below_top;
35
36 Derived& derived()
37 {
38 return static_cast<Derived&>(*this);
39 }
40
41 void leave(const and_&)
42 {
43 auto& left = below_top();
44 auto const& right = top();
45 left.join_and(right);
46 pop();
47 }
48
49 void leave(const or_&)
50 {
51 auto& left = below_top();
52 auto const& right = top();
53 left.join_or(right);
54 pop();
55 }
56
57 void leave(const imp&)
58 {
59 auto& left = below_top();
60 auto const& right = top();
61 left.swap();
62 left.join_or(right);
63 pop();
64 }
65
66 void leave(const not_&)
67 {
68 top().swap();
69 }
70
71 void leave(const forall& x)
72 {
73 top().delete_(x.variables());
74 }
75
76 void leave(const exists& x)
77 {
78 top().delete_(x.variables());
79 }
80
81 // N.B. Use apply here, to avoid going into the recursion
83 {
85 }
86
87#if BOOST_MSVC
89#endif
90};
91
92struct find_equalities_traverser_inst: public pbes_system::detail::find_equalities_traverser<pbes_system::data_expression_traverser, find_equalities_traverser_inst>
93{
95
96 using super::enter;
97 using super::leave;
98 using super::apply;
99};
100
101} // namespace detail
102
103inline
104std::map<data::variable, std::set<data::data_expression> > find_equalities(const pbes_expression& x)
105{
107 f.apply(x);
108 assert(f.expression_stack.size() == 1);
109 f.top().close();
110 return f.top().equalities.assignments;
111}
112
113inline
114std::map<data::variable, std::set<data::data_expression> > find_inequalities(const pbes_expression& x)
115{
117 f.apply(x);
118 assert(f.expression_stack.size() == 1);
119 f.top().close();
120 return f.top().inequalities.assignments;
121}
122
123} // namespace pbes_system
124
125} // namespace mcrl2
126
127#endif // MCRL2_PBES_FIND_EQUALITIES_H
void swap(unprotected_aterm_core &t) noexcept
Swaps this term with its argument.
Definition aterm_core.h:152
\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...
Definition indexed_set.h:72
add your file description here.
void push(const find_equalities_expression &x)
std::vector< find_equalities_expression > expression_stack
pbes_system::detail::find_equalities_traverser< pbes_system::data_expression_traverser, find_equalities_traverser_inst > super
void push(const find_equalities_expression &x)
data::detail::find_equalities_traverser< Traverser, Derived > super
void apply(const propositional_variable_instantiation &)
add your file description here.