Improved DSD.

src/map/if/ifMan.c

@@ -32,7 +32,7 @@ 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];
+extern clock_t s_TimeComp[4];
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -158,6 +158,7 @@ void If_ManStop( If_Man_t * p )
         Abc_PrintTime( 1, "Time0", s_TimeComp[0] );
         Abc_PrintTime( 1, "Time1", s_TimeComp[1] );
         Abc_PrintTime( 1, "Time2", s_TimeComp[2] );
+        Abc_PrintTime( 1, "Time3", s_TimeComp[3] );
 //        Abc_NamPrint( p->pNamDsd );
         Abc_NamStop( p->pNamDsd );
     }

src/map/if/ifTruth.c

@@ -519,6 +519,15 @@ static inline int If_CutComputeTruth6( If_Man_t * p, If_Cut_t * pCut, If_Cut_t *
     t0 = If_TruthStretch6( t0, pCut, pCut0 );
     t1 = If_TruthStretch6( t1, pCut, pCut1 );
     *If_CutTruthW(pCut) = t0 & t1;
+
+    if ( 0 )
+    {
+        word pCopy[1024];
+        char pCanonPerm[16];
+        memcpy( pCopy, If_CutTruthW(pCut), sizeof(word) * 1 );
+        Abc_TtCanonicize( pCopy, pCut->nLimit, pCanonPerm );
+    }
+
     if ( p->pPars->fCutMin )
         return If_CutTruthMinimize6( p, pCut );
     return 0;
@@ -628,6 +637,15 @@ inline int If_CutComputeTruth2( If_Man_t * p, If_Cut_t * pCut, If_Cut_t * pCut0,
     If_TruthStretch2( (word *)p->puTemp[0], pCut, pCut0 );
     If_TruthStretch2( (word *)p->puTemp[1], pCut, pCut1 );
     Abc_TtAnd( If_CutTruthW(pCut), (word *)p->puTemp[0], (word *)p->puTemp[1], nWords, 0 );
+
+    if ( 0 )
+    {
+        word pCopy[1024];
+        char pCanonPerm[16];
+        memcpy( pCopy, If_CutTruthW(pCut), sizeof(word) * nWords );
+        Abc_TtCanonicize( pCopy, pCut->nLimit, pCanonPerm );
+    }
+
     if ( p->pPars->fCutMin )
         return If_CutTruthMinimize2( p, pCut );
     return 0;

src/opt/dau/dauDsd.c

@@ -1498,6 +1498,7 @@ void Dau_DsdTest44()
 //    Dau_DsdNormalize( pStr2 );
 //    Dau_DsdExtract( pStr, 2, 0 );
     t = 0; 
+    nNonDec = 0;
 }
 
 void Dau_DsdTest33()

src/opt/dau/dauMerge.c

@@ -586,7 +586,7 @@ void Dau_DsdRemoveBraces( char * pDsd, int * pMatches )
 }
 
 
-clock_t s_TimeComp[3] = {0};
+clock_t s_TimeComp[4] = {0};
 
 /**Function*************************************************************
 
@@ -602,7 +602,7 @@ clock_t s_TimeComp[3] = {0};
 char * Dau_DsdMerge( char * pDsd0i, int * pPerm0, char * pDsd1i, int * pPerm1, int fCompl0, int fCompl1 )
 {
     int fVerbose = 0;
-    int fCheck = 1;
+    int fCheck = 0;
     static int Counter = 0;
     static char pRes[DAU_MAX_STR];
     char pDsd0[DAU_MAX_STR];
@@ -658,7 +658,6 @@ printf( "%s\n", pDsd0 );
 if ( fVerbose )
 printf( "%s\n", pDsd1 );
 
-//s_TimeComp[2] += clock() - clk;
 
     if ( fCheck )
         t0 = Dau_Dsd6ToTruth( pDsd0 );
@@ -683,9 +682,10 @@ printf( "Normalized:\n" );
 if ( fVerbose )
 printf( "%s\n", pRes );
 
-        s_TimeComp[2] += clock() - clk;
+        s_TimeComp[0] += clock() - clk;
         return pRes;
     }
+s_TimeComp[3] += clock() - clk;
     // create variable mapping
     nVarsTotal = Dau_DsdMergeCreateMaps( pVarPres, nVarsShared, pOld2New, pNew2Old );
     // perform variable replacement
@@ -766,9 +766,9 @@ printf( "%s\n", pRes );
         printf( "Dau_DsdMerge(): Verification failed!\n" );
 
     if ( Status == 0 )
-        s_TimeComp[0] += clock() - clk;
-    else
         s_TimeComp[1] += clock() - clk;
+    else
+        s_TimeComp[2] += clock() - clk;
     return pRes;
 }