diff options
Diffstat (limited to 'src/opt/dau/dauMerge.c')
| -rw-r--r-- | src/opt/dau/dauMerge.c | 722 |
1 files changed, 722 insertions, 0 deletions
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 + |