From 19c25fd6aab057b2373717f996fe538507c1b1e1 Mon Sep 17 00:00:00 2001
From: Alan Mishchenko <alanmi@berkeley.edu>
Date: Mon, 27 May 2013 15:09:23 -0700
Subject: Adding a wrapper around clock() for more accurate time counting in
 ABC.

---
 src/sat/bsat/satSolver.c | 24 ++++++++++++------------
 1 file changed, 12 insertions(+), 12 deletions(-)

(limited to 'src/sat/bsat/satSolver.c')

diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c
index d1310c81..8d1bd455 100644
--- a/src/sat/bsat/satSolver.c
+++ b/src/sat/bsat/satSolver.c
@@ -224,16 +224,16 @@ static inline void act_var_rescale(sat_solver* s)  {
     s->var_inc *= 1e-100;
 }
 static inline void act_clause_rescale(sat_solver* s) {
-//    static clock_t Total = 0;
+//    static abctime Total = 0;
     clause** cs = (clause**)veci_begin(&s->learnts);
-    int i;//, clk = clock();
+    int i;//, clk = Abc_Clock();
     for (i = 0; i < veci_size(&s->learnts); i++){
         float a = clause_activity(cs[i]);
         clause_setactivity(cs[i], a * (float)1e-20);
     }
     s->cla_inc *= (float)1e-20;
 
-    Total += clock() - clk;
+    Total += Abc_Clock() - clk;
 //    printf( "Rescaling...   Cla inc = %10.3f  Conf = %10d   ", s->cla_inc,  s->stats.conflicts );
 //    Abc_PrintTime( 1, "Time", Total );
 }
@@ -282,15 +282,15 @@ static inline void act_var_rescale(sat_solver* s) {
 }
 
 static inline void act_clause_rescale(sat_solver* s) {
-    static clock_t Total = 0;
-    clock_t clk = clock();
+    static abctime Total = 0;
+    abctime clk = Abc_Clock();
     unsigned* activity = (unsigned *)veci_begin(&s->act_clas);
     int i;
     for (i = 0; i < veci_size(&s->act_clas); i++)
         activity[i] >>= 14;
     s->cla_inc >>= 14;
     s->cla_inc = Abc_MaxInt( s->cla_inc, (1<<10) );
-    Total += clock() - clk;
+    Total += Abc_Clock() - clk;
 //    printf( "Rescaling...   Cla inc = %5d  Conf = %10d   ", s->cla_inc,  s->stats.conflicts );
 //    Abc_PrintTime( 1, "Time", Total );
 }
@@ -1226,8 +1226,8 @@ int sat_solver_simplify(sat_solver* s)
 
 void sat_solver_reducedb(sat_solver* s)
 {
-    static clock_t TimeTotal = 0;
-    clock_t clk = clock();
+    static abctime TimeTotal = 0;
+    abctime clk = Abc_Clock();
     Sat_Mem_t * pMem = &s->Mem;
     int nLearnedOld = veci_size(&s->act_clas);
     int * act_clas = veci_begin(&s->act_clas);
@@ -1330,7 +1330,7 @@ void sat_solver_reducedb(sat_solver* s)
     assert( Counter == (int)s->stats.learnts );
 
     // report the results
-    TimeTotal += clock() - clk;
+    TimeTotal += Abc_Clock() - clk;
     if ( s->fVerbose )
     {
     Abc_Print(1, "reduceDB: Keeping %7d out of %7d clauses (%5.2f %%)  ",
@@ -1576,7 +1576,7 @@ static lbool sat_solver_search(sat_solver* s, ABC_INT64_T nof_conflicts)
             int next;
  
             // Reached bound on number of conflicts:
-            if ((nof_conflicts >= 0 && conflictC >= nof_conflicts) || (s->nRuntimeLimit && clock() > s->nRuntimeLimit)){
+            if ((nof_conflicts >= 0 && conflictC >= nof_conflicts) || (s->nRuntimeLimit && Abc_Clock() > s->nRuntimeLimit)){
                 s->progress_estimate = sat_solver_progress(s);
                 sat_solver_canceluntil(s,s->root_level);
                 veci_delete(&learnt_clause);
@@ -1786,7 +1786,7 @@ int sat_solver_solve(sat_solver* s, lit* begin, lit* end, ABC_INT64_T nConfLimit
     while (status == l_Undef){
         double Ratio = (s->stats.learnts == 0)? 0.0 :
             s->stats.learnts_literals / (double)s->stats.learnts;
-        if ( s->nRuntimeLimit && clock() > s->nRuntimeLimit )
+        if ( s->nRuntimeLimit && Abc_Clock() > s->nRuntimeLimit )
             break;
         if (s->verbosity >= 1)
         {
@@ -1810,7 +1810,7 @@ int sat_solver_solve(sat_solver* s, lit* begin, lit* end, ABC_INT64_T nConfLimit
             break;
         if ( s->nInsLimit  && s->stats.propagations > s->nInsLimit )
             break;
-        if ( s->nRuntimeLimit && clock() > s->nRuntimeLimit )
+        if ( s->nRuntimeLimit && Abc_Clock() > s->nRuntimeLimit )
             break;
     }
     if (s->verbosity >= 1)
-- 
cgit v1.2.3