Fix(&dch): choices bugs in &put

berkeley-abc · Jan 9, 2025 · 8c7c9d0 · 8c7c9d0
1 parent d5e1a5d
commit 8c7c9d0
Show file tree

Hide file tree

Showing 4 changed files with 41 additions and 0 deletions.
diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
@@ -478,6 +478,7 @@ static inline int          Gia_ManConstrNum( Gia_Man_t * p )   { return p->nCons
 static inline void         Gia_ManFlipVerbose( Gia_Man_t * p ) { p->fVerbose ^= 1;                                                         } 
 static inline int          Gia_ManHasChoices( Gia_Man_t * p )  { return p->pSibls != NULL;                                                 } 
 static inline int          Gia_ManChoiceNum( Gia_Man_t * p )   { int c = 0; if (p->pSibls) { int i; for (i = 0; i < p->nObjs; i++) c += (int)(p->pSibls[i] > 0); } return c; } 
+static inline int          Gia_ManHasChoicesOri( Gia_Man_t *p ){ return p->pReprs != NULL;                                                  }
 
 static inline Gia_Obj_t *  Gia_ManConst0( Gia_Man_t * p )      { return p->pObjs;                                                          }
 static inline Gia_Obj_t *  Gia_ManConst1( Gia_Man_t * p )      { return Gia_Not(Gia_ManConst0(p));                                         }
@@ -1436,6 +1437,7 @@ extern void                Gia_ManEquivFixOutputPairs( Gia_Man_t * p );
 extern int                 Gia_ManCheckTopoOrder( Gia_Man_t * p );
 extern int *               Gia_ManDeriveNexts( Gia_Man_t * p );
 extern void                Gia_ManDeriveReprs( Gia_Man_t * p );
+extern void                Gia_ManDeriveReprsFromSibls( Gia_Man_t *p );
 extern int                 Gia_ManEquivCountLits( Gia_Man_t * p );
 extern int                 Gia_ManEquivCountLitsAll( Gia_Man_t * p );
 extern int                 Gia_ManEquivCountClasses( Gia_Man_t * p );

diff --git a/src/aig/gia/giaAig.c b/src/aig/gia/giaAig.c
@@ -19,10 +19,12 @@
 ***********************************************************************/
 
 #include "giaAig.h"
+#include "aig/gia/gia.h"
 #include "proof/fra/fra.h"
 #include "proof/dch/dch.h"
 #include "opt/dar/dar.h"
 #include "opt/dau/dau.h"
+#include <assert.h>
 
 ABC_NAMESPACE_IMPL_START
 
@@ -191,6 +193,8 @@ Gia_Man_t * Gia_ManFromAigChoices( Aig_Man_t * p )
     Gia_ManSetRegNum( pNew, Aig_ManRegNum(p) );
     //assert( Gia_ManObjNum(pNew) == Aig_ManObjNum(p) );
     //Gia_ManCheckChoices( pNew );
+    if ( pNew->pSibls )
+        Gia_ManDeriveReprsFromSibls( pNew );
     return pNew;
 }
 

diff --git a/src/aig/gia/giaEquiv.c b/src/aig/gia/giaEquiv.c
@@ -310,6 +310,39 @@ void Gia_ManDeriveReprs( Gia_Man_t * p )
     }
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Given pSibls, derives original representitives and nexts.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+
+void Gia_ManDeriveReprsFromSibls( Gia_Man_t *p )
+{
+
+    int i, iObj;
+    assert( !p->pReprs && p->pSibls );
+    p->pReprs = ABC_CALLOC( Gia_Rpr_t, Gia_ManObjNum(p) );
+    for ( i = 0; i < Gia_ManObjNum(p); i++ )
+        Gia_ObjSetRepr( p, i, GIA_VOID );
+    for ( i = 0; i < Gia_ManObjNum(p); i++ )
+    {
+        if ( p->pSibls[i] == 0 )
+            continue;
+        if ( p->pReprs[i].iRepr != GIA_VOID )
+            continue;
+        for ( iObj = p->pSibls[i]; iObj; iObj = p->pSibls[iObj] )
+            p->pReprs[iObj].iRepr = i;
+    }
+    ABC_FREE( p->pNexts );
+    p->pNexts = Gia_ManDeriveNexts( p );
+}
+
 /**Function*************************************************************
 
   Synopsis    []

diff --git a/src/aig/gia/giaMan.c b/src/aig/gia/giaMan.c
@@ -557,6 +557,8 @@ void Gia_ManPrintStats( Gia_Man_t * p, Gps_Par_t * pPars )
     Abc_Print( 1, "  mem =%5.2f MB", Gia_ManMemory(p)/(1<<20) );
     if ( Gia_ManHasChoices(p) )
         Abc_Print( 1, "  ch =%5d", Gia_ManChoiceNum(p) );
+    if ( Gia_ManHasChoicesOri(p))
+        Abc_Print( 1, "  chOri =%5d", Gia_ManEquivCountClasses(p) );
     if ( p->pManTime )
         Abc_Print( 1, "  box = %d", Gia_ManNonRegBoxNum(p) );
     if ( p->pManTime )