mCRL2
Loading...
Searching...
No Matches
find_equalities.h
Go to the documentation of this file.
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//
11
12#ifndef MCRL2_DATA_FIND_EQUALITIES_H
13#define MCRL2_DATA_FIND_EQUALITIES_H
14
16#include "mcrl2/data/find.h"
17
18namespace mcrl2 {
19
20namespace data {
21
22namespace detail {
23
25{
26 std::map<variable, std::set<data_expression> > assignments;
27 bool is_top = false;
28
29 std::set<data_expression>& operator[](const variable& var)
30 {
31 return assignments[var];
32 }
36 {
37 if (other.is_top)
38 {
39 return *this;
40 }
41 if (is_top)
42 {
43 *this = other;
44 return *this;
45 }
46
47 auto i1 = assignments.begin();
48 auto i2 = other.assignments.begin();
49 while (i1 != assignments.end())
50 {
51 if (i2 == other.assignments.end())
52 {
53 assignments.erase(i1, assignments.end());
54 break;
55 }
56 if (i1->first > i2->first)
57 {
58 assignments.erase(i1++);
59 }
60 else if (i2->first > i1->first)
61 {
62 ++i2;
63 }
64 else
65 {
66 i1->second = utilities::detail::set_intersection(i1->second, i2->second);
67 if (i1->second.empty())
68 {
69 assignments.erase(i1++);
70 }
71 else
72 {
73 ++i1;
74 }
75 ++i2;
76 }
77 }
78
79 return *this;
80 }
81
84 {
85 is_top |= other.is_top;
86 for (const auto& [lhs, rhss]: other.assignments)
87 {
88 assignments[lhs].insert(rhss.begin(), rhss.end());
89 }
90 return *this;
91 }
92
93 bool non_empty_intersection(const data::variable_list& variables, const std::set<data::variable>& V) const
94 {
96 return std::any_of(variables.begin(), variables.end(), [&](const variable& v) { return contains(V,v); });
97 }
98
99 bool must_delete(const data::variable_list& variables, const data::variable& lhs, std::set<data::data_expression>& rhs) const
100 {
103 if (contains(variables, lhs))
104 {
105 return true;
106 }
107 remove_if(rhs, [&](const data::data_expression& x) { return non_empty_intersection(variables, data::find_free_variables(x)); });
108 return rhs.empty();
109 }
110
111 void delete_(const data::variable_list& variables)
112 {
114 remove_if(assignments, [&](std::pair<const variable, std::set<data_expression> >& p) { return must_delete(variables, p.first, p.second); });
115 }
116
117 // for each entry b = b', b' = b is added too
118 void close()
119 {
120 for (auto i = assignments.begin(); i != assignments.end(); ++i)
121 {
122 const variable& v = i->first;
123 std::vector<variable> W;
124 for (const data_expression& e: i->second)
125 {
126 if (is_variable(e))
127 {
128 W.push_back(atermpp::down_cast<variable>(e));
129 }
130 }
131 for (const variable& w: W)
132 {
133 assignments[w].insert(v);
134 }
135 }
136 }
137};
138
140{
143
146 {}
147
150 find_equalities_expression(const variable& lhs, const data_expression& rhs, bool is_equality)
151 {
152 if (is_equality)
153 {
154 equalities[lhs].insert(rhs);
155 if (is_variable(rhs))
156 {
157 equalities[atermpp::down_cast<variable>(rhs)].insert(lhs);
158 }
159 }
160 else
161 {
162 inequalities[lhs].insert(rhs);
163 if (is_variable(rhs))
164 {
165 inequalities[atermpp::down_cast<variable>(rhs)].insert(lhs);
166 }
167 }
168 }
169
172 {
173 assert(lhs.sort() == sort_bool::bool_());
174 equalities[lhs].insert(sort_bool::true_());
175 inequalities[lhs].insert(sort_bool::false_());
176 }
177
180 {
181 equalities.is_top = !ineq_top;
182 inequalities.is_top = ineq_top;
183 }
184
185 void swap()
186 {
188 }
189
191 {
194 }
195
197 {
200 }
201
202 void delete_(const data::variable_list& variables)
203 {
204 equalities.delete_(variables);
205 inequalities.delete_(variables);
206 }
207
208 void close()
209 {
212 }
213};
214
215inline
216std::ostream& operator<<(std::ostream& out, const find_equalities_expression& x)
217{
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
238template <template <class> class Traverser, class Derived>
239struct 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 Derived& derived()
249 {
250 return static_cast<Derived&>(*this);
251 }
252
254 {
255 expression_stack.push_back(x);
256 }
257
259 {
260 assert(!expression_stack.empty());
261 return expression_stack.back();
262 }
263
265 {
266 assert(!expression_stack.empty());
267 return expression_stack.back();
268 }
269
271 {
272 assert(expression_stack.size() >= 2);
273 return expression_stack[expression_stack.size() - 2];
274 }
275
277 {
278 assert(expression_stack.size() >= 2);
279 return expression_stack[expression_stack.size() - 2];
280 }
281
283 {
284 assert(expression_stack.size() >= 3);
285 return expression_stack[expression_stack.size() - 3];
286 }
287
289 {
290 assert(expression_stack.size() >= 3);
291 return expression_stack[expression_stack.size() - 3];
292 }
293
295 {
296 assert(!expression_stack.empty());
298 expression_stack.pop_back();
299 return result;
300 }
301
302
304 {
306 {
307 const data_expression& left = binary_left(x);
308 const data_expression& right = binary_right(x);
309 if (is_variable(left) && !search_free_variable(right, atermpp::down_cast<variable>(left)))
310 {
311 push(find_equalities_expression(atermpp::down_cast<variable>(left), right, true));
312 }
313 else if (is_variable(right) && !search_free_variable(left, atermpp::down_cast<variable>(right)))
314 {
315 push(find_equalities_expression(atermpp::down_cast<variable>(right), left, true));
316 }
317 else
318 {
320 }
321 }
323 {
324 const data_expression& left = binary_left(x);
325 const data_expression& right = binary_right(x);
326 if (is_variable(left) && !search_free_variable(right, atermpp::down_cast<variable>(left)))
327 {
328 push(find_equalities_expression(atermpp::down_cast<variable>(left), right, false));
329 }
330 else if (is_variable(right) && !search_free_variable(left, atermpp::down_cast<variable>(right)))
331 {
332 push(find_equalities_expression(atermpp::down_cast<variable>(right), left, false));
333 }
334 else
335 {
337 }
338 }
340 {
341 derived().apply(sort_bool::arg(x));
342 top().swap();
343 }
345 {
346 derived().apply(binary_left(x));
347 derived().apply(binary_right(x));
349 const find_equalities_expression& right = top();
350 left.join_and(right);
351 pop();
352 }
354 {
355 derived().apply(binary_left(x));
356 derived().apply(binary_right(x));
358 const find_equalities_expression& right = top();
359 left.join_or(right);
360 pop();
361 }
363 {
364 derived().apply(binary_left(x));
365 derived().apply(binary_right(x));
367 const find_equalities_expression& right = top();
368 left.swap();
369 left.join_or(right);
370 pop();
371 }
372 else if (is_if_application(x))
373 {
374 derived().apply(x[1]);
375 derived().apply(x[2]);
376 derived().apply(x[0]);
379 const find_equalities_expression& cond = top();
380
381 then.equalities.union_(cond.equalities);
382 else_.equalities.union_(cond.inequalities);
383 then.equalities.intersect(else_.equalities);
384
385 then.inequalities.union_(cond.equalities);
386 else_.inequalities.union_(cond.inequalities);
388
389 pop();
390 pop();
391 }
392 else
393 {
394 mCRL2log(log::trace) << "ignoring " << x << std::endl;
396 }
397 }
398
399 void leave(const data::variable& x)
400 {
401 if (sort_bool::is_bool(x.sort()))
402 {
404 }
405 else
406 {
408 }
409 }
410
412 {
413 top().delete_(x.variables());
414 }
415
417 {
419 {
421 }
423 {
425 }
426 else
427 {
429 }
430 }
431
433 {
434 throw mcrl2::runtime_error("not implemented yet!");
435 }
436};
437
438struct find_equalities_traverser_inst: public find_equalities_traverser<data::data_expression_traverser, find_equalities_traverser_inst>
439{
441
442 using super::enter;
443 using super::leave;
444 using super::apply;
445};
446
447} // namespace detail
448
449inline
450std::map<variable, std::set<data_expression> > find_equalities(const data_expression& x)
451{
453 f.apply(x);
454 assert(f.expression_stack.size() == 1);
455 f.top().close();
456 return f.top().equalities.assignments;
457}
458
459inline
460std::map<variable, std::set<data_expression> > find_inequalities(const data_expression& x)
461{
463 f.apply(x);
464 assert(f.expression_stack.size() == 1);
465 f.top().close();
466 return f.top().inequalities.assignments;
467}
468
469inline
470std::string print_equalities(const std::map<variable, std::set<data_expression> >& equalities)
471{
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
484inline
485std::string print_inequalities(const std::map<variable, std::set<data_expression> >& inequalities)
486{
488 std::vector<data_expression> result;
489 for (const auto& [lhs, rhss]: inequalities)
490 {
491 for (const data_expression& rhs: rhss)
492 {
493 result.push_back(not_equal_to(lhs, rhs));
494 }
495 }
496 return print_set(result);
497}
498
499} // namespace data
500
501} // namespace mcrl2
502
503#endif // MCRL2_DATA_FIND_EQUALITIES_H
const_iterator end() const
Returns a const_iterator pointing to the end of the term_list.
Definition aterm_list.h:282
const_iterator begin() const
Returns a const_iterator pointing to the beginning of the term_list.
Definition aterm_list.h:275
void swap(unprotected_aterm_core &t) noexcept
Swaps this term with its argument.
Definition aterm_core.h:152
An abstraction expression.
Definition abstraction.h:26
const variable_list & variables() const
Definition abstraction.h:63
An application of a data expression to a number of arguments.
\brief A function symbol
\brief A data variable
Definition variable.h:28
const sort_expression & sort() const
Definition variable.h:43
\brief A where expression
Standard exception class for reporting runtime errors.
Definition exception.h:27
add your file description here.
Search functions of the data library.
#define mCRL2log(LEVEL)
mCRL2log(LEVEL) provides the stream used to log.
Definition logger.h:395
std::string print_set(const Container &v, const std::string &message="", bool print_index=false, bool boundary_spaces=true)
Creates a string representation of a container.
std::ostream & operator<<(std::ostream &os, smt_solver_type s)
standard conversion from solvert type to stream
Definition solver_type.h:71
bool is_false_function_symbol(const atermpp::aterm &e)
Recogniser for function false.
Definition bool.h:119
const data_expression & arg(const data_expression &e)
Function for projecting out argument. arg from an application.
Definition bool.h:469
bool is_or_application(const atermpp::aterm &e)
Recogniser for application of ||.
Definition bool.h:345
bool is_bool(const sort_expression &e)
Recogniser for sort expression Bool.
Definition bool.h:54
const basic_sort & bool_()
Constructor for sort expression Bool.
Definition bool.h:44
bool is_implies_application(const atermpp::aterm &e)
Recogniser for application of =>.
Definition bool.h:409
const function_symbol & false_()
Constructor for function symbol false.
Definition bool.h:109
bool is_and_application(const atermpp::aterm &e)
Recogniser for application of &&.
Definition bool.h:281
bool is_true_function_symbol(const atermpp::aterm &e)
Recogniser for function true.
Definition bool.h:87
bool is_not_application(const atermpp::aterm &e)
Recogniser for application of !.
Definition bool.h:217
const function_symbol & true_()
Constructor for function symbol true.
Definition bool.h:77
const data_expression & binary_right(const application &x)
function_symbol not_equal_to(const sort_expression &s)
Constructor for function symbol !=.
Definition standard.h:163
bool is_if_application(const DataExpression &e)
Recogniser for application of if.
Definition standard.h:232
bool is_not_equal_to_application(const DataExpression &e)
Recogniser for application of !=.
Definition standard.h:192
bool search_free_variable(const T &x, const variable &v)
Returns true if the term has a given free variable as subterm.
Definition find.h:456
const data_expression & binary_left(const application &x)
std::map< variable, std::set< data_expression > > find_inequalities(const data_expression &x)
std::map< variable, std::set< data_expression > > find_equalities(const data_expression &x)
std::set< data::variable > find_free_variables(const data::data_expression &x)
Definition data.cpp:99
std::string print_equalities(const std::map< variable, std::set< data_expression > > &equalities)
function_symbol equal_to(const sort_expression &s)
Constructor for function symbol ==.
Definition standard.h:126
std::string print_inequalities(const std::map< variable, std::set< data_expression > > &inequalities)
bool is_equal_to_application(const DataExpression &e)
Recogniser for application of ==.
Definition standard.h:155
bool is_variable(const atermpp::aterm &x)
Returns true if the term t is a variable.
bool contains(const atermpp::indexed_set< Key, ThreadSafe, Hash, Equals, Allocator, KeyTable > &c, const typename atermpp::indexed_set< Key, ThreadSafe, Hash, Equals, Allocator, KeyTable >::key_type &v, const std::size_t thread_index=0)
Definition indexed_set.h:86
void remove_if(ContainerT &items, const PredicateT &predicate)
std::set< T > set_intersection(const std::set< T > &x, const std::set< T > &y)
Returns the intersection 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
void swap(atermpp::unprotected_aterm_core &t1, atermpp::unprotected_aterm_core &t2) noexcept
Swaps two aterms.
Definition aterm.h:462
std::set< data_expression > & operator[](const variable &var)
bool non_empty_intersection(const data::variable_list &variables, const std::set< data::variable > &V) const
bool must_delete(const data::variable_list &variables, const data::variable &lhs, std::set< data::data_expression > &rhs) const
std::map< variable, std::set< data_expression > > assignments
equality_set_with_top & union_(const equality_set_with_top &other)
Computes union, modifying this set.
void delete_(const data::variable_list &variables)
equality_set_with_top & intersect(const equality_set_with_top &other)
Computes intersection, modifying this set.
find_equalities_expression(bool ineq_top)
Creates (empty,top) if ineq_top is true and (top,empty) otherwise.
void join_or(const find_equalities_expression &other)
find_equalities_expression(const variable &lhs, const data_expression &rhs, bool is_equality)
Creates ({lhs == rhs}, empty) if is_equality is true, and (empty, {lhs == rhs}) otherwise.
void delete_(const data::variable_list &variables)
find_equalities_expression(const variable &lhs)
Creates ({lhs == true}, {lhs != false})
void join_and(const find_equalities_expression &other)
find_equalities_traverser< data::data_expression_traverser, find_equalities_traverser_inst > super
void push(const find_equalities_expression &x)
const find_equalities_expression & two_below_top() const
const find_equalities_expression & top() const
const find_equalities_expression & below_top() const
std::vector< find_equalities_expression > expression_stack
find_equalities_expression & two_below_top()
void leave(const data::function_symbol &f)