From bd7fb12e183188c7bb8afdc2ac12fc1fc4ba7755 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Wed, 24 Dec 2025 13:37:06 -0800 Subject: [PATCH] Upgrading "lutexact -c" to be like "lutexact -k". --- src/sat/bmc/bmcMaj7.c | 148 ++++++++++++++++++++++++++++++++++++++++-- 1 file changed, 144 insertions(+), 4 deletions(-) diff --git a/src/sat/bmc/bmcMaj7.c b/src/sat/bmc/bmcMaj7.c index b957e8112..167216586 100644 --- a/src/sat/bmc/bmcMaj7.c +++ b/src/sat/bmc/bmcMaj7.c @@ -405,6 +405,77 @@ static void Exa7_ManPrintSolution( Exa7_Man_t * p, int fCompl ) } } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static Vec_Wrd_t * Exa7_ManSaveTruthTables( Exa7_Man_t * p, int fCompl ) +{ + int i, k, nWordsNode, nMintsNode; + assert( p->nLutSize <= 8 ); + nMintsNode = 1 << p->nLutSize; + nWordsNode = (p->nLutSize <= 6) ? 1 : (p->nLutSize == 7 ? 2 : 4); + Vec_Wrd_t * vTruths = Vec_WrdStart( p->nObjs * nWordsNode ); + for ( i = p->nVars; i < p->nObjs; i++ ) + { + word Truth[4] = {0, 0, 0, 0}; + int iVarStart = 1 + p->LutMask*(i - p->nVars); + for ( k = 0; k < p->LutMask; k++ ) + { + if ( cadical_solver_get_var_value(p->pSat, iVarStart + k) ) + { + int bit = k + 1; // minterm index (minterm 0 is fixed to 0) + int w = bit >> 6; + int b = bit & 63; + Truth[w] |= ((word)1 << b); + } + } + // complement the output fully if needed (including minterm 0) + if ( i == p->nObjs - 1 && fCompl ) + { + for ( int w = 0; w < nWordsNode; w++ ) + { + word Mask; + int rem = nMintsNode - w * 64; + if ( rem <= 0 ) + Mask = 0; + else if ( rem >= 64 ) + Mask = ~(word)0; + else + Mask = (((word)1) << rem) - 1; + Truth[w] = (~Truth[w]) & Mask; + } + } + if ( p->nLutSize < 6 ) + Truth[0] = Abc_Tt6Stretch( Truth[0], p->nLutSize ); + for ( int w = 0; w < nWordsNode; w++ ) + Vec_WrdWriteEntry( vTruths, i * nWordsNode + w, Truth[w] ); + } + return vTruths; +} +static void Exa7_ManPrintPerm( Exa7_Man_t * p ) +{ + int i, k, iVar; + for ( i = p->nVars; i < p->nObjs; i++ ) + { + if ( i > p->nVars ) + printf( "_" ); + for ( k = p->nLutSize - 1; k >= 0; k-- ) + { + iVar = Exa7_ManFindFanin( p, i, k ); + if ( iVar >= 0 && iVar < p->nVars ) + printf( "%c", 'a'+iVar ); + } + } +} + /**Function************************************************************* Synopsis [] @@ -705,6 +776,9 @@ void Exa7_ManPrint( Exa7_Man_t * p, int i, int iMint, abctime clk ) } int Exa7_ManExactSynthesis( Bmc_EsPar_t * pPars ) { + extern int Exa7_ManExactSynthesisIter( Bmc_EsPar_t * pPars ); + if ( pPars->fMinNodes ) + return Exa7_ManExactSynthesisIter( pPars ); int i, status, Res = 0, iMint = 1; abctime clkTotal = Abc_Clock(); Exa7_Man_t * p; int fCompl = 0; @@ -713,7 +787,7 @@ int Exa7_ManExactSynthesis( Bmc_EsPar_t * pPars ) word * pFun = Abc_TtSymFunGenerate( pPars->pSymStr, pPars->nVars ); pPars->pTtStr = ABC_CALLOC( char, pPars->nVars > 2 ? (1 << (pPars->nVars-2)) + 1 : 2 ); Extra_PrintHexadecimalString( pPars->pTtStr, (unsigned *)pFun, pPars->nVars ); - if ( !pPars->fSilent ) printf( "Generated symmetric function: %s\n", pPars->pTtStr ); + if ( !pPars->fSilent && pPars->nVars <= 7 ) printf( "Generated symmetric function: %s\n", pPars->pTtStr ); ABC_FREE( pFun ); } if ( pPars->pTtStr ) @@ -745,21 +819,87 @@ int Exa7_ManExactSynthesis( Bmc_EsPar_t * pPars ) if ( pPars->fVerbose && status != CADICAL_UNDEC ) Exa7_ManPrint( p, i, iMint, Abc_Clock() - clkTotal ); if ( iMint == -1 ) - Exa7_ManPrintSolution( p, fCompl ), Res = 1; + { + Exa7_ManPrintSolution( p, fCompl ); + printf( "The variable permutation is \"" ); + Exa7_ManPrintPerm( p ); + printf( "\".\n" ); + if ( pPars->fDumpBlif ) + Exa7_ManDumpBlif( p, fCompl ); + if ( p->pPars->fGenTruths ) { + if ( p->pPars->vTruths ) + Vec_WrdFreeP( &p->pPars->vTruths ); + p->pPars->vTruths = Exa7_ManSaveTruthTables( p, fCompl ); + } + Res = 1; + } else if ( status == CADICAL_UNDEC ) printf( "The solver timed out after %d sec.\n", pPars->RuntimeLim ); else if ( !p->pPars->fSilent ) printf( "The problem has no solution.\n" ), Res = 2; if ( !pPars->fSilent && (p->nUsed[0] || p->nUsed[1]) ) printf( "Added = %d. Tried = %d. ", p->nUsed[1], p->nUsed[0] ); if ( !pPars->fSilent ) Abc_PrintTime( 1, "Total runtime", Abc_Clock() - clkTotal ); - if ( iMint == -1 && pPars->fDumpBlif ) - Exa7_ManDumpBlif( p, fCompl ); if ( pPars->pSymStr ) ABC_FREE( pPars->pTtStr ); Exa7_ManFree( p ); return Res; } +int Exa7_ManExactSynthesisIter( Bmc_EsPar_t * pPars ) +{ + pPars->fMinNodes = 0; + int nNodeMin = (pPars->nVars-2)/(pPars->nLutSize-1) + 1; + int nNodeMax = pPars->nNodes, Result = 0; + int fGenPerm = pPars->pPermStr == NULL; + for ( int n = nNodeMin; n <= nNodeMax; n++ ) { + if ( !pPars->fSilent ) printf( "\nTrying M = %d:\n", n ); + pPars->nNodes = n; + if ( !pPars->fUsePerm && fGenPerm ) { + Vec_Str_t * vStr = Vec_StrAlloc( 100 ); + for ( int v = 0; v < pPars->nLutSize; v++ ) + Vec_StrPush( vStr, 'a'+v ); + int nDupVars = Abc_MaxInt(0, (pPars->nLutSize-1) - (pPars->nVars-pPars->nLutSize)); + Vec_StrPush( vStr, '_' ); + for ( int v = 0; v < nDupVars; v++ ) + Vec_StrPush( vStr, 'a'+v ); + for ( int v = 0; v < pPars->nLutSize-1-nDupVars; v++ ) + Vec_StrPush( vStr, '*' ); + for ( int m = 2; m < pPars->nNodes; m++ ) { + Vec_StrPush( vStr, '_' ); + for ( int v = 0; v < pPars->nLutSize-1; v++ ) + Vec_StrPush( vStr, '*' ); + } + Vec_StrPush( vStr, '\0' ); + ABC_FREE( pPars->pPermStr ); + pPars->pPermStr = Vec_StrReleaseArray(vStr); + Vec_StrFree( vStr ); + } + else if ( pPars->fUsePerm && fGenPerm ) { + Vec_Str_t * vStr = Vec_StrAlloc( 100 ); + for ( int v = 0; v < pPars->nLutSize; v++ ) + Vec_StrPush( vStr, 'a'+v ); + for ( int m = 1; m < pPars->nNodes; m++ ) { + Vec_StrPush( vStr, '_' ); + if ( m & 1 ) + for ( int v = 0; v < pPars->nLutSize-1; v++ ) + Vec_StrPush( vStr, 'a'+(pPars->nVars-(pPars->nLutSize-1-v)) ); + else + for ( int v = 0; v < pPars->nLutSize-1; v++ ) + Vec_StrPush( vStr, 'a'+v ); + } + Vec_StrPush( vStr, '\0' ); + ABC_FREE( pPars->pPermStr ); + pPars->pPermStr = Vec_StrReleaseArray(vStr); + Vec_StrFree( vStr ); + } + Result = Exa7_ManExactSynthesis(pPars); + fflush( stdout ); + if ( Result == 1 ) + break; + } + return Result; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE ///