From a7e214bb01085492e330186295a71da35846a6b7 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sun, 13 Feb 2011 20:50:29 -0800 Subject: Improved timeout in the BDD reachability engines. --- src/aig/llb/llb1Reach.c | 61 ++++++++++++++++++++++++++++++++++--------- src/aig/llb/llb2Bad.c | 7 +++-- src/aig/llb/llb2Core.c | 47 ++++++++++++++++++++++++++++----- src/aig/llb/llb2Driver.c | 7 +++-- src/aig/llb/llb2Image.c | 27 ++++++++++++++----- src/aig/llb/llb3Image.c | 23 ++++++++++++---- src/aig/llb/llb3Nonlin.c | 46 +++++++++++++++++++++++++++----- src/bdd/cudd/cuddAndAbs.c | 3 +++ src/bdd/cudd/cuddBddIte.c | 3 +++ src/bdd/cudd/cuddBridge.c | 5 ++++ src/misc/extra/extraBddMisc.c | 5 ++++ 11 files changed, 195 insertions(+), 39 deletions(-) (limited to 'src') diff --git a/src/aig/llb/llb1Reach.c b/src/aig/llb/llb1Reach.c index 443d2d81..32944bef 100644 --- a/src/aig/llb/llb1Reach.c +++ b/src/aig/llb/llb1Reach.c @@ -48,9 +48,10 @@ DdNode * Llb_ManConstructOutBdd( Aig_Man_t * pAig, Aig_Obj_t * pNode, DdManager DdNode * bBdd0, * bBdd1, * bFunc; Vec_Ptr_t * vNodes; Aig_Obj_t * pObj; - int i; + int i, TimeStop; if ( Aig_ObjFanin0(pNode) == Aig_ManConst1(pAig) ) return Cudd_NotCond( Cudd_ReadOne(dd), Aig_ObjFaninC0(pNode) ); + TimeStop = dd->TimeStop; dd->TimeStop = 0; vNodes = Aig_ManDfsNodes( pAig, &pNode, 1 ); assert( Vec_PtrSize(vNodes) > 0 ); Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i ) @@ -72,6 +73,7 @@ DdNode * Llb_ManConstructOutBdd( Aig_Man_t * pAig, Aig_Obj_t * pNode, DdManager if ( Aig_ObjIsPo(pNode) ) bFunc = Cudd_NotCond( bFunc, Aig_ObjFaninC0(pNode) ); Cudd_Deref( bFunc ); + dd->TimeStop = TimeStop; return bFunc; } @@ -98,7 +100,8 @@ DdNode * Llb_ManConstructGroupBdd( Llb_Man_t * p, Llb_Grp_t * pGroup ) { bBdd0 = Cudd_NotCond( Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj) ); bBdd1 = Cudd_NotCond( Aig_ObjFanin1(pObj)->pData, Aig_ObjFaninC1(pObj) ); - pObj->pData = Extra_bddAndTime( p->dd, bBdd0, bBdd1, p->pPars->TimeTarget ); +// pObj->pData = Extra_bddAndTime( p->dd, bBdd0, bBdd1, p->pPars->TimeTarget ); + pObj->pData = Cudd_bddAnd( p->dd, bBdd0, bBdd1 ); if ( pObj->pData == NULL ) { Vec_PtrForEachEntryStop( Aig_Obj_t *, pGroup->vNodes, pObj, k, i ) @@ -117,7 +120,8 @@ DdNode * Llb_ManConstructGroupBdd( Llb_Man_t * p, Llb_Grp_t * pGroup ) bBdd0 = (DdNode *)pObj->pData; bBdd1 = Cudd_bddIthVar( p->dd, Vec_IntEntry(p->vObj2Var, Aig_ObjId(pObj)) ); bXor = Cudd_bddXor( p->dd, bBdd0, bBdd1 ); Cudd_Ref( bXor ); - bRes = Extra_bddAndTime( p->dd, bTemp = bRes, Cudd_Not(bXor), p->pPars->TimeTarget ); +// bRes = Extra_bddAndTime( p->dd, bTemp = bRes, Cudd_Not(bXor), p->pPars->TimeTarget ); + bRes = Cudd_bddAnd( p->dd, bTemp = bRes, Cudd_Not(bXor) ); if ( bRes == NULL ) { Cudd_RecursiveDeref( p->dd, bTemp ); @@ -153,6 +157,8 @@ DdNode * Llb_ManConstructQuantCubeIntern( Llb_Man_t * p, Llb_Grp_t * pGroup, int Aig_Obj_t * pObj; DdNode * bRes, * bTemp, * bVar; int i, iGroupFirst, iGroupLast; + int TimeStop; + TimeStop = p->dd->TimeStop; p->dd->TimeStop = 0; bRes = Cudd_ReadOne( p->dd ); Cudd_Ref( bRes ); Vec_PtrForEachEntry( Aig_Obj_t *, pGroup->vIns, pObj, i ) { @@ -177,6 +183,7 @@ DdNode * Llb_ManConstructQuantCubeIntern( Llb_Man_t * p, Llb_Grp_t * pGroup, int Cudd_RecursiveDeref( p->dd, bTemp ); } Cudd_Deref( bRes ); + p->dd->TimeStop = TimeStop; return bRes; } @@ -195,7 +202,8 @@ DdNode * Llb_ManConstructQuantCube( Llb_Man_t * p, Llb_Grp_t * pGroup, int iGrpP { Aig_Obj_t * pObj; DdNode * bRes, * bTemp, * bVar; - int i, iGroupLast; + int i, iGroupLast, TimeStop; + TimeStop = p->dd->TimeStop; p->dd->TimeStop = 0; bRes = Cudd_ReadOne( p->dd ); Cudd_Ref( bRes ); Vec_PtrForEachEntry( Aig_Obj_t *, pGroup->vIns, pObj, i ) { @@ -218,6 +226,7 @@ DdNode * Llb_ManConstructQuantCube( Llb_Man_t * p, Llb_Grp_t * pGroup, int iGrpP Cudd_RecursiveDeref( p->dd, bTemp ); } Cudd_Deref( bRes ); + p->dd->TimeStop = TimeStop; return bRes; } @@ -236,7 +245,8 @@ DdNode * Llb_ManComputeInitState( Llb_Man_t * p, DdManager * dd ) { Aig_Obj_t * pObj; DdNode * bRes, * bVar, * bTemp; - int i, iVar; + int i, iVar, TimeStop; + TimeStop = dd->TimeStop; dd->TimeStop = 0; bRes = Cudd_ReadOne( dd ); Cudd_Ref( bRes ); Saig_ManForEachLo( p->pAig, pObj, i ) { @@ -246,6 +256,7 @@ DdNode * Llb_ManComputeInitState( Llb_Man_t * p, DdManager * dd ) Cudd_RecursiveDeref( dd, bTemp ); } Cudd_Deref( bRes ); + dd->TimeStop = TimeStop; return bRes; } @@ -280,12 +291,20 @@ DdNode * Llb_ManComputeImage( Llb_Man_t * p, DdNode * bInit ) Cudd_Ref( bGroup ); // quantify variables appearing only in this group bCube = Llb_ManConstructQuantCubeIntern( p, pGroup, i ); Cudd_Ref( bCube ); - bGroup = Cudd_bddExistAbstract( p->dd, bTemp = bGroup, bCube ); Cudd_Ref( bGroup ); + bGroup = Cudd_bddExistAbstract( p->dd, bTemp = bGroup, bCube ); + if ( bGroup == NULL ) + { + Cudd_RecursiveDeref( p->dd, bTemp ); + Cudd_RecursiveDeref( p->dd, bCube ); + return NULL; + } + Cudd_Ref( bGroup ); Cudd_RecursiveDeref( p->dd, bTemp ); Cudd_RecursiveDeref( p->dd, bCube ); // perform partial product bCube = Llb_ManConstructQuantCube( p, pGroup, i ); Cudd_Ref( bCube ); - bImage = Extra_bddAndAbstractTime( p->dd, bTemp = bImage, bGroup, bCube, p->pPars->TimeTarget ); +// bImage = Extra_bddAndAbstractTime( p->dd, bTemp = bImage, bGroup, bCube, p->pPars->TimeTarget ); + bImage = Cudd_bddAndAbstract( p->dd, bTemp = bImage, bGroup, bCube ); if ( bImage == NULL ) { Cudd_RecursiveDeref( p->dd, bTemp ); @@ -331,9 +350,10 @@ DdNode * Llb_ManCreateConstraints( Llb_Man_t * p, Vec_Int_t * vHints, int fUseNs { DdNode * bConstr, * bFunc, * bTemp; Aig_Obj_t * pObj; - int i, Entry; + int i, Entry, TimeStop; if ( vHints == NULL ) return Cudd_ReadOne( p->dd ); + TimeStop = p->dd->TimeStop; p->dd->TimeStop = 0; assert( Aig_ManPiNum(p->pAig) == Aig_ManPiNum(p->pAigGlo) ); // assign const and PI nodes to the original AIG Aig_ManCleanData( p->pAig ); @@ -367,6 +387,7 @@ DdNode * Llb_ManCreateConstraints( Llb_Man_t * p, Vec_Int_t * vHints, int fUseNs Cudd_RecursiveDeref( p->dd, bFunc ); } Cudd_Deref( bConstr ); + p->dd->TimeStop = TimeStop; return bConstr; } @@ -558,7 +579,8 @@ int Llb_ManReachability( Llb_Man_t * p, Vec_Int_t * vHints, DdManager ** pddGlo // remap these states into the current state vars // bNext = Extra_TransferPermute( p->dd, p->ddG, bTemp = bNext, pNs2Glo ); Cudd_Ref( bNext ); // Cudd_RecursiveDeref( p->dd, bTemp ); - bNext = Extra_TransferPermuteTime( p->dd, p->ddG, bTemp = bNext, pNs2Glo, p->pPars->TimeTarget ); +// bNext = Extra_TransferPermuteTime( p->dd, p->ddG, bTemp = bNext, pNs2Glo, p->pPars->TimeTarget ); + bNext = Extra_TransferPermute( p->dd, p->ddG, bTemp = bNext, pNs2Glo ); if ( bNext == NULL ) { if ( !p->pPars->fSilent ) @@ -590,7 +612,14 @@ int Llb_ManReachability( Llb_Man_t * p, Vec_Int_t * vHints, DdManager ** pddGlo } // get the new states - bCurrent = Cudd_bddAnd( p->ddG, bNext, Cudd_Not(bReached) ); Cudd_Ref( bCurrent ); + bCurrent = Cudd_bddAnd( p->ddG, bNext, Cudd_Not(bReached) ); + if ( bCurrent == NULL ) + { + Cudd_RecursiveDeref( p->ddG, bNext ); bNext = NULL; + Cudd_RecursiveDeref( p->ddG, bReached ); bReached = NULL; + break; + } + Cudd_Ref( bCurrent ); // minimize the new states with the reached states // bCurrent = Cudd_bddConstrain( p->ddG, bTemp = bCurrent, Cudd_Not(bReached) ); Cudd_Ref( bCurrent ); // bCurrent = Cudd_bddRestrict( p->ddG, bTemp = bCurrent, Cudd_Not(bReached) ); Cudd_Ref( bCurrent ); @@ -600,7 +629,8 @@ int Llb_ManReachability( Llb_Man_t * p, Vec_Int_t * vHints, DdManager ** pddGlo // remap these states into the current state vars // bCurrent = Extra_TransferPermute( p->ddG, p->dd, bTemp = bCurrent, pGlo2Cs ); Cudd_Ref( bCurrent ); // Cudd_RecursiveDeref( p->ddG, bTemp ); - bCurrent = Extra_TransferPermuteTime( p->ddG, p->dd, bTemp = bCurrent, pGlo2Cs, p->pPars->TimeTarget ); +// bCurrent = Extra_TransferPermuteTime( p->ddG, p->dd, bTemp = bCurrent, pGlo2Cs, p->pPars->TimeTarget ); + bCurrent = Extra_TransferPermute( p->ddG, p->dd, bTemp = bCurrent, pGlo2Cs ); if ( bCurrent == NULL ) { if ( !p->pPars->fSilent ) @@ -617,7 +647,14 @@ int Llb_ManReachability( Llb_Man_t * p, Vec_Int_t * vHints, DdManager ** pddGlo // add to the reached states - bReached = Cudd_bddOr( p->ddG, bTemp = bReached, bNext ); Cudd_Ref( bReached ); + bReached = Cudd_bddOr( p->ddG, bTemp = bReached, bNext ); + if ( bReached == NULL ) + { + Cudd_RecursiveDeref( p->ddG, bTemp ); bTemp = NULL; + Cudd_RecursiveDeref( p->ddG, bNext ); bNext = NULL; + break; + } + Cudd_Ref( bReached ); Cudd_RecursiveDeref( p->ddG, bTemp ); Cudd_RecursiveDeref( p->ddG, bNext ); bNext = NULL; 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; } diff --git a/src/aig/llb/llb2Core.c b/src/aig/llb/llb2Core.c index 4685db0e..446f1a67 100644 --- a/src/aig/llb/llb2Core.c +++ b/src/aig/llb/llb2Core.c @@ -68,7 +68,8 @@ struct Llb_Img_t_ DdNode * Llb_CoreComputeCube( DdManager * dd, Vec_Int_t * vVars, int fUseVarIndex, char * pValues ) { DdNode * bRes, * bVar, * bTemp; - int i, iVar, Index; + int i, iVar, Index, TimeStop; + TimeStop = dd->TimeStop; dd->TimeStop = 0; bRes = Cudd_ReadOne( dd ); Cudd_Ref( bRes ); Vec_IntForEachEntry( vVars, Index, i ) { @@ -78,6 +79,7 @@ DdNode * Llb_CoreComputeCube( DdManager * dd, Vec_Int_t * vVars, int fUseVarInde Cudd_RecursiveDeref( dd, bTemp ); } Cudd_Deref( bRes ); + dd->TimeStop = TimeStop; return bRes; } @@ -102,6 +104,9 @@ Abc_Cex_t * Llb_CoreDeriveCex( Llb_Img_t * p ) char * pValues = ABC_ALLOC( char, Cudd_ReadSize(p->ddR) ); assert( Vec_PtrSize(p->vRings) > 0 ); + p->dd->TimeStop = 0; + p->ddR->TimeStop = 0; + // get supports and quantified variables Vec_PtrReverseOrder( p->vDdMans ); vSupps = Llb_ImgSupports( p->pAig, p->vDdMans, p->vVarsNs, p->vVarsCs, 1, 0 ); @@ -244,7 +249,15 @@ int Llb_CoreReachability_int( Llb_Img_t * p, Vec_Ptr_t * vQuant0, Vec_Ptr_t * vQ bReached = Cudd_bddTransfer( p->ddR, p->ddG, bCurrent ); Cudd_Ref( bReached ); Cudd_RecursiveDeref( p->ddR, bCurrent ); // move init state to the working manager - bCurrent = Extra_TransferPermute( p->ddG, p->dd, bReached, pGlo2Loc ); Cudd_Ref( bCurrent ); + bCurrent = Extra_TransferPermute( p->ddG, p->dd, bReached, pGlo2Loc ); + if ( bCurrent == NULL ) + { + Cudd_RecursiveDeref( p->ddG, bReached ); + if ( !p->pPars->fSilent ) + printf( "Reached timeout (%d seconds) during transfer 0.\n", p->pPars->TimeLimit ); + return -1; + } + Cudd_Ref( bCurrent ); } else { @@ -282,7 +295,17 @@ int Llb_CoreReachability_int( Llb_Img_t * p, Vec_Ptr_t * vQuant0, Vec_Ptr_t * vQ } // save the onion ring - bTemp = Extra_TransferPermute( p->dd, p->ddR, bCurrent, pLoc2GloR ); Cudd_Ref( bTemp ); + bTemp = Extra_TransferPermute( p->dd, p->ddR, bCurrent, pLoc2GloR ); + if ( bTemp == NULL ) + { + if ( !p->pPars->fSilent ) + printf( "Reached timeout (%d seconds) during image computation.\n", p->pPars->TimeLimit ); + p->pPars->iFrame = nIters - 1; + Cudd_RecursiveDeref( p->dd, bCurrent ); bCurrent = NULL; + Cudd_RecursiveDeref( p->ddG, bReached ); bReached = NULL; + return -1; + } + Cudd_Ref( bTemp ); Vec_PtrPush( p->vRings, bTemp ); // check it for bad states @@ -325,7 +348,8 @@ int Llb_CoreReachability_int( Llb_Img_t * p, Vec_Ptr_t * vQuant0, Vec_Ptr_t * vQ // bNext = Extra_TransferPermute( p->dd, p->ddG, bTemp = bNext, pLoc2Glo ); Cudd_Ref( bNext ); // Cudd_RecursiveDeref( p->dd, bTemp ); - bNext = Extra_TransferPermuteTime( p->dd, p->ddG, bTemp = bNext, pLoc2Glo, p->pPars->TimeTarget ); +// bNext = Extra_TransferPermuteTime( p->dd, p->ddG, bTemp = bNext, pLoc2Glo, p->pPars->TimeTarget ); + bNext = Extra_TransferPermute( p->dd, p->ddG, bTemp = bNext, pLoc2Glo ); if ( bNext == NULL ) { if ( !p->pPars->fSilent ) @@ -347,13 +371,24 @@ int Llb_CoreReachability_int( Llb_Img_t * p, Vec_Ptr_t * vQuant0, Vec_Ptr_t * vQ } // get the new states - bCurrent = Cudd_bddAnd( p->ddG, bNext, Cudd_Not(bReached) ); Cudd_Ref( bCurrent ); + bCurrent = Cudd_bddAnd( p->ddG, bNext, Cudd_Not(bReached) ); + 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; + Cudd_RecursiveDeref( p->ddG, bNext ); + Cudd_RecursiveDeref( p->ddG, bReached ); bReached = NULL; + return -1; + } + Cudd_Ref( bCurrent ); // remap these states into the current state vars // bCurrent = Extra_TransferPermute( p->ddG, p->dd, bTemp = bCurrent, pGlo2Loc ); Cudd_Ref( bCurrent ); // Cudd_RecursiveDeref( p->ddG, bTemp ); - bCurrent = Extra_TransferPermuteTime( p->ddG, p->dd, bTemp = bCurrent, pGlo2Loc, p->pPars->TimeTarget ); +// bCurrent = Extra_TransferPermuteTime( p->ddG, p->dd, bTemp = bCurrent, pGlo2Loc, p->pPars->TimeTarget ); + bCurrent = Extra_TransferPermute( p->ddG, p->dd, bTemp = bCurrent, pGlo2Loc ); if ( bCurrent == NULL ) { if ( !p->pPars->fSilent ) diff --git a/src/aig/llb/llb2Driver.c b/src/aig/llb/llb2Driver.c index aab65317..3b4f23fc 100644 --- a/src/aig/llb/llb2Driver.c +++ b/src/aig/llb/llb2Driver.c @@ -129,7 +129,8 @@ DdNode * Llb_DriverPhaseCube( Aig_Man_t * pAig, Vec_Int_t * vDriRefs, DdManager { DdNode * bCube, * bVar, * bTemp; Aig_Obj_t * pObj; - int i; + int i, TimeStop; + TimeStop = dd->TimeStop; dd->TimeStop = 0; bCube = Cudd_ReadOne( dd ); Cudd_Ref( bCube ); Saig_ManForEachLi( pAig, pObj, i ) { @@ -143,6 +144,7 @@ DdNode * Llb_DriverPhaseCube( Aig_Man_t * pAig, Vec_Int_t * vDriRefs, DdManager Cudd_RecursiveDeref( dd, bTemp ); } Cudd_Deref( bCube ); + dd->TimeStop = TimeStop; return bCube; } @@ -181,7 +183,8 @@ DdManager * Llb_DriverLastPartition( Aig_Man_t * p, Vec_Int_t * vVarsNs, int Tim bVar2 = Cudd_NotCond( bVar2, Aig_ObjFaninC0(pObj) ); bProd = Cudd_bddXnor( dd, bVar1, bVar2 ); Cudd_Ref( bProd ); // bRes = Cudd_bddAnd( dd, bTemp = bRes, bProd ); Cudd_Ref( bRes ); - bRes = Extra_bddAndTime( dd, bTemp = bRes, bProd, TimeTarget ); +// bRes = Extra_bddAndTime( dd, bTemp = bRes, bProd, TimeTarget ); + bRes = Cudd_bddAnd( dd, bTemp = bRes, bProd ); if ( bRes == NULL ) { Cudd_RecursiveDeref( dd, bTemp ); diff --git a/src/aig/llb/llb2Image.c b/src/aig/llb/llb2Image.c index 78ff9da1..caf8f9f7 100644 --- a/src/aig/llb/llb2Image.c +++ b/src/aig/llb/llb2Image.c @@ -200,7 +200,8 @@ DdManager * Llb_ImgPartition( Aig_Man_t * p, Vec_Ptr_t * vLower, Vec_Ptr_t * vUp 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 ); - pObj->pData = Extra_bddAndTime( dd, bBdd0, bBdd1, TimeTarget ); +// pObj->pData = Extra_bddAndTime( dd, bBdd0, bBdd1, TimeTarget ); + pObj->pData = Cudd_bddAnd( dd, bBdd0, bBdd1 ); if ( pObj->pData == NULL ) { Cudd_Quit( dd ); @@ -217,7 +218,8 @@ DdManager * Llb_ImgPartition( Aig_Man_t * p, Vec_Ptr_t * vLower, Vec_Ptr_t * vUp assert( Aig_ObjIsNode(pObj) ); bProd = Cudd_bddXnor( dd, Cudd_bddIthVar(dd, Aig_ObjId(pObj)), (DdNode *)pObj->pData ); Cudd_Ref( bProd ); // bRes = Cudd_bddAnd( dd, bTemp = bRes, bProd ); Cudd_Ref( bRes ); - bRes = Extra_bddAndTime( dd, bTemp = bRes, bProd, TimeTarget ); +// bRes = Extra_bddAndTime( dd, bTemp = bRes, bProd, TimeTarget ); + bRes = Cudd_bddAnd( dd, bTemp = bRes, bProd ); if ( bRes == NULL ) { Cudd_Quit( dd ); @@ -257,7 +259,8 @@ DdNode * Llb_ImgComputeCube( Aig_Man_t * pAig, Vec_Int_t * vNodeIds, DdManager * { DdNode * bProd, * bTemp; Aig_Obj_t * pObj; - int i; + int i, TimeStop; + TimeStop = dd->TimeStop; dd->TimeStop = 0; bProd = Cudd_ReadOne(dd); Cudd_Ref( bProd ); Aig_ManForEachNodeVec( pAig, vNodeIds, pObj, i ) { @@ -265,6 +268,7 @@ DdNode * Llb_ImgComputeCube( Aig_Man_t * pAig, Vec_Int_t * vNodeIds, DdManager * Cudd_RecursiveDeref( dd, bTemp ); } Cudd_Deref( bProd ); + dd->TimeStop = TimeStop; return bProd; } @@ -376,7 +380,14 @@ DdNode * Llb_ImgComputeImage( Aig_Man_t * pAig, Vec_Ptr_t * vDdMans, DdManager * { // quantify unique vriables bCube = Llb_ImgComputeCube( pAig, (Vec_Int_t *)Vec_PtrEntry(vQuant0, 0), dd ); Cudd_Ref( bCube ); - bImage = Cudd_bddExistAbstract( dd, bTemp = bImage, bCube ); Cudd_Ref( bImage ); + bImage = Cudd_bddExistAbstract( dd, bTemp = bImage, bCube ); + if ( bImage == NULL ) + { + Cudd_RecursiveDeref( dd, bTemp ); + Cudd_RecursiveDeref( dd, bCube ); + return NULL; + } + Cudd_Ref( bImage ); Cudd_RecursiveDeref( dd, bTemp ); Cudd_RecursiveDeref( dd, bCube ); } @@ -387,13 +398,17 @@ DdNode * Llb_ImgComputeImage( Aig_Man_t * pAig, Vec_Ptr_t * vDdMans, DdManager * if ( fVerbose ) printf( " %2d : ", i ); // transfer the BDD from the group manager to the main manager - bGroup = Cudd_bddTransfer( ddPart, dd, ddPart->bFunc ); Cudd_Ref( bGroup ); + bGroup = Cudd_bddTransfer( ddPart, dd, ddPart->bFunc ); + if ( bGroup == NULL ) + return NULL; + Cudd_Ref( bGroup ); if ( fVerbose ) printf( "Pt0 =%6d. Pt1 =%6d. ", Cudd_DagSize(ddPart->bFunc), Cudd_DagSize(bGroup) ); // perform partial product bCube = Llb_ImgComputeCube( pAig, (Vec_Int_t *)Vec_PtrEntry(vQuant1, i+1), dd ); Cudd_Ref( bCube ); // bImage = Cudd_bddAndAbstract( dd, bTemp = bImage, bGroup, bCube ); - bImage = Extra_bddAndAbstractTime( dd, bTemp = bImage, bGroup, bCube, TimeTarget ); +// bImage = Extra_bddAndAbstractTime( dd, bTemp = bImage, bGroup, bCube, TimeTarget ); + bImage = Cudd_bddAndAbstract( dd, bTemp = bImage, bGroup, bCube ); if ( bImage == NULL ) { Cudd_RecursiveDeref( dd, bTemp ); diff --git a/src/aig/llb/llb3Image.c b/src/aig/llb/llb3Image.c index 9bb01195..2c16c550 100644 --- a/src/aig/llb/llb3Image.c +++ b/src/aig/llb/llb3Image.c @@ -141,7 +141,8 @@ DdNode * Llb_NonlinCreateCube1( Llb_Mgr_t * p, Llb_Prt_t * pPart ) { DdNode * bCube, * bTemp; Llb_Var_t * pVar; - int i; + int i, TimeStop; + TimeStop = p->dd->TimeStop; p->dd->TimeStop = 0; bCube = Cudd_ReadOne(p->dd); Cudd_Ref( bCube ); Llb_PartForEachVar( p, pPart, pVar, i ) { @@ -153,6 +154,7 @@ DdNode * Llb_NonlinCreateCube1( Llb_Mgr_t * p, Llb_Prt_t * pPart ) Cudd_RecursiveDeref( p->dd, bTemp ); } Cudd_Deref( bCube ); + p->dd->TimeStop = TimeStop; return bCube; } @@ -171,7 +173,8 @@ DdNode * Llb_NonlinCreateCube2( Llb_Mgr_t * p, Llb_Prt_t * pPart1, Llb_Prt_t * p { DdNode * bCube, * bTemp; Llb_Var_t * pVar; - int i; + int i, TimeStop; + TimeStop = p->dd->TimeStop; p->dd->TimeStop = 0; bCube = Cudd_ReadOne(p->dd); Cudd_Ref( bCube ); Llb_PartForEachVar( p, pPart1, pVar, i ) { @@ -186,6 +189,7 @@ DdNode * Llb_NonlinCreateCube2( Llb_Mgr_t * p, Llb_Prt_t * pPart1, Llb_Prt_t * p } } Cudd_Deref( bCube ); + p->dd->TimeStop = TimeStop; return bCube; } @@ -376,7 +380,8 @@ Extra_bddPrintSupport( p->dd, bCube ); printf( "\n" ); Cudd_Ref( bFunc ); */ - bFunc = Extra_bddAndAbstractTime( p->dd, pPart1->bFunc, pPart2->bFunc, bCube, TimeOut ); +// bFunc = Extra_bddAndAbstractTime( p->dd, pPart1->bFunc, pPart2->bFunc, bCube, TimeOut ); + bFunc = Cudd_bddAndAbstract( p->dd, pPart1->bFunc, pPart2->bFunc, bCube ); if ( bFunc == NULL ) { Cudd_RecursiveDeref( p->dd, bCube ); @@ -549,7 +554,8 @@ 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 = 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 ) @@ -907,7 +913,14 @@ DdNode * Llb_NonlinImage( Aig_Man_t * pAig, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vRo bFunc = Cudd_ReadOne(p->dd); Cudd_Ref( bFunc ); Llb_MgrForEachPart( p, pPart, i ) { - bFunc = Cudd_bddAnd( p->dd, bTemp = bFunc, pPart->bFunc ); Cudd_Ref( bFunc ); + bFunc = Cudd_bddAnd( p->dd, bTemp = bFunc, pPart->bFunc ); + if ( bFunc == NULL ) + { + Cudd_RecursiveDeref( p->dd, bTemp ); + Llb_NonlinFree( p ); + return NULL; + } + Cudd_Ref( bFunc ); Cudd_RecursiveDeref( p->dd, bTemp ); } nSuppMax = p->nSuppMax; diff --git a/src/aig/llb/llb3Nonlin.c b/src/aig/llb/llb3Nonlin.c index 62ce441c..c10db9e3 100644 --- a/src/aig/llb/llb3Nonlin.c +++ b/src/aig/llb/llb3Nonlin.c @@ -210,7 +210,8 @@ DdNode * Llb_NonlinComputeInitState( Aig_Man_t * pAig, DdManager * dd ) { Aig_Obj_t * pObj; DdNode * bRes, * bVar, * bTemp; - int i, iVar; + int i, iVar, TimeStop; + TimeStop = dd->TimeStop; dd->TimeStop = 0; bRes = Cudd_ReadOne( dd ); Cudd_Ref( bRes ); Saig_ManForEachLo( pAig, pObj, i ) { @@ -220,6 +221,7 @@ DdNode * Llb_NonlinComputeInitState( Aig_Man_t * pAig, DdManager * dd ) Cudd_RecursiveDeref( dd, bTemp ); } Cudd_Deref( bRes ); + dd->TimeStop = TimeStop; return bRes; } @@ -245,6 +247,9 @@ Abc_Cex_t * Llb_NonlinDeriveCex( Llb_Mnn_t * p ) char * pValues = ABC_ALLOC( char, Cudd_ReadSize(p->ddR) ); assert( Vec_PtrSize(p->vRings) > 0 ); + p->dd->TimeStop = 0; + p->ddR->TimeStop = 0; + // update quantifiable vars memset( p->pVars2Q, 0, sizeof(int) * Cudd_ReadSize(p->dd) ); vVarsNs = Vec_IntAlloc( Aig_ManRegNum(p->pAig) ); @@ -437,7 +442,16 @@ int Llb_NonlinReachability( Llb_Mnn_t * p ) } // save the onion ring - bTemp = Extra_TransferPermute( p->dd, p->ddR, bCurrent, Vec_IntArray(p->vCs2Glo) ); Cudd_Ref( bTemp ); + bTemp = Extra_TransferPermute( p->dd, p->ddR, bCurrent, Vec_IntArray(p->vCs2Glo) ); + if ( bTemp == NULL ) + { + if ( !p->pPars->fSilent ) + printf( "Reached timeout (%d seconds) during ring transfer.\n", p->pPars->TimeLimit ); + p->pPars->iFrame = nIters - 1; + Cudd_RecursiveDeref( p->dd, bCurrent ); bCurrent = NULL; + return -1; + } + Cudd_Ref( bTemp ); Vec_PtrPush( p->vRings, bTemp ); // check it for bad states @@ -533,7 +547,8 @@ 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_TransferPermuteTime( p->dd, p->ddG, bNext, Vec_IntArray(p->vNs2Glo), p->pPars->TimeTarget ); +// p->ddG->bFunc2 = Extra_TransferPermuteTime( p->dd, p->ddG, bNext, Vec_IntArray(p->vNs2Glo), p->pPars->TimeTarget ); + p->ddG->bFunc2 = Extra_TransferPermute( p->dd, p->ddG, bNext, Vec_IntArray(p->vNs2Glo) ); if ( p->ddG->bFunc2 == NULL ) { if ( !p->pPars->fSilent ) @@ -548,12 +563,30 @@ int Llb_NonlinReachability( Llb_Mnn_t * p ) // derive new states clk3 = clock(); - p->ddG->bFunc2 = Cudd_bddAnd( p->ddG, bTemp = p->ddG->bFunc2, Cudd_Not(p->ddG->bFunc) ); Cudd_Ref( p->ddG->bFunc2 ); + p->ddG->bFunc2 = Cudd_bddAnd( p->ddG, bTemp = p->ddG->bFunc2, Cudd_Not(p->ddG->bFunc) ); + 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->ddG, bTemp ); + return -1; + } + Cudd_Ref( p->ddG->bFunc2 ); Cudd_RecursiveDeref( p->ddG, bTemp ); if ( Cudd_IsConstant(p->ddG->bFunc2) ) break; // add to the reached set - p->ddG->bFunc = Cudd_bddOr( p->ddG, bTemp = p->ddG->bFunc, p->ddG->bFunc2 ); Cudd_Ref( p->ddG->bFunc ); + p->ddG->bFunc = Cudd_bddOr( p->ddG, bTemp = p->ddG->bFunc, p->ddG->bFunc2 ); + if ( p->ddG->bFunc == 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->ddG, bTemp ); + return -1; + } + Cudd_Ref( p->ddG->bFunc ); Cudd_RecursiveDeref( p->ddG, bTemp ); p->timeGloba += clock() - clk3; @@ -564,7 +597,8 @@ int Llb_NonlinReachability( Llb_Mnn_t * p ) // move new states to the working manager clk3 = clock(); - bCurrent = Extra_TransferPermuteTime( p->ddG, p->dd, p->ddG->bFunc2, Vec_IntArray(p->vGlo2Cs), p->pPars->TimeTarget ); +// bCurrent = Extra_TransferPermuteTime( p->ddG, p->dd, p->ddG->bFunc2, Vec_IntArray(p->vGlo2Cs), p->pPars->TimeTarget ); + bCurrent = Extra_TransferPermute( p->ddG, p->dd, p->ddG->bFunc2, Vec_IntArray(p->vGlo2Cs) ); if ( bCurrent == NULL ) { if ( !p->pPars->fSilent ) diff --git a/src/bdd/cudd/cuddAndAbs.c b/src/bdd/cudd/cuddAndAbs.c index 39695918..2f38490d 100644 --- a/src/bdd/cudd/cuddAndAbs.c +++ b/src/bdd/cudd/cuddAndAbs.c @@ -259,6 +259,9 @@ cuddBddAndAbstractRecur( } } + if ( manager->TimeStop && manager->TimeStop < clock() ) + return NULL; + if (topf == top) { index = F->index; ft = cuddT(F); diff --git a/src/bdd/cudd/cuddBddIte.c b/src/bdd/cudd/cuddBddIte.c index 1b152f02..4e75aab2 100644 --- a/src/bdd/cudd/cuddBddIte.c +++ b/src/bdd/cudd/cuddBddIte.c @@ -926,6 +926,9 @@ cuddBddAndRecur( if (r != NULL) return(r); } + if ( manager->TimeStop && manager->TimeStop < clock() ) + return NULL; + /* Here we can skip the use of cuddI, because the operands are known ** to be non-constant. */ diff --git a/src/bdd/cudd/cuddBridge.c b/src/bdd/cudd/cuddBridge.c index d0f96a2f..97a6f393 100644 --- a/src/bdd/cudd/cuddBridge.c +++ b/src/bdd/cudd/cuddBridge.c @@ -975,6 +975,11 @@ cuddBddTransferRecur( /* Check the cache. */ if (st_lookup(table, (const char *)f, (char **)&res)) return(Cudd_NotCond(res,comple)); + + if ( ddS->TimeStop && ddS->TimeStop < clock() ) + return NULL; + if ( ddD->TimeStop && ddD->TimeStop < clock() ) + return NULL; /* Recursive step. */ index = f->index; diff --git a/src/misc/extra/extraBddMisc.c b/src/misc/extra/extraBddMisc.c index 69309a4d..11c7d959 100644 --- a/src/misc/extra/extraBddMisc.c +++ b/src/misc/extra/extraBddMisc.c @@ -1277,6 +1277,11 @@ extraTransferPermuteRecur( if ( st_lookup( table, ( char * ) f, ( char ** ) &res ) ) return ( Cudd_NotCond( res, comple ) ); + if ( ddS->TimeStop && ddS->TimeStop < clock() ) + return NULL; + if ( ddD->TimeStop && ddD->TimeStop < clock() ) + return NULL; + /* Recursive step. */ if ( Permute ) index = Permute[f->index]; -- cgit v1.2.3