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

  Synopsis    [Builds ZDD representing the set of fixed-size variable tuples.]

  Description [Creates ZDD of all combinations of variables in Support that
  is represented by a BDD.]

  SideEffects [New ZDD variables are created if indices of the variables
               present in the combination are larger than the currently
               allocated number of ZDD variables.]

  SeeAlso     []

******************************************************************************/
Function
Synopsis    [Builds ZDD representing the set of fixed-size variable tuples.]

Description [Creates ZDD of all combinations of variables in Support that
is represented by a BDD.]

SideEffects [New ZDD variables are created if indices of the variables
present in the combination are larger than the currently
allocated number of ZDD variables.]


Function Synopsis [ Builds ZDD representing the set of fixed - size variable tuples . ] Description [ Creates ZDD of all combinations of variables in Support that is represented by a BDD . ] SideEffects [ New ZDD variables are created if indices of the variables present in the combination are larger than the currently allocated number of ZDD variables . ]
DdNode* Extra_zddTuplesFromBdd( 
  DdManager * dd,   
  int K,            
  DdNode * bVarsN)   
{
    DdNode  *zRes;
    int     autoDynZ;
    autoDynZ = dd->autoDynZ;
    dd->autoDynZ = 0;
    do {
        DdNode *bVarSet = bVarsN, *bVarsK = bVarsN;
        int     nVars = 0, i;
        while ( bVarSet != b1 )
        {
            nVars++;
            if ( cuddE( bVarSet ) != b0 )
                return NULL;
            bVarSet = cuddT( bVarSet );
        }
        if ( K > nVars )
            return NULL;
        for ( i = 0; i < nVars-K; i++ )
            bVarsK = cuddT( bVarsK );
        dd->reordered = 0;
        zRes = extraZddTuplesFromBdd(dd, bVarsK, bVarsN );
    } while (dd->reordered == 1);
    dd->autoDynZ = autoDynZ;
    return zRes;
}
DdNode * Extra_zddTuplesFromBdd ( DdManager * dd , int K , DdNode * bVarsN ) { DdNode * zRes ; int autoDynZ ; autoDynZ = dd -> autoDynZ ; dd -> autoDynZ = 0 ; do { DdNode * bVarSet = bVarsN , * bVarsK = bVarsN ; int nVars = 0 , i ; while ( bVarSet != b1 ) { nVars ++ ; if ( cuddE ( bVarSet ) != b0 ) return NULL ; bVarSet = cuddT ( bVarSet ) ; } if ( K > nVars ) return NULL ; for ( i = 0 ; i < nVars - K ; i ++ ) bVarsK = cuddT ( bVarsK ) ; dd -> reordered = 0 ; zRes = extraZddTuplesFromBdd ( dd , bVarsK , bVarsN ) ; } while ( dd -> reordered == 1 ) ; dd -> autoDynZ = autoDynZ ; return zRes ; }
Function
Synopsis    [Builds ZDD representing the set of fixed-size variable tuples.]
Function Synopsis [ Builds ZDD representing the set of fixed - size variable tuples . ]
/* the DD manager */ /* the number of variables in tuples */ /* the set of all variables represented as a BDD */ /* transform the numeric arguments (K) into a DdNode* argument;
         * this allows us to use the standard internal CUDD cache */ /* determine the number of variables in VarSet */ /* make sure that the VarSet is a cube */ /* make sure that the number of variables in VarSet is less or equal 
           that the number of variables that should be present in the tuples
        */ /* the second argument in the recursive call stannds for <n>;
         * reate the first argument, which stands for <k>
         * as when we are talking about the tuple of <k> out of <n> */