From 35a1bbbdb4943bf1436984148728aa14563b9aa8 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Fri, 9 Aug 2024 18:33:36 -0700 Subject: [PATCH] Ongoing development related to Boolean decomposition. --- src/aig/gia/giaClp.c | 100 +++++++++++++++++++++- src/base/abci/abc.c | 21 ++--- src/bdd/dsd/dsd.h | 4 + src/bdd/dsd/dsdTree.c | 189 ++++++++++++++++++++++++++++++++++++++++++ 4 files changed, 303 insertions(+), 11 deletions(-) diff --git a/src/aig/gia/giaClp.c b/src/aig/gia/giaClp.c index feadd38d7..5102d4973 100644 --- a/src/aig/gia/giaClp.c +++ b/src/aig/gia/giaClp.c @@ -404,6 +404,41 @@ void Gia_ManCollapseTestTest( Gia_Man_t * p ) Gia_ManStop( pNew ); } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_ManPrintDsdOne( Dsd_Manager_t * pManDsd, int Output, int OffSet ) +{ + Vec_Str_t * vStr = Vec_StrAlloc( 100 ); + Dsd_TreePrint4( vStr, pManDsd, Output ); + for ( int i = 0; i < OffSet; i++ ) + printf( " " ); + printf( "Supp %2d nDsd %2d %s\n", Dsd_TreeSuppSize(pManDsd, Output), Dsd_TreeNonDsdMax(pManDsd, Output), Vec_StrArray(vStr) ); + Vec_StrFree( vStr ); + fflush( stdout ); +} +void Gia_ManPrintDsd( Dsd_Manager_t * pManDsd, int Output, int nOutputs, int OffSet ) +{ + if ( Output == -1 ) + { + for ( int i = 0; i < nOutputs; i++ ) + Gia_ManPrintDsdOne( pManDsd, i, OffSet ); + } + else + { + assert( Output >= 0 && Output < nOutputs ); + Gia_ManPrintDsdOne( pManDsd, Output, OffSet ); + } +} + void Gia_ManCheckDsd( Gia_Man_t * p, int OffSet, int fVerbose ) { DdManager * dd; @@ -425,7 +460,8 @@ void Gia_ManCheckDsd( Gia_Man_t * p, int OffSet, int fVerbose ) Cudd_Quit( dd ); return; } - Dsd_Decompose( pManDsd, (DdNode **)vFuncs->pArray, Gia_ManCoNum(p) ); + Dsd_Decompose( pManDsd, (DdNode **)Vec_PtrArray(vFuncs), Vec_PtrSize(vFuncs) ); + if ( fVerbose ) { Vec_Ptr_t * vNamesCi = Gia_GetFakeNames( Gia_ManCiNum(p) ); @@ -436,13 +472,75 @@ void Gia_ManCheckDsd( Gia_Man_t * p, int OffSet, int fVerbose ) Vec_PtrFreeFree( vNamesCi ); Vec_PtrFreeFree( vNamesCo ); } + else + Gia_ManPrintDsd( pManDsd, 0, Vec_PtrSize(vFuncs), 0 ); + Dsd_ManagerStop( pManDsd ); Gia_ManCollapseDeref( dd, vFuncs ); Extra_StopManager( dd ); } +Vec_Ptr_t * Gia_ManRecurDsdCof( DdManager * dd, Vec_Ptr_t * vFuncs, int iVar ) +{ + Vec_Ptr_t * vNew = Vec_PtrAlloc( 2 * Vec_PtrSize(vFuncs) ); DdNode * bFunc; int i; + Vec_PtrForEachEntry( DdNode *, vFuncs, bFunc, i ) { + DdNode * bCof0 = Cudd_Cofactor( dd, bFunc, Cudd_Not(Cudd_bddIthVar(dd, iVar)) ); Cudd_Ref( bCof0 ); + DdNode * bCof1 = Cudd_Cofactor( dd, bFunc, Cudd_bddIthVar(dd, iVar) ); Cudd_Ref( bCof1 ); + Vec_PtrPush( vNew, bCof0 ); + Vec_PtrPush( vNew, bCof1 ); + } + return vNew; +} void Gia_ManRecurDsd( Gia_Man_t * p, int fVerbose ) { + DdManager * dd; + Dsd_Manager_t * pManDsd; + Vec_Ptr_t * vFuncs, * vAux; + dd = Cudd_Init( Gia_ManCiNum(p), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 ); + Cudd_AutodynEnable( dd, CUDD_REORDER_SYMM_SIFT ); + vFuncs = Gia_ManCollapse( p, dd, 10000, 0 ); + Cudd_AutodynDisable( dd ); + if ( vFuncs == NULL ) + { + Extra_StopManager( dd ); + return; + } + pManDsd = Dsd_ManagerStart( dd, Gia_ManCiNum(p), 0 ); + if ( pManDsd == NULL ) + { + Gia_ManCollapseDeref( dd, vFuncs ); + Cudd_Quit( dd ); + return; + } + Dsd_Decompose( pManDsd, (DdNode **)Vec_PtrArray(vFuncs), Vec_PtrSize(vFuncs) ); + + printf( "Function:\n" ); + Gia_ManPrintDsd( pManDsd, 0, Vec_PtrSize(vFuncs), 0 ); + + for ( int i = 0; i < 5 && Dsd_TreeNonDsdMax(pManDsd, -1) > 0; i++ ) + { + int v, iBestV = -1, DsdMin = ABC_INFINITY, SuppMin = ABC_INFINITY; + for ( v = 0; v < Gia_ManCiNum(p); v++ ) + { + Vec_Ptr_t * vTemp = Gia_ManRecurDsdCof( dd, vFuncs, v ); + Dsd_Decompose( pManDsd, (DdNode **)Vec_PtrArray(vTemp), Vec_PtrSize(vTemp) ); + int DsdCur = Dsd_TreeNonDsdMax( pManDsd, -1 ); + int SuppCur = Dsd_TreeSuppSize( pManDsd, -1 ); + if ( DsdMin > DsdCur || (DsdMin == DsdCur && SuppMin > SuppCur) ) + DsdMin = DsdCur, SuppMin = SuppCur, iBestV = v; + Gia_ManCollapseDeref( dd, vTemp ); + } + assert( iBestV >= 0 ); + vFuncs = Gia_ManRecurDsdCof( dd, vAux = vFuncs, iBestV ); + Gia_ManCollapseDeref( dd, vAux ); + printf( "Cofactoring variable %c:\n", (int)(iBestV >= 26 ? 'A' - 26 : 'a') + iBestV ); + Dsd_Decompose( pManDsd, (DdNode **)Vec_PtrArray(vFuncs), Vec_PtrSize(vFuncs) ); + Gia_ManPrintDsd( pManDsd, -1, Vec_PtrSize(vFuncs), (i+1)*2 ); + } + + Dsd_ManagerStop( pManDsd ); + Gia_ManCollapseDeref( dd, vFuncs ); + Extra_StopManager( dd ); } #else diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 4daaccecd..346a1ae92 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -54145,13 +54145,14 @@ int Abc_CommandAbc9DsdInfo( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( fDsd ) { if ( iIn == -1 ) { - Gia_ManCheckDsd( pAbc->pGia, 0, 1 ); + printf( "Function = " ); + Gia_ManCheckDsd( pAbc->pGia, 0, fVerbose ); if ( fAll ) { for ( iIn = 0; iIn < Gia_ManPiNum(pAbc->pGia); iIn++ ) for ( c = 0; c < 2; c++ ) { Gia_Man_t * pTemp = Gia_ManDupCofactorVar( pAbc->pGia, iIn, c ); - printf( "%s %2d = %d:\n", c ? " " : "Var", iIn, c ); - Gia_ManCheckDsd( pTemp, 12, 1 ); + printf( "Cof(%c=%d) = ", 'a' + iIn, c ); + Gia_ManCheckDsd( pTemp, 12, fVerbose ); Gia_ManStop( pTemp ); } } @@ -54159,14 +54160,14 @@ int Abc_CommandAbc9DsdInfo( Abc_Frame_t * pAbc, int argc, char ** argv ) } for ( c = 0; c < 2; c++ ) { Gia_Man_t * pTemp = Gia_ManDupCofactorVar( pAbc->pGia, iIn, c ); - printf( "Var %2d Cof %d:\n", iIn, c ); - Gia_ManCheckDsd( pTemp, 0, 1 ); + printf( " Cof(%c=%d) = ", 'a' + iIn, c ); + Gia_ManCheckDsd( pTemp, 0, fVerbose ); if ( fAll ) { - for ( int iIn = 0; iIn < Gia_ManPiNum(pAbc->pGia); iIn++ ) - for ( int c = 0; c < 2; c++ ) { - Gia_Man_t * pTemp2 = Gia_ManDupCofactorVar( pTemp, iIn, c ); - printf( "%s %2d = %d:\n", c ? " " : "Var", iIn, c ); - Gia_ManCheckDsd( pTemp2, 12, 1 ); + for ( int iIn2 = 0; iIn2 < Gia_ManPiNum(pAbc->pGia); iIn2++ ) if ( iIn2 != iIn ) + for ( int c2 = 0; c2 < 2; c2++ ) { + Gia_Man_t * pTemp2 = Gia_ManDupCofactorVar( pTemp, iIn2, c2 ); + printf( "Cof(%c=%d,%c=%d) = ", 'a' + iIn, c, 'a' + iIn2, c2 ); + Gia_ManCheckDsd( pTemp2, 12, fVerbose ); Gia_ManStop( pTemp2 ); } } diff --git a/src/bdd/dsd/dsd.h b/src/bdd/dsd/dsd.h index 2990c0259..e8d017fe0 100644 --- a/src/bdd/dsd/dsd.h +++ b/src/bdd/dsd/dsd.h @@ -117,7 +117,11 @@ extern Dsd_Node_t ** Dsd_TreeCollectNodesDfs( Dsd_Manager_t * dMan, int * pnNo extern Dsd_Node_t ** Dsd_TreeCollectNodesDfsOne( Dsd_Manager_t * pDsdMan, Dsd_Node_t * pNode, int * pnNodes ); extern void Dsd_TreePrint( FILE * pFile, Dsd_Manager_t * dMan, char * pInputNames[], char * pOutputNames[], int fShortNames, int Output, int OffSet ); extern void Dsd_TreePrint2( FILE * pFile, Dsd_Manager_t * dMan, char * pInputNames[], char * pOutputNames[], int Output ); +extern void Dsd_TreePrint3( void * pStr, Dsd_Manager_t * pDsdMan, int Output ); +extern void Dsd_TreePrint4( void * pStr, Dsd_Manager_t * pDsdMan, int Output ); extern void Dsd_NodePrint( FILE * pFile, Dsd_Node_t * pNode ); +extern int Dsd_TreeNonDsdMax( Dsd_Manager_t * pDsdMan, int Output ); +extern int Dsd_TreeSuppSize( Dsd_Manager_t * pDsdMan, int Output ); /*=== dsdLocal.c =======================================================*/ extern DdNode * Dsd_TreeGetPrimeFunction( DdManager * dd, Dsd_Node_t * pNode ); diff --git a/src/bdd/dsd/dsdTree.c b/src/bdd/dsd/dsdTree.c index 42eee2cc5..1873ae0c1 100644 --- a/src/bdd/dsd/dsdTree.c +++ b/src/bdd/dsd/dsdTree.c @@ -627,6 +627,195 @@ void Dsd_TreeCollectNodesDfs_rec( Dsd_Node_t * pNode, Dsd_Node_t * ppNodes[], in ppNodes[ (*pnNodes)++ ] = pNode; } +/**Function************************************************************* + + Synopsis [Returns the size of the largest non-DSD block.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Dsd_TreeNonDsdMax_rec( Dsd_Node_t * pNode ) +{ + if ( pNode->Type == DSD_NODE_CONST1 ) + return 0; + if ( pNode->Type == DSD_NODE_BUF ) + return 0; + int MaxBlock = pNode->Type == DSD_NODE_PRIME ? pNode->nDecs : 0; + for ( int i = 0; i < pNode->nDecs; i++ ) + { + int MaxThis = Dsd_TreeNonDsdMax_rec( Dsd_Regular( pNode->pDecs[i] ) ); + MaxBlock = Abc_MaxInt( MaxBlock, MaxThis ); + } + return MaxBlock; +} +int Dsd_TreeNonDsdMax( Dsd_Manager_t * pDsdMan, int Output ) +{ + if ( Output == -1 ) + { + int i, Res = 0; + for ( i = 0; i < pDsdMan->nRoots; i++ ) + Res = Abc_MaxInt( Res, Dsd_TreeNonDsdMax_rec( Dsd_Regular( pDsdMan->pRoots[i] ) ) ); + return Res; + } + else + { + assert( Output >= 0 && Output < pDsdMan->nRoots ); + return Dsd_TreeNonDsdMax_rec( Dsd_Regular( pDsdMan->pRoots[Output] ) ); + } +} + +/**Function************************************************************* + + Synopsis [Returns the support size.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Dsd_TreeSuppSize_rec( Dsd_Node_t * pNode ) +{ + if ( pNode->Type == DSD_NODE_CONST1 ) + return 0; + if ( pNode->Type == DSD_NODE_BUF ) + return 1; + int nSuppSize = 0; + for ( int i = 0; i < pNode->nDecs; i++ ) + nSuppSize += Dsd_TreeSuppSize_rec( Dsd_Regular( pNode->pDecs[i] ) ); + return nSuppSize; +} +int Dsd_TreeSuppSize( Dsd_Manager_t * pDsdMan, int Output ) +{ + if ( Output == -1 ) + { + int i, Res = 0; + for ( i = 0; i < pDsdMan->nRoots; i++ ) + Res += Dsd_TreeSuppSize_rec( Dsd_Regular( pDsdMan->pRoots[i] ) ); + return Res; + } + else + { + assert( Output >= 0 && Output < pDsdMan->nRoots ); + return Dsd_TreeSuppSize_rec( Dsd_Regular( pDsdMan->pRoots[Output] ) ); + } +} + +/**Function************************************************************* + + Synopsis [Prints the decompostion tree into a string.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Dsd_TreePrint3_rec( Vec_Str_t * p, Dsd_Node_t * pNode ) +{ + if ( pNode->Type == DSD_NODE_BUF ) { + Vec_StrPush( p, (int)(pNode->S->index >= 26 ? 'A' - 26 : 'a') + pNode->S->index ); + return; + } + if ( pNode->Type == DSD_NODE_PRIME ) + Vec_StrPush( p, '{' ); + else if ( pNode->Type == DSD_NODE_OR ) + Vec_StrPush( p, '(' ); + else if ( pNode->Type == DSD_NODE_EXOR ) + Vec_StrPush( p, '[' ); + else assert( 0 ); + for ( int i = 0; i < pNode->nDecs; i++ ) + { + Dsd_Node_t * pInput = Dsd_Regular( pNode->pDecs[i] ); + if ( pInput != pNode->pDecs[i] ) + Vec_StrPush( p, '~' ); + Dsd_TreePrint3_rec( p, pInput ); + } + if ( pNode->Type == DSD_NODE_PRIME ) + Vec_StrPush( p, '}' ); + else if ( pNode->Type == DSD_NODE_OR ) + Vec_StrPush( p, ')' ); + else if ( pNode->Type == DSD_NODE_EXOR ) + Vec_StrPush( p, ']' ); + else assert( 0 ); +} +void Dsd_TreePrint3( void * pStr, Dsd_Manager_t * pDsdMan, int Output ) +{ + Vec_Str_t * p = (Vec_Str_t *)pStr; + assert( Output >= 0 && Output < pDsdMan->nRoots ); + Dsd_Node_t * pNode = Dsd_Regular( pDsdMan->pRoots[Output] ); + int fCompl = pNode != pDsdMan->pRoots[Output]; + if ( pNode->Type == DSD_NODE_CONST1 ) + Vec_StrPush( p, fCompl ? '0' : '1' ); + else { + if ( fCompl ) + Vec_StrPush( p, '~' ); + Dsd_TreePrint3_rec( p, pNode ); + } + Vec_StrPush( p, '\0' ); +} + +/**Function************************************************************* + + Synopsis [Prints the decompostion tree into a string.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Dsd_TreePrint4_rec( Vec_Str_t * p, Dsd_Node_t * pNode ) +{ + if ( pNode->Type == DSD_NODE_BUF ) { + Vec_StrPush( p, (int)(pNode->S->index >= 26 ? 'A' - 26 : 'a') + pNode->S->index ); + return; + } + if ( pNode->Type == DSD_NODE_PRIME ) + Vec_StrPush( p, '{' ); + else if ( pNode->Type == DSD_NODE_OR ) + Vec_StrPush( p, '(' ); + else if ( pNode->Type == DSD_NODE_EXOR ) + Vec_StrPush( p, '[' ); + else assert( 0 ); + for ( int i = 0; i < pNode->nDecs; i++ ) + { + Dsd_Node_t * pInput = Dsd_Regular( pNode->pDecs[i] ); + if ( (pInput != pNode->pDecs[i]) ^ (pNode->Type == DSD_NODE_OR) ^ (pInput->Type == DSD_NODE_OR) ) + Vec_StrPush( p, '~' ); + Dsd_TreePrint4_rec( p, pInput ); + } + if ( pNode->Type == DSD_NODE_PRIME ) + Vec_StrPush( p, '}' ); + else if ( pNode->Type == DSD_NODE_OR ) + Vec_StrPush( p, ')' ); + else if ( pNode->Type == DSD_NODE_EXOR ) + Vec_StrPush( p, ']' ); + else assert( 0 ); +} +void Dsd_TreePrint4( void * pStr, Dsd_Manager_t * pDsdMan, int Output ) +{ + Vec_Str_t * p = (Vec_Str_t *)pStr; + assert( Output >= 0 && Output < pDsdMan->nRoots ); + Dsd_Node_t * pNode = Dsd_Regular( pDsdMan->pRoots[Output] ); + int fCompl = pNode != pDsdMan->pRoots[Output]; + if ( pNode->Type == DSD_NODE_CONST1 ) + Vec_StrPush( p, fCompl ? '0' : '1' ); + else { + if ( fCompl ^ (pNode->Type == DSD_NODE_OR) ) + Vec_StrPush( p, '~' ); + Dsd_TreePrint4_rec( p, pNode ); + } + Vec_StrPush( p, '\0' ); +} + /**Function************************************************************* Synopsis [Prints the decompostion tree into file.]