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/bbr | |
| 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/bbr')
| -rw-r--r-- | src/proof/bbr/bbrCex.c | 4 | ||||
| -rw-r--r-- | src/proof/bbr/bbrReach.c | 10 |
2 files changed, 7 insertions, 7 deletions
diff --git a/src/proof/bbr/bbrCex.c b/src/proof/bbr/bbrCex.c index 60fef07c..31a46d61 100644 --- a/src/proof/bbr/bbrCex.c +++ b/src/proof/bbr/bbrCex.c @@ -55,7 +55,7 @@ Abc_Cex_t * Aig_ManVerifyUsingBddsCountExample( Aig_Man_t * p, DdManager * dd, DdNode * bTemp, * bVar, * bRing; int i, v, RetValue, nPiOffset; char * pValues; - clock_t clk = clock(); + abctime clk = Abc_Clock(); //printf( "\nDeriving counter-example.\n" ); // allocate room for the counter-example @@ -158,7 +158,7 @@ Abc_Cex_t * Aig_ManVerifyUsingBddsCountExample( Aig_Man_t * p, DdManager * dd, } if ( fVerbose && !fSilent ) { - ABC_PRT( "Counter-example generation time", clock() - clk ); + ABC_PRT( "Counter-example generation time", Abc_Clock() - clk ); } return pCex; } diff --git a/src/proof/bbr/bbrReach.c b/src/proof/bbr/bbrReach.c index 0becaa39..b5125ec7 100644 --- a/src/proof/bbr/bbrReach.c +++ b/src/proof/bbr/bbrReach.c @@ -247,7 +247,7 @@ int Aig_ManComputeReachable( DdManager * dd, Aig_Man_t * p, DdNode ** pbParts, D Cudd_ReorderingType method; int i, nIters, nBddSize = 0, status; int nThreshold = 10000; - clock_t clk = clock(); + abctime clk = Abc_Clock(); Vec_Ptr_t * vOnionRings; int fixedPoint = 0; @@ -282,7 +282,7 @@ int Aig_ManComputeReachable( DdManager * dd, Aig_Man_t * p, DdNode ** pbParts, D for ( nIters = 0; nIters < pPars->nIterMax; nIters++ ) { // check the runtime limit - if ( pPars->TimeLimit && pPars->TimeLimit <= (clock()-clk)/CLOCKS_PER_SEC ) + if ( pPars->TimeLimit && pPars->TimeLimit <= (Abc_Clock()-clk)/CLOCKS_PER_SEC ) { printf( "Reached timeout after image computation (%d seconds).\n", pPars->TimeLimit ); Vec_PtrFree( vOnionRings ); @@ -442,7 +442,7 @@ int Aig_ManVerifyUsingBdds_int( Aig_Man_t * p, Saig_ParBbr_t * pPars ) DdNode ** pbParts, ** pbOutputs; DdNode * bInitial, * bTemp; int RetValue, i; - clock_t clk = clock(); + abctime clk = Abc_Clock(); Vec_Ptr_t * vOnionRings; assert( Saig_ManRegNum(p) > 0 ); @@ -459,7 +459,7 @@ int Aig_ManVerifyUsingBdds_int( Aig_Man_t * p, Saig_ParBbr_t * pPars ) printf( "Shared BDD size is %6d nodes.\n", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) ); // check the runtime limit - if ( pPars->TimeLimit && pPars->TimeLimit <= (clock()-clk)/CLOCKS_PER_SEC ) + if ( pPars->TimeLimit && pPars->TimeLimit <= (Abc_Clock()-clk)/CLOCKS_PER_SEC ) { printf( "Reached timeout after constructing global BDDs (%d seconds).\n", pPars->TimeLimit ); Cudd_Quit( dd ); @@ -524,7 +524,7 @@ int Aig_ManVerifyUsingBdds_int( Aig_Man_t * p, Saig_ParBbr_t * pPars ) // report the runtime if ( !pPars->fSilent ) { - ABC_PRT( "Time", clock() - clk ); + ABC_PRT( "Time", Abc_Clock() - clk ); fflush( stdout ); } return RetValue; |