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/sat/bsat/satInterA.c | |
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/sat/bsat/satInterA.c')
-rw-r--r-- | src/sat/bsat/satInterA.c | 22 |
1 files changed, 11 insertions, 11 deletions
diff --git a/src/sat/bsat/satInterA.c b/src/sat/bsat/satInterA.c index a4a06439..dabb10a3 100644 --- a/src/sat/bsat/satInterA.c +++ b/src/sat/bsat/satInterA.c @@ -70,9 +70,9 @@ struct Inta_Man_t_ int nResLits; // the number of literals of the resolvent int nResLitsAlloc;// the number of literals of the resolvent // runtime stats - clock_t timeBcp; // the runtime for BCP - clock_t timeTrace; // the runtime of trace construction - clock_t timeTotal; // the total runtime of interpolation + abctime timeBcp; // the runtime for BCP + abctime timeTrace; // the runtime of trace construction + abctime timeTotal; // the total runtime of interpolation }; // procedure to get hold of the clauses' truth table @@ -491,17 +491,17 @@ Sto_Cls_t * Inta_ManPropagate( Inta_Man_t * p, int Start ) { Sto_Cls_t * pClause; int i; - clock_t clk = clock(); + abctime clk = Abc_Clock(); for ( i = Start; i < p->nTrailSize; i++ ) { pClause = Inta_ManPropagateOne( p, p->pTrail[i] ); if ( pClause ) { -p->timeBcp += clock() - clk; +p->timeBcp += Abc_Clock() - clk; return pClause; } } -p->timeBcp += clock() - clk; +p->timeBcp += Abc_Clock() - clk; return NULL; } @@ -547,7 +547,7 @@ int Inta_ManProofTraceOne( Inta_Man_t * p, Sto_Cls_t * pConflict, Sto_Cls_t * pF Sto_Cls_t * pReason; int i, v, Var, PrevId; int fPrint = 0; - clock_t clk = clock(); + abctime clk = Abc_Clock(); // collect resolvent literals if ( p->fProofVerif ) @@ -697,7 +697,7 @@ int Inta_ManProofTraceOne( Inta_Man_t * p, Sto_Cls_t * pConflict, Sto_Cls_t * pF assert( p->nResLits == (int)pFinal->nLits ); } } -p->timeTrace += clock() - clk; +p->timeTrace += Abc_Clock() - clk; // return the proof pointer if ( p->pCnf->nClausesA ) @@ -954,7 +954,7 @@ void * Inta_ManInterpolate( Inta_Man_t * p, Sto_Man_t * pCnf, void * vVarsAB, in Aig_Obj_t * pObj; Sto_Cls_t * pClause; int RetValue = 1; - clock_t clkTotal = clock(); + abctime clkTotal = Abc_Clock(); // check that the CNF makes sense assert( pCnf->nVars > 0 && pCnf->nClauses > 0 ); @@ -1008,12 +1008,12 @@ void * Inta_ManInterpolate( Inta_Man_t * p, Sto_Man_t * pCnf, void * vVarsAB, in if ( fVerbose ) { -// ABC_PRT( "Interpo", clock() - clkTotal ); +// ABC_PRT( "Interpo", Abc_Clock() - clkTotal ); printf( "Vars = %d. Roots = %d. Learned = %d. Resol steps = %d. Ave = %.2f. Mem = %.2f MB\n", p->pCnf->nVars, p->pCnf->nRoots, p->pCnf->nClauses-p->pCnf->nRoots, p->Counter, 1.0*(p->Counter-p->pCnf->nRoots)/(p->pCnf->nClauses-p->pCnf->nRoots), 1.0*Sto_ManMemoryReport(p->pCnf)/(1<<20) ); -p->timeTotal += clock() - clkTotal; +p->timeTotal += Abc_Clock() - clkTotal; } pObj = *Inta_ManAigRead( p, p->pCnf->pTail ); |