diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2013-10-31 20:30:40 -0400 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2013-10-31 20:30:40 -0400 |
commit | 34366b8aca94b80051de58291ef853d292827f1d (patch) | |
tree | bc4284cec4af0561e0ae09cf4f3463a1b69e3a40 /src/base/abci | |
parent | e8c765c0d1b722f5d1e143928ee7fbf05ec713c6 (diff) | |
download | abc-34366b8aca94b80051de58291ef853d292827f1d.tar.gz abc-34366b8aca94b80051de58291ef853d292827f1d.tar.bz2 abc-34366b8aca94b80051de58291ef853d292827f1d.zip |
Specialized induction check.
Diffstat (limited to 'src/base/abci')
-rw-r--r-- | src/base/abci/abc.c | 18 |
1 files changed, 11 insertions, 7 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 075dd9ca..3da41636 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -32576,9 +32576,9 @@ usage: ***********************************************************************/ int Abc_CommandAbc9ICheck( Abc_Frame_t * pAbc, int argc, char ** argv ) { - int c, nFramesMax = 1, nTimeOut = 0, fVerbose = 0; + int c, nFramesMax = 1, nTimeOut = 0, fEmpty = 0, fVerbose = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "MTvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "MTevh" ) ) != EOF ) { switch ( c ) { @@ -32604,6 +32604,9 @@ int Abc_CommandAbc9ICheck( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( nTimeOut < 0 ) goto usage; break; + case 'e': + fEmpty ^= 1; + break; case 'v': fVerbose ^= 1; break; @@ -32623,15 +32626,16 @@ int Abc_CommandAbc9ICheck( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( -1, "Abc_CommandAbc9ICheck(): The AIG is combinational.\n" ); return 0; } - Bmc_PerformICheck( pAbc->pGia, nFramesMax, nTimeOut, fVerbose ); + Bmc_PerformICheck( pAbc->pGia, nFramesMax, nTimeOut, fEmpty, fVerbose ); return 0; usage: - Abc_Print( -2, "usage: &icheck [-MT num] [-cvh]\n" ); + Abc_Print( -2, "usage: &icheck [-MT num] [-evh]\n" ); Abc_Print( -2, "\t performs specialized induction check\n" ); - Abc_Print( -2, "\t-M num : the number of timeframes used for induction [default = %d]\n", nFramesMax ); - Abc_Print( -2, "\t-T num : approximate global runtime limit in seconds [default = %d]\n", nTimeOut ); - Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); + Abc_Print( -2, "\t-M num : the number of timeframes used for induction [default = %d]\n", nFramesMax ); + Abc_Print( -2, "\t-T num : approximate global runtime limit in seconds [default = %d]\n", nTimeOut ); + Abc_Print( -2, "\t-e : toggle using empty set of next-state functions [default = %s]\n", fEmpty? "yes": "no" ); + Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); return 1; } |