Improvements to Boolean matching.

4 files changed, 29 insertions, 5 deletions

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