Improvements to Boolean matching.

1 files changed, 29 insertions, 4 deletions

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index dad29ae5..091b3b88 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -16042,9 +16042,11 @@ usage:
 ***********************************************************************/
 int Abc_CommandDsdTune( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
-    int c, fVerbose = 0, fFast = 0, fAdd = 0, fSpec = 0, LutSize = 0;
+    char * pStruct = NULL;
+    int c, fVerbose = 0, fFast = 0, fAdd = 0, fSpec = 0, LutSize = 0, nConfls = 10000;
+    If_DsdMan_t * pDsdMan = (If_DsdMan_t *)Abc_FrameReadManDsd();
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "Kfasvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "KCSfasvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -16059,6 +16061,24 @@ int Abc_CommandDsdTune( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( LutSize < 4 || LutSize > 6 )
                 goto usage;
             break;
+        case 'C':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-C\" should be followed by a floating point number.\n" );
+                goto usage;
+            }
+            nConfls = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            break;
+        case 'S':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-S\" should be followed by string.\n" );
+                goto usage;
+            }
+            pStruct = argv[globalUtilOptind];
+            globalUtilOptind++;
+            break;
         case 'f':
             fFast ^= 1;
             break;
@@ -16082,17 +16102,22 @@ int Abc_CommandDsdTune( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_Print( 1, "The DSD manager is not started.\n" );
         return 0;
     }
-    If_DsdManTune( (If_DsdMan_t *)Abc_FrameReadManDsd(), LutSize, fFast, fAdd, fSpec, fVerbose );
+    if ( pStruct )
+        Id_DsdManTuneStr( pDsdMan, pStruct, nConfls, fVerbose );
+    else
+        If_DsdManTune( pDsdMan, LutSize, fFast, fAdd, fSpec, fVerbose );
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: dsd_tune [-K num] [-fasvh]\n" );
+    Abc_Print( -2, "usage: dsd_tune [-KC num] [-fasvh] [-S str]\n" );
     Abc_Print( -2, "\t         tunes DSD manager for the given LUT size\n" );
     Abc_Print( -2, "\t-K num : LUT size used for tuning [default = %d]\n",        LutSize );
+    Abc_Print( -2, "\t-C num : the maximum number of conflicts [default = %d]\n", nConfls );
     Abc_Print( -2, "\t-f     : toggles using fast check [default = %s]\n",        fFast? "yes": "no" );
     Abc_Print( -2, "\t-a     : toggles adding tuning to the current one [default = %s]\n",    fAdd? "yes": "no" );
     Abc_Print( -2, "\t-s     : toggles using specialized check [default = %s]\n", fSpec? "yes": "no" );
     Abc_Print( -2, "\t-v     : toggles verbose output [default = %s]\n",          fVerbose? "yes": "no" );
+    Abc_Print( -2, "\t-S str : string representing programmable cell [default = %s]\n", pStruct ? pStruct : "not used" );
     Abc_Print( -2, "\t-h     : print the command usage\n");
     return 1;
 }