diff options
Diffstat (limited to 'src/base/io')
| -rw-r--r-- | src/base/io/io.c | 28 |
1 files changed, 20 insertions, 8 deletions
diff --git a/src/base/io/io.c b/src/base/io/io.c index b047bf92..11b1fa57 100644 --- a/src/base/io/io.c +++ b/src/base/io/io.c @@ -2310,6 +2310,8 @@ int IoCommandWriteCex( Abc_Frame_t * pAbc, int argc, char **argv ) char * pFileName; int c, fNames = 0; int fMinimize = 0; + int fUseSatBased = 0; + int fHighEffort = 0; int fUseOldMin = 0; int fCheckCex = 0; int forceSeq = 0; @@ -2318,7 +2320,7 @@ int IoCommandWriteCex( Abc_Frame_t * pAbc, int argc, char **argv ) int fVerbose = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "snmocafvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "snmueocafvh" ) ) != EOF ) { switch ( c ) { @@ -2331,6 +2333,12 @@ int IoCommandWriteCex( Abc_Frame_t * pAbc, int argc, char **argv ) case 'm': fMinimize ^= 1; break; + case 'u': + fUseSatBased ^= 1; + break; + case 'e': + fHighEffort ^= 1; + break; case 'o': fUseOldMin ^= 1; break; @@ -2419,6 +2427,8 @@ int IoCommandWriteCex( Abc_Frame_t * pAbc, int argc, char **argv ) if ( fCheckCex ) Bmc_CexCareVerify( pAig, pCex, pCare, fVerbose ); } + else if ( fUseSatBased ) + pCare = Bmc_CexCareSatBasedMinimize( pAig, Saig_ManPiNum(pAig), pCex, fHighEffort, fCheckCex, fVerbose ); else pCare = Bmc_CexCareMinimize( pAig, Saig_ManPiNum(pAig), pCex, 4, fCheckCex, fVerbose ); Aig_ManStop( pAig ); @@ -2477,19 +2487,21 @@ int IoCommandWriteCex( Abc_Frame_t * pAbc, int argc, char **argv ) return 0; usage: - fprintf( pAbc->Err, "usage: write_cex [-snmocfvh] <file>\n" ); - fprintf( pAbc->Err, "\t saves counter-example derived by \"sat\", \"iprove\", or \"dprove\"\n" ); - fprintf( pAbc->Err, "\t the file contains values for each PI in the natural order\n" ); - fprintf( pAbc->Err, "\t-s : always report a sequential ctrex (cycle 0 for comb) [default = %s]\n", forceSeq? "yes": "no" ); + fprintf( pAbc->Err, "usage: write_cex [-snmueocfvh] <file>\n" ); + fprintf( pAbc->Err, "\t saves counter-example (CEX) derived by \"sat\", \"iprove\", \"dprove\", etc\n" ); + fprintf( pAbc->Err, "\t the output file <file> contains values for each PI in natural order\n" ); + fprintf( pAbc->Err, "\t-s : always report a sequential CEX (cycle 0 for comb) [default = %s]\n", forceSeq? "yes": "no" ); fprintf( pAbc->Err, "\t-n : write input names into the file [default = %s]\n", fNames? "yes": "no" ); fprintf( pAbc->Err, "\t-m : minimize counter-example by dropping don't-care values [default = %s]\n", fMinimize? "yes": "no" ); - fprintf( pAbc->Err, "\t-o : use old counter-example minimization algorithm [default = %s]\n", fUseOldMin? "yes": "no" ); - fprintf( pAbc->Err, "\t-c : check generated counter-example using ternary simulation [default = %s]\n", fCheckCex? "yes": "no" ); + fprintf( pAbc->Err, "\t-u : use SAT-based CEX minimization [default = %s]\n", fUseSatBased? "yes": "no" ); + fprintf( pAbc->Err, "\t-e : use high-effort SAT-based CEX minimization [default = %s]\n", fHighEffort? "yes": "no" ); + fprintf( pAbc->Err, "\t-o : use old CEX minimization algorithm [default = %s]\n", fUseOldMin? "yes": "no" ); + fprintf( pAbc->Err, "\t-c : check generated CEX using ternary simulation [default = %s]\n", fCheckCex? "yes": "no" ); fprintf( pAbc->Err, "\t-a : print cex in AIGER 1.9 format [default = %s].\n", fAiger? "yes": "no" ); fprintf( pAbc->Err, "\t-f : enable printing flop values in each timeframe [default = %s].\n", fPrintFull? "yes": "no" ); fprintf( pAbc->Err, "\t-v : enable verbose output [default = %s].\n", fVerbose? "yes": "no" ); fprintf( pAbc->Err, "\t-h : print the help massage\n" ); - fprintf( pAbc->Err, "\tfile : the name of the file to write\n" ); + fprintf( pAbc->Err, "\t<file> : the name of the file to write\n" ); return 1; } |