Updating command 'dsd_clean'.

4 files changed, 45 insertions, 10 deletions

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 78185dd2..ed58d412 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -16232,9 +16232,9 @@ usage:
 int Abc_CommandDsdClean( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     If_DsdMan_t * pDsd = (If_DsdMan_t *)Abc_FrameReadManDsd();
-    int c, nLimit = 0, fVerbose = 0;
+    int c, nLimit = 0, nLutSize = -1, fCleanOccur = 0, fCleanMarks = 0, fVerbose = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "Lvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "LKomvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -16247,6 +16247,21 @@ int Abc_CommandDsdClean( Abc_Frame_t * pAbc, int argc, char ** argv )
             nLimit = atoi(argv[globalUtilOptind]);
             globalUtilOptind++;
             break;
+        case 'K':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-K\" should be followed by a floating point number.\n" );
+                goto usage;
+            }
+            nLutSize = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            break;
+        case 'o':
+            fCleanOccur ^= 1;
+            break;
+        case 'm':
+            fCleanMarks ^= 1;
+            break;
         case 'v':
             fVerbose ^= 1;
             break;
@@ -16263,15 +16278,22 @@ int Abc_CommandDsdClean( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     if ( nLimit > 0 )
         Abc_FrameSetManDsd( If_DsdManFilter(pDsd, nLimit) );
-    else
-        If_DsdManClean( pDsd, fVerbose );
+    if ( nLutSize >= 0 )
+        If_DsdManSetLutSize( pDsd, nLutSize );
+    if ( fCleanOccur )
+        If_DsdManCleanOccur( pDsd, fVerbose );
+    if ( fCleanMarks )
+        If_DsdManCleanMarks( pDsd, fVerbose );
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: dsd_clean [-L num] [-vh]\n" );
-    Abc_Print( -2, "\t         cleans the occurrence counters\n" );
+    Abc_Print( -2, "usage: dsd_clean [-LK num] [-omvh]\n" );
+    Abc_Print( -2, "\t         modifying parameters of the DSD manager\n" );
     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-K num : new LUT size to set for the DSD manager [default = %d]\n",           nLutSize );
+    Abc_Print( -2, "\t-o     : toggles cleaning occurrence counters [default = %s]\n",              fCleanOccur? "yes": "no" );
+    Abc_Print( -2, "\t-m     : toggles cleaning matching marks [default = %s]\n",                   fCleanMarks? "yes": "no" );
+    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 a0180563..8114e5c3 100644
--- a/src/map/if/if.h
+++ b/src/map/if/if.h
@@ -547,13 +547,15 @@ extern void            If_DsdManFree( If_DsdMan_t * p, int fVerbose );
 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 void            If_DsdManCleanOccur( If_DsdMan_t * p, int fVerbose );
+extern void            If_DsdManCleanMarks( 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 );
 extern int             If_DsdManObjNum( If_DsdMan_t * p );
 extern int             If_DsdManLutSize( If_DsdMan_t * p );
+extern void            If_DsdManSetLutSize( If_DsdMan_t * p, int nLutSize );
 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 );
diff --git a/src/map/if/ifDsd.c b/src/map/if/ifDsd.c
index 8afa9e03..48100a1e 100644
--- a/src/map/if/ifDsd.c
+++ b/src/map/if/ifDsd.c
@@ -173,6 +173,10 @@ int If_DsdManLutSize( If_DsdMan_t * p )
 {
     return p->LutSize;
 }
+void If_DsdManSetLutSize( If_DsdMan_t * p, int nLutSize )
+{
+    p->LutSize = nLutSize;
+}
 int If_DsdManSuppSize( If_DsdMan_t * p, int iDsd )
 {
     return If_DsdVecLitSuppSize( &p->vObjs, iDsd );
@@ -1170,13 +1174,20 @@ void If_DsdManMerge( If_DsdMan_t * p, If_DsdMan_t * pNew )
     assert( Vec_IntSize(vMap) == Vec_PtrSize(&pNew->vObjs) );
     Vec_IntFree( vMap );
 }
-void If_DsdManClean( If_DsdMan_t * p, int fVerbose )
+void If_DsdManCleanOccur( If_DsdMan_t * p, int fVerbose )
 {
     If_DsdObj_t * pObj; 
     int i;
     If_DsdVecForEachObj( &p->vObjs, pObj, i )
         pObj->Count = 0;
 }
+void If_DsdManCleanMarks( If_DsdMan_t * p, int fVerbose )
+{
+    If_DsdObj_t * pObj; 
+    int i;
+    If_DsdVecForEachObj( &p->vObjs, pObj, i )
+        pObj->fMark = 0;
+}
 void If_DsdManFilter_rec( If_DsdMan_t * pNew, If_DsdMan_t * p, int i, Vec_Int_t * vMap )
 {
     If_DsdObj_t * pObj;
diff --git a/src/map/if/ifTune.c b/src/map/if/ifTune.c
index e7b1ad05..f75192b6 100644
--- a/src/map/if/ifTune.c
+++ b/src/map/if/ifTune.c
@@ -459,7 +459,7 @@ Ifn_Ntk_t * Ifn_NtkParse( char * pStr )
     }
     Ifn_NtkParseConstraints( pStr, p );
     Abc_TtElemInit2( p->pTtElems, p->nInps );
-    printf( "Finished parsing: " ); Ifn_NtkPrint(p);
+//    printf( "Finished parsing: " ); Ifn_NtkPrint(p);
     return p;
 }