Version abc70930

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