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

00001 
00072 #include "util.h"
00073 #include "cuddInt.h"
00074 
00075 /*---------------------------------------------------------------------------*/
00076 /* Constant declarations                                                     */
00077 /*---------------------------------------------------------------------------*/
00078 
00079 
00080 /*---------------------------------------------------------------------------*/
00081 /* Stucture declarations                                                     */
00082 /*---------------------------------------------------------------------------*/
00083 
00084 
00085 /*---------------------------------------------------------------------------*/
00086 /* Type declarations                                                         */
00087 /*---------------------------------------------------------------------------*/
00088 
00089 
00090 /*---------------------------------------------------------------------------*/
00091 /* Variable declarations                                                     */
00092 /*---------------------------------------------------------------------------*/
00093 
00094 #ifndef lint
00095 static char rcsid[] DD_UNUSED = "$Id: cuddAddApply.c,v 1.18 2009/02/19 16:15:26 fabio Exp $";
00096 #endif
00097 
00098 
00099 /*---------------------------------------------------------------------------*/
00100 /* Macro declarations                                                        */
00101 /*---------------------------------------------------------------------------*/
00102 
00103 
00106 /*---------------------------------------------------------------------------*/
00107 /* Static function prototypes                                                */
00108 /*---------------------------------------------------------------------------*/
00109 
00110 
00114 /*---------------------------------------------------------------------------*/
00115 /* Definition of exported functions                                          */
00116 /*---------------------------------------------------------------------------*/
00117 
00133 DdNode *
00134 Cudd_addApply(
00135   DdManager * dd,
00136   DD_AOP op,
00137   DdNode * f,
00138   DdNode * g)
00139 {
00140     DdNode *res;
00141 
00142     do {
00143         dd->reordered = 0;
00144         res = cuddAddApplyRecur(dd,op,f,g);
00145     } while (dd->reordered == 1);
00146     return(res);
00147 
00148 } /* end of Cudd_addApply */
00149 
00150 
00163 DdNode *
00164 Cudd_addPlus(
00165   DdManager * dd,
00166   DdNode ** f,
00167   DdNode ** g)
00168 {
00169     DdNode *res;
00170     DdNode *F, *G;
00171     CUDD_VALUE_TYPE value;
00172 
00173     F = *f; G = *g;
00174     if (F == DD_ZERO(dd)) return(G);
00175     if (G == DD_ZERO(dd)) return(F);
00176     if (cuddIsConstant(F) && cuddIsConstant(G)) {
00177         value = cuddV(F)+cuddV(G);
00178         res = cuddUniqueConst(dd,value);
00179         return(res);
00180     }
00181     if (F > G) { /* swap f and g */
00182         *f = G;
00183         *g = F;
00184     }
00185     return(NULL);
00186 
00187 } /* end of Cudd_addPlus */
00188 
00189 
00203 DdNode *
00204 Cudd_addTimes(
00205   DdManager * dd,
00206   DdNode ** f,
00207   DdNode ** g)
00208 {
00209     DdNode *res;
00210     DdNode *F, *G;
00211     CUDD_VALUE_TYPE value;
00212 
00213     F = *f; G = *g;
00214     if (F == DD_ZERO(dd) || G == DD_ZERO(dd)) return(DD_ZERO(dd));
00215     if (F == DD_ONE(dd)) return(G);
00216     if (G == DD_ONE(dd)) return(F);
00217     if (cuddIsConstant(F) && cuddIsConstant(G)) {
00218         value = cuddV(F)*cuddV(G);
00219         res = cuddUniqueConst(dd,value);
00220         return(res);
00221     }
00222     if (F > G) { /* swap f and g */
00223         *f = G;
00224         *g = F;
00225     }
00226     return(NULL);
00227 
00228 } /* end of Cudd_addTimes */
00229 
00230 
00243 DdNode *
00244 Cudd_addThreshold(
00245   DdManager * dd,
00246   DdNode ** f,
00247   DdNode ** g)
00248 {
00249     DdNode *F, *G;
00250 
00251     F = *f; G = *g;
00252     if (F == G || F == DD_PLUS_INFINITY(dd)) return(F);
00253     if (cuddIsConstant(F) && cuddIsConstant(G)) {
00254         if (cuddV(F) >= cuddV(G)) {
00255             return(F);
00256         } else {
00257             return(DD_ZERO(dd));
00258         }
00259     }
00260     return(NULL);
00261 
00262 } /* end of Cudd_addThreshold */
00263 
00264 
00277 DdNode *
00278 Cudd_addSetNZ(
00279   DdManager * dd,
00280   DdNode ** f,
00281   DdNode ** g)
00282 {
00283     DdNode *F, *G;
00284 
00285     F = *f; G = *g;
00286     if (F == G) return(F);
00287     if (F == DD_ZERO(dd)) return(G);
00288     if (G == DD_ZERO(dd)) return(F);
00289     if (cuddIsConstant(G)) return(G);
00290     return(NULL);
00291 
00292 } /* end of Cudd_addSetNZ */
00293 
00294 
00307 DdNode *
00308 Cudd_addDivide(
00309   DdManager * dd,
00310   DdNode ** f,
00311   DdNode ** g)
00312 {
00313     DdNode *res;
00314     DdNode *F, *G;
00315     CUDD_VALUE_TYPE value;
00316 
00317     F = *f; G = *g;
00318     /* We would like to use F == G -> F/G == 1, but F and G may
00319     ** contain zeroes. */
00320     if (F == DD_ZERO(dd)) return(DD_ZERO(dd));
00321     if (G == DD_ONE(dd)) return(F);
00322     if (cuddIsConstant(F) && cuddIsConstant(G)) {
00323         value = cuddV(F)/cuddV(G);
00324         res = cuddUniqueConst(dd,value);
00325         return(res);
00326     }
00327     return(NULL);
00328 
00329 } /* end of Cudd_addDivide */
00330 
00331 
00344 DdNode *
00345 Cudd_addMinus(
00346   DdManager * dd,
00347   DdNode ** f,
00348   DdNode ** g)
00349 {
00350     DdNode *res;
00351     DdNode *F, *G;
00352     CUDD_VALUE_TYPE value;
00353 
00354     F = *f; G = *g;
00355     if (F == G) return(DD_ZERO(dd));
00356     if (F == DD_ZERO(dd)) return(cuddAddNegateRecur(dd,G));
00357     if (G == DD_ZERO(dd)) return(F);
00358     if (cuddIsConstant(F) && cuddIsConstant(G)) {
00359         value = cuddV(F)-cuddV(G);
00360         res = cuddUniqueConst(dd,value);
00361         return(res);
00362     }
00363     return(NULL);
00364 
00365 } /* end of Cudd_addMinus */
00366 
00367 
00380 DdNode *
00381 Cudd_addMinimum(
00382   DdManager * dd,
00383   DdNode ** f,
00384   DdNode ** g)
00385 {
00386     DdNode *F, *G;
00387 
00388     F = *f; G = *g;
00389     if (F == DD_PLUS_INFINITY(dd)) return(G);
00390     if (G == DD_PLUS_INFINITY(dd)) return(F);
00391     if (F == G) return(F);
00392 #if 0
00393     /* These special cases probably do not pay off. */
00394     if (F == DD_MINUS_INFINITY(dd)) return(F);
00395     if (G == DD_MINUS_INFINITY(dd)) return(G);
00396 #endif
00397     if (cuddIsConstant(F) && cuddIsConstant(G)) {
00398         if (cuddV(F) <= cuddV(G)) {
00399             return(F);
00400         } else {
00401             return(G);
00402         }
00403     }
00404     if (F > G) { /* swap f and g */
00405         *f = G;
00406         *g = F;
00407     }
00408     return(NULL);
00409 
00410 } /* end of Cudd_addMinimum */
00411 
00412 
00425 DdNode *
00426 Cudd_addMaximum(
00427   DdManager * dd,
00428   DdNode ** f,
00429   DdNode ** g)
00430 {
00431     DdNode *F, *G;
00432 
00433     F = *f; G = *g;
00434     if (F == G) return(F);
00435     if (F == DD_MINUS_INFINITY(dd)) return(G);
00436     if (G == DD_MINUS_INFINITY(dd)) return(F);
00437 #if 0
00438     /* These special cases probably do not pay off. */
00439     if (F == DD_PLUS_INFINITY(dd)) return(F);
00440     if (G == DD_PLUS_INFINITY(dd)) return(G);
00441 #endif
00442     if (cuddIsConstant(F) && cuddIsConstant(G)) {
00443         if (cuddV(F) >= cuddV(G)) {
00444             return(F);
00445         } else {
00446             return(G);
00447         }
00448     }
00449     if (F > G) { /* swap f and g */
00450         *f = G;
00451         *g = F;
00452     }
00453     return(NULL);
00454 
00455 } /* end of Cudd_addMaximum */
00456 
00457 
00471 DdNode *
00472 Cudd_addOneZeroMaximum(
00473   DdManager * dd,
00474   DdNode ** f,
00475   DdNode ** g)
00476 {
00477 
00478     if (*f == *g) return(DD_ZERO(dd));
00479     if (*g == DD_PLUS_INFINITY(dd))
00480         return DD_ZERO(dd);
00481     if (cuddIsConstant(*f) && cuddIsConstant(*g)) {
00482         if (cuddV(*f) > cuddV(*g)) {
00483             return(DD_ONE(dd));
00484         } else {
00485             return(DD_ZERO(dd));
00486         }
00487     }
00488 
00489     return(NULL);
00490 
00491 } /* end of Cudd_addOneZeroMaximum */
00492 
00493 
00506 DdNode *
00507 Cudd_addDiff(
00508   DdManager * dd,
00509   DdNode ** f,
00510   DdNode ** g)
00511 {
00512     DdNode *F, *G;
00513 
00514     F = *f; G = *g;
00515     if (F == G) return(DD_PLUS_INFINITY(dd));
00516     if (F == DD_PLUS_INFINITY(dd)) return(G);
00517     if (G == DD_PLUS_INFINITY(dd)) return(F);
00518     if (cuddIsConstant(F) && cuddIsConstant(G)) {
00519         if (cuddV(F) != cuddV(G)) {
00520             if (cuddV(F) < cuddV(G)) {
00521                 return(F);
00522             } else {
00523                 return(G);
00524             }
00525         } else {
00526             return(DD_PLUS_INFINITY(dd));
00527         }
00528     }
00529     return(NULL);
00530 
00531 } /* end of Cudd_addDiff */
00532 
00533 
00546 DdNode *
00547 Cudd_addAgreement(
00548   DdManager * dd,
00549   DdNode ** f,
00550   DdNode ** g)
00551 {
00552     DdNode *F, *G;
00553 
00554     F = *f; G = *g;
00555     if (F == G) return(F);
00556     if (F == dd->background) return(F);
00557     if (G == dd->background) return(G);
00558     if (cuddIsConstant(F) && cuddIsConstant(G)) return(dd->background);
00559     return(NULL);
00560 
00561 } /* end of Cudd_addAgreement */
00562 
00563 
00576 DdNode *
00577 Cudd_addOr(
00578   DdManager * dd,
00579   DdNode ** f,
00580   DdNode ** g)
00581 {
00582     DdNode *F, *G;
00583 
00584     F = *f; G = *g;
00585     if (F == DD_ONE(dd) || G == DD_ONE(dd)) return(DD_ONE(dd));
00586     if (cuddIsConstant(F)) return(G);
00587     if (cuddIsConstant(G)) return(F);
00588     if (F == G) return(F);
00589     if (F > G) { /* swap f and g */
00590         *f = G;
00591         *g = F;
00592     }
00593     return(NULL);
00594 
00595 } /* end of Cudd_addOr */
00596 
00597 
00610 DdNode *
00611 Cudd_addNand(
00612   DdManager * dd,
00613   DdNode ** f,
00614   DdNode ** g)
00615 {
00616     DdNode *F, *G;
00617 
00618     F = *f; G = *g;
00619     if (F == DD_ZERO(dd) || G == DD_ZERO(dd)) return(DD_ONE(dd));
00620     if (cuddIsConstant(F) && cuddIsConstant(G)) return(DD_ZERO(dd));
00621     if (F > G) { /* swap f and g */
00622         *f = G;
00623         *g = F;
00624     }
00625     return(NULL);
00626 
00627 } /* end of Cudd_addNand */
00628 
00629 
00642 DdNode *
00643 Cudd_addNor(
00644   DdManager * dd,
00645   DdNode ** f,
00646   DdNode ** g)
00647 {
00648     DdNode *F, *G;
00649 
00650     F = *f; G = *g;
00651     if (F == DD_ONE(dd) || G == DD_ONE(dd)) return(DD_ZERO(dd));
00652     if (cuddIsConstant(F) && cuddIsConstant(G)) return(DD_ONE(dd));
00653     if (F > G) { /* swap f and g */
00654         *f = G;
00655         *g = F;
00656     }
00657     return(NULL);
00658 
00659 } /* end of Cudd_addNor */
00660 
00661 
00674 DdNode *
00675 Cudd_addXor(
00676   DdManager * dd,
00677   DdNode ** f,
00678   DdNode ** g)
00679 {
00680     DdNode *F, *G;
00681 
00682     F = *f; G = *g;
00683     if (F == G) return(DD_ZERO(dd));
00684     if (F == DD_ONE(dd) && G == DD_ZERO(dd)) return(DD_ONE(dd));
00685     if (G == DD_ONE(dd) && F == DD_ZERO(dd)) return(DD_ONE(dd));
00686     if (cuddIsConstant(F) && cuddIsConstant(G)) return(DD_ZERO(dd));
00687     if (F > G) { /* swap f and g */
00688         *f = G;
00689         *g = F;
00690     }
00691     return(NULL);
00692 
00693 } /* end of Cudd_addXor */
00694 
00695 
00708 DdNode *
00709 Cudd_addXnor(
00710   DdManager * dd,
00711   DdNode ** f,
00712   DdNode ** g)
00713 {
00714     DdNode *F, *G;
00715 
00716     F = *f; G = *g;
00717     if (F == G) return(DD_ONE(dd));
00718     if (F == DD_ONE(dd) && G == DD_ONE(dd)) return(DD_ONE(dd));
00719     if (G == DD_ZERO(dd) && F == DD_ZERO(dd)) return(DD_ONE(dd));
00720     if (cuddIsConstant(F) && cuddIsConstant(G)) return(DD_ZERO(dd));
00721     if (F > G) { /* swap f and g */
00722         *f = G;
00723         *g = F;
00724     }
00725     return(NULL);
00726 
00727 } /* end of Cudd_addXnor */
00728 
00729 
00742 DdNode *
00743 Cudd_addMonadicApply(
00744   DdManager * dd,
00745   DD_MAOP op,
00746   DdNode * f)
00747 {
00748     DdNode *res;
00749 
00750     do {
00751         dd->reordered = 0;
00752         res = cuddAddMonadicApplyRecur(dd,op,f);
00753     } while (dd->reordered == 1);
00754     return(res);
00755 
00756 } /* end of Cudd_addMonadicApply */
00757 
00758 
00772 DdNode *
00773 Cudd_addLog(
00774   DdManager * dd,
00775   DdNode * f)
00776 {
00777     if (cuddIsConstant(f)) {
00778         CUDD_VALUE_TYPE value = log(cuddV(f));
00779         DdNode *res = cuddUniqueConst(dd,value);
00780         return(res);
00781     }
00782     return(NULL);
00783 
00784 } /* end of Cudd_addLog */
00785 
00786 
00787 /*---------------------------------------------------------------------------*/
00788 /* Definition of internal functions                                          */
00789 /*---------------------------------------------------------------------------*/
00790 
00791 
00804 DdNode *
00805 cuddAddApplyRecur(
00806   DdManager * dd,
00807   DD_AOP op,
00808   DdNode * f,
00809   DdNode * g)
00810 {
00811     DdNode *res,
00812            *fv, *fvn, *gv, *gvn,
00813            *T, *E;
00814     unsigned int ford, gord;
00815     unsigned int index;
00816     DD_CTFP cacheOp;
00817 
00818     /* Check terminal cases. Op may swap f and g to increase the
00819      * cache hit rate.
00820      */
00821     statLine(dd);
00822     res = (*op)(dd,&f,&g);
00823     if (res != NULL) return(res);
00824 
00825     /* Check cache. */
00826     cacheOp = (DD_CTFP) op;
00827     res = cuddCacheLookup2(dd,cacheOp,f,g);
00828     if (res != NULL) return(res);
00829 
00830     /* Recursive step. */
00831     ford = cuddI(dd,f->index);
00832     gord = cuddI(dd,g->index);
00833     if (ford <= gord) {
00834         index = f->index;
00835         fv = cuddT(f);
00836         fvn = cuddE(f);
00837     } else {
00838         index = g->index;
00839         fv = fvn = f;
00840     }
00841     if (gord <= ford) {
00842         gv = cuddT(g);
00843         gvn = cuddE(g);
00844     } else {
00845         gv = gvn = g;
00846     }
00847 
00848     T = cuddAddApplyRecur(dd,op,fv,gv);
00849     if (T == NULL) return(NULL);
00850     cuddRef(T);
00851 
00852     E = cuddAddApplyRecur(dd,op,fvn,gvn);
00853     if (E == NULL) {
00854         Cudd_RecursiveDeref(dd,T);
00855         return(NULL);
00856     }
00857     cuddRef(E);
00858 
00859     res = (T == E) ? T : cuddUniqueInter(dd,(int)index,T,E);
00860     if (res == NULL) {
00861         Cudd_RecursiveDeref(dd, T);
00862         Cudd_RecursiveDeref(dd, E);
00863         return(NULL);
00864     }
00865     cuddDeref(T);
00866     cuddDeref(E);
00867 
00868     /* Store result. */
00869     cuddCacheInsert2(dd,cacheOp,f,g,res);
00870 
00871     return(res);
00872 
00873 } /* end of cuddAddApplyRecur */
00874 
00875 
00888 DdNode *
00889 cuddAddMonadicApplyRecur(
00890   DdManager * dd,
00891   DD_MAOP op,
00892   DdNode * f)
00893 {
00894     DdNode *res, *ft, *fe, *T, *E;
00895     unsigned int index;
00896 
00897     /* Check terminal cases. */
00898     statLine(dd);
00899     res = (*op)(dd,f);
00900     if (res != NULL) return(res);
00901 
00902     /* Check cache. */
00903     res = cuddCacheLookup1(dd,op,f);
00904     if (res != NULL) return(res);
00905 
00906     /* Recursive step. */
00907     index = f->index;
00908     ft = cuddT(f);
00909     fe = cuddE(f);
00910 
00911     T = cuddAddMonadicApplyRecur(dd,op,ft);
00912     if (T == NULL) return(NULL);
00913     cuddRef(T);
00914 
00915     E = cuddAddMonadicApplyRecur(dd,op,fe);
00916     if (E == NULL) {
00917         Cudd_RecursiveDeref(dd,T);
00918         return(NULL);
00919     }
00920     cuddRef(E);
00921 
00922     res = (T == E) ? T : cuddUniqueInter(dd,(int)index,T,E);
00923     if (res == NULL) {
00924         Cudd_RecursiveDeref(dd, T);
00925         Cudd_RecursiveDeref(dd, E);
00926         return(NULL);
00927     }
00928     cuddDeref(T);
00929     cuddDeref(E);
00930 
00931     /* Store result. */
00932     cuddCacheInsert1(dd,op,f,res);
00933 
00934     return(res);
00935 
00936 } /* end of cuddAddMonadicApplyRecur */
00937 
00938 
00939 /*---------------------------------------------------------------------------*/
00940 /* Definition of static functions                                            */
00941 /*---------------------------------------------------------------------------*/