Fixing timeout in reachability engines.

5 files changed, 38 insertions, 6 deletions

diff --git a/src/aig/llb/llb1Reach.c b/src/aig/llb/llb1Reach.c
index 341ebd95..16b62850 100644
--- a/src/aig/llb/llb1Reach.c
+++ b/src/aig/llb/llb1Reach.c
@@ -629,6 +629,7 @@ int Llb_ManReachability( Llb_Man_t * p, Vec_Int_t * vHints, DdManager ** pddGlo
     {
         if ( !p->pPars->fSilent )
             printf( "Reached timeout (%d seconds) during constructing the bad states.\n", p->pPars->TimeLimit );
+        p->pPars->iFrame = -1;
         return -1;
     }
     Cudd_Ref( p->ddR->bFunc );
@@ -701,6 +702,7 @@ int Llb_ManReachability( Llb_Man_t * p, Vec_Int_t * vHints, DdManager ** pddGlo
                     printf( "Output ??? was asserted in frame %d (counter-example is not produced).  ", nIters );
                 Abc_PrintTime( 1, "Time", clock() - clk );
             }
+            p->pPars->iFrame = nIters - 1;
             Cudd_RecursiveDeref( p->dd,  bCurrent );  bCurrent = NULL;
             Cudd_RecursiveDeref( p->dd,  bConstrCs ); bConstrCs = NULL;
             Cudd_RecursiveDeref( p->dd,  bConstrNs ); bConstrNs = NULL;
@@ -850,7 +852,10 @@ int Llb_ManReachability( Llb_Man_t * p, Vec_Int_t * vHints, DdManager ** pddGlo
     Cudd_RecursiveDeref( p->dd, bConstrCs ); bConstrCs = NULL;
     Cudd_RecursiveDeref( p->dd, bConstrNs ); bConstrNs = NULL;
     if ( bReached == NULL )
+    {
+        p->pPars->iFrame = nIters - 1;
         return 0; // reachable
+    }
 //    assert( bCurrent == NULL );
     if ( bCurrent )
         Cudd_RecursiveDeref( p->dd, bCurrent );
@@ -869,6 +874,7 @@ int Llb_ManReachability( Llb_Man_t * p, Vec_Int_t * vHints, DdManager ** pddGlo
     {
         if ( !p->pPars->fSilent )
             printf( "Verified only for states reachable in %d frames.  ", nIters );
+        p->pPars->iFrame = p->pPars->nIterMax;
         Cudd_RecursiveDeref( p->ddG, bReached );
         return -1; // undecided
     }
diff --git a/src/aig/llb/llb2Core.c b/src/aig/llb/llb2Core.c
index 446f1a67..7badc1fb 100644
--- a/src/aig/llb/llb2Core.c
+++ b/src/aig/llb/llb2Core.c
@@ -222,6 +222,7 @@ int Llb_CoreReachability_int( Llb_Img_t * p, Vec_Ptr_t * vQuant0, Vec_Ptr_t * vQ
     {
         if ( !p->pPars->fSilent )
             printf( "Reached timeout (%d seconds) before image computation.\n", p->pPars->TimeLimit );
+        p->pPars->iFrame = -1;
         return -1;
     }
 
@@ -239,6 +240,7 @@ int Llb_CoreReachability_int( Llb_Img_t * p, Vec_Ptr_t * vQuant0, Vec_Ptr_t * vQ
         {
             if ( !p->pPars->fSilent )
                 printf( "Reached timeout (%d seconds) while computing bad states.\n", p->pPars->TimeLimit );
+            p->pPars->iFrame = -1;
             return -1;
         }
         Cudd_Ref( bTemp );
@@ -255,6 +257,7 @@ int Llb_CoreReachability_int( Llb_Img_t * p, Vec_Ptr_t * vQuant0, Vec_Ptr_t * vQ
             Cudd_RecursiveDeref( p->ddG, bReached );
             if ( !p->pPars->fSilent )
                 printf( "Reached timeout (%d seconds) during transfer 0.\n", p->pPars->TimeLimit );
+            p->pPars->iFrame = -1;
             return -1;
         }
         Cudd_Ref( bCurrent );
@@ -267,10 +270,9 @@ int Llb_CoreReachability_int( Llb_Img_t * p, Vec_Ptr_t * vQuant0, Vec_Ptr_t * vQ
         {
             if ( !p->pPars->fSilent )
                 printf( "Reached timeout (%d seconds) while computing bad states.\n", p->pPars->TimeLimit );
+            p->pPars->iFrame = -1;
             return -1;
         }
-        if ( p->ddR->bFunc == NULL )
-            return -1;
         Cudd_Ref( p->ddR->bFunc );
         // create init state in the working and global manager
         bCurrent = Llb_CoreComputeCube( p->dd,  p->vVarsCs, 1, NULL );           Cudd_Ref( bCurrent );
@@ -324,6 +326,7 @@ int Llb_CoreReachability_int( Llb_Img_t * p, Vec_Ptr_t * vQuant0, Vec_Ptr_t * vQ
                     printf( "Output ??? was asserted in frame %d (counter-example is not produced).  ", nIters );
                 Abc_PrintTime( 1, "Time", clock() - clk );
             }
+            p->pPars->iFrame = nIters - 1;
             return 0;
         }
 
@@ -438,7 +441,10 @@ int Llb_CoreReachability_int( Llb_Img_t * p, Vec_Ptr_t * vQuant0, Vec_Ptr_t * vQ
         }
     }
     if ( bReached == NULL )
+    {
+        p->pPars->iFrame = nIters - 1;
         return 0; // reachable
+    }
     if ( bCurrent )
         Cudd_RecursiveDeref( p->dd, bCurrent );
     // report the stats
@@ -465,6 +471,7 @@ int Llb_CoreReachability_int( Llb_Img_t * p, Vec_Ptr_t * vQuant0, Vec_Ptr_t * vQ
             printf( "Verified only for states reachable in %d frames.  ", nIters );
             Abc_PrintTime( 1, "Time", clock() - clk );
         }
+        p->pPars->iFrame = p->pPars->nIterMax;
         return -1; // undecided
     }
     if ( !p->pPars->fSilent )
diff --git a/src/aig/llb/llb3Image.c b/src/aig/llb/llb3Image.c
index 098f9f45..09f2700c 100644
--- a/src/aig/llb/llb3Image.c
+++ b/src/aig/llb/llb3Image.c
@@ -958,13 +958,14 @@ static Llb_Mgr_t * p = NULL;
   SeeAlso     []
 
 ***********************************************************************/
-DdManager * Llb_NonlinImageStart( Aig_Man_t * pAig, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vRoots, int * pVars2Q, int * pOrder, int fFirst )
+DdManager * Llb_NonlinImageStart( Aig_Man_t * pAig, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vRoots, int * pVars2Q, int * pOrder, int fFirst, int TimeTarget )
 {
     DdManager * dd;
     int clk = clock();
     assert( p == NULL );
     // start a new manager (disable reordering)
     dd = Cudd_Init( Aig_ManObjNumMax(pAig), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
+    dd->TimeStop = TimeTarget;
     Cudd_ShuffleHeap( dd, pOrder );
 //    if ( fFirst )
         Cudd_AutodynEnable( dd,  CUDD_REORDER_SYMM_SIFT );
@@ -973,6 +974,7 @@ DdManager * Llb_NonlinImageStart( Aig_Man_t * pAig, Vec_Ptr_t * vLeaves, Vec_Ptr
     if ( !Llb_NonlinStart( p, 0 ) )
     {
         Llb_NonlinFree( p );
+        p = NULL;
         return NULL;
     }
     timeBuild += clock() - clk;
diff --git a/src/aig/llb/llb3Nonlin.c b/src/aig/llb/llb3Nonlin.c
index 6a0c871e..f41e0f6e 100644
--- a/src/aig/llb/llb3Nonlin.c
+++ b/src/aig/llb/llb3Nonlin.c
@@ -453,12 +453,20 @@ int Llb_NonlinReachability( Llb_Mnn_t * p )
     {
         if ( !p->pPars->fSilent )
             printf( "Reached timeout (%d seconds) during constructing the bad states.\n", p->pPars->TimeLimit );
+        p->pPars->iFrame = -1;
         return -1;
     }
     Cudd_Ref( p->ddR->bFunc );
     // compute the starting set of states
     Cudd_Quit( p->dd );
-    p->dd = Llb_NonlinImageStart( p->pAig, p->vLeaves, p->vRoots, p->pVars2Q, p->pOrderL, 1 );
+    p->dd = Llb_NonlinImageStart( p->pAig, p->vLeaves, p->vRoots, p->pVars2Q, p->pOrderL, 1, p->pPars->TimeTarget );
+    if ( p->dd == NULL )
+    {
+        if ( !p->pPars->fSilent )
+            printf( "Reached timeout (%d seconds) during constructing the bad states.\n", p->pPars->TimeLimit );
+        p->pPars->iFrame = -1;
+        return -1;
+    }
     p->dd->bFunc   = Llb_NonlinComputeInitState( p->pAig, p->dd );   Cudd_Ref( p->dd->bFunc );   // current
     p->ddG->bFunc  = Llb_NonlinComputeInitState( p->pAig, p->ddG );  Cudd_Ref( p->ddG->bFunc );  // reached
     p->ddG->bFunc2 = Llb_NonlinComputeInitState( p->pAig, p->ddG );  Cudd_Ref( p->ddG->bFunc2 ); // frontier 
@@ -502,6 +510,7 @@ int Llb_NonlinReachability( Llb_Mnn_t * p )
                     printf( "Output ??? was asserted in frame %d (counter-example is not produced).  ", nIters );
                 Abc_PrintTime( 1, "Time", clock() - clk );
             }
+            p->pPars->iFrame = nIters - 1;
             Llb_NonlinImageQuit();
             return 0;
         }
@@ -552,7 +561,14 @@ int Llb_NonlinReachability( Llb_Mnn_t * p )
         p->ddLocReos += Cudd_ReadReorderings(p->dd);
         p->ddLocGrbs += Cudd_ReadGarbageCollections(p->dd);
         Llb_NonlinImageQuit();
-        p->dd = Llb_NonlinImageStart( p->pAig, p->vLeaves, p->vRoots, p->pVars2Q, p->pOrderL, 0 );
+        p->dd = Llb_NonlinImageStart( p->pAig, p->vLeaves, p->vRoots, p->pVars2Q, p->pOrderL, 0, p->pPars->TimeTarget );
+        if ( p->dd == NULL )
+        {
+            if ( !p->pPars->fSilent )
+                printf( "Reached timeout (%d seconds) during constructing the bad states.\n", p->pPars->TimeLimit );
+            p->pPars->iFrame = nIters - 1;
+            return -1;
+        }
         //Extra_TestAndPerm( p->ddG, Cudd_Not(p->ddG->bFunc), p->ddG->bFunc2 );    
 
         // derive new states
@@ -658,6 +674,7 @@ int Llb_NonlinReachability( Llb_Mnn_t * p )
     {
         if ( !p->pPars->fSilent )
             printf( "Verified only for states reachable in %d frames.  ", nIters );
+        p->pPars->iFrame = p->pPars->nIterMax;
         return -1; // undecided
     }
     // report
diff --git a/src/aig/llb/llbInt.h b/src/aig/llb/llbInt.h
index dd938436..496d975d 100644
--- a/src/aig/llb/llbInt.h
+++ b/src/aig/llb/llbInt.h
@@ -172,7 +172,7 @@ extern DdNode *        Llb_ImgComputeImage( Aig_Man_t * pAig, Vec_Ptr_t * vDdMan
                            Vec_Ptr_t * vQuant0, Vec_Ptr_t * vQuant1, Vec_Int_t * vDriRefs, 
                            int TimeTarget, int fBackward, int fReorder, int fVerbose );
 
-extern DdManager *     Llb_NonlinImageStart( Aig_Man_t * pAig, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vRoots, int * pVars2Q, int * pOrder, int fFirst );
+extern DdManager *     Llb_NonlinImageStart( Aig_Man_t * pAig, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vRoots, int * pVars2Q, int * pOrder, int fFirst, int TimeTarget );
 extern DdNode *        Llb_NonlinImageCompute( DdNode * bCurrent, int fReorder, int fDrop, int fVerbose, int * pOrder );
 extern void            Llb_NonlinImageQuit();