diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/opt/dau/dau.h | 2 | ||||
| -rw-r--r-- | src/opt/dau/dauDsd.c | 600 |
2 files changed, 384 insertions, 218 deletions
diff --git a/src/opt/dau/dau.h b/src/opt/dau/dau.h index b65a1b2c..1db02a0d 100644 --- a/src/opt/dau/dau.h +++ b/src/opt/dau/dau.h @@ -55,7 +55,7 @@ ABC_NAMESPACE_HEADER_START /*=== dauCanon.c ==========================================================*/ extern unsigned Abc_TtCanonicize( word * pTruth, int nVars, char * pCanonPerm ); - +extern char * Dau_DsdDecompose( word * pTruth, int nVarsInit, int * pnSizeNonDec ); ABC_NAMESPACE_HEADER_END diff --git a/src/opt/dau/dauDsd.c b/src/opt/dau/dauDsd.c index be269ebf..2dd7875d 100644 --- a/src/opt/dau/dauDsd.c +++ b/src/opt/dau/dauDsd.c @@ -38,6 +38,7 @@ ABC_NAMESPACE_IMPL_START <abc> = ITE( a, b, c ) */ + //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// @@ -706,21 +707,34 @@ char * Dau_DsdRun( word * p, int nVars ) +/**Function************************************************************* + + Synopsis [Data-structure to store DSD information.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ typedef struct Dau_Dsd_t_ Dau_Dsd_t; struct Dau_Dsd_t_ { int nVarsInit; // the initial number of variables int nVarsUsed; // the current number of variables - char pVarDefs[32][8]; // variable definitions - char pOutput[DAU_MAX_STR]; // output stream int nPos; // writing position + int nSizeNonDec; // size of the largest non-decomposable block int nConsts; // the number of constant decompositions int uConstMask; // constant decomposition mask + char pVarDefs[32][8]; // variable definitions + char Cache[32][32]; // variable cache + char pOutput[DAU_MAX_STR]; // output stream }; /**Function************************************************************* - Synopsis [] + Synopsis [Manipulation of DSD data-structure.] Description [] @@ -729,49 +743,88 @@ struct Dau_Dsd_t_ SeeAlso [] ***********************************************************************/ -void Dua_DsdInit( Dau_Dsd_t * p, int nVarsInit ) +static inline void Dau_DsdInitialize( Dau_Dsd_t * p, int nVarsInit ) { - int i; - memset( p, 0, sizeof(Dau_Dsd_t) ); - p->nVarsInit = p->nVarsUsed = nVarsInit; + int i, v, u; + assert( nVarsInit >= 0 && nVarsInit <= 16 ); + p->nVarsInit = nVarsInit; + p->nVarsUsed = nVarsInit; + p->nPos = 0; + p->nSizeNonDec = 0; + p->nConsts = 0; + p->uConstMask = 0; for ( i = 0; i < nVarsInit; i++ ) - p->pVarDefs[i][0] = 'a' + i; + p->pVarDefs[i][0] = 'a' + i, p->pVarDefs[i][1] = 0; + for ( v = 0; v < nVarsInit; v++ ) + for ( u = 0; u < nVarsInit; u++ ) + p->Cache[v][u] = 0; + } -void Dua_DsdWrite( Dau_Dsd_t * p, char * pStr ) +static inline void Dau_DsdWriteString( Dau_Dsd_t * p, char * pStr ) { while ( *pStr ) p->pOutput[ p->nPos++ ] = *pStr++; } -void Dua_DsdWriteInv( Dau_Dsd_t * p, int Cond ) -{ - if ( Cond ) - p->pOutput[ p->nPos++ ] = '!'; -} -void Dua_DsdWriteVar( Dau_Dsd_t * p, int iVar, int fInv ) +static inline void Dau_DsdWriteVar( Dau_Dsd_t * p, int iVar, int fInv ) { char * pStr; if ( fInv ) p->pOutput[ p->nPos++ ] = '!'; for ( pStr = p->pVarDefs[iVar]; *pStr; pStr++ ) if ( *pStr >= 'a' + p->nVarsInit && *pStr < 'a' + p->nVarsUsed ) - Dua_DsdWriteVar( p, *pStr - 'a', 0 ); + Dau_DsdWriteVar( p, *pStr - 'a', 0 ); + else + p->pOutput[ p->nPos++ ] = *pStr; +} +static inline void Dau_DsdTranslate( Dau_Dsd_t * p, int * pVars, int nVars, char * pStr ) +{ + for ( ; *pStr; pStr++ ) + if ( *pStr >= 'a' + nVars && *pStr < 'a' + nVars ) + Dau_DsdWriteVar( p, pVars[*pStr - 'a'], 0 ); else p->pOutput[ p->nPos++ ] = *pStr; } -void Dua_DsdWriteStop( Dau_Dsd_t * p ) +static inline void Dau_DsdWritePrime( Dau_Dsd_t * p, word * pTruth, int * pVars, int nVars ) +{ + int v; + assert( nVars > 2 ); + p->nPos += Abc_TtWriteHexRev( p->pOutput + p->nPos, pTruth, nVars ); + Dau_DsdWriteString( p, "{" ); + for ( v = 0; v < nVars; v++ ) + Dau_DsdWriteVar( p, pVars[v], 0 ); + Dau_DsdWriteString( p, "}" ); + p->nSizeNonDec = nVars; +} +static inline void Dau_DsdFinalize( Dau_Dsd_t * p ) { int i; for ( i = 0; i < p->nConsts; i++ ) - p->pOutput[ p->nPos++ ] = ((p->uConstMask >> i) & 1) ? ']' : ')'; + p->pOutput[ p->nPos++ ] = ((p->uConstMask >> (p->nConsts-1-i)) & 1) ? ']' : ')'; p->pOutput[ p->nPos++ ] = 0; } -int Dua_DsdAddVarDef( Dau_Dsd_t * p, char * pStr ) +static inline int Dau_DsdAddVarDef( Dau_Dsd_t * p, char * pStr ) { + int u; assert( strlen(pStr) < 8 ); assert( p->nVarsUsed < 32 ); + for ( u = 0; u < p->nVarsUsed; u++ ) + p->Cache[p->nVarsUsed][u] = 0; + for ( u = 0; u < p->nVarsUsed; u++ ) + p->Cache[u][p->nVarsUsed] = 0; sprintf( p->pVarDefs[p->nVarsUsed++], "%s", pStr ); return p->nVarsUsed - 1; } +static inline void Dau_DsdInsertVarCache( Dau_Dsd_t * p, int v, int u, int Status ) +{ + assert( v != u ); + assert( Status > 0 && Status < 4 ); + assert( p->Cache[v][u] == 0 ); + p->Cache[v][u] = Status; +} +static inline int Dau_DsdLookupVarCache( Dau_Dsd_t * p, int v, int u ) +{ + return p->Cache[v][u]; +} /**Function************************************************************* @@ -784,7 +837,7 @@ int Dua_DsdAddVarDef( Dau_Dsd_t * p, char * pStr ) SeeAlso [] ***********************************************************************/ -int Dua_DsdMinBase( word * pTruth, int nVars, int * pVarsNew ) +int Dau_DsdMinBase( word * pTruth, int nVars, int * pVarsNew ) { int v; for ( v = 0; v < nVars; v++ ) @@ -801,7 +854,7 @@ int Dua_DsdMinBase( word * pTruth, int nVars, int * pVarsNew ) /**Function************************************************************* - Synopsis [Returns 1 if constant cofactor is found.] + Synopsis [Procedures specialized for 6-variable functions.] Description [] @@ -810,14 +863,14 @@ int Dua_DsdMinBase( word * pTruth, int nVars, int * pVarsNew ) SeeAlso [] ***********************************************************************/ -int Dau_Dsd6DecomposeConstCofOne( Dau_Dsd_t * p, word * pTruth, int * pVars, int nVars, int v ) +static inline int Dau_Dsd6DecomposeSingleVarOne( Dau_Dsd_t * p, word * pTruth, int * pVars, int nVars, int v ) { // consider negative cofactors if ( pTruth[0] & 1 ) { if ( Abc_Tt6Cof0IsConst1( pTruth[0], v ) ) // !(ax) { - Dua_DsdWrite( p, "!(" ); + Dau_DsdWriteString( p, "!(" ); pTruth[0] = ~Abc_Tt6Cofactor1( pTruth[0], v ); goto finish; } @@ -826,7 +879,7 @@ int Dau_Dsd6DecomposeConstCofOne( Dau_Dsd_t * p, word * pTruth, int * pVars, int { if ( Abc_Tt6Cof0IsConst0( pTruth[0], v ) ) // ax { - Dua_DsdWrite( p, "(" ); + Dau_DsdWriteString( p, "(" ); pTruth[0] = Abc_Tt6Cofactor1( pTruth[0], v ); goto finish; } @@ -836,7 +889,7 @@ int Dau_Dsd6DecomposeConstCofOne( Dau_Dsd_t * p, word * pTruth, int * pVars, int { if ( Abc_Tt6Cof1IsConst1( pTruth[0], v ) ) // !(!ax) { - Dua_DsdWrite( p, "!(!" ); + Dau_DsdWriteString( p, "!(!" ); pTruth[0] = ~Abc_Tt6Cofactor0( pTruth[0], v ); goto finish; } @@ -845,7 +898,7 @@ int Dau_Dsd6DecomposeConstCofOne( Dau_Dsd_t * p, word * pTruth, int * pVars, int { if ( Abc_Tt6Cof1IsConst0( pTruth[0], v ) ) // !ax { - Dua_DsdWrite( p, "(!" ); + Dau_DsdWriteString( p, "(!" ); pTruth[0] = Abc_Tt6Cofactor0( pTruth[0], v ); goto finish; } @@ -853,7 +906,7 @@ int Dau_Dsd6DecomposeConstCofOne( Dau_Dsd_t * p, word * pTruth, int * pVars, int // consider equal cofactors if ( Abc_Tt6CofsOpposite( pTruth[0], v ) ) // [ax] { - Dua_DsdWrite( p, "[" ); + Dau_DsdWriteString( p, "[" ); pTruth[0] = Abc_Tt6Cofactor0( pTruth[0], v ); p->uConstMask |= (1 << p->nConsts); goto finish; @@ -862,247 +915,360 @@ int Dau_Dsd6DecomposeConstCofOne( Dau_Dsd_t * p, word * pTruth, int * pVars, int finish: p->nConsts++; - Dua_DsdWriteVar( p, pVars[v], 0 ); + Dau_DsdWriteVar( p, pVars[v], 0 ); pVars[v] = pVars[nVars-1]; Abc_TtSwapVars( pTruth, 6, v, nVars-1 ); return 1; } -int Dau_Dsd6DecomposeConstCof( Dau_Dsd_t * p, word * pTruth, int * pVars, int nVars ) +int Dau_Dsd6DecomposeSingleVar( Dau_Dsd_t * p, word * pTruth, int * pVars, int nVars ) { - int v, nVarsOld; assert( nVars > 1 ); while ( 1 ) { - nVarsOld = nVars; + int v; for ( v = nVars - 1; v >= 0 && nVars > 1; v-- ) - if ( Dau_Dsd6DecomposeConstCofOne( p, pTruth, pVars, nVars, v ) ) + if ( Dau_Dsd6DecomposeSingleVarOne( p, pTruth, pVars, nVars, v ) ) + { nVars--; - if ( nVarsOld == nVars || nVars == 1 ) + break; + } + if ( v == -1 || nVars == 1 ) break; } if ( nVars == 1 ) - Dua_DsdWriteVar( p, pVars[--nVars], (int)(pTruth[0] & 1) ); + Dau_DsdWriteVar( p, pVars[--nVars], (int)(pTruth[0] & 1) ); return nVars; } -void Dau_Dsd6DecomposeInternal( Dau_Dsd_t * p, word t, int * pVars, int nVars ) +static inline int Dau_Dsd6FindSupportOne( Dau_Dsd_t * p, word tCof0, word tCof1, int * pVars, int nVars, int v, int u ) { - char pBuffer[10]; - int v, u; - nVars = Dau_Dsd6DecomposeConstCof( p, &t, pVars, nVars ); - if ( nVars == 0 ) - return; - // consider two-variable cofactors - for ( v = nVars - 1; v > 0; v-- ) + int Status = Dau_DsdLookupVarCache( p, pVars[v], pVars[u] ); + if ( Status == 0 ) { - word tCof0 = Abc_Tt6Cofactor0( t, v ); - word tCof1 = Abc_Tt6Cofactor1( t, v ); - unsigned uSupp0 = 0, uSupp1 = 0; - Kit_DsdPrintFromTruth( &t, 6 );printf( "\n" ); - pBuffer[0] = 0; - for ( u = v - 1; u >= 0; u-- ) + Status = (Abc_Tt6HasVar(tCof1, u) << 1) | Abc_Tt6HasVar(tCof0, u); + Dau_DsdInsertVarCache( p, pVars[v], pVars[u], Status ); + } + return Status; +} +static inline unsigned Dau_Dsd6FindSupports( Dau_Dsd_t * p, word * pTruth, int * pVars, int nVars, int v ) +{ + int u; + unsigned uSupports = 0; + word tCof0 = Abc_Tt6Cofactor0( pTruth[0], v ); + word tCof1 = Abc_Tt6Cofactor1( pTruth[0], v ); + for ( u = 0; u < nVars; u++ ) + if ( u != v ) + uSupports |= (Dau_Dsd6FindSupportOne( p, tCof0, tCof1, pVars, nVars, v, u ) << (2 * u)); + return uSupports; +} +static inline void Dau_DsdPrintSupports( unsigned uSupp, int nVars ) +{ + int v, Value; + printf( "Cofactor supports: " ); + for ( v = nVars - 1; v >= 0; v-- ) + { + Value = ((uSupp >> (2*v)) & 3); + if ( Value == 1 ) + printf( "01" ); + else if ( Value == 2 ) + printf( "10" ); + else if ( Value == 3 ) + printf( "11" ); + else + printf( "00" ); + if ( v ) + printf( "-" ); + } + printf( "\n" ); +} +// checks decomposability with respect to the pair (v, u) +static inline int Dau_Dsd6DecomposeDoubleVarsOne( Dau_Dsd_t * p, word * pTruth, int * pVars, int nVars, int v, int u ) +{ + char pBuffer[10] = { 0 }; + word tCof0 = Abc_Tt6Cofactor0( pTruth[0], v ); + word tCof1 = Abc_Tt6Cofactor1( pTruth[0], v ); + int Status = Dau_Dsd6FindSupportOne( p, tCof0, tCof1, pVars, nVars, v, u ); + assert( v > u ); +// Kit_DsdPrintFromTruth( (unsigned *)pTruth, 6 );printf( "\n" ); + if ( Status == 3 ) + { + // both F(v=0) and F(v=1) depend on u + if ( Abc_Tt6Cof0EqualCof1(tCof0, tCof1, u) && Abc_Tt6Cof0EqualCof1(tCof1, tCof0, u) ) // v+u { - if ( !Abc_Tt6HasVar(tCof0, u) ) - { - if ( Abc_Tt6HasVar(tCof1, u) ) - { - uSupp1 |= (1 << u); - // F(v=0) does not depend on u; F(v=1) depends on u - if ( Abc_Tt6Cof0EqualCof0(tCof0, tCof1, u) ) // vu - { - sprintf( pBuffer, "(%c%c)", 'a' + pVars[v], 'a' + pVars[u] ); - t = (s_Truths6[u] & Abc_Tt6Cofactor1(tCof1, u)) | (~s_Truths6[u] & Abc_Tt6Cofactor0(tCof0, u)); - break; - } - if ( Abc_Tt6Cof0EqualCof1(tCof0, tCof1, u) ) // v!u - { - sprintf( pBuffer, "(%c!%c)", 'a' + pVars[v], 'a' + pVars[u] ); - t = (s_Truths6[u] & Abc_Tt6Cofactor0(tCof1, u)) | (~s_Truths6[u] & Abc_Tt6Cofactor0(tCof0, u)); - break; - } - } - else assert( 0 ); // should depend on u - } - else - { - uSupp0 |= (1 << u); - if ( !Abc_Tt6HasVar(tCof1, u) ) - { - // F(v=0) depends on u; F(v=1) does not depend on u - if ( Abc_Tt6Cof0EqualCof1(tCof0, tCof1, u) ) // !vu - { - sprintf( pBuffer, "(!%c%c)", 'a' + pVars[v], 'a' + pVars[u] ); - t = (s_Truths6[u] & Abc_Tt6Cofactor1(tCof0, u)) | (~s_Truths6[u] & Abc_Tt6Cofactor0(tCof0, u)); - break; - } - if ( Abc_Tt6Cof1EqualCof1(tCof0, tCof1, u) ) // !v!u - { - sprintf( pBuffer, "(!%c!%c)", 'a' + pVars[v], 'a' + pVars[u] ); - t = (s_Truths6[u] & Abc_Tt6Cofactor0(tCof0, u)) | (~s_Truths6[u] & Abc_Tt6Cofactor1(tCof1, u)); - break; - } - } - else - { - uSupp1 |= (1 << u); - // both F(v=0) and F(v=1) depend on u - if ( Abc_Tt6Cof0EqualCof1(tCof0, tCof1, u) && Abc_Tt6Cof0EqualCof1(tCof1, tCof0, u) ) // v+u - { - t = (s_Truths6[u] & Abc_Tt6Cofactor1(tCof0, u)) | (~s_Truths6[u] & Abc_Tt6Cofactor0(tCof0, u)); - sprintf( pBuffer, "[%c%c]", 'a' + pVars[v], 'a' + pVars[u] ); - break; - } - } - } + pTruth[0] = (s_Truths6[u] & Abc_Tt6Cofactor1(tCof0, u)) | (~s_Truths6[u] & Abc_Tt6Cofactor0(tCof0, u)); + sprintf( pBuffer, "[%c%c]", 'a' + pVars[v], 'a' + pVars[u] ); + goto finish; } - // check if decomposition happened - if ( u >= 0 ) + } + else if ( Status == 2 ) + { + // F(v=0) does not depend on u; F(v=1) depends on u + if ( Abc_Tt6Cof0EqualCof0(tCof0, tCof1, u) ) // vu { - // finalize decomposition - assert( pBuffer[0] != 0 ); - pVars[u] = Dua_DsdAddVarDef( p, pBuffer ); - pVars[v] = pVars[nVars-1]; - Abc_TtSwapVars( &t, 6, v, nVars-1 ); - nVars = Dau_Dsd6DecomposeConstCof( p, &t, pVars, --nVars ); - v = Abc_MinInt( v, nVars - 1 ) + 1; - if ( nVars == 0 ) - return; - continue; + sprintf( pBuffer, "(%c%c)", 'a' + pVars[v], 'a' + pVars[u] ); + pTruth[0] = (s_Truths6[u] & Abc_Tt6Cofactor1(tCof1, u)) | (~s_Truths6[u] & Abc_Tt6Cofactor0(tCof0, u)); + goto finish; } - // check MUX decomposition w.r.t. u - if ( Abc_TtSuppOnlyOne( uSupp0 & ~uSupp1 ) && Abc_TtSuppOnlyOne( ~uSupp0 & uSupp1 ) ) + if ( Abc_Tt6Cof0EqualCof1(tCof0, tCof1, u) ) // v!u { - // check MUX - int iVar0 = Abc_TtSuppFindFirst( uSupp0 & ~uSupp1 ); - int iVar1 = Abc_TtSuppFindFirst( ~uSupp0 & uSupp1 ); - int iVarMin = Abc_MinInt( v, Abc_MinInt( iVar0, iVar1 ) ); - int fEqual0, fEqual1; - word C00, C01, C10, C11; - // check existence conditions - if ( iVar0 > iVar1 ) - ABC_SWAP( int, iVar0, iVar1 ); - assert( iVar0 < iVar1 ); -// fEqual0 = Abc_TtCheckEqualCofs( &t, 1, iVar0, iVar1, 0, 2 ) && Abc_TtCheckEqualCofs( &t, 1, iVar0, iVar1, 1, 3 ); -// fEqual1 = Abc_TtCheckEqualCofs( &t, 1, iVar0, iVar1, 0, 3 ) && Abc_TtCheckEqualCofs( &t, 1, iVar0, iVar1, 1, 2 ); - C00 = Abc_Tt6Cofactor0(tCof0, iVar0); - C01 = Abc_Tt6Cofactor1(tCof0, iVar0); - C10 = Abc_Tt6Cofactor0(tCof1, iVar1); - C11 = Abc_Tt6Cofactor1(tCof1, iVar1); - fEqual0 = (C00 == C10) && (C01 == C11); - fEqual1 = (C00 == C11) && (C01 == C10); - if ( fEqual0 || fEqual1 ) + sprintf( pBuffer, "(%c!%c)", 'a' + pVars[v], 'a' + pVars[u] ); + pTruth[0] = (s_Truths6[u] & Abc_Tt6Cofactor0(tCof1, u)) | (~s_Truths6[u] & Abc_Tt6Cofactor0(tCof0, u)); + goto finish; + } + } + else if ( Status == 1 ) + { + // F(v=0) depends on u; F(v=1) does not depend on u + if ( Abc_Tt6Cof0EqualCof1(tCof0, tCof1, u) ) // !vu + { + sprintf( pBuffer, "(!%c%c)", 'a' + pVars[v], 'a' + pVars[u] ); + pTruth[0] = (s_Truths6[u] & Abc_Tt6Cofactor1(tCof0, u)) | (~s_Truths6[u] & Abc_Tt6Cofactor0(tCof0, u)); + goto finish; + } + if ( Abc_Tt6Cof1EqualCof1(tCof0, tCof1, u) ) // !v!u + { + sprintf( pBuffer, "(!%c!%c)", 'a' + pVars[v], 'a' + pVars[u] ); + pTruth[0] = (s_Truths6[u] & Abc_Tt6Cofactor0(tCof0, u)) | (~s_Truths6[u] & Abc_Tt6Cofactor1(tCof1, u)); + goto finish; + } + } + return nVars; +finish: + // finalize decomposition + assert( pBuffer[0] ); + pVars[u] = Dau_DsdAddVarDef( p, pBuffer ); + pVars[v] = pVars[nVars-1]; + Abc_TtSwapVars( pTruth, 6, v, nVars-1 ); + if ( Dau_Dsd6DecomposeSingleVarOne( p, pTruth, pVars, --nVars, u ) ) + nVars = Dau_Dsd6DecomposeSingleVar( p, pTruth, pVars, --nVars ); + return nVars; +} +int Dau_Dsd6DecomposeDoubleVars( Dau_Dsd_t * p, word * pTruth, int * pVars, int nVars ) +{ + while ( 1 ) + { + int v, u, nVarsOld; + for ( v = nVars - 1; v > 0; v-- ) + { + for ( u = v - 1; u >= 0; u-- ) { - assert( iVarMin < iVar0 && iVar0 < iVar1 ); - t = (s_Truths6[iVarMin] & Abc_Tt6Cofactor0(tCof1, iVar1)) | (~s_Truths6[iVarMin] & Abc_Tt6Cofactor1(tCof1, iVar1)); - if ( fEqual1 ) - t = ~t; - sprintf( pBuffer, "<%c%c%c>", 'a' + pVars[v], 'a' + pVars[iVar1], 'a' + pVars[iVar0] ); - pVars[iVarMin] = Dua_DsdAddVarDef( p, pBuffer ); - pVars[iVar1] = pVars[nVars-1]; - Abc_TtSwapVars( &t, 6, iVar1, nVars-1 ); - pVars[iVar0] = pVars[nVars-2]; - Abc_TtSwapVars( &t, 6, iVar0, nVars-2 ); - nVars -= 2; - nVars = Dau_Dsd6DecomposeConstCof( p, &t, pVars, nVars ); - v = Abc_MinInt( v, nVars - 1 ) + 1; + if ( Dau_DsdLookupVarCache( p, v, u ) ) + continue; + nVarsOld = nVars; + nVars = Dau_Dsd6DecomposeDoubleVarsOne( p, pTruth, pVars, nVars, v, u ); if ( nVars == 0 ) - return; - break; + return 0; + if ( nVarsOld > nVars ) + break; } + if ( u >= 0 ) // found + break; } + if ( v == 0 ) // not found + break; + } + return nVars; +} - -/* - // get the single variale cofactors - Kit_TruthCofactor0New( pCofs2[0], pTruth, pObj->nFans, i ); // tCof0 - Kit_TruthCofactor1New( pCofs2[1], pTruth, pObj->nFans, i ); // tCof1 - // get four cofactors - Kit_TruthCofactor0New( pCofs4[0][0], pCofs2[0], pObj->nFans, iLit0 ); // Abc_Tt6Cofactor0(tCof0, iLit0) - Kit_TruthCofactor1New( pCofs4[0][1], pCofs2[0], pObj->nFans, iLit0 ); // Abc_Tt6Cofactor1(tCof0, iLit0) - Kit_TruthCofactor0New( pCofs4[1][0], pCofs2[1], pObj->nFans, iLit1 ); // Abc_Tt6Cofactor0(tCof1, iLit1) - Kit_TruthCofactor1New( pCofs4[1][1], pCofs2[1], pObj->nFans, iLit1 ); // Abc_Tt6Cofactor1(tCof1, iLit1) - // check existence conditions - fEquals[0][0] = Kit_TruthIsEqual( pCofs4[0][0], pCofs4[1][0], pObj->nFans ); - fEquals[0][1] = Kit_TruthIsEqual( pCofs4[0][1], pCofs4[1][1], pObj->nFans ); - fEquals[1][0] = Kit_TruthIsEqual( pCofs4[0][0], pCofs4[1][1], pObj->nFans ); - fEquals[1][1] = Kit_TruthIsEqual( pCofs4[0][1], pCofs4[1][0], pObj->nFans ); - if ( (fEquals[0][0] && fEquals[0][1]) || (fEquals[1][0] && fEquals[1][1]) ) +// look for MUX-decomposable variable on top or at the bottom +static inline int Dau_Dsd6DecomposeTripleVarsOuter( Dau_Dsd_t * p, word * pTruth, int * pVars, int nVars, int v ) +{ + extern void Dau_DsdDecomposeInt( Dau_Dsd_t * p, word * pTruth, int nVarsInit ); + Dau_Dsd_t P1, * p1 = &P1; + Dau_Dsd_t P2, * p2 = &P2; + word tCof0, tCof1; + // move this variable to the top + pVars[v] = pVars[nVars-1]; + Abc_TtSwapVars( pTruth, 6, v, nVars-1 ); + // cofactor w.r.t the last variable + tCof0 = Abc_Tt6Cofactor0( pTruth[0], nVars - 1 ); + tCof1 = Abc_Tt6Cofactor1( pTruth[0], nVars - 1 ); + // split decomposition + Dau_DsdDecomposeInt( p1, &tCof0, nVars - 1 ); + Dau_DsdDecomposeInt( p2, &tCof1, nVars - 1 ); + p->nSizeNonDec = Abc_MaxInt( p1->nSizeNonDec, p2->nSizeNonDec ); + // compose the result + Dau_DsdWriteString( p, "<" ); + Dau_DsdWriteVar( p, pVars[nVars - 1], 0 ); + Dau_DsdTranslate( p, pVars, nVars - 1, p1->pOutput ); + Dau_DsdTranslate( p, pVars, nVars - 1, p2->pOutput ); + Dau_DsdWriteString( p, ">" ); + return 0; +} +static inline int Dau_Dsd6DecomposeTripleVarsInner( Dau_Dsd_t * p, word * pTruth, int * pVars, int nVars, int v, unsigned uSupports ) +{ + int iVar0 = Abc_TtSuppFindFirst( uSupports & (~uSupports >> 1) & 0x55555555 ) >> 1; + int iVar1 = Abc_TtSuppFindFirst( ~uSupports & ( uSupports >> 1) & 0x55555555 ) >> 1; + word tCof0 = Abc_Tt6Cofactor0( pTruth[0], v ); + word tCof1 = Abc_Tt6Cofactor1( pTruth[0], v ); + word C00 = Abc_Tt6Cofactor0( tCof0, iVar0 ); + word C01 = Abc_Tt6Cofactor1( tCof0, iVar0 ); + word C10 = Abc_Tt6Cofactor0( tCof1, iVar1 ); + word C11 = Abc_Tt6Cofactor1( tCof1, iVar1 ); + int fEqual0 = (C00 == C10) && (C01 == C11); + int fEqual1 = (C00 == C11) && (C01 == C10); +// assert( iVar0 < iVar1 ); +// fEqual0 = Abc_TtCheckEqualCofs( &t, 1, iVar0, iVar1, 0, 2 ) && Abc_TtCheckEqualCofs( &t, 1, iVar0, iVar1, 1, 3 ); +// fEqual1 = Abc_TtCheckEqualCofs( &t, 1, iVar0, iVar1, 0, 3 ) && Abc_TtCheckEqualCofs( &t, 1, iVar0, iVar1, 1, 2 ); + if ( fEqual0 || fEqual1 ) + { + char pBuffer[10]; + int iVarMin = Abc_MinInt( v, Abc_MinInt( iVar0, iVar1 ) ); +// assert( iVarMin < iVar0 && iVar0 < iVar1 ); + pTruth[0] = (s_Truths6[iVarMin] & Abc_Tt6Cofactor0(tCof1, iVar1)) | (~s_Truths6[iVarMin] & Abc_Tt6Cofactor1(tCof1, iVar1)); + if ( fEqual1 ) + pTruth[0] = ~pTruth[0]; + sprintf( pBuffer, "<%c%c%c>", 'a' + pVars[v], 'a' + pVars[iVar1], 'a' + pVars[iVar0] ); + pVars[iVarMin] = Dau_DsdAddVarDef( p, pBuffer ); + + pVars[iVar1] = pVars[nVars-1]; + Abc_TtSwapVars( pTruth, 6, iVar1, nVars-1 ); + pVars[iVar0] = pVars[nVars-2]; + Abc_TtSwapVars( pTruth, 6, iVar0, nVars-2 ); + nVars -= 2; + return Dau_Dsd6DecomposeSingleVar( p, pTruth, pVars, nVars ); + } + return nVars; +} +int Dau_Dsd6DecomposeTripleVars( Dau_Dsd_t * p, word * pTruth, int * pVars, int nVars ) +{ + while ( 1 ) + { + int v; + for ( v = nVars - 1; v >= 0; v-- ) + { + unsigned uSupports = Dau_Dsd6FindSupports( p, pTruth, pVars, nVars, v ); + Dau_DsdPrintSupports( uSupports, nVars ); + if ( (uSupports & (uSupports >> 1) & 0x55555555) == 0 ) // non-overlapping supports + return Dau_Dsd6DecomposeTripleVarsOuter( p, pTruth, pVars, nVars, v ); + if ( Abc_TtSuppOnlyOne( uSupports & (~uSupports >> 1) & 0x55555555) || + Abc_TtSuppOnlyOne(~uSupports & ( uSupports >> 1) & 0x55555555) ) // one unique variable in each cofactor { - // construct the MUX - pRes = Kit_DsdObjAlloc( pNtk, KIT_DSD_PRIME, 3 ); - Kit_DsdObjTruth(pRes)[0] = 0xCACACACA; - pRes->nRefs++; - pRes->nFans = 3; - pRes->pFans[0] = pObj->pFans[iLit0]; pObj->pFans[iLit0] = 127; uSupp &= ~(1 << iLit0); - pRes->pFans[1] = pObj->pFans[iLit1]; pObj->pFans[iLit1] = 127; uSupp &= ~(1 << iLit1); - pRes->pFans[2] = pObj->pFans[i]; pObj->pFans[i] = 2 * pRes->Id; // remains in support - // update the node -// if ( fEquals[0][0] && fEquals[0][1] ) -// Kit_TruthMuxVar( pTruth, pCofs4[0][0], pCofs4[0][1], pObj->nFans, i ); -// else -// Kit_TruthMuxVar( pTruth, pCofs4[0][1], pCofs4[0][0], pObj->nFans, i ); - Kit_TruthMuxVar( pTruth, pCofs4[1][0], pCofs4[1][1], pObj->nFans, i ); - if ( fEquals[1][0] && fEquals[1][1] ) - pRes->pFans[0] = Abc_LitNot(pRes->pFans[0]); - // decompose the remainder - Kit_DsdDecompose_rec( pNtk, pObj, uSupp, pPar, nDecMux ); - return; + nVars = Dau_Dsd6DecomposeTripleVarsInner( p, pTruth, pVars, nVars, v, uSupports ); + if ( nVars == 0 ) + return 0; + nVars = Dau_Dsd6DecomposeDoubleVars( p, pTruth, pVars, nVars ); + if ( nVars == 0 ) + return 0; + break; } -*/ + } + if ( v == -1 ) + return nVars; + } + assert( 0 ); + return -1; +} +void Dau_Dsd6DecomposeInternal( Dau_Dsd_t * p, word * pTruth, int * pVars, int nVars ) +{ + // decompose single variales on the output side + nVars = Dau_Dsd6DecomposeSingleVar( p, pTruth, pVars, nVars ); + if ( nVars == 0 ) + return; + // decompose double variables on the input side + nVars = Dau_Dsd6DecomposeDoubleVars( p, pTruth, pVars, nVars ); + if ( nVars == 0 ) + return; + // decompose MUX on the output/input side + nVars = Dau_Dsd6DecomposeTripleVars( p, pTruth, pVars, nVars ); + if ( nVars == 0 ) + return; + // write non-decomposable function + Dau_DsdWritePrime( p, pTruth, pVars, nVars ); +} +/**Function************************************************************* + Synopsis [Procedures specialized for 6-variable functions.] -/* - // check MUX decomposition w.r.t. u - if ( (uSupp0 & uSupp1) == 0 ) - { - // perform MUX( v, F(v=1), F(v=0) ) - } -*/ - } - // this non-DSD-decomposable function - assert( nVars > 2 ); - // write truth table - p->nPos += Abc_TtWriteHexRev( p->pOutput + p->nPos, &t, nVars ); - Dua_DsdWrite( p, "{" ); - for ( v = 0; v < nVars; v++ ) - Dua_DsdWriteVar( p, pVars[v], 0 ); - Dua_DsdWrite( p, "}" ); + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Dau_DsdDecomposeSingleVar( Dau_Dsd_t * p, word * pTruth, int * pVars, int nVars ) +{ + return 0; +} +int Dau_DsdDecomposeDoubleVars( Dau_Dsd_t * p, word * pTruth, int * pVars, int nVars ) +{ + return 0; +} +int Dau_DsdDecomposeTripleVars( Dau_Dsd_t * p, word * pTruth, int * pVars, int nVars ) +{ + return 0; } void Dau_DsdDecomposeInternal( Dau_Dsd_t * p, word * pTruth, int * pVars, int nVars ) { + // decompose single variales on the output side + nVars = Dau_DsdDecomposeSingleVar( p, pTruth, pVars, nVars ); + if ( nVars == 0 ) + return; + // decompose double variables on the input side + nVars = Dau_DsdDecomposeDoubleVars( p, pTruth, pVars, nVars ); + if ( nVars == 0 ) + return; + // decompose MUX on the output/input side + nVars = Dau_DsdDecomposeTripleVars( p, pTruth, pVars, nVars ); + if ( nVars == 0 ) + return; + // write non-decomposable function + Dau_DsdWritePrime( p, pTruth, pVars, nVars ); } -char * Dau_DsdDecompose( word * pTruth, int nVarsInit ) + +/**Function************************************************************* + + Synopsis [Fast DSD for truth tables.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Dau_DsdDecomposeInt( Dau_Dsd_t * p, word * pTruth, int nVarsInit ) { - Dau_Dsd_t P, * p = &P; int nVars, pVars[16]; - Dua_DsdInit( p, nVarsInit ); + Dau_DsdInitialize( p, nVarsInit ); + nVars = Dau_DsdMinBase( pTruth, nVarsInit, pVars ); + assert( nVars > 0 && nVars <= 6 ); + if ( nVars == 1 ) + Dau_DsdWriteVar( p, pVars[0], (int)(pTruth[0] & 1) ); + else if ( nVars <= 6 ) + Dau_Dsd6DecomposeInternal( p, pTruth, pVars, nVars ); + else + Dau_DsdDecomposeInternal( p, pTruth, pVars, nVars ); + Dau_DsdFinalize( p ); +} +char * Dau_DsdDecompose( word * pTruth, int nVarsInit, int * pnSizeNonDec ) +{ + static Dau_Dsd_t P; + Dau_Dsd_t * p = &P; if ( (pTruth[0] & 1) == 0 && Abc_TtIsConst0(pTruth, Abc_TtWordNum(nVarsInit)) ) - Dua_DsdWrite( p, "0" ); + p->pOutput[0] = '0', p->pOutput[1] = 0; else if ( (pTruth[0] & 1) && Abc_TtIsConst1(pTruth, Abc_TtWordNum(nVarsInit)) ) - Dua_DsdWrite( p, "1" ); + p->pOutput[0] = '1', p->pOutput[1] = 0; else { - nVars = Dua_DsdMinBase( pTruth, nVarsInit, pVars ); - assert( nVars > 0 && nVars <= 6 ); - if ( nVars == 1 ) - Dua_DsdWriteVar( p, pVars[0], (int)(pTruth[0] & 1) ); - else if ( nVars <= 6 ) - Dau_Dsd6DecomposeInternal( p, pTruth[0], pVars, nVars ); - else - Dau_DsdDecomposeInternal( p, pTruth, pVars, nVars ); + Dau_DsdDecomposeInt( p, pTruth, nVarsInit ); + Dau_DsdCleanBraces( p->pOutput ); + if ( pnSizeNonDec ) + *pnSizeNonDec = p->nSizeNonDec; } - Dua_DsdWriteStop( p ); - Dau_DsdCleanBraces( p->pOutput ); return p->pOutput; } void Dau_DsdTest() { // char * pStr = "(!(!a<bcd>)!(!fe))"; - char * pStr = "<cba>"; +// char * pStr = "<cba>"; +// char * pStr = "!(f!(b!c!(d[ea])))"; + char * pStr = "[!(a[be])!(c!df)]"; char * pStr2; word t = Dau_DsdToTruth( pStr ); return; - pStr2 = Dau_DsdDecompose( &t, 6 ); + pStr2 = Dau_DsdDecompose( &t, 6, NULL ); t = 0; } |