diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2007-08-28 08:01:00 -0700 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2007-08-28 08:01:00 -0700 |
commit | ddc6d1c1682a18e293399b7d6c9f4a9018c30c70 (patch) | |
tree | 165c2a7ebb0561d9272673ce8caaa012f82d4717 /src/opt | |
parent | 28467823812f63a40f9a322b1fefc7decce4b766 (diff) | |
download | abc-ddc6d1c1682a18e293399b7d6c9f4a9018c30c70.tar.gz abc-ddc6d1c1682a18e293399b7d6c9f4a9018c30c70.tar.bz2 abc-ddc6d1c1682a18e293399b7d6c9f4a9018c30c70.zip |
Version abc70828
Diffstat (limited to 'src/opt')
-rw-r--r-- | src/opt/fxu/fxu.c | 14 | ||||
-rw-r--r-- | src/opt/fxu/fxu.h | 3 | ||||
-rw-r--r-- | src/opt/fxu/fxuCreate.c | 21 | ||||
-rw-r--r-- | src/opt/fxu/fxuInt.h | 4 | ||||
-rw-r--r-- | src/opt/fxu/fxuSingle.c | 138 | ||||
-rw-r--r-- | src/opt/fxu/fxuUpdate.c | 3 |
6 files changed, 161 insertions, 22 deletions
diff --git a/src/opt/fxu/fxu.c b/src/opt/fxu/fxu.c index a92ef934..d11fd793 100644 --- a/src/opt/fxu/fxu.c +++ b/src/opt/fxu/fxu.c @@ -58,6 +58,7 @@ int Fxu_FastExtract( Fxu_Data_t * pData ) Fxu_Single * pSingle; Fxu_Double * pDouble; int Weight1, Weight2, Weight3; + int Counter = 0; s_MemoryTotal = 0; s_MemoryPeak = 0; @@ -77,7 +78,7 @@ int Fxu_FastExtract( Fxu_Data_t * pData ) { Weight1 = Fxu_HeapSingleReadMaxWeight( p->pHeapSingle ); if ( pData->fVerbose ) - printf( "Best single = %3d.\n", Weight1 ); + printf( "Div %5d : Best single = %5d.\r", Counter++, Weight1 ); if ( Weight1 > 0 || Weight1 == 0 && pData->fUse0 ) Fxu_UpdateSingle( p ); else @@ -92,7 +93,7 @@ int Fxu_FastExtract( Fxu_Data_t * pData ) { Weight2 = Fxu_HeapDoubleReadMaxWeight( p->pHeapDouble ); if ( pData->fVerbose ) - printf( "Best double = %3d.\n", Weight2 ); + printf( "Div %5d : Best double = %5d.\r", Counter++, Weight2 ); if ( Weight2 > 0 || Weight2 == 0 && pData->fUse0 ) Fxu_UpdateDouble( p ); else @@ -109,7 +110,7 @@ int Fxu_FastExtract( Fxu_Data_t * pData ) Weight2 = Fxu_HeapDoubleReadMaxWeight( p->pHeapDouble ); if ( pData->fVerbose ) - printf( "Best double = %3d. Best single = %3d.\n", Weight2, Weight1 ); + printf( "Div %5d : Best double = %5d. Best single = %5d.\r", Counter++, Weight2, Weight1 ); //Fxu_Select( p, &pSingle, &pDouble ); if ( Weight1 >= Weight2 ) @@ -140,8 +141,8 @@ int Fxu_FastExtract( Fxu_Data_t * pData ) // select the best single and double Weight3 = Fxu_Select( p, &pSingle, &pDouble ); if ( pData->fVerbose ) - printf( "Best double = %3d. Best single = %3d. Best complement = %3d.\n", - Weight2, Weight1, Weight3 ); + printf( "Div %5d : Best double = %5d. Best single = %5d. Best complement = %5d.\r", + Counter++, Weight2, Weight1, Weight3 ); if ( Weight3 > 0 || Weight3 == 0 && pData->fUse0 ) Fxu_Update( p, pSingle, pDouble ); @@ -152,7 +153,8 @@ int Fxu_FastExtract( Fxu_Data_t * pData ) } if ( pData->fVerbose ) - printf( "Total single = %3d. Total double = %3d. Total compl = %3d.\n", p->nDivs1, p->nDivs2, p->nDivs3 ); + printf( "Total single = %3d. Total double = %3d. Total compl = %3d. \n", + p->nDivs1, p->nDivs2, p->nDivs3 ); // create the new covers if ( pData->nNodesNew ) diff --git a/src/opt/fxu/fxu.h b/src/opt/fxu/fxu.h index 7025d019..e6d0b69e 100644 --- a/src/opt/fxu/fxu.h +++ b/src/opt/fxu/fxu.h @@ -55,7 +55,8 @@ struct FxuDataStruct bool fUseCompl; // set to 1 to have complement taken into account bool fVerbose; // set to 1 to have verbose output int nNodesExt; // the number of divisors to extract - int nPairsMax; // the maximum number of cube pairs to consider + int nSingleMax; // the max number of single-cube divisors to consider + int nPairsMax; // the max number of double-cube divisors to consider // the input information Vec_Ptr_t * vSops; // the SOPs for each node in the network Vec_Ptr_t * vFanins; // the fanins of each node in the network diff --git a/src/opt/fxu/fxuCreate.c b/src/opt/fxu/fxuCreate.c index 99942a88..e3300df9 100644 --- a/src/opt/fxu/fxuCreate.c +++ b/src/opt/fxu/fxuCreate.c @@ -178,12 +178,26 @@ Fxu_Matrix * Fxu_CreateMatrix( Fxu_Data_t * pData ) // consider the case when cube pairs should be preprocessed // before adding them to the set of divisors +// if ( pData->fVerbose ) +// printf( "The total number of cube pairs is %d.\n", nPairsTotal ); + if ( nPairsTotal > 10000000 ) + { + printf( "The total number of cube pairs of the network is more than 10,000,000.\n" ); + printf( "Command \"fx\" takes a long time to run in such cases. It is suggested\n" ); + printf( "that the user changes the network by reducing the size of logic node and\n" ); + printf( "consequently the number of cube pairs to be processed by this command.\n" ); + printf( "One way to achieve this is to run the commands \"st; multi -m -F <num>\"\n" ); + printf( "as a proprocessing step, while selecting <num> as approapriate.\n" ); + return NULL; + } if ( nPairsTotal > pData->nPairsMax ) if ( !Fxu_PreprocessCubePairs( p, pData->vSops, nPairsTotal, pData->nPairsMax ) ) return NULL; +// if ( pData->fVerbose ) +// printf( "Only %d best cube pairs will be used by the fast extract command.\n", pData->nPairsMax ); // add the var pairs to the heap - Fxu_MatrixComputeSingles( p ); + Fxu_MatrixComputeSingles( p, pData->fUse0, pData->nSingleMax ); // print stats if ( pData->fVerbose ) @@ -194,9 +208,8 @@ Fxu_Matrix * Fxu_CreateMatrix( Fxu_Data_t * pData ) p->lVars.nItems, p->lCubes.nItems ); fprintf( stdout, "Lits = %d Density = %.5f%%\n", p->nEntries, Density ); - fprintf( stdout, "1-cube divisors = %6d. ", p->lSingles.nItems ); - fprintf( stdout, "2-cube divisors = %6d. ", p->nDivsTotal ); - fprintf( stdout, "Cube pairs = %6d.", nPairsTotal ); + fprintf( stdout, "1-cube divs = %6d. (Total = %6d) ", p->lSingles.nItems, p->nSingleTotal ); + fprintf( stdout, "2-cube divs = %6d. (Total = %6d)", p->nDivsTotal, nPairsTotal ); fprintf( stdout, "\n" ); } // Fxu_MatrixPrint( stdout, p ); diff --git a/src/opt/fxu/fxuInt.h b/src/opt/fxu/fxuInt.h index 0ae1d79e..ea85cb79 100644 --- a/src/opt/fxu/fxuInt.h +++ b/src/opt/fxu/fxuInt.h @@ -172,6 +172,8 @@ struct FxuMatrix // ~ 30 words // the single cube divisors Fxu_ListSingle lSingles; // the linked list of single cube divisors Fxu_HeapSingle * pHeapSingle; // the heap of variables by the number of literals in the matrix + int nWeightLimit;// the limit on weight of single cube divisors collected + int nSingleTotal;// the total number of single cube divisors // storage for cube pairs Fxu_Pair *** pppPairs; Fxu_Pair ** ppPairs; @@ -459,7 +461,7 @@ extern void Fxu_PairClearStorage( Fxu_Cube * pCube ); extern Fxu_Pair * Fxu_PairAlloc( Fxu_Matrix * p, Fxu_Cube * pCube1, Fxu_Cube * pCube2 ); extern void Fxu_PairAdd( Fxu_Pair * pPair ); /*===== fxuSingle.c ====================================================*/ -extern void Fxu_MatrixComputeSingles( Fxu_Matrix * p ); +extern void Fxu_MatrixComputeSingles( Fxu_Matrix * p, int fUse0, int nSingleMax ); extern void Fxu_MatrixComputeSinglesOne( Fxu_Matrix * p, Fxu_Var * pVar ); extern int Fxu_SingleCountCoincidence( Fxu_Matrix * p, Fxu_Var * pVar1, Fxu_Var * pVar2 ); /*===== fxuMatrix.c ====================================================*/ diff --git a/src/opt/fxu/fxuSingle.c b/src/opt/fxu/fxuSingle.c index be90e159..73d9a76c 100644 --- a/src/opt/fxu/fxuSingle.c +++ b/src/opt/fxu/fxuSingle.c @@ -17,11 +17,14 @@ ***********************************************************************/ #include "fxuInt.h" +#include "vec.h" //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// +static void Fxu_MatrixComputeSinglesOneCollect( Fxu_Matrix * p, Fxu_Var * pVar, Vec_Ptr_t * vSingles ); + //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// @@ -38,12 +41,130 @@ SeeAlso [] ***********************************************************************/ -void Fxu_MatrixComputeSingles( Fxu_Matrix * p ) +void Fxu_MatrixComputeSingles( Fxu_Matrix * p, int fUse0, int nSingleMax ) { Fxu_Var * pVar; - // iterate through the columns in the matrix + Vec_Ptr_t * vSingles; + int i, k; + // set the weight limit + p->nWeightLimit = 1 - fUse0; + // iterate through columns in the matrix and collect single-cube divisors + vSingles = Vec_PtrAlloc( 10000 ); Fxu_MatrixForEachVariable( p, pVar ) - Fxu_MatrixComputeSinglesOne( p, pVar ); + Fxu_MatrixComputeSinglesOneCollect( p, pVar, vSingles ); + p->nSingleTotal = Vec_PtrSize(vSingles) / 3; + // check if divisors should be filtered + if ( Vec_PtrSize(vSingles) > nSingleMax ) + { + int * pWeigtCounts, nDivCount, Weight, i, c;; + assert( Vec_PtrSize(vSingles) % 3 == 0 ); + // count how many divisors have the given weight + pWeigtCounts = ALLOC( int, 1000 ); + memset( pWeigtCounts, 0, sizeof(int) * 1000 ); + for ( i = 2; i < Vec_PtrSize(vSingles); i += 3 ) + { + Weight = (int)Vec_PtrEntry(vSingles, i); + if ( Weight >= 999 ) + pWeigtCounts[999]++; + else + pWeigtCounts[Weight]++; + } + // select the bound on the weight (above this bound, singles will be included) + nDivCount = 0; + for ( c = 999; c >= 0; c-- ) + { + nDivCount += pWeigtCounts[c]; + if ( nDivCount >= nSingleMax ) + break; + } + free( pWeigtCounts ); + // collect singles with the given costs + k = 0; + for ( i = 2; i < Vec_PtrSize(vSingles); i += 3 ) + { + Weight = (int)Vec_PtrEntry(vSingles, i); + if ( Weight < c ) + continue; + Vec_PtrWriteEntry( vSingles, k++, Vec_PtrEntry(vSingles, i-2) ); + Vec_PtrWriteEntry( vSingles, k++, Vec_PtrEntry(vSingles, i-1) ); + Vec_PtrWriteEntry( vSingles, k++, Vec_PtrEntry(vSingles, i) ); + if ( k/3 == nSingleMax ) + break; + } + Vec_PtrShrink( vSingles, k ); + // adjust the weight limit + p->nWeightLimit = c; + } + // collect the selected divisors + assert( Vec_PtrSize(vSingles) % 3 == 0 ); + for ( i = 0; i < Vec_PtrSize(vSingles); i += 3 ) + { + Fxu_MatrixAddSingle( p, + Vec_PtrEntry(vSingles,i), + Vec_PtrEntry(vSingles,i+1), + (int)Vec_PtrEntry(vSingles,i+2) ); + } + Vec_PtrFree( vSingles ); +} + +/**Function************************************************************* + + Synopsis [Adds the single-cube divisors associated with a new column.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fxu_MatrixComputeSinglesOneCollect( Fxu_Matrix * p, Fxu_Var * pVar, Vec_Ptr_t * vSingles ) +{ + Fxu_Lit * pLitV, * pLitH; + Fxu_Var * pVar2; + int Coin; + int WeightCur; + + // start collecting the affected vars + Fxu_MatrixRingVarsStart( p ); + // go through all the literals of this variable + for ( pLitV = pVar->lLits.pHead; pLitV; pLitV = pLitV->pVNext ) + // for this literal, go through all the horizontal literals + for ( pLitH = pLitV->pHPrev; pLitH; pLitH = pLitH->pHPrev ) + { + // get another variable + pVar2 = pLitH->pVar; + // skip the var if it is already used + if ( pVar2->pOrder ) + continue; + // skip the var if it belongs to the same node +// if ( pValue2Node[pVar->iVar] == pValue2Node[pVar2->iVar] ) +// continue; + // collect the var + Fxu_MatrixRingVarsAdd( p, pVar2 ); + } + // stop collecting the selected vars + Fxu_MatrixRingVarsStop( p ); + + // iterate through the selected vars + Fxu_MatrixForEachVarInRing( p, pVar2 ) + { + // count the coincidence + Coin = Fxu_SingleCountCoincidence( p, pVar2, pVar ); + assert( Coin > 0 ); + // get the new weight + WeightCur = Coin - 2; + // peformance fix (August 24, 2007) + if ( WeightCur >= p->nWeightLimit ) + { + Vec_PtrPush( vSingles, pVar2 ); + Vec_PtrPush( vSingles, pVar ); + Vec_PtrPush( vSingles, (void *)WeightCur ); + } + } + + // unmark the vars + Fxu_MatrixRingVarsUnmark( p ); } /**Function************************************************************* @@ -59,12 +180,9 @@ void Fxu_MatrixComputeSingles( Fxu_Matrix * p ) ***********************************************************************/ void Fxu_MatrixComputeSinglesOne( Fxu_Matrix * p, Fxu_Var * pVar ) { -// int * pValue2Node = p->pValue2Node; Fxu_Lit * pLitV, * pLitH; Fxu_Var * pVar2; int Coin; -// int CounterAll; -// int CounterTest; int WeightCur; // start collecting the affected vars @@ -76,7 +194,6 @@ void Fxu_MatrixComputeSinglesOne( Fxu_Matrix * p, Fxu_Var * pVar ) { // get another variable pVar2 = pLitH->pVar; -// CounterAll++; // skip the var if it is already used if ( pVar2->pOrder ) continue; @@ -92,16 +209,17 @@ void Fxu_MatrixComputeSinglesOne( Fxu_Matrix * p, Fxu_Var * pVar ) // iterate through the selected vars Fxu_MatrixForEachVarInRing( p, pVar2 ) { -// CounterTest++; // count the coincidence Coin = Fxu_SingleCountCoincidence( p, pVar2, pVar ); assert( Coin > 0 ); // get the new weight WeightCur = Coin - 2; - if ( WeightCur >= 0 ) + // peformance fix (August 24, 2007) +// if ( WeightCur >= 0 ) +// Fxu_MatrixAddSingle( p, pVar2, pVar, WeightCur ); + if ( WeightCur >= p->nWeightLimit ) Fxu_MatrixAddSingle( p, pVar2, pVar, WeightCur ); } - // unmark the vars Fxu_MatrixRingVarsUnmark( p ); } diff --git a/src/opt/fxu/fxuUpdate.c b/src/opt/fxu/fxuUpdate.c index a430b9c1..274f79f6 100644 --- a/src/opt/fxu/fxuUpdate.c +++ b/src/opt/fxu/fxuUpdate.c @@ -757,12 +757,14 @@ void Fxu_UpdateCleanOldSingles( Fxu_Matrix * p ) { Fxu_Single * pSingle, * pSingle2; int WeightNew; + int Counter = 0; Fxu_MatrixForEachSingleSafe( p, pSingle, pSingle2 ) { // if at least one of the variables is marked, recalculate if ( pSingle->pVar1->pOrder || pSingle->pVar2->pOrder ) { + Counter++; // get the new weight WeightNew = -2 + Fxu_SingleCountCoincidence( p, pSingle->pVar1, pSingle->pVar2 ); if ( WeightNew >= 0 ) @@ -778,6 +780,7 @@ void Fxu_UpdateCleanOldSingles( Fxu_Matrix * p ) } } } +// printf( "Called procedure %d times.\n", Counter ); } /**Function************************************************************* |