abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
reoProfile.c File Reference
#include "reo.h"

Go to the source code of this file.

Functions

ABC_NAMESPACE_IMPL_START void reoProfileNodesStart (reo_man *p)
 DECLARATIONS ///. More...
 
void reoProfileAplStart (reo_man *p)
 
void reoProfileWidthStart (reo_man *p)
 
void reoProfileWidthStart2 (reo_man *p)
 
void reoProfileNodesPrint (reo_man *p)
 
void reoProfileAplPrint (reo_man *p)
 
void reoProfileWidthPrint (reo_man *p)
 
void reoProfileWidthVerifyLevel (reo_plane *pPlane, int Level)
 

Function Documentation

void reoProfileAplPrint ( reo_man p)

Function********************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 305 of file reoProfile.c.

306 {
307  printf( "APL: Total = %8.2f. Average =%6.2f.\n", p->nAplCur, p->nAplCur / (float)p->nSupp );
308 }
double nAplCur
Definition: reo.h:132
int nSupp
Definition: reo.h:119
void reoProfileAplStart ( reo_man p)

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 []

Definition at line 78 of file reoProfile.c.

79 {
80  reo_unit * pER, * pTR;
81  reo_unit * pUnit;
82  double Res, Half;
83  int i;
84 
85  // clean the weights of all nodes
86  for ( i = 0; i < p->nSupp; i++ )
87  for ( pUnit = p->pPlanes[i].pHead; pUnit; pUnit = pUnit->Next )
88  pUnit->Weight = 0.0;
89  // to assign the node weights (the probability of visiting each node)
90  // we visit the node after visiting its predecessors
91 
92  // set the probability of visits to the top nodes
93  for ( i = 0; i < p->nTops; i++ )
94  Unit_Regular(p->pTops[i])->Weight += 1.0;
95 
96  // to compute the path length (the sum of products of edge weight by edge length)
97  // we visit the nodes in any order (the above order will do)
98  Res = 0.0;
99  for ( i = 0; i < p->nSupp; i++ )
100  {
101  p->pPlanes[i].statsCost = 0.0;
102  for ( pUnit = p->pPlanes[i].pHead; pUnit; pUnit = pUnit->Next )
103  {
104  pER = Unit_Regular(pUnit->pE);
105  pTR = Unit_Regular(pUnit->pT);
106  Half = 0.5 * pUnit->Weight;
107  pER->Weight += Half;
108  pTR->Weight += Half;
109  // add to the path length
110  p->pPlanes[i].statsCost += pUnit->Weight;
111  }
112  Res += p->pPlanes[i].statsCost;
113  }
114  p->pPlanes[p->nSupp].statsCost = 0.0;
115  p->nAplBeg = p->nAplCur = Res;
116 }
double Weight
Definition: reo.h:77
double nAplCur
Definition: reo.h:132
int nTops
Definition: reo.h:145
int nSupp
Definition: reo.h:119
double nAplBeg
Definition: reo.h:133
reo_unit * pT
Definition: reo.h:75
reo_unit * Next
Definition: reo.h:76
reo_unit * pE
Definition: reo.h:74
double statsCost
Definition: reo.h:86
reo_unit ** pTops
Definition: reo.h:144
#define Unit_Regular(u)
Definition: reo.h:174
reo_plane * pPlanes
Definition: reo.h:142
Definition: reo.h:66
reo_unit * pHead
Definition: reo.h:90
void reoProfileNodesPrint ( reo_man p)

Function********************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 289 of file reoProfile.c.

290 {
291  printf( "NODES: Total = %6d. Average = %6.2f.\n", p->nNodesCur, p->nNodesCur / (float)p->nSupp );
292 }
int nNodesCur
Definition: reo.h:127
int nSupp
Definition: reo.h:119
ABC_NAMESPACE_IMPL_START void reoProfileNodesStart ( reo_man p)

DECLARATIONS ///.

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

]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 []

Definition at line 46 of file reoProfile.c.

47 {
48  int Total, i;
49  Total = 0;
50  for ( i = 0; i <= p->nSupp; i++ )
51  {
52  p->pPlanes[i].statsCost = p->pPlanes[i].statsNodes;
53  Total += p->pPlanes[i].statsNodes;
54  }
55  assert( Total == p->nNodesCur );
56  p->nNodesBeg = p->nNodesCur;
57 }
int nNodesCur
Definition: reo.h:127
int nSupp
Definition: reo.h:119
int nNodesBeg
Definition: reo.h:126
double statsCost
Definition: reo.h:86
reo_plane * pPlanes
Definition: reo.h:142
#define assert(ex)
Definition: util_old.h:213
int statsNodes
Definition: reo.h:83
void reoProfileWidthPrint ( reo_man p)

Function********************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 321 of file reoProfile.c.

322 {
323  int WidthMax;
324  int TotalWidth;
325  int i;
326 
327  WidthMax = 0;
328  TotalWidth = 0;
329  for ( i = 0; i <= p->nSupp; i++ )
330  {
331  printf( "Level = %2d. Width = %3d.\n", i, p->pPlanes[i].statsWidth );
332  if ( WidthMax < p->pPlanes[i].statsWidth )
333  WidthMax = p->pPlanes[i].statsWidth;
334  TotalWidth += p->pPlanes[i].statsWidth;
335  }
336  assert( p->nWidthCur == TotalWidth );
337  printf( "WIDTH: " );
338  printf( "Maximum = %5d. ", WidthMax );
339  printf( "Total = %7d. ", p->nWidthCur );
340  printf( "Average = %6.2f.\n", TotalWidth / (float)p->nSupp );
341 }
int nSupp
Definition: reo.h:119
int statsWidth
Definition: reo.h:84
reo_plane * pPlanes
Definition: reo.h:142
#define assert(ex)
Definition: util_old.h:213
int nWidthCur
Definition: reo.h:129
void reoProfileWidthStart ( reo_man p)

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 []

Definition at line 130 of file reoProfile.c.

131 {
132  reo_unit * pUnit;
133  int * pWidthStart;
134  int * pWidthStop;
135  int v;
136 
137  // allocate and clean the storage for starting and stopping levels
138  pWidthStart = ABC_ALLOC( int, p->nSupp + 1 );
139  pWidthStop = ABC_ALLOC( int, p->nSupp + 1 );
140  memset( pWidthStart, 0, sizeof(int) * (p->nSupp + 1) );
141  memset( pWidthStop, 0, sizeof(int) * (p->nSupp + 1) );
142 
143  // go through the non-constant nodes and set the topmost level of their cofactors
144  for ( v = 0; v <= p->nSupp; v++ )
145  for ( pUnit = p->pPlanes[v].pHead; pUnit; pUnit = pUnit->Next )
146  {
147  pUnit->TopRef = REO_TOPREF_UNDEF;
148  pUnit->Sign = 0;
149  }
150 
151  // add the topmost level of the width profile
152  for ( v = 0; v < p->nTops; v++ )
153  {
154  pUnit = Unit_Regular(p->pTops[v]);
155  if ( pUnit->TopRef == REO_TOPREF_UNDEF )
156  {
157  // set the starting level
158  pUnit->TopRef = 0;
159  pWidthStart[pUnit->TopRef]++;
160  // set the stopping level
161  if ( pUnit->lev != REO_CONST_LEVEL )
162  pWidthStop[pUnit->lev+1]++;
163  }
164  }
165 
166  for ( v = 0; v < p->nSupp; v++ )
167  for ( pUnit = p->pPlanes[v].pHead; pUnit; pUnit = pUnit->Next )
168  {
169  if ( pUnit->pE->TopRef == REO_TOPREF_UNDEF )
170  {
171  // set the starting level
172  pUnit->pE->TopRef = pUnit->lev + 1;
173  pWidthStart[pUnit->pE->TopRef]++;
174  // set the stopping level
175  if ( pUnit->pE->lev != REO_CONST_LEVEL )
176  pWidthStop[pUnit->pE->lev+1]++;
177  }
178  if ( pUnit->pT->TopRef == REO_TOPREF_UNDEF )
179  {
180  // set the starting level
181  pUnit->pT->TopRef = pUnit->lev + 1;
182  pWidthStart[pUnit->pT->TopRef]++;
183  // set the stopping level
184  if ( pUnit->pT->lev != REO_CONST_LEVEL )
185  pWidthStop[pUnit->pT->lev+1]++;
186  }
187  }
188 
189  // verify the top reference
190  for ( v = 0; v < p->nSupp; v++ )
191  reoProfileWidthVerifyLevel( p->pPlanes + v, v );
192 
193  // derive the profile
194  p->nWidthCur = 0;
195  for ( v = 0; v <= p->nSupp; v++ )
196  {
197  if ( v == 0 )
198  p->pPlanes[v].statsWidth = pWidthStart[v] - pWidthStop[v];
199  else
200  p->pPlanes[v].statsWidth = p->pPlanes[v-1].statsWidth + pWidthStart[v] - pWidthStop[v];
201  p->pPlanes[v].statsCost = p->pPlanes[v].statsWidth;
202  p->nWidthCur += p->pPlanes[v].statsWidth;
203  printf( "Level %2d: Width = %5d.\n", v, p->pPlanes[v].statsWidth );
204  }
205  p->nWidthBeg = p->nWidthCur;
206  ABC_FREE( pWidthStart );
207  ABC_FREE( pWidthStop );
208 }
char * memset()
int nWidthBeg
Definition: reo.h:130
short lev
Definition: reo.h:68
int nTops
Definition: reo.h:145
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
int nSupp
Definition: reo.h:119
int statsWidth
Definition: reo.h:84
#define REO_TOPREF_UNDEF
Definition: reo.h:41
reo_unit * pT
Definition: reo.h:75
reo_unit * Next
Definition: reo.h:76
short TopRef
Definition: reo.h:69
reo_unit * pE
Definition: reo.h:74
double statsCost
Definition: reo.h:86
reo_unit ** pTops
Definition: reo.h:144
#define Unit_Regular(u)
Definition: reo.h:174
int Sign
Definition: reo.h:72
reo_plane * pPlanes
Definition: reo.h:142
void reoProfileWidthVerifyLevel(reo_plane *pPlane, int Level)
Definition: reoProfile.c:354
#define ABC_FREE(obj)
Definition: abc_global.h:232
Definition: reo.h:66
reo_unit * pHead
Definition: reo.h:90
#define REO_CONST_LEVEL
Definition: reo.h:40
int nWidthCur
Definition: reo.h:129
void reoProfileWidthStart2 ( reo_man p)

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 []

Definition at line 222 of file reoProfile.c.

223 {
224  reo_unit * pUnit;
225  int i, v;
226 
227  // clean the profile
228  for ( i = 0; i <= p->nSupp; i++ )
229  p->pPlanes[i].statsWidth = 0;
230 
231  // clean the node structures
232  for ( v = 0; v <= p->nSupp; v++ )
233  for ( pUnit = p->pPlanes[v].pHead; pUnit; pUnit = pUnit->Next )
234  {
235  pUnit->TopRef = REO_TOPREF_UNDEF;
236  pUnit->Sign = 0;
237  }
238 
239  // set the topref to the topmost nodes
240  for ( i = 0; i < p->nTops; i++ )
241  Unit_Regular(p->pTops[i])->TopRef = 0;
242 
243  // go through the non-constant nodes and set the topmost level of their cofactors
244  for ( i = 0; i < p->nSupp; i++ )
245  for ( pUnit = p->pPlanes[i].pHead; pUnit; pUnit = pUnit->Next )
246  {
247  if ( pUnit->pE->TopRef > i+1 )
248  pUnit->pE->TopRef = i+1;
249  if ( pUnit->pT->TopRef > i+1 )
250  pUnit->pT->TopRef = i+1;
251  }
252 
253  // verify the top reference
254  for ( i = 0; i < p->nSupp; i++ )
255  reoProfileWidthVerifyLevel( p->pPlanes + i, i );
256 
257  // compute the profile for the internal nodes
258  for ( i = 0; i < p->nSupp; i++ )
259  for ( pUnit = p->pPlanes[i].pHead; pUnit; pUnit = pUnit->Next )
260  for ( v = pUnit->TopRef; v <= pUnit->lev; v++ )
261  p->pPlanes[v].statsWidth++;
262 
263  // compute the profile for the constant nodes
264  for ( pUnit = p->pPlanes[p->nSupp].pHead; pUnit; pUnit = pUnit->Next )
265  for ( v = pUnit->TopRef; v <= p->nSupp; v++ )
266  p->pPlanes[v].statsWidth++;
267 
268  // get the width cost
269  p->nWidthCur = 0;
270  for ( i = 0; i <= p->nSupp; i++ )
271  {
272  p->pPlanes[i].statsCost = p->pPlanes[i].statsWidth;
273  p->nWidthCur += p->pPlanes[i].statsWidth;
274  }
275  p->nWidthBeg = p->nWidthCur;
276 }
int nWidthBeg
Definition: reo.h:130
int nTops
Definition: reo.h:145
int nSupp
Definition: reo.h:119
int statsWidth
Definition: reo.h:84
for(p=first;p->value< newval;p=p->next)
#define REO_TOPREF_UNDEF
Definition: reo.h:41
reo_unit * pT
Definition: reo.h:75
reo_unit * Next
Definition: reo.h:76
short TopRef
Definition: reo.h:69
reo_unit * pE
Definition: reo.h:74
double statsCost
Definition: reo.h:86
reo_unit ** pTops
Definition: reo.h:144
#define Unit_Regular(u)
Definition: reo.h:174
int Sign
Definition: reo.h:72
reo_plane * pPlanes
Definition: reo.h:142
void reoProfileWidthVerifyLevel(reo_plane *pPlane, int Level)
Definition: reoProfile.c:354
Definition: reo.h:66
reo_unit * pHead
Definition: reo.h:90
int nWidthCur
Definition: reo.h:129
void reoProfileWidthVerifyLevel ( reo_plane pPlane,
int  Level 
)

Function********************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 354 of file reoProfile.c.

355 {
356  reo_unit * pUnit;
357  for ( pUnit = pPlane->pHead; pUnit; pUnit = pUnit->Next )
358  {
359  assert( pUnit->TopRef <= Level );
360  assert( pUnit->pE->TopRef <= Level + 1 );
361  assert( pUnit->pT->TopRef <= Level + 1 );
362  }
363 }
reo_unit * pT
Definition: reo.h:75
reo_unit * Next
Definition: reo.h:76
short TopRef
Definition: reo.h:69
reo_unit * pE
Definition: reo.h:74
Definition: reo.h:66
#define assert(ex)
Definition: util_old.h:213
reo_unit * pHead
Definition: reo.h:90