/**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 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