diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2017-09-07 19:16:13 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2017-09-07 19:16:13 -0700 |
| commit | ba0d855fd4eed9439e4ce4fa6eb778cbb2250708 (patch) | |
| tree | a348bf91fc74532e874613c9d3628d4af02460d5 /src/base | |
| parent | 68b59b8a1e09722cd71490c91904d5c3104535fa (diff) | |
| download | abc-ba0d855fd4eed9439e4ce4fa6eb778cbb2250708.tar.gz abc-ba0d855fd4eed9439e4ce4fa6eb778cbb2250708.tar.bz2 abc-ba0d855fd4eed9439e4ce4fa6eb778cbb2250708.zip | |
Trying to enable CNF simplification in &bmcs -g.
Diffstat (limited to 'src/base')
| -rw-r--r-- | src/base/abci/abc.c | 9 |
1 files changed, 7 insertions, 2 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 6c5e762a..66c0ecca 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -40017,6 +40017,7 @@ int Abc_CommandAbc9SBmc( Abc_Frame_t * pAbc, int argc, char ** argv ) pPars->fUseSynth = 0; // use synthesis pPars->fUseOldCnf = 0; // use old CNF construction pPars->fUseGlucose = 0; // use Glucose 3.0 + pPars->fUseEliminate = 0; // use variable elimination pPars->fVerbose = 0; // verbose pPars->fVeryVerbose = 0; // very verbose pPars->fNotVerbose = 0; // skip line-by-line print-out @@ -40026,7 +40027,7 @@ int Abc_CommandAbc9SBmc( Abc_Frame_t * pAbc, int argc, char ** argv ) pPars->pFuncOnFrameDone = pAbc->pFuncOnFrameDone; // frame done callback Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "PCFATgvwh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "PCFATgevwh" ) ) != EOF ) { switch ( c ) { @@ -40088,6 +40089,9 @@ int Abc_CommandAbc9SBmc( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'g': pPars->fUseGlucose ^= 1; break; + case 'e': + pPars->fUseEliminate ^= 1; + break; case 'v': pPars->fVerbose ^= 1; break; @@ -40116,7 +40120,7 @@ int Abc_CommandAbc9SBmc( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: &bmcs [-PCFAT num] [-gvwh]\n" ); + Abc_Print( -2, "usage: &bmcs [-PCFAT num] [-gevwh]\n" ); Abc_Print( -2, "\t performs bounded model checking\n" ); Abc_Print( -2, "\t-P num : the number of parallel solvers [default = %d]\n", pPars->nProcs ); Abc_Print( -2, "\t-C num : the SAT solver conflict limit [default = %d]\n", pPars->nConfLimit ); @@ -40124,6 +40128,7 @@ usage: Abc_Print( -2, "\t-A num : the number of additional frames to unroll [default = %d]\n", pPars->nFramesAdd ); Abc_Print( -2, "\t-T num : approximate timeout in seconds [default = %d]\n", pPars->nTimeOut ); Abc_Print( -2, "\t-g : toggle using Glucose 3.0 [default = %s]\n", pPars->fUseGlucose? "Glucose" : "Satoko" ); + Abc_Print( -2, "\t-e : toggle using variable eliminatation [default = %s]\n", pPars->fUseEliminate?"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"); |