From 8c302870f44d718261962d24e034ee19a8b6add8 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Mon, 3 Oct 2011 13:34:17 +0700 Subject: Changes to the matching procedure. --- src/map/if/ifDec16.c | 216 +++++++++++++++++++++++++++++++++++++++++++++++++-- 1 file changed, 210 insertions(+), 6 deletions(-) (limited to 'src/map/if/ifDec16.c') diff --git a/src/map/if/ifDec16.c b/src/map/if/ifDec16.c index a6d0edee..39881875 100644 --- a/src/map/if/ifDec16.c +++ b/src/map/if/ifDec16.c @@ -92,6 +92,15 @@ static inline int If_CluWordNum( int nVars ) { return nVars <= 6 ? 1 : 1 << (nVars-6); } +static inline int If_CluCountOnes( word t ) +{ + t = (t & 0x5555555555555555) + ((t>> 1) & 0x5555555555555555); + t = (t & 0x3333333333333333) + ((t>> 2) & 0x3333333333333333); + t = (t & 0x0F0F0F0F0F0F0F0F) + ((t>> 4) & 0x0F0F0F0F0F0F0F0F); + t = (t & 0x00FF00FF00FF00FF) + ((t>> 8) & 0x00FF00FF00FF00FF); + t = (t & 0x0000FFFF0000FFFF) + ((t>>16) & 0x0000FFFF0000FFFF); + return (t & 0x00000000FFFFFFFF) + (t>>32); +} int If_CluHashKey( word * pTruth, int nWords, int Size ) { static unsigned BigPrimes[8] = {12582917, 25165843, 50331653, 100663319, 201326611, 402653189, 805306457, 1610612741}; @@ -130,6 +139,22 @@ If_Grp_t * If_CluHashLookup( If_Man_t * p, word * pTruth ) ((If_Hte_t **)p->pHashTable)[HashKey] = pEntry; return &pEntry->Group; } +void If_CluHashPrintStats( If_Man_t * p ) +{ + If_Hte_t * pEntry; + int i, Counter; + for ( i = 0; i < p->nTableSize; i++ ) + { + Counter = 0; + for ( pEntry = ((If_Hte_t **)p->pHashTable)[i]; pEntry; pEntry = pEntry->pNext ) + Counter++; + if ( Counter == 0 ) + continue; + if ( Counter < 10 ) + continue; + printf( "%d=%d ", i, Counter ); + } +} // variable permutation for large functions static inline void If_CluClear( word * pIn, int nVars ) @@ -194,6 +219,18 @@ static inline word If_CluAdjust( word t, int nVars ) t |= t << (1<> Shift); + } + else + { + word Temp; + int i, k, Step = (1 << (iVar - 6)); + for ( k = 0; k < nWords; k += 2*Step ) + { + for ( i = 0; i < Step; i++ ) + { + Temp = pF[i]; + pF[i] = pF[Step+i]; + pF[Step+i] = Temp; + } + pF += 2*Step; + } + } +} +void If_CluCountOnesInCofs( word * pTruth, int nVars, int * pStore ) +{ + int nWords = If_CluWordNum( nVars ); + int i, k, nOnes = 0, Limit = Abc_MinInt( nVars, 6 ); + memset( pStore, 0, sizeof(int) * 2 * nVars ); + // compute positive cofactors + for ( k = 0; k < nWords; k++ ) + for ( i = 0; i < Limit; i++ ) + pStore[2*i+1] += If_CluCountOnes( pTruth[k] & Truth6[i] ); + if ( nVars > 6 ) + for ( k = 0; k < nWords; k++ ) + for ( i = 6; i < nVars; i++ ) + if ( k & (1 << (i-6)) ) + pStore[2*i+1] += If_CluCountOnes( pTruth[k] ); + // compute negative cofactors + for ( k = 0; k < nWords; k++ ) + nOnes += If_CluCountOnes( pTruth[k] ); + for ( i = 0; i < nVars; i++ ) + pStore[2*i] = nOnes - pStore[2*i+1]; +} +unsigned If_CluSemiCanonicize( word * pTruth, int nVars, int * pCanonPerm ) +{ + word pFunc[CLU_WRD_MAX], * pIn = pTruth, * pOut = pFunc, * pTemp; + int pStore[CLU_VAR_MAX*2]; + unsigned uCanonPhase = 0; + int i, Temp, fChange, Counter = 0; +//Kit_DsdPrintFromTruth( (unsigned*)pTruth, nVars ); printf( "\n" ); + + // collect signatures + If_CluCountOnesInCofs( pTruth, nVars, pStore ); + // canonicize phase + for ( i = 0; i < nVars; i++ ) + { + if ( pStore[2*i+0] <= pStore[2*i+1] ) + continue; + uCanonPhase |= (1 << i); + Temp = pStore[2*i+0]; + pStore[2*i+0] = pStore[2*i+1]; + pStore[2*i+1] = Temp; + If_CluChangePhase( pIn, nVars, i ); + } + // compute permutation + for ( i = 0; i < nVars; i++ ) + pCanonPerm[i] = i; + do { + fChange = 0; + for ( i = 0; i < nVars-1; i++ ) + { + if ( pStore[2*i] <= pStore[2*(i+1)] ) + continue; + Counter++; + fChange = 1; + + Temp = pCanonPerm[i]; + pCanonPerm[i] = pCanonPerm[i+1]; + pCanonPerm[i+1] = Temp; + + Temp = pStore[2*i]; + pStore[2*i] = pStore[2*(i+1)]; + pStore[2*(i+1)] = Temp; + + Temp = pStore[2*i+1]; + pStore[2*i+1] = pStore[2*(i+1)+1]; + pStore[2*(i+1)+1] = Temp; + + If_CluSwapAdjacent( pOut, pIn, i, nVars ); + pTemp = pIn; pIn = pOut; pOut = pTemp; + } + } while ( fChange ); + // swap if it was moved an odd number of times + if ( Counter & 1 ) + If_CluCopy( pOut, pIn, nVars ); + return uCanonPhase; +} +void If_CluSemiCanonicizeVerify( word * pTruth, word * pTruth0, int nVars, int * pCanonPerm, unsigned uCanonPhase ) +{ + word pFunc[CLU_WRD_MAX], pGunc[CLU_WRD_MAX], * pIn = pTruth, * pOut = pFunc, * pTemp; + int i, Temp, fChange, Counter = 0; + If_CluCopy( pGunc, pTruth, nVars ); + // undo permutation + do { + fChange = 0; + for ( i = 0; i < nVars-1; i++ ) + { + if ( pCanonPerm[i] < pCanonPerm[i+1] ) + continue; + + Counter++; + fChange = 1; + + Temp = pCanonPerm[i]; + pCanonPerm[i] = pCanonPerm[i+1]; + pCanonPerm[i+1] = Temp; + + If_CluSwapAdjacent( pOut, pIn, i, nVars ); + pTemp = pIn; pIn = pOut; pOut = pTemp; + } + } while ( fChange ); + if ( Counter & 1 ) + If_CluCopy( pOut, pIn, nVars ); + // undo phase + for ( i = 0; i < nVars; i++ ) + if ( (uCanonPhase >> i) & 1 ) + If_CluChangePhase( pTruth, nVars, i ); + // compare + if ( !If_CluEqual(pTruth0, pTruth, nVars) ) + { + Kit_DsdPrintFromTruth( (unsigned*)pTruth0, nVars ); printf( "\n" ); + Kit_DsdPrintFromTruth( (unsigned*)pGunc, nVars ); printf( "\n" ); + Kit_DsdPrintFromTruth( (unsigned*)pTruth, nVars ); printf( "\n" ); + printf( "SemiCanonical verification FAILED!\n" ); + } +} + + void If_CluPrintGroup( If_Grp_t * g ) { int i; @@ -898,15 +1076,28 @@ static inline int If_CluSupport( word * t, int nVars ) } // returns the best group found -If_Grp_t If_CluCheck( If_Man_t * p, word * pTruth, int nVars, int nLutLeaf, int nLutRoot ) +If_Grp_t If_CluCheck( If_Man_t * p, word * pTruth0, int nVars, int nLutLeaf, int nLutRoot ) { If_Grp_t G1 = {0}, R = {0}, * pHashed = NULL; - word Truth, pF[CLU_WRD_MAX];//, pG[CLU_WRD_MAX]; - int V2P[CLU_VAR_MAX+2], P2V[CLU_VAR_MAX+2]; - int i, nSupp; + word Truth, pTruth[CLU_WRD_MAX], pF[CLU_WRD_MAX];//, pG[CLU_WRD_MAX]; + int V2P[CLU_VAR_MAX+2], P2V[CLU_VAR_MAX+2], pCanonPerm[CLU_VAR_MAX]; + int i, nSupp, uCanonPhase; assert( nVars <= CLU_VAR_MAX ); assert( nVars <= nLutLeaf + nLutRoot - 1 ); + // canonicize truth table + If_CluCopy( pTruth, pTruth0, p->pPars->nLutSize ); + + if ( 0 ) + { + uCanonPhase = If_CluSemiCanonicize( pTruth, nVars, pCanonPerm ); + If_CluAdjustBig( pTruth, nVars, p->pPars->nLutSize ); + } + +// If_CluSemiCanonicizeVerify( pTruth, pTruth0, nVars, pCanonPerm, uCanonPhase ); +// If_CluCopy( pTruth, pTruth0, p->pPars->nLutSize ); + + /* { int pCanonPerm[32]; @@ -929,6 +1120,8 @@ If_Grp_t If_CluCheck( If_Man_t * p, word * pTruth, int nVars, int nLutLeaf, int if ( !nSupp || !If_CluSuppIsMinBase(nSupp) ) return G1; + + // check hash table pHashed = If_CluHashLookup( p, pTruth ); if ( pHashed && pHashed->nVars != CLU_UNUSED ) @@ -1161,14 +1354,25 @@ void If_CluTest() // word t = 0x0100200000000001; // word t2[4] = { 0x0000800080008000, 0x8000000000008000, 0x8000000080008000, 0x0000000080008000 }; // word t = 0x07770FFF07770FFF; -// word t = 0x002000D000D00020; + word t = 0x002000D000D00020; // word t = 0x000F000E000F000F; - word t = 0xF7FFF7F7F7F7F7F7; +// word t = 0xF7FFF7F7F7F7F7F7; + word s = t; int nVars = 6; int nLutLeaf = 4; int nLutRoot = 4; If_Grp_t G; +/* + int pCanonPerm[CLU_VAR_MAX]; + int uCanonPhase; + + Kit_DsdPrintFromTruth( (unsigned*)&s, nVars ); printf( "\n" ); + uCanonPhase = If_CluSemiCanonicize( &s, nVars, pCanonPerm ); + Kit_DsdPrintFromTruth( (unsigned*)&s, nVars ); printf( "\n" ); + + If_CluSemiCanonicizeVerify( &s, &t, nVars, pCanonPerm, uCanonPhase ); +*/ return; If_CutPerformCheck07( NULL, (unsigned *)&t, 6, 6, NULL ); -- cgit v1.2.3