src/bdd/reo/reoSwap.c File Reference
#include "reo.h"
Include dependency graph for reoSwap.c:
Go to the source code of this file.
Defines | |
| #define | AddToLinkedList(ppList, pLink) (((pLink)->Next = *(ppList)), (*(ppList) = (pLink))) |
Functions | |
| double | reoReorderSwapAdjacentVars (reo_man *p, int lev0, int fMovingUp) |
Define Documentation
| #define AddToLinkedList | ( | ppList, | |||
| pLink | ) | (((pLink)->Next = *(ppList)), (*(ppList) = (pLink))) |
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
] DECLARATIONS ///
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 43 of file reoSwap.c.
00044 { 00045 // the levels in the decision diagram 00046 int lev1 = lev0 + 1, lev2 = lev0 + 2; 00047 // the new nodes on lev0 00048 reo_unit * pLoop, * pUnit; 00049 // the new nodes on lev1 00050 reo_unit * pNewPlane20, * pNewPlane21, * pNewPlane20R; 00051 reo_unit * pUnitE, * pUnitER, * pUnitT; 00052 // the nodes below lev1 00053 reo_unit * pNew1E, * pNew1T, * pNew2E, * pNew2T; 00054 reo_unit * pNew1ER, * pNew2ER; 00055 // the old linked lists 00056 reo_unit * pListOld0 = p->pPlanes[lev0].pHead; 00057 reo_unit * pListOld1 = p->pPlanes[lev1].pHead; 00058 // working planes and one more temporary plane 00059 reo_unit * pListNew0 = NULL, ** ppListNew0 = &pListNew0; 00060 reo_unit * pListNew1 = NULL, ** ppListNew1 = &pListNew1; 00061 reo_unit * pListTemp = NULL, ** ppListTemp = &pListTemp; 00062 // various integer variables 00063 int fComp, fCompT, fFound, nWidthCofs, HKey, fInteract, temp, c; 00064 // statistical variables 00065 int nNodesUpMovedDown = 0; 00066 int nNodesDownMovedUp = 0; 00067 int nNodesUnrefRemoved = 0; 00068 int nNodesUnrefAdded = 0; 00069 int nWidthReduction = 0; 00070 double AplWeightTotalLev0; 00071 double AplWeightTotalLev1; 00072 double AplWeightHalf; 00073 double AplWeightPrev; 00074 double AplWeightAfter; 00075 double nCostGain; 00076 00077 // set the old lists 00078 assert( lev0 >= 0 && lev1 < p->nSupp ); 00079 pListOld0 = p->pPlanes[lev0].pHead; 00080 pListOld1 = p->pPlanes[lev1].pHead; 00081 00082 // make sure the planes have nodes 00083 assert( p->pPlanes[lev0].statsNodes && p->pPlanes[lev1].statsNodes ); 00084 assert( pListOld0 && pListOld1 ); 00085 00086 if ( p->fMinWidth ) 00087 { 00088 // verify that the width parameters are set correctly 00089 reoProfileWidthVerifyLevel( p->pPlanes + lev0, lev0 ); 00090 reoProfileWidthVerifyLevel( p->pPlanes + lev1, lev1 ); 00091 // start the storage for cofactors 00092 nWidthCofs = 0; 00093 } 00094 else if ( p->fMinApl ) 00095 { 00096 AplWeightPrev = p->nAplCur; 00097 AplWeightAfter = p->nAplCur; 00098 AplWeightTotalLev0 = 0.0; 00099 AplWeightTotalLev1 = 0.0; 00100 } 00101 00102 // check if the planes interact 00103 fInteract = 0; // assume that they do not interact 00104 for ( pUnit = pListOld0; pUnit; pUnit = pUnit->Next ) 00105 { 00106 if ( pUnit->pT->lev == lev1 || Unit_Regular(pUnit->pE)->lev == lev1 ) 00107 { 00108 fInteract = 1; 00109 break; 00110 } 00111 // change the level now, this is done for efficiency reasons 00112 pUnit->lev = lev1; 00113 } 00114 00115 // set the new signature for hashing 00116 p->nSwaps++; 00117 if ( !fInteract ) 00118 // if ( 0 ) 00119 { 00120 // perform the swap without interaction 00121 p->nNISwaps++; 00122 00123 // change the levels 00124 if ( p->fMinWidth ) 00125 { 00126 // go through the current lower level, which will become upper 00127 for ( pUnit = pListOld1; pUnit; pUnit = pUnit->Next ) 00128 { 00129 pUnit->lev = lev0; 00130 00131 pUnitER = Unit_Regular(pUnit->pE); 00132 if ( pUnitER->TopRef > lev0 ) 00133 { 00134 if ( pUnitER->Sign != p->nSwaps ) 00135 { 00136 if ( pUnitER->TopRef == lev2 ) 00137 { 00138 pUnitER->TopRef = lev1; 00139 nWidthReduction--; 00140 } 00141 else 00142 { 00143 assert( pUnitER->TopRef == lev1 ); 00144 } 00145 pUnitER->Sign = p->nSwaps; 00146 } 00147 } 00148 00149 pUnitT = pUnit->pT; 00150 if ( pUnitT->TopRef > lev0 ) 00151 { 00152 if ( pUnitT->Sign != p->nSwaps ) 00153 { 00154 if ( pUnitT->TopRef == lev2 ) 00155 { 00156 pUnitT->TopRef = lev1; 00157 nWidthReduction--; 00158 } 00159 else 00160 { 00161 assert( pUnitT->TopRef == lev1 ); 00162 } 00163 pUnitT->Sign = p->nSwaps; 00164 } 00165 } 00166 00167 } 00168 00169 // go through the current upper level, which will become lower 00170 for ( pUnit = pListOld0; pUnit; pUnit = pUnit->Next ) 00171 { 00172 pUnit->lev = lev1; 00173 00174 pUnitER = Unit_Regular(pUnit->pE); 00175 if ( pUnitER->TopRef > lev0 ) 00176 { 00177 if ( pUnitER->Sign != p->nSwaps ) 00178 { 00179 assert( pUnitER->TopRef == lev1 ); 00180 pUnitER->TopRef = lev2; 00181 pUnitER->Sign = p->nSwaps; 00182 nWidthReduction++; 00183 } 00184 } 00185 00186 pUnitT = pUnit->pT; 00187 if ( pUnitT->TopRef > lev0 ) 00188 { 00189 if ( pUnitT->Sign != p->nSwaps ) 00190 { 00191 assert( pUnitT->TopRef == lev1 ); 00192 pUnitT->TopRef = lev2; 00193 pUnitT->Sign = p->nSwaps; 00194 nWidthReduction++; 00195 } 00196 } 00197 } 00198 } 00199 else 00200 { 00201 // for ( pUnit = pListOld0; pUnit; pUnit = pUnit->Next ) 00202 // pUnit->lev = lev1; 00203 for ( pUnit = pListOld1; pUnit; pUnit = pUnit->Next ) 00204 pUnit->lev = lev0; 00205 } 00206 00207 // set the new linked lists, which will be attached to the planes 00208 pListNew0 = pListOld1; 00209 pListNew1 = pListOld0; 00210 00211 if ( p->fMinApl ) 00212 { 00213 AplWeightTotalLev0 = p->pPlanes[lev1].statsCost; 00214 AplWeightTotalLev1 = p->pPlanes[lev0].statsCost; 00215 } 00216 00217 // set the changes in terms of nodes 00218 nNodesUpMovedDown = p->pPlanes[lev0].statsNodes; 00219 nNodesDownMovedUp = p->pPlanes[lev1].statsNodes; 00220 goto finish; 00221 } 00222 p->Signature++; 00223 00224 00225 // two-variable swap is done in three easy steps 00226 // previously I thought that steps (1) and (2) can be merged into one step 00227 // now it is clear that this cannot be done without changing a lot of other stuff... 00228 00229 // (1) walk through the upper level, find units without cofactors in the lower level 00230 // and move them to the new lower level (while adding to the cache) 00231 // (2) walk through the uppoer level, and tranform all the remaning nodes 00232 // while employing cache for the new lower level 00233 // (3) walk through the old lower level, find those nodes whose ref counters are not zero, 00234 // and move them to the new uppoer level, free other nodes 00235 00236 // (1) walk through the upper level, find units without cofactors in the lower level 00237 // and move them to the new lower level (while adding to the cache) 00238 for ( pLoop = pListOld0; pLoop; ) 00239 { 00240 pUnit = pLoop; 00241 pLoop = pLoop->Next; 00242 00243 pUnitE = pUnit->pE; 00244 pUnitER = Unit_Regular(pUnitE); 00245 pUnitT = pUnit->pT; 00246 00247 if ( pUnitER->lev != lev1 && pUnitT->lev != lev1 ) 00248 { 00249 // before after 00250 // 00251 // <p1> 00252 // 0 / \ 1 00253 // / \ 00254 // / \ 00255 // / \ <p2n> 00256 // / \ 0 / \ 1 00257 // / \ / \ 00258 // / \ / \ 00259 // F0 F1 F0 F1 00260 00261 // move to plane-2-new 00262 // nothing changes in the process (cofactors, ref counter, APL weight) 00263 pUnit->lev = lev1; 00264 AddToLinkedList( ppListNew1, pUnit ); 00265 if ( p->fMinApl ) 00266 AplWeightTotalLev1 += pUnit->Weight; 00267 00268 // add to cache - find the cell with different signature (not the current one!) 00269 for ( HKey = hashKey3(p->Signature, pUnitE, pUnitT, p->nTableSize); 00270 p->HTable[HKey].Sign == p->Signature; 00271 HKey = (HKey+1) % p->nTableSize ); 00272 assert( p->HTable[HKey].Sign != p->Signature ); 00273 p->HTable[HKey].Sign = p->Signature; 00274 p->HTable[HKey].Arg1 = pUnitE; 00275 p->HTable[HKey].Arg2 = pUnitT; 00276 p->HTable[HKey].Arg3 = pUnit; 00277 00278 nNodesUpMovedDown++; 00279 00280 if ( p->fMinWidth ) 00281 { 00282 // update the cofactors's top ref 00283 if ( pUnitER->TopRef > lev0 ) // the cofactor's top ref level is one of the current two levels 00284 { 00285 assert( pUnitER->TopRef == lev1 ); 00286 pUnitER->TopRefNew = lev2; 00287 if ( pUnitER->Sign != p->nSwaps ) 00288 { 00289 pUnitER->Sign = p->nSwaps; // set the current signature 00290 p->pWidthCofs[ nWidthCofs++ ] = pUnitER; 00291 } 00292 } 00293 if ( pUnitT->TopRef > lev0 ) // the cofactor's top ref level is one of the current two levels 00294 { 00295 assert( pUnitT->TopRef == lev1 ); 00296 pUnitT->TopRefNew = lev2; 00297 if ( pUnitT->Sign != p->nSwaps ) 00298 { 00299 pUnitT->Sign = p->nSwaps; // set the current signature 00300 p->pWidthCofs[ nWidthCofs++ ] = pUnitT; 00301 } 00302 } 00303 } 00304 } 00305 else 00306 { 00307 // add to the temporary plane 00308 AddToLinkedList( ppListTemp, pUnit ); 00309 } 00310 } 00311 00312 00313 // (2) walk through the uppoer level, and tranform all the remaning nodes 00314 // while employing cache for the new lower level 00315 for ( pLoop = pListTemp; pLoop; ) 00316 { 00317 pUnit = pLoop; 00318 pLoop = pLoop->Next; 00319 00320 pUnitE = pUnit->pE; 00321 pUnitER = Unit_Regular(pUnitE); 00322 pUnitT = pUnit->pT; 00323 fComp = (int)(pUnitER != pUnitE); 00324 00325 // count the amount of weight to reduce the APL of the children of this node 00326 if ( p->fMinApl ) 00327 AplWeightHalf = 0.5 * pUnit->Weight; 00328 00329 // determine what situation is this 00330 if ( pUnitER->lev == lev1 && pUnitT->lev == lev1 ) 00331 { 00332 if ( fComp == 0 ) 00333 { 00334 // before after 00335 // 00336 // <p1> <p1n> 00337 // 0 / \ 1 0 / \ 1 00338 // / \ / \ 00339 // / \ / \ 00340 // <p2> <p2> <p2n> <p2n> 00341 // 0 / \ 1 0 / \ 1 0 / \ 1 0 / \ 1 00342 // / \ / \ / \ / \ 00343 // / \ / \ / \ / \ 00344 // F0 F1 F2 F3 F0 F2 F1 F3 00345 // pNew1E pNew1T pNew2E pNew2T 00346 // 00347 pNew1E = pUnitE->pE; // F0 00348 pNew1T = pUnitT->pE; // F2 00349 00350 pNew2E = pUnitE->pT; // F1 00351 pNew2T = pUnitT->pT; // F3 00352 } 00353 else 00354 { 00355 // before after 00356 // 00357 // <p1> <p1n> 00358 // 0 . \ 1 0 / \ 1 00359 // . \ / \ 00360 // . \ / \ 00361 // <p2> <p2> <p2n> <p2n> 00362 // 0 / \ 1 0 / \ 1 0 . \ 1 0 . \ 1 00363 // / \ / \ . \ . \ 00364 // / \ / \ . \ . \ 00365 // F0 F1 F2 F3 F0 F2 F1 F3 00366 // pNew1E pNew1T pNew2E pNew2T 00367 // 00368 pNew1E = Unit_Not(pUnitER->pE); // F0 00369 pNew1T = pUnitT->pE; // F2 00370 00371 pNew2E = Unit_Not(pUnitER->pT); // F1 00372 pNew2T = pUnitT->pT; // F3 00373 } 00374 // subtract ref counters - on the level P2 00375 pUnitER->n--; 00376 pUnitT->n--; 00377 00378 // mark the change in the APL weights 00379 if ( p->fMinApl ) 00380 { 00381 pUnitER->Weight -= AplWeightHalf; 00382 pUnitT->Weight -= AplWeightHalf; 00383 AplWeightAfter -= pUnit->Weight; 00384 } 00385 } 00386 else if ( pUnitER->lev == lev1 ) 00387 { 00388 if ( fComp == 0 ) 00389 { 00390 // before after 00391 // 00392 // <p1> <p1n> 00393 // 0 / \ 1 0 / \ 1 00394 // / \ / \ 00395 // / \ / \ 00396 // <p2> \ <p2n> <p2n> 00397 // 0 / \ 1 \ 0 / \ 1 0 / \ 1 00398 // / \ \ / \ / \ 00399 // / \ \ / \ / \ 00400 // F0 F1 F3 F0 F3 F1 F3 00401 // pNew1E pNew1T pNew2E pNew2T 00402 // 00403 pNew1E = pUnitER->pE; // F0 00404 pNew1T = pUnitT; // F3 00405 00406 pNew2E = pUnitER->pT; // F1 00407 pNew2T = pUnitT; // F3 00408 } 00409 else 00410 { 00411 // before after 00412 // 00413 // <p1> <p1n> 00414 // 0 . \ 1 0 / \ 1 00415 // . \ / \ 00416 // . \ / \ 00417 // <p2> \ <p2n> <p2n> 00418 // 0 / \ 1 \ 0 . \ 1 0 . \ 1 00419 // / \ \ . \ . \ 00420 // / \ \ . \ . \ 00421 // F0 F1 F3 F0 F3 F1 F3 00422 // pNew1E pNew1T pNew2E pNew2T 00423 // 00424 pNew1E = Unit_Not(pUnitER->pE); // F0 00425 pNew1T = pUnitT; // F3 00426 00427 pNew2E = Unit_Not(pUnitER->pT); // F1 00428 pNew2T = pUnitT; // F3 00429 } 00430 // subtract ref counter - on the level P2 00431 pUnitER->n--; 00432 // subtract ref counter - on other levels 00433 pUnitT->n--; 00434 00435 // mark the change in the APL weights 00436 if ( p->fMinApl ) 00437 { 00438 pUnitER->Weight -= AplWeightHalf; 00439 AplWeightAfter -= AplWeightHalf; 00440 } 00441 } 00442 else if ( pUnitT->lev == lev1 ) 00443 { 00444 // before after 00445 // 00446 // <p1> <p1n> 00447 // 0 / \ 1 0 / \ 1 00448 // / \ / \ 00449 // / \ / \ 00450 // / <p2> <p2n> <p2n> 00451 // / 0 / \ 1 0 / \ 1 0 / \ 1 00452 // / / \ / \ / \ 00453 // / / \ / \ / \ 00454 // F0 F2 F3 F0 F2 F0 F3 00455 // pNew1E pNew1T pNew2E pNew2T 00456 // 00457 pNew1E = pUnitE; // F0 00458 pNew1T = pUnitT->pE; // F2 00459 00460 pNew2E = pUnitE; // F0 00461 pNew2T = pUnitT->pT; // F3 00462 00463 // subtract incoming edge counter - on the level P2 00464 pUnitT->n--; 00465 // subtract ref counter - on other levels 00466 pUnitER->n--; 00467 00468 // mark the change in the APL weights 00469 if ( p->fMinApl ) 00470 { 00471 pUnitT->Weight -= AplWeightHalf; 00472 AplWeightAfter -= AplWeightHalf; 00473 } 00474 } 00475 else 00476 { 00477 assert( 0 ); // should never happen 00478 } 00479 00480 00481 // consider all the cases except the last one 00482 if ( pNew1E == pNew1T ) 00483 { 00484 pNewPlane20 = pNew1T; 00485 00486 if ( p->fMinWidth ) 00487 { 00488 // update the cofactors's top ref 00489 if ( pNew1T->TopRef > lev0 ) // the cofactor's top ref level is one of the current two levels 00490 { 00491 pNew1T->TopRefNew = lev1; 00492 if ( pNew1T->Sign != p->nSwaps ) 00493 { 00494 pNew1T->Sign = p->nSwaps; // set the current signature 00495 p->pWidthCofs[ nWidthCofs++ ] = pNew1T; 00496 } 00497 } 00498 } 00499 } 00500 else 00501 { 00502 // pNew1T can be complemented 00503 fCompT = Cudd_IsComplement(pNew1T); 00504 if ( fCompT ) 00505 { 00506 pNew1E = Unit_Not(pNew1E); 00507 pNew1T = Unit_Not(pNew1T); 00508 } 00509 00510 // check the hash-table 00511 fFound = 0; 00512 for ( HKey = hashKey3(p->Signature, pNew1E, pNew1T, p->nTableSize); 00513 p->HTable[HKey].Sign == p->Signature; 00514 HKey = (HKey+1) % p->nTableSize ) 00515 if ( p->HTable[HKey].Arg1 == pNew1E && p->HTable[HKey].Arg2 == pNew1T ) 00516 { // the entry is present 00517 // assign this entry 00518 pNewPlane20 = p->HTable[HKey].Arg3; 00519 assert( pNewPlane20->lev == lev1 ); 00520 fFound = 1; 00521 p->HashSuccess++; 00522 break; 00523 } 00524 00525 if ( !fFound ) 00526 { // create the new entry 00527 pNewPlane20 = reoUnitsGetNextUnit( p ); // increments the unit counter 00528 pNewPlane20->pE = pNew1E; 00529 pNewPlane20->pT = pNew1T; 00530 pNewPlane20->n = 0; // ref will be added later 00531 pNewPlane20->lev = lev1; 00532 if ( p->fMinWidth ) 00533 { 00534 pNewPlane20->TopRef = lev1; 00535 pNewPlane20->Sign = 0; 00536 } 00537 // set the weight of this node 00538 if ( p->fMinApl ) 00539 pNewPlane20->Weight = 0.0; 00540 00541 // increment ref counters of children 00542 pNew1ER = Unit_Regular(pNew1E); 00543 pNew1ER->n++; // 00544 pNew1T->n++; // 00545 00546 // insert into the data structure 00547 AddToLinkedList( ppListNew1, pNewPlane20 ); 00548 00549 // add this entry to cache 00550 assert( p->HTable[HKey].Sign != p->Signature ); 00551 p->HTable[HKey].Sign = p->Signature; 00552 p->HTable[HKey].Arg1 = pNew1E; 00553 p->HTable[HKey].Arg2 = pNew1T; 00554 p->HTable[HKey].Arg3 = pNewPlane20; 00555 00556 nNodesUnrefAdded++; 00557 00558 if ( p->fMinWidth ) 00559 { 00560 // update the cofactors's top ref 00561 if ( pNew1ER->TopRef > lev0 ) // the cofactor's top ref level is one of the current two levels 00562 { 00563 if ( pNew1ER->Sign != p->nSwaps ) 00564 { 00565 pNew1ER->TopRefNew = lev2; 00566 if ( pNew1ER->Sign != p->nSwaps ) 00567 { 00568 pNew1ER->Sign = p->nSwaps; // set the current signature 00569 p->pWidthCofs[ nWidthCofs++ ] = pNew1ER; 00570 } 00571 } 00572 // otherwise the level is already set correctly 00573 else 00574 { 00575 assert( pNew1ER->TopRefNew == lev1 || pNew1ER->TopRefNew == lev2 ); 00576 } 00577 } 00578 // update the cofactors's top ref 00579 if ( pNew1T->TopRef > lev0 ) // the cofactor's top ref level is one of the current two levels 00580 { 00581 if ( pNew1T->Sign != p->nSwaps ) 00582 { 00583 pNew1T->TopRefNew = lev2; 00584 if ( pNew1T->Sign != p->nSwaps ) 00585 { 00586 pNew1T->Sign = p->nSwaps; // set the current signature 00587 p->pWidthCofs[ nWidthCofs++ ] = pNew1T; 00588 } 00589 } 00590 // otherwise the level is already set correctly 00591 else 00592 { 00593 assert( pNew1T->TopRefNew == lev1 || pNew1T->TopRefNew == lev2 ); 00594 } 00595 } 00596 } 00597 } 00598 00599 if ( p->fMinApl ) 00600 { 00601 // increment the weight of this node 00602 pNewPlane20->Weight += AplWeightHalf; 00603 // mark the change in the APL weight 00604 AplWeightAfter += AplWeightHalf; 00605 // update the total weight of this level 00606 AplWeightTotalLev1 += AplWeightHalf; 00607 } 00608 00609 if ( fCompT ) 00610 pNewPlane20 = Unit_Not(pNewPlane20); 00611 } 00612 00613 if ( pNew2E == pNew2T ) 00614 { 00615 pNewPlane21 = pNew2T; 00616 00617 if ( p->fMinWidth ) 00618 { 00619 // update the cofactors's top ref 00620 if ( pNew2T->TopRef > lev0 ) // the cofactor's top ref level is one of the current two levels 00621 { 00622 pNew2T->TopRefNew = lev1; 00623 if ( pNew2T->Sign != p->nSwaps ) 00624 { 00625 pNew2T->Sign = p->nSwaps; // set the current signature 00626 p->pWidthCofs[ nWidthCofs++ ] = pNew2T; 00627 } 00628 } 00629 } 00630 } 00631 else 00632 { 00633 assert( !Cudd_IsComplement(pNew2T) ); 00634 00635 // check the hash-table 00636 fFound = 0; 00637 for ( HKey = hashKey3(p->Signature, pNew2E, pNew2T, p->nTableSize); 00638 p->HTable[HKey].Sign == p->Signature; 00639 HKey = (HKey+1) % p->nTableSize ) 00640 if ( p->HTable[HKey].Arg1 == pNew2E && p->HTable[HKey].Arg2 == pNew2T ) 00641 { // the entry is present 00642 // assign this entry 00643 pNewPlane21 = p->HTable[HKey].Arg3; 00644 assert( pNewPlane21->lev == lev1 ); 00645 fFound = 1; 00646 p->HashSuccess++; 00647 break; 00648 } 00649 00650 if ( !fFound ) 00651 { // create the new entry 00652 pNewPlane21 = reoUnitsGetNextUnit( p ); // increments the unit counter 00653 pNewPlane21->pE = pNew2E; 00654 pNewPlane21->pT = pNew2T; 00655 pNewPlane21->n = 0; // ref will be added later 00656 pNewPlane21->lev = lev1; 00657 if ( p->fMinWidth ) 00658 { 00659 pNewPlane21->TopRef = lev1; 00660 pNewPlane21->Sign = 0; 00661 } 00662 // set the weight of this node 00663 if ( p->fMinApl ) 00664 pNewPlane21->Weight = 0.0; 00665 00666 // increment ref counters of children 00667 pNew2ER = Unit_Regular(pNew2E); 00668 pNew2ER->n++; // 00669 pNew2T->n++; // 00670 00671 // insert into the data structure 00672 // reoUnitsAddUnitToPlane( &P2new, pNewPlane21 ); 00673 AddToLinkedList( ppListNew1, pNewPlane21 ); 00674 00675 // add this entry to cache 00676 assert( p->HTable[HKey].Sign != p->Signature ); 00677 p->HTable[HKey].Sign = p->Signature; 00678 p->HTable[HKey].Arg1 = pNew2E; 00679 p->HTable[HKey].Arg2 = pNew2T; 00680 p->HTable[HKey].Arg3 = pNewPlane21; 00681 00682 nNodesUnrefAdded++; 00683 00684 00685 if ( p->fMinWidth ) 00686 { 00687 // update the cofactors's top ref 00688 if ( pNew2ER->TopRef > lev0 ) // the cofactor's top ref level is one of the current two levels 00689 { 00690 if ( pNew2ER->Sign != p->nSwaps ) 00691 { 00692 pNew2ER->TopRefNew = lev2; 00693 if ( pNew2ER->Sign != p->nSwaps ) 00694 { 00695 pNew2ER->Sign = p->nSwaps; // set the current signature 00696 p->pWidthCofs[ nWidthCofs++ ] = pNew2ER; 00697 } 00698 } 00699 // otherwise the level is already set correctly 00700 else 00701 { 00702 assert( pNew2ER->TopRefNew == lev1 || pNew2ER->TopRefNew == lev2 ); 00703 } 00704 } 00705 // update the cofactors's top ref 00706 if ( pNew2T->TopRef > lev0 ) // the cofactor's top ref level is one of the current two levels 00707 { 00708 if ( pNew2T->Sign != p->nSwaps ) 00709 { 00710 pNew2T->TopRefNew = lev2; 00711 if ( pNew2T->Sign != p->nSwaps ) 00712 { 00713 pNew2T->Sign = p->nSwaps; // set the current signature 00714 p->pWidthCofs[ nWidthCofs++ ] = pNew2T; 00715 } 00716 } 00717 // otherwise the level is already set correctly 00718 else 00719 { 00720 assert( pNew2T->TopRefNew == lev1 || pNew2T->TopRefNew == lev2 ); 00721 } 00722 } 00723 } 00724 } 00725 00726 if ( p->fMinApl ) 00727 { 00728 // increment the weight of this node 00729 pNewPlane21->Weight += AplWeightHalf; 00730 // mark the change in the APL weight 00731 AplWeightAfter += AplWeightHalf; 00732 // update the total weight of this level 00733 AplWeightTotalLev1 += AplWeightHalf; 00734 } 00735 } 00736 // in all cases, the node will be added to the plane-1 00737 // this should be the same node (pUnit) as was originally there 00738 // because it is referenced by the above nodes 00739 00740 assert( !Cudd_IsComplement(pNewPlane21) ); 00741 // should be the case; otherwise reordering is not a local operation 00742 00743 pUnit->pE = pNewPlane20; 00744 pUnit->pT = pNewPlane21; 00745 assert( pUnit->lev == lev0 ); 00746 // reference counter remains the same; the APL weight remains the same 00747 00748 // increment ref counters of children 00749 pNewPlane20R = Unit_Regular(pNewPlane20); 00750 pNewPlane20R->n++; 00751 pNewPlane21->n++; 00752 00753 // insert into the data structure 00754 AddToLinkedList( ppListNew0, pUnit ); 00755 if ( p->fMinApl ) 00756 AplWeightTotalLev0 += pUnit->Weight; 00757 } 00758 00759 // (3) walk through the old lower level, find those nodes whose ref counters are not zero, 00760 // and move them to the new uppoer level, free other nodes 00761 for ( pLoop = pListOld1; pLoop; ) 00762 { 00763 pUnit = pLoop; 00764 pLoop = pLoop->Next; 00765 if ( pUnit->n ) 00766 { 00767 assert( !p->fMinApl || pUnit->Weight > 0.0 ); 00768 // the node should be added to the new level 00769 // no need to check the hash table 00770 pUnit->lev = lev0; 00771 AddToLinkedList( ppListNew0, pUnit ); 00772 if ( p->fMinApl ) 00773 AplWeightTotalLev0 += pUnit->Weight; 00774 00775 nNodesDownMovedUp++; 00776 00777 if ( p->fMinWidth ) 00778 { 00779 pUnitER = Unit_Regular(pUnit->pE); 00780 pUnitT = pUnit->pT; 00781 00782 // update the cofactors's top ref 00783 if ( pUnitER->TopRef > lev0 ) // the cofactor's top ref level is one of the current two levels 00784 { 00785 pUnitER->TopRefNew = lev1; 00786 if ( pUnitER->Sign != p->nSwaps ) 00787 { 00788 pUnitER->Sign = p->nSwaps; // set the current signature 00789 p->pWidthCofs[ nWidthCofs++ ] = pUnitER; 00790 } 00791 } 00792 if ( pUnitT->TopRef > lev0 ) // the cofactor's top ref level is one of the current two levels 00793 { 00794 pUnitT->TopRefNew = lev1; 00795 if ( pUnitT->Sign != p->nSwaps ) 00796 { 00797 pUnitT->Sign = p->nSwaps; // set the current signature 00798 p->pWidthCofs[ nWidthCofs++ ] = pUnitT; 00799 } 00800 } 00801 } 00802 } 00803 else 00804 { 00805 assert( !p->fMinApl || pUnit->Weight == 0.0 ); 00806 // decrement reference counters of children 00807 pUnitER = Unit_Regular(pUnit->pE); 00808 pUnitT = pUnit->pT; 00809 pUnitER->n--; 00810 pUnitT->n--; 00811 // the node should be thrown away 00812 reoUnitsRecycleUnit( p, pUnit ); 00813 nNodesUnrefRemoved++; 00814 } 00815 } 00816 00817 finish: 00818 00819 // attach the new levels to the planes 00820 p->pPlanes[lev0].pHead = pListNew0; 00821 p->pPlanes[lev1].pHead = pListNew1; 00822 00823 // swap the sift status 00824 temp = p->pPlanes[lev0].fSifted; 00825 p->pPlanes[lev0].fSifted = p->pPlanes[lev1].fSifted; 00826 p->pPlanes[lev1].fSifted = temp; 00827 00828 // swap variables in the variable map 00829 if ( p->pOrderInt ) 00830 { 00831 temp = p->pOrderInt[lev0]; 00832 p->pOrderInt[lev0] = p->pOrderInt[lev1]; 00833 p->pOrderInt[lev1] = temp; 00834 } 00835 00836 // adjust the node profile 00837 p->pPlanes[lev0].statsNodes -= (nNodesUpMovedDown - nNodesDownMovedUp); 00838 p->pPlanes[lev1].statsNodes -= (nNodesDownMovedUp - nNodesUpMovedDown) + nNodesUnrefRemoved - nNodesUnrefAdded; 00839 p->nNodesCur -= nNodesUnrefRemoved - nNodesUnrefAdded; 00840 00841 // adjust the node profile on this level 00842 if ( p->fMinWidth ) 00843 { 00844 for ( c = 0; c < nWidthCofs; c++ ) 00845 { 00846 if ( p->pWidthCofs[c]->TopRefNew < p->pWidthCofs[c]->TopRef ) 00847 { 00848 p->pWidthCofs[c]->TopRef = p->pWidthCofs[c]->TopRefNew; 00849 nWidthReduction--; 00850 } 00851 else if ( p->pWidthCofs[c]->TopRefNew > p->pWidthCofs[c]->TopRef ) 00852 { 00853 p->pWidthCofs[c]->TopRef = p->pWidthCofs[c]->TopRefNew; 00854 nWidthReduction++; 00855 } 00856 } 00857 // verify that the profile is okay 00858 reoProfileWidthVerifyLevel( p->pPlanes + lev0, lev0 ); 00859 reoProfileWidthVerifyLevel( p->pPlanes + lev1, lev1 ); 00860 00861 // compute the total gain in terms of width 00862 nCostGain = (nNodesDownMovedUp - nNodesUpMovedDown + nNodesUnrefRemoved - nNodesUnrefAdded) + nWidthReduction; 00863 // adjust the width on this level 00864 p->pPlanes[lev1].statsWidth -= (int)nCostGain; 00865 // set the cost 00866 p->pPlanes[lev1].statsCost = p->pPlanes[lev1].statsWidth; 00867 } 00868 else if ( p->fMinApl ) 00869 { 00870 // compute the total gain in terms of APL 00871 nCostGain = AplWeightPrev - AplWeightAfter; 00872 // make sure that the ALP is updated correctly 00873 // assert( p->pPlanes[lev0].statsCost + p->pPlanes[lev1].statsCost - nCostGain == 00874 // AplWeightTotalLev0 + AplWeightTotalLev1 ); 00875 // adjust the profile 00876 p->pPlanes[lev0].statsApl = AplWeightTotalLev0; 00877 p->pPlanes[lev1].statsApl = AplWeightTotalLev1; 00878 // set the cost 00879 p->pPlanes[lev0].statsCost = p->pPlanes[lev0].statsApl; 00880 p->pPlanes[lev1].statsCost = p->pPlanes[lev1].statsApl; 00881 } 00882 else 00883 { 00884 // compute the total gain in terms of the number of nodes 00885 nCostGain = nNodesUnrefRemoved - nNodesUnrefAdded; 00886 // adjust the profile (adjusted above) 00887 // set the cost 00888 p->pPlanes[lev0].statsCost = p->pPlanes[lev0].statsNodes; 00889 p->pPlanes[lev1].statsCost = p->pPlanes[lev1].statsNodes; 00890 } 00891 00892 return nCostGain; 00893 }
