reoswap.c

主要进行大规模的电路综合

			//            /       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 == (unsigned)pNew1E && p->HTable[HKey].Arg2 == (unsigned)pNew1T )
			{ // the entry is present 
				// assign this entry
				pNewPlane20 = (reo_unit *)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 = (unsigned)pNew1E;
				p->HTable[HKey].Arg2 = (unsigned)pNew1T;
				p->HTable[HKey].Arg3 = (unsigned)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 == (unsigned)pNew2E && p->HTable[HKey].Arg2 == (unsigned)pNew2T )
			{ // the entry is present 
				// assign this entry
				pNewPlane21 = (reo_unit *)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 = (unsigned)pNew2E;
				p->HTable[HKey].Arg2 = (unsigned)pNew2T;
				p->HTable[HKey].Arg3 = (unsigned)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                              ///
////////////////////////////////////////////////////////////////////////