luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Give more reasonable error on read_cex and handle status

This commit is contained in:
Miodrag Milanovic 2022-05-06 15:41:34 +02:00
parent c84323b5a5
commit 6234e18df7
1 changed files with 7 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

9
src/base/io/io.c
View File

@ -686,7 +686,7 @@ int Abc_NtkReadCexFile( char * pFileName, Abc_Ntk_t * pNtk, Abc_Cex_t ** ppCex,
FILE * pFile; FILE * pFile;
Abc_Cex_t * pCex; Abc_Cex_t * pCex;
Vec_Int_t * vNums; Vec_Int_t * vNums;
int c, nRegs = -1, nFrames = -1, Status = 0; int c, nRegs = -1, nFrames = -1;
pFile = fopen( pFileName, "r" ); pFile = fopen( pFileName, "r" );
if ( pFile == NULL ) if ( pFile == NULL )
{ {
@ -804,7 +804,10 @@ int Abc_NtkReadCexFile( char * pFileName, Abc_Ntk_t * pNtk, Abc_Cex_t ** ppCex,
Abc_NtkForEachPo(pNtk, pObj, i ) nPoNtk++; Abc_NtkForEachPo(pNtk, pObj, i ) nPoNtk++;
if ( nRegs < 0 ) if ( nRegs < 0 )
{ {
if (status == 1)
printf( "ERROR: Cannot read register number.\n" ); printf( "ERROR: Cannot read register number.\n" );
else
printf( "Counter-example is not available.\n" );
Vec_IntFree( vNums ); Vec_IntFree( vNums );
return -1; return -1;
} }
@ -866,7 +869,7 @@ int Abc_NtkReadCexFile( char * pFileName, Abc_Ntk_t * pNtk, Abc_Cex_t ** ppCex,
if ( pnFrames ) if ( pnFrames )
*pnFrames = nFrames; *pnFrames = nFrames;
return Status; return status;
} }
/**Function************************************************************* /**Function*************************************************************
@ -927,7 +930,7 @@ int IoCommandReadCex( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_FrameClearVerifStatus( pAbc ); Abc_FrameClearVerifStatus( pAbc );
pAbc->Status = Abc_NtkReadCexFile( pFileName, pNtk, &pAbc->pCex, &pAbc->nFrames, &fOldFormat ); pAbc->Status = Abc_NtkReadCexFile( pFileName, pNtk, &pAbc->pCex, &pAbc->nFrames, &fOldFormat );
if ( fCheck ) { if ( fCheck && pAbc->Status==1) {
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 );
Bmc_CexCareVerify( pAig, pAbc->pCex, pAbc->pCex, false ); Bmc_CexCareVerify( pAig, pAbc->pCex, pAbc->pCex, false );