source: vis_dev/glu-2.3/src/cuBdd/cuddZddIsop.c @ 42

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

library glu 2.3
File size: 25.0 KB
Line 
1/**CFile***********************************************************************
2
3  FileName    [cuddZddIsop.c]
4
5  PackageName [cudd]
6
7  Synopsis    [Functions to find irredundant SOP covers as ZDDs from BDDs.]
8
9  Description [External procedures included in this module:
10                    <ul>
11                    <li> Cudd_bddIsop()
12                    <li> Cudd_zddIsop()
13                    <li> Cudd_MakeBddFromZddCover()
14                    </ul>
15               Internal procedures included in this module:
16                    <ul>
17                    <li> cuddBddIsop()
18                    <li> cuddZddIsop()
19                    <li> cuddMakeBddFromZddCover()
20                    </ul>
21               Static procedures included in this module:
22                    <ul>
23                    </ul>
24              ]
25
26  SeeAlso     []
27
28  Author      [In-Ho Moon]
29
30  Copyright   [Copyright (c) 1995-2004, Regents of the University of Colorado
31
32  All rights reserved.
33
34  Redistribution and use in source and binary forms, with or without
35  modification, are permitted provided that the following conditions
36  are met:
37
38  Redistributions of source code must retain the above copyright
39  notice, this list of conditions and the following disclaimer.
40
41  Redistributions in binary form must reproduce the above copyright
42  notice, this list of conditions and the following disclaimer in the
43  documentation and/or other materials provided with the distribution.
44
45  Neither the name of the University of Colorado nor the names of its
46  contributors may be used to endorse or promote products derived from
47  this software without specific prior written permission.
48
49  THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
50  "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
51  LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
52  FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
53  COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
54  INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
55  BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
56  LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
57  CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
58  LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
59  ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
60  POSSIBILITY OF SUCH DAMAGE.]
61
62******************************************************************************/
63
64#include "util.h"
65#include "cuddInt.h"
66
67/*---------------------------------------------------------------------------*/
68/* Constant declarations                                                     */
69/*---------------------------------------------------------------------------*/
70
71
72/*---------------------------------------------------------------------------*/
73/* Stucture declarations                                                     */
74/*---------------------------------------------------------------------------*/
75
76
77/*---------------------------------------------------------------------------*/
78/* Type declarations                                                         */
79/*---------------------------------------------------------------------------*/
80
81
82/*---------------------------------------------------------------------------*/
83/* Variable declarations                                                     */
84/*---------------------------------------------------------------------------*/
85
86#ifndef lint
87static char rcsid[] DD_UNUSED = "$Id: cuddZddIsop.c,v 1.20 2009/02/19 16:26:12 fabio Exp $";
88#endif
89
90/*---------------------------------------------------------------------------*/
91/* Macro declarations                                                        */
92/*---------------------------------------------------------------------------*/
93
94
95/**AutomaticStart*************************************************************/
96
97/*---------------------------------------------------------------------------*/
98/* Static function prototypes                                                */
99/*---------------------------------------------------------------------------*/
100
101
102/**AutomaticEnd***************************************************************/
103
104/*---------------------------------------------------------------------------*/
105/* Definition of exported functions                                          */
106/*---------------------------------------------------------------------------*/
107
108/**Function********************************************************************
109
110  Synopsis    [Computes an ISOP in ZDD form from BDDs.]
111
112  Description [Computes an irredundant sum of products (ISOP) in ZDD
113  form from BDDs. The two BDDs L and U represent the lower bound and
114  the upper bound, respectively, of the function. The ISOP uses two
115  ZDD variables for each BDD variable: One for the positive literal,
116  and one for the negative literal. These two variables should be
117  adjacent in the ZDD order. The two ZDD variables corresponding to
118  BDD variable <code>i</code> should have indices <code>2i</code> and
119  <code>2i+1</code>.  The result of this procedure depends on the
120  variable order. If successful, Cudd_zddIsop returns the BDD for
121  the function chosen from the interval. The ZDD representing the
122  irredundant cover is returned as a side effect in zdd_I. In case of
123  failure, NULL is returned.]
124
125  SideEffects [zdd_I holds the pointer to the ZDD for the ISOP on
126  successful return.]
127
128  SeeAlso     [Cudd_bddIsop Cudd_zddVarsFromBddVars]
129
130******************************************************************************/
131DdNode  *
132Cudd_zddIsop(
133  DdManager * dd,
134  DdNode * L,
135  DdNode * U,
136  DdNode ** zdd_I)
137{
138    DdNode      *res;
139    int         autoDynZ;
140
141    autoDynZ = dd->autoDynZ;
142    dd->autoDynZ = 0;
143
144    do {
145        dd->reordered = 0;
146        res = cuddZddIsop(dd, L, U, zdd_I);
147    } while (dd->reordered == 1);
148    dd->autoDynZ = autoDynZ;
149    return(res);
150
151} /* end of Cudd_zddIsop */
152
153
154/**Function********************************************************************
155
156  Synopsis    [Computes a BDD in the interval between L and U with a
157  simple sum-of-produuct cover.]
158
159  Description [Computes a BDD in the interval between L and U with a
160  simple sum-of-produuct cover. This procedure is similar to
161  Cudd_zddIsop, but it does not return the ZDD for the cover. Returns
162  a pointer to the BDD if successful; NULL otherwise.]
163
164  SideEffects [None]
165
166  SeeAlso     [Cudd_zddIsop]
167
168******************************************************************************/
169DdNode  *
170Cudd_bddIsop(
171  DdManager * dd,
172  DdNode * L,
173  DdNode * U)
174{
175    DdNode      *res;
176
177    do {
178        dd->reordered = 0;
179        res = cuddBddIsop(dd, L, U);
180    } while (dd->reordered == 1);
181    return(res);
182
183} /* end of Cudd_bddIsop */
184
185
186/**Function********************************************************************
187
188  Synopsis [Converts a ZDD cover to a BDD graph.]
189
190  Description [Converts a ZDD cover to a BDD graph. If successful, it
191  returns a BDD node, otherwise it returns NULL.]
192
193  SideEffects []
194
195  SeeAlso     [cuddMakeBddFromZddCover]
196
197******************************************************************************/
198DdNode  *
199Cudd_MakeBddFromZddCover(
200  DdManager * dd,
201  DdNode * node)
202{
203    DdNode      *res;
204
205    do {
206        dd->reordered = 0;
207        res = cuddMakeBddFromZddCover(dd, node);
208    } while (dd->reordered == 1);
209    return(res);
210} /* end of Cudd_MakeBddFromZddCover */
211
212
213/*---------------------------------------------------------------------------*/
214/* Definition of internal functions                                          */
215/*---------------------------------------------------------------------------*/
216
217
218/**Function********************************************************************
219
220  Synopsis [Performs the recursive step of Cudd_zddIsop.]
221
222  Description []
223
224  SideEffects [None]
225
226  SeeAlso     [Cudd_zddIsop]
227
228******************************************************************************/
229DdNode  *
230cuddZddIsop(
231  DdManager * dd,
232  DdNode * L,
233  DdNode * U,
234  DdNode ** zdd_I)
235{
236    DdNode      *one = DD_ONE(dd);
237    DdNode      *zero = Cudd_Not(one);
238    DdNode      *zdd_one = DD_ONE(dd);
239    DdNode      *zdd_zero = DD_ZERO(dd);
240    int         v, top_l, top_u;
241    DdNode      *Lsub0, *Usub0, *Lsub1, *Usub1, *Ld, *Ud;
242    DdNode      *Lsuper0, *Usuper0, *Lsuper1, *Usuper1;
243    DdNode      *Isub0, *Isub1, *Id;
244    DdNode      *zdd_Isub0, *zdd_Isub1, *zdd_Id;
245    DdNode      *x;
246    DdNode      *term0, *term1, *sum;
247    DdNode      *Lv, *Uv, *Lnv, *Unv;
248    DdNode      *r, *y, *z;
249    int         index;
250    DD_CTFP     cacheOp;
251
252    statLine(dd);
253    if (L == zero) {
254        *zdd_I = zdd_zero;
255        return(zero);
256    }
257    if (U == one) {
258        *zdd_I = zdd_one;
259        return(one);
260    }
261
262    if (U == zero || L == one) {
263        printf("*** ERROR : illegal condition for ISOP (U < L).\n");
264        exit(1);
265    }
266
267    /* Check the cache. We store two results for each recursive call.
268    ** One is the BDD, and the other is the ZDD. Both are needed.
269    ** Hence we need a double hit in the cache to terminate the
270    ** recursion. Clearly, collisions may evict only one of the two
271    ** results. */
272    cacheOp = (DD_CTFP) cuddZddIsop;
273    r = cuddCacheLookup2(dd, cuddBddIsop, L, U);
274    if (r) {
275        *zdd_I = cuddCacheLookup2Zdd(dd, cacheOp, L, U);
276        if (*zdd_I)
277            return(r);
278        else {
279            /* The BDD result may have been dead. In that case
280            ** cuddCacheLookup2 would have called cuddReclaim,
281            ** whose effects we now have to undo. */
282            cuddRef(r);
283            Cudd_RecursiveDeref(dd, r);
284        }
285    }
286
287    top_l = dd->perm[Cudd_Regular(L)->index];
288    top_u = dd->perm[Cudd_Regular(U)->index];
289    v = ddMin(top_l, top_u);
290
291    /* Compute cofactors. */
292    if (top_l == v) {
293        index = Cudd_Regular(L)->index;
294        Lv = Cudd_T(L);
295        Lnv = Cudd_E(L);
296        if (Cudd_IsComplement(L)) {
297            Lv = Cudd_Not(Lv);
298            Lnv = Cudd_Not(Lnv);
299        }
300    }
301    else {
302        index = Cudd_Regular(U)->index;
303        Lv = Lnv = L;
304    }
305
306    if (top_u == v) {
307        Uv = Cudd_T(U);
308        Unv = Cudd_E(U);
309        if (Cudd_IsComplement(U)) {
310            Uv = Cudd_Not(Uv);
311            Unv = Cudd_Not(Unv);
312        }
313    }
314    else {
315        Uv = Unv = U;
316    }
317
318    Lsub0 = cuddBddAndRecur(dd, Lnv, Cudd_Not(Uv));
319    if (Lsub0 == NULL)
320        return(NULL);
321    Cudd_Ref(Lsub0);
322    Usub0 = Unv;
323    Lsub1 = cuddBddAndRecur(dd, Lv, Cudd_Not(Unv));
324    if (Lsub1 == NULL) {
325        Cudd_RecursiveDeref(dd, Lsub0);
326        return(NULL);
327    }
328    Cudd_Ref(Lsub1);
329    Usub1 = Uv;
330
331    Isub0 = cuddZddIsop(dd, Lsub0, Usub0, &zdd_Isub0);
332    if (Isub0 == NULL) {
333        Cudd_RecursiveDeref(dd, Lsub0);
334        Cudd_RecursiveDeref(dd, Lsub1);
335        return(NULL);
336    }
337    /*
338    if ((!cuddIsConstant(Cudd_Regular(Isub0))) &&
339        (Cudd_Regular(Isub0)->index != zdd_Isub0->index / 2 ||
340        dd->permZ[index * 2] > dd->permZ[zdd_Isub0->index])) {
341        printf("*** ERROR : illegal permutation in ZDD. ***\n");
342    }
343    */
344    Cudd_Ref(Isub0);
345    Cudd_Ref(zdd_Isub0);
346    Isub1 = cuddZddIsop(dd, Lsub1, Usub1, &zdd_Isub1);
347    if (Isub1 == NULL) {
348        Cudd_RecursiveDeref(dd, Lsub0);
349        Cudd_RecursiveDeref(dd, Lsub1);
350        Cudd_RecursiveDeref(dd, Isub0);
351        Cudd_RecursiveDerefZdd(dd, zdd_Isub0);
352        return(NULL);
353    }
354    /*
355    if ((!cuddIsConstant(Cudd_Regular(Isub1))) &&
356        (Cudd_Regular(Isub1)->index != zdd_Isub1->index / 2 ||
357        dd->permZ[index * 2] > dd->permZ[zdd_Isub1->index])) {
358        printf("*** ERROR : illegal permutation in ZDD. ***\n");
359    }
360    */
361    Cudd_Ref(Isub1);
362    Cudd_Ref(zdd_Isub1);
363    Cudd_RecursiveDeref(dd, Lsub0);
364    Cudd_RecursiveDeref(dd, Lsub1);
365
366    Lsuper0 = cuddBddAndRecur(dd, Lnv, Cudd_Not(Isub0));
367    if (Lsuper0 == NULL) {
368        Cudd_RecursiveDeref(dd, Isub0);
369        Cudd_RecursiveDerefZdd(dd, zdd_Isub0);
370        Cudd_RecursiveDeref(dd, Isub1);
371        Cudd_RecursiveDerefZdd(dd, zdd_Isub1);
372        return(NULL);
373    }
374    Cudd_Ref(Lsuper0);
375    Lsuper1 = cuddBddAndRecur(dd, Lv, Cudd_Not(Isub1));
376    if (Lsuper1 == NULL) {
377        Cudd_RecursiveDeref(dd, Isub0);
378        Cudd_RecursiveDerefZdd(dd, zdd_Isub0);
379        Cudd_RecursiveDeref(dd, Isub1);
380        Cudd_RecursiveDerefZdd(dd, zdd_Isub1);
381        Cudd_RecursiveDeref(dd, Lsuper0);
382        return(NULL);
383    }
384    Cudd_Ref(Lsuper1);
385    Usuper0 = Unv;
386    Usuper1 = Uv;
387
388    /* Ld = Lsuper0 + Lsuper1 */
389    Ld = cuddBddAndRecur(dd, Cudd_Not(Lsuper0), Cudd_Not(Lsuper1));
390    if (Ld == NULL) {
391        Cudd_RecursiveDeref(dd, Isub0);
392        Cudd_RecursiveDerefZdd(dd, zdd_Isub0);
393        Cudd_RecursiveDeref(dd, Isub1);
394        Cudd_RecursiveDerefZdd(dd, zdd_Isub1);
395        Cudd_RecursiveDeref(dd, Lsuper0);
396        Cudd_RecursiveDeref(dd, Lsuper1);
397        return(NULL);
398    }
399    Ld = Cudd_Not(Ld);
400    Cudd_Ref(Ld);
401    /* Ud = Usuper0 * Usuper1 */
402    Ud = cuddBddAndRecur(dd, Usuper0, Usuper1);
403    if (Ud == NULL) {
404        Cudd_RecursiveDeref(dd, Isub0);
405        Cudd_RecursiveDerefZdd(dd, zdd_Isub0);
406        Cudd_RecursiveDeref(dd, Isub1);
407        Cudd_RecursiveDerefZdd(dd, zdd_Isub1);
408        Cudd_RecursiveDeref(dd, Lsuper0);
409        Cudd_RecursiveDeref(dd, Lsuper1);
410        Cudd_RecursiveDeref(dd, Ld);
411        return(NULL);
412    }
413    Cudd_Ref(Ud);
414    Cudd_RecursiveDeref(dd, Lsuper0);
415    Cudd_RecursiveDeref(dd, Lsuper1);
416
417    Id = cuddZddIsop(dd, Ld, Ud, &zdd_Id);
418    if (Id == NULL) {
419        Cudd_RecursiveDeref(dd, Isub0);
420        Cudd_RecursiveDerefZdd(dd, zdd_Isub0);
421        Cudd_RecursiveDeref(dd, Isub1);
422        Cudd_RecursiveDerefZdd(dd, zdd_Isub1);
423        Cudd_RecursiveDeref(dd, Ld);
424        Cudd_RecursiveDeref(dd, Ud);
425        return(NULL);
426    }
427    /*
428    if ((!cuddIsConstant(Cudd_Regular(Id))) &&
429        (Cudd_Regular(Id)->index != zdd_Id->index / 2 ||
430        dd->permZ[index * 2] > dd->permZ[zdd_Id->index])) {
431        printf("*** ERROR : illegal permutation in ZDD. ***\n");
432    }
433    */
434    Cudd_Ref(Id);
435    Cudd_Ref(zdd_Id);
436    Cudd_RecursiveDeref(dd, Ld);
437    Cudd_RecursiveDeref(dd, Ud);
438
439    x = cuddUniqueInter(dd, index, one, zero);
440    if (x == NULL) {
441        Cudd_RecursiveDeref(dd, Isub0);
442        Cudd_RecursiveDerefZdd(dd, zdd_Isub0);
443        Cudd_RecursiveDeref(dd, Isub1);
444        Cudd_RecursiveDerefZdd(dd, zdd_Isub1);
445        Cudd_RecursiveDeref(dd, Id);
446        Cudd_RecursiveDerefZdd(dd, zdd_Id);
447        return(NULL);
448    }
449    Cudd_Ref(x);
450    /* term0 = x * Isub0 */
451    term0 = cuddBddAndRecur(dd, Cudd_Not(x), Isub0);
452    if (term0 == NULL) {
453        Cudd_RecursiveDeref(dd, Isub0);
454        Cudd_RecursiveDerefZdd(dd, zdd_Isub0);
455        Cudd_RecursiveDeref(dd, Isub1);
456        Cudd_RecursiveDerefZdd(dd, zdd_Isub1);
457        Cudd_RecursiveDeref(dd, Id);
458        Cudd_RecursiveDerefZdd(dd, zdd_Id);
459        Cudd_RecursiveDeref(dd, x);
460        return(NULL);
461    }
462    Cudd_Ref(term0);
463    Cudd_RecursiveDeref(dd, Isub0);
464    /* term1 = x * Isub1 */
465    term1 = cuddBddAndRecur(dd, x, Isub1);
466    if (term1 == NULL) {
467        Cudd_RecursiveDerefZdd(dd, zdd_Isub0);
468        Cudd_RecursiveDeref(dd, Isub1);
469        Cudd_RecursiveDerefZdd(dd, zdd_Isub1);
470        Cudd_RecursiveDeref(dd, Id);
471        Cudd_RecursiveDerefZdd(dd, zdd_Id);
472        Cudd_RecursiveDeref(dd, x);
473        Cudd_RecursiveDeref(dd, term0);
474        return(NULL);
475    }
476    Cudd_Ref(term1);
477    Cudd_RecursiveDeref(dd, x);
478    Cudd_RecursiveDeref(dd, Isub1);
479    /* sum = term0 + term1 */
480    sum = cuddBddAndRecur(dd, Cudd_Not(term0), Cudd_Not(term1));
481    if (sum == NULL) {
482        Cudd_RecursiveDerefZdd(dd, zdd_Isub0);
483        Cudd_RecursiveDerefZdd(dd, zdd_Isub1);
484        Cudd_RecursiveDeref(dd, Id);
485        Cudd_RecursiveDerefZdd(dd, zdd_Id);
486        Cudd_RecursiveDeref(dd, term0);
487        Cudd_RecursiveDeref(dd, term1);
488        return(NULL);
489    }
490    sum = Cudd_Not(sum);
491    Cudd_Ref(sum);
492    Cudd_RecursiveDeref(dd, term0);
493    Cudd_RecursiveDeref(dd, term1);
494    /* r = sum + Id */
495    r = cuddBddAndRecur(dd, Cudd_Not(sum), Cudd_Not(Id));
496    r = Cudd_NotCond(r, r != NULL);
497    if (r == NULL) {
498        Cudd_RecursiveDerefZdd(dd, zdd_Isub0);
499        Cudd_RecursiveDerefZdd(dd, zdd_Isub1);
500        Cudd_RecursiveDeref(dd, Id);
501        Cudd_RecursiveDerefZdd(dd, zdd_Id);
502        Cudd_RecursiveDeref(dd, sum);
503        return(NULL);
504    }
505    Cudd_Ref(r);
506    Cudd_RecursiveDeref(dd, sum);
507    Cudd_RecursiveDeref(dd, Id);
508
509    if (zdd_Isub0 != zdd_zero) {
510        z = cuddZddGetNodeIVO(dd, index * 2 + 1, zdd_Isub0, zdd_Id);
511        if (z == NULL) {
512            Cudd_RecursiveDerefZdd(dd, zdd_Isub0);
513            Cudd_RecursiveDerefZdd(dd, zdd_Isub1);
514            Cudd_RecursiveDerefZdd(dd, zdd_Id);
515            Cudd_RecursiveDeref(dd, r);
516            return(NULL);
517        }
518    }
519    else {
520        z = zdd_Id;
521    }
522    Cudd_Ref(z);
523    if (zdd_Isub1 != zdd_zero) {
524        y = cuddZddGetNodeIVO(dd, index * 2, zdd_Isub1, z);
525        if (y == NULL) {
526            Cudd_RecursiveDerefZdd(dd, zdd_Isub0);
527            Cudd_RecursiveDerefZdd(dd, zdd_Isub1);
528            Cudd_RecursiveDerefZdd(dd, zdd_Id);
529            Cudd_RecursiveDeref(dd, r);
530            Cudd_RecursiveDerefZdd(dd, z);
531            return(NULL);
532        }
533    }
534    else
535        y = z;
536    Cudd_Ref(y);
537
538    Cudd_RecursiveDerefZdd(dd, zdd_Isub0);
539    Cudd_RecursiveDerefZdd(dd, zdd_Isub1);
540    Cudd_RecursiveDerefZdd(dd, zdd_Id);
541    Cudd_RecursiveDerefZdd(dd, z);
542
543    cuddCacheInsert2(dd, cuddBddIsop, L, U, r);
544    cuddCacheInsert2(dd, cacheOp, L, U, y);
545
546    Cudd_Deref(r);
547    Cudd_Deref(y);
548    *zdd_I = y;
549    /*
550    if (Cudd_Regular(r)->index != y->index / 2) {
551        printf("*** ERROR : mismatch in indices between BDD and ZDD. ***\n");
552    }
553    */
554    return(r);
555
556} /* end of cuddZddIsop */
557
558
559/**Function********************************************************************
560
561  Synopsis [Performs the recursive step of Cudd_bddIsop.]
562
563  Description []
564
565  SideEffects [None]
566
567  SeeAlso     [Cudd_bddIsop]
568
569******************************************************************************/
570DdNode  *
571cuddBddIsop(
572  DdManager * dd,
573  DdNode * L,
574  DdNode * U)
575{
576    DdNode      *one = DD_ONE(dd);
577    DdNode      *zero = Cudd_Not(one);
578    int         v, top_l, top_u;
579    DdNode      *Lsub0, *Usub0, *Lsub1, *Usub1, *Ld, *Ud;
580    DdNode      *Lsuper0, *Usuper0, *Lsuper1, *Usuper1;
581    DdNode      *Isub0, *Isub1, *Id;
582    DdNode      *x;
583    DdNode      *term0, *term1, *sum;
584    DdNode      *Lv, *Uv, *Lnv, *Unv;
585    DdNode      *r;
586    int         index;
587
588    statLine(dd);
589    if (L == zero)
590        return(zero);
591    if (U == one)
592        return(one);
593
594    /* Check cache */
595    r = cuddCacheLookup2(dd, cuddBddIsop, L, U);
596    if (r)
597        return(r);
598
599    top_l = dd->perm[Cudd_Regular(L)->index];
600    top_u = dd->perm[Cudd_Regular(U)->index];
601    v = ddMin(top_l, top_u);
602
603    /* Compute cofactors */
604    if (top_l == v) {
605        index = Cudd_Regular(L)->index;
606        Lv = Cudd_T(L);
607        Lnv = Cudd_E(L);
608        if (Cudd_IsComplement(L)) {
609            Lv = Cudd_Not(Lv);
610            Lnv = Cudd_Not(Lnv);
611        }
612    }
613    else {
614        index = Cudd_Regular(U)->index;
615        Lv = Lnv = L;
616    }
617
618    if (top_u == v) {
619        Uv = Cudd_T(U);
620        Unv = Cudd_E(U);
621        if (Cudd_IsComplement(U)) {
622            Uv = Cudd_Not(Uv);
623            Unv = Cudd_Not(Unv);
624        }
625    }
626    else {
627        Uv = Unv = U;
628    }
629
630    Lsub0 = cuddBddAndRecur(dd, Lnv, Cudd_Not(Uv));
631    if (Lsub0 == NULL)
632        return(NULL);
633    Cudd_Ref(Lsub0);
634    Usub0 = Unv;
635    Lsub1 = cuddBddAndRecur(dd, Lv, Cudd_Not(Unv));
636    if (Lsub1 == NULL) {
637        Cudd_RecursiveDeref(dd, Lsub0);
638        return(NULL);
639    }
640    Cudd_Ref(Lsub1);
641    Usub1 = Uv;
642
643    Isub0 = cuddBddIsop(dd, Lsub0, Usub0);
644    if (Isub0 == NULL) {
645        Cudd_RecursiveDeref(dd, Lsub0);
646        Cudd_RecursiveDeref(dd, Lsub1);
647        return(NULL);
648    }
649    Cudd_Ref(Isub0);
650    Isub1 = cuddBddIsop(dd, Lsub1, Usub1);
651    if (Isub1 == NULL) {
652        Cudd_RecursiveDeref(dd, Lsub0);
653        Cudd_RecursiveDeref(dd, Lsub1);
654        Cudd_RecursiveDeref(dd, Isub0);
655        return(NULL);
656    }
657    Cudd_Ref(Isub1);
658    Cudd_RecursiveDeref(dd, Lsub0);
659    Cudd_RecursiveDeref(dd, Lsub1);
660
661    Lsuper0 = cuddBddAndRecur(dd, Lnv, Cudd_Not(Isub0));
662    if (Lsuper0 == NULL) {
663        Cudd_RecursiveDeref(dd, Isub0);
664        Cudd_RecursiveDeref(dd, Isub1);
665        return(NULL);
666    }
667    Cudd_Ref(Lsuper0);
668    Lsuper1 = cuddBddAndRecur(dd, Lv, Cudd_Not(Isub1));
669    if (Lsuper1 == NULL) {
670        Cudd_RecursiveDeref(dd, Isub0);
671        Cudd_RecursiveDeref(dd, Isub1);
672        Cudd_RecursiveDeref(dd, Lsuper0);
673        return(NULL);
674    }
675    Cudd_Ref(Lsuper1);
676    Usuper0 = Unv;
677    Usuper1 = Uv;
678
679    /* Ld = Lsuper0 + Lsuper1 */
680    Ld = cuddBddAndRecur(dd, Cudd_Not(Lsuper0), Cudd_Not(Lsuper1));
681    Ld = Cudd_NotCond(Ld, Ld != NULL);
682    if (Ld == NULL) {
683        Cudd_RecursiveDeref(dd, Isub0);
684        Cudd_RecursiveDeref(dd, Isub1);
685        Cudd_RecursiveDeref(dd, Lsuper0);
686        Cudd_RecursiveDeref(dd, Lsuper1);
687        return(NULL);
688    }
689    Cudd_Ref(Ld);
690    Ud = cuddBddAndRecur(dd, Usuper0, Usuper1);
691    if (Ud == NULL) {
692        Cudd_RecursiveDeref(dd, Isub0);
693        Cudd_RecursiveDeref(dd, Isub1);
694        Cudd_RecursiveDeref(dd, Lsuper0);
695        Cudd_RecursiveDeref(dd, Lsuper1);
696        Cudd_RecursiveDeref(dd, Ld);
697        return(NULL);
698    }
699    Cudd_Ref(Ud);
700    Cudd_RecursiveDeref(dd, Lsuper0);
701    Cudd_RecursiveDeref(dd, Lsuper1);
702
703    Id = cuddBddIsop(dd, Ld, Ud);
704    if (Id == NULL) {
705        Cudd_RecursiveDeref(dd, Isub0);
706        Cudd_RecursiveDeref(dd, Isub1);
707        Cudd_RecursiveDeref(dd, Ld);
708        Cudd_RecursiveDeref(dd, Ud);
709        return(NULL);
710    }
711    Cudd_Ref(Id);
712    Cudd_RecursiveDeref(dd, Ld);
713    Cudd_RecursiveDeref(dd, Ud);
714
715    x = cuddUniqueInter(dd, index, one, zero);
716    if (x == NULL) {
717        Cudd_RecursiveDeref(dd, Isub0);
718        Cudd_RecursiveDeref(dd, Isub1);
719        Cudd_RecursiveDeref(dd, Id);
720        return(NULL);
721    }
722    Cudd_Ref(x);
723    term0 = cuddBddAndRecur(dd, Cudd_Not(x), Isub0);
724    if (term0 == NULL) {
725        Cudd_RecursiveDeref(dd, Isub0);
726        Cudd_RecursiveDeref(dd, Isub1);
727        Cudd_RecursiveDeref(dd, Id);
728        Cudd_RecursiveDeref(dd, x);
729        return(NULL);
730    }
731    Cudd_Ref(term0);
732    Cudd_RecursiveDeref(dd, Isub0);
733    term1 = cuddBddAndRecur(dd, x, Isub1);
734    if (term1 == NULL) {
735        Cudd_RecursiveDeref(dd, Isub1);
736        Cudd_RecursiveDeref(dd, Id);
737        Cudd_RecursiveDeref(dd, x);
738        Cudd_RecursiveDeref(dd, term0);
739        return(NULL);
740    }
741    Cudd_Ref(term1);
742    Cudd_RecursiveDeref(dd, x);
743    Cudd_RecursiveDeref(dd, Isub1);
744    /* sum = term0 + term1 */
745    sum = cuddBddAndRecur(dd, Cudd_Not(term0), Cudd_Not(term1));
746    sum = Cudd_NotCond(sum, sum != NULL);
747    if (sum == NULL) {
748        Cudd_RecursiveDeref(dd, Id);
749        Cudd_RecursiveDeref(dd, term0);
750        Cudd_RecursiveDeref(dd, term1);
751        return(NULL);
752    }
753    Cudd_Ref(sum);
754    Cudd_RecursiveDeref(dd, term0);
755    Cudd_RecursiveDeref(dd, term1);
756    /* r = sum + Id */
757    r = cuddBddAndRecur(dd, Cudd_Not(sum), Cudd_Not(Id));
758    r = Cudd_NotCond(r, r != NULL);
759    if (r == NULL) {
760        Cudd_RecursiveDeref(dd, Id);
761        Cudd_RecursiveDeref(dd, sum);
762        return(NULL);
763    }
764    Cudd_Ref(r);
765    Cudd_RecursiveDeref(dd, sum);
766    Cudd_RecursiveDeref(dd, Id);
767
768    cuddCacheInsert2(dd, cuddBddIsop, L, U, r);
769
770    Cudd_Deref(r);
771    return(r);
772
773} /* end of cuddBddIsop */
774
775
776/**Function********************************************************************
777
778  Synopsis [Converts a ZDD cover to a BDD graph.]
779
780  Description [Converts a ZDD cover to a BDD graph. If successful, it
781  returns a BDD node, otherwise it returns NULL. It is a recursive
782  algorithm as the following. First computes 3 cofactors of a ZDD cover;
783  f1, f0 and fd. Second, compute BDDs(b1, b0 and bd) of f1, f0 and fd.
784  Third, compute T=b1+bd and E=b0+bd. Fourth, compute ITE(v,T,E) where v
785  is the variable which has the index of the top node of the ZDD cover.
786  In this case, since the index of v can be larger than either one of T or
787  one of E, cuddUniqueInterIVO is called, here IVO stands for
788  independent variable ordering.]
789
790  SideEffects []
791
792  SeeAlso     [Cudd_MakeBddFromZddCover]
793
794******************************************************************************/
795DdNode  *
796cuddMakeBddFromZddCover(
797  DdManager * dd,
798  DdNode * node)
799{
800    DdNode      *neW;
801    int         v;
802    DdNode      *f1, *f0, *fd;
803    DdNode      *b1, *b0, *bd;
804    DdNode      *T, *E;
805
806    statLine(dd);
807    if (node == dd->one)
808        return(dd->one);
809    if (node == dd->zero)
810        return(Cudd_Not(dd->one));
811
812    /* Check cache */
813    neW = cuddCacheLookup1(dd, cuddMakeBddFromZddCover, node);
814    if (neW)
815        return(neW);
816
817    v = Cudd_Regular(node)->index;      /* either yi or zi */
818    if (cuddZddGetCofactors3(dd, node, v, &f1, &f0, &fd)) return(NULL);
819    Cudd_Ref(f1);
820    Cudd_Ref(f0);
821    Cudd_Ref(fd);
822
823    b1 = cuddMakeBddFromZddCover(dd, f1);
824    if (!b1) {
825        Cudd_RecursiveDerefZdd(dd, f1);
826        Cudd_RecursiveDerefZdd(dd, f0);
827        Cudd_RecursiveDerefZdd(dd, fd);
828        return(NULL);
829    }
830    Cudd_Ref(b1);
831    b0 = cuddMakeBddFromZddCover(dd, f0);
832    if (!b0) {
833        Cudd_RecursiveDerefZdd(dd, f1);
834        Cudd_RecursiveDerefZdd(dd, f0);
835        Cudd_RecursiveDerefZdd(dd, fd);
836        Cudd_RecursiveDeref(dd, b1);
837        return(NULL);
838    }
839    Cudd_Ref(b0);
840    Cudd_RecursiveDerefZdd(dd, f1);
841    Cudd_RecursiveDerefZdd(dd, f0);
842    if (fd != dd->zero) {
843        bd = cuddMakeBddFromZddCover(dd, fd);
844        if (!bd) {
845            Cudd_RecursiveDerefZdd(dd, fd);
846            Cudd_RecursiveDeref(dd, b1);
847            Cudd_RecursiveDeref(dd, b0);
848            return(NULL);
849        }
850        Cudd_Ref(bd);
851        Cudd_RecursiveDerefZdd(dd, fd);
852
853        T = cuddBddAndRecur(dd, Cudd_Not(b1), Cudd_Not(bd));
854        if (!T) {
855            Cudd_RecursiveDeref(dd, b1);
856            Cudd_RecursiveDeref(dd, b0);
857            Cudd_RecursiveDeref(dd, bd);
858            return(NULL);
859        }
860        T = Cudd_NotCond(T, T != NULL);
861        Cudd_Ref(T);
862        Cudd_RecursiveDeref(dd, b1);
863        E = cuddBddAndRecur(dd, Cudd_Not(b0), Cudd_Not(bd));
864        if (!E) {
865            Cudd_RecursiveDeref(dd, b0);
866            Cudd_RecursiveDeref(dd, bd);
867            Cudd_RecursiveDeref(dd, T);
868            return(NULL);
869        }
870        E = Cudd_NotCond(E, E != NULL);
871        Cudd_Ref(E);
872        Cudd_RecursiveDeref(dd, b0);
873        Cudd_RecursiveDeref(dd, bd);
874    }
875    else {
876        Cudd_RecursiveDerefZdd(dd, fd);
877        T = b1;
878        E = b0;
879    }
880
881    if (Cudd_IsComplement(T)) {
882        neW = cuddUniqueInterIVO(dd, v / 2, Cudd_Not(T), Cudd_Not(E));
883        if (!neW) {
884            Cudd_RecursiveDeref(dd, T);
885            Cudd_RecursiveDeref(dd, E);
886            return(NULL);
887        }
888        neW = Cudd_Not(neW);
889    }
890    else {
891        neW = cuddUniqueInterIVO(dd, v / 2, T, E);
892        if (!neW) {
893            Cudd_RecursiveDeref(dd, T);
894            Cudd_RecursiveDeref(dd, E);
895            return(NULL);
896        }
897    }
898    Cudd_Ref(neW);
899    Cudd_RecursiveDeref(dd, T);
900    Cudd_RecursiveDeref(dd, E);
901
902    cuddCacheInsert1(dd, cuddMakeBddFromZddCover, node, neW);
903    Cudd_Deref(neW);
904    return(neW);
905
906} /* end of cuddMakeBddFromZddCover */
907
908
909/*---------------------------------------------------------------------------*/
910/* Definition of static functions                                            */
911/*---------------------------------------------------------------------------*/
Note: See TracBrowser for help on using the repository browser.