From 5222f382af8c6d9174359da92f44abee4afa0331 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Fri, 8 Apr 2011 15:35:59 -0700 Subject: Adding SAT-solver-level timeouts to the BMC engines. --- src/aig/saig/saigBmc2.c | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) (limited to 'src/aig/saig/saigBmc2.c') diff --git a/src/aig/saig/saigBmc2.c b/src/aig/saig/saigBmc2.c index 8e537142..1fc5a11a 100644 --- a/src/aig/saig/saigBmc2.c +++ b/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; -- cgit v1.2.3