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

Go to the source code of this file.

Macros

#define AddToLinkedList(ppList, pLink)   (((pLink)->Next = *(ppList)), (*(ppList) = (pLink)))
 DECLARATIONS ///. More...
 

Functions

double reoReorderSwapAdjacentVars (reo_man *p, int lev0, int fMovingUp)
 FUNCTION DEFINITIONS ///. More...
 

Macro Definition Documentation

#define AddToLinkedList (   ppList,
  pLink 
)    (((pLink)->Next = *(ppList)), (*(ppList) = (pLink)))

DECLARATIONS ///.

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

FileName [reoSwap.c]

PackageName [REO: A specialized DD reordering engine.]

Synopsis [Implementation of the two-variable swap.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

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

]

Definition at line 28 of file reoSwap.c.

Function Documentation

double reoReorderSwapAdjacentVars ( reo_man *  p,
int  lev0,
int  fMovingUp 
)

FUNCTION DEFINITIONS ///.

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

Synopsis []

Description [Takes the level (lev0) of the plane, which should be swapped with the next plane. Returns the gain using the current cost function.]

SideEffects []

SeeAlso []

Definition at line 46 of file reoSwap.c.

47 {
48  // the levels in the decision diagram
49  int lev1 = lev0 + 1, lev2 = lev0 + 2;
50  // the new nodes on lev0
51  reo_unit * pLoop, * pUnit;
52  // the new nodes on lev1
53  reo_unit * pNewPlane20 = NULL, * pNewPlane21 = NULL; // Suppress "might be used uninitialized"
54  reo_unit * pNewPlane20R;
55  reo_unit * pUnitE, * pUnitER, * pUnitT;
56  // the nodes below lev1
57  reo_unit * pNew1E, * pNew1T, * pNew2E, * pNew2T;
58  reo_unit * pNew1ER, * pNew2ER;
59  // the old linked lists
60  reo_unit * pListOld0 = p->pPlanes[lev0].pHead;
61  reo_unit * pListOld1 = p->pPlanes[lev1].pHead;
62  // working planes and one more temporary plane
63  reo_unit * pListNew0 = NULL, ** ppListNew0 = &pListNew0;
64  reo_unit * pListNew1 = NULL, ** ppListNew1 = &pListNew1;
65  reo_unit * pListTemp = NULL, ** ppListTemp = &pListTemp;
66  // various integer variables
67  int fComp, fCompT, fFound, HKey, fInteract, temp, c;
68  int nWidthCofs = -1; // Suppress "might be used uninitialized"
69  // statistical variables
70  int nNodesUpMovedDown = 0;
71  int nNodesDownMovedUp = 0;
72  int nNodesUnrefRemoved = 0;
73  int nNodesUnrefAdded = 0;
74  int nWidthReduction = 0;
75  double AplWeightTotalLev0 = 0.0; // Suppress "might be used uninitialized"
76  double AplWeightTotalLev1 = 0.0; // Suppress "might be used uninitialized"
77  double AplWeightHalf = 0.0; // Suppress "might be used uninitialized"
78  double AplWeightPrev = 0.0; // Suppress "might be used uninitialized"
79  double AplWeightAfter = 0.0; // Suppress "might be used uninitialized"
80  double nCostGain;
81 
82  // set the old lists
83  assert( lev0 >= 0 && lev1 < p->nSupp );
84  pListOld0 = p->pPlanes[lev0].pHead;
85  pListOld1 = p->pPlanes[lev1].pHead;
86 
87  // make sure the planes have nodes
88  assert( p->pPlanes[lev0].statsNodes && p->pPlanes[lev1].statsNodes );
89  assert( pListOld0 && pListOld1 );
90 
91  if ( p->fMinWidth )
92  {
93  // verify that the width parameters are set correctly
94  reoProfileWidthVerifyLevel( p->pPlanes + lev0, lev0 );
95  reoProfileWidthVerifyLevel( p->pPlanes + lev1, lev1 );
96  // start the storage for cofactors
97  nWidthCofs = 0;
98  }
99  else if ( p->fMinApl )
100  {
101  AplWeightPrev = p->nAplCur;
102  AplWeightAfter = p->nAplCur;
103  AplWeightTotalLev0 = 0.0;
104  AplWeightTotalLev1 = 0.0;
105  }
106 
107  // check if the planes interact
108  fInteract = 0; // assume that they do not interact
109  for ( pUnit = pListOld0; pUnit; pUnit = pUnit->Next )
110  {
111  if ( pUnit->pT->lev == lev1 || Unit_Regular(pUnit->pE)->lev == lev1 )
112  {
113  fInteract = 1;
114  break;
115  }
116  // change the level now, this is done for efficiency reasons
117  pUnit->lev = lev1;
118  }
119 
120  // set the new signature for hashing
121  p->nSwaps++;
122  if ( !fInteract )
123 // if ( 0 )
124  {
125  // perform the swap without interaction
126  p->nNISwaps++;
127 
128  // change the levels
129  if ( p->fMinWidth )
130  {
131  // go through the current lower level, which will become upper
132  for ( pUnit = pListOld1; pUnit; pUnit = pUnit->Next )
133  {
134  pUnit->lev = lev0;
135 
136  pUnitER = Unit_Regular(pUnit->pE);
137  if ( pUnitER->TopRef > lev0 )
138  {
139  if ( pUnitER->Sign != p->nSwaps )
140  {
141  if ( pUnitER->TopRef == lev2 )
142  {
143  pUnitER->TopRef = lev1;
144  nWidthReduction--;
145  }
146  else
147  {
148  assert( pUnitER->TopRef == lev1 );
149  }
150  pUnitER->Sign = p->nSwaps;
151  }
152  }
153 
154  pUnitT = pUnit->pT;
155  if ( pUnitT->TopRef > lev0 )
156  {
157  if ( pUnitT->Sign != p->nSwaps )
158  {
159  if ( pUnitT->TopRef == lev2 )
160  {
161  pUnitT->TopRef = lev1;
162  nWidthReduction--;
163  }
164  else
165  {
166  assert( pUnitT->TopRef == lev1 );
167  }
168  pUnitT->Sign = p->nSwaps;
169  }
170  }
171 
172  }
173 
174  // go through the current upper level, which will become lower
175  for ( pUnit = pListOld0; pUnit; pUnit = pUnit->Next )
176  {
177  pUnit->lev = lev1;
178 
179  pUnitER = Unit_Regular(pUnit->pE);
180  if ( pUnitER->TopRef > lev0 )
181  {
182  if ( pUnitER->Sign != p->nSwaps )
183  {
184  assert( pUnitER->TopRef == lev1 );
185  pUnitER->TopRef = lev2;
186  pUnitER->Sign = p->nSwaps;
187  nWidthReduction++;
188  }
189  }
190 
191  pUnitT = pUnit->pT;
192  if ( pUnitT->TopRef > lev0 )
193  {
194  if ( pUnitT->Sign != p->nSwaps )
195  {
196  assert( pUnitT->TopRef == lev1 );
197  pUnitT->TopRef = lev2;
198  pUnitT->Sign = p->nSwaps;
199  nWidthReduction++;
200  }
201  }
202  }
203  }
204  else
205  {
206 // for ( pUnit = pListOld0; pUnit; pUnit = pUnit->Next )
207 // pUnit->lev = lev1;
208  for ( pUnit = pListOld1; pUnit; pUnit = pUnit->Next )
209  pUnit->lev = lev0;
210  }
211 
212  // set the new linked lists, which will be attached to the planes
213  pListNew0 = pListOld1;
214  pListNew1 = pListOld0;
215 
216  if ( p->fMinApl )
217  {
218  AplWeightTotalLev0 = p->pPlanes[lev1].statsCost;
219  AplWeightTotalLev1 = p->pPlanes[lev0].statsCost;
220  }
221 
222  // set the changes in terms of nodes
223  nNodesUpMovedDown = p->pPlanes[lev0].statsNodes;
224  nNodesDownMovedUp = p->pPlanes[lev1].statsNodes;
225  goto finish;
226  }
227  p->Signature++;
228 
229 
230  // two-variable swap is done in three easy steps
231  // previously I thought that steps (1) and (2) can be merged into one step
232  // now it is clear that this cannot be done without changing a lot of other stuff...
233 
234  // (1) walk through the upper level, find units without cofactors in the lower level
235  // and move them to the new lower level (while adding to the cache)
236  // (2) walk through the uppoer level, and tranform all the remaning nodes
237  // while employing cache for the new lower level
238  // (3) walk through the old lower level, find those nodes whose ref counters are not zero,
239  // and move them to the new uppoer level, free other nodes
240 
241  // (1) walk through the upper level, find units without cofactors in the lower level
242  // and move them to the new lower level (while adding to the cache)
243  for ( pLoop = pListOld0; pLoop; )
244  {
245  pUnit = pLoop;
246  pLoop = pLoop->Next;
247 
248  pUnitE = pUnit->pE;
249  pUnitER = Unit_Regular(pUnitE);
250  pUnitT = pUnit->pT;
251 
252  if ( pUnitER->lev != lev1 && pUnitT->lev != lev1 )
253  {
254  // before after
255  //
256  // <p1> .
257  // 0 / \ 1 .
258  // / \ .
259  // / \ .
260  // / \ <p2n> .
261  // / \ 0 / \ 1 .
262  // / \ / \ .
263  // / \ / \ .
264  // F0 F1 F0 F1
265 
266  // move to plane-2-new
267  // nothing changes in the process (cofactors, ref counter, APL weight)
268  pUnit->lev = lev1;
269  AddToLinkedList( ppListNew1, pUnit );
270  if ( p->fMinApl )
271  AplWeightTotalLev1 += pUnit->Weight;
272 
273  // add to cache - find the cell with different signature (not the current one!)
274  for ( HKey = hashKey3(p->Signature, pUnitE, pUnitT, p->nTableSize);
275  p->HTable[HKey].Sign == p->Signature;
276  HKey = (HKey+1) % p->nTableSize );
277  assert( p->HTable[HKey].Sign != p->Signature );
278  p->HTable[HKey].Sign = p->Signature;
279  p->HTable[HKey].Arg1 = pUnitE;
280  p->HTable[HKey].Arg2 = pUnitT;
281  p->HTable[HKey].Arg3 = pUnit;
282 
283  nNodesUpMovedDown++;
284 
285  if ( p->fMinWidth )
286  {
287  // update the cofactors's top ref
288  if ( pUnitER->TopRef > lev0 ) // the cofactor's top ref level is one of the current two levels
289  {
290  assert( pUnitER->TopRef == lev1 );
291  pUnitER->TopRefNew = lev2;
292  if ( pUnitER->Sign != p->nSwaps )
293  {
294  pUnitER->Sign = p->nSwaps; // set the current signature
295  p->pWidthCofs[ nWidthCofs++ ] = pUnitER;
296  }
297  }
298  if ( pUnitT->TopRef > lev0 ) // the cofactor's top ref level is one of the current two levels
299  {
300  assert( pUnitT->TopRef == lev1 );
301  pUnitT->TopRefNew = lev2;
302  if ( pUnitT->Sign != p->nSwaps )
303  {
304  pUnitT->Sign = p->nSwaps; // set the current signature
305  p->pWidthCofs[ nWidthCofs++ ] = pUnitT;
306  }
307  }
308  }
309  }
310  else
311  {
312  // add to the temporary plane
313  AddToLinkedList( ppListTemp, pUnit );
314  }
315  }
316 
317 
318  // (2) walk through the uppoer level, and tranform all the remaning nodes
319  // while employing cache for the new lower level
320  for ( pLoop = pListTemp; pLoop; )
321  {
322  pUnit = pLoop;
323  pLoop = pLoop->Next;
324 
325  pUnitE = pUnit->pE;
326  pUnitER = Unit_Regular(pUnitE);
327  pUnitT = pUnit->pT;
328  fComp = (int)(pUnitER != pUnitE);
329 
330  // count the amount of weight to reduce the APL of the children of this node
331  if ( p->fMinApl )
332  AplWeightHalf = 0.5 * pUnit->Weight;
333 
334  // determine what situation is this
335  if ( pUnitER->lev == lev1 && pUnitT->lev == lev1 )
336  {
337  if ( fComp == 0 )
338  {
339  // before after
340  //
341  // <p1> <p1n> .
342  // 0 / \ 1 0 / \ 1 .
343  // / \ / \ .
344  // / \ / \ .
345  // <p2> <p2> <p2n> <p2n> .
346  // 0 / \ 1 0 / \ 1 0 / \ 1 0 / \ 1 .
347  // / \ / \ / \ / \ .
348  // / \ / \ / \ / \ .
349  // F0 F1 F2 F3 F0 F2 F1 F3 .
350  // pNew1E pNew1T pNew2E pNew2T
351  //
352  pNew1E = pUnitE->pE; // F0
353  pNew1T = pUnitT->pE; // F2
354 
355  pNew2E = pUnitE->pT; // F1
356  pNew2T = pUnitT->pT; // F3
357  }
358  else
359  {
360  // before after
361  //
362  // <p1> <p1n> .
363  // 0 . \ 1 0 / \ 1 .
364  // . \ / \ .
365  // . \ / \ .
366  // <p2> <p2> <p2n> <p2n> .
367  // 0 / \ 1 0 / \ 1 0 . \ 1 0 . \ 1 .
368  // / \ / \ . \ . \ .
369  // / \ / \ . \ . \ .
370  // F0 F1 F2 F3 F0 F2 F1 F3 .
371  // pNew1E pNew1T pNew2E pNew2T
372  //
373  pNew1E = Unit_Not(pUnitER->pE); // F0
374  pNew1T = pUnitT->pE; // F2
375 
376  pNew2E = Unit_Not(pUnitER->pT); // F1
377  pNew2T = pUnitT->pT; // F3
378  }
379  // subtract ref counters - on the level P2
380  pUnitER->n--;
381  pUnitT->n--;
382 
383  // mark the change in the APL weights
384  if ( p->fMinApl )
385  {
386  pUnitER->Weight -= AplWeightHalf;
387  pUnitT->Weight -= AplWeightHalf;
388  AplWeightAfter -= pUnit->Weight;
389  }
390  }
391  else if ( pUnitER->lev == lev1 )
392  {
393  if ( fComp == 0 )
394  {
395  // before after
396  //
397  // <p1> <p1n> .
398  // 0 / \ 1 0 / \ 1 .
399  // / \ / \ .
400  // / \ / \ .
401  // <p2> \ <p2n> <p2n> .
402  // 0 / \ 1 \ 0 / \ 1 0 / \ 1 .
403  // / \ \ / \ / \ .
404  // / \ \ / \ / \ .
405  // F0 F1 F3 F0 F3 F1 F3 .
406  // pNew1E pNew1T pNew2E pNew2T
407  //
408  pNew1E = pUnitER->pE; // F0
409  pNew1T = pUnitT; // F3
410 
411  pNew2E = pUnitER->pT; // F1
412  pNew2T = pUnitT; // F3
413  }
414  else
415  {
416  // before after
417  //
418  // <p1> <p1n> .
419  // 0 . \ 1 0 / \ 1 .
420  // . \ / \ .
421  // . \ / \ .
422  // <p2> \ <p2n> <p2n> .
423  // 0 / \ 1 \ 0 . \ 1 0 . \ 1 .
424  // / \ \ . \ . \ .
425  // / \ \ . \ . \ .
426  // F0 F1 F3 F0 F3 F1 F3 .
427  // pNew1E pNew1T pNew2E pNew2T
428  //
429  pNew1E = Unit_Not(pUnitER->pE); // F0
430  pNew1T = pUnitT; // F3
431 
432  pNew2E = Unit_Not(pUnitER->pT); // F1
433  pNew2T = pUnitT; // F3
434  }
435  // subtract ref counter - on the level P2
436  pUnitER->n--;
437  // subtract ref counter - on other levels
438  pUnitT->n--; ///
439 
440  // mark the change in the APL weights
441  if ( p->fMinApl )
442  {
443  pUnitER->Weight -= AplWeightHalf;
444  AplWeightAfter -= AplWeightHalf;
445  }
446  }
447  else if ( pUnitT->lev == lev1 )
448  {
449  // before after
450  //
451  // <p1> <p1n> .
452  // 0 / \ 1 0 / \ 1 .
453  // / \ / \ .
454  // / \ / \ .
455  // / <p2> <p2n> <p2n> .
456  // / 0 / \ 1 0 / \ 1 0 / \ 1 .
457  // / / \ / \ / \ .
458  // / / \ / \ / \ .
459  // F0 F2 F3 F0 F2 F0 F3 .
460  // pNew1E pNew1T pNew2E pNew2T
461  //
462  pNew1E = pUnitE; // F0
463  pNew1T = pUnitT->pE; // F2
464 
465  pNew2E = pUnitE; // F0
466  pNew2T = pUnitT->pT; // F3
467 
468  // subtract incoming edge counter - on the level P2
469  pUnitT->n--;
470  // subtract ref counter - on other levels
471  pUnitER->n--; ///
472 
473  // mark the change in the APL weights
474  if ( p->fMinApl )
475  {
476  pUnitT->Weight -= AplWeightHalf;
477  AplWeightAfter -= AplWeightHalf;
478  }
479  }
480  else
481  {
482  assert( 0 ); // should never happen
483  }
484 
485 
486  // consider all the cases except the last one
487  if ( pNew1E == pNew1T )
488  {
489  pNewPlane20 = pNew1T;
490 
491  if ( p->fMinWidth )
492  {
493  // update the cofactors's top ref
494  if ( pNew1T->TopRef > lev0 ) // the cofactor's top ref level is one of the current two levels
495  {
496  pNew1T->TopRefNew = lev1;
497  if ( pNew1T->Sign != p->nSwaps )
498  {
499  pNew1T->Sign = p->nSwaps; // set the current signature
500  p->pWidthCofs[ nWidthCofs++ ] = pNew1T;
501  }
502  }
503  }
504  }
505  else
506  {
507  // pNew1T can be complemented
508  fCompT = Cudd_IsComplement(pNew1T);
509  if ( fCompT )
510  {
511  pNew1E = Unit_Not(pNew1E);
512  pNew1T = Unit_Not(pNew1T);
513  }
514 
515  // check the hash-table
516  fFound = 0;
517  for ( HKey = hashKey3(p->Signature, pNew1E, pNew1T, p->nTableSize);
518  p->HTable[HKey].Sign == p->Signature;
519  HKey = (HKey+1) % p->nTableSize )
520  if ( p->HTable[HKey].Arg1 == pNew1E && p->HTable[HKey].Arg2 == pNew1T )
521  { // the entry is present
522  // assign this entry
523  pNewPlane20 = p->HTable[HKey].Arg3;
524  assert( pNewPlane20->lev == lev1 );
525  fFound = 1;
526  p->HashSuccess++;
527  break;
528  }
529 
530  if ( !fFound )
531  { // create the new entry
532  pNewPlane20 = reoUnitsGetNextUnit( p ); // increments the unit counter
533  pNewPlane20->pE = pNew1E;
534  pNewPlane20->pT = pNew1T;
535  pNewPlane20->n = 0; // ref will be added later
536  pNewPlane20->lev = lev1;
537  if ( p->fMinWidth )
538  {
539  pNewPlane20->TopRef = lev1;
540  pNewPlane20->Sign = 0;
541  }
542  // set the weight of this node
543  if ( p->fMinApl )
544  pNewPlane20->Weight = 0.0;
545 
546  // increment ref counters of children
547  pNew1ER = Unit_Regular(pNew1E);
548  pNew1ER->n++; //
549  pNew1T->n++; //
550 
551  // insert into the data structure
552  AddToLinkedList( ppListNew1, pNewPlane20 );
553 
554  // add this entry to cache
555  assert( p->HTable[HKey].Sign != p->Signature );
556  p->HTable[HKey].Sign = p->Signature;
557  p->HTable[HKey].Arg1 = pNew1E;
558  p->HTable[HKey].Arg2 = pNew1T;
559  p->HTable[HKey].Arg3 = pNewPlane20;
560 
561  nNodesUnrefAdded++;
562 
563  if ( p->fMinWidth )
564  {
565  // update the cofactors's top ref
566  if ( pNew1ER->TopRef > lev0 ) // the cofactor's top ref level is one of the current two levels
567  {
568  if ( pNew1ER->Sign != p->nSwaps )
569  {
570  pNew1ER->TopRefNew = lev2;
571  if ( pNew1ER->Sign != p->nSwaps )
572  {
573  pNew1ER->Sign = p->nSwaps; // set the current signature
574  p->pWidthCofs[ nWidthCofs++ ] = pNew1ER;
575  }
576  }
577  // otherwise the level is already set correctly
578  else
579  {
580  assert( pNew1ER->TopRefNew == lev1 || pNew1ER->TopRefNew == lev2 );
581  }
582  }
583  // update the cofactors's top ref
584  if ( pNew1T->TopRef > lev0 ) // the cofactor's top ref level is one of the current two levels
585  {
586  if ( pNew1T->Sign != p->nSwaps )
587  {
588  pNew1T->TopRefNew = lev2;
589  if ( pNew1T->Sign != p->nSwaps )
590  {
591  pNew1T->Sign = p->nSwaps; // set the current signature
592  p->pWidthCofs[ nWidthCofs++ ] = pNew1T;
593  }
594  }
595  // otherwise the level is already set correctly
596  else
597  {
598  assert( pNew1T->TopRefNew == lev1 || pNew1T->TopRefNew == lev2 );
599  }
600  }
601  }
602  }
603 
604  if ( p->fMinApl )
605  {
606  // increment the weight of this node
607  pNewPlane20->Weight += AplWeightHalf;
608  // mark the change in the APL weight
609  AplWeightAfter += AplWeightHalf;
610  // update the total weight of this level
611  AplWeightTotalLev1 += AplWeightHalf;
612  }
613 
614  if ( fCompT )
615  pNewPlane20 = Unit_Not(pNewPlane20);
616  }
617 
618  if ( pNew2E == pNew2T )
619  {
620  pNewPlane21 = pNew2T;
621 
622  if ( p->fMinWidth )
623  {
624  // update the cofactors's top ref
625  if ( pNew2T->TopRef > lev0 ) // the cofactor's top ref level is one of the current two levels
626  {
627  pNew2T->TopRefNew = lev1;
628  if ( pNew2T->Sign != p->nSwaps )
629  {
630  pNew2T->Sign = p->nSwaps; // set the current signature
631  p->pWidthCofs[ nWidthCofs++ ] = pNew2T;
632  }
633  }
634  }
635  }
636  else
637  {
638  assert( !Cudd_IsComplement(pNew2T) );
639 
640  // check the hash-table
641  fFound = 0;
642  for ( HKey = hashKey3(p->Signature, pNew2E, pNew2T, p->nTableSize);
643  p->HTable[HKey].Sign == p->Signature;
644  HKey = (HKey+1) % p->nTableSize )
645  if ( p->HTable[HKey].Arg1 == pNew2E && p->HTable[HKey].Arg2 == pNew2T )
646  { // the entry is present
647  // assign this entry
648  pNewPlane21 = p->HTable[HKey].Arg3;
649  assert( pNewPlane21->lev == lev1 );
650  fFound = 1;
651  p->HashSuccess++;
652  break;
653  }
654 
655  if ( !fFound )
656  { // create the new entry
657  pNewPlane21 = reoUnitsGetNextUnit( p ); // increments the unit counter
658  pNewPlane21->pE = pNew2E;
659  pNewPlane21->pT = pNew2T;
660  pNewPlane21->n = 0; // ref will be added later
661  pNewPlane21->lev = lev1;
662  if ( p->fMinWidth )
663  {
664  pNewPlane21->TopRef = lev1;
665  pNewPlane21->Sign = 0;
666  }
667  // set the weight of this node
668  if ( p->fMinApl )
669  pNewPlane21->Weight = 0.0;
670 
671  // increment ref counters of children
672  pNew2ER = Unit_Regular(pNew2E);
673  pNew2ER->n++; //
674  pNew2T->n++; //
675 
676  // insert into the data structure
677 // reoUnitsAddUnitToPlane( &P2new, pNewPlane21 );
678  AddToLinkedList( ppListNew1, pNewPlane21 );
679 
680  // add this entry to cache
681  assert( p->HTable[HKey].Sign != p->Signature );
682  p->HTable[HKey].Sign = p->Signature;
683  p->HTable[HKey].Arg1 = pNew2E;
684  p->HTable[HKey].Arg2 = pNew2T;
685  p->HTable[HKey].Arg3 = pNewPlane21;
686 
687  nNodesUnrefAdded++;
688 
689 
690  if ( p->fMinWidth )
691  {
692  // update the cofactors's top ref
693  if ( pNew2ER->TopRef > lev0 ) // the cofactor's top ref level is one of the current two levels
694  {
695  if ( pNew2ER->Sign != p->nSwaps )
696  {
697  pNew2ER->TopRefNew = lev2;
698  if ( pNew2ER->Sign != p->nSwaps )
699  {
700  pNew2ER->Sign = p->nSwaps; // set the current signature
701  p->pWidthCofs[ nWidthCofs++ ] = pNew2ER;
702  }
703  }
704  // otherwise the level is already set correctly
705  else
706  {
707  assert( pNew2ER->TopRefNew == lev1 || pNew2ER->TopRefNew == lev2 );
708  }
709  }
710  // update the cofactors's top ref
711  if ( pNew2T->TopRef > lev0 ) // the cofactor's top ref level is one of the current two levels
712  {
713  if ( pNew2T->Sign != p->nSwaps )
714  {
715  pNew2T->TopRefNew = lev2;
716  if ( pNew2T->Sign != p->nSwaps )
717  {
718  pNew2T->Sign = p->nSwaps; // set the current signature
719  p->pWidthCofs[ nWidthCofs++ ] = pNew2T;
720  }
721  }
722  // otherwise the level is already set correctly
723  else
724  {
725  assert( pNew2T->TopRefNew == lev1 || pNew2T->TopRefNew == lev2 );
726  }
727  }
728  }
729  }
730 
731  if ( p->fMinApl )
732  {
733  // increment the weight of this node
734  pNewPlane21->Weight += AplWeightHalf;
735  // mark the change in the APL weight
736  AplWeightAfter += AplWeightHalf;
737  // update the total weight of this level
738  AplWeightTotalLev1 += AplWeightHalf;
739  }
740  }
741  // in all cases, the node will be added to the plane-1
742  // this should be the same node (pUnit) as was originally there
743  // because it is referenced by the above nodes
744 
745  assert( !Cudd_IsComplement(pNewPlane21) );
746  // should be the case; otherwise reordering is not a local operation
747 
748  pUnit->pE = pNewPlane20;
749  pUnit->pT = pNewPlane21;
750  assert( pUnit->lev == lev0 );
751  // reference counter remains the same; the APL weight remains the same
752 
753  // increment ref counters of children
754  pNewPlane20R = Unit_Regular(pNewPlane20);
755  pNewPlane20R->n++; ///
756  pNewPlane21->n++; ///
757 
758  // insert into the data structure
759  AddToLinkedList( ppListNew0, pUnit );
760  if ( p->fMinApl )
761  AplWeightTotalLev0 += pUnit->Weight;
762  }
763 
764  // (3) walk through the old lower level, find those nodes whose ref counters are not zero,
765  // and move them to the new uppoer level, free other nodes
766  for ( pLoop = pListOld1; pLoop; )
767  {
768  pUnit = pLoop;
769  pLoop = pLoop->Next;
770  if ( pUnit->n )
771  {
772  assert( !p->fMinApl || pUnit->Weight > 0.0 );
773  // the node should be added to the new level
774  // no need to check the hash table
775  pUnit->lev = lev0;
776  AddToLinkedList( ppListNew0, pUnit );
777  if ( p->fMinApl )
778  AplWeightTotalLev0 += pUnit->Weight;
779 
780  nNodesDownMovedUp++;
781 
782  if ( p->fMinWidth )
783  {
784  pUnitER = Unit_Regular(pUnit->pE);
785  pUnitT = pUnit->pT;
786 
787  // update the cofactors's top ref
788  if ( pUnitER->TopRef > lev0 ) // the cofactor's top ref level is one of the current two levels
789  {
790  pUnitER->TopRefNew = lev1;
791  if ( pUnitER->Sign != p->nSwaps )
792  {
793  pUnitER->Sign = p->nSwaps; // set the current signature
794  p->pWidthCofs[ nWidthCofs++ ] = pUnitER;
795  }
796  }
797  if ( pUnitT->TopRef > lev0 ) // the cofactor's top ref level is one of the current two levels
798  {
799  pUnitT->TopRefNew = lev1;
800  if ( pUnitT->Sign != p->nSwaps )
801  {
802  pUnitT->Sign = p->nSwaps; // set the current signature
803  p->pWidthCofs[ nWidthCofs++ ] = pUnitT;
804  }
805  }
806  }
807  }
808  else
809  {
810  assert( !p->fMinApl || pUnit->Weight == 0.0 );
811  // decrement reference counters of children
812  pUnitER = Unit_Regular(pUnit->pE);
813  pUnitT = pUnit->pT;
814  pUnitER->n--; ///
815  pUnitT->n--; ///
816  // the node should be thrown away
817  reoUnitsRecycleUnit( p, pUnit );
818  nNodesUnrefRemoved++;
819  }
820  }
821 
822 finish:
823 
824  // attach the new levels to the planes
825  p->pPlanes[lev0].pHead = pListNew0;
826  p->pPlanes[lev1].pHead = pListNew1;
827 
828  // swap the sift status
829  temp = p->pPlanes[lev0].fSifted;
830  p->pPlanes[lev0].fSifted = p->pPlanes[lev1].fSifted;
831  p->pPlanes[lev1].fSifted = temp;
832 
833  // swap variables in the variable map
834  if ( p->pOrderInt )
835  {
836  temp = p->pOrderInt[lev0];
837  p->pOrderInt[lev0] = p->pOrderInt[lev1];
838  p->pOrderInt[lev1] = temp;
839  }
840 
841  // adjust the node profile
842  p->pPlanes[lev0].statsNodes -= (nNodesUpMovedDown - nNodesDownMovedUp);
843  p->pPlanes[lev1].statsNodes -= (nNodesDownMovedUp - nNodesUpMovedDown) + nNodesUnrefRemoved - nNodesUnrefAdded;
844  p->nNodesCur -= nNodesUnrefRemoved - nNodesUnrefAdded;
845 
846  // adjust the node profile on this level
847  if ( p->fMinWidth )
848  {
849  for ( c = 0; c < nWidthCofs; c++ )
850  {
851  if ( p->pWidthCofs[c]->TopRefNew < p->pWidthCofs[c]->TopRef )
852  {
853  p->pWidthCofs[c]->TopRef = p->pWidthCofs[c]->TopRefNew;
854  nWidthReduction--;
855  }
856  else if ( p->pWidthCofs[c]->TopRefNew > p->pWidthCofs[c]->TopRef )
857  {
858  p->pWidthCofs[c]->TopRef = p->pWidthCofs[c]->TopRefNew;
859  nWidthReduction++;
860  }
861  }
862  // verify that the profile is okay
863  reoProfileWidthVerifyLevel( p->pPlanes + lev0, lev0 );
864  reoProfileWidthVerifyLevel( p->pPlanes + lev1, lev1 );
865 
866  // compute the total gain in terms of width
867  nCostGain = (nNodesDownMovedUp - nNodesUpMovedDown + nNodesUnrefRemoved - nNodesUnrefAdded) + nWidthReduction;
868  // adjust the width on this level
869  p->pPlanes[lev1].statsWidth -= (int)nCostGain;
870  // set the cost
871  p->pPlanes[lev1].statsCost = p->pPlanes[lev1].statsWidth;
872  }
873  else if ( p->fMinApl )
874  {
875  // compute the total gain in terms of APL
876  nCostGain = AplWeightPrev - AplWeightAfter;
877  // make sure that the ALP is updated correctly
878 // assert( p->pPlanes[lev0].statsCost + p->pPlanes[lev1].statsCost - nCostGain ==
879 // AplWeightTotalLev0 + AplWeightTotalLev1 );
880  // adjust the profile
881  p->pPlanes[lev0].statsApl = AplWeightTotalLev0;
882  p->pPlanes[lev1].statsApl = AplWeightTotalLev1;
883  // set the cost
884  p->pPlanes[lev0].statsCost = p->pPlanes[lev0].statsApl;
885  p->pPlanes[lev1].statsCost = p->pPlanes[lev1].statsApl;
886  }
887  else
888  {
889  // compute the total gain in terms of the number of nodes
890  nCostGain = nNodesUnrefRemoved - nNodesUnrefAdded;
891  // adjust the profile (adjusted above)
892  // set the cost
893  p->pPlanes[lev0].statsCost = p->pPlanes[lev0].statsNodes;
894  p->pPlanes[lev1].statsCost = p->pPlanes[lev1].statsNodes;
895  }
896 
897  return nCostGain;
898 }
_reo_man::fMinApl
int fMinApl
Definition: reo.h:105
AddToLinkedList
#define AddToLinkedList(ppList, pLink)
DECLARATIONS ///.
Definition: reoSwap.c:28
_reo_unit::lev
short lev
Definition: reo.h:68
_reo_hash::Sign
int Sign
Definition: reo.h:95
_reo_unit::Weight
double Weight
Definition: reo.h:77
_reo_man::pWidthCofs
reo_unit ** pWidthCofs
Definition: reo.h:123
_reo_man::nAplCur
double nAplCur
Definition: reo.h:132
reoUnitsGetNextUnit
reo_unit * reoUnitsGetNextUnit(reo_man *p)
FUNCTION DEFINITIONS ///.
Definition: reoUnits.c:45
_reo_man::Signature
int Signature
Definition: reo.h:151
_reo_man::nNodesCur
int nNodesCur
Definition: reo.h:127
_reo_hash::Arg2
reo_unit * Arg2
Definition: reo.h:97
_reo_plane::statsWidth
int statsWidth
Definition: reo.h:84
_reo_man::nNISwaps
int nNISwaps
Definition: reo.h:170
hashKey3
#define hashKey3(a, b, c, TSIZE)
Definition: extraBdd.h:89
Cudd_IsComplement
#define Cudd_IsComplement(node)
Definition: cudd.h:425
reoProfileWidthVerifyLevel
void reoProfileWidthVerifyLevel(reo_plane *pPlane, int Level)
Definition: reoProfile.c:354
_reo_unit::pT
reo_unit * pT
Definition: reo.h:75
_reo_man::fMinWidth
int fMinWidth
Definition: reo.h:104
_reo_unit::Next
reo_unit * Next
Definition: reo.h:76
_reo_unit::TopRef
short TopRef
Definition: reo.h:69
_reo_unit::n
short n
Definition: reo.h:71
_reo_unit::pE
reo_unit * pE
Definition: reo.h:74
_reo_man::HTable
reo_hash * HTable
Definition: reo.h:149
_reo_man::nTableSize
int nTableSize
Definition: reo.h:150
_reo_unit::TopRefNew
short TopRefNew
Definition: reo.h:70
_reo_plane::statsCost
double statsCost
Definition: reo.h:86
_reo_plane::statsApl
double statsApl
Definition: reo.h:85
Unit_Regular
#define Unit_Regular(u)
Definition: reo.h:174
_reo_unit::Sign
int Sign
Definition: reo.h:72
_reo_man::pPlanes
reo_plane * pPlanes
Definition: reo.h:142
Unit_Not
#define Unit_Not(u)
Definition: reo.h:175
_reo_man::nSwaps
int nSwaps
Definition: reo.h:169
_reo_hash::Arg3
reo_unit * Arg3
Definition: reo.h:98
reoUnitsRecycleUnit
void reoUnitsRecycleUnit(reo_man *p, reo_unit *pUnit)
Definition: reoUnits.c:69
_reo_hash::Arg1
reo_unit * Arg1
Definition: reo.h:96
_reo_unit
Definition: reo.h:66
assert
#define assert(ex)
Definition: util_old.h:213
_reo_man::HashSuccess
int HashSuccess
Definition: reo.h:167
_reo_plane::statsNodes
int statsNodes
Definition: reo.h:83
_reo_plane::pHead
reo_unit * pHead
Definition: reo.h:90
_reo_man::pOrderInt
int * pOrderInt
Definition: reo.h:120
_reo_plane::fSifted
int fSifted
Definition: reo.h:82