From 5a9a902044182bac824a98cfdccbe9aae411a7c6 Mon Sep 17 00:00:00 2001
From: Alan Mishchenko <alanmi@berkeley.edu>
Date: Wed, 17 May 2023 10:34:14 -0700
Subject: [PATCH] Bug fix in equivalence class handling (another try).

---
 src/proof/cec/cecChoice.c | 23 -----------------------
 src/proof/cec/cecSatG2.c  | 25 ++++++++++++++++++++++---
 src/proof/cec/cecSatG3.c  |  2 ++
 3 files changed, 24 insertions(+), 26 deletions(-)

diff --git a/src/proof/cec/cecChoice.c b/src/proof/cec/cecChoice.c
index 433f42c3c..0c7d1be05 100644
--- a/src/proof/cec/cecChoice.c
+++ b/src/proof/cec/cecChoice.c
@@ -412,33 +412,11 @@ Aig_Man_t * Cec_ComputeChoices( Gia_Man_t * pGia, Dch_Pars_t * pPars )
   SeeAlso     []
 
 ***********************************************************************/
-void Gia_ManRemoveWrongChoices( Gia_Man_t * p )
-{
-    int i, iObj, iPrev, Counter = 0;
-    Gia_ManForEachClass( p, i )
-    {
-        for ( iPrev = i, iObj = Gia_ObjNext(p, i); -1 < iObj; iObj = Gia_ObjNext(p, iPrev) )
-        {
-            Gia_Obj_t * pRepr = Gia_ObjReprObj(p, iObj);
-            if( !Gia_ObjFailed(p,iObj) && Abc_Lit2Var(Gia_ManObj(p,iObj)->Value) == Abc_Lit2Var(pRepr->Value) )
-            {
-                iPrev = iObj;
-                continue;
-            }
-            Gia_ObjSetRepr( p, iObj, GIA_VOID );
-            Gia_ObjSetNext( p, iPrev, Gia_ObjNext(p, iObj) );
-            Gia_ObjSetNext( p, iObj, 0 );
-            Counter++;
-        }
-    }
-    //Abc_Print( 1, "Removed %d wrong choices.\n", Counter );
-}
 Aig_Man_t * Cec_ComputeChoicesNew( Gia_Man_t * pGia, int nConfs, int fVerbose )
 {
     extern void Cec4_ManSimulateTest2( Gia_Man_t * p, int nConfs, int fVerbose );
     Aig_Man_t * pAig;
     Cec4_ManSimulateTest2( pGia, nConfs, fVerbose );
-    Gia_ManRemoveWrongChoices( pGia );
     pGia = Gia_ManEquivToChoices( pGia, 3 );
     pAig = Gia_ManToAig( pGia, 1 );
     Gia_ManStop( pGia );
@@ -450,7 +428,6 @@ Aig_Man_t * Cec_ComputeChoicesNew2( Gia_Man_t * pGia, int nConfs, int fVerbose )
     Aig_Man_t * pAig;
     Gia_Man_t * pNew = Cec5_ManSimulateTest3( pGia, nConfs, fVerbose );
     Gia_ManStop( pNew );
-    Gia_ManRemoveWrongChoices( pGia );
     pGia = Gia_ManEquivToChoices( pGia, 3 );
     pAig = Gia_ManToAig( pGia, 1 );
     Gia_ManStop( pGia );
diff --git a/src/proof/cec/cecSatG2.c b/src/proof/cec/cecSatG2.c
index 2ee8e3f86..00673c165 100644
--- a/src/proof/cec/cecSatG2.c
+++ b/src/proof/cec/cecSatG2.c
@@ -1729,6 +1729,27 @@ Gia_Obj_t * Cec4_ManFindRepr( Gia_Man_t * p, Cec4_Man_t * pMan, int iObj )
     pMan->timeResimLoc += Abc_Clock() - clk;
     return NULL;
 }
+void Gia_ManRemoveWrongChoices( Gia_Man_t * p )
+{
+    int i, iObj, iPrev, Counter = 0;
+    Gia_ManForEachClass( p, i )
+    {
+        for ( iPrev = i, iObj = Gia_ObjNext(p, i); -1 < iObj; iObj = Gia_ObjNext(p, iPrev) )
+        {
+            Gia_Obj_t * pRepr = Gia_ObjReprObj(p, iObj);
+            if( !Gia_ObjFailed(p,iObj) && Abc_Lit2Var(Gia_ManObj(p,iObj)->Value) == Abc_Lit2Var(pRepr->Value) )
+            {
+                iPrev = iObj;
+                continue;
+            }
+            Gia_ObjSetRepr( p, iObj, GIA_VOID );
+            Gia_ObjSetNext( p, iPrev, Gia_ObjNext(p, iObj) );
+            Gia_ObjSetNext( p, iObj, 0 );
+            Counter++;
+        }
+    }
+    //Abc_Print( 1, "Removed %d wrong choices.\n", Counter );
+}
 int Cec4_ManPerformSweeping( Gia_Man_t * p, Cec_ParFra_t * pPars, Gia_Man_t ** ppNew, int fSimOnly )
 {
     Cec4_Man_t * pMan = Cec4_ManCreate( p, pPars ); 
@@ -1862,13 +1883,11 @@ finalize:
             pMan->nSatUndec,  
             pMan->nSimulates, pMan->nRecycles, 100.0*pMan->nGates[1]/Abc_MaxInt(1, pMan->nGates[0]+pMan->nGates[1]) );
     Cec4_ManDestroy( pMan );
-    Gia_ManForEachAnd( p, pObj, i )
-        if ( Gia_ObjHasRepr(p, i) && !Gia_ObjProved(p, i) )
-            Gia_ObjSetRepr(p, i, GIA_VOID);
     //Gia_ManStaticFanoutStop( p );
     //Gia_ManEquivPrintClasses( p, 1, 0 );
     if ( ppNew && *ppNew == NULL )
         *ppNew = Gia_ManDup(p);
+    Gia_ManRemoveWrongChoices( p );
     return p->pCexSeq ? 0 : 1;
 }
 Gia_Man_t * Cec4_ManSimulateTest( Gia_Man_t * p, Cec_ParFra_t * pPars )
diff --git a/src/proof/cec/cecSatG3.c b/src/proof/cec/cecSatG3.c
index 44b5c2fa3..58696310b 100644
--- a/src/proof/cec/cecSatG3.c
+++ b/src/proof/cec/cecSatG3.c
@@ -1871,6 +1871,7 @@ void Cec5_ManExtend( Cec5_Man_t * pMan, CbsP_Man_t * pCbs ){
 int Cec5_ManSweepNodeCbs( Cec5_Man_t * p, CbsP_Man_t * pCbs, int iObj, int iRepr, int fTagFail );
 int Cec5_ManPerformSweeping( Gia_Man_t * p, Cec_ParFra_t * pPars, Gia_Man_t ** ppNew, int fSimOnly, int fCbs, int approxLim, int subBatchSz, int adaRecycle )
 {
+    extern void Gia_ManRemoveWrongChoices( Gia_Man_t * p );
     Gia_Obj_t * pObj, * pRepr; 
     CbsP_Man_t * pCbs = NULL;
     int i, fSimulate = 1;
@@ -2119,6 +2120,7 @@ finalize:
         CbsP_ManStop(pCbs);
     //Gia_ManStaticFanoutStop( p );
     //Gia_ManEquivPrintClasses( p, 1, 0 );
+    Gia_ManRemoveWrongChoices( p );
     return p->pCexSeq ? 0 : 1;
 }
 Gia_Man_t * Cec5_ManSimulateTest( Gia_Man_t * p, Cec_ParFra_t * pPars, int fCbs, int approxLim, int subBatchSz, int adaRecycle )