From 6119f7068aea9f844ebe9b9dc6126d2883c4fecb Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Mon, 28 Feb 2011 14:52:51 -0800 Subject: Cumulative update to BDD-based reachability, speeding up &reachm and other changes. --- src/aig/llb/llb3Image.c | 228 ++++++++++++++++++++++++++++++++++++++--------- src/aig/llb/llb3Nonlin.c | 167 +++++++++++++++++----------------- src/aig/llb/llbInt.h | 6 ++ src/base/abci/abc.c | 4 +- 4 files changed, 279 insertions(+), 126 deletions(-) diff --git a/src/aig/llb/llb3Image.c b/src/aig/llb/llb3Image.c index 2c16c550..098f9f45 100644 --- a/src/aig/llb/llb3Image.c +++ b/src/aig/llb/llb3Image.c @@ -50,7 +50,6 @@ struct Llb_Mgr_t_ Vec_Ptr_t * vLeaves; // leaves in the AIG manager Vec_Ptr_t * vRoots; // roots in the AIG manager DdManager * dd; // working BDD manager - DdNode * bCurrent; // current state functions in terms of vLeaves int * pVars2Q; // variables to quantify // internal Llb_Prt_t ** pParts; // partitions @@ -613,6 +612,38 @@ void Llb_NonlinAddPair( Llb_Mgr_t * p, DdNode * bFunc, int iPart, int iVar ) Vec_IntPush( p->pParts[iPart]->vVars, iVar ); } +/**Function************************************************************* + + Synopsis [Starts non-linear quantification scheduling.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Llb_NonlinAddPartition( Llb_Mgr_t * p, int i, DdNode * bFunc ) +{ + int k, nSuppSize; + assert( !Cudd_IsConstant(bFunc) ); + // create partition + p->pParts[i] = ABC_CALLOC( Llb_Prt_t, 1 ); + p->pParts[i]->iPart = i; + p->pParts[i]->bFunc = bFunc; + p->pParts[i]->vVars = Vec_IntAlloc( 8 ); + // add support dependencies + nSuppSize = 0; + Extra_SupportArray( p->dd, bFunc, p->pSupp ); + for ( k = 0; k < p->nVars; k++ ) + { + nSuppSize += p->pSupp[k]; + if ( p->pSupp[k] && p->pVars2Q[k] ) + Llb_NonlinAddPair( p, bFunc, i, k ); + } + p->nSuppMax = ABC_MAX( p->nSuppMax, nSuppSize ); +} + /**Function************************************************************* Synopsis [Starts non-linear quantification scheduling.] @@ -627,39 +658,16 @@ void Llb_NonlinAddPair( Llb_Mgr_t * p, DdNode * bFunc, int iPart, int iVar ) int Llb_NonlinStart( Llb_Mgr_t * p, int TimeOut ) { Vec_Ptr_t * vRootBdds; - Llb_Prt_t * pPart; DdNode * bFunc; - int i, k, nSuppSize; + int i; // create and collect BDDs vRootBdds = Llb_NonlinBuildBdds( p->pAig, p->vLeaves, p->vRoots, p->dd, TimeOut ); // come referenced if ( vRootBdds == NULL ) return 0; - Vec_PtrPush( vRootBdds, p->bCurrent ); // add pairs (refs are consumed inside) Vec_PtrForEachEntry( DdNode *, vRootBdds, bFunc, i ) - { - assert( !Cudd_IsConstant(bFunc) ); - // create partition - p->pParts[i] = ABC_CALLOC( Llb_Prt_t, 1 ); - p->pParts[i]->iPart = i; - p->pParts[i]->bFunc = bFunc; - p->pParts[i]->vVars = Vec_IntAlloc( 8 ); - // add support dependencies - nSuppSize = 0; - Extra_SupportArray( p->dd, bFunc, p->pSupp ); - for ( k = 0; k < p->nVars; k++ ) - { - nSuppSize += p->pSupp[k]; - if ( p->pSupp[k] && p->pVars2Q[k] ) - Llb_NonlinAddPair( p, bFunc, i, k ); - } - p->nSuppMax = ABC_MAX( p->nSuppMax, nSuppSize ); - } + Llb_NonlinAddPartition( p, i, bFunc ); Vec_PtrFree( vRootBdds ); - // remove singles - Llb_MgrForEachPart( p, pPart, i ) - if ( Llb_NonlinHasSingletonVars(p, pPart) ) - Llb_NonlinQuantify1( p, pPart, 0 ); return 1; } @@ -672,8 +680,7 @@ int Llb_NonlinStart( Llb_Mgr_t * p, int TimeOut ) SideEffects [] SeeAlso [] - -***********************************************************************/ +**********************************************************************/ void Llb_NonlinCheckVars( Llb_Mgr_t * p ) { Llb_Var_t * pVar; @@ -736,7 +743,7 @@ int Llb_NonlinNextPartitions( Llb_Mgr_t * p, Llb_Prt_t ** ppPart1, Llb_Prt_t ** SeeAlso [] ***********************************************************************/ -void Llb_NonlinReorder( DdManager * dd, int fVerbose ) +void Llb_NonlinReorder( DdManager * dd, int fTwice, int fVerbose ) { int clk = clock(); if ( fVerbose ) @@ -744,9 +751,12 @@ void Llb_NonlinReorder( DdManager * dd, int fVerbose ) Cudd_ReduceHeap( dd, CUDD_REORDER_SYMM_SIFT, 100 ); if ( fVerbose ) Abc_Print( 1, "After =%5d. ", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) ); - Cudd_ReduceHeap( dd, CUDD_REORDER_SYMM_SIFT, 100 ); - if ( fVerbose ) - Abc_Print( 1, "After =%5d. ", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) ); + if ( fTwice ) + { + Cudd_ReduceHeap( dd, CUDD_REORDER_SYMM_SIFT, 100 ); + if ( fVerbose ) + Abc_Print( 1, "After =%5d. ", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) ); + } if ( fVerbose ) Abc_PrintTime( 1, "Time", clock() - clk ); } @@ -815,7 +825,7 @@ void Llb_NonlinVerifyScores( Llb_Mgr_t * p ) SeeAlso [] ***********************************************************************/ -Llb_Mgr_t * Llb_NonlinAlloc( Aig_Man_t * pAig, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vRoots, int * pVars2Q, DdManager * dd, DdNode * bCurrent ) +Llb_Mgr_t * Llb_NonlinAlloc( Aig_Man_t * pAig, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vRoots, int * pVars2Q, DdManager * dd ) { Llb_Mgr_t * p; p = ABC_CALLOC( Llb_Mgr_t, 1 ); @@ -823,12 +833,11 @@ Llb_Mgr_t * Llb_NonlinAlloc( Aig_Man_t * pAig, Vec_Ptr_t * vLeaves, Vec_Ptr_t * p->vLeaves = vLeaves; p->vRoots = vRoots; p->dd = dd; - p->bCurrent = bCurrent; p->pVars2Q = pVars2Q; p->nVars = Cudd_ReadSize(dd); - p->iPartFree = Vec_PtrSize(vRoots) + 1; + p->iPartFree = Vec_PtrSize(vRoots); p->pVars = ABC_CALLOC( Llb_Var_t *, p->nVars ); - p->pParts = ABC_CALLOC( Llb_Prt_t *, 2 * p->iPartFree ); + p->pParts = ABC_CALLOC( Llb_Prt_t *, 2 * p->iPartFree + 2 ); p->pSupp = ABC_ALLOC( int, Cudd_ReadSize(dd) ); return p; } @@ -880,17 +889,24 @@ DdNode * Llb_NonlinImage( Aig_Man_t * pAig, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vRo int clk = clock(), clk2; // start the manager clk2 = clock(); - p = Llb_NonlinAlloc( pAig, vLeaves, vRoots, pVars2Q, dd, bCurrent ); + p = Llb_NonlinAlloc( pAig, vLeaves, vRoots, pVars2Q, dd ); if ( !Llb_NonlinStart( p, TimeOut ) ) { Llb_NonlinFree( p ); return NULL; } + // add partition + Llb_NonlinAddPartition( p, p->iPartFree++, bCurrent ); + // remove singles + Llb_MgrForEachPart( p, pPart, i ) + if ( Llb_NonlinHasSingletonVars(p, pPart) ) + Llb_NonlinQuantify1( p, pPart, 0 ); timeBuild += clock() - clk2; timeInside = clock() - clk2; // compute scores Llb_NonlinRecomputeScores( p ); // save permutation + if ( pOrder ) memcpy( pOrder, dd->invperm, sizeof(int) * dd->size ); // iteratively quantify variables while ( Llb_NonlinNextPartitions(p, &pPart1, &pPart2) ) @@ -907,6 +923,111 @@ DdNode * Llb_NonlinImage( Aig_Man_t * pAig, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vRo if ( nReorders < Cudd_ReadReorderings(dd) ) Llb_NonlinRecomputeScores( p ); // else +// Llb_NonlinVerifyScores( p ); + } + // load partitions + 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 ); + Cudd_RecursiveDeref( p->dd, bTemp ); + } + nSuppMax = p->nSuppMax; + Llb_NonlinFree( p ); + // reorder variables + if ( fReorder ) + Llb_NonlinReorder( dd, 0, fVerbose ); + timeOther += clock() - clk - timeInside; + // return + Cudd_Deref( bFunc ); + return bFunc; +} + + + +static Llb_Mgr_t * p = NULL; + +/**Function************************************************************* + + Synopsis [Starts image computation manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +DdManager * Llb_NonlinImageStart( Aig_Man_t * pAig, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vRoots, int * pVars2Q, int * pOrder, int fFirst ) +{ + DdManager * dd; + int clk = clock(); + assert( p == NULL ); + // start a new manager (disable reordering) + dd = Cudd_Init( Aig_ManObjNumMax(pAig), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 ); + Cudd_ShuffleHeap( dd, pOrder ); +// if ( fFirst ) + Cudd_AutodynEnable( dd, CUDD_REORDER_SYMM_SIFT ); + // start the manager + p = Llb_NonlinAlloc( pAig, vLeaves, vRoots, pVars2Q, dd ); + if ( !Llb_NonlinStart( p, 0 ) ) + { + Llb_NonlinFree( p ); + return NULL; + } + timeBuild += clock() - clk; +// if ( !fFirst ) +// Cudd_AutodynEnable( dd, CUDD_REORDER_SYMM_SIFT ); + return dd; +} + +/**Function************************************************************* + + Synopsis [Performs image computation.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +DdNode * Llb_NonlinImageCompute( DdNode * bCurrent, int fReorder, int fDrop, int fVerbose, int * pOrder ) +{ + Llb_Prt_t * pPart, * pPart1, * pPart2; + DdNode * bFunc, * bTemp; + int i, nReorders, timeInside = 0; + int clk = clock(), clk2; + + // add partition + Llb_NonlinAddPartition( p, p->iPartFree++, bCurrent ); + // remove singles + Llb_MgrForEachPart( p, pPart, i ) + if ( Llb_NonlinHasSingletonVars(p, pPart) ) + Llb_NonlinQuantify1( p, pPart, 0 ); + // reorder + if ( fReorder ) + Llb_NonlinReorder( p->dd, 0, 0 ); + // save permutation + memcpy( pOrder, p->dd->invperm, sizeof(int) * p->dd->size ); + + // compute scores + Llb_NonlinRecomputeScores( p ); + // iteratively quantify variables + while ( Llb_NonlinNextPartitions(p, &pPart1, &pPart2) ) + { + clk2 = clock(); + nReorders = Cudd_ReadReorderings(p->dd); + if ( !Llb_NonlinQuantify2( p, pPart1, pPart2, 0, 0 ) ) + { + Llb_NonlinFree( p ); + return NULL; + } + timeAndEx += clock() - clk2; + timeInside += clock() - clk2; + if ( nReorders < Cudd_ReadReorderings(p->dd) ) + Llb_NonlinRecomputeScores( p ); +// else // Llb_NonlinVerifyScores( p ); } // load partitions @@ -924,16 +1045,43 @@ DdNode * Llb_NonlinImage( Aig_Man_t * pAig, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vRo Cudd_RecursiveDeref( p->dd, bTemp ); } nSuppMax = p->nSuppMax; - Llb_NonlinFree( p ); // reorder variables - if ( fReorder ) - Llb_NonlinReorder( dd, fVerbose ); +// if ( fReorder ) +// Llb_NonlinReorder( p->dd, 0, fVerbose ); + // save permutation +// memcpy( pOrder, p->dd->invperm, sizeof(int) * Cudd_ReadSize(p->dd) ); + timeOther += clock() - clk - timeInside; // return Cudd_Deref( bFunc ); return bFunc; } +/**Function************************************************************* + + Synopsis [Quits image computation manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Llb_NonlinImageQuit() +{ + DdManager * dd; + if ( p == NULL ) + return; + dd = p->dd; + Llb_NonlinFree( p ); + if ( dd->bFunc ) + Cudd_RecursiveDeref( dd, dd->bFunc ); + Extra_StopManager( dd ); +// Cudd_Quit ( dd ); + p = NULL; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/llb/llb3Nonlin.c b/src/aig/llb/llb3Nonlin.c index c10db9e3..1cdd2c96 100644 --- a/src/aig/llb/llb3Nonlin.c +++ b/src/aig/llb/llb3Nonlin.c @@ -42,13 +42,18 @@ struct Llb_Mnn_t_ Vec_Ptr_t * vLeaves; Vec_Ptr_t * vRoots; int * pVars2Q; - int * pOrder; + int * pOrderL; + int * pOrderL2; + int * pOrderG; Vec_Int_t * vCs2Glo; // cur state variables into global variables Vec_Int_t * vNs2Glo; // next state variables into global variables Vec_Int_t * vGlo2Cs; // global variables into cur state variables Vec_Int_t * vGlo2Ns; // global variables into next state variables + int ddLocReos; + int ddLocGrbs; + int timeImage; int timeTran1; int timeTran2; @@ -297,7 +302,7 @@ Abc_Cex_t * Llb_NonlinDeriveCex( Llb_Mnn_t * p ) //Extra_bddPrintSupport( p->dd, bRing ); printf( "\n" ); // compute the next states bImage = Llb_NonlinImage( p->pAig, p->vLeaves, p->vRoots, p->pVars2Q, p->dd, bState, - p->pPars->fReorder, p->pPars->fVeryVerbose, p->pOrder, ABC_INFINITY, ABC_INFINITY ); // consumed reference + p->pPars->fReorder, p->pPars->fVeryVerbose, NULL, ABC_INFINITY, ABC_INFINITY ); // consumed reference assert( bImage != NULL ); Cudd_Ref( bImage ); //Extra_bddPrintSupport( p->dd, bImage ); printf( "\n" ); @@ -382,6 +387,33 @@ int Llb_NonlinReoHook( DdManager * dd, char * Type, void * Method ) return 1; } +/**Function************************************************************* + + Synopsis [Perform reachability with hints.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Llb_NonlinCompPerms( DdManager * dd, int * pVar2Lev ) +{ + DdSubtable * pSubt; + int i, Sum = 0, Entry; + for ( i = 0; i < dd->size; i++ ) + { + pSubt = &(dd->subtables[dd->perm[i]]); + if ( pSubt->keys == pSubt->dead + 1 ) + continue; + Entry = ABC_MAX(dd->perm[i], pVar2Lev[i]) - ABC_MIN(dd->perm[i], pVar2Lev[i]); + Sum += Entry; +//printf( "%d-%d(%d) ", dd->perm[i], pV2L[i], Entry ); + } + return Sum; +} + /**Function************************************************************* Synopsis [Perform reachability with hints.] @@ -395,8 +427,8 @@ int Llb_NonlinReoHook( DdManager * dd, char * Type, void * Method ) ***********************************************************************/ int Llb_NonlinReachability( Llb_Mnn_t * p ) { - DdNode * bCurrent, * bNext, * bTemp; - int iVar, nIters, nBddSize0, nBddSize, Limit = p->pPars->nBddMax; + DdNode * bTemp, * bNext; + int nIters, nBddSize0, nBddSize, NumCmp, Limit = p->pPars->nBddMax; int clk2, clk3, clk = clock(); assert( Aig_ManRegNum(p->pAig) > 0 ); @@ -425,7 +457,9 @@ int Llb_NonlinReachability( Llb_Mnn_t * p ) } Cudd_Ref( p->ddR->bFunc ); // compute the starting set of states - bCurrent = Llb_NonlinComputeInitState( p->pAig, p->dd ); Cudd_Ref( bCurrent ); + Cudd_Quit( p->dd ); + p->dd = Llb_NonlinImageStart( p->pAig, p->vLeaves, p->vRoots, p->pVars2Q, p->pOrderL, 1 ); + p->dd->bFunc = Llb_NonlinComputeInitState( p->pAig, p->dd ); Cudd_Ref( p->dd->bFunc ); // current p->ddG->bFunc = Llb_NonlinComputeInitState( p->pAig, p->ddG ); Cudd_Ref( p->ddG->bFunc ); // reached p->ddG->bFunc2 = Llb_NonlinComputeInitState( p->pAig, p->ddG ); Cudd_Ref( p->ddG->bFunc2 ); // frontier for ( nIters = 0; nIters < p->pPars->nIterMax; nIters++ ) @@ -437,18 +471,18 @@ int Llb_NonlinReachability( Llb_Mnn_t * p ) 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; + Llb_NonlinImageQuit(); return -1; } // save the onion ring - bTemp = Extra_TransferPermute( p->dd, p->ddR, bCurrent, Vec_IntArray(p->vCs2Glo) ); + bTemp = Extra_TransferPermute( p->dd, p->ddR, p->dd->bFunc, 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; + Llb_NonlinImageQuit(); return -1; } Cudd_Ref( bTemp ); @@ -460,7 +494,6 @@ int Llb_NonlinReachability( Llb_Mnn_t * p ) assert( p->pInit->pSeqModel == NULL ); if ( !p->pPars->fBackward ) p->pInit->pSeqModel = Llb_NonlinDeriveCex( p ); - Cudd_RecursiveDeref( p->dd, bCurrent ); bCurrent = NULL; if ( !p->pPars->fSilent ) { if ( !p->pPars->fBackward ) @@ -469,85 +502,32 @@ int Llb_NonlinReachability( Llb_Mnn_t * p ) printf( "Output ??? was asserted in frame %d (counter-example is not produced). ", nIters ); Abc_PrintTime( 1, "Time", clock() - clk ); } + Llb_NonlinImageQuit(); return 0; } - // check the size - if ( Cudd_DagSize(bCurrent) > p->pPars->nBddMax ) - { - DdNode * bVar, * bVarG; - - // find the best variable - iVar = Llb_NonlinFindBestVar( p->dd, bCurrent, p->pAig ); - - // get cofactor in the working manager - bVar = Cudd_bddIthVar( p->dd, Aig_ObjId(Saig_ManLo(p->pAig,iVar)) ); - bCurrent = Cudd_bddAnd( p->dd, bTemp = bCurrent, Cudd_Not(bVar) ); Cudd_Ref( bCurrent ); - Cudd_RecursiveDeref( p->dd, bTemp ); - - // get cofactor in the global manager - bVarG = Cudd_bddIthVar(p->ddG, iVar); - p->ddG->bFunc2 = Cudd_bddAnd( p->ddG, bTemp = p->ddG->bFunc2, Cudd_Not(bVarG) ); Cudd_Ref( p->ddG->bFunc2 ); - Cudd_RecursiveDeref( p->ddG, bTemp ); - } - // compute the next states clk3 = clock(); - nBddSize0 = Cudd_DagSize( bCurrent ); - bNext = Llb_NonlinImage( p->pAig, p->vLeaves, p->vRoots, p->pVars2Q, p->dd, bCurrent, -// p->pPars->fReorder, p->pPars->fVeryVerbose, p->pOrder, nIters ? p->pPars->nBddMax : ABC_INFINITY ); - p->pPars->fReorder, p->pPars->fVeryVerbose, p->pOrder, ABC_INFINITY, p->pPars->TimeTarget ); -// Abc_PrintTime( 1, "Image time", clock() - clk3 ); + nBddSize0 = Cudd_DagSize( p->dd->bFunc ); + bNext = Llb_NonlinImageCompute( p->dd->bFunc, p->pPars->fReorder, 0, 1, p->pOrderL ); // consumes ref +// bNext = Llb_NonlinImage( p->pAig, p->vLeaves, p->vRoots, p->pVars2Q, p->dd, bCurrent, +// p->pPars->fReorder, p->pPars->fVeryVerbose, NULL, ABC_INFINITY, p->pPars->TimeTarget ); if ( bNext == NULL ) { if ( !p->pPars->fSilent ) printf( "Reached timeout (%d seconds) during image computation in quantification.\n", p->pPars->TimeLimit ); p->pPars->iFrame = nIters - 1; - Cudd_RecursiveDeref( p->dd, bCurrent ); bCurrent = NULL; + Llb_NonlinImageQuit(); return -1; } - if ( bNext == NULL ) // Llb_NonlimImage() consumes reference of bCurrent!!! - { - DdNode * bVar, * bVarG; -// if ( !p->pPars->fSilent ) -// printf( "Reached timeout during image computation (%d seconds).\n", p->pPars->TimeLimit ); -// p->pPars->iFrame = nIters - 1; -// return -1; - - printf( "Should never happen!\n" ); - - // get the frontier in the working manager - bCurrent = Extra_TransferPermute( p->ddG, p->dd, p->ddG->bFunc2, Vec_IntArray(p->vGlo2Cs) ); Cudd_Ref( bCurrent ); - - // find the best variable - iVar = Llb_NonlinFindBestVar( p->dd, bCurrent, p->pAig ); - - // get cofactor in the working manager - bVar = Cudd_bddIthVar( p->dd, Aig_ObjId(Saig_ManLo(p->pAig,iVar)) ); - bCurrent = Cudd_bddAnd( p->dd, bTemp = bCurrent, Cudd_Not(bVar) ); Cudd_Ref( bCurrent ); - Cudd_RecursiveDeref( p->dd, bTemp ); - - // get cofactor in the global manager - bVarG = Cudd_bddIthVar(p->dd, iVar); - p->ddG->bFunc2 = Cudd_bddAnd( p->ddG, bTemp = p->ddG->bFunc2, Cudd_Not(bVarG) ); Cudd_Ref( p->ddG->bFunc2 ); - Cudd_RecursiveDeref( p->ddG, bTemp ); - -// Cudd_ReduceHeap( p->dd, CUDD_REORDER_SIFT, 1 ); - p->pPars->nBddMax = ABC_INFINITY; - nIters--; - continue; - } - else - p->pPars->nBddMax = Limit; - Cudd_Ref( bNext ); nBddSize = Cudd_DagSize( bNext ); p->timeImage += clock() - clk3; + // 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_TransferPermute( p->dd, p->ddG, bNext, Vec_IntArray(p->vNs2Glo) ); if ( p->ddG->bFunc2 == NULL ) { @@ -555,12 +535,24 @@ int Llb_NonlinReachability( Llb_Mnn_t * p ) printf( "Reached timeout (%d seconds) during image computation in transfer 1.\n", p->pPars->TimeLimit ); p->pPars->iFrame = nIters - 1; Cudd_RecursiveDeref( p->dd, bNext ); + Llb_NonlinImageQuit(); return -1; } Cudd_Ref( p->ddG->bFunc2 ); Cudd_RecursiveDeref( p->dd, bNext ); p->timeTran1 += clock() - clk3; + // save permutation + NumCmp = Llb_NonlinCompPerms( p->dd, p->pOrderL2 ); + // save order before image computation + memcpy( p->pOrderL2, p->dd->perm, sizeof(int) * p->dd->size ); + // update the image computation manager + p->timeReo += Cudd_ReadReorderingTime(p->dd); + p->ddLocReos += Cudd_ReadReorderings(p->dd); + p->ddLocGrbs += Cudd_ReadGarbageCollections(p->dd); + Llb_NonlinImageQuit(); + p->dd = Llb_NonlinImageStart( p->pAig, p->vLeaves, p->vRoots, p->pVars2Q, p->pOrderL, 0 ); + // derive new states clk3 = clock(); p->ddG->bFunc2 = Cudd_bddAnd( p->ddG, bTemp = p->ddG->bFunc2, Cudd_Not(p->ddG->bFunc) ); @@ -570,6 +562,7 @@ int Llb_NonlinReachability( Llb_Mnn_t * p ) 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 ); + Llb_NonlinImageQuit(); return -1; } Cudd_Ref( p->ddG->bFunc2 ); @@ -584,6 +577,7 @@ int Llb_NonlinReachability( Llb_Mnn_t * p ) 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 ); + Llb_NonlinImageQuit(); return -1; } Cudd_Ref( p->ddG->bFunc ); @@ -593,20 +587,20 @@ int Llb_NonlinReachability( Llb_Mnn_t * p ) // reset permutation // RetValue = Cudd_CheckZeroRef( dd ); // assert( RetValue == 0 ); -// Cudd_ShuffleHeap( dd, pOrder ); +// Cudd_ShuffleHeap( dd, pOrderG ); // 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_TransferPermute( p->ddG, p->dd, p->ddG->bFunc2, Vec_IntArray(p->vGlo2Cs) ); - if ( bCurrent == NULL ) + p->dd->bFunc = Extra_TransferPermute( p->ddG, p->dd, p->ddG->bFunc2, Vec_IntArray(p->vGlo2Cs) ); + if ( p->dd->bFunc == 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; + Llb_NonlinImageQuit(); return -1; } - Cudd_Ref( bCurrent ); + Cudd_Ref( p->dd->bFunc ); p->timeTran2 += clock() - clk3; // report the results @@ -615,11 +609,14 @@ int Llb_NonlinReachability( Llb_Mnn_t * p ) printf( "I =%3d : ", nIters ); printf( "Fr =%7d ", nBddSize0 ); printf( "Im =%7d ", nBddSize ); - printf( "(%4d %4d) ", Cudd_ReadReorderings(p->dd), Cudd_ReadGarbageCollections(p->dd) ); + printf( "(%4d %4d) ", p->ddLocReos, p->ddLocGrbs ); printf( "Rea =%6d ", Cudd_DagSize(p->ddG->bFunc) ); printf( "(%4d %4d) ", Cudd_ReadReorderings(p->ddG), Cudd_ReadGarbageCollections(p->ddG) ); printf( "S =%4d ", nSuppMax ); + printf( "cL =%5d ", NumCmp ); + printf( "cG =%5d ", Llb_NonlinCompPerms( p->ddG, p->pOrderG ) ); Abc_PrintTime( 1, "T", clock() - clk2 ); + memcpy( p->pOrderG, p->ddG->perm, sizeof(int) * p->ddG->size ); } /* if ( pPars->fVerbose ) @@ -630,18 +627,16 @@ int Llb_NonlinReachability( Llb_Mnn_t * p ) fflush( stdout ); } */ - if ( nIters == p->pPars->nIterMax - 1 ) { if ( !p->pPars->fSilent ) printf( "Reached limit on the number of timeframes (%d).\n", p->pPars->nIterMax ); p->pPars->iFrame = nIters; - Cudd_RecursiveDeref( p->dd, bCurrent ); bCurrent = NULL; + Llb_NonlinImageQuit(); return -1; } -// Llb_NonlinReorder( p->ddG, 1 ); -// Llb_NonlinFindBestVar( p->ddG, bReached, NULL ); } + Llb_NonlinImageQuit(); // report the stats if ( p->pPars->fVerbose ) @@ -704,10 +699,14 @@ Llb_Mnn_t * Llb_MnnStart( Aig_Man_t * pInit, Aig_Man_t * pAig, Gia_ParLlb_t * p Saig_ManForEachLi( pAig, pObj, i ) Vec_PtrPush( p->vRoots, pObj ); // variables to quantify - p->pOrder = ABC_CALLOC( int, Aig_ManObjNumMax(pAig) ); + p->pOrderL = ABC_CALLOC( int, Aig_ManObjNumMax(pAig) ); + p->pOrderL2= ABC_CALLOC( int, Aig_ManObjNumMax(pAig) ); + p->pOrderG = ABC_CALLOC( int, Aig_ManObjNumMax(pAig) ); p->pVars2Q = ABC_CALLOC( int, Aig_ManObjNumMax(pAig) ); Aig_ManForEachPi( pAig, pObj, i ) p->pVars2Q[Aig_ObjId(pObj)] = 1; + for ( i = 0; i < Aig_ManObjNumMax(pAig); i++ ) + p->pOrderL[i] = p->pOrderL2[i] = p->pOrderG[i] = i; Llb_NonlinPrepareVarMap( p ); return p; } @@ -730,7 +729,6 @@ void Llb_MnnStop( Llb_Mnn_t * p ) if ( p->pPars->fVerbose ) { p->timeOther = p->timeTotal - p->timeImage - p->timeTran1 - p->timeTran2 - p->timeGloba; - p->timeReo = Cudd_ReadReorderingTime(p->dd); p->timeReoG = Cudd_ReadReorderingTime(p->ddG); ABC_PRTP( "Image ", p->timeImage, p->timeTotal ); ABC_PRTP( " build ", timeBuild, p->timeTotal ); @@ -744,7 +742,6 @@ void Llb_MnnStop( Llb_Mnn_t * p ) ABC_PRTP( " reo ", p->timeReo, p->timeTotal ); ABC_PRTP( " reoG ", p->timeReoG, p->timeTotal ); } - p->dd->bFunc = NULL; if ( p->ddR->bFunc ) Cudd_RecursiveDeref( p->ddR, p->ddR->bFunc ); Vec_PtrForEachEntry( DdNode *, p->vRings, bTemp, i ) @@ -755,7 +752,7 @@ void Llb_MnnStop( Llb_Mnn_t * p ) if ( p->ddG->bFunc2 ) Cudd_RecursiveDeref( p->ddG, p->ddG->bFunc2 ); // printf( "manager1\n" ); - Extra_StopManager( p->dd ); +// Extra_StopManager( p->dd ); // printf( "manager2\n" ); Extra_StopManager( p->ddG ); // printf( "manager3\n" ); @@ -767,7 +764,9 @@ void Llb_MnnStop( Llb_Mnn_t * p ) Vec_PtrFree( p->vLeaves ); Vec_PtrFree( p->vRoots ); ABC_FREE( p->pVars2Q ); - ABC_FREE( p->pOrder ); + ABC_FREE( p->pOrderL ); + ABC_FREE( p->pOrderL2 ); + ABC_FREE( p->pOrderG ); ABC_FREE( p ); } diff --git a/src/aig/llb/llbInt.h b/src/aig/llb/llbInt.h index 6bca2adb..dd938436 100644 --- a/src/aig/llb/llbInt.h +++ b/src/aig/llb/llbInt.h @@ -172,9 +172,15 @@ extern DdNode * Llb_ImgComputeImage( Aig_Man_t * pAig, Vec_Ptr_t * vDdMan Vec_Ptr_t * vQuant0, Vec_Ptr_t * vQuant1, Vec_Int_t * vDriRefs, int TimeTarget, int fBackward, int fReorder, int fVerbose ); +extern DdManager * Llb_NonlinImageStart( Aig_Man_t * pAig, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vRoots, int * pVars2Q, int * pOrder, int fFirst ); +extern DdNode * Llb_NonlinImageCompute( DdNode * bCurrent, int fReorder, int fDrop, int fVerbose, int * pOrder ); +extern void Llb_NonlinImageQuit(); + /*=== 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 TimeTarget ); +/*=== llb3Nonlin.c ======================================================*/ +extern DdNode * Llb_NonlinComputeInitState( Aig_Man_t * pAig, DdManager * dd ); ABC_NAMESPACE_HEADER_END diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 9890dbcf..c055c3ad 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -27937,7 +27937,7 @@ usage: Abc_Print( -2, "\t-F num : max number of reachability iterations [default = %d]\n", pPars->nIterMax ); Abc_Print( -2, "\t-T num : approximate time limit in seconds (0=infinite) [default = %d]\n", pPars->TimeLimit ); Abc_Print( -2, "\t-L file: the log file name [default = %s]\n", pLogFileName ? pLogFileName : "no logging" ); - Abc_Print( -2, "\t-r : enable dynamic BDD variable reordering [default = %s]\n", pPars->fReorder? "yes": "no" ); + Abc_Print( -2, "\t-r : enable additional BDD var reordering before image [default = %s]\n", pPars->fReorder? "yes": "no" ); Abc_Print( -2, "\t-b : perform backward reachability analysis [default = %s]\n", pPars->fBackward? "yes": "no" ); Abc_Print( -2, "\t-y : skip checking property outputs [default = %s]\n", pPars->fSkipOutCheck? "yes": "no" ); Abc_Print( -2, "\t-z : skip reachability (run preparation phase only) [default = %s]\n", pPars->fSkipReach? "yes": "no" ); @@ -28069,7 +28069,7 @@ usage: Abc_Print( -2, "\t-F num : max number of reachability iterations [default = %d]\n", pPars->nIterMax ); Abc_Print( -2, "\t-T num : approximate time limit in seconds (0=infinite) [default = %d]\n", pPars->TimeLimit ); Abc_Print( -2, "\t-L file: the log file name [default = %s]\n", pLogFileName ? pLogFileName : "no logging" ); - Abc_Print( -2, "\t-r : enable dynamic BDD variable reordering [default = %s]\n", pPars->fReorder? "yes": "no" ); + Abc_Print( -2, "\t-r : enable additional BDD var reordering before image [default = %s]\n", pPars->fReorder? "yes": "no" ); Abc_Print( -2, "\t-y : skip checking property outputs [default = %s]\n", pPars->fSkipOutCheck? "yes": "no" ); Abc_Print( -2, "\t-z : skip reachability (run preparation phase only) [default = %s]\n", pPars->fSkipReach? "yes": "no" ); Abc_Print( -2, "\t-v : prints verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" ); -- cgit v1.2.3