From badbb5a6cc8a794bfd7c5adef62b0d6c2e583e42 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sat, 5 Mar 2011 16:17:12 -0800 Subject: Fixing bugs in the new procedures added to the library. --- src/aig/llb/llb3Nonlin.c | 5 +++++ src/misc/extra/extra.h | 3 +-- src/misc/extra/extraBddMisc.c | 52 +++++++++++++++++++++++++++++++------------ 3 files changed, 44 insertions(+), 16 deletions(-) diff --git a/src/aig/llb/llb3Nonlin.c b/src/aig/llb/llb3Nonlin.c index 1cdd2c96..6a0c871e 100644 --- a/src/aig/llb/llb3Nonlin.c +++ b/src/aig/llb/llb3Nonlin.c @@ -529,6 +529,7 @@ int Llb_NonlinReachability( Llb_Mnn_t * p ) clk3 = clock(); Cudd_RecursiveDeref( p->ddG, p->ddG->bFunc2 ); p->ddG->bFunc2 = Extra_TransferPermute( p->dd, p->ddG, bNext, Vec_IntArray(p->vNs2Glo) ); +// p->ddG->bFunc2 = Extra_bddAndPermute( p->ddG, Cudd_Not(p->ddG->bFunc), p->dd, bNext, Vec_IntArray(p->vNs2Glo) ); if ( p->ddG->bFunc2 == NULL ) { if ( !p->pPars->fSilent ) @@ -552,6 +553,7 @@ int Llb_NonlinReachability( Llb_Mnn_t * p ) p->ddLocGrbs += Cudd_ReadGarbageCollections(p->dd); Llb_NonlinImageQuit(); p->dd = Llb_NonlinImageStart( p->pAig, p->vLeaves, p->vRoots, p->pVars2Q, p->pOrderL, 0 ); + //Extra_TestAndPerm( p->ddG, Cudd_Not(p->ddG->bFunc), p->ddG->bFunc2 ); // derive new states clk3 = clock(); @@ -567,9 +569,12 @@ int Llb_NonlinReachability( Llb_Mnn_t * p ) } Cudd_Ref( p->ddG->bFunc2 ); Cudd_RecursiveDeref( p->ddG, bTemp ); + p->timeGloba += clock() - clk3; + if ( Cudd_IsConstant(p->ddG->bFunc2) ) break; // add to the reached set + clk3 = clock(); p->ddG->bFunc = Cudd_bddOr( p->ddG, bTemp = p->ddG->bFunc, p->ddG->bFunc2 ); if ( p->ddG->bFunc == NULL ) { diff --git a/src/misc/extra/extra.h b/src/misc/extra/extra.h index 3598b69f..693c25bd 100644 --- a/src/misc/extra/extra.h +++ b/src/misc/extra/extra.h @@ -199,8 +199,7 @@ extern DdNode * Extra_bddComputeCube( DdManager * dd, DdNode ** bXVars, int extern DdNode * Extra_bddChangePolarity( DdManager * dd, DdNode * bFunc, DdNode * bVars ); extern DdNode * extraBddChangePolarity( DdManager * dd, DdNode * bFunc, DdNode * bVars ); extern int Extra_bddVarIsInCube( DdNode * bCube, int iVar ); -extern DdNode * Extra_bddAndPerm( DdManager * ddF, DdNode * bF, DdManager * ddG, DdNode * bG ); -extern DdNode * extraBddAndPerm( DdManager * ddF, DdNode * bF, DdManager * ddG, DdNode * bG ); +extern DdNode * Extra_bddAndPermute( DdManager * ddF, DdNode * bF, DdManager * ddG, DdNode * bG, int * pPermute ); #ifndef ABC_PRB #define ABC_PRB(dd,f) printf("%s = ", #f); Extra_bddPrint(dd,f); printf("\n") diff --git a/src/misc/extra/extraBddMisc.c b/src/misc/extra/extraBddMisc.c index 82b9f649..7d63980a 100644 --- a/src/misc/extra/extraBddMisc.c +++ b/src/misc/extra/extraBddMisc.c @@ -55,6 +55,8 @@ static DdNode * extraTransferPermuteRecur( DdManager * ddS, DdManager * ddD, DdN static DdNode * extraTransferPermute( DdManager * ddS, DdManager * ddD, DdNode * f, int * Permute ); static DdNode * cuddBddPermuteRecur ARGS( ( DdManager * manager, DdHashTable * table, DdNode * node, int *permut ) ); +static DdNode * extraBddAndPermute( DdHashTable * table, DdManager * ddF, DdNode * bF, DdManager * ddG, DdNode * bG, int * pPermute ); + // file "cuddUtils.c" static void ddSupportStep(DdNode *f, int *support); static void ddClearFlag(DdNode *f); @@ -1072,27 +1074,39 @@ int Extra_bddVarIsInCube( DdNode * bCube, int iVar ) } return -1; } - + /**Function************************************************************* Synopsis [Computes the AND of two BDD with different orders.] - Description [] + Description [Derives the result of Boolean AND of bF and bG in ddF. + The array pPermute gives the mapping of variables of ddG into that of ddF.] SideEffects [] SeeAlso [] ***********************************************************************/ -DdNode * Extra_bddAndPerm( DdManager * ddF, DdNode * bF, DdManager * ddG, DdNode * bG ) +DdNode * Extra_bddAndPermute( DdManager * ddF, DdNode * bF, DdManager * ddG, DdNode * bG, int * pPermute ) { + DdHashTable * table; DdNode * bRes; do { ddF->reordered = 0; - bRes = extraBddAndPerm( ddF, bF, ddG, bG ); + table = cuddHashTableInit( ddF, 2, 256 ); + if (table == NULL) return NULL; + bRes = extraBddAndPermute( table, ddF, bF, ddG, bG, pPermute ); + if ( bRes ) cuddRef( bRes ); + cuddHashTableQuit( table ); + if ( bRes ) cuddDeref( bRes ); +//if ( ddF->reordered == 1 ) +//printf( "Reordering happened\n" ); } while ( ddF->reordered == 1 ); +//printf( "|F| =%6d |G| =%6d |H| =%6d |F|*|G| =%9d\n", +// Cudd_DagSize(bF), Cudd_DagSize(bG), Cudd_DagSize(bRes), +// Cudd_DagSize(bF) * Cudd_DagSize(bG) ); return ( bRes ); } @@ -1876,7 +1890,7 @@ static int Counter = 0; SeeAlso [] ***********************************************************************/ -DdNode * extraBddAndPerm( DdManager * ddF, DdNode * bF, DdManager * ddG, DdNode * bG ) +DdNode * extraBddAndPermute( DdHashTable * table, DdManager * ddF, DdNode * bF, DdManager * ddG, DdNode * bG, int * pPermute ) { DdNode * bF0, * bF1, * bG0, * bG1, * bRes0, * bRes1, * bRes, * bVar; int LevF, LevG, Lev; @@ -1893,14 +1907,19 @@ DdNode * extraBddAndPerm( DdManager * ddF, DdNode * bF, DdManager * ddG, DdNode // cannot use F == 1, because the var order of G has to be changed // check cache - if ( (Cudd_Regular(bF)->ref != 1 || Cudd_Regular(bG)->ref != 1) && - (bRes = cuddCacheLookup2(ddF, (DD_CTFP)extraBddAndPerm, bF, bG)) ) + if ( //(Cudd_Regular(bF)->ref != 1 || Cudd_Regular(bG)->ref != 1) && + (bRes = cuddHashTableLookup2(table, bF, bG)) ) return bRes; Counter++; + if ( ddF->TimeStop && ddF->TimeStop < clock() ) + return NULL; + if ( ddG->TimeStop && ddG->TimeStop < clock() ) + return NULL; + // find the topmost variable in F and G using var order of F LevF = cuddI( ddF, Cudd_Regular(bF)->index ); - LevG = cuddI( ddF, Cudd_Regular(bG)->index ); + LevG = cuddI( ddF, pPermute ? pPermute[Cudd_Regular(bG)->index] : Cudd_Regular(bG)->index ); Lev = ABC_MIN( LevF, LevG ); assert( Lev < ddF->size ); bVar = ddF->vars[ddF->invperm[Lev]]; @@ -1912,12 +1931,12 @@ DdNode * extraBddAndPerm( DdManager * ddF, DdNode * bF, DdManager * ddG, DdNode bG1 = (Lev < LevG) ? bG : Cudd_NotCond( cuddT(Cudd_Regular(bG)), Cudd_IsComplement(bG) ); // call for cofactors - bRes0 = extraBddAndPerm( ddF, bF0, ddG, bG0 ); + bRes0 = extraBddAndPermute( table, ddF, bF0, ddG, bG0, pPermute ); if ( bRes0 == NULL ) return NULL; cuddRef( bRes0 ); // call for cofactors - bRes1 = extraBddAndPerm( ddF, bF1, ddG, bG1 ); + bRes1 = extraBddAndPermute( table, ddF, bF1, ddG, bG1, pPermute ); if ( bRes1 == NULL ) { Cudd_IterDerefBdd( ddF, bRes0 ); @@ -1931,17 +1950,22 @@ DdNode * extraBddAndPerm( DdManager * ddF, DdNode * bF, DdManager * ddG, DdNode { Cudd_IterDerefBdd( ddF, bRes0 ); Cudd_IterDerefBdd( ddF, bRes1 ); + return NULL; } cuddRef( bRes ); Cudd_IterDerefBdd( ddF, bRes0 ); Cudd_IterDerefBdd( ddF, bRes1 ); // cache the result - if ( Cudd_Regular(bF)->ref != 1 || Cudd_Regular(bG)->ref != 1 ) - cuddCacheInsert2( ddF, (DD_CTFP)extraBddAndPerm, bF, bG, bRes ); +// if ( Cudd_Regular(bF)->ref != 1 || Cudd_Regular(bG)->ref != 1 ) + { + ptrint fanout = (ptrint)Cudd_Regular(bF)->ref * Cudd_Regular(bG)->ref; + cuddSatDec(fanout); + cuddHashTableInsert2( table, bF, bG, bRes, fanout ); + } cuddDeref( bRes ); return bRes; -} +} /**Function************************************************************* @@ -1981,7 +2005,7 @@ Abc_PrintTime( 1, "Runtime of Cudd_bddAnd ", clock() - clk ); // compute the result Counter = 0; clk = clock(); - bRes2 = Extra_bddAndPerm( ddF, bF, ddG, bG2 ); Cudd_Ref( bRes2 ); + bRes2 = Extra_bddAndPermute( ddF, bF, ddG, bG2, NULL ); Cudd_Ref( bRes2 ); Abc_PrintTime( 1, "Runtime of new procedure", clock() - clk ); printf( "Recursive calls = %d\n", Counter ); printf( "|F| =%6d |G| =%6d |H| =%6d |F|*|G| =%9d ", -- cgit v1.2.3