Isomorphism checking code.

1 files changed, 361 insertions, 869 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,30 +490,58 @@ 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*************************************************************
@@ -911,179 +555,27 @@ void Gia_ManFindIsoPermCos( Gia_Man_t * p, Vec_Int_t * vPermCis, Vec_Ptr_t * vTe
   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    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
 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                                ///
 ////////////////////////////////////////////////////////////////////////