diff options
Diffstat (limited to 'src/proof/int')
| -rw-r--r-- | src/proof/int/intCheck.c | 2 | ||||
| -rw-r--r-- | src/proof/int/intCore.c | 9 | ||||
| -rw-r--r-- | src/proof/int/intCtrex.c | 3 | ||||
| -rw-r--r-- | src/proof/int/intInt.h | 18 | ||||
| -rw-r--r-- | src/proof/int/intM114.c | 5 | ||||
| -rw-r--r-- | src/proof/int/intUtil.c | 4 |
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 ); |