From 51fbf37cb42951c668e9fa4df9ddd99897a6fb4d Mon Sep 17 00:00:00 2001
From: Yen-Sheng Ho <ysho@berkeley.edu>
Date: Sun, 19 Mar 2017 12:41:06 -0700
Subject: %pdra: working on bmc3

---
 src/sat/bmc/bmc.h     | 2 ++
 src/sat/bmc/bmcBmc3.c | 6 ++++++
 2 files changed, 8 insertions(+)

(limited to 'src/sat/bmc')

diff --git a/src/sat/bmc/bmc.h b/src/sat/bmc/bmc.h
index a3f353c2..22ae765d 100644
--- a/src/sat/bmc/bmc.h
+++ b/src/sat/bmc/bmc.h
@@ -73,6 +73,8 @@ struct Saig_ParBmc_t_
     int         nDropOuts;      // the number of dropped outputs
     abctime     timeLastSolved; // the time when the last output was solved
     int(*pFuncOnFail)(int,Abc_Cex_t*); // called for a failed output in MO mode
+    int         RunId;          // BMC id in this run 
+    int(*pFuncStop)(int);       // callback to terminate
 };
 
  
diff --git a/src/sat/bmc/bmcBmc3.c b/src/sat/bmc/bmcBmc3.c
index ccd0bb90..34fdf45f 100644
--- a/src/sat/bmc/bmcBmc3.c
+++ b/src/sat/bmc/bmcBmc3.c
@@ -1533,6 +1533,12 @@ clkOther += Abc_Clock() - clk2;
                     Abc_Print( 1, "Reached timeout (%d seconds).\n",  pPars->nTimeOut );
                 goto finish;
             }
+            if ( p->pPars->pFuncStop && p->pPars->pFuncStop(p->pPars->RunId) )
+            {
+                if ( !pPars->fSilent )
+                    Abc_Print( 1, "Bmc3 got callbacks.\n" );
+                goto finish;
+            }
             // skip solved outputs
             if ( p->vCexes && Vec_PtrEntry(p->vCexes, i) )
                 continue;
-- 
cgit v1.2.3