Fixing time primtouts in &vta and &gla.

2 files changed, 22 insertions, 19 deletions

diff --git a/src/aig/gia/giaAbsGla.c b/src/aig/gia/giaAbsGla.c
index c95c68cb..1a4e9cd2 100644
--- a/src/aig/gia/giaAbsGla.c
+++ b/src/aig/gia/giaAbsGla.c
@@ -86,11 +86,11 @@ struct Gla_Man_t_
     Vec_Int_t *    pvRefis;         // vectors of each object
 //    Vec_Int_t *    vPrioSels;       // selected priorities
     // statistics  
-    int            timeInit;
-    int            timeSat;
-    int            timeUnsat;
-    int            timeCex;
-    int            timeOther;
+    clock_t        timeInit;
+    clock_t        timeSat;
+    clock_t        timeUnsat;
+    clock_t        timeCex;
+    clock_t        timeOther;
 };
 
 // declarations
@@ -194,7 +194,8 @@ int Gia_ManGlaRefine( Gia_Man_t * p, Abc_Cex_t * pCex, int fMinCut, int fVerbose
     Aig_Man_t * pAig;
     Abc_Cex_t * pCare;
     Vec_Int_t * vPis, * vPPis;
-    int f, i, iObjId, clk = clock();
+    int f, i, iObjId;
+    clock_t clk = clock();
     int nOnes = 0, Counter = 0;
     if ( p->vGateClasses == NULL )
     {
@@ -1547,7 +1548,8 @@ Vec_Int_t * Gla_ManUnsatCore( Gla_Man_t * p, int f, Vec_Int_t * vCla2Obj, sat_so
     Vec_Int_t * vCore;
     int iLit = Gla_ManGetOutLit( p, f );
     int nConfPrev = pSat->stats.conflicts;
-    int i, Entry, RetValue, clk = clock();
+    int i, Entry, RetValue;
+    clock_t clk = clock();
     if ( piRetValue )
         *piRetValue = 1;
     // consider special case when PO points to the flop
@@ -1616,7 +1618,7 @@ Vec_Int_t * Gla_ManUnsatCore( Gla_Man_t * p, int f, Vec_Int_t * vCla2Obj, sat_so
   SeeAlso     []
 
 ***********************************************************************/
-void Gla_ManAbsPrintFrame( Gla_Man_t * p, int nCoreSize, int nFrames, int nConfls, int nCexes, int Time )
+void Gla_ManAbsPrintFrame( Gla_Man_t * p, int nCoreSize, int nFrames, int nConfls, int nCexes, clock_t Time )
 {
     if ( Abc_FrameIsBatchMode() && nCoreSize <= 0 )
         return;
@@ -1633,7 +1635,7 @@ void Gla_ManAbsPrintFrame( Gla_Man_t * p, int nCoreSize, int nFrames, int nConfl
         Abc_Print( 1, "%5d", nCexes ); 
     Abc_Print( 1, " %9d", sat_solver2_nvars(p->pSat) ); 
     Abc_Print( 1, " %6d", nCoreSize > 0 ? nCoreSize : 0 ); 
-    Abc_Print( 1, "%9.2f sec", (float)(Time)/(float)(CLOCKS_PER_SEC) );
+    Abc_Print( 1, "%9.2f sec", 1.0*Time/CLOCKS_PER_SEC );
     Abc_Print( 1, "%5.1f Gb", sat_solver2_memory_proof( p->pSat ) / (1<<30) );
     Abc_Print( 1, "%s", nCoreSize > 0 ? "\n" : "\r" );
     fflush( stdout );
@@ -1750,7 +1752,7 @@ int Gia_GlaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars, int fStartVta )
     Vec_Int_t * vCore, * vPPis;
     Abc_Cex_t * pCex = NULL;
     int f, i, iPrev, nConfls, Status, nCoreSize, fOneIsSent = 0, RetValue = -1;
-    int clk = clock(), clk2;
+    clock_t clk = clock(), clk2;
     // preconditions
     assert( Gia_ManPoNum(pAig) == 1 );
     assert( pPars->nFramesMax == 0 || pPars->nFramesStart <= pPars->nFramesMax );
diff --git a/src/aig/gia/giaAbsVta.c b/src/aig/gia/giaAbsVta.c
index 6358f957..4ac4045e 100644
--- a/src/aig/gia/giaAbsVta.c
+++ b/src/aig/gia/giaAbsVta.c
@@ -72,10 +72,10 @@ struct Vta_Man_t_
     sat_solver2 * pSat;         // incremental SAT solver
     Vec_Int_t *   vAddedNew;    // the IDs of variables added to the solver
     // statistics 
-    int           timeSat;
-    int           timeUnsat;
-    int           timeCex;
-    int           timeOther;
+    clock_t       timeSat;
+    clock_t       timeUnsat;
+    clock_t       timeCex;
+    clock_t       timeOther;
 };
 
 
@@ -1108,7 +1108,8 @@ Vec_Int_t * Vta_ManUnsatCore( int iLit, Vec_Int_t * vCla2Var, sat_solver2 * pSat
 {
     Vec_Int_t * vPres;
     Vec_Int_t * vCore;
-    int k, i, Entry, RetValue, clk = clock();
+    int k, i, Entry, RetValue;
+    clock_t clk = clock();
     int nConfPrev = pSat->stats.conflicts;
     if ( piRetValue )
         *piRetValue = 1;
@@ -1186,7 +1187,7 @@ Vec_Int_t * Vta_ManUnsatCore( int iLit, Vec_Int_t * vCla2Var, sat_solver2 * pSat
   SeeAlso     []
 
 ***********************************************************************/
-int Vta_ManAbsPrintFrame( Vta_Man_t * p, Vec_Int_t * vCore, int nFrames, int nConfls, int nCexes, int Time, int fVerbose )
+int Vta_ManAbsPrintFrame( Vta_Man_t * p, Vec_Int_t * vCore, int nFrames, int nConfls, int nCexes, clock_t Time, int fVerbose )
 {
     unsigned * pInfo;
     int * pCountAll = NULL, * pCountUni = NULL;
@@ -1245,7 +1246,7 @@ int Vta_ManAbsPrintFrame( Vta_Man_t * p, Vec_Int_t * vCore, int nFrames, int nCo
         Abc_Print( 1, "    ..." ); 
         for ( k = 0; k < 7; k++ )
             Abc_Print( 1, "     " );
-        Abc_Print( 1, "%9.2f sec", (float)(Time)/(float)(CLOCKS_PER_SEC) );
+        Abc_Print( 1, "%9.2f sec", 1.0*Time/CLOCKS_PER_SEC );
         Abc_Print( 1, "%5.1f Gb", sat_solver2_memory_proof( p->pSat ) / (1<<30) );
         Abc_Print( 1, "\r" );
     }
@@ -1267,7 +1268,7 @@ int Vta_ManAbsPrintFrame( Vta_Man_t * p, Vec_Int_t * vCore, int nFrames, int nCo
             for ( k = nFrames; k < 7; k++ )
                 Abc_Print( 1, "     " );
         }
-        Abc_Print( 1, "%9.2f sec", (float)(Time)/(float)(CLOCKS_PER_SEC) );
+        Abc_Print( 1, "%9.2f sec", 1.0*Time/CLOCKS_PER_SEC );
         Abc_Print( 1, "%5.1f Gb", sat_solver2_memory_proof( p->pSat ) / (1<<30) );
         Abc_Print( 1, "\n" );
     }
@@ -1546,7 +1547,7 @@ int Gia_VtaPerformInt( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
     Vec_Int_t * vCore;
     Abc_Cex_t * pCex = NULL;
     int i, f, nConfls, Status, nObjOld, RetValue = -1, nCountNoChange = 0, fOneIsSent = 0;
-    int clk = clock(), clk2;
+    clock_t clk = clock(), clk2;
     // preconditions
     assert( Gia_ManPoNum(pAig) == 1 );
     assert( pPars->nFramesMax == 0 || pPars->nFramesStart <= pPars->nFramesMax );