From ca5d7eef2f5fbaaf5b57f32bc0b4088682ec2323 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Thu, 17 Mar 2011 13:43:07 -0700 Subject: Fixing timeout in reachability engines. --- src/aig/llb/llb1Reach.c | 6 ++++++ src/aig/llb/llb2Core.c | 11 +++++++++-- src/aig/llb/llb3Image.c | 4 +++- src/aig/llb/llb3Nonlin.c | 21 +++++++++++++++++++-- src/aig/llb/llbInt.h | 2 +- 5 files changed, 38 insertions(+), 6 deletions(-) (limited to 'src/aig/llb') 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(); -- cgit v1.2.3