diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2011-02-07 15:58:29 -0800 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2011-02-07 15:58:29 -0800 |
commit | 21bb515b3c32aee47a34e9dfc162c8bc09a5cdc9 (patch) | |
tree | 6618ca8b55fbdc87e67c1a9b79306a7eb97bd068 /src/aig | |
parent | 3e92b873622ce7ca7baf74520abc28cc7c68dded (diff) | |
download | abc-21bb515b3c32aee47a34e9dfc162c8bc09a5cdc9.tar.gz abc-21bb515b3c32aee47a34e9dfc162c8bc09a5cdc9.tar.bz2 abc-21bb515b3c32aee47a34e9dfc162c8bc09a5cdc9.zip |
Added handling runtime limit inside And and AndExist.
Diffstat (limited to 'src/aig')
-rw-r--r-- | src/aig/llb/llb2Bad.c | 14 | ||||
-rw-r--r-- | src/aig/llb/llb3Image.c | 31 | ||||
-rw-r--r-- | src/aig/llb/llbInt.h | 2 |
3 files changed, 28 insertions, 19 deletions
diff --git a/src/aig/llb/llb2Bad.c b/src/aig/llb/llb2Bad.c index 4099805b..88ff4c75 100644 --- a/src/aig/llb/llb2Bad.c +++ b/src/aig/llb/llb2Bad.c @@ -63,15 +63,16 @@ 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 = Cudd_bddAnd( dd, bBdd0, bBdd1 ); Cudd_Ref( (DdNode *)pObj->pData ); - - if ( i % 10 == 0 && TimeOut && clock() >= TimeOut ) + pObj->pData = Extra_bddAndTime( dd, bBdd0, bBdd1, TimeOut ); + if ( pObj->pData == NULL ) { - Vec_PtrForEachEntryStop( Aig_Obj_t *, vNodes, pObj, k, i+1 ) - Cudd_RecursiveDeref( dd, (DdNode *)pObj->pData ); + Vec_PtrForEachEntryStop( Aig_Obj_t *, vNodes, pObj, k, i ) + if ( pObj->pData ) + Cudd_RecursiveDeref( dd, (DdNode *)pObj->pData ); Vec_PtrFree( vNodes ); return NULL; } + Cudd_Ref( (DdNode *)pObj->pData ); } // quantify PIs of each PO bResult = Cudd_ReadLogicZero( dd ); Cudd_Ref( bResult ); @@ -112,8 +113,7 @@ DdNode * Llb_BddQuantifyPis( Aig_Man_t * pInit, DdManager * dd, DdNode * bFunc ) assert( Cudd_ReadSize(dd) == Aig_ManPiNum(pInit) ); // create PI cube bCube = Cudd_ReadOne( dd ); Cudd_Ref( bCube ); - Saig_ManForEachPi( pInit, pObj, i ) - { + Saig_ManForEachPi( pInit, pObj, i ) { bVar = Cudd_bddIthVar( dd, Aig_ManRegNum(pInit) + i ); bCube = Cudd_bddAnd( dd, bTemp = bCube, bVar ); Cudd_Ref( bCube ); Cudd_RecursiveDeref( dd, bTemp ); diff --git a/src/aig/llb/llb3Image.c b/src/aig/llb/llb3Image.c index 87e09c46..9bb01195 100644 --- a/src/aig/llb/llb3Image.c +++ b/src/aig/llb/llb3Image.c @@ -334,7 +334,7 @@ int Llb_NonlinQuantify1( Llb_Mgr_t * p, Llb_Prt_t * pPart, int fSubset ) SeeAlso [] ***********************************************************************/ -int Llb_NonlinQuantify2( Llb_Mgr_t * p, Llb_Prt_t * pPart1, Llb_Prt_t * pPart2, int Limit ) +int Llb_NonlinQuantify2( Llb_Mgr_t * p, Llb_Prt_t * pPart1, Llb_Prt_t * pPart2, int Limit, int TimeOut ) { int fVerbose = 0; Llb_Var_t * pVar; @@ -358,10 +358,10 @@ Extra_bddPrintSupport( p->dd, bCube ); printf( "\n" ); // derive new function // bFunc = Cudd_bddAndAbstract( p->dd, pPart1->bFunc, pPart2->bFunc, bCube ); Cudd_Ref( bFunc ); +/* bFunc = Cudd_bddAndAbstractLimit( p->dd, pPart1->bFunc, pPart2->bFunc, bCube, Limit ); if ( bFunc == NULL ) { -/* int RetValue; Cudd_RecursiveDeref( p->dd, bCube ); if ( pPart1->nSize < pPart2->nSize ) @@ -370,12 +370,21 @@ Extra_bddPrintSupport( p->dd, bCube ); printf( "\n" ); RetValue = Llb_NonlinQuantify1( p, pPart2, 1 ); if ( RetValue ) Limit = Limit + 1000; - Llb_NonlinQuantify2( p, pPart1, pPart2, Limit ); + Llb_NonlinQuantify2( p, pPart1, pPart2, Limit, TimeOut ); + return 0; + } + Cudd_Ref( bFunc ); */ - return 1; + + bFunc = Extra_bddAndAbstractTime( p->dd, pPart1->bFunc, pPart2->bFunc, bCube, TimeOut ); + if ( bFunc == NULL ) + { + Cudd_RecursiveDeref( p->dd, bCube ); + return 0; } Cudd_Ref( bFunc ); Cudd_RecursiveDeref( p->dd, bCube ); + // create new partition pTemp = p->pParts[p->iPartFree] = ABC_CALLOC( Llb_Prt_t, 1 ); pTemp->iPart = p->iPartFree++; @@ -454,7 +463,7 @@ printf( "Updating partitiong %d with singlton vars.\n", pTemp->iPart ); if ( fVerbose ) Llb_NonlinPrint( p ); Vec_PtrFree( vSingles ); - return 0; + return 1; } /**Function************************************************************* @@ -529,7 +538,7 @@ Vec_Ptr_t * Llb_NonlinBuildBdds( Aig_Man_t * p, Vec_Ptr_t * vLower, Vec_Ptr_t * Vec_Ptr_t * vNodes, * vResult; Aig_Obj_t * pObj; DdNode * bBdd0, * bBdd1, * bProd; - int i; + int i, k; Aig_ManConst1(p)->pData = Cudd_ReadOne( dd ); Vec_PtrForEachEntry( Aig_Obj_t *, vLower, pObj, i ) @@ -540,16 +549,16 @@ Vec_Ptr_t * Llb_NonlinBuildBdds( Aig_Man_t * p, Vec_Ptr_t * vLower, Vec_Ptr_t * { 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 ) + pObj->pData = Extra_bddAndTime( dd, bBdd0, bBdd1, TimeOut ); + if ( pObj->pData == NULL ) { - Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i ) + Vec_PtrForEachEntryStop( Aig_Obj_t *, vNodes, pObj, k, i ) if ( pObj->pData ) Cudd_RecursiveDeref( dd, (DdNode *)pObj->pData ); Vec_PtrFree( vNodes ); return NULL; } + Cudd_Ref( (DdNode *)pObj->pData ); } vResult = Vec_PtrAlloc( 100 ); @@ -882,7 +891,7 @@ DdNode * Llb_NonlinImage( Aig_Man_t * pAig, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vRo { clk2 = clock(); nReorders = Cudd_ReadReorderings(dd); - if ( Llb_NonlinQuantify2( p, pPart1, pPart2, Limit ) ) + if ( !Llb_NonlinQuantify2( p, pPart1, pPart2, Limit, TimeOut ) ) { Llb_NonlinFree( p ); return NULL; diff --git a/src/aig/llb/llbInt.h b/src/aig/llb/llbInt.h index 36d3796c..1294438e 100644 --- a/src/aig/llb/llbInt.h +++ b/src/aig/llb/llbInt.h @@ -168,7 +168,7 @@ extern DdNode * Llb_ImgComputeImage( Aig_Man_t * pAig, Vec_Ptr_t * vDdMan /*=== llb3Image.c ======================================================*/ extern DdNode * Llb_NonlinImage( Aig_Man_t * pAig, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vRoots, int * pVars2Q, - DdManager * dd, DdNode * bCurrent, int fReorder, int fVerbose, int * pOrder, int Limit, int TimeLimit ); + DdManager * dd, DdNode * bCurrent, int fReorder, int fVerbose, int * pOrder, int Limit, int TimeTarget ); ABC_NAMESPACE_HEADER_END |