diff options
Diffstat (limited to 'src/misc/extra')
| -rw-r--r-- | src/misc/extra/extra.h | 3 | ||||
| -rw-r--r-- | src/misc/extra/extraBddMisc.c | 199 |
2 files changed, 202 insertions, 0 deletions
diff --git a/src/misc/extra/extra.h b/src/misc/extra/extra.h index dd0edb44..3598b69f 100644 --- a/src/misc/extra/extra.h +++ b/src/misc/extra/extra.h @@ -198,6 +198,9 @@ extern void Extra_bddPermuteArray( DdManager * dd, DdNode ** bNodesIn, D extern DdNode * Extra_bddComputeCube( DdManager * dd, DdNode ** bXVars, int nVars ); 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 ); #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 11c7d959..82b9f649 100644 --- a/src/misc/extra/extraBddMisc.c +++ b/src/misc/extra/extraBddMisc.c @@ -1039,6 +1039,63 @@ DdNode * Extra_bddChangePolarity( } /* end of Extra_bddChangePolarity */ +/**Function************************************************************* + + Synopsis [Checks if the given variable belongs to the cube.] + + Description [Return -1 if the var does not appear in the cube. + Otherwise, returns polarity (0 or 1) of the var in the cube.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Extra_bddVarIsInCube( DdNode * bCube, int iVar ) +{ + DdNode * bCube0, * bCube1; + while ( Cudd_Regular(bCube)->index != CUDD_CONST_INDEX ) + { + bCube0 = Cudd_NotCond( cuddE(Cudd_Regular(bCube)), Cudd_IsComplement(bCube) ); + bCube1 = Cudd_NotCond( cuddT(Cudd_Regular(bCube)), Cudd_IsComplement(bCube) ); + // make sure it is a cube + assert( (Cudd_IsComplement(bCube0) && Cudd_Regular(bCube0)->index == CUDD_CONST_INDEX) || // bCube0 == 0 + (Cudd_IsComplement(bCube1) && Cudd_Regular(bCube1)->index == CUDD_CONST_INDEX) ); // bCube1 == 0 + // quit if it is the last one + if ( Cudd_Regular(bCube)->index == iVar ) + return (int)(Cudd_IsComplement(bCube0) && Cudd_Regular(bCube0)->index == CUDD_CONST_INDEX); + // get the next cube + if ( (Cudd_IsComplement(bCube0) && Cudd_Regular(bCube0)->index == CUDD_CONST_INDEX) ) + bCube = bCube1; + else + bCube = bCube0; + } + return -1; +} + +/**Function************************************************************* + + Synopsis [Computes the AND of two BDD with different orders.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +DdNode * Extra_bddAndPerm( DdManager * ddF, DdNode * bF, DdManager * ddG, DdNode * bG ) +{ + DdNode * bRes; + do + { + ddF->reordered = 0; + bRes = extraBddAndPerm( ddF, bF, ddG, bG ); + } + while ( ddF->reordered == 1 ); + return ( bRes ); +} + /*---------------------------------------------------------------------------*/ /* Definition of internal functions */ /*---------------------------------------------------------------------------*/ @@ -1805,6 +1862,148 @@ DdNode * extraBddChangePolarity( } /* end of extraBddChangePolarity */ + +static int Counter = 0; + +/**Function************************************************************* + + Synopsis [Computes the AND of two BDD with different orders.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +DdNode * extraBddAndPerm( DdManager * ddF, DdNode * bF, DdManager * ddG, DdNode * bG ) +{ + DdNode * bF0, * bF1, * bG0, * bG1, * bRes0, * bRes1, * bRes, * bVar; + int LevF, LevG, Lev; + + // if F == 0, return 0 + if ( bF == Cudd_Not(ddF->one) ) + return Cudd_Not(ddF->one); + // if G == 0, return 0 + if ( bG == Cudd_Not(ddG->one) ) + return Cudd_Not(ddF->one); + // if G == 1, return F + if ( bG == ddG->one ) + return bF; + // 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)) ) + return bRes; + Counter++; + + // 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 ); + Lev = ABC_MIN( LevF, LevG ); + assert( Lev < ddF->size ); + bVar = ddF->vars[ddF->invperm[Lev]]; + + // cofactor + bF0 = (Lev < LevF) ? bF : Cudd_NotCond( cuddE(Cudd_Regular(bF)), Cudd_IsComplement(bF) ); + bF1 = (Lev < LevF) ? bF : Cudd_NotCond( cuddT(Cudd_Regular(bF)), Cudd_IsComplement(bF) ); + bG0 = (Lev < LevG) ? bG : Cudd_NotCond( cuddE(Cudd_Regular(bG)), Cudd_IsComplement(bG) ); + bG1 = (Lev < LevG) ? bG : Cudd_NotCond( cuddT(Cudd_Regular(bG)), Cudd_IsComplement(bG) ); + + // call for cofactors + bRes0 = extraBddAndPerm( ddF, bF0, ddG, bG0 ); + if ( bRes0 == NULL ) + return NULL; + cuddRef( bRes0 ); + // call for cofactors + bRes1 = extraBddAndPerm( ddF, bF1, ddG, bG1 ); + if ( bRes1 == NULL ) + { + Cudd_IterDerefBdd( ddF, bRes0 ); + return NULL; + } + cuddRef( bRes1 ); + + // compose the result + bRes = cuddBddIteRecur( ddF, bVar, bRes1, bRes0 ); + if ( bRes == NULL ) + { + Cudd_IterDerefBdd( ddF, bRes0 ); + Cudd_IterDerefBdd( ddF, bRes1 ); + } + 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 ); + cuddDeref( bRes ); + return bRes; +} + +/**Function************************************************************* + + Synopsis [Testbench.] + + Description [This procedure takes BDD manager ddF and two BDDs + in this manager (bF and bG). It creates a new manager ddG, + transfers bG into it and then reorders it, resulting in bG2. + Then it tries to compute the product of bF and bG2 in ddF.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Extra_TestAndPerm( DdManager * ddF, DdNode * bF, DdNode * bG ) +{ + DdManager * ddG; + DdNode * bG2, * bRes1, * bRes2; + int clk; + // disable variable ordering in ddF + Cudd_AutodynDisable( ddF ); + + // create new BDD manager + ddG = Cudd_Init( ddF->size, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 ); + // transfer BDD into it + Cudd_ShuffleHeap( ddG, ddF->invperm ); + bG2 = Extra_TransferLevelByLevel( ddF, ddG, bG ); Cudd_Ref( bG2 ); + // reorder the new manager + Cudd_ReduceHeap( ddG, CUDD_REORDER_SYMM_SIFT, 1 ); + + // compute the result +clk = clock(); + bRes1 = Cudd_bddAnd( ddF, bF, bG ); Cudd_Ref( bRes1 ); +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 ); +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 ", + Cudd_DagSize(bF), Cudd_DagSize(bG), Cudd_DagSize(bRes2), + Cudd_DagSize(bF) * Cudd_DagSize(bG) ); + + if ( bRes1 == bRes2 ) + printf( "Result verified.\n\n" ); + else + printf( "Result is incorrect.\n\n" ); + + Cudd_RecursiveDeref( ddF, bRes1 ); + Cudd_RecursiveDeref( ddF, bRes2 ); + // quit the new manager + Cudd_RecursiveDeref( ddG, bG2 ); + Extra_StopManager( ddG ); + + // re-enable variable ordering in ddF + Cudd_AutodynEnable( ddF, CUDD_REORDER_SYMM_SIFT ); +} + + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// |