diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2011-02-07 20:37:53 -0800 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2011-02-07 20:37:53 -0800 |
| commit | 53217cdc8b87d693fe187b788ca5aaa9daf0ab32 (patch) | |
| tree | 7db9dc3a05021722960f530e7ab13252d06f33a2 /src/aig/llb | |
| parent | 21bb515b3c32aee47a34e9dfc162c8bc09a5cdc9 (diff) | |
| download | abc-53217cdc8b87d693fe187b788ca5aaa9daf0ab32.tar.gz abc-53217cdc8b87d693fe187b788ca5aaa9daf0ab32.tar.bz2 abc-53217cdc8b87d693fe187b788ca5aaa9daf0ab32.zip | |
Yet another update to the runtime control in BDD operations.
Diffstat (limited to 'src/aig/llb')
| -rw-r--r-- | src/aig/llb/llb3Nonlin.c | 25 |
1 files changed, 21 insertions, 4 deletions
diff --git a/src/aig/llb/llb3Nonlin.c b/src/aig/llb/llb3Nonlin.c index 59304768..2b4272d9 100644 --- a/src/aig/llb/llb3Nonlin.c +++ b/src/aig/llb/llb3Nonlin.c @@ -427,7 +427,7 @@ int Llb_NonlinReachability( Llb_Mnn_t * p ) 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; return -1; @@ -484,7 +484,7 @@ int Llb_NonlinReachability( Llb_Mnn_t * p ) 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 in quantification.\n", p->pPars->TimeLimit ); p->pPars->iFrame = nIters - 1; Cudd_RecursiveDeref( p->dd, bCurrent ); bCurrent = NULL; return -1; @@ -530,7 +530,16 @@ int Llb_NonlinReachability( Llb_Mnn_t * p ) // transfer to the state manager clk3 = clock(); Cudd_RecursiveDeref( p->ddG, p->ddG->bFunc2 ); - p->ddG->bFunc2 = Extra_TransferPermute( p->dd, p->ddG, bNext, Vec_IntArray(p->vNs2Glo) ); Cudd_Ref( p->ddG->bFunc2 ); + p->ddG->bFunc2 = Extra_TransferPermuteTime( p->dd, p->ddG, bNext, Vec_IntArray(p->vNs2Glo), p->pPars->TimeTarget ); + if ( p->ddG->bFunc2 == 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, bNext ); + return -1; + } + Cudd_Ref( p->ddG->bFunc2 ); Cudd_RecursiveDeref( p->dd, bNext ); p->timeTran1 += clock() - clk3; @@ -552,7 +561,15 @@ int Llb_NonlinReachability( Llb_Mnn_t * p ) // move new states to the working manager clk3 = clock(); - bCurrent = Extra_TransferPermute( p->ddG, p->dd, p->ddG->bFunc2, Vec_IntArray(p->vGlo2Cs) ); Cudd_Ref( bCurrent ); + bCurrent = Extra_TransferPermuteTime( p->ddG, p->dd, p->ddG->bFunc2, Vec_IntArray(p->vGlo2Cs), 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; + return -1; + } + Cudd_Ref( bCurrent ); p->timeTran2 += clock() - clk3; // report the results |