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

  Synopsis    [Implements the recursive step of Cudd_bddIte.]

  Description [Implements the recursive step of Cudd_bddIte. Returns a
  pointer to the resulting BDD. NULL if the intermediate result blows
  up or if reordering occurs.]

  SideEffects [None]

  SeeAlso     []

******************************************************************************/
Function
Synopsis    [Implements the recursive step of Cudd_bddIte.]

Description [Implements the recursive step of Cudd_bddIte. Returns a
pointer to the resulting BDD. NULL if the intermediate result blows
up or if reordering occurs.]




Function Synopsis [ Implements the recursive step of Cudd_bddIte . ] Description [ Implements the recursive step of Cudd_bddIte . Returns a pointer to the resulting BDD . NULL if the intermediate result blows up or if reordering occurs . ]
DdNode *
cuddBddIteRecur(
  DdManager * dd,
  DdNode * f,
  DdNode * g,
  DdNode * h)
{
    DdNode       *one, *zero, *res;
    DdNode       *r, *Fv, *Fnv, *Gv, *Gnv, *H, *Hv, *Hnv, *t, *e;
    unsigned int topf, topg, toph, v;
    int          index = -1;
    int          comple;
    statLine(dd);
    if (f == (one = DD_ONE(dd)))        
        return(g);
    if (f == (zero = Cudd_Not(one)))    
        return(h);
    if (g == one || f == g) {   
        if (h == zero) {        
            return(f);
        } else {
            res = cuddBddAndRecur(dd,Cudd_Not(f),Cudd_Not(h));
            return(Cudd_NotCond(res,res != NULL));
        }
    } else if (g == zero || f == Cudd_Not(g)) { 
        if (h == one) {         
            return(Cudd_Not(f));
        } else {
            res = cuddBddAndRecur(dd,Cudd_Not(f),h);
            return(res);
        }
    }
    if (h == zero || f == h) {    
        res = cuddBddAndRecur(dd,f,g);
        return(res);
    } else if (h == one || f == Cudd_Not(h)) { 
        res = cuddBddAndRecur(dd,f,Cudd_Not(g));
        return(Cudd_NotCond(res,res != NULL));
    }
    if (g == h) {               
        return(g);
    } else if (g == Cudd_Not(h)) { 
        res = cuddBddXorRecur(dd,f,h);
        return(res);
    }
    comple = bddVarToCanonicalSimple(dd, &f, &g, &h, &topf, &topg, &toph);
    v = ddMin(topg, toph);
    if (topf < v && cuddT(f) == one && cuddE(f) == zero) {
        r = cuddUniqueInter(dd, (int) f->index, g, h);
        return(Cudd_NotCond(r,comple && r != NULL));
    }
    r = cuddCacheLookup(dd, DD_BDD_ITE_TAG, f, g, h);
    if (r != NULL) {
        return(Cudd_NotCond(r,comple));
    }
    if (topf <= v) {
        v = ddMin(topf, v);     
        index = f->index;
        Fv = cuddT(f); Fnv = cuddE(f);
    } else {
        Fv = Fnv = f;
    }
    if (topg == v) {
        index = g->index;
        Gv = cuddT(g); Gnv = cuddE(g);
    } else {
        Gv = Gnv = g;
    }
    if (toph == v) {
        H = Cudd_Regular(h);
        index = H->index;
        Hv = cuddT(H); Hnv = cuddE(H);
        if (Cudd_IsComplement(h)) {
            Hv = Cudd_Not(Hv);
            Hnv = Cudd_Not(Hnv);
        }
    } else {
        Hv = Hnv = h;
    }
    t = cuddBddIteRecur(dd,Fv,Gv,Hv);
    if (t == NULL) return(NULL);
    cuddRef(t);
    e = cuddBddIteRecur(dd,Fnv,Gnv,Hnv);
    if (e == NULL) {
        Cudd_IterDerefBdd(dd,t);
        return(NULL);
    }
    cuddRef(e);
    r = (t == e) ? t : cuddUniqueInter(dd,index,t,e);
    if (r == NULL) {
        Cudd_IterDerefBdd(dd,t);
        Cudd_IterDerefBdd(dd,e);
        return(NULL);
    }
    cuddDeref(t);
    cuddDeref(e);
    cuddCacheInsert(dd, DD_BDD_ITE_TAG, f, g, h, r);
    return(Cudd_NotCond(r,comple));
}
DdNode * cuddBddIteRecur ( DdManager * dd , DdNode * f , DdNode * g , DdNode * h ) { DdNode * one , * zero , * res ; DdNode * r , * Fv , * Fnv , * Gv , * Gnv , * H , * Hv , * Hnv , * t , * e ; unsigned int topf , topg , toph , v ; int index = -1 ; int comple ; statLine ( dd ) ; if ( f == ( one = DD_ONE ( dd ) ) ) return ( g ) ; if ( f == ( zero = Cudd_Not ( one ) ) ) return ( h ) ; if ( g == one || f == g ) { if ( h == zero ) { return ( f ) ; } else { res = cuddBddAndRecur ( dd , Cudd_Not ( f ) , Cudd_Not ( h ) ) ; return ( Cudd_NotCond ( res , res != NULL ) ) ; } } else if ( g == zero || f == Cudd_Not ( g ) ) { if ( h == one ) { return ( Cudd_Not ( f ) ) ; } else { res = cuddBddAndRecur ( dd , Cudd_Not ( f ) , h ) ; return ( res ) ; } } if ( h == zero || f == h ) { res = cuddBddAndRecur ( dd , f , g ) ; return ( res ) ; } else if ( h == one || f == Cudd_Not ( h ) ) { res = cuddBddAndRecur ( dd , f , Cudd_Not ( g ) ) ; return ( Cudd_NotCond ( res , res != NULL ) ) ; } if ( g == h ) { return ( g ) ; } else if ( g == Cudd_Not ( h ) ) { res = cuddBddXorRecur ( dd , f , h ) ; return ( res ) ; } comple = bddVarToCanonicalSimple ( dd , & f , & g , & h , & topf , & topg , & toph ) ; v = ddMin ( topg , toph ) ; if ( topf < v && cuddT ( f ) == one && cuddE ( f ) == zero ) { r = cuddUniqueInter ( dd , ( int ) f -> index , g , h ) ; return ( Cudd_NotCond ( r , comple && r != NULL ) ) ; } r = cuddCacheLookup ( dd , DD_BDD_ITE_TAG , f , g , h ) ; if ( r != NULL ) { return ( Cudd_NotCond ( r , comple ) ) ; } if ( topf <= v ) { v = ddMin ( topf , v ) ; index = f -> index ; Fv = cuddT ( f ) ; Fnv = cuddE ( f ) ; } else { Fv = Fnv = f ; } if ( topg == v ) { index = g -> index ; Gv = cuddT ( g ) ; Gnv = cuddE ( g ) ; } else { Gv = Gnv = g ; } if ( toph == v ) { H = Cudd_Regular ( h ) ; index = H -> index ; Hv = cuddT ( H ) ; Hnv = cuddE ( H ) ; if ( Cudd_IsComplement ( h ) ) { Hv = Cudd_Not ( Hv ) ; Hnv = Cudd_Not ( Hnv ) ; } } else { Hv = Hnv = h ; } t = cuddBddIteRecur ( dd , Fv , Gv , Hv ) ; if ( t == NULL ) return ( NULL ) ; cuddRef ( t ) ; e = cuddBddIteRecur ( dd , Fnv , Gnv , Hnv ) ; if ( e == NULL ) { Cudd_IterDerefBdd ( dd , t ) ; return ( NULL ) ; } cuddRef ( e ) ; r = ( t == e ) ? t : cuddUniqueInter ( dd , index , t , e ) ; if ( r == NULL ) { Cudd_IterDerefBdd ( dd , t ) ; Cudd_IterDerefBdd ( dd , e ) ; return ( NULL ) ; } cuddDeref ( t ) ; cuddDeref ( e ) ; cuddCacheInsert ( dd , DD_BDD_ITE_TAG , f , g , h , r ) ; return ( Cudd_NotCond ( r , comple ) ) ; }
Function
Synopsis    [Implements the recursive step of Cudd_bddIte.]
Function Synopsis [ Implements the recursive step of Cudd_bddIte . ]
/* Terminal cases. */ /* One variable cases. */ /* ITE(1,G,H) = G */ /* ITE(0,G,H) = H */ /* From now on, f is known not to be a constant. */ /* ITE(F,F,H) = ITE(F,1,H) = F + H */ /* ITE(F,1,0) = F */ /* ITE(F,!F,H) = ITE(F,0,H) = !F * H */ /* ITE(F,0,1) = !F */ /* ITE(F,G,F) = ITE(F,G,0) = F * G */ /* ITE(F,G,!F) = ITE(F,G,1) = !F + G */ /* Check remaining one variable case. */ /* ITE(F,G,G) = G */ /* ITE(F,G,!G) = F <-> G */ /* From here, there are no constants. */ /* f & g are now regular pointers */ /* A shortcut: ITE(F,G,H) = (v,G,H) if F = (v,1,0), v < top(G,H). */ /* Check cache. */ /* Compute cofactors. */ /* v = top_var(F,G,H) */ /* Recursive step. */