%pdra: added top level callbacks

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;

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