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

00001 
00062 #include "util.h"
00063 #include "cuddInt.h"
00064 
00065 /*---------------------------------------------------------------------------*/
00066 /* Constant declarations                                                     */
00067 /*---------------------------------------------------------------------------*/
00068 
00069 
00070 /*---------------------------------------------------------------------------*/
00071 /* Stucture declarations                                                     */
00072 /*---------------------------------------------------------------------------*/
00073 
00074 
00075 /*---------------------------------------------------------------------------*/
00076 /* Type declarations                                                         */
00077 /*---------------------------------------------------------------------------*/
00078 
00079 
00080 /*---------------------------------------------------------------------------*/
00081 /* Variable declarations                                                     */
00082 /*---------------------------------------------------------------------------*/
00083 
00084 #ifndef lint
00085 static char rcsid[] DD_UNUSED = "$Id: cuddAddAbs.c,v 1.15 2004/08/13 18:04:45 fabio Exp $";
00086 #endif
00087 
00088 static  DdNode  *two;
00089 
00090 /*---------------------------------------------------------------------------*/
00091 /* Macro declarations                                                        */
00092 /*---------------------------------------------------------------------------*/
00093 
00094 
00097 /*---------------------------------------------------------------------------*/
00098 /* Static function prototypes                                                */
00099 /*---------------------------------------------------------------------------*/
00100 
00101 static int addCheckPositiveCube (DdManager *manager, DdNode *cube);
00102 
00106 /*---------------------------------------------------------------------------*/
00107 /* Definition of exported functions                                          */
00108 /*---------------------------------------------------------------------------*/
00109 
00124 DdNode *
00125 Cudd_addExistAbstract(
00126   DdManager * manager,
00127   DdNode * f,
00128   DdNode * cube)
00129 {
00130     DdNode *res;
00131 
00132     two = cuddUniqueConst(manager,(CUDD_VALUE_TYPE) 2);
00133     if (two == NULL) return(NULL);
00134     cuddRef(two);
00135 
00136     if (addCheckPositiveCube(manager, cube) == 0) {
00137         (void) fprintf(manager->err,"Error: Can only abstract cubes");
00138         return(NULL);
00139     }
00140 
00141     do {
00142         manager->reordered = 0;
00143         res = cuddAddExistAbstractRecur(manager, f, cube);
00144     } while (manager->reordered == 1);
00145 
00146     if (res == NULL) {
00147         Cudd_RecursiveDeref(manager,two);
00148         return(NULL);
00149     }
00150     cuddRef(res);
00151     Cudd_RecursiveDeref(manager,two);
00152     cuddDeref(res);
00153 
00154     return(res);
00155 
00156 } /* end of Cudd_addExistAbstract */
00157 
00158 
00173 DdNode *
00174 Cudd_addUnivAbstract(
00175   DdManager * manager,
00176   DdNode * f,
00177   DdNode * cube)
00178 {
00179     DdNode              *res;
00180 
00181     if (addCheckPositiveCube(manager, cube) == 0) {
00182         (void) fprintf(manager->err,"Error:  Can only abstract cubes");
00183         return(NULL);
00184     }
00185 
00186     do {
00187         manager->reordered = 0;
00188         res = cuddAddUnivAbstractRecur(manager, f, cube);
00189     } while (manager->reordered == 1);
00190 
00191     return(res);
00192 
00193 } /* end of Cudd_addUnivAbstract */
00194 
00195 
00211 DdNode *
00212 Cudd_addOrAbstract(
00213   DdManager * manager,
00214   DdNode * f,
00215   DdNode * cube)
00216 {
00217     DdNode *res;
00218 
00219     if (addCheckPositiveCube(manager, cube) == 0) {
00220         (void) fprintf(manager->err,"Error: Can only abstract cubes");
00221         return(NULL);
00222     }
00223 
00224     do {
00225         manager->reordered = 0;
00226         res = cuddAddOrAbstractRecur(manager, f, cube);
00227     } while (manager->reordered == 1);
00228     return(res);
00229 
00230 } /* end of Cudd_addOrAbstract */
00231 
00232 
00233 /*---------------------------------------------------------------------------*/
00234 /* Definition of internal functions                                          */
00235 /*---------------------------------------------------------------------------*/
00236 
00237 
00251 DdNode *
00252 cuddAddExistAbstractRecur(
00253   DdManager * manager,
00254   DdNode * f,
00255   DdNode * cube)
00256 {
00257     DdNode      *T, *E, *res, *res1, *res2, *zero;
00258 
00259     statLine(manager);
00260     zero = DD_ZERO(manager);
00261 
00262     /* Cube is guaranteed to be a cube at this point. */        
00263     if (f == zero || cuddIsConstant(cube)) {  
00264         return(f);
00265     }
00266 
00267     /* Abstract a variable that does not appear in f => multiply by 2. */
00268     if (cuddI(manager,f->index) > cuddI(manager,cube->index)) {
00269         res1 = cuddAddExistAbstractRecur(manager, f, cuddT(cube));
00270         if (res1 == NULL) return(NULL);
00271         cuddRef(res1);
00272         /* Use the "internal" procedure to be alerted in case of
00273         ** dynamic reordering. If dynamic reordering occurs, we
00274         ** have to abort the entire abstraction.
00275         */
00276         res = cuddAddApplyRecur(manager,Cudd_addTimes,res1,two);
00277         if (res == NULL) {
00278             Cudd_RecursiveDeref(manager,res1);
00279             return(NULL);
00280         }
00281         cuddRef(res);
00282         Cudd_RecursiveDeref(manager,res1);
00283         cuddDeref(res);
00284         return(res);
00285     }
00286 
00287     if ((res = cuddCacheLookup2(manager, Cudd_addExistAbstract, f, cube)) != NULL) {
00288         return(res);
00289     }
00290 
00291     T = cuddT(f);
00292     E = cuddE(f);
00293 
00294     /* If the two indices are the same, so are their levels. */
00295     if (f->index == cube->index) {
00296         res1 = cuddAddExistAbstractRecur(manager, T, cuddT(cube));
00297         if (res1 == NULL) return(NULL);
00298         cuddRef(res1);
00299         res2 = cuddAddExistAbstractRecur(manager, E, cuddT(cube));
00300         if (res2 == NULL) {
00301             Cudd_RecursiveDeref(manager,res1);
00302             return(NULL);
00303         }
00304         cuddRef(res2);
00305         res = cuddAddApplyRecur(manager, Cudd_addPlus, res1, res2);
00306         if (res == NULL) {
00307             Cudd_RecursiveDeref(manager,res1);
00308             Cudd_RecursiveDeref(manager,res2);
00309             return(NULL);
00310         }
00311         cuddRef(res);
00312         Cudd_RecursiveDeref(manager,res1);
00313         Cudd_RecursiveDeref(manager,res2);
00314         cuddCacheInsert2(manager, Cudd_addExistAbstract, f, cube, res);
00315         cuddDeref(res);
00316         return(res);
00317     } else { /* if (cuddI(manager,f->index) < cuddI(manager,cube->index)) */
00318         res1 = cuddAddExistAbstractRecur(manager, T, cube);
00319         if (res1 == NULL) return(NULL);
00320         cuddRef(res1);
00321         res2 = cuddAddExistAbstractRecur(manager, E, cube);
00322         if (res2 == NULL) {
00323             Cudd_RecursiveDeref(manager,res1);
00324             return(NULL);
00325         }
00326         cuddRef(res2);
00327         res = (res1 == res2) ? res1 :
00328             cuddUniqueInter(manager, (int) f->index, res1, res2);
00329         if (res == NULL) {
00330             Cudd_RecursiveDeref(manager,res1);
00331             Cudd_RecursiveDeref(manager,res2);
00332             return(NULL);
00333         }
00334         cuddDeref(res1);
00335         cuddDeref(res2);
00336         cuddCacheInsert2(manager, Cudd_addExistAbstract, f, cube, res);
00337         return(res);
00338     }       
00339 
00340 } /* end of cuddAddExistAbstractRecur */
00341 
00342 
00356 DdNode *
00357 cuddAddUnivAbstractRecur(
00358   DdManager * manager,
00359   DdNode * f,
00360   DdNode * cube)
00361 {
00362     DdNode      *T, *E, *res, *res1, *res2, *one, *zero;
00363 
00364     statLine(manager);
00365     one = DD_ONE(manager);
00366     zero = DD_ZERO(manager);
00367 
00368     /* Cube is guaranteed to be a cube at this point.
00369     ** zero and one are the only constatnts c such that c*c=c.
00370     */
00371     if (f == zero || f == one || cube == one) {  
00372         return(f);
00373     }
00374 
00375     /* Abstract a variable that does not appear in f. */
00376     if (cuddI(manager,f->index) > cuddI(manager,cube->index)) {
00377         res1 = cuddAddUnivAbstractRecur(manager, f, cuddT(cube));
00378         if (res1 == NULL) return(NULL);
00379         cuddRef(res1);
00380         /* Use the "internal" procedure to be alerted in case of
00381         ** dynamic reordering. If dynamic reordering occurs, we
00382         ** have to abort the entire abstraction.
00383         */
00384         res = cuddAddApplyRecur(manager, Cudd_addTimes, res1, res1);
00385         if (res == NULL) {
00386             Cudd_RecursiveDeref(manager,res1);
00387             return(NULL);
00388         }
00389         cuddRef(res);
00390         Cudd_RecursiveDeref(manager,res1);
00391         cuddDeref(res);
00392         return(res);
00393     }
00394 
00395     if ((res = cuddCacheLookup2(manager, Cudd_addUnivAbstract, f, cube)) != NULL) {
00396         return(res);
00397     }
00398 
00399     T = cuddT(f);
00400     E = cuddE(f);
00401 
00402     /* If the two indices are the same, so are their levels. */
00403     if (f->index == cube->index) {
00404         res1 = cuddAddUnivAbstractRecur(manager, T, cuddT(cube));
00405         if (res1 == NULL) return(NULL);
00406         cuddRef(res1);
00407         res2 = cuddAddUnivAbstractRecur(manager, E, cuddT(cube));
00408         if (res2 == NULL) {
00409             Cudd_RecursiveDeref(manager,res1);
00410             return(NULL);
00411         }
00412         cuddRef(res2);
00413         res = cuddAddApplyRecur(manager, Cudd_addTimes, res1, res2);
00414         if (res == NULL) {
00415             Cudd_RecursiveDeref(manager,res1);
00416             Cudd_RecursiveDeref(manager,res2);
00417             return(NULL);
00418         }
00419         cuddRef(res);
00420         Cudd_RecursiveDeref(manager,res1);
00421         Cudd_RecursiveDeref(manager,res2);
00422         cuddCacheInsert2(manager, Cudd_addUnivAbstract, f, cube, res);
00423         cuddDeref(res);
00424         return(res);
00425     } else { /* if (cuddI(manager,f->index) < cuddI(manager,cube->index)) */
00426         res1 = cuddAddUnivAbstractRecur(manager, T, cube);
00427         if (res1 == NULL) return(NULL);
00428         cuddRef(res1);
00429         res2 = cuddAddUnivAbstractRecur(manager, E, cube);
00430         if (res2 == NULL) {
00431             Cudd_RecursiveDeref(manager,res1);
00432             return(NULL);
00433         }
00434         cuddRef(res2);
00435         res = (res1 == res2) ? res1 :
00436             cuddUniqueInter(manager, (int) f->index, res1, res2);
00437         if (res == NULL) {
00438             Cudd_RecursiveDeref(manager,res1);
00439             Cudd_RecursiveDeref(manager,res2);
00440             return(NULL);
00441         }
00442         cuddDeref(res1);
00443         cuddDeref(res2);
00444         cuddCacheInsert2(manager, Cudd_addUnivAbstract, f, cube, res);
00445         return(res);
00446     }
00447 
00448 } /* end of cuddAddUnivAbstractRecur */
00449 
00450 
00464 DdNode *
00465 cuddAddOrAbstractRecur(
00466   DdManager * manager,
00467   DdNode * f,
00468   DdNode * cube)
00469 {
00470     DdNode      *T, *E, *res, *res1, *res2, *one;
00471 
00472     statLine(manager);
00473     one = DD_ONE(manager);
00474 
00475     /* Cube is guaranteed to be a cube at this point. */
00476     if (cuddIsConstant(f) || cube == one) {  
00477         return(f);
00478     }
00479 
00480     /* Abstract a variable that does not appear in f. */
00481     if (cuddI(manager,f->index) > cuddI(manager,cube->index)) {
00482         res = cuddAddOrAbstractRecur(manager, f, cuddT(cube));
00483         return(res);
00484     }
00485 
00486     if ((res = cuddCacheLookup2(manager, Cudd_addOrAbstract, f, cube)) != NULL) {
00487         return(res);
00488     }
00489 
00490     T = cuddT(f);
00491     E = cuddE(f);
00492 
00493     /* If the two indices are the same, so are their levels. */
00494     if (f->index == cube->index) {
00495         res1 = cuddAddOrAbstractRecur(manager, T, cuddT(cube));
00496         if (res1 == NULL) return(NULL);
00497         cuddRef(res1);
00498         if (res1 != one) {
00499             res2 = cuddAddOrAbstractRecur(manager, E, cuddT(cube));
00500             if (res2 == NULL) {
00501                 Cudd_RecursiveDeref(manager,res1);
00502                 return(NULL);
00503             }
00504             cuddRef(res2);
00505             res = cuddAddApplyRecur(manager, Cudd_addOr, res1, res2);
00506             if (res == NULL) {
00507                 Cudd_RecursiveDeref(manager,res1);
00508                 Cudd_RecursiveDeref(manager,res2);
00509                 return(NULL);
00510             }
00511             cuddRef(res);
00512             Cudd_RecursiveDeref(manager,res1);
00513             Cudd_RecursiveDeref(manager,res2);
00514         } else {
00515             res = res1;
00516         }
00517         cuddCacheInsert2(manager, Cudd_addOrAbstract, f, cube, res);
00518         cuddDeref(res);
00519         return(res);
00520     } else { /* if (cuddI(manager,f->index) < cuddI(manager,cube->index)) */
00521         res1 = cuddAddOrAbstractRecur(manager, T, cube);
00522         if (res1 == NULL) return(NULL);
00523         cuddRef(res1);
00524         res2 = cuddAddOrAbstractRecur(manager, E, cube);
00525         if (res2 == NULL) {
00526             Cudd_RecursiveDeref(manager,res1);
00527             return(NULL);
00528         }
00529         cuddRef(res2);
00530         res = (res1 == res2) ? res1 :
00531             cuddUniqueInter(manager, (int) f->index, res1, res2);
00532         if (res == NULL) {
00533             Cudd_RecursiveDeref(manager,res1);
00534             Cudd_RecursiveDeref(manager,res2);
00535             return(NULL);
00536         }
00537         cuddDeref(res1);
00538         cuddDeref(res2);
00539         cuddCacheInsert2(manager, Cudd_addOrAbstract, f, cube, res);
00540         return(res);
00541     }
00542 
00543 } /* end of cuddAddOrAbstractRecur */
00544 
00545 
00546 
00547 /*---------------------------------------------------------------------------*/
00548 /* Definition of static functions                                            */
00549 /*---------------------------------------------------------------------------*/
00550 
00551 
00565 static int
00566 addCheckPositiveCube(
00567   DdManager * manager,
00568   DdNode * cube)
00569 {
00570     if (Cudd_IsComplement(cube)) return(0);
00571     if (cube == DD_ONE(manager)) return(1);
00572     if (cuddIsConstant(cube)) return(0);
00573     if (cuddE(cube) == DD_ZERO(manager)) {
00574         return(addCheckPositiveCube(manager, cuddT(cube)));
00575     }
00576     return(0);
00577 
00578 } /* end of addCheckPositiveCube */
00579