diff options
Diffstat (limited to 'src/base/abci/abc.c')
| -rw-r--r-- | src/base/abci/abc.c | 12 |
1 files changed, 10 insertions, 2 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 0414687e..eb6f6145 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -8770,7 +8770,7 @@ int Abc_CommandTwoExact( Abc_Frame_t * pAbc, int argc, char ** argv ) Bmc_EsPar_t Pars, * pPars = &Pars; Bmc_EsParSetDefault( pPars ); Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "INTaogvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "INTadcogvh" ) ) != EOF ) { switch ( c ) { @@ -8810,6 +8810,12 @@ int Abc_CommandTwoExact( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'a': pPars->fOnlyAnd ^= 1; break; + case 'd': + pPars->fDynConstr ^= 1; + break; + case 'c': + pPars->fDumpCnf ^= 1; + break; case 'o': pPars->fFewerVars ^= 1; break; @@ -8854,12 +8860,14 @@ int Abc_CommandTwoExact( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: twoexact [-INT <num>] [-aogvh] <hex>\n" ); + Abc_Print( -2, "usage: twoexact [-INT <num>] [-adcogvh] <hex>\n" ); Abc_Print( -2, "\t exact synthesis of multi-input function using two-input gates\n" ); Abc_Print( -2, "\t-I <num> : the number of input variables [default = %d]\n", pPars->nVars ); Abc_Print( -2, "\t-N <num> : the number of two-input nodes [default = %d]\n", pPars->nNodes ); Abc_Print( -2, "\t-T <num> : the runtime limit in seconds [default = %d]\n", pPars->RuntimeLim ); Abc_Print( -2, "\t-a : toggle using only AND-gates (without XOR-gates) [default = %s]\n", pPars->fOnlyAnd ? "yes" : "no" ); + Abc_Print( -2, "\t-d : toggle using dynamic constraint addition [default = %s]\n", pPars->fDynConstr ? "yes" : "no" ); + Abc_Print( -2, "\t-c : toggle dumping CNF into a file [default = %s]\n", pPars->fDumpCnf ? "yes" : "no" ); Abc_Print( -2, "\t-o : toggle using additional optimizations [default = %s]\n", pPars->fFewerVars ? "yes" : "no" ); Abc_Print( -2, "\t-g : toggle using Glucose 3.0 by Gilles Audemard and Laurent Simon [default = %s]\n", pPars->fGlucose ? "yes" : "no" ); Abc_Print( -2, "\t-v : toggle verbose printout [default = %s]\n", pPars->fVerbose ? "yes" : "no" ); |