cprover
union_find.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 
10 #ifndef CPROVER_UTIL_UNION_FIND_H
11 #define CPROVER_UTIL_UNION_FIND_H
12 
13 #include <cassert>
14 #include <vector>
15 
16 #include "numbering.h"
17 
18 // Standard union find with weighting and path compression.
19 // See http://www.cs.princeton.edu/~rs/AlgsDS07/01UnionFind.pdf
20 
21 // NOLINTNEXTLINE(readability/identifiers)
23 {
24 public:
25  // NOLINTNEXTLINE(readability/identifiers)
26  typedef std::size_t size_type;
27 
28 protected:
29  struct nodet
30  {
31  size_type count; // set size
32  size_type parent;
33 
34  // constructs a root node
35  explicit nodet(size_type index):count(1), parent(index)
36  {
37  }
38  };
39 
40  // This is mutable to allow path compression in find().
41  mutable std::vector<nodet> nodes;
42 
43 public:
44  // merge the sets 'a' and 'b'
45  void make_union(size_type a, size_type b);
46 
47  // find the root of the set 'a' belongs to
48  size_type find(size_type a) const;
49 
50  // Makes 'this' the union-find with the following:
51  // any union in 'this' will be present in both source sets,
52  // i.e., this is the strongest implication of the two
53  // data structures.
54  void intersection(const unsigned_union_find &other);
55 
56  // remove from any sets
57  void isolate(size_type a);
58 
60  {
61  other.nodes.swap(nodes);
62  }
63 
64  void resize(size_type size)
65  {
66  // We only enlarge. Shrinking is yet to be implemented.
67  assert(nodes.size()<=size);
68  nodes.reserve(size);
69  while(nodes.size()<size)
70  nodes.push_back(nodet(nodes.size()));
71  }
72 
73  void clear()
74  {
75  nodes.clear();
76  }
77 
78  // is 'a' a root?
79  bool is_root(size_type a) const
80  {
81  if(a>=size())
82  return true;
83  // a root is its own parent
84  return nodes[a].parent==a;
85  }
86 
87  // are 'a' and 'b' in the same set?
88  bool same_set(size_type a, size_type b) const
89  {
90  return find(a)==find(b);
91  }
92 
93  // total number of elements
94  size_type size() const
95  {
96  return nodes.size();
97  }
98 
99  // size of the set that 'a' is in
100  size_type count(size_type a) const
101  {
102  if(a>=size())
103  return 1;
104  return nodes[find(a)].count;
105  }
106 
107  // make the array large enough to contain 'a'
108  void check_index(size_type a)
109  {
110  if(a>=size())
111  resize(a+1);
112  }
113 
114  // number of disjoint sets
115  size_type count_roots() const
116  {
117  size_type c=0;
118  for(size_type i=0; i<nodes.size(); i++)
119  if(is_root(i))
120  c++;
121  return c;
122  }
123 
124  // makes 'new_root' the root of the set 'old'
125  void re_root(size_type old, size_type new_root);
126 
127  // find a different member of the same set
128  size_type get_other(size_type a);
129 };
130 
131 template <typename T>
132 // NOLINTNEXTLINE(readability/identifiers)
133 class union_find:public numbering<T>
134 {
135 public:
136  // NOLINTNEXTLINE(readability/identifiers)
138 
139  // true == already in same set
140  bool make_union(const T &a, const T &b)
141  {
142  size_type na=number(a), nb=number(b);
143  bool is_union=find_number(na)==find_number(nb);
144  uuf.make_union(na, nb);
145  return is_union;
146  }
147 
148  // true == already in same set
150  typename numbering<T>::const_iterator it_b)
151  {
152  size_type na=it_a-numbering<T>::begin(), nb=it_b-numbering<T>::begin();
153  bool is_union=find_number(na)==find_number(nb);
154  uuf.make_union(na, nb);
155  return is_union;
156  }
157 
158  // are 'a' and 'b' in the same set?
159  bool same_set(const T &a, const T &b) const
160  {
161  typedef typename subt::number_type subt_number_typet;
162  subt_number_typet na=subt_number_typet(), nb=subt_number_typet();
163  bool have_na=!subt::get_number(a, na),
164  have_nb=!subt::get_number(b, nb);
165 
166  if(have_na && have_nb)
167  return uuf.same_set(na, nb);
168  else if(!have_na && !have_nb)
169  return a==b;
170  else
171  return false;
172  }
173 
174  // are 'a' and 'b' in the same set?
176  typename numbering<T>::const_iterator it_b) const
177  {
178  return uuf.same_set(it_a-numbering<T>::begin(), it_b-numbering<T>::begin());
179  }
180 
181  const T &find(typename numbering<T>::const_iterator it) const
182  {
183  return numbering<T>::operator[](find_number(it-numbering<T>::begin()));
184  }
185 
186  const T &find(const T &a)
187  {
188  return numbering<T>::operator[](find_number(number(a)));
189  }
190 
191  size_type find_number(typename numbering<T>::const_iterator it) const
192  {
193  return find_number(it-numbering<T>::begin());
194  }
195 
196  size_type find_number(size_type a) const
197  {
198  return uuf.find(a);
199  }
200 
201  size_type find_number(const T &a)
202  {
203  return uuf.find(number(a));
204  }
205 
206  bool is_root_number(size_type a) const
207  {
208  return uuf.is_root(a);
209  }
210 
211  bool is_root(const T &a) const
212  {
213  typename subt::number_type na;
214 
215  if(subt::get_number(a, na))
216  return true; // not found, it's a root
217  else
218  return uuf.is_root(na);
219  }
220 
221  bool is_root(typename numbering<T>::const_iterator it) const
222  {
223  return uuf.is_root(it-numbering<T>::begin());
224  }
225 
226  size_type number(const T &a)
227  {
228  size_type n=subt::number(a);
229 
230  if(n>=uuf.size())
231  uuf.resize(this->size());
232 
233  assert(uuf.size()==this->size());
234 
235  return n;
236  }
237 
238  void clear()
239  {
240  subt::clear();
241  uuf.clear();
242  }
243 
245  {
246  uuf.isolate(it-numbering<T>::begin());
247  }
248 
249  void isolate(const T &a)
250  {
251  uuf.isolate(number(a));
252  }
253 
254 protected:
257 };
258 
259 #endif // CPROVER_UTIL_UNION_FIND_H
size_type find_number(typename numbering< T >::const_iterator it) const
Definition: union_find.h:191
bool is_root(typename numbering< T >::const_iterator it) const
Definition: union_find.h:221
const T & find(const T &a)
Definition: union_find.h:186
nodet(size_type index)
Definition: union_find.h:35
void isolate(typename numbering< T >::const_iterator it)
Definition: union_find.h:244
size_type size() const
Definition: union_find.h:94
size_type count_roots() const
Definition: union_find.h:115
void resize(size_type size)
Definition: union_find.h:64
const T & find(typename numbering< T >::const_iterator it) const
Definition: union_find.h:181
numbering< T > subt
Definition: union_find.h:256
void make_union(size_type a, size_type b)
Definition: union_find.cpp:13
bool is_root(size_type a) const
Definition: union_find.h:79
bool same_set(const T &a, const T &b) const
Definition: union_find.h:159
size_type find(size_type a) const
Definition: union_find.cpp:145
size_type number(const T &a)
Definition: union_find.h:226
bool make_union(typename numbering< T >::const_iterator it_a, typename numbering< T >::const_iterator it_b)
Definition: union_find.h:149
size_type count(size_type a) const
Definition: union_find.h:100
void re_root(size_type old, size_type new_root)
Definition: union_find.cpp:74
void isolate(size_type a)
Definition: union_find.cpp:41
void check_index(size_type a)
Definition: union_find.h:108
void clear()
Definition: union_find.h:238
void isolate(const T &a)
Definition: union_find.h:249
std::size_t size_type
Definition: union_find.h:26
void swap(unsigned_union_find &other)
Definition: union_find.h:59
size_type find_number(size_type a) const
Definition: union_find.h:196
std::vector< nodet > nodes
Definition: union_find.h:41
numbering< T >::size_type size_type
Definition: union_find.h:137
bool is_root(const T &a) const
Definition: union_find.h:211
size_type find_number(const T &a)
Definition: union_find.h:201
bool make_union(const T &a, const T &b)
Definition: union_find.h:140
void intersection(const unsigned_union_find &other)
Definition: union_find.cpp:124
unsigned_union_find uuf
Definition: union_find.h:255
bool same_set(size_type a, size_type b) const
Definition: union_find.h:88
size_type get_other(size_type a)
Definition: union_find.cpp:108
bool same_set(typename numbering< T >::const_iterator it_a, typename numbering< T >::const_iterator it_b) const
Definition: union_find.h:175
bool is_root_number(size_type a) const
Definition: union_find.h:206