path: root/src/bdd/reo/reoSwap.c

/**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"

ABC_NAMESPACE_IMPL_START


////////////////////////////////////////////////////////////////////////
///                        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 = NULL, * pNewPlane21 = NULL; // Suppress "might be used uninitialized"
        reo_unit * 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, HKey, fInteract, temp, c;
        int nWidthCofs = -1; // Suppress "might be used uninitialized"
    // statistical variables
    int nNodesUpMovedDown  = 0;
    int nNodesDownMovedUp  = 0;
    int nNodesUnrefRemoved = 0;
    int nNodesUnrefAdded   = 0;
    int nWidthReduction    = 0;
    double AplWeightTotalLev0 = 0.0; // Suppress "might be used uninitialized"
    double AplWeightTotalLev1 = 0.0; // Suppress "might be used uninitialized"
    double AplWeightHalf      = 0.0; // Suppress "might be used uninitialized"
    double AplWeightPrev      = 0.0; // Suppress "might be used uninitialized"
    double AplWeightAfter     = 0.0; // Suppress "might be used uninitialized"
    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                              ///
////////////////////////////////////////////////////////////////////////

ABC_NAMESPACE_IMPL_END