Commit db7ebfb4 by Claire Xenia Wolf

Cleanups in write_cex output format

Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>
parent 1aeff032
...@@ -2471,8 +2471,11 @@ void Abc_NtkDumpOneCex( FILE * pFile, Abc_Ntk_t * pNtk, Abc_Cex_t * pCex, ...@@ -2471,8 +2471,11 @@ void Abc_NtkDumpOneCex( FILE * pFile, Abc_Ntk_t * pNtk, Abc_Cex_t * pCex,
{ {
extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters ); extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
Aig_Man_t * pAig = Abc_NtkToDar( pNtk, 0, 1 ); Aig_Man_t * pAig = Abc_NtkToDar( pNtk, 0, 1 );
fprintf( pFile, "# FALSIFYING OUTPUTS:"); if ( fNames )
fprintf( pFile, " %s", Abc_ObjName(Abc_NtkCo(pNtk, pCex->iPo)) ); {
fprintf( pFile, "# FALSIFYING OUTPUTS:");
fprintf( pFile, " %s", Abc_ObjName(Abc_NtkCo(pNtk, pCex->iPo)) );
}
if ( fUseOldMin ) if ( fUseOldMin )
{ {
pCare = Saig_ManCbaFindCexCareBits( pAig, pCex, 0, fVerbose ); pCare = Saig_ManCbaFindCexCareBits( pAig, pCex, 0, fVerbose );
...@@ -2582,6 +2585,8 @@ void Abc_NtkDumpOneCex( FILE * pFile, Abc_Ntk_t * pNtk, Abc_Cex_t * pCex, ...@@ -2582,6 +2585,8 @@ void Abc_NtkDumpOneCex( FILE * pFile, Abc_Ntk_t * pNtk, Abc_Cex_t * pCex,
fprintf( pFile, "\n"); fprintf( pFile, "\n");
fprintf( pFile, "%c", (pCare && !Abc_InfoHasBit(pCare->pData, i)) ? 'x' : '0'+Abc_InfoHasBit(pCex->pData, i) ); fprintf( pFile, "%c", (pCare && !Abc_InfoHasBit(pCare->pData, i)) ? 'x' : '0'+Abc_InfoHasBit(pCex->pData, i) );
} }
if ( fAiger )
fprintf( pFile, "\n");
Abc_CexFreeP( &pCare ); Abc_CexFreeP( &pCare );
} }
} }
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment