diff options
Diffstat (limited to 'src/opt/fxu/fxuSingle.c')
-rw-r--r-- | src/opt/fxu/fxuSingle.c | 140 |
1 files changed, 129 insertions, 11 deletions
diff --git a/src/opt/fxu/fxuSingle.c b/src/opt/fxu/fxuSingle.c index 5af5c341..73d9a76c 100644 --- a/src/opt/fxu/fxuSingle.c +++ b/src/opt/fxu/fxuSingle.c @@ -17,13 +17,16 @@ ***********************************************************************/ #include "fxuInt.h" +#include "vec.h" //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// +static void Fxu_MatrixComputeSinglesOneCollect( Fxu_Matrix * p, Fxu_Var * pVar, Vec_Ptr_t * vSingles ); + //////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFITIONS /// +/// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// /**Function************************************************************* @@ -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 ); } |