Adding timeout to AIG rewriting inside 'int'.

6 files changed, 51 insertions, 1 deletions

diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h
index 697238ae..2a1e7d7d 100644
--- a/src/aig/aig/aig.h
+++ b/src/aig/aig/aig.h
@@ -160,6 +160,7 @@ struct Aig_Man_t_
     Vec_Int_t *      vProbs;         // probability of node being 1 
     Vec_Int_t *      vCiNumsOrig;    // original CI names
     int              nComplEdges;    // complemented edges
+    abctime          Time2Quit;
     // timing statistics
     abctime          time1;
     abctime          time2;
diff --git a/src/opt/dar/darBalance.c b/src/opt/dar/darBalance.c
index c2ebfc61..01cd7953 100644
--- a/src/opt/dar/darBalance.c
+++ b/src/opt/dar/darBalance.c
@@ -521,6 +521,8 @@ Aig_Obj_t * Dar_Balance_rec( Aig_Man_t * pNew, Aig_Obj_t * pObjOld, Vec_Vec_t *
     for ( i = 0; i < Vec_PtrSize(vSuper); i++ )
     {
         pObjNew = Dar_Balance_rec( pNew, Aig_Regular((Aig_Obj_t *)vSuper->pArray[i]), vStore, Level + 1, fUpdateLevel );
+        if ( pObjNew == NULL )
+            return NULL;
         vSuper->pArray[i] = Aig_NotCond( pObjNew, Aig_IsComplement((Aig_Obj_t *)vSuper->pArray[i]) );
     }
     // build the supergate
@@ -529,6 +531,8 @@ Aig_Obj_t * Dar_Balance_rec( Aig_Man_t * pNew, Aig_Obj_t * pObjOld, Vec_Vec_t *
 #else
     pObjNew = Dar_BalanceBuildSuper( pNew, vSuper, Aig_ObjType(pObjOld), fUpdateLevel );
 #endif
+    if ( pNew->Time2Quit && !(Aig_Regular(pObjNew)->Id & 255) && Abc_Clock() > pNew->Time2Quit )
+        return NULL;
     // make sure the balanced node is not assigned
 //    assert( pObjOld->Level >= Aig_Regular(pObjNew)->Level );
     assert( pObjOld->pData == NULL );
@@ -559,6 +563,7 @@ Aig_Man_t * Dar_ManBalance( Aig_Man_t * p, int fUpdateLevel )
     pNew->pSpec = Abc_UtilStrsav( p->pSpec );
     pNew->nAsserts = p->nAsserts;
     pNew->nConstrs = p->nConstrs;
+    pNew->Time2Quit = p->Time2Quit;
     if ( p->vFlopNums )
         pNew->vFlopNums = Vec_IntDup( p->vFlopNums );
     // map the PI nodes
@@ -588,6 +593,12 @@ Aig_Man_t * Dar_ManBalance( Aig_Man_t * p, int fUpdateLevel )
                 // perform balancing
                 pDriver = Aig_ObjReal_rec( Aig_ObjChild0(pObj) );
                 pObjNew = Dar_Balance_rec( pNew, Aig_Regular(pDriver), vStore, 0, fUpdateLevel );
+                if ( pObjNew == NULL )
+                {
+                    Vec_VecFree( vStore );
+                    Aig_ManStop( pNew );
+                    return NULL;
+                }
                 pObjNew = Aig_NotCond( pObjNew, Aig_IsComplement(pDriver) );
                 // save arrival time of the output
                 arrTime = (float)Aig_Regular(pObjNew)->Level;
@@ -613,6 +624,12 @@ Aig_Man_t * Dar_ManBalance( Aig_Man_t * p, int fUpdateLevel )
         {
             pDriver = Aig_ObjReal_rec( Aig_ObjChild0(pObj) );
             pObjNew = Dar_Balance_rec( pNew, Aig_Regular(pDriver), vStore, 0, fUpdateLevel );
+            if ( pObjNew == NULL )
+            {
+                Vec_VecFree( vStore );
+                Aig_ManStop( pNew );
+                return NULL;
+            }
             pObjNew = Aig_NotCond( pObjNew, Aig_IsComplement(pDriver) );
             pObjNew = Aig_ObjCreateCo( pNew, pObjNew );
         }
diff --git a/src/opt/dar/darCore.c b/src/opt/dar/darCore.c
index 17074123..24e5a741 100644
--- a/src/opt/dar/darCore.c
+++ b/src/opt/dar/darCore.c
@@ -112,6 +112,8 @@ int Dar_ManRewrite( Aig_Man_t * pAig, Dar_RwrPar_t * pPars )
 //    Aig_ManOrderStart( pAig );
 //    Aig_ManForEachNodeInOrder( pAig, pObj )
     {
+        if ( pAig->Time2Quit && !(i & 256) && Abc_Clock() > pAig->Time2Quit )
+            break;
 //        Bar_ProgressUpdate( pProgress, 100*pAig->nAndPrev/pAig->nAndTotal, NULL );
 //        Bar_ProgressUpdate( pProgress, i, NULL );
         if ( !Aig_ObjIsNode(pObj) )
diff --git a/src/opt/dar/darRefact.c b/src/opt/dar/darRefact.c
index 45e150c4..6083c035 100644
--- a/src/opt/dar/darRefact.c
+++ b/src/opt/dar/darRefact.c
@@ -526,6 +526,8 @@ int Dar_ManRefactor( Aig_Man_t * pAig, Dar_RefPar_t * pPars )
             continue;
         if ( i > nNodesOld )
             break;
+        if ( pAig->Time2Quit && !(i & 256) && Abc_Clock() > pAig->Time2Quit )
+            break;
         Vec_VecClear( p->vCuts );
 
 //printf( "\nConsidering node %d.\n", pObj->Id );
diff --git a/src/opt/dar/darScript.c b/src/opt/dar/darScript.c
index f1a30a82..f8fa3788 100644
--- a/src/opt/dar/darScript.c
+++ b/src/opt/dar/darScript.c
@@ -72,6 +72,7 @@ Aig_Man_t * Dar_ManRwsat( Aig_Man_t * pAig, int fBalance, int fVerbose )
 //alias rwsat       "st; rw -l; b -l; rw -l; rf -l"
 {
     Aig_Man_t * pTemp;
+    abctime Time = pAig->Time2Quit;
 
     Dar_RwrPar_t ParsRwr, * pParsRwr = &ParsRwr;
     Dar_RefPar_t ParsRef, * pParsRef = &ParsRef;
@@ -92,41 +93,56 @@ Aig_Man_t * Dar_ManRwsat( Aig_Man_t * pAig, int fBalance, int fVerbose )
     // balance
     if ( fBalance )
     {
+    pAig->Time2Quit = Time;
     pAig = Dar_ManBalance( pTemp = pAig, 0 );
     Aig_ManStop( pTemp );
     if ( fVerbose ) printf( "Balance:   " ), Aig_ManPrintStats( pAig );
+    if ( Time && Abc_Clock() > Time )
+        { if ( pAig ) Aig_ManStop( pAig ); return NULL; }
     }
    
 //Aig_ManDumpBlif( pAig, "inter.blif", NULL, NULL );
 //printf( "3" );
     // rewrite
+    pAig->Time2Quit = Time;
     Dar_ManRewrite( pAig, pParsRwr );
     pAig = Aig_ManDupDfs( pTemp = pAig ); 
     Aig_ManStop( pTemp );
     if ( fVerbose ) printf( "Rewrite:   " ), Aig_ManPrintStats( pAig );
+    if ( Time && Abc_Clock() > Time )
+        { if ( pAig ) Aig_ManStop( pAig ); return NULL; }
 
 //printf( "4" );
     // refactor
+    pAig->Time2Quit = Time;
     Dar_ManRefactor( pAig, pParsRef );
     pAig = Aig_ManDupDfs( pTemp = pAig ); 
     Aig_ManStop( pTemp );
     if ( fVerbose ) printf( "Refactor:  " ), Aig_ManPrintStats( pAig );
+    if ( Time && Abc_Clock() > Time )
+        { if ( pAig ) Aig_ManStop( pAig ); return NULL; }
 
 //printf( "5" );
     // balance
     if ( fBalance )
     {
+    pAig->Time2Quit = Time;
     pAig = Dar_ManBalance( pTemp = pAig, 0 );
     Aig_ManStop( pTemp );
     if ( fVerbose ) printf( "Balance:   " ), Aig_ManPrintStats( pAig );
+    if ( Time && Abc_Clock() > Time )
+        { if ( pAig ) Aig_ManStop( pAig ); return NULL; }
     }
-    
+
 //printf( "6" );
     // rewrite
+    pAig->Time2Quit = Time;
     Dar_ManRewrite( pAig, pParsRwr );
     pAig = Aig_ManDupDfs( pTemp = pAig ); 
     Aig_ManStop( pTemp );
     if ( fVerbose ) printf( "Rewrite:   " ), Aig_ManPrintStats( pAig );
+    if ( Time && Abc_Clock() > Time )
+        { if ( pAig ) Aig_ManStop( pAig ); return NULL; }
 
 //printf( "7" );
     return pAig;
diff --git a/src/proof/int/intCore.c b/src/proof/int/intCore.c
index dedf987e..1418402c 100644
--- a/src/proof/int/intCore.c
+++ b/src/proof/int/intCore.c
@@ -280,10 +280,22 @@ p->timeEqu += Abc_Clock() - clk;
 clk = Abc_Clock();
             if ( p->pInterNew )
             {
+                Abc_PrintTime( 1, "Before time", clock() - clkTotal );
+                // save the timeout value
+                p->pInterNew->Time2Quit = nTimeNewOut;
 //                Ioa_WriteAiger( p->pInterNew, "interpol.aig", 0, 0 );
                 p->pInterNew = Dar_ManRwsat( pAigTemp = p->pInterNew, 1, 0 );
 //                p->pInterNew = Dar_ManRwsat( pAigTemp = p->pInterNew, 0, 0 );
+                Abc_PrintTime( 1, "After time", clock() - clkTotal );
                 Aig_ManStop( pAigTemp );
+                if ( p->pInterNew == NULL )
+                {
+                    printf( "Reached timeout (%d seconds) during rewriting.\n",  pPars->nSecLimit );
+                    p->timeTotal = Abc_Clock() - clkTotal;
+                    Inter_ManStop( p, 1 );
+                    Inter_CheckStop( pCheck );
+                    return -1;
+                }
             }
 p->timeRwr += Abc_Clock() - clk;