Fix(&dch): choices bugs in &put

This commit is contained in:
wjrforcyber 2025-01-09 22:21:32 +08:00
parent d5e1a5d445
commit 8c7c9d0ccf
No known key found for this signature in database
4 changed files with 41 additions and 0 deletions

View File

@ -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 );

View File

@ -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;
}

View File

@ -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 []

View File

@ -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 )