abc/src/bdd/extrab/extraBddSymm.c
/**Function********************************************************************

  Synopsis    [Performs a recursive step of Extra_bddReduceVarSet.]

  Description [Returns the set of all variables in the given set that are not in the 
  support of the given function.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
Function
Synopsis    [Performs a recursive step of Extra_bddReduceVarSet.]

Description [Returns the set of all variables in the given set that are not in the
support of the given function.]




Function Synopsis [ Performs a recursive step of Extra_bddReduceVarSet . ] Description [ Returns the set of all variables in the given set that are not in the support of the given function . ]
DdNode * extraBddReduceVarSet( 
  DdManager * dd,    
  DdNode * bVars,    
  DdNode * bF)       
{
    DdNode * bRes;
    DdNode * bFR = Cudd_Regular(bF);
    if ( cuddIsConstant(bFR) || bVars == b1 )
        return bVars;
    if ( (bRes = cuddCacheLookup2(dd, extraBddReduceVarSet, bVars, bF)) )
        return bRes;
    else
    {
        DdNode * bF0, * bF1;             
        DdNode * bVarsThis, * bVarsLower, * bTemp;
        int LevelF;
        LevelF = dd->perm[bFR->index];
        for ( bVarsThis = bVars; LevelF > cuddI(dd,bVarsThis->index); bVarsThis = cuddT(bVarsThis) );
        if ( LevelF == cuddI(dd,bVarsThis->index) )
            bVarsLower = cuddT(bVarsThis);
        else
            bVarsLower = bVarsThis;
        if ( bFR != bF ) 
        {
            bF0 = Cudd_Not( cuddE(bFR) );
            bF1 = Cudd_Not( cuddT(bFR) );
        }
        else
        {
            bF0 = cuddE(bFR);
            bF1 = cuddT(bFR);
        }
        bRes = extraBddReduceVarSet( dd, bVarsLower, bF0 );
        if ( bRes == NULL ) 
            return NULL;
        cuddRef( bRes );
        bRes = extraBddReduceVarSet( dd, bTemp = bRes, bF1 );
        if ( bRes == NULL ) 
        {
            Cudd_RecursiveDeref( dd, bTemp );
            return NULL;
        }
        cuddRef( bRes );
        Cudd_RecursiveDeref( dd, bTemp );
        if ( bVarsThis != bVars )
        {
            DdNode * bVarsExtra;
            bVarsExtra = cuddBddExistAbstractRecur( dd, bVars, bVarsThis );
            if ( bVarsExtra == NULL )
            {
                Cudd_RecursiveDeref( dd, bRes );
                return NULL;
            }
            cuddRef( bVarsExtra );
            bRes = cuddBddAndRecur( dd, bTemp = bRes, bVarsExtra );
            if ( bRes == NULL ) 
            {
                Cudd_RecursiveDeref( dd, bTemp );
                Cudd_RecursiveDeref( dd, bVarsExtra );
                return NULL;
            }
            cuddRef( bRes );
            Cudd_RecursiveDeref( dd, bTemp );
            Cudd_RecursiveDeref( dd, bVarsExtra );
        }
        cuddDeref( bRes );
        cuddCacheInsert2( dd, extraBddReduceVarSet, bVars, bF, bRes );
        return bRes;
    }
}
DdNode * extraBddReduceVarSet ( DdManager * dd , DdNode * bVars , DdNode * bF ) { DdNode * bRes ; DdNode * bFR = Cudd_Regular ( bF ) ; if ( cuddIsConstant ( bFR ) || bVars == b1 ) return bVars ; if ( ( bRes = cuddCacheLookup2 ( dd , extraBddReduceVarSet , bVars , bF ) ) ) return bRes ; else { DdNode * bF0 , * bF1 ; DdNode * bVarsThis , * bVarsLower , * bTemp ; int LevelF ; LevelF = dd -> perm [ bFR -> index ] ; for ( bVarsThis = bVars ; LevelF > cuddI ( dd , bVarsThis -> index ) ; bVarsThis = cuddT ( bVarsThis ) ) ; if ( LevelF == cuddI ( dd , bVarsThis -> index ) ) bVarsLower = cuddT ( bVarsThis ) ; else bVarsLower = bVarsThis ; if ( bFR != bF ) { bF0 = Cudd_Not ( cuddE ( bFR ) ) ; bF1 = Cudd_Not ( cuddT ( bFR ) ) ; } else { bF0 = cuddE ( bFR ) ; bF1 = cuddT ( bFR ) ; } bRes = extraBddReduceVarSet ( dd , bVarsLower , bF0 ) ; if ( bRes == NULL ) return NULL ; cuddRef ( bRes ) ; bRes = extraBddReduceVarSet ( dd , bTemp = bRes , bF1 ) ; if ( bRes == NULL ) { Cudd_RecursiveDeref ( dd , bTemp ) ; return NULL ; } cuddRef ( bRes ) ; Cudd_RecursiveDeref ( dd , bTemp ) ; if ( bVarsThis != bVars ) { DdNode * bVarsExtra ; bVarsExtra = cuddBddExistAbstractRecur ( dd , bVars , bVarsThis ) ; if ( bVarsExtra == NULL ) { Cudd_RecursiveDeref ( dd , bRes ) ; return NULL ; } cuddRef ( bVarsExtra ) ; bRes = cuddBddAndRecur ( dd , bTemp = bRes , bVarsExtra ) ; if ( bRes == NULL ) { Cudd_RecursiveDeref ( dd , bTemp ) ; Cudd_RecursiveDeref ( dd , bVarsExtra ) ; return NULL ; } cuddRef ( bRes ) ; Cudd_RecursiveDeref ( dd , bTemp ) ; Cudd_RecursiveDeref ( dd , bVarsExtra ) ; } cuddDeref ( bRes ) ; cuddCacheInsert2 ( dd , extraBddReduceVarSet , bVars , bF , bRes ) ; return bRes ; } }
Function
Synopsis    [Performs a recursive step of Extra_bddReduceVarSet.]
Function Synopsis [ Performs a recursive step of Extra_bddReduceVarSet . ]
/* the DD manager */ /* the set of variables to be reduced */ /* the function whose support is used for reduction */ // if LevelF is below LevelV, scroll through the vars in bVars  // scroll also through the current var, because it should be not be added // cofactor the function // bFunc is complemented  // solve subproblems // the current var should not be added // add the skipped vars // extract the skipped variables // add these variables