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

Added bridge integration for multi-output 'bmc3 -a'.

This commit is contained in:
Alan Mishchenko 2013-09-17 23:25:15 -07:00
parent d4bd7846c3
commit 080a7420fc
1 changed files with 5 additions and 8 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

13
src/sat/bmc/bmcBmc3.c
View File

@ -1300,6 +1300,7 @@ int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars )
{
Gia_ManBmc_t * p;
Aig_Obj_t * pObj;
Abc_Cex_t * pCexNew;
unsigned * pInfo;
int RetValue = -1, fFirst = 1, nJumpFrame = 0, fUnfinished = 0;
int nOutDigits = Abc_Base10Log( Saig_ManPoNum(pAig) );
@ -1426,12 +1427,10 @@ clkOther += Abc_Clock() - clk2;
nOutDigits, i, f, nOutDigits, pPars->nFailOuts, nOutDigits, Saig_ManPoNum(pAig) );
if ( p->vCexes == NULL )
p->vCexes = Vec_PtrStart( Saig_ManPoNum(pAig) );
pCexNew = (p->pPars->fUseBridge || pPars->fStoreCex) ? Abc_CexMakeTriv( Aig_ManRegNum(pAig), Saig_ManPiNum(pAig), Saig_ManPoNum(pAig), f*Saig_ManPoNum(pAig)+i ) : (void *)(ABC_PTRINT_T)1;
if ( p->pPars->fUseBridge )
{
Abc_Cex_t * pCexNew = Abc_CexMakeTriv( Aig_ManRegNum(pAig), Saig_ManPiNum(pAig), Saig_ManPoNum(pAig), f*Saig_ManPoNum(pAig)+i );
Gia_ManToBridgeResult( stdout, 0, pCexNew, pCexNew->iPo );
}
Vec_PtrWriteEntry( p->vCexes, i, pPars->fStoreCex ? Abc_CexMakeTriv( Aig_ManRegNum(pAig), Saig_ManPiNum(pAig), Saig_ManPoNum(pAig), f*Saig_ManPoNum(pAig)+i ) : (void *)(ABC_PTRINT_T)1 );
Vec_PtrWriteEntry( p->vCexes, i, pCexNew );
if ( pPars->pFuncOnFail && pPars->pFuncOnFail(i, pPars->fStoreCex ? (Abc_Cex_t *)Vec_PtrEntry(p->vCexes, i) : NULL) )
{
Abc_Print( 1, "Quitting due to callback on fail.\n" );
@ -1521,12 +1520,10 @@ nTimeSat += Abc_Clock() - clk2;
nOutDigits, i, f, nOutDigits, pPars->nFailOuts, nOutDigits, Saig_ManPoNum(pAig) );
if ( p->vCexes == NULL )
p->vCexes = Vec_PtrStart( Saig_ManPoNum(pAig) );
pCexNew = (p->pPars->fUseBridge || pPars->fStoreCex) ? Saig_ManGenerateCex( p, f, i ) : (void *)(ABC_PTRINT_T)1;
if ( p->pPars->fUseBridge )
{
Abc_Cex_t * pCexNew = Saig_ManGenerateCex( p, f, i );
Gia_ManToBridgeResult( stdout, 0, pCexNew, pCexNew->iPo );
}
Vec_PtrWriteEntry( p->vCexes, i, pPars->fStoreCex? Saig_ManGenerateCex( p, f, i ) : (void *)(ABC_PTRINT_T)1 );
Vec_PtrWriteEntry( p->vCexes, i, pCexNew );
if ( pPars->pFuncOnFail && pPars->pFuncOnFail(i, pPars->fStoreCex ? (Abc_Cex_t *)Vec_PtrEntry(p->vCexes, i) : NULL) )
{
Abc_Print( 1, "Quitting due to callback on fail.\n" );