diff options
Diffstat (limited to 'src/bdd/reo/reoSwap.c')
-rw-r--r-- | src/bdd/reo/reoSwap.c | 898 |
1 files changed, 0 insertions, 898 deletions
diff --git a/src/bdd/reo/reoSwap.c b/src/bdd/reo/reoSwap.c deleted file mode 100644 index 4afa650c..00000000 --- a/src/bdd/reo/reoSwap.c +++ /dev/null @@ -1,898 +0,0 @@ -/**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 /// -//////////////////////////////////////////////////////////////////////// - |