CBMC
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  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 
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 
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 
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 
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 }
void intersection(const unsigned_union_find &other)
Definition: union_find.cpp:120
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)
Definition: union_find.cpp:71
size_type find(size_type a) const
Definition: union_find.cpp:141
size_type count(size_type a) const
Definition: union_find.h:103
void swap(unsigned_union_find &other)
Definition: union_find.h:59
bool is_root(size_type a) const
Definition: union_find.h:82
size_type get_other(size_type a)
Definition: union_find.cpp:103
std::size_t size_type
Definition: union_find.h:26
void make_union(size_type a, size_type b)
Definition: union_find.cpp:13
bool same_set(size_type a, size_type b) const
Definition: union_find.h:91
void isolate(size_type a)
Definition: union_find.cpp:41
static int8_t r
Definition: irep_hash.h:60
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:495
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:534
#define PRECONDITION(CONDITION)
Definition: invariant.h:463