diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2013-01-25 05:59:56 +0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2013-01-25 05:59:56 +0700 |
| commit | aa9c87cf8d9d3e729ef5ab263c34d531a8f73d07 (patch) | |
| tree | 6eeb0d01ac0b6c3fe4abe1b9433dca3c11c8da25 /src/base/abci/abcLog.c | |
| parent | 4bd54729d799513d8c21333446706d387aac7192 (diff) | |
| download | abc-aa9c87cf8d9d3e729ef5ab263c34d531a8f73d07.tar.gz abc-aa9c87cf8d9d3e729ef5ab263c34d531a8f73d07.tar.bz2 abc-aa9c87cf8d9d3e729ef5ab263c34d531a8f73d07.zip | |
Extending verification status file format to allow for SAT status without CEX.
Diffstat (limited to 'src/base/abci/abcLog.c')
| -rw-r--r-- | src/base/abci/abcLog.c | 19 |
1 files changed, 15 insertions, 4 deletions
diff --git a/src/base/abci/abcLog.c b/src/base/abci/abcLog.c index 32635a91..b583aa02 100644 --- a/src/base/abci/abcLog.c +++ b/src/base/abci/abcLog.c @@ -156,10 +156,16 @@ int Abc_NtkReadLogFile( char * pFileName, Abc_Cex_t ** ppCex, int * pnFrames ) nFrames = atoi( pToken ); pToken = strtok( NULL, " \t\n" ); pToken = strtok( NULL, " \t\n" ); - iPo = atoi( pToken ); - pToken = strtok( NULL, " \t\n" ); - if ( pToken ) - nFrames2 = atoi( pToken ); + if ( pToken != NULL ) + { + iPo = atoi( pToken ); + pToken = strtok( NULL, " \t\n" ); + if ( pToken ) + nFrames2 = atoi( pToken ); + } + else + printf( "Warning! The current status is SAT but the current CEX is not given.\n" ); + } else if ( !strncmp( Buffer, "snl_UNK", strlen("snl_UNK") ) ) { @@ -193,16 +199,19 @@ int Abc_NtkReadLogFile( char * pFileName, Abc_Cex_t ** ppCex, int * pnFrames ) if ( nRegs < 0 ) { printf( "Cannot read register number.\n" ); + Vec_IntFree( vNums ); return -1; } if ( Vec_IntSize(vNums)-nRegs == 0 ) { printf( "Cannot read counter example.\n" ); + Vec_IntFree( vNums ); return -1; } if ( (Vec_IntSize(vNums)-nRegs) % (iFrameCex + 1) != 0 ) { printf( "Incorrect number of bits.\n" ); + Vec_IntFree( vNums ); return -1; } pCex = Abc_CexAlloc( nRegs, (Vec_IntSize(vNums)-nRegs)/(iFrameCex + 1), iFrameCex + 1 ); @@ -218,6 +227,8 @@ int Abc_NtkReadLogFile( char * pFileName, Abc_Cex_t ** ppCex, int * pnFrames ) else ABC_FREE( pCex ); } + else + Vec_IntFree( vNums ); if ( pnFrames ) *pnFrames = nFrames; return Status; |