Graph isomorphism checking code.

src/aig/aig/aig.h

@@ -163,6 +163,7 @@ struct Aig_Man_t_
     Vec_Vec_t *      vClockDoms; 
     Vec_Int_t *      vProbs;         // probability of node being 1 
     Vec_Int_t *      vCiNumsOrig;    // original CI names
+    int              nComplEdges;    // complemented edges
     // timing statistics
     int              time1;
     int              time2;

src/aig/aig/aigIso.c

@@ -92,6 +92,8 @@ 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) )
         {
@@ -100,7 +102,7 @@ int Iso_ManNegEdgeNum( Aig_Man_t * pAig )
         }
         else if ( Aig_ObjIsPo(pObj) )
             Counter += Aig_ObjFaninC0(pObj);
-    return Counter;
+    return (pAig->nComplEdges = Counter);
 }
 
 /**Function*************************************************************
@@ -716,7 +718,7 @@ int Iso_ManCheckMapping( Aig_Man_t * pAig1, Aig_Man_t * pAig2, Vec_Int_t * vMap2
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Int_t * Iso_ManFindMapping( Aig_Man_t * pAig1, Aig_Man_t * pAig2, int fVerbose )
+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;
@@ -732,12 +734,16 @@ Vec_Int_t * Iso_ManFindMapping( Aig_Man_t * pAig1, Aig_Man_t * pAig2, int fVerbo
         return NULL;
     if ( Iso_ManNegEdgeNum(pAig1) != Iso_ManNegEdgeNum(pAig2) )
         return NULL;
-    if ( fVerbose )
+    if ( fVerbose ) 
         printf( "AIG1:\n" );
-    vPerm1 = Iso_ManFindPerm( pAig1, fVerbose );
+    vPerm1 = vPerm1_ ? vPerm1_ : Iso_ManFindPerm( pAig1, fVerbose );
     if ( fVerbose )
         printf( "AIG1:\n" );
-    vPerm2 = Iso_ManFindPerm( pAig2, fVerbose );
+    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 );
@@ -746,8 +752,10 @@ Vec_Int_t * Iso_ManFindMapping( Aig_Man_t * pAig1, Aig_Man_t * pAig2, int fVerbo
         assert( Entry >= 0 && Entry < Aig_ManPiNum(pAig1) );
         Vec_IntWriteEntry( vInvPerm2, i, Vec_IntEntry(vPerm1, Entry) );
     }
-    Vec_IntFree( vPerm1 );
-    Vec_IntFree( vPerm2 );
+    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 );
@@ -772,9 +780,10 @@ void Iso_ManTestOne( Aig_Man_t * pAig, int fVerbose )
     Vec_IntFree( vPerm );
 }
 
-#include "src/base/abc/abc.h"
 
 
+#include "src/aig/saig/saig.h"
+
 /**Function*************************************************************
 
   Synopsis    []
@@ -786,7 +795,91 @@ void Iso_ManTestOne( Aig_Man_t * pAig, int fVerbose )
   SeeAlso     []
 
 ***********************************************************************/
-void Iso_ManTest( Aig_Man_t * pAig1, int fVerbose )
+Aig_Man_t * Iso_ManFilterPos( 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 );
+    }
+
+    // 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 );
+    return pPart;
+}
+
+
+#include "src/base/abc/abc.h"
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Iso_ManTestOld( 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 );
@@ -799,7 +892,7 @@ void Iso_ManTest( Aig_Man_t * pAig1, int fVerbose )
     pAig2 = Abc_NtkToDar( pNtk, 0, 1 );
     Abc_NtkDelete( pNtk );
 
-    vMap = Iso_ManFindMapping( pAig1, pAig2, fVerbose );
+    vMap = Iso_ManFindMapping( pAig1, pAig2, NULL, NULL, fVerbose );
     Aig_ManStop( pAig2 );
 
     if ( vMap != NULL )
@@ -813,6 +906,28 @@ void Iso_ManTest( Aig_Man_t * pAig1, int fVerbose )
     Vec_IntFreeP( &vMap );
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Iso_ManTest( 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;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////

src/aig/saig/saig.h

@@ -174,6 +174,7 @@ extern int               Saig_ManVerifyCex( Aig_Man_t * pAig, Abc_Cex_t * p );
 extern Abc_Cex_t *       Saig_ManExtendCex( Aig_Man_t * pAig, Abc_Cex_t * p );
 extern int               Saig_ManFindFailedPoCex( Aig_Man_t * pAig, Abc_Cex_t * p );
 extern Aig_Man_t *       Saig_ManDupWithPhase( Aig_Man_t * pAig, Vec_Int_t * vInit );
+extern Aig_Man_t *       Saig_ManDupCones( Aig_Man_t * pAig, int * pPos, int nPos );
 /*=== saigHaig.c ==========================================================*/
 extern Aig_Man_t *       Saig_ManHaigRecord( Aig_Man_t * p, int nIters, int nSteps, int fRetimingOnly, int fAddBugs, int fUseCnf, int fVerbose );
 /*=== saigInd.c ==========================================================*/

src/aig/saig/saigDup.c

@@ -446,6 +446,82 @@ Aig_Man_t * Saig_ManDupWithPhase( Aig_Man_t * pAig, Vec_Int_t * vInit )
     return pAigNew;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Copy an AIG structure related to the selected POs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Saig_ManDupCones_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vNodes, Vec_Ptr_t * vRoots )
+{
+    if ( Aig_ObjIsTravIdCurrent(p, pObj) )
+        return;
+    Aig_ObjSetTravIdCurrent(p, pObj);
+    if ( Aig_ObjIsNode(pObj) )
+    {
+        Saig_ManDupCones_rec( p, Aig_ObjFanin0(pObj), vLeaves, vNodes, vRoots );
+        Saig_ManDupCones_rec( p, Aig_ObjFanin1(pObj), vLeaves, vNodes, vRoots );
+        Vec_PtrPush( vNodes, pObj );
+    }
+    else if ( Aig_ObjIsPo(pObj) )
+        Saig_ManDupCones_rec( p, Aig_ObjFanin0(pObj), vLeaves, vNodes, vRoots );
+    else if ( Saig_ObjIsLo(p, pObj) )
+        Vec_PtrPush( vRoots, Saig_ObjLoToLi(p, pObj) );
+    else if ( Saig_ObjIsPi(p, pObj) )
+        Vec_PtrPush( vLeaves, pObj );
+    else assert( 0 );
+}
+Aig_Man_t * Saig_ManDupCones( Aig_Man_t * pAig, int * pPos, int nPos )
+{
+    Aig_Man_t * pAigNew;
+    Vec_Ptr_t * vLeaves, * vNodes, * vRoots;
+    Aig_Obj_t * pObj;
+    int i;
+
+    // collect initial POs
+    vLeaves = Vec_PtrAlloc( 100 );
+    vNodes = Vec_PtrAlloc( 100 );
+    vRoots = Vec_PtrAlloc( 100 );
+    for ( i = 0; i < nPos; i++ )
+        Vec_PtrPush( vRoots, Aig_ManPo(pAig, pPos[i]) );
+
+    // mark internal nodes
+    Aig_ManIncrementTravId( pAig );
+    Aig_ObjSetTravIdCurrent( pAig, Aig_ManConst1(pAig) );
+    Vec_PtrForEachEntry( Aig_Obj_t *, vRoots, pObj, i )
+        Saig_ManDupCones_rec( pAig, pObj, vLeaves, vNodes, vRoots );
+
+    // start the new manager
+    pAigNew = Aig_ManStart( Vec_PtrSize(vNodes) );
+    pAigNew->pName = Abc_UtilStrsav( pAig->pName );
+    // map the constant node
+    Aig_ManConst1(pAig)->pData = Aig_ManConst1( pAigNew );
+    // create PIs
+    Vec_PtrForEachEntry( Aig_Obj_t *, vLeaves, pObj, i )
+        pObj->pData = Aig_ObjCreatePi( pAigNew );
+    // create LOs
+    Vec_PtrForEachEntryStart( Aig_Obj_t *, vRoots, pObj, i, nPos )
+        Saig_ObjLiToLo(pAig, pObj)->pData = Aig_ObjCreatePi( pAigNew );
+    // create internal nodes
+    Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
+        pObj->pData = Aig_And( pAigNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
+    // create COs
+    Vec_PtrForEachEntry( Aig_Obj_t *, vRoots, pObj, i )
+        Aig_ObjCreatePo( pAigNew, Aig_ObjChild0Copy(pObj) );
+    // finalize
+    Aig_ManSetRegNum( pAigNew, Vec_PtrSize(vRoots)-nPos );
+    Vec_PtrFree( vLeaves );
+    Vec_PtrFree( vNodes );
+    Vec_PtrFree( vRoots );
+    return pAigNew;
+
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////

src/base/abci/abc.c

@@ -8837,16 +8837,26 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
     extern void Aig_ManSupportsTest( Aig_Man_t * pMan );
     extern int Aig_SupportSizeTest( Aig_Man_t * pMan );
     extern int Abc_NtkSuppSizeTest( Abc_Ntk_t * p );
-    extern void Iso_ManTest( Aig_Man_t * pAig, int fVerbose );
+    extern Aig_Man_t * Iso_ManTest( Aig_Man_t * pAig, int fVerbose );
+    extern Abc_Ntk_t * Abc_NtkFromAigPhase( Aig_Man_t * pMan );
     if ( pNtk )
     {
         Aig_Man_t * pAig = Abc_NtkToDar( pNtk, 0, 1 );
+        Aig_Man_t * pRes;
+        Abc_Ntk_t * pNtkRes;
 //        Aig_ManInterRepar( pAig, 1 );
 //        Aig_ManInterTest( pAig, 1 );
 //        Aig_ManSupportsTest( pAig );
 //        Aig_SupportSizeTest( pAig );
-        Iso_ManTest( pAig, fVerbose );
+        pRes = Iso_ManTest( pAig, fVerbose );
         Aig_ManStop( pAig );
+
+        pNtkRes = Abc_NtkFromAigPhase( pRes );
+        Aig_ManStop( pRes );
+
+        ABC_FREE( pNtkRes->pName );
+        pNtkRes->pName = Extra_UtilStrsav(pNtk->pName);
+        Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
     }
 }
 

src/misc/vec/vecInt.h

@@ -926,6 +926,8 @@ static inline Vec_Int_t * Vec_IntInvert( Vec_Int_t * p, int Fill )
 {
     int Entry, i;
     Vec_Int_t * vRes = Vec_IntAlloc( 0 );
+    if ( Vec_IntSize(p) == 0 )
+        return vRes;
     Vec_IntFill( vRes, Vec_IntFindMax(p) + 1, Fill );
     Vec_IntForEachEntry( p, Entry, i )
         if ( Entry != Fill )