source: vis_dev/glu-2.3/src/cuBdd/cuddBridge.c@ 104

Last change on this file since 104 was 13, checked in by cecile, 15 years ago

library glu 2.3
File size: 26.1 KB
Line 
1/**CFile***********************************************************************
2
3 FileName [cuddBridge.c]
4
5 PackageName [cudd]
6
7 Synopsis [Translation from BDD to ADD and vice versa and transfer between
8 different managers.]
9
10 Description [External procedures included in this file:
11 <ul>
12 <li> Cudd_addBddThreshold()
13 <li> Cudd_addBddStrictThreshold()
14 <li> Cudd_addBddInterval()
15 <li> Cudd_addBddIthBit()
16 <li> Cudd_BddToAdd()
17 <li> Cudd_addBddPattern()
18 <li> Cudd_bddTransfer()
19 </ul>
20 Internal procedures included in this file:
21 <ul>
22 <li> cuddBddTransfer()
23 <li> cuddAddBddDoPattern()
24 </ul>
25 Static procedures included in this file:
26 <ul>
27 <li> addBddDoThreshold()
28 <li> addBddDoStrictThreshold()
29 <li> addBddDoInterval()
30 <li> addBddDoIthBit()
31 <li> ddBddToAddRecur()
32 <li> cuddBddTransferRecur()
33 </ul>
34 ]
35
36 SeeAlso []
37
38 Author [Fabio Somenzi]
39
40 Copyright [Copyright (c) 1995-2004, Regents of the University of Colorado
41
42 All rights reserved.
43
44 Redistribution and use in source and binary forms, with or without
45 modification, are permitted provided that the following conditions
46 are met:
47
48 Redistributions of source code must retain the above copyright
49 notice, this list of conditions and the following disclaimer.
50
51 Redistributions in binary form must reproduce the above copyright
52 notice, this list of conditions and the following disclaimer in the
53 documentation and/or other materials provided with the distribution.
54
55 Neither the name of the University of Colorado nor the names of its
56 contributors may be used to endorse or promote products derived from
57 this software without specific prior written permission.
58
59 THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
60 "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
61 LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
62 FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
63 COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
64 INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
65 BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
66 LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
67 CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
68 LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
69 ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
70 POSSIBILITY OF SUCH DAMAGE.]
71
72******************************************************************************/
73
74#include "util.h"
75#include "cuddInt.h"
76
77/*---------------------------------------------------------------------------*/
78/* Constant declarations */
79/*---------------------------------------------------------------------------*/
80
81
82/*---------------------------------------------------------------------------*/
83/* Stucture declarations */
84/*---------------------------------------------------------------------------*/
85
86
87/*---------------------------------------------------------------------------*/
88/* Type declarations */
89/*---------------------------------------------------------------------------*/
90
91
92/*---------------------------------------------------------------------------*/
93/* Variable declarations */
94/*---------------------------------------------------------------------------*/
95
96#ifndef lint
97static char rcsid[] DD_UNUSED = "$Id: cuddBridge.c,v 1.19 2008/04/25 06:42:55 fabio Exp $";
98#endif
99
100/*---------------------------------------------------------------------------*/
101/* Macro declarations */
102/*---------------------------------------------------------------------------*/
103
104
105#ifdef __cplusplus
106extern "C" {
107#endif
108
109/**AutomaticStart*************************************************************/
110
111/*---------------------------------------------------------------------------*/
112/* Static function prototypes */
113/*---------------------------------------------------------------------------*/
114
115static DdNode * addBddDoThreshold (DdManager *dd, DdNode *f, DdNode *val);
116static DdNode * addBddDoStrictThreshold (DdManager *dd, DdNode *f, DdNode *val);
117static DdNode * addBddDoInterval (DdManager *dd, DdNode *f, DdNode *l, DdNode *u);
118static DdNode * addBddDoIthBit (DdManager *dd, DdNode *f, DdNode *index);
119static DdNode * ddBddToAddRecur (DdManager *dd, DdNode *B);
120static DdNode * cuddBddTransferRecur (DdManager *ddS, DdManager *ddD, DdNode *f, st_table *table);
121
122/**AutomaticEnd***************************************************************/
123
124#ifdef __cplusplus
125}
126#endif
127
128
129/*---------------------------------------------------------------------------*/
130/* Definition of exported functions */
131/*---------------------------------------------------------------------------*/
132
133
134/**Function********************************************************************
135
136 Synopsis [Converts an ADD to a BDD.]
137
138 Description [Converts an ADD to a BDD by replacing all
139 discriminants greater than or equal to value with 1, and all other
140 discriminants with 0. Returns a pointer to the resulting BDD if
141 successful; NULL otherwise.]
142
143 SideEffects [None]
144
145 SeeAlso [Cudd_addBddInterval Cudd_addBddPattern Cudd_BddToAdd
146 Cudd_addBddStrictThreshold]
147
148******************************************************************************/
149DdNode *
150Cudd_addBddThreshold(
151 DdManager * dd,
152 DdNode * f,
153 CUDD_VALUE_TYPE value)
154{
155 DdNode *res;
156 DdNode *val;
157
158 val = cuddUniqueConst(dd,value);
159 if (val == NULL) return(NULL);
160 cuddRef(val);
161
162 do {
163 dd->reordered = 0;
164 res = addBddDoThreshold(dd, f, val);
165 } while (dd->reordered == 1);
166
167 if (res == NULL) {
168 Cudd_RecursiveDeref(dd, val);
169 return(NULL);
170 }
171 cuddRef(res);
172 Cudd_RecursiveDeref(dd, val);
173 cuddDeref(res);
174 return(res);
175
176} /* end of Cudd_addBddThreshold */
177
178
179/**Function********************************************************************
180
181 Synopsis [Converts an ADD to a BDD.]
182
183 Description [Converts an ADD to a BDD by replacing all
184 discriminants STRICTLY greater than value with 1, and all other
185 discriminants with 0. Returns a pointer to the resulting BDD if
186 successful; NULL otherwise.]
187
188 SideEffects [None]
189
190 SeeAlso [Cudd_addBddInterval Cudd_addBddPattern Cudd_BddToAdd
191 Cudd_addBddThreshold]
192
193******************************************************************************/
194DdNode *
195Cudd_addBddStrictThreshold(
196 DdManager * dd,
197 DdNode * f,
198 CUDD_VALUE_TYPE value)
199{
200 DdNode *res;
201 DdNode *val;
202
203 val = cuddUniqueConst(dd,value);
204 if (val == NULL) return(NULL);
205 cuddRef(val);
206
207 do {
208 dd->reordered = 0;
209 res = addBddDoStrictThreshold(dd, f, val);
210 } while (dd->reordered == 1);
211
212 if (res == NULL) {
213 Cudd_RecursiveDeref(dd, val);
214 return(NULL);
215 }
216 cuddRef(res);
217 Cudd_RecursiveDeref(dd, val);
218 cuddDeref(res);
219 return(res);
220
221} /* end of Cudd_addBddStrictThreshold */
222
223
224/**Function********************************************************************
225
226 Synopsis [Converts an ADD to a BDD.]
227
228 Description [Converts an ADD to a BDD by replacing all
229 discriminants greater than or equal to lower and less than or equal to
230 upper with 1, and all other discriminants with 0. Returns a pointer to
231 the resulting BDD if successful; NULL otherwise.]
232
233 SideEffects [None]
234
235 SeeAlso [Cudd_addBddThreshold Cudd_addBddStrictThreshold
236 Cudd_addBddPattern Cudd_BddToAdd]
237
238******************************************************************************/
239DdNode *
240Cudd_addBddInterval(
241 DdManager * dd,
242 DdNode * f,
243 CUDD_VALUE_TYPE lower,
244 CUDD_VALUE_TYPE upper)
245{
246 DdNode *res;
247 DdNode *l;
248 DdNode *u;
249
250 /* Create constant nodes for the interval bounds, so that we can use
251 ** the global cache.
252 */
253 l = cuddUniqueConst(dd,lower);
254 if (l == NULL) return(NULL);
255 cuddRef(l);
256 u = cuddUniqueConst(dd,upper);
257 if (u == NULL) {
258 Cudd_RecursiveDeref(dd,l);
259 return(NULL);
260 }
261 cuddRef(u);
262
263 do {
264 dd->reordered = 0;
265 res = addBddDoInterval(dd, f, l, u);
266 } while (dd->reordered == 1);
267
268 if (res == NULL) {
269 Cudd_RecursiveDeref(dd, l);
270 Cudd_RecursiveDeref(dd, u);
271 return(NULL);
272 }
273 cuddRef(res);
274 Cudd_RecursiveDeref(dd, l);
275 Cudd_RecursiveDeref(dd, u);
276 cuddDeref(res);
277 return(res);
278
279} /* end of Cudd_addBddInterval */
280
281
282/**Function********************************************************************
283
284 Synopsis [Converts an ADD to a BDD by extracting the i-th bit from
285 the leaves.]
286
287 Description [Converts an ADD to a BDD by replacing all
288 discriminants whose i-th bit is equal to 1 with 1, and all other
289 discriminants with 0. The i-th bit refers to the integer
290 representation of the leaf value. If the value is has a fractional
291 part, it is ignored. Repeated calls to this procedure allow one to
292 transform an integer-valued ADD into an array of BDDs, one for each
293 bit of the leaf values. Returns a pointer to the resulting BDD if
294 successful; NULL otherwise.]
295
296 SideEffects [None]
297
298 SeeAlso [Cudd_addBddInterval Cudd_addBddPattern Cudd_BddToAdd]
299
300******************************************************************************/
301DdNode *
302Cudd_addBddIthBit(
303 DdManager * dd,
304 DdNode * f,
305 int bit)
306{
307 DdNode *res;
308 DdNode *index;
309
310 index = cuddUniqueConst(dd,(CUDD_VALUE_TYPE) bit);
311 if (index == NULL) return(NULL);
312 cuddRef(index);
313
314 do {
315 dd->reordered = 0;
316 res = addBddDoIthBit(dd, f, index);
317 } while (dd->reordered == 1);
318
319 if (res == NULL) {
320 Cudd_RecursiveDeref(dd, index);
321 return(NULL);
322 }
323 cuddRef(res);
324 Cudd_RecursiveDeref(dd, index);
325 cuddDeref(res);
326 return(res);
327
328} /* end of Cudd_addBddIthBit */
329
330
331/**Function********************************************************************
332
333 Synopsis [Converts a BDD to a 0-1 ADD.]
334
335 Description [Converts a BDD to a 0-1 ADD. Returns a pointer to the
336 resulting ADD if successful; NULL otherwise.]
337
338 SideEffects [None]
339
340 SeeAlso [Cudd_addBddPattern Cudd_addBddThreshold Cudd_addBddInterval
341 Cudd_addBddStrictThreshold]
342
343******************************************************************************/
344DdNode *
345Cudd_BddToAdd(
346 DdManager * dd,
347 DdNode * B)
348{
349 DdNode *res;
350
351 do {
352 dd->reordered = 0;
353 res = ddBddToAddRecur(dd, B);
354 } while (dd->reordered ==1);
355 return(res);
356
357} /* end of Cudd_BddToAdd */
358
359
360/**Function********************************************************************
361
362 Synopsis [Converts an ADD to a BDD.]
363
364 Description [Converts an ADD to a BDD by replacing all
365 discriminants different from 0 with 1. Returns a pointer to the
366 resulting BDD if successful; NULL otherwise.]
367
368 SideEffects [None]
369
370 SeeAlso [Cudd_BddToAdd Cudd_addBddThreshold Cudd_addBddInterval
371 Cudd_addBddStrictThreshold]
372
373******************************************************************************/
374DdNode *
375Cudd_addBddPattern(
376 DdManager * dd,
377 DdNode * f)
378{
379 DdNode *res;
380
381 do {
382 dd->reordered = 0;
383 res = cuddAddBddDoPattern(dd, f);
384 } while (dd->reordered == 1);
385 return(res);
386
387} /* end of Cudd_addBddPattern */
388
389
390/**Function********************************************************************
391
392 Synopsis [Convert a BDD from a manager to another one.]
393
394 Description [Convert a BDD from a manager to another one. The orders of the
395 variables in the two managers may be different. Returns a
396 pointer to the BDD in the destination manager if successful; NULL
397 otherwise.]
398
399 SideEffects [None]
400
401 SeeAlso []
402
403******************************************************************************/
404DdNode *
405Cudd_bddTransfer(
406 DdManager * ddSource,
407 DdManager * ddDestination,
408 DdNode * f)
409{
410 DdNode *res;
411 do {
412 ddDestination->reordered = 0;
413 res = cuddBddTransfer(ddSource, ddDestination, f);
414 } while (ddDestination->reordered == 1);
415 return(res);
416
417} /* end of Cudd_bddTransfer */
418
419
420/*---------------------------------------------------------------------------*/
421/* Definition of internal functions */
422/*---------------------------------------------------------------------------*/
423
424
425/**Function********************************************************************
426
427 Synopsis [Convert a BDD from a manager to another one.]
428
429 Description [Convert a BDD from a manager to another one. Returns a
430 pointer to the BDD in the destination manager if successful; NULL
431 otherwise.]
432
433 SideEffects [None]
434
435 SeeAlso [Cudd_bddTransfer]
436
437******************************************************************************/
438DdNode *
439cuddBddTransfer(
440 DdManager * ddS,
441 DdManager * ddD,
442 DdNode * f)
443{
444 DdNode *res;
445 st_table *table = NULL;
446 st_generator *gen = NULL;
447 DdNode *key, *value;
448
449 table = st_init_table(st_ptrcmp,st_ptrhash);
450 if (table == NULL) goto failure;
451 res = cuddBddTransferRecur(ddS, ddD, f, table);
452 if (res != NULL) cuddRef(res);
453
454 /* Dereference all elements in the table and dispose of the table.
455 ** This must be done also if res is NULL to avoid leaks in case of
456 ** reordering. */
457 gen = st_init_gen(table);
458 if (gen == NULL) goto failure;
459 while (st_gen(gen, &key, &value)) {
460 Cudd_RecursiveDeref(ddD, value);
461 }
462 st_free_gen(gen); gen = NULL;
463 st_free_table(table); table = NULL;
464
465 if (res != NULL) cuddDeref(res);
466 return(res);
467
468failure:
469 /* No need to free gen because it is always NULL here. */
470 if (table != NULL) st_free_table(table);
471 return(NULL);
472
473} /* end of cuddBddTransfer */
474
475
476/**Function********************************************************************
477
478 Synopsis [Performs the recursive step for Cudd_addBddPattern.]
479
480 Description [Performs the recursive step for Cudd_addBddPattern. Returns a
481 pointer to the resulting BDD if successful; NULL otherwise.]
482
483 SideEffects [None]
484
485 SeeAlso []
486
487******************************************************************************/
488DdNode *
489cuddAddBddDoPattern(
490 DdManager * dd,
491 DdNode * f)
492{
493 DdNode *res, *T, *E;
494 DdNode *fv, *fvn;
495 int v;
496
497 statLine(dd);
498 /* Check terminal case. */
499 if (cuddIsConstant(f)) {
500 return(Cudd_NotCond(DD_ONE(dd),f == DD_ZERO(dd)));
501 }
502
503 /* Check cache. */
504 res = cuddCacheLookup1(dd,Cudd_addBddPattern,f);
505 if (res != NULL) return(res);
506
507 /* Recursive step. */
508 v = f->index;
509 fv = cuddT(f); fvn = cuddE(f);
510
511 T = cuddAddBddDoPattern(dd,fv);
512 if (T == NULL) return(NULL);
513 cuddRef(T);
514
515 E = cuddAddBddDoPattern(dd,fvn);
516 if (E == NULL) {
517 Cudd_RecursiveDeref(dd, T);
518 return(NULL);
519 }
520 cuddRef(E);
521 if (Cudd_IsComplement(T)) {
522 res = (T == E) ? Cudd_Not(T) : cuddUniqueInter(dd,v,Cudd_Not(T),Cudd_Not(E));
523 if (res == NULL) {
524 Cudd_RecursiveDeref(dd, T);
525 Cudd_RecursiveDeref(dd, E);
526 return(NULL);
527 }
528 res = Cudd_Not(res);
529 } else {
530 res = (T == E) ? T : cuddUniqueInter(dd,v,T,E);
531 if (res == NULL) {
532 Cudd_RecursiveDeref(dd, T);
533 Cudd_RecursiveDeref(dd, E);
534 return(NULL);
535 }
536 }
537 cuddDeref(T);
538 cuddDeref(E);
539
540 /* Store result. */
541 cuddCacheInsert1(dd,Cudd_addBddPattern,f,res);
542
543 return(res);
544
545} /* end of cuddAddBddDoPattern */
546
547
548/*---------------------------------------------------------------------------*/
549/* Definition of static functions */
550/*---------------------------------------------------------------------------*/
551
552
553/**Function********************************************************************
554
555 Synopsis [Performs the recursive step for Cudd_addBddThreshold.]
556
557 Description [Performs the recursive step for Cudd_addBddThreshold.
558 Returns a pointer to the BDD if successful; NULL otherwise.]
559
560 SideEffects [None]
561
562 SeeAlso [addBddDoStrictThreshold]
563
564******************************************************************************/
565static DdNode *
566addBddDoThreshold(
567 DdManager * dd,
568 DdNode * f,
569 DdNode * val)
570{
571 DdNode *res, *T, *E;
572 DdNode *fv, *fvn;
573 int v;
574
575 statLine(dd);
576 /* Check terminal case. */
577 if (cuddIsConstant(f)) {
578 return(Cudd_NotCond(DD_ONE(dd),cuddV(f) < cuddV(val)));
579 }
580
581 /* Check cache. */
582 res = cuddCacheLookup2(dd,addBddDoThreshold,f,val);
583 if (res != NULL) return(res);
584
585 /* Recursive step. */
586 v = f->index;
587 fv = cuddT(f); fvn = cuddE(f);
588
589 T = addBddDoThreshold(dd,fv,val);
590 if (T == NULL) return(NULL);
591 cuddRef(T);
592
593 E = addBddDoThreshold(dd,fvn,val);
594 if (E == NULL) {
595 Cudd_RecursiveDeref(dd, T);
596 return(NULL);
597 }
598 cuddRef(E);
599 if (Cudd_IsComplement(T)) {
600 res = (T == E) ? Cudd_Not(T) : cuddUniqueInter(dd,v,Cudd_Not(T),Cudd_Not(E));
601 if (res == NULL) {
602 Cudd_RecursiveDeref(dd, T);
603 Cudd_RecursiveDeref(dd, E);
604 return(NULL);
605 }
606 res = Cudd_Not(res);
607 } else {
608 res = (T == E) ? T : cuddUniqueInter(dd,v,T,E);
609 if (res == NULL) {
610 Cudd_RecursiveDeref(dd, T);
611 Cudd_RecursiveDeref(dd, E);
612 return(NULL);
613 }
614 }
615 cuddDeref(T);
616 cuddDeref(E);
617
618 /* Store result. */
619 cuddCacheInsert2(dd,addBddDoThreshold,f,val,res);
620
621 return(res);
622
623} /* end of addBddDoThreshold */
624
625
626/**Function********************************************************************
627
628 Synopsis [Performs the recursive step for Cudd_addBddStrictThreshold.]
629
630 Description [Performs the recursive step for Cudd_addBddStrictThreshold.
631 Returns a pointer to the BDD if successful; NULL otherwise.]
632
633 SideEffects [None]
634
635 SeeAlso [addBddDoThreshold]
636
637******************************************************************************/
638static DdNode *
639addBddDoStrictThreshold(
640 DdManager * dd,
641 DdNode * f,
642 DdNode * val)
643{
644 DdNode *res, *T, *E;
645 DdNode *fv, *fvn;
646 int v;
647
648 statLine(dd);
649 /* Check terminal case. */
650 if (cuddIsConstant(f)) {
651 return(Cudd_NotCond(DD_ONE(dd),cuddV(f) <= cuddV(val)));
652 }
653
654 /* Check cache. */
655 res = cuddCacheLookup2(dd,addBddDoStrictThreshold,f,val);
656 if (res != NULL) return(res);
657
658 /* Recursive step. */
659 v = f->index;
660 fv = cuddT(f); fvn = cuddE(f);
661
662 T = addBddDoStrictThreshold(dd,fv,val);
663 if (T == NULL) return(NULL);
664 cuddRef(T);
665
666 E = addBddDoStrictThreshold(dd,fvn,val);
667 if (E == NULL) {
668 Cudd_RecursiveDeref(dd, T);
669 return(NULL);
670 }
671 cuddRef(E);
672 if (Cudd_IsComplement(T)) {
673 res = (T == E) ? Cudd_Not(T) : cuddUniqueInter(dd,v,Cudd_Not(T),Cudd_Not(E));
674 if (res == NULL) {
675 Cudd_RecursiveDeref(dd, T);
676 Cudd_RecursiveDeref(dd, E);
677 return(NULL);
678 }
679 res = Cudd_Not(res);
680 } else {
681 res = (T == E) ? T : cuddUniqueInter(dd,v,T,E);
682 if (res == NULL) {
683 Cudd_RecursiveDeref(dd, T);
684 Cudd_RecursiveDeref(dd, E);
685 return(NULL);
686 }
687 }
688 cuddDeref(T);
689 cuddDeref(E);
690
691 /* Store result. */
692 cuddCacheInsert2(dd,addBddDoStrictThreshold,f,val,res);
693
694 return(res);
695
696} /* end of addBddDoStrictThreshold */
697
698
699/**Function********************************************************************
700
701 Synopsis [Performs the recursive step for Cudd_addBddInterval.]
702
703 Description [Performs the recursive step for Cudd_addBddInterval.
704 Returns a pointer to the BDD if successful; NULL otherwise.]
705
706 SideEffects [None]
707
708 SeeAlso [addBddDoThreshold addBddDoStrictThreshold]
709
710******************************************************************************/
711static DdNode *
712addBddDoInterval(
713 DdManager * dd,
714 DdNode * f,
715 DdNode * l,
716 DdNode * u)
717{
718 DdNode *res, *T, *E;
719 DdNode *fv, *fvn;
720 int v;
721
722 statLine(dd);
723 /* Check terminal case. */
724 if (cuddIsConstant(f)) {
725 return(Cudd_NotCond(DD_ONE(dd),cuddV(f) < cuddV(l) || cuddV(f) > cuddV(u)));
726 }
727
728 /* Check cache. */
729 res = cuddCacheLookup(dd,DD_ADD_BDD_DO_INTERVAL_TAG,f,l,u);
730 if (res != NULL) return(res);
731
732 /* Recursive step. */
733 v = f->index;
734 fv = cuddT(f); fvn = cuddE(f);
735
736 T = addBddDoInterval(dd,fv,l,u);
737 if (T == NULL) return(NULL);
738 cuddRef(T);
739
740 E = addBddDoInterval(dd,fvn,l,u);
741 if (E == NULL) {
742 Cudd_RecursiveDeref(dd, T);
743 return(NULL);
744 }
745 cuddRef(E);
746 if (Cudd_IsComplement(T)) {
747 res = (T == E) ? Cudd_Not(T) : cuddUniqueInter(dd,v,Cudd_Not(T),Cudd_Not(E));
748 if (res == NULL) {
749 Cudd_RecursiveDeref(dd, T);
750 Cudd_RecursiveDeref(dd, E);
751 return(NULL);
752 }
753 res = Cudd_Not(res);
754 } else {
755 res = (T == E) ? T : cuddUniqueInter(dd,v,T,E);
756 if (res == NULL) {
757 Cudd_RecursiveDeref(dd, T);
758 Cudd_RecursiveDeref(dd, E);
759 return(NULL);
760 }
761 }
762 cuddDeref(T);
763 cuddDeref(E);
764
765 /* Store result. */
766 cuddCacheInsert(dd,DD_ADD_BDD_DO_INTERVAL_TAG,f,l,u,res);
767
768 return(res);
769
770} /* end of addBddDoInterval */
771
772
773/**Function********************************************************************
774
775 Synopsis [Performs the recursive step for Cudd_addBddIthBit.]
776
777 Description [Performs the recursive step for Cudd_addBddIthBit.
778 Returns a pointer to the BDD if successful; NULL otherwise.]
779
780 SideEffects [None]
781
782 SeeAlso []
783
784******************************************************************************/
785static DdNode *
786addBddDoIthBit(
787 DdManager * dd,
788 DdNode * f,
789 DdNode * index)
790{
791 DdNode *res, *T, *E;
792 DdNode *fv, *fvn;
793 int mask, value;
794 int v;
795
796 statLine(dd);
797 /* Check terminal case. */
798 if (cuddIsConstant(f)) {
799 mask = 1 << ((int) cuddV(index));
800 value = (int) cuddV(f);
801 return(Cudd_NotCond(DD_ONE(dd),(value & mask) == 0));
802 }
803
804 /* Check cache. */
805 res = cuddCacheLookup2(dd,addBddDoIthBit,f,index);
806 if (res != NULL) return(res);
807
808 /* Recursive step. */
809 v = f->index;
810 fv = cuddT(f); fvn = cuddE(f);
811
812 T = addBddDoIthBit(dd,fv,index);
813 if (T == NULL) return(NULL);
814 cuddRef(T);
815
816 E = addBddDoIthBit(dd,fvn,index);
817 if (E == NULL) {
818 Cudd_RecursiveDeref(dd, T);
819 return(NULL);
820 }
821 cuddRef(E);
822 if (Cudd_IsComplement(T)) {
823 res = (T == E) ? Cudd_Not(T) : cuddUniqueInter(dd,v,Cudd_Not(T),Cudd_Not(E));
824 if (res == NULL) {
825 Cudd_RecursiveDeref(dd, T);
826 Cudd_RecursiveDeref(dd, E);
827 return(NULL);
828 }
829 res = Cudd_Not(res);
830 } else {
831 res = (T == E) ? T : cuddUniqueInter(dd,v,T,E);
832 if (res == NULL) {
833 Cudd_RecursiveDeref(dd, T);
834 Cudd_RecursiveDeref(dd, E);
835 return(NULL);
836 }
837 }
838 cuddDeref(T);
839 cuddDeref(E);
840
841 /* Store result. */
842 cuddCacheInsert2(dd,addBddDoIthBit,f,index,res);
843
844 return(res);
845
846} /* end of addBddDoIthBit */
847
848
849/**Function********************************************************************
850
851 Synopsis [Performs the recursive step for Cudd_BddToAdd.]
852
853 Description [Performs the recursive step for Cudd_BddToAdd. Returns a
854 pointer to the resulting ADD if successful; NULL otherwise.]
855
856 SideEffects [None]
857
858 SeeAlso []
859
860******************************************************************************/
861static DdNode *
862ddBddToAddRecur(
863 DdManager * dd,
864 DdNode * B)
865{
866 DdNode *one;
867 DdNode *res, *res1, *T, *E, *Bt, *Be;
868 int complement = 0;
869
870 statLine(dd);
871 one = DD_ONE(dd);
872
873 if (Cudd_IsConstant(B)) {
874 if (B == one) {
875 res = one;
876 } else {
877 res = DD_ZERO(dd);
878 }
879 return(res);
880 }
881 /* Check visited table */
882 res = cuddCacheLookup1(dd,ddBddToAddRecur,B);
883 if (res != NULL) return(res);
884
885 if (Cudd_IsComplement(B)) {
886 complement = 1;
887 Bt = cuddT(Cudd_Regular(B));
888 Be = cuddE(Cudd_Regular(B));
889 } else {
890 Bt = cuddT(B);
891 Be = cuddE(B);
892 }
893
894 T = ddBddToAddRecur(dd, Bt);
895 if (T == NULL) return(NULL);
896 cuddRef(T);
897
898 E = ddBddToAddRecur(dd, Be);
899 if (E == NULL) {
900 Cudd_RecursiveDeref(dd, T);
901 return(NULL);
902 }
903 cuddRef(E);
904
905 /* No need to check for T == E, because it is guaranteed not to happen. */
906 res = cuddUniqueInter(dd, (int) Cudd_Regular(B)->index, T, E);
907 if (res == NULL) {
908 Cudd_RecursiveDeref(dd ,T);
909 Cudd_RecursiveDeref(dd ,E);
910 return(NULL);
911 }
912 cuddDeref(T);
913 cuddDeref(E);
914
915 if (complement) {
916 cuddRef(res);
917 res1 = cuddAddCmplRecur(dd, res);
918 if (res1 == NULL) {
919 Cudd_RecursiveDeref(dd, res);
920 return(NULL);
921 }
922 cuddRef(res1);
923 Cudd_RecursiveDeref(dd, res);
924 res = res1;
925 cuddDeref(res);
926 }
927
928 /* Store result. */
929 cuddCacheInsert1(dd,ddBddToAddRecur,B,res);
930
931 return(res);
932
933} /* end of ddBddToAddRecur */
934
935
936/**Function********************************************************************
937
938 Synopsis [Performs the recursive step of Cudd_bddTransfer.]
939
940 Description [Performs the recursive step of Cudd_bddTransfer.
941 Returns a pointer to the result if successful; NULL otherwise.]
942
943 SideEffects [None]
944
945 SeeAlso [cuddBddTransfer]
946
947******************************************************************************/
948static DdNode *
949cuddBddTransferRecur(
950 DdManager * ddS,
951 DdManager * ddD,
952 DdNode * f,
953 st_table * table)
954{
955 DdNode *ft, *fe, *t, *e, *var, *res;
956 DdNode *one, *zero;
957 int index;
958 int comple = 0;
959
960 statLine(ddD);
961 one = DD_ONE(ddD);
962 comple = Cudd_IsComplement(f);
963
964 /* Trivial cases. */
965 if (Cudd_IsConstant(f)) return(Cudd_NotCond(one, comple));
966
967 /* Make canonical to increase the utilization of the cache. */
968 f = Cudd_NotCond(f,comple);
969 /* Now f is a regular pointer to a non-constant node. */
970
971 /* Check the cache. */
972 if (st_lookup(table, f, &res))
973 return(Cudd_NotCond(res,comple));
974
975 /* Recursive step. */
976 index = f->index;
977 ft = cuddT(f); fe = cuddE(f);
978
979 t = cuddBddTransferRecur(ddS, ddD, ft, table);
980 if (t == NULL) {
981 return(NULL);
982 }
983 cuddRef(t);
984
985 e = cuddBddTransferRecur(ddS, ddD, fe, table);
986 if (e == NULL) {
987 Cudd_RecursiveDeref(ddD, t);
988 return(NULL);
989 }
990 cuddRef(e);
991
992 zero = Cudd_Not(one);
993 var = cuddUniqueInter(ddD,index,one,zero);
994 if (var == NULL) {
995 Cudd_RecursiveDeref(ddD, t);
996 Cudd_RecursiveDeref(ddD, e);
997 return(NULL);
998 }
999 res = cuddBddIteRecur(ddD,var,t,e);
1000 if (res == NULL) {
1001 Cudd_RecursiveDeref(ddD, t);
1002 Cudd_RecursiveDeref(ddD, e);
1003 return(NULL);
1004 }
1005 cuddRef(res);
1006 Cudd_RecursiveDeref(ddD, t);
1007 Cudd_RecursiveDeref(ddD, e);
1008
1009 if (st_add_direct(table, (char *) f, (char *) res) == ST_OUT_OF_MEM) {
1010 Cudd_RecursiveDeref(ddD, res);
1011 return(NULL);
1012 }
1013 return(Cudd_NotCond(res,comple));
1014
1015} /* end of cuddBddTransferRecur */
1016
Note: See TracBrowser for help on using the repository browser.