From 9c152b71e934f616240c33618edc05ebf5e3bf9d Mon Sep 17 00:00:00 2001
From: Alan Mishchenko <alanmi@berkeley.edu>
Date: Thu, 12 Sep 2024 18:11:59 -0700
Subject: [PATCH] Trasferring equivalence in the special-case usage of &scorr.

---
 src/aig/gia/giaEquiv.c | 48 ++++++++++++++++++++++++++++++++++++++++++
 src/base/abci/abc.c    |  2 ++
 2 files changed, 50 insertions(+)

diff --git a/src/aig/gia/giaEquiv.c b/src/aig/gia/giaEquiv.c
index aec9d39ca..09def827d 100644
--- a/src/aig/gia/giaEquiv.c
+++ b/src/aig/gia/giaEquiv.c
@@ -2732,6 +2732,54 @@ void Gia_ManTransferTest( Gia_Man_t * p )
     Gia_ManStop( pNew );
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Transfer from new to old.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_ManTransferEquivs2( Gia_Man_t * p, Gia_Man_t * pOld )
+{
+    Gia_Obj_t * pObj;
+    Vec_Int_t * vClass;
+    int i, k, iNode, iRepr;
+    assert( p->pReprs != NULL );
+    assert( p->pNexts != NULL );
+    assert( pOld->pReprs == NULL );
+    assert( pOld->pNexts == NULL );
+    // create map
+    Gia_ManFillValue( p );
+    Gia_ManForEachObj( pOld, pObj, i )
+        if ( ~pObj->Value )
+            Gia_ManObj(p, Abc_Lit2Var(pObj->Value))->Value = Abc_Var2Lit(i, 0);
+    // start representatives
+    pOld->pReprs = ABC_CALLOC( Gia_Rpr_t, Gia_ManObjNum(pOld) );
+    for ( i = 0; i < Gia_ManObjNum(pOld); i++ )
+        Gia_ObjSetRepr( pOld, i, GIA_VOID );
+    // iterate over constant candidates
+    Gia_ManForEachConst( p, i )
+        Gia_ObjSetRepr( pOld, Abc_Lit2Var(Gia_ManObj(p, i)->Value), 0 );
+    // iterate over class candidates
+    vClass = Vec_IntAlloc( 100 );
+    Gia_ManForEachClass( p, i )
+    {
+        Vec_IntClear( vClass );
+        Gia_ClassForEachObj( p, i, k )
+            Vec_IntPushUnique( vClass, Abc_Lit2Var(Gia_ManObj(p, k)->Value) );
+        assert( Vec_IntSize( vClass ) > 1 );
+        Vec_IntSort( vClass, 0 );
+        iRepr = Vec_IntEntry( vClass, 0 );
+        Vec_IntForEachEntryStart( vClass, iNode, k, 1 )
+            Gia_ObjSetRepr( pOld, iNode, iRepr );
+    }
+    Vec_IntFree( vClass );
+    pOld->pNexts = Gia_ManDeriveNexts( pOld );
+}
 
 /**Function*************************************************************
 
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 29b418fa3..88753520e 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -38616,6 +38616,7 @@ int Abc_CommandAbc9Scorr( Abc_Frame_t * pAbc, int argc, char ** argv )
         Vec_Int_t * vStops = Gia_ManFindStopFlops( pAbc->pGia, nFlopIncFreq, pPars->fVerbose );
         if ( vStops )
         {
+            extern void Gia_ManTransferEquivs2( Gia_Man_t * p, Gia_Man_t * pNew );
             Gia_Man_t * pUsed = Gia_ManDupStopsAdd( pAbc->pGia, vStops );
             if ( pPars->nPartSize > 0 )
                 pTemp = Gia_SignalCorrespondencePart( pUsed, pPars );
@@ -38625,6 +38626,7 @@ int Abc_CommandAbc9Scorr( Abc_Frame_t * pAbc, int argc, char ** argv )
                 pTemp = Gia_ManScorrDivideTest( pUsed, pPars );
             else
                 pTemp = Cec_ManLSCorrespondence( pUsed, pPars );
+            Gia_ManTransferEquivs2( pUsed, pAbc->pGia );
             Gia_ManStop( pUsed );
             pTemp = Gia_ManDupStopsRem( pUsed = pTemp, vStops );
             Gia_ManStop( pUsed );