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

Last change on this file since 19 was 13, checked in by cecile, 13 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.