Fixing time primtouts throughout the code.

14 files changed, 72 insertions, 51 deletions

diff --git a/src/proof/fra/fra.h b/src/proof/fra/fra.h
index 3e50ff57..c1dd6b44 100644
--- a/src/proof/fra/fra.h
+++ b/src/proof/fra/fra.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/aig/aig/aig.h"
@@ -238,17 +237,17 @@ struct Fra_Man_t_
     int              nSatCallsRecent;
     int              nSatCallsSkipped;
     // runtime
-    int              timeSim;
-    int              timeTrav;
-    int              timeRwr;
-    int              timeSat;
-    int              timeSatUnsat;
-    int              timeSatSat;
-    int              timeSatFail;
-    int              timeRef;
-    int              timeTotal;
-    int              time1;
-    int              time2;
+    clock_t          timeSim;
+    clock_t          timeTrav;
+    clock_t          timeRwr;
+    clock_t          timeSat;
+    clock_t          timeSatUnsat;
+    clock_t          timeSatSat;
+    clock_t          timeSatFail;
+    clock_t          timeRef;
+    clock_t          timeTotal;
+    clock_t          time1;
+    clock_t          time2;
 };
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/proof/fra/fraBmc.c b/src/proof/fra/fraBmc.c
index 2ddecf48..4b68a79a 100644
--- a/src/proof/fra/fraBmc.c
+++ b/src/proof/fra/fraBmc.c
@@ -311,7 +311,8 @@ Aig_Man_t * Fra_BmcFrames( Fra_Bmc_t * p, int fKeepPos )
 void Fra_BmcPerform( Fra_Man_t * p, int nPref, int nDepth )
 {
     Aig_Obj_t * pObj;
-    int i, nImpsOld = 0, clk = clock();
+    int i, nImpsOld = 0;
+    clock_t clk = clock();
     assert( p->pBmc == NULL );
     // derive and fraig the frames
     p->pBmc = Fra_BmcStart( p->pManAig, nPref, nDepth );
@@ -385,7 +386,8 @@ void Fra_BmcPerformSimple( Aig_Man_t * pAig, int nFrames, int nBTLimit, int fRew
     Fra_Man_t * pTemp;
     Fra_Bmc_t * pBmc;
     Aig_Man_t * pAigTemp;
-    int clk, iOutput;
+    clock_t clk;
+    int iOutput;
     // derive and fraig the frames
     clk = clock();
     pBmc = Fra_BmcStart( pAig, 0, nFrames );
diff --git a/src/proof/fra/fraCec.c b/src/proof/fra/fraCec.c
index 0acca245..20805ec2 100644
--- a/src/proof/fra/fraCec.c
+++ b/src/proof/fra/fraCec.c
@@ -53,7 +53,8 @@ int Fra_FraigSat( Aig_Man_t * pMan, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimi
 
         sat_solver2 * pSat;
         Cnf_Dat_t * pCnf;
-        int status, RetValue, clk = clock();
+        int status, RetValue;
+        clock_t clk = clock();
         Vec_Int_t * vCiIds;
 
         assert( Aig_ManRegNum(pMan) == 0 );
@@ -159,7 +160,8 @@ int Fra_FraigSat( Aig_Man_t * pMan, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimi
     {
         sat_solver * pSat;
         Cnf_Dat_t * pCnf;
-        int status, RetValue, clk = clock();
+        int status, RetValue;
+        clock_t clk = clock();
         Vec_Int_t * vCiIds;
 
         assert( Aig_ManRegNum(pMan) == 0 );
@@ -282,7 +284,8 @@ int Fra_FraigCec( Aig_Man_t ** ppAig, int nConfLimit, int fVerbose )
 
     Fra_Par_t Params, * pParams = &Params;
     Aig_Man_t * pAig = *ppAig, * pTemp;
-    int i, RetValue, clk;
+    int i, RetValue;
+    clock_t clk;
 
     // report the original miter
     if ( fVerbose )
@@ -457,7 +460,8 @@ int Fra_FraigCecTop( Aig_Man_t * pMan1, Aig_Man_t * pMan2, int nConfLimit, int n
 {
     Aig_Man_t * pTemp;
     //Abc_NtkDarCec( pNtk1, pNtk2, fPartition, fVerbose );
-    int RetValue, clkTotal = clock();
+    int RetValue;
+    clock_t clkTotal = clock();
 
     if ( Aig_ManCiNum(pMan1) != Aig_ManCiNum(pMan1) )
     {
diff --git a/src/proof/fra/fraClaus.c b/src/proof/fra/fraClaus.c
index f651b0ad..97ac3e40 100644
--- a/src/proof/fra/fraClaus.c
+++ b/src/proof/fra/fraClaus.c
@@ -605,7 +605,8 @@ int Fra_ClausProcessClauses( Clu_Man_t * p, int fRefs )
     Fra_Sml_t * pComb, * pSeq;
     Aig_Obj_t * pObj;
     Dar_Cut_t * pCut;
-    int Scores[16], uScores, i, k, j, clk, nCuts = 0;
+    int Scores[16], uScores, i, k, j, nCuts = 0;
+    clock_t clk;
 
     // simulate the AIG
 clk = clock();
@@ -727,7 +728,8 @@ int Fra_ClausProcessClauses2( Clu_Man_t * p, int fRefs )
     Fra_Sml_t * pComb, * pSeq;
     Aig_Obj_t * pObj;
     Aig_Cut_t * pCut;
-    int i, k, j, clk, nCuts = 0;
+    int i, k, j, nCuts = 0;
+    clock_t clk;
     int ScoresSeq[1<<12], ScoresComb[1<<12];
     assert( p->nLutSize < 13 );
 
@@ -1622,7 +1624,7 @@ void Fra_ClausEstimateCoverage( Clu_Man_t * p )
     unsigned * pResultTot, * pResultOne;
     int nCovered, Beg, End, i, w;
     int * pStart, * pVar2Id; 
-    int clk = clock();
+    clock_t clk = clock();
     // simulate the circuit with nCombSimWords * 32 = 64K patterns
 //    srand( 0xAABBAABB );
     Aig_ManRandom(1);
@@ -1680,7 +1682,7 @@ void Fra_ClausEstimateCoverage( Clu_Man_t * p )
 int Fra_Claus( Aig_Man_t * pAig, int nFrames, int nPref, int nClausesMax, int nLutSize, int nLevels, int nCutsMax, int nBatches, int fStepUp, int fBmc, int fRefs, int fTarget, int fVerbose, int fVeryVerbose )
 {
     Clu_Man_t * p;
-    int clk, clkTotal = clock(), clkInd;
+    clock_t clk, clkTotal = clock(), clkInd;
     int b, Iter, Counter, nPrefOld;
     int nClausesBeg = 0;
 
diff --git a/src/proof/fra/fraCore.c b/src/proof/fra/fraCore.c
index 37aaa0da..35888f43 100644
--- a/src/proof/fra/fraCore.c
+++ b/src/proof/fra/fraCore.c
@@ -376,7 +376,7 @@ Aig_Man_t * Fra_FraigPerform( Aig_Man_t * pManAig, Fra_Par_t * pPars )
 {
     Fra_Man_t * p;
     Aig_Man_t * pManAigNew;
-    int clk;
+    clock_t clk;
     if ( Aig_ManNodeNum(pManAig) == 0 )
         return Aig_ManDupOrdered(pManAig);
 clk = clock();
@@ -402,7 +402,7 @@ Fra_ClassesPrint( p->pCla, 1 );
     Fra_ManFinalizeComb( p );
     if ( p->pPars->fChoicing )
     { 
-int clk2 = clock();
+clock_t clk2 = clock();
         Fra_ClassesCopyReprs( p->pCla, p->vTimeouts );
         pManAigNew = Aig_ManDupRepr( p->pManAig, 1 );
         Aig_ManReprStart( pManAigNew, Aig_ManObjNumMax(pManAigNew) );
diff --git a/src/proof/fra/fraHot.c b/src/proof/fra/fraHot.c
index 338b5717..a91c939f 100644
--- a/src/proof/fra/fraHot.c
+++ b/src/proof/fra/fraHot.c
@@ -332,7 +332,7 @@ void Fra_OneHotEstimateCoverage( Fra_Man_t * p, Vec_Int_t * vOneHots )
     Vec_Ptr_t * vSimInfo;
     unsigned * pSim1, * pSim2, * pSimTot;
     int i, w, Out1, Out2, nCovered, Counter = 0;
-    int clk = clock();
+    clock_t clk = clock();
 
     // generate random sim-info at register outputs
     vSimInfo = Vec_PtrAllocSimInfo( nRegs + 1, nSimWords );
diff --git a/src/proof/fra/fraImp.c b/src/proof/fra/fraImp.c
index f65aca5c..4d33717a 100644
--- a/src/proof/fra/fraImp.c
+++ b/src/proof/fra/fraImp.c
@@ -327,7 +327,8 @@ Vec_Int_t * Fra_ImpDerive( Fra_Man_t * p, int nImpMaxLimit, int nImpUseLimit, in
     int * pImpCosts, * pNodesI, * pNodesK;
     int nImpsTotal = 0, nImpsTried = 0, nImpsNonSeq = 0, nImpsComb = 0, nImpsCollected = 0;
     int CostMin = ABC_INFINITY, CostMax = 0;
-    int i, k, Imp, CostRange, clk = clock();
+    int i, k, Imp, CostRange;
+    clock_t clk = clock();
     assert( Aig_ManObjNumMax(p->pManAig) < (1 << 15) );
     assert( nImpMaxLimit > 0 && nImpUseLimit > 0 && nImpUseLimit <= nImpMaxLimit );
     // normalize both managers
diff --git a/src/proof/fra/fraInd.c b/src/proof/fra/fraInd.c
index 29a76eea..633f8979 100644
--- a/src/proof/fra/fraInd.c
+++ b/src/proof/fra/fraInd.c
@@ -49,7 +49,8 @@ void Fra_FraigInductionRewrite( Fra_Man_t * p )
 {
     Aig_Man_t * pTemp;
     Aig_Obj_t * pObj, * pObjPo;
-    int nTruePis, k, i, clk = clock();
+    int nTruePis, k, i;
+    clock_t clk = clock();
     // perform AIG rewriting on the speculated frames
 //    pTemp = Dar_ManRwsat( pTemp, 1, 0 );
     pTemp = Dar_ManRewriteDefault( p->pManFraig );
@@ -259,7 +260,7 @@ Aig_Man_t * Fra_FraigInductionPart( Aig_Man_t * pAig, Fra_Ssw_t * pPars )
     int * pMapBack;
     int i, nCountPis, nCountRegs;
     int nClasses, nPartSize, fVerbose;
-    int clk = clock();
+    clock_t clk = clock();
 
     // save parameters
     nPartSize = pPars->nPartSize; pPars->nPartSize = 0;
@@ -357,8 +358,9 @@ Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, Fra_Ssw_t * pParams )
     Aig_Man_t * pManAigNew = NULL;
     int nNodesBeg, nRegsBeg;
     int nIter = -1; // Suppress "might be used uninitialized"
-    int i, clk = clock(), clk2;
-    int TimeToStop = (pParams->TimeLimit == 0.0)? 0 : clock() + (int)(pParams->TimeLimit * CLOCKS_PER_SEC);
+    int i;
+    clock_t clk = clock(), clk2;
+    clock_t TimeToStop = pParams->TimeLimit ? pParams->TimeLimit * CLOCKS_PER_SEC + clock() : 0;
 
     if ( Aig_ManNodeNum(pManAig) == 0 )
     {
@@ -473,7 +475,7 @@ ABC_PRT( "Time", clock() - clk );
         int nLitsOld = Fra_ClassesCountLits(p->pCla);
         int nImpsOld = p->pCla->vImps? Vec_IntSize(p->pCla->vImps) : 0;
         int nHotsOld = p->vOneHots? Fra_OneHotCount(p, p->vOneHots) : 0;
-        int clk3 = clock();
+        clock_t clk3 = clock();
 
         if ( pParams->TimeLimit != 0.0 && clock() > TimeToStop )
         {
diff --git a/src/proof/fra/fraIndVer.c b/src/proof/fra/fraIndVer.c
index 7c5e9e70..099256ac 100644
--- a/src/proof/fra/fraIndVer.c
+++ b/src/proof/fra/fraIndVer.c
@@ -50,7 +50,7 @@ int Fra_InvariantVerify( Aig_Man_t * pAig, int nFrames, Vec_Int_t * vClauses, Ve
     int * pStart;
     int RetValue, Beg, End, i, k;
     int CounterBase = 0, CounterInd = 0;
-    int clk = clock();
+    clock_t clk = clock();
 
     if ( nFrames != 1 )
     {
diff --git a/src/proof/fra/fraLcr.c b/src/proof/fra/fraLcr.c
index 8ea6d297..2941f24f 100644
--- a/src/proof/fra/fraLcr.c
+++ b/src/proof/fra/fraLcr.c
@@ -54,12 +54,12 @@ struct Fra_Lcr_t_
     int              nRegsBeg;
     int              nRegsEnd;
     // runtime
-    int              timeSim;
-    int              timePart;
-    int              timeTrav;
-    int              timeFraig;
-    int              timeUpdate;
-    int              timeTotal;
+    clock_t          timeSim;
+    clock_t          timePart;
+    clock_t          timeTrav;
+    clock_t          timeFraig;
+    clock_t          timeUpdate;
+    clock_t          timeTotal;
 };
 
 ////////////////////////////////////////////////////////////////////////
@@ -538,8 +538,9 @@ Aig_Man_t * Fra_FraigLatchCorrespondence( Aig_Man_t * pAig, int nFramesP, int nC
     Fra_Man_t * pTemp;
     Aig_Man_t * pAigPart, * pAigTemp, * pAigNew = NULL;
     Vec_Int_t * vPart;
-    int i, nIter, timeSim, clk2, clk3, clk = clock();
-    int TimeToStop = (TimeLimit == 0.0)? 0 : clock() + (int)(TimeLimit * CLOCKS_PER_SEC);
+    int i, nIter;
+    clock_t timeSim, clk2, clk3, clk = clock();
+    clock_t TimeToStop = TimeLimit ? TimeLimit * CLOCKS_PER_SEC + clock() : 0;
     if ( Aig_ManNodeNum(pAig) == 0 )
     {
         if ( pnIter ) *pnIter = 0;
diff --git a/src/proof/fra/fraPart.c b/src/proof/fra/fraPart.c
index e3bb2850..e1c8ddf4 100644
--- a/src/proof/fra/fraPart.c
+++ b/src/proof/fra/fraPart.c
@@ -53,7 +53,7 @@ void Fra_ManPartitionTest( Aig_Man_t * p, int nComLim )
     int i, k, nCommon, CountOver, CountQuant;
     int nTotalSupp, nTotalSupp2, Entry, Largest;//, iVar;
     double Ratio, R;
-    int clk;
+    clock_t clk;
 
     nTotalSupp = 0;
     nTotalSupp2 = 0;
@@ -190,7 +190,8 @@ void Fra_ManPartitionTest2( Aig_Man_t * p )
     Vec_Int_t * vSup, * vSup2, * vSup3;
     Aig_Obj_t * pObj;
     int Entry, Entry2, Entry3, Counter;
-    int i, k, m, n, clk;
+    int i, k, m, n;
+    clock_t clk;
     char * pSupp;
  
     // compute supports
diff --git a/src/proof/fra/fraSat.c b/src/proof/fra/fraSat.c
index 2702113c..fc95fd62 100644
--- a/src/proof/fra/fraSat.c
+++ b/src/proof/fra/fraSat.c
@@ -47,7 +47,8 @@ static int Fra_SetActivityFactors( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t *
 ***********************************************************************/
 int Fra_NodesAreEquiv( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew )
 {
-    int pLits[4], RetValue, RetValue1, nBTLimit, clk;//, clk2 = clock();
+    int pLits[4], RetValue, RetValue1, nBTLimit;
+    clock_t clk;//, clk2 = clock();
     int status;
 
     // make sure the nodes are not complemented
@@ -207,7 +208,8 @@ p->timeSatFail += clock() - clk;
 ***********************************************************************/
 int Fra_NodesAreImp( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew, int fComplL, int fComplR )
 {
-    int pLits[4], RetValue, RetValue1, nBTLimit, clk;//, clk2 = clock();
+    int pLits[4], RetValue, RetValue1, nBTLimit;
+    clock_t clk;//, clk2 = clock();
     int status;
 
     // make sure the nodes are not complemented
@@ -314,7 +316,8 @@ p->timeSatFail += clock() - clk;
 ***********************************************************************/
 int Fra_NodesAreClause( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew, int fComplL, int fComplR )
 {
-    int pLits[4], RetValue, RetValue1, nBTLimit, clk;//, clk2 = clock();
+    int pLits[4], RetValue, RetValue1, nBTLimit;
+    clock_t clk;//, clk2 = clock();
     int status;
 
     // make sure the nodes are not complemented
@@ -421,7 +424,8 @@ p->timeSatFail += clock() - clk;
 ***********************************************************************/
 int Fra_NodeIsConst( Fra_Man_t * p, Aig_Obj_t * pNew )
 {
-    int pLits[2], RetValue1, RetValue, clk;
+    int pLits[2], RetValue1, RetValue;
+    clock_t clk;
 
     // make sure the nodes are not complemented
     assert( !Aig_IsComplement(pNew) );
@@ -535,7 +539,8 @@ int Fra_SetActivityFactors_rec( Fra_Man_t * p, Aig_Obj_t * pObj, int LevelMin, i
 ***********************************************************************/
 int Fra_SetActivityFactors( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew )
 {
-    int clk, LevelMin, LevelMax;
+    int LevelMin, LevelMax;
+    clock_t clk;
     assert( pOld || pNew );
 clk = clock(); 
     // reset the active variables
diff --git a/src/proof/fra/fraSec.c b/src/proof/fra/fraSec.c
index cde56809..ac6cd67e 100644
--- a/src/proof/fra/fraSec.c
+++ b/src/proof/fra/fraSec.c
@@ -98,7 +98,8 @@ int Fra_FraigSec( Aig_Man_t * p, Fra_Sec_t * pParSec, Aig_Man_t ** ppResult )
     Fra_Ssw_t Pars, * pPars = &Pars;
     Fra_Sml_t * pSml;
     Aig_Man_t * pNew, * pTemp;
-    int nFrames, RetValue, nIter, clk, clkTotal = clock();
+    int nFrames, RetValue, nIter;
+    clock_t clk, clkTotal = clock();
     int TimeOut = 0;
     int fLatchCorr = 0;
     float TimeLeft = 0.0;
diff --git a/src/proof/fra/fraSim.c b/src/proof/fra/fraSim.c
index 66579be3..555789e2 100644
--- a/src/proof/fra/fraSim.c
+++ b/src/proof/fra/fraSim.c
@@ -662,7 +662,8 @@ int Fra_SmlCheckNonConstOutputs( Fra_Sml_t * p )
 void Fra_SmlSimulateOne( Fra_Sml_t * p )
 {
     Aig_Obj_t * pObj, * pObjLi, * pObjLo;
-    int f, i, clk;
+    int f, i;
+    clock_t clk;
 clk = clock();
     for ( f = 0; f < p->nFrames; f++ )
     {
@@ -700,7 +701,8 @@ p->nSimRounds++;
 ***********************************************************************/
 void Fra_SmlResimulate( Fra_Man_t * p )
 {
-    int nChanges, clk;
+    int nChanges;
+    clock_t clk;
     Fra_SmlAssignDist1( p->pSml, p->pPatWords );
     Fra_SmlSimulateOne( p->pSml );
 //    if ( p->pPars->fPatScores )
@@ -735,7 +737,8 @@ p->timeRef += clock() - clk;
 void Fra_SmlSimulate( Fra_Man_t * p, int fInit )
 {
     int fVerbose = 0;
-    int nChanges, nClasses, clk;
+    int nChanges, nClasses;
+    clock_t clk;
     assert( !fInit || Aig_ManRegNum(p->pManAig) );
     // start the classes
     Fra_SmlInitialize( p->pSml, fInit );