diff options
| author | Claire Xenia Wolf <claire@clairexen.net> | 2022-02-15 16:05:47 +0100 |
|---|---|---|
| committer | Claire Xenia Wolf <claire@clairexen.net> | 2022-02-15 16:05:47 +0100 |
| commit | 1aeff0325e20f2f4109284f328e4f32e2035187e (patch) | |
| tree | d1f014718736f2471b4b22f6fa2e854bac281e47 /src/base | |
| parent | 87a0a718c9c86b0931777914f5185823f5a96131 (diff) | |
| download | abc-1aeff0325e20f2f4109284f328e4f32e2035187e.tar.gz abc-1aeff0325e20f2f4109284f328e4f32e2035187e.tar.bz2 abc-1aeff0325e20f2f4109284f328e4f32e2035187e.zip | |
Enable writing of minimized Cex in non-names mode
Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>
Diffstat (limited to 'src/base')
| -rw-r--r-- | src/base/io/io.c | 10 |
1 files changed, 7 insertions, 3 deletions
diff --git a/src/base/io/io.c b/src/base/io/io.c index f254181a..529c444b 100644 --- a/src/base/io/io.c +++ b/src/base/io/io.c @@ -2449,6 +2449,7 @@ void Abc_NtkDumpOneCex( FILE * pFile, Abc_Ntk_t * pNtk, Abc_Cex_t * pCex, int fPrintFull, int fNames, int fUseFfNames, int fMinimize, int fUseOldMin, int fCexInfo, int fCheckCex, int fUseSatBased, int fHighEffort, int fAiger, int fVerbose ) { + Abc_Cex_t * pCare = NULL; Abc_Obj_t * pObj; int i, f; if ( fPrintFull ) @@ -2464,9 +2465,8 @@ void Abc_NtkDumpOneCex( FILE * pFile, Abc_Ntk_t * pNtk, Abc_Cex_t * pCex, fprintf( pFile, "%s@%d=%c ", Abc_ObjName(pObj), f, '0'+Abc_InfoHasBit(pCexFull->pData, Abc_NtkCiNum(pNtk)*f + i) ); Abc_CexFreeP( &pCexFull ); } - else if ( fNames ) + else if ( fNames || fMinimize ) { - Abc_Cex_t * pCare = NULL; if ( fMinimize ) { extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters ); @@ -2509,6 +2509,8 @@ void Abc_NtkDumpOneCex( FILE * pFile, Abc_Ntk_t * pNtk, Abc_Cex_t * pCex, Aig_ManStop( pAig ); if(pCare == NULL) printf( "Counter-example minimization has failed.\n" ); + if (!fNames) + goto no_names; } else { @@ -2570,6 +2572,7 @@ void Abc_NtkDumpOneCex( FILE * pFile, Abc_Ntk_t * pNtk, Abc_Cex_t * pCex, } else { + no_names: Abc_NtkForEachLatch( pNtk, pObj, i ) fprintf( pFile, "%c", '0'+!Abc_LatchIsInit0(pObj) ); @@ -2577,8 +2580,9 @@ void Abc_NtkDumpOneCex( FILE * pFile, Abc_Ntk_t * pNtk, Abc_Cex_t * pCex, { if ( fAiger && (i-pCex->nRegs)%pCex->nPis == 0) fprintf( pFile, "\n"); - fprintf( pFile, "%c", '0'+Abc_InfoHasBit(pCex->pData, i) ); + fprintf( pFile, "%c", (pCare && !Abc_InfoHasBit(pCare->pData, i)) ? 'x' : '0'+Abc_InfoHasBit(pCex->pData, i) ); } + Abc_CexFreeP( &pCare ); } } |