From ee9f66e2c4dba55e5ab4c7ce16223054b291d5fb Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Fri, 17 Feb 2012 13:19:09 -0800 Subject: Isomorphism checking code. --- src/aig/saig/saig.h | 2 +- src/aig/saig/saigIso.c | 21 ++++++++++++++------- src/base/abci/abc.c | 26 +++++++++++++++++++++++++- src/base/main/main.h | 3 ++- src/base/main/mainFrame.c | 27 +++++++++++++++------------ src/base/main/mainInt.h | 9 +++++---- src/misc/vec/vecVec.h | 12 +++++++----- 7 files changed, 69 insertions(+), 31 deletions(-) diff --git a/src/aig/saig/saig.h b/src/aig/saig/saig.h index 218cb31c..8fde2ef6 100644 --- a/src/aig/saig/saig.h +++ b/src/aig/saig/saig.h @@ -185,7 +185,7 @@ extern Aig_Man_t * Saig_ManReadBlif( char * pFileName ); /*=== saigIso.c ==========================================================*/ extern Vec_Int_t * Saig_ManFindIsoPerm( Aig_Man_t * pAig, int fVerbose ); extern Aig_Man_t * Saig_ManDupIsoCanonical( Aig_Man_t * pAig, int fVerbose ); -extern Aig_Man_t * Saig_ManIsoReduce( Aig_Man_t * pAig, int fVerbose ); +extern Aig_Man_t * Saig_ManIsoReduce( Aig_Man_t * pAig, Vec_Ptr_t ** pvPosEquivs, int fVerbose ); /*=== saigIsoFast.c ==========================================================*/ extern Vec_Vec_t * Saig_IsoDetectFast( Aig_Man_t * pAig ); /*=== saigMiter.c ==========================================================*/ diff --git a/src/aig/saig/saigIso.c b/src/aig/saig/saigIso.c index 0e7c9de1..ff10df82 100644 --- a/src/aig/saig/saigIso.c +++ b/src/aig/saig/saigIso.c @@ -362,8 +362,8 @@ Aig_Man_t * Iso_ManFilterPos_old( Aig_Man_t * pAig, int fVerbose ) { if ( fVeryVerbose ) printf( "Found match\n" ); - if ( fVerbose ) - printf( "Found match for AIG %4d and AIG %4d.\n", Vec_IntEntry(vPos,k), i ); +// if ( fVerbose ) +// printf( "Found match for AIG %4d and AIG %4d.\n", Vec_IntEntry(vPos,k), i ); Vec_IntFree( vMap ); break; } @@ -419,7 +419,7 @@ int Iso_StoCompareVecStr( Vec_Str_t ** p1, Vec_Str_t ** p2 ) SeeAlso [] ***********************************************************************/ -Aig_Man_t * Iso_ManFilterPos( Aig_Man_t * pAig, int fVerbose ) +Aig_Man_t * Iso_ManFilterPos( Aig_Man_t * pAig, Vec_Ptr_t ** pvPosEquivs, int fVerbose ) { // int fVeryVerbose = 0; Aig_Man_t * pPart, * pTemp; @@ -492,6 +492,7 @@ Aig_Man_t * Iso_ManFilterPos( Aig_Man_t * pAig, int fVerbose ) // report the results // Vec_VecPrintInt( (Vec_Vec_t *)vClasses ); // printf( "Devided %d outputs into %d cand equiv classes.\n", Saig_ManPoNum(pAig), Vec_PtrSize(vClasses) ); +/* if ( fVerbose ) { Vec_PtrForEachEntry( Vec_Int_t *, vClasses, vLevel, i ) @@ -501,7 +502,7 @@ Aig_Man_t * Iso_ManFilterPos( Aig_Man_t * pAig, int fVerbose ) nUnique++; printf( " Unique = %d\n", nUnique ); } - +*/ // collect the first ones vRemain = Vec_IntAlloc( 100 ); Vec_PtrForEachEntry( Vec_Int_t *, vClasses, vLevel, i ) @@ -512,7 +513,13 @@ Aig_Man_t * Iso_ManFilterPos( Aig_Man_t * pAig, int fVerbose ) Vec_IntFree( vRemain ); // return (Vec_Vec_t *)vClasses; - Vec_VecFree( (Vec_Vec_t *)vClasses ); +// Vec_VecFree( (Vec_Vec_t *)vClasses ); + *pvPosEquivs = vClasses; + if ( fVerbose && vClasses ) + { + printf( "Non-trivial equivalence clases of primary outputs:\n" ); + Vec_VecPrintInt( (Vec_Vec_t *)vClasses, 1 ); + } // printf( "The number of all checks %d. Complex checks %d.\n", nPos*(nPos-1)/2, s_Counter ); return pPart; @@ -550,11 +557,11 @@ Aig_Man_t * Iso_ManTest( Aig_Man_t * pAig, int fVerbose ) SeeAlso [] ***********************************************************************/ -Aig_Man_t * Saig_ManIsoReduce( Aig_Man_t * pAig, int fVerbose ) +Aig_Man_t * Saig_ManIsoReduce( Aig_Man_t * pAig, Vec_Ptr_t ** pvPosEquivs, int fVerbose ) { Aig_Man_t * pPart; int clk = clock(); - pPart = Iso_ManFilterPos( pAig, fVerbose ); + pPart = Iso_ManFilterPos( pAig, pvPosEquivs, fVerbose ); printf( "Reduced %d outputs to %d outputs. ", Saig_ManPoNum(pAig), Saig_ManPoNum(pPart) ); Abc_PrintTime( 1, "Time", clock() - clk ); // Aig_ManStop( pPart ); 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 @@ -411,6 +411,26 @@ void Abc_FrameReplaceCexVec( Abc_Frame_t * pAbc, Vec_Ptr_t ** pvCexVec ) ABC_FREE( pAbc->pCex ); } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + 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 [] @@ -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; diff --git a/src/misc/vec/vecVec.h b/src/misc/vec/vecVec.h index f72bd93c..e0f18983 100644 --- a/src/misc/vec/vecVec.h +++ b/src/misc/vec/vecVec.h @@ -597,17 +597,19 @@ static inline void Vec_VecSort( Vec_Vec_t * p, int fReverse ) SeeAlso [] ***********************************************************************/ -static inline void Vec_VecPrintInt( Vec_Vec_t * p ) +static inline void Vec_VecPrintInt( Vec_Vec_t * p, int fSkipSingles ) { int i, k, Entry; - printf( "Integers by level" ); Vec_VecForEachEntryInt( p, Entry, i, k ) { + if ( Vec_VecLevelSize(p, i) == 1 ) + break; if ( k == 0 ) - printf( "\n%3d : ", i ); - printf( "%6d ", Entry ); + printf( " %4d : {", i ); + printf( " %d", Entry ); + if ( k == Vec_VecLevelSize(p, i) - 1 ) + printf( " }\n" ); } - printf( "\n" ); } -- cgit v1.2.3