abc/src/bdd/reo/reoTest.c
/**Function*************************************************************

  Synopsis    [Reorders the DD using CUDD package.]

  Description [Transfers the DD into a temporary manager in such a way
  that the level correspondence is preserved. Reorders the manager
  and transfers the DD back into the original manager using the topmost
  levels of the manager, in such a way that the ordering of levels is
  preserved. The resulting permutation is returned in the array
  given by the user.]

  SideEffects []

  SeeAlso     []

***********************************************************************/
Function
Synopsis    [Reorders the DD using CUDD package.]

Description [Transfers the DD into a temporary manager in such a way
that the level correspondence is preserved. Reorders the manager
and transfers the DD back into the original manager using the topmost
levels of the manager, in such a way that the ordering of levels is
preserved. The resulting permutation is returned in the array
given by the user.]




Function Synopsis [ Reorders the DD using CUDD package . ] Description [ Transfers the DD into a temporary manager in such a way that the level correspondence is preserved . Reorders the manager and transfers the DD back into the original manager using the topmost levels of the manager in such a way that the ordering of levels is preserved . The resulting permutation is returned in the array given by the user . ]
DdNode * Extra_ReorderCudd( DdManager * dd, DdNode * aFunc, int pPermuteReo[] )
{
    static DdManager * ddReorder = NULL;
    static int * Permute     = NULL;
    static int * PermuteReo1 = NULL;
    static int * PermuteReo2 = NULL;
    DdNode * aFuncReorder, * aFuncNew;
    int lev, var;
    if ( ddReorder == NULL )
    {
        Permute       = ABC_ALLOC( int, dd->size );
        PermuteReo1   = ABC_ALLOC( int, dd->size );
        PermuteReo2   = ABC_ALLOC( int, dd->size );
        ddReorder = Cudd_Init( dd->size, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
        Cudd_AutodynDisable(ddReorder);
    }
    for ( lev = 0; lev < dd->size; lev++ )
    {
        Permute[ dd->invperm[lev] ] = ddReorder->invperm[lev];
        PermuteReo1[ ddReorder->invperm[lev] ] = dd->invperm[lev];
    }
    aFuncReorder = Extra_TransferPermute( dd, ddReorder, aFunc, Permute );  Cudd_Ref( aFuncReorder );
printf( "Nodes before = %d.\n", Cudd_DagSize(aFuncReorder) );
    Cudd_ReduceHeap( ddReorder, CUDD_REORDER_SYMM_SIFT, 1 );
printf( "Nodes before = %d.\n", Cudd_DagSize(aFuncReorder) );
    for ( lev = 0; lev < dd->size; lev++ )
    {
        Permute[ ddReorder->invperm[lev] ] = dd->invperm[lev];
        PermuteReo2[ dd->invperm[lev] ] = ddReorder->invperm[lev];
    }
    aFuncNew = Extra_TransferPermute( ddReorder, dd, aFuncReorder, Permute );  Cudd_Ref( aFuncNew );
    Cudd_RecursiveDeref( ddReorder, aFuncReorder );
    if ( pPermuteReo )
        for ( var = 0; var < dd->size; var++ )
            pPermuteReo[var] = PermuteReo1[ PermuteReo2[var] ];
    Cudd_Deref( aFuncNew );
    return aFuncNew;
}
DdNode * Extra_ReorderCudd ( DdManager * dd , DdNode * aFunc , int pPermuteReo [ ] ) { static DdManager * ddReorder = NULL ; static int * Permute = NULL ; static int * PermuteReo1 = NULL ; static int * PermuteReo2 = NULL ; DdNode * aFuncReorder , * aFuncNew ; int lev , var ; if ( ddReorder == NULL ) { Permute = ABC_ALLOC ( int , dd -> size ) ; PermuteReo1 = ABC_ALLOC ( int , dd -> size ) ; PermuteReo2 = ABC_ALLOC ( int , dd -> size ) ; ddReorder = Cudd_Init ( dd -> size , 0 , CUDD_UNIQUE_SLOTS , CUDD_CACHE_SLOTS , 0 ) ; Cudd_AutodynDisable ( ddReorder ) ; } for ( lev = 0 ; lev < dd -> size ; lev ++ ) { Permute [ dd -> invperm [ lev ] ] = ddReorder -> invperm [ lev ] ; PermuteReo1 [ ddReorder -> invperm [ lev ] ] = dd -> invperm [ lev ] ; } aFuncReorder = Extra_TransferPermute ( dd , ddReorder , aFunc , Permute ) ; Cudd_Ref ( aFuncReorder ) ; printf ( " \n " , Cudd_DagSize ( aFuncReorder ) ) ; Cudd_ReduceHeap ( ddReorder , CUDD_REORDER_SYMM_SIFT , 1 ) ; printf ( " \n " , Cudd_DagSize ( aFuncReorder ) ) ; for ( lev = 0 ; lev < dd -> size ; lev ++ ) { Permute [ ddReorder -> invperm [ lev ] ] = dd -> invperm [ lev ] ; PermuteReo2 [ dd -> invperm [ lev ] ] = ddReorder -> invperm [ lev ] ; } aFuncNew = Extra_TransferPermute ( ddReorder , dd , aFuncReorder , Permute ) ; Cudd_Ref ( aFuncNew ) ; Cudd_RecursiveDeref ( ddReorder , aFuncReorder ) ; if ( pPermuteReo ) for ( var = 0 ; var < dd -> size ; var ++ ) pPermuteReo [ var ] = PermuteReo1 [ PermuteReo2 [ var ] ] ; Cudd_Deref ( aFuncNew ) ; return aFuncNew ; }
Function
Synopsis    [Reorders the DD using CUDD package.]
Function Synopsis [ Reorders the DD using CUDD package . ]
// start the reordering manager // determine the permutation of variable to make sure that var order in bFunc // will not change when this function is transfered into the new manager // transfer this function into the new manager in such a way that ordering of vars does not change //    assert( Cudd_DagSize(aFunc) == Cudd_DagSize(aFuncReorder)  ); // perform the reordering // determine the reverse variable permutation // transfer this function into the new manager in such a way that ordering of vars does not change //    assert( Cudd_DagSize(aFuncNew) == Cudd_DagSize(aFuncReorder)  ); // derive the resulting variable ordering