| /**CFile**************************************************************** |
| |
| FileName [giaIso.c] |
| |
| SystemName [ABC: Logic synthesis and verification system.] |
| |
| PackageName [Scalable AIG package.] |
| |
| Synopsis [Graph isomorphism.] |
| |
| Author [Alan Mishchenko] |
| |
| Affiliation [UC Berkeley] |
| |
| Date [Ver. 1.0. Started - June 20, 2005.] |
| |
| Revision [$Id: giaIso.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] |
| |
| ***********************************************************************/ |
| |
| #include "gia.h" |
| |
| ABC_NAMESPACE_IMPL_START |
| |
| |
| #define ISO_MASK 0xFF |
| static unsigned int s_256Primes[ISO_MASK+1] = |
| { |
| 0x984b6ad9,0x18a6eed3,0x950353e2,0x6222f6eb,0xdfbedd47,0xef0f9023,0xac932a26,0x590eaf55, |
| 0x97d0a034,0xdc36cd2e,0x22736b37,0xdc9066b0,0x2eb2f98b,0x5d9c7baf,0x85747c9e,0x8aca1055, |
| 0x50d66b74,0x2f01ae9e,0xa1a80123,0x3e1ce2dc,0xebedbc57,0x4e68bc34,0x855ee0cf,0x17275120, |
| 0x2ae7f2df,0xf71039eb,0x7c283eec,0x70cd1137,0x7cf651f3,0xa87bfa7a,0x14d87f02,0xe82e197d, |
| 0x8d8a5ebe,0x1e6a15dc,0x197d49db,0x5bab9c89,0x4b55dea7,0x55dede49,0x9a6a8080,0xe5e51035, |
| 0xe148d658,0x8a17eb3b,0xe22e4b38,0xe5be2a9a,0xbe938cbb,0x3b981069,0x7f9c0c8e,0xf756df10, |
| 0x8fa783f7,0x252062ce,0x3dc46b4b,0xf70f6432,0x3f378276,0x44b137a1,0x2bf74b77,0x04892ed6, |
| 0xfd318de1,0xd58c235e,0x94c6d25b,0x7aa5f218,0x35c9e921,0x5732fbbb,0x06026481,0xf584a44f, |
| 0x946e1b5f,0x8463d5b2,0x4ebca7b2,0x54887b15,0x08d1e804,0x5b22067d,0x794580f6,0xb351ea43, |
| 0xbce555b9,0x19ae2194,0xd32f1396,0x6fc1a7f1,0x1fd8a867,0x3a89fdb0,0xea49c61c,0x25f8a879, |
| 0xde1e6437,0x7c74afca,0x8ba63e50,0xb1572074,0xe4655092,0xdb6f8b1c,0xc2955f3c,0x327f85ba, |
| 0x60a17021,0x95bd261d,0xdea94f28,0x04528b65,0xbe0109cc,0x26dd5688,0x6ab2729d,0xc4f029ce, |
| 0xacf7a0be,0x4c912f55,0x34c06e65,0x4fbb938e,0x1533fb5f,0x03da06bd,0x48262889,0xc2523d7d, |
| 0x28a71d57,0x89f9713a,0xf574c551,0x7a99deb5,0x52834d91,0x5a6f4484,0xc67ba946,0x13ae698f, |
| 0x3e390f34,0x34fc9593,0x894c7932,0x6cf414a3,0xdb7928ab,0x13a3b8a3,0x4b381c1d,0xa10b54cb, |
| 0x55359d9d,0x35a3422a,0x58d1b551,0x0fd4de20,0x199eb3f4,0x167e09e2,0x3ee6a956,0x5371a7fa, |
| 0xd424efda,0x74f521c5,0xcb899ff6,0x4a42e4f4,0x747917b6,0x4b08df0b,0x090c7a39,0x11e909e4, |
| 0x258e2e32,0xd9fad92d,0x48fe5f69,0x0545cde6,0x55937b37,0x9b4ae4e4,0x1332b40e,0xc3792351, |
| 0xaff982ef,0x4dba132a,0x38b81ef1,0x28e641bf,0x227208c1,0xec4bbe37,0xc4e1821c,0x512c9d09, |
| 0xdaef1257,0xb63e7784,0x043e04d7,0x9c2cea47,0x45a0e59a,0x281315ca,0x849f0aac,0xa4071ed3, |
| 0x0ef707b3,0xfe8dac02,0x12173864,0x471f6d46,0x24a53c0a,0x35ab9265,0xbbf77406,0xa2144e79, |
| 0xb39a884a,0x0baf5b6d,0xcccee3dd,0x12c77584,0x2907325b,0xfd1adcd2,0xd16ee972,0x345ad6c1, |
| 0x315ebe66,0xc7ad2b8d,0x99e82c8d,0xe52da8c8,0xba50f1d3,0x66689cd8,0x2e8e9138,0x43e15e74, |
| 0xf1ced14d,0x188ec52a,0xe0ef3cbb,0xa958aedc,0x4107a1bc,0x5a9e7a3e,0x3bde939f,0xb5b28d5a, |
| 0x596fe848,0xe85ad00c,0x0b6b3aae,0x44503086,0x25b5695c,0xc0c31dcd,0x5ee617f0,0x74d40c3a, |
| 0xd2cb2b9f,0x1e19f5fa,0x81e24faf,0xa01ed68f,0xcee172fc,0x7fdf2e4d,0x002f4774,0x664f82dd, |
| 0xc569c39a,0xa2d4dcbe,0xaadea306,0xa4c947bf,0xa413e4e3,0x81fb5486,0x8a404970,0x752c980c, |
| 0x98d1d881,0x5c932c1e,0xeee65dfb,0x37592cdd,0x0fd4e65b,0xad1d383f,0x62a1452f,0x8872f68d, |
| 0xb58c919b,0x345c8ee3,0xb583a6d6,0x43d72cb3,0x77aaa0aa,0xeb508242,0xf2db64f8,0x86294328, |
| 0x82211731,0x1239a9d5,0x673ba5de,0xaf4af007,0x44203b19,0x2399d955,0xa175cd12,0x595928a7, |
| 0x6918928b,0xde3126bb,0x6c99835c,0x63ba1fa2,0xdebbdff0,0x3d02e541,0xd6f7aac6,0xe80b4cd0, |
| 0xd0fa29f1,0x804cac5e,0x2c226798,0x462f624c,0xad05b377,0x22924fcd,0xfbea205c,0x1b47586d |
| }; |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// DECLARATIONS /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| typedef struct Gia_IsoMan_t_ Gia_IsoMan_t; |
| struct Gia_IsoMan_t_ |
| { |
| Gia_Man_t * pGia; |
| int nObjs; |
| int nUniques; |
| int nSingles; |
| int nEntries; |
| // internal data |
| int * pLevels; |
| int * pUniques; |
| word * pStoreW; |
| unsigned * pStoreU; |
| // equivalence classes |
| Vec_Int_t * vLevCounts; |
| Vec_Int_t * vClasses; |
| Vec_Int_t * vClasses2; |
| // statistics |
| abctime timeStart; |
| abctime timeSim; |
| abctime timeRefine; |
| abctime timeSort; |
| abctime timeOther; |
| abctime timeTotal; |
| }; |
| |
| static inline unsigned Gia_IsoGetValue( Gia_IsoMan_t * p, int i ) { return (unsigned)(p->pStoreW[i]); } |
| static inline unsigned Gia_IsoGetItem( Gia_IsoMan_t * p, int i ) { return (unsigned)(p->pStoreW[i] >> 32); } |
| |
| static inline void Gia_IsoSetValue( Gia_IsoMan_t * p, int i, unsigned v ) { ((unsigned *)(p->pStoreW + i))[0] = v; } |
| static inline void Gia_IsoSetItem( Gia_IsoMan_t * p, int i, unsigned v ) { ((unsigned *)(p->pStoreW + i))[1] = v; } |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// FUNCTION DEFINITIONS /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Gia_IsoMan_t * Gia_IsoManStart( Gia_Man_t * pGia ) |
| { |
| Gia_IsoMan_t * p; |
| p = ABC_CALLOC( Gia_IsoMan_t, 1 ); |
| p->pGia = pGia; |
| p->nObjs = Gia_ManObjNum( pGia ); |
| p->nUniques = 1; |
| p->nEntries = p->nObjs; |
| // internal data |
| p->pLevels = ABC_CALLOC( int, p->nObjs ); |
| p->pUniques = ABC_CALLOC( int, p->nObjs ); |
| p->pStoreW = ABC_CALLOC( word, p->nObjs ); |
| // class representation |
| p->vClasses = Vec_IntAlloc( p->nObjs/4 ); |
| p->vClasses2 = Vec_IntAlloc( p->nObjs/4 ); |
| return p; |
| } |
| void Gia_IsoManStop( Gia_IsoMan_t * p ) |
| { |
| // class representation |
| Vec_IntFree( p->vClasses ); |
| Vec_IntFree( p->vClasses2 ); |
| // internal data |
| ABC_FREE( p->pLevels ); |
| ABC_FREE( p->pUniques ); |
| ABC_FREE( p->pStoreW ); |
| ABC_FREE( p ); |
| } |
| void Gia_IsoManTransferUnique( Gia_IsoMan_t * p ) |
| { |
| Gia_Obj_t * pObj; |
| int i; |
| // copy unique numbers into the nodes |
| Gia_ManForEachObj( p->pGia, pObj, i ) |
| pObj->Value = p->pUniques[i]; |
| } |
| |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Gia_IsoPrintClasses( Gia_IsoMan_t * p ) |
| { |
| int fVerbose = 0; |
| int i, k, iBegin, nSize; |
| printf( "The total of %d classes:\n", Vec_IntSize(p->vClasses)/2 ); |
| Vec_IntForEachEntryDouble( p->vClasses, iBegin, nSize, i ) |
| { |
| printf( "%5d : (%3d,%3d) ", i/2, iBegin, nSize ); |
| if ( fVerbose ) |
| { |
| printf( "{" ); |
| for ( k = 0; k < nSize; k++ ) |
| printf( " %3d,%08x", Gia_IsoGetItem(p, iBegin+k), Gia_IsoGetValue(p, iBegin+k) ); |
| printf( " }" ); |
| } |
| printf( "\n" ); |
| } |
| } |
| void Gia_IsoPrint( Gia_IsoMan_t * p, int Iter, abctime Time ) |
| { |
| printf( "Iter %4d : ", Iter ); |
| printf( "Entries =%8d. ", p->nEntries ); |
| // printf( "Classes =%8d. ", Vec_IntSize(p->vClasses)/2 ); |
| printf( "Uniques =%8d. ", p->nUniques ); |
| printf( "Singles =%8d. ", p->nSingles ); |
| printf( "%9.2f sec", (float)(Time)/(float)(CLOCKS_PER_SEC) ); |
| printf( "\n" ); |
| fflush( stdout ); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Gia_IsoPrepare( Gia_IsoMan_t * p ) |
| { |
| Gia_Obj_t * pObj; |
| int * pLevBegins, * pLevSizes; |
| int i, iObj, MaxLev = 0; |
| // assign levels |
| p->pLevels[0] = 0; |
| Gia_ManForEachCi( p->pGia, pObj, i ) |
| p->pLevels[Gia_ObjId(p->pGia, pObj)] = 0; |
| Gia_ManForEachAnd( p->pGia, pObj, i ) |
| p->pLevels[i] = 1 + Abc_MaxInt( p->pLevels[Gia_ObjFaninId0(pObj, i)], p->pLevels[Gia_ObjFaninId1(pObj, i)] ); |
| Gia_ManForEachCo( p->pGia, pObj, i ) |
| { |
| iObj = Gia_ObjId(p->pGia, pObj); |
| p->pLevels[iObj] = 1 + p->pLevels[Gia_ObjFaninId0(pObj, iObj)]; // "1 +" is different! |
| MaxLev = Abc_MaxInt( MaxLev, p->pLevels[Gia_ObjId(p->pGia, pObj)] ); |
| } |
| |
| // count nodes on each level |
| pLevSizes = ABC_CALLOC( int, MaxLev+1 ); |
| for ( i = 1; i < p->nObjs; i++ ) |
| pLevSizes[p->pLevels[i]]++; |
| // start classes |
| Vec_IntClear( p->vClasses ); |
| Vec_IntPush( p->vClasses, 0 ); |
| Vec_IntPush( p->vClasses, 1 ); |
| // find beginning of each level |
| pLevBegins = ABC_CALLOC( int, MaxLev+2 ); |
| pLevBegins[0] = 1; |
| for ( i = 0; i <= MaxLev; i++ ) |
| { |
| assert( pLevSizes[i] > 0 ); // we do not allow AIG with a const node and no PIs |
| Vec_IntPush( p->vClasses, pLevBegins[i] ); |
| Vec_IntPush( p->vClasses, pLevSizes[i] ); |
| pLevBegins[i+1] = pLevBegins[i] + pLevSizes[i]; |
| } |
| assert( pLevBegins[MaxLev+1] == p->nObjs ); |
| // put them into the structure |
| for ( i = 1; i < p->nObjs; i++ ) |
| Gia_IsoSetItem( p, pLevBegins[p->pLevels[i]]++, i ); |
| ABC_FREE( pLevBegins ); |
| ABC_FREE( pLevSizes ); |
| /* |
| // print the results |
| for ( i = 0; i < p->nObjs; i++ ) |
| printf( "%3d : (%d,%d)\n", i, Gia_IsoGetItem(p, i), Gia_IsoGetValue(p, i) ); |
| printf( "\n" ); |
| */ |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Gia_IsoAssignUnique( Gia_IsoMan_t * p ) |
| { |
| int i, iBegin, nSize; |
| p->nSingles = 0; |
| Vec_IntClear( p->vClasses2 ); |
| Vec_IntForEachEntryDouble( p->vClasses, iBegin, nSize, i ) |
| { |
| if ( nSize == 1 ) |
| { |
| assert( p->pUniques[Gia_IsoGetItem(p, iBegin)] == 0 ); |
| p->pUniques[Gia_IsoGetItem(p, iBegin)] = p->nUniques++; |
| p->nSingles++; |
| } |
| else |
| { |
| Vec_IntPush( p->vClasses2, iBegin ); |
| Vec_IntPush( p->vClasses2, nSize ); |
| } |
| } |
| ABC_SWAP( Vec_Int_t *, p->vClasses, p->vClasses2 ); |
| p->nEntries -= p->nSingles; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Gia_IsoSort( Gia_IsoMan_t * p ) |
| { |
| Gia_Obj_t * pObj, * pObj0; |
| int i, k, fSameValue, iBegin, iBeginOld, nSize, nSizeNew; |
| int fRefined = 0; |
| abctime clk; |
| |
| // go through the equiv classes |
| p->nSingles = 0; |
| Vec_IntClear( p->vClasses2 ); |
| Vec_IntForEachEntryDouble( p->vClasses, iBegin, nSize, i ) |
| { |
| assert( nSize > 1 ); |
| fSameValue = 1; |
| pObj0 = Gia_ManObj( p->pGia, Gia_IsoGetItem(p,iBegin) ); |
| for ( k = 0; k < nSize; k++ ) |
| { |
| pObj = Gia_ManObj( p->pGia, Gia_IsoGetItem(p,iBegin+k) ); |
| Gia_IsoSetValue( p, iBegin+k, pObj->Value ); |
| if ( pObj->Value != pObj0->Value ) |
| fSameValue = 0; |
| } |
| if ( fSameValue ) |
| { |
| Vec_IntPush( p->vClasses2, iBegin ); |
| Vec_IntPush( p->vClasses2, nSize ); |
| continue; |
| } |
| fRefined = 1; |
| // sort objects |
| clk = Abc_Clock(); |
| Abc_QuickSort3( p->pStoreW + iBegin, nSize, 0 ); |
| p->timeSort += Abc_Clock() - clk; |
| // divide into new classes |
| iBeginOld = iBegin; |
| pObj0 = Gia_ManObj( p->pGia, Gia_IsoGetItem(p,iBegin) ); |
| for ( k = 1; k < nSize; k++ ) |
| { |
| pObj = Gia_ManObj( p->pGia, Gia_IsoGetItem(p,iBegin+k) ); |
| if ( pObj0->Value == pObj->Value ) |
| continue; |
| nSizeNew = iBegin + k - iBeginOld; |
| if ( nSizeNew == 1 ) |
| { |
| assert( p->pUniques[Gia_IsoGetItem(p, iBeginOld)] == 0 ); |
| p->pUniques[Gia_IsoGetItem(p, iBeginOld)] = p->nUniques++; |
| p->nSingles++; |
| } |
| else |
| { |
| Vec_IntPush( p->vClasses2, iBeginOld ); |
| Vec_IntPush( p->vClasses2, nSizeNew ); |
| } |
| iBeginOld = iBegin + k; |
| pObj0 = pObj; |
| } |
| // add the last one |
| nSizeNew = iBegin + k - iBeginOld; |
| if ( nSizeNew == 1 ) |
| { |
| assert( p->pUniques[Gia_IsoGetItem(p, iBeginOld)] == 0 ); |
| p->pUniques[Gia_IsoGetItem(p, iBeginOld)] = p->nUniques++; |
| p->nSingles++; |
| } |
| else |
| { |
| Vec_IntPush( p->vClasses2, iBeginOld ); |
| Vec_IntPush( p->vClasses2, nSizeNew ); |
| } |
| } |
| |
| ABC_SWAP( Vec_Int_t *, p->vClasses, p->vClasses2 ); |
| p->nEntries -= p->nSingles; |
| return fRefined; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Vec_Ptr_t * Gia_IsoCollectCosClasses( Gia_IsoMan_t * p, int fVerbose ) |
| { |
| Vec_Ptr_t * vGroups; |
| Vec_Int_t * vLevel; |
| Gia_Obj_t * pObj; |
| int i, k, iBegin, nSize; |
| // add singletons |
| vGroups = Vec_PtrAlloc( 1000 ); |
| Gia_ManForEachPo( p->pGia, pObj, i ) |
| if ( p->pUniques[Gia_ObjId(p->pGia, pObj)] > 0 ) |
| { |
| vLevel = Vec_IntAlloc( 1 ); |
| Vec_IntPush( vLevel, i ); |
| Vec_PtrPush( vGroups, vLevel ); |
| } |
| |
| // add groups |
| Vec_IntForEachEntryDouble( p->vClasses, iBegin, nSize, i ) |
| { |
| for ( k = 0; k < nSize; k++ ) |
| { |
| pObj = Gia_ManObj( p->pGia, Gia_IsoGetItem(p,iBegin+k) ); |
| if ( Gia_ObjIsPo(p->pGia, pObj) ) |
| break; |
| } |
| if ( k == nSize ) |
| continue; |
| vLevel = Vec_IntAlloc( 8 ); |
| for ( k = 0; k < nSize; k++ ) |
| { |
| pObj = Gia_ManObj( p->pGia, Gia_IsoGetItem(p,iBegin+k) ); |
| if ( Gia_ObjIsPo(p->pGia, pObj) ) |
| Vec_IntPush( vLevel, Gia_ObjCioId(pObj) ); |
| } |
| Vec_PtrPush( vGroups, vLevel ); |
| } |
| // canonicize order |
| Vec_PtrForEachEntry( Vec_Int_t *, vGroups, vLevel, i ) |
| Vec_IntSort( vLevel, 0 ); |
| Vec_VecSortByFirstInt( (Vec_Vec_t *)vGroups, 0 ); |
| // Vec_VecFree( (Vec_Vec_t *)vGroups ); |
| // return NULL; |
| return vGroups; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| static inline unsigned Gia_IsoUpdateValue( int Value, int fCompl ) |
| { |
| return (Value+1) * s_256Primes[Abc_Var2Lit(Value, fCompl) & ISO_MASK]; |
| } |
| static inline unsigned Gia_IsoUpdate( Gia_IsoMan_t * p, int Iter, int iObj, int fCompl ) |
| { |
| if ( Iter == 0 ) return Gia_IsoUpdateValue( p->pLevels[iObj], fCompl ); |
| if ( p->pUniques[iObj] > 0 ) return Gia_IsoUpdateValue( p->pUniques[iObj], fCompl ); |
| // if ( p->pUniques[iObj] > 0 ) return Gia_IsoUpdateValue( 11, fCompl ); |
| return 0; |
| } |
| void Gia_IsoSimulate( Gia_IsoMan_t * p, int Iter ) |
| { |
| Gia_Obj_t * pObj, * pObjF; |
| int i, iObj; |
| // initialize constant, inputs, and flops in the first frame |
| Gia_ManConst0(p->pGia)->Value += s_256Primes[ISO_MASK]; |
| Gia_ManForEachPi( p->pGia, pObj, i ) |
| pObj->Value += s_256Primes[ISO_MASK-1]; |
| if ( Iter == 0 ) |
| Gia_ManForEachRo( p->pGia, pObj, i ) |
| pObj->Value += s_256Primes[ISO_MASK-2]; |
| // simulate nodes |
| Gia_ManForEachAnd( p->pGia, pObj, i ) |
| { |
| pObj->Value += Gia_ObjFanin0(pObj)->Value + Gia_IsoUpdate(p, Iter, Gia_ObjFaninId0(pObj, i), Gia_ObjFaninC0(pObj)); |
| pObj->Value += Gia_ObjFanin1(pObj)->Value + Gia_IsoUpdate(p, Iter, Gia_ObjFaninId1(pObj, i), Gia_ObjFaninC1(pObj)); |
| } |
| // simulate COs |
| Gia_ManForEachCo( p->pGia, pObj, i ) |
| { |
| iObj = Gia_ObjId(p->pGia, pObj); |
| pObj->Value += Gia_ObjFanin0(pObj)->Value + Gia_IsoUpdate(p, Iter, Gia_ObjFaninId0(pObj, iObj), Gia_ObjFaninC0(pObj)); |
| } |
| // transfer flop values |
| Gia_ManForEachRiRo( p->pGia, pObjF, pObj, i ) |
| pObj->Value += pObjF->Value; |
| } |
| void Gia_IsoSimulateBack( Gia_IsoMan_t * p, int Iter ) |
| { |
| Gia_Obj_t * pObj, * pObjF; |
| int i, iObj; |
| // simulate COs |
| Gia_ManForEachCo( p->pGia, pObj, i ) |
| { |
| iObj = Gia_ObjId(p->pGia, pObj); |
| Gia_ObjFanin0(pObj)->Value += pObj->Value + Gia_IsoUpdate(p, Iter, iObj, Gia_ObjFaninC0(pObj)); |
| } |
| // simulate objects |
| Gia_ManForEachAndReverse( p->pGia, pObj, i ) |
| { |
| Gia_ObjFanin0(pObj)->Value += pObj->Value + Gia_IsoUpdate(p, Iter, i, Gia_ObjFaninC0(pObj)); |
| Gia_ObjFanin1(pObj)->Value += pObj->Value + Gia_IsoUpdate(p, Iter, i, Gia_ObjFaninC1(pObj)); |
| } |
| // transfer flop values |
| Gia_ManForEachRiRo( p->pGia, pObjF, pObj, i ) |
| pObjF->Value += pObj->Value; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Gia_IsoAssignOneClass2( Gia_IsoMan_t * p ) |
| { |
| int i, iBegin = -1, nSize = -1; |
| // find two variable class |
| assert( Vec_IntSize(p->vClasses) > 0 ); |
| Vec_IntForEachEntryDouble( p->vClasses, iBegin, nSize, i ) |
| { |
| if ( nSize == 2 ) |
| break; |
| } |
| assert( nSize > 1 ); |
| |
| if ( nSize == 2 ) |
| { |
| assert( p->pUniques[Gia_IsoGetItem(p, iBegin)] == 0 ); |
| p->pUniques[Gia_IsoGetItem(p, iBegin)] = p->nUniques++; |
| p->nSingles++; |
| p->nEntries--; |
| |
| assert( p->pUniques[Gia_IsoGetItem(p, iBegin+1)] == 0 ); |
| p->pUniques[Gia_IsoGetItem(p, iBegin+1)] = p->nUniques++; |
| p->nSingles++; |
| p->nEntries--; |
| } |
| else |
| { |
| assert( p->pUniques[Gia_IsoGetItem(p, iBegin)] == 0 ); |
| p->pUniques[Gia_IsoGetItem(p, iBegin)] = p->nUniques++; |
| p->nSingles++; |
| p->nEntries--; |
| } |
| |
| for ( ; i < Vec_IntSize(p->vClasses) - 2; i += 2 ) |
| { |
| p->vClasses->pArray[i+0] = p->vClasses->pArray[i+2]; |
| p->vClasses->pArray[i+1] = p->vClasses->pArray[i+3]; |
| } |
| Vec_IntShrink( p->vClasses, Vec_IntSize(p->vClasses) - 2 ); |
| |
| printf( "Broke ties in class %d of size %d at level %d.\n", i/2, nSize, p->pLevels[Gia_IsoGetItem(p, iBegin)] ); |
| } |
| |
| void Gia_IsoAssignOneClass3( Gia_IsoMan_t * p ) |
| { |
| int iBegin, nSize; |
| // find the last class |
| assert( Vec_IntSize(p->vClasses) > 0 ); |
| iBegin = Vec_IntEntry( p->vClasses, Vec_IntSize(p->vClasses) - 2 ); |
| nSize = Vec_IntEntry( p->vClasses, Vec_IntSize(p->vClasses) - 1 ); |
| Vec_IntShrink( p->vClasses, Vec_IntSize(p->vClasses) - 2 ); |
| |
| // assign the class |
| assert( nSize > 1 ); |
| if ( nSize == 2 ) |
| { |
| assert( p->pUniques[Gia_IsoGetItem(p, iBegin)] == 0 ); |
| p->pUniques[Gia_IsoGetItem(p, iBegin)] = p->nUniques++; |
| p->nSingles++; |
| p->nEntries--; |
| |
| assert( p->pUniques[Gia_IsoGetItem(p, iBegin+1)] == 0 ); |
| p->pUniques[Gia_IsoGetItem(p, iBegin+1)] = p->nUniques++; |
| p->nSingles++; |
| p->nEntries--; |
| } |
| else |
| { |
| assert( p->pUniques[Gia_IsoGetItem(p, iBegin)] == 0 ); |
| p->pUniques[Gia_IsoGetItem(p, iBegin)] = p->nUniques++; |
| p->nSingles++; |
| p->nEntries--; |
| } |
| printf( "Broke ties in last class of size %d at level %d.\n", nSize, p->pLevels[Gia_IsoGetItem(p, iBegin)] ); |
| } |
| |
| void Gia_IsoAssignOneClass( Gia_IsoMan_t * p, int fVerbose ) |
| { |
| int i, k, iBegin0, iBegin, nSize, Shrink; |
| // find the classes with the highest level |
| assert( Vec_IntSize(p->vClasses) > 0 ); |
| iBegin0 = Vec_IntEntry( p->vClasses, Vec_IntSize(p->vClasses) - 2 ); |
| for ( i = Vec_IntSize(p->vClasses) - 2; i >= 0; i -= 2 ) |
| { |
| iBegin = Vec_IntEntry( p->vClasses, i ); |
| if ( p->pLevels[Gia_IsoGetItem(p, iBegin)] != p->pLevels[Gia_IsoGetItem(p, iBegin0)] ) |
| break; |
| } |
| i += 2; |
| assert( i >= 0 ); |
| // assign all classes starting with this one |
| for ( Shrink = i; i < Vec_IntSize(p->vClasses); i += 2 ) |
| { |
| iBegin = Vec_IntEntry( p->vClasses, i ); |
| nSize = Vec_IntEntry( p->vClasses, i + 1 ); |
| for ( k = 0; k < nSize; k++ ) |
| { |
| assert( p->pUniques[Gia_IsoGetItem(p, iBegin+k)] == 0 ); |
| p->pUniques[Gia_IsoGetItem(p, iBegin+k)] = p->nUniques++; |
| // Gia_ManObj(p->pGia, Gia_IsoGetItem(p, iBegin+k))->Value += s_256Primes[0]; /// new addition!!! |
| p->nSingles++; |
| p->nEntries--; |
| } |
| if ( fVerbose ) |
| printf( "Broke ties in class of size %d at level %d.\n", nSize, p->pLevels[Gia_IsoGetItem(p, iBegin)] ); |
| } |
| Vec_IntShrink( p->vClasses, Shrink ); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Report topmost equiv nodes.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Gia_IsoReportTopmost( Gia_IsoMan_t * p ) |
| { |
| Gia_Obj_t * pObj; |
| int i, k, iBegin, nSize, Counter = 0; |
| // go through equivalence classes |
| Gia_ManIncrementTravId( p->pGia ); |
| Vec_IntForEachEntryDouble( p->vClasses, iBegin, nSize, i ) |
| { |
| // printf( "%d(%d) ", nSize, p->pLevels[Gia_IsoGetItem(p, iBegin)] ); |
| for ( k = 0; k < nSize; k++ ) |
| { |
| pObj = Gia_ManObj( p->pGia, Gia_IsoGetItem(p, iBegin+k) ); |
| if ( Gia_ObjIsAnd(pObj) ) |
| { |
| Gia_ObjSetTravIdCurrent( p->pGia, Gia_ObjFanin0(pObj) ); |
| Gia_ObjSetTravIdCurrent( p->pGia, Gia_ObjFanin1(pObj) ); |
| } |
| else if ( Gia_ObjIsRo(p->pGia, pObj) ) |
| Gia_ObjSetTravIdCurrent( p->pGia, Gia_ObjFanin0(Gia_ObjRoToRi(p->pGia, pObj)) ); |
| } |
| } |
| // printf( "\n" ); |
| |
| // report non-labeled nodes |
| Vec_IntForEachEntryDouble( p->vClasses, iBegin, nSize, i ) |
| { |
| for ( k = 0; k < nSize; k++ ) |
| { |
| pObj = Gia_ManObj( p->pGia, Gia_IsoGetItem(p, iBegin+k) ); |
| if ( !Gia_ObjIsTravIdCurrent(p->pGia, pObj) ) |
| { |
| printf( "%5d : ", ++Counter ); |
| printf( "Obj %6d : Level = %4d. iBegin = %4d. Size = %4d.\n", |
| Gia_ObjId(p->pGia, pObj), p->pLevels[Gia_ObjId(p->pGia, pObj)], iBegin, nSize ); |
| break; |
| } |
| } |
| } |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Gia_IsoRecognizeMuxes( Gia_Man_t * pGia ) |
| { |
| Gia_Obj_t * pObj, * pObjC, * pObj1, * pObj0; |
| int i; |
| Gia_ManForEachAnd( pGia, pObj, i ) |
| { |
| if ( !Gia_ObjIsMuxType(pObj) ) |
| continue; |
| pObjC = Gia_ObjRecognizeMux( pObj, &pObj1, &pObj0 ); |
| if ( Gia_Regular(pObj0) == Gia_Regular(pObj1) ) |
| { |
| // this is XOR |
| Gia_Regular(pObj)->Value += s_256Primes[233]; |
| Gia_Regular(pObjC)->Value += s_256Primes[234]; |
| Gia_Regular(pObj0)->Value += s_256Primes[234]; |
| } |
| else |
| { |
| // this is MUX |
| Gia_Regular(pObj)->Value += s_256Primes[235]; |
| Gia_Regular(pObjC)->Value += s_256Primes[236]; |
| Gia_Regular(pObj0)->Value += s_256Primes[237]; |
| Gia_Regular(pObj1)->Value += s_256Primes[237]; |
| } |
| } |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Vec_Ptr_t * Gia_IsoDeriveEquivPos( Gia_Man_t * pGia, int fForward, int fVerbose ) |
| { |
| int nIterMax = 10000; |
| int nFixedPoint = 1; |
| Gia_IsoMan_t * p; |
| Vec_Ptr_t * vEquivs = NULL; |
| int fRefined, fRefinedAll; |
| int i, c; |
| abctime clk = Abc_Clock(), clkTotal = Abc_Clock(); |
| assert( Gia_ManCiNum(pGia) > 0 ); |
| assert( Gia_ManPoNum(pGia) > 0 ); |
| |
| Gia_ManCleanValue( pGia ); |
| p = Gia_IsoManStart( pGia ); |
| Gia_IsoPrepare( p ); |
| Gia_IsoAssignUnique( p ); |
| p->timeStart = Abc_Clock() - clk; |
| if ( fVerbose ) |
| Gia_IsoPrint( p, 0, Abc_Clock() - clkTotal ); |
| |
| // Gia_IsoRecognizeMuxes( pGia ); |
| |
| i = 0; |
| if ( fForward ) |
| { |
| for ( c = 0; i < nIterMax && c < nFixedPoint+1; i++, c = fRefined ? 0 : c+1 ) |
| { |
| clk = Abc_Clock(); Gia_IsoSimulate( p, i ); p->timeSim += Abc_Clock() - clk; |
| clk = Abc_Clock(); fRefined = Gia_IsoSort( p ); p->timeRefine += Abc_Clock() - clk; |
| if ( fVerbose ) |
| Gia_IsoPrint( p, i+1, Abc_Clock() - clkTotal ); |
| } |
| } |
| else |
| { |
| while ( Vec_IntSize(p->vClasses) > 0 ) |
| { |
| for ( fRefinedAll = 1; i < nIterMax && fRefinedAll; ) |
| { |
| fRefinedAll = 0; |
| for ( c = 0; i < nIterMax && c < nFixedPoint+1; i++, c = fRefined ? 0 : c+1 ) |
| { |
| clk = Abc_Clock(); Gia_IsoSimulate( p, i ); p->timeSim += Abc_Clock() - clk; |
| clk = Abc_Clock(); fRefined = Gia_IsoSort( p ); p->timeRefine += Abc_Clock() - clk; |
| if ( fVerbose ) |
| Gia_IsoPrint( p, i+1, Abc_Clock() - clkTotal ); |
| fRefinedAll |= fRefined; |
| } |
| for ( c = 0; i < nIterMax && c < nFixedPoint+1; i++, c = fRefined ? 0 : c+1 ) |
| { |
| clk = Abc_Clock(); Gia_IsoSimulateBack( p, i ); p->timeSim += Abc_Clock() - clk; |
| clk = Abc_Clock(); fRefined = Gia_IsoSort( p ); p->timeRefine += Abc_Clock() - clk; |
| if ( fVerbose ) |
| Gia_IsoPrint( p, i+1, Abc_Clock() - clkTotal ); |
| fRefinedAll |= fRefined; |
| } |
| } |
| if ( !fRefinedAll ) |
| break; |
| } |
| |
| // Gia_IsoReportTopmost( p ); |
| |
| while ( Vec_IntSize(p->vClasses) > 0 ) |
| { |
| Gia_IsoAssignOneClass( p, fVerbose ); |
| for ( fRefinedAll = 1; i < nIterMax && fRefinedAll; ) |
| { |
| fRefinedAll = 0; |
| for ( c = 0; i < nIterMax && c < nFixedPoint; i++, c = fRefined ? 0 : c+1 ) |
| { |
| clk = Abc_Clock(); Gia_IsoSimulateBack( p, i ); p->timeSim += Abc_Clock() - clk; |
| clk = Abc_Clock(); fRefined = Gia_IsoSort( p ); p->timeRefine += Abc_Clock() - clk; |
| if ( fVerbose ) |
| Gia_IsoPrint( p, i+1, Abc_Clock() - clkTotal ); |
| fRefinedAll |= fRefined; |
| } |
| for ( c = 0; i < nIterMax && c < nFixedPoint; i++, c = fRefined ? 0 : c+1 ) |
| { |
| clk = Abc_Clock(); Gia_IsoSimulate( p, i ); p->timeSim += Abc_Clock() - clk; |
| clk = Abc_Clock(); fRefined = Gia_IsoSort( p ); p->timeRefine += Abc_Clock() - clk; |
| if ( fVerbose ) |
| Gia_IsoPrint( p, i+1, Abc_Clock() - clkTotal ); |
| fRefinedAll |= fRefined; |
| // if ( fRefined ) |
| // printf( "Refinedment happened.\n" ); |
| } |
| } |
| } |
| |
| if ( fVerbose ) |
| Gia_IsoPrint( p, i+2, Abc_Clock() - clkTotal ); |
| } |
| // Gia_IsoPrintClasses( p ); |
| if ( fVerbose ) |
| { |
| p->timeTotal = Abc_Clock() - clkTotal; |
| p->timeOther = p->timeTotal - p->timeStart - p->timeSim - p->timeRefine; |
| ABC_PRTP( "Start ", p->timeStart, p->timeTotal ); |
| ABC_PRTP( "Simulate ", p->timeSim, p->timeTotal ); |
| ABC_PRTP( "Refine ", p->timeRefine-p->timeSort, p->timeTotal ); |
| ABC_PRTP( "Sort ", p->timeSort, p->timeTotal ); |
| ABC_PRTP( "Other ", p->timeOther, p->timeTotal ); |
| ABC_PRTP( "TOTAL ", p->timeTotal, p->timeTotal ); |
| } |
| |
| if ( Gia_ManPoNum(p->pGia) > 1 ) |
| vEquivs = Gia_IsoCollectCosClasses( p, fVerbose ); |
| Gia_IsoManTransferUnique( p ); |
| Gia_IsoManStop( p ); |
| |
| return vEquivs; |
| } |
| |
| |
| |
| |
| /**Function************************************************************* |
| |
| Synopsis [Finds canonical ordering of CIs/COs/nodes.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Gia_ObjCompareByValue( Gia_Obj_t ** pp1, Gia_Obj_t ** pp2 ) |
| { |
| Gia_Obj_t * pObj1 = *pp1; |
| Gia_Obj_t * pObj2 = *pp2; |
| // assert( pObj1->Value != pObj2->Value ); |
| return (int)pObj1->Value - (int)pObj2->Value; |
| } |
| void Gia_ManFindCaninicalOrder_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vAnds ) |
| { |
| if ( Gia_ObjIsTravIdCurrent(p, pObj) ) |
| return; |
| Gia_ObjSetTravIdCurrent(p, pObj); |
| assert( Gia_ObjIsAnd(pObj) ); |
| if ( !Gia_ObjIsAnd(Gia_ObjFanin0(pObj)) || !Gia_ObjIsAnd(Gia_ObjFanin1(pObj)) ) |
| { |
| Gia_ManFindCaninicalOrder_rec( p, Gia_ObjFanin0(pObj), vAnds ); |
| Gia_ManFindCaninicalOrder_rec( p, Gia_ObjFanin1(pObj), vAnds ); |
| } |
| else |
| { |
| assert( Gia_ObjFanin0(pObj)->Value != Gia_ObjFanin1(pObj)->Value ); |
| if ( Gia_ObjFanin0(pObj)->Value < Gia_ObjFanin1(pObj)->Value ) |
| { |
| Gia_ManFindCaninicalOrder_rec( p, Gia_ObjFanin0(pObj), vAnds ); |
| Gia_ManFindCaninicalOrder_rec( p, Gia_ObjFanin1(pObj), vAnds ); |
| } |
| else |
| { |
| Gia_ManFindCaninicalOrder_rec( p, Gia_ObjFanin1(pObj), vAnds ); |
| Gia_ManFindCaninicalOrder_rec( p, Gia_ObjFanin0(pObj), vAnds ); |
| } |
| } |
| Vec_IntPush( vAnds, Gia_ObjId(p, pObj) ); |
| } |
| void Gia_ManFindCaninicalOrder( Gia_Man_t * p, Vec_Int_t * vCis, Vec_Int_t * vAnds, Vec_Int_t * vCos, Vec_Int_t ** pvPiPerm ) |
| { |
| Vec_Ptr_t * vTemp; |
| Gia_Obj_t * pObj; |
| int i; |
| |
| vTemp = Vec_PtrAlloc( 1000 ); |
| Vec_IntClear( vCis ); |
| Vec_IntClear( vAnds ); |
| Vec_IntClear( vCos ); |
| |
| // assign unique IDs to PIs |
| Vec_PtrClear( vTemp ); |
| Gia_ManForEachPi( p, pObj, i ) |
| Vec_PtrPush( vTemp, pObj ); |
| Vec_PtrSort( vTemp, (int (*)(void))Gia_ObjCompareByValue ); |
| // create the result |
| Vec_PtrForEachEntry( Gia_Obj_t *, vTemp, pObj, i ) |
| Vec_IntPush( vCis, Gia_ObjId(p, pObj) ); |
| // remember PI permutation |
| if ( pvPiPerm ) |
| { |
| *pvPiPerm = Vec_IntAlloc( Gia_ManPiNum(p) ); |
| Vec_PtrForEachEntry( Gia_Obj_t *, vTemp, pObj, i ) |
| Vec_IntPush( *pvPiPerm, Gia_ObjCioId(pObj) ); |
| } |
| |
| // assign unique IDs to POs |
| if ( Gia_ManPoNum(p) == 1 ) |
| Vec_IntPush( vCos, Gia_ObjId(p, Gia_ManPo(p, 0)) ); |
| else |
| { |
| Vec_PtrClear( vTemp ); |
| Gia_ManForEachPo( p, pObj, i ) |
| { |
| pObj->Value = Abc_Var2Lit( Gia_ObjFanin0(pObj)->Value, Gia_ObjFaninC0(pObj) ); |
| Vec_PtrPush( vTemp, pObj ); |
| } |
| Vec_PtrSort( vTemp, (int (*)(void))Gia_ObjCompareByValue ); |
| Vec_PtrForEachEntry( Gia_Obj_t *, vTemp, pObj, i ) |
| Vec_IntPush( vCos, Gia_ObjId(p, pObj) ); |
| } |
| |
| // assign unique IDs to ROs |
| Vec_PtrClear( vTemp ); |
| Gia_ManForEachRo( p, pObj, i ) |
| Vec_PtrPush( vTemp, pObj ); |
| Vec_PtrSort( vTemp, (int (*)(void))Gia_ObjCompareByValue ); |
| // create the result |
| Vec_PtrForEachEntry( Gia_Obj_t *, vTemp, pObj, i ) |
| { |
| Vec_IntPush( vCis, Gia_ObjId(p, pObj) ); |
| Vec_IntPush( vCos, Gia_ObjId(p, Gia_ObjRoToRi(p, pObj)) ); |
| } |
| Vec_PtrFree( vTemp ); |
| |
| // assign unique IDs to internal nodes |
| Gia_ManIncrementTravId( p ); |
| Gia_ObjSetTravIdCurrent( p, Gia_ManConst0(p) ); |
| Gia_ManForEachObjVec( vCis, p, pObj, i ) |
| Gia_ObjSetTravIdCurrent( p, pObj ); |
| Gia_ManForEachObjVec( vCos, p, pObj, i ) |
| Gia_ManFindCaninicalOrder_rec( p, Gia_ObjFanin0(pObj), vAnds ); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Gia_Man_t * Gia_ManIsoCanonicize( Gia_Man_t * p, int fVerbose ) |
| { |
| Gia_Man_t * pRes = NULL; |
| Vec_Int_t * vCis, * vAnds, * vCos; |
| Vec_Ptr_t * vEquiv; |
| if ( Gia_ManCiNum(p) == 0 ) // const AIG |
| { |
| assert( Gia_ManPoNum(p) == 1 ); |
| assert( Gia_ManObjNum(p) == 2 ); |
| return Gia_ManDup(p); |
| } |
| // derive canonical values |
| vEquiv = Gia_IsoDeriveEquivPos( p, 0, fVerbose ); |
| Vec_VecFreeP( (Vec_Vec_t **)&vEquiv ); |
| // find canonical order of CIs/COs/nodes |
| // find canonical order |
| vCis = Vec_IntAlloc( Gia_ManCiNum(p) ); |
| vAnds = Vec_IntAlloc( Gia_ManAndNum(p) ); |
| vCos = Vec_IntAlloc( Gia_ManCoNum(p) ); |
| Gia_ManFindCaninicalOrder( p, vCis, vAnds, vCos, NULL ); |
| // derive the new AIG |
| pRes = Gia_ManDupFromVecs( p, vCis, vAnds, vCos, Gia_ManRegNum(p) ); |
| // cleanup |
| Vec_IntFree( vCis ); |
| Vec_IntFree( vAnds ); |
| Vec_IntFree( vCos ); |
| return pRes; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Vec_Str_t * Gia_ManIsoFindString( Gia_Man_t * p, int iPo, int fVerbose, Vec_Int_t ** pvPiPerm ) |
| { |
| Gia_Man_t * pPart; |
| Vec_Ptr_t * vEquiv; |
| Vec_Int_t * vCis, * vAnds, * vCos; |
| Vec_Str_t * vStr; |
| // duplicate |
| pPart = Gia_ManDupCones( p, &iPo, 1, 1 ); |
| //Gia_ManPrint( pPart ); |
| assert( Gia_ManPoNum(pPart) == 1 ); |
| if ( Gia_ManCiNum(pPart) == 0 ) // const AIG |
| { |
| assert( Gia_ManPoNum(pPart) == 1 ); |
| assert( Gia_ManObjNum(pPart) == 2 ); |
| vStr = Gia_AigerWriteIntoMemoryStr( pPart ); |
| Gia_ManStop( pPart ); |
| if ( pvPiPerm ) |
| *pvPiPerm = Vec_IntAlloc( 0 ); |
| return vStr; |
| } |
| // derive canonical values |
| vEquiv = Gia_IsoDeriveEquivPos( pPart, 0, fVerbose ); |
| Vec_VecFreeP( (Vec_Vec_t **)&vEquiv ); |
| // find canonical order |
| vCis = Vec_IntAlloc( Gia_ManCiNum(pPart) ); |
| vAnds = Vec_IntAlloc( Gia_ManAndNum(pPart) ); |
| vCos = Vec_IntAlloc( Gia_ManCoNum(pPart) ); |
| Gia_ManFindCaninicalOrder( pPart, vCis, vAnds, vCos, pvPiPerm ); |
| //printf( "Internal: " ); |
| //Vec_IntPrint( vCis ); |
| // derive the AIGER string |
| vStr = Gia_AigerWriteIntoMemoryStrPart( pPart, vCis, vAnds, vCos, Gia_ManRegNum(pPart) ); |
| // cleanup |
| Vec_IntFree( vCis ); |
| Vec_IntFree( vAnds ); |
| Vec_IntFree( vCos ); |
| Gia_ManStop( pPart ); |
| return vStr; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Vec_IntCountNonTrivial( Vec_Ptr_t * vEquivs, int * pnUsed ) |
| { |
| Vec_Int_t * vClass; |
| int i, nClasses = 0; |
| *pnUsed = 0; |
| Vec_PtrForEachEntry( Vec_Int_t *, vEquivs, vClass, i ) |
| { |
| if ( Vec_IntSize(vClass) < 2 ) |
| continue; |
| nClasses++; |
| (*pnUsed) += Vec_IntSize(vClass); |
| } |
| return nClasses; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Gia_Man_t * Gia_ManIsoReduce( Gia_Man_t * pInit, Vec_Ptr_t ** pvPosEquivs, Vec_Ptr_t ** pvPiPerms, int fEstimate, int fDualOut, int fVerbose, int fVeryVerbose ) |
| { |
| Gia_Man_t * p, * pPart; |
| Vec_Ptr_t * vEquivs, * vEquivs2, * vStrings; |
| Vec_Int_t * vRemain, * vLevel, * vLevel2; |
| Vec_Str_t * vStr, * vStr2; |
| int i, k, s, sStart, iPo, Counter; |
| int nClasses, nUsedPos; |
| abctime clk = Abc_Clock(); |
| if ( pvPosEquivs ) |
| *pvPosEquivs = NULL; |
| if ( pvPiPerms ) |
| *pvPiPerms = Vec_PtrStart( Gia_ManPoNum(pInit) ); |
| |
| if ( fDualOut ) |
| { |
| assert( (Gia_ManPoNum(pInit) & 1) == 0 ); |
| if ( Gia_ManPoNum(pInit) == 2 ) |
| return Gia_ManDup(pInit); |
| p = Gia_ManTransformMiter( pInit ); |
| p = Gia_ManSeqStructSweep( pPart = p, 1, 1, 0 ); |
| Gia_ManStop( pPart ); |
| } |
| else |
| { |
| if ( Gia_ManPoNum(pInit) == 1 ) |
| return Gia_ManDup(pInit); |
| p = pInit; |
| } |
| |
| // create preliminary equivalences |
| vEquivs = Gia_IsoDeriveEquivPos( p, 1, fVeryVerbose ); |
| if ( vEquivs == NULL ) |
| { |
| if ( fDualOut ) |
| Gia_ManStop( p ); |
| return NULL; |
| } |
| nClasses = Vec_IntCountNonTrivial( vEquivs, &nUsedPos ); |
| printf( "Reduced %d outputs to %d candidate classes (%d outputs are in %d non-trivial classes). ", |
| Gia_ManPoNum(p), Vec_PtrSize(vEquivs), nUsedPos, nClasses ); |
| Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); |
| if ( fEstimate ) |
| { |
| Vec_VecFree( (Vec_Vec_t *)vEquivs ); |
| return Gia_ManDup(pInit); |
| } |
| |
| // perform refinement of equivalence classes |
| Counter = 0; |
| vEquivs2 = Vec_PtrAlloc( 100 ); |
| Vec_PtrForEachEntry( Vec_Int_t *, vEquivs, vLevel, i ) |
| { |
| if ( Vec_IntSize(vLevel) < 2 ) |
| { |
| Vec_PtrPush( vEquivs2, Vec_IntDup(vLevel) ); |
| for ( k = 0; k < Vec_IntSize(vLevel); k++ ) |
| if ( ++Counter % 100 == 0 ) |
| printf( "%6d finished...\r", Counter ); |
| continue; |
| } |
| |
| if ( fVerbose ) |
| { |
| iPo = Vec_IntEntry(vLevel, 0); |
| printf( "%6d %6d %6d : ", i, Vec_IntSize(vLevel), iPo ); |
| pPart = Gia_ManDupCones( p, &iPo, 1, 1 ); |
| Gia_ManPrintStats(pPart, NULL); |
| Gia_ManStop( pPart ); |
| } |
| |
| sStart = Vec_PtrSize( vEquivs2 ); |
| vStrings = Vec_PtrAlloc( 100 ); |
| Vec_IntForEachEntry( vLevel, iPo, k ) |
| { |
| if ( ++Counter % 100 == 0 ) |
| printf( "%6d finished...\r", Counter ); |
| assert( pvPiPerms == NULL || Vec_PtrArray(*pvPiPerms)[iPo] == NULL ); |
| vStr = Gia_ManIsoFindString( p, iPo, 0, pvPiPerms ? (Vec_Int_t **)Vec_PtrArray(*pvPiPerms) + iPo : NULL ); |
| |
| // printf( "Output %2d : ", iPo ); |
| // Vec_IntPrint( Vec_PtrArray(*pvPiPerms)[iPo] ); |
| |
| // check if this string already exists |
| Vec_PtrForEachEntry( Vec_Str_t *, vStrings, vStr2, s ) |
| if ( Vec_StrCompareVec(vStr, vStr2) == 0 ) |
| break; |
| if ( s == Vec_PtrSize(vStrings) ) |
| { |
| Vec_PtrPush( vStrings, vStr ); |
| Vec_PtrPush( vEquivs2, Vec_IntAlloc(8) ); |
| } |
| else |
| Vec_StrFree( vStr ); |
| // add this entry to the corresponding level |
| vLevel2 = (Vec_Int_t *)Vec_PtrEntry( vEquivs2, sStart + s ); |
| Vec_IntPush( vLevel2, iPo ); |
| } |
| // if ( Vec_PtrSize(vEquivs2) - sStart > 1 ) |
| // printf( "Refined class %d into %d classes.\n", i, Vec_PtrSize(vEquivs2) - sStart ); |
| Vec_VecFree( (Vec_Vec_t *)vStrings ); |
| } |
| assert( Counter == Gia_ManPoNum(p) ); |
| Vec_VecSortByFirstInt( (Vec_Vec_t *)vEquivs2, 0 ); |
| Vec_VecFree( (Vec_Vec_t *)vEquivs ); |
| vEquivs = vEquivs2; |
| |
| // collect the first ones |
| vRemain = Vec_IntAlloc( 100 ); |
| Vec_PtrForEachEntry( Vec_Int_t *, vEquivs, vLevel, i ) |
| Vec_IntPush( vRemain, Vec_IntEntry(vLevel, 0) ); |
| |
| if ( fDualOut ) |
| { |
| Vec_Int_t * vTemp = Vec_IntAlloc( Vec_IntSize(vRemain) ); |
| int i, Entry; |
| Vec_IntForEachEntry( vRemain, Entry, i ) |
| { |
| // printf( "%d ", Entry ); |
| Vec_IntPush( vTemp, 2*Entry ); |
| Vec_IntPush( vTemp, 2*Entry+1 ); |
| } |
| // printf( "\n" ); |
| Vec_IntFree( vRemain ); |
| vRemain = vTemp; |
| Gia_ManStop( p ); |
| p = pInit; |
| } |
| |
| |
| // derive the resulting AIG |
| pPart = Gia_ManDupCones( p, Vec_IntArray(vRemain), Vec_IntSize(vRemain), 0 ); |
| Vec_IntFree( vRemain ); |
| // report the results |
| nClasses = Vec_IntCountNonTrivial( vEquivs, &nUsedPos ); |
| if ( !fDualOut ) |
| printf( "Reduced %d outputs to %d equivalence classes (%d outputs are in %d non-trivial classes). ", |
| Gia_ManPoNum(p), Vec_PtrSize(vEquivs), nUsedPos, nClasses ); |
| else |
| printf( "Reduced %d dual outputs to %d dual outputs. ", Gia_ManPoNum(p)/2, Gia_ManPoNum(pPart)/2 ); |
| Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); |
| if ( fVerbose ) |
| { |
| printf( "Nontrivial classes:\n" ); |
| Vec_VecPrintInt( (Vec_Vec_t *)vEquivs, 1 ); |
| } |
| if ( pvPosEquivs ) |
| *pvPosEquivs = vEquivs; |
| else |
| Vec_VecFree( (Vec_Vec_t *)vEquivs ); |
| // Gia_ManStopP( &pPart ); |
| return pPart; |
| } |
| |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Gia_IsoTestOld( Gia_Man_t * p, int fVerbose ) |
| { |
| Vec_Ptr_t * vEquivs; |
| abctime clk = Abc_Clock(); |
| vEquivs = Gia_IsoDeriveEquivPos( p, 0, fVerbose ); |
| printf( "Reduced %d outputs to %d. ", Gia_ManPoNum(p), vEquivs ? Vec_PtrSize(vEquivs) : 1 ); |
| Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); |
| if ( fVerbose && vEquivs && Gia_ManPoNum(p) != Vec_PtrSize(vEquivs) ) |
| { |
| printf( "Nontrivial classes:\n" ); |
| // Vec_VecPrintInt( (Vec_Vec_t *)vEquivs, 1 ); |
| } |
| Vec_VecFreeP( (Vec_Vec_t **)&vEquivs ); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Test remapping of CEXes for isomorphic POs.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Vec_Int_t * Gia_IsoTestGenPerm( int nPis ) |
| { |
| Vec_Int_t * vPerm; |
| int i, * pArray; |
| vPerm = Vec_IntStartNatural( nPis ); |
| pArray = Vec_IntArray( vPerm ); |
| for ( i = 0; i < nPis; i++ ) |
| { |
| int iNew = rand() % nPis; |
| ABC_SWAP( int, pArray[i], pArray[iNew] ); |
| } |
| return vPerm; |
| } |
| void Gia_IsoTest( Gia_Man_t * p, Abc_Cex_t * pCex, int fVerbose ) |
| { |
| Abc_Cex_t * pCexNew; |
| Vec_Int_t * vPiPerm; |
| Vec_Ptr_t * vPosEquivs, * vPisPerm; |
| Vec_Int_t * vPerm0, * vPerm1; |
| Gia_Man_t * pPerm, * pDouble, * pAig; |
| assert( Gia_ManPoNum(p) == 1 ); |
| assert( Gia_ManRegNum(p) > 0 ); |
| // generate random permutation of PIs |
| vPiPerm = Gia_IsoTestGenPerm( Gia_ManPiNum(p) ); |
| printf( "Considering random permutation of the primary inputs of the AIG:\n" ); |
| Vec_IntPrint( vPiPerm ); |
| // create AIG with two primary outputs (original and permuted) |
| pPerm = Gia_ManDupPerm( p, vPiPerm ); |
| pDouble = Gia_ManDupAppendNew( p, pPerm ); |
| //Gia_AigerWrite( pDouble, "test.aig", 0, 0 ); |
| |
| // analyze the two-output miter |
| pAig = Gia_ManIsoReduce( pDouble, &vPosEquivs, &vPisPerm, 0, 0, 0, 0 ); |
| Vec_VecFree( (Vec_Vec_t *)vPosEquivs ); |
| |
| // given CEX for output 0, derive CEX for output 1 |
| vPerm0 = (Vec_Int_t *)Vec_PtrEntry( vPisPerm, 0 ); |
| vPerm1 = (Vec_Int_t *)Vec_PtrEntry( vPisPerm, 1 ); |
| pCexNew = Abc_CexPermuteTwo( pCex, vPerm0, vPerm1 ); |
| Vec_VecFree( (Vec_Vec_t *)vPisPerm ); |
| |
| // check that original CEX and the resulting CEX is valid |
| if ( Gia_ManVerifyCex(p, pCex, 0) ) |
| printf( "CEX for the init AIG is valid.\n" ); |
| else |
| printf( "CEX for the init AIG is not valid.\n" ); |
| if ( Gia_ManVerifyCex(pPerm, pCexNew, 0) ) |
| printf( "CEX for the perm AIG is valid.\n" ); |
| else |
| printf( "CEX for the perm AIG is not valid.\n" ); |
| // delete |
| Gia_ManStop( pAig ); |
| Gia_ManStop( pDouble ); |
| Gia_ManStop( pPerm ); |
| Vec_IntFree( vPiPerm ); |
| Abc_CexFree( pCexNew ); |
| } |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// END OF FILE /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| |
| ABC_NAMESPACE_IMPL_END |
| |
