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