diff options
Diffstat (limited to 'src/bdd/cudd/cuddSplit.c')
| -rw-r--r-- | src/bdd/cudd/cuddSplit.c | 657 |
1 files changed, 0 insertions, 657 deletions
diff --git a/src/bdd/cudd/cuddSplit.c b/src/bdd/cudd/cuddSplit.c deleted file mode 100644 index e21ea7cb..00000000 --- a/src/bdd/cudd/cuddSplit.c +++ /dev/null @@ -1,657 +0,0 @@ -/**CFile*********************************************************************** - - FileName [cuddSplit.c] - - PackageName [cudd] - - Synopsis [Returns a subset of minterms from a boolean function.] - - Description [External functions included in this modoule: - <ul> - <li> Cudd_SplitSet() - </ul> - Internal functions included in this module: - <ul> - <li> cuddSplitSetRecur() - </u> - Static functions included in this module: - <ul> - <li> selectMintermsFromUniverse() - <li> mintermsFromUniverse() - <li> bddAnnotateMintermCount() - </ul> ] - - SeeAlso [] - - Author [Balakrishna Kumthekar] - - Copyright [This file was created at the University of Colorado at - Boulder. The University of Colorado at Boulder makes no warranty - about the suitability of this software for any purpose. It is - presented on an AS IS basis.] - -******************************************************************************/ - -#include "util_hack.h" -#include "cuddInt.h" - -/*---------------------------------------------------------------------------*/ -/* Constant declarations */ -/*---------------------------------------------------------------------------*/ - -/*---------------------------------------------------------------------------*/ -/* Type declarations */ -/*---------------------------------------------------------------------------*/ - - -/*---------------------------------------------------------------------------*/ -/* Structure declarations */ -/*---------------------------------------------------------------------------*/ - - -/*---------------------------------------------------------------------------*/ -/* Variable declarations */ -/*---------------------------------------------------------------------------*/ - - -/*---------------------------------------------------------------------------*/ -/* Macro declarations */ -/*---------------------------------------------------------------------------*/ - - -/**AutomaticStart*************************************************************/ - -/*---------------------------------------------------------------------------*/ -/* Static function prototypes */ -/*---------------------------------------------------------------------------*/ - -static DdNode * selectMintermsFromUniverse ARGS((DdManager *manager, int *varSeen, double n)); -static DdNode * mintermsFromUniverse ARGS((DdManager *manager, DdNode **vars, int numVars, double n, int index)); -static double bddAnnotateMintermCount ARGS((DdManager *manager, DdNode *node, double max, st_table *table)); - -/**AutomaticEnd***************************************************************/ - - -/*---------------------------------------------------------------------------*/ -/* Definition of exported functions */ -/*---------------------------------------------------------------------------*/ - - -/**Function******************************************************************** - - Synopsis [Returns m minterms from a BDD.] - - Description [Returns <code>m</code> minterms from a BDD whose - support has <code>n</code> variables at most. The procedure tries - to create as few extra nodes as possible. The function represented - by <code>S</code> depends on at most <code>n</code> of the variables - in <code>xVars</code>. Returns a BDD with <code>m</code> minterms - of the on-set of S if successful; NULL otherwise.] - - SideEffects [None] - - SeeAlso [] - -******************************************************************************/ -DdNode * -Cudd_SplitSet( - DdManager * manager, - DdNode * S, - DdNode ** xVars, - int n, - double m) -{ - DdNode *result; - DdNode *zero, *one; - double max, num; - st_table *mtable; - int *varSeen; - int i,index, size; - - size = manager->size; - one = DD_ONE(manager); - zero = Cudd_Not(one); - - /* Trivial cases. */ - if (m == 0.0) { - return(zero); - } - if (S == zero) { - return(NULL); - } - - max = pow(2.0,(double)n); - if (m > max) - return(NULL); - - do { - manager->reordered = 0; - /* varSeen is used to mark the variables that are encountered - ** while traversing the BDD S. - */ - varSeen = ALLOC(int, size); - if (varSeen == NULL) { - manager->errorCode = CUDD_MEMORY_OUT; - return(NULL); - } - for (i = 0; i < size; i++) { - varSeen[i] = -1; - } - for (i = 0; i < n; i++) { - index = (xVars[i])->index; - varSeen[manager->invperm[index]] = 0; - } - - if (S == one) { - if (m == max) - return(S); - result = selectMintermsFromUniverse(manager,varSeen,m); - if (result) - cuddRef(result); - FREE(varSeen); - } else { - mtable = st_init_table(st_ptrcmp,st_ptrhash); - if (mtable == NULL) { - (void) fprintf(manager->out, - "Cudd_SplitSet: out-of-memory.\n"); - FREE(varSeen); - manager->errorCode = CUDD_MEMORY_OUT; - return(NULL); - } - /* The nodes of BDD S are annotated by the number of minterms - ** in their onset. The node and the number of minterms in its - ** onset are stored in mtable. - */ - num = bddAnnotateMintermCount(manager,S,max,mtable); - if (m == num) { - st_foreach(mtable,cuddStCountfree,NIL(char)); - st_free_table(mtable); - FREE(varSeen); - return(S); - } - - result = cuddSplitSetRecur(manager,mtable,varSeen,S,m,max,0); - if (result) - cuddRef(result); - st_foreach(mtable,cuddStCountfree,NULL); - st_free_table(mtable); - FREE(varSeen); - } - } while (manager->reordered == 1); - - cuddDeref(result); - return(result); - -} /* end of Cudd_SplitSet */ - - -/*---------------------------------------------------------------------------*/ -/* Definition of internal functions */ -/*---------------------------------------------------------------------------*/ - -/**Function******************************************************************** - - Synopsis [Implements the recursive step of Cudd_SplitSet.] - - Description [Implements the recursive step of Cudd_SplitSet. The - procedure recursively traverses the BDD and checks to see if any - node satisfies the minterm requirements as specified by 'n'. At any - node X, n is compared to the number of minterms in the onset of X's - children. If either of the child nodes have exactly n minterms, then - that node is returned; else, if n is greater than the onset of one - of the child nodes, that node is retained and the difference in the - number of minterms is extracted from the other child. In case n - minterms can be extracted from constant 1, the algorithm returns the - result with at most log(n) nodes.] - - SideEffects [The array 'varSeen' is updated at every recursive call - to set the variables traversed by the procedure.] - - SeeAlso [] - -******************************************************************************/ -DdNode* -cuddSplitSetRecur( - DdManager * manager, - st_table * mtable, - int * varSeen, - DdNode * p, - double n, - double max, - int index) -{ - DdNode *one, *zero, *N, *Nv; - DdNode *Nnv, *q, *r, *v; - DdNode *result; - double *dummy, numT, numE; - int variable, positive; - - statLine(manager); - one = DD_ONE(manager); - zero = Cudd_Not(one); - - /* If p is constant, extract n minterms from constant 1. The procedure by - ** construction guarantees that minterms will not be extracted from - ** constant 0. - */ - if (Cudd_IsConstant(p)) { - q = selectMintermsFromUniverse(manager,varSeen,n); - return(q); - } - - N = Cudd_Regular(p); - - /* Set variable as seen. */ - variable = N->index; - varSeen[manager->invperm[variable]] = -1; - - Nv = cuddT(N); - Nnv = cuddE(N); - if (Cudd_IsComplement(p)) { - Nv = Cudd_Not(Nv); - Nnv = Cudd_Not(Nnv); - } - - /* If both the children of 'p' are constants, extract n minterms from a - ** constant node. - */ - if (Cudd_IsConstant(Nv) && Cudd_IsConstant(Nnv)) { - q = selectMintermsFromUniverse(manager,varSeen,n); - if (q == NULL) { - return(NULL); - } - cuddRef(q); - r = cuddBddAndRecur(manager,p,q); - if (r == NULL) { - Cudd_RecursiveDeref(manager,q); - return(NULL); - } - cuddRef(r); - Cudd_RecursiveDeref(manager,q); - cuddDeref(r); - return(r); - } - - /* Lookup the # of minterms in the onset of the node from the table. */ - if (!Cudd_IsConstant(Nv)) { - st_lookup(mtable,(char *)Nv, (char **)&dummy); - numT = *dummy/(2*(1<<index)); - } else if (Nv == one) { - numT = max/(2*(1<<index)); - } else { - numT = 0; - } - - if (!Cudd_IsConstant(Nnv)) { - st_lookup(mtable,(char *)Nnv, (char **)&dummy); - numE = *dummy/(2*(1<<index)); - } else if (Nnv == one) { - numE = max/(2*(1<<index)); - } else { - numE = 0; - } - - v = cuddUniqueInter(manager,variable,one,zero); - cuddRef(v); - - /* If perfect match. */ - if (numT == n) { - q = cuddBddAndRecur(manager,v,Nv); - if (q == NULL) { - Cudd_RecursiveDeref(manager,v); - return(NULL); - } - cuddRef(q); - Cudd_RecursiveDeref(manager,v); - cuddDeref(q); - return(q); - } - if (numE == n) { - q = cuddBddAndRecur(manager,Cudd_Not(v),Nnv); - if (q == NULL) { - Cudd_RecursiveDeref(manager,v); - return(NULL); - } - cuddRef(q); - Cudd_RecursiveDeref(manager,v); - cuddDeref(q); - return(q); - } - /* If n is greater than numT, extract the difference from the ELSE child - ** and retain the function represented by the THEN branch. - */ - if (numT < n) { - q = cuddSplitSetRecur(manager,mtable,varSeen, - Nnv,(n-numT),max,index+1); - if (q == NULL) { - Cudd_RecursiveDeref(manager,v); - return(NULL); - } - cuddRef(q); - r = cuddBddIteRecur(manager,v,Nv,q); - if (r == NULL) { - Cudd_RecursiveDeref(manager,q); - Cudd_RecursiveDeref(manager,v); - return(NULL); - } - cuddRef(r); - Cudd_RecursiveDeref(manager,q); - Cudd_RecursiveDeref(manager,v); - cuddDeref(r); - return(r); - } - /* If n is greater than numE, extract the difference from the THEN child - ** and retain the function represented by the ELSE branch. - */ - if (numE < n) { - q = cuddSplitSetRecur(manager,mtable,varSeen, - Nv, (n-numE),max,index+1); - if (q == NULL) { - Cudd_RecursiveDeref(manager,v); - return(NULL); - } - cuddRef(q); - r = cuddBddIteRecur(manager,v,q,Nnv); - if (r == NULL) { - Cudd_RecursiveDeref(manager,q); - Cudd_RecursiveDeref(manager,v); - return(NULL); - } - cuddRef(r); - Cudd_RecursiveDeref(manager,q); - Cudd_RecursiveDeref(manager,v); - cuddDeref(r); - return(r); - } - - /* None of the above cases; (n < numT and n < numE) and either of - ** the Nv, Nnv or both are not constants. If possible extract the - ** required minterms the constant branch. - */ - if (Cudd_IsConstant(Nv) && !Cudd_IsConstant(Nnv)) { - q = selectMintermsFromUniverse(manager,varSeen,n); - if (q == NULL) { - Cudd_RecursiveDeref(manager,v); - return(NULL); - } - cuddRef(q); - result = cuddBddAndRecur(manager,v,q); - if (result == NULL) { - Cudd_RecursiveDeref(manager,q); - Cudd_RecursiveDeref(manager,v); - return(NULL); - } - cuddRef(result); - Cudd_RecursiveDeref(manager,q); - Cudd_RecursiveDeref(manager,v); - cuddDeref(result); - return(result); - } else if (!Cudd_IsConstant(Nv) && Cudd_IsConstant(Nnv)) { - q = selectMintermsFromUniverse(manager,varSeen,n); - if (q == NULL) { - Cudd_RecursiveDeref(manager,v); - return(NULL); - } - cuddRef(q); - result = cuddBddAndRecur(manager,Cudd_Not(v),q); - if (result == NULL) { - Cudd_RecursiveDeref(manager,q); - Cudd_RecursiveDeref(manager,v); - return(NULL); - } - cuddRef(result); - Cudd_RecursiveDeref(manager,q); - Cudd_RecursiveDeref(manager,v); - cuddDeref(result); - return(result); - } - - /* Both Nv and Nnv are not constants. So choose the one which - ** has fewer minterms in its onset. - */ - positive = 0; - if (numT < numE) { - q = cuddSplitSetRecur(manager,mtable,varSeen, - Nv,n,max,index+1); - positive = 1; - } else { - q = cuddSplitSetRecur(manager,mtable,varSeen, - Nnv,n,max,index+1); - } - - if (q == NULL) { - Cudd_RecursiveDeref(manager,v); - return(NULL); - } - cuddRef(q); - - if (positive) { - result = cuddBddAndRecur(manager,v,q); - } else { - result = cuddBddAndRecur(manager,Cudd_Not(v),q); - } - if (result == NULL) { - Cudd_RecursiveDeref(manager,q); - Cudd_RecursiveDeref(manager,v); - return(NULL); - } - cuddRef(result); - Cudd_RecursiveDeref(manager,q); - Cudd_RecursiveDeref(manager,v); - cuddDeref(result); - - return(result); - -} /* end of cuddSplitSetRecur */ - - -/*---------------------------------------------------------------------------*/ -/* Definition of static functions */ -/*---------------------------------------------------------------------------*/ - -/**Function******************************************************************** - - Synopsis [This function prepares an array of variables which have not been - encountered so far when traversing the procedure cuddSplitSetRecur.] - - Description [This function prepares an array of variables which have not been - encountered so far when traversing the procedure cuddSplitSetRecur. This - array is then used to extract the required number of minterms from a constant - 1. The algorithm guarantees that the size of BDD will be utmost \log(n).] - - SideEffects [None] - -******************************************************************************/ -static DdNode * -selectMintermsFromUniverse( - DdManager * manager, - int * varSeen, - double n) -{ - int numVars; - int i, size, j; - DdNode *one, *zero, *result; - DdNode **vars; - - numVars = 0; - size = manager->size; - one = DD_ONE(manager); - zero = Cudd_Not(one); - - /* Count the number of variables not encountered so far in procedure - ** cuddSplitSetRecur. - */ - for (i = size-1; i >= 0; i--) { - if(varSeen[i] == 0) - numVars++; - } - vars = ALLOC(DdNode *, numVars); - if (!vars) { - manager->errorCode = CUDD_MEMORY_OUT; - return(NULL); - } - - j = 0; - for (i = size-1; i >= 0; i--) { - if(varSeen[i] == 0) { - vars[j] = cuddUniqueInter(manager,manager->perm[i],one,zero); - cuddRef(vars[j]); - j++; - } - } - - /* Compute a function which has n minterms and depends on at most - ** numVars variables. - */ - result = mintermsFromUniverse(manager,vars,numVars,n, 0); - if (result) - cuddRef(result); - - for (i = 0; i < numVars; i++) - Cudd_RecursiveDeref(manager,vars[i]); - FREE(vars); - - return(result); - -} /* end of selectMintermsFromUniverse */ - - -/**Function******************************************************************** - - Synopsis [Recursive procedure to extract n mintems from constant 1.] - - Description [Recursive procedure to extract n mintems from constant 1.] - - SideEffects [None] - -******************************************************************************/ -static DdNode * -mintermsFromUniverse( - DdManager * manager, - DdNode ** vars, - int numVars, - double n, - int index) -{ - DdNode *one, *zero; - DdNode *q, *result; - double max, max2; - - statLine(manager); - one = DD_ONE(manager); - zero = Cudd_Not(one); - - max = pow(2.0, (double)numVars); - max2 = max / 2.0; - - if (n == max) - return(one); - if (n == 0.0) - return(zero); - /* if n == 2^(numVars-1), return a single variable */ - if (n == max2) - return vars[index]; - else if (n > max2) { - /* When n > 2^(numVars-1), a single variable vars[index] - ** contains 2^(numVars-1) minterms. The rest are extracted - ** from a constant with 1 less variable. - */ - q = mintermsFromUniverse(manager,vars,numVars-1,(n-max2),index+1); - if (q == NULL) - return(NULL); - cuddRef(q); - result = cuddBddIteRecur(manager,vars[index],one,q); - } else { - /* When n < 2^(numVars-1), a literal of variable vars[index] - ** is selected. The required n minterms are extracted from a - ** constant with 1 less variable. - */ - q = mintermsFromUniverse(manager,vars,numVars-1,n,index+1); - if (q == NULL) - return(NULL); - cuddRef(q); - result = cuddBddAndRecur(manager,vars[index],q); - } - - if (result == NULL) { - Cudd_RecursiveDeref(manager,q); - return(NULL); - } - cuddRef(result); - Cudd_RecursiveDeref(manager,q); - cuddDeref(result); - return(result); - -} /* end of mintermsFromUniverse */ - - -/**Function******************************************************************** - - Synopsis [Annotates every node in the BDD node with its minterm count.] - - Description [Annotates every node in the BDD node with its minterm count. - In this function, every node and the minterm count represented by it are - stored in a hash table.] - - SideEffects [Fills up 'table' with the pair <node,minterm_count>.] - -******************************************************************************/ -static double -bddAnnotateMintermCount( - DdManager * manager, - DdNode * node, - double max, - st_table * table) -{ - - DdNode *N,*Nv,*Nnv; - register double min_v,min_nv; - register double min_N; - double *pmin; - double *dummy; - - statLine(manager); - N = Cudd_Regular(node); - if (cuddIsConstant(N)) { - if (node == DD_ONE(manager)) { - return(max); - } else { - return(0.0); - } - } - - if (st_lookup(table,(char *)node,(char **)&dummy)) { - return(*dummy); - } - - Nv = cuddT(N); - Nnv = cuddE(N); - if (N != node) { - Nv = Cudd_Not(Nv); - Nnv = Cudd_Not(Nnv); - } - - /* Recur on the two branches. */ - min_v = bddAnnotateMintermCount(manager,Nv,max,table) / 2.0; - if (min_v == (double)CUDD_OUT_OF_MEM) - return ((double)CUDD_OUT_OF_MEM); - min_nv = bddAnnotateMintermCount(manager,Nnv,max,table) / 2.0; - if (min_nv == (double)CUDD_OUT_OF_MEM) - return ((double)CUDD_OUT_OF_MEM); - min_N = min_v + min_nv; - - pmin = ALLOC(double,1); - if (pmin == NULL) { - manager->errorCode = CUDD_MEMORY_OUT; - return((double)CUDD_OUT_OF_MEM); - } - *pmin = min_N; - - if (st_insert(table,(char *)node, (char *)pmin) == ST_OUT_OF_MEM) { - FREE(pmin); - return((double)CUDD_OUT_OF_MEM); - } - - return(min_N); - -} /* end of bddAnnotateMintermCount */ |