diff options
author | Baruch Sterin <baruchs@gmail.com> | 2014-05-12 15:20:17 -0700 |
---|---|---|
committer | Baruch Sterin <baruchs@gmail.com> | 2014-05-12 15:20:17 -0700 |
commit | 26c92f161a95ab3b30991174e79dd99f19b1c86f (patch) | |
tree | bf93eab40203e1ecc9fa26bbe61a86d4738e1a60 /src/base | |
parent | b902b6843c5099f115fcf68f6567969c7233475e (diff) | |
download | abc-26c92f161a95ab3b30991174e79dd99f19b1c86f.tar.gz abc-26c92f161a95ab3b30991174e79dd99f19b1c86f.tar.bz2 abc-26c92f161a95ab3b30991174e79dd99f19b1c86f.zip |
add an option to write_cex to write the CEX in AIGER 1.9 format.
Diffstat (limited to 'src/base')
-rw-r--r-- | src/base/io/io.c | 12 |
1 files changed, 11 insertions, 1 deletions
diff --git a/src/base/io/io.c b/src/base/io/io.c index 4308b243..82b050c3 100644 --- a/src/base/io/io.c +++ b/src/base/io/io.c @@ -2010,11 +2010,12 @@ int IoCommandWriteCex( Abc_Frame_t * pAbc, int argc, char **argv ) int fUseOldMin = 0; int fCheckCex = 0; int forceSeq = 0; + int fAiger = 0; int fPrintFull = 0; int fVerbose = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "snmocfvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "snmocafvh" ) ) != EOF ) { switch ( c ) { @@ -2033,6 +2034,9 @@ int IoCommandWriteCex( Abc_Frame_t * pAbc, int argc, char **argv ) case 'c': fCheckCex ^= 1; break; + case 'a': + fAiger ^= 1; + break; case 'f': fPrintFull ^= 1; break; @@ -2129,8 +2133,13 @@ int IoCommandWriteCex( Abc_Frame_t * pAbc, int argc, char **argv ) { Abc_NtkForEachLatch( pNtk, pObj, i ) fprintf( pFile, "%c", '0'+!Abc_LatchIsInit0(pObj) ); + for ( i = pCex->nRegs; i < pCex->nBits; i++ ) + { + if ( fAiger && (i-pCex->nRegs)%pCex->nPis == 0) + fprintf( pFile, "\n"); fprintf( pFile, "%c", '0'+Abc_InfoHasBit(pCex->pData, i) ); + } } fprintf( pFile, "\n" ); fclose( pFile ); @@ -2172,6 +2181,7 @@ usage: 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-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" ); |