cprover
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 
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 
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 
50  // already isolated?
51  if(c==1)
52  return;
53 
54  assert(c>=2);
55 
56  // find a new root
57  size_type new_root=get_other(a);
58  assert(new_root!=a);
59 
60  re_root(a, new_root);
61  }
62 
63  // now it's not a root
64  // get its root
65  size_type r=find(a);
66 
67  // assert(r!=a);
68 
69  nodes[r].count--;
70  nodes[a].parent=a;
71  nodes[a].count=1;
72 }
73 
75 {
76  check_index(old_root);
77  check_index(new_root);
78 
79  // make sure old_root is a root
80  old_root=find(old_root);
81 
82  // same set?
83  // assert(find(new_root)==old_root);
84  if(find(new_root)!=old_root)
85  return;
86 
87  // make sure we actually do something
88  assert(new_root!=old_root);
89  assert(nodes[old_root].count>=2);
90 
91  nodes[new_root].parent=new_root;
92  nodes[new_root].count=nodes[old_root].count;
93 
94  nodes[old_root].parent=new_root;
95  nodes[old_root].count=0;
96 
97  // the order here is important!
98 
99  for(size_type i=0; i<size(); i++)
100  if(i!=new_root && i!=old_root && !is_root(i))
101  {
102  size_type r=find(i);
103  if(r==old_root || r==new_root)
104  nodes[i].parent=new_root;
105  }
106 }
107 
109 {
110  check_index(a);
111  a=find(a);
112 
113  assert(nodes[a].count>=2);
114 
115  // find a different member of the same set
116  for(size_type i=0; i<size(); i++)
117  if(find(i)==a && i!=a)
118  return i;
119 
120 // UNREACHABLE;
121  return 0;
122 }
123 
125  const unsigned_union_find &other)
126 {
127  unsigned_union_find new_sets;
128 
129  new_sets.resize(std::max(size(), other.size()));
130 
131  // should be n log n
132 
133  for(size_type i=0; i<size(); i++)
134  if(!is_root(i))
135  {
136  size_type j=find(i);
137 
138  if(other.same_set(i, j))
139  new_sets.make_union(i, j);
140  }
141 
142  swap(new_sets);
143 }
144 
146 {
147  if(a>=size())
148  return a;
149 
150  while(!is_root(a))
151  {
152  // one-pass variant of path-compression:
153  // make every other node in path
154  // point to its grandparent.
155  nodes[a].parent=nodes[nodes[a].parent].parent;
156 
157  a=nodes[a].parent;
158  }
159 
160  return a;
161 }
static int8_t r
Definition: irep_hash.h:59
size_type size() const
Definition: union_find.h:94
void resize(size_type size)
Definition: union_find.h:64
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
size_type find(size_type a) const
Definition: union_find.cpp:145
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
std::size_t size_type
Definition: union_find.h:26
void swap(unsigned_union_find &other)
Definition: union_find.h:59
std::vector< nodet > nodes
Definition: union_find.h:41
void intersection(const unsigned_union_find &other)
Definition: union_find.cpp:124
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