summaryrefslogtreecommitdiffstats
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/base/abci/abcDec.c4
-rw-r--r--src/opt/dau/dau.h11
-rw-r--r--src/opt/dau/dauDsd.c437
-rw-r--r--src/opt/dau/dauMerge.c722
-rw-r--r--src/opt/dau/module.make3
5 files changed, 1032 insertions, 145 deletions
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
generated by cgit v1.2.3 (git 2.25.1) at 2025-02-15 21:56:54 +0000