Adding a wrapper around clock() for more accurate time counting in ABC.

1 files changed, 13 insertions, 13 deletions

diff --git a/src/sat/bsat/satInterP.c b/src/sat/bsat/satInterP.c
index 404d5503..414879b6 100644
--- a/src/sat/bsat/satInterP.c
+++ b/src/sat/bsat/satInterP.c
@@ -69,9 +69,9 @@ struct Intp_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
 };
 
 // reading/writing the proof for a clause
@@ -419,17 +419,17 @@ Sto_Cls_t * Intp_ManPropagate( Intp_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 = Intp_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;
 }
 
@@ -475,7 +475,7 @@ int Intp_ManProofTraceOne( Intp_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 )
@@ -639,7 +639,7 @@ int Intp_ManProofTraceOne( Intp_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 )
@@ -864,7 +864,7 @@ void Intp_ManUnsatCoreVerify( Sto_Man_t * pCnf, Vec_Int_t * vCore )
     Sto_Cls_t * pClause;
     Vec_Ptr_t * vClauses;
     int i, iClause, RetValue;
-    clock_t clk = clock();
+    abctime clk = Abc_Clock();
     // collect the clauses
     vClauses = Vec_PtrAlloc( 1000 );
     Sto_ManForEachClauseRoot( pCnf, pClause )
@@ -896,7 +896,7 @@ void Intp_ManUnsatCoreVerify( Sto_Man_t * pCnf, Vec_Int_t * vCore )
             printf( "UNSAT core verification FAILED.  " );
         else
             printf( "UNSAT core verification succeeded.  " );
-        ABC_PRT( "Time", clock() - clk );
+        ABC_PRT( "Time", Abc_Clock() - clk );
     }
     else
     {
@@ -962,7 +962,7 @@ void * Intp_ManUnsatCore( Intp_Man_t * p, Sto_Man_t * pCnf, int fVerbose )
     Vec_Int_t * vVisited;
     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 );
@@ -1021,12 +1021,12 @@ void * Intp_ManUnsatCore( Intp_Man_t * p, Sto_Man_t * pCnf, int fVerbose )
 
     if ( fVerbose )
     {
-        ABC_PRT( "Core", clock() - clkTotal );
+        ABC_PRT( "Core", 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;
     }
 
     // derive the UNSAT core