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

  Synopsis [Implements the recursive step of Cudd_bddClippingAnd.]

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

  SideEffects [None]

  SeeAlso     [cuddBddClippingAnd]

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

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




Function Synopsis [ Implements the recursive step of Cudd_bddClippingAnd . ] Description [ Implements the recursive step of Cudd_bddClippingAnd by taking the conjunction of two BDDs . Returns a pointer to the result is successful ; NULL otherwise . ]
static DdNode *
cuddBddClippingAndRecur(
  DdManager * manager,
  DdNode * f,
  DdNode * g,
  int  distance,
  int  direction)
{
    DdNode *F, *ft, *fe, *G, *gt, *ge;
    DdNode *one, *zero, *r, *t, *e;
    unsigned int topf, topg, index;
    DD_CTFP cacheOp;
    statLine(manager);
    one = DD_ONE(manager);
    zero = Cudd_Not(one);
    if (f == zero || g == zero || f == Cudd_Not(g)) return(zero);
    if (f == g || g == one) return(f);
    if (f == one) return(g);
    if (distance == 0) {
        if (Cudd_bddLeq(manager,f,g)) return(f);
        if (Cudd_bddLeq(manager,g,f)) return(g);
        if (direction == 1) {
            if (Cudd_bddLeq(manager,f,Cudd_Not(g)) ||
                Cudd_bddLeq(manager,g,Cudd_Not(f))) return(zero);
        }
        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);
    cacheOp = (DD_CTFP)
        (direction ? Cudd_bddClippingAnd : cuddBddClippingAnd);
    if (F->ref != 1 || G->ref != 1) {
        r = cuddCacheLookup2(manager, cacheOp, f, g);
        if (r != NULL) return(r);
    }
    topf = manager->perm[F->index];
    topg = manager->perm[G->index];
    if (topf <= topg) {
        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 <= topf) {
        gt = cuddT(G);
        ge = cuddE(G);
        if (Cudd_IsComplement(g)) {
            gt = Cudd_Not(gt);
            ge = Cudd_Not(ge);
        }
    } else {
        gt = ge = g;
    }
    t = cuddBddClippingAndRecur(manager, ft, gt, distance, direction);
    if (t == NULL) return(NULL);
    cuddRef(t);
    e = cuddBddClippingAndRecur(manager, fe, ge, distance, direction);
    if (e == NULL) {
        Cudd_RecursiveDeref(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_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)
        cuddCacheInsert2(manager, cacheOp, f, g, r);
    return(r);
}
static DdNode * cuddBddClippingAndRecur ( DdManager * manager , DdNode * f , DdNode * g , int distance , int direction ) { DdNode * F , * ft , * fe , * G , * gt , * ge ; DdNode * one , * zero , * r , * t , * e ; unsigned int topf , topg , index ; DD_CTFP cacheOp ; statLine ( manager ) ; one = DD_ONE ( manager ) ; zero = Cudd_Not ( one ) ; if ( f == zero || g == zero || f == Cudd_Not ( g ) ) return ( zero ) ; if ( f == g || g == one ) return ( f ) ; if ( f == one ) return ( g ) ; if ( distance == 0 ) { if ( Cudd_bddLeq ( manager , f , g ) ) return ( f ) ; if ( Cudd_bddLeq ( manager , g , f ) ) return ( g ) ; if ( direction == 1 ) { if ( Cudd_bddLeq ( manager , f , Cudd_Not ( g ) ) || Cudd_bddLeq ( manager , g , Cudd_Not ( f ) ) ) return ( zero ) ; } 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 ) ; cacheOp = ( DD_CTFP ) ( direction ? Cudd_bddClippingAnd : cuddBddClippingAnd ) ; if ( F -> ref != 1 || G -> ref != 1 ) { r = cuddCacheLookup2 ( manager , cacheOp , f , g ) ; if ( r != NULL ) return ( r ) ; } topf = manager -> perm [ F -> index ] ; topg = manager -> perm [ G -> index ] ; if ( topf <= topg ) { 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 <= topf ) { gt = cuddT ( G ) ; ge = cuddE ( G ) ; if ( Cudd_IsComplement ( g ) ) { gt = Cudd_Not ( gt ) ; ge = Cudd_Not ( ge ) ; } } else { gt = ge = g ; } t = cuddBddClippingAndRecur ( manager , ft , gt , distance , direction ) ; if ( t == NULL ) return ( NULL ) ; cuddRef ( t ) ; e = cuddBddClippingAndRecur ( manager , fe , ge , distance , direction ) ; if ( e == NULL ) { Cudd_RecursiveDeref ( 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_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 ) cuddCacheInsert2 ( manager , cacheOp , f , g , r ) ; return ( r ) ; }
Function
Synopsis [Implements the recursive step of Cudd_bddClippingAnd.]
Function Synopsis [ Implements the recursive step of Cudd_bddClippingAnd . ]
/* Terminal cases. */ /* One last attempt at returning the right result. We sort of
        ** cheat by calling Cudd_bddLeq. */ /* At this point f and g are not constant. */ /* Check cache. Try to increase cache efficiency by sorting the
    ** pointers. */ /* Here we can skip the use of cuddI, because the operands are known
    ** to be non-constant.
    */ /* Compute cofactors. */