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

Improving timeout in the interpolation package.

This commit is contained in:
Alan Mishchenko 2011-04-15 09:29:13 -07:00
parent 3dfdbe1402
commit 813245b29a
5 changed files with 38 additions and 19 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
src/aig/int/intCheck.c
View File

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

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

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

4
src/aig/int/intInt.h
View File

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

6
src/aig/int/intM114.c
View File

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

5
src/base/abci/abc.c
View File

@ -8535,11 +8535,6 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
}
*/
{
// extern void Ssm_ManExperiment( char * pFileIn, char * pFileOut );
// Ssm_ManExperiment( "m\\big2.ssim", "m\\big2_.ssim" );
}
return 0;
usage:
Abc_Print( -2, "usage: test [-CKDN] [-vwh] <file_name>\n" );