Improvements to Boolean matching.

5 files changed, 57 insertions, 19 deletions

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 923082e0..23983869 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -15312,7 +15312,7 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv )
             pPars->fEnableCheck08 ^= 1;
             break;
         case 'k':
-            pPars->fEnableCheck10 ^= 1;
+            pPars->fUseDsdTune ^= 1;
             break;
         case 't':
             pPars->fDoAverage ^= 1;
@@ -15376,7 +15376,7 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv )
         pPars->fCutMin = 1;
     }
 
-    if ( pPars->fEnableCheck07 + pPars->fEnableCheck08 + pPars->fEnableCheck10 + (pPars->pLutStruct != NULL) > 1 )
+    if ( pPars->fEnableCheck07 + pPars->fEnableCheck08 + pPars->fUseDsdTune + (pPars->pLutStruct != NULL) > 1 )
     {
         Abc_Print( -1, "Only one additional check can be performed at the same time.\n" );
         return 1;
@@ -15401,15 +15401,22 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv )
         pPars->pFuncCell = If_CutPerformCheck08;
         pPars->fCutMin = 1;
     }
-    if ( pPars->fEnableCheck10 )
+    if ( pPars->fUseDsdTune )
     {
-        if ( pPars->nLutSize < 6 || pPars->nLutSize > 10 )
+        If_DsdMan_t * pDsdMan = (If_DsdMan_t *)Abc_FrameReadManDsd();
+        if ( pDsdMan == NULL )
         {
-            Abc_Print( -1, "This feature only works for {6,7,8,9,10}-LUTs.\n" );
+            Abc_Print( -1, "DSD manager is not available.\n" );
+            return 1;
+        }
+        if ( pPars->nLutSize > If_DsdManLutSize(pDsdMan) )
+        {
+            Abc_Print( -1, "LUT size (%d) is more than the number of variables in the DSD manager (%d).\n", pPars->nLutSize, If_DsdManLutSize(pDsdMan) );
             return 1;
         }
-        pPars->pFuncCell = If_CutPerformCheck10;
         pPars->fCutMin = 1;
+        pPars->fUseDsd = 1;
+        If_DsdManSetNewAsUseless( pDsdMan );
     }
     if ( pPars->pLutStruct )
     {
@@ -15604,7 +15611,7 @@ usage:
     Abc_Print( -2, "\t-o       : toggles using buffers to decouple combinational outputs [default = %s]\n", pPars->fUseBuffs? "yes": "no" );
     Abc_Print( -2, "\t-j       : toggles enabling additional check [default = %s]\n", pPars->fEnableCheck07? "yes": "no" );
     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-k       : toggles matching based on precomputed DSD manager [default = %s]\n", pPars->fUseDsdTune? "yes": "no" );
     Abc_Print( -2, "\t-t       : toggles optimizing average rather than maximum level [default = %s]\n", pPars->fDoAverage? "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-c       : toggles computing truth tables in a new way [default = %s]\n", pPars->fUseTtPerm? "yes": "no" );
@@ -31156,7 +31163,7 @@ int Abc_CommandAbc9If( Abc_Frame_t * pAbc, int argc, char ** argv )
             pPars->fEnableCheck08 ^= 1;
             break;
         case 'k':
-            pPars->fEnableCheck10 ^= 1;
+            pPars->fUseDsdTune ^= 1;
             break;
         case 'f':
             pPars->fEnableCheck75 ^= 1;
@@ -31240,7 +31247,7 @@ int Abc_CommandAbc9If( Abc_Frame_t * pAbc, int argc, char ** argv )
         pPars->fCutMin = 1;
     }
 
-    if ( pPars->fEnableCheck07 + pPars->fEnableCheck08 + pPars->fEnableCheck10 + pPars->fEnableCheck75 + pPars->fEnableCheck75u + (pPars->pLutStruct != NULL) > 1 )
+    if ( pPars->fEnableCheck07 + pPars->fEnableCheck08 + pPars->fUseDsdTune + pPars->fEnableCheck75 + pPars->fEnableCheck75u + (pPars->pLutStruct != NULL) > 1 )
     {
         Abc_Print( -1, "Only one additional check can be performed at the same time.\n" );
         return 1;
@@ -31265,15 +31272,22 @@ int Abc_CommandAbc9If( Abc_Frame_t * pAbc, int argc, char ** argv )
         pPars->pFuncCell = If_CutPerformCheck08;
         pPars->fCutMin = 1;
     }
-    if ( pPars->fEnableCheck10 )
+    if ( pPars->fUseDsdTune )
     {
-        if ( pPars->nLutSize < 6 || pPars->nLutSize > 10 )
+        If_DsdMan_t * pDsdMan = (If_DsdMan_t *)Abc_FrameReadManDsd();
+        if ( pDsdMan == NULL )
         {
-            Abc_Print( -1, "This feature only works for {6,7,8,9,10}-LUTs.\n" );
+            Abc_Print( -1, "DSD manager is not available.\n" );
+            return 1;
+        }
+        if ( pPars->nLutSize > If_DsdManLutSize(pDsdMan) )
+        {
+            Abc_Print( -1, "LUT size (%d) is more than the number of variables in the DSD manager (%d).\n", pPars->nLutSize, If_DsdManLutSize(pDsdMan) );
             return 1;
         }
-        pPars->pFuncCell = If_CutPerformCheck10;
         pPars->fCutMin = 1;
+        pPars->fUseDsd = 1;
+        If_DsdManSetNewAsUseless( pDsdMan );
     }
     if ( pPars->fEnableCheck75 || pPars->fEnableCheck75u )
     {
@@ -31454,9 +31468,9 @@ usage:
     Abc_Print( -2, "\t-o       : toggles using buffers to decouple combinational outputs [default = %s]\n", pPars->fUseBuffs? "yes": "no" );
     Abc_Print( -2, "\t-j       : toggles enabling additional check [default = %s]\n", pPars->fEnableCheck07? "yes": "no" );
     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-f       : toggles enabling additional check [default = %s]\n", pPars->fEnableCheck75? "yes": "no" );
     Abc_Print( -2, "\t-u       : toggles enabling additional check [default = %s]\n", pPars->fEnableCheck75u? "yes": "no" );
+    Abc_Print( -2, "\t-k       : toggles matching based on precomputed DSD manager [default = %s]\n", pPars->fUseDsdTune? "yes": "no" );
     Abc_Print( -2, "\t-z       : toggles deriving LUTs when mapping into LUT structures [default = %s]\n", pPars->fDeriveLuts? "yes": "no" );
     Abc_Print( -2, "\t-t       : toggles optimizing average rather than maximum level [default = %s]\n", pPars->fDoAverage? "yes": "no" );
     Abc_Print( -2, "\t-n       : toggles computing DSDs of the cut functions [default = %s]\n", pPars->fUseDsd? "yes": "no" );
diff --git a/src/map/if/if.h b/src/map/if/if.h
index 3527b231..f6849337 100644
--- a/src/map/if/if.h
+++ b/src/map/if/if.h
@@ -130,6 +130,7 @@ struct If_Par_t_
     int                fEnableCheck75;// enable additional checking
     int                fEnableCheck75u;// enable additional checking
     int                fUseDsd;       // compute DSD of the cut functions
+    int                fUseDsdTune;   // use matching based on precomputed manager
     int                fUseTtPerm;    // compute truth tables of the cut functions
     int                fDeriveLuts;   // enables deriving LUT structures
     int                fDoAverage;    // optimize average rather than maximum level
@@ -549,9 +550,12 @@ extern If_DsdMan_t *   If_DsdManFilter( If_DsdMan_t * p, int Limit );
 extern int             If_DsdManCompute( If_DsdMan_t * p, word * pTruth, int nLeaves, unsigned char * pPerm, char * pLutStruct );
 extern char *          If_DsdManFileName( If_DsdMan_t * p );
 extern int             If_DsdManVarNum( If_DsdMan_t * p );
+extern int             If_DsdManObjNum( If_DsdMan_t * p );
 extern int             If_DsdManLutSize( If_DsdMan_t * p );
 extern int             If_DsdManSuppSize( If_DsdMan_t * p, int iDsd );
 extern int             If_DsdManCheckDec( If_DsdMan_t * p, int iDsd );
+extern int             If_DsdManReadMark( If_DsdMan_t * p, int iDsd );
+extern void            If_DsdManSetNewAsUseless( If_DsdMan_t * p );
 extern unsigned        If_DsdManCheckXY( If_DsdMan_t * p, int iDsd, int LutSize, int fDerive, unsigned uMaskNot, int fHighEffort, int fVerbose );
 extern int             If_CutDsdBalanceEval( If_Man_t * p, If_Cut_t * pCut, Vec_Int_t * vAig );
 extern int             If_CutDsdBalancePinDelays( If_Man_t * p, If_Cut_t * pCut, char * pPerm );
diff --git a/src/map/if/ifCut.c b/src/map/if/ifCut.c
index 6303524c..d13d6a49 100644
--- a/src/map/if/ifCut.c
+++ b/src/map/if/ifCut.c
@@ -755,7 +755,7 @@ void If_CutSort( If_Man_t * p, If_Set_t * pCutSet, If_Cut_t * pCut )
          (p->pPars->fUseDsd || p->pPars->fUseBat || 
           p->pPars->pLutStruct || p->pPars->fUserRecLib || 
           p->pPars->fEnableCheck07 || p->pPars->fEnableCheck08 || 
-          p->pPars->fEnableCheck10 || p->pPars->fEnableCheck75 || 
+          p->pPars->fUseDsdTune || p->pPars->fEnableCheck75 || 
           p->pPars->fEnableCheck75u) )
     {
         If_Cut_t * pFirst = pCutSet->ppCuts[0];
diff --git a/src/map/if/ifDsd.c b/src/map/if/ifDsd.c
index 66535b57..27e260d5 100644
--- a/src/map/if/ifDsd.c
+++ b/src/map/if/ifDsd.c
@@ -89,6 +89,7 @@ struct If_DsdMan_t_
     Gia_Man_t *    pTtGia;         // GIA to represent truth tables
     Vec_Int_t *    vCover;         // temporary memory
     void *         pSat;           // SAT solver
+    int            fNewAsUseless;  // set new as useless
     int            nUniqueHits;    // statistics
     int            nUniqueMisses;  // statistics
     abctime        timeDsd;        // statistics
@@ -160,6 +161,10 @@ int If_DsdManVarNum( If_DsdMan_t * p )
 {
     return p->nVars;
 }
+int If_DsdManObjNum( If_DsdMan_t * p )
+{
+    return Vec_PtrSize( &p->vObjs );
+}
 int If_DsdManLutSize( If_DsdMan_t * p )
 {
     return p->LutSize;
@@ -172,6 +177,14 @@ int If_DsdManCheckDec( If_DsdMan_t * p, int iDsd )
 {
     return If_DsdVecObjMark( &p->vObjs, Abc_Lit2Var(iDsd) );
 }
+int If_DsdManReadMark( If_DsdMan_t * p, int iDsd )
+{
+    return If_DsdVecObjMark( &p->vObjs, Abc_Lit2Var(iDsd) );
+}
+void If_DsdManSetNewAsUseless( If_DsdMan_t * p )
+{
+    p->fNewAsUseless = 1;
+}
 
 /**Function*************************************************************
 
@@ -204,7 +217,7 @@ If_DsdObj_t * If_DsdObjAlloc( If_DsdMan_t * p, int Type, int nFans )
     pObj->Type   = Type;
     pObj->nFans  = nFans;
     pObj->Id     = Vec_PtrSize( &p->vObjs );
-    pObj->fMark  = 0;
+    pObj->fMark  = p->fNewAsUseless;
     pObj->Count  = 0;
     Vec_PtrPush( &p->vObjs, pObj );
     Vec_IntPush( &p->vNexts, 0 );
@@ -2401,8 +2414,7 @@ void Id_DsdManTuneStr1( If_DsdMan_t * p, char * pStruct, int nConfls, int fVerbo
         if ( fVeryVerbose )
             printf( "\n" );
         if ( Value == 0 )
-            continue;
-        If_DsdVecObjSetMark( &p->vObjs, i );
+            If_DsdVecObjSetMark( &p->vObjs, i );
     }
     Extra_ProgressBarStop( pProgress );
     printf( "Finished matching %d functions. ", Vec_PtrSize(&p->vObjs) );
@@ -2542,7 +2554,7 @@ void Id_DsdManTuneStr( If_DsdMan_t * p, char * pStruct, int nConfls, int nProcs,
                 {
                     //printf( "Closing obj %d with Thread %d:\n", ThData[i].Id, i );
                     assert( ThData[i].Result == 0 || ThData[i].Result == 1 );
-                    if ( ThData[i].Result == 1 )
+                    if ( ThData[i].Result == 0 )
                         If_DsdVecObjSetMark( &p->vObjs, ThData[i].Id );
                     ThData[i].Id     = -1;
                     ThData[i].Result = -1;
diff --git a/src/map/if/ifMap.c b/src/map/if/ifMap.c
index 2b2d1758..18b1eed2 100644
--- a/src/map/if/ifMap.c
+++ b/src/map/if/ifMap.c
@@ -262,6 +262,14 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPrep
                         p->nCuts5a++;
                 }
             }
+            else if ( p->pPars->fUseDsdTune )
+            {
+                pCut->fUseless = If_DsdManReadMark( p->pIfDsdMan, If_CutDsdLit(p, pCut) );
+                p->nCutsUselessAll += pCut->fUseless;
+                p->nCutsUseless[pCut->nLeaves] += pCut->fUseless;
+                p->nCutsCountAll++;
+                p->nCutsCount[pCut->nLeaves]++;
+            }
         }
         
         // compute the application-specific cost and depth