Fixing time primtouts throughout the code.

11 files changed, 16 insertions, 17 deletions

diff --git a/src/bdd/cas/casCore.c b/src/bdd/cas/casCore.c
index b73b5b3f..66d11082 100644
--- a/src/bdd/cas/casCore.c
+++ b/src/bdd/cas/casCore.c
@@ -21,7 +21,6 @@
 #include <stdio.h>
 #include <stdlib.h>
 #include <string.h>
-#include <time.h>
 
 #include "src/base/main/main.h"
 #include "src/base/cmd/cmd.h"
@@ -82,7 +81,7 @@ int Abc_CascadeExperiment( char * pFileGeneric, DdManager * dd, DdNode ** pOutpu
     int i;
     int nVars = nInputs;
     int nOuts = nOutputs;
-    long clk1;
+    clock_t clk1;
 
     int      nVarsEnc;              // the number of additional variables to encode outputs
     DdNode * pbVarsEnc[MAXOUTPUTS]; // the BDDs of the encoding vars
@@ -955,7 +954,7 @@ void WriteDDintoBLIFfileReorder( DdManager * dd, FILE * pFile, DdNode * Func, ch
 
     ///////////////////////////////////////////////////////////////
     DdNode * bFmin;
-    int clk1;
+    clock_t clk1;
 
     if ( s_ddmin == NULL )
         s_ddmin = Cudd_Init( dd->size, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0);
diff --git a/src/bdd/cas/casDec.c b/src/bdd/cas/casDec.c
index ea132540..794f6fd3 100644
--- a/src/bdd/cas/casDec.c
+++ b/src/bdd/cas/casDec.c
@@ -21,7 +21,6 @@
 #include <stdio.h>
 #include <string.h>
 #include <stdlib.h>
-#include <time.h>
 
 #include "src/misc/extra/extraBdd.h"
 #include "cas.h"
@@ -129,7 +128,7 @@ int CreateDecomposedNetwork( DdManager * dd, DdNode * aFunc, char ** pNames, int
     int nLutOutputs = 0;
     int nLutOutputsOrig = 0;
 
-    long clk1;
+    clock_t clk1;
 
     s_LutSize = nLutSize;
 
@@ -285,7 +284,7 @@ int CreateDecomposedNetwork( DdManager * dd, DdNode * aFunc, char ** pNames, int
         }
         else
         {
-            long clk2 = clock();
+            clock_t clk2 = 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;
diff --git a/src/bdd/cudd/cuddAndAbs.c b/src/bdd/cudd/cuddAndAbs.c
index 00ba67b4..0db3e4e4 100644
--- a/src/bdd/cudd/cuddAndAbs.c
+++ b/src/bdd/cudd/cuddAndAbs.c
@@ -259,7 +259,7 @@ cuddBddAndAbstractRecur(
         }
     }
 
-    if ( manager->TimeStop && manager->TimeStop < time(NULL) )
+    if ( manager->TimeStop && clock() > manager->TimeStop )
         return NULL;
 
     if (topf == top) {
diff --git a/src/bdd/cudd/cuddBddIte.c b/src/bdd/cudd/cuddBddIte.c
index 18ebee20..43dbcd60 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 && manager->TimeStop < time(NULL) )
+    if ( manager->TimeStop && 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 75a5fa2a..cedf920b 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 && ddS->TimeStop < time(NULL) )
+    if ( ddS->TimeStop && clock() > ddS->TimeStop )
         return NULL;
-    if ( ddD->TimeStop && ddD->TimeStop < time(NULL) )
+    if ( ddD->TimeStop && clock() > ddD->TimeStop )
         return NULL;
     
     /* Recursive step. */
diff --git a/src/bdd/cudd/cuddCompose.c b/src/bdd/cudd/cuddCompose.c
index 6264513f..d88491b0 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 && manager->TimeStop < time(NULL) )
+    if ( manager->TimeStop && 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 3d4b3db9..6e32acd2 100644
--- a/src/bdd/cudd/cuddInt.h
+++ b/src/bdd/cudd/cuddInt.h
@@ -481,7 +481,7 @@ struct DdManager {      /* specialized DD symbol table */
 #endif
     DdNode * bFunc;
     DdNode * bFunc2;
-    int TimeStop;           /* timeout for reordering */
+    clock_t TimeStop;           /* timeout for reordering */
 };
 
 typedef struct Move {
diff --git a/src/bdd/cudd/cuddSymmetry.c b/src/bdd/cudd/cuddSymmetry.c
index dfdc6c85..d2269a36 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 && table->TimeStop < time(NULL) )
+        if ( table->TimeStop && 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 7171315c..291648b3 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;
-    long clk;
+    clock_t clk;
     Dsd_Node_t * pTemp;
     int SumMaxGateSize = 0;
     int nDecOutputs = 0;
@@ -156,7 +156,7 @@ s_Loops2Useless = 0;
         int nCascades;
         int MaxBlock;
         int nPrimeBlocks;
-        long clk;
+        clock_t clk;
 
         clk = clock();
         nLiteralsPrev     = s_nLiterals;
diff --git a/src/bdd/reo/reoShuffle.c b/src/bdd/reo/reoShuffle.c
index 8d43cb3b..86aab4b9 100644
--- a/src/bdd/reo/reoShuffle.c
+++ b/src/bdd/reo/reoShuffle.c
@@ -161,7 +161,8 @@ void Extra_ShuffleTest( reo_man * pReo, DdManager * dd, DdNode * Func )
 //    extern int runtime1, runtime2;
 
     DdNode * Temp, * bRemap;
-    int nSuppSize, OffSet, Num, i, clk;
+    int nSuppSize, OffSet, Num, i;
+    clock_t clk;
     int pOrder[1000], pOrderInv[1000];
     assert( dd->size < 1000 );
 
diff --git a/src/bdd/reo/reoTest.c b/src/bdd/reo/reoTest.c
index f59da1a7..1e5fa1e0 100644
--- a/src/bdd/reo/reoTest.c
+++ b/src/bdd/reo/reoTest.c
@@ -222,7 +222,7 @@ int Extra_addReorderTest( DdManager * dd, DdNode * aF )
     DdNode * aFmin;
     int  nNodesBeg;
     int  nNodesEnd;
-    int clk1;
+    clock_t clk1;
 
     if ( s_ddmin == NULL )
         s_ddmin = Cudd_Init( dd->size, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0);