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

00001 
00035 #include        "util_hack.h"
00036 #include        "cuddInt.h"
00037 
00038 /*---------------------------------------------------------------------------*/
00039 /* Constant declarations                                                     */
00040 /*---------------------------------------------------------------------------*/
00041 
00042 
00043 /*---------------------------------------------------------------------------*/
00044 /* Stucture declarations                                                     */
00045 /*---------------------------------------------------------------------------*/
00046 
00047 
00048 /*---------------------------------------------------------------------------*/
00049 /* Type declarations                                                         */
00050 /*---------------------------------------------------------------------------*/
00051 
00052 
00053 /*---------------------------------------------------------------------------*/
00054 /* Variable declarations                                                     */
00055 /*---------------------------------------------------------------------------*/
00056 
00057 #ifndef lint
00058 static char rcsid[] DD_UNUSED = "$Id: cuddAddAbs.c,v 1.1.1.1 2003/02/24 22:23:50 wjiang Exp $";
00059 #endif
00060 
00061 static  DdNode  *two;
00062 
00063 /*---------------------------------------------------------------------------*/
00064 /* Macro declarations                                                        */
00065 /*---------------------------------------------------------------------------*/
00066 
00067 
00070 /*---------------------------------------------------------------------------*/
00071 /* Static function prototypes                                                */
00072 /*---------------------------------------------------------------------------*/
00073 
00074 static int addCheckPositiveCube ARGS((DdManager *manager, DdNode *cube));
00075 
00079 /*---------------------------------------------------------------------------*/
00080 /* Definition of exported functions                                          */
00081 /*---------------------------------------------------------------------------*/
00082 
00097 DdNode *
00098 Cudd_addExistAbstract(
00099   DdManager * manager,
00100   DdNode * f,
00101   DdNode * cube)
00102 {
00103     DdNode *res;
00104 
00105     two = cuddUniqueConst(manager,(CUDD_VALUE_TYPE) 2);
00106     if (two == NULL) return(NULL);
00107     cuddRef(two);
00108 
00109     if (addCheckPositiveCube(manager, cube) == 0) {
00110         (void) fprintf(manager->err,"Error: Can only abstract cubes");
00111         return(NULL);
00112     }
00113 
00114     do {
00115         manager->reordered = 0;
00116         res = cuddAddExistAbstractRecur(manager, f, cube);
00117     } while (manager->reordered == 1);
00118 
00119     if (res == NULL) {
00120         Cudd_RecursiveDeref(manager,two);
00121         return(NULL);
00122     }
00123     cuddRef(res);
00124     Cudd_RecursiveDeref(manager,two);
00125     cuddDeref(res);
00126 
00127     return(res);
00128 
00129 } /* end of Cudd_addExistAbstract */
00130 
00131 
00146 DdNode *
00147 Cudd_addUnivAbstract(
00148   DdManager * manager,
00149   DdNode * f,
00150   DdNode * cube)
00151 {
00152     DdNode              *res;
00153 
00154     if (addCheckPositiveCube(manager, cube) == 0) {
00155         (void) fprintf(manager->err,"Error:  Can only abstract cubes");
00156         return(NULL);
00157     }
00158 
00159     do {
00160         manager->reordered = 0;
00161         res = cuddAddUnivAbstractRecur(manager, f, cube);
00162     } while (manager->reordered == 1);
00163 
00164     return(res);
00165 
00166 } /* end of Cudd_addUnivAbstract */
00167 
00168 
00184 DdNode *
00185 Cudd_addOrAbstract(
00186   DdManager * manager,
00187   DdNode * f,
00188   DdNode * cube)
00189 {
00190     DdNode *res;
00191 
00192     if (addCheckPositiveCube(manager, cube) == 0) {
00193         (void) fprintf(manager->err,"Error: Can only abstract cubes");
00194         return(NULL);
00195     }
00196 
00197     do {
00198         manager->reordered = 0;
00199         res = cuddAddOrAbstractRecur(manager, f, cube);
00200     } while (manager->reordered == 1);
00201     return(res);
00202 
00203 } /* end of Cudd_addOrAbstract */
00204 
00205 
00206 /*---------------------------------------------------------------------------*/
00207 /* Definition of internal functions                                          */
00208 /*---------------------------------------------------------------------------*/
00209 
00210 
00224 DdNode *
00225 cuddAddExistAbstractRecur(
00226   DdManager * manager,
00227   DdNode * f,
00228   DdNode * cube)
00229 {
00230     DdNode      *T, *E, *res, *res1, *res2, *zero;
00231 
00232     statLine(manager);
00233     zero = DD_ZERO(manager);
00234 
00235     /* Cube is guaranteed to be a cube at this point. */        
00236     if (f == zero || cuddIsConstant(cube)) {  
00237         return(f);
00238     }
00239 
00240     /* Abstract a variable that does not appear in f => multiply by 2. */
00241     if (cuddI(manager,f->index) > cuddI(manager,cube->index)) {
00242         res1 = cuddAddExistAbstractRecur(manager, f, cuddT(cube));
00243         if (res1 == NULL) return(NULL);
00244         cuddRef(res1);
00245         /* Use the "internal" procedure to be alerted in case of
00246         ** dynamic reordering. If dynamic reordering occurs, we
00247         ** have to abort the entire abstraction.
00248         */
00249         res = cuddAddApplyRecur(manager,Cudd_addTimes,res1,two);
00250         if (res == NULL) {
00251             Cudd_RecursiveDeref(manager,res1);
00252             return(NULL);
00253         }
00254         cuddRef(res);
00255         Cudd_RecursiveDeref(manager,res1);
00256         cuddDeref(res);
00257         return(res);
00258     }
00259 
00260     if ((res = cuddCacheLookup2(manager, Cudd_addExistAbstract, f, cube)) != NULL) {
00261         return(res);
00262     }
00263 
00264     T = cuddT(f);
00265     E = cuddE(f);
00266 
00267     /* If the two indices are the same, so are their levels. */
00268     if (f->index == cube->index) {
00269         res1 = cuddAddExistAbstractRecur(manager, T, cuddT(cube));
00270         if (res1 == NULL) return(NULL);
00271         cuddRef(res1);
00272         res2 = cuddAddExistAbstractRecur(manager, E, cuddT(cube));
00273         if (res2 == NULL) {
00274             Cudd_RecursiveDeref(manager,res1);
00275             return(NULL);
00276         }
00277         cuddRef(res2);
00278         res = cuddAddApplyRecur(manager, Cudd_addPlus, res1, res2);
00279         if (res == NULL) {
00280             Cudd_RecursiveDeref(manager,res1);
00281             Cudd_RecursiveDeref(manager,res2);
00282             return(NULL);
00283         }
00284         cuddRef(res);
00285         Cudd_RecursiveDeref(manager,res1);
00286         Cudd_RecursiveDeref(manager,res2);
00287         cuddCacheInsert2(manager, Cudd_addExistAbstract, f, cube, res);
00288         cuddDeref(res);
00289         return(res);
00290     } else { /* if (cuddI(manager,f->index) < cuddI(manager,cube->index)) */
00291         res1 = cuddAddExistAbstractRecur(manager, T, cube);
00292         if (res1 == NULL) return(NULL);
00293         cuddRef(res1);
00294         res2 = cuddAddExistAbstractRecur(manager, E, cube);
00295         if (res2 == NULL) {
00296             Cudd_RecursiveDeref(manager,res1);
00297             return(NULL);
00298         }
00299         cuddRef(res2);
00300         res = (res1 == res2) ? res1 :
00301             cuddUniqueInter(manager, (int) f->index, res1, res2);
00302         if (res == NULL) {
00303             Cudd_RecursiveDeref(manager,res1);
00304             Cudd_RecursiveDeref(manager,res2);
00305             return(NULL);
00306         }
00307         cuddDeref(res1);
00308         cuddDeref(res2);
00309         cuddCacheInsert2(manager, Cudd_addExistAbstract, f, cube, res);
00310         return(res);
00311     }       
00312 
00313 } /* end of cuddAddExistAbstractRecur */
00314 
00315 
00329 DdNode *
00330 cuddAddUnivAbstractRecur(
00331   DdManager * manager,
00332   DdNode * f,
00333   DdNode * cube)
00334 {
00335     DdNode      *T, *E, *res, *res1, *res2, *one, *zero;
00336 
00337     statLine(manager);
00338     one = DD_ONE(manager);
00339     zero = DD_ZERO(manager);
00340 
00341     /* Cube is guaranteed to be a cube at this point.
00342     ** zero and one are the only constatnts c such that c*c=c.
00343     */
00344     if (f == zero || f == one || cube == one) {  
00345         return(f);
00346     }
00347 
00348     /* Abstract a variable that does not appear in f. */
00349     if (cuddI(manager,f->index) > cuddI(manager,cube->index)) {
00350         res1 = cuddAddUnivAbstractRecur(manager, f, cuddT(cube));
00351         if (res1 == NULL) return(NULL);
00352         cuddRef(res1);
00353         /* Use the "internal" procedure to be alerted in case of
00354         ** dynamic reordering. If dynamic reordering occurs, we
00355         ** have to abort the entire abstraction.
00356         */
00357         res = cuddAddApplyRecur(manager, Cudd_addTimes, res1, res1);
00358         if (res == NULL) {
00359             Cudd_RecursiveDeref(manager,res1);
00360             return(NULL);
00361         }
00362         cuddRef(res);
00363         Cudd_RecursiveDeref(manager,res1);
00364         cuddDeref(res);
00365         return(res);
00366     }
00367 
00368     if ((res = cuddCacheLookup2(manager, Cudd_addUnivAbstract, f, cube)) != NULL) {
00369         return(res);
00370     }
00371 
00372     T = cuddT(f);
00373     E = cuddE(f);
00374 
00375     /* If the two indices are the same, so are their levels. */
00376     if (f->index == cube->index) {
00377         res1 = cuddAddUnivAbstractRecur(manager, T, cuddT(cube));
00378         if (res1 == NULL) return(NULL);
00379         cuddRef(res1);
00380         res2 = cuddAddUnivAbstractRecur(manager, E, cuddT(cube));
00381         if (res2 == NULL) {
00382             Cudd_RecursiveDeref(manager,res1);
00383             return(NULL);
00384         }
00385         cuddRef(res2);
00386         res = cuddAddApplyRecur(manager, Cudd_addTimes, res1, res2);
00387         if (res == NULL) {
00388             Cudd_RecursiveDeref(manager,res1);
00389             Cudd_RecursiveDeref(manager,res2);
00390             return(NULL);
00391         }
00392         cuddRef(res);
00393         Cudd_RecursiveDeref(manager,res1);
00394         Cudd_RecursiveDeref(manager,res2);
00395         cuddCacheInsert2(manager, Cudd_addUnivAbstract, f, cube, res);
00396         cuddDeref(res);
00397         return(res);
00398     } else { /* if (cuddI(manager,f->index) < cuddI(manager,cube->index)) */
00399         res1 = cuddAddUnivAbstractRecur(manager, T, cube);
00400         if (res1 == NULL) return(NULL);
00401         cuddRef(res1);
00402         res2 = cuddAddUnivAbstractRecur(manager, E, cube);
00403         if (res2 == NULL) {
00404             Cudd_RecursiveDeref(manager,res1);
00405             return(NULL);
00406         }
00407         cuddRef(res2);
00408         res = (res1 == res2) ? res1 :
00409             cuddUniqueInter(manager, (int) f->index, res1, res2);
00410         if (res == NULL) {
00411             Cudd_RecursiveDeref(manager,res1);
00412             Cudd_RecursiveDeref(manager,res2);
00413             return(NULL);
00414         }
00415         cuddDeref(res1);
00416         cuddDeref(res2);
00417         cuddCacheInsert2(manager, Cudd_addUnivAbstract, f, cube, res);
00418         return(res);
00419     }
00420 
00421 } /* end of cuddAddUnivAbstractRecur */
00422 
00423 
00437 DdNode *
00438 cuddAddOrAbstractRecur(
00439   DdManager * manager,
00440   DdNode * f,
00441   DdNode * cube)
00442 {
00443     DdNode      *T, *E, *res, *res1, *res2, *one;
00444 
00445     statLine(manager);
00446     one = DD_ONE(manager);
00447 
00448     /* Cube is guaranteed to be a cube at this point. */
00449     if (cuddIsConstant(f) || cube == one) {  
00450         return(f);
00451     }
00452 
00453     /* Abstract a variable that does not appear in f. */
00454     if (cuddI(manager,f->index) > cuddI(manager,cube->index)) {
00455         res1 = cuddAddOrAbstractRecur(manager, f, cuddT(cube));
00456         if (res1 == NULL) return(NULL);
00457         cuddRef(res1);
00458         /* Use the "internal" procedure to be alerted in case of
00459         ** dynamic reordering. If dynamic reordering occurs, we
00460         ** have to abort the entire abstraction.
00461         */
00462         res = cuddAddApplyRecur(manager, Cudd_addOr, res1, res1);
00463         if (res == NULL) {
00464             Cudd_RecursiveDeref(manager,res1);
00465             return(NULL);
00466         }
00467         cuddRef(res);
00468         Cudd_RecursiveDeref(manager,res1);
00469         cuddDeref(res);
00470         return(res);
00471     }
00472 
00473     if ((res = cuddCacheLookup2(manager, Cudd_addOrAbstract, f, cube)) != NULL) {
00474         return(res);
00475     }
00476 
00477     T = cuddT(f);
00478     E = cuddE(f);
00479 
00480     /* If the two indices are the same, so are their levels. */
00481     if (f->index == cube->index) {
00482         res1 = cuddAddOrAbstractRecur(manager, T, cuddT(cube));
00483         if (res1 == NULL) return(NULL);
00484         cuddRef(res1);
00485         if (res1 != one) {
00486             res2 = cuddAddOrAbstractRecur(manager, E, cuddT(cube));
00487             if (res2 == NULL) {
00488                 Cudd_RecursiveDeref(manager,res1);
00489                 return(NULL);
00490             }
00491             cuddRef(res2);
00492             res = cuddAddApplyRecur(manager, Cudd_addOr, res1, res2);
00493             if (res == NULL) {
00494                 Cudd_RecursiveDeref(manager,res1);
00495                 Cudd_RecursiveDeref(manager,res2);
00496                 return(NULL);
00497             }
00498             cuddRef(res);
00499             Cudd_RecursiveDeref(manager,res1);
00500             Cudd_RecursiveDeref(manager,res2);
00501         } else {
00502             res = res1;
00503         }
00504         cuddCacheInsert2(manager, Cudd_addOrAbstract, f, cube, res);
00505         cuddDeref(res);
00506         return(res);
00507     } else { /* if (cuddI(manager,f->index) < cuddI(manager,cube->index)) */
00508         res1 = cuddAddOrAbstractRecur(manager, T, cube);
00509         if (res1 == NULL) return(NULL);
00510         cuddRef(res1);
00511         res2 = cuddAddOrAbstractRecur(manager, E, cube);
00512         if (res2 == NULL) {
00513             Cudd_RecursiveDeref(manager,res1);
00514             return(NULL);
00515         }
00516         cuddRef(res2);
00517         res = (res1 == res2) ? res1 :
00518             cuddUniqueInter(manager, (int) f->index, res1, res2);
00519         if (res == NULL) {
00520             Cudd_RecursiveDeref(manager,res1);
00521             Cudd_RecursiveDeref(manager,res2);
00522             return(NULL);
00523         }
00524         cuddDeref(res1);
00525         cuddDeref(res2);
00526         cuddCacheInsert2(manager, Cudd_addOrAbstract, f, cube, res);
00527         return(res);
00528     }
00529 
00530 } /* end of cuddAddOrAbstractRecur */
00531 
00532 
00533 
00534 /*---------------------------------------------------------------------------*/
00535 /* Definition of static functions                                            */
00536 /*---------------------------------------------------------------------------*/
00537 
00538 
00552 static int
00553 addCheckPositiveCube(
00554   DdManager * manager,
00555   DdNode * cube)
00556 {
00557     if (Cudd_IsComplement(cube)) return(0);
00558     if (cube == DD_ONE(manager)) return(1);
00559     if (cuddIsConstant(cube)) return(0);
00560     if (cuddE(cube) == DD_ZERO(manager)) {
00561         return(addCheckPositiveCube(manager, cuddT(cube)));
00562     }
00563     return(0);
00564 
00565 } /* end of addCheckPositiveCube */
00566