The-OpenROAD-Project/abc
1
0
Fork 0
mirror of https://github.com/The-OpenROAD-Project/abc.git synced 2026-03-12 11:26:17 +08:00
Code Issues Actions Packages Projects Releases Wiki Activity

Changes to "lutexact".

Browse Source
This commit is contained in:
Alan Mishchenko
2025-11-11 06:55:24 -08:00
parent 169e288fc4
commit 91d2f3d7e8
2 changed files with 8 additions and 4 deletions
Download Patch File Download Diff File Expand all files Collapse all files

6
src/base/abci/abc.c
View File

@@ -10826,11 +10826,15 @@ int Abc_CommandLutExact( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -1, "Truth table should be given on the command line.\n" );
return 1;
}
if ( pPars->nVars == 0 && pPars->pTtStr )
pPars->nVars = 2 + Abc_Base2Log((int)strlen(pPars->pTtStr));
if ( pPars->pTtStr && (1 << (pPars->nVars-2)) != (int)strlen(pPars->pTtStr) )
{
Abc_Print( -1, "Truth table is expected to have %d hex digits (instead of %d).\n", (1 << (pPars->nVars-2)), strlen(pPars->pTtStr) );
return 1;
}
if ( pPars->nVars == 0 && pPars->pSymStr )
pPars->nVars = (int)strlen(pPars->pSymStr) - 1;
if ( pPars->pSymStr && pPars->nVars+1 != strlen(pPars->pSymStr) )
{
Abc_Print( -1, "The char string of the %d-variable symmetric function should have %d zeros and ones (instead of %d).\n", pPars->nVars, pPars->nVars+1, strlen(pPars->pSymStr) );
@@ -10843,7 +10847,7 @@ int Abc_CommandLutExact( Abc_Frame_t * pAbc, int argc, char ** argv )
}
if ( pPars->nVars > 12 )
{
Abc_Print( -1, "Function should not have more than 10 inputs.\n" );
Abc_Print( -1, "Function should not have more than 12 inputs.\n" );
return 1;
}
if ( pPars->nLutSize > 6 )

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

@@ -1291,7 +1291,7 @@ static void Exa3_ManPrintSolution( Exa3_Man_t * p, int fCompl )
for ( i = p->nObjs - 1; i >= p->nVars; i-- )
{
int Val, iVarStart = 1 + p->LutMask*(i - p->nVars);
printf( "%02d = %d\'b", i, 1 << p->nLutSize );
printf( "%c = %d\'b", 'A'+i-p->nVars, 1 << p->nLutSize );
for ( k = p->LutMask - 1; k >= 0; k-- )
{
Val = bmcg_sat_solver_read_cex_varvalue(p->pSat, iVarStart+k);
@@ -1311,7 +1311,7 @@ static void Exa3_ManPrintSolution( Exa3_Man_t * p, int fCompl )
if ( iVar >= 0 && iVar < p->nVars )
printf( " %c", 'a'+iVar );
else
printf( " %02d", iVar );
printf( " %c", 'A'+iVar-p->nVars );
}
printf( " )\n" );
}
@@ -1332,7 +1332,7 @@ static void Exa3_ManDumpBlif( Exa3_Man_t * p, int fCompl )
{
int i, k, b, iVar;
char pFileName[1000];
char * pStr = Abc_UtilStrsav(p->pPars->pTtStr);
char * pStr = Abc_UtilStrsav(p->pPars->pSymStr ? p->pPars->pSymStr : p->pPars->pTtStr);
if ( strlen(pStr) > 16 ) {
pStr[16] = '_';
pStr[17] = '\0';