Skip to content

A
abc
Commit a7e214bb by Alan Mishchenko
Options

Improved timeout in the BDD reachability engines.

parent 573694f9
Showing with 195 additions and 39 deletions
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;
......
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;
}
......
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 )
......
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 );
......
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 );
......
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;
......
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 )
......
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);
......
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.
*/
......
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;
......
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];
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment