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

6 files changed, 61 insertions, 61 deletions

diff --git a/src/proof/int/intCheck.c b/src/proof/int/intCheck.c
index 28ef54a7..4e58440b 100644
--- a/src/proof/int/intCheck.c
+++ b/src/proof/int/intCheck.c
@@ -217,7 +217,7 @@ void Inter_CheckAddEqual( Inter_Check_t * p, int iVarA, int iVarB )
   SeeAlso     []
 
 ***********************************************************************/
-int Inter_CheckPerform( Inter_Check_t * p, Cnf_Dat_t * pCnfInt, clock_t nTimeNewOut )
+int Inter_CheckPerform( Inter_Check_t * p, Cnf_Dat_t * pCnfInt, abctime nTimeNewOut )
 {
     Aig_Obj_t * pObj, * pObj2;
     int i, f, VarA, VarB, RetValue, Entry, status;
diff --git a/src/proof/int/intCore.c b/src/proof/int/intCore.c
index cfab05dc..dedf987e 100644
--- a/src/proof/int/intCore.c
+++ b/src/proof/int/intCore.c
@@ -83,8 +83,8 @@ int Inter_ManPerformInterpolation( Aig_Man_t * pAig, Inter_ManParams_t * pPars,
     Inter_Check_t * pCheck = NULL;
     Aig_Man_t * pAigTemp;
     int s, i, RetValue, Status;
-    clock_t clk, clk2, clkTotal = clock(), timeTemp = 0;
-    clock_t nTimeNewOut = pPars->nSecLimit ? pPars->nSecLimit * CLOCKS_PER_SEC + clock() : 0;
+    abctime clk, clk2, clkTotal = Abc_Clock(), timeTemp = 0;
+    abctime nTimeNewOut = pPars->nSecLimit ? pPars->nSecLimit * CLOCKS_PER_SEC + Abc_Clock() : 0;
 
     // enable ORing of the interpolants, if containment check is performed inductively with K > 1
     if ( pPars->nFramesK > 1 )
@@ -118,9 +118,9 @@ int Inter_ManPerformInterpolation( Aig_Man_t * pAig, Inter_ManParams_t * pPars,
     else
         p->pAigTrans = Inter_ManStartDuplicated( pAig );
     // derive CNF for the transformed AIG
-clk = clock();
+clk = Abc_Clock();
     p->pCnfAig = Cnf_Derive( p->pAigTrans, Aig_ManRegNum(p->pAigTrans) ); 
-p->timeCnf += clock() - clk;    
+p->timeCnf += Abc_Clock() - clk;    
     if ( pPars->fVerbose )
     { 
         printf( "AIG: PI/PO/Reg = %d/%d/%d. And = %d. Lev = %d.  CNF: Var/Cla = %d/%d.\n",
@@ -136,19 +136,19 @@ p->timeCnf += clock() - clk;
     {
         Cnf_Dat_t * pCnfInter2;
 
-clk2 = clock();
+clk2 = Abc_Clock();
         // initial state
         if ( pPars->fUseBackward )
             p->pInter = Inter_ManStartOneOutput( pAig, 1 );
         else
             p->pInter = Inter_ManStartInitState( Aig_ManRegNum(pAig) );
         assert( Aig_ManCoNum(p->pInter) == 1 );
-clk = clock();
+clk = Abc_Clock();
         p->pCnfInter = Cnf_Derive( p->pInter, 0 );  
-p->timeCnf += clock() - clk;    
+p->timeCnf += Abc_Clock() - clk;    
         // timeframes
         p->pFrames = Inter_ManFramesInter( pAig, p->nFrames, pPars->fUseBackward, pPars->fUseTwoFrames );
-clk = clock();
+clk = Abc_Clock();
         if ( pPars->fRewrite )
         {
             p->pFrames = Dar_ManRwsat( pAigTemp = p->pFrames, 1, 0 );
@@ -156,21 +156,21 @@ clk = clock();
 //        p->pFrames = Fra_FraigEquivence( pAigTemp = p->pFrames, 100, 0 );
 //        Aig_ManStop( pAigTemp );
         }
-p->timeRwr += clock() - clk;
+p->timeRwr += Abc_Clock() - clk;
         // can also do SAT sweeping on the timeframes...
-clk = clock();
+clk = Abc_Clock();
         if ( pPars->fUseBackward )
             p->pCnfFrames = Cnf_Derive( p->pFrames, Aig_ManCoNum(p->pFrames) );  
         else
 //            p->pCnfFrames = Cnf_Derive( p->pFrames, 0 );  
             p->pCnfFrames = Cnf_DeriveSimple( p->pFrames, 0 );  
-p->timeCnf += clock() - clk;    
+p->timeCnf += Abc_Clock() - clk;    
         // report statistics
         if ( pPars->fVerbose )
         {
             printf( "Step = %2d. Frames = 1 + %d. And = %5d. Lev = %5d.  ", 
                 s+1, p->nFrames, Aig_ManNodeNum(p->pFrames), Aig_ManLevelNum(p->pFrames) );
-            ABC_PRT( "Time", clock() - clk2 );
+            ABC_PRT( "Time", Abc_Clock() - clk2 );
         }
 
 
@@ -180,12 +180,12 @@ p->timeCnf += clock() - clk;
         {
             pCheck = Inter_CheckStart( p->pAigTrans, pPars->nFramesK );
             // try new containment check for the initial state
-clk = clock();
+clk = Abc_Clock();
             pCnfInter2 = Cnf_Derive( p->pInter, 1 );  
-p->timeCnf += clock() - clk;    
-clk = clock();
+p->timeCnf += Abc_Clock() - clk;    
+clk = Abc_Clock();
             RetValue = Inter_CheckPerform( pCheck, pCnfInter2, nTimeNewOut );
-p->timeEqu += clock() - clk;
+p->timeEqu += Abc_Clock() - clk;
 //            assert( RetValue == 0 );
             Cnf_DataFree( pCnfInter2 );
             if ( p->vInters )
@@ -200,14 +200,14 @@ p->timeEqu += clock() - clk;
             { 
                 if ( pPars->fVerbose )
                     printf( "Reached limit (%d) on the number of timeframes.\n", pPars->nFramesMax );
-                p->timeTotal = clock() - clkTotal;
+                p->timeTotal = Abc_Clock() - clkTotal;
                 Inter_ManStop( p, 0 );
                 Inter_CheckStop( pCheck );
                 return -1;
             }
 
             // perform interpolation
-            clk = clock();
+            clk = Abc_Clock();
 #ifdef ABC_USE_LIBRARIES
             if ( pPars->fUseMiniSat )
             {
@@ -222,7 +222,7 @@ p->timeEqu += clock() - clk;
             {
                 printf( "   I = %2d. Bmc =%3d. IntAnd =%6d. IntLev =%5d. Conf =%6d.  ", 
                     i+1, i + 1 + p->nFrames, Aig_ManNodeNum(p->pInter), Aig_ManLevelNum(p->pInter), p->nConfCur );
-                ABC_PRT( "Time", clock() - clk );
+                ABC_PRT( "Time", Abc_Clock() - clk );
             }
             // remember the number of timeframes completed
             pPars->iFrameMax = i - 1 + p->nFrames;
@@ -232,7 +232,7 @@ p->timeEqu += clock() - clk;
                 {
                     if ( pPars->fVerbose )
                         printf( "Found a real counterexample in frame %d.\n", p->nFrames );
-                    p->timeTotal = clock() - clkTotal;
+                    p->timeTotal = Abc_Clock() - clkTotal;
                     *piFrame = p->nFrames;
 //                    pAig->pSeqModel = (Abc_Cex_t *)Inter_ManGetCounterExample( pAig, p->nFrames+1, pPars->fVerbose );
                     {
@@ -259,7 +259,7 @@ p->timeEqu += clock() - clk;
             }
             else if ( RetValue == -1 ) 
             {
-                if ( pPars->nSecLimit && clock() > nTimeNewOut ) // timed out
+                if ( pPars->nSecLimit && Abc_Clock() > nTimeNewOut ) // timed out
                 {
                     if ( pPars->fVerbose )
                         printf( "Reached timeout (%d seconds).\n",  pPars->nSecLimit );
@@ -270,14 +270,14 @@ p->timeEqu += clock() - clk;
                     if ( pPars->fVerbose )
                         printf( "Reached limit (%d) on the number of conflicts.\n", p->nConfLimit );
                 }
-                p->timeTotal = clock() - clkTotal;
+                p->timeTotal = Abc_Clock() - clkTotal;
                 Inter_ManStop( p, 0 );
                 Inter_CheckStop( pCheck );
                 return -1;
             }
             assert( RetValue == 1 ); // found new interpolant
             // compress the interpolant
-clk = clock();
+clk = Abc_Clock();
             if ( p->pInterNew )
             {
 //                Ioa_WriteAiger( p->pInterNew, "interpol.aig", 0, 0 );
@@ -285,7 +285,7 @@ clk = clock();
 //                p->pInterNew = Dar_ManRwsat( pAigTemp = p->pInterNew, 0, 0 );
                 Aig_ManStop( pAigTemp );
             }
-p->timeRwr += clock() - clk;
+p->timeRwr += Abc_Clock() - clk;
 
             // check if interpolant is trivial
             if ( p->pInterNew == NULL || Aig_ObjChild0(Aig_ManCo(p->pInterNew,0)) == Aig_ManConst0(p->pInterNew) )
@@ -293,30 +293,30 @@ p->timeRwr += clock() - clk;
 //                printf( "interpolant is constant 0\n" );
                 if ( pPars->fVerbose )
                     printf( "The problem is trivially true for all states.\n" );
-                p->timeTotal = clock() - clkTotal;
+                p->timeTotal = Abc_Clock() - clkTotal;
                 Inter_ManStop( p, 1 );
                 Inter_CheckStop( pCheck );
                 return 1;
             }
 
             // check containment of interpolants
-clk = clock();
+clk = Abc_Clock();
             if ( pPars->fCheckKstep ) // k-step unique-state induction
             {
                 if ( Aig_ManCiNum(p->pInterNew) == Aig_ManCiNum(p->pInter) )
                 {
                     if ( pPars->fTransLoop || pPars->fUseBackward || pPars->nFramesK > 1 )
                     {
-clk2 = clock();
+clk2 = Abc_Clock();
                         Status = Inter_ManCheckInductiveContainment( p->pAigTrans, p->pInterNew, Abc_MinInt(i + 1, pPars->nFramesK), pPars->fUseBackward );
-timeTemp = clock() - clk2;
+timeTemp = Abc_Clock() - clk2;
                     }
                     else
                     {   // new containment check
-clk2 = clock();
+clk2 = Abc_Clock();
                         pCnfInter2 = Cnf_Derive( p->pInterNew, 1 );  
-p->timeCnf += clock() - clk2;
-timeTemp = clock() - clk2;
+p->timeCnf += Abc_Clock() - clk2;
+timeTemp = Abc_Clock() - clk2;
             
                         Status = Inter_CheckPerform( pCheck, pCnfInter2, nTimeNewOut );
                         Cnf_DataFree( pCnfInter2 );
@@ -334,20 +334,20 @@ timeTemp = clock() - clk2;
                 else
                     Status = 0;
             }
-p->timeEqu += clock() - clk - timeTemp;
+p->timeEqu += Abc_Clock() - clk - timeTemp;
             if ( Status ) // contained
             {
                 if ( pPars->fVerbose )
                     printf( "Proved containment of interpolants.\n" );
-                p->timeTotal = clock() - clkTotal;
+                p->timeTotal = Abc_Clock() - clkTotal;
                 Inter_ManStop( p, 1 );
                 Inter_CheckStop( pCheck );
                 return 1;
             }
-            if ( pPars->nSecLimit && clock() > nTimeNewOut )
+            if ( pPars->nSecLimit && Abc_Clock() > nTimeNewOut )
             {
                 printf( "Reached timeout (%d seconds).\n",  pPars->nSecLimit );
-                p->timeTotal = clock() - clkTotal;
+                p->timeTotal = Abc_Clock() - clkTotal;
                 Inter_ManStop( p, 1 );
                 Inter_CheckStop( pCheck );
                 return -1;
@@ -366,10 +366,10 @@ p->timeEqu += clock() - clk - timeTemp;
                     Aig_ManStop( pAigTemp );
                     Aig_ManStop( p->pInterNew );
                     // compress the interpolant
-clk = clock();
+clk = Abc_Clock();
                     p->pInter = Dar_ManRwsat( pAigTemp = p->pInter, 1, 0 );
                     Aig_ManStop( pAigTemp );
-p->timeRwr += clock() - clk;
+p->timeRwr += Abc_Clock() - clk;
                 }
                 else // forward with the new containment checking (using only the frontier)
                 {
@@ -379,9 +379,9 @@ p->timeRwr += clock() - clk;
             }
             p->pInterNew = NULL;
             Cnf_DataFree( p->pCnfInter );
-clk = clock();
+clk = Abc_Clock();
             p->pCnfInter = Cnf_Derive( p->pInter, 0 );  
-p->timeCnf += clock() - clk;
+p->timeCnf += Abc_Clock() - clk;
         }
 
         // start containment checking
diff --git a/src/proof/int/intCtrex.c b/src/proof/int/intCtrex.c
index 9b2946e9..91740e6c 100644
--- a/src/proof/int/intCtrex.c
+++ b/src/proof/int/intCtrex.c
@@ -100,7 +100,7 @@ void * Inter_ManGetCounterExample( Aig_Man_t * pAig, int nFrames, int fVerbose )
     sat_solver * pSat;
     Cnf_Dat_t * pCnf;
     int status;
-    clock_t clk = clock();
+    abctime clk = Abc_Clock();
     Vec_Int_t * vCiIds;
     // create timeframes
     assert( Saig_ManPoNum(pAig) == 1 );
@@ -152,7 +152,7 @@ void * Inter_ManGetCounterExample( Aig_Man_t * pAig, int nFrames, int fVerbose )
     // report the results
     if ( fVerbose )
     {
-        ABC_PRT( "Total ctrex generation time", clock() - clk );
+        ABC_PRT( "Total ctrex generation time", Abc_Clock() - clk );
     }
     return pCtrex;
 
diff --git a/src/proof/int/intInt.h b/src/proof/int/intInt.h
index bf591b7a..37bcf51c 100644
--- a/src/proof/int/intInt.h
+++ b/src/proof/int/intInt.h
@@ -71,13 +71,13 @@ struct Inter_Man_t_
     int              fVerbose;     // the verbosiness flag
     char *           pFileName;
     // runtime
-    clock_t          timeRwr;
-    clock_t          timeCnf;
-    clock_t          timeSat;
-    clock_t          timeInt;
-    clock_t          timeEqu;
-    clock_t          timeOther;
-    clock_t          timeTotal;
+    abctime          timeRwr;
+    abctime          timeCnf;
+    abctime          timeSat;
+    abctime          timeInt;
+    abctime          timeEqu;
+    abctime          timeOther;
+    abctime          timeTotal;
 };
 
 // containment checking manager
@@ -94,7 +94,7 @@ typedef struct Inter_Check_t_ Inter_Check_t;
 /*=== intCheck.c ============================================================*/
 extern Inter_Check_t * Inter_CheckStart( Aig_Man_t * pTrans, int nFramesK );
 extern void            Inter_CheckStop( Inter_Check_t * p );
-extern int             Inter_CheckPerform( Inter_Check_t * p, Cnf_Dat_t * pCnf, clock_t nTimeNewOut );
+extern int             Inter_CheckPerform( Inter_Check_t * p, Cnf_Dat_t * pCnf, abctime nTimeNewOut );
 
 /*=== intContain.c ============================================================*/
 extern int             Inter_ManCheckContainment( Aig_Man_t * pNew, Aig_Man_t * pOld );
@@ -118,7 +118,7 @@ extern void            Inter_ManClean( Inter_Man_t * p );
 extern void            Inter_ManStop( Inter_Man_t * p, int fProved );
 
 /*=== intM114.c ============================================================*/
-extern int             Inter_ManPerformOneStep( Inter_Man_t * p, int fUseBias, int fUseBackward, clock_t nTimeNewOut );
+extern int             Inter_ManPerformOneStep( Inter_Man_t * p, int fUseBias, int fUseBackward, abctime nTimeNewOut );
 
 /*=== intM114p.c ============================================================*/
 #ifdef ABC_USE_LIBRARIES
diff --git a/src/proof/int/intM114.c b/src/proof/int/intM114.c
index bf44696d..64b18ae0 100644
--- a/src/proof/int/intM114.c
+++ b/src/proof/int/intM114.c
@@ -200,7 +200,7 @@ sat_solver * Inter_ManDeriveSatSolver(
   SeeAlso     []
 
 ***********************************************************************/
-int Inter_ManPerformOneStep( Inter_Man_t * p, int fUseBias, int fUseBackward, clock_t nTimeNewOut )
+int Inter_ManPerformOneStep( Inter_Man_t * p, int fUseBias, int fUseBackward, abctime nTimeNewOut )
 {
     sat_solver * pSat;
     void * pSatCnf = NULL;
@@ -209,7 +209,7 @@ int Inter_ManPerformOneStep( Inter_Man_t * p, int fUseBias, int fUseBackward, cl
     int * pGlobalVars;
     int status, RetValue;
     int i, Var;
-    clock_t clk;
+    abctime clk;
 //    assert( p->pInterNew == NULL );
 
     // derive the SAT solver
@@ -231,10 +231,10 @@ int Inter_ManPerformOneStep( Inter_Man_t * p, int fUseBias, int fUseBackward, cl
     pSat->pGlobalVars = fUseBias? pGlobalVars : NULL;
 
     // solve the problem
-clk = clock();
+clk = Abc_Clock();
     status = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)p->nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
     p->nConfCur = pSat->stats.conflicts;
-p->timeSat += clock() - clk;
+p->timeSat += Abc_Clock() - clk;
 
     pSat->pGlobalVars = NULL;
     ABC_FREE( pGlobalVars );
@@ -256,7 +256,7 @@ p->timeSat += clock() - clk;
         return RetValue;
 
     // create the resulting manager
-clk = clock();
+clk = Abc_Clock();
 /*
     if ( !fUseIp )
     {
@@ -307,7 +307,7 @@ clk = clock();
     p->pInterNew = (Aig_Man_t *)Inta_ManInterpolate( pManInterA, (Sto_Man_t *)pSatCnf, p->vVarsAB, 0 );
     Inta_ManFree( pManInterA );
 
-p->timeInt += clock() - clk;
+p->timeInt += Abc_Clock() - clk;
     Sto_ManFree( (Sto_Man_t *)pSatCnf );
     return RetValue;
 }
diff --git a/src/proof/int/intUtil.c b/src/proof/int/intUtil.c
index b93a7453..b7e18f09 100644
--- a/src/proof/int/intUtil.c
+++ b/src/proof/int/intUtil.c
@@ -49,7 +49,7 @@ int Inter_ManCheckInitialState( Aig_Man_t * p )
     Aig_Obj_t * pObj;
     sat_solver * pSat;
     int i, status;
-    clock_t clk = clock();
+    abctime clk = Abc_Clock();
     pCnf = Cnf_Derive( p, Saig_ManRegNum(p) ); 
     pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 1 );
     if ( pSat == NULL )
@@ -58,7 +58,7 @@ int Inter_ManCheckInitialState( Aig_Man_t * p )
         return 0;
     }
     status = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
-    ABC_PRT( "Time", clock() - clk );
+    ABC_PRT( "Time", Abc_Clock() - clk );
     if ( status == l_True )
     {
         p->pSeqModel = Abc_CexAlloc( Aig_ManRegNum(p), Saig_ManPiNum(p), 1 );
@@ -87,7 +87,7 @@ int Inter_ManCheckAllStates( Aig_Man_t * p )
     Cnf_Dat_t * pCnf;
     sat_solver * pSat;
     int status;
-    clock_t clk = clock();
+    abctime clk = Abc_Clock();
     pCnf = Cnf_Derive( p, Saig_ManRegNum(p) ); 
     pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
     Cnf_DataFree( pCnf );
@@ -95,7 +95,7 @@ int Inter_ManCheckAllStates( Aig_Man_t * p )
         return 1;
     status = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
     sat_solver_delete( pSat );
-    ABC_PRT( "Time", clock() - clk );
+    ABC_PRT( "Time", Abc_Clock() - clk );
     return status == l_False;
 }