luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Adding permutation printout in "lutexact".

This commit is contained in:
Alan Mishchenko 2025-11-18 18:10:31 -08:00
parent 281204f938
commit 8c27e4bc90
2 changed files with 38 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

22
src/sat/bmc/bmcMaj.c
View File

@ -1340,7 +1340,21 @@ static void Exa3_ManPrintSolution( Exa3_Man_t * p, int fCompl )
printf( " )\n" );
}
}
static void Exa3_ManPrintPerm( Exa3_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 = Exa3_ManFindFanin( p, i, k );
if ( iVar >= 0 && iVar < p->nVars )
printf( "%c", 'a'+iVar );
}
}
}
/**Function*************************************************************
Synopsis []
@ -1678,8 +1692,12 @@ int Exa3_ManExactSynthesis( Bmc_EsPar_t * pPars )
}
if ( pPars->fVerbose && status != GLUCOSE_UNDEC )
Exa3_ManPrint( p, i, iMint, Abc_Clock() - clkTotal );
if ( iMint == -1 )
if ( iMint == -1 ) {
Exa3_ManPrintSolution( p, fCompl ), Res = 1;
printf( "The variable permutation is \"" );
Exa3_ManPrintPerm(p);
printf( "\".\n" );
}
else if ( status == GLUCOSE_UNDEC )
printf( "The solver timed out after %d sec.\n", pPars->RuntimeLim );
else if ( !p->pPars->fSilent )

18
src/sat/bmc/bmcMaj8.c
View File

@ -419,6 +419,21 @@ static void Exa8_ManPrintSolution( Exa8_Man_t * p, int fCompl )
printf( " )\n" );
}
}
static void Exa8_ManPrintPerm( Exa8_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 = Exa8_ManFindFanin( p, i, k );
if ( iVar >= 0 && iVar < p->nVars )
printf( "%c", 'a'+iVar );
}
}
}
/**Function*************************************************************
@ -714,6 +729,9 @@ int Exa8_ManExactSynthesis( Bmc_EsPar_t * pPars )
if ( DiffMint != -1 )
printf( "Warning: Verification detected a mismatch at minterm %d.\n", DiffMint );
Exa8_ManPrintSolution( p, fCompl );
printf( "The variable permutation is \"" );
Exa8_ManPrintPerm(p);
printf( "\".\n" );
if ( pPars->fDumpBlif )
Exa8_ManDumpBlif( p, fCompl );
Res = 1;