Improved DSD.

7 files changed, 256 insertions, 58 deletions

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 3941fe5d..4395607d 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -14541,7 +14541,7 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv )
 
     fLutMux = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "KCFAGDEWSqaflepmrsdbugyojikcvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "KCFAGDEWSqaflepmrsdbugyojikcnvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -14706,6 +14706,9 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'c':
             pPars->fEnableRealPos ^= 1;
             break;
+        case 'n':
+            pPars->fUseDsd ^= 1;
+            break;
         case 'v':
             pPars->fVerbose ^= 1;
             break;
@@ -14958,7 +14961,7 @@ usage:
         sprintf(LutSize, "library" );
     else
         sprintf(LutSize, "%d", pPars->nLutSize );
-    Abc_Print( -2, "usage: if [-KCFAG num] [-DEW float] [-S str] [-qarlepmsdbugyojikcvh]\n" );
+    Abc_Print( -2, "usage: if [-KCFAG num] [-DEW float] [-S str] [-qarlepmsdbugyojikcnvh]\n" );
     Abc_Print( -2, "\t           performs FPGA technology mapping of the network\n" );
     Abc_Print( -2, "\t-K num   : the number of LUT inputs (2 < num < %d) [default = %s]\n", IF_MAX_LUTSIZE+1, LutSize );
     Abc_Print( -2, "\t-C num   : the max number of priority cuts (0 < num < 2^12) [default = %d]\n", pPars->nCutsMax );
@@ -14988,6 +14991,7 @@ usage:
     Abc_Print( -2, "\t-i       : toggles enabling additional check [default = %s]\n", pPars->fEnableCheck08? "yes": "no" );
     Abc_Print( -2, "\t-k       : toggles enabling additional check [default = %s]\n", pPars->fEnableCheck10? "yes": "no" );
     Abc_Print( -2, "\t-c       : toggles enabling additional feature [default = %s]\n", pPars->fEnableRealPos? "yes": "no" );
+    Abc_Print( -2, "\t-n       : toggles computing DSDs of the cut functions [default = %s]\n", pPars->fUseDsd? "yes": "no" );
     Abc_Print( -2, "\t-v       : toggles verbose output [default = %s]\n", pPars->fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h       : prints the command usage\n");
     return 1;
diff --git a/src/map/if/if.h b/src/map/if/if.h
index 04ff59e4..6a2fdd5d 100644
--- a/src/map/if/if.h
+++ b/src/map/if/if.h
@@ -34,7 +34,7 @@
 #include "misc/vec/vec.h"
 #include "misc/mem/mem.h"
 #include "misc/tim/tim.h"
-
+#include "misc/util/utilNam.h"
 
 
 ABC_NAMESPACE_HEADER_START
@@ -116,6 +116,7 @@ struct If_Par_t_
     int                fEnableCheck08;// enable additional checking
     int                fEnableCheck10;// enable additional checking
     int                fEnableRealPos;// enable additional feature
+    int                fUseDsd;       // compute DSD of the cut functions
     int                fVerbose;      // the verbosity flag
     char *             pLutStruct;    // LUT structure
     float              WireDelay;     // wire delay
@@ -215,6 +216,9 @@ struct If_Man_t_
     int                nCutsCount[32];
     int                nCutsCountAll;
     int                nCutsUselessAll;
+    Abc_Nam_t *        pNamDsd;
+    int                iNamVar;
+
     // timing manager
     Tim_Man_t *        pManTim;
     Vec_Int_t *        vCoAttrs;      // CO attributes   0=optimize; 1=keep; 2=relax
@@ -235,6 +239,7 @@ struct If_Cut_t_
     float              Edge;          // the edge flow
     float              Power;         // the power flow
     float              Delay;         // delay of the cut
+    int                iDsd;          // DSD ID of the cut
     unsigned           uSign;         // cut signature
     unsigned           Cost    : 13;  // the user's cost of the cut (related to IF_COST_MAX)
     unsigned           fCompl  :  1;  // the complemented attribute 
diff --git a/src/map/if/ifMan.c b/src/map/if/ifMan.c
index 0ebdec1b..db63a831 100644
--- a/src/map/if/ifMan.c
+++ b/src/map/if/ifMan.c
@@ -32,6 +32,8 @@ static If_Obj_t * If_ManSetupObj( If_Man_t * p );
 static void       If_ManCutSetRecycle( If_Man_t * p, If_Set_t * pSet ) { pSet->pNext = p->pFreeList; p->pFreeList = pSet;                            }
 static If_Set_t * If_ManCutSetFetch( If_Man_t * p )                    { If_Set_t * pTemp = p->pFreeList; p->pFreeList = p->pFreeList->pNext; return pTemp; }
 
+extern clock_t s_TimeComp[3];
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
@@ -79,6 +81,11 @@ If_Man_t * If_ManStart( If_Par_t * pPars )
     p->puTemp[2] = p->puTemp[1] + p->nTruthWords;
     p->puTemp[3] = p->puTemp[2] + p->nTruthWords;
     p->pCutTemp  = (If_Cut_t *)ABC_ALLOC( char, p->nCutBytes );
+    if ( pPars->fUseDsd )
+    {
+    p->pNamDsd   = Abc_NamStart( 1000, 20 );
+    p->iNamVar   = Abc_NamStrFindOrAdd( p->pNamDsd, "a", NULL );
+    }
 
     // create the constant node
     p->pConst1   = If_ManSetupObj( p );
@@ -143,6 +150,17 @@ void If_ManStop( If_Man_t * p )
                 Abc_Print( 1, "Useless cuts %2d  = %9d  (out of %9d)  (%6.2f %%)\n", i, p->nCutsUseless[i], p->nCutsCount[i], 100.0*p->nCutsUseless[i]/(p->nCutsCount[i]+1) );
         Abc_Print( 1, "Useless cuts all = %9d  (out of %9d)  (%6.2f %%)\n", p->nCutsUselessAll, p->nCutsCountAll, 100.0*p->nCutsUselessAll/(p->nCutsCountAll+1) );
     }
+    if ( p->pNamDsd )
+    {
+        if ( p->pPars->fVerbose )
+            Abc_Print( 1, "Number of unique entries in the DSD table = %d.  Memory = %.1f MB.\n", 
+                Abc_NamObjNumMax(p->pNamDsd), 1.0*Abc_NamMemAlloc(p->pNamDsd)/(1<<20) );
+        Abc_PrintTime( 1, "Time0", s_TimeComp[0] );
+        Abc_PrintTime( 1, "Time1", s_TimeComp[1] );
+        Abc_PrintTime( 1, "Time2", s_TimeComp[2] );
+//        Abc_NamPrint( p->pNamDsd );
+        Abc_NamStop( p->pNamDsd );
+    }
 //    Abc_PrintTime( 1, "Truth", p->timeTruth );
 //    Abc_Print( 1, "Small support = %d.\n", p->nSmallSupp );
     Vec_IntFreeP( &p->vCoAttrs );
@@ -408,6 +426,7 @@ void If_ManSetupCutTriv( If_Man_t * p, If_Cut_t * pCut, int ObjId )
     pCut->nLeaves    = 1;
     pCut->pLeaves[0] = p->pPars->fLiftLeaves? (ObjId << 8) : ObjId;
     pCut->uSign      = If_ObjCutSign( pCut->pLeaves[0] );
+    pCut->iDsd       = p->iNamVar;
     // set up elementary truth table of the unit cut
     if ( p->pPars->fTruth )
     {
diff --git a/src/map/if/ifMap.c b/src/map/if/ifMap.c
index d4d0d1dd..cb3c6832 100644
--- a/src/map/if/ifMap.c
+++ b/src/map/if/ifMap.c
@@ -27,6 +27,8 @@ ABC_NAMESPACE_IMPL_START
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
+extern char * Dau_DsdMerge( char * pDsd0i, int * pPerm0, char * pDsd1i, int * pPerm1, int fCompl0, int fCompl1 );
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
@@ -80,6 +82,50 @@ float If_CutDelaySpecial( If_Man_t * p, If_Cut_t * pCut, int fCarry )
 
 /**Function*************************************************************
 
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int * If_CutPerm0( If_Cut_t * pCut, If_Cut_t * pCut0 )
+{
+    static int pPerm[IF_MAX_LUTSIZE];
+    int i, k;
+    for ( i = k = 0; i < (int)pCut->nLeaves; i++ )
+    {
+        if ( k == (int)pCut0->nLeaves )
+            break;
+        if ( pCut->pLeaves[i] < pCut0->pLeaves[k] )
+            continue;
+        assert( pCut->pLeaves[i] == pCut0->pLeaves[k] );
+        pPerm[k++] = i;
+    }
+    return pPerm;
+}
+static inline int * If_CutPerm1( If_Cut_t * pCut, If_Cut_t * pCut1 )
+{
+    static int pPerm[IF_MAX_LUTSIZE];
+    int i, k;
+    for ( i = k = 0; i < (int)pCut->nLeaves; i++ )
+    {
+        if ( k == (int)pCut1->nLeaves )
+            break;
+        if ( pCut->pLeaves[i] < pCut1->pLeaves[k] )
+            continue;
+        assert( pCut->pLeaves[i] == pCut1->pLeaves[k] );
+        pPerm[k++] = i;
+    }
+    return pPerm;
+}
+
+
+
+/**Function*************************************************************
+
   Synopsis    [Finds the best cut for the given node.]
 
   Description [Mapping modes: delay (0), area flow (1), area (2).]
@@ -227,7 +273,16 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPrep
                 p->nCutsCountAll++;
                 p->nCutsCount[pCut->nLeaves]++;
             }
-
+        }
+        if ( p->pPars->fUseDsd )
+        {
+            char * pName = Dau_DsdMerge( 
+                Abc_NamStr(p->pNamDsd, pCut0->iDsd), 
+                If_CutPerm0(pCut, pCut0), 
+                Abc_NamStr(p->pNamDsd, pCut1->iDsd), 
+                If_CutPerm1(pCut, pCut1), 
+                pObj->fCompl0, pObj->fCompl1 );
+            pCut->iDsd = Abc_NamStrFindOrAdd( p->pNamDsd, pName, NULL );
         }
         
         // compute the application-specific cost and depth
diff --git a/src/opt/dau/dau.h b/src/opt/dau/dau.h
index f9d4f2b2..277da3d3 100644
--- a/src/opt/dau/dau.h
+++ b/src/opt/dau/dau.h
@@ -39,8 +39,8 @@
 
 ABC_NAMESPACE_HEADER_START
 
-#define DAU_MAX_VAR    16 // should be 6 or more
-#define DAU_MAX_STR   256
+#define DAU_MAX_VAR     8 // should be 6 or more
+#define DAU_MAX_STR    64
 #define DAU_MAX_WORD  (1<<(DAU_MAX_VAR-6))
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/opt/dau/dauDsd.c b/src/opt/dau/dauDsd.c
index 80782429..fbba16db 100644
--- a/src/opt/dau/dauDsd.c
+++ b/src/opt/dau/dauDsd.c
@@ -184,6 +184,14 @@ void Dau_DsdNormalize_rec( char * pStr, char ** p, int * pMatches )
     static char pBuffer[DAU_MAX_STR];
     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 == '[' ) // and/or/xor
diff --git a/src/opt/dau/dauMerge.c b/src/opt/dau/dauMerge.c
index cbb8e145..8ab39568 100644
--- a/src/opt/dau/dauMerge.c
+++ b/src/opt/dau/dauMerge.c
@@ -43,23 +43,40 @@ ABC_NAMESPACE_IMPL_START
   SeeAlso     []
 
 ***********************************************************************/
+static inline int Dau_DsdIsConst( char * p )  { return (p[0] == '0' || p[0] == '1') && p[1] == 0; }
+static inline int Dau_DsdIsConst0( char * p ) { return  p[0] == '0' && p[1] == 0; }
+static inline int Dau_DsdIsConst1( char * p ) { return  p[0] == '1' && p[1] == 0; }
+
+
+/**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)
+    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_VAR][DAU_MAX_STR];  // storage for definitions
+    char *   pPosStore[DAU_MAX_VAR];            // place in the store
 };
 
 static inline void Dau_DsdMergeStoreClean( Dau_Sto_t * pS, int nShared )
 {
+    int i;
     pS->iVarUsed  = nShared;
-    pS->pPosStore = pS->pStore;
-    memset( pS->pVarDefs, 0, sizeof(char *) * DAU_MAX_VAR );
+    for ( i = 0; i < DAU_MAX_VAR; i++ )
+        pS->pStore[i][0] = 0;
 }
+
 static inline void Dau_DsdMergeStoreCleanOutput( Dau_Sto_t * pS )
 {
     pS->pPosOutput = pS->pOutput;
@@ -74,39 +91,40 @@ 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 )
+static inline int Dau_DsdMergeStoreStartDef( Dau_Sto_t * pS, char c )
 {
-    pS->pVarDefs[pS->iVarUsed] = pS->pPosStore;
-    if (c) *pS->pPosStore++ = c;
+    pS->pPosStore[pS->iVarUsed] = pS->pStore[pS->iVarUsed];
+    if (c) *pS->pPosStore[pS->iVarUsed]++ = c;
+    return pS->iVarUsed++;
 }
-static inline void Dau_DsdMergeStoreAddToDef( Dau_Sto_t * pS, char * pBeg, char * pEnd )
+static inline void Dau_DsdMergeStoreAddToDef( Dau_Sto_t * pS, int New, char * pBeg, char * pEnd )
 {
     while ( pBeg < pEnd )
-        *pS->pPosStore++ = *pBeg++;
+        *pS->pPosStore[New]++ = *pBeg++;
 }
-static inline void Dau_DsdMergeStoreAddToDefChar( Dau_Sto_t * pS, char c )
+static inline void Dau_DsdMergeStoreAddToDefChar( Dau_Sto_t * pS, int New, char c )
 {
-    *pS->pPosStore++ = c;
+    *pS->pPosStore[New]++ = c;
 }
-static inline char Dau_DsdMergeStoreStopDef( Dau_Sto_t * pS, char c )
+static inline void Dau_DsdMergeStoreStopDef( Dau_Sto_t * pS, int New, char c )
 {
-    if (c) *pS->pPosStore++ = c;
-    *pS->pPosStore++ = 0;
-    return 'a' + pS->iVarUsed++;
+    if (c) *pS->pPosStore[New]++ = c;
+    *pS->pPosStore[New]++ = 0;
 }
 
 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 );
+    int New = Dau_DsdMergeStoreStartDef( pS, 0 );
+    Dau_DsdMergeStoreAddToDef( pS, New, pBeg, pEnd );
+    Dau_DsdMergeStoreStopDef( pS, New, 0 );
+    return New;
 }
 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] );
+        if ( pS->pStore[i][0] )
+            printf( "%c = %s\n", 'a' + i, pS->pStore[i] );
 }
 
 /**Function*************************************************************
@@ -124,7 +142,7 @@ static inline void Dau_DsdMergeCopy( char * pDsd, int fCompl, char * pRes )
 {
     if ( fCompl && pDsd[0] == '!' )
         fCompl = 0, pDsd++;
-    if ( pDsd[1] == 0 ) // constant
+    if ( Dau_DsdIsConst(pDsd) ) // constant
         pRes[0] = (fCompl ? (char)((int)pDsd[0] ^ 1) : pDsd[0]), pRes[1] = 0;
     else
         sprintf( pRes, "%s%s", fCompl ? "!" : "", pDsd );
@@ -226,7 +244,7 @@ static inline int Dau_DsdMergeCreateMaps( int * pVarPres, int nShared, int * pOl
     }
     return Counter2;
 }
-static inline void Dau_DsdMergeInlineDefinitions( char * pDsd, int * pMatches, char ** pVarDefs, char * pRes, int nShared )
+static inline void Dau_DsdMergeInlineDefinitions( char * pDsd, int * pMatches, Dau_Sto_t * pS, char * pRes, int nShared )
 {
     int i;
     char * pDef;
@@ -251,7 +269,7 @@ static inline void Dau_DsdMergeInlineDefinitions( char * pDsd, int * pMatches, c
         }
         // inline definition
         assert( pDsd[i]-'a' < DAU_MAX_STR );
-        for ( pDef = pVarDefs[pDsd[i]-'a']; *pDef; pDef++ )
+        for ( pDef = pS->pStore[pDsd[i]-'a']; *pDef; pDef++ )
             *pRes++ = *pDef;
     }
     *pRes++ = 0;
@@ -372,15 +390,15 @@ static inline int Dau_DsdMergeGetStatus( char * pBeg, char * pStr, int * pMatche
 }
 void Dau_DsdMergeSubstitute_rec( Dau_Sto_t * pS, char * pStr, char ** p, int * pMatches, int * pStatus, int fWrite )
 {
-    assert( **p != '!' );
-/*
+//    assert( **p != '!' );
+
     if ( **p == '!' )
     {
         if ( fWrite )
             Dau_DsdMergeStoreAddToOutputChar( pS, **p );
         (*p)++;
     }
-*/
+
     while ( (**p >= 'A' && **p <= 'F') || (**p >= '0' && **p <= '9') )
     {
         if ( fWrite )
@@ -407,8 +425,8 @@ void Dau_DsdMergeSubstitute_rec( Dau_Sto_t * pS, char * pStr, char ** p, int * p
     }
     if ( **p == '(' || **p == '[' || **p == '<' || **p == '{' ) // and/or/xor
     {
-        int StatusFan, Status = pStatus[*p - pStr];
-        char New, * pBeg, * q = pStr + pMatches[ *p - pStr ];
+        int New, StatusFan, Status = pStatus[*p - pStr];
+        char * pBeg, * q = pStr + pMatches[ *p - pStr ];
         assert( *q == **p + 1 + (**p != '(') );
         if ( !fWrite )
         {
@@ -448,8 +466,8 @@ void Dau_DsdMergeSubstitute_rec( Dau_Sto_t * pS, char * pStr, char ** p, int * p
                 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 );
+                    int New = Dau_DsdMergeStoreCreateDef( pS, pBeg, *p+1 );
+                    Dau_DsdMergeStoreAddToOutputChar( pS, (char)('a' + New) );
                 }
             }
             Dau_DsdMergeStoreAddToOutputChar( pS, **p );
@@ -460,7 +478,7 @@ void Dau_DsdMergeSubstitute_rec( Dau_Sto_t * pS, char * pStr, char ** p, int * p
         {
             // add more than one defs
             Dau_DsdMergeStoreAddToOutputChar( pS, **p );
-            Dau_DsdMergeStoreStartDef( pS, **p );
+            New = Dau_DsdMergeStoreStartDef( pS, **p );
             for ( (*p)++; *p < q; (*p)++ )
             {
                 pBeg = *p;
@@ -470,16 +488,16 @@ void Dau_DsdMergeSubstitute_rec( Dau_Sto_t * pS, char * pStr, char ** p, int * p
                     if ( StatusFan != 3 )
                         Dau_DsdMergeStoreAddToOutputChar( pS, '!' );
                     else
-                        Dau_DsdMergeStoreAddToDefChar( pS, '!' );
+                        Dau_DsdMergeStoreAddToDefChar( pS, New, '!' );
                     (*p)++;
                     pBeg++;
                 }
                 Dau_DsdMergeSubstitute_rec( pS, pStr, p, pMatches, pStatus, StatusFan != 3 );
                 if ( StatusFan == 3 )
-                    Dau_DsdMergeStoreAddToDef( pS, pBeg, *p+1 );
+                    Dau_DsdMergeStoreAddToDef( pS, New, pBeg, *p+1 );
             }
-            New = Dau_DsdMergeStoreStopDef( pS, *q );
-            Dau_DsdMergeStoreAddToOutputChar( pS, New );
+            Dau_DsdMergeStoreStopDef( pS, New, *q );
+            Dau_DsdMergeStoreAddToOutputChar( pS, (char)('a' + New) );
             Dau_DsdMergeStoreAddToOutputChar( pS, **p );
             return;
         }
@@ -490,11 +508,15 @@ void Dau_DsdMergeSubstitute_rec( Dau_Sto_t * pS, char * pStr, char ** p, int * p
 }
 static inline void Dau_DsdMergeSubstitute( Dau_Sto_t * pS, char * pDsd, int * pMatches, int * pStatus )
 {
+/*
+    int fCompl = 0;
     if ( pDsd[0] == '!' )
     {
         Dau_DsdMergeStoreAddToOutputChar( pS, '!' );
         pDsd++;
+        fCompl = 1;
     }
+*/
     Dau_DsdMergeSubstitute_rec( pS, pDsd, &pDsd, pMatches, pStatus, 1 );
     Dau_DsdMergeStoreAddToOutputChar( pS, 0 );
 }
@@ -552,11 +574,20 @@ void Dau_DsdRemoveBraces( char * pDsd, int * pMatches )
     Dau_DsdRemoveBraces_rec( pDsd, &pDsd, pMatches );
     for ( q = p; *p; p++ )
         if ( *p != ' ' )
+        {
+            if ( *p == '!' && *(q-1) == '!' && p != q )
+            {
+                q--;
+                continue;
+            }
             *q++ = *p;
+        }
     *q = 0;
 }
 
 
+clock_t s_TimeComp[3] = {0};
+
 /**Function*************************************************************
 
   Synopsis    [Performs merging of two DSD formulas.]
@@ -570,6 +601,9 @@ void Dau_DsdRemoveBraces( char * pDsd, int * pMatches )
 ***********************************************************************/
 char * Dau_DsdMerge( char * pDsd0i, int * pPerm0, char * pDsd1i, int * pPerm1, int fCompl0, int fCompl1 )
 {
+    int fVerbose = 0;
+    int fCheck = 1;
+    static int Counter = 0;
     static char pRes[DAU_MAX_STR];
     char pDsd0[DAU_MAX_STR];
     char pDsd1[DAU_MAX_STR];
@@ -583,40 +617,73 @@ char * Dau_DsdMerge( char * pDsd0i, int * pPerm0, char * pDsd1i, int * pPerm1, i
     int pMatches[DAU_MAX_STR];
     int nVarsShared, nVarsTotal;
     Dau_Sto_t S, * pS = &S;
-    word Truth, t, t0, t1;
+    word Truth, t = 0, t0 = 0, t1 = 0;
     int Status;
+    clock_t clk = clock();
+    Counter++;
     // create local copies
     Dau_DsdMergeCopy( pDsd0i, fCompl0, pDsd0 );
     Dau_DsdMergeCopy( pDsd1i, fCompl1, pDsd1 );
+if ( fVerbose )
+printf( "\nAfter copying:\n" );
+if ( fVerbose )
+printf( "%s\n", pDsd0 );
+if ( fVerbose )
+printf( "%s\n", pDsd1 );
     // handle constants
-    if ( pDsd0[1] == 0 || pDsd1[1] == 0 )
+    if ( Dau_DsdIsConst(pDsd0) || Dau_DsdIsConst(pDsd1) )
     {
-        if ( pDsd0[0] == '0' )
+        if ( Dau_DsdIsConst0(pDsd0) )
             strcpy( pRes, pDsd0 );
-        else if ( pDsd0[0] == '1' )
+        else if ( Dau_DsdIsConst1(pDsd0) )
             strcpy( pRes, pDsd1 );
-        else if ( pDsd1[0] == '0' )
+        else if ( Dau_DsdIsConst0(pDsd1) )
             strcpy( pRes, pDsd1 );
-        else if ( pDsd1[0] == '1' )
+        else if ( Dau_DsdIsConst1(pDsd1) )
             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 );
+if ( fVerbose )
+printf( "After replacement:\n" );
+if ( fVerbose )
 printf( "%s\n", pDsd0 );
+if ( fVerbose )
 printf( "%s\n", pDsd1 );
-    t0 = Dau_Dsd6ToTruth( pDsd0 );
-    t1 = Dau_Dsd6ToTruth( pDsd1 );
+
+//s_TimeComp[2] += clock() - clk;
+
+    if ( fCheck )
+        t0 = Dau_Dsd6ToTruth( pDsd0 );
+    if ( fCheck )
+        t1 = Dau_Dsd6ToTruth( pDsd1 );
+
     // find shared varaiables
     nVarsShared = Dau_DsdMergeFindShared(pDsd0, pDsd1, pMatches0, pMatches1, pVarPres);
     if ( nVarsShared == 0 )
     {
         sprintf( pRes, "(%s%s)", pDsd0, pDsd1 );
+if ( fVerbose )
+printf( "Disjoint:\n" );
+if ( fVerbose )
+printf( "%s\n", pRes );
+
+        Dau_DsdMergeMatches( pRes, pMatches );
+        Dau_DsdRemoveBraces( pRes, pMatches );
+        Dau_DsdNormalize( pRes );
+if ( fVerbose )
+printf( "Normalized:\n" );
+if ( fVerbose )
+printf( "%s\n", pRes );
+
+        s_TimeComp[2] += clock() - clk;
         return pRes;
     }
     // create variable mapping
@@ -627,7 +694,11 @@ printf( "%s\n", pDsd1 );
     // find uniqueness status
     Dau_DsdMergeStatus( pDsd0, pMatches0, nVarsShared, pStatus0 );
     Dau_DsdMergeStatus( pDsd1, pMatches1, nVarsShared, pStatus1 );
+if ( fVerbose )
+printf( "Individual status:\n" );
+if ( fVerbose )
 Dau_DsdMergePrintWithStatus( pDsd0, pStatus0 );
+if ( fVerbose )
 Dau_DsdMergePrintWithStatus( pDsd1, pStatus1 );
     // prepare storage
     Dau_DsdMergeStoreClean( pS, nVarsShared );
@@ -635,13 +706,18 @@ Dau_DsdMergePrintWithStatus( pDsd1, pStatus1 );
     Dau_DsdMergeStoreCleanOutput( pS );
     Dau_DsdMergeSubstitute( pS, pDsd0, pMatches0, pStatus0 );
     strcpy( pDsd0, pS->pOutput );
+if ( fVerbose )
+printf( "Substitutions:\n" );
+if ( fVerbose )
 printf( "%s\n", pDsd0 );
 
     // perform substitutions
     Dau_DsdMergeStoreCleanOutput( pS );
     Dau_DsdMergeSubstitute( pS, pDsd1, pMatches1, pStatus1 );
     strcpy( pDsd1, pS->pOutput );
+if ( fVerbose )
 printf( "%s\n", pDsd1 );
+if ( fVerbose )
 Dau_DsdMergeStorePrintDefs( pS );
 
     // create new function
@@ -649,24 +725,50 @@ Dau_DsdMergeStorePrintDefs( pS );
     sprintf( pS->pOutput, "(%s%s)", pDsd0, pDsd1 );
     Truth = Dau_Dsd6ToTruth( pS->pOutput );
     Status = Dau_DsdDecompose( &Truth, nVarsTotal, 0, pS->pOutput );
+//printf( "%d ", Status );
     if ( Status == -1 ) // did not find 1-step DSD
         return NULL;
     if ( Status > 6 ) // non-DSD part is too large
         return NULL;
+    if ( Dau_DsdIsConst(pS->pOutput) )
+    {
+        strcpy( pRes, pS->pOutput );
+        return pRes;
+    }
+if ( fVerbose )
+printf( "Decomposition:\n" );
+if ( fVerbose )
 printf( "%s\n", pS->pOutput );
     // substitute definitions
     Dau_DsdMergeMatches( pS->pOutput, pMatches );
-    Dau_DsdMergeInlineDefinitions( pS->pOutput, pMatches, pS->pVarDefs, pRes, nVarsShared );
+    Dau_DsdMergeInlineDefinitions( pS->pOutput, pMatches, pS, pRes, nVarsShared );
+if ( fVerbose )
+printf( "Inlining:\n" );
+if ( fVerbose )
 printf( "%s\n", pRes );
     // perform variable replacement
     Dau_DsdMergeMatches( pRes, pMatches );
     Dau_DsdMergeReplace( pRes, pMatches, pNew2Old );
     Dau_DsdRemoveBraces( pRes, pMatches );
+if ( fVerbose )
+printf( "Replaced:\n" );
+if ( fVerbose )
 printf( "%s\n", pRes );
     Dau_DsdNormalize( pRes );
+if ( fVerbose )
+printf( "Normalized:\n" );
+if ( fVerbose )
 printf( "%s\n", pRes );
-    t = Dau_Dsd6ToTruth( pRes );
-    assert( t == (t0 & t1) );
+
+    if ( fCheck )
+        t = Dau_Dsd6ToTruth( pRes );
+    if ( t != (t0 & t1) )
+        printf( "Dau_DsdMerge(): Verification failed!\n" );
+
+    if ( Status == 0 )
+        s_TimeComp[0] += clock() - clk;
+    else
+        s_TimeComp[1] += clock() - clk;
     return pRes;
 }
 
@@ -696,11 +798,16 @@ void Dau_DsdTest()
 //    char * pStr2 = "(df)";
 //    char * pStr1 = "(abf)";
 //    char * pStr2 = "(a[(bc)(fde)])";
-    char * pStr1 = "8001{abc[ef]}";
-    char * pStr2 = "(abe)";
+//    char * pStr1 = "8001{abc[ef]}";
+//    char * pStr2 = "(abe)";
+
+    char * pStr1 = "(!(ab)de)";
+    char * pStr2 = "(!(ac)f)";
+
     char * pRes;
     word t = Dau_Dsd6ToTruth( pStr );
     return;
+
 //    pStr2 = Dau_DsdDecompose( &t, 6, 0, NULL );
 //    Dau_DsdNormalize( pStr2 );