diff options
-rw-r--r-- | abclib.dsp | 4 | ||||
-rw-r--r-- | src/base/abci/abcDec.c | 4 | ||||
-rw-r--r-- | src/opt/dau/dau.h | 11 | ||||
-rw-r--r-- | src/opt/dau/dauDsd.c | 437 | ||||
-rw-r--r-- | src/opt/dau/dauMerge.c | 722 | ||||
-rw-r--r-- | src/opt/dau/module.make | 3 |
6 files changed, 1036 insertions, 145 deletions
@@ -1997,6 +1997,10 @@ SOURCE=.\src\opt\dau\dauEnum.c SOURCE=.\src\opt\dau\dauInt.h # End Source File +# Begin Source File + +SOURCE=.\src\opt\dau\dauMerge.c +# End Source File # End Group # End Group # Begin Group "map" diff --git a/src/base/abci/abcDec.c b/src/base/abci/abcDec.c index f5dce96e..94b4ef07 100644 --- a/src/base/abci/abcDec.c +++ b/src/base/abci/abcDec.c @@ -541,7 +541,7 @@ void Abc_TruthDecPerform( Abc_TtStore_t * p, int DecType, int fVerbose ) } else if ( DecType == 4 ) { - extern void Dau_DsdTestOne( word t, int i ); +// extern void Dau_DsdTestOne( word t, int i ); if ( p->nVars != 6 ) { printf( "Currently only works for 6 variables.\n" ); @@ -554,7 +554,7 @@ void Abc_TruthDecPerform( Abc_TtStore_t * p, int DecType, int fVerbose ) { if ( fVerbose ) printf( "%7d : ", i ); - Dau_DsdTestOne( *p->pFuncs[i], i ); +// Dau_DsdTestOne( *p->pFuncs[i], i ); } } else assert( 0 ); diff --git a/src/opt/dau/dau.h b/src/opt/dau/dau.h index 78b1535c..f9d4f2b2 100644 --- a/src/opt/dau/dau.h +++ b/src/opt/dau/dau.h @@ -37,9 +37,11 @@ /// PARAMETERS /// //////////////////////////////////////////////////////////////////////// - ABC_NAMESPACE_HEADER_START +#define DAU_MAX_VAR 16 // should be 6 or more +#define DAU_MAX_STR 256 +#define DAU_MAX_WORD (1<<(DAU_MAX_VAR-6)) //////////////////////////////////////////////////////////////////////// /// BASIC TYPES /// @@ -56,9 +58,14 @@ ABC_NAMESPACE_HEADER_START /*=== dauCanon.c ==========================================================*/ extern unsigned Abc_TtCanonicize( word * pTruth, int nVars, char * pCanonPerm ); /*=== dauDsd.c ==========================================================*/ -extern char * Dau_DsdDecompose( word * pTruth, int nVarsInit, int * pnSizeNonDec ); +extern int Dau_DsdDecompose( word * pTruth, int nVarsInit, int fSplitPrime, char * pRes ); extern word * Dau_DsdToTruth( char * p, int nVars ); +extern word Dau_Dsd6ToTruth( char * p ); +extern void Dau_DsdNormalize( char * p ); +/*=== dauMerge.c ==========================================================*/ +extern void Dau_DsdRemoveBraces( char * pDsd, int * pMatches ); +extern char * Dau_DsdMerge( char * pDsd0i, int * pPerm0, char * pDsd1i, int * pPerm1, int fCompl0, int fCompl1 ); ABC_NAMESPACE_HEADER_END diff --git a/src/opt/dau/dauDsd.c b/src/opt/dau/dauDsd.c index b291a2a0..80782429 100644 --- a/src/opt/dau/dauDsd.c +++ b/src/opt/dau/dauDsd.c @@ -28,10 +28,6 @@ ABC_NAMESPACE_IMPL_START /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// -#define DAU_MAX_VAR 16 // should be 6 or more -#define DAU_MAX_STR 256 -#define DAU_MAX_WORD (1<<(DAU_MAX_VAR-6)) - /* This code performs truth-table-based decomposition for 6-variable functions. Representation of operations: @@ -73,70 +69,8 @@ int * Dau_DsdComputeMatches( char * p ) assert( nNested < DAU_MAX_VAR ); } assert( nNested == 0 ); -/* - // verify - for ( v = 0; p[v]; v++ ) - if ( p[v] == '(' || p[v] == '[' || p[v] == '<' || p[v] == '{' ) - assert( pMatches[v] > 0 ); - else - assert( pMatches[v] == 0 ); -*/ return pMatches; } -char * Dau_DsdFindMatch( char * p ) -{ - int Counter = 0; - assert( *p == '(' || *p == '[' || *p == '<' || *p == '{' ); - while ( *p ) - { - if ( *p == '(' || *p == '[' || *p == '<' || *p == '{' ) - Counter++; - else if ( *p == ')' || *p == ']' || *p == '>' || *p == '}' ) - Counter--; - if ( Counter == 0 ) - return p; - p++; - } - return NULL; -} -static inline void Dau_DsdCleanBraces( char * p ) -{ - char * q, Last = -1; - int i; - for ( i = 0; p[i]; i++ ) - { - if ( p[i] == '(' || p[i] == '[' || p[i] == '<' ) - { - if ( p[i] != '<' && p[i] == Last && i > 0 && p[i-1] != '!' ) - { - q = Dau_DsdFindMatch( p + i ); - assert( (p[i] == '(') == (*q == ')') ); - assert( (p[i] == '[') == (*q == ']') ); - p[i] = *q = 'x'; - } - else - Last = p[i]; - } - else if ( p[i] == ')' || p[i] == ']' || p[i] == '>' ) - Last = -1; - } -/* - if ( p[0] == '(' ) - { - assert( p[i-1] == ')' ); - p[0] = p[i-1] = 'x'; - } - else if ( p[0] == '[' ) - { - assert( p[i-1] == ']' ); - p[0] = p[i-1] = 'x'; - } -*/ - for ( q = p; *p; p++ ) - if ( *p != 'x' ) - *q++ = *p; - *q = 0; -} /**Function************************************************************* @@ -180,6 +114,130 @@ void Dau_DsdPermute( char * pDsd ) *pDsd = 'a' + pPerm[*pDsd - 'a']; } +/**Function************************************************************* + + Synopsis [Normalize the ordering of components.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +char * Dau_DsdNormalizeCopy( char * pDest, char * pSour, int * pMarks, int i ) +{ + int s; + for ( s = pMarks[i]; s < pMarks[i+1]; s++ ) + *pDest++ = pSour[s]; + return pDest; +} +int Dau_DsdNormalizeCompare( char * pStr, int * pMarks, int i, int j ) +{ + char * pStr1 = pStr + pMarks[i]; + char * pStr2 = pStr + pMarks[j]; + char * pLimit1 = pStr + pMarks[i+1]; + char * pLimit2 = pStr + pMarks[j+1]; + for ( ; pStr1 < pLimit1 && pStr2 < pLimit2; pStr1++, pStr2++ ) + { + if ( !(*pStr1 >= 'a' && *pStr1 <= 'z') ) + { + pStr2--; + continue; + } + if ( !(*pStr2 >= 'a' && *pStr2 <= 'z') ) + { + pStr1--; + continue; + } + if ( *pStr1 < *pStr2 ) + return -1; + if ( *pStr1 > *pStr2 ) + return 1; + } + assert( pStr1 < pLimit1 || pStr2 < pLimit2 ); + if ( pStr1 == pLimit1 ) + return -1; + if ( pStr2 == pLimit2 ) + return 1; + assert( 0 ); + return 0; +} +int * Dau_DsdNormalizePerm( char * pStr, int * pMarks, int nMarks ) +{ + static int pPerm[DAU_MAX_VAR]; + int i, k; + for ( i = 0; i < nMarks; i++ ) + pPerm[i] = i; + for ( i = 0; i < nMarks; i++ ) + { + int iBest = i; + for ( k = i + 1; k < nMarks; k++ ) + if ( Dau_DsdNormalizeCompare( pStr, pMarks, pPerm[iBest], pPerm[k] ) == 1 ) + iBest = k; + ABC_SWAP( int, pPerm[i], pPerm[iBest] ); + } + return pPerm; +} +void Dau_DsdNormalize_rec( char * pStr, char ** p, int * pMatches ) +{ + static char pBuffer[DAU_MAX_STR]; + if ( **p == '!' ) + (*p)++; + if ( **p >= 'a' && **p <= 'f' ) // var + return; + if ( **p == '(' || **p == '[' ) // and/or/xor + { + char * pStore, * pOld = *p + 1; + char * q = pStr + pMatches[ *p - pStr ]; + int i, * pPerm, nMarks = 0, pMarks[DAU_MAX_VAR+1]; + assert( *q == **p + 1 + (**p != '(') ); + for ( (*p)++; *p < q; (*p)++ ) + { + pMarks[nMarks++] = *p - pStr; + Dau_DsdNormalize_rec( pStr, p, pMatches ); + } + pMarks[nMarks] = *p - pStr; + assert( *p == q ); + // add to buffer in good order + pPerm = Dau_DsdNormalizePerm( pStr, pMarks, nMarks ); + // copy to the buffer + pStore = pBuffer; + for ( i = 0; i < nMarks; i++ ) + pStore = Dau_DsdNormalizeCopy( pStore, pStr, pMarks, pPerm[i] ); + assert( pStore - pBuffer == *p - pOld ); + memcpy( pOld, pBuffer, pStore - pBuffer ); + return; + } + if ( **p == '<' || **p == '{' ) // mux + { + char * q = pStr + pMatches[ *p - pStr ]; + assert( *q == **p + 1 + (**p != '(') ); + if ( (**p == '<') && (*(q+1) == '{') ) + { + *p = q+1; + Dau_DsdNormalize_rec( pStr, p, pMatches ); + return; + } + for ( (*p)++; *p < q; (*p)++ ) + Dau_DsdNormalize_rec( pStr, p, pMatches ); + assert( *p == q ); + return; + } + if ( (**p >= 'A' && **p <= 'F') || (**p >= '0' && **p <= '9') ) + { + (*p)++; + return; + } + assert( 0 ); +} +void Dau_DsdNormalize( char * pDsd ) +{ + if ( pDsd[1] != 0 ) + Dau_DsdNormalize_rec( pDsd, &pDsd, Dau_DsdComputeMatches(pDsd) ); +} + + /**Function************************************************************* @@ -211,7 +269,7 @@ word Dau_Dsd6TruthCompose_rec( word Func, word * pFanins, int nVars ) t1 = Dau_Dsd6TruthCompose_rec( Abc_Tt6Cofactor1(Func, nVars), pFanins, nVars ); return (~pFanins[nVars] & t0) | (pFanins[nVars] & t1); } -word Dau_Dsd6ToTruth_rec( char * pStr, char ** p, int * pMatches ) +word Dau_Dsd6ToTruth_rec( char * pStr, char ** p, int * pMatches, word * pTruths ) { int fCompl = 0; if ( **p == '!' ) @@ -219,7 +277,7 @@ word Dau_Dsd6ToTruth_rec( char * pStr, char ** p, int * pMatches ) if ( **p >= 'a' && **p <= 'f' ) // var { assert( **p - 'a' >= 0 && **p - 'a' < 6 ); - return fCompl ? ~s_Truths6[**p - 'a'] : s_Truths6[**p - 'a']; + return fCompl ? ~pTruths[**p - 'a'] : pTruths[**p - 'a']; } if ( **p == '(' ) // and/or { @@ -227,7 +285,7 @@ word Dau_Dsd6ToTruth_rec( char * pStr, char ** p, int * pMatches ) word Res = ~(word)0; assert( **p == '(' && *q == ')' ); for ( (*p)++; *p < q; (*p)++ ) - Res &= Dau_Dsd6ToTruth_rec( pStr, p, pMatches ); + Res &= Dau_Dsd6ToTruth_rec( pStr, p, pMatches, pTruths ); assert( *p == q ); return fCompl ? ~Res : Res; } @@ -237,19 +295,51 @@ word Dau_Dsd6ToTruth_rec( char * pStr, char ** p, int * pMatches ) word Res = 0; assert( **p == '[' && *q == ']' ); for ( (*p)++; *p < q; (*p)++ ) - Res ^= Dau_Dsd6ToTruth_rec( pStr, p, pMatches ); + Res ^= Dau_Dsd6ToTruth_rec( pStr, p, pMatches, pTruths ); assert( *p == q ); return fCompl ? ~Res : Res; } if ( **p == '<' ) // mux { - char * q = pStr + pMatches[ *p - pStr ]; + int nVars = 0; word Temp[3], * pTemp = Temp, Res; + word Fanins[6], * pTruths2; + char * pOld = *p; + char * q = pStr + pMatches[ *p - pStr ]; + // read fanins + if ( *(q+1) == '{' ) + { + char * q2; + *p = q+1; + q2 = pStr + pMatches[ *p - pStr ]; + assert( **p == '{' && *q2 == '}' ); + for ( nVars = 0, (*p)++; *p < q2; (*p)++, nVars++ ) + Fanins[nVars] = Dau_Dsd6ToTruth_rec( pStr, p, pMatches, pTruths ); + assert( *p == q2 ); + pTruths2 = Fanins; + } + else + pTruths2 = pTruths; + // read MUX + *p = pOld; + q = pStr + pMatches[ *p - pStr ]; assert( **p == '<' && *q == '>' ); + // verify internal variables + if ( nVars ) + for ( ; pOld < q; pOld++ ) + if ( *pOld >= 'a' && *pOld <= 'z' ) + assert( *pOld - 'a' < nVars ); + // derive MAX components for ( (*p)++; *p < q; (*p)++ ) - *pTemp++ = Dau_Dsd6ToTruth_rec( pStr, p, pMatches ); + *pTemp++ = Dau_Dsd6ToTruth_rec( pStr, p, pMatches, pTruths2 ); assert( pTemp == Temp + 3 ); assert( *p == q ); + if ( *(q+1) == '{' ) // and/or + { + char * q = pStr + pMatches[ ++(*p) - pStr ]; + assert( **p == '{' && *q == '}' ); + *p = q; + } Res = (Temp[0] & Temp[1]) | (~Temp[0] & Temp[2]); return fCompl ? ~Res : Res; } @@ -262,7 +352,7 @@ word Dau_Dsd6ToTruth_rec( char * pStr, char ** p, int * pMatches ) q = pStr + pMatches[ *p - pStr ]; assert( **p == '{' && *q == '}' ); for ( i = 0, (*p)++; *p < q; (*p)++, i++ ) - Fanins[i] = Dau_Dsd6ToTruth_rec( pStr, p, pMatches ); + Fanins[i] = Dau_Dsd6ToTruth_rec( pStr, p, pMatches, pTruths ); assert( i == nVars ); assert( *p == q ); Res = Dau_Dsd6TruthCompose_rec( Func, Fanins, nVars ); @@ -279,7 +369,7 @@ word Dau_Dsd6ToTruth( char * p ) else if ( *p == '1' && *(p+1) == 0 ) Res = ~(word)0; else - Res = Dau_Dsd6ToTruth_rec( p, &p, Dau_DsdComputeMatches(p) ); + Res = Dau_Dsd6ToTruth_rec( p, &p, Dau_DsdComputeMatches(p), s_Truths6 ); assert( *++p == 0 ); return Res; } @@ -495,7 +585,7 @@ void Dau_DsdTest2() ***********************************************************************/ static inline int Dau_DsdPerformReplace( char * pBuffer, int PosStart, int Pos, int Symb, char * pNext ) { - static char pTemp[DAU_MAX_STR+20]; + static char pTemp[DAU_MAX_STR]; char * pCur = pTemp; int i, k, RetValue; for ( i = PosStart; i < Pos; i++ ) @@ -666,7 +756,7 @@ int Dau_DsdPerform_rec( word t, char * pBuffer, int Pos, int * pVars, int nVars } char * Dau_DsdPerform( word t ) { - static char pBuffer[DAU_MAX_STR+20]; + static char pBuffer[DAU_MAX_STR]; int pVarsNew[6] = {0, 1, 2, 3, 4, 5}; int Pos = 0; if ( t == 0 ) @@ -678,7 +768,7 @@ char * Dau_DsdPerform( word t ) pBuffer[Pos++] = 0; // printf( "%d ", strlen(pBuffer) ); // printf( "%s ->", pBuffer ); - Dau_DsdCleanBraces( pBuffer ); + Dau_DsdRemoveBraces( pBuffer, Dau_DsdComputeMatches(pBuffer) ); // printf( " %s\n", pBuffer ); return pBuffer; } @@ -713,34 +803,55 @@ void Dau_DsdTest3() if ( t != t2 ) printf( "Verification failed.\n" ); } -void Dau_DsdTestOne( word t, int i ) -{ - int nSizeNonDec; - word t2; -// char * p = Dau_DsdPerform( t ); - char * p = Dau_DsdDecompose( &t, 6, &nSizeNonDec ); - return; - t2 = Dau_Dsd6ToTruth( p ); - if ( t != t2 ) - { - printf( "Verification failed. " ); - printf( "%8d : ", i ); - printf( "%30s ", p ); -// Kit_DsdPrintFromTruth( (unsigned *)&t, 6 ); -// printf( " " ); -// Kit_DsdPrintFromTruth( (unsigned *)&t2, 6 ); - printf( "\n" ); - } -} -/* - extern void Dau_DsdTestOne( word t, int i ); - assert( p->nVars == 6 ); - Dau_DsdTestOne( *p->pFuncs[i], i ); -*/ +/**Function************************************************************* + + Synopsis [Find the best cofactoring variable.] + + Description [Return -2 if non-DSD; -1 if full DSD; otherwise, + returns cofactoring variables i (i >= 0).] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Dau_DsdCheck1Step( word * pTruth, int nVarsInit ) +{ + word pCofTemp[DAU_MAX_WORD]; + int nWords = Abc_TtWordNum(nVarsInit); + int nSizeNonDec, nSizeNonDec0, nSizeNonDec1; + int v, vBest = -2, nSumCofsBest = ABC_INFINITY, nSumCofs; + nSizeNonDec = Dau_DsdDecompose( pTruth, nVarsInit, 0, NULL ); + if ( nSizeNonDec == 0 ) + return -1; + assert( nSizeNonDec > 0 ); + for ( v = 0; v < nVarsInit; v++ ) + { + // try first cofactor + Abc_TtCopy( pCofTemp, pTruth, nWords, 0 ); + Abc_TtCofactor0( pCofTemp, nWords, v ); + nSumCofs = Abc_TtSupportSize( pCofTemp, nVarsInit ); + nSizeNonDec0 = Dau_DsdDecompose( pCofTemp, nVarsInit, 0, NULL ); + // try second cofactor + Abc_TtCopy( pCofTemp, pTruth, nWords, 0 ); + Abc_TtCofactor1( pCofTemp, nWords, v ); + nSumCofs += Abc_TtSupportSize( pCofTemp, nVarsInit ); + nSizeNonDec1 = Dau_DsdDecompose( pCofTemp, nVarsInit, 0, NULL ); + // compare cofactors + if ( nSizeNonDec0 || nSizeNonDec1 ) + continue; + if ( nSumCofsBest > nSumCofs ) + { + vBest = v; + nSumCofsBest = nSumCofs; + } + } + return vBest; +} /**Function************************************************************* @@ -762,6 +873,7 @@ struct Dau_Dsd_t_ int nSizeNonDec; // size of the largest non-decomposable block int nConsts; // the number of constant decompositions int uConstMask; // constant decomposition mask + int fSplitPrime; // represent prime function as 1-step DSD char pVarDefs[32][8]; // variable definitions char Cache[32][32]; // variable cache char pOutput[DAU_MAX_STR]; // output stream @@ -821,16 +933,49 @@ static inline void Dau_DsdTranslate( Dau_Dsd_t * p, int * pVars, int nVars, char else p->pOutput[ p->nPos++ ] = *pStr; } -static inline void Dau_DsdWritePrime( Dau_Dsd_t * p, word * pTruth, int * pVars, int nVars ) +static inline int Dau_DsdWritePrime( Dau_Dsd_t * p, word * pTruth, int * pVars, int nVars ) { - int v; + int v, RetValue = 2; assert( nVars > 2 ); - p->nPos += Abc_TtWriteHexRev( p->pOutput + p->nPos, pTruth, nVars ); + if ( p->fSplitPrime ) + { + word pCofTemp[DAU_MAX_WORD]; + int nWords = Abc_TtWordNum(nVars); + int vBest = Dau_DsdCheck1Step( pTruth, nVars ); + assert( vBest != -1 ); + if ( vBest == -2 ) // non-dec + p->nPos += Abc_TtWriteHexRev( p->pOutput + p->nPos, pTruth, nVars ); + else + { + char pRes[DAU_MAX_STR]; + int nNonDecSize; + // compose the result + Dau_DsdWriteString( p, "<" ); + Dau_DsdWriteVar( p, pVars[vBest], 0 ); + // split decomposition + Abc_TtCopy( pCofTemp, pTruth, nWords, 0 ); + Abc_TtCofactor1( pCofTemp, nWords, vBest ); + nNonDecSize = Dau_DsdDecompose( pCofTemp, nVars, 0, pRes ); + assert( nNonDecSize == 0 ); + Dau_DsdWriteString( p, pRes ); + // split decomposition + Abc_TtCopy( pCofTemp, pTruth, nWords, 0 ); + Abc_TtCofactor0( pCofTemp, nWords, vBest ); + nNonDecSize = Dau_DsdDecompose( pCofTemp, nVars, 0, pRes ); + assert( nNonDecSize == 0 ); + Dau_DsdWriteString( p, pRes ); + Dau_DsdWriteString( p, ">" ); + RetValue = 1; + } + } + else + 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; + return RetValue; } static inline void Dau_DsdFinalize( Dau_Dsd_t * p ) { @@ -1012,6 +1157,8 @@ static inline int Dau_Dsd6DecomposeDoubleVarsOne( Dau_Dsd_t * p, word * pTruth, word tCof1 = Abc_Tt6Cofactor1( pTruth[0], v ); int Status = Dau_Dsd6FindSupportOne( p, tCof0, tCof1, pVars, nVars, v, u ); assert( v > u ); +//printf( "Checking %s and %s.\n", p->pVarDefs[pVars[v]], p->pVarDefs[pVars[u]] ); + // Kit_DsdPrintFromTruth( (unsigned *)pTruth, 6 );printf( "\n" ); if ( Status == 3 ) { @@ -1101,9 +1248,10 @@ int Dau_Dsd6DecomposeDoubleVars( Dau_Dsd_t * p, word * pTruth, int * pVars, int // 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 ); + extern int Dau_DsdDecomposeInt( Dau_Dsd_t * p, word * pTruth, int nVarsInit ); Dau_Dsd_t P1, * p1 = &P1; word tCof0, tCof1; + p1->fSplitPrime = 0; // move this variable to the top ABC_SWAP( int, pVars[v], pVars[nVars-1] ); Abc_TtSwapVars( pTruth, 6, v, nVars-1 ); @@ -1204,22 +1352,22 @@ int Dau_Dsd6DecomposeTripleVars( Dau_Dsd_t * p, word * pTruth, int * pVars, int assert( 0 ); return -1; } -void Dau_Dsd6DecomposeInternal( Dau_Dsd_t * p, word * pTruth, int * pVars, int nVars ) +int 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; + return 0; // decompose double variables on the input side nVars = Dau_Dsd6DecomposeDoubleVars( p, pTruth, pVars, nVars ); if ( nVars == 0 ) - return; + return 0; // decompose MUX on the output/input side nVars = Dau_Dsd6DecomposeTripleVars( p, pTruth, pVars, nVars ); if ( nVars == 0 ) - return; + return 0; // write non-decomposable function - Dau_DsdWritePrime( p, pTruth, pVars, nVars ); + return Dau_DsdWritePrime( p, pTruth, pVars, nVars ); } /**Function************************************************************* @@ -1245,22 +1393,22 @@ int Dau_DsdDecomposeTripleVars( Dau_Dsd_t * p, word * pTruth, int * pVars, int { return 0; } -void Dau_DsdDecomposeInternal( Dau_Dsd_t * p, word * pTruth, int * pVars, int nVars ) +int 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; + return 0; // decompose double variables on the input side nVars = Dau_DsdDecomposeDoubleVars( p, pTruth, pVars, nVars ); if ( nVars == 0 ) - return; + return 0; // decompose MUX on the output/input side nVars = Dau_DsdDecomposeTripleVars( p, pTruth, pVars, nVars ); if ( nVars == 0 ) - return; + return 0; // write non-decomposable function - Dau_DsdWritePrime( p, pTruth, pVars, nVars ); + return Dau_DsdWritePrime( p, pTruth, pVars, nVars ); } /**Function************************************************************* @@ -1288,50 +1436,59 @@ int Dau_DsdMinBase( word * pTruth, int nVars, int * pVarsNew ) } return nVars; } -void Dau_DsdDecomposeInt( Dau_Dsd_t * p, word * pTruth, int nVarsInit ) +int Dau_DsdDecomposeInt( Dau_Dsd_t * p, word * pTruth, int nVarsInit ) { - int nVars, pVars[16]; + int Status = 0, nVars, pVars[16]; 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 ); + Status = Dau_Dsd6DecomposeInternal( p, pTruth, pVars, nVars ); else - Dau_DsdDecomposeInternal( p, pTruth, pVars, nVars ); + Status = Dau_DsdDecomposeInternal( p, pTruth, pVars, nVars ); Dau_DsdFinalize( p ); + return Status; } -char * Dau_DsdDecompose( word * pTruth, int nVarsInit, int * pnSizeNonDec ) +int Dau_DsdDecompose( word * pTruth, int nVarsInit, int fSplitPrime, char * pRes ) { - static Dau_Dsd_t P; - Dau_Dsd_t * p = &P; + Dau_Dsd_t P, * p = &P; + p->fSplitPrime = fSplitPrime; p->nSizeNonDec = 0; if ( (pTruth[0] & 1) == 0 && Abc_TtIsConst0(pTruth, Abc_TtWordNum(nVarsInit)) ) - p->pOutput[0] = '0', p->pOutput[1] = 0; + pRes[0] = '0', pRes[1] = 0; else if ( (pTruth[0] & 1) && Abc_TtIsConst1(pTruth, Abc_TtWordNum(nVarsInit)) ) - p->pOutput[0] = '1', p->pOutput[1] = 0; + pRes[0] = '1', pRes[1] = 0; else { - Dau_DsdDecomposeInt( p, pTruth, nVarsInit ); - Dau_DsdCleanBraces( p->pOutput ); + int Status = Dau_DsdDecomposeInt( p, pTruth, nVarsInit ); + Dau_DsdRemoveBraces( p->pOutput, Dau_DsdComputeMatches(p->pOutput) ); + if ( pRes ) + strcpy( pRes, p->pOutput ); + assert( fSplitPrime || Status != 1 ); + if ( fSplitPrime && Status == 2 ) + return -1; } - if ( pnSizeNonDec ) - *pnSizeNonDec = p->nSizeNonDec; - return p->pOutput; + return p->nSizeNonDec; } -void Dau_DsdTest() + +void Dau_DsdTest44() { + char pRes[DAU_MAX_STR]; // char * pStr = "(!(!a<bcd>)!(!fe))"; // char * pStr = "([acb]<!edf>)"; // char * pStr = "!(f!(b!c!(d[ea])))"; // char * pStr = "[!(a[be])!(c!df)]"; -// char * pStr = "<(a<bcd>)ef>"; - char * pStr = "[d8001{a(!bc)ef}]"; - char * pStr2; +// char * pStr = "<(e<bca>)fd>"; +// char * pStr = "[d8001{abef}c]"; + char * pStr = "[dc<a(cbd)(!c!b!d)>{abef}]"; +// char * pStr3; word t = Dau_Dsd6ToTruth( pStr ); - return; - pStr2 = Dau_DsdDecompose( &t, 6, NULL ); +// return; + int nNonDec = Dau_DsdDecompose( &t, 6, 1, pRes ); +// Dau_DsdNormalize( pStr2 ); +// Dau_DsdExtract( pStr, 2, 0 ); t = 0; } @@ -1341,13 +1498,13 @@ void Dau_DsdTest33() FILE * pFile = fopen( pFileName, "rb" ); word t, t1, t2; char pBuffer[100]; - char * pStr2; + char pRes[DAU_MAX_STR]; int nSizeNonDec; int i, Counter = 0; clock_t clk = clock(); while ( fgets( pBuffer, 100, pFile ) != NULL ) { - pStr2 = pBuffer + strlen(pBuffer)-1; + char * pStr2 = pBuffer + strlen(pBuffer)-1; if ( *pStr2 == '\n' ) *pStr2-- = 0; if ( *pStr2 == '\r' ) @@ -1359,12 +1516,12 @@ void Dau_DsdTest33() for ( i = 0; i < 1000; i++ ) { Dau_DsdPermute( pBuffer ); - t = t1 = Dau_Dsd6ToTruth( pBuffer[0] == '*' ? pBuffer + 1 : pBuffer ); - pStr2 = Dau_DsdDecompose( &t, 6, &nSizeNonDec ); + nSizeNonDec = Dau_DsdDecompose( &t, 6, 0, pRes ); + Dau_DsdNormalize( pRes ); // pStr2 = Dau_DsdPerform( t ); nSizeNonDec = 0; assert( nSizeNonDec == 0 ); - t2 = Dau_Dsd6ToTruth( pStr2 ); + t2 = Dau_Dsd6ToTruth( pRes ); if ( t1 != t2 ) { // Kit_DsdPrintFromTruth( (unsigned *)&t, 6 ); diff --git a/src/opt/dau/dauMerge.c b/src/opt/dau/dauMerge.c new file mode 100644 index 00000000..cbb8e145 --- /dev/null +++ b/src/opt/dau/dauMerge.c @@ -0,0 +1,722 @@ +/**CFile**************************************************************** + + FileName [dauMerge.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [DAG-aware unmapping.] + + Synopsis [Enumeration of decompositions.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: dauMerge.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "dau.h" +#include "dauInt.h" + +ABC_NAMESPACE_IMPL_START + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Substitution storage.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +typedef struct Dau_Sto_t_ Dau_Sto_t; +struct Dau_Sto_t_ +{ + int iVarUsed; // counter of used variables + char pOutput[DAU_MAX_STR]; // storage for reduced function + char * pPosOutput; // place in the output + char pStore[DAU_MAX_STR]; // storage for definitions + char * pPosStore; // place in the store + char * pVarDefs[DAU_MAX_VAR];// variable definition (inside pStore) +}; + +static inline void Dau_DsdMergeStoreClean( Dau_Sto_t * pS, int nShared ) +{ + pS->iVarUsed = nShared; + pS->pPosStore = pS->pStore; + memset( pS->pVarDefs, 0, sizeof(char *) * DAU_MAX_VAR ); +} +static inline void Dau_DsdMergeStoreCleanOutput( Dau_Sto_t * pS ) +{ + pS->pPosOutput = pS->pOutput; +} +static inline void Dau_DsdMergeStoreAddToOutput( Dau_Sto_t * pS, char * pBeg, char * pEnd ) +{ + while ( pBeg < pEnd ) + *pS->pPosOutput++ = *pBeg++; +} +static inline void Dau_DsdMergeStoreAddToOutputChar( Dau_Sto_t * pS, char c ) +{ + *pS->pPosOutput++ = c; +} + +static inline void Dau_DsdMergeStoreStartDef( Dau_Sto_t * pS, char c ) +{ + pS->pVarDefs[pS->iVarUsed] = pS->pPosStore; + if (c) *pS->pPosStore++ = c; +} +static inline void Dau_DsdMergeStoreAddToDef( Dau_Sto_t * pS, char * pBeg, char * pEnd ) +{ + while ( pBeg < pEnd ) + *pS->pPosStore++ = *pBeg++; +} +static inline void Dau_DsdMergeStoreAddToDefChar( Dau_Sto_t * pS, char c ) +{ + *pS->pPosStore++ = c; +} +static inline char Dau_DsdMergeStoreStopDef( Dau_Sto_t * pS, char c ) +{ + if (c) *pS->pPosStore++ = c; + *pS->pPosStore++ = 0; + return 'a' + pS->iVarUsed++; +} + +static inline char Dau_DsdMergeStoreCreateDef( Dau_Sto_t * pS, char * pBeg, char * pEnd ) +{ + Dau_DsdMergeStoreStartDef( pS, 0 ); + Dau_DsdMergeStoreAddToDef( pS, pBeg, pEnd ); + return Dau_DsdMergeStoreStopDef( pS, 0 ); +} +static inline void Dau_DsdMergeStorePrintDefs( Dau_Sto_t * pS ) +{ + int i; + for ( i = 0; i < DAU_MAX_VAR; i++ ) + if ( pS->pVarDefs[i] != NULL ) + printf( "%c = %s\n", 'a' + i, pS->pVarDefs[i] ); +} + +/**Function************************************************************* + + Synopsis [Creates local copy.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Dau_DsdMergeCopy( char * pDsd, int fCompl, char * pRes ) +{ + if ( fCompl && pDsd[0] == '!' ) + fCompl = 0, pDsd++; + if ( pDsd[1] == 0 ) // constant + pRes[0] = (fCompl ? (char)((int)pDsd[0] ^ 1) : pDsd[0]), pRes[1] = 0; + else + sprintf( pRes, "%s%s", fCompl ? "!" : "", pDsd ); +} + +/**Function************************************************************* + + Synopsis [Replaces variables according to the mapping.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Dau_DsdMergeReplace( char * pDsd, int * pMatches, int * pMap ) +{ + int i; + for ( i = 0; pDsd[i]; i++ ) + { + // skip non-DSD block + if ( pDsd[i] == '<' && pDsd[pMatches[i]+1] == '{' ) + i = pMatches[i] + 1; + if ( (pDsd[i] >= 'A' && pDsd[i] <= 'F') || (pDsd[i] >= '0' && pDsd[i] <= '9') ) + while ( (pDsd[i] >= 'A' && pDsd[i] <= 'F') || (pDsd[i] >= '0' && pDsd[i] <= '9') ) + i++; + // detect variables + if ( pDsd[i] >= 'a' && pDsd[i] <= 'z' ) + pDsd[i] = 'a' + pMap[ pDsd[i] - 'a' ]; + } +} +static inline void Dau_DsdMergeMatches( char * pDsd, int * pMatches ) +{ + int pNested[DAU_MAX_VAR]; + int i, nNested = 0; + for ( i = 0; pDsd[i]; i++ ) + { + pMatches[i] = 0; + if ( pDsd[i] == '(' || pDsd[i] == '[' || pDsd[i] == '<' || pDsd[i] == '{' ) + pNested[nNested++] = i; + else if ( pDsd[i] == ')' || pDsd[i] == ']' || pDsd[i] == '>' || pDsd[i] == '}' ) + pMatches[pNested[--nNested]] = i; + assert( nNested < DAU_MAX_VAR ); + } + assert( nNested == 0 ); +} +static inline void Dau_DsdMergeVarPres( char * pDsd, int * pMatches, int * pPres, int Mask ) +{ + int i; + for ( i = 0; pDsd[i]; i++ ) + { + // skip non-DSD block + if ( pDsd[i] == '<' && pDsd[pMatches[i]+1] == '{' ) + i = pMatches[i] + 1; + if ( (pDsd[i] >= 'A' && pDsd[i] <= 'F') || (pDsd[i] >= '0' && pDsd[i] <= '9') ) + while ( (pDsd[i] >= 'A' && pDsd[i] <= 'F') || (pDsd[i] >= '0' && pDsd[i] <= '9') ) + i++; + // skip non-variables + if ( !(pDsd[i] >= 'a' && pDsd[i] <= 'z') ) + continue; + // record the mask + assert( pDsd[i]-'a' < DAU_MAX_VAR ); + pPres[pDsd[i]-'a'] |= Mask; + } +} +static inline int Dau_DsdMergeCountShared( int * pPres, int Mask ) +{ + int i, Counter = 0; + for ( i = 0; i < DAU_MAX_VAR; i++ ) + Counter += (pPres[i] == Mask); + return Counter; +} +static inline int Dau_DsdMergeFindShared( char * pDsd0, char * pDsd1, int * pMatches0, int * pMatches1, int * pVarPres ) +{ + memset( pVarPres, 0, sizeof(int)*DAU_MAX_VAR ); + Dau_DsdMergeVarPres( pDsd0, pMatches0, pVarPres, 1 ); + Dau_DsdMergeVarPres( pDsd1, pMatches1, pVarPres, 2 ); + return Dau_DsdMergeCountShared( pVarPres, 3 ); +} +static inline int Dau_DsdMergeCreateMaps( int * pVarPres, int nShared, int * pOld2New, int * pNew2Old ) +{ + int i, Counter = 0, Counter2 = nShared; + for ( i = 0; i < DAU_MAX_VAR; i++ ) + { + if ( pVarPres[i] == 0 ) + continue; + if ( pVarPres[i] == 3 ) + { + pOld2New[i] = Counter; + pNew2Old[Counter] = i; + Counter++; + continue; + } + assert( pVarPres[i] == 1 || pVarPres[i] == 2 ); + pOld2New[i] = Counter2; + pNew2Old[Counter2] = i; + Counter2++; + } + return Counter2; +} +static inline void Dau_DsdMergeInlineDefinitions( char * pDsd, int * pMatches, char ** pVarDefs, char * pRes, int nShared ) +{ + int i; + char * pDef; + char * pBegin = pRes; + for ( i = 0; pDsd[i]; i++ ) + { + // skip non-DSD block + if ( pDsd[i] == '<' && pDsd[pMatches[i]+1] == '{' ) + { + assert( pDsd[pMatches[i]] == '>' ); + for ( ; i <= pMatches[i]; i++ ) + *pRes++ = pDsd[i]; + } + if ( (pDsd[i] >= 'A' && pDsd[i] <= 'F') || (pDsd[i] >= '0' && pDsd[i] <= '9') ) + while ( (pDsd[i] >= 'A' && pDsd[i] <= 'F') || (pDsd[i] >= '0' && pDsd[i] <= '9') ) + *pRes++ = pDsd[i++]; + // detect variables + if ( !(pDsd[i] >= 'a' && pDsd[i] <= 'z') || (pDsd[i] - 'a' < nShared) ) + { + *pRes++ = pDsd[i]; + continue; + } + // inline definition + assert( pDsd[i]-'a' < DAU_MAX_STR ); + for ( pDef = pVarDefs[pDsd[i]-'a']; *pDef; pDef++ ) + *pRes++ = *pDef; + } + *pRes++ = 0; + assert( pRes - pBegin < DAU_MAX_STR ); +} + + +/**Function************************************************************* + + Synopsis [Computes independence status for each opening paranthesis.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Dau_DsdMergePrintWithStatus( char * p, int * pStatus ) +{ + int i; + printf( "%s\n", p ); + for ( i = 0; p[i]; i++ ) + if ( !(p[i] == '(' || p[i] == '[' || p[i] == '<' || p[i] == '{' || (p[i] >= 'a' && p[i] <= 'z')) ) + printf( " " ); + else if ( pStatus[i] >= 0 ) + printf( "%d", pStatus[i] ); + else + printf( "-" ); + printf( "\n" ); +} +int Dau_DsdMergeStatus_rec( char * pStr, char ** p, int * pMatches, int nShared, int * pStatus ) +{ + // none pure + // 1 one pure + // 2 two or more pure + // 3 all pure + if ( **p == '!' ) + { + pStatus[*p - pStr] = -1; + (*p)++; + } + while ( (**p >= 'A' && **p <= 'F') || (**p >= '0' && **p <= '9') ) + { + pStatus[*p - pStr] = -1; + (*p)++; + } + if ( **p == '<' ) + { + char * q = pStr + pMatches[ *p - pStr ]; + if ( *(q+1) == '{' ) + { + char * pTemp = *p; + *p = q+1; + for ( ; pTemp < q+1; pTemp++ ) + pStatus[pTemp - pStr] = -1; + } + } + if ( **p >= 'a' && **p <= 'f' ) // var + return pStatus[*p - pStr] = (**p - 'a' < nShared) ? 0 : 3; + if ( **p == '(' || **p == '[' || **p == '<' || **p == '{' ) // and/or/xor + { + int Status, nPure = 0, nTotal = 0; + char * pOld = *p; + char * q = pStr + pMatches[ *p - pStr ]; + assert( *q == **p + 1 + (**p != '(') ); + for ( (*p)++; *p < q; (*p)++ ) + { + Status = Dau_DsdMergeStatus_rec( pStr, p, pMatches, nShared, pStatus ); + nPure += (Status == 3); + nTotal++; + } + assert( *p == q ); + assert( nTotal > 1 ); + if ( nPure == 0 ) + Status = 0; + else if ( nPure == 1 ) + Status = 1; + else if ( nPure < nTotal ) + Status = 2; + else if ( nPure == nTotal ) + Status = 3; + else assert( 0 ); + return (pStatus[pOld - pStr] = Status); + } + assert( 0 ); + return 0; +} +static inline int Dau_DsdMergeStatus( char * pDsd, int * pMatches, int nShared, int * pStatus ) +{ + return Dau_DsdMergeStatus_rec( pDsd, &pDsd, pMatches, nShared, pStatus ); +} + +/**Function************************************************************* + + Synopsis [Extracts the formula.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Dau_DsdMergeGetStatus( char * pBeg, char * pStr, int * pMatches, int * pStatus ) +{ + if ( *pBeg == '!' ) + pBeg++; + while ( (*pBeg >= 'A' && *pBeg <= 'F') || (*pBeg >= '0' && *pBeg <= '9') ) + pBeg++; + if ( *pBeg == '<' ) + { + char * q = pStr + pMatches[pBeg - pStr]; + if ( *(q+1) == '{' ) + pBeg = q+1; + } + return pStatus[pBeg - pStr]; +} +void Dau_DsdMergeSubstitute_rec( Dau_Sto_t * pS, char * pStr, char ** p, int * pMatches, int * pStatus, int fWrite ) +{ + assert( **p != '!' ); +/* + if ( **p == '!' ) + { + if ( fWrite ) + Dau_DsdMergeStoreAddToOutputChar( pS, **p ); + (*p)++; + } +*/ + while ( (**p >= 'A' && **p <= 'F') || (**p >= '0' && **p <= '9') ) + { + if ( fWrite ) + Dau_DsdMergeStoreAddToOutputChar( pS, **p ); + (*p)++; + } + if ( **p == '<' ) + { + char * q = pStr + pMatches[ *p - pStr ]; + if ( *(q+1) == '{' ) + { + char * pTemp = *p; + *p = q+1; + if ( fWrite ) + for ( ; pTemp < q+1; pTemp++ ) + Dau_DsdMergeStoreAddToOutputChar( pS, *pTemp ); + } + } + if ( **p >= 'a' && **p <= 'f' ) // var + { + if ( fWrite ) + Dau_DsdMergeStoreAddToOutputChar( pS, **p ); + return; + } + if ( **p == '(' || **p == '[' || **p == '<' || **p == '{' ) // and/or/xor + { + int StatusFan, Status = pStatus[*p - pStr]; + char New, * pBeg, * q = pStr + pMatches[ *p - pStr ]; + assert( *q == **p + 1 + (**p != '(') ); + if ( !fWrite ) + { + assert( Status == 3 ); + *p = q; + return; + } + assert( Status != 3 ); + if ( Status == 0 ) // none pure + { + Dau_DsdMergeStoreAddToOutputChar( pS, **p ); + for ( (*p)++; *p < q; (*p)++ ) + { + if ( **p == '!' ) + { + Dau_DsdMergeStoreAddToOutputChar( pS, '!' ); + (*p)++; + } + Dau_DsdMergeSubstitute_rec( pS, pStr, p, pMatches, pStatus, 1 ); + } + Dau_DsdMergeStoreAddToOutputChar( pS, **p ); + assert( *p == q ); + return; + } + if ( Status == 1 || **p == '<' || **p == '{' ) // 1 pure + { + Dau_DsdMergeStoreAddToOutputChar( pS, **p ); + for ( (*p)++; *p < q; (*p)++ ) + { + if ( **p == '!' ) + { + Dau_DsdMergeStoreAddToOutputChar( pS, '!' ); + (*p)++; + } + pBeg = *p; + StatusFan = Dau_DsdMergeGetStatus( pBeg, pStr, pMatches, pStatus ); + Dau_DsdMergeSubstitute_rec( pS, pStr, p, pMatches, pStatus, StatusFan != 3 ); + if ( StatusFan == 3 ) + { + char New = Dau_DsdMergeStoreCreateDef( pS, pBeg, *p+1 ); + Dau_DsdMergeStoreAddToOutputChar( pS, New ); + } + } + Dau_DsdMergeStoreAddToOutputChar( pS, **p ); + assert( *p == q ); + return; + } + if ( Status == 2 ) + { + // add more than one defs + Dau_DsdMergeStoreAddToOutputChar( pS, **p ); + Dau_DsdMergeStoreStartDef( pS, **p ); + for ( (*p)++; *p < q; (*p)++ ) + { + pBeg = *p; + StatusFan = Dau_DsdMergeGetStatus( pBeg, pStr, pMatches, pStatus ); + if ( **p == '!' ) + { + if ( StatusFan != 3 ) + Dau_DsdMergeStoreAddToOutputChar( pS, '!' ); + else + Dau_DsdMergeStoreAddToDefChar( pS, '!' ); + (*p)++; + pBeg++; + } + Dau_DsdMergeSubstitute_rec( pS, pStr, p, pMatches, pStatus, StatusFan != 3 ); + if ( StatusFan == 3 ) + Dau_DsdMergeStoreAddToDef( pS, pBeg, *p+1 ); + } + New = Dau_DsdMergeStoreStopDef( pS, *q ); + Dau_DsdMergeStoreAddToOutputChar( pS, New ); + Dau_DsdMergeStoreAddToOutputChar( pS, **p ); + return; + } + assert( 0 ); + return; + } + assert( 0 ); +} +static inline void Dau_DsdMergeSubstitute( Dau_Sto_t * pS, char * pDsd, int * pMatches, int * pStatus ) +{ + if ( pDsd[0] == '!' ) + { + Dau_DsdMergeStoreAddToOutputChar( pS, '!' ); + pDsd++; + } + Dau_DsdMergeSubstitute_rec( pS, pDsd, &pDsd, pMatches, pStatus, 1 ); + Dau_DsdMergeStoreAddToOutputChar( pS, 0 ); +} + +/**Function************************************************************* + + Synopsis [Removes braces.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Dau_DsdRemoveBraces_rec( char * pStr, char ** p, int * pMatches ) +{ + if ( **p == '!' ) + (*p)++; + while ( (**p >= 'A' && **p <= 'F') || (**p >= '0' && **p <= '9') ) + (*p)++; + if ( **p == '<' ) + { + char * q = pStr + pMatches[*p - pStr]; + if ( *(q+1) == '{' ) + *p = q+1; + } + if ( **p >= 'a' && **p <= 'f' ) // var + return; + if ( **p == '(' || **p == '[' || **p == '<' || **p == '{' ) + { + char * q = pStr + pMatches[ *p - pStr ]; + assert( *q == **p + 1 + (**p != '(') ); + for ( (*p)++; *p < q; (*p)++ ) + { + int fCompl = (**p == '!'); + char * pBeg = fCompl ? *p + 1 : *p; + Dau_DsdRemoveBraces_rec( pStr, p, pMatches ); + if ( (!fCompl && *pBeg == '(' && *q == ')') || (*pBeg == '[' && *q == ']') ) + { + assert( **p == ')' || **p == ']' ); + *pBeg = **p = ' '; + } + } + assert( *p == q ); + return; + } + assert( 0 ); +} +void Dau_DsdRemoveBraces( char * pDsd, int * pMatches ) +{ + char * q, * p = pDsd; + if ( pDsd[1] == 0 ) + return; + Dau_DsdRemoveBraces_rec( pDsd, &pDsd, pMatches ); + for ( q = p; *p; p++ ) + if ( *p != ' ' ) + *q++ = *p; + *q = 0; +} + + +/**Function************************************************************* + + Synopsis [Performs merging of two DSD formulas.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +char * Dau_DsdMerge( char * pDsd0i, int * pPerm0, char * pDsd1i, int * pPerm1, int fCompl0, int fCompl1 ) +{ + static char pRes[DAU_MAX_STR]; + char pDsd0[DAU_MAX_STR]; + char pDsd1[DAU_MAX_STR]; + int pMatches0[DAU_MAX_STR]; + int pMatches1[DAU_MAX_STR]; + int pVarPres[DAU_MAX_VAR]; + int pOld2New[DAU_MAX_VAR]; + int pNew2Old[DAU_MAX_VAR]; + int pStatus0[DAU_MAX_STR]; + int pStatus1[DAU_MAX_STR]; + int pMatches[DAU_MAX_STR]; + int nVarsShared, nVarsTotal; + Dau_Sto_t S, * pS = &S; + word Truth, t, t0, t1; + int Status; + // create local copies + Dau_DsdMergeCopy( pDsd0i, fCompl0, pDsd0 ); + Dau_DsdMergeCopy( pDsd1i, fCompl1, pDsd1 ); + // handle constants + if ( pDsd0[1] == 0 || pDsd1[1] == 0 ) + { + if ( pDsd0[0] == '0' ) + strcpy( pRes, pDsd0 ); + else if ( pDsd0[0] == '1' ) + strcpy( pRes, pDsd1 ); + else if ( pDsd1[0] == '0' ) + strcpy( pRes, pDsd1 ); + else if ( pDsd1[0] == '1' ) + strcpy( pRes, pDsd0 ); + else assert( 0 ); + return pRes; + } + // compute matches + Dau_DsdMergeMatches( pDsd0, pMatches0 ); + Dau_DsdMergeMatches( pDsd1, pMatches1 ); + // implement permutation + Dau_DsdMergeReplace( pDsd0, pMatches0, pPerm0 ); + Dau_DsdMergeReplace( pDsd1, pMatches1, pPerm1 ); +printf( "%s\n", pDsd0 ); +printf( "%s\n", pDsd1 ); + t0 = Dau_Dsd6ToTruth( pDsd0 ); + t1 = Dau_Dsd6ToTruth( pDsd1 ); + // find shared varaiables + nVarsShared = Dau_DsdMergeFindShared(pDsd0, pDsd1, pMatches0, pMatches1, pVarPres); + if ( nVarsShared == 0 ) + { + sprintf( pRes, "(%s%s)", pDsd0, pDsd1 ); + return pRes; + } + // create variable mapping + nVarsTotal = Dau_DsdMergeCreateMaps( pVarPres, nVarsShared, pOld2New, pNew2Old ); + // perform variable replacement + Dau_DsdMergeReplace( pDsd0, pMatches0, pOld2New ); + Dau_DsdMergeReplace( pDsd1, pMatches1, pOld2New ); + // find uniqueness status + Dau_DsdMergeStatus( pDsd0, pMatches0, nVarsShared, pStatus0 ); + Dau_DsdMergeStatus( pDsd1, pMatches1, nVarsShared, pStatus1 ); +Dau_DsdMergePrintWithStatus( pDsd0, pStatus0 ); +Dau_DsdMergePrintWithStatus( pDsd1, pStatus1 ); + // prepare storage + Dau_DsdMergeStoreClean( pS, nVarsShared ); + // perform substitutions + Dau_DsdMergeStoreCleanOutput( pS ); + Dau_DsdMergeSubstitute( pS, pDsd0, pMatches0, pStatus0 ); + strcpy( pDsd0, pS->pOutput ); +printf( "%s\n", pDsd0 ); + + // perform substitutions + Dau_DsdMergeStoreCleanOutput( pS ); + Dau_DsdMergeSubstitute( pS, pDsd1, pMatches1, pStatus1 ); + strcpy( pDsd1, pS->pOutput ); +printf( "%s\n", pDsd1 ); +Dau_DsdMergeStorePrintDefs( pS ); + + // create new function + assert( nVarsTotal <= 6 ); + sprintf( pS->pOutput, "(%s%s)", pDsd0, pDsd1 ); + Truth = Dau_Dsd6ToTruth( pS->pOutput ); + Status = Dau_DsdDecompose( &Truth, nVarsTotal, 0, pS->pOutput ); + if ( Status == -1 ) // did not find 1-step DSD + return NULL; + if ( Status > 6 ) // non-DSD part is too large + return NULL; +printf( "%s\n", pS->pOutput ); + // substitute definitions + Dau_DsdMergeMatches( pS->pOutput, pMatches ); + Dau_DsdMergeInlineDefinitions( pS->pOutput, pMatches, pS->pVarDefs, pRes, nVarsShared ); +printf( "%s\n", pRes ); + // perform variable replacement + Dau_DsdMergeMatches( pRes, pMatches ); + Dau_DsdMergeReplace( pRes, pMatches, pNew2Old ); + Dau_DsdRemoveBraces( pRes, pMatches ); +printf( "%s\n", pRes ); + Dau_DsdNormalize( pRes ); +printf( "%s\n", pRes ); + t = Dau_Dsd6ToTruth( pRes ); + assert( t == (t0 & t1) ); + return pRes; +} + + +void Dau_DsdTest() +{ + int Perm0[DAU_MAX_VAR] = { 0, 1, 2, 3, 4, 5 }; +// int pMatches[DAU_MAX_STR]; +// int pStatus[DAU_MAX_STR]; + +// char * pStr = "(!(!a<bcd>)!(!fe))"; +// char * pStr = "([acb]<!edf>)"; +// char * pStr = "!(f!(b!c!(d[ea])))"; + char * pStr = "[!(a[be])!(c!df)]"; +// char * pStr = "<(e<bca>)fd>"; +// char * pStr = "[d8001{abef}c]"; +// char * pStr1 = "(abc)"; +// char * pStr2 = "[adf]"; +// char * pStr1 = "(!abce)"; +// char * pStr2 = "[adf!b]"; +// char * pStr1 = "(!abc)"; +// char * pStr2 = "[ab]"; +// char * pStr1 = "[d81{abe}c]"; +// char * pStr1 = "[d<a(bc)(!b!c)>{abe}c]"; +// char * pStr1 = "[d81{abe}c]"; +// char * pStr1 = "[d(a[be])c]"; +// char * pStr2 = "(df)"; +// char * pStr1 = "(abf)"; +// char * pStr2 = "(a[(bc)(fde)])"; + char * pStr1 = "8001{abc[ef]}"; + char * pStr2 = "(abe)"; + char * pRes; + word t = Dau_Dsd6ToTruth( pStr ); + return; +// pStr2 = Dau_DsdDecompose( &t, 6, 0, NULL ); +// Dau_DsdNormalize( pStr2 ); + +// Dau_DsdMergeMatches( pStr, pMatches ); +// Dau_DsdMergeStatus( pStr, pMatches, 2, pStatus ); +// Dau_DsdMergePrintWithStatus( pStr, pStatus ); + + pRes = Dau_DsdMerge( pStr1, Perm0, pStr2, Perm0, 0, 0 ); + + t = 0; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/opt/dau/module.make b/src/opt/dau/module.make index 854c0667..ad32445c 100644 --- a/src/opt/dau/module.make +++ b/src/opt/dau/module.make @@ -2,4 +2,5 @@ SRC += src/opt/dau/dau.c \ src/opt/dau/dauCanon.c \ src/opt/dau/dauCore.c \ src/opt/dau/dauDsd.c \ - src/opt/dau/dauEnum.c + src/opt/dau/dauEnum.c \ + src/opt/dau/dauMerge.c |