diff options
Diffstat (limited to 'src/base/abci/abc.c')
| -rw-r--r-- | src/base/abci/abc.c | 40 |
1 files changed, 33 insertions, 7 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 563876e7..e26be80b 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -15114,6 +15114,7 @@ int Abc_CommandIProve( Abc_Frame_t * pAbc, int argc, char ** argv ) Prove_Params_t Params, * pParams = &Params; Abc_Ntk_t * pNtk, * pNtkTemp; int c, RetValue, iOut = -1; + char * pLogFileName = NULL; abctime clk; extern int Abc_NtkIvyProve( Abc_Ntk_t ** ppNtk, void * pPars ); @@ -15124,7 +15125,7 @@ int Abc_CommandIProve( Abc_Frame_t * pAbc, int argc, char ** argv ) pParams->fUseRewriting = 1; pParams->fVerbose = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "NCFGLIrfbvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "NCFGMILrfbvh" ) ) != EOF ) { switch ( c ) { @@ -15172,10 +15173,10 @@ int Abc_CommandIProve( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( pParams->nFraigingLimitMulti < 0 ) goto usage; break; - case 'L': + case 'M': if ( globalUtilOptind >= argc ) { - Abc_Print( -1, "Command line switch \"-L\" should be followed by an integer.\n" ); + Abc_Print( -1, "Command line switch \"-M\" should be followed by an integer.\n" ); goto usage; } pParams->nMiteringLimitLast = atoi(argv[globalUtilOptind]); @@ -15194,6 +15195,15 @@ int Abc_CommandIProve( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( pParams->nTotalInspectLimit < 0 ) goto usage; break; + case 'L': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-L\" should be followed by a file name.\n" ); + goto usage; + } + pLogFileName = argv[globalUtilOptind]; + globalUtilOptind++; + break; case 'r': pParams->fUseRewriting ^= 1; break; @@ -15267,17 +15277,20 @@ int Abc_CommandIProve( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Cex_t * pCex = Abc_CexDeriveFromCombModel( pNtkTemp->pModel, Abc_NtkPiNum(pNtkTemp), 0, iOut ); Abc_FrameReplaceCex( pAbc, &pCex ); } + if ( pLogFileName ) + Abc_NtkWriteLogFile( pLogFileName, pAbc->pCex, pAbc->Status, pAbc->nFrames, "iprove" ); return 0; usage: - Abc_Print( -2, "usage: iprove [-NCFGLI num] [-rfbvh]\n" ); + Abc_Print( -2, "usage: iprove [-NCFGMI num] [-L file] [-rfbvh]\n" ); Abc_Print( -2, "\t performs CEC using a new method\n" ); Abc_Print( -2, "\t-N num : max number of iterations [default = %d]\n", pParams->nItersMax ); Abc_Print( -2, "\t-C num : max starting number of conflicts in mitering [default = %d]\n", pParams->nMiteringLimitStart ); Abc_Print( -2, "\t-F num : max starting number of conflicts in fraiging [default = %d]\n", pParams->nFraigingLimitStart ); Abc_Print( -2, "\t-G num : multiplicative coefficient for fraiging [default = %d]\n", (int)pParams->nFraigingLimitMulti ); - Abc_Print( -2, "\t-L num : max last-gasp number of conflicts in mitering [default = %d]\n", pParams->nMiteringLimitLast ); + Abc_Print( -2, "\t-M num : max last-gasp number of conflicts in mitering [default = %d]\n", pParams->nMiteringLimitLast ); Abc_Print( -2, "\t-I num : max number of clause inspections in all SAT calls [default = %d]\n", (int)pParams->nTotalInspectLimit ); + Abc_Print( -2, "\t-L file: the log file name [default = %s]\n", pLogFileName ? pLogFileName : "no logging" ); Abc_Print( -2, "\t-r : toggle the use of rewriting [default = %s]\n", pParams->fUseRewriting? "yes": "no" ); Abc_Print( -2, "\t-f : toggle the use of FRAIGing [default = %s]\n", pParams->fUseFraiging? "yes": "no" ); Abc_Print( -2, "\t-b : toggle the use of BDDs [default = %s]\n", pParams->fUseBdds? "yes": "no" ); @@ -27781,10 +27794,11 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv ) extern int Abc_NtkDarPdr( Abc_Ntk_t * pNtk, Pdr_Par_t * pPars ); Pdr_Par_t Pars, * pPars = &Pars; Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc), * pNtkUsed, * pNtkFlop = NULL; + char * pLogFileName = NULL; int c; Pdr_ManSetDefaultParams( pPars ); Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "MFCDQTHGSaxrmuyfqipdegjonctkvwzh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "MFCDQTHGSLaxrmuyfqipdegjonctkvwzh" ) ) != EOF ) { switch ( c ) { @@ -27887,6 +27901,15 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( pPars->nRandomSeed < 0 ) goto usage; break; + case 'L': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-L\" should be followed by a file name.\n" ); + goto usage; + } + pLogFileName = argv[globalUtilOptind]; + globalUtilOptind++; + break; case 'a': pPars->fSolveAll ^= 1; break; @@ -27984,10 +28007,12 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv ) else Abc_FrameReplaceCex( pAbc, &pNtkUsed->pSeqModel ); if ( pNtkFlop ) Abc_NtkDelete( pNtkFlop ); + if ( pLogFileName ) + Abc_NtkWriteLogFile( pLogFileName, pAbc->pCex, pAbc->Status, pAbc->nFrames, "pdr" ); return 0; usage: - Abc_Print( -2, "usage: pdr [-MFCDQTHGS <num>] [-axrmuyfqipdegjonctkvwzh]\n" ); + Abc_Print( -2, "usage: pdr [-MFCDQTHGS <num>] [-L <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" ); @@ -28000,6 +28025,7 @@ usage: Abc_Print( -2, "\t-H num : runtime limit per output, in miliseconds (with \"-a\") [default = %d]\n", pPars->nTimeOutOne ); 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-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" ); |