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

  Synopsis    [Reorders BDD variables according to the order of the ZDD
  variables.]

  Description [Reorders BDD variables according to the order of the
  ZDD variables. This function can be called at the end of ZDD
  reordering to insure that the order of the BDD variables is
  consistent with the order of the ZDD variables. The number of ZDD
  variables must be a multiple of the number of BDD variables. Let
  <code>M</code> be the ratio of the two numbers. cuddBddAlignToZdd
  then considers the ZDD variables from <code>M*i</code> to
  <code>(M+1)*i-1</code> as corresponding to BDD variable
  <code>i</code>.  This function should be normally called from
  Cudd_zddReduceHeap, which clears the cache.  Returns 1 in case of
  success; 0 otherwise.]

  SideEffects [Changes the BDD variable order for all diagrams and performs
  garbage collection of the BDD unique table.]

  SeeAlso [Cudd_ShuffleHeap Cudd_zddReduceHeap]

******************************************************************************/
Function
Synopsis    [Reorders BDD variables according to the order of the ZDD
variables.]

Description [Reorders BDD variables according to the order of the
ZDD variables. This function can be called at the end of ZDD
reordering to insure that the order of the BDD variables is
consistent with the order of the ZDD variables. The number of ZDD
variables must be a multiple of the number of BDD variables. Let
M be the ratio of the two numbers. cuddBddAlignToZdd
then considers the ZDD variables from M*i to
(M+1)*i-1 as corresponding to BDD variable
i.  This function should be normally called from
Cudd_zddReduceHeap, which clears the cache.  Returns 1 in case of
success; 0 otherwise.]

SideEffects [Changes the BDD variable order for all diagrams and performs
garbage collection of the BDD unique table.]


Function Synopsis [ Reorders BDD variables according to the order of the ZDD variables . ] Description [ Reorders BDD variables according to the order of the ZDD variables . This function can be called at the end of ZDD reordering to insure that the order of the BDD variables is consistent with the order of the ZDD variables . The number of ZDD variables must be a multiple of the number of BDD variables . Let M be the ratio of the two numbers . cuddBddAlignToZdd then considers the ZDD variables from M * i to ( M + 1 ) * i - 1 as corresponding to BDD variable i . This function should be normally called from Cudd_zddReduceHeap which clears the cache . Returns 1 in case of success ; 0 otherwise . ] SideEffects [ Changes the BDD variable order for all diagrams and performs garbage collection of the BDD unique table . ]
int
cuddBddAlignToZdd(
  DdManager * table )
{
    int *invperm;               
    int M;                      
    int i;                      
    int result;                 
    if (table->size == 0)
        return(1);
    M = table->sizeZ / table->size;
    if (M * table->size != table->sizeZ)
        return(0);
    invperm = ABC_ALLOC(int,table->size);
    if (invperm == NULL) {
        table->errorCode = CUDD_MEMORY_OUT;
        return(0);
    }
    for (i = 0; i < table->sizeZ; i += M) {
        int indexZ = table->invpermZ[i];
        int index  = indexZ / M;
        invperm[i / M] = index;
    }
    cuddGarbageCollect(table,0);
    table->isolated = 0;
    for (i = 0; i < table->size; i++) {
        if (table->vars[i]->ref == 1) table->isolated++;
    }
    result = cuddInitInteract(table);
    if (result == 0) return(0);
    result = ddShuffle(table, invperm);
    ABC_FREE(invperm);
    ABC_FREE(table->interact);
    bddFixTree(table,table->tree);
    return(result);
}
int cuddBddAlignToZdd ( DdManager * table ) { int * invperm ; int M ; int i ; int result ; if ( table -> size == 0 ) return ( 1 ) ; M = table -> sizeZ / table -> size ; if ( M * table -> size != table -> sizeZ ) return ( 0 ) ; invperm = ABC_ALLOC ( int , table -> size ) ; if ( invperm == NULL ) { table -> errorCode = CUDD_MEMORY_OUT ; return ( 0 ) ; } for ( i = 0 ; i < table -> sizeZ ; i += M ) { int indexZ = table -> invpermZ [ i ] ; int index = indexZ / M ; invperm [ i / M ] = index ; } cuddGarbageCollect ( table , 0 ) ; table -> isolated = 0 ; for ( i = 0 ; i < table -> size ; i ++ ) { if ( table -> vars [ i ] -> ref == 1 ) table -> isolated ++ ; } result = cuddInitInteract ( table ) ; if ( result == 0 ) return ( 0 ) ; result = ddShuffle ( table , invperm ) ; ABC_FREE ( invperm ) ; ABC_FREE ( table -> interact ) ; bddFixTree ( table , table -> tree ) ; return ( result ) ; }
Function
Synopsis    [Reorders BDD variables according to the order of the ZDD
variables.]
Function Synopsis [ Reorders BDD variables according to the order of the ZDD variables . ]
/* DD manager */ /* permutation array */ /* ratio of ZDD variables to BDD variables */ /* loop index */ /* return value */ /* We assume that a ratio of 0 is OK. */ /* Check whether the number of ZDD variables is a multiple of the
    ** number of BDD variables.
    */ /* Create and initialize the inverse permutation array. */ /* Eliminate dead nodes. Do not scan the cache again, because we
    ** assume that Cudd_zddReduceHeap has already cleared it.
    */ /* Initialize number of isolated projection functions. */ /* Initialize the interaction matrix. */ /* Free interaction matrix. */ /* Fix the BDD variable group tree. */