summaryrefslogtreecommitdiffstats
path: root/src/proof/fra
diff options
context:
space:
mode:
Diffstat (limited to 'src/proof/fra')
-rw-r--r--src/proof/fra/fra.h23
-rw-r--r--src/proof/fra/fraBmc.c6
-rw-r--r--src/proof/fra/fraCec.c12
-rw-r--r--src/proof/fra/fraClaus.c10
-rw-r--r--src/proof/fra/fraCore.c4
-rw-r--r--src/proof/fra/fraHot.c2
-rw-r--r--src/proof/fra/fraImp.c3
-rw-r--r--src/proof/fra/fraInd.c12
-rw-r--r--src/proof/fra/fraIndVer.c2
-rw-r--r--src/proof/fra/fraLcr.c17
-rw-r--r--src/proof/fra/fraPart.c5
-rw-r--r--src/proof/fra/fraSat.c15
-rw-r--r--src/proof/fra/fraSec.c3
-rw-r--r--src/proof/fra/fraSim.c9
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 );
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-05 03:35:38 +0000