diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2011-02-13 20:50:29 -0800 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2011-02-13 20:50:29 -0800 |
| commit | a7e214bb01085492e330186295a71da35846a6b7 (patch) | |
| tree | f0d2d8753a12036226752f92771bfed5b7876d39 /src/aig/llb/llb2Bad.c | |
| parent | 573694f9bf9cc019c9a4d265fbcb04c0fbde78e1 (diff) | |
| download | abc-a7e214bb01085492e330186295a71da35846a6b7.tar.gz abc-a7e214bb01085492e330186295a71da35846a6b7.tar.bz2 abc-a7e214bb01085492e330186295a71da35846a6b7.zip | |
Improved timeout in the BDD reachability engines.
Diffstat (limited to 'src/aig/llb/llb2Bad.c')
| -rw-r--r-- | src/aig/llb/llb2Bad.c | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/src/aig/llb/llb2Bad.c b/src/aig/llb/llb2Bad.c index 8e2a37ff..9aecb9ff 100644 --- a/src/aig/llb/llb2Bad.c +++ b/src/aig/llb/llb2Bad.c @@ -63,7 +63,8 @@ DdNode * Llb_BddComputeBad( Aig_Man_t * pInit, DdManager * dd, int TimeOut ) continue; bBdd0 = Cudd_NotCond( (DdNode *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj) ); bBdd1 = Cudd_NotCond( (DdNode *)Aig_ObjFanin1(pObj)->pData, Aig_ObjFaninC1(pObj) ); - pObj->pData = Extra_bddAndTime( dd, bBdd0, bBdd1, TimeOut ); +// pObj->pData = Extra_bddAndTime( dd, bBdd0, bBdd1, TimeOut ); + pObj->pData = Cudd_bddAnd( dd, bBdd0, bBdd1 ); if ( pObj->pData == NULL ) { Vec_PtrForEachEntryStop( Aig_Obj_t *, vNodes, pObj, k, i ) @@ -109,8 +110,9 @@ DdNode * Llb_BddQuantifyPis( Aig_Man_t * pInit, DdManager * dd, DdNode * bFunc ) { DdNode * bVar, * bCube, * bTemp; Aig_Obj_t * pObj; - int i; + int i, TimeStop; assert( Cudd_ReadSize(dd) == Aig_ManPiNum(pInit) ); + TimeStop = dd->TimeStop; dd->TimeStop = 0; // create PI cube bCube = Cudd_ReadOne( dd ); Cudd_Ref( bCube ); Saig_ManForEachPi( pInit, pObj, i ) { @@ -122,6 +124,7 @@ DdNode * Llb_BddQuantifyPis( Aig_Man_t * pInit, DdManager * dd, DdNode * bFunc ) bFunc = Cudd_bddExistAbstract( dd, bFunc, bCube ); Cudd_Ref( bFunc ); Cudd_RecursiveDeref( dd, bCube ); Cudd_Deref( bFunc ); + dd->TimeStop = TimeStop; return bFunc; } |