Line data Source code
1 : // Author(s): Wieger Wesselink, Thomas Neele
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 : //
9 : /// \file mcrl2/data/find_equalities.h
10 : /// \brief add your file description here.
11 :
12 : #ifndef MCRL2_DATA_FIND_EQUALITIES_H
13 : #define MCRL2_DATA_FIND_EQUALITIES_H
14 :
15 : #include "mcrl2/core/detail/print_utility.h"
16 : #include "mcrl2/data/find.h"
17 :
18 : namespace mcrl2 {
19 :
20 : namespace data {
21 :
22 : namespace detail {
23 :
24 : struct equality_set_with_top
25 : {
26 : std::map<variable, std::set<data_expression> > assignments;
27 : bool is_top = false;
28 :
29 60709 : std::set<data_expression>& operator[](const variable& var)
30 : {
31 60709 : return assignments[var];
32 : }
33 :
34 : /// @brief Computes intersection, modifying this set
35 42088 : equality_set_with_top& intersect(const equality_set_with_top& other)
36 : {
37 42088 : if (other.is_top)
38 : {
39 14 : return *this;
40 : }
41 42074 : if (is_top)
42 : {
43 1 : *this = other;
44 1 : return *this;
45 : }
46 :
47 42073 : auto i1 = assignments.begin();
48 42073 : auto i2 = other.assignments.begin();
49 50978 : while (i1 != assignments.end())
50 : {
51 9053 : if (i2 == other.assignments.end())
52 : {
53 148 : assignments.erase(i1, assignments.end());
54 148 : break;
55 : }
56 8905 : if (i1->first > i2->first)
57 : {
58 29 : assignments.erase(i1++);
59 : }
60 8876 : else if (i2->first > i1->first)
61 : {
62 56 : ++i2;
63 : }
64 : else
65 : {
66 8820 : i1->second = utilities::detail::set_intersection(i1->second, i2->second);
67 8820 : if (i1->second.empty())
68 : {
69 8820 : assignments.erase(i1++);
70 : }
71 : else
72 : {
73 0 : ++i1;
74 : }
75 8820 : ++i2;
76 : }
77 : }
78 :
79 42073 : return *this;
80 : }
81 :
82 : /// @brief Computes union, modifying this set
83 47928 : equality_set_with_top& union_(const equality_set_with_top& other)
84 : {
85 47928 : is_top |= other.is_top;
86 112332 : for (const auto& [lhs, rhss]: other.assignments)
87 : {
88 64404 : assignments[lhs].insert(rhss.begin(), rhss.end());
89 : }
90 47928 : return *this;
91 : }
92 :
93 2 : bool non_empty_intersection(const data::variable_list& variables, const std::set<data::variable>& V) const
94 : {
95 : using utilities::detail::contains;
96 4 : return std::any_of(variables.begin(), variables.end(), [&](const variable& v) { return contains(V,v); });
97 : }
98 :
99 4 : bool must_delete(const data::variable_list& variables, const data::variable& lhs, std::set<data::data_expression>& rhs) const
100 : {
101 : using utilities::detail::contains;
102 : using utilities::detail::remove_if;
103 4 : if (contains(variables, lhs))
104 : {
105 2 : return true;
106 : }
107 4 : remove_if(rhs, [&](const data::data_expression& x) { return non_empty_intersection(variables, data::find_free_variables(x)); });
108 2 : return rhs.empty();
109 : }
110 :
111 52 : void delete_(const data::variable_list& variables)
112 : {
113 : using utilities::detail::remove_if;
114 56 : remove_if(assignments, [&](std::pair<const variable, std::set<data_expression> >& p) { return must_delete(variables, p.first, p.second); });
115 52 : }
116 :
117 : // for each entry b = b', b' = b is added too
118 29828 : void close()
119 : {
120 74318 : for (auto i = assignments.begin(); i != assignments.end(); ++i)
121 : {
122 44490 : const variable& v = i->first;
123 44490 : std::vector<variable> W;
124 89004 : for (const data_expression& e: i->second)
125 : {
126 44514 : if (is_variable(e))
127 : {
128 3142 : W.push_back(atermpp::down_cast<variable>(e));
129 : }
130 : }
131 47632 : for (const variable& w: W)
132 : {
133 3142 : assignments[w].insert(v);
134 : }
135 44490 : }
136 29828 : }
137 : };
138 :
139 : struct find_equalities_expression
140 : {
141 : equality_set_with_top equalities;
142 : equality_set_with_top inequalities;
143 :
144 : /// @brief Creates (empty,empty)
145 1064 : find_equalities_expression()
146 1064 : {}
147 :
148 : /// @brief Creates ({lhs == rhs}, empty) if is_equality is true, and (empty, {lhs == rhs}) otherwise
149 : /// @param is_equality Indicates whether to construct an equality or inequality
150 51788 : find_equalities_expression(const variable& lhs, const data_expression& rhs, bool is_equality)
151 51788 : {
152 51788 : if (is_equality)
153 : {
154 51783 : equalities[lhs].insert(rhs);
155 51783 : if (is_variable(rhs))
156 : {
157 3063 : equalities[atermpp::down_cast<variable>(rhs)].insert(lhs);
158 : }
159 : }
160 : else
161 : {
162 5 : inequalities[lhs].insert(rhs);
163 5 : if (is_variable(rhs))
164 : {
165 2 : inequalities[atermpp::down_cast<variable>(rhs)].insert(lhs);
166 : }
167 : }
168 51788 : }
169 :
170 : /// @brief Creates ({lhs == true}, {lhs != false})
171 2928 : find_equalities_expression(const variable& lhs)
172 2928 : {
173 2928 : assert(lhs.sort() == sort_bool::bool_());
174 2928 : equalities[lhs].insert(sort_bool::true_());
175 2928 : inequalities[lhs].insert(sort_bool::false_());
176 2928 : }
177 :
178 : /// @brief Creates (empty,top) if ineq_top is true and (top,empty) otherwise
179 1222 : find_equalities_expression(bool ineq_top)
180 1222 : {
181 1222 : equalities.is_top = !ineq_top;
182 1222 : inequalities.is_top = ineq_top;
183 1222 : }
184 :
185 2009 : void swap()
186 : {
187 2009 : std::swap(equalities, inequalities);
188 2009 : }
189 :
190 36086 : void join_and(const find_equalities_expression& other)
191 : {
192 36086 : equalities.union_(other.equalities);
193 36086 : inequalities.intersect(other.inequalities);
194 36086 : }
195 :
196 162 : void join_or(const find_equalities_expression& other)
197 : {
198 162 : equalities.intersect(other.equalities);
199 162 : inequalities.union_(other.inequalities);
200 162 : }
201 :
202 26 : void delete_(const data::variable_list& variables)
203 : {
204 26 : equalities.delete_(variables);
205 26 : inequalities.delete_(variables);
206 26 : }
207 :
208 14914 : void close()
209 : {
210 14914 : equalities.close();
211 14914 : inequalities.close();
212 14914 : }
213 : };
214 :
215 : inline
216 : std::ostream& operator<<(std::ostream& out, const find_equalities_expression& x)
217 : {
218 : using core::detail::print_set;
219 : std::vector<data_expression> result;
220 : for (const auto& [lhs, rhss]: x.equalities.assignments)
221 : {
222 : for (const data_expression& rhs: rhss)
223 : {
224 : result.push_back(equal_to(lhs, rhs));
225 : }
226 : }
227 : for (const auto& [lhs, rhss]: x.inequalities.assignments)
228 : {
229 : for (const data_expression& rhs: rhss)
230 : {
231 : result.push_back(not_equal_to(lhs, rhs));
232 : }
233 : }
234 : out << print_set(result);
235 : return out;
236 : }
237 :
238 : template <template <class> class Traverser, class Derived>
239 : struct find_equalities_traverser: public Traverser<Derived>
240 : {
241 : typedef Traverser<Derived> super;
242 : using super::enter;
243 : using super::leave;
244 : using super::apply;
245 :
246 : std::vector<find_equalities_expression> expression_stack;
247 :
248 82894 : Derived& derived()
249 : {
250 82894 : return static_cast<Derived&>(*this);
251 : }
252 :
253 57002 : void push(const find_equalities_expression& x)
254 : {
255 57002 : expression_stack.push_back(x);
256 57002 : }
257 :
258 113116 : find_equalities_expression& top()
259 : {
260 113116 : assert(!expression_stack.empty());
261 113116 : return expression_stack.back();
262 : }
263 :
264 : const find_equalities_expression& top() const
265 : {
266 : assert(!expression_stack.empty());
267 : return expression_stack.back();
268 : }
269 :
270 39168 : find_equalities_expression& below_top()
271 : {
272 39168 : assert(expression_stack.size() >= 2);
273 39168 : return expression_stack[expression_stack.size() - 2];
274 : }
275 :
276 : const find_equalities_expression& below_top() const
277 : {
278 : assert(expression_stack.size() >= 2);
279 : return expression_stack[expression_stack.size() - 2];
280 : }
281 :
282 2920 : find_equalities_expression& two_below_top()
283 : {
284 2920 : assert(expression_stack.size() >= 3);
285 2920 : return expression_stack[expression_stack.size() - 3];
286 : }
287 :
288 : const find_equalities_expression& two_below_top() const
289 : {
290 : assert(expression_stack.size() >= 3);
291 : return expression_stack[expression_stack.size() - 3];
292 : }
293 :
294 42088 : find_equalities_expression pop()
295 : {
296 42088 : assert(!expression_stack.empty());
297 42088 : find_equalities_expression result = top();
298 42088 : expression_stack.pop_back();
299 42088 : return result;
300 : }
301 :
302 :
303 93698 : void apply(const data::application& x)
304 : {
305 93698 : if (data::is_equal_to_application(x))
306 : {
307 52160 : const data_expression& left = binary_left(x);
308 52160 : const data_expression& right = binary_right(x);
309 52160 : if (is_variable(left) && !search_free_variable(right, atermpp::down_cast<variable>(left)))
310 : {
311 49894 : push(find_equalities_expression(atermpp::down_cast<variable>(left), right, true));
312 : }
313 2266 : else if (is_variable(right) && !search_free_variable(left, atermpp::down_cast<variable>(right)))
314 : {
315 1889 : push(find_equalities_expression(atermpp::down_cast<variable>(right), left, true));
316 : }
317 : else
318 : {
319 377 : push(find_equalities_expression());
320 : }
321 : }
322 41538 : else if (data::is_not_equal_to_application(x))
323 : {
324 7 : const data_expression& left = binary_left(x);
325 7 : const data_expression& right = binary_right(x);
326 7 : if (is_variable(left) && !search_free_variable(right, atermpp::down_cast<variable>(left)))
327 : {
328 5 : push(find_equalities_expression(atermpp::down_cast<variable>(left), right, false));
329 : }
330 2 : else if (is_variable(right) && !search_free_variable(left, atermpp::down_cast<variable>(right)))
331 : {
332 0 : push(find_equalities_expression(atermpp::down_cast<variable>(right), left, false));
333 : }
334 : else
335 : {
336 2 : push(find_equalities_expression());
337 : }
338 : }
339 41531 : else if (sort_bool::is_not_application(x))
340 : {
341 2006 : derived().apply(sort_bool::arg(x));
342 2006 : top().swap();
343 : }
344 39525 : else if (sort_bool::is_and_application(x))
345 : {
346 35949 : derived().apply(binary_left(x));
347 35949 : derived().apply(binary_right(x));
348 35949 : find_equalities_expression& left = below_top();
349 35949 : const find_equalities_expression& right = top();
350 35949 : left.join_and(right);
351 35949 : pop();
352 : }
353 3576 : else if (sort_bool::is_or_application(x))
354 : {
355 115 : derived().apply(binary_left(x));
356 115 : derived().apply(binary_right(x));
357 115 : find_equalities_expression& left = below_top();
358 115 : const find_equalities_expression& right = top();
359 115 : left.join_or(right);
360 115 : pop();
361 : }
362 3461 : else if (sort_bool::is_implies_application(x))
363 : {
364 0 : derived().apply(binary_left(x));
365 0 : derived().apply(binary_right(x));
366 0 : find_equalities_expression& left = below_top();
367 0 : const find_equalities_expression& right = top();
368 0 : left.swap();
369 0 : left.join_or(right);
370 0 : pop();
371 : }
372 3461 : else if (is_if_application(x))
373 : {
374 2920 : derived().apply(x[1]);
375 2920 : derived().apply(x[2]);
376 2920 : derived().apply(x[0]);
377 2920 : find_equalities_expression& then = two_below_top();
378 2920 : find_equalities_expression& else_ = below_top();
379 2920 : const find_equalities_expression& cond = top();
380 :
381 2920 : then.equalities.union_(cond.equalities);
382 2920 : else_.equalities.union_(cond.inequalities);
383 2920 : then.equalities.intersect(else_.equalities);
384 :
385 2920 : then.inequalities.union_(cond.equalities);
386 2920 : else_.inequalities.union_(cond.inequalities);
387 2920 : then.inequalities.intersect(else_.inequalities);
388 :
389 2920 : pop();
390 2920 : pop();
391 : }
392 : else
393 : {
394 541 : mCRL2log(log::trace) << "ignoring " << x << std::endl;
395 541 : push(find_equalities_expression());
396 : }
397 93698 : }
398 :
399 2928 : void leave(const data::variable& x)
400 : {
401 2928 : if (sort_bool::is_bool(x.sort()))
402 : {
403 2928 : push(find_equalities_expression(x));
404 : }
405 : else
406 : {
407 0 : push(find_equalities_expression());
408 : }
409 2928 : }
410 :
411 0 : void leave(const data::abstraction& x)
412 : {
413 0 : top().delete_(x.variables());
414 0 : }
415 :
416 1222 : void leave(const data::function_symbol& f)
417 : {
418 1222 : if (sort_bool::is_true_function_symbol(f))
419 : {
420 148 : push(find_equalities_expression(true));
421 : }
422 1074 : else if (sort_bool::is_false_function_symbol(f))
423 : {
424 1074 : push(find_equalities_expression(false));
425 : }
426 : else
427 : {
428 0 : push(find_equalities_expression());
429 : }
430 1222 : }
431 :
432 0 : void leave(const data::where_clause&)
433 : {
434 0 : throw mcrl2::runtime_error("not implemented yet!");
435 : }
436 : };
437 :
438 : struct find_equalities_traverser_inst: public find_equalities_traverser<data::data_expression_traverser, find_equalities_traverser_inst>
439 : {
440 : typedef find_equalities_traverser<data::data_expression_traverser, find_equalities_traverser_inst> super;
441 :
442 : using super::enter;
443 : using super::leave;
444 : using super::apply;
445 : };
446 :
447 : } // namespace detail
448 :
449 : inline
450 14668 : std::map<variable, std::set<data_expression> > find_equalities(const data_expression& x)
451 : {
452 14668 : detail::find_equalities_traverser_inst f;
453 14668 : f.apply(x);
454 14668 : assert(f.expression_stack.size() == 1);
455 14668 : f.top().close();
456 29336 : return f.top().equalities.assignments;
457 14668 : }
458 :
459 : inline
460 1 : std::map<variable, std::set<data_expression> > find_inequalities(const data_expression& x)
461 : {
462 1 : detail::find_equalities_traverser_inst f;
463 1 : f.apply(x);
464 1 : assert(f.expression_stack.size() == 1);
465 1 : f.top().close();
466 2 : return f.top().inequalities.assignments;
467 1 : }
468 :
469 : inline
470 : std::string print_equalities(const std::map<variable, std::set<data_expression> >& equalities)
471 : {
472 : using core::detail::print_set;
473 : std::vector<data_expression> result;
474 : for (const auto& [lhs, rhss]: equalities)
475 : {
476 : for (const data_expression& rhs: rhss)
477 : {
478 : result.push_back(equal_to(lhs, rhs));
479 : }
480 : }
481 : return print_set(result);
482 : }
483 :
484 : inline
485 0 : std::string print_inequalities(const std::map<variable, std::set<data_expression> >& inequalities)
486 : {
487 : using core::detail::print_set;
488 0 : std::vector<data_expression> result;
489 0 : for (const auto& [lhs, rhss]: inequalities)
490 : {
491 0 : for (const data_expression& rhs: rhss)
492 : {
493 0 : result.push_back(not_equal_to(lhs, rhs));
494 : }
495 : }
496 0 : return print_set(result);
497 0 : }
498 :
499 : } // namespace data
500 :
501 : } // namespace mcrl2
502 :
503 : #endif // MCRL2_DATA_FIND_EQUALITIES_H
|
