diff options
| author | Baruch Sterin <baruchs@gmail.com> | 2017-08-09 12:01:07 -0700 |
|---|---|---|
| committer | Baruch Sterin <baruchs@gmail.com> | 2017-08-09 12:01:07 -0700 |
| commit | cf427690a5df7decdfb6dd21d076e68415b82f46 (patch) | |
| tree | 918708d5164690be89061edf1af2bb0f286a0071 /src/sat/bmc/bmcBmcS.c | |
| parent | 590ae696526823709bd6c38726c1c21695babe15 (diff) | |
| download | abc-cf427690a5df7decdfb6dd21d076e68415b82f46.tar.gz abc-cf427690a5df7decdfb6dd21d076e68415b82f46.tar.bz2 abc-cf427690a5df7decdfb6dd21d076e68415b82f46.zip | |
add frame done callback support for command &bmcs
Diffstat (limited to 'src/sat/bmc/bmcBmcS.c')
| -rw-r--r-- | src/sat/bmc/bmcBmcS.c | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/src/sat/bmc/bmcBmcS.c b/src/sat/bmc/bmcBmcS.c index d6452340..e22796d3 100644 --- a/src/sat/bmc/bmcBmcS.c +++ b/src/sat/bmc/bmcBmcS.c @@ -551,6 +551,9 @@ int Bmcs_ManPerform( Gia_Man_t * pGia, Bmc_AndPar_t * pPars ) if ( pCnf == NULL ) { Bmcs_ManPrintFrame( p, f, nClauses, clkStart ); + if( pPars->pFuncOnFrameDone) + for ( i = 0; i < Gia_ManPoNum(pGia); i++ ) + pPars->pFuncOnFrameDone(f, i, 0); continue; } nClauses += pCnf->nClauses; @@ -571,6 +574,8 @@ int Bmcs_ManPerform( Gia_Man_t * pGia, Bmc_AndPar_t * pPars ) if ( status == SATOKO_UNSAT ) { Bmcs_ManPrintFrame( p, f, nClauses, clkStart ); + if( pPars->pFuncOnFrameDone) + pPars->pFuncOnFrameDone(f, i, 0); continue; } if ( status == SATOKO_SAT ) @@ -586,6 +591,8 @@ int Bmcs_ManPerform( Gia_Man_t * pGia, Bmc_AndPar_t * pPars ) fflush( stdout ); pGia->pCexSeq = Bmcs_ManGenerateCex( p, i, f ); } + if( pPars->pFuncOnFrameDone) + pPars->pFuncOnFrameDone(f, i, 1); } break; } |