Tuning for multi-ouptut solver.

5 files changed, 51 insertions, 4 deletions

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 69e8ed84..d94adf08 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -32439,8 +32439,9 @@ int Abc_CommandAbc9MultiProve( Abc_Frame_t * pAbc, int argc, char ** argv )
     pPars->TimeOutGlo =  30;
     pPars->TimeOutLoc =   2;
     pPars->TimeOutInc = 100;
+    pPars->TimePerOut =   0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "TLMsdvwh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "TLMHsdvwh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -32477,6 +32478,17 @@ int Abc_CommandAbc9MultiProve( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( pPars->TimeOutInc <= 0 )
                 goto usage;
             break;
+        case 'H':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-M\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->TimePerOut = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->TimePerOut <= 0 )
+                goto usage;
+            break;
         case 's':
             pPars->fUseSyn ^= 1;
             break;
@@ -32512,6 +32524,7 @@ usage:
     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-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" );
     Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n",             pPars->fVerbose?     "yes": "no" );
diff --git a/src/misc/util/utilCex.c b/src/misc/util/utilCex.c
index b0ce66be..1399f55d 100644
--- a/src/misc/util/utilCex.c
+++ b/src/misc/util/utilCex.c
@@ -351,7 +351,10 @@ void Abc_CexFreeP( Abc_Cex_t ** p )
 {
     if ( *p == NULL )
         return;
-    ABC_FREE( *p );
+    if ( *p == (Abc_Cex_t *)(ABC_PTRINT_T)1 )
+        *p = NULL;
+    else
+        ABC_FREE( *p );
 }
 
 /**Function*************************************************************
diff --git a/src/sat/bmc/bmc.h b/src/sat/bmc/bmc.h
index 5d45c562..74128047 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         TimePerOut;
     int         fUseSyn;
     int         fDumpFinal;
     int         fVerbose;
diff --git a/src/sat/bmc/bmcBmc3.c b/src/sat/bmc/bmcBmc3.c
index 28b89f7b..72fbcc21 100644
--- a/src/sat/bmc/bmcBmc3.c
+++ b/src/sat/bmc/bmcBmc3.c
@@ -1649,7 +1649,7 @@ nTimeSat += Abc_Clock() - clk2;
                     Vec_PtrWriteEntry( p->vCexes, k, Abc_CexDup(pCexNew, Saig_ManRegNum(pAig)) );
                 }
                 Abc_CexFreeP( &pCexNew0 );
-                Abc_CexFreeP( &pCexNew );
+                Abc_CexFree( pCexNew );
             }
             else 
             {
diff --git a/src/sat/bmc/bmcMulti.c b/src/sat/bmc/bmcMulti.c
index 699835ca..1968b5a8 100644
--- a/src/sat/bmc/bmcMulti.c
+++ b/src/sat/bmc/bmcMulti.c
@@ -75,6 +75,34 @@ Vec_Int_t * Gia_ManProcessOutputs( Vec_Ptr_t * vCexesIn, Vec_Ptr_t * vCexesOut,
 
 /**Function*************************************************************
 
+  Synopsis    [Counts the number of constant 0 POs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Gia_ManCountConst0PosGia( Gia_Man_t * p )
+{
+    Gia_Obj_t * pObj;
+    int i, Counter = 0;
+    Gia_ManForEachPo( p, pObj, i )
+        Counter += (Gia_ObjFaninLit0p(p, pObj) == 0);
+    return Counter;
+}
+int Gia_ManCountConst0Pos( Aig_Man_t * p )
+{
+    Aig_Obj_t * pObj;
+    int i, Counter = 0;
+    Saig_ManForEachPo( p, pObj, i )
+        Counter += (Aig_ObjChild0(pObj) == Aig_ManConst0(p));
+    return Counter;
+}
+
+/**Function*************************************************************
+
   Synopsis    []
 
   Description []
@@ -186,7 +214,7 @@ Vec_Ptr_t * Gia_ManMultiProveAig( Aig_Man_t * p, Bmc_MulPar_t * pPars )
         pParsBmc->fNotVerbose = 1;
         pParsBmc->fSilent = !pPars->fVeryVerbose;
         pParsBmc->nTimeOut = TimeOutLoc;
-        pParsBmc->nTimeOutOne = 100;
+        pParsBmc->nTimeOutOne = pPars->TimePerOut;
         RetValue *= Saig_ManBmcScalable( p, pParsBmc );
         if ( pPars->fVeryVerbose )
             Abc_Print( 1, "Some outputs are SAT (%d out of %d) after %d frames.\n", 
@@ -225,6 +253,8 @@ Vec_Ptr_t * Gia_ManMultiProveAig( Aig_Man_t * p, Bmc_MulPar_t * pPars )
         TimeOutLoc += TimeOutLoc * pPars->TimeOutInc / 100;
     }
     Vec_IntFree( vOutMap );
+    if ( pPars->fVerbose )
+        printf( "The number of const0 POs = %d.\n", Gia_ManCountConst0Pos(p) );
     if ( pPars->fDumpFinal )
     {
         char * pFileName = Extra_FileNameGenericAppend( p->pName, "_out.aig" );