1 /*========================================================================
2 Copyright (C) 1996-2002 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: /Volumes/CVS/repository/spot/spot/buddy/src/tree.c,v 1.2 2003/05/05 13:45:08 aduret Exp $
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
45 BddTree *bddtree_addrange_rec(BddTree *, BddTree *, int, int, int, int);
46
47
48 /*======================================================================*/
49
update_seq(BddTree * t)50 static 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
bddtree_new(int id)64 BddTree *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
bddtree_del(BddTree * t)79 void 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
bddtree_addrange_rec(BddTree * t,BddTree * prev,int first,int last,int fixed,int id)92 BddTree *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
bddtree_addrange(BddTree * t,int first,int last,int fixed,int id)189 BddTree *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
196 int 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