1/*========================================================================
2               Copyright (C) 1996-2001 by Jorn Lind-Nielsen
3                            All rights reserved
4
5    Permission is hereby granted, without written agreement and without
6    license or royalty fees, to use, reproduce, prepare derivative
7    works, distribute, and display this software and its documentation
8    for any purpose, provided that (1) the above copyright notice and
9    the following two paragraphs appear in all copies of the source code
10    and (2) redistributions, including without limitation binaries,
11    reproduce these notices in the supporting documentation. Substantial
12    modifications to this software may be copyrighted by their authors
13    and need not follow the licensing terms described here, provided
14    that the new terms are clearly indicated in all files where they apply.
15
16    IN NO EVENT SHALL JORN LIND-NIELSEN, OR DISTRIBUTORS OF THIS
17    SOFTWARE BE LIABLE TO ANY PARTY FOR DIRECT, INDIRECT, SPECIAL,
18    INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT OF THE USE OF THIS
19    SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE AUTHORS OR ANY OF THE
20    ABOVE PARTIES HAVE BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
21
22    JORN LIND-NIELSEN SPECIFICALLY DISCLAIM ANY WARRANTIES, INCLUDING,
23    BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND
24    FITNESS FOR A PARTICULAR PURPOSE. THE SOFTWARE PROVIDED HEREUNDER IS
25    ON AN "AS IS" BASIS, AND THE AUTHORS AND DISTRIBUTORS HAVE NO
26    OBLIGATION TO PROVIDE MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR
27    MODIFICATIONS.
28========================================================================*/
29
30/*************************************************************************
31  $Header$
32  FILE:  tree.c
33  DESCR: Trees for BDD variables
34  AUTH:  Jorn Lind
35  DATE:  (C) march 1998
36*************************************************************************/
37#include <stdio.h>
38#include <stdlib.h>
39#include "kernel.h"
40#include "bddtree.h"
41
42/*************************************************************************
43*************************************************************************/
44
45BddTree *bddtree_addrange_rec(BddTree *, BddTree *, int, int, int, int);
46
47
48/*======================================================================*/
49
50static void update_seq(BddTree *t)
51{
52   int n;
53   int low = t->first;
54
55   for (n=t->first ; n<=t->last ; n++)
56      if (bddvar2level[n] < bddvar2level[low])
57	 low = n;
58
59   for (n=t->first ; n<=t->last ; n++)
60      t->seq[bddvar2level[n]-bddvar2level[low]] = n;
61}
62
63
64BddTree *bddtree_new(int id)
65{
66   BddTree *t = NEW(BddTree,1);
67   if (t == NULL)
68      return NULL;
69
70   t->first = t->last = -1;
71   t->fixed = 1;
72   t->next = t->prev = t->nextlevel = NULL;
73   t->seq = NULL;
74   t->id = id;
75   return t;
76}
77
78
79void bddtree_del(BddTree *t)
80{
81   if (t == NULL)
82      return;
83
84   bddtree_del(t->nextlevel);
85   bddtree_del(t->next);
86   if (t->seq != NULL)
87      free(t->seq);
88   free(t);
89}
90
91
92BddTree *bddtree_addrange_rec(BddTree *t, BddTree *prev,
93			      int first, int last, int fixed, int id)
94{
95   if (first < 0  ||  last < 0  ||  last < first)
96      return NULL;
97
98      /* Empty tree -> build one */
99   if (t == NULL)
100   {
101      if ((t=bddtree_new(id)) == NULL)
102	 return NULL;
103      t->first = first;
104      t->fixed = fixed;
105      t->seq = NEW(int,last-first+1);
106      t->last = last;
107      update_seq(t);
108      t->prev = prev;
109      return t;
110   }
111
112      /* Check for identity */
113   if (first == t->first  &&  last == t->last)
114      return t;
115
116      /* Before this section -> insert */
117   if (last < t->first)
118   {
119      BddTree *tnew = bddtree_new(id);
120      if (tnew == NULL)
121	 return NULL;
122      tnew->first = first;
123      tnew->last = last;
124      tnew->fixed = fixed;
125      tnew->seq = NEW(int,last-first+1);
126      update_seq(tnew);
127      tnew->next = t;
128      tnew->prev = t->prev;
129      t->prev = tnew;
130      return tnew;
131   }
132
133      /* After this this section -> go to next */
134   if (first > t->last)
135   {
136      t->next = bddtree_addrange_rec(t->next, t, first, last, fixed, id);
137      return t;
138   }
139
140      /* Inside this section -> insert in next level */
141   if (first >= t->first  &&  last <= t->last)
142   {
143      t->nextlevel =
144	 bddtree_addrange_rec(t->nextlevel,NULL,first,last,fixed,id);
145      return t;
146   }
147
148      /* Covering this section -> insert above this level */
149   if (first <= t->first)
150   {
151      BddTree *tnew;
152      BddTree *this = t;
153
154      while (1)
155      {
156	    /* Partial cover ->error */
157	 if (last >= this->first  &&  last < this->last)
158	    return NULL;
159
160	 if (this->next == NULL  ||  last < this->next->first)
161	 {
162	    tnew = bddtree_new(id);
163	    if (tnew == NULL)
164	       return NULL;
165	    tnew->first = first;
166	    tnew->last = last;
167	    tnew->fixed = fixed;
168	    tnew->seq = NEW(int,last-first+1);
169	    update_seq(tnew);
170	    tnew->nextlevel = t;
171	    tnew->next = this->next;
172	    tnew->prev = t->prev;
173	    if (this->next != NULL)
174	       this->next->prev = tnew;
175	    this->next = NULL;
176	    t->prev = NULL;
177	    return tnew;
178	 }
179
180	 this = this->next;
181      }
182
183   }
184
185   return NULL;
186}
187
188
189BddTree *bddtree_addrange(BddTree *t, int first, int last, int fixed,int id)
190{
191   return bddtree_addrange_rec(t,NULL,first,last,fixed,id);
192}
193
194
195#if 0
196int main(void)
197{
198   BddTree *t = NULL;
199
200   t = bddtree_addrange(t, 8,10,1);
201   printf("A\n"); bddtree_print(stdout, t, 0);
202   t = bddtree_addrange(t, 2,99,1);
203   printf("B\n"); bddtree_print(stdout, t, 0);
204   t = bddtree_addrange(t, 11,50,1);
205   printf("C\n"); bddtree_print(stdout, t, 0);
206   t = bddtree_addrange(t, 5,7,1);
207   printf("D\n"); bddtree_print(stdout, t, 0);
208   t = bddtree_addrange(t, 5,10,1);
209   printf("E\n"); bddtree_print(stdout, t, 0);
210   t = bddtree_addrange(t, 100,150,1);
211   printf("F\n"); bddtree_print(stdout, t, 0);
212   t = bddtree_addrange(t, 60,65,1);
213   printf("G\n"); bddtree_print(stdout, t, 0);
214   t = bddtree_addrange(t, 3,200,1);
215
216   printf("H\n"); bddtree_print(stdout, t, 0);
217   bddtree_del(t);
218   return 0;
219}
220#endif
221
222/* EOF */
223