summaryrefslogtreecommitdiffstats
path: root/src/sat/bmc
diff options
context:
space:
mode:
Diffstat (limited to 'src/sat/bmc')
-rw-r--r--src/sat/bmc/bmc.h2
-rw-r--r--src/sat/bmc/bmcBmc.c22
-rw-r--r--src/sat/bmc/bmcBmc2.c22
-rw-r--r--src/sat/bmc/bmcBmc3.c64
-rw-r--r--src/sat/bmc/bmcCexDepth.c12
-rw-r--r--src/sat/bmc/bmcCexTools.c26
-rw-r--r--src/sat/bmc/bmcUnroll.c4
7 files changed, 76 insertions, 76 deletions
diff --git a/src/sat/bmc/bmc.h b/src/sat/bmc/bmc.h
index b5f07151..6e1fd62a 100644
--- a/src/sat/bmc/bmc.h
+++ b/src/sat/bmc/bmc.h
@@ -64,7 +64,7 @@ struct Saig_ParBmc_t_
int iFrame; // explored up to this frame
int nFailOuts; // the number of failed outputs
int nDropOuts; // the number of dropped outputs
- clock_t timeLastSolved; // the time when the last output was solved
+ abctime timeLastSolved; // the time when the last output was solved
int(*pFuncOnFail)(int,Abc_Cex_t*); // called for a failed output in MO mode
};
diff --git a/src/sat/bmc/bmcBmc.c b/src/sat/bmc/bmcBmc.c
index 7a7c8940..bcad9013 100644
--- a/src/sat/bmc/bmcBmc.c
+++ b/src/sat/bmc/bmcBmc.c
@@ -191,10 +191,10 @@ int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nConfLim
Aig_Man_t * pFrames, * pAigTemp;
Aig_Obj_t * pObj;
int status, Lit, i, RetValue = -1;
- clock_t clk;
+ abctime clk;
// derive the timeframes
- clk = clock();
+ clk = Abc_Clock();
if ( nCofFanLit )
{
pFrames = Gia_ManCofactorAig( pAig, nFrames, nCofFanLit );
@@ -218,13 +218,13 @@ int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nConfLim
printf( "Time-frames (%d): PI/PO = %d/%d. Node = %6d. Lev = %5d. ",
nFrames, Aig_ManCiNum(pFrames), Aig_ManCoNum(pFrames),
Aig_ManNodeNum(pFrames), Aig_ManLevelNum(pFrames) );
- ABC_PRT( "Time", clock() - clk );
+ ABC_PRT( "Time", Abc_Clock() - clk );
fflush( stdout );
}
// rewrite the timeframes
if ( fRewrite )
{
- clk = clock();
+ clk = Abc_Clock();
// pFrames = Dar_ManBalance( pAigTemp = pFrames, 0 );
pFrames = Dar_ManRwsat( pAigTemp = pFrames, 1, 0 );
Aig_ManStop( pAigTemp );
@@ -232,12 +232,12 @@ int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nConfLim
{
printf( "Time-frames after rewriting: Node = %6d. Lev = %5d. ",
Aig_ManNodeNum(pFrames), Aig_ManLevelNum(pFrames) );
- ABC_PRT( "Time", clock() - clk );
+ ABC_PRT( "Time", Abc_Clock() - clk );
fflush( stdout );
}
}
// create the SAT solver
- clk = clock();
+ clk = Abc_Clock();
pCnf = Cnf_Derive( pFrames, Aig_ManCoNum(pFrames) );
//if ( s_fInterrupt )
//return -1;
@@ -251,7 +251,7 @@ int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nConfLim
if ( fVerbose )
{
printf( "CNF: Variables = %6d. Clauses = %7d. Literals = %8d. ", pCnf->nVars, pCnf->nClauses, pCnf->nLiterals );
- ABC_PRT( "Time", clock() - clk );
+ ABC_PRT( "Time", Abc_Clock() - clk );
fflush( stdout );
}
status = sat_solver_simplify(pSat);
@@ -265,7 +265,7 @@ int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nConfLim
}
else
{
- clock_t clkPart = clock();
+ abctime clkPart = Abc_Clock();
Aig_ManForEachCo( pFrames, pObj, i )
{
//if ( s_fInterrupt )
@@ -276,15 +276,15 @@ int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nConfLim
printf( "Solving output %2d of frame %3d ... \r",
i % Saig_ManPoNum(pAig), i / Saig_ManPoNum(pAig) );
}
- clk = clock();
+ clk = Abc_Clock();
status = sat_solver_solve( pSat, &Lit, &Lit + 1, (ABC_INT64_T)nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
if ( fVerbose && (i % Saig_ManPoNum(pAig) == Saig_ManPoNum(pAig) - 1) )
{
printf( "Solved %2d outputs of frame %3d. ",
Saig_ManPoNum(pAig), i / Saig_ManPoNum(pAig) );
printf( "Conf =%8.0f. Imp =%11.0f. ", (double)pSat->stats.conflicts, (double)pSat->stats.propagations );
- ABC_PRT( "T", clock() - clkPart );
- clkPart = clock();
+ ABC_PRT( "T", Abc_Clock() - clkPart );
+ clkPart = Abc_Clock();
fflush( stdout );
}
if ( status == l_False )
diff --git a/src/sat/bmc/bmcBmc2.c b/src/sat/bmc/bmcBmc2.c
index 658010c0..47bfc008 100644
--- a/src/sat/bmc/bmcBmc2.c
+++ b/src/sat/bmc/bmcBmc2.c
@@ -202,7 +202,7 @@ Vec_Ptr_t * Abs_ManTernarySimulate( Aig_Man_t * p, int nFramesMax, int fVerbose
Vec_Ptr_t * vSimInfo;
Aig_Obj_t * pObj;
int i, f, nFramesLimit, nFrameWords;
- clock_t clk = clock();
+ abctime clk = Abc_Clock();
assert( Aig_ManRegNum(p) > 0 );
// the maximum number of frames will be determined to use at most 200Mb of RAM
nFramesLimit = 1 + (200000000 * 4)/Aig_ManObjNum(p);
@@ -231,7 +231,7 @@ Vec_Ptr_t * Abs_ManTernarySimulate( Aig_Man_t * p, int nFramesMax, int fVerbose
{
printf( "Ternary sim found non-zero output in frame %d. Used %5.2f MB. ",
f, 0.25 * (f+1) * Aig_ManObjNum(p) / (1<<20) );
- ABC_PRT( "Time", clock() - clk );
+ ABC_PRT( "Time", Abc_Clock() - clk );
}
return vSimInfo;
}
@@ -240,7 +240,7 @@ Vec_Ptr_t * Abs_ManTernarySimulate( Aig_Man_t * p, int nFramesMax, int fVerbose
{
printf( "Ternary sim proved all outputs in the first %d frames. Used %5.2f MB. ",
nFramesLimit, 0.25 * nFramesLimit * Aig_ManObjNum(p) / (1<<20) );
- ABC_PRT( "Time", clock() - clk );
+ ABC_PRT( "Time", Abc_Clock() - clk );
}
return vSimInfo;
}
@@ -765,8 +765,8 @@ int Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax
Cnf_Dat_t * pCnf;
int nOutsSolved = 0;
int Iter, RetValue = -1;
- clock_t nTimeToStop = nTimeOut ? nTimeOut * CLOCKS_PER_SEC + clock(): 0;
- clock_t clk = clock(), clk2, clkTotal = clock();
+ abctime nTimeToStop = nTimeOut ? nTimeOut * CLOCKS_PER_SEC + Abc_Clock(): 0;
+ abctime clk = Abc_Clock(), clk2, clkTotal = Abc_Clock();
int Status = -1;
/*
Vec_Ptr_t * vSimInfo;
@@ -788,7 +788,7 @@ int Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax
sat_solver_set_runtime_limit( p->pSat, nTimeToStop );
for ( Iter = 0; ; Iter++ )
{
- clk2 = clock();
+ clk2 = Abc_Clock();
// add new logic interval to frames
Saig_BmcInterval( p );
// Saig_BmcAddTargetsAsPos( p );
@@ -812,14 +812,14 @@ int Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax
printf( "%4d : F =%5d. O =%4d. And =%8d. Var =%8d. Conf =%7d. ",
Iter, p->iFrameLast, p->iOutputLast, Aig_ManNodeNum(p->pFrm), p->nSatVars, (int)p->pSat->stats.conflicts );
printf( "%4.0f MB", 4.0*(p->iFrameLast+1)*p->nObjs/(1<<20) );
- printf( "%9.2f sec", (float)(clock() - clkTotal)/(float)(CLOCKS_PER_SEC) );
+ printf( "%9.2f sec", (float)(Abc_Clock() - clkTotal)/(float)(CLOCKS_PER_SEC) );
printf( "\n" );
fflush( stdout );
}
if ( RetValue != l_False )
break;
// check the timeout
- if ( nTimeOut && clock() > nTimeToStop )
+ if ( nTimeOut && Abc_Clock() > nTimeToStop )
{
if ( !fSilent )
printf( "Reached timeout (%d seconds).\n", nTimeOut );
@@ -855,11 +855,11 @@ int Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax
{
if ( fVerbOverwrite )
{
- ABC_PRTr( "Time", clock() - clk );
+ ABC_PRTr( "Time", Abc_Clock() - clk );
}
else
{
- ABC_PRT( "Time", clock() - clk );
+ ABC_PRT( "Time", Abc_Clock() - clk );
}
if ( RetValue != l_True )
{
@@ -867,7 +867,7 @@ int Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax
printf( "Reached limit on the number of timeframes (%d).\n", p->nFramesMax );
else if ( p->nConfMaxAll && p->pSat->stats.conflicts > p->nConfMaxAll )
printf( "Reached global conflict limit (%d).\n", p->nConfMaxAll );
- else if ( nTimeOut && clock() > nTimeToStop )
+ else if ( nTimeOut && Abc_Clock() > nTimeToStop )
printf( "Reached timeout (%d seconds).\n", nTimeOut );
else
printf( "Reached local conflict limit (%d).\n", p->nConfMaxOne );
diff --git a/src/sat/bmc/bmcBmc3.c b/src/sat/bmc/bmcBmc3.c
index 87edbb5f..9d399a20 100644
--- a/src/sat/bmc/bmcBmc3.c
+++ b/src/sat/bmc/bmcBmc3.c
@@ -44,7 +44,7 @@ struct Gia_ManBmc_t_
Vec_Int_t * vId2Num; // number of each node
Vec_Ptr_t * vTerInfo; // ternary information
Vec_Ptr_t * vId2Var; // SAT vars for each object
- clock_t * pTime4Outs; // timeout per output
+ abctime * pTime4Outs; // timeout per output
// hash table
Vec_Int_t * vData; // storage for cuts
Hsh_IntMan_t * vHash; // hash table
@@ -742,7 +742,7 @@ Gia_ManBmc_t * Saig_Bmc3ManStart( Aig_Man_t * pAig, int nTimeOutOne )
// time spent on each outputs
if ( nTimeOutOne )
{
- p->pTime4Outs = ABC_ALLOC( clock_t, Saig_ManPoNum(pAig) );
+ p->pTime4Outs = ABC_ALLOC( abctime, Saig_ManPoNum(pAig) );
for ( i = 0; i < Saig_ManPoNum(pAig); i++ )
p->pTime4Outs[i] = nTimeOutOne * CLOCKS_PER_SEC / 1000 + 1;
}
@@ -1243,10 +1243,10 @@ void Saig_ParBmcSetDefaultParams( Saig_ParBmc_t * p )
SeeAlso []
***********************************************************************/
-clock_t Saig_ManBmcTimeToStop( Saig_ParBmc_t * pPars, clock_t nTimeToStopNG )
+abctime Saig_ManBmcTimeToStop( Saig_ParBmc_t * pPars, abctime nTimeToStopNG )
{
- clock_t nTimeToStopGap = pPars->nTimeOutGap ? pPars->nTimeOutGap * CLOCKS_PER_SEC + clock(): 0;
- clock_t nTimeToStop = 0;
+ abctime nTimeToStopGap = pPars->nTimeOutGap ? pPars->nTimeOutGap * CLOCKS_PER_SEC + Abc_Clock(): 0;
+ abctime nTimeToStop = 0;
if ( nTimeToStopNG && nTimeToStopGap )
nTimeToStop = Abc_MinInt( nTimeToStopNG, nTimeToStopGap );
else if ( nTimeToStopNG )
@@ -1302,14 +1302,14 @@ int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars )
int RetValue = -1, fFirst = 1, nJumpFrame = 0, fUnfinished = 0;
int nOutDigits = Abc_Base10Log( Saig_ManPoNum(pAig) );
int i, f, k, Lit, status;
- clock_t clk, clk2, clkOther = 0, clkTotal = clock();
- clock_t nTimeUnsat = 0, nTimeSat = 0, nTimeUndec = 0, clkOne = 0;
- clock_t nTimeToStopNG, nTimeToStop;
+ abctime clk, clk2, clkOther = 0, clkTotal = Abc_Clock();
+ abctime nTimeUnsat = 0, nTimeSat = 0, nTimeUndec = 0, clkOne = 0;
+ abctime nTimeToStopNG, nTimeToStop;
if ( pPars->nTimeOutOne )
pPars->nTimeOut = pPars->nTimeOutOne * Saig_ManPoNum(pAig) / 1000 + 1;
if ( pPars->nTimeOutOne && !pPars->fSolveAll )
pPars->nTimeOutOne = 0;
- nTimeToStopNG = pPars->nTimeOut ? pPars->nTimeOut * CLOCKS_PER_SEC + clock(): 0;
+ nTimeToStopNG = pPars->nTimeOut ? pPars->nTimeOut * CLOCKS_PER_SEC + Abc_Clock(): 0;
nTimeToStop = Saig_ManBmcTimeToStop( pPars, nTimeToStopNG );
// create BMC manager
p = Saig_Bmc3ManStart( pAig, pPars->nTimeOutOne );
@@ -1332,7 +1332,7 @@ int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars )
sat_solver_set_runtime_limit( p->pSat, nTimeToStop );
// perform frames
Aig_ManRandom( 1 );
- pPars->timeLastSolved = clock();
+ pPars->timeLastSolved = Abc_Clock();
for ( f = 0; f < pPars->nFramesMax; f++ )
{
// stop BMC after exploring all reachable states
@@ -1379,18 +1379,18 @@ int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars )
if ( (pPars->nStart && f < pPars->nStart) || (nJumpFrame && f < nJumpFrame) )
continue;
// solve SAT
- clk = clock();
+ clk = Abc_Clock();
Saig_ManForEachPo( pAig, pObj, i )
{
if ( i >= Saig_ManPoNum(pAig) )
break;
// check for timeout
- if ( pPars->nTimeOutGap && pPars->timeLastSolved && clock() > pPars->timeLastSolved + pPars->nTimeOutGap * CLOCKS_PER_SEC )
+ if ( pPars->nTimeOutGap && pPars->timeLastSolved && Abc_Clock() > pPars->timeLastSolved + pPars->nTimeOutGap * CLOCKS_PER_SEC )
{
printf( "Reached gap timeout (%d seconds).\n", pPars->nTimeOutGap );
goto finish;
}
- if ( nTimeToStop && clock() > nTimeToStop )
+ if ( nTimeToStop && Abc_Clock() > nTimeToStop )
{
printf( "Reached timeout (%d seconds).\n", pPars->nTimeOut );
goto finish;
@@ -1402,9 +1402,9 @@ int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars )
if ( p->pTime4Outs && p->pTime4Outs[i] == 0 )
continue;
// add constraints for this output
-clk2 = clock();
+clk2 = Abc_Clock();
Lit = Saig_ManBmcCreateCnf( p, pObj, f );
-clkOther += clock() - clk2;
+clkOther += Abc_Clock() - clk2;
if ( Lit == 0 )
continue;
if ( Lit == 1 )
@@ -1431,7 +1431,7 @@ clkOther += clock() - clk2;
goto finish;
}
// reset the timeout
- pPars->timeLastSolved = clock();
+ pPars->timeLastSolved = Abc_Clock();
nTimeToStop = Saig_ManBmcTimeToStop( pPars, nTimeToStopNG );
if ( nTimeToStop )
sat_solver_set_runtime_limit( p->pSat, nTimeToStop );
@@ -1440,17 +1440,17 @@ clkOther += clock() - clk2;
// solve this output
fUnfinished = 0;
sat_solver_compress( p->pSat );
-clk2 = clock();
+clk2 = Abc_Clock();
if ( p->pTime4Outs )
{
assert( p->pTime4Outs[i] > 0 );
- clkOne = clock();
- sat_solver_set_runtime_limit( p->pSat, p->pTime4Outs[i] + clock() );
+ clkOne = Abc_Clock();
+ sat_solver_set_runtime_limit( p->pSat, p->pTime4Outs[i] + Abc_Clock() );
}
status = sat_solver_solve( p->pSat, &Lit, &Lit + 1, (ABC_INT64_T)pPars->nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
if ( p->pTime4Outs )
{
- clock_t timeSince = clock() - clkOne;
+ abctime timeSince = Abc_Clock() - clkOne;
assert( p->pTime4Outs[i] > 0 );
p->pTime4Outs[i] = (p->pTime4Outs[i] > timeSince) ? p->pTime4Outs[i] - timeSince : 0;
if ( p->pTime4Outs[i] == 0 && status != l_True )
@@ -1458,7 +1458,7 @@ clk2 = clock();
}
if ( status == l_False )
{
-nTimeUnsat += clock() - clk2;
+nTimeUnsat += Abc_Clock() - clk2;
if ( 1 )
{
// add final unit clause
@@ -1479,7 +1479,7 @@ nTimeUnsat += clock() - clk2;
}
else if ( status == l_True )
{
-nTimeSat += clock() - clk2;
+nTimeSat += Abc_Clock() - clk2;
RetValue = 0;
fFirst = 0;
if ( !pPars->fSolveAll )
@@ -1492,10 +1492,10 @@ nTimeSat += clock() - clk2;
printf( "Conf =%7.0f. ", (double)p->pSat->stats.conflicts );
// printf( "Imp =%10.0f. ", (double)p->pSat->stats.propagations );
printf( "Uni =%7.0f. ",(double)sat_solver_count_assigned(p->pSat) );
-// ABC_PRT( "Time", clock() - clk );
+// ABC_PRT( "Time", Abc_Clock() - clk );
printf( "%4.0f MB", 4.25*(f+1)*p->nObjNums /(1<<20) );
printf( "%4.0f MB", 1.0*sat_solver_memory(p->pSat)/(1<<20) );
- printf( "%9.2f sec ", (float)(clock() - clkTotal)/(float)(CLOCKS_PER_SEC) );
+ printf( "%9.2f sec ", (float)(Abc_Clock() - clkTotal)/(float)(CLOCKS_PER_SEC) );
// printf( "\n" );
// ABC_PRMn( "Id2Var", (f+1)*p->nObjNums*4 );
// ABC_PRMn( "SAT", 42 * p->pSat->size + 16 * (int)p->pSat->stats.clauses + 4 * (int)p->pSat->stats.clauses_literals );
@@ -1521,14 +1521,14 @@ nTimeSat += clock() - clk2;
goto finish;
}
// reset the timeout
- pPars->timeLastSolved = clock();
+ pPars->timeLastSolved = Abc_Clock();
nTimeToStop = Saig_ManBmcTimeToStop( pPars, nTimeToStopNG );
if ( nTimeToStop )
sat_solver_set_runtime_limit( p->pSat, nTimeToStop );
}
else
{
-nTimeUndec += clock() - clk2;
+nTimeUndec += Abc_Clock() - clk2;
assert( status == l_Undef );
if ( pPars->nFramesJump )
{
@@ -1559,12 +1559,12 @@ nTimeUndec += clock() - clk2;
printf( "CEX =%5d. ", pPars->nFailOuts );
if ( pPars->nTimeOutOne )
printf( "T/O =%4d. ", pPars->nDropOuts );
-// ABC_PRT( "Time", clock() - clk );
+// ABC_PRT( "Time", Abc_Clock() - clk );
// printf( "%4.0f MB", 4.0*Vec_IntSize(p->vVisited) /(1<<20) );
printf( "%4.0f MB", 4.0*(f+1)*p->nObjNums /(1<<20) );
printf( "%4.0f MB", 1.0*sat_solver_memory(p->pSat)/(1<<20) );
// printf( " %6d %6d ", p->nLitUsed, p->nLitUseless );
- printf( "%9.2f sec ", 1.0*(clock() - clkTotal)/CLOCKS_PER_SEC );
+ printf( "%9.2f sec ", 1.0*(Abc_Clock() - clkTotal)/CLOCKS_PER_SEC );
// printf( "\n" );
// ABC_PRMn( "Id2Var", (f+1)*p->nObjNums*4 );
// ABC_PRMn( "SAT", 42 * p->pSat->size + 16 * (int)p->pSat->stats.clauses + 4 * (int)p->pSat->stats.clauses_literals );
@@ -1584,10 +1584,10 @@ finish:
if ( pPars->fVerbose )
{
printf( "Runtime: " );
- printf( "CNF = %.1f sec (%.1f %%) ", 1.0*clkOther/CLOCKS_PER_SEC, 100.0*clkOther/(clock() - clkTotal) );
- printf( "UNSAT = %.1f sec (%.1f %%) ", 1.0*nTimeUnsat/CLOCKS_PER_SEC, 100.0*nTimeUnsat/(clock() - clkTotal) );
- printf( "SAT = %.1f sec (%.1f %%) ", 1.0*nTimeSat/CLOCKS_PER_SEC, 100.0*nTimeSat/(clock() - clkTotal) );
- printf( "UNDEC = %.1f sec (%.1f %%)", 1.0*nTimeUndec/CLOCKS_PER_SEC, 100.0*nTimeUndec/(clock() - clkTotal) );
+ printf( "CNF = %.1f sec (%.1f %%) ", 1.0*clkOther/CLOCKS_PER_SEC, 100.0*clkOther/(Abc_Clock() - clkTotal) );
+ printf( "UNSAT = %.1f sec (%.1f %%) ", 1.0*nTimeUnsat/CLOCKS_PER_SEC, 100.0*nTimeUnsat/(Abc_Clock() - clkTotal) );
+ printf( "SAT = %.1f sec (%.1f %%) ", 1.0*nTimeSat/CLOCKS_PER_SEC, 100.0*nTimeSat/(Abc_Clock() - clkTotal) );
+ printf( "UNDEC = %.1f sec (%.1f %%)", 1.0*nTimeUndec/CLOCKS_PER_SEC, 100.0*nTimeUndec/(Abc_Clock() - clkTotal) );
printf( "\n" );
}
Saig_Bmc3ManStop( p );
diff --git a/src/sat/bmc/bmcCexDepth.c b/src/sat/bmc/bmcCexDepth.c
index b28a7ba7..7bdfd0ad 100644
--- a/src/sat/bmc/bmcCexDepth.c
+++ b/src/sat/bmc/bmcCexDepth.c
@@ -343,7 +343,7 @@ Gia_Man_t * Bmc_CexBuildNetwork2Test( Gia_Man_t * p, Abc_Cex_t * pCex, int nFram
{
Gia_Man_t * pNew, * pTemp;
Vec_Ptr_t * vCones;
- clock_t clk = clock();
+ abctime clk = Abc_Clock();
int i;
nFramesMax = Abc_MinInt( nFramesMax, pCex->iFrame );
printf( "Processing CEX in frame %d (max frames %d).\n", pCex->iFrame, nFramesMax );
@@ -357,13 +357,13 @@ Gia_Man_t * Bmc_CexBuildNetwork2Test( Gia_Man_t * p, Abc_Cex_t * pCex, int nFram
}
pNew = Gia_ManDupAppendCones( p, (Gia_Man_t **)Vec_PtrArray(vCones), Vec_PtrSize(vCones), 1 );
Gia_AigerWrite( pNew, "miter2.aig", 0, 0 );
-//Bmc_CexDumpAogStats( pNew, clock() - clk );
+//Bmc_CexDumpAogStats( pNew, Abc_Clock() - clk );
Vec_PtrForEachEntry( Gia_Man_t *, vCones, pTemp, i )
Gia_ManStop( pTemp );
Vec_PtrFree( vCones );
printf( "GIA with additional properties is written into \"miter2.aig\".\n" );
// printf( "CE-induced network is written into file \"unate.aig\".\n" );
- Abc_PrintTime( 1, "Time", clock() - clk );
+ Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
// Gia_ManStop( pNew );
return pNew;
}
@@ -383,7 +383,7 @@ Gia_Man_t * Bmc_CexBuildNetwork2Test( Gia_Man_t * p, Abc_Cex_t * pCex, int nFram
Gia_Man_t * Bmc_CexDepthTest( Gia_Man_t * p, Abc_Cex_t * pCex, int nFrames, int fVerbose )
{
Gia_Man_t * pNew;
- clock_t clk = clock();
+ abctime clk = Abc_Clock();
Abc_Cex_t * pCexImpl = NULL;
Abc_Cex_t * pCexStates = Bmc_CexInnerStates( p, pCex, &pCexImpl, fVerbose );
Abc_Cex_t * pCexCare = Bmc_CexCareBits( p, pCexStates, pCexImpl, NULL, 1, fVerbose );
@@ -398,9 +398,9 @@ Gia_Man_t * Bmc_CexDepthTest( Gia_Man_t * p, Abc_Cex_t * pCex, int nFrames, int
// if ( !Bmc_CexVerify( p, pCex, pCexMin ) )
// printf( "Counter-example min-set verification has failed.\n" );
-// Bmc_CexDumpStats( p, pCex, pCexCare, pCexEss, pCexMin, clock() - clk );
+// Bmc_CexDumpStats( p, pCex, pCexCare, pCexEss, pCexMin, Abc_Clock() - clk );
- Abc_PrintTime( 1, "Time", clock() - clk );
+ Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
pNew = Bmc_CexBuildNetwork2Test( p, pCexStates, nFrames );
// Bmc_CexPerformUnrollingTest( p, pCex );
diff --git a/src/sat/bmc/bmcCexTools.c b/src/sat/bmc/bmcCexTools.c
index bbf7d1ad..0260b537 100644
--- a/src/sat/bmc/bmcCexTools.c
+++ b/src/sat/bmc/bmcCexTools.c
@@ -75,7 +75,7 @@ int Bmc_CexBitCount( Abc_Cex_t * p, int nInputs )
SeeAlso []
***********************************************************************/
-void Bmc_CexDumpStats( Gia_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexCare, Abc_Cex_t * pCexEss, Abc_Cex_t * pCexMin, clock_t clk )
+void Bmc_CexDumpStats( Gia_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexCare, Abc_Cex_t * pCexEss, Abc_Cex_t * pCexMin, abctime clk )
{
int nInputs = Gia_ManPiNum(p);
int nBitsTotal = (pCex->iFrame + 1) * nInputs;
@@ -112,7 +112,7 @@ void Bmc_CexDumpStats( Gia_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexCare, Ab
SeeAlso []
***********************************************************************/
-void Bmc_CexDumpAogStats( Gia_Man_t * p, clock_t clk )
+void Bmc_CexDumpAogStats( Gia_Man_t * p, abctime clk )
{
FILE * pTable = fopen( "cex/aig_stats.txt", "a+" );
fprintf( pTable, "%s ", p->pName );
@@ -170,14 +170,14 @@ Gia_Man_t * Bmc_CexPerformUnrolling( Gia_Man_t * p, Abc_Cex_t * pCex )
void Bmc_CexPerformUnrollingTest( Gia_Man_t * p, Abc_Cex_t * pCex )
{
Gia_Man_t * pNew;
- clock_t clk = clock();
+ abctime clk = Abc_Clock();
pNew = Bmc_CexPerformUnrolling( p, pCex );
Gia_ManPrintStats( pNew, 0, 0, 0 );
Gia_AigerWrite( pNew, "unroll.aig", 0, 0 );
-//Bmc_CexDumpAogStats( pNew, clock() - clk );
+//Bmc_CexDumpAogStats( pNew, Abc_Clock() - clk );
Gia_ManStop( pNew );
printf( "CE-induced network is written into file \"unroll.aig\".\n" );
- Abc_PrintTime( 1, "Time", clock() - clk );
+ Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
}
@@ -282,14 +282,14 @@ Gia_Man_t * Bmc_CexBuildNetwork( Gia_Man_t * p, Abc_Cex_t * pCex )
void Bmc_CexBuildNetworkTest( Gia_Man_t * p, Abc_Cex_t * pCex )
{
Gia_Man_t * pNew;
- clock_t clk = clock();
+ abctime clk = Abc_Clock();
pNew = Bmc_CexBuildNetwork( p, pCex );
Gia_ManPrintStats( pNew, 0, 0, 0 );
Gia_AigerWrite( pNew, "unate.aig", 0, 0 );
-//Bmc_CexDumpAogStats( pNew, clock() - clk );
+//Bmc_CexDumpAogStats( pNew, Abc_Clock() - clk );
Gia_ManStop( pNew );
printf( "CE-induced network is written into file \"unate.aig\".\n" );
- Abc_PrintTime( 1, "Time", clock() - clk );
+ Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
}
@@ -756,7 +756,7 @@ Abc_Cex_t * Bmc_CexEssentialBits( Gia_Man_t * p, Abc_Cex_t * pCexState, Abc_Cex_
{
Abc_Cex_t * pNew, * pTemp, * pPrev = NULL;
int b, fEqual = 0, fPrevStatus = 0;
-// clock_t clk = clock();
+// abctime clk = Abc_Clock();
assert( pCexState->nBits == pCexCare->nBits );
// start the counter-example
pNew = Abc_CexAlloc( 0, Gia_ManCiNum(p), pCexState->iFrame + 1 );
@@ -795,7 +795,7 @@ Abc_Cex_t * Bmc_CexEssentialBits( Gia_Man_t * p, Abc_Cex_t * pCexState, Abc_Cex_
Abc_InfoSetBit( pNew->pData, b );
}
Abc_CexFreeP( &pPrev );
-// Abc_PrintTime( 1, "Time", clock() - clk );
+// Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
printf( "Essentials: " );
Bmc_CexPrint( pNew, Gia_ManPiNum(p), fVerbose );
return pNew;
@@ -815,7 +815,7 @@ Abc_Cex_t * Bmc_CexEssentialBits( Gia_Man_t * p, Abc_Cex_t * pCexState, Abc_Cex_
***********************************************************************/
void Bmc_CexTest( Gia_Man_t * p, Abc_Cex_t * pCex, int fVerbose )
{
- clock_t clk = clock();
+ abctime clk = Abc_Clock();
Abc_Cex_t * pCexImpl = NULL;
Abc_Cex_t * pCexStates = Bmc_CexInnerStates( p, pCex, &pCexImpl, fVerbose );
Abc_Cex_t * pCexCare = Bmc_CexCareBits( p, pCexStates, pCexImpl, NULL, 1, fVerbose );
@@ -830,7 +830,7 @@ void Bmc_CexTest( Gia_Man_t * p, Abc_Cex_t * pCex, int fVerbose )
if ( !Bmc_CexVerify( p, pCex, pCexMin ) )
printf( "Counter-example min-set verification has failed.\n" );
-// Bmc_CexDumpStats( p, pCex, pCexCare, pCexEss, pCexMin, clock() - clk );
+// Bmc_CexDumpStats( p, pCex, pCexCare, pCexEss, pCexMin, Abc_Clock() - clk );
Abc_CexFreeP( &pCexStates );
Abc_CexFreeP( &pCexImpl );
@@ -838,7 +838,7 @@ void Bmc_CexTest( Gia_Man_t * p, Abc_Cex_t * pCex, int fVerbose )
Abc_CexFreeP( &pCexEss );
Abc_CexFreeP( &pCexMin );
- Abc_PrintTime( 1, "Time", clock() - clk );
+ Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
// Bmc_CexBuildNetworkTest( p, pCex );
// Bmc_CexPerformUnrollingTest( p, pCex );
}
diff --git a/src/sat/bmc/bmcUnroll.c b/src/sat/bmc/bmcUnroll.c
index 83848c49..dd1abde6 100644
--- a/src/sat/bmc/bmcUnroll.c
+++ b/src/sat/bmc/bmcUnroll.c
@@ -177,7 +177,7 @@ void Unr_ManSetup( Unr_Man_t * p )
Gia_Obj_t * pObj, * pObjRi;
Unr_Obj_t * pUnrObj;
int i, k, t, iObj, nInts, * pInts;
- clock_t clk = clock();
+ abctime clk = Abc_Clock();
vRoots = Vec_IntAlloc( 100 );
vRoots2 = Vec_IntAlloc( 100 );
// create zero rank
@@ -268,7 +268,7 @@ Unr_ManProfileRanks( p->vRanks );
Vec_IntFreeP( &vMap );
printf( "Memory usage = %6.2f MB\n", 4.0 * nInts / (1<<20) );
- Abc_PrintTime( 1, "Time", clock() - clk );
+ Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
}
generated by cgit v1.2.3 (git 2.25.1) at 2024-10-28 03:09:07 +0000