diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2007-10-01 08:01:00 -0700 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2007-10-01 08:01:00 -0700 |
commit | 4812c90424dfc40d26725244723887a2d16ddfd9 (patch) | |
tree | b32ace96e7e2d84d586e09ba605463b6f49c3271 /src/bdd/reo/reoProfile.c | |
parent | e54d9691616b9a0326e2fdb3156bb4eeb8abfcd7 (diff) | |
download | abc-4812c90424dfc40d26725244723887a2d16ddfd9.tar.gz abc-4812c90424dfc40d26725244723887a2d16ddfd9.tar.bz2 abc-4812c90424dfc40d26725244723887a2d16ddfd9.zip |
Version abc71001
Diffstat (limited to 'src/bdd/reo/reoProfile.c')
-rw-r--r-- | src/bdd/reo/reoProfile.c | 365 |
1 files changed, 365 insertions, 0 deletions
diff --git a/src/bdd/reo/reoProfile.c b/src/bdd/reo/reoProfile.c new file mode 100644 index 00000000..84a0bc19 --- /dev/null +++ b/src/bdd/reo/reoProfile.c @@ -0,0 +1,365 @@ +/**CFile**************************************************************** + + FileName [reoProfile.c] + + PackageName [REO: A specialized DD reordering engine.] + + Synopsis [Procudures that compute variables profiles (nodes, width, APL).] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - October 15, 2002.] + + Revision [$Id: reoProfile.c,v 1.0 2002/15/10 03:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "reo.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + + +/**Function******************************************************************** + + Synopsis [Start the profile for the BDD nodes.] + + Description [TopRef is the first level, on this the given node counts towards + the width of the BDDs. (In other words, it is the level of the referencing node plus 1.)] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +void reoProfileNodesStart( reo_man * p ) +{ + int Total, i; + Total = 0; + for ( i = 0; i <= p->nSupp; i++ ) + { + p->pPlanes[i].statsCost = p->pPlanes[i].statsNodes; + Total += p->pPlanes[i].statsNodes; + } + assert( Total == p->nNodesCur ); + p->nNodesBeg = p->nNodesCur; +} + +/**Function************************************************************* + + Synopsis [Start the profile for the APL.] + + Description [Computes the total path length. The path length is normalized + by dividing it by 2^|supp(f)|. To get the "real" APL, multiply by 2^|supp(f)|. + This procedure assumes that Weight field of all nodes has been set to 0.0 + before the call, except for the weight of the topmost node, which is set to 1.0 + (1.0 is the probability of traversing the topmost node). This procedure + assigns the edge weights. Because of the equal probability of selecting 0 and 1 + assignment at a node, the edge weights are the same for the node. + Instead of storing them, we store the weight of the node, which is the probability + of traversing the node (pUnit->Weight) during the top down evalation of the BDD. ] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void reoProfileAplStart( reo_man * p ) +{ + reo_unit * pER, * pTR; + reo_unit * pUnit; + double Res, Half; + int i; + + // clean the weights of all nodes + for ( i = 0; i < p->nSupp; i++ ) + for ( pUnit = p->pPlanes[i].pHead; pUnit; pUnit = pUnit->Next ) + pUnit->Weight = 0.0; + // to assign the node weights (the probability of visiting each node) + // we visit the node after visiting its predecessors + + // set the probability of visits to the top nodes + for ( i = 0; i < p->nTops; i++ ) + Unit_Regular(p->pTops[i])->Weight += 1.0; + + // to compute the path length (the sum of products of edge weight by edge length) + // we visit the nodes in any order (the above order will do) + Res = 0.0; + for ( i = 0; i < p->nSupp; i++ ) + { + p->pPlanes[i].statsCost = 0.0; + for ( pUnit = p->pPlanes[i].pHead; pUnit; pUnit = pUnit->Next ) + { + pER = Unit_Regular(pUnit->pE); + pTR = Unit_Regular(pUnit->pT); + Half = 0.5 * pUnit->Weight; + pER->Weight += Half; + pTR->Weight += Half; + // add to the path length + p->pPlanes[i].statsCost += pUnit->Weight; + } + Res += p->pPlanes[i].statsCost; + } + p->pPlanes[p->nSupp].statsCost = 0.0; + p->nAplBeg = p->nAplCur = Res; +} + +/**Function******************************************************************** + + Synopsis [Start the profile for the BDD width. Complexity of the algorithm is O(N + n).] + + Description [TopRef is the first level, on which the given node counts towards + the width of the BDDs. (In other words, it is the level of the referencing node plus 1.)] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +void reoProfileWidthStart( reo_man * p ) +{ + reo_unit * pUnit; + int * pWidthStart; + int * pWidthStop; + int v; + + // allocate and clean the storage for starting and stopping levels + pWidthStart = ALLOC( int, p->nSupp + 1 ); + pWidthStop = ALLOC( int, p->nSupp + 1 ); + memset( pWidthStart, 0, sizeof(int) * (p->nSupp + 1) ); + memset( pWidthStop, 0, sizeof(int) * (p->nSupp + 1) ); + + // go through the non-constant nodes and set the topmost level of their cofactors + for ( v = 0; v <= p->nSupp; v++ ) + for ( pUnit = p->pPlanes[v].pHead; pUnit; pUnit = pUnit->Next ) + { + pUnit->TopRef = REO_TOPREF_UNDEF; + pUnit->Sign = 0; + } + + // add the topmost level of the width profile + for ( v = 0; v < p->nTops; v++ ) + { + pUnit = Unit_Regular(p->pTops[v]); + if ( pUnit->TopRef == REO_TOPREF_UNDEF ) + { + // set the starting level + pUnit->TopRef = 0; + pWidthStart[pUnit->TopRef]++; + // set the stopping level + if ( pUnit->lev != REO_CONST_LEVEL ) + pWidthStop[pUnit->lev+1]++; + } + } + + for ( v = 0; v < p->nSupp; v++ ) + for ( pUnit = p->pPlanes[v].pHead; pUnit; pUnit = pUnit->Next ) + { + if ( pUnit->pE->TopRef == REO_TOPREF_UNDEF ) + { + // set the starting level + pUnit->pE->TopRef = pUnit->lev + 1; + pWidthStart[pUnit->pE->TopRef]++; + // set the stopping level + if ( pUnit->pE->lev != REO_CONST_LEVEL ) + pWidthStop[pUnit->pE->lev+1]++; + } + if ( pUnit->pT->TopRef == REO_TOPREF_UNDEF ) + { + // set the starting level + pUnit->pT->TopRef = pUnit->lev + 1; + pWidthStart[pUnit->pT->TopRef]++; + // set the stopping level + if ( pUnit->pT->lev != REO_CONST_LEVEL ) + pWidthStop[pUnit->pT->lev+1]++; + } + } + + // verify the top reference + for ( v = 0; v < p->nSupp; v++ ) + reoProfileWidthVerifyLevel( p->pPlanes + v, v ); + + // derive the profile + p->nWidthCur = 0; + for ( v = 0; v <= p->nSupp; v++ ) + { + if ( v == 0 ) + p->pPlanes[v].statsWidth = pWidthStart[v] - pWidthStop[v]; + else + p->pPlanes[v].statsWidth = p->pPlanes[v-1].statsWidth + pWidthStart[v] - pWidthStop[v]; + p->pPlanes[v].statsCost = p->pPlanes[v].statsWidth; + p->nWidthCur += p->pPlanes[v].statsWidth; +// printf( "Level %2d: Width = %5d. Correct = %d.\n", v, Temp, p->pPlanes[v].statsWidth ); + } + p->nWidthBeg = p->nWidthCur; + free( pWidthStart ); + free( pWidthStop ); +} + +/**Function******************************************************************** + + Synopsis [Start the profile for the BDD width. Complexity of the algorithm is O(N * n).] + + Description [TopRef is the first level, on which the given node counts towards + the width of the BDDs. (In other words, it is the level of the referencing node plus 1.)] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +void reoProfileWidthStart2( reo_man * p ) +{ + reo_unit * pUnit; + int i, v; + + // clean the profile + for ( i = 0; i <= p->nSupp; i++ ) + p->pPlanes[i].statsWidth = 0; + + // clean the node structures + for ( v = 0; v <= p->nSupp; v++ ) + for ( pUnit = p->pPlanes[v].pHead; pUnit; pUnit = pUnit->Next ) + { + pUnit->TopRef = REO_TOPREF_UNDEF; + pUnit->Sign = 0; + } + + // set the topref to the topmost nodes + for ( i = 0; i < p->nTops; i++ ) + Unit_Regular(p->pTops[i])->TopRef = 0; + + // go through the non-constant nodes and set the topmost level of their cofactors + for ( i = 0; i < p->nSupp; i++ ) + for ( pUnit = p->pPlanes[i].pHead; pUnit; pUnit = pUnit->Next ) + { + if ( pUnit->pE->TopRef > i+1 ) + pUnit->pE->TopRef = i+1; + if ( pUnit->pT->TopRef > i+1 ) + pUnit->pT->TopRef = i+1; + } + + // verify the top reference + for ( i = 0; i < p->nSupp; i++ ) + reoProfileWidthVerifyLevel( p->pPlanes + i, i ); + + // compute the profile for the internal nodes + for ( i = 0; i < p->nSupp; i++ ) + for ( pUnit = p->pPlanes[i].pHead; pUnit; pUnit = pUnit->Next ) + for ( v = pUnit->TopRef; v <= pUnit->lev; v++ ) + p->pPlanes[v].statsWidth++; + + // compute the profile for the constant nodes + for ( pUnit = p->pPlanes[p->nSupp].pHead; pUnit; pUnit = pUnit->Next ) + for ( v = pUnit->TopRef; v <= p->nSupp; v++ ) + p->pPlanes[v].statsWidth++; + + // get the width cost + p->nWidthCur = 0; + for ( i = 0; i <= p->nSupp; i++ ) + { + p->pPlanes[i].statsCost = p->pPlanes[i].statsWidth; + p->nWidthCur += p->pPlanes[i].statsWidth; + } + p->nWidthBeg = p->nWidthCur; +} + +/**Function******************************************************************** + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +void reoProfileNodesPrint( reo_man * p ) +{ + printf( "NODES: Total = %6d. Average = %6.2f.\n", p->nNodesCur, p->nNodesCur / (float)p->nSupp ); +} + +/**Function******************************************************************** + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +void reoProfileAplPrint( reo_man * p ) +{ + printf( "APL: Total = %8.2f. Average =%6.2f.\n", p->nAplCur, p->nAplCur / (float)p->nSupp ); +} + +/**Function******************************************************************** + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +void reoProfileWidthPrint( reo_man * p ) +{ + int WidthMax; + int TotalWidth; + int i; + + WidthMax = 0; + TotalWidth = 0; + for ( i = 0; i <= p->nSupp; i++ ) + { +// printf( "Level = %2d. Width = %3d.\n", i, p->pProfile[i] ); + if ( WidthMax < p->pPlanes[i].statsWidth ) + WidthMax = p->pPlanes[i].statsWidth; + TotalWidth += p->pPlanes[i].statsWidth; + } + assert( p->nWidthCur == TotalWidth ); + printf( "WIDTH: " ); + printf( "Maximum = %5d. ", WidthMax ); + printf( "Total = %7d. ", p->nWidthCur ); + printf( "Average = %6.2f.\n", TotalWidth / (float)p->nSupp ); +} + +/**Function******************************************************************** + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +void reoProfileWidthVerifyLevel( reo_plane * pPlane, int Level ) +{ + reo_unit * pUnit; + for ( pUnit = pPlane->pHead; pUnit; pUnit = pUnit->Next ) + { + assert( pUnit->TopRef <= Level ); + assert( pUnit->pE->TopRef <= Level + 1 ); + assert( pUnit->pT->TopRef <= Level + 1 ); + } +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + |