glu-2.2: src/cuBdd/cuddSplit.c Source File

00001 
00062 #include "util.h"
00063 #include "cuddInt.h"
00064 
00065 /*---------------------------------------------------------------------------*/
00066 /* Constant declarations                                                     */
00067 /*---------------------------------------------------------------------------*/
00068 
00069 /*---------------------------------------------------------------------------*/
00070 /* Type declarations                                                         */
00071 /*---------------------------------------------------------------------------*/
00072 
00073 
00074 /*---------------------------------------------------------------------------*/
00075 /* Structure declarations                                                    */
00076 /*---------------------------------------------------------------------------*/
00077 
00078 
00079 /*---------------------------------------------------------------------------*/
00080 /* Variable declarations                                                     */
00081 /*---------------------------------------------------------------------------*/
00082 
00083 
00084 /*---------------------------------------------------------------------------*/
00085 /* Macro declarations                                                        */
00086 /*---------------------------------------------------------------------------*/
00087 
00088 
00091 /*---------------------------------------------------------------------------*/
00092 /* Static function prototypes                                                */
00093 /*---------------------------------------------------------------------------*/
00094 
00095 static DdNode * selectMintermsFromUniverse (DdManager *manager, int *varSeen, double n);
00096 static DdNode * mintermsFromUniverse (DdManager *manager, DdNode **vars, int numVars, double n, int index);
00097 static double bddAnnotateMintermCount (DdManager *manager, DdNode *node, double max, st_table *table);
00098 
00102 /*---------------------------------------------------------------------------*/
00103 /* Definition of exported functions                                          */
00104 /*---------------------------------------------------------------------------*/
00105 
00106 
00123 DdNode *
00124 Cudd_SplitSet(
00125   DdManager * manager,
00126   DdNode * S,
00127   DdNode ** xVars,
00128   int  n,
00129   double  m)
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 */
00215 
00216 
00217 /*---------------------------------------------------------------------------*/
00218 /* Definition of internal functions                                          */
00219 /*---------------------------------------------------------------------------*/
00220 
00242 DdNode*
00243 cuddSplitSetRecur(
00244   DdManager * manager,
00245   st_table * mtable,
00246   int * varSeen,
00247   DdNode * p,
00248   double  n,
00249   double  max,
00250   int  index)
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 */
00475 
00476 
00477 /*---------------------------------------------------------------------------*/
00478 /* Definition of static functions                                            */
00479 /*---------------------------------------------------------------------------*/
00480 
00494 static DdNode *
00495 selectMintermsFromUniverse(
00496   DdManager * manager,
00497   int * varSeen,
00498   double  n)
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 */
00546 
00547 
00557 static DdNode *
00558 mintermsFromUniverse(
00559   DdManager * manager,
00560   DdNode ** vars,
00561   int  numVars,
00562   double  n,
00563   int  index)
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 */
00615 
00616 
00628 static double
00629 bddAnnotateMintermCount(
00630   DdManager * manager,
00631   DdNode * node,
00632   double  max,
00633   st_table * table)
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 */