From 3401ed364bd031aca55d076afa50752293be497e Mon Sep 17 00:00:00 2001
From: Yen-Sheng Ho <ysho@berkeley.edu>
Date: Sun, 9 Apr 2017 14:38:37 -0700
Subject: %pdra: added top level callbacks

---
 src/base/wlc/wlc.h    | 2 ++
 src/base/wlc/wlcAbs.c | 4 +++-
 2 files changed, 5 insertions(+), 1 deletion(-)

diff --git a/src/base/wlc/wlc.h b/src/base/wlc/wlc.h
index eb8f4aa4..229a6bfb 100644
--- a/src/base/wlc/wlc.h
+++ b/src/base/wlc/wlc.h
@@ -185,6 +185,8 @@ struct Wlc_Par_t_
     int                    fShrinkScratch;     // Restart pdr from scratch after shrinking
     int                    fVerbose;           // verbose output
     int                    fPdrVerbose;        // verbose output
+    int                    RunId;              // id in this run 
+    int                    (*pFuncStop)(int);  // callback to terminate
 };
 
 typedef struct Wla_Man_t_ Wla_Man_t;
diff --git a/src/base/wlc/wlcAbs.c b/src/base/wlc/wlcAbs.c
index e355c313..3a8ff704 100644
--- a/src/base/wlc/wlcAbs.c
+++ b/src/base/wlc/wlcAbs.c
@@ -1659,6 +1659,8 @@ Wla_Man_t * Wla_ManStart( Wlc_Ntk_t * pNtk, Wlc_Par_t * pPars )
     Pdr_ManSetDefaultParams( pPdrPars );
     pPdrPars->fVerbose   = pPars->fPdrVerbose;
     pPdrPars->fVeryVerbose = 0;
+    pPdrPars->pFuncStop  = pPars->pFuncStop;
+    pPdrPars->RunId      = pPars->RunId;
     if ( pPars->fPdra )
     {
         pPdrPars->fUseAbs    = 1;   // use 'pdr -t'  (on-the-fly abstraction)
@@ -1713,7 +1715,7 @@ int Wla_ManSolve( Wla_Man_t * pWla, Wlc_Par_t * pPars )
         RetValue = Wla_ManSolveInt( pWla, pAig );
         Aig_ManStop( pAig );
 
-        if ( RetValue != -1 )
+        if ( RetValue != -1 || pPars->pFuncStop( pPars->RunId) )
             break;
 
         Wla_ManRefine( pWla );
-- 
cgit v1.2.3