From c5067f7d04dc4c8ee919d9597a4a94a5c4ac3552 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sat, 11 Feb 2012 00:22:05 -0800 Subject: Graph isomorphism checking code. --- src/aig/saig/module.make | 3 + src/aig/saig/saig.h | 6 + src/aig/saig/saigIso.c | 597 ++++++++++++++++++++++++++++++++++ src/aig/saig/saigIsoFast.c | 352 ++++++++++++++++++++ src/aig/saig/saigIsoSlow.c | 775 +++++++++++++++++++++++++++++++++++++++++++++ 5 files changed, 1733 insertions(+) create mode 100644 src/aig/saig/saigIso.c create mode 100644 src/aig/saig/saigIsoFast.c create mode 100644 src/aig/saig/saigIsoSlow.c (limited to 'src/aig/saig') diff --git a/src/aig/saig/module.make b/src/aig/saig/module.make index 327b9dd5..42e3c090 100644 --- a/src/aig/saig/module.make +++ b/src/aig/saig/module.make @@ -18,6 +18,9 @@ SRC += src/aig/saig/saigAbs.c \ src/aig/saig/saigHaig.c \ src/aig/saig/saigInd.c \ src/aig/saig/saigIoa.c \ + src/aig/saig/saigIso.c \ + src/aig/saig/saigIsoFast.c \ + src/aig/saig/saigIsoSlow.c \ src/aig/saig/saigMiter.c \ src/aig/saig/saigOutDec.c \ src/aig/saig/saigPhase.c \ diff --git a/src/aig/saig/saig.h b/src/aig/saig/saig.h index 74566966..218cb31c 100644 --- a/src/aig/saig/saig.h +++ b/src/aig/saig/saig.h @@ -182,6 +182,12 @@ extern int Saig_ManInduction( Aig_Man_t * p, int nFramesMax, int n /*=== saigIoa.c ==========================================================*/ extern void Saig_ManDumpBlif( Aig_Man_t * p, char * pFileName ); 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 ); +/*=== saigIsoFast.c ==========================================================*/ +extern Vec_Vec_t * Saig_IsoDetectFast( Aig_Man_t * pAig ); /*=== saigMiter.c ==========================================================*/ extern Sec_MtrStatus_t Sec_MiterStatus( Aig_Man_t * p ); extern Aig_Man_t * Saig_ManCreateMiter( Aig_Man_t * p1, Aig_Man_t * p2, int Oper ); diff --git a/src/aig/saig/saigIso.c b/src/aig/saig/saigIso.c new file mode 100644 index 00000000..1001f153 --- /dev/null +++ b/src/aig/saig/saigIso.c @@ -0,0 +1,597 @@ +/**CFile**************************************************************** + + FileName [saigIso.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Sequential AIG package.] + + Synopsis [Sequential cleanup.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: saigIso.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "src/aig/ioa/ioa.h" +#include "saig.h" + +ABC_NAMESPACE_IMPL_START + + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Find the canonical permutation of the COs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Saig_ManFindIsoPermCos( Aig_Man_t * pAig, Vec_Int_t * vPermCis ) +{ + extern int Iso_ObjCompareAigObjByData( Aig_Obj_t ** pp1, Aig_Obj_t ** pp2 ); + Vec_Int_t * vPermCos; + Aig_Obj_t * pObj, * pFanin; + int i, Entry, Diff; + assert( Vec_IntSize(vPermCis) == Aig_ManPiNum(pAig) ); + vPermCos = Vec_IntAlloc( Aig_ManPoNum(pAig) ); + if ( Saig_ManPoNum(pAig) == 1 ) + Vec_IntPush( vPermCos, 0 ); + else + { + Vec_Ptr_t * vRoots = Vec_PtrAlloc( Saig_ManPoNum(pAig) ); + Saig_ManForEachPo( pAig, pObj, i ) + { + pFanin = Aig_ObjFanin0(pObj); + assert( Aig_ObjIsConst1(pFanin) || pFanin->iData > 0 ); + pObj->iData = Abc_Var2Lit( pFanin->iData, Aig_ObjFaninC0(pObj) ); + Vec_PtrPush( vRoots, pObj ); + } + Vec_PtrSort( vRoots, (int (*)(void))Iso_ObjCompareAigObjByData ); + Vec_PtrForEachEntry( Aig_Obj_t *, vRoots, pObj, i ) + Vec_IntPush( vPermCos, Aig_ObjPioNum(pObj) ); + Vec_PtrFree( vRoots ); + } + // add flop outputs + Diff = Saig_ManPoNum(pAig) - Saig_ManPiNum(pAig); + Vec_IntForEachEntryStart( vPermCis, Entry, i, Saig_ManPiNum(pAig) ) + Vec_IntPush( vPermCos, Entry + Diff ); + return vPermCos; +} + +/**Function************************************************************* + + Synopsis [Performs canonical duplication of the AIG.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Saig_ManDupIsoCanonical_rec( Aig_Man_t * pNew, Aig_Man_t * pAig, Aig_Obj_t * pObj ) +{ + if ( Aig_ObjIsTravIdCurrent(pAig, pObj) ) + return; + Aig_ObjSetTravIdCurrent(pAig, pObj); + assert( Aig_ObjIsNode(pObj) ); + if ( !Aig_ObjIsNode(Aig_ObjFanin0(pObj)) || !Aig_ObjIsNode(Aig_ObjFanin1(pObj)) ) + { + Saig_ManDupIsoCanonical_rec( pNew, pAig, Aig_ObjFanin0(pObj) ); + Saig_ManDupIsoCanonical_rec( pNew, pAig, Aig_ObjFanin1(pObj) ); + } + else + { + assert( Aig_ObjFanin0(pObj)->iData != Aig_ObjFanin1(pObj)->iData ); + if ( Aig_ObjFanin0(pObj)->iData < Aig_ObjFanin1(pObj)->iData ) + { + Saig_ManDupIsoCanonical_rec( pNew, pAig, Aig_ObjFanin0(pObj) ); + Saig_ManDupIsoCanonical_rec( pNew, pAig, Aig_ObjFanin1(pObj) ); + } + else + { + Saig_ManDupIsoCanonical_rec( pNew, pAig, Aig_ObjFanin1(pObj) ); + Saig_ManDupIsoCanonical_rec( pNew, pAig, Aig_ObjFanin0(pObj) ); + } + } + pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); +} + +/**Function************************************************************* + + Synopsis [Performs canonical duplication of the AIG.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Saig_ManDupIsoCanonical( Aig_Man_t * pAig, int fVerbose ) +{ + Aig_Man_t * pNew; + Aig_Obj_t * pObj; + Vec_Int_t * vPerm, * vPermCo; + int i, Entry; + // derive permutations + vPerm = Saig_ManFindIsoPerm( pAig, fVerbose ); + vPermCo = Saig_ManFindIsoPermCos( pAig, vPerm ); + // create the new manager + pNew = Aig_ManStart( Aig_ManNodeNum(pAig) ); + pNew->pName = Abc_UtilStrsav( pAig->pName ); + Aig_ManIncrementTravId( pAig ); + // create constant + pObj = Aig_ManConst1(pAig); + pObj->pData = Aig_ManConst1(pNew); + Aig_ObjSetTravIdCurrent( pAig, pObj ); + // create PIs + Vec_IntForEachEntry( vPerm, Entry, i ) + { + pObj = Aig_ManPi(pAig, Entry); + pObj->pData = Aig_ObjCreatePi(pNew); + Aig_ObjSetTravIdCurrent( pAig, pObj ); + } + // traverse from the POs + Vec_IntForEachEntry( vPermCo, Entry, i ) + { + pObj = Aig_ManPo(pAig, Entry); + Saig_ManDupIsoCanonical_rec( pNew, pAig, Aig_ObjFanin0(pObj) ); + } + // create POs + Vec_IntForEachEntry( vPermCo, Entry, i ) + { + pObj = Aig_ManPo(pAig, Entry); + Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) ); + } + Aig_ManSetRegNum( pNew, Aig_ManRegNum(pAig) ); + Vec_IntFreeP( &vPerm ); + Vec_IntFreeP( &vPermCo ); + return pNew; +} + + + + + +/**Function************************************************************* + + Synopsis [Checks structural equivalence of AIG1 and AIG2.] + + Description [Returns 1 if AIG1 and AIG2 are structurally equivalent + under this mapping.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Iso_ManCheckMapping( Aig_Man_t * pAig1, Aig_Man_t * pAig2, Vec_Int_t * vMap2to1, int fVerbose ) +{ + Aig_Obj_t * pObj, * pFanin0, * pFanin1; + int i; + assert( Aig_ManPiNum(pAig1) == Aig_ManPiNum(pAig2) ); + assert( Aig_ManPoNum(pAig1) == Aig_ManPoNum(pAig2) ); + assert( Aig_ManRegNum(pAig1) == Aig_ManRegNum(pAig2) ); + assert( Aig_ManNodeNum(pAig1) == Aig_ManNodeNum(pAig2) ); + Aig_ManCleanData( pAig1 ); + // map const and PI nodes + Aig_ManConst1(pAig2)->pData = Aig_ManConst1(pAig1); + Aig_ManForEachPi( pAig2, pObj, i ) + pObj->pData = Aig_ManPi( pAig1, Vec_IntEntry(vMap2to1, i) ); + // try internal nodes + Aig_ManForEachNode( pAig2, pObj, i ) + { + pFanin0 = Aig_ObjChild0Copy( pObj ); + pFanin1 = Aig_ObjChild1Copy( pObj ); + pObj->pData = Aig_TableLookupTwo( pAig1, pFanin0, pFanin1 ); + if ( pObj->pData == NULL ) + { + if ( fVerbose ) + printf( "Structural equivalence failed at node %d.\n", i ); + return 0; + } + } + // make sure the first PO points to the same node + if ( Aig_ManPoNum(pAig1)-Aig_ManRegNum(pAig1) == 1 && Aig_ObjChild0Copy(Aig_ManPo(pAig2, 0)) != Aig_ObjChild0(Aig_ManPo(pAig1, 0)) ) + { + if ( fVerbose ) + printf( "Structural equivalence failed at primary output 0.\n" ); + return 0; + } + return 1; +} + +//static int s_Counter; + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Iso_ManNegEdgeNum( Aig_Man_t * pAig ) +{ + Aig_Obj_t * pObj; + int i, Counter = 0; + if ( pAig->nComplEdges > 0 ) + return pAig->nComplEdges; + Aig_ManForEachObj( pAig, pObj, i ) + if ( Aig_ObjIsNode(pObj) ) + { + Counter += Aig_ObjFaninC0(pObj); + Counter += Aig_ObjFaninC1(pObj); + } + else if ( Aig_ObjIsPo(pObj) ) + Counter += Aig_ObjFaninC0(pObj); + return (pAig->nComplEdges = Counter); +} + +/**Function************************************************************* + + Synopsis [Finds mapping of CIs of AIG2 into those of AIG1.] + + Description [Returns the mapping of CIs of the two AIGs, or NULL + if there is no mapping.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Iso_ManFindMapping( Aig_Man_t * pAig1, Aig_Man_t * pAig2, Vec_Int_t * vPerm1_, Vec_Int_t * vPerm2_, int fVerbose ) +{ + Vec_Int_t * vPerm1, * vPerm2, * vInvPerm2; + int i, Entry; + if ( Aig_ManPiNum(pAig1) != Aig_ManPiNum(pAig2) ) + return NULL; + if ( Aig_ManPoNum(pAig1) != Aig_ManPoNum(pAig2) ) + return NULL; + if ( Aig_ManRegNum(pAig1) != Aig_ManRegNum(pAig2) ) + return NULL; + if ( Aig_ManNodeNum(pAig1) != Aig_ManNodeNum(pAig2) ) + return NULL; + if ( Aig_ManLevelNum(pAig1) != Aig_ManLevelNum(pAig2) ) + return NULL; +// if ( Iso_ManNegEdgeNum(pAig1) != Iso_ManNegEdgeNum(pAig2) ) +// return NULL; +// s_Counter++; + + if ( fVerbose ) + printf( "AIG1:\n" ); + vPerm1 = vPerm1_ ? vPerm1_ : Saig_ManFindIsoPerm( pAig1, fVerbose ); + if ( fVerbose ) + printf( "AIG1:\n" ); + vPerm2 = vPerm2_ ? vPerm2_ : Saig_ManFindIsoPerm( pAig2, fVerbose ); + if ( vPerm1_ ) + assert( Vec_IntSize(vPerm1_) == Aig_ManPiNum(pAig1) ); + if ( vPerm2_ ) + assert( Vec_IntSize(vPerm2_) == Aig_ManPiNum(pAig2) ); + // find canonical permutation + // vPerm1/vPerm2 give canonical order of CIs of AIG1/AIG2 + vInvPerm2 = Vec_IntInvert( vPerm2, -1 ); + Vec_IntForEachEntry( vInvPerm2, Entry, i ) + { + assert( Entry >= 0 && Entry < Aig_ManPiNum(pAig1) ); + Vec_IntWriteEntry( vInvPerm2, i, Vec_IntEntry(vPerm1, Entry) ); + } + if ( vPerm1_ == NULL ) + Vec_IntFree( vPerm1 ); + if ( vPerm2_ == NULL ) + Vec_IntFree( vPerm2 ); + // check if they are indeed equivalent + if ( !Iso_ManCheckMapping( pAig1, pAig2, vInvPerm2, fVerbose ) ) + Vec_IntFreeP( &vInvPerm2 ); + return vInvPerm2; +} + + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Iso_ManFilterPos_old( Aig_Man_t * pAig, int fVerbose ) +{ + int fVeryVerbose = 0; + Vec_Ptr_t * vParts, * vPerms, * vAigs; + Vec_Int_t * vPos, * vMap; + Aig_Man_t * pPart, * pTemp; + int i, k, nPos; + + // derive AIG for each PO + nPos = Aig_ManPoNum(pAig) - Aig_ManRegNum(pAig); + vParts = Vec_PtrAlloc( nPos ); + vPerms = Vec_PtrAlloc( nPos ); + for ( i = 0; i < nPos; i++ ) + { + pPart = Saig_ManDupCones( pAig, &i, 1 ); + vMap = Saig_ManFindIsoPerm( pPart, fVeryVerbose ); + Vec_PtrPush( vParts, pPart ); + Vec_PtrPush( vPerms, vMap ); + } +// s_Counter = 0; + + // check AIGs for each PO + vAigs = Vec_PtrAlloc( 1000 ); + vPos = Vec_IntAlloc( 1000 ); + Vec_PtrForEachEntry( Aig_Man_t *, vParts, pPart, i ) + { + if ( fVeryVerbose ) + { + printf( "AIG %4d : ", i ); + Aig_ManPrintStats( pPart ); + } + Vec_PtrForEachEntry( Aig_Man_t *, vAigs, pTemp, k ) + { + if ( fVeryVerbose ) + printf( "Comparing AIG %4d and AIG %4d. ", Vec_IntEntry(vPos,k), i ); + vMap = Iso_ManFindMapping( pTemp, pPart, + (Vec_Int_t *)Vec_PtrEntry(vPerms, Vec_IntEntry(vPos,k)), + (Vec_Int_t *)Vec_PtrEntry(vPerms, i), + fVeryVerbose ); + if ( vMap != NULL ) + { + if ( fVeryVerbose ) + printf( "Found match\n" ); + if ( fVerbose ) + printf( "Found match for AIG %4d and AIG %4d.\n", Vec_IntEntry(vPos,k), i ); + Vec_IntFree( vMap ); + break; + } + if ( fVeryVerbose ) + printf( "No match.\n" ); + } + if ( k == Vec_PtrSize(vAigs) ) + { + Vec_PtrPush( vAigs, pPart ); + Vec_IntPush( vPos, i ); + } + } + // delete AIGs + Vec_PtrForEachEntry( Aig_Man_t *, vParts, pPart, i ) + Aig_ManStop( pPart ); + Vec_PtrFree( vParts ); + Vec_PtrForEachEntry( Vec_Int_t *, vPerms, vMap, i ) + Vec_IntFree( vMap ); + Vec_PtrFree( vPerms ); + // derive the resulting AIG + pPart = Saig_ManDupCones( pAig, Vec_IntArray(vPos), Vec_IntSize(vPos) ); + Vec_PtrFree( vAigs ); + Vec_IntFree( vPos ); + +// printf( "The number of all checks %d. Complex checks %d.\n", nPos*(nPos-1)/2, s_Counter ); + return pPart; +} + +/**Function************************************************************* + + Synopsis [Takes multi-output sequential AIG.] + + Description [Returns candidate equivalence classes of POs.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Iso_StoCompareVecStr( Vec_Str_t ** p1, Vec_Str_t ** p2 ) +{ + return Vec_StrCompareVec( *p1, *p2 ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Iso_ManFilterPos( Aig_Man_t * pAig, int fVerbose ) +{ + int fVeryVerbose = 0; + Aig_Man_t * pPart, * pTemp; + Vec_Ptr_t * vBuffers, * vClasses; + Vec_Int_t * vLevel, * vRemain; + Vec_Str_t * vStr, * vPrev; + int i, nPos, nUnique = 0, clk = clock(); + + // derive AIG for each PO + nPos = Aig_ManPoNum(pAig) - Aig_ManRegNum(pAig); + vBuffers = Vec_PtrAlloc( nPos ); + for ( i = 0; i < nPos; i++ ) + { +// if ( i % 100 == 0 ) +// printf( "%d finished...\n", i ); + pPart = Saig_ManDupCones( pAig, &i, 1 ); + pTemp = Saig_ManDupIsoCanonical( pPart, 0 ); + vStr = Ioa_WriteAigerIntoMemoryStr( pTemp ); + Vec_PtrPush( vBuffers, vStr ); + Aig_ManStop( pTemp ); + Aig_ManStop( pPart ); + // remember the output number in nCap (attention: hack!) + vStr->nCap = i; + } +// s_Counter = 0; + if ( fVerbose ) + Abc_PrintTime( 1, "Isomorph time", clock() - clk ); + + // sort the infos + clk = clock(); + Vec_PtrSort( vBuffers, (int (*)(void))Iso_StoCompareVecStr ); + + // create classes + clk = clock(); + vClasses = Vec_PtrAlloc( Saig_ManPoNum(pAig) ); + // start the first class + Vec_PtrPush( vClasses, (vLevel = Vec_IntAlloc(4)) ); + vPrev = (Vec_Str_t *)Vec_PtrEntry( vBuffers, 0 ); + Vec_IntPush( vLevel, vPrev->nCap ); + // consider other classes + Vec_PtrForEachEntryStart( Vec_Str_t *, vBuffers, vStr, i, 1 ) + { + if ( Vec_StrCompareVec(vPrev, vStr) ) + Vec_PtrPush( vClasses, Vec_IntAlloc(4) ); + vLevel = (Vec_Int_t *)Vec_PtrEntryLast( vClasses ); + Vec_IntPush( vLevel, vStr->nCap ); + vPrev = vStr; + } + Vec_VecFree( (Vec_Vec_t *)vBuffers ); + + if ( fVerbose ) + Abc_PrintTime( 1, "Sorting time", clock() - clk ); +// Abc_PrintTime( 1, "Traversal time", time_Trav ); + + // 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 ) + if ( Vec_IntSize(vLevel) > 1 ) + printf( "%d ", Vec_IntSize(vLevel) ); + else + nUnique++; + printf( " Unique = %d\n", nUnique ); + } + + // collect the first ones + vRemain = Vec_IntAlloc( 100 ); + Vec_PtrForEachEntry( Vec_Int_t *, vClasses, vLevel, i ) + Vec_IntPush( vRemain, Vec_IntEntry(vLevel, 0) ); + + // derive the resulting AIG + pPart = Saig_ManDupCones( pAig, Vec_IntArray(vRemain), Vec_IntSize(vRemain) ); + Vec_IntFree( vRemain ); + +// return (Vec_Vec_t *)vClasses; + Vec_VecFree( (Vec_Vec_t *)vClasses ); + +// printf( "The number of all checks %d. Complex checks %d.\n", nPos*(nPos-1)/2, s_Counter ); + return pPart; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Iso_ManTest( Aig_Man_t * pAig, int fVerbose ) +{ + Vec_Int_t * vPerm; + int clk = clock(); + vPerm = Saig_ManFindIsoPerm( pAig, fVerbose ); + Vec_IntFree( vPerm ); + Abc_PrintTime( 1, "Time", clock() - clk ); + return NULL; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Saig_ManIsoReduce( Aig_Man_t * pAig, int fVerbose ) +{ + Aig_Man_t * pPart; + int clk = clock(); + pPart = Iso_ManFilterPos( pAig, fVerbose ); + printf( "Reduced %d outputs to %d outputs. ", Saig_ManPoNum(pAig), Saig_ManPoNum(pPart) ); + Abc_PrintTime( 1, "Time", clock() - clk ); +// Aig_ManStop( pPart ); + return pPart; +} + + +#include "src/base/abc/abc.h" + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Iso_ManTest888( Aig_Man_t * pAig1, int fVerbose ) +{ + extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters ); + extern Abc_Ntk_t * Abc_NtkFromAigPhase( Aig_Man_t * pMan ); + Abc_Ntk_t * pNtk; + Aig_Man_t * pAig2; + Vec_Int_t * vMap; + + pNtk = Abc_NtkFromAigPhase( pAig1 ); + Abc_NtkPermute( pNtk, 1, 0, 1 ); + pAig2 = Abc_NtkToDar( pNtk, 0, 1 ); + Abc_NtkDelete( pNtk ); + + vMap = Iso_ManFindMapping( pAig1, pAig2, NULL, NULL, fVerbose ); + Aig_ManStop( pAig2 ); + + if ( vMap != NULL ) + { + printf( "Mapping of AIGs is found.\n" ); + if ( fVerbose ) + Vec_IntPrint( vMap ); + } + else + printf( "Mapping of AIGs is NOT found.\n" ); + Vec_IntFreeP( &vMap ); + return NULL; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/aig/saig/saigIsoFast.c b/src/aig/saig/saigIsoFast.c new file mode 100644 index 00000000..6556b90f --- /dev/null +++ b/src/aig/saig/saigIsoFast.c @@ -0,0 +1,352 @@ +/**CFile**************************************************************** + + FileName [aigIsoFast.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [AIG package.] + + Synopsis [Graph isomorphism package.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - April 28, 2007.] + + Revision [$Id: aigIsoFast.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "saig.h" + +ABC_NAMESPACE_IMPL_START + + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +#define AIG_ISO_NUM 16 + +typedef struct Iso_Dat_t_ Iso_Dat_t; +struct Iso_Dat_t_ +{ + unsigned nFiNeg : 3; + unsigned nFoNeg : 2; + unsigned nFoPos : 2; + unsigned Fi0Lev : 3; + unsigned Fi1Lev : 3; + unsigned Level : 3; + unsigned fVisit : 16; +}; + +typedef struct Iso_Dat2_t_ Iso_Dat2_t; +struct Iso_Dat2_t_ +{ + unsigned Data : 16; +}; + +typedef struct Iso_Sto_t_ Iso_Sto_t; +struct Iso_Sto_t_ +{ + Aig_Man_t * pAig; // user's AIG manager + int nObjs; // number of objects + Iso_Dat_t * pData; // data for each object + Vec_Int_t * vVisited; // visited nodes + Vec_Ptr_t * vRoots; // root nodes + Vec_Int_t * vPlaces; // places in the counter lists + int * pCounters; // counters +}; + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Iso_Sto_t * Iso_StoStart( Aig_Man_t * pAig ) +{ + Iso_Sto_t * p; + p = ABC_CALLOC( Iso_Sto_t, 1 ); + p->pAig = pAig; + p->nObjs = Aig_ManObjNumMax( pAig ); + p->pData = ABC_CALLOC( Iso_Dat_t, p->nObjs ); + p->vVisited = Vec_IntStart( 1000 ); + p->vPlaces = Vec_IntStart( 1000 ); + p->vRoots = Vec_PtrStart( 1000 ); + p->pCounters = ABC_CALLOC( int, (1 << AIG_ISO_NUM) ); + return p; +} +void Iso_StoStop( Iso_Sto_t * p ) +{ + Vec_IntFree( p->vPlaces ); + Vec_IntFree( p->vVisited ); + Vec_PtrFree( p->vRoots ); + ABC_FREE( p->pCounters ); + ABC_FREE( p->pData ); + ABC_FREE( p ); +} + +/**Function************************************************************* + + Synopsis [Collect statistics about one node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Iso_StoCollectInfo_rec( Aig_Man_t * p, Aig_Obj_t * pObj, int fCompl, Vec_Int_t * vVisited, Iso_Dat_t * pData, Vec_Ptr_t * vRoots ) +{ + Iso_Dat_t * pThis = pData + Aig_ObjId(pObj); + assert( Aig_ObjIsPi(pObj) || Aig_ObjIsNode(pObj) ); + if ( pThis->fVisit ) + { + if ( fCompl ) + pThis->nFoNeg++; + else + pThis->nFoPos++; + return; + } + assert( *((int *)pThis) == 0 ); + pThis->fVisit = 1; + if ( fCompl ) + pThis->nFoNeg++; + else + pThis->nFoPos++; + pThis->Level = pObj->Level; + pThis->nFiNeg = Aig_ObjFaninC0(pObj) + Aig_ObjFaninC1(pObj); + if ( Aig_ObjIsNode(pObj) ) + { + if ( Aig_ObjFaninC0(pObj) < Aig_ObjFaninC1(pObj) || (Aig_ObjFaninC0(pObj) == Aig_ObjFaninC1(pObj) && Aig_ObjFanin0(pObj)->Level < Aig_ObjFanin1(pObj)->Level) ) + { + pThis->Fi0Lev = pObj->Level - Aig_ObjFanin0(pObj)->Level; + pThis->Fi1Lev = pObj->Level - Aig_ObjFanin1(pObj)->Level; + } + else + { + pThis->Fi0Lev = pObj->Level - Aig_ObjFanin1(pObj)->Level; + pThis->Fi1Lev = pObj->Level - Aig_ObjFanin0(pObj)->Level; + } + Iso_StoCollectInfo_rec( p, Aig_ObjFanin0(pObj), Aig_ObjFaninC0(pObj), vVisited, pData, vRoots ); + Iso_StoCollectInfo_rec( p, Aig_ObjFanin1(pObj), Aig_ObjFaninC1(pObj), vVisited, pData, vRoots ); + } + else if ( Saig_ObjIsLo(p, pObj) ) + { + pThis->Fi0Lev = 1; + pThis->Fi1Lev = 0; + Vec_PtrPush( vRoots, Saig_ObjLoToLi(p, pObj) ); + } + else if ( Saig_ObjIsPi(p, pObj) ) + { + pThis->Fi0Lev = 0; + pThis->Fi1Lev = 0; + } + else + assert( 0 ); + assert( pThis->nFoNeg + pThis->nFoPos ); + Vec_IntPush( vVisited, Aig_ObjId(pObj) ); +} + +//static int time_Trav = 0; + +/**Function************************************************************* + + Synopsis [Collect statistics about one output.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Iso_StoCollectInfo( Iso_Sto_t * p, Aig_Obj_t * pPo ) +{ + int fVerboseShow = 0; + Vec_Int_t * vInfo; + Iso_Dat2_t * pData2 = (Iso_Dat2_t *)p->pData; + Aig_Man_t * pAig = p->pAig; + Aig_Obj_t * pObj; + int i, Value, Entry, * pPerm; + int clk = clock(); + + assert( Aig_ObjIsPo(pPo) ); + + // collect initial POs + Vec_IntClear( p->vVisited ); + Vec_PtrClear( p->vRoots ); + Vec_PtrPush( p->vRoots, pPo ); + + // mark internal nodes + Vec_PtrForEachEntry( Aig_Obj_t *, p->vRoots, pObj, i ) + if ( !Aig_ObjIsConst1(Aig_ObjFanin0(pObj)) ) + Iso_StoCollectInfo_rec( pAig, Aig_ObjFanin0(pObj), Aig_ObjFaninC0(pObj), p->vVisited, p->pData, p->vRoots ); +// time_Trav += clock() - clk; + + // count how many times each data entry appears + Vec_IntClear( p->vPlaces ); + Vec_IntForEachEntry( p->vVisited, Entry, i ) + { + Value = pData2[Entry].Data; +// assert( Value > 0 ); + if ( p->pCounters[Value]++ == 0 ) + Vec_IntPush( p->vPlaces, Value ); +// pData2[Entry].Data = 0; + *((int *)(p->pData + Entry)) = 0; + } + + // collect non-trivial counters + Vec_IntClear( p->vVisited ); + Vec_IntForEachEntry( p->vPlaces, Entry, i ) + { + assert( p->pCounters[Entry] ); + Vec_IntPush( p->vVisited, p->pCounters[Entry] ); + p->pCounters[Entry] = 0; + } +// printf( "%d ", Vec_IntSize(p->vVisited) ); + + // sort the costs in the increasing order + pPerm = Abc_SortCost( Vec_IntArray(p->vVisited), Vec_IntSize(p->vVisited) ); + assert( Vec_IntEntry(p->vVisited, pPerm[0]) <= Vec_IntEntry(p->vVisited, pPerm[Vec_IntSize(p->vVisited)-1]) ); + + // create information + vInfo = Vec_IntAlloc( Vec_IntSize(p->vVisited) ); + for ( i = Vec_IntSize(p->vVisited)-1; i >= 0; i-- ) + { + Entry = Vec_IntEntry( p->vVisited, pPerm[i] ); + Entry = (Entry << AIG_ISO_NUM) | Vec_IntEntry( p->vPlaces, pPerm[i] ); + Vec_IntPush( vInfo, Entry ); + } + ABC_FREE( pPerm ); + + // show the final result + if ( fVerboseShow ) + Vec_IntForEachEntry( vInfo, Entry, i ) + { + Iso_Dat2_t Data = { Entry & 0xFFFF }; + Iso_Dat_t * pData = (Iso_Dat_t *)&Data; + + printf( "%6d : ", i ); + printf( "Freq =%6d ", Entry >> 16 ); + + printf( "FiNeg =%3d ", pData->nFiNeg ); + printf( "FoNeg =%3d ", pData->nFoNeg ); + printf( "FoPos =%3d ", pData->nFoPos ); + printf( "Fi0L =%3d ", pData->Fi0Lev ); + printf( "Fi1L =%3d ", pData->Fi1Lev ); + printf( "Lev =%3d ", pData->Level ); + printf( "\n" ); + } + return vInfo; +} + +/**Function************************************************************* + + Synopsis [Takes multi-output sequential AIG.] + + Description [Returns candidate equivalence classes of POs.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Iso_StoCompareVecInt( Vec_Int_t ** p1, Vec_Int_t ** p2 ) +{ + return Vec_IntCompareVec( *p1, *p2 ); +} + +/**Function************************************************************* + + Synopsis [Takes multi-output sequential AIG.] + + Description [Returns candidate equivalence classes of POs.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Vec_t * Saig_IsoDetectFast( Aig_Man_t * pAig ) +{ + Iso_Sto_t * pMan; + Aig_Obj_t * pObj; + Vec_Ptr_t * vClasses, * vInfos; + Vec_Int_t * vInfo, * vPrev, * vLevel; + int i, Number, nUnique = 0, clk = clock(); + + // collect infos and remember their number + pMan = Iso_StoStart( pAig ); + vInfos = Vec_PtrAlloc( Saig_ManPoNum(pAig) ); + Saig_ManForEachPo( pAig, pObj, i ) + { + vInfo = Iso_StoCollectInfo(pMan, pObj); + Vec_IntPush( vInfo, i ); + Vec_PtrPush( vInfos, vInfo ); + } + Iso_StoStop( pMan ); + Abc_PrintTime( 1, "Info computation time", clock() - clk ); + + // sort the infos + clk = clock(); + Vec_PtrSort( vInfos, (int (*)(void))Iso_StoCompareVecInt ); + + // create classes + clk = clock(); + vClasses = Vec_PtrAlloc( Saig_ManPoNum(pAig) ); + // start the first class + Vec_PtrPush( vClasses, (vLevel = Vec_IntAlloc(4)) ); + vPrev = (Vec_Int_t *)Vec_PtrEntry( vInfos, 0 ); + Vec_IntPush( vLevel, Vec_IntPop(vPrev) ); + // consider other classes + Vec_PtrForEachEntryStart( Vec_Int_t *, vInfos, vInfo, i, 1 ) + { + Number = Vec_IntPop( vInfo ); + if ( Vec_IntCompareVec(vPrev, vInfo) ) + Vec_PtrPush( vClasses, Vec_IntAlloc(4) ); + vLevel = (Vec_Int_t *)Vec_PtrEntryLast( vClasses ); + Vec_IntPush( vLevel, Number ); + vPrev = vInfo; + } + Vec_VecFree( (Vec_Vec_t *)vInfos ); + Abc_PrintTime( 1, "Sorting time", clock() - clk ); +// Abc_PrintTime( 1, "Traversal time", time_Trav ); + + // 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) ); + + Vec_PtrForEachEntry( Vec_Int_t *, vClasses, vLevel, i ) + if ( Vec_IntSize(vLevel) > 1 ) + printf( "%d ", Vec_IntSize(vLevel) ); + else + nUnique++; + printf( " Unique = %d\n", nUnique ); + +// return (Vec_Vec_t *)vClasses; + Vec_VecFree( (Vec_Vec_t *)vClasses ); + return NULL; +} + + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/aig/saig/saigIsoSlow.c b/src/aig/saig/saigIsoSlow.c new file mode 100644 index 00000000..7510c911 --- /dev/null +++ b/src/aig/saig/saigIsoSlow.c @@ -0,0 +1,775 @@ +/**CFile**************************************************************** + + FileName [aigIso.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [AIG package.] + + Synopsis [Graph isomorphism package.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - April 28, 2007.] + + Revision [$Id: aigIso.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "saig.h" + +ABC_NAMESPACE_IMPL_START + + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +#define ISO_NUM_INTS 3 + +typedef struct Iso_Obj_t_ Iso_Obj_t; +struct Iso_Obj_t_ +{ + // hashing entries (related to the parameter ISO_NUM_INTS!) + unsigned Level : 30; + unsigned nFinNeg : 2; + unsigned nFoutPos : 16; + unsigned nFoutNeg : 16; + unsigned nFinLev0 : 16; + unsigned nFinLev1 : 16; +// unsigned nNodes : 16; +// unsigned nEdges : 16; + // other data + int iNext; // hash table entry + int iClass; // next one in class + int Id; // unique ID + Vec_Int_t * vAllies; // solved neighbors +}; + +typedef struct Iso_Man_t_ Iso_Man_t; +struct Iso_Man_t_ +{ + Aig_Man_t * pAig; // user's AIG manager + Iso_Obj_t * pObjs; // isomorphism objects + int nObjIds; // counter of object IDs + int nClasses; // total number of classes + int nEntries; // total number of entries + int nSingles; // total number of singletons + int nObjs; // total objects + int nBins; // hash table size + int * pBins; // hash table + Vec_Ptr_t * vSingles; // singletons + Vec_Ptr_t * vClasses; // other classes + Vec_Ptr_t * vTemp1; // other classes + Vec_Ptr_t * vTemp2; // other classes +}; + +static inline Iso_Obj_t * Iso_ManObj( Iso_Man_t * p, int i ) { assert( i >= 0 && i < p->nObjs ); return i ? p->pObjs + i : NULL; } +static inline int Iso_ObjId( Iso_Man_t * p, Iso_Obj_t * pObj ) { assert( pObj > p->pObjs && pObj < p->pObjs + p->nObjs ); return pObj - p->pObjs; } +static inline Aig_Obj_t * Iso_AigObj( Iso_Man_t * p, Iso_Obj_t * q ) { return Aig_ManObj( p->pAig, Iso_ObjId(p, q) ); } + +#define Iso_ManForEachObj( p, pObj, i ) \ + for ( i = 1; (i < p->nObjs) && ((pObj) = Iso_ManObj(p, i)); i++ ) if ( pIso->Level == -1 ) {} else + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Iso_ManObjCount_rec( Aig_Man_t * p, Aig_Obj_t * pObj, int * pnNodes, int * pnEdges ) +{ + if ( Aig_ObjIsPi(pObj) ) + return; + if ( Aig_ObjIsTravIdCurrent(p, pObj) ) + return; + Aig_ObjSetTravIdCurrent(p, pObj); + Iso_ManObjCount_rec( p, Aig_ObjFanin0(pObj), pnNodes, pnEdges ); + Iso_ManObjCount_rec( p, Aig_ObjFanin1(pObj), pnNodes, pnEdges ); + (*pnEdges) += Aig_ObjFaninC0(pObj) + Aig_ObjFaninC1(pObj); + (*pnNodes)++; +} +void Iso_ManObjCount( Aig_Man_t * p, Aig_Obj_t * pObj, int * pnNodes, int * pnEdges ) +{ + assert( Aig_ObjIsNode(pObj) ); + *pnNodes = *pnEdges = 0; + Aig_ManIncrementTravId( p ); + Iso_ManObjCount_rec( p, pObj, pnNodes, pnEdges ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Iso_Man_t * Iso_ManStart( Aig_Man_t * pAig ) +{ + Iso_Man_t * p; + p = ABC_CALLOC( Iso_Man_t, 1 ); + p->pAig = pAig; + p->nObjs = Aig_ManObjNumMax( pAig ); + p->pObjs = ABC_CALLOC( Iso_Obj_t, p->nObjs ); + p->nBins = Abc_PrimeCudd( p->nObjs ); + p->pBins = ABC_CALLOC( int, p->nBins ); + p->vSingles = Vec_PtrAlloc( 1000 ); + p->vClasses = Vec_PtrAlloc( 1000 ); + p->vTemp1 = Vec_PtrAlloc( 1000 ); + p->vTemp2 = Vec_PtrAlloc( 1000 ); + p->nObjIds = 1; + return p; +} +void Iso_ManStop( Iso_Man_t * p ) +{ + Iso_Obj_t * pIso; + int i; + Iso_ManForEachObj( p, pIso, i ) + Vec_IntFreeP( &pIso->vAllies ); + Vec_PtrFree( p->vTemp1 ); + Vec_PtrFree( p->vTemp2 ); + Vec_PtrFree( p->vClasses ); + Vec_PtrFree( p->vSingles ); + ABC_FREE( p->pBins ); + ABC_FREE( p->pObjs ); + ABC_FREE( p ); +} + + +/**Function************************************************************* + + Synopsis [Compares two objects by their signature.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Iso_ObjCompare( Iso_Obj_t ** pp1, Iso_Obj_t ** pp2 ) +{ + Iso_Obj_t * pIso1 = *pp1; + Iso_Obj_t * pIso2 = *pp2; + int Diff = -memcmp( pIso1, pIso2, sizeof(int) * ISO_NUM_INTS ); + if ( Diff ) + return Diff; + return -Vec_IntCompareVec( pIso1->vAllies, pIso2->vAllies ); +} + +/**Function************************************************************* + + Synopsis [Compares two objects by their ID.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Iso_ObjCompareById( Iso_Obj_t ** pp1, Iso_Obj_t ** pp2 ) +{ + Iso_Obj_t * pIso1 = *pp1; + Iso_Obj_t * pIso2 = *pp2; + return pIso1->Id - pIso2->Id; +} + +/**Function************************************************************* + + Synopsis [Compares two objects by their ID.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Iso_ObjCompareAigObjByData( Aig_Obj_t ** pp1, Aig_Obj_t ** pp2 ) +{ + Aig_Obj_t * pIso1 = *pp1; + Aig_Obj_t * pIso2 = *pp2; + assert( Aig_ObjIsPi(pIso1) || Aig_ObjIsPo(pIso1) ); + assert( Aig_ObjIsPi(pIso2) || Aig_ObjIsPo(pIso2) ); + return pIso1->iData - pIso2->iData; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Iso_ObjHash( Iso_Obj_t * pIso, int nBins ) +{ + static unsigned BigPrimes[8] = {12582917, 25165843, 50331653, 100663319, 201326611, 402653189, 805306457, 1610612741}; + unsigned * pArray = (unsigned *)pIso; + unsigned i, Value = 0; + assert( ISO_NUM_INTS < 8 ); + for ( i = 0; i < ISO_NUM_INTS; i++ ) + Value ^= BigPrimes[i] * pArray[i]; + return Value % nBins; +} +static inline int Iso_ObjHashAdd( Iso_Man_t * p, Iso_Obj_t * pIso ) +{ + Iso_Obj_t * pThis; + int * pPlace = p->pBins + Iso_ObjHash( pIso, p->nBins ); + p->nEntries++; + for ( pThis = Iso_ManObj(p, *pPlace); + pThis; pPlace = &pThis->iNext, + pThis = Iso_ManObj(p, *pPlace) ) + if ( Iso_ObjCompare( &pThis, &pIso ) == 0 ) // equal signatures + { + if ( pThis->iClass == 0 ) + { + p->nClasses++; + p->nSingles--; + } + // add to the list + pIso->iClass = pThis->iClass; + pThis->iClass = Iso_ObjId( p, pIso ); + return 1; + } + // create new list + *pPlace = Iso_ObjId( p, pIso ); + p->nSingles++; + return 0; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Iso_ManCollectClasses( Iso_Man_t * p ) +{ + Iso_Obj_t * pIso; + int i; + Vec_PtrClear( p->vSingles ); + Vec_PtrClear( p->vClasses ); + for ( i = 0; i < p->nBins; i++ ) + for ( pIso = Iso_ManObj(p, p->pBins[i]); pIso; pIso = Iso_ManObj(p, pIso->iNext) ) + { + assert( pIso->Id == 0 ); + if ( pIso->iClass ) + Vec_PtrPush( p->vClasses, pIso ); + else + Vec_PtrPush( p->vSingles, pIso ); + } + Vec_PtrSort( p->vSingles, (int (*)(void))Iso_ObjCompare ); + Vec_PtrSort( p->vClasses, (int (*)(void))Iso_ObjCompare ); + assert( Vec_PtrSize(p->vSingles) == p->nSingles ); + assert( Vec_PtrSize(p->vClasses) == p->nClasses ); + // assign IDs to singletons + Vec_PtrForEachEntry( Iso_Obj_t *, p->vSingles, pIso, i ) + if ( pIso->Id == 0 ) + pIso->Id = p->nObjIds++; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Iso_Man_t * Iso_ManCreate( Aig_Man_t * pAig ) +{ + Iso_Man_t * p; + Iso_Obj_t * pIso; + Aig_Obj_t * pObj; + int i, nNodes = 0, nEdges = 0; + p = Iso_ManStart( pAig ); + Aig_ManForEachObj( pAig, pObj, i ) + { + if ( Aig_ObjIsNode(pObj) ) + { + pIso = p->pObjs + Aig_ObjFaninId0(pObj); + if ( Aig_ObjFaninC0(pObj) ) + pIso->nFoutNeg++; + else + pIso->nFoutPos++; + pIso = p->pObjs + Aig_ObjFaninId1(pObj); + if ( Aig_ObjFaninC1(pObj) ) + pIso->nFoutNeg++; + else + pIso->nFoutPos++; + } + else if ( Aig_ObjIsPo(pObj) ) + { + pIso = p->pObjs + Aig_ObjFaninId0(pObj); + if ( Aig_ObjFaninC0(pObj) ) + pIso->nFoutNeg++; + else + pIso->nFoutPos++; + } + } + Aig_ManForEachObj( pAig, pObj, i ) + { + if ( !Aig_ObjIsPi(pObj) && !Aig_ObjIsNode(pObj) ) + continue; + pIso = p->pObjs + i; + pIso->Level = pObj->Level; + pIso->nFinNeg = Aig_ObjFaninC0(pObj) + Aig_ObjFaninC1(pObj); + if ( Aig_ObjIsNode(pObj) ) + { + if ( Aig_ObjIsMuxType(pObj) ) // uniqify MUX/XOR + pIso->nFinNeg = 3; + if ( Aig_ObjFaninC0(pObj) < Aig_ObjFaninC1(pObj) || (Aig_ObjFaninC0(pObj) == Aig_ObjFaninC1(pObj) && Aig_ObjFanin0(pObj)->Level < Aig_ObjFanin1(pObj)->Level) ) + { + pIso->nFinLev0 = Aig_ObjFanin0(pObj)->Level; + pIso->nFinLev1 = Aig_ObjFanin1(pObj)->Level; + } + else + { + pIso->nFinLev0 = Aig_ObjFanin1(pObj)->Level; + pIso->nFinLev1 = Aig_ObjFanin0(pObj)->Level; + } +// Iso_ManObjCount( pAig, pObj, &nNodes, &nEdges ); +// pIso->nNodes = nNodes; +// pIso->nEdges = nEdges; + } + else + { + pIso->nFinLev0 = (int)(Aig_ObjPioNum(pObj) >= Aig_ManPiNum(pAig) - Aig_ManRegNum(pAig)); // uniqify flop + } + // add to the hash table + Iso_ObjHashAdd( p, pIso ); + } + Iso_ManCollectClasses( p ); + return p; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Iso_ManPrintClasses( Iso_Man_t * p, int fVerbose, int fVeryVerbose ) +{ + int fOnlyCis = 0; + Iso_Obj_t * pIso, * pTemp; + int i; + + // count unique objects + if ( fVerbose ) + printf( "Total objects =%7d. Entries =%7d. Classes =%7d. Singles =%7d.\n", + p->nObjs, p->nEntries, p->nClasses, p->nSingles ); + + if ( !fVeryVerbose ) + return; + + printf( "Non-trivial classes:\n" ); + Vec_PtrForEachEntry( Iso_Obj_t *, p->vClasses, pIso, i ) + { + if ( fOnlyCis && pIso->Level > 0 ) + continue; + + printf( "%5d : {", i ); + for ( pTemp = pIso; pTemp; pTemp = Iso_ManObj(p, pTemp->iClass) ) + { + if ( fOnlyCis ) + printf( " %d", Aig_ObjPioNum( Iso_AigObj(p, pTemp) ) ); + else + { + Aig_Obj_t * pObj = Iso_AigObj(p, pTemp); + if ( Aig_ObjIsNode(pObj) ) + printf( " %d{%s%d(%d),%s%d(%d)}", Iso_ObjId(p, pTemp), + Aig_ObjFaninC0(pObj)? "-": "+", Aig_ObjFaninId0(pObj), Aig_ObjLevel(Aig_ObjFanin0(pObj)), + Aig_ObjFaninC1(pObj)? "-": "+", Aig_ObjFaninId1(pObj), Aig_ObjLevel(Aig_ObjFanin1(pObj)) ); + else + printf( " %d", Iso_ObjId(p, pTemp) ); + } + printf( "(%d,%d,%d)", pTemp->Level, pTemp->nFoutPos, pTemp->nFoutNeg ); + if ( pTemp->vAllies ) + { + int Entry, k; + printf( "[" ); + Vec_IntForEachEntry( pTemp->vAllies, Entry, k ) + printf( "%s%d", k?",":"", Entry ); + printf( "]" ); + } + } + printf( " }\n" ); + } +} + + +/**Function************************************************************* + + Synopsis [Creates adjacency lists.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Iso_ObjAddToAllies( Iso_Obj_t * pIso, int Id, int fCompl ) +{ + assert( pIso->Id == 0 ); + if ( pIso->vAllies == NULL ) + pIso->vAllies = Vec_IntAlloc( 8 ); + Vec_IntPush( pIso->vAllies, fCompl ? -Id : Id ); +} +void Iso_ManAssignAdjacency( Iso_Man_t * p ) +{ + Iso_Obj_t * pIso, * pIso0, * pIso1; + Aig_Obj_t * pObj, * pObjLi; + int i; + // clean + Aig_ManForEachObj( p->pAig, pObj, i ) + { + if ( i == 0 ) continue; + pIso = Iso_ManObj( p, i ); + if ( pIso->vAllies ) + Vec_IntClear( pIso->vAllies ); + } + // create + Aig_ManForEachNode( p->pAig, pObj, i ) + { + pIso = Iso_ManObj( p, i ); + pIso0 = Iso_ManObj( p, Aig_ObjFaninId0(pObj) ); + pIso1 = Iso_ManObj( p, Aig_ObjFaninId1(pObj) ); + if ( pIso->Id ) // unique - add to non-unique fanins + { + if ( pIso0->Id == 0 ) + Iso_ObjAddToAllies( pIso0, pIso->Id, Aig_ObjFaninC0(pObj) ); + if ( pIso1->Id == 0 ) + Iso_ObjAddToAllies( pIso1, pIso->Id, Aig_ObjFaninC1(pObj) ); + } + else // non-unique - assign unique fanins to it + { + if ( pIso0->Id != 0 ) + Iso_ObjAddToAllies( pIso, pIso0->Id, Aig_ObjFaninC0(pObj) ); + if ( pIso1->Id != 0 ) + Iso_ObjAddToAllies( pIso, pIso1->Id, Aig_ObjFaninC1(pObj) ); + } + } + // consider flops + Aig_ManForEachLiLoSeq( p->pAig, pObjLi, pObj, i ) + { + if ( Aig_ObjFaninId0(pObjLi) == 0 ) // ignore constant! + continue; + pIso = Iso_ManObj( p, Aig_ObjId(pObj) ); + pIso0 = Iso_ManObj( p, Aig_ObjFaninId0(pObjLi) ); + if ( pIso->Id ) // unique - add to non-unique fanins + { + if ( pIso0->Id == 0 ) + Iso_ObjAddToAllies( pIso0, pIso->Id, Aig_ObjFaninC0(pObjLi) ); + } + else // non-unique - assign unique fanins to it + { + if ( pIso0->Id != 0 ) + Iso_ObjAddToAllies( pIso, pIso0->Id, Aig_ObjFaninC0(pObjLi) ); + } + } + // sort + Aig_ManForEachObj( p->pAig, pObj, i ) + { + if ( i == 0 ) continue; + pIso = Iso_ManObj( p, i ); + if ( pIso->vAllies ) + Vec_IntSort( pIso->vAllies, 0 ); + } +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Iso_ManRehashClassNodes( Iso_Man_t * p ) +{ + Iso_Obj_t * pIso, * pTemp; + int i; + // collect nodes + Vec_PtrClear( p->vTemp1 ); + Vec_PtrClear( p->vTemp2 ); + Vec_PtrForEachEntry( Iso_Obj_t *, p->vClasses, pIso, i ) + { + for ( pTemp = pIso; pTemp; pTemp = Iso_ManObj(p, pTemp->iClass) ) + if ( pTemp->Id == 0 ) + Vec_PtrPush( p->vTemp1, pTemp ); + else + Vec_PtrPush( p->vTemp2, pTemp ); + } + // clean and add nodes + p->nClasses = 0; // total number of classes + p->nEntries = 0; // total number of entries + p->nSingles = 0; // total number of singletons + memset( p->pBins, 0, sizeof(int) * p->nBins ); + Vec_PtrForEachEntry( Iso_Obj_t *, p->vTemp1, pTemp, i ) + { + assert( pTemp->Id == 0 ); + pTemp->iClass = pTemp->iNext = 0; + Iso_ObjHashAdd( p, pTemp ); + } + Vec_PtrForEachEntry( Iso_Obj_t *, p->vTemp2, pTemp, i ) + { + assert( pTemp->Id != 0 ); + pTemp->iClass = pTemp->iNext = 0; + } + // collect new classes + Iso_ManCollectClasses( p ); +} + +/**Function************************************************************* + + Synopsis [Find nodes with the min number of edges.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Iso_Obj_t * Iso_ManFindBestObj( Iso_Man_t * p, Iso_Obj_t * pIso ) +{ + Iso_Obj_t * pTemp, * pBest = NULL; + int nNodesBest = -1, nNodes; + int nEdgesBest = -1, nEdges; + assert( pIso->Id == 0 ); + if ( pIso->Level == 0 ) + return pIso; + for ( pTemp = pIso; pTemp; pTemp = Iso_ManObj(p, pTemp->iClass) ) + { + assert( pTemp->Id == 0 ); + Iso_ManObjCount( p->pAig, Iso_AigObj(p, pTemp), &nNodes, &nEdges ); +// printf( "%d,%d ", nNodes, nEdges ); + if ( nNodesBest < nNodes || (nNodesBest == nNodes && nEdgesBest < nEdges) ) + { + nNodesBest = nNodes; + nEdgesBest = nEdges; + pBest = pTemp; + } + } +// printf( "\n" ); + return pBest; +} + +/**Function************************************************************* + + Synopsis [Find nodes with the min number of edges.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Iso_ManBreakTies( Iso_Man_t * p, int fVerbose ) +{ + int fUseOneBest = 0; + Iso_Obj_t * pIso, * pTemp; + int i, LevelStart = 0; + pIso = (Iso_Obj_t *)Vec_PtrEntry( p->vClasses, 0 ); + LevelStart = pIso->Level; + if ( fVerbose ) + printf( "Best level %d\n", LevelStart ); + Vec_PtrForEachEntry( Iso_Obj_t *, p->vClasses, pIso, i ) + { + if ( (int)pIso->Level < LevelStart ) + break; + if ( !fUseOneBest ) + { + for ( pTemp = pIso; pTemp; pTemp = Iso_ManObj(p, pTemp->iClass) ) + { + assert( pTemp->Id == 0 ); + pTemp->Id = p->nObjIds++; + } + continue; + } + if ( pIso->Level == 0 && pIso->nFoutPos + pIso->nFoutNeg == 0 ) + { + for ( pTemp = pIso; pTemp; pTemp = Iso_ManObj(p, pTemp->iClass) ) + pTemp->Id = p->nObjIds++; + continue; + } + pIso = Iso_ManFindBestObj( p, pIso ); + pIso->Id = p->nObjIds++; + } +} + +/**Function************************************************************* + + Synopsis [Finalizes unification of combinational outputs.] + + Description [Assigns IDs to the unclassified CIs in the order of obj IDs.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Iso_ManFinalize( Iso_Man_t * p ) +{ + Vec_Int_t * vRes; + Aig_Obj_t * pObj; + int i; + assert( p->nClasses == 0 ); + assert( Vec_PtrSize(p->vClasses) == 0 ); + // set canonical numbers + Aig_ManForEachObj( p->pAig, pObj, i ) + { + if ( !Aig_ObjIsPi(pObj) && !Aig_ObjIsNode(pObj) ) + { + pObj->iData = -1; + continue; + } + pObj->iData = Iso_ManObj(p, Aig_ObjId(pObj))->Id; + assert( pObj->iData > 0 ); + } + Aig_ManConst1(p->pAig)->iData = 0; + // assign unique IDs to the CIs + Vec_PtrClear( p->vTemp1 ); + Vec_PtrClear( p->vTemp2 ); + Aig_ManForEachPi( p->pAig, pObj, i ) + { + assert( pObj->iData > 0 ); + if ( Aig_ObjPioNum(pObj) >= Aig_ManPiNum(p->pAig) - Aig_ManRegNum(p->pAig) ) // flop + Vec_PtrPush( p->vTemp2, pObj ); + else // PI + Vec_PtrPush( p->vTemp1, pObj ); + } + // sort CIs by their IDs + Vec_PtrSort( p->vTemp1, (int (*)(void))Iso_ObjCompareAigObjByData ); + Vec_PtrSort( p->vTemp2, (int (*)(void))Iso_ObjCompareAigObjByData ); + // create the result + vRes = Vec_IntAlloc( Aig_ManPiNum(p->pAig) ); + Vec_PtrForEachEntry( Aig_Obj_t *, p->vTemp1, pObj, i ) + Vec_IntPush( vRes, Aig_ObjPioNum(pObj) ); + Vec_PtrForEachEntry( Aig_Obj_t *, p->vTemp2, pObj, i ) + Vec_IntPush( vRes, Aig_ObjPioNum(pObj) ); + return vRes; +} + +/**Function************************************************************* + + Synopsis [Find nodes with the min number of edges.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Iso_ManDumpOneClass( Iso_Man_t * p ) +{ + Vec_Ptr_t * vNodes = Vec_PtrAlloc( 100 ); + Iso_Obj_t * pIso, * pTemp; + Aig_Man_t * pNew = NULL; + assert( p->nClasses > 0 ); + pIso = (Iso_Obj_t *)Vec_PtrEntry( p->vClasses, 0 ); + assert( pIso->Id == 0 ); + for ( pTemp = pIso; pTemp; pTemp = Iso_ManObj(p, pTemp->iClass) ) + { + assert( pTemp->Id == 0 ); + Vec_PtrPush( vNodes, Iso_AigObj(p, pTemp) ); + } + pNew = Aig_ManDupNodes( p->pAig, vNodes ); + Vec_PtrFree( vNodes ); + Aig_ManShow( pNew, 0, NULL ); + Aig_ManStopP( &pNew ); +} + +/**Function************************************************************* + + Synopsis [Finds canonical permutation of CIs and assigns unique IDs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Saig_ManFindIsoPerm( Aig_Man_t * pAig, int fVerbose ) +{ + Vec_Int_t * vRes; + Iso_Man_t * p; + p = Iso_ManCreate( pAig ); + Iso_ManPrintClasses( p, fVerbose, 0 ); + while ( p->nClasses ) + { + // assign adjacency to classes + Iso_ManAssignAdjacency( p ); + // rehash the class nodes + Iso_ManRehashClassNodes( p ); + Iso_ManPrintClasses( p, fVerbose, 0 ); + // force refinement + while ( p->nSingles == 0 && p->nClasses ) + { + // assign IDs to the topmost level of classes + Iso_ManBreakTies( p, fVerbose ); + // assign adjacency to classes + Iso_ManAssignAdjacency( p ); + // rehash the class nodes + Iso_ManRehashClassNodes( p ); + Iso_ManPrintClasses( p, fVerbose, 0 ); + } + } +// printf( "IDs assigned = %d. Objects = %d.\n", p->nObjIds, 1+Aig_ManPiNum(p->pAig)+Aig_ManNodeNum(p->pAig) ); + assert( p->nObjIds == 1+Aig_ManPiNum(p->pAig)+Aig_ManNodeNum(p->pAig) ); +// if ( p->nClasses ) +// Iso_ManDumpOneClass( p ); + vRes = Iso_ManFinalize( p ); + Iso_ManStop( p ); + return vRes; +} + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + -- cgit v1.2.3