Improved timeout in &reachp.

src/aig/llb/llb2Core.c

@@ -207,22 +207,35 @@ int Llb_CoreReachability_int( Llb_Img_t * p, Vec_Ptr_t * vQuant0, Vec_Ptr_t * vQ
     int * pGlo2Loc  = p->pPars->fBackward? Vec_IntArray( p->vGlo2Ns ) : Vec_IntArray( p->vGlo2Cs );
     DdNode * bCurrent, * bReached, * bNext, * bTemp;
     int clk2, clk = clock(), nIters, nBddSize, iOutFail = -1;
-
+/*
     // compute time to stop
     if ( p->pPars->TimeLimit )
         p->pPars->TimeTarget = clock() + p->pPars->TimeLimit * CLOCKS_PER_SEC;
     else
         p->pPars->TimeTarget = 0;
+*/
+
+    if ( p->pPars->TimeLimit && clock() >= p->pPars->TimeTarget )
+    {
+        if ( !p->pPars->fSilent )
+            printf( "Reached timeout (%d seconds) before image computation.\n", p->pPars->TimeLimit );
+        return -1;
+    }
+
+    // set the stop time parameter
+    p->dd->TimeStop  = p->pPars->TimeTarget;
+    p->ddG->TimeStop = p->pPars->TimeTarget;
+    p->ddR->TimeStop = p->pPars->TimeTarget;
 
     // compute initial states
     if ( p->pPars->fBackward )
     {
         // create init state in the global manager
-        bTemp = Llb_BddComputeBad( p->pInit, p->ddR, p->pPars->TimeLimit );   
+        bTemp = Llb_BddComputeBad( p->pInit, p->ddR, p->pPars->TimeTarget );   
         if ( bTemp == NULL )
         {
             if ( !p->pPars->fSilent )
-                printf( "Reached timeout (%d seconds) during constructing the bad states.\n", p->pPars->TimeLimit );
+                printf( "Reached timeout (%d seconds) while computing bad states.\n", p->pPars->TimeLimit );
             return -1;
         }
         Cudd_Ref( bTemp );
@@ -238,11 +251,11 @@ int Llb_CoreReachability_int( Llb_Img_t * p, Vec_Ptr_t * vQuant0, Vec_Ptr_t * vQ
     else
     {
         // create bad state in the ring manager
-        p->ddR->bFunc = Llb_BddComputeBad( p->pInit, p->ddR, p->pPars->TimeLimit );  
+        p->ddR->bFunc = Llb_BddComputeBad( p->pInit, p->ddR, p->pPars->TimeTarget );  
         if ( p->ddR->bFunc == NULL )
         {
             if ( !p->pPars->fSilent )
-                printf( "Reached timeout (%d seconds) during constructing the bad states.\n", p->pPars->TimeLimit );
+                printf( "Reached timeout (%d seconds) while computing bad states.\n", p->pPars->TimeLimit );
             return -1;
         }
         if ( p->ddR->bFunc == NULL )
@@ -263,7 +276,7 @@ int Llb_CoreReachability_int( Llb_Img_t * p, Vec_Ptr_t * vQuant0, Vec_Ptr_t * vQ
         if ( p->pPars->TimeLimit && clock() >= p->pPars->TimeTarget )
         {
             if ( !p->pPars->fSilent )
-                printf( "Reached timeout during image computation (%d seconds).\n",  p->pPars->TimeLimit );
+                printf( "Reached timeout (%d seconds) during image computation.\n",  p->pPars->TimeLimit );
             p->pPars->iFrame = nIters - 1;
             Cudd_RecursiveDeref( p->dd,  bCurrent );  bCurrent = NULL;
             Cudd_RecursiveDeref( p->ddG, bReached );  bReached = NULL;
@@ -300,7 +313,7 @@ int Llb_CoreReachability_int( Llb_Img_t * p, Vec_Ptr_t * vQuant0, Vec_Ptr_t * vQ
         if ( bNext == NULL )
         {
             if ( !p->pPars->fSilent )
-                printf( "Reached timeout during image computation (%d seconds).\n",  p->pPars->TimeLimit );
+                printf( "Reached timeout (%d seconds) during image computation.\n",  p->pPars->TimeLimit );
             p->pPars->iFrame = nIters - 1;
             Cudd_RecursiveDeref( p->dd,  bCurrent );   bCurrent = NULL;
             Cudd_RecursiveDeref( p->ddG, bReached );   bReached = NULL;
@@ -311,10 +324,23 @@ int Llb_CoreReachability_int( Llb_Img_t * p, Vec_Ptr_t * vQuant0, Vec_Ptr_t * vQ
 //Extra_bddPrintSupport( p->dd, bNext ); printf( "\n" );
 
         // remap these states into the global manager
-        bNext = Extra_TransferPermute( p->dd, p->ddG, bTemp = bNext, pLoc2Glo );    Cudd_Ref( bNext );
-        Cudd_RecursiveDeref( p->dd, bTemp );
-        nBddSize = Cudd_DagSize(bNext);
+//        bNext = Extra_TransferPermute( p->dd, p->ddG, bTemp = bNext, pLoc2Glo );    Cudd_Ref( bNext );
+//        Cudd_RecursiveDeref( p->dd, bTemp );
 
+        bNext = Extra_TransferPermuteTime( p->dd, p->ddG, bTemp = bNext, pLoc2Glo, p->pPars->TimeTarget );    
+        if ( bNext == NULL )
+        {
+            if ( !p->pPars->fSilent )
+                printf( "Reached timeout (%d seconds) during image computation in transfer 1.\n",  p->pPars->TimeLimit );
+            p->pPars->iFrame = nIters - 1;
+            Cudd_RecursiveDeref( p->dd,  bTemp );  
+            Cudd_RecursiveDeref( p->ddG, bReached );   bReached = NULL;
+            return -1;
+        }
+        Cudd_Ref( bNext );
+        Cudd_RecursiveDeref( p->dd, bTemp );  
+
+        nBddSize = Cudd_DagSize(bNext);
         // check if there are any new states
         if ( Cudd_bddLeq( p->ddG, bNext, bReached ) ) // implication = no new states
         {
@@ -324,8 +350,22 @@ int Llb_CoreReachability_int( Llb_Img_t * p, Vec_Ptr_t * vQuant0, Vec_Ptr_t * vQ
 
         // get the new states
         bCurrent = Cudd_bddAnd( p->ddG, bNext, Cudd_Not(bReached) );                    Cudd_Ref( bCurrent );
+
         // remap these states into the current state vars
-        bCurrent = Extra_TransferPermute( p->ddG, p->dd, bTemp = bCurrent, pGlo2Loc );   Cudd_Ref( bCurrent );
+//        bCurrent = Extra_TransferPermute( p->ddG, p->dd, bTemp = bCurrent, pGlo2Loc );   Cudd_Ref( bCurrent );
+//        Cudd_RecursiveDeref( p->ddG, bTemp );
+
+        bCurrent = Extra_TransferPermuteTime( p->ddG, p->dd, bTemp = bCurrent, pGlo2Loc, p->pPars->TimeTarget );    
+        if ( bCurrent == NULL )
+        {
+            if ( !p->pPars->fSilent )
+                printf( "Reached timeout (%d seconds) during image computation in transfer 2.\n",  p->pPars->TimeLimit );
+            p->pPars->iFrame = nIters - 1;
+            Cudd_RecursiveDeref( p->ddG, bTemp );  
+            Cudd_RecursiveDeref( p->ddG, bReached );   bReached = NULL;
+            return -1;
+        }
+        Cudd_Ref( bCurrent );
         Cudd_RecursiveDeref( p->ddG, bTemp );
 
         // add to the reached states
@@ -449,7 +489,7 @@ int Llb_CoreReachability( Llb_Img_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Ptr_t * Llb_CoreConstructAll( Aig_Man_t * p, Vec_Ptr_t * vResult, Vec_Int_t * vVarsNs )
+Vec_Ptr_t * Llb_CoreConstructAll( Aig_Man_t * p, Vec_Ptr_t * vResult, Vec_Int_t * vVarsNs, int TimeTarget )
 {
     DdManager * dd;
     Vec_Ptr_t * vDdMans;
@@ -459,9 +499,22 @@ Vec_Ptr_t * Llb_CoreConstructAll( Aig_Man_t * p, Vec_Ptr_t * vResult, Vec_Int_t
     Vec_PtrForEachEntryReverse( Vec_Ptr_t *, vResult, vLower, i )
     {
         if ( i < Vec_PtrSize(vResult) - 1 )
-            dd = Llb_ImgPartition( p, vLower, vUpper );
+            dd = Llb_ImgPartition( p, vLower, vUpper, TimeTarget );
         else
-            dd = Llb_DriverLastPartition( p, vVarsNs );
+            dd = Llb_DriverLastPartition( p, vVarsNs, TimeTarget );
+        if ( dd == NULL )
+        {
+            Vec_PtrForEachEntry( DdManager *, vDdMans, dd, i )
+            {
+                if ( dd == NULL )
+                    continue;
+                if ( dd->bFunc )
+                    Cudd_RecursiveDeref( dd, dd->bFunc );
+                Extra_StopManager( dd );
+            }
+            Vec_PtrFree( vDdMans );
+            return NULL;
+        }
         Vec_PtrWriteEntry( vDdMans, i, dd );
         vUpper = vLower;
     }
@@ -557,6 +610,7 @@ void Llb_CoreStop( Llb_Img_t * p )
     DdManager * dd;
     DdNode * bTemp;
     int i;
+    if ( p->vDdMans )
     Vec_PtrForEachEntry( DdManager *, p->vDdMans, dd, i )
     {
         if ( dd->bFunc )
@@ -565,7 +619,7 @@ void Llb_CoreStop( Llb_Img_t * p )
             Cudd_RecursiveDeref( dd, dd->bFunc2 );
         Extra_StopManager( dd );
     }
-    Vec_PtrFree( p->vDdMans );
+    Vec_PtrFreeP( &p->vDdMans );
     if ( p->ddR->bFunc )
         Cudd_RecursiveDeref( p->ddR, p->ddR->bFunc );
     Vec_PtrForEachEntry( DdNode *, p->vRings, bTemp, i )
@@ -595,14 +649,21 @@ void Llb_CoreStop( Llb_Img_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-int Llb_CoreExperiment( Aig_Man_t * pInit, Aig_Man_t * pAig, Gia_ParLlb_t * pPars, Vec_Ptr_t * vResult )
+int Llb_CoreExperiment( Aig_Man_t * pInit, Aig_Man_t * pAig, Gia_ParLlb_t * pPars, Vec_Ptr_t * vResult, int TimeTarget )
 {
     int RetValue;
     Llb_Img_t * p;
 //    printf( "\n" );
 //    pPars->fVerbose = 1;
     p = Llb_CoreStart( pInit, pAig, pPars );
-    p->vDdMans = Llb_CoreConstructAll( pAig, vResult, p->vVarsNs );
+    p->vDdMans = Llb_CoreConstructAll( pAig, vResult, p->vVarsNs, TimeTarget );
+    if ( p->vDdMans == NULL )
+    {
+        if ( !pPars->fSilent )
+            printf( "Reached timeout (%d seconds) while deriving the partitions.\n", pPars->TimeLimit );
+        Llb_CoreStop( p );
+        return -1;
+    }
     RetValue = Llb_CoreReachability( p );
     Llb_CoreStop( p );
     return RetValue;
@@ -625,6 +686,13 @@ int Llb_ManReachMinCut( Aig_Man_t * pAig, Gia_ParLlb_t * pPars )
     Vec_Ptr_t * vResult;
     Aig_Man_t * p;
     int RetValue = -1;
+    int clk = clock();
+
+    // compute time to stop
+    if ( pPars->TimeLimit )
+        pPars->TimeTarget = clock() + pPars->TimeLimit * CLOCKS_PER_SEC;
+    else
+        pPars->TimeTarget = 0;
 
     p = Aig_ManDupFlopsOnly( pAig );
 //Aig_ManShow( p, 0, NULL );
@@ -635,13 +703,29 @@ int Llb_ManReachMinCut( Aig_Man_t * pAig, Gia_ParLlb_t * pPars )
     Aig_ManFanoutStart( p );
 
     vResult = Llb_ManComputeCuts( p, pPars->nPartValue, pPars->fVerbose, pPars->fVeryVerbose );
+
+    if ( pPars->TimeLimit && clock() >= pPars->TimeTarget )
+    {
+        if ( !pPars->fSilent )
+            printf( "Reached timeout (%d seconds) after partitioning.\n", pPars->TimeLimit );
+
+        Vec_VecFree( (Vec_Vec_t *)vResult );
+        Aig_ManFanoutStop( p );
+        Aig_ManCleanMarkAB( p );
+        Aig_ManStop( p );
+        return RetValue;
+    }
+
     if ( !pPars->fSkipReach )
-        RetValue = Llb_CoreExperiment( pAig, p, pPars, vResult );
-    Vec_VecFree( (Vec_Vec_t *)vResult );
+        RetValue = Llb_CoreExperiment( pAig, p, pPars, vResult, pPars->TimeTarget );
 
+    Vec_VecFree( (Vec_Vec_t *)vResult );
     Aig_ManFanoutStop( p );
     Aig_ManCleanMarkAB( p );
     Aig_ManStop( p );
+
+    if ( RetValue == -1 )
+        Abc_PrintTime( 1, "Total runtime of the min-cut-based reachability engine", clock() - clk );
     return RetValue;
 }
 

src/aig/llb/llb2Driver.c

@@ -157,7 +157,7 @@ DdNode * Llb_DriverPhaseCube( Aig_Man_t * pAig, Vec_Int_t * vDriRefs, DdManager
   SeeAlso     []
 
 ***********************************************************************/
-DdManager * Llb_DriverLastPartition( Aig_Man_t * p, Vec_Int_t * vVarsNs )
+DdManager * Llb_DriverLastPartition( Aig_Man_t * p, Vec_Int_t * vVarsNs, int TimeTarget )
 {
     int fVerbose = 1;
     DdManager * dd;
@@ -166,6 +166,7 @@ DdManager * Llb_DriverLastPartition( Aig_Man_t * p, Vec_Int_t * vVarsNs )
     int i;
     dd = Cudd_Init( Aig_ManObjNumMax(p), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
     Cudd_AutodynEnable( dd, CUDD_REORDER_SYMM_SIFT );
+    dd->TimeStop = TimeTarget;
     bRes = Cudd_ReadOne(dd);                                   Cudd_Ref( bRes );
 
     // mark the duplicated flop inputs
@@ -179,7 +180,15 @@ DdManager * Llb_DriverLastPartition( Aig_Man_t * p, Vec_Int_t * vVarsNs )
             bVar2 = Cudd_ReadOne(dd);
         bVar2 = Cudd_NotCond( bVar2, Aig_ObjFaninC0(pObj) );
         bProd = Cudd_bddXnor( dd, bVar1, bVar2 );              Cudd_Ref( bProd );
-        bRes  = Cudd_bddAnd( dd, bTemp = bRes, bProd );        Cudd_Ref( bRes );
+//        bRes  = Cudd_bddAnd( dd, bTemp = bRes, bProd );        Cudd_Ref( bRes );
+        bRes  = Extra_bddAndTime( dd, bTemp = bRes, bProd, TimeTarget );  
+        if ( bRes == NULL )
+        {
+            Cudd_RecursiveDeref( dd, bTemp );
+            Cudd_RecursiveDeref( dd, bProd );
+            return NULL;
+        }        
+        Cudd_Ref( bRes );
         Cudd_RecursiveDeref( dd, bTemp );
         Cudd_RecursiveDeref( dd, bProd );
     }
@@ -196,6 +205,7 @@ DdManager * Llb_DriverLastPartition( Aig_Man_t * p, Vec_Int_t * vVarsNs )
 //    Cudd_RecursiveDeref( dd, bRes );
 //    Extra_StopManager( dd );
     dd->bFunc = bRes;
+    dd->TimeStop = 0;
     return dd;
 }
 

src/aig/llb/llb2Image.c

@@ -179,7 +179,7 @@ void Llb_ImgSchedule( Vec_Ptr_t * vSupps, Vec_Ptr_t ** pvQuant0, Vec_Ptr_t ** pv
   SeeAlso     []
 
 ***********************************************************************/
-DdManager * Llb_ImgPartition( Aig_Man_t * p, Vec_Ptr_t * vLower, Vec_Ptr_t * vUpper )
+DdManager * Llb_ImgPartition( Aig_Man_t * p, Vec_Ptr_t * vLower, Vec_Ptr_t * vUpper, int TimeTarget )
 {
     Vec_Ptr_t * vNodes, * vRange;
     Aig_Obj_t * pObj;
@@ -189,6 +189,7 @@ DdManager * Llb_ImgPartition( Aig_Man_t * p, Vec_Ptr_t * vLower, Vec_Ptr_t * vUp
 
     dd = Cudd_Init( Aig_ManObjNumMax(p), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
     Cudd_AutodynEnable( dd,  CUDD_REORDER_SYMM_SIFT );
+    dd->TimeStop = TimeTarget;
 
     Vec_PtrForEachEntry( Aig_Obj_t *, vLower, pObj, i )
         pObj->pData = Cudd_bddIthVar( dd, Aig_ObjId(pObj) );
@@ -198,7 +199,15 @@ DdManager * Llb_ImgPartition( Aig_Man_t * p, Vec_Ptr_t * vLower, Vec_Ptr_t * vUp
     {
         bBdd0 = Cudd_NotCond( (DdNode *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj) );
         bBdd1 = Cudd_NotCond( (DdNode *)Aig_ObjFanin1(pObj)->pData, Aig_ObjFaninC1(pObj) );
-        pObj->pData = Cudd_bddAnd( dd, bBdd0, bBdd1 );   Cudd_Ref( (DdNode *)pObj->pData );
+//        pObj->pData = Cudd_bddAnd( dd, bBdd0, bBdd1 );   Cudd_Ref( (DdNode *)pObj->pData );
+        pObj->pData = Extra_bddAndTime( dd, bBdd0, bBdd1, TimeTarget );  
+        if ( pObj->pData == NULL )
+        {
+            Cudd_Quit( dd );
+            Vec_PtrFree( vNodes );
+            return NULL;
+        }
+        Cudd_Ref( (DdNode *)pObj->pData );
     }
 
     vRange = Llb_ManCutRange( p, vLower, vUpper );
@@ -207,7 +216,16 @@ DdManager * Llb_ImgPartition( Aig_Man_t * p, Vec_Ptr_t * vLower, Vec_Ptr_t * vUp
     {
         assert( Aig_ObjIsNode(pObj) );
         bProd = Cudd_bddXnor( dd, Cudd_bddIthVar(dd, Aig_ObjId(pObj)), (DdNode *)pObj->pData );   Cudd_Ref( bProd );
-        bRes  = Cudd_bddAnd( dd, bTemp = bRes, bProd ); Cudd_Ref( bRes );
+//        bRes  = Cudd_bddAnd( dd, bTemp = bRes, bProd ); Cudd_Ref( bRes );
+        bRes  = Extra_bddAndTime( dd, bTemp = bRes, bProd, TimeTarget );  
+        if ( bRes == NULL )
+        {
+            Cudd_Quit( dd );
+            Vec_PtrFree( vRange );
+            Vec_PtrFree( vNodes );
+            return NULL;
+        }        
+        Cudd_Ref( bRes );
         Cudd_RecursiveDeref( dd, bTemp );
         Cudd_RecursiveDeref( dd, bProd );
     }
@@ -220,6 +238,7 @@ DdManager * Llb_ImgPartition( Aig_Man_t * p, Vec_Ptr_t * vLower, Vec_Ptr_t * vUp
 //    Cudd_RecursiveDeref( dd, bRes );
 //    Extra_StopManager( dd );
     dd->bFunc = bRes;
+    dd->TimeStop = 0;
     return dd;
 }
 
@@ -373,7 +392,17 @@ if ( fVerbose )
 printf( "Pt0 =%6d. Pt1 =%6d. ", Cudd_DagSize(ddPart->bFunc), Cudd_DagSize(bGroup) );
         // perform partial product
         bCube  = Llb_ImgComputeCube( pAig, (Vec_Int_t *)Vec_PtrEntry(vQuant1, i+1), dd ); Cudd_Ref( bCube );
-        bImage = Cudd_bddAndAbstract( dd, bTemp = bImage, bGroup, bCube );                Cudd_Ref( bImage );
+//        bImage = Cudd_bddAndAbstract( dd, bTemp = bImage, bGroup, bCube );                
+        bImage = Extra_bddAndAbstractTime( dd, bTemp = bImage, bGroup, bCube, TimeTarget );  
+        if ( bImage == NULL )
+        {
+            Cudd_RecursiveDeref( dd, bTemp );
+            Cudd_RecursiveDeref( dd, bCube );
+            Cudd_RecursiveDeref( dd, bGroup );
+            return NULL;
+        }
+        Cudd_Ref( bImage );
+
 if ( fVerbose )
 printf( "Im0 =%6d. Im1 =%6d. ", Cudd_DagSize(bTemp), Cudd_DagSize(bImage) );
 //printf("\n"); Extra_bddPrintSupport(dd, bImage); printf("\n");
@@ -384,12 +413,6 @@ printf( "Im0 =%6d. Im1 =%6d. ", Cudd_DagSize(bTemp), Cudd_DagSize(bImage) );
 //        Cudd_ReduceHeap( dd, CUDD_REORDER_SYMM_SIFT, 100 );
 //        Abc_Print( 1, "Reo =%6d.  ", Cudd_DagSize(bImage) );
 
-        // chech runtime
-        if ( TimeTarget && clock() >= TimeTarget )
-        {
-            Cudd_RecursiveDeref( dd, bImage );
-            return NULL;
-        }
 if ( fVerbose )
 printf( "Supp =%3d. ", Cudd_SupportSize(dd, bImage) );
 if ( fVerbose )

src/aig/llb/llbInt.h

@@ -155,11 +155,11 @@ extern Vec_Int_t *     Llb_DriverCountRefs( Aig_Man_t * p );
 extern Vec_Int_t *     Llb_DriverCollectNs( Aig_Man_t * pAig, Vec_Int_t * vDriRefs );
 extern Vec_Int_t *     Llb_DriverCollectCs( Aig_Man_t * pAig );
 extern DdNode *        Llb_DriverPhaseCube( Aig_Man_t * pAig, Vec_Int_t * vDriRefs, DdManager * dd );
-extern DdManager *     Llb_DriverLastPartition( Aig_Man_t * p, Vec_Int_t * vVarsNs );
+extern DdManager *     Llb_DriverLastPartition( Aig_Man_t * p, Vec_Int_t * vVarsNs, int TimeTarget );
 /*=== llb2Image.c ======================================================*/
 extern Vec_Ptr_t *     Llb_ImgSupports( Aig_Man_t * p, Vec_Ptr_t * vDdMans, Vec_Int_t * vStart, Vec_Int_t * vStop, int fAddPis, int fVerbose );
 extern void            Llb_ImgSchedule( Vec_Ptr_t * vSupps, Vec_Ptr_t ** pvQuant0, Vec_Ptr_t ** pvQuant1, int fVerbose );
-extern DdManager *     Llb_ImgPartition( Aig_Man_t * p, Vec_Ptr_t * vLower, Vec_Ptr_t * vUpper );
+extern DdManager *     Llb_ImgPartition( Aig_Man_t * p, Vec_Ptr_t * vLower, Vec_Ptr_t * vUpper, int TimeTarget );
 extern void            Llb_ImgQuantifyFirst( Aig_Man_t * pAig, Vec_Ptr_t * vDdMans, Vec_Ptr_t * vQuant0, int fVerbose );
 extern void            Llb_ImgQuantifyReset( Vec_Ptr_t * vDdMans );
 extern DdNode *        Llb_ImgComputeImage( Aig_Man_t * pAig, Vec_Ptr_t * vDdMans, DdManager * dd, DdNode * bInit,