mCRL2
Searching...
No Matches
quantifiers_inside_rewriter.h
Go to the documentation of this file.
2// Copyright: see the accompanying file COPYING or copy at
3// https://github.com/mCRL2org/mCRL2/blob/master/COPYING
4//
6// (See accompanying file LICENSE_1_0.txt or copy at
8//
11
12#ifndef MCRL2_PBES_REWRITERS_QUANTIFIERS_INSIDE_REWRITER_H
13#define MCRL2_PBES_REWRITERS_QUANTIFIERS_INSIDE_REWRITER_H
14
15
16#include "mcrl2/pbes/builder.h"
17#include "mcrl2/pbes/join.h"
18
19namespace mcrl2 {
20
21namespace pbes_system {
22
23namespace detail {
24
25pbes_expression quantifiers_inside(const pbes_expression& x);
26pbes_expression quantifiers_inside_forall(const std::set<data::variable>& variables, const pbes_expression& x);
27pbes_expression quantifiers_inside_exists(const std::set<data::variable>& variables, const pbes_expression& x);
28
29template <typename BinaryOperation>
30std::tuple<pbes_expression, pbes_expression> compute_Phi_Psi(const std::vector<pbes_expression>& X, const std::set<data::variable>& V, BinaryOperation op, pbes_expression empty_sequence_result)
31{
34
35 std::vector<std::set<data::variable>> vars; // free variables
36 for (const pbes_expression& x_j: X)
37 {
38 vars.push_back(set_intersection(find_free_variables(x_j), V));
39 }
40 auto j = std::min_element(vars.begin(), vars.end(),
41 [&](const std::set<data::variable>& x, const std::set<data::variable>& y)
42 {
43 return x.size() < y.size();
44 }
45 );
46 const std::set<data::variable>& Z = *j;
47
48 std::vector<pbes_expression> phi;
49 std::vector<pbes_expression> psi;
50 for (std::size_t i = 0; i < X.size(); i++)
51 {
52 if (std::includes(Z.begin(), Z.end(), vars[i].begin(), vars[i].end()))
53 {
54 phi.push_back(X[i]);
55 }
56 else
57 {
58 psi.push_back(X[i]);
59 }
60 }
61 pbes_expression Phi = utilities::detail::join(phi.begin(), phi.end(), op, empty_sequence_result);
62 pbes_expression Psi = utilities::detail::join(psi.begin(), psi.end(), op, empty_sequence_result);
63 return { Phi, Psi };
64}
65
66struct quantifiers_inside_builder: public pbes_expression_builder<quantifiers_inside_builder>
67{
69 using super::apply;
70
71 template <class T>
72 void apply(T& result, const forall& x)
73 {
74 pbes_expression const& phi = x.body();
75 std::set<data::variable> W = data::detail::make_variable_set(x.variables());
76 apply(result, phi);
77 result = quantifiers_inside_forall(W, result);
78 }
79
80 template <class T>
81 void apply(T& result, const exists& x)
82 {
83 pbes_expression const& phi = x.body();
84 std::set<data::variable> W = data::detail::make_variable_set(x.variables());
85 apply(result, phi);
86 result = quantifiers_inside_exists(W, result);
87 }
88};
89
90struct quantifiers_inside_forall_builder: public data_expression_builder<quantifiers_inside_forall_builder>
91{
93 using super::apply;
94
95 const std::set<data::variable>& V;
96
97 explicit quantifiers_inside_forall_builder(const std::set<data::variable>& V_)
98 : V(V_)
99 {}
100
102 {
103 return vars.empty() ? body : forall(vars, body);
104 }
105
106 // default case
107 template <typename T>
109 {
111 std::set<data::variable> W = set_intersection(V, find_free_variables(x));
112 return make_forall_(data::variable_list(W.begin(), W.end()), x);
113 }
114
115 template <class T>
116 void apply(T& result, const forall& x)
117 {
119 std::set<data::variable> W = data::detail::make_variable_set(x.variables());
120 result = quantifiers_inside_forall(set_union(V, W), x.body());
121 }
122
123 template <class T>
124 void apply(T& result, const not_& x)
125 {
126 const auto& phi = x.operand();
127 result = not_(quantifiers_inside_exists(V, phi));
128 }
129
130 template <class T>
131 void apply(T& result, const and_& x)
132 {
133 const pbes_expression& phi = x.left();
134 const pbes_expression& psi = x.right();
136 }
137
138 template <class T>
139 void apply(T& result, const or_& x)
140 {
144
145 std::vector<pbes_expression> X;
146 utilities::detail::split(x, std::back_inserter(X), tr::is_or, tr::left, tr::right);
147 const auto [Phi, Psi] = compute_Phi_Psi(X, V, tr::or_, tr::false_());
148 if (is_false(Psi))
149 {
151 return;
152 }
153 std::set<data::variable> vars_Phi = find_free_variables(Phi);
154 std::set<data::variable> vars_Psi = find_free_variables(Psi);
155 optimized_or(result,
156 quantifiers_inside_forall(set_difference(set_intersection(V, vars_Phi), vars_Psi), Phi),
157 quantifiers_inside_forall(set_difference(set_intersection(V, vars_Psi), vars_Phi), Psi));
159 result);
160 }
161
162 template <class T>
163 void apply(T& result, const imp& x)
164 {
165 result = quantifiers_inside_forall(V, or_(not_(x.left()), x.right()));
166 }
167
168 template <class T>
170 {
171 result = apply_default(x);
172 }
173
174 template <class T>
175 void apply(T& result, const exists& x)
176 {
177 result = apply_default(x);
178 }
179
180 template <class T>
181 void apply(T& result, const data::data_expression& x)
182 {
184 }
185};
186
187struct quantifiers_inside_exists_builder: public pbes_expression_builder<quantifiers_inside_exists_builder>
188{
190 using super::apply;
191
192 const std::set<data::variable>& V;
193
194 explicit quantifiers_inside_exists_builder(const std::set<data::variable>& V_)
195 : V(V_)
196 {}
197
199 {
200 return vars.empty() ? body : exists(vars, body);
201 }
202
203 // default case
204 template <typename T>
206 {
208 std::set<data::variable> W = set_intersection(V, find_free_variables(x));
209 return make_exists_(data::variable_list(W.begin(), W.end()), x);
210 }
211
212 template <class T>
213 void apply(T& result, const exists& x)
214 {
216 std::set<data::variable> W = data::detail::make_variable_set(x.variables());
217 result = quantifiers_inside_exists(set_union(V, W), x.body());
218 }
219
220 template <class T>
221 void apply(T& result, const not_& x)
222 {
223 const auto& phi = x.operand();
224 result = not_(quantifiers_inside_forall(V, phi));
225 }
226
227 template <class T>
228 void apply(T& result, const or_& x)
229 {
230 const pbes_expression& phi = x.left();
231 const pbes_expression& psi = x.right();
233 }
234
235 template <class T>
236 void apply(T& result, const and_& x)
237 {
241
242 std::vector<pbes_expression> X;
243 utilities::detail::split(x, std::back_inserter(X), tr::is_and, tr::left, tr::right);
244 const auto [Phi, Psi] = compute_Phi_Psi(X, V, tr::and_, tr::true_());
245 if (is_true(Psi))
246 {
248 return;
249 }
250 std::set<data::variable> vars_Phi = find_free_variables(Phi);
251 std::set<data::variable> vars_Psi = find_free_variables(Psi);
252 optimized_and(result,
253 quantifiers_inside_exists(set_difference(set_intersection(V, vars_Phi), vars_Psi), Phi),
254 quantifiers_inside_exists(set_difference(set_intersection(V, vars_Psi), vars_Phi), Psi));
256 result);
257 }
258
259 template <class T>
260 void apply(T& result, const imp& x)
261 {
262 result = quantifiers_inside_exists(V, and_(not_(x.left()), x.right()));
263 }
264
265 template <class T>
267 {
268 result = apply_default(x);
269 }
270
271 template <class T>
272 void apply(T& result, const forall& x)
273 {
274 result = apply_default(x);
275 }
276
277 template <class T>
278 void apply(T& result, const data::data_expression& x)
279 {
281 }
282};
283
284inline
286{
288 pbes_expression result;
289 f.apply(result, x);
290 return result;
291}
292
293inline
294pbes_expression quantifiers_inside_forall(const std::set<data::variable>& variables, const pbes_expression& x)
295{
297 pbes_expression result;
298 f.apply(result, x);
299 return result;
300}
301
302inline
303pbes_expression quantifiers_inside_exists(const std::set<data::variable>& variables, const pbes_expression& x)
304{
306 pbes_expression result;
307 f.apply(result, x);
308 return result;
309}
310
311} // namespace detail
312
315{
316 public:
319
322
327 {
329 }
330};
331
332} // namespace pbes_system
333
334} // namespace mcrl2
335
336#endif // MCRL2_PBES_REWRITERS_QUANTIFIERS_INSIDE_REWRITER_H
bool empty() const
Returns true if the list's size is 0.
Definition aterm_list.h:268
\brief A data variable
Definition variable.h:28
\brief The and operator for pbes expressions
const pbes_expression & left() const
const pbes_expression & right() const
\brief The existential quantification operator for pbes expressions
const data::variable_list & variables() const
const pbes_expression & body() const
\brief The universal quantification operator for pbes expressions
const pbes_expression & body() const
const data::variable_list & variables() const
\brief The implication operator for pbes expressions
const pbes_expression & left() const
const pbes_expression & right() const
\brief The not operator for pbes expressions
const pbes_expression & operand() const
\brief The or operator for pbes expressions
const pbes_expression & left() const
const pbes_expression & right() const
\brief A propositional variable instantiation
A rewriter that pushes quantifiers inside in a PBES expression.
pbes_expression operator()(const pbes_expression &x) const
Rewrites a pbes expression.
data_expression quantifiers_inside_forall(const std::set< variable > &variables, const data_expression &x)
data_expression quantifiers_inside_exists(const std::set< variable > &variables, const data_expression &x)
variable_list make_variable_list(const std::set< variable > &x)
std::set< variable > make_variable_set(const variable_list &x)
pbes_expression quantifiers_inside_forall(const std::set< data::variable > &variables, const pbes_expression &x)
pbes_expression quantifiers_inside_exists(const std::set< data::variable > &variables, const pbes_expression &x)
std::tuple< pbes_expression, pbes_expression > compute_Phi_Psi(const std::vector< pbes_expression > &X, const std::set< data::variable > &V, BinaryOperation op, pbes_expression empty_sequence_result)
pbes_expression quantifiers_inside(const pbes_expression &x)
std::set< data::variable > find_free_variables(const pbes_expression &x, const data::variable_list &bound_variables=data::variable_list(), bool search_propositional_variables=true)
void make_and_(atermpp::aterm &t, const ARGUMENTS &... args)
vertex_set set_union(const vertex_set &V, const vertex_set &W)
bool is_false(const pbes_expression &t)
Test for the value false.
void optimized_or(pbes_expression &result, const pbes_expression &p, const pbes_expression &q)
Make a disjunction.
void optimized_and(pbes_expression &result, const pbes_expression &p, const pbes_expression &q)
Make a conjunction.
vertex_set set_intersection(const VertexSet &V, const vertex_set &W)
bool is_true(const pbes_expression &t)
Test for the value true.
T join(FwdIt first, FwdIt last, BinaryOperation op, T empty_sequence_result)
Given a sequence [t1, t2, ..., tn] of elements of type T, returns op(t1, op(t2, .....
Definition join.h:55
std::set< T > set_union(const std::set< T > &x, const std::set< T > &y)
Returns the union of two sets.
void split(const T &t, OutputIterator i, MatchFunction match, AccessorFunction1 lhs, AccessorFunction2 rhs)
Splits a binary tree T into a sequence, and writes the result to the output range given by an output ...
Definition join.h:34
std::set< T > set_intersection(const std::set< T > &x, const std::set< T > &y)
Returns the intersection of two sets.
std::set< T > set_difference(const std::set< T > &x, const std::set< T > &y)
Returns the difference of two sets.
A class that takes a linear process specification and checks all tau-summands of that LPS for conflue...
Definition indexed_set.h:72