1 /*-----------------------------------------------------------------------
2
3 File : clb_objtrees.c
4
5 Author: Stephan Schulz
6
7 Contents
8
9 Functions for object storing SPLAY trees.
10
11 Copyright 1998, 1999 by the author.
12 This code is released under the GNU General Public Licence and
13 the GNU Lesser General Public License.
14 See the file COPYING in the main E directory for details..
15 Run "eprover -h" for contact information.
16
17 Changes
18
19 <1> Mon Feb 15 16:43:21 MET 1999
20 Imported from clb_ptrees.c
21
22 -----------------------------------------------------------------------*/
23
24 #include "clb_objtrees.h"
25
26
27
28 /*---------------------------------------------------------------------*/
29 /* Global Variables */
30 /*---------------------------------------------------------------------*/
31
32
33 /*---------------------------------------------------------------------*/
34 /* Forward Declarations */
35 /*---------------------------------------------------------------------*/
36
37
38 /*---------------------------------------------------------------------*/
39 /* Internal Functions */
40 /*---------------------------------------------------------------------*/
41
42 /*-----------------------------------------------------------------------
43 //
44 // Function: splay_tree()
45 //
46 // Perform the splay operation on tree at node with key.
47 //
48 // Global Variables: -
49 //
50 // Side Effects : Changes tree
51 //
52 /----------------------------------------------------------------------*/
53
splay_tree(PObjTree_p tree,void * key,ComparisonFunctionType cmpfun)54 static PObjTree_p splay_tree(PObjTree_p tree, void* key,
55 ComparisonFunctionType cmpfun)
56 {
57 PObjTree_p left, right, tmp;
58 PTreeCell newnode;
59 int cmpres;
60
61 if (!tree)
62 {
63 return tree;
64 }
65
66 newnode.lson = NULL;
67 newnode.rson = NULL;
68 left = &newnode;
69 right = &newnode;
70
71 for (;;)
72 {
73 cmpres = cmpfun(key, tree->key);
74 if (cmpres < 0)
75 {
76 if(!tree->lson)
77 {
78 break;
79 }
80 if(cmpfun(key, tree->lson->key) < 0)
81 {
82 tmp = tree->lson;
83 tree->lson = tmp->rson;
84 tmp->rson = tree;
85 tree = tmp;
86 if (!tree->lson)
87 {
88 break;
89 }
90 }
91 right->lson = tree;
92 right = tree;
93 tree = tree->lson;
94 }
95 else if(cmpres > 0)
96 {
97 if (!tree->rson)
98 {
99 break;
100 }
101 if(cmpfun(key, tree->rson->key) > 0)
102 {
103 tmp = tree->rson;
104 tree->rson = tmp->lson;
105 tmp->lson = tree;
106 tree = tmp;
107 if (!tree->rson)
108 {
109 break;
110 }
111 }
112 left->rson = tree;
113 left = tree;
114 tree = tree->rson;
115 }
116 else
117 {
118 break;
119 }
120 }
121 left->rson = tree->lson;
122 right->lson = tree->rson;
123 tree->lson = newnode.rson;
124 tree->rson = newnode.lson;
125
126 return tree;
127 }
128
129
130
131
132 /*---------------------------------------------------------------------*/
133 /* Exported Functions */
134 /*---------------------------------------------------------------------*/
135
136
137 /*-----------------------------------------------------------------------
138 //
139 // Function: PTreeObjInsert()
140 //
141 // If an entry with cmpfun(*root->key, newnode->key) == 0 exists in the
142 // tree return a pointer to it. Otherwise insert *newnode in the tree
143 // and return NULL. Will splay the tree!
144 //
145 // Global Variables: -
146 //
147 // Side Effects : Changes the tree.
148 //
149 /----------------------------------------------------------------------*/
150
PTreeObjInsert(PObjTree_p * root,PObjTree_p newnode,ComparisonFunctionType cmpfun)151 PObjTree_p PTreeObjInsert(PObjTree_p *root, PObjTree_p newnode,
152 ComparisonFunctionType cmpfun)
153 {
154 int cmpres;
155 if (!*root)
156 {
157 newnode->lson = newnode->rson = NULL;
158 *root = newnode;
159 return NULL;
160 }
161 *root = splay_tree(*root, newnode->key, cmpfun);
162
163 cmpres = cmpfun(newnode->key, (*root)->key);
164
165 if (cmpres < 0)
166 {
167 newnode->lson = (*root)->lson;
168 newnode->rson = *root;
169 (*root)->lson = NULL;
170 *root = newnode;
171 return NULL;
172 }
173 else if(cmpres > 0)
174 {
175 newnode->rson = (*root)->rson;
176 newnode->lson = *root;
177 (*root)->rson = NULL;
178 *root = newnode;
179 return NULL;
180 }
181 return *root;
182 }
183
184
185
186
187 /*-----------------------------------------------------------------------
188 //
189 // Function: PTreeObjStore()
190 //
191 // Store object in the tree. If an object that is equal to obj
192 // already exists in the tree, return it, otherwise return NULL.
193 //
194 // otherwise.
195 //
196 // Global Variables: -
197 //
198 // Side Effects : Changes tree
199 //
200 /----------------------------------------------------------------------*/
201
PTreeObjStore(PObjTree_p * root,void * key,ComparisonFunctionType cmpfun)202 void* PTreeObjStore(PObjTree_p *root, void* key,
203 ComparisonFunctionType cmpfun)
204 {
205 PObjTree_p handle, newnode;
206
207 handle = PTreeCellAlloc();
208 handle->key = key;
209
210 newnode = PTreeObjInsert(root, handle, cmpfun);
211
212 if(newnode)
213 {
214 PTreeCellFree(handle);
215 return newnode->key;
216 }
217 return NULL;
218 }
219
220 /*-----------------------------------------------------------------------
221 //
222 // Function: PTreeObjFind()
223 //
224 // Find the entry with key key in the tree and return it. Return
225 // NULL if no such key exists.
226 //
227 // Global Variables: -
228 //
229 // Side Effects : -
230 //
231 /----------------------------------------------------------------------*/
232
PTreeObjFind(PObjTree_p * root,void * key,ComparisonFunctionType cmpfun)233 PObjTree_p PTreeObjFind(PObjTree_p *root, void* key, ComparisonFunctionType
234 cmpfun)
235 {
236 if(*root)
237 {
238 *root = splay_tree(*root, key, cmpfun);
239 if(cmpfun((*root)->key, key)==0)
240 {
241 return *root;
242 }
243 }
244 return NULL;
245 }
246
247 /*-----------------------------------------------------------------------
248 //
249 // Function: PTreeObjFindObj()
250 //
251 // Find and return object matching key (if any), return NULL if
252 // none.
253 //
254 // Global Variables: -
255 //
256 // Side Effects : -
257 //
258 /----------------------------------------------------------------------*/
259
PTreeObjFindObj(PObjTree_p * root,void * key,ComparisonFunctionType cmpfun)260 void* PTreeObjFindObj(PObjTree_p *root, void* key,
261 ComparisonFunctionType cmpfun)
262 {
263 PObjTree_p node = PTreeObjFind(root, key, cmpfun);
264
265 if(node)
266 {
267 return node->key;
268 }
269 return NULL;
270 }
271
272
273
274 /*-----------------------------------------------------------------------
275 //
276 // Function: PTreeObjFindBinary()
277 //
278 // Find the entry with key key in the tree and return it. Return
279 // NULL if no such key exists. Does not reorganize the tree!
280 //
281 // Global Variables: -
282 //
283 // Side Effects : -
284 //
285 /----------------------------------------------------------------------*/
286
PTreeObjFindBinary(PObjTree_p root,void * key,ComparisonFunctionType cmpfun)287 PObjTree_p PTreeObjFindBinary(PObjTree_p root, void* key, ComparisonFunctionType
288 cmpfun)
289 {
290 int cmpres;
291
292 while(root)
293 {
294 cmpres = cmpfun(key, root->key);
295 if(cmpres < 0)
296 {
297 root = root->lson;
298 }
299 else if(cmpres > 0)
300 {
301 root = root->rson;
302 }
303 else
304 {
305 break;
306 }
307 }
308 return root;
309 }
310
311
312
313 /*-----------------------------------------------------------------------
314 //
315 // Function: PTreeObjExtractEntry()
316 //
317 // Find the entry with key key, remove it from the tree, rebalance
318 // the tree, and return the pointer to the removed element. Return
319 // NULL if no matching element exists.
320 //
321 //
322 // Global Variables: -
323 //
324 // Side Effects : Changes the tree
325 //
326 /----------------------------------------------------------------------*/
327
PTreeObjExtractEntry(PObjTree_p * root,void * key,ComparisonFunctionType cmpfun)328 PObjTree_p PTreeObjExtractEntry(PObjTree_p *root, void* key,
329 ComparisonFunctionType cmpfun)
330 {
331 PObjTree_p x, cell;
332
333 if (!(*root))
334 {
335 return NULL;
336 }
337 *root = splay_tree(*root, key, cmpfun);
338 if(cmpfun(key, (*root)->key)==0)
339 {
340 if (!(*root)->lson)
341 {
342 x = (*root)->rson;
343 }
344 else
345 {
346 x = splay_tree((*root)->lson, key, cmpfun);
347 x->rson = (*root)->rson;
348 }
349 cell = *root;
350 cell->lson = cell->rson = NULL;
351 *root = x;
352 return cell;
353 }
354 return NULL;
355 }
356
357
358 /*-----------------------------------------------------------------------
359 //
360 // Function: PTreeObjExtractObject()
361 //
362 // Extract the entry object, delete the PTree-Node and return
363 // the pointer to the object.
364 //
365 // Global Variables: -
366 //
367 // Side Effects : Memory operations, by PTreeExtractEntry()
368 //
369 /----------------------------------------------------------------------*/
370
PTreeObjExtractObject(PObjTree_p * root,void * key,ComparisonFunctionType cmpfun)371 void* PTreeObjExtractObject(PObjTree_p *root, void* key,
372 ComparisonFunctionType cmpfun)
373 {
374 PObjTree_p handle;
375 void* res = NULL;
376
377 handle = PTreeObjExtractEntry(root, key, cmpfun);
378 if(handle)
379 {
380 res = handle->key;
381 PTreeCellFree(handle);
382 }
383 return res;
384 }
385
386 /*-----------------------------------------------------------------------
387 //
388 // Function: PTreeObjExtractRootObject()
389 //
390 // Extract the root node of the tree, delete it and return the
391 // key. Return NULL if the tree is empty.
392 //
393 // Global Variables: -
394 //
395 // Side Effects : Changes tree
396 //
397 /----------------------------------------------------------------------*/
398
PTreeObjExtractRootObject(PObjTree_p * root,ComparisonFunctionType cmpfun)399 void* PTreeObjExtractRootObject(PObjTree_p *root, ComparisonFunctionType
400 cmpfun)
401 {
402 if(*root)
403 {
404 return PTreeObjExtractObject(root, (*root)->key, cmpfun);
405 }
406 return NULL;
407 }
408
409
410 /*-----------------------------------------------------------------------
411 //
412 // Function: PTreeObjMerge()
413 //
414 // Merge the two trees, i.e. destroy the second one and add its
415 // element to the first one.
416 //
417 // Global Variables: -
418 //
419 // Side Effects : Changes both trees.
420 //
421 /----------------------------------------------------------------------*/
422
PTreeObjMerge(PObjTree_p * root,PObjTree_p add,ComparisonFunctionType cmpfun)423 void PTreeObjMerge(PObjTree_p *root, PObjTree_p add, ComparisonFunctionType
424 cmpfun)
425 {
426 PStack_p stack = PStackAlloc();
427 PObjTree_p res;
428
429 PStackPushP(stack, add);
430
431 while(!PStackEmpty(stack))
432 {
433 add = PStackPopP(stack);
434 if(add)
435 {
436 PStackPushP(stack, add->lson);
437 PStackPushP(stack, add->rson);
438 res = PTreeObjInsert(root, add, cmpfun);
439 UNUSED(res); assert(!res); /* Pointers should never be in two trees at
440 once for my intended application */
441 }
442 }
443 PStackFree(stack);
444 }
445
446
447 /*-----------------------------------------------------------------------
448 //
449 // Function: PObjTreeFree()
450 //
451 // Free a PObjTree, including the objects.
452 //
453 // Global Variables: -
454 //
455 // Side Effects : Memory operations
456 //
457 /----------------------------------------------------------------------*/
458
PObjTreeFree(PObjTree_p root,ObjDelFun del_fun)459 void PObjTreeFree(PObjTree_p root, ObjDelFun del_fun)
460 {
461 if(root)
462 {
463 PObjTreeFree(root->lson, del_fun);
464 PObjTreeFree(root->rson, del_fun);
465 del_fun(root->key);
466 PTreeCellFree(root);
467 }
468 }
469
470
471 /*-----------------------------------------------------------------------
472 //
473 // Function: PObjTreeNodes()
474 //
475 // Return the number of nodes in the tree.
476 //
477 // Global Variables: -
478 //
479 // Side Effects : -
480 //
481 /----------------------------------------------------------------------*/
482
PObjTreeNodes(PObjTree_p root)483 long PObjTreeNodes(PObjTree_p root)
484 {
485 PStack_p stack = PStackAlloc();
486 long res = 0;
487
488 PStackPushP(stack, root);
489
490 while(!PStackEmpty(stack))
491 {
492 root = PStackPopP(stack);
493 if(root)
494 {
495 PStackPushP(stack, root->lson);
496 PStackPushP(stack, root->rson);
497 res++;
498 }
499 }
500 PStackFree(stack);
501
502 return res;
503 }
504
505
506 /*---------------------------------------------------------------------*/
507 /* End of File */
508 /*---------------------------------------------------------------------*/
509
510
511