Skip to content

Commit 745376d

Browse files
committed
Reconstruction of structural choices.
1 parent 9478c17 commit 745376d

File tree

2 files changed

+94
-4
lines changed

2 files changed

+94
-4
lines changed

src/aig/gia/giaDup.c

Lines changed: 74 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -4162,6 +4162,80 @@ Gia_Man_t * Gia_ManDupLevelized( Gia_Man_t * p )
41624162
return pNew;
41634163
}
41644164

4165+
/**Function*************************************************************
4166+
4167+
Synopsis []
4168+
4169+
Description []
4170+
4171+
SideEffects []
4172+
4173+
SeeAlso []
4174+
4175+
***********************************************************************/
4176+
void Gia_ManDupChoicesTest( Gia_Man_t * p, Gia_Man_t * pNew )
4177+
{
4178+
Gia_ManCreateRefs( p );
4179+
Gia_ManMarkFanoutDrivers( p );
4180+
Gia_Obj_t * pObj; int i;
4181+
int ChoiceCounts[2][1000] = {{0}};
4182+
Gia_ManForEachAnd( p, pObj, i )
4183+
if ( Gia_ObjSibl(p, i) && pObj->fMark0 )
4184+
{
4185+
Gia_Obj_t * pSibl, * pPrev; int Size = 1;
4186+
for ( pPrev = pObj, pSibl = Gia_ObjSiblObj(p, i); pSibl; pPrev = pSibl, pSibl = Gia_ObjSiblObj(p, Gia_ObjId(p, pSibl)) )
4187+
Size++;
4188+
assert( Size < 1000 );
4189+
ChoiceCounts[0][Size]++;
4190+
}
4191+
Gia_ManCleanMark0( p );
4192+
int nSize = 1;
4193+
Gia_ManForEachAnd( pNew, pObj, i )
4194+
if ( Gia_ObjRefNumId(p, i) == 0 )
4195+
nSize++;
4196+
else if ( nSize > 1 ) {
4197+
assert( nSize < 1000 );
4198+
ChoiceCounts[1][nSize]++;
4199+
nSize = 1;
4200+
}
4201+
printf( "Choice counting statistics:\n" );
4202+
for ( i = 0; i < 1000; i++ )
4203+
if ( ChoiceCounts[0][i] || ChoiceCounts[1][i] )
4204+
printf( "%3d : %6d %6d\n", i, ChoiceCounts[0][i], ChoiceCounts[1][i] );
4205+
}
4206+
void Gia_ManDupChoices_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj )
4207+
{
4208+
if ( ~pObj->Value )
4209+
return;
4210+
assert( Gia_ObjIsAnd(pObj) );
4211+
Gia_ManDupChoices_rec( pNew, p, Gia_ObjFanin0(pObj) );
4212+
Gia_ManDupChoices_rec( pNew, p, Gia_ObjFanin1(pObj) );
4213+
Gia_Obj_t * pSibl = Gia_ObjSiblObj(p, Gia_ObjId(p, pObj));
4214+
if ( pSibl ) Gia_ManDupChoices_rec( pNew, p, pSibl );
4215+
pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
4216+
if ( pSibl ) pNew->pSibls[Abc_Lit2Var(pObj->Value)] = Abc_Lit2Var(pObj->Value)-1;
4217+
}
4218+
Gia_Man_t * Gia_ManDupChoices( Gia_Man_t * p )
4219+
{
4220+
//Gia_ManPrintChoices( p );
4221+
assert( p->pSibls );
4222+
Gia_Obj_t * pObj; int i;
4223+
Gia_Man_t * pNew = Gia_ManStart( Gia_ManObjNum(p) );
4224+
pNew->pName = Abc_UtilStrsav( p->pName );
4225+
pNew->pSpec = Abc_UtilStrsav( p->pSpec );
4226+
pNew->pSibls = ABC_CALLOC( int, Gia_ManObjNum(p) );
4227+
Gia_ManFillValue(p);
4228+
Gia_ManForEachCi( p, pObj, i )
4229+
pObj->Value = Gia_ManAppendCi(pNew);
4230+
Gia_ManForEachCo( p, pObj, i )
4231+
Gia_ManDupChoices_rec( pNew, p, Gia_ObjFanin0(pObj) );
4232+
Gia_ManForEachCo( p, pObj, i )
4233+
Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
4234+
Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
4235+
//Gia_ManDupChoicesTest( p, pNew );
4236+
return pNew;
4237+
}
4238+
41654239
/**Function*************************************************************
41664240
41674241
Synopsis []

src/base/abci/abc.c

Lines changed: 20 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -36126,21 +36126,26 @@ int Abc_CommandAbc9Trim( Abc_Frame_t * pAbc, int argc, char ** argv )
3612636126
***********************************************************************/
3612736127
int Abc_CommandAbc9Dfs( Abc_Frame_t * pAbc, int argc, char ** argv )
3612836128
{
36129+
extern Gia_Man_t * Gia_ManDupChoices( Gia_Man_t * p );
3612936130
Gia_Man_t * pTemp;
3613036131
int c;
3613136132
int fNormal = 0;
36133+
int fChoices = 0;
3613236134
int fRevFans = 0;
3613336135
int fRevOuts = 0;
3613436136
int fLeveled = 0;
3613536137
int fVerbose = 0;
3613636138
Extra_UtilGetoptReset();
36137-
while ( ( c = Extra_UtilGetopt( argc, argv, "nfolvh" ) ) != EOF )
36139+
while ( ( c = Extra_UtilGetopt( argc, argv, "ncfolvh" ) ) != EOF )
3613836140
{
3613936141
switch ( c )
3614036142
{
3614136143
case 'n':
3614236144
fNormal ^= 1;
3614336145
break;
36146+
case 'c':
36147+
fChoices ^= 1;
36148+
break;
3614436149
case 'f':
3614536150
fRevFans ^= 1;
3614636151
break;
@@ -36164,7 +36169,9 @@ int Abc_CommandAbc9Dfs( Abc_Frame_t * pAbc, int argc, char ** argv )
3616436169
Abc_Print( -1, "Abc_CommandAbc9Dfs(): There is no AIG.\n" );
3616536170
return 1;
3616636171
}
36167-
if ( fLeveled )
36172+
if ( fChoices )
36173+
pTemp = Gia_ManDupChoices( pAbc->pGia );
36174+
else if ( fLeveled )
3616836175
pTemp = Gia_ManDupLevelized( pAbc->pGia );
3616936176
else if ( fNormal )
3617036177
pTemp = Gia_ManDupOrderAiger( pAbc->pGia );
@@ -36174,9 +36181,10 @@ int Abc_CommandAbc9Dfs( Abc_Frame_t * pAbc, int argc, char ** argv )
3617436181
return 0;
3617536182

3617636183
usage:
36177-
Abc_Print( -2, "usage: &dfs [-nfolvh]\n" );
36184+
Abc_Print( -2, "usage: &dfs [-ncfolvh]\n" );
3617836185
Abc_Print( -2, "\t orders objects in the DFS order\n" );
3617936186
Abc_Print( -2, "\t-n : toggle using normalized ordering [default = %s]\n", fNormal? "yes": "no" );
36187+
Abc_Print( -2, "\t-c : toggle using ordering for AIG with choices [default = %s]\n", fChoices? "yes": "no" );
3618036188
Abc_Print( -2, "\t-f : toggle using reverse fanin traversal order [default = %s]\n", fRevFans? "yes": "no" );
3618136189
Abc_Print( -2, "\t-o : toggle using reverse output traversal order [default = %s]\n", fRevOuts? "yes": "no" );
3618236190
Abc_Print( -2, "\t-l : toggle using levelized order [default = %s]\n", fLeveled? "yes": "no" );
@@ -57706,14 +57714,22 @@ int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv )
5770657714
goto usage;
5770757715
}
5770857716
}
57717+
/*
57718+
Gia_Obj_t * pObj; int i;
57719+
Gia_ManCreateRefs(pAbc->pGia);
57720+
Gia_ManForEachAnd( pAbc->pGia, pObj, i )
57721+
if ( !Gia_ObjIsLut(pAbc->pGia, i) && Gia_ObjRefNum(pAbc->pGia, pObj) > 1 )
57722+
printf( "%d ", Gia_ObjRefNum(pAbc->pGia, pObj) );
57723+
printf( "\n" );
57724+
return 0;
5770957725

5771057726
extern void cadical_solver_test();
5771157727
cadical_solver_test();
5771257728
return 0;
5771357729
extern void kissat_solver_test();
5771457730
kissat_solver_test();
5771557731
return 0;
57716-
57732+
*/
5771757733
if ( pAbc->pGia == NULL )
5771857734
{
5771957735
Abc_Print( -1, "Abc_CommandAbc9Test(): There is no AIG.\n" );

0 commit comments

Comments
 (0)