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

  Synopsis [Implements the recursive step of Cudd_bddAnd.]

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

  SideEffects [None]

  SeeAlso     [Cudd_bddAnd]

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

Description [Implements the recursive step of Cudd_bddAnd 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_bddAnd . ] Description [ Implements the recursive step of Cudd_bddAnd by taking the conjunction of two BDDs . Returns a pointer to the result is successful ; NULL otherwise . ]
DdNode *
cuddBddAndRecur(
  DdManager * manager,
  DdNode * f,
  DdNode * g)
{
    DdNode *F, *fv, *fnv, *G, *gv, *gnv;
    DdNode *one, *r, *t, *e;
    unsigned int topf, topg, index;
    statLine(manager);
    one = DD_ONE(manager);
    F = Cudd_Regular(f);
    G = Cudd_Regular(g);
    if (F == G) {
        if (f == g) return(f);
        else return(Cudd_Not(one));
    }
    if (F == one) {
        if (f == one) return(g);
        else return(f);
    }
    if (G == one) {
        if (g == one) return(f);
        else return(g);
    }
    if (cuddF2L(f) > cuddF2L(g)) { 
        DdNode *tmp = f;
        f = g;
        g = tmp;
        F = Cudd_Regular(f);
        G = Cudd_Regular(g);
    }
    if (F->ref != 1 || G->ref != 1) {
        r = cuddCacheLookup2(manager, Cudd_bddAnd, f, g);
        if (r != NULL) return(r);
    }
    if ( manager->TimeStop && Abc_Clock() > manager->TimeStop )
        return NULL;
    topf = manager->perm[F->index];
    topg = manager->perm[G->index];
    if (topf <= topg) {
        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 <= topf) {
        gv = cuddT(G);
        gnv = cuddE(G);
        if (Cudd_IsComplement(g)) {
            gv = Cudd_Not(gv);
            gnv = Cudd_Not(gnv);
        }
    } else {
        gv = gnv = g;
    }
    t = cuddBddAndRecur(manager, fv, gv);
    if (t == NULL) return(NULL);
    cuddRef(t);
    e = cuddBddAndRecur(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);
    if (F->ref != 1 || G->ref != 1)
        cuddCacheInsert2(manager, Cudd_bddAnd, f, g, r);
    return(r);
}
DdNode * cuddBddAndRecur ( DdManager * manager , DdNode * f , DdNode * g ) { DdNode * F , * fv , * fnv , * G , * gv , * gnv ; DdNode * one , * r , * t , * e ; unsigned int topf , topg , index ; statLine ( manager ) ; one = DD_ONE ( manager ) ; F = Cudd_Regular ( f ) ; G = Cudd_Regular ( g ) ; if ( F == G ) { if ( f == g ) return ( f ) ; else return ( Cudd_Not ( one ) ) ; } if ( F == one ) { if ( f == one ) return ( g ) ; else return ( f ) ; } if ( G == one ) { if ( g == one ) return ( f ) ; else return ( g ) ; } if ( cuddF2L ( f ) > cuddF2L ( g ) ) { DdNode * tmp = f ; f = g ; g = tmp ; F = Cudd_Regular ( f ) ; G = Cudd_Regular ( g ) ; } if ( F -> ref != 1 || G -> ref != 1 ) { r = cuddCacheLookup2 ( manager , Cudd_bddAnd , f , g ) ; if ( r != NULL ) return ( r ) ; } if ( manager -> TimeStop && Abc_Clock ( ) > manager -> TimeStop ) return NULL ; topf = manager -> perm [ F -> index ] ; topg = manager -> perm [ G -> index ] ; if ( topf <= topg ) { 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 <= topf ) { gv = cuddT ( G ) ; gnv = cuddE ( G ) ; if ( Cudd_IsComplement ( g ) ) { gv = Cudd_Not ( gv ) ; gnv = Cudd_Not ( gnv ) ; } } else { gv = gnv = g ; } t = cuddBddAndRecur ( manager , fv , gv ) ; if ( t == NULL ) return ( NULL ) ; cuddRef ( t ) ; e = cuddBddAndRecur ( 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 ) ; if ( F -> ref != 1 || G -> ref != 1 ) cuddCacheInsert2 ( manager , Cudd_bddAnd , f , g , r ) ; return ( r ) ; }
Function
Synopsis [Implements the recursive step of Cudd_bddAnd.]
Function Synopsis [ Implements the recursive step of Cudd_bddAnd . ]
/* Terminal cases. */ /* At this point f and g 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.
    */ /* Compute cofactors. */