Faster isomorphism detection (command &iso).

abclib.dsp

@@ -3563,6 +3563,10 @@ SOURCE=.\src\aig\gia\giaIso.c
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\aig\gia\giaIso2.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\aig\gia\giaMan.c
 # End Source File
 # Begin Source File

src/aig/gia/gia.h

@@ -951,7 +951,8 @@ extern void                Gia_ManSetIfParsDefault( void * pIfPars );
 extern Gia_Man_t *         Gia_ManPerformMapping( Gia_Man_t * p, void * pIfPars );
 /*=== 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 fDualOut, int fVerbose, int fVeryVerbose );
+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 );
 /*=== giaLogic.c ===========================================================*/
 extern void                Gia_ManTestDistance( Gia_Man_t * p );
 extern void                Gia_ManSolveProblem( Gia_Man_t * pGia, Emb_Par_t * pPars );

src/aig/gia/giaDfs.c

@@ -431,6 +431,76 @@ Vec_Int_t * Gia_ManOrderReverse( Gia_Man_t * p )
     return vResult;
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_ManCollectSeq_rec( Gia_Man_t * p, int Id, Vec_Int_t * vRoots, Vec_Int_t * vObjs )
+{
+    Gia_Obj_t * pObj;
+    if ( Gia_ObjIsTravIdCurrentId( p, Id ) )
+        return;
+    Gia_ObjSetTravIdCurrentId( p, Id );
+    pObj = Gia_ManObj( p, Id );
+    if ( Gia_ObjIsAnd(pObj) )
+    {
+        Gia_ManCollectSeq_rec( p, Gia_ObjFaninId0(pObj, Id), vRoots, vObjs );
+        Gia_ManCollectSeq_rec( p, Gia_ObjFaninId1(pObj, Id), vRoots, vObjs );
+    }
+    else if ( Gia_ObjIsCi(pObj) )
+    {
+        if ( Gia_ObjIsRo(p, pObj) )
+            Vec_IntPush( vRoots, Gia_ObjId(p, Gia_ObjRoToRi(p, pObj)) );
+    }
+    else if ( Gia_ObjIsCo(pObj) )
+        Gia_ManCollectSeq_rec( p, Gia_ObjFaninId0(pObj, Id), vRoots, vObjs );
+    else assert( 0 );
+    Vec_IntPush( vObjs, Id );
+}
+Vec_Int_t * Gia_ManCollectSeq( Gia_Man_t * p, int * pPos, int nPos )
+{
+    Vec_Int_t * vObjs, * vRoots;
+    int i, iRoot;
+    // collect roots
+    vRoots = Vec_IntAlloc( 100 );
+    for ( i = 0; i < nPos; i++ )
+        Vec_IntPush( vRoots, Gia_ObjId(p, Gia_ManPo(p, pPos[i])) );
+    // start trav IDs
+    Gia_ManIncrementTravId( p );
+    Gia_ObjSetTravIdCurrentId( p, 0 );
+    // collect objects
+    vObjs = Vec_IntAlloc( 1000 );
+    Vec_IntPush( vObjs, 0 );
+    Vec_IntForEachEntry( vRoots, iRoot, i )
+        Gia_ManCollectSeq_rec( p, iRoot, vRoots, vObjs );
+    Vec_IntFree( vRoots );
+    return vObjs;
+}
+void Gia_ManCollectSeqTest( Gia_Man_t * p )
+{
+    Vec_Int_t * vObjs;
+    int i;
+    clock_t clk = clock();
+    for ( i = 0; i < Gia_ManPoNum(p); i++ )
+    {
+        if ( i % 10000 == 0 )
+            printf( "%8d finished...\r", i );
+
+        vObjs = Gia_ManCollectSeq( p, &i, 1 );
+//        printf( "%d ", Vec_IntSize(vObjs) );
+        Vec_IntFree( vObjs );
+    }
+    Abc_PrintTime( 1, "Time", clock() - clk );
+
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////

src/aig/gia/giaIso.c

@@ -182,7 +182,8 @@ void Gia_IsoPrint( Gia_IsoMan_t * p, int Iter, clock_t Time )
 {
     printf( "Iter %4d :  ", Iter );
     printf( "Entries =%8d.  ", p->nEntries );
-    printf( "Classes =%8d.  ", Vec_IntSize(p->vClasses)/2 );
+//    printf( "Classes =%8d.  ", Vec_IntSize(p->vClasses)/2 );
+    printf( "Uniques =%8d.  ", p->nUniques );
     printf( "Singles =%8d.  ", p->nSingles );
     printf( "%9.2f sec", (float)(Time)/(float)(CLOCKS_PER_SEC) );
     printf( "\n" );
@@ -1080,13 +1081,40 @@ Vec_Str_t * Gia_ManIsoFindString( Gia_Man_t * p, int iPo, int fVerbose, Vec_Int_
   SeeAlso     []
 
 ***********************************************************************/
-Gia_Man_t * Gia_ManIsoReduce( Gia_Man_t * pInit, Vec_Ptr_t ** pvPosEquivs, Vec_Ptr_t ** pvPiPerms, int fDualOut, int fVerbose, int fVeryVerbose )
+int Vec_IntCountNonTrivial( Vec_Ptr_t * vEquivs, int * pnUsed )
+{
+    Vec_Int_t * vClass;
+    int i, nClasses = 0;
+    *pnUsed = 0;
+    Vec_PtrForEachEntry( Vec_Int_t *, vEquivs, vClass, i )
+    {
+        if ( Vec_IntSize(vClass) < 2 )
+            continue;
+        nClasses++;
+        (*pnUsed) += Vec_IntSize(vClass);
+    }
+    return nClasses;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Gia_Man_t * Gia_ManIsoReduce( Gia_Man_t * pInit, Vec_Ptr_t ** pvPosEquivs, Vec_Ptr_t ** pvPiPerms, int fEstimate, int fDualOut, int fVerbose, int fVeryVerbose )
 { 
     Gia_Man_t * p, * pPart;
     Vec_Ptr_t * vEquivs, * vEquivs2, * vStrings;
     Vec_Int_t * vRemain, * vLevel, * vLevel2;
     Vec_Str_t * vStr, * vStr2;
     int i, k, s, sStart, iPo, Counter;
+    int nClasses, nUsedPos;
     clock_t clk = clock();
     if ( pvPosEquivs )
         *pvPosEquivs = NULL;
@@ -1117,8 +1145,15 @@ Gia_Man_t * Gia_ManIsoReduce( Gia_Man_t * pInit, Vec_Ptr_t ** pvPosEquivs, Vec_P
             Gia_ManStop( p );
         return NULL;
     }
-    printf( "Reduced %d outputs to %d candidate classes.  ", Gia_ManPoNum(p), Vec_PtrSize(vEquivs) );
+    nClasses = Vec_IntCountNonTrivial( vEquivs, &nUsedPos );
+    printf( "Reduced %d outputs to %d candidate   classes (%d outputs are in %d non-trivial classes).  ", 
+        Gia_ManPoNum(p), Vec_PtrSize(vEquivs), nUsedPos, nClasses );
     Abc_PrintTime( 1, "Time", clock() - clk );
+    if ( fEstimate )
+    {
+        Vec_VecFree( (Vec_Vec_t *)vEquivs );
+        return Gia_ManDup(pInit);
+    }
 
     // perform refinement of equivalence classes
     Counter = 0;
@@ -1170,6 +1205,8 @@ Gia_Man_t * Gia_ManIsoReduce( Gia_Man_t * pInit, Vec_Ptr_t ** pvPosEquivs, Vec_P
             vLevel2 = (Vec_Int_t *)Vec_PtrEntry( vEquivs2, sStart + s );
             Vec_IntPush( vLevel2, iPo );
         }
+//        if ( Vec_PtrSize(vEquivs2) - sStart > 1 )
+//            printf( "Refined class %d into %d classes.\n", i, Vec_PtrSize(vEquivs2) - sStart );
         Vec_VecFree( (Vec_Vec_t *)vStrings );
     }
     assert( Counter == Gia_ManPoNum(p) );
@@ -1204,8 +1241,10 @@ Gia_Man_t * Gia_ManIsoReduce( Gia_Man_t * pInit, Vec_Ptr_t ** pvPosEquivs, Vec_P
     pPart = Gia_ManDupCones( p, Vec_IntArray(vRemain), Vec_IntSize(vRemain), 0 );
     Vec_IntFree( vRemain );
     // report the results
+    nClasses = Vec_IntCountNonTrivial( vEquivs, &nUsedPos );
     if ( !fDualOut )
-        printf( "Reduced %d outputs to %d outputs.  ", Gia_ManPoNum(p), Gia_ManPoNum(pPart) );
+        printf( "Reduced %d outputs to %d equivalence classes (%d outputs are in %d non-trivial classes).  ", 
+            Gia_ManPoNum(p), Vec_PtrSize(vEquivs), nUsedPos, nClasses );
     else
         printf( "Reduced %d dual outputs to %d dual outputs.  ", Gia_ManPoNum(p)/2, Gia_ManPoNum(pPart)/2 );
     Abc_PrintTime( 1, "Time", clock() - clk );
@@ -1292,7 +1331,7 @@ void Gia_IsoTest( Gia_Man_t * p, Abc_Cex_t * pCex, int fVerbose )
 //Gia_AigerWrite( pDouble, "test.aig", 0, 0 );
 
     // analyze the two-output miter
-    pAig = Gia_ManIsoReduce( pDouble, &vPosEquivs, &vPisPerm, 0, 0, 0 );
+    pAig = Gia_ManIsoReduce( pDouble, &vPosEquivs, &vPisPerm, 0, 0, 0, 0 );
     Vec_VecFree( (Vec_Vec_t *)vPosEquivs );
 
     // given CEX for output 0, derive CEX for output 1

src/aig/gia/module.make

@@ -25,6 +25,7 @@ SRC +=    src/aig/gia/giaAig.c \
     src/aig/gia/giaHash.c \
     src/aig/gia/giaIf.c \
     src/aig/gia/giaIso.c \
+    src/aig/gia/giaIso2.c \
     src/aig/gia/giaMan.c \
     src/aig/gia/giaMem.c \
     src/aig/gia/giaPat.c \

src/base/abci/abc.c

@@ -29808,12 +29808,18 @@ 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, fDualOut = 0, fVerbose = 0, fVeryVerbose = 0;
+    int c, fNewAlgo = 1, fEstimate = 0, fDualOut = 0, fVerbose = 0, fVeryVerbose = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "dvwh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "nedvwh" ) ) != EOF )
     {
         switch ( c )
         {
+        case 'n':
+            fNewAlgo ^= 1;
+            break;
+        case 'e':
+            fEstimate ^= 1;
+            break;
         case 'd':
             fDualOut ^= 1;
             break;
@@ -29839,8 +29845,11 @@ int Abc_CommandAbc9Iso( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_Print( -1, "Abc_CommandAbc9Iso(): The AIG has only one PO. Isomorphism detection is not performed.\n" );
         return 1;
     }
-    pAig = Gia_ManIsoReduce( pAbc->pGia, &vPosEquivs, NULL, fDualOut, fVerbose, fVeryVerbose );
-//    pAig = Gia_ManIsoReduce( pAbc->pGia, &vPosEquivs, &vPiPerms, fDualOut, fVerbose, fVeryVerbose );
+    if ( fNewAlgo )
+        pAig = Gia_ManIsoReduce2( pAbc->pGia, &vPosEquivs, NULL, fEstimate, 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 );
 //    Vec_VecFree( (Vec_Vec_t *)vPiPerms );
     if ( pAig == NULL )
     {
@@ -29854,9 +29863,11 @@ int Abc_CommandAbc9Iso( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &iso [-dvwh]\n" );
+    Abc_Print( -2, "usage: &iso [-nedvwh]\n" );
     Abc_Print( -2, "\t         removes POs with isomorphic sequential COI\n" );
-    Abc_Print( -2, "\t-d     : treat the current AIG as a dual-output miter [default = %s]\n", fDualOut? "yes": "no" );
+    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-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" );
     Abc_Print( -2, "\t-h     : print the command usage\n");
@@ -31556,7 +31567,8 @@ int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv )
 //    extern void Mig_ManTest( Gia_Man_t * pGia );
 //    extern int Gia_ManVerify( Gia_Man_t * pGia );
 //    extern Gia_Man_t * Gia_SweeperFraigTest( Gia_Man_t * p, int nWords, int nConfs, int fVerbose );
-    extern Gia_Man_t * Gia_ManOptimizeRing( Gia_Man_t * p );
+//    extern Gia_Man_t * Gia_ManOptimizeRing( Gia_Man_t * p );
+//    extern void Gia_ManCollectSeqTest( Gia_Man_t * p );
 
     Extra_UtilGetoptReset();
     while ( ( c = Extra_UtilGetopt( argc, argv, "svh" ) ) != EOF )
@@ -31609,8 +31621,9 @@ int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv )
 //    Mig_ManTest( pAbc->pGia );
 //    Gia_ManVerifyWithBoxes( pAbc->pGia );
 //    pTemp = Gia_SweeperFraigTest( pAbc->pGia, 4, 1000, 0 );
-    pTemp = Gia_ManOptimizeRing( pAbc->pGia );
-    Abc_FrameUpdateGia( pAbc, pTemp );
+//    pTemp = Gia_ManOptimizeRing( pAbc->pGia );
+//    Abc_FrameUpdateGia( pAbc, pTemp );
+//    Gia_ManCollectSeqTest( pAbc->pGia );
     return 0;
 usage:
     Abc_Print( -2, "usage: &test [-svh]\n" );

src/misc/vec/vecWec.h

@@ -458,7 +458,7 @@ static inline void Vec_WecPrint( Vec_Wec_t * p, int fSkipSingles )
     Vec_WecForEachLevel( p, vVec, i )
     {
         if ( fSkipSingles && Vec_IntSize(vVec) == 1 )
-            break;
+            continue;
         printf( " %4d : {", i );
         Vec_IntForEachEntry( vVec, Entry, k )
             printf( " %d", Entry );
@@ -466,6 +466,97 @@ static inline void Vec_WecPrint( Vec_Wec_t * p, int fSkipSingles )
     }
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Derives the set of equivalence classes.]
+
+  Description []
+  
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline Vec_Wec_t * Vec_WecCreateClasses( Vec_Int_t * vMap )
+{
+    Vec_Wec_t * vClasses;
+    int i, Entry;
+    vClasses = Vec_WecStart( Vec_IntFindMax(vMap) + 1 );
+    Vec_IntForEachEntry( vMap, Entry, i )
+        Vec_WecPush( vClasses, Entry, i );
+    return vClasses;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Vec_WecCountNonTrivial( Vec_Wec_t * p, int * pnUsed )
+{
+    Vec_Int_t * vClass;
+    int i, nClasses = 0;
+    *pnUsed = 0;
+    Vec_WecForEachLevel( p, vClass, i )
+    {
+        if ( Vec_IntSize(vClass) < 2 )
+            continue;
+        nClasses++;
+        (*pnUsed) += Vec_IntSize(vClass);
+    }
+    return nClasses;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline Vec_Int_t * Vec_WecCollectFirsts( Vec_Wec_t * p )
+{
+    Vec_Int_t * vFirsts, * vLevel;
+    int i;
+    vFirsts = Vec_IntAlloc( Vec_WecSize(p) );
+    Vec_WecForEachLevel( p, vLevel, i )
+        if ( Vec_IntSize(vLevel) > 0 )
+            Vec_IntPush( vFirsts, Vec_IntEntry(vLevel, 0) );
+    return vFirsts;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline Vec_Ptr_t * Vec_WecConvertToVecPtr( Vec_Wec_t * p )
+{
+    Vec_Ptr_t * vCopy;
+    Vec_Int_t * vLevel;
+    int i;
+    vCopy = Vec_PtrAlloc( Vec_WecSize(p) );
+    Vec_WecForEachLevel( p, vLevel, i )
+        Vec_PtrPush( vCopy, Vec_IntDup(vLevel) );
+    return vCopy;
+}
+
 ABC_NAMESPACE_HEADER_END
 
 #endif