Commit 7857b7fd by Alan Mishchenko

Renaming command-line option '-s' to be '-q' in 'pdr'.

parent be49b0fa
...@@ -26678,7 +26678,7 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -26678,7 +26678,7 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv )
int c; int c;
Pdr_ManSetDefaultParams( pPars ); Pdr_ManSetDefaultParams( pPars );
Extra_UtilGetoptReset(); Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "MFCDQTHGSaxrmuyfsipdegjonctkvwzh" ) ) != EOF ) while ( ( c = Extra_UtilGetopt( argc, argv, "MFCDQTHGSaxrmuyfqipdegjonctkvwzh" ) ) != EOF )
{ {
switch ( c ) switch ( c )
{ {
...@@ -26802,7 +26802,7 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -26802,7 +26802,7 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'f': case 'f':
pPars->fFlopOrder ^= 1; pPars->fFlopOrder ^= 1;
break; break;
case 's': case 'q':
pPars->fShortest ^= 1; pPars->fShortest ^= 1;
break; break;
case 'i': case 'i':
...@@ -26879,7 +26879,7 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -26879,7 +26879,7 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0; return 0;
usage: usage:
Abc_Print( -2, "usage: pdr [-MFCDQTHGS <num>] [-axrmuyfsipdegjonctkvwzh]\n" ); Abc_Print( -2, "usage: pdr [-MFCDQTHGS <num>] [-axrmuyfqipdegjonctkvwzh]\n" );
Abc_Print( -2, "\t model checking using property directed reachability (aka IC3)\n" ); Abc_Print( -2, "\t model checking using property directed reachability (aka IC3)\n" );
Abc_Print( -2, "\t pioneered by Aaron R. Bradley (http://theory.stanford.edu/~arbrad/)\n" ); Abc_Print( -2, "\t pioneered by Aaron R. Bradley (http://theory.stanford.edu/~arbrad/)\n" );
Abc_Print( -2, "\t with improvements by Niklas Een (http://een.se/niklas/)\n" ); Abc_Print( -2, "\t with improvements by Niklas Een (http://een.se/niklas/)\n" );
...@@ -26899,7 +26899,7 @@ usage: ...@@ -26899,7 +26899,7 @@ usage:
Abc_Print( -2, "\t-u : toggle updated X-valued simulation [default = %s]\n", pPars->fNewXSim? "yes": "no" ); Abc_Print( -2, "\t-u : toggle updated X-valued simulation [default = %s]\n", pPars->fNewXSim? "yes": "no" );
Abc_Print( -2, "\t-y : toggle using structural flop priorities [default = %s]\n", pPars->fFlopPrio? "yes": "no" ); Abc_Print( -2, "\t-y : toggle using structural flop priorities [default = %s]\n", pPars->fFlopPrio? "yes": "no" );
Abc_Print( -2, "\t-f : toggle ordering flops by cost before generalization [default = %s]\n", pPars->fFlopOrder? "yes": "no" ); Abc_Print( -2, "\t-f : toggle ordering flops by cost before generalization [default = %s]\n", pPars->fFlopOrder? "yes": "no" );
Abc_Print( -2, "\t-s : toggle creating only shortest counter-examples [default = %s]\n", pPars->fShortest? "yes": "no" ); Abc_Print( -2, "\t-q : toggle creating only shortest counter-examples [default = %s]\n", pPars->fShortest? "yes": "no" );
Abc_Print( -2, "\t-i : toggle clause pushing from an intermediate timeframe [default = %s]\n", pPars->fShiftStart? "yes": "no" ); Abc_Print( -2, "\t-i : toggle clause pushing from an intermediate timeframe [default = %s]\n", pPars->fShiftStart? "yes": "no" );
Abc_Print( -2, "\t-p : toggle reusing proof-obligations in the last timeframe [default = %s]\n", pPars->fReuseProofOblig? "yes": "no" ); Abc_Print( -2, "\t-p : toggle reusing proof-obligations in the last timeframe [default = %s]\n", pPars->fReuseProofOblig? "yes": "no" );
Abc_Print( -2, "\t-d : toggle dumping invariant (valid if init state is all-0) [default = %s]\n", pPars->fDumpInv? "yes": "no" ); Abc_Print( -2, "\t-d : toggle dumping invariant (valid if init state is all-0) [default = %s]\n", pPars->fDumpInv? "yes": "no" );
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment