From 7ca9c116df0475d567d6fbc616b454f40a44003c Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sat, 18 Feb 2012 19:20:02 -0800 Subject: Isomorphism checking code. --- src/aig/gia/giaIso.c | 1230 +++++++++++++------------------------------- src/aig/saig/saigIsoSlow.c | 182 ++++++- src/base/abci/abc.c | 8 +- 3 files changed, 542 insertions(+), 878 deletions(-) diff --git a/src/aig/gia/giaIso.c b/src/aig/gia/giaIso.c index 8359146c..cabad6ba 100644 --- a/src/aig/gia/giaIso.c +++ b/src/aig/gia/giaIso.c @@ -23,6 +23,78 @@ 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 +}; +static int s_256Primes2[ISO_MASK+1] = +{ + 0xcaa57efb,0x64bd4878,0x3419334a,0x712e5f6b,0x9fa9d687,0x06f8645f,0x620ca96f,0xdc5d6cce, + 0x392f3257,0x52140f06,0xc4b3bda4,0xe8c7eba7,0x066bd754,0xc5941f26,0xe6dfd573,0x328dd14d, + 0xb1cb4ba7,0x1d37a9b8,0x96a195a5,0x970e535a,0x290351b8,0x570000f6,0xe14ae341,0x35ede6a6, + 0x9a02f032,0xaf2ebb58,0x146be492,0x670b3e4b,0x72fa6cfd,0xa243af97,0xbbd5fc21,0xcb8852a2, + 0x5d5b4a42,0xeefff0ac,0xa59ad1b6,0x3ec55544,0x48d64f69,0x9065d3d0,0xdd09485b,0xdd63bd09, + 0x605e811d,0xc4b4ed7d,0xb0b58558,0x0644400b,0x12222346,0x086f146a,0xad6dee36,0x5488d1a3, + 0x0c93bc0c,0x18555d92,0x9f4427bf,0xa590a66a,0x3a630fda,0xf1681c2e,0x948a16fb,0x16fe3338, + 0xc9832357,0xd1e8e6b5,0xd9cfe034,0x05b22f26,0x27233c6e,0x355890e1,0xfbe6eaf3,0x0dcd8e8f, + 0x00b5df46,0xd97730ac,0xc6dfd8ff,0x0cb1840a,0x41e9d249,0xbb471b4e,0x480b8f63,0x1ffe8871, + 0x17b11821,0x1709e440,0xcefb3668,0xa4954ddd,0xf03ef8b5,0x6b3e633c,0xe5813096,0x3697c9a6, + 0x7800f52f,0x73a7aa39,0x59ac23b7,0xb4663166,0x9ca9d6f8,0x2d441072,0x38cef3d3,0x39a3faf6, + 0x89299fb9,0xd558295f,0xcf79c633,0x232dd96e,0xadb2955b,0xe962cbb9,0xab7c0061,0x1027c329, + 0xb4b43e07,0x25240a7a,0x98ea4825,0xdbf2edbd,0x8be15d26,0x879f3cd9,0xa4138089,0xa32dcb06, + 0x602af961,0x4b13f451,0x1c87d0d5,0xc3bb141b,0x9ebf55a1,0xef030a9a,0x8d199b93,0xdabcbb56, + 0xf412f80f,0x302e90ad,0xc4d9878b,0xc392f650,0x4fd3a614,0x0a96ddc4,0xcd1878c7,0x9ddd3ae1, + 0xdaf46458,0xba7c8656,0xf667948f,0xc37e3c23,0x04a577c6,0xbe615f1e,0xcc97406c,0xd497f16f, + 0x79586586,0xd2057d14,0x1bb92028,0xab888e5e,0x26bef100,0xf46b3671,0xf21f1acc,0x67f288c8, + 0x39c722df,0x61d21eaf,0x9c5853a0,0x63b693c7,0x1ea53c0a,0x95bc0a85,0xa7372f2d,0x3ef6a6b3, + 0x82c9c4ac,0x4dea10ee,0xdfcb543d,0xd412f427,0x53e27f2c,0x875d8422,0x5367a7d8,0x41acf3fa, + 0xbce47234,0x8056fb9a,0x4e9a4c48,0xe4a45945,0x2cfee3ae,0xb4554b10,0x5e37a915,0x591b1963, + 0x4fa255c1,0xe01c897b,0x504e6208,0x7c7368eb,0x13808fd7,0x02ac0816,0x30305d2c,0x6c4bbdb7, + 0xa48a9599,0x57466059,0x4c6ebfc7,0x8587ccdf,0x6ff0abf0,0x5b6b63fe,0x31d9ec64,0x63458abd, + 0x21245905,0xccdb28fc,0xac828acb,0xe5e82bea,0xa7d76141,0xa699038e,0xcaba7e06,0x2710253f, + 0x2ff9c94d,0x26e48a2c,0xd713ec5e,0x869f2ed4,0x25bcd712,0xcb3e918f,0x615c3a5a,0x9fb43903, + 0x37900eb9,0x4f682db0,0x35a80dc6,0x4eb27c65,0x502735ab,0xb163b4c8,0x604649a8,0xb23a6cd3, + 0x9f715091,0x2e6fbb51,0x2ec9144b,0x272cbe65,0x90a0a453,0x420e1503,0x2d00d338,0x4aa96675, + 0xd025b61c,0xab02d9d7,0x2afe2a37,0xf8129b9b,0x4db04c54,0x654a5c06,0x3213ff51,0x4e09d0b1, + 0x333369a3,0xae27310a,0x91d076d0,0xa96ebcd0,0xefde54f4,0x021c309a,0xd506f53d,0xa5635251, + 0x2f23916e,0x1fe86bb1,0xcbc62160,0x2147c8cc,0xdeb3e47c,0x028e3987,0x8061de42,0x39be931b, + 0x2b7e54c5,0xe64d2f96,0x4069522d,0x4aa66857,0x83b62634,0x4ba72095,0x9aade2a9,0xf1223cd9, + 0x91cbddf0,0xec5d237f,0x593f3280,0x0b924439,0x446f4063,0xc66f8d8c,0x8b7128ba,0xb597f451, + 0xc8925236,0x1720f235,0x7cd2e9a0,0x4c130339,0x8a665a52,0x5bef2733,0xba35d9bc,0x6d26644c +}; + //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// @@ -33,40 +105,24 @@ struct Gia_IsoMan_t_ Gia_Man_t * pGia; int nObjs; int nUniques; - // collected info - Vec_Int_t * vLevels; - Vec_Int_t * vFin0Levs; - Vec_Int_t * vFin1Levs; - Vec_Int_t * vFinSig; - Vec_Int_t * vFoutPos; - Vec_Int_t * vFoutNeg; - // sorting structures - Vec_Int_t * vMap; - Vec_Int_t * vSeens; - Vec_Int_t * vCounts; - Vec_Int_t * vResult; - // fanout representation - Vec_Int_t * vFanout; - Vec_Int_t * vFanout2; - // class representation - Vec_Int_t * vItems; - Vec_Int_t * vUniques; - Vec_Int_t * vClass; - Vec_Int_t * vClass2; - Vec_Int_t * vClassNew; - Vec_Int_t * vLevelLim; - // temporary storage - Vec_Ptr_t * vRoots; - Vec_Int_t * vUsed; - Vec_Int_t * vRefs; - // results - Vec_Ptr_t * vResults; - Vec_Int_t * vPermCis; - Vec_Int_t * vPermCos; + 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; }; -static inline int * Gia_IsoFanoutVec( Vec_Int_t * p, int Id ) { return Vec_IntEntryP( p, Vec_IntEntry(p, Id) ); } +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 /// @@ -74,249 +130,76 @@ static inline int * Gia_IsoFanoutVec( Vec_Int_t * p, int Id ) { return Vec_Int /**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 ); - // collected info - p->vLevels = Vec_IntAlloc( p->nObjs ); - p->vFin0Levs = Vec_IntAlloc( p->nObjs ); - p->vFin1Levs = Vec_IntAlloc( p->nObjs ); - p->vFinSig = Vec_IntAlloc( p->nObjs ); - p->vFoutPos = Vec_IntAlloc( p->nObjs ); - p->vFoutNeg = Vec_IntAlloc( p->nObjs ); - // sorting structures - p->vMap = Vec_IntStartFull( 2*p->nObjs ); - p->vSeens = Vec_IntAlloc( p->nObjs ); - p->vCounts = Vec_IntAlloc( p->nObjs ); - p->vResult = Vec_IntAlloc( p->nObjs ); - // class representation - p->vItems = Vec_IntAlloc( p->nObjs ); - p->vUniques = Vec_IntAlloc( p->nObjs ); - p->vClass = Vec_IntAlloc( p->nObjs/2 ); - p->vClass2 = Vec_IntAlloc( p->nObjs/2 ); - p->vClassNew = Vec_IntAlloc( p->nObjs/2 ); - p->vLevelLim = Vec_IntAlloc( 1000 ); - // fanout representation - p->vFanout = Vec_IntAlloc( 6 * p->nObjs ); - p->vFanout2 = Vec_IntAlloc( 0 ); - // temporary storage - p->vRoots = Vec_PtrAlloc( 1000 ); - p->vUsed = Vec_IntAlloc( p->nObjs ); - p->vRefs = Vec_IntAlloc( p->nObjs ); - // results - p->vResults = Vec_PtrAlloc( Gia_ManPoNum(pGia) ); - p->vPermCis = Vec_IntAlloc( Gia_ManCiNum(pGia) ); - p->vPermCos = Vec_IntAlloc( Gia_ManCoNum(pGia) ); - return p; -} -void Gia_IsoManStop( Gia_IsoMan_t * p ) -{ - // collected info - Vec_IntFree( p->vLevels ); - Vec_IntFree( p->vFin0Levs ); - Vec_IntFree( p->vFin1Levs ); - Vec_IntFree( p->vFinSig ); - Vec_IntFree( p->vFoutPos ); - Vec_IntFree( p->vFoutNeg ); - // sorting structures - Vec_IntFree( p->vMap ); - Vec_IntFree( p->vSeens ); - Vec_IntFree( p->vCounts ); - Vec_IntFree( p->vResult ); - // class representation - Vec_IntFree( p->vItems ); - Vec_IntFree( p->vUniques ); - Vec_IntFree( p->vClass ); - Vec_IntFree( p->vClass2 ); - Vec_IntFree( p->vClassNew ); - Vec_IntFree( p->vLevelLim ); - // fanout representation - Vec_IntFree( p->vFanout ); - Vec_IntFree( p->vFanout2 ); - // temporary storage - Vec_IntFree( p->vRefs ); - Vec_IntFree( p->vUsed ); - Vec_PtrFree( p->vRoots ); - // results -// Vec_PtrFree( p->vResults ); - Vec_IntFree( p->vPermCis ); - Vec_IntFree( p->vPermCos ); - ABC_FREE( p ); -} - - -/**Function************************************************************* + Synopsis [QuickSort algorithm based on 3-way partitioning.] - Synopsis [Collect the nodes used for the given PO.] + Description [This code is based on the online presentation + "QuickSort is Optimal" by Robert Sedgewick and Jon Bentley. + http://www.sorting-algorithms.com/static/QuicksortIsOptimal.pdf - Description [Includes Const0, CI and AND nodes, no COs.] + The first 32-bits of the input data contain values to be compared. + The last 32-bits contain the user's data. When sorting is finished, + the 64-bit words are ordered in the increasing order of their value ] SideEffects [] SeeAlso [] ***********************************************************************/ -void Gia_IsoCleanUsed( Gia_Man_t * p, Vec_Int_t * vUsed ) +#define ISO_SWAP(Type, a, b) { Type t = a; a = b; b = t; } +static inline void Iso_SelectSort( word * pData, int nSize ) { - Gia_Obj_t * pObj; - int i; - Gia_ManForEachObjVec( vUsed, p, pObj, i ) - pObj->Value = 0; -} -void Gia_IsoCollectUsed_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vUsed, Vec_Ptr_t * vRoots ) -{ - if ( pObj->Value ) - return; - if ( Gia_ObjIsAnd(pObj) ) + int i, j, best_i; + for ( i = 0; i < nSize-1; i++ ) { - Gia_IsoCollectUsed_rec( p, Gia_ObjFanin0(pObj), vUsed, vRoots ); - Gia_IsoCollectUsed_rec( p, Gia_ObjFanin1(pObj), vUsed, vRoots ); + best_i = i; + for ( j = i+1; j < nSize; j++ ) + if ( (unsigned)pData[j] < (unsigned)pData[best_i] ) + best_i = j; + ISO_SWAP( word, pData[i], pData[best_i] ); } - else if ( Gia_ObjIsRo(p, pObj) ) - Vec_PtrPush( vRoots, Gia_ObjRoToRi(p, pObj) ); - else if ( !Gia_ObjIsPi(p, pObj) ) - assert( 0 ); - pObj->Value = Vec_IntSize( vUsed ); - Vec_IntPush( vUsed, Gia_ObjId(p, pObj) ); } -void Gia_IsoCollectUsed( Gia_Man_t * p, int iPo, Vec_Int_t * vUsed, Vec_Ptr_t * vRoots ) +void Iso_QuickSort_rec( word * pData, int l, int r ) { - Gia_Obj_t * pObj; - int i; - assert( iPo >= 0 && iPo < Gia_ManPoNum(p) ); - Vec_PtrClear( vRoots ); - Vec_PtrPush( vRoots, Gia_ManPo(p, iPo) ); - // collect used nodes - Vec_IntClear( vUsed ); - Vec_IntPush( vUsed, 0 ); - Vec_PtrForEachEntry( Gia_Obj_t *, vRoots, pObj, i ) - if ( !Gia_ObjIsConst0(Gia_ObjFanin0(pObj)) ) - Gia_IsoCollectUsed_rec( p, Gia_ObjFanin0(pObj), vUsed, vRoots ); -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Gia_IsoCreateFanout( Gia_Man_t * p, Vec_Int_t * vUsed, Vec_Int_t * vRefs, Vec_Int_t * vFanout ) -{ - // Value of GIA objects points to the index in Used - // vUsed includes only CIs and ANDs - Gia_Obj_t * pObj, * pObjRi; - int * pOff, * pOff0, * pOff1; - int i, nOffset, Counter = 0; - - // count references - Vec_IntFill( vRefs, Vec_IntSize(vUsed), 0 ); - Gia_ManForEachObjVec( vUsed, p, pObj, i ) - { - if ( !i ) continue; - if ( Gia_ObjIsAnd(pObj) ) - { - Vec_IntAddToEntry( vRefs, Gia_ObjFanin0(pObj)->Value, 1 ); - Vec_IntAddToEntry( vRefs, Gia_ObjFanin1(pObj)->Value, 1 ); - Counter += 2; - } - else if ( Gia_ObjIsRo(p, pObj) ) - { - pObj = Gia_ObjRoToRi(p, pObj); - Vec_IntAddToEntry( vRefs, Gia_ObjFanin0(pObj)->Value, 1 ); - Counter += 1; - } - else if ( !Gia_ObjIsPi(p, pObj) ) - assert( 0 ); - } - - // create fanout - nOffset = Vec_IntSize(vUsed); - Vec_IntGrowResize( vFanout, 2 * Vec_IntSize(vUsed) + 2 * Counter ); - Gia_ManForEachObjVec( vUsed, p, pObj, i ) - { - Vec_IntWriteEntry( vFanout, i, nOffset ); - Vec_IntWriteEntry( vFanout, nOffset, 0 ); - nOffset += 1 + Vec_IntEntry(vRefs, pObj->Value); - if ( Gia_ObjIsAnd(pObj) ) - nOffset += 2; - else if ( Gia_ObjIsRo(p, pObj) ) - nOffset += 1; - } - assert( nOffset == 2 * Vec_IntSize(vUsed) + 2 * Counter ); - - // load fanout - Gia_ManForEachObjVec( vUsed, p, pObj, i ) + word v = pData[r]; + int k, i = l-1, j = r, p = l-1, q = r; + if ( l >= r ) + return; + assert( l < r ); + if ( r - l < 10 ) { - pOff = Vec_IntEntryP( vFanout, Vec_IntEntry(vFanout, pObj->Value) ); - if ( Gia_ObjIsAnd(pObj) ) - { - pOff0 = Gia_IsoFanoutVec( vFanout, Gia_ObjFanin0(pObj)->Value ); - pOff1 = Gia_IsoFanoutVec( vFanout, Gia_ObjFanin1(pObj)->Value ); - pOff[1+(*pOff)++] = Abc_Var2Lit( Gia_ObjFanin0(pObj)->Value, Gia_ObjFaninC0(pObj) ); - pOff[1+(*pOff)++] = Abc_Var2Lit( Gia_ObjFanin1(pObj)->Value, Gia_ObjFaninC1(pObj) ); - pOff0[1+(*pOff0)++] = Abc_Var2Lit( pObj->Value, Gia_ObjFaninC0(pObj) ); - pOff1[1+(*pOff1)++] = Abc_Var2Lit( pObj->Value, Gia_ObjFaninC1(pObj) ); - - } - else if ( Gia_ObjIsRo(p, pObj) ) - { - pObjRi = Gia_ObjRoToRi(p, pObj); - pOff0 = Gia_IsoFanoutVec( vFanout, Gia_ObjFanin0(pObjRi)->Value ); - pOff[1+(*pOff)++] = Abc_Var2Lit( Gia_ObjFanin0(pObjRi)->Value, Gia_ObjFaninC0(pObjRi) ); - pOff0[1+(*pOff0)++] = Abc_Var2Lit( pObj->Value, Gia_ObjFaninC0(pObjRi) ); - } + Iso_SelectSort( pData, r - l + 1 ); + return; } - // verify - Gia_ManForEachObjVec( vUsed, p, pObj, i ) + while ( 1 ) { - nOffset = *Gia_IsoFanoutVec( vFanout, pObj->Value ); - if ( Gia_ObjIsAnd(pObj) ) - nOffset -= 2; - else if ( Gia_ObjIsRo(p, pObj) ) - nOffset -= 1; - assert( nOffset == Vec_IntEntry(vRefs, pObj->Value) ); + while ( (unsigned)pData[++i] < (unsigned)v ); + while ( (unsigned)v < (unsigned)pData[--j] ) + if ( j == l ) + break; + if ( i >= j ) + break; + ISO_SWAP( word, pData[i], pData[j] ); + if ( (unsigned)pData[i] == (unsigned)v ) + { p++; ISO_SWAP( word, pData[p], pData[i] ); } + if ( (unsigned)v == (unsigned)pData[j] ) + { q--; ISO_SWAP( word, pData[j], pData[q] ); } } + ISO_SWAP( word, pData[i], pData[r] ); + j = i-1; i = i+1; + for ( k = l; k < p; k++, j-- ) + ISO_SWAP( word, pData[k], pData[j] ); + for ( k = r-1; k > q; k--, i++ ) + ISO_SWAP( word, pData[i], pData[k] ); + Iso_QuickSort_rec( pData, l, j ); + Iso_QuickSort_rec( pData, i, r ); } - -/**Function************************************************************* - - Synopsis [Add fanouts of a new singleton object.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static inline void Gia_IsoAddSingletonFanouts( Gia_IsoMan_t * p, int Item, int Unique ) +void Iso_QuickSort( word * pData, int nSize ) { - int i, * pFan, * pFan2; - pFan = Gia_IsoFanoutVec( p->vFanout, Item ); - for ( i = 0; i < pFan[0]; i++ ) - { - if ( Vec_IntEntry( p->vUniques, Abc_Lit2Var(pFan[1+i]) ) >= 0 ) - continue; - pFan2 = Gia_IsoFanoutVec( p->vFanout2, Abc_Lit2Var(pFan[1+i]) ); - pFan2[1+(*pFan2)++] = Abc_Var2Lit( Unique, Abc_LitIsCompl(pFan[1+i]) ); - } + int i, fVerify = 1; + Iso_QuickSort_rec( pData, 0, nSize - 1 ); + if ( fVerify ) + for ( i = 1; i < nSize; i++ ) + assert( (unsigned)pData[i-1] <= (unsigned)pData[i] ); } /**Function************************************************************* @@ -330,40 +213,50 @@ static inline void Gia_IsoAddSingletonFanouts( Gia_IsoMan_t * p, int Item, int U SeeAlso [] ***********************************************************************/ -void Gia_IsoCreateFanout2( Gia_IsoMan_t * p ) +int Iso_QuickSortCompare( word * p1, word * p2 ) { - int i, Entry, nOffset, nFanouts = 0, nLeftover = 0; - assert( Vec_IntSize(p->vFanout2) == 0 ); - // count the number of fanouts and objects remaining - Vec_IntForEachEntry( p->vUniques, Entry, i ) - { - if ( Entry >= 0 ) - continue; - nLeftover++; - nFanouts += *Gia_IsoFanoutVec(p->vFanout, i); - } - assert( nLeftover + p->nUniques == Vec_IntSize(p->vUsed) ); - // assign the fanouts - nOffset = Vec_IntSize(p->vUsed); - Vec_IntGrowResize( p->vFanout2, Vec_IntSize(p->vUsed) + 2 * nLeftover + nFanouts ); - Vec_IntForEachEntry( p->vUniques, Entry, i ) + return (unsigned)(*p1)-(unsigned)(*p2); +} +void Iso_QuickSortTest() +{ + int Size = 10000000; + int fVerbose = 0; + word * pData1, * pData2; + int i, clk = clock(); + // generate numbers + pData1 = ABC_ALLOC( word, Size ); + pData2 = ABC_ALLOC( word, Size ); + srand( 1111 ); + for ( i = 0; i < Size; i++ ) + pData2[i] = pData1[i] = ((word)i << 32) | rand(); + Abc_PrintTime( 1, "Prepare ", clock() - clk ); + // perform sorting + clk = clock(); + Iso_QuickSort_rec( pData1, 0, Size-1 ); + Abc_PrintTime( 1, "Sort new", clock() - clk ); + // print the result + if ( fVerbose ) { - if ( Entry >= 0 ) - continue; - Vec_IntWriteEntry( p->vFanout2, i, nOffset ); - Vec_IntWriteEntry( p->vFanout2, nOffset, 0 ); - nOffset += 2 + *Gia_IsoFanoutVec(p->vFanout, i); + for ( i = 0; i < Size; i++ ) + printf( "(%d,%d) ", (int)(pData1[i] >> 32), (int)pData1[i] ); + printf( "\n" ); } - assert( nOffset == Vec_IntSize(p->vUsed) + 2 * nLeftover + nFanouts ); - // add currently available items - Vec_IntForEachEntry( p->vUniques, Entry, i ) + // create new numbers + clk = clock(); + qsort( (void *)pData2, Size, sizeof(word), (int (*)(const void *, const void *))Iso_QuickSortCompare ); + Abc_PrintTime( 1, "Sort old", clock() - clk ); + // print the result + if ( fVerbose ) { - if ( Entry == -1 ) - continue; - Gia_IsoAddSingletonFanouts( p, i, Entry ); + for ( i = 0; i < Size; i++ ) + printf( "(%d,%d) ", (int)(pData2[i] >> 32), (int)pData2[i] ); + printf( "\n" ); } + ABC_FREE( pData1 ); + ABC_FREE( pData2 ); } + /**Function************************************************************* Synopsis [] @@ -375,75 +268,33 @@ void Gia_IsoCreateFanout2( Gia_IsoMan_t * p ) SeeAlso [] ***********************************************************************/ -void Gia_IsoCreateSigs( Gia_IsoMan_t * p ) +Gia_IsoMan_t * Gia_IsoManStart( Gia_Man_t * pGia ) { - Gia_Obj_t * pObj, * pObjRi; - int i, Lev0, Lev1, Lev; - Vec_IntClear( p->vLevels ); - Vec_IntClear( p->vFin0Levs ); - Vec_IntClear( p->vFin1Levs ); - Vec_IntClear( p->vFinSig ); - Vec_IntFill( p->vFoutPos, Vec_IntSize(p->vUsed), 0 ); - Vec_IntFill( p->vFoutNeg, Vec_IntSize(p->vUsed), 0 ); - Gia_ManForEachObjVec( p->vUsed, p->pGia, pObj, i ) - { - if ( Gia_ObjIsAnd(pObj) ) - { - Lev0 = Vec_IntEntry( p->vLevels, Gia_ObjFanin0(pObj)->Value ); - Lev1 = Vec_IntEntry( p->vLevels, Gia_ObjFanin1(pObj)->Value ); - Lev = 1 + Abc_MaxInt( Lev0, Lev1 ); - - Vec_IntPush( p->vLevels, Lev ); - if ( Gia_ObjFaninC0(pObj) < Gia_ObjFaninC1(pObj) || (Gia_ObjFaninC0(pObj) == Gia_ObjFaninC1(pObj) && Lev0 < Lev1) ) - { - Vec_IntPush( p->vFin0Levs, Lev-Lev0 ); - Vec_IntPush( p->vFin1Levs, Lev-Lev1 ); - } - else - { - Vec_IntPush( p->vFin0Levs, Lev-Lev1 ); - Vec_IntPush( p->vFin1Levs, Lev-Lev0 ); - } - if ( Gia_ObjIsMuxType(pObj) ) // uniqify MUX/XOR - Vec_IntPush( p->vFinSig, 3 ); - else - Vec_IntPush( p->vFinSig, Gia_ObjFaninC0(pObj) + Gia_ObjFaninC1(pObj) ); - Vec_IntAddToEntry( Gia_ObjFaninC0(pObj) ? p->vFoutNeg : p->vFoutPos, Gia_ObjFanin0(pObj)->Value, 1 ); - Vec_IntAddToEntry( Gia_ObjFaninC1(pObj) ? p->vFoutNeg : p->vFoutPos, Gia_ObjFanin1(pObj)->Value, 1 ); - } - else if ( Gia_ObjIsRo(p->pGia, pObj) ) - { - pObjRi = Gia_ObjRoToRi(p->pGia, pObj); - Vec_IntPush( p->vLevels, 0 ); - Vec_IntPush( p->vFin0Levs, 1 ); // not ready yet! - Vec_IntPush( p->vFin1Levs, 0 ); - Vec_IntPush( p->vFinSig, Gia_ObjFaninC0(pObjRi) ); - Vec_IntAddToEntry( Gia_ObjFaninC0(pObjRi) ? p->vFoutNeg : p->vFoutPos, Gia_ObjFanin0(pObjRi)->Value, 1 ); - } - else if ( Gia_ObjIsPi(p->pGia, pObj) ) - { - Vec_IntPush( p->vLevels, 0 ); - Vec_IntPush( p->vFin0Levs, 0 ); - Vec_IntPush( p->vFin1Levs, 0 ); - Vec_IntPush( p->vFinSig, 4 ); - } - else if ( Gia_ObjIsConst0(pObj) ) - { - Vec_IntPush( p->vLevels, 0 ); - Vec_IntPush( p->vFin0Levs, 0 ); - Vec_IntPush( p->vFin1Levs, 0 ); - Vec_IntPush( p->vFinSig, 5 ); - } - else assert( 0 ); - } - assert( Vec_IntSize( p->vLevels ) == Vec_IntSize(p->vUsed) ); - assert( Vec_IntSize( p->vFin0Levs ) == Vec_IntSize(p->vUsed) ); - assert( Vec_IntSize( p->vFin1Levs ) == Vec_IntSize(p->vUsed) ); - assert( Vec_IntSize( p->vFinSig ) == Vec_IntSize(p->vUsed) ); - // prepare items - Vec_IntClear( p->vItems ); - for ( i = 0; i < Vec_IntSize(p->vUsed); i++ ) - Vec_IntPush( p->vItems, i ); + 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 ); } @@ -458,252 +309,131 @@ void Gia_IsoCreateSigs( Gia_IsoMan_t * p ) SeeAlso [] ***********************************************************************/ -void Gia_IsoSortStats( Vec_Int_t * vItems, Vec_Int_t * vCosts, Vec_Int_t * vMap, Vec_Int_t * vSeens, Vec_Int_t * vCounts, Vec_Int_t * vResult ) +void Gia_IsoPrintClasses( Gia_IsoMan_t * p ) { - int i, Entry, Place; - // assumes vCosts are between 0 and Vec_IntSize(vMap) - // assumes vMap is clean and leaves it clean -// Vec_IntForEachEntry( vMap, Entry, i ) -// assert( Entry == -1 ); - -// printf( "vItems: " ); -// Vec_IntPrint( vItems ); -// printf( "vCosts: " ); -// Vec_IntPrint( vCosts ); - - // collect places - Vec_IntClear( vSeens ); - Vec_IntClear( vCounts ); - Vec_IntForEachEntry( vItems, Entry, i ) + 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 ) { - Entry = Vec_IntEntry(vCosts, Entry); - Place = Vec_IntEntry(vMap, Entry); - if ( Place == -1 ) + printf( "%5d : (%d,%d) ", i/2, iBegin, nSize ); + if ( fVerbose ) { - Vec_IntWriteEntry( vMap, Entry, Vec_IntSize(vSeens) ); - Vec_IntPush( vSeens, Entry ); - Vec_IntPush( vCounts, 1 ); + printf( "{" ); + for ( k = 0; k < nSize; k++ ) + printf( " %d,%d", Gia_IsoGetItem(p, iBegin+k), Gia_IsoGetValue(p, iBegin+k) ); + printf( " }" ); } - else - Vec_IntAddToEntry( vCounts, Place, 1 ); + printf( "\n" ); } - - // sort places - Vec_IntSort( vSeens, 0 ); - -// printf( "vCounts: " ); -// Vec_IntPrint( vCounts ); -// printf( "vSeens: " ); -// Vec_IntPrint( vSeens ); - - // create the final array - Vec_IntClear( vResult ); - Vec_IntForEachEntry( vSeens, Entry, i ) - { - Place = Vec_IntEntry( vMap, Entry ); - Vec_IntPush( vResult, Entry ); - Vec_IntPush( vResult, Vec_IntEntry(vCounts, Place) ); - } - - // clean map - Vec_IntForEachEntry( vSeens, Entry, i ) - Vec_IntWriteEntry( vMap, Entry, -1 ); - -// printf( "vResult: " ); -// Vec_IntPrint( vResult ); - -// printf( "(%d)", Vec_IntSize(vResult)/2 ); } - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Vec_Int_t * Gia_IsoCreateStats( Gia_IsoMan_t * p, int iPo ) +void Gia_IsoPrint( Gia_IsoMan_t * p, int Iter, int Time ) { - Vec_Int_t * vStats = Vec_IntAlloc( 1000 ); - Gia_IsoCollectUsed( p->pGia, iPo, p->vUsed, p->vRoots ); - Gia_IsoSortStats( p->vItems, p->vLevels, p->vMap, p->vSeens, p->vCounts, p->vResult ); Vec_IntAppend( vStats, p->vResult ); - Gia_IsoSortStats( p->vItems, p->vFin0Levs, p->vMap, p->vSeens, p->vCounts, p->vResult ); Vec_IntAppend( vStats, p->vResult ); - Gia_IsoSortStats( p->vItems, p->vFin1Levs, p->vMap, p->vSeens, p->vCounts, p->vResult ); Vec_IntAppend( vStats, p->vResult ); - Gia_IsoSortStats( p->vItems, p->vFoutPos, p->vMap, p->vSeens, p->vCounts, p->vResult ); Vec_IntAppend( vStats, p->vResult ); - Gia_IsoSortStats( p->vItems, p->vFoutNeg, p->vMap, p->vSeens, p->vCounts, p->vResult ); Vec_IntAppend( vStats, p->vResult ); - Gia_IsoSortStats( p->vItems, p->vFinSig, p->vMap, p->vSeens, p->vCounts, p->vResult ); Vec_IntAppend( vStats, p->vResult ); - Gia_IsoCleanUsed( p->pGia, p->vUsed ); - return vStats; + printf( "Iter %4d : ", Iter ); + printf( "Entries =%8d. ", p->nEntries ); + printf( "Classes =%8d. ", Vec_IntSize(p->vClasses)/2 ); + printf( "Singles =%8d. ", p->nSingles ); + printf( "%9.2f sec", (float)(Time)/(float)(CLOCKS_PER_SEC) ); + printf( "\n" ); + fflush( stdout ); } - - - /**Function************************************************************* - Synopsis [Sorting an array of entries.] + Synopsis [] - Description [This procedure can have the following outcomes: - - There is no refinement (the class remains unchanged). - - There is complete refinement (all elements became singletons) - - There is partial refinement (some new classes and some singletons) - The permutes set of items if returned in vItems.] + Description [] SideEffects [] SeeAlso [] ***********************************************************************/ -void Gia_IsoSortVec( Vec_Int_t * vItems, Vec_Int_t * vCosts, Vec_Int_t * vMap, - Vec_Int_t * vSeens, Vec_Int_t * vCounts, Vec_Int_t * vResult, - Vec_Int_t * vClassNew ) +void Gia_IsoPrepare( Gia_IsoMan_t * p ) { - int i, Entry, Entry0, Place, Counter; - // assumes vCosts are between 0 and Vec_IntSize(vMap) - // assumes vMap is clean and leaves it clean - assert( Vec_IntSize(vItems) > 1 ); - - // prepare return values - Vec_IntClear( vClassNew ); - - // collect places - Vec_IntClear( vSeens ); - Vec_IntClear( vCounts ); - Vec_IntForEachEntry( vItems, Entry0, i ) + 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 ) { - Entry = Vec_IntEntry(vCosts, Entry0); - Place = Vec_IntEntry(vMap, Entry); - if ( Place == -1 ) - { - Vec_IntWriteEntry( vMap, Entry, Vec_IntSize(vSeens) ); - Vec_IntPush( vSeens, Entry ); - Vec_IntPush( vCounts, 1 ); - } - else - Vec_IntAddToEntry( vCounts, Place, 1 ); + 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)] ); } - // check if refinement is happening - if ( Vec_IntSize(vSeens) == 1 ) // there is no refinement + // 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++ ) { - Vec_IntPush( vClassNew, 0 ); - Vec_IntPush( vClassNew, Vec_IntSize(vItems) ); - // no need to change vItems + Vec_IntPush( p->vClasses, pLevBegins[i] ); + Vec_IntPush( p->vClasses, pLevSizes[i] ); + pLevBegins[i+1] = pLevBegins[i] + pLevSizes[i]; } - else // complete or partial refinement + assert( pLevBegins[MaxLev+1] == p->nObjs ); + // put them into the structure + for ( i = 1; i < p->nObjs; i++ ) { - // sort places - Vec_IntSort( vSeens, 0 ); - - // set the map to point to the place in the final array - Counter = 0; - Vec_IntForEachEntry( vSeens, Entry, i ) - { - Place = Vec_IntEntry( vMap, Entry ); - Vec_IntWriteEntry( vMap, Entry, Counter ); - Vec_IntPush( vClassNew, Counter ); - Vec_IntPush( vClassNew, Vec_IntEntry( vCounts, Place ) ); - assert( Vec_IntEntry( vCounts, Place ) > 0 ); - Counter += Vec_IntEntry( vCounts, Place ); - } - assert( Counter == Vec_IntSize(vItems) ); - - // fill the result - Vec_IntGrowResize( vResult, Vec_IntSize(vItems) ); - Vec_IntFill( vResult, Vec_IntSize(vItems), -1 ); // verify - Vec_IntForEachEntry( vItems, Entry0, i ) - { - Entry = Vec_IntEntry(vCosts, Entry0); - Place = Vec_IntAddToEntry( vMap, Entry, 1 ) - 1; - Vec_IntWriteEntry( vResult, Place, Entry0 ); - } - Vec_IntForEachEntry( vResult, Entry, i ) // verify - assert( Entry >= 0 ); - assert( Vec_IntSize(vItems) == Vec_IntSize(vResult) ); - memmove( Vec_IntArray(vItems), Vec_IntArray(vResult), sizeof(int) * Vec_IntSize(vResult) ); +// Gia_IsoSetValue( p, pLevBegins[p->pLevels[i]], p->pLevels[i] ); + Gia_IsoSetItem( p, pLevBegins[p->pLevels[i]]++, i ); } - - // clean map - Vec_IntForEachEntry( vSeens, Entry, i ) - Vec_IntWriteEntry( vMap, Entry, -1 ); -} - -/**Function************************************************************* - - Synopsis [Introduces a new singleton object.] - - Description [Updates current equivalence classes.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Gia_IsoAddSingleton( Gia_IsoMan_t * p, int Item ) -{ - // assign unique number - assert( Vec_IntEntry( p->vUniques, Item ) == -1 ); - Vec_IntWriteEntry( p->vUniques, Item, p->nUniques++ ); - if ( Vec_IntSize(p->vFanout2) == 0 ) - return; - // create fanouts - Gia_IsoAddSingletonFanouts( p, Item, p->nUniques-1 ); + 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" ); +*/ +// Gia_IsoPrintClasses( p ); } /**Function************************************************************* - Synopsis [Updates current equivalence classes.]] + Synopsis [] - Description [ + Description [] SideEffects [] SeeAlso [] ***********************************************************************/ -int Gia_IsoRefine( Gia_IsoMan_t * p, Vec_Int_t * vParam ) +void Gia_IsoAssignUnique( Gia_IsoMan_t * p ) { - Vec_Int_t vThis, * pTemp; - int i, k, Begin, nSize, Begin2, nSize2, Counter = 0; - assert( Vec_IntSize(p->vClass) > 0 ); - assert( Vec_IntSize(p->vClass) % 2 == 0 ); - Vec_IntClear( p->vClass2 ); - Vec_IntForEachEntryDouble( p->vClass, Begin, nSize, i ) + int i, iBegin, nSize; + p->nSingles = 0; + Vec_IntClear( p->vClasses2 ); + Vec_IntForEachEntryDouble( p->vClasses, iBegin, nSize, i ) { - vThis.nSize = vThis.nCap = nSize; - vThis.pArray = Vec_IntArray(p->vItems) + Begin; - Gia_IsoSortVec( &vThis, vParam, p->vMap, p->vSeens, p->vCounts, p->vResult, p->vClassNew ); - Vec_IntForEachEntryDouble( p->vClassNew, Begin2, nSize2, k ) + if ( nSize == 1 ) { - if ( nSize2 == 1 ) - { - Gia_IsoAddSingleton( p, Vec_IntEntry(p->vItems, Begin+Begin2) ); - Counter++; - continue; - } - Vec_IntPush( p->vClass2, Begin+Begin2 ); - Vec_IntPush( p->vClass2, nSize2 ); + assert( p->pUniques[Gia_IsoGetItem(p, iBegin)] == 0 ); + p->pUniques[Gia_IsoGetItem(p, iBegin)] = p->nUniques++; + p->nSingles++; } - } - // update classes - pTemp = p->vClass2; p->vClass2 = p->vClass; p->vClass = pTemp; - // remember beginning of each level - if ( vParam == p->vLevels ) - { - Vec_IntClear( p->vLevelLim ); - Vec_IntForEachEntryDouble( p->vClass, Begin, nSize, i ) + else { - assert( nSize > 0 ); - assert( Vec_IntEntry(p->vLevels, Vec_IntEntry(p->vItems, Begin)) == i ); - Vec_IntPush( p->vLevelLim, Begin ); + Vec_IntPush( p->vClasses2, iBegin ); + Vec_IntPush( p->vClasses2, nSize ); } - Vec_IntPush( p->vLevelLim, Vec_IntSize(p->vItems) ); } - return Counter; + ISO_SWAP( Vec_Int_t *, p->vClasses, p->vClasses2 ); + p->nEntries -= p->nSingles; } /**Function************************************************************* @@ -717,155 +447,41 @@ int Gia_IsoRefine( Gia_IsoMan_t * p, Vec_Int_t * vParam ) SeeAlso [] ***********************************************************************/ -int Gia_IsoAssignUniqueToLastLevel( Gia_IsoMan_t * p ) +static inline unsigned Gia_IsoUpdate( int iLevel, int iUniqueF, int fCompl ) { - int i, Begin, End, Item, Level, Counter = 0; - assert( Vec_IntSize( p->vClass ) > 0 ); - // get the last unrefined class - Begin = Vec_IntEntry( p->vClass, Vec_IntSize(p->vClass)-2 ); - // get the last unrefined class - Item = Vec_IntEntry( p->vItems, Begin ); - // get the level of this class - Level = Vec_IntEntry( p->vLevels, Item ); - // get the first entry on this level - Begin = Vec_IntEntry( p->vLevelLim, Level ); - End = Vec_IntEntry( p->vLevelLim, Level+1 ); - // assign all unassigned items on this level - Vec_IntForEachEntryStartStop( p->vItems, Item, i, Begin, End ) - if ( Vec_IntEntry( p->vUniques, Item ) == -1 ) - { - Gia_IsoAddSingleton( p, Item ); - Counter++; - } - return Counter; + return iLevel * s_256Primes[Abc_Var2Lit(iLevel, fCompl) & ISO_MASK] + + iUniqueF * s_256Primes[Abc_Var2Lit(iUniqueF+ISO_MASK/2, fCompl) & ISO_MASK]; } - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Gia_IsoPrint( Gia_IsoMan_t * p, int Iter, int nSingles, int Time ) +void Gia_IsoSimulate( Gia_IsoMan_t * p, int Iter ) { - printf( "Iter %3d : ", Iter ); - printf( "Classes =%7d. ", Vec_IntSize(p->vClass)/2 ); - printf( "Uniques =%7d. ", p->nUniques ); - printf( "Singles =%7d. ", nSingles ); - Abc_PrintTime( 1, "Time", Time ); -} - -/**Function************************************************************* - - Synopsis [Compares two objects by their ID.] - - 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( Gia_ObjIsTerm(pObj1) && Gia_ObjIsTerm(pObj2) ); - return pObj1->Value - pObj2->Value; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Gia_IsoCreateUniques( Gia_IsoMan_t * p, int iPo ) -{ - Vec_Int_t * vArray[6] = { p->vLevels, p->vFin0Levs, p->vFin1Levs, p->vFoutPos, p->vFoutNeg, p->vFinSig }; - int i, nSingles, clk = clock(); - Gia_IsoCollectUsed( p->pGia, iPo, p->vUsed, p->vRoots ); - Vec_IntClear( p->vFanout2 ); - // prepare uniques - p->nUniques = 0; - Vec_IntFill( p->vUniques, Vec_IntSize(p->vUsed), -1 ); - Gia_IsoAddSingleton( p, 0 ); - // prepare classes - Vec_IntClear( p->vClass ); - Vec_IntPush( p->vClass, 1 ); - Vec_IntPush( p->vClass, Vec_IntSize(p->vUsed) ); - // perform refinement - Gia_IsoPrint( p, 0, 0, clock() - clk ); - for ( i = 0; i < 6; i++ ) + Gia_Obj_t * pObj, * pObjF; + int i, iObj; + // initialize constant, inputs, and flops in the first frame + Gia_ManConst0(p->pGia)->Value = s_256Primes2[Abc_Var2Lit(Iter, 0) & ISO_MASK]; + Gia_ManForEachPi( p->pGia, pObj, i ) + pObj->Value = s_256Primes2[Abc_Var2Lit(Iter, 1) & ISO_MASK]; + if ( Iter == 0 ) + Gia_ManForEachRo( p->pGia, pObj, i ) + pObj->Value = s_256Primes2[ISO_MASK]; + // simiulate objects + Gia_ManForEachAnd( p->pGia, pObj, i ) { - nSingles = Gia_IsoRefine( p, vArray[i] ); - Gia_IsoPrint( p, i+1, nSingles, clock() - clk ); + pObj->Value += Gia_ObjFanin0(pObj)->Value + Gia_IsoUpdate(p->pLevels[i], p->pUniques[Gia_ObjFaninId0(pObj, i)], Gia_ObjFaninC0(pObj)); + pObj->Value += Gia_ObjFanin1(pObj)->Value + Gia_IsoUpdate(p->pLevels[i], p->pUniques[Gia_ObjFaninId1(pObj, i)], Gia_ObjFaninC1(pObj)); } - // derive fanouts - Gia_IsoCreateFanout( p->pGia, p->vUsed, p->vRefs, p->vFanout ); - Gia_IsoCreateFanout2( p ); - // perform refinement - for ( i = 6; p->nUniques < Vec_IntSize(p->vUsed); i++ ) + Gia_ManForEachCo( p->pGia, pObj, i ) { - nSingles = Gia_IsoRefine( p, NULL ); - Gia_IsoPrint( p, i+1, nSingles, clock() - clk ); - if ( nSingles == 0 ) - { - nSingles = Gia_IsoAssignUniqueToLastLevel( p ); - Gia_IsoPrint( p, i+1, nSingles, clock() - clk ); - } + iObj = Gia_ObjId(p->pGia, pObj); + pObj->Value += Gia_ObjFanin0(pObj)->Value + Gia_IsoUpdate(p->pLevels[iObj], p->pUniques[Gia_ObjFaninId0(pObj, iObj)], Gia_ObjFaninC0(pObj)); } - // finished refinement - Gia_IsoCleanUsed( p->pGia, p->vUsed ); + // transfer flop values + Gia_ManForEachRiRo( p->pGia, pObjF, pObj, i ) + pObj->Value += pObjF->Value; } /**Function************************************************************* - Synopsis [Returns canonical permutation of the inputs.] - - Description [Assumes that each CI/AND object has its unique number set.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Gia_ManFindIsoPermCis( Gia_Man_t * p, Vec_Ptr_t * vTemp, Vec_Int_t * vRes ) -{ - Gia_Obj_t * pObj; - int i; - Vec_IntClear( vRes ); - // 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( vRes, Gia_ObjCioId(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( vRes, Gia_ObjCioId(pObj) ); -} - -/**Function************************************************************* - - Synopsis [Find the canonical permutation of the COs.] + Synopsis [] Description [] @@ -874,65 +490,60 @@ void Gia_ManFindIsoPermCis( Gia_Man_t * p, Vec_Ptr_t * vTemp, Vec_Int_t * vRes ) SeeAlso [] ***********************************************************************/ -void Gia_ManFindIsoPermCos( Gia_Man_t * p, Vec_Int_t * vPermCis, Vec_Ptr_t * vTemp, Vec_Int_t * vRes ) +void Gia_IsoSort( Gia_IsoMan_t * p ) { - Gia_Obj_t * pObj; - int i, Entry, Diff; - assert( Vec_IntSize(vPermCis) == Gia_ManCiNum(p) ); - Vec_IntClear( vRes ); - if ( Gia_ManPoNum(p) == 1 ) - Vec_IntPush( vRes, 0 ); - else + Gia_Obj_t * pObj, * pObj0; + int i, k, fSameValue, iBegin, iBeginOld, nSize, nSizeNew; + // go through the equiv classes + p->nSingles = 0; + Vec_IntClear( p->vClasses2 ); + Vec_IntForEachEntryDouble( p->vClasses, iBegin, nSize, i ) { - Vec_PtrClear( vTemp ); - Gia_ManForEachPo( p, pObj, 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 ) { - pObj->Value = Abc_Var2Lit( Gia_ObjFanin0(pObj)->Value, Gia_ObjFaninC0(pObj) ); - Vec_PtrPush( vTemp, pObj ); + Vec_IntPush( p->vClasses2, iBegin ); + Vec_IntPush( p->vClasses2, nSize ); + continue; + } + // sort the objects + Iso_QuickSort( p->pStoreW + iBegin, nSize ); + // divide them into 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; } - Vec_PtrSort( vTemp, (int (*)(void))Gia_ObjCompareByValue ); - Vec_PtrForEachEntry( Gia_Obj_t *, vTemp, pObj, i ) - Vec_IntPush( vRes, Gia_ObjCioId(pObj) ); } - // add flop outputs - Diff = Gia_ManPoNum(p) - Gia_ManPiNum(p); - Vec_IntForEachEntryStart( vPermCis, Entry, i, Gia_ManPiNum(p) ) - Vec_IntPush( vRes, Entry + Diff ); + ISO_SWAP( Vec_Int_t *, p->vClasses, p->vClasses2 ); + p->nEntries -= p->nSingles; } -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Gia_Man_t * Gia_ManDupCanonical( Gia_Man_t * p, Vec_Int_t * vUsed, Vec_Int_t * vUniques ) -{ - return NULL; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Gia_IsoCompareVecStr( Vec_Str_t ** p1, Vec_Str_t ** p2 ) -{ - return Vec_StrCompareVec( *p1, *p2 ); -} - - /**Function************************************************************* Synopsis [] @@ -946,144 +557,25 @@ int Gia_IsoCompareVecStr( Vec_Str_t ** p1, Vec_Str_t ** p2 ) ***********************************************************************/ void Gia_IsoTest( Gia_Man_t * pGia ) { - int fVerbose = 0; - Vec_Ptr_t * vResults; - Vec_Int_t * vStats; + int nIterMax = 0; Gia_IsoMan_t * p; int i, clk = clock(); Gia_ManCleanValue( pGia ); p = Gia_IsoManStart( pGia ); - for ( i = 0; i < Gia_ManPoNum(pGia); i++ ) + Gia_IsoPrepare( p ); + Gia_IsoAssignUnique( p ); + Gia_IsoPrint( p, 0, clock() - clk ); + for ( i = 0; i < nIterMax; i++ ) { - if ( i % 100 == 0 ) - printf( "Finished %5d\r", i ); - vStats = Gia_IsoCreateStats( p, i ); - Vec_PtrPush( p->vResults, vStats ); - if ( fVerbose ) - printf( "%d ", Vec_IntSize(vStats)/2 ); + Gia_IsoSimulate( p, i ); + Gia_IsoSort( p ); + Gia_IsoPrint( p, i+1, clock() - clk ); } - if ( fVerbose ) - printf( " \n" ); - vResults = p->vResults; - p->vResults = NULL; Gia_IsoManStop( p ); -// return vResults; - Vec_VecFree( (Vec_Vec_t *)vResults ); Abc_PrintTime( 1, "Time", clock() - clk ); } -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Gia_Man_t * Gia_IsoFilterPos( Gia_Man_t * pGia, int fVerbose ) -{ -// int fVeryVerbose = 0; - Gia_IsoMan_t * p; - Gia_Man_t * pTemp; - Vec_Ptr_t * vBuffers, * vClasses; - Vec_Int_t * vLevel, * vRemain; - Vec_Str_t * vStr, * vPrev; - int i, nUnique = 0, clk = clock(); - int clkAig = 0, clkIso = 0, clk2; - - // start the manager - Gia_ManCleanValue( pGia ); - p = Gia_IsoManStart( pGia ); - // derive AIG for each PO - vBuffers = Vec_PtrAlloc( Gia_ManPoNum(pGia) ); - for ( i = 0; i < Gia_ManPoNum(pGia); i++ ) - { - if ( i % 100 == 0 ) - printf( "%6d finished...\r", i ); - - clk2 = clock(); - pTemp = Gia_ManDupCanonical( pGia, p->vUsed, p->vUniques ); - clkIso += clock() - clk2; - - clk2 = clock(); - vStr = Gia_WriteAigerIntoMemoryStr( pTemp ); - clkAig += clock() - clk2; - - Vec_PtrPush( vBuffers, vStr ); - Gia_ManStop( pTemp ); - // remember the output number in nCap (attention: hack!) - vStr->nCap = i; - } - // stop the manager - Gia_IsoManStop( p ); - -// s_Counter = 0; - if ( fVerbose ) - { - Abc_PrintTime( 1, "Isomorph time", clkIso ); - Abc_PrintTime( 1, "AIGER time", clkAig ); - } - - // sort the infos - clk = clock(); - Vec_PtrSort( vBuffers, (int (*)(void))Gia_IsoCompareVecStr ); - - // create classes - clk = clock(); - vClasses = Vec_PtrAlloc( Gia_ManPoNum(pGia) ); - // 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", Gia_ManPoNum(pGia), 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 - pTemp = Gia_ManDupCones( pGia, 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 pTemp; -} - - //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/saig/saigIsoSlow.c b/src/aig/saig/saigIsoSlow.c index 0528bf08..a5b1a2d8 100644 --- a/src/aig/saig/saigIsoSlow.c +++ b/src/aig/saig/saigIsoSlow.c @@ -93,6 +93,7 @@ static int s_1kPrimes[ISO_MASK+1] = }; */ +/* #define ISO_MASK 0x7F static int s_1kPrimes[ISO_MASK+1] = { 1009, 1049, 1093, 1151, 1201, 1249, 1297, 1361, 1427, 1459, @@ -109,6 +110,7 @@ static int s_1kPrimes[ISO_MASK+1] = { 7393, 7477, 7523, 7561, 7607, 7681, 7727, 7817, 7877, 7933, 8011, 8039, 8059, 8081, 8093, 8111, 8123, 8147 }; +*/ /* #define ISO_MASK 0x7 @@ -117,6 +119,141 @@ static int s_1kPrimes[ISO_MASK+1] = { }; */ +#define ISO_MASK 0x3FF +static int s_1kPrimes[ISO_MASK+1] = +//#define ISO_MASK 0xFF +//static int s_1kPrimes[0x3FF+1] = +{ + 0x38c19891,0xde37b0ed,0xdebcd025,0xe19b7bbe,0x7e7ebd0e,0xaeed03a1,0x811230dc,0x10bfece0, + 0xb3b23fb1,0x74176098,0xc34ec7c5,0x6bef8939,0xc40be5e3,0x2ab51a09,0xafc17cea,0x0dccc7a2, + 0xdf7db34d,0x1009c96f,0x93fd7494,0x54385b33,0x6f36eed8,0xa1953f82,0xfbd1144a,0xde533a46, + 0x23aa1cad,0x9a18943c,0xb65000d8,0x867e9974,0xe7880035,0xf9931ad4,0xcfca1e45,0x6b5aec96, + 0xe9c1a119,0xfa4968c5,0x94cf93da,0xe8c9eac4,0x95884242,0x1bba52c7,0x9232c321,0x9cec8658, + 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, + 0x214d04ab,0xe093e487,0x10607ada,0x42b261cc,0x1a85e0f6,0xb851bfc3,0x77d5591c,0xda13f344, + 0xc39c4c00,0xe60d75fc,0x7edae36a,0x3e4ac3ec,0x8bc38db4,0xe848dce9,0xb2407d4d,0x0d79c61e, + 0x1e6c293a,0x7bc30986,0xdf18cb8f,0x23003172,0x6948e3fa,0x9b7e4f09,0x14b3b339,0x9c8078c2, + 0x9a47c29f,0x85bb45ec,0x9ca35a93,0xd7db5227,0x1d9b0a10,0xb7fbbfe9,0x05b72426,0x6f30b2fa, + 0x9fb44078,0xedffd3f8,0x1b02b7bc,0x43e3cfd3,0x0d44293e,0x25c8d552,0xedd3f85d,0x6f921c8c, + 0x953cca0c,0x9c975b70,0xc6bd0b53,0x4f204f3e,0xa3cc69cc,0xceec390b,0x34905626,0x82ad5d41, + 0xe46589a5,0x7989841d,0x045d7d9f,0xe49b7b2f,0x46baf101,0x996f92de,0x427566c8,0x918a1ee1, + 0xf4baa589,0x6bdff7c7,0x3c6936ea,0xe85bfb70,0x5d96ea26,0x6d5a8991,0x7f0a528d,0x852f0634, + 0x2ec04501,0x5ca15c35,0xd8695e7a,0x456876c7,0x52e97b83,0x34b4c5ed,0x54d73fbb,0x44a6be01, + 0xf8019155,0x33d55a31,0x3fe51c99,0xe1cb94fd,0x8c39cd60,0xd585efba,0x2765579b,0xb8f7ed12, + 0xbb04b2cd,0xd8859981,0xd966988d,0xa68bfeda,0x73110705,0x38d6aec0,0x613bc275,0xc7283c2d, + 0xe051d0b1,0x32b8c2ee,0x0e73fb9e,0x7ab05c25,0x6ff652b9,0x45aeabc6,0x6be1a891,0x5b43531b, + 0xcd711248,0x2b777d40,0x46956d16,0x474355a8,0xe872d6c6,0xe4158d96,0xabe03036,0x5b4fd9a4, + 0xeceba1db,0xaac9713f,0xe953153b,0xf44a9229,0x460cba72,0xfd13fdf6,0x8bbf82ae,0xaf55778f, + 0xa447a5b2,0x98b647b3,0x5f351c57,0x69d0bb71,0xf14d2706,0x78b1a3af,0x7206c73f,0x3f5cd4a6, + 0x5c0e4515,0xdb46a663,0x10c3a9b0,0x8eda7748,0x52bb44c9,0x3df62689,0xc83e2732,0xf36c99af, + 0x7ec7a94c,0x5c823718,0x6586e58e,0x4b726e75,0xcfe03a05,0x34eb2f4b,0xf4eec9cf,0xb38d6d73, + 0x71fafa9e,0x0371a29a,0xc405f83b,0x889f49c2,0xd1443000,0x469665bf,0x609ed65d,0x67c8f9ba, + 0x9d2f6055,0xb91b8eb1,0x96c809fe,0x2d6ab0f5,0xc16d4f04,0x590171ab,0x73d67526,0xf724e44c, + 0x6aef02b7,0x6489a325,0x4458401e,0x22d94ad7,0x05e5be57,0x5634fad8,0x951fcf70,0x4baad7f0, + 0x40c1090d,0xedc28abd,0x343cc6e4,0x4ff7c030,0x0734a641,0x2635a90e,0x2e000c84,0x4b617a70, + 0x872e9c9e,0x3dceeb42,0xd0fcc398,0x9cc9b9c8,0x2de02f0c,0xaf0e2614,0xa60253aa,0xe0517492, + 0xa7bde4b4,0x3bb66d7d,0x7f215e82,0xf259de66,0xe17380fe,0xdbc718b4,0x66abcc29,0xf0826e1f, + 0x08f60995,0xce81b933,0xa832c0e9,0x37aed7d4,0x8a75c261,0x916627b4,0xd486a04b,0x64fd0fde, + 0x1261328a,0xe037772f,0xb5b71117,0x55d04bd8,0x8f6c1c7b,0xb9f5fcdd,0x5918f756,0x25c90099, + 0x2e8787db,0x58e14e38,0x0d397852,0x32c8e33b,0x5ae2b795,0x3a7b3ff7,0x5eebf893,0x1aeee816, + 0xc2ef31d0,0x1d86e615,0x183f1de3,0xb89d46c4,0x525ebbf6,0xfe0198ca,0x4986cc4a,0x2a75701e, + 0x382158b1,0x192ee88f,0x3e512912,0xcd571c3d,0xdf694fe8,0xec8ead1d,0x83719ac3,0x3f654079, + 0xf6a623c5,0x33e1fc6e,0xe7f7c426,0x5bff0f6c,0x698a9bb1,0xec2a29ba,0x75358b45,0x40c6ffef, + 0x6605bb55,0x53a8c97a,0x7bba1569,0x499bc51b,0x5849c89a,0xe6ddb267,0x8659c719,0x14a05548, + 0xeec648a9,0x618af87a,0x62214521,0x7f36e610,0x152efeeb,0xc2b0f0ed,0x1d657588,0xa5fcec4b, + 0xf872f109,0x46903038,0x04b57b97,0xe5d51b14,0x06c264ec,0x68aa8d14,0xa4e1bed8,0xdae169c2, + 0xeb90debd,0xe8c11a7a,0xcafce013,0x63820cee,0x948c23e5,0xc1d42ea3,0x8256c951,0x9b587773, + 0x2fa8380c,0x30255e09,0x1a809cdc,0xe1446068,0x2714621d,0xb3347d64,0x1f4cbf3d,0xd068bc26, + 0x2c422740,0x06c4a3ad,0x5dc9d63c,0x4724bf48,0x28e34add,0x27d5221d,0xe349c7e2,0x6119e0a5, + 0x4ae7d29f,0x53a7912d,0xfc5db779,0x7d28d357,0xfd80036d,0x06bcc597,0x36d70a8a,0x37738cb7, + 0xf11e6272,0xfdd5d153,0x5dc666dc,0x6b5a415d,0x1073b415,0x36f30d9a,0x807daf7b,0x387f6823, + 0x8970fe00,0xee560be5,0xea8c0bad,0xfac2b422,0xc845861d,0xa181a2ee,0x29c4dffd,0x4d441bb2, + 0x7a64cf93,0x0c33e6ac,0x0a35d034,0x1067d26d,0x8c7da0cc,0x2d6e2d5a,0x9932c25a,0x5fca4e2c, + 0x2c82fd71,0x41730b70,0x244bdbb9,0x96514307,0xc6a32a6b,0xc4c256a7,0x38517fd8,0x541aa859, + 0x0752afe3,0x741e22f9,0xa2565483,0x7588b0b9,0xdd404e42,0x4d86c49d,0x6fa93fc1,0x163bd200, + 0x745d0d31,0x8d3dd20e,0xebdc64db,0x9315c149,0x39db3299,0xb0c22004,0xa4c0295b,0x8b3573eb, + 0xd92a40a3,0x73d6c379,0x67673309,0xdaff1d7f,0x42fcfeb8,0xd57c11a4,0x402066ef,0x9d1134e0, + 0x9f417081,0x10f49e00,0x7e7ee855,0x314e6d25,0x602bdbe6,0xa4be4045,0xac511dc4,0x33d6bda8, + 0x2f2bc412,0x4b9c0b6c,0x98aaab06,0x7f0a5801,0xfbf1f16d,0x058f54ae,0x4fd97724,0x348cb50b, + 0xef6f659f,0x0cd8b184,0x1d71a666,0xae3c87dd,0x7bd56793,0xe0f8f6a8,0x90429c55,0x8a3cc4d0, + 0x49957b70,0x3baf3912,0x755efebb,0xa5eca17f,0x486065a1,0x1dffcefb,0xd914b3a0,0x1ced93c1, + 0xa4262dcd,0xc12a4adc,0x08f6de4e,0x4c204faf,0xca1815de,0xa4af836f,0x91d5e44d,0xd2a7caa4, + 0x68a9a3fe,0x844f8dac,0x3fc36c67,0x8be23937,0x69879d94,0x5d0dbecb,0x1f0f59a4,0x94721142, + 0xfca6064a,0x6d28aa48,0x804cd04e,0x4a3906de,0x8e352509,0x302326d9,0xed4937ed,0x4a570e63, + 0xcaa57efb,0x64bd4878,0x3419334a,0x712e5f6b,0x9fa9d687,0x06f8645f,0x620ca96f,0xdc5d6cce, + 0x392f3257,0x52140f06,0xc4b3bda4,0xe8c7eba7,0x066bd754,0xc5941f26,0xe6dfd573,0x328dd14d, + 0xb1cb4ba7,0x1d37a9b8,0x96a195a5,0x970e535a,0x290351b8,0x570000f6,0xe14ae341,0x35ede6a6, + 0x9a02f032,0xaf2ebb58,0x146be492,0x670b3e4b,0x72fa6cfd,0xa243af97,0xbbd5fc21,0xcb8852a2, + 0x5d5b4a42,0xeefff0ac,0xa59ad1b6,0x3ec55544,0x48d64f69,0x9065d3d0,0xdd09485b,0xdd63bd09, + 0x605e811d,0xc4b4ed7d,0xb0b58558,0x0644400b,0x12222346,0x086f146a,0xad6dee36,0x5488d1a3, + 0x0c93bc0c,0x18555d92,0x9f4427bf,0xa590a66a,0x3a630fda,0xf1681c2e,0x948a16fb,0x16fe3338, + 0xc9832357,0xd1e8e6b5,0xd9cfe034,0x05b22f26,0x27233c6e,0x355890e1,0xfbe6eaf3,0x0dcd8e8f, + 0x00b5df46,0xd97730ac,0xc6dfd8ff,0x0cb1840a,0x41e9d249,0xbb471b4e,0x480b8f63,0x1ffe8871, + 0x17b11821,0x1709e440,0xcefb3668,0xa4954ddd,0xf03ef8b5,0x6b3e633c,0xe5813096,0x3697c9a6, + 0x7800f52f,0x73a7aa39,0x59ac23b7,0xb4663166,0x9ca9d6f8,0x2d441072,0x38cef3d3,0x39a3faf6, + 0x89299fb9,0xd558295f,0xcf79c633,0x232dd96e,0xadb2955b,0xe962cbb9,0xab7c0061,0x1027c329, + 0xb4b43e07,0x25240a7a,0x98ea4825,0xdbf2edbd,0x8be15d26,0x879f3cd9,0xa4138089,0xa32dcb06, + 0x602af961,0x4b13f451,0x1c87d0d5,0xc3bb141b,0x9ebf55a1,0xef030a9a,0x8d199b93,0xdabcbb56, + 0xf412f80f,0x302e90ad,0xc4d9878b,0xc392f650,0x4fd3a614,0x0a96ddc4,0xcd1878c7,0x9ddd3ae1, + 0xdaf46458,0xba7c8656,0xf667948f,0xc37e3c23,0x04a577c6,0xbe615f1e,0xcc97406c,0xd497f16f, + 0x79586586,0xd2057d14,0x1bb92028,0xab888e5e,0x26bef100,0xf46b3671,0xf21f1acc,0x67f288c8, + 0x39c722df,0x61d21eaf,0x9c5853a0,0x63b693c7,0x1ea53c0a,0x95bc0a85,0xa7372f2d,0x3ef6a6b3, + 0x82c9c4ac,0x4dea10ee,0xdfcb543d,0xd412f427,0x53e27f2c,0x875d8422,0x5367a7d8,0x41acf3fa, + 0xbce47234,0x8056fb9a,0x4e9a4c48,0xe4a45945,0x2cfee3ae,0xb4554b10,0x5e37a915,0x591b1963, + 0x4fa255c1,0xe01c897b,0x504e6208,0x7c7368eb,0x13808fd7,0x02ac0816,0x30305d2c,0x6c4bbdb7, + 0xa48a9599,0x57466059,0x4c6ebfc7,0x8587ccdf,0x6ff0abf0,0x5b6b63fe,0x31d9ec64,0x63458abd, + 0x21245905,0xccdb28fc,0xac828acb,0xe5e82bea,0xa7d76141,0xa699038e,0xcaba7e06,0x2710253f, + 0x2ff9c94d,0x26e48a2c,0xd713ec5e,0x869f2ed4,0x25bcd712,0xcb3e918f,0x615c3a5a,0x9fb43903, + 0x37900eb9,0x4f682db0,0x35a80dc6,0x4eb27c65,0x502735ab,0xb163b4c8,0x604649a8,0xb23a6cd3, + 0x9f715091,0x2e6fbb51,0x2ec9144b,0x272cbe65,0x90a0a453,0x420e1503,0x2d00d338,0x4aa96675, + 0xd025b61c,0xab02d9d7,0x2afe2a37,0xf8129b9b,0x4db04c54,0x654a5c06,0x3213ff51,0x4e09d0b1, + 0x333369a3,0xae27310a,0x91d076d0,0xa96ebcd0,0xefde54f4,0x021c309a,0xd506f53d,0xa5635251, + 0x2f23916e,0x1fe86bb1,0xcbc62160,0x2147c8cc,0xdeb3e47c,0x028e3987,0x8061de42,0x39be931b, + 0x2b7e54c5,0xe64d2f96,0x4069522d,0x4aa66857,0x83b62634,0x4ba72095,0x9aade2a9,0xf1223cd9, + 0x91cbddf0,0xec5d237f,0x593f3280,0x0b924439,0x446f4063,0xc66f8d8c,0x8b7128ba,0xb597f451, + 0xc8925236,0x1720f235,0x7cd2e9a0,0x4c130339,0x8a665a52,0x5bef2733,0xba35d9bc,0x6d26644c, + 0x385cdce1,0x509e4280,0x12aa9ed7,0xf5314d21,0xbe249d4a,0xf32e9753,0x91821cf9,0x01d63491, + 0x49afa237,0x80e0bc27,0x844d796b,0xeff5ccb7,0x46303091,0x743484b4,0x77de1ab7,0x5ab00bea, + 0x6316cd81,0x8ded07f4,0x3845a3a5,0x206625c4,0x8c123c6f,0xc80a971e,0xd4d4fa3f,0x5eba911d, + 0xee168406,0x61cdcbad,0x981a44cd,0x718d030f,0xf653e92e,0xd5b77859,0x11e9e5d9,0xf6fe6ff3, + 0x5239f010,0xe289b21b,0x0b52832b,0xca700c62,0xee7a5e15,0x8543ce2c,0x94a703cc,0x0b844d34, + 0xf70638e5,0xfa286206,0xf8778906,0x1419e883,0xdb0fc46b,0xbeb74261,0xc6957b62,0x8352d2a8, + 0x460586ce,0x90b28336,0xc9107ea8,0x3590403b,0x259a4279,0x6a1a7bbe,0x0f3b76e1,0x4872a716, + 0xa5bfff13,0x8b30be72,0xe5a68957,0x17dbbc52,0x33a40187,0x7074220c,0xd8221b92,0x40ec7448, + 0x7dbbcdfc,0xd5a9bb83,0xb4c0d25c,0xa0040390,0x6fb429dc,0xb8cede12,0x87d193bd,0x55c6e004 +}; + //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// @@ -155,6 +292,7 @@ struct Iso_Man_t_ Vec_Ptr_t * vTemp2; // other classes int timeHash; int timeFout; + int timeSort; int timeOther; int timeTotal; }; @@ -213,6 +351,35 @@ void Iso_ReadPrimes( char * pFileName ) } } +/**Function************************************************************* + + Synopsis [Read primes from file.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Iso_FindNumbers() +{ + unsigned Nums[1024]; + unsigned char * pNums = (unsigned char *)Nums; + int i, j; + srand( 111 ); + for ( i = 0; i < 1024 * 4; i++ ) + pNums[i] = (unsigned char)rand(); + // write out + for ( i = 0; i < 128; i++ ) + { + printf( " " ); + for ( j = 0; j < 8; j++ ) + printf( "0x%08x,", Nums[i*8+j] ); + printf( "\n" ); + } +} + /**Function************************************************************* Synopsis [] @@ -276,10 +443,11 @@ void Iso_ManStop( Iso_Man_t * p, int fVerbose ) if ( fVerbose ) { p->timeOther = p->timeTotal - p->timeHash - p->timeFout; - ABC_PRTP( "Building ", p->timeFout, p->timeTotal ); - ABC_PRTP( "Hashing ", p->timeHash, p->timeTotal ); - ABC_PRTP( "Other ", p->timeOther, p->timeTotal ); - ABC_PRTP( "TOTAL ", p->timeTotal, p->timeTotal ); + ABC_PRTP( "Building ", p->timeFout, p->timeTotal ); + ABC_PRTP( "Hashing ", p->timeHash-p->timeSort, p->timeTotal ); + ABC_PRTP( "Sorting ", p->timeSort, p->timeTotal ); + ABC_PRTP( "Other ", p->timeOther, p->timeTotal ); + ABC_PRTP( "TOTAL ", p->timeTotal, p->timeTotal ); } Vec_PtrFree( p->vTemp1 ); Vec_PtrFree( p->vTemp2 ); @@ -388,7 +556,7 @@ static inline int Iso_ObjHashAdd( Iso_Man_t * p, Iso_Obj_t * pIso ) void Iso_ManCollectClasses( Iso_Man_t * p ) { Iso_Obj_t * pIso; - int i; + int i, clk = clock(); Vec_PtrClear( p->vSingles ); Vec_PtrClear( p->vClasses ); for ( i = 0; i < p->nBins; i++ ) @@ -402,8 +570,10 @@ void Iso_ManCollectClasses( Iso_Man_t * p ) Vec_PtrPush( p->vSingles, pIso ); } } + clk = clock(); Vec_PtrSort( p->vSingles, (int (*)(void))Iso_ObjCompare ); Vec_PtrSort( p->vClasses, (int (*)(void))Iso_ObjCompare ); + p->timeSort += clock() - clk; assert( Vec_PtrSize(p->vSingles) == p->nSingles ); assert( Vec_PtrSize(p->vClasses) == p->nClasses ); // assign IDs to singletons @@ -439,7 +609,7 @@ Iso_Man_t * Iso_ManCreate( Aig_Man_t * pAig ) continue; pIso = p->pObjs + i; pIso->Level = pObj->Level; - pIso->nFinNeg = Aig_ObjFaninC0(pObj) + Aig_ObjFaninC1(pObj); +// pIso->nFinNeg = Aig_ObjFaninC0(pObj) + Aig_ObjFaninC1(pObj); assert( pIso->FaninSig == 0 ); assert( pIso->FanoutSig == 0 ); diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 1f8d98c0..36e3fbd0 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -846,8 +846,10 @@ void Abc_Init( Abc_Frame_t * pAbc ) } */ { - extern void If_CluTest(); - If_CluTest(); +// extern void If_CluTest(); +// If_CluTest(); +// extern void Iso_QuickSortTest(); +// Iso_QuickSortTest(); } } @@ -8875,7 +8877,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) // Aig_ManInterTest( pAig, 1 ); // Aig_ManSupportsTest( pAig ); // Aig_SupportSizeTest( pAig ); - if ( !fNewAlgo ) + if ( fNewAlgo ) Saig_IsoDetectFast( pAig ); else { -- cgit v1.2.3