diff options
| -rw-r--r-- | src/base/abci/abc.c | 2 | ||||
| -rw-r--r-- | src/sat/bmc/bmc.h | 2 | ||||
| -rw-r--r-- | src/sat/bmc/bmcBmcS.c | 7 |
3 files changed, 11 insertions, 0 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 89a3b299..6d22c10f 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -40000,6 +40000,8 @@ int Abc_CommandAbc9SBmc( Abc_Frame_t * pAbc, int argc, char ** argv ) pPars->iFrame = 0; // explored up to this frame pPars->nFailOuts = 0; // the number of failed outputs pPars->nDropOuts = 0; // the number of dropped outputs + pPars->pFuncOnFrameDone = pAbc->pFuncOnFrameDone; // frame done callback + Extra_UtilGetoptReset(); while ( ( c = Extra_UtilGetopt( argc, argv, "CFTvwh" ) ) != EOF ) { 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; } |