diff options
Diffstat (limited to 'src/base')
| -rw-r--r-- | src/base/abci/abc.c | 40 |
1 files changed, 38 insertions, 2 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index a30a2e55..62bed4c1 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -21246,7 +21246,7 @@ int Abc_CommandBmc3( Abc_Frame_t * pAbc, int argc, char ** argv ) int c; Saig_ParBmcSetDefaultParams( pPars ); Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "SFTHGCDJILaxdruvzh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "SFTHGCDJIPQRLaxdruvzh" ) ) != EOF ) { switch ( c ) { @@ -21349,6 +21349,39 @@ int Abc_CommandBmc3( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( pPars->nPisAbstract < 0 ) goto usage; break; + case 'P': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-P\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nLearnedStart = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nLearnedStart < 0 ) + goto usage; + break; + case 'Q': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-Q\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nLearnedDelta = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nLearnedDelta < 0 ) + goto usage; + break; + case 'R': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-R\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nLearnedPerce = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nLearnedPerce < 0 ) + goto usage; + break; case 'L': if ( globalUtilOptind >= argc ) { @@ -21433,7 +21466,7 @@ int Abc_CommandBmc3( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: bmc3 [-SFTHGCDJI num] [-L file] [-axduvzh]\n" ); + Abc_Print( -2, "usage: bmc3 [-SFTHGCDJIPQR num] [-L file] [-axduvzh]\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 (0 = unused) [default = %d]\n", pPars->nFramesMax ); @@ -21444,6 +21477,9 @@ usage: Abc_Print( -2, "\t-D num : max conflicts after jumping (0 = infinity) [default = %d]\n", pPars->nConfLimitJump ); Abc_Print( -2, "\t-J num : the number of timeframes to jump (0 = not used) [default = %d]\n", pPars->nFramesJump ); Abc_Print( -2, "\t-I num : the number of PIs to abstract [default = %d]\n", pPars->nPisAbstract ); + Abc_Print( -2, "\t-P num : the max number of learned clauses to keep (0=unused) [default = %d]\n", pPars->nLearnedStart ); + Abc_Print( -2, "\t-Q num : delta value for learned clause removal [default = %d]\n", pPars->nLearnedDelta ); + Abc_Print( -2, "\t-R num : ratio percentage for learned clause removal [default = %d]\n", pPars->nLearnedPerce ); Abc_Print( -2, "\t-L file: the log file name [default = %s]\n", pLogFileName ? pLogFileName : "no logging" ); Abc_Print( -2, "\t-a : solve all outputs (do not stop when one is SAT) [default = %s]\n", pPars->fSolveAll? "yes": "no" ); Abc_Print( -2, "\t-x : toggle storing CEXes when solving all outputs [default = %s]\n", pPars->fStoreCex? "yes": "no" ); |