SVF
cuddZddIsop.c
Go to the documentation of this file.
1 
64 #include "CUDD/util.h"
65 #include "CUDD/cuddInt.h"
66 
67 /*---------------------------------------------------------------------------*/
68 /* Constant declarations */
69 /*---------------------------------------------------------------------------*/
70 
71 
72 /*---------------------------------------------------------------------------*/
73 /* Stucture declarations */
74 /*---------------------------------------------------------------------------*/
75 
76 
77 /*---------------------------------------------------------------------------*/
78 /* Type declarations */
79 /*---------------------------------------------------------------------------*/
80 
81 
82 /*---------------------------------------------------------------------------*/
83 /* Variable declarations */
84 /*---------------------------------------------------------------------------*/
85 
86 #ifndef lint
87 static char rcsid[] DD_UNUSED = "$Id: cuddZddIsop.c,v 1.22 2012/02/05 01:07:19 fabio Exp $";
88 #endif
89 
90 /*---------------------------------------------------------------------------*/
91 /* Macro declarations */
92 /*---------------------------------------------------------------------------*/
93 
94 
97 /*---------------------------------------------------------------------------*/
98 /* Static function prototypes */
99 /*---------------------------------------------------------------------------*/
100 
101 
104 /*---------------------------------------------------------------------------*/
105 /* Definition of exported functions */
106 /*---------------------------------------------------------------------------*/
107 
131 DdNode *
132 Cudd_zddIsop(
133  DdManager * dd,
134  DdNode * L,
135  DdNode * U,
136  DdNode ** zdd_I)
137 {
138  DdNode *res;
139  int autoDynZ;
140 
141  autoDynZ = dd->autoDynZ;
142  dd->autoDynZ = 0;
143 
144  do {
145  dd->reordered = 0;
146  res = cuddZddIsop(dd, L, U, zdd_I);
147  } while (dd->reordered == 1);
148  dd->autoDynZ = autoDynZ;
149  return(res);
150 
151 } /* end of Cudd_zddIsop */
152 
153 
169 DdNode *
170 Cudd_bddIsop(
171  DdManager * dd,
172  DdNode * L,
173  DdNode * U)
174 {
175  DdNode *res;
176 
177  do {
178  dd->reordered = 0;
179  res = cuddBddIsop(dd, L, U);
180  } while (dd->reordered == 1);
181  return(res);
182 
183 } /* end of Cudd_bddIsop */
184 
185 
199 DdNode *
200 Cudd_MakeBddFromZddCover(
201  DdManager * dd,
202  DdNode * node)
203 {
204  DdNode *res;
205 
206  do {
207  dd->reordered = 0;
208  res = cuddMakeBddFromZddCover(dd, node);
209  } while (dd->reordered == 1);
210  return(res);
211 } /* end of Cudd_MakeBddFromZddCover */
212 
213 
214 /*---------------------------------------------------------------------------*/
215 /* Definition of internal functions */
216 /*---------------------------------------------------------------------------*/
217 
218 
230 DdNode *
231 cuddZddIsop(
232  DdManager * dd,
233  DdNode * L,
234  DdNode * U,
235  DdNode ** zdd_I)
236 {
237  DdNode *one = DD_ONE(dd);
238  DdNode *zero = Cudd_Not(one);
239  DdNode *zdd_one = DD_ONE(dd);
240  DdNode *zdd_zero = DD_ZERO(dd);
241  int v, top_l, top_u;
242  DdNode *Lsub0, *Usub0, *Lsub1, *Usub1, *Ld, *Ud;
243  DdNode *Lsuper0, *Usuper0, *Lsuper1, *Usuper1;
244  DdNode *Isub0, *Isub1, *Id;
245  DdNode *zdd_Isub0, *zdd_Isub1, *zdd_Id;
246  DdNode *x;
247  DdNode *term0, *term1, *sum;
248  DdNode *Lv, *Uv, *Lnv, *Unv;
249  DdNode *r, *y, *z;
250  int index;
251  DD_CTFP cacheOp;
252 
253  statLine(dd);
254  if (L == zero) {
255  *zdd_I = zdd_zero;
256  return(zero);
257  }
258  if (U == one) {
259  *zdd_I = zdd_one;
260  return(one);
261  }
262 
263  if (U == zero || L == one) {
264  printf("*** ERROR : illegal condition for ISOP (U < L).\n");
265  exit(1);
266  }
267 
268  /* Check the cache. We store two results for each recursive call.
269  ** One is the BDD, and the other is the ZDD. Both are needed.
270  ** Hence we need a double hit in the cache to terminate the
271  ** recursion. Clearly, collisions may evict only one of the two
272  ** results. */
273  cacheOp = (DD_CTFP) cuddZddIsop;
274  r = cuddCacheLookup2(dd, cuddBddIsop, L, U);
275  if (r) {
276  *zdd_I = cuddCacheLookup2Zdd(dd, cacheOp, L, U);
277  if (*zdd_I)
278  return(r);
279  else {
280  /* The BDD result may have been dead. In that case
281  ** cuddCacheLookup2 would have called cuddReclaim,
282  ** whose effects we now have to undo. */
283  cuddRef(r);
284  Cudd_RecursiveDeref(dd, r);
285  }
286  }
287 
288  top_l = dd->perm[Cudd_Regular(L)->index];
289  top_u = dd->perm[Cudd_Regular(U)->index];
290  v = ddMin(top_l, top_u);
291 
292  /* Compute cofactors. */
293  if (top_l == v) {
294  index = Cudd_Regular(L)->index;
295  Lv = Cudd_T(L);
296  Lnv = Cudd_E(L);
297  if (Cudd_IsComplement(L)) {
298  Lv = Cudd_Not(Lv);
299  Lnv = Cudd_Not(Lnv);
300  }
301  }
302  else {
303  index = Cudd_Regular(U)->index;
304  Lv = Lnv = L;
305  }
306 
307  if (top_u == v) {
308  Uv = Cudd_T(U);
309  Unv = Cudd_E(U);
310  if (Cudd_IsComplement(U)) {
311  Uv = Cudd_Not(Uv);
312  Unv = Cudd_Not(Unv);
313  }
314  }
315  else {
316  Uv = Unv = U;
317  }
318 
319  Lsub0 = cuddBddAndRecur(dd, Lnv, Cudd_Not(Uv));
320  if (Lsub0 == NULL)
321  return(NULL);
322  Cudd_Ref(Lsub0);
323  Usub0 = Unv;
324  Lsub1 = cuddBddAndRecur(dd, Lv, Cudd_Not(Unv));
325  if (Lsub1 == NULL) {
326  Cudd_RecursiveDeref(dd, Lsub0);
327  return(NULL);
328  }
329  Cudd_Ref(Lsub1);
330  Usub1 = Uv;
331 
332  Isub0 = cuddZddIsop(dd, Lsub0, Usub0, &zdd_Isub0);
333  if (Isub0 == NULL) {
334  Cudd_RecursiveDeref(dd, Lsub0);
335  Cudd_RecursiveDeref(dd, Lsub1);
336  return(NULL);
337  }
338  /*
339  if ((!cuddIsConstant(Cudd_Regular(Isub0))) &&
340  (Cudd_Regular(Isub0)->index != zdd_Isub0->index / 2 ||
341  dd->permZ[index * 2] > dd->permZ[zdd_Isub0->index])) {
342  printf("*** ERROR : illegal permutation in ZDD. ***\n");
343  }
344  */
345  Cudd_Ref(Isub0);
346  Cudd_Ref(zdd_Isub0);
347  Isub1 = cuddZddIsop(dd, Lsub1, Usub1, &zdd_Isub1);
348  if (Isub1 == NULL) {
349  Cudd_RecursiveDeref(dd, Lsub0);
350  Cudd_RecursiveDeref(dd, Lsub1);
351  Cudd_RecursiveDeref(dd, Isub0);
352  Cudd_RecursiveDerefZdd(dd, zdd_Isub0);
353  return(NULL);
354  }
355  /*
356  if ((!cuddIsConstant(Cudd_Regular(Isub1))) &&
357  (Cudd_Regular(Isub1)->index != zdd_Isub1->index / 2 ||
358  dd->permZ[index * 2] > dd->permZ[zdd_Isub1->index])) {
359  printf("*** ERROR : illegal permutation in ZDD. ***\n");
360  }
361  */
362  Cudd_Ref(Isub1);
363  Cudd_Ref(zdd_Isub1);
364  Cudd_RecursiveDeref(dd, Lsub0);
365  Cudd_RecursiveDeref(dd, Lsub1);
366 
367  Lsuper0 = cuddBddAndRecur(dd, Lnv, Cudd_Not(Isub0));
368  if (Lsuper0 == NULL) {
369  Cudd_RecursiveDeref(dd, Isub0);
370  Cudd_RecursiveDerefZdd(dd, zdd_Isub0);
371  Cudd_RecursiveDeref(dd, Isub1);
372  Cudd_RecursiveDerefZdd(dd, zdd_Isub1);
373  return(NULL);
374  }
375  Cudd_Ref(Lsuper0);
376  Lsuper1 = cuddBddAndRecur(dd, Lv, Cudd_Not(Isub1));
377  if (Lsuper1 == NULL) {
378  Cudd_RecursiveDeref(dd, Isub0);
379  Cudd_RecursiveDerefZdd(dd, zdd_Isub0);
380  Cudd_RecursiveDeref(dd, Isub1);
381  Cudd_RecursiveDerefZdd(dd, zdd_Isub1);
382  Cudd_RecursiveDeref(dd, Lsuper0);
383  return(NULL);
384  }
385  Cudd_Ref(Lsuper1);
386  Usuper0 = Unv;
387  Usuper1 = Uv;
388 
389  /* Ld = Lsuper0 + Lsuper1 */
390  Ld = cuddBddAndRecur(dd, Cudd_Not(Lsuper0), Cudd_Not(Lsuper1));
391  if (Ld == NULL) {
392  Cudd_RecursiveDeref(dd, Isub0);
393  Cudd_RecursiveDerefZdd(dd, zdd_Isub0);
394  Cudd_RecursiveDeref(dd, Isub1);
395  Cudd_RecursiveDerefZdd(dd, zdd_Isub1);
396  Cudd_RecursiveDeref(dd, Lsuper0);
397  Cudd_RecursiveDeref(dd, Lsuper1);
398  return(NULL);
399  }
400  Ld = Cudd_Not(Ld);
401  Cudd_Ref(Ld);
402  /* Ud = Usuper0 * Usuper1 */
403  Ud = cuddBddAndRecur(dd, Usuper0, Usuper1);
404  if (Ud == NULL) {
405  Cudd_RecursiveDeref(dd, Isub0);
406  Cudd_RecursiveDerefZdd(dd, zdd_Isub0);
407  Cudd_RecursiveDeref(dd, Isub1);
408  Cudd_RecursiveDerefZdd(dd, zdd_Isub1);
409  Cudd_RecursiveDeref(dd, Lsuper0);
410  Cudd_RecursiveDeref(dd, Lsuper1);
411  Cudd_RecursiveDeref(dd, Ld);
412  return(NULL);
413  }
414  Cudd_Ref(Ud);
415  Cudd_RecursiveDeref(dd, Lsuper0);
416  Cudd_RecursiveDeref(dd, Lsuper1);
417 
418  Id = cuddZddIsop(dd, Ld, Ud, &zdd_Id);
419  if (Id == NULL) {
420  Cudd_RecursiveDeref(dd, Isub0);
421  Cudd_RecursiveDerefZdd(dd, zdd_Isub0);
422  Cudd_RecursiveDeref(dd, Isub1);
423  Cudd_RecursiveDerefZdd(dd, zdd_Isub1);
424  Cudd_RecursiveDeref(dd, Ld);
425  Cudd_RecursiveDeref(dd, Ud);
426  return(NULL);
427  }
428  /*
429  if ((!cuddIsConstant(Cudd_Regular(Id))) &&
430  (Cudd_Regular(Id)->index != zdd_Id->index / 2 ||
431  dd->permZ[index * 2] > dd->permZ[zdd_Id->index])) {
432  printf("*** ERROR : illegal permutation in ZDD. ***\n");
433  }
434  */
435  Cudd_Ref(Id);
436  Cudd_Ref(zdd_Id);
437  Cudd_RecursiveDeref(dd, Ld);
438  Cudd_RecursiveDeref(dd, Ud);
439 
440  x = cuddUniqueInter(dd, index, one, zero);
441  if (x == NULL) {
442  Cudd_RecursiveDeref(dd, Isub0);
443  Cudd_RecursiveDerefZdd(dd, zdd_Isub0);
444  Cudd_RecursiveDeref(dd, Isub1);
445  Cudd_RecursiveDerefZdd(dd, zdd_Isub1);
446  Cudd_RecursiveDeref(dd, Id);
447  Cudd_RecursiveDerefZdd(dd, zdd_Id);
448  return(NULL);
449  }
450  Cudd_Ref(x);
451  /* term0 = x * Isub0 */
452  term0 = cuddBddAndRecur(dd, Cudd_Not(x), Isub0);
453  if (term0 == NULL) {
454  Cudd_RecursiveDeref(dd, Isub0);
455  Cudd_RecursiveDerefZdd(dd, zdd_Isub0);
456  Cudd_RecursiveDeref(dd, Isub1);
457  Cudd_RecursiveDerefZdd(dd, zdd_Isub1);
458  Cudd_RecursiveDeref(dd, Id);
459  Cudd_RecursiveDerefZdd(dd, zdd_Id);
460  Cudd_RecursiveDeref(dd, x);
461  return(NULL);
462  }
463  Cudd_Ref(term0);
464  Cudd_RecursiveDeref(dd, Isub0);
465  /* term1 = x * Isub1 */
466  term1 = cuddBddAndRecur(dd, x, Isub1);
467  if (term1 == NULL) {
468  Cudd_RecursiveDerefZdd(dd, zdd_Isub0);
469  Cudd_RecursiveDeref(dd, Isub1);
470  Cudd_RecursiveDerefZdd(dd, zdd_Isub1);
471  Cudd_RecursiveDeref(dd, Id);
472  Cudd_RecursiveDerefZdd(dd, zdd_Id);
473  Cudd_RecursiveDeref(dd, x);
474  Cudd_RecursiveDeref(dd, term0);
475  return(NULL);
476  }
477  Cudd_Ref(term1);
478  Cudd_RecursiveDeref(dd, x);
479  Cudd_RecursiveDeref(dd, Isub1);
480  /* sum = term0 + term1 */
481  sum = cuddBddAndRecur(dd, Cudd_Not(term0), Cudd_Not(term1));
482  if (sum == NULL) {
483  Cudd_RecursiveDerefZdd(dd, zdd_Isub0);
484  Cudd_RecursiveDerefZdd(dd, zdd_Isub1);
485  Cudd_RecursiveDeref(dd, Id);
486  Cudd_RecursiveDerefZdd(dd, zdd_Id);
487  Cudd_RecursiveDeref(dd, term0);
488  Cudd_RecursiveDeref(dd, term1);
489  return(NULL);
490  }
491  sum = Cudd_Not(sum);
492  Cudd_Ref(sum);
493  Cudd_RecursiveDeref(dd, term0);
494  Cudd_RecursiveDeref(dd, term1);
495  /* r = sum + Id */
496  r = cuddBddAndRecur(dd, Cudd_Not(sum), Cudd_Not(Id));
497  r = Cudd_NotCond(r, r != NULL);
498  if (r == NULL) {
499  Cudd_RecursiveDerefZdd(dd, zdd_Isub0);
500  Cudd_RecursiveDerefZdd(dd, zdd_Isub1);
501  Cudd_RecursiveDeref(dd, Id);
502  Cudd_RecursiveDerefZdd(dd, zdd_Id);
503  Cudd_RecursiveDeref(dd, sum);
504  return(NULL);
505  }
506  Cudd_Ref(r);
507  Cudd_RecursiveDeref(dd, sum);
508  Cudd_RecursiveDeref(dd, Id);
509 
510  if (zdd_Isub0 != zdd_zero) {
511  z = cuddZddGetNodeIVO(dd, index * 2 + 1, zdd_Isub0, zdd_Id);
512  if (z == NULL) {
513  Cudd_RecursiveDerefZdd(dd, zdd_Isub0);
514  Cudd_RecursiveDerefZdd(dd, zdd_Isub1);
515  Cudd_RecursiveDerefZdd(dd, zdd_Id);
516  Cudd_RecursiveDeref(dd, r);
517  return(NULL);
518  }
519  }
520  else {
521  z = zdd_Id;
522  }
523  Cudd_Ref(z);
524  if (zdd_Isub1 != zdd_zero) {
525  y = cuddZddGetNodeIVO(dd, index * 2, zdd_Isub1, z);
526  if (y == NULL) {
527  Cudd_RecursiveDerefZdd(dd, zdd_Isub0);
528  Cudd_RecursiveDerefZdd(dd, zdd_Isub1);
529  Cudd_RecursiveDerefZdd(dd, zdd_Id);
530  Cudd_RecursiveDeref(dd, r);
531  Cudd_RecursiveDerefZdd(dd, z);
532  return(NULL);
533  }
534  }
535  else
536  y = z;
537  Cudd_Ref(y);
538 
539  Cudd_RecursiveDerefZdd(dd, zdd_Isub0);
540  Cudd_RecursiveDerefZdd(dd, zdd_Isub1);
541  Cudd_RecursiveDerefZdd(dd, zdd_Id);
542  Cudd_RecursiveDerefZdd(dd, z);
543 
544  cuddCacheInsert2(dd, cuddBddIsop, L, U, r);
545  cuddCacheInsert2(dd, cacheOp, L, U, y);
546 
547  Cudd_Deref(r);
548  Cudd_Deref(y);
549  *zdd_I = y;
550  /*
551  if (Cudd_Regular(r)->index != y->index / 2) {
552  printf("*** ERROR : mismatch in indices between BDD and ZDD. ***\n");
553  }
554  */
555  return(r);
556 
557 } /* end of cuddZddIsop */
558 
559 
571 DdNode *
572 cuddBddIsop(
573  DdManager * dd,
574  DdNode * L,
575  DdNode * U)
576 {
577  DdNode *one = DD_ONE(dd);
578  DdNode *zero = Cudd_Not(one);
579  int v, top_l, top_u;
580  DdNode *Lsub0, *Usub0, *Lsub1, *Usub1, *Ld, *Ud;
581  DdNode *Lsuper0, *Usuper0, *Lsuper1, *Usuper1;
582  DdNode *Isub0, *Isub1, *Id;
583  DdNode *x;
584  DdNode *term0, *term1, *sum;
585  DdNode *Lv, *Uv, *Lnv, *Unv;
586  DdNode *r;
587  int index;
588 
589  statLine(dd);
590  if (L == zero)
591  return(zero);
592  if (U == one)
593  return(one);
594 
595  /* Check cache */
596  r = cuddCacheLookup2(dd, cuddBddIsop, L, U);
597  if (r)
598  return(r);
599 
600  top_l = dd->perm[Cudd_Regular(L)->index];
601  top_u = dd->perm[Cudd_Regular(U)->index];
602  v = ddMin(top_l, top_u);
603 
604  /* Compute cofactors */
605  if (top_l == v) {
606  index = Cudd_Regular(L)->index;
607  Lv = Cudd_T(L);
608  Lnv = Cudd_E(L);
609  if (Cudd_IsComplement(L)) {
610  Lv = Cudd_Not(Lv);
611  Lnv = Cudd_Not(Lnv);
612  }
613  }
614  else {
615  index = Cudd_Regular(U)->index;
616  Lv = Lnv = L;
617  }
618 
619  if (top_u == v) {
620  Uv = Cudd_T(U);
621  Unv = Cudd_E(U);
622  if (Cudd_IsComplement(U)) {
623  Uv = Cudd_Not(Uv);
624  Unv = Cudd_Not(Unv);
625  }
626  }
627  else {
628  Uv = Unv = U;
629  }
630 
631  Lsub0 = cuddBddAndRecur(dd, Lnv, Cudd_Not(Uv));
632  if (Lsub0 == NULL)
633  return(NULL);
634  Cudd_Ref(Lsub0);
635  Usub0 = Unv;
636  Lsub1 = cuddBddAndRecur(dd, Lv, Cudd_Not(Unv));
637  if (Lsub1 == NULL) {
638  Cudd_RecursiveDeref(dd, Lsub0);
639  return(NULL);
640  }
641  Cudd_Ref(Lsub1);
642  Usub1 = Uv;
643 
644  Isub0 = cuddBddIsop(dd, Lsub0, Usub0);
645  if (Isub0 == NULL) {
646  Cudd_RecursiveDeref(dd, Lsub0);
647  Cudd_RecursiveDeref(dd, Lsub1);
648  return(NULL);
649  }
650  Cudd_Ref(Isub0);
651  Isub1 = cuddBddIsop(dd, Lsub1, Usub1);
652  if (Isub1 == NULL) {
653  Cudd_RecursiveDeref(dd, Lsub0);
654  Cudd_RecursiveDeref(dd, Lsub1);
655  Cudd_RecursiveDeref(dd, Isub0);
656  return(NULL);
657  }
658  Cudd_Ref(Isub1);
659  Cudd_RecursiveDeref(dd, Lsub0);
660  Cudd_RecursiveDeref(dd, Lsub1);
661 
662  Lsuper0 = cuddBddAndRecur(dd, Lnv, Cudd_Not(Isub0));
663  if (Lsuper0 == NULL) {
664  Cudd_RecursiveDeref(dd, Isub0);
665  Cudd_RecursiveDeref(dd, Isub1);
666  return(NULL);
667  }
668  Cudd_Ref(Lsuper0);
669  Lsuper1 = cuddBddAndRecur(dd, Lv, Cudd_Not(Isub1));
670  if (Lsuper1 == NULL) {
671  Cudd_RecursiveDeref(dd, Isub0);
672  Cudd_RecursiveDeref(dd, Isub1);
673  Cudd_RecursiveDeref(dd, Lsuper0);
674  return(NULL);
675  }
676  Cudd_Ref(Lsuper1);
677  Usuper0 = Unv;
678  Usuper1 = Uv;
679 
680  /* Ld = Lsuper0 + Lsuper1 */
681  Ld = cuddBddAndRecur(dd, Cudd_Not(Lsuper0), Cudd_Not(Lsuper1));
682  Ld = Cudd_NotCond(Ld, Ld != NULL);
683  if (Ld == NULL) {
684  Cudd_RecursiveDeref(dd, Isub0);
685  Cudd_RecursiveDeref(dd, Isub1);
686  Cudd_RecursiveDeref(dd, Lsuper0);
687  Cudd_RecursiveDeref(dd, Lsuper1);
688  return(NULL);
689  }
690  Cudd_Ref(Ld);
691  Ud = cuddBddAndRecur(dd, Usuper0, Usuper1);
692  if (Ud == NULL) {
693  Cudd_RecursiveDeref(dd, Isub0);
694  Cudd_RecursiveDeref(dd, Isub1);
695  Cudd_RecursiveDeref(dd, Lsuper0);
696  Cudd_RecursiveDeref(dd, Lsuper1);
697  Cudd_RecursiveDeref(dd, Ld);
698  return(NULL);
699  }
700  Cudd_Ref(Ud);
701  Cudd_RecursiveDeref(dd, Lsuper0);
702  Cudd_RecursiveDeref(dd, Lsuper1);
703 
704  Id = cuddBddIsop(dd, Ld, Ud);
705  if (Id == NULL) {
706  Cudd_RecursiveDeref(dd, Isub0);
707  Cudd_RecursiveDeref(dd, Isub1);
708  Cudd_RecursiveDeref(dd, Ld);
709  Cudd_RecursiveDeref(dd, Ud);
710  return(NULL);
711  }
712  Cudd_Ref(Id);
713  Cudd_RecursiveDeref(dd, Ld);
714  Cudd_RecursiveDeref(dd, Ud);
715 
716  x = cuddUniqueInter(dd, index, one, zero);
717  if (x == NULL) {
718  Cudd_RecursiveDeref(dd, Isub0);
719  Cudd_RecursiveDeref(dd, Isub1);
720  Cudd_RecursiveDeref(dd, Id);
721  return(NULL);
722  }
723  Cudd_Ref(x);
724  term0 = cuddBddAndRecur(dd, Cudd_Not(x), Isub0);
725  if (term0 == NULL) {
726  Cudd_RecursiveDeref(dd, Isub0);
727  Cudd_RecursiveDeref(dd, Isub1);
728  Cudd_RecursiveDeref(dd, Id);
729  Cudd_RecursiveDeref(dd, x);
730  return(NULL);
731  }
732  Cudd_Ref(term0);
733  Cudd_RecursiveDeref(dd, Isub0);
734  term1 = cuddBddAndRecur(dd, x, Isub1);
735  if (term1 == NULL) {
736  Cudd_RecursiveDeref(dd, Isub1);
737  Cudd_RecursiveDeref(dd, Id);
738  Cudd_RecursiveDeref(dd, x);
739  Cudd_RecursiveDeref(dd, term0);
740  return(NULL);
741  }
742  Cudd_Ref(term1);
743  Cudd_RecursiveDeref(dd, x);
744  Cudd_RecursiveDeref(dd, Isub1);
745  /* sum = term0 + term1 */
746  sum = cuddBddAndRecur(dd, Cudd_Not(term0), Cudd_Not(term1));
747  sum = Cudd_NotCond(sum, sum != NULL);
748  if (sum == NULL) {
749  Cudd_RecursiveDeref(dd, Id);
750  Cudd_RecursiveDeref(dd, term0);
751  Cudd_RecursiveDeref(dd, term1);
752  return(NULL);
753  }
754  Cudd_Ref(sum);
755  Cudd_RecursiveDeref(dd, term0);
756  Cudd_RecursiveDeref(dd, term1);
757  /* r = sum + Id */
758  r = cuddBddAndRecur(dd, Cudd_Not(sum), Cudd_Not(Id));
759  r = Cudd_NotCond(r, r != NULL);
760  if (r == NULL) {
761  Cudd_RecursiveDeref(dd, Id);
762  Cudd_RecursiveDeref(dd, sum);
763  return(NULL);
764  }
765  Cudd_Ref(r);
766  Cudd_RecursiveDeref(dd, sum);
767  Cudd_RecursiveDeref(dd, Id);
768 
769  cuddCacheInsert2(dd, cuddBddIsop, L, U, r);
770 
771  Cudd_Deref(r);
772  return(r);
773 
774 } /* end of cuddBddIsop */
775 
776 
796 DdNode *
797 cuddMakeBddFromZddCover(
798  DdManager * dd,
799  DdNode * node)
800 {
801  DdNode *neW;
802  int v;
803  DdNode *f1, *f0, *fd;
804  DdNode *b1, *b0, *bd;
805  DdNode *T, *E;
806 
807  statLine(dd);
808  if (node == dd->one)
809  return(dd->one);
810  if (node == dd->zero)
811  return(Cudd_Not(dd->one));
812 
813  /* Check cache */
814  neW = cuddCacheLookup1(dd, cuddMakeBddFromZddCover, node);
815  if (neW)
816  return(neW);
817 
818  v = Cudd_Regular(node)->index; /* either yi or zi */
819  if (cuddZddGetCofactors3(dd, node, v, &f1, &f0, &fd)) return(NULL);
820  Cudd_Ref(f1);
821  Cudd_Ref(f0);
822  Cudd_Ref(fd);
823 
824  b1 = cuddMakeBddFromZddCover(dd, f1);
825  if (!b1) {
826  Cudd_RecursiveDerefZdd(dd, f1);
827  Cudd_RecursiveDerefZdd(dd, f0);
828  Cudd_RecursiveDerefZdd(dd, fd);
829  return(NULL);
830  }
831  Cudd_Ref(b1);
832  b0 = cuddMakeBddFromZddCover(dd, f0);
833  if (!b0) {
834  Cudd_RecursiveDerefZdd(dd, f1);
835  Cudd_RecursiveDerefZdd(dd, f0);
836  Cudd_RecursiveDerefZdd(dd, fd);
837  Cudd_RecursiveDeref(dd, b1);
838  return(NULL);
839  }
840  Cudd_Ref(b0);
841  Cudd_RecursiveDerefZdd(dd, f1);
842  Cudd_RecursiveDerefZdd(dd, f0);
843  if (fd != dd->zero) {
844  bd = cuddMakeBddFromZddCover(dd, fd);
845  if (!bd) {
846  Cudd_RecursiveDerefZdd(dd, fd);
847  Cudd_RecursiveDeref(dd, b1);
848  Cudd_RecursiveDeref(dd, b0);
849  return(NULL);
850  }
851  Cudd_Ref(bd);
852  Cudd_RecursiveDerefZdd(dd, fd);
853 
854  T = cuddBddAndRecur(dd, Cudd_Not(b1), Cudd_Not(bd));
855  if (!T) {
856  Cudd_RecursiveDeref(dd, b1);
857  Cudd_RecursiveDeref(dd, b0);
858  Cudd_RecursiveDeref(dd, bd);
859  return(NULL);
860  }
861  T = Cudd_NotCond(T, T != NULL);
862  Cudd_Ref(T);
863  Cudd_RecursiveDeref(dd, b1);
864  E = cuddBddAndRecur(dd, Cudd_Not(b0), Cudd_Not(bd));
865  if (!E) {
866  Cudd_RecursiveDeref(dd, b0);
867  Cudd_RecursiveDeref(dd, bd);
868  Cudd_RecursiveDeref(dd, T);
869  return(NULL);
870  }
871  E = Cudd_NotCond(E, E != NULL);
872  Cudd_Ref(E);
873  Cudd_RecursiveDeref(dd, b0);
874  Cudd_RecursiveDeref(dd, bd);
875  }
876  else {
877  Cudd_RecursiveDerefZdd(dd, fd);
878  T = b1;
879  E = b0;
880  }
881 
882  if (Cudd_IsComplement(T)) {
883  neW = cuddUniqueInterIVO(dd, v / 2, Cudd_Not(T), Cudd_Not(E));
884  if (!neW) {
885  Cudd_RecursiveDeref(dd, T);
886  Cudd_RecursiveDeref(dd, E);
887  return(NULL);
888  }
889  neW = Cudd_Not(neW);
890  }
891  else {
892  neW = cuddUniqueInterIVO(dd, v / 2, T, E);
893  if (!neW) {
894  Cudd_RecursiveDeref(dd, T);
895  Cudd_RecursiveDeref(dd, E);
896  return(NULL);
897  }
898  }
899  Cudd_Ref(neW);
900  Cudd_RecursiveDeref(dd, T);
901  Cudd_RecursiveDeref(dd, E);
902 
903  cuddCacheInsert1(dd, cuddMakeBddFromZddCover, node, neW);
904  Cudd_Deref(neW);
905  return(neW);
906 
907 } /* end of cuddMakeBddFromZddCover */
908 
909 
910 /*---------------------------------------------------------------------------*/
911 /* Definition of static functions */
912 /*---------------------------------------------------------------------------*/
cuddZddGetNodeIVO
DdNode * cuddZddGetNodeIVO(DdManager *dd, int index, DdNode *g, DdNode *h)
Definition: cuddTable.c:1083
cuddRef
#define cuddRef(n)
Definition: cuddInt.h:557
Cudd_RecursiveDerefZdd
void Cudd_RecursiveDerefZdd(DdManager *table, DdNode *n)
Definition: cuddRef.c:381
Cudd_T
#define Cudd_T(node)
Definition: cudd.h:427
exit
VOID_OR_INT exit()
Cudd_E
#define Cudd_E(node)
Definition: cudd.h:442
Cudd_RecursiveDeref
void Cudd_RecursiveDeref(DdManager *table, DdNode *n)
Definition: cuddRef.c:150
DdNode
Definition: cudd.h:270
Cudd_Not
#define Cudd_Not(node)
Definition: cudd.h:354
cuddCacheLookup1
DdNode * cuddCacheLookup1(DdManager *table, DdNode *(*)(DdManager *, DdNode *), DdNode *f)
Cudd_Deref
void Cudd_Deref(DdNode *node)
Definition: cuddRef.c:434
cuddCacheLookup2
DdNode * cuddCacheLookup2(DdManager *table, DdNode *(*)(DdManager *, DdNode *, DdNode *), DdNode *f, DdNode *g)
DdManager::zero
DdNode * zero
Definition: cuddInt.h:330
Cudd_Regular
#define Cudd_Regular(node)
Definition: cudd.h:384
cuddCacheInsert1
void cuddCacheInsert1(DdManager *table, DdNode *(*)(DdManager *, DdNode *), DdNode *f, DdNode *data)
cuddMakeBddFromZddCover
DdNode * cuddMakeBddFromZddCover(DdManager *dd, DdNode *node)
Definition: cuddZddIsop.c:797
statLine
#define statLine(dd)
Definition: cuddInt.h:990
cuddZddIsop
DdNode * cuddZddIsop(DdManager *dd, DdNode *L, DdNode *U, DdNode **zdd_I)
Definition: cuddZddIsop.c:231
DdManager::reordered
int reordered
Definition: cuddInt.h:392
one
static DdNode * one
Definition: cuddSat.c:105
Cudd_IsComplement
#define Cudd_IsComplement(node)
Definition: cudd.h:412
DD_CTFP
DdNode *(* DD_CTFP)(DdManager *, DdNode *, DdNode *)
Definition: cudd.h:308
cuddUniqueInterIVO
DdNode * cuddUniqueInterIVO(DdManager *unique, int index, DdNode *T, DdNode *E)
Definition: cuddTable.c:1333
Cudd_zddIsop
DdNode * Cudd_zddIsop(DdManager *dd, DdNode *L, DdNode *U, DdNode **zdd_I)
Definition: cuddZddIsop.c:132
ddMin
#define ddMin(x, y)
Definition: cuddInt.h:771
cuddZddGetCofactors3
int cuddZddGetCofactors3(DdManager *dd, DdNode *f, int v, DdNode **f1, DdNode **f0, DdNode **fd)
Definition: cuddZddFuncs.c:1356
cuddCacheLookup2Zdd
DdNode * cuddCacheLookup2Zdd(DdManager *table, DdNode *(*)(DdManager *, DdNode *, DdNode *), DdNode *f, DdNode *g)
cuddBddAndRecur
DdNode * cuddBddAndRecur(DdManager *manager, DdNode *f, DdNode *g)
Definition: cuddBddIte.c:995
Cudd_MakeBddFromZddCover
DdNode * Cudd_MakeBddFromZddCover(DdManager *dd, DdNode *node)
Definition: cuddZddIsop.c:200
cuddCacheInsert2
void cuddCacheInsert2(DdManager *table, DdNode *(*)(DdManager *, DdNode *, DdNode *), DdNode *f, DdNode *g, DdNode *data)
zero
static DdNode * zero
Definition: cuddSat.c:105
DdManager::one
DdNode * one
Definition: cuddInt.h:329
cuddBddIsop
DdNode * cuddBddIsop(DdManager *dd, DdNode *L, DdNode *U)
Definition: cuddZddIsop.c:572
DdManager::autoDynZ
int autoDynZ
Definition: cuddInt.h:401
Cudd_NotCond
#define Cudd_NotCond(node, c)
Definition: cudd.h:370
Cudd_bddIsop
DdNode * Cudd_bddIsop(DdManager *dd, DdNode *L, DdNode *U)
Definition: cuddZddIsop.c:170
DD_UNUSED
static char rcsid [] DD_UNUSED
Definition: cuddZddIsop.c:87
Cudd_Ref
void Cudd_Ref(DdNode *n)
Definition: cuddRef.c:125
DD_ONE
#define DD_ONE(dd)
Definition: cuddInt.h:864
DdManager::perm
int * perm
Definition: cuddInt.h:369
cuddUniqueInter
DdNode * cuddUniqueInter(DdManager *unique, int index, DdNode *T, DdNode *E)
Definition: cuddTable.c:1137
DD_ZERO
#define DD_ZERO(dd)
Definition: cuddInt.h:880
Generated by   doxygen 1.8.13