diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2011-04-08 15:35:59 -0700 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2011-04-08 15:35:59 -0700 |
commit | 5222f382af8c6d9174359da92f44abee4afa0331 (patch) | |
tree | f88b424d57e36b20f03244778043b13e91c1c2d6 /src/base/abci | |
parent | 234fb8c7e323679d5ce9daa161bb1a0bba07a96b (diff) | |
download | abc-5222f382af8c6d9174359da92f44abee4afa0331.tar.gz abc-5222f382af8c6d9174359da92f44abee4afa0331.tar.bz2 abc-5222f382af8c6d9174359da92f44abee4afa0331.zip |
Adding SAT-solver-level timeouts to the BMC engines.
Diffstat (limited to 'src/base/abci')
-rw-r--r-- | src/base/abci/abcDar.c | 58 |
1 files changed, 32 insertions, 26 deletions
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c index b28d3de4..d443c5e5 100644 --- a/src/base/abci/abcDar.c +++ b/src/base/abci/abcDar.c @@ -1682,18 +1682,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(); - -/* - s_fInterrupt = 0; - if ( signal(SIGINT,sigfunc) == SIG_ERR ) - { - printf("Could not setup signal handler for SIGINT!\n"); - return RetValue; - } - printf("Waiting for SIGINT. Press Ctrl+C to exit.\n"); -// while ( !s_fInterrupt ); -// return RetValue; -*/ + int nTimeLimit = nTimeOut ? clock() + nTimeOut * CLOCKS_PER_SEC : 0; // derive the AIG manager pMan = Abc_NtkToDar( pNtk, 0, 1 ); @@ -1715,17 +1704,23 @@ int Abc_NtkDarBmc( Abc_Ntk_t * pNtk, int nStart, int nFrames, int nSizeMax, int pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL; if ( RetValue == 1 ) { -// printf( "No output was asserted in %d frames. ", iFrame ); +// printf( "No output asserted in %d frames. ", iFrame ); printf( "Incorrect return value. " ); } else if ( RetValue == -1 ) - printf( "No output was asserted in %d frames. Reached conflict limit (%d). ", iFrame, nBTLimit ); + { + printf( "No output asserted in %d frames. Resource limit reached ", iFrame ); + if ( nTimeLimit < clock() ) + printf( "(timeout %d sec). ", nTimeLimit ); + else + printf( "(conf limit %d). ", nBTLimit ); + } else // if ( RetValue == 0 ) { // extern void Aig_ManCounterExampleValueTest( Aig_Man_t * pAig, Abc_Cex_t * pCex ); Abc_Cex_t * pCex = pNtk->pSeqModel; - printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump a witness). ", pCex->iPo, pCex->iFrame ); + printf( "Output %d asserted in frame %d (use \"write_counter\" to dump a witness). ", pCex->iPo, pCex->iFrame ); // Aig_ManCounterExampleValueTest( pMan, pCex ); } @@ -1741,12 +1736,12 @@ ABC_PRT( "Time", clock() - clk ); if ( pNtk->pSeqModel ) { Abc_Cex_t * pCex = pNtk->pSeqModel; - printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump a witness). ", pCex->iPo, pCex->iFrame ); + printf( "Output %d asserted in frame %d (use \"write_counter\" to dump a witness). ", pCex->iPo, pCex->iFrame ); RetValue = 0; } else { - printf( "No output was asserted in %d frames. ", nFrames ); + printf( "No output asserted in %d frames. ", nFrames ); RetValue = 1; } */ @@ -1757,13 +1752,13 @@ ABC_PRT( "Time", clock() - clk ); ABC_FREE( pNtk->pSeqModel ); pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL; if ( RetValue == 1 ) - printf( "No output was asserted in %d frames. ", iFrame ); + printf( "No output asserted in %d frames. ", iFrame ); else if ( RetValue == -1 ) - printf( "No output was asserted in %d frames. Reached conflict limit (%d). ", iFrame, nBTLimit ); + printf( "No output asserted in %d frames. Reached conflict limit (%d). ", iFrame, nBTLimit ); else // if ( RetValue == 0 ) { Abc_Cex_t * pCex = pNtk->pSeqModel; - printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump a witness). ", pCex->iPo, pCex->iFrame ); + printf( "Output %d asserted in frame %d (use \"write_counter\" to dump a witness). ", pCex->iPo, pCex->iFrame ); } */ RetValue = Saig_BmcPerform( pMan, nStart, nFrames, nNodeDelta, nTimeOut, nBTLimit, nBTLimitAll, fVerbose, 0, piFrames ); @@ -1797,6 +1792,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; pMan = Abc_NtkToDar( pNtk, 0, 1 ); if ( pMan == NULL ) { @@ -1810,16 +1806,26 @@ int Abc_NtkDarBmc3( Abc_Ntk_t * pNtk, Saig_ParBmc_t * pPars ) pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL; if ( RetValue == 1 ) { -// printf( "No output was asserted in %d frames. ", pPars->iFrame ); +// printf( "No output asserted in %d frames. ", pPars->iFrame ); printf( "Incorrect return value. " ); } else if ( RetValue == -1 ) { if ( pPars->nFailOuts == 0 ) - printf( "No output was asserted in %d frames. Reached conflict limit (%d). ", pPars->iFrame, pPars->nConfLimit ); + { + printf( "No output asserted in %d frames. Resource limit reached ", pPars->iFrame ); + if ( nTimeOut < clock() ) + printf( "(timeout %d sec). ", pPars->nTimeOut ); + else + printf( "(conf limit %d). ", pPars->nConfLimit ); + } else { - printf( "The total of %d outputs was asserted in %d frames. Reached conflict limit (%d). ", pPars->nFailOuts, pPars->iFrame, pPars->nConfLimit ); + printf( "The total of %d outputs asserted in %d frames. Resource limit reached ", pPars->nFailOuts, pPars->iFrame ); + if ( nTimeOut < clock() ) + printf( "(timeout %d sec). ", pPars->nTimeOut ); + else + printf( "(conf limit %d). ", pPars->nConfLimit ); if ( pNtk->pSeqModelVec ) Vec_PtrFreeFree( pNtk->pSeqModelVec ); pNtk->pSeqModelVec = pMan->pSeqModelVec; pMan->pSeqModelVec = NULL; @@ -1830,12 +1836,12 @@ int Abc_NtkDarBmc3( Abc_Ntk_t * pNtk, Saig_ParBmc_t * pPars ) if ( !pPars->fSolveAll ) { Abc_Cex_t * pCex = pNtk->pSeqModel; - printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump a witness). ", pCex->iPo, pCex->iFrame ); + printf( "Output %d asserted in frame %d (use \"write_counter\" to dump a witness). ", pCex->iPo, pCex->iFrame ); } else { printf( "Incorrect return value. " ); -// printf( "At least one output was asserted (out=%d, frame=%d). ", pCex->iPo, pCex->iFrame ); +// printf( "At least one output asserted (out=%d, frame=%d). ", pCex->iPo, pCex->iFrame ); } } ABC_PRT( "Time", clock() - clk ); @@ -2133,7 +2139,7 @@ int Abc_NtkDarProve( Abc_Ntk_t * pNtk, Fra_Sec_t * pSecPar ) if ( pNtk->pSeqModel ) { Abc_Cex_t * pCex = pNtk->pSeqModel; - printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump a witness).\n", pCex->iPo, pCex->iFrame ); + printf( "Output %d asserted in frame %d (use \"write_counter\" to dump a witness).\n", pCex->iPo, pCex->iFrame ); if ( !Saig_ManVerifyCex( pMan, pNtk->pSeqModel ) ) printf( "Abc_NtkDarProve(): Counter-example verification has FAILED.\n" ); } |