summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/aig/saig/saigBmc2.c8
-rw-r--r--src/aig/saig/saigBmc3.c4
-rw-r--r--src/base/abci/abcDar.c58
-rw-r--r--src/sat/bsat/satSolver.c2
-rw-r--r--src/sat/bsat/satSolver.h8
5 files changed, 51 insertions, 29 deletions
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;
diff --git a/src/aig/saig/saigBmc3.c b/src/aig/saig/saigBmc3.c
index 570e8a26..e038d7a0 100644
--- a/src/aig/saig/saigBmc3.c
+++ b/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;
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" );
}
diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c
index aa8c7f08..de186047 100644
--- a/src/sat/bsat/satSolver.c
+++ b/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");
diff --git a/src/sat/bsat/satSolver.h b/src/sat/bsat/satSolver.h
index 2b148328..a33c7240 100644
--- a/src/sat/bsat/satSolver.h
+++ b/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
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-15 23:34:10 +0000