diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2019-04-22 12:14:31 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2019-04-22 12:14:31 -0700 |
| commit | d07608c052cb673f4aef8096b5ad71dd662214cc (patch) | |
| tree | 9fb47da8cbfb09713d5c29e3fedbc6324f8263c3 /src/base | |
| parent | fa8716152f7dac92e868a5ccdca3507e282e5deb (diff) | |
| download | abc-d07608c052cb673f4aef8096b5ad71dd662214cc.tar.gz abc-d07608c052cb673f4aef8096b5ad71dd662214cc.tar.bz2 abc-d07608c052cb673f4aef8096b5ad71dd662214cc.zip | |
Adding the possibility to specify file name in 'pdr'.
Diffstat (limited to 'src/base')
| -rw-r--r-- | src/base/abci/abc.c | 14 |
1 files changed, 12 insertions, 2 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index a4e5cd22..b538db54 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -27945,7 +27945,7 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv ) int c; Pdr_ManSetDefaultParams( pPars ); Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "MFCDQTHGSLaxrmuyfqipdegjonctkvwzh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "MFCDQTHGSLIaxrmuyfqipdegjonctkvwzh" ) ) != EOF ) { switch ( c ) { @@ -28057,6 +28057,15 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv ) pLogFileName = argv[globalUtilOptind]; globalUtilOptind++; break; + case 'I': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-I\" should be followed by a file name.\n" ); + goto usage; + } + pPars->pInvFileName = argv[globalUtilOptind]; + globalUtilOptind++; + break; case 'a': pPars->fSolveAll ^= 1; break; @@ -28164,7 +28173,7 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: pdr [-MFCDQTHGS <num>] [-L <file>] [-axrmuyfqipdegjonctkvwzh]\n" ); + Abc_Print( -2, "usage: pdr [-MFCDQTHGS <num>] [-LI <file>] [-axrmuyfqipdegjonctkvwzh]\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 with improvements by Niklas Een (http://een.se/niklas/)\n" ); @@ -28178,6 +28187,7 @@ usage: Abc_Print( -2, "\t-G num : runtime gap since the last CEX (0 = no limit) [default = %d]\n", pPars->nTimeOutGap ); Abc_Print( -2, "\t-S num : * value to seed the SAT solver with [default = %d]\n", pPars->nRandomSeed ); Abc_Print( -2, "\t-L file: the log file name [default = %s]\n", pLogFileName ? pLogFileName : "no logging" ); + Abc_Print( -2, "\t-I file: the invariant file name [default = %s]\n", pPars->pInvFileName ? pPars->pInvFileName : "default name" ); Abc_Print( -2, "\t-a : toggle solving all outputs even if one of them is SAT [default = %s]\n", pPars->fSolveAll? "yes": "no" ); Abc_Print( -2, "\t-x : toggle storing CEXes when solving all outputs [default = %s]\n", pPars->fStoreCex? "yes": "no" ); Abc_Print( -2, "\t-r : toggle using more effort in generalization [default = %s]\n", pPars->fTwoRounds? "yes": "no" ); |