Prepared &gla to try abstracting and proving concurrently.

2 files changed, 48 insertions, 26 deletions

diff --git a/src/proof/pdr/pdr.h b/src/proof/pdr/pdr.h
index d245b467..491477dd 100644
--- a/src/proof/pdr/pdr.h
+++ b/src/proof/pdr/pdr.h
@@ -40,20 +40,23 @@ ABC_NAMESPACE_HEADER_START
 typedef struct Pdr_Par_t_ Pdr_Par_t;
 struct Pdr_Par_t_
 {
-    int iOutput;      // zero-based number of primary output to solve
-    int nRecycle;     // limit on vars for recycling
-    int nFrameMax;    // limit on frame count
-    int nConfLimit;   // limit on SAT solver conflicts
-    int nRestLimit;   // limit on the number of proof-obligations
-    int nTimeOut;     // timeout in seconds
-    int fTwoRounds;   // use two rounds for generalization
-    int fMonoCnf;     // monolythic CNF
-    int fDumpInv;     // dump inductive invariant
-    int fShortest;    // forces bug traces to be shortest
-    int fSkipGeneral; // skips expensive generalization step
-    int fVerbose;     // verbose output
-    int fVeryVerbose; // very verbose output
-    int iFrame;       // explored up to this frame
+    int iOutput;          // zero-based number of primary output to solve
+    int nRecycle;         // limit on vars for recycling
+    int nFrameMax;        // limit on frame count
+    int nConfLimit;       // limit on SAT solver conflicts
+    int nRestLimit;       // limit on the number of proof-obligations
+    int nTimeOut;         // timeout in seconds
+    int fTwoRounds;       // use two rounds for generalization
+    int fMonoCnf;         // monolythic CNF
+    int fDumpInv;         // dump inductive invariant
+    int fShortest;        // forces bug traces to be shortest
+    int fSkipGeneral;     // skips expensive generalization step
+    int fVerbose;         // verbose output`
+    int fVeryVerbose;     // very verbose output
+    int fSilent;          // totally silent execution
+    int iFrame;           // explored up to this frame
+    int RunId;            // PDR id in this run 
+    int(*pFuncStop)(int); // callback to terminate
 };
 
 ////////////////////////////////////////////////////////////////////////
@@ -65,8 +68,8 @@ struct Pdr_Par_t_
 ////////////////////////////////////////////////////////////////////////
 
 /*=== pdrCore.c ==========================================================*/
-extern void            Pdr_ManSetDefaultParams( Pdr_Par_t * pPars );
-extern int             Pdr_ManSolve( Aig_Man_t * p, Pdr_Par_t * pPars, Abc_Cex_t ** ppCex );
+extern void               Pdr_ManSetDefaultParams( Pdr_Par_t * pPars );
+extern int                Pdr_ManSolve( Aig_Man_t * p, Pdr_Par_t * pPars, Abc_Cex_t ** ppCex );
 
 
 ABC_NAMESPACE_HEADER_END
diff --git a/src/proof/pdr/pdrCore.c b/src/proof/pdr/pdrCore.c
index 765894e3..5cb05143 100644
--- a/src/proof/pdr/pdrCore.c
+++ b/src/proof/pdr/pdrCore.c
@@ -528,7 +528,9 @@ int Pdr_ManBlockCube( Pdr_Man_t * p, Pdr_Set_t * pCube )
             Pdr_QueuePush( p, pThis );
         }
 
-        // check the timeout
+        // check termination
+        if ( p->pPars->pFuncStop && p->pPars->pFuncStop(p->pPars->RunId) )
+            return -1;
         if ( p->timeToStop && clock() > p->timeToStop )
             return -1;
     }
@@ -565,7 +567,10 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
         {
             if ( p->pPars->fVerbose ) 
                 Pdr_ManPrintProgress( p, 1, clock() - clkStart );
-            Abc_Print( 1, "Reached conflict limit (%d).\n",  p->pPars->nConfLimit );
+                if ( p->pPars->nConfLimit )
+                    Abc_Print( 1, "Reached conflict limit (%d).\n",  p->pPars->nConfLimit );
+                else if ( p->pPars->fVerbose ) 
+                    Abc_Print( 1, "Computation cancelled by the callback.\n" );
             p->pPars->iFrame = k;
             return -1;
         }
@@ -576,7 +581,10 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
             {
                 if ( p->pPars->fVerbose ) 
                     Pdr_ManPrintProgress( p, 1, clock() - clkStart );
-                Abc_Print( 1, "Reached conflict limit (%d).\n",  p->pPars->nConfLimit );
+                if ( p->pPars->nConfLimit )
+                    Abc_Print( 1, "Reached conflict limit (%d).\n",  p->pPars->nConfLimit );
+                else if ( p->pPars->fVerbose ) 
+                    Abc_Print( 1, "Computation cancelled by the callback.\n" );
                 p->pPars->iFrame = k;
                 return -1;
             }
@@ -615,7 +623,8 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
             {
                 if ( p->pPars->fVerbose ) 
                     Pdr_ManPrintProgress( p, 1, clock() - clkStart );
-                Abc_Print( 1, "Reached conflict limit (%d).\n",  p->pPars->nConfLimit );
+                if ( !p->pPars->fSilent )
+                    Abc_Print( 1, "Reached conflict limit (%d).\n",  p->pPars->nConfLimit );
                 p->pPars->iFrame = k;
                 return -1;
             }
@@ -623,8 +632,10 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
             {
                 if ( p->pPars->fVerbose ) 
                     Pdr_ManPrintProgress( p, 1, clock() - clkStart );
-                Pdr_ManReportInvariant( p );
-                Pdr_ManVerifyInvariant( p );
+                if ( !p->pPars->fSilent )
+                    Pdr_ManReportInvariant( p );
+                if ( !p->pPars->fSilent )
+                    Pdr_ManVerifyInvariant( p );
                 p->pPars->iFrame = k;
                 return 1; // UNSAT
             }
@@ -633,7 +644,12 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
 //            clkStart = clock();
         }
 
-        // check the timeout
+        // check termination
+        if ( p->pPars->pFuncStop && p->pPars->pFuncStop(p->pPars->RunId) )
+        {
+            p->pPars->iFrame = k;
+            return -1;
+        }
         if ( p->timeToStop && clock() > p->timeToStop )
         {
             if ( fPrintClauses )
@@ -643,7 +659,8 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
             }
             if ( p->pPars->fVerbose ) 
                 Pdr_ManPrintProgress( p, 1, clock() - clkStart );
-            Abc_Print( 1, "Reached timeout (%d seconds).\n",  p->pPars->nTimeOut );
+            if ( !p->pPars->fSilent )
+                Abc_Print( 1, "Reached timeout (%d seconds).\n",  p->pPars->nTimeOut );
             p->pPars->iFrame = k;
             return -1;
         }
@@ -651,7 +668,8 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
         {
             if ( p->pPars->fVerbose ) 
                 Pdr_ManPrintProgress( p, 1, clock() - clkStart );
-            Abc_Print( 1, "Reached limit on the number of timeframes (%d).\n", p->pPars->nFrameMax );
+            if ( !p->pPars->fSilent )
+                Abc_Print( 1, "Reached limit on the number of timeframes (%d).\n", p->pPars->nFrameMax );
             p->pPars->iFrame = k;
             return -1;
         } 
@@ -677,7 +695,8 @@ int Pdr_ManSolve_( Aig_Man_t * pAig, Pdr_Par_t * pPars, Vec_Int_t ** pvPrioInit,
     clock_t clk = clock();
     p = Pdr_ManStart( pAig, pPars, pvPrioInit? *pvPrioInit : NULL );
     RetValue = Pdr_ManSolveInt( p );
-    *ppCex = RetValue ? NULL : Pdr_ManDeriveCex( p );
+    if ( ppCex )
+        *ppCex = RetValue ? NULL : Pdr_ManDeriveCex( p );
     if ( p->pPars->fDumpInv )
         Pdr_ManDumpClauses( p, (char *)"inv.pla", RetValue==1 );
 //    if ( *ppCex && pPars->fVerbose )