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: /cvsroot/buddy/buddy/src/pairs.c,v 1.1.1.1 2004/06/25 13:22:50 haimcohen Exp $
32 FILE: pairs.c
33 DESCR: Pair management for BDD package.
34 AUTH: Jorn Lind
35 DATE: february 1997
36 *************************************************************************/
37 #include <stdlib.h>
38 #include <limits.h>
39 #include "kernel.h"
40
41 /*======================================================================*/
42
43 static int pairsid; /* Pair identifier */
44 static bddPair* pairs; /* List of all replacement pairs in use */
45
46
47 /*************************************************************************
48 *************************************************************************/
49
bdd_pairs_init(void)50 void bdd_pairs_init(void)
51 {
52 pairsid = 0;
53 pairs = NULL;
54 }
55
56
bdd_pairs_done(void)57 void bdd_pairs_done(void)
58 {
59 bddPair *p = pairs;
60 int n;
61
62 while (p != NULL)
63 {
64 bddPair *next = p->next;
65 for (n=0 ; n<bddvarnum ; n++)
66 bdd_delref( p->result[n] );
67 free(p->result);
68 free(p);
69 p = next;
70 }
71 }
72
73
update_pairsid(void)74 static int update_pairsid(void)
75 {
76 pairsid++;
77
78 if (pairsid == (INT_MAX >> 2))
79 {
80 bddPair *p;
81 pairsid = 0;
82 for (p=pairs ; p!=NULL ; p=p->next)
83 p->id = pairsid++;
84 bdd_operator_reset();
85 }
86
87 return pairsid;
88 }
89
90
bdd_register_pair(bddPair * p)91 void bdd_register_pair(bddPair *p)
92 {
93 p->next = pairs;
94 pairs = p;
95 }
96
97
bdd_pairs_vardown(int level)98 void bdd_pairs_vardown(int level)
99 {
100 bddPair *p;
101
102 for (p=pairs ; p!=NULL ; p=p->next)
103 {
104 int tmp;
105
106 tmp = p->result[level];
107 p->result[level] = p->result[level+1];
108 p->result[level+1] = tmp;
109
110 if (p->last == level)
111 p->last++;
112 }
113 }
114
115
bdd_pairs_resize(int oldsize,int newsize)116 int bdd_pairs_resize(int oldsize, int newsize)
117 {
118 bddPair *p;
119 int n;
120
121 for (p=pairs ; p!=NULL ; p=p->next)
122 {
123 if ((p->result=(BDD*)realloc(p->result,sizeof(BDD)*newsize)) == NULL)
124 return bdd_error(BDD_MEMORY);
125
126 for (n=oldsize ; n<newsize ; n++)
127 p->result[n] = bdd_ithvar(bddlevel2var[n]);
128 }
129
130 return 0;
131 }
132
133
134 /*
135 NAME {* bdd\_newpair *}
136 SECTION {* kernel *}
137 SHORT {* creates an empty variable pair table *}
138 PROTO {* bddPair *bdd_newpair(void) *}
139 DESCR {* Variable pairs of the type {\tt bddPair} are used in
140 {\tt bdd\_replace} to define which variables to replace with
141 other variables. This function allocates such an empty table. The
142 table can be freed by a call to {\em bdd\_freepair}. *}
143 RETURN {* Returns a new table of pairs. *}
144 ALSO {* bdd\_freepair, bdd\_replace, bdd\_setpair, bdd\_setpairs *}
145 */
bdd_newpair(void)146 bddPair *bdd_newpair(void)
147 {
148 int n;
149 bddPair *p;
150
151 if ((p=(bddPair*)malloc(sizeof(bddPair))) == NULL)
152 {
153 bdd_error(BDD_MEMORY);
154 return NULL;
155 }
156
157 if ((p->result=(BDD*)malloc(sizeof(BDD)*bddvarnum)) == NULL)
158 {
159 free(p);
160 bdd_error(BDD_MEMORY);
161 return NULL;
162 }
163
164 for (n=0 ; n<bddvarnum ; n++)
165 p->result[n] = bdd_ithvar(bddlevel2var[n]);
166
167 p->id = update_pairsid();
168 p->last = -1;
169
170 bdd_register_pair(p);
171 return p;
172 }
173
174
175 /*
176 NAME {* bdd\_setpair *}
177 EXTRA {* bdd\_setbddpair *}
178 SECTION {* kernel *}
179 SHORT {* set one variable pair *}
180 PROTO {* int bdd_setpair(bddPair *pair, int oldvar, int newvar)
181 int bdd_setbddpair(bddPair *pair, BDD oldvar, BDD newvar) *}
182 DESCR {* Adds the pair {\tt (oldvar,newvar)} to the table of pairs
183 {\tt pair}. This results in {\tt oldvar} being substituted
184 with {\tt newvar} in a call to {\tt bdd\_replace}. In the first
185 version {\tt newvar} is an integer representing the variable
186 to be replaced with the old variable.
187 In the second version {\tt oldvar} is a BDD.
188 In this case the variable {\tt oldvar} is substituted with the
189 BDD {\tt newvar}.
190 The possibility to substitute with any BDD as {\tt newvar} is
191 utilized in bdd\_compose, whereas only the topmost variable
192 in the BDD is used in bdd\_replace. *}
193 RETURN {* Zero on success, otherwise a negative error code. *}
194 ALSO {* bdd\_newpair, bdd\_setpairs, bdd\_resetpair, bdd\_replace, bdd\_compose *}
195 */
bdd_setpair(bddPair * pair,int oldvar,int newvar)196 int bdd_setpair(bddPair *pair, int oldvar, int newvar)
197 {
198 if (pair == NULL)
199 return 0;
200
201 if (oldvar < 0 || oldvar > bddvarnum-1)
202 return bdd_error(BDD_VAR);
203 if (newvar < 0 || newvar > bddvarnum-1)
204 return bdd_error(BDD_VAR);
205
206 bdd_delref( pair->result[bddvar2level[oldvar]] );
207 pair->result[bddvar2level[oldvar]] = bdd_ithvar(newvar);
208 pair->id = update_pairsid();
209
210 if (bddvar2level[oldvar] > pair->last)
211 pair->last = bddvar2level[oldvar];
212
213 return 0;
214 }
215
216
bdd_setbddpair(bddPair * pair,int oldvar,BDD newvar)217 int bdd_setbddpair(bddPair *pair, int oldvar, BDD newvar)
218 {
219 int oldlevel;
220
221 if (pair == NULL)
222 return 0;
223
224 CHECK(newvar);
225 if (oldvar < 0 || oldvar >= bddvarnum)
226 return bdd_error(BDD_VAR);
227 oldlevel = bddvar2level[oldvar];
228
229 bdd_delref( pair->result[oldlevel] );
230 pair->result[oldlevel] = bdd_addref(newvar);
231 pair->id = update_pairsid();
232
233 if (oldlevel > pair->last)
234 pair->last = oldlevel;
235
236 return 0;
237 }
238
239
240 /*
241 NAME {* bdd\_setpairs *}
242 EXTRA {* bdd\_setbddpairs *}
243 SECTION {* kernel *}
244 SHORT {* defines a whole set of pairs *}
245 PROTO {* int bdd_setpairs(bddPair *pair, int *oldvar, int *newvar, int size)
246 int bdd_setbddpairs(bddPair *pair, int *oldvar, BDD *newvar, int size) *}
247 DESCR {* As for {\tt bdd\_setpair} but with {\tt oldvar} and {\tt newvar}
248 being arrays of variables (BDDs) of size {\tt size}. *}
249 RETURN {* Zero on success, otherwise a negative error code. *}
250 ALSO {* bdd\_newpair, bdd\_setpair, bdd\_replace, bdd\_compose *}
251 */
bdd_setpairs(bddPair * pair,int * oldvar,int * newvar,int size)252 int bdd_setpairs(bddPair *pair, int *oldvar, int *newvar, int size)
253 {
254 int n,e;
255 if (pair == NULL)
256 return 0;
257
258 for (n=0 ; n<size ; n++)
259 if ((e=bdd_setpair(pair, oldvar[n], newvar[n])) < 0)
260 return e;
261
262 return 0;
263 }
264
265
bdd_setbddpairs(bddPair * pair,int * oldvar,BDD * newvar,int size)266 int bdd_setbddpairs(bddPair *pair, int *oldvar, BDD *newvar, int size)
267 {
268 int n,e;
269 if (pair == NULL)
270 return 0;
271
272 for (n=0 ; n<size ; n++)
273 if ((e=bdd_setbddpair(pair, oldvar[n], newvar[n])) < 0)
274 return e;
275
276 return 0;
277 }
278
279
280 /*
281 NAME {* bdd\_freepair *}
282 SECTION {* kernel *}
283 SHORT {* frees a table of pairs *}
284 PROTO {* void bdd_freepair(bddPair *pair) *}
285 DESCR {* Frees the table of pairs {\tt pair} that has been allocated
286 by a call to {\tt bdd\_newpair}. *}
287 ALSO {* bdd\_replace, bdd\_newpair, bdd\_setpair, bdd\_resetpair *}
288 */
bdd_freepair(bddPair * p)289 void bdd_freepair(bddPair *p)
290 {
291 int n;
292
293 if (p == NULL)
294 return;
295
296 if (pairs != p)
297 {
298 bddPair *bp = pairs;
299 while (bp != NULL && bp->next != p)
300 bp = bp->next;
301
302 if (bp != NULL)
303 bp->next = p->next;
304 }
305 else
306 pairs = p->next;
307
308 for (n=0 ; n<bddvarnum ; n++)
309 bdd_delref( p->result[n] );
310 free(p->result);
311 free(p);
312 }
313
314
315 /*
316 NAME {* bdd\_resetpair *}
317 SECTION {* kernel *}
318 SHORT {* clear all variable pairs *}
319 PROTO {* void bdd_resetpair(bddPair *pair) *}
320 DESCR {* Resets the table of pairs {\tt pair} by setting all substitutions
321 to their default values (that is no change). *}
322 ALSO {* bdd\_newpair, bdd\_setpair, bdd\_freepair *}
323 */
bdd_resetpair(bddPair * p)324 void bdd_resetpair(bddPair *p)
325 {
326 int n;
327
328 for (n=0 ; n<bddvarnum ; n++)
329 p->result[n] = bdd_ithvar(n);
330 p->last = 0;
331 }
332
333
334 /* EOF */
335
336