Adding timeout to the interpolant computation procedure.

4 files changed, 23 insertions, 4 deletions

diff --git a/src/aig/aig/aigInter.c b/src/aig/aig/aigInter.c
index 8f9318b3..f09a41f8 100644
--- a/src/aig/aig/aigInter.c
+++ b/src/aig/aig/aigInter.c
@@ -271,7 +271,7 @@ timeSat += Abc_Clock() - clk;
     // create the resulting manager
 clk = Abc_Clock();
     pManInter = Inta_ManAlloc();
-    pRes = (Aig_Man_t *)Inta_ManInterpolate( pManInter, (Sto_Man_t *)pSatCnf, vVarsAB, fVerbose );
+    pRes = (Aig_Man_t *)Inta_ManInterpolate( pManInter, (Sto_Man_t *)pSatCnf, 0, vVarsAB, fVerbose );
     Inta_ManFree( pManInter );
 timeInt += Abc_Clock() - clk;
 /*
diff --git a/src/proof/int/intM114.c b/src/proof/int/intM114.c
index 64b18ae0..e5da012a 100644
--- a/src/proof/int/intM114.c
+++ b/src/proof/int/intM114.c
@@ -304,11 +304,13 @@ clk = Abc_Clock();
 */
 
     pManInterA = Inta_ManAlloc();
-    p->pInterNew = (Aig_Man_t *)Inta_ManInterpolate( pManInterA, (Sto_Man_t *)pSatCnf, p->vVarsAB, 0 );
+    p->pInterNew = (Aig_Man_t *)Inta_ManInterpolate( pManInterA, (Sto_Man_t *)pSatCnf, nTimeNewOut, p->vVarsAB, 0 );
     Inta_ManFree( pManInterA );
 
 p->timeInt += Abc_Clock() - clk;
     Sto_ManFree( (Sto_Man_t *)pSatCnf );
+    if ( p->pInterNew == NULL )
+        RetValue = -1;
     return RetValue;
 }
 
diff --git a/src/sat/bsat/satInterA.c b/src/sat/bsat/satInterA.c
index dabb10a3..b3b4ec7f 100644
--- a/src/sat/bsat/satInterA.c
+++ b/src/sat/bsat/satInterA.c
@@ -948,7 +948,7 @@ void Inta_ManPrepareInter( Inta_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-void * Inta_ManInterpolate( Inta_Man_t * p, Sto_Man_t * pCnf, void * vVarsAB, int fVerbose )
+void * Inta_ManInterpolate( Inta_Man_t * p, Sto_Man_t * pCnf, abctime TimeToStop, void * vVarsAB, int fVerbose )
 {
     Aig_Man_t * pRes;
     Aig_Obj_t * pObj;
@@ -956,6 +956,9 @@ void * Inta_ManInterpolate( Inta_Man_t * p, Sto_Man_t * pCnf, void * vVarsAB, in
     int RetValue = 1;
     abctime clkTotal = Abc_Clock();
 
+    if ( Abc_Clock() > TimeToStop )
+        return NULL;
+
     // check that the CNF makes sense
     assert( pCnf->nVars > 0 && pCnf->nClauses > 0 );
     p->pCnf = pCnf;
@@ -980,7 +983,15 @@ void * Inta_ManInterpolate( Inta_Man_t * p, Sto_Man_t * pCnf, void * vVarsAB, in
 
     // write the root clauses
     Sto_ManForEachClauseRoot( p->pCnf, pClause )
+    {
         Inta_ManProofWriteOne( p, pClause );
+        if ( TimeToStop && Abc_Clock() > TimeToStop )
+        {
+            Aig_ManStop( pRes );
+            p->pAig = NULL;
+            return NULL;
+        }
+    }
 
     // propagate root level assignments
     if ( Inta_ManProcessRoots( p ) )
@@ -995,6 +1006,12 @@ void * Inta_ManInterpolate( Inta_Man_t * p, Sto_Man_t * pCnf, void * vVarsAB, in
                 RetValue = 0;
                 break;
             }
+            if ( TimeToStop && Abc_Clock() > TimeToStop )
+            {
+                Aig_ManStop( pRes );
+                p->pAig = NULL;
+                return NULL;
+            }
         }
     }
 
diff --git a/src/sat/bsat/satStore.h b/src/sat/bsat/satStore.h
index 206c6939..960f391a 100644
--- a/src/sat/bsat/satStore.h
+++ b/src/sat/bsat/satStore.h
@@ -130,7 +130,7 @@ extern int          Int_ManInterpolate( Int_Man_t * p, Sto_Man_t * pCnf, int fVe
 typedef struct Inta_Man_t_ Inta_Man_t;
 extern Inta_Man_t * Inta_ManAlloc();
 extern void         Inta_ManFree( Inta_Man_t * p );
-extern void *       Inta_ManInterpolate( Inta_Man_t * p, Sto_Man_t * pCnf, void * vVarsAB, int fVerbose );
+extern void *       Inta_ManInterpolate( Inta_Man_t * p, Sto_Man_t * pCnf, abctime TimeToStop, void * vVarsAB, int fVerbose );
 
 /*=== satInterB.c ==========================================================*/
 typedef struct Intb_Man_t_ Intb_Man_t;