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