From a511d753a66048ccfb90006b248285ea69fd04da Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sun, 20 Jul 2025 18:29:20 -0700 Subject: [PATCH] Improvements to "lutcasdec". --- src/base/abci/abc.c | 38 ++++- src/base/abci/abcCas.c | 16 +- src/misc/util/utilBSet.c | 306 +++++++++++++++++++++++++++++--------- src/misc/util/utilTruth.h | 14 ++ 4 files changed, 288 insertions(+), 86 deletions(-) diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 40b362c60..c68bcc870 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -9182,12 +9182,12 @@ usage: int Abc_CommandLutCasDec( Abc_Frame_t * pAbc, int argc, char ** argv ) { extern Abc_Ntk_t * Abc_NtkLutCascadeGen( int nLutSize, int nStages, int nRails, int nShared, int fVerbose ); - extern Abc_Ntk_t * Abc_NtkLutCascadeOne( Abc_Ntk_t * pNtk, int nLutSize, int nLuts, int nRails, int nIters, int nJRatio, int nZParam, int fXRail, int Seed, int fVerbose, int fVeryVerbose, char * pGuide ); - extern void Abc_NtkLutCascadeFile( char * pFileName, int nVarNum, int nLutSize, int nLuts, int nRails, int nIters, int nJRatio, int nZParam, int Seed, int fVerbose, int fVeryVerbose, int fPrintMyu, int fPrintLev, int fXRail ); + extern Abc_Ntk_t * Abc_NtkLutCascadeOne( Abc_Ntk_t * pNtk, int nLutSize, int nLuts, int nRails, int nIters, int nJRatio, int nZParam, int fXRail, int Seed, int fVerbose, int fVeryVerbose, char * pGuide, int nSubsets, int nBest ); + extern void Abc_NtkLutCascadeFile( char * pFileName, int nVarNum, int nLutSize, int nLuts, int nRails, int nIters, int nJRatio, int nZParam, int Seed, int fVerbose, int fVeryVerbose, int fPrintMyu, int fPrintLev, int fXRail, int nSubsets, int nBest ); Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc), * pNtkRes; char * pGuide = NULL, * pFileName = NULL; - int c, nVarNum = -1, nLutSize = 6, nStages = 8, nRails = 1, nShared = 2, Seed = 0, nIters = 10, nJRatio = -1, nZParam = 5, fGen = 0, fPrintMyu = 0, fPrintLev = 0, fXRail = 0, fVerbose = 0, fVeryVerbose = 0; + int c, nVarNum = -1, nLutSize = 6, nStages = 8, nRails = 1, nShared = 2, Seed = 0, nIters = 10, nJRatio = -1, nZParam = 5, fGen = 0, fPrintMyu = 0, fPrintLev = 0, fXRail = 0, nSubsets = 0, nBest = 0, fVerbose = 0, fVeryVerbose = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "KMRSCIZNFgmlxvwh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "KMRSCIZNGBFgmlxvwh" ) ) != EOF ) { switch ( c ) { @@ -9288,6 +9288,28 @@ int Abc_CommandLutCasDec( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( nVarNum < 0 ) goto usage; break; + case 'G': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-G\" should be followed by an integer.\n" ); + goto usage; + } + nSubsets = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nSubsets < 0 ) + goto usage; + break; + case 'B': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-B\" should be followed by an integer.\n" ); + goto usage; + } + nBest = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nBest < 0 ) + goto usage; + break; case 'F': if ( globalUtilOptind >= argc ) { @@ -9328,7 +9350,7 @@ int Abc_CommandLutCasDec( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( -1, "The number of variables should be given on the command line using switch \"-N \".\n" ); return 1; } - Abc_NtkLutCascadeFile( pFileName, nVarNum, nLutSize, nStages, nRails, nIters, nJRatio, nZParam, Seed, fVerbose, fVeryVerbose, fPrintMyu, fPrintLev, fXRail ); + Abc_NtkLutCascadeFile( pFileName, nVarNum, nLutSize, nStages, nRails, nIters, nJRatio, nZParam, Seed, fVerbose, fVeryVerbose, fPrintMyu, fPrintLev, fXRail, nSubsets, nBest ); return 0; } if ( fGen ) @@ -9365,7 +9387,7 @@ int Abc_CommandLutCasDec( Abc_Frame_t * pAbc, int argc, char ** argv ) } if ( argc == globalUtilOptind + 1 ) pGuide = argv[globalUtilOptind]; - pNtkRes = Abc_NtkLutCascadeOne( pNtk, nLutSize, nStages, nRails, nIters, nJRatio, nZParam, fXRail, Seed, fVerbose, fVeryVerbose, pGuide ); + pNtkRes = Abc_NtkLutCascadeOne( pNtk, nLutSize, nStages, nRails, nIters, nJRatio, nZParam, fXRail, Seed, fVerbose, fVeryVerbose, pGuide, nSubsets, nBest ); if ( pNtkRes == NULL ) { Abc_Print( -1, "LUT cascade mapping failed.\n" ); @@ -9375,7 +9397,7 @@ int Abc_CommandLutCasDec( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: lutcasdec [-KMRCSIZN ] [-F ] [-gmlxvwh]\n" ); + Abc_Print( -2, "usage: lutcasdec [-KMRCSIZNGB ] [-F ] [-gmlxvwh]\n" ); Abc_Print( -2, "\t decomposes the primary output functions into LUT cascades\n" ); Abc_Print( -2, "\t-K : the number of LUT inputs [default = %d]\n", nLutSize ); Abc_Print( -2, "\t-M : the maximum delay (the number of stages) [default = %d]\n", nStages ); @@ -9386,6 +9408,8 @@ usage: //Abc_Print( -2, "\t-J : toggle using random bound-set every this many iterations [default = %d]\n", nJRatio ); Abc_Print( -2, "\t-Z : the number determining how many decompositions are tried [default = %d]\n", nZParam ); Abc_Print( -2, "\t-N : the number of support variables (for truth table files only) [default = unused]\n" ); + Abc_Print( -2, "\t-G : the number of variable groups to consider [default = %d]\n", nSubsets ); + Abc_Print( -2, "\t-B : the number of best groups to use as bound-sets [default = %d]\n", nBest ); Abc_Print( -2, "\t-F : a text file with truth tables in hexadecimal listed one per line\n"); Abc_Print( -2, "\t-g : toggle generating random cascade with these parameters [default = %s]\n", fGen? "yes": "no" ); Abc_Print( -2, "\t-m : toggle printing column multiplicity statistics [default = %s]\n", fPrintMyu? "yes": "no" ); diff --git a/src/base/abci/abcCas.c b/src/base/abci/abcCas.c index 0abb679d3..07b738423 100644 --- a/src/base/abci/abcCas.c +++ b/src/base/abci/abcCas.c @@ -742,9 +742,9 @@ typedef struct Abc_BSEval_t_ Abc_BSEval_t; extern Abc_BSEval_t * Abc_BSEvalAlloc(); extern void Abc_BSEvalFree( Abc_BSEval_t * p ); -word * Abc_LutCascadeDec( Abc_BSEval_t * p, char * pGuide, word * pTruth, int nVarsOrig, Vec_Int_t * vVarIDs, int nRails, int nLutSize, int nStages, int fUseRand, int nZParam, int fXRail, int fVerbose, int * pnStages, int * pMyu ) +word * Abc_LutCascadeDec( Abc_BSEval_t * p, char * pGuide, word * pTruth, int nVarsOrig, Vec_Int_t * vVarIDs, int nRails, int nLutSize, int nStages, int fUseRand, int nZParam, int fXRail, int fVerbose, int * pnStages, int * pMyu, int nSubsets, int nBest ) { - extern Vec_Wrd_t * Abc_TtFindBVarsSVars2( Abc_BSEval_t * p, word * pTruth, int nVars, int nCVars, int nRails, int nLutSize, int fVerbose, int * pMyu, int nMyuIncrease ); + extern Vec_Wrd_t * Abc_TtFindBVarsSVars2( Abc_BSEval_t * p, word * pTruth, int nVars, int nCVars, int nRails, int nLutSize, int fVerbose, int * pMyu, int nMyuIncrease, int nSubsets, int nBest ); word * pRes = NULL; int i, nRVars = 0, nVars = Vec_IntSize(vVarIDs); Vec_Wrd_t * vFuncs[3] = { Vec_WrdStart(Abc_TtWordNum(nVars)), Vec_WrdAlloc(0), Vec_WrdAlloc(0) }; Abc_TtCopy( Vec_WrdArray(vFuncs[0]), pTruth, Abc_TtWordNum(nVars), 0 ); @@ -752,7 +752,7 @@ word * Abc_LutCascadeDec( Abc_BSEval_t * p, char * pGuide, word * pTruth, int nV if ( pnStages ) *pnStages = 0; for ( i = 0; Vec_IntSize(vVarIDs) > nLutSize; i++ ) { int nRVarsOld = nRVars; - Vec_Wrd_t * vGuides = Abc_TtFindBVarsSVars2( p, Vec_WrdArray(vFuncs[0]), Vec_IntSize(vVarIDs), nRVars, nRails, nLutSize, fVerbose, pMyu, nZParam ); + Vec_Wrd_t * vGuides = Abc_TtFindBVarsSVars2( p, Vec_WrdArray(vFuncs[0]), Vec_IntSize(vVarIDs), nRVars, nRails, nLutSize, fVerbose, pMyu, nZParam, nSubsets, nBest ); if ( vGuides ) { int iEntry = fUseRand ? Abc_Random(0) % Vec_WrdSize(vGuides) : 0; nRVars = Abc_LutCascadeDecStage( Vec_WrdEntry(vGuides, iEntry), pGuide, i, vFuncs, vVarIDs, nRVarsOld, nRails, nLutSize, nZParam, fVerbose, vCas, i ? NULL : pMyu ); @@ -766,7 +766,7 @@ word * Abc_LutCascadeDec( Abc_BSEval_t * p, char * pGuide, word * pTruth, int nV nRVars = -1; } if ( fXRail && nRVars == -1 && Vec_IntSize(vVarIDs) > nLutSize-1 ) { - Vec_Wrd_t * vGuides = Abc_TtFindBVarsSVars2( p, Vec_WrdArray(vFuncs[0]), Vec_IntSize(vVarIDs), nRVarsOld, nRails+1, nLutSize-1, fVerbose, pMyu, nZParam ); + Vec_Wrd_t * vGuides = Abc_TtFindBVarsSVars2( p, Vec_WrdArray(vFuncs[0]), Vec_IntSize(vVarIDs), nRVarsOld, nRails+1, nLutSize-1, fVerbose, pMyu, nZParam, nSubsets, nBest ); if ( vGuides ) { int iEntry = fUseRand ? Abc_Random(0) % Vec_WrdSize(vGuides) : 0; nRVars = Abc_LutCascadeDecStage( Vec_WrdEntry(vGuides, iEntry), pGuide, i, vFuncs, vVarIDs, nRVarsOld, nRails+1, nLutSize-1, nZParam, fVerbose, vCas, NULL ); @@ -890,7 +890,7 @@ Abc_Ntk_t * Abc_NtkLutCascade( Abc_Ntk_t * pNtk, int nLutSize, int nStages, int Gia_ManStop( pGia ); return pNew; } -Abc_Ntk_t * Abc_NtkLutCascadeOne( Abc_Ntk_t * pNtk, int nLutSize, int nStages, int nRails, int nIters, int nJRatio, int nZParam, int fXRail, int Seed, int fVerbose, int fVeryVerbose, char * pGuide ) +Abc_Ntk_t * Abc_NtkLutCascadeOne( Abc_Ntk_t * pNtk, int nLutSize, int nStages, int nRails, int nIters, int nJRatio, int nZParam, int fXRail, int Seed, int fVerbose, int fVeryVerbose, char * pGuide, int nSubsets, int nBest ) { extern Gia_Man_t * Abc_NtkStrashToGia( Abc_Ntk_t * pNtk ); int i, nWords = Abc_TtWordNum(Abc_NtkCiNum(pNtk)); @@ -919,7 +919,7 @@ Abc_Ntk_t * Abc_NtkLutCascadeOne( Abc_Ntk_t * pNtk, int nLutSize, int nStages, i printf( ".\n" ); } - word * pLuts = Abc_LutCascadeDec( p, pGuide, pTruth1, Abc_NtkCiNum(pNtk), vVarIDs, nRails, nLutSize, nStages, (int)(Iter >= 0), nZParam, fXRail, fVeryVerbose, NULL, NULL ); + word * pLuts = Abc_LutCascadeDec( p, pGuide, pTruth1, Abc_NtkCiNum(pNtk), vVarIDs, nRails, nLutSize, nStages, (int)(Iter >= 0), nZParam, fXRail, fVeryVerbose, NULL, NULL, nSubsets, nBest ); pNew = pLuts ? Abc_NtkLutCascadeFromLuts( pLuts, Abc_NtkCiNum(pNtk), pNtk, nLutSize, fVerbose ) : NULL; Vec_IntFree( vVarIDs ); @@ -1434,7 +1434,7 @@ Vec_Wrd_t * Abc_NtkLutCasReadTruths( char * pFileName, int nVarsOrig ) SeeAlso [] ***********************************************************************/ -void Abc_NtkLutCascadeFile( char * pFileName, int nVarsOrig, int nLutSize, int nStages, int nRails, int nIters, int nJRatio, int nZParam, int Seed, int fVerbose, int fVeryVerbose, int fPrintMyu, int fPrintLev, int fXRail ) +void Abc_NtkLutCascadeFile( char * pFileName, int nVarsOrig, int nLutSize, int nStages, int nRails, int nIters, int nJRatio, int nZParam, int Seed, int fVerbose, int fVeryVerbose, int fPrintMyu, int fPrintLev, int fXRail, int nSubsets, int nBest ) { abctime clkStart = Abc_Clock(); int i, nErrors = 0, Sum = 0, nStageCount = 0, MyuMin = 0, nTotalLuts = 0, nWords = Abc_TtWordNum(nVarsOrig); @@ -1483,7 +1483,7 @@ void Abc_NtkLutCascadeFile( char * pFileName, int nVarsOrig, int nLutSize, int n printf( "Decomposing %d-var function into %d-rail cascade of %d-LUTs.\n", nVars, nRails, nLutSize ); } - word * pLuts = Abc_LutCascadeDec( p, NULL, pTruth, nVarsOrig, vVarIDs, nRails, nLutSize, nStages, (int)(Iter >= 0), nZParam, fXRail, fVeryVerbose, &nStageCount, &MyuMin ); + word * pLuts = Abc_LutCascadeDec( p, NULL, pTruth, nVarsOrig, vVarIDs, nRails, nLutSize, nStages, (int)(Iter >= 0), nZParam, fXRail, fVeryVerbose, &nStageCount, &MyuMin, nSubsets, nBest ); Vec_IntFree( vVarIDs ); if ( MyuMin < 50 ) MyuStats[MyuMin]++, IterReal++; if ( pLuts == NULL ) { diff --git a/src/misc/util/utilBSet.c b/src/misc/util/utilBSet.c index 80c9974b7..4fbd73393 100644 --- a/src/misc/util/utilBSet.c +++ b/src/misc/util/utilBSet.c @@ -1006,11 +1006,125 @@ word Abc_BSEvalEncode( int * pPermBest, int nVars, int nLutSize, int Shared, int mSVars |= (word)1 << (nVars-nLutSize+v); return ((word)MyuMin << 48) | (mSVars << 24) | mBVars; } -Vec_Wrd_t * Abc_TtFindBVarsSVars2( Abc_BSEval_t * p, word * pTruth, int nVars, int nCVars, int nRails, int nLutSize, int fVerbose, int * pMyu, int nMyuIncrease ) + + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Wec_t * Abc_BSFind( Vec_Int_t * vVars, int nLutSize, int nSubsets ) +{ + assert( Vec_IntSize(vVars) > nLutSize ); + Vec_Wec_t * vRes = Vec_WecAlloc( nSubsets ); int i; + for ( i = 0; i < nSubsets; i++ ) { + Vec_Int_t * vNew = Vec_WecPushLevel( vRes ); + while ( Vec_IntSize(vNew) < nLutSize ) + Vec_IntPushUniqueOrder( vNew, Vec_IntEntry(vVars, Abc_Random(0)%Vec_IntSize(vVars)) ); + } + return vRes; +} +Vec_Int_t * Abc_BSFindNextVars( Vec_Wec_t * vPrev, int nLutSize, int nSubsets, int nBest ) +{ + assert( Vec_WecSize(vPrev) == nSubsets ); + assert( Vec_IntSize(Vec_WecEntry(vPrev,0)) == nLutSize + 1 ); + Vec_Int_t * vVars = Vec_IntAlloc( 100 ); + Vec_Int_t * vLevel; int i, k, Var; + Vec_WecForEachLevelStop( vPrev, vLevel, i, nBest ) + Vec_IntForEachEntry( vLevel, Var, k ) + if ( k < nLutSize ) + Vec_IntPush( vVars, Var ); + Vec_IntUniqify( vVars ); + return vVars; +} +// this procedure considers boundsets in vSets and adds CM as the last entry in each one +void Abc_BSEvalSet( Abc_BSEval_t * p, Vec_Wec_t * vSets, word * pTruth, int nVars, int nCVars, int nLutSize ) +{ + int nWords = Abc_TtWordNum(nVars); + word * pCopy = ABC_ALLOC( word, nWords ); + Abc_TtCopy( pCopy, pTruth, nWords, 0 ); + + int i, k, Var, Pla2Var[32], Var2Pla[32]; + for ( i = 0; i < nVars; i++ ) + Pla2Var[i] = Var2Pla[i] = i; + + Vec_Int_t * vLevel; + Vec_WecForEachLevel( vSets, vLevel, i ) { + assert( Vec_IntSize(vLevel) == nLutSize-nCVars ); + Vec_IntForEachEntry( vLevel, Var, k ) + Abc_TtMoveVar( pCopy, nVars, Var2Pla, Pla2Var, Var, nVars - nLutSize + k ); + int MyuThis = Abc_TtGetCM( pCopy, nVars, nVars-nLutSize, p->vCounts, p->vTable, p->vStore, p->vUsed, 0 ); + Vec_IntPush( vLevel, MyuThis ); + } + + for ( i = 0; i < nVars; i++ ) + Abc_TtMoveVar( pCopy, nVars, Var2Pla, Pla2Var, i, i ); + if ( !Abc_TtEqual(pCopy, pTruth, nWords) ) + printf( "Internal truth table check failed.\n" ); +} +void Vec_WecAppend( Vec_Wec_t * vBase, Vec_Wec_t * vNew ) +{ + Vec_Int_t * vLevel; int i; + Vec_WecForEachLevel( vNew, vLevel, i ) + Vec_IntAppend( Vec_WecPushLevel(vBase), vLevel ); +} +Vec_Wec_t * Abc_TtFindBVars3( Abc_BSEval_t * p, word * pTruth, int nVars, int nCVars, int nRails, int nLutSize, int fVerbose, int * pMyu, int nMyuIncrease, int nSubsets, int nBest ) +{ + Vec_Wec_t * vAllSets = Vec_WecAlloc( 1000 ); + Vec_Wec_t * vSets = NULL; + for ( int Iter = 0; Iter < 3; Iter++ ) { + Vec_Int_t * vVars = NULL; + if ( Iter == 0 ) + vVars = Vec_IntStartNatural( nVars-nCVars ); + else + vVars = Abc_BSFindNextVars( vSets, nLutSize-nCVars, nSubsets, nBest ); + if ( Vec_IntSize(vVars) <= nLutSize-nCVars ) + break; + Vec_WecFreeP( &vSets ); + vSets = Abc_BSFind( vVars, nLutSize-nCVars, nSubsets ); + Abc_BSEvalSet( p, vSets, pTruth, nVars, nCVars, nLutSize ); + Vec_WecSortByLastInt( vSets, 0 ); + Vec_WecAppend( vAllSets, vSets ); + if ( 0 ) + { + printf( "Iteration %d :\n", Iter ); + Vec_WecPrint( vSets, 0 ); + printf( "Variables: " ); + Vec_IntPrint( vVars ); + printf( "\n" ); + } + Vec_IntFree( vVars ); + } + Vec_WecFreeP( &vSets ); + //Vec_WecPrint( vAllSets, 0 ); + //Vec_WecFreeP( &vAllSets ); + return vAllSets; +} + + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Wrd_t * Abc_TtFindBVarsSVars2( Abc_BSEval_t * p, word * pTruth, int nVars, int nCVars, int nRails, int nLutSize, int fVerbose, int * pMyu, int nMyuIncrease, int nSubsets, int nBest ) { // Abc_BSEval_t * p = Abc_BSEvalAlloc(); int nFVars = nVars-nLutSize; int nPermVars = nVars-nCVars; + int nBSets = 0; if ( p->nVars != nPermVars ) { p->nVars = nPermVars; @@ -1041,80 +1155,130 @@ Vec_Wrd_t * Abc_TtFindBVarsSVars2( Abc_BSEval_t * p, word * pTruth, int nVars, i int nSetSizeBest = nVars; if ( pMyu ) *pMyu = 1 << nVars; - Vec_IntForEachEntryDouble( p->vPairs[p->nVars][p->nLVars], Var0, Var1, i ) { - int MyuThis = Abc_TtGetCM( pCopy, nVars, nFVars, p->vCounts, p->vTable, p->vStore, p->vUsed, 0 ); - MyuOrigBest = Abc_MinInt( MyuOrigBest, MyuThis ); - if ( pMyu ) *pMyu = Abc_MinInt( *pMyu, MyuThis ); - if ( fVerbose ) + if ( nSubsets && nBest && nVars > nLutSize+1 ) { + Vec_Wec_t * vAllSets = Abc_TtFindBVars3( p, pTruth, nVars, nCVars, nRails, nLutSize, fVerbose, pMyu, nMyuIncrease, nSubsets, nBest ); + Vec_WecSortByLastInt( vAllSets, 0 ); +// Vec_IntForEachEntryDouble( p->vPairs[p->nVars][p->nLVars], Var0, Var1, i ) { +// int MyuThis = Abc_TtGetCM( pCopy, nVars, nFVars, p->vCounts, p->vTable, p->vStore, p->vUsed, 0 ); + Vec_Int_t * vLevel; int Var; + Vec_WecForEachLevelStop( vAllSets, vLevel, i, nBest ) { - printf( "%3d : ", i/2 ); - for ( k = nCVars-1; k >= 0; k-- ) - printf( " %d", nVars-nCVars+k ); - printf( " " ); - for ( k = nPermVars-1; k >= nFVars; k-- ) - printf( " %d", Pla2Var[k] ); - printf( " " ); - for ( k = nFVars-1; k >= 0; k-- ) - printf( " %d", Pla2Var[k] ); - printf( " : Myu = %3d", MyuThis ); + int MyuThis = Vec_IntPop( vLevel ); + MyuOrigBest = Abc_MinInt( MyuOrigBest, MyuThis ); + if ( pMyu ) *pMyu = Abc_MinInt( *pMyu, MyuThis ); + + Vec_IntForEachEntry( vLevel, Var, k ) + Abc_TtMoveVar( pCopy, nVars, Var2Pla, Pla2Var, Var, nVars - nLutSize + k ); + //int MyuThis1 = Abc_TtGetCM( pCopy, nVars, nFVars, p->vCounts, p->vTable, p->vStore, p->vUsed, 0 ); + //assert( MyuThis1 == MyuThis ); + + if ( fVerbose ) + { + printf( "%3d : ", i/2 ); + for ( k = nCVars-1; k >= 0; k-- ) + printf( " %d", nVars-nCVars+k ); + printf( " " ); + for ( k = nPermVars-1; k >= nFVars; k-- ) + printf( " %d", Pla2Var[k] ); + printf( " " ); + for ( k = nFVars-1; k >= 0; k-- ) + printf( " %d", Pla2Var[k] ); + printf( " : Myu = %3d", MyuThis ); + } + if ( MyuThis <= MyuOrigBest + nMyuIncrease ) { + int Shared = 0, nSetSize = 0; + if ( MyuThis > 2 ) { + int SharedThis = 0, nSetSizeThis = 0; + int nRailsMin = 100; + for ( int r = 1; r <= nRails && nRailsMin > r; r++ ) { + int nRailsMinNew = Abc_SharedEvalBest( p, pCopy, nVars, nCVars, nFVars, MyuThis, r, 0, &SharedThis, &nSetSizeThis, p->pPat ); + if ( nRailsMinNew < 100 ) + nRailsMin = nRailsMinNew; + } + if ( fVerbose ) + printf( " RailsMyu = %3d. RailsMin = %3d. Shared = %2d. SetSize = %d.", Abc_Base2Log(MyuThis), nRailsMin, SharedThis, nSetSizeThis ); + if ( nRailsMin <= nRails ) { + MyuThis = 1 << nRailsMin; + Shared = SharedThis; + nSetSize = nSetSizeThis; + } + } + if ( MyuBest > MyuThis || (MyuBest == MyuThis && nSetSizeBest >= nSetSize) ) { + int fSave = (MyuBest == MyuThis && nSetSizeBest == nSetSize); + MyuBest = MyuThis; + nSetSizeBest = nSetSize; + word Result = Abc_BSEvalEncode( Pla2Var, nVars, nLutSize, Shared, MyuBest, nSetSize ); + if ( fSave ) + Vec_WrdPush( vRes, Result ); + else + Vec_WrdFill( vRes, 1, Result ); + if ( fVerbose ) + printf( " <== best" ); + } + nBSets++; + } + if ( fVerbose ) + printf( "\n" ); } - if ( MyuThis <= MyuOrigBest + nMyuIncrease ) { - int Shared = 0, nSetSize = 0; - if ( MyuThis > 2 ) { - int SharedThis = 0, nSetSizeThis = 0; - int nRailsMin = 100; - for ( int r = 1; r <= nRails && nRailsMin > r; r++ ) { - int nRailsMinNew = Abc_SharedEvalBest( p, pCopy, nVars, nCVars, nFVars, MyuThis, r, 0, &SharedThis, &nSetSizeThis, p->pPat ); - if ( nRailsMinNew < 100 ) - nRailsMin = nRailsMinNew; - } - if ( fVerbose ) - printf( " RailsMyu = %3d. RailsMin = %3d. Shared = %2d. SetSize = %d.", Abc_Base2Log(MyuThis), nRailsMin, SharedThis, nSetSizeThis ); - if ( nRailsMin <= nRails ) { - MyuThis = 1 << nRailsMin; - Shared = SharedThis; - nSetSize = nSetSizeThis; - } + Vec_WecFree( vAllSets ); + } + else { + Vec_IntForEachEntryDouble( p->vPairs[p->nVars][p->nLVars], Var0, Var1, i ) { + int MyuThis = Abc_TtGetCM( pCopy, nVars, nFVars, p->vCounts, p->vTable, p->vStore, p->vUsed, 0 ); + MyuOrigBest = Abc_MinInt( MyuOrigBest, MyuThis ); + if ( pMyu ) *pMyu = Abc_MinInt( *pMyu, MyuThis ); + if ( fVerbose ) + { + printf( "%3d : ", i/2 ); + for ( k = nCVars-1; k >= 0; k-- ) + printf( " %d", nVars-nCVars+k ); + printf( " " ); + for ( k = nPermVars-1; k >= nFVars; k-- ) + printf( " %d", Pla2Var[k] ); + printf( " " ); + for ( k = nFVars-1; k >= 0; k-- ) + printf( " %d", Pla2Var[k] ); + printf( " : Myu = %3d", MyuThis ); } - if ( MyuBest > MyuThis || (MyuBest == MyuThis && nSetSizeBest >= nSetSize) ) { - int fSave = (MyuBest == MyuThis && nSetSizeBest == nSetSize); - MyuBest = MyuThis; - nSetSizeBest = nSetSize; - word Result = Abc_BSEvalEncode( Pla2Var, nVars, nLutSize, Shared, MyuBest, nSetSize ); - if ( fSave ) - Vec_WrdPush( vRes, Result ); - else - Vec_WrdFill( vRes, 1, Result ); - if ( fVerbose ) - printf( " <== best" ); - } - } - if ( fVerbose ) - printf( "\n" ); - int iPlace0 = Var2Pla[Var0]; - int iPlace1 = Var2Pla[Var1]; - if ( iPlace0 == iPlace1 ) - continue; - Abc_TtSwapVars( pCopy, nVars, iPlace0, iPlace1 ); - Var2Pla[Pla2Var[iPlace0]] = iPlace1; - Var2Pla[Pla2Var[iPlace1]] = iPlace0; - Pla2Var[iPlace0] ^= Pla2Var[iPlace1]; - Pla2Var[iPlace1] ^= Pla2Var[iPlace0]; - Pla2Var[iPlace0] ^= Pla2Var[iPlace1]; + if ( MyuThis <= MyuOrigBest + nMyuIncrease ) { + int Shared = 0, nSetSize = 0; + if ( MyuThis > 2 ) { + int SharedThis = 0, nSetSizeThis = 0; + int nRailsMin = 100; + for ( int r = 1; r <= nRails && nRailsMin > r; r++ ) { + int nRailsMinNew = Abc_SharedEvalBest( p, pCopy, nVars, nCVars, nFVars, MyuThis, r, 0, &SharedThis, &nSetSizeThis, p->pPat ); + if ( nRailsMinNew < 100 ) + nRailsMin = nRailsMinNew; + } + if ( fVerbose ) + printf( " RailsMyu = %3d. RailsMin = %3d. Shared = %2d. SetSize = %d.", Abc_Base2Log(MyuThis), nRailsMin, SharedThis, nSetSizeThis ); + if ( nRailsMin <= nRails ) { + MyuThis = 1 << nRailsMin; + Shared = SharedThis; + nSetSize = nSetSizeThis; + } + } + if ( MyuBest > MyuThis || (MyuBest == MyuThis && nSetSizeBest >= nSetSize) ) { + int fSave = (MyuBest == MyuThis && nSetSizeBest == nSetSize); + MyuBest = MyuThis; + nSetSizeBest = nSetSize; + word Result = Abc_BSEvalEncode( Pla2Var, nVars, nLutSize, Shared, MyuBest, nSetSize ); + if ( fSave ) + Vec_WrdPush( vRes, Result ); + else + Vec_WrdFill( vRes, 1, Result ); + if ( fVerbose ) + printf( " <== best" ); + } + nBSets++; + } + if ( fVerbose ) + printf( "\n" ); + Abc_TtExchangeVars( pCopy, nVars, Var2Pla, Pla2Var, Var0, Var1 ); + } } for ( i = 0; i < nPermVars; i++ ) - { - int iPlace0 = i; - int iPlace1 = Var2Pla[i]; - if ( iPlace0 == iPlace1 ) - continue; - Abc_TtSwapVars( pCopy, nVars, iPlace0, iPlace1 ); - Var2Pla[Pla2Var[iPlace0]] = iPlace1; - Var2Pla[Pla2Var[iPlace1]] = iPlace0; - Pla2Var[iPlace0] ^= Pla2Var[iPlace1]; - Pla2Var[iPlace1] ^= Pla2Var[iPlace0]; - Pla2Var[iPlace0] ^= Pla2Var[iPlace1]; - } + Abc_TtMoveVar( pCopy, nVars, Var2Pla, Pla2Var, i, i ); if ( !Abc_TtEqual(pCopy, pTruth, nWords) ) printf( "Internal truth table check failed.\n" ); @@ -1124,7 +1288,7 @@ Vec_Wrd_t * Abc_TtFindBVarsSVars2( Abc_BSEval_t * p, word * pTruth, int nVars, i return NULL; } if ( fVerbose ) - printf( "COllected %d solutions with MyuMin = %d and SharedSize = %d.\n", Vec_WrdSize(vRes), MyuBest, nSetSizeBest ); + printf( "Tried %d bound-sets and collected %d solutions with MyuMin = %d and SharedSize = %d.\n", nBSets, Vec_WrdSize(vRes), MyuBest, nSetSizeBest ); return vRes; } diff --git a/src/misc/util/utilTruth.h b/src/misc/util/utilTruth.h index cf3d6cedf..c9d453d06 100644 --- a/src/misc/util/utilTruth.h +++ b/src/misc/util/utilTruth.h @@ -1987,6 +1987,20 @@ static inline void Abc_TtSwapVars( word * pTruth, int nVars, int iVar, int jVar return; } } +// exchanges places of v1 and v2 +static inline void Abc_TtExchangeVars( word * pF, int nVars, int * V2P, int * P2V, int v1, int v2 ) +{ + int iPlace0 = V2P[v1]; + int iPlace1 = V2P[v2]; + if ( iPlace0 == iPlace1 ) + return; + Abc_TtSwapVars( pF, nVars, iPlace0, iPlace1 ); + V2P[P2V[iPlace0]] = iPlace1; + V2P[P2V[iPlace1]] = iPlace0; + P2V[iPlace0] ^= P2V[iPlace1]; + P2V[iPlace1] ^= P2V[iPlace0]; + P2V[iPlace0] ^= P2V[iPlace1]; +} // moves one var (v) to the given position (p) static inline void Abc_TtMoveVar( word * pF, int nVars, int * V2P, int * P2V, int v, int p ) {