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

  Synopsis [Approximates the AND of two BDDs and simultaneously abstracts the
  variables in cube.]

  Description [Approximates the AND 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_bddClippingAndAbstract]

******************************************************************************/
Function
Synopsis [Approximates the AND of two BDDs and simultaneously abstracts the
variables in cube.]

Description [Approximates the AND 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 [ Approximates the AND of two BDDs and simultaneously abstracts the variables in cube . ] Description [ Approximates the AND 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 . ]
static DdNode *
cuddBddClipAndAbsRecur(
  DdManager * manager,
  DdNode * f,
  DdNode * g,
  DdNode * cube,
  int  distance,
  int  direction)
{
    DdNode *F, *ft, *fe, *G, *gt, *ge;
    DdNode *one, *zero, *r, *t, *e, *Cube;
    unsigned int topf, topg, topcube, top, index;
    ptruint cacheTag;
    statLine(manager);
    one = DD_ONE(manager);
    zero = Cudd_Not(one);
    if (f == zero || g == zero || f == Cudd_Not(g)) return(zero);
    if (f == one && g == one)   return(one);
    if (cube == one) {
        return(cuddBddClippingAndRecur(manager, f, g, distance, direction));
    }
    if (f == one || f == g) {
        return (cuddBddExistAbstractRecur(manager, g, cube));
    }
    if (g == one) {
        return (cuddBddExistAbstractRecur(manager, f, cube));
    }
    if (distance == 0) return(Cudd_NotCond(one,(direction == 0)));
    distance--;
    if (f > g) { 
        DdNode *tmp = f;
        f = g; g = tmp;
    }
    F = Cudd_Regular(f);
    G = Cudd_Regular(g);
    cacheTag = direction ? DD_BDD_CLIPPING_AND_ABSTRACT_UP_TAG :
        DD_BDD_CLIPPING_AND_ABSTRACT_DOWN_TAG;
    if (F->ref != 1 || G->ref != 1) {
        r = cuddCacheLookup(manager, cacheTag,
                            f, g, cube);
        if (r != NULL) {
            return(r);
        }
    }
    topf = manager->perm[F->index];
    topg = manager->perm[G->index];
    top = ddMin(topf, topg);
    topcube = manager->perm[cube->index];
    if (topcube < top) {
        return(cuddBddClipAndAbsRecur(manager, f, g, cuddT(cube),
                                      distance, direction));
    }
    if (topf == top) {
        index = F->index;
        ft = cuddT(F);
        fe = cuddE(F);
        if (Cudd_IsComplement(f)) {
            ft = Cudd_Not(ft);
            fe = Cudd_Not(fe);
        }
    } else {
        index = G->index;
        ft = fe = f;
    }
    if (topg == top) {
        gt = cuddT(G);
        ge = cuddE(G);
        if (Cudd_IsComplement(g)) {
            gt = Cudd_Not(gt);
            ge = Cudd_Not(ge);
        }
    } else {
        gt = ge = g;
    }
    if (topcube == top) {
        Cube = cuddT(cube);
    } else {
        Cube = cube;
    }
    t = cuddBddClipAndAbsRecur(manager, ft, gt, Cube, distance, direction);
    if (t == NULL) return(NULL);
    if (t == one && topcube == top) {
        if (F->ref != 1 || G->ref != 1)
            cuddCacheInsert(manager, cacheTag, f, g, cube, one);
        return(one);
    }
    cuddRef(t);
    e = cuddBddClipAndAbsRecur(manager, fe, ge, Cube, distance, direction);
    if (e == NULL) {
        Cudd_RecursiveDeref(manager, t);
        return(NULL);
    }
    cuddRef(e);
    if (topcube == top) {       
        r = cuddBddClippingAndRecur(manager, Cudd_Not(t), Cudd_Not(e),
                                    distance, (direction == 0));
        if (r == NULL) {
            Cudd_RecursiveDeref(manager, t);
            Cudd_RecursiveDeref(manager, e);
            return(NULL);
        }
        r = Cudd_Not(r);
        cuddRef(r);
        Cudd_RecursiveDeref(manager, t);
        Cudd_RecursiveDeref(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_RecursiveDeref(manager, t);
                Cudd_RecursiveDeref(manager, e);
                return(NULL);
            }
            r = Cudd_Not(r);
        } else {
            r = cuddUniqueInter(manager,(int)index,t,e);
            if (r == NULL) {
                Cudd_RecursiveDeref(manager, t);
                Cudd_RecursiveDeref(manager, e);
                return(NULL);
            }
        }
        cuddDeref(e);
        cuddDeref(t);
    }
    if (F->ref != 1 || G->ref != 1)
        cuddCacheInsert(manager, cacheTag, f, g, cube, r);
    return (r);
}
static DdNode * cuddBddClipAndAbsRecur ( DdManager * manager , DdNode * f , DdNode * g , DdNode * cube , int distance , int direction ) { DdNode * F , * ft , * fe , * G , * gt , * ge ; DdNode * one , * zero , * r , * t , * e , * Cube ; unsigned int topf , topg , topcube , top , index ; ptruint cacheTag ; statLine ( manager ) ; one = DD_ONE ( manager ) ; zero = Cudd_Not ( one ) ; if ( f == zero || g == zero || f == Cudd_Not ( g ) ) return ( zero ) ; if ( f == one && g == one ) return ( one ) ; if ( cube == one ) { return ( cuddBddClippingAndRecur ( manager , f , g , distance , direction ) ) ; } if ( f == one || f == g ) { return ( cuddBddExistAbstractRecur ( manager , g , cube ) ) ; } if ( g == one ) { return ( cuddBddExistAbstractRecur ( manager , f , cube ) ) ; } if ( distance == 0 ) return ( Cudd_NotCond ( one , ( direction == 0 ) ) ) ; distance -- ; if ( f > g ) { DdNode * tmp = f ; f = g ; g = tmp ; } F = Cudd_Regular ( f ) ; G = Cudd_Regular ( g ) ; cacheTag = direction ? DD_BDD_CLIPPING_AND_ABSTRACT_UP_TAG : DD_BDD_CLIPPING_AND_ABSTRACT_DOWN_TAG ; if ( F -> ref != 1 || G -> ref != 1 ) { r = cuddCacheLookup ( manager , cacheTag , f , g , cube ) ; if ( r != NULL ) { return ( r ) ; } } topf = manager -> perm [ F -> index ] ; topg = manager -> perm [ G -> index ] ; top = ddMin ( topf , topg ) ; topcube = manager -> perm [ cube -> index ] ; if ( topcube < top ) { return ( cuddBddClipAndAbsRecur ( manager , f , g , cuddT ( cube ) , distance , direction ) ) ; } if ( topf == top ) { index = F -> index ; ft = cuddT ( F ) ; fe = cuddE ( F ) ; if ( Cudd_IsComplement ( f ) ) { ft = Cudd_Not ( ft ) ; fe = Cudd_Not ( fe ) ; } } else { index = G -> index ; ft = fe = f ; } if ( topg == top ) { gt = cuddT ( G ) ; ge = cuddE ( G ) ; if ( Cudd_IsComplement ( g ) ) { gt = Cudd_Not ( gt ) ; ge = Cudd_Not ( ge ) ; } } else { gt = ge = g ; } if ( topcube == top ) { Cube = cuddT ( cube ) ; } else { Cube = cube ; } t = cuddBddClipAndAbsRecur ( manager , ft , gt , Cube , distance , direction ) ; if ( t == NULL ) return ( NULL ) ; if ( t == one && topcube == top ) { if ( F -> ref != 1 || G -> ref != 1 ) cuddCacheInsert ( manager , cacheTag , f , g , cube , one ) ; return ( one ) ; } cuddRef ( t ) ; e = cuddBddClipAndAbsRecur ( manager , fe , ge , Cube , distance , direction ) ; if ( e == NULL ) { Cudd_RecursiveDeref ( manager , t ) ; return ( NULL ) ; } cuddRef ( e ) ; if ( topcube == top ) { r = cuddBddClippingAndRecur ( manager , Cudd_Not ( t ) , Cudd_Not ( e ) , distance , ( direction == 0 ) ) ; if ( r == NULL ) { Cudd_RecursiveDeref ( manager , t ) ; Cudd_RecursiveDeref ( manager , e ) ; return ( NULL ) ; } r = Cudd_Not ( r ) ; cuddRef ( r ) ; Cudd_RecursiveDeref ( manager , t ) ; Cudd_RecursiveDeref ( 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_RecursiveDeref ( manager , t ) ; Cudd_RecursiveDeref ( manager , e ) ; return ( NULL ) ; } r = Cudd_Not ( r ) ; } else { r = cuddUniqueInter ( manager , ( int ) index , t , e ) ; if ( r == NULL ) { Cudd_RecursiveDeref ( manager , t ) ; Cudd_RecursiveDeref ( manager , e ) ; return ( NULL ) ; } } cuddDeref ( e ) ; cuddDeref ( t ) ; } if ( F -> ref != 1 || G -> ref != 1 ) cuddCacheInsert ( manager , cacheTag , f , g , cube , r ) ; return ( r ) ; }
Function
Synopsis [Approximates the AND of two BDDs and simultaneously abstracts the
variables in cube.]
Function Synopsis [ Approximates the AND of two BDDs and simultaneously abstracts the variables in cube . ]
/* Terminal cases. */ /* At this point f, g, and cube are not constant. */ /* Check cache. */ /* Try to increase cache efficiency. */ /* 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 */