diff options
| -rw-r--r-- | src/proof/pdr/pdrCore.c | 11 | ||||
| -rw-r--r-- | src/proof/pdr/pdrInt.h | 21 | ||||
| -rw-r--r-- | src/proof/pdr/pdrInv.c | 3 | ||||
| -rw-r--r-- | src/proof/pdr/pdrMan.c | 1 | ||||
| -rw-r--r-- | src/proof/pdr/pdrSat.c | 5 | ||||
| -rw-r--r-- | src/proof/pdr/pdrTsim.c | 2 |
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 ); |