Skip to content

A
abc
Commit 5222f382 by Alan Mishchenko
Options

Adding SAT-solver-level timeouts to the BMC engines.

parent 234fb8c7
Showing with 51 additions and 29 deletions
src/aig/saig/saigBmc2.c
......@@ -767,7 +767,9 @@ int Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax
printf( "Params: FramesMax = %d. NodesDelta = %d. ConfMaxOne = %d. ConfMaxAll = %d.\n",
nFramesMax, nNodesMax, nConfMaxOne, nConfMaxAll );
}
// set runtime limit
if ( nTimeOut )
sat_solver_set_runtime_limit( p->pSat, clock() + nTimeOut * CLOCKS_PER_SEC );
for ( Iter = 0; ; Iter++ )
{
clk2 = clock();
......@@ -841,8 +843,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
else if ( nTimeOut == 0 || nTimeOut > clock() )
printf( "Reached local conflict limit (%d).\n", p->nConfMaxOne );
else
printf( "Reached timeout (%d sec).\n", nTimeOut );
}
Saig_BmcManStop( p );
return Status;
......
src/aig/saig/saigBmc3.c
......@@ -1054,6 +1054,10 @@ int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars )
printf( "Params: Start = %d. FramesMax = %d. ConfLimit = %d. TimeOut = %d. SolveAll = %d.\n",
pPars->nStart, pPars->nFramesMax, pPars->nConfLimit, pPars->nTimeOut, pPars->fSolveAll );
}
// set runtime limit
if ( p->pPars->nTimeOut )
sat_solver_set_runtime_limit( p->pSat, clock() + p->pPars->nTimeOut * CLOCKS_PER_SEC );
// perform frames
for ( f = 0; f < pPars->nFramesMax; f++ )
{
pPars->iFrame = f;
......
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" );
}
......
src/sat/bsat/satSolver.c
......@@ -1521,6 +1521,8 @@ 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 )
break;
}
if (s->verbosity >= 1)
printf("==============================================================================\n");
......
src/sat/bsat/satSolver.h
......@@ -164,6 +164,7 @@ struct sat_solver_t
ABC_INT64_T nConfLimit; // external limit on the number of conflicts
ABC_INT64_T nInsLimit; // external limit on the number of implications
int nRuntimeLimit; // external limit on runtime
veci act_vars; // variables whose activity has changed
double* factors; // the activity factors
......@@ -220,7 +221,12 @@ static int sat_solver_final(sat_solver* s, int ** ppArray)
return s->conf_final.size;
}
static int sat_solver_set_runtime_limit(sat_solver* s, int Limit)
{
int nRuntimeLimit = s->nRuntimeLimit;
s->nRuntimeLimit = Limit;
return nRuntimeLimit;
}
ABC_NAMESPACE_HEADER_END
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment