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

  Synopsis    [Performs the recursive steps of Cudd_bddExistAbstract.]

  Description [Performs the recursive steps of Cudd_bddExistAbstract.
  Returns the BDD obtained by abstracting the variables
  of cube from f if successful; NULL otherwise. It is also used by
  Cudd_bddUnivAbstract.]

  SideEffects [None]

  SeeAlso     [Cudd_bddExistAbstract Cudd_bddUnivAbstract]

******************************************************************************/
Function
Synopsis    [Performs the recursive steps of Cudd_bddExistAbstract.]

Description [Performs the recursive steps of Cudd_bddExistAbstract.
Returns the BDD obtained by abstracting the variables
of cube from f if successful; NULL otherwise. It is also used by
Cudd_bddUnivAbstract.]




Function Synopsis [ Performs the recursive steps of Cudd_bddExistAbstract . ] Description [ Performs the recursive steps of Cudd_bddExistAbstract . Returns the BDD obtained by abstracting the variables of cube from f if successful ; NULL otherwise . It is also used by Cudd_bddUnivAbstract . ]
DdNode *
cuddBddExistAbstractRecur(
  DdManager * manager,
  DdNode * f,
  DdNode * cube)
{
    DdNode      *F, *T, *E, *res, *res1, *res2, *one;
    statLine(manager);
    one = DD_ONE(manager);
    F = Cudd_Regular(f);
    if (cube == one || F == one) {  
        return(f);
    }
    while (manager->perm[F->index] > manager->perm[cube->index]) {
        cube = cuddT(cube);
        if (cube == one) return(f);
    }
    if (F->ref != 1 && (res = cuddCacheLookup2(manager, Cudd_bddExistAbstract, f, cube)) != NULL) {
        return(res);
    }
    T = cuddT(F); E = cuddE(F);
    if (f != F) {
        T = Cudd_Not(T); E = Cudd_Not(E);
    }
    if (F->index == cube->index) {
        if (T == one || E == one || T == Cudd_Not(E)) {
            return(one);
        }
        res1 = cuddBddExistAbstractRecur(manager, T, cuddT(cube));
        if (res1 == NULL) return(NULL);
        if (res1 == one) {
            if (F->ref != 1)
                cuddCacheInsert2(manager, Cudd_bddExistAbstract, f, cube, one);
            return(one);
        }
        cuddRef(res1);
        res2 = cuddBddExistAbstractRecur(manager, E, cuddT(cube));
        if (res2 == NULL) {
            Cudd_IterDerefBdd(manager,res1);
            return(NULL);
        }
        cuddRef(res2);
        res = cuddBddAndRecur(manager, Cudd_Not(res1), Cudd_Not(res2));
        if (res == NULL) {
            Cudd_IterDerefBdd(manager, res1);
            Cudd_IterDerefBdd(manager, res2);
            return(NULL);
        }
        res = Cudd_Not(res);
        cuddRef(res);
        Cudd_IterDerefBdd(manager, res1);
        Cudd_IterDerefBdd(manager, res2);
        if (F->ref != 1)
            cuddCacheInsert2(manager, Cudd_bddExistAbstract, f, cube, res);
        cuddDeref(res);
        return(res);
    } else { 
        res1 = cuddBddExistAbstractRecur(manager, T, cube);
        if (res1 == NULL) return(NULL);
        cuddRef(res1);
        res2 = cuddBddExistAbstractRecur(manager, E, cube);
        if (res2 == NULL) {
            Cudd_IterDerefBdd(manager, res1);
            return(NULL);
        }
        cuddRef(res2);
        res = cuddBddIteRecur(manager, manager->vars[F->index], res1, res2);
        if (res == NULL) {
            Cudd_IterDerefBdd(manager, res1);
            Cudd_IterDerefBdd(manager, res2);
            return(NULL);
        }
        cuddRef(res); 
        Cudd_IterDerefBdd(manager, res1); 
        Cudd_IterDerefBdd(manager, res2); 
        cuddDeref(res); 
        if (F->ref != 1)
            cuddCacheInsert2(manager, Cudd_bddExistAbstract, f, cube, res);
        return(res);
    }       
}
DdNode * cuddBddExistAbstractRecur ( DdManager * manager , DdNode * f , DdNode * cube ) { DdNode * F , * T , * E , * res , * res1 , * res2 , * one ; statLine ( manager ) ; one = DD_ONE ( manager ) ; F = Cudd_Regular ( f ) ; if ( cube == one || F == one ) { return ( f ) ; } while ( manager -> perm [ F -> index ] > manager -> perm [ cube -> index ] ) { cube = cuddT ( cube ) ; if ( cube == one ) return ( f ) ; } if ( F -> ref != 1 && ( res = cuddCacheLookup2 ( manager , Cudd_bddExistAbstract , f , cube ) ) != NULL ) { return ( res ) ; } T = cuddT ( F ) ; E = cuddE ( F ) ; if ( f != F ) { T = Cudd_Not ( T ) ; E = Cudd_Not ( E ) ; } if ( F -> index == cube -> index ) { if ( T == one || E == one || T == Cudd_Not ( E ) ) { return ( one ) ; } res1 = cuddBddExistAbstractRecur ( manager , T , cuddT ( cube ) ) ; if ( res1 == NULL ) return ( NULL ) ; if ( res1 == one ) { if ( F -> ref != 1 ) cuddCacheInsert2 ( manager , Cudd_bddExistAbstract , f , cube , one ) ; return ( one ) ; } cuddRef ( res1 ) ; res2 = cuddBddExistAbstractRecur ( manager , E , cuddT ( cube ) ) ; if ( res2 == NULL ) { Cudd_IterDerefBdd ( manager , res1 ) ; return ( NULL ) ; } cuddRef ( res2 ) ; res = cuddBddAndRecur ( manager , Cudd_Not ( res1 ) , Cudd_Not ( res2 ) ) ; if ( res == NULL ) { Cudd_IterDerefBdd ( manager , res1 ) ; Cudd_IterDerefBdd ( manager , res2 ) ; return ( NULL ) ; } res = Cudd_Not ( res ) ; cuddRef ( res ) ; Cudd_IterDerefBdd ( manager , res1 ) ; Cudd_IterDerefBdd ( manager , res2 ) ; if ( F -> ref != 1 ) cuddCacheInsert2 ( manager , Cudd_bddExistAbstract , f , cube , res ) ; cuddDeref ( res ) ; return ( res ) ; } else { res1 = cuddBddExistAbstractRecur ( manager , T , cube ) ; if ( res1 == NULL ) return ( NULL ) ; cuddRef ( res1 ) ; res2 = cuddBddExistAbstractRecur ( manager , E , cube ) ; if ( res2 == NULL ) { Cudd_IterDerefBdd ( manager , res1 ) ; return ( NULL ) ; } cuddRef ( res2 ) ; res = cuddBddIteRecur ( manager , manager -> vars [ F -> index ] , res1 , res2 ) ; if ( res == NULL ) { Cudd_IterDerefBdd ( manager , res1 ) ; Cudd_IterDerefBdd ( manager , res2 ) ; return ( NULL ) ; } cuddRef ( res ) ; Cudd_IterDerefBdd ( manager , res1 ) ; Cudd_IterDerefBdd ( manager , res2 ) ; cuddDeref ( res ) ; if ( F -> ref != 1 ) cuddCacheInsert2 ( manager , Cudd_bddExistAbstract , f , cube , res ) ; return ( res ) ; } }
Function
Synopsis    [Performs the recursive steps of Cudd_bddExistAbstract.]
Function Synopsis [ Performs the recursive steps of Cudd_bddExistAbstract . ]
/* Cube is guaranteed to be a cube at this point. */ /* From now on, f and cube are non-constant. */ /* Abstract a variable that does not appear in f. */ /* Check the cache. */ /* Compute the cofactors of f. */ /* If the two indices are the same, so are their levels. */ /* if (cuddI(manager,F->index) < cuddI(manager,cube->index)) */ /* ITE takes care of possible complementation of res1 and of the
        ** case in which res1 == res2. */ //Added //cuddDeref(res1); //cuddDeref(res2); //Added