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

11 files changed, 56 insertions, 56 deletions

diff --git a/src/bdd/cas/casCore.c b/src/bdd/cas/casCore.c
index 35b1145c..b2e06805 100644
--- a/src/bdd/cas/casCore.c
+++ b/src/bdd/cas/casCore.c
@@ -81,7 +81,7 @@ int Abc_CascadeExperiment( char * pFileGeneric, DdManager * dd, DdNode ** pOutpu
     int i;
     int nVars = nInputs;
     int nOuts = nOutputs;
-    clock_t clk1;
+    abctime clk1;
 
     int      nVarsEnc;              // the number of additional variables to encode outputs
     DdNode * pbVarsEnc[MAXOUTPUTS]; // the BDDs of the encoding vars
@@ -140,11 +140,11 @@ int Abc_CascadeExperiment( char * pFileGeneric, DdManager * dd, DdNode ** pOutpu
 //  printf( "\n" );
 
     // derive the single-output function
-    clk1 = clock();
+    clk1 = Abc_Clock();
     aFunc = GetSingleOutputFunction( dd, pOutputs, nOuts, pbVarsEnc, nVarsEnc, fVerbose );  Cudd_Ref( aFunc );
 //  aFunc = GetSingleOutputFunctionRemapped( dd, pOutputs, nOuts, pbVarsEnc, nVarsEnc );  Cudd_Ref( aFunc );
 //  if ( fVerbose )
-//  printf( "Single-output function computation time = %.2f sec\n", (float)(clock() - clk1)/(float)(CLOCKS_PER_SEC) );
+//  printf( "Single-output function computation time = %.2f sec\n", (float)(Abc_Clock() - clk1)/(float)(CLOCKS_PER_SEC) );
  
 //fprintf( pTable, "%d ", Cudd_SharingSize( pOutputs, nOutputs ) );
 //fprintf( pTable, "%d ", Extra_ProfileWidthSharingMax(dd, pOutputs, nOutputs) );
@@ -155,7 +155,7 @@ int Abc_CascadeExperiment( char * pFileGeneric, DdManager * dd, DdNode ** pOutpu
     // reorder the single output function
 //    if ( fVerbose )
 //  printf( "Reordering variables...\n");
-    clk1 = clock();
+    clk1 = Abc_Clock();
 //  if ( fVerbose )
 //  printf( "Node count before = %6d\n", Cudd_DagSize( aFunc ) );
 //  Cudd_ReduceHeap(dd, CUDD_REORDER_SIFT,1);
@@ -168,7 +168,7 @@ int Abc_CascadeExperiment( char * pFileGeneric, DdManager * dd, DdNode ** pOutpu
     if ( fVerbose )
     printf( "MTBDD reordered = %6d nodes\n", Cudd_DagSize( aFunc ) );
     if ( fVerbose )
-    printf( "Variable reordering time = %.2f sec\n", (float)(clock() - clk1)/(float)(CLOCKS_PER_SEC) );
+    printf( "Variable reordering time = %.2f sec\n", (float)(Abc_Clock() - clk1)/(float)(CLOCKS_PER_SEC) );
 //  printf( "\n" );
 //  printf( "Variable order is: " );
 //  for ( i = 0; i < dd->size; i++ )
@@ -178,16 +178,16 @@ int Abc_CascadeExperiment( char * pFileGeneric, DdManager * dd, DdNode ** pOutpu
 //fprintf( pTable, "%d ", Extra_ProfileWidthMax(dd, aFunc) );
 
     // write the single-output function into BLIF for verification
-    clk1 = clock();
+    clk1 = Abc_Clock();
     if ( fCheck )
     WriteSingleOutputFunctionBlif( dd, aFunc, pNames, nNames, FileNameIni );
 //    if ( fVerbose )
-//  printf( "Single-output function writing time = %.2f sec\n", (float)(clock() - clk1)/(float)(CLOCKS_PER_SEC) );
+//  printf( "Single-output function writing time = %.2f sec\n", (float)(Abc_Clock() - clk1)/(float)(CLOCKS_PER_SEC) );
 
 /*
     ///////////////////////////////////////////////////////////////////
     // verification of single output function
-    clk1 = clock();
+    clk1 = Abc_Clock();
     {
         BFunc g_Func;
         DdNode * aRes;
@@ -214,7 +214,7 @@ int Abc_CascadeExperiment( char * pFileGeneric, DdManager * dd, DdNode ** pOutpu
         // delocate
         Extra_Dissolve( &g_Func );
     }
-    printf( "Preliminary verification time = %.2f sec\n", (float)(clock() - clk1)/(float)(CLOCKS_PER_SEC) );
+    printf( "Preliminary verification time = %.2f sec\n", (float)(Abc_Clock() - clk1)/(float)(CLOCKS_PER_SEC) );
     ///////////////////////////////////////////////////////////////////
 */
 
@@ -224,7 +224,7 @@ int Abc_CascadeExperiment( char * pFileGeneric, DdManager * dd, DdNode ** pOutpu
 /*
     ///////////////////////////////////////////////////////////////////
     // verification of the decomposed LUT network
-    clk1 = clock();
+    clk1 = Abc_Clock();
     {
         BFunc g_Func;
         DdNode * aRes;
@@ -251,7 +251,7 @@ int Abc_CascadeExperiment( char * pFileGeneric, DdManager * dd, DdNode ** pOutpu
         // delocate 
         Extra_Dissolve( &g_Func );
     }
-    printf( "Final verification time = %.2f sec\n", (float)(clock() - clk1)/(float)(CLOCKS_PER_SEC) );
+    printf( "Final verification time = %.2f sec\n", (float)(Abc_Clock() - clk1)/(float)(CLOCKS_PER_SEC) );
     ///////////////////////////////////////////////////////////////////
 */
  
@@ -325,24 +325,24 @@ void Experiment2( BFunc * pFunc )
     strcat( FileNameFin, "_LUT.blif" );
 
     // derive the single-output function IN THE NEW MANAGER
-    clk1 = clock();
+    clk1 = Abc_Clock();
 //  aFunc = GetSingleOutputFunction( dd, pFunc->pOutputs, nOuts, pbVarsEnc, nVarsEnc );  Cudd_Ref( aFunc );
     aFunc = GetSingleOutputFunctionRemappedNewDD( dd, pFunc->pOutputs, nOuts, &DdNew );  Cudd_Ref( aFunc );
-    printf( "Single-output function derivation time = %.2f sec\n", (float)(clock() - clk1)/(float)(CLOCKS_PER_SEC) );
-//  s_RemappingTime = clock() - clk1;
+    printf( "Single-output function derivation time = %.2f sec\n", (float)(Abc_Clock() - clk1)/(float)(CLOCKS_PER_SEC) );
+//  s_RemappingTime = Abc_Clock() - clk1;
 
     // dispose of the multiple-output function
     Extra_Dissolve( pFunc );
 
     // reorder the single output function
     printf( "\nReordering variables in the new manager...\n");
-    clk1 = clock();
+    clk1 = Abc_Clock();
     printf( "Node count before = %d\n", Cudd_DagSize( aFunc ) );
 //  Cudd_ReduceHeap(DdNew, CUDD_REORDER_SIFT,1);
     Cudd_ReduceHeap(DdNew, CUDD_REORDER_SYMM_SIFT,1);
 //  Cudd_ReduceHeap(DdNew, CUDD_REORDER_SYMM_SIFT,1);
     printf( "Node count after  = %d\n", Cudd_DagSize( aFunc ) );
-    printf( "Variable reordering time = %.2f sec\n", (float)(clock() - clk1)/(float)(CLOCKS_PER_SEC) );
+    printf( "Variable reordering time = %.2f sec\n", (float)(Abc_Clock() - clk1)/(float)(CLOCKS_PER_SEC) );
     printf( "\n" );
 
 //fprintf( pTable, "%d ", Cudd_DagSize( aFunc ) );
@@ -360,14 +360,14 @@ void Experiment2( BFunc * pFunc )
 
 
     // write the single-output function into BLIF for verification
-    clk1 = clock();
+    clk1 = Abc_Clock();
     WriteSingleOutputFunctionBlif( DdNew, aFunc, pNames, nNames, FileNameIni );
-    printf( "Single-output function writing time = %.2f sec\n", (float)(clock() - clk1)/(float)(CLOCKS_PER_SEC) );
+    printf( "Single-output function writing time = %.2f sec\n", (float)(Abc_Clock() - clk1)/(float)(CLOCKS_PER_SEC) );
 
 
     ///////////////////////////////////////////////////////////////////
     // verification of single output function
-    clk1 = clock();
+    clk1 = Abc_Clock();
     {
         BFunc g_Func;
         DdNode * aRes;
@@ -394,7 +394,7 @@ void Experiment2( BFunc * pFunc )
         // delocate
         Extra_Dissolve( &g_Func );
     }
-    printf( "Preliminary verification time = %.2f sec\n", (float)(clock() - clk1)/(float)(CLOCKS_PER_SEC) );
+    printf( "Preliminary verification time = %.2f sec\n", (float)(Abc_Clock() - clk1)/(float)(CLOCKS_PER_SEC) );
     ///////////////////////////////////////////////////////////////////
 
 
@@ -403,7 +403,7 @@ void Experiment2( BFunc * pFunc )
 /*
     ///////////////////////////////////////////////////////////////////
     // verification of the decomposed LUT network
-    clk1 = clock();
+    clk1 = Abc_Clock();
     {
         BFunc g_Func;
         DdNode * aRes;
@@ -430,7 +430,7 @@ void Experiment2( BFunc * pFunc )
         // delocate
         Extra_Dissolve( &g_Func );
     }
-    printf( "Final verification time = %.2f sec\n", (float)(clock() - clk1)/(float)(CLOCKS_PER_SEC) );
+    printf( "Final verification time = %.2f sec\n", (float)(Abc_Clock() - clk1)/(float)(CLOCKS_PER_SEC) );
     ///////////////////////////////////////////////////////////////////
 */
 
@@ -954,12 +954,12 @@ void WriteDDintoBLIFfileReorder( DdManager * dd, FILE * pFile, DdNode * Func, ch
 
     ///////////////////////////////////////////////////////////////
     DdNode * bFmin;
-    clock_t clk1;
+    abctime clk1;
 
     if ( s_ddmin == NULL )
         s_ddmin = Cudd_Init( dd->size, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0);
 
-    clk1 = clock();
+    clk1 = Abc_Clock();
     bFmin = Cudd_bddTransfer( dd, s_ddmin, Func );  Cudd_Ref( bFmin );
 
     // reorder
diff --git a/src/bdd/cas/casDec.c b/src/bdd/cas/casDec.c
index 06ce04ea..82c23240 100644
--- a/src/bdd/cas/casDec.c
+++ b/src/bdd/cas/casDec.c
@@ -128,14 +128,14 @@ int CreateDecomposedNetwork( DdManager * dd, DdNode * aFunc, char ** pNames, int
     int nLutOutputs = 0;
     int nLutOutputsOrig = 0;
 
-    clock_t clk1;
+    abctime clk1;
 
     s_LutSize = nLutSize;
 
     s_nFuncVars = nNames;
 
     // get the profile
-    clk1 = clock();
+    clk1 = Abc_Clock();
     Extra_ProfileWidth( dd, aFunc, Profile, -1 );
 
 
@@ -284,10 +284,10 @@ int CreateDecomposedNetwork( DdManager * dd, DdNode * aFunc, char ** pNames, int
         }
         else
         {
-            clock_t clk2 = clock();
+            abctime clk2 = Abc_Clock();
 //          p->bRelation = PerformTheEncoding( dd, p->pbCols, p->nCols, bVarsCube, bCVars, p->nMulti, &p->nSimple );  Cudd_Ref( p->bRelation );
             p->bRelation = Extra_bddEncodingNonStrict( dd, p->pbCols, p->nCols, bVarsCube, bCVars, p->nMulti, &p->nSimple );  Cudd_Ref( p->bRelation );
-            s_EncodingTime += clock() - clk2;
+            s_EncodingTime += Abc_Clock() - clk2;
         }
 
         // update the number of LUT outputs
@@ -353,7 +353,7 @@ printf( "Stage %3d: In = %3d  InP = %3d  Cols = %5d  Multi = %2d  Simple = %2d
 
     if ( fVerbose )
     {
-    printf( "Pure decomposition time   = %.2f sec\n", (float)(clock() - clk1 - s_EncodingTime)/(float)(CLOCKS_PER_SEC) );
+    printf( "Pure decomposition time   = %.2f sec\n", (float)(Abc_Clock() - clk1 - s_EncodingTime)/(float)(CLOCKS_PER_SEC) );
     printf( "Encoding time             = %.2f sec\n", (float)(s_EncodingTime)/(float)(CLOCKS_PER_SEC) );
 //  printf( "Encoding search time      = %.2f sec\n", (float)(s_EncSearchTime)/(float)(CLOCKS_PER_SEC) );
 //  printf( "Encoding compute time     = %.2f sec\n", (float)(s_EncComputeTime)/(float)(CLOCKS_PER_SEC) );
@@ -361,13 +361,13 @@ printf( "Stage %3d: In = %3d  InP = %3d  Cols = %5d  Multi = %2d  Simple = %2d
 
 
 //fprintf( pTable, "%.2f ", (float)(s_ReadingTime)/(float)(CLOCKS_PER_SEC) );
-//fprintf( pTable, "%.2f ", (float)(clock() - clk1 - s_EncodingTime)/(float)(CLOCKS_PER_SEC) );
+//fprintf( pTable, "%.2f ", (float)(Abc_Clock() - clk1 - s_EncodingTime)/(float)(CLOCKS_PER_SEC) );
 //fprintf( pTable, "%.2f ", (float)(s_EncodingTime)/(float)(CLOCKS_PER_SEC) );
 //fprintf( pTable, "%.2f ", (float)(s_RemappingTime)/(float)(CLOCKS_PER_SEC) );
 
 
     // write LUTs into the BLIF file
-    clk1 = clock();
+    clk1 = Abc_Clock();
     if ( fCheck )
     {
         FILE * pFile;
@@ -388,7 +388,7 @@ printf( "Stage %3d: In = %3d  InP = %3d  Cols = %5d  Multi = %2d  Simple = %2d
         fprintf( pFile, ".end\n" );
         fclose( pFile );
         if ( fVerbose )
-        printf( "Output file writing time  = %.2f sec\n", (float)(clock() - clk1)/(float)(CLOCKS_PER_SEC) );
+        printf( "Output file writing time  = %.2f sec\n", (float)(Abc_Clock() - clk1)/(float)(CLOCKS_PER_SEC) );
     }
 
 
diff --git a/src/bdd/cudd/cuddAndAbs.c b/src/bdd/cudd/cuddAndAbs.c
index 8e1fd161..d9ad1d23 100644
--- a/src/bdd/cudd/cuddAndAbs.c
+++ b/src/bdd/cudd/cuddAndAbs.c
@@ -259,7 +259,7 @@ cuddBddAndAbstractRecur(
         }
     }
 
-    if ( manager->TimeStop && clock() > manager->TimeStop )
+    if ( manager->TimeStop && Abc_Clock() > manager->TimeStop )
         return NULL;
 
     if (topf == top) {
diff --git a/src/bdd/cudd/cuddBddIte.c b/src/bdd/cudd/cuddBddIte.c
index 0d28ce96..803d5f19 100644
--- a/src/bdd/cudd/cuddBddIte.c
+++ b/src/bdd/cudd/cuddBddIte.c
@@ -926,7 +926,7 @@ cuddBddAndRecur(
         if (r != NULL) return(r);
     }
 
-    if ( manager->TimeStop && clock() > manager->TimeStop )
+    if ( manager->TimeStop && Abc_Clock() > manager->TimeStop )
         return NULL;
 
     /* Here we can skip the use of cuddI, because the operands are known
diff --git a/src/bdd/cudd/cuddBridge.c b/src/bdd/cudd/cuddBridge.c
index 8cbb22d5..94b388f5 100644
--- a/src/bdd/cudd/cuddBridge.c
+++ b/src/bdd/cudd/cuddBridge.c
@@ -976,9 +976,9 @@ cuddBddTransferRecur(
     if ( st__lookup(table, (const char *)f, (char **)&res))
         return(Cudd_NotCond(res,comple));
 
-    if ( ddS->TimeStop && clock() > ddS->TimeStop )
+    if ( ddS->TimeStop && Abc_Clock() > ddS->TimeStop )
         return NULL;
-    if ( ddD->TimeStop && clock() > ddD->TimeStop )
+    if ( ddD->TimeStop && Abc_Clock() > ddD->TimeStop )
         return NULL;
     
     /* Recursive step. */
diff --git a/src/bdd/cudd/cuddCompose.c b/src/bdd/cudd/cuddCompose.c
index f3aff14b..0341ef53 100644
--- a/src/bdd/cudd/cuddCompose.c
+++ b/src/bdd/cudd/cuddCompose.c
@@ -1251,7 +1251,7 @@ cuddBddVarMapRecur(
         return(Cudd_NotCond(res,F != f));
     }
 
-    if ( manager->TimeStop && clock() > manager->TimeStop )
+    if ( manager->TimeStop && Abc_Clock() > manager->TimeStop )
         return NULL;
 
     /* Split and recur on children of this node. */
diff --git a/src/bdd/cudd/cuddInt.h b/src/bdd/cudd/cuddInt.h
index f0aab056..2ccf86a7 100644
--- a/src/bdd/cudd/cuddInt.h
+++ b/src/bdd/cudd/cuddInt.h
@@ -486,7 +486,7 @@ struct DdManager {      /* specialized DD symbol table */
 #endif
     DdNode * bFunc;
     DdNode * bFunc2;
-    clock_t TimeStop;           /* timeout for reordering */
+    abctime TimeStop;           /* timeout for reordering */
 };
 
 typedef struct Move {
diff --git a/src/bdd/cudd/cuddSymmetry.c b/src/bdd/cudd/cuddSymmetry.c
index 5813f123..c2b1e858 100644
--- a/src/bdd/cudd/cuddSymmetry.c
+++ b/src/bdd/cudd/cuddSymmetry.c
@@ -367,7 +367,7 @@ cuddSymmSifting(
         if (ddTotalNumberSwapping >= table->siftMaxSwap)
             break;
         // enable timeout during variable reodering - alanmi 2/13/11
-        if ( table->TimeStop && clock() > table->TimeStop )
+        if ( table->TimeStop && Abc_Clock() > table->TimeStop )
             break;
         x = table->perm[var[i]];
 #ifdef DD_STATS
diff --git a/src/bdd/dsd/dsdProc.c b/src/bdd/dsd/dsdProc.c
index 996fd3dc..bcc3102c 100644
--- a/src/bdd/dsd/dsdProc.c
+++ b/src/bdd/dsd/dsdProc.c
@@ -114,7 +114,7 @@ void Dsd_Decompose( Dsd_Manager_t * pDsdMan, DdNode ** pbFuncs, int nFuncs )
 {
     DdManager * dd = pDsdMan->dd;
     int i;
-    clock_t clk;
+    abctime clk;
     Dsd_Node_t * pTemp;
     int SumMaxGateSize = 0;
     int nDecOutputs = 0;
@@ -144,7 +144,7 @@ s_Loops2Useless = 0;
     s_nDecBlocks = 0;
 
     // perform decomposition for all outputs
-    clk = clock();
+    clk = Abc_Clock();
     pDsdMan->nRoots = 0;
     s_nCascades = 0;
     for ( i = 0; i < nFuncs; i++ )
@@ -156,9 +156,9 @@ s_Loops2Useless = 0;
         int nCascades;
         int MaxBlock;
         int nPrimeBlocks;
-        clock_t clk;
+        abctime clk;
 
-        clk = clock();
+        clk = Abc_Clock();
         nLiteralsPrev     = s_nLiterals;
         nDecBlocksPrev    = s_nDecBlocks;
         nExorGatesPrev    = s_nExorGates;
@@ -185,7 +185,7 @@ s_Loops2Useless = 0;
             printf("Max=%3d. ", MaxBlock ); 
             printf("Reuse=%2d. ", s_nReusedBlocks-nReusedBlocksPres ); 
             printf("Csc=%2d. ", nCascades ); 
-            printf("T= %.2f s. ", (float)(clock()-clk)/(float)(CLOCKS_PER_SEC) ) ;
+            printf("T= %.2f s. ", (float)(Abc_Clock()-clk)/(float)(CLOCKS_PER_SEC) ) ;
             printf("Bdd=%2d. ", Cudd_DagSize(pbFuncs[i]) ); 
             printf("\n");
             fflush( stdout );
@@ -203,7 +203,7 @@ s_Loops2Useless = 0;
         printf( "  The sum of max gate sizes                 = %5d\n", SumMaxGateSize );
         printf( "  Shared BDD size                           = %5d\n", Cudd_SharingSize( pbFuncs, nFuncs ) );
         printf( "  Decomposition entries                     = %5d\n", st__count( pDsdMan->Table ) );
-        printf( "  Pure decomposition time                   =  %.2f sec\n", (float)(clock() - clk)/(float)(CLOCKS_PER_SEC) );
+        printf( "  Pure decomposition time                   =  %.2f sec\n", (float)(Abc_Clock() - clk)/(float)(CLOCKS_PER_SEC) );
     }
 /*
     printf( "s_Loops1 = %d.\n", s_Loops1 );
diff --git a/src/bdd/reo/reoShuffle.c b/src/bdd/reo/reoShuffle.c
index 86aab4b9..e1c33617 100644
--- a/src/bdd/reo/reoShuffle.c
+++ b/src/bdd/reo/reoShuffle.c
@@ -162,7 +162,7 @@ void Extra_ShuffleTest( reo_man * pReo, DdManager * dd, DdNode * Func )
 
     DdNode * Temp, * bRemap;
     int nSuppSize, OffSet, Num, i;
-    clock_t clk;
+    abctime clk;
     int pOrder[1000], pOrderInv[1000];
     assert( dd->size < 1000 );
 
@@ -198,17 +198,17 @@ void Extra_ShuffleTest( reo_man * pReo, DdManager * dd, DdNode * Func )
 //    Extra_ReorderSetVerification( pReo, 1 );
     bRemap = Extra_bddRemapUp( dd, Func );  Cudd_Ref( bRemap );
 
-clk = clock();
+clk = Abc_Clock();
     Temp  = reoShuffle( pReo, dd, bRemap, pOrder, pOrderInv );  Cudd_Ref( Temp );
-//runtime1 += clock() - clk;
+//runtime1 += Abc_Clock() - clk;
 
 //printf( "Initial = %d. Final = %d.\n", Cudd_DagSize(bRemap), Cudd_DagSize(Temp)  );
 
     {
         DdNode * bFuncPerm;
-clk = clock();
+clk = Abc_Clock();
         bFuncPerm = Cudd_bddPermute( dd, bRemap, pOrderInv );  Cudd_Ref( bFuncPerm );
-//runtime2 += clock() - clk;
+//runtime2 += Abc_Clock() - clk;
         if ( bFuncPerm != Temp )
         {
             printf( "REO: Internal verification has failed!\n" );
diff --git a/src/bdd/reo/reoTest.c b/src/bdd/reo/reoTest.c
index 58e442f3..f9b1cc04 100644
--- a/src/bdd/reo/reoTest.c
+++ b/src/bdd/reo/reoTest.c
@@ -182,21 +182,21 @@ int Extra_bddReorderTest( DdManager * dd, DdNode * bF )
     static DdManager * s_ddmin;
     DdNode * bFmin;
     int  nNodes;
-//    clock_t clk1;
+//    abctime clk1;
 
     if ( s_ddmin == NULL )
         s_ddmin = Cudd_Init( dd->size, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0);
 
 //    Cudd_ShuffleHeap( s_ddmin, dd->invperm );
 
-//    clk1 = clock();
+//    clk1 = Abc_Clock();
     bFmin = Cudd_bddTransfer( dd, s_ddmin, bF );  Cudd_Ref( bFmin );
     Cudd_ReduceHeap(s_ddmin,CUDD_REORDER_SIFT,1);
 //    Cudd_ReduceHeap(s_ddmin,CUDD_REORDER_SYMM_SIFT,1);
     nNodes = Cudd_DagSize( bFmin );
     Cudd_RecursiveDeref( s_ddmin, bFmin );
 
-//    printf( "Classical variable reordering time = %.2f sec\n", (float)(clock() - clk1)/(float)(CLOCKS_PER_SEC) );
+//    printf( "Classical variable reordering time = %.2f sec\n", (float)(Abc_Clock() - clk1)/(float)(CLOCKS_PER_SEC) );
     return nNodes;
 }
 
@@ -222,14 +222,14 @@ int Extra_addReorderTest( DdManager * dd, DdNode * aF )
     DdNode * aFmin;
     int  nNodesBeg;
     int  nNodesEnd;
-    clock_t clk1;
+    abctime clk1;
 
     if ( s_ddmin == NULL )
         s_ddmin = Cudd_Init( dd->size, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0);
 
 //    Cudd_ShuffleHeap( s_ddmin, dd->invperm );
 
-    clk1 = clock();
+    clk1 = Abc_Clock();
     bF    = Cudd_addBddPattern( dd, aF );         Cudd_Ref( bF );
     bFmin = Cudd_bddTransfer( dd, s_ddmin, bF );  Cudd_Ref( bFmin );
     Cudd_RecursiveDeref( dd, bF );
@@ -243,7 +243,7 @@ int Extra_addReorderTest( DdManager * dd, DdNode * aF )
     Cudd_RecursiveDeref( s_ddmin, aFmin );
 
     printf( "Classical reordering of ADDs: Before = %d. After = %d.\n", nNodesBeg, nNodesEnd );
-    printf( "Classical variable reordering time = %.2f sec\n", (float)(clock() - clk1)/(float)(CLOCKS_PER_SEC) );
+    printf( "Classical variable reordering time = %.2f sec\n", (float)(Abc_Clock() - clk1)/(float)(CLOCKS_PER_SEC) );
     return nNodesEnd;
 }