From cf427690a5df7decdfb6dd21d076e68415b82f46 Mon Sep 17 00:00:00 2001 From: Baruch Sterin Date: Wed, 9 Aug 2017 12:01:07 -0700 Subject: add frame done callback support for command &bmcs --- src/sat/bmc/bmcBmcS.c | 7 +++++++ 1 file changed, 7 insertions(+) (limited to 'src/sat/bmc/bmcBmcS.c') 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; } -- cgit v1.2.3