From 1256abca718aa24c036b8a59324bd3c33c7d3954 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sun, 29 Jul 2018 22:39:27 -0800 Subject: Adding procedure to compute tuples of k out of n as a BDD. --- src/bdd/extrab/extraBdd.h | 4 ++ src/bdd/extrab/extraBddMisc.c | 157 ++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 161 insertions(+) (limited to 'src') diff --git a/src/bdd/extrab/extraBdd.h b/src/bdd/extrab/extraBdd.h index 3dbc6264..e7a65a94 100644 --- a/src/bdd/extrab/extraBdd.h +++ b/src/bdd/extrab/extraBdd.h @@ -198,6 +198,10 @@ extern DdNode * Extra_bddAndPermute( DdManager * ddF, DdNode * bF, DdManager extern int Extra_bddCountCubes( DdManager * dd, DdNode ** pFuncs, int nFuncs, int fMode, int nLimit, int * pGuide ); extern void Extra_zddDumpPla( DdManager * dd, DdNode * zCover, int nVars, char * pFileName ); +/* build the set of all tuples of K variables out of N */ +extern DdNode * Extra_bddTuples( DdManager * dd, int K, DdNode * bVarsN ); +extern DdNode * extraBddTuples( DdManager * dd, DdNode * bVarsK, DdNode * bVarsN ); + #ifndef ABC_PRB #define ABC_PRB(dd,f) printf("%s = ", #f); Extra_bddPrint(dd,f); printf("\n") #endif diff --git a/src/bdd/extrab/extraBddMisc.c b/src/bdd/extrab/extraBddMisc.c index a5cda242..335f6754 100644 --- a/src/bdd/extrab/extraBddMisc.c +++ b/src/bdd/extrab/extraBddMisc.c @@ -2582,6 +2582,163 @@ void Extra_ZddTest() } +/**Function******************************************************************** + + Synopsis [Performs the reordering-sensitive step of Extra_bddTuples().] + + Description [Generates in a bottom-up fashion BDD for all combinations + composed of k variables out of variables belonging to bVarsN.] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +DdNode * extraBddTuples( + DdManager * dd, /* the DD manager */ + DdNode * bVarsK, /* the number of variables in tuples */ + DdNode * bVarsN) /* the set of all variables */ +{ + DdNode *bRes, *bRes0, *bRes1; + statLine(dd); + + /* terminal cases */ +/* if ( k < 0 || k > n ) + * return dd->zero; + * if ( n == 0 ) + * return dd->one; + */ + if ( cuddI( dd, bVarsK->index ) < cuddI( dd, bVarsN->index ) ) + return b0; + if ( bVarsN == b1 ) + return b1; + + /* check cache */ + bRes = cuddCacheLookup2(dd, extraBddTuples, bVarsK, bVarsN); + if (bRes) + return(bRes); + + /* ZDD in which is variable is 0 */ +/* bRes0 = extraBddTuples( dd, k, n-1 ); */ + bRes0 = extraBddTuples( dd, bVarsK, cuddT(bVarsN) ); + if ( bRes0 == NULL ) + return NULL; + cuddRef( bRes0 ); + + /* ZDD in which is variable is 1 */ +/* bRes1 = extraBddTuples( dd, k-1, n-1 ); */ + if ( bVarsK == b1 ) + { + bRes1 = b0; + cuddRef( bRes1 ); + } + else + { + bRes1 = extraBddTuples( dd, cuddT(bVarsK), cuddT(bVarsN) ); + if ( bRes1 == NULL ) + { + Cudd_RecursiveDeref( dd, bRes0 ); + return NULL; + } + cuddRef( bRes1 ); + } + + /* consider the case when Res0 and Res1 are the same node */ + if ( bRes0 == bRes1 ) + bRes = bRes1; + /* consider the case when Res1 is complemented */ + else if ( Cudd_IsComplement(bRes1) ) + { + bRes = cuddUniqueInter(dd, bVarsN->index, Cudd_Not(bRes1), Cudd_Not(bRes0)); + if ( bRes == NULL ) + { + Cudd_RecursiveDeref(dd,bRes0); + Cudd_RecursiveDeref(dd,bRes1); + return NULL; + } + bRes = Cudd_Not(bRes); + } + else + { + bRes = cuddUniqueInter( dd, bVarsN->index, bRes1, bRes0 ); + if ( bRes == NULL ) + { + Cudd_RecursiveDeref(dd,bRes0); + Cudd_RecursiveDeref(dd,bRes1); + return NULL; + } + } + cuddDeref( bRes0 ); + cuddDeref( bRes1 ); + + /* insert the result into cache */ + cuddCacheInsert2(dd, extraBddTuples, bVarsK, bVarsN, bRes); + return bRes; + +} /* end of extraBddTuples */ + +/**Function******************************************************************** + + Synopsis [Builds BDD representing the set of fixed-size variable tuples.] + + Description [Creates BDD of all combinations of variables in Support that have k vars in them.] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +DdNode * Extra_bddTuples( + DdManager * dd, /* the DD manager */ + int K, /* the number of variables in tuples */ + DdNode * VarsN) /* the set of all variables represented as a BDD */ +{ + DdNode *res; + int autoDyn; + + /* it is important that reordering does not happen, + otherwise, this methods will not work */ + + autoDyn = dd->autoDyn; + dd->autoDyn = 0; + + do { + /* transform the numeric arguments (K) into a DdNode * argument; + * this allows us to use the standard internal CUDD cache */ + DdNode *VarSet = VarsN, *VarsK = VarsN; + int nVars = 0, i; + + /* determine the number of variables in VarSet */ + while ( VarSet != b1 ) + { + nVars++; + /* make sure that the VarSet is a cube */ + if ( cuddE( VarSet ) != b0 ) + return NULL; + VarSet = cuddT( VarSet ); + } + /* make sure that the number of variables in VarSet is less or equal + that the number of variables that should be present in the tuples + */ + if ( K > nVars ) + return NULL; + + /* the second argument in the recursive call stannds for ; + /* reate the first argument, which stands for + * as when we are talking about the tuple of out of */ + for ( i = 0; i < nVars-K; i++ ) + VarsK = cuddT( VarsK ); + + dd->reordered = 0; + res = extraBddTuples(dd, VarsK, VarsN ); + + } while (dd->reordered == 1); + dd->autoDyn = autoDyn; + return(res); + +} /* end of Extra_bddTuples */ + + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// -- cgit v1.2.3