abc/src/bdd/cudd/cuddZddIsop.c
/**Function********************************************************************

  Synopsis [Converts a ZDD cover to a BDD graph.]

  Description [Converts a ZDD cover to a BDD graph. If successful, it
  returns a BDD node, otherwise it returns NULL. It is a recursive
  algorithm as the following. First computes 3 cofactors of a ZDD cover;
  f1, f0 and fd. Second, compute BDDs(b1, b0 and bd) of f1, f0 and fd.
  Third, compute T=b1+bd and E=b0+bd. Fourth, compute ITE(v,T,E) where v
  is the variable which has the index of the top node of the ZDD cover.
  In this case, since the index of v can be larger than either one of T or
  one of E, cuddUniqueInterIVO is called, here IVO stands for
  independent variable ordering.]

  SideEffects []

  SeeAlso     [Cudd_MakeBddFromZddCover]

******************************************************************************/
Function
Synopsis [Converts a ZDD cover to a BDD graph.]

Description [Converts a ZDD cover to a BDD graph. If successful, it
returns a BDD node, otherwise it returns NULL. It is a recursive
algorithm as the following. First computes 3 cofactors of a ZDD cover;
f1, f0 and fd. Second, compute BDDs(b1, b0 and bd) of f1, f0 and fd.
Third, compute T=b1+bd and E=b0+bd. Fourth, compute ITE(v,T,E) where v
is the variable which has the index of the top node of the ZDD cover.
In this case, since the index of v can be larger than either one of T or
one of E, cuddUniqueInterIVO is called, here IVO stands for
independent variable ordering.]




Function Synopsis [ Converts a ZDD cover to a BDD graph . ] Description [ Converts a ZDD cover to a BDD graph . If successful it returns a BDD node otherwise it returns NULL . It is a recursive algorithm as the following . First computes 3 cofactors of a ZDD cover ; f1 f0 and fd . Second compute BDDs ( b1 b0 and bd ) of f1 f0 and fd . Third compute T = b1 + bd and E = b0 + bd . Fourth compute ITE ( v T E ) where v is the variable which has the index of the top node of the ZDD cover . In this case since the index of v can be larger than either one of T or one of E cuddUniqueInterIVO is called here IVO stands for independent variable ordering . ]
DdNode  *
cuddMakeBddFromZddCover(
  DdManager * dd,
  DdNode * node)
{
    DdNode      *neW;
    int         v;
    DdNode      *f1, *f0, *fd;
    DdNode      *b1, *b0, *bd;
    DdNode      *T, *E;
    statLine(dd);
    if (node == dd->one)
        return(dd->one);
    if (node == dd->zero)
        return(Cudd_Not(dd->one));
    neW = cuddCacheLookup1(dd, cuddMakeBddFromZddCover, node);
    if (neW)
        return(neW);
    v = Cudd_Regular(node)->index;      
    if (cuddZddGetCofactors3(dd, node, v, &f1, &f0, &fd)) return(NULL);
    Cudd_Ref(f1);
    Cudd_Ref(f0);
    Cudd_Ref(fd);
    b1 = cuddMakeBddFromZddCover(dd, f1);
    if (!b1) {
        Cudd_RecursiveDerefZdd(dd, f1);
        Cudd_RecursiveDerefZdd(dd, f0);
        Cudd_RecursiveDerefZdd(dd, fd);
        return(NULL);
    }
    Cudd_Ref(b1);
    b0 = cuddMakeBddFromZddCover(dd, f0);
    if (!b0) {
        Cudd_RecursiveDerefZdd(dd, f1);
        Cudd_RecursiveDerefZdd(dd, f0);
        Cudd_RecursiveDerefZdd(dd, fd);
        Cudd_RecursiveDeref(dd, b1);
        return(NULL);
    }
    Cudd_Ref(b0);
    Cudd_RecursiveDerefZdd(dd, f1);
    Cudd_RecursiveDerefZdd(dd, f0);
    if (fd != dd->zero) {
        bd = cuddMakeBddFromZddCover(dd, fd);
        if (!bd) {
            Cudd_RecursiveDerefZdd(dd, fd);
            Cudd_RecursiveDeref(dd, b1);
            Cudd_RecursiveDeref(dd, b0);
            return(NULL);
        }
        Cudd_Ref(bd);
        Cudd_RecursiveDerefZdd(dd, fd);
        T = cuddBddAndRecur(dd, Cudd_Not(b1), Cudd_Not(bd));
        if (!T) {
            Cudd_RecursiveDeref(dd, b1);
            Cudd_RecursiveDeref(dd, b0);
            Cudd_RecursiveDeref(dd, bd);
            return(NULL);
        }
        T = Cudd_NotCond(T, T != NULL);
        Cudd_Ref(T);
        Cudd_RecursiveDeref(dd, b1);
        E = cuddBddAndRecur(dd, Cudd_Not(b0), Cudd_Not(bd));
        if (!E) {
            Cudd_RecursiveDeref(dd, b0);
            Cudd_RecursiveDeref(dd, bd);
            Cudd_RecursiveDeref(dd, T);
            return(NULL);
        }
        E = Cudd_NotCond(E, E != NULL);
        Cudd_Ref(E);
        Cudd_RecursiveDeref(dd, b0);
        Cudd_RecursiveDeref(dd, bd);
    }
    else {
        Cudd_RecursiveDerefZdd(dd, fd);
        T = b1;
        E = b0;
    }
    if (Cudd_IsComplement(T)) {
        neW = cuddUniqueInterIVO(dd, v / 2, Cudd_Not(T), Cudd_Not(E));
        if (!neW) {
            Cudd_RecursiveDeref(dd, T);
            Cudd_RecursiveDeref(dd, E);
            return(NULL);
        }
        neW = Cudd_Not(neW);
    }
    else {
        neW = cuddUniqueInterIVO(dd, v / 2, T, E);
        if (!neW) {
            Cudd_RecursiveDeref(dd, T);
            Cudd_RecursiveDeref(dd, E);
            return(NULL);
        }
    }
    Cudd_Ref(neW);
    Cudd_RecursiveDeref(dd, T);
    Cudd_RecursiveDeref(dd, E);
    cuddCacheInsert1(dd, cuddMakeBddFromZddCover, node, neW);
    Cudd_Deref(neW);
    return(neW);
}
DdNode * cuddMakeBddFromZddCover ( DdManager * dd , DdNode * node ) { DdNode * neW ; int v ; DdNode * f1 , * f0 , * fd ; DdNode * b1 , * b0 , * bd ; DdNode * T , * E ; statLine ( dd ) ; if ( node == dd -> one ) return ( dd -> one ) ; if ( node == dd -> zero ) return ( Cudd_Not ( dd -> one ) ) ; neW = cuddCacheLookup1 ( dd , cuddMakeBddFromZddCover , node ) ; if ( neW ) return ( neW ) ; v = Cudd_Regular ( node ) -> index ; if ( cuddZddGetCofactors3 ( dd , node , v , & f1 , & f0 , & fd ) ) return ( NULL ) ; Cudd_Ref ( f1 ) ; Cudd_Ref ( f0 ) ; Cudd_Ref ( fd ) ; b1 = cuddMakeBddFromZddCover ( dd , f1 ) ; if ( ! b1 ) { Cudd_RecursiveDerefZdd ( dd , f1 ) ; Cudd_RecursiveDerefZdd ( dd , f0 ) ; Cudd_RecursiveDerefZdd ( dd , fd ) ; return ( NULL ) ; } Cudd_Ref ( b1 ) ; b0 = cuddMakeBddFromZddCover ( dd , f0 ) ; if ( ! b0 ) { Cudd_RecursiveDerefZdd ( dd , f1 ) ; Cudd_RecursiveDerefZdd ( dd , f0 ) ; Cudd_RecursiveDerefZdd ( dd , fd ) ; Cudd_RecursiveDeref ( dd , b1 ) ; return ( NULL ) ; } Cudd_Ref ( b0 ) ; Cudd_RecursiveDerefZdd ( dd , f1 ) ; Cudd_RecursiveDerefZdd ( dd , f0 ) ; if ( fd != dd -> zero ) { bd = cuddMakeBddFromZddCover ( dd , fd ) ; if ( ! bd ) { Cudd_RecursiveDerefZdd ( dd , fd ) ; Cudd_RecursiveDeref ( dd , b1 ) ; Cudd_RecursiveDeref ( dd , b0 ) ; return ( NULL ) ; } Cudd_Ref ( bd ) ; Cudd_RecursiveDerefZdd ( dd , fd ) ; T = cuddBddAndRecur ( dd , Cudd_Not ( b1 ) , Cudd_Not ( bd ) ) ; if ( ! T ) { Cudd_RecursiveDeref ( dd , b1 ) ; Cudd_RecursiveDeref ( dd , b0 ) ; Cudd_RecursiveDeref ( dd , bd ) ; return ( NULL ) ; } T = Cudd_NotCond ( T , T != NULL ) ; Cudd_Ref ( T ) ; Cudd_RecursiveDeref ( dd , b1 ) ; E = cuddBddAndRecur ( dd , Cudd_Not ( b0 ) , Cudd_Not ( bd ) ) ; if ( ! E ) { Cudd_RecursiveDeref ( dd , b0 ) ; Cudd_RecursiveDeref ( dd , bd ) ; Cudd_RecursiveDeref ( dd , T ) ; return ( NULL ) ; } E = Cudd_NotCond ( E , E != NULL ) ; Cudd_Ref ( E ) ; Cudd_RecursiveDeref ( dd , b0 ) ; Cudd_RecursiveDeref ( dd , bd ) ; } else { Cudd_RecursiveDerefZdd ( dd , fd ) ; T = b1 ; E = b0 ; } if ( Cudd_IsComplement ( T ) ) { neW = cuddUniqueInterIVO ( dd , v / 2 , Cudd_Not ( T ) , Cudd_Not ( E ) ) ; if ( ! neW ) { Cudd_RecursiveDeref ( dd , T ) ; Cudd_RecursiveDeref ( dd , E ) ; return ( NULL ) ; } neW = Cudd_Not ( neW ) ; } else { neW = cuddUniqueInterIVO ( dd , v / 2 , T , E ) ; if ( ! neW ) { Cudd_RecursiveDeref ( dd , T ) ; Cudd_RecursiveDeref ( dd , E ) ; return ( NULL ) ; } } Cudd_Ref ( neW ) ; Cudd_RecursiveDeref ( dd , T ) ; Cudd_RecursiveDeref ( dd , E ) ; cuddCacheInsert1 ( dd , cuddMakeBddFromZddCover , node , neW ) ; Cudd_Deref ( neW ) ; return ( neW ) ; }
Function
Synopsis [Converts a ZDD cover to a BDD graph.]
Function Synopsis [ Converts a ZDD cover to a BDD graph . ]
/* Check cache */ /* either yi or zi */