diff options
| -rw-r--r-- | src/base/abci/abcDar.c | 10 | ||||
| -rw-r--r-- | src/misc/extra/extraBddMisc.c | 8 | ||||
| -rw-r--r-- | src/misc/extra/extraBddTime.c | 6 |
3 files changed, 12 insertions, 12 deletions
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c index 13aeaaa0..dc090791 100644 --- a/src/base/abci/abcDar.c +++ b/src/base/abci/abcDar.c @@ -1694,7 +1694,7 @@ int Abc_NtkDarBmc( Abc_Ntk_t * pNtk, int nStart, int nFrames, int nSizeMax, int { Aig_Man_t * pMan; int status, RetValue = -1, clk = clock(); - int nTimeLimit = nTimeOut ? clock() + nTimeOut * CLOCKS_PER_SEC : 0; + int nTimeLimit = nTimeOut ? time(NULL) + nTimeOut : 0; // derive the AIG manager pMan = Abc_NtkToDar( pNtk, 0, 1 ); @@ -1722,7 +1722,7 @@ int Abc_NtkDarBmc( Abc_Ntk_t * pNtk, int nStart, int nFrames, int nSizeMax, int else if ( RetValue == -1 ) { printf( "No output asserted in %d frames. Resource limit reached ", iFrame ); - if ( nTimeLimit < clock() ) + if ( time(NULL) > nTimeLimit ) printf( "(timeout %d sec). ", nTimeLimit ); else printf( "(conf limit %d). ", nBTLimit ); @@ -1804,7 +1804,7 @@ int Abc_NtkDarBmc3( Abc_Ntk_t * pNtk, Saig_ParBmc_t * pPars ) { Aig_Man_t * pMan; int status, RetValue = -1, clk = clock(); - int nTimeOut = pPars->nTimeOut ? clock() + pPars->nTimeOut * CLOCKS_PER_SEC : 0; + int nTimeOut = pPars->nTimeOut ? time(NULL) + pPars->nTimeOut : 0; pMan = Abc_NtkToDar( pNtk, 0, 1 ); if ( pMan == NULL ) { @@ -1825,7 +1825,7 @@ int Abc_NtkDarBmc3( Abc_Ntk_t * pNtk, Saig_ParBmc_t * pPars ) if ( pPars->nFailOuts == 0 ) { printf( "No output asserted in %d frames. Resource limit reached ", pPars->iFrame ); - if ( nTimeOut < clock() ) + if ( time(NULL) > nTimeOut ) printf( "(timeout %d sec). ", pPars->nTimeOut ); else printf( "(conf limit %d). ", pPars->nConfLimit ); @@ -1833,7 +1833,7 @@ int Abc_NtkDarBmc3( Abc_Ntk_t * pNtk, Saig_ParBmc_t * pPars ) else { printf( "The total of %d outputs asserted in %d frames. Resource limit reached ", pPars->nFailOuts, pPars->iFrame ); - if ( nTimeOut < clock() ) + if ( time(NULL) > nTimeOut ) printf( "(timeout %d sec). ", pPars->nTimeOut ); else printf( "(conf limit %d). ", pPars->nConfLimit ); diff --git a/src/misc/extra/extraBddMisc.c b/src/misc/extra/extraBddMisc.c index 0bc4a8c5..3af9c81e 100644 --- a/src/misc/extra/extraBddMisc.c +++ b/src/misc/extra/extraBddMisc.c @@ -1348,9 +1348,9 @@ extraTransferPermuteRecur( if ( st_lookup( table, ( char * ) f, ( char ** ) &res ) ) return ( Cudd_NotCond( res, comple ) ); - if ( ddS->TimeStop && ddS->TimeStop < clock() ) + if ( ddS->TimeStop && time(NULL) > ddS->TimeStop ) return NULL; - if ( ddD->TimeStop && ddD->TimeStop < clock() ) + if ( ddD->TimeStop && time(NULL) > ddD->TimeStop ) return NULL; /* Recursive step. */ @@ -1909,9 +1909,9 @@ DdNode * extraBddAndPermute( DdHashTable * table, DdManager * ddF, DdNode * bF, return bRes; Counter++; - if ( ddF->TimeStop && ddF->TimeStop < clock() ) + if ( ddF->TimeStop && time(NULL) > ddF->TimeStop ) return NULL; - if ( ddG->TimeStop && ddG->TimeStop < clock() ) + if ( ddG->TimeStop && time(NULL) > ddG->TimeStop ) return NULL; // find the topmost variable in F and G using var order of F diff --git a/src/misc/extra/extraBddTime.c b/src/misc/extra/extraBddTime.c index 9cc5ce89..b861d51a 100644 --- a/src/misc/extra/extraBddTime.c +++ b/src/misc/extra/extraBddTime.c @@ -225,7 +225,7 @@ cuddBddAndRecurTime( } // if ( TimeOut && ((*pRecCalls)++ % CHECK_FACTOR) == 0 && TimeOut < clock() ) - if ( TimeOut && TimeOut < clock() ) + if ( TimeOut && time(NULL) > TimeOut ) return NULL; /* Here we can skip the use of cuddI, because the operands are known @@ -379,7 +379,7 @@ cuddBddAndAbstractRecurTime( } // if ( TimeOut && ((*pRecCalls)++ % CHECK_FACTOR) == 0 && TimeOut < clock() ) - if ( TimeOut && TimeOut < clock() ) + if ( TimeOut && time(NULL) > TimeOut ) return NULL; if (topf == top) { @@ -596,7 +596,7 @@ extraTransferPermuteRecurTime( if ( st_lookup( table, ( char * ) f, ( char ** ) &res ) ) return ( Cudd_NotCond( res, comple ) ); - if ( TimeOut && TimeOut < clock() ) + if ( TimeOut && time(NULL) > TimeOut ) return NULL; /* Recursive step. */ |