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

3 files changed, 33 insertions, 33 deletions

diff --git a/src/proof/ssc/sscCore.c b/src/proof/ssc/sscCore.c
index 411df1e5..4c3f98da 100644
--- a/src/proof/ssc/sscCore.c
+++ b/src/proof/ssc/sscCore.c
@@ -218,9 +218,9 @@ Gia_Man_t * Ssc_PerformSweeping( Gia_Man_t * pAig, Gia_Man_t * pCare, Ssc_Pars_t
     Ssc_Man_t * p;
     Gia_Man_t * pResult, * pTemp;
     Gia_Obj_t * pObj, * pRepr;
-    clock_t clk, clkTotal = clock();
+    abctime clk, clkTotal = Abc_Clock();
     int i, fCompl, nRefined, status;
-clk = clock();
+clk = Abc_Clock();
     assert( Gia_ManRegNum(pCare) == 0 );
     assert( Gia_ManCiNum(pAig) == Gia_ManCiNum(pCare) );
     assert( Gia_ManIsNormalized(pAig) );
@@ -250,7 +250,7 @@ clk = clock();
         if ( nRefined <= Gia_ManCandNum(pAig) / 100 )
             break;
     }
-p->timeSimInit += clock() - clk;
+p->timeSimInit += Abc_Clock() - clk;
 
     // prepare user's AIG
     Gia_ManFillValue(pAig);
@@ -267,7 +267,7 @@ p->timeSimInit += clock() - clk;
     {
         if ( pAig->iPatsPi == 64 * pPars->nWords )
         {
-clk = clock();
+clk = Abc_Clock();
             Ssc_GiaSimRound( pAig );
             Ssc_GiaClassesRefine( pAig );
             if ( pPars->fVerbose ) 
@@ -277,7 +277,7 @@ clk = clock();
             // prepare next patterns
             Ssc_GiaResetPiPattern( pAig, pPars->nWords );
             Ssc_GiaSavePiPattern( pAig, p->vPivot );
-p->timeSimSat += clock() - clk;
+p->timeSimSat += Abc_Clock() - clk;
 //printf( "\n" );
         }
         if ( Gia_ObjIsAnd(pObj) )
@@ -294,7 +294,7 @@ p->timeSimSat += clock() - clk;
         fCompl = pRepr->fPhase ^ pObj->fPhase ^ Abc_LitIsCompl(pRepr->Value) ^ Abc_LitIsCompl(pObj->Value);
 
         // perform SAT call
-clk = clock();
+clk = Abc_Clock();
         p->nSatCalls++;
         status = Ssc_ManCheckEquivalence( p, Abc_Lit2Var(pRepr->Value), Abc_Lit2Var(pObj->Value), fCompl );
         if ( status == l_False )
@@ -317,11 +317,11 @@ clk = clock();
         else if ( status == l_Undef )
             p->nSatCallsUndec++;
         else assert( 0 );
-p->timeSat += clock() - clk;
+p->timeSat += Abc_Clock() - clk;
     }
     if ( pAig->iPatsPi > 1 )
     {
-clk = clock();
+clk = Abc_Clock();
         while ( pAig->iPatsPi < 64 * pPars->nWords )
             Ssc_GiaSavePiPattern( pAig, p->vPivot );
         Ssc_GiaSimRound( pAig );
@@ -330,7 +330,7 @@ clk = clock();
             Gia_ManEquivPrintClasses( pAig, 0, 0 );
         Ssc_GiaClassesCheckPairs( pAig, p->vDisPairs );
         Vec_IntClear( p->vDisPairs );
-p->timeSimSat += clock() - clk;
+p->timeSimSat += Abc_Clock() - clk;
     }
 //    Gia_ManEquivPrintClasses( pAig, 1, 0 );
 //    Gia_ManPrint( pAig );
@@ -346,7 +346,7 @@ p->timeSimSat += clock() - clk;
     }
     pResult = Gia_ManCleanup( pTemp = pResult );
     Gia_ManStop( pTemp );
-    p->timeTotal = clock() - clkTotal;
+    p->timeTotal = Abc_Clock() - clkTotal;
     if ( pPars->fVerbose )
         Ssc_ManPrintStats( p );
     Ssc_ManStop( p );
@@ -356,7 +356,7 @@ p->timeSimSat += clock() - clk;
         Abc_Print( 1, "Reduction in AIG nodes:%8d  ->%8d (%6.2f %%).  ", 
             Gia_ManAndNum(pAig), Gia_ManAndNum(pResult), 
             100.0 - 100.0 * Gia_ManAndNum(pResult) / Gia_ManAndNum(pAig) );
-        Abc_PrintTime( 1, "Time", clock() - clkTotal );
+        Abc_PrintTime( 1, "Time", Abc_Clock() - clkTotal );
     }
     return pResult;
 }
diff --git a/src/proof/ssc/sscInt.h b/src/proof/ssc/sscInt.h
index 0be25174..4e785bce 100644
--- a/src/proof/ssc/sscInt.h
+++ b/src/proof/ssc/sscInt.h
@@ -72,15 +72,15 @@ struct Ssc_Man_t_
     int              nSatCallsSat;   // the number of sat SAT calls
     int              nSatCallsUndec; // the number of undec SAT calls
     // runtime stats
-    clock_t          timeSimInit;    // simulation and class computation
-    clock_t          timeSimSat;     // simulation of the counter-examples
-    clock_t          timeCnfGen;     // generation of CNF
-    clock_t          timeSat;        // total SAT time
-    clock_t          timeSatSat;     // sat
-    clock_t          timeSatUnsat;   // unsat
-    clock_t          timeSatUndec;   // undecided
-    clock_t          timeOther;      // other runtime
-    clock_t          timeTotal;      // total runtime
+    abctime          timeSimInit;    // simulation and class computation
+    abctime          timeSimSat;     // simulation of the counter-examples
+    abctime          timeCnfGen;     // generation of CNF
+    abctime          timeSat;        // total SAT time
+    abctime          timeSatSat;     // sat
+    abctime          timeSatUnsat;   // unsat
+    abctime          timeSatUndec;   // undecided
+    abctime          timeOther;      // other runtime
+    abctime          timeTotal;      // total runtime
 };
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/proof/ssc/sscSat.c b/src/proof/ssc/sscSat.c
index 1de99c2e..9992f18e 100644
--- a/src/proof/ssc/sscSat.c
+++ b/src/proof/ssc/sscSat.c
@@ -209,12 +209,12 @@ static void Ssc_ManCnfNodeAddToSolver( Ssc_Man_t * p, int NodeId )
 {
     Gia_Obj_t * pNode;
     int i, k, Id, Lit;
-    clock_t clk;
+    abctime clk;
     assert( NodeId > 0 );
     // quit if CNF is ready
     if ( Ssc_ObjSatVar(p, NodeId) )
         return;
-clk = clock();
+clk = Abc_Clock();
     // start the frontier
     Vec_IntClear( p->vFront );
     Ssc_ManCnfAddToFrontier( p, NodeId, p->vFront );
@@ -243,7 +243,7 @@ clk = clock();
         }
         assert( Vec_IntSize(p->vFanins) > 1 );
     }
-p->timeCnfGen += clock() - clk;
+p->timeCnfGen += Abc_Clock() - clk;
 }
 
 
@@ -346,10 +346,10 @@ Vec_Int_t * Ssc_ManFindPivotSat( Ssc_Man_t * p )
 int Ssc_ManCheckEquivalence( Ssc_Man_t * p, int iRepr, int iNode, int fCompl )
 {
     int pLitsSat[2], RetValue;
-    clock_t clk;
+    abctime clk;
     assert( iRepr < iNode );
 //    if ( p->nTimeOut )
-//        sat_solver_set_runtime_limit( p->pSat, p->nTimeOut * CLOCKS_PER_SEC + clock() );
+//        sat_solver_set_runtime_limit( p->pSat, p->nTimeOut * CLOCKS_PER_SEC + Abc_Clock() );
 
     // create CNF
     if ( iRepr )
@@ -363,7 +363,7 @@ int Ssc_ManCheckEquivalence( Ssc_Man_t * p, int iRepr, int iNode, int fCompl )
 
     // solve under assumptions
     // A = 1; B = 0
-    clk = clock();
+    clk = Abc_Clock();
     RetValue = sat_solver_solve( p->pSat, pLitsSat, pLitsSat + 2, (ABC_INT64_T)p->pPars->nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
     if ( RetValue == l_False )
     {
@@ -371,17 +371,17 @@ int Ssc_ManCheckEquivalence( Ssc_Man_t * p, int iRepr, int iNode, int fCompl )
         pLitsSat[1] = Abc_LitNot( pLitsSat[1] ); // compl
         RetValue = sat_solver_addclause( p->pSat, pLitsSat, pLitsSat + 2 );
         assert( RetValue );
-        p->timeSatUnsat += clock() - clk;
+        p->timeSatUnsat += Abc_Clock() - clk;
     }
     else if ( RetValue == l_True )
     {
         Ssc_ManCollectSatPattern( p, p->vPattern );
-        p->timeSatSat += clock() - clk;
+        p->timeSatSat += Abc_Clock() - clk;
         return l_True;
     }
     else // if ( RetValue1 == l_Undef )
     {
-        p->timeSatUndec += clock() - clk;
+        p->timeSatUndec += Abc_Clock() - clk;
         return l_Undef;
     }
 
@@ -391,7 +391,7 @@ int Ssc_ManCheckEquivalence( Ssc_Man_t * p, int iRepr, int iNode, int fCompl )
 
     // solve under assumptions
     // A = 0; B = 1
-    clk = clock();
+    clk = Abc_Clock();
     RetValue = sat_solver_solve( p->pSat, pLitsSat, pLitsSat + 2, (ABC_INT64_T)p->pPars->nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
     if ( RetValue == l_False )
     {
@@ -399,17 +399,17 @@ int Ssc_ManCheckEquivalence( Ssc_Man_t * p, int iRepr, int iNode, int fCompl )
         pLitsSat[1] = Abc_LitNot( pLitsSat[1] );
         RetValue = sat_solver_addclause( p->pSat, pLitsSat, pLitsSat + 2 );
         assert( RetValue );
-        p->timeSatUnsat += clock() - clk;
+        p->timeSatUnsat += Abc_Clock() - clk;
     }
     else if ( RetValue == l_True )
     {
         Ssc_ManCollectSatPattern( p, p->vPattern );
-        p->timeSatSat += clock() - clk;
+        p->timeSatSat += Abc_Clock() - clk;
         return l_True;
     }
     else // if ( RetValue1 == l_Undef )
     {
-        p->timeSatUndec += clock() - clk;
+        p->timeSatUndec += Abc_Clock() - clk;
         return l_Undef;
     }
     return l_False;