diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2011-04-15 09:29:13 -0700 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2011-04-15 09:29:13 -0700 |
commit | 813245b29af60137f5bb94dfa2831d2454c8a9b5 (patch) | |
tree | 4f833c5cc9e6dbe7d3080b90fa79a43e77ef7514 /src/aig/int | |
parent | 3dfdbe1402ffebf902e9700ac85ed5bffd16f7d2 (diff) | |
download | abc-813245b29af60137f5bb94dfa2831d2454c8a9b5.tar.gz abc-813245b29af60137f5bb94dfa2831d2454c8a9b5.tar.bz2 abc-813245b29af60137f5bb94dfa2831d2454c8a9b5.zip |
Improving timeout in the interpolation package.
Diffstat (limited to 'src/aig/int')
-rw-r--r-- | src/aig/int/intCheck.c | 6 | ||||
-rw-r--r-- | src/aig/int/intCore.c | 36 | ||||
-rw-r--r-- | src/aig/int/intInt.h | 4 | ||||
-rw-r--r-- | src/aig/int/intM114.c | 6 |
4 files changed, 38 insertions, 14 deletions
diff --git a/src/aig/int/intCheck.c b/src/aig/int/intCheck.c index 54bb7ad9..6b36fe30 100644 --- a/src/aig/int/intCheck.c +++ b/src/aig/int/intCheck.c @@ -217,7 +217,7 @@ void Inter_CheckAddEqual( Inter_Check_t * p, int iVarA, int iVarB ) SeeAlso [] ***********************************************************************/ -int Inter_CheckPerform( Inter_Check_t * p, Cnf_Dat_t * pCnfInt ) +int Inter_CheckPerform( Inter_Check_t * p, Cnf_Dat_t * pCnfInt, int nTimeNewOut ) { Aig_Obj_t * pObj, * pObj2; int i, f, VarA, VarB, RetValue, Entry, status; @@ -225,6 +225,10 @@ int Inter_CheckPerform( Inter_Check_t * p, Cnf_Dat_t * pCnfInt ) assert( Aig_ManPoNum(p->pCnf->pMan) == p->nFramesK * nRegs ); assert( Aig_ManPoNum(pCnfInt->pMan) == 1 ); + // set runtime limit + if ( nTimeNewOut ) + sat_solver_set_runtime_limit( p->pSat, nTimeNewOut ); + // add clauses to the SAT solver Cnf_DataLift( pCnfInt, p->nVars ); for ( f = 0; f <= p->nFramesK; f++ ) diff --git a/src/aig/int/intCore.c b/src/aig/int/intCore.c index fdc2241e..ceb0025c 100644 --- a/src/aig/int/intCore.c +++ b/src/aig/int/intCore.c @@ -80,7 +80,13 @@ int Inter_ManPerformInterpolation( Aig_Man_t * pAig, Inter_ManParams_t * pPars, Inter_Man_t * p; Inter_Check_t * pCheck = NULL; Aig_Man_t * pAigTemp; - int s, i, RetValue, Status, clk, clk2, clkTotal = clock(); + 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; + // sanity checks assert( Saig_ManRegNum(pAig) > 0 ); assert( Saig_ManPiNum(pAig) > 0 ); @@ -171,7 +177,7 @@ p->timeCnf += clock() - clk; clk = clock(); pCnfInter2 = Cnf_Derive( p->pInter, 1 ); p->timeCnf += clock() - clk; - RetValue = Inter_CheckPerform( pCheck, pCnfInter2 ); + RetValue = Inter_CheckPerform( pCheck, pCnfInter2, nTimeNewOut ); // assert( RetValue == 0 ); Cnf_DataFree( pCnfInter2 ); } @@ -200,7 +206,7 @@ p->timeCnf += clock() - clk; } else #endif - RetValue = Inter_ManPerformOneStep( p, pPars->fUseBias, pPars->fUseBackward ); + RetValue = Inter_ManPerformOneStep( p, pPars->fUseBias, pPars->fUseBackward, nTimeNewOut ); if ( pPars->fVerbose ) { @@ -228,11 +234,19 @@ p->timeCnf += clock() - clk; Inter_ManClean( p ); break; } - else if ( RetValue == -1 ) // timed out + else if ( RetValue == -1 ) { - if ( pPars->fVerbose ) - printf( "Reached limit (%d) on the number of conflicts.\n", p->nConfLimit ); - assert( p->nConfCur >= p->nConfLimit ); + if ( pPars->nSecLimit && clock() > nTimeNewOut ) // timed out + { + if ( pPars->fVerbose ) + printf( "Reached timeout (%d seconds).\n", pPars->nSecLimit ); + } + else + { + assert( p->nConfCur >= p->nConfLimit ); + if ( pPars->fVerbose ) + printf( "Reached limit (%d) on the number of conflicts.\n", p->nConfLimit ); + } p->timeTotal = clock() - clkTotal; Inter_ManStop( p ); Inter_CheckStop( pCheck ); @@ -275,7 +289,9 @@ clk = clock(); clk2 = clock(); pCnfInter2 = Cnf_Derive( p->pInterNew, 1 ); p->timeCnf += clock() - clk2; - Status = Inter_CheckPerform( pCheck, pCnfInter2 ); +timeTemp = clock() - clk2; + + Status = Inter_CheckPerform( pCheck, pCnfInter2, nTimeNewOut ); Cnf_DataFree( pCnfInter2 ); } } @@ -289,7 +305,7 @@ p->timeCnf += clock() - clk2; else Status = 0; } -p->timeEqu += clock() - clk; +p->timeEqu += clock() - clk - timeTemp; if ( Status ) // contained { if ( pPars->fVerbose ) @@ -299,7 +315,7 @@ p->timeEqu += clock() - clk; Inter_CheckStop( pCheck ); return 1; } - if ( pPars->nSecLimit && ((float)pPars->nSecLimit <= (float)(clock()-clkTotal)/(float)(CLOCKS_PER_SEC)) ) + if ( pPars->nSecLimit && clock() > nTimeNewOut ) { printf( "Reached timeout (%d seconds).\n", pPars->nSecLimit ); p->timeTotal = clock() - clkTotal; diff --git a/src/aig/int/intInt.h b/src/aig/int/intInt.h index d5e8ed00..3eab7883 100644 --- a/src/aig/int/intInt.h +++ b/src/aig/int/intInt.h @@ -93,7 +93,7 @@ typedef struct Inter_Check_t_ Inter_Check_t; /*=== intCheck.c ============================================================*/ extern Inter_Check_t * Inter_CheckStart( Aig_Man_t * pTrans, int nFramesK ); extern void Inter_CheckStop( Inter_Check_t * p ); -extern int Inter_CheckPerform( Inter_Check_t * p, Cnf_Dat_t * pCnf ); +extern int Inter_CheckPerform( Inter_Check_t * p, Cnf_Dat_t * pCnf, int nTimeNewOut ); /*=== intContain.c ============================================================*/ extern int Inter_ManCheckContainment( Aig_Man_t * pNew, Aig_Man_t * pOld ); @@ -117,7 +117,7 @@ extern void Inter_ManClean( Inter_Man_t * p ); extern void Inter_ManStop( Inter_Man_t * p ); /*=== intM114.c ============================================================*/ -extern int Inter_ManPerformOneStep( Inter_Man_t * p, int fUseBias, int fUseBackward ); +extern int Inter_ManPerformOneStep( Inter_Man_t * p, int fUseBias, int fUseBackward, int nTimeNewOut ); /*=== intM114p.c ============================================================*/ #ifdef ABC_USE_LIBRARIES diff --git a/src/aig/int/intM114.c b/src/aig/int/intM114.c index c1718eae..139c9bbd 100644 --- a/src/aig/int/intM114.c +++ b/src/aig/int/intM114.c @@ -200,7 +200,7 @@ sat_solver * Inter_ManDeriveSatSolver( SeeAlso [] ***********************************************************************/ -int Inter_ManPerformOneStep( Inter_Man_t * p, int fUseBias, int fUseBackward ) +int Inter_ManPerformOneStep( Inter_Man_t * p, int fUseBias, int fUseBackward, int nTimeNewOut ) { sat_solver * pSat; void * pSatCnf = NULL; @@ -219,6 +219,10 @@ int Inter_ManPerformOneStep( Inter_Man_t * p, int fUseBias, int fUseBackward ) return 1; } + // set runtime limit + if ( nTimeNewOut ) + sat_solver_set_runtime_limit( pSat, nTimeNewOut ); + // collect global variables pGlobalVars = ABC_CALLOC( int, sat_solver_nvars(pSat) ); Vec_IntForEachEntry( p->vVarsAB, Var, i ) |