src/bdd/cudd/cuddZddFuncs.c File Reference
#include "util_hack.h"#include "cuddInt.h"
Include dependency graph for cuddZddFuncs.c:
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 301 of file cuddZddFuncs.c.
00304 { 00305 DdNode *b, *isop, *zdd_I; 00306 00307 /* Check cache */ 00308 zdd_I = cuddCacheLookup1Zdd(dd, cuddZddComplement, node); 00309 if (zdd_I) 00310 return(zdd_I); 00311 00312 b = Cudd_MakeBddFromZddCover(dd, node); 00313 if (!b) 00314 return(NULL); 00315 Cudd_Ref(b); 00316 isop = Cudd_zddIsop(dd, Cudd_Not(b), Cudd_Not(b), &zdd_I); 00317 if (!isop) { 00318 Cudd_RecursiveDeref(dd, b); 00319 return(NULL); 00320 } 00321 Cudd_Ref(isop); 00322 Cudd_Ref(zdd_I); 00323 Cudd_RecursiveDeref(dd, b); 00324 Cudd_RecursiveDeref(dd, isop); 00325 00326 cuddCacheInsert1(dd, cuddZddComplement, node, zdd_I); 00327 Cudd_Deref(zdd_I); 00328 return(zdd_I); 00329 } /* 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 210 of file cuddZddFuncs.c.
00214 { 00215 DdNode *res; 00216 00217 do { 00218 dd->reordered = 0; 00219 res = cuddZddDivide(dd, f, g); 00220 } while (dd->reordered == 1); 00221 return(res); 00222 00223 } /* 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 268 of file cuddZddFuncs.c.
00272 { 00273 DdNode *res; 00274 00275 do { 00276 dd->reordered = 0; 00277 res = cuddZddDivideF(dd, f, g); 00278 } while (dd->reordered == 1); 00279 return(res); 00280 00281 } /* 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 114 of file cuddZddFuncs.c.
00118 { 00119 DdNode *res; 00120 00121 do { 00122 dd->reordered = 0; 00123 res = cuddZddProduct(dd, f, g); 00124 } while (dd->reordered == 1); 00125 return(res); 00126 00127 } /* 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 145 of file cuddZddFuncs.c.
00149 { 00150 DdNode *res; 00151 00152 do { 00153 dd->reordered = 0; 00154 res = cuddZddUnateProduct(dd, f, g); 00155 } while (dd->reordered == 1); 00156 return(res); 00157 00158 } /* 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 179 of file cuddZddFuncs.c.
00183 { 00184 DdNode *res; 00185 00186 do { 00187 dd->reordered = 0; 00188 res = cuddZddWeakDiv(dd, f, g); 00189 } while (dd->reordered == 1); 00190 return(res); 00191 00192 } /* 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 239 of file cuddZddFuncs.c.
00243 { 00244 DdNode *res; 00245 00246 do { 00247 dd->reordered = 0; 00248 res = cuddZddWeakDivF(dd, f, g); 00249 } while (dd->reordered == 1); 00250 return(res); 00251 00252 } /* 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 1491 of file cuddZddFuncs.c.
01494 { 01495 DdNode *b, *isop, *zdd_I; 01496 01497 /* Check cache */ 01498 zdd_I = cuddCacheLookup1Zdd(dd, cuddZddComplement, node); 01499 if (zdd_I) 01500 return(zdd_I); 01501 01502 b = cuddMakeBddFromZddCover(dd, node); 01503 if (!b) 01504 return(NULL); 01505 cuddRef(b); 01506 isop = cuddZddIsop(dd, Cudd_Not(b), Cudd_Not(b), &zdd_I); 01507 if (!isop) { 01508 Cudd_RecursiveDeref(dd, b); 01509 return(NULL); 01510 } 01511 cuddRef(isop); 01512 cuddRef(zdd_I); 01513 Cudd_RecursiveDeref(dd, b); 01514 Cudd_RecursiveDeref(dd, isop); 01515 01516 cuddCacheInsert1(dd, cuddZddComplement, node, zdd_I); 01517 cuddDeref(zdd_I); 01518 return(zdd_I); 01519 } /* end of cuddZddComplement */
Function********************************************************************
Synopsis [Performs the recursive step of Cudd_zddDivide.]
Description []
SideEffects [None]
SeeAlso [Cudd_zddDivide]
Definition at line 1128 of file cuddZddFuncs.c.
01132 { 01133 int v; 01134 DdNode *one = DD_ONE(dd); 01135 DdNode *zero = DD_ZERO(dd); 01136 DdNode *f0, *f1, *g0, *g1; 01137 DdNode *q, *r, *tmp; 01138 int flag; 01139 01140 statLine(dd); 01141 if (g == one) 01142 return(f); 01143 if (f == zero || f == one) 01144 return(zero); 01145 if (f == g) 01146 return(one); 01147 01148 /* Check cache. */ 01149 r = cuddCacheLookup2Zdd(dd, cuddZddDivide, f, g); 01150 if (r) 01151 return(r); 01152 01153 v = g->index; 01154 01155 flag = cuddZddGetCofactors2(dd, f, v, &f1, &f0); 01156 if (flag == 1) 01157 return(NULL); 01158 Cudd_Ref(f1); 01159 Cudd_Ref(f0); 01160 flag = cuddZddGetCofactors2(dd, g, v, &g1, &g0); /* g1 != zero */ 01161 if (flag == 1) { 01162 Cudd_RecursiveDerefZdd(dd, f1); 01163 Cudd_RecursiveDerefZdd(dd, f0); 01164 return(NULL); 01165 } 01166 Cudd_Ref(g1); 01167 Cudd_Ref(g0); 01168 01169 r = cuddZddDivide(dd, f1, g1); 01170 if (r == NULL) { 01171 Cudd_RecursiveDerefZdd(dd, f1); 01172 Cudd_RecursiveDerefZdd(dd, f0); 01173 Cudd_RecursiveDerefZdd(dd, g1); 01174 Cudd_RecursiveDerefZdd(dd, g0); 01175 return(NULL); 01176 } 01177 Cudd_Ref(r); 01178 01179 if (r != zero && g0 != zero) { 01180 tmp = r; 01181 q = cuddZddDivide(dd, f0, g0); 01182 if (q == NULL) { 01183 Cudd_RecursiveDerefZdd(dd, f1); 01184 Cudd_RecursiveDerefZdd(dd, f0); 01185 Cudd_RecursiveDerefZdd(dd, g1); 01186 Cudd_RecursiveDerefZdd(dd, g0); 01187 return(NULL); 01188 } 01189 Cudd_Ref(q); 01190 r = cuddZddIntersect(dd, r, q); 01191 if (r == NULL) { 01192 Cudd_RecursiveDerefZdd(dd, f1); 01193 Cudd_RecursiveDerefZdd(dd, f0); 01194 Cudd_RecursiveDerefZdd(dd, g1); 01195 Cudd_RecursiveDerefZdd(dd, g0); 01196 Cudd_RecursiveDerefZdd(dd, q); 01197 return(NULL); 01198 } 01199 Cudd_Ref(r); 01200 Cudd_RecursiveDerefZdd(dd, q); 01201 Cudd_RecursiveDerefZdd(dd, tmp); 01202 } 01203 01204 Cudd_RecursiveDerefZdd(dd, f1); 01205 Cudd_RecursiveDerefZdd(dd, f0); 01206 Cudd_RecursiveDerefZdd(dd, g1); 01207 Cudd_RecursiveDerefZdd(dd, g0); 01208 01209 cuddCacheInsert2(dd, cuddZddDivide, f, g, r); 01210 Cudd_Deref(r); 01211 return(r); 01212 01213 } /* end of cuddZddDivide */
Function********************************************************************
Synopsis [Performs the recursive step of Cudd_zddDivideF.]
Description []
SideEffects [None]
SeeAlso [Cudd_zddDivideF]
Definition at line 1228 of file cuddZddFuncs.c.
01232 { 01233 int v; 01234 DdNode *one = DD_ONE(dd); 01235 DdNode *zero = DD_ZERO(dd); 01236 DdNode *f0, *f1, *g0, *g1; 01237 DdNode *q, *r, *tmp; 01238 int flag; 01239 01240 statLine(dd); 01241 if (g == one) 01242 return(f); 01243 if (f == zero || f == one) 01244 return(zero); 01245 if (f == g) 01246 return(one); 01247 01248 /* Check cache. */ 01249 r = cuddCacheLookup2Zdd(dd, cuddZddDivideF, f, g); 01250 if (r) 01251 return(r); 01252 01253 v = g->index; 01254 01255 flag = cuddZddGetCofactors2(dd, f, v, &f1, &f0); 01256 if (flag == 1) 01257 return(NULL); 01258 Cudd_Ref(f1); 01259 Cudd_Ref(f0); 01260 flag = cuddZddGetCofactors2(dd, g, v, &g1, &g0); /* g1 != zero */ 01261 if (flag == 1) { 01262 Cudd_RecursiveDerefZdd(dd, f1); 01263 Cudd_RecursiveDerefZdd(dd, f0); 01264 return(NULL); 01265 } 01266 Cudd_Ref(g1); 01267 Cudd_Ref(g0); 01268 01269 r = cuddZddDivideF(dd, f1, g1); 01270 if (r == NULL) { 01271 Cudd_RecursiveDerefZdd(dd, f1); 01272 Cudd_RecursiveDerefZdd(dd, f0); 01273 Cudd_RecursiveDerefZdd(dd, g1); 01274 Cudd_RecursiveDerefZdd(dd, g0); 01275 return(NULL); 01276 } 01277 Cudd_Ref(r); 01278 01279 if (r != zero && g0 != zero) { 01280 tmp = r; 01281 q = cuddZddDivideF(dd, f0, g0); 01282 if (q == NULL) { 01283 Cudd_RecursiveDerefZdd(dd, f1); 01284 Cudd_RecursiveDerefZdd(dd, f0); 01285 Cudd_RecursiveDerefZdd(dd, g1); 01286 Cudd_RecursiveDerefZdd(dd, g0); 01287 return(NULL); 01288 } 01289 Cudd_Ref(q); 01290 r = cuddZddIntersect(dd, r, q); 01291 if (r == NULL) { 01292 Cudd_RecursiveDerefZdd(dd, f1); 01293 Cudd_RecursiveDerefZdd(dd, f0); 01294 Cudd_RecursiveDerefZdd(dd, g1); 01295 Cudd_RecursiveDerefZdd(dd, g0); 01296 Cudd_RecursiveDerefZdd(dd, q); 01297 return(NULL); 01298 } 01299 Cudd_Ref(r); 01300 Cudd_RecursiveDerefZdd(dd, q); 01301 Cudd_RecursiveDerefZdd(dd, tmp); 01302 } 01303 01304 Cudd_RecursiveDerefZdd(dd, f1); 01305 Cudd_RecursiveDerefZdd(dd, f0); 01306 Cudd_RecursiveDerefZdd(dd, g1); 01307 Cudd_RecursiveDerefZdd(dd, g0); 01308 01309 cuddCacheInsert2(dd, cuddZddDivideF, f, g, r); 01310 Cudd_Deref(r); 01311 return(r); 01312 01313 } /* 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 1456 of file cuddZddFuncs.c.
01462 { 01463 *f1 = cuddZddSubset1(dd, f, v); 01464 if (*f1 == NULL) 01465 return(1); 01466 *f0 = cuddZddSubset0(dd, f, v); 01467 if (*f0 == NULL) { 01468 Cudd_RecursiveDerefZdd(dd, *f1); 01469 return(1); 01470 } 01471 return(0); 01472 01473 } /* 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.]
SideEffects [The results are returned in f1, f0, and fd.]
SeeAlso [cuddZddGetCofactors2]
Definition at line 1329 of file cuddZddFuncs.c.
01336 { 01337 DdNode *pc, *nc; 01338 DdNode *zero = DD_ZERO(dd); 01339 int top, hv, ht, pv, nv; 01340 int level; 01341 01342 top = dd->permZ[f->index]; 01343 level = dd->permZ[v]; 01344 hv = level >> 1; 01345 ht = top >> 1; 01346 01347 if (hv < ht) { 01348 *f1 = zero; 01349 *f0 = zero; 01350 *fd = f; 01351 } 01352 else { 01353 pv = cuddZddGetPosVarIndex(dd, v); 01354 nv = cuddZddGetNegVarIndex(dd, v); 01355 01356 /* not to create intermediate ZDD node */ 01357 if (cuddZddGetPosVarLevel(dd, v) < cuddZddGetNegVarLevel(dd, v)) { 01358 pc = cuddZddSubset1(dd, f, pv); 01359 if (pc == NULL) 01360 return(1); 01361 Cudd_Ref(pc); 01362 nc = cuddZddSubset0(dd, f, pv); 01363 if (nc == NULL) { 01364 Cudd_RecursiveDerefZdd(dd, pc); 01365 return(1); 01366 } 01367 Cudd_Ref(nc); 01368 01369 *f1 = cuddZddSubset0(dd, pc, nv); 01370 if (*f1 == NULL) { 01371 Cudd_RecursiveDerefZdd(dd, pc); 01372 Cudd_RecursiveDerefZdd(dd, nc); 01373 return(1); 01374 } 01375 Cudd_Ref(*f1); 01376 *f0 = cuddZddSubset1(dd, nc, nv); 01377 if (*f0 == NULL) { 01378 Cudd_RecursiveDerefZdd(dd, pc); 01379 Cudd_RecursiveDerefZdd(dd, nc); 01380 Cudd_RecursiveDerefZdd(dd, *f1); 01381 return(1); 01382 } 01383 Cudd_Ref(*f0); 01384 01385 *fd = cuddZddSubset0(dd, nc, nv); 01386 if (*fd == NULL) { 01387 Cudd_RecursiveDerefZdd(dd, pc); 01388 Cudd_RecursiveDerefZdd(dd, nc); 01389 Cudd_RecursiveDerefZdd(dd, *f1); 01390 Cudd_RecursiveDerefZdd(dd, *f0); 01391 return(1); 01392 } 01393 Cudd_Ref(*fd); 01394 } else { 01395 pc = cuddZddSubset1(dd, f, nv); 01396 if (pc == NULL) 01397 return(1); 01398 Cudd_Ref(pc); 01399 nc = cuddZddSubset0(dd, f, nv); 01400 if (nc == NULL) { 01401 Cudd_RecursiveDerefZdd(dd, pc); 01402 return(1); 01403 } 01404 Cudd_Ref(nc); 01405 01406 *f0 = cuddZddSubset0(dd, pc, pv); 01407 if (*f0 == NULL) { 01408 Cudd_RecursiveDerefZdd(dd, pc); 01409 Cudd_RecursiveDerefZdd(dd, nc); 01410 return(1); 01411 } 01412 Cudd_Ref(*f0); 01413 *f1 = cuddZddSubset1(dd, nc, pv); 01414 if (*f1 == NULL) { 01415 Cudd_RecursiveDerefZdd(dd, pc); 01416 Cudd_RecursiveDerefZdd(dd, nc); 01417 Cudd_RecursiveDerefZdd(dd, *f1); 01418 return(1); 01419 } 01420 Cudd_Ref(*f1); 01421 01422 *fd = cuddZddSubset0(dd, nc, pv); 01423 if (*fd == NULL) { 01424 Cudd_RecursiveDerefZdd(dd, pc); 01425 Cudd_RecursiveDerefZdd(dd, nc); 01426 Cudd_RecursiveDerefZdd(dd, *f1); 01427 Cudd_RecursiveDerefZdd(dd, *f0); 01428 return(1); 01429 } 01430 Cudd_Ref(*fd); 01431 } 01432 01433 Cudd_RecursiveDerefZdd(dd, pc); 01434 Cudd_RecursiveDerefZdd(dd, nc); 01435 Cudd_Deref(*f1); 01436 Cudd_Deref(*f0); 01437 Cudd_Deref(*fd); 01438 } 01439 return(0); 01440 01441 } /* 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 1555 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 1597 of file cuddZddFuncs.c.
01600 { 01601 int nv = cuddZddGetNegVarIndex(dd, index); 01602 return(dd->permZ[nv]); 01603 } /* 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 1534 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 1576 of file cuddZddFuncs.c.
01579 { 01580 int pv = cuddZddGetPosVarIndex(dd, index); 01581 return(dd->permZ[pv]); 01582 } /* end of cuddZddGetPosVarLevel */
Function********************************************************************
Synopsis [Performs the recursive step of Cudd_zddProduct.]
Description []
SideEffects [None]
SeeAlso [Cudd_zddProduct]
Definition at line 349 of file cuddZddFuncs.c.
00353 { 00354 int v, top_f, top_g; 00355 DdNode *tmp, *term1, *term2, *term3; 00356 DdNode *f0, *f1, *fd, *g0, *g1, *gd; 00357 DdNode *R0, *R1, *Rd, *N0, *N1; 00358 DdNode *r; 00359 DdNode *one = DD_ONE(dd); 00360 DdNode *zero = DD_ZERO(dd); 00361 int flag; 00362 int pv, nv; 00363 00364 statLine(dd); 00365 if (f == zero || g == zero) 00366 return(zero); 00367 if (f == one) 00368 return(g); 00369 if (g == one) 00370 return(f); 00371 00372 top_f = dd->permZ[f->index]; 00373 top_g = dd->permZ[g->index]; 00374 00375 if (top_f > top_g) 00376 return(cuddZddProduct(dd, g, f)); 00377 00378 /* Check cache */ 00379 r = cuddCacheLookup2Zdd(dd, cuddZddProduct, f, g); 00380 if (r) 00381 return(r); 00382 00383 v = f->index; /* either yi or zi */ 00384 flag = cuddZddGetCofactors3(dd, f, v, &f1, &f0, &fd); 00385 if (flag == 1) 00386 return(NULL); 00387 Cudd_Ref(f1); 00388 Cudd_Ref(f0); 00389 Cudd_Ref(fd); 00390 flag = cuddZddGetCofactors3(dd, g, v, &g1, &g0, &gd); 00391 if (flag == 1) { 00392 Cudd_RecursiveDerefZdd(dd, f1); 00393 Cudd_RecursiveDerefZdd(dd, f0); 00394 Cudd_RecursiveDerefZdd(dd, fd); 00395 return(NULL); 00396 } 00397 Cudd_Ref(g1); 00398 Cudd_Ref(g0); 00399 Cudd_Ref(gd); 00400 pv = cuddZddGetPosVarIndex(dd, v); 00401 nv = cuddZddGetNegVarIndex(dd, v); 00402 00403 Rd = cuddZddProduct(dd, fd, gd); 00404 if (Rd == NULL) { 00405 Cudd_RecursiveDerefZdd(dd, f1); 00406 Cudd_RecursiveDerefZdd(dd, f0); 00407 Cudd_RecursiveDerefZdd(dd, fd); 00408 Cudd_RecursiveDerefZdd(dd, g1); 00409 Cudd_RecursiveDerefZdd(dd, g0); 00410 Cudd_RecursiveDerefZdd(dd, gd); 00411 return(NULL); 00412 } 00413 Cudd_Ref(Rd); 00414 00415 term1 = cuddZddProduct(dd, f0, g0); 00416 if (term1 == NULL) { 00417 Cudd_RecursiveDerefZdd(dd, f1); 00418 Cudd_RecursiveDerefZdd(dd, f0); 00419 Cudd_RecursiveDerefZdd(dd, fd); 00420 Cudd_RecursiveDerefZdd(dd, g1); 00421 Cudd_RecursiveDerefZdd(dd, g0); 00422 Cudd_RecursiveDerefZdd(dd, gd); 00423 Cudd_RecursiveDerefZdd(dd, Rd); 00424 return(NULL); 00425 } 00426 Cudd_Ref(term1); 00427 term2 = cuddZddProduct(dd, f0, gd); 00428 if (term2 == NULL) { 00429 Cudd_RecursiveDerefZdd(dd, f1); 00430 Cudd_RecursiveDerefZdd(dd, f0); 00431 Cudd_RecursiveDerefZdd(dd, fd); 00432 Cudd_RecursiveDerefZdd(dd, g1); 00433 Cudd_RecursiveDerefZdd(dd, g0); 00434 Cudd_RecursiveDerefZdd(dd, gd); 00435 Cudd_RecursiveDerefZdd(dd, Rd); 00436 Cudd_RecursiveDerefZdd(dd, term1); 00437 return(NULL); 00438 } 00439 Cudd_Ref(term2); 00440 term3 = cuddZddProduct(dd, fd, g0); 00441 if (term3 == NULL) { 00442 Cudd_RecursiveDerefZdd(dd, f1); 00443 Cudd_RecursiveDerefZdd(dd, f0); 00444 Cudd_RecursiveDerefZdd(dd, fd); 00445 Cudd_RecursiveDerefZdd(dd, g1); 00446 Cudd_RecursiveDerefZdd(dd, g0); 00447 Cudd_RecursiveDerefZdd(dd, gd); 00448 Cudd_RecursiveDerefZdd(dd, Rd); 00449 Cudd_RecursiveDerefZdd(dd, term1); 00450 Cudd_RecursiveDerefZdd(dd, term2); 00451 return(NULL); 00452 } 00453 Cudd_Ref(term3); 00454 Cudd_RecursiveDerefZdd(dd, f0); 00455 Cudd_RecursiveDerefZdd(dd, g0); 00456 tmp = cuddZddUnion(dd, term1, term2); 00457 if (tmp == NULL) { 00458 Cudd_RecursiveDerefZdd(dd, f1); 00459 Cudd_RecursiveDerefZdd(dd, fd); 00460 Cudd_RecursiveDerefZdd(dd, g1); 00461 Cudd_RecursiveDerefZdd(dd, gd); 00462 Cudd_RecursiveDerefZdd(dd, Rd); 00463 Cudd_RecursiveDerefZdd(dd, term1); 00464 Cudd_RecursiveDerefZdd(dd, term2); 00465 Cudd_RecursiveDerefZdd(dd, term3); 00466 return(NULL); 00467 } 00468 Cudd_Ref(tmp); 00469 Cudd_RecursiveDerefZdd(dd, term1); 00470 Cudd_RecursiveDerefZdd(dd, term2); 00471 R0 = cuddZddUnion(dd, tmp, term3); 00472 if (R0 == NULL) { 00473 Cudd_RecursiveDerefZdd(dd, f1); 00474 Cudd_RecursiveDerefZdd(dd, fd); 00475 Cudd_RecursiveDerefZdd(dd, g1); 00476 Cudd_RecursiveDerefZdd(dd, gd); 00477 Cudd_RecursiveDerefZdd(dd, Rd); 00478 Cudd_RecursiveDerefZdd(dd, term3); 00479 Cudd_RecursiveDerefZdd(dd, tmp); 00480 return(NULL); 00481 } 00482 Cudd_Ref(R0); 00483 Cudd_RecursiveDerefZdd(dd, tmp); 00484 Cudd_RecursiveDerefZdd(dd, term3); 00485 N0 = cuddZddGetNode(dd, nv, R0, Rd); /* nv = zi */ 00486 if (N0 == NULL) { 00487 Cudd_RecursiveDerefZdd(dd, f1); 00488 Cudd_RecursiveDerefZdd(dd, fd); 00489 Cudd_RecursiveDerefZdd(dd, g1); 00490 Cudd_RecursiveDerefZdd(dd, gd); 00491 Cudd_RecursiveDerefZdd(dd, Rd); 00492 Cudd_RecursiveDerefZdd(dd, R0); 00493 return(NULL); 00494 } 00495 Cudd_Ref(N0); 00496 Cudd_RecursiveDerefZdd(dd, R0); 00497 Cudd_RecursiveDerefZdd(dd, Rd); 00498 00499 term1 = cuddZddProduct(dd, f1, g1); 00500 if (term1 == NULL) { 00501 Cudd_RecursiveDerefZdd(dd, f1); 00502 Cudd_RecursiveDerefZdd(dd, fd); 00503 Cudd_RecursiveDerefZdd(dd, g1); 00504 Cudd_RecursiveDerefZdd(dd, gd); 00505 Cudd_RecursiveDerefZdd(dd, N0); 00506 return(NULL); 00507 } 00508 Cudd_Ref(term1); 00509 term2 = cuddZddProduct(dd, f1, gd); 00510 if (term2 == NULL) { 00511 Cudd_RecursiveDerefZdd(dd, f1); 00512 Cudd_RecursiveDerefZdd(dd, fd); 00513 Cudd_RecursiveDerefZdd(dd, g1); 00514 Cudd_RecursiveDerefZdd(dd, gd); 00515 Cudd_RecursiveDerefZdd(dd, N0); 00516 Cudd_RecursiveDerefZdd(dd, term1); 00517 return(NULL); 00518 } 00519 Cudd_Ref(term2); 00520 term3 = cuddZddProduct(dd, fd, g1); 00521 if (term3 == NULL) { 00522 Cudd_RecursiveDerefZdd(dd, f1); 00523 Cudd_RecursiveDerefZdd(dd, fd); 00524 Cudd_RecursiveDerefZdd(dd, g1); 00525 Cudd_RecursiveDerefZdd(dd, gd); 00526 Cudd_RecursiveDerefZdd(dd, N0); 00527 Cudd_RecursiveDerefZdd(dd, term1); 00528 Cudd_RecursiveDerefZdd(dd, term2); 00529 return(NULL); 00530 } 00531 Cudd_Ref(term3); 00532 Cudd_RecursiveDerefZdd(dd, f1); 00533 Cudd_RecursiveDerefZdd(dd, g1); 00534 Cudd_RecursiveDerefZdd(dd, fd); 00535 Cudd_RecursiveDerefZdd(dd, gd); 00536 tmp = cuddZddUnion(dd, term1, term2); 00537 if (tmp == NULL) { 00538 Cudd_RecursiveDerefZdd(dd, N0); 00539 Cudd_RecursiveDerefZdd(dd, term1); 00540 Cudd_RecursiveDerefZdd(dd, term2); 00541 Cudd_RecursiveDerefZdd(dd, term3); 00542 return(NULL); 00543 } 00544 Cudd_Ref(tmp); 00545 Cudd_RecursiveDerefZdd(dd, term1); 00546 Cudd_RecursiveDerefZdd(dd, term2); 00547 R1 = cuddZddUnion(dd, tmp, term3); 00548 if (R1 == NULL) { 00549 Cudd_RecursiveDerefZdd(dd, N0); 00550 Cudd_RecursiveDerefZdd(dd, term3); 00551 Cudd_RecursiveDerefZdd(dd, tmp); 00552 return(NULL); 00553 } 00554 Cudd_Ref(R1); 00555 Cudd_RecursiveDerefZdd(dd, tmp); 00556 Cudd_RecursiveDerefZdd(dd, term3); 00557 N1 = cuddZddGetNode(dd, pv, R1, N0); /* pv = yi */ 00558 if (N1 == NULL) { 00559 Cudd_RecursiveDerefZdd(dd, N0); 00560 Cudd_RecursiveDerefZdd(dd, R1); 00561 return(NULL); 00562 } 00563 Cudd_Ref(N1); 00564 Cudd_RecursiveDerefZdd(dd, R1); 00565 Cudd_RecursiveDerefZdd(dd, N0); 00566 00567 cuddCacheInsert2(dd, cuddZddProduct, f, g, N1); 00568 Cudd_Deref(N1); 00569 return(N1); 00570 00571 } /* end of cuddZddProduct */
Function********************************************************************
Synopsis [Performs the recursive step of Cudd_zddUnateProduct.]
Description []
SideEffects [None]
SeeAlso [Cudd_zddUnateProduct]
Definition at line 586 of file cuddZddFuncs.c.
00590 { 00591 int v, top_f, top_g; 00592 DdNode *term1, *term2, *term3, *term4; 00593 DdNode *sum1, *sum2; 00594 DdNode *f0, *f1, *g0, *g1; 00595 DdNode *r; 00596 DdNode *one = DD_ONE(dd); 00597 DdNode *zero = DD_ZERO(dd); 00598 int flag; 00599 00600 statLine(dd); 00601 if (f == zero || g == zero) 00602 return(zero); 00603 if (f == one) 00604 return(g); 00605 if (g == one) 00606 return(f); 00607 00608 top_f = dd->permZ[f->index]; 00609 top_g = dd->permZ[g->index]; 00610 00611 if (top_f > top_g) 00612 return(cuddZddUnateProduct(dd, g, f)); 00613 00614 /* Check cache */ 00615 r = cuddCacheLookup2Zdd(dd, cuddZddUnateProduct, f, g); 00616 if (r) 00617 return(r); 00618 00619 v = f->index; /* either yi or zi */ 00620 flag = cuddZddGetCofactors2(dd, f, v, &f1, &f0); 00621 if (flag == 1) 00622 return(NULL); 00623 Cudd_Ref(f1); 00624 Cudd_Ref(f0); 00625 flag = cuddZddGetCofactors2(dd, g, v, &g1, &g0); 00626 if (flag == 1) { 00627 Cudd_RecursiveDerefZdd(dd, f1); 00628 Cudd_RecursiveDerefZdd(dd, f0); 00629 return(NULL); 00630 } 00631 Cudd_Ref(g1); 00632 Cudd_Ref(g0); 00633 00634 term1 = cuddZddUnateProduct(dd, f1, g1); 00635 if (term1 == NULL) { 00636 Cudd_RecursiveDerefZdd(dd, f1); 00637 Cudd_RecursiveDerefZdd(dd, f0); 00638 Cudd_RecursiveDerefZdd(dd, g1); 00639 Cudd_RecursiveDerefZdd(dd, g0); 00640 return(NULL); 00641 } 00642 Cudd_Ref(term1); 00643 term2 = cuddZddUnateProduct(dd, f1, g0); 00644 if (term2 == NULL) { 00645 Cudd_RecursiveDerefZdd(dd, f1); 00646 Cudd_RecursiveDerefZdd(dd, f0); 00647 Cudd_RecursiveDerefZdd(dd, g1); 00648 Cudd_RecursiveDerefZdd(dd, g0); 00649 Cudd_RecursiveDerefZdd(dd, term1); 00650 return(NULL); 00651 } 00652 Cudd_Ref(term2); 00653 term3 = cuddZddUnateProduct(dd, f0, g1); 00654 if (term3 == NULL) { 00655 Cudd_RecursiveDerefZdd(dd, f1); 00656 Cudd_RecursiveDerefZdd(dd, f0); 00657 Cudd_RecursiveDerefZdd(dd, g1); 00658 Cudd_RecursiveDerefZdd(dd, g0); 00659 Cudd_RecursiveDerefZdd(dd, term1); 00660 Cudd_RecursiveDerefZdd(dd, term2); 00661 return(NULL); 00662 } 00663 Cudd_Ref(term3); 00664 term4 = cuddZddUnateProduct(dd, f0, g0); 00665 if (term4 == NULL) { 00666 Cudd_RecursiveDerefZdd(dd, f1); 00667 Cudd_RecursiveDerefZdd(dd, f0); 00668 Cudd_RecursiveDerefZdd(dd, g1); 00669 Cudd_RecursiveDerefZdd(dd, g0); 00670 Cudd_RecursiveDerefZdd(dd, term1); 00671 Cudd_RecursiveDerefZdd(dd, term2); 00672 Cudd_RecursiveDerefZdd(dd, term3); 00673 return(NULL); 00674 } 00675 Cudd_Ref(term4); 00676 Cudd_RecursiveDerefZdd(dd, f1); 00677 Cudd_RecursiveDerefZdd(dd, f0); 00678 Cudd_RecursiveDerefZdd(dd, g1); 00679 Cudd_RecursiveDerefZdd(dd, g0); 00680 sum1 = cuddZddUnion(dd, term1, term2); 00681 if (sum1 == NULL) { 00682 Cudd_RecursiveDerefZdd(dd, term1); 00683 Cudd_RecursiveDerefZdd(dd, term2); 00684 Cudd_RecursiveDerefZdd(dd, term3); 00685 Cudd_RecursiveDerefZdd(dd, term4); 00686 return(NULL); 00687 } 00688 Cudd_Ref(sum1); 00689 Cudd_RecursiveDerefZdd(dd, term1); 00690 Cudd_RecursiveDerefZdd(dd, term2); 00691 sum2 = cuddZddUnion(dd, sum1, term3); 00692 if (sum2 == NULL) { 00693 Cudd_RecursiveDerefZdd(dd, term3); 00694 Cudd_RecursiveDerefZdd(dd, term4); 00695 Cudd_RecursiveDerefZdd(dd, sum1); 00696 return(NULL); 00697 } 00698 Cudd_Ref(sum2); 00699 Cudd_RecursiveDerefZdd(dd, sum1); 00700 Cudd_RecursiveDerefZdd(dd, term3); 00701 r = cuddZddGetNode(dd, v, sum2, term4); 00702 if (r == NULL) { 00703 Cudd_RecursiveDerefZdd(dd, term4); 00704 Cudd_RecursiveDerefZdd(dd, sum2); 00705 return(NULL); 00706 } 00707 Cudd_Ref(r); 00708 Cudd_RecursiveDerefZdd(dd, sum2); 00709 Cudd_RecursiveDerefZdd(dd, term4); 00710 00711 cuddCacheInsert2(dd, cuddZddUnateProduct, f, g, r); 00712 Cudd_Deref(r); 00713 return(r); 00714 00715 } /* end of cuddZddUnateProduct */
Function********************************************************************
Synopsis [Performs the recursive step of Cudd_zddWeakDiv.]
Description []
SideEffects [None]
SeeAlso [Cudd_zddWeakDiv]
Definition at line 730 of file cuddZddFuncs.c.
00734 { 00735 int v; 00736 DdNode *one = DD_ONE(dd); 00737 DdNode *zero = DD_ZERO(dd); 00738 DdNode *f0, *f1, *fd, *g0, *g1, *gd; 00739 DdNode *q, *tmp; 00740 DdNode *r; 00741 int flag; 00742 00743 statLine(dd); 00744 if (g == one) 00745 return(f); 00746 if (f == zero || f == one) 00747 return(zero); 00748 if (f == g) 00749 return(one); 00750 00751 /* Check cache. */ 00752 r = cuddCacheLookup2Zdd(dd, cuddZddWeakDiv, f, g); 00753 if (r) 00754 return(r); 00755 00756 v = g->index; 00757 00758 flag = cuddZddGetCofactors3(dd, f, v, &f1, &f0, &fd); 00759 if (flag == 1) 00760 return(NULL); 00761 Cudd_Ref(f1); 00762 Cudd_Ref(f0); 00763 Cudd_Ref(fd); 00764 flag = cuddZddGetCofactors3(dd, g, v, &g1, &g0, &gd); 00765 if (flag == 1) { 00766 Cudd_RecursiveDerefZdd(dd, f1); 00767 Cudd_RecursiveDerefZdd(dd, f0); 00768 Cudd_RecursiveDerefZdd(dd, fd); 00769 return(NULL); 00770 } 00771 Cudd_Ref(g1); 00772 Cudd_Ref(g0); 00773 Cudd_Ref(gd); 00774 00775 q = g; 00776 00777 if (g0 != zero) { 00778 q = cuddZddWeakDiv(dd, f0, g0); 00779 if (q == NULL) { 00780 Cudd_RecursiveDerefZdd(dd, f1); 00781 Cudd_RecursiveDerefZdd(dd, f0); 00782 Cudd_RecursiveDerefZdd(dd, fd); 00783 Cudd_RecursiveDerefZdd(dd, g1); 00784 Cudd_RecursiveDerefZdd(dd, g0); 00785 Cudd_RecursiveDerefZdd(dd, gd); 00786 return(NULL); 00787 } 00788 Cudd_Ref(q); 00789 } 00790 else 00791 Cudd_Ref(q); 00792 Cudd_RecursiveDerefZdd(dd, f0); 00793 Cudd_RecursiveDerefZdd(dd, g0); 00794 00795 if (q == zero) { 00796 Cudd_RecursiveDerefZdd(dd, f1); 00797 Cudd_RecursiveDerefZdd(dd, g1); 00798 Cudd_RecursiveDerefZdd(dd, fd); 00799 Cudd_RecursiveDerefZdd(dd, gd); 00800 cuddCacheInsert2(dd, cuddZddWeakDiv, f, g, zero); 00801 Cudd_Deref(q); 00802 return(zero); 00803 } 00804 00805 if (g1 != zero) { 00806 Cudd_RecursiveDerefZdd(dd, q); 00807 tmp = cuddZddWeakDiv(dd, f1, g1); 00808 if (tmp == NULL) { 00809 Cudd_RecursiveDerefZdd(dd, f1); 00810 Cudd_RecursiveDerefZdd(dd, g1); 00811 Cudd_RecursiveDerefZdd(dd, fd); 00812 Cudd_RecursiveDerefZdd(dd, gd); 00813 return(NULL); 00814 } 00815 Cudd_Ref(tmp); 00816 Cudd_RecursiveDerefZdd(dd, f1); 00817 Cudd_RecursiveDerefZdd(dd, g1); 00818 if (q == g) 00819 q = tmp; 00820 else { 00821 q = cuddZddIntersect(dd, q, tmp); 00822 if (q == NULL) { 00823 Cudd_RecursiveDerefZdd(dd, fd); 00824 Cudd_RecursiveDerefZdd(dd, gd); 00825 return(NULL); 00826 } 00827 Cudd_Ref(q); 00828 Cudd_RecursiveDerefZdd(dd, tmp); 00829 } 00830 } 00831 else { 00832 Cudd_RecursiveDerefZdd(dd, f1); 00833 Cudd_RecursiveDerefZdd(dd, g1); 00834 } 00835 00836 if (q == zero) { 00837 Cudd_RecursiveDerefZdd(dd, fd); 00838 Cudd_RecursiveDerefZdd(dd, gd); 00839 cuddCacheInsert2(dd, cuddZddWeakDiv, f, g, zero); 00840 Cudd_Deref(q); 00841 return(zero); 00842 } 00843 00844 if (gd != zero) { 00845 Cudd_RecursiveDerefZdd(dd, q); 00846 tmp = cuddZddWeakDiv(dd, fd, gd); 00847 if (tmp == NULL) { 00848 Cudd_RecursiveDerefZdd(dd, fd); 00849 Cudd_RecursiveDerefZdd(dd, gd); 00850 return(NULL); 00851 } 00852 Cudd_Ref(tmp); 00853 Cudd_RecursiveDerefZdd(dd, fd); 00854 Cudd_RecursiveDerefZdd(dd, gd); 00855 if (q == g) 00856 q = tmp; 00857 else { 00858 q = cuddZddIntersect(dd, q, tmp); 00859 if (q == NULL) { 00860 Cudd_RecursiveDerefZdd(dd, tmp); 00861 return(NULL); 00862 } 00863 Cudd_Ref(q); 00864 Cudd_RecursiveDerefZdd(dd, tmp); 00865 } 00866 } 00867 else { 00868 Cudd_RecursiveDerefZdd(dd, fd); 00869 Cudd_RecursiveDerefZdd(dd, gd); 00870 } 00871 00872 cuddCacheInsert2(dd, cuddZddWeakDiv, f, g, q); 00873 Cudd_Deref(q); 00874 return(q); 00875 00876 } /* end of cuddZddWeakDiv */
Function********************************************************************
Synopsis [Performs the recursive step of Cudd_zddWeakDivF.]
Description []
SideEffects [None]
SeeAlso [Cudd_zddWeakDivF]
Definition at line 891 of file cuddZddFuncs.c.
00895 { 00896 int v, top_f, top_g, vf, vg; 00897 DdNode *one = DD_ONE(dd); 00898 DdNode *zero = DD_ZERO(dd); 00899 DdNode *f0, *f1, *fd, *g0, *g1, *gd; 00900 DdNode *q, *tmp; 00901 DdNode *r; 00902 DdNode *term1, *term0, *termd; 00903 int flag; 00904 int pv, nv; 00905 00906 statLine(dd); 00907 if (g == one) 00908 return(f); 00909 if (f == zero || f == one) 00910 return(zero); 00911 if (f == g) 00912 return(one); 00913 00914 /* Check cache. */ 00915 r = cuddCacheLookup2Zdd(dd, cuddZddWeakDivF, f, g); 00916 if (r) 00917 return(r); 00918 00919 top_f = dd->permZ[f->index]; 00920 top_g = dd->permZ[g->index]; 00921 vf = top_f >> 1; 00922 vg = top_g >> 1; 00923 v = ddMin(top_f, top_g); 00924 00925 if (v == top_f && vf < vg) { 00926 v = f->index; 00927 flag = cuddZddGetCofactors3(dd, f, v, &f1, &f0, &fd); 00928 if (flag == 1) 00929 return(NULL); 00930 Cudd_Ref(f1); 00931 Cudd_Ref(f0); 00932 Cudd_Ref(fd); 00933 00934 pv = cuddZddGetPosVarIndex(dd, v); 00935 nv = cuddZddGetNegVarIndex(dd, v); 00936 00937 term1 = cuddZddWeakDivF(dd, f1, g); 00938 if (term1 == NULL) { 00939 Cudd_RecursiveDerefZdd(dd, f1); 00940 Cudd_RecursiveDerefZdd(dd, f0); 00941 Cudd_RecursiveDerefZdd(dd, fd); 00942 return(NULL); 00943 } 00944 Cudd_Ref(term1); 00945 Cudd_RecursiveDerefZdd(dd, f1); 00946 term0 = cuddZddWeakDivF(dd, f0, g); 00947 if (term0 == NULL) { 00948 Cudd_RecursiveDerefZdd(dd, f0); 00949 Cudd_RecursiveDerefZdd(dd, fd); 00950 Cudd_RecursiveDerefZdd(dd, term1); 00951 return(NULL); 00952 } 00953 Cudd_Ref(term0); 00954 Cudd_RecursiveDerefZdd(dd, f0); 00955 termd = cuddZddWeakDivF(dd, fd, g); 00956 if (termd == NULL) { 00957 Cudd_RecursiveDerefZdd(dd, fd); 00958 Cudd_RecursiveDerefZdd(dd, term1); 00959 Cudd_RecursiveDerefZdd(dd, term0); 00960 return(NULL); 00961 } 00962 Cudd_Ref(termd); 00963 Cudd_RecursiveDerefZdd(dd, fd); 00964 00965 tmp = cuddZddGetNode(dd, nv, term0, termd); /* nv = zi */ 00966 if (tmp == NULL) { 00967 Cudd_RecursiveDerefZdd(dd, term1); 00968 Cudd_RecursiveDerefZdd(dd, term0); 00969 Cudd_RecursiveDerefZdd(dd, termd); 00970 return(NULL); 00971 } 00972 Cudd_Ref(tmp); 00973 Cudd_RecursiveDerefZdd(dd, term0); 00974 Cudd_RecursiveDerefZdd(dd, termd); 00975 q = cuddZddGetNode(dd, pv, term1, tmp); /* pv = yi */ 00976 if (q == NULL) { 00977 Cudd_RecursiveDerefZdd(dd, term1); 00978 Cudd_RecursiveDerefZdd(dd, tmp); 00979 return(NULL); 00980 } 00981 Cudd_Ref(q); 00982 Cudd_RecursiveDerefZdd(dd, term1); 00983 Cudd_RecursiveDerefZdd(dd, tmp); 00984 00985 cuddCacheInsert2(dd, cuddZddWeakDivF, f, g, q); 00986 Cudd_Deref(q); 00987 return(q); 00988 } 00989 00990 if (v == top_f) 00991 v = f->index; 00992 else 00993 v = g->index; 00994 00995 flag = cuddZddGetCofactors3(dd, f, v, &f1, &f0, &fd); 00996 if (flag == 1) 00997 return(NULL); 00998 Cudd_Ref(f1); 00999 Cudd_Ref(f0); 01000 Cudd_Ref(fd); 01001 flag = cuddZddGetCofactors3(dd, g, v, &g1, &g0, &gd); 01002 if (flag == 1) { 01003 Cudd_RecursiveDerefZdd(dd, f1); 01004 Cudd_RecursiveDerefZdd(dd, f0); 01005 Cudd_RecursiveDerefZdd(dd, fd); 01006 return(NULL); 01007 } 01008 Cudd_Ref(g1); 01009 Cudd_Ref(g0); 01010 Cudd_Ref(gd); 01011 01012 q = g; 01013 01014 if (g0 != zero) { 01015 q = cuddZddWeakDivF(dd, f0, g0); 01016 if (q == NULL) { 01017 Cudd_RecursiveDerefZdd(dd, f1); 01018 Cudd_RecursiveDerefZdd(dd, f0); 01019 Cudd_RecursiveDerefZdd(dd, fd); 01020 Cudd_RecursiveDerefZdd(dd, g1); 01021 Cudd_RecursiveDerefZdd(dd, g0); 01022 Cudd_RecursiveDerefZdd(dd, gd); 01023 return(NULL); 01024 } 01025 Cudd_Ref(q); 01026 } 01027 else 01028 Cudd_Ref(q); 01029 Cudd_RecursiveDerefZdd(dd, f0); 01030 Cudd_RecursiveDerefZdd(dd, g0); 01031 01032 if (q == zero) { 01033 Cudd_RecursiveDerefZdd(dd, f1); 01034 Cudd_RecursiveDerefZdd(dd, g1); 01035 Cudd_RecursiveDerefZdd(dd, fd); 01036 Cudd_RecursiveDerefZdd(dd, gd); 01037 cuddCacheInsert2(dd, cuddZddWeakDivF, f, g, zero); 01038 Cudd_Deref(q); 01039 return(zero); 01040 } 01041 01042 if (g1 != zero) { 01043 Cudd_RecursiveDerefZdd(dd, q); 01044 tmp = cuddZddWeakDivF(dd, f1, g1); 01045 if (tmp == NULL) { 01046 Cudd_RecursiveDerefZdd(dd, f1); 01047 Cudd_RecursiveDerefZdd(dd, g1); 01048 Cudd_RecursiveDerefZdd(dd, fd); 01049 Cudd_RecursiveDerefZdd(dd, gd); 01050 return(NULL); 01051 } 01052 Cudd_Ref(tmp); 01053 Cudd_RecursiveDerefZdd(dd, f1); 01054 Cudd_RecursiveDerefZdd(dd, g1); 01055 if (q == g) 01056 q = tmp; 01057 else { 01058 q = cuddZddIntersect(dd, q, tmp); 01059 if (q == NULL) { 01060 Cudd_RecursiveDerefZdd(dd, fd); 01061 Cudd_RecursiveDerefZdd(dd, gd); 01062 return(NULL); 01063 } 01064 Cudd_Ref(q); 01065 Cudd_RecursiveDerefZdd(dd, tmp); 01066 } 01067 } 01068 else { 01069 Cudd_RecursiveDerefZdd(dd, f1); 01070 Cudd_RecursiveDerefZdd(dd, g1); 01071 } 01072 01073 if (q == zero) { 01074 Cudd_RecursiveDerefZdd(dd, fd); 01075 Cudd_RecursiveDerefZdd(dd, gd); 01076 cuddCacheInsert2(dd, cuddZddWeakDivF, f, g, zero); 01077 Cudd_Deref(q); 01078 return(zero); 01079 } 01080 01081 if (gd != zero) { 01082 Cudd_RecursiveDerefZdd(dd, q); 01083 tmp = cuddZddWeakDivF(dd, fd, gd); 01084 if (tmp == NULL) { 01085 Cudd_RecursiveDerefZdd(dd, fd); 01086 Cudd_RecursiveDerefZdd(dd, gd); 01087 return(NULL); 01088 } 01089 Cudd_Ref(tmp); 01090 Cudd_RecursiveDerefZdd(dd, fd); 01091 Cudd_RecursiveDerefZdd(dd, gd); 01092 if (q == g) 01093 q = tmp; 01094 else { 01095 q = cuddZddIntersect(dd, q, tmp); 01096 if (q == NULL) { 01097 Cudd_RecursiveDerefZdd(dd, tmp); 01098 return(NULL); 01099 } 01100 Cudd_Ref(q); 01101 Cudd_RecursiveDerefZdd(dd, tmp); 01102 } 01103 } 01104 else { 01105 Cudd_RecursiveDerefZdd(dd, fd); 01106 Cudd_RecursiveDerefZdd(dd, gd); 01107 } 01108 01109 cuddCacheInsert2(dd, cuddZddWeakDivF, f, g, q); 01110 Cudd_Deref(q); 01111 return(q); 01112 01113 } /* end of cuddZddWeakDivF */
Variable Documentation
char rcsid [] DD_UNUSED = "$Id: cuddZddFuncs.c,v 1.1.1.1 2003/02/24 22:23:53 wjiang 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 [ This file was created at the University of Colorado at Boulder. The University of Colorado at Boulder makes no warranty about the suitability of this software for any purpose. It is presented on an AS IS basis.]
Definition at line 74 of file cuddZddFuncs.c.
