diff options
Diffstat (limited to 'src/base/main')
| -rw-r--r-- | src/base/main/main.h | 3 | ||||
| -rw-r--r-- | src/base/main/mainFrame.c | 27 | ||||
| -rw-r--r-- | src/base/main/mainInt.h | 9 |
3 files changed, 22 insertions, 17 deletions
diff --git a/src/base/main/main.h b/src/base/main/main.h index 33f8a110..ac30f358 100644 --- a/src/base/main/main.h +++ b/src/base/main/main.h @@ -108,7 +108,8 @@ extern ABC_DLL int Abc_FrameIsFlagEnabled( char * pFlag ); extern ABC_DLL int Abc_FrameReadBmcFrames( Abc_Frame_t * p ); extern ABC_DLL int Abc_FrameReadProbStatus( Abc_Frame_t * p ); extern ABC_DLL Abc_Cex_t * Abc_FrameReadCex( Abc_Frame_t * p ); -extern ABC_DLL Vec_Ptr_t * Abc_FrameReadCexVec( Abc_Frame_t * p ); +extern ABC_DLL Vec_Ptr_t * Abc_FrameReadCexVec( Abc_Frame_t * p ); +extern ABC_DLL Vec_Ptr_t * Abc_FrameReadPoEquivs( Abc_Frame_t * p ); extern ABC_DLL int Abc_FrameReadCexPiNum( Abc_Frame_t * p ); extern ABC_DLL int Abc_FrameReadCexRegNum( Abc_Frame_t * p ); diff --git a/src/base/main/mainFrame.c b/src/base/main/mainFrame.c index d03acf28..6a63cdd6 100644 --- a/src/base/main/mainFrame.c +++ b/src/base/main/mainFrame.c @@ -63,11 +63,12 @@ int Abc_FrameReadBmcFrames( Abc_Frame_t * p ) { return s_GlobalFr int Abc_FrameReadProbStatus( Abc_Frame_t * p ) { return s_GlobalFrame->Status; } Abc_Cex_t * Abc_FrameReadCex( Abc_Frame_t * p ) { return s_GlobalFrame->pCex; } Vec_Ptr_t * Abc_FrameReadCexVec( Abc_Frame_t * p ) { return s_GlobalFrame->vCexVec; } +Vec_Ptr_t * Abc_FrameReadPoEquivs( Abc_Frame_t * p ) { return s_GlobalFrame->vPoEquivs; } -int Abc_FrameReadCexPiNum( Abc_Frame_t * p ) { return s_GlobalFrame->pCex->nPis; } -int Abc_FrameReadCexRegNum( Abc_Frame_t * p ) { return s_GlobalFrame->pCex->nRegs; } -int Abc_FrameReadCexPo( Abc_Frame_t * p ) { return s_GlobalFrame->pCex->iPo; } -int Abc_FrameReadCexFrame( Abc_Frame_t * p ) { return s_GlobalFrame->pCex->iFrame; } +int Abc_FrameReadCexPiNum( Abc_Frame_t * p ) { return s_GlobalFrame->pCex->nPis; } +int Abc_FrameReadCexRegNum( Abc_Frame_t * p ) { return s_GlobalFrame->pCex->nRegs; } +int Abc_FrameReadCexPo( Abc_Frame_t * p ) { return s_GlobalFrame->pCex->iPo; } +int Abc_FrameReadCexFrame( Abc_Frame_t * p ) { return s_GlobalFrame->pCex->iFrame; } void Abc_FrameSetLibLut( void * pLib ) { s_GlobalFrame->pLibLut = pLib; } void Abc_FrameSetLibGen( void * pLib ) { s_GlobalFrame->pLibGen = pLib; } @@ -162,14 +163,16 @@ void Abc_FrameDeallocate( Abc_Frame_t * p ) // undefine_cube_size(); Rwt_ManGlobalStop(); // Ivy_TruthManStop(); - if ( p->pLibVer ) Abc_LibFree( (Abc_Lib_t *)p->pLibVer, NULL ); - if ( p->pManDec ) Dec_ManStop( (Dec_Man_t *)p->pManDec ); - if ( p->dd ) Extra_StopManager( p->dd ); - if ( p->vStore ) Vec_PtrFree( p->vStore ); - if ( p->pSave1 ) Aig_ManStop( (Aig_Man_t *)p->pSave1 ); - if ( p->pSave2 ) Aig_ManStop( (Aig_Man_t *)p->pSave2 ); - if ( p->pSave3 ) Aig_ManStop( (Aig_Man_t *)p->pSave3 ); - if ( p->pSave4 ) Aig_ManStop( (Aig_Man_t *)p->pSave4 ); + if ( p->vCexVec ) Vec_PtrFreeFree( p->vCexVec ); + if ( p->vPoEquivs ) Vec_VecFree( (Vec_Vec_t *)p->vPoEquivs ); + if ( p->pLibVer ) Abc_LibFree( (Abc_Lib_t *)p->pLibVer, NULL ); + if ( p->pManDec ) Dec_ManStop( (Dec_Man_t *)p->pManDec ); + if ( p->dd ) Extra_StopManager( p->dd ); + if ( p->vStore ) Vec_PtrFree( p->vStore ); + if ( p->pSave1 ) Aig_ManStop( (Aig_Man_t *)p->pSave1 ); + if ( p->pSave2 ) Aig_ManStop( (Aig_Man_t *)p->pSave2 ); + if ( p->pSave3 ) Aig_ManStop( (Aig_Man_t *)p->pSave3 ); + if ( p->pSave4 ) Aig_ManStop( (Aig_Man_t *)p->pSave4 ); if ( p->vPlugInComBinPairs ) { char * pTemp; diff --git a/src/base/main/mainInt.h b/src/base/main/mainInt.h index 979d376c..2eca004e 100644 --- a/src/base/main/mainInt.h +++ b/src/base/main/mainInt.h @@ -90,10 +90,11 @@ struct Abc_Frame_t_ void * pLibVer; // the current Verilog library // new code - Gia_Man_t * pGia; - Gia_Man_t * pGia2; - Abc_Cex_t * pCex; - Vec_Ptr_t * vCexVec; + Gia_Man_t * pGia; // alternative current network as a light-weight AIG + Gia_Man_t * pGia2; // copy of the above + Abc_Cex_t * pCex; // a counter-example to fail the current network + Vec_Ptr_t * vCexVec; // a vector of counter-examples if more than one PO fails + Vec_Ptr_t * vPoEquivs; // equivalence classes of isomorphic primary outputs void * pSave1; void * pSave2; |