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/base/wlc/wlcAbs.c | 15 +++++++++++----
 src/sat/bmc/bmc.h     |  2 ++
 src/sat/bmc/bmcBmc3.c |  6 ++++++
 3 files changed, 19 insertions(+), 4 deletions(-)

diff --git a/src/base/wlc/wlcAbs.c b/src/base/wlc/wlcAbs.c
index b58ef5b5..8f3fe92f 100644
--- a/src/base/wlc/wlcAbs.c
+++ b/src/base/wlc/wlcAbs.c
@@ -87,6 +87,7 @@ typedef struct Bmc3_ThData_t_
     Aig_Man_t *  pAig;
     Abc_Cex_t ** ppCex;
     int          RunId;
+    int          fVerbose;
 } Bmc3_ThData_t;
 
 // mutext to control access to shared variables
@@ -1334,6 +1335,8 @@ void * Wla_Bmc3Thread ( void * pArg )
     Abc_Ntk_t * pAbcNtk = Abc_NtkFromAigPhase( pData->pAig );
     Saig_ParBmc_t BmcPars, *pBmcPars = &BmcPars;
     Saig_ParBmcSetDefaultParams( pBmcPars );
+    pBmcPars->pFuncStop = Wla_CallBackToStop;
+    pBmcPars->RunId = pData->RunId;
 
     RetValue = Abc_NtkDarBmc3( pAbcNtk, pBmcPars, 0 );
 
@@ -1342,7 +1345,9 @@ void * Wla_Bmc3Thread ( void * pArg )
         assert( pAbcNtk->pSeqModel );
         *(pData->ppCex) = pAbcNtk->pSeqModel;
         pAbcNtk->pSeqModel = NULL;
-        Abc_Print( 1, "BMC3 found CEX. RunId=%d.\n", pData->RunId );
+
+        if ( pData->fVerbose )
+            Abc_Print( 1, "Bmc3 found CEX. RunId=%d.\n", pData->RunId );
 
         status = pthread_mutex_lock(&g_mutex);  assert( status == 0 );
         ++g_nRunIds;
@@ -1350,7 +1355,8 @@ void * Wla_Bmc3Thread ( void * pArg )
     }
     else
     {
-        Abc_Print( 1, "BMC3 got cancelled. RunId=%d.\n", pData->RunId );
+        if ( pData->fVerbose )
+            Abc_Print( 1, "Bmc3 was cancelled. RunId=%d.\n", pData->RunId );
     }
 
     // free memory
@@ -1364,7 +1370,7 @@ void * Wla_Bmc3Thread ( void * pArg )
     return NULL;
 }
 
-void Wla_ManConcurrentBmc3( pthread_t * pThread, Aig_Man_t * pAig, Abc_Cex_t ** ppCex )
+void Wla_ManConcurrentBmc3( pthread_t * pThread, Aig_Man_t * pAig, Abc_Cex_t ** ppCex, int fVerbose )
 {
     int status;
 
@@ -1373,6 +1379,7 @@ void Wla_ManConcurrentBmc3( pthread_t * pThread, Aig_Man_t * pAig, Abc_Cex_t **
     pData->pAig = pAig;
     pData->ppCex = ppCex;
     pData->RunId = g_nRunIds;
+    pData->fVerbose = fVerbose;
 
     status = pthread_create( pThread, NULL, Wla_Bmc3Thread, pData );
     assert( status == 0 );
@@ -1410,7 +1417,7 @@ int Wla_ManSolve( Wla_Man_t * pWla, Aig_Man_t * pAig )
         pWla->pPdrPars->pFuncStop = Wla_CallBackToStop;
 
         pBmc3Thread = ABC_CALLOC( pthread_t, 1 );
-        Wla_ManConcurrentBmc3( pBmc3Thread, Aig_ManDupSimple( pAig ), &pBmcCex );
+        Wla_ManConcurrentBmc3( pBmc3Thread, Aig_ManDupSimple( pAig ), &pBmcCex, pWla->pPars->fVerbose );
     }
 
     clk = Abc_Clock();
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