diff options
-rw-r--r-- | src/misc/util/utilTruth.h | 107 | ||||
-rw-r--r-- | src/opt/dau/dauDsd.c | 339 |
2 files changed, 442 insertions, 4 deletions
diff --git a/src/misc/util/utilTruth.h b/src/misc/util/utilTruth.h index 8ec4a513..6bfb5699 100644 --- a/src/misc/util/utilTruth.h +++ b/src/misc/util/utilTruth.h @@ -115,7 +115,7 @@ static inline int Abc_TtSuppIsMinBase( int Supp ) } static inline int Abc_Tt6HasVar( word t, int iVar ) { - return (t & ~s_Truths6[iVar]) != ((t & s_Truths6[iVar]) >> (1<<iVar)); + return ((t << (1<<iVar)) & s_Truths6[iVar]) != (t & s_Truths6[iVar]); } static inline int Abc_TtHasVar( word * t, int nVars, int iVar ) { @@ -125,14 +125,15 @@ static inline int Abc_TtHasVar( word * t, int nVars, int iVar ) { int i, Shift = (1 << iVar); for ( i = 0; i < nWords; i++ ) - if ( (t[i] & ~s_Truths6[iVar]) != ((t[i] & s_Truths6[iVar]) >> Shift) ) + if ( ((t[i] << Shift) & s_Truths6[iVar]) != (t[i] & s_Truths6[iVar]) ) return 1; return 0; } else { - int i, k, Step = (1 << (iVar - 6)); - for ( k = 0; k < nWords; k += 2*Step, t += 2*Step ) + int i, Step = (1 << (iVar - 6)); + word * tLimit = t + nWords; + for ( ; t < tLimit; t += 2*Step ) for ( i = 0; i < Step; i++ ) if ( t[i] != t[Step+i] ) return 1; @@ -189,6 +190,103 @@ static inline int Abc_Tt6SupportAndSize( word t, int nVars, int * pSuppSize ) ***********************************************************************/ static inline void Abc_TtSwapVars( word * pTruth, int nVars, int iVar, int jVar ) { + static word PPMasks[5][6][3] = { + { + { 0x0000000000000000, 0x0000000000000000, 0x0000000000000000 }, // 0 0 + { 0x9999999999999999, 0x2222222222222222, 0x4444444444444444 }, // 0 1 + { 0xA5A5A5A5A5A5A5A5, 0x0A0A0A0A0A0A0A0A, 0x5050505050505050 }, // 0 2 + { 0xAA55AA55AA55AA55, 0x00AA00AA00AA00AA, 0x5500550055005500 }, // 0 3 + { 0xAAAA5555AAAA5555, 0x0000AAAA0000AAAA, 0x5555000055550000 }, // 0 4 + { 0xAAAAAAAA55555555, 0x00000000AAAAAAAA, 0x5555555500000000 } // 0 5 + }, + { + { 0x0000000000000000, 0x0000000000000000, 0x0000000000000000 }, // 1 0 + { 0x0000000000000000, 0x0000000000000000, 0x0000000000000000 }, // 1 1 + { 0xC3C3C3C3C3C3C3C3, 0x0C0C0C0C0C0C0C0C, 0x3030303030303030 }, // 1 2 + { 0xCC33CC33CC33CC33, 0x00CC00CC00CC00CC, 0x3300330033003300 }, // 1 3 + { 0xCCCC3333CCCC3333, 0x0000CCCC0000CCCC, 0x3333000033330000 }, // 1 4 + { 0xCCCCCCCC33333333, 0x00000000CCCCCCCC, 0x3333333300000000 } // 1 5 + }, + { + { 0x0000000000000000, 0x0000000000000000, 0x0000000000000000 }, // 2 0 + { 0x0000000000000000, 0x0000000000000000, 0x0000000000000000 }, // 2 1 + { 0x0000000000000000, 0x0000000000000000, 0x0000000000000000 }, // 2 2 + { 0xF00FF00FF00FF00F, 0x00F000F000F000F0, 0x0F000F000F000F00 }, // 2 3 + { 0xF0F00F0FF0F00F0F, 0x0000F0F00000F0F0, 0x0F0F00000F0F0000 }, // 2 4 + { 0xF0F0F0F00F0F0F0F, 0x00000000F0F0F0F0, 0x0F0F0F0F00000000 } // 2 5 + }, + { + { 0x0000000000000000, 0x0000000000000000, 0x0000000000000000 }, // 3 0 + { 0x0000000000000000, 0x0000000000000000, 0x0000000000000000 }, // 3 1 + { 0x0000000000000000, 0x0000000000000000, 0x0000000000000000 }, // 3 2 + { 0x0000000000000000, 0x0000000000000000, 0x0000000000000000 }, // 3 3 + { 0xFF0000FFFF0000FF, 0x0000FF000000FF00, 0x00FF000000FF0000 }, // 3 4 + { 0xFF00FF0000FF00FF, 0x00000000FF00FF00, 0x00FF00FF00000000 } // 3 5 + }, + { + { 0x0000000000000000, 0x0000000000000000, 0x0000000000000000 }, // 4 0 + { 0x0000000000000000, 0x0000000000000000, 0x0000000000000000 }, // 4 1 + { 0x0000000000000000, 0x0000000000000000, 0x0000000000000000 }, // 4 2 + { 0x0000000000000000, 0x0000000000000000, 0x0000000000000000 }, // 4 3 + { 0x0000000000000000, 0x0000000000000000, 0x0000000000000000 }, // 4 4 + { 0xFFFF00000000FFFF, 0x00000000FFFF0000, 0x0000FFFF00000000 } // 4 5 + } + }; + if ( iVar == jVar ) + return; + if ( jVar < iVar ) + ABC_SWAP( int, iVar, jVar ); + assert( iVar < jVar && jVar < nVars ); + if ( nVars <= 6 ) + { + 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); + } + else + { + 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 temp, * 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++ ) + { + temp = pTruth[iStep + i + j]; + pTruth[iStep + i + j] = pTruth[jStep + i + j]; + pTruth[jStep + i + j] = temp; + } + } + } +} + +static inline void Abc_TtSwapVars_( word * pTruth, int nVars, int iVar, int jVar ) +{ static word PPMasks[6][6] = { { 0x2222222222222222, 0x0A0A0A0A0A0A0A0A, 0x00AA00AA00AA00AA, 0x0000AAAA0000AAAA, 0x00000000AAAAAAAA, 0xAAAAAAAAAAAAAAAA }, { 0x0000000000000000, 0x0C0C0C0C0C0C0C0C, 0x00CC00CC00CC00CC, 0x0000CCCC0000CCCC, 0x00000000CCCCCCCC, 0xCCCCCCCCCCCCCCCC }, @@ -269,6 +367,7 @@ static inline void Abc_TtSwapVars( word * pTruth, int nVars, int iVar, int jVar } + /**Function************************************************************* Synopsis [Stretch truthtable to have more input variables.] diff --git a/src/opt/dau/dauDsd.c b/src/opt/dau/dauDsd.c index 262314d8..f6367304 100644 --- a/src/opt/dau/dauDsd.c +++ b/src/opt/dau/dauDsd.c @@ -19,6 +19,7 @@ ***********************************************************************/ #include "dauInt.h" +#include "misc/util/utilTruth.h" ABC_NAMESPACE_IMPL_START @@ -463,6 +464,344 @@ void Dau_DsdTestOne( word t, int i ) Dau_DsdTestOne( *p->pFuncs[i], i ); */ + + + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Abc_TtTruthIsConst0( word * p, int nWords ) { int w; for ( w = 0; w < nWords; w++ ) if ( p[w] != 0 ) return 0; return 1; } +static inline int Abc_TtTruthIsConst1( word * p, int nWords ) { int w; for ( w = 0; w < nWords; w++ ) if ( p[w] != ~(word)0 ) return 0; return 1; } + +static inline int Abc_TtCof0IsConst0( word * t, int nWords, int iVar ) +{ + if ( iVar < 6 ) + { + int i; + for ( i = 0; i < nWords; i++ ) + if ( t[i] & ~s_Truths6[iVar] ) + return 0; + return 1; + } + else + { + int i, Step = (1 << (iVar - 6)); + word * tLimit = t + nWords; + for ( ; t < tLimit; t += 2*Step ) + for ( i = 0; i < Step; i++ ) + if ( t[i] ) + return 0; + return 1; + } +} +static inline int Abc_TtCof0IsConst1( word * t, int nWords, int iVar ) +{ + if ( iVar < 6 ) + { + int i; + for ( i = 0; i < nWords; i++ ) + if ( (t[i] & ~s_Truths6[iVar]) != ~s_Truths6[iVar] ) + return 0; + return 1; + } + else + { + int i, Step = (1 << (iVar - 6)); + word * tLimit = t + nWords; + for ( ; t < tLimit; t += 2*Step ) + for ( i = 0; i < Step; i++ ) + if ( t[i] != ~(word)0 ) + return 0; + return 1; + } +} +static inline int Abc_TtCof1IsConst0( word * t, int nWords, int iVar ) +{ + if ( iVar < 6 ) + { + int i; + for ( i = 0; i < nWords; i++ ) + if ( t[i] & s_Truths6[iVar] ) + return 0; + return 1; + } + else + { + int i, Step = (1 << (iVar - 6)); + word * tLimit = t + nWords; + for ( ; t < tLimit; t += 2*Step ) + for ( i = 0; i < Step; i++ ) + if ( t[i+Step] ) + return 0; + return 1; + } +} +static inline int Abc_TtCof1IsConst1( word * t, int nWords, int iVar ) +{ + if ( iVar < 6 ) + { + int i; + for ( i = 0; i < nWords; i++ ) + if ( (t[i] & s_Truths6[iVar]) != s_Truths6[iVar] ) + return 0; + return 1; + } + else + { + int i, Step = (1 << (iVar - 6)); + word * tLimit = t + nWords; + for ( ; t < tLimit; t += 2*Step ) + for ( i = 0; i < Step; i++ ) + if ( t[i+Step] != ~(word)0 ) + return 0; + return 1; + } +} +static inline int Abc_TtCofsOpposite( word * t, int nWords, int iVar ) +{ + if ( iVar < 6 ) + { + int i, Shift = (1 << iVar); + for ( i = 0; i < nWords; i++ ) + if ( ((t[i] << Shift) & s_Truths6[iVar]) != (~t[i] & s_Truths6[iVar]) ) + return 0; + return 1; + } + else + { + int i, Step = (1 << (iVar - 6)); + word * tLimit = t + nWords; + for ( ; t < tLimit; t += 2*Step ) + for ( i = 0; i < Step; i++ ) + if ( t[i] != ~t[i+Step] ) + return 0; + return 1; + } +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Abc_TtCof0HasVar( word * t, int nWords, int iVarI, int iVarJ ) +{ + assert( iVarI > iVarJ ); + if ( iVarI < 6 ) + { + int i, Shift = (1 << iVarJ); + for ( i = 0; i < nWords; i++ ) + if ( (((t[i] & ~s_Truths6[iVarI]) << Shift) & s_Truths6[iVarJ]) != ((t[i] & ~s_Truths6[iVarI]) & s_Truths6[iVarJ]) ) + return 0; + return 1; + } + else if ( iVarI == 6 ) + { + } + else + { + int i, Step = (1 << (iVarJ - 6)); + word * tLimit = t + nWords; + for ( ; t < tLimit; t += 2*Step ) + for ( i = 0; i < Step; i++ ) + if ( t[i] != t[i+Step] ) + return 0; + return 1; + } +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Dau_DsdMinimize( word * p, int * pVars, int nVars ) +{ + int i, k; + assert( nVars > 6 ); + for ( i = k = nVars - 1; i >= 0; i-- ) + { + if ( Abc_TtHasVar( p, nVars, i ) ) + continue; + if ( i < k ) + { + pVars[i] = pVars[k]; + Abc_TtSwapVars( p, nVars, i, k ); + } + k--; + nVars--; + } + return nVars; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Dau_DsdRun6_rec( word * p, int * pVars, int nVars, char * pBuffer, int Pos, char pStore[16][16], int Func ) +{ + return 0; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Dau_DsdRun_rec( word * p, int * pVars, int nVars, char * pBuffer, int Pos, char pStore[16][16], int Func ) +{ + int v, nWords = Abc_TtWordNum( nVars ); + nVars = Dau_DsdMinimize( p, pVars, nVars ); + if ( nVars <= 6 ) + return Dau_DsdRun6_rec( p, pVars, nVars, pBuffer, Pos, pStore, Func ); + if ( p[0] & 1 ) + { + // check for !(ax) + for ( v = 0; v < nVars; v++ ) + if ( Abc_TtCof0IsConst0( p, nWords, v ) ) + { + pBuffer[Pos++] = '('; + pBuffer[Pos++] = 'a' + pVars[v]; + Abc_TtSwapVars( p, nVars, v, nVars - 1 ); + pVars[v] = pVars[nVars-1]; + Pos = Dau_DsdRun_rec( p + nWords/2, pVars, nVars-1, pBuffer, Pos, pStore, Func ); + pBuffer[Pos++] = ')'; + return Pos; + } + } + else + { + // check for ax + for ( v = 0; v < nVars; v++ ) + if ( Abc_TtCof0IsConst1( p, nWords, v ) ) + { + pBuffer[Pos++] = '!'; + pBuffer[Pos++] = '('; + pBuffer[Pos++] = 'a' + pVars[v]; + Abc_TtSwapVars( p, nVars, v, nVars - 1 ); + pVars[v] = pVars[nVars-1]; + Pos = Dau_DsdRun_rec( p + nWords/2, pVars, nVars-1, pBuffer, Pos, pStore, Func ); + pBuffer[Pos++] = ')'; + return Pos; + } + } + if ( (p[nWords-1] >> 63) & 1 ) + { + // check for !(!ax) + for ( v = 0; v < nVars; v++ ) + if ( Abc_TtCof0IsConst1( p, nWords, v ) ) + { + pBuffer[Pos++] = '!'; + pBuffer[Pos++] = '('; + pBuffer[Pos++] = '!'; + pBuffer[Pos++] = 'a' + pVars[v]; + Abc_TtSwapVars( p, nVars, v, nVars - 1 ); + pVars[v] = pVars[nVars-1]; + Pos = Dau_DsdRun_rec( p, pVars, nVars-1, pBuffer, Pos, pStore, Func ); + pBuffer[Pos++] = ')'; + return Pos; + } + } + else + { + // check for !ax + for ( v = 0; v < nVars; v++ ) + if ( Abc_TtCof1IsConst0( p, nWords, v ) ) + { + pBuffer[Pos++] = '('; + pBuffer[Pos++] = '!'; + pBuffer[Pos++] = 'a' + pVars[v]; + Abc_TtSwapVars( p, nVars, v, nVars - 1 ); + pVars[v] = pVars[nVars-1]; + Pos = Dau_DsdRun_rec( p, pVars, nVars-1, pBuffer, Pos, pStore, Func ); + pBuffer[Pos++] = ')'; + return Pos; + } + } + // check for a^x + for ( v = 0; v < nVars; v++ ) + if ( Abc_TtCofsOpposite( p, nWords, v ) ) + { + pBuffer[Pos++] = '['; + pBuffer[Pos++] = 'a' + pVars[v]; + Abc_TtSwapVars( p, nVars, v, nVars - 1 ); + pVars[v] = pVars[nVars-1]; + Pos = Dau_DsdRun_rec( p, pVars, nVars-1, pBuffer, Pos, pStore, Func ); + pBuffer[Pos++] = ']'; + return Pos; + } + + return 0; +} + + + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +char * Dau_DsdRun( word * p, int nVars ) +{ + static char pBuffer[DAU_MAX_STR+20]; + static char pStore[16][16]; + int nWords = Abc_TtWordNum( nVars ); + int i, Pos = 0, Func = 0, pVars[16]; + assert( nVars <= 16 ); + for ( i = 0; i < nVars; i++ ) + pVars[i] = i; + if ( Abc_TtTruthIsConst0( p, nWords ) ) + pBuffer[Pos++] = '0'; + else if ( Abc_TtTruthIsConst1( p, nWords ) ) + pBuffer[Pos++] = '1'; + else if ( nVars <= 6 ) + Pos = Dau_DsdRun6_rec( p, pVars, nVars, pBuffer, Pos, pStore, Func ); + else + Pos = Dau_DsdRun_rec( p, pVars, nVars, pBuffer, Pos, pStore, Func ); + pBuffer[Pos++] = 0; + Dau_DsdCleanBraces( pBuffer ); + return pBuffer; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// |