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

Update to "lutexact".

This commit is contained in:
Alan Mishchenko 2024-11-10 19:12:40 -08:00
parent aeb977286f
commit f2e4ceb0e3
1 changed files with 8 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -953,7 +953,7 @@ void Exa_ManExactSynthesis( Bmc_EsPar_t * pPars )
}
if ( status == GLUCOSE_UNDEC )
{
printf( "The problem timed out after %d sec.\n", pPars->RuntimeLim );
printf( "The solver timed out after %d sec.\n", pPars->RuntimeLim );
break;
}
iMint = Exa_ManEval( p );
@ -1544,7 +1544,7 @@ int Exa3_ManExactSynthesis( Bmc_EsPar_t * pPars )
if ( iMint == -1 )
Exa3_ManPrintSolution( p, fCompl ), Res = 1;
else if ( status == GLUCOSE_UNDEC )
printf( "The problem timed out after %d sec.\n", pPars->RuntimeLim );
printf( "The solver timed out after %d sec.\n", pPars->RuntimeLim );
else
printf( "The problem has no solution.\n" );
printf( "Added = %d. Tried = %d. ", p->nUsed[1], p->nUsed[0] );
@ -1577,10 +1577,14 @@ void Exa3_ManExactSynthesisRand( Bmc_EsPar_t * pPars )
}
pPars->pTtStr = ABC_CALLOC( char, pPars->nVars > 2 ? (1 << (pPars->nVars-2)) + 1 : 2 );
Extra_PrintHexadecimalString( pPars->pTtStr, (unsigned *)pFun, pPars->nVars );
printf( "Generated random function: %s\n", pPars->pTtStr );
printf( "\nIteration %d : ", i );
if ( pPars->nMintNum )
printf( "Random function has %d positive minterms.", pPars->nMintNum );
printf( "\n" );
if ( pPars->fVerbose )
printf( "Truth table : %s\n", pPars->pTtStr );
nDecs += Exa3_ManExactSynthesis( pPars );
ABC_FREE( pPars->pTtStr );
printf( "\n" );
}
printf( "Decomposable are %d (out of %d) functions (%.2f %%).\n", nDecs, pPars->nRandFuncs, 100.0*nDecs/pPars->nRandFuncs );
ABC_FREE( pFun );