Bug fix and performance improvement in &iso.

3 files changed, 141 insertions, 66 deletions

diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index 4a41ee9f..fb93e0c2 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -1093,7 +1093,7 @@ extern Gia_Man_t *         Jf_ManPerformMapping( Gia_Man_t * pGia, Jf_Par_t * pP
 /*=== 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, Vec_Ptr_t ** pvPiPerms, int fEstimate, int fDualOut, int fVerbose, int fVeryVerbose );
-extern Gia_Man_t *         Gia_ManIsoReduce2( Gia_Man_t * p, Vec_Ptr_t ** pvPosEquivs, Vec_Ptr_t ** pvPiPerms, int fEstimate, int fDualOut, int fVerbose, int fVeryVerbose );
+extern Gia_Man_t *         Gia_ManIsoReduce2( Gia_Man_t * p, Vec_Ptr_t ** pvPosEquivs, Vec_Ptr_t ** pvPiPerms, int fEstimate, int fBetterQual, int fDualOut, int fVerbose, int fVeryVerbose );
 /*=== 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/giaIso2.c b/src/aig/gia/giaIso2.c
index ef5dbf42..e9d9d883 100644
--- a/src/aig/gia/giaIso2.c
+++ b/src/aig/gia/giaIso2.c
@@ -486,68 +486,87 @@ void Gia_Iso2ManCollectOrder( Gia_Man_t * pGia, int * pPos, int nPos, Vec_Int_t
   SeeAlso     []
 
 ***********************************************************************/
-int Gia_Iso2ManCheckIsoClass( Gia_Man_t * p, Vec_Int_t * vClass, Vec_Int_t * vRoots, Vec_Int_t * vVec0, Vec_Int_t * vVec1, Vec_Int_t * vMap0, Vec_Int_t * vMap1 )
+int Gia_Iso2ManCheckIsoPair( Gia_Man_t * p, Vec_Int_t * vVec0, Vec_Int_t * vVec1, Vec_Int_t * vMap0, Vec_Int_t * vMap1 )
 {
     Gia_Obj_t * pObj0, * pObj1;
-    int i, k, iObj0, iObj1, iPo;
-    assert( Vec_IntSize(vClass) > 1 );
-    iPo = Vec_IntEntry( vClass, 0 );
-    Gia_Iso2ManCollectOrder( p, &iPo, 1, vRoots, vVec0, vMap0 );
-    Vec_IntForEachEntryStart( vClass, iPo, i, 1 )
+    int k, iObj0, iObj1;
+    Vec_IntForEachEntryTwo( vVec0, vVec1, iObj0, iObj1, k )
     {
-        Gia_Iso2ManCollectOrder( p, &iPo, 1, vRoots, vVec1, vMap1 );
-        if ( Vec_IntSize(vVec0) != Vec_IntSize(vVec1) )
+        if ( iObj0 == iObj1 )
+            continue;
+        pObj0 = Gia_ManObj(p, iObj0);
+        pObj1 = Gia_ManObj(p, iObj1);
+        if ( pObj0->Value != pObj1->Value )
+            return 0;
+        assert( pObj0->Value == pObj1->Value );
+        if ( !Gia_ObjIsAnd(pObj0) )
             continue;
-        Vec_IntForEachEntryTwo( vVec0, vVec1, iObj0, iObj1, k )
+        if ( Gia_ObjFanin0(pObj0)->Value <= Gia_ObjFanin1(pObj0)->Value )
+        {
+            if ( Gia_ObjFanin0(pObj1)->Value <= Gia_ObjFanin1(pObj1)->Value )
+            {
+                if ( Gia_ObjFaninC0(pObj0) != Gia_ObjFaninC0(pObj1)  || Gia_ObjFaninC1(pObj0) != Gia_ObjFaninC1(pObj1)   ||
+                     Vec_IntEntry(vMap0, Gia_ObjFaninId0p(p, pObj0)) != Vec_IntEntry( vMap1, Gia_ObjFaninId0p(p, pObj1)) || 
+                     Vec_IntEntry(vMap0, Gia_ObjFaninId1p(p, pObj0)) != Vec_IntEntry( vMap1, Gia_ObjFaninId1p(p, pObj1)) )
+                     return 0;
+            }
+            else
+            {
+                if ( Gia_ObjFaninC0(pObj0) != Gia_ObjFaninC1(pObj1)  || Gia_ObjFaninC1(pObj0) != Gia_ObjFaninC0(pObj1)   ||
+                     Vec_IntEntry(vMap0, Gia_ObjFaninId0p(p, pObj0)) != Vec_IntEntry( vMap1, Gia_ObjFaninId1p(p, pObj1)) || 
+                     Vec_IntEntry(vMap0, Gia_ObjFaninId1p(p, pObj0)) != Vec_IntEntry( vMap1, Gia_ObjFaninId0p(p, pObj1)) )
+                     return 0;
+            }
+        }
+        else
         {
-            if ( iObj0 == iObj1 )
-                continue;
-            pObj0 = Gia_ManObj(p, iObj0);
-            pObj1 = Gia_ManObj(p, iObj1);
-            if ( pObj0->Value != pObj1->Value )
-                return 0;
-            assert( pObj0->Value == pObj1->Value );
-            if ( !Gia_ObjIsAnd(pObj0) )
-                continue;
-            if ( Gia_ObjFanin0(pObj0)->Value <= Gia_ObjFanin1(pObj0)->Value )
+            if ( Gia_ObjFanin0(pObj1)->Value <= Gia_ObjFanin1(pObj1)->Value )
             {
-                if ( Gia_ObjFanin0(pObj1)->Value <= Gia_ObjFanin1(pObj1)->Value )
-                {
-                    if ( Gia_ObjFaninC0(pObj0) != Gia_ObjFaninC0(pObj1)  || Gia_ObjFaninC1(pObj0) != Gia_ObjFaninC1(pObj1)   ||
-                         Vec_IntEntry(vMap0, Gia_ObjFaninId0p(p, pObj0)) != Vec_IntEntry( vMap1, Gia_ObjFaninId0p(p, pObj1)) || 
-                         Vec_IntEntry(vMap0, Gia_ObjFaninId1p(p, pObj0)) != Vec_IntEntry( vMap1, Gia_ObjFaninId1p(p, pObj1)) )
-                         return 0;
-                }
-                else
-                {
-                    if ( Gia_ObjFaninC0(pObj0) != Gia_ObjFaninC1(pObj1)  || Gia_ObjFaninC1(pObj0) != Gia_ObjFaninC0(pObj1)   ||
-                         Vec_IntEntry(vMap0, Gia_ObjFaninId0p(p, pObj0)) != Vec_IntEntry( vMap1, Gia_ObjFaninId1p(p, pObj1)) || 
-                         Vec_IntEntry(vMap0, Gia_ObjFaninId1p(p, pObj0)) != Vec_IntEntry( vMap1, Gia_ObjFaninId0p(p, pObj1)) )
-                         return 0;
-                }
+                if ( Gia_ObjFaninC1(pObj0) != Gia_ObjFaninC0(pObj1)  || Gia_ObjFaninC0(pObj0) != Gia_ObjFaninC1(pObj1)   ||
+                     Vec_IntEntry(vMap0, Gia_ObjFaninId1p(p, pObj0)) != Vec_IntEntry( vMap1, Gia_ObjFaninId0p(p, pObj1)) || 
+                     Vec_IntEntry(vMap0, Gia_ObjFaninId0p(p, pObj0)) != Vec_IntEntry( vMap1, Gia_ObjFaninId1p(p, pObj1)) )
+                     return 0;
             }
             else
             {
-                if ( Gia_ObjFanin0(pObj1)->Value <= Gia_ObjFanin1(pObj1)->Value )
-                {
-                    if ( Gia_ObjFaninC1(pObj0) != Gia_ObjFaninC0(pObj1)  || Gia_ObjFaninC0(pObj0) != Gia_ObjFaninC1(pObj1)   ||
-                         Vec_IntEntry(vMap0, Gia_ObjFaninId1p(p, pObj0)) != Vec_IntEntry( vMap1, Gia_ObjFaninId0p(p, pObj1)) || 
-                         Vec_IntEntry(vMap0, Gia_ObjFaninId0p(p, pObj0)) != Vec_IntEntry( vMap1, Gia_ObjFaninId1p(p, pObj1)) )
-                         return 0;
-                }
-                else
-                {
-                    if ( Gia_ObjFaninC1(pObj0) != Gia_ObjFaninC1(pObj1)  || Gia_ObjFaninC0(pObj0) != Gia_ObjFaninC0(pObj1)   ||
-                         Vec_IntEntry(vMap0, Gia_ObjFaninId1p(p, pObj0)) != Vec_IntEntry( vMap1, Gia_ObjFaninId1p(p, pObj1)) || 
-                         Vec_IntEntry(vMap0, Gia_ObjFaninId0p(p, pObj0)) != Vec_IntEntry( vMap1, Gia_ObjFaninId0p(p, pObj1)) )
-                         return 0;
-                }
+                if ( Gia_ObjFaninC1(pObj0) != Gia_ObjFaninC1(pObj1)  || Gia_ObjFaninC0(pObj0) != Gia_ObjFaninC0(pObj1)   ||
+                     Vec_IntEntry(vMap0, Gia_ObjFaninId1p(p, pObj0)) != Vec_IntEntry( vMap1, Gia_ObjFaninId1p(p, pObj1)) || 
+                     Vec_IntEntry(vMap0, Gia_ObjFaninId0p(p, pObj0)) != Vec_IntEntry( vMap1, Gia_ObjFaninId0p(p, pObj1)) )
+                     return 0;
             }
         }
     }
     return 1;
 } 
-Vec_Wec_t * Gia_Iso2ManCheckIsoClasses( Gia_Man_t * p, Vec_Wec_t * vEquivs )
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Gia_Iso2ManCheckIsoClassOneSkip( Gia_Man_t * p, Vec_Int_t * vClass, Vec_Int_t * vRoots, Vec_Int_t * vVec0, Vec_Int_t * vVec1, Vec_Int_t * vMap0, Vec_Int_t * vMap1 )
+{
+    int i, iPo;
+    assert( Vec_IntSize(vClass) > 1 );
+    iPo = Vec_IntEntry( vClass, 0 );
+    Gia_Iso2ManCollectOrder( p, &iPo, 1, vRoots, vVec0, vMap0 );
+    Vec_IntForEachEntryStart( vClass, iPo, i, 1 )
+    {
+        Gia_Iso2ManCollectOrder( p, &iPo, 1, vRoots, vVec1, vMap1 );
+        if ( Vec_IntSize(vVec0) != Vec_IntSize(vVec1) )
+            return 0;
+        if ( !Gia_Iso2ManCheckIsoPair( p, vVec0, vVec1, vMap0, vMap1 ) )
+            return 0;
+    }
+    return 1;
+} 
+Vec_Wec_t * Gia_Iso2ManCheckIsoClassesSkip( Gia_Man_t * p, Vec_Wec_t * vEquivs )
 {
     Vec_Wec_t * vEquivs2;
     Vec_Int_t * vRoots = Vec_IntAlloc( 10000 );
@@ -562,16 +581,7 @@ Vec_Wec_t * Gia_Iso2ManCheckIsoClasses( Gia_Man_t * p, Vec_Wec_t * vEquivs )
     {
         if ( i % 100 == 0 )
             printf( "%8d finished...\r", i );
-/*
-        if ( i == 17 )
-        {
-            Gia_Man_t * pCone;
-            pCone = Gia_ManDupCones( p, Vec_IntArray(vClass), 2, 1 );
-            Gia_AigerWrite( pCone, "dump.aig", 0, 0 );
-            Gia_ManStop( pCone );
-        }
-*/
-        if ( Vec_IntSize(vClass) < 2 || Gia_Iso2ManCheckIsoClass(p, vClass, vRoots, vVec0, vVec1, vMap0, vMap1) )
+        if ( Vec_IntSize(vClass) < 2 || Gia_Iso2ManCheckIsoClassOneSkip(p, vClass, vRoots, vVec0, vVec1, vMap0, vMap1) )
         {
             vClass2 = Vec_WecPushLevel( vEquivs2 );
             *vClass2 = *vClass;
@@ -580,7 +590,6 @@ Vec_Wec_t * Gia_Iso2ManCheckIsoClasses( Gia_Man_t * p, Vec_Wec_t * vEquivs )
         }
         else
         {
-//            printf( "Class %d failed.\n", i );
             Vec_IntForEachEntry( vClass, Entry, k )
             {
                 vClass2 = Vec_WecPushLevel( vEquivs2 );
@@ -596,6 +605,65 @@ Vec_Wec_t * Gia_Iso2ManCheckIsoClasses( Gia_Man_t * p, Vec_Wec_t * vEquivs )
     return vEquivs2;
 }
 
+void Gia_Iso2ManCheckIsoClassOne( Gia_Man_t * p, Vec_Int_t * vClass, Vec_Int_t * vRoots, Vec_Int_t * vVec0, Vec_Int_t * vVec1, Vec_Int_t * vMap0, Vec_Int_t * vMap1, Vec_Int_t * vNewClass )
+{
+    int i, k = 1, iPo;
+    Vec_IntClear( vNewClass );
+    if ( Vec_IntSize(vClass) <= 1 )
+        return;
+    assert( Vec_IntSize(vClass) > 1 );
+    iPo = Vec_IntEntry( vClass, 0 );
+    Gia_Iso2ManCollectOrder( p, &iPo, 1, vRoots, vVec0, vMap0 );
+    Vec_IntForEachEntryStart( vClass, iPo, i, 1 )
+    {
+        Gia_Iso2ManCollectOrder( p, &iPo, 1, vRoots, vVec1, vMap1 );
+        if ( Vec_IntSize(vVec0) == Vec_IntSize(vVec1) && Gia_Iso2ManCheckIsoPair(p, vVec0, vVec1, vMap0, vMap1) )
+            Vec_IntWriteEntry( vClass, k++, iPo );
+        else
+            Vec_IntPush( vNewClass, iPo );
+    }
+    Vec_IntShrink( vClass, k );
+} 
+Vec_Wec_t * Gia_Iso2ManCheckIsoClasses( Gia_Man_t * p, Vec_Wec_t * vEquivs )
+{
+    Vec_Wec_t * vEquivs2;
+    Vec_Int_t * vRoots = Vec_IntAlloc( 10000 );
+    Vec_Int_t * vVec0 = Vec_IntAlloc( 10000 );
+    Vec_Int_t * vVec1 = Vec_IntAlloc( 10000 );
+    Vec_Int_t * vMap0 = Vec_IntStart( Gia_ManObjNum(p) );
+    Vec_Int_t * vMap1 = Vec_IntStart( Gia_ManObjNum(p) );
+    Vec_Int_t * vClass, * vClass2, * vNewClass;
+    int i;
+    vNewClass = Vec_IntAlloc( 100 );
+    vEquivs2 = Vec_WecAlloc( 2 * Vec_WecSize(vEquivs) );
+    Vec_WecForEachLevel( vEquivs, vClass, i )
+    {
+        if ( i % 100 == 0 )
+            printf( "%8d finished...\r", i );
+        // split this class
+        Gia_Iso2ManCheckIsoClassOne( p, vClass, vRoots, vVec0, vVec1, vMap0, vMap1, vNewClass );
+        assert( Vec_IntSize(vClass) > 0 );
+        // add remaining class
+        vClass2 = Vec_WecPushLevel( vEquivs2 );
+        *vClass2 = *vClass;
+        vClass->pArray = NULL;
+        vClass->nSize = vClass->nCap = 0;
+        // add new class
+        if ( Vec_IntSize(vNewClass) == 0 )
+            continue;
+        vClass = Vec_WecPushLevel( vEquivs );
+        Vec_IntAppend( vClass, vNewClass );
+    }
+    Vec_IntFree( vNewClass );   
+    Vec_IntFree( vRoots );
+    Vec_IntFree( vVec0 );
+    Vec_IntFree( vVec1 );
+    Vec_IntFree( vMap0 );
+    Vec_IntFree( vMap1 );
+    return vEquivs2;
+}
+
+
 
 /**Function*************************************************************
 
@@ -646,7 +714,7 @@ Vec_Wec_t * Gia_Iso2ManPerform( Gia_Man_t * pGia, int fVerbose )
   SeeAlso     []
 
 ***********************************************************************/
-Gia_Man_t * Gia_ManIsoReduce2( Gia_Man_t * pGia, Vec_Ptr_t ** pvPosEquivs, Vec_Ptr_t ** pvPiPerms, int fEstimate, int fDualOut, int fVerbose, int fVeryVerbose )
+Gia_Man_t * Gia_ManIsoReduce2( Gia_Man_t * pGia, Vec_Ptr_t ** pvPosEquivs, Vec_Ptr_t ** pvPiPerms, int fEstimate, int fBetterQual, int fDualOut, int fVerbose, int fVeryVerbose )
 {
     Gia_Man_t * pPart;
     Vec_Wec_t * vEquivs, * vEquivs2;
@@ -665,7 +733,10 @@ Gia_Man_t * Gia_ManIsoReduce2( Gia_Man_t * pGia, Vec_Ptr_t ** pvPosEquivs, Vec_P
         return Gia_ManDup(pGia);
     }
     // verify classes
-    vEquivs2 = Gia_Iso2ManCheckIsoClasses( pGia, vEquivs );
+    if ( fBetterQual )
+        vEquivs2 = Gia_Iso2ManCheckIsoClasses( pGia, vEquivs );
+    else
+        vEquivs2 = Gia_Iso2ManCheckIsoClassesSkip( pGia, vEquivs );
     Vec_WecFree( vEquivs );
     vEquivs = vEquivs2;
     // sort equiv classes by the first integer
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 50c29b88..c9633158 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -31542,9 +31542,9 @@ int Abc_CommandAbc9Iso( Abc_Frame_t * pAbc, int argc, char ** argv )
     Gia_Man_t * pAig;
     Vec_Ptr_t * vPosEquivs;
 //    Vec_Ptr_t * vPiPerms;
-    int c, fNewAlgo = 1, fEstimate = 0, fDualOut = 0, fVerbose = 0, fVeryVerbose = 0;
+    int c, fNewAlgo = 1, fEstimate = 0, fBetterQual = 0, fDualOut = 0, fVerbose = 0, fVeryVerbose = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "nedvwh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "neqdvwh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -31554,6 +31554,9 @@ int Abc_CommandAbc9Iso( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'e':
             fEstimate ^= 1;
             break;
+        case 'q':
+            fBetterQual ^= 1;
+            break;
         case 'd':
             fDualOut ^= 1;
             break;
@@ -31580,7 +31583,7 @@ int Abc_CommandAbc9Iso( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
     if ( fNewAlgo )
-        pAig = Gia_ManIsoReduce2( pAbc->pGia, &vPosEquivs, NULL, fEstimate, fDualOut, fVerbose, fVeryVerbose );
+        pAig = Gia_ManIsoReduce2( pAbc->pGia, &vPosEquivs, NULL, fEstimate, fBetterQual, fDualOut, fVerbose, fVeryVerbose );
     else
         pAig = Gia_ManIsoReduce( pAbc->pGia, &vPosEquivs, NULL, fEstimate, fDualOut, fVerbose, fVeryVerbose );
 //    pAig = Gia_ManIsoReduce( pAbc->pGia, &vPosEquivs, &vPiPerms, 0, fDualOut, fVerbose, fVeryVerbose );
@@ -31597,10 +31600,11 @@ int Abc_CommandAbc9Iso( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &iso [-nedvwh]\n" );
+    Abc_Print( -2, "usage: &iso [-neqdvwh]\n" );
     Abc_Print( -2, "\t         removes POs with isomorphic sequential COI\n" );
     Abc_Print( -2, "\t-n     : toggle using new fast algorithm [default = %s]\n", fNewAlgo? "yes": "no" );
     Abc_Print( -2, "\t-e     : toggle computing lower bound on equivalence classes [default = %s]\n", fEstimate? "yes": "no" );
+    Abc_Print( -2, "\t-q     : toggle improving quality at the expense of runtime [default = %s]\n", fBetterQual? "yes": "no" );
     Abc_Print( -2, "\t-d     : toggle treating the current AIG as a dual-output miter [default = %s]\n", fDualOut? "yes": "no" );
     Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-w     : toggle printing very verbose information [default = %s]\n", fVeryVerbose? "yes": "no" );