diff options
Diffstat (limited to 'src/base/abci/abc.c')
-rw-r--r-- | src/base/abci/abc.c | 17 |
1 files changed, 12 insertions, 5 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index cb3d2d86..264b1df4 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -15348,9 +15348,10 @@ int Abc_CommandBmcInter( Abc_Frame_t * pAbc, int argc, char ** argv ) int fTransLoop; int fUsePudlak; int fCheckInd; + int fCheckKstep; int fVerbose; - extern int Abc_NtkDarBmcInter( Abc_Ntk_t * pNtk, int nConfLimit, int nFramesMax, int fRewrite, int fTransLoop, int fUsePudlak, int fCheckInd, int fVerbose ); + extern int Abc_NtkDarBmcInter( Abc_Ntk_t * pNtk, int nConfLimit, int nFramesMax, int fRewrite, int fTransLoop, int fUsePudlak, int fCheckInd, int fCheckKstep, int fVerbose ); pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); @@ -15363,9 +15364,10 @@ int Abc_CommandBmcInter( Abc_Frame_t * pAbc, int argc, char ** argv ) fTransLoop = 1; fUsePudlak = 0; fCheckInd = 0; + fCheckKstep= 0; fVerbose = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "CFrtpivh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "CFrtpikvh" ) ) != EOF ) { switch ( c ) { @@ -15403,6 +15405,9 @@ int Abc_CommandBmcInter( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'i': fCheckInd ^= 1; break; + case 'k': + fCheckKstep ^= 1; + break; case 'v': fVerbose ^= 1; break; @@ -15432,18 +15437,20 @@ int Abc_CommandBmcInter( Abc_Frame_t * pAbc, int argc, char ** argv ) fprintf( stdout, "Currently only works for single-output miters (run \"orpos\").\n" ); return 0; } - Abc_NtkDarBmcInter( pNtk, nBTLimit, nFramesMax, fRewrite, fTransLoop, fUsePudlak, fCheckInd, fVerbose ); + Abc_NtkDarBmcInter( pNtk, nBTLimit, nFramesMax, fRewrite, fTransLoop, fUsePudlak, fCheckInd, fCheckKstep, fVerbose ); return 0; usage: - fprintf( pErr, "usage: int [-CF num] [-rtpivh]\n" ); + fprintf( pErr, "usage: int [-CF num] [-rtpikvh]\n" ); fprintf( pErr, "\t uses interpolation to prove the property\n" ); fprintf( pErr, "\t-C num : the limit on conflicts for one SAT run [default = %d]\n", nBTLimit ); fprintf( pErr, "\t-F num : the limit on number of frames to unroll [default = %d]\n", nFramesMax ); fprintf( pErr, "\t-r : toggle the use of rewriting [default = %s]\n", fRewrite? "yes": "no" ); fprintf( pErr, "\t-t : toggle adding transition into the init state [default = %s]\n", fTransLoop? "yes": "no" ); - fprintf( pErr, "\t-p : toggle using original Pudlak's interpolation procedure [default = %s]\n", fUsePudlak? "yes": "no" ); +// fprintf( pErr, "\t-p : toggle using original Pudlak's interpolation procedure [default = %s]\n", fUsePudlak? "yes": "no" ); + fprintf( pErr, "\t-p : toggle using MiniSat-1.14p (now, Windows-only) [default = %s]\n", fUsePudlak? "yes": "no" ); fprintf( pErr, "\t-i : toggle inductive containment checking [default = %s]\n", fCheckInd? "yes": "no" ); + fprintf( pErr, "\t-k : toggle simple and k-step induction [default = %s]\n", fCheckKstep? "k-step": "simple" ); fprintf( pErr, "\t-v : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" ); fprintf( pErr, "\t-h : print the command usage\n"); return 1; |