Isomorphism checking code.

src/aig/gia/giaDup.c

@@ -1762,7 +1762,7 @@ void Gia_ManDupCones_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Ptr_t * vLeaves,
         Gia_ManDupCones_rec( p, Gia_ObjFanin1(pObj), vLeaves, vNodes, vRoots );
         Vec_PtrPush( vNodes, pObj );
     }
-    else if ( Gia_ObjIsPo(p, pObj) )
+    else if ( Gia_ObjIsCo(pObj) )
         Gia_ManDupCones_rec( p, Gia_ObjFanin0(pObj), vLeaves, vNodes, vRoots );
     else if ( Gia_ObjIsRo(p, pObj) )
         Vec_PtrPush( vRoots, Gia_ObjRoToRi(p, pObj) );

src/aig/gia/giaIso.c

@@ -458,11 +458,68 @@ void Gia_IsoSort( Gia_IsoMan_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-void Gia_IsoTest( Gia_Man_t * pGia )
+Vec_Ptr_t * Gia_IsoCollectCos( Gia_IsoMan_t * p, int fVerbose )
 {
-    int fVerbose = 1;
-    int nIterMax = 50;
+    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 )
+        if ( p->pUniques[Gia_ObjId(p->pGia, pObj)] > 0 )
+        {
+            vLevel = Vec_IntAlloc( 1 );
+            Vec_IntPush( vLevel, i );
+            Vec_PtrPush( vGroups, vLevel );
+        }
+
+    // add groups
+    Vec_IntForEachEntryDouble( p->vClasses, iBegin, nSize, i )
+    {
+        for ( k = 0; k < nSize; k++ )
+        {
+            pObj = Gia_ManObj( p->pGia, Gia_IsoGetItem(p,iBegin+k) );
+            if ( Gia_ObjIsPo(p->pGia, pObj) )
+                break;
+        }
+        if ( k == nSize )
+            continue;
+        vLevel = Vec_IntAlloc( 8 );
+        for ( k = 0; k < nSize; k++ )
+        {
+            pObj = Gia_ManObj( p->pGia, Gia_IsoGetItem(p,iBegin+k) );
+            if ( Gia_ObjIsPo(p->pGia, pObj) )
+                Vec_IntPush( vLevel, Gia_ObjCioId(pObj) );
+        }
+        Vec_PtrPush( vGroups, vLevel );
+    }
+    // canonicize order
+    Vec_PtrForEachEntry( Vec_Int_t *, vGroups, vLevel, i )
+        Vec_IntSort( vLevel, 0 );
+    Vec_VecSortByFirstInt( (Vec_Vec_t *)vGroups, 0 );
+//    Vec_VecFree( (Vec_Vec_t *)vGroups );
+//    return NULL;
+    return vGroups;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Gia_IsoDeriveEquivPos( Gia_Man_t * pGia, int fVerbose )
+{
+    Vec_Ptr_t * vEquivs;
     Gia_IsoMan_t * p;
+    int nIterMax = 1000;
     int i, clk = clock(), clkTotal = clock();
 
     Gia_ManCleanValue( pGia );
@@ -470,8 +527,8 @@ void Gia_IsoTest( Gia_Man_t * 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; i < nIterMax; i++ )
     {
@@ -484,11 +541,11 @@ void Gia_IsoTest( Gia_Man_t * pGia )
         p->timeRefine += clock() - clk;
 
 //        Gia_IsoPrintClasses( p );
+        if ( fVerbose )
             Gia_IsoPrint( p, i+1, clock() - clkTotal );
         if ( p->nSingles == 0 )
             break;
     }
-
     if ( fVerbose )
     {
         p->timeTotal = clock() - clkTotal;
@@ -501,11 +558,81 @@ void Gia_IsoTest( Gia_Man_t * pGia )
         ABC_PRTP( "Other    ", p->timeOther,              p->timeTotal );
         ABC_PRTP( "TOTAL    ", p->timeTotal,              p->timeTotal );
     }
-
+    vEquivs = Gia_IsoCollectCos( p, fVerbose );
     Gia_IsoManStop( p );
+    return vEquivs;
 }
 
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Gia_Man_t * Gia_ManIsoReduce( Gia_Man_t * pGia, Vec_Ptr_t ** pvPosEquivs, int fVerbose )
+{ 
+    Gia_Man_t * pPart;
+    Vec_Ptr_t * vEquivs;
+    Vec_Int_t * vRemain, * vLevel;
+    int i, clk = clock();
+    // create equivalences
+    vEquivs = Gia_IsoDeriveEquivPos( pGia, fVerbose );
+    // 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) );
+    Vec_IntFree( vRemain );
+    // report the results
+    printf( "Reduced %d outputs to %d outputs.  ", Gia_ManPoNum(pGia), Gia_ManPoNum(pPart) );
+    Abc_PrintTime( 1, "Time", clock() - clk );
+    if ( fVerbose )
+    {
+        printf( "Nontrivial classes:\n" );
+        Vec_VecPrintInt( (Vec_Vec_t *)vEquivs, 1 );
+    }
+    if ( pvPosEquivs )
+        *pvPosEquivs = vEquivs;
+    else
+        Vec_VecFree( (Vec_Vec_t *)vEquivs );
+//    Gia_ManStopP( &pPart );
+    return pPart;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_IsoTest( Gia_Man_t * pGia, 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) );
+    Abc_PrintTime( 1, "Time", clock() - clk );
+    if ( fVerbose )
+    {
+        printf( "Nontrivial classes:\n" );
+        Vec_VecPrintInt( (Vec_Vec_t *)vEquivs, 1 );
+    }
+    Vec_VecFree( (Vec_Vec_t *)vEquivs );
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////

src/aig/saig/saigIso.c

@@ -428,6 +428,7 @@ Aig_Man_t * Iso_ManFilterPos( Aig_Man_t * pAig, Vec_Ptr_t ** pvPosEquivs, int fV
     Vec_Str_t * vStr, * vPrev;
     int i, nPos, nUnique = 0, clk = clock();
     int clkDup = 0, clkAig = 0, clkIso = 0, clk2;
+    *pvPosEquivs = NULL;
 
     // derive AIG for each PO
     nPos = Aig_ManPoNum(pAig) - Aig_ManRegNum(pAig);
@@ -521,13 +522,6 @@ Aig_Man_t * Iso_ManFilterPos( Aig_Man_t * pAig, Vec_Ptr_t ** pvPosEquivs, int fV
 //    return (Vec_Vec_t *)vClasses;
 //    Vec_VecFree( (Vec_Vec_t *)vClasses );
     *pvPosEquivs = vClasses;
-    if ( fVerbose && vClasses )
-    {
-        printf( "Non-trivial equivalence clases of primary outputs:\n" );
-        Vec_VecPrintInt( (Vec_Vec_t *)vClasses, 1 );
-    }
-
-//    printf( "The number of all checks %d.  Complex checks %d.\n", nPos*(nPos-1)/2, s_Counter );
     return pPart;
 }
 
@@ -570,7 +564,12 @@ Aig_Man_t * Saig_ManIsoReduce( Aig_Man_t * pAig, Vec_Ptr_t ** pvPosEquivs, int f
     pPart = Iso_ManFilterPos( pAig, pvPosEquivs, fVerbose );
     printf( "Reduced %d outputs to %d outputs.  ", Saig_ManPoNum(pAig), Saig_ManPoNum(pPart) );
     Abc_PrintTime( 1, "Time", clock() - clk );
-//    Aig_ManStop( pPart );
+    if ( fVerbose && *pvPosEquivs )
+    {
+        printf( "Nontrivial classes:\n" );
+        Vec_VecPrintInt( (Vec_Vec_t *)*pvPosEquivs, 1 );
+    }
+//    Aig_ManStopP( &pPart );
     return pPart;
 }
 

src/base/abci/abc.c

@@ -352,6 +352,7 @@ static int Abc_CommandAbc9ReachP             ( Abc_Frame_t * pAbc, int argc, cha
 static int Abc_CommandAbc9ReachN             ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9ReachY             ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Undo               ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9Iso                ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Test               ( Abc_Frame_t * pAbc, int argc, char ** argv );
 
 static int Abc_CommandAbcTestNew             ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -782,6 +783,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "ABC9",         "&reachn",       Abc_CommandAbc9ReachN,       0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&reachy",       Abc_CommandAbc9ReachY,       0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&undo",         Abc_CommandAbc9Undo,         0 );
+    Cmd_CommandAdd( pAbc, "ABC9",         "&iso",          Abc_CommandAbc9Iso,          0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&test",         Abc_CommandAbc9Test,         0 );
 
     Cmd_CommandAdd( pAbc, "Liveness",     "l2s",           Abc_CommandAbcLivenessToSafety,    0 );
@@ -27835,6 +27837,58 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
+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;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pAbc->pGia == NULL )
+    {
+        Abc_Print( -1, "Abc_CommandAbc9Iso(): There is no AIG.\n" );
+        return 1;
+    }
+    pAig = Gia_ManIsoReduce( pAbc->pGia, &vPosEquivs, fVerbose );
+    // update the internal storage of PO equivalences
+    Abc_FrameReplacePoEquivs( pAbc, &vPosEquivs );
+    // update the AIG
+    Abc_CommandUpdate9( pAbc, pAig );
+    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_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
 //    Gia_Man_t * pTemp = NULL;
@@ -27843,7 +27897,7 @@ int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv )
 //    extern Gia_Man_t * Gia_VtaTest( Gia_Man_t * p );
 //    extern int Gia_ManSuppSizeTest( Gia_Man_t * p );
 //    extern void Gia_VtaTest( Gia_Man_t * p, int nFramesStart, int nFramesMax, int nConfMax, int nTimeMax, int fVerbose );
-    extern void Gia_IsoTest( Gia_Man_t * p );
+    extern void Gia_IsoTest( Gia_Man_t * p, int fVerbose );
 
     Extra_UtilGetoptReset();
     while ( ( c = Extra_UtilGetopt( argc, argv, "svh" ) ) != EOF )
@@ -27882,7 +27936,7 @@ int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv )
 //    Gia_ManSuppSizeTest( pAbc->pGia );
 //    Gia_VtaTest( pAbc->pGia, 10, 100000, 0, 0, 1 );
 
-    Gia_IsoTest( pAbc->pGia );
+    Gia_IsoTest( pAbc->pGia, fVerbose );
     return 0;
 usage:
     Abc_Print( -2, "usage: &test [-svh]\n" );

src/base/abci/abcSweep.c

@@ -177,7 +177,7 @@ void Abc_NtkFraigSweepUsingExdc( Fraig_Man_t * pMan, Abc_Ntk_t * pNtk )
 
 /**Function*************************************************************
 
-  Synopsis    [Collects equivalence classses of node in the network.]
+  Synopsis    [Collects equivalence classes of node in the network.]
 
   Description []
                

src/proof/ssw/sswSemi.c

@@ -6,7 +6,7 @@
 
   PackageName [Inductive prover with constraints.]
 
-  Synopsis    [Semiformal for equivalence clases.]
+  Synopsis    [Semiformal for equivalence classes.]
 
   Author      [Alan Mishchenko]