Graph isomorphism checking code.

17 files changed, 1455 insertions, 532 deletions

diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h
index 0a2ea6b6..52985546 100644
--- a/src/aig/aig/aig.h
+++ b/src/aig/aig/aig.h
@@ -504,6 +504,7 @@ extern Aig_Man_t *     Aig_ManDupOrpos( Aig_Man_t * p, int fAddRegs );
 extern Aig_Man_t *     Aig_ManDupOneOutput( Aig_Man_t * p, int iPoNum, int fAddRegs );
 extern Aig_Man_t *     Aig_ManDupUnsolvedOutputs( Aig_Man_t * p, int fAddRegs );
 extern Aig_Man_t *     Aig_ManDupArray( Vec_Ptr_t * vArray );
+extern Aig_Man_t *     Aig_ManDupNodes( Aig_Man_t * pMan, Vec_Ptr_t * vArray );
 /*=== aigFanout.c ==========================================================*/
 extern void            Aig_ObjAddFanout( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pFanout );
 extern void            Aig_ObjRemoveFanout( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pFanout );
diff --git a/src/aig/aig/aigDup.c b/src/aig/aig/aigDup.c
index c2127262..59547586 100644
--- a/src/aig/aig/aigDup.c
+++ b/src/aig/aig/aigDup.c
@@ -1342,6 +1342,43 @@ Aig_Man_t * Aig_ManDupArray( Vec_Ptr_t * vArray )
     return pNew;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Duplicates AIG with only one primary output.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Aig_ManDupNodes( Aig_Man_t * pMan, Vec_Ptr_t * vArray )
+{
+    Aig_Man_t * pNew;
+    Vec_Ptr_t * vObjs;
+    Aig_Obj_t * pObj;
+    int i;
+    if ( Vec_PtrSize(vArray) == 0 )
+        return NULL;
+    vObjs = Aig_ManDfsNodes( pMan, (Aig_Obj_t **)Vec_PtrArray(vArray), Vec_PtrSize(vArray) );
+    // create the new manager
+    pNew = Aig_ManStart( 10000 );
+    pNew->pName = Abc_UtilStrsav( pMan->pName );
+    Aig_ManConst1(pMan)->pData = Aig_ManConst1(pNew);
+    Vec_PtrForEachEntry( Aig_Obj_t *, vObjs, pObj, i )
+        if ( Aig_ObjIsPi(pObj) )
+            pObj->pData = Aig_ObjCreatePi(pNew);
+    Vec_PtrForEachEntry( Aig_Obj_t *, vObjs, pObj, i )
+        if ( Aig_ObjIsNode(pObj) )
+            pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
+    Vec_PtrForEachEntry( Aig_Obj_t *, vArray, pObj, i )
+            Aig_ObjCreatePo( pNew, pObj->pData );
+    Aig_ManSetRegNum( pNew, 0 );
+    Vec_PtrFree( vObjs );
+    return pNew;
+}
+
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
diff --git a/src/aig/aig/module.make b/src/aig/aig/module.make
index 04fe8771..aaf5bf6d 100644
--- a/src/aig/aig/module.make
+++ b/src/aig/aig/module.make
@@ -6,7 +6,6 @@ SRC +=    src/aig/aig/aigCheck.c \
     src/aig/aig/aigFanout.c \
     src/aig/aig/aigFrames.c \
     src/aig/aig/aigInter.c \
-    src/aig/aig/aigIso.c \
     src/aig/aig/aigJust.c \
     src/aig/aig/aigMan.c \
     src/aig/aig/aigMem.c \
diff --git a/src/aig/ioa/ioa.h b/src/aig/ioa/ioa.h
index b86bc13a..a427f507 100644
--- a/src/aig/ioa/ioa.h
+++ b/src/aig/ioa/ioa.h
@@ -65,6 +65,7 @@ ABC_NAMESPACE_HEADER_START
 extern Aig_Man_t *    Ioa_ReadAigerFromMemory( char * pContents, int nFileSize, int fCheck );
 extern Aig_Man_t *    Ioa_ReadAiger( char * pFileName, int fCheck );
 /*=== ioaWriteAig.c =======================================================*/
+extern Vec_Str_t *    Ioa_WriteAigerIntoMemoryStr( Aig_Man_t * pMan );
 extern char *         Ioa_WriteAigerIntoMemory( Aig_Man_t * pMan, int * pnSize );
 extern void           Ioa_WriteAiger( Aig_Man_t * pMan, char * pFileName, int fWriteSymbols, int fCompact );
 /*=== ioaUtil.c =======================================================*/
diff --git a/src/aig/ioa/ioaWriteAig.c b/src/aig/ioa/ioaWriteAig.c
index 2f682775..d19d23ff 100644
--- a/src/aig/ioa/ioaWriteAig.c
+++ b/src/aig/ioa/ioaWriteAig.c
@@ -283,9 +283,8 @@ Vec_Str_t * Ioa_WriteEncodeLiterals( Vec_Int_t * vLits )
   SeeAlso     []
 
 ***********************************************************************/
-char * Ioa_WriteAigerIntoMemory( Aig_Man_t * pMan, int * pnSize )
+Vec_Str_t * Ioa_WriteAigerIntoMemoryStr( Aig_Man_t * pMan )
 {
-    char * pBuffer;
     Vec_Str_t * vBuffer;
     Aig_Obj_t * pObj, * pDriver;
     int nNodes, i, uLit, uLit0, uLit1; 
@@ -357,10 +356,28 @@ char * Ioa_WriteAigerIntoMemory( Aig_Man_t * pMan, int * pnSize )
         Ioa_WriteAigerEncodeStr( vBuffer, uLit  - uLit1 );
         Ioa_WriteAigerEncodeStr( vBuffer, uLit1 - uLit0 );
     }
-//    fprintf( pFile, "c" );
-//    if ( pMan->pName )
-//        fprintf( pFile, "n%s%c", pMan->pName, '\0' );
     Vec_StrPrintStr( vBuffer, "c" );
+    return vBuffer;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Writes the AIG in into the memory buffer.]
+
+  Description [The resulting buffer constains the AIG in AIGER format. 
+  The returned size (pnSize) gives the number of bytes in the buffer. 
+  The resulting buffer should be deallocated by the user.]
+  
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+char * Ioa_WriteAigerIntoMemory( Aig_Man_t * pMan, int * pnSize )
+{
+    char * pBuffer;
+    Vec_Str_t * vBuffer;
+    vBuffer = Ioa_WriteAigerIntoMemoryStr( pMan );
     if ( pMan->pName )
     {
         Vec_StrPrintStr( vBuffer, "n" );
diff --git a/src/aig/saig/module.make b/src/aig/saig/module.make
index 327b9dd5..42e3c090 100644
--- a/src/aig/saig/module.make
+++ b/src/aig/saig/module.make
@@ -18,6 +18,9 @@ SRC +=    src/aig/saig/saigAbs.c \
     src/aig/saig/saigHaig.c \
     src/aig/saig/saigInd.c \
     src/aig/saig/saigIoa.c \
+    src/aig/saig/saigIso.c \
+    src/aig/saig/saigIsoFast.c \
+    src/aig/saig/saigIsoSlow.c \
     src/aig/saig/saigMiter.c \
     src/aig/saig/saigOutDec.c \
     src/aig/saig/saigPhase.c \
diff --git a/src/aig/saig/saig.h b/src/aig/saig/saig.h
index 74566966..218cb31c 100644
--- a/src/aig/saig/saig.h
+++ b/src/aig/saig/saig.h
@@ -182,6 +182,12 @@ extern int               Saig_ManInduction( Aig_Man_t * p, int nFramesMax, int n
 /*=== saigIoa.c ==========================================================*/
 extern void              Saig_ManDumpBlif( Aig_Man_t * p, char * pFileName );
 extern Aig_Man_t *       Saig_ManReadBlif( char * pFileName );
+/*=== saigIso.c ==========================================================*/
+extern Vec_Int_t *       Saig_ManFindIsoPerm( Aig_Man_t * pAig, int fVerbose );
+extern Aig_Man_t *       Saig_ManDupIsoCanonical( Aig_Man_t * pAig, int fVerbose );
+extern Aig_Man_t *       Saig_ManIsoReduce( Aig_Man_t * pAig, int fVerbose );
+/*=== saigIsoFast.c ==========================================================*/
+extern Vec_Vec_t *       Saig_IsoDetectFast( Aig_Man_t * pAig );
 /*=== saigMiter.c ==========================================================*/
 extern Sec_MtrStatus_t   Sec_MiterStatus( Aig_Man_t * p );
 extern Aig_Man_t *       Saig_ManCreateMiter( Aig_Man_t * p1, Aig_Man_t * p2, int Oper );
diff --git a/src/aig/saig/saigIso.c b/src/aig/saig/saigIso.c
new file mode 100644
index 00000000..1001f153
--- /dev/null
+++ b/src/aig/saig/saigIso.c
@@ -0,0 +1,597 @@
+/**CFile****************************************************************
+
+  FileName    [saigIso.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Sequential AIG package.]
+
+  Synopsis    [Sequential cleanup.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: saigIso.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "src/aig/ioa/ioa.h"
+#include "saig.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Find the canonical permutation of the COs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Saig_ManFindIsoPermCos( Aig_Man_t * pAig, Vec_Int_t * vPermCis )
+{
+    extern int Iso_ObjCompareAigObjByData( Aig_Obj_t ** pp1, Aig_Obj_t ** pp2 );
+    Vec_Int_t * vPermCos;
+    Aig_Obj_t * pObj, * pFanin;
+    int i, Entry, Diff;
+    assert( Vec_IntSize(vPermCis) == Aig_ManPiNum(pAig) );
+    vPermCos = Vec_IntAlloc( Aig_ManPoNum(pAig) );
+    if ( Saig_ManPoNum(pAig) == 1 )
+        Vec_IntPush( vPermCos, 0 );
+    else
+    {
+        Vec_Ptr_t * vRoots = Vec_PtrAlloc( Saig_ManPoNum(pAig) );
+        Saig_ManForEachPo( pAig, pObj, i )
+        {
+            pFanin = Aig_ObjFanin0(pObj);
+            assert( Aig_ObjIsConst1(pFanin) || pFanin->iData > 0 );
+            pObj->iData = Abc_Var2Lit( pFanin->iData, Aig_ObjFaninC0(pObj) );
+            Vec_PtrPush( vRoots, pObj );
+        }
+        Vec_PtrSort( vRoots, (int (*)(void))Iso_ObjCompareAigObjByData );
+        Vec_PtrForEachEntry( Aig_Obj_t *, vRoots, pObj, i )
+            Vec_IntPush( vPermCos, Aig_ObjPioNum(pObj) );
+        Vec_PtrFree( vRoots );
+    }
+    // add flop outputs
+    Diff = Saig_ManPoNum(pAig) - Saig_ManPiNum(pAig);
+    Vec_IntForEachEntryStart( vPermCis, Entry, i, Saig_ManPiNum(pAig) )
+        Vec_IntPush( vPermCos, Entry + Diff );
+    return vPermCos;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs canonical duplication of the AIG.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Saig_ManDupIsoCanonical_rec( Aig_Man_t * pNew, Aig_Man_t * pAig, Aig_Obj_t * pObj )
+{
+    if ( Aig_ObjIsTravIdCurrent(pAig, pObj) )
+        return;
+    Aig_ObjSetTravIdCurrent(pAig, pObj);
+    assert( Aig_ObjIsNode(pObj) );
+    if ( !Aig_ObjIsNode(Aig_ObjFanin0(pObj)) || !Aig_ObjIsNode(Aig_ObjFanin1(pObj)) )
+    {
+        Saig_ManDupIsoCanonical_rec( pNew, pAig, Aig_ObjFanin0(pObj) );
+        Saig_ManDupIsoCanonical_rec( pNew, pAig, Aig_ObjFanin1(pObj) );
+    }
+    else
+    {
+        assert( Aig_ObjFanin0(pObj)->iData != Aig_ObjFanin1(pObj)->iData );
+        if ( Aig_ObjFanin0(pObj)->iData < Aig_ObjFanin1(pObj)->iData )
+        {
+            Saig_ManDupIsoCanonical_rec( pNew, pAig, Aig_ObjFanin0(pObj) );
+            Saig_ManDupIsoCanonical_rec( pNew, pAig, Aig_ObjFanin1(pObj) );
+        }
+        else
+        {
+            Saig_ManDupIsoCanonical_rec( pNew, pAig, Aig_ObjFanin1(pObj) );
+            Saig_ManDupIsoCanonical_rec( pNew, pAig, Aig_ObjFanin0(pObj) );
+        }
+    }
+    pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs canonical duplication of the AIG.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Saig_ManDupIsoCanonical( Aig_Man_t * pAig, int fVerbose )
+{
+    Aig_Man_t * pNew;
+    Aig_Obj_t * pObj;
+    Vec_Int_t * vPerm, * vPermCo;
+    int i, Entry;
+    // derive permutations
+    vPerm   = Saig_ManFindIsoPerm( pAig, fVerbose );
+    vPermCo = Saig_ManFindIsoPermCos( pAig, vPerm );
+    // create the new manager
+    pNew = Aig_ManStart( Aig_ManNodeNum(pAig) );
+    pNew->pName = Abc_UtilStrsav( pAig->pName );
+    Aig_ManIncrementTravId( pAig );
+    // create constant
+    pObj = Aig_ManConst1(pAig);
+    pObj->pData = Aig_ManConst1(pNew);
+    Aig_ObjSetTravIdCurrent( pAig, pObj );
+    // create PIs
+    Vec_IntForEachEntry( vPerm, Entry, i )
+    {
+        pObj = Aig_ManPi(pAig, Entry);
+        pObj->pData = Aig_ObjCreatePi(pNew);
+        Aig_ObjSetTravIdCurrent( pAig, pObj );
+    }
+    // traverse from the POs
+    Vec_IntForEachEntry( vPermCo, Entry, i )
+    {
+        pObj = Aig_ManPo(pAig, Entry);
+        Saig_ManDupIsoCanonical_rec( pNew, pAig, Aig_ObjFanin0(pObj) );
+    }
+    // create POs
+    Vec_IntForEachEntry( vPermCo, Entry, i )
+    {
+        pObj = Aig_ManPo(pAig, Entry);
+        Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
+    }
+    Aig_ManSetRegNum( pNew, Aig_ManRegNum(pAig) );
+    Vec_IntFreeP( &vPerm );
+    Vec_IntFreeP( &vPermCo );
+    return pNew;
+}
+
+
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Checks structural equivalence of AIG1 and AIG2.]
+
+  Description [Returns 1 if AIG1 and AIG2 are structurally equivalent 
+  under this mapping.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Iso_ManCheckMapping( Aig_Man_t * pAig1, Aig_Man_t * pAig2, Vec_Int_t * vMap2to1, int fVerbose )
+{
+    Aig_Obj_t * pObj, * pFanin0, * pFanin1;
+    int i;
+    assert( Aig_ManPiNum(pAig1) == Aig_ManPiNum(pAig2) );
+    assert( Aig_ManPoNum(pAig1) == Aig_ManPoNum(pAig2) );
+    assert( Aig_ManRegNum(pAig1) == Aig_ManRegNum(pAig2) );
+    assert( Aig_ManNodeNum(pAig1) == Aig_ManNodeNum(pAig2) );
+    Aig_ManCleanData( pAig1 );
+    // map const and PI nodes
+    Aig_ManConst1(pAig2)->pData = Aig_ManConst1(pAig1);
+    Aig_ManForEachPi( pAig2, pObj, i )
+        pObj->pData = Aig_ManPi( pAig1, Vec_IntEntry(vMap2to1, i) );
+    // try internal nodes
+    Aig_ManForEachNode( pAig2, pObj, i )
+    {
+        pFanin0 = Aig_ObjChild0Copy( pObj );
+        pFanin1 = Aig_ObjChild1Copy( pObj );
+        pObj->pData = Aig_TableLookupTwo( pAig1, pFanin0, pFanin1 );
+        if ( pObj->pData == NULL )
+        {
+            if ( fVerbose )
+                printf( "Structural equivalence failed at node %d.\n", i );
+            return 0;
+        }
+    }
+    // make sure the first PO points to the same node
+    if ( Aig_ManPoNum(pAig1)-Aig_ManRegNum(pAig1) == 1 && Aig_ObjChild0Copy(Aig_ManPo(pAig2, 0)) != Aig_ObjChild0(Aig_ManPo(pAig1, 0)) )
+    {
+        if ( fVerbose )
+            printf( "Structural equivalence failed at primary output 0.\n" );
+        return 0;
+    }
+    return 1;    
+}
+
+//static int s_Counter;
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Iso_ManNegEdgeNum( Aig_Man_t * pAig )
+{
+    Aig_Obj_t * pObj;
+    int i, Counter = 0;
+    if ( pAig->nComplEdges > 0 )
+        return pAig->nComplEdges;
+    Aig_ManForEachObj( pAig, pObj, i )
+        if ( Aig_ObjIsNode(pObj) )
+        {
+            Counter += Aig_ObjFaninC0(pObj);
+            Counter += Aig_ObjFaninC1(pObj);
+        }
+        else if ( Aig_ObjIsPo(pObj) )
+            Counter += Aig_ObjFaninC0(pObj);
+    return (pAig->nComplEdges = Counter);
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Finds mapping of CIs of AIG2 into those of AIG1.]
+
+  Description [Returns the mapping of CIs of the two AIGs, or NULL
+  if there is no mapping.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Iso_ManFindMapping( Aig_Man_t * pAig1, Aig_Man_t * pAig2, Vec_Int_t * vPerm1_, Vec_Int_t * vPerm2_, int fVerbose )
+{
+    Vec_Int_t * vPerm1, * vPerm2, * vInvPerm2;
+    int i, Entry;
+    if ( Aig_ManPiNum(pAig1) != Aig_ManPiNum(pAig2) )
+        return NULL;
+    if ( Aig_ManPoNum(pAig1) != Aig_ManPoNum(pAig2) )
+        return NULL;
+    if ( Aig_ManRegNum(pAig1) != Aig_ManRegNum(pAig2) )
+        return NULL;
+    if ( Aig_ManNodeNum(pAig1) != Aig_ManNodeNum(pAig2) )
+        return NULL;
+    if ( Aig_ManLevelNum(pAig1) != Aig_ManLevelNum(pAig2) )
+        return NULL;
+//    if ( Iso_ManNegEdgeNum(pAig1) != Iso_ManNegEdgeNum(pAig2) )
+//        return NULL;
+//    s_Counter++;
+
+    if ( fVerbose ) 
+        printf( "AIG1:\n" );
+    vPerm1 = vPerm1_ ? vPerm1_ : Saig_ManFindIsoPerm( pAig1, fVerbose );
+    if ( fVerbose )
+        printf( "AIG1:\n" );
+    vPerm2 = vPerm2_ ? vPerm2_ : Saig_ManFindIsoPerm( pAig2, fVerbose );
+    if ( vPerm1_ )
+        assert( Vec_IntSize(vPerm1_) == Aig_ManPiNum(pAig1) );
+    if ( vPerm2_ )
+        assert( Vec_IntSize(vPerm2_) == Aig_ManPiNum(pAig2) );
+    // find canonical permutation
+    // vPerm1/vPerm2 give canonical order of CIs of AIG1/AIG2
+    vInvPerm2 = Vec_IntInvert( vPerm2, -1 );
+    Vec_IntForEachEntry( vInvPerm2, Entry, i )
+    {
+        assert( Entry >= 0 && Entry < Aig_ManPiNum(pAig1) );
+        Vec_IntWriteEntry( vInvPerm2, i, Vec_IntEntry(vPerm1, Entry) );
+    }
+    if ( vPerm1_ == NULL )
+        Vec_IntFree( vPerm1 );
+    if ( vPerm2_ == NULL )
+        Vec_IntFree( vPerm2 );
+    // check if they are indeed equivalent
+    if ( !Iso_ManCheckMapping( pAig1, pAig2, vInvPerm2, fVerbose ) )
+        Vec_IntFreeP( &vInvPerm2 );
+    return vInvPerm2;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Iso_ManFilterPos_old( Aig_Man_t * pAig, int fVerbose )
+{
+    int fVeryVerbose = 0;
+    Vec_Ptr_t * vParts, * vPerms, * vAigs;
+    Vec_Int_t * vPos, * vMap;
+    Aig_Man_t * pPart, * pTemp;
+    int i, k, nPos;
+
+    // derive AIG for each PO
+    nPos = Aig_ManPoNum(pAig) - Aig_ManRegNum(pAig);
+    vParts = Vec_PtrAlloc( nPos );
+    vPerms = Vec_PtrAlloc( nPos );
+    for ( i = 0; i < nPos; i++ )
+    {
+        pPart = Saig_ManDupCones( pAig, &i, 1 );
+        vMap  = Saig_ManFindIsoPerm( pPart, fVeryVerbose );
+        Vec_PtrPush( vParts, pPart ); 
+        Vec_PtrPush( vPerms, vMap );
+    }
+//    s_Counter = 0;
+
+    // check AIGs for each PO
+    vAigs = Vec_PtrAlloc( 1000 );
+    vPos  = Vec_IntAlloc( 1000 );
+    Vec_PtrForEachEntry( Aig_Man_t *, vParts, pPart, i )
+    {
+        if ( fVeryVerbose )
+        {
+            printf( "AIG %4d : ", i );
+            Aig_ManPrintStats( pPart );
+        }
+        Vec_PtrForEachEntry( Aig_Man_t *, vAigs, pTemp, k )
+        {
+            if ( fVeryVerbose )
+                printf( "Comparing AIG %4d and AIG %4d.  ", Vec_IntEntry(vPos,k), i );
+            vMap = Iso_ManFindMapping( pTemp, pPart, 
+                (Vec_Int_t *)Vec_PtrEntry(vPerms, Vec_IntEntry(vPos,k)), 
+                (Vec_Int_t *)Vec_PtrEntry(vPerms, i),
+                fVeryVerbose );
+            if ( vMap != NULL )
+            {
+                if ( fVeryVerbose )
+                    printf( "Found match\n" );
+                if ( fVerbose )
+                    printf( "Found match for AIG %4d and AIG %4d.\n", Vec_IntEntry(vPos,k), i );
+                Vec_IntFree( vMap );
+                break;
+            }
+            if ( fVeryVerbose )
+                printf( "No match.\n" );
+        }
+        if ( k == Vec_PtrSize(vAigs) )
+        {
+            Vec_PtrPush( vAigs, pPart );
+            Vec_IntPush( vPos, i );
+        }
+    }
+    // delete AIGs
+    Vec_PtrForEachEntry( Aig_Man_t *, vParts, pPart, i )
+        Aig_ManStop( pPart );
+    Vec_PtrFree( vParts );
+    Vec_PtrForEachEntry( Vec_Int_t *, vPerms, vMap, i )
+        Vec_IntFree( vMap );
+    Vec_PtrFree( vPerms );
+    // derive the resulting AIG
+    pPart = Saig_ManDupCones( pAig, Vec_IntArray(vPos), Vec_IntSize(vPos) );
+    Vec_PtrFree( vAigs );
+    Vec_IntFree( vPos );
+
+//    printf( "The number of all checks %d.  Complex checks %d.\n", nPos*(nPos-1)/2, s_Counter );
+    return pPart;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Takes multi-output sequential AIG.]
+
+  Description [Returns candidate equivalence classes of POs.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Iso_StoCompareVecStr( Vec_Str_t ** p1, Vec_Str_t ** p2 )
+{
+    return Vec_StrCompareVec( *p1, *p2 );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Iso_ManFilterPos( Aig_Man_t * pAig, int fVerbose )
+{
+    int fVeryVerbose = 0;
+    Aig_Man_t * pPart, * pTemp;
+    Vec_Ptr_t * vBuffers, * vClasses;
+    Vec_Int_t * vLevel, * vRemain;
+    Vec_Str_t * vStr, * vPrev;
+    int i, nPos, nUnique = 0, clk = clock();
+
+    // derive AIG for each PO
+    nPos = Aig_ManPoNum(pAig) - Aig_ManRegNum(pAig);
+    vBuffers = Vec_PtrAlloc( nPos );
+    for ( i = 0; i < nPos; i++ )
+    {
+//        if ( i % 100 == 0 )
+//            printf( "%d finished...\n", i );
+        pPart = Saig_ManDupCones( pAig, &i, 1 );
+        pTemp = Saig_ManDupIsoCanonical( pPart, 0 );
+        vStr  = Ioa_WriteAigerIntoMemoryStr( pTemp );
+        Vec_PtrPush( vBuffers, vStr );
+        Aig_ManStop( pTemp );
+        Aig_ManStop( pPart );
+        // remember the output number in nCap (attention: hack!)
+        vStr->nCap = i;
+    }
+//    s_Counter = 0;
+    if ( fVerbose )
+    Abc_PrintTime( 1, "Isomorph time", clock() - clk );
+
+    // sort the infos
+    clk = clock();
+    Vec_PtrSort( vBuffers, (int (*)(void))Iso_StoCompareVecStr );
+
+    // create classes
+    clk = clock();
+    vClasses = Vec_PtrAlloc( Saig_ManPoNum(pAig) );
+    // 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", Saig_ManPoNum(pAig), 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
+    pPart = Saig_ManDupCones( pAig, 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 pPart;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Iso_ManTest( Aig_Man_t * pAig, int fVerbose )
+{
+    Vec_Int_t * vPerm;
+    int clk = clock();
+    vPerm = Saig_ManFindIsoPerm( pAig, fVerbose );
+    Vec_IntFree( vPerm );
+    Abc_PrintTime( 1, "Time", clock() - clk );
+    return NULL;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Saig_ManIsoReduce( Aig_Man_t * pAig, int fVerbose )
+{ 
+    Aig_Man_t * pPart;
+    int clk = clock();
+    pPart = Iso_ManFilterPos( pAig, fVerbose );
+    printf( "Reduced %d outputs to %d outputs.  ", Saig_ManPoNum(pAig), Saig_ManPoNum(pPart) );
+    Abc_PrintTime( 1, "Time", clock() - clk );
+//    Aig_ManStop( pPart );
+    return pPart;
+}
+
+
+#include "src/base/abc/abc.h"
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Iso_ManTest888( Aig_Man_t * pAig1, int fVerbose )
+{
+    extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
+    extern Abc_Ntk_t * Abc_NtkFromAigPhase( Aig_Man_t * pMan );
+    Abc_Ntk_t * pNtk;
+    Aig_Man_t * pAig2;
+    Vec_Int_t * vMap;
+    
+    pNtk = Abc_NtkFromAigPhase( pAig1 );
+    Abc_NtkPermute( pNtk, 1, 0, 1 );
+    pAig2 = Abc_NtkToDar( pNtk, 0, 1 );
+    Abc_NtkDelete( pNtk );
+
+    vMap = Iso_ManFindMapping( pAig1, pAig2, NULL, NULL, fVerbose );
+    Aig_ManStop( pAig2 );
+
+    if ( vMap != NULL )
+    {
+        printf( "Mapping of AIGs is found.\n" );
+        if ( fVerbose )
+            Vec_IntPrint( vMap );
+    }
+    else
+        printf( "Mapping of AIGs is NOT found.\n" );
+    Vec_IntFreeP( &vMap );
+    return NULL;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/saig/saigIsoFast.c b/src/aig/saig/saigIsoFast.c
new file mode 100644
index 00000000..6556b90f
--- /dev/null
+++ b/src/aig/saig/saigIsoFast.c
@@ -0,0 +1,352 @@
+/**CFile****************************************************************
+
+  FileName    [aigIsoFast.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [AIG package.]
+
+  Synopsis    [Graph isomorphism package.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - April 28, 2007.]
+
+  Revision    [$Id: aigIsoFast.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "saig.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+#define AIG_ISO_NUM 16
+
+typedef struct Iso_Dat_t_ Iso_Dat_t;
+struct Iso_Dat_t_
+{
+    unsigned      nFiNeg    :  3;
+    unsigned      nFoNeg    :  2;
+    unsigned      nFoPos    :  2;
+    unsigned      Fi0Lev    :  3;
+    unsigned      Fi1Lev    :  3;
+    unsigned      Level     :  3;
+    unsigned      fVisit    : 16;
+};
+
+typedef struct Iso_Dat2_t_ Iso_Dat2_t;
+struct Iso_Dat2_t_
+{
+    unsigned      Data      : 16;
+};
+
+typedef struct Iso_Sto_t_ Iso_Sto_t;
+struct Iso_Sto_t_
+{
+    Aig_Man_t *   pAig;       // user's AIG manager
+    int           nObjs;      // number of objects
+    Iso_Dat_t *   pData;      // data for each object
+    Vec_Int_t *   vVisited;   // visited nodes
+    Vec_Ptr_t *   vRoots;     // root nodes
+    Vec_Int_t *   vPlaces;    // places in the counter lists
+    int *         pCounters;  // counters    
+};
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Iso_Sto_t * Iso_StoStart( Aig_Man_t * pAig )
+{
+    Iso_Sto_t * p;
+    p = ABC_CALLOC( Iso_Sto_t, 1 );
+    p->pAig      = pAig;
+    p->nObjs     = Aig_ManObjNumMax( pAig );
+    p->pData     = ABC_CALLOC( Iso_Dat_t, p->nObjs );
+    p->vVisited  = Vec_IntStart( 1000 );
+    p->vPlaces   = Vec_IntStart( 1000 );
+    p->vRoots    = Vec_PtrStart( 1000 );
+    p->pCounters = ABC_CALLOC( int, (1 << AIG_ISO_NUM) );
+    return p;
+}
+void Iso_StoStop( Iso_Sto_t * p )
+{
+    Vec_IntFree( p->vPlaces );
+    Vec_IntFree( p->vVisited );
+    Vec_PtrFree( p->vRoots );
+    ABC_FREE( p->pCounters );
+    ABC_FREE( p->pData );
+    ABC_FREE( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collect statistics about one node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Iso_StoCollectInfo_rec( Aig_Man_t * p, Aig_Obj_t * pObj, int fCompl, Vec_Int_t * vVisited, Iso_Dat_t * pData, Vec_Ptr_t * vRoots )
+{
+    Iso_Dat_t * pThis = pData + Aig_ObjId(pObj);
+    assert( Aig_ObjIsPi(pObj) || Aig_ObjIsNode(pObj) );
+    if ( pThis->fVisit )
+    {
+        if ( fCompl )
+            pThis->nFoNeg++;
+        else
+            pThis->nFoPos++;
+        return;
+    }
+    assert( *((int *)pThis) == 0 );
+    pThis->fVisit = 1;
+    if ( fCompl )
+        pThis->nFoNeg++;
+    else
+        pThis->nFoPos++;
+    pThis->Level = pObj->Level;
+    pThis->nFiNeg = Aig_ObjFaninC0(pObj) + Aig_ObjFaninC1(pObj);
+    if ( Aig_ObjIsNode(pObj) )
+    {
+        if ( Aig_ObjFaninC0(pObj) < Aig_ObjFaninC1(pObj) || (Aig_ObjFaninC0(pObj) == Aig_ObjFaninC1(pObj) && Aig_ObjFanin0(pObj)->Level < Aig_ObjFanin1(pObj)->Level) )
+        {
+            pThis->Fi0Lev = pObj->Level - Aig_ObjFanin0(pObj)->Level;
+            pThis->Fi1Lev = pObj->Level - Aig_ObjFanin1(pObj)->Level;
+        }
+        else
+        {
+            pThis->Fi0Lev = pObj->Level - Aig_ObjFanin1(pObj)->Level;
+            pThis->Fi1Lev = pObj->Level - Aig_ObjFanin0(pObj)->Level;
+        }
+        Iso_StoCollectInfo_rec( p, Aig_ObjFanin0(pObj), Aig_ObjFaninC0(pObj), vVisited, pData, vRoots );
+        Iso_StoCollectInfo_rec( p, Aig_ObjFanin1(pObj), Aig_ObjFaninC1(pObj), vVisited, pData, vRoots );
+    }
+    else if ( Saig_ObjIsLo(p, pObj) )
+    {
+        pThis->Fi0Lev = 1;
+        pThis->Fi1Lev = 0;
+        Vec_PtrPush( vRoots, Saig_ObjLoToLi(p, pObj) );
+    }
+    else if ( Saig_ObjIsPi(p, pObj) )
+    {
+        pThis->Fi0Lev = 0;
+        pThis->Fi1Lev = 0;
+    }
+    else
+        assert( 0 );
+    assert( pThis->nFoNeg + pThis->nFoPos );
+    Vec_IntPush( vVisited, Aig_ObjId(pObj) );
+}
+
+//static int time_Trav = 0;
+
+/**Function*************************************************************
+
+  Synopsis    [Collect statistics about one output.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Iso_StoCollectInfo( Iso_Sto_t * p, Aig_Obj_t * pPo )
+{
+    int fVerboseShow = 0;
+    Vec_Int_t * vInfo;
+    Iso_Dat2_t * pData2 = (Iso_Dat2_t *)p->pData;
+    Aig_Man_t * pAig = p->pAig;
+    Aig_Obj_t * pObj;
+    int i, Value, Entry, * pPerm;
+    int clk = clock();
+
+    assert( Aig_ObjIsPo(pPo) );
+
+    // collect initial POs
+    Vec_IntClear( p->vVisited );
+    Vec_PtrClear( p->vRoots );
+    Vec_PtrPush( p->vRoots, pPo );
+
+    // mark internal nodes
+    Vec_PtrForEachEntry( Aig_Obj_t *, p->vRoots, pObj, i )
+        if ( !Aig_ObjIsConst1(Aig_ObjFanin0(pObj)) )
+            Iso_StoCollectInfo_rec( pAig, Aig_ObjFanin0(pObj), Aig_ObjFaninC0(pObj), p->vVisited, p->pData, p->vRoots );
+//    time_Trav += clock() - clk;
+
+    // count how many times each data entry appears
+    Vec_IntClear( p->vPlaces );
+    Vec_IntForEachEntry( p->vVisited, Entry, i )
+    {
+        Value = pData2[Entry].Data;
+//        assert( Value > 0 );
+        if ( p->pCounters[Value]++ == 0 )
+            Vec_IntPush( p->vPlaces, Value );
+//        pData2[Entry].Data = 0;
+        *((int *)(p->pData + Entry)) = 0;
+    }
+
+    // collect non-trivial counters
+    Vec_IntClear( p->vVisited );
+    Vec_IntForEachEntry( p->vPlaces, Entry, i )
+    {
+        assert( p->pCounters[Entry] );
+        Vec_IntPush( p->vVisited, p->pCounters[Entry] );
+        p->pCounters[Entry] = 0;
+    }
+//    printf( "%d ", Vec_IntSize(p->vVisited) );
+
+    // sort the costs in the increasing order
+    pPerm = Abc_SortCost( Vec_IntArray(p->vVisited), Vec_IntSize(p->vVisited) );
+    assert( Vec_IntEntry(p->vVisited, pPerm[0]) <= Vec_IntEntry(p->vVisited, pPerm[Vec_IntSize(p->vVisited)-1]) );
+
+    // create information
+    vInfo = Vec_IntAlloc( Vec_IntSize(p->vVisited) );
+    for ( i = Vec_IntSize(p->vVisited)-1; i >= 0; i-- )
+    {
+        Entry = Vec_IntEntry( p->vVisited, pPerm[i] );
+        Entry = (Entry << AIG_ISO_NUM) | Vec_IntEntry( p->vPlaces, pPerm[i] );
+        Vec_IntPush( vInfo, Entry );
+    }
+    ABC_FREE( pPerm );
+
+    // show the final result
+    if ( fVerboseShow )
+    Vec_IntForEachEntry( vInfo, Entry, i )
+    {
+        Iso_Dat2_t Data = { Entry & 0xFFFF };
+        Iso_Dat_t * pData = (Iso_Dat_t *)&Data;
+
+        printf( "%6d : ", i );
+        printf( "Freq =%6d ", Entry >> 16 );
+
+        printf( "FiNeg =%3d ", pData->nFiNeg );
+        printf( "FoNeg =%3d ", pData->nFoNeg );
+        printf( "FoPos =%3d ", pData->nFoPos );
+        printf( "Fi0L  =%3d ", pData->Fi0Lev );
+        printf( "Fi1L  =%3d ", pData->Fi1Lev );
+        printf( "Lev   =%3d ", pData->Level  );
+        printf( "\n" );
+    }
+    return vInfo;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Takes multi-output sequential AIG.]
+
+  Description [Returns candidate equivalence classes of POs.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Iso_StoCompareVecInt( Vec_Int_t ** p1, Vec_Int_t ** p2 )
+{
+    return Vec_IntCompareVec( *p1, *p2 );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Takes multi-output sequential AIG.]
+
+  Description [Returns candidate equivalence classes of POs.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Vec_t * Saig_IsoDetectFast( Aig_Man_t * pAig )
+{
+    Iso_Sto_t * pMan;
+    Aig_Obj_t * pObj;
+    Vec_Ptr_t * vClasses, * vInfos;
+    Vec_Int_t * vInfo, * vPrev, * vLevel;
+    int i, Number, nUnique = 0, clk = clock();
+
+    // collect infos and remember their number
+    pMan = Iso_StoStart( pAig );
+    vInfos = Vec_PtrAlloc( Saig_ManPoNum(pAig) );
+    Saig_ManForEachPo( pAig, pObj, i )
+    {
+        vInfo = Iso_StoCollectInfo(pMan, pObj);
+        Vec_IntPush( vInfo, i );
+        Vec_PtrPush( vInfos, vInfo );
+    }
+    Iso_StoStop( pMan );
+    Abc_PrintTime( 1, "Info computation time", clock() - clk );
+
+    // sort the infos
+    clk = clock();
+    Vec_PtrSort( vInfos, (int (*)(void))Iso_StoCompareVecInt );
+
+    // create classes
+    clk = clock();
+    vClasses = Vec_PtrAlloc( Saig_ManPoNum(pAig) );
+    // start the first class
+    Vec_PtrPush( vClasses, (vLevel = Vec_IntAlloc(4)) );
+    vPrev = (Vec_Int_t *)Vec_PtrEntry( vInfos, 0 );
+    Vec_IntPush( vLevel, Vec_IntPop(vPrev) );
+    // consider other classes
+    Vec_PtrForEachEntryStart( Vec_Int_t *, vInfos, vInfo, i, 1 )
+    {
+        Number = Vec_IntPop( vInfo );
+        if ( Vec_IntCompareVec(vPrev, vInfo) )
+            Vec_PtrPush( vClasses, Vec_IntAlloc(4) );
+        vLevel = (Vec_Int_t *)Vec_PtrEntryLast( vClasses );
+        Vec_IntPush( vLevel, Number );
+        vPrev = vInfo;
+    }
+    Vec_VecFree( (Vec_Vec_t *)vInfos );
+    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", Saig_ManPoNum(pAig), Vec_PtrSize(vClasses) );
+
+    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 );
+
+//    return (Vec_Vec_t *)vClasses;
+    Vec_VecFree( (Vec_Vec_t *)vClasses );
+    return NULL;
+}
+
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/aig/aigIso.c b/src/aig/saig/saigIsoSlow.c
index 27789107..7510c911 100644
--- a/src/aig/aig/aigIso.c
+++ b/src/aig/saig/saigIsoSlow.c
@@ -18,7 +18,7 @@
 
 ***********************************************************************/
 
-#include "aig.h"
+#include "saig.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -33,15 +33,14 @@ typedef struct Iso_Obj_t_ Iso_Obj_t;
 struct Iso_Obj_t_
 {
     // hashing entries (related to the parameter ISO_NUM_INTS!)
-    int           Level;
-    unsigned      fFlop    :  1;
-    unsigned      fMux     :  1;
-    unsigned      nFinPos  :  2;
-    unsigned      nFoutPos : 28;
-    unsigned      fCLow    :  1;
-    unsigned      fCHigh   :  1;
+    unsigned      Level    : 30;
     unsigned      nFinNeg  :  2;
-    unsigned      nFoutNeg : 28;
+    unsigned      nFoutPos : 16;
+    unsigned      nFoutNeg : 16;
+    unsigned      nFinLev0 : 16;
+    unsigned      nFinLev1 : 16;
+//    unsigned      nNodes   : 16;
+//    unsigned      nEdges   : 16;
     // other data
     int           iNext;          // hash table entry
     int           iClass;         // next one in class
@@ -61,16 +60,15 @@ struct Iso_Man_t_
     int           nObjs;          // total objects
     int           nBins;          // hash table size
     int *         pBins;          // hash table 
-    Vec_Int_t *   vPolRefs;       // polarity references
     Vec_Ptr_t *   vSingles;       // singletons 
     Vec_Ptr_t *   vClasses;       // other classes
+    Vec_Ptr_t *   vTemp1;         // other classes
+    Vec_Ptr_t *   vTemp2;         // other classes
 };
 
 static inline Iso_Obj_t *  Iso_ManObj( Iso_Man_t * p, int i )            { assert( i >= 0 && i < p->nObjs ); return i ? p->pObjs + i : NULL;                     }
 static inline int          Iso_ObjId( Iso_Man_t * p, Iso_Obj_t * pObj )  { assert( pObj > p->pObjs && pObj < p->pObjs + p->nObjs ); return pObj - p->pObjs;      }
-
-static inline void Iso_ObjIncPolRef0( Vec_Int_t * vPolRefs, Aig_Obj_t * pObj ) { Vec_IntAddToEntry( vPolRefs, 2*Aig_ObjFaninId0(pObj)+Aig_ObjFaninC0(pObj), 1 ); }
-static inline void Iso_ObjIncPolRef1( Vec_Int_t * vPolRefs, Aig_Obj_t * pObj ) { Vec_IntAddToEntry( vPolRefs, 2*Aig_ObjFaninId1(pObj)+Aig_ObjFaninC1(pObj), 1 ); }
+static inline Aig_Obj_t *  Iso_AigObj( Iso_Man_t * p, Iso_Obj_t * q )    { return Aig_ManObj( p->pAig, Iso_ObjId(p, q) );                                        }
 
 #define Iso_ManForEachObj( p, pObj, i )   \
     for ( i = 1; (i < p->nObjs) && ((pObj) = Iso_ManObj(p, i)); i++ ) if ( pIso->Level == -1 ) {} else
@@ -90,49 +88,24 @@ static inline void Iso_ObjIncPolRef1( Vec_Int_t * vPolRefs, Aig_Obj_t * pObj ) {
   SeeAlso     []
 
 ***********************************************************************/
-int Iso_ManNegEdgeNum( Aig_Man_t * pAig )
+void Iso_ManObjCount_rec( Aig_Man_t * p, Aig_Obj_t * pObj, int * pnNodes, int * pnEdges )
 {
-    Aig_Obj_t * pObj;
-    int i, Counter = 0;
-    if ( pAig->nComplEdges > 0 )
-        return pAig->nComplEdges;
-    Aig_ManForEachObj( pAig, pObj, i )
-        if ( Aig_ObjIsNode(pObj) )
-        {
-            Counter += Aig_ObjFaninC0(pObj);
-            Counter += Aig_ObjFaninC1(pObj);
-        }
-        else if ( Aig_ObjIsPo(pObj) )
-            Counter += Aig_ObjFaninC0(pObj);
-    return (pAig->nComplEdges = Counter);
+    if ( Aig_ObjIsPi(pObj) )
+        return;
+    if ( Aig_ObjIsTravIdCurrent(p, pObj) )
+        return;
+    Aig_ObjSetTravIdCurrent(p, pObj);
+    Iso_ManObjCount_rec( p, Aig_ObjFanin0(pObj), pnNodes, pnEdges );
+    Iso_ManObjCount_rec( p, Aig_ObjFanin1(pObj), pnNodes, pnEdges );
+    (*pnEdges) += Aig_ObjFaninC0(pObj) + Aig_ObjFaninC1(pObj);
+    (*pnNodes)++;
 }
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Vec_Int_t * Iso_ManComputePolRefs( Aig_Man_t * pAig )
+void Iso_ManObjCount( Aig_Man_t * p, Aig_Obj_t * pObj, int * pnNodes, int * pnEdges )
 {
-    Vec_Int_t * vPolRefs;
-    Aig_Obj_t * pObj;
-    int i;
-    vPolRefs = Vec_IntStart( 2 * Aig_ManObjNumMax( pAig ) );
-    Aig_ManForEachObj( pAig, pObj, i )
-        if ( Aig_ObjIsNode(pObj) )
-        {
-            Iso_ObjIncPolRef0( vPolRefs, pObj );
-            Iso_ObjIncPolRef1( vPolRefs, pObj );
-        }
-        else if ( Aig_ObjIsPo(pObj) )
-            Iso_ObjIncPolRef0( vPolRefs, pObj );
-    return vPolRefs;
+    assert( Aig_ObjIsNode(pObj) );
+    *pnNodes = *pnEdges = 0;
+    Aig_ManIncrementTravId( p );
+    Iso_ManObjCount_rec( p, pObj, pnNodes, pnEdges );
 }
 
 /**Function*************************************************************
@@ -155,9 +128,10 @@ Iso_Man_t * Iso_ManStart( Aig_Man_t * pAig )
     p->pObjs    = ABC_CALLOC( Iso_Obj_t, p->nObjs );
     p->nBins    = Abc_PrimeCudd( p->nObjs );
     p->pBins    = ABC_CALLOC( int, p->nBins );    
-    p->vPolRefs = Iso_ManComputePolRefs( pAig );
     p->vSingles = Vec_PtrAlloc( 1000 );
     p->vClasses = Vec_PtrAlloc( 1000 );
+    p->vTemp1   = Vec_PtrAlloc( 1000 );
+    p->vTemp2   = Vec_PtrAlloc( 1000 );
     p->nObjIds  = 1;
     return p;
 }
@@ -167,9 +141,10 @@ void Iso_ManStop( Iso_Man_t * p )
     int i;
     Iso_ManForEachObj( p, pIso, i )
         Vec_IntFreeP( &pIso->vAllies );
+    Vec_PtrFree( p->vTemp1 );
+    Vec_PtrFree( p->vTemp2 );
     Vec_PtrFree( p->vClasses );
     Vec_PtrFree( p->vSingles );
-    Vec_IntFree( p->vPolRefs );
     ABC_FREE( p->pBins );
     ABC_FREE( p->pObjs );
     ABC_FREE( p );
@@ -187,54 +162,14 @@ void Iso_ManStop( Iso_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-int Iso_ObjCompareBasic( Iso_Obj_t * pIso1, Iso_Obj_t * pIso2 )
-{
-    int fCLow1, fCLow2, fCHigh1, fCHigh2, Diff;
-
-    fCLow1  = pIso1->fCLow;  pIso1->fCLow = 0;
-    fCLow2  = pIso2->fCLow;  pIso2->fCLow = 0;
-    fCHigh1 = pIso1->fCHigh; pIso1->fCHigh = 0;
-    fCHigh2 = pIso2->fCHigh; pIso2->fCHigh = 0;
-
-    Diff = memcmp( pIso1, pIso2, sizeof(int) * ISO_NUM_INTS );
-
-    pIso1->fCLow  = fCLow1;
-    pIso2->fCLow  = fCLow2;
-    pIso1->fCHigh = fCHigh1;
-    pIso2->fCHigh = fCHigh2;
-
-    return -Diff;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Compares two objects by their signature.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
 int Iso_ObjCompare( Iso_Obj_t ** pp1, Iso_Obj_t ** pp2 )
 {
     Iso_Obj_t * pIso1 = *pp1;
     Iso_Obj_t * pIso2 = *pp2;
-    int Diff = memcmp( pIso1, pIso2, sizeof(int) * ISO_NUM_INTS );
-    if ( Diff )
-        return -Diff;
-//    return 0;
-    if ( pIso1->vAllies == NULL && pIso2->vAllies == NULL )
-        return  0;
-    if ( pIso1->vAllies == NULL && pIso2->vAllies != NULL )
-        return  1;
-    if ( pIso1->vAllies != NULL && pIso2->vAllies == NULL )
-        return -1;
-    Diff = Vec_IntSize(pIso1->vAllies) - Vec_IntSize(pIso2->vAllies);
+    int Diff = -memcmp( pIso1, pIso2, sizeof(int) * ISO_NUM_INTS );
     if ( Diff )
-        return -Diff;
-    return memcmp( Vec_IntArray(pIso1->vAllies), Vec_IntArray(pIso2->vAllies), Vec_IntSize(pIso1->vAllies) * sizeof(int) );
+        return Diff;
+    return -Vec_IntCompareVec( pIso1->vAllies, pIso2->vAllies );
 }
 
 /**Function*************************************************************
@@ -270,7 +205,8 @@ int Iso_ObjCompareAigObjByData( Aig_Obj_t ** pp1, Aig_Obj_t ** pp2 )
 {
     Aig_Obj_t * pIso1 = *pp1;
     Aig_Obj_t * pIso2 = *pp2;
-    assert( Aig_ObjIsPi(pIso1) && Aig_ObjIsPi(pIso2) );
+    assert( Aig_ObjIsPi(pIso1) || Aig_ObjIsPo(pIso1) );
+    assert( Aig_ObjIsPi(pIso2) || Aig_ObjIsPo(pIso2) );
     return pIso1->iData - pIso2->iData;
 }
 
@@ -332,55 +268,29 @@ static inline int Iso_ObjHashAdd( Iso_Man_t * p, Iso_Obj_t * pIso )
   SeeAlso     []
 
 ***********************************************************************/
-Iso_Man_t * Iso_ManCreate( Aig_Man_t * pAig )
+void Iso_ManCollectClasses( Iso_Man_t * p )
 {
-    Iso_Man_t * p;
     Iso_Obj_t * pIso;
-    Aig_Obj_t * pObj;
     int i;
-    p = Iso_ManStart( pAig );
-    Iso_ManForEachObj( p, pIso, i )
-        pIso->Level = -1;
-    Aig_ManForEachObj( pAig, pObj, i )
-    {
-        if ( !Aig_ObjIsPi(pObj) && !Aig_ObjIsNode(pObj) )
-            continue;
-        pIso = p->pObjs + i;
-        if ( Aig_ObjIsNode(pObj) )
+    Vec_PtrClear( p->vSingles );
+    Vec_PtrClear( p->vClasses );
+    for ( i = 0; i < p->nBins; i++ )
+        for ( pIso = Iso_ManObj(p, p->pBins[i]); pIso; pIso = Iso_ManObj(p, pIso->iNext) )
         {
-            pIso->nFinNeg  = Aig_ObjFaninC0(pObj) + Aig_ObjFaninC1(pObj);
-            pIso->nFinPos  = 2 - pIso->nFinNeg;
-            pIso->fMux  = Aig_ObjIsMuxType( pObj );
-            if ( Aig_ObjFaninC0(pObj) != Aig_ObjFaninC1(pObj) )
-            {
-                // fanins are already assigned!!!
-                if ( Aig_ObjFaninC0(pObj) )
-                {
-                    int Diff = Iso_ObjCompareBasic( Iso_ManObj(p,Aig_ObjFaninId0(pObj)), Iso_ManObj(p,Aig_ObjFaninId1(pObj)) );
-                    if ( Diff < 0 )
-                        pIso->fCLow  = 1;
-                    else if ( Diff > 0 )
-                        pIso->fCHigh = 1;
-                }
-                else
-                {
-                    int Diff = Iso_ObjCompareBasic( Iso_ManObj(p,Aig_ObjFaninId1(pObj)), Iso_ManObj(p,Aig_ObjFaninId0(pObj)) );
-                    if ( Diff < 0 )
-                        pIso->fCLow  = 1;
-                    else if ( Diff > 0 )
-                        pIso->fCHigh = 1;
-                }
-            }
+            assert( pIso->Id == 0 );
+            if ( pIso->iClass )
+                Vec_PtrPush( p->vClasses, pIso );
+            else 
+                Vec_PtrPush( p->vSingles, pIso );
         }
-        else
-            pIso->fFlop = (int)(Aig_ObjPioNum(pObj) >= Aig_ManPiNum(pAig) - Aig_ManRegNum(pAig));
-        pIso->nFoutPos = Vec_IntEntry( p->vPolRefs, 2*i );
-        pIso->nFoutNeg = Vec_IntEntry( p->vPolRefs, 2*i+1 );
-        pIso->Level = pObj->Level;
-        // add to the hash table
-        Iso_ObjHashAdd( p, pIso );
-    }
-    return p;
+    Vec_PtrSort( p->vSingles, (int (*)(void))Iso_ObjCompare );
+    Vec_PtrSort( p->vClasses, (int (*)(void))Iso_ObjCompare );
+    assert( Vec_PtrSize(p->vSingles) == p->nSingles );
+    assert( Vec_PtrSize(p->vClasses) == p->nClasses );
+    // assign IDs to singletons
+    Vec_PtrForEachEntry( Iso_Obj_t *, p->vSingles, pIso, i )
+        if ( pIso->Id == 0 )
+            pIso->Id = p->nObjIds++;
 }
 
 /**Function*************************************************************
@@ -394,25 +304,71 @@ Iso_Man_t * Iso_ManCreate( Aig_Man_t * pAig )
   SeeAlso     []
 
 ***********************************************************************/
-void Iso_ManCollectClasses( Iso_Man_t * p )
+Iso_Man_t * Iso_ManCreate( Aig_Man_t * pAig )
 {
+    Iso_Man_t * p;
     Iso_Obj_t * pIso;
-    int i;
-    Vec_PtrClear( p->vSingles );
-    Vec_PtrClear( p->vClasses );
-    for ( i = 0; i < p->nBins; i++ )
-        for ( pIso = Iso_ManObj(p, p->pBins[i]); pIso; pIso = Iso_ManObj(p, pIso->iNext) )
+    Aig_Obj_t * pObj;
+    int i, nNodes = 0, nEdges = 0;
+    p = Iso_ManStart( pAig );
+    Aig_ManForEachObj( pAig, pObj, i )
+    {
+        if ( Aig_ObjIsNode(pObj) )
         {
-//            assert( pIso->Id == 0 );
-            if ( pIso->iClass )
-                Vec_PtrPush( p->vClasses, pIso );
-            else 
-                Vec_PtrPush( p->vSingles, pIso );
+            pIso = p->pObjs + Aig_ObjFaninId0(pObj);
+            if ( Aig_ObjFaninC0(pObj) )
+                pIso->nFoutNeg++;
+            else
+                pIso->nFoutPos++;
+            pIso = p->pObjs + Aig_ObjFaninId1(pObj);
+            if ( Aig_ObjFaninC1(pObj) )
+                pIso->nFoutNeg++;
+            else
+                pIso->nFoutPos++;
         }
-    Vec_PtrSort( p->vSingles, (int (*)(void))Iso_ObjCompare );
-    Vec_PtrSort( p->vClasses, (int (*)(void))Iso_ObjCompare );
-    assert( Vec_PtrSize(p->vSingles) == p->nSingles );
-    assert( Vec_PtrSize(p->vClasses) == p->nClasses );
+        else if ( Aig_ObjIsPo(pObj) )
+        {
+            pIso = p->pObjs + Aig_ObjFaninId0(pObj);
+            if ( Aig_ObjFaninC0(pObj) )
+                pIso->nFoutNeg++;
+            else
+                pIso->nFoutPos++;
+        }
+    }
+    Aig_ManForEachObj( pAig, pObj, i )
+    {
+        if ( !Aig_ObjIsPi(pObj) && !Aig_ObjIsNode(pObj) )
+            continue;
+        pIso = p->pObjs + i;
+        pIso->Level = pObj->Level;
+        pIso->nFinNeg = Aig_ObjFaninC0(pObj) + Aig_ObjFaninC1(pObj);
+        if ( Aig_ObjIsNode(pObj) )
+        {
+            if ( Aig_ObjIsMuxType(pObj) ) // uniqify MUX/XOR
+                pIso->nFinNeg = 3;
+            if ( Aig_ObjFaninC0(pObj) < Aig_ObjFaninC1(pObj) || (Aig_ObjFaninC0(pObj) == Aig_ObjFaninC1(pObj) && Aig_ObjFanin0(pObj)->Level < Aig_ObjFanin1(pObj)->Level) )
+            {
+                pIso->nFinLev0 = Aig_ObjFanin0(pObj)->Level;
+                pIso->nFinLev1 = Aig_ObjFanin1(pObj)->Level;
+            }
+            else
+            {
+                pIso->nFinLev0 = Aig_ObjFanin1(pObj)->Level;
+                pIso->nFinLev1 = Aig_ObjFanin0(pObj)->Level;
+            }
+//            Iso_ManObjCount( pAig, pObj, &nNodes, &nEdges );
+//            pIso->nNodes = nNodes;
+//            pIso->nEdges = nEdges;
+        }
+        else
+        {  
+            pIso->nFinLev0 = (int)(Aig_ObjPioNum(pObj) >= Aig_ManPiNum(pAig) - Aig_ManRegNum(pAig)); // uniqify flop
+        }
+        // add to the hash table
+        Iso_ObjHashAdd( p, pIso );
+    }
+    Iso_ManCollectClasses( p );
+    return p;
 }
 
 /**Function*************************************************************
@@ -440,8 +396,6 @@ void Iso_ManPrintClasses( Iso_Man_t * p, int fVerbose, int fVeryVerbose )
     if ( !fVeryVerbose )
         return;
 
-    Iso_ManCollectClasses( p );
-
     printf( "Non-trivial classes:\n" );
     Vec_PtrForEachEntry( Iso_Obj_t *, p->vClasses, pIso, i )
     {
@@ -452,10 +406,10 @@ void Iso_ManPrintClasses( Iso_Man_t * p, int fVerbose, int fVeryVerbose )
         for ( pTemp = pIso; pTemp; pTemp = Iso_ManObj(p, pTemp->iClass) )
         {
             if ( fOnlyCis )
-                printf( " %d", Aig_ObjPioNum(Aig_ManObj(p->pAig, Iso_ObjId(p, pTemp))) );
+                printf( " %d", Aig_ObjPioNum( Iso_AigObj(p, pTemp) ) );
             else
             {
-                Aig_Obj_t * pObj = Aig_ManObj(p->pAig, Iso_ObjId(p, pTemp));
+                Aig_Obj_t * pObj = Iso_AigObj(p, pTemp);
                 if ( Aig_ObjIsNode(pObj) )
                     printf( " %d{%s%d(%d),%s%d(%d)}", Iso_ObjId(p, pTemp), 
                         Aig_ObjFaninC0(pObj)? "-": "+", Aig_ObjFaninId0(pObj), Aig_ObjLevel(Aig_ObjFanin0(pObj)), 
@@ -489,12 +443,12 @@ void Iso_ManPrintClasses( Iso_Man_t * p, int fVerbose, int fVeryVerbose )
   SeeAlso     []
 
 ***********************************************************************/
-static inline void Iso_ObjAddToAllies( Iso_Obj_t * pIso, int Id )
+static inline void Iso_ObjAddToAllies( Iso_Obj_t * pIso, int Id, int fCompl )
 {
     assert( pIso->Id == 0 );
     if ( pIso->vAllies == NULL )
         pIso->vAllies = Vec_IntAlloc( 8 );
-    Vec_IntPush( pIso->vAllies, Id );        
+    Vec_IntPush( pIso->vAllies, fCompl ? -Id : Id );        
 }
 void Iso_ManAssignAdjacency( Iso_Man_t * p )
 {
@@ -518,34 +472,34 @@ void Iso_ManAssignAdjacency( Iso_Man_t * p )
         if ( pIso->Id ) // unique - add to non-unique fanins
         {
             if ( pIso0->Id == 0 )
-                Iso_ObjAddToAllies( pIso0, pIso->Id );
+                Iso_ObjAddToAllies( pIso0, pIso->Id, Aig_ObjFaninC0(pObj) );
             if ( pIso1->Id == 0 )
-                Iso_ObjAddToAllies( pIso1, pIso->Id );
+                Iso_ObjAddToAllies( pIso1, pIso->Id, Aig_ObjFaninC1(pObj) );
         }
         else // non-unique - assign unique fanins to it
         {
             if ( pIso0->Id != 0 )
-                Iso_ObjAddToAllies( pIso, pIso0->Id );
+                Iso_ObjAddToAllies( pIso, pIso0->Id, Aig_ObjFaninC0(pObj) );
             if ( pIso1->Id != 0 )
-                Iso_ObjAddToAllies( pIso, pIso1->Id );
+                Iso_ObjAddToAllies( pIso, pIso1->Id, Aig_ObjFaninC1(pObj) );
         }
     }
     // consider flops
     Aig_ManForEachLiLoSeq( p->pAig, pObjLi, pObj, i )
     {
-        if ( Aig_ObjFaninId0(pObjLi) == 0 ) // ignore!
+        if ( Aig_ObjFaninId0(pObjLi) == 0 ) // ignore constant!
             continue;
         pIso  = Iso_ManObj( p, Aig_ObjId(pObj) );
         pIso0 = Iso_ManObj( p, Aig_ObjFaninId0(pObjLi) );
         if ( pIso->Id ) // unique - add to non-unique fanins
         {
             if ( pIso0->Id == 0 )
-                Iso_ObjAddToAllies( pIso0, pIso->Id );
+                Iso_ObjAddToAllies( pIso0, pIso->Id, Aig_ObjFaninC0(pObjLi) );
         }
         else // non-unique - assign unique fanins to it
         {
             if ( pIso0->Id != 0 )
-                Iso_ObjAddToAllies( pIso, pIso0->Id );
+                Iso_ObjAddToAllies( pIso, pIso0->Id, Aig_ObjFaninC0(pObjLi) );
         }
     }
     // sort
@@ -574,26 +528,39 @@ void Iso_ManRehashClassNodes( Iso_Man_t * p )
     Iso_Obj_t * pIso, * pTemp;
     int i;
     // collect nodes
-    Vec_PtrClear( p->vSingles );
+    Vec_PtrClear( p->vTemp1 );
+    Vec_PtrClear( p->vTemp2 );
     Vec_PtrForEachEntry( Iso_Obj_t *, p->vClasses, pIso, i )
+    {
         for ( pTemp = pIso; pTemp; pTemp = Iso_ManObj(p, pTemp->iClass) )
-            Vec_PtrPush( p->vSingles, pTemp );
+            if ( pTemp->Id == 0 )
+                Vec_PtrPush( p->vTemp1, pTemp );
+            else
+                Vec_PtrPush( p->vTemp2, pTemp );
+    }
     // clean and add nodes
     p->nClasses = 0;       // total number of classes
     p->nEntries = 0;       // total number of entries
     p->nSingles = 0;       // total number of singletons
     memset( p->pBins, 0, sizeof(int) * p->nBins );
-    Vec_PtrForEachEntry( Iso_Obj_t *, p->vSingles, pIso, i )
+    Vec_PtrForEachEntry( Iso_Obj_t *, p->vTemp1, pTemp, i )
     {
-        pIso->iClass = pIso->iNext = 0;
-        Iso_ObjHashAdd( p, pIso );
+        assert( pTemp->Id == 0 );
+        pTemp->iClass = pTemp->iNext = 0;
+        Iso_ObjHashAdd( p, pTemp );
     }
-    Vec_PtrClear( p->vSingles );
+    Vec_PtrForEachEntry( Iso_Obj_t *, p->vTemp2, pTemp, i )
+    {
+        assert( pTemp->Id != 0 );
+        pTemp->iClass = pTemp->iNext = 0;
+    }
+    // collect new classes
+    Iso_ManCollectClasses( p );
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Returns one if there are unclassified CIs.]
+  Synopsis    [Find nodes with the min number of edges.]
 
   Description []
                
@@ -602,84 +569,33 @@ void Iso_ManRehashClassNodes( Iso_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-int Iso_ManCheckCis( Iso_Man_t * p )
+Iso_Obj_t * Iso_ManFindBestObj( Iso_Man_t * p, Iso_Obj_t * pIso )
 {
-    Aig_Obj_t * pObj;
-    int i;
-    Aig_ManForEachPi( p->pAig, pObj, i )
-        if ( Aig_ObjRefs(pObj) > 0 && Iso_ManObj(p, Aig_ObjId(pObj))->Id == 0 )
-            return 0;
-    return 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Finalizes unification of combinational outputs.]
-
-  Description [Assigns IDs to the unclassified CIs in the order of obj IDs.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Vec_Int_t * Iso_ManFinalize( Iso_Man_t * p )
-{
-    Vec_Int_t * vRes;
-    Vec_Ptr_t * vClass, * vClass2;
-    Iso_Obj_t * pIso, * pTemp;
-    Aig_Obj_t * pObj;
-    int i, k;
-
-    vClass  = Vec_PtrAlloc( Aig_ManPiNum(p->pAig)-Aig_ManRegNum(p->pAig) );
-    vClass2 = Vec_PtrAlloc( Aig_ManRegNum(p->pAig) );
-    Vec_PtrForEachEntry( Iso_Obj_t *, p->vClasses, pIso, i )
+    Iso_Obj_t * pTemp, * pBest = NULL;
+    int nNodesBest = -1, nNodes;
+    int nEdgesBest = -1, nEdges;
+    assert( pIso->Id == 0 );
+    if ( pIso->Level == 0 )
+        return pIso;
+    for ( pTemp = pIso; pTemp; pTemp = Iso_ManObj(p, pTemp->iClass) )
     {
-        if ( pIso->Level > 0 )
-            continue;
-        Vec_PtrClear( vClass );
-        for ( pTemp = pIso; pTemp; pTemp = Iso_ManObj(p, pTemp->iClass) )
+        assert( pTemp->Id == 0 );
+        Iso_ManObjCount( p->pAig, Iso_AigObj(p, pTemp), &nNodes, &nEdges );
+//        printf( "%d,%d ", nNodes, nEdges );
+        if ( nNodesBest < nNodes || (nNodesBest == nNodes && nEdgesBest < nEdges) )
         {
-            assert( pTemp->Id == 0 );
-            pTemp->Id = Aig_ObjPioNum(Aig_ManObj(p->pAig, Iso_ObjId(p, pTemp)));
-            Vec_PtrPush( vClass, pTemp );
+            nNodesBest = nNodes;
+            nEdgesBest = nEdges;
+            pBest = pTemp;
         }
-        Vec_PtrSort( vClass, (int (*)(void))Iso_ObjCompareById );
-        // assign IDs in this order
-        Vec_PtrForEachEntry( Iso_Obj_t *, vClass, pIso, k )
-            pIso->Id = p->nObjIds++;
     }
-
-    // assign unique IDs to the CIs
-    Vec_PtrClear( vClass );
-    Vec_PtrClear( vClass2 );
-    Aig_ManForEachPi( p->pAig, pObj, i )
-    {
-        pObj->iData = Iso_ManObj(p, Aig_ObjId(pObj))->Id;
-        if ( Aig_ObjPioNum(pObj) >= Aig_ManPiNum(p->pAig) - Aig_ManRegNum(p->pAig) )
-            Vec_PtrPush( vClass2, pObj );
-        else
-            Vec_PtrPush( vClass, pObj );
-    }
-    // sort CIs by their IDs
-    Vec_PtrSort( vClass, (int (*)(void))Iso_ObjCompareAigObjByData );
-    Vec_PtrSort( vClass2, (int (*)(void))Iso_ObjCompareAigObjByData );
-
-    // create the result
-    vRes = Vec_IntAlloc( Aig_ManPiNum(p->pAig) );
-    Vec_PtrForEachEntry( Aig_Obj_t *, vClass, pObj, i )
-        Vec_IntPush( vRes, Aig_ObjPioNum(pObj) );
-    Vec_PtrForEachEntry( Aig_Obj_t *, vClass2, pObj, i )
-        Vec_IntPush( vRes, Aig_ObjPioNum(pObj) );
-
-    Vec_PtrFree( vClass );
-    Vec_PtrFree( vClass2 );
-    return vRes;
+//    printf( "\n" );
+    return pBest;
 }
 
 /**Function*************************************************************
 
-  Synopsis    []
+  Synopsis    [Find nodes with the min number of edges.]
 
   Description []
                
@@ -688,169 +604,125 @@ Vec_Int_t * Iso_ManFinalize( Iso_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Int_t * Iso_ManFindPerm( Aig_Man_t * pAig, int fVerbose )
+void Iso_ManBreakTies( Iso_Man_t * p, int fVerbose )
 {
-    Iso_Man_t * p;
-    Iso_Obj_t * pIso;
-    Vec_Int_t * vRes;
-    int i;
-    p = Iso_ManCreate( pAig );
-    Iso_ManPrintClasses( p, fVerbose, 0 );
-    while ( p->nSingles )
+    int fUseOneBest = 0;
+    Iso_Obj_t * pIso, * pTemp;
+    int i, LevelStart = 0;
+    pIso = (Iso_Obj_t *)Vec_PtrEntry( p->vClasses, 0 );
+    LevelStart = pIso->Level;
+    if ( fVerbose )
+        printf( "Best level %d\n", LevelStart ); 
+    Vec_PtrForEachEntry( Iso_Obj_t *, p->vClasses, pIso, i )
     {
-        // collect singletons and classes
-        Iso_ManCollectClasses( p );
-        // assign IDs to singletons
-        Vec_PtrForEachEntry( Iso_Obj_t *, p->vSingles, pIso, i )
-            pIso->Id = p->nObjIds++;
-        // check termination
-        if ( p->nClasses == 0 )
+        if ( (int)pIso->Level < LevelStart )
             break;
-        // assign adjacency to classes
-        Iso_ManAssignAdjacency( p );
-        // rehash the class nodes
-        Iso_ManRehashClassNodes( p );
-        Iso_ManPrintClasses( p, fVerbose, 0 );
-
-        if ( p->nSingles == 0 )
+        if ( !fUseOneBest )
         {
-            // assign ID to the first class
-            pIso = (Iso_Obj_t *)Vec_PtrEntry( p->vClasses, 0 );
-            assert( pIso->Id == 0 );
-            pIso->Id = p->nObjIds++;
-            // assign adjacency to classes
-            Iso_ManAssignAdjacency( p );
-            // rehash the class nodes
-            Iso_ManRehashClassNodes( p );
-            Iso_ManPrintClasses( p, fVerbose, 0 );
-            if ( p->nSingles == 0 )
+            for ( pTemp = pIso; pTemp; pTemp = Iso_ManObj(p, pTemp->iClass) )
             {
-                pIso->Id = 0;
-                p->nObjIds--;
+                assert( pTemp->Id ==  0 );
+                pTemp->Id = p->nObjIds++;
             }
+            continue;
         }
+        if ( pIso->Level == 0 && pIso->nFoutPos + pIso->nFoutNeg == 0 )
+        {
+            for ( pTemp = pIso; pTemp; pTemp = Iso_ManObj(p, pTemp->iClass) )
+                pTemp->Id = p->nObjIds++;
+            continue;
+        }
+        pIso = Iso_ManFindBestObj( p, pIso );
+        pIso->Id = p->nObjIds++;
     }
-//    Iso_ManPrintClasses( p, fVerbose, 1 );
-    vRes = Iso_ManFinalize( p );
-    Iso_ManStop( p );
-    return vRes;
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Checks structural equivalence of AIG1 and AIG2.]
+  Synopsis    [Finalizes unification of combinational outputs.]
 
-  Description [Returns 1 if AIG1 and AIG2 are structurally equivalent 
-  under this mapping.]
+  Description [Assigns IDs to the unclassified CIs in the order of obj IDs.]
                
   SideEffects []
 
   SeeAlso     []
 
 ***********************************************************************/
-int Iso_ManCheckMapping( Aig_Man_t * pAig1, Aig_Man_t * pAig2, Vec_Int_t * vMap2to1, int fVerbose )
+Vec_Int_t * Iso_ManFinalize( Iso_Man_t * p )
 {
-    Aig_Obj_t * pObj, * pFanin0, * pFanin1;
+    Vec_Int_t * vRes;
+    Aig_Obj_t * pObj;
     int i;
-    assert( Aig_ManPiNum(pAig1) == Aig_ManPiNum(pAig2) );
-    assert( Aig_ManPoNum(pAig1) == Aig_ManPoNum(pAig2) );
-    assert( Aig_ManRegNum(pAig1) == Aig_ManRegNum(pAig2) );
-    assert( Aig_ManNodeNum(pAig1) == Aig_ManNodeNum(pAig2) );
-    Aig_ManCleanData( pAig1 );
-    // map const and PI nodes
-    Aig_ManConst1(pAig2)->pData = Aig_ManConst1(pAig1);
-    Aig_ManForEachPi( pAig2, pObj, i )
-        pObj->pData = Aig_ManPi( pAig1, Vec_IntEntry(vMap2to1, i) );
-    // try internal nodes
-    Aig_ManForEachNode( pAig2, pObj, i )
+    assert( p->nClasses == 0 );
+    assert( Vec_PtrSize(p->vClasses) == 0 );
+    // set canonical numbers
+    Aig_ManForEachObj( p->pAig, pObj, i )
     {
-        pFanin0 = Aig_ObjChild0Copy( pObj );
-        pFanin1 = Aig_ObjChild1Copy( pObj );
-        pObj->pData = Aig_TableLookupTwo( pAig1, pFanin0, pFanin1 );
-        if ( pObj->pData == NULL )
+        if ( !Aig_ObjIsPi(pObj) && !Aig_ObjIsNode(pObj) )
         {
-            if ( fVerbose )
-                printf( "Structural equivalence failed at node %d.\n", i );
-            return 0;
+            pObj->iData = -1;
+            continue;
         }
+        pObj->iData = Iso_ManObj(p, Aig_ObjId(pObj))->Id;
+        assert( pObj->iData > 0 );
     }
-    // make sure the first PO points to the same node
-    if ( Aig_ManPoNum(pAig1)-Aig_ManRegNum(pAig1) == 1 && Aig_ObjChild0Copy(Aig_ManPo(pAig2, 0)) != Aig_ObjChild0(Aig_ManPo(pAig1, 0)) )
+    Aig_ManConst1(p->pAig)->iData = 0;
+    // assign unique IDs to the CIs
+    Vec_PtrClear( p->vTemp1 );
+    Vec_PtrClear( p->vTemp2 );
+    Aig_ManForEachPi( p->pAig, pObj, i )
     {
-        if ( fVerbose )
-            printf( "Structural equivalence failed at primary output 0.\n" );
-        return 0;
+        assert( pObj->iData > 0 );
+        if ( Aig_ObjPioNum(pObj) >= Aig_ManPiNum(p->pAig) - Aig_ManRegNum(p->pAig) ) // flop
+            Vec_PtrPush( p->vTemp2, pObj );
+        else // PI
+            Vec_PtrPush( p->vTemp1, pObj );
     }
-    return 1;    
+    // sort CIs by their IDs
+    Vec_PtrSort( p->vTemp1, (int (*)(void))Iso_ObjCompareAigObjByData );
+    Vec_PtrSort( p->vTemp2, (int (*)(void))Iso_ObjCompareAigObjByData );
+    // create the result
+    vRes = Vec_IntAlloc( Aig_ManPiNum(p->pAig) );
+    Vec_PtrForEachEntry( Aig_Obj_t *, p->vTemp1, pObj, i )
+        Vec_IntPush( vRes, Aig_ObjPioNum(pObj) );
+    Vec_PtrForEachEntry( Aig_Obj_t *, p->vTemp2, pObj, i )
+        Vec_IntPush( vRes, Aig_ObjPioNum(pObj) );
+    return vRes;
 }
 
-//static int s_Counter;
-
 /**Function*************************************************************
 
-  Synopsis    [Finds mapping of CIs of AIG2 into those of AIG1.]
+  Synopsis    [Find nodes with the min number of edges.]
 
-  Description [Returns the mapping of CIs of the two AIGs, or NULL
-  if there is no mapping.]
+  Description []
                
   SideEffects []
 
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Int_t * Iso_ManFindMapping( Aig_Man_t * pAig1, Aig_Man_t * pAig2, Vec_Int_t * vPerm1_, Vec_Int_t * vPerm2_, int fVerbose )
+void Iso_ManDumpOneClass( Iso_Man_t * p )
 {
-    Vec_Int_t * vPerm1, * vPerm2, * vInvPerm2;
-    int i, Entry;
-    if ( Aig_ManPiNum(pAig1) != Aig_ManPiNum(pAig2) )
-        return NULL;
-    if ( Aig_ManPoNum(pAig1) != Aig_ManPoNum(pAig2) )
-        return NULL;
-    if ( Aig_ManRegNum(pAig1) != Aig_ManRegNum(pAig2) )
-        return NULL;
-    if ( Aig_ManNodeNum(pAig1) != Aig_ManNodeNum(pAig2) )
-        return NULL;
-    if ( Aig_ManLevelNum(pAig1) != Aig_ManLevelNum(pAig2) )
-        return NULL;
-    if ( Iso_ManNegEdgeNum(pAig1) != Iso_ManNegEdgeNum(pAig2) )
-        return NULL;
-//    s_Counter++;
-
-    if ( fVerbose ) 
-        printf( "AIG1:\n" );
-    vPerm1 = vPerm1_ ? vPerm1_ : Iso_ManFindPerm( pAig1, fVerbose );
-    if ( fVerbose )
-        printf( "AIG1:\n" );
-    vPerm2 = vPerm2_ ? vPerm2_ : Iso_ManFindPerm( pAig2, fVerbose );
-    if ( vPerm1_ )
-        assert( Vec_IntSize(vPerm1_) == Aig_ManPiNum(pAig1) );
-    if ( vPerm2_ )
-        assert( Vec_IntSize(vPerm2_) == Aig_ManPiNum(pAig2) );
-    // find canonical permutation
-    // vPerm1/vPerm2 give canonical order of CIs of AIG1/AIG2
-    vInvPerm2 = Vec_IntInvert( vPerm2, -1 );
-    Vec_IntForEachEntry( vInvPerm2, Entry, i )
+    Vec_Ptr_t * vNodes = Vec_PtrAlloc( 100 );
+    Iso_Obj_t * pIso, * pTemp;
+    Aig_Man_t * pNew = NULL;
+    assert( p->nClasses > 0 );
+    pIso = (Iso_Obj_t *)Vec_PtrEntry( p->vClasses, 0 );
+    assert( pIso->Id == 0 );
+    for ( pTemp = pIso; pTemp; pTemp = Iso_ManObj(p, pTemp->iClass) )
     {
-        assert( Entry >= 0 && Entry < Aig_ManPiNum(pAig1) );
-        Vec_IntWriteEntry( vInvPerm2, i, Vec_IntEntry(vPerm1, Entry) );
+        assert( pTemp->Id == 0 );
+        Vec_PtrPush( vNodes, Iso_AigObj(p, pTemp) );
     }
-    if ( vPerm1_ == NULL )
-        Vec_IntFree( vPerm1 );
-    if ( vPerm2_ == NULL )
-        Vec_IntFree( vPerm2 );
-    // check if they are indeed equivalent
-    if ( !Iso_ManCheckMapping( pAig1, pAig2, vInvPerm2, fVerbose ) )
-        Vec_IntFreeP( &vInvPerm2 );
-    return vInvPerm2;
+    pNew = Aig_ManDupNodes( p->pAig, vNodes );
+    Vec_PtrFree( vNodes );
+    Aig_ManShow( pNew, 0, NULL ); 
+    Aig_ManStopP( &pNew );
 }
 
-
-
-#include "src/aig/saig/saig.h"
-
 /**Function*************************************************************
 
-  Synopsis    []
+  Synopsis    [Finds canonical permutation of CIs and assigns unique IDs.]
 
   Description []
                
@@ -859,161 +731,40 @@ Vec_Int_t * Iso_ManFindMapping( Aig_Man_t * pAig1, Aig_Man_t * pAig2, Vec_Int_t
   SeeAlso     []
 
 ***********************************************************************/
-Aig_Man_t * Iso_ManFilterPos( Aig_Man_t * pAig, int fVerbose )
+Vec_Int_t * Saig_ManFindIsoPerm( Aig_Man_t * pAig, int fVerbose )
 {
-    int fVeryVerbose = 0;
-    Vec_Ptr_t * vParts, * vPerms, * vAigs;
-    Vec_Int_t * vPos, * vMap;
-    Aig_Man_t * pPart, * pTemp;
-    int i, k, nPos;
-
-    // derive AIG for each PO
-    nPos = Aig_ManPoNum(pAig) - Aig_ManRegNum(pAig);
-    vParts = Vec_PtrAlloc( nPos );
-    vPerms = Vec_PtrAlloc( nPos );
-    for ( i = 0; i < nPos; i++ )
-    {
-        pPart = Saig_ManDupCones( pAig, &i, 1 );
-        vMap  = Iso_ManFindPerm( pPart, fVeryVerbose );
-        Vec_PtrPush( vParts, pPart ); 
-        Vec_PtrPush( vPerms, vMap );
-    }
-//    s_Counter = 0;
-
-    // check AIGs for each PO
-    vAigs = Vec_PtrAlloc( 1000 );
-    vPos  = Vec_IntAlloc( 1000 );
-    Vec_PtrForEachEntry( Aig_Man_t *, vParts, pPart, i )
+    Vec_Int_t * vRes;
+    Iso_Man_t * p;
+    p = Iso_ManCreate( pAig );
+    Iso_ManPrintClasses( p, fVerbose, 0 );
+    while ( p->nClasses )
     {
-        if ( fVeryVerbose )
-        {
-            printf( "AIG %4d : ", i );
-            Aig_ManPrintStats( pPart );
-        }
-        Vec_PtrForEachEntry( Aig_Man_t *, vAigs, pTemp, k )
-        {
-            if ( fVeryVerbose )
-                printf( "Comparing AIG %4d and AIG %4d.  ", Vec_IntEntry(vPos,k), i );
-            vMap = Iso_ManFindMapping( pTemp, pPart, 
-                (Vec_Int_t *)Vec_PtrEntry(vPerms, Vec_IntEntry(vPos,k)), 
-                (Vec_Int_t *)Vec_PtrEntry(vPerms, i),
-                fVeryVerbose );
-            if ( vMap != NULL )
-            {
-                if ( fVeryVerbose )
-                    printf( "Found match\n" );
-                if ( fVerbose )
-                    printf( "Found match for AIG %4d and AIG %4d.\n", Vec_IntEntry(vPos,k), i );
-                Vec_IntFree( vMap );
-                break;
-            }
-            if ( fVeryVerbose )
-                printf( "No match.\n" );
-        }
-        if ( k == Vec_PtrSize(vAigs) )
+        // assign adjacency to classes
+        Iso_ManAssignAdjacency( p );
+        // rehash the class nodes
+        Iso_ManRehashClassNodes( p );
+        Iso_ManPrintClasses( p, fVerbose, 0 );
+        // force refinement
+        while ( p->nSingles == 0 && p->nClasses )
         {
-            Vec_PtrPush( vAigs, pPart );
-            Vec_IntPush( vPos, i );
+            // assign IDs to the topmost level of classes
+            Iso_ManBreakTies( p, fVerbose );
+            // assign adjacency to classes
+            Iso_ManAssignAdjacency( p );
+            // rehash the class nodes
+            Iso_ManRehashClassNodes( p );
+            Iso_ManPrintClasses( p, fVerbose, 0 );
         }
     }
-    // delete AIGs
-    Vec_PtrForEachEntry( Aig_Man_t *, vParts, pPart, i )
-        Aig_ManStop( pPart );
-    Vec_PtrFree( vParts );
-    Vec_PtrForEachEntry( Vec_Int_t *, vPerms, vMap, i )
-        Vec_IntFree( vMap );
-    Vec_PtrFree( vPerms );
-    // derive the resulting AIG
-    pPart = Saig_ManDupCones( pAig, Vec_IntArray(vPos), Vec_IntSize(vPos) );
-    Vec_PtrFree( vAigs );
-    Vec_IntFree( vPos );
-
-//    printf( "The number of all checks %d.  Complex checks %d.\n", nPos*(nPos-1)/2, s_Counter );
-    return pPart;
-}
-
-
-#include "src/base/abc/abc.h"
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Aig_Man_t * Iso_ManTest( Aig_Man_t * pAig1, int fVerbose )
-{
-    extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
-    extern Abc_Ntk_t * Abc_NtkFromAigPhase( Aig_Man_t * pMan );
-    Abc_Ntk_t * pNtk;
-    Aig_Man_t * pAig2;
-    Vec_Int_t * vMap;
-    
-    pNtk = Abc_NtkFromAigPhase( pAig1 );
-    Abc_NtkPermute( pNtk, 1, 0, 1 );
-    pAig2 = Abc_NtkToDar( pNtk, 0, 1 );
-    Abc_NtkDelete( pNtk );
-
-    vMap = Iso_ManFindMapping( pAig1, pAig2, NULL, NULL, fVerbose );
-    Aig_ManStop( pAig2 );
-
-    if ( vMap != NULL )
-    {
-        printf( "Mapping of AIGs is found.\n" );
-        if ( fVerbose )
-            Vec_IntPrint( vMap );
-    }
-    else
-        printf( "Mapping of AIGs is NOT found.\n" );
-    Vec_IntFreeP( &vMap );
-    return NULL;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Aig_Man_t * Iso_ManTest666( Aig_Man_t * pAig, int fVerbose )
-{ 
-    Aig_Man_t * pPart;
-    int clk = clock();
-    pPart = Iso_ManFilterPos( pAig, fVerbose );
-    printf( "Reduced %d outputs to %d outputs.  ", Saig_ManPoNum(pAig), Saig_ManPoNum(pPart) );
-    Abc_PrintTime( 1, "Time", clock() - clk );
-//    Aig_ManStop( pPart );
-    return pPart;
+//    printf( "IDs assigned = %d.  Objects = %d.\n", p->nObjIds, 1+Aig_ManPiNum(p->pAig)+Aig_ManNodeNum(p->pAig) );
+    assert( p->nObjIds == 1+Aig_ManPiNum(p->pAig)+Aig_ManNodeNum(p->pAig) );
+//    if ( p->nClasses )
+//        Iso_ManDumpOneClass( p );
+    vRes = Iso_ManFinalize( p );
+    Iso_ManStop( p );
+    return vRes;
 }
 
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Aig_Man_t * Iso_ManTest777( Aig_Man_t * pAig, int fVerbose )
-{
-    Vec_Int_t * vPerm;
-    vPerm = Iso_ManFindPerm( pAig, fVerbose );
-    Vec_IntFree( vPerm );
-    return NULL;
-}
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index a4b5d566..8a95e252 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -278,6 +278,7 @@ static int Abc_CommandReconcile              ( Abc_Frame_t * pAbc, int argc, cha
 static int Abc_CommandCexMin                 ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandDualRail               ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandBlockPo                ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandIso                    ( Abc_Frame_t * pAbc, int argc, char ** argv );
 
 static int Abc_CommandTraceStart             ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandTraceCheck             ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -690,6 +691,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "Verification", "cexmin",        Abc_CommandCexMin,           0 );
     Cmd_CommandAdd( pAbc, "Verification", "dualrail",      Abc_CommandDualRail,         1 );
     Cmd_CommandAdd( pAbc, "Verification", "blockpo",       Abc_CommandBlockPo,          1 );
+    Cmd_CommandAdd( pAbc, "Verification", "iso",           Abc_CommandIso,              1 );
 
     Cmd_CommandAdd( pAbc, "ABC9",         "&get",          Abc_CommandAbc9Get,          0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&put",          Abc_CommandAbc9Put,          0 );
@@ -8839,17 +8841,26 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
     extern int Abc_NtkSuppSizeTest( Abc_Ntk_t * p );
     extern Aig_Man_t * Iso_ManTest( Aig_Man_t * pAig, int fVerbose );
     extern Abc_Ntk_t * Abc_NtkFromAigPhase( Aig_Man_t * pMan );
+    extern Vec_Vec_t * Saig_IsoDetectFast( Aig_Man_t * pAig );
     if ( pNtk )
     {
         Aig_Man_t * pAig = Abc_NtkToDar( pNtk, 0, 1 );
         Aig_Man_t * pRes;
-        Abc_Ntk_t * pNtkRes;
+//        Abc_Ntk_t * pNtkRes;
 //        Aig_ManInterRepar( pAig, 1 );
 //        Aig_ManInterTest( pAig, 1 );
 //        Aig_ManSupportsTest( pAig );
 //        Aig_SupportSizeTest( pAig );
+        if ( !fNewAlgo )
+            Saig_IsoDetectFast( pAig );
+        else
+        {
+            pRes = Iso_ManTest( pAig, fVerbose );
+            Aig_ManStopP( &pRes );
+        }
+
+/*
         pRes = Iso_ManTest( pAig, fVerbose );
-        Aig_ManStop( pAig );
         if ( pRes != NULL )
         {
             pNtkRes = Abc_NtkFromAigPhase( pRes );
@@ -8859,6 +8870,8 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
             pNtkRes->pName = Extra_UtilStrsav(pNtk->pName);
             Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
         }
+*/
+        Aig_ManStop( pAig );
     }
 }
 
@@ -21300,6 +21313,77 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
+int Abc_CommandIso( Abc_Frame_t * pAbc, int argc, char ** argv )
+{   
+    extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
+    extern Abc_Ntk_t * Abc_NtkFromAigPhase( Aig_Man_t * pMan );
+    Abc_Ntk_t * pNtk, * pNtkNew = NULL;
+    Aig_Man_t * pAig, * pTemp;
+    int c, fVerbose = 0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            Abc_Print( -2, "Unknown switch.\n");
+            goto usage;
+        }
+    }
+
+    // check the main AIG
+    pNtk = Abc_FrameReadNtk(pAbc);
+    if ( pNtk == NULL )
+    {
+        Abc_Print( 1, "Main AIG: There is no current network.\n");
+        return 0;
+    }
+    if ( !Abc_NtkIsStrash(pNtk) )
+    {
+        Abc_Print( 1, "Main AIG: The current network is not an AIG.\n");
+        return 0;
+    }
+    if ( Abc_NtkPoNum(pNtk) == 1 )
+    {
+        Abc_Print( 1, "Current AIG has only one PO. Transformation is not performed.\n");
+        return 0;
+    }
+
+    // transform
+    pAig = Abc_NtkToDar( pNtk, 0, 1 );
+    pTemp = Saig_ManIsoReduce( pAig, fVerbose );
+    pNtkNew = Abc_NtkFromAigPhase( pTemp );
+    Aig_ManStop( pTemp );
+    Aig_ManStop( pAig );
+
+    // replace the current network
+    Abc_FrameReplaceCurrentNetwork( pAbc, pNtkNew );
+    return 0;
+
+usage:
+    Abc_Print( -2, "usage: iso [-vh]\n" );
+    Abc_Print( -2, "\t         removes POs with isomorphic sequential COI\n" );
+    Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
+    Abc_Print( -2, "\t-h     : print the command usage\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Abc_CommandTraceStart( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
diff --git a/src/base/io/io.c b/src/base/io/io.c
index 92dbe9fc..550ff7dd 100644
--- a/src/base/io/io.c
+++ b/src/base/io/io.c
@@ -1382,12 +1382,16 @@ int IoCommandWriteAiger( Abc_Frame_t * pAbc, int argc, char **argv )
     char * pFileName;
     int fWriteSymbols;
     int fCompact;
+    int fUnique;
+    int fVerbose;
     int c;
 
-    fCompact      = 1;
     fWriteSymbols = 0;
+    fCompact      = 1;
+    fUnique       = 0;
+    fVerbose      = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "sch" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "scuvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -1397,6 +1401,12 @@ int IoCommandWriteAiger( Abc_Frame_t * pAbc, int argc, char **argv )
             case 'c':
                 fCompact ^= 1;
                 break;
+            case 'u':
+                fUnique ^= 1;
+                break;
+            case 'v':
+                fVerbose ^= 1;
+                break;
             case 'h':
                 goto usage;
             default:
@@ -1418,14 +1428,29 @@ int IoCommandWriteAiger( Abc_Frame_t * pAbc, int argc, char **argv )
         fprintf( stdout, "Writing this format is only possible for structurally hashed AIGs.\n" );
         return 1;
     }
-    Io_WriteAiger( pAbc->pNtkCur, pFileName, fWriteSymbols, fCompact );
+    if ( fUnique )
+    {
+        extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
+        extern Abc_Ntk_t * Abc_NtkFromAigPhase( Aig_Man_t * pMan );
+        Aig_Man_t * pAig = Abc_NtkToDar( pAbc->pNtkCur, 0, 1 );
+        Aig_Man_t * pCan = Saig_ManDupIsoCanonical( pAig, fVerbose );
+        Abc_Ntk_t * pTemp = Abc_NtkFromAigPhase( pCan );
+        Aig_ManStop( pCan );
+        Aig_ManStop( pAig );
+        Io_WriteAiger( pTemp, pFileName, fWriteSymbols, fCompact, fUnique );
+        Abc_NtkDelete( pTemp );
+    }
+    else
+        Io_WriteAiger( pAbc->pNtkCur, pFileName, fWriteSymbols, fCompact, fUnique );
     return 0;
 
 usage:
-    fprintf( pAbc->Err, "usage: write_aiger [-sch] <file>\n" );
+    fprintf( pAbc->Err, "usage: write_aiger [-scuvh] <file>\n" );
     fprintf( pAbc->Err, "\t         writes the network in the AIGER format (http://fmv.jku.at/aiger)\n" );
     fprintf( pAbc->Err, "\t-s     : toggle saving I/O names [default = %s]\n", fWriteSymbols? "yes" : "no" );
     fprintf( pAbc->Err, "\t-c     : toggle writing more compactly [default = %s]\n", fCompact? "yes" : "no" );
+    fprintf( pAbc->Err, "\t-u     : toggle writing canonical AIG structure [default = %s]\n", fUnique? "yes" : "no" );
+    fprintf( pAbc->Err, "\t-v     : toggle printing verbose information [default = %s]\n", fVerbose? "yes" : "no" );
     fprintf( pAbc->Err, "\t-h     : print the help massage\n" );
     fprintf( pAbc->Err, "\tfile   : the name of the file to write (extension .aig)\n" );
     return 1;
diff --git a/src/base/io/ioAbc.h b/src/base/io/ioAbc.h
index 7a38ae5c..14d688f0 100644
--- a/src/base/io/ioAbc.h
+++ b/src/base/io/ioAbc.h
@@ -96,7 +96,7 @@ extern Abc_Ntk_t *        Io_ReadPla( char * pFileName, int fZeros, int fCheck )
 /*=== abcReadVerilog.c ========================================================*/
 extern Abc_Ntk_t *        Io_ReadVerilog( char * pFileName, int fCheck );
 /*=== abcWriteAiger.c =========================================================*/
-extern void               Io_WriteAiger( Abc_Ntk_t * pNtk, char * pFileName, int fWriteSymbols, int fCompact );
+extern void               Io_WriteAiger( Abc_Ntk_t * pNtk, char * pFileName, int fWriteSymbols, int fCompact, int fUnique );
 extern void               Io_WriteAigerCex( Abc_Cex_t * pCex, Abc_Ntk_t * pNtk, void * pG, char * pFileName );
 /*=== abcWriteBaf.c ===========================================================*/
 extern void               Io_WriteBaf( Abc_Ntk_t * pNtk, char * pFileName );
diff --git a/src/base/io/ioUtil.c b/src/base/io/ioUtil.c
index e8a018c2..dbaa9138 100644
--- a/src/base/io/ioUtil.c
+++ b/src/base/io/ioUtil.c
@@ -320,7 +320,7 @@ void Io_Write( Abc_Ntk_t * pNtk, char * pFileName, Io_FileType_t FileType )
             return;
         }
         if ( FileType == IO_FILE_AIGER )
-            Io_WriteAiger( pNtk, pFileName, 1, 0 );
+            Io_WriteAiger( pNtk, pFileName, 1, 0, 0 );
         else //if ( FileType == IO_FILE_BAF )
             Io_WriteBaf( pNtk, pFileName );
         return;
diff --git a/src/base/io/ioWriteAiger.c b/src/base/io/ioWriteAiger.c
index 0f725be3..93b17c37 100644
--- a/src/base/io/ioWriteAiger.c
+++ b/src/base/io/ioWriteAiger.c
@@ -581,7 +581,7 @@ int fprintfBz2Aig( bz2file * b, char * fmt, ... ) {
   SeeAlso     []
 
 ***********************************************************************/
-void Io_WriteAiger( Abc_Ntk_t * pNtk, char * pFileName, int fWriteSymbols, int fCompact )
+void Io_WriteAiger( Abc_Ntk_t * pNtk, char * pFileName, int fWriteSymbols, int fCompact, int fUnique )
 {
     ProgressBar * pProgress;
 //    FILE * pFile;
@@ -591,6 +591,13 @@ void Io_WriteAiger( Abc_Ntk_t * pNtk, char * pFileName, int fWriteSymbols, int f
     unsigned uLit0, uLit1, uLit;
     bz2file b;
 
+    // define unique writing
+    if ( fUnique )
+    {
+        fWriteSymbols = 0;
+        fCompact = 0;
+    }
+
     // check that the network is valid
     assert( Abc_NtkIsStrash(pNtk) );
     Abc_NtkForEachLatch( pNtk, pObj, i )
@@ -750,10 +757,13 @@ void Io_WriteAiger( Abc_Ntk_t * pNtk, char * pFileName, int fWriteSymbols, int f
 
     // write the comment
     fprintfBz2Aig( &b, "c" );
-    if ( pNtk->pName && strlen(pNtk->pName) > 0 )
-        fprintfBz2Aig( &b, "\n%s%c", pNtk->pName, '\0' );
-    fprintfBz2Aig( &b, "\nThis file was written by ABC on %s\n", Extra_TimeStamp() );
-    fprintfBz2Aig( &b, "For information about AIGER format, refer to %s\n", "http://fmv.jku.at/aiger" );
+    if ( !fUnique )
+    {
+        if ( pNtk->pName && strlen(pNtk->pName) > 0 )
+            fprintfBz2Aig( &b, "\n%s%c", pNtk->pName, '\0' );
+        fprintfBz2Aig( &b, "\nThis file was written by ABC on %s\n", Extra_TimeStamp() );
+        fprintfBz2Aig( &b, "For information about AIGER format, refer to %s\n", "http://fmv.jku.at/aiger" );
+    }
 
     // close the file
     if (b.b) {
diff --git a/src/misc/vec/vecInt.h b/src/misc/vec/vecInt.h
index be54e583..39ab2623 100644
--- a/src/misc/vec/vecInt.h
+++ b/src/misc/vec/vecInt.h
@@ -1259,6 +1259,26 @@ static inline void Vec_IntPrint( Vec_Int_t * vVec )
     printf( " }\n" );
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Vec_IntCompareVec( Vec_Int_t * p1, Vec_Int_t * p2 )
+{
+    if ( p1 == NULL || p2 == NULL )
+        return (p1 != NULL) - (p2 != NULL);
+    if ( Vec_IntSize(p1) != Vec_IntSize(p2) )
+        return Vec_IntSize(p1) - Vec_IntSize(p2);
+    return memcmp( Vec_IntArray(p1), Vec_IntArray(p2), sizeof(int)*Vec_IntSize(p1) );
+}
+
 
 ABC_NAMESPACE_HEADER_END
 
diff --git a/src/misc/vec/vecStr.h b/src/misc/vec/vecStr.h
index cec3e7e1..c794dc2f 100644
--- a/src/misc/vec/vecStr.h
+++ b/src/misc/vec/vecStr.h
@@ -650,6 +650,26 @@ static inline void Vec_StrSort( Vec_Str_t * p, int fReverse )
                 (int (*)(const void *, const void *)) Vec_StrSortCompare1 );
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Vec_StrCompareVec( Vec_Str_t * p1, Vec_Str_t * p2 )
+{
+    if ( p1 == NULL || p2 == NULL )
+        return (p1 != NULL) - (p2 != NULL);
+    if ( Vec_StrSize(p1) != Vec_StrSize(p2) )
+        return Vec_StrSize(p1) - Vec_StrSize(p2);
+    return memcmp( Vec_StrArray(p1), Vec_StrArray(p2), Vec_StrSize(p1) );
+}
+
 
 
 ABC_NAMESPACE_HEADER_END