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

  Synopsis [Implements the recursive step of Cudd_bddXor.]

  Description [Implements the recursive step of Cudd_bddXor by taking
  the exclusive OR of two BDDs.  Returns a pointer to the result is
  successful; NULL otherwise.]

  SideEffects [None]

  SeeAlso     [Cudd_bddXor]

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

Description [Implements the recursive step of Cudd_bddXor by taking
the exclusive OR of two BDDs.  Returns a pointer to the result is
successful; NULL otherwise.]




Function Synopsis [ Implements the recursive step of Cudd_bddXor . ] Description [ Implements the recursive step of Cudd_bddXor by taking the exclusive OR of two BDDs . Returns a pointer to the result is successful ; NULL otherwise . ]
DdNode *
cuddBddXorRecur(
  DdManager * manager,
  DdNode * f,
  DdNode * g)
{
    DdNode *fv, *fnv, *G, *gv, *gnv;
    DdNode *one, *zero, *r, *t, *e;
    unsigned int topf, topg, index;
    statLine(manager);
    one = DD_ONE(manager);
    zero = Cudd_Not(one);
    if (f == g) return(zero);
    if (f == Cudd_Not(g)) return(one);
    if (cuddF2L(f) > cuddF2L(g)) { 
        DdNode *tmp = f;
        f = g;
        g = tmp;
    }
    if (g == zero) return(f);
    if (g == one) return(Cudd_Not(f));
    if (Cudd_IsComplement(f)) {
        f = Cudd_Not(f);
        g = Cudd_Not(g);
    }
    if (f == one) return(Cudd_Not(g));
    r = cuddCacheLookup2(manager, Cudd_bddXor, f, g);
    if (r != NULL) return(r);
    topf = manager->perm[f->index];
    G = Cudd_Regular(g);
    topg = manager->perm[G->index];
    if (topf <= topg) {
        index = f->index;
        fv = cuddT(f);
        fnv = cuddE(f);
    } else {
        index = G->index;
        fv = fnv = f;
    }
    if (topg <= topf) {
        gv = cuddT(G);
        gnv = cuddE(G);
        if (Cudd_IsComplement(g)) {
            gv = Cudd_Not(gv);
            gnv = Cudd_Not(gnv);
        }
    } else {
        gv = gnv = g;
    }
    t = cuddBddXorRecur(manager, fv, gv);
    if (t == NULL) return(NULL);
    cuddRef(t);
    e = cuddBddXorRecur(manager, fnv, gnv);
    if (e == NULL) {
        Cudd_IterDerefBdd(manager, t);
        return(NULL);
    }
    cuddRef(e);
    if (t == e) {
        r = t;
    } else {
        if (Cudd_IsComplement(t)) {
            r = cuddUniqueInter(manager,(int)index,Cudd_Not(t),Cudd_Not(e));
            if (r == NULL) {
                Cudd_IterDerefBdd(manager, t);
                Cudd_IterDerefBdd(manager, e);
                return(NULL);
            }
            r = Cudd_Not(r);
        } else {
            r = cuddUniqueInter(manager,(int)index,t,e);
            if (r == NULL) {
                Cudd_IterDerefBdd(manager, t);
                Cudd_IterDerefBdd(manager, e);
                return(NULL);
            }
        }
    }
    cuddDeref(e);
    cuddDeref(t);
    cuddCacheInsert2(manager, Cudd_bddXor, f, g, r);
    return(r);
}
DdNode * cuddBddXorRecur ( DdManager * manager , DdNode * f , DdNode * g ) { DdNode * fv , * fnv , * G , * gv , * gnv ; DdNode * one , * zero , * r , * t , * e ; unsigned int topf , topg , index ; statLine ( manager ) ; one = DD_ONE ( manager ) ; zero = Cudd_Not ( one ) ; if ( f == g ) return ( zero ) ; if ( f == Cudd_Not ( g ) ) return ( one ) ; if ( cuddF2L ( f ) > cuddF2L ( g ) ) { DdNode * tmp = f ; f = g ; g = tmp ; } if ( g == zero ) return ( f ) ; if ( g == one ) return ( Cudd_Not ( f ) ) ; if ( Cudd_IsComplement ( f ) ) { f = Cudd_Not ( f ) ; g = Cudd_Not ( g ) ; } if ( f == one ) return ( Cudd_Not ( g ) ) ; r = cuddCacheLookup2 ( manager , Cudd_bddXor , f , g ) ; if ( r != NULL ) return ( r ) ; topf = manager -> perm [ f -> index ] ; G = Cudd_Regular ( g ) ; topg = manager -> perm [ G -> index ] ; if ( topf <= topg ) { index = f -> index ; fv = cuddT ( f ) ; fnv = cuddE ( f ) ; } else { index = G -> index ; fv = fnv = f ; } if ( topg <= topf ) { gv = cuddT ( G ) ; gnv = cuddE ( G ) ; if ( Cudd_IsComplement ( g ) ) { gv = Cudd_Not ( gv ) ; gnv = Cudd_Not ( gnv ) ; } } else { gv = gnv = g ; } t = cuddBddXorRecur ( manager , fv , gv ) ; if ( t == NULL ) return ( NULL ) ; cuddRef ( t ) ; e = cuddBddXorRecur ( manager , fnv , gnv ) ; if ( e == NULL ) { Cudd_IterDerefBdd ( manager , t ) ; return ( NULL ) ; } cuddRef ( e ) ; if ( t == e ) { r = t ; } else { if ( Cudd_IsComplement ( t ) ) { r = cuddUniqueInter ( manager , ( int ) index , Cudd_Not ( t ) , Cudd_Not ( e ) ) ; if ( r == NULL ) { Cudd_IterDerefBdd ( manager , t ) ; Cudd_IterDerefBdd ( manager , e ) ; return ( NULL ) ; } r = Cudd_Not ( r ) ; } else { r = cuddUniqueInter ( manager , ( int ) index , t , e ) ; if ( r == NULL ) { Cudd_IterDerefBdd ( manager , t ) ; Cudd_IterDerefBdd ( manager , e ) ; return ( NULL ) ; } } } cuddDeref ( e ) ; cuddDeref ( t ) ; cuddCacheInsert2 ( manager , Cudd_bddXor , f , g , r ) ; return ( r ) ; }
Function
Synopsis [Implements the recursive step of Cudd_bddXor.]
Function Synopsis [ Implements the recursive step of Cudd_bddXor . ]
/* Terminal cases. */ /* Try to increase cache efficiency and simplify tests. */ /* Now the first argument is regular. */ /* At this point f and g are not constant. */ /* Check cache. */ /* Here we can skip the use of cuddI, because the operands are known
    ** to be non-constant.
    */ /* Compute cofactors. */