diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2013-11-01 13:36:51 -0400 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2013-11-01 13:36:51 -0400 |
| commit | a564e2ab8184f330e87da811cedfd3faf2ee4041 (patch) | |
| tree | c356f2df0bc385b936e9bb68f68b31cda822a975 /src/base/abci | |
| parent | a509fa8ea89cc6374c7a13e7632cb51bc455ce43 (diff) | |
| download | abc-a564e2ab8184f330e87da811cedfd3faf2ee4041.tar.gz abc-a564e2ab8184f330e87da811cedfd3faf2ee4041.tar.bz2 abc-a564e2ab8184f330e87da811cedfd3faf2ee4041.zip | |
Sweeper internal verification and new switch for &cfraig.
Diffstat (limited to 'src/base/abci')
| -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 e37944cf..69e8ed84 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -28733,7 +28733,7 @@ int Abc_CommandAbc9CFraig( Abc_Frame_t * pAbc, int argc, char ** argv ) Ssc_Pars_t Pars, * pPars = &Pars; Ssc_ManSetDefaultParams( pPars ); Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "WCavh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "WCacvh" ) ) != EOF ) { switch ( c ) { @@ -28762,6 +28762,9 @@ int Abc_CommandAbc9CFraig( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'a': pPars->fAppend ^= 1; break; + case 'c': + pPars->fVerify ^= 1; + break; case 'v': pPars->fVerbose ^= 1; break; @@ -28779,13 +28782,14 @@ int Abc_CommandAbc9CFraig( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: &cfraig [-WC <num>] [-avh]\n" ); + Abc_Print( -2, "usage: &cfraig [-WC <num>] [-acvh]\n" ); Abc_Print( -2, "\t performs combinational SAT sweeping under constraints\n" ); Abc_Print( -2, "\t which are present in the AIG or set manually using \"constr\"\n" ); Abc_Print( -2, "\t (constraints are listed as last POs and true when they are 0)\n" ); Abc_Print( -2, "\t-W num : the number of simulation words [default = %d]\n", pPars->nWords ); Abc_Print( -2, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit ); Abc_Print( -2, "\t-a : toggle appending constraints to the result [default = %s]\n", pPars->fAppend? "yes": "no" ); + Abc_Print( -2, "\t-c : toggle performing internal verification [default = %s]\n", pPars->fVerify? "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"); return 1; |