summaryrefslogtreecommitdiffstats
path: root/src/proof/fra
diff options
context:
space:
mode:
Diffstat (limited to 'src/proof/fra')
-rw-r--r--src/proof/fra/fra.h22
-rw-r--r--src/proof/fra/fraBmc.c18
-rw-r--r--src/proof/fra/fraCec.c54
-rw-r--r--src/proof/fra/fraClaus.c90
-rw-r--r--src/proof/fra/fraCore.c10
-rw-r--r--src/proof/fra/fraHot.c4
-rw-r--r--src/proof/fra/fraImp.c4
-rw-r--r--src/proof/fra/fraInd.c38
-rw-r--r--src/proof/fra/fraIndVer.c4
-rw-r--r--src/proof/fra/fraLcr.c54
-rw-r--r--src/proof/fra/fraPart.c28
-rw-r--r--src/proof/fra/fraSat.c70
-rw-r--r--src/proof/fra/fraSec.c74
-rw-r--r--src/proof/fra/fraSim.c26
14 files changed, 248 insertions, 248 deletions
diff --git a/src/proof/fra/fra.h b/src/proof/fra/fra.h
index b1fdb539..391ba482 100644
--- a/src/proof/fra/fra.h
+++ b/src/proof/fra/fra.h
@@ -237,17 +237,17 @@ struct Fra_Man_t_
int nSatCallsRecent;
int nSatCallsSkipped;
// runtime
- 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;
+ abctime timeSim;
+ abctime timeTrav;
+ abctime timeRwr;
+ abctime timeSat;
+ abctime timeSatUnsat;
+ abctime timeSatSat;
+ abctime timeSatFail;
+ abctime timeRef;
+ abctime timeTotal;
+ abctime time1;
+ abctime time2;
};
////////////////////////////////////////////////////////////////////////
diff --git a/src/proof/fra/fraBmc.c b/src/proof/fra/fraBmc.c
index 4b68a79a..cc6bb8c0 100644
--- a/src/proof/fra/fraBmc.c
+++ b/src/proof/fra/fraBmc.c
@@ -312,7 +312,7 @@ void Fra_BmcPerform( Fra_Man_t * p, int nPref, int nDepth )
{
Aig_Obj_t * pObj;
int i, nImpsOld = 0;
- clock_t clk = clock();
+ abctime clk = Abc_Clock();
assert( p->pBmc == NULL );
// derive and fraig the frames
p->pBmc = Fra_BmcStart( p->pManAig, nPref, nDepth );
@@ -337,7 +337,7 @@ void Fra_BmcPerform( Fra_Man_t * p, int nPref, int nDepth )
printf( "Original AIG = %d. Init %d frames = %d. Fraig = %d. ",
Aig_ManNodeNum(p->pBmc->pAig), p->pBmc->nFramesAll,
Aig_ManNodeNum(p->pBmc->pAigFrames), Aig_ManNodeNum(p->pBmc->pAigFraig) );
- ABC_PRT( "Time", clock() - clk );
+ ABC_PRT( "Time", Abc_Clock() - clk );
printf( "Before BMC: " );
// Fra_ClassesPrint( p->pCla, 0 );
printf( "Const = %5d. Class = %5d. Lit = %5d. ",
@@ -386,10 +386,10 @@ 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;
- clock_t clk;
+ abctime clk;
int iOutput;
// derive and fraig the frames
- clk = clock();
+ clk = Abc_Clock();
pBmc = Fra_BmcStart( pAig, 0, nFrames );
pTemp = Fra_LcrAigPrepare( pAig );
pTemp->pBmc = pBmc;
@@ -402,21 +402,21 @@ void Fra_BmcPerformSimple( Aig_Man_t * pAig, int nFrames, int nBTLimit, int fRew
printf( "Time-frames (%d): PI/PO = %d/%d. Node = %6d. Lev = %5d. ",
nFrames, Aig_ManCiNum(pBmc->pAigFrames), Aig_ManCoNum(pBmc->pAigFrames),
Aig_ManNodeNum(pBmc->pAigFrames), Aig_ManLevelNum(pBmc->pAigFrames) );
- ABC_PRT( "Time", clock() - clk );
+ ABC_PRT( "Time", Abc_Clock() - clk );
}
if ( fRewrite )
{
- clk = clock();
+ clk = Abc_Clock();
pBmc->pAigFrames = Dar_ManRwsat( pAigTemp = pBmc->pAigFrames, 1, 0 );
Aig_ManStop( pAigTemp );
if ( fVerbose )
{
printf( "Time-frames after rewriting: Node = %6d. Lev = %5d. ",
Aig_ManNodeNum(pBmc->pAigFrames), Aig_ManLevelNum(pBmc->pAigFrames) );
- ABC_PRT( "Time", clock() - clk );
+ ABC_PRT( "Time", Abc_Clock() - clk );
}
}
- clk = clock();
+ clk = Abc_Clock();
iOutput = Fra_FraigMiterAssertedOutput( pBmc->pAigFrames );
if ( iOutput >= 0 )
pAig->pSeqModel = Abc_CexMakeTriv( Aig_ManRegNum(pAig), Aig_ManCiNum(pAig)-Aig_ManRegNum(pAig), Aig_ManCoNum(pAig)-Aig_ManRegNum(pAig), iOutput );
@@ -437,7 +437,7 @@ void Fra_BmcPerformSimple( Aig_Man_t * pAig, int nFrames, int nBTLimit, int fRew
printf( "Fraiged init frames: Node = %6d. Lev = %5d. ",
pBmc->pAigFraig? Aig_ManNodeNum(pBmc->pAigFraig) : -1,
pBmc->pAigFraig? Aig_ManLevelNum(pBmc->pAigFraig) : -1 );
- ABC_PRT( "Time", clock() - clk );
+ ABC_PRT( "Time", Abc_Clock() - clk );
}
Fra_BmcStop( pBmc );
ABC_FREE( pTemp );
diff --git a/src/proof/fra/fraCec.c b/src/proof/fra/fraCec.c
index 3e7addb2..662a1d9e 100644
--- a/src/proof/fra/fraCec.c
+++ b/src/proof/fra/fraCec.c
@@ -54,7 +54,7 @@ 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;
- clock_t clk = clock();
+ abctime clk = Abc_Clock();
Vec_Int_t * vCiIds;
assert( Aig_ManRegNum(pMan) == 0 );
@@ -100,13 +100,13 @@ int Fra_FraigSat( Aig_Man_t * pMan, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimi
printf( "Created SAT problem with %d variable and %d clauses. ", sat_solver2_nvars(pSat), sat_solver2_nclauses(pSat) );
- ABC_PRT( "Time", clock() - clk );
+ ABC_PRT( "Time", Abc_Clock() - clk );
// simplify the problem
- clk = clock();
+ clk = Abc_Clock();
status = sat_solver2_simplify(pSat);
// printf( "Simplified the problem to %d variables and %d clauses. ", sat_solver2_nvars(pSat), sat_solver2_nclauses(pSat) );
-// ABC_PRT( "Time", clock() - clk );
+// ABC_PRT( "Time", Abc_Clock() - clk );
if ( status == 0 )
{
Vec_IntFree( vCiIds );
@@ -116,7 +116,7 @@ int Fra_FraigSat( Aig_Man_t * pMan, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimi
}
// solve the miter
- clk = clock();
+ clk = Abc_Clock();
if ( fVerbose )
pSat->verbosity = 1;
status = sat_solver2_solve( pSat, NULL, NULL, (ABC_INT64_T)nConfLimit, (ABC_INT64_T)nInsLimit, (ABC_INT64_T)0, (ABC_INT64_T)0 );
@@ -139,7 +139,7 @@ int Fra_FraigSat( Aig_Man_t * pMan, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimi
assert( 0 );
// Abc_Print( 1, "The number of conflicts = %6d. ", (int)pSat->stats.conflicts );
- // Abc_PrintTime( 1, "Solving time", clock() - clk );
+ // Abc_PrintTime( 1, "Solving time", Abc_Clock() - clk );
// if the problem is SAT, get the counterexample
if ( status == l_True )
@@ -160,7 +160,7 @@ 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;
- clock_t clk = clock();
+ abctime clk = Abc_Clock();
Vec_Int_t * vCiIds;
assert( Aig_ManRegNum(pMan) == 0 );
@@ -215,13 +215,13 @@ int Fra_FraigSat( Aig_Man_t * pMan, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimi
// printf( "Created SAT problem with %d variable and %d clauses. ", sat_solver_nvars(pSat), sat_solver_nclauses(pSat) );
- // ABC_PRT( "Time", clock() - clk );
+ // ABC_PRT( "Time", Abc_Clock() - clk );
// simplify the problem
- clk = clock();
+ clk = Abc_Clock();
status = sat_solver_simplify(pSat);
// printf( "Simplified the problem to %d variables and %d clauses. ", sat_solver_nvars(pSat), sat_solver_nclauses(pSat) );
- // ABC_PRT( "Time", clock() - clk );
+ // ABC_PRT( "Time", Abc_Clock() - clk );
if ( status == 0 )
{
Vec_IntFree( vCiIds );
@@ -231,7 +231,7 @@ int Fra_FraigSat( Aig_Man_t * pMan, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimi
}
// solve the miter
- clk = clock();
+ clk = Abc_Clock();
// if ( fVerbose )
// pSat->verbosity = 1;
status = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)nConfLimit, (ABC_INT64_T)nInsLimit, (ABC_INT64_T)0, (ABC_INT64_T)0 );
@@ -254,7 +254,7 @@ int Fra_FraigSat( Aig_Man_t * pMan, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimi
assert( 0 );
// Abc_Print( 1, "The number of conflicts = %6d. ", (int)pSat->stats.conflicts );
- // Abc_PrintTime( 1, "Solving time", clock() - clk );
+ // Abc_PrintTime( 1, "Solving time", Abc_Clock() - clk );
// if the problem is SAT, get the counterexample
if ( status == l_True )
@@ -292,7 +292,7 @@ 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;
- clock_t clk;
+ abctime clk;
// report the original miter
if ( fVerbose )
@@ -309,24 +309,24 @@ int Fra_FraigCec( Aig_Man_t ** ppAig, int nConfLimit, int fVerbose )
}
// if SAT only, solve without iteration
-clk = clock();
+clk = Abc_Clock();
RetValue = Fra_FraigSat( pAig, (ABC_INT64_T)2*nBTLimitStart, (ABC_INT64_T)0, 0, 0, 0, 1, 0, 0, 0 );
if ( fVerbose )
{
printf( "Initial SAT: Nodes = %6d. ", Aig_ManNodeNum(pAig) );
-ABC_PRT( "Time", clock() - clk );
+ABC_PRT( "Time", Abc_Clock() - clk );
}
if ( RetValue >= 0 )
return RetValue;
// duplicate the AIG
-clk = clock();
+clk = Abc_Clock();
pAig = Dar_ManRwsat( pTemp = pAig, 1, 0 );
Aig_ManStop( pTemp );
if ( fVerbose )
{
printf( "Rewriting: Nodes = %6d. ", Aig_ManNodeNum(pAig) );
-ABC_PRT( "Time", clock() - clk );
+ABC_PRT( "Time", Abc_Clock() - clk );
}
// perform the loop
@@ -339,13 +339,13 @@ ABC_PRT( "Time", clock() - clk );
{
//printf( "Running fraiging with %d BTnode and %d BTmiter.\n", pParams->nBTLimitNode, pParams->nBTLimitMiter );
// run fraiging
-clk = clock();
+clk = Abc_Clock();
pAig = Fra_FraigPerform( pTemp = pAig, pParams );
Aig_ManStop( pTemp );
if ( fVerbose )
{
printf( "Fraiging (i=%d): Nodes = %6d. ", i+1, Aig_ManNodeNum(pAig) );
-ABC_PRT( "Time", clock() - clk );
+ABC_PRT( "Time", Abc_Clock() - clk );
}
// check the miter status
@@ -354,13 +354,13 @@ ABC_PRT( "Time", clock() - clk );
break;
// perform rewriting
-clk = clock();
+clk = Abc_Clock();
pAig = Dar_ManRewriteDefault( pTemp = pAig );
Aig_ManStop( pTemp );
if ( fVerbose )
{
printf( "Rewriting: Nodes = %6d. ", Aig_ManNodeNum(pAig) );
-ABC_PRT( "Time", clock() - clk );
+ABC_PRT( "Time", Abc_Clock() - clk );
}
// check the miter status
@@ -377,12 +377,12 @@ ABC_PRT( "Time", clock() - clk );
// if still unsolved try last gasp
if ( RetValue == -1 )
{
-clk = clock();
+clk = Abc_Clock();
RetValue = Fra_FraigSat( pAig, (ABC_INT64_T)nBTLimitLast, (ABC_INT64_T)0, 0, 0, 0, 1, 0, 0, 0 );
if ( fVerbose )
{
printf( "Final SAT: Nodes = %6d. ", Aig_ManNodeNum(pAig) );
-ABC_PRT( "Time", clock() - clk );
+ABC_PRT( "Time", Abc_Clock() - clk );
}
}
@@ -468,7 +468,7 @@ 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;
- clock_t clkTotal = clock();
+ abctime clkTotal = Abc_Clock();
if ( Aig_ManCiNum(pMan1) != Aig_ManCiNum(pMan1) )
{
@@ -501,17 +501,17 @@ int Fra_FraigCecTop( Aig_Man_t * pMan1, Aig_Man_t * pMan2, int nConfLimit, int n
if ( RetValue == 1 )
{
printf( "Networks are equivalent. " );
-ABC_PRT( "Time", clock() - clkTotal );
+ABC_PRT( "Time", Abc_Clock() - clkTotal );
}
else if ( RetValue == 0 )
{
printf( "Networks are NOT EQUIVALENT. " );
-ABC_PRT( "Time", clock() - clkTotal );
+ABC_PRT( "Time", Abc_Clock() - clkTotal );
}
else
{
printf( "Networks are UNDECIDED. " );
-ABC_PRT( "Time", clock() - clkTotal );
+ABC_PRT( "Time", Abc_Clock() - clkTotal );
}
fflush( stdout );
return RetValue;
diff --git a/src/proof/fra/fraClaus.c b/src/proof/fra/fraClaus.c
index c4f50559..cb41dc5e 100644
--- a/src/proof/fra/fraClaus.c
+++ b/src/proof/fra/fraClaus.c
@@ -606,10 +606,10 @@ int Fra_ClausProcessClauses( Clu_Man_t * p, int fRefs )
Aig_Obj_t * pObj;
Dar_Cut_t * pCut;
int Scores[16], uScores, i, k, j, nCuts = 0;
- clock_t clk;
+ abctime clk;
// simulate the AIG
-clk = clock();
+clk = Abc_Clock();
// srand( 0xAABBAABB );
Aig_ManRandom(1);
pSeq = Fra_SmlSimulateSeq( p->pAig, 0, p->nPref + p->nSimFrames, p->nSimWords/p->nSimFrames, 1 );
@@ -621,32 +621,32 @@ clk = clock();
}
if ( p->fVerbose )
{
-ABC_PRT( "Sim-seq", clock() - clk );
+ABC_PRT( "Sim-seq", Abc_Clock() - clk );
}
-clk = clock();
+clk = Abc_Clock();
if ( fRefs )
{
Fra_ClausCollectLatchClauses( p, pSeq );
if ( p->fVerbose )
{
-ABC_PRT( "Lat-cla", clock() - clk );
+ABC_PRT( "Lat-cla", Abc_Clock() - clk );
}
}
// generate cuts for all nodes, assign cost, and find best cuts
-clk = clock();
+clk = Abc_Clock();
pMemCuts = Dar_ManComputeCuts( p->pAig, 10, 0, 1 );
// pManCut = Aig_ComputeCuts( p->pAig, 10, 4, 0, 1 );
if ( p->fVerbose )
{
-ABC_PRT( "Cuts ", clock() - clk );
+ABC_PRT( "Cuts ", Abc_Clock() - clk );
}
// collect sequential info for each cut
-clk = clock();
+clk = Abc_Clock();
Aig_ManForEachNode( p->pAig, pObj, i )
Dar_ObjForEachCut( pObj, pCut, k )
if ( pCut->nLeaves > 1 )
@@ -660,22 +660,22 @@ clk = clock();
}
if ( p->fVerbose )
{
-ABC_PRT( "Infoseq", clock() - clk );
+ABC_PRT( "Infoseq", Abc_Clock() - clk );
}
Fra_SmlStop( pSeq );
// perform combinational simulation
-clk = clock();
+clk = Abc_Clock();
// srand( 0xAABBAABB );
Aig_ManRandom(1);
pComb = Fra_SmlSimulateComb( p->pAig, p->nSimWords + p->nSimWordsPref, 0 );
if ( p->fVerbose )
{
-ABC_PRT( "Sim-cmb", clock() - clk );
+ABC_PRT( "Sim-cmb", Abc_Clock() - clk );
}
// collect combinational info for each cut
-clk = clock();
+clk = Abc_Clock();
Aig_ManForEachNode( p->pAig, pObj, i )
Dar_ObjForEachCut( pObj, pCut, k )
if ( pCut->nLeaves > 1 )
@@ -696,7 +696,7 @@ clk = clock();
// Aig_ManCutStop( pManCut );
if ( p->fVerbose )
{
-ABC_PRT( "Infocmb", clock() - clk );
+ABC_PRT( "Infocmb", Abc_Clock() - clk );
}
if ( p->fVerbose )
@@ -729,12 +729,12 @@ int Fra_ClausProcessClauses2( Clu_Man_t * p, int fRefs )
Aig_Obj_t * pObj;
Aig_Cut_t * pCut;
int i, k, j, nCuts = 0;
- clock_t clk;
+ abctime clk;
int ScoresSeq[1<<12], ScoresComb[1<<12];
assert( p->nLutSize < 13 );
// simulate the AIG
-clk = clock();
+clk = Abc_Clock();
// srand( 0xAABBAABB );
Aig_ManRandom(1);
pSeq = Fra_SmlSimulateSeq( p->pAig, 0, p->nPref + p->nSimFrames, p->nSimWords/p->nSimFrames, 1 );
@@ -746,42 +746,42 @@ clk = clock();
}
if ( p->fVerbose )
{
-//ABC_PRT( "Sim-seq", clock() - clk );
+//ABC_PRT( "Sim-seq", Abc_Clock() - clk );
}
// perform combinational simulation
-clk = clock();
+clk = Abc_Clock();
// srand( 0xAABBAABB );
Aig_ManRandom(1);
pComb = Fra_SmlSimulateComb( p->pAig, p->nSimWords + p->nSimWordsPref, 0 );
if ( p->fVerbose )
{
-//ABC_PRT( "Sim-cmb", clock() - clk );
+//ABC_PRT( "Sim-cmb", Abc_Clock() - clk );
}
-clk = clock();
+clk = Abc_Clock();
if ( fRefs )
{
Fra_ClausCollectLatchClauses( p, pSeq );
if ( p->fVerbose )
{
-//ABC_PRT( "Lat-cla", clock() - clk );
+//ABC_PRT( "Lat-cla", Abc_Clock() - clk );
}
}
// generate cuts for all nodes, assign cost, and find best cuts
-clk = clock();
+clk = Abc_Clock();
// pMemCuts = Dar_ManComputeCuts( p->pAig, 10, 0, 1 );
pManCut = Aig_ComputeCuts( p->pAig, p->nCutsMax, p->nLutSize, 0, p->fVerbose );
if ( p->fVerbose )
{
-//ABC_PRT( "Cuts ", clock() - clk );
+//ABC_PRT( "Cuts ", Abc_Clock() - clk );
}
// collect combinational info for each cut
-clk = clock();
+clk = Abc_Clock();
Aig_ManForEachNode( p->pAig, pObj, i )
{
if ( pObj->Level > (unsigned)p->nLevels )
@@ -810,7 +810,7 @@ clk = clock();
{
printf( "Node = %5d. Cuts = %7d. Clauses = %6d. Clause/cut = %6.2f.\n",
Aig_ManNodeNum(p->pAig), nCuts, Vec_IntSize(p->vClauses), 1.0*Vec_IntSize(p->vClauses)/nCuts );
- ABC_PRT( "Processing sim-info to find candidate clauses (unoptimized)", clock() - clk );
+ ABC_PRT( "Processing sim-info to find candidate clauses (unoptimized)", Abc_Clock() - clk );
}
// filter out clauses that are contained in the already proven clauses
@@ -1624,7 +1624,7 @@ void Fra_ClausEstimateCoverage( Clu_Man_t * p )
unsigned * pResultTot, * pResultOne;
int nCovered, Beg, End, i, w;
int * pStart, * pVar2Id;
- clock_t clk = clock();
+ abctime clk = Abc_Clock();
// simulate the circuit with nCombSimWords * 32 = 64K patterns
// srand( 0xAABBAABB );
Aig_ManRandom(1);
@@ -1664,7 +1664,7 @@ void Fra_ClausEstimateCoverage( Clu_Man_t * p )
// print the result
printf( "Care states ratio = %f. ", 1.0 * (nCombSimWords * 32 - nCovered) / (nCombSimWords * 32) );
printf( "(%d out of %d patterns) ", nCombSimWords * 32 - nCovered, nCombSimWords * 32 );
- ABC_PRT( "Time", clock() - clk );
+ ABC_PRT( "Time", Abc_Clock() - clk );
}
@@ -1682,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;
- clock_t clk, clkTotal = clock(), clkInd;
+ abctime clk, clkTotal = Abc_Clock(), clkInd;
int b, Iter, Counter, nPrefOld;
int nClausesBeg = 0;
@@ -1692,12 +1692,12 @@ if ( p->fVerbose )
{
printf( "PARAMETERS: Frames = %d. Pref = %d. Clauses max = %d. Cut size = %d.\n", nFrames, nPref, nClausesMax, nLutSize );
printf( "Level max = %d. Cuts max = %d. Batches = %d. Increment cut size = %s.\n", nLevels, nCutsMax, nBatches, fStepUp? "yes":"no" );
-//ABC_PRT( "Sim-seq", clock() - clk );
+//ABC_PRT( "Sim-seq", Abc_Clock() - clk );
}
assert( !p->fTarget || Aig_ManCoNum(pAig) - Aig_ManRegNum(pAig) == 1 );
-clk = clock();
+clk = Abc_Clock();
// derive CNF
// if ( p->fTarget )
// p->pAig->nRegs++;
@@ -1706,11 +1706,11 @@ clk = clock();
// p->pAig->nRegs--;
if ( fVerbose )
{
-//ABC_PRT( "CNF ", clock() - clk );
+//ABC_PRT( "CNF ", Abc_Clock() - clk );
}
// check BMC
-clk = clock();
+clk = Abc_Clock();
p->pSatBmc = (sat_solver *)Cnf_DataWriteIntoSolver( p->pCnf, p->nPref + p->nFrames, 1 );
if ( p->pSatBmc == NULL )
{
@@ -1726,11 +1726,11 @@ clk = clock();
}
if ( fVerbose )
{
-//ABC_PRT( "SAT-bmc", clock() - clk );
+//ABC_PRT( "SAT-bmc", Abc_Clock() - clk );
}
// start the SAT solver
-clk = clock();
+clk = Abc_Clock();
p->pSatMain = (sat_solver *)Cnf_DataWriteIntoSolver( p->pCnf, p->nFrames+1, 0 );
if ( p->pSatMain == NULL )
{
@@ -1757,11 +1757,11 @@ clk = clock();
}
if ( fVerbose )
{
-// ABC_PRT( "SAT-ind", clock() - clk );
+// ABC_PRT( "SAT-ind", Abc_Clock() - clk );
}
// collect the candidate inductive clauses using 4-cuts
- clk = clock();
+ clk = Abc_Clock();
nPrefOld = p->nPref; p->nPref = 0; p->nSimWordsPref = 0;
// Fra_ClausProcessClauses( p, fRefs );
Fra_ClausProcessClauses2( p, fRefs );
@@ -1769,25 +1769,25 @@ clk = clock();
p->nSimWordsPref = p->nPref*p->nSimWords/p->nSimFrames;
nClausesBeg = p->nClauses;
- //ABC_PRT( "Clauses", clock() - clk );
+ //ABC_PRT( "Clauses", Abc_Clock() - clk );
// check clauses using BMC
if ( fBmc )
{
- clk = clock();
+ clk = Abc_Clock();
Counter = Fra_ClausBmcClauses( p );
p->nClauses -= Counter;
if ( fVerbose )
{
printf( "BMC disproved %d clauses. ", Counter );
- ABC_PRT( "Time", clock() - clk );
+ ABC_PRT( "Time", Abc_Clock() - clk );
}
}
// prove clauses inductively
- clkInd = clk = clock();
+ clkInd = clk = Abc_Clock();
Counter = 1;
for ( Iter = 0; Counter > 0; Iter++ )
{
@@ -1800,9 +1800,9 @@ clk = clock();
{
printf( "End = %5d. Exs = %5d. ", p->nClauses, p->nCexes );
// printf( "\n" );
- ABC_PRT( "Time", clock() - clk );
+ ABC_PRT( "Time", Abc_Clock() - clk );
}
- clk = clock();
+ clk = Abc_Clock();
}
// add proved clauses to storage
Fra_ClausAddToStorage( p );
@@ -1815,14 +1815,14 @@ clk = clock();
printf( "Property FAILS during refinement. " );
else
printf( "Property HOLDS inductively after strengthening. " );
- ABC_PRT( "Time ", clock() - clkTotal );
+ ABC_PRT( "Time ", Abc_Clock() - clkTotal );
if ( !p->fFail )
break;
}
else
{
printf( "Finished proving inductive clauses. " );
- ABC_PRT( "Time ", clock() - clkTotal );
+ ABC_PRT( "Time ", Abc_Clock() - clkTotal );
}
}
@@ -1857,8 +1857,8 @@ clk = clock();
fprintf( pTable, "%d ", p->nClauses );
fprintf( pTable, "%d ", Iter );
fprintf( pTable, "%.2f ", (float)(clkInd-clkTotal)/(float)(CLOCKS_PER_SEC) );
- fprintf( pTable, "%.2f ", (float)(clock()-clkInd)/(float)(CLOCKS_PER_SEC) );
- fprintf( pTable, "%.2f ", (float)(clock()-clkTotal)/(float)(CLOCKS_PER_SEC) );
+ fprintf( pTable, "%.2f ", (float)(Abc_Clock()-clkInd)/(float)(CLOCKS_PER_SEC) );
+ fprintf( pTable, "%.2f ", (float)(Abc_Clock()-clkTotal)/(float)(CLOCKS_PER_SEC) );
fprintf( pTable, "\n" );
fclose( pTable );
}
diff --git a/src/proof/fra/fraCore.c b/src/proof/fra/fraCore.c
index 35888f43..1e517e7d 100644
--- a/src/proof/fra/fraCore.c
+++ b/src/proof/fra/fraCore.c
@@ -376,10 +376,10 @@ Aig_Man_t * Fra_FraigPerform( Aig_Man_t * pManAig, Fra_Par_t * pPars )
{
Fra_Man_t * p;
Aig_Man_t * pManAigNew;
- clock_t clk;
+ abctime clk;
if ( Aig_ManNodeNum(pManAig) == 0 )
return Aig_ManDupOrdered(pManAig);
-clk = clock();
+clk = Abc_Clock();
p = Fra_ManStart( pManAig, pPars );
p->pManFraig = Fra_ManPrepareComb( p );
p->pSml = Fra_SmlStart( pManAig, 0, 1, pPars->nSimWords );
@@ -402,7 +402,7 @@ Fra_ClassesPrint( p->pCla, 1 );
Fra_ManFinalizeComb( p );
if ( p->pPars->fChoicing )
{
-clock_t clk2 = clock();
+abctime clk2 = Abc_Clock();
Fra_ClassesCopyReprs( p->pCla, p->vTimeouts );
pManAigNew = Aig_ManDupRepr( p->pManAig, 1 );
Aig_ManReprStart( pManAigNew, Aig_ManObjNumMax(pManAigNew) );
@@ -410,7 +410,7 @@ clock_t clk2 = clock();
Aig_ManMarkValidChoices( pManAigNew );
Aig_ManStop( p->pManFraig );
p->pManFraig = NULL;
-p->timeTrav += clock() - clk2;
+p->timeTrav += Abc_Clock() - clk2;
}
else
{
@@ -419,7 +419,7 @@ p->timeTrav += clock() - clk2;
pManAigNew = p->pManFraig;
p->pManFraig = NULL;
}
-p->timeTotal = clock() - clk;
+p->timeTotal = Abc_Clock() - clk;
// collect final stats
p->nLitsEnd = Fra_ClassesCountLits( p->pCla );
p->nNodesEnd = Aig_ManNodeNum(pManAigNew);
diff --git a/src/proof/fra/fraHot.c b/src/proof/fra/fraHot.c
index a91c939f..36bea9e7 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;
- clock_t clk = clock();
+ abctime clk = Abc_Clock();
// generate random sim-info at register outputs
vSimInfo = Vec_PtrAllocSimInfo( nRegs + 1, nSimWords );
@@ -381,7 +381,7 @@ void Fra_OneHotEstimateCoverage( Fra_Man_t * p, Vec_Int_t * vOneHots )
// print the result
printf( "Care states ratio = %f. ", 1.0 * (nSimWords * 32 - nCovered) / (nSimWords * 32) );
printf( "(%d out of %d patterns) ", nSimWords * 32 - nCovered, nSimWords * 32 );
- ABC_PRT( "Time", clock() - clk );
+ ABC_PRT( "Time", Abc_Clock() - clk );
}
/**Function*************************************************************
diff --git a/src/proof/fra/fraImp.c b/src/proof/fra/fraImp.c
index 809ad8e4..027d8eb2 100644
--- a/src/proof/fra/fraImp.c
+++ b/src/proof/fra/fraImp.c
@@ -328,7 +328,7 @@ Vec_Int_t * Fra_ImpDerive( Fra_Man_t * p, int nImpMaxLimit, int nImpUseLimit, in
int nImpsTotal = 0, nImpsTried = 0, nImpsNonSeq = 0, nImpsComb = 0, nImpsCollected = 0;
int CostMin = ABC_INFINITY, CostMax = 0;
int i, k, Imp, CostRange;
- clock_t clk = clock();
+ abctime clk = Abc_Clock();
assert( Aig_ManObjNumMax(p->pManAig) < (1 << 15) );
assert( nImpMaxLimit > 0 && nImpUseLimit > 0 && nImpUseLimit <= nImpMaxLimit );
// normalize both managers
@@ -403,7 +403,7 @@ printf( "Implications: All = %d. Try = %d. NonSeq = %d. Comb = %d. Res = %d.\n",
nImpsTotal, nImpsTried, nImpsNonSeq, nImpsComb, nImpsCollected );
printf( "Implication weight: Min = %d. Pivot = %d. Max = %d. ",
CostMin, CostRange, CostMax );
-ABC_PRT( "Time", clock() - clk );
+ABC_PRT( "Time", Abc_Clock() - clk );
}
return vImps;
}
diff --git a/src/proof/fra/fraInd.c b/src/proof/fra/fraInd.c
index e0a54a4e..012f8fc8 100644
--- a/src/proof/fra/fraInd.c
+++ b/src/proof/fra/fraInd.c
@@ -50,7 +50,7 @@ void Fra_FraigInductionRewrite( Fra_Man_t * p )
Aig_Man_t * pTemp;
Aig_Obj_t * pObj, * pObjPo;
int nTruePis, k, i;
- clock_t clk = clock();
+ abctime clk = Abc_Clock();
// perform AIG rewriting on the speculated frames
// pTemp = Dar_ManRwsat( pTemp, 1, 0 );
pTemp = Dar_ManRewriteDefault( p->pManFraig );
@@ -77,7 +77,7 @@ void Fra_FraigInductionRewrite( Fra_Man_t * p )
// exchange
Aig_ManStop( p->pManFraig );
p->pManFraig = pTemp;
-p->timeRwr += clock() - clk;
+p->timeRwr += Abc_Clock() - clk;
}
/**Function*************************************************************
@@ -260,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;
- clock_t clk = clock();
+ abctime clk = Abc_Clock();
// save parameters
nPartSize = pPars->nPartSize; pPars->nPartSize = 0;
@@ -325,7 +325,7 @@ Aig_Man_t * Fra_FraigInductionPart( Aig_Man_t * pAig, Fra_Ssw_t * pPars )
pPars->fVerbose = fVerbose;
if ( fVerbose )
{
- ABC_PRT( "Total time", clock() - clk );
+ ABC_PRT( "Total time", Abc_Clock() - clk );
}
return pNew;
}
@@ -359,8 +359,8 @@ Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, Fra_Ssw_t * pParams )
int nNodesBeg, nRegsBeg;
int nIter = -1; // Suppress "might be used uninitialized"
int i;
- clock_t clk = clock(), clk2;
- clock_t TimeToStop = pParams->TimeLimit ? pParams->TimeLimit * CLOCKS_PER_SEC + clock() : 0;
+ abctime clk = Abc_Clock(), clk2;
+ abctime TimeToStop = pParams->TimeLimit ? pParams->TimeLimit * CLOCKS_PER_SEC + Abc_Clock() : 0;
if ( Aig_ManNodeNum(pManAig) == 0 )
{
@@ -429,7 +429,7 @@ printf( "Simulating %d AIG nodes for %d cycles ... ", Aig_ManNodeNum(pManAig), p
p->pSml = Fra_SmlSimulateSeq( pManAig, pPars->nFramesP, 32, 1, 1 ); //pPars->nFramesK + 1, 1 );
if ( pPars->fVerbose )
{
-ABC_PRT( "Time", clock() - clk );
+ABC_PRT( "Time", Abc_Clock() - clk );
}
Fra_ClassesPrepare( p->pCla, p->pPars->fLatchCorr, p->pPars->nMaxLevs );
// Fra_ClassesPostprocess( p->pCla );
@@ -445,7 +445,7 @@ ABC_PRT( "Time", clock() - clk );
if ( pPars->fUseImps )
p->pCla->vImps = Fra_ImpDerive( p, 5000000, pPars->nMaxImps, pPars->fLatchCorr );
- if ( pParams->TimeLimit != 0.0 && clock() > TimeToStop )
+ if ( pParams->TimeLimit != 0.0 && Abc_Clock() > TimeToStop )
{
if ( !pParams->fSilent )
printf( "Fra_FraigInduction(): Runtime limit exceeded.\n" );
@@ -475,9 +475,9 @@ 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;
- clock_t clk3 = clock();
+ abctime clk3 = Abc_Clock();
- if ( pParams->TimeLimit != 0.0 && clock() > TimeToStop )
+ if ( pParams->TimeLimit != 0.0 && Abc_Clock() > TimeToStop )
{
if ( !pParams->fSilent )
printf( "Fra_FraigInduction(): Runtime limit exceeded.\n" );
@@ -487,9 +487,9 @@ ABC_PRT( "Time", clock() - clk );
// mark the classes as non-refined
p->pCla->fRefinement = 0;
// derive non-init K-timeframes while implementing e-classes
-clk2 = clock();
+clk2 = Abc_Clock();
p->pManFraig = Fra_FramesWithClasses( p );
-p->timeTrav += clock() - clk2;
+p->timeTrav += Abc_Clock() - clk2;
//Aig_ManDumpBlif( p->pManFraig, "testaig.blif", NULL, NULL );
// perform AIG rewriting
@@ -556,13 +556,13 @@ p->timeTrav += clock() - clk2;
// perform sweeping
p->nSatCallsRecent = 0;
p->nSatCallsSkipped = 0;
-clk2 = clock();
+clk2 = Abc_Clock();
if ( p->pPars->fUse1Hot )
Fra_OneHotCheck( p, p->vOneHots );
Fra_FraigSweep( p );
if ( pPars->fVerbose )
{
- ABC_PRT( "T", clock() - clk3 );
+ ABC_PRT( "T", Abc_Clock() - clk3 );
}
// Sat_SolverPrintStats( stdout, p->pSat );
@@ -591,17 +591,17 @@ clk2 = clock();
if ( p->pCla->vImps && Vec_IntSize(p->pCla->vImps) )
{
int Temp;
- clock_t clk = clock();
+ abctime clk = Abc_Clock();
if ( Temp = Fra_ImpVerifyUsingSimulation( p ) )
printf( "Implications failing the simulation test = %d (out of %d). ", Temp, Vec_IntSize(p->pCla->vImps) );
else
printf( "All %d implications have passed the simulation test. ", Vec_IntSize(p->pCla->vImps) );
- ABC_PRT( "Time", clock() - clk );
+ ABC_PRT( "Time", Abc_Clock() - clk );
}
*/
// move the classes into representatives and reduce AIG
-clk2 = clock();
+clk2 = Abc_Clock();
if ( p->pPars->fWriteImps && p->vOneHots && Fra_OneHotCount(p, p->vOneHots) )
{
extern void Ioa_WriteAiger( Aig_Man_t * pMan, char * pFileName, int fWriteSymbols, int fCompact );
@@ -630,8 +630,8 @@ clk2 = clock();
// if ( pObj->pData && Aig_ObjIsNone(pObj->pData) )
// pObj->pData = NULL;
// Aig_ManCountMergeRegs( pManAigNew );
-p->timeTrav += clock() - clk2;
-p->timeTotal = clock() - clk;
+p->timeTrav += Abc_Clock() - clk2;
+p->timeTotal = Abc_Clock() - clk;
// get the final stats
p->nLitsEnd = Fra_ClassesCountLits( p->pCla );
p->nNodesEnd = Aig_ManNodeNum(pManAigNew);
diff --git a/src/proof/fra/fraIndVer.c b/src/proof/fra/fraIndVer.c
index 26b64647..a219ec52 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;
- clock_t clk = clock();
+ abctime clk = Abc_Clock();
if ( nFrames != 1 )
{
@@ -153,7 +153,7 @@ int Fra_InvariantVerify( Aig_Man_t * pAig, int nFrames, Vec_Int_t * vClauses, Ve
if ( CounterBase || CounterInd )
return 0;
printf( "Invariant verification: %d clauses verified correctly. ", Vec_IntSize(vClauses) );
- ABC_PRT( "Time", clock() - clk );
+ ABC_PRT( "Time", Abc_Clock() - clk );
return 1;
}
diff --git a/src/proof/fra/fraLcr.c b/src/proof/fra/fraLcr.c
index 9d573bee..2d8b3d64 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
- clock_t timeSim;
- clock_t timePart;
- clock_t timeTrav;
- clock_t timeFraig;
- clock_t timeUpdate;
- clock_t timeTotal;
+ abctime timeSim;
+ abctime timePart;
+ abctime timeTrav;
+ abctime timeFraig;
+ abctime timeUpdate;
+ abctime timeTotal;
};
////////////////////////////////////////////////////////////////////////
@@ -538,8 +538,8 @@ Aig_Man_t * Fra_FraigLatchCorrespondence( Aig_Man_t * pAig, int nFramesP, int nC
Aig_Man_t * pAigPart, * pAigTemp, * pAigNew = NULL;
Vec_Int_t * vPart;
int i, nIter;
- clock_t timeSim, clk2, clk3, clk = clock();
- clock_t TimeToStop = TimeLimit ? TimeLimit * CLOCKS_PER_SEC + clock() : 0;
+ abctime timeSim, clk2, clk3, clk = Abc_Clock();
+ abctime TimeToStop = TimeLimit ? TimeLimit * CLOCKS_PER_SEC + Abc_Clock() : 0;
if ( Aig_ManNodeNum(pAig) == 0 )
{
if ( pnIter ) *pnIter = 0;
@@ -550,15 +550,15 @@ Aig_Man_t * Fra_FraigLatchCorrespondence( Aig_Man_t * pAig, int nFramesP, int nC
assert( Aig_ManRegNum(pAig) > 0 );
// simulate the AIG
-clk2 = clock();
+clk2 = Abc_Clock();
if ( fVerbose )
printf( "Simulating AIG with %d nodes for %d cycles ... ", Aig_ManNodeNum(pAig), nFramesP + 32 );
pSml = Fra_SmlSimulateSeq( pAig, nFramesP, 32, 1, 1 );
if ( fVerbose )
{
-ABC_PRT( "Time", clock() - clk2 );
+ABC_PRT( "Time", Abc_Clock() - clk2 );
}
-timeSim = clock() - clk2;
+timeSim = Abc_Clock() - clk2;
// check if simulation discovered non-constant-0 POs
if ( fProve && pSml->fNonConstOut )
@@ -586,7 +586,7 @@ timeSim = clock() - clk2;
Fra_SmlStop( pTemp->pSml );
// partition the AIG for latch correspondence computation
-clk2 = clock();
+clk2 = Abc_Clock();
if ( fVerbose )
printf( "Partitioning AIG ... " );
pAigPart = Fra_LcrDeriveAigForPartitioning( p );
@@ -595,8 +595,8 @@ printf( "Partitioning AIG ... " );
Aig_ManStop( pAigPart );
if ( fVerbose )
{
-ABC_PRT( "Time", clock() - clk2 );
-p->timePart += clock() - clk2;
+ABC_PRT( "Time", Abc_Clock() - clk2 );
+p->timePart += Abc_Clock() - clk2;
}
// get the initial stats
@@ -609,13 +609,13 @@ p->timePart += clock() - clk2;
for ( nIter = 0; p->fRefining; nIter++ )
{
p->fRefining = 0;
- clk3 = clock();
+ clk3 = Abc_Clock();
// derive AIGs for each partition
Fra_ClassNodesMark( p );
Vec_PtrClear( p->vFraigs );
Vec_PtrForEachEntry( Vec_Int_t *, p->vParts, vPart, i )
{
- if ( TimeLimit != 0.0 && clock() > TimeToStop )
+ if ( TimeLimit != 0.0 && Abc_Clock() > TimeToStop )
{
Vec_PtrForEachEntry( Aig_Man_t *, p->vFraigs, pAigPart, i )
Aig_ManStop( pAigPart );
@@ -624,12 +624,12 @@ p->timePart += clock() - clk2;
printf( "Fra_FraigLatchCorrespondence(): Runtime limit exceeded.\n" );
goto finish;
}
-clk2 = clock();
+clk2 = Abc_Clock();
pAigPart = Fra_LcrCreatePart( p, vPart );
-p->timeTrav += clock() - clk2;
-clk2 = clock();
+p->timeTrav += Abc_Clock() - clk2;
+clk2 = Abc_Clock();
pAigTemp = Fra_FraigEquivence( pAigPart, nConfMax, 0 );
-p->timeFraig += clock() - clk2;
+p->timeFraig += Abc_Clock() - clk2;
Vec_PtrPush( p->vFraigs, pAigTemp );
/*
{
@@ -638,7 +638,7 @@ p->timeFraig += clock() - clk2;
Aig_ManDumpBlif( pAigPart, Name, NULL, NULL );
}
printf( "Finished part %4d (out of %4d). ", i, Vec_PtrSize(p->vParts) );
-ABC_PRT( "Time", clock() - clk3 );
+ABC_PRT( "Time", Abc_Clock() - clk3 );
*/
Aig_ManStop( pAigPart );
@@ -650,7 +650,7 @@ ABC_PRT( "Time", clock() - clk3 );
printf( "%3d : Const = %6d. Class = %6d. L = %6d. Part = %3d. ",
nIter, Vec_PtrSize(p->pCla->vClasses1), Vec_PtrSize(p->pCla->vClasses),
Fra_ClassesCountLits(p->pCla), Vec_PtrSize(p->vParts) );
- ABC_PRT( "T", clock() - clk3 );
+ ABC_PRT( "T", Abc_Clock() - clk3 );
}
// refine the classes
Fra_LcrAigPrepareTwo( p->pAig, pTemp );
@@ -665,19 +665,19 @@ ABC_PRT( "Time", clock() - clk3 );
// repartition if needed
if ( 1 )
{
-clk2 = clock();
+clk2 = Abc_Clock();
Vec_VecFree( (Vec_Vec_t *)p->vParts );
pAigPart = Fra_LcrDeriveAigForPartitioning( p );
p->vParts = (Vec_Ptr_t *)Aig_ManPartitionSmart( pAigPart, nPartSize, 0, NULL );
Fra_LcrRemapPartitions( p->vParts, p->pCla, p->pInToOutPart, p->pInToOutNum );
Aig_ManStop( pAigPart );
-p->timePart += clock() - clk2;
+p->timePart += Abc_Clock() - clk2;
}
}
p->nIters = nIter;
// move the classes into representatives and reduce AIG
-clk2 = clock();
+clk2 = Abc_Clock();
// Fra_ClassesPrint( p->pCla, 1 );
if ( fReprSelect )
Fra_ClassesSelectRepr( p->pCla );
@@ -685,8 +685,8 @@ clk2 = clock();
pAigNew = Aig_ManDupRepr( p->pAig, 0 );
Aig_ManSeqCleanup( pAigNew );
// Aig_ManCountMergeRegs( pAigNew );
-p->timeUpdate += clock() - clk2;
-p->timeTotal = clock() - clk;
+p->timeUpdate += Abc_Clock() - clk2;
+p->timeTotal = Abc_Clock() - clk;
// get the final stats
p->nLitsEnd = Fra_ClassesCountLits( p->pCla );
p->nNodesEnd = Aig_ManNodeNum(pAigNew);
diff --git a/src/proof/fra/fraPart.c b/src/proof/fra/fraPart.c
index e1c8ddf4..34d6cce2 100644
--- a/src/proof/fra/fraPart.c
+++ b/src/proof/fra/fraPart.c
@@ -53,16 +53,16 @@ void Fra_ManPartitionTest( Aig_Man_t * p, int nComLim )
int i, k, nCommon, CountOver, CountQuant;
int nTotalSupp, nTotalSupp2, Entry, Largest;//, iVar;
double Ratio, R;
- clock_t clk;
+ abctime clk;
nTotalSupp = 0;
nTotalSupp2 = 0;
Ratio = 0.0;
// compute supports
-clk = clock();
+clk = Abc_Clock();
vSupps = (Vec_Vec_t *)Aig_ManSupports( p );
-ABC_PRT( "Supports", clock() - clk );
+ABC_PRT( "Supports", Abc_Clock() - clk );
// remove last entry
Aig_ManForEachCo( p, pObj, i )
{
@@ -73,7 +73,7 @@ ABC_PRT( "Supports", clock() - clk );
}
// create reverse supports
-clk = clock();
+clk = Abc_Clock();
vSuppsIn = Vec_VecStart( Aig_ManCiNum(p) );
Aig_ManForEachCo( p, pObj, i )
{
@@ -81,9 +81,9 @@ clk = clock();
Vec_IntForEachEntry( vSup, Entry, k )
Vec_VecPush( vSuppsIn, Entry, (void *)(ABC_PTRUINT_T)i );
}
-ABC_PRT( "Inverse ", clock() - clk );
+ABC_PRT( "Inverse ", Abc_Clock() - clk );
-clk = clock();
+clk = Abc_Clock();
// compute extended supports
Largest = 0;
vSuppsNew = Vec_PtrAlloc( Aig_ManCoNum(p) );
@@ -156,7 +156,7 @@ clk = clock();
*/
}
// Bar_ProgressStop( pProgress );
-ABC_PRT( "Scanning", clock() - clk );
+ABC_PRT( "Scanning", Abc_Clock() - clk );
// print cumulative statistics
printf( "PIs = %6d. POs = %6d. Lim = %3d. AveS = %3d. SN = %3d. R = %4.2f Max = %5d.\n",
@@ -191,13 +191,13 @@ void Fra_ManPartitionTest2( Aig_Man_t * p )
Aig_Obj_t * pObj;
int Entry, Entry2, Entry3, Counter;
int i, k, m, n;
- clock_t clk;
+ abctime clk;
char * pSupp;
// compute supports
-clk = clock();
+clk = Abc_Clock();
vSupps = (Vec_Vec_t *)Aig_ManSupports( p );
-ABC_PRT( "Supports", clock() - clk );
+ABC_PRT( "Supports", Abc_Clock() - clk );
// remove last entry
Aig_ManForEachCo( p, pObj, i )
{
@@ -208,7 +208,7 @@ ABC_PRT( "Supports", clock() - clk );
}
// create reverse supports
-clk = clock();
+clk = Abc_Clock();
vSuppsIn = Vec_VecStart( Aig_ManCiNum(p) );
Aig_ManForEachCo( p, pObj, i )
{
@@ -218,10 +218,10 @@ clk = clock();
Vec_IntForEachEntry( vSup, Entry, k )
Vec_VecPush( vSuppsIn, Entry, (void *)(ABC_PTRUINT_T)i );
}
-ABC_PRT( "Inverse ", clock() - clk );
+ABC_PRT( "Inverse ", Abc_Clock() - clk );
// create affective supports
-clk = clock();
+clk = Abc_Clock();
pSupp = ABC_ALLOC( char, Aig_ManCiNum(p) );
Aig_ManForEachCo( p, pObj, i )
{
@@ -252,7 +252,7 @@ clk = clock();
printf( "%d(%d) ", Vec_IntSize(vSup), Counter );
}
printf( "\n" );
-ABC_PRT( "Extension ", clock() - clk );
+ABC_PRT( "Extension ", Abc_Clock() - clk );
ABC_FREE( pSupp );
Vec_VecFree( vSupps );
diff --git a/src/proof/fra/fraSat.c b/src/proof/fra/fraSat.c
index fc95fd62..e1e1c57f 100644
--- a/src/proof/fra/fraSat.c
+++ b/src/proof/fra/fraSat.c
@@ -48,7 +48,7 @@ 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;
- clock_t clk;//, clk2 = clock();
+ abctime clk;//, clk2 = Abc_Clock();
int status;
// make sure the nodes are not complemented
@@ -100,17 +100,17 @@ int Fra_NodesAreEquiv( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew )
// solve under assumptions
// A = 1; B = 0 OR A = 1; B = 1
-clk = clock();
+clk = Abc_Clock();
pLits[0] = toLitCond( Fra_ObjSatNum(pOld), 0 );
pLits[1] = toLitCond( Fra_ObjSatNum(pNew), pOld->fPhase == pNew->fPhase );
//Sat_SolverWriteDimacs( p->pSat, "temp.cnf", pLits, pLits + 2, 1 );
RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 2,
(ABC_INT64_T)nBTLimit, (ABC_INT64_T)0,
p->nBTLimitGlobal, p->nInsLimitGlobal );
-p->timeSat += clock() - clk;
+p->timeSat += Abc_Clock() - clk;
if ( RetValue1 == l_False )
{
-p->timeSatUnsat += clock() - clk;
+p->timeSatUnsat += Abc_Clock() - clk;
pLits[0] = lit_neg( pLits[0] );
pLits[1] = lit_neg( pLits[1] );
RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
@@ -120,14 +120,14 @@ p->timeSatUnsat += clock() - clk;
}
else if ( RetValue1 == l_True )
{
-p->timeSatSat += clock() - clk;
+p->timeSatSat += Abc_Clock() - clk;
Fra_SmlSavePattern( p );
p->nSatCallsSat++;
return 0;
}
else // if ( RetValue1 == l_Undef )
{
-p->timeSatFail += clock() - clk;
+p->timeSatFail += Abc_Clock() - clk;
// mark the node as the failed node
if ( pOld != p->pManFraig->pConst1 )
pOld->fMarkB = 1;
@@ -145,16 +145,16 @@ p->timeSatFail += clock() - clk;
// solve under assumptions
// A = 0; B = 1 OR A = 0; B = 0
-clk = clock();
+clk = Abc_Clock();
pLits[0] = toLitCond( Fra_ObjSatNum(pOld), 1 );
pLits[1] = toLitCond( Fra_ObjSatNum(pNew), pOld->fPhase ^ pNew->fPhase );
RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 2,
(ABC_INT64_T)nBTLimit, (ABC_INT64_T)0,
p->nBTLimitGlobal, p->nInsLimitGlobal );
-p->timeSat += clock() - clk;
+p->timeSat += Abc_Clock() - clk;
if ( RetValue1 == l_False )
{
-p->timeSatUnsat += clock() - clk;
+p->timeSatUnsat += Abc_Clock() - clk;
pLits[0] = lit_neg( pLits[0] );
pLits[1] = lit_neg( pLits[1] );
RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
@@ -163,14 +163,14 @@ p->timeSatUnsat += clock() - clk;
}
else if ( RetValue1 == l_True )
{
-p->timeSatSat += clock() - clk;
+p->timeSatSat += Abc_Clock() - clk;
Fra_SmlSavePattern( p );
p->nSatCallsSat++;
return 0;
}
else // if ( RetValue1 == l_Undef )
{
-p->timeSatFail += clock() - clk;
+p->timeSatFail += Abc_Clock() - clk;
// mark the node as the failed node
pOld->fMarkB = 1;
pNew->fMarkB = 1;
@@ -181,12 +181,12 @@ p->timeSatFail += clock() - clk;
// check BDD proof
{
int RetVal;
- ABC_PRT( "Sat", clock() - clk2 );
- clk2 = clock();
+ ABC_PRT( "Sat", Abc_Clock() - clk2 );
+ clk2 = Abc_Clock();
RetVal = Fra_NodesAreEquivBdd( pOld, pNew );
// printf( "%d ", RetVal );
assert( RetVal );
- ABC_PRT( "Bdd", clock() - clk2 );
+ ABC_PRT( "Bdd", Abc_Clock() - clk2 );
printf( "\n" );
}
*/
@@ -209,7 +209,7 @@ 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;
- clock_t clk;//, clk2 = clock();
+ abctime clk;//, clk2 = Abc_Clock();
int status;
// make sure the nodes are not complemented
@@ -261,7 +261,7 @@ int Fra_NodesAreImp( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew, int fCom
// solve under assumptions
// A = 1; B = 0 OR A = 1; B = 1
-clk = clock();
+clk = Abc_Clock();
// pLits[0] = toLitCond( Fra_ObjSatNum(pOld), 0 );
// pLits[1] = toLitCond( Fra_ObjSatNum(pNew), pOld->fPhase == pNew->fPhase );
pLits[0] = toLitCond( Fra_ObjSatNum(pOld), fComplL );
@@ -270,10 +270,10 @@ clk = clock();
RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 2,
(ABC_INT64_T)nBTLimit, (ABC_INT64_T)0,
p->nBTLimitGlobal, p->nInsLimitGlobal );
-p->timeSat += clock() - clk;
+p->timeSat += Abc_Clock() - clk;
if ( RetValue1 == l_False )
{
-p->timeSatUnsat += clock() - clk;
+p->timeSatUnsat += Abc_Clock() - clk;
pLits[0] = lit_neg( pLits[0] );
pLits[1] = lit_neg( pLits[1] );
RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
@@ -283,14 +283,14 @@ p->timeSatUnsat += clock() - clk;
}
else if ( RetValue1 == l_True )
{
-p->timeSatSat += clock() - clk;
+p->timeSatSat += Abc_Clock() - clk;
Fra_SmlSavePattern( p );
p->nSatCallsSat++;
return 0;
}
else // if ( RetValue1 == l_Undef )
{
-p->timeSatFail += clock() - clk;
+p->timeSatFail += Abc_Clock() - clk;
// mark the node as the failed node
if ( pOld != p->pManFraig->pConst1 )
pOld->fMarkB = 1;
@@ -317,7 +317,7 @@ 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;
- clock_t clk;//, clk2 = clock();
+ abctime clk;//, clk2 = Abc_Clock();
int status;
// make sure the nodes are not complemented
@@ -369,7 +369,7 @@ int Fra_NodesAreClause( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew, int f
// solve under assumptions
// A = 1; B = 0 OR A = 1; B = 1
-clk = clock();
+clk = Abc_Clock();
// pLits[0] = toLitCond( Fra_ObjSatNum(pOld), 0 );
// pLits[1] = toLitCond( Fra_ObjSatNum(pNew), pOld->fPhase == pNew->fPhase );
pLits[0] = toLitCond( Fra_ObjSatNum(pOld), !fComplL );
@@ -378,10 +378,10 @@ clk = clock();
RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 2,
(ABC_INT64_T)nBTLimit, (ABC_INT64_T)0,
p->nBTLimitGlobal, p->nInsLimitGlobal );
-p->timeSat += clock() - clk;
+p->timeSat += Abc_Clock() - clk;
if ( RetValue1 == l_False )
{
-p->timeSatUnsat += clock() - clk;
+p->timeSatUnsat += Abc_Clock() - clk;
pLits[0] = lit_neg( pLits[0] );
pLits[1] = lit_neg( pLits[1] );
RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
@@ -391,14 +391,14 @@ p->timeSatUnsat += clock() - clk;
}
else if ( RetValue1 == l_True )
{
-p->timeSatSat += clock() - clk;
+p->timeSatSat += Abc_Clock() - clk;
Fra_SmlSavePattern( p );
p->nSatCallsSat++;
return 0;
}
else // if ( RetValue1 == l_Undef )
{
-p->timeSatFail += clock() - clk;
+p->timeSatFail += Abc_Clock() - clk;
// mark the node as the failed node
if ( pOld != p->pManFraig->pConst1 )
pOld->fMarkB = 1;
@@ -425,7 +425,7 @@ p->timeSatFail += clock() - clk;
int Fra_NodeIsConst( Fra_Man_t * p, Aig_Obj_t * pNew )
{
int pLits[2], RetValue1, RetValue;
- clock_t clk;
+ abctime clk;
// make sure the nodes are not complemented
assert( !Aig_IsComplement(pNew) );
@@ -451,15 +451,15 @@ int Fra_NodeIsConst( Fra_Man_t * p, Aig_Obj_t * pNew )
Fra_SetActivityFactors( p, NULL, pNew );
// solve under assumptions
-clk = clock();
+clk = Abc_Clock();
pLits[0] = toLitCond( Fra_ObjSatNum(pNew), pNew->fPhase );
RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 1,
(ABC_INT64_T)p->pPars->nBTLimitMiter, (ABC_INT64_T)0,
p->nBTLimitGlobal, p->nInsLimitGlobal );
-p->timeSat += clock() - clk;
+p->timeSat += Abc_Clock() - clk;
if ( RetValue1 == l_False )
{
-p->timeSatUnsat += clock() - clk;
+p->timeSatUnsat += Abc_Clock() - clk;
pLits[0] = lit_neg( pLits[0] );
RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 1 );
assert( RetValue );
@@ -468,7 +468,7 @@ p->timeSatUnsat += clock() - clk;
}
else if ( RetValue1 == l_True )
{
-p->timeSatSat += clock() - clk;
+p->timeSatSat += Abc_Clock() - clk;
if ( p->pPatWords )
Fra_SmlSavePattern( p );
p->nSatCallsSat++;
@@ -476,7 +476,7 @@ p->timeSatSat += clock() - clk;
}
else // if ( RetValue1 == l_Undef )
{
-p->timeSatFail += clock() - clk;
+p->timeSatFail += Abc_Clock() - clk;
// mark the node as the failed node
pNew->fMarkB = 1;
p->nSatFailsReal++;
@@ -540,9 +540,9 @@ 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 LevelMin, LevelMax;
- clock_t clk;
+ abctime clk;
assert( pOld || pNew );
-clk = clock();
+clk = Abc_Clock();
// reset the active variables
veci_resize(&p->pSat->act_vars, 0);
// prepare for traversal
@@ -557,7 +557,7 @@ clk = clock();
if ( pNew && !Aig_ObjIsConst1(pNew) )
Fra_SetActivityFactors_rec( p, pNew, LevelMin, LevelMax );
//Fra_PrintActivity( p );
-p->timeTrav += clock() - clk;
+p->timeTrav += Abc_Clock() - clk;
return 1;
}
diff --git a/src/proof/fra/fraSec.c b/src/proof/fra/fraSec.c
index 04c9d668..dea2c3dc 100644
--- a/src/proof/fra/fraSec.c
+++ b/src/proof/fra/fraSec.c
@@ -99,7 +99,7 @@ int Fra_FraigSec( Aig_Man_t * p, Fra_Sec_t * pParSec, Aig_Man_t ** ppResult )
Fra_Sml_t * pSml;
Aig_Man_t * pNew, * pTemp;
int nFrames, RetValue, nIter;
- clock_t clk, clkTotal = clock();
+ abctime clk, clkTotal = Abc_Clock();
int TimeOut = 0;
int fLatchCorr = 0;
float TimeLeft = 0.0;
@@ -123,7 +123,7 @@ int Fra_FraigSec( Aig_Man_t * p, Fra_Sec_t * pParSec, Aig_Man_t ** ppResult )
//Aig_ManDumpBlif( pNew, "after.blif", NULL, NULL );
// perform sequential cleanup
-clk = clock();
+clk = Abc_Clock();
if ( pNew->nRegs )
pNew = Aig_ManReduceLaches( pNew, 0 );
if ( pNew->nRegs )
@@ -132,14 +132,14 @@ clk = clock();
{
printf( "Sequential cleanup: Latches = %5d. Nodes = %6d. ",
Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
-ABC_PRT( "Time", clock() - clk );
+ABC_PRT( "Time", Abc_Clock() - clk );
}
RetValue = Fra_FraigMiterStatus( pNew );
if ( RetValue >= 0 )
goto finish;
// perform phase abstraction
-clk = clock();
+clk = Abc_Clock();
if ( pParSec->fPhaseAbstract )
{
extern Aig_Man_t * Saig_ManPhaseAbstractAuto( Aig_Man_t * p, int fVerbose );
@@ -151,14 +151,14 @@ clk = clock();
{
printf( "Phase abstraction: Latches = %5d. Nodes = %6d. ",
Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
-ABC_PRT( "Time", clock() - clk );
+ABC_PRT( "Time", Abc_Clock() - clk );
}
}
// perform forward retiming
if ( pParSec->fRetimeFirst && pNew->nRegs )
{
-clk = clock();
+clk = Abc_Clock();
// pNew = Rtm_ManRetime( pTemp = pNew, 1, 1000, 0 );
pNew = Saig_ManRetimeForward( pTemp = pNew, 100, 0 );
Aig_ManStop( pTemp );
@@ -166,12 +166,12 @@ clk = clock();
{
printf( "Forward retiming: Latches = %5d. Nodes = %6d. ",
Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
-ABC_PRT( "Time", clock() - clk );
+ABC_PRT( "Time", Abc_Clock() - clk );
}
}
// run latch correspondence
-clk = clock();
+clk = Abc_Clock();
if ( pNew->nRegs )
{
pNew = Aig_ManDupOrdered( pTemp = pNew );
@@ -180,7 +180,7 @@ clk = clock();
/*
if ( RetValue == -1 && pParSec->TimeLimit )
{
- TimeLeft = (float)pParSec->TimeLimit - ((float)(clock()-clkTotal)/(float)(CLOCKS_PER_SEC));
+ TimeLeft = (float)pParSec->TimeLimit - ((float)(Abc_Clock()-clkTotal)/(float)(CLOCKS_PER_SEC));
TimeLeft = Abc_MaxInt( TimeLeft, 0.0 );
if ( TimeLeft == 0.0 )
{
@@ -223,12 +223,12 @@ clk = clock();
if ( !pParSec->fSilent )
{
printf( "Networks are NOT EQUIVALENT after simulation. " );
-ABC_PRT( "Time", clock() - clkTotal );
+ABC_PRT( "Time", Abc_Clock() - clkTotal );
}
if ( pParSec->fReportSolution && !pParSec->fRecursive )
{
printf( "SOLUTION: FAIL " );
-ABC_PRT( "Time", clock() - clkTotal );
+ABC_PRT( "Time", Abc_Clock() - clkTotal );
}
Aig_ManStop( pTemp );
return RetValue;
@@ -244,13 +244,13 @@ ABC_PRT( "Time", clock() - clkTotal );
{
printf( "Latch-corr (I=%3d): Latches = %5d. Nodes = %6d. ",
nIter, Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
-ABC_PRT( "Time", clock() - clk );
+ABC_PRT( "Time", Abc_Clock() - clk );
}
}
/*
if ( RetValue == -1 && pParSec->TimeLimit )
{
- TimeLeft = (float)pParSec->TimeLimit - ((float)(clock()-clkTotal)/(float)(CLOCKS_PER_SEC));
+ TimeLeft = (float)pParSec->TimeLimit - ((float)(Abc_Clock()-clkTotal)/(float)(CLOCKS_PER_SEC));
TimeLeft = Abc_MaxInt( TimeLeft, 0.0 );
if ( TimeLeft == 0.0 )
{
@@ -265,14 +265,14 @@ ABC_PRT( "Time", clock() - clk );
// perform fraiging
if ( pParSec->fFraiging )
{
-clk = clock();
+clk = Abc_Clock();
pNew = Fra_FraigEquivence( pTemp = pNew, 100, 0 );
Aig_ManStop( pTemp );
if ( pParSec->fVerbose )
{
printf( "Fraiging: Latches = %5d. Nodes = %6d. ",
Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
-ABC_PRT( "Time", clock() - clk );
+ABC_PRT( "Time", Abc_Clock() - clk );
}
}
@@ -285,7 +285,7 @@ ABC_PRT( "Time", clock() - clk );
/*
if ( RetValue == -1 && pParSec->TimeLimit )
{
- TimeLeft = (float)pParSec->TimeLimit - ((float)(clock()-clkTotal)/(float)(CLOCKS_PER_SEC));
+ TimeLeft = (float)pParSec->TimeLimit - ((float)(Abc_Clock()-clkTotal)/(float)(CLOCKS_PER_SEC));
TimeLeft = Abc_MaxInt( TimeLeft, 0.0 );
if ( TimeLeft == 0.0 )
{
@@ -301,7 +301,7 @@ ABC_PRT( "Time", clock() - clk );
if ( pParSec->fRetimeRegs && pNew->nRegs )
{
// extern Aig_Man_t * Saig_ManRetimeMinArea( Aig_Man_t * p, int nMaxIters, int fForwardOnly, int fBackwardOnly, int fInitial, int fVerbose );
-clk = clock();
+clk = Abc_Clock();
pNew->nTruePis = Aig_ManCiNum(pNew) - Aig_ManRegNum(pNew);
pNew->nTruePos = Aig_ManCoNum(pNew) - Aig_ManRegNum(pNew);
// pNew = Rtm_ManRetime( pTemp = pNew, 1, 1000, 0 );
@@ -313,7 +313,7 @@ clk = clock();
{
printf( "Min-reg retiming: Latches = %5d. Nodes = %6d. ",
Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
-ABC_PRT( "Time", clock() - clk );
+ABC_PRT( "Time", Abc_Clock() - clk );
}
}
@@ -325,7 +325,7 @@ ABC_PRT( "Time", clock() - clk );
/*
if ( RetValue == -1 && pParSec->TimeLimit )
{
- TimeLeft = (float)pParSec->TimeLimit - ((float)(clock()-clkTotal)/(float)(CLOCKS_PER_SEC));
+ TimeLeft = (float)pParSec->TimeLimit - ((float)(Abc_Clock()-clkTotal)/(float)(CLOCKS_PER_SEC));
TimeLeft = Abc_MaxInt( TimeLeft, 0.0 );
if ( TimeLeft == 0.0 )
{
@@ -338,7 +338,7 @@ ABC_PRT( "Time", clock() - clk );
}
*/
-clk = clock();
+clk = Abc_Clock();
pPars->nFramesK = nFrames;
pPars->TimeLimit = TimeLeft;
pPars->fSilent = pParSec->fSilent;
@@ -381,7 +381,7 @@ clk = clock();
{
printf( "K-step (K=%2d,I=%3d): Latches = %5d. Nodes = %6d. ",
nFrames, pPars2->nIters, Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
-ABC_PRT( "Time", clock() - clk );
+ABC_PRT( "Time", Abc_Clock() - clk );
}
if ( RetValue != -1 )
break;
@@ -391,7 +391,7 @@ ABC_PRT( "Time", clock() - clk );
if ( pNew->nRegs )
{
// extern Aig_Man_t * Saig_ManRetimeMinArea( Aig_Man_t * p, int nMaxIters, int fForwardOnly, int fBackwardOnly, int fInitial, int fVerbose );
-clk = clock();
+clk = Abc_Clock();
pNew->nTruePis = Aig_ManCiNum(pNew) - Aig_ManRegNum(pNew);
pNew->nTruePos = Aig_ManCoNum(pNew) - Aig_ManRegNum(pNew);
// pNew = Rtm_ManRetime( pTemp = pNew, 1, 1000, 0 );
@@ -403,7 +403,7 @@ clk = clock();
{
printf( "Min-reg retiming: Latches = %5d. Nodes = %6d. ",
Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
-ABC_PRT( "Time", clock() - clk );
+ABC_PRT( "Time", Abc_Clock() - clk );
}
}
@@ -411,7 +411,7 @@ ABC_PRT( "Time", clock() - clk );
pNew = Aig_ManConstReduce( pNew, 0, -1, -1, 0, 0 );
// perform rewriting
-clk = clock();
+clk = Abc_Clock();
pNew = Aig_ManDupOrdered( pTemp = pNew );
Aig_ManStop( pTemp );
// pNew = Dar_ManRewriteDefault( pTemp = pNew );
@@ -421,19 +421,19 @@ clk = clock();
{
printf( "Rewriting: Latches = %5d. Nodes = %6d. ",
Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
-ABC_PRT( "Time", clock() - clk );
+ABC_PRT( "Time", Abc_Clock() - clk );
}
// perform sequential simulation
if ( pNew->nRegs )
{
-clk = clock();
+clk = Abc_Clock();
pSml = Fra_SmlSimulateSeq( pNew, 0, 128 * nFrames, 1 + 16/(1+Aig_ManNodeNum(pNew)/1000), 1 );
if ( pParSec->fVerbose )
{
printf( "Seq simulation : Latches = %5d. Nodes = %6d. ",
Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
-ABC_PRT( "Time", clock() - clk );
+ABC_PRT( "Time", Abc_Clock() - clk );
}
if ( pSml->fNonConstOut )
{
@@ -454,12 +454,12 @@ ABC_PRT( "Time", clock() - clk );
if ( !pParSec->fSilent )
{
printf( "Networks are NOT EQUIVALENT after simulation. " );
-ABC_PRT( "Time", clock() - clkTotal );
+ABC_PRT( "Time", Abc_Clock() - clkTotal );
}
if ( pParSec->fReportSolution && !pParSec->fRecursive )
{
printf( "SOLUTION: FAIL " );
-ABC_PRT( "Time", clock() - clkTotal );
+ABC_PRT( "Time", Abc_Clock() - clkTotal );
}
return RetValue;
}
@@ -471,7 +471,7 @@ ABC_PRT( "Time", clock() - clkTotal );
RetValue = Fra_FraigMiterStatus( pNew );
// try interplation
-clk = clock();
+clk = Abc_Clock();
Aig_ManSetRegNum( pNew, Aig_ManRegNum(pNew) );
if ( pParSec->fInterpolation && RetValue == -1 && Aig_ManRegNum(pNew) > 0 )
{
@@ -564,7 +564,7 @@ clk = clock();
printf( "Property UNDECIDED after interpolation. " );
else
assert( 0 );
-ABC_PRT( "Time", clock() - clk );
+ABC_PRT( "Time", Abc_Clock() - clk );
}
}
@@ -607,12 +607,12 @@ finish:
if ( !pParSec->fSilent )
{
printf( "Networks are equivalent. " );
-ABC_PRT( "Time", clock() - clkTotal );
+ABC_PRT( "Time", Abc_Clock() - clkTotal );
}
if ( pParSec->fReportSolution && !pParSec->fRecursive )
{
printf( "SOLUTION: PASS " );
-ABC_PRT( "Time", clock() - clkTotal );
+ABC_PRT( "Time", Abc_Clock() - clkTotal );
}
}
else if ( RetValue == 0 )
@@ -631,12 +631,12 @@ ABC_PRT( "Time", clock() - clkTotal );
if ( !pParSec->fSilent )
{
printf( "Networks are NOT EQUIVALENT. " );
-ABC_PRT( "Time", clock() - clkTotal );
+ABC_PRT( "Time", Abc_Clock() - clkTotal );
}
if ( pParSec->fReportSolution && !pParSec->fRecursive )
{
printf( "SOLUTION: FAIL " );
-ABC_PRT( "Time", clock() - clkTotal );
+ABC_PRT( "Time", Abc_Clock() - clkTotal );
}
}
else
@@ -649,12 +649,12 @@ ABC_PRT( "Time", clock() - clkTotal );
if ( !pParSec->fSilent )
{
printf( "Networks are UNDECIDED. " );
-ABC_PRT( "Time", clock() - clkTotal );
+ABC_PRT( "Time", Abc_Clock() - clkTotal );
}
if ( pParSec->fReportSolution && !pParSec->fRecursive )
{
printf( "SOLUTION: UNDECIDED " );
-ABC_PRT( "Time", clock() - clkTotal );
+ABC_PRT( "Time", Abc_Clock() - clkTotal );
}
if ( !TimeOut && !pParSec->fSilent )
{
diff --git a/src/proof/fra/fraSim.c b/src/proof/fra/fraSim.c
index bbe68717..2d2ee93f 100644
--- a/src/proof/fra/fraSim.c
+++ b/src/proof/fra/fraSim.c
@@ -664,8 +664,8 @@ void Fra_SmlSimulateOne( Fra_Sml_t * p )
{
Aig_Obj_t * pObj, * pObjLi, * pObjLo;
int f, i;
- clock_t clk;
-clk = clock();
+ abctime clk;
+clk = Abc_Clock();
for ( f = 0; f < p->nFrames; f++ )
{
// simulate the nodes
@@ -684,7 +684,7 @@ clk = clock();
Aig_ManForEachLiLoSeq( p->pAig, pObjLi, pObjLo, i )
Fra_SmlNodeTransferNext( p, pObjLi, pObjLo, f );
}
-p->timeSim += clock() - clk;
+p->timeSim += Abc_Clock() - clk;
p->nSimRounds++;
}
@@ -703,21 +703,21 @@ p->nSimRounds++;
void Fra_SmlResimulate( Fra_Man_t * p )
{
int nChanges;
- clock_t clk;
+ abctime clk;
Fra_SmlAssignDist1( p->pSml, p->pPatWords );
Fra_SmlSimulateOne( p->pSml );
// if ( p->pPars->fPatScores )
// Fra_CleanPatScores( p );
if ( p->pPars->fProve && Fra_SmlCheckOutput(p) )
return;
-clk = clock();
+clk = Abc_Clock();
nChanges = Fra_ClassesRefine( p->pCla );
nChanges += Fra_ClassesRefine1( p->pCla, 1, NULL );
if ( p->pCla->vImps )
nChanges += Fra_ImpRefineUsingCex( p, p->pCla->vImps );
if ( p->vOneHots )
nChanges += Fra_OneHotRefineUsingCex( p, p->vOneHots );
-p->timeRef += clock() - clk;
+p->timeRef += Abc_Clock() - clk;
if ( !p->pPars->nFramesK && nChanges < 1 )
printf( "Error: A counter-example did not refine classes!\n" );
// assert( nChanges >= 1 );
@@ -739,7 +739,7 @@ void Fra_SmlSimulate( Fra_Man_t * p, int fInit )
{
int fVerbose = 0;
int nChanges, nClasses;
- clock_t clk;
+ abctime clk;
assert( !fInit || Aig_ManRegNum(p->pManAig) );
// start the classes
Fra_SmlInitialize( p->pSml, fInit );
@@ -759,10 +759,10 @@ printf( "Starting classes = %5d. Lits = %6d.\n", Vec_PtrSize(p->pCla->vClasses
Fra_SmlSimulateOne( p->pSml );
if ( p->pPars->fProve && Fra_SmlCheckOutput(p) )
return;
-clk = clock();
+clk = Abc_Clock();
nChanges = Fra_ClassesRefine( p->pCla );
nChanges += Fra_ClassesRefine1( p->pCla, 1, NULL );
-p->timeRef += clock() - clk;
+p->timeRef += Abc_Clock() - clk;
if ( fVerbose )
printf( "Refined classes = %5d. Changes = %4d. Lits = %6d.\n", Vec_PtrSize(p->pCla->vClasses), nChanges, Fra_ClassesCountLits(p->pCla) );
Fra_SmlSavePattern1( p, fInit );
@@ -770,10 +770,10 @@ printf( "Refined classes = %5d. Changes = %4d. Lits = %6d.\n", Vec_PtrSize(
Fra_SmlSimulateOne( p->pSml );
if ( p->pPars->fProve && Fra_SmlCheckOutput(p) )
return;
-clk = clock();
+clk = Abc_Clock();
nChanges = Fra_ClassesRefine( p->pCla );
nChanges += Fra_ClassesRefine1( p->pCla, 1, NULL );
-p->timeRef += clock() - clk;
+p->timeRef += Abc_Clock() - clk;
if ( fVerbose )
printf( "Refined classes = %5d. Changes = %4d. Lits = %6d.\n", Vec_PtrSize(p->pCla->vClasses), nChanges, Fra_ClassesCountLits(p->pCla) );
@@ -784,10 +784,10 @@ printf( "Refined classes = %5d. Changes = %4d. Lits = %6d.\n", Vec_PtrSize(
nClasses = Vec_PtrSize(p->pCla->vClasses);
if ( p->pPars->fProve && Fra_SmlCheckOutput(p) )
return;
-clk = clock();
+clk = Abc_Clock();
nChanges = Fra_ClassesRefine( p->pCla );
nChanges += Fra_ClassesRefine1( p->pCla, 1, NULL );
-p->timeRef += clock() - clk;
+p->timeRef += Abc_Clock() - clk;
if ( fVerbose )
printf( "Refined classes = %5d. Changes = %4d. Lits = %6d.\n", Vec_PtrSize(p->pCla->vClasses), nChanges, Fra_ClassesCountLits(p->pCla) );
} while ( (double)nChanges / nClasses > p->pPars->dSimSatur );
generated by cgit v1.2.3 (git 2.25.1) at 2024-06-30 18:52:01 +0000