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

  Synopsis    [Performs the reordering-sensitive step of Extra_zddTupleFromBdd().]

  Description [Generates in a bottom-up fashion ZDD for all combinations
               composed of k variables out of variables belonging to Support.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
Function
Synopsis    [Performs the reordering-sensitive step of Extra_zddTupleFromBdd().]

Description [Generates in a bottom-up fashion ZDD for all combinations
composed of k variables out of variables belonging to Support.]




Function Synopsis [ Performs the reordering - sensitive step of Extra_zddTupleFromBdd () . ] Description [ Generates in a bottom - up fashion ZDD for all combinations composed of k variables out of variables belonging to Support . ]
DdNode* extraZddTuplesFromBdd( 
  DdManager * dd,   
  DdNode * bVarsK,   
  DdNode * bVarsN)   
{
    DdNode *zRes, *zRes0, *zRes1;
    statLine(dd); 
    if ( cuddI( dd, bVarsK->index ) < cuddI( dd, bVarsN->index ) )
        return z0;
    if ( bVarsN == b1 )
        return z1;
    zRes = cuddCacheLookup2Zdd(dd, extraZddTuplesFromBdd, bVarsK, bVarsN);
    if (zRes)
        return(zRes);
    zRes0 = extraZddTuplesFromBdd( dd, bVarsK, cuddT(bVarsN) );
    if ( zRes0 == NULL ) 
        return NULL;
    cuddRef( zRes0 );
    if ( bVarsK == b1 )
    {
        zRes1 = z0;
        cuddRef( zRes1 );
    }
    else
    {
        zRes1 = extraZddTuplesFromBdd( dd, cuddT(bVarsK), cuddT(bVarsN) );
        if ( zRes1 == NULL ) 
        {
            Cudd_RecursiveDerefZdd( dd, zRes0 );
            return NULL;
        }
        cuddRef( zRes1 );
    }
    zRes = cuddZddGetNode( dd, 2*bVarsN->index, zRes1, zRes0 );
    if ( zRes == NULL ) 
    {
        Cudd_RecursiveDerefZdd( dd, zRes0 );
        Cudd_RecursiveDerefZdd( dd, zRes1 );
        return NULL;
    }
    cuddDeref( zRes0 );
    cuddDeref( zRes1 );
    cuddCacheInsert2(dd, extraZddTuplesFromBdd, bVarsK, bVarsN, zRes);
    return zRes;
}
DdNode * extraZddTuplesFromBdd ( DdManager * dd , DdNode * bVarsK , DdNode * bVarsN ) { DdNode * zRes , * zRes0 , * zRes1 ; statLine ( dd ) ; if ( cuddI ( dd , bVarsK -> index ) < cuddI ( dd , bVarsN -> index ) ) return z0 ; if ( bVarsN == b1 ) return z1 ; zRes = cuddCacheLookup2Zdd ( dd , extraZddTuplesFromBdd , bVarsK , bVarsN ) ; if ( zRes ) return ( zRes ) ; zRes0 = extraZddTuplesFromBdd ( dd , bVarsK , cuddT ( bVarsN ) ) ; if ( zRes0 == NULL ) return NULL ; cuddRef ( zRes0 ) ; if ( bVarsK == b1 ) { zRes1 = z0 ; cuddRef ( zRes1 ) ; } else { zRes1 = extraZddTuplesFromBdd ( dd , cuddT ( bVarsK ) , cuddT ( bVarsN ) ) ; if ( zRes1 == NULL ) { Cudd_RecursiveDerefZdd ( dd , zRes0 ) ; return NULL ; } cuddRef ( zRes1 ) ; } zRes = cuddZddGetNode ( dd , 2 * bVarsN -> index , zRes1 , zRes0 ) ; if ( zRes == NULL ) { Cudd_RecursiveDerefZdd ( dd , zRes0 ) ; Cudd_RecursiveDerefZdd ( dd , zRes1 ) ; return NULL ; } cuddDeref ( zRes0 ) ; cuddDeref ( zRes1 ) ; cuddCacheInsert2 ( dd , extraZddTuplesFromBdd , bVarsK , bVarsN , zRes ) ; return zRes ; }
Function
Synopsis    [Performs the reordering-sensitive step of Extra_zddTupleFromBdd().]
Function Synopsis [ Performs the reordering - sensitive step of Extra_zddTupleFromBdd () . ]
/* the DD manager */ /* the number of variables in tuples */ /* the set of all variables */ /* terminal cases */ /*  if ( k < 0 || k > n )
 *      return dd->zero;
 *  if ( n == 0 )
 *      return dd->one; 
 */ /* check cache */ /* ZDD in which this variable is 0 */ /*  zRes0 = extraZddTuplesFromBdd( dd, k,     n-1 ); */ /* ZDD in which this variable is 1 */ /*  zRes1 = extraZddTuplesFromBdd( dd, k-1,          n-1 ); */ /* compose Res0 and Res1 with the given ZDD variable */ /* insert the result into cache */