Fixing time primtouts throughout the code.

12 files changed, 32 insertions, 21 deletions

diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h
index 3c390a37..adad1837 100644
--- a/src/aig/aig/aig.h
+++ b/src/aig/aig/aig.h
@@ -30,7 +30,6 @@
 #include <stdlib.h>
 #include <string.h>
 #include <assert.h>
-#include <time.h>
 
 #include "src/misc/vec/vec.h"
 #include "src/misc/util/utilCex.h"
@@ -165,8 +164,8 @@ struct Aig_Man_t_
     Vec_Int_t *      vCiNumsOrig;    // original CI names
     int              nComplEdges;    // complemented edges
     // timing statistics
-    int              time1;
-    int              time2;
+    clock_t          time1;
+    clock_t          time2;
 };
 
 // cut computation
diff --git a/src/aig/aig/aigCuts.c b/src/aig/aig/aigCuts.c
index ed824fac..5e3bb93a 100644
--- a/src/aig/aig/aigCuts.c
+++ b/src/aig/aig/aigCuts.c
@@ -632,7 +632,8 @@ Aig_ManCut_t * Aig_ComputeCuts( Aig_Man_t * pAig, int nCutsMax, int nLeafMax, in
 {
     Aig_ManCut_t * p;
     Aig_Obj_t * pObj;
-    int i, clk = clock();
+    int i;
+    clock_t clk = clock();
     assert( pAig->pManCuts == NULL );
     // start the manager
     p = Aig_ManCutStart( pAig, nCutsMax, nLeafMax, fTruth, fVerbose );
diff --git a/src/aig/aig/aigDfs.c b/src/aig/aig/aigDfs.c
index ace723a2..b4b7862e 100644
--- a/src/aig/aig/aigDfs.c
+++ b/src/aig/aig/aigDfs.c
@@ -767,7 +767,8 @@ int Aig_SupportSize( Aig_Man_t * p, Aig_Obj_t * pObj )
 int Aig_SupportSizeTest( Aig_Man_t * p )
 {
     Aig_Obj_t * pObj;
-    int i, Counter = 0, clk = clock();
+    int i, Counter = 0;
+    clock_t clk = clock();
     Aig_ManForEachObj( p, pObj, i )
         if ( Aig_ObjIsNode(pObj) )
             Counter += (Aig_SupportSize(p, pObj) <= 16);
diff --git a/src/aig/aig/aigDoms.c b/src/aig/aig/aigDoms.c
index 00350304..fe9403b5 100644
--- a/src/aig/aig/aigDoms.c
+++ b/src/aig/aig/aigDoms.c
@@ -623,7 +623,8 @@ Aig_Sto_t * Aig_ManComputeDomsFlops( Aig_Man_t * pAig, int Limit )
     Aig_Sto_t * pSto;
     Vec_Ptr_t * vNodes;
     Aig_Obj_t * pObj;
-    int i, clk = clock();
+    int i;
+    clock_t clk = clock();
     pSto = Aig_ManDomStart( pAig, Limit );
     // initialize flop inputs
     Saig_ManForEachLi( pAig, pObj, i )
@@ -663,7 +664,8 @@ Aig_Sto_t * Aig_ManComputeDomsPis( Aig_Man_t * pAig, int Limit )
     Aig_Sto_t * pSto;
     Vec_Ptr_t * vNodes;
     Aig_Obj_t * pObj;
-    int i, clk = clock();
+    int i;
+    clock_t clk = clock();
     pSto = Aig_ManDomStart( pAig, Limit );
     // initialize flop inputs
     Aig_ManForEachCo( pAig, pObj, i )
@@ -703,7 +705,8 @@ Aig_Sto_t * Aig_ManComputeDomsNodes( Aig_Man_t * pAig, int Limit )
     Aig_Sto_t * pSto;
     Vec_Ptr_t * vNodes;
     Aig_Obj_t * pObj;
-    int i, clk = clock();
+    int i;
+    clock_t clk = clock();
     pSto = Aig_ManDomStart( pAig, Limit );
     // initialize flop inputs
     Aig_ManForEachCo( pAig, pObj, i )
diff --git a/src/aig/aig/aigInter.c b/src/aig/aig/aigInter.c
index fcf32236..6f183925 100644
--- a/src/aig/aig/aigInter.c
+++ b/src/aig/aig/aigInter.c
@@ -29,9 +29,9 @@ ABC_NAMESPACE_IMPL_START
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-extern int timeCnf;
-extern int timeSat;
-extern int timeInt;
+extern clock_t timeCnf;
+extern clock_t timeSat;
+extern clock_t timeInt;
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -156,7 +156,7 @@ Aig_Man_t * Aig_ManInter( Aig_Man_t * pManOn, Aig_Man_t * pManOff, int fRelation
     Vec_Int_t * vVarsAB;
     Aig_Obj_t * pObj, * pObj2;
     int Lits[3], status, i;
-    int clk;
+    clock_t clk;
     int iLast = -1; // Suppress "might be used uninitialized"
 
     assert( Aig_ManCiNum(pManOn) == Aig_ManCiNum(pManOff) );
diff --git a/src/aig/aig/aigJust.c b/src/aig/aig/aigJust.c
index 2c524c85..2ee60748 100644
--- a/src/aig/aig/aigJust.c
+++ b/src/aig/aig/aigJust.c
@@ -253,7 +253,9 @@ void Aig_ManJustExperiment( Aig_Man_t * pAig )
     Aig_ManPack_t * pPack;
     Vec_Int_t * vSuppLits, * vNodes;
     Aig_Obj_t * pObj;
-    int i, clk = clock(), Count0 = 0, Count0f = 0, Count1 = 0, Count1f = 0;
+    int i;
+    clock_t clk = clock();
+    int Count0 = 0, Count0f = 0, Count1 = 0, Count1f = 0;
     int nTotalLits = 0;
     vSuppLits = Vec_IntAlloc( 100 );
     pPack = Aig_ManPackStart( pAig );
diff --git a/src/aig/aig/aigPart.c b/src/aig/aig/aigPart.c
index 56d2fd3f..fdbba36a 100644
--- a/src/aig/aig/aigPart.c
+++ b/src/aig/aig/aigPart.c
@@ -688,7 +688,8 @@ Vec_Ptr_t * Aig_ManPartitionSmart( Aig_Man_t * p, int nSuppSizeLimit, int fVerbo
     Vec_Ptr_t * vPartSuppsBit;
     Vec_Ptr_t * vSupports, * vPartsAll, * vPartsAll2, * vPartSuppsAll;//, * vPartPtr;
     Vec_Int_t * vOne, * vPart, * vPartSupp, * vTemp;
-    int i, iPart, iOut, clk;
+    int i, iPart, iOut;
+    clock_t clk;
 
     // compute the supports for all outputs
 clk = clock();
@@ -812,7 +813,8 @@ Vec_Ptr_t * Aig_ManPartitionSmartRegisters( Aig_Man_t * pAig, int nSuppSizeLimit
     Vec_Ptr_t * vPartSuppsBit;
     Vec_Ptr_t * vSupports, * vPartsAll, * vPartsAll2, * vPartSuppsAll;
     Vec_Int_t * vOne, * vPart, * vPartSupp, * vTemp;
-    int i, iPart, iOut, clk;
+    int i, iPart, iOut;
+    clock_t clk;
 
     // add output number to each
 clk = clock();
diff --git a/src/aig/aig/aigPartSat.c b/src/aig/aig/aigPartSat.c
index 839a17ee..d187a19b 100644
--- a/src/aig/aig/aigPartSat.c
+++ b/src/aig/aig/aigPartSat.c
@@ -497,7 +497,8 @@ int Aig_ManPartitionedSat( Aig_Man_t * p, int nAlgo, int nPartSize,
     Aig_Man_t * pAig, * pTemp;
     Vec_Int_t * vNode2Part, * vNode2Var;
     int nConfRemaining = nConfTotal, nNodes = 0;
-    int i, clk, status, RetValue = -1;
+    int i, status, RetValue = -1;
+    clock_t clk;
 
     // perform partitioning according to the selected algorithm
     clk = clock();
diff --git a/src/aig/aig/aigRepar.c b/src/aig/aig/aigRepar.c
index 1b017346..7f9699fd 100644
--- a/src/aig/aig/aigRepar.c
+++ b/src/aig/aig/aigRepar.c
@@ -129,7 +129,7 @@ void Aig_ManInterTest( Aig_Man_t * pMan, int fVerbose )
     Cnf_Dat_t * pCnf;
     Aig_Obj_t * pObj;
     int Lit, Cid, Var, status, i;
-    int clk = clock();
+    clock_t clk = clock();
     assert( Aig_ManRegNum(pMan) == 0 );
     assert( Aig_ManCoNum(pMan) == 1 );
 
@@ -251,7 +251,7 @@ Aig_Man_t * Aig_ManInterRepar( Aig_Man_t * pMan, int fVerbose )
     int nOuts = Aig_ManCoNum(pMan);
     int ShiftP[2], ShiftCnf[2], ShiftOr[2], ShiftAssume;
     int Cid, Lit, status, i, k, c;
-    int clk = clock();
+    clock_t clk = clock();
     assert( Aig_ManRegNum(pMan) == 0 );
 
     // derive CNFs
diff --git a/src/aig/aig/aigRet.c b/src/aig/aig/aigRet.c
index 58a04fb0..1cf45ebe 100644
--- a/src/aig/aig/aigRet.c
+++ b/src/aig/aig/aigRet.c
@@ -839,7 +839,7 @@ Aig_Man_t * Rtm_ManRetime( Aig_Man_t * p, int fForward, int nStepsMax, int fVerb
     Rtm_Obj_t * pObj, * pNext;
     Aig_Obj_t * pObjAig;
     int i, k, nAutos, Degree, DegreeMax = 0; 
-    int clk;
+    clock_t clk;
 
     // create the retiming manager
 clk = clock();
diff --git a/src/aig/aig/aigSplit.c b/src/aig/aig/aigSplit.c
index f187860f..50f96a81 100644
--- a/src/aig/aig/aigSplit.c
+++ b/src/aig/aig/aigSplit.c
@@ -258,7 +258,8 @@ Aig_Man_t * Aig_ManSplit( Aig_Man_t * p, int nVars, int fVerbose )
     DdNode * bFunc;
     DdManager * dd;
     Vec_Ptr_t * vSupp, * vSubs, * vCofs;
-    int i, clk = clock();
+    int i;
+    clock_t clk = clock();
     if ( Saig_ManPoNum(p) != 1 )
     {
         printf( "Currently works only for one primary output.\n" );
diff --git a/src/aig/aig/aigTable.c b/src/aig/aig/aigTable.c
index ec2531c7..abd9960a 100644
--- a/src/aig/aig/aigTable.c
+++ b/src/aig/aig/aigTable.c
@@ -70,7 +70,8 @@ void Aig_TableResize( Aig_Man_t * p )
 {
     Aig_Obj_t * pEntry, * pNext;
     Aig_Obj_t ** pTableOld, ** ppPlace;
-    int nTableSizeOld, Counter, i, clk;
+    int nTableSizeOld, Counter, i;
+    clock_t clk;
     assert( p->pTable != NULL );
 clk = clock();
     // save the old table