luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Fixed the overflow timeout problem in bmc/bmc2/bmc3/int/pdr/sim, etc.

This commit is contained in:
Alan Mishchenko 2011-10-31 14:59:47 -05:00
parent f08be2742e
commit 868a1b9aeb
22 changed files with 78 additions and 62 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
src/aig/gia/giaSim.c
View File

@ -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;

3
src/aig/gia/giaSim2.c
View File

@ -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;

10
src/aig/int/intCore.c
View File

@ -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;

7
src/aig/llb/llb1Reach.c
View File

@ -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 );

11
src/aig/llb/llb2Core.c
View File

@ -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 );

8
src/aig/llb/llb3Nonlin.c
View File

@ -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 );

8
src/aig/llb/llb4Nonlin.c
View File

@ -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 );

3
src/aig/saig/saigAbsPba.c
View File

@ -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();

11
src/aig/saig/saigBmc2.c
View File

@ -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;

7
src/aig/saig/saigBmc3.c
View File

@ -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 );

5
src/aig/saig/saigGlaCba.c
View File

@ -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 );

22
src/aig/saig/saigGlaPba.c
View File

@ -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();

5
src/aig/ssw/sswFilter.c
View File

@ -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;

6
src/aig/ssw/sswRarity.c
View File

@ -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 );

6
src/aig/ssw/sswRarity2.c
View File

@ -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 );

2
src/bdd/cudd/cuddAndAbs.c
View File

@ -259,7 +259,7 @@ cuddBddAndAbstractRecur(
}
}
if ( manager->TimeStop && manager->TimeStop < clock() )
if ( manager->TimeStop && manager->TimeStop < time(NULL) )
return NULL;
if (topf == top) {

2
src/bdd/cudd/cuddBddIte.c
View File

@ -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

4
src/bdd/cudd/cuddBridge.c
View File

@ -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. */

2
src/bdd/cudd/cuddCompose.c
View File

@ -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. */

2
src/bdd/cudd/cuddSymmetry.c
View File

@ -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

7
src/sat/bsat/satSolver.c
View File

@ -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");

6
src/sat/pdr/pdrCore.c
View File

@ -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 )
{