Improving DSD manager.

3 files changed, 89 insertions, 6 deletions

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index c39eea0a..923082e0 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -16223,12 +16223,22 @@ usage:
 ***********************************************************************/
 int Abc_CommandDsdClean( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
-    int c, fVerbose = 0;
+    If_DsdMan_t * pDsd = (If_DsdMan_t *)Abc_FrameReadManDsd();
+    int c, nLimit = 0, fVerbose = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "Lvh" ) ) != EOF )
     {
         switch ( c )
         {
+        case 'L':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-L\" should be followed by a floating point number.\n" );
+                goto usage;
+            }
+            nLimit = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            break;
         case 'v':
             fVerbose ^= 1;
             break;
@@ -16238,18 +16248,22 @@ int Abc_CommandDsdClean( Abc_Frame_t * pAbc, int argc, char ** argv )
             goto usage;
         }
     }
-    if ( !Abc_FrameReadManDsd() )
+    if ( pDsd == NULL )
     {
         Abc_Print( -1, "The DSD manager is not started.\n" );
         return 0;
     }
-    If_DsdManClean( (If_DsdMan_t *)Abc_FrameReadManDsd(), fVerbose );
+    if ( nLimit > 0 )
+        Abc_FrameSetManDsd( If_DsdManFilter(pDsd, nLimit) );
+    else
+        If_DsdManClean( pDsd, fVerbose );
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: dsd_clean [-K num] [-vh]\n" );
+    Abc_Print( -2, "usage: dsd_clean [-L num] [-vh]\n" );
     Abc_Print( -2, "\t         cleans the occurrence counters\n" );
-    Abc_Print( -2, "\t-v     : toggles verbose output [default = %s]\n",          fVerbose? "yes": "no" );
+    Abc_Print( -2, "\t-L num : remove structures with fewer occurances that this [default = %d]\n", nLimit );
+    Abc_Print( -2, "\t-v     : toggles verbose output [default = %s]\n", fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h     : print the command usage\n");
     return 1;
 }
diff --git a/src/map/if/if.h b/src/map/if/if.h
index 1d5dec16..3527b231 100644
--- a/src/map/if/if.h
+++ b/src/map/if/if.h
@@ -545,6 +545,7 @@ extern void            If_DsdManSave( If_DsdMan_t * p, char * pFileName );
 extern If_DsdMan_t *   If_DsdManLoad( char * pFileName );
 extern void            If_DsdManMerge( If_DsdMan_t * p, If_DsdMan_t * pNew );
 extern void            If_DsdManClean( If_DsdMan_t * p, int fVerbose );
+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 );
diff --git a/src/map/if/ifDsd.c b/src/map/if/ifDsd.c
index a8224d63..66535b57 100644
--- a/src/map/if/ifDsd.c
+++ b/src/map/if/ifDsd.c
@@ -378,6 +378,15 @@ void If_DsdManDumpAll( If_DsdMan_t * p, int Support )
     }
     fclose( pFile );
 }
+int If_DsdManHasMarks( If_DsdMan_t * p )
+{
+    If_DsdObj_t * pObj;
+    int i;
+    If_DsdVecForEachObj( &p->vObjs, pObj, i )
+        if ( pObj->fMark )
+            return 1;
+    return 0;
+}
 
 /**Function*************************************************************
 
@@ -651,6 +660,24 @@ void If_DsdManPrint( If_DsdMan_t * p, char * pFileName, int Number, int Support,
         printf( "cannot open output file\n" );
         return;
     }
+    if ( fVerbose )
+    {
+        fprintf( pFile, "*****  NOTATIONS USED BELOW  *****\n" );
+        fprintf( pFile, "Support -- the support size\n" );
+        fprintf( pFile, "Obj     -- the number of nodes in the DSD manager for each support size\n" );
+        fprintf( pFile, "           (the constant node and the primary input node have no support)\n" );
+        fprintf( pFile, "ObjNDSD -- the number of prime nodes (that is, nodes whose function has no DSD)\n" );
+        fprintf( pFile, "           (percentage is relative to the number of all nodes of that size)\n" );
+        fprintf( pFile, "NPNNDSD -- the number of different NPN classes of prime nodes\n" );
+        fprintf( pFile, "           (Each NPN class may appear more than once. For example: F1 = 17(ab(cd))\n" ); 
+        fprintf( pFile, "           and F2 = 17(ab[cd]) both have prime majority node (hex TT is 17),\n" ); 
+        fprintf( pFile, "           but in one case the majority node is fed by AND, and in another by XOR.\n" );
+        fprintf( pFile, "           These two majority nodes are different nodes in the DSD manager\n" );
+        fprintf( pFile, "Str     -- the number of structures for each support size\n" );
+        fprintf( pFile, "           (each structure is composed of one or more nodes)\n" );
+        fprintf( pFile, "StrNDSD -- the number of DSD structures containing at least one prime node\n" );
+        fprintf( pFile, "Marked  -- the number of DSD structures matchable with the LUT structure (say, \"44\")\n" );
+    }
     If_DsdVecForEachObj( &p->vObjs, pObj, i )
     {
         if ( If_DsdObjType(pObj) == IF_DSD_PRIME )
@@ -1105,6 +1132,9 @@ void If_DsdManMerge( If_DsdMan_t * p, If_DsdMan_t * pNew )
         printf( "LUT size should be the same.\n" );
         return;
     }
+    if ( If_DsdManHasMarks(p) != If_DsdManHasMarks(pNew) )
+        printf( "Warning! Old manager has %smarks while new manager has %smarks.\n", 
+            If_DsdManHasMarks(p) ? "" : "no ", If_DsdManHasMarks(pNew) ? "" : "no " );
     vMap = Vec_IntAlloc( Vec_PtrSize(&pNew->vObjs) );
     Vec_IntPush( vMap, 0 );
     Vec_IntPush( vMap, 1 );
@@ -1113,6 +1143,8 @@ void If_DsdManMerge( If_DsdMan_t * p, If_DsdMan_t * pNew )
         If_DsdObjForEachFaninLit( &pNew->vObjs, pObj, iFanin, k )
             pFanins[k] = Abc_Lit2LitV( Vec_IntArray(vMap), iFanin );
         Id = If_DsdObjFindOrAdd( p, pObj->Type, pFanins, pObj->nFans, pObj->Type == IF_DSD_PRIME ? If_DsdObjTruth(pNew, pObj) : NULL );
+        if ( pObj->fMark )
+            If_DsdVecObjSetMark( &p->vObjs, Id );
         Vec_IntPush( vMap, Id );
     }
     assert( Vec_IntSize(vMap) == Vec_PtrSize(&pNew->vObjs) );
@@ -1125,6 +1157,42 @@ void If_DsdManClean( If_DsdMan_t * p, int fVerbose )
     If_DsdVecForEachObj( &p->vObjs, pObj, i )
         pObj->Count = 0;
 }
+void If_DsdManFilter_rec( If_DsdMan_t * pNew, If_DsdMan_t * p, int i, Vec_Int_t * vMap )
+{
+    If_DsdObj_t * pObj;
+    int pFanins[DAU_MAX_VAR];
+    int k, iFanin, Id;
+    if ( Vec_IntEntry(vMap, i) >= 0 )
+        return;
+    // call recursively
+    pObj = If_DsdVecObj( &p->vObjs, i );
+    If_DsdObjForEachFaninLit( &p->vObjs, pObj, iFanin, k )
+        If_DsdManFilter_rec( pNew, p, Abc_Lit2Var(iFanin), vMap );
+    // duplicate this one
+    If_DsdObjForEachFaninLit( &p->vObjs, pObj, iFanin, k )
+        pFanins[k] = Abc_Lit2LitV( Vec_IntArray(vMap), iFanin );
+    Id = If_DsdObjFindOrAdd( pNew, pObj->Type, pFanins, pObj->nFans, pObj->Type == IF_DSD_PRIME ? If_DsdObjTruth(p, pObj) : NULL );
+    if ( pObj->fMark )
+        If_DsdVecObjSetMark( &pNew->vObjs, Id );
+    If_DsdVecObj( &pNew->vObjs, Id )->Count = pObj->Count;
+    // save the result
+    Vec_IntWriteEntry( vMap, i, Id );
+}
+If_DsdMan_t * If_DsdManFilter( If_DsdMan_t * p, int Limit )
+{
+    If_DsdMan_t * pNew = If_DsdManAlloc( p->nVars, p->LutSize );
+    If_DsdObj_t * pObj; 
+    Vec_Int_t * vMap;
+    int i;
+    vMap = Vec_IntStartFull( Vec_PtrSize(&p->vObjs) );
+    Vec_IntWriteEntry( vMap, 0, 0 );
+    Vec_IntWriteEntry( vMap, 1, 1 );
+    If_DsdVecForEachNode( &p->vObjs, pObj, i )
+        if ( (int)pObj->Count >= Limit )
+            If_DsdManFilter_rec( pNew, p, i, vMap );
+    Vec_IntFree( vMap );
+    return pNew;
+}
 
 /**Function*************************************************************