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