cprover
Toggle main menu visibility
Loading...
Searching...
No Matches
union_find.cpp
Go to the documentation of this file.
1
/*******************************************************************\
2
3
Module:
4
5
Author: Daniel Kroening, kroening@kroening.com
6
7
\*******************************************************************/
8
9
#include "
union_find.h
"
10
11
#include <algorithm>
12
13
void
unsigned_union_find::make_union
(
size_type
j,
size_type
k)
14
{
15
check_index
(j);
16
check_index
(k);
17
18
// make sure j, k are roots
19
j=
find
(j);
20
k=
find
(k);
21
22
if
(j==k)
23
return
;
// already in same set
24
25
// weight it
26
27
if
(
nodes
[j].
count
<
nodes
[k].
count
)
// j is the smaller set
28
{
29
nodes
[k].count+=
nodes
[j].count;
// so k becomes parent to j
30
nodes
[j].parent=k;
31
nodes
[j].count=0;
32
}
33
else
// j is NOT the smaller
34
{
35
nodes
[j].count+=
nodes
[k].count;
// so j becomes parent to k
36
nodes
[k].parent=j;
37
nodes
[k].count=0;
38
}
39
}
40
41
void
unsigned_union_find::isolate
(
size_type
a)
42
{
43
check_index
(a);
44
45
// is a itself a root?
46
if
(
is_root
(a))
47
{
48
size_type
c=
nodes
[a].count;
49
DATA_INVARIANT
(c != 0,
"a root cannot have a node count of zero"
);
50
51
// already isolated?
52
if
(c==1)
53
return
;
54
55
// find a new root
56
size_type
new_root=
get_other
(a);
57
CHECK_RETURN
(new_root != a);
58
59
re_root
(a, new_root);
60
}
61
62
// now it's not a root
63
// get its root
64
size_type
r
=
find
(a);
65
66
nodes
[
r
].count--;
67
nodes
[a].parent=a;
68
nodes
[a].count=1;
69
}
70
71
void
unsigned_union_find::re_root
(
size_type
old_root,
size_type
new_root)
72
{
73
check_index
(old_root);
74
check_index
(new_root);
75
76
// make sure old_root is a root
77
old_root=
find
(old_root);
78
79
// same set?
80
if
(
find
(new_root)!=old_root)
81
return
;
82
83
PRECONDITION
(!
is_root
(new_root));
84
PRECONDITION
(
nodes
[old_root].
count
>= 2);
85
86
nodes
[new_root].parent=new_root;
87
nodes
[new_root].count=
nodes
[old_root].count;
88
89
nodes
[old_root].parent=new_root;
90
nodes
[old_root].count=0;
91
92
// the order here is important!
93
94
for
(
size_type
i=0; i<
size
(); i++)
95
if
(i!=new_root && i!=old_root && !
is_root
(i))
96
{
97
size_type
r
=
find
(i);
98
if
(
r
==old_root ||
r
==new_root)
99
nodes
[i].parent=new_root;
100
}
101
}
102
103
unsigned_union_find::size_type
unsigned_union_find::get_other
(
size_type
a)
104
{
105
check_index
(a);
106
a=
find
(a);
107
108
// Cannot find another node in a singleton set
109
PRECONDITION
(
nodes
[a].
count
>= 2);
110
111
// find a different member of the same set
112
for
(
size_type
i=0; i<
size
(); i++)
113
if
(
find
(i)==a && i!=a)
114
return
i;
115
116
// UNREACHABLE;
117
return
0;
118
}
119
120
void
unsigned_union_find::intersection
(
121
const
unsigned_union_find
&other)
122
{
123
unsigned_union_find
new_sets;
124
125
new_sets.
resize
(std::max(
size
(), other.
size
()));
126
127
// should be n log n
128
129
for
(
size_type
i=0; i<
size
(); i++)
130
if
(!
is_root
(i))
131
{
132
size_type
j=
find
(i);
133
134
if
(other.
same_set
(i, j))
135
new_sets.
make_union
(i, j);
136
}
137
138
swap
(new_sets);
139
}
140
141
unsigned_union_find::size_type
unsigned_union_find::find
(
size_type
a)
const
142
{
143
if
(a>=
size
())
144
return
a;
145
146
while
(!
is_root
(a))
147
{
148
// one-pass variant of path-compression:
149
// make every other node in path
150
// point to its grandparent.
151
nodes
[a].parent=
nodes
[
nodes
[a].parent].parent;
152
153
a=
nodes
[a].parent;
154
}
155
156
return
a;
157
}
unsigned_union_find
Definition
union_find.h:23
unsigned_union_find::intersection
void intersection(const unsigned_union_find &other)
Definition
union_find.cpp:120
unsigned_union_find::resize
void resize(size_type size)
Definition
union_find.h:64
unsigned_union_find::size
size_type size() const
Definition
union_find.h:97
unsigned_union_find::nodes
std::vector< nodet > nodes
Definition
union_find.h:41
unsigned_union_find::check_index
void check_index(size_type a)
Definition
union_find.h:111
unsigned_union_find::re_root
void re_root(size_type old, size_type new_root)
Definition
union_find.cpp:71
unsigned_union_find::find
size_type find(size_type a) const
Definition
union_find.cpp:141
unsigned_union_find::count
size_type count(size_type a) const
Definition
union_find.h:103
unsigned_union_find::swap
void swap(unsigned_union_find &other)
Definition
union_find.h:59
unsigned_union_find::is_root
bool is_root(size_type a) const
Definition
union_find.h:82
unsigned_union_find::get_other
size_type get_other(size_type a)
Definition
union_find.cpp:103
unsigned_union_find::size_type
std::size_t size_type
Definition
union_find.h:26
unsigned_union_find::make_union
void make_union(size_type a, size_type b)
Definition
union_find.cpp:13
unsigned_union_find::same_set
bool same_set(size_type a, size_type b) const
Definition
union_find.h:91
unsigned_union_find::isolate
void isolate(size_type a)
Definition
union_find.cpp:41
r
static int8_t r
Definition
irep_hash.h:60
CHECK_RETURN
#define CHECK_RETURN(CONDITION)
Definition
invariant.h:495
DATA_INVARIANT
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition
invariant.h:534
PRECONDITION
#define PRECONDITION(CONDITION)
Definition
invariant.h:463
union_find.h
util
union_find.cpp
Generated by
1.17.0