ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
reoSift.c File Reference
#include "reo.h"
Include dependency graph for reoSift.c:

Go to the source code of this file.

Functions

ABC_NAMESPACE_IMPL_START void reoReorderSift (reo_man *p)
 DECLARATIONS ///.
 

Function Documentation

◆ reoReorderSift()

ABC_NAMESPACE_IMPL_START void reoReorderSift ( reo_man * p)

DECLARATIONS ///.

CFile****************************************************************

FileName [reoSift.c]

PackageName [REO: A specialized DD reordering engine.]

Synopsis [Implementation of the sifting algorihtm.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - October 15, 2002.]

Revision [

Id
reoSift.c,v 1.0 2002/15/10 03:00:00 alanmi Exp

] FUNCTION DEFINITIONS /// Function*************************************************************

Synopsis [Implements the variable sifting algorithm.]

Description [Performs a sequence of adjacent variable swaps known as "sifting". Uses the cost functions determined by the flag.]

SideEffects []

SeeAlso []

Definition at line 44 of file reoSift.c.

45{
46 double CostCurrent; // the cost of the current permutation
47 double CostLimit; // the maximum increase in cost that can be tolerated
48 double CostBest; // the best cost
49 int BestQ; // the best position
50 int VarCurrent; // the current variable to move
51 int q; // denotes the current position of the variable
52 int c; // performs the loops over variables until all of them are sifted
53 int v; // used for other purposes
54
55 assert( p->nSupp > 0 );
56
57 // set the current cost depending on the minimization criteria
58 if ( p->fMinWidth )
59 CostCurrent = p->nWidthCur;
60 else if ( p->fMinApl )
61 CostCurrent = p->nAplCur;
62 else
63 CostCurrent = p->nNodesCur;
64
65 // find the upper bound on tbe cost growth
66 CostLimit = 1 + (int)(REO_REORDER_LIMIT * CostCurrent);
67
68 // perform sifting for each of p->nSupp variables
69 for ( c = 0; c < p->nSupp; c++ )
70 {
71 // select the current variable to be the one with the largest number of nodes that is not sifted yet
72 VarCurrent = -1;
73 CostBest = -1.0;
74 for ( v = 0; v < p->nSupp; v++ )
75 {
76 p->pVarCosts[v] = REO_HIGH_VALUE;
77 if ( !p->pPlanes[v].fSifted )
78 {
79// VarCurrent = v;
80// if ( CostBest < p->pPlanes[v].statsCost )
81 if ( CostBest < p->pPlanes[v].statsNodes )
82 {
83// CostBest = p->pPlanes[v].statsCost;
84 CostBest = p->pPlanes[v].statsNodes;
85 VarCurrent = v;
86 }
87
88 }
89 }
90 assert( VarCurrent != -1 );
91 // mark this variable as sifted
92 p->pPlanes[VarCurrent].fSifted = 1;
93
94 // set the current value
95 p->pVarCosts[VarCurrent] = CostCurrent;
96
97 // set the best cost
98 CostBest = CostCurrent;
99 BestQ = VarCurrent;
100
101 // determine which way to move the variable first (up or down)
102 // the rationale is that if we move the shorter way first
103 // it is more likely that the best position will be found on the longer way
104 // and the reverse movement (to take the best position) will be faster
105 if ( VarCurrent < p->nSupp/2 ) // move up first, then down
106 {
107 // set the total cost on all levels above the current level
108 p->pPlanes[0].statsCostAbove = 0;
109 for ( v = 1; v <= VarCurrent; v++ )
110 p->pPlanes[v].statsCostAbove = p->pPlanes[v-1].statsCostAbove + p->pPlanes[v-1].statsCost;
111 // set the total cost on all levels below the current level
112 p->pPlanes[p->nSupp].statsCostBelow = 0;
113 for ( v = p->nSupp - 1; v >= VarCurrent; v-- )
114 p->pPlanes[v].statsCostBelow = p->pPlanes[v+1].statsCostBelow + p->pPlanes[v+1].statsCost;
115
116 assert( CostCurrent == p->pPlanes[VarCurrent].statsCostAbove +
117 p->pPlanes[VarCurrent].statsCost +
118 p->pPlanes[VarCurrent].statsCostBelow );
119
120 // move up
121 for ( q = VarCurrent-1; q >= 0; q-- )
122 {
123 CostCurrent -= reoReorderSwapAdjacentVars( p, q, 1 );
124 // now q points to the position of this var in the order
125 p->pVarCosts[q] = CostCurrent;
126 // update the lower bound (assuming that for level q+1 it is set correctly)
127 p->pPlanes[q].statsCostBelow = p->pPlanes[q+1].statsCostBelow + p->pPlanes[q+1].statsCost;
128 // check the upper bound
129 if ( CostCurrent >= CostLimit )
130 break;
131 // check the lower bound
132 if ( p->pPlanes[q].statsCostBelow + (REO_QUAL_PAR-1)*p->pPlanes[q].statsCostAbove/REO_QUAL_PAR >= CostBest )
133 break;
134 // update the best cost
135 if ( CostBest > CostCurrent )
136 {
137 CostBest = CostCurrent;
138 BestQ = q;
139 // adjust node limit
140 CostLimit = ddMin( CostLimit, 1 + (int)(REO_REORDER_LIMIT * CostCurrent) );
141 }
142
143 // when we are reordering for width or APL, it may happen that
144 // the number of nodes has grown above certain limit,
145 // in which case we have to resize the data structures
146 if ( p->fMinWidth || p->fMinApl )
147 {
148 if ( p->nNodesCur >= 2 * p->nNodesMaxAlloc )
149 {
150// printf( "Resizing data structures. Old size = %6d. New size = %6d.\n", p->nNodesMaxAlloc, p->nNodesCur );
151 reoResizeStructures( p, 0, p->nNodesCur, 0 );
152 }
153 }
154 }
155 // fix the plane index
156 if ( q == -1 )
157 q++;
158 // now p points to the position of this var in the order
159
160 // move down
161 for ( ; q < p->nSupp-1; )
162 {
163 CostCurrent -= reoReorderSwapAdjacentVars( p, q, 0 );
164 q++; // change q to point to the position of this var in the order
165 // sanity check: the number of nodes on the back pass should be the same
166 if ( p->pVarCosts[q] != REO_HIGH_VALUE && fabs( p->pVarCosts[q] - CostCurrent ) > REO_COST_EPSILON )
167 printf("reoReorderSift(): Error! On the backward move, the costs are different.\n");
168 p->pVarCosts[q] = CostCurrent;
169 // update the lower bound (assuming that for level q-1 it is set correctly)
170 p->pPlanes[q].statsCostAbove = p->pPlanes[q-1].statsCostAbove + p->pPlanes[q-1].statsCost;
171 // check the bounds only if the variable already reached its previous position
172 if ( q >= BestQ )
173 {
174 // check the upper bound
175 if ( CostCurrent >= CostLimit )
176 break;
177 // check the lower bound
178 if ( p->pPlanes[q].statsCostAbove + (REO_QUAL_PAR-1)*p->pPlanes[q].statsCostBelow/REO_QUAL_PAR >= CostBest )
179 break;
180 }
181 // update the best cost
182 if ( CostBest >= CostCurrent )
183 {
184 CostBest = CostCurrent;
185 BestQ = q;
186 // adjust node limit
187 CostLimit = ddMin( CostLimit, 1 + (int)(REO_REORDER_LIMIT * CostCurrent) );
188 }
189
190 // when we are reordering for width or APL, it may happen that
191 // the number of nodes has grown above certain limit,
192 // in which case we have to resize the data structures
193 if ( p->fMinWidth || p->fMinApl )
194 {
195 if ( p->nNodesCur >= 2 * p->nNodesMaxAlloc )
196 {
197// printf( "Resizing data structures. Old size = %6d. New size = %6d.\n", p->nNodesMaxAlloc, p->nNodesCur );
198 reoResizeStructures( p, 0, p->nNodesCur, 0 );
199 }
200 }
201 }
202 // move the variable up from the given position (q) to the best position (BestQ)
203 assert( q >= BestQ );
204 for ( ; q > BestQ; q-- )
205 {
206 CostCurrent -= reoReorderSwapAdjacentVars( p, q-1, 1 );
207 // sanity check: the number of nodes on the back pass should be the same
208 if ( fabs( p->pVarCosts[q-1] - CostCurrent ) > REO_COST_EPSILON )
209 {
210 printf("reoReorderSift(): Error! On the return move, the costs are different.\n" );
211 fflush(stdout);
212 }
213 }
214 }
215 else // move down first, then up
216 {
217 // set the current number of nodes on all levels above the given level
218 p->pPlanes[0].statsCostAbove = 0;
219 for ( v = 1; v <= VarCurrent; v++ )
220 p->pPlanes[v].statsCostAbove = p->pPlanes[v-1].statsCostAbove + p->pPlanes[v-1].statsCost;
221 // set the current number of nodes on all levels below the given level
222 p->pPlanes[p->nSupp].statsCostBelow = 0;
223 for ( v = p->nSupp - 1; v >= VarCurrent; v-- )
224 p->pPlanes[v].statsCostBelow = p->pPlanes[v+1].statsCostBelow + p->pPlanes[v+1].statsCost;
225
226 assert( CostCurrent == p->pPlanes[VarCurrent].statsCostAbove +
227 p->pPlanes[VarCurrent].statsCost +
228 p->pPlanes[VarCurrent].statsCostBelow );
229
230 // move down
231 for ( q = VarCurrent; q < p->nSupp-1; )
232 {
233 CostCurrent -= reoReorderSwapAdjacentVars( p, q, 0 );
234 q++; // change q to point to the position of this var in the order
235 p->pVarCosts[q] = CostCurrent;
236 // update the lower bound (assuming that for level q-1 it is set correctly)
237 p->pPlanes[q].statsCostAbove = p->pPlanes[q-1].statsCostAbove + p->pPlanes[q-1].statsCost;
238 // check the upper bound
239 if ( CostCurrent >= CostLimit )
240 break;
241 // check the lower bound
242 if ( p->pPlanes[q].statsCostAbove + (REO_QUAL_PAR-1)*p->pPlanes[q].statsCostBelow/REO_QUAL_PAR >= CostBest )
243 break;
244 // update the best cost
245 if ( CostBest > CostCurrent )
246 {
247 CostBest = CostCurrent;
248 BestQ = q;
249 // adjust node limit
250 CostLimit = ddMin( CostLimit, 1 + (int)(REO_REORDER_LIMIT * CostCurrent) );
251 }
252
253 // when we are reordering for width or APL, it may happen that
254 // the number of nodes has grown above certain limit,
255 // in which case we have to resize the data structures
256 if ( p->fMinWidth || p->fMinApl )
257 {
258 if ( p->nNodesCur >= 2 * p->nNodesMaxAlloc )
259 {
260// printf( "Resizing data structures. Old size = %6d. New size = %6d.\n", p->nNodesMaxAlloc, p->nNodesCur );
261 reoResizeStructures( p, 0, p->nNodesCur, 0 );
262 }
263 }
264 }
265
266 // move up
267 for ( --q; q >= 0; q-- )
268 {
269 CostCurrent -= reoReorderSwapAdjacentVars( p, q, 1 );
270 // now q points to the position of this var in the order
271 // sanity check: the number of nodes on the back pass should be the same
272 if ( p->pVarCosts[q] != REO_HIGH_VALUE && fabs( p->pVarCosts[q] - CostCurrent ) > REO_COST_EPSILON )
273 printf("reoReorderSift(): Error! On the backward move, the costs are different.\n");
274 p->pVarCosts[q] = CostCurrent;
275 // update the lower bound (assuming that for level q+1 it is set correctly)
276 p->pPlanes[q].statsCostBelow = p->pPlanes[q+1].statsCostBelow + p->pPlanes[q+1].statsCost;
277 // check the bounds only if the variable already reached its previous position
278 if ( q <= BestQ )
279 {
280 // check the upper bound
281 if ( CostCurrent >= CostLimit )
282 break;
283 // check the lower bound
284 if ( p->pPlanes[q].statsCostBelow + (REO_QUAL_PAR-1)*p->pPlanes[q].statsCostAbove/REO_QUAL_PAR >= CostBest )
285 break;
286 }
287 // update the best cost
288 if ( CostBest >= CostCurrent )
289 {
290 CostBest = CostCurrent;
291 BestQ = q;
292 // adjust node limit
293 CostLimit = ddMin( CostLimit, 1 + (int)(REO_REORDER_LIMIT * CostCurrent) );
294 }
295
296 // when we are reordering for width or APL, it may happen that
297 // the number of nodes has grown above certain limit,
298 // in which case we have to resize the data structures
299 if ( p->fMinWidth || p->fMinApl )
300 {
301 if ( p->nNodesCur >= 2 * p->nNodesMaxAlloc )
302 {
303// printf( "Resizing data structures. Old size = %6d. New size = %6d.\n", p->nNodesMaxAlloc, p->nNodesCur );
304 reoResizeStructures( p, 0, p->nNodesCur, 0 );
305 }
306 }
307 }
308 // fix the plane index
309 if ( q == -1 )
310 q++;
311 // now q points to the position of this var in the order
312 // move the variable down from the given position (q) to the best position (BestQ)
313 assert( q <= BestQ );
314 for ( ; q < BestQ; q++ )
315 {
316 CostCurrent -= reoReorderSwapAdjacentVars( p, q, 0 );
317 // sanity check: the number of nodes on the back pass should be the same
318 if ( fabs( p->pVarCosts[q+1] - CostCurrent ) > REO_COST_EPSILON )
319 {
320 printf("reoReorderSift(): Error! On the return move, the costs are different.\n" );
321 fflush(stdout);
322 }
323 }
324 }
325 assert( fabs( CostBest - CostCurrent ) < REO_COST_EPSILON );
326
327 // update the cost
328 if ( p->fMinWidth )
329 p->nWidthCur = (int)CostBest;
330 else if ( p->fMinApl )
331 p->nAplCur = CostCurrent;
332 else
333 p->nNodesCur = (int)CostBest;
334 }
335
336 // remove the sifted attributes if any
337 for ( v = 0; v < p->nSupp; v++ )
338 p->pPlanes[v].fSifted = 0;
339}
Cube * p
Definition exorList.c:222
void reoResizeStructures(reo_man *p, int nDdVarsMax, int nNodesMax, int nFuncs)
Definition reoCore.c:269
double reoReorderSwapAdjacentVars(reo_man *p, int Level, int fMovingUp)
FUNCTION DEFINITIONS ///.
Definition reoSwap.c:46
#define REO_REORDER_LIMIT
MACRO DEFINITIONS ///.
Definition reo.h:37
#define REO_QUAL_PAR
Definition reo.h:38
#define REO_COST_EPSILON
Definition reo.h:43
#define REO_HIGH_VALUE
Definition reo.h:44
#define assert(ex)
Definition util_old.h:213
Here is the call graph for this function:
Here is the caller graph for this function: