add frame done callback support for command &bmcs

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 )
     {

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;

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;
         }