cprover
union_find_replace.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: util
4 
5 Author: Romain Brenguier, romain.brenguier@diffblue.com
6 
7 \*******************************************************************/
8 
9 #include "union_find_replace.h"
10 
19 {
20  const exprt &lhs_root = find(a);
21  const exprt &rhs_root = find(b);
22  if(lhs_root != rhs_root)
23  map[lhs_root] = rhs_root;
24  return rhs_root;
25 }
26 
32 {
33  bool unchanged = ::replace_expr(map, expr);
34  while(!unchanged && !::replace_expr(map, expr))
35  continue;
36  return unchanged;
37 }
38 
43 {
44  replace_expr(expr);
45  return expr;
46 }
47 
50 std::vector<std::pair<exprt, exprt>> union_find_replacet::to_vector() const
51 {
52  std::vector<std::pair<exprt, exprt>> equations;
53  for(const auto &pair : map)
54  equations.emplace_back(pair.first, find(pair.second));
55  return equations;
56 }
bool replace_expr(exprt &expr) const
Replace subexpressions of expr by a canonical element of the set they belong to.
exprt make_union(const exprt &a, const exprt &b)
Keeps a map of symbols to expressions, such as none of the mapped values exist as a key...
exprt find(exprt expr) const
Base class for all expressions.
Definition: expr.h:42
std::vector< std::pair< exprt, exprt > > to_vector() const