Provide number of max cubes as parameter.

3 files changed, 21 insertions, 7 deletions

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 2dab60c9..a3b40084 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -40401,13 +40401,13 @@ usage:
 ***********************************************************************/
 int Abc_CommandAbc9Exorcism( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
-    extern int Abc_ExorcismMain( Vec_Wec_t * vEsop, int nIns, int nOuts, char * pFileNameOut, int Quality, int Verbosity, int fUseQCost );
+    extern int Abc_ExorcismMain( Vec_Wec_t * vEsop, int nIns, int nOuts, char * pFileNameOut, int Quality, int Verbosity, int nCubesMax, int fUseQCost );
     extern Gia_Man_t * Eso_ManCompute( Gia_Man_t * pGia, int fVerbose, Vec_Wec_t ** pvRes );
     Vec_Wec_t * vEsop = NULL;
     char * pFileNameOut = NULL;
-    int c, Quality = 2, Verbosity = 0, fUseQCost = 0, fVerbose = 0;
+    int c, Quality = 2, Verbosity = 0, nCubesMax = 20000, fUseQCost = 0, fVerbose = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "QVqvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "QVCqvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -40433,6 +40433,17 @@ int Abc_CommandAbc9Exorcism( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( Verbosity < 0 )
                 goto usage;
             break;
+        case 'C':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-C\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nCubesMax = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nCubesMax < 0 )
+                goto usage;
+            break;
         case 'q':
             fUseQCost ^= 1;
             break;
@@ -40455,7 +40466,7 @@ int Abc_CommandAbc9Exorcism( Abc_Frame_t * pAbc, int argc, char ** argv )
         pFileNameOut = argv[globalUtilOptind];
     // generate starting cover and run minimization
     Eso_ManCompute( pAbc->pGia, fVerbose, &vEsop );
-    Abc_ExorcismMain( vEsop, Gia_ManCiNum(pAbc->pGia), Gia_ManCoNum(pAbc->pGia), pFileNameOut, Quality, Verbosity, fUseQCost );
+    Abc_ExorcismMain( vEsop, Gia_ManCiNum(pAbc->pGia), Gia_ManCoNum(pAbc->pGia), pFileNameOut, Quality, Verbosity, nCubesMax, fUseQCost );
     Vec_WecFree( vEsop );
     return 0;
 
@@ -40466,6 +40477,7 @@ usage:
     Abc_Print( -2, "                increasing this number improves quality and adds to runtime\n");
     Abc_Print( -2, "        -V N  : verbosity level [default = %d]\n", Verbosity);
     Abc_Print( -2, "                0 = no output; 1 = outline; 2 = verbose\n");
+  Abc_Print( -2, "        -C N  : maximum number of cubes in startign cover [default = %s]\n", nCubesMax );
 //    Abc_Print( -2, "        -q    : toggle using quantum cost [default = %s]\n", fUseQCost? "yes": "no" );
     Abc_Print( -2, "        <file>: the output file name in ESOP-PLA format\n");
     Abc_Print( -2, "\n" );
diff --git a/src/base/exor/exor.c b/src/base/exor/exor.c
index e800744c..9aec90d7 100644
--- a/src/base/exor/exor.c
+++ b/src/base/exor/exor.c
@@ -742,9 +742,9 @@ int Exorcism( Vec_Wec_t * vEsop, int nIns, int nOuts, char * pFileNameOut )
     printf( "The number of cubes in the starting cover is %d\n", g_CoverInfo.nCubesBefore );
     }
 
-    if ( g_CoverInfo.nCubesBefore > 20000 )
+    if ( g_CoverInfo.nCubesBefore > g_CoverInfo.nCubesMax )
     {
-        printf( "\nThe size of the starting cover is more than 20000 cubes. Quitting...\n" );
+        printf( "\nThe size of the starting cover is more than %d cubes. Quitting...\n", g_CoverInfo.nCubesMax );
         return 0;
     }
 
@@ -852,11 +852,12 @@ int Exorcism( Vec_Wec_t * vEsop, int nIns, int nOuts, char * pFileNameOut )
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_ExorcismMain( Vec_Wec_t * vEsop, int nIns, int nOuts, char * pFileNameOut, int Quality, int Verbosity, int fUseQCost )
+int Abc_ExorcismMain( Vec_Wec_t * vEsop, int nIns, int nOuts, char * pFileNameOut, int Quality, int Verbosity, int nCubesMax, int fUseQCost )
 {
     memset( &g_CoverInfo, 0, sizeof(cinfo) );
     g_CoverInfo.Quality = Quality;
     g_CoverInfo.Verbosity = Verbosity;
+    g_CoverInfo.nCubesMax = nCubesMax;
     g_CoverInfo.fUseQCost = fUseQCost;
     if ( g_CoverInfo.Verbosity )
     {
diff --git a/src/base/exor/exor.h b/src/base/exor/exor.h
index 15a62bbe..afd9cc08 100644
--- a/src/base/exor/exor.h
+++ b/src/base/exor/exor.h
@@ -112,6 +112,7 @@ typedef struct cinfo_tag
 
     int Verbosity;      // verbosity level
     int Quality;        // quality
+    int nCubesMax;      // maximum number of cubes in starting cover
     int fUseQCost;      // use q-cost instead of literal count
 
     abctime TimeRead;   // reading time