Isomorphism checking code.

7 files changed, 69 insertions, 31 deletions

diff --git a/src/aig/saig/saig.h b/src/aig/saig/saig.h
index 218cb31c..8fde2ef6 100644
--- a/src/aig/saig/saig.h
+++ b/src/aig/saig/saig.h
@@ -185,7 +185,7 @@ extern Aig_Man_t *       Saig_ManReadBlif( char * pFileName );
 /*=== saigIso.c ==========================================================*/
 extern Vec_Int_t *       Saig_ManFindIsoPerm( Aig_Man_t * pAig, int fVerbose );
 extern Aig_Man_t *       Saig_ManDupIsoCanonical( Aig_Man_t * pAig, int fVerbose );
-extern Aig_Man_t *       Saig_ManIsoReduce( Aig_Man_t * pAig, int fVerbose );
+extern Aig_Man_t *       Saig_ManIsoReduce( Aig_Man_t * pAig, Vec_Ptr_t ** pvPosEquivs, int fVerbose );
 /*=== saigIsoFast.c ==========================================================*/
 extern Vec_Vec_t *       Saig_IsoDetectFast( Aig_Man_t * pAig );
 /*=== saigMiter.c ==========================================================*/
diff --git a/src/aig/saig/saigIso.c b/src/aig/saig/saigIso.c
index 0e7c9de1..ff10df82 100644
--- a/src/aig/saig/saigIso.c
+++ b/src/aig/saig/saigIso.c
@@ -362,8 +362,8 @@ Aig_Man_t * Iso_ManFilterPos_old( Aig_Man_t * pAig, int fVerbose )
             {
                 if ( fVeryVerbose )
                     printf( "Found match\n" );
-                if ( fVerbose )
-                    printf( "Found match for AIG %4d and AIG %4d.\n", Vec_IntEntry(vPos,k), i );
+//                if ( fVerbose )
+//                    printf( "Found match for AIG %4d and AIG %4d.\n", Vec_IntEntry(vPos,k), i );
                 Vec_IntFree( vMap );
                 break;
             }
@@ -419,7 +419,7 @@ int Iso_StoCompareVecStr( Vec_Str_t ** p1, Vec_Str_t ** p2 )
   SeeAlso     []
 
 ***********************************************************************/
-Aig_Man_t * Iso_ManFilterPos( Aig_Man_t * pAig, int fVerbose )
+Aig_Man_t * Iso_ManFilterPos( Aig_Man_t * pAig, Vec_Ptr_t ** pvPosEquivs, int fVerbose )
 {
 //    int fVeryVerbose = 0;
     Aig_Man_t * pPart, * pTemp;
@@ -492,6 +492,7 @@ Aig_Man_t * Iso_ManFilterPos( Aig_Man_t * pAig, int fVerbose )
     // report the results
 //    Vec_VecPrintInt( (Vec_Vec_t *)vClasses );
 //    printf( "Devided %d outputs into %d cand equiv classes.\n", Saig_ManPoNum(pAig), Vec_PtrSize(vClasses) );
+/*
     if ( fVerbose )
     {
         Vec_PtrForEachEntry( Vec_Int_t *, vClasses, vLevel, i )
@@ -501,7 +502,7 @@ Aig_Man_t * Iso_ManFilterPos( Aig_Man_t * pAig, int fVerbose )
                 nUnique++;
         printf( " Unique = %d\n", nUnique );
     }
-
+*/
     // collect the first ones
     vRemain = Vec_IntAlloc( 100 );
     Vec_PtrForEachEntry( Vec_Int_t *, vClasses, vLevel, i )
@@ -512,7 +513,13 @@ Aig_Man_t * Iso_ManFilterPos( Aig_Man_t * pAig, int fVerbose )
     Vec_IntFree( vRemain );
 
 //    return (Vec_Vec_t *)vClasses;
-    Vec_VecFree( (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;
@@ -550,11 +557,11 @@ Aig_Man_t * Iso_ManTest( Aig_Man_t * pAig, int fVerbose )
   SeeAlso     []
 
 ***********************************************************************/
-Aig_Man_t * Saig_ManIsoReduce( Aig_Man_t * pAig, int fVerbose )
+Aig_Man_t * Saig_ManIsoReduce( Aig_Man_t * pAig, Vec_Ptr_t ** pvPosEquivs, int fVerbose )
 { 
     Aig_Man_t * pPart;
     int clk = clock();
-    pPart = Iso_ManFilterPos( pAig, fVerbose );
+    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 );
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 16c9ffe7..c77a4f2b 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -422,6 +422,26 @@ void Abc_FrameReplaceCexVec( Abc_Frame_t * pAbc, Vec_Ptr_t ** pvCexVec )
   SeeAlso     []
 
 ***********************************************************************/
+void Abc_FrameReplacePoEquivs( Abc_Frame_t * pAbc, Vec_Ptr_t ** pvPoEquivs )
+{
+    // update the array vector
+    if ( pAbc->vPoEquivs )
+        Vec_VecFree( (Vec_Vec_t *)pAbc->vPoEquivs );
+    pAbc->vPoEquivs = *pvPoEquivs;
+    *pvPoEquivs = NULL;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 void Abc_FrameClearDesign()
 {
 }
@@ -21335,6 +21355,7 @@ int Abc_CommandIso( Abc_Frame_t * pAbc, int argc, char ** argv )
     extern Abc_Ntk_t * Abc_NtkFromAigPhase( Aig_Man_t * pMan );
     Abc_Ntk_t * pNtk, * pNtkNew = NULL;
     Aig_Man_t * pAig, * pTemp;
+    Vec_Ptr_t * vPosEquivs = NULL;
     int c, fVerbose = 0;
     Extra_UtilGetoptReset();
     while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
@@ -21372,11 +21393,14 @@ int Abc_CommandIso( Abc_Frame_t * pAbc, int argc, char ** argv )
 
     // transform
     pAig = Abc_NtkToDar( pNtk, 0, 1 );
-    pTemp = Saig_ManIsoReduce( pAig, fVerbose );
+    pTemp = Saig_ManIsoReduce( pAig, &vPosEquivs, fVerbose );
     pNtkNew = Abc_NtkFromAigPhase( pTemp );
     Aig_ManStop( pTemp );
     Aig_ManStop( pAig );
 
+    // update the internal storage of PO equivalences
+    Abc_FrameReplacePoEquivs( pAbc, &vPosEquivs );
+
     // replace the current network
     Abc_FrameReplaceCurrentNetwork( pAbc, pNtkNew );
     return 0;
diff --git a/src/base/main/main.h b/src/base/main/main.h
index 33f8a110..ac30f358 100644
--- a/src/base/main/main.h
+++ b/src/base/main/main.h
@@ -108,7 +108,8 @@ extern ABC_DLL int             Abc_FrameIsFlagEnabled( char * pFlag );
 extern ABC_DLL int             Abc_FrameReadBmcFrames( Abc_Frame_t * p );              
 extern ABC_DLL int             Abc_FrameReadProbStatus( Abc_Frame_t * p );              
 extern ABC_DLL Abc_Cex_t *     Abc_FrameReadCex( Abc_Frame_t * p );              
-extern ABC_DLL Vec_Ptr_t *     Abc_FrameReadCexVec( Abc_Frame_t * p );              
+extern ABC_DLL Vec_Ptr_t *     Abc_FrameReadCexVec( Abc_Frame_t * p );  
+extern ABC_DLL Vec_Ptr_t *     Abc_FrameReadPoEquivs( Abc_Frame_t * p );  
 
 extern ABC_DLL int             Abc_FrameReadCexPiNum( Abc_Frame_t * p );              
 extern ABC_DLL int             Abc_FrameReadCexRegNum( Abc_Frame_t * p );              
diff --git a/src/base/main/mainFrame.c b/src/base/main/mainFrame.c
index d03acf28..6a63cdd6 100644
--- a/src/base/main/mainFrame.c
+++ b/src/base/main/mainFrame.c
@@ -63,11 +63,12 @@ int         Abc_FrameReadBmcFrames( Abc_Frame_t * p )        { return s_GlobalFr
 int         Abc_FrameReadProbStatus( Abc_Frame_t * p )       { return s_GlobalFrame->Status;       }               
 Abc_Cex_t * Abc_FrameReadCex( Abc_Frame_t * p )              { return s_GlobalFrame->pCex;         }        
 Vec_Ptr_t * Abc_FrameReadCexVec( Abc_Frame_t * p )           { return s_GlobalFrame->vCexVec;      }        
+Vec_Ptr_t * Abc_FrameReadPoEquivs( Abc_Frame_t * p )         { return s_GlobalFrame->vPoEquivs;    }        
        
-int         Abc_FrameReadCexPiNum( Abc_Frame_t * p )         { return s_GlobalFrame->pCex->nPis;      }               
-int         Abc_FrameReadCexRegNum( Abc_Frame_t * p )        { return s_GlobalFrame->pCex->nRegs;     }               
-int         Abc_FrameReadCexPo( Abc_Frame_t * p )            { return s_GlobalFrame->pCex->iPo;       }               
-int         Abc_FrameReadCexFrame( Abc_Frame_t * p )         { return s_GlobalFrame->pCex->iFrame;    }               
+int         Abc_FrameReadCexPiNum( Abc_Frame_t * p )         { return s_GlobalFrame->pCex->nPis;   }               
+int         Abc_FrameReadCexRegNum( Abc_Frame_t * p )        { return s_GlobalFrame->pCex->nRegs;  }               
+int         Abc_FrameReadCexPo( Abc_Frame_t * p )            { return s_GlobalFrame->pCex->iPo;    }               
+int         Abc_FrameReadCexFrame( Abc_Frame_t * p )         { return s_GlobalFrame->pCex->iFrame; }               
 
 void        Abc_FrameSetLibLut( void * pLib )                { s_GlobalFrame->pLibLut   = pLib;    } 
 void        Abc_FrameSetLibGen( void * pLib )                { s_GlobalFrame->pLibGen   = pLib;    } 
@@ -162,14 +163,16 @@ void Abc_FrameDeallocate( Abc_Frame_t * p )
 //    undefine_cube_size();
     Rwt_ManGlobalStop();
 //    Ivy_TruthManStop();
-    if ( p->pLibVer ) Abc_LibFree( (Abc_Lib_t *)p->pLibVer, NULL );
-    if ( p->pManDec ) Dec_ManStop( (Dec_Man_t *)p->pManDec );
-    if ( p->dd )      Extra_StopManager( p->dd );
-    if ( p->vStore )  Vec_PtrFree( p->vStore );
-    if ( p->pSave1 )  Aig_ManStop( (Aig_Man_t *)p->pSave1 );
-    if ( p->pSave2 )  Aig_ManStop( (Aig_Man_t *)p->pSave2 );
-    if ( p->pSave3 )  Aig_ManStop( (Aig_Man_t *)p->pSave3 );
-    if ( p->pSave4 )  Aig_ManStop( (Aig_Man_t *)p->pSave4 );
+    if ( p->vCexVec   )  Vec_PtrFreeFree( p->vCexVec );
+    if ( p->vPoEquivs )  Vec_VecFree( (Vec_Vec_t *)p->vPoEquivs );
+    if ( p->pLibVer   )  Abc_LibFree( (Abc_Lib_t *)p->pLibVer, NULL );
+    if ( p->pManDec   )  Dec_ManStop( (Dec_Man_t *)p->pManDec );
+    if ( p->dd        )  Extra_StopManager( p->dd );
+    if ( p->vStore    )  Vec_PtrFree( p->vStore );
+    if ( p->pSave1    )  Aig_ManStop( (Aig_Man_t *)p->pSave1 );
+    if ( p->pSave2    )  Aig_ManStop( (Aig_Man_t *)p->pSave2 );
+    if ( p->pSave3    )  Aig_ManStop( (Aig_Man_t *)p->pSave3 );
+    if ( p->pSave4    )  Aig_ManStop( (Aig_Man_t *)p->pSave4 );
     if ( p->vPlugInComBinPairs ) 
     {
         char * pTemp;
diff --git a/src/base/main/mainInt.h b/src/base/main/mainInt.h
index 979d376c..2eca004e 100644
--- a/src/base/main/mainInt.h
+++ b/src/base/main/mainInt.h
@@ -90,10 +90,11 @@ struct Abc_Frame_t_
     void *          pLibVer;     // the current Verilog library
 
     // new code
-    Gia_Man_t *     pGia;
-    Gia_Man_t *     pGia2;
-    Abc_Cex_t *     pCex; 
-    Vec_Ptr_t *     vCexVec;
+    Gia_Man_t *     pGia;        // alternative current network as a light-weight AIG
+    Gia_Man_t *     pGia2;       // copy of the above
+    Abc_Cex_t *     pCex;        // a counter-example to fail the current network
+    Vec_Ptr_t *     vCexVec;     // a vector of counter-examples if more than one PO fails
+    Vec_Ptr_t *     vPoEquivs;   // equivalence classes of isomorphic primary outputs
 
     void *          pSave1; 
     void *          pSave2; 
diff --git a/src/misc/vec/vecVec.h b/src/misc/vec/vecVec.h
index f72bd93c..e0f18983 100644
--- a/src/misc/vec/vecVec.h
+++ b/src/misc/vec/vecVec.h
@@ -597,17 +597,19 @@ static inline void Vec_VecSort( Vec_Vec_t * p, int fReverse )
   SeeAlso     []
 
 ***********************************************************************/
-static inline void Vec_VecPrintInt( Vec_Vec_t * p )
+static inline void Vec_VecPrintInt( Vec_Vec_t * p, int fSkipSingles )
 {
     int i, k, Entry;
-    printf( "Integers by level" );
     Vec_VecForEachEntryInt( p, Entry, i, k )
     {
+        if ( Vec_VecLevelSize(p, i) == 1 )
+            break;
         if ( k == 0 )
-            printf( "\n%3d : ", i );
-        printf( "%6d ", Entry );
+            printf( " %4d : {", i );
+        printf( " %d", Entry );
+        if ( k == Vec_VecLevelSize(p, i) - 1 )
+            printf( " }\n" );
     }
-    printf( "\n" );
 }