Improving timeout in the interpolation package.

5 files changed, 38 insertions, 19 deletions

diff --git a/src/aig/int/intCheck.c b/src/aig/int/intCheck.c
index 54bb7ad9..6b36fe30 100644
--- a/src/aig/int/intCheck.c
+++ b/src/aig/int/intCheck.c
@@ -217,7 +217,7 @@ void Inter_CheckAddEqual( Inter_Check_t * p, int iVarA, int iVarB )
   SeeAlso     []
 
 ***********************************************************************/
-int Inter_CheckPerform( Inter_Check_t * p, Cnf_Dat_t * pCnfInt )
+int Inter_CheckPerform( Inter_Check_t * p, Cnf_Dat_t * pCnfInt, int nTimeNewOut )
 {
     Aig_Obj_t * pObj, * pObj2;
     int i, f, VarA, VarB, RetValue, Entry, status;
@@ -225,6 +225,10 @@ int Inter_CheckPerform( Inter_Check_t * p, Cnf_Dat_t * pCnfInt )
     assert( Aig_ManPoNum(p->pCnf->pMan) == p->nFramesK * nRegs );
     assert( Aig_ManPoNum(pCnfInt->pMan) == 1 );
 
+    // set runtime limit
+    if ( nTimeNewOut )
+        sat_solver_set_runtime_limit( p->pSat, nTimeNewOut );
+
     // add clauses to the SAT solver
     Cnf_DataLift( pCnfInt, p->nVars );
     for ( f = 0; f <= p->nFramesK; f++ )
diff --git a/src/aig/int/intCore.c b/src/aig/int/intCore.c
index fdc2241e..ceb0025c 100644
--- a/src/aig/int/intCore.c
+++ b/src/aig/int/intCore.c
@@ -80,7 +80,13 @@ int Inter_ManPerformInterpolation( Aig_Man_t * pAig, Inter_ManParams_t * pPars,
     Inter_Man_t * p;
     Inter_Check_t * pCheck = NULL;
     Aig_Man_t * pAigTemp;
-    int s, i, RetValue, Status, clk, clk2, clkTotal = clock();
+    int s, i, RetValue, Status, clk, clk2, clkTotal = clock(), timeTemp;
+    int nTimeNewOut = 0;
+
+    // set runtime limit
+    if ( pPars->nSecLimit )
+        nTimeNewOut = clock() + pPars->nSecLimit * CLOCKS_PER_SEC;
+
     // sanity checks
     assert( Saig_ManRegNum(pAig) > 0 );
     assert( Saig_ManPiNum(pAig) > 0 );
@@ -171,7 +177,7 @@ p->timeCnf += clock() - clk;
 clk = clock();
             pCnfInter2 = Cnf_Derive( p->pInter, 1 );  
 p->timeCnf += clock() - clk;    
-            RetValue = Inter_CheckPerform( pCheck, pCnfInter2 );
+            RetValue = Inter_CheckPerform( pCheck, pCnfInter2, nTimeNewOut );
 //            assert( RetValue == 0 );
             Cnf_DataFree( pCnfInter2 );
         }
@@ -200,7 +206,7 @@ p->timeCnf += clock() - clk;
             }
             else 
 #endif
-                RetValue = Inter_ManPerformOneStep( p, pPars->fUseBias, pPars->fUseBackward );
+                RetValue = Inter_ManPerformOneStep( p, pPars->fUseBias, pPars->fUseBackward, nTimeNewOut );
 
             if ( pPars->fVerbose )
             {
@@ -228,11 +234,19 @@ p->timeCnf += clock() - clk;
                 Inter_ManClean( p ); 
                 break;
             }
-            else if ( RetValue == -1 ) // timed out
+            else if ( RetValue == -1 ) 
             {
-                if ( pPars->fVerbose )
-                    printf( "Reached limit (%d) on the number of conflicts.\n", p->nConfLimit );
-                assert( p->nConfCur >= p->nConfLimit );
+                if ( pPars->nSecLimit && clock() > nTimeNewOut ) // timed out
+                {
+                    if ( pPars->fVerbose )
+                        printf( "Reached timeout (%d seconds).\n",  pPars->nSecLimit );
+                }
+                else
+                {
+                    assert( p->nConfCur >= p->nConfLimit );
+                    if ( pPars->fVerbose )
+                        printf( "Reached limit (%d) on the number of conflicts.\n", p->nConfLimit );
+                }
                 p->timeTotal = clock() - clkTotal;
                 Inter_ManStop( p );
                 Inter_CheckStop( pCheck );
@@ -275,7 +289,9 @@ clk = clock();
 clk2 = clock();
                         pCnfInter2 = Cnf_Derive( p->pInterNew, 1 );  
 p->timeCnf += clock() - clk2;
-                        Status = Inter_CheckPerform( pCheck, pCnfInter2 );
+timeTemp = clock() - clk2;
+            
+                        Status = Inter_CheckPerform( pCheck, pCnfInter2, nTimeNewOut );
                         Cnf_DataFree( pCnfInter2 );
                     }
                 }
@@ -289,7 +305,7 @@ p->timeCnf += clock() - clk2;
                 else
                     Status = 0;
             }
-p->timeEqu += clock() - clk;
+p->timeEqu += clock() - clk - timeTemp;
             if ( Status ) // contained
             {
                 if ( pPars->fVerbose )
@@ -299,7 +315,7 @@ p->timeEqu += clock() - clk;
                 Inter_CheckStop( pCheck );
                 return 1;
             }
-            if ( pPars->nSecLimit && ((float)pPars->nSecLimit <= (float)(clock()-clkTotal)/(float)(CLOCKS_PER_SEC)) )
+            if ( pPars->nSecLimit && clock() > nTimeNewOut )
             {
                 printf( "Reached timeout (%d seconds).\n",  pPars->nSecLimit );
                 p->timeTotal = clock() - clkTotal;
diff --git a/src/aig/int/intInt.h b/src/aig/int/intInt.h
index d5e8ed00..3eab7883 100644
--- a/src/aig/int/intInt.h
+++ b/src/aig/int/intInt.h
@@ -93,7 +93,7 @@ typedef struct Inter_Check_t_ Inter_Check_t;
 /*=== intCheck.c ============================================================*/
 extern Inter_Check_t * Inter_CheckStart( Aig_Man_t * pTrans, int nFramesK );
 extern void            Inter_CheckStop( Inter_Check_t * p );
-extern int             Inter_CheckPerform( Inter_Check_t * p, Cnf_Dat_t * pCnf );
+extern int             Inter_CheckPerform( Inter_Check_t * p, Cnf_Dat_t * pCnf, int nTimeNewOut );
 
 /*=== intContain.c ============================================================*/
 extern int             Inter_ManCheckContainment( Aig_Man_t * pNew, Aig_Man_t * pOld );
@@ -117,7 +117,7 @@ extern void            Inter_ManClean( Inter_Man_t * p );
 extern void            Inter_ManStop( Inter_Man_t * p );
 
 /*=== intM114.c ============================================================*/
-extern int             Inter_ManPerformOneStep( Inter_Man_t * p, int fUseBias, int fUseBackward );
+extern int             Inter_ManPerformOneStep( Inter_Man_t * p, int fUseBias, int fUseBackward, int nTimeNewOut );
 
 /*=== intM114p.c ============================================================*/
 #ifdef ABC_USE_LIBRARIES
diff --git a/src/aig/int/intM114.c b/src/aig/int/intM114.c
index c1718eae..139c9bbd 100644
--- a/src/aig/int/intM114.c
+++ b/src/aig/int/intM114.c
@@ -200,7 +200,7 @@ sat_solver * Inter_ManDeriveSatSolver(
   SeeAlso     []
 
 ***********************************************************************/
-int Inter_ManPerformOneStep( Inter_Man_t * p, int fUseBias, int fUseBackward )
+int Inter_ManPerformOneStep( Inter_Man_t * p, int fUseBias, int fUseBackward, int nTimeNewOut )
 {
     sat_solver * pSat;
     void * pSatCnf = NULL;
@@ -219,6 +219,10 @@ int Inter_ManPerformOneStep( Inter_Man_t * p, int fUseBias, int fUseBackward )
         return 1;
     }
 
+    // set runtime limit
+    if ( nTimeNewOut )
+        sat_solver_set_runtime_limit( pSat, nTimeNewOut );
+
     // collect global variables
     pGlobalVars = ABC_CALLOC( int, sat_solver_nvars(pSat) );
     Vec_IntForEachEntry( p->vVarsAB, Var, i )
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index e8ac4d76..f4fb5ccc 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -8535,11 +8535,6 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
 */
 
-{
-//    extern void Ssm_ManExperiment( char * pFileIn, char * pFileOut );
-//    Ssm_ManExperiment( "m\\big2.ssim", "m\\big2_.ssim" );
-}
-
     return 0;
 usage:
     Abc_Print( -2, "usage: test [-CKDN] [-vwh] <file_name>\n" );