mCRL2
Loading...
Searching...
No Matches
tree_set.cpp
Go to the documentation of this file.
1// Author(s): Bas Ploeger
2// Copyright: see the accompanying file COPYING or copy at
3// https://github.com/mCRL2org/mCRL2/blob/master/COPYING
4//
5// Distributed under the Boost Software License, Version 1.0.
6// (See accompanying file LICENSE_1_0.txt or copy at
7// http://www.boost.org/LICENSE_1_0.txt)
8//
10
15
16#define EMPTY_SET (-1)
17#define EMPTY_LIST (-1)
18#define EMPTY_TAG (-1)
19#define HASH_CLASS 16
20#define TAGS_BLOCK 15000
21#define BUCKETS_BLOCK 25000
22// simple hash function; uses two large primes
23#define hash(l,r,m) (36425657*l + 77673689*r) & m
24
25namespace mcrl2
26{
27namespace lts
28{
29
31{
32 buckets = nullptr;
33 buckets_size = 0;
34 buckets_next = 0;
35
36 tags = nullptr;
37 tags_size = 0;
38 tags_next = 0;
39
40 hashmask = (1 << HASH_CLASS) - 1;
41 hashtable = (ptrdiff_t*)malloc((hashmask+1)*sizeof(ptrdiff_t));
42 if (hashtable == nullptr)
43 {
44 throw mcrl2::runtime_error("Out of memory.");
45 }
46 for (ptrdiff_t i=0; i<=hashmask; ++i)
47 {
49 }
50}
51
53{
54 if (tags != nullptr)
55 {
56 free(tags);
57 tags = nullptr;
58 }
59 if (buckets != nullptr)
60 {
61 free(buckets);
62 buckets = nullptr;
63 }
64 free(hashtable);
65 hashtable = nullptr;
66}
67
69{
70 if (tags_next >= tags_size)
71 {
73 tags = (ptrdiff_t*)realloc(tags,tags_size*sizeof(ptrdiff_t));
74 if (tags == nullptr)
75 {
76 throw mcrl2::runtime_error("Out of memory.");
77 }
78 }
79}
80
82{
84 {
86 buckets = (bucket*)realloc(buckets,buckets_size*sizeof(bucket));
87 if (buckets == nullptr)
88 {
89 throw mcrl2::runtime_error("Out of memory.");
90 }
91 }
92 if (buckets_next*4 >= hashmask*3)
93 {
95 hashtable = (ptrdiff_t*)realloc(hashtable,(hashmask+1)*sizeof(ptrdiff_t));
96 if (hashtable == nullptr)
97 {
98 throw mcrl2::runtime_error("Out of memory.");
99 }
100 ptrdiff_t i,hc;
101 for (i=0; i<=hashmask; ++i)
102 {
104 }
105 for (i=0; i<buckets_next; ++i)
106 {
107 hc = hash(buckets[i].child_l,buckets[i].child_r,hashmask);
108 buckets[i].next = hashtable[hc];
109 hashtable[hc] = i;
110 }
111 }
112}
113
114ptrdiff_t tree_set_store::build_set(ptrdiff_t child_l,ptrdiff_t child_r)
115{
117 ptrdiff_t hc = hash(child_l,child_r,hashmask);
118 buckets[buckets_next].child_l = child_l;
119 buckets[buckets_next].child_r = child_r;
123 return buckets_next++;
124}
125
126ptrdiff_t tree_set_store::find_set(ptrdiff_t child_l,ptrdiff_t child_r)
127{
128 ptrdiff_t hc = hash(child_l,child_r,hashmask);
129 for (ptrdiff_t i=hashtable[hc]; i!=EMPTY_LIST; i=buckets[i].next)
130 {
131 if (buckets[i].child_l==child_l && buckets[i].child_r==child_r)
132 {
133 return i;
134 }
135 }
136 return build_set(child_l,child_r);
137}
138
139ptrdiff_t tree_set_store::create_set(std::vector<ptrdiff_t> &elems)
140{
141 if (elems.size() == 0)
142 {
143 return EMPTY_SET;
144 }
145
146 ptrdiff_t* nodes = MCRL2_SPECIFIC_STACK_ALLOCATOR(ptrdiff_t,elems.size());
147 std::size_t node_size = 0;
148 std::size_t i,j;
149 for (i=0; i < elems.size(); ++i)
150 {
151 nodes[i]=find_set(elems[i],EMPTY_SET);
152 }
153 node_size = i;
154 while (node_size > 1)
155 {
156 j = 0;
157 for (i=0; i<node_size; i+=2)
158 {
159 if (i == node_size-1)
160 {
161 nodes[j] = nodes[i];
162 }
163 else
164 {
165 nodes[j] = find_set(nodes[i],nodes[i+1]);
166 }
167 ++j;
168 }
169 node_size = j;
170 }
171 ptrdiff_t r = nodes[0];
172 return r;
173}
174
176{
177 return tags_next;
178}
179
180ptrdiff_t tree_set_store::get_set(ptrdiff_t tag)
181{
182 return tags[tag];
183}
184
186{
187 return buckets[set].child_l;
188}
189
191{
192 return buckets[set].child_r;
193}
194
195ptrdiff_t tree_set_store::get_set_size(ptrdiff_t set)
196{
197 if (buckets[set].child_r == EMPTY_SET)
198 {
199 return 1;
200 }
201 return get_set_size(buckets[set].child_l) +
202 get_set_size(buckets[set].child_r);
203}
204
206{
207 return (set == EMPTY_SET);
208}
209
210ptrdiff_t tree_set_store::set_set_tag(ptrdiff_t set)
211{
212 if (buckets[set].tag != EMPTY_TAG)
213 {
214 return buckets[set].tag;
215 }
216 check_tags();
217 tags[tags_next] = set;
218 buckets[set].tag = tags_next;
219 return tags_next++;
220}
221
222}
223}
bool is_set_empty(ptrdiff_t set)
Definition tree_set.cpp:205
ptrdiff_t get_set_child_left(ptrdiff_t set)
Definition tree_set.cpp:185
ptrdiff_t find_set(ptrdiff_t child_l, ptrdiff_t child_r)
Definition tree_set.cpp:126
ptrdiff_t create_set(std::vector< ptrdiff_t > &elems)
Definition tree_set.cpp:139
ptrdiff_t get_set(ptrdiff_t tag)
Definition tree_set.cpp:180
ptrdiff_t get_set_child_right(ptrdiff_t set)
Definition tree_set.cpp:190
ptrdiff_t build_set(ptrdiff_t child_l, ptrdiff_t child_r)
Definition tree_set.cpp:114
ptrdiff_t set_set_tag(ptrdiff_t set)
Definition tree_set.cpp:210
ptrdiff_t get_set_size(ptrdiff_t set)
Definition tree_set.cpp:195
Standard exception class for reporting runtime errors.
Definition exception.h:27
Exception classes for use in libraries and tools.
This file contains a workaround that allows to assign a small array of elements on the stack....
A class that takes a linear process specification and checks all tau-summands of that LPS for conflue...
Definition indexed_set.h:72
#define EMPTY_LIST
Definition tree_set.cpp:17
#define TAGS_BLOCK
Definition tree_set.cpp:20
#define HASH_CLASS
Definition tree_set.cpp:19
#define BUCKETS_BLOCK
Definition tree_set.cpp:21
#define EMPTY_SET
Definition tree_set.cpp:16
#define hash(l, r, m)
Definition tree_set.cpp:23
#define EMPTY_TAG
Definition tree_set.cpp:18