From 329831bdacfeb6c68bf9782daaa9c2d2bea9ce32 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Tue, 28 Aug 2012 12:12:24 -0700 Subject: Bug fix: abstraction commands not properly updating status when dumping intermediate abstraction. --- src/aig/gia/giaAbsGla.c | 1 + src/aig/gia/giaAbsGla2.c | 1 + src/aig/gia/giaAbsVta.c | 1 + src/base/abci/abcLog.c | 2 +- src/base/main/main.h | 3 +-- src/base/main/mainFrame.c | 1 + 6 files changed, 6 insertions(+), 3 deletions(-) diff --git a/src/aig/gia/giaAbsGla.c b/src/aig/gia/giaAbsGla.c index 508dd218..a3efac14 100644 --- a/src/aig/gia/giaAbsGla.c +++ b/src/aig/gia/giaAbsGla.c @@ -2082,6 +2082,7 @@ int Gia_GlaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars, int fStartVta ) // dump the model into file if ( p->pPars->fDumpVabs ) { + Abc_FrameSetStatus( -1 ); Abc_FrameSetCex( NULL ); Abc_FrameSetNFrames( f+1 ); Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), "write_status gla.status" ); diff --git a/src/aig/gia/giaAbsGla2.c b/src/aig/gia/giaAbsGla2.c index fe8c7e3d..dd349162 100644 --- a/src/aig/gia/giaAbsGla2.c +++ b/src/aig/gia/giaAbsGla2.c @@ -1639,6 +1639,7 @@ int Ga2_ManPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars ) // dump the model into file if ( p->pPars->fDumpVabs || p->pPars->fDumpMabs ) { + Abc_FrameSetStatus( -1 ); Abc_FrameSetCex( NULL ); Abc_FrameSetNFrames( f+1 ); Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), "write_status gla.status" ); diff --git a/src/aig/gia/giaAbsVta.c b/src/aig/gia/giaAbsVta.c index 136455f8..084cb903 100644 --- a/src/aig/gia/giaAbsVta.c +++ b/src/aig/gia/giaAbsVta.c @@ -1683,6 +1683,7 @@ int Gia_VtaPerformInt( Gia_Man_t * pAig, Gia_ParVta_t * pPars ) // dump the model if ( p->pPars->fDumpVabs && (f & 1) ) { + Abc_FrameSetStatus( -1 ); Abc_FrameSetCex( NULL ); Abc_FrameSetNFrames( f+1 ); Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), "write_status vta.status" ); diff --git a/src/base/abci/abcLog.c b/src/base/abci/abcLog.c index 64f5d548..32635a91 100644 --- a/src/base/abci/abcLog.c +++ b/src/base/abci/abcLog.c @@ -90,7 +90,7 @@ void Abc_NtkWriteLogFile( char * pFileName, Abc_Cex_t * pCex, int Status, int nF fprintf( pFile, " " ); // write fprintf( pFile, "%s", pCommand ? pCommand : "unknown" ); - if ( Status == 0 ) + if ( pCex && Status == 0 ) fprintf( pFile, " %d", pCex->iPo ); // write if ( pCex && pCex->iFrame != nFrames ) diff --git a/src/base/main/main.h b/src/base/main/main.h index 620ddac6..849e1956 100644 --- a/src/base/main/main.h +++ b/src/base/main/main.h @@ -129,8 +129,7 @@ extern ABC_DLL void Abc_FrameSetLibVer( void * pLib ); extern ABC_DLL void Abc_FrameSetFlag( char * pFlag, char * pValue ); extern ABC_DLL void Abc_FrameSetCex( Abc_Cex_t * pCex ); extern ABC_DLL void Abc_FrameSetNFrames( int nFrames ); - - +extern ABC_DLL void Abc_FrameSetStatus( int Status ); ABC_NAMESPACE_HEADER_END diff --git a/src/base/main/mainFrame.c b/src/base/main/mainFrame.c index 269a4f8f..d0edf8fc 100644 --- a/src/base/main/mainFrame.c +++ b/src/base/main/mainFrame.c @@ -78,6 +78,7 @@ void Abc_FrameSetLibVer( void * pLib ) { s_GlobalFrame->pL void Abc_FrameSetFlag( char * pFlag, char * pValue ) { Cmd_FlagUpdateValue( s_GlobalFrame, pFlag, pValue ); } void Abc_FrameSetCex( Abc_Cex_t * pCex ) { ABC_FREE( s_GlobalFrame->pCex ); s_GlobalFrame->pCex = pCex; } void Abc_FrameSetNFrames( int nFrames ) { ABC_FREE( s_GlobalFrame->pCex ); s_GlobalFrame->nFrames = nFrames; } +void Abc_FrameSetStatus( int Status ) { ABC_FREE( s_GlobalFrame->pCex ); s_GlobalFrame->Status = Status; } int Abc_FrameIsBatchMode() { return s_GlobalFrame ? s_GlobalFrame->fBatchMode : 0; } -- cgit v1.2.3