src/bdd/cudd/cuddAddAbs.c File Reference

#include "util_hack.h"
#include "cuddInt.h"
Include dependency graph for cuddAddAbs.c:

Go to the source code of this file.

Functions

static int addCheckPositiveCube ARGS ((DdManager *manager, DdNode *cube))
DdNode * Cudd_addExistAbstract (DdManager *manager, DdNode *f, DdNode *cube)
DdNode * Cudd_addUnivAbstract (DdManager *manager, DdNode *f, DdNode *cube)
DdNode * Cudd_addOrAbstract (DdManager *manager, DdNode *f, DdNode *cube)
DdNode * cuddAddExistAbstractRecur (DdManager *manager, DdNode *f, DdNode *cube)
DdNode * cuddAddUnivAbstractRecur (DdManager *manager, DdNode *f, DdNode *cube)
DdNode * cuddAddOrAbstractRecur (DdManager *manager, DdNode *f, DdNode *cube)
static int addCheckPositiveCube (DdManager *manager, DdNode *cube)

Variables

static char rcsid[] DD_UNUSED = "$Id: cuddAddAbs.c,v 1.1.1.1 2003/02/24 22:23:50 wjiang Exp $"
static DdNode * two

Function Documentation

static int addCheckPositiveCube ( DdManager *  manager,
DdNode *  cube 
) [static]

Function********************************************************************

Synopsis [Checks whether cube is an ADD representing the product of positive literals.]

Description [Checks whether cube is an ADD representing the product of positive literals. Returns 1 in case of success; 0 otherwise.]

SideEffects [None]

SeeAlso []

Definition at line 553 of file cuddAddAbs.c.

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 */

static int addCheckPositiveCube ARGS ( (DdManager *manager, DdNode *cube)   )  [static]

AutomaticStart

DdNode* Cudd_addExistAbstract ( DdManager *  manager,
DdNode *  f,
DdNode *  cube 
)

AutomaticEnd Function********************************************************************

Synopsis [Existentially Abstracts all the variables in cube from f.]

Description [Abstracts all the variables in cube from f by summing over all possible values taken by the variables. Returns the abstracted ADD.]

SideEffects [None]

SeeAlso [Cudd_addUnivAbstract Cudd_bddExistAbstract Cudd_addOrAbstract]

Definition at line 98 of file cuddAddAbs.c.

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 */

DdNode* Cudd_addOrAbstract ( DdManager *  manager,
DdNode *  f,
DdNode *  cube 
)

Function********************************************************************

Synopsis [Disjunctively abstracts all the variables in cube from the 0-1 ADD f.]

Description [Abstracts all the variables in cube from the 0-1 ADD f by taking the disjunction over all possible values taken by the variables. Returns the abstracted ADD if successful; NULL otherwise.]

SideEffects [None]

SeeAlso [Cudd_addUnivAbstract Cudd_addExistAbstract]

Definition at line 185 of file cuddAddAbs.c.

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 */

DdNode* Cudd_addUnivAbstract ( DdManager *  manager,
DdNode *  f,
DdNode *  cube 
)

Function********************************************************************

Synopsis [Universally Abstracts all the variables in cube from f.]

Description [Abstracts all the variables in cube from f by taking the product over all possible values taken by the variable. Returns the abstracted ADD if successful; NULL otherwise.]

SideEffects [None]

SeeAlso [Cudd_addExistAbstract Cudd_bddUnivAbstract Cudd_addOrAbstract]

Definition at line 147 of file cuddAddAbs.c.

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 */

DdNode* cuddAddExistAbstractRecur ( DdManager *  manager,
DdNode *  f,
DdNode *  cube 
)

Function********************************************************************

Synopsis [Performs the recursive step of Cudd_addExistAbstract.]

Description [Performs the recursive step of Cudd_addExistAbstract. Returns the ADD obtained by abstracting the variables of cube from f, if successful; NULL otherwise.]

SideEffects [None]

SeeAlso []

Definition at line 225 of file cuddAddAbs.c.

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 */

DdNode* cuddAddOrAbstractRecur ( DdManager *  manager,
DdNode *  f,
DdNode *  cube 
)

Function********************************************************************

Synopsis [Performs the recursive step of Cudd_addOrAbstract.]

Description [Performs the recursive step of Cudd_addOrAbstract. Returns the ADD obtained by abstracting the variables of cube from f, if successful; NULL otherwise.]

SideEffects [None]

SeeAlso []

Definition at line 438 of file cuddAddAbs.c.

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 */

DdNode* cuddAddUnivAbstractRecur ( DdManager *  manager,
DdNode *  f,
DdNode *  cube 
)

Function********************************************************************

Synopsis [Performs the recursive step of Cudd_addUnivAbstract.]

Description [Performs the recursive step of Cudd_addUnivAbstract. Returns the ADD obtained by abstracting the variables of cube from f, if successful; NULL otherwise.]

SideEffects [None]

SeeAlso []

Definition at line 330 of file cuddAddAbs.c.

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 */

Variable Documentation

char rcsid [] DD_UNUSED = "$Id: cuddAddAbs.c,v 1.1.1.1 2003/02/24 22:23:50 wjiang Exp $" [static]

CFile***********************************************************************

FileName [cuddAddAbs.c]

PackageName [cudd]

Synopsis [Quantification functions for ADDs.]

Description [External procedures included in this module:

Internal procedures included in this module:

Static procedures included in this module:

]

Author [Fabio Somenzi]

Copyright [This file was created at the University of Colorado at Boulder. The University of Colorado at Boulder makes no warranty about the suitability of this software for any purpose. It is presented on an AS IS basis.]

Definition at line 58 of file cuddAddAbs.c.

DdNode* two [static]

Definition at line 61 of file cuddAddAbs.c.

Generated on Tue Jan 5 12:18:51 2010 for abc70930 by  doxygen 1.6.1