From 6e1653426f41529cd3d42bbe39d322750387205e Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Thu, 28 Mar 2024 16:22:06 +0800 Subject: [PATCH] Switch to randomly select one choice. --- src/aig/gia/giaEquiv.c | 33 +++++++++++++++++++++++++++++---- src/base/abci/abc.c | 18 +++++++++++------- 2 files changed, 40 insertions(+), 11 deletions(-) diff --git a/src/aig/gia/giaEquiv.c b/src/aig/gia/giaEquiv.c index 1c3aa4311..aec9d39ca 100644 --- a/src/aig/gia/giaEquiv.c +++ b/src/aig/gia/giaEquiv.c @@ -715,6 +715,30 @@ Gia_Man_t * Gia_ManEquivReduce( Gia_Man_t * p, int fUseAll, int fDualOut, int fS return pNew; } +/**Function************************************************************* + + Synopsis [Duplicates the AIG in the DFS order.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_Obj_t * Gia_MakeRandomChoice( Gia_Man_t * p, int iRepr ) +{ + int iTemp, Rand, Count = 0; + Gia_ClassForEachObj( p, iRepr, iTemp ) + Count++; + Rand = rand() % Count; + Count = 0; + Gia_ClassForEachObj( p, iRepr, iTemp ) + if ( Count++ == Rand ) + break; + return Gia_ManObj(p, iTemp); +} + /**Function************************************************************* Synopsis [Duplicates the AIG in the DFS order.] @@ -735,7 +759,7 @@ void Gia_ManEquivReduce2_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, if ( fDiveIn && (pRepr = Gia_ManEquivRepr(p, pObj, 1, 0)) ) { int iTemp, iRepr = Gia_ObjId(p, pRepr); - Gia_Obj_t * pRepr2 = Gia_ManObj( p, Vec_IntEntry(vMap, iRepr) ); + Gia_Obj_t * pRepr2 = vMap ? Gia_ManObj( p, Vec_IntEntry(vMap, iRepr) ) : Gia_MakeRandomChoice(p, iRepr); Gia_ManEquivReduce2_rec( pNew, p, pRepr2, vMap, 0 ); Gia_ClassForEachObj( p, iRepr, iTemp ) { @@ -751,12 +775,13 @@ void Gia_ManEquivReduce2_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, Gia_ManEquivReduce2_rec( pNew, p, Gia_ObjFanin1(pObj), vMap, 1 ); pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); } -Gia_Man_t * Gia_ManEquivReduce2( Gia_Man_t * p ) +Gia_Man_t * Gia_ManEquivReduce2( Gia_Man_t * p, int fRandom ) { Vec_Int_t * vMap; Gia_Man_t * pNew; Gia_Obj_t * pObj; int i; + if ( fRandom ) srand(time(NULL)); if ( !p->pReprs && p->pSibls ) { int * pMap = ABC_FALLOC( int, Gia_ManObjNum(p) ); @@ -789,7 +814,7 @@ Gia_Man_t * Gia_ManEquivReduce2( Gia_Man_t * p ) break; if ( i == Gia_ManObjNum(p) ) return Gia_ManDup( p ); - vMap = Gia_ManChoiceMinLevel( p ); + vMap = fRandom ? NULL : Gia_ManChoiceMinLevel( p ); Gia_ManSetPhase( p ); pNew = Gia_ManStart( Gia_ManObjNum(p) ); pNew->pName = Abc_UtilStrsav( p->pName ); @@ -805,7 +830,7 @@ Gia_Man_t * Gia_ManEquivReduce2( Gia_Man_t * p ) pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); Gia_ManHashStop( pNew ); Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) ); - Vec_IntFree( vMap ); + Vec_IntFreeP( &vMap ); return pNew; } diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index c1e90a4ed..4c540b383 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -44103,14 +44103,14 @@ usage: ***********************************************************************/ int Abc_CommandAbc9Dch( Abc_Frame_t * pAbc, int argc, char ** argv ) { - extern Gia_Man_t * Gia_ManEquivReduce2( Gia_Man_t * p ); + extern Gia_Man_t * Gia_ManEquivReduce2( Gia_Man_t * p, int fRandom ); Gia_Man_t * pTemp; Dch_Pars_t Pars, * pPars = &Pars; - int c, fMinLevel = 0, fEquiv = 0; + int c, fMinLevel = 0, fEquiv = 0, fRandom = 0; // set defaults Dch_ManSetDefaultParams( pPars ); Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "WCSsptfremgcxyvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "WCSsptfremngcxyvh" ) ) != EOF ) { switch ( c ) { @@ -44168,6 +44168,9 @@ int Abc_CommandAbc9Dch( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'm': fMinLevel ^= 1; break; + case 'n': + fRandom ^= 1; + break; case 'g': pPars->fUseGia ^= 1; break; @@ -44212,14 +44215,14 @@ int Abc_CommandAbc9Dch( Abc_Frame_t * pAbc, int argc, char ** argv ) { pTemp = Gia_ManPerformDch( pAbc->pGia, pPars ); Abc_FrameUpdateGia( pAbc, pTemp ); - if ( fMinLevel ) - pTemp = Gia_ManEquivReduce2( pAbc->pGia ); + if ( fMinLevel || fRandom ) + pTemp = Gia_ManEquivReduce2( pAbc->pGia, fRandom ); } Abc_FrameUpdateGia( pAbc, pTemp ); return 0; usage: - Abc_Print( -2, "usage: &dch [-WCS num] [-sptfremgcxyvh]\n" ); + Abc_Print( -2, "usage: &dch [-WCS num] [-sptfremngcxyvh]\n" ); Abc_Print( -2, "\t computes structural choices using a new approach\n" ); Abc_Print( -2, "\t-W num : the max number of simulation words [default = %d]\n", pPars->nWords ); Abc_Print( -2, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit ); @@ -44230,7 +44233,8 @@ usage: Abc_Print( -2, "\t-f : toggle using lighter logic synthesis [default = %s]\n", pPars->fLightSynth? "yes": "no" ); Abc_Print( -2, "\t-r : toggle skipping choices with redundant support [default = %s]\n", pPars->fSkipRedSupp? "yes": "no" ); Abc_Print( -2, "\t-e : toggle computing and merging equivalences [default = %s]\n", fEquiv? "yes": "no" ); - Abc_Print( -2, "\t-m : toggle minimizing logic level after merging equivalences [default = %s]\n", fMinLevel? "yes": "no" ); + Abc_Print( -2, "\t-m : toggle minimizing logic level after merging equivalences [default = %s]\n", fRandom? "yes": "no" ); + Abc_Print( -2, "\t-n : toggle selecting random choices while merging equivalences [default = %s]\n", fMinLevel? "yes": "no" ); Abc_Print( -2, "\t-g : toggle using GIA to prove equivalences [default = %s]\n", pPars->fUseGia? "yes": "no" ); Abc_Print( -2, "\t-c : toggle using circuit-based SAT vs. MiniSat [default = %s]\n", pPars->fUseCSat? "yes": "no" ); Abc_Print( -2, "\t-x : toggle using new choice computation [default = %s]\n", pPars->fUseNew? "yes": "no" );