src/cuBdd/cuddSplit.c File Reference

#include "util.h"
#include "cuddInt.h"
Include dependency graph for cuddSplit.c:

Go to the source code of this file.

Functions

static DdNode * selectMintermsFromUniverse (DdManager *manager, int *varSeen, double n)
static DdNode * mintermsFromUniverse (DdManager *manager, DdNode **vars, int numVars, double n, int index)
static double bddAnnotateMintermCount (DdManager *manager, DdNode *node, double max, st_table *table)
DdNode * Cudd_SplitSet (DdManager *manager, DdNode *S, DdNode **xVars, int n, double m)
DdNode * cuddSplitSetRecur (DdManager *manager, st_table *mtable, int *varSeen, DdNode *p, double n, double max, int index)

Function Documentation

static double bddAnnotateMintermCount ( DdManager *  manager,
DdNode *  node,
double  max,
st_table *  table 
) [static]

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>.]

Definition at line 629 of file cuddSplit.c.

00634 {
00635 
00636     DdNode *N,*Nv,*Nnv;
00637     register double min_v,min_nv;
00638     register double min_N;
00639     double *pmin;
00640     double *dummy;
00641 
00642     statLine(manager);
00643     N = Cudd_Regular(node);
00644     if (cuddIsConstant(N)) {
00645         if (node == DD_ONE(manager)) {
00646             return(max);
00647         } else {
00648             return(0.0);
00649         }
00650     }
00651 
00652     if (st_lookup(table, node, &dummy)) {
00653         return(*dummy);
00654     }   
00655   
00656     Nv = cuddT(N);
00657     Nnv = cuddE(N);
00658     if (N != node) {
00659         Nv = Cudd_Not(Nv);
00660         Nnv = Cudd_Not(Nnv);
00661     }
00662 
00663     /* Recur on the two branches. */
00664     min_v  = bddAnnotateMintermCount(manager,Nv,max,table) / 2.0;
00665     if (min_v == (double)CUDD_OUT_OF_MEM)
00666         return ((double)CUDD_OUT_OF_MEM);
00667     min_nv = bddAnnotateMintermCount(manager,Nnv,max,table) / 2.0;
00668     if (min_nv == (double)CUDD_OUT_OF_MEM)
00669         return ((double)CUDD_OUT_OF_MEM);
00670     min_N  = min_v + min_nv;
00671 
00672     pmin = ALLOC(double,1);
00673     if (pmin == NULL) {
00674         manager->errorCode = CUDD_MEMORY_OUT;
00675         return((double)CUDD_OUT_OF_MEM);
00676     }
00677     *pmin = min_N;
00678 
00679     if (st_insert(table,(char *)node, (char *)pmin) == ST_OUT_OF_MEM) {
00680         FREE(pmin);
00681         return((double)CUDD_OUT_OF_MEM);
00682     }
00683     
00684     return(min_N);
00685 
00686 } /* end of bddAnnotateMintermCount */

DdNode* Cudd_SplitSet ( DdManager *  manager,
DdNode *  S,
DdNode **  xVars,
int  n,
double  m 
)

AutomaticEnd Function********************************************************************

Synopsis [Returns m minterms from a BDD.]

Description [Returns m minterms from a BDD whose support has n variables at most. The procedure tries to create as few extra nodes as possible. The function represented by S depends on at most n of the variables in xVars. Returns a BDD with m minterms of the on-set of S if successful; NULL otherwise.]

SideEffects [None]

SeeAlso []

Definition at line 124 of file cuddSplit.c.

00130 {
00131     DdNode *result;
00132     DdNode *zero, *one;
00133     double  max, num;
00134     st_table *mtable;
00135     int *varSeen;
00136     int i,index, size;
00137 
00138     size = manager->size;
00139     one = DD_ONE(manager);
00140     zero = Cudd_Not(one);
00141 
00142     /* Trivial cases. */
00143     if (m == 0.0) {
00144         return(zero);
00145     }
00146     if (S == zero) {
00147         return(NULL);
00148     }
00149 
00150     max = pow(2.0,(double)n);
00151     if (m > max)
00152         return(NULL);
00153 
00154     do {
00155         manager->reordered = 0;
00156         /* varSeen is used to mark the variables that are encountered
00157         ** while traversing the BDD S.
00158         */
00159         varSeen = ALLOC(int, size);
00160         if (varSeen == NULL) {
00161             manager->errorCode = CUDD_MEMORY_OUT;
00162             return(NULL);
00163         }
00164         for (i = 0; i < size; i++) {
00165             varSeen[i] = -1;
00166         }
00167         for (i = 0; i < n; i++) {
00168             index = (xVars[i])->index;
00169             varSeen[manager->invperm[index]] = 0;
00170         }
00171 
00172         if (S == one) {
00173             if (m == max) {
00174                 FREE(varSeen);
00175                 return(S);
00176             }
00177             result = selectMintermsFromUniverse(manager,varSeen,m);
00178             if (result)
00179                 cuddRef(result);
00180             FREE(varSeen);
00181         } else {
00182             mtable = st_init_table(st_ptrcmp,st_ptrhash);
00183             if (mtable == NULL) {
00184                 (void) fprintf(manager->out,
00185                                "Cudd_SplitSet: out-of-memory.\n");
00186                 FREE(varSeen);
00187                 manager->errorCode = CUDD_MEMORY_OUT;
00188                 return(NULL);
00189             }
00190             /* The nodes of BDD S are annotated by the number of minterms
00191             ** in their onset. The node and the number of minterms in its
00192             ** onset are stored in mtable.
00193             */
00194             num = bddAnnotateMintermCount(manager,S,max,mtable);
00195             if (m == num) {
00196                 st_foreach(mtable,cuddStCountfree,NIL(char));
00197                 st_free_table(mtable);
00198                 FREE(varSeen);
00199                 return(S);
00200             }
00201             
00202             result = cuddSplitSetRecur(manager,mtable,varSeen,S,m,max,0);
00203             if (result)
00204                 cuddRef(result);
00205             st_foreach(mtable,cuddStCountfree,NULL);
00206             st_free_table(mtable);
00207             FREE(varSeen);
00208         }
00209     } while (manager->reordered == 1);
00210 
00211     cuddDeref(result);
00212     return(result);
00213 
00214 } /* end of Cudd_SplitSet */

DdNode* cuddSplitSetRecur ( DdManager *  manager,
st_table *  mtable,
int *  varSeen,
DdNode *  p,
double  n,
double  max,
int  index 
)

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 []

Definition at line 243 of file cuddSplit.c.

00251 {
00252     DdNode *one, *zero, *N, *Nv;
00253     DdNode *Nnv, *q, *r, *v;
00254     DdNode *result;
00255     double *dummy, numT, numE;
00256     int variable, positive;
00257   
00258     statLine(manager);
00259     one = DD_ONE(manager);
00260     zero = Cudd_Not(one);
00261 
00262     /* If p is constant, extract n minterms from constant 1.  The procedure by
00263     ** construction guarantees that minterms will not be extracted from
00264     ** constant 0.
00265     */
00266     if (Cudd_IsConstant(p)) {
00267         q = selectMintermsFromUniverse(manager,varSeen,n);
00268         return(q);
00269     }
00270 
00271     N = Cudd_Regular(p);
00272 
00273     /* Set variable as seen. */
00274     variable = N->index;
00275     varSeen[manager->invperm[variable]] = -1;
00276 
00277     Nv = cuddT(N);
00278     Nnv = cuddE(N);
00279     if (Cudd_IsComplement(p)) {
00280         Nv = Cudd_Not(Nv);
00281         Nnv = Cudd_Not(Nnv);
00282     }
00283 
00284     /* If both the children of 'p' are constants, extract n minterms from a
00285     ** constant node.
00286     */
00287     if (Cudd_IsConstant(Nv) && Cudd_IsConstant(Nnv)) {
00288         q = selectMintermsFromUniverse(manager,varSeen,n);
00289         if (q == NULL) {
00290             return(NULL);
00291         }
00292         cuddRef(q);
00293         r = cuddBddAndRecur(manager,p,q);
00294         if (r == NULL) {
00295             Cudd_RecursiveDeref(manager,q);
00296             return(NULL);
00297         }
00298         cuddRef(r);
00299         Cudd_RecursiveDeref(manager,q);
00300         cuddDeref(r);
00301         return(r);
00302     }
00303   
00304     /* Lookup the # of minterms in the onset of the node from the table. */
00305     if (!Cudd_IsConstant(Nv)) {
00306         if (!st_lookup(mtable, Nv, &dummy)) return(NULL);
00307         numT = *dummy/(2*(1<<index));
00308     } else if (Nv == one) {
00309         numT = max/(2*(1<<index));
00310     } else {
00311         numT = 0;
00312     }
00313   
00314     if (!Cudd_IsConstant(Nnv)) {
00315         if (!st_lookup(mtable, Nnv, &dummy)) return(NULL);
00316         numE = *dummy/(2*(1<<index));
00317     } else if (Nnv == one) {
00318         numE = max/(2*(1<<index));
00319     } else {
00320         numE = 0;
00321     }
00322 
00323     v = cuddUniqueInter(manager,variable,one,zero);
00324     cuddRef(v);
00325 
00326     /* If perfect match. */
00327     if (numT == n) {
00328         q = cuddBddAndRecur(manager,v,Nv);
00329         if (q == NULL) {
00330             Cudd_RecursiveDeref(manager,v);
00331             return(NULL);
00332         }
00333         cuddRef(q);
00334         Cudd_RecursiveDeref(manager,v);
00335         cuddDeref(q);
00336         return(q);
00337     }
00338     if (numE == n) {
00339         q = cuddBddAndRecur(manager,Cudd_Not(v),Nnv);
00340         if (q == NULL) {
00341             Cudd_RecursiveDeref(manager,v);
00342             return(NULL);
00343         }
00344         cuddRef(q);
00345         Cudd_RecursiveDeref(manager,v);
00346         cuddDeref(q);
00347         return(q);
00348     }
00349     /* If n is greater than numT, extract the difference from the ELSE child
00350     ** and retain the function represented by the THEN branch.
00351     */
00352     if (numT < n) {
00353         q = cuddSplitSetRecur(manager,mtable,varSeen,
00354                               Nnv,(n-numT),max,index+1);
00355         if (q == NULL) {
00356             Cudd_RecursiveDeref(manager,v);
00357             return(NULL);
00358         }
00359         cuddRef(q);
00360         r = cuddBddIteRecur(manager,v,Nv,q);
00361         if (r == NULL) {
00362             Cudd_RecursiveDeref(manager,q);
00363             Cudd_RecursiveDeref(manager,v);
00364             return(NULL);
00365         }
00366         cuddRef(r);
00367         Cudd_RecursiveDeref(manager,q);
00368         Cudd_RecursiveDeref(manager,v);
00369         cuddDeref(r);
00370         return(r);
00371     }
00372     /* If n is greater than numE, extract the difference from the THEN child
00373     ** and retain the function represented by the ELSE branch.
00374     */
00375     if (numE < n) {
00376         q = cuddSplitSetRecur(manager,mtable,varSeen,
00377                               Nv, (n-numE),max,index+1);
00378         if (q == NULL) {
00379             Cudd_RecursiveDeref(manager,v);
00380             return(NULL);
00381         }
00382         cuddRef(q);
00383         r = cuddBddIteRecur(manager,v,q,Nnv);
00384         if (r == NULL) {
00385             Cudd_RecursiveDeref(manager,q);
00386             Cudd_RecursiveDeref(manager,v);
00387             return(NULL);
00388         }
00389         cuddRef(r);
00390         Cudd_RecursiveDeref(manager,q);
00391         Cudd_RecursiveDeref(manager,v);
00392         cuddDeref(r);    
00393         return(r);
00394     }
00395 
00396     /* None of the above cases; (n < numT and n < numE) and either of
00397     ** the Nv, Nnv or both are not constants. If possible extract the
00398     ** required minterms the constant branch.
00399     */
00400     if (Cudd_IsConstant(Nv) && !Cudd_IsConstant(Nnv)) {
00401         q = selectMintermsFromUniverse(manager,varSeen,n);
00402         if (q == NULL) {
00403             Cudd_RecursiveDeref(manager,v);
00404             return(NULL);
00405         }
00406         cuddRef(q);
00407         result = cuddBddAndRecur(manager,v,q);
00408         if (result == NULL) {
00409             Cudd_RecursiveDeref(manager,q);
00410             Cudd_RecursiveDeref(manager,v);
00411             return(NULL);
00412         }
00413         cuddRef(result);
00414         Cudd_RecursiveDeref(manager,q);
00415         Cudd_RecursiveDeref(manager,v);
00416         cuddDeref(result);
00417         return(result);
00418     } else if (!Cudd_IsConstant(Nv) && Cudd_IsConstant(Nnv)) {
00419         q = selectMintermsFromUniverse(manager,varSeen,n);
00420         if (q == NULL) {
00421             Cudd_RecursiveDeref(manager,v);
00422             return(NULL);
00423         }
00424         cuddRef(q);
00425         result = cuddBddAndRecur(manager,Cudd_Not(v),q);
00426         if (result == NULL) {
00427             Cudd_RecursiveDeref(manager,q);
00428             Cudd_RecursiveDeref(manager,v);
00429             return(NULL);
00430         }
00431         cuddRef(result);
00432         Cudd_RecursiveDeref(manager,q);
00433         Cudd_RecursiveDeref(manager,v);
00434         cuddDeref(result);
00435         return(result);
00436     }
00437 
00438     /* Both Nv and Nnv are not constants. So choose the one which
00439     ** has fewer minterms in its onset.
00440     */
00441     positive = 0;
00442     if (numT < numE) {
00443         q = cuddSplitSetRecur(manager,mtable,varSeen,
00444                               Nv,n,max,index+1);
00445         positive = 1;
00446     } else {
00447         q = cuddSplitSetRecur(manager,mtable,varSeen,
00448                               Nnv,n,max,index+1);
00449     }
00450 
00451     if (q == NULL) {
00452         Cudd_RecursiveDeref(manager,v);
00453         return(NULL);
00454     }
00455     cuddRef(q);
00456 
00457     if (positive) {
00458         result = cuddBddAndRecur(manager,v,q);
00459     } else {
00460         result = cuddBddAndRecur(manager,Cudd_Not(v),q);
00461     }
00462     if (result == NULL) {
00463         Cudd_RecursiveDeref(manager,q);
00464         Cudd_RecursiveDeref(manager,v);
00465         return(NULL);
00466     }
00467     cuddRef(result);
00468     Cudd_RecursiveDeref(manager,q);
00469     Cudd_RecursiveDeref(manager,v);
00470     cuddDeref(result);
00471 
00472     return(result);
00473 
00474 } /* end of cuddSplitSetRecur */

static DdNode * mintermsFromUniverse ( DdManager *  manager,
DdNode **  vars,
int  numVars,
double  n,
int  index 
) [static]

Function********************************************************************

Synopsis [Recursive procedure to extract n mintems from constant 1.]

Description [Recursive procedure to extract n mintems from constant 1.]

SideEffects [None]

Definition at line 558 of file cuddSplit.c.

00564 {
00565     DdNode *one, *zero;
00566     DdNode *q, *result;
00567     double max, max2;
00568     
00569     statLine(manager);
00570     one = DD_ONE(manager);
00571     zero = Cudd_Not(one);
00572 
00573     max = pow(2.0, (double)numVars);
00574     max2 = max / 2.0;
00575 
00576     if (n == max)
00577         return(one);
00578     if (n == 0.0)
00579         return(zero);
00580     /* if n == 2^(numVars-1), return a single variable */
00581     if (n == max2)
00582         return vars[index];
00583     else if (n > max2) {
00584         /* When n > 2^(numVars-1), a single variable vars[index]
00585         ** contains 2^(numVars-1) minterms. The rest are extracted
00586         ** from a constant with 1 less variable.
00587         */
00588         q = mintermsFromUniverse(manager,vars,numVars-1,(n-max2),index+1);
00589         if (q == NULL)
00590             return(NULL);
00591         cuddRef(q);
00592         result = cuddBddIteRecur(manager,vars[index],one,q);
00593     } else {
00594         /* When n < 2^(numVars-1), a literal of variable vars[index]
00595         ** is selected. The required n minterms are extracted from a
00596         ** constant with 1 less variable.
00597         */
00598         q = mintermsFromUniverse(manager,vars,numVars-1,n,index+1);
00599         if (q == NULL)
00600             return(NULL);
00601         cuddRef(q);
00602         result = cuddBddAndRecur(manager,vars[index],q);
00603     }
00604     
00605     if (result == NULL) {
00606         Cudd_RecursiveDeref(manager,q);
00607         return(NULL);
00608     }
00609     cuddRef(result);
00610     Cudd_RecursiveDeref(manager,q);
00611     cuddDeref(result);
00612     return(result);
00613 
00614 } /* end of mintermsFromUniverse */

static DdNode * selectMintermsFromUniverse ( DdManager *  manager,
int *  varSeen,
double  n 
) [static]

CFile***********************************************************************

FileName [cuddSplit.c]

PackageName [cudd]

Synopsis [Returns a subset of minterms from a boolean function.]

Description [External functions included in this modoule:

Internal functions included in this module:

  • cuddSplitSetRecur() </u> Static functions included in this module:

    ]

    SeeAlso []

    Author [Balakrishna Kumthekar]

    Copyright [Copyright (c) 1995-2004, Regents of the University of Colorado

    All rights reserved.

    Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met:

    Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer.

    Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution.

    Neither the name of the University of Colorado nor the names of its contributors may be used to endorse or promote products derived from this software without specific prior written permission.

    THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.]AutomaticStart

    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 (n).]

    SideEffects [None]

Definition at line 495 of file cuddSplit.c.

00499 {
00500     int numVars;
00501     int i, size, j;
00502      DdNode *one, *zero, *result;
00503     DdNode **vars;
00504 
00505     numVars = 0;
00506     size = manager->size;
00507     one = DD_ONE(manager);
00508     zero = Cudd_Not(one);
00509 
00510     /* Count the number of variables not encountered so far in procedure
00511     ** cuddSplitSetRecur.
00512     */
00513     for (i = size-1; i >= 0; i--) {
00514         if(varSeen[i] == 0)
00515             numVars++;
00516     }
00517     vars = ALLOC(DdNode *, numVars);
00518     if (!vars) {
00519         manager->errorCode = CUDD_MEMORY_OUT;
00520         return(NULL);
00521     }
00522 
00523     j = 0;
00524     for (i = size-1; i >= 0; i--) {
00525         if(varSeen[i] == 0) {
00526             vars[j] = cuddUniqueInter(manager,manager->perm[i],one,zero);
00527             cuddRef(vars[j]);
00528             j++;
00529         }
00530     }
00531 
00532     /* Compute a function which has n minterms and depends on at most
00533     ** numVars variables.
00534     */
00535     result = mintermsFromUniverse(manager,vars,numVars,n, 0);
00536     if (result) 
00537         cuddRef(result);
00538 
00539     for (i = 0; i < numVars; i++)
00540         Cudd_RecursiveDeref(manager,vars[i]);
00541     FREE(vars);
00542 
00543     return(result);
00544 
00545 } /* end of selectMintermsFromUniverse */

Generated on Tue Jan 12 13:57:21 2010 for glu-2.2 by  doxygen 1.6.1