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

Enabling runtime limit in "lutexact".

This commit is contained in:
Alan Mishchenko 2025-11-02 19:08:59 -08:00
parent f897673f68
commit 8f06ce9112
1 changed files with 8 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
src/sat/bmc/bmcMaj2.c
View File

@ -1411,6 +1411,8 @@ void Exa3_ManExactSynthesis2( Bmc_EsPar_t * pPars )
status = Exa3_ManAddCnfStart( p, pPars->fOnlyAnd );
assert( status );
printf( "Running exact synthesis for %d-input function with %d %d-input LUTs...\n", p->nVars, p->nNodes, p->nLutSize );
abctime nTimeToStop = pPars->RuntimeLim ? pPars->RuntimeLim * CLOCKS_PER_SEC + Abc_Clock(): 0;
sat_solver_set_runtime_limit( p->pSat, nTimeToStop );
for ( i = 0; iMint != -1; i++ )
{
abctime clk = Abc_Clock();
@ -1426,6 +1428,12 @@ void Exa3_ManExactSynthesis2( Bmc_EsPar_t * pPars )
printf( "Conf =%9d ", sat_solver_nconflicts(p->pSat) );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
}
if ( nTimeToStop && Abc_Clock() > nTimeToStop )
{
printf( "Runtime limit (%d sec) is reached. ", pPars->RuntimeLim );
status = l_Undef;
break;
}
if ( status == l_False )
{
printf( "The problem has no solution.\n" );