From a620c09c401a3d219d91151f39e74943b65d7f40 Mon Sep 17 00:00:00 2001
From: Alan Mishchenko <alanmi@berkeley.edu>
Date: Sat, 22 Jul 2023 16:44:33 -0700
Subject: [PATCH] Adding functional comparison to &compare.

---
 src/aig/gia/giaSimBase.c | 52 ++++++++++++++++++++++++++++++++++++++++
 src/base/abci/abc.c      | 18 ++++++++++----
 2 files changed, 65 insertions(+), 5 deletions(-)

diff --git a/src/aig/gia/giaSimBase.c b/src/aig/gia/giaSimBase.c
index 47f645413..97335d378 100644
--- a/src/aig/gia/giaSimBase.c
+++ b/src/aig/gia/giaSimBase.c
@@ -3689,6 +3689,58 @@ Vec_Str_t * Gia_ManComputeRange( Gia_Man_t * p )
     return vOut;
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_ManComparePrint( Gia_Man_t * p, Gia_Man_t * q )
+{
+    Vec_Wrd_t * vSimsPi = Vec_WrdStartTruthTables( Gia_ManCiNum(p) );
+    Vec_Wrd_t * vSimsP  = Gia_ManSimPatSimOut( p, vSimsPi, 0 );
+    Vec_Wrd_t * vSimsQ  = Gia_ManSimPatSimOut( q, vSimsPi, 0 );
+    int i, k, nWords = Vec_WrdSize(vSimsPi) / Gia_ManCiNum(p), Count = 0;
+    Gia_Obj_t * pObjP, * pObjQ;
+    Gia_ManSetPhase( p );
+    Gia_ManSetPhase( q );
+    Gia_ManForEachObj( p, pObjP, i ) {
+        word * pSim = Vec_WrdEntryP( vSimsP, i * nWords );
+        if ( pSim[0] & 1 ) Abc_TtNot( pSim, nWords );
+    }
+    Gia_ManForEachObj( q, pObjQ, i ) {
+        word * pSim = Vec_WrdEntryP( vSimsQ, i * nWords );
+        if ( pSim[0] & 1 ) Abc_TtNot( pSim, nWords );
+    }    
+    Gia_ManForEachAnd( q, pObjQ, i ) {
+        word * pSimQ = Vec_WrdEntryP( vSimsQ, i * nWords );
+        int fFirst = 1;
+        Gia_ManForEachObj( p, pObjP, k ) {
+            word * pSimP = Vec_WrdEntryP( vSimsP, k * nWords );
+            if ( !Abc_TtEqual(pSimQ, pSimP, nWords) )
+                continue;
+            if ( fFirst ) {
+                printf( "%5d :", i );
+                fFirst = 0;
+                Count++;
+            }
+            printf( " %5d(%d)", k, pObjQ->fPhase ^ pObjP->fPhase );
+        }
+        if ( !fFirst )
+            printf( "\n");
+    }   
+    printf( "Found %d equivalent nodes.\n", Count );
+    Vec_WrdFree( vSimsP );
+    Vec_WrdFree( vSimsQ );
+    Vec_WrdFree( vSimsPi );
+}
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index baf0d7eec..d2bc978d4 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -45032,17 +45032,21 @@ usage:
 int Abc_CommandAbc9Compare( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     extern void Gia_Iso4TestTwo( Gia_Man_t * pGia0, Gia_Man_t * pGia1 );
+    extern void Gia_ManComparePrint( Gia_Man_t * p, Gia_Man_t * q );
     Gia_Man_t * pGia0, * pGia1;
     char ** pArgvNew; int nArgcNew;
-    int c, fVerbose = 0;
+    int c, fFunc = 0, fVerbose = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "fvh" ) ) != EOF )
     {
         switch ( c )
         {
+        case 'f':
+            fFunc ^= 1;
+            break;
         case 'v':
             fVerbose ^= 1;
-            break;
+            break;        
         case 'h':
             goto usage;
         default:
@@ -45063,14 +45067,18 @@ int Abc_CommandAbc9Compare( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_Print( -1, "Abc_CommandAbc9Compare(): Reading input files did not work.\n" );
         return 1;
     }
-    Gia_Iso4TestTwo( pGia0, pGia1 );
+    if ( fFunc )
+        Gia_ManComparePrint( pGia0, pGia1 );
+    else
+        Gia_Iso4TestTwo( pGia0, pGia1 );
     Gia_ManStop( pGia0 );
     Gia_ManStop( pGia1 );
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &compare <file1> <file2> [-vh]\n" );
+    Abc_Print( -2, "usage: &compare <file1> <file2> [-fvh]\n" );
     Abc_Print( -2, "\t         compared two AIGs for structural similarity\n" );
+    Abc_Print( -2, "\t-f     : toggle functional comparison [default = %s]\n", fFunc? "yes": "no" );
     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;