summaryrefslogtreecommitdiffstats
path: root/src/sat
diff options
context:
space:
mode:
Diffstat (limited to 'src/sat')
-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
-rw-r--r--src/sat/bsat/satInter.c20
-rw-r--r--src/sat/bsat/satInterA.c22
-rw-r--r--src/sat/bsat/satInterB.c22
-rw-r--r--src/sat/bsat/satInterP.c26
-rw-r--r--src/sat/bsat/satProof.c24
-rw-r--r--src/sat/bsat/satSolver.c24
-rw-r--r--src/sat/bsat/satSolver.h6
-rw-r--r--src/sat/bsat/satSolver2.c22
-rw-r--r--src/sat/bsat/satSolver2.h6
-rw-r--r--src/sat/cnf/cnf.h6
-rw-r--r--src/sat/cnf/cnfCore.c50
-rw-r--r--src/sat/cnf/cnfFast.c12
-rw-r--r--src/sat/msat/msatOrderH.c14
-rw-r--r--src/sat/msat/msatSolverCore.c8
-rw-r--r--src/sat/proof/pr.c26
22 files changed, 220 insertions, 220 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 );
}
diff --git a/src/sat/bsat/satInter.c b/src/sat/bsat/satInter.c
index 6bd07fb7..45908225 100644
--- a/src/sat/bsat/satInter.c
+++ b/src/sat/bsat/satInter.c
@@ -71,9 +71,9 @@ struct Int_Man_t_
int nResLits; // the number of literals of the resolvent
int nResLitsAlloc;// the number of literals of the resolvent
// runtime stats
- clock_t timeBcp; // the runtime for BCP
- clock_t timeTrace; // the runtime of trace construction
- clock_t timeTotal; // the total runtime of interpolation
+ abctime timeBcp; // the runtime for BCP
+ abctime timeTrace; // the runtime of trace construction
+ abctime timeTotal; // the total runtime of interpolation
};
// procedure to get hold of the clauses' truth table
@@ -535,17 +535,17 @@ Sto_Cls_t * Int_ManPropagate( Int_Man_t * p, int Start )
{
Sto_Cls_t * pClause;
int i;
- clock_t clk = clock();
+ abctime clk = Abc_Clock();
for ( i = Start; i < p->nTrailSize; i++ )
{
pClause = Int_ManPropagateOne( p, p->pTrail[i] );
if ( pClause )
{
-p->timeBcp += clock() - clk;
+p->timeBcp += Abc_Clock() - clk;
return pClause;
}
}
-p->timeBcp += clock() - clk;
+p->timeBcp += Abc_Clock() - clk;
return NULL;
}
@@ -591,7 +591,7 @@ int Int_ManProofTraceOne( Int_Man_t * p, Sto_Cls_t * pConflict, Sto_Cls_t * pFin
Sto_Cls_t * pReason;
int i, v, Var, PrevId;
int fPrint = 0;
- clock_t clk = clock();
+ abctime clk = Abc_Clock();
// collect resolvent literals
if ( p->fProofVerif )
@@ -743,7 +743,7 @@ int Int_ManProofTraceOne( Int_Man_t * p, Sto_Cls_t * pConflict, Sto_Cls_t * pFin
assert( p->nResLits == (int)pFinal->nLits );
}
}
-p->timeTrace += clock() - clk;
+p->timeTrace += Abc_Clock() - clk;
// return the proof pointer
if ( p->pCnf->nClausesA )
@@ -1006,7 +1006,7 @@ int Int_ManInterpolate( Int_Man_t * p, Sto_Man_t * pCnf, int fVerbose, unsigned
{
Sto_Cls_t * pClause;
int RetValue = 1;
- clock_t clkTotal = clock();
+ abctime clkTotal = Abc_Clock();
// check that the CNF makes sense
assert( pCnf->nVars > 0 && pCnf->nClauses > 0 );
@@ -1061,7 +1061,7 @@ int Int_ManInterpolate( Int_Man_t * p, Sto_Man_t * pCnf, int fVerbose, unsigned
p->pCnf->nVars, p->pCnf->nRoots, p->pCnf->nClauses-p->pCnf->nRoots, p->Counter,
1.0*(p->Counter-p->pCnf->nRoots)/(p->pCnf->nClauses-p->pCnf->nRoots),
1.0*Sto_ManMemoryReport(p->pCnf)/(1<<20) );
-p->timeTotal += clock() - clkTotal;
+p->timeTotal += Abc_Clock() - clkTotal;
}
*ppResult = Int_ManTruthRead( p, p->pCnf->pTail );
diff --git a/src/sat/bsat/satInterA.c b/src/sat/bsat/satInterA.c
index a4a06439..dabb10a3 100644
--- a/src/sat/bsat/satInterA.c
+++ b/src/sat/bsat/satInterA.c
@@ -70,9 +70,9 @@ struct Inta_Man_t_
int nResLits; // the number of literals of the resolvent
int nResLitsAlloc;// the number of literals of the resolvent
// runtime stats
- clock_t timeBcp; // the runtime for BCP
- clock_t timeTrace; // the runtime of trace construction
- clock_t timeTotal; // the total runtime of interpolation
+ abctime timeBcp; // the runtime for BCP
+ abctime timeTrace; // the runtime of trace construction
+ abctime timeTotal; // the total runtime of interpolation
};
// procedure to get hold of the clauses' truth table
@@ -491,17 +491,17 @@ Sto_Cls_t * Inta_ManPropagate( Inta_Man_t * p, int Start )
{
Sto_Cls_t * pClause;
int i;
- clock_t clk = clock();
+ abctime clk = Abc_Clock();
for ( i = Start; i < p->nTrailSize; i++ )
{
pClause = Inta_ManPropagateOne( p, p->pTrail[i] );
if ( pClause )
{
-p->timeBcp += clock() - clk;
+p->timeBcp += Abc_Clock() - clk;
return pClause;
}
}
-p->timeBcp += clock() - clk;
+p->timeBcp += Abc_Clock() - clk;
return NULL;
}
@@ -547,7 +547,7 @@ int Inta_ManProofTraceOne( Inta_Man_t * p, Sto_Cls_t * pConflict, Sto_Cls_t * pF
Sto_Cls_t * pReason;
int i, v, Var, PrevId;
int fPrint = 0;
- clock_t clk = clock();
+ abctime clk = Abc_Clock();
// collect resolvent literals
if ( p->fProofVerif )
@@ -697,7 +697,7 @@ int Inta_ManProofTraceOne( Inta_Man_t * p, Sto_Cls_t * pConflict, Sto_Cls_t * pF
assert( p->nResLits == (int)pFinal->nLits );
}
}
-p->timeTrace += clock() - clk;
+p->timeTrace += Abc_Clock() - clk;
// return the proof pointer
if ( p->pCnf->nClausesA )
@@ -954,7 +954,7 @@ void * Inta_ManInterpolate( Inta_Man_t * p, Sto_Man_t * pCnf, void * vVarsAB, in
Aig_Obj_t * pObj;
Sto_Cls_t * pClause;
int RetValue = 1;
- clock_t clkTotal = clock();
+ abctime clkTotal = Abc_Clock();
// check that the CNF makes sense
assert( pCnf->nVars > 0 && pCnf->nClauses > 0 );
@@ -1008,12 +1008,12 @@ void * Inta_ManInterpolate( Inta_Man_t * p, Sto_Man_t * pCnf, void * vVarsAB, in
if ( fVerbose )
{
-// ABC_PRT( "Interpo", clock() - clkTotal );
+// ABC_PRT( "Interpo", Abc_Clock() - clkTotal );
printf( "Vars = %d. Roots = %d. Learned = %d. Resol steps = %d. Ave = %.2f. Mem = %.2f MB\n",
p->pCnf->nVars, p->pCnf->nRoots, p->pCnf->nClauses-p->pCnf->nRoots, p->Counter,
1.0*(p->Counter-p->pCnf->nRoots)/(p->pCnf->nClauses-p->pCnf->nRoots),
1.0*Sto_ManMemoryReport(p->pCnf)/(1<<20) );
-p->timeTotal += clock() - clkTotal;
+p->timeTotal += Abc_Clock() - clkTotal;
}
pObj = *Inta_ManAigRead( p, p->pCnf->pTail );
diff --git a/src/sat/bsat/satInterB.c b/src/sat/bsat/satInterB.c
index 07edf7a8..8226fb6d 100644
--- a/src/sat/bsat/satInterB.c
+++ b/src/sat/bsat/satInterB.c
@@ -70,9 +70,9 @@ struct Intb_Man_t_
int nResLits; // the number of literals of the resolvent
int nResLitsAlloc;// the number of literals of the resolvent
// runtime stats
- clock_t timeBcp; // the runtime for BCP
- clock_t timeTrace; // the runtime of trace construction
- clock_t timeTotal; // the total runtime of interpolation
+ abctime timeBcp; // the runtime for BCP
+ abctime timeTrace; // the runtime of trace construction
+ abctime timeTotal; // the total runtime of interpolation
};
// procedure to get hold of the clauses' truth table
@@ -493,17 +493,17 @@ Sto_Cls_t * Intb_ManPropagate( Intb_Man_t * p, int Start )
{
Sto_Cls_t * pClause;
int i;
- clock_t clk = clock();
+ abctime clk = Abc_Clock();
for ( i = Start; i < p->nTrailSize; i++ )
{
pClause = Intb_ManPropagateOne( p, p->pTrail[i] );
if ( pClause )
{
-p->timeBcp += clock() - clk;
+p->timeBcp += Abc_Clock() - clk;
return pClause;
}
}
-p->timeBcp += clock() - clk;
+p->timeBcp += Abc_Clock() - clk;
return NULL;
}
@@ -570,7 +570,7 @@ int Intb_ManProofTraceOne( Intb_Man_t * p, Sto_Cls_t * pConflict, Sto_Cls_t * pF
Sto_Cls_t * pReason;
int i, v, Var, PrevId;
int fPrint = 0;
- clock_t clk = clock();
+ abctime clk = Abc_Clock();
// collect resolvent literals
if ( p->fProofVerif )
@@ -733,7 +733,7 @@ int Intb_ManProofTraceOne( Intb_Man_t * p, Sto_Cls_t * pConflict, Sto_Cls_t * pF
assert( p->nResLits == (int)pFinal->nLits );
}
}
-p->timeTrace += clock() - clk;
+p->timeTrace += Abc_Clock() - clk;
// return the proof pointer
if ( p->pCnf->nClausesA )
@@ -990,7 +990,7 @@ void * Intb_ManInterpolate( Intb_Man_t * p, Sto_Man_t * pCnf, void * vVarsAB, in
Aig_Obj_t * pObj;
Sto_Cls_t * pClause;
int RetValue = 1;
- clock_t clkTotal = clock();
+ abctime clkTotal = Abc_Clock();
// check that the CNF makes sense
assert( pCnf->nVars > 0 && pCnf->nClauses > 0 );
@@ -1044,12 +1044,12 @@ void * Intb_ManInterpolate( Intb_Man_t * p, Sto_Man_t * pCnf, void * vVarsAB, in
if ( fVerbose )
{
-// ABC_PRT( "Interpo", clock() - clkTotal );
+// ABC_PRT( "Interpo", Abc_Clock() - clkTotal );
printf( "Vars = %d. Roots = %d. Learned = %d. Resol steps = %d. Ave = %.2f. Mem = %.2f MB\n",
p->pCnf->nVars, p->pCnf->nRoots, p->pCnf->nClauses-p->pCnf->nRoots, p->Counter,
1.0*(p->Counter-p->pCnf->nRoots)/(p->pCnf->nClauses-p->pCnf->nRoots),
1.0*Sto_ManMemoryReport(p->pCnf)/(1<<20) );
-p->timeTotal += clock() - clkTotal;
+p->timeTotal += Abc_Clock() - clkTotal;
}
pObj = *Intb_ManAigRead( p, p->pCnf->pTail );
diff --git a/src/sat/bsat/satInterP.c b/src/sat/bsat/satInterP.c
index 404d5503..414879b6 100644
--- a/src/sat/bsat/satInterP.c
+++ b/src/sat/bsat/satInterP.c
@@ -69,9 +69,9 @@ struct Intp_Man_t_
int nResLits; // the number of literals of the resolvent
int nResLitsAlloc;// the number of literals of the resolvent
// runtime stats
- clock_t timeBcp; // the runtime for BCP
- clock_t timeTrace; // the runtime of trace construction
- clock_t timeTotal; // the total runtime of interpolation
+ abctime timeBcp; // the runtime for BCP
+ abctime timeTrace; // the runtime of trace construction
+ abctime timeTotal; // the total runtime of interpolation
};
// reading/writing the proof for a clause
@@ -419,17 +419,17 @@ Sto_Cls_t * Intp_ManPropagate( Intp_Man_t * p, int Start )
{
Sto_Cls_t * pClause;
int i;
- clock_t clk = clock();
+ abctime clk = Abc_Clock();
for ( i = Start; i < p->nTrailSize; i++ )
{
pClause = Intp_ManPropagateOne( p, p->pTrail[i] );
if ( pClause )
{
-p->timeBcp += clock() - clk;
+p->timeBcp += Abc_Clock() - clk;
return pClause;
}
}
-p->timeBcp += clock() - clk;
+p->timeBcp += Abc_Clock() - clk;
return NULL;
}
@@ -475,7 +475,7 @@ int Intp_ManProofTraceOne( Intp_Man_t * p, Sto_Cls_t * pConflict, Sto_Cls_t * pF
Sto_Cls_t * pReason;
int i, v, Var, PrevId;
int fPrint = 0;
- clock_t clk = clock();
+ abctime clk = Abc_Clock();
// collect resolvent literals
if ( p->fProofVerif )
@@ -639,7 +639,7 @@ int Intp_ManProofTraceOne( Intp_Man_t * p, Sto_Cls_t * pConflict, Sto_Cls_t * pF
assert( p->nResLits == (int)pFinal->nLits );
}
}
-p->timeTrace += clock() - clk;
+p->timeTrace += Abc_Clock() - clk;
// return the proof pointer
// if ( p->pCnf->nClausesA )
@@ -864,7 +864,7 @@ void Intp_ManUnsatCoreVerify( Sto_Man_t * pCnf, Vec_Int_t * vCore )
Sto_Cls_t * pClause;
Vec_Ptr_t * vClauses;
int i, iClause, RetValue;
- clock_t clk = clock();
+ abctime clk = Abc_Clock();
// collect the clauses
vClauses = Vec_PtrAlloc( 1000 );
Sto_ManForEachClauseRoot( pCnf, pClause )
@@ -896,7 +896,7 @@ void Intp_ManUnsatCoreVerify( Sto_Man_t * pCnf, Vec_Int_t * vCore )
printf( "UNSAT core verification FAILED. " );
else
printf( "UNSAT core verification succeeded. " );
- ABC_PRT( "Time", clock() - clk );
+ ABC_PRT( "Time", Abc_Clock() - clk );
}
else
{
@@ -962,7 +962,7 @@ void * Intp_ManUnsatCore( Intp_Man_t * p, Sto_Man_t * pCnf, int fVerbose )
Vec_Int_t * vVisited;
Sto_Cls_t * pClause;
int RetValue = 1;
- clock_t clkTotal = clock();
+ abctime clkTotal = Abc_Clock();
// check that the CNF makes sense
assert( pCnf->nVars > 0 && pCnf->nClauses > 0 );
@@ -1021,12 +1021,12 @@ void * Intp_ManUnsatCore( Intp_Man_t * p, Sto_Man_t * pCnf, int fVerbose )
if ( fVerbose )
{
- ABC_PRT( "Core", clock() - clkTotal );
+ ABC_PRT( "Core", Abc_Clock() - clkTotal );
printf( "Vars = %d. Roots = %d. Learned = %d. Resol steps = %d. Ave = %.2f. Mem = %.2f MB\n",
p->pCnf->nVars, p->pCnf->nRoots, p->pCnf->nClauses-p->pCnf->nRoots, p->Counter,
1.0*(p->Counter-p->pCnf->nRoots)/(p->pCnf->nClauses-p->pCnf->nRoots),
1.0*Sto_ManMemoryReport(p->pCnf)/(1<<20) );
-p->timeTotal += clock() - clkTotal;
+p->timeTotal += Abc_Clock() - clkTotal;
}
// derive the UNSAT core
diff --git a/src/sat/bsat/satProof.c b/src/sat/bsat/satProof.c
index e70a60ef..a4067160 100644
--- a/src/sat/bsat/satProof.c
+++ b/src/sat/bsat/satProof.c
@@ -146,7 +146,7 @@ Vec_Int_t * Proof_CollectUsedIter( Vec_Set_t * vProof, Vec_Int_t * vRoots, int f
{
int fVerify = 0;
Vec_Int_t * vUsed, * vStack;
- clock_t clk = clock();
+ abctime clk = Abc_Clock();
int i, Entry, iPrev = 0;
vUsed = Vec_IntAlloc( 1000 );
vStack = Vec_IntAlloc( 1000 );
@@ -154,10 +154,10 @@ Vec_Int_t * Proof_CollectUsedIter( Vec_Set_t * vProof, Vec_Int_t * vRoots, int f
if ( Entry >= 0 )
Proof_CollectUsed_iter( vProof, Entry, vUsed, vStack );
Vec_IntFree( vStack );
-// Abc_PrintTime( 1, "Iterative clause collection time", clock() - clk );
- clk = clock();
+// Abc_PrintTime( 1, "Iterative clause collection time", Abc_Clock() - clk );
+ clk = Abc_Clock();
Abc_MergeSort( Vec_IntArray(vUsed), Vec_IntSize(vUsed) );
-// Abc_PrintTime( 1, "Postprocessing with sorting time", clock() - clk );
+// Abc_PrintTime( 1, "Postprocessing with sorting time", Abc_Clock() - clk );
// verify topological order
if ( fVerify )
{
@@ -314,8 +314,8 @@ void Sat_ProofReduce2( sat_solver2 * s )
Vec_Int_t * vUsed;
satset * pNode, * pFanin, * pPivot;
int i, k, hTemp;
- clock_t clk = clock();
- static clock_t TimeTotal = 0;
+ abctime clk = Abc_Clock();
+ static abctime TimeTotal = 0;
// collect visited nodes
vUsed = Proof_CollectUsedIter( vProof, vRoots, 1 );
@@ -359,7 +359,7 @@ void Sat_ProofReduce2( sat_solver2 * s )
printf( "The proof was reduced from %6.2f MB to %6.2f MB (by %6.2f %%) ",
1.0 * Vec_SetMemory(vProof) / (1<<20), 1.0 * Vec_SetMemoryS(vProof) / (1<<20),
100.0 * (Vec_SetMemory(vProof) - Vec_SetMemoryS(vProof)) / Vec_SetMemory(vProof) );
- TimeTotal += clock() - clk;
+ TimeTotal += Abc_Clock() - clk;
Abc_PrintTime( 1, "Time", TimeTotal );
}
Vec_SetShrink( vProof, Vec_SetHandCurrentS(vProof) );
@@ -390,8 +390,8 @@ int Sat_ProofReduce( Vec_Set_t * vProof, void * pRoots, int hProofPivot )
Vec_Ptr_t * vUsed;
satset * pNode, * pFanin, * pPivot;
int i, j, k, hTemp, nSize;
- clock_t clk = clock();
- static clock_t TimeTotal = 0;
+ abctime clk = Abc_Clock();
+ static abctime TimeTotal = 0;
int RetValue;
//Sat_ProofCheck0( vProof );
@@ -448,7 +448,7 @@ int Sat_ProofReduce( Vec_Set_t * vProof, void * pRoots, int hProofPivot )
printf( "The proof was reduced from %6.2f MB to %6.2f MB (by %6.2f %%) ",
1.0 * Vec_SetMemory(vProof) / (1<<20), 1.0 * Vec_SetMemoryS(vProof) / (1<<20),
100.0 * (Vec_SetMemory(vProof) - Vec_SetMemoryS(vProof)) / Vec_SetMemory(vProof) );
- TimeTotal += clock() - clk;
+ TimeTotal += Abc_Clock() - clk;
Abc_PrintTime( 1, "Time", TimeTotal );
}
Vec_SetShrink( vProof, Vec_SetHandCurrentS(vProof) );
@@ -554,7 +554,7 @@ void Sat_ProofCheck( sat_solver2 * s )
Vec_Int_t * vUsed, * vTemp;
satset * pSet, * pSet0 = NULL, * pSet1;
int i, k, hRoot, Handle, Counter = 0;
- clock_t clk = clock();
+ abctime clk = Abc_Clock();
hRoot = s->hProofLast;
if ( hRoot == -1 )
return;
@@ -586,7 +586,7 @@ void Sat_ProofCheck( sat_solver2 * s )
printf( "Derived clause with %d lits instead of the empty clause. ", pSet0->nEnts );
else
printf( "Proof verification successful. " );
- Abc_PrintTime( 1, "Time", clock() - clk );
+ Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
// cleanup
Vec_SetFree( vResolves );
Vec_IntFree( vUsed );
diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c
index d1310c81..8d1bd455 100644
--- a/src/sat/bsat/satSolver.c
+++ b/src/sat/bsat/satSolver.c
@@ -224,16 +224,16 @@ static inline void act_var_rescale(sat_solver* s) {
s->var_inc *= 1e-100;
}
static inline void act_clause_rescale(sat_solver* s) {
-// static clock_t Total = 0;
+// static abctime Total = 0;
clause** cs = (clause**)veci_begin(&s->learnts);
- int i;//, clk = clock();
+ int i;//, clk = Abc_Clock();
for (i = 0; i < veci_size(&s->learnts); i++){
float a = clause_activity(cs[i]);
clause_setactivity(cs[i], a * (float)1e-20);
}
s->cla_inc *= (float)1e-20;
- Total += clock() - clk;
+ Total += Abc_Clock() - clk;
// printf( "Rescaling... Cla inc = %10.3f Conf = %10d ", s->cla_inc, s->stats.conflicts );
// Abc_PrintTime( 1, "Time", Total );
}
@@ -282,15 +282,15 @@ static inline void act_var_rescale(sat_solver* s) {
}
static inline void act_clause_rescale(sat_solver* s) {
- static clock_t Total = 0;
- clock_t clk = clock();
+ static abctime Total = 0;
+ abctime clk = Abc_Clock();
unsigned* activity = (unsigned *)veci_begin(&s->act_clas);
int i;
for (i = 0; i < veci_size(&s->act_clas); i++)
activity[i] >>= 14;
s->cla_inc >>= 14;
s->cla_inc = Abc_MaxInt( s->cla_inc, (1<<10) );
- Total += clock() - clk;
+ Total += Abc_Clock() - clk;
// printf( "Rescaling... Cla inc = %5d Conf = %10d ", s->cla_inc, s->stats.conflicts );
// Abc_PrintTime( 1, "Time", Total );
}
@@ -1226,8 +1226,8 @@ int sat_solver_simplify(sat_solver* s)
void sat_solver_reducedb(sat_solver* s)
{
- static clock_t TimeTotal = 0;
- clock_t clk = clock();
+ static abctime TimeTotal = 0;
+ abctime clk = Abc_Clock();
Sat_Mem_t * pMem = &s->Mem;
int nLearnedOld = veci_size(&s->act_clas);
int * act_clas = veci_begin(&s->act_clas);
@@ -1330,7 +1330,7 @@ void sat_solver_reducedb(sat_solver* s)
assert( Counter == (int)s->stats.learnts );
// report the results
- TimeTotal += clock() - clk;
+ TimeTotal += Abc_Clock() - clk;
if ( s->fVerbose )
{
Abc_Print(1, "reduceDB: Keeping %7d out of %7d clauses (%5.2f %%) ",
@@ -1576,7 +1576,7 @@ static lbool sat_solver_search(sat_solver* s, ABC_INT64_T nof_conflicts)
int next;
// Reached bound on number of conflicts:
- if ((nof_conflicts >= 0 && conflictC >= nof_conflicts) || (s->nRuntimeLimit && clock() > s->nRuntimeLimit)){
+ if ((nof_conflicts >= 0 && conflictC >= nof_conflicts) || (s->nRuntimeLimit && Abc_Clock() > s->nRuntimeLimit)){
s->progress_estimate = sat_solver_progress(s);
sat_solver_canceluntil(s,s->root_level);
veci_delete(&learnt_clause);
@@ -1786,7 +1786,7 @@ int sat_solver_solve(sat_solver* s, lit* begin, lit* end, ABC_INT64_T nConfLimit
while (status == l_Undef){
double Ratio = (s->stats.learnts == 0)? 0.0 :
s->stats.learnts_literals / (double)s->stats.learnts;
- if ( s->nRuntimeLimit && clock() > s->nRuntimeLimit )
+ if ( s->nRuntimeLimit && Abc_Clock() > s->nRuntimeLimit )
break;
if (s->verbosity >= 1)
{
@@ -1810,7 +1810,7 @@ int sat_solver_solve(sat_solver* s, lit* begin, lit* end, ABC_INT64_T nConfLimit
break;
if ( s->nInsLimit && s->stats.propagations > s->nInsLimit )
break;
- if ( s->nRuntimeLimit && clock() > s->nRuntimeLimit )
+ if ( s->nRuntimeLimit && Abc_Clock() > s->nRuntimeLimit )
break;
}
if (s->verbosity >= 1)
diff --git a/src/sat/bsat/satSolver.h b/src/sat/bsat/satSolver.h
index e5ea1ba5..50a4727c 100644
--- a/src/sat/bsat/satSolver.h
+++ b/src/sat/bsat/satSolver.h
@@ -160,7 +160,7 @@ struct sat_solver_t
ABC_INT64_T nConfLimit; // external limit on the number of conflicts
ABC_INT64_T nInsLimit; // external limit on the number of implications
- clock_t nRuntimeLimit; // external limit on runtime
+ abctime nRuntimeLimit; // external limit on runtime
veci act_vars; // variables whose activity has changed
double* factors; // the activity factors
@@ -223,9 +223,9 @@ static int sat_solver_final(sat_solver* s, int ** ppArray)
return s->conf_final.size;
}
-static clock_t sat_solver_set_runtime_limit(sat_solver* s, clock_t Limit)
+static abctime sat_solver_set_runtime_limit(sat_solver* s, abctime Limit)
{
- clock_t nRuntimeLimit = s->nRuntimeLimit;
+ abctime nRuntimeLimit = s->nRuntimeLimit;
s->nRuntimeLimit = Limit;
return nRuntimeLimit;
}
diff --git a/src/sat/bsat/satSolver2.c b/src/sat/bsat/satSolver2.c
index 12d74c0d..cde1d3b1 100644
--- a/src/sat/bsat/satSolver2.c
+++ b/src/sat/bsat/satSolver2.c
@@ -304,15 +304,15 @@ static inline void act_var_rescale(sat_solver2* s) {
s->var_inc *= 1e-100;
}
static inline void act_clause2_rescale(sat_solver2* s) {
- static clock_t Total = 0;
+ static abctime Total = 0;
float * act_clas = (float *)veci_begin(&s->act_clas);
int i;
- clock_t clk = clock();
+ abctime clk = Abc_Clock();
for (i = 0; i < veci_size(&s->act_clas); i++)
act_clas[i] *= (float)1e-20;
s->cla_inc *= (float)1e-20;
- Total += clock() - clk;
+ Total += Abc_Clock() - clk;
Abc_Print(1, "Rescaling... Cla inc = %10.3f Conf = %10d ", s->cla_inc, s->stats.conflicts );
Abc_PrintTime( 1, "Time", Total );
}
@@ -344,15 +344,15 @@ static inline void act_var_rescale(sat_solver2* s) {
s->var_inc = Abc_MaxInt( s->var_inc, (1<<4) );
}
static inline void act_clause2_rescale(sat_solver2* s) {
-// static clock_t Total = 0;
-// clock_t clk = clock();
+// static abctime Total = 0;
+// abctime clk = Abc_Clock();
int i;
unsigned * act_clas = (unsigned *)veci_begin(&s->act_clas);
for (i = 0; i < veci_size(&s->act_clas); i++)
act_clas[i] >>= 14;
s->cla_inc >>= 14;
s->cla_inc = Abc_MaxInt( s->cla_inc, (1<<10) );
-// Total += clock() - clk;
+// Total += Abc_Clock() - clk;
// Abc_Print(1, "Rescaling... Cla inc = %5d Conf = %10d ", s->cla_inc, s->stats.conflicts );
// Abc_PrintTime( 1, "Time", Total );
}
@@ -1037,7 +1037,7 @@ static lbool solver2_search(sat_solver2* s, ABC_INT64_T nof_conflicts)
// NO CONFLICT
int next;
- if ((nof_conflicts >= 0 && conflictC >= nof_conflicts) || (s->nRuntimeLimit && clock() > s->nRuntimeLimit)){
+ if ((nof_conflicts >= 0 && conflictC >= nof_conflicts) || (s->nRuntimeLimit && Abc_Clock() > s->nRuntimeLimit)){
// Reached bound on number of conflicts:
s->progress_estimate = solver2_progress(s);
solver2_canceluntil(s,s->root_level);
@@ -1390,7 +1390,7 @@ void luby2_test()
// updates clauses, watches, units, and proof
void sat_solver2_reducedb(sat_solver2* s)
{
- static clock_t TimeTotal = 0;
+ static abctime TimeTotal = 0;
Sat_Mem_t * pMem = &s->Mem;
clause * c = NULL;
int nLearnedOld = veci_size(&s->act_clas);
@@ -1398,7 +1398,7 @@ void sat_solver2_reducedb(sat_solver2* s)
int * pPerm, * pSortValues, nCutoffValue, * pClaProofs;
int i, j, k, Id, nSelected;//, LastSize = 0;
int Counter, CounterStart;
- clock_t clk = clock();
+ abctime clk = Abc_Clock();
static int Count = 0;
Count++;
assert( s->nLearntMax );
@@ -1558,7 +1558,7 @@ void sat_solver2_reducedb(sat_solver2* s)
}
// report the results
- TimeTotal += clock() - clk;
+ TimeTotal += Abc_Clock() - clk;
if ( s->fVerbose )
{
Abc_Print(1, "reduceDB: Keeping %7d out of %7d clauses (%5.2f %%) ",
@@ -1943,7 +1943,7 @@ int sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLim
s->progress_estimate*100);
fflush(stdout);
}
- if ( s->nRuntimeLimit && clock() > s->nRuntimeLimit )
+ if ( s->nRuntimeLimit && Abc_Clock() > s->nRuntimeLimit )
break;
// reduce the set of learnt clauses
if ( s->nLearntMax && veci_size(&s->act_clas) >= s->nLearntMax && s->pPrf2 == NULL )
diff --git a/src/sat/bsat/satSolver2.h b/src/sat/bsat/satSolver2.h
index 8c32cbde..d7d16d73 100644
--- a/src/sat/bsat/satSolver2.h
+++ b/src/sat/bsat/satSolver2.h
@@ -161,7 +161,7 @@ struct sat_solver2_t
stats_t stats;
ABC_INT64_T nConfLimit; // external limit on the number of conflicts
ABC_INT64_T nInsLimit; // external limit on the number of implications
- clock_t nRuntimeLimit; // external limit on runtime
+ abctime nRuntimeLimit; // external limit on runtime
};
static inline clause * clause2_read( sat_solver2 * s, cla h ) { return Sat_MemClauseHand( &s->Mem, h ); }
@@ -220,9 +220,9 @@ static inline int sat_solver2_final(sat_solver2* s, int ** ppArray)
return s->conf_final.size;
}
-static inline clock_t sat_solver2_set_runtime_limit(sat_solver2* s, clock_t Limit)
+static inline abctime sat_solver2_set_runtime_limit(sat_solver2* s, abctime Limit)
{
- clock_t temp = s->nRuntimeLimit;
+ abctime temp = s->nRuntimeLimit;
s->nRuntimeLimit = Limit;
return temp;
}
diff --git a/src/sat/cnf/cnf.h b/src/sat/cnf/cnf.h
index 61fa7f14..e5079a46 100644
--- a/src/sat/cnf/cnf.h
+++ b/src/sat/cnf/cnf.h
@@ -87,9 +87,9 @@ struct Cnf_Man_t_
int nMergeLimit; // the limit on the size of merged cut
unsigned * pTruths[4]; // temporary truth tables
Vec_Int_t * vMemory; // memory for intermediate ISOP representation
- clock_t timeCuts;
- clock_t timeMap;
- clock_t timeSave;
+ abctime timeCuts;
+ abctime timeMap;
+ abctime timeSave;
};
diff --git a/src/sat/cnf/cnfCore.c b/src/sat/cnf/cnfCore.c
index 9a845007..8cb86f87 100644
--- a/src/sat/cnf/cnfCore.c
+++ b/src/sat/cnf/cnfCore.c
@@ -81,30 +81,30 @@ Vec_Int_t * Cnf_DeriveMappingArray( Aig_Man_t * pAig )
Cnf_Man_t * p;
Vec_Ptr_t * vMapped;
Aig_MmFixed_t * pMemCuts;
- clock_t clk;
+ abctime clk;
// allocate the CNF manager
p = Cnf_ManStart();
p->pManAig = pAig;
// generate cuts for all nodes, assign cost, and find best cuts
-clk = clock();
+clk = Abc_Clock();
pMemCuts = Dar_ManComputeCuts( pAig, 10, 0, 0 );
-p->timeCuts = clock() - clk;
+p->timeCuts = Abc_Clock() - clk;
// find the mapping
-clk = clock();
+clk = Abc_Clock();
Cnf_DeriveMapping( p );
-p->timeMap = clock() - clk;
+p->timeMap = Abc_Clock() - clk;
// Aig_ManScanMapping( p, 1 );
// convert it into CNF
-clk = clock();
+clk = Abc_Clock();
Cnf_ManTransferCuts( p );
vMapped = Cnf_ManScanMapping( p, 1, 0 );
vResult = Cnf_ManWriteCnfMapping( p, vMapped );
Vec_PtrFree( vMapped );
Aig_MmFixedStop( pMemCuts, 0 );
-p->timeSave = clock() - clk;
+p->timeSave = Abc_Clock() - clk;
// reset reference counters
Aig_ManResetRefs( pAig );
@@ -131,29 +131,29 @@ Cnf_Dat_t * Cnf_DeriveWithMan( Cnf_Man_t * p, Aig_Man_t * pAig, int nOutputs )
Cnf_Dat_t * pCnf;
Vec_Ptr_t * vMapped;
Aig_MmFixed_t * pMemCuts;
- clock_t clk;
+ abctime clk;
// connect the managers
p->pManAig = pAig;
// generate cuts for all nodes, assign cost, and find best cuts
-clk = clock();
+clk = Abc_Clock();
pMemCuts = Dar_ManComputeCuts( pAig, 10, 0, 0 );
-p->timeCuts = clock() - clk;
+p->timeCuts = Abc_Clock() - clk;
// find the mapping
-clk = clock();
+clk = Abc_Clock();
Cnf_DeriveMapping( p );
-p->timeMap = clock() - clk;
+p->timeMap = Abc_Clock() - clk;
// Aig_ManScanMapping( p, 1 );
// convert it into CNF
-clk = clock();
+clk = Abc_Clock();
Cnf_ManTransferCuts( p );
vMapped = Cnf_ManScanMapping( p, 1, 1 );
pCnf = Cnf_ManWriteCnf( p, vMapped, nOutputs );
Vec_PtrFree( vMapped );
Aig_MmFixedStop( pMemCuts, 0 );
-p->timeSave = clock() - clk;
+p->timeSave = Abc_Clock() - clk;
// reset reference counters
Aig_ManResetRefs( pAig );
@@ -184,30 +184,30 @@ Cnf_Dat_t * Cnf_DeriveOtherWithMan( Cnf_Man_t * p, Aig_Man_t * pAig, int fSkipTt
Cnf_Dat_t * pCnf;
Vec_Ptr_t * vMapped;
Aig_MmFixed_t * pMemCuts;
- clock_t clk;
+ abctime clk;
// connect the managers
p->pManAig = pAig;
// generate cuts for all nodes, assign cost, and find best cuts
-clk = clock();
+clk = Abc_Clock();
pMemCuts = Dar_ManComputeCuts( pAig, 10, fSkipTtMin, 0 );
-p->timeCuts = clock() - clk;
+p->timeCuts = Abc_Clock() - clk;
// find the mapping
-clk = clock();
+clk = Abc_Clock();
Cnf_DeriveMapping( p );
-p->timeMap = clock() - clk;
+p->timeMap = Abc_Clock() - clk;
// Aig_ManScanMapping( p, 1 );
// convert it into CNF
-clk = clock();
+clk = Abc_Clock();
Cnf_ManTransferCuts( p );
vMapped = Cnf_ManScanMapping( p, 1, 1 );
pCnf = Cnf_ManWriteCnfOther( p, vMapped );
pCnf->vMapping = Cnf_ManWriteCnfMapping( p, vMapped );
Vec_PtrFree( vMapped );
Aig_MmFixedStop( pMemCuts, 0 );
-p->timeSave = clock() - clk;
+p->timeSave = Abc_Clock() - clk;
// reset reference counters
Aig_ManResetRefs( pAig );
@@ -241,17 +241,17 @@ Cnf_Dat_t * Cnf_Derive_old( Aig_Man_t * pAig )
// iteratively improve area flow
for ( i = 0; i < nIters; i++ )
{
-clk = clock();
+clk = Abc_Clock();
Cnf_ManScanMapping( p, 0 );
Cnf_ManMapForCnf( p );
-ABC_PRT( "iter ", clock() - clk );
+ABC_PRT( "iter ", Abc_Clock() - clk );
}
*/
// write the file
vMapped = Aig_ManScanMapping( p, 1 );
Vec_PtrFree( vMapped );
-clk = clock();
+clk = Abc_Clock();
Cnf_ManTransferCuts( p );
Cnf_ManPostprocess( p );
@@ -262,7 +262,7 @@ clk = clock();
Cnf_ManPostprocess( p );
Cnf_ManScanMapping( p, 0 );
*/
-ABC_PRT( "Ext ", clock() - clk );
+ABC_PRT( "Ext ", Abc_Clock() - clk );
/*
vMapped = Cnf_ManScanMapping( p, 1 );
diff --git a/src/sat/cnf/cnfFast.c b/src/sat/cnf/cnfFast.c
index 87af9520..4ab4e77f 100644
--- a/src/sat/cnf/cnfFast.c
+++ b/src/sat/cnf/cnfFast.c
@@ -666,20 +666,20 @@ Cnf_Dat_t * Cnf_DeriveFastClauses( Aig_Man_t * p, int nOutputs )
Cnf_Dat_t * Cnf_DeriveFast( Aig_Man_t * p, int nOutputs )
{
Cnf_Dat_t * pCnf = NULL;
- clock_t clk;//, clkTotal = clock();
+ abctime clk;//, clkTotal = Abc_Clock();
// printf( "\n" );
Aig_ManCleanMarkAB( p );
// create initial marking
- clk = clock();
+ clk = Abc_Clock();
Cnf_DeriveFastMark( p );
-// Abc_PrintTime( 1, "Marking", clock() - clk );
+// Abc_PrintTime( 1, "Marking", Abc_Clock() - clk );
// compute CNF size
- clk = clock();
+ clk = Abc_Clock();
pCnf = Cnf_DeriveFastClauses( p, nOutputs );
-// Abc_PrintTime( 1, "Clauses", clock() - clk );
+// Abc_PrintTime( 1, "Clauses", Abc_Clock() - clk );
// derive the resulting CNF
Aig_ManCleanMarkA( p );
-// Abc_PrintTime( 1, "TOTAL ", clock() - clkTotal );
+// Abc_PrintTime( 1, "TOTAL ", Abc_Clock() - clkTotal );
// printf( "Vars = %6d. Clauses = %7d. Literals = %8d. \n", pCnf->nVars, pCnf->nClauses, pCnf->nLiterals );
diff --git a/src/sat/msat/msatOrderH.c b/src/sat/msat/msatOrderH.c
index d0c9c997..90568ec2 100644
--- a/src/sat/msat/msatOrderH.c
+++ b/src/sat/msat/msatOrderH.c
@@ -58,7 +58,7 @@ static void Msat_HeapIncrease( Msat_Order_t * p, int n );
static void Msat_HeapPercolateUp( Msat_Order_t * p, int i );
static void Msat_HeapPercolateDown( Msat_Order_t * p, int i );
-extern clock_t timeSelect;
+extern abctime timeSelect;
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
@@ -191,7 +191,7 @@ int Msat_OrderVarSelect( Msat_Order_t * p )
// return var_Undef;
int Var;
- clock_t clk = clock();
+ abctime clk = Abc_Clock();
while ( !HEMPTY(p) )
{
@@ -199,7 +199,7 @@ int Msat_OrderVarSelect( Msat_Order_t * p )
if ( (p)->pSat->pAssigns[Var] == MSAT_VAR_UNASSIGNED )
{
//assert( Msat_OrderCheck(p) );
-timeSelect += clock() - clk;
+timeSelect += Abc_Clock() - clk;
return Var;
}
}
@@ -237,10 +237,10 @@ void Msat_OrderVarUnassigned( Msat_Order_t * p, int Var )
// if (!heap.inHeap(x))
// heap.insert(x);
- clock_t clk = clock();
+ abctime clk = Abc_Clock();
if ( !HINHEAP(p,Var) )
Msat_HeapInsert( p, Var );
-timeSelect += clock() - clk;
+timeSelect += Abc_Clock() - clk;
}
/**Function*************************************************************
@@ -259,10 +259,10 @@ void Msat_OrderUpdate( Msat_Order_t * p, int Var )
// if (heap.inHeap(x))
// heap.increase(x);
- clock_t clk = clock();
+ abctime clk = Abc_Clock();
if ( HINHEAP(p,Var) )
Msat_HeapIncrease( p, Var );
-timeSelect += clock() - clk;
+timeSelect += Abc_Clock() - clk;
}
diff --git a/src/sat/msat/msatSolverCore.c b/src/sat/msat/msatSolverCore.c
index eff1d6d7..352a4a5a 100644
--- a/src/sat/msat/msatSolverCore.c
+++ b/src/sat/msat/msatSolverCore.c
@@ -140,7 +140,7 @@ int Msat_SolverSolve( Msat_Solver_t * p, Msat_IntVec_t * vAssumps, int nBackTra
Msat_SearchParams_t Params = { 0.95, 0.999 };
double nConflictsLimit, nLearnedLimit;
Msat_Type_t Status;
- clock_t timeStart = clock();
+ abctime timeStart = Abc_Clock();
// p->pFreq = ABC_ALLOC( int, p->nVarsAlloc );
// memset( p->pFreq, 0, sizeof(int) * p->nVarsAlloc );
@@ -181,13 +181,13 @@ int Msat_SolverSolve( Msat_Solver_t * p, Msat_IntVec_t * vAssumps, int nBackTra
if ( nBackTrackLimit > 0 && (int)p->Stats.nConflicts - p->nBackTracks > nBackTrackLimit )
break;
// if the runtime limit is exceeded, quit the restart loop
- if ( nTimeLimit > 0 && clock() - timeStart >= nTimeLimit * CLOCKS_PER_SEC )
+ if ( nTimeLimit > 0 && Abc_Clock() - timeStart >= nTimeLimit * CLOCKS_PER_SEC )
break;
}
Msat_SolverCancelUntil( p, 0 );
p->nBackTracks = (int)p->Stats.nConflicts - p->nBackTracks;
/*
- ABC_PRT( "True solver runtime", clock() - timeStart );
+ ABC_PRT( "True solver runtime", Abc_Clock() - timeStart );
// print the statistics
{
int i, Counter = 0;
@@ -200,7 +200,7 @@ int Msat_SolverSolve( Msat_Solver_t * p, Msat_IntVec_t * vAssumps, int nBackTra
if ( Counter )
printf( "\n" );
printf( "Total = %d. Used = %d. Decisions = %d. Imps = %d. Conflicts = %d. ", p->nVars, Counter, (int)p->Stats.nDecisions, (int)p->Stats.nPropagations, (int)p->Stats.nConflicts );
- ABC_PRT( "Time", clock() - timeStart );
+ ABC_PRT( "Time", Abc_Clock() - timeStart );
}
*/
return Status;
diff --git a/src/sat/proof/pr.c b/src/sat/proof/pr.c
index 2727997a..7683affc 100644
--- a/src/sat/proof/pr.c
+++ b/src/sat/proof/pr.c
@@ -88,10 +88,10 @@ struct Pr_Man_t_
int nResLits; // the number of literals of the resolvent
int nResLitsAlloc;// the number of literals of the resolvent
// runtime stats
- clock_t timeBcp;
- clock_t timeTrace;
- clock_t timeRead;
- clock_t timeTotal;
+ abctime timeBcp;
+ abctime timeTrace;
+ abctime timeRead;
+ abctime timeTotal;
};
// variable assignments
@@ -578,17 +578,17 @@ Pr_Cls_t * Pr_ManPropagate( Pr_Man_t * p, int Start )
{
Pr_Cls_t * pClause;
int i;
- clock_t clk = clock();
+ abctime clk = Abc_Clock();
for ( i = Start; i < p->nTrailSize; i++ )
{
pClause = Pr_ManPropagateOne( p, p->pTrail[i] );
if ( pClause )
{
-p->timeBcp += clock() - clk;
+p->timeBcp += Abc_Clock() - clk;
return pClause;
}
}
-p->timeBcp += clock() - clk;
+p->timeBcp += Abc_Clock() - clk;
return NULL;
}
@@ -674,7 +674,7 @@ int Pr_ManProofTraceOne( Pr_Man_t * p, Pr_Cls_t * pConflict, Pr_Cls_t * pFinal )
Pr_Cls_t * pReason;
int i, v, Var, PrevId;
int fPrint = 0;
- clock_t clk = clock();
+ abctime clk = Abc_Clock();
// collect resolvent literals
if ( p->fProofVerif )
@@ -805,7 +805,7 @@ int Pr_ManProofTraceOne( Pr_Man_t * p, Pr_Cls_t * pConflict, Pr_Cls_t * pFinal )
Pr_ManPrintClause( pFinal );
}
}
-p->timeTrace += clock() - clk;
+p->timeTrace += Abc_Clock() - clk;
// return the proof pointer
if ( p->nClausesA )
@@ -1226,11 +1226,11 @@ int Pr_ManProofCount_rec( Pr_Cls_t * pClause )
int Pr_ManProofTest( char * pFileName )
{
Pr_Man_t * p;
- clock_t clk, clkTotal = clock();
+ abctime clk, clkTotal = Abc_Clock();
-clk = clock();
+clk = Abc_Clock();
p = Pr_ManProofRead( pFileName );
-p->timeRead = clock() - clk;
+p->timeRead = Abc_Clock() - clk;
if ( p == NULL )
return 0;
@@ -1249,7 +1249,7 @@ p->timeRead = clock() - clk;
1.0*(p->Counter-p->nRoots)/(p->nClauses-p->nRoots),
1.0*Pr_ManMemoryReport(p)/(1<<20) );
-p->timeTotal = clock() - clkTotal;
+p->timeTotal = Abc_Clock() - clkTotal;
Pr_ManFree( p );
return 1;
}
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-08 00:35:23 +0000