1 /*-----------------------------------------------------------------------
2
3 File : clb_ptrees.c
4
5 Author: Stephan Schulz
6
7 Contents
8
9 Functions for pointer 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> Wed Dec 17 21:17:34 MET 1997
20 New
21
22 -----------------------------------------------------------------------*/
23
24 #include "clb_ptrees.h"
25
26
27 /*---------------------------------------------------------------------*/
28 /* Global Variables */
29 /*---------------------------------------------------------------------*/
30
31
32 /*---------------------------------------------------------------------*/
33 /* Forward Declarations */
34 /*---------------------------------------------------------------------*/
35
36
37 /*---------------------------------------------------------------------*/
38 /* Internal Functions */
39 /*---------------------------------------------------------------------*/
40
41 /*-----------------------------------------------------------------------
42 //
43 // Function: splay_tree()
44 //
45 // Perform the splay operation on tree at node with key.
46 //
47 // Global Variables: -
48 //
49 // Side Effects : Changes tree
50 //
51 /----------------------------------------------------------------------*/
52
splay_ptree(PTree_p tree,void * key)53 static PTree_p splay_ptree(PTree_p tree, void* key)
54 {
55 PTree_p left, right, tmp;
56 PTreeCell newnode;
57
58 if (!tree)
59 {
60 return tree;
61 }
62
63 newnode.lson = NULL;
64 newnode.rson = NULL;
65 left = &newnode;
66 right = &newnode;
67
68 for (;;)
69 {
70 if(PLesser(key, tree->key))
71 {
72 if(!tree->lson)
73 {
74 break;
75 }
76 if(PLesser(key, tree->lson->key))
77 {
78 tmp = tree->lson;
79 tree->lson = tmp->rson;
80 tmp->rson = tree;
81 tree = tmp;
82 if (!tree->lson)
83 {
84 break;
85 }
86 }
87 right->lson = tree;
88 right = tree;
89 tree = tree->lson;
90 }
91 else if(PGreater(key, tree->key))
92 {
93 if (!tree->rson)
94 {
95 break;
96 }
97 if(PGreater(key, tree->rson->key))
98 {
99 tmp = tree->rson;
100 tree->rson = tmp->lson;
101 tmp->lson = tree;
102 tree = tmp;
103 if (!tree->rson)
104 {
105 break;
106 }
107 }
108 left->rson = tree;
109 left = tree;
110 tree = tree->rson;
111 }
112 else
113 {
114 break;
115 }
116 }
117 left->rson = tree->lson;
118 right->lson = tree->rson;
119 tree->lson = newnode.rson;
120 tree->rson = newnode.lson;
121
122 return tree;
123 }
124
125
126
127
128 /*---------------------------------------------------------------------*/
129 /* Exported Functions */
130 /*---------------------------------------------------------------------*/
131
132
133
134 /*-----------------------------------------------------------------------
135 //
136 // Function: PTreeCellAllocEmpty()
137 //
138 // Allocate a empty, initialized PTreeCell. Pointers to children
139 // are NULL, int values are 0 (and pointer values in ANSI-World
140 // undefined, in practice NULL on 32 bit machines)(This comment is
141 // superfluous!). The balance field is (correctly) set to 0.
142 //
143 // Global Variables: -
144 //
145 // Side Effects : Memory operations
146 //
147 /----------------------------------------------------------------------*/
148
PTreeCellAllocEmpty(void)149 PTree_p PTreeCellAllocEmpty(void)
150 {
151 PTree_p handle = PTreeCellAlloc();
152
153 handle->lson = handle->rson = NULL;
154
155 return handle;
156 }
157
158 /*-----------------------------------------------------------------------
159 //
160 // Function: PTreeFree()
161 //
162 // Free a PTree (including the keys, but not potential objects
163 // pointed to in the val fields
164 //
165 // Global Variables: -
166 //
167 // Side Effects : Memory operations
168 //
169 /----------------------------------------------------------------------*/
170
PTreeFree(PTree_p junk)171 void PTreeFree(PTree_p junk)
172 {
173 if(junk)
174 {
175 PStack_p stack = PStackAlloc();
176
177 PStackPushP(stack, junk);
178
179 while(!PStackEmpty(stack))
180 {
181 junk = PStackPopP(stack);
182 if(junk->lson)
183 {
184 PStackPushP(stack, junk->lson);
185 }
186 if(junk->rson)
187 {
188 PStackPushP(stack, junk->rson);
189 }
190 PTreeCellFree(junk);
191 }
192 PStackFree(stack);
193 }
194 }
195
196
197 /*-----------------------------------------------------------------------
198 //
199 // Function: PTreeInsert()
200 //
201 // If an entry with key *newnode->key exists in the tree return a
202 // pointer to it. Otherwise insert *newnode in the tree and return
203 // NULL. Will splay the tree!
204 //
205 // Global Variables: -
206 //
207 // Side Effects : Changes the tree.
208 //
209 /----------------------------------------------------------------------*/
210
PTreeInsert(PTree_p * root,PTree_p newnode)211 PTree_p PTreeInsert(PTree_p *root, PTree_p newnode)
212 {
213 if (!*root)
214 {
215 newnode->lson = newnode->rson = NULL;
216 *root = newnode;
217 return NULL;
218 }
219 *root = splay_ptree(*root, newnode->key);
220
221 if(PLesser(newnode->key, (*root)->key))
222 {
223 newnode->lson = (*root)->lson;
224 newnode->rson = *root;
225 (*root)->lson = NULL;
226 *root = newnode;
227 return NULL;
228 }
229 else if(PGreater(newnode->key, (*root)->key))
230 {
231 newnode->rson = (*root)->rson;
232 newnode->lson = *root;
233 (*root)->rson = NULL;
234 *root = newnode;
235 return NULL;
236 }
237 return *root;
238 }
239
240
241
242
243 /*-----------------------------------------------------------------------
244 //
245 // Function: PTreeStore()
246 //
247 // Insert a cell with given key into the tree. Return false if an
248 // entry for this key exists, true otherwise.
249 //
250 // Global Variables: -
251 //
252 // Side Effects : Changes tree
253 //
254 /----------------------------------------------------------------------*/
255
PTreeStore(PTree_p * root,void * key)256 bool PTreeStore(PTree_p *root, void* key)
257 {
258 PTree_p handle, newnode;
259
260 handle = PTreeCellAlloc();
261 handle->key = key;
262
263 newnode = PTreeInsert(root, handle);
264
265 if(newnode)
266 {
267 PTreeCellFree(handle);
268 return false;
269 }
270 return true;
271 }
272
273 /*-----------------------------------------------------------------------
274 //
275 // Function: PTreeFind()
276 //
277 // Find the entry with key key in the tree and return it. Return
278 // NULL if no such key exists.
279 //
280 // Global Variables: -
281 //
282 // Side Effects : -
283 //
284 /----------------------------------------------------------------------*/
285
PTreeFind(PTree_p * root,void * key)286 PTree_p PTreeFind(PTree_p *root, void* key)
287 {
288 if(*root)
289 {
290 *root = splay_ptree(*root, key);
291 if(PEqual((*root)->key, key))
292 {
293 return *root;
294 }
295 }
296 return NULL;
297 }
298
299
300 /*-----------------------------------------------------------------------
301 //
302 // Function: PTreeFindBinary()
303 //
304 // Find an entry by simple binary search. This does not reorganize
305 // the tree, otherwise it is inferior to PTreeFind()!
306 //
307 // Global Variables: -
308 //
309 // Side Effects : -
310 //
311 /----------------------------------------------------------------------*/
312
PTreeFindBinary(PTree_p root,void * key)313 PTree_p PTreeFindBinary(PTree_p root, void* key)
314 {
315 while(root)
316 {
317 if(PLesser(key, root->key))
318 {
319 root = root->lson;
320 }
321 else if(PGreater(key, root->key))
322 {
323 root = root->rson;
324 }
325 else
326 {
327 break;
328 }
329 }
330 return root;
331 }
332
333
334 /*-----------------------------------------------------------------------
335 //
336 // Function: PTreeExtractEntry()
337 //
338 // Find the entry with key key, remove it from the tree, rebalance
339 // the tree, and return the pointer to the removed element. Return
340 // NULL if no matching element exists.
341 //
342 //
343 // Global Variables: -
344 //
345 // Side Effects : Changes the tree
346 //
347 /----------------------------------------------------------------------*/
348
349
PTreeExtractEntry(PTree_p * root,void * key)350 PTree_p PTreeExtractEntry(PTree_p *root, void* key)
351 {
352 PTree_p x, cell;
353
354 if (!(*root))
355 {
356 return NULL;
357 }
358 *root = splay_ptree(*root, key);
359 if(PEqual(key, (*root)->key))
360 {
361 if (!(*root)->lson)
362 {
363 x = (*root)->rson;
364 }
365 else
366 {
367 x = splay_ptree((*root)->lson, key);
368 x->rson = (*root)->rson;
369 }
370 cell = *root;
371 cell->lson = cell->rson = NULL;
372 *root = x;
373 return cell;
374 }
375 return NULL;
376 }
377
378
379 /*-----------------------------------------------------------------------
380 //
381 // Function: PTreeExtractKey()
382 //
383 // Extract the entry with key key, delete the PTree-Node and return
384 // the key.
385 //
386 // Global Variables: -
387 //
388 // Side Effects : Memory operations, by PTreeExtractEntry()
389 //
390 /----------------------------------------------------------------------*/
391
PTreeExtractKey(PTree_p * root,void * key)392 void* PTreeExtractKey(PTree_p *root, void* key)
393 {
394 PTree_p handle;
395 void* res = NULL;
396
397 handle = PTreeExtractEntry(root, key);
398 if(handle)
399 {
400 res = handle->key;
401 PTreeCellFree(handle);
402 }
403 return res;
404 }
405
406 /*-----------------------------------------------------------------------
407 //
408 // Function: PTreeExtractRootKey()
409 //
410 // Extract the root node of the tree, delete it and return the
411 // key. Return NULL if the tree is empty.
412 //
413 // Global Variables: -
414 //
415 // Side Effects : Changes tree
416 //
417 /----------------------------------------------------------------------*/
418
PTreeExtractRootKey(PTree_p * root)419 void* PTreeExtractRootKey(PTree_p *root)
420 {
421 if(*root)
422 {
423 return PTreeExtractKey(root, (*root)->key);
424 }
425 return NULL;
426 }
427
428 /*-----------------------------------------------------------------------
429 //
430 // Function: PTreeDeleteEntry()
431 //
432 // Delete the entry with key key from the tree. Return true, if the
433 // key existed, false otherwise.
434 //
435 // Global Variables: -
436 //
437 // Side Effects : By PTreeExtract(), memory operations
438 //
439 /----------------------------------------------------------------------*/
440
PTreeDeleteEntry(PTree_p * root,void * key)441 bool PTreeDeleteEntry(PTree_p *root, void* key)
442 {
443 PTree_p cell;
444
445 cell = PTreeExtractEntry(root, key);
446 if(cell)
447 {
448 PTreeCellFree(cell);
449 return true;
450 }
451 return false;
452 }
453
454
455 /*-----------------------------------------------------------------------
456 //
457 // Function: PTreeMerge()
458 //
459 // Merge the two trees, i.e. destroy the second one and add its
460 // elements to the first one. Return true if *root gains a new
461 // element.
462 //
463 // Global Variables: -
464 //
465 // Side Effects : Changes both trees.
466 //
467 /----------------------------------------------------------------------*/
468
PTreeMerge(PTree_p * root,PTree_p add)469 bool PTreeMerge(PTree_p *root, PTree_p add)
470 {
471 PStack_p stack = PStackAlloc();
472 PTree_p tmp;
473 bool res = false;
474
475 PStackPushP(stack, add);
476
477 while(!PStackEmpty(stack))
478 {
479 add = PStackPopP(stack);
480 if(add)
481 {
482 PStackPushP(stack, add->lson);
483 PStackPushP(stack, add->rson);
484 tmp = PTreeInsert(root, add);
485 if(tmp)
486 {
487 PTreeCellFree(add);
488 }
489 else
490 {
491 res = true;
492 }
493 }
494 }
495 PStackFree(stack);
496 return res;
497 }
498
499
500 /*-----------------------------------------------------------------------
501 //
502 // Function: PTreeInsertTree()
503 //
504 // Insert the elements stored in add into *root.
505 //
506 // Global Variables: -
507 //
508 // Side Effects : Memory operations.
509 //
510 /----------------------------------------------------------------------*/
511
PTreeInsertTree(PTree_p * root,PTree_p add)512 void PTreeInsertTree(PTree_p *root, PTree_p add)
513 {
514 PStack_p stack = PStackAlloc();
515
516 PStackPushP(stack, add);
517
518 while(!PStackEmpty(stack))
519 {
520 add = PStackPopP(stack);
521 if(add)
522 {
523 PStackPushP(stack, add->lson);
524 PStackPushP(stack, add->rson);
525 PTreeStore(root, add->key);
526 }
527 }
528 PStackFree(stack);
529 }
530
531
532 /*-----------------------------------------------------------------------
533 //
534 // Function: PTreeNodes()
535 //
536 // Return the number of nodes in the tree.
537 //
538 // Global Variables: -
539 //
540 // Side Effects : -
541 //
542 /----------------------------------------------------------------------*/
543
PTreeNodes(PTree_p root)544 long PTreeNodes(PTree_p root)
545 {
546 PStack_p stack = PStackAlloc();
547 long res = 0;
548
549 PStackPushP(stack, root);
550
551 while(!PStackEmpty(stack))
552 {
553 root = PStackPopP(stack);
554 if(root)
555 {
556 PStackPushP(stack, root->lson);
557 PStackPushP(stack, root->rson);
558 res++;
559 }
560 }
561 PStackFree(stack);
562
563 return res;
564 }
565
566
567 /*-----------------------------------------------------------------------
568 //
569 // Function: PTreeDebugPrint()
570 //
571 // Print the keys stored in the tree. Returns number of nodes (why
572 // not ?).
573 //
574 // Global Variables: -
575 //
576 // Side Effects : Output
577 //
578 /----------------------------------------------------------------------*/
579
PTreeDebugPrint(FILE * out,PTree_p root)580 long PTreeDebugPrint(FILE* out, PTree_p root)
581 {
582 PStack_p stack = PStackAlloc();
583 long res = 0;
584
585 PStackPushP(stack, root);
586
587 while(!PStackEmpty(stack))
588 {
589 root = PStackPopP(stack);
590 if(root)
591 {
592 if(res % 10 == 0)
593 {
594 fprintf(out, "\n#");
595 }
596 fprintf(out, " %7p", root->key);
597 PStackPushP(stack, root->lson);
598 PStackPushP(stack, root->rson);
599 res++;
600 }
601 }
602 PStackFree(stack);
603 fprintf(out, "\n");
604
605 return res;
606 }
607
608
609 /*-----------------------------------------------------------------------
610 //
611 // Function: PStackToPTree()
612 //
613 // Interprete a stack as a list of pointers and insert these
614 // pointers into the tree at *root. Returns number of new elements
615 // in the tree.
616 //
617 // Global Variables: -
618 //
619 // Side Effects : -
620 //
621 /----------------------------------------------------------------------*/
622
PStackToPTree(PTree_p * root,PStack_p stack)623 long PStackToPTree(PTree_p *root, PStack_p stack)
624 {
625 PStackPointer i;
626 long res = 0;
627
628 for(i=0; i<PStackGetSP(stack); i++)
629 {
630 if(PTreeStore(root, PStackElementP(stack,i)))
631 {
632 res++;
633 }
634 }
635 return res;
636 }
637
638
639 /*-----------------------------------------------------------------------
640 //
641 // Function: PTreeToPStack()
642 //
643 // Push all the keys in the tree onto the stack (in arbitrary
644 // order). Return number of values pushed.
645 //
646 // Global Variables: -
647 //
648 // Side Effects : -
649 //
650 /----------------------------------------------------------------------*/
651
PTreeToPStack(PStack_p target_stack,PTree_p root)652 long PTreeToPStack(PStack_p target_stack, PTree_p root)
653 {
654 long res = 0;
655 PStack_p stack = PStackAlloc();
656 PTree_p handle;
657
658 PStackPushP(stack, root);
659
660 while(!PStackEmpty(stack))
661 {
662 handle = PStackPopP(stack);
663 if(handle)
664 {
665 PStackPushP(target_stack, handle->key);
666 res++;
667 PStackPushP(stack,handle->lson);
668 PStackPushP(stack,handle->rson);
669 }
670 }
671 PStackFree(stack);
672
673 return res;
674 }
675
676
677 /*-----------------------------------------------------------------------
678 //
679 // Function: PTreeSharedElement()
680 //
681 // If there exists an element common in both trees, return the first
682 // one found. Otherwise return NULL. This iterates over the elements
683 // of the second tree and searches in the first, so make the second
684 // one smaller if you have a choice.
685 //
686 // Global Variables: -
687 //
688 // Side Effects : Reorganizes tree1!
689 //
690 /----------------------------------------------------------------------*/
691
PTreeSharedElement(PTree_p * tree1,PTree_p tree2)692 void* PTreeSharedElement(PTree_p *tree1, PTree_p tree2)
693 {
694 PStack_p stack = PStackAlloc();
695 PTree_p handle, tmp;
696 void* res = NULL;
697
698 PStackPushP(stack, tree2);
699
700 while(!PStackEmpty(stack))
701 {
702 handle = PStackPopP(stack);
703 if(handle)
704 {
705 tmp = PTreeFind(tree1, handle->key);
706 if(tmp)
707 {
708 res = tmp->key;
709 break;
710 }
711 PStackPushP(stack,handle->lson);
712 PStackPushP(stack,handle->rson);
713 }
714 }
715 PStackFree(stack);
716 return res;
717 }
718
719
720 /*-----------------------------------------------------------------------
721 //
722 // Function: PTreeIntersection()
723 //
724 // Compute the intersection of the two PTrees and return it.
725 //
726 // Global Variables: -
727 //
728 // Side Effects : Memory operations
729 //
730 /----------------------------------------------------------------------*/
731
PTreeIntersection(PTree_p tree1,PTree_p tree2)732 PTree_p PTreeIntersection(PTree_p tree1, PTree_p tree2)
733 {
734 PStack_p stack = PStackAlloc();
735 PTree_p handle, tmp, res=NULL;
736
737 PStackPushP(stack, tree2);
738
739 while(!PStackEmpty(stack))
740 {
741 handle = PStackPopP(stack);
742 if(handle)
743 {
744 tmp = PTreeFindBinary(tree1, handle->key);
745 if(tmp)
746 {
747 PTreeStore(&res, handle->key);
748 }
749 PStackPushP(stack,handle->lson);
750 PStackPushP(stack,handle->rson);
751 }
752 }
753 PStackFree(stack);
754 return res;
755 }
756
757 /*-----------------------------------------------------------------------
758 //
759 // Function: PTreeIntersection()
760 //
761 // Make tree1 the intersection of tree1 and tree2. Does not change
762 // tree 2. Return the number of keys removed.
763 //
764 // Global Variables: -
765 //
766 // Side Effects : Memory operations
767 //
768 /----------------------------------------------------------------------*/
769
PTreeDestrIntersection(PTree_p * tree1,PTree_p tree2)770 long PTreeDestrIntersection(PTree_p *tree1, PTree_p tree2)
771 {
772 PTree_p tmp = NULL;
773 void* key;
774 long res = 0;
775
776 while((key = PTreeExtractRootKey(tree1)))
777 {
778 if(PTreeFindBinary(tree2, key))
779 {
780 PTreeStore(&tmp, key);
781 }
782 else
783 {
784 res++;
785 }
786 }
787 assert(!(*tree1));
788 *tree1 = tmp;
789
790 return res;
791 }
792
793
794 /*-----------------------------------------------------------------------
795 //
796 // Function: PTreeCopy()
797 //
798 // Return a Ptree that stores the same elements as tree.
799 //
800 // Global Variables: -
801 //
802 // Side Effects : Memory operations.
803 //
804 /----------------------------------------------------------------------*/
805
PTreeCopy(PTree_p tree)806 PTree_p PTreeCopy(PTree_p tree)
807 {
808 PTree_p res = NULL, handle;
809 PStack_p stack = PStackAlloc();
810
811 PStackPushP(stack, tree);
812
813 while(!PStackEmpty(stack))
814 {
815 handle = PStackPopP(stack);
816 if(handle)
817 {
818 PTreeStore(&res, handle->key);
819 PStackPushP(stack,handle->lson);
820 PStackPushP(stack,handle->rson);
821 }
822 }
823 PStackFree(stack);
824 return res;
825 }
826
827 AVL_TRAVERSE_DEFINITION(PTree, PTree_p)
828
829 /*---------------------------------------------------------------------*/
830 /* End of File */
831 /*---------------------------------------------------------------------*/
832
833
834
835
836