diff options
Diffstat (limited to 'src/sat/bmc')
| -rw-r--r-- | src/sat/bmc/bmc.h | 2 | ||||
| -rw-r--r-- | src/sat/bmc/bmcBmcS.c | 7 |
2 files changed, 9 insertions, 0 deletions
diff --git a/src/sat/bmc/bmc.h b/src/sat/bmc/bmc.h index 22ae765d..0c1744de 100644 --- a/src/sat/bmc/bmc.h +++ b/src/sat/bmc/bmc.h @@ -97,6 +97,8 @@ struct Bmc_AndPar_t_ int iFrame; // explored up to this frame int nFailOuts; // the number of failed outputs int nDropOuts; // the number of dropped outputs + + void (*pFuncOnFrameDone)(int, int, int); // callback on each frame status (frame, po, statuss) }; typedef struct Bmc_BCorePar_t_ Bmc_BCorePar_t; 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; } |