Tuning for multi-ouptut solver.

1 files changed, 15 insertions, 2 deletions

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 7af30b0b..0ac0b7cf 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -32439,9 +32439,10 @@ int Abc_CommandAbc9MultiProve( Abc_Frame_t * pAbc, int argc, char ** argv )
     pPars->TimeOutGlo =  30;
     pPars->TimeOutLoc =   2;
     pPars->TimeOutInc = 100;
+    pPars->TimeOutGap =   0;
     pPars->TimePerOut =   0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "TLMHsdvwh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "TLMGHsdvwh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -32478,6 +32479,17 @@ int Abc_CommandAbc9MultiProve( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( pPars->TimeOutInc <= 0 )
                 goto usage;
             break;
+        case 'G':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-G\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->TimeOutGap = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->TimeOutGap <= 0 )
+                goto usage;
+            break;
         case 'H':
             if ( globalUtilOptind >= argc )
             {
@@ -32519,11 +32531,12 @@ int Abc_CommandAbc9MultiProve( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &mprove [-TLMH num] [-sdvwh]\n" );
+    Abc_Print( -2, "usage: &mprove [-TLMGH num] [-sdvwh]\n" );
     Abc_Print( -2, "\t         proves multi-output testcase by applying several engines\n" );
     Abc_Print( -2, "\t-T num : approximate global runtime limit in seconds [default = %d]\n",     pPars->TimeOutGlo );
     Abc_Print( -2, "\t-L num : approximate local runtime limit in seconds [default = %d]\n",      pPars->TimeOutLoc );
     Abc_Print( -2, "\t-M num : percentage of local runtime limit increase [default = %d]\n",      pPars->TimeOutInc );
+    Abc_Print( -2, "\t-G num : approximate gap runtime limit in seconds [default = %d]\n",        pPars->TimeOutGap );
     Abc_Print( -2, "\t-H num : timeout per output in miliseconds [default = %d]\n",               pPars->TimePerOut );
     Abc_Print( -2, "\t-s     : toggle using combinational synthesis [default = %s]\n",            pPars->fUseSyn?      "yes": "no" );
     Abc_Print( -2, "\t-d     : toggle dumping invariant into a file [default = %s]\n",            pPars->fDumpFinal?   "yes": "no" );