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

Setting the default limit on the number of timeframe in bmc2/bmc3 to 0 (infinity).

This commit is contained in:
Alan Mishchenko 2012-02-19 09:55:52 -08:00
parent 7ca9c116df
commit c9147d76cc
3 changed files with 10 additions and 6 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
src/aig/saig/saigBmc2.c
View File

@ -759,7 +759,6 @@ int Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax
vSimInfo = Abs_ManTernarySimulate( pAig, nFramesMax, fVerbose );
Abs_ManFreeAray( vSimInfo );
*/
p = Saig_BmcManStart( pAig, nFramesMax, nNodesMax, nConfMaxOne, nConfMaxAll, fVerbose );
if ( fVerbose )
{
printf( "Running \"bmc2\". AIG: PI/PO/Reg = %d/%d/%d. Node = %6d. Lev = %5d.\n",
@ -768,6 +767,8 @@ 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 );
}
nFramesMax = nFramesMax ? nFramesMax : ABC_INFINITY;
p = Saig_BmcManStart( pAig, nFramesMax, nNodesMax, nConfMaxOne, nConfMaxAll, fVerbose );
// set runtime limit
if ( nTimeOut )
sat_solver_set_runtime_limit( p->pSat, nTimeToStop );

7
src/aig/saig/saigBmc3.c
View File

@ -1076,7 +1076,7 @@ void Saig_ParBmcSetDefaultParams( Saig_ParBmc_t * p )
{
memset( p, 0, sizeof(Saig_ParBmc_t) );
p->nStart = 0; // maximum number of timeframes
p->nFramesMax = 2000; // maximum number of timeframes
p->nFramesMax = 0; // maximum number of timeframes
p->nConfLimit = 2000; // maximum number of conflicts at a node
p->nConfLimitJump = 0; // maximum number of conflicts after jumping
p->nFramesJump = 0; // the number of tiemframes to jump
@ -1120,6 +1120,7 @@ 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 );
}
pPars->nFramesMax = pPars->nFramesMax ? pPars->nFramesMax : ABC_INFINITY;
// set runtime limit
if ( p->pPars->nTimeOut )
sat_solver_set_runtime_limit( p->pSat, nTimeToStop );
@ -1246,7 +1247,9 @@ clkOther += clock() - clk2;
printf( "Cla =%9.0f. ", (double)p->pSat->stats.clauses );
printf( "Conf =%7.0f. ",(double)p->pSat->stats.conflicts );
printf( "Imp =%10.0f. ", (double)p->pSat->stats.propagations );
ABC_PRT( "Time", clock() - clk );
// ABC_PRT( "Time", clock() - clk );
printf( "%9.2f sec", (float)(clock() - clkTotal)/(float)(CLOCKS_PER_SEC) );
printf( "\n" );
// ABC_PRM( "Id2Var", (f+1)*p->nObjNums*4 );
// ABC_PRM( "SAT", 42 * p->pSat->size + 16 * (int)p->pSat->stats.clauses + 4 * (int)p->pSat->stats.clauses_literals );
// printf( "Simples = %6d. ", p->nBufNum );

6
src/base/abci/abc.c
View File

@ -19113,7 +19113,7 @@ int Abc_CommandBmc2( Abc_Frame_t * pAbc, int argc, char ** argv )
// set defaults
nStart = 0;
nFrames = 2000;
nFrames = 0;
nSizeMax = 200000;
nBTLimit = 2000;
nBTLimitAll = 2000000;
@ -19255,7 +19255,7 @@ usage:
Abc_Print( -2, "usage: bmc2 [-SFTCGD num] [-L file] [-vh]\n" );
Abc_Print( -2, "\t performs bounded model checking with dynamic unrolling\n" );
Abc_Print( -2, "\t-S num : the starting time frame [default = %d]\n", nStart );
Abc_Print( -2, "\t-F num : the max number of time frames [default = %d]\n", nFrames );
Abc_Print( -2, "\t-F num : the max number of time frames (0 = unused) [default = %d]\n", nFrames );
// Abc_Print( -2, "\t-N num : the max number of nodes in the frames [default = %d]\n", nSizeMax );
Abc_Print( -2, "\t-T num : approximate runtime limit in seconds [default = %d]\n", nTimeOut );
Abc_Print( -2, "\t-C num : the max number of conflicts at a node [default = %d]\n", nBTLimit );
@ -19442,7 +19442,7 @@ usage:
Abc_Print( -2, "usage: bmc3 [-SFTCDJI num] [-L file] [-sdvh]\n" );
Abc_Print( -2, "\t performs bounded model checking with dynamic unrolling\n" );
Abc_Print( -2, "\t-S num : the starting time frame [default = %d]\n", pPars->nStart );
Abc_Print( -2, "\t-F num : the max number of time frames [default = %d]\n", pPars->nFramesMax );
Abc_Print( -2, "\t-F num : the max number of time frames (0 = unused) [default = %d]\n", pPars->nFramesMax );
Abc_Print( -2, "\t-T num : approximate runtime limit in seconds [default = %d]\n", pPars->nTimeOut );
Abc_Print( -2, "\t-C num : max conflicts at an output [default = %d]\n", pPars->nConfLimit );
Abc_Print( -2, "\t-D num : max conflicts after jumping (0 = infinity) [default = %d]\n", pPars->nConfLimitJump );