src/cuBdd/cuddBddIte.c File Reference
#include "util.h"#include "cuddInt.h"
Go to the source code of this file.
Function Documentation
| static int bddVarToCanonical | ( | DdManager * | dd, | |
| DdNode ** | fp, | |||
| DdNode ** | gp, | |||
| DdNode ** | hp, | |||
| unsigned int * | topfp, | |||
| unsigned int * | topgp, | |||
| unsigned int * | tophp | |||
| ) | [static] |
Function********************************************************************
Synopsis [Picks unique member from equiv expressions.]
Description [Reduces 2 variable expressions to canonical form.]
SideEffects [None]
SeeAlso [bddVarToConst bddVarToCanonicalSimple]
Definition at line 1166 of file cuddBddIte.c.
01174 { 01175 register DdNode *F, *G, *H, *r, *f, *g, *h; 01176 register unsigned int topf, topg, toph; 01177 DdNode *one = dd->one; 01178 int comple, change; 01179 01180 f = *fp; 01181 g = *gp; 01182 h = *hp; 01183 F = Cudd_Regular(f); 01184 G = Cudd_Regular(g); 01185 H = Cudd_Regular(h); 01186 topf = cuddI(dd,F->index); 01187 topg = cuddI(dd,G->index); 01188 toph = cuddI(dd,H->index); 01189 01190 change = 0; 01191 01192 if (G == one) { /* ITE(F,c,H) */ 01193 if ((topf > toph) || (topf == toph && f > h)) { 01194 r = h; 01195 h = f; 01196 f = r; /* ITE(F,1,H) = ITE(H,1,F) */ 01197 if (g != one) { /* g == zero */ 01198 f = Cudd_Not(f); /* ITE(F,0,H) = ITE(!H,0,!F) */ 01199 h = Cudd_Not(h); 01200 } 01201 change = 1; 01202 } 01203 } else if (H == one) { /* ITE(F,G,c) */ 01204 if ((topf > topg) || (topf == topg && f > g)) { 01205 r = g; 01206 g = f; 01207 f = r; /* ITE(F,G,0) = ITE(G,F,0) */ 01208 if (h == one) { 01209 f = Cudd_Not(f); /* ITE(F,G,1) = ITE(!G,!F,1) */ 01210 g = Cudd_Not(g); 01211 } 01212 change = 1; 01213 } 01214 } else if (g == Cudd_Not(h)) { /* ITE(F,G,!G) = ITE(G,F,!F) */ 01215 if ((topf > topg) || (topf == topg && f > g)) { 01216 r = f; 01217 f = g; 01218 g = r; 01219 h = Cudd_Not(r); 01220 change = 1; 01221 } 01222 } 01223 /* adjust pointers so that the first 2 arguments to ITE are regular */ 01224 if (Cudd_IsComplement(f) != 0) { /* ITE(!F,G,H) = ITE(F,H,G) */ 01225 f = Cudd_Not(f); 01226 r = g; 01227 g = h; 01228 h = r; 01229 change = 1; 01230 } 01231 comple = 0; 01232 if (Cudd_IsComplement(g) != 0) { /* ITE(F,!G,H) = !ITE(F,G,!H) */ 01233 g = Cudd_Not(g); 01234 h = Cudd_Not(h); 01235 change = 1; 01236 comple = 1; 01237 } 01238 if (change != 0) { 01239 *fp = f; 01240 *gp = g; 01241 *hp = h; 01242 } 01243 *topfp = cuddI(dd,f->index); 01244 *topgp = cuddI(dd,g->index); 01245 *tophp = cuddI(dd,Cudd_Regular(h)->index); 01246 01247 return(comple); 01248 01249 } /* end of bddVarToCanonical */
| static int bddVarToCanonicalSimple | ( | DdManager * | dd, | |
| DdNode ** | fp, | |||
| DdNode ** | gp, | |||
| DdNode ** | hp, | |||
| unsigned int * | topfp, | |||
| unsigned int * | topgp, | |||
| unsigned int * | tophp | |||
| ) | [static] |
Function********************************************************************
Synopsis [Picks unique member from equiv expressions.]
Description [Makes sure the first two pointers are regular. This mat require the complementation of the result, which is signaled by returning 1 instead of 0. This function is simpler than the general case because it assumes that no two arguments are the same or complementary, and no argument is constant.]
SideEffects [None]
SeeAlso [bddVarToConst bddVarToCanonical]
Definition at line 1268 of file cuddBddIte.c.
01276 { 01277 register DdNode *r, *f, *g, *h; 01278 int comple, change; 01279 01280 f = *fp; 01281 g = *gp; 01282 h = *hp; 01283 01284 change = 0; 01285 01286 /* adjust pointers so that the first 2 arguments to ITE are regular */ 01287 if (Cudd_IsComplement(f)) { /* ITE(!F,G,H) = ITE(F,H,G) */ 01288 f = Cudd_Not(f); 01289 r = g; 01290 g = h; 01291 h = r; 01292 change = 1; 01293 } 01294 comple = 0; 01295 if (Cudd_IsComplement(g)) { /* ITE(F,!G,H) = !ITE(F,G,!H) */ 01296 g = Cudd_Not(g); 01297 h = Cudd_Not(h); 01298 change = 1; 01299 comple = 1; 01300 } 01301 if (change) { 01302 *fp = f; 01303 *gp = g; 01304 *hp = h; 01305 } 01306 01307 /* Here we can skip the use of cuddI, because the operands are known 01308 ** to be non-constant. 01309 */ 01310 *topfp = dd->perm[f->index]; 01311 *topgp = dd->perm[g->index]; 01312 *tophp = dd->perm[Cudd_Regular(h)->index]; 01313 01314 return(comple); 01315 01316 } /* end of bddVarToCanonicalSimple */
AutomaticStart
Function********************************************************************
Synopsis [Replaces variables with constants if possible.]
Description [This function performs part of the transformation to standard form by replacing variables with constants if possible.]
SideEffects [None]
SeeAlso [bddVarToCanonical bddVarToCanonicalSimple]
Definition at line 1131 of file cuddBddIte.c.
01136 { 01137 DdNode *g = *gp; 01138 DdNode *h = *hp; 01139 01140 if (f == g) { /* ITE(F,F,H) = ITE(F,1,H) = F + H */ 01141 *gp = one; 01142 } else if (f == Cudd_Not(g)) { /* ITE(F,!F,H) = ITE(F,0,H) = !F * H */ 01143 *gp = Cudd_Not(one); 01144 } 01145 if (f == h) { /* ITE(F,G,F) = ITE(F,G,0) = F * G */ 01146 *hp = Cudd_Not(one); 01147 } else if (f == Cudd_Not(h)) { /* ITE(F,G,!F) = ITE(F,G,1) = !F + G */ 01148 *hp = one; 01149 } 01150 01151 } /* end of bddVarToConst */
Function********************************************************************
Synopsis [Computes the conjunction of two BDDs f and g.]
Description [Computes the conjunction of two BDDs f and g. Returns a pointer to the resulting BDD if successful; NULL if the intermediate result blows up.]
SideEffects [None]
SeeAlso [Cudd_bddIte Cudd_addApply Cudd_bddAndAbstract Cudd_bddIntersect Cudd_bddOr Cudd_bddNand Cudd_bddNor Cudd_bddXor Cudd_bddXnor]
Definition at line 310 of file cuddBddIte.c.
00314 { 00315 DdNode *res; 00316 00317 do { 00318 dd->reordered = 0; 00319 res = cuddBddAndRecur(dd,f,g); 00320 } while (dd->reordered == 1); 00321 return(res); 00322 00323 } /* end of Cudd_bddAnd */
Function********************************************************************
Synopsis [Computes the conjunction of two BDDs f and g. Returns NULL if too many nodes are required.]
Description [Computes the conjunction of two BDDs f and g. Returns a pointer to the resulting BDD if successful; NULL if the intermediate result blows up or more new nodes than limit are required.]
SideEffects [None]
SeeAlso [Cudd_bddAnd]
Definition at line 342 of file cuddBddIte.c.
00347 { 00348 DdNode *res; 00349 unsigned int saveLimit = dd->maxLive; 00350 00351 dd->maxLive = (dd->keys - dd->dead) + (dd->keysZ - dd->deadZ) + limit; 00352 do { 00353 dd->reordered = 0; 00354 res = cuddBddAndRecur(dd,f,g); 00355 } while (dd->reordered == 1); 00356 dd->maxLive = saveLimit; 00357 return(res); 00358 00359 } /* end of Cudd_bddAndLimit */
Function********************************************************************
Synopsis [Returns a function included in the intersection of f and g.]
Description [Computes a function included in the intersection of f and g. (That is, a witness that the intersection is not empty.) Cudd_bddIntersect tries to build as few new nodes as possible. If the only result of interest is whether f and g intersect, Cudd_bddLeq should be used instead.]
SideEffects [None]
SeeAlso [Cudd_bddLeq Cudd_bddIteConstant]
Definition at line 278 of file cuddBddIte.c.
00282 { 00283 DdNode *res; 00284 00285 do { 00286 dd->reordered = 0; 00287 res = cuddBddIntersectRecur(dd,f,g); 00288 } while (dd->reordered == 1); 00289 00290 return(res); 00291 00292 } /* end of Cudd_bddIntersect */
AutomaticEnd Function********************************************************************
Synopsis [Implements ITE(f,g,h).]
Description [Implements ITE(f,g,h). Returns a pointer to the resulting BDD if successful; NULL if the intermediate result blows up.]
SideEffects [None]
SeeAlso [Cudd_addIte Cudd_bddIteConstant Cudd_bddIntersect]
Definition at line 139 of file cuddBddIte.c.
00144 { 00145 DdNode *res; 00146 00147 do { 00148 dd->reordered = 0; 00149 res = cuddBddIteRecur(dd,f,g,h); 00150 } while (dd->reordered == 1); 00151 return(res); 00152 00153 } /* end of Cudd_bddIte */
Function********************************************************************
Synopsis [Implements ITEconstant(f,g,h).]
Description [Implements ITEconstant(f,g,h). Returns a pointer to the resulting BDD (which may or may not be constant) or DD_NON_CONSTANT. No new nodes are created.]
SideEffects [None]
SeeAlso [Cudd_bddIte Cudd_bddIntersect Cudd_bddLeq Cudd_addIteConstant]
Definition at line 170 of file cuddBddIte.c.
00175 { 00176 DdNode *r, *Fv, *Fnv, *Gv, *Gnv, *H, *Hv, *Hnv, *t, *e; 00177 DdNode *one = DD_ONE(dd); 00178 DdNode *zero = Cudd_Not(one); 00179 int comple; 00180 unsigned int topf, topg, toph, v; 00181 00182 statLine(dd); 00183 /* Trivial cases. */ 00184 if (f == one) /* ITE(1,G,H) => G */ 00185 return(g); 00186 00187 if (f == zero) /* ITE(0,G,H) => H */ 00188 return(h); 00189 00190 /* f now not a constant. */ 00191 bddVarToConst(f, &g, &h, one); /* possibly convert g or h */ 00192 /* to constants */ 00193 00194 if (g == h) /* ITE(F,G,G) => G */ 00195 return(g); 00196 00197 if (Cudd_IsConstant(g) && Cudd_IsConstant(h)) 00198 return(DD_NON_CONSTANT); /* ITE(F,1,0) or ITE(F,0,1) */ 00199 /* => DD_NON_CONSTANT */ 00200 00201 if (g == Cudd_Not(h)) 00202 return(DD_NON_CONSTANT); /* ITE(F,G,G') => DD_NON_CONSTANT */ 00203 /* if F != G and F != G' */ 00204 00205 comple = bddVarToCanonical(dd, &f, &g, &h, &topf, &topg, &toph); 00206 00207 /* Cache lookup. */ 00208 r = cuddConstantLookup(dd, DD_BDD_ITE_CONSTANT_TAG, f, g, h); 00209 if (r != NULL) { 00210 return(Cudd_NotCond(r,comple && r != DD_NON_CONSTANT)); 00211 } 00212 00213 v = ddMin(topg, toph); 00214 00215 /* ITE(F,G,H) = (v,G,H) (non constant) if F = (v,1,0), v < top(G,H). */ 00216 if (topf < v && cuddT(f) == one && cuddE(f) == zero) { 00217 return(DD_NON_CONSTANT); 00218 } 00219 00220 /* Compute cofactors. */ 00221 if (topf <= v) { 00222 v = ddMin(topf, v); /* v = top_var(F,G,H) */ 00223 Fv = cuddT(f); Fnv = cuddE(f); 00224 } else { 00225 Fv = Fnv = f; 00226 } 00227 00228 if (topg == v) { 00229 Gv = cuddT(g); Gnv = cuddE(g); 00230 } else { 00231 Gv = Gnv = g; 00232 } 00233 00234 if (toph == v) { 00235 H = Cudd_Regular(h); 00236 Hv = cuddT(H); Hnv = cuddE(H); 00237 if (Cudd_IsComplement(h)) { 00238 Hv = Cudd_Not(Hv); 00239 Hnv = Cudd_Not(Hnv); 00240 } 00241 } else { 00242 Hv = Hnv = h; 00243 } 00244 00245 /* Recursion. */ 00246 t = Cudd_bddIteConstant(dd, Fv, Gv, Hv); 00247 if (t == DD_NON_CONSTANT || !Cudd_IsConstant(t)) { 00248 cuddCacheInsert(dd, DD_BDD_ITE_CONSTANT_TAG, f, g, h, DD_NON_CONSTANT); 00249 return(DD_NON_CONSTANT); 00250 } 00251 e = Cudd_bddIteConstant(dd, Fnv, Gnv, Hnv); 00252 if (e == DD_NON_CONSTANT || !Cudd_IsConstant(e) || t != e) { 00253 cuddCacheInsert(dd, DD_BDD_ITE_CONSTANT_TAG, f, g, h, DD_NON_CONSTANT); 00254 return(DD_NON_CONSTANT); 00255 } 00256 cuddCacheInsert(dd, DD_BDD_ITE_CONSTANT_TAG, f, g, h, t); 00257 return(Cudd_NotCond(t,comple)); 00258 00259 } /* end of Cudd_bddIteConstant */
Function********************************************************************
Synopsis [Determines whether f is less than or equal to g.]
Description [Returns 1 if f is less than or equal to g; 0 otherwise. No new nodes are created.]
SideEffects [None]
SeeAlso [Cudd_bddIteConstant Cudd_addEvalConst]
Definition at line 532 of file cuddBddIte.c.
00536 { 00537 DdNode *one, *zero, *tmp, *F, *fv, *fvn, *gv, *gvn; 00538 unsigned int topf, topg, res; 00539 00540 statLine(dd); 00541 /* Terminal cases and normalization. */ 00542 if (f == g) return(1); 00543 00544 if (Cudd_IsComplement(g)) { 00545 /* Special case: if f is regular and g is complemented, 00546 ** f(1,...,1) = 1 > 0 = g(1,...,1). 00547 */ 00548 if (!Cudd_IsComplement(f)) return(0); 00549 /* Both are complemented: Swap and complement because 00550 ** f <= g <=> g' <= f' and we want the second argument to be regular. 00551 */ 00552 tmp = g; 00553 g = Cudd_Not(f); 00554 f = Cudd_Not(tmp); 00555 } else if (Cudd_IsComplement(f) && g < f) { 00556 tmp = g; 00557 g = Cudd_Not(f); 00558 f = Cudd_Not(tmp); 00559 } 00560 00561 /* Now g is regular and, if f is not regular, f < g. */ 00562 one = DD_ONE(dd); 00563 if (g == one) return(1); /* no need to test against zero */ 00564 if (f == one) return(0); /* since at this point g != one */ 00565 if (Cudd_Not(f) == g) return(0); /* because neither is constant */ 00566 zero = Cudd_Not(one); 00567 if (f == zero) return(1); 00568 00569 /* Here neither f nor g is constant. */ 00570 00571 /* Check cache. */ 00572 tmp = cuddCacheLookup2(dd,(DD_CTFP)Cudd_bddLeq,f,g); 00573 if (tmp != NULL) { 00574 return(tmp == one); 00575 } 00576 00577 /* Compute cofactors. */ 00578 F = Cudd_Regular(f); 00579 topf = dd->perm[F->index]; 00580 topg = dd->perm[g->index]; 00581 if (topf <= topg) { 00582 fv = cuddT(F); fvn = cuddE(F); 00583 if (f != F) { 00584 fv = Cudd_Not(fv); 00585 fvn = Cudd_Not(fvn); 00586 } 00587 } else { 00588 fv = fvn = f; 00589 } 00590 if (topg <= topf) { 00591 gv = cuddT(g); gvn = cuddE(g); 00592 } else { 00593 gv = gvn = g; 00594 } 00595 00596 /* Recursive calls. Since we want to maximize the probability of 00597 ** the special case f(1,...,1) > g(1,...,1), we consider the negative 00598 ** cofactors first. Indeed, the complementation parity of the positive 00599 ** cofactors is the same as the one of the parent functions. 00600 */ 00601 res = Cudd_bddLeq(dd,fvn,gvn) && Cudd_bddLeq(dd,fv,gv); 00602 00603 /* Store result in cache and return. */ 00604 cuddCacheInsert2(dd,(DD_CTFP)Cudd_bddLeq,f,g,(res ? one : zero)); 00605 return(res); 00606 00607 } /* end of Cudd_bddLeq */
Function********************************************************************
Synopsis [Computes the NAND of two BDDs f and g.]
Description [Computes the NAND of two BDDs f and g. Returns a pointer to the resulting BDD if successful; NULL if the intermediate result blows up.]
SideEffects [None]
SeeAlso [Cudd_bddIte Cudd_addApply Cudd_bddAnd Cudd_bddOr Cudd_bddNor Cudd_bddXor Cudd_bddXnor]
Definition at line 409 of file cuddBddIte.c.
00413 { 00414 DdNode *res; 00415 00416 do { 00417 dd->reordered = 0; 00418 res = cuddBddAndRecur(dd,f,g); 00419 } while (dd->reordered == 1); 00420 res = Cudd_NotCond(res,res != NULL); 00421 return(res); 00422 00423 } /* end of Cudd_bddNand */
Function********************************************************************
Synopsis [Computes the NOR of two BDDs f and g.]
Description [Computes the NOR of two BDDs f and g. Returns a pointer to the resulting BDD if successful; NULL if the intermediate result blows up.]
SideEffects [None]
SeeAlso [Cudd_bddIte Cudd_addApply Cudd_bddAnd Cudd_bddOr Cudd_bddNand Cudd_bddXor Cudd_bddXnor]
Definition at line 441 of file cuddBddIte.c.
Function********************************************************************
Synopsis [Computes the disjunction of two BDDs f and g.]
Description [Computes the disjunction of two BDDs f and g. Returns a pointer to the resulting BDD if successful; NULL if the intermediate result blows up.]
SideEffects [None]
SeeAlso [Cudd_bddIte Cudd_addApply Cudd_bddAnd Cudd_bddNand Cudd_bddNor Cudd_bddXor Cudd_bddXnor]
Definition at line 377 of file cuddBddIte.c.
00381 { 00382 DdNode *res; 00383 00384 do { 00385 dd->reordered = 0; 00386 res = cuddBddAndRecur(dd,Cudd_Not(f),Cudd_Not(g)); 00387 } while (dd->reordered == 1); 00388 res = Cudd_NotCond(res,res != NULL); 00389 return(res); 00390 00391 } /* end of Cudd_bddOr */
Function********************************************************************
Synopsis [Computes the exclusive NOR of two BDDs f and g.]
Description [Computes the exclusive NOR of two BDDs f and g. Returns a pointer to the resulting BDD if successful; NULL if the intermediate result blows up.]
SideEffects [None]
SeeAlso [Cudd_bddIte Cudd_addApply Cudd_bddAnd Cudd_bddOr Cudd_bddNand Cudd_bddNor Cudd_bddXor]
Definition at line 503 of file cuddBddIte.c.
00507 { 00508 DdNode *res; 00509 00510 do { 00511 dd->reordered = 0; 00512 res = cuddBddXorRecur(dd,f,Cudd_Not(g)); 00513 } while (dd->reordered == 1); 00514 return(res); 00515 00516 } /* end of Cudd_bddXnor */
Function********************************************************************
Synopsis [Computes the exclusive OR of two BDDs f and g.]
Description [Computes the exclusive OR of two BDDs f and g. Returns a pointer to the resulting BDD if successful; NULL if the intermediate result blows up.]
SideEffects [None]
SeeAlso [Cudd_bddIte Cudd_addApply Cudd_bddAnd Cudd_bddOr Cudd_bddNand Cudd_bddNor Cudd_bddXnor]
Definition at line 472 of file cuddBddIte.c.
00476 { 00477 DdNode *res; 00478 00479 do { 00480 dd->reordered = 0; 00481 res = cuddBddXorRecur(dd,f,g); 00482 } while (dd->reordered == 1); 00483 return(res); 00484 00485 } /* end of Cudd_bddXor */
Function********************************************************************
Synopsis [Implements the recursive step of Cudd_bddAnd.]
Description [Implements the recursive step of Cudd_bddAnd by taking the conjunction of two BDDs. Returns a pointer to the result is successful; NULL otherwise.]
SideEffects [None]
SeeAlso [Cudd_bddAnd]
Definition at line 882 of file cuddBddIte.c.
00886 { 00887 DdNode *F, *fv, *fnv, *G, *gv, *gnv; 00888 DdNode *one, *r, *t, *e; 00889 unsigned int topf, topg, index; 00890 00891 statLine(manager); 00892 one = DD_ONE(manager); 00893 00894 /* Terminal cases. */ 00895 F = Cudd_Regular(f); 00896 G = Cudd_Regular(g); 00897 if (F == G) { 00898 if (f == g) return(f); 00899 else return(Cudd_Not(one)); 00900 } 00901 if (F == one) { 00902 if (f == one) return(g); 00903 else return(f); 00904 } 00905 if (G == one) { 00906 if (g == one) return(f); 00907 else return(g); 00908 } 00909 00910 /* At this point f and g are not constant. */ 00911 if (f > g) { /* Try to increase cache efficiency. */ 00912 DdNode *tmp = f; 00913 f = g; 00914 g = tmp; 00915 F = Cudd_Regular(f); 00916 G = Cudd_Regular(g); 00917 } 00918 00919 /* Check cache. */ 00920 if (F->ref != 1 || G->ref != 1) { 00921 r = cuddCacheLookup2(manager, Cudd_bddAnd, f, g); 00922 if (r != NULL) return(r); 00923 } 00924 00925 /* Here we can skip the use of cuddI, because the operands are known 00926 ** to be non-constant. 00927 */ 00928 topf = manager->perm[F->index]; 00929 topg = manager->perm[G->index]; 00930 00931 /* Compute cofactors. */ 00932 if (topf <= topg) { 00933 index = F->index; 00934 fv = cuddT(F); 00935 fnv = cuddE(F); 00936 if (Cudd_IsComplement(f)) { 00937 fv = Cudd_Not(fv); 00938 fnv = Cudd_Not(fnv); 00939 } 00940 } else { 00941 index = G->index; 00942 fv = fnv = f; 00943 } 00944 00945 if (topg <= topf) { 00946 gv = cuddT(G); 00947 gnv = cuddE(G); 00948 if (Cudd_IsComplement(g)) { 00949 gv = Cudd_Not(gv); 00950 gnv = Cudd_Not(gnv); 00951 } 00952 } else { 00953 gv = gnv = g; 00954 } 00955 00956 t = cuddBddAndRecur(manager, fv, gv); 00957 if (t == NULL) return(NULL); 00958 cuddRef(t); 00959 00960 e = cuddBddAndRecur(manager, fnv, gnv); 00961 if (e == NULL) { 00962 Cudd_IterDerefBdd(manager, t); 00963 return(NULL); 00964 } 00965 cuddRef(e); 00966 00967 if (t == e) { 00968 r = t; 00969 } else { 00970 if (Cudd_IsComplement(t)) { 00971 r = cuddUniqueInter(manager,(int)index,Cudd_Not(t),Cudd_Not(e)); 00972 if (r == NULL) { 00973 Cudd_IterDerefBdd(manager, t); 00974 Cudd_IterDerefBdd(manager, e); 00975 return(NULL); 00976 } 00977 r = Cudd_Not(r); 00978 } else { 00979 r = cuddUniqueInter(manager,(int)index,t,e); 00980 if (r == NULL) { 00981 Cudd_IterDerefBdd(manager, t); 00982 Cudd_IterDerefBdd(manager, e); 00983 return(NULL); 00984 } 00985 } 00986 } 00987 cuddDeref(e); 00988 cuddDeref(t); 00989 if (F->ref != 1 || G->ref != 1) 00990 cuddCacheInsert2(manager, Cudd_bddAnd, f, g, r); 00991 return(r); 00992 00993 } /* end of cuddBddAndRecur */
Function********************************************************************
Synopsis [Implements the recursive step of Cudd_bddIntersect.]
Description []
SideEffects [None]
SeeAlso [Cudd_bddIntersect]
Definition at line 767 of file cuddBddIte.c.
00771 { 00772 DdNode *res; 00773 DdNode *F, *G, *t, *e; 00774 DdNode *fv, *fnv, *gv, *gnv; 00775 DdNode *one, *zero; 00776 unsigned int index, topf, topg; 00777 00778 statLine(dd); 00779 one = DD_ONE(dd); 00780 zero = Cudd_Not(one); 00781 00782 /* Terminal cases. */ 00783 if (f == zero || g == zero || f == Cudd_Not(g)) return(zero); 00784 if (f == g || g == one) return(f); 00785 if (f == one) return(g); 00786 00787 /* At this point f and g are not constant. */ 00788 if (f > g) { DdNode *tmp = f; f = g; g = tmp; } 00789 res = cuddCacheLookup2(dd,Cudd_bddIntersect,f,g); 00790 if (res != NULL) return(res); 00791 00792 /* Find splitting variable. Here we can skip the use of cuddI, 00793 ** because the operands are known to be non-constant. 00794 */ 00795 F = Cudd_Regular(f); 00796 topf = dd->perm[F->index]; 00797 G = Cudd_Regular(g); 00798 topg = dd->perm[G->index]; 00799 00800 /* Compute cofactors. */ 00801 if (topf <= topg) { 00802 index = F->index; 00803 fv = cuddT(F); 00804 fnv = cuddE(F); 00805 if (Cudd_IsComplement(f)) { 00806 fv = Cudd_Not(fv); 00807 fnv = Cudd_Not(fnv); 00808 } 00809 } else { 00810 index = G->index; 00811 fv = fnv = f; 00812 } 00813 00814 if (topg <= topf) { 00815 gv = cuddT(G); 00816 gnv = cuddE(G); 00817 if (Cudd_IsComplement(g)) { 00818 gv = Cudd_Not(gv); 00819 gnv = Cudd_Not(gnv); 00820 } 00821 } else { 00822 gv = gnv = g; 00823 } 00824 00825 /* Compute partial results. */ 00826 t = cuddBddIntersectRecur(dd,fv,gv); 00827 if (t == NULL) return(NULL); 00828 cuddRef(t); 00829 if (t != zero) { 00830 e = zero; 00831 } else { 00832 e = cuddBddIntersectRecur(dd,fnv,gnv); 00833 if (e == NULL) { 00834 Cudd_IterDerefBdd(dd, t); 00835 return(NULL); 00836 } 00837 } 00838 cuddRef(e); 00839 00840 if (t == e) { /* both equal zero */ 00841 res = t; 00842 } else if (Cudd_IsComplement(t)) { 00843 res = cuddUniqueInter(dd,(int)index,Cudd_Not(t),Cudd_Not(e)); 00844 if (res == NULL) { 00845 Cudd_IterDerefBdd(dd, t); 00846 Cudd_IterDerefBdd(dd, e); 00847 return(NULL); 00848 } 00849 res = Cudd_Not(res); 00850 } else { 00851 res = cuddUniqueInter(dd,(int)index,t,e); 00852 if (res == NULL) { 00853 Cudd_IterDerefBdd(dd, t); 00854 Cudd_IterDerefBdd(dd, e); 00855 return(NULL); 00856 } 00857 } 00858 cuddDeref(e); 00859 cuddDeref(t); 00860 00861 cuddCacheInsert2(dd,Cudd_bddIntersect,f,g,res); 00862 00863 return(res); 00864 00865 } /* end of cuddBddIntersectRecur */
Function********************************************************************
Synopsis [Implements the recursive step of Cudd_bddIte.]
Description [Implements the recursive step of Cudd_bddIte. Returns a pointer to the resulting BDD. NULL if the intermediate result blows up or if reordering occurs.]
SideEffects [None]
SeeAlso []
Definition at line 629 of file cuddBddIte.c.
00634 { 00635 DdNode *one, *zero, *res; 00636 DdNode *r, *Fv, *Fnv, *Gv, *Gnv, *H, *Hv, *Hnv, *t, *e; 00637 unsigned int topf, topg, toph, v; 00638 int index; 00639 int comple; 00640 00641 statLine(dd); 00642 /* Terminal cases. */ 00643 00644 /* One variable cases. */ 00645 if (f == (one = DD_ONE(dd))) /* ITE(1,G,H) = G */ 00646 return(g); 00647 00648 if (f == (zero = Cudd_Not(one))) /* ITE(0,G,H) = H */ 00649 return(h); 00650 00651 /* From now on, f is known not to be a constant. */ 00652 if (g == one || f == g) { /* ITE(F,F,H) = ITE(F,1,H) = F + H */ 00653 if (h == zero) { /* ITE(F,1,0) = F */ 00654 return(f); 00655 } else { 00656 res = cuddBddAndRecur(dd,Cudd_Not(f),Cudd_Not(h)); 00657 return(Cudd_NotCond(res,res != NULL)); 00658 } 00659 } else if (g == zero || f == Cudd_Not(g)) { /* ITE(F,!F,H) = ITE(F,0,H) = !F * H */ 00660 if (h == one) { /* ITE(F,0,1) = !F */ 00661 return(Cudd_Not(f)); 00662 } else { 00663 res = cuddBddAndRecur(dd,Cudd_Not(f),h); 00664 return(res); 00665 } 00666 } 00667 if (h == zero || f == h) { /* ITE(F,G,F) = ITE(F,G,0) = F * G */ 00668 res = cuddBddAndRecur(dd,f,g); 00669 return(res); 00670 } else if (h == one || f == Cudd_Not(h)) { /* ITE(F,G,!F) = ITE(F,G,1) = !F + G */ 00671 res = cuddBddAndRecur(dd,f,Cudd_Not(g)); 00672 return(Cudd_NotCond(res,res != NULL)); 00673 } 00674 00675 /* Check remaining one variable case. */ 00676 if (g == h) { /* ITE(F,G,G) = G */ 00677 return(g); 00678 } else if (g == Cudd_Not(h)) { /* ITE(F,G,!G) = F <-> G */ 00679 res = cuddBddXorRecur(dd,f,h); 00680 return(res); 00681 } 00682 00683 /* From here, there are no constants. */ 00684 comple = bddVarToCanonicalSimple(dd, &f, &g, &h, &topf, &topg, &toph); 00685 00686 /* f & g are now regular pointers */ 00687 00688 v = ddMin(topg, toph); 00689 00690 /* A shortcut: ITE(F,G,H) = (v,G,H) if F = (v,1,0), v < top(G,H). */ 00691 if (topf < v && cuddT(f) == one && cuddE(f) == zero) { 00692 r = cuddUniqueInter(dd, (int) f->index, g, h); 00693 return(Cudd_NotCond(r,comple && r != NULL)); 00694 } 00695 00696 /* Check cache. */ 00697 r = cuddCacheLookup(dd, DD_BDD_ITE_TAG, f, g, h); 00698 if (r != NULL) { 00699 return(Cudd_NotCond(r,comple)); 00700 } 00701 00702 /* Compute cofactors. */ 00703 if (topf <= v) { 00704 v = ddMin(topf, v); /* v = top_var(F,G,H) */ 00705 index = f->index; 00706 Fv = cuddT(f); Fnv = cuddE(f); 00707 } else { 00708 Fv = Fnv = f; 00709 } 00710 if (topg == v) { 00711 index = g->index; 00712 Gv = cuddT(g); Gnv = cuddE(g); 00713 } else { 00714 Gv = Gnv = g; 00715 } 00716 if (toph == v) { 00717 H = Cudd_Regular(h); 00718 index = H->index; 00719 Hv = cuddT(H); Hnv = cuddE(H); 00720 if (Cudd_IsComplement(h)) { 00721 Hv = Cudd_Not(Hv); 00722 Hnv = Cudd_Not(Hnv); 00723 } 00724 } else { 00725 Hv = Hnv = h; 00726 } 00727 00728 /* Recursive step. */ 00729 t = cuddBddIteRecur(dd,Fv,Gv,Hv); 00730 if (t == NULL) return(NULL); 00731 cuddRef(t); 00732 00733 e = cuddBddIteRecur(dd,Fnv,Gnv,Hnv); 00734 if (e == NULL) { 00735 Cudd_IterDerefBdd(dd,t); 00736 return(NULL); 00737 } 00738 cuddRef(e); 00739 00740 r = (t == e) ? t : cuddUniqueInter(dd,index,t,e); 00741 if (r == NULL) { 00742 Cudd_IterDerefBdd(dd,t); 00743 Cudd_IterDerefBdd(dd,e); 00744 return(NULL); 00745 } 00746 cuddDeref(t); 00747 cuddDeref(e); 00748 00749 cuddCacheInsert(dd, DD_BDD_ITE_TAG, f, g, h, r); 00750 return(Cudd_NotCond(r,comple)); 00751 00752 } /* end of cuddBddIteRecur */
Function********************************************************************
Synopsis [Implements the recursive step of Cudd_bddXor.]
Description [Implements the recursive step of Cudd_bddXor by taking the exclusive OR of two BDDs. Returns a pointer to the result is successful; NULL otherwise.]
SideEffects [None]
SeeAlso [Cudd_bddXor]
Definition at line 1010 of file cuddBddIte.c.
01014 { 01015 DdNode *fv, *fnv, *G, *gv, *gnv; 01016 DdNode *one, *zero, *r, *t, *e; 01017 unsigned int topf, topg, index; 01018 01019 statLine(manager); 01020 one = DD_ONE(manager); 01021 zero = Cudd_Not(one); 01022 01023 /* Terminal cases. */ 01024 if (f == g) return(zero); 01025 if (f == Cudd_Not(g)) return(one); 01026 if (f > g) { /* Try to increase cache efficiency and simplify tests. */ 01027 DdNode *tmp = f; 01028 f = g; 01029 g = tmp; 01030 } 01031 if (g == zero) return(f); 01032 if (g == one) return(Cudd_Not(f)); 01033 if (Cudd_IsComplement(f)) { 01034 f = Cudd_Not(f); 01035 g = Cudd_Not(g); 01036 } 01037 /* Now the first argument is regular. */ 01038 if (f == one) return(Cudd_Not(g)); 01039 01040 /* At this point f and g are not constant. */ 01041 01042 /* Check cache. */ 01043 r = cuddCacheLookup2(manager, Cudd_bddXor, f, g); 01044 if (r != NULL) return(r); 01045 01046 /* Here we can skip the use of cuddI, because the operands are known 01047 ** to be non-constant. 01048 */ 01049 topf = manager->perm[f->index]; 01050 G = Cudd_Regular(g); 01051 topg = manager->perm[G->index]; 01052 01053 /* Compute cofactors. */ 01054 if (topf <= topg) { 01055 index = f->index; 01056 fv = cuddT(f); 01057 fnv = cuddE(f); 01058 } else { 01059 index = G->index; 01060 fv = fnv = f; 01061 } 01062 01063 if (topg <= topf) { 01064 gv = cuddT(G); 01065 gnv = cuddE(G); 01066 if (Cudd_IsComplement(g)) { 01067 gv = Cudd_Not(gv); 01068 gnv = Cudd_Not(gnv); 01069 } 01070 } else { 01071 gv = gnv = g; 01072 } 01073 01074 t = cuddBddXorRecur(manager, fv, gv); 01075 if (t == NULL) return(NULL); 01076 cuddRef(t); 01077 01078 e = cuddBddXorRecur(manager, fnv, gnv); 01079 if (e == NULL) { 01080 Cudd_IterDerefBdd(manager, t); 01081 return(NULL); 01082 } 01083 cuddRef(e); 01084 01085 if (t == e) { 01086 r = t; 01087 } else { 01088 if (Cudd_IsComplement(t)) { 01089 r = cuddUniqueInter(manager,(int)index,Cudd_Not(t),Cudd_Not(e)); 01090 if (r == NULL) { 01091 Cudd_IterDerefBdd(manager, t); 01092 Cudd_IterDerefBdd(manager, e); 01093 return(NULL); 01094 } 01095 r = Cudd_Not(r); 01096 } else { 01097 r = cuddUniqueInter(manager,(int)index,t,e); 01098 if (r == NULL) { 01099 Cudd_IterDerefBdd(manager, t); 01100 Cudd_IterDerefBdd(manager, e); 01101 return(NULL); 01102 } 01103 } 01104 } 01105 cuddDeref(e); 01106 cuddDeref(t); 01107 cuddCacheInsert2(manager, Cudd_bddXor, f, g, r); 01108 return(r); 01109 01110 } /* end of cuddBddXorRecur */
Variable Documentation
char rcsid [] DD_UNUSED = "$Id: cuddBddIte.c,v 1.24 2004/08/13 18:04:46 fabio Exp $" [static] |
CFile***********************************************************************
FileName [cuddBddIte.c]
PackageName [cudd]
Synopsis [BDD ITE function and satellites.]
Description [External procedures included in this module:
- Cudd_bddIte()
- Cudd_bddIteConstant()
- Cudd_bddIntersect()
- Cudd_bddAnd()
- Cudd_bddAndLimit()
- Cudd_bddOr()
- Cudd_bddNand()
- Cudd_bddNor()
- Cudd_bddXor()
- Cudd_bddXnor()
- Cudd_bddLeq()
Internal procedures included in this module:
Static procedures included in this module:
]
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 99 of file cuddBddIte.c.
