src/bdd/reo/reoSwap.c

Go to the documentation of this file.

#include "reo.h"


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


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;
}

---