Fixing time primtouts throughout the code.

6 files changed, 22 insertions, 19 deletions

diff --git a/src/proof/int/intCheck.c b/src/proof/int/intCheck.c
index 2b14d8ae..28ef54a7 100644
--- a/src/proof/int/intCheck.c
+++ b/src/proof/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 nTimeNewOut )
+int Inter_CheckPerform( Inter_Check_t * p, Cnf_Dat_t * pCnfInt, clock_t nTimeNewOut )
 {
     Aig_Obj_t * pObj, * pObj2;
     int i, f, VarA, VarB, RetValue, Entry, status;
diff --git a/src/proof/int/intCore.c b/src/proof/int/intCore.c
index d4ef1f94..c226c7e1 100644
--- a/src/proof/int/intCore.c
+++ b/src/proof/int/intCore.c
@@ -80,8 +80,9 @@ 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(), timeTemp = 0;
-    int nTimeNewOut = pPars->nSecLimit ? time(NULL) + pPars->nSecLimit : 0;
+    int s, i, RetValue, Status;
+    clock_t clk, clk2, clkTotal = clock(), timeTemp = 0;
+    clock_t nTimeNewOut = pPars->nSecLimit ? pPars->nSecLimit * CLOCKS_PER_SEC + clock() : 0;
 
     // enable ORing of the interpolants, if containment check is performed inductively with K > 1
     if ( pPars->nFramesK > 1 )
@@ -256,7 +257,7 @@ p->timeEqu += clock() - clk;
             }
             else if ( RetValue == -1 ) 
             {
-                if ( pPars->nSecLimit && time(NULL) > nTimeNewOut ) // timed out
+                if ( pPars->nSecLimit && clock() > nTimeNewOut ) // timed out
                 {
                     if ( pPars->fVerbose )
                         printf( "Reached timeout (%d seconds).\n",  pPars->nSecLimit );
@@ -341,7 +342,7 @@ p->timeEqu += clock() - clk - timeTemp;
                 Inter_CheckStop( pCheck );
                 return 1;
             }
-            if ( pPars->nSecLimit && time(NULL) > nTimeNewOut )
+            if ( pPars->nSecLimit && clock() > nTimeNewOut )
             {
                 printf( "Reached timeout (%d seconds).\n",  pPars->nSecLimit );
                 p->timeTotal = clock() - clkTotal;
diff --git a/src/proof/int/intCtrex.c b/src/proof/int/intCtrex.c
index 04aaa271..840ae75d 100644
--- a/src/proof/int/intCtrex.c
+++ b/src/proof/int/intCtrex.c
@@ -99,7 +99,8 @@ void * Inter_ManGetCounterExample( Aig_Man_t * pAig, int nFrames, int fVerbose )
     Aig_Man_t * pFrames;
     sat_solver * pSat;
     Cnf_Dat_t * pCnf;
-    int status, clk = clock();
+    int status;
+    clock_t clk = clock();
     Vec_Int_t * vCiIds;
     // create timeframes
     assert( Saig_ManPoNum(pAig) == 1 );
diff --git a/src/proof/int/intInt.h b/src/proof/int/intInt.h
index 6a033d85..ec2a0356 100644
--- a/src/proof/int/intInt.h
+++ b/src/proof/int/intInt.h
@@ -70,13 +70,13 @@ struct Inter_Man_t_
     int              nConfLimit;   // the limit on the number of conflicts
     int              fVerbose;     // the verbosiness flag
     // runtime
-    int              timeRwr;
-    int              timeCnf;
-    int              timeSat;
-    int              timeInt;
-    int              timeEqu;
-    int              timeOther;
-    int              timeTotal;
+    clock_t          timeRwr;
+    clock_t          timeCnf;
+    clock_t          timeSat;
+    clock_t          timeInt;
+    clock_t          timeEqu;
+    clock_t          timeOther;
+    clock_t          timeTotal;
 };
 
 // containment checking manager
@@ -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, int nTimeNewOut );
+extern int             Inter_CheckPerform( Inter_Check_t * p, Cnf_Dat_t * pCnf, clock_t 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, int fProved );
 
 /*=== intM114.c ============================================================*/
-extern int             Inter_ManPerformOneStep( Inter_Man_t * p, int fUseBias, int fUseBackward, int nTimeNewOut );
+extern int             Inter_ManPerformOneStep( Inter_Man_t * p, int fUseBias, int fUseBackward, clock_t nTimeNewOut );
 
 /*=== intM114p.c ============================================================*/
 #ifdef ABC_USE_LIBRARIES
diff --git a/src/proof/int/intM114.c b/src/proof/int/intM114.c
index ed3ef80e..bf44696d 100644
--- a/src/proof/int/intM114.c
+++ b/src/proof/int/intM114.c
@@ -200,15 +200,16 @@ sat_solver * Inter_ManDeriveSatSolver(
   SeeAlso     []
 
 ***********************************************************************/
-int Inter_ManPerformOneStep( Inter_Man_t * p, int fUseBias, int fUseBackward, int nTimeNewOut )
+int Inter_ManPerformOneStep( Inter_Man_t * p, int fUseBias, int fUseBackward, clock_t nTimeNewOut )
 {
     sat_solver * pSat;
     void * pSatCnf = NULL;
     Inta_Man_t * pManInterA; 
 //    Intb_Man_t * pManInterB; 
     int * pGlobalVars;
-    int clk, status, RetValue;
+    int status, RetValue;
     int i, Var;
+    clock_t clk;
 //    assert( p->pInterNew == NULL );
 
     // derive the SAT solver
diff --git a/src/proof/int/intUtil.c b/src/proof/int/intUtil.c
index 8027bdef..b93a7453 100644
--- a/src/proof/int/intUtil.c
+++ b/src/proof/int/intUtil.c
@@ -49,7 +49,7 @@ int Inter_ManCheckInitialState( Aig_Man_t * p )
     Aig_Obj_t * pObj;
     sat_solver * pSat;
     int i, status;
-    int clk = clock();
+    clock_t clk = clock();
     pCnf = Cnf_Derive( p, Saig_ManRegNum(p) ); 
     pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 1 );
     if ( pSat == NULL )
@@ -87,7 +87,7 @@ int Inter_ManCheckAllStates( Aig_Man_t * p )
     Cnf_Dat_t * pCnf;
     sat_solver * pSat;
     int status;
-    int clk = clock();
+    clock_t clk = clock();
     pCnf = Cnf_Derive( p, Saig_ManRegNum(p) ); 
     pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
     Cnf_DataFree( pCnf );