Fixing time printouts in 'pdr'.

6 files changed, 21 insertions, 22 deletions

diff --git a/src/proof/pdr/pdrCore.c b/src/proof/pdr/pdrCore.c
index 3e006c4e..9cecbd78 100644
--- a/src/proof/pdr/pdrCore.c
+++ b/src/proof/pdr/pdrCore.c
@@ -130,7 +130,7 @@ int Pdr_ManPushClauses( Pdr_Man_t * p )
     Vec_Ptr_t * vArrayK, * vArrayK1;
     int i, j, k, m, RetValue = 0, RetValue2, kMax = Vec_PtrSize(p->vSolvers)-1;
     int Counter = 0;
-    int clk = clock();
+    clock_t clk = clock();
     Vec_VecForEachLevelStartStop( p->vClauses, vArrayK, k, 1, kMax )
     {
         Vec_PtrSort( vArrayK, (int (*)(void))Pdr_SetCompare );
@@ -294,7 +294,8 @@ int * Pdr_ManSortByPriority( Pdr_Man_t * p, Pdr_Set_t * pCube )
 int Pdr_ManGeneralize( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppPred, Pdr_Set_t ** ppCubeMin )
 {
     Pdr_Set_t * pCubeMin, * pCubeTmp = NULL;
-    int i, j, n, Lit, RetValue,  clk = clock();
+    int i, j, n, Lit, RetValue;
+    clock_t clk = clock();
     int * pOrder;
     // if there is no induction, return
     *ppCubeMin = NULL;
@@ -549,8 +550,7 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
     int fPrintClauses = 0;
     Pdr_Set_t * pCube;
     int k, RetValue = -1;
-//    int clkTotal = clock();
-    int clkStart = clock();
+    clock_t clkStart = clock();
     p->timeToStop = p->pPars->nTimeOut ? time(NULL) + p->pPars->nTimeOut : 0;
     assert( Vec_PtrSize(p->vSolvers) == 0 );
     // create the first timeframe
@@ -673,13 +673,12 @@ int Pdr_ManSolve_( Aig_Man_t * pAig, Pdr_Par_t * pPars, Vec_Int_t ** pvPrioInit,
 {
     Pdr_Man_t * p;
     int RetValue;
-    int clk = clock();
+    clock_t clk = clock();
     p = Pdr_ManStart( pAig, pPars, pvPrioInit? *pvPrioInit : NULL );
     RetValue = Pdr_ManSolveInt( p );
     *ppCex = RetValue ? NULL : Pdr_ManDeriveCex( p );
     if ( p->pPars->fDumpInv )
         Pdr_ManDumpClauses( p, (char *)"inv.pla", RetValue==1 );
-
 //    if ( *ppCex && pPars->fVerbose )
 //        Abc_Print( 1, "Found counter-example in frame %d after exploring %d frames.\n", 
 //            (*ppCex)->iFrame, p->nFrames );
diff --git a/src/proof/pdr/pdrInt.h b/src/proof/pdr/pdrInt.h
index 075484bf..fda287eb 100644
--- a/src/proof/pdr/pdrInt.h
+++ b/src/proof/pdr/pdrInt.h
@@ -111,18 +111,17 @@ struct Pdr_Man_t_
     int         nQueMax;
     int         nQueLim;
     // runtime
-    ABC_INT64_T timeStart;
-    ABC_INT64_T timeToStop;
+    time_t      timeToStop;
     // time stats
-    ABC_INT64_T tSat;
-    ABC_INT64_T tSatSat;
-    ABC_INT64_T tSatUnsat;
-    ABC_INT64_T tGeneral;
-    ABC_INT64_T tPush;
-    ABC_INT64_T tTsim;
-    ABC_INT64_T tContain;
-    ABC_INT64_T tCnf;
-    ABC_INT64_T tTotal;
+    clock_t     tSat;
+    clock_t     tSatSat;
+    clock_t     tSatUnsat;
+    clock_t     tGeneral;
+    clock_t     tPush;
+    clock_t     tTsim;
+    clock_t     tContain;
+    clock_t     tCnf;
+    clock_t     tTotal;
 };
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/proof/pdr/pdrInv.c b/src/proof/pdr/pdrInv.c
index de21bdeb..cd94e22e 100644
--- a/src/proof/pdr/pdrInv.c
+++ b/src/proof/pdr/pdrInv.c
@@ -320,7 +320,8 @@ void Pdr_ManVerifyInvariant( Pdr_Man_t * p )
     Vec_Int_t * vLits;
     Vec_Ptr_t * vCubes;
     Pdr_Set_t * pCube;
-    int i, kStart, kThis, RetValue, Counter = 0, clk = clock();
+    int i, kStart, kThis, RetValue, Counter = 0;
+    clock_t clk = clock();
     // collect cubes used in the inductive invariant
     kStart = Pdr_ManFindInvariantStart( p );
     vCubes = Pdr_ManCollectCubes( p, kStart );
diff --git a/src/proof/pdr/pdrMan.c b/src/proof/pdr/pdrMan.c
index 73c12a7d..d3fcd112 100644
--- a/src/proof/pdr/pdrMan.c
+++ b/src/proof/pdr/pdrMan.c
@@ -72,7 +72,6 @@ Pdr_Man_t * Pdr_ManStart( Aig_Man_t * pAig, Pdr_Par_t * pPars, Vec_Int_t * vPrio
         Aig_ManFanoutStart( pAig );
     if ( pAig->pTerSimData == NULL )
         pAig->pTerSimData = ABC_CALLOC( unsigned, 1 + (Aig_ManObjNumMax(pAig) / 16) );
-    p->timeStart = clock();
     return p;
 }
 
diff --git a/src/proof/pdr/pdrSat.c b/src/proof/pdr/pdrSat.c
index de661905..50402ee5 100644
--- a/src/proof/pdr/pdrSat.c
+++ b/src/proof/pdr/pdrSat.c
@@ -140,7 +140,7 @@ Vec_Int_t * Pdr_ManCubeToLits( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, int fCom
 {
     Aig_Obj_t * pObj;
     int i, iVar, iVarMax = 0;
-    int clk = clock();
+    clock_t clk = clock();
     Vec_IntClear( p->vLits );
     for ( i = 0; i < pCube->nLits; i++ )
     {
@@ -272,7 +272,8 @@ int Pdr_ManCheckCube( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppPr
     int fLitUsed = 0;
     sat_solver * pSat;
     Vec_Int_t * vLits;
-    int Lit, RetValue, clk;
+    int Lit, RetValue;
+    clock_t clk;
     p->nCalls++;
     pSat = Pdr_ManFetchSolver( p, k );
     if ( pCube == NULL ) // solve the property
diff --git a/src/proof/pdr/pdrTsim.c b/src/proof/pdr/pdrTsim.c
index cf4756d1..59127461 100644
--- a/src/proof/pdr/pdrTsim.c
+++ b/src/proof/pdr/pdrTsim.c
@@ -363,7 +363,7 @@ Pdr_Set_t * Pdr_ManTernarySim( Pdr_Man_t * p, int k, Pdr_Set_t * pCube )
     Vec_Int_t * vRes    = p->vRes;     // final result (flop literals)
     Aig_Obj_t * pObj;
     int i, Entry, RetValue;
-    int clk = clock();
+    clock_t clk = clock();
 
     // collect CO objects
     Vec_IntClear( vCoObjs );