Tuning for multi-ouptut solver.

3 files changed, 30 insertions, 4 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" );
diff --git a/src/sat/bmc/bmc.h b/src/sat/bmc/bmc.h
index 74128047..0cfc9b37 100644
--- a/src/sat/bmc/bmc.h
+++ b/src/sat/bmc/bmc.h
@@ -100,6 +100,7 @@ struct Bmc_MulPar_t_
     int         TimeOutGlo;
     int         TimeOutLoc;
     int         TimeOutInc;
+    int         TimeOutGap;
     int         TimePerOut;
     int         fUseSyn;
     int         fDumpFinal;
diff --git a/src/sat/bmc/bmcMulti.c b/src/sat/bmc/bmcMulti.c
index a86228df..cf04ab62 100644
--- a/src/sat/bmc/bmcMulti.c
+++ b/src/sat/bmc/bmcMulti.c
@@ -172,12 +172,17 @@ Vec_Ptr_t * Gia_ManMultiProveAig( Aig_Man_t * p, Bmc_MulPar_t * pPars )
     int TimeOutLoc   = pPars->TimeOutLoc;
     int i, RetValue  = -1;
     if ( pPars->fVerbose )
-        printf( "MultiProve parameters: Global timeout = %d sec.  Local timeout = %d sec.  Time increase = %d %%.\n", pPars->TimeOutGlo, pPars->TimeOutLoc, pPars->TimeOutInc );
+        printf( "MultiProve parameters: Global timeout = %d sec.  Local timeout = %d sec.  Time increase = %d %%.\n", 
+            pPars->TimeOutGlo, pPars->TimeOutLoc, pPars->TimeOutInc );
+    if ( pPars->fVerbose )
+        printf( "Gap timout = %d sec. Per-output timeout = %d msec. Use synthesis = %d. Dump final = %d. Verbose = %d.\n", 
+            pPars->TimeOutGap, pPars->TimePerOut, pPars->fUseSyn, pPars->fDumpFinal, pPars->fVerbose );
     // create output map
     vOutMap = Vec_IntStartNatural( Saig_ManPoNum(p) ); // maps current outputs into their original IDs
     vCexes  = Vec_PtrStart( Saig_ManPoNum(p) );        // maps solved outputs into their CEXes (or markers)
     for ( i = 0; i < 1000; i++ )
     {
+        int nSolved = Vec_PtrCountZero(vCexes);
         // perform SIM3
         Ssw_RarSetDefaultParams( pParsSim );
         pParsSim->fSolveAll = 1;
@@ -240,6 +245,13 @@ Vec_Ptr_t * Gia_ManMultiProveAig( Aig_Man_t * p, Bmc_MulPar_t * pPars )
             break;
         }
 
+        // check gap timeout
+        if ( pPars->TimeOutGap && pPars->TimeOutGap <= TimeOutLoc && nSolved == Vec_PtrCountZero(vCexes) )
+        {
+            printf( "Gap timeout (%d sec) is reached.\n", pPars->TimeOutGap );
+            break;
+        }
+
         // synthesize
         if ( pPars->fUseSyn )
         {
@@ -254,7 +266,7 @@ Vec_Ptr_t * Gia_ManMultiProveAig( Aig_Man_t * p, Bmc_MulPar_t * pPars )
     }
     Vec_IntFree( vOutMap );
     if ( pPars->fVerbose )
-        printf( "The number of const0 POs = %d.\n", Gia_ManCountConst0Pos(p) );
+        printf( "The number of POs proved UNSAT by synthesis = %d.\n", Gia_ManCountConst0Pos(p) );
     if ( pPars->fDumpFinal )
     {
         char * pFileName = Extra_FileNameGenericAppend( p->pName, "_out.aig" );