abc70930: src/bdd/cudd/cuddAddApply.c Source File

00001 
00045 #include    "util_hack.h"
00046 #include    "cuddInt.h"
00047 
00048 /*---------------------------------------------------------------------------*/
00049 /* Constant declarations                                                     */
00050 /*---------------------------------------------------------------------------*/
00051 
00052 
00053 /*---------------------------------------------------------------------------*/
00054 /* Stucture declarations                                                     */
00055 /*---------------------------------------------------------------------------*/
00056 
00057 
00058 /*---------------------------------------------------------------------------*/
00059 /* Type declarations                                                         */
00060 /*---------------------------------------------------------------------------*/
00061 
00062 
00063 /*---------------------------------------------------------------------------*/
00064 /* Variable declarations                                                     */
00065 /*---------------------------------------------------------------------------*/
00066 
00067 #ifndef lint
00068 static char rcsid[] DD_UNUSED = "$Id: cuddAddApply.c,v 1.1.1.1 2003/02/24 22:23:50 wjiang Exp $";
00069 #endif
00070 
00071 
00072 /*---------------------------------------------------------------------------*/
00073 /* Macro declarations                                                        */
00074 /*---------------------------------------------------------------------------*/
00075 
00076 
00079 /*---------------------------------------------------------------------------*/
00080 /* Static function prototypes                                                */
00081 /*---------------------------------------------------------------------------*/
00082 
00083 
00087 /*---------------------------------------------------------------------------*/
00088 /* Definition of exported functions                                          */
00089 /*---------------------------------------------------------------------------*/
00090 
00106 DdNode *
00107 Cudd_addApply(
00108   DdManager * dd,
00109   DdNode * (*op)(DdManager *, DdNode **, DdNode **),
00110   DdNode * f,
00111   DdNode * g)
00112 {
00113     DdNode *res;
00114 
00115     do {
00116         dd->reordered = 0;
00117         res = cuddAddApplyRecur(dd,op,f,g);
00118     } while (dd->reordered == 1);
00119     return(res);
00120 
00121 } /* end of Cudd_addApply */
00122 
00123 
00136 DdNode *
00137 Cudd_addPlus(
00138   DdManager * dd,
00139   DdNode ** f,
00140   DdNode ** g)
00141 {
00142     DdNode *res;
00143     DdNode *F, *G;
00144     CUDD_VALUE_TYPE value;
00145 
00146     F = *f; G = *g;
00147     if (F == DD_ZERO(dd)) return(G);
00148     if (G == DD_ZERO(dd)) return(F);
00149     if (cuddIsConstant(F) && cuddIsConstant(G)) {
00150         value = cuddV(F)+cuddV(G);
00151         res = cuddUniqueConst(dd,value);
00152         return(res);
00153     }
00154     if (F > G) { /* swap f and g */
00155         *f = G;
00156         *g = F;
00157     }
00158     return(NULL);
00159 
00160 } /* end of Cudd_addPlus */
00161 
00162 
00176 DdNode *
00177 Cudd_addTimes(
00178   DdManager * dd,
00179   DdNode ** f,
00180   DdNode ** g)
00181 {
00182     DdNode *res;
00183     DdNode *F, *G;
00184     CUDD_VALUE_TYPE value;
00185 
00186     F = *f; G = *g;
00187     if (F == DD_ZERO(dd) || G == DD_ZERO(dd)) return(DD_ZERO(dd));
00188     if (F == DD_ONE(dd)) return(G);
00189     if (G == DD_ONE(dd)) return(F);
00190     if (cuddIsConstant(F) && cuddIsConstant(G)) {
00191         value = cuddV(F)*cuddV(G);
00192         res = cuddUniqueConst(dd,value);
00193         return(res);
00194     }
00195     if (F > G) { /* swap f and g */
00196         *f = G;
00197         *g = F;
00198     }
00199     return(NULL);
00200 
00201 } /* end of Cudd_addTimes */
00202 
00203 
00216 DdNode *
00217 Cudd_addThreshold(
00218   DdManager * dd,
00219   DdNode ** f,
00220   DdNode ** g)
00221 {
00222     DdNode *F, *G;
00223 
00224     F = *f; G = *g;
00225     if (F == G || F == DD_PLUS_INFINITY(dd)) return(F);
00226     if (cuddIsConstant(F) && cuddIsConstant(G)) {
00227         if (cuddV(F) >= cuddV(G)) {
00228             return(F);
00229         } else {
00230             return(DD_ZERO(dd));
00231         }
00232     }
00233     return(NULL);
00234 
00235 } /* end of Cudd_addThreshold */
00236 
00237 
00250 DdNode *
00251 Cudd_addSetNZ(
00252   DdManager * dd,
00253   DdNode ** f,
00254   DdNode ** g)
00255 {
00256     DdNode *F, *G;
00257 
00258     F = *f; G = *g;
00259     if (F == G) return(F);
00260     if (F == DD_ZERO(dd)) return(G);
00261     if (G == DD_ZERO(dd)) return(F);
00262     if (cuddIsConstant(G)) return(G);
00263     return(NULL);
00264 
00265 } /* end of Cudd_addSetNZ */
00266 
00267 
00280 DdNode *
00281 Cudd_addDivide(
00282   DdManager * dd,
00283   DdNode ** f,
00284   DdNode ** g)
00285 {
00286     DdNode *res;
00287     DdNode *F, *G;
00288     CUDD_VALUE_TYPE value;
00289 
00290     F = *f; G = *g;
00291     /* We would like to use F == G -> F/G == 1, but F and G may
00292     ** contain zeroes. */
00293     if (F == DD_ZERO(dd)) return(DD_ZERO(dd));
00294     if (G == DD_ONE(dd)) return(F);
00295     if (cuddIsConstant(F) && cuddIsConstant(G)) {
00296         value = cuddV(F)/cuddV(G);
00297         res = cuddUniqueConst(dd,value);
00298         return(res);
00299     }
00300     return(NULL);
00301 
00302 } /* end of Cudd_addDivide */
00303 
00304 
00317 DdNode *
00318 Cudd_addMinus(
00319   DdManager * dd,
00320   DdNode ** f,
00321   DdNode ** g)
00322 {
00323     DdNode *res;
00324     DdNode *F, *G;
00325     CUDD_VALUE_TYPE value;
00326 
00327     F = *f; G = *g;
00328     if (F == G) return(DD_ZERO(dd));
00329     if (F == DD_ZERO(dd)) return(cuddAddNegateRecur(dd,G));
00330     if (G == DD_ZERO(dd)) return(F);
00331     if (cuddIsConstant(F) && cuddIsConstant(G)) {
00332         value = cuddV(F)-cuddV(G);
00333         res = cuddUniqueConst(dd,value);
00334         return(res);
00335     }
00336     return(NULL);
00337 
00338 } /* end of Cudd_addMinus */
00339 
00340 
00353 DdNode *
00354 Cudd_addMinimum(
00355   DdManager * dd,
00356   DdNode ** f,
00357   DdNode ** g)
00358 {
00359     DdNode *F, *G;
00360 
00361     F = *f; G = *g;
00362     if (F == DD_PLUS_INFINITY(dd)) return(G);
00363     if (G == DD_PLUS_INFINITY(dd)) return(F);
00364     if (F == G) return(F);
00365 #if 0
00366     /* These special cases probably do not pay off. */
00367     if (F == DD_MINUS_INFINITY(dd)) return(F);
00368     if (G == DD_MINUS_INFINITY(dd)) return(G);
00369 #endif
00370     if (cuddIsConstant(F) && cuddIsConstant(G)) {
00371         if (cuddV(F) <= cuddV(G)) {
00372             return(F);
00373         } else {
00374             return(G);
00375         }
00376     }
00377     if (F > G) { /* swap f and g */
00378         *f = G;
00379         *g = F;
00380     }
00381     return(NULL);
00382 
00383 } /* end of Cudd_addMinimum */
00384 
00385 
00398 DdNode *
00399 Cudd_addMaximum(
00400   DdManager * dd,
00401   DdNode ** f,
00402   DdNode ** g)
00403 {
00404     DdNode *F, *G;
00405 
00406     F = *f; G = *g;
00407     if (F == G) return(F);
00408     if (F == DD_MINUS_INFINITY(dd)) return(G);
00409     if (G == DD_MINUS_INFINITY(dd)) return(F);
00410 #if 0
00411     /* These special cases probably do not pay off. */
00412     if (F == DD_PLUS_INFINITY(dd)) return(F);
00413     if (G == DD_PLUS_INFINITY(dd)) return(G);
00414 #endif
00415     if (cuddIsConstant(F) && cuddIsConstant(G)) {
00416         if (cuddV(F) >= cuddV(G)) {
00417             return(F);
00418         } else {
00419             return(G);
00420         }
00421     }
00422     if (F > G) { /* swap f and g */
00423         *f = G;
00424         *g = F;
00425     }
00426     return(NULL);
00427 
00428 } /* end of Cudd_addMaximum */
00429 
00430 
00444 DdNode *
00445 Cudd_addOneZeroMaximum(
00446   DdManager * dd,
00447   DdNode ** f,
00448   DdNode ** g)
00449 {
00450 
00451     if (*f == *g) return(DD_ZERO(dd));
00452     if (*g == DD_PLUS_INFINITY(dd))
00453         return DD_ZERO(dd);
00454     if (cuddIsConstant(*f) && cuddIsConstant(*g)) {
00455         if (cuddV(*f) > cuddV(*g)) {
00456             return(DD_ONE(dd));
00457         } else {
00458             return(DD_ZERO(dd));
00459         }
00460     }
00461 
00462     return(NULL);
00463 
00464 } /* end of Cudd_addOneZeroMaximum */
00465 
00466 
00479 DdNode *
00480 Cudd_addDiff(
00481   DdManager * dd,
00482   DdNode ** f,
00483   DdNode ** g)
00484 {
00485     DdNode *F, *G;
00486 
00487     F = *f; G = *g;
00488     if (F == G) return(DD_PLUS_INFINITY(dd));
00489     if (F == DD_PLUS_INFINITY(dd)) return(G);
00490     if (G == DD_PLUS_INFINITY(dd)) return(F);
00491     if (cuddIsConstant(F) && cuddIsConstant(G)) {
00492         if (cuddV(F) != cuddV(G)) {
00493             if (cuddV(F) < cuddV(G)) {
00494                 return(F);
00495             } else {
00496                 return(G);
00497             }
00498         } else {
00499             return(DD_PLUS_INFINITY(dd));
00500         }
00501     }
00502     return(NULL);
00503 
00504 } /* end of Cudd_addDiff */
00505 
00506 
00519 DdNode *
00520 Cudd_addAgreement(
00521   DdManager * dd,
00522   DdNode ** f,
00523   DdNode ** g)
00524 {
00525     DdNode *F, *G;
00526 
00527     F = *f; G = *g;
00528     if (F == G) return(F);
00529     if (F == dd->background) return(F);
00530     if (G == dd->background) return(G);
00531     if (cuddIsConstant(F) && cuddIsConstant(G)) return(dd->background);
00532     return(NULL);
00533 
00534 } /* end of Cudd_addAgreement */
00535 
00536 
00549 DdNode *
00550 Cudd_addOr(
00551   DdManager * dd,
00552   DdNode ** f,
00553   DdNode ** g)
00554 {
00555     DdNode *F, *G;
00556 
00557     F = *f; G = *g;
00558     if (F == DD_ONE(dd) || G == DD_ONE(dd)) return(DD_ONE(dd));
00559     if (cuddIsConstant(F)) return(G);
00560     if (cuddIsConstant(G)) return(F);
00561     if (F == G) return(F);
00562     if (F > G) { /* swap f and g */
00563         *f = G;
00564         *g = F;
00565     }
00566     return(NULL);
00567 
00568 } /* end of Cudd_addOr */
00569 
00570 
00583 DdNode *
00584 Cudd_addNand(
00585   DdManager * dd,
00586   DdNode ** f,
00587   DdNode ** g)
00588 {
00589     DdNode *F, *G;
00590 
00591     F = *f; G = *g;
00592     if (F == DD_ZERO(dd) || G == DD_ZERO(dd)) return(DD_ONE(dd));
00593     if (cuddIsConstant(F) && cuddIsConstant(G)) return(DD_ZERO(dd));
00594     if (F > G) { /* swap f and g */
00595         *f = G;
00596         *g = F;
00597     }
00598     return(NULL);
00599 
00600 } /* end of Cudd_addNand */
00601 
00602 
00615 DdNode *
00616 Cudd_addNor(
00617   DdManager * dd,
00618   DdNode ** f,
00619   DdNode ** g)
00620 {
00621     DdNode *F, *G;
00622 
00623     F = *f; G = *g;
00624     if (F == DD_ONE(dd) || G == DD_ONE(dd)) return(DD_ZERO(dd));
00625     if (cuddIsConstant(F) && cuddIsConstant(G)) return(DD_ONE(dd));
00626     if (F > G) { /* swap f and g */
00627         *f = G;
00628         *g = F;
00629     }
00630     return(NULL);
00631 
00632 } /* end of Cudd_addNor */
00633 
00634 
00647 DdNode *
00648 Cudd_addXor(
00649   DdManager * dd,
00650   DdNode ** f,
00651   DdNode ** g)
00652 {
00653     DdNode *F, *G;
00654 
00655     F = *f; G = *g;
00656     if (F == G) return(DD_ZERO(dd));
00657     if (F == DD_ONE(dd) && G == DD_ZERO(dd)) return(DD_ONE(dd));
00658     if (G == DD_ONE(dd) && F == DD_ZERO(dd)) return(DD_ONE(dd));
00659     if (cuddIsConstant(F) && cuddIsConstant(G)) return(DD_ZERO(dd));
00660     if (F > G) { /* swap f and g */
00661         *f = G;
00662         *g = F;
00663     }
00664     return(NULL);
00665 
00666 } /* end of Cudd_addXor */
00667 
00668 
00681 DdNode *
00682 Cudd_addXnor(
00683   DdManager * dd,
00684   DdNode ** f,
00685   DdNode ** g)
00686 {
00687     DdNode *F, *G;
00688 
00689     F = *f; G = *g;
00690     if (F == G) return(DD_ONE(dd));
00691     if (F == DD_ONE(dd) && G == DD_ONE(dd)) return(DD_ONE(dd));
00692     if (G == DD_ZERO(dd) && F == DD_ZERO(dd)) return(DD_ONE(dd));
00693     if (cuddIsConstant(F) && cuddIsConstant(G)) return(DD_ZERO(dd));
00694     if (F > G) { /* swap f and g */
00695         *f = G;
00696         *g = F;
00697     }
00698     return(NULL);
00699 
00700 } /* end of Cudd_addXnor */
00701 
00702 
00715 DdNode *
00716 Cudd_addMonadicApply(
00717   DdManager * dd,
00718   DdNode * (*op)(DdManager *, DdNode *),
00719   DdNode * f)
00720 {
00721     DdNode *res;
00722 
00723     do {
00724         dd->reordered = 0;
00725         res = cuddAddMonadicApplyRecur(dd,op,f);
00726     } while (dd->reordered == 1);
00727     return(res);
00728 
00729 } /* end of Cudd_addMonadicApply */
00730 
00731 
00745 DdNode *
00746 Cudd_addLog(
00747   DdManager * dd,
00748   DdNode * f)
00749 {
00750     if (cuddIsConstant(f)) {
00751         CUDD_VALUE_TYPE value = log(cuddV(f));
00752         DdNode *res = cuddUniqueConst(dd,value);
00753         return(res);
00754     }
00755     return(NULL);
00756 
00757 } /* end of Cudd_addLog */
00758 
00759 
00760 /*---------------------------------------------------------------------------*/
00761 /* Definition of internal functions                                          */
00762 /*---------------------------------------------------------------------------*/
00763 
00764 
00777 DdNode *
00778 cuddAddApplyRecur(
00779   DdManager * dd,
00780   DdNode * (*op)(DdManager *, DdNode **, DdNode **),
00781   DdNode * f,
00782   DdNode * g)
00783 {
00784     DdNode *res,
00785            *fv, *fvn, *gv, *gvn,
00786            *T, *E;
00787     unsigned int ford, gord;
00788     unsigned int index;
00789     DdNode *(*cacheOp)(DdManager *, DdNode *, DdNode *);
00790 
00791     /* Check terminal cases. Op may swap f and g to increase the
00792      * cache hit rate.
00793      */
00794     statLine(dd);
00795     res = (*op)(dd,&f,&g);
00796     if (res != NULL) return(res);
00797 
00798     /* Check cache. */
00799     cacheOp = (DdNode *(*)(DdManager *, DdNode *, DdNode *)) op;
00800     res = cuddCacheLookup2(dd,cacheOp,f,g);
00801     if (res != NULL) return(res);
00802 
00803     /* Recursive step. */
00804     ford = cuddI(dd,f->index);
00805     gord = cuddI(dd,g->index);
00806     if (ford <= gord) {
00807         index = f->index;
00808         fv = cuddT(f);
00809         fvn = cuddE(f);
00810     } else {
00811         index = g->index;
00812         fv = fvn = f;
00813     }
00814     if (gord <= ford) {
00815         gv = cuddT(g);
00816         gvn = cuddE(g);
00817     } else {
00818         gv = gvn = g;
00819     }
00820 
00821     T = cuddAddApplyRecur(dd,op,fv,gv);
00822     if (T == NULL) return(NULL);
00823     cuddRef(T);
00824 
00825     E = cuddAddApplyRecur(dd,op,fvn,gvn);
00826     if (E == NULL) {
00827         Cudd_RecursiveDeref(dd,T);
00828         return(NULL);
00829     }
00830     cuddRef(E);
00831 
00832     res = (T == E) ? T : cuddUniqueInter(dd,(int)index,T,E);
00833     if (res == NULL) {
00834         Cudd_RecursiveDeref(dd, T);
00835         Cudd_RecursiveDeref(dd, E);
00836         return(NULL);
00837     }
00838     cuddDeref(T);
00839     cuddDeref(E);
00840 
00841     /* Store result. */
00842     cuddCacheInsert2(dd,cacheOp,f,g,res);
00843 
00844     return(res);
00845 
00846 } /* end of cuddAddApplyRecur */
00847 
00848 
00861 DdNode *
00862 cuddAddMonadicApplyRecur(
00863   DdManager * dd,
00864   DdNode * (*op)(DdManager *, DdNode *),
00865   DdNode * f)
00866 {
00867     DdNode *res, *ft, *fe, *T, *E;
00868     unsigned int ford;
00869     unsigned int index;
00870 
00871     /* Check terminal cases. */
00872     statLine(dd);
00873     res = (*op)(dd,f);
00874     if (res != NULL) return(res);
00875 
00876     /* Check cache. */
00877     res = cuddCacheLookup1(dd,op,f);
00878     if (res != NULL) return(res);
00879 
00880     /* Recursive step. */
00881     ford = cuddI(dd,f->index);
00882     index = f->index;
00883     ft = cuddT(f);
00884     fe = cuddE(f);
00885 
00886     T = cuddAddMonadicApplyRecur(dd,op,ft);
00887     if (T == NULL) return(NULL);
00888     cuddRef(T);
00889 
00890     E = cuddAddMonadicApplyRecur(dd,op,fe);
00891     if (E == NULL) {
00892         Cudd_RecursiveDeref(dd,T);
00893         return(NULL);
00894     }
00895     cuddRef(E);
00896 
00897     res = (T == E) ? T : cuddUniqueInter(dd,(int)index,T,E);
00898     if (res == NULL) {
00899         Cudd_RecursiveDeref(dd, T);
00900         Cudd_RecursiveDeref(dd, E);
00901         return(NULL);
00902     }
00903     cuddDeref(T);
00904     cuddDeref(E);
00905 
00906     /* Store result. */
00907     cuddCacheInsert1(dd,op,f,res);
00908 
00909     return(res);
00910 
00911 } /* end of cuddAddMonadicApplyRecur */
00912 
00913 
00914 /*---------------------------------------------------------------------------*/
00915 /* Definition of static functions                                            */
00916 /*---------------------------------------------------------------------------*/
00917