Fixing time primtouts throughout the code.

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

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 );

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);

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 )

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) );

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 );

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();

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();

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

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();

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" );

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

src/aig/gia/gia.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"

src/aig/gia/giaAbsGla.c

@@ -800,13 +800,10 @@ Vec_Int_t * Gla_ManRefinement( Gla_Man_t * p )
 
     // select objects
     vSelect = Vec_IntAlloc( 100 );
-//    Vec_IntFill( p->vPrioSels, Vec_IntSize(vPPis)+1, 0 );
     Vec_IntFill( p->vObjCounts, p->pPars->iFrame+1, 0 );
     Gla_ManRefSelect_rec( p, Gia_ObjFanin0(Gia_ManPo(p->pGia, 0)), p->pPars->iFrame, vSelect, Sign );
     Vec_IntUniqify( vSelect );
 
-//    printf( "\nSelected %d.\n", Vec_IntSize(vSelect) );
-
 /*
     for ( f = 0; f < p->pPars->iFrame; f++ )
         printf( "%2d", Vec_IntEntry(p->vObjCounts, f) );
@@ -976,7 +973,6 @@ Gla_Man_t * Gla_ManStart( Gia_Man_t * pGia0, Gia_ParVta_t * pPars )
     p->pGia = Gia_ManDupMapped( pGia0, p->pCnf->vMapping );
     if ( pPars->fPropFanout )
         Gia_ManStaticFanoutStart( p->pGia );
-//printf( "Old GIA = %d.  New GIA = %d.\n", Gia_ManObjNum(pGia0), Gia_ManObjNum(p->pGia) );
 
     // derive new gate map
     assert( pGia0->vGateClasses != 0 );
@@ -1797,7 +1793,7 @@ int Gia_GlaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars, int fStartVta )
     p->timeInit = clock() - clk;
     // set runtime limit
     if ( p->pPars->nTimeOut )
-        sat_solver2_set_runtime_limit( p->pSat, time(NULL) + p->pPars->nTimeOut - 1 );
+        sat_solver2_set_runtime_limit( p->pSat, p->pPars->nTimeOut * CLOCKS_PER_SEC + clock() );
     // perform initial abstraction
     if ( p->pPars->fVerbose )
     {
@@ -1831,9 +1827,9 @@ int Gia_GlaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars, int fStartVta )
                 goto finish;
             }
             // check timeout
-            if ( p->pSat->nRuntimeLimit && time(NULL) > p->pSat->nRuntimeLimit )
+            if ( p->pSat->nRuntimeLimit && clock() > p->pSat->nRuntimeLimit )
             {
-                Gla_ManRollBack( p ); // 1155046
+                Gla_ManRollBack( p );
                 goto finish;
             }
             if ( vCore != NULL )
@@ -1960,7 +1956,7 @@ int Gia_GlaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars, int fStartVta )
         pAig->vGateClasses = Gla_ManTranslate( p );
         if ( Status == -1 )
         {
-            if ( p->pPars->nTimeOut && time(NULL) >= p->pSat->nRuntimeLimit ) 
+            if ( p->pPars->nTimeOut && clock() >= p->pSat->nRuntimeLimit ) 
                 Abc_Print( 1, "SAT solver ran out of time at %d sec in frame %d.  ", p->pPars->nTimeOut, f );
             else if ( pPars->nConfLimit && sat_solver2_nconflicts(p->pSat) >= pPars->nConfLimit )
                 Abc_Print( 1, "SAT solver ran out of resources at %d conflicts in frame %d.  ", pPars->nConfLimit, f );

src/aig/gia/giaAbsVta.c

@@ -1564,7 +1564,7 @@ int Gia_VtaPerformInt( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
     p = Vga_ManStart( pAig, pPars );
     // set runtime limit
     if ( p->pPars->nTimeOut )
-        sat_solver2_set_runtime_limit( p->pSat, time(NULL) + p->pPars->nTimeOut - 1 );
+        sat_solver2_set_runtime_limit( p->pSat, p->pPars->nTimeOut * CLOCKS_PER_SEC + clock() );
     // perform initial abstraction
     if ( p->pPars->fVerbose )
     {
@@ -1609,7 +1609,7 @@ int Gia_VtaPerformInt( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
                 goto finish;
             }
             // check timeout
-            if ( p->pSat->nRuntimeLimit && time(NULL) > p->pSat->nRuntimeLimit )
+            if ( p->pSat->nRuntimeLimit && clock() > p->pSat->nRuntimeLimit )
             {
                 Vga_ManRollBack( p, nObjOld );
                 goto finish;
@@ -1716,7 +1716,7 @@ int Gia_VtaPerformInt( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
             pAig->vObjClasses = Gia_VtaFramesToAbs( (Vec_Vec_t *)p->vCores );
             if ( Status == -1 )
             {
-                if ( p->pPars->nTimeOut && time(NULL) >= p->pSat->nRuntimeLimit ) 
+                if ( p->pPars->nTimeOut && clock() >= p->pSat->nRuntimeLimit ) 
                     Abc_Print( 1, "SAT solver ran out of time at %d sec in frame %d.  ", p->pPars->nTimeOut, f );
                 else if ( pPars->nConfLimit && sat_solver2_nconflicts(p->pSat) >= pPars->nConfLimit )
                     Abc_Print( 1, "SAT solver ran out of resources at %d conflicts in frame %d.  ", pPars->nConfLimit, f );

src/aig/gia/giaCCof.c

@@ -219,8 +219,9 @@ int Gia_ManCofOneDerive( Ccf_Man_t * p, int LitProp )
 ***********************************************************************/
 int Gia_ManCofGetReachable( Ccf_Man_t * p, int Lit )
 {
-    int ObjPrev = 0, ConfPrev = 0, clk;
+    int ObjPrev = 0, ConfPrev = 0;
     int Count = 0, LitOut, RetValue;
+    clock_t clk;
     // try solving for the first time and quit if converged
     RetValue = sat_solver_solve( p->pSat, &Lit, &Lit + 1, p->nConfMax, 0, 0, 0 );
     if ( RetValue == l_False )
@@ -268,8 +269,8 @@ Gia_Man_t * Gia_ManCofTest( Gia_Man_t * pGia, int nFrameMax, int nConfMax, int n
     Ccf_Man_t * p;
     Gia_Obj_t * pObj;
     int f, i, Lit, RetValue = -1, fFailed = 0;
-    int nTimeToStop = time(NULL) + nTimeMax;
-    int clk = clock();
+    clock_t nTimeToStop = clock() + nTimeMax * CLOCKS_PER_SEC;
+    clock_t clk = clock();
     assert( Gia_ManPoNum(pGia) == 1 );
 
     // create reachability manager
@@ -309,7 +310,7 @@ Gia_Man_t * Gia_ManCofTest( Gia_Man_t * pGia, int nFrameMax, int nConfMax, int n
     }
 
     // report the result
-    if ( nTimeToStop && time(NULL) > nTimeToStop )
+    if ( nTimeToStop && clock() > nTimeToStop )
         printf( "Runtime limit (%d sec) is reached after %d frames.  ", nTimeMax, f );
     else if ( f == nFrameMax )
         printf( "Completed %d frames without converging.  ", f );

src/aig/gia/giaCSat.c

@@ -81,10 +81,10 @@ struct Cbs_Man_t_
     int           nConfSat;     // conflicts in sat problems
     int           nConfUndec;   // conflicts in undec problems
     // runtime stats
-    int           timeSatUnsat; // unsat
-    int           timeSatSat;   // sat
-    int           timeSatUndec; // undecided
-    int           timeTotal;    // total runtime
+    clock_t       timeSatUnsat; // unsat
+    clock_t       timeSatSat;   // sat
+    clock_t       timeSatUndec; // undecided
+    clock_t       timeTotal;    // total runtime
 };
 
 static inline int   Cbs_VarIsAssigned( Gia_Obj_t * pVar )      { return pVar->fMark0;                        }
@@ -1003,7 +1003,8 @@ Vec_Int_t * Cbs_ManSolveMiterNc( Gia_Man_t * pAig, int nConfs, Vec_Str_t ** pvSt
     Vec_Int_t * vCex, * vVisit, * vCexStore;
     Vec_Str_t * vStatus;
     Gia_Obj_t * pRoot; 
-    int i, status, clk, clkTotal = clock();
+    int i, status;
+    clock_t clk, clkTotal = clock();
     assert( Gia_ManRegNum(pAig) == 0 );
 //    Gia_ManCollectTest( pAig );
     // prepare AIG

src/aig/gia/giaCSatOld.c

@@ -73,10 +73,10 @@ struct Cbs0_Man_t_
     int           nConfSat;     // conflicts in sat problems
     int           nConfUndec;   // conflicts in undec problems
     // runtime stats
-    int           timeSatUnsat; // unsat
-    int           timeSatSat;   // sat
-    int           timeSatUndec; // undecided
-    int           timeTotal;    // total runtime
+    clock_t       timeSatUnsat; // unsat
+    clock_t       timeSatSat;   // sat
+    clock_t       timeSatUndec; // undecided
+    clock_t       timeTotal;    // total runtime
 };
 
 static inline int   Cbs0_VarIsAssigned( Gia_Obj_t * pVar )      { return pVar->fMark0;                        }
@@ -712,7 +712,8 @@ Vec_Int_t * Cbs_ManSolveMiter( Gia_Man_t * pAig, int nConfs, Vec_Str_t ** pvStat
     Vec_Int_t * vCex, * vVisit, * vCexStore;
     Vec_Str_t * vStatus;
     Gia_Obj_t * pRoot; 
-    int i, status, clk, clkTotal = clock();
+    int i, status;
+    clock_t clk, clkTotal = clock();
     assert( Gia_ManRegNum(pAig) == 0 );
     // prepare AIG
     Gia_ManCreateRefs( pAig );

src/aig/gia/giaCTas.c

@@ -108,10 +108,10 @@ struct Tas_Man_t_
     int           nConfSat;     // conflicts in sat problems
     int           nConfUndec;   // conflicts in undec problems
     // runtime stats
-    int           timeSatUnsat; // unsat
-    int           timeSatSat;   // sat
-    int           timeSatUndec; // undecided
-    int           timeTotal;    // total runtime
+    clock_t       timeSatUnsat; // unsat
+    clock_t       timeSatSat;   // sat
+    clock_t       timeSatUndec; // undecided
+    clock_t       timeTotal;    // total runtime
 };
 
 static inline int   Tas_VarIsAssigned( Gia_Obj_t * pVar )      { return pVar->fMark0;                        }
@@ -1524,7 +1524,8 @@ Vec_Int_t * Tas_ManSolveMiterNc( Gia_Man_t * pAig, int nConfs, Vec_Str_t ** pvSt
     Gia_Obj_t * pRoot;//, * pRootCopy; 
 //    Gia_Man_t * pAigCopy = Gia_ManDup( pAig ), * pAigTemp;
 
-    int i, status, clk, clkTotal = clock();
+    int i, status;
+    clock_t clk, clkTotal = clock();
     assert( Gia_ManRegNum(pAig) == 0 );
 //    Gia_ManCollectTest( pAig );
     // prepare AIG
@@ -1703,7 +1704,8 @@ void Tas_ManSolveMiterNc2( Gia_Man_t * pAig, int nConfs, Gia_Man_t * pAigOld, Ve
     Vec_Int_t * vCex, * vVisit, * vCexStore;
     Vec_Str_t * vStatus;
     Gia_Obj_t * pRoot, * pOldRoot; 
-    int i, status, clk, clkTotal = clock();
+    int i, status;
+    clock_t clk, clkTotal = clock();
     int Tried = 0, Stored = 0, Step = Gia_ManCoNum(pAig) / nPatMax;
     assert( Gia_ManRegNum(pAig) == 0 );
 //    Gia_ManCollectTest( pAig );

src/aig/gia/giaCTas2.c

@@ -115,10 +115,10 @@ struct Tas_Man_t_
     int           nConfUndec;   // conflicts in undec problems
     int           nConfTotal;   // total conflicts
     // runtime stats
-    int           timeSatUnsat; // unsat
-    int           timeSatSat;   // sat
-    int           timeSatUndec; // undecided
-    int           timeTotal;    // total runtime
+    clock_t       timeSatUnsat; // unsat
+    clock_t       timeSatSat;   // sat
+    clock_t       timeSatUndec; // undecided
+    clock_t       timeTotal;    // total runtime
 };
 
 static inline int         Tas_VarIsAssigned( Tas_Var_t * pVar )        { return pVar->fAssign;                                      }