diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2014-08-12 18:54:43 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2014-08-12 18:54:43 -0700 |
| commit | f907347484874a4c5ff9ffdde9426e0229fac22d (patch) | |
| tree | 8c26bb12e6c080ccdeee17cf38b4324558cc639a /src/base | |
| parent | 9055265394006a1c14688a018db48d06ba14e756 (diff) | |
| download | abc-f907347484874a4c5ff9ffdde9426e0229fac22d.tar.gz abc-f907347484874a4c5ff9ffdde9426e0229fac22d.tar.bz2 abc-f907347484874a4c5ff9ffdde9426e0229fac22d.zip | |
Enabling circuit solver in &fraig.
Diffstat (limited to 'src/base')
| -rw-r--r-- | src/base/abci/abc.c | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index dff328eb..6ca352cd 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -28931,7 +28931,7 @@ int Abc_CommandAbc9Fraig( Abc_Frame_t * pAbc, int argc, char ** argv ) Cec_ManFraSetDefaultParams( pPars ); pPars->fSatSweeping = 1; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "WRILDCrmdwvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "WRILDCrmdcwvh" ) ) != EOF ) { switch ( c ) { @@ -29010,6 +29010,9 @@ int Abc_CommandAbc9Fraig( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'd': pPars->fDualOut ^= 1; break; + case 'c': + pPars->fRunCSat ^= 1; + break; case 'w': pPars->fVeryVerbose ^= 1; break; @@ -29030,7 +29033,7 @@ int Abc_CommandAbc9Fraig( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: &fraig [-WRILDC <num>] [-rmdwvh]\n" ); + Abc_Print( -2, "usage: &fraig [-WRILDC <num>] [-rmdcwvh]\n" ); Abc_Print( -2, "\t performs combinational SAT sweeping\n" ); Abc_Print( -2, "\t-W num : the number of simulation words [default = %d]\n", pPars->nWords ); Abc_Print( -2, "\t-R num : the number of simulation rounds [default = %d]\n", pPars->nRounds ); @@ -29041,6 +29044,7 @@ usage: Abc_Print( -2, "\t-r : toggle the use of AIG rewriting [default = %s]\n", pPars->fRewriting? "yes": "no" ); Abc_Print( -2, "\t-m : toggle miter vs. any circuit [default = %s]\n", pPars->fCheckMiter? "miter": "circuit" ); Abc_Print( -2, "\t-d : toggle using double output miters [default = %s]\n", pPars->fDualOut? "yes": "no" ); + Abc_Print( -2, "\t-c : toggle using circuit-based solver [default = %s]\n", pPars->fRunCSat? "yes": "no" ); Abc_Print( -2, "\t-w : toggle printing even more verbose information [default = %s]\n", pPars->fVeryVerbose? "yes": "no" ); Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); |