diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2013-09-05 19:32:45 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2013-09-05 19:32:45 -0700 |
| commit | 9d14b0c094cc0509bf167166e6fbddeb0f8ba954 (patch) | |
| tree | 14f9944a133c9a444a86118d92cf76feff6e2e1f /src/base | |
| parent | 191a9ccd385c853c4485e170c7669997371334b8 (diff) | |
| download | abc-9d14b0c094cc0509bf167166e6fbddeb0f8ba954.tar.gz abc-9d14b0c094cc0509bf167166e6fbddeb0f8ba954.tar.bz2 abc-9d14b0c094cc0509bf167166e6fbddeb0f8ba954.zip | |
Updates for the new BMC engine.
Diffstat (limited to 'src/base')
| -rw-r--r-- | src/base/abci/abc.c | 17 |
1 files changed, 11 insertions, 6 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 9c51f5da..122e5b38 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -31619,6 +31619,7 @@ int Abc_CommandAbc9Bmc( Abc_Frame_t * pAbc, int argc, char ** argv ) pPars->nFramesMax = 0; // maximum number of timeframes pPars->nConfLimit = 0; // maximum number of conflicts at a node pPars->fLoadCnf = 0; // dynamic CNF loading + pPars->fDumpFrames = 0; // dump unrolled timeframes pPars->fVerbose = 0; // verbose pPars->fVeryVerbose = 0; // very verbose pPars->fNotVerbose = 0; // skip line-by-line print-out @@ -31626,7 +31627,7 @@ int Abc_CommandAbc9Bmc( Abc_Frame_t * pAbc, int argc, char ** argv ) pPars->nFailOuts = 0; // the number of failed outputs pPars->nDropOuts = 0; // the number of dropped outputs Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "SFcvwh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "SFcdvwh" ) ) != EOF ) { switch ( c ) { @@ -31655,6 +31656,9 @@ int Abc_CommandAbc9Bmc( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'c': pPars->fLoadCnf ^= 1; break; + case 'd': + pPars->fDumpFrames ^= 1; + break; case 'v': pPars->fVerbose ^= 1; break; @@ -31677,12 +31681,13 @@ int Abc_CommandAbc9Bmc( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: &bmc [-SF num] [-cvwh]\n" ); + Abc_Print( -2, "usage: &bmc [-SF num] [-cdvwh]\n" ); Abc_Print( -2, "\t performs bounded model checking\n" ); - Abc_Print( -2, "\t-S num : the starting timeframe [default = %d]\n", pPars->nStart ); - Abc_Print( -2, "\t-F num : the maximum number of timeframes [default = %d]\n", pPars->nFramesMax ); - Abc_Print( -2, "\t-c : toggle dynamic CNF loading [default = %s]\n", pPars->fLoadCnf? "yes": "no" ); - Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" ); + Abc_Print( -2, "\t-S num : the starting timeframe [default = %d]\n", pPars->nStart ); + Abc_Print( -2, "\t-F num : the maximum number of timeframes [default = %d]\n", pPars->nFramesMax ); + Abc_Print( -2, "\t-c : toggle dynamic CNF loading [default = %s]\n", pPars->fLoadCnf? "yes": "no" ); + Abc_Print( -2, "\t-d : toggle dumping unfolded timeframes [default = %s]\n", pPars->fDumpFrames? "yes": "no" ); + Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" ); Abc_Print( -2, "\t-w : toggle printing information about unfolding [default = %s]\n", pPars->fVeryVerbose? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); return 1; |