diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2011-02-17 09:18:07 -0800 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2011-02-17 09:18:07 -0800 |
| commit | 06ae1644b221df44e29b909b7dc4c7557369f5a8 (patch) | |
| tree | 4e93549750f4b65b0fcca3997bdd8833d471d19c | |
| parent | 5b4ef503bd660c1df7e1739d8f1502cb01341904 (diff) | |
| download | abc-06ae1644b221df44e29b909b7dc4c7557369f5a8.tar.gz abc-06ae1644b221df44e29b909b7dc4c7557369f5a8.tar.bz2 abc-06ae1644b221df44e29b909b7dc4c7557369f5a8.zip | |
Fixing the problem with writing/reading bug-free depth in status files.
| -rw-r--r-- | src/base/abci/abcLog.c | 19 |
1 files changed, 13 insertions, 6 deletions
diff --git a/src/base/abci/abcLog.c b/src/base/abci/abcLog.c index 7eece0e3..79947b52 100644 --- a/src/base/abci/abcLog.c +++ b/src/base/abci/abcLog.c @@ -84,13 +84,16 @@ void Abc_NtkWriteLogFile( char * pFileName, Abc_Cex_t * pCex, int Status, int nF else printf( "Abc_NtkWriteLogFile(): Cannot recognize solving status.\n" ); fprintf( pFile, " " ); - // write <cyc> - fprintf( pFile, "%d", pCex ? pCex->iFrame : nFrames ); + // write <bug_free_depth> + fprintf( pFile, "%d", nFrames ); fprintf( pFile, " " ); // write <engine_name> fprintf( pFile, "%s", pCommand ? pCommand : "unknown" ); if ( Status == 0 ) fprintf( pFile, " %d", pCex->iPo ); + // write <cyc> + if ( pCex && pCex->iFrame != nFrames ) + fprintf( pFile, " %d", pCex->iFrame ); fprintf( pFile, "\n" ); // write <INIT_STATE> if ( pCex == NULL ) @@ -131,7 +134,7 @@ int Abc_NtkReadLogFile( char * pFileName, Abc_Cex_t ** ppCex, int * pnFrames ) Abc_Cex_t * pCex; Vec_Int_t * vNums; char Buffer[1000], * pToken; - int c, nRegs = -1, nFrames = -1, iPo = -1, Status = -1; + int c, nRegs = -1, nFrames = -1, iPo = -1, Status = -1, nFrames2 = -1; pFile = fopen( pFileName, "r" ); if ( pFile == NULL ) { @@ -153,6 +156,9 @@ int Abc_NtkReadLogFile( char * pFileName, Abc_Cex_t ** ppCex, int * pnFrames ) pToken = strtok( NULL, " \t\n" ); pToken = strtok( NULL, " \t\n" ); iPo = atoi( pToken ); + pToken = strtok( NULL, " \t\n" ); + if ( pToken ) + nFrames2 = atoi( pToken ); } else if ( !strncmp( Buffer, "snl_UNK", strlen("snl_UNK") ) ) { @@ -182,6 +188,7 @@ int Abc_NtkReadLogFile( char * pFileName, Abc_Cex_t ** ppCex, int * pnFrames ) fclose( pFile ); if ( Vec_IntSize(vNums) ) { + int iFrameCex = (nFrames2 == -1) ? nFrames : nFrames2; if ( nRegs == 0 ) { printf( "Cannot read register number.\n" ); @@ -192,14 +199,14 @@ int Abc_NtkReadLogFile( char * pFileName, Abc_Cex_t ** ppCex, int * pnFrames ) printf( "Cannot read counter example.\n" ); return -1; } - if ( (Vec_IntSize(vNums)-nRegs) % nFrames != 0 ) + if ( (Vec_IntSize(vNums)-nRegs) % (iFrameCex + 1) != 0 ) { printf( "Incorrect number of bits.\n" ); return -1; } - pCex = Abc_CexAlloc( nRegs, (Vec_IntSize(vNums)-nRegs)/nFrames, nFrames ); + pCex = Abc_CexAlloc( nRegs, (Vec_IntSize(vNums)-nRegs)/(iFrameCex + 1), iFrameCex + 1 ); pCex->iPo = iPo; - pCex->iFrame = nFrames - 1; + pCex->iFrame = iFrameCex; assert( Vec_IntSize(vNums) == pCex->nBits ); for ( c = 0; c < pCex->nBits; c++ ) if ( Vec_IntEntry(vNums, c) ) |