From 19c25fd6aab057b2373717f996fe538507c1b1e1 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Mon, 27 May 2013 15:09:23 -0700 Subject: Adding a wrapper around clock() for more accurate time counting in ABC. --- src/proof/bbr/bbrCex.c | 4 ++-- src/proof/bbr/bbrReach.c | 10 +++++----- 2 files changed, 7 insertions(+), 7 deletions(-) (limited to 'src/proof/bbr') 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; -- cgit v1.2.3