Isomorphism checking code.

1 files changed, 579 insertions, 86 deletions

diff --git a/src/aig/gia/giaIso.c b/src/aig/gia/giaIso.c
index aca4ba99..c0feb735 100644
--- a/src/aig/gia/giaIso.c
+++ b/src/aig/gia/giaIso.c
@@ -27,56 +27,47 @@ ABC_NAMESPACE_IMPL_START
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-typedef struct Gia_IsoLnk_t_       Gia_IsoLnk_t;
-struct Gia_IsoLnk_t_ 
-{
-    int              iBeg;
-    int              nSize;
-    int              iPrev;
-    int              iNext;
-};
-
-typedef struct Gia_IsoLst_t_       Gia_IsoLst_t;
-struct Gia_IsoLst_t_ 
-{
-    int              iHead;
-    int              iTail;
-};
-
 typedef struct Gia_IsoMan_t_       Gia_IsoMan_t;
 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;
-    Vec_Int_t *      vFinSig;
     // sorting structures
     Vec_Int_t *      vMap;
     Vec_Int_t *      vSeens;
     Vec_Int_t *      vCounts;
     Vec_Int_t *      vResult;
     // fanout representation
-    Vec_Int_t *      vFanouts;
+    Vec_Int_t *      vFanout;
+    Vec_Int_t *      vFanout2;
     // class representation
     Vec_Int_t *      vItems;
-    Gia_IsoLst_t     List;
-    Gia_IsoLnk_t *   pLinks;
-    Gia_IsoLnk_t *   pLinksFree;
-    int              nLinksUsed;
-    int              nLinksAlloc;
+    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;
 };
 
+static inline int *  Gia_IsoFanoutVec( Vec_Int_t * p, int Id )  { return Vec_IntEntryP( p, Vec_IntEntry(p, Id) );       }
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
@@ -102,9 +93,9 @@ Gia_IsoMan_t * Gia_IsoManStart( Gia_Man_t * pGia )
     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 );
-    p->vFinSig   = Vec_IntAlloc( p->nObjs );
     // sorting structures
     p->vMap      = Vec_IntStartFull( 2*p->nObjs );
     p->vSeens    = Vec_IntAlloc( p->nObjs );
@@ -112,14 +103,22 @@ Gia_IsoMan_t * Gia_IsoManStart( Gia_Man_t * pGia )
     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->vFanouts  = Vec_IntAlloc( 6 * p->nObjs );
+    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 )
@@ -128,9 +127,9 @@ void Gia_IsoManStop( Gia_IsoMan_t * p )
     Vec_IntFree( p->vLevels );
     Vec_IntFree( p->vFin0Levs );
     Vec_IntFree( p->vFin1Levs );
+    Vec_IntFree( p->vFinSig );
     Vec_IntFree( p->vFoutPos );
     Vec_IntFree( p->vFoutNeg );
-    Vec_IntFree( p->vFinSig );
     // sorting structures
     Vec_IntFree( p->vMap );
     Vec_IntFree( p->vSeens );
@@ -138,13 +137,22 @@ void Gia_IsoManStop( Gia_IsoMan_t * p )
     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->vFanouts );
+    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 );
 }
 
@@ -259,8 +267,8 @@ void Gia_IsoCreateFanout( Gia_Man_t * p, Vec_Int_t * vUsed, Vec_Int_t * vRefs, V
         pOff = Vec_IntEntryP( vFanout, Vec_IntEntry(vFanout, pObj->Value) );
         if ( Gia_ObjIsAnd(pObj) )
         {
-            pOff0 = Vec_IntEntryP( vFanout, Vec_IntEntry(vFanout, Gia_ObjFanin0(pObj)->Value) );
-            pOff1 = Vec_IntEntryP( vFanout, Vec_IntEntry(vFanout, Gia_ObjFanin1(pObj)->Value) );
+            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) );
@@ -270,15 +278,15 @@ void Gia_IsoCreateFanout( Gia_Man_t * p, Vec_Int_t * vUsed, Vec_Int_t * vRefs, V
         else if ( Gia_ObjIsRo(p, pObj) )
         {
             pObjRi = Gia_ObjRoToRi(p, pObj);
-            pOff0  = Vec_IntEntryP( vFanout, Vec_IntEntry(vFanout, Gia_ObjFanin0(pObjRi)->Value) );
-            pOff[1+(*pOff)++] = Abc_Var2Lit( Gia_ObjFanin0(pObj)->Value, Gia_ObjFaninC0(pObj) );
-            pOff0[1+(*pOff0)++] = Abc_Var2Lit( pObj->Value, Gia_ObjFaninC0(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) );
         }
     }
     // verify
     Gia_ManForEachObjVec( vUsed, p, pObj, i )
     {
-        nOffset = Vec_IntEntry( vFanout, Vec_IntEntry(vFanout, pObj->Value) );
+        nOffset = *Gia_IsoFanoutVec( vFanout, pObj->Value );
         if ( Gia_ObjIsAnd(pObj) )
             nOffset -= 2;
         else if ( Gia_ObjIsRo(p, pObj) )
@@ -289,6 +297,75 @@ void Gia_IsoCreateFanout( Gia_Man_t * p, Vec_Int_t * vUsed, Vec_Int_t * vRefs, V
 
 /**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 )
+{
+    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]) );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_IsoCreateFanout2( Gia_IsoMan_t * p )
+{
+    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 )
+    {
+        if ( Entry >= 0 )
+            continue;
+        Vec_IntWriteEntry( p->vFanout2, i, nOffset );
+        Vec_IntWriteEntry( p->vFanout2, nOffset, 0 );
+        nOffset += 2 + *Gia_IsoFanoutVec(p->vFanout, i);
+    }
+    assert( nOffset == Vec_IntSize(p->vUsed) + 2 * nLeftover + nFanouts );
+    // add currently available items
+    Vec_IntForEachEntry( p->vUniques, Entry, i )
+    {
+        if ( Entry == -1 )
+            continue;
+        Gia_IsoAddSingletonFanouts( p, i, Entry );
+    }
+}
+
+/**Function*************************************************************
+
   Synopsis    []
 
   Description []
@@ -306,8 +383,8 @@ void Gia_IsoCreateSigs( Gia_IsoMan_t * p )
     Vec_IntClear( p->vFin0Levs );
     Vec_IntClear( p->vFin1Levs );
     Vec_IntClear( p->vFinSig );
-    Vec_IntFill( p->vFoutPos, p->nObjs, 0 );
-    Vec_IntFill( p->vFoutNeg, p->nObjs, 0 );
+    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) )
@@ -338,7 +415,7 @@ void Gia_IsoCreateSigs( Gia_IsoMan_t * p )
         {
             pObjRi = Gia_ObjRoToRi(p->pGia, pObj);
             Vec_IntPush( p->vLevels, 0 );
-            Vec_IntPush( p->vFin0Levs, 1 );
+            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 );
@@ -359,7 +436,11 @@ void Gia_IsoCreateSigs( Gia_IsoMan_t * p )
         }
         else assert( 0 );
     }
-    // create items
+    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 );
@@ -393,8 +474,9 @@ void Gia_IsoSortStats( Vec_Int_t * vItems, Vec_Int_t * vCosts, Vec_Int_t * vMap,
     // collect places
     Vec_IntClear( vSeens );
     Vec_IntClear( vCounts );
-    Vec_IntForEachEntry( vCosts, Entry, i )
+    Vec_IntForEachEntry( vItems, Entry, i )
     {
+        Entry = Vec_IntEntry(vCosts, Entry);
         Place = Vec_IntEntry(vMap, Entry);
         if ( Place == -1 )
         {
@@ -444,25 +526,56 @@ void Gia_IsoSortStats( Vec_Int_t * vItems, Vec_Int_t * vCosts, Vec_Int_t * vMap,
   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 * Gia_IsoCreateStats( Gia_IsoMan_t * p, int iPo )
+{
+    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;
+}
+
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Sorting an array of entries.]
+
+  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.]
+               
+  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 )
 {
-    int i, Entry, Place, Counter;
+    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 );
-    if ( Vec_IntSize(vItems) < 15 )
-    {
-        Vec_IntGrowResize( vResult, Vec_IntSize(vItems) );
-        memmove( Vec_IntArray(vResult),  Vec_IntArray(vItems), sizeof(int) * Vec_IntSize(vItems) );
-        Vec_IntSelectSortCost( Vec_IntArray(vResult), Vec_IntSize(vItems), vCosts );
-        return;
-    }
+
+    // prepare return values
+    Vec_IntClear( vClassNew );
 
     // collect places
     Vec_IntClear( vSeens );
     Vec_IntClear( vCounts );
-    Vec_IntForEachEntry( vCosts, Entry, i )
+    Vec_IntForEachEntry( vItems, Entry0, i )
     {
+        Entry = Vec_IntEntry(vCosts, Entry0);
         Place = Vec_IntEntry(vMap, Entry);
         if ( Place == -1 )
         {
@@ -474,29 +587,45 @@ void Gia_IsoSortVec( Vec_Int_t * vItems, Vec_Int_t * vCosts, Vec_Int_t * vMap, V
             Vec_IntAddToEntry( vCounts, Place, 1 );
     }
 
-    // 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 )
+    // check if refinement is happening
+    if ( Vec_IntSize(vSeens) == 1 ) // there is no refinement
     {
-        Place = Vec_IntEntry( vMap, Entry ); 
-        Vec_IntWriteEntry( vMap, Entry, Counter );
-        Counter += Vec_IntEntry( vCounts, Place );
+        Vec_IntPush( vClassNew, 0 );
+        Vec_IntPush( vClassNew, Vec_IntSize(vItems) );
+        // no need to change vItems
     }
-    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, Entry, i )
+    else // complete or partial refinement
     {
-        Place = Vec_IntAddToEntry( vMap, Entry, 1 ) - 1;
-        Vec_IntWriteEntry( vResult, Place, Entry );
+        // 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) );
     }
-    Vec_IntForEachEntry( vResult, Entry, i ) // verify
-        assert( Entry >= 0 );
 
     // clean map
     Vec_IntForEachEntry( vSeens, Entry, i )
@@ -505,6 +634,114 @@ void Gia_IsoSortVec( Vec_Int_t * vItems, Vec_Int_t * vCosts, Vec_Int_t * vMap, V
 
 /**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 );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Updates current equivalence classes.]]
+
+  Description [
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Gia_IsoRefine( Gia_IsoMan_t * p, Vec_Int_t * vParam )
+{
+    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 )
+    {
+        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 ( nSize2 == 1 )
+            {
+                Gia_IsoAddSingleton( p, Vec_IntEntry(p->vItems, Begin+Begin2) );
+                Counter++;
+                continue;
+            }
+            Vec_IntPush( p->vClass2, Begin+Begin2 );
+            Vec_IntPush( p->vClass2, nSize2 );
+        }
+    }
+    // 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 )
+        {
+            assert( nSize > 0 );
+            assert( Vec_IntEntry(p->vLevels, Vec_IntEntry(p->vItems, Begin)) == i );
+            Vec_IntPush( p->vLevelLim, Begin );
+        }
+        Vec_IntPush( p->vLevelLim, Vec_IntSize(p->vItems) );
+    }
+    return Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Gia_IsoAssignUniqueToLastLevel( Gia_IsoMan_t * p )
+{
+    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;
+}
+
+/**Function*************************************************************
+
   Synopsis    []
 
   Description []
@@ -514,17 +751,32 @@ void Gia_IsoSortVec( Vec_Int_t * vItems, Vec_Int_t * vCosts, Vec_Int_t * vMap, V
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Int_t * Gia_IsoCreateStats( Gia_IsoMan_t * p )
+void Gia_IsoPrint( Gia_IsoMan_t * p, int Iter, int nSingles, int Time )
 {
-    Vec_Int_t * vRes;
-    vRes = Vec_IntAlloc( 1000 );
-    Gia_IsoSortStats( p->vItems, p->vLevels,   p->vMap, p->vSeens, p->vCounts, p->vResult );   Vec_IntAppend( vRes, p->vResult );
-    Gia_IsoSortStats( p->vItems, p->vFin0Levs, p->vMap, p->vSeens, p->vCounts, p->vResult );   Vec_IntAppend( vRes, p->vResult );
-    Gia_IsoSortStats( p->vItems, p->vFin1Levs, p->vMap, p->vSeens, p->vCounts, p->vResult );   Vec_IntAppend( vRes, p->vResult );
-    Gia_IsoSortStats( p->vItems, p->vFoutPos,  p->vMap, p->vSeens, p->vCounts, p->vResult );   Vec_IntAppend( vRes, p->vResult );
-    Gia_IsoSortStats( p->vItems, p->vFoutNeg,  p->vMap, p->vSeens, p->vCounts, p->vResult );   Vec_IntAppend( vRes, p->vResult );
-    Gia_IsoSortStats( p->vItems, p->vFinSig,   p->vMap, p->vSeens, p->vCounts, p->vResult );   Vec_IntAppend( vRes, p->vResult );
-    return vRes;
+    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*************************************************************
@@ -538,15 +790,130 @@ Vec_Int_t * Gia_IsoCreateStats( Gia_IsoMan_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Int_t * Gia_IsoOne( Gia_IsoMan_t * p, int iPo )
+void Gia_IsoCreateUniques( Gia_IsoMan_t * p, int iPo )
 {
-    Vec_Int_t * vStats = NULL;
+    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 );
-//    Gia_IsoCreateFanout( p->pGia, p->vUsed, p->vRefs, p->vFanouts );
-    Gia_IsoCreateSigs( p );
-    vStats = Gia_IsoCreateStats( p );
+    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++ )
+    {
+        nSingles = Gia_IsoRefine( p, vArray[i] );
+        Gia_IsoPrint( p, i+1, nSingles, clock() - clk );
+    }
+    // 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++ )
+    {
+        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 );
+        }
+    }
+    // finished refinement
     Gia_IsoCleanUsed( p->pGia, p->vUsed );
-    return vStats;
+}
+
+/**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.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_ManFindIsoPermCos( Gia_Man_t * p, Vec_Int_t * vPermCis, Vec_Ptr_t * vTemp, Vec_Int_t * vRes )
+{
+    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
+    {
+        Vec_PtrClear( vTemp );
+        Gia_ManForEachPo( p, pObj, i )
+        {
+            pObj->Value = Abc_Var2Lit( Gia_ObjFanin0(pObj)->Value, Gia_ObjFaninC0(pObj) );
+            Vec_PtrPush( vTemp, pObj );
+        }
+        Vec_PtrSort( vTemp, (int (*)(void))Gia_ObjCompareByValue );
+        Vec_PtrForEachEntry( Gia_Obj_t *, vTemp, pObj, i )
+            Vec_IntPush( 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 );
+}
+
+/**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*************************************************************
@@ -560,6 +927,23 @@ Vec_Int_t * Gia_IsoOne( Gia_IsoMan_t * p, int iPo )
   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;
@@ -571,16 +955,15 @@ void Gia_IsoTest( Gia_Man_t * pGia )
     p = Gia_IsoManStart( pGia );
     for ( i = 0; i < Gia_ManPoNum(pGia); i++ )
     {
-        if ( i % 1000 == 0 )
+        if ( i % 100 == 0 )
             printf( "Finished %5d\r", i );
-        vStats = Gia_IsoOne( p, i );
+        vStats = Gia_IsoCreateStats( p, i );
         Vec_PtrPush( p->vResults, vStats );
         if ( fVerbose )
         printf( "%d ", Vec_IntSize(vStats)/2 );
     }
     if ( fVerbose )
     printf( "               \n" );
-
     vResults = p->vResults;
     p->vResults = NULL;
     Gia_IsoManStop( p );
@@ -590,6 +973,116 @@ void Gia_IsoTest( Gia_Man_t * pGia )
 }
 
 
+/**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                                ///