ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
reoSwap.c
Go to the documentation of this file.
1
18
19#include "reo.h"
20
21ABC_NAMESPACE_IMPL_START
22
23
27
28#define AddToLinkedList( ppList, pLink ) (((pLink)->Next = *(ppList)), (*(ppList) = (pLink)))
29
33
46double reoReorderSwapAdjacentVars( reo_man * p, int lev0, int fMovingUp )
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 = NULL, * pNew1T = NULL, * pNew2E = NULL, * pNew2T = NULL;
58 reo_unit * pNew1ER = NULL, * pNew2ER = NULL;
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
822finish:
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}
899
903
904ABC_NAMESPACE_IMPL_END
905
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition abc_namespaces.h:54
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition abc_namespaces.h:55
p
Cube * p
Definition exorList.c:222
hashKey3
#define hashKey3(a, b, c, TSIZE)
Definition extraBdd.h:89
AddToLinkedList
#define AddToLinkedList(ppList, pLink)
DECLARATIONS ///.
Definition reoSwap.c:28
reoReorderSwapAdjacentVars
double reoReorderSwapAdjacentVars(reo_man *p, int lev0, int fMovingUp)
FUNCTION DEFINITIONS ///.
Definition reoSwap.c:46
reo_man
struct _reo_man reo_man
Definition reo.h:63
reoProfileWidthVerifyLevel
void reoProfileWidthVerifyLevel(reo_plane *pPlane, int Level)
Definition reoProfile.c:354
Unit_Not
#define Unit_Not(u)
Definition reo.h:175
Unit_Regular
#define Unit_Regular(u)
Definition reo.h:174
reoUnitsRecycleUnit
void reoUnitsRecycleUnit(reo_man *p, reo_unit *pUnit)
Definition reoUnits.c:69
reoUnitsGetNextUnit
reo_unit * reoUnitsGetNextUnit(reo_man *p)
FUNCTION DEFINITIONS ///.
Definition reoUnits.c:45
reo_unit
struct _reo_unit reo_unit
DATA STRUCTURES ///.
Definition reo.h:60
_reo_unit::Next
reo_unit * Next
Definition reo.h:76
_reo_unit::lev
short lev
Definition reo.h:68
_reo_unit::Sign
int Sign
Definition reo.h:72
_reo_unit::Weight
double Weight
Definition reo.h:77
_reo_unit::n
short n
Definition reo.h:71
_reo_unit::TopRef
short TopRef
Definition reo.h:69
_reo_unit::pE
reo_unit * pE
Definition reo.h:74
_reo_unit::TopRefNew
short TopRefNew
Definition reo.h:70
_reo_unit::pT
reo_unit * pT
Definition reo.h:75
assert
#define assert(ex)
Definition util_old.h:213