Skip to content

A
abc
Commit ca5d7eef by Alan Mishchenko
Options

Fixing timeout in reachability engines.

parent 464fda3f
Showing with 38 additions and 6 deletions
src/aig/llb/llb1Reach.c
...@@ -629,6 +629,7 @@ int Llb_ManReachability( Llb_Man_t * p, Vec_Int_t * vHints, DdManager ** pddGlo ...@@ -629,6 +629,7 @@ int Llb_ManReachability( Llb_Man_t * p, Vec_Int_t * vHints, DdManager ** pddGlo
{ {
if ( !p->pPars->fSilent ) if ( !p->pPars->fSilent )
printf( "Reached timeout (%d seconds) during constructing the bad states.\n", p->pPars->TimeLimit ); printf( "Reached timeout (%d seconds) during constructing the bad states.\n", p->pPars->TimeLimit );
p->pPars->iFrame = -1;
return -1; return -1;
} }
Cudd_Ref( p->ddR->bFunc ); Cudd_Ref( p->ddR->bFunc );
...@@ -701,6 +702,7 @@ int Llb_ManReachability( Llb_Man_t * p, Vec_Int_t * vHints, DdManager ** pddGlo ...@@ -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 ); printf( "Output ??? was asserted in frame %d (counter-example is not produced). ", nIters );
Abc_PrintTime( 1, "Time", clock() - clk ); Abc_PrintTime( 1, "Time", clock() - clk );
} }
p->pPars->iFrame = nIters - 1;
Cudd_RecursiveDeref( p->dd, bCurrent ); bCurrent = NULL; Cudd_RecursiveDeref( p->dd, bCurrent ); bCurrent = NULL;
Cudd_RecursiveDeref( p->dd, bConstrCs ); bConstrCs = NULL; Cudd_RecursiveDeref( p->dd, bConstrCs ); bConstrCs = NULL;
Cudd_RecursiveDeref( p->dd, bConstrNs ); bConstrNs = 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 ...@@ -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, bConstrCs ); bConstrCs = NULL;
Cudd_RecursiveDeref( p->dd, bConstrNs ); bConstrNs = NULL; Cudd_RecursiveDeref( p->dd, bConstrNs ); bConstrNs = NULL;
if ( bReached == NULL ) if ( bReached == NULL )
{
p->pPars->iFrame = nIters - 1;
return 0; // reachable return 0; // reachable
}
// assert( bCurrent == NULL ); // assert( bCurrent == NULL );
if ( bCurrent ) if ( bCurrent )
Cudd_RecursiveDeref( p->dd, bCurrent ); Cudd_RecursiveDeref( p->dd, bCurrent );
...@@ -869,6 +874,7 @@ int Llb_ManReachability( Llb_Man_t * p, Vec_Int_t * vHints, DdManager ** pddGlo ...@@ -869,6 +874,7 @@ int Llb_ManReachability( Llb_Man_t * p, Vec_Int_t * vHints, DdManager ** pddGlo
{ {
if ( !p->pPars->fSilent ) if ( !p->pPars->fSilent )
printf( "Verified only for states reachable in %d frames. ", nIters ); printf( "Verified only for states reachable in %d frames. ", nIters );
p->pPars->iFrame = p->pPars->nIterMax;
Cudd_RecursiveDeref( p->ddG, bReached ); Cudd_RecursiveDeref( p->ddG, bReached );
return -1; // undecided return -1; // undecided
} }
......
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 ...@@ -222,6 +222,7 @@ int Llb_CoreReachability_int( Llb_Img_t * p, Vec_Ptr_t * vQuant0, Vec_Ptr_t * vQ
{ {
if ( !p->pPars->fSilent ) if ( !p->pPars->fSilent )
printf( "Reached timeout (%d seconds) before image computation.\n", p->pPars->TimeLimit ); printf( "Reached timeout (%d seconds) before image computation.\n", p->pPars->TimeLimit );
p->pPars->iFrame = -1;
return -1; return -1;
} }
...@@ -239,6 +240,7 @@ int Llb_CoreReachability_int( Llb_Img_t * p, Vec_Ptr_t * vQuant0, Vec_Ptr_t * vQ ...@@ -239,6 +240,7 @@ int Llb_CoreReachability_int( Llb_Img_t * p, Vec_Ptr_t * vQuant0, Vec_Ptr_t * vQ
{ {
if ( !p->pPars->fSilent ) if ( !p->pPars->fSilent )
printf( "Reached timeout (%d seconds) while computing bad states.\n", p->pPars->TimeLimit ); printf( "Reached timeout (%d seconds) while computing bad states.\n", p->pPars->TimeLimit );
p->pPars->iFrame = -1;
return -1; return -1;
} }
Cudd_Ref( bTemp ); Cudd_Ref( bTemp );
...@@ -255,6 +257,7 @@ int Llb_CoreReachability_int( Llb_Img_t * p, Vec_Ptr_t * vQuant0, Vec_Ptr_t * vQ ...@@ -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 ); Cudd_RecursiveDeref( p->ddG, bReached );
if ( !p->pPars->fSilent ) if ( !p->pPars->fSilent )
printf( "Reached timeout (%d seconds) during transfer 0.\n", p->pPars->TimeLimit ); printf( "Reached timeout (%d seconds) during transfer 0.\n", p->pPars->TimeLimit );
p->pPars->iFrame = -1;
return -1; return -1;
} }
Cudd_Ref( bCurrent ); Cudd_Ref( bCurrent );
...@@ -267,10 +270,9 @@ int Llb_CoreReachability_int( Llb_Img_t * p, Vec_Ptr_t * vQuant0, Vec_Ptr_t * vQ ...@@ -267,10 +270,9 @@ int Llb_CoreReachability_int( Llb_Img_t * p, Vec_Ptr_t * vQuant0, Vec_Ptr_t * vQ
{ {
if ( !p->pPars->fSilent ) if ( !p->pPars->fSilent )
printf( "Reached timeout (%d seconds) while computing bad states.\n", p->pPars->TimeLimit ); printf( "Reached timeout (%d seconds) while computing bad states.\n", p->pPars->TimeLimit );
p->pPars->iFrame = -1;
return -1; return -1;
} }
if ( p->ddR->bFunc == NULL )
return -1;
Cudd_Ref( p->ddR->bFunc ); Cudd_Ref( p->ddR->bFunc );
// create init state in the working and global manager // create init state in the working and global manager
bCurrent = Llb_CoreComputeCube( p->dd, p->vVarsCs, 1, NULL ); Cudd_Ref( bCurrent ); 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 ...@@ -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 ); printf( "Output ??? was asserted in frame %d (counter-example is not produced). ", nIters );
Abc_PrintTime( 1, "Time", clock() - clk ); Abc_PrintTime( 1, "Time", clock() - clk );
} }
p->pPars->iFrame = nIters - 1;
return 0; return 0;
} }
...@@ -438,7 +441,10 @@ int Llb_CoreReachability_int( Llb_Img_t * p, Vec_Ptr_t * vQuant0, Vec_Ptr_t * vQ ...@@ -438,7 +441,10 @@ int Llb_CoreReachability_int( Llb_Img_t * p, Vec_Ptr_t * vQuant0, Vec_Ptr_t * vQ
} }
} }
if ( bReached == NULL ) if ( bReached == NULL )
{
p->pPars->iFrame = nIters - 1;
return 0; // reachable return 0; // reachable
}
if ( bCurrent ) if ( bCurrent )
Cudd_RecursiveDeref( p->dd, bCurrent ); Cudd_RecursiveDeref( p->dd, bCurrent );
// report the stats // report the stats
...@@ -465,6 +471,7 @@ int Llb_CoreReachability_int( Llb_Img_t * p, Vec_Ptr_t * vQuant0, Vec_Ptr_t * vQ ...@@ -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 ); printf( "Verified only for states reachable in %d frames. ", nIters );
Abc_PrintTime( 1, "Time", clock() - clk ); Abc_PrintTime( 1, "Time", clock() - clk );
} }
p->pPars->iFrame = p->pPars->nIterMax;
return -1; // undecided return -1; // undecided
} }
if ( !p->pPars->fSilent ) if ( !p->pPars->fSilent )
......
src/aig/llb/llb3Image.c
...@@ -958,13 +958,14 @@ static Llb_Mgr_t * p = NULL; ...@@ -958,13 +958,14 @@ static Llb_Mgr_t * p = NULL;
SeeAlso [] 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; DdManager * dd;
int clk = clock(); int clk = clock();
assert( p == NULL ); assert( p == NULL );
// start a new manager (disable reordering) // start a new manager (disable reordering)
dd = Cudd_Init( Aig_ManObjNumMax(pAig), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 ); dd = Cudd_Init( Aig_ManObjNumMax(pAig), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
dd->TimeStop = TimeTarget;
Cudd_ShuffleHeap( dd, pOrder ); Cudd_ShuffleHeap( dd, pOrder );
// if ( fFirst ) // if ( fFirst )
Cudd_AutodynEnable( dd, CUDD_REORDER_SYMM_SIFT ); Cudd_AutodynEnable( dd, CUDD_REORDER_SYMM_SIFT );
...@@ -973,6 +974,7 @@ DdManager * Llb_NonlinImageStart( Aig_Man_t * pAig, Vec_Ptr_t * vLeaves, Vec_Ptr ...@@ -973,6 +974,7 @@ DdManager * Llb_NonlinImageStart( Aig_Man_t * pAig, Vec_Ptr_t * vLeaves, Vec_Ptr
if ( !Llb_NonlinStart( p, 0 ) ) if ( !Llb_NonlinStart( p, 0 ) )
{ {
Llb_NonlinFree( p ); Llb_NonlinFree( p );
p = NULL;
return NULL; return NULL;
} }
timeBuild += clock() - clk; timeBuild += clock() - clk;
......
src/aig/llb/llb3Nonlin.c
...@@ -453,12 +453,20 @@ int Llb_NonlinReachability( Llb_Mnn_t * p ) ...@@ -453,12 +453,20 @@ int Llb_NonlinReachability( Llb_Mnn_t * p )
{ {
if ( !p->pPars->fSilent ) if ( !p->pPars->fSilent )
printf( "Reached timeout (%d seconds) during constructing the bad states.\n", p->pPars->TimeLimit ); printf( "Reached timeout (%d seconds) during constructing the bad states.\n", p->pPars->TimeLimit );
p->pPars->iFrame = -1;
return -1; return -1;
} }
Cudd_Ref( p->ddR->bFunc ); Cudd_Ref( p->ddR->bFunc );
// compute the starting set of states // compute the starting set of states
Cudd_Quit( p->dd ); 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->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->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 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 ) ...@@ -502,6 +510,7 @@ int Llb_NonlinReachability( Llb_Mnn_t * p )
printf( "Output ??? was asserted in frame %d (counter-example is not produced). ", nIters ); printf( "Output ??? was asserted in frame %d (counter-example is not produced). ", nIters );
Abc_PrintTime( 1, "Time", clock() - clk ); Abc_PrintTime( 1, "Time", clock() - clk );
} }
p->pPars->iFrame = nIters - 1;
Llb_NonlinImageQuit(); Llb_NonlinImageQuit();
return 0; return 0;
} }
...@@ -552,7 +561,14 @@ int Llb_NonlinReachability( Llb_Mnn_t * p ) ...@@ -552,7 +561,14 @@ int Llb_NonlinReachability( Llb_Mnn_t * p )
p->ddLocReos += Cudd_ReadReorderings(p->dd); p->ddLocReos += Cudd_ReadReorderings(p->dd);
p->ddLocGrbs += Cudd_ReadGarbageCollections(p->dd); p->ddLocGrbs += Cudd_ReadGarbageCollections(p->dd);
Llb_NonlinImageQuit(); 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 ); //Extra_TestAndPerm( p->ddG, Cudd_Not(p->ddG->bFunc), p->ddG->bFunc2 );
// derive new states // derive new states
...@@ -658,6 +674,7 @@ int Llb_NonlinReachability( Llb_Mnn_t * p ) ...@@ -658,6 +674,7 @@ int Llb_NonlinReachability( Llb_Mnn_t * p )
{ {
if ( !p->pPars->fSilent ) if ( !p->pPars->fSilent )
printf( "Verified only for states reachable in %d frames. ", nIters ); printf( "Verified only for states reachable in %d frames. ", nIters );
p->pPars->iFrame = p->pPars->nIterMax;
return -1; // undecided return -1; // undecided
} }
// report // report
......
src/aig/llb/llbInt.h
...@@ -172,7 +172,7 @@ extern DdNode * Llb_ImgComputeImage( Aig_Man_t * pAig, Vec_Ptr_t * vDdMan ...@@ -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, Vec_Ptr_t * vQuant0, Vec_Ptr_t * vQuant1, Vec_Int_t * vDriRefs,
int TimeTarget, int fBackward, int fReorder, int fVerbose ); 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 DdNode * Llb_NonlinImageCompute( DdNode * bCurrent, int fReorder, int fDrop, int fVerbose, int * pOrder );
extern void Llb_NonlinImageQuit(); extern void Llb_NonlinImageQuit();
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment