src/cuBdd/cuddZddFuncs.c File Reference
#include "util.h"#include "cuddInt.h"
Go to the source code of this file.
Function Documentation
Function********************************************************************
Synopsis [Computes a complement cover for a ZDD node.]
Description [Computes a complement cover for a ZDD node. For lack of a better method, we first extract the function BDD from the ZDD cover, then make the complement of the ZDD cover from the complement of the BDD node by using ISOP. Returns a pointer to the resulting cover if successful; NULL otherwise. The result depends on current variable order.]
SideEffects [The result depends on current variable order.]
SeeAlso []
Definition at line 328 of file cuddZddFuncs.c.
00331 { 00332 DdNode *b, *isop, *zdd_I; 00333 00334 /* Check cache */ 00335 zdd_I = cuddCacheLookup1Zdd(dd, cuddZddComplement, node); 00336 if (zdd_I) 00337 return(zdd_I); 00338 00339 b = Cudd_MakeBddFromZddCover(dd, node); 00340 if (!b) 00341 return(NULL); 00342 Cudd_Ref(b); 00343 isop = Cudd_zddIsop(dd, Cudd_Not(b), Cudd_Not(b), &zdd_I); 00344 if (!isop) { 00345 Cudd_RecursiveDeref(dd, b); 00346 return(NULL); 00347 } 00348 Cudd_Ref(isop); 00349 Cudd_Ref(zdd_I); 00350 Cudd_RecursiveDeref(dd, b); 00351 Cudd_RecursiveDeref(dd, isop); 00352 00353 cuddCacheInsert1(dd, cuddZddComplement, node, zdd_I); 00354 Cudd_Deref(zdd_I); 00355 return(zdd_I); 00356 } /* end of Cudd_zddComplement */
Function********************************************************************
Synopsis [Computes the quotient of two unate covers.]
Description [Computes the quotient of two unate covers represented by ZDDs. Unate covers use one ZDD variable for each BDD variable. Returns a pointer to the resulting ZDD if successful; NULL otherwise.]
SideEffects [None]
SeeAlso [Cudd_zddWeakDiv]
Definition at line 237 of file cuddZddFuncs.c.
00241 { 00242 DdNode *res; 00243 00244 do { 00245 dd->reordered = 0; 00246 res = cuddZddDivide(dd, f, g); 00247 } while (dd->reordered == 1); 00248 return(res); 00249 00250 } /* end of Cudd_zddDivide */
Function********************************************************************
Synopsis [Modified version of Cudd_zddDivide.]
Description [Modified version of Cudd_zddDivide. This function may disappear in future releases.]
SideEffects [None]
SeeAlso []
Definition at line 295 of file cuddZddFuncs.c.
00299 { 00300 DdNode *res; 00301 00302 do { 00303 dd->reordered = 0; 00304 res = cuddZddDivideF(dd, f, g); 00305 } while (dd->reordered == 1); 00306 return(res); 00307 00308 } /* end of Cudd_zddDivideF */
AutomaticStart AutomaticEnd Function********************************************************************
Synopsis [Computes the product of two covers represented by ZDDs.]
Description [Computes the product of two covers represented by ZDDs. The result is also a ZDD. Returns a pointer to the result if successful; NULL otherwise. The covers on which Cudd_zddProduct operates use two ZDD variables for each function variable (one ZDD variable for each literal of the variable). Those two ZDD variables should be adjacent in the order.]
SideEffects [None]
SeeAlso [Cudd_zddUnateProduct]
Definition at line 141 of file cuddZddFuncs.c.
00145 { 00146 DdNode *res; 00147 00148 do { 00149 dd->reordered = 0; 00150 res = cuddZddProduct(dd, f, g); 00151 } while (dd->reordered == 1); 00152 return(res); 00153 00154 } /* end of Cudd_zddProduct */
Function********************************************************************
Synopsis [Computes the product of two unate covers.]
Description [Computes the product of two unate covers represented as ZDDs. Unate covers use one ZDD variable for each BDD variable. Returns a pointer to the result if successful; NULL otherwise.]
SideEffects [None]
SeeAlso [Cudd_zddProduct]
Definition at line 172 of file cuddZddFuncs.c.
00176 { 00177 DdNode *res; 00178 00179 do { 00180 dd->reordered = 0; 00181 res = cuddZddUnateProduct(dd, f, g); 00182 } while (dd->reordered == 1); 00183 return(res); 00184 00185 } /* end of Cudd_zddUnateProduct */
Function********************************************************************
Synopsis [Applies weak division to two covers.]
Description [Applies weak division to two ZDDs representing two covers. Returns a pointer to the ZDD representing the result if successful; NULL otherwise. The result of weak division depends on the variable order. The covers on which Cudd_zddWeakDiv operates use two ZDD variables for each function variable (one ZDD variable for each literal of the variable). Those two ZDD variables should be adjacent in the order.]
SideEffects [None]
SeeAlso [Cudd_zddDivide]
Definition at line 206 of file cuddZddFuncs.c.
00210 { 00211 DdNode *res; 00212 00213 do { 00214 dd->reordered = 0; 00215 res = cuddZddWeakDiv(dd, f, g); 00216 } while (dd->reordered == 1); 00217 return(res); 00218 00219 } /* end of Cudd_zddWeakDiv */
Function********************************************************************
Synopsis [Modified version of Cudd_zddWeakDiv.]
Description [Modified version of Cudd_zddWeakDiv. This function may disappear in future releases.]
SideEffects [None]
SeeAlso [Cudd_zddWeakDiv]
Definition at line 266 of file cuddZddFuncs.c.
00270 { 00271 DdNode *res; 00272 00273 do { 00274 dd->reordered = 0; 00275 res = cuddZddWeakDivF(dd, f, g); 00276 } while (dd->reordered == 1); 00277 return(res); 00278 00279 } /* end of Cudd_zddWeakDivF */
Function********************************************************************
Synopsis [Computes a complement of a ZDD node.]
Description [Computes the complement of a ZDD node. So far, since we couldn't find a direct way to get the complement of a ZDD cover, we first convert a ZDD cover to a BDD, then make the complement of the ZDD cover from the complement of the BDD node by using ISOP.]
SideEffects [The result depends on current variable order.]
SeeAlso []
Definition at line 1518 of file cuddZddFuncs.c.
01521 { 01522 DdNode *b, *isop, *zdd_I; 01523 01524 /* Check cache */ 01525 zdd_I = cuddCacheLookup1Zdd(dd, cuddZddComplement, node); 01526 if (zdd_I) 01527 return(zdd_I); 01528 01529 b = cuddMakeBddFromZddCover(dd, node); 01530 if (!b) 01531 return(NULL); 01532 cuddRef(b); 01533 isop = cuddZddIsop(dd, Cudd_Not(b), Cudd_Not(b), &zdd_I); 01534 if (!isop) { 01535 Cudd_RecursiveDeref(dd, b); 01536 return(NULL); 01537 } 01538 cuddRef(isop); 01539 cuddRef(zdd_I); 01540 Cudd_RecursiveDeref(dd, b); 01541 Cudd_RecursiveDeref(dd, isop); 01542 01543 cuddCacheInsert1(dd, cuddZddComplement, node, zdd_I); 01544 cuddDeref(zdd_I); 01545 return(zdd_I); 01546 } /* end of cuddZddComplement */
Function********************************************************************
Synopsis [Performs the recursive step of Cudd_zddDivide.]
Description []
SideEffects [None]
SeeAlso [Cudd_zddDivide]
Definition at line 1155 of file cuddZddFuncs.c.
01159 { 01160 int v; 01161 DdNode *one = DD_ONE(dd); 01162 DdNode *zero = DD_ZERO(dd); 01163 DdNode *f0, *f1, *g0, *g1; 01164 DdNode *q, *r, *tmp; 01165 int flag; 01166 01167 statLine(dd); 01168 if (g == one) 01169 return(f); 01170 if (f == zero || f == one) 01171 return(zero); 01172 if (f == g) 01173 return(one); 01174 01175 /* Check cache. */ 01176 r = cuddCacheLookup2Zdd(dd, cuddZddDivide, f, g); 01177 if (r) 01178 return(r); 01179 01180 v = g->index; 01181 01182 flag = cuddZddGetCofactors2(dd, f, v, &f1, &f0); 01183 if (flag == 1) 01184 return(NULL); 01185 Cudd_Ref(f1); 01186 Cudd_Ref(f0); 01187 flag = cuddZddGetCofactors2(dd, g, v, &g1, &g0); /* g1 != zero */ 01188 if (flag == 1) { 01189 Cudd_RecursiveDerefZdd(dd, f1); 01190 Cudd_RecursiveDerefZdd(dd, f0); 01191 return(NULL); 01192 } 01193 Cudd_Ref(g1); 01194 Cudd_Ref(g0); 01195 01196 r = cuddZddDivide(dd, f1, g1); 01197 if (r == NULL) { 01198 Cudd_RecursiveDerefZdd(dd, f1); 01199 Cudd_RecursiveDerefZdd(dd, f0); 01200 Cudd_RecursiveDerefZdd(dd, g1); 01201 Cudd_RecursiveDerefZdd(dd, g0); 01202 return(NULL); 01203 } 01204 Cudd_Ref(r); 01205 01206 if (r != zero && g0 != zero) { 01207 tmp = r; 01208 q = cuddZddDivide(dd, f0, g0); 01209 if (q == NULL) { 01210 Cudd_RecursiveDerefZdd(dd, f1); 01211 Cudd_RecursiveDerefZdd(dd, f0); 01212 Cudd_RecursiveDerefZdd(dd, g1); 01213 Cudd_RecursiveDerefZdd(dd, g0); 01214 return(NULL); 01215 } 01216 Cudd_Ref(q); 01217 r = cuddZddIntersect(dd, r, q); 01218 if (r == NULL) { 01219 Cudd_RecursiveDerefZdd(dd, f1); 01220 Cudd_RecursiveDerefZdd(dd, f0); 01221 Cudd_RecursiveDerefZdd(dd, g1); 01222 Cudd_RecursiveDerefZdd(dd, g0); 01223 Cudd_RecursiveDerefZdd(dd, q); 01224 return(NULL); 01225 } 01226 Cudd_Ref(r); 01227 Cudd_RecursiveDerefZdd(dd, q); 01228 Cudd_RecursiveDerefZdd(dd, tmp); 01229 } 01230 01231 Cudd_RecursiveDerefZdd(dd, f1); 01232 Cudd_RecursiveDerefZdd(dd, f0); 01233 Cudd_RecursiveDerefZdd(dd, g1); 01234 Cudd_RecursiveDerefZdd(dd, g0); 01235 01236 cuddCacheInsert2(dd, cuddZddDivide, f, g, r); 01237 Cudd_Deref(r); 01238 return(r); 01239 01240 } /* end of cuddZddDivide */
Function********************************************************************
Synopsis [Performs the recursive step of Cudd_zddDivideF.]
Description []
SideEffects [None]
SeeAlso [Cudd_zddDivideF]
Definition at line 1255 of file cuddZddFuncs.c.
01259 { 01260 int v; 01261 DdNode *one = DD_ONE(dd); 01262 DdNode *zero = DD_ZERO(dd); 01263 DdNode *f0, *f1, *g0, *g1; 01264 DdNode *q, *r, *tmp; 01265 int flag; 01266 01267 statLine(dd); 01268 if (g == one) 01269 return(f); 01270 if (f == zero || f == one) 01271 return(zero); 01272 if (f == g) 01273 return(one); 01274 01275 /* Check cache. */ 01276 r = cuddCacheLookup2Zdd(dd, cuddZddDivideF, f, g); 01277 if (r) 01278 return(r); 01279 01280 v = g->index; 01281 01282 flag = cuddZddGetCofactors2(dd, f, v, &f1, &f0); 01283 if (flag == 1) 01284 return(NULL); 01285 Cudd_Ref(f1); 01286 Cudd_Ref(f0); 01287 flag = cuddZddGetCofactors2(dd, g, v, &g1, &g0); /* g1 != zero */ 01288 if (flag == 1) { 01289 Cudd_RecursiveDerefZdd(dd, f1); 01290 Cudd_RecursiveDerefZdd(dd, f0); 01291 return(NULL); 01292 } 01293 Cudd_Ref(g1); 01294 Cudd_Ref(g0); 01295 01296 r = cuddZddDivideF(dd, f1, g1); 01297 if (r == NULL) { 01298 Cudd_RecursiveDerefZdd(dd, f1); 01299 Cudd_RecursiveDerefZdd(dd, f0); 01300 Cudd_RecursiveDerefZdd(dd, g1); 01301 Cudd_RecursiveDerefZdd(dd, g0); 01302 return(NULL); 01303 } 01304 Cudd_Ref(r); 01305 01306 if (r != zero && g0 != zero) { 01307 tmp = r; 01308 q = cuddZddDivideF(dd, f0, g0); 01309 if (q == NULL) { 01310 Cudd_RecursiveDerefZdd(dd, f1); 01311 Cudd_RecursiveDerefZdd(dd, f0); 01312 Cudd_RecursiveDerefZdd(dd, g1); 01313 Cudd_RecursiveDerefZdd(dd, g0); 01314 return(NULL); 01315 } 01316 Cudd_Ref(q); 01317 r = cuddZddIntersect(dd, r, q); 01318 if (r == NULL) { 01319 Cudd_RecursiveDerefZdd(dd, f1); 01320 Cudd_RecursiveDerefZdd(dd, f0); 01321 Cudd_RecursiveDerefZdd(dd, g1); 01322 Cudd_RecursiveDerefZdd(dd, g0); 01323 Cudd_RecursiveDerefZdd(dd, q); 01324 return(NULL); 01325 } 01326 Cudd_Ref(r); 01327 Cudd_RecursiveDerefZdd(dd, q); 01328 Cudd_RecursiveDerefZdd(dd, tmp); 01329 } 01330 01331 Cudd_RecursiveDerefZdd(dd, f1); 01332 Cudd_RecursiveDerefZdd(dd, f0); 01333 Cudd_RecursiveDerefZdd(dd, g1); 01334 Cudd_RecursiveDerefZdd(dd, g0); 01335 01336 cuddCacheInsert2(dd, cuddZddDivideF, f, g, r); 01337 Cudd_Deref(r); 01338 return(r); 01339 01340 } /* end of cuddZddDivideF */
Function********************************************************************
Synopsis [Computes the two-way decomposition of f w.r.t. v.]
Description []
SideEffects [The results are returned in f1 and f0.]
SeeAlso [cuddZddGetCofactors3]
Definition at line 1483 of file cuddZddFuncs.c.
01489 { 01490 *f1 = cuddZddSubset1(dd, f, v); 01491 if (*f1 == NULL) 01492 return(1); 01493 *f0 = cuddZddSubset0(dd, f, v); 01494 if (*f0 == NULL) { 01495 Cudd_RecursiveDerefZdd(dd, *f1); 01496 return(1); 01497 } 01498 return(0); 01499 01500 } /* end of cuddZddGetCofactors2 */
| int cuddZddGetCofactors3 | ( | DdManager * | dd, | |
| DdNode * | f, | |||
| int | v, | |||
| DdNode ** | f1, | |||
| DdNode ** | f0, | |||
| DdNode ** | fd | |||
| ) |
Function********************************************************************
Synopsis [Computes the three-way decomposition of f w.r.t. v.]
Description [Computes the three-way decomposition of function f (represented by a ZDD) wit respect to variable v. Returns 0 if successful; 1 otherwise.]
SideEffects [The results are returned in f1, f0, and fd.]
SeeAlso [cuddZddGetCofactors2]
Definition at line 1356 of file cuddZddFuncs.c.
01363 { 01364 DdNode *pc, *nc; 01365 DdNode *zero = DD_ZERO(dd); 01366 int top, hv, ht, pv, nv; 01367 int level; 01368 01369 top = dd->permZ[f->index]; 01370 level = dd->permZ[v]; 01371 hv = level >> 1; 01372 ht = top >> 1; 01373 01374 if (hv < ht) { 01375 *f1 = zero; 01376 *f0 = zero; 01377 *fd = f; 01378 } 01379 else { 01380 pv = cuddZddGetPosVarIndex(dd, v); 01381 nv = cuddZddGetNegVarIndex(dd, v); 01382 01383 /* not to create intermediate ZDD node */ 01384 if (cuddZddGetPosVarLevel(dd, v) < cuddZddGetNegVarLevel(dd, v)) { 01385 pc = cuddZddSubset1(dd, f, pv); 01386 if (pc == NULL) 01387 return(1); 01388 Cudd_Ref(pc); 01389 nc = cuddZddSubset0(dd, f, pv); 01390 if (nc == NULL) { 01391 Cudd_RecursiveDerefZdd(dd, pc); 01392 return(1); 01393 } 01394 Cudd_Ref(nc); 01395 01396 *f1 = cuddZddSubset0(dd, pc, nv); 01397 if (*f1 == NULL) { 01398 Cudd_RecursiveDerefZdd(dd, pc); 01399 Cudd_RecursiveDerefZdd(dd, nc); 01400 return(1); 01401 } 01402 Cudd_Ref(*f1); 01403 *f0 = cuddZddSubset1(dd, nc, nv); 01404 if (*f0 == NULL) { 01405 Cudd_RecursiveDerefZdd(dd, pc); 01406 Cudd_RecursiveDerefZdd(dd, nc); 01407 Cudd_RecursiveDerefZdd(dd, *f1); 01408 return(1); 01409 } 01410 Cudd_Ref(*f0); 01411 01412 *fd = cuddZddSubset0(dd, nc, nv); 01413 if (*fd == NULL) { 01414 Cudd_RecursiveDerefZdd(dd, pc); 01415 Cudd_RecursiveDerefZdd(dd, nc); 01416 Cudd_RecursiveDerefZdd(dd, *f1); 01417 Cudd_RecursiveDerefZdd(dd, *f0); 01418 return(1); 01419 } 01420 Cudd_Ref(*fd); 01421 } else { 01422 pc = cuddZddSubset1(dd, f, nv); 01423 if (pc == NULL) 01424 return(1); 01425 Cudd_Ref(pc); 01426 nc = cuddZddSubset0(dd, f, nv); 01427 if (nc == NULL) { 01428 Cudd_RecursiveDerefZdd(dd, pc); 01429 return(1); 01430 } 01431 Cudd_Ref(nc); 01432 01433 *f0 = cuddZddSubset0(dd, pc, pv); 01434 if (*f0 == NULL) { 01435 Cudd_RecursiveDerefZdd(dd, pc); 01436 Cudd_RecursiveDerefZdd(dd, nc); 01437 return(1); 01438 } 01439 Cudd_Ref(*f0); 01440 *f1 = cuddZddSubset1(dd, nc, pv); 01441 if (*f1 == NULL) { 01442 Cudd_RecursiveDerefZdd(dd, pc); 01443 Cudd_RecursiveDerefZdd(dd, nc); 01444 Cudd_RecursiveDerefZdd(dd, *f0); 01445 return(1); 01446 } 01447 Cudd_Ref(*f1); 01448 01449 *fd = cuddZddSubset0(dd, nc, pv); 01450 if (*fd == NULL) { 01451 Cudd_RecursiveDerefZdd(dd, pc); 01452 Cudd_RecursiveDerefZdd(dd, nc); 01453 Cudd_RecursiveDerefZdd(dd, *f1); 01454 Cudd_RecursiveDerefZdd(dd, *f0); 01455 return(1); 01456 } 01457 Cudd_Ref(*fd); 01458 } 01459 01460 Cudd_RecursiveDerefZdd(dd, pc); 01461 Cudd_RecursiveDerefZdd(dd, nc); 01462 Cudd_Deref(*f1); 01463 Cudd_Deref(*f0); 01464 Cudd_Deref(*fd); 01465 } 01466 return(0); 01467 01468 } /* end of cuddZddGetCofactors3 */
| int cuddZddGetNegVarIndex | ( | DdManager * | dd, | |
| int | index | |||
| ) |
Function********************************************************************
Synopsis [Returns the index of negative ZDD variable.]
Description [Returns the index of negative ZDD variable.]
SideEffects []
SeeAlso []
Definition at line 1582 of file cuddZddFuncs.c.
| int cuddZddGetNegVarLevel | ( | DdManager * | dd, | |
| int | index | |||
| ) |
Function********************************************************************
Synopsis [Returns the level of negative ZDD variable.]
Description [Returns the level of negative ZDD variable.]
SideEffects []
SeeAlso []
Definition at line 1624 of file cuddZddFuncs.c.
01627 { 01628 int nv = cuddZddGetNegVarIndex(dd, index); 01629 return(dd->permZ[nv]); 01630 } /* end of cuddZddGetNegVarLevel */
| int cuddZddGetPosVarIndex | ( | DdManager * | dd, | |
| int | index | |||
| ) |
Function********************************************************************
Synopsis [Returns the index of positive ZDD variable.]
Description [Returns the index of positive ZDD variable.]
SideEffects []
SeeAlso []
Definition at line 1561 of file cuddZddFuncs.c.
| int cuddZddGetPosVarLevel | ( | DdManager * | dd, | |
| int | index | |||
| ) |
Function********************************************************************
Synopsis [Returns the level of positive ZDD variable.]
Description [Returns the level of positive ZDD variable.]
SideEffects []
SeeAlso []
Definition at line 1603 of file cuddZddFuncs.c.
01606 { 01607 int pv = cuddZddGetPosVarIndex(dd, index); 01608 return(dd->permZ[pv]); 01609 } /* end of cuddZddGetPosVarLevel */
Function********************************************************************
Synopsis [Performs the recursive step of Cudd_zddProduct.]
Description []
SideEffects [None]
SeeAlso [Cudd_zddProduct]
Definition at line 376 of file cuddZddFuncs.c.
00380 { 00381 int v, top_f, top_g; 00382 DdNode *tmp, *term1, *term2, *term3; 00383 DdNode *f0, *f1, *fd, *g0, *g1, *gd; 00384 DdNode *R0, *R1, *Rd, *N0, *N1; 00385 DdNode *r; 00386 DdNode *one = DD_ONE(dd); 00387 DdNode *zero = DD_ZERO(dd); 00388 int flag; 00389 int pv, nv; 00390 00391 statLine(dd); 00392 if (f == zero || g == zero) 00393 return(zero); 00394 if (f == one) 00395 return(g); 00396 if (g == one) 00397 return(f); 00398 00399 top_f = dd->permZ[f->index]; 00400 top_g = dd->permZ[g->index]; 00401 00402 if (top_f > top_g) 00403 return(cuddZddProduct(dd, g, f)); 00404 00405 /* Check cache */ 00406 r = cuddCacheLookup2Zdd(dd, cuddZddProduct, f, g); 00407 if (r) 00408 return(r); 00409 00410 v = f->index; /* either yi or zi */ 00411 flag = cuddZddGetCofactors3(dd, f, v, &f1, &f0, &fd); 00412 if (flag == 1) 00413 return(NULL); 00414 Cudd_Ref(f1); 00415 Cudd_Ref(f0); 00416 Cudd_Ref(fd); 00417 flag = cuddZddGetCofactors3(dd, g, v, &g1, &g0, &gd); 00418 if (flag == 1) { 00419 Cudd_RecursiveDerefZdd(dd, f1); 00420 Cudd_RecursiveDerefZdd(dd, f0); 00421 Cudd_RecursiveDerefZdd(dd, fd); 00422 return(NULL); 00423 } 00424 Cudd_Ref(g1); 00425 Cudd_Ref(g0); 00426 Cudd_Ref(gd); 00427 pv = cuddZddGetPosVarIndex(dd, v); 00428 nv = cuddZddGetNegVarIndex(dd, v); 00429 00430 Rd = cuddZddProduct(dd, fd, gd); 00431 if (Rd == NULL) { 00432 Cudd_RecursiveDerefZdd(dd, f1); 00433 Cudd_RecursiveDerefZdd(dd, f0); 00434 Cudd_RecursiveDerefZdd(dd, fd); 00435 Cudd_RecursiveDerefZdd(dd, g1); 00436 Cudd_RecursiveDerefZdd(dd, g0); 00437 Cudd_RecursiveDerefZdd(dd, gd); 00438 return(NULL); 00439 } 00440 Cudd_Ref(Rd); 00441 00442 term1 = cuddZddProduct(dd, f0, g0); 00443 if (term1 == NULL) { 00444 Cudd_RecursiveDerefZdd(dd, f1); 00445 Cudd_RecursiveDerefZdd(dd, f0); 00446 Cudd_RecursiveDerefZdd(dd, fd); 00447 Cudd_RecursiveDerefZdd(dd, g1); 00448 Cudd_RecursiveDerefZdd(dd, g0); 00449 Cudd_RecursiveDerefZdd(dd, gd); 00450 Cudd_RecursiveDerefZdd(dd, Rd); 00451 return(NULL); 00452 } 00453 Cudd_Ref(term1); 00454 term2 = cuddZddProduct(dd, f0, gd); 00455 if (term2 == NULL) { 00456 Cudd_RecursiveDerefZdd(dd, f1); 00457 Cudd_RecursiveDerefZdd(dd, f0); 00458 Cudd_RecursiveDerefZdd(dd, fd); 00459 Cudd_RecursiveDerefZdd(dd, g1); 00460 Cudd_RecursiveDerefZdd(dd, g0); 00461 Cudd_RecursiveDerefZdd(dd, gd); 00462 Cudd_RecursiveDerefZdd(dd, Rd); 00463 Cudd_RecursiveDerefZdd(dd, term1); 00464 return(NULL); 00465 } 00466 Cudd_Ref(term2); 00467 term3 = cuddZddProduct(dd, fd, g0); 00468 if (term3 == NULL) { 00469 Cudd_RecursiveDerefZdd(dd, f1); 00470 Cudd_RecursiveDerefZdd(dd, f0); 00471 Cudd_RecursiveDerefZdd(dd, fd); 00472 Cudd_RecursiveDerefZdd(dd, g1); 00473 Cudd_RecursiveDerefZdd(dd, g0); 00474 Cudd_RecursiveDerefZdd(dd, gd); 00475 Cudd_RecursiveDerefZdd(dd, Rd); 00476 Cudd_RecursiveDerefZdd(dd, term1); 00477 Cudd_RecursiveDerefZdd(dd, term2); 00478 return(NULL); 00479 } 00480 Cudd_Ref(term3); 00481 Cudd_RecursiveDerefZdd(dd, f0); 00482 Cudd_RecursiveDerefZdd(dd, g0); 00483 tmp = cuddZddUnion(dd, term1, term2); 00484 if (tmp == NULL) { 00485 Cudd_RecursiveDerefZdd(dd, f1); 00486 Cudd_RecursiveDerefZdd(dd, fd); 00487 Cudd_RecursiveDerefZdd(dd, g1); 00488 Cudd_RecursiveDerefZdd(dd, gd); 00489 Cudd_RecursiveDerefZdd(dd, Rd); 00490 Cudd_RecursiveDerefZdd(dd, term1); 00491 Cudd_RecursiveDerefZdd(dd, term2); 00492 Cudd_RecursiveDerefZdd(dd, term3); 00493 return(NULL); 00494 } 00495 Cudd_Ref(tmp); 00496 Cudd_RecursiveDerefZdd(dd, term1); 00497 Cudd_RecursiveDerefZdd(dd, term2); 00498 R0 = cuddZddUnion(dd, tmp, term3); 00499 if (R0 == NULL) { 00500 Cudd_RecursiveDerefZdd(dd, f1); 00501 Cudd_RecursiveDerefZdd(dd, fd); 00502 Cudd_RecursiveDerefZdd(dd, g1); 00503 Cudd_RecursiveDerefZdd(dd, gd); 00504 Cudd_RecursiveDerefZdd(dd, Rd); 00505 Cudd_RecursiveDerefZdd(dd, term3); 00506 Cudd_RecursiveDerefZdd(dd, tmp); 00507 return(NULL); 00508 } 00509 Cudd_Ref(R0); 00510 Cudd_RecursiveDerefZdd(dd, tmp); 00511 Cudd_RecursiveDerefZdd(dd, term3); 00512 N0 = cuddZddGetNode(dd, nv, R0, Rd); /* nv = zi */ 00513 if (N0 == NULL) { 00514 Cudd_RecursiveDerefZdd(dd, f1); 00515 Cudd_RecursiveDerefZdd(dd, fd); 00516 Cudd_RecursiveDerefZdd(dd, g1); 00517 Cudd_RecursiveDerefZdd(dd, gd); 00518 Cudd_RecursiveDerefZdd(dd, Rd); 00519 Cudd_RecursiveDerefZdd(dd, R0); 00520 return(NULL); 00521 } 00522 Cudd_Ref(N0); 00523 Cudd_RecursiveDerefZdd(dd, R0); 00524 Cudd_RecursiveDerefZdd(dd, Rd); 00525 00526 term1 = cuddZddProduct(dd, f1, g1); 00527 if (term1 == NULL) { 00528 Cudd_RecursiveDerefZdd(dd, f1); 00529 Cudd_RecursiveDerefZdd(dd, fd); 00530 Cudd_RecursiveDerefZdd(dd, g1); 00531 Cudd_RecursiveDerefZdd(dd, gd); 00532 Cudd_RecursiveDerefZdd(dd, N0); 00533 return(NULL); 00534 } 00535 Cudd_Ref(term1); 00536 term2 = cuddZddProduct(dd, f1, gd); 00537 if (term2 == NULL) { 00538 Cudd_RecursiveDerefZdd(dd, f1); 00539 Cudd_RecursiveDerefZdd(dd, fd); 00540 Cudd_RecursiveDerefZdd(dd, g1); 00541 Cudd_RecursiveDerefZdd(dd, gd); 00542 Cudd_RecursiveDerefZdd(dd, N0); 00543 Cudd_RecursiveDerefZdd(dd, term1); 00544 return(NULL); 00545 } 00546 Cudd_Ref(term2); 00547 term3 = cuddZddProduct(dd, fd, g1); 00548 if (term3 == NULL) { 00549 Cudd_RecursiveDerefZdd(dd, f1); 00550 Cudd_RecursiveDerefZdd(dd, fd); 00551 Cudd_RecursiveDerefZdd(dd, g1); 00552 Cudd_RecursiveDerefZdd(dd, gd); 00553 Cudd_RecursiveDerefZdd(dd, N0); 00554 Cudd_RecursiveDerefZdd(dd, term1); 00555 Cudd_RecursiveDerefZdd(dd, term2); 00556 return(NULL); 00557 } 00558 Cudd_Ref(term3); 00559 Cudd_RecursiveDerefZdd(dd, f1); 00560 Cudd_RecursiveDerefZdd(dd, g1); 00561 Cudd_RecursiveDerefZdd(dd, fd); 00562 Cudd_RecursiveDerefZdd(dd, gd); 00563 tmp = cuddZddUnion(dd, term1, term2); 00564 if (tmp == NULL) { 00565 Cudd_RecursiveDerefZdd(dd, N0); 00566 Cudd_RecursiveDerefZdd(dd, term1); 00567 Cudd_RecursiveDerefZdd(dd, term2); 00568 Cudd_RecursiveDerefZdd(dd, term3); 00569 return(NULL); 00570 } 00571 Cudd_Ref(tmp); 00572 Cudd_RecursiveDerefZdd(dd, term1); 00573 Cudd_RecursiveDerefZdd(dd, term2); 00574 R1 = cuddZddUnion(dd, tmp, term3); 00575 if (R1 == NULL) { 00576 Cudd_RecursiveDerefZdd(dd, N0); 00577 Cudd_RecursiveDerefZdd(dd, term3); 00578 Cudd_RecursiveDerefZdd(dd, tmp); 00579 return(NULL); 00580 } 00581 Cudd_Ref(R1); 00582 Cudd_RecursiveDerefZdd(dd, tmp); 00583 Cudd_RecursiveDerefZdd(dd, term3); 00584 N1 = cuddZddGetNode(dd, pv, R1, N0); /* pv = yi */ 00585 if (N1 == NULL) { 00586 Cudd_RecursiveDerefZdd(dd, N0); 00587 Cudd_RecursiveDerefZdd(dd, R1); 00588 return(NULL); 00589 } 00590 Cudd_Ref(N1); 00591 Cudd_RecursiveDerefZdd(dd, R1); 00592 Cudd_RecursiveDerefZdd(dd, N0); 00593 00594 cuddCacheInsert2(dd, cuddZddProduct, f, g, N1); 00595 Cudd_Deref(N1); 00596 return(N1); 00597 00598 } /* end of cuddZddProduct */
Function********************************************************************
Synopsis [Performs the recursive step of Cudd_zddUnateProduct.]
Description []
SideEffects [None]
SeeAlso [Cudd_zddUnateProduct]
Definition at line 613 of file cuddZddFuncs.c.
00617 { 00618 int v, top_f, top_g; 00619 DdNode *term1, *term2, *term3, *term4; 00620 DdNode *sum1, *sum2; 00621 DdNode *f0, *f1, *g0, *g1; 00622 DdNode *r; 00623 DdNode *one = DD_ONE(dd); 00624 DdNode *zero = DD_ZERO(dd); 00625 int flag; 00626 00627 statLine(dd); 00628 if (f == zero || g == zero) 00629 return(zero); 00630 if (f == one) 00631 return(g); 00632 if (g == one) 00633 return(f); 00634 00635 top_f = dd->permZ[f->index]; 00636 top_g = dd->permZ[g->index]; 00637 00638 if (top_f > top_g) 00639 return(cuddZddUnateProduct(dd, g, f)); 00640 00641 /* Check cache */ 00642 r = cuddCacheLookup2Zdd(dd, cuddZddUnateProduct, f, g); 00643 if (r) 00644 return(r); 00645 00646 v = f->index; /* either yi or zi */ 00647 flag = cuddZddGetCofactors2(dd, f, v, &f1, &f0); 00648 if (flag == 1) 00649 return(NULL); 00650 Cudd_Ref(f1); 00651 Cudd_Ref(f0); 00652 flag = cuddZddGetCofactors2(dd, g, v, &g1, &g0); 00653 if (flag == 1) { 00654 Cudd_RecursiveDerefZdd(dd, f1); 00655 Cudd_RecursiveDerefZdd(dd, f0); 00656 return(NULL); 00657 } 00658 Cudd_Ref(g1); 00659 Cudd_Ref(g0); 00660 00661 term1 = cuddZddUnateProduct(dd, f1, g1); 00662 if (term1 == NULL) { 00663 Cudd_RecursiveDerefZdd(dd, f1); 00664 Cudd_RecursiveDerefZdd(dd, f0); 00665 Cudd_RecursiveDerefZdd(dd, g1); 00666 Cudd_RecursiveDerefZdd(dd, g0); 00667 return(NULL); 00668 } 00669 Cudd_Ref(term1); 00670 term2 = cuddZddUnateProduct(dd, f1, g0); 00671 if (term2 == NULL) { 00672 Cudd_RecursiveDerefZdd(dd, f1); 00673 Cudd_RecursiveDerefZdd(dd, f0); 00674 Cudd_RecursiveDerefZdd(dd, g1); 00675 Cudd_RecursiveDerefZdd(dd, g0); 00676 Cudd_RecursiveDerefZdd(dd, term1); 00677 return(NULL); 00678 } 00679 Cudd_Ref(term2); 00680 term3 = cuddZddUnateProduct(dd, f0, g1); 00681 if (term3 == NULL) { 00682 Cudd_RecursiveDerefZdd(dd, f1); 00683 Cudd_RecursiveDerefZdd(dd, f0); 00684 Cudd_RecursiveDerefZdd(dd, g1); 00685 Cudd_RecursiveDerefZdd(dd, g0); 00686 Cudd_RecursiveDerefZdd(dd, term1); 00687 Cudd_RecursiveDerefZdd(dd, term2); 00688 return(NULL); 00689 } 00690 Cudd_Ref(term3); 00691 term4 = cuddZddUnateProduct(dd, f0, g0); 00692 if (term4 == NULL) { 00693 Cudd_RecursiveDerefZdd(dd, f1); 00694 Cudd_RecursiveDerefZdd(dd, f0); 00695 Cudd_RecursiveDerefZdd(dd, g1); 00696 Cudd_RecursiveDerefZdd(dd, g0); 00697 Cudd_RecursiveDerefZdd(dd, term1); 00698 Cudd_RecursiveDerefZdd(dd, term2); 00699 Cudd_RecursiveDerefZdd(dd, term3); 00700 return(NULL); 00701 } 00702 Cudd_Ref(term4); 00703 Cudd_RecursiveDerefZdd(dd, f1); 00704 Cudd_RecursiveDerefZdd(dd, f0); 00705 Cudd_RecursiveDerefZdd(dd, g1); 00706 Cudd_RecursiveDerefZdd(dd, g0); 00707 sum1 = cuddZddUnion(dd, term1, term2); 00708 if (sum1 == NULL) { 00709 Cudd_RecursiveDerefZdd(dd, term1); 00710 Cudd_RecursiveDerefZdd(dd, term2); 00711 Cudd_RecursiveDerefZdd(dd, term3); 00712 Cudd_RecursiveDerefZdd(dd, term4); 00713 return(NULL); 00714 } 00715 Cudd_Ref(sum1); 00716 Cudd_RecursiveDerefZdd(dd, term1); 00717 Cudd_RecursiveDerefZdd(dd, term2); 00718 sum2 = cuddZddUnion(dd, sum1, term3); 00719 if (sum2 == NULL) { 00720 Cudd_RecursiveDerefZdd(dd, term3); 00721 Cudd_RecursiveDerefZdd(dd, term4); 00722 Cudd_RecursiveDerefZdd(dd, sum1); 00723 return(NULL); 00724 } 00725 Cudd_Ref(sum2); 00726 Cudd_RecursiveDerefZdd(dd, sum1); 00727 Cudd_RecursiveDerefZdd(dd, term3); 00728 r = cuddZddGetNode(dd, v, sum2, term4); 00729 if (r == NULL) { 00730 Cudd_RecursiveDerefZdd(dd, term4); 00731 Cudd_RecursiveDerefZdd(dd, sum2); 00732 return(NULL); 00733 } 00734 Cudd_Ref(r); 00735 Cudd_RecursiveDerefZdd(dd, sum2); 00736 Cudd_RecursiveDerefZdd(dd, term4); 00737 00738 cuddCacheInsert2(dd, cuddZddUnateProduct, f, g, r); 00739 Cudd_Deref(r); 00740 return(r); 00741 00742 } /* end of cuddZddUnateProduct */
Function********************************************************************
Synopsis [Performs the recursive step of Cudd_zddWeakDiv.]
Description []
SideEffects [None]
SeeAlso [Cudd_zddWeakDiv]
Definition at line 757 of file cuddZddFuncs.c.
00761 { 00762 int v; 00763 DdNode *one = DD_ONE(dd); 00764 DdNode *zero = DD_ZERO(dd); 00765 DdNode *f0, *f1, *fd, *g0, *g1, *gd; 00766 DdNode *q, *tmp; 00767 DdNode *r; 00768 int flag; 00769 00770 statLine(dd); 00771 if (g == one) 00772 return(f); 00773 if (f == zero || f == one) 00774 return(zero); 00775 if (f == g) 00776 return(one); 00777 00778 /* Check cache. */ 00779 r = cuddCacheLookup2Zdd(dd, cuddZddWeakDiv, f, g); 00780 if (r) 00781 return(r); 00782 00783 v = g->index; 00784 00785 flag = cuddZddGetCofactors3(dd, f, v, &f1, &f0, &fd); 00786 if (flag == 1) 00787 return(NULL); 00788 Cudd_Ref(f1); 00789 Cudd_Ref(f0); 00790 Cudd_Ref(fd); 00791 flag = cuddZddGetCofactors3(dd, g, v, &g1, &g0, &gd); 00792 if (flag == 1) { 00793 Cudd_RecursiveDerefZdd(dd, f1); 00794 Cudd_RecursiveDerefZdd(dd, f0); 00795 Cudd_RecursiveDerefZdd(dd, fd); 00796 return(NULL); 00797 } 00798 Cudd_Ref(g1); 00799 Cudd_Ref(g0); 00800 Cudd_Ref(gd); 00801 00802 q = g; 00803 00804 if (g0 != zero) { 00805 q = cuddZddWeakDiv(dd, f0, g0); 00806 if (q == NULL) { 00807 Cudd_RecursiveDerefZdd(dd, f1); 00808 Cudd_RecursiveDerefZdd(dd, f0); 00809 Cudd_RecursiveDerefZdd(dd, fd); 00810 Cudd_RecursiveDerefZdd(dd, g1); 00811 Cudd_RecursiveDerefZdd(dd, g0); 00812 Cudd_RecursiveDerefZdd(dd, gd); 00813 return(NULL); 00814 } 00815 Cudd_Ref(q); 00816 } 00817 else 00818 Cudd_Ref(q); 00819 Cudd_RecursiveDerefZdd(dd, f0); 00820 Cudd_RecursiveDerefZdd(dd, g0); 00821 00822 if (q == zero) { 00823 Cudd_RecursiveDerefZdd(dd, f1); 00824 Cudd_RecursiveDerefZdd(dd, g1); 00825 Cudd_RecursiveDerefZdd(dd, fd); 00826 Cudd_RecursiveDerefZdd(dd, gd); 00827 cuddCacheInsert2(dd, cuddZddWeakDiv, f, g, zero); 00828 Cudd_Deref(q); 00829 return(zero); 00830 } 00831 00832 if (g1 != zero) { 00833 Cudd_RecursiveDerefZdd(dd, q); 00834 tmp = cuddZddWeakDiv(dd, f1, g1); 00835 if (tmp == NULL) { 00836 Cudd_RecursiveDerefZdd(dd, f1); 00837 Cudd_RecursiveDerefZdd(dd, g1); 00838 Cudd_RecursiveDerefZdd(dd, fd); 00839 Cudd_RecursiveDerefZdd(dd, gd); 00840 return(NULL); 00841 } 00842 Cudd_Ref(tmp); 00843 Cudd_RecursiveDerefZdd(dd, f1); 00844 Cudd_RecursiveDerefZdd(dd, g1); 00845 if (q == g) 00846 q = tmp; 00847 else { 00848 q = cuddZddIntersect(dd, q, tmp); 00849 if (q == NULL) { 00850 Cudd_RecursiveDerefZdd(dd, fd); 00851 Cudd_RecursiveDerefZdd(dd, gd); 00852 return(NULL); 00853 } 00854 Cudd_Ref(q); 00855 Cudd_RecursiveDerefZdd(dd, tmp); 00856 } 00857 } 00858 else { 00859 Cudd_RecursiveDerefZdd(dd, f1); 00860 Cudd_RecursiveDerefZdd(dd, g1); 00861 } 00862 00863 if (q == zero) { 00864 Cudd_RecursiveDerefZdd(dd, fd); 00865 Cudd_RecursiveDerefZdd(dd, gd); 00866 cuddCacheInsert2(dd, cuddZddWeakDiv, f, g, zero); 00867 Cudd_Deref(q); 00868 return(zero); 00869 } 00870 00871 if (gd != zero) { 00872 Cudd_RecursiveDerefZdd(dd, q); 00873 tmp = cuddZddWeakDiv(dd, fd, gd); 00874 if (tmp == NULL) { 00875 Cudd_RecursiveDerefZdd(dd, fd); 00876 Cudd_RecursiveDerefZdd(dd, gd); 00877 return(NULL); 00878 } 00879 Cudd_Ref(tmp); 00880 Cudd_RecursiveDerefZdd(dd, fd); 00881 Cudd_RecursiveDerefZdd(dd, gd); 00882 if (q == g) 00883 q = tmp; 00884 else { 00885 q = cuddZddIntersect(dd, q, tmp); 00886 if (q == NULL) { 00887 Cudd_RecursiveDerefZdd(dd, tmp); 00888 return(NULL); 00889 } 00890 Cudd_Ref(q); 00891 Cudd_RecursiveDerefZdd(dd, tmp); 00892 } 00893 } 00894 else { 00895 Cudd_RecursiveDerefZdd(dd, fd); 00896 Cudd_RecursiveDerefZdd(dd, gd); 00897 } 00898 00899 cuddCacheInsert2(dd, cuddZddWeakDiv, f, g, q); 00900 Cudd_Deref(q); 00901 return(q); 00902 00903 } /* end of cuddZddWeakDiv */
Function********************************************************************
Synopsis [Performs the recursive step of Cudd_zddWeakDivF.]
Description []
SideEffects [None]
SeeAlso [Cudd_zddWeakDivF]
Definition at line 918 of file cuddZddFuncs.c.
00922 { 00923 int v, top_f, top_g, vf, vg; 00924 DdNode *one = DD_ONE(dd); 00925 DdNode *zero = DD_ZERO(dd); 00926 DdNode *f0, *f1, *fd, *g0, *g1, *gd; 00927 DdNode *q, *tmp; 00928 DdNode *r; 00929 DdNode *term1, *term0, *termd; 00930 int flag; 00931 int pv, nv; 00932 00933 statLine(dd); 00934 if (g == one) 00935 return(f); 00936 if (f == zero || f == one) 00937 return(zero); 00938 if (f == g) 00939 return(one); 00940 00941 /* Check cache. */ 00942 r = cuddCacheLookup2Zdd(dd, cuddZddWeakDivF, f, g); 00943 if (r) 00944 return(r); 00945 00946 top_f = dd->permZ[f->index]; 00947 top_g = dd->permZ[g->index]; 00948 vf = top_f >> 1; 00949 vg = top_g >> 1; 00950 v = ddMin(top_f, top_g); 00951 00952 if (v == top_f && vf < vg) { 00953 v = f->index; 00954 flag = cuddZddGetCofactors3(dd, f, v, &f1, &f0, &fd); 00955 if (flag == 1) 00956 return(NULL); 00957 Cudd_Ref(f1); 00958 Cudd_Ref(f0); 00959 Cudd_Ref(fd); 00960 00961 pv = cuddZddGetPosVarIndex(dd, v); 00962 nv = cuddZddGetNegVarIndex(dd, v); 00963 00964 term1 = cuddZddWeakDivF(dd, f1, g); 00965 if (term1 == NULL) { 00966 Cudd_RecursiveDerefZdd(dd, f1); 00967 Cudd_RecursiveDerefZdd(dd, f0); 00968 Cudd_RecursiveDerefZdd(dd, fd); 00969 return(NULL); 00970 } 00971 Cudd_Ref(term1); 00972 Cudd_RecursiveDerefZdd(dd, f1); 00973 term0 = cuddZddWeakDivF(dd, f0, g); 00974 if (term0 == NULL) { 00975 Cudd_RecursiveDerefZdd(dd, f0); 00976 Cudd_RecursiveDerefZdd(dd, fd); 00977 Cudd_RecursiveDerefZdd(dd, term1); 00978 return(NULL); 00979 } 00980 Cudd_Ref(term0); 00981 Cudd_RecursiveDerefZdd(dd, f0); 00982 termd = cuddZddWeakDivF(dd, fd, g); 00983 if (termd == NULL) { 00984 Cudd_RecursiveDerefZdd(dd, fd); 00985 Cudd_RecursiveDerefZdd(dd, term1); 00986 Cudd_RecursiveDerefZdd(dd, term0); 00987 return(NULL); 00988 } 00989 Cudd_Ref(termd); 00990 Cudd_RecursiveDerefZdd(dd, fd); 00991 00992 tmp = cuddZddGetNode(dd, nv, term0, termd); /* nv = zi */ 00993 if (tmp == NULL) { 00994 Cudd_RecursiveDerefZdd(dd, term1); 00995 Cudd_RecursiveDerefZdd(dd, term0); 00996 Cudd_RecursiveDerefZdd(dd, termd); 00997 return(NULL); 00998 } 00999 Cudd_Ref(tmp); 01000 Cudd_RecursiveDerefZdd(dd, term0); 01001 Cudd_RecursiveDerefZdd(dd, termd); 01002 q = cuddZddGetNode(dd, pv, term1, tmp); /* pv = yi */ 01003 if (q == NULL) { 01004 Cudd_RecursiveDerefZdd(dd, term1); 01005 Cudd_RecursiveDerefZdd(dd, tmp); 01006 return(NULL); 01007 } 01008 Cudd_Ref(q); 01009 Cudd_RecursiveDerefZdd(dd, term1); 01010 Cudd_RecursiveDerefZdd(dd, tmp); 01011 01012 cuddCacheInsert2(dd, cuddZddWeakDivF, f, g, q); 01013 Cudd_Deref(q); 01014 return(q); 01015 } 01016 01017 if (v == top_f) 01018 v = f->index; 01019 else 01020 v = g->index; 01021 01022 flag = cuddZddGetCofactors3(dd, f, v, &f1, &f0, &fd); 01023 if (flag == 1) 01024 return(NULL); 01025 Cudd_Ref(f1); 01026 Cudd_Ref(f0); 01027 Cudd_Ref(fd); 01028 flag = cuddZddGetCofactors3(dd, g, v, &g1, &g0, &gd); 01029 if (flag == 1) { 01030 Cudd_RecursiveDerefZdd(dd, f1); 01031 Cudd_RecursiveDerefZdd(dd, f0); 01032 Cudd_RecursiveDerefZdd(dd, fd); 01033 return(NULL); 01034 } 01035 Cudd_Ref(g1); 01036 Cudd_Ref(g0); 01037 Cudd_Ref(gd); 01038 01039 q = g; 01040 01041 if (g0 != zero) { 01042 q = cuddZddWeakDivF(dd, f0, g0); 01043 if (q == NULL) { 01044 Cudd_RecursiveDerefZdd(dd, f1); 01045 Cudd_RecursiveDerefZdd(dd, f0); 01046 Cudd_RecursiveDerefZdd(dd, fd); 01047 Cudd_RecursiveDerefZdd(dd, g1); 01048 Cudd_RecursiveDerefZdd(dd, g0); 01049 Cudd_RecursiveDerefZdd(dd, gd); 01050 return(NULL); 01051 } 01052 Cudd_Ref(q); 01053 } 01054 else 01055 Cudd_Ref(q); 01056 Cudd_RecursiveDerefZdd(dd, f0); 01057 Cudd_RecursiveDerefZdd(dd, g0); 01058 01059 if (q == zero) { 01060 Cudd_RecursiveDerefZdd(dd, f1); 01061 Cudd_RecursiveDerefZdd(dd, g1); 01062 Cudd_RecursiveDerefZdd(dd, fd); 01063 Cudd_RecursiveDerefZdd(dd, gd); 01064 cuddCacheInsert2(dd, cuddZddWeakDivF, f, g, zero); 01065 Cudd_Deref(q); 01066 return(zero); 01067 } 01068 01069 if (g1 != zero) { 01070 Cudd_RecursiveDerefZdd(dd, q); 01071 tmp = cuddZddWeakDivF(dd, f1, g1); 01072 if (tmp == NULL) { 01073 Cudd_RecursiveDerefZdd(dd, f1); 01074 Cudd_RecursiveDerefZdd(dd, g1); 01075 Cudd_RecursiveDerefZdd(dd, fd); 01076 Cudd_RecursiveDerefZdd(dd, gd); 01077 return(NULL); 01078 } 01079 Cudd_Ref(tmp); 01080 Cudd_RecursiveDerefZdd(dd, f1); 01081 Cudd_RecursiveDerefZdd(dd, g1); 01082 if (q == g) 01083 q = tmp; 01084 else { 01085 q = cuddZddIntersect(dd, q, tmp); 01086 if (q == NULL) { 01087 Cudd_RecursiveDerefZdd(dd, fd); 01088 Cudd_RecursiveDerefZdd(dd, gd); 01089 return(NULL); 01090 } 01091 Cudd_Ref(q); 01092 Cudd_RecursiveDerefZdd(dd, tmp); 01093 } 01094 } 01095 else { 01096 Cudd_RecursiveDerefZdd(dd, f1); 01097 Cudd_RecursiveDerefZdd(dd, g1); 01098 } 01099 01100 if (q == zero) { 01101 Cudd_RecursiveDerefZdd(dd, fd); 01102 Cudd_RecursiveDerefZdd(dd, gd); 01103 cuddCacheInsert2(dd, cuddZddWeakDivF, f, g, zero); 01104 Cudd_Deref(q); 01105 return(zero); 01106 } 01107 01108 if (gd != zero) { 01109 Cudd_RecursiveDerefZdd(dd, q); 01110 tmp = cuddZddWeakDivF(dd, fd, gd); 01111 if (tmp == NULL) { 01112 Cudd_RecursiveDerefZdd(dd, fd); 01113 Cudd_RecursiveDerefZdd(dd, gd); 01114 return(NULL); 01115 } 01116 Cudd_Ref(tmp); 01117 Cudd_RecursiveDerefZdd(dd, fd); 01118 Cudd_RecursiveDerefZdd(dd, gd); 01119 if (q == g) 01120 q = tmp; 01121 else { 01122 q = cuddZddIntersect(dd, q, tmp); 01123 if (q == NULL) { 01124 Cudd_RecursiveDerefZdd(dd, tmp); 01125 return(NULL); 01126 } 01127 Cudd_Ref(q); 01128 Cudd_RecursiveDerefZdd(dd, tmp); 01129 } 01130 } 01131 else { 01132 Cudd_RecursiveDerefZdd(dd, fd); 01133 Cudd_RecursiveDerefZdd(dd, gd); 01134 } 01135 01136 cuddCacheInsert2(dd, cuddZddWeakDivF, f, g, q); 01137 Cudd_Deref(q); 01138 return(q); 01139 01140 } /* end of cuddZddWeakDivF */
Variable Documentation
char rcsid [] DD_UNUSED = "$Id: cuddZddFuncs.c,v 1.16 2008/04/25 07:39:33 fabio Exp $" [static] |
CFile***********************************************************************
FileName [cuddZddFuncs.c]
PackageName [cudd]
Synopsis [Functions to manipulate covers represented as ZDDs.]
Description [External procedures included in this module:
- Cudd_zddProduct();
- Cudd_zddUnateProduct();
- Cudd_zddWeakDiv();
- Cudd_zddWeakDivF();
- Cudd_zddDivide();
- Cudd_zddDivideF();
- Cudd_zddComplement();
Internal procedures included in this module:
- cuddZddProduct();
- cuddZddUnateProduct();
- cuddZddWeakDiv();
- cuddZddWeakDivF();
- cuddZddDivide();
- cuddZddDivideF();
- cuddZddGetCofactors3()
- cuddZddGetCofactors2()
- cuddZddComplement();
- cuddZddGetPosVarIndex();
- cuddZddGetNegVarIndex();
- cuddZddGetPosVarLevel();
- cuddZddGetNegVarLevel();
Static procedures included in this module:
SeeAlso []
Author [In-Ho Moon]
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 101 of file cuddZddFuncs.c.
