Isomorphism checking code.

5 files changed, 603 insertions, 138 deletions

diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index 96cfda34..2c7d57b2 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -623,6 +623,7 @@ extern void                Gia_WriteAiger( Gia_Man_t * p, char * pFileName, int
 extern void                Gia_DumpAiger( Gia_Man_t * p, char * pFilePrefix, int iFileNum, int nFileNumDigits );
 extern Vec_Str_t *         Gia_WriteAigerIntoMemoryStr( Gia_Man_t * p );
 extern Vec_Str_t *         Gia_WriteAigerIntoMemoryStrPart( Gia_Man_t * p, Vec_Int_t * vCis, Vec_Int_t * vAnds, Vec_Int_t * vCos, int nRegs );
+extern void                Gia_WriteAigerSimple( Gia_Man_t * pInit, char * pFileName );
 /*=== giaBidec.c ===========================================================*/
 extern unsigned *          Gia_ManConvertAigToTruth( Gia_Man_t * p, Gia_Obj_t * pRoot, Vec_Int_t * vLeaves, Vec_Int_t * vTruth, Vec_Int_t * vVisited );
 extern Gia_Man_t *         Gia_ManPerformBidec( Gia_Man_t * p, int fVerbose );
@@ -735,6 +736,9 @@ extern void                Gia_ManHashProfile( Gia_Man_t * p );
 extern int                 Gia_ManHashLookup( Gia_Man_t * p, Gia_Obj_t * p0, Gia_Obj_t * p1 );
 /*=== giaIf.c ===========================================================*/
 extern void                Gia_ManPrintNpnClasses( Gia_Man_t * p );
+/*=== giaIso.c ===========================================================*/
+extern Gia_Man_t *         Gia_ManIsoCanonicize( Gia_Man_t * p, int fVerbose );
+extern Gia_Man_t *         Gia_ManIsoReduce( Gia_Man_t * p, Vec_Ptr_t ** pvPosEquivs, int fVerbose );
 /*=== giaLogic.c ===========================================================*/
 extern void                Gia_ManTestDistance( Gia_Man_t * p );
 extern void                Gia_ManSolveProblem( Gia_Man_t * pGia, Emb_Par_t * pPars );
diff --git a/src/aig/gia/giaAiger.c b/src/aig/gia/giaAiger.c
index 5f1bb25d..a0adce33 100644
--- a/src/aig/gia/giaAiger.c
+++ b/src/aig/gia/giaAiger.c
@@ -1614,7 +1614,7 @@ Vec_Str_t * Gia_WriteAigerIntoMemoryStr( Gia_Man_t * p )
     Gia_Obj_t * pObj;
     int nNodes = 0, i, uLit, uLit0, uLit1; 
     // set the node numbers to be used in the output file
-    Gia_ManConst1(p)->Value = nNodes++;
+    Gia_ManConst0(p)->Value = nNodes++;
     Gia_ManForEachCi( p, pObj, i )
         pObj->Value = nNodes++;
     Gia_ManForEachAnd( p, pObj, i )
@@ -1638,7 +1638,6 @@ Vec_Str_t * Gia_WriteAigerIntoMemoryStr( Gia_Man_t * p )
     Gia_ManForEachRi( p, pObj, i )
     {
         uLit = Abc_Var2Lit( Gia_ObjValue(Gia_ObjFanin0(pObj)), Gia_ObjFaninC0(pObj) );
-//        fprintf( pFile, "%u\n", uLit );
         Vec_StrPrintNum( vBuffer, uLit );
         Vec_StrPrintStr( vBuffer, "\n" );
     }
@@ -1647,7 +1646,6 @@ Vec_Str_t * Gia_WriteAigerIntoMemoryStr( Gia_Man_t * p )
     Gia_ManForEachPo( p, pObj, i )
     {
         uLit = Abc_Var2Lit( Gia_ObjValue(Gia_ObjFanin0(pObj)), Gia_ObjFaninC0(pObj) );
-//        fprintf( pFile, "%u\n", uLit );
         Vec_StrPrintNum( vBuffer, uLit );
         Vec_StrPrintStr( vBuffer, "\n" );
     }
@@ -1679,7 +1677,7 @@ Vec_Str_t * Gia_WriteAigerIntoMemoryStr( Gia_Man_t * p )
   The CI/CO/AND nodes are assumed to be ordered according to some rule.
   The resulting buffer should be deallocated by the user.]
   
-  SideEffects [Note that in vCos, the latches should be ordered first!!!]
+  SideEffects [Note that in vCos, PIs are order first, followed by latches!]
 
   SeeAlso     []
 
@@ -1690,7 +1688,7 @@ Vec_Str_t * Gia_WriteAigerIntoMemoryStrPart( Gia_Man_t * p, Vec_Int_t * vCis, Ve
     Gia_Obj_t * pObj;
     int nNodes = 0, i, uLit, uLit0, uLit1; 
     // set the node numbers to be used in the output file
-    Gia_ManConst1(p)->Value = nNodes++;
+    Gia_ManConst0(p)->Value = nNodes++;
     Gia_ManForEachObjVec( vCis, p, pObj, i )
     {
         assert( Gia_ObjIsCi(pObj) );
@@ -1720,8 +1718,19 @@ Vec_Str_t * Gia_WriteAigerIntoMemoryStrPart( Gia_Man_t * p, Vec_Int_t * vCis, Ve
     Gia_ManForEachObjVec( vCos, p, pObj, i )
     {
         assert( Gia_ObjIsCo(pObj) );
+        if ( i < Vec_IntSize(vCos) - nRegs )
+            continue;
+        uLit = Abc_Var2Lit( Gia_ObjValue(Gia_ObjFanin0(pObj)), Gia_ObjFaninC0(pObj) );
+        Vec_StrPrintNum( vBuffer, uLit );
+        Vec_StrPrintStr( vBuffer, "\n" );
+    }
+    // write output drivers
+    Gia_ManForEachObjVec( vCos, p, pObj, i )
+    {
+        assert( Gia_ObjIsCo(pObj) );
+        if ( i >= Vec_IntSize(vCos) - nRegs )
+            continue;
         uLit = Abc_Var2Lit( Gia_ObjValue(Gia_ObjFanin0(pObj)), Gia_ObjFaninC0(pObj) );
-//        fprintf( pFile, "%u\n", uLit );
         Vec_StrPrintNum( vBuffer, uLit );
         Vec_StrPrintStr( vBuffer, "\n" );
     }
@@ -1746,6 +1755,40 @@ Vec_Str_t * Gia_WriteAigerIntoMemoryStrPart( Gia_Man_t * p, Vec_Int_t * vCis, Ve
     return vBuffer;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Writes the AIG in the binary AIGER format.]
+
+  Description []
+  
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_WriteAigerSimple( Gia_Man_t * pInit, char * pFileName )
+{
+    FILE * pFile;
+    Vec_Str_t * vStr;
+    if ( Gia_ManPoNum(pInit) == 0 )
+    {
+        printf( "Gia_WriteAigerSimple(): AIG cannot be written because it has no POs.\n" );
+        return;
+    }
+    // start the output stream
+    pFile = fopen( pFileName, "wb" );
+    if ( pFile == NULL )
+    {
+        fprintf( stdout, "Gia_WriteAigerSimple(): Cannot open the output file \"%s\".\n", pFileName );
+        return;
+    }
+    // write the buffer
+    vStr = Gia_WriteAigerIntoMemoryStr( pInit );
+    fwrite( Vec_StrArray(vStr), 1, Vec_StrSize(vStr), pFile );
+    Vec_StrFree( vStr );
+    fclose( pFile );
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c
index 577a0180..7084a38e 100644
--- a/src/aig/gia/giaDup.c
+++ b/src/aig/gia/giaDup.c
@@ -1791,7 +1791,7 @@ Gia_Man_t * Gia_ManDupCones( Gia_Man_t * p, int * pPos, int nPos )
         Gia_ManDupCones_rec( p, pObj, vLeaves, vNodes, vRoots );
 
     // start the new manager
-    Gia_ManFillValue( p );
+//    Gia_ManFillValue( p );
     pNew = Gia_ManStart( Vec_PtrSize(vLeaves) + Vec_PtrSize(vNodes) + Vec_PtrSize(vRoots) + 1);
     pNew->pName = Abc_UtilStrsav( p->pName );
     // map the constant node
diff --git a/src/aig/gia/giaIso.c b/src/aig/gia/giaIso.c
index bdbb0d2d..fc726d8d 100644
--- a/src/aig/gia/giaIso.c
+++ b/src/aig/gia/giaIso.c
@@ -59,41 +59,6 @@ static int s_256Primes[ISO_MASK+1] =
     0x6918928b,0xde3126bb,0x6c99835c,0x63ba1fa2,0xdebbdff0,0x3d02e541,0xd6f7aac6,0xe80b4cd0,
     0xd0fa29f1,0x804cac5e,0x2c226798,0x462f624c,0xad05b377,0x22924fcd,0xfbea205c,0x1b47586d
 };
-static int s_256Primes2[ISO_MASK+1] = 
-{
-    0xcaa57efb,0x64bd4878,0x3419334a,0x712e5f6b,0x9fa9d687,0x06f8645f,0x620ca96f,0xdc5d6cce,
-    0x392f3257,0x52140f06,0xc4b3bda4,0xe8c7eba7,0x066bd754,0xc5941f26,0xe6dfd573,0x328dd14d,
-    0xb1cb4ba7,0x1d37a9b8,0x96a195a5,0x970e535a,0x290351b8,0x570000f6,0xe14ae341,0x35ede6a6,
-    0x9a02f032,0xaf2ebb58,0x146be492,0x670b3e4b,0x72fa6cfd,0xa243af97,0xbbd5fc21,0xcb8852a2,
-    0x5d5b4a42,0xeefff0ac,0xa59ad1b6,0x3ec55544,0x48d64f69,0x9065d3d0,0xdd09485b,0xdd63bd09,
-    0x605e811d,0xc4b4ed7d,0xb0b58558,0x0644400b,0x12222346,0x086f146a,0xad6dee36,0x5488d1a3,
-    0x0c93bc0c,0x18555d92,0x9f4427bf,0xa590a66a,0x3a630fda,0xf1681c2e,0x948a16fb,0x16fe3338,
-    0xc9832357,0xd1e8e6b5,0xd9cfe034,0x05b22f26,0x27233c6e,0x355890e1,0xfbe6eaf3,0x0dcd8e8f,
-    0x00b5df46,0xd97730ac,0xc6dfd8ff,0x0cb1840a,0x41e9d249,0xbb471b4e,0x480b8f63,0x1ffe8871,
-    0x17b11821,0x1709e440,0xcefb3668,0xa4954ddd,0xf03ef8b5,0x6b3e633c,0xe5813096,0x3697c9a6,
-    0x7800f52f,0x73a7aa39,0x59ac23b7,0xb4663166,0x9ca9d6f8,0x2d441072,0x38cef3d3,0x39a3faf6,
-    0x89299fb9,0xd558295f,0xcf79c633,0x232dd96e,0xadb2955b,0xe962cbb9,0xab7c0061,0x1027c329,
-    0xb4b43e07,0x25240a7a,0x98ea4825,0xdbf2edbd,0x8be15d26,0x879f3cd9,0xa4138089,0xa32dcb06,
-    0x602af961,0x4b13f451,0x1c87d0d5,0xc3bb141b,0x9ebf55a1,0xef030a9a,0x8d199b93,0xdabcbb56,
-    0xf412f80f,0x302e90ad,0xc4d9878b,0xc392f650,0x4fd3a614,0x0a96ddc4,0xcd1878c7,0x9ddd3ae1,
-    0xdaf46458,0xba7c8656,0xf667948f,0xc37e3c23,0x04a577c6,0xbe615f1e,0xcc97406c,0xd497f16f,
-    0x79586586,0xd2057d14,0x1bb92028,0xab888e5e,0x26bef100,0xf46b3671,0xf21f1acc,0x67f288c8,
-    0x39c722df,0x61d21eaf,0x9c5853a0,0x63b693c7,0x1ea53c0a,0x95bc0a85,0xa7372f2d,0x3ef6a6b3,
-    0x82c9c4ac,0x4dea10ee,0xdfcb543d,0xd412f427,0x53e27f2c,0x875d8422,0x5367a7d8,0x41acf3fa,
-    0xbce47234,0x8056fb9a,0x4e9a4c48,0xe4a45945,0x2cfee3ae,0xb4554b10,0x5e37a915,0x591b1963,
-    0x4fa255c1,0xe01c897b,0x504e6208,0x7c7368eb,0x13808fd7,0x02ac0816,0x30305d2c,0x6c4bbdb7,
-    0xa48a9599,0x57466059,0x4c6ebfc7,0x8587ccdf,0x6ff0abf0,0x5b6b63fe,0x31d9ec64,0x63458abd,
-    0x21245905,0xccdb28fc,0xac828acb,0xe5e82bea,0xa7d76141,0xa699038e,0xcaba7e06,0x2710253f,
-    0x2ff9c94d,0x26e48a2c,0xd713ec5e,0x869f2ed4,0x25bcd712,0xcb3e918f,0x615c3a5a,0x9fb43903,
-    0x37900eb9,0x4f682db0,0x35a80dc6,0x4eb27c65,0x502735ab,0xb163b4c8,0x604649a8,0xb23a6cd3,
-    0x9f715091,0x2e6fbb51,0x2ec9144b,0x272cbe65,0x90a0a453,0x420e1503,0x2d00d338,0x4aa96675,
-    0xd025b61c,0xab02d9d7,0x2afe2a37,0xf8129b9b,0x4db04c54,0x654a5c06,0x3213ff51,0x4e09d0b1,
-    0x333369a3,0xae27310a,0x91d076d0,0xa96ebcd0,0xefde54f4,0x021c309a,0xd506f53d,0xa5635251,
-    0x2f23916e,0x1fe86bb1,0xcbc62160,0x2147c8cc,0xdeb3e47c,0x028e3987,0x8061de42,0x39be931b,
-    0x2b7e54c5,0xe64d2f96,0x4069522d,0x4aa66857,0x83b62634,0x4ba72095,0x9aade2a9,0xf1223cd9,
-    0x91cbddf0,0xec5d237f,0x593f3280,0x0b924439,0x446f4063,0xc66f8d8c,0x8b7128ba,0xb597f451,
-    0xc8925236,0x1720f235,0x7cd2e9a0,0x4c130339,0x8a665a52,0x5bef2733,0xba35d9bc,0x6d26644c
-};
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
@@ -174,6 +139,14 @@ void Gia_IsoManStop( Gia_IsoMan_t * p )
     ABC_FREE( p->pStoreW );
     ABC_FREE( p );
 }
+void Gia_IsoManTransferUnique( Gia_IsoMan_t * p )
+{
+    Gia_Obj_t * pObj;
+    int i;
+    // copy unique numbers into the nodes
+    Gia_ManForEachObj( p->pGia, pObj, i )
+        pObj->Value = p->pUniques[i];
+}
 
 
 /**Function*************************************************************
@@ -258,6 +231,7 @@ void Gia_IsoPrepare( Gia_IsoMan_t * p )
     pLevBegins[0] = 1;
     for ( i = 0; i <= MaxLev; i++ )
     {
+        assert( pLevSizes[i] > 0 ); // we do not allow AIG has a const node and no PIs
         Vec_IntPush( p->vClasses, pLevBegins[i] );
         Vec_IntPush( p->vClasses, pLevSizes[i] );
         pLevBegins[i+1] = pLevBegins[i] + pLevSizes[i];
@@ -265,10 +239,7 @@ void Gia_IsoPrepare( Gia_IsoMan_t * p )
     assert( pLevBegins[MaxLev+1] == p->nObjs );
     // put them into the structure
     for ( i = 1; i < p->nObjs; i++ )
-    {
-//        Gia_IsoSetValue( p, pLevBegins[p->pLevels[i]], p->pLevels[i] );
         Gia_IsoSetItem( p, pLevBegins[p->pLevels[i]]++, i );
-    }
     ABC_FREE( pLevBegins );
     ABC_FREE( pLevSizes );
 /*
@@ -324,57 +295,6 @@ void Gia_IsoAssignUnique( Gia_IsoMan_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-static inline unsigned Gia_IsoUpdate( int Iter, int iLevel, int iUniqueF, int fCompl )
-{
-//    iLevel = ((Iter + iLevel) * (Iter + iLevel + 1)) >> 1;
-    if ( iUniqueF == 0 )
-        return iLevel * s_256Primes[Abc_Var2Lit(iLevel, fCompl) & ISO_MASK];
-//    iUniqueF = ((Iter + iUniqueF) * (Iter + iUniqueF + 1)) >> 1;
-    return iLevel * s_256Primes[Abc_Var2Lit(iLevel, fCompl) & ISO_MASK] + 
-           iUniqueF * s_256Primes[Abc_Var2Lit(iUniqueF, fCompl) & ISO_MASK];
-}
-void Gia_IsoSimulate( Gia_IsoMan_t * p, int Iter )
-{
-    Gia_Obj_t * pObj, * pObjF;
-    int i, iObj;
-    // initialize constant, inputs, and flops in the first frame
-//    Gia_ManConst0(p->pGia)->Value = s_256Primes2[Abc_Var2Lit(Iter, 0) & ISO_MASK];
-    Gia_ManConst0(p->pGia)->Value = s_256Primes2[ISO_MASK-2];
-    Gia_ManForEachPi( p->pGia, pObj, i )
-//        pObj->Value = s_256Primes2[Abc_Var2Lit(Iter, 1) & ISO_MASK];
-        pObj->Value = s_256Primes2[ISO_MASK-1];
-    if ( Iter == 0 )
-        Gia_ManForEachRo( p->pGia, pObj, i )
-            pObj->Value = s_256Primes2[ISO_MASK];
-    // simulate objects
-    Gia_ManForEachAnd( p->pGia, pObj, i )
-    {
-        pObj->Value += Gia_ObjFanin0(pObj)->Value + Gia_IsoUpdate(Iter, p->pLevels[i], p->pUniques[Gia_ObjFaninId0(pObj, i)], Gia_ObjFaninC0(pObj));
-        pObj->Value += Gia_ObjFanin1(pObj)->Value + Gia_IsoUpdate(Iter, p->pLevels[i], p->pUniques[Gia_ObjFaninId1(pObj, i)], Gia_ObjFaninC1(pObj));
-//printf( "AND %3d: %08x\n", i, pObj->Value );
-    }
-    Gia_ManForEachCo( p->pGia, pObj, i )
-    {
-        iObj = Gia_ObjId(p->pGia, pObj);
-        pObj->Value += Gia_ObjFanin0(pObj)->Value + Gia_IsoUpdate(Iter, p->pLevels[iObj], p->pUniques[Gia_ObjFaninId0(pObj, iObj)], Gia_ObjFaninC0(pObj));
-//printf( "CO  %3d: %08x\n", i, pObj->Value );
-    }
-    // transfer flop values
-    Gia_ManForEachRiRo( p->pGia, pObjF, pObj, i )
-        pObj->Value += pObjF->Value;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
 int Gia_IsoSort( Gia_IsoMan_t * p )
 {
     Gia_Obj_t * pObj, * pObj0;
@@ -461,13 +381,12 @@ int Gia_IsoSort( Gia_IsoMan_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Ptr_t * Gia_IsoCollectCos( Gia_IsoMan_t * p, int fVerbose )
+Vec_Ptr_t * Gia_IsoCollectCosClasses( Gia_IsoMan_t * p, int fVerbose )
 {
     Vec_Ptr_t * vGroups;
     Vec_Int_t * vLevel;
     Gia_Obj_t * pObj;
     int i, k, iBegin, nSize;
-
     // add singletons
     vGroups = Vec_PtrAlloc( 1000 );
     Gia_ManForEachPo( p->pGia, pObj, i )
@@ -518,42 +437,258 @@ Vec_Ptr_t * Gia_IsoCollectCos( Gia_IsoMan_t * p, int fVerbose )
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Ptr_t * Gia_IsoDeriveEquivPos( Gia_Man_t * pGia, int fVerbose )
+static inline unsigned Gia_IsoUpdateValue( int Value, int fCompl )
 {
-    Vec_Ptr_t * vEquivs;
+    return (Value+1) * s_256Primes[Abc_Var2Lit(Value, fCompl) & ISO_MASK];
+}
+static inline unsigned Gia_IsoUpdate( Gia_IsoMan_t * p, int Iter, int iObj, int fCompl )
+{
+    if ( Iter == 0 )              return Gia_IsoUpdateValue( p->pLevels[iObj], fCompl );
+    if ( p->pUniques[iObj] > 0 )  return Gia_IsoUpdateValue( p->pUniques[iObj], fCompl );
+    return 0;
+}
+void Gia_IsoSimulate( Gia_IsoMan_t * p, int Iter )
+{
+    Gia_Obj_t * pObj, * pObjF;
+    int i, iObj;
+    // initialize constant, inputs, and flops in the first frame
+    Gia_ManConst0(p->pGia)->Value = s_256Primes[ISO_MASK];
+    Gia_ManForEachPi( p->pGia, pObj, i )
+        pObj->Value = s_256Primes[ISO_MASK-1];
+    if ( Iter == 0 )
+        Gia_ManForEachRo( p->pGia, pObj, i )
+            pObj->Value = s_256Primes[ISO_MASK-2];
+    // simulate nodes
+    Gia_ManForEachAnd( p->pGia, pObj, i )
+    {
+        pObj->Value += Gia_ObjFanin0(pObj)->Value + Gia_IsoUpdate(p, Iter, Gia_ObjFaninId0(pObj, i), Gia_ObjFaninC0(pObj));
+        pObj->Value += Gia_ObjFanin1(pObj)->Value + Gia_IsoUpdate(p, Iter, Gia_ObjFaninId1(pObj, i), Gia_ObjFaninC1(pObj));
+    }
+    // simulate COs
+    Gia_ManForEachCo( p->pGia, pObj, i )
+    {
+        iObj = Gia_ObjId(p->pGia, pObj);
+        pObj->Value += Gia_ObjFanin0(pObj)->Value + Gia_IsoUpdate(p, Iter, Gia_ObjFaninId0(pObj, iObj), Gia_ObjFaninC0(pObj));
+    }
+    // transfer flop values
+    Gia_ManForEachRiRo( p->pGia, pObjF, pObj, i )
+        pObj->Value += pObjF->Value;
+}
+void Gia_IsoSimulateBack( Gia_IsoMan_t * p, int Iter )
+{
+    Gia_Obj_t * pObj, * pObjF;
+    int i, iObj;
+    // simulate COs
+    Gia_ManForEachCo( p->pGia, pObj, i )
+    {
+        iObj = Gia_ObjId(p->pGia, pObj);
+        Gia_ObjFanin0(pObj)->Value += pObj->Value + Gia_IsoUpdate(p, Iter, iObj, Gia_ObjFaninC0(pObj));
+    }
+    // simulate objects
+    Gia_ManForEachAndReverse( p->pGia, pObj, i )
+    {
+        Gia_ObjFanin0(pObj)->Value += pObj->Value + Gia_IsoUpdate(p, Iter, i, Gia_ObjFaninC0(pObj));
+        Gia_ObjFanin1(pObj)->Value += pObj->Value + Gia_IsoUpdate(p, Iter, i, Gia_ObjFaninC1(pObj));
+    }
+    // transfer flop values
+    Gia_ManForEachRiRo( p->pGia, pObjF, pObj, i )
+        pObjF->Value += pObj->Value;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_IsoAssignOneClass2( Gia_IsoMan_t * p )
+{
+    int i, iBegin, nSize = -1;
+    // find two variable class
+    assert( Vec_IntSize(p->vClasses) > 0 );
+    Vec_IntForEachEntryDouble( p->vClasses, iBegin, nSize, i )
+    {
+        if ( nSize == 2 )
+            break;
+    }
+    assert( nSize > 1 );
+
+    if ( nSize == 2 )
+    {
+        assert( p->pUniques[Gia_IsoGetItem(p, iBegin)] == 0 );
+        p->pUniques[Gia_IsoGetItem(p, iBegin)] = p->nUniques++;
+        p->nSingles++;
+        p->nEntries--;
+
+        assert( p->pUniques[Gia_IsoGetItem(p, iBegin+1)] == 0 );
+        p->pUniques[Gia_IsoGetItem(p, iBegin+1)] = p->nUniques++;
+        p->nSingles++;
+        p->nEntries--;
+    }
+    else
+    {
+        assert( p->pUniques[Gia_IsoGetItem(p, iBegin)] == 0 );
+        p->pUniques[Gia_IsoGetItem(p, iBegin)] = p->nUniques++;
+        p->nSingles++;
+        p->nEntries--;
+    }
+
+    for ( ; i < Vec_IntSize(p->vClasses) - 2; i += 2 )
+    {
+        p->vClasses->pArray[i+0] = p->vClasses->pArray[i+2];
+        p->vClasses->pArray[i+1] = p->vClasses->pArray[i+3];
+    }
+    Vec_IntShrink( p->vClasses, Vec_IntSize(p->vClasses) - 2 );
+
+    printf( "Assinged class %d of size %d at level %d.\n", i/2, nSize, p->pLevels[Gia_IsoGetItem(p, iBegin)] );
+}
+
+void Gia_IsoAssignOneClass3( Gia_IsoMan_t * p )
+{
+    int iBegin, nSize;
+    // find the last class
+    assert( Vec_IntSize(p->vClasses) > 0 );
+    iBegin = Vec_IntEntry( p->vClasses, Vec_IntSize(p->vClasses) - 2 );
+    nSize  = Vec_IntEntry( p->vClasses, Vec_IntSize(p->vClasses) - 1 );
+    Vec_IntShrink( p->vClasses, Vec_IntSize(p->vClasses) - 2 );
+
+    // assign the class
+    assert( nSize > 1 );
+    if ( nSize == 2 )
+    {
+        assert( p->pUniques[Gia_IsoGetItem(p, iBegin)] == 0 );
+        p->pUniques[Gia_IsoGetItem(p, iBegin)] = p->nUniques++;
+        p->nSingles++;
+        p->nEntries--;
+
+        assert( p->pUniques[Gia_IsoGetItem(p, iBegin+1)] == 0 );
+        p->pUniques[Gia_IsoGetItem(p, iBegin+1)] = p->nUniques++;
+        p->nSingles++;
+        p->nEntries--;
+    }
+    else
+    {
+        assert( p->pUniques[Gia_IsoGetItem(p, iBegin)] == 0 );
+        p->pUniques[Gia_IsoGetItem(p, iBegin)] = p->nUniques++;
+        p->nSingles++;
+        p->nEntries--;
+    }
+    printf( "Assinged last class of size %d at level %d.\n", nSize, p->pLevels[Gia_IsoGetItem(p, iBegin)] );
+}
+
+void Gia_IsoAssignOneClass( Gia_IsoMan_t * p, int fVerbose )
+{
+    int i, k, iBegin0, iBegin, nSize, Shrink;
+    // find the classes with the highest level
+    assert( Vec_IntSize(p->vClasses) > 0 );
+    iBegin0 = Vec_IntEntry( p->vClasses, Vec_IntSize(p->vClasses) - 2 );
+    for ( i = Vec_IntSize(p->vClasses) - 2; i >= 0; i -= 2 )
+    {
+        iBegin = Vec_IntEntry( p->vClasses, i );
+        if ( p->pLevels[Gia_IsoGetItem(p, iBegin)] != p->pLevels[Gia_IsoGetItem(p, iBegin0)] )
+            break;
+    }
+    i += 2;
+    assert( i >= 0 );
+    // assign all classes starting with this one
+    for ( Shrink = i; i < Vec_IntSize(p->vClasses); i += 2 )
+    {
+        iBegin = Vec_IntEntry( p->vClasses, i );
+        nSize  = Vec_IntEntry( p->vClasses, i + 1 );
+        for ( k = 0; k < nSize; k++ )
+        {
+            assert( p->pUniques[Gia_IsoGetItem(p, iBegin+k)] == 0 );
+            p->pUniques[Gia_IsoGetItem(p, iBegin+k)] = p->nUniques++;
+            p->nSingles++;
+            p->nEntries--;
+        }
+        if ( fVerbose )
+            printf( "Assinged class of size %d at level %d.\n", nSize, p->pLevels[Gia_IsoGetItem(p, iBegin)] );
+    }
+    Vec_IntShrink( p->vClasses, Shrink );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Gia_IsoDeriveEquivPos( Gia_Man_t * pGia, int fForward, int fVerbose )
+{
+    int nIterMax = 10000;
     Gia_IsoMan_t * p;
-    int nIterMax = 1000, fRefined;
+    Vec_Ptr_t * vEquivs = NULL;
+    int fRefined, fRefinedAll;
     int i, c, clk = clock(), clkTotal = clock();
+    assert( Gia_ManCiNum(pGia) > 0 );
+    assert( Gia_ManPoNum(pGia) > 0 );
 
     Gia_ManCleanValue( pGia );
     p = Gia_IsoManStart( pGia );
     Gia_IsoPrepare( p );
     Gia_IsoAssignUnique( p );
     p->timeStart = clock() - clk;
-//    Gia_IsoPrintClasses( p );
     if ( fVerbose )
         Gia_IsoPrint( p, 0, clock() - clkTotal );
-    for ( i = 0, c = 0; i < nIterMax && c < 3; i++, c++ )
-    {
-        clk = clock();
-        Gia_IsoSimulate( p, i );
-        p->timeSim += clock() - clk;
 
-        clk = clock();
-        fRefined = Gia_IsoSort( p );
-        if ( fRefined )
-            c = 0;
-        p->timeRefine += clock() - clk;
+    i = 0;
+    if ( fForward )
+    {
+        for ( c = 0; i < nIterMax && c < 2; i++, c = fRefined ? 0 : c+1 )
+        {
+            clk = clock();   Gia_IsoSimulate( p, i );      p->timeSim += clock() - clk;
+            clk = clock();   fRefined = Gia_IsoSort( p );  p->timeRefine += clock() - clk;
+            if ( fVerbose )
+                Gia_IsoPrint( p, i+1, clock() - clkTotal );
+        }
+    }
+    else
+    {
+        while ( Vec_IntSize(p->vClasses) > 0 )
+        {
+            for ( fRefinedAll = 1; i < nIterMax && fRefinedAll; )
+            {
+                fRefinedAll = 0;
+                for ( c = 0; i < nIterMax && c < 2; i++, c = fRefined ? 0 : c+1 )
+                {
+                    clk = clock();   Gia_IsoSimulate( p, i );      p->timeSim += clock() - clk;
+                    clk = clock();   fRefined = Gia_IsoSort( p );  p->timeRefine += clock() - clk;
+                    if ( fVerbose )
+                        Gia_IsoPrint( p, i+1, clock() - clkTotal );
+                    fRefinedAll |= fRefined;
+                }
+                for ( c = 0; i < nIterMax && c < 2; i++, c = fRefined ? 0 : c+1 )
+                {
+                    clk = clock();   Gia_IsoSimulateBack( p, i );  p->timeSim += clock() - clk;
+                    clk = clock();   fRefined = Gia_IsoSort( p );  p->timeRefine += clock() - clk;
+                    if ( fVerbose )
+                        Gia_IsoPrint( p, i+1, clock() - clkTotal );
+                    fRefinedAll |= fRefined;
+                }
+            }
+            if ( Vec_IntSize(p->vClasses) > 0 )
+                Gia_IsoAssignOneClass( p, fVerbose );
 
-//        Gia_IsoPrintClasses( p );
+        }
         if ( fVerbose )
-            Gia_IsoPrint( p, i+1, clock() - clkTotal );
+            Gia_IsoPrint( p, i+2, clock() - clkTotal );
     }
+//    Gia_IsoPrintClasses( p );
     if ( fVerbose )
     {
         p->timeTotal = clock() - clkTotal;
         p->timeOther = p->timeTotal - p->timeStart - p->timeSim - p->timeRefine;
-
         ABC_PRTP( "Start    ", p->timeStart,              p->timeTotal );
         ABC_PRTP( "Simulate ", p->timeSim,                p->timeTotal );
         ABC_PRTP( "Refine   ", p->timeRefine-p->timeSort, p->timeTotal );
@@ -561,12 +696,239 @@ Vec_Ptr_t * Gia_IsoDeriveEquivPos( Gia_Man_t * pGia, int fVerbose )
         ABC_PRTP( "Other    ", p->timeOther,              p->timeTotal );
         ABC_PRTP( "TOTAL    ", p->timeTotal,              p->timeTotal );
     }
-    vEquivs = Gia_IsoCollectCos( p, fVerbose );
+    if ( Gia_ManPoNum(p->pGia) > 1 )
+        vEquivs = Gia_IsoCollectCosClasses( p, fVerbose );
+    Gia_IsoManTransferUnique( p );
     Gia_IsoManStop( p );
     return vEquivs;
 }
 
 
+
+
+/**Function*************************************************************
+
+  Synopsis    [Finds canonical ordering of CIs/COs/nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Gia_ObjCompareByValue( Gia_Obj_t ** pp1, Gia_Obj_t ** pp2 )
+{
+    Gia_Obj_t * pObj1 = *pp1;
+    Gia_Obj_t * pObj2 = *pp2;
+//    assert( pObj1->Value != pObj2->Value );
+    return (int)pObj1->Value - (int)pObj2->Value;
+}
+void Gia_ManFindCaninicalOrder_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vAnds )
+{
+    if ( Gia_ObjIsTravIdCurrent(p, pObj) )
+        return;
+    Gia_ObjSetTravIdCurrent(p, pObj);
+    assert( Gia_ObjIsAnd(pObj) );
+    if ( !Gia_ObjIsAnd(Gia_ObjFanin0(pObj)) || !Gia_ObjIsAnd(Gia_ObjFanin1(pObj)) )
+    {
+        Gia_ManFindCaninicalOrder_rec( p, Gia_ObjFanin0(pObj), vAnds );
+        Gia_ManFindCaninicalOrder_rec( p, Gia_ObjFanin1(pObj), vAnds );
+    }
+    else
+    {
+        assert( Gia_ObjFanin0(pObj)->Value != Gia_ObjFanin1(pObj)->Value );
+        if ( Gia_ObjFanin0(pObj)->Value < Gia_ObjFanin1(pObj)->Value )
+        {
+            Gia_ManFindCaninicalOrder_rec( p, Gia_ObjFanin0(pObj), vAnds );
+            Gia_ManFindCaninicalOrder_rec( p, Gia_ObjFanin1(pObj), vAnds );
+        }
+        else
+        {
+            Gia_ManFindCaninicalOrder_rec( p, Gia_ObjFanin1(pObj), vAnds );
+            Gia_ManFindCaninicalOrder_rec( p, Gia_ObjFanin0(pObj), vAnds );
+        }
+    }
+    Vec_IntPush( vAnds, Gia_ObjId(p, pObj) );
+}
+void Gia_ManFindCaninicalOrder( Gia_Man_t * p, Vec_Int_t * vCis, Vec_Int_t * vAnds, Vec_Int_t * vCos )
+{
+    Vec_Ptr_t * vTemp;
+    Gia_Obj_t * pObj;
+    int i;
+
+    vTemp = Vec_PtrAlloc( 1000 );
+    Vec_IntClear( vCis );
+    Vec_IntClear( vAnds );
+    Vec_IntClear( vCos );
+
+    // assign unique IDs to PIs
+    Vec_PtrClear( vTemp );
+    Gia_ManForEachPi( p, pObj, i )
+        Vec_PtrPush( vTemp, pObj );
+    Vec_PtrSort( vTemp, (int (*)(void))Gia_ObjCompareByValue );
+    // create the result
+    Vec_PtrForEachEntry( Gia_Obj_t *, vTemp, pObj, i )
+        Vec_IntPush( vCis, Gia_ObjId(p, pObj) );
+
+    // assign unique IDs to POs
+    if ( Gia_ManPoNum(p) == 1 )
+        Vec_IntPush( vCos, Gia_ObjId(p, Gia_ManPo(p, 0)) );
+    else
+    {
+        Vec_PtrClear( vTemp );
+        Gia_ManForEachPo( p, pObj, i )
+        {
+            pObj->Value = Abc_Var2Lit( Gia_ObjFanin0(pObj)->Value, Gia_ObjFaninC0(pObj) );
+            Vec_PtrPush( vTemp, pObj );
+        }
+        Vec_PtrSort( vTemp, (int (*)(void))Gia_ObjCompareByValue );
+        Vec_PtrForEachEntry( Gia_Obj_t *, vTemp, pObj, i )
+            Vec_IntPush( vCos, Gia_ObjId(p, pObj) );
+    }
+
+    // assign unique IDs to ROs
+    Vec_PtrClear( vTemp );
+    Gia_ManForEachRo( p, pObj, i )
+        Vec_PtrPush( vTemp, pObj );
+    Vec_PtrSort( vTemp, (int (*)(void))Gia_ObjCompareByValue );
+    // create the result
+    Vec_PtrForEachEntry( Gia_Obj_t *, vTemp, pObj, i )
+    {
+        Vec_IntPush( vCis, Gia_ObjId(p, pObj) );
+        Vec_IntPush( vCos, Gia_ObjId(p, Gia_ObjRoToRi(p, pObj)) );
+    }
+    Vec_PtrFree( vTemp );
+
+    // assign unique IDs to internal nodes
+    Gia_ManIncrementTravId( p );
+    Gia_ObjSetTravIdCurrent( p, Gia_ManConst0(p) );
+    Gia_ManForEachObjVec( vCis, p, pObj, i )
+        Gia_ObjSetTravIdCurrent( p, pObj );
+    Gia_ManForEachObjVec( vCos, p, pObj, i )
+        Gia_ManFindCaninicalOrder_rec( p, Gia_ObjFanin0(pObj), vAnds );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Gia_Man_t * Gia_ManDupFromVecs( Gia_Man_t * p, Vec_Int_t * vCis, Vec_Int_t * vAnds, Vec_Int_t * vCos, int nRegs )
+{
+    Gia_Man_t * pNew;
+    Gia_Obj_t * pObj;
+    int i;
+    // start the new manager
+    pNew = Gia_ManStart( 5000 );
+    pNew->pName = Abc_UtilStrsav( p->pName );
+    // create constant
+    Gia_ManConst0(p)->Value = 0;
+    // create PIs
+    Gia_ManForEachObjVec( vCis, p, pObj, i )
+        pObj->Value = Gia_ManAppendCi( pNew );
+    // create internal nodes
+    Gia_ManForEachObjVec( vAnds, p, pObj, i )
+        pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+    // create ROs
+    Gia_ManForEachObjVec( vCos, p, pObj, i )
+        pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
+    Gia_ManSetRegNum( pNew, nRegs );
+    return pNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Gia_Man_t * Gia_ManIsoCanonicize( Gia_Man_t * p, int fVerbose )
+{
+    Gia_Man_t * vResult = NULL;
+    Vec_Int_t * vCis, * vAnds, * vCos;
+    Vec_Ptr_t * vEquiv;
+    if ( Gia_ManCiNum(p) == 0 ) // const AIG
+    {
+        assert( Gia_ManPoNum(p) == 1 );
+        assert( Gia_ManObjNum(p) == 2 );
+        return Gia_ManDup(p);
+    }
+    // derive canonical values
+    vEquiv = Gia_IsoDeriveEquivPos( p, 0, fVerbose );
+    Vec_VecFreeP( (Vec_Vec_t **)&vEquiv );
+    // find canonical order of CIs/COs/nodes
+    // find canonical order
+    vCis  = Vec_IntAlloc( Gia_ManCiNum(p) );
+    vAnds = Vec_IntAlloc( Gia_ManAndNum(p) );
+    vCos  = Vec_IntAlloc( Gia_ManCoNum(p) );
+    Gia_ManFindCaninicalOrder( p, vCis, vAnds, vCos );
+    // derive the new AIG
+    vResult = Gia_ManDupFromVecs( p, vCis, vAnds, vCos, Gia_ManRegNum(p) );
+    // cleanup
+    Vec_IntFree( vCis );
+    Vec_IntFree( vAnds );
+    Vec_IntFree( vCos );
+    return vResult;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Str_t * Gia_ManIsoFindString( Gia_Man_t * p, int iPo, int fVerbose )
+{
+    Gia_Man_t * pPart;
+    Vec_Ptr_t * vEquiv;
+    Vec_Int_t * vCis, * vAnds, * vCos;
+    Vec_Str_t * vStr;
+    // duplicate
+    pPart = Gia_ManDupCones( p, &iPo, 1 );
+    assert( Gia_ManPoNum(pPart) == 1 );
+    if ( Gia_ManCiNum(pPart) == 0 ) // const AIG
+    {
+        assert( Gia_ManPoNum(pPart) == 1 );
+        assert( Gia_ManObjNum(pPart) == 2 );
+        vStr = Gia_WriteAigerIntoMemoryStr( pPart );
+        Gia_ManStop( pPart );
+        return vStr;
+    }
+    // derive canonical values
+    vEquiv = Gia_IsoDeriveEquivPos( pPart, 0, fVerbose );
+    Vec_VecFreeP( (Vec_Vec_t **)&vEquiv );
+    // find canonical order
+    vCis  = Vec_IntAlloc( Gia_ManCiNum(pPart) );
+    vAnds = Vec_IntAlloc( Gia_ManAndNum(pPart) );
+    vCos  = Vec_IntAlloc( Gia_ManCoNum(pPart) );
+    Gia_ManFindCaninicalOrder( pPart, vCis, vAnds, vCos );
+    // derive the AIGER string
+    vStr = Gia_WriteAigerIntoMemoryStrPart( pPart, vCis, vAnds, vCos, Gia_ManRegNum(pPart) );
+    // cleanup
+    Vec_IntFree( vCis );
+    Vec_IntFree( vAnds );
+    Vec_IntFree( vCos );
+    Gia_ManStop( pPart );
+    return vStr;
+}
+
 /**Function*************************************************************
 
   Synopsis    []
@@ -578,23 +940,65 @@ Vec_Ptr_t * Gia_IsoDeriveEquivPos( Gia_Man_t * pGia, int fVerbose )
   SeeAlso     []
 
 ***********************************************************************/
-Gia_Man_t * Gia_ManIsoReduce( Gia_Man_t * pGia, Vec_Ptr_t ** pvPosEquivs, int fVerbose )
+Gia_Man_t * Gia_ManIsoReduce( Gia_Man_t * p, Vec_Ptr_t ** pvPosEquivs, int fVerbose )
 { 
+    int fVeryVerbose = 0;
     Gia_Man_t * pPart;
-    Vec_Ptr_t * vEquivs;
-    Vec_Int_t * vRemain, * vLevel;
-    int i, clk = clock();
-    // create equivalences
-    vEquivs = Gia_IsoDeriveEquivPos( pGia, fVerbose );
+    Vec_Ptr_t * vEquivs, * vEquivs2, * vStrings;
+    Vec_Int_t * vRemain, * vLevel, * vLevel2;
+    Vec_Str_t * vStr, * vStr2;
+    int i, k, s, sStart, Entry, clk = clock();
+
+    // create preliminary equivalences
+    vEquivs = Gia_IsoDeriveEquivPos( p, 1, fVeryVerbose );
+//    printf( "Reduced %d outputs to %d outputs.  ", Gia_ManPoNum(p), Vec_PtrSize(vEquivs) );
+//    Abc_PrintTime( 1, "Time", clock() - clk );
+
+    // perform refinement of equivalence classes
+    vEquivs2 = Vec_PtrAlloc( 100 );
+    Vec_PtrForEachEntry( Vec_Int_t *, vEquivs, vLevel, i )
+    {
+        if ( Vec_IntSize(vLevel) < 2 )
+        {
+            Vec_PtrPush( vEquivs2, Vec_IntDup(vLevel) );
+            continue;
+        }
+        sStart = Vec_PtrSize( vEquivs2 );
+        vStrings = Vec_PtrAlloc( 100 );
+        Vec_IntForEachEntry( vLevel, Entry, k )
+        {
+            vStr = Gia_ManIsoFindString( p, Entry, 0 );
+            // check if this string already exists
+            Vec_PtrForEachEntry( Vec_Str_t *, vStrings, vStr2, s )
+                if ( Vec_StrCompareVec(vStr, vStr2) == 0 )
+                    break;
+            if ( s == Vec_PtrSize(vStrings) )
+            {
+                Vec_PtrPush( vStrings, vStr );
+                Vec_PtrPush( vEquivs2, Vec_IntAlloc(8) );
+            }
+            else
+                Vec_StrFree( vStr );
+            // add this entry to the corresponding level
+            vLevel2 = (Vec_Int_t *)Vec_PtrEntry( vEquivs2, sStart + s );
+            Vec_IntPush( vLevel2, Entry );
+        }
+        Vec_VecFree( (Vec_Vec_t *)vStrings );
+    }
+    Vec_VecSortByFirstInt( (Vec_Vec_t *)vEquivs2, 0 );
+    Vec_VecFree( (Vec_Vec_t *)vEquivs );
+    vEquivs = vEquivs2;
+
     // collect the first ones
     vRemain = Vec_IntAlloc( 100 );
     Vec_PtrForEachEntry( Vec_Int_t *, vEquivs, vLevel, i )
         Vec_IntPush( vRemain, Vec_IntEntry(vLevel, 0) );
+
     // derive the resulting AIG
-    pPart = Gia_ManDupCones( pGia, Vec_IntArray(vRemain), Vec_IntSize(vRemain) );
+    pPart = Gia_ManDupCones( p, Vec_IntArray(vRemain), Vec_IntSize(vRemain) );
     Vec_IntFree( vRemain );
     // report the results
-    printf( "Reduced %d outputs to %d outputs.  ", Gia_ManPoNum(pGia), Gia_ManPoNum(pPart) );
+    printf( "Reduced %d outputs to %d outputs.  ", Gia_ManPoNum(p), Gia_ManPoNum(pPart) );
     Abc_PrintTime( 1, "Time", clock() - clk );
     if ( fVerbose )
     {
@@ -621,17 +1025,17 @@ Gia_Man_t * Gia_ManIsoReduce( Gia_Man_t * pGia, Vec_Ptr_t ** pvPosEquivs, int fV
   SeeAlso     []
 
 ***********************************************************************/
-void Gia_IsoTest( Gia_Man_t * pGia, int fVerbose )
+void Gia_IsoTest( Gia_Man_t * p, int fVerbose )
 {
     Vec_Ptr_t * vEquivs;
     int clk = clock(); 
-    vEquivs = Gia_IsoDeriveEquivPos( pGia, fVerbose );
-    printf( "Reduced %d outputs to %d.  ", Gia_ManPoNum(pGia), Vec_PtrSize(vEquivs) );
+    vEquivs = Gia_IsoDeriveEquivPos( p, 1, fVerbose );
+    printf( "Reduced %d outputs to %d.  ", Gia_ManPoNum(p), Vec_PtrSize(vEquivs) );
     Abc_PrintTime( 1, "Time", clock() - clk );
-    if ( fVerbose && Gia_ManPoNum(pGia) != Vec_PtrSize(vEquivs) )
+    if ( fVerbose && Gia_ManPoNum(p) != Vec_PtrSize(vEquivs) )
     {
         printf( "Nontrivial classes:\n" );
-        Vec_VecPrintInt( (Vec_Vec_t *)vEquivs, 1 );
+//        Vec_VecPrintInt( (Vec_Vec_t *)vEquivs, 1 );
     }
     Vec_VecFree( (Vec_Vec_t *)vEquivs );
 }
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index c9640db0..69d46075 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -21982,11 +21982,19 @@ int Abc_CommandAbc9Write( Abc_Frame_t * pAbc, int argc, char ** argv )
     char * pFileName;
     char ** pArgvNew;
     int c, nArgcNew;
+    int fUnique = 0;
+    int fVerbose = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "uvh" ) ) != EOF )
     {
         switch ( c )
         {
+        case 'u':
+            fUnique ^= 1;
+            break;
+        case 'v':
+            fVerbose ^= 1;
+            break;
         case 'h':
             goto usage;
         default:
@@ -22004,16 +22012,24 @@ int Abc_CommandAbc9Write( Abc_Frame_t * pAbc, int argc, char ** argv )
     {
         Abc_Print( -1, "Abc_CommandAbc9Write(): There is no AIG to write.\n" );
         return 1;
-    } 
-    // create the design to write
+    }
     pFileName = argv[globalUtilOptind];
-    Gia_WriteAiger( pAbc->pGia, pFileName, 0, 0 );
+    if ( fUnique )
+    {
+        Gia_Man_t * pGia = Gia_ManIsoCanonicize( pAbc->pGia, fVerbose );
+        Gia_WriteAigerSimple( pGia, pFileName );
+        Gia_ManStop( pGia );
+    }
+    else
+        Gia_WriteAiger( pAbc->pGia, pFileName, 0, 0 );
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &w [-h] <file>\n" );
-    Abc_Print( -2, "\t        writes the current AIG into the AIGER file\n" );
-    Abc_Print( -2, "\t-h    : print the command usage\n");
+    Abc_Print( -2, "usage: &w [-uvh] <file>\n" );
+    Abc_Print( -2, "\t         writes the current AIG into the AIGER file\n" );
+    Abc_Print( -2, "\t-u     : toggle writing canonical AIG structure [default = %s]\n", fUnique? "yes" : "no" );
+    Abc_Print( -2, "\t-v     : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" );
+    Abc_Print( -2, "\t-h     : print the command usage\n");
     Abc_Print( -2, "\t<file> : the file name\n");
     return 1;
 }
@@ -27839,8 +27855,6 @@ usage:
 ***********************************************************************/
 int Abc_CommandAbc9Iso( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
-    extern Gia_Man_t * Gia_ManIsoReduce( Gia_Man_t * pGia, Vec_Ptr_t ** pvPosEquivs, int fVerbose );
-
     Gia_Man_t * pAig;
     Vec_Ptr_t * vPosEquivs;
     int c, fVerbose = 0;