src/cuBdd/cuddBridge.c File Reference
#include "util.h"#include "cuddInt.h"
Go to the source code of this file.
Function Documentation
Function********************************************************************
Synopsis [Performs the recursive step for Cudd_addBddInterval.]
Description [Performs the recursive step for Cudd_addBddInterval. Returns a pointer to the BDD if successful; NULL otherwise.]
SideEffects [None]
SeeAlso [addBddDoThreshold addBddDoStrictThreshold]
Definition at line 712 of file cuddBridge.c.
00717 { 00718 DdNode *res, *T, *E; 00719 DdNode *fv, *fvn; 00720 int v; 00721 00722 statLine(dd); 00723 /* Check terminal case. */ 00724 if (cuddIsConstant(f)) { 00725 return(Cudd_NotCond(DD_ONE(dd),cuddV(f) < cuddV(l) || cuddV(f) > cuddV(u))); 00726 } 00727 00728 /* Check cache. */ 00729 res = cuddCacheLookup(dd,DD_ADD_BDD_DO_INTERVAL_TAG,f,l,u); 00730 if (res != NULL) return(res); 00731 00732 /* Recursive step. */ 00733 v = f->index; 00734 fv = cuddT(f); fvn = cuddE(f); 00735 00736 T = addBddDoInterval(dd,fv,l,u); 00737 if (T == NULL) return(NULL); 00738 cuddRef(T); 00739 00740 E = addBddDoInterval(dd,fvn,l,u); 00741 if (E == NULL) { 00742 Cudd_RecursiveDeref(dd, T); 00743 return(NULL); 00744 } 00745 cuddRef(E); 00746 if (Cudd_IsComplement(T)) { 00747 res = (T == E) ? Cudd_Not(T) : cuddUniqueInter(dd,v,Cudd_Not(T),Cudd_Not(E)); 00748 if (res == NULL) { 00749 Cudd_RecursiveDeref(dd, T); 00750 Cudd_RecursiveDeref(dd, E); 00751 return(NULL); 00752 } 00753 res = Cudd_Not(res); 00754 } else { 00755 res = (T == E) ? T : cuddUniqueInter(dd,v,T,E); 00756 if (res == NULL) { 00757 Cudd_RecursiveDeref(dd, T); 00758 Cudd_RecursiveDeref(dd, E); 00759 return(NULL); 00760 } 00761 } 00762 cuddDeref(T); 00763 cuddDeref(E); 00764 00765 /* Store result. */ 00766 cuddCacheInsert(dd,DD_ADD_BDD_DO_INTERVAL_TAG,f,l,u,res); 00767 00768 return(res); 00769 00770 } /* end of addBddDoInterval */
Function********************************************************************
Synopsis [Performs the recursive step for Cudd_addBddIthBit.]
Description [Performs the recursive step for Cudd_addBddIthBit. Returns a pointer to the BDD if successful; NULL otherwise.]
SideEffects [None]
SeeAlso []
Definition at line 786 of file cuddBridge.c.
00790 { 00791 DdNode *res, *T, *E; 00792 DdNode *fv, *fvn; 00793 int mask, value; 00794 int v; 00795 00796 statLine(dd); 00797 /* Check terminal case. */ 00798 if (cuddIsConstant(f)) { 00799 mask = 1 << ((int) cuddV(index)); 00800 value = (int) cuddV(f); 00801 return(Cudd_NotCond(DD_ONE(dd),(value & mask) == 0)); 00802 } 00803 00804 /* Check cache. */ 00805 res = cuddCacheLookup2(dd,addBddDoIthBit,f,index); 00806 if (res != NULL) return(res); 00807 00808 /* Recursive step. */ 00809 v = f->index; 00810 fv = cuddT(f); fvn = cuddE(f); 00811 00812 T = addBddDoIthBit(dd,fv,index); 00813 if (T == NULL) return(NULL); 00814 cuddRef(T); 00815 00816 E = addBddDoIthBit(dd,fvn,index); 00817 if (E == NULL) { 00818 Cudd_RecursiveDeref(dd, T); 00819 return(NULL); 00820 } 00821 cuddRef(E); 00822 if (Cudd_IsComplement(T)) { 00823 res = (T == E) ? Cudd_Not(T) : cuddUniqueInter(dd,v,Cudd_Not(T),Cudd_Not(E)); 00824 if (res == NULL) { 00825 Cudd_RecursiveDeref(dd, T); 00826 Cudd_RecursiveDeref(dd, E); 00827 return(NULL); 00828 } 00829 res = Cudd_Not(res); 00830 } else { 00831 res = (T == E) ? T : cuddUniqueInter(dd,v,T,E); 00832 if (res == NULL) { 00833 Cudd_RecursiveDeref(dd, T); 00834 Cudd_RecursiveDeref(dd, E); 00835 return(NULL); 00836 } 00837 } 00838 cuddDeref(T); 00839 cuddDeref(E); 00840 00841 /* Store result. */ 00842 cuddCacheInsert2(dd,addBddDoIthBit,f,index,res); 00843 00844 return(res); 00845 00846 } /* end of addBddDoIthBit */
Function********************************************************************
Synopsis [Performs the recursive step for Cudd_addBddStrictThreshold.]
Description [Performs the recursive step for Cudd_addBddStrictThreshold. Returns a pointer to the BDD if successful; NULL otherwise.]
SideEffects [None]
SeeAlso [addBddDoThreshold]
Definition at line 639 of file cuddBridge.c.
00643 { 00644 DdNode *res, *T, *E; 00645 DdNode *fv, *fvn; 00646 int v; 00647 00648 statLine(dd); 00649 /* Check terminal case. */ 00650 if (cuddIsConstant(f)) { 00651 return(Cudd_NotCond(DD_ONE(dd),cuddV(f) <= cuddV(val))); 00652 } 00653 00654 /* Check cache. */ 00655 res = cuddCacheLookup2(dd,addBddDoStrictThreshold,f,val); 00656 if (res != NULL) return(res); 00657 00658 /* Recursive step. */ 00659 v = f->index; 00660 fv = cuddT(f); fvn = cuddE(f); 00661 00662 T = addBddDoStrictThreshold(dd,fv,val); 00663 if (T == NULL) return(NULL); 00664 cuddRef(T); 00665 00666 E = addBddDoStrictThreshold(dd,fvn,val); 00667 if (E == NULL) { 00668 Cudd_RecursiveDeref(dd, T); 00669 return(NULL); 00670 } 00671 cuddRef(E); 00672 if (Cudd_IsComplement(T)) { 00673 res = (T == E) ? Cudd_Not(T) : cuddUniqueInter(dd,v,Cudd_Not(T),Cudd_Not(E)); 00674 if (res == NULL) { 00675 Cudd_RecursiveDeref(dd, T); 00676 Cudd_RecursiveDeref(dd, E); 00677 return(NULL); 00678 } 00679 res = Cudd_Not(res); 00680 } else { 00681 res = (T == E) ? T : cuddUniqueInter(dd,v,T,E); 00682 if (res == NULL) { 00683 Cudd_RecursiveDeref(dd, T); 00684 Cudd_RecursiveDeref(dd, E); 00685 return(NULL); 00686 } 00687 } 00688 cuddDeref(T); 00689 cuddDeref(E); 00690 00691 /* Store result. */ 00692 cuddCacheInsert2(dd,addBddDoStrictThreshold,f,val,res); 00693 00694 return(res); 00695 00696 } /* end of addBddDoStrictThreshold */
AutomaticStart
Function********************************************************************
Synopsis [Performs the recursive step for Cudd_addBddThreshold.]
Description [Performs the recursive step for Cudd_addBddThreshold. Returns a pointer to the BDD if successful; NULL otherwise.]
SideEffects [None]
SeeAlso [addBddDoStrictThreshold]
Definition at line 566 of file cuddBridge.c.
00570 { 00571 DdNode *res, *T, *E; 00572 DdNode *fv, *fvn; 00573 int v; 00574 00575 statLine(dd); 00576 /* Check terminal case. */ 00577 if (cuddIsConstant(f)) { 00578 return(Cudd_NotCond(DD_ONE(dd),cuddV(f) < cuddV(val))); 00579 } 00580 00581 /* Check cache. */ 00582 res = cuddCacheLookup2(dd,addBddDoThreshold,f,val); 00583 if (res != NULL) return(res); 00584 00585 /* Recursive step. */ 00586 v = f->index; 00587 fv = cuddT(f); fvn = cuddE(f); 00588 00589 T = addBddDoThreshold(dd,fv,val); 00590 if (T == NULL) return(NULL); 00591 cuddRef(T); 00592 00593 E = addBddDoThreshold(dd,fvn,val); 00594 if (E == NULL) { 00595 Cudd_RecursiveDeref(dd, T); 00596 return(NULL); 00597 } 00598 cuddRef(E); 00599 if (Cudd_IsComplement(T)) { 00600 res = (T == E) ? Cudd_Not(T) : cuddUniqueInter(dd,v,Cudd_Not(T),Cudd_Not(E)); 00601 if (res == NULL) { 00602 Cudd_RecursiveDeref(dd, T); 00603 Cudd_RecursiveDeref(dd, E); 00604 return(NULL); 00605 } 00606 res = Cudd_Not(res); 00607 } else { 00608 res = (T == E) ? T : cuddUniqueInter(dd,v,T,E); 00609 if (res == NULL) { 00610 Cudd_RecursiveDeref(dd, T); 00611 Cudd_RecursiveDeref(dd, E); 00612 return(NULL); 00613 } 00614 } 00615 cuddDeref(T); 00616 cuddDeref(E); 00617 00618 /* Store result. */ 00619 cuddCacheInsert2(dd,addBddDoThreshold,f,val,res); 00620 00621 return(res); 00622 00623 } /* end of addBddDoThreshold */
| DdNode* Cudd_addBddInterval | ( | DdManager * | dd, | |
| DdNode * | f, | |||
| CUDD_VALUE_TYPE | lower, | |||
| CUDD_VALUE_TYPE | upper | |||
| ) |
Function********************************************************************
Synopsis [Converts an ADD to a BDD.]
Description [Converts an ADD to a BDD by replacing all discriminants greater than or equal to lower and less than or equal to upper with 1, and all other discriminants with 0. Returns a pointer to the resulting BDD if successful; NULL otherwise.]
SideEffects [None]
SeeAlso [Cudd_addBddThreshold Cudd_addBddStrictThreshold Cudd_addBddPattern Cudd_BddToAdd]
Definition at line 240 of file cuddBridge.c.
00245 { 00246 DdNode *res; 00247 DdNode *l; 00248 DdNode *u; 00249 00250 /* Create constant nodes for the interval bounds, so that we can use 00251 ** the global cache. 00252 */ 00253 l = cuddUniqueConst(dd,lower); 00254 if (l == NULL) return(NULL); 00255 cuddRef(l); 00256 u = cuddUniqueConst(dd,upper); 00257 if (u == NULL) { 00258 Cudd_RecursiveDeref(dd,l); 00259 return(NULL); 00260 } 00261 cuddRef(u); 00262 00263 do { 00264 dd->reordered = 0; 00265 res = addBddDoInterval(dd, f, l, u); 00266 } while (dd->reordered == 1); 00267 00268 if (res == NULL) { 00269 Cudd_RecursiveDeref(dd, l); 00270 Cudd_RecursiveDeref(dd, u); 00271 return(NULL); 00272 } 00273 cuddRef(res); 00274 Cudd_RecursiveDeref(dd, l); 00275 Cudd_RecursiveDeref(dd, u); 00276 cuddDeref(res); 00277 return(res); 00278 00279 } /* end of Cudd_addBddInterval */
Function********************************************************************
Synopsis [Converts an ADD to a BDD by extracting the i-th bit from the leaves.]
Description [Converts an ADD to a BDD by replacing all discriminants whose i-th bit is equal to 1 with 1, and all other discriminants with 0. The i-th bit refers to the integer representation of the leaf value. If the value is has a fractional part, it is ignored. Repeated calls to this procedure allow one to transform an integer-valued ADD into an array of BDDs, one for each bit of the leaf values. Returns a pointer to the resulting BDD if successful; NULL otherwise.]
SideEffects [None]
SeeAlso [Cudd_addBddInterval Cudd_addBddPattern Cudd_BddToAdd]
Definition at line 302 of file cuddBridge.c.
00306 { 00307 DdNode *res; 00308 DdNode *index; 00309 00310 index = cuddUniqueConst(dd,(CUDD_VALUE_TYPE) bit); 00311 if (index == NULL) return(NULL); 00312 cuddRef(index); 00313 00314 do { 00315 dd->reordered = 0; 00316 res = addBddDoIthBit(dd, f, index); 00317 } while (dd->reordered == 1); 00318 00319 if (res == NULL) { 00320 Cudd_RecursiveDeref(dd, index); 00321 return(NULL); 00322 } 00323 cuddRef(res); 00324 Cudd_RecursiveDeref(dd, index); 00325 cuddDeref(res); 00326 return(res); 00327 00328 } /* end of Cudd_addBddIthBit */
Function********************************************************************
Synopsis [Converts an ADD to a BDD.]
Description [Converts an ADD to a BDD by replacing all discriminants different from 0 with 1. Returns a pointer to the resulting BDD if successful; NULL otherwise.]
SideEffects [None]
SeeAlso [Cudd_BddToAdd Cudd_addBddThreshold Cudd_addBddInterval Cudd_addBddStrictThreshold]
Definition at line 375 of file cuddBridge.c.
00378 { 00379 DdNode *res; 00380 00381 do { 00382 dd->reordered = 0; 00383 res = cuddAddBddDoPattern(dd, f); 00384 } while (dd->reordered == 1); 00385 return(res); 00386 00387 } /* end of Cudd_addBddPattern */
Function********************************************************************
Synopsis [Converts an ADD to a BDD.]
Description [Converts an ADD to a BDD by replacing all discriminants STRICTLY greater than value with 1, and all other discriminants with 0. Returns a pointer to the resulting BDD if successful; NULL otherwise.]
SideEffects [None]
SeeAlso [Cudd_addBddInterval Cudd_addBddPattern Cudd_BddToAdd Cudd_addBddThreshold]
Definition at line 195 of file cuddBridge.c.
00199 { 00200 DdNode *res; 00201 DdNode *val; 00202 00203 val = cuddUniqueConst(dd,value); 00204 if (val == NULL) return(NULL); 00205 cuddRef(val); 00206 00207 do { 00208 dd->reordered = 0; 00209 res = addBddDoStrictThreshold(dd, f, val); 00210 } while (dd->reordered == 1); 00211 00212 if (res == NULL) { 00213 Cudd_RecursiveDeref(dd, val); 00214 return(NULL); 00215 } 00216 cuddRef(res); 00217 Cudd_RecursiveDeref(dd, val); 00218 cuddDeref(res); 00219 return(res); 00220 00221 } /* end of Cudd_addBddStrictThreshold */
AutomaticEnd Function********************************************************************
Synopsis [Converts an ADD to a BDD.]
Description [Converts an ADD to a BDD by replacing all discriminants greater than or equal to value with 1, and all other discriminants with 0. Returns a pointer to the resulting BDD if successful; NULL otherwise.]
SideEffects [None]
SeeAlso [Cudd_addBddInterval Cudd_addBddPattern Cudd_BddToAdd Cudd_addBddStrictThreshold]
Definition at line 150 of file cuddBridge.c.
00154 { 00155 DdNode *res; 00156 DdNode *val; 00157 00158 val = cuddUniqueConst(dd,value); 00159 if (val == NULL) return(NULL); 00160 cuddRef(val); 00161 00162 do { 00163 dd->reordered = 0; 00164 res = addBddDoThreshold(dd, f, val); 00165 } while (dd->reordered == 1); 00166 00167 if (res == NULL) { 00168 Cudd_RecursiveDeref(dd, val); 00169 return(NULL); 00170 } 00171 cuddRef(res); 00172 Cudd_RecursiveDeref(dd, val); 00173 cuddDeref(res); 00174 return(res); 00175 00176 } /* end of Cudd_addBddThreshold */
Function********************************************************************
Synopsis [Converts a BDD to a 0-1 ADD.]
Description [Converts a BDD to a 0-1 ADD. Returns a pointer to the resulting ADD if successful; NULL otherwise.]
SideEffects [None]
SeeAlso [Cudd_addBddPattern Cudd_addBddThreshold Cudd_addBddInterval Cudd_addBddStrictThreshold]
Definition at line 345 of file cuddBridge.c.
00348 { 00349 DdNode *res; 00350 00351 do { 00352 dd->reordered = 0; 00353 res = ddBddToAddRecur(dd, B); 00354 } while (dd->reordered ==1); 00355 return(res); 00356 00357 } /* end of Cudd_BddToAdd */
Function********************************************************************
Synopsis [Convert a BDD from a manager to another one.]
Description [Convert a BDD from a manager to another one. The orders of the variables in the two managers may be different. Returns a pointer to the BDD in the destination manager if successful; NULL otherwise.]
SideEffects [None]
SeeAlso []
Definition at line 405 of file cuddBridge.c.
00409 { 00410 DdNode *res; 00411 do { 00412 ddDestination->reordered = 0; 00413 res = cuddBddTransfer(ddSource, ddDestination, f); 00414 } while (ddDestination->reordered == 1); 00415 return(res); 00416 00417 } /* end of Cudd_bddTransfer */
Function********************************************************************
Synopsis [Performs the recursive step for Cudd_addBddPattern.]
Description [Performs the recursive step for Cudd_addBddPattern. Returns a pointer to the resulting BDD if successful; NULL otherwise.]
SideEffects [None]
SeeAlso []
Definition at line 489 of file cuddBridge.c.
00492 { 00493 DdNode *res, *T, *E; 00494 DdNode *fv, *fvn; 00495 int v; 00496 00497 statLine(dd); 00498 /* Check terminal case. */ 00499 if (cuddIsConstant(f)) { 00500 return(Cudd_NotCond(DD_ONE(dd),f == DD_ZERO(dd))); 00501 } 00502 00503 /* Check cache. */ 00504 res = cuddCacheLookup1(dd,Cudd_addBddPattern,f); 00505 if (res != NULL) return(res); 00506 00507 /* Recursive step. */ 00508 v = f->index; 00509 fv = cuddT(f); fvn = cuddE(f); 00510 00511 T = cuddAddBddDoPattern(dd,fv); 00512 if (T == NULL) return(NULL); 00513 cuddRef(T); 00514 00515 E = cuddAddBddDoPattern(dd,fvn); 00516 if (E == NULL) { 00517 Cudd_RecursiveDeref(dd, T); 00518 return(NULL); 00519 } 00520 cuddRef(E); 00521 if (Cudd_IsComplement(T)) { 00522 res = (T == E) ? Cudd_Not(T) : cuddUniqueInter(dd,v,Cudd_Not(T),Cudd_Not(E)); 00523 if (res == NULL) { 00524 Cudd_RecursiveDeref(dd, T); 00525 Cudd_RecursiveDeref(dd, E); 00526 return(NULL); 00527 } 00528 res = Cudd_Not(res); 00529 } else { 00530 res = (T == E) ? T : cuddUniqueInter(dd,v,T,E); 00531 if (res == NULL) { 00532 Cudd_RecursiveDeref(dd, T); 00533 Cudd_RecursiveDeref(dd, E); 00534 return(NULL); 00535 } 00536 } 00537 cuddDeref(T); 00538 cuddDeref(E); 00539 00540 /* Store result. */ 00541 cuddCacheInsert1(dd,Cudd_addBddPattern,f,res); 00542 00543 return(res); 00544 00545 } /* end of cuddAddBddDoPattern */
Function********************************************************************
Synopsis [Convert a BDD from a manager to another one.]
Description [Convert a BDD from a manager to another one. Returns a pointer to the BDD in the destination manager if successful; NULL otherwise.]
SideEffects [None]
SeeAlso [Cudd_bddTransfer]
Definition at line 439 of file cuddBridge.c.
00443 { 00444 DdNode *res; 00445 st_table *table = NULL; 00446 st_generator *gen = NULL; 00447 DdNode *key, *value; 00448 00449 table = st_init_table(st_ptrcmp,st_ptrhash); 00450 if (table == NULL) goto failure; 00451 res = cuddBddTransferRecur(ddS, ddD, f, table); 00452 if (res != NULL) cuddRef(res); 00453 00454 /* Dereference all elements in the table and dispose of the table. 00455 ** This must be done also if res is NULL to avoid leaks in case of 00456 ** reordering. */ 00457 gen = st_init_gen(table); 00458 if (gen == NULL) goto failure; 00459 while (st_gen(gen, &key, &value)) { 00460 Cudd_RecursiveDeref(ddD, value); 00461 } 00462 st_free_gen(gen); gen = NULL; 00463 st_free_table(table); table = NULL; 00464 00465 if (res != NULL) cuddDeref(res); 00466 return(res); 00467 00468 failure: 00469 /* No need to free gen because it is always NULL here. */ 00470 if (table != NULL) st_free_table(table); 00471 return(NULL); 00472 00473 } /* end of cuddBddTransfer */
| static DdNode * cuddBddTransferRecur | ( | DdManager * | ddS, | |
| DdManager * | ddD, | |||
| DdNode * | f, | |||
| st_table * | table | |||
| ) | [static] |
Function********************************************************************
Synopsis [Performs the recursive step of Cudd_bddTransfer.]
Description [Performs the recursive step of Cudd_bddTransfer. Returns a pointer to the result if successful; NULL otherwise.]
SideEffects [None]
SeeAlso [cuddBddTransfer]
Definition at line 949 of file cuddBridge.c.
00954 { 00955 DdNode *ft, *fe, *t, *e, *var, *res; 00956 DdNode *one, *zero; 00957 int index; 00958 int comple = 0; 00959 00960 statLine(ddD); 00961 one = DD_ONE(ddD); 00962 comple = Cudd_IsComplement(f); 00963 00964 /* Trivial cases. */ 00965 if (Cudd_IsConstant(f)) return(Cudd_NotCond(one, comple)); 00966 00967 /* Make canonical to increase the utilization of the cache. */ 00968 f = Cudd_NotCond(f,comple); 00969 /* Now f is a regular pointer to a non-constant node. */ 00970 00971 /* Check the cache. */ 00972 if (st_lookup(table, f, &res)) 00973 return(Cudd_NotCond(res,comple)); 00974 00975 /* Recursive step. */ 00976 index = f->index; 00977 ft = cuddT(f); fe = cuddE(f); 00978 00979 t = cuddBddTransferRecur(ddS, ddD, ft, table); 00980 if (t == NULL) { 00981 return(NULL); 00982 } 00983 cuddRef(t); 00984 00985 e = cuddBddTransferRecur(ddS, ddD, fe, table); 00986 if (e == NULL) { 00987 Cudd_RecursiveDeref(ddD, t); 00988 return(NULL); 00989 } 00990 cuddRef(e); 00991 00992 zero = Cudd_Not(one); 00993 var = cuddUniqueInter(ddD,index,one,zero); 00994 if (var == NULL) { 00995 Cudd_RecursiveDeref(ddD, t); 00996 Cudd_RecursiveDeref(ddD, e); 00997 return(NULL); 00998 } 00999 res = cuddBddIteRecur(ddD,var,t,e); 01000 if (res == NULL) { 01001 Cudd_RecursiveDeref(ddD, t); 01002 Cudd_RecursiveDeref(ddD, e); 01003 return(NULL); 01004 } 01005 cuddRef(res); 01006 Cudd_RecursiveDeref(ddD, t); 01007 Cudd_RecursiveDeref(ddD, e); 01008 01009 if (st_add_direct(table, (char *) f, (char *) res) == ST_OUT_OF_MEM) { 01010 Cudd_RecursiveDeref(ddD, res); 01011 return(NULL); 01012 } 01013 return(Cudd_NotCond(res,comple)); 01014 01015 } /* end of cuddBddTransferRecur */
Function********************************************************************
Synopsis [Performs the recursive step for Cudd_BddToAdd.]
Description [Performs the recursive step for Cudd_BddToAdd. Returns a pointer to the resulting ADD if successful; NULL otherwise.]
SideEffects [None]
SeeAlso []
Definition at line 862 of file cuddBridge.c.
00865 { 00866 DdNode *one; 00867 DdNode *res, *res1, *T, *E, *Bt, *Be; 00868 int complement = 0; 00869 00870 statLine(dd); 00871 one = DD_ONE(dd); 00872 00873 if (Cudd_IsConstant(B)) { 00874 if (B == one) { 00875 res = one; 00876 } else { 00877 res = DD_ZERO(dd); 00878 } 00879 return(res); 00880 } 00881 /* Check visited table */ 00882 res = cuddCacheLookup1(dd,ddBddToAddRecur,B); 00883 if (res != NULL) return(res); 00884 00885 if (Cudd_IsComplement(B)) { 00886 complement = 1; 00887 Bt = cuddT(Cudd_Regular(B)); 00888 Be = cuddE(Cudd_Regular(B)); 00889 } else { 00890 Bt = cuddT(B); 00891 Be = cuddE(B); 00892 } 00893 00894 T = ddBddToAddRecur(dd, Bt); 00895 if (T == NULL) return(NULL); 00896 cuddRef(T); 00897 00898 E = ddBddToAddRecur(dd, Be); 00899 if (E == NULL) { 00900 Cudd_RecursiveDeref(dd, T); 00901 return(NULL); 00902 } 00903 cuddRef(E); 00904 00905 /* No need to check for T == E, because it is guaranteed not to happen. */ 00906 res = cuddUniqueInter(dd, (int) Cudd_Regular(B)->index, T, E); 00907 if (res == NULL) { 00908 Cudd_RecursiveDeref(dd ,T); 00909 Cudd_RecursiveDeref(dd ,E); 00910 return(NULL); 00911 } 00912 cuddDeref(T); 00913 cuddDeref(E); 00914 00915 if (complement) { 00916 cuddRef(res); 00917 res1 = cuddAddCmplRecur(dd, res); 00918 if (res1 == NULL) { 00919 Cudd_RecursiveDeref(dd, res); 00920 return(NULL); 00921 } 00922 cuddRef(res1); 00923 Cudd_RecursiveDeref(dd, res); 00924 res = res1; 00925 cuddDeref(res); 00926 } 00927 00928 /* Store result. */ 00929 cuddCacheInsert1(dd,ddBddToAddRecur,B,res); 00930 00931 return(res); 00932 00933 } /* end of ddBddToAddRecur */
Variable Documentation
char rcsid [] DD_UNUSED = "$Id: cuddBridge.c,v 1.19 2008/04/25 06:42:55 fabio Exp $" [static] |
CFile***********************************************************************
FileName [cuddBridge.c]
PackageName [cudd]
Synopsis [Translation from BDD to ADD and vice versa and transfer between different managers.]
Description [External procedures included in this file:
- Cudd_addBddThreshold()
- Cudd_addBddStrictThreshold()
- Cudd_addBddInterval()
- Cudd_addBddIthBit()
- Cudd_BddToAdd()
- Cudd_addBddPattern()
- Cudd_bddTransfer()
Internal procedures included in this file:
Static procedures included in this file:
- addBddDoThreshold()
- addBddDoStrictThreshold()
- addBddDoInterval()
- addBddDoIthBit()
- ddBddToAddRecur()
- cuddBddTransferRecur()
]
SeeAlso []
Author [Fabio Somenzi]
Copyright [Copyright (c) 1995-2004, Regents of the University of Colorado
All rights reserved.
Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met:
Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer.
Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution.
Neither the name of the University of Colorado nor the names of its contributors may be used to endorse or promote products derived from this software without specific prior written permission.
THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.]
Definition at line 97 of file cuddBridge.c.
