diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2012-11-01 02:53:09 -0700 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2012-11-01 02:53:09 -0700 |
commit | ce3f8cb1d11b7b39fa48f809baa1419e9984fe8c (patch) | |
tree | 0c77a969bcd9c04b29b5460dab4bb274db7452d5 /src | |
parent | 42e767c2943ee14fb85fec3fa1f45610dcc424bb (diff) | |
download | abc-ce3f8cb1d11b7b39fa48f809baa1419e9984fe8c.tar.gz abc-ce3f8cb1d11b7b39fa48f809baa1419e9984fe8c.tar.bz2 abc-ce3f8cb1d11b7b39fa48f809baa1419e9984fe8c.zip |
Improvements to the truth table computations.
Diffstat (limited to 'src')
-rw-r--r-- | src/base/abci/abcNpn.c | 4 | ||||
-rw-r--r-- | src/misc/util/utilTruth.h | 185 | ||||
-rw-r--r-- | src/opt/dau/dauCanon.c | 388 |
3 files changed, 451 insertions, 126 deletions
diff --git a/src/base/abci/abcNpn.c b/src/base/abci/abcNpn.c index 06732d2b..759d91b3 100644 --- a/src/base/abci/abcNpn.c +++ b/src/base/abci/abcNpn.c @@ -202,10 +202,10 @@ void Abc_TruthNpnPerform( Abc_TtStore_t * p, int NpnType, int fVerbose ) { for ( i = 0; i < p->nFuncs; i++ ) { - extern void Abc_TtConfactorTest( word * pTruth, int nVars, int i ); + extern void Abc_TtCofactorTest( word * pTruth, int nVars, int i ); if ( fVerbose ) printf( "%7d : ", i ); - Abc_TtConfactorTest( p->pFuncs[i], p->nVars, i ); + Abc_TtCofactorTest( p->pFuncs[i], p->nVars, i ); if ( fVerbose ) Extra_PrintHex( stdout, (unsigned *)p->pFuncs[i], p->nVars ), printf( "\n" ); } diff --git a/src/misc/util/utilTruth.h b/src/misc/util/utilTruth.h index 443ff061..236c0d62 100644 --- a/src/misc/util/utilTruth.h +++ b/src/misc/util/utilTruth.h @@ -943,43 +943,43 @@ static inline void Abc_TtSwapVars( word * pTruth, int nVars, int iVar, int jVar word * pMasks = PPMasks[iVar][jVar]; int shift = (1 << jVar) - (1 << iVar); pTruth[0] = (pTruth[0] & pMasks[0]) | ((pTruth[0] & pMasks[1]) << shift) | ((pTruth[0] & pMasks[2]) >> shift); + return; } - else + if ( jVar <= 5 ) { - if ( jVar <= 5 ) - { - word * pMasks = PPMasks[iVar][jVar]; - int nWords = Abc_TtWordNum(nVars); - int w, shift = (1 << jVar) - (1 << iVar); - for ( w = 0; w < nWords; w++ ) - pTruth[w] = (pTruth[w] & pMasks[0]) | ((pTruth[w] & pMasks[1]) << shift) | ((pTruth[w] & pMasks[2]) >> shift); - } - else if ( iVar <= 5 && jVar > 5 ) - { - word low2High, high2Low; - word * pLimit = pTruth + Abc_TtWordNum(nVars); - int j, jStep = Abc_TtWordNum(jVar); - int shift = 1 << iVar; - for ( ; pTruth < pLimit; pTruth += 2*jStep ) - for ( j = 0; j < jStep; j++ ) - { - low2High = (pTruth[j] & s_Truths6[iVar]) >> shift; - high2Low = (pTruth[j+jStep] << shift) & s_Truths6[iVar]; - pTruth[j] = (pTruth[j] & ~s_Truths6[iVar]) | high2Low; - pTruth[j+jStep] = (pTruth[j+jStep] & s_Truths6[iVar]) | low2High; - } - } - else - { - word * pLimit = pTruth + Abc_TtWordNum(nVars); - int i, iStep = Abc_TtWordNum(iVar); - int j, jStep = Abc_TtWordNum(jVar); - for ( ; pTruth < pLimit; pTruth += 2*jStep ) - for ( i = 0; i < jStep; i += 2*iStep ) - for ( j = 0; j < iStep; j++ ) - ABC_SWAP( word, pTruth[iStep + i + j], pTruth[jStep + i + j] ); - } + word * pMasks = PPMasks[iVar][jVar]; + int nWords = Abc_TtWordNum(nVars); + int w, shift = (1 << jVar) - (1 << iVar); + for ( w = 0; w < nWords; w++ ) + pTruth[w] = (pTruth[w] & pMasks[0]) | ((pTruth[w] & pMasks[1]) << shift) | ((pTruth[w] & pMasks[2]) >> shift); + return; + } + if ( iVar <= 5 && jVar > 5 ) + { + word low2High, high2Low; + word * pLimit = pTruth + Abc_TtWordNum(nVars); + int j, jStep = Abc_TtWordNum(jVar); + int shift = 1 << iVar; + for ( ; pTruth < pLimit; pTruth += 2*jStep ) + for ( j = 0; j < jStep; j++ ) + { + low2High = (pTruth[j] & s_Truths6[iVar]) >> shift; + high2Low = (pTruth[j+jStep] << shift) & s_Truths6[iVar]; + pTruth[j] = (pTruth[j] & ~s_Truths6[iVar]) | high2Low; + pTruth[j+jStep] = (pTruth[j+jStep] & s_Truths6[iVar]) | low2High; + } + return; } + { + word * pLimit = pTruth + Abc_TtWordNum(nVars); + int i, iStep = Abc_TtWordNum(iVar); + int j, jStep = Abc_TtWordNum(jVar); + for ( ; pTruth < pLimit; pTruth += 2*jStep ) + for ( i = 0; i < jStep; i += 2*iStep ) + for ( j = 0; j < iStep; j++ ) + ABC_SWAP( word, pTruth[iStep + i + j], pTruth[jStep + i + j] ); + return; + } } /**Function************************************************************* @@ -1037,16 +1037,18 @@ static inline void Abc_TtCountOnesInCofs( word * pTruth, int nVars, int * pStore { word Temp; int i, k, Counter, nWords; - memset( pStore, 0, sizeof(int) * nVars ); if ( nVars <= 6 ) { for ( i = 0; i < nVars; i++ ) if ( pTruth[0] & s_Truths6Neg[i] ) pStore[i] = Abc_TtCountOnes( pTruth[0] & s_Truths6Neg[i] ); + else + pStore[i] = 0; return; } assert( nVars > 6 ); nWords = Abc_TtWordNum( nVars ); + memset( pStore, 0, sizeof(int) * nVars ); for ( k = 0; k < nWords; k++ ) { // count 1's for the first six variables @@ -1110,16 +1112,21 @@ static inline void Abc_TtCountOnesInCofsSlow( word * pTruth, int nVars, int * pS SeeAlso [] ***********************************************************************/ -static inline unsigned Abc_TtSemiCanonicize( word * pTruth, int nVars, char * pCanonPerm ) +static inline unsigned Abc_TtSemiCanonicize( word * pTruth, int nVars, char * pCanonPerm, int * pStoreOut ) { extern int Abc_TtCountOnesInCofsFast( word * pTruth, int nVars, int * pStore ); - int pStore[16]; -// int pStore2[16]; + int fOldSwap = 0; + int pStoreIn[17]; + int * pStore = pStoreOut ? pStoreOut : pStoreIn; +// int pStore2[17]; int nWords = Abc_TtWordNum( nVars ); - int i, k, BestK, Temp, nOnes;//, nSwaps = 0;//, fChange; + int i, Temp, nOnes;//, fChange;//, nSwaps = 0;//; + int k, BestK; unsigned uCanonPhase = 0; assert( nVars <= 16 ); + for ( i = 0; i < nVars; i++ ) + pCanonPerm[i] = i; // normalize polarity nOnes = Abc_TtCountOnesInTruth( pTruth, nVars ); if ( nOnes > nWords * 32 ) @@ -1130,6 +1137,7 @@ static inline unsigned Abc_TtSemiCanonicize( word * pTruth, int nVars, char * pC } // normalize phase Abc_TtCountOnesInCofs( pTruth, nVars, pStore ); + pStore[nVars] = nOnes; // Abc_TtCountOnesInCofsFast( pTruth, nVars, pStore ); // Abc_TtCountOnesInCofsFast( pTruth, nVars, pStore2 ); @@ -1144,62 +1152,71 @@ static inline unsigned Abc_TtSemiCanonicize( word * pTruth, int nVars, char * pC uCanonPhase |= (1 << i); pStore[i] = nOnes - pStore[i]; } -/* - do { - fChange = 0; - for ( i = 0; i < nVars-1; i++ ) - { - if ( pStore[i] <= pStore[i+1] ) - continue; + + if ( fOldSwap ) + { + int fChange; + do { + fChange = 0; + for ( i = 0; i < nVars-1; i++ ) + { + // if ( pStore[i] <= pStore[i+1] ) + if ( pStore[i] >= pStore[i+1] ) + continue; - Temp = pCanonPerm[i]; - pCanonPerm[i] = pCanonPerm[i+1]; - pCanonPerm[i+1] = Temp; + Temp = pCanonPerm[i]; + pCanonPerm[i] = pCanonPerm[i+1]; + pCanonPerm[i+1] = Temp; - Temp = pStore[i]; - pStore[i] = pStore[i+1]; - pStore[i+1] = Temp; + Temp = pStore[i]; + pStore[i] = pStore[i+1]; + pStore[i+1] = Temp; - if ( ((uCanonPhase >> i) & 1) != ((uCanonPhase >> (i+1)) & 1) ) - { - uCanonPhase ^= (1 << i); - uCanonPhase ^= (1 << (i+1)); + if ( ((uCanonPhase >> i) & 1) != ((uCanonPhase >> (i+1)) & 1) ) + { + uCanonPhase ^= (1 << i); + uCanonPhase ^= (1 << (i+1)); + } + Abc_TtSwapAdjacent( pTruth, nWords, i ); + fChange = 1; + // nSwaps++; } - Abc_TtSwapAdjacent( pTruth, nWords, i ); - fChange = 1; -// nSwaps++; - } - } while ( fChange ); -*/ - - for ( i = 0; i < nVars - 1; i++ ) + } while ( fChange ); + } + else { - BestK = i + 1; - for ( k = i + 2; k < nVars; k++ ) - if ( pStore[BestK] > pStore[k] ) - BestK = k; - if ( pStore[BestK] >= pStore[i] ) - continue; + for ( i = 0; i < nVars - 1; i++ ) + { + BestK = i + 1; + for ( k = i + 2; k < nVars; k++ ) + // if ( pStore[BestK] > pStore[k] ) + if ( pStore[BestK] < pStore[k] ) + BestK = k; + // if ( pStore[i] <= pStore[BestK] ) + if ( pStore[i] >= pStore[BestK] ) + continue; - Temp = pCanonPerm[i]; - pCanonPerm[i] = pCanonPerm[BestK]; - pCanonPerm[BestK] = Temp; + Temp = pCanonPerm[i]; + pCanonPerm[i] = pCanonPerm[BestK]; + pCanonPerm[BestK] = Temp; - Temp = pStore[i]; - pStore[i] = pStore[BestK]; - pStore[BestK] = Temp; + Temp = pStore[i]; + pStore[i] = pStore[BestK]; + pStore[BestK] = Temp; - if ( ((uCanonPhase >> i) & 1) != ((uCanonPhase >> BestK) & 1) ) - { - uCanonPhase ^= (1 << i); - uCanonPhase ^= (1 << BestK); + if ( ((uCanonPhase >> i) & 1) != ((uCanonPhase >> BestK) & 1) ) + { + uCanonPhase ^= (1 << i); + uCanonPhase ^= (1 << BestK); + } + Abc_TtSwapVars( pTruth, nVars, i, BestK ); + // nSwaps++; } - Abc_TtSwapVars( pTruth, nVars, i, BestK ); -// nSwaps++; } -/* - printf( "%d ", nSwaps ); + +// printf( "%d ", nSwaps ); +/* printf( "Minterms: " ); for ( i = 0; i < nVars; i++ ) printf( "%d ", pStore[i] ); diff --git a/src/opt/dau/dauCanon.c b/src/opt/dau/dauCanon.c index 3ad44715..b66b276b 100644 --- a/src/opt/dau/dauCanon.c +++ b/src/opt/dau/dauCanon.c @@ -70,7 +70,7 @@ void Abc_TtReverseBypes() SeeAlso [] ***********************************************************************/ -void Abc_TtConfactorTest7( word * pTruth, int nVars, int N ) +void Abc_TtCofactorTest7( word * pTruth, int nVars, int N ) { word Cof[4][1024]; int i, nWords = Abc_TtWordNum( nVars ); @@ -125,7 +125,7 @@ void Abc_TtConfactorTest7( word * pTruth, int nVars, int N ) */ } } -void Abc_TtConfactorTest2( word * pTruth, int nVars, int N ) +void Abc_TtCofactorTest2( word * pTruth, int nVars, int N ) { // word Cof[4][1024]; int i, j, nWords = Abc_TtWordNum( nVars ); @@ -185,7 +185,7 @@ void Abc_TtConfactorTest2( word * pTruth, int nVars, int N ) */ } } -void Abc_TtConfactorTest3( word * pTruth, int nVars, int N ) +void Abc_TtCofactorTest3( word * pTruth, int nVars, int N ) { word Cof[4][1024]; int i, j, nWords = Abc_TtWordNum( nVars ); @@ -217,7 +217,7 @@ void Abc_TtConfactorTest3( word * pTruth, int nVars, int N ) } } -void Abc_TtConfactorTest4( word * pTruth, int nVars, int N ) +void Abc_TtCofactorTest4( word * pTruth, int nVars, int N ) { word Cof[4][1024]; int i, j, nWords = Abc_TtWordNum( nVars ); @@ -259,7 +259,7 @@ void Abc_TtConfactorTest4( word * pTruth, int nVars, int N ) } } -void Abc_TtConfactorTest6( word * pTruth, int nVars, int N ) +void Abc_TtCofactorTest6( word * pTruth, int nVars, int N ) { // word Cof[4][1024]; int i, nWords = Abc_TtWordNum( nVars ); @@ -304,12 +304,22 @@ void Abc_TtConfactorTest6( word * pTruth, int nVars, int N ) i = 0; } -int Abc_TtConfactorPermNaive( word * pTruth, int i, int nVars ) +int Abc_TtCofactorPermNaive( word * pTruth, int i, int nWords, int fSwapOnly ) { static word pCopy[1024]; static word pBest[1024]; - int nWords = Abc_TtWordNum( nVars ); + if ( fSwapOnly ) + { + Abc_TtCopy( pCopy, pTruth, nWords, 0 ); + Abc_TtSwapAdjacent( pCopy, nWords, i ); + if ( Abc_TtCompareRev(pTruth, pCopy, nWords) == 1 ) + { + Abc_TtCopy( pTruth, pCopy, nWords, 0 ); + return 1; + } + return 0; + } // save two copies Abc_TtCopy( pCopy, pTruth, nWords, 0 ); @@ -335,7 +345,7 @@ int Abc_TtConfactorPermNaive( word * pTruth, int i, int nVars ) // PXY // 110 - Abc_TtSwapVars( pCopy, nVars, i, i+1 ); + Abc_TtSwapAdjacent( pCopy, nWords, i ); if ( Abc_TtCompareRev(pBest, pCopy, nWords) == 1 ) Abc_TtCopy( pBest, pCopy, nWords, 0 ); @@ -359,76 +369,261 @@ int Abc_TtConfactorPermNaive( word * pTruth, int i, int nVars ) // PXY // 000 - Abc_TtSwapVars( pCopy, nVars, i, i+1 ); + Abc_TtSwapAdjacent( pCopy, nWords, i ); if ( Abc_TtCompareRev(pBest, pCopy, nWords) == 1 ) Abc_TtCopy( pBest, pCopy, nWords, 0 ); assert( Abc_TtEqual( pTruth, pCopy, nWords ) ); if ( Abc_TtEqual( pTruth, pBest, nWords ) ) return 0; + assert( Abc_TtCompareRev(pTruth, pBest, nWords) == 1 ); Abc_TtCopy( pTruth, pBest, nWords, 0 ); return 1; } -int Abc_TtConfactorPerm( word * pTruth, int i, int nVars ) +int Abc_TtCofactorPerm( word * pTruth, int i, int nWords, char * pCanonPerm, unsigned * puCanonPhase, int fSwapOnly ) { - int nWords = Abc_TtWordNum( nVars ); + static word pCopy1[1024]; int fComp01, fComp02, fComp03, fComp12, fComp13, fComp23; + unsigned uPhaseInit = *puCanonPhase; int RetValue = 0; - fComp23 = Abc_TtCompare2VarCofsRev( pTruth, nWords, i, 2, 3 ); + + if ( fSwapOnly ) + { + fComp12 = Abc_TtCompare2VarCofsRev( pTruth, nWords, i, 1, 2 ); + if ( fComp12 < 0 ) // Cof1 < Cof2 + { + Abc_TtSwapAdjacent( pTruth, nWords, i ); + RetValue = 1; + + if ( ((*puCanonPhase >> i) & 1) != ((*puCanonPhase >> (i+1)) & 1) ) + { + *puCanonPhase ^= (1 << i); + *puCanonPhase ^= (1 << (i+1)); + } + + ABC_SWAP( int, pCanonPerm[i], pCanonPerm[i+1] ); + } + return RetValue; + } + + Abc_TtCopy( pCopy1, pTruth, nWords, 0 ); + fComp01 = Abc_TtCompare2VarCofsRev( pTruth, nWords, i, 0, 1 ); - if ( fComp23 >= 1 ) // Cof2 >= Cof3 + fComp23 = Abc_TtCompare2VarCofsRev( pTruth, nWords, i, 2, 3 ); + if ( fComp23 >= 0 ) // Cof2 >= Cof3 { - if ( fComp01 >= 1 ) // Cof0 >= Cof1 + if ( fComp01 >= 0 ) // Cof0 >= Cof1 { fComp13 = Abc_TtCompare2VarCofsRev( pTruth, nWords, i, 1, 3 ); - if ( fComp13 < 1 ) // Cof1 < Cof3 ) - Abc_TtFlip( pTruth, nWords, i + 1 ), RetValue = 1; + if ( fComp13 < 0 ) // Cof1 < Cof3 + { + Abc_TtFlip( pTruth, nWords, i + 1 ); + *puCanonPhase ^= (1 << (i+1)); + RetValue = 1; + } + else if ( fComp13 == 0 ) // Cof1 == Cof3 + { + fComp02 = Abc_TtCompare2VarCofsRev( pTruth, nWords, i, 0, 2 ); + if ( fComp02 < 0 ) + { + Abc_TtFlip( pTruth, nWords, i + 1 ); + *puCanonPhase ^= (1 << (i+1)); + RetValue = 1; + } + } + // else Cof1 > Cof3 -- do nothing } else // Cof0 < Cof1 { fComp03 = Abc_TtCompare2VarCofsRev( pTruth, nWords, i, 0, 3 ); - if ( fComp03 < 1 ) // Cof0 < Cof3 ) + if ( fComp03 < 0 ) // Cof0 < Cof3 { Abc_TtFlip( pTruth, nWords, i ); - Abc_TtFlip( pTruth, nWords, i + 1 ), RetValue = 1; + Abc_TtFlip( pTruth, nWords, i + 1 ); + *puCanonPhase ^= (1 << i); + *puCanonPhase ^= (1 << (i+1)); + RetValue = 1; } - else // Cof0 >= Cof3 + else // Cof0 >= Cof3 { - if ( fComp23 == 0 ) - Abc_TtFlip( pTruth, nWords, i ), RetValue = 1; + if ( fComp23 == 0 ) // can flip Cof0 and Cof1 + { + Abc_TtFlip( pTruth, nWords, i ); + *puCanonPhase ^= (1 << i); + RetValue = 1; + } } } } else // Cof2 < Cof3 { - if ( fComp01 >= 1 ) // Cof0 >= Cof1 + if ( fComp01 >= 0 ) // Cof0 >= Cof1 { fComp12 = Abc_TtCompare2VarCofsRev( pTruth, nWords, i, 1, 2 ); - if ( fComp12 < 1 ) // Cof1 < Cof2 ) - Abc_TtFlip( pTruth, nWords, i + 1 ), RetValue = 1; + if ( fComp12 > 0 ) // Cof1 > Cof2 + { + Abc_TtFlip( pTruth, nWords, i ); + *puCanonPhase ^= (1 << i); + } + else if ( fComp12 == 0 ) // Cof1 == Cof2 + { + Abc_TtFlip( pTruth, nWords, i ); + Abc_TtFlip( pTruth, nWords, i + 1 ); + *puCanonPhase ^= (1 << i); + *puCanonPhase ^= (1 << (i+1)); + } + else // Cof1 < Cof2 + { + Abc_TtFlip( pTruth, nWords, i + 1 ); + *puCanonPhase ^= (1 << (i+1)); + if ( fComp01 == 0 ) + { + Abc_TtFlip( pTruth, nWords, i ); + *puCanonPhase ^= (1 << i); + } + } } else // Cof0 < Cof1 { fComp02 = Abc_TtCompare2VarCofsRev( pTruth, nWords, i, 0, 2 ); - if ( fComp02 == -1 ) // Cof0 < Cof2 ) + if ( fComp02 == -1 ) // Cof0 < Cof2 + { + Abc_TtFlip( pTruth, nWords, i ); Abc_TtFlip( pTruth, nWords, i + 1 ); - Abc_TtFlip( pTruth, nWords, i ), RetValue = 1; + *puCanonPhase ^= (1 << i); + *puCanonPhase ^= (1 << (i+1)); + } + else if ( fComp02 == 0 ) // Cof0 == Cof2 + { + fComp13 = Abc_TtCompare2VarCofsRev( pTruth, nWords, i, 1, 3 ); + if ( fComp13 >= 0 ) // Cof1 >= Cof3 + { + Abc_TtFlip( pTruth, nWords, i ); + *puCanonPhase ^= (1 << i); + } + else // Cof1 < Cof3 + { + Abc_TtFlip( pTruth, nWords, i ); + Abc_TtFlip( pTruth, nWords, i + 1 ); + *puCanonPhase ^= (1 << i); + *puCanonPhase ^= (1 << (i+1)); + } + } + else // Cof0 > Cof2 + { + Abc_TtFlip( pTruth, nWords, i ); + *puCanonPhase ^= (1 << i); + } } + RetValue = 1; } - // perform final swap if needed fComp12 = Abc_TtCompare2VarCofsRev( pTruth, nWords, i, 1, 2 ); - if ( fComp12 == 1 ) // Cof1 > Cof2 - Abc_TtSwapVars( pTruth, nVars, i, i+1 ), RetValue = 1; + if ( fComp12 < 0 ) // Cof1 < Cof2 + { + Abc_TtSwapAdjacent( pTruth, nWords, i ); + RetValue = 1; + + if ( ((*puCanonPhase >> i) & 1) != ((*puCanonPhase >> (i+1)) & 1) ) + { + *puCanonPhase ^= (1 << i); + *puCanonPhase ^= (1 << (i+1)); + } + + ABC_SWAP( int, pCanonPerm[i], pCanonPerm[i+1] ); + } + + if ( RetValue == 1 ) + { + if ( Abc_TtCompareRev(pTruth, pCopy1, nWords) == 1 ) // made it worse + { + Abc_TtCopy( pTruth, pCopy1, nWords, 0 ); + // undo the flips + *puCanonPhase = uPhaseInit; + // undo the swap + if ( fComp12 < 0 ) // Cof1 < Cof2 + ABC_SWAP( int, pCanonPerm[i], pCanonPerm[i+1] ); + RetValue = 0; + } + } return RetValue; } -void Abc_TtConfactorTest8( word * pTruth, int nVars, int N ) + +void Abc_TtCofactorTest__( word * pTruth, int nVars, int N ) +{ + char pCanonPerm[16]; + unsigned uCanonPhase; + static word pCopy1[1024]; + static word pCopy2[1024]; + int i, nWords = Abc_TtWordNum( nVars ); + static int Counter = 0; + +// pTruth[0] = (s_Truths6[0] & s_Truths6[1]) | s_Truths6[2]; +// nVars = 3; + +/* + printf( "\n" ); + Kit_DsdPrintFromTruth( pTruth, nVars ); printf( "\n" ); + Abc_TtPrintBinary( pTruth, nVars ); + printf( "\n" ); +*/ + +// for ( i = nVars - 2; i >= 0; i-- ) + for ( i = 3; i < nVars - 1; i++ ) + { +/* + word Cof0s = Abc_Tt6Cof0( pTruth[0], i+1 ); + word Cof1s = Abc_Tt6Cof1( pTruth[0], i+1 ); + + word Cof0 = Abc_Tt6Cof0( Cof0s, i ); + word Cof1 = Abc_Tt6Cof1( Cof0s, i ); + word Cof2 = Abc_Tt6Cof0( Cof1s, i ); + word Cof3 = Abc_Tt6Cof1( Cof1s, i ); + + Abc_TtPrintBinary( &Cof0, 6 ); + Abc_TtPrintBinary( &Cof1, 6 ); + Abc_TtPrintBinary( &Cof2, 6 ); + Abc_TtPrintBinary( &Cof3, 6 ); + + printf( "01 = %d\n", Abc_TtCompare2VarCofsRev(pTruth, nWords, i, 0, 1) ); + printf( "02 = %d\n", Abc_TtCompare2VarCofsRev(pTruth, nWords, i, 0, 2) ); + printf( "03 = %d\n", Abc_TtCompare2VarCofsRev(pTruth, nWords, i, 0, 3) ); + printf( "12 = %d\n", Abc_TtCompare2VarCofsRev(pTruth, nWords, i, 1, 2) ); + printf( "13 = %d\n", Abc_TtCompare2VarCofsRev(pTruth, nWords, i, 1, 3) ); + printf( "23 = %d\n", Abc_TtCompare2VarCofsRev(pTruth, nWords, i, 2, 3) ); + + if ( i == 0 && N == 74 ) + { + int s = 0; + continue; + } +*/ + Abc_TtCopy( pCopy1, pTruth, nWords, 0 ); + Abc_TtCofactorPermNaive( pCopy1, i, nWords, 0 ); + + Abc_TtCopy( pCopy2, pTruth, nWords, 0 ); + Abc_TtCofactorPerm( pCopy2, i, nWords, pCanonPerm, &uCanonPhase, 0 ); + +// assert( Abc_TtEqual( pCopy1, pCopy2, nWords ) ); + if ( !Abc_TtEqual( pCopy1, pCopy2, nWords ) ) + Counter++; + + } + if ( Counter % 1000 == 0 ) + printf( "%d ", Counter ); + +} + + + +void Abc_TtCofactorTest8( word * pTruth, int nVars, int N ) { int fVerbose = 0; int i; + int nWords = Abc_TtWordNum( nVars ); if ( fVerbose ) printf( "\n " ), Abc_TtPrintHex( pTruth, nVars ); @@ -437,7 +632,7 @@ void Abc_TtConfactorTest8( word * pTruth, int nVars, int N ) printf( "Round 1\n" ); for ( i = nVars - 2; i >= 0; i-- ) { - if ( Abc_TtConfactorPermNaive( pTruth, i, nVars ) ) + if ( Abc_TtCofactorPermNaive( pTruth, i, nWords, 0 ) ) { if ( fVerbose ) printf( "%d ", i ), Abc_TtPrintHex( pTruth, nVars ); @@ -448,7 +643,7 @@ void Abc_TtConfactorTest8( word * pTruth, int nVars, int N ) printf( "Round 2\n" ); for ( i = 0; i < nVars - 1; i++ ) { - if ( Abc_TtConfactorPermNaive( pTruth, i, nVars ) ) + if ( Abc_TtCofactorPermNaive( pTruth, i, nWords, 0 ) ) { if ( fVerbose ) printf( "%d ", i ), Abc_TtPrintHex( pTruth, nVars ); @@ -461,7 +656,7 @@ void Abc_TtConfactorTest8( word * pTruth, int nVars, int N ) printf( "Round 3\n" ); for ( i = nVars - 2; i >= 0; i-- ) { - if ( Abc_TtConfactorPermNaive( pTruth, i, nVars ) ) + if ( Abc_TtCofactorPermNaive( pTruth, i, nWords, 0 ) ) { if ( fVerbose ) printf( "%d ", i ), Abc_TtPrintHex( pTruth, nVars ); @@ -472,7 +667,7 @@ void Abc_TtConfactorTest8( word * pTruth, int nVars, int N ) printf( "Round 4\n" ); for ( i = 0; i < nVars - 1; i++ ) { - if ( Abc_TtConfactorPermNaive( pTruth, i, nVars ) ) + if ( Abc_TtCofactorPermNaive( pTruth, i, nWords, 0 ) ) { if ( fVerbose ) printf( "%d ", i ), Abc_TtPrintHex( pTruth, nVars ); @@ -481,7 +676,7 @@ void Abc_TtConfactorTest8( word * pTruth, int nVars, int N ) i = 0; } -void Abc_TtConfactorTest10( word * pTruth, int nVars, int N ) +void Abc_TtCofactorTest10( word * pTruth, int nVars, int N ) { static word pCopy1[1024]; static word pCopy2[1024]; @@ -505,24 +700,137 @@ void Abc_TtConfactorTest10( word * pTruth, int nVars, int N ) } -void Abc_TtConfactorTest( word * pTruth, int nVars, int N ) +void Abc_TtCofactorTest111( word * pTruth, int nVars, int N ) { char pCanonPerm[32]; -// static word pCopy1[1024]; + static word pCopy1[1024]; static word pCopy2[1024]; int nWords = Abc_TtWordNum( nVars ); // Kit_DsdPrintFromTruth( pTruth, nVars ); printf( "\n" ); -// Abc_TtCopy( pCopy1, pTruth, nWords, 0 ); + Abc_TtCopy( pCopy1, pTruth, nWords, 0 ); // Kit_TruthSemiCanonicize_Yasha( pCopy1, nVars, pCanonPerm ); // Kit_DsdPrintFromTruth( pCopy1, nVars ); printf( "\n" ); Abc_TtCopy( pCopy2, pTruth, nWords, 0 ); - Abc_TtSemiCanonicize( pCopy2, nVars, pCanonPerm ); + Abc_TtSemiCanonicize( pCopy2, nVars, pCanonPerm, NULL ); // Kit_DsdPrintFromTruth( pCopy2, nVars ); printf( "\n" ); -// assert( Abc_TtEqual( pCopy1, pCopy2, nWords ) ); + assert( Abc_TtEqual( pCopy1, pCopy2, nWords ) ); +} + + + + +void Abc_TtCofactorMinimize( word * pTruth, int nVars, int N ) +{ + char pCanonPerm[16]; + unsigned uCanonPhase; + int i, fVerbose = 0; + int nWords = Abc_TtWordNum( nVars ); + + if ( fVerbose ) + printf( "\n " ), Abc_TtPrintHex( pTruth, nVars ); + + if ( fVerbose ) + printf( "Round 1\n" ); + for ( i = nVars - 2; i >= 0; i-- ) + { + if ( Abc_TtCofactorPerm( pTruth, i, nWords, pCanonPerm, &uCanonPhase, 0 ) ) + { + if ( fVerbose ) + printf( "%d ", i ), Abc_TtPrintHex( pTruth, nVars ); + } + } + + if ( fVerbose ) + printf( "Round 2\n" ); + for ( i = 0; i < nVars - 1; i++ ) + { + if ( Abc_TtCofactorPerm( pTruth, i, nWords, pCanonPerm, &uCanonPhase, 0 ) ) + { + if ( fVerbose ) + printf( "%d ", i ), Abc_TtPrintHex( pTruth, nVars ); + } + } +} + + +void Abc_TtCofactorVerify( word * pTruth, int nVars, char * pCanonPerm, unsigned uCanonPhase ) +{ + int i, k, nWords = Abc_TtWordNum( nVars ); + if ( (uCanonPhase >> nVars) & 1 ) + Abc_TtNot( pTruth, nWords ); + for ( i = 0; i < nVars; i++ ) + if ( (uCanonPhase >> i) & 1 ) + Abc_TtFlip( pTruth, nWords, i ); + for ( i = 0; i < nVars; i++ ) + { + for ( k = i; k < nVars; k++ ) + if ( pCanonPerm[k] == i ) + break; + assert( k < nVars ); + if ( i == k ) + continue; + Abc_TtSwapVars( pTruth, nVars, i, k ); + ABC_SWAP( int, pCanonPerm[i], pCanonPerm[k] ); + } +} + +//#define CANON_VERIFY + +void Abc_TtCofactorTest( word * pTruth, int nVars, int N ) +{ + int pStoreIn[17]; + char pCanonPerm[16]; + unsigned uCanonPhase; + int i, nWords = Abc_TtWordNum( nVars ); + +#ifdef CANON_VERIFY + char pCanonPermCopy[16]; + static word pCopy1[1024]; + static word pCopy2[1024]; + Abc_TtCopy( pCopy1, pTruth, nWords, 0 ); +#endif + + uCanonPhase = Abc_TtSemiCanonicize( pTruth, nVars, pCanonPerm, pStoreIn ); + + for ( i = nVars - 2; i >= 0; i-- ) + if ( pStoreIn[i] == pStoreIn[i+1] ) + Abc_TtCofactorPerm( pTruth, i, nWords, pCanonPerm, &uCanonPhase, pStoreIn[i] != pStoreIn[nVars]/2 ); +// Abc_TtCofactorPermNaive( pTruth, i, nWords, pStoreIn[i] != pStoreIn[nVars]/2 ); + + for ( i = 1; i < nVars - 1; i++ ) + if ( pStoreIn[i] == pStoreIn[i+1] ) + Abc_TtCofactorPerm( pTruth, i, nWords, pCanonPerm, &uCanonPhase, pStoreIn[i] != pStoreIn[nVars]/2 ); +// Abc_TtCofactorPermNaive( pTruth, i, nWords, pStoreIn[i] != pStoreIn[nVars]/2 ); + + for ( i = nVars - 3; i >= 0; i-- ) + if ( pStoreIn[i] == pStoreIn[i+1] ) + Abc_TtCofactorPerm( pTruth, i, nWords, pCanonPerm, &uCanonPhase, pStoreIn[i] != pStoreIn[nVars]/2 ); +// Abc_TtCofactorPermNaive( pTruth, i, nWords, pStoreIn[i] != pStoreIn[nVars]/2 ); + + for ( i = 1; i < nVars - 1; i++ ) + if ( pStoreIn[i] == pStoreIn[i+1] ) + Abc_TtCofactorPerm( pTruth, i, nWords, pCanonPerm, &uCanonPhase, pStoreIn[i] != pStoreIn[nVars]/2 ); +// Abc_TtCofactorPermNaive( pTruth, i, nWords, pStoreIn[i] != pStoreIn[nVars]/2 ); + +#ifdef CANON_VERIFY + Abc_TtCopy( pCopy2, pTruth, nWords, 0 ); + memcpy( pCanonPermCopy, pCanonPerm, sizeof(char) * nVars ); + Abc_TtCofactorVerify( pCopy2, nVars, pCanonPermCopy, uCanonPhase ); + if ( !Abc_TtEqual( pCopy1, pCopy2, nWords ) ) + printf( "Canonical form verification failed!\n" ); +#endif +/* + if ( !Abc_TtEqual( pCopy1, pCopy2, nWords ) ) + { + Kit_DsdPrintFromTruth( pCopy1, nVars ); printf( "\n" ); + Kit_DsdPrintFromTruth( pCopy2, nVars ); printf( "\n" ); + i = 0; + } +*/ } |