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

  Synopsis    [Symmetric sifting to convergence algorithm.]

  Description [Symmetric sifting to convergence algorithm.
  Assumes that no dead nodes are present.
    <ol>
    <li> Order all the variables according to the number of entries in
    each unique subtable.
    <li> Sift the variable up and down, remembering each time the total
    size of the DD heap and grouping variables that are symmetric.
    <li> Select the best permutation.
    <li> Repeat 3 and 4 for all variables.
    <li> Repeat 1-4 until no further improvement.
    </ol>
  Returns 1 plus the number of symmetric variables if successful; 0
  otherwise.]

  SideEffects [None]

  SeeAlso     [cuddSymmSifting]

******************************************************************************/
Function
Synopsis    [Symmetric sifting to convergence algorithm.]

Description [Symmetric sifting to convergence algorithm.
Assumes that no dead nodes are present.

 Order all the variables according to the number of entries in
each unique subtable.
 Sift the variable up and down, remembering each time the total
size of the DD heap and grouping variables that are symmetric.
 Select the best permutation.
 Repeat 3 and 4 for all variables.
 Repeat 1-4 until no further improvement.

Returns 1 plus the number of symmetric variables if successful; 0
otherwise.]




Function Synopsis [ Symmetric sifting to convergence algorithm . ] Description [ Symmetric sifting to convergence algorithm . Assumes that no dead nodes are present . Order all the variables according to the number of entries in each unique subtable . Sift the variable up and down remembering each time the total size of the DD heap and grouping variables that are symmetric . Select the best permutation . Repeat 3 and 4 for all variables . Repeat 1 - 4 until no further improvement . Returns 1 plus the number of symmetric variables if successful ; 0 otherwise . ]
int
cuddSymmSiftingConv(
  DdManager * table,
  int  lower,
  int  upper)
{
    int         i;
    int         *var;
    int         size;
    int         x;
    int         result;
    int         symvars;
    int         symgroups;
    int         classes;
    int         initialSize;
#ifdef DD_STATS
    int         previousSize;
#endif
    initialSize = table->keys - table->isolated;
    size = table->size;
    var = NULL;
    entry = ABC_ALLOC(int,size);
    if (entry == NULL) {
        table->errorCode = CUDD_MEMORY_OUT;
        goto ddSymmSiftingConvOutOfMem;
    }
    var = ABC_ALLOC(int,size);
    if (var == NULL) {
        table->errorCode = CUDD_MEMORY_OUT;
        goto ddSymmSiftingConvOutOfMem;
    }
    for (i = 0; i < size; i++) {
        x = table->perm[i];
        entry[i] = table->subtables[x].keys;
        var[i] = i;
    }
    qsort((void *)var,size,sizeof(int),(DD_QSFP)ddSymmUniqueCompare);
    for (i = lower; i <= upper; i++) {
        table->subtables[i].next = i;
    }
    for (i = 0; i < ddMin(table->siftMaxVar, table->size); i++) {
        if (ddTotalNumberSwapping >= table->siftMaxSwap)
            break;
        x = table->perm[var[i]];
        if (x < lower || x > upper) continue;
        if (table->subtables[x].next == (unsigned) x) {
#ifdef DD_STATS
            previousSize = table->keys - table->isolated;
#endif
            result = ddSymmSiftingAux(table,x,lower,upper);
            if (!result) goto ddSymmSiftingConvOutOfMem;
#ifdef DD_STATS
            if (table->keys < (unsigned) previousSize + table->isolated) {
                (void) fprintf(table->out,"-");
            } else if (table->keys > (unsigned) previousSize +
                       table->isolated) {
                (void) fprintf(table->out,"+");
            } else {
                (void) fprintf(table->out,"=");
            }
            fflush(table->out);
#endif
        }
    }
    while ((unsigned) initialSize > table->keys - table->isolated) {
        initialSize = table->keys - table->isolated;
#ifdef DD_STATS
        (void) fprintf(table->out,"\n");
#endif
        for (x = lower, classes = 0; x <= upper; x++, classes++) {
            while ((unsigned) x < table->subtables[x].next) {
                x = table->subtables[x].next;
            }
            i = table->invperm[x];
            entry[i] = table->subtables[x].keys;
            var[classes] = i;
        }
        qsort((void *)var,classes,sizeof(int),(DD_QSFP)ddSymmUniqueCompare);
        for (i = 0; i < ddMin(table->siftMaxVar,classes); i++) {
            if (ddTotalNumberSwapping >= table->siftMaxSwap)
                break;
            x = table->perm[var[i]];
            if ((unsigned) x >= table->subtables[x].next) {
#ifdef DD_STATS
                previousSize = table->keys - table->isolated;
#endif
                result = ddSymmSiftingConvAux(table,x,lower,upper);
                if (!result ) goto ddSymmSiftingConvOutOfMem;
#ifdef DD_STATS
                if (table->keys < (unsigned) previousSize + table->isolated) {
                    (void) fprintf(table->out,"-");
                } else if (table->keys > (unsigned) previousSize +
                           table->isolated) {
                    (void) fprintf(table->out,"+");
                } else {
                    (void) fprintf(table->out,"=");
                }
                fflush(table->out);
#endif
            }
        } 
    }
    ddSymmSummary(table, lower, upper, &symvars, &symgroups);
#ifdef DD_STATS
    (void) fprintf(table->out, "\n#:S_SIFTING %8d: symmetric variables\n",
                   symvars);
    (void) fprintf(table->out, "#:G_SIFTING %8d: symmetric groups",
                   symgroups);
#endif
    ABC_FREE(var);
    ABC_FREE(entry);
    return(1+symvars);
ddSymmSiftingConvOutOfMem:
    if (entry != NULL) ABC_FREE(entry);
    if (var != NULL) ABC_FREE(var);
    return(0);
}
int cuddSymmSiftingConv ( DdManager * table , int lower , int upper ) { int i ; int * var ; int size ; int x ; int result ; int symvars ; int symgroups ; int classes ; int initialSize ; #ifdef DD_STATS int previousSize ; #endif initialSize = table -> keys - table -> isolated ; size = table -> size ; var = NULL ; entry = ABC_ALLOC ( int , size ) ; if ( entry == NULL ) { table -> errorCode = CUDD_MEMORY_OUT ; goto ddSymmSiftingConvOutOfMem ; } var = ABC_ALLOC ( int , size ) ; if ( var == NULL ) { table -> errorCode = CUDD_MEMORY_OUT ; goto ddSymmSiftingConvOutOfMem ; } for ( i = 0 ; i < size ; i ++ ) { x = table -> perm [ i ] ; entry [ i ] = table -> subtables [ x ] . keys ; var [ i ] = i ; } qsort ( ( void * ) var , size , sizeof ( int ) , ( DD_QSFP ) ddSymmUniqueCompare ) ; for ( i = lower ; i <= upper ; i ++ ) { table -> subtables [ i ] . next = i ; } for ( i = 0 ; i < ddMin ( table -> siftMaxVar , table -> size ) ; i ++ ) { if ( ddTotalNumberSwapping >= table -> siftMaxSwap ) break ; x = table -> perm [ var [ i ] ] ; if ( x < lower || x > upper ) continue ; if ( table -> subtables [ x ] . next == ( unsigned ) x ) { #ifdef DD_STATS previousSize = table -> keys - table -> isolated ; #endif result = ddSymmSiftingAux ( table , x , lower , upper ) ; if ( ! result ) goto ddSymmSiftingConvOutOfMem ; #ifdef DD_STATS if ( table -> keys < ( unsigned ) previousSize + table -> isolated ) { ( void ) fprintf ( table -> out , " " ) ; } else if ( table -> keys > ( unsigned ) previousSize + table -> isolated ) { ( void ) fprintf ( table -> out , " " ) ; } else { ( void ) fprintf ( table -> out , " " ) ; } fflush ( table -> out ) ; #endif } } while ( ( unsigned ) initialSize > table -> keys - table -> isolated ) { initialSize = table -> keys - table -> isolated ; #ifdef DD_STATS ( void ) fprintf ( table -> out , " \n " ) ; #endif for ( x = lower , classes = 0 ; x <= upper ; x ++ , classes ++ ) { while ( ( unsigned ) x < table -> subtables [ x ] . next ) { x = table -> subtables [ x ] . next ; } i = table -> invperm [ x ] ; entry [ i ] = table -> subtables [ x ] . keys ; var [ classes ] = i ; } qsort ( ( void * ) var , classes , sizeof ( int ) , ( DD_QSFP ) ddSymmUniqueCompare ) ; for ( i = 0 ; i < ddMin ( table -> siftMaxVar , classes ) ; i ++ ) { if ( ddTotalNumberSwapping >= table -> siftMaxSwap ) break ; x = table -> perm [ var [ i ] ] ; if ( ( unsigned ) x >= table -> subtables [ x ] . next ) { #ifdef DD_STATS previousSize = table -> keys - table -> isolated ; #endif result = ddSymmSiftingConvAux ( table , x , lower , upper ) ; if ( ! result ) goto ddSymmSiftingConvOutOfMem ; #ifdef DD_STATS if ( table -> keys < ( unsigned ) previousSize + table -> isolated ) { ( void ) fprintf ( table -> out , " " ) ; } else if ( table -> keys > ( unsigned ) previousSize + table -> isolated ) { ( void ) fprintf ( table -> out , " " ) ; } else { ( void ) fprintf ( table -> out , " " ) ; } fflush ( table -> out ) ; #endif } } } ddSymmSummary ( table , lower , upper , & symvars , & symgroups ) ; #ifdef DD_STATS ( void ) fprintf ( table -> out , " \n \n " , symvars ) ; ( void ) fprintf ( table -> out , " " , symgroups ) ; #endif ABC_FREE ( var ) ; ABC_FREE ( entry ) ; return ( 1 + symvars ) ; ddSymmSiftingConvOutOfMem : if ( entry != NULL ) ABC_FREE ( entry ) ; if ( var != NULL ) ABC_FREE ( var ) ; return ( 0 ) ; }
Function
Synopsis    [Symmetric sifting to convergence algorithm.]
Function Synopsis [ Symmetric sifting to convergence algorithm . ]
/* Find order in which to sift variables. */ /* Initialize the symmetry of each subtable to itself
    ** for first pass of converging symmetric sifting.
    */ /* Only sift if not in symmetry group already. */ /* Sifting now until convergence. */ /* Here we consider only one representative for each symmetry class. */ /* Here x is the largest index in a group.
            ** Groups consist of adjacent variables.
            ** Hence, the next increment of x will move it to a new group.
            */ /* Now sift. */ /* for */