CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
union_find.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: 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{
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
58
60 }
61
62 // now it's not a root
63 // get its root
65
66 nodes[r].count--;
67 nodes[a].parent=a;
68 nodes[a].count=1;
69}
70
72{
75
76 // make sure old_root is a root
78
79 // same set?
81 return;
82
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{
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}
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
void intersection(const unsigned_union_find &other)
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
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)
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