diff options
Diffstat (limited to 'src/base')
-rw-r--r-- | src/base/abci/abc.c | 26 | ||||
-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 |
4 files changed, 47 insertions, 18 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 16c9ffe7..c77a4f2b 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -422,6 +422,26 @@ void Abc_FrameReplaceCexVec( Abc_Frame_t * pAbc, Vec_Ptr_t ** pvCexVec ) SeeAlso [] ***********************************************************************/ +void Abc_FrameReplacePoEquivs( Abc_Frame_t * pAbc, Vec_Ptr_t ** pvPoEquivs ) +{ + // update the array vector + if ( pAbc->vPoEquivs ) + Vec_VecFree( (Vec_Vec_t *)pAbc->vPoEquivs ); + pAbc->vPoEquivs = *pvPoEquivs; + *pvPoEquivs = NULL; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ void Abc_FrameClearDesign() { } @@ -21335,6 +21355,7 @@ int Abc_CommandIso( Abc_Frame_t * pAbc, int argc, char ** argv ) extern Abc_Ntk_t * Abc_NtkFromAigPhase( Aig_Man_t * pMan ); Abc_Ntk_t * pNtk, * pNtkNew = NULL; Aig_Man_t * pAig, * pTemp; + Vec_Ptr_t * vPosEquivs = NULL; int c, fVerbose = 0; Extra_UtilGetoptReset(); while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF ) @@ -21372,11 +21393,14 @@ int Abc_CommandIso( Abc_Frame_t * pAbc, int argc, char ** argv ) // transform pAig = Abc_NtkToDar( pNtk, 0, 1 ); - pTemp = Saig_ManIsoReduce( pAig, fVerbose ); + pTemp = Saig_ManIsoReduce( pAig, &vPosEquivs, fVerbose ); pNtkNew = Abc_NtkFromAigPhase( pTemp ); Aig_ManStop( pTemp ); Aig_ManStop( pAig ); + // update the internal storage of PO equivalences + Abc_FrameReplacePoEquivs( pAbc, &vPosEquivs ); + // replace the current network Abc_FrameReplaceCurrentNetwork( pAbc, pNtkNew ); return 0; 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; |