diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2013-05-27 15:09:23 -0700 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2013-05-27 15:09:23 -0700 |
commit | 19c25fd6aab057b2373717f996fe538507c1b1e1 (patch) | |
tree | 7aa7cd7609a5de31d11b3455b6388fd9300c8d0f /src/proof/pdr/pdrInt.h | |
parent | 94356f0d1fa8e671303299717f631ecf0ca2f17e (diff) | |
download | abc-19c25fd6aab057b2373717f996fe538507c1b1e1.tar.gz abc-19c25fd6aab057b2373717f996fe538507c1b1e1.tar.bz2 abc-19c25fd6aab057b2373717f996fe538507c1b1e1.zip |
Adding a wrapper around clock() for more accurate time counting in ABC.
Diffstat (limited to 'src/proof/pdr/pdrInt.h')
-rw-r--r-- | src/proof/pdr/pdrInt.h | 28 |
1 files changed, 14 insertions, 14 deletions
diff --git a/src/proof/pdr/pdrInt.h b/src/proof/pdr/pdrInt.h index 3f74dd5f..72393077 100644 --- a/src/proof/pdr/pdrInt.h +++ b/src/proof/pdr/pdrInt.h @@ -97,7 +97,7 @@ struct Pdr_Man_t_ Vec_Int_t * vRes; // final result Vec_Int_t * vSuppLits; // support literals Pdr_Set_t * pCubeJust; // justification - clock_t * pTime4Outs;// timeout per output + abctime * pTime4Outs;// timeout per output // statistics int nBlocks; // the number of times blockState was called int nObligs; // the number of proof obligations derived @@ -115,18 +115,18 @@ struct Pdr_Man_t_ int nQueMax; int nQueLim; // runtime - time_t timeToStop; - time_t timeToStopOne; + abctime timeToStop; + abctime timeToStopOne; // time stats - 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; + abctime tSat; + abctime tSatSat; + abctime tSatUnsat; + abctime tGeneral; + abctime tPush; + abctime tTsim; + abctime tContain; + abctime tCnf; + abctime tTotal; }; //////////////////////////////////////////////////////////////////////// @@ -135,7 +135,7 @@ struct Pdr_Man_t_ static inline sat_solver * Pdr_ManSolver( Pdr_Man_t * p, int k ) { return (sat_solver *)Vec_PtrEntry(p->vSolvers, k); } -static inline clock_t Pdr_ManTimeLimit( Pdr_Man_t * p ) +static inline abctime Pdr_ManTimeLimit( Pdr_Man_t * p ) { if ( p->timeToStop == 0 ) return p->timeToStopOne; @@ -160,7 +160,7 @@ extern sat_solver * Pdr_ManNewSolver( sat_solver * pSat, Pdr_Man_t * p, int k /*=== pdrCore.c ==========================================================*/ extern int Pdr_ManCheckContainment( Pdr_Man_t * p, int k, Pdr_Set_t * pSet ); /*=== pdrInv.c ==========================================================*/ -extern void Pdr_ManPrintProgress( Pdr_Man_t * p, int fClose, clock_t Time ); +extern void Pdr_ManPrintProgress( Pdr_Man_t * p, int fClose, abctime Time ); extern void Pdr_ManPrintClauses( Pdr_Man_t * p, int kStart ); extern void Pdr_ManDumpClauses( Pdr_Man_t * p, char * pFileName, int fProved ); extern void Pdr_ManReportInvariant( Pdr_Man_t * p ); |