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

  Synopsis [Takes the exclusive OR of two BDDs and simultaneously abstracts the
  variables in cube.]

  Description [Takes the exclusive OR of two BDDs and simultaneously abstracts
  the variables in cube. The variables are existentially abstracted.  Returns a
  pointer to the result is successful; NULL otherwise.]

  SideEffects [None]

  SeeAlso     [Cudd_bddAndAbstract]

******************************************************************************/
Function
Synopsis [Takes the exclusive OR of two BDDs and simultaneously abstracts the
variables in cube.]

Description [Takes the exclusive OR of two BDDs and simultaneously abstracts
the variables in cube. The variables are existentially abstracted.  Returns a
pointer to the result is successful; NULL otherwise.]




Function Synopsis [ Takes the exclusive OR of two BDDs and simultaneously abstracts the variables in cube . ] Description [ Takes the exclusive OR of two BDDs and simultaneously abstracts the variables in cube . The variables are existentially abstracted . Returns a pointer to the result is successful ; NULL otherwise . ]
DdNode *
cuddBddXorExistAbstractRecur(
  DdManager * manager,
  DdNode * f,
  DdNode * g,
  DdNode * cube)
{
    DdNode *F, *fv, *fnv, *G, *gv, *gnv;
    DdNode *one, *zero, *r, *t, *e, *Cube;
    unsigned int topf, topg, topcube, top, index;
    statLine(manager);
    one = DD_ONE(manager);
    zero = Cudd_Not(one);
    if (f == g) {
        return(zero);
    }
    if (f == Cudd_Not(g)) {
        return(one);
    }
    if (cube == one) {
        return(cuddBddXorRecur(manager, f, g));
    }
    if (f == one) {
        return(cuddBddExistAbstractRecur(manager, Cudd_Not(g), cube));
    }
    if (g == one) {
        return(cuddBddExistAbstractRecur(manager, Cudd_Not(f), cube));
    }
    if (f == zero) {
        return(cuddBddExistAbstractRecur(manager, g, cube));
    }
    if (g == zero) {
        return(cuddBddExistAbstractRecur(manager, f, cube));
    }
    if (cuddF2L(f) > cuddF2L(g)) { 
        DdNode *tmp = f;
        f = g;
        g = tmp;
    }
    r = cuddCacheLookup(manager, DD_BDD_XOR_EXIST_ABSTRACT_TAG, f, g, cube);
    if (r != NULL) {
        return(r);
    }
    F = Cudd_Regular(f);
    topf = manager->perm[F->index];
    G = Cudd_Regular(g);
    topg = manager->perm[G->index];
    top = ddMin(topf, topg);
    topcube = manager->perm[cube->index];
    if (topcube < top) {
        return(cuddBddXorExistAbstractRecur(manager, f, g, cuddT(cube)));
    }
    if (topf == top) {
        index = F->index;
        fv = cuddT(F);
        fnv = cuddE(F);
        if (Cudd_IsComplement(f)) {
            fv = Cudd_Not(fv);
            fnv = Cudd_Not(fnv);
        }
    } else {
        index = G->index;
        fv = fnv = f;
    }
    if (topg == top) {
        gv = cuddT(G);
        gnv = cuddE(G);
        if (Cudd_IsComplement(g)) {
            gv = Cudd_Not(gv);
            gnv = Cudd_Not(gnv);
        }
    } else {
        gv = gnv = g;
    }
    if (topcube == top) {
        Cube = cuddT(cube);
    } else {
        Cube = cube;
    }
    t = cuddBddXorExistAbstractRecur(manager, fv, gv, Cube);
    if (t == NULL) return(NULL);
    if (t == one && topcube == top) {
        cuddCacheInsert(manager, DD_BDD_XOR_EXIST_ABSTRACT_TAG, f, g, cube, one);
        return(one);
    }
    cuddRef(t);
    e = cuddBddXorExistAbstractRecur(manager, fnv, gnv, Cube);
    if (e == NULL) {
        Cudd_IterDerefBdd(manager, t);
        return(NULL);
    }
    cuddRef(e);
    if (topcube == top) {       
        r = cuddBddAndRecur(manager, Cudd_Not(t), Cudd_Not(e));
        if (r == NULL) {
            Cudd_IterDerefBdd(manager, t);
            Cudd_IterDerefBdd(manager, e);
            return(NULL);
        }
        r = Cudd_Not(r);
        cuddRef(r);
        Cudd_IterDerefBdd(manager, t);
        Cudd_IterDerefBdd(manager, e);
        cuddDeref(r);
    } else if (t == e) {
        r = t;
        cuddDeref(t);
        cuddDeref(e);
    } 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);
    }
    cuddCacheInsert(manager, DD_BDD_XOR_EXIST_ABSTRACT_TAG, f, g, cube, r);
    return (r);
}
DdNode * cuddBddXorExistAbstractRecur ( DdManager * manager , DdNode * f , DdNode * g , DdNode * cube ) { DdNode * F , * fv , * fnv , * G , * gv , * gnv ; DdNode * one , * zero , * r , * t , * e , * Cube ; unsigned int topf , topg , topcube , top , index ; statLine ( manager ) ; one = DD_ONE ( manager ) ; zero = Cudd_Not ( one ) ; if ( f == g ) { return ( zero ) ; } if ( f == Cudd_Not ( g ) ) { return ( one ) ; } if ( cube == one ) { return ( cuddBddXorRecur ( manager , f , g ) ) ; } if ( f == one ) { return ( cuddBddExistAbstractRecur ( manager , Cudd_Not ( g ) , cube ) ) ; } if ( g == one ) { return ( cuddBddExistAbstractRecur ( manager , Cudd_Not ( f ) , cube ) ) ; } if ( f == zero ) { return ( cuddBddExistAbstractRecur ( manager , g , cube ) ) ; } if ( g == zero ) { return ( cuddBddExistAbstractRecur ( manager , f , cube ) ) ; } if ( cuddF2L ( f ) > cuddF2L ( g ) ) { DdNode * tmp = f ; f = g ; g = tmp ; } r = cuddCacheLookup ( manager , DD_BDD_XOR_EXIST_ABSTRACT_TAG , f , g , cube ) ; if ( r != NULL ) { return ( r ) ; } F = Cudd_Regular ( f ) ; topf = manager -> perm [ F -> index ] ; G = Cudd_Regular ( g ) ; topg = manager -> perm [ G -> index ] ; top = ddMin ( topf , topg ) ; topcube = manager -> perm [ cube -> index ] ; if ( topcube < top ) { return ( cuddBddXorExistAbstractRecur ( manager , f , g , cuddT ( cube ) ) ) ; } if ( topf == top ) { index = F -> index ; fv = cuddT ( F ) ; fnv = cuddE ( F ) ; if ( Cudd_IsComplement ( f ) ) { fv = Cudd_Not ( fv ) ; fnv = Cudd_Not ( fnv ) ; } } else { index = G -> index ; fv = fnv = f ; } if ( topg == top ) { gv = cuddT ( G ) ; gnv = cuddE ( G ) ; if ( Cudd_IsComplement ( g ) ) { gv = Cudd_Not ( gv ) ; gnv = Cudd_Not ( gnv ) ; } } else { gv = gnv = g ; } if ( topcube == top ) { Cube = cuddT ( cube ) ; } else { Cube = cube ; } t = cuddBddXorExistAbstractRecur ( manager , fv , gv , Cube ) ; if ( t == NULL ) return ( NULL ) ; if ( t == one && topcube == top ) { cuddCacheInsert ( manager , DD_BDD_XOR_EXIST_ABSTRACT_TAG , f , g , cube , one ) ; return ( one ) ; } cuddRef ( t ) ; e = cuddBddXorExistAbstractRecur ( manager , fnv , gnv , Cube ) ; if ( e == NULL ) { Cudd_IterDerefBdd ( manager , t ) ; return ( NULL ) ; } cuddRef ( e ) ; if ( topcube == top ) { r = cuddBddAndRecur ( manager , Cudd_Not ( t ) , Cudd_Not ( e ) ) ; if ( r == NULL ) { Cudd_IterDerefBdd ( manager , t ) ; Cudd_IterDerefBdd ( manager , e ) ; return ( NULL ) ; } r = Cudd_Not ( r ) ; cuddRef ( r ) ; Cudd_IterDerefBdd ( manager , t ) ; Cudd_IterDerefBdd ( manager , e ) ; cuddDeref ( r ) ; } else if ( t == e ) { r = t ; cuddDeref ( t ) ; cuddDeref ( e ) ; } 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 ) ; } cuddCacheInsert ( manager , DD_BDD_XOR_EXIST_ABSTRACT_TAG , f , g , cube , r ) ; return ( r ) ; }
Function
Synopsis [Takes the exclusive OR of two BDDs and simultaneously abstracts the
variables in cube.]
Function Synopsis [ Takes the exclusive OR of two BDDs and simultaneously abstracts the variables in cube . ]
/* Terminal cases. */ /* At this point f, g, and cube are not constant. */ /* Try to increase cache efficiency. */ /* Check cache. */ /* Here we can skip the use of cuddI, because the operands are known
    ** to be non-constant.
    */ /* Now, topcube >= top. */ /* Special case: 1 OR anything = 1. Hence, no need to compute
    ** the else branch if t is 1.
    */ /* abstract */