Improved DSD.

6 files changed, 1036 insertions, 145 deletions

diff --git a/abclib.dsp b/abclib.dsp
index 5cff7a83..c971cb63 100644
--- a/abclib.dsp
+++ b/abclib.dsp
@@ -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