CBMC: /home/runner/work/cbmc/cbmc/src/util/union_find.cpp Source File

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}

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}

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}

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}

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}

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}

ait

ait supplies three of the four components needed: an abstract interpreter (in this case handling func...

Definition ai.h:566

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::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