diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2007-10-01 08:01:00 -0700 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2007-10-01 08:01:00 -0700 |
commit | 4812c90424dfc40d26725244723887a2d16ddfd9 (patch) | |
tree | b32ace96e7e2d84d586e09ba605463b6f49c3271 /src/bdd/reo/reoSwap.c | |
parent | e54d9691616b9a0326e2fdb3156bb4eeb8abfcd7 (diff) | |
download | abc-4812c90424dfc40d26725244723887a2d16ddfd9.tar.gz abc-4812c90424dfc40d26725244723887a2d16ddfd9.tar.bz2 abc-4812c90424dfc40d26725244723887a2d16ddfd9.zip |
Version abc71001
Diffstat (limited to 'src/bdd/reo/reoSwap.c')
-rw-r--r-- | src/bdd/reo/reoSwap.c | 898 |
1 files changed, 898 insertions, 0 deletions
diff --git a/src/bdd/reo/reoSwap.c b/src/bdd/reo/reoSwap.c new file mode 100644 index 00000000..4afa650c --- /dev/null +++ b/src/bdd/reo/reoSwap.c @@ -0,0 +1,898 @@ +/**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 $] + +***********************************************************************/ + +#include "reo.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +#define AddToLinkedList( ppList, pLink ) (((pLink)->Next = *(ppList)), (*(ppList) = (pLink))) + +//////////////////////////////////////////////////////////////////////// +/// 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 [] + +***********************************************************************/ +double reoReorderSwapAdjacentVars( reo_man * p, int lev0, int fMovingUp ) +{ + // the levels in the decision diagram + int lev1 = lev0 + 1, lev2 = lev0 + 2; + // the new nodes on lev0 + reo_unit * pLoop, * pUnit; + // the new nodes on lev1 + reo_unit * pNewPlane20, * pNewPlane21, * pNewPlane20R; + reo_unit * pUnitE, * pUnitER, * pUnitT; + // the nodes below lev1 + reo_unit * pNew1E, * pNew1T, * pNew2E, * pNew2T; + reo_unit * pNew1ER, * pNew2ER; + // the old linked lists + reo_unit * pListOld0 = p->pPlanes[lev0].pHead; + reo_unit * pListOld1 = p->pPlanes[lev1].pHead; + // working planes and one more temporary plane + reo_unit * pListNew0 = NULL, ** ppListNew0 = &pListNew0; + reo_unit * pListNew1 = NULL, ** ppListNew1 = &pListNew1; + reo_unit * pListTemp = NULL, ** ppListTemp = &pListTemp; + // various integer variables + int fComp, fCompT, fFound, nWidthCofs, HKey, fInteract, temp, c; + // statistical variables + int nNodesUpMovedDown = 0; + int nNodesDownMovedUp = 0; + int nNodesUnrefRemoved = 0; + int nNodesUnrefAdded = 0; + int nWidthReduction = 0; + double AplWeightTotalLev0; + double AplWeightTotalLev1; + double AplWeightHalf; + double AplWeightPrev; + double AplWeightAfter; + double nCostGain; + + // set the old lists + assert( lev0 >= 0 && lev1 < p->nSupp ); + pListOld0 = p->pPlanes[lev0].pHead; + pListOld1 = p->pPlanes[lev1].pHead; + + // make sure the planes have nodes + assert( p->pPlanes[lev0].statsNodes && p->pPlanes[lev1].statsNodes ); + assert( pListOld0 && pListOld1 ); + + if ( p->fMinWidth ) + { + // verify that the width parameters are set correctly + reoProfileWidthVerifyLevel( p->pPlanes + lev0, lev0 ); + reoProfileWidthVerifyLevel( p->pPlanes + lev1, lev1 ); + // start the storage for cofactors + nWidthCofs = 0; + } + else if ( p->fMinApl ) + { + AplWeightPrev = p->nAplCur; + AplWeightAfter = p->nAplCur; + AplWeightTotalLev0 = 0.0; + AplWeightTotalLev1 = 0.0; + } + + // check if the planes interact + fInteract = 0; // assume that they do not interact + for ( pUnit = pListOld0; pUnit; pUnit = pUnit->Next ) + { + if ( pUnit->pT->lev == lev1 || Unit_Regular(pUnit->pE)->lev == lev1 ) + { + fInteract = 1; + break; + } + // change the level now, this is done for efficiency reasons + pUnit->lev = lev1; + } + + // set the new signature for hashing + p->nSwaps++; + if ( !fInteract ) +// if ( 0 ) + { + // perform the swap without interaction + p->nNISwaps++; + + // change the levels + if ( p->fMinWidth ) + { + // go through the current lower level, which will become upper + for ( pUnit = pListOld1; pUnit; pUnit = pUnit->Next ) + { + pUnit->lev = lev0; + + pUnitER = Unit_Regular(pUnit->pE); + if ( pUnitER->TopRef > lev0 ) + { + if ( pUnitER->Sign != p->nSwaps ) + { + if ( pUnitER->TopRef == lev2 ) + { + pUnitER->TopRef = lev1; + nWidthReduction--; + } + else + { + assert( pUnitER->TopRef == lev1 ); + } + pUnitER->Sign = p->nSwaps; + } + } + + pUnitT = pUnit->pT; + if ( pUnitT->TopRef > lev0 ) + { + if ( pUnitT->Sign != p->nSwaps ) + { + if ( pUnitT->TopRef == lev2 ) + { + pUnitT->TopRef = lev1; + nWidthReduction--; + } + else + { + assert( pUnitT->TopRef == lev1 ); + } + pUnitT->Sign = p->nSwaps; + } + } + + } + + // go through the current upper level, which will become lower + for ( pUnit = pListOld0; pUnit; pUnit = pUnit->Next ) + { + pUnit->lev = lev1; + + pUnitER = Unit_Regular(pUnit->pE); + if ( pUnitER->TopRef > lev0 ) + { + if ( pUnitER->Sign != p->nSwaps ) + { + assert( pUnitER->TopRef == lev1 ); + pUnitER->TopRef = lev2; + pUnitER->Sign = p->nSwaps; + nWidthReduction++; + } + } + + pUnitT = pUnit->pT; + if ( pUnitT->TopRef > lev0 ) + { + if ( pUnitT->Sign != p->nSwaps ) + { + assert( pUnitT->TopRef == lev1 ); + pUnitT->TopRef = lev2; + pUnitT->Sign = p->nSwaps; + nWidthReduction++; + } + } + } + } + else + { +// for ( pUnit = pListOld0; pUnit; pUnit = pUnit->Next ) +// pUnit->lev = lev1; + for ( pUnit = pListOld1; pUnit; pUnit = pUnit->Next ) + pUnit->lev = lev0; + } + + // set the new linked lists, which will be attached to the planes + pListNew0 = pListOld1; + pListNew1 = pListOld0; + + if ( p->fMinApl ) + { + AplWeightTotalLev0 = p->pPlanes[lev1].statsCost; + AplWeightTotalLev1 = p->pPlanes[lev0].statsCost; + } + + // set the changes in terms of nodes + nNodesUpMovedDown = p->pPlanes[lev0].statsNodes; + nNodesDownMovedUp = p->pPlanes[lev1].statsNodes; + goto finish; + } + p->Signature++; + + + // two-variable swap is done in three easy steps + // previously I thought that steps (1) and (2) can be merged into one step + // now it is clear that this cannot be done without changing a lot of other stuff... + + // (1) walk through the upper level, find units without cofactors in the lower level + // and move them to the new lower level (while adding to the cache) + // (2) walk through the uppoer level, and tranform all the remaning nodes + // while employing cache for the new lower level + // (3) walk through the old lower level, find those nodes whose ref counters are not zero, + // and move them to the new uppoer level, free other nodes + + // (1) walk through the upper level, find units without cofactors in the lower level + // and move them to the new lower level (while adding to the cache) + for ( pLoop = pListOld0; pLoop; ) + { + pUnit = pLoop; + pLoop = pLoop->Next; + + pUnitE = pUnit->pE; + pUnitER = Unit_Regular(pUnitE); + pUnitT = pUnit->pT; + + if ( pUnitER->lev != lev1 && pUnitT->lev != lev1 ) + { + // before after + // + // <p1> + // 0 / \ 1 + // / \ + // / \ + // / \ <p2n> + // / \ 0 / \ 1 + // / \ / \ + // / \ / \ + // F0 F1 F0 F1 + + // move to plane-2-new + // nothing changes in the process (cofactors, ref counter, APL weight) + pUnit->lev = lev1; + AddToLinkedList( ppListNew1, pUnit ); + if ( p->fMinApl ) + AplWeightTotalLev1 += pUnit->Weight; + + // add to cache - find the cell with different signature (not the current one!) + for ( HKey = hashKey3(p->Signature, pUnitE, pUnitT, p->nTableSize); + p->HTable[HKey].Sign == p->Signature; + HKey = (HKey+1) % p->nTableSize ); + assert( p->HTable[HKey].Sign != p->Signature ); + p->HTable[HKey].Sign = p->Signature; + p->HTable[HKey].Arg1 = pUnitE; + p->HTable[HKey].Arg2 = pUnitT; + p->HTable[HKey].Arg3 = pUnit; + + nNodesUpMovedDown++; + + if ( p->fMinWidth ) + { + // update the cofactors's top ref + if ( pUnitER->TopRef > lev0 ) // the cofactor's top ref level is one of the current two levels + { + assert( pUnitER->TopRef == lev1 ); + pUnitER->TopRefNew = lev2; + if ( pUnitER->Sign != p->nSwaps ) + { + pUnitER->Sign = p->nSwaps; // set the current signature + p->pWidthCofs[ nWidthCofs++ ] = pUnitER; + } + } + if ( pUnitT->TopRef > lev0 ) // the cofactor's top ref level is one of the current two levels + { + assert( pUnitT->TopRef == lev1 ); + pUnitT->TopRefNew = lev2; + if ( pUnitT->Sign != p->nSwaps ) + { + pUnitT->Sign = p->nSwaps; // set the current signature + p->pWidthCofs[ nWidthCofs++ ] = pUnitT; + } + } + } + } + else + { + // add to the temporary plane + AddToLinkedList( ppListTemp, pUnit ); + } + } + + + // (2) walk through the uppoer level, and tranform all the remaning nodes + // while employing cache for the new lower level + for ( pLoop = pListTemp; pLoop; ) + { + pUnit = pLoop; + pLoop = pLoop->Next; + + pUnitE = pUnit->pE; + pUnitER = Unit_Regular(pUnitE); + pUnitT = pUnit->pT; + fComp = (int)(pUnitER != pUnitE); + + // count the amount of weight to reduce the APL of the children of this node + if ( p->fMinApl ) + AplWeightHalf = 0.5 * pUnit->Weight; + + // determine what situation is this + if ( pUnitER->lev == lev1 && pUnitT->lev == lev1 ) + { + if ( fComp == 0 ) + { + // before after + // + // <p1> <p1n> + // 0 / \ 1 0 / \ 1 + // / \ / \ + // / \ / \ + // <p2> <p2> <p2n> <p2n> + // 0 / \ 1 0 / \ 1 0 / \ 1 0 / \ 1 + // / \ / \ / \ / \ + // / \ / \ / \ / \ + // F0 F1 F2 F3 F0 F2 F1 F3 + // pNew1E pNew1T pNew2E pNew2T + // + pNew1E = pUnitE->pE; // F0 + pNew1T = pUnitT->pE; // F2 + + pNew2E = pUnitE->pT; // F1 + pNew2T = pUnitT->pT; // F3 + } + else + { + // before after + // + // <p1> <p1n> + // 0 . \ 1 0 / \ 1 + // . \ / \ + // . \ / \ + // <p2> <p2> <p2n> <p2n> + // 0 / \ 1 0 / \ 1 0 . \ 1 0 . \ 1 + // / \ / \ . \ . \ + // / \ / \ . \ . \ + // F0 F1 F2 F3 F0 F2 F1 F3 + // pNew1E pNew1T pNew2E pNew2T + // + pNew1E = Unit_Not(pUnitER->pE); // F0 + pNew1T = pUnitT->pE; // F2 + + pNew2E = Unit_Not(pUnitER->pT); // F1 + pNew2T = pUnitT->pT; // F3 + } + // subtract ref counters - on the level P2 + pUnitER->n--; + pUnitT->n--; + + // mark the change in the APL weights + if ( p->fMinApl ) + { + pUnitER->Weight -= AplWeightHalf; + pUnitT->Weight -= AplWeightHalf; + AplWeightAfter -= pUnit->Weight; + } + } + else if ( pUnitER->lev == lev1 ) + { + if ( fComp == 0 ) + { + // before after + // + // <p1> <p1n> + // 0 / \ 1 0 / \ 1 + // / \ / \ + // / \ / \ + // <p2> \ <p2n> <p2n> + // 0 / \ 1 \ 0 / \ 1 0 / \ 1 + // / \ \ / \ / \ + // / \ \ / \ / \ + // F0 F1 F3 F0 F3 F1 F3 + // pNew1E pNew1T pNew2E pNew2T + // + pNew1E = pUnitER->pE; // F0 + pNew1T = pUnitT; // F3 + + pNew2E = pUnitER->pT; // F1 + pNew2T = pUnitT; // F3 + } + else + { + // before after + // + // <p1> <p1n> + // 0 . \ 1 0 / \ 1 + // . \ / \ + // . \ / \ + // <p2> \ <p2n> <p2n> + // 0 / \ 1 \ 0 . \ 1 0 . \ 1 + // / \ \ . \ . \ + // / \ \ . \ . \ + // F0 F1 F3 F0 F3 F1 F3 + // pNew1E pNew1T pNew2E pNew2T + // + pNew1E = Unit_Not(pUnitER->pE); // F0 + pNew1T = pUnitT; // F3 + + pNew2E = Unit_Not(pUnitER->pT); // F1 + pNew2T = pUnitT; // F3 + } + // subtract ref counter - on the level P2 + pUnitER->n--; + // subtract ref counter - on other levels + pUnitT->n--; /// + + // mark the change in the APL weights + if ( p->fMinApl ) + { + pUnitER->Weight -= AplWeightHalf; + AplWeightAfter -= AplWeightHalf; + } + } + else if ( pUnitT->lev == lev1 ) + { + // before after + // + // <p1> <p1n> + // 0 / \ 1 0 / \ 1 + // / \ / \ + // / \ / \ + // / <p2> <p2n> <p2n> + // / 0 / \ 1 0 / \ 1 0 / \ 1 + // / / \ / \ / \ + // / / \ / \ / \ + // F0 F2 F3 F0 F2 F0 F3 + // pNew1E pNew1T pNew2E pNew2T + // + pNew1E = pUnitE; // F0 + pNew1T = pUnitT->pE; // F2 + + pNew2E = pUnitE; // F0 + pNew2T = pUnitT->pT; // F3 + + // subtract incoming edge counter - on the level P2 + pUnitT->n--; + // subtract ref counter - on other levels + pUnitER->n--; /// + + // mark the change in the APL weights + if ( p->fMinApl ) + { + pUnitT->Weight -= AplWeightHalf; + AplWeightAfter -= AplWeightHalf; + } + } + else + { + assert( 0 ); // should never happen + } + + + // consider all the cases except the last one + if ( pNew1E == pNew1T ) + { + pNewPlane20 = pNew1T; + + if ( p->fMinWidth ) + { + // update the cofactors's top ref + if ( pNew1T->TopRef > lev0 ) // the cofactor's top ref level is one of the current two levels + { + pNew1T->TopRefNew = lev1; + if ( pNew1T->Sign != p->nSwaps ) + { + pNew1T->Sign = p->nSwaps; // set the current signature + p->pWidthCofs[ nWidthCofs++ ] = pNew1T; + } + } + } + } + else + { + // pNew1T can be complemented + fCompT = Cudd_IsComplement(pNew1T); + if ( fCompT ) + { + pNew1E = Unit_Not(pNew1E); + pNew1T = Unit_Not(pNew1T); + } + + // check the hash-table + fFound = 0; + for ( HKey = hashKey3(p->Signature, pNew1E, pNew1T, p->nTableSize); + p->HTable[HKey].Sign == p->Signature; + HKey = (HKey+1) % p->nTableSize ) + if ( p->HTable[HKey].Arg1 == pNew1E && p->HTable[HKey].Arg2 == pNew1T ) + { // the entry is present + // assign this entry + pNewPlane20 = p->HTable[HKey].Arg3; + assert( pNewPlane20->lev == lev1 ); + fFound = 1; + p->HashSuccess++; + break; + } + + if ( !fFound ) + { // create the new entry + pNewPlane20 = reoUnitsGetNextUnit( p ); // increments the unit counter + pNewPlane20->pE = pNew1E; + pNewPlane20->pT = pNew1T; + pNewPlane20->n = 0; // ref will be added later + pNewPlane20->lev = lev1; + if ( p->fMinWidth ) + { + pNewPlane20->TopRef = lev1; + pNewPlane20->Sign = 0; + } + // set the weight of this node + if ( p->fMinApl ) + pNewPlane20->Weight = 0.0; + + // increment ref counters of children + pNew1ER = Unit_Regular(pNew1E); + pNew1ER->n++; // + pNew1T->n++; // + + // insert into the data structure + AddToLinkedList( ppListNew1, pNewPlane20 ); + + // add this entry to cache + assert( p->HTable[HKey].Sign != p->Signature ); + p->HTable[HKey].Sign = p->Signature; + p->HTable[HKey].Arg1 = pNew1E; + p->HTable[HKey].Arg2 = pNew1T; + p->HTable[HKey].Arg3 = pNewPlane20; + + nNodesUnrefAdded++; + + if ( p->fMinWidth ) + { + // update the cofactors's top ref + if ( pNew1ER->TopRef > lev0 ) // the cofactor's top ref level is one of the current two levels + { + if ( pNew1ER->Sign != p->nSwaps ) + { + pNew1ER->TopRefNew = lev2; + if ( pNew1ER->Sign != p->nSwaps ) + { + pNew1ER->Sign = p->nSwaps; // set the current signature + p->pWidthCofs[ nWidthCofs++ ] = pNew1ER; + } + } + // otherwise the level is already set correctly + else + { + assert( pNew1ER->TopRefNew == lev1 || pNew1ER->TopRefNew == lev2 ); + } + } + // update the cofactors's top ref + if ( pNew1T->TopRef > lev0 ) // the cofactor's top ref level is one of the current two levels + { + if ( pNew1T->Sign != p->nSwaps ) + { + pNew1T->TopRefNew = lev2; + if ( pNew1T->Sign != p->nSwaps ) + { + pNew1T->Sign = p->nSwaps; // set the current signature + p->pWidthCofs[ nWidthCofs++ ] = pNew1T; + } + } + // otherwise the level is already set correctly + else + { + assert( pNew1T->TopRefNew == lev1 || pNew1T->TopRefNew == lev2 ); + } + } + } + } + + if ( p->fMinApl ) + { + // increment the weight of this node + pNewPlane20->Weight += AplWeightHalf; + // mark the change in the APL weight + AplWeightAfter += AplWeightHalf; + // update the total weight of this level + AplWeightTotalLev1 += AplWeightHalf; + } + + if ( fCompT ) + pNewPlane20 = Unit_Not(pNewPlane20); + } + + if ( pNew2E == pNew2T ) + { + pNewPlane21 = pNew2T; + + if ( p->fMinWidth ) + { + // update the cofactors's top ref + if ( pNew2T->TopRef > lev0 ) // the cofactor's top ref level is one of the current two levels + { + pNew2T->TopRefNew = lev1; + if ( pNew2T->Sign != p->nSwaps ) + { + pNew2T->Sign = p->nSwaps; // set the current signature + p->pWidthCofs[ nWidthCofs++ ] = pNew2T; + } + } + } + } + else + { + assert( !Cudd_IsComplement(pNew2T) ); + + // check the hash-table + fFound = 0; + for ( HKey = hashKey3(p->Signature, pNew2E, pNew2T, p->nTableSize); + p->HTable[HKey].Sign == p->Signature; + HKey = (HKey+1) % p->nTableSize ) + if ( p->HTable[HKey].Arg1 == pNew2E && p->HTable[HKey].Arg2 == pNew2T ) + { // the entry is present + // assign this entry + pNewPlane21 = p->HTable[HKey].Arg3; + assert( pNewPlane21->lev == lev1 ); + fFound = 1; + p->HashSuccess++; + break; + } + + if ( !fFound ) + { // create the new entry + pNewPlane21 = reoUnitsGetNextUnit( p ); // increments the unit counter + pNewPlane21->pE = pNew2E; + pNewPlane21->pT = pNew2T; + pNewPlane21->n = 0; // ref will be added later + pNewPlane21->lev = lev1; + if ( p->fMinWidth ) + { + pNewPlane21->TopRef = lev1; + pNewPlane21->Sign = 0; + } + // set the weight of this node + if ( p->fMinApl ) + pNewPlane21->Weight = 0.0; + + // increment ref counters of children + pNew2ER = Unit_Regular(pNew2E); + pNew2ER->n++; // + pNew2T->n++; // + + // insert into the data structure +// reoUnitsAddUnitToPlane( &P2new, pNewPlane21 ); + AddToLinkedList( ppListNew1, pNewPlane21 ); + + // add this entry to cache + assert( p->HTable[HKey].Sign != p->Signature ); + p->HTable[HKey].Sign = p->Signature; + p->HTable[HKey].Arg1 = pNew2E; + p->HTable[HKey].Arg2 = pNew2T; + p->HTable[HKey].Arg3 = pNewPlane21; + + nNodesUnrefAdded++; + + + if ( p->fMinWidth ) + { + // update the cofactors's top ref + if ( pNew2ER->TopRef > lev0 ) // the cofactor's top ref level is one of the current two levels + { + if ( pNew2ER->Sign != p->nSwaps ) + { + pNew2ER->TopRefNew = lev2; + if ( pNew2ER->Sign != p->nSwaps ) + { + pNew2ER->Sign = p->nSwaps; // set the current signature + p->pWidthCofs[ nWidthCofs++ ] = pNew2ER; + } + } + // otherwise the level is already set correctly + else + { + assert( pNew2ER->TopRefNew == lev1 || pNew2ER->TopRefNew == lev2 ); + } + } + // update the cofactors's top ref + if ( pNew2T->TopRef > lev0 ) // the cofactor's top ref level is one of the current two levels + { + if ( pNew2T->Sign != p->nSwaps ) + { + pNew2T->TopRefNew = lev2; + if ( pNew2T->Sign != p->nSwaps ) + { + pNew2T->Sign = p->nSwaps; // set the current signature + p->pWidthCofs[ nWidthCofs++ ] = pNew2T; + } + } + // otherwise the level is already set correctly + else + { + assert( pNew2T->TopRefNew == lev1 || pNew2T->TopRefNew == lev2 ); + } + } + } + } + + if ( p->fMinApl ) + { + // increment the weight of this node + pNewPlane21->Weight += AplWeightHalf; + // mark the change in the APL weight + AplWeightAfter += AplWeightHalf; + // update the total weight of this level + AplWeightTotalLev1 += AplWeightHalf; + } + } + // in all cases, the node will be added to the plane-1 + // this should be the same node (pUnit) as was originally there + // because it is referenced by the above nodes + + assert( !Cudd_IsComplement(pNewPlane21) ); + // should be the case; otherwise reordering is not a local operation + + pUnit->pE = pNewPlane20; + pUnit->pT = pNewPlane21; + assert( pUnit->lev == lev0 ); + // reference counter remains the same; the APL weight remains the same + + // increment ref counters of children + pNewPlane20R = Unit_Regular(pNewPlane20); + pNewPlane20R->n++; /// + pNewPlane21->n++; /// + + // insert into the data structure + AddToLinkedList( ppListNew0, pUnit ); + if ( p->fMinApl ) + AplWeightTotalLev0 += pUnit->Weight; + } + + // (3) walk through the old lower level, find those nodes whose ref counters are not zero, + // and move them to the new uppoer level, free other nodes + for ( pLoop = pListOld1; pLoop; ) + { + pUnit = pLoop; + pLoop = pLoop->Next; + if ( pUnit->n ) + { + assert( !p->fMinApl || pUnit->Weight > 0.0 ); + // the node should be added to the new level + // no need to check the hash table + pUnit->lev = lev0; + AddToLinkedList( ppListNew0, pUnit ); + if ( p->fMinApl ) + AplWeightTotalLev0 += pUnit->Weight; + + nNodesDownMovedUp++; + + if ( p->fMinWidth ) + { + pUnitER = Unit_Regular(pUnit->pE); + pUnitT = pUnit->pT; + + // update the cofactors's top ref + if ( pUnitER->TopRef > lev0 ) // the cofactor's top ref level is one of the current two levels + { + pUnitER->TopRefNew = lev1; + if ( pUnitER->Sign != p->nSwaps ) + { + pUnitER->Sign = p->nSwaps; // set the current signature + p->pWidthCofs[ nWidthCofs++ ] = pUnitER; + } + } + if ( pUnitT->TopRef > lev0 ) // the cofactor's top ref level is one of the current two levels + { + pUnitT->TopRefNew = lev1; + if ( pUnitT->Sign != p->nSwaps ) + { + pUnitT->Sign = p->nSwaps; // set the current signature + p->pWidthCofs[ nWidthCofs++ ] = pUnitT; + } + } + } + } + else + { + assert( !p->fMinApl || pUnit->Weight == 0.0 ); + // decrement reference counters of children + pUnitER = Unit_Regular(pUnit->pE); + pUnitT = pUnit->pT; + pUnitER->n--; /// + pUnitT->n--; /// + // the node should be thrown away + reoUnitsRecycleUnit( p, pUnit ); + nNodesUnrefRemoved++; + } + } + +finish: + + // attach the new levels to the planes + p->pPlanes[lev0].pHead = pListNew0; + p->pPlanes[lev1].pHead = pListNew1; + + // swap the sift status + temp = p->pPlanes[lev0].fSifted; + p->pPlanes[lev0].fSifted = p->pPlanes[lev1].fSifted; + p->pPlanes[lev1].fSifted = temp; + + // swap variables in the variable map + if ( p->pOrderInt ) + { + temp = p->pOrderInt[lev0]; + p->pOrderInt[lev0] = p->pOrderInt[lev1]; + p->pOrderInt[lev1] = temp; + } + + // adjust the node profile + p->pPlanes[lev0].statsNodes -= (nNodesUpMovedDown - nNodesDownMovedUp); + p->pPlanes[lev1].statsNodes -= (nNodesDownMovedUp - nNodesUpMovedDown) + nNodesUnrefRemoved - nNodesUnrefAdded; + p->nNodesCur -= nNodesUnrefRemoved - nNodesUnrefAdded; + + // adjust the node profile on this level + if ( p->fMinWidth ) + { + for ( c = 0; c < nWidthCofs; c++ ) + { + if ( p->pWidthCofs[c]->TopRefNew < p->pWidthCofs[c]->TopRef ) + { + p->pWidthCofs[c]->TopRef = p->pWidthCofs[c]->TopRefNew; + nWidthReduction--; + } + else if ( p->pWidthCofs[c]->TopRefNew > p->pWidthCofs[c]->TopRef ) + { + p->pWidthCofs[c]->TopRef = p->pWidthCofs[c]->TopRefNew; + nWidthReduction++; + } + } + // verify that the profile is okay + reoProfileWidthVerifyLevel( p->pPlanes + lev0, lev0 ); + reoProfileWidthVerifyLevel( p->pPlanes + lev1, lev1 ); + + // compute the total gain in terms of width + nCostGain = (nNodesDownMovedUp - nNodesUpMovedDown + nNodesUnrefRemoved - nNodesUnrefAdded) + nWidthReduction; + // adjust the width on this level + p->pPlanes[lev1].statsWidth -= (int)nCostGain; + // set the cost + p->pPlanes[lev1].statsCost = p->pPlanes[lev1].statsWidth; + } + else if ( p->fMinApl ) + { + // compute the total gain in terms of APL + nCostGain = AplWeightPrev - AplWeightAfter; + // make sure that the ALP is updated correctly +// assert( p->pPlanes[lev0].statsCost + p->pPlanes[lev1].statsCost - nCostGain == +// AplWeightTotalLev0 + AplWeightTotalLev1 ); + // adjust the profile + p->pPlanes[lev0].statsApl = AplWeightTotalLev0; + p->pPlanes[lev1].statsApl = AplWeightTotalLev1; + // set the cost + p->pPlanes[lev0].statsCost = p->pPlanes[lev0].statsApl; + p->pPlanes[lev1].statsCost = p->pPlanes[lev1].statsApl; + } + else + { + // compute the total gain in terms of the number of nodes + nCostGain = nNodesUnrefRemoved - nNodesUnrefAdded; + // adjust the profile (adjusted above) + // set the cost + p->pPlanes[lev0].statsCost = p->pPlanes[lev0].statsNodes; + p->pPlanes[lev1].statsCost = p->pPlanes[lev1].statsNodes; + } + + return nCostGain; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + |