abcBridge-0.10.0.0: abc-build/src/bdd/reo/reoCore.c
/**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"
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
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:\n" );
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:\n", 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 = ABC_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 )
ABC_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 = ABC_ALLOC( int, nDdVarsMax + 1 );
p->pOrderInt = ABC_ALLOC( int, nDdVarsMax + 1 );
p->pMapToPlanes = ABC_ALLOC( int, nDdVarsMax + 1 );
p->pMapToDdVarsOrig = ABC_ALLOC( int, nDdVarsMax + 1 );
p->pMapToDdVarsFinal = ABC_ALLOC( int, nDdVarsMax + 1 );
p->pPlanes = ABC_CALLOC( reo_plane, nDdVarsMax + 1 );
p->pVarCosts = ABC_ALLOC( double, nDdVarsMax + 1 );
p->pLevelOrder = ABC_ALLOC( int, nDdVarsMax + 1 );
p->nSuppAlloc = nDdVarsMax + 1;
}
else if ( p->nSuppAlloc < nDdVarsMax )
{
ABC_FREE( p->pSupp );
ABC_FREE( p->pOrderInt );
ABC_FREE( p->pMapToPlanes );
ABC_FREE( p->pMapToDdVarsOrig );
ABC_FREE( p->pMapToDdVarsFinal );
ABC_FREE( p->pPlanes );
ABC_FREE( p->pVarCosts );
ABC_FREE( p->pLevelOrder );
p->pSupp = ABC_ALLOC( int, nDdVarsMax + 1 );
p->pOrderInt = ABC_ALLOC( int, nDdVarsMax + 1 );
p->pMapToPlanes = ABC_ALLOC( int, nDdVarsMax + 1 );
p->pMapToDdVarsOrig = ABC_ALLOC( int, nDdVarsMax + 1 );
p->pMapToDdVarsFinal = ABC_ALLOC( int, nDdVarsMax + 1 );
p->pPlanes = ABC_CALLOC( reo_plane, nDdVarsMax + 1 );
p->pVarCosts = ABC_ALLOC( double, nDdVarsMax + 1 );
p->pLevelOrder = ABC_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 = ABC_CALLOC( reo_hash, p->nTableSize );
p->pRefNodes = ABC_ALLOC( DdNode *, p->nRefNodesAlloc );
p->pWidthCofs = ABC_ALLOC( reo_unit *, p->nRefNodesAlloc );
p->pMemChunks = ABC_ALLOC( reo_unit *, p->nMemChunksAlloc );
}
else if ( p->nNodesMaxAlloc < nNodesMax )
{
reo_unit ** 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;
ABC_FREE( p->HTable );
ABC_FREE( p->pRefNodes );
ABC_FREE( p->pWidthCofs );
p->HTable = ABC_CALLOC( reo_hash, p->nTableSize );
p->pRefNodes = ABC_ALLOC( DdNode *, p->nRefNodesAlloc );
p->pWidthCofs = ABC_ALLOC( reo_unit *, p->nRefNodesAlloc );
// p->pMemChunks should be reallocated because it contains pointers currently in use
pTemp = ABC_ALLOC( reo_unit *, p->nMemChunksAlloc );
memmove( pTemp, p->pMemChunks, sizeof(reo_unit *) * nMemChunksAllocPrev );
ABC_FREE( p->pMemChunks );
p->pMemChunks = pTemp;
}
// resize the data structures depending on the number of functions
if ( p->nTopsAlloc == 0 )
{
p->pTops = ABC_ALLOC( reo_unit *, nFuncs );
p->nTopsAlloc = nFuncs;
}
else if ( p->nTopsAlloc < nFuncs )
{
ABC_FREE( p->pTops );
p->pTops = ABC_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 ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END