1 /*********************************************************************
2 Copyright 2013 JST ERATO Minato project and other contributors
3 http://www-erato.ist.hokudai.ac.jp/?language=en
4
5 Permission is hereby granted, free of charge, to any person obtaining
6 a copy of this software and associated documentation files (the
7 "Software"), to deal in the Software without restriction, including
8 without limitation the rights to use, copy, modify, merge, publish,
9 distribute, sublicense, and/or sell copies of the Software, and to
10 permit persons to whom the Software is furnished to do so, subject to
11 the following conditions:
12
13 The above copyright notice and this permission notice shall be
14 included in all copies or substantial portions of the Software.
15
16 THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
17 EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
18 MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
19 NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE
20 LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION
21 OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION
22 WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
23 **********************************************************************/
24 /*****************************************
25 * BDD Package (SAPPORO-1.57) - Body *
26 * (C) Shin-ichi MINATO (June 14, 2013) *
27 ******************************************/
28
29 #include <stdio.h>
30 #include <stdlib.h>
31 #include "SAPPOROBDD/bddc.h"
32
33 /* ----------------- MACRO Definitions ---------------- */
34 /* Operation IDs in Cache */
35 #define BC_NULL 0
36 #define BC_AND 1
37 #define BC_XOR 2
38 #define BC_AT0 3
39 #define BC_AT1 4
40 #define BC_LSHIFT 5
41 #define BC_RSHIFT 6
42 #define BC_COFACTOR 7
43 #define BC_UNIV 8
44 #define BC_SUPPORT 9
45 #define BC_INTERSEC 10
46 #define BC_UNION 11
47 #define BC_SUBTRACT 12
48 #define BC_OFFSET 13
49 #define BC_ONSET 14
50 #define BC_CHANGE 15
51 #define BC_CARD 16
52 #define BC_LIT 17
53 #define BC_LEN 18
54
55 /* Macros for malloc, realloc */
56 #define B_MALLOC(type, size) \
57 (type *)malloc(sizeof(type) * size)
58 #define B_REALLOC(ptr, type, size) \
59 (type *)realloc(ptr, sizeof(type) * size)
60
61 /* Printf format of bddp */
62 #ifdef B_64
63 # define B_BDDP_FD "%lld"
64 # define B_BDDP_FX "0x%llX"
65 #else
66 # define B_BDDP_FD "%d"
67 # define B_BDDP_FX "0x%X"
68 #endif
69
70 /* strtol or strtoll */
71 #ifdef B_64
72 # define B_STRTOI strtoll
73 #else
74 # define B_STRTOI strtol
75 #endif
76
77 /* Table spaces */
78 #define B_NODE_MAX (B_VAL_MASK>>1U) /* Max number of BDD nodes */
79 #define B_NODE_SPC0 256 /* Default initial node size */
80 #define B_VAR_SPC0 16 /* Initial var table size */
81 #define B_HASH_SPC0 4 /* Initial hash size */
82 #define B_RFCT_SPC0 4 /* Initial RFCT size */
83
84 /* Negative edge manipulation */
85 #define B_NEG(f) ((f) & B_INV_MASK)
86 #define B_NOT(f) ((f) ^ B_INV_MASK)
87 #define B_ABS(f) ((f) & ~B_INV_MASK)
88
89 /* Constant node manipulation */
90 #define B_CST(f) ((f) & B_CST_MASK)
91 #define B_VAL(f) ((f) & B_VAL_MASK)
92
93 /* Conversion of bddp and node index/pointer */
94 #define B_NP(f) (Node+(B_ABS(f)>>1U))
95 #define B_NDX(f) (B_ABS(f)>>1U)
96 #define B_BDDP_NP(p) ((bddp)((p)-Node) << 1U)
97
98 /* Read & Write of bddp field in the tables */
99 #ifdef B_64
100 # define B_LOW32(f) ((bddp_32)((f)&((1ULL<<32U)-1U)))
101 # define B_HIGH8(f) ((bddp_h8)((f)>>32U))
102 # define B_SET_NXP(p, f, i) \
103 (p ## _h8 = f ## _h8 + i, p ## _32 = f ## _32 + i)
104 # define B_GET_BDDP(f) \
105 ((bddp) f ## _32 | ((bddp) f ## _h8 << 32U))
106 # define B_SET_BDDP(f, g) \
107 (f ## _h8 = B_HIGH8(g), f ## _32 = B_LOW32(g))
108 # define B_CPY_BDDP(f, g) \
109 (f ## _h8 = g ## _h8, f ## _32 = g ## _32)
110 #else
111 # define B_SET_NXP(p, f, i) (p ## _32 = f ## _32 + i)
112 # define B_GET_BDDP(f) (f ## _32)
113 # define B_SET_BDDP(f, g) (f ## _32 = g)
114 # define B_CPY_BDDP(f, g) (f ## _32 = g ## _32)
115 #endif /* B_64 */
116
117 /* var & rfc manipulation */
118 #define B_VAR_NP(p) ((p)->varrfc & B_VAR_MASK)
119 #define B_RFC_MASK (~B_VAR_MASK)
120 #define B_RFC_UNIT (1U << B_VAR_WIDTH)
121 #define B_RFC_NP(p) ((p)->varrfc >> B_VAR_WIDTH)
122 #define B_RFC_ZERO_NP(p) ((p)->varrfc < B_RFC_UNIT)
123 #define B_RFC_ONE_NP(p) (((p)->varrfc & B_RFC_MASK) == B_RFC_UNIT)
124 #define B_RFC_INC_NP(p) \
125 (((p)->varrfc < B_RFC_MASK - B_RFC_UNIT)? \
126 ((p)->varrfc += B_RFC_UNIT, 0) : rfc_inc_ovf(p))
127 #define B_RFC_DEC_NP(p) \
128 (((p)->varrfc >= B_RFC_MASK)? rfc_dec_ovf(p): \
129 (B_RFC_ZERO_NP(p))? \
130 err("B_RFC_DEC_NP: rfc under flow", p-Node): \
131 ((p)->varrfc -= B_RFC_UNIT, 0))
132
133 /* ----------- Stack overflow limitter ------------ */
134 const int BDD_RecurLimit = 65536;
135 int BDD_RecurCount = 0;
136 #define BDD_RECUR_INC \
137 {if(++BDD_RecurCount >= BDD_RecurLimit) \
138 err("BDD_RECUR_INC: Recursion Limit", BDD_RecurCount);}
139 #define BDD_RECUR_DEC BDD_RecurCount--
140
141 /* Conversion of ZBDD node flag */
142 #define B_Z_NP(p) ((p)->f0_32 & (bddp_32)B_INV_MASK)
143
144 /* Hash Functions */
145 #define B_HASHKEY(f0, f1, hashSpc) \
146 (((B_CST(f0)? (f0): (f0)+2U) \
147 ^(B_NEG(f0)? ~((f0)>>1U): ((f0)>>1U)) \
148 ^(B_CST(f1)? (f1)<<1U: ((f1)+2U)<<1U) \
149 ^(B_NEG(f1)? ~((f1)>>1U): ((f1)>>1U)) )\
150 & (hashSpc-1U))
151 /* (((f0)^((f0)>>10)^((f0)>>31)^(f1)^((f1)>>8)^((f1)>>31)) \*/
152 #define B_CACHEKEY(op, f, g) \
153 ((((bddp)(op)<<2U) \
154 ^(B_CST(f)? (f): (f)+2U) \
155 ^(B_NEG(f)? ~((f)>>1U): ((f)>>1U)) \
156 ^(B_CST(g)? (g)<<3U: ((g)+2U)<<3U) \
157 ^(B_NEG(g)? ~((g)>>1U): ((g)>>1U)) )\
158 & (CacheSpc-1U))
159
160 /* ------- Declaration of static (internal) data ------- */
161 /* typedef of bddp field in the tables */
162 typedef unsigned int bddp_32;
163 #ifdef B_64
164 typedef unsigned char bddp_h8;
165 #endif
166
167 /* Declaration of Node table */
168 struct B_NodeTable
169 {
170 bddp_32 f0_32; /* 0-edge */
171 bddp_32 f1_32; /* 1-edge */
172 bddp_32 nx_32; /* Node index */
173 unsigned int varrfc; /* VarID & Reference counter */
174 #ifdef B_64
175 bddp_h8 f0_h8; /* Extention of 0-edge */
176 bddp_h8 f1_h8; /* Extention of 1-edge */
177 bddp_h8 nx_h8; /* Extention of node index */
178 #endif /* B_64 */
179 };
180 static struct B_NodeTable *Node = 0; /* Node Table */
181 static bddp NodeLimit = 0; /* Final limit size */
182 static bddp NodeUsed = 0; /* Number of used node */
183 static bddp Avail = bddnull; /* Head of available node */
184 static bddp NodeSpc = 0; /* Current Node-Table size */
185
186 /* Declaration of Hash-table per Var */
187 struct B_VarTable
188 {
189 bddp hashSpc; /* Current hash-table size */
190 bddp hashUsed; /* Current used entries */
191 bddvar lev; /* Level of the variable */
192 bddp_32 *hash_32; /* Hash-table */
193 #ifdef B_64
194 bddp_h8 *hash_h8; /* Extension of hash-table */
195 #endif /* B_64 */
196 };
197 static struct B_VarTable *Var = 0; /* Var-tables */
198 static bddvar *VarID = 0; /* VarID reverse table */
199 static bddvar VarUsed = 0; /* Number of used Var */
200 static bddvar VarSpc = 0; /* Current Var-table size */
201
202 /* Declaration of Operation Cache */
203 struct B_CacheTable
204 {
205 bddp_32 f_32; /* an operand BDD */
206 bddp_32 g_32; /* an operand BDD */
207 bddp_32 h_32; /* Result BDD */
208 unsigned char op; /* Operation code */
209 #ifdef B_64
210 bddp_h8 f_h8; /* Extention of an operand BDD */
211 bddp_h8 g_h8; /* Extention of an operand BDD */
212 bddp_h8 h_h8; /* Extention of result BDD */
213 #endif /* B_64 */
214 };
215 static struct B_CacheTable *Cache = 0; /* Opeartion cache */
216 static bddp CacheSpc = 0; /* Current cache size */
217
218 /* Declaration of RFC-table */
219 struct B_RFC_Table
220 {
221 bddp_32 nx_32; /* Node index */
222 bddp_32 rfc_32; /* RFC */
223 #ifdef B_64
224 bddp_h8 nx_h8; /* Extension of Node index */
225 bddp_h8 rfc_h8; /* Extension of RFC */
226 #endif /* B_64 */
227 };
228 static struct B_RFC_Table *RFCT = 0; /* RFC-Table */
229 static bddp RFCT_Spc; /* Current RFC-table size */
230 static bddp RFCT_Used; /* Current RFC-table used entries */
231
232 /* ----- Declaration of static (internal) functions ------ */
233 /* Private procedure */
234 static int err B_ARG((char *msg, bddp num));
235 static int rfc_inc_ovf B_ARG((struct B_NodeTable *np));
236 static int rfc_dec_ovf B_ARG((struct B_NodeTable *np));
237 static void var_enlarge B_ARG((void));
238 static int node_enlarge B_ARG((void));
239 static int hash_enlarge B_ARG((bddvar v));
240 static bddp getnode B_ARG((bddvar v, bddp f0, bddp f1));
241 static bddp getbddp B_ARG((bddvar v, bddp f0, bddp f1));
242 static bddp getzbddp B_ARG((bddvar v, bddp f0, bddp f1));
243 static bddp apply B_ARG((bddp f, bddp g, unsigned char op, unsigned char skip));
244 static void gc1 B_ARG((struct B_NodeTable *np));
245 static bddp count B_ARG((bddp f));
246 static void dump B_ARG((bddp f));
247 static void reset B_ARG((bddp f));
248 static void export B_ARG((FILE *strm, bddp f));
249 static int import B_ARG((FILE *strm, bddp *p, int lim, int z));
250 static int andfalse B_ARG((bddp f, bddp g));
251
252
253 /* ------------------ Body of program -------------------- */
254 /* ----------------- External functions ------------------ */
bddinit(initsize,limitsize)255 int bddinit(initsize, limitsize)
256 bddp initsize;
257 bddp limitsize;
258 /* Returns 1 if not enough memory (usually 0) */
259 {
260 bddp ix;
261 bddvar i;
262
263 /* Check dupulicate initialization */
264 if(Node) free(Node);
265 if(Var)
266 {
267 for(i=0; i<VarSpc; i++)
268 {
269 if(Var[i].hash_32) free(Var[i].hash_32);
270 #ifdef B_64
271 if(Var[i].hash_h8) free(Var[i].hash_h8);
272 #endif
273 }
274 free(Var);
275 }
276 if(VarID) free(VarID);
277 if(Cache) free(Cache);
278 if(RFCT) free(RFCT);
279
280 /* Set NodeLimit */
281 if(limitsize < B_NODE_SPC0) NodeLimit = B_NODE_SPC0;
282 else if(limitsize > B_NODE_MAX) NodeLimit = B_NODE_MAX;
283 else NodeLimit = limitsize;
284
285 /* Set NodeSpc */
286 if(initsize < B_NODE_SPC0) NodeSpc = B_NODE_SPC0;
287 else if(initsize > NodeLimit) NodeSpc = NodeLimit;
288 else NodeSpc = initsize;
289
290 /* Set CacheSpc */
291 for(CacheSpc=B_NODE_SPC0; CacheSpc<NodeSpc>>1; CacheSpc<<=1U)
292 ; /* empty */
293
294 /* Set VarSpc */
295 VarSpc = B_VAR_SPC0;
296
297 /* Memory allocation */
298 Node = B_MALLOC(struct B_NodeTable, NodeSpc);
299 Var = B_MALLOC(struct B_VarTable, VarSpc);
300 VarID = B_MALLOC(bddvar, VarSpc);
301 Cache = B_MALLOC(struct B_CacheTable, CacheSpc);
302
303 /* Check overflow */
304 if(Node == 0 || Var == 0 || VarID == 0 || Cache == 0)
305 {
306 if(Cache){ free(Cache); Cache = 0; }
307 if(VarID){ free(VarID); VarID = 0; }
308 if(Var){ free(Var); Var = 0; }
309 if(Node){ free(Node); Node = 0; }
310 NodeLimit = 0;
311 return 1;
312 }
313
314 /* Initialize */
315 NodeUsed = 0;
316 Node[NodeSpc-1U].varrfc = 0;
317 B_SET_BDDP(Node[NodeSpc-1U].nx, bddnull);
318 for(ix=0; ix<NodeSpc-1U; ix++)
319 {
320 Node[ix].varrfc = 0;
321 B_SET_BDDP(Node[ix].nx, ix+1U);
322 }
323 Avail = 0;
324
325 VarUsed = 0;
326 for(i=0; i<VarSpc; i++)
327 {
328 Var[i].hashSpc = 0;
329 Var[i].hashUsed = 0;
330 Var[i].lev = i;
331 VarID[i] = i;
332 Var[i].hash_32 = 0;
333 #ifdef B_64
334 Var[i].hash_h8 = 0;
335 #endif
336 }
337
338 for(ix=0; ix<CacheSpc; ix++) Cache[ix].op = BC_NULL;
339
340 RFCT_Spc = 0;
341 RFCT_Used = 0;
342
343 return 0;
344 }
345
bddcopy(f)346 bddp bddcopy(f)
347 bddp f;
348 {
349 struct B_NodeTable *fp;
350
351 if(f == bddnull) return bddnull;
352 if(B_CST(f)) return f; /* Constant */
353 fp = B_NP(f);
354 if(fp >= Node+NodeSpc || fp->varrfc == 0)
355 err("bddcopy: Invalid bddp", f);
356 B_RFC_INC_NP(fp);
357 return f;
358 }
359
bddfree(f)360 void bddfree(f)
361 bddp f;
362 {
363 struct B_NodeTable *fp;
364
365 if(f == bddnull) return;
366 if(B_CST(f)) return; /* Constant */
367 fp = B_NP(f);
368 if(fp >= Node+NodeSpc || fp->varrfc == 0)
369 err("bddfree: Invalid bddp", f);
370 B_RFC_DEC_NP(fp);
371 }
372
bddgc()373 int bddgc()
374 /* Returns 1 if there are no free node (usually 0) */
375 {
376 bddp i, n, f;
377 struct B_NodeTable *fp;
378 struct B_CacheTable *cachep;
379 struct B_NodeTable *np;
380 struct B_VarTable *varp;
381 bddvar v;
382 bddp oldSpc, newSpc, nx, key, f0, f1;
383 bddp_32 *newhash_32, *p_32, *p2_32;
384 #ifdef B_64
385 bddp_h8 *newhash_h8, *p_h8, *p2_h8;
386 #endif
387
388 n = NodeUsed;
389 for(fp=Node; fp<Node+NodeSpc; fp++)
390 if(fp->varrfc != 0 && B_RFC_ZERO_NP(fp))
391 gc1(fp);
392 if(n == NodeUsed) return 1; /* No free node */
393
394 /* Cache clear */
395 for(cachep=Cache; cachep<Cache+CacheSpc; cachep++)
396 {
397 switch(cachep->op)
398 {
399 case BC_NULL:
400 break;
401 case BC_AND:
402 case BC_XOR:
403 case BC_INTERSEC:
404 case BC_UNION:
405 case BC_SUBTRACT:
406 case BC_CHANGE:
407 f = B_GET_BDDP(cachep->f);
408 if(!B_CST(f) && (fp=B_NP(f))<Node+NodeSpc && fp->varrfc == 0)
409 {
410 cachep->op = BC_NULL;
411 break;
412 }
413 f = B_GET_BDDP(cachep->g);
414 if(!B_CST(f) && (fp=B_NP(f))<Node+NodeSpc && fp->varrfc == 0)
415 {
416 cachep->op = BC_NULL;
417 break;
418 }
419 f = B_GET_BDDP(cachep->h);
420 if(!B_CST(f) && (fp=B_NP(f))<Node+NodeSpc && fp->varrfc == 0)
421 {
422 cachep->op = BC_NULL;
423 break;
424 }
425 break;
426 case BC_AT0:
427 case BC_AT1:
428 case BC_OFFSET:
429 case BC_ONSET:
430 f = B_GET_BDDP(cachep->f);
431 if(!B_CST(f) && (fp=B_NP(f))<Node+NodeSpc && fp->varrfc == 0)
432 {
433 cachep->op = BC_NULL;
434 break;
435 }
436 f = B_GET_BDDP(cachep->h);
437 if(!B_CST(f) && (fp=B_NP(f))<Node+NodeSpc && fp->varrfc == 0)
438 {
439 cachep->op = BC_NULL;
440 break;
441 }
442 break;
443 case BC_CARD:
444 case BC_LIT:
445 case BC_LEN:
446 f = B_GET_BDDP(cachep->f);
447 if(!B_CST(f) && (fp=B_NP(f))<Node+NodeSpc && fp->varrfc == 0)
448 {
449 cachep->op = BC_NULL;
450 break;
451 }
452 break;
453 default:
454 cachep->op = BC_NULL;
455 break;
456 }
457 }
458
459 /* Hash-table packing */
460 for(v=1; v<=VarUsed; v++)
461 {
462 varp = &Var[v];
463
464 /* Get new size */
465 oldSpc = varp->hashSpc;
466 newSpc = oldSpc;
467 while(newSpc > B_HASH_SPC0)
468 {
469 if(newSpc>>2 < varp->hashUsed) break;
470 newSpc >>= 1;
471 }
472 if(newSpc == oldSpc) continue;
473
474 /* Reduce space */
475 #ifdef B_64
476 newhash_32 = B_MALLOC(bddp_32, newSpc);
477 newhash_h8 = B_MALLOC(bddp_h8, newSpc);
478 if(!newhash_32 || !newhash_h8)
479 {
480 if(newhash_32) free(newhash_32);
481 if(newhash_h8) free(newhash_h8);
482 break; /* Not enough memory */
483 }
484 #else
485 newhash_32 = B_MALLOC(bddp_32, newSpc);
486 if(!newhash_32) break; /* Not enough memory */
487 #endif
488
489 /* Initialize new hash entry */
490 for(i=0; i<newSpc; i++)
491 {
492 B_SET_NXP(p, newhash, i);
493 B_SET_BDDP(*p, bddnull);
494 }
495
496 /* restore hash entry */
497 for(i=0; i<oldSpc; i++)
498 {
499 key = i & (newSpc-1U);
500 np = 0;
501 B_SET_NXP(p, newhash, key);
502 nx = B_GET_BDDP(*p);
503 while(nx != bddnull)
504 {
505 np = Node + nx;
506 nx = B_GET_BDDP(np->nx);
507 }
508 if(np) { B_SET_NXP(p2, varp->hash, i); B_CPY_BDDP(np->nx, *p2); }
509 else
510 {
511 B_SET_NXP(p, newhash, key);
512 B_SET_NXP(p2, varp->hash, i);
513 B_CPY_BDDP(*p, *p2);
514 }
515 }
516 varp->hashSpc = newSpc;
517 free(varp->hash_32);
518 varp->hash_32 = newhash_32;
519 #ifdef B_64
520 free(varp->hash_h8);
521 varp->hash_h8 = newhash_h8;
522 #endif
523 }
524 return 0;
525 }
526
bddused()527 bddp bddused() { return NodeUsed; }
528
bddsize(f)529 bddp bddsize(f)
530 bddp f;
531 /* Returns 0 for bddnull */
532 {
533 bddp num;
534 struct B_NodeTable *fp;
535
536 if(f == bddnull) return 0;
537 if(B_CST(f)) return 0; /* Constant */
538 if((fp=B_NP(f))>=Node+NodeSpc || fp->varrfc == 0)
539 err("bddsize: Invalid bddp", f);
540
541 num = count(f);
542 reset(f);
543 return num;
544 }
545
bddvsize(p,lim)546 bddp bddvsize(p, lim)
547 bddp *p;
548 int lim;
549 /* Returns 0 for bddnull */
550 {
551 bddp num;
552 struct B_NodeTable *fp;
553 int n, i;
554
555 /* Check operand */
556 n = lim;
557 for(i=0; i<n; i++)
558 {
559 if(p[i] == bddnull)
560 {
561 n = i;
562 break;
563 }
564 if(!B_CST(p[i])&&
565 ((fp=B_NP(p[i]))>=Node+NodeSpc || fp->varrfc==0))
566 err("bddvsize: Invalid bddp", p[i]);
567 }
568 num = 0;
569 for(i=0; i<n; i++) num += count(p[i]);
570 for(i=0; i<n; i++) reset(p[i]);
571 return num;
572 }
573
bddexport(strm,p,lim)574 void bddexport(strm, p, lim)
575 FILE *strm;
576 bddp *p;
577 int lim;
578 {
579 struct B_NodeTable *fp;
580 int n, i, lev, lev0;
581
582 /* Check operands */
583 n = lim;
584 lev = 0;
585 for(i=0; i<n; i++)
586 {
587 if(p[i] == bddnull)
588 {
589 n = i;
590 break;
591 }
592 if(!B_CST(p[i])&&
593 ((fp=B_NP(p[i]))>=Node+NodeSpc || fp->varrfc==0))
594 err("bddvexport: Invalid bddp", p[i]);
595 lev0 = bddlevofvar(bddtop(p[i]));
596 if(lev0 > lev) lev = lev0;
597 }
598
599 fprintf(strm, "_i %d\n_o %d\n_n ", lev, n);
600 fprintf(strm, B_BDDP_FD, bddvsize(p, n));
601 fprintf(strm, "\n");
602
603 /* Put internal nodes */
604 for(i=0; i<n; i++) export(strm, p[i]);
605 for(i=0; i<n; i++) reset(p[i]);
606
607 /* Put external node */
608 for(i=0; i<n; i++)
609 {
610 if(p[i] == bddfalse) fprintf(strm, "F");
611 else if(p[i] == bddtrue) fprintf(strm, "T");
612 else fprintf(strm, B_BDDP_FD, p[i]);
613 fprintf(strm, "\n");
614 }
615 }
616
bdddump(f)617 void bdddump(f)
618 bddp f;
619 {
620 struct B_NodeTable *fp;
621
622 /* Check indexes */
623 if(f == bddnull) { printf("RT = NULL\n\n"); return; }
624 if(!B_CST(f)&&
625 ((fp=B_NP(f))>=Node+NodeSpc || fp->varrfc==0))
626 err("bdddump: Invalid bddp", f);
627
628 /* Dump nodes */
629 dump(f);
630 reset(f);
631
632 /* Dump top node */
633 printf("RT = ");
634 if(B_NEG(f)) putchar('~');
635 if(B_CST(f)) printf(B_BDDP_FD, B_ABS(B_VAL(f)));
636 else { printf("N"); printf(B_BDDP_FD, B_NDX(f)); }
637 printf("\n\n");
638 }
639
bddvdump(p,n)640 void bddvdump(p, n)
641 bddp *p;
642 int n;
643 {
644 struct B_NodeTable *fp;
645 int i;
646
647 /* Check operands */
648 for(i=0; i<n; i++)
649 {
650 if(p[i] == bddnull) return;
651 if(!B_CST(p[i])&&
652 ((fp=B_NP(p[i]))>=Node+NodeSpc || fp->varrfc==0))
653 err("bddvdump: Invalid bddp", p[i]);
654 }
655
656 /* Dump nodes */
657 for(i=0; i<n; i++) if(p[i] != bddnull) dump(p[i]);
658 for(i=0; i<n; i++) if(p[i] != bddnull) reset(p[i]);
659
660 /* Dump top node */
661 for(i=0; i<n; i++)
662 {
663 printf("RT%d = ", i);
664 if(p[i] == bddnull) printf("NULL");
665 else
666 {
667 if(B_NEG(p[i])) putchar('~');
668 if(B_CST(p[i])) printf(B_BDDP_FD, B_ABS(B_VAL(p[i])));
669 else { printf("N"); printf(B_BDDP_FD, B_NDX(p[i])); }
670 }
671 putchar('\n');
672 }
673 printf("\n");
674 }
675
bddrcache(op,f,g)676 bddp bddrcache(op, f, g)
677 unsigned char op;
678 bddp f, g;
679 {
680 struct B_CacheTable *cachep;
681
682 cachep = Cache + B_CACHEKEY(op, f, g);
683 if(op == cachep->op &&
684 f == B_GET_BDDP(cachep->f) &&
685 g == B_GET_BDDP(cachep->g))
686 return B_GET_BDDP(cachep->h); /* Hit */
687 return bddnull;
688 }
689
bddwcache(op,f,g,h)690 void bddwcache(op, f, g, h)
691 unsigned char op;
692 bddp f, g, h;
693 {
694 struct B_CacheTable *cachep;
695
696 if(op < 20) err("bddwcache: op < 20", op);
697 if(h == bddnull) return;
698 cachep = Cache + B_CACHEKEY(op, f, g);
699 cachep->op = op;
700 B_SET_BDDP(cachep->f, f);
701 B_SET_BDDP(cachep->g, g);
702 B_SET_BDDP(cachep->h, h);
703 }
704
bddnot(f)705 bddp bddnot(f)
706 bddp f;
707 {
708 if(f == bddnull) return bddnull;
709 return B_NOT(bddcopy(f));
710 }
711
bddlevofvar(v)712 bddvar bddlevofvar(v)
713 bddvar v;
714 {
715 if(v > VarUsed)
716 err("bddlevofvar: Invalid VarID", v);
717 return Var[v].lev;
718 }
719
bddvaroflev(lev)720 bddvar bddvaroflev(lev)
721 bddvar lev;
722 {
723 if(lev > VarUsed)
724 err("bddvaroflev: Invalid level", lev);
725 return VarID[lev];
726 }
727
bddvarused()728 bddvar bddvarused()
729 {
730 return VarUsed;
731 }
732
bddnewvar()733 bddvar bddnewvar()
734 {
735 if(++VarUsed == VarSpc) var_enlarge();
736 return VarUsed;
737 }
738
bddnewvaroflev(lev)739 bddvar bddnewvaroflev(lev)
740 bddvar lev;
741 {
742 bddvar i, v;
743
744 if(lev == 0 || lev > ++VarUsed)
745 err("bddnewvaroflev: Invalid level", lev);
746 if(VarUsed == VarSpc) var_enlarge();
747 for(i=VarUsed; i>lev; i--) Var[ VarID[i] = VarID[i-1U] ].lev = i;
748 Var[ VarID[lev] = VarUsed ].lev = lev;
749 return VarUsed;
750 }
751
bddtop(f)752 bddvar bddtop(f)
753 bddp f;
754 {
755 struct B_NodeTable *fp;
756
757 if(f == bddnull) return 0;
758 if(B_CST(f)) return 0; /* Constant */
759 fp = B_NP(f);
760 if(fp >= Node+NodeSpc || fp->varrfc == 0)
761 err("bddtop: Invalid bddp", f);
762 return B_VAR_NP(fp);
763 }
764
bddprime(v)765 bddp bddprime(v)
766 bddvar v;
767 /* Returns bddnull if not enough memory */
768 {
769 if(v == 0 || v > VarUsed)
770 err("bddprime: Invalid VarID", v);
771 return getbddp(v, bddfalse, bddtrue);
772 }
773
774
bddand(f,g)775 bddp bddand(f, g)
776 bddp f, g;
777 /* Returns bddnull if not enough memory */
778 {
779 struct B_NodeTable *fp;
780
781 /* Check operands */
782 if(f == bddnull) return bddnull;
783 if(g == bddnull) return bddnull;
784 if(B_CST(f))
785 { if(B_ABS(f) != bddfalse) err("bddand: Invalid bddp", f); }
786 else
787 {
788 fp = B_NP(f);
789 if(fp>=Node+NodeSpc || !fp->varrfc)
790 err("bddand: Invalid bddp", f);
791 if(B_Z_NP(fp)) err("bddand: applying ZBDD node", f);
792 }
793 if(B_CST(g))
794 { if(B_ABS(g) != bddfalse) err("bddand: Invalid bddp", g); }
795 else
796 {
797 fp = B_NP(g);
798 if(fp>=Node+NodeSpc || !fp->varrfc)
799 err("bddand: Invalid bddp", g);
800 if(B_Z_NP(fp)) err("bddand: applying ZBDD node", g);
801 }
802
803 return apply(f, g, BC_AND, 0);
804 }
805
bddor(f,g)806 bddp bddor(f, g)
807 bddp f, g;
808 /* Returns bddnull if not enough memory */
809 {
810 bddp h;
811
812 if(f == bddnull) return bddnull;
813 if(g == bddnull) return bddnull;
814 h = bddand(B_NOT(f), B_NOT(g));
815 if(h == bddnull) return bddnull;
816 return B_NOT(h);
817 }
818
bddxor(f,g)819 bddp bddxor(f, g)
820 bddp f, g;
821 /* Returns bddnull if not enough memory */
822 {
823 struct B_NodeTable *fp;
824
825 /* Check operands */
826 if(f == bddnull) return bddnull;
827 if(g == bddnull) return bddnull;
828 if(B_CST(f))
829 { if(B_ABS(f) != bddfalse) err("bddand: Invalid bddp", f); }
830 else
831 {
832 fp = B_NP(f);
833 if(fp>=Node+NodeSpc || !fp->varrfc)
834 err("bddxor: Invalid bddp", f);
835 if(B_Z_NP(fp)) err("bddand: applying ZBDD node", f);
836 }
837 if(B_CST(g))
838 { if(B_ABS(g) != bddfalse) err("bddand: Invalid bddp", g); }
839 else
840 {
841 fp = B_NP(g);
842 if(fp>=Node+NodeSpc || !fp->varrfc)
843 err("bddxor: Invalid bddp", g);
844 if(B_Z_NP(fp)) err("bddand: applying ZBDD node", g);
845 }
846
847 return apply(f, g, BC_XOR, 0);
848 }
849
bddnand(f,g)850 bddp bddnand(f, g)
851 bddp f, g;
852 /* Returns bddnull if not enough memory */
853 {
854 bddp h;
855
856 h = bddand(f, g);
857 if(h == bddnull) return bddnull;
858 return B_NOT(h);
859 }
860
bddnor(f,g)861 bddp bddnor(f, g)
862 bddp f, g;
863 /* Returns bddnull if not enough memory */
864 {
865 if(f == bddnull) return bddnull;
866 if(g == bddnull) return bddnull;
867 return bddand(B_NOT(f), B_NOT(g));
868 }
869
bddxnor(f,g)870 bddp bddxnor(f, g)
871 bddp f, g;
872 /* Returns bddnull if not enough memory */
873 {
874 if(g == bddnull) return bddnull;
875 return bddxor(f, B_NOT(g));
876 }
877
bddcofactor(f,g)878 bddp bddcofactor(f, g)
879 bddp f, g;
880 /* Returns bddnull if not enough memory */
881 {
882 struct B_NodeTable *fp;
883
884 /* Check operands */
885 if(f == bddnull) return bddnull;
886 if(g == bddnull) return bddnull;
887 if(B_CST(f))
888 { if(B_ABS(f) != bddfalse) err("bddcofactor: Invalid bddp", f); }
889 else
890 {
891 fp = B_NP(f);
892 if(fp>=Node+NodeSpc || !fp->varrfc)
893 err("bddcofactor: Invalid bddp", f);
894 if(B_Z_NP(fp)) err("bddcofactor: applying ZBDD node", f);
895 }
896 if(B_CST(g))
897 { if(B_ABS(g) != bddfalse) err("bddcofactor: Invalid bddp", g); }
898 else
899 {
900 fp = B_NP(g);
901 if(fp>=Node+NodeSpc || !fp->varrfc)
902 err("bddcofactor: Invalid bddp", g);
903 if(B_Z_NP(fp)) err("bddcofactor: applying ZBDD node", g);
904 }
905
906 return apply(f, g, BC_COFACTOR, 0);
907 }
908
bdduniv(f,g)909 bddp bdduniv(f, g)
910 bddp f, g;
911 /* Returns bddnull if not enough memory */
912 {
913 struct B_NodeTable *fp;
914
915 /* Check operands */
916 if(f == bddnull) return bddnull;
917 if(g == bddnull) return bddnull;
918 if(B_CST(f))
919 { if(B_ABS(f) != bddfalse) err("bdduniv: Invalid bddp", f); }
920 else
921 {
922 fp = B_NP(f);
923 if(fp>=Node+NodeSpc || !fp->varrfc)
924 err("bdduniv: Invalid bddp", f);
925 if(B_Z_NP(fp)) err("bdduniv: applying ZBDD node", f);
926 }
927 if(B_CST(g))
928 { if(B_ABS(g) != bddfalse) err("bdduniv: Invalid bddp", g); }
929 else
930 {
931 fp = B_NP(g);
932 if(fp>=Node+NodeSpc || !fp->varrfc)
933 err("bdduniv: Invalid bddp", g);
934 if(B_Z_NP(fp)) err("bdduniv: applying ZBDD node", g);
935 }
936
937 return apply(f, g, BC_UNIV, 0);
938 }
939
bddexist(f,g)940 bddp bddexist(f, g)
941 bddp f, g;
942 /* Returns bddnull if not enough memory */
943 {
944 bddp h;
945
946 if(f == bddnull) return bddnull;
947 if(g == bddnull) return bddnull;
948 h = bdduniv(B_NOT(f), g);
949 if(h == bddnull) return bddnull;
950 return B_NOT(h);
951 }
952
bddimply(f,g)953 int bddimply(f, g)
954 bddp f, g;
955 {
956 struct B_NodeTable *fp;
957
958 /* Check operands */
959 if(f == bddnull) return 0;
960 if(g == bddnull) return 0;
961 if(B_CST(f))
962 { if(B_ABS(f) != bddfalse) err("bddimply: Invalid bddp", f); }
963 else
964 {
965 fp = B_NP(f);
966 if(fp>=Node+NodeSpc || !fp->varrfc)
967 err("bddimply: Invalid bddp", f);
968 if(B_Z_NP(fp)) err("bddimply: applying ZBDD node", f);
969 }
970 if(B_CST(g))
971 { if(B_ABS(g) != bddfalse) err("bddimply: Invalid bddp", g); }
972 else
973 {
974 fp = B_NP(g);
975 if(fp>=Node+NodeSpc || !fp->varrfc)
976 err("bddimply: Invalid bddp", g);
977 if(B_Z_NP(fp)) err("bddimply: applying ZBDD node", g);
978 }
979
980 return ! andfalse(f, B_NOT(g));
981 }
982
bddsupport(f)983 bddp bddsupport(f)
984 bddp f;
985 /* Returns bddnull if not enough memory */
986 {
987 struct B_NodeTable *fp;
988
989 /* Check operands */
990 if(f == bddnull) return bddnull;
991 if(B_CST(f)) return bddfalse;
992 fp = B_NP(f);
993 if(fp>=Node+NodeSpc || !fp->varrfc)
994 err("bddsupport: Invalid bddp", f);
995
996 return apply(f, bddfalse, BC_SUPPORT, 0);
997 }
998
bddat0(f,v)999 bddp bddat0(f, v)
1000 bddp f;
1001 bddvar v;
1002 /* Returns bddnull if not enough memory */
1003 {
1004 struct B_NodeTable *fp;
1005
1006 /* Check operands */
1007 if(v > VarUsed || v == 0) err("bddat0: Invalid VarID", v);
1008 if(f == bddnull) return bddnull;
1009 if(B_CST(f)) return f;
1010 fp = B_NP(f);
1011 if(fp>=Node+NodeSpc || !fp->varrfc)
1012 err("bddat0: Invalid bddp", f);
1013
1014 return apply(f, (bddp)v, BC_AT0, 0);
1015 }
1016
bddat1(f,v)1017 bddp bddat1(f, v)
1018 bddp f;
1019 bddvar v;
1020 /* Returns bddnull if not enough memory */
1021 {
1022 struct B_NodeTable *fp;
1023
1024 /* Check operands */
1025 if(v > VarUsed || v == 0) err("bddat1: Invalid VarID", v);
1026 if(f == bddnull) return bddnull;
1027 if(B_CST(f)) return f;
1028 fp = B_NP(f);
1029 if(fp>=Node+NodeSpc || !fp->varrfc)
1030 err("bddat1: Invalid bddp", f);
1031
1032 return apply(f, (bddp)v, BC_AT1, 0);
1033 }
1034
bddlshift(f,shift)1035 bddp bddlshift(f, shift)
1036 bddp f;
1037 bddvar shift;
1038 /* Returns bddnull if not enough memory */
1039 {
1040 struct B_NodeTable *fp;
1041 bddvar flev;
1042
1043 /* Check operands */
1044 if(shift >= VarUsed)
1045 err("bddlshift: Invalid shift", shift);
1046 if(f == bddnull) return bddnull;
1047 if(B_CST(f)) return f;
1048 if(shift == 0) return bddcopy(f);
1049 if((fp=B_NP(f))>=Node+NodeSpc || !fp->varrfc)
1050 err("bddlshift: Invalid bddp", f);
1051
1052 return apply(f, (bddp)shift, BC_LSHIFT, 0);
1053 }
1054
bddrshift(f,shift)1055 bddp bddrshift(f, shift)
1056 bddp f;
1057 bddvar shift;
1058 /* Returns bddnull if not enough memory */
1059 {
1060 struct B_NodeTable *fp;
1061 bddvar flev;
1062
1063 /* Check operands */
1064 if(shift >= VarUsed)
1065 err("bddrshift: Invalid shift", shift);
1066 if(f == bddnull) return bddnull;
1067 if(B_CST(f)) return f;
1068 if(shift == 0) return bddcopy(f);
1069 if((fp=B_NP(f))>=Node+NodeSpc || !fp->varrfc)
1070 err("bddrshift: Invalid bddp", f);
1071
1072 return apply(f, (bddp)shift, BC_RSHIFT, 0);
1073 }
1074
bddoffset(f,v)1075 bddp bddoffset(f, v)
1076 bddp f;
1077 bddvar v;
1078 /* Returns bddnull if not enough memory */
1079 {
1080 struct B_NodeTable *fp;
1081
1082 /* Check operands */
1083 if(v > VarUsed || v == 0) err("bddoffset: Invalid VarID", v);
1084 if(f == bddnull) return bddnull;
1085 if(B_CST(f)) return f;
1086 fp = B_NP(f);
1087 if(fp>=Node+NodeSpc || !fp->varrfc)
1088 err("bddoffset: Invalid bddp", f);
1089 if(!B_Z_NP(fp)) err("bddoffset: applying non-ZBDD node", f);
1090
1091 return apply(f, (bddp)v, BC_OFFSET, 0);
1092 }
1093
bddonset0(f,v)1094 bddp bddonset0(f, v)
1095 bddp f;
1096 bddvar v;
1097 /* Returns bddnull if not enough memory */
1098 {
1099 struct B_NodeTable *fp;
1100
1101 /* Check operands */
1102 if(v > VarUsed || v == 0) err("bddonset0: Invalid VarID", v);
1103 if(f == bddnull) return bddnull;
1104 if(B_CST(f)) return bddfalse;
1105 fp = B_NP(f);
1106 if(fp>=Node+NodeSpc || !fp->varrfc)
1107 err("bddonset0: Invalid bddp", f);
1108 if(!B_Z_NP(fp)) err("bddonset0: applying non-ZBDD node", f);
1109
1110 return apply(f, (bddp)v, BC_ONSET, 0);
1111 }
1112
bddonset(f,v)1113 bddp bddonset(f, v)
1114 bddp f;
1115 bddvar v;
1116 /* Returns bddnull if not enough memory */
1117 {
1118 bddp g, h;
1119
1120 g = bddonset0(f, v);
1121 h = bddchange(g, v);
1122 bddfree(g);
1123 return h;
1124 }
1125
bddchange(f,v)1126 bddp bddchange(f, v)
1127 bddp f;
1128 bddvar v;
1129 /* Returns bddnull if not enough memory */
1130 {
1131 struct B_NodeTable *fp;
1132
1133 /* Check operands */
1134 if(v > VarUsed || v == 0) err("bddchange: Invalid VarID", v);
1135 if(f == bddnull) return bddnull;
1136 if(!B_CST(f))
1137 {
1138 fp = B_NP(f);
1139 if(fp>=Node+NodeSpc || !fp->varrfc)
1140 err("bddchange: Invalid bddp", f);
1141 if(!B_Z_NP(fp)) err("bddchange: applying non-ZBDD node", f);
1142 }
1143
1144 return apply(f, (bddp)v, BC_CHANGE, 0);
1145 }
1146
bddintersec(f,g)1147 bddp bddintersec(f, g)
1148 bddp f, g;
1149 /* Returns bddnull if not enough memory */
1150 {
1151 struct B_NodeTable *fp;
1152
1153 /* Check operands */
1154 if(f == bddnull) return bddnull;
1155 if(g == bddnull) return bddnull;
1156 if(B_CST(f))
1157 { if(B_ABS(f) != bddfalse) err("bddintersec: Invalid bddp", f); }
1158 else
1159 {
1160 fp = B_NP(f);
1161 if(fp>=Node+NodeSpc || !fp->varrfc)
1162 err("bddintersec: Invalid bddp", f);
1163 if(!B_Z_NP(fp)) err("bddintersec: applying non-ZBDD node", f);
1164 }
1165 if(B_CST(g))
1166 { if(B_ABS(g) != bddfalse) err("bddintersec: Invalid bddp", g); }
1167 else
1168 {
1169 fp = B_NP(g);
1170 if(fp>=Node+NodeSpc || !fp->varrfc)
1171 err("bddintersec: Invalid bddp", g);
1172 if(!B_Z_NP(fp)) err("bddintersec: applying non-ZBDD node", g);
1173 }
1174
1175 return apply(f, g, BC_INTERSEC, 0);
1176 }
1177
bddunion(f,g)1178 bddp bddunion(f, g)
1179 bddp f, g;
1180 /* Returns bddnull if not enough memory */
1181 {
1182 struct B_NodeTable *fp;
1183
1184 /* Check operands */
1185 if(f == bddnull) return bddnull;
1186 if(g == bddnull) return bddnull;
1187 if(B_CST(f))
1188 { if(B_ABS(f) != bddfalse) err("bddunion: Invalid bddp", f); }
1189 else
1190 {
1191 fp = B_NP(f);
1192 if(fp>=Node+NodeSpc || !fp->varrfc)
1193 err("bddunion: Invalid bddp", f);
1194 if(!B_Z_NP(fp)) err("bddunion: applying non-ZBDD node", f);
1195 }
1196 if(B_CST(g))
1197 { if(B_ABS(g) != bddfalse) err("bddunion: Invalid bddp", g); }
1198 else
1199 {
1200 fp = B_NP(g);
1201 if(fp>=Node+NodeSpc || !fp->varrfc)
1202 err("bddunion: Invalid bddp", g);
1203 if(!B_Z_NP(fp)) err("bddunion: applying non-ZBDD node", g);
1204 }
1205
1206 return apply(f, g, BC_UNION, 0);
1207 }
1208
bddsubtract(f,g)1209 bddp bddsubtract(f, g)
1210 bddp f, g;
1211 /* Returns bddnull if not enough memory */
1212 {
1213 struct B_NodeTable *fp;
1214
1215 /* Check operands */
1216 if(f == bddnull) return bddnull;
1217 if(g == bddnull) return bddnull;
1218 if(B_CST(f))
1219 { if(B_ABS(f) != bddfalse) err("bddsubtract: Invalid bddp", f); }
1220 else
1221 {
1222 fp = B_NP(f);
1223 if(fp>=Node+NodeSpc || !fp->varrfc)
1224 err("bddsubtarct: Invalid bddp", f);
1225 if(!B_Z_NP(fp)) err("bddsubtarct: applying non-ZBDD node", f);
1226 }
1227 if(B_CST(g))
1228 { if(B_ABS(g) != bddfalse) err("bddsubtarct: Invalid bddp", g); }
1229 else
1230 {
1231 fp = B_NP(g);
1232 if(fp>=Node+NodeSpc || !fp->varrfc)
1233 err("bddsubtarct: Invalid bddp", g);
1234 if(!B_Z_NP(fp)) err("bddsubtarct: applying non-ZBDD node", g);
1235 }
1236
1237 return apply(f, g, BC_SUBTRACT, 0);
1238 }
1239
bddcard(f)1240 bddp bddcard(f)
1241 bddp f;
1242 {
1243 struct B_NodeTable *fp;
1244
1245 if(f == bddnull) return 0;
1246 if(B_CST(f)) return (f == bddempty)? 0: 1;
1247 fp = B_NP(f);
1248 if(fp>=Node+NodeSpc || !fp->varrfc)
1249 err("bddcard: Invalid bddp", f);
1250 if(!B_Z_NP(fp)) err("bddcard: applying non-ZBDD node", f);
1251
1252 return apply(f, bddempty, BC_CARD, 0);
1253 }
1254
bddlit(f)1255 bddp bddlit(f)
1256 bddp f;
1257 {
1258 struct B_NodeTable *fp;
1259
1260 if(f == bddnull) return 0;
1261 if(B_CST(f)) return 0;
1262 fp = B_NP(f);
1263 if(fp>=Node+NodeSpc || !fp->varrfc)
1264 err("bddlit: Invalid bddp", f);
1265 if(!B_Z_NP(fp)) err("bddlit: applying non-ZBDD node", f);
1266
1267 return apply(f, bddempty, BC_LIT, 0);
1268 }
1269
bddlen(f)1270 bddp bddlen(f)
1271 bddp f;
1272 {
1273 struct B_NodeTable *fp;
1274
1275 if(f == bddnull) return 0;
1276 if(B_CST(f)) return 0;
1277 fp = B_NP(f);
1278 if(fp>=Node+NodeSpc || !fp->varrfc)
1279 err("bddlen: Invalid bddp", f);
1280 if(!B_Z_NP(fp)) err("bddlen: applying non-ZBDD node", f);
1281
1282 return apply(f, bddempty, BC_LEN, 0);
1283 }
1284
1285
1286
1287 /* ----------------- Internal functions ------------------ */
var_enlarge()1288 static void var_enlarge()
1289 {
1290 bddvar i, newSpc;
1291 struct B_VarTable *newVar;
1292 unsigned int *newVarID;
1293
1294 /* Get new size */
1295 if(VarSpc == bddvarmax+1U)
1296 err("var_enlarge: var index range full", VarSpc);
1297 newSpc = VarSpc << 2U;
1298 if(newSpc > bddvarmax+1) newSpc = bddvarmax+1U;
1299
1300 /* Enlarge space */
1301 newVar = B_MALLOC(struct B_VarTable, newSpc);
1302 newVarID = B_MALLOC(unsigned int, newSpc);
1303 if(newVar && newVarID)
1304 {
1305 for(i=0; i<VarSpc; i++)
1306 {
1307 newVar[i].hashSpc = Var[i].hashSpc;
1308 newVar[i].hashUsed = Var[i].hashUsed;
1309 newVar[i].lev = Var[i].lev;
1310 newVar[i].hash_32 = Var[i].hash_32;
1311 newVarID[i] = VarID[i];
1312 #ifdef B_64
1313 newVar[i].hash_h8 = Var[i].hash_h8;
1314 #endif
1315 }
1316 free(Var);
1317 free(VarID);
1318 Var = newVar;
1319 VarID = newVarID;
1320 }
1321 else
1322 {
1323 if(newVar) free(newVar);
1324 if(newVarID) free(newVarID);
1325 err("var_enlarge: memory allocation failed", VarSpc);
1326 }
1327
1328 /* Initialize new space */
1329 for(i=VarSpc; i<newSpc; i++)
1330 {
1331 Var[i].hashSpc = 0;
1332 Var[i].hashUsed = 0;
1333 Var[i].lev = i;
1334 Var[i].hash_32 = 0;
1335 VarID[i] = i;
1336 #ifdef B_64
1337 Var[i].hash_h8 = 0;
1338 #endif
1339 }
1340 VarSpc = newSpc;
1341 }
1342
node_enlarge()1343 static int node_enlarge()
1344 /* Returns 1 if not enough memory */
1345 {
1346 bddp i, newSpc;
1347 struct B_NodeTable *newNode;
1348 struct B_CacheTable *newCache, *cp, *cp1;
1349
1350 /* Get new size */
1351 if(NodeSpc == NodeLimit) return 1; /* Cannot enlarge */
1352 newSpc = NodeSpc << 1U;
1353 if(newSpc > NodeLimit) newSpc = NodeLimit;
1354
1355 /* Enlarge space */
1356 newNode = B_MALLOC(struct B_NodeTable, newSpc);
1357 if(newNode)
1358 {
1359 for(i=0; i<NodeSpc; i++)
1360 {
1361 newNode[i].varrfc = Node[i].varrfc;
1362 newNode[i].f0_32 = Node[i].f0_32;
1363 newNode[i].f1_32 = Node[i].f1_32;
1364 newNode[i].nx_32 = Node[i].nx_32;
1365 #ifdef B_64
1366 newNode[i].f0_h8 = Node[i].f0_h8;
1367 newNode[i].f1_h8 = Node[i].f1_h8;
1368 newNode[i].nx_h8 = Node[i].nx_h8;
1369 #endif /* B_64 */
1370 }
1371 free(Node);
1372 Node = newNode;
1373 }
1374 else return 1; /* Not enough memory */
1375
1376 /* Initialize new space */
1377 Node[newSpc-1U].varrfc = 0;
1378 B_SET_BDDP(Node[newSpc-1U].nx, Avail);
1379 for(i=NodeSpc; i<newSpc-1U; i++)
1380 {
1381 Node[i].varrfc = 0;
1382 B_SET_BDDP(Node[i].nx, i+1U);
1383 }
1384 Avail = NodeSpc;
1385 NodeSpc = newSpc;
1386
1387 /* Realloc Cache */
1388 for(newSpc=CacheSpc; newSpc<NodeSpc>>1U; newSpc<<=1U)
1389 ; /* empty */
1390 newCache = B_MALLOC(struct B_CacheTable, newSpc);
1391 if(newCache)
1392 {
1393 for(i=0; i<CacheSpc; i++)
1394 {
1395 cp = newCache + i;
1396 cp1 = Cache + i;
1397 cp->op = cp1->op;
1398 B_CPY_BDDP(cp->f, cp1->f);
1399 B_CPY_BDDP(cp->g, cp1->g);
1400 B_CPY_BDDP(cp->h, cp1->h);
1401 }
1402 free(Cache);
1403 Cache = newCache;
1404 }
1405 else return 0; /* Only NodeTable enlarged */
1406
1407 /* Reconstruct Cache */
1408 for(i=CacheSpc; i<newSpc; i++)
1409 {
1410 cp = Cache + i;
1411 cp1 = Cache + (i & (CacheSpc - 1));
1412 cp->op = cp1->op;
1413 B_CPY_BDDP(cp->f, cp1->f);
1414 B_CPY_BDDP(cp->g, cp1->g);
1415 B_CPY_BDDP(cp->h, cp1->h);
1416 }
1417 CacheSpc = newSpc;
1418
1419 return 0;
1420 }
1421
hash_enlarge(v)1422 static int hash_enlarge(v)
1423 bddvar v;
1424 /* Returns 1 if not enough memory */
1425 {
1426 struct B_NodeTable *np, *np0;
1427 struct B_VarTable *varp;
1428 bddp i, oldSpc, newSpc, nx, key, f0, f1;
1429 bddp_32 *newhash_32, *p_32;
1430 #ifdef B_64
1431 bddp_h8 *newhash_h8, *p_h8;
1432 #endif
1433
1434 varp = &Var[v];
1435 /* Get new size */
1436 oldSpc = varp->hashSpc;
1437 if(oldSpc == B_NODE_MAX + 1U)
1438 return 0; /* Cancel enlarging */
1439 newSpc = oldSpc << 1U;
1440
1441 /* Enlarge space */
1442 #ifdef B_64
1443 newhash_32 = B_MALLOC(bddp_32, newSpc);
1444 newhash_h8 = B_MALLOC(bddp_h8, newSpc);
1445 if(newhash_32 && newhash_h8)
1446 {
1447 for(i=0; i<varp->hashSpc; i++)
1448 {
1449 newhash_32[i] = varp->hash_32[i];
1450 newhash_h8[i] = varp->hash_h8[i];
1451 }
1452 free(varp->hash_32);
1453 free(varp->hash_h8);
1454 varp->hash_32 = newhash_32;
1455 varp->hash_h8 = newhash_h8;
1456 }
1457 else
1458 {
1459 if(newhash_32) free(newhash_32);
1460 if(newhash_h8) free(newhash_h8);
1461 return 1;
1462 }
1463 #else
1464 newhash_32 = B_MALLOC(bddp_32, newSpc);
1465 if(newhash_32)
1466 {
1467 for(i=0; i<varp->hashSpc; i++) newhash_32[i] = varp->hash_32[i];
1468 free(varp->hash_32);
1469 varp->hash_32 = newhash_32;
1470 }
1471 else return 1; /* Not enough memory */
1472 #endif
1473 varp->hashSpc = newSpc;
1474
1475 /* Initialize new hash entry */
1476 for(i=oldSpc; i<newSpc; i++)
1477 {
1478 B_SET_NXP(p, varp->hash, i);
1479 B_SET_BDDP(*p, bddnull);
1480 }
1481
1482 /* restore hash entry */
1483 for(i=0; i<oldSpc; i++)
1484 {
1485 np0 = 0;
1486 B_SET_NXP(p, varp->hash, i);
1487 nx = B_GET_BDDP(*p);
1488 while(nx != bddnull)
1489 {
1490 np = Node + nx;
1491 f0 = B_GET_BDDP(np->f0);
1492 f1 = B_GET_BDDP(np->f1);
1493 key = B_HASHKEY(f0, f1, newSpc);
1494 if(key == i) np0 = np;
1495 else
1496 {
1497 if(np0) B_CPY_BDDP(np0->nx, np->nx);
1498 else { B_SET_NXP(p, varp->hash, i); B_CPY_BDDP(*p, np->nx); }
1499 B_SET_NXP(p, varp->hash, key);
1500 B_CPY_BDDP(np->nx, *p);
1501 B_SET_BDDP(*p, nx);
1502 }
1503 if(np0) nx = B_GET_BDDP(np0->nx);
1504 else { B_SET_NXP(p, varp->hash, i); nx = B_GET_BDDP(*p); }
1505 }
1506 }
1507 return 0;
1508 }
1509
getnode(v,f0,f1)1510 static bddp getnode(v, f0, f1)
1511 bddvar v;
1512 bddp f0, f1;
1513 /* Returns bddnull if not enough memory */
1514 {
1515 /* After checking elimination rule & negative edge rule */
1516 struct B_NodeTable *np, *fp;
1517 struct B_VarTable *varp;
1518 bddp ix, nx, key;
1519 bddp_32 *p_32;
1520 #ifdef B_64
1521 bddp_h8 *p_h8;
1522 #endif
1523
1524 varp = &Var[v];
1525 if(varp->hashSpc == 0)
1526 /* Create hash-table */
1527 {
1528 varp->hash_32 = B_MALLOC(bddp_32, B_HASH_SPC0);
1529 if(!varp->hash_32) return bddnull;
1530 #ifdef B_64
1531 varp->hash_h8 = B_MALLOC(bddp_h8, B_HASH_SPC0);
1532 if(!varp->hash_h8)
1533 {
1534 free(varp->hash_32);
1535 return bddnull;
1536 }
1537 #endif
1538 for(ix=0; ix<B_HASH_SPC0; ix++)
1539 {
1540 B_SET_NXP(p, varp->hash, ix);
1541 B_SET_BDDP(*p, bddnull);
1542 }
1543 varp->hashSpc = B_HASH_SPC0;
1544 key = B_HASHKEY(f0, f1, varp->hashSpc);
1545 }
1546 else
1547 /* Looking for equivalent existing node */
1548 {
1549 key = B_HASHKEY(f0, f1, varp->hashSpc);
1550 B_SET_NXP(p, varp->hash, key);
1551 nx = B_GET_BDDP(*p);
1552 while(nx != bddnull)
1553 {
1554 np = Node + nx;
1555 if(f0 == B_GET_BDDP(np->f0) &&
1556 f1 == B_GET_BDDP(np->f1) )
1557 {
1558 /* Sharing equivalent node */
1559 if(!B_CST(f0)) { fp = B_NP(f0); B_RFC_DEC_NP(fp); }
1560 if(!B_CST(f1)) { fp = B_NP(f1); B_RFC_DEC_NP(fp); }
1561 B_RFC_INC_NP(np);
1562 return B_BDDP_NP(np);
1563 }
1564 nx = B_GET_BDDP(np->nx);
1565 }
1566 }
1567
1568 /* Check hash-table overflow */
1569 if(++ varp->hashUsed >= varp->hashSpc)
1570 {
1571 if(hash_enlarge(v)) return bddnull; /* Hash-table overflow */
1572 key = B_HASHKEY(f0, f1, varp->hashSpc); /* Enlarge success */
1573 }
1574
1575 /* Check node-table overflow */
1576 if(NodeUsed >= NodeSpc-1U)
1577 {
1578 if(node_enlarge())
1579 {
1580 if(bddgc()) return bddnull; /* Node-table overflow */
1581 key = B_HASHKEY(f0, f1, varp->hashSpc);
1582 }
1583 /* Node-table enlarged or GC succeeded */
1584 }
1585 NodeUsed++;
1586
1587 /* Creating a new node */
1588 nx = Avail;
1589 np = Node + nx;
1590 Avail = B_GET_BDDP(np->nx);
1591 B_SET_NXP(p, varp->hash, key);
1592 B_CPY_BDDP(np->nx, *p);
1593 B_SET_BDDP(*p, nx);
1594 B_SET_BDDP(np->f0, f0);
1595 B_SET_BDDP(np->f1, f1);
1596 np->varrfc = v;
1597 B_RFC_INC_NP(np);
1598 return B_BDDP_NP(np);
1599 }
1600
getbddp(v,f0,f1)1601 static bddp getbddp(v, f0, f1)
1602 bddvar v;
1603 bddp f0, f1;
1604 /* Returns bddnull if not enough memory */
1605 {
1606 struct B_NodeTable *fp;
1607
1608 /* Check elimination rule */
1609 if(f0 == f1)
1610 {
1611 if(!B_CST(f0)) { fp = B_NP(f0); B_RFC_DEC_NP(fp); }
1612 return f0;
1613 }
1614
1615 /* Negative edge constraint */
1616 if(B_NEG(f0))
1617 {
1618 bddp h;
1619
1620 h = getnode(v, B_NOT(f0), B_NOT(f1));
1621 if(h == bddnull) return bddnull;
1622 return B_NOT(h);
1623 }
1624 return getnode(v, f0, f1);
1625 }
1626
apply(f,g,op,skip)1627 static bddp apply(f, g, op, skip)
1628 bddp f, g;
1629 unsigned char op, skip;
1630 /* Returns bddnull if not enough memory */
1631 {
1632 struct B_NodeTable *fp, *gp;
1633 struct B_CacheTable *cachep;
1634 bddp key, f0, f1, g0, g1, h0, h1, h;
1635 bddvar v, flev, glev;
1636 char z; /* flag to check ZBDD node */
1637
1638 /* Check terminal case */
1639 if(!skip) switch(op)
1640 {
1641 case BC_AND:
1642 /* Check trivial cases */
1643 if(f == bddfalse || g == bddfalse || f == B_NOT(g))
1644 return bddfalse;
1645 if(f == g)
1646 {
1647 if(f != bddtrue) { fp = B_NP(f); B_RFC_INC_NP(fp); }
1648 return f;
1649 }
1650 if(f == bddtrue) { fp = B_NP(g); B_RFC_INC_NP(fp); return g; }
1651 if(g == bddtrue) { fp = B_NP(f); B_RFC_INC_NP(fp); return f; }
1652 /* Check operand swap */
1653 if(f < g) { h = f; f = g; g = h; } /* swap (f, g) */
1654 break;
1655
1656 case BC_XOR:
1657 /* Check trivial cases */
1658 if(f == g) return bddfalse;
1659 if(f == B_NOT(g)) return bddtrue;
1660 if(f == bddfalse) { fp = B_NP(g); B_RFC_INC_NP(fp); return g; }
1661 if(g == bddfalse) { fp = B_NP(f); B_RFC_INC_NP(fp); return f; }
1662 if(f == bddtrue) {fp=B_NP(g); B_RFC_INC_NP(fp); return B_NOT(g);}
1663 if(g == bddtrue) {fp=B_NP(f); B_RFC_INC_NP(fp); return B_NOT(f);}
1664 /* Check negation */
1665 if(B_NEG(f) && B_NEG(g)) { f = B_NOT(f); g = B_NOT(g); }
1666 else if(B_NEG(f) || B_NEG(g))
1667 {
1668 f = B_ABS(f); g = B_ABS(g);
1669 /* Check operand swap */
1670 h = (f < g)? apply(g, f, op, 1): apply(f, g, op, 1);
1671 if(h == bddnull) return bddnull;
1672 return B_NOT(h);
1673 }
1674 /* Check operand swap */
1675 if(f < g) { h = f; f = g; g = h; } /* swap (f, g) */
1676 break;
1677
1678 case BC_COFACTOR:
1679 /* Check trivial cases */
1680 if(B_CST(f)) return f;
1681 if(g == bddfalse || f == B_NOT(g)) return bddfalse;
1682 if(f == g) return bddtrue;
1683 if(g == bddtrue) { fp = B_NP(f); B_RFC_INC_NP(fp); return f; }
1684 break;
1685
1686 case BC_UNIV:
1687 /* Check trivial cases */
1688 if(B_CST(f)) return f;
1689 if(B_CST(g)) { fp = B_NP(f); B_RFC_INC_NP(fp); return f; }
1690 if(B_NEG(g)) g = B_NOT(g);
1691 break;
1692
1693 case BC_SUPPORT:
1694 if(B_CST(f)) return bddfalse;
1695 if(B_NEG(f)) f = B_NOT(f);
1696 break;
1697
1698 case BC_INTERSEC:
1699 /* Check trivial cases */
1700 if(f == bddfalse || g == bddfalse) return bddfalse;
1701 if(f == bddtrue) return B_NEG(g)? bddtrue: bddfalse;
1702 if(g == bddtrue) return B_NEG(f)? bddtrue: bddfalse;
1703 if(f == g) { fp = B_NP(f); B_RFC_INC_NP(fp); return f; }
1704 if(f == B_NOT(g)) {fp=B_NP(f); B_RFC_INC_NP(fp); return B_ABS(f); }
1705 /* Check operand swap */
1706 if(f < g) { h = f; f = g; g = h; } /* swap (f, g) */
1707 break;
1708
1709 case BC_UNION:
1710 /* Check trivial cases */
1711 if(f == bddfalse)
1712 {
1713 if(!B_CST(g)) {fp=B_NP(g); B_RFC_INC_NP(fp); }
1714 return g;
1715 }
1716 if(f == bddtrue)
1717 {
1718 if(!B_CST(g)) {fp=B_NP(g); B_RFC_INC_NP(fp); }
1719 return B_NEG(g)? g: B_NOT(g);
1720 }
1721 if(g == bddfalse || f == g)
1722 { fp=B_NP(f); B_RFC_INC_NP(fp); return f; }
1723 if(g == bddtrue || f == B_NOT(g))
1724 {
1725 fp=B_NP(f); B_RFC_INC_NP(fp);
1726 return B_NEG(f)? f: B_NOT(f);
1727 }
1728 /* Check operand swap */
1729 if(f < g) { h = f; f = g; g = h; } /* swap (f, g) */
1730 break;
1731
1732 case BC_SUBTRACT:
1733 /* Check trivial cases */
1734 if(f == bddfalse || f == g) return bddfalse;
1735 if(f == bddtrue || f == B_NOT(g))
1736 return B_NEG(g)? bddfalse: bddtrue;
1737 if(g == bddfalse) { fp=B_NP(f); B_RFC_INC_NP(fp); return f; }
1738 if(g == bddtrue) { fp=B_NP(f); B_RFC_INC_NP(fp); return B_ABS(f); }
1739 break;
1740
1741 case BC_AT0:
1742 case BC_AT1:
1743 case BC_OFFSET:
1744 /* Check trivial cases */
1745 if(B_CST(f)) return f;
1746 /* special cases */
1747 fp = B_NP(f); flev = Var[B_VAR_NP(fp)].lev;
1748 glev = Var[(bddvar)g].lev;
1749 if(flev < glev) { B_RFC_INC_NP(fp); return f; }
1750 if(flev == glev)
1751 {
1752 if(op != BC_AT1)
1753 {
1754 h = B_GET_BDDP(fp->f0);
1755 if(B_NEG(f)^B_NEG(h)) h = B_NOT(h);
1756 }
1757 else
1758 {
1759 h = B_GET_BDDP(fp->f1);
1760 if(B_NEG(f)) h = B_NOT(h);
1761 }
1762 if(!B_CST(h)) { fp = B_NP(h); B_RFC_INC_NP(fp); }
1763 return h;
1764 }
1765 /* Check negation */
1766 if(B_NEG(f))
1767 {
1768 h = apply(B_NOT(f), g, op, 1);
1769 if(h == bddnull) return bddnull;
1770 return B_NOT(h);
1771 }
1772 break;
1773
1774 case BC_ONSET:
1775 /* Check trivial cases */
1776 if(B_CST(f)) return bddfalse;
1777 /* special cases */
1778 fp = B_NP(f); flev = Var[B_VAR_NP(fp)].lev;
1779 glev = Var[(bddvar)g].lev;
1780 if(flev < glev) return bddfalse;
1781 if(flev == glev)
1782 {
1783 h = B_GET_BDDP(fp->f1);
1784 if(!B_CST(h)) { fp = B_NP(h); B_RFC_INC_NP(fp); }
1785 return h;
1786 }
1787 /* Check negation */
1788 if(B_NEG(f)) f = B_NOT(f);
1789 break;
1790
1791 case BC_CHANGE:
1792 /* Check trivial cases */
1793 if(f == bddfalse) return f;
1794 if(B_CST(f)) return getzbddp((bddvar)g, bddfalse, f);
1795 /* special cases */
1796 fp = B_NP(f); flev = Var[B_VAR_NP(fp)].lev;
1797 glev = Var[(bddvar)g].lev;
1798 if(flev < glev)
1799 {
1800 B_RFC_INC_NP(fp);
1801 h = getzbddp((bddvar)g, bddfalse, f);
1802 if(h == bddnull) bddfree(f);
1803 return h;
1804 }
1805 if(flev == glev)
1806 {
1807 h0 = B_GET_BDDP(fp->f1);
1808 h1 = B_GET_BDDP(fp->f0);
1809 if(B_NEG(f)^B_NEG(h1)) h1 = B_NOT(h1);
1810 if(!B_CST(h0)) { fp = B_NP(h0); B_RFC_INC_NP(fp); }
1811 if(!B_CST(h1)) { fp = B_NP(h1); B_RFC_INC_NP(fp); }
1812 h = getzbddp((bddvar)g, h0, h1);
1813 if(h == bddnull) { bddfree(h0); bddfree(h1); }
1814 return h;
1815 }
1816 break;
1817
1818 case BC_LSHIFT:
1819 case BC_RSHIFT:
1820 /* Check trivial cases */
1821 if(B_CST(f)) return f;
1822
1823 /* Check negation */
1824 if(B_NEG(f))
1825 {
1826 h = apply(B_NOT(f), g, op, 1);
1827 if(h == bddnull) return bddnull;
1828 return B_NOT(h);
1829 }
1830 break;
1831
1832 case BC_CARD:
1833 if(B_CST(f)) return (f == bddempty)? 0: 1;
1834 if(B_NEG(f)) return apply(B_NOT(f), bddempty, op, 1) + 1;
1835 break;
1836
1837 case BC_LIT:
1838 if(B_CST(f)) return 0;
1839 if(B_NEG(f)) f = B_NOT(f);
1840 break;
1841
1842 case BC_LEN:
1843 if(B_CST(f)) return 0;
1844 if(B_NEG(f)) f = B_NOT(f);
1845 break;
1846
1847 default:
1848 err("apply: unknown opcode", op);
1849 break;
1850 }
1851
1852 /* Non-trivial operations */
1853 switch(op)
1854 {
1855 /* binary operation */
1856 case BC_AND:
1857 case BC_XOR:
1858 case BC_COFACTOR:
1859 case BC_UNIV:
1860 case BC_INTERSEC:
1861 case BC_UNION:
1862 case BC_SUBTRACT:
1863 /* Try cache? */
1864 if((B_CST(f) || B_RFC_ONE_NP(B_NP(f))) &&
1865 (B_CST(g) || B_RFC_ONE_NP(B_NP(g)))) key = bddnull;
1866 else
1867 {
1868 /* Checking Cache */
1869 key = B_CACHEKEY(op, f, g);
1870 cachep = Cache + key;
1871 if(cachep->op == op &&
1872 f == B_GET_BDDP(cachep->f) &&
1873 g == B_GET_BDDP(cachep->g))
1874 {
1875 /* Hit */
1876 h = B_GET_BDDP(cachep->h);
1877 if(!B_CST(h) && h != bddnull) { fp = B_NP(h); B_RFC_INC_NP(fp); }
1878 return h;
1879 }
1880 }
1881 /* Get (f0, f1) and (g0, g1)*/
1882 z = 0;
1883 fp = B_NP(f);
1884 flev = B_CST(f)? 0: Var[B_VAR_NP(fp)].lev;
1885 gp = B_NP(g);
1886 glev = B_CST(g)? 0: Var[B_VAR_NP(gp)].lev;
1887 f0 = f; f1 = f;
1888 g0 = g; g1 = g;
1889
1890 if(flev <= glev)
1891 {
1892 v = B_VAR_NP(gp);
1893 if(B_Z_NP(gp))
1894 {
1895 z = 1;
1896 if(flev < glev) f1 = bddfalse;
1897 }
1898 g0 = B_GET_BDDP(gp->f0);
1899 g1 = B_GET_BDDP(gp->f1);
1900 if(B_NEG(g)^B_NEG(g0)) g0 = B_NOT(g0);
1901 if(B_NEG(g) && !z) g1 = B_NOT(g1);
1902 }
1903
1904 if(flev >= glev)
1905 {
1906 v = B_VAR_NP(fp);
1907 if(B_Z_NP(fp))
1908 {
1909 z = 1;
1910 if(flev > glev) g1 = bddfalse;
1911 }
1912 f0 = B_GET_BDDP(fp->f0);
1913 f1 = B_GET_BDDP(fp->f1);
1914 if(B_NEG(f)^B_NEG(f0)) f0 = B_NOT(f0);
1915 if(B_NEG(f) && !z) f1 = B_NOT(f1);
1916 }
1917 break;
1918
1919 /* unary operation */
1920 case BC_AT0:
1921 case BC_AT1:
1922 case BC_LSHIFT:
1923 case BC_RSHIFT:
1924 case BC_SUPPORT:
1925 case BC_OFFSET:
1926 case BC_ONSET:
1927 case BC_CHANGE:
1928 fp = B_NP(f);
1929 if(B_RFC_ONE_NP(fp)) key = bddnull;
1930 else
1931 {
1932 /* Checking Cache */
1933 key = B_CACHEKEY(op, f, g);
1934 cachep = Cache + key;
1935 if(cachep->op == op &&
1936 f == B_GET_BDDP(cachep->f) &&
1937 g == B_GET_BDDP(cachep->g))
1938 {
1939 /* Hit */
1940 h = B_GET_BDDP(cachep->h);
1941 if(!B_CST(h) && h != bddnull) { fp = B_NP(h); B_RFC_INC_NP(fp); }
1942 return h;
1943 }
1944 }
1945 /* Get (f0, f1)*/
1946 v = B_VAR_NP(fp);
1947 z = B_Z_NP(fp)? 1: 0;
1948 f0 = B_GET_BDDP(fp->f0);
1949 f1 = B_GET_BDDP(fp->f1);
1950 if(B_NEG(f)^B_NEG(f0)) f0 = B_NOT(f0);
1951 if(B_NEG(f) && !z) f1 = B_NOT(f1);
1952 break;
1953
1954 case BC_CARD:
1955 case BC_LIT:
1956 case BC_LEN:
1957 fp = B_NP(f);
1958 if(B_RFC_ONE_NP(fp)) key = bddnull;
1959 else
1960 {
1961 /* Checking Cache */
1962 key = B_CACHEKEY(op, f, bddempty);
1963 cachep = Cache + key;
1964 if(cachep->op == op &&
1965 f == B_GET_BDDP(cachep->f) &&
1966 bddempty == B_GET_BDDP(cachep->g))
1967 {
1968 /* Hit */
1969 return B_GET_BDDP(cachep->h);
1970 }
1971 }
1972 /* Get (f0, f1)*/
1973 f0 = B_GET_BDDP(fp->f0);
1974 f1 = B_GET_BDDP(fp->f1);
1975 if(B_NEG(f)^B_NEG(f0)) f0 = B_NOT(f0);
1976 break;
1977
1978 default:
1979 err("apply: unknown opcode", op);
1980 }
1981
1982 /* Stack overflow limitter */
1983 BDD_RECUR_INC;
1984
1985 /* Get result node */
1986 switch(op)
1987 {
1988 case BC_AND:
1989 case BC_XOR:
1990 case BC_INTERSEC:
1991 case BC_UNION:
1992 case BC_SUBTRACT:
1993 h0 = apply(f0, g0, op, 0);
1994 if(h0 == bddnull) { h = h0; break; } /* Overflow */
1995 h1 = apply(f1, g1, op, 0);
1996 if(h1 == bddnull) { bddfree(h0); h = h1; break; } /* Overflow */
1997 h = z? getzbddp(v, h0, h1): getbddp(v, h0, h1);
1998 if(h == bddnull) { bddfree(h0); bddfree(h1); } /* Overflow */
1999 break;
2000
2001 case BC_COFACTOR:
2002 if(g0 == bddfalse && g1 != bddfalse)
2003 {
2004 h = apply(f1, g1, op, 0);
2005 }
2006 else if(g1 == bddfalse && g0 != bddfalse)
2007 {
2008 h = apply(f0, g0, op, 0);
2009 }
2010 else
2011 {
2012 h0 = apply(f0, g0, op, 0);
2013 if(h0 == bddnull) { h = h0; break; } /* Overflow */
2014 h1 = apply(f1, g1, op, 0);
2015 if(h1 == bddnull) { bddfree(h0); h = h1; break; } /* Overflow */
2016 h = getbddp(v, h0, h1);
2017 if(h == bddnull) { bddfree(h0); bddfree(h1); } /* Overflow */
2018 }
2019 break;
2020
2021 case BC_UNIV:
2022 if(g0 != g1)
2023 {
2024 h0 = apply(f0, g0, op, 0);
2025 if(h0 == bddnull) { h = h0; break; } /* Overflow */
2026 h1 = apply(f1, g0, op, 0);
2027 if(h1 == bddnull) { bddfree(h0); h = h1; break; } /* Overflow */
2028 h = apply(h0, h1, BC_AND, 0);
2029 bddfree(h0); bddfree(h1);
2030 }
2031 else
2032 {
2033 h0 = apply(f0, g0, op, 0);
2034 if(h0 == bddnull) { h = h0; break; } /* Overflow */
2035 h1 = apply(f1, g0, op, 0);
2036 if(h1 == bddnull) { bddfree(h0); h = h1; break; } /* Overflow */
2037 h = getbddp(v, h0, h1);
2038 if(h == bddnull) { bddfree(h0); bddfree(h1); } /* Overflow */
2039 }
2040 break;
2041
2042 case BC_AT0:
2043 case BC_AT1:
2044 case BC_OFFSET:
2045 case BC_ONSET:
2046 case BC_CHANGE:
2047 h0 = apply(f0, g, op, 0);
2048 if(h0 == bddnull) { h = h0; break; } /* Overflow */
2049 h1 = apply(f1, g, op, 0);
2050 if(h1 == bddnull) { bddfree(h0); h = h1; break; } /* Overflow */
2051 h = z? getzbddp(v, h0, h1): getbddp(v, h0, h1);
2052 if(h == bddnull) { bddfree(h0); bddfree(h1); } /* Overflow */
2053 break;
2054
2055 case BC_SUPPORT:
2056 h0 = apply(f0, bddfalse, op, 0);
2057 if(h0 == bddnull) { h = h0; break; } /* Overflow */
2058 h1 = apply(f1, bddfalse, op, 0);
2059 if(h1 == bddnull) { bddfree(h0); h = h1; break; } /* Overflow */
2060 h = z? apply(h0, h1, BC_UNION, 0):
2061 apply(B_NOT(h0), B_NOT(h1), BC_AND, 0);
2062 bddfree(h0); bddfree(h1);
2063 if(h == bddnull) break; /* Overflow */
2064 h0 = h;
2065 h = z? getzbddp(v, h0, bddtrue):
2066 getbddp(v, B_NOT(h0), bddtrue);
2067 if(h == bddnull) bddfree(h0); /* Overflow */
2068 break;
2069
2070 case BC_LSHIFT:
2071 case BC_RSHIFT:
2072 /* Get VarID of new level */
2073 {
2074 bddvar flev, newlev;
2075
2076 flev = bddlevofvar(v);
2077 if(op == BC_LSHIFT)
2078 {
2079 newlev = flev + (bddvar)g;
2080 if(newlev > VarUsed || newlev < flev)
2081 err("apply: Invald shift", newlev);
2082 }
2083 else
2084 {
2085 newlev = flev - (bddvar)g;
2086 if(newlev == 0 || newlev > flev)
2087 err("apply: Invald shift", newlev);
2088 }
2089 v = bddvaroflev(newlev);
2090 }
2091 h0 = apply(f0, g, op, 0);
2092 if(h0 == bddnull) { h = h0; break; } /* Overflow */
2093 h1 = apply(f1, g, op, 0);
2094 if(h1 == bddnull) { bddfree(h0); h = h1; break; } /* Overflow */
2095 h = z? getzbddp(v, h0, h1): getbddp(v, h0, h1);
2096 if(h == bddnull) { bddfree(h0); bddfree(h1); } /* Overflow */
2097 break;
2098
2099 case BC_CARD:
2100 h = apply(f0, bddempty, op, 0)
2101 + apply(f1, bddempty, op, 0);
2102 if(h >= bddnull) h = bddnull - 1;
2103 break;
2104
2105 case BC_LIT:
2106 h = apply(f0, bddempty, op, 0)
2107 + apply(f1, bddempty, op, 0);
2108 if(h >= bddnull) h = bddnull - 1;
2109 h += apply(f1, bddempty, BC_CARD, 0);
2110 if(h >= bddnull) h = bddnull - 1;
2111 break;
2112
2113 case BC_LEN:
2114 h0 = apply(f0, bddempty, op, 0);
2115 h1 = apply(f1, bddempty, op, 0) + 1;
2116 h = (h0 < h1)? h1: h0;
2117 break;
2118
2119 default:
2120 err("apply: unknown opcode", op);
2121 break;
2122 }
2123
2124 /* Stack overflow limitter */
2125 BDD_RECUR_DEC;
2126
2127 /* Saving to Cache */
2128 if(key != bddnull && h != bddnull)
2129 {
2130 cachep = Cache + key;
2131 cachep->op = op;
2132 B_SET_BDDP(cachep->f, f);
2133 B_SET_BDDP(cachep->g, g);
2134 B_SET_BDDP(cachep->h, h);
2135 if(h == f) switch(op)
2136 {
2137 case BC_AT0:
2138 key = B_CACHEKEY(BC_AT1, f, g);
2139 cachep = Cache + key;
2140 cachep->op = BC_AT1;
2141 B_SET_BDDP(cachep->f, f);
2142 B_SET_BDDP(cachep->g, g);
2143 B_SET_BDDP(cachep->h, h);
2144 break;
2145 case BC_AT1:
2146 key = B_CACHEKEY(BC_AT0, f, g);
2147 cachep = Cache + key;
2148 cachep->op = BC_AT0;
2149 B_SET_BDDP(cachep->f, f);
2150 B_SET_BDDP(cachep->g, g);
2151 B_SET_BDDP(cachep->h, h);
2152 break;
2153 case BC_OFFSET:
2154 key = B_CACHEKEY(BC_ONSET, f, g);
2155 cachep = Cache + key;
2156 cachep->op = BC_ONSET;
2157 B_SET_BDDP(cachep->f, f);
2158 B_SET_BDDP(cachep->g, g);
2159 B_SET_BDDP(cachep->h, bddfalse);
2160 break;
2161 default:
2162 break;
2163 }
2164 if(h == bddfalse && op == BC_ONSET)
2165 {
2166 key = B_CACHEKEY(BC_OFFSET, f, g);
2167 cachep = Cache + key;
2168 cachep->op = BC_OFFSET;
2169 B_SET_BDDP(cachep->f, f);
2170 B_SET_BDDP(cachep->g, g);
2171 B_SET_BDDP(cachep->h, f);
2172 }
2173 }
2174 return h;
2175 }
2176
gc1(np)2177 static void gc1(np)
2178 struct B_NodeTable *np;
2179 {
2180 /* np is a node ptr to be collected. (refc == 0) */
2181 bddp key, nx1, f0, f1;
2182 struct B_VarTable *varp;
2183 struct B_NodeTable *np1, *np2;
2184 bddp_32 *p_32;
2185 #ifdef B_64
2186 bddp_h8 *p_h8;
2187 #endif
2188
2189 /* remove the node from hash list */
2190 varp = Var + B_VAR_NP(np);
2191 f0 = B_GET_BDDP(np->f0);
2192 f1 = B_GET_BDDP(np->f1);
2193 key = B_HASHKEY(f0, f1, varp->hashSpc);
2194 B_SET_NXP(p, varp->hash, key);
2195 nx1 = B_GET_BDDP(*p);
2196 np1 = Node + nx1;
2197
2198 if(np1 == np) B_CPY_BDDP(*p, np->nx);
2199 else
2200 {
2201 while(np1 != np)
2202 {
2203 if(nx1 == bddnull)
2204 err("gc1: Fail to find the node to be deleted", np-Node);
2205 np2 = np1;
2206 nx1 = B_GET_BDDP(np2->nx);
2207 np1 = Node + nx1;
2208 }
2209 B_CPY_BDDP(np2->nx, np->nx);
2210 }
2211 varp->hashUsed--;
2212
2213 /* append the node to avail list */
2214 B_SET_BDDP(np->nx, Avail);
2215 Avail = np - Node;
2216
2217 NodeUsed--;
2218 np->varrfc = 0;
2219
2220 /* Check sub-graphs recursively */
2221 if(!B_CST(f0))
2222 {
2223 np1 = B_NP(f0);
2224 B_RFC_DEC_NP(np1);
2225 if(B_RFC_ZERO_NP(np1))
2226 { BDD_RECUR_INC; gc1(np1); BDD_RECUR_DEC; }
2227 }
2228 if(!B_CST(f1))
2229 {
2230 np1 = B_NP(f1);
2231 B_RFC_DEC_NP(np1);
2232 if(B_RFC_ZERO_NP(np1))
2233 { BDD_RECUR_INC; gc1(np1); BDD_RECUR_DEC; }
2234 }
2235 }
2236
count(f)2237 static bddp count(f)
2238 bddp f;
2239 {
2240 bddp nx;
2241 bddp c, g;
2242 bddvar flev, glev;
2243 struct B_NodeTable *fp;
2244 struct B_NodeTable *gp;
2245
2246 /* Check consistensy
2247 if(f == bddnull)
2248 err("count: bddnull found", bddnull);
2249 */
2250
2251 if(B_CST(f)) return 0; /* Constant */
2252 fp = B_NP(f);
2253
2254 /* Check visit flag */
2255 nx = B_GET_BDDP(fp->nx);
2256 if(nx & B_CST_MASK) return 0;
2257
2258 /* Check consistensy
2259 flev = Var[B_VAR_NP(fp)].lev;
2260 g = B_GET_BDDP(fp->f0);
2261 if(!B_CST(g))
2262 {
2263 gp = B_NP(g); glev = Var[B_VAR_NP(gp)].lev;
2264 if(flev <= glev)
2265 err("count: inconsistensy found at f0", fp-Node);
2266 }
2267 g = B_GET_BDDP(fp->f1);
2268 if(!B_CST(g))
2269 {
2270 gp = B_NP(g); glev = Var[B_VAR_NP(gp)].lev;
2271 if(flev <= glev)
2272 err("count: inconsistensy found at f1", fp-Node);
2273 }
2274 */
2275
2276 BDD_RECUR_INC;
2277 c = count(B_GET_BDDP(fp->f0)) + count(B_GET_BDDP(fp->f1)) + 1U ;
2278 BDD_RECUR_DEC;
2279
2280 /* Set visit flag */
2281 B_SET_BDDP(fp->nx, nx | B_CST_MASK);
2282
2283 return c;
2284 }
2285
export(strm,f)2286 static void export(strm, f)
2287 FILE *strm;
2288 bddp f;
2289 {
2290 bddp nx, f0, f1;
2291 bddvar v;
2292 struct B_NodeTable *fp;
2293
2294 if(B_CST(f)) return; /* Constant */
2295 fp = B_NP(f);
2296
2297 /* Check visit flag */
2298 nx = B_GET_BDDP(fp->nx);
2299 if(nx & B_CST_MASK) return;
2300
2301 /* Set visit flag */
2302 B_SET_BDDP(fp->nx, nx | B_CST_MASK);
2303
2304 /* Dump its subgraphs recursively */
2305 v = B_VAR_NP(fp);
2306 f0 = B_GET_BDDP(fp->f0);
2307 f0 = B_ABS(f0);
2308 f1 = B_GET_BDDP(fp->f1);
2309 BDD_RECUR_INC;
2310 export(strm, f0);
2311 export(strm, f1);
2312 BDD_RECUR_DEC;
2313
2314 /* Dump this node */
2315 fprintf(strm, B_BDDP_FD, B_ABS(f));
2316 fprintf(strm, " %d ", Var[v].lev);
2317 if(f0 == bddfalse) fprintf(strm, "F");
2318 else if(f0 == bddtrue) fprintf(strm, "T");
2319 else fprintf(strm, B_BDDP_FD, f0);
2320 fprintf(strm, " ");
2321 if(f1 == bddfalse) fprintf(strm, "F");
2322 else if(f1 == bddtrue) fprintf(strm, "T");
2323 else fprintf(strm, B_BDDP_FD, f1);
2324 fprintf(strm, "\n");
2325 }
2326
dump(f)2327 static void dump(f)
2328 bddp f;
2329 {
2330 bddp nx, f0, f1;
2331 bddvar v;
2332 struct B_NodeTable *fp;
2333
2334 if(B_CST(f)) return; /* Constant */
2335 fp = B_NP(f);
2336
2337 /* Check visit flag */
2338 nx = B_GET_BDDP(fp->nx);
2339 if(nx & B_CST_MASK) return;
2340
2341 /* Set visit flag */
2342 B_SET_BDDP(fp->nx, nx | B_CST_MASK);
2343
2344 /* Dump its subgraphs recursively */
2345 v = B_VAR_NP(fp);
2346 f0 = B_GET_BDDP(fp->f0);
2347 f0 = B_ABS(f0);
2348 f1 = B_GET_BDDP(fp->f1);
2349 BDD_RECUR_INC;
2350 dump(f0);
2351 dump(f1);
2352 BDD_RECUR_DEC;
2353
2354 /* Dump this node */
2355 printf("N");
2356 printf(B_BDDP_FD, B_NDX(f));
2357 printf(" = [V%d(%d), ", v, Var[v].lev);
2358 if(B_CST(f0)) printf(B_BDDP_FD, B_VAL(f0));
2359 else { printf("N"); printf(B_BDDP_FD, B_NDX(f0)); }
2360 printf(", ");
2361 if(B_NEG(f1)) putchar('~');
2362 if(B_CST(f1)) printf(B_BDDP_FD, B_ABS(B_VAL(f1)));
2363 else { printf("N"); printf(B_BDDP_FD, B_NDX(f1)); }
2364 printf("]");
2365 if(B_Z_NP(fp)) printf(" #Z");
2366 printf("\n");
2367 }
2368
reset(f)2369 static void reset(f)
2370 bddp f;
2371 {
2372 bddp nx;
2373 struct B_NodeTable *fp;
2374
2375 if(B_CST(f)) return; /* Constant */
2376 fp = B_NP(f);
2377
2378 /* Check visit flag */
2379 nx = B_GET_BDDP(fp->nx);
2380 if(nx & B_CST_MASK)
2381 {
2382 /* Reset visit flag */
2383 B_SET_BDDP(fp->nx, nx & ~B_CST_MASK);
2384 BDD_RECUR_INC;
2385 reset(B_GET_BDDP(fp->f0));
2386 reset(B_GET_BDDP(fp->f1));
2387 BDD_RECUR_DEC;
2388 }
2389 }
2390
getzbddp(v,f0,f1)2391 static bddp getzbddp(v, f0, f1)
2392 bddvar v;
2393 bddp f0, f1;
2394 /* Returns bddnull if not enough memory */
2395 {
2396 struct B_NodeTable *fp;
2397
2398 /* Check elimination rule */
2399 if(f1 == bddfalse) return f0;
2400
2401 /* Negative edge constraint */
2402 if(B_NEG(f0))
2403 {
2404 bddp h;
2405
2406 h = getnode(v, f0, f1);
2407 if(h == bddnull) return bddnull;
2408 return B_NOT(h);
2409 }
2410 return getnode(v, B_NOT(f0), f1);
2411 }
2412
andfalse(f,g)2413 static int andfalse(f, g)
2414 bddp f, g;
2415 {
2416 struct B_NodeTable *fp, *gp;
2417 struct B_CacheTable *cachep;
2418 bddp key, f0, f1, g0, g1, h0, h1, h;
2419 bddvar v, flev, glev;
2420
2421 /* Check trivial cases */
2422 if(f == bddfalse || g == bddfalse || f == B_NOT(g)) return 0;
2423 if(f == bddtrue || g == bddtrue || f == g) return 1;
2424 /* Check operand swap */
2425 if(f > g) { h = f; f = g; g = h; } /* swap (f, g) */
2426
2427 /* Non-trivial operations */
2428 /* Try cache? */
2429 if((B_CST(f) || B_RFC_ONE_NP(B_NP(f))) &&
2430 (B_CST(g) || B_RFC_ONE_NP(B_NP(g)))) key = bddnull;
2431 else
2432 {
2433 /* Checking Cache */
2434 key = B_CACHEKEY(BC_AND, f, g);
2435 cachep = Cache + key;
2436 if(cachep->op == BC_AND &&
2437 f == B_GET_BDDP(cachep->f) &&
2438 g == B_GET_BDDP(cachep->g))
2439 {
2440 /* Hit */
2441 h = B_GET_BDDP(cachep->h);
2442 return (h==bddfalse)? 0: 1;
2443 }
2444 }
2445 /* Get (f0, f1) and (g0, g1)*/
2446 fp = B_NP(f);
2447 flev = B_CST(f)? 0: Var[B_VAR_NP(fp)].lev;
2448 gp = B_NP(g);
2449 glev = B_CST(g)? 0: Var[B_VAR_NP(gp)].lev;
2450 f0 = f; f1 = f;
2451 g0 = g; g1 = g;
2452
2453 if(flev <= glev)
2454 {
2455 v = B_VAR_NP(gp);
2456 g0 = B_GET_BDDP(gp->f0);
2457 g1 = B_GET_BDDP(gp->f1);
2458 if(B_NEG(g)) { g0 = B_NOT(g0); g1 = B_NOT(g1); }
2459 }
2460
2461 if(flev >= glev)
2462 {
2463 v = B_VAR_NP(fp);
2464 f0 = B_GET_BDDP(fp->f0);
2465 f1 = B_GET_BDDP(fp->f1);
2466 if(B_NEG(f)) { f0 = B_NOT(f0); f1 = B_NOT(f1); }
2467 }
2468
2469 /* Get result */
2470 if(andfalse(f0, g0) == 1) return 1;
2471 if(andfalse(f1, g1) == 1) return 1;
2472
2473 /* Saving to Cache */
2474 if(key != bddnull)
2475 {
2476 cachep = Cache + key;
2477 cachep->op = BC_AND;
2478 B_SET_BDDP(cachep->f, f);
2479 B_SET_BDDP(cachep->g, g);
2480 B_SET_BDDP(cachep->h, bddfalse);
2481 }
2482 return 0;
2483 }
2484
err(msg,num)2485 static int err(msg, num)
2486 char *msg;
2487 bddp num;
2488 {
2489 fprintf(stderr,"***** ERROR %s ( ", msg);
2490 fprintf(stderr, B_BDDP_FX, num);
2491 fprintf(stderr," ) *****\n");
2492 fprintf(stderr," NodeLimit : ");
2493 fprintf(stderr, B_BDDP_FD, NodeLimit);
2494 fprintf(stderr,"\t NodeSpc : ");
2495 fprintf(stderr, B_BDDP_FD, NodeSpc);
2496 fprintf(stderr,"\t VarSpc : %d",VarSpc);
2497 fprintf(stderr,"\n CacheSpc : ");
2498 fprintf(stderr, B_BDDP_FD, CacheSpc);
2499 fprintf(stderr,"\t NodeUsed : ");
2500 fprintf(stderr, B_BDDP_FD, NodeUsed);
2501 fprintf(stderr,"\t VarUsed : %d\n",VarUsed);
2502 exit(1);
2503 return 1;
2504 }
2505
rfc_inc_ovf(np)2506 static int rfc_inc_ovf(np)
2507 struct B_NodeTable *np;
2508 {
2509 bddp ix, nx, nx2, key, rfc, oldSpc;
2510 bddp *p, *p2;
2511 struct B_RFC_Table *oldRFCT;
2512
2513 /* printf("rfc_inc %d (u:%d)\n", np-Node, RFCT_Used); */
2514 if(RFCT_Spc == 0)
2515 {
2516 /* Create RFC-table */
2517 RFCT = B_MALLOC(struct B_RFC_Table, B_RFCT_SPC0);
2518 if(!RFCT)
2519 {
2520 err("B_RFC_INC_NP: rfc memory over flow", np-Node);
2521 return 1;
2522 }
2523 for(ix=0; ix<B_RFCT_SPC0; ix++)
2524 {
2525 B_SET_BDDP((RFCT+ix)->nx, bddnull);
2526 B_SET_BDDP((RFCT+ix)->rfc, (bddp)0);
2527 }
2528 RFCT_Spc = B_RFCT_SPC0;
2529 }
2530
2531 nx = np - Node;
2532 key = nx & (RFCT_Spc-1);
2533 nx2 = B_GET_BDDP((RFCT+key)->nx);
2534 while(nx2 != bddnull)
2535 {
2536 if(nx == nx2)
2537 {
2538 if(np->varrfc < B_RFC_MASK)
2539 {
2540 rfc = 0;
2541 np->varrfc += B_RFC_UNIT;
2542 }
2543 else rfc = B_GET_BDDP((RFCT+key)->rfc) + 1;
2544 B_SET_BDDP((RFCT+key)->rfc, rfc);
2545 return 0;
2546 }
2547 key = (key+1) & (RFCT_Spc-1);
2548 nx2 = B_GET_BDDP((RFCT+key)->nx);
2549 }
2550
2551 /* new rfc entry */
2552 B_SET_BDDP((RFCT+key)->nx, nx);
2553 B_SET_BDDP((RFCT+key)->rfc, (bddp)0);
2554 np->varrfc += B_RFC_UNIT;
2555 RFCT_Used++;
2556
2557 if((RFCT_Used << 1) >= RFCT_Spc)
2558 {
2559 /* Enlarge RFC-table */
2560 oldSpc = RFCT_Spc;
2561 RFCT_Spc <<= 2;
2562
2563 oldRFCT = RFCT;
2564 RFCT = B_MALLOC(struct B_RFC_Table, RFCT_Spc);
2565 if(!RFCT)
2566 {
2567 err("B_RFC_INC_NP: rfc memory over flow", np-Node);
2568 return 1;
2569 }
2570 for(ix=0; ix<RFCT_Spc; ix++)
2571 {
2572 B_SET_BDDP((RFCT+ix)->nx, bddnull);
2573 B_SET_BDDP((RFCT+ix)->rfc, (bddp)0);
2574 }
2575 for(ix=0; ix<oldSpc; ix++)
2576 {
2577 nx = B_GET_BDDP((oldRFCT+ix)->nx);
2578 if(nx == bddnull) continue;
2579 key = nx & (RFCT_Spc-1);
2580 nx2 = B_GET_BDDP((RFCT+key)->nx);
2581 while(nx2 != bddnull)
2582 {
2583 key = (key+1) & (RFCT_Spc-1);
2584 nx2 = B_GET_BDDP((RFCT+key)->nx);
2585 }
2586 B_SET_BDDP((RFCT+key)->nx, nx);
2587 rfc = B_GET_BDDP((oldRFCT+ix)->rfc);
2588 B_SET_BDDP((RFCT+key)->rfc, rfc);
2589 }
2590 free(oldRFCT);
2591 }
2592
2593 return 0;
2594 }
2595
rfc_dec_ovf(np)2596 static int rfc_dec_ovf(np)
2597 struct B_NodeTable *np;
2598 {
2599 bddp nx, key, nx2, rfc;
2600
2601 /* printf("rfc_dec %d (u:%d)\n", np-Node, RFCT_Used); */
2602 nx = np - Node;
2603 key = nx & (RFCT_Spc-1);
2604 nx2 = B_GET_BDDP((RFCT+key)->nx);
2605 while(nx2 != bddnull)
2606 {
2607 if(nx == nx2)
2608 {
2609 rfc = B_GET_BDDP((RFCT+key)->rfc);
2610 if(rfc == 0)
2611 {
2612 np->varrfc -= B_RFC_UNIT;
2613 return 0;
2614 }
2615 B_SET_BDDP((RFCT+key)->rfc, rfc-1);
2616 return 0;
2617 }
2618 key = (key+1) & (RFCT_Spc-1);
2619 nx2 = B_GET_BDDP((RFCT+key)->nx);
2620 }
2621 return 0;
2622 }
2623
2624 #define IMPORTHASH(x) (((x >> 1) ^ (x >> 16)) & (hashsize - 1))
2625
import(strm,p,lim,z)2626 int import(strm, p, lim, z)
2627 FILE *strm;
2628 bddp *p;
2629 int lim;
2630 int z;
2631 {
2632 int n, m, v, i, lev, var, inv, e;
2633 bddp n_nd, ix, f, f0, f1, nd, nd0, nd1, hashsize, ixx;
2634 char s[256];
2635 bddp *hash1;
2636 bddp *hash2;
2637
2638 v = fscanf(strm, "%s", s);
2639 if(v == EOF) return 1;
2640 if(strcmp(s, "_i") != 0) return 1;
2641 v = fscanf(strm, "%s", s);
2642 if(v == EOF) return 1;
2643 n = strtol(s, NULL, 10);
2644 while(n > bddvarused()) bddnewvar();
2645
2646 v = fscanf(strm, "%s", s);
2647 if(v == EOF) return 1;
2648 if(strcmp(s, "_o") != 0) return 1;
2649 v = fscanf(strm, "%s", s);
2650 if(v == EOF) return 1;
2651 m = strtol(s, NULL, 10);
2652
2653 v = fscanf(strm, "%s", s);
2654 if(v == EOF) return 1;
2655 if(strcmp(s, "_n") != 0) return 1;
2656 v = fscanf(strm, "%s", s);
2657 if(v == EOF) return 1;
2658 n_nd = B_STRTOI(s, NULL, 10);
2659
2660 for(hashsize = 1; hashsize < (n_nd<<1); hashsize <<= 1)
2661 ; /* empty */
2662 hash1 = B_MALLOC(bddp, hashsize);
2663 if(hash1 == 0) return 1;
2664 hash2 = B_MALLOC(bddp, hashsize);
2665 if(hash2 == 0)
2666 {
2667 free(hash1);
2668 return 1;
2669 }
2670 for(ix=0; ix<hashsize; ix++) hash1[ix] = bddnull;
2671
2672 e = 0;
2673 for(ix=0; ix<n_nd; ix++)
2674 {
2675 v = fscanf(strm, "%s", s);
2676 if(v == EOF) { e = 1; break; }
2677 nd = B_STRTOI(s, NULL, 10);
2678
2679 v = fscanf(strm, "%s", s);
2680 if(v == EOF) { e = 1; break; }
2681 lev = strtol(s, NULL, 10);
2682 var = bddvaroflev(lev);
2683
2684 v = fscanf(strm, "%s", s);
2685 if(v == EOF) { e = 1; break; }
2686 if(strcmp(s, "F") == 0) f0 = bddfalse;
2687 else if(strcmp(s, "T") == 0) f0 = bddtrue;
2688 else
2689 {
2690 nd0 = B_STRTOI(s, NULL, 10);
2691
2692 ixx = IMPORTHASH(nd0);
2693 while(hash1[ixx] != nd0)
2694 {
2695 if(hash1[ixx] == bddnull)
2696 {
2697 err("bddimport: internal error", ixx);
2698 return 1;
2699 }
2700 ixx++;
2701 ixx &= (hashsize-1);
2702 }
2703 f0 = bddcopy(hash2[ixx]);
2704 }
2705
2706 v = fscanf(strm, "%s", s);
2707 if(v == EOF) { e = 1; bddfree(f0); break; }
2708 if(strcmp(s, "F") == 0) f1 = bddfalse;
2709 else if(strcmp(s, "T") == 0) f1 = bddtrue;
2710 else
2711 {
2712 nd1 = B_STRTOI(s, NULL, 10);
2713 if(nd1 & 1) { inv = 1; nd1 ^= 1; }
2714 else inv = 0;
2715
2716 ixx = IMPORTHASH(nd1);
2717 while(hash1[ixx] != nd1)
2718 {
2719 if(hash1[ixx] == bddnull)
2720 {
2721 err("bddimport: internal error", ixx);
2722 return 1;
2723 }
2724 ixx++;
2725 ixx &= (hashsize-1);
2726 }
2727 f1 = (inv)? bddnot(hash2[ixx]): bddcopy(hash2[ixx]);
2728 }
2729
2730 f = (z)? getzbddp(var, f0, f1): getbddp(var, f0, f1);
2731 if(f == bddnull)
2732 {
2733 e = 1;
2734 bddfree(f1);
2735 bddfree(f0);
2736 break;
2737 }
2738
2739 ixx = IMPORTHASH(nd);
2740 while(hash1[ixx] != bddnull)
2741 {
2742 if(hash1[ixx] == nd)
2743 {
2744 err("bddimport: internal error", ixx);
2745 return 1;
2746 }
2747 ixx++;
2748 ixx &= (hashsize-1);
2749 }
2750 hash1[ixx] = nd;
2751 hash2[ixx] = f;
2752 }
2753
2754 if(e)
2755 {
2756 for(ix=0; ix<hashsize; ix++)
2757 if(hash1[ix] != bddnull) bddfree(hash2[ix]);
2758 free(hash2);
2759 free(hash1);
2760 return 1;
2761 }
2762
2763 for(i=0; i<m; i++)
2764 {
2765 if(i >= lim) break;
2766 v = fscanf(strm, "%s", s);
2767 if(v == EOF)
2768 {
2769 for(i--; i>=0; i--) bddfree(p[i]);
2770 for(ix=0; ix<hashsize; ix++)
2771 if(hash1[ix] != bddnull) bddfree(hash2[ix]);
2772 free(hash2);
2773 free(hash1);
2774 return 1;
2775 }
2776 nd = B_STRTOI(s, NULL, 10);
2777 if(strcmp(s, "F") == 0) p[i] = bddfalse;
2778 else if(strcmp(s, "T") == 0) p[i] = bddtrue;
2779 else
2780 {
2781 if(nd & 1) { inv = 1; nd ^= 1; }
2782 else inv = 0;
2783
2784 ixx = IMPORTHASH(nd);
2785 while(hash1[ixx] != nd)
2786 {
2787 if(hash1[ixx] == bddnull)
2788 {
2789 err("bddimport: internal error", ixx);
2790 return 1;
2791 }
2792 ixx++;
2793 ixx &= (hashsize-1);
2794 }
2795 p[i] = (inv)? bddnot(hash2[ixx]): bddcopy(hash2[ixx]);
2796 }
2797 }
2798 if(i < lim) p[i] = bddnull;
2799
2800 /* clear hash table */
2801 for(ix=0; ix<hashsize; ix++)
2802 if(hash1[ix] != bddnull) bddfree(hash2[ix]);
2803 free(hash2);
2804 free(hash1);
2805
2806 return 0;
2807 }
2808
bddimport(strm,p,lim)2809 int bddimport(strm, p, lim)
2810 FILE *strm;
2811 bddp *p;
2812 int lim;
2813 {
2814 return import(strm, p, lim, 0);
2815 }
2816
bddimportz(strm,p,lim)2817 int bddimportz(strm, p, lim)
2818 FILE *strm;
2819 bddp *p;
2820 int lim;
2821 {
2822 return import(strm, p, lim, 1);
2823 }
2824
bddpush(f,v)2825 bddp bddpush(f, v)
2826 bddp f;
2827 bddvar v;
2828 /* Returns bddnull if not enough memory */
2829 {
2830 struct B_NodeTable *fp;
2831
2832 /* Check operands */
2833 if(v > VarUsed || v == 0) err("bddpush: Invalid VarID", v);
2834 if(f == bddnull) return bddnull;
2835
2836 if(!B_CST(f)) { fp = B_NP(f); B_RFC_INC_NP(fp); }
2837 return getzbddp(v, bddfalse, f);
2838 }
2839
2840