CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
union_find.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: 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 <vector>
14
15#include "invariant.h"
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{
24public:
25 // NOLINTNEXTLINE(readability/identifiers)
26 typedef std::size_t size_type;
27
28protected:
29 struct nodet
30 {
31 size_type count; // set size
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
43public:
44 // merge the sets 'a' and 'b'
46
47 // find the root of the set 'a' belongs to
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
65 {
66 if(size < nodes.size())
67 {
68 INVARIANT(false, "we don't implement shrinking yet");
69 }
70
71 nodes.reserve(size);
72 while(nodes.size()<size)
73 nodes.push_back(nodet(nodes.size()));
74 }
75
76 void clear()
77 {
78 nodes.clear();
79 }
80
81 // is 'a' a root?
82 bool is_root(size_type a) const
83 {
84 if(a>=size())
85 return true;
86 // a root is its own parent
87 return nodes[a].parent==a;
88 }
89
90 // are 'a' and 'b' in the same set?
92 {
93 return find(a)==find(b);
94 }
95
96 // total number of elements
98 {
99 return nodes.size();
100 }
101
102 // size of the set that 'a' is in
104 {
105 if(a>=size())
106 return 1;
107 return nodes[find(a)].count;
108 }
109
110 // make the array large enough to contain 'a'
112 {
113 if(a>=size())
114 resize(a+1);
115 }
116
117 // number of disjoint sets
119 {
120 size_type c=0;
121 for(size_type i=0; i<nodes.size(); i++)
122 if(is_root(i))
123 c++;
124 return c;
125 }
126
127 // makes 'new_root' the root of the set 'old'
129
130 // find a different member of the same set
132};
133
136template <typename T, typename hasht = std::hash<T>>
137// NOLINTNEXTLINE(readability/identifiers)
138class union_find final
139{
142
143 // NOLINTNEXTLINE(readability/identifiers)
144 using number_type = typename numbering_typet::number_type;
145
146public:
147 // NOLINTNEXTLINE(readability/identifiers)
148 using size_type = typename numbering_typet::size_type;
149 // NOLINTNEXTLINE(readability/identifiers)
150 using iterator = typename numbering_typet::iterator;
151 // NOLINTNEXTLINE(readability/identifiers)
152 using const_iterator = typename numbering_typet::const_iterator;
153
154 // true == already in same set
155 bool make_union(const T &a, const T &b)
156 {
160 return is_union;
161 }
162
163 // true == already in same set
165 {
166 size_type na=it_a-numbers.begin(), nb=it_b-numbers.begin();
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 {
175 const std::optional<number_type> na = numbers.get_number(a);
176 const std::optional<number_type> nb = numbers.get_number(b);
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 {
188 return uuf.same_set(it_a-numbers.begin(), it_b-numbers.begin());
189 }
190
191 const T &find(const_iterator it) const
192 {
193 return numbers[find_number(it-numbers.begin())];
194 }
195
196 const T &find(const T &a)
197 {
198 return numbers[find_number(number(a))];
199 }
200
202 {
203 return find_number(it-numbers.begin());
204 }
205
207 {
208 return uuf.find(a);
209 }
210
212 {
213 return uuf.find(number(a));
214 }
215
217 {
218 return uuf.is_root(a);
219 }
220
221 bool is_root(const T &a) const
222 {
224 if(numbers.get_number(a, na))
225 return true; // not found, it's a root
226 else
227 return uuf.is_root(na);
228 }
229
230 bool is_root(const_iterator it) const
231 {
232 return uuf.is_root(it-numbers.begin());
233 }
234
236 {
237 size_type n=numbers.number(a);
238
239 if(n>=uuf.size())
240 uuf.resize(numbers.size());
241
242 INVARIANT(uuf.size()==numbers.size(), "container sizes must match");
243
244 return n;
245 }
246
247 void clear()
248 {
249 numbers.clear();
250 uuf.clear();
251 }
252
254 {
255 uuf.isolate(it-numbers.begin());
256 }
257
258 void isolate(const T &a)
259 {
261 }
262
263 std::optional<number_type> get_number(const T &a) const
264 {
265 return numbers.get_number(a);
266 }
267
268 size_t size() const { return numbers.size(); }
269
270 T &operator[](size_type t) { return numbers[t]; }
271 const T &operator[](size_type t) const { return numbers[t]; }
272
273 iterator begin() { return numbers.begin(); }
274 const_iterator begin() const { return numbers.begin(); }
275 const_iterator cbegin() const { return numbers.cbegin(); }
276
277 iterator end() { return numbers.end(); }
278 const_iterator end() const { return numbers.end(); }
279 const_iterator cend() const { return numbers.cend(); }
280
281protected:
284};
285
286#endif // CPROVER_UTIL_UNION_FIND_H
virtual void clear()
Reset the abstract state.
Definition ai.h:265
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
size_type number(const T &a)
Definition union_find.h:235
T & operator[](size_type t)
Definition union_find.h:270
void isolate(const_iterator it)
Definition union_find.h:253
const T & find(const_iterator it) const
Definition union_find.h:191
bool make_union(const T &a, const T &b)
Definition union_find.h:155
iterator begin()
Definition union_find.h:273
size_t size() const
Definition union_find.h:268
size_type find_number(const T &a)
Definition union_find.h:211
const_iterator cbegin() const
Definition union_find.h:275
const_iterator cend() const
Definition union_find.h:279
bool make_union(const_iterator it_a, const_iterator it_b)
Definition union_find.h:164
typename numbering_typet::number_type number_type
Definition union_find.h:144
numbering_typet numbers
Definition union_find.h:141
const_iterator begin() const
Definition union_find.h:274
numberingt< T, hasht > numbering_typet
Definition union_find.h:140
size_type find_number(size_type a) const
Definition union_find.h:206
const_iterator end() const
Definition union_find.h:278
unsigned_union_find uuf
Definition union_find.h:282
size_type find_number(const_iterator it) const
Definition union_find.h:201
bool same_set(const T &a, const T &b) const
Definition union_find.h:173
typename numbering_typet::size_type size_type
Definition union_find.h:148
void isolate(const T &a)
Definition union_find.h:258
typename numbering_typet::const_iterator const_iterator
Definition union_find.h:152
const T & operator[](size_type t) const
Definition union_find.h:271
typename numbering_typet::iterator iterator
Definition union_find.h:150
bool is_root(const T &a) const
Definition union_find.h:221
std::optional< number_type > get_number(const T &a) const
Definition union_find.h:263
bool same_set(const_iterator it_a, const_iterator it_b) const
Definition union_find.h:186
bool is_root_number(size_type a) const
Definition union_find.h:216
iterator end()
Definition union_find.h:277
bool is_root(const_iterator it) const
Definition union_find.h:230
void clear()
Definition union_find.h:247
const T & find(const T &a)
Definition union_find.h:196
void intersection(const unsigned_union_find &other)
void resize(size_type size)
Definition union_find.h:64
size_type size() const
Definition union_find.h:97
std::vector< nodet > nodes
Definition union_find.h:41
void check_index(size_type a)
Definition union_find.h:111
void re_root(size_type old, size_type new_root)
size_type find(size_type a) const
size_type count(size_type a) const
Definition union_find.h:103
void swap(unsigned_union_find &other)
Definition union_find.h:59
size_type count_roots() const
Definition union_find.h:118
bool is_root(size_type a) const
Definition union_find.h:82
size_type get_other(size_type a)
std::size_t size_type
Definition union_find.h:26
void make_union(size_type a, size_type b)
bool same_set(size_type a, size_type b) const
Definition union_find.h:91
void isolate(size_type a)
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423
nodet(size_type index)
Definition union_find.h:35