diff options
-rw-r--r-- | src/base/abci/abc.c | 1 | ||||
-rw-r--r-- | src/base/abci/abcNpn.c | 18 | ||||
-rw-r--r-- | src/misc/util/utilTruth.h | 531 | ||||
-rw-r--r-- | src/opt/dau/dau.h | 69 | ||||
-rw-r--r-- | src/opt/dau/dauCanon.c | 1370 |
5 files changed, 889 insertions, 1100 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index b973aba7..3b6746ed 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -4937,6 +4937,7 @@ usage: Abc_Print( -2, "\t 2: semi-canonical form by counting 1s in cofactors\n" ); Abc_Print( -2, "\t 3: Jake's hybrid semi-canonical form (fast)\n" ); Abc_Print( -2, "\t 4: Jake's hybrid semi-canonical form (high-effort)\n" ); + Abc_Print( -2, "\t 5: new fast hybrid semi-canonical form\n" ); Abc_Print( -2, "\t-N <num> : the number of support variables (binary files only) [default = unused]\n" ); Abc_Print( -2, "\t-d : toggle dumping resulting functions into a file [default = %s]\n", fDumpRes? "yes": "no" ); Abc_Print( -2, "\t-b : toggle dumping in binary format [default = %s]\n", fBinary? "yes": "no" ); diff --git a/src/base/abci/abcNpn.c b/src/base/abci/abcNpn.c index 759d91b3..ffcf00f7 100644 --- a/src/base/abci/abcNpn.c +++ b/src/base/abci/abcNpn.c @@ -23,6 +23,7 @@ #include "bool/kit/kit.h" #include "bool/lucky/lucky.h" +#include "opt/dau/dau.h" ABC_NAMESPACE_IMPL_START @@ -190,6 +191,8 @@ void Abc_TruthNpnPerform( Abc_TtStore_t * p, int NpnType, int fVerbose ) pAlgoName = "Jake's hybrid fast "; else if ( NpnType == 4 ) pAlgoName = "Jake's hybrid good "; + else if ( NpnType == 5 ) + pAlgoName = "new hybrid fast "; assert( p->nVars <= 16 ); if ( pAlgoName ) @@ -202,10 +205,8 @@ void Abc_TruthNpnPerform( Abc_TtStore_t * p, int NpnType, int fVerbose ) { for ( i = 0; i < p->nFuncs; i++ ) { - extern void Abc_TtCofactorTest( word * pTruth, int nVars, int i ); if ( fVerbose ) printf( "%7d : ", i ); - Abc_TtCofactorTest( p->pFuncs[i], p->nVars, i ); if ( fVerbose ) Extra_PrintHex( stdout, (unsigned *)p->pFuncs[i], p->nVars ), printf( "\n" ); } @@ -261,6 +262,17 @@ void Abc_TruthNpnPerform( Abc_TtStore_t * p, int NpnType, int fVerbose ) Extra_PrintHex( stdout, (unsigned *)p->pFuncs[i], p->nVars ), Abc_TruthNpnPrint(pCanonPerm, uCanonPhase, p->nVars), printf( "\n" ); } } + else if ( NpnType == 5 ) + { + for ( i = 0; i < p->nFuncs; i++ ) + { + if ( fVerbose ) + printf( "%7d : ", i ); + uCanonPhase = Abc_TtCanonicize( p->pFuncs[i], p->nVars, pCanonPerm ); + if ( fVerbose ) + Extra_PrintHex( stdout, (unsigned *)p->pFuncs[i], p->nVars ), Abc_TruthNpnPrint(pCanonPerm, uCanonPhase, p->nVars), printf( "\n" ); + } + } else assert( 0 ); clk = clock() - clk; printf( "Classes =%9d ", Abc_TruthNpnCountUnique(p) ); @@ -324,7 +336,7 @@ int Abc_NpnTest( char * pFileName, int NpnType, int nVarNum, int fDumpRes, int f { if ( fVerbose ) printf( "Using truth tables from file \"%s\"...\n", pFileName ); - if ( NpnType >= 0 && NpnType <= 4 ) + if ( NpnType >= 0 && NpnType <= 5 ) Abc_TruthNpnTest( pFileName, NpnType, nVarNum, fDumpRes, fBinary, fVerbose ); else printf( "Unknown canonical form value (%d).\n", NpnType ); diff --git a/src/misc/util/utilTruth.h b/src/misc/util/utilTruth.h index 236c0d62..c742aac9 100644 --- a/src/misc/util/utilTruth.h +++ b/src/misc/util/utilTruth.h @@ -61,6 +61,14 @@ static word s_CMasks6[5] = { 0x000000000000FFFF }; +static word s_PMasks[5][3] = { + { 0x9999999999999999, 0x2222222222222222, 0x4444444444444444 }, + { 0xC3C3C3C3C3C3C3C3, 0x0C0C0C0C0C0C0C0C, 0x3030303030303030 }, + { 0xF00FF00FF00FF00F, 0x00F000F000F000F0, 0x0F000F000F000F00 }, + { 0xFF0000FFFF0000FF, 0x0000FF000000FF00, 0x00FF000000FF0000 }, + { 0xFFFF00000000FFFF, 0x00000000FFFF0000, 0x0000FFFF00000000 } +}; + //////////////////////////////////////////////////////////////////////// /// MACRO DEFINITIONS /// //////////////////////////////////////////////////////////////////////// @@ -161,10 +169,9 @@ static inline int Abc_TtIsConst1( word * pIn1, int nWords ) return 1; } - /**Function************************************************************* - Synopsis [Compares Cof0 and Cof1.] + Synopsis [] Description [] @@ -173,217 +180,42 @@ static inline int Abc_TtIsConst1( word * pIn1, int nWords ) SeeAlso [] ***********************************************************************/ -static inline int Abc_TtCompare1VarCofs( word * pTruth, int nWords, int iVar ) +static inline void Abc_TtCofactor0( word * pTruth, int nWords, int iVar ) { if ( nWords == 1 ) + pTruth[0] = ((pTruth[0] & s_Truths6Neg[iVar]) << (1 << iVar)) | (pTruth[0] & s_Truths6Neg[iVar]); + else if ( iVar <= 5 ) { - word Cof0 = pTruth[0] & s_Truths6Neg[iVar]; - word Cof1 = (pTruth[0] >> (1 << iVar)) & s_Truths6Neg[iVar]; - if ( Cof0 != Cof1 ) - return Cof0 < Cof1 ? -1 : 1; - return 0; - } - if ( iVar <= 5 ) - { - word Cof0, Cof1; int w, shift = (1 << iVar); for ( w = 0; w < nWords; w++ ) - { - Cof0 = pTruth[w] & s_Truths6Neg[iVar]; - Cof1 = (pTruth[w] >> shift) & s_Truths6Neg[iVar]; - if ( Cof0 != Cof1 ) - return Cof0 < Cof1 ? -1 : 1; - } - return 0; + pTruth[w] = ((pTruth[w] & s_Truths6Neg[iVar]) << shift) | (pTruth[w] & s_Truths6Neg[iVar]); } - // if ( iVar > 5 ) + else // if ( iVar > 5 ) { word * pLimit = pTruth + nWords; int i, iStep = Abc_TtWordNum(iVar); - assert( nWords >= 2 ); for ( ; pTruth < pLimit; pTruth += 2*iStep ) for ( i = 0; i < iStep; i++ ) - if ( pTruth[i] != pTruth[i + iStep] ) - return pTruth[i] < pTruth[i + iStep] ? -1 : 1; - return 0; - } -} -static inline int Abc_TtCompare1VarCofsRev( word * pTruth, int nWords, int iVar ) -{ - if ( nWords == 1 ) - { - word Cof0 = pTruth[0] & s_Truths6Neg[iVar]; - word Cof1 = (pTruth[0] >> (1 << iVar)) & s_Truths6Neg[iVar]; - if ( Cof0 != Cof1 ) - return Cof0 < Cof1 ? -1 : 1; - return 0; - } - if ( iVar <= 5 ) - { - word Cof0, Cof1; - int w, shift = (1 << iVar); - for ( w = nWords - 1; w >= 0; w-- ) - { - Cof0 = pTruth[w] & s_Truths6Neg[iVar]; - Cof1 = (pTruth[w] >> shift) & s_Truths6Neg[iVar]; - if ( Cof0 != Cof1 ) - return Cof0 < Cof1 ? -1 : 1; - } - return 0; - } - // if ( iVar > 5 ) - { - word * pLimit = pTruth + nWords; - int i, iStep = Abc_TtWordNum(iVar); - assert( nWords >= 2 ); - for ( pLimit -= 2*iStep; pLimit >= pTruth; pLimit -= 2*iStep ) - for ( i = iStep - 1; i >= 0; i-- ) - if ( pLimit[i] != pLimit[i + iStep] ) - return pLimit[i] < pLimit[i + iStep] ? -1 : 1; - return 0; - } -} - -/**Function************************************************************* - - Synopsis [Checks pairs of cofactors w.r.t. adjacent variables.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static inline int Abc_TtCheckEqual2VarCofs( word * pTruth, int nWords, int iVar, int Num1, int Num2 ) -{ - assert( Num1 < Num2 && Num2 < 4 ); - if ( nWords == 1 ) - return ((pTruth[0] >> (Num2 * (1 << iVar))) & s_CMasks6[iVar]) == ((pTruth[0] >> (Num1 * (1 << iVar))) & s_CMasks6[iVar]); - if ( iVar <= 4 ) - { - int w, shift = (1 << iVar); - for ( w = 0; w < nWords; w++ ) - if ( ((pTruth[w] >> Num2 * shift) & s_CMasks6[iVar]) != ((pTruth[w] >> Num1 * shift) & s_CMasks6[iVar]) ) - return 0; - return 1; - } - if ( iVar == 5 ) - { - unsigned * pTruthU = (unsigned *)pTruth; - unsigned * pLimitU = (unsigned *)(pTruth + nWords); - assert( nWords >= 2 ); - for ( ; pTruthU < pLimitU; pTruthU += 4 ) - if ( pTruthU[Num2] != pTruthU[Num1] ) - return 0; - return 1; - } - // if ( iVar > 5 ) - { - word * pLimit = pTruth + nWords; - int i, iStep = Abc_TtWordNum(iVar); - assert( nWords >= 4 ); - for ( ; pTruth < pLimit; pTruth += 4*iStep ) - for ( i = 0; i < iStep; i++ ) - if ( pTruth[i+Num2*iStep] != pTruth[i+Num1*iStep] ) - return 0; - return 1; + pTruth[i + iStep] = pTruth[i]; } } -static inline int Abc_TtCompare2VarCofs( word * pTruth, int nWords, int iVar, int Num1, int Num2 ) +static inline void Abc_TtCofactor1( word * pTruth, int nWords, int iVar ) { - assert( Num1 < Num2 && Num2 < 4 ); if ( nWords == 1 ) + pTruth[0] = (pTruth[0] & s_Truths6[iVar]) | ((pTruth[0] & s_Truths6[iVar]) >> (1 << iVar)); + else if ( iVar <= 5 ) { - word Cof1 = (pTruth[0] >> (Num1 * (1 << iVar))) & s_CMasks6[iVar]; - word Cof2 = (pTruth[0] >> (Num2 * (1 << iVar))) & s_CMasks6[iVar]; - if ( Cof1 != Cof2 ) - return Cof1 < Cof2 ? -1 : 1; - return 0; - } - if ( iVar <= 4 ) - { - word Cof1, Cof2; int w, shift = (1 << iVar); for ( w = 0; w < nWords; w++ ) - { - Cof1 = (pTruth[w] >> Num1 * shift) & s_CMasks6[iVar]; - Cof2 = (pTruth[w] >> Num2 * shift) & s_CMasks6[iVar]; - if ( Cof1 != Cof2 ) - return Cof1 < Cof2 ? -1 : 1; - } - return 0; - } - if ( iVar == 5 ) - { - unsigned * pTruthU = (unsigned *)pTruth; - unsigned * pLimitU = (unsigned *)(pTruth + nWords); - assert( nWords >= 2 ); - for ( ; pTruthU < pLimitU; pTruthU += 4 ) - if ( pTruthU[Num1] != pTruthU[Num2] ) - return pTruthU[Num1] < pTruthU[Num2] ? -1 : 1; - return 0; + pTruth[w] = (pTruth[w] & s_Truths6[iVar]) | ((pTruth[w] & s_Truths6[iVar]) >> shift); } - // if ( iVar > 5 ) + else // if ( iVar > 5 ) { word * pLimit = pTruth + nWords; int i, iStep = Abc_TtWordNum(iVar); - int Offset1 = Num1*iStep; - int Offset2 = Num2*iStep; - assert( nWords >= 4 ); - for ( ; pTruth < pLimit; pTruth += 4*iStep ) + for ( ; pTruth < pLimit; pTruth += 2*iStep ) for ( i = 0; i < iStep; i++ ) - if ( pTruth[i + Offset1] != pTruth[i + Offset2] ) - return pTruth[i + Offset1] < pTruth[i + Offset2] ? -1 : 1; - return 0; - } -} -static inline int Abc_TtCompare2VarCofsRev( word * pTruth, int nWords, int iVar, int Num1, int Num2 ) -{ - assert( Num1 < Num2 && Num2 < 4 ); - if ( nWords == 1 ) - { - word Cof1 = (pTruth[0] >> (Num1 * (1 << iVar))) & s_CMasks6[iVar]; - word Cof2 = (pTruth[0] >> (Num2 * (1 << iVar))) & s_CMasks6[iVar]; - if ( Cof1 != Cof2 ) - return Cof1 < Cof2 ? -1 : 1; - return 0; - } - if ( iVar <= 4 ) - { - word Cof1, Cof2; - int w, shift = (1 << iVar); - for ( w = nWords - 1; w >= 0; w-- ) - { - Cof1 = (pTruth[w] >> Num1 * shift) & s_CMasks6[iVar]; - Cof2 = (pTruth[w] >> Num2 * shift) & s_CMasks6[iVar]; - if ( Cof1 != Cof2 ) - return Cof1 < Cof2 ? -1 : 1; - } - return 0; - } - if ( iVar == 5 ) - { - unsigned * pTruthU = (unsigned *)pTruth; - unsigned * pLimitU = (unsigned *)(pTruth + nWords); - assert( nWords >= 2 ); - for ( pLimitU -= 4; pLimitU >= pTruthU; pLimitU -= 4 ) - if ( pLimitU[Num1] != pLimitU[Num2] ) - return pLimitU[Num1] < pLimitU[Num2] ? -1 : 1; - return 0; - } - // if ( iVar > 5 ) - { - word * pLimit = pTruth + nWords; - int i, iStep = Abc_TtWordNum(iVar); - int Offset1 = Num1*iStep; - int Offset2 = Num2*iStep; - assert( nWords >= 4 ); - for ( pLimit -= 4*iStep; pLimit >= pTruth; pLimit -= 4*iStep ) - for ( i = iStep - 1; i >= 0; i-- ) - if ( pLimit[i + Offset1] != pLimit[i + Offset2] ) - return pLimit[i + Offset1] < pLimit[i + Offset2] ? -1 : 1; - return 0; + pTruth[i] = pTruth[i + iStep]; } } @@ -449,56 +281,6 @@ static inline int Abc_TtCheckEqualCofs( word * pTruth, int nWords, int iVar, int } } -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static inline void Abc_TtCofactor0( word * pTruth, int nWords, int iVar ) -{ - if ( nWords == 1 ) - pTruth[0] = ((pTruth[0] & s_Truths6Neg[iVar]) << (1 << iVar)) | (pTruth[0] & s_Truths6Neg[iVar]); - else if ( iVar <= 5 ) - { - int w, shift = (1 << iVar); - for ( w = 0; w < nWords; w++ ) - pTruth[w] = ((pTruth[w] & s_Truths6Neg[iVar]) << shift) | (pTruth[w] & s_Truths6Neg[iVar]); - } - else // if ( iVar > 5 ) - { - word * pLimit = pTruth + nWords; - int i, iStep = Abc_TtWordNum(iVar); - for ( ; pTruth < pLimit; pTruth += 2*iStep ) - for ( i = 0; i < iStep; i++ ) - pTruth[i + iStep] = pTruth[i]; - } -} -static inline void Abc_TtCofactor1( word * pTruth, int nWords, int iVar ) -{ - if ( nWords == 1 ) - pTruth[0] = (pTruth[0] & s_Truths6[iVar]) | ((pTruth[0] & s_Truths6[iVar]) >> (1 << iVar)); - else if ( iVar <= 5 ) - { - int w, shift = (1 << iVar); - for ( w = 0; w < nWords; w++ ) - pTruth[w] = (pTruth[w] & s_Truths6[iVar]) | ((pTruth[w] & s_Truths6[iVar]) >> shift); - } - else // if ( iVar > 5 ) - { - word * pLimit = pTruth + nWords; - int i, iStep = Abc_TtWordNum(iVar); - for ( ; pTruth < pLimit; pTruth += 2*iStep ) - for ( i = 0; i < iStep; i++ ) - pTruth[i] = pTruth[i + iStep]; - } -} - /**Function************************************************************* @@ -826,6 +608,10 @@ static inline int Abc_Tt6SupportAndSize( word t, int nVars, int * pSuppSize ) SeeAlso [] ***********************************************************************/ +static inline word Abc_Tt6Flip( word Truth, int iVar ) +{ + return Truth = ((Truth << (1 << iVar)) & s_Truths6[iVar]) | ((Truth & s_Truths6[iVar]) >> (1 << iVar)); +} static inline void Abc_TtFlip( word * pTruth, int nWords, int iVar ) { if ( nWords == 1 ) @@ -857,9 +643,13 @@ static inline void Abc_TtFlip( word * pTruth, int nWords, int iVar ) SeeAlso [] ***********************************************************************/ +static inline word Abc_Tt6SwapAdjacent( word Truth, int iVar ) +{ + return (Truth & s_PMasks[iVar][0]) | ((Truth & s_PMasks[iVar][1]) << (1 << iVar)) | ((Truth & s_PMasks[iVar][2]) >> (1 << iVar)); +} static inline void Abc_TtSwapAdjacent( word * pTruth, int nWords, int iVar ) { - static word PMasks[5][3] = { + static word s_PMasks[5][3] = { { 0x9999999999999999, 0x2222222222222222, 0x4444444444444444 }, { 0xC3C3C3C3C3C3C3C3, 0x0C0C0C0C0C0C0C0C, 0x3030303030303030 }, { 0xF00FF00FF00FF00F, 0x00F000F000F000F0, 0x0F000F000F000F00 }, @@ -870,7 +660,7 @@ static inline void Abc_TtSwapAdjacent( word * pTruth, int nWords, int iVar ) { int i, Shift = (1 << iVar); for ( i = 0; i < nWords; i++ ) - pTruth[i] = (pTruth[i] & PMasks[iVar][0]) | ((pTruth[i] & PMasks[iVar][1]) << Shift) | ((pTruth[i] & PMasks[iVar][2]) >> Shift); + pTruth[i] = (pTruth[i] & s_PMasks[iVar][0]) | ((pTruth[i] & s_PMasks[iVar][1]) << Shift) | ((pTruth[i] & s_PMasks[iVar][2]) >> Shift); } else if ( iVar == 5 ) { @@ -888,10 +678,9 @@ static inline void Abc_TtSwapAdjacent( word * pTruth, int nWords, int iVar ) ABC_SWAP( word, pTruth[i + iStep], pTruth[i + 2*iStep] ); } } - static inline void Abc_TtSwapVars( word * pTruth, int nVars, int iVar, int jVar ) { - static word PPMasks[5][6][3] = { + static word Ps_PMasks[5][6][3] = { { { 0x0000000000000000, 0x0000000000000000, 0x0000000000000000 }, // 0 0 { 0x9999999999999999, 0x2222222222222222, 0x4444444444444444 }, // 0 1 @@ -940,18 +729,18 @@ static inline void Abc_TtSwapVars( word * pTruth, int nVars, int iVar, int jVar assert( iVar < jVar && jVar < nVars ); if ( nVars <= 6 ) { - word * pMasks = PPMasks[iVar][jVar]; + word * s_PMasks = Ps_PMasks[iVar][jVar]; int shift = (1 << jVar) - (1 << iVar); - pTruth[0] = (pTruth[0] & pMasks[0]) | ((pTruth[0] & pMasks[1]) << shift) | ((pTruth[0] & pMasks[2]) >> shift); + pTruth[0] = (pTruth[0] & s_PMasks[0]) | ((pTruth[0] & s_PMasks[1]) << shift) | ((pTruth[0] & s_PMasks[2]) >> shift); return; } if ( jVar <= 5 ) { - word * pMasks = PPMasks[iVar][jVar]; + word * s_PMasks = Ps_PMasks[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); + pTruth[w] = (pTruth[w] & s_PMasks[0]) | ((pTruth[w] & s_PMasks[1]) << shift) | ((pTruth[w] & s_PMasks[2]) >> shift); return; } if ( iVar <= 5 && jVar > 5 ) @@ -984,6 +773,38 @@ static inline void Abc_TtSwapVars( word * pTruth, int nVars, int iVar, int jVar /**Function************************************************************* + Synopsis [Implemeting given NPN config.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Abc_TtImplementNpnConfig( 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] ); + } +} + +/**Function************************************************************* + Synopsis [] Description [] @@ -1024,220 +845,6 @@ static inline int Abc_TtCountOnes( word x ) SeeAlso [] ***********************************************************************/ -static inline int Abc_TtCountOnesInTruth( word * pTruth, int nVars ) -{ - int nWords = Abc_TtWordNum( nVars ); - int k, Counter = 0; - for ( k = 0; k < nWords; k++ ) - if ( pTruth[k] ) - Counter += Abc_TtCountOnes( pTruth[k] ); - return Counter; -} -static inline void Abc_TtCountOnesInCofs( word * pTruth, int nVars, int * pStore ) -{ - word Temp; - int i, k, Counter, nWords; - 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 - for ( i = 0; i < 6; i++ ) - if ( (Temp = (pTruth[k] & s_Truths6Neg[i]) | ((pTruth[k+1] & s_Truths6Neg[i]) << (1 << i))) ) - pStore[i] += Abc_TtCountOnes( Temp ); - // count 1's for all other variables - if ( pTruth[k] ) - { - Counter = Abc_TtCountOnes( pTruth[k] ); - for ( i = 6; i < nVars; i++ ) - if ( (k & (1 << (i-6))) == 0 ) - pStore[i] += Counter; - } - k++; - // count 1's for all other variables - if ( pTruth[k] ) - { - Counter = Abc_TtCountOnes( pTruth[k] ); - for ( i = 6; i < nVars; i++ ) - if ( (k & (1 << (i-6))) == 0 ) - pStore[i] += Counter; - } - } -} -static inline void Abc_TtCountOnesInCofsSlow( word * pTruth, int nVars, int * pStore ) -{ - static int bit_count[256] = { - 0,1,1,2,1,2,2,3,1,2,2,3,2,3,3,4,1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5, - 1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6, - 1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6, - 2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7, - 1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6, - 2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7, - 2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7, - 3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,4,5,5,6,5,6,6,7,5,6,6,7,6,7,7,8 - }; - int i, k, nBytes; - unsigned char * pTruthC = (unsigned char *)pTruth; - nBytes = 8 * Abc_TtWordNum( nVars ); - memset( pStore, 0, sizeof(int) * nVars ); - for ( k = 0; k < nBytes; k++ ) - { - pStore[0] += bit_count[ pTruthC[k] & 0x55 ]; - pStore[1] += bit_count[ pTruthC[k] & 0x33 ]; - pStore[2] += bit_count[ pTruthC[k] & 0x0F ]; - for ( i = 3; i < nVars; i++ ) - if ( (k & (1 << (i-3))) == 0 ) - pStore[i] += bit_count[pTruthC[k]]; - } -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static inline unsigned Abc_TtSemiCanonicize( word * pTruth, int nVars, char * pCanonPerm, int * pStoreOut ) -{ - extern int Abc_TtCountOnesInCofsFast( word * pTruth, int nVars, int * pStore ); - - int fOldSwap = 0; - int pStoreIn[17]; - int * pStore = pStoreOut ? pStoreOut : pStoreIn; -// int pStore2[17]; - int nWords = Abc_TtWordNum( nVars ); - 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 ) - { - Abc_TtNot( pTruth, nWords ); - nOnes = nWords*64 - nOnes; - uCanonPhase |= (1 << nVars); - } - // normalize phase - Abc_TtCountOnesInCofs( pTruth, nVars, pStore ); - pStore[nVars] = nOnes; -// Abc_TtCountOnesInCofsFast( pTruth, nVars, pStore ); - -// Abc_TtCountOnesInCofsFast( pTruth, nVars, pStore2 ); -// for ( i = 0; i < nVars; i++ ) -// assert( pStore[i] == pStore2[i] ); - - for ( i = 0; i < nVars; i++ ) - { - if ( pStore[i] >= nOnes - pStore[i] ) - continue; - Abc_TtFlip( pTruth, nWords, i ); - uCanonPhase |= (1 << i); - pStore[i] = nOnes - pStore[i]; - } - - 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 = 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)); - } - Abc_TtSwapAdjacent( pTruth, nWords, i ); - fChange = 1; - // nSwaps++; - } - } while ( fChange ); - } - else - { - 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 = pStore[i]; - pStore[i] = pStore[BestK]; - pStore[BestK] = Temp; - - if ( ((uCanonPhase >> i) & 1) != ((uCanonPhase >> BestK) & 1) ) - { - uCanonPhase ^= (1 << i); - uCanonPhase ^= (1 << BestK); - } - Abc_TtSwapVars( pTruth, nVars, i, BestK ); - // nSwaps++; - } - } - - -// printf( "%d ", nSwaps ); -/* - printf( "Minterms: " ); - for ( i = 0; i < nVars; i++ ) - printf( "%d ", pStore[i] ); - printf( "\n" ); -*/ - return uCanonPhase; -} - - - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ static inline void Abc_TtReverseVars( word * pTruth, int nVars ) { int k; diff --git a/src/opt/dau/dau.h b/src/opt/dau/dau.h new file mode 100644 index 00000000..b65a1b2c --- /dev/null +++ b/src/opt/dau/dau.h @@ -0,0 +1,69 @@ +/**CFile**************************************************************** + + FileName [dau.h] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [DAG-aware unmapping.] + + Synopsis [External declarations.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: dau.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#ifndef ABC__DAU___h +#define ABC__DAU___h + + +//////////////////////////////////////////////////////////////////////// +/// INCLUDES /// +//////////////////////////////////////////////////////////////////////// + +#include <stdio.h> +#include <stdlib.h> +#include <string.h> +#include <assert.h> +#include <time.h> +#include "misc/vec/vec.h" + +//////////////////////////////////////////////////////////////////////// +/// PARAMETERS /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_HEADER_START + + +//////////////////////////////////////////////////////////////////////// +/// BASIC TYPES /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// MACRO DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +/*=== dauCanon.c ==========================================================*/ +extern unsigned Abc_TtCanonicize( word * pTruth, int nVars, char * pCanonPerm ); + + +ABC_NAMESPACE_HEADER_END + + + +#endif + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + diff --git a/src/opt/dau/dauCanon.c b/src/opt/dau/dauCanon.c index b66b276b..2853f238 100644 --- a/src/opt/dau/dauCanon.c +++ b/src/opt/dau/dauCanon.c @@ -30,10 +30,10 @@ ABC_NAMESPACE_IMPL_START //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// - + /**Function************************************************************* - Synopsis [Generate reverse bytes.] + Synopsis [Compares Cof0 and Cof1.] Description [] @@ -42,26 +42,80 @@ ABC_NAMESPACE_IMPL_START SeeAlso [] ***********************************************************************/ -void Abc_TtReverseBypes() +static inline int Abc_TtCompare1VarCofs( word * pTruth, int nWords, int iVar ) { - int i, k; - for ( i = 0; i < 256; i++ ) + if ( nWords == 1 ) { - int Mask = 0; - for ( k = 0; k < 8; k++ ) - if ( (i >> k) & 1 ) - Mask |= (1 << (7-k)); -// printf( "%3d %3d\n", i, Mask ); - - if ( i % 16 == 0 ) - printf( "\n" ); - printf( "%-3d, ", Mask ); + word Cof0 = pTruth[0] & s_Truths6Neg[iVar]; + word Cof1 = (pTruth[0] >> (1 << iVar)) & s_Truths6Neg[iVar]; + if ( Cof0 != Cof1 ) + return Cof0 < Cof1 ? -1 : 1; + return 0; + } + if ( iVar <= 5 ) + { + word Cof0, Cof1; + int w, shift = (1 << iVar); + for ( w = 0; w < nWords; w++ ) + { + Cof0 = pTruth[w] & s_Truths6Neg[iVar]; + Cof1 = (pTruth[w] >> shift) & s_Truths6Neg[iVar]; + if ( Cof0 != Cof1 ) + return Cof0 < Cof1 ? -1 : 1; + } + return 0; } + // if ( iVar > 5 ) + { + word * pLimit = pTruth + nWords; + int i, iStep = Abc_TtWordNum(iVar); + assert( nWords >= 2 ); + for ( ; pTruth < pLimit; pTruth += 2*iStep ) + for ( i = 0; i < iStep; i++ ) + if ( pTruth[i] != pTruth[i + iStep] ) + return pTruth[i] < pTruth[i + iStep] ? -1 : 1; + return 0; + } +} +static inline int Abc_TtCompare1VarCofsRev( word * pTruth, int nWords, int iVar ) +{ + if ( nWords == 1 ) + { + word Cof0 = pTruth[0] & s_Truths6Neg[iVar]; + word Cof1 = (pTruth[0] >> (1 << iVar)) & s_Truths6Neg[iVar]; + if ( Cof0 != Cof1 ) + return Cof0 < Cof1 ? -1 : 1; + return 0; + } + if ( iVar <= 5 ) + { + word Cof0, Cof1; + int w, shift = (1 << iVar); + for ( w = nWords - 1; w >= 0; w-- ) + { + Cof0 = pTruth[w] & s_Truths6Neg[iVar]; + Cof1 = (pTruth[w] >> shift) & s_Truths6Neg[iVar]; + if ( Cof0 != Cof1 ) + return Cof0 < Cof1 ? -1 : 1; + } + return 0; + } + // if ( iVar > 5 ) + { + word * pLimit = pTruth + nWords; + int i, iStep = Abc_TtWordNum(iVar); + assert( nWords >= 2 ); + for ( pLimit -= 2*iStep; pLimit >= pTruth; pLimit -= 2*iStep ) + for ( i = iStep - 1; i >= 0; i-- ) + if ( pLimit[i] != pLimit[i + iStep] ) + return pLimit[i] < pLimit[i + iStep] ? -1 : 1; + return 0; + } } /**Function************************************************************* - Synopsis [] + Synopsis [Checks equality of pairs of cofactors w.r.t. adjacent variables.] Description [] @@ -70,722 +124,772 @@ void Abc_TtReverseBypes() SeeAlso [] ***********************************************************************/ -void Abc_TtCofactorTest7( word * pTruth, int nVars, int N ) +static inline int Abc_TtCheckEqual2VarCofs( word * pTruth, int nWords, int iVar, int Num1, int Num2 ) { - word Cof[4][1024]; - int i, nWords = Abc_TtWordNum( nVars ); -// int Counter = 0; - for ( i = 0; i < nVars-1; i++ ) + assert( Num1 < Num2 && Num2 < 4 ); + if ( nWords == 1 ) + return ((pTruth[0] >> (Num2 * (1 << iVar))) & s_CMasks6[iVar]) == ((pTruth[0] >> (Num1 * (1 << iVar))) & s_CMasks6[iVar]); + if ( iVar <= 4 ) + { + int w, shift = (1 << iVar); + for ( w = 0; w < nWords; w++ ) + if ( ((pTruth[w] >> Num2 * shift) & s_CMasks6[iVar]) != ((pTruth[w] >> Num1 * shift) & s_CMasks6[iVar]) ) + return 0; + return 1; + } + if ( iVar == 5 ) + { + unsigned * pTruthU = (unsigned *)pTruth; + unsigned * pLimitU = (unsigned *)(pTruth + nWords); + assert( nWords >= 2 ); + for ( ; pTruthU < pLimitU; pTruthU += 4 ) + if ( pTruthU[Num2] != pTruthU[Num1] ) + return 0; + return 1; + } + // if ( iVar > 5 ) { - Abc_TtCopy( Cof[0], pTruth, nWords, 0 ); - Abc_TtCofactor0( Cof[0], nWords, i ); - Abc_TtCofactor0( Cof[0], nWords, i + 1 ); + word * pLimit = pTruth + nWords; + int i, iStep = Abc_TtWordNum(iVar); + assert( nWords >= 4 ); + for ( ; pTruth < pLimit; pTruth += 4*iStep ) + for ( i = 0; i < iStep; i++ ) + if ( pTruth[i+Num2*iStep] != pTruth[i+Num1*iStep] ) + return 0; + return 1; + } +} - Abc_TtCopy( Cof[1], pTruth, nWords, 0 ); - Abc_TtCofactor1( Cof[1], nWords, i ); - Abc_TtCofactor0( Cof[1], nWords, i + 1 ); +/**Function************************************************************* - Abc_TtCopy( Cof[2], pTruth, nWords, 0 ); - Abc_TtCofactor0( Cof[2], nWords, i ); - Abc_TtCofactor1( Cof[2], nWords, i + 1 ); + Synopsis [Compares pairs of cofactors w.r.t. adjacent variables.] - Abc_TtCopy( Cof[3], pTruth, nWords, 0 ); - Abc_TtCofactor1( Cof[3], nWords, i ); - Abc_TtCofactor1( Cof[3], nWords, i + 1 ); + Description [] + + SideEffects [] - if ( i == 5 && N == 4 ) - { - printf( "\n" ); - Abc_TtPrintHex( Cof[0], nVars ); - Abc_TtPrintHex( Cof[1], nVars ); - Abc_TtPrintHex( Cof[2], nVars ); - Abc_TtPrintHex( Cof[3], nVars ); - } + SeeAlso [] - assert( Abc_TtCompareRev(Cof[0], Cof[1], nWords) == Abc_TtCompare2VarCofsRev(pTruth, nWords, i, 0, 1) ); - assert( Abc_TtCompareRev(Cof[0], Cof[2], nWords) == Abc_TtCompare2VarCofsRev(pTruth, nWords, i, 0, 2) ); - assert( Abc_TtCompareRev(Cof[0], Cof[3], nWords) == Abc_TtCompare2VarCofsRev(pTruth, nWords, i, 0, 3) ); - assert( Abc_TtCompareRev(Cof[1], Cof[2], nWords) == Abc_TtCompare2VarCofsRev(pTruth, nWords, i, 1, 2) ); - assert( Abc_TtCompareRev(Cof[1], Cof[3], nWords) == Abc_TtCompare2VarCofsRev(pTruth, nWords, i, 1, 3) ); - assert( Abc_TtCompareRev(Cof[2], Cof[3], nWords) == Abc_TtCompare2VarCofsRev(pTruth, nWords, i, 2, 3) ); -/* - Counter += Abc_TtCompare(Cof[0], Cof[1], nWords); - Counter += Abc_TtCompare(Cof[0], Cof[2], nWords); - Counter += Abc_TtCompare(Cof[0], Cof[3], nWords); - Counter += Abc_TtCompare(Cof[1], Cof[2], nWords); - Counter += Abc_TtCompare(Cof[1], Cof[3], nWords); - Counter += Abc_TtCompare(Cof[2], Cof[3], nWords); - - Counter += Abc_TtCompare2VarCofs(pTruth, nWords, i, 0, 1); - Counter += Abc_TtCompare2VarCofs(pTruth, nWords, i, 0, 2); - Counter += Abc_TtCompare2VarCofs(pTruth, nWords, i, 0, 3); - Counter += Abc_TtCompare2VarCofs(pTruth, nWords, i, 1, 2); - Counter += Abc_TtCompare2VarCofs(pTruth, nWords, i, 1, 3); - Counter += Abc_TtCompare2VarCofs(pTruth, nWords, i, 2, 3); -*/ - } -} -void Abc_TtCofactorTest2( word * pTruth, int nVars, int N ) +***********************************************************************/ +static inline int Abc_TtCompare2VarCofs( word * pTruth, int nWords, int iVar, int Num1, int Num2 ) { -// word Cof[4][1024]; - int i, j, nWords = Abc_TtWordNum( nVars ); - int Counter = 0; - for ( i = 0; i < nVars-1; i++ ) - for ( j = i+1; j < nVars; j++ ) + assert( Num1 < Num2 && Num2 < 4 ); + if ( nWords == 1 ) { -/* - Abc_TtCopy( Cof[0], pTruth, nWords, 0 ); - Abc_TtCofactor0( Cof[0], nWords, i ); - Abc_TtCofactor0( Cof[0], nWords, j ); - - Abc_TtCopy( Cof[1], pTruth, nWords, 0 ); - Abc_TtCofactor1( Cof[1], nWords, i ); - Abc_TtCofactor0( Cof[1], nWords, j ); - - Abc_TtCopy( Cof[2], pTruth, nWords, 0 ); - Abc_TtCofactor0( Cof[2], nWords, i ); - Abc_TtCofactor1( Cof[2], nWords, j ); - - Abc_TtCopy( Cof[3], pTruth, nWords, 0 ); - Abc_TtCofactor1( Cof[3], nWords, i ); - Abc_TtCofactor1( Cof[3], nWords, j ); -*/ -/* - if ( i == 0 && j == 1 && N == 0 ) + word Cof1 = (pTruth[0] >> (Num1 * (1 << iVar))) & s_CMasks6[iVar]; + word Cof2 = (pTruth[0] >> (Num2 * (1 << iVar))) & s_CMasks6[iVar]; + if ( Cof1 != Cof2 ) + return Cof1 < Cof2 ? -1 : 1; + return 0; + } + if ( iVar <= 4 ) + { + word Cof1, Cof2; + int w, shift = (1 << iVar); + for ( w = 0; w < nWords; w++ ) { - printf( "\n" ); - Abc_TtPrintHexSpecial( Cof[0], nVars ); printf( "\n" ); - Abc_TtPrintHexSpecial( Cof[1], nVars ); printf( "\n" ); - Abc_TtPrintHexSpecial( Cof[2], nVars ); printf( "\n" ); - Abc_TtPrintHexSpecial( Cof[3], nVars ); printf( "\n" ); + Cof1 = (pTruth[w] >> Num1 * shift) & s_CMasks6[iVar]; + Cof2 = (pTruth[w] >> Num2 * shift) & s_CMasks6[iVar]; + if ( Cof1 != Cof2 ) + return Cof1 < Cof2 ? -1 : 1; } -*/ -/* - assert( Abc_TtEqual(Cof[0], Cof[1], nWords) == Abc_TtCheckEqualCofs(pTruth, nWords, i, j, 0, 1) ); - assert( Abc_TtEqual(Cof[0], Cof[2], nWords) == Abc_TtCheckEqualCofs(pTruth, nWords, i, j, 0, 2) ); - assert( Abc_TtEqual(Cof[0], Cof[3], nWords) == Abc_TtCheckEqualCofs(pTruth, nWords, i, j, 0, 3) ); - assert( Abc_TtEqual(Cof[1], Cof[2], nWords) == Abc_TtCheckEqualCofs(pTruth, nWords, i, j, 1, 2) ); - assert( Abc_TtEqual(Cof[1], Cof[3], nWords) == Abc_TtCheckEqualCofs(pTruth, nWords, i, j, 1, 3) ); - assert( Abc_TtEqual(Cof[2], Cof[3], nWords) == Abc_TtCheckEqualCofs(pTruth, nWords, i, j, 2, 3) ); -*/ - - Counter += Abc_TtCheckEqualCofs(pTruth, nWords, i, j, 0, 1); - Counter += Abc_TtCheckEqualCofs(pTruth, nWords, i, j, 0, 2); - Counter += Abc_TtCheckEqualCofs(pTruth, nWords, i, j, 0, 3); - Counter += Abc_TtCheckEqualCofs(pTruth, nWords, i, j, 1, 2); - Counter += Abc_TtCheckEqualCofs(pTruth, nWords, i, j, 1, 3); - Counter += Abc_TtCheckEqualCofs(pTruth, nWords, i, j, 2, 3); -/* - Counter += Abc_TtEqual(Cof[0], Cof[1], nWords); - Counter += Abc_TtEqual(Cof[0], Cof[2], nWords); - Counter += Abc_TtEqual(Cof[0], Cof[3], nWords); - Counter += Abc_TtEqual(Cof[1], Cof[2], nWords); - Counter += Abc_TtEqual(Cof[1], Cof[3], nWords); - Counter += Abc_TtEqual(Cof[2], Cof[3], nWords); -*/ + return 0; } -} -void Abc_TtCofactorTest3( word * pTruth, int nVars, int N ) -{ - word Cof[4][1024]; - int i, j, nWords = Abc_TtWordNum( nVars ); - for ( i = 0; i < nVars-1; i++ ) - for ( j = i+1; j < nVars; j++ ) - { - Abc_TtCopy( Cof[0], pTruth, nWords, 0 ); - Abc_TtCofactor0( Cof[0], nWords, i ); - Abc_TtCofactor0( Cof[0], nWords, j ); - - Abc_TtCopy( Cof[1], pTruth, nWords, 0 ); - Abc_TtCofactor1( Cof[1], nWords, i ); - Abc_TtCofactor0( Cof[1], nWords, j ); - - Abc_TtCopy( Cof[2], pTruth, nWords, 0 ); - Abc_TtCofactor0( Cof[2], nWords, i ); - Abc_TtCofactor1( Cof[2], nWords, j ); - - Abc_TtCopy( Cof[3], pTruth, nWords, 0 ); - Abc_TtCofactor1( Cof[3], nWords, i ); - Abc_TtCofactor1( Cof[3], nWords, j ); - - assert( Abc_TtEqual(Cof[0], Cof[1], nWords) == Abc_TtCheckEqualCofs(pTruth, nWords, i, j, 0, 1) ); - assert( Abc_TtEqual(Cof[0], Cof[2], nWords) == Abc_TtCheckEqualCofs(pTruth, nWords, i, j, 0, 2) ); - assert( Abc_TtEqual(Cof[0], Cof[3], nWords) == Abc_TtCheckEqualCofs(pTruth, nWords, i, j, 0, 3) ); - assert( Abc_TtEqual(Cof[1], Cof[2], nWords) == Abc_TtCheckEqualCofs(pTruth, nWords, i, j, 1, 2) ); - assert( Abc_TtEqual(Cof[1], Cof[3], nWords) == Abc_TtCheckEqualCofs(pTruth, nWords, i, j, 1, 3) ); - assert( Abc_TtEqual(Cof[2], Cof[3], nWords) == Abc_TtCheckEqualCofs(pTruth, nWords, i, j, 2, 3) ); + if ( iVar == 5 ) + { + unsigned * pTruthU = (unsigned *)pTruth; + unsigned * pLimitU = (unsigned *)(pTruth + nWords); + assert( nWords >= 2 ); + for ( ; pTruthU < pLimitU; pTruthU += 4 ) + if ( pTruthU[Num1] != pTruthU[Num2] ) + return pTruthU[Num1] < pTruthU[Num2] ? -1 : 1; + return 0; } + // if ( iVar > 5 ) + { + word * pLimit = pTruth + nWords; + int i, iStep = Abc_TtWordNum(iVar); + int Offset1 = Num1*iStep; + int Offset2 = Num2*iStep; + assert( nWords >= 4 ); + for ( ; pTruth < pLimit; pTruth += 4*iStep ) + for ( i = 0; i < iStep; i++ ) + if ( pTruth[i + Offset1] != pTruth[i + Offset2] ) + return pTruth[i + Offset1] < pTruth[i + Offset2] ? -1 : 1; + return 0; + } } - -void Abc_TtCofactorTest4( word * pTruth, int nVars, int N ) +static inline int Abc_TtCompare2VarCofsRev( word * pTruth, int nWords, int iVar, int Num1, int Num2 ) { - word Cof[4][1024]; - int i, j, nWords = Abc_TtWordNum( nVars ); - int Sum = 0; - for ( i = 0; i < nVars-1; i++ ) - for ( j = i+1; j < nVars; j++ ) - { - Abc_TtCopy( Cof[0], pTruth, nWords, 0 ); - Abc_TtCofactor0( Cof[0], nWords, i ); - Abc_TtCofactor0( Cof[0], nWords, j ); - - Abc_TtCopy( Cof[1], pTruth, nWords, 0 ); - Abc_TtCofactor1( Cof[1], nWords, i ); - Abc_TtCofactor0( Cof[1], nWords, j ); - - Abc_TtCopy( Cof[2], pTruth, nWords, 0 ); - Abc_TtCofactor0( Cof[2], nWords, i ); - Abc_TtCofactor1( Cof[2], nWords, j ); - - Abc_TtCopy( Cof[3], pTruth, nWords, 0 ); - Abc_TtCofactor1( Cof[3], nWords, i ); - Abc_TtCofactor1( Cof[3], nWords, j ); - - - Sum = 0; - Sum += Abc_TtEqual(Cof[0], Cof[1], nWords); - Sum += Abc_TtEqual(Cof[0], Cof[2], nWords); - Sum += Abc_TtEqual(Cof[0], Cof[3], nWords); - Sum += Abc_TtEqual(Cof[1], Cof[2], nWords); - Sum += Abc_TtEqual(Cof[1], Cof[3], nWords); - Sum += Abc_TtEqual(Cof[2], Cof[3], nWords); - - assert( Abc_TtEqual(Cof[0], Cof[1], nWords) == Abc_TtCheckEqualCofs(pTruth, nWords, i, j, 0, 1) ); - assert( Abc_TtEqual(Cof[0], Cof[2], nWords) == Abc_TtCheckEqualCofs(pTruth, nWords, i, j, 0, 2) ); - assert( Abc_TtEqual(Cof[0], Cof[3], nWords) == Abc_TtCheckEqualCofs(pTruth, nWords, i, j, 0, 3) ); - assert( Abc_TtEqual(Cof[1], Cof[2], nWords) == Abc_TtCheckEqualCofs(pTruth, nWords, i, j, 1, 2) ); - assert( Abc_TtEqual(Cof[1], Cof[3], nWords) == Abc_TtCheckEqualCofs(pTruth, nWords, i, j, 1, 3) ); - assert( Abc_TtEqual(Cof[2], Cof[3], nWords) == Abc_TtCheckEqualCofs(pTruth, nWords, i, j, 2, 3) ); + assert( Num1 < Num2 && Num2 < 4 ); + if ( nWords == 1 ) + { + word Cof1 = (pTruth[0] >> (Num1 * (1 << iVar))) & s_CMasks6[iVar]; + word Cof2 = (pTruth[0] >> (Num2 * (1 << iVar))) & s_CMasks6[iVar]; + if ( Cof1 != Cof2 ) + return Cof1 < Cof2 ? -1 : 1; + return 0; } -} - -void Abc_TtCofactorTest6( word * pTruth, int nVars, int N ) -{ -// word Cof[4][1024]; - int i, nWords = Abc_TtWordNum( nVars ); -// if ( N != 30 ) -// return; - printf( "\n " ); - Abc_TtPrintHex( pTruth, nVars ); -// Kit_DsdPrintFromTruth( pTruth, nVars ); printf( "\n" ); - - for ( i = nVars - 1; i >= 0; i-- ) + if ( iVar <= 4 ) { -/* - Abc_TtCopy( Cof[0], pTruth, nWords, 0 ); - Abc_TtCofactor0( Cof[0], nWords, i ); - printf( "- " ); - Abc_TtPrintHex( Cof[0], nVars ); - - Abc_TtCopy( Cof[1], pTruth, nWords, 0 ); - Abc_TtCofactor1( Cof[1], nWords, i ); - printf( "+ " ); - Abc_TtPrintHex( Cof[1], nVars ); -*/ - if ( Abc_TtCompare1VarCofsRev( pTruth, nWords, i ) == -1 ) + word Cof1, Cof2; + int w, shift = (1 << iVar); + for ( w = nWords - 1; w >= 0; w-- ) { - printf( "%d ", i ); - Abc_TtFlip( pTruth, nWords, i ); - Abc_TtPrintHex( pTruth, nVars ); -// Kit_DsdPrintFromTruth( pTruth, nVars ); printf( "\n" ); + Cof1 = (pTruth[w] >> Num1 * shift) & s_CMasks6[iVar]; + Cof2 = (pTruth[w] >> Num2 * shift) & s_CMasks6[iVar]; + if ( Cof1 != Cof2 ) + return Cof1 < Cof2 ? -1 : 1; } - - -/* - Abc_TtCopy( Cof[0], pTruth, nWords, 0 ); - Abc_TtCofactor0( Cof[0], nWords, i ); - - Abc_TtCopy( Cof[1], pTruth, nWords, 0 ); - Abc_TtCofactor1( Cof[1], nWords, i ); - - assert( Abc_TtCompareRev(Cof[0], Cof[1], nWords) == Abc_TtCompare1VarCofsRev(pTruth, nWords, i) ); -*/ + return 0; } - i = 0; -} - -int Abc_TtCofactorPermNaive( word * pTruth, int i, int nWords, int fSwapOnly ) -{ - static word pCopy[1024]; - static word pBest[1024]; - - if ( fSwapOnly ) + if ( iVar == 5 ) { - 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; - } + unsigned * pTruthU = (unsigned *)pTruth; + unsigned * pLimitU = (unsigned *)(pTruth + nWords); + assert( nWords >= 2 ); + for ( pLimitU -= 4; pLimitU >= pTruthU; pLimitU -= 4 ) + if ( pLimitU[Num1] != pLimitU[Num2] ) + return pLimitU[Num1] < pLimitU[Num2] ? -1 : 1; return 0; } - - // save two copies - Abc_TtCopy( pCopy, pTruth, nWords, 0 ); - Abc_TtCopy( pBest, pTruth, nWords, 0 ); - - // PXY - // 001 - Abc_TtFlip( pCopy, nWords, i ); - if ( Abc_TtCompareRev(pBest, pCopy, nWords) == 1 ) - Abc_TtCopy( pBest, pCopy, nWords, 0 ); - - // PXY - // 011 - Abc_TtFlip( pCopy, nWords, i+1 ); - if ( Abc_TtCompareRev(pBest, pCopy, nWords) == 1 ) - Abc_TtCopy( pBest, pCopy, nWords, 0 ); - - // PXY - // 010 - Abc_TtFlip( pCopy, nWords, i ); - if ( Abc_TtCompareRev(pBest, pCopy, nWords) == 1 ) - Abc_TtCopy( pBest, pCopy, nWords, 0 ); - - // PXY - // 110 - Abc_TtSwapAdjacent( pCopy, nWords, i ); - if ( Abc_TtCompareRev(pBest, pCopy, nWords) == 1 ) - Abc_TtCopy( pBest, pCopy, nWords, 0 ); - - // PXY - // 111 - Abc_TtFlip( pCopy, nWords, i+1 ); - if ( Abc_TtCompareRev(pBest, pCopy, nWords) == 1 ) - Abc_TtCopy( pBest, pCopy, nWords, 0 ); - - // PXY - // 101 - Abc_TtFlip( pCopy, nWords, i ); - if ( Abc_TtCompareRev(pBest, pCopy, nWords) == 1 ) - Abc_TtCopy( pBest, pCopy, nWords, 0 ); - - // PXY - // 100 - Abc_TtFlip( pCopy, nWords, i+1 ); - if ( Abc_TtCompareRev(pBest, pCopy, nWords) == 1 ) - Abc_TtCopy( pBest, pCopy, nWords, 0 ); - - // PXY - // 000 - 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 ) ) + // if ( iVar > 5 ) + { + word * pLimit = pTruth + nWords; + int i, iStep = Abc_TtWordNum(iVar); + int Offset1 = Num1*iStep; + int Offset2 = Num2*iStep; + assert( nWords >= 4 ); + for ( pLimit -= 4*iStep; pLimit >= pTruth; pLimit -= 4*iStep ) + for ( i = iStep - 1; i >= 0; i-- ) + if ( pLimit[i + Offset1] != pLimit[i + Offset2] ) + return pLimit[i + Offset1] < pLimit[i + Offset2] ? -1 : 1; return 0; - assert( Abc_TtCompareRev(pTruth, pBest, nWords) == 1 ); - Abc_TtCopy( pTruth, pBest, nWords, 0 ); - return 1; + } } +/**Function************************************************************* -int Abc_TtCofactorPerm( word * pTruth, int i, int nWords, char * pCanonPerm, unsigned * puCanonPhase, int fSwapOnly ) -{ - static word pCopy1[1024]; - int fComp01, fComp02, fComp03, fComp12, fComp13, fComp23; - unsigned uPhaseInit = *puCanonPhase; - int RetValue = 0; - - if ( fSwapOnly ) - { - fComp12 = Abc_TtCompare2VarCofsRev( pTruth, nWords, i, 1, 2 ); - if ( fComp12 < 0 ) // Cof1 < Cof2 - { - Abc_TtSwapAdjacent( pTruth, nWords, i ); - RetValue = 1; + Synopsis [Minterm counting in all cofactors.] - if ( ((*puCanonPhase >> i) & 1) != ((*puCanonPhase >> (i+1)) & 1) ) - { - *puCanonPhase ^= (1 << i); - *puCanonPhase ^= (1 << (i+1)); - } + Description [] + + SideEffects [] - ABC_SWAP( int, pCanonPerm[i], pCanonPerm[i+1] ); - } - return RetValue; - } + SeeAlso [] - Abc_TtCopy( pCopy1, pTruth, nWords, 0 ); - - fComp01 = Abc_TtCompare2VarCofsRev( pTruth, nWords, i, 0, 1 ); - fComp23 = Abc_TtCompare2VarCofsRev( pTruth, nWords, i, 2, 3 ); - if ( fComp23 >= 0 ) // Cof2 >= Cof3 +***********************************************************************/ +static inline int Abc_TtCountOnesInTruth( word * pTruth, int nVars ) +{ + int nWords = Abc_TtWordNum( nVars ); + int k, Counter = 0; + for ( k = 0; k < nWords; k++ ) + if ( pTruth[k] ) + Counter += Abc_TtCountOnes( pTruth[k] ); + return Counter; +} +static inline void Abc_TtCountOnesInCofs( word * pTruth, int nVars, int * pStore ) +{ + word Temp; + int i, k, Counter, nWords; + if ( nVars <= 6 ) { - if ( fComp01 >= 0 ) // Cof0 >= Cof1 - { - fComp13 = Abc_TtCompare2VarCofsRev( pTruth, nWords, i, 1, 3 ); - 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 < 0 ) // Cof0 < Cof3 - { - Abc_TtFlip( pTruth, nWords, i ); - Abc_TtFlip( pTruth, nWords, i + 1 ); - *puCanonPhase ^= (1 << i); - *puCanonPhase ^= (1 << (i+1)); - RetValue = 1; - } - else // Cof0 >= Cof3 - { - if ( fComp23 == 0 ) // can flip Cof0 and Cof1 - { - Abc_TtFlip( pTruth, nWords, i ); - *puCanonPhase ^= (1 << i); - RetValue = 1; - } - } - } + for ( i = 0; i < nVars; i++ ) + pStore[i] = Abc_TtCountOnes( pTruth[0] & s_Truths6Neg[i] ); + return; } - else // Cof2 < Cof3 + assert( nVars > 6 ); + nWords = Abc_TtWordNum( nVars ); + memset( pStore, 0, sizeof(int) * nVars ); + for ( k = 0; k < nWords; k++ ) { - if ( fComp01 >= 0 ) // Cof0 >= Cof1 + // count 1's for the first six variables + for ( i = 0; i < 6; i++ ) + if ( (Temp = (pTruth[k] & s_Truths6Neg[i]) | ((pTruth[k+1] & s_Truths6Neg[i]) << (1 << i))) ) + pStore[i] += Abc_TtCountOnes( Temp ); + // count 1's for all other variables + if ( pTruth[k] ) { - fComp12 = Abc_TtCompare2VarCofsRev( pTruth, nWords, i, 1, 2 ); - 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); - } - } + Counter = Abc_TtCountOnes( pTruth[k] ); + for ( i = 6; i < nVars; i++ ) + if ( (k & (1 << (i-6))) == 0 ) + pStore[i] += Counter; } - else // Cof0 < Cof1 + k++; + // count 1's for all other variables + if ( pTruth[k] ) { - fComp02 = Abc_TtCompare2VarCofsRev( pTruth, nWords, i, 0, 2 ); - if ( fComp02 == -1 ) // Cof0 < Cof2 - { - Abc_TtFlip( pTruth, nWords, i ); - Abc_TtFlip( pTruth, nWords, i + 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); - } + Counter = Abc_TtCountOnes( pTruth[k] ); + for ( i = 6; i < nVars; i++ ) + if ( (k & (1 << (i-6))) == 0 ) + pStore[i] += Counter; } - RetValue = 1; - } - // perform final swap if needed - 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)); - } +/**Function************************************************************* - ABC_SWAP( int, pCanonPerm[i], pCanonPerm[i+1] ); - } + Synopsis [Minterm counting in all cofactors.] - if ( RetValue == 1 ) + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Abc_TtCountOnesInCofsSlow( word * pTruth, int nVars, int * pStore ) +{ + static int bit_count[256] = { + 0,1,1,2,1,2,2,3,1,2,2,3,2,3,3,4,1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5, + 1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6, + 1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6, + 2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7, + 1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6, + 2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7, + 2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7, + 3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,4,5,5,6,5,6,6,7,5,6,6,7,6,7,7,8 + }; + int i, k, nBytes; + unsigned char * pTruthC = (unsigned char *)pTruth; + nBytes = 8 * Abc_TtWordNum( nVars ); + memset( pStore, 0, sizeof(int) * nVars ); + for ( k = 0; k < nBytes; k++ ) { - 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; - } + pStore[0] += bit_count[ pTruthC[k] & 0x55 ]; + pStore[1] += bit_count[ pTruthC[k] & 0x33 ]; + pStore[2] += bit_count[ pTruthC[k] & 0x0F ]; + for ( i = 3; i < nVars; i++ ) + if ( (k & (1 << (i-3))) == 0 ) + pStore[i] += bit_count[pTruthC[k]]; } - return RetValue; } +/**Function************************************************************* -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; + Synopsis [Minterm counting in all cofactors.] -// pTruth[0] = (s_Truths6[0] & s_Truths6[1]) | s_Truths6[2]; -// nVars = 3; + Description [] + + SideEffects [] -/* - printf( "\n" ); - Kit_DsdPrintFromTruth( pTruth, nVars ); printf( "\n" ); - Abc_TtPrintBinary( pTruth, nVars ); - printf( "\n" ); -*/ + SeeAlso [] -// for ( i = nVars - 2; i >= 0; i-- ) - for ( i = 3; i < nVars - 1; i++ ) +***********************************************************************/ +int Abc_TtCountOnesInCofsFast6_rec( word Truth, int iVar, int nBytes, int * pStore ) +{ + static int bit_count[256] = { + 0,1,1,2,1,2,2,3,1,2,2,3,2,3,3,4,1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5, + 1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6, + 1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6, + 2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7, + 1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6, + 2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7, + 2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7, + 3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,4,5,5,6,5,6,6,7,5,6,6,7,6,7,7,8 + }; + int nMints0, nMints1; + if ( Truth == 0 ) + return 0; + if ( ~Truth == 0 ) { -/* - 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 i; + for ( i = 0; i <= iVar; i++ ) + pStore[i] += nBytes * 4; + return nBytes * 8; + } + if ( nBytes == 1 ) + { + assert( iVar == 2 ); + pStore[0] += bit_count[ Truth & 0x55 ]; + pStore[1] += bit_count[ Truth & 0x33 ]; + pStore[2] += bit_count[ Truth & 0x0F ]; + return bit_count[ Truth & 0xFF ]; + } + nMints0 = Abc_TtCountOnesInCofsFast6_rec( Abc_Tt6Cof0(Truth, iVar), iVar - 1, nBytes/2, pStore ); + nMints1 = Abc_TtCountOnesInCofsFast6_rec( Abc_Tt6Cof1(Truth, iVar), iVar - 1, nBytes/2, pStore ); + pStore[iVar] += nMints0; + return nMints0 + nMints1; +} + +int Abc_TtCountOnesInCofsFast_rec( word * pTruth, int iVar, int nWords, int * pStore ) +{ + int nMints0, nMints1; + if ( nWords == 1 ) + { + assert( iVar == 5 ); + return Abc_TtCountOnesInCofsFast6_rec( pTruth[0], iVar, 8, pStore ); + } + assert( nWords > 1 ); + assert( iVar > 5 ); + if ( pTruth[0] & 1 ) + { + if ( Abc_TtIsConst1( pTruth, nWords ) ) { - int s = 0; - continue; + int i; + for ( i = 0; i <= iVar; i++ ) + pStore[i] += nWords * 32; + return nWords * 64; } -*/ - 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 ); - + else + { + if ( Abc_TtIsConst0( pTruth, nWords ) ) + return 0; + } + nMints0 = Abc_TtCountOnesInCofsFast_rec( pTruth, iVar - 1, nWords/2, pStore ); + nMints1 = Abc_TtCountOnesInCofsFast_rec( pTruth + nWords/2, iVar - 1, nWords/2, pStore ); + pStore[iVar] += nMints0; + return nMints0 + nMints1; +} +int Abc_TtCountOnesInCofsFast( word * pTruth, int nVars, int * pStore ) +{ + memset( pStore, 0, sizeof(int) * nVars ); + assert( nVars >= 3 ); + if ( nVars <= 6 ) + return Abc_TtCountOnesInCofsFast6_rec( pTruth[0], nVars - 1, Abc_TtByteNum( nVars ), pStore ); + else + return Abc_TtCountOnesInCofsFast_rec( pTruth, nVars - 1, Abc_TtWordNum( nVars ), pStore ); } +/**Function************************************************************* -void Abc_TtCofactorTest8( word * pTruth, int nVars, int N ) -{ - int fVerbose = 0; - int i; - int nWords = Abc_TtWordNum( nVars ); + Synopsis [] - if ( fVerbose ) - printf( "\n " ), Abc_TtPrintHex( pTruth, nVars ); + Description [] + + SideEffects [] - if ( fVerbose ) - printf( "Round 1\n" ); - for ( i = nVars - 2; i >= 0; i-- ) + SeeAlso [] + +***********************************************************************/ +static inline unsigned Abc_TtSemiCanonicize( word * pTruth, int nVars, char * pCanonPerm, int * pStoreOut ) +{ + int fOldSwap = 0; + int pStoreIn[17]; + int * pStore = pStoreOut ? pStoreOut : pStoreIn; + int i, nOnes, nWords = Abc_TtWordNum( nVars ); + 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 ) { - if ( Abc_TtCofactorPermNaive( pTruth, i, nWords, 0 ) ) - { - if ( fVerbose ) - printf( "%d ", i ), Abc_TtPrintHex( pTruth, nVars ); - } + Abc_TtNot( pTruth, nWords ); + nOnes = nWords*64 - nOnes; + uCanonPhase |= (1 << nVars); } - - if ( fVerbose ) - printf( "Round 2\n" ); - for ( i = 0; i < nVars - 1; i++ ) + // normalize phase + Abc_TtCountOnesInCofs( pTruth, nVars, pStore ); + pStore[nVars] = nOnes; + for ( i = 0; i < nVars; i++ ) { - if ( Abc_TtCofactorPermNaive( pTruth, i, nWords, 0 ) ) - { - if ( fVerbose ) - printf( "%d ", i ), Abc_TtPrintHex( pTruth, nVars ); - } + if ( pStore[i] >= nOnes - pStore[i] ) + continue; + Abc_TtFlip( pTruth, nWords, i ); + uCanonPhase |= (1 << i); + pStore[i] = nOnes - pStore[i]; } - - return; - - if ( fVerbose ) - printf( "Round 3\n" ); - for ( i = nVars - 2; i >= 0; i-- ) + // normalize permutation + if ( fOldSwap ) { - if ( Abc_TtCofactorPermNaive( pTruth, i, nWords, 0 ) ) - { - if ( fVerbose ) - printf( "%d ", i ), Abc_TtPrintHex( pTruth, nVars ); - } + 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; + ABC_SWAP( int, pCanonPerm[i], pCanonPerm[i+1] ); + ABC_SWAP( int, pStore[i], pStore[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++; + } + } + while ( fChange ); } - - if ( fVerbose ) - printf( "Round 4\n" ); - for ( i = 0; i < nVars - 1; i++ ) + else { - if ( Abc_TtCofactorPermNaive( pTruth, i, nWords, 0 ) ) + int k, BestK; + for ( i = 0; i < nVars - 1; i++ ) { - if ( fVerbose ) - printf( "%d ", i ), Abc_TtPrintHex( pTruth, nVars ); + 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; + ABC_SWAP( int, pCanonPerm[i], pCanonPerm[BestK] ); + ABC_SWAP( int, pStore[i], pStore[BestK] ); + if ( ((uCanonPhase >> i) & 1) != ((uCanonPhase >> BestK) & 1) ) + { + uCanonPhase ^= (1 << i); + uCanonPhase ^= (1 << BestK); + } + Abc_TtSwapVars( pTruth, nVars, i, BestK ); + // nSwaps++; } } - i = 0; + return uCanonPhase; } + + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ void Abc_TtCofactorTest10( word * pTruth, int nVars, int N ) { static word pCopy1[1024]; static word pCopy2[1024]; int nWords = Abc_TtWordNum( nVars ); int i; - for ( i = 0; i < nVars - 1; i++ ) { // Kit_DsdPrintFromTruth( pTruth, nVars ); printf( "\n" ); - Abc_TtCopy( pCopy1, pTruth, nWords, 0 ); Abc_TtSwapAdjacent( pCopy1, nWords, i ); // Kit_DsdPrintFromTruth( pCopy1, nVars ); printf( "\n" ); - Abc_TtCopy( pCopy2, pTruth, nWords, 0 ); Abc_TtSwapVars( pCopy2, nVars, i, i+1 ); // Kit_DsdPrintFromTruth( pCopy2, nVars ); printf( "\n" ); - assert( Abc_TtEqual( pCopy1, pCopy2, nWords ) ); } } +/**Function************************************************************* -void Abc_TtCofactorTest111( word * pTruth, int nVars, int N ) -{ - char pCanonPerm[32]; - static word pCopy1[1024]; - static word pCopy2[1024]; - int nWords = Abc_TtWordNum( nVars ); - -// Kit_DsdPrintFromTruth( pTruth, nVars ); printf( "\n" ); + Synopsis [Naive evaluation.] - Abc_TtCopy( pCopy1, pTruth, nWords, 0 ); -// Kit_TruthSemiCanonicize_Yasha( pCopy1, nVars, pCanonPerm ); -// Kit_DsdPrintFromTruth( pCopy1, nVars ); printf( "\n" ); + Description [] + + SideEffects [] - Abc_TtCopy( pCopy2, pTruth, nWords, 0 ); - Abc_TtSemiCanonicize( pCopy2, nVars, pCanonPerm, NULL ); -// Kit_DsdPrintFromTruth( pCopy2, nVars ); printf( "\n" ); + SeeAlso [] - assert( Abc_TtEqual( pCopy1, pCopy2, nWords ) ); +***********************************************************************/ +int Abc_Tt6CofactorPermNaive( word * pTruth, int i, int fSwapOnly ) +{ + if ( fSwapOnly ) + { + word Copy = Abc_Tt6SwapAdjacent( pTruth[0], i ); + if ( pTruth[0] > Copy ) + { + pTruth[0] = Copy; + return 4; + } + return 0; + } + { + word Copy = pTruth[0]; + word Best = pTruth[0]; + int Config = 0; + // PXY + // 001 + Copy = Abc_Tt6Flip( Copy, i ); + if ( Best > Copy ) + Best = Copy, Config = 1; + // PXY + // 011 + Copy = Abc_Tt6Flip( Copy, i+1 ); + if ( Best > Copy ) + Best = Copy, Config = 3; + // PXY + // 010 + Copy = Abc_Tt6Flip( Copy, i ); + if ( Best > Copy ) + Best = Copy, Config = 2; + // PXY + // 110 + Copy = Abc_Tt6SwapAdjacent( Copy, i ); + if ( Best > Copy ) + Best = Copy, Config = 6; + // PXY + // 111 + Copy = Abc_Tt6Flip( Copy, i+1 ); + if ( Best > Copy ) + Best = Copy, Config = 7; + // PXY + // 101 + Copy = Abc_Tt6Flip( Copy, i ); + if ( Best > Copy ) + Best = Copy, Config = 5; + // PXY + // 100 + Copy = Abc_Tt6Flip( Copy, i+1 ); + if ( Best > Copy ) + Best = Copy, Config = 4; + // PXY + // 000 + Copy = Abc_Tt6SwapAdjacent( Copy, i ); + assert( Copy == pTruth[0] ); + assert( Best <= pTruth[0] ); + pTruth[0] = Best; + return Config; + } +} +int Abc_TtCofactorPermNaive( word * pTruth, int i, int nWords, int fSwapOnly ) +{ + if ( fSwapOnly ) + { + static word pCopy[1024]; + 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 4; + } + return 0; + } + { + static word pCopy[1024]; + static word pBest[1024]; + int Config = 0; + // save two copies + Abc_TtCopy( pCopy, pTruth, nWords, 0 ); + Abc_TtCopy( pBest, pTruth, nWords, 0 ); + // PXY + // 001 + Abc_TtFlip( pCopy, nWords, i ); + if ( Abc_TtCompareRev(pBest, pCopy, nWords) == 1 ) + Abc_TtCopy( pBest, pCopy, nWords, 0 ), Config = 1; + // PXY + // 011 + Abc_TtFlip( pCopy, nWords, i+1 ); + if ( Abc_TtCompareRev(pBest, pCopy, nWords) == 1 ) + Abc_TtCopy( pBest, pCopy, nWords, 0 ), Config = 3; + // PXY + // 010 + Abc_TtFlip( pCopy, nWords, i ); + if ( Abc_TtCompareRev(pBest, pCopy, nWords) == 1 ) + Abc_TtCopy( pBest, pCopy, nWords, 0 ), Config = 2; + // PXY + // 110 + Abc_TtSwapAdjacent( pCopy, nWords, i ); + if ( Abc_TtCompareRev(pBest, pCopy, nWords) == 1 ) + Abc_TtCopy( pBest, pCopy, nWords, 0 ), Config = 6; + // PXY + // 111 + Abc_TtFlip( pCopy, nWords, i+1 ); + if ( Abc_TtCompareRev(pBest, pCopy, nWords) == 1 ) + Abc_TtCopy( pBest, pCopy, nWords, 0 ), Config = 7; + // PXY + // 101 + Abc_TtFlip( pCopy, nWords, i ); + if ( Abc_TtCompareRev(pBest, pCopy, nWords) == 1 ) + Abc_TtCopy( pBest, pCopy, nWords, 0 ), Config = 5; + // PXY + // 100 + Abc_TtFlip( pCopy, nWords, i+1 ); + if ( Abc_TtCompareRev(pBest, pCopy, nWords) == 1 ) + Abc_TtCopy( pBest, pCopy, nWords, 0 ), Config = 4; + // PXY + // 000 + Abc_TtSwapAdjacent( pCopy, nWords, i ); + assert( Abc_TtEqual( pTruth, pCopy, nWords ) ); + if ( Config == 0 ) + return 0; + assert( Abc_TtCompareRev(pTruth, pBest, nWords) == 1 ); + Abc_TtCopy( pTruth, pBest, nWords, 0 ); + return Config; + } } +/**Function************************************************************* + Synopsis [Smart evaluation.] -void Abc_TtCofactorMinimize( word * pTruth, int nVars, int N ) -{ - char pCanonPerm[16]; - unsigned uCanonPhase; - int i, fVerbose = 0; - int nWords = Abc_TtWordNum( nVars ); + Description [] + + SideEffects [] - if ( fVerbose ) - printf( "\n " ), Abc_TtPrintHex( pTruth, nVars ); + SeeAlso [] - if ( fVerbose ) - printf( "Round 1\n" ); - for ( i = nVars - 2; i >= 0; i-- ) +***********************************************************************/ +int Abc_TtCofactorPermConfig( word * pTruth, int i, int nWords, int fSwapOnly, int fNaive ) +{ + if ( nWords == 1 ) + return Abc_Tt6CofactorPermNaive( pTruth, i, fSwapOnly ); + if ( fNaive ) + return Abc_TtCofactorPermNaive( pTruth, i, nWords, fSwapOnly ); + if ( fSwapOnly ) { - if ( Abc_TtCofactorPerm( pTruth, i, nWords, pCanonPerm, &uCanonPhase, 0 ) ) + if ( Abc_TtCompare2VarCofsRev( pTruth, nWords, i, 1, 2 ) < 0 ) // Cof1 < Cof2 { - if ( fVerbose ) - printf( "%d ", i ), Abc_TtPrintHex( pTruth, nVars ); + Abc_TtSwapAdjacent( pTruth, nWords, i ); + return 4; } + return 0; } - - if ( fVerbose ) - printf( "Round 2\n" ); - for ( i = 0; i < nVars - 1; i++ ) - { - if ( Abc_TtCofactorPerm( pTruth, i, nWords, pCanonPerm, &uCanonPhase, 0 ) ) + { + int fComp01, fComp02, fComp03, fComp12, fComp13, fComp23, Config = 0; + fComp01 = Abc_TtCompare2VarCofsRev( pTruth, nWords, i, 0, 1 ); + fComp23 = Abc_TtCompare2VarCofsRev( pTruth, nWords, i, 2, 3 ); + if ( fComp23 >= 0 ) // Cof2 >= Cof3 { - if ( fVerbose ) - printf( "%d ", i ), Abc_TtPrintHex( pTruth, nVars ); + if ( fComp01 >= 0 ) // Cof0 >= Cof1 + { + fComp13 = Abc_TtCompare2VarCofsRev( pTruth, nWords, i, 1, 3 ); + if ( fComp13 < 0 ) // Cof1 < Cof3 + Abc_TtFlip( pTruth, nWords, i + 1 ), Config = 2; + else if ( fComp13 == 0 ) // Cof1 == Cof3 + { + fComp02 = Abc_TtCompare2VarCofsRev( pTruth, nWords, i, 0, 2 ); + if ( fComp02 < 0 ) + Abc_TtFlip( pTruth, nWords, i + 1 ), Config = 2; + } + // else Cof1 > Cof3 -- do nothing + } + else // Cof0 < Cof1 + { + fComp03 = Abc_TtCompare2VarCofsRev( pTruth, nWords, i, 0, 3 ); + if ( fComp03 < 0 ) // Cof0 < Cof3 + { + Abc_TtFlip( pTruth, nWords, i ); + Abc_TtFlip( pTruth, nWords, i + 1 ), Config = 3; + } + else // Cof0 >= Cof3 + { + if ( fComp23 == 0 ) // can flip Cof0 and Cof1 + Abc_TtFlip( pTruth, nWords, i ), Config = 1; + } + } + } + else // Cof2 < Cof3 + { + if ( fComp01 >= 0 ) // Cof0 >= Cof1 + { + fComp12 = Abc_TtCompare2VarCofsRev( pTruth, nWords, i, 1, 2 ); + if ( fComp12 > 0 ) // Cof1 > Cof2 + Abc_TtFlip( pTruth, nWords, i ), Config = 1; + else if ( fComp12 == 0 ) // Cof1 == Cof2 + { + Abc_TtFlip( pTruth, nWords, i ); + Abc_TtFlip( pTruth, nWords, i + 1 ), Config = 3; + } + else // Cof1 < Cof2 + { + Abc_TtFlip( pTruth, nWords, i + 1 ), Config = 2; + if ( fComp01 == 0 ) + Abc_TtFlip( pTruth, nWords, i ), Config ^= 1; + } + } + else // Cof0 < Cof1 + { + fComp02 = Abc_TtCompare2VarCofsRev( pTruth, nWords, i, 0, 2 ); + if ( fComp02 == -1 ) // Cof0 < Cof2 + { + Abc_TtFlip( pTruth, nWords, i ); + Abc_TtFlip( pTruth, nWords, i + 1 ), Config = 3; + } + else if ( fComp02 == 0 ) // Cof0 == Cof2 + { + fComp13 = Abc_TtCompare2VarCofsRev( pTruth, nWords, i, 1, 3 ); + if ( fComp13 >= 0 ) // Cof1 >= Cof3 + Abc_TtFlip( pTruth, nWords, i ), Config = 1; + else // Cof1 < Cof3 + { + Abc_TtFlip( pTruth, nWords, i ); + Abc_TtFlip( pTruth, nWords, i + 1 ), Config = 3; + } + } + else // Cof0 > Cof2 + Abc_TtFlip( pTruth, nWords, i ), Config = 1; + } } + // perform final swap if needed + fComp12 = Abc_TtCompare2VarCofsRev( pTruth, nWords, i, 1, 2 ); + if ( fComp12 < 0 ) // Cof1 < Cof2 + Abc_TtSwapAdjacent( pTruth, nWords, i ), Config ^= 4; + return Config; } } - - -void Abc_TtCofactorVerify( word * pTruth, int nVars, char * pCanonPerm, unsigned uCanonPhase ) +int Abc_TtCofactorPerm( word * pTruth, int i, int nWords, int fSwapOnly, char * pCanonPerm, unsigned * puCanonPhase, int fNaive ) { - 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++ ) + if ( fSwapOnly ) { - 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] ); + int Config = Abc_TtCofactorPermConfig( pTruth, i, nWords, 1, 0 ); + if ( Config ) + { + if ( ((*puCanonPhase >> i) & 1) != ((*puCanonPhase >> (i+1)) & 1) ) + { + *puCanonPhase ^= (1 << i); + *puCanonPhase ^= (1 << (i+1)); + } + ABC_SWAP( int, pCanonPerm[i], pCanonPerm[i+1] ); + } + return Config; + } + { + static word pCopy1[1024]; + int Config; + Abc_TtCopy( pCopy1, pTruth, nWords, 0 ); + Config = Abc_TtCofactorPermConfig( pTruth, i, nWords, 0, fNaive ); + if ( Config == 0 ) + return 0; + if ( Abc_TtCompareRev(pTruth, pCopy1, nWords) == 1 ) // made it worse + { + Abc_TtCopy( pTruth, pCopy1, nWords, 0 ); + return 0; + } + // improved + if ( Config & 1 ) + *puCanonPhase ^= (1 << i); + if ( Config & 2 ) + *puCanonPhase ^= (1 << (i+1)); + if ( Config & 4 ) + { + if ( ((*puCanonPhase >> i) & 1) != ((*puCanonPhase >> (i+1)) & 1) ) + { + *puCanonPhase ^= (1 << i); + *puCanonPhase ^= (1 << (i+1)); + } + ABC_SWAP( int, pCanonPerm[i], pCanonPerm[i+1] ); + } + return Config; } } -//#define CANON_VERIFY +/**Function************************************************************* + + Synopsis [Semi-canonical form computation.] + + Description [] + + SideEffects [] + + SeeAlso [] -void Abc_TtCofactorTest( word * pTruth, int nVars, int N ) +***********************************************************************/ +//#define CANON_VERIFY +unsigned Abc_TtCanonicize( word * pTruth, int nVars, char * pCanonPerm ) { int pStoreIn[17]; - char pCanonPerm[16]; unsigned uCanonPhase; - int i, nWords = Abc_TtWordNum( nVars ); + int i, k, nWords = Abc_TtWordNum( nVars ); + int fNaive = 1; #ifdef CANON_VERIFY char pCanonPermCopy[16]; @@ -795,31 +899,26 @@ void Abc_TtCofactorTest( word * pTruth, int nVars, int N ) #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 ); + for ( k = 0; k < 3; k++ ) + { + int fChanges = 0; + for ( i = nVars - 2; i >= 0; i-- ) + if ( pStoreIn[i] == pStoreIn[i+1] ) + fChanges |= Abc_TtCofactorPerm( pTruth, i, nWords, pStoreIn[i] != pStoreIn[nVars]/2, pCanonPerm, &uCanonPhase, fNaive ); + if ( !fChanges ) + break; + fChanges = 0; + for ( i = 1; i < nVars - 1; i++ ) + if ( pStoreIn[i] == pStoreIn[i+1] ) + fChanges |= Abc_TtCofactorPerm( pTruth, i, nWords, pStoreIn[i] != pStoreIn[nVars]/2, pCanonPerm, &uCanonPhase, fNaive ); + if ( !fChanges ) + break; + } #ifdef CANON_VERIFY Abc_TtCopy( pCopy2, pTruth, nWords, 0 ); memcpy( pCanonPermCopy, pCanonPerm, sizeof(char) * nVars ); - Abc_TtCofactorVerify( pCopy2, nVars, pCanonPermCopy, uCanonPhase ); + Abc_TtImplementNpnConfig( pCopy2, nVars, pCanonPermCopy, uCanonPhase ); if ( !Abc_TtEqual( pCopy1, pCopy2, nWords ) ) printf( "Canonical form verification failed!\n" ); #endif @@ -831,6 +930,7 @@ void Abc_TtCofactorTest( word * pTruth, int nVars, int N ) i = 0; } */ + return uCanonPhase; } |