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/proof/ssc/sscSat.c | 26 +++++++++++++-------------
 1 file changed, 13 insertions(+), 13 deletions(-)

(limited to 'src/proof/ssc/sscSat.c')

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;
-- 
cgit v1.2.3