summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/aig/gia/giaSim.c3
-rw-r--r--src/aig/gia/giaSim2.c3
-rw-r--r--src/aig/int/intCore.c10
-rw-r--r--src/aig/llb/llb1Reach.c7
-rw-r--r--src/aig/llb/llb2Core.c11
-rw-r--r--src/aig/llb/llb3Nonlin.c8
-rw-r--r--src/aig/llb/llb4Nonlin.c8
-rw-r--r--src/aig/saig/saigAbsPba.c3
-rw-r--r--src/aig/saig/saigBmc2.c11
-rw-r--r--src/aig/saig/saigBmc3.c7
-rw-r--r--src/aig/saig/saigGlaCba.c5
-rw-r--r--src/aig/saig/saigGlaPba.c22
-rw-r--r--src/aig/ssw/sswFilter.c5
-rw-r--r--src/aig/ssw/sswRarity.c6
-rw-r--r--src/aig/ssw/sswRarity2.c6
-rw-r--r--src/bdd/cudd/cuddAndAbs.c2
-rw-r--r--src/bdd/cudd/cuddBddIte.c2
-rw-r--r--src/bdd/cudd/cuddBridge.c4
-rw-r--r--src/bdd/cudd/cuddCompose.c2
-rw-r--r--src/bdd/cudd/cuddSymmetry.c2
-rw-r--r--src/sat/bsat/satSolver.c7
-rw-r--r--src/sat/pdr/pdrCore.c6
22 files changed, 78 insertions, 62 deletions
diff --git a/src/aig/gia/giaSim.c b/src/aig/gia/giaSim.c
index 44b917c7..4be740cd 100644
--- a/src/aig/gia/giaSim.c
+++ b/src/aig/gia/giaSim.c
@@ -611,6 +611,7 @@ int Gia_ManSimSimulate( Gia_Man_t * pAig, Gia_ParSim_t * pPars )
Gia_ManSim_t * p;
int i, clkTotal = clock();
int iOut, iPat, RetValue = 0;
+ int nTimeToStop = pPars->TimeLimit ? pPars->TimeLimit + time(NULL) : 0;
if ( pAig->pReprs && pAig->pNexts )
return Gia_ManSimSimulateEquiv( pAig, pPars );
ABC_FREE( pAig->pCexSeq );
@@ -647,7 +648,7 @@ int Gia_ManSimSimulate( Gia_Man_t * pAig, Gia_ParSim_t * pPars )
RetValue = 1;
break;
}
- if ( (clock() - clkTotal)/CLOCKS_PER_SEC >= pPars->TimeLimit )
+ if ( time(NULL) > pPars->TimeLimit )
{
i++;
break;
diff --git a/src/aig/gia/giaSim2.c b/src/aig/gia/giaSim2.c
index e1a5aa07..27945704 100644
--- a/src/aig/gia/giaSim2.c
+++ b/src/aig/gia/giaSim2.c
@@ -641,6 +641,7 @@ int Gia_ManSimSimulateEquiv( Gia_Man_t * pAig, Gia_ParSim_t * pPars )
Gia_Obj_t * pObj;
int i, clkTotal = clock();
int RetValue = 0, iOut, iPat;
+ int nTimeToStop = pPars->TimeLimit ? pPars->TimeLimit + time(NULL) : 0;
assert( pAig->pReprs && pAig->pNexts );
ABC_FREE( pAig->pCexSeq );
p = Gia_Sim2Create( pAig, pPars );
@@ -681,7 +682,7 @@ int Gia_ManSimSimulateEquiv( Gia_Man_t * pAig, Gia_ParSim_t * pPars )
}
if ( pAig->pReprs && pAig->pNexts )
Gia_Sim2InfoRefineEquivs( p );
- if ( (clock() - clkTotal)/CLOCKS_PER_SEC >= pPars->TimeLimit )
+ if ( time(NULL) > nTimeToStop )
{
i++;
break;
diff --git a/src/aig/int/intCore.c b/src/aig/int/intCore.c
index d6295931..0cd5eb36 100644
--- a/src/aig/int/intCore.c
+++ b/src/aig/int/intCore.c
@@ -81,11 +81,7 @@ int Inter_ManPerformInterpolation( Aig_Man_t * pAig, Inter_ManParams_t * pPars,
Inter_Check_t * pCheck = NULL;
Aig_Man_t * pAigTemp;
int s, i, RetValue, Status, clk, clk2, clkTotal = clock(), timeTemp;
- int nTimeNewOut = 0;
-
- // set runtime limit
- if ( pPars->nSecLimit )
- nTimeNewOut = clock() + pPars->nSecLimit * CLOCKS_PER_SEC;
+ int nTimeNewOut = pPars->nSecLimit ? time(NULL) + pPars->nSecLimit : 0;
// sanity checks
assert( Saig_ManRegNum(pAig) > 0 );
@@ -252,7 +248,7 @@ p->timeCnf += clock() - clk;
}
else if ( RetValue == -1 )
{
- if ( pPars->nSecLimit && clock() > nTimeNewOut ) // timed out
+ if ( pPars->nSecLimit && time(NULL) > nTimeNewOut ) // timed out
{
if ( pPars->fVerbose )
printf( "Reached timeout (%d seconds).\n", pPars->nSecLimit );
@@ -331,7 +327,7 @@ p->timeEqu += clock() - clk - timeTemp;
Inter_CheckStop( pCheck );
return 1;
}
- if ( pPars->nSecLimit && clock() > nTimeNewOut )
+ if ( pPars->nSecLimit && time(NULL) > nTimeNewOut )
{
printf( "Reached timeout (%d seconds).\n", pPars->nSecLimit );
p->timeTotal = clock() - clkTotal;
diff --git a/src/aig/llb/llb1Reach.c b/src/aig/llb/llb1Reach.c
index 16b62850..e427eb24 100644
--- a/src/aig/llb/llb1Reach.c
+++ b/src/aig/llb/llb1Reach.c
@@ -586,10 +586,7 @@ int Llb_ManReachability( Llb_Man_t * p, Vec_Int_t * vHints, DdManager ** pddGlo
int nThreshold = 10000;
// compute time to stop
- if ( p->pPars->TimeLimit )
- p->pPars->TimeTarget = clock() + p->pPars->TimeLimit * CLOCKS_PER_SEC;
- else
- p->pPars->TimeTarget = 0;
+ p->pPars->TimeTarget = p->pPars->TimeLimit ? time(NULL) + p->pPars->TimeLimit : 0;
// define variable limits
Llb_ManPrepareVarLimits( p );
@@ -660,7 +657,7 @@ int Llb_ManReachability( Llb_Man_t * p, Vec_Int_t * vHints, DdManager ** pddGlo
{
clk2 = clock();
// check the runtime limit
- if ( p->pPars->TimeLimit && clock() >= p->pPars->TimeTarget )
+ if ( p->pPars->TimeLimit && time(NULL) > p->pPars->TimeTarget )
{
if ( !p->pPars->fSilent )
printf( "Reached timeout during image computation (%d seconds).\n", p->pPars->TimeLimit );
diff --git a/src/aig/llb/llb2Core.c b/src/aig/llb/llb2Core.c
index 7badc1fb..4ecd1cdf 100644
--- a/src/aig/llb/llb2Core.c
+++ b/src/aig/llb/llb2Core.c
@@ -218,7 +218,7 @@ int Llb_CoreReachability_int( Llb_Img_t * p, Vec_Ptr_t * vQuant0, Vec_Ptr_t * vQ
p->pPars->TimeTarget = 0;
*/
- if ( p->pPars->TimeLimit && clock() >= p->pPars->TimeTarget )
+ if ( time(NULL) > p->pPars->TimeTarget )
{
if ( !p->pPars->fSilent )
printf( "Reached timeout (%d seconds) before image computation.\n", p->pPars->TimeLimit );
@@ -286,7 +286,7 @@ int Llb_CoreReachability_int( Llb_Img_t * p, Vec_Ptr_t * vQuant0, Vec_Ptr_t * vQ
{
clk2 = clock();
// check the runtime limit
- if ( p->pPars->TimeLimit && clock() >= p->pPars->TimeTarget )
+ if ( p->pPars->TimeLimit && time(NULL) > p->pPars->TimeTarget )
{
if ( !p->pPars->fSilent )
printf( "Reached timeout (%d seconds) during image computation.\n", p->pPars->TimeLimit );
@@ -729,10 +729,7 @@ int Llb_ManReachMinCut( Aig_Man_t * pAig, Gia_ParLlb_t * pPars )
int clk = clock();
// compute time to stop
- if ( pPars->TimeLimit )
- pPars->TimeTarget = clock() + pPars->TimeLimit * CLOCKS_PER_SEC;
- else
- pPars->TimeTarget = 0;
+ pPars->TimeTarget = pPars->TimeLimit ? time(NULL) + pPars->TimeLimit : 0;
p = Aig_ManDupFlopsOnly( pAig );
//Aig_ManShow( p, 0, NULL );
@@ -744,7 +741,7 @@ int Llb_ManReachMinCut( Aig_Man_t * pAig, Gia_ParLlb_t * pPars )
vResult = Llb_ManComputeCuts( p, pPars->nPartValue, pPars->fVerbose, pPars->fVeryVerbose );
- if ( pPars->TimeLimit && clock() >= pPars->TimeTarget )
+ if ( pPars->TimeLimit && time(NULL) > pPars->TimeTarget )
{
if ( !pPars->fSilent )
printf( "Reached timeout (%d seconds) after partitioning.\n", pPars->TimeLimit );
diff --git a/src/aig/llb/llb3Nonlin.c b/src/aig/llb/llb3Nonlin.c
index f41e0f6e..e20a1541 100644
--- a/src/aig/llb/llb3Nonlin.c
+++ b/src/aig/llb/llb3Nonlin.c
@@ -433,10 +433,8 @@ int Llb_NonlinReachability( Llb_Mnn_t * p )
assert( Aig_ManRegNum(p->pAig) > 0 );
// compute time to stop
- if ( p->pPars->TimeLimit )
- p->pPars->TimeTarget = clock() + p->pPars->TimeLimit * CLOCKS_PER_SEC;
- else
- p->pPars->TimeTarget = 0;
+ p->pPars->TimeTarget = p->pPars->TimeLimit ? time(NULL) + p->pPars->TimeLimit : 0;
+
// set the stop time parameter
p->dd->TimeStop = p->pPars->TimeTarget;
p->ddG->TimeStop = p->pPars->TimeTarget;
@@ -474,7 +472,7 @@ int Llb_NonlinReachability( Llb_Mnn_t * p )
{
// check the runtime limit
clk2 = clock();
- if ( p->pPars->TimeLimit && clock() >= p->pPars->TimeTarget )
+ if ( p->pPars->TimeLimit && time(NULL) > p->pPars->TimeTarget )
{
if ( !p->pPars->fSilent )
printf( "Reached timeout (%d seconds) during image computation.\n", p->pPars->TimeLimit );
diff --git a/src/aig/llb/llb4Nonlin.c b/src/aig/llb/llb4Nonlin.c
index 8d096b20..24cd0ac5 100644
--- a/src/aig/llb/llb4Nonlin.c
+++ b/src/aig/llb/llb4Nonlin.c
@@ -725,7 +725,7 @@ int Llb_Nonlin4Reachability( Llb_Mnx_t * p )
{
clkIter = clock();
// check the runtime limit
- if ( p->pPars->TimeLimit && clock() >= p->pPars->TimeTarget )
+ if ( p->pPars->TimeLimit && time(NULL) > p->pPars->TimeTarget )
{
if ( !p->pPars->fSilent )
printf( "Reached timeout (%d seconds) during image computation.\n", p->pPars->TimeLimit );
@@ -929,10 +929,8 @@ Llb_Mnx_t * Llb_MnxStart( Aig_Man_t * pAig, Gia_ParLlb_t * pPars )
p->pPars = pPars;
// compute time to stop
- if ( p->pPars->TimeLimit )
- p->pPars->TimeTarget = clock() + p->pPars->TimeLimit * CLOCKS_PER_SEC;
- else
- p->pPars->TimeTarget = 0;
+ p->pPars->TimeTarget = p->pPars->TimeLimit ? time(NULL) + p->pPars->TimeLimit : 0;
+
if ( pPars->fCluster )
{
// Llb_Nonlin4Cluster( p->pAig, &p->dd, &p->vOrder, &p->vRoots, pPars->nBddMax, pPars->fVerbose );
diff --git a/src/aig/saig/saigAbsPba.c b/src/aig/saig/saigAbsPba.c
index 574371ff..a42515f3 100644
--- a/src/aig/saig/saigAbsPba.c
+++ b/src/aig/saig/saigAbsPba.c
@@ -254,6 +254,7 @@ Vec_Int_t * Saig_ManPbaDerive( Aig_Man_t * pAig, int nInputs, int nStart, int nF
sat_solver * pSat;
Cnf_Dat_t * pCnf;
Aig_Obj_t * pObj;
+ int nTimeToStop = time(NULL) + TimeLimit;
int nCoreLits, * pCoreLits;
int i, iVar, RetValue, clk;
if ( fVerbose )
@@ -295,7 +296,7 @@ Abc_PrintTime( 1, "Preparing", clock() - clk );
// set runtime limit
if ( TimeLimit )
- sat_solver_set_runtime_limit( pSat, clock() + TimeLimit * CLOCKS_PER_SEC );
+ sat_solver_set_runtime_limit( pSat, nTimeToStop );
// run SAT solver
clk = clock();
diff --git a/src/aig/saig/saigBmc2.c b/src/aig/saig/saigBmc2.c
index 1fc5a11a..8d9f4ac8 100644
--- a/src/aig/saig/saigBmc2.c
+++ b/src/aig/saig/saigBmc2.c
@@ -750,6 +750,7 @@ int Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax
Saig_Bmc_t * p;
Aig_Man_t * pNew;
Cnf_Dat_t * pCnf;
+ int nTimeToStop = time(NULL) + nTimeOut;
int nOutsSolved = 0;
int Iter, RetValue = -1, clk = clock(), clk2, clkTotal = clock();
int Status = -1;
@@ -769,7 +770,7 @@ int Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax
}
// set runtime limit
if ( nTimeOut )
- sat_solver_set_runtime_limit( p->pSat, clock() + nTimeOut * CLOCKS_PER_SEC );
+ sat_solver_set_runtime_limit( p->pSat, nTimeToStop );
for ( Iter = 0; ; Iter++ )
{
clk2 = clock();
@@ -800,7 +801,7 @@ int Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax
if ( RetValue != l_False )
break;
// check the timeout
- if ( nTimeOut && ((float)nTimeOut <= (float)(clock()-clkTotal)/(float)(CLOCKS_PER_SEC)) )
+ if ( nTimeOut && time(NULL) > nTimeToStop )
{
printf( "Reached timeout (%d seconds).\n", nTimeOut );
if ( piFrames )
@@ -843,10 +844,10 @@ 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 == 0 || nTimeOut > clock() )
- printf( "Reached local conflict limit (%d).\n", p->nConfMaxOne );
+ else if ( nTimeOut && time(NULL) > nTimeToStop )
+ printf( "Reached timeout (%d seconds).\n", nTimeOut );
else
- printf( "Reached timeout (%d sec).\n", nTimeOut );
+ printf( "Reached local conflict limit (%d).\n", p->nConfMaxOne );
}
Saig_BmcManStop( p );
return Status;
diff --git a/src/aig/saig/saigBmc3.c b/src/aig/saig/saigBmc3.c
index 7248ed1a..f6ec3e0d 100644
--- a/src/aig/saig/saigBmc3.c
+++ b/src/aig/saig/saigBmc3.c
@@ -1102,6 +1102,7 @@ int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars )
int RetValue = -1, fFirst = 1, nJumpFrame = 0, fUnfinished = 0;
int nOutDigits = Aig_Base10Log( Saig_ManPoNum(pAig) - Saig_ManConstrNum(pAig) );
int i, f, Lit, status, clk, clk2, clkOther = 0, clkTotal = clock();
+ int nTimeToStop = time(NULL) + pPars->nTimeOut;
if ( pPars->fVerbose && Aig_ManConstrNum(pAig) > 0 )
printf( "Performing BMC with constraints...\n" );
p = Saig_Bmc3ManStart( pAig );
@@ -1116,7 +1117,7 @@ int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars )
}
// set runtime limit
if ( p->pPars->nTimeOut )
- sat_solver_set_runtime_limit( p->pSat, clock() + p->pPars->nTimeOut * CLOCKS_PER_SEC );
+ sat_solver_set_runtime_limit( p->pSat, nTimeToStop );
// perform frames
Aig_ManRandom( 1 );
Saig_ManBmcMarkPis( pAig, pPars->nPisAbstract );
@@ -1264,7 +1265,7 @@ clkOther += clock() - clk2;
else
{
assert( status == l_Undef );
- if ( pPars->nTimeOut && ((float)pPars->nTimeOut <= (float)(clock()-clkTotal)/(float)(CLOCKS_PER_SEC)) )
+ if ( pPars->nTimeOut && time(NULL) > nTimeToStop )
{
printf( "Reached timeout (%d seconds).\n", pPars->nTimeOut );
Saig_Bmc3ManStop( p );
@@ -1280,7 +1281,7 @@ clkOther += clock() - clk2;
Saig_Bmc3ManStop( p );
return RetValue;
}
- if ( pPars->nTimeOut && ((float)pPars->nTimeOut <= (float)(clock()-clkTotal)/(float)(CLOCKS_PER_SEC)) )
+ if ( pPars->nTimeOut && time(NULL) > nTimeToStop )
{
printf( "Reached timeout (%d seconds).\n", pPars->nTimeOut );
Saig_Bmc3ManStop( p );
diff --git a/src/aig/saig/saigGlaCba.c b/src/aig/saig/saigGlaCba.c
index 5c7c76cf..d0fd2db3 100644
--- a/src/aig/saig/saigGlaCba.c
+++ b/src/aig/saig/saigGlaCba.c
@@ -686,6 +686,7 @@ Vec_Int_t * Aig_Gla1ManTest( Aig_Man_t * pAig, Vec_Int_t * vGateClassesOld, int
Vec_Int_t * vPPiRefine;
int f, g, r, i, iSatVar, Lit, Entry, RetValue;
int nConfBef, nConfAft, clk, clkTotal = clock();
+ int nTimeToStop = time(NULL) + TimeLimit;
assert( Saig_ManPoNum(pAig) == 1 );
if ( nFramesMax == 0 )
@@ -711,7 +712,7 @@ Vec_Int_t * Aig_Gla1ManTest( Aig_Man_t * pAig, Vec_Int_t * vGateClassesOld, int
// set runtime limit
if ( TimeLimit )
- sat_solver_set_runtime_limit( p->pSat, clock() + TimeLimit * CLOCKS_PER_SEC );
+ sat_solver_set_runtime_limit( p->pSat, nTimeToStop );
// iterate over the timeframes
for ( f = 0; f < nFramesMax; f++ )
@@ -750,7 +751,7 @@ Vec_Int_t * Aig_Gla1ManTest( Aig_Man_t * pAig, Vec_Int_t * vGateClassesOld, int
printf( "== %3d ==", f );
else
printf( " " );
- if ( TimeLimit && clock() > clkTotal + TimeLimit * CLOCKS_PER_SEC )
+ if ( TimeLimit && time(NULL) > nTimeToStop )
printf( " SAT solver timed out after %d seconds.\n", TimeLimit );
else if ( RetValue != l_False )
printf( " SAT solver returned UNDECIDED after %5d conflicts.\n", nConfAft - nConfBef );
diff --git a/src/aig/saig/saigGlaPba.c b/src/aig/saig/saigGlaPba.c
index aed78f36..cedf3c9e 100644
--- a/src/aig/saig/saigGlaPba.c
+++ b/src/aig/saig/saigGlaPba.c
@@ -465,13 +465,30 @@ Vec_Int_t * Aig_Gla2ManCollect( Aig_Gla2Man_t * p, Vec_Int_t * vCore )
continue;
assert( Saig_ObjIsLo(p->pAig, pObj) || Aig_ObjIsNode(pObj) );
Vec_IntWriteEntry( vResult, Aig_ObjId(pObj), 1 );
-
+/*
+ // add flop inputs with multiple fanouts
+ if ( Saig_ObjIsLo(p->pAig, pObj) )
+ {
+ Aig_Obj_t * pObjLi = Saig_ObjLoToLi(p->pAig, pObj);
+ if ( !Saig_ObjIsPi(p->pAig, Aig_ObjFanin0(pObjLi)) )
+// if ( Aig_ObjRefs( Aig_ObjFanin0(pObjLi) ) > 1 )
+ Vec_IntWriteEntry( vResult, Aig_ObjFaninId0(pObjLi), 1 );
+ }
+ else
+ {
+ if ( !Saig_ObjIsPi(p->pAig, Aig_ObjFanin0(pObj)) )
+ Vec_IntWriteEntry( vResult, Aig_ObjFaninId0(pObj), 1 );
+ if ( !Saig_ObjIsPi(p->pAig, Aig_ObjFanin1(pObj)) )
+ Vec_IntWriteEntry( vResult, Aig_ObjFaninId1(pObj), 1 );
+ }
+*/
if ( p->vVec2Use )
{
iVecId = Vec_IntEntry( p->vObj2Vec, Aig_ObjId(pObj) );
Vec_IntWriteEntry( p->vVec2Use, iVecId * p->nFramesMax + Vec_IntEntry(p->vCla2Fra, ClaId), 1 );
}
}
+// printf( "Number of entries %d\n", Vec_IntCountPositive(vResult) );
// count the number of objects in each frame
if ( p->vVec2Use )
@@ -508,6 +525,7 @@ Vec_Int_t * Aig_Gla2ManTest( Aig_Man_t * pAig, int nStart, int nFramesMax, int n
Aig_Gla2Man_t * p;
Vec_Int_t * vCore, * vResult;
int clk, clkTotal = clock();
+ int nTimeToStop = time(NULL) + TimeLimit;
assert( Saig_ManPoNum(pAig) == 1 );
if ( fVerbose )
@@ -531,7 +549,7 @@ Vec_Int_t * Aig_Gla2ManTest( Aig_Man_t * pAig, int nStart, int nFramesMax, int n
// set runtime limit
if ( TimeLimit )
- sat_solver_set_runtime_limit( p->pSat, clock() + TimeLimit * CLOCKS_PER_SEC );
+ sat_solver_set_runtime_limit( p->pSat, nTimeToStop );
// compute UNSAT core
clk = clock();
diff --git a/src/aig/ssw/sswFilter.c b/src/aig/ssw/sswFilter.c
index 8b758915..7298c5f8 100644
--- a/src/aig/ssw/sswFilter.c
+++ b/src/aig/ssw/sswFilter.c
@@ -383,6 +383,7 @@ void Ssw_SignalFilter( Aig_Man_t * pAig, int nFramesMax, int nConfMax, int nRoun
Ssw_Pars_t Pars, * pPars = &Pars;
Ssw_Man_t * p;
int r, TimeLimitPart, clkTotal = clock();
+ int nTimeToStop = TimeLimit ? TimeLimit + time(NULL) : 0;
assert( Aig_ManRegNum(pAig) > 0 );
assert( Aig_ManConstrNum(pAig) == 0 );
// consider the case of empty AIG
@@ -428,7 +429,7 @@ void Ssw_SignalFilter( Aig_Man_t * pAig, int nFramesMax, int nConfMax, int nRoun
Ssw_ClassesPrint( p->ppClasses, 0 );
}
p->pMSat = Ssw_SatStart( 0 );
- TimeLimitPart = TimeLimit ? TimeLimit - (int)((float)(clock()-clkTotal)/(float)(CLOCKS_PER_SEC)) : 0;
+ TimeLimitPart = TimeLimit ? nTimeToStop - time(NULL) : 0;
if ( TimeLimit2 )
{
if ( TimeLimitPart )
@@ -443,7 +444,7 @@ void Ssw_SignalFilter( Aig_Man_t * pAig, int nFramesMax, int nConfMax, int nRoun
// simulate pattern forward
Ssw_ManRollForward( p, p->pPars->nFramesK );
// check timeout
- if ( TimeLimit && ((float)TimeLimit <= (float)(clock()-clkTotal)/(float)(CLOCKS_PER_SEC)) )
+ if ( TimeLimit && time(NULL) > nTimeToStop )
{
printf( "Reached timeout (%d seconds).\n", TimeLimit );
break;
diff --git a/src/aig/ssw/sswRarity.c b/src/aig/ssw/sswRarity.c
index ad37af25..7a676fee 100644
--- a/src/aig/ssw/sswRarity.c
+++ b/src/aig/ssw/sswRarity.c
@@ -895,6 +895,7 @@ int Ssw_RarSimulate( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, in
int fMiter = 1;
Ssw_RarMan_t * p;
int r, f, clk, clkTotal = clock();
+ int nTimeToStop = time(NULL) + TimeOut;
int RetValue = -1;
assert( Aig_ManRegNum(pAig) > 0 );
assert( Aig_ManConstrNum(pAig) == 0 );
@@ -933,7 +934,7 @@ int Ssw_RarSimulate( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, in
goto finish;
}
// check timeout
- if ( TimeOut && ((float)TimeOut <= (float)(clock()-clkTotal)/(float)(CLOCKS_PER_SEC)) )
+ if ( TimeOut && time(NULL) > nTimeToStop )
{
if ( fVerbose ) printf( "\n" );
printf( "Reached timeout (%d seconds).\n", TimeOut );
@@ -1002,6 +1003,7 @@ int Ssw_RarSignalFilter( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize
{
Ssw_RarMan_t * p;
int r, f, i, k, clkTotal = clock();
+ int nTimeToStop = time(NULL) + TimeOut;
int RetValue = -1;
assert( Aig_ManRegNum(pAig) > 0 );
assert( Aig_ManConstrNum(pAig) == 0 );
@@ -1071,7 +1073,7 @@ int Ssw_RarSignalFilter( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize
goto finish;
}
// check timeout
- if ( TimeOut && ((float)TimeOut <= (float)(clock()-clkTotal)/(float)(CLOCKS_PER_SEC)) )
+ if ( TimeOut && time(NULL) > nTimeToStop )
{
if ( fVerbose ) printf( "\n" );
printf( "Reached timeout (%d seconds).\n", TimeOut );
diff --git a/src/aig/ssw/sswRarity2.c b/src/aig/ssw/sswRarity2.c
index 3026cf6b..d8cb9c16 100644
--- a/src/aig/ssw/sswRarity2.c
+++ b/src/aig/ssw/sswRarity2.c
@@ -309,6 +309,7 @@ int Ssw_RarSimulate2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, i
int fMiter = 1;
Ssw_RarMan_t * p;
int r, clk, clkTotal = clock();
+ int nTimeToStop = time(NULL) + TimeOut;
int RetValue = -1;
assert( Aig_ManRegNum(pAig) > 0 );
assert( Aig_ManConstrNum(pAig) == 0 );
@@ -351,7 +352,7 @@ int Ssw_RarSimulate2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, i
printf( "." );
}
// check timeout
- if ( TimeOut && ((float)TimeOut <= (float)(clock()-clkTotal)/(float)(CLOCKS_PER_SEC)) )
+ if ( TimeOut && time(NULL) > nTimeToStop )
{
if ( fVerbose ) printf( "\n" );
printf( "Reached timeout (%d seconds).\n", TimeOut );
@@ -386,6 +387,7 @@ int Ssw_RarSignalFilter2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSiz
int fMiter = 0;
Ssw_RarMan_t * p;
int r, i, k, clkTotal = clock();
+ int nTimeToStop = time(NULL) + TimeOut;
int RetValue = -1;
assert( Aig_ManRegNum(pAig) > 0 );
assert( Aig_ManConstrNum(pAig) == 0 );
@@ -458,7 +460,7 @@ int Ssw_RarSignalFilter2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSiz
Ssw_RarTransferPatterns( p, p->vInits );
Ssw_SmlInitializeSpecial( p->pSml, p->vInits );
// check timeout
- if ( TimeOut && ((float)TimeOut <= (float)(clock()-clkTotal)/(float)(CLOCKS_PER_SEC)) )
+ if ( TimeOut && time(NULL) > nTimeToStop )
{
if ( fVerbose ) printf( "\n" );
printf( "Reached timeout (%d seconds).\n", TimeOut );
diff --git a/src/bdd/cudd/cuddAndAbs.c b/src/bdd/cudd/cuddAndAbs.c
index 2f38490d..b42f376d 100644
--- a/src/bdd/cudd/cuddAndAbs.c
+++ b/src/bdd/cudd/cuddAndAbs.c
@@ -259,7 +259,7 @@ cuddBddAndAbstractRecur(
}
}
- if ( manager->TimeStop && manager->TimeStop < clock() )
+ if ( manager->TimeStop && manager->TimeStop < time(NULL) )
return NULL;
if (topf == top) {
diff --git a/src/bdd/cudd/cuddBddIte.c b/src/bdd/cudd/cuddBddIte.c
index 4e75aab2..d1afdbee 100644
--- a/src/bdd/cudd/cuddBddIte.c
+++ b/src/bdd/cudd/cuddBddIte.c
@@ -926,7 +926,7 @@ cuddBddAndRecur(
if (r != NULL) return(r);
}
- if ( manager->TimeStop && manager->TimeStop < clock() )
+ if ( manager->TimeStop && manager->TimeStop < time(NULL) )
return NULL;
/* Here we can skip the use of cuddI, because the operands are known
diff --git a/src/bdd/cudd/cuddBridge.c b/src/bdd/cudd/cuddBridge.c
index 97a6f393..c051666d 100644
--- a/src/bdd/cudd/cuddBridge.c
+++ b/src/bdd/cudd/cuddBridge.c
@@ -976,9 +976,9 @@ cuddBddTransferRecur(
if (st_lookup(table, (const char *)f, (char **)&res))
return(Cudd_NotCond(res,comple));
- if ( ddS->TimeStop && ddS->TimeStop < clock() )
+ if ( ddS->TimeStop && ddS->TimeStop < time(NULL) )
return NULL;
- if ( ddD->TimeStop && ddD->TimeStop < clock() )
+ if ( ddD->TimeStop && ddD->TimeStop < time(NULL) )
return NULL;
/* Recursive step. */
diff --git a/src/bdd/cudd/cuddCompose.c b/src/bdd/cudd/cuddCompose.c
index 8dd8f8c5..7c99ac62 100644
--- a/src/bdd/cudd/cuddCompose.c
+++ b/src/bdd/cudd/cuddCompose.c
@@ -1251,7 +1251,7 @@ cuddBddVarMapRecur(
return(Cudd_NotCond(res,F != f));
}
- if ( manager->TimeStop && manager->TimeStop < clock() )
+ if ( manager->TimeStop && manager->TimeStop < time(NULL) )
return NULL;
/* Split and recur on children of this node. */
diff --git a/src/bdd/cudd/cuddSymmetry.c b/src/bdd/cudd/cuddSymmetry.c
index a7ef7845..3386e798 100644
--- a/src/bdd/cudd/cuddSymmetry.c
+++ b/src/bdd/cudd/cuddSymmetry.c
@@ -367,7 +367,7 @@ cuddSymmSifting(
if (ddTotalNumberSwapping >= table->siftMaxSwap)
break;
// enable timeout during variable reodering - alanmi 2/13/11
- if ( table->TimeStop && table->TimeStop < clock() )
+ if ( table->TimeStop && table->TimeStop < time(NULL) )
break;
x = table->perm[var[i]];
#ifdef DD_STATS
diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c
index a3da3e30..ac2202dc 100644
--- a/src/sat/bsat/satSolver.c
+++ b/src/sat/bsat/satSolver.c
@@ -1485,7 +1485,7 @@ int sat_solver_solve(sat_solver* s, lit* begin, lit* end, ABC_INT64_T nConfLimit
// int nConfs = 0;
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 && time(NULL) > s->nRuntimeLimit )
break;
if (s->verbosity >= 1)
@@ -1510,7 +1510,7 @@ int sat_solver_solve(sat_solver* s, lit* begin, lit* end, ABC_INT64_T nConfLimit
// nof_conflicts = nof_conflicts * 3 / 2; //*= 1.5;
nof_learnts = nof_learnts * 11 / 10; //*= 1.1;
-
+//printf( "%d ", s->stats.conflicts );
// quit the loop if reached an external limit
if ( s->nConfLimit && s->stats.conflicts > s->nConfLimit )
{
@@ -1523,9 +1523,10 @@ int sat_solver_solve(sat_solver* s, lit* begin, lit* end, ABC_INT64_T nConfLimit
// printf( "Reached the limit on the number of implications (%d).\n", s->nInsLimit );
break;
}
- if ( s->nRuntimeLimit && clock() > s->nRuntimeLimit )
+ if ( s->nRuntimeLimit && time(NULL) > s->nRuntimeLimit )
break;
}
+//printf( "\n" );
if (s->verbosity >= 1)
printf("==============================================================================\n");
diff --git a/src/sat/pdr/pdrCore.c b/src/sat/pdr/pdrCore.c
index 04caba1e..e3c3781f 100644
--- a/src/sat/pdr/pdrCore.c
+++ b/src/sat/pdr/pdrCore.c
@@ -514,7 +514,7 @@ int Pdr_ManBlockCube( Pdr_Man_t * p, Pdr_Set_t * pCube )
}
// check the timeout
- if ( p->timeToStop && clock() >= p->timeToStop )
+ if ( p->timeToStop && time(NULL) > p->timeToStop )
return -1;
}
return 1;
@@ -538,7 +538,7 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
int k, RetValue = -1;
int clkTotal = clock();
int clkStart = clock();
- p->timeToStop = (p->pPars->nTimeOut == 0) ? 0 : clock() + (CLOCKS_PER_SEC * p->pPars->nTimeOut);
+ p->timeToStop = p->pPars->nTimeOut ? time(NULL) + p->pPars->nTimeOut : 0;
assert( Vec_PtrSize(p->vSolvers) == 0 );
// create the first timeframe
Pdr_ManCreateSolver( p, (k = 0) );
@@ -619,7 +619,7 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
}
// check the timeout
- if ( p->timeToStop && clock() >= p->timeToStop )
+ if ( p->timeToStop && time(NULL) > p->timeToStop )
{
if ( fPrintClauses )
{
generated by cgit v1.2.3 (git 2.25.1) at 2024-11-04 21:39:08 +0000