diff options
Diffstat (limited to 'src/bdd/reo/reoCore.c')
-rw-r--r-- | src/bdd/reo/reoCore.c | 438 |
1 files changed, 0 insertions, 438 deletions
diff --git a/src/bdd/reo/reoCore.c b/src/bdd/reo/reoCore.c deleted file mode 100644 index 3782631c..00000000 --- a/src/bdd/reo/reoCore.c +++ /dev/null @@ -1,438 +0,0 @@ -/**CFile**************************************************************** - - FileName [reoCore.c] - - PackageName [REO: A specialized DD reordering engine.] - - Synopsis [Implementation of the core reordering procedure.] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - October 15, 2002.] - - Revision [$Id: reoCore.c,v 1.0 2002/15/10 03:00:00 alanmi Exp $] - -***********************************************************************/ - -#include "reo.h" - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -#define CALLOC(type, num) ((type *) calloc((long)(num), (long)sizeof(type))) - -static int reoRecursiveDeref( reo_unit * pUnit ); -static int reoCheckZeroRefs( reo_plane * pPlane ); -static int reoCheckLevels( reo_man * p ); - -double s_AplBefore; -double s_AplAfter; - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void reoReorderArray( reo_man * p, DdManager * dd, DdNode * Funcs[], DdNode * FuncsRes[], int nFuncs, int * pOrder ) -{ - int Counter, i; - - // set the initial parameters - p->dd = dd; - p->pOrder = pOrder; - p->nTops = nFuncs; - // get the initial number of nodes - p->nNodesBeg = Cudd_SharingSize( Funcs, nFuncs ); - // resize the internal data structures of the manager if necessary - reoResizeStructures( p, ddMax(dd->size,dd->sizeZ), p->nNodesBeg, nFuncs ); - // compute the support - p->pSupp = Extra_VectorSupportArray( dd, Funcs, nFuncs, p->pSupp ); - // get the number of support variables - p->nSupp = 0; - for ( i = 0; i < dd->size; i++ ) - p->nSupp += p->pSupp[i]; - - // if it is the constant function, no need to reorder - if ( p->nSupp == 0 ) - { - for ( i = 0; i < nFuncs; i++ ) - { - FuncsRes[i] = Funcs[i]; Cudd_Ref( FuncsRes[i] ); - } - return; - } - - // create the internal variable maps - // go through variable levels in the manager - Counter = 0; - for ( i = 0; i < dd->size; i++ ) - if ( p->pSupp[ dd->invperm[i] ] ) - { - p->pMapToPlanes[ dd->invperm[i] ] = Counter; - p->pMapToDdVarsOrig[Counter] = dd->invperm[i]; - if ( !p->fRemapUp ) - p->pMapToDdVarsFinal[Counter] = dd->invperm[i]; - else - p->pMapToDdVarsFinal[Counter] = dd->invperm[Counter]; - p->pOrderInt[Counter] = Counter; - Counter++; - } - - // set the initial parameters - p->nUnitsUsed = 0; - p->nNodesCur = 0; - p->fThisIsAdd = 0; - p->Signature++; - // transfer the function from the CUDD package into REO"s internal data structure - for ( i = 0; i < nFuncs; i++ ) - p->pTops[i] = reoTransferNodesToUnits_rec( p, Funcs[i] ); - assert( p->nNodesBeg == p->nNodesCur ); - - if ( !p->fThisIsAdd && p->fMinWidth ) - { - printf( "An important message from the REO reordering engine:\n" ); - printf( "The BDD given to the engine for reordering contains complemented edges.\n" ); - printf( "Currently, such BDDs cannot be reordered for the minimum width.\n" ); - printf( "Therefore, minimization for the number of BDD nodes is performed.\n" ); - fflush( stdout ); - p->fMinApl = 0; - p->fMinWidth = 0; - } - - if ( p->fMinWidth ) - reoProfileWidthStart(p); - else if ( p->fMinApl ) - reoProfileAplStart(p); - else - reoProfileNodesStart(p); - - if ( p->fVerbose ) - { - printf( "INITIAL: " ); - if ( p->fMinWidth ) - reoProfileWidthPrint(p); - else if ( p->fMinApl ) - reoProfileAplPrint(p); - else - reoProfileNodesPrint(p); - } - - /////////////////////////////////////////////////////////////////// - // performs the reordering - p->nSwaps = 0; - p->nNISwaps = 0; - for ( i = 0; i < p->nIters; i++ ) - { - reoReorderSift( p ); - // print statistics after each iteration - if ( p->fVerbose ) - { - printf( "ITER #%d: ", i+1 ); - if ( p->fMinWidth ) - reoProfileWidthPrint(p); - else if ( p->fMinApl ) - reoProfileAplPrint(p); - else - reoProfileNodesPrint(p); - } - // if the cost function did not change, stop iterating - if ( p->fMinWidth ) - { - p->nWidthEnd = p->nWidthCur; - assert( p->nWidthEnd <= p->nWidthBeg ); - if ( p->nWidthEnd == p->nWidthBeg ) - break; - } - else if ( p->fMinApl ) - { - p->nAplEnd = p->nAplCur; - assert( p->nAplEnd <= p->nAplBeg ); - if ( p->nAplEnd == p->nAplBeg ) - break; - } - else - { - p->nNodesEnd = p->nNodesCur; - assert( p->nNodesEnd <= p->nNodesBeg ); - if ( p->nNodesEnd == p->nNodesBeg ) - break; - } - } - assert( reoCheckLevels( p ) ); - /////////////////////////////////////////////////////////////////// - -s_AplBefore = p->nAplBeg; -s_AplAfter = p->nAplEnd; - - // set the initial parameters - p->nRefNodes = 0; - p->nNodesCur = 0; - p->Signature++; - // transfer the BDDs from REO's internal data structure to CUDD - for ( i = 0; i < nFuncs; i++ ) - { - FuncsRes[i] = reoTransferUnitsToNodes_rec( p, p->pTops[i] ); Cudd_Ref( FuncsRes[i] ); - } - // undo the DDs referenced for storing in the cache - for ( i = 0; i < p->nRefNodes; i++ ) - Cudd_RecursiveDeref( dd, p->pRefNodes[i] ); - // verify zero refs of the terminal nodes - for ( i = 0; i < nFuncs; i++ ) - { - assert( reoRecursiveDeref( p->pTops[i] ) ); - } - assert( reoCheckZeroRefs( &(p->pPlanes[p->nSupp]) ) ); - - // prepare the variable map to return to the user - if ( p->pOrder ) - { - // i is the current level in the planes data structure - // p->pOrderInt[i] is the original level in the planes data structure - // p->pMapToDdVarsOrig[i] is the variable, into which we remap when we construct the BDD from planes - // p->pMapToDdVarsOrig[ p->pOrderInt[i] ] is the original BDD variable corresponding to this level - // Therefore, p->pOrder[ p->pMapToDdVarsFinal[i] ] = p->pMapToDdVarsOrig[ p->pOrderInt[i] ] - // creates the permutation, which remaps the resulting BDD variable into the original BDD variable - for ( i = 0; i < p->nSupp; i++ ) - p->pOrder[ p->pMapToDdVarsFinal[i] ] = p->pMapToDdVarsOrig[ p->pOrderInt[i] ]; - } - - if ( p->fVerify ) - { - int fVerification; - DdNode * FuncRemapped; - int * pOrder; - - if ( p->pOrder == NULL ) - { - pOrder = ALLOC( int, p->nSupp ); - for ( i = 0; i < p->nSupp; i++ ) - pOrder[ p->pMapToDdVarsFinal[i] ] = p->pMapToDdVarsOrig[ p->pOrderInt[i] ]; - } - else - pOrder = p->pOrder; - - fVerification = 1; - for ( i = 0; i < nFuncs; i++ ) - { - // verify the result - if ( p->fThisIsAdd ) - FuncRemapped = Cudd_addPermute( dd, FuncsRes[i], pOrder ); - else - FuncRemapped = Cudd_bddPermute( dd, FuncsRes[i], pOrder ); - Cudd_Ref( FuncRemapped ); - - if ( FuncRemapped != Funcs[i] ) - { - fVerification = 0; - printf( "REO: Internal verification has failed!\n" ); - fflush( stdout ); - } - Cudd_RecursiveDeref( dd, FuncRemapped ); - } - if ( fVerification ) - printf( "REO: Internal verification is okay!\n" ); - - if ( p->pOrder == NULL ) - free( pOrder ); - } - - // recycle the data structure - for ( i = 0; i <= p->nSupp; i++ ) - reoUnitsRecycleUnitList( p, p->pPlanes + i ); -} - -/**Function************************************************************* - - Synopsis [Resizes the internal manager data structures.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void reoResizeStructures( reo_man * p, int nDdVarsMax, int nNodesMax, int nFuncs ) -{ - // resize data structures depending on the number of variables in the DD manager - if ( p->nSuppAlloc == 0 ) - { - p->pSupp = ALLOC( int, nDdVarsMax + 1 ); - p->pOrderInt = ALLOC( int, nDdVarsMax + 1 ); - p->pMapToPlanes = ALLOC( int, nDdVarsMax + 1 ); - p->pMapToDdVarsOrig = ALLOC( int, nDdVarsMax + 1 ); - p->pMapToDdVarsFinal = ALLOC( int, nDdVarsMax + 1 ); - p->pPlanes = CALLOC( reo_plane, nDdVarsMax + 1 ); - p->pVarCosts = ALLOC( double, nDdVarsMax + 1 ); - p->pLevelOrder = ALLOC( int, nDdVarsMax + 1 ); - p->nSuppAlloc = nDdVarsMax + 1; - } - else if ( p->nSuppAlloc < nDdVarsMax ) - { - free( p->pSupp ); - free( p->pOrderInt ); - free( p->pMapToPlanes ); - free( p->pMapToDdVarsOrig ); - free( p->pMapToDdVarsFinal ); - free( p->pPlanes ); - free( p->pVarCosts ); - free( p->pLevelOrder ); - - p->pSupp = ALLOC( int, nDdVarsMax + 1 ); - p->pOrderInt = ALLOC( int, nDdVarsMax + 1 ); - p->pMapToPlanes = ALLOC( int, nDdVarsMax + 1 ); - p->pMapToDdVarsOrig = ALLOC( int, nDdVarsMax + 1 ); - p->pMapToDdVarsFinal = ALLOC( int, nDdVarsMax + 1 ); - p->pPlanes = CALLOC( reo_plane, nDdVarsMax + 1 ); - p->pVarCosts = ALLOC( double, nDdVarsMax + 1 ); - p->pLevelOrder = ALLOC( int, nDdVarsMax + 1 ); - p->nSuppAlloc = nDdVarsMax + 1; - } - - // resize the data structures depending on the number of nodes - if ( p->nRefNodesAlloc == 0 ) - { - p->nNodesMaxAlloc = nNodesMax; - p->nTableSize = 3*nNodesMax + 1; - p->nRefNodesAlloc = 3*nNodesMax + 1; - p->nMemChunksAlloc = (10*nNodesMax + 1)/REO_CHUNK_SIZE + 1; - - p->HTable = CALLOC( reo_hash, p->nTableSize ); - p->pRefNodes = ALLOC( DdNode *, p->nRefNodesAlloc ); - p->pWidthCofs = ALLOC( reo_unit *, p->nRefNodesAlloc ); - p->pMemChunks = ALLOC( reo_unit *, p->nMemChunksAlloc ); - } - else if ( p->nNodesMaxAlloc < nNodesMax ) - { - void * pTemp; - int nMemChunksAllocPrev = p->nMemChunksAlloc; - - p->nNodesMaxAlloc = nNodesMax; - p->nTableSize = 3*nNodesMax + 1; - p->nRefNodesAlloc = 3*nNodesMax + 1; - p->nMemChunksAlloc = (10*nNodesMax + 1)/REO_CHUNK_SIZE + 1; - - free( p->HTable ); - free( p->pRefNodes ); - free( p->pWidthCofs ); - p->HTable = CALLOC( reo_hash, p->nTableSize ); - p->pRefNodes = ALLOC( DdNode *, p->nRefNodesAlloc ); - p->pWidthCofs = ALLOC( reo_unit *, p->nRefNodesAlloc ); - // p->pMemChunks should be reallocated because it contains pointers currently in use - pTemp = ALLOC( reo_unit *, p->nMemChunksAlloc ); - memmove( pTemp, p->pMemChunks, sizeof(reo_unit *) * nMemChunksAllocPrev ); - free( p->pMemChunks ); - p->pMemChunks = pTemp; - } - - // resize the data structures depending on the number of functions - if ( p->nTopsAlloc == 0 ) - { - p->pTops = ALLOC( reo_unit *, nFuncs ); - p->nTopsAlloc = nFuncs; - } - else if ( p->nTopsAlloc < nFuncs ) - { - free( p->pTops ); - p->pTops = ALLOC( reo_unit *, nFuncs ); - p->nTopsAlloc = nFuncs; - } -} - - -/**Function************************************************************* - - Synopsis [Dereferences units the data structure after reordering.] - - Description [This function is only useful for debugging.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int reoRecursiveDeref( reo_unit * pUnit ) -{ - reo_unit * pUnitR; - pUnitR = Unit_Regular(pUnit); - pUnitR->n--; - if ( Unit_IsConstant(pUnitR) ) - return 1; - if ( pUnitR->n == 0 ) - { - reoRecursiveDeref( pUnitR->pE ); - reoRecursiveDeref( pUnitR->pT ); - } - return 1; -} - -/**Function************************************************************* - - Synopsis [Checks the zero references for the given plane.] - - Description [This function is only useful for debugging.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int reoCheckZeroRefs( reo_plane * pPlane ) -{ - reo_unit * pUnit; - for ( pUnit = pPlane->pHead; pUnit; pUnit = pUnit->Next ) - { - if ( pUnit->n != 0 ) - { - assert( 0 ); - } - } - return 1; -} - -/**Function************************************************************* - - Synopsis [Checks the zero references for the given plane.] - - Description [This function is only useful for debugging.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int reoCheckLevels( reo_man * p ) -{ - reo_unit * pUnit; - int i; - - for ( i = 0; i < p->nSupp; i++ ) - { - // there are some nodes left on each level - assert( p->pPlanes[i].statsNodes ); - for ( pUnit = p->pPlanes[i].pHead; pUnit; pUnit = pUnit->Next ) - { - // the level is properly set - assert( pUnit->lev == i ); - } - } - return 1; -} - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - |