Fixing time primtouts throughout the code.

11 files changed, 51 insertions, 48 deletions

diff --git a/src/sat/bsat/satChecker.c b/src/sat/bsat/satChecker.c
index f478928c..70bb9c85 100644
--- a/src/sat/bsat/satChecker.c
+++ b/src/sat/bsat/satChecker.c
@@ -22,7 +22,7 @@
 #include <stdlib.h>
 #include <string.h>
 #include <assert.h>
-#include <time.h>
+
 #include "misc/vec/vec.h"
 
 ABC_NAMESPACE_IMPL_START
diff --git a/src/sat/bsat/satInter.c b/src/sat/bsat/satInter.c
index 8617def9..6f564225 100644
--- a/src/sat/bsat/satInter.c
+++ b/src/sat/bsat/satInter.c
@@ -22,7 +22,7 @@
 #include <stdlib.h>
 #include <string.h>
 #include <assert.h>
-#include <time.h>
+
 #include "satStore.h"
 
 ABC_NAMESPACE_IMPL_START
@@ -71,9 +71,9 @@ struct Int_Man_t_
     int             nResLits;     // the number of literals of the resolvent
     int             nResLitsAlloc;// the number of literals of the resolvent
     // runtime stats
-    int             timeBcp;      // the runtime for BCP
-    int             timeTrace;    // the runtime of trace construction
-    int             timeTotal;    // the total runtime of interpolation
+    clock_t         timeBcp;      // the runtime for BCP
+    clock_t         timeTrace;    // the runtime of trace construction
+    clock_t         timeTotal;    // the total runtime of interpolation
 };
 
 // procedure to get hold of the clauses' truth table 
@@ -535,7 +535,7 @@ Sto_Cls_t * Int_ManPropagate( Int_Man_t * p, int Start )
 {
     Sto_Cls_t * pClause;
     int i;
-    int clk = clock();
+    clock_t clk = clock();
     for ( i = Start; i < p->nTrailSize; i++ )
     {
         pClause = Int_ManPropagateOne( p, p->pTrail[i] );
@@ -591,7 +591,7 @@ int Int_ManProofTraceOne( Int_Man_t * p, Sto_Cls_t * pConflict, Sto_Cls_t * pFin
     Sto_Cls_t * pReason;
     int i, v, Var, PrevId;
     int fPrint = 0;
-    int clk = clock();
+    clock_t clk = clock();
 
     // collect resolvent literals
     if ( p->fProofVerif )
@@ -1006,7 +1006,7 @@ int Int_ManInterpolate( Int_Man_t * p, Sto_Man_t * pCnf, int fVerbose, unsigned
 {
     Sto_Cls_t * pClause;
     int RetValue = 1;
-    int clkTotal = clock();
+    clock_t clkTotal = clock();
 
     // check that the CNF makes sense
     assert( pCnf->nVars > 0 && pCnf->nClauses > 0 );
diff --git a/src/sat/bsat/satInterA.c b/src/sat/bsat/satInterA.c
index 4057ce7e..8b2ef8b7 100644
--- a/src/sat/bsat/satInterA.c
+++ b/src/sat/bsat/satInterA.c
@@ -22,7 +22,7 @@
 #include <stdlib.h>
 #include <string.h>
 #include <assert.h>
-#include <time.h>
+
 #include "satStore.h"
 #include "src/aig/aig/aig.h"
 
@@ -70,9 +70,9 @@ struct Inta_Man_t_
     int             nResLits;     // the number of literals of the resolvent
     int             nResLitsAlloc;// the number of literals of the resolvent
     // runtime stats
-    int             timeBcp;      // the runtime for BCP
-    int             timeTrace;    // the runtime of trace construction
-    int             timeTotal;    // the total runtime of interpolation
+    clock_t         timeBcp;      // the runtime for BCP
+    clock_t         timeTrace;    // the runtime of trace construction
+    clock_t         timeTotal;    // the total runtime of interpolation
 };
 
 // procedure to get hold of the clauses' truth table 
@@ -491,7 +491,7 @@ Sto_Cls_t * Inta_ManPropagate( Inta_Man_t * p, int Start )
 {
     Sto_Cls_t * pClause;
     int i;
-    int clk = clock();
+    clock_t clk = clock();
     for ( i = Start; i < p->nTrailSize; i++ )
     {
         pClause = Inta_ManPropagateOne( p, p->pTrail[i] );
@@ -547,7 +547,7 @@ int Inta_ManProofTraceOne( Inta_Man_t * p, Sto_Cls_t * pConflict, Sto_Cls_t * pF
     Sto_Cls_t * pReason;
     int i, v, Var, PrevId;
     int fPrint = 0;
-    int clk = clock();
+    clock_t clk = clock();
 
     // collect resolvent literals
     if ( p->fProofVerif )
@@ -954,7 +954,7 @@ void * Inta_ManInterpolate( Inta_Man_t * p, Sto_Man_t * pCnf, void * vVarsAB, in
     Aig_Obj_t * pObj;
     Sto_Cls_t * pClause;
     int RetValue = 1;
-    int clkTotal = clock();
+    clock_t clkTotal = clock();
 
     // check that the CNF makes sense
     assert( pCnf->nVars > 0 && pCnf->nClauses > 0 );
diff --git a/src/sat/bsat/satInterB.c b/src/sat/bsat/satInterB.c
index a9b18fd5..5a154aa0 100644
--- a/src/sat/bsat/satInterB.c
+++ b/src/sat/bsat/satInterB.c
@@ -22,7 +22,7 @@
 #include <stdlib.h>
 #include <string.h>
 #include <assert.h>
-#include <time.h>
+
 #include "satStore.h"
 #include "src/aig/aig/aig.h"
 
@@ -70,9 +70,9 @@ struct Intb_Man_t_
     int             nResLits;     // the number of literals of the resolvent
     int             nResLitsAlloc;// the number of literals of the resolvent
     // runtime stats
-    int             timeBcp;      // the runtime for BCP
-    int             timeTrace;    // the runtime of trace construction
-    int             timeTotal;    // the total runtime of interpolation
+    clock_t         timeBcp;      // the runtime for BCP
+    clock_t         timeTrace;    // the runtime of trace construction
+    clock_t         timeTotal;    // the total runtime of interpolation
 };
 
 // procedure to get hold of the clauses' truth table 
@@ -493,7 +493,7 @@ Sto_Cls_t * Intb_ManPropagate( Intb_Man_t * p, int Start )
 {
     Sto_Cls_t * pClause;
     int i;
-    int clk = clock();
+    clock_t clk = clock();
     for ( i = Start; i < p->nTrailSize; i++ )
     {
         pClause = Intb_ManPropagateOne( p, p->pTrail[i] );
@@ -570,7 +570,7 @@ int Intb_ManProofTraceOne( Intb_Man_t * p, Sto_Cls_t * pConflict, Sto_Cls_t * pF
     Sto_Cls_t * pReason;
     int i, v, Var, PrevId;
     int fPrint = 0;
-    int clk = clock();
+    clock_t clk = clock();
 
     // collect resolvent literals
     if ( p->fProofVerif )
@@ -990,7 +990,7 @@ void * Intb_ManInterpolate( Intb_Man_t * p, Sto_Man_t * pCnf, void * vVarsAB, in
     Aig_Obj_t * pObj;
     Sto_Cls_t * pClause;
     int RetValue = 1;
-    int clkTotal = clock();
+    clock_t clkTotal = clock();
 
     // check that the CNF makes sense
     assert( pCnf->nVars > 0 && pCnf->nClauses > 0 );
diff --git a/src/sat/bsat/satInterP.c b/src/sat/bsat/satInterP.c
index b8ab473a..2e3caeeb 100644
--- a/src/sat/bsat/satInterP.c
+++ b/src/sat/bsat/satInterP.c
@@ -22,7 +22,6 @@
 #include <stdlib.h>
 #include <string.h>
 #include <assert.h>
-#include <time.h>
 
 #include "satStore.h"
 #include "src/misc/vec/vec.h"
@@ -70,9 +69,9 @@ struct Intp_Man_t_
     int             nResLits;     // the number of literals of the resolvent
     int             nResLitsAlloc;// the number of literals of the resolvent
     // runtime stats
-    int             timeBcp;      // the runtime for BCP
-    int             timeTrace;    // the runtime of trace construction
-    int             timeTotal;    // the total runtime of interpolation
+    clock_t         timeBcp;      // the runtime for BCP
+    clock_t         timeTrace;    // the runtime of trace construction
+    clock_t         timeTotal;    // the total runtime of interpolation
 };
 
 // reading/writing the proof for a clause
@@ -420,7 +419,7 @@ Sto_Cls_t * Intp_ManPropagate( Intp_Man_t * p, int Start )
 {
     Sto_Cls_t * pClause;
     int i;
-    int clk = clock();
+    clock_t clk = clock();
     for ( i = Start; i < p->nTrailSize; i++ )
     {
         pClause = Intp_ManPropagateOne( p, p->pTrail[i] );
@@ -476,7 +475,7 @@ int Intp_ManProofTraceOne( Intp_Man_t * p, Sto_Cls_t * pConflict, Sto_Cls_t * pF
     Sto_Cls_t * pReason;
     int i, v, Var, PrevId;
     int fPrint = 0;
-    int clk = clock();
+    clock_t clk = clock();
 
     // collect resolvent literals
     if ( p->fProofVerif )
@@ -864,7 +863,8 @@ void Intp_ManUnsatCoreVerify( Sto_Man_t * pCnf, Vec_Int_t * vCore )
     sat_solver * pSat;
     Sto_Cls_t * pClause;
     Vec_Ptr_t * vClauses;
-    int i, iClause, RetValue, clk = clock();
+    int i, iClause, RetValue;
+    clock_t clk = clock();
     // collect the clauses
     vClauses = Vec_PtrAlloc( 1000 );
     Sto_ManForEachClauseRoot( pCnf, pClause )
@@ -962,7 +962,7 @@ void * Intp_ManUnsatCore( Intp_Man_t * p, Sto_Man_t * pCnf, int fVerbose )
     Vec_Int_t * vVisited;
     Sto_Cls_t * pClause;
     int RetValue = 1;
-    int clkTotal = clock();
+    clock_t clkTotal = clock();
 
     // check that the CNF makes sense
     assert( pCnf->nVars > 0 && pCnf->nClauses > 0 );
diff --git a/src/sat/bsat/satProof.c b/src/sat/bsat/satProof.c
index f56c20cc..f7e08592 100644
--- a/src/sat/bsat/satProof.c
+++ b/src/sat/bsat/satProof.c
@@ -145,7 +145,7 @@ Vec_Int_t * Proof_CollectUsedIter( Vec_Set_t * vProof, Vec_Int_t * vRoots, int f
 {
     int fVerify = 0;
     Vec_Int_t * vUsed, * vStack;
-    int clk = clock();
+    clock_t clk = clock();
     int i, Entry, iPrev = 0;
     vUsed = Vec_IntAlloc( 1000 );
     vStack = Vec_IntAlloc( 1000 );
@@ -309,8 +309,9 @@ void Sat_ProofReduce2( sat_solver2 * s )
     int fVerbose = 0;
     Vec_Int_t * vUsed;
     satset * pNode, * pFanin, * pPivot;
-    int i, k, hTemp, clk = clock();
-    static int TimeTotal = 0;
+    int i, k, hTemp;
+    clock_t clk = clock();
+    static clock_t TimeTotal = 0;
 
     // collect visited nodes
     vUsed = Proof_CollectUsedIter( vProof, vRoots, 1 );
@@ -371,8 +372,9 @@ void Sat_ProofReduce( sat_solver2 * s )
     int fVerbose = 0;
     Vec_Ptr_t * vUsed;
     satset * pNode, * pFanin, * pPivot;
-    int i, j, k, hTemp, nSize, clk = clock();
-    static int TimeTotal = 0;
+    int i, j, k, hTemp, nSize;
+    clock_t clk = clock();
+    static clock_t TimeTotal = 0;
 
     // collect visited nodes
     nSize = Proof_MarkUsedRec( vProof, vRoots );
@@ -525,7 +527,8 @@ void Sat_ProofCheck( sat_solver2 * s )
     Vec_Set_t * vResolves;
     Vec_Int_t * vUsed, * vTemp;
     satset * pSet, * pSet0 = NULL, * pSet1;
-    int i, k, hRoot, Handle, Counter = 0, clk = clock(); 
+    int i, k, hRoot, Handle, Counter = 0;
+    clock_t clk = clock(); 
     hRoot = s->hProofLast;
     if ( hRoot == -1 )
         return;
diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c
index 2d41e2fe..f143916a 100644
--- a/src/sat/bsat/satSolver.c
+++ b/src/sat/bsat/satSolver.c
@@ -1605,7 +1605,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 && time(NULL) > s->nRuntimeLimit )
+        if ( s->nRuntimeLimit && clock() > s->nRuntimeLimit )
             break;
         if (s->verbosity >= 1)
         {
@@ -1629,7 +1629,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 && time(NULL) > s->nRuntimeLimit )
+        if ( s->nRuntimeLimit && clock() > s->nRuntimeLimit )
             break;
     }
     if (s->verbosity >= 1)
diff --git a/src/sat/bsat/satSolver.h b/src/sat/bsat/satSolver.h
index 40f637ee..62ad5e0c 100644
--- a/src/sat/bsat/satSolver.h
+++ b/src/sat/bsat/satSolver.h
@@ -142,7 +142,7 @@ struct sat_solver_t
 
     ABC_INT64_T nConfLimit;    // external limit on the number of conflicts
     ABC_INT64_T nInsLimit;     // external limit on the number of implications
-    int         nRuntimeLimit; // external limit on runtime
+    clock_t     nRuntimeLimit; // external limit on runtime
 
     veci        act_vars;      // variables whose activity has changed
     double*     factors;       // the activity factors
@@ -198,9 +198,9 @@ static int sat_solver_final(sat_solver* s, int ** ppArray)
     return s->conf_final.size;
 }
 
-static int sat_solver_set_runtime_limit(sat_solver* s, int Limit)
+static clock_t sat_solver_set_runtime_limit(sat_solver* s, clock_t Limit)
 {
-    int nRuntimeLimit = s->nRuntimeLimit;
+    clock_t nRuntimeLimit = s->nRuntimeLimit;
     s->nRuntimeLimit = Limit;
     return nRuntimeLimit;
 }
diff --git a/src/sat/bsat/satSolver2.c b/src/sat/bsat/satSolver2.c
index 2e0a5f4a..cbe6bc52 100644
--- a/src/sat/bsat/satSolver2.c
+++ b/src/sat/bsat/satSolver2.c
@@ -1398,12 +1398,13 @@ void luby2_test()
 // updates clauses, watches, units, and proof
 void sat_solver2_reducedb(sat_solver2* s)
 {
-    static int TimeTotal = 0;
+    static clock_t TimeTotal = 0;
     satset * c, * pivot;
     cla h,* pArray,* pArray2;
     int * pPerm, * pClaAct, nClaAct, ActCutOff;
     int i, j, k, hTemp, hHandle, LastSize = 0;
-    int Counter, CounterStart, clk = clock();
+    int Counter, CounterStart;
+    clock_t clk = clock();
 
     // check if it is time to reduce
     if ( s->nLearntMax == 0 || s->stats.learnts < (unsigned)s->nLearntMax )
@@ -1845,7 +1846,7 @@ int sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLim
                 s->progress_estimate*100);
             fflush(stdout);
         }
-        if ( s->nRuntimeLimit && time(NULL) > s->nRuntimeLimit )
+        if ( s->nRuntimeLimit && clock() > s->nRuntimeLimit )
             break;
         // reduce the set of learnt clauses:
         sat_solver2_reducedb(s);
diff --git a/src/sat/bsat/satSolver2.h b/src/sat/bsat/satSolver2.h
index 79eb64ed..ffab91be 100644
--- a/src/sat/bsat/satSolver2.h
+++ b/src/sat/bsat/satSolver2.h
@@ -160,7 +160,7 @@ struct sat_solver2_t
     stats_t         stats;
     ABC_INT64_T     nConfLimit;     // external limit on the number of conflicts
     ABC_INT64_T     nInsLimit;      // external limit on the number of implications
-    int             nRuntimeLimit;  // external limit on runtime
+    clock_t         nRuntimeLimit;  // external limit on runtime
 };
 
 typedef struct satset_t satset;
@@ -240,9 +240,9 @@ static inline int sat_solver2_final(sat_solver2* s, int ** ppArray)
     return s->conf_final.size;
 }
 
-static inline int sat_solver2_set_runtime_limit(sat_solver2* s, int Limit)
+static inline clock_t sat_solver2_set_runtime_limit(sat_solver2* s, clock_t Limit)
 {
-    int temp = s->nRuntimeLimit;
+    clock_t temp = s->nRuntimeLimit;
     s->nRuntimeLimit = Limit;
     return temp;
 }
diff --git a/src/sat/bsat/satStore.c b/src/sat/bsat/satStore.c
index ac74c4a6..fab13666 100644
--- a/src/sat/bsat/satStore.c
+++ b/src/sat/bsat/satStore.c
@@ -22,7 +22,6 @@
 #include <stdlib.h>
 #include <string.h>
 #include <assert.h>
-#include <time.h>
 
 #include "satStore.h"