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

  Synopsis    [Implementation of the linear sifting algorithm for ZDDs.]

  Description [Implementation of the linear sifting algorithm for ZDDs.
  Assumes that no dead nodes are present.
    <ol>
    <li> Order all the variables according to the number of entries
    in each unique table.
    <li> Sift the variable up and down and applies the XOR transformation,
    remembering each time the total size of the DD heap.
    <li> Select the best permutation.
    <li> Repeat 3 and 4 for all variables.
    </ol>
  Returns 1 if successful; 0 otherwise.]

  SideEffects [None]

  SeeAlso     []

******************************************************************************/
Function
Synopsis    [Implementation of the linear sifting algorithm for ZDDs.]

Description [Implementation of the linear sifting algorithm for ZDDs.
Assumes that no dead nodes are present.

 Order all the variables according to the number of entries
in each unique table.
 Sift the variable up and down and applies the XOR transformation,
remembering each time the total size of the DD heap.
 Select the best permutation.
 Repeat 3 and 4 for all variables.

Returns 1 if successful; 0 otherwise.]




Function Synopsis [ Implementation of the linear sifting algorithm for ZDDs . ] Description [ Implementation of the linear sifting algorithm for ZDDs . Assumes that no dead nodes are present . Order all the variables according to the number of entries in each unique table . Sift the variable up and down and applies the XOR transformation remembering each time the total size of the DD heap . Select the best permutation . Repeat 3 and 4 for all variables . Returns 1 if successful ; 0 otherwise . ]
int
cuddZddLinearSifting(
  DdManager * table,
  int  lower,
  int  upper)
{
    int i;
    int *var;
    int size;
    int x;
    int result;
#ifdef DD_STATS
    int previousSize;
#endif
    size = table->sizeZ;
    empty = table->zero;
    var = NULL;
    zdd_entry = ABC_ALLOC(int, size);
    if (zdd_entry == NULL) {
        table->errorCode = CUDD_MEMORY_OUT;
        goto cuddZddSiftingOutOfMem;
    }
    var = ABC_ALLOC(int, size);
    if (var == NULL) {
        table->errorCode = CUDD_MEMORY_OUT;
        goto cuddZddSiftingOutOfMem;
    }
    for (i = 0; i < size; i++) {
        x = table->permZ[i];
        zdd_entry[i] = table->subtableZ[x].keys;
        var[i] = i;
    }
    qsort((void *)var, size, sizeof(int), (DD_QSFP)cuddZddUniqueCompare);
    for (i = 0; i < ddMin(table->siftMaxVar, size); i++) {
        if (zddTotalNumberSwapping >= table->siftMaxSwap)
            break;
        x = table->permZ[var[i]];
        if (x < lower || x > upper) continue;
#ifdef DD_STATS
        previousSize = table->keysZ;
#endif
        result = cuddZddLinearAux(table, x, lower, upper);
        if (!result)
            goto cuddZddSiftingOutOfMem;
#ifdef DD_STATS
        if (table->keysZ < (unsigned) previousSize) {
            (void) fprintf(table->out,"-");
        } else if (table->keysZ > (unsigned) previousSize) {
            (void) fprintf(table->out,"+");     
            (void) fprintf(table->out,"\nSize increased from %d to %d while sifting variable %d\n", previousSize, table->keysZ , var[i]);
        } else {
            (void) fprintf(table->out,"=");
        }
        fflush(table->out);
#endif
    }
    ABC_FREE(var);
    ABC_FREE(zdd_entry);
    return(1);
cuddZddSiftingOutOfMem:
    if (zdd_entry != NULL) ABC_FREE(zdd_entry);
    if (var != NULL) ABC_FREE(var);
    return(0);
}
int cuddZddLinearSifting ( DdManager * table , int lower , int upper ) { int i ; int * var ; int size ; int x ; int result ; #ifdef DD_STATS int previousSize ; #endif size = table -> sizeZ ; empty = table -> zero ; var = NULL ; zdd_entry = ABC_ALLOC ( int , size ) ; if ( zdd_entry == NULL ) { table -> errorCode = CUDD_MEMORY_OUT ; goto cuddZddSiftingOutOfMem ; } var = ABC_ALLOC ( int , size ) ; if ( var == NULL ) { table -> errorCode = CUDD_MEMORY_OUT ; goto cuddZddSiftingOutOfMem ; } for ( i = 0 ; i < size ; i ++ ) { x = table -> permZ [ i ] ; zdd_entry [ i ] = table -> subtableZ [ x ] . keys ; var [ i ] = i ; } qsort ( ( void * ) var , size , sizeof ( int ) , ( DD_QSFP ) cuddZddUniqueCompare ) ; for ( i = 0 ; i < ddMin ( table -> siftMaxVar , size ) ; i ++ ) { if ( zddTotalNumberSwapping >= table -> siftMaxSwap ) break ; x = table -> permZ [ var [ i ] ] ; if ( x < lower || x > upper ) continue ; #ifdef DD_STATS previousSize = table -> keysZ ; #endif result = cuddZddLinearAux ( table , x , lower , upper ) ; if ( ! result ) goto cuddZddSiftingOutOfMem ; #ifdef DD_STATS if ( table -> keysZ < ( unsigned ) previousSize ) { ( void ) fprintf ( table -> out , " " ) ; } else if ( table -> keysZ > ( unsigned ) previousSize ) { ( void ) fprintf ( table -> out , " " ) ; ( void ) fprintf ( table -> out , " \n \n " , previousSize , table -> keysZ , var [ i ] ) ; } else { ( void ) fprintf ( table -> out , " " ) ; } fflush ( table -> out ) ; #endif } ABC_FREE ( var ) ; ABC_FREE ( zdd_entry ) ; return ( 1 ) ; cuddZddSiftingOutOfMem : if ( zdd_entry != NULL ) ABC_FREE ( zdd_entry ) ; if ( var != NULL ) ABC_FREE ( var ) ; return ( 0 ) ; }
Function
Synopsis    [Implementation of the linear sifting algorithm for ZDDs.]
Function Synopsis [ Implementation of the linear sifting algorithm for ZDDs . ]
/* Find order in which to sift variables. */ /* Now sift. */ /* should never happen */