diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2011-02-04 20:22:10 -0800 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2011-02-04 20:22:10 -0800 |
| commit | 3e92b873622ce7ca7baf74520abc28cc7c68dded (patch) | |
| tree | 44db42075cc0ff05d7b92d00c926aace7ec00816 /src/aig/llb/llb2Bad.c | |
| parent | 82e9de90005ee38fdc9fa4c52d335d4e87c93196 (diff) | |
| download | abc-3e92b873622ce7ca7baf74520abc28cc7c68dded.tar.gz abc-3e92b873622ce7ca7baf74520abc28cc7c68dded.tar.bz2 abc-3e92b873622ce7ca7baf74520abc28cc7c68dded.zip | |
Added timeout to &reachn.
Diffstat (limited to 'src/aig/llb/llb2Bad.c')
| -rw-r--r-- | src/aig/llb/llb2Bad.c | 12 |
1 files changed, 10 insertions, 2 deletions
diff --git a/src/aig/llb/llb2Bad.c b/src/aig/llb/llb2Bad.c index 8322698b..4099805b 100644 --- a/src/aig/llb/llb2Bad.c +++ b/src/aig/llb/llb2Bad.c @@ -42,12 +42,12 @@ ABC_NAMESPACE_IMPL_START SeeAlso [] ***********************************************************************/ -DdNode * Llb_BddComputeBad( Aig_Man_t * pInit, DdManager * dd ) +DdNode * Llb_BddComputeBad( Aig_Man_t * pInit, DdManager * dd, int TimeOut ) { Vec_Ptr_t * vNodes; DdNode * bBdd0, * bBdd1, * bTemp, * bResult; Aig_Obj_t * pObj; - int i; + int i, k; assert( Cudd_ReadSize(dd) == Aig_ManPiNum(pInit) ); // initialize elementary variables Aig_ManConst1(pInit)->pData = Cudd_ReadOne( dd ); @@ -64,6 +64,14 @@ DdNode * Llb_BddComputeBad( Aig_Man_t * pInit, DdManager * dd ) 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 ); + + if ( i % 10 == 0 && TimeOut && clock() >= TimeOut ) + { + Vec_PtrForEachEntryStop( Aig_Obj_t *, vNodes, pObj, k, i+1 ) + Cudd_RecursiveDeref( dd, (DdNode *)pObj->pData ); + Vec_PtrFree( vNodes ); + return NULL; + } } // quantify PIs of each PO bResult = Cudd_ReadLogicZero( dd ); Cudd_Ref( bResult ); |