From 9bb736acee7ff3d5c4e14d48e836287767559134 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Tue, 20 May 2025 06:39:28 -0700 Subject: [PATCH] Improvements to "lutcasdec". --- src/base/abci/abc.c | 24 +++-- src/base/abci/abcCas.c | 22 ++-- src/misc/util/utilBSet.c | 214 +++++++++++++++++++++++---------------- 3 files changed, 156 insertions(+), 104 deletions(-) diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 8dc00865e..31a202f8c 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -9171,12 +9171,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_NtkLutCascade2( Abc_Ntk_t * pNtk, int nLutSize, int nLuts, int nRails, int nIters, int nJRatio, int Seed, int fVerbose, char * pGuide ); - extern void Abc_NtkLutCascadeFile( char * pFileName, int nVarNum, int nLutSize, int nLuts, int nRails, int nIters, int nJRatio, int Seed, int fVerbose, int fVeryVerbose, int fPrintMyu ); + extern Abc_Ntk_t * Abc_NtkLutCascade2( Abc_Ntk_t * pNtk, int nLutSize, int nLuts, int nRails, int nIters, int nJRatio, int nZParam, 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 ); 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 = 0, fGen = 0, fPrintMyu = 0, fVerbose = 0, fVeryVerbose = 0; + int c, nVarNum = -1, nLutSize = 6, nStages = 8, nRails = 1, nShared = 2, Seed = 0, nIters = 1, nJRatio = 0, nZParam = 0, fGen = 0, fPrintMyu = 0, fVerbose = 0, fVeryVerbose = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "KMRSCIJNFgmvwh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "KMRSCIJZNFgmvwh" ) ) != EOF ) { switch ( c ) { @@ -9257,6 +9257,15 @@ int Abc_CommandLutCasDec( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( nJRatio < 0 ) goto usage; break; + case 'Z': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-Z\" should be followed by a file name.\n" ); + goto usage; + } + nZParam = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + break; case 'N': if ( globalUtilOptind >= argc ) { @@ -9302,7 +9311,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, Seed, fVerbose, fVeryVerbose, fPrintMyu ); + Abc_NtkLutCascadeFile( pFileName, nVarNum, nLutSize, nStages, nRails, nIters, nJRatio, nZParam, Seed, fVerbose, fVeryVerbose, fPrintMyu ); return 0; } if ( fGen ) @@ -9339,7 +9348,7 @@ int Abc_CommandLutCasDec( Abc_Frame_t * pAbc, int argc, char ** argv ) } if ( argc == globalUtilOptind + 1 ) pGuide = argv[globalUtilOptind]; - pNtkRes = Abc_NtkLutCascade2( pNtk, nLutSize, nStages, nRails, nIters, nJRatio, Seed, fVerbose, pGuide ); + pNtkRes = Abc_NtkLutCascade2( pNtk, nLutSize, nStages, nRails, nIters, nJRatio, nZParam, Seed, fVerbose, fVeryVerbose, pGuide ); if ( pNtkRes == NULL ) { Abc_Print( -1, "LUT cascade mapping failed.\n" ); @@ -9349,7 +9358,7 @@ int Abc_CommandLutCasDec( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: lutcasdec [-KMRCSIJN ] [-F ] [-gmvwh]\n" ); + Abc_Print( -2, "usage: lutcasdec [-KMRCSIJZN ] [-F ] [-gmvwh]\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 ); @@ -9358,6 +9367,7 @@ usage: Abc_Print( -2, "\t-S : the random seed for randomized bound-set selection [default = %d]\n", Seed ); Abc_Print( -2, "\t-I : the number of iterations when looking for a solution [default = %d]\n", nIters ); 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-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" ); diff --git a/src/base/abci/abcCas.c b/src/base/abci/abcCas.c index 9eb682c62..e1a67dad6 100644 --- a/src/base/abci/abcCas.c +++ b/src/base/abci/abcCas.c @@ -656,12 +656,18 @@ void Abc_LutCascadeDerive( word * p, int nVars, int nBVars, int Myu, word * pRem } // performs decomposition of one stage -static inline int Abc_LutCascadeDecStage( char * pGuide, int Iter, Vec_Wrd_t * vFuncs[3], Vec_Int_t * vVarIDs, int nRVars, int nRails, int nLutSize, int nJRatio, int fVerbose, Vec_Wrd_t * vCas, int * pMyu ) +static inline int Abc_LutCascadeDecStage( char * pGuide, int Iter, Vec_Wrd_t * vFuncs[3], Vec_Int_t * vVarIDs, int nRVars, int nRails, int nLutSize, int nJRatio, int nZParam, int fVerbose, Vec_Wrd_t * vCas, int * pMyu ) { extern word Abc_TtFindBVarsSVars( word * p, int nVars, int nRVars, int nRails, int nLutSize, int fVerbose, int * pMyu, int nJRatio ); + extern word Abc_TtFindBVarsSVars2( word * p, int nVars, int nRVars, int nRails, int nLutSize, int fVerbose, int * pMyu, int nJRatio ); assert( Vec_IntSize(vVarIDs) > nLutSize ); assert( Vec_IntSize(vVarIDs) <= 24 ); - word Guide = pGuide ? 0 : Abc_TtFindBVarsSVars( Vec_WrdArray(vFuncs[0]), Vec_IntSize(vVarIDs), nRVars, nRails, nLutSize, fVerbose, pMyu, nJRatio ); + //word Guide = pGuide ? 0 : Abc_TtFindBVarsSVars( Vec_WrdArray(vFuncs[0]), Vec_IntSize(vVarIDs), nRVars, nRails, nLutSize, fVerbose, pMyu, nJRatio ); + word Guide = pGuide ? 0 : Abc_TtFindBVarsSVars2( Vec_WrdArray(vFuncs[0]), Vec_IntSize(vVarIDs), nRVars, nRails, nLutSize, fVerbose, pMyu, nZParam ); +// if ( nZParam ) +// Guide = pGuide ? 0 : Abc_TtFindBVarsSVars2( Vec_WrdArray(vFuncs[0]), Vec_IntSize(vVarIDs), nRVars, nRails, nLutSize, fVerbose, pMyu, nZParam ); +// else +// Guide = pGuide ? 0 : Abc_TtFindBVarsSVars( Vec_WrdArray(vFuncs[0]), Vec_IntSize(vVarIDs), nRVars, nRails, nLutSize, fVerbose, pMyu, nJRatio ); if ( !pGuide && !Guide ) { if ( fVerbose ) printf( "The function is not decomposable with %d rails.\n", nRails ); @@ -716,7 +722,7 @@ static inline int Abc_LutCascadeDecStage( char * pGuide, int Iter, Vec_Wrd_t * v Vec_IntShrink( vVarIDs, nFVars+nSVars+nEVars ); return nEVars; } -word * Abc_LutCascadeDec( char * pGuide, word * pTruth, int nVarsOrig, Vec_Int_t * vVarIDs, int nRails, int nLutSize, int nStages, int nJRatio, int fVerbose, int * pnStages, int * pMyu ) +word * Abc_LutCascadeDec( char * pGuide, word * pTruth, int nVarsOrig, Vec_Int_t * vVarIDs, int nRails, int nLutSize, int nStages, int nJRatio, int nZParam, int fVerbose, int * pnStages, int * pMyu ) { 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) }; @@ -724,7 +730,7 @@ word * Abc_LutCascadeDec( char * pGuide, word * pTruth, int nVarsOrig, Vec_Int_t Vec_Wrd_t * vCas = Vec_WrdAlloc( 100 ); Vec_WrdPush( vCas, nVarsOrig ); if ( pnStages ) *pnStages = 0; for ( i = 0; Vec_IntSize(vVarIDs) > nLutSize; i++ ) { - nRVars = Abc_LutCascadeDecStage( pGuide, i, vFuncs, vVarIDs, nRVars, nRails, nLutSize, nJRatio, fVerbose, vCas, i ? NULL : pMyu ); + nRVars = Abc_LutCascadeDecStage( pGuide, i, vFuncs, vVarIDs, nRVars, nRails, nLutSize, nJRatio, nZParam, fVerbose, vCas, i ? NULL : pMyu ); if ( i+2 > nStages ) { if ( fVerbose ) printf( "The length of the cascade (%d) exceeds the max allowed number of stages (%d).\n", i+2, nStages ); @@ -836,7 +842,7 @@ Abc_Ntk_t * Abc_NtkLutCascade( Abc_Ntk_t * pNtk, int nLutSize, int nStages, int Gia_ManStop( pGia ); return pNew; } -Abc_Ntk_t * Abc_NtkLutCascade2( Abc_Ntk_t * pNtk, int nLutSize, int nStages, int nRails, int nIters, int nJRatio, int Seed, int fVerbose, char * pGuide ) +Abc_Ntk_t * Abc_NtkLutCascade2( Abc_Ntk_t * pNtk, int nLutSize, int nStages, int nRails, int nIters, int nJRatio, int nZParam, int Seed, int fVerbose, int fVeryVerbose, char * pGuide ) { extern Gia_Man_t * Abc_NtkStrashToGia( Abc_Ntk_t * pNtk ); int i, nWords = Abc_TtWordNum(Abc_NtkCiNum(pNtk)); @@ -864,7 +870,7 @@ Abc_Ntk_t * Abc_NtkLutCascade2( Abc_Ntk_t * pNtk, int nLutSize, int nStages, int printf( ".\n" ); } - word * pLuts = Abc_LutCascadeDec( pGuide, pTruth1, Abc_NtkCiNum(pNtk), vVarIDs, nRails, nLutSize, nStages, Iter >= nIters ? 1 : 0, fVerbose, NULL, NULL ); + word * pLuts = Abc_LutCascadeDec( pGuide, pTruth1, Abc_NtkCiNum(pNtk), vVarIDs, nRails, nLutSize, nStages, Iter >= nIters ? 1 : 0, nZParam, fVeryVerbose, NULL, NULL ); pNew = pLuts ? Abc_NtkLutCascadeFromLuts( pLuts, Abc_NtkCiNum(pNtk), pNtk, nLutSize, fVerbose ) : NULL; Vec_IntFree( vVarIDs ); @@ -1377,7 +1383,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 Seed, int fVerbose, int fVeryVerbose, int fPrintMyu ) +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 ) { abctime clkStart = Abc_Clock(); int i, Sum = 0, nStageCount = 0, MyuMin = 0, nTotalLuts = 0, nWords = Abc_TtWordNum(nVarsOrig); @@ -1425,7 +1431,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( NULL, pTruth, nVarsOrig, vVarIDs, nRails, nLutSize, nStages, (int)(Iter >= nIters), fVeryVerbose, &nStageCount, &MyuMin ); + word * pLuts = Abc_LutCascadeDec( NULL, pTruth, nVarsOrig, vVarIDs, nRails, nLutSize, nStages, (int)(Iter >= nIters), nZParam, fVeryVerbose, &nStageCount, &MyuMin ); 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 705892579..1e731c8e1 100644 --- a/src/misc/util/utilBSet.c +++ b/src/misc/util/utilBSet.c @@ -635,10 +635,10 @@ int Abc_BSEvalBest( Abc_BSEval_t * p, word * pIn, word * pBest, word * pBest2, i } if ( 0 ) { //word pPat[MAX_PAT_WORD_SIZE]; - int nRails = 1, Shared = 0; + int nRails = 1, Shared = 0, nSetSize = 0; if ( CostThis > (1 << nRails) ) { - extern int Abc_SharedEvalBest( Abc_BSEval_t * p, word * pTruth, int nVars, int nCVars, int nFVars, int MyuMin, int nRails, int fVerbose, int * pSetShared, word * pPat ); - int nRailsMin = Abc_SharedEvalBest( p, pIn, nVars, nCVars, nFVars, CostThis, nRails, 0, &Shared, p->pPat ); + extern int Abc_SharedEvalBest( Abc_BSEval_t * p, word * pTruth, int nVars, int nCVars, int nFVars, int MyuMin, int nRails, int fVerbose, int * pSetShared, int * pSetSize, word * pPat ); + int nRailsMin = Abc_SharedEvalBest( p, pIn, nVars, nCVars, nFVars, CostThis, nRails, 0, &Shared, &nSetSize, p->pPat ); printf( " RailMin = %d. Shared = %2d. ", nRailsMin, Shared ); } } @@ -892,7 +892,7 @@ int Abc_BSEvalFindShared( int nVars, word * pISets, int nISets, int nBSWords, Ve SeeAlso [] ***********************************************************************/ -int Abc_SharedEvalBest( Abc_BSEval_t * p, word * pTruth, int nVars, int nCVars, int nFVars, int MyuMin, int nRails, int fVerbose, int * pSetShared, word * pPat ) +int Abc_SharedEvalBest( Abc_BSEval_t * p, word * pTruth, int nVars, int nCVars, int nFVars, int MyuMin, int nRails, int fVerbose, int * pSetShared, int * pnSetSize, word * pPat ) { int nBSWords = Abc_Truth6WordNum( nVars - nFVars ), CVarMask = nCVars ? Abc_InfoMask(nCVars) << (nVars - nCVars - nFVars) : 0; int MyuCur, Myu = Abc_TtGetCMInt( pTruth, nVars, nFVars, p->vCounts, p->vTable, p->vStore, p->vUsed, pPat ); @@ -914,6 +914,7 @@ int Abc_SharedEvalBest( Abc_BSEval_t * p, word * pTruth, int nVars, int nCVars, if ( nRailsMin > nRailsCur ) { nRailsMin = nRailsCur; *pSetShared = iSet; + *pnSetSize = i; } } if ( nRailsMin <= nRails ) @@ -921,89 +922,6 @@ int Abc_SharedEvalBest( Abc_BSEval_t * p, word * pTruth, int nVars, int nCVars, } return nRailsMin; } -int Abc_DeriveLutDec( word * pTruth, int nVars, int nCVars, int nFVars, int * pPerm, int nRails, int Shared, int fVerbose, Vec_Wrd_t * vRes ) -{ - return 0; -} - -/**Function************************************************************* - - Synopsis [Decomposing truth table into a K-LUT cascade with R rails.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -word * Abc_LutCascade2( word * pFunc, int nVars, int nLutSize, int nLuts, int nRails, int nIters, int fVerbose ) -{ - Abc_BSEval_t * p = Abc_BSEvalAlloc(); - Vec_Wrd_t * vRes = Vec_WrdStart( 1 ); word * pRes = NULL; - word * pTruth = ABC_ALLOC( word, Abc_TtWordNum(nVars) ); - word * pBest = ABC_ALLOC( word, Abc_TtWordNum(nVars) ); - word * pBest2 = ABC_ALLOC( word, Abc_TtWordNum(nVars) ); - Abc_TtCopy( pTruth, pFunc, Abc_TtWordNum(nVars), 0 ); - int i, r, nVarsCur = nVars, nOutVars = 0; - while ( nVarsCur > nLutSize ) - { - int pPerm[32] = {0}; - int pPerm2[32] = {0}; - if ( p->nVars != nVarsCur || p->nBVars != nLutSize ) { - Vec_IntFreeP( &p->vPairs ); - if ( p->nBVars != nLutSize ) { - Vec_WecFreeP( &p->vSets ); - Vec_WrdFreeP( &p->vCofs ); - p->vCofs = Abc_BSEvalCreateCofactorSets( nLutSize, &p->vSets ); - if ( p->nBVars < nLutSize ) { - ABC_FREE( p->pPat ); - p->pPat = ABC_ALLOC( word, (1 << nLutSize)*Abc_TtWordNum(nLutSize) ); - } - } - p->vPairs = Abc_GenChasePairs( nVarsCur, nLutSize ); - p->nVars = nVarsCur; - p->nBVars = nLutSize; - } - int MyuMin = Abc_BSEvalBest( p, pTruth, pBest, pBest2, nVarsCur, nOutVars, nVarsCur-nLutSize, fVerbose, pPerm, pPerm2, 0, 0 ); - int Shared = 0, nRailsMin = Abc_Base2Log( MyuMin ); - for ( r = 1; r <= nRails && nRailsMin > r; r++ ) { - int nRailsMinNew = Abc_SharedEvalBest( p, pBest, nVarsCur, nOutVars, nVarsCur-nLutSize, MyuMin, nRails, fVerbose, &Shared, p->pPat ); - if ( nRailsMinNew < 100 ) - nRailsMin = nRailsMinNew; - } - MyuMin = 1 << nRailsMin; - if ( nRailsMin > nRails ) { - Vec_WrdFreeP( &vRes ); - break; - } - // update nVarsCur, pTruth, nOutVars, and vRes - nVarsCur = Abc_DeriveLutDec( pBest, nVarsCur, nOutVars, nVarsCur-nLutSize, pPerm, nRailsMin, Shared, fVerbose, vRes ); - Abc_TtCopy( pTruth, pBest, Abc_TtWordNum(nVarsCur), 0 ); - nOutVars = nRailsMin; - } - if ( vRes ) // decomposition succeeded - { - // create the last node - assert( nVarsCur <= nLutSize ); - Vec_WrdAddToEntry( vRes, 0, 1 ); - Vec_WrdPush( vRes, nVarsCur+4 ); - Vec_WrdPush( vRes, nVarsCur ); - for ( i = 0; i < nVarsCur; i++ ) - Vec_WrdPush( vRes, i ); - Vec_WrdPush( vRes, 0 ); - Vec_WrdPush( vRes, pTruth[0] ); - // extract the output array - pRes = Vec_WrdReleaseArray( vRes ); - Vec_WrdFree( vRes ); - } - // cleanup and return - Abc_BSEvalFree(p); - ABC_FREE( pTruth ); - ABC_FREE( pBest ); - ABC_FREE( pBest2 ); - return pRes; -} /**Function************************************************************* @@ -1057,9 +975,9 @@ word Abc_TtFindBVarsSVars( word * pTruth, int nVars, int nRVars, int nRails, int printf( " Myu = %d. ", MyuMin ); } - int Shared = 0, nRailsMin = Abc_Base2Log( MyuMin ); + int Shared = 0, nSetSize = 0, nRailsMin = Abc_Base2Log( MyuMin ); for ( r = 1; r <= nRails && nRailsMin > r; r++ ) { - int nRailsMinNew = Abc_SharedEvalBest( p, pBest, nVars, nRVars, nVars-nLutSize, MyuMin, r, 0, &Shared, p->pPat ); + int nRailsMinNew = Abc_SharedEvalBest( p, pBest, nVars, nRVars, nVars-nLutSize, MyuMin, r, 0, &Shared, &nSetSize, p->pPat ); if ( nRailsMinNew < 100 ) nRailsMin = nRailsMinNew; } @@ -1088,6 +1006,124 @@ word Abc_TtFindBVarsSVars( word * pTruth, int nVars, int nRVars, int nRails, int return ((word)MyuMin << 48) | (mSVars << 24) | mBVars; } +word Abc_BSEvalEncode( int * pPermBest, int nVars, int nLutSize, int Shared, int MyuMin, int SharedSize ) +{ + int v; + word mBVars = 0; + for ( v = 0; v < nLutSize; v++ ) + mBVars |= (word)1 << pPermBest[nVars-nLutSize+v]; + word mSVars = 0; + for ( v = 0; v < nLutSize; v++ ) + if ( (Shared >> v) & 1 ) + mSVars |= (word)1 << (nVars-nLutSize+v); + return ((word)MyuMin << 48) | (mSVars << 24) | mBVars; +} +word Abc_TtFindBVarsSVars2( word * pTruth, int nVars, int nCVars, int nRails, int nLutSize, int fVerbose, int * pMyu, int nMyuIncrease ) +{ + Abc_BSEval_t * p = Abc_BSEvalAlloc(); + int nFVars = nVars-nLutSize; + int nPermVars = nVars-nCVars; + if ( p->nVars != nPermVars ) { + Vec_IntFreeP( &p->vPairs ); + p->vPairs = Abc_GenChasePairs( nPermVars, nLutSize-nCVars ); + p->nVars = nPermVars; + } + if ( p->nBVars != nLutSize ) { + Vec_WecFreeP( &p->vSets ); + Vec_WrdFreeP( &p->vCofs ); + p->vCofs = Abc_BSEvalCreateCofactorSets( nLutSize, &p->vSets ); + if ( p->nBVars < nLutSize ) { + ABC_FREE( p->pPat ); + p->pPat = ABC_ALLOC( word, (1 << nLutSize)*Abc_TtWordNum(nLutSize) ); + } + p->nBVars = nLutSize; + } + + int nWords = Abc_TtWordNum(nVars); + word * pCopy = ABC_ALLOC( word, nWords ); + Abc_TtCopy( pCopy, pTruth, nWords, 0 ); + + word Result = 0; + int i, k, Var0, Var1, Pla2Var[32], Var2Pla[32]; + for ( i = 0; i < nVars; i++ ) + Pla2Var[i] = Var2Pla[i] = i; + int MyuBest = 1 << nVars; + int nSetSizeBest = nVars; + + if ( pMyu ) *pMyu = 1 << nVars; + Vec_IntForEachEntryDouble( p->vPairs, Var0, Var1, i ) { + int MyuThis = Abc_TtGetCM( pCopy, nVars, nFVars, p->vCounts, p->vTable, p->vStore, p->vUsed, 0 ); + 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 ( MyuThis <= MyuBest + nMyuIncrease ) { + int Shared = 0, nSetSize = 0; + if ( MyuThis > 2 ) { + int SharedThis = 0, nSetSizeThis = 0; + int nRailsMin = Abc_SharedEvalBest( p, pCopy, nVars, nCVars, nFVars, MyuThis, nRails, 0, &SharedThis, &nSetSizeThis, p->pPat ); + if ( fVerbose ) + printf( " RailsMyu = %3d. RailsMin = %3d. Shared = %2d. SetSize = %d.", Abc_Base2Log(MyuThis), nRailsMin, SharedThis, nSetSizeThis ); + if ( nRailsMin <= nRails ) { + assert( Abc_Base2Log(MyuThis) >= nRailsMin ); + MyuThis = 1 << nRailsMin; + Shared = SharedThis; + nSetSize = nSetSizeThis; + } + } + if ( MyuBest > MyuThis || (MyuBest == MyuThis && nSetSizeBest > nSetSize) ) { + MyuBest = MyuThis; + nSetSizeBest = nSetSize; + Result = Abc_BSEvalEncode( Pla2Var, nVars, p->nBVars, Shared, MyuBest, nSetSize ); + 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]; + } + 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]; + } + if ( !Abc_TtEqual(pCopy, pTruth, nWords) ) + printf( "Internal truth table check failed.\n" ); + + Abc_BSEvalFree(p); + if ( MyuBest > (1 << nRails) ) + return 0; + return Result; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// ////////////////////////////////////////////////////////////////////////