summaryrefslogtreecommitdiffstats
path: root/src/bdd/extrab
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2017-02-17 14:09:58 -0800
committerAlan Mishchenko <alanmi@berkeley.edu>2017-02-17 14:09:58 -0800
commit378af9d94fc32232f638c784fb9cb9095f410bee (patch)
tree80351e283f5465f45f609b7af8ad6737bf6741a3 /src/bdd/extrab
parent6d6bf8740d246b1478b636a1d300ede371bffabe (diff)
downloadabc-378af9d94fc32232f638c784fb9cb9095f410bee.tar.gz
abc-378af9d94fc32232f638c784fb9cb9095f410bee.tar.bz2
abc-378af9d94fc32232f638c784fb9cb9095f410bee.zip
Experiment with graph constuction using ZDDs.
Diffstat (limited to 'src/bdd/extrab')
-rw-r--r--src/bdd/extrab/extraBddMisc.c203
1 files changed, 203 insertions, 0 deletions
diff --git a/src/bdd/extrab/extraBddMisc.c b/src/bdd/extrab/extraBddMisc.c
index 44170102..bc4d8a7a 100644
--- a/src/bdd/extrab/extraBddMisc.c
+++ b/src/bdd/extrab/extraBddMisc.c
@@ -2379,6 +2379,209 @@ void Extra_GraphExperiment()
Cudd_RecursiveDerefZdd( dd, zGraph );
Cudd_Quit(dd);
}
+
+
+
+
+/**Function********************************************************************
+
+ Synopsis [Performs the reordering-sensitive step of Extra_zddCombination().]
+
+ Description [Generates in a bottom-up fashion ZDD for one combination
+ whose var values are given in the array VarValues. If necessary,
+ creates new variables on the fly.]
+
+ SideEffects []
+
+ SeeAlso []
+
+******************************************************************************/
+DdNode * extraZddCombination(
+ DdManager* dd,
+ int* VarValues,
+ int nVars )
+{
+ int lev, index;
+ DdNode *zRes, *zTemp;
+
+ /* transform the combination from the array VarValues into a ZDD cube. */
+ zRes = dd->one;
+ cuddRef(zRes);
+
+ /* go through levels starting bottom-up and create nodes
+ * if these variables are present in the comb
+ */
+ for (lev = nVars - 1; lev >= 0; lev--)
+ {
+ index = (lev >= dd->sizeZ) ? lev : dd->invpermZ[lev];
+ if (VarValues[index] == 1)
+ {
+ /* compose zRes with ZERO for the given ZDD variable */
+ zRes = cuddZddGetNode( dd, index, zTemp = zRes, dd->zero );
+ if ( zRes == NULL )
+ {
+ Cudd_RecursiveDerefZdd( dd, zTemp );
+ return NULL;
+ }
+ cuddRef( zRes );
+ cuddDeref( zTemp );
+ }
+ }
+ cuddDeref( zRes );
+ return zRes;
+
+} /* end of extraZddCombination */
+
+/**Function********************************************************************
+
+ Synopsis [Creates ZDD of the combination containing given variables.]
+
+ Description [Creates ZDD of the combination containing given variables.
+ VarValues contains 1 for a variable that belongs to the
+ combination and 0 for a varible that does not belong.
+ nVars is number of ZDD variables in the array.]
+
+ SideEffects [New ZDD variables are created if indices of the variables
+ present in the combination are larger than the currently
+ allocated number of ZDD variables.]
+
+ SeeAlso []
+
+******************************************************************************/
+DdNode * Extra_zddCombination(
+ DdManager *dd,
+ int* VarValues,
+ int nVars )
+{
+ DdNode *res;
+ do {
+ dd->reordered = 0;
+ res = extraZddCombination(dd, VarValues, nVars);
+ } while (dd->reordered == 1);
+ return(res);
+
+} /* end of Extra_zddCombination */
+
+/**Function********************************************************************
+
+ Synopsis [Generates a random set of combinations.]
+
+ Description [Given a set of n elements, each of which is encoded using one
+ ZDD variable, this function generates a random set of k subsets
+ (combinations of elements) with density d. Assumes that k and n
+ are positive integers. Returns NULL if density is less than 0.0
+ or more than 1.0.]
+
+ SideEffects [Allocates new ZDD variables if their current number is less than n.]
+
+ SeeAlso []
+
+******************************************************************************/
+DdNode* Extra_zddRandomSet(
+ DdManager * dd, /* the DD manager */
+ int n, /* the number of elements */
+ int k, /* the number of combinations (subsets) */
+ double d) /* average density of elements in combinations */
+{
+ DdNode *Result, *TempComb, *Aux;
+ int c, v, Limit, *VarValues;
+
+ /* sanity check the parameters */
+ if ( n <= 0 || k <= 0 || d < 0.0 || d > 1.0 )
+ return NULL;
+
+ /* allocate temporary storage for variable values */
+ VarValues = ABC_ALLOC( int, n );
+ if (VarValues == NULL)
+ {
+ dd->errorCode = CUDD_MEMORY_OUT;
+ return NULL;
+ }
+
+ /* start the new set */
+ Result = dd->zero;
+ Cudd_Ref( Result );
+
+ /* seed random number generator */
+ Cudd_Srandom( time(NULL) );
+// Cudd_Srandom( 4 );
+ /* determine the limit below which var belongs to the combination */
+ Limit = (int)(d * 2147483561.0);
+
+ /* add combinations one by one */
+ for ( c = 0; c < k; c++ )
+ {
+ for ( v = 0; v < n; v++ )
+ if ( Cudd_Random() <= Limit )
+ VarValues[v] = 1;
+ else
+ VarValues[v] = 0;
+
+ TempComb = Extra_zddCombination( dd, VarValues, n );
+ Cudd_Ref( TempComb );
+
+ /* make sure that this combination is not already in the set */
+ if ( c )
+ { /* at least one combination is already included */
+
+ Aux = Cudd_zddDiff( dd, Result, TempComb );
+ Cudd_Ref( Aux );
+ if ( Aux != Result )
+ {
+ Cudd_RecursiveDerefZdd( dd, Aux );
+ Cudd_RecursiveDerefZdd( dd, TempComb );
+ c--;
+ continue;
+ }
+ else
+ { /* Aux is the same node as Result */
+ Cudd_Deref( Aux );
+ }
+ }
+
+ Result = Cudd_zddUnion( dd, Aux = Result, TempComb );
+ Cudd_Ref( Result );
+ Cudd_RecursiveDerefZdd( dd, Aux );
+ Cudd_RecursiveDerefZdd( dd, TempComb );
+ }
+
+ ABC_FREE( VarValues );
+ Cudd_Deref( Result );
+ return Result;
+
+} /* end of Extra_zddRandomSet */
+
+/**Function********************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+******************************************************************************/
+void Extra_ZddTest()
+{
+ int N = 64;
+ int K0 = 1000;
+ int i, Size;
+ DdManager * dd = Cudd_Init( 0, 32, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
+ for ( i = 1; i <= 10; i++ )
+ {
+ int K = K0 * i;
+ DdNode * zRandSet = Extra_zddRandomSet( dd, N, K, 0.5 ); Cudd_Ref(zRandSet);
+ Size = Cudd_zddDagSize(zRandSet);
+ //Cudd_zddPrintMinterm( dd, zRandSet );
+ printf( "N = %5d K = %5d BddSize = %6d MemBdd = %8.3f MB MemBit = %8.3f MB Ratio = %8.3f %%\n",
+ N, K, Size, 20.0*Size/(1<<20), 0.125 * N * K /(1<<20), 100.0*(0.125 * N * K)/(20.0*Size) );
+ Cudd_RecursiveDerefZdd( dd, zRandSet );
+ }
+ Cudd_Quit(dd);
+}
+
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////