Fixing time primtouts throughout the code.

11 files changed, 54 insertions, 40 deletions

diff --git a/src/proof/cec/cecCec.c b/src/proof/cec/cecCec.c
index b9b3e1f1..841b6a0b 100644
--- a/src/proof/cec/cecCec.c
+++ b/src/proof/cec/cecCec.c
@@ -72,7 +72,8 @@ int Cec_ManVerifyOld( Gia_Man_t * pMiter, int fVerbose, int * piOutFail )
     extern int Ssw_SecCexResimulate( Aig_Man_t * p, int * pModel, int * pnOutputs );
     Gia_Man_t * pTemp = Gia_ManTransformMiter( pMiter );
     Aig_Man_t * pMiterCec = Gia_ManToAig( pTemp, 0 );
-    int RetValue, iOut, nOuts, clkTotal = clock();
+    int RetValue, iOut, nOuts;
+    clock_t clkTotal = clock();
     if ( piOutFail )
         *piOutFail = -1;
     Gia_ManStop( pTemp );
@@ -134,7 +135,8 @@ int Cec_ManHandleSpecialCases( Gia_Man_t * p, Cec_ParCec_t * pPars )
 {
     Gia_Obj_t * pObj1, * pObj2;
     Gia_Obj_t * pDri1, * pDri2;
-    int i, clk = clock();
+    int i;
+    clock_t clk = clock();
     Gia_ManSetPhase( p );
     Gia_ManForEachPo( p, pObj1, i )
     {
@@ -206,8 +208,9 @@ int Cec_ManVerify( Gia_Man_t * pInit, Cec_ParCec_t * pPars )
     int fDumpUndecided = 0;
     Cec_ParFra_t ParsFra, * pParsFra = &ParsFra;
     Gia_Man_t * p, * pNew;
-    int RetValue, clk = clock();
-    double clkTotal = clock();
+    int RetValue;
+    clock_t clk = clock();
+    clock_t clkTotal = clock();
     // consider special cases:
     // 1) (SAT) a pair of POs have different value under all-0 pattern
     // 2) (SAT) a pair of POs has different PI/Const drivers
@@ -263,7 +266,7 @@ int Cec_ManVerify( Gia_Man_t * pInit, Cec_ParCec_t * pPars )
         Gia_WriteAiger( pNew, "gia_cec_undecided.aig", 0, 0 );
         Abc_Print( 1, "The result is written into file \"%s\".\n", "gia_cec_undecided.aig" );
     }
-    if ( pPars->TimeLimit && ((double)clock() - clkTotal)/CLOCKS_PER_SEC >= pPars->TimeLimit )
+    if ( pPars->TimeLimit && (clock() - clkTotal)/CLOCKS_PER_SEC >= pPars->TimeLimit )
     {
         Gia_ManStop( pNew );
         return -1;
diff --git a/src/proof/cec/cecChoice.c b/src/proof/cec/cecChoice.c
index 3ddb975e..05b372f8 100644
--- a/src/proof/cec/cecChoice.c
+++ b/src/proof/cec/cecChoice.c
@@ -208,8 +208,8 @@ int Cec_ManChoiceComputation_int( Gia_Man_t * pAig, Cec_ParChc_t * pPars )
     Cec_ManSim_t * pSim;
     Gia_Man_t * pSrm;
     int r, RetValue;
-    int clkSat = 0, clkSim = 0, clkSrm = 0, clkTotal = clock();
-    int clk2, clk = clock();
+    clock_t clkSat = 0, clkSim = 0, clkSrm = 0, clkTotal = clock();
+    clock_t clk2, clk = clock();
     ABC_FREE( pAig->pReprs );
     ABC_FREE( pAig->pNexts );
     Gia_ManRandom( 1 );
diff --git a/src/proof/cec/cecCore.c b/src/proof/cec/cecCore.c
index 65c4b970..71519323 100644
--- a/src/proof/cec/cecCore.c
+++ b/src/proof/cec/cecCore.c
@@ -257,7 +257,8 @@ Gia_Man_t * Cec_ManSatSolving( Gia_Man_t * pAig, Cec_ParSat_t * pPars )
 int Cec_ManSimulationOne( Gia_Man_t * pAig, Cec_ParSim_t * pPars )
 {
     Cec_ManSim_t * pSim;
-    int RetValue = 0, clkTotal = clock();
+    int RetValue = 0;
+    clock_t clkTotal = clock();
     pSim = Cec_ManSimStart( pAig, pPars );
     if ( (pAig->pReprs == NULL && (RetValue = Cec_ManSimClassesPrepare( pSim, -1 ))) ||
          (RetValue == 0 &&        (RetValue = Cec_ManSimClassesRefine( pSim ))) )
@@ -342,8 +343,8 @@ Gia_Man_t * Cec_ManSatSweeping( Gia_Man_t * pAig, Cec_ParFra_t * pPars )
     Cec_ManFra_t * p;
     Cec_ManSim_t * pSim;
     Cec_ManPat_t * pPat;
-    int i, fTimeOut = 0, nMatches = 0, clk, clk2;
-    double clkTotal = clock();
+    int i, fTimeOut = 0, nMatches = 0;
+    clock_t clk, clk2, clkTotal = clock();
 
     // duplicate AIG and transfer equivalence classes
     Gia_ManRandom( 1 );
@@ -457,7 +458,7 @@ p->timeSat += clock() - clk;
             break;
         }
         // check resource limits
-        if ( p->pPars->TimeLimit && ((double)clock() - clkTotal)/CLOCKS_PER_SEC >= p->pPars->TimeLimit )
+        if ( p->pPars->TimeLimit && (clock() - clkTotal)/CLOCKS_PER_SEC >= p->pPars->TimeLimit )
         {
             fTimeOut = 1;
             break;
diff --git a/src/proof/cec/cecCorr.c b/src/proof/cec/cecCorr.c
index d080dfea..e8b25b48 100644
--- a/src/proof/cec/cecCorr.c
+++ b/src/proof/cec/cecCorr.c
@@ -719,7 +719,7 @@ Gia_Man_t * Gia_ManCorrReduce( Gia_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-void Cec_ManRefinedClassPrintStats( Gia_Man_t * p, Vec_Str_t * vStatus, int iIter, int Time )
+void Cec_ManRefinedClassPrintStats( Gia_Man_t * p, Vec_Str_t * vStatus, int iIter, clock_t Time )
 { 
     int nLits, CounterX = 0, Counter0 = 0, Counter = 0;
     int i, Entry, nProve = 0, nDispr = 0, nFail = 0;
@@ -789,7 +789,7 @@ void Cec_ManLSCorrespondenceBmc( Gia_Man_t * pAig, Cec_ParCor_t * pPars, int nPr
     fChanges = 1;
     while ( fChanges )
     {
-        int clkBmc = clock();
+        clock_t clkBmc = clock();
         fChanges = 0;
         pSrm = Gia_ManCorrSpecReduceInit( pAig, pPars->nFrames, nPrefs, !pPars->fLatchCorr, &vOutputs, pPars->fUseRings );
         if ( Gia_ManPoNum(pSrm) == 0 )
@@ -844,9 +844,10 @@ int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
     Cec_ParSat_t ParsSat, * pParsSat = &ParsSat;
     Cec_ManSim_t * pSim;
     Gia_Man_t * pSrm;
-    int r, RetValue, clkTotal = clock();
-    int clkSat = 0, clkSim = 0, clkSrm = 0;
-    int clk2, clk = clock();
+    int r, RetValue;
+    clock_t clkTotal = clock();
+    clock_t clkSat = 0, clkSim = 0, clkSrm = 0;
+    clock_t clk2, clk = clock();
     if ( Gia_ManRegNum(pAig) == 0 )
     {
         Abc_Print( 1, "Cec_ManLatchCorrespondence(): Not a sequential AIG.\n" );
diff --git a/src/proof/cec/cecCorr_updated.c b/src/proof/cec/cecCorr_updated.c
index 1db30705..3bea8dbf 100644
--- a/src/proof/cec/cecCorr_updated.c
+++ b/src/proof/cec/cecCorr_updated.c
@@ -728,7 +728,7 @@ Gia_Man_t * Gia_ManCorrReduce( Gia_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-void Cec_ManRefinedClassPrintStats( Gia_Man_t * p, Vec_Str_t * vStatus, int iIter, int Time )
+void Cec_ManRefinedClassPrintStats( Gia_Man_t * p, Vec_Str_t * vStatus, int iIter, clock_t Time )
 { 
     int nLits, CounterX = 0, Counter0 = 0, Counter = 0;
     int i, Entry, nProve = 0, nDispr = 0, nFail = 0;
diff --git a/src/proof/cec/cecInt.h b/src/proof/cec/cecInt.h
index 371dedda..8d9fe472 100644
--- a/src/proof/cec/cecInt.h
+++ b/src/proof/cec/cecInt.h
@@ -61,13 +61,13 @@ struct Cec_ManPat_t_
     int              nSeries;        // simulation series
     int              fVerbose;       // verbose stats
     // runtime statistics
-    int              timeFind;       // detecting the pattern  
-    int              timeShrink;     // minimizing the pattern
-    int              timeVerify;     // verifying the result of minimisation
-    int              timeSort;       // sorting literals 
-    int              timePack;       // packing into sim info structures 
-    int              timeTotal;      // total runtime  
-    int              timeTotalSave;  // total runtime for saving  
+    clock_t          timeFind;       // detecting the pattern  
+    clock_t          timeShrink;     // minimizing the pattern
+    clock_t          timeVerify;     // verifying the result of minimisation
+    clock_t          timeSort;       // sorting literals 
+    clock_t          timePack;       // packing into sim info structures 
+    clock_t          timeTotal;      // total runtime  
+    clock_t          timeTotalSave;  // total runtime for saving  
 };
 
 // SAT solving manager
@@ -154,10 +154,10 @@ struct Cec_ManFra_t_
     int              nAllDisproved;  // total number of disproved nodes
     int              nAllFailed;     // total number of failed nodes
     // runtime stats
-    int              timeSim;        // unsat
-    int              timePat;        // unsat
-    int              timeSat;        // sat
-    int              timeTotal;      // total runtime
+    clock_t          timeSim;        // unsat
+    clock_t          timePat;        // unsat
+    clock_t          timeSat;        // sat
+    clock_t          timeTotal;      // total runtime
 };
 
 ////////////////////////////////////////////////////////////////////////
@@ -169,7 +169,7 @@ struct Cec_ManFra_t_
 ////////////////////////////////////////////////////////////////////////
 
 /*=== cecCorr.c ============================================================*/
-extern void                 Cec_ManRefinedClassPrintStats( Gia_Man_t * p, Vec_Str_t * vStatus, int iIter, int Time );
+extern void                 Cec_ManRefinedClassPrintStats( Gia_Man_t * p, Vec_Str_t * vStatus, int iIter, clock_t Time );
 /*=== cecClass.c ============================================================*/
 extern int                  Cec_ManSimClassRemoveOne( Cec_ManSim_t * p, int i );
 extern int                  Cec_ManSimClassesPrepare( Cec_ManSim_t * p, int LevelMax );
diff --git a/src/proof/cec/cecPat.c b/src/proof/cec/cecPat.c
index cb1dae46..f372f3bb 100644
--- a/src/proof/cec/cecPat.c
+++ b/src/proof/cec/cecPat.c
@@ -359,7 +359,8 @@ void Cec_ManPatCleanMark0( Gia_Man_t * p, Gia_Obj_t * pObj )
 void Cec_ManPatSavePattern( Cec_ManPat_t * pMan, Cec_ManSat_t *  p, Gia_Obj_t * pObj )
 {
     Vec_Int_t * vPat;
-    int nPatLits, clk, clkTotal = clock();
+    int nPatLits;
+    clock_t clk, clkTotal = clock();
     assert( Gia_ObjIsCo(pObj) );
     pMan->nPats++;
     pMan->nPatsAll++;
@@ -451,7 +452,7 @@ Vec_Ptr_t * Cec_ManPatCollectPatterns( Cec_ManPat_t *  pMan, int nInputs, int nW
     int iStartOld = pMan->iStart;
     int nWords = nWordsInit;
     int nBits = 32 * nWords;
-    int clk = clock();
+    clock_t clk = clock();
     vInfo = Vec_PtrAllocSimInfo( nInputs, nWords );
     Gia_ManRandomInfo( vInfo, 0, 0, nWords );
     vPres = Vec_PtrAllocSimInfo( nInputs, nWords );
diff --git a/src/proof/cec/cecSeq.c b/src/proof/cec/cecSeq.c
index 2ccbe524..3afbd1c8 100644
--- a/src/proof/cec/cecSeq.c
+++ b/src/proof/cec/cecSeq.c
@@ -215,7 +215,8 @@ int Cec_ManSeqResimulateInfo( Gia_Man_t * pAig, Vec_Ptr_t * vSimInfo, Abc_Cex_t
 int Cec_ManSeqResimulateCounter( Gia_Man_t * pAig, Cec_ParSim_t * pPars, Abc_Cex_t * pCex )
 {
     Vec_Ptr_t * vSimInfo;
-    int RetValue, clkTotal = clock();
+    int RetValue;
+    clock_t clkTotal = clock();
     if ( pCex == NULL )
     {
         Abc_Print( 1, "Cec_ManSeqResimulateCounter(): Counter-example is not available.\n" );
diff --git a/src/proof/cec/cecSolve.c b/src/proof/cec/cecSolve.c
index e779e68c..5e108ae5 100644
--- a/src/proof/cec/cecSolve.c
+++ b/src/proof/cec/cecSolve.c
@@ -471,7 +471,8 @@ int Cec_ManSatCheckNode( Cec_ManSat_t * p, Gia_Obj_t * pObj )
 {
     Gia_Obj_t * pObjR = Gia_Regular(pObj);
     int nBTLimit = p->pPars->nBTLimit;
-    int Lit, RetValue, status, clk, clk2, nConflicts;
+    int Lit, RetValue, status, nConflicts;
+    clock_t clk, clk2;
 
     if ( pObj == Gia_ManConst0(p->pAig) )
         return 1;
@@ -570,7 +571,8 @@ int Cec_ManSatCheckNodeTwo( Cec_ManSat_t * p, Gia_Obj_t * pObj1, Gia_Obj_t * pOb
     Gia_Obj_t * pObjR1 = Gia_Regular(pObj1);
     Gia_Obj_t * pObjR2 = Gia_Regular(pObj2);
     int nBTLimit = p->pPars->nBTLimit;
-    int Lits[2], RetValue, status, clk, clk2, nConflicts;
+    int Lits[2], RetValue, status, nConflicts;
+    clock_t clk, clk2;
 
     if ( pObj1 == Gia_ManConst0(p->pAig) || pObj2 == Gia_ManConst0(p->pAig) || pObj1 == Gia_Not(pObj2) )
         return 1;
@@ -676,7 +678,8 @@ void Cec_ManSatSolve( Cec_ManPat_t * pPat, Gia_Man_t * pAig, Cec_ParSat_t * pPar
     Bar_Progress_t * pProgress = NULL;
     Cec_ManSat_t * p;
     Gia_Obj_t * pObj;
-    int i, status, clk = clock(), clk2;
+    int i, status;
+    clock_t clk = clock(), clk2;
     // reset the manager
     if ( pPat )
     {
@@ -717,7 +720,7 @@ clk2 = clock();
         // save the pattern
         if ( pPat )
         {
-            int clk3 = clock();
+            clock_t clk3 = clock();
             Cec_ManPatSavePattern( pPat, p, pObj );
             pPat->timeTotalSave += clock() - clk3;
         }
@@ -799,7 +802,8 @@ Vec_Str_t * Cec_ManSatSolveSeq( Vec_Ptr_t * vPatts, Gia_Man_t * pAig, Cec_ParSat
     Cec_ManSat_t * p;
     Gia_Obj_t * pObj;
     int iPat = 0, nPatsInit, nPats;
-    int i, status, clk = clock();
+    int i, status;
+    clock_t clk = clock();
     nPatsInit = nPats = 32 * Vec_PtrReadWordsSimInfo(vPatts);
     Gia_ManSetPhase( pAig );
     Gia_ManLevelNum( pAig );
@@ -957,7 +961,8 @@ Vec_Int_t * Cec_ManSatSolveMiter( Gia_Man_t * pAig, Cec_ParSat_t * pPars, Vec_St
     Vec_Str_t * vStatus;
     Cec_ManSat_t * p;
     Gia_Obj_t * pObj;
-    int i, status, clk = clock();
+    int i, status;
+    clock_t clk = clock();
     // prepare AIG
     Gia_ManSetPhase( pAig );
     Gia_ManLevelNum( pAig );
diff --git a/src/proof/cec/cecSweep.c b/src/proof/cec/cecSweep.c
index 4523810e..505de076 100644
--- a/src/proof/cec/cecSweep.c
+++ b/src/proof/cec/cecSweep.c
@@ -188,7 +188,8 @@ int Cec_ManFraClassesUpdate( Cec_ManFra_t * p, Cec_ManSim_t * pSim, Cec_ManPat_t
 {
     Vec_Ptr_t * vInfo;
     Gia_Obj_t * pObj, * pObjOld, * pReprOld;
-    int i, k, iRepr, iNode, clk;
+    int i, k, iRepr, iNode;
+    clock_t clk;
 clk = clock();
     vInfo = Cec_ManPatCollectPatterns( pPat, Gia_ManCiNum(p->pAig), pSim->nWords );
 p->timePat += clock() - clk;
diff --git a/src/proof/cec/cecSynth.c b/src/proof/cec/cecSynth.c
index 21470dd4..b13b5204 100644
--- a/src/proof/cec/cecSynth.c
+++ b/src/proof/cec/cecSynth.c
@@ -297,7 +297,8 @@ int Cec_SequentialSynthesisPart( Gia_Man_t * p, Cec_ParSeq_t * pPars )
     Vec_Int_t * vPart;
     int * pMapBack, * pReprs;
     int i, nCountPis, nCountRegs;
-    int nClasses, clk = clock();
+    int nClasses;
+    clock_t clk = clock();
 
     // save parameters
     if ( fPrintParts )