SVF
cuddZddFuncs.c
Go to the documentation of this file.
1 
78 #include "CUDD/util.h"
79 #include "CUDD/cuddInt.h"
80 
81 /*---------------------------------------------------------------------------*/
82 /* Constant declarations */
83 /*---------------------------------------------------------------------------*/
84 
85 
86 /*---------------------------------------------------------------------------*/
87 /* Stucture declarations */
88 /*---------------------------------------------------------------------------*/
89 
90 
91 /*---------------------------------------------------------------------------*/
92 /* Type declarations */
93 /*---------------------------------------------------------------------------*/
94 
95 
96 /*---------------------------------------------------------------------------*/
97 /* Variable declarations */
98 /*---------------------------------------------------------------------------*/
99 
100 #ifndef lint
101 static char rcsid[] DD_UNUSED = "$Id: cuddZddFuncs.c,v 1.17 2012/02/05 01:07:19 fabio Exp $";
102 #endif
103 
104 /*---------------------------------------------------------------------------*/
105 /* Macro declarations */
106 /*---------------------------------------------------------------------------*/
107 
108 
111 /*---------------------------------------------------------------------------*/
112 /* Static function prototypes */
113 /*---------------------------------------------------------------------------*/
114 
115 
119 /*---------------------------------------------------------------------------*/
120 /* Definition of exported functions */
121 /*---------------------------------------------------------------------------*/
122 
123 
140 DdNode *
141 Cudd_zddProduct(
142  DdManager * dd,
143  DdNode * f,
144  DdNode * g)
145 {
146  DdNode *res;
147 
148  do {
149  dd->reordered = 0;
150  res = cuddZddProduct(dd, f, g);
151  } while (dd->reordered == 1);
152  return(res);
153 
154 } /* end of Cudd_zddProduct */
155 
156 
171 DdNode *
172 Cudd_zddUnateProduct(
173  DdManager * dd,
174  DdNode * f,
175  DdNode * g)
176 {
177  DdNode *res;
178 
179  do {
180  dd->reordered = 0;
181  res = cuddZddUnateProduct(dd, f, g);
182  } while (dd->reordered == 1);
183  return(res);
184 
185 } /* end of Cudd_zddUnateProduct */
186 
187 
205 DdNode *
206 Cudd_zddWeakDiv(
207  DdManager * dd,
208  DdNode * f,
209  DdNode * g)
210 {
211  DdNode *res;
212 
213  do {
214  dd->reordered = 0;
215  res = cuddZddWeakDiv(dd, f, g);
216  } while (dd->reordered == 1);
217  return(res);
218 
219 } /* end of Cudd_zddWeakDiv */
220 
221 
236 DdNode *
237 Cudd_zddDivide(
238  DdManager * dd,
239  DdNode * f,
240  DdNode * g)
241 {
242  DdNode *res;
243 
244  do {
245  dd->reordered = 0;
246  res = cuddZddDivide(dd, f, g);
247  } while (dd->reordered == 1);
248  return(res);
249 
250 } /* end of Cudd_zddDivide */
251 
252 
265 DdNode *
266 Cudd_zddWeakDivF(
267  DdManager * dd,
268  DdNode * f,
269  DdNode * g)
270 {
271  DdNode *res;
272 
273  do {
274  dd->reordered = 0;
275  res = cuddZddWeakDivF(dd, f, g);
276  } while (dd->reordered == 1);
277  return(res);
278 
279 } /* end of Cudd_zddWeakDivF */
280 
281 
294 DdNode *
295 Cudd_zddDivideF(
296  DdManager * dd,
297  DdNode * f,
298  DdNode * g)
299 {
300  DdNode *res;
301 
302  do {
303  dd->reordered = 0;
304  res = cuddZddDivideF(dd, f, g);
305  } while (dd->reordered == 1);
306  return(res);
307 
308 } /* end of Cudd_zddDivideF */
309 
310 
327 DdNode *
328 Cudd_zddComplement(
329  DdManager *dd,
330  DdNode *node)
331 {
332  DdNode *b, *isop, *zdd_I;
333 
334  /* Check cache */
335  zdd_I = cuddCacheLookup1Zdd(dd, cuddZddComplement, node);
336  if (zdd_I)
337  return(zdd_I);
338 
339  b = Cudd_MakeBddFromZddCover(dd, node);
340  if (!b)
341  return(NULL);
342  Cudd_Ref(b);
343  isop = Cudd_zddIsop(dd, Cudd_Not(b), Cudd_Not(b), &zdd_I);
344  if (!isop) {
345  Cudd_RecursiveDeref(dd, b);
346  return(NULL);
347  }
348  Cudd_Ref(isop);
349  Cudd_Ref(zdd_I);
350  Cudd_RecursiveDeref(dd, b);
351  Cudd_RecursiveDeref(dd, isop);
352 
353  cuddCacheInsert1(dd, cuddZddComplement, node, zdd_I);
354  Cudd_Deref(zdd_I);
355  return(zdd_I);
356 } /* end of Cudd_zddComplement */
357 
358 
359 /*---------------------------------------------------------------------------*/
360 /* Definition of internal functions */
361 /*---------------------------------------------------------------------------*/
362 
363 
375 DdNode *
376 cuddZddProduct(
377  DdManager * dd,
378  DdNode * f,
379  DdNode * g)
380 {
381  int v, top_f, top_g;
382  DdNode *tmp, *term1, *term2, *term3;
383  DdNode *f0, *f1, *fd, *g0, *g1, *gd;
384  DdNode *R0, *R1, *Rd, *N0, *N1;
385  DdNode *r;
386  DdNode *one = DD_ONE(dd);
387  DdNode *zero = DD_ZERO(dd);
388  int flag;
389  int pv, nv;
390 
391  statLine(dd);
392  if (f == zero || g == zero)
393  return(zero);
394  if (f == one)
395  return(g);
396  if (g == one)
397  return(f);
398 
399  top_f = dd->permZ[f->index];
400  top_g = dd->permZ[g->index];
401 
402  if (top_f > top_g)
403  return(cuddZddProduct(dd, g, f));
404 
405  /* Check cache */
406  r = cuddCacheLookup2Zdd(dd, cuddZddProduct, f, g);
407  if (r)
408  return(r);
409 
410  v = f->index; /* either yi or zi */
411  flag = cuddZddGetCofactors3(dd, f, v, &f1, &f0, &fd);
412  if (flag == 1)
413  return(NULL);
414  Cudd_Ref(f1);
415  Cudd_Ref(f0);
416  Cudd_Ref(fd);
417  flag = cuddZddGetCofactors3(dd, g, v, &g1, &g0, &gd);
418  if (flag == 1) {
419  Cudd_RecursiveDerefZdd(dd, f1);
420  Cudd_RecursiveDerefZdd(dd, f0);
421  Cudd_RecursiveDerefZdd(dd, fd);
422  return(NULL);
423  }
424  Cudd_Ref(g1);
425  Cudd_Ref(g0);
426  Cudd_Ref(gd);
427  pv = cuddZddGetPosVarIndex(dd, v);
428  nv = cuddZddGetNegVarIndex(dd, v);
429 
430  Rd = cuddZddProduct(dd, fd, gd);
431  if (Rd == NULL) {
432  Cudd_RecursiveDerefZdd(dd, f1);
433  Cudd_RecursiveDerefZdd(dd, f0);
434  Cudd_RecursiveDerefZdd(dd, fd);
435  Cudd_RecursiveDerefZdd(dd, g1);
436  Cudd_RecursiveDerefZdd(dd, g0);
437  Cudd_RecursiveDerefZdd(dd, gd);
438  return(NULL);
439  }
440  Cudd_Ref(Rd);
441 
442  term1 = cuddZddProduct(dd, f0, g0);
443  if (term1 == NULL) {
444  Cudd_RecursiveDerefZdd(dd, f1);
445  Cudd_RecursiveDerefZdd(dd, f0);
446  Cudd_RecursiveDerefZdd(dd, fd);
447  Cudd_RecursiveDerefZdd(dd, g1);
448  Cudd_RecursiveDerefZdd(dd, g0);
449  Cudd_RecursiveDerefZdd(dd, gd);
450  Cudd_RecursiveDerefZdd(dd, Rd);
451  return(NULL);
452  }
453  Cudd_Ref(term1);
454  term2 = cuddZddProduct(dd, f0, gd);
455  if (term2 == NULL) {
456  Cudd_RecursiveDerefZdd(dd, f1);
457  Cudd_RecursiveDerefZdd(dd, f0);
458  Cudd_RecursiveDerefZdd(dd, fd);
459  Cudd_RecursiveDerefZdd(dd, g1);
460  Cudd_RecursiveDerefZdd(dd, g0);
461  Cudd_RecursiveDerefZdd(dd, gd);
462  Cudd_RecursiveDerefZdd(dd, Rd);
463  Cudd_RecursiveDerefZdd(dd, term1);
464  return(NULL);
465  }
466  Cudd_Ref(term2);
467  term3 = cuddZddProduct(dd, fd, g0);
468  if (term3 == NULL) {
469  Cudd_RecursiveDerefZdd(dd, f1);
470  Cudd_RecursiveDerefZdd(dd, f0);
471  Cudd_RecursiveDerefZdd(dd, fd);
472  Cudd_RecursiveDerefZdd(dd, g1);
473  Cudd_RecursiveDerefZdd(dd, g0);
474  Cudd_RecursiveDerefZdd(dd, gd);
475  Cudd_RecursiveDerefZdd(dd, Rd);
476  Cudd_RecursiveDerefZdd(dd, term1);
477  Cudd_RecursiveDerefZdd(dd, term2);
478  return(NULL);
479  }
480  Cudd_Ref(term3);
481  Cudd_RecursiveDerefZdd(dd, f0);
482  Cudd_RecursiveDerefZdd(dd, g0);
483  tmp = cuddZddUnion(dd, term1, term2);
484  if (tmp == NULL) {
485  Cudd_RecursiveDerefZdd(dd, f1);
486  Cudd_RecursiveDerefZdd(dd, fd);
487  Cudd_RecursiveDerefZdd(dd, g1);
488  Cudd_RecursiveDerefZdd(dd, gd);
489  Cudd_RecursiveDerefZdd(dd, Rd);
490  Cudd_RecursiveDerefZdd(dd, term1);
491  Cudd_RecursiveDerefZdd(dd, term2);
492  Cudd_RecursiveDerefZdd(dd, term3);
493  return(NULL);
494  }
495  Cudd_Ref(tmp);
496  Cudd_RecursiveDerefZdd(dd, term1);
497  Cudd_RecursiveDerefZdd(dd, term2);
498  R0 = cuddZddUnion(dd, tmp, term3);
499  if (R0 == NULL) {
500  Cudd_RecursiveDerefZdd(dd, f1);
501  Cudd_RecursiveDerefZdd(dd, fd);
502  Cudd_RecursiveDerefZdd(dd, g1);
503  Cudd_RecursiveDerefZdd(dd, gd);
504  Cudd_RecursiveDerefZdd(dd, Rd);
505  Cudd_RecursiveDerefZdd(dd, term3);
506  Cudd_RecursiveDerefZdd(dd, tmp);
507  return(NULL);
508  }
509  Cudd_Ref(R0);
510  Cudd_RecursiveDerefZdd(dd, tmp);
511  Cudd_RecursiveDerefZdd(dd, term3);
512  N0 = cuddZddGetNode(dd, nv, R0, Rd); /* nv = zi */
513  if (N0 == NULL) {
514  Cudd_RecursiveDerefZdd(dd, f1);
515  Cudd_RecursiveDerefZdd(dd, fd);
516  Cudd_RecursiveDerefZdd(dd, g1);
517  Cudd_RecursiveDerefZdd(dd, gd);
518  Cudd_RecursiveDerefZdd(dd, Rd);
519  Cudd_RecursiveDerefZdd(dd, R0);
520  return(NULL);
521  }
522  Cudd_Ref(N0);
523  Cudd_RecursiveDerefZdd(dd, R0);
524  Cudd_RecursiveDerefZdd(dd, Rd);
525 
526  term1 = cuddZddProduct(dd, f1, g1);
527  if (term1 == NULL) {
528  Cudd_RecursiveDerefZdd(dd, f1);
529  Cudd_RecursiveDerefZdd(dd, fd);
530  Cudd_RecursiveDerefZdd(dd, g1);
531  Cudd_RecursiveDerefZdd(dd, gd);
532  Cudd_RecursiveDerefZdd(dd, N0);
533  return(NULL);
534  }
535  Cudd_Ref(term1);
536  term2 = cuddZddProduct(dd, f1, gd);
537  if (term2 == NULL) {
538  Cudd_RecursiveDerefZdd(dd, f1);
539  Cudd_RecursiveDerefZdd(dd, fd);
540  Cudd_RecursiveDerefZdd(dd, g1);
541  Cudd_RecursiveDerefZdd(dd, gd);
542  Cudd_RecursiveDerefZdd(dd, N0);
543  Cudd_RecursiveDerefZdd(dd, term1);
544  return(NULL);
545  }
546  Cudd_Ref(term2);
547  term3 = cuddZddProduct(dd, fd, g1);
548  if (term3 == NULL) {
549  Cudd_RecursiveDerefZdd(dd, f1);
550  Cudd_RecursiveDerefZdd(dd, fd);
551  Cudd_RecursiveDerefZdd(dd, g1);
552  Cudd_RecursiveDerefZdd(dd, gd);
553  Cudd_RecursiveDerefZdd(dd, N0);
554  Cudd_RecursiveDerefZdd(dd, term1);
555  Cudd_RecursiveDerefZdd(dd, term2);
556  return(NULL);
557  }
558  Cudd_Ref(term3);
559  Cudd_RecursiveDerefZdd(dd, f1);
560  Cudd_RecursiveDerefZdd(dd, g1);
561  Cudd_RecursiveDerefZdd(dd, fd);
562  Cudd_RecursiveDerefZdd(dd, gd);
563  tmp = cuddZddUnion(dd, term1, term2);
564  if (tmp == NULL) {
565  Cudd_RecursiveDerefZdd(dd, N0);
566  Cudd_RecursiveDerefZdd(dd, term1);
567  Cudd_RecursiveDerefZdd(dd, term2);
568  Cudd_RecursiveDerefZdd(dd, term3);
569  return(NULL);
570  }
571  Cudd_Ref(tmp);
572  Cudd_RecursiveDerefZdd(dd, term1);
573  Cudd_RecursiveDerefZdd(dd, term2);
574  R1 = cuddZddUnion(dd, tmp, term3);
575  if (R1 == NULL) {
576  Cudd_RecursiveDerefZdd(dd, N0);
577  Cudd_RecursiveDerefZdd(dd, term3);
578  Cudd_RecursiveDerefZdd(dd, tmp);
579  return(NULL);
580  }
581  Cudd_Ref(R1);
582  Cudd_RecursiveDerefZdd(dd, tmp);
583  Cudd_RecursiveDerefZdd(dd, term3);
584  N1 = cuddZddGetNode(dd, pv, R1, N0); /* pv = yi */
585  if (N1 == NULL) {
586  Cudd_RecursiveDerefZdd(dd, N0);
587  Cudd_RecursiveDerefZdd(dd, R1);
588  return(NULL);
589  }
590  Cudd_Ref(N1);
591  Cudd_RecursiveDerefZdd(dd, R1);
592  Cudd_RecursiveDerefZdd(dd, N0);
593 
594  cuddCacheInsert2(dd, cuddZddProduct, f, g, N1);
595  Cudd_Deref(N1);
596  return(N1);
597 
598 } /* end of cuddZddProduct */
599 
600 
612 DdNode *
613 cuddZddUnateProduct(
614  DdManager * dd,
615  DdNode * f,
616  DdNode * g)
617 {
618  int v, top_f, top_g;
619  DdNode *term1, *term2, *term3, *term4;
620  DdNode *sum1, *sum2;
621  DdNode *f0, *f1, *g0, *g1;
622  DdNode *r;
623  DdNode *one = DD_ONE(dd);
624  DdNode *zero = DD_ZERO(dd);
625  int flag;
626 
627  statLine(dd);
628  if (f == zero || g == zero)
629  return(zero);
630  if (f == one)
631  return(g);
632  if (g == one)
633  return(f);
634 
635  top_f = dd->permZ[f->index];
636  top_g = dd->permZ[g->index];
637 
638  if (top_f > top_g)
639  return(cuddZddUnateProduct(dd, g, f));
640 
641  /* Check cache */
642  r = cuddCacheLookup2Zdd(dd, cuddZddUnateProduct, f, g);
643  if (r)
644  return(r);
645 
646  v = f->index; /* either yi or zi */
647  flag = cuddZddGetCofactors2(dd, f, v, &f1, &f0);
648  if (flag == 1)
649  return(NULL);
650  Cudd_Ref(f1);
651  Cudd_Ref(f0);
652  flag = cuddZddGetCofactors2(dd, g, v, &g1, &g0);
653  if (flag == 1) {
654  Cudd_RecursiveDerefZdd(dd, f1);
655  Cudd_RecursiveDerefZdd(dd, f0);
656  return(NULL);
657  }
658  Cudd_Ref(g1);
659  Cudd_Ref(g0);
660 
661  term1 = cuddZddUnateProduct(dd, f1, g1);
662  if (term1 == NULL) {
663  Cudd_RecursiveDerefZdd(dd, f1);
664  Cudd_RecursiveDerefZdd(dd, f0);
665  Cudd_RecursiveDerefZdd(dd, g1);
666  Cudd_RecursiveDerefZdd(dd, g0);
667  return(NULL);
668  }
669  Cudd_Ref(term1);
670  term2 = cuddZddUnateProduct(dd, f1, g0);
671  if (term2 == NULL) {
672  Cudd_RecursiveDerefZdd(dd, f1);
673  Cudd_RecursiveDerefZdd(dd, f0);
674  Cudd_RecursiveDerefZdd(dd, g1);
675  Cudd_RecursiveDerefZdd(dd, g0);
676  Cudd_RecursiveDerefZdd(dd, term1);
677  return(NULL);
678  }
679  Cudd_Ref(term2);
680  term3 = cuddZddUnateProduct(dd, f0, g1);
681  if (term3 == NULL) {
682  Cudd_RecursiveDerefZdd(dd, f1);
683  Cudd_RecursiveDerefZdd(dd, f0);
684  Cudd_RecursiveDerefZdd(dd, g1);
685  Cudd_RecursiveDerefZdd(dd, g0);
686  Cudd_RecursiveDerefZdd(dd, term1);
687  Cudd_RecursiveDerefZdd(dd, term2);
688  return(NULL);
689  }
690  Cudd_Ref(term3);
691  term4 = cuddZddUnateProduct(dd, f0, g0);
692  if (term4 == NULL) {
693  Cudd_RecursiveDerefZdd(dd, f1);
694  Cudd_RecursiveDerefZdd(dd, f0);
695  Cudd_RecursiveDerefZdd(dd, g1);
696  Cudd_RecursiveDerefZdd(dd, g0);
697  Cudd_RecursiveDerefZdd(dd, term1);
698  Cudd_RecursiveDerefZdd(dd, term2);
699  Cudd_RecursiveDerefZdd(dd, term3);
700  return(NULL);
701  }
702  Cudd_Ref(term4);
703  Cudd_RecursiveDerefZdd(dd, f1);
704  Cudd_RecursiveDerefZdd(dd, f0);
705  Cudd_RecursiveDerefZdd(dd, g1);
706  Cudd_RecursiveDerefZdd(dd, g0);
707  sum1 = cuddZddUnion(dd, term1, term2);
708  if (sum1 == NULL) {
709  Cudd_RecursiveDerefZdd(dd, term1);
710  Cudd_RecursiveDerefZdd(dd, term2);
711  Cudd_RecursiveDerefZdd(dd, term3);
712  Cudd_RecursiveDerefZdd(dd, term4);
713  return(NULL);
714  }
715  Cudd_Ref(sum1);
716  Cudd_RecursiveDerefZdd(dd, term1);
717  Cudd_RecursiveDerefZdd(dd, term2);
718  sum2 = cuddZddUnion(dd, sum1, term3);
719  if (sum2 == NULL) {
720  Cudd_RecursiveDerefZdd(dd, term3);
721  Cudd_RecursiveDerefZdd(dd, term4);
722  Cudd_RecursiveDerefZdd(dd, sum1);
723  return(NULL);
724  }
725  Cudd_Ref(sum2);
726  Cudd_RecursiveDerefZdd(dd, sum1);
727  Cudd_RecursiveDerefZdd(dd, term3);
728  r = cuddZddGetNode(dd, v, sum2, term4);
729  if (r == NULL) {
730  Cudd_RecursiveDerefZdd(dd, term4);
731  Cudd_RecursiveDerefZdd(dd, sum2);
732  return(NULL);
733  }
734  Cudd_Ref(r);
735  Cudd_RecursiveDerefZdd(dd, sum2);
736  Cudd_RecursiveDerefZdd(dd, term4);
737 
738  cuddCacheInsert2(dd, cuddZddUnateProduct, f, g, r);
739  Cudd_Deref(r);
740  return(r);
741 
742 } /* end of cuddZddUnateProduct */
743 
744 
756 DdNode *
757 cuddZddWeakDiv(
758  DdManager * dd,
759  DdNode * f,
760  DdNode * g)
761 {
762  int v;
763  DdNode *one = DD_ONE(dd);
764  DdNode *zero = DD_ZERO(dd);
765  DdNode *f0, *f1, *fd, *g0, *g1, *gd;
766  DdNode *q, *tmp;
767  DdNode *r;
768  int flag;
769 
770  statLine(dd);
771  if (g == one)
772  return(f);
773  if (f == zero || f == one)
774  return(zero);
775  if (f == g)
776  return(one);
777 
778  /* Check cache. */
779  r = cuddCacheLookup2Zdd(dd, cuddZddWeakDiv, f, g);
780  if (r)
781  return(r);
782 
783  v = g->index;
784 
785  flag = cuddZddGetCofactors3(dd, f, v, &f1, &f0, &fd);
786  if (flag == 1)
787  return(NULL);
788  Cudd_Ref(f1);
789  Cudd_Ref(f0);
790  Cudd_Ref(fd);
791  flag = cuddZddGetCofactors3(dd, g, v, &g1, &g0, &gd);
792  if (flag == 1) {
793  Cudd_RecursiveDerefZdd(dd, f1);
794  Cudd_RecursiveDerefZdd(dd, f0);
795  Cudd_RecursiveDerefZdd(dd, fd);
796  return(NULL);
797  }
798  Cudd_Ref(g1);
799  Cudd_Ref(g0);
800  Cudd_Ref(gd);
801 
802  q = g;
803 
804  if (g0 != zero) {
805  q = cuddZddWeakDiv(dd, f0, g0);
806  if (q == NULL) {
807  Cudd_RecursiveDerefZdd(dd, f1);
808  Cudd_RecursiveDerefZdd(dd, f0);
809  Cudd_RecursiveDerefZdd(dd, fd);
810  Cudd_RecursiveDerefZdd(dd, g1);
811  Cudd_RecursiveDerefZdd(dd, g0);
812  Cudd_RecursiveDerefZdd(dd, gd);
813  return(NULL);
814  }
815  Cudd_Ref(q);
816  }
817  else
818  Cudd_Ref(q);
819  Cudd_RecursiveDerefZdd(dd, f0);
820  Cudd_RecursiveDerefZdd(dd, g0);
821 
822  if (q == zero) {
823  Cudd_RecursiveDerefZdd(dd, f1);
824  Cudd_RecursiveDerefZdd(dd, g1);
825  Cudd_RecursiveDerefZdd(dd, fd);
826  Cudd_RecursiveDerefZdd(dd, gd);
827  cuddCacheInsert2(dd, cuddZddWeakDiv, f, g, zero);
828  Cudd_Deref(q);
829  return(zero);
830  }
831 
832  if (g1 != zero) {
833  Cudd_RecursiveDerefZdd(dd, q);
834  tmp = cuddZddWeakDiv(dd, f1, g1);
835  if (tmp == NULL) {
836  Cudd_RecursiveDerefZdd(dd, f1);
837  Cudd_RecursiveDerefZdd(dd, g1);
838  Cudd_RecursiveDerefZdd(dd, fd);
839  Cudd_RecursiveDerefZdd(dd, gd);
840  return(NULL);
841  }
842  Cudd_Ref(tmp);
843  Cudd_RecursiveDerefZdd(dd, f1);
844  Cudd_RecursiveDerefZdd(dd, g1);
845  if (q == g)
846  q = tmp;
847  else {
848  q = cuddZddIntersect(dd, q, tmp);
849  if (q == NULL) {
850  Cudd_RecursiveDerefZdd(dd, fd);
851  Cudd_RecursiveDerefZdd(dd, gd);
852  return(NULL);
853  }
854  Cudd_Ref(q);
855  Cudd_RecursiveDerefZdd(dd, tmp);
856  }
857  }
858  else {
859  Cudd_RecursiveDerefZdd(dd, f1);
860  Cudd_RecursiveDerefZdd(dd, g1);
861  }
862 
863  if (q == zero) {
864  Cudd_RecursiveDerefZdd(dd, fd);
865  Cudd_RecursiveDerefZdd(dd, gd);
866  cuddCacheInsert2(dd, cuddZddWeakDiv, f, g, zero);
867  Cudd_Deref(q);
868  return(zero);
869  }
870 
871  if (gd != zero) {
872  Cudd_RecursiveDerefZdd(dd, q);
873  tmp = cuddZddWeakDiv(dd, fd, gd);
874  if (tmp == NULL) {
875  Cudd_RecursiveDerefZdd(dd, fd);
876  Cudd_RecursiveDerefZdd(dd, gd);
877  return(NULL);
878  }
879  Cudd_Ref(tmp);
880  Cudd_RecursiveDerefZdd(dd, fd);
881  Cudd_RecursiveDerefZdd(dd, gd);
882  if (q == g)
883  q = tmp;
884  else {
885  q = cuddZddIntersect(dd, q, tmp);
886  if (q == NULL) {
887  Cudd_RecursiveDerefZdd(dd, tmp);
888  return(NULL);
889  }
890  Cudd_Ref(q);
891  Cudd_RecursiveDerefZdd(dd, tmp);
892  }
893  }
894  else {
895  Cudd_RecursiveDerefZdd(dd, fd);
896  Cudd_RecursiveDerefZdd(dd, gd);
897  }
898 
899  cuddCacheInsert2(dd, cuddZddWeakDiv, f, g, q);
900  Cudd_Deref(q);
901  return(q);
902 
903 } /* end of cuddZddWeakDiv */
904 
905 
917 DdNode *
918 cuddZddWeakDivF(
919  DdManager * dd,
920  DdNode * f,
921  DdNode * g)
922 {
923  int v, top_f, top_g, vf, vg;
924  DdNode *one = DD_ONE(dd);
925  DdNode *zero = DD_ZERO(dd);
926  DdNode *f0, *f1, *fd, *g0, *g1, *gd;
927  DdNode *q, *tmp;
928  DdNode *r;
929  DdNode *term1, *term0, *termd;
930  int flag;
931  int pv, nv;
932 
933  statLine(dd);
934  if (g == one)
935  return(f);
936  if (f == zero || f == one)
937  return(zero);
938  if (f == g)
939  return(one);
940 
941  /* Check cache. */
942  r = cuddCacheLookup2Zdd(dd, cuddZddWeakDivF, f, g);
943  if (r)
944  return(r);
945 
946  top_f = dd->permZ[f->index];
947  top_g = dd->permZ[g->index];
948  vf = top_f >> 1;
949  vg = top_g >> 1;
950  v = ddMin(top_f, top_g);
951 
952  if (v == top_f && vf < vg) {
953  v = f->index;
954  flag = cuddZddGetCofactors3(dd, f, v, &f1, &f0, &fd);
955  if (flag == 1)
956  return(NULL);
957  Cudd_Ref(f1);
958  Cudd_Ref(f0);
959  Cudd_Ref(fd);
960 
961  pv = cuddZddGetPosVarIndex(dd, v);
962  nv = cuddZddGetNegVarIndex(dd, v);
963 
964  term1 = cuddZddWeakDivF(dd, f1, g);
965  if (term1 == NULL) {
966  Cudd_RecursiveDerefZdd(dd, f1);
967  Cudd_RecursiveDerefZdd(dd, f0);
968  Cudd_RecursiveDerefZdd(dd, fd);
969  return(NULL);
970  }
971  Cudd_Ref(term1);
972  Cudd_RecursiveDerefZdd(dd, f1);
973  term0 = cuddZddWeakDivF(dd, f0, g);
974  if (term0 == NULL) {
975  Cudd_RecursiveDerefZdd(dd, f0);
976  Cudd_RecursiveDerefZdd(dd, fd);
977  Cudd_RecursiveDerefZdd(dd, term1);
978  return(NULL);
979  }
980  Cudd_Ref(term0);
981  Cudd_RecursiveDerefZdd(dd, f0);
982  termd = cuddZddWeakDivF(dd, fd, g);
983  if (termd == NULL) {
984  Cudd_RecursiveDerefZdd(dd, fd);
985  Cudd_RecursiveDerefZdd(dd, term1);
986  Cudd_RecursiveDerefZdd(dd, term0);
987  return(NULL);
988  }
989  Cudd_Ref(termd);
990  Cudd_RecursiveDerefZdd(dd, fd);
991 
992  tmp = cuddZddGetNode(dd, nv, term0, termd); /* nv = zi */
993  if (tmp == NULL) {
994  Cudd_RecursiveDerefZdd(dd, term1);
995  Cudd_RecursiveDerefZdd(dd, term0);
996  Cudd_RecursiveDerefZdd(dd, termd);
997  return(NULL);
998  }
999  Cudd_Ref(tmp);
1000  Cudd_RecursiveDerefZdd(dd, term0);
1001  Cudd_RecursiveDerefZdd(dd, termd);
1002  q = cuddZddGetNode(dd, pv, term1, tmp); /* pv = yi */
1003  if (q == NULL) {
1004  Cudd_RecursiveDerefZdd(dd, term1);
1005  Cudd_RecursiveDerefZdd(dd, tmp);
1006  return(NULL);
1007  }
1008  Cudd_Ref(q);
1009  Cudd_RecursiveDerefZdd(dd, term1);
1010  Cudd_RecursiveDerefZdd(dd, tmp);
1011 
1012  cuddCacheInsert2(dd, cuddZddWeakDivF, f, g, q);
1013  Cudd_Deref(q);
1014  return(q);
1015  }
1016 
1017  if (v == top_f)
1018  v = f->index;
1019  else
1020  v = g->index;
1021 
1022  flag = cuddZddGetCofactors3(dd, f, v, &f1, &f0, &fd);
1023  if (flag == 1)
1024  return(NULL);
1025  Cudd_Ref(f1);
1026  Cudd_Ref(f0);
1027  Cudd_Ref(fd);
1028  flag = cuddZddGetCofactors3(dd, g, v, &g1, &g0, &gd);
1029  if (flag == 1) {
1030  Cudd_RecursiveDerefZdd(dd, f1);
1031  Cudd_RecursiveDerefZdd(dd, f0);
1032  Cudd_RecursiveDerefZdd(dd, fd);
1033  return(NULL);
1034  }
1035  Cudd_Ref(g1);
1036  Cudd_Ref(g0);
1037  Cudd_Ref(gd);
1038 
1039  q = g;
1040 
1041  if (g0 != zero) {
1042  q = cuddZddWeakDivF(dd, f0, g0);
1043  if (q == NULL) {
1044  Cudd_RecursiveDerefZdd(dd, f1);
1045  Cudd_RecursiveDerefZdd(dd, f0);
1046  Cudd_RecursiveDerefZdd(dd, fd);
1047  Cudd_RecursiveDerefZdd(dd, g1);
1048  Cudd_RecursiveDerefZdd(dd, g0);
1049  Cudd_RecursiveDerefZdd(dd, gd);
1050  return(NULL);
1051  }
1052  Cudd_Ref(q);
1053  }
1054  else
1055  Cudd_Ref(q);
1056  Cudd_RecursiveDerefZdd(dd, f0);
1057  Cudd_RecursiveDerefZdd(dd, g0);
1058 
1059  if (q == zero) {
1060  Cudd_RecursiveDerefZdd(dd, f1);
1061  Cudd_RecursiveDerefZdd(dd, g1);
1062  Cudd_RecursiveDerefZdd(dd, fd);
1063  Cudd_RecursiveDerefZdd(dd, gd);
1064  cuddCacheInsert2(dd, cuddZddWeakDivF, f, g, zero);
1065  Cudd_Deref(q);
1066  return(zero);
1067  }
1068 
1069  if (g1 != zero) {
1070  Cudd_RecursiveDerefZdd(dd, q);
1071  tmp = cuddZddWeakDivF(dd, f1, g1);
1072  if (tmp == NULL) {
1073  Cudd_RecursiveDerefZdd(dd, f1);
1074  Cudd_RecursiveDerefZdd(dd, g1);
1075  Cudd_RecursiveDerefZdd(dd, fd);
1076  Cudd_RecursiveDerefZdd(dd, gd);
1077  return(NULL);
1078  }
1079  Cudd_Ref(tmp);
1080  Cudd_RecursiveDerefZdd(dd, f1);
1081  Cudd_RecursiveDerefZdd(dd, g1);
1082  if (q == g)
1083  q = tmp;
1084  else {
1085  q = cuddZddIntersect(dd, q, tmp);
1086  if (q == NULL) {
1087  Cudd_RecursiveDerefZdd(dd, fd);
1088  Cudd_RecursiveDerefZdd(dd, gd);
1089  return(NULL);
1090  }
1091  Cudd_Ref(q);
1092  Cudd_RecursiveDerefZdd(dd, tmp);
1093  }
1094  }
1095  else {
1096  Cudd_RecursiveDerefZdd(dd, f1);
1097  Cudd_RecursiveDerefZdd(dd, g1);
1098  }
1099 
1100  if (q == zero) {
1101  Cudd_RecursiveDerefZdd(dd, fd);
1102  Cudd_RecursiveDerefZdd(dd, gd);
1103  cuddCacheInsert2(dd, cuddZddWeakDivF, f, g, zero);
1104  Cudd_Deref(q);
1105  return(zero);
1106  }
1107 
1108  if (gd != zero) {
1109  Cudd_RecursiveDerefZdd(dd, q);
1110  tmp = cuddZddWeakDivF(dd, fd, gd);
1111  if (tmp == NULL) {
1112  Cudd_RecursiveDerefZdd(dd, fd);
1113  Cudd_RecursiveDerefZdd(dd, gd);
1114  return(NULL);
1115  }
1116  Cudd_Ref(tmp);
1117  Cudd_RecursiveDerefZdd(dd, fd);
1118  Cudd_RecursiveDerefZdd(dd, gd);
1119  if (q == g)
1120  q = tmp;
1121  else {
1122  q = cuddZddIntersect(dd, q, tmp);
1123  if (q == NULL) {
1124  Cudd_RecursiveDerefZdd(dd, tmp);
1125  return(NULL);
1126  }
1127  Cudd_Ref(q);
1128  Cudd_RecursiveDerefZdd(dd, tmp);
1129  }
1130  }
1131  else {
1132  Cudd_RecursiveDerefZdd(dd, fd);
1133  Cudd_RecursiveDerefZdd(dd, gd);
1134  }
1135 
1136  cuddCacheInsert2(dd, cuddZddWeakDivF, f, g, q);
1137  Cudd_Deref(q);
1138  return(q);
1139 
1140 } /* end of cuddZddWeakDivF */
1141 
1142 
1154 DdNode *
1155 cuddZddDivide(
1156  DdManager * dd,
1157  DdNode * f,
1158  DdNode * g)
1159 {
1160  int v;
1161  DdNode *one = DD_ONE(dd);
1162  DdNode *zero = DD_ZERO(dd);
1163  DdNode *f0, *f1, *g0, *g1;
1164  DdNode *q, *r, *tmp;
1165  int flag;
1166 
1167  statLine(dd);
1168  if (g == one)
1169  return(f);
1170  if (f == zero || f == one)
1171  return(zero);
1172  if (f == g)
1173  return(one);
1174 
1175  /* Check cache. */
1176  r = cuddCacheLookup2Zdd(dd, cuddZddDivide, f, g);
1177  if (r)
1178  return(r);
1179 
1180  v = g->index;
1181 
1182  flag = cuddZddGetCofactors2(dd, f, v, &f1, &f0);
1183  if (flag == 1)
1184  return(NULL);
1185  Cudd_Ref(f1);
1186  Cudd_Ref(f0);
1187  flag = cuddZddGetCofactors2(dd, g, v, &g1, &g0); /* g1 != zero */
1188  if (flag == 1) {
1189  Cudd_RecursiveDerefZdd(dd, f1);
1190  Cudd_RecursiveDerefZdd(dd, f0);
1191  return(NULL);
1192  }
1193  Cudd_Ref(g1);
1194  Cudd_Ref(g0);
1195 
1196  r = cuddZddDivide(dd, f1, g1);
1197  if (r == NULL) {
1198  Cudd_RecursiveDerefZdd(dd, f1);
1199  Cudd_RecursiveDerefZdd(dd, f0);
1200  Cudd_RecursiveDerefZdd(dd, g1);
1201  Cudd_RecursiveDerefZdd(dd, g0);
1202  return(NULL);
1203  }
1204  Cudd_Ref(r);
1205 
1206  if (r != zero && g0 != zero) {
1207  tmp = r;
1208  q = cuddZddDivide(dd, f0, g0);
1209  if (q == NULL) {
1210  Cudd_RecursiveDerefZdd(dd, f1);
1211  Cudd_RecursiveDerefZdd(dd, f0);
1212  Cudd_RecursiveDerefZdd(dd, g1);
1213  Cudd_RecursiveDerefZdd(dd, g0);
1214  return(NULL);
1215  }
1216  Cudd_Ref(q);
1217  r = cuddZddIntersect(dd, r, q);
1218  if (r == NULL) {
1219  Cudd_RecursiveDerefZdd(dd, f1);
1220  Cudd_RecursiveDerefZdd(dd, f0);
1221  Cudd_RecursiveDerefZdd(dd, g1);
1222  Cudd_RecursiveDerefZdd(dd, g0);
1223  Cudd_RecursiveDerefZdd(dd, q);
1224  return(NULL);
1225  }
1226  Cudd_Ref(r);
1227  Cudd_RecursiveDerefZdd(dd, q);
1228  Cudd_RecursiveDerefZdd(dd, tmp);
1229  }
1230 
1231  Cudd_RecursiveDerefZdd(dd, f1);
1232  Cudd_RecursiveDerefZdd(dd, f0);
1233  Cudd_RecursiveDerefZdd(dd, g1);
1234  Cudd_RecursiveDerefZdd(dd, g0);
1235 
1236  cuddCacheInsert2(dd, cuddZddDivide, f, g, r);
1237  Cudd_Deref(r);
1238  return(r);
1239 
1240 } /* end of cuddZddDivide */
1241 
1242 
1254 DdNode *
1255 cuddZddDivideF(
1256  DdManager * dd,
1257  DdNode * f,
1258  DdNode * g)
1259 {
1260  int v;
1261  DdNode *one = DD_ONE(dd);
1262  DdNode *zero = DD_ZERO(dd);
1263  DdNode *f0, *f1, *g0, *g1;
1264  DdNode *q, *r, *tmp;
1265  int flag;
1266 
1267  statLine(dd);
1268  if (g == one)
1269  return(f);
1270  if (f == zero || f == one)
1271  return(zero);
1272  if (f == g)
1273  return(one);
1274 
1275  /* Check cache. */
1276  r = cuddCacheLookup2Zdd(dd, cuddZddDivideF, f, g);
1277  if (r)
1278  return(r);
1279 
1280  v = g->index;
1281 
1282  flag = cuddZddGetCofactors2(dd, f, v, &f1, &f0);
1283  if (flag == 1)
1284  return(NULL);
1285  Cudd_Ref(f1);
1286  Cudd_Ref(f0);
1287  flag = cuddZddGetCofactors2(dd, g, v, &g1, &g0); /* g1 != zero */
1288  if (flag == 1) {
1289  Cudd_RecursiveDerefZdd(dd, f1);
1290  Cudd_RecursiveDerefZdd(dd, f0);
1291  return(NULL);
1292  }
1293  Cudd_Ref(g1);
1294  Cudd_Ref(g0);
1295 
1296  r = cuddZddDivideF(dd, f1, g1);
1297  if (r == NULL) {
1298  Cudd_RecursiveDerefZdd(dd, f1);
1299  Cudd_RecursiveDerefZdd(dd, f0);
1300  Cudd_RecursiveDerefZdd(dd, g1);
1301  Cudd_RecursiveDerefZdd(dd, g0);
1302  return(NULL);
1303  }
1304  Cudd_Ref(r);
1305 
1306  if (r != zero && g0 != zero) {
1307  tmp = r;
1308  q = cuddZddDivideF(dd, f0, g0);
1309  if (q == NULL) {
1310  Cudd_RecursiveDerefZdd(dd, f1);
1311  Cudd_RecursiveDerefZdd(dd, f0);
1312  Cudd_RecursiveDerefZdd(dd, g1);
1313  Cudd_RecursiveDerefZdd(dd, g0);
1314  return(NULL);
1315  }
1316  Cudd_Ref(q);
1317  r = cuddZddIntersect(dd, r, q);
1318  if (r == NULL) {
1319  Cudd_RecursiveDerefZdd(dd, f1);
1320  Cudd_RecursiveDerefZdd(dd, f0);
1321  Cudd_RecursiveDerefZdd(dd, g1);
1322  Cudd_RecursiveDerefZdd(dd, g0);
1323  Cudd_RecursiveDerefZdd(dd, q);
1324  return(NULL);
1325  }
1326  Cudd_Ref(r);
1327  Cudd_RecursiveDerefZdd(dd, q);
1328  Cudd_RecursiveDerefZdd(dd, tmp);
1329  }
1330 
1331  Cudd_RecursiveDerefZdd(dd, f1);
1332  Cudd_RecursiveDerefZdd(dd, f0);
1333  Cudd_RecursiveDerefZdd(dd, g1);
1334  Cudd_RecursiveDerefZdd(dd, g0);
1335 
1336  cuddCacheInsert2(dd, cuddZddDivideF, f, g, r);
1337  Cudd_Deref(r);
1338  return(r);
1339 
1340 } /* end of cuddZddDivideF */
1341 
1342 
1355 int
1356 cuddZddGetCofactors3(
1357  DdManager * dd,
1358  DdNode * f,
1359  int v,
1360  DdNode ** f1,
1361  DdNode ** f0,
1362  DdNode ** fd)
1363 {
1364  DdNode *pc, *nc;
1365  DdNode *zero = DD_ZERO(dd);
1366  int top, hv, ht, pv, nv;
1367  int level;
1368 
1369  top = dd->permZ[f->index];
1370  level = dd->permZ[v];
1371  hv = level >> 1;
1372  ht = top >> 1;
1373 
1374  if (hv < ht) {
1375  *f1 = zero;
1376  *f0 = zero;
1377  *fd = f;
1378  }
1379  else {
1380  pv = cuddZddGetPosVarIndex(dd, v);
1381  nv = cuddZddGetNegVarIndex(dd, v);
1382 
1383  /* not to create intermediate ZDD node */
1384  if (cuddZddGetPosVarLevel(dd, v) < cuddZddGetNegVarLevel(dd, v)) {
1385  pc = cuddZddSubset1(dd, f, pv);
1386  if (pc == NULL)
1387  return(1);
1388  Cudd_Ref(pc);
1389  nc = cuddZddSubset0(dd, f, pv);
1390  if (nc == NULL) {
1391  Cudd_RecursiveDerefZdd(dd, pc);
1392  return(1);
1393  }
1394  Cudd_Ref(nc);
1395 
1396  *f1 = cuddZddSubset0(dd, pc, nv);
1397  if (*f1 == NULL) {
1398  Cudd_RecursiveDerefZdd(dd, pc);
1399  Cudd_RecursiveDerefZdd(dd, nc);
1400  return(1);
1401  }
1402  Cudd_Ref(*f1);
1403  *f0 = cuddZddSubset1(dd, nc, nv);
1404  if (*f0 == NULL) {
1405  Cudd_RecursiveDerefZdd(dd, pc);
1406  Cudd_RecursiveDerefZdd(dd, nc);
1407  Cudd_RecursiveDerefZdd(dd, *f1);
1408  return(1);
1409  }
1410  Cudd_Ref(*f0);
1411 
1412  *fd = cuddZddSubset0(dd, nc, nv);
1413  if (*fd == NULL) {
1414  Cudd_RecursiveDerefZdd(dd, pc);
1415  Cudd_RecursiveDerefZdd(dd, nc);
1416  Cudd_RecursiveDerefZdd(dd, *f1);
1417  Cudd_RecursiveDerefZdd(dd, *f0);
1418  return(1);
1419  }
1420  Cudd_Ref(*fd);
1421  } else {
1422  pc = cuddZddSubset1(dd, f, nv);
1423  if (pc == NULL)
1424  return(1);
1425  Cudd_Ref(pc);
1426  nc = cuddZddSubset0(dd, f, nv);
1427  if (nc == NULL) {
1428  Cudd_RecursiveDerefZdd(dd, pc);
1429  return(1);
1430  }
1431  Cudd_Ref(nc);
1432 
1433  *f0 = cuddZddSubset0(dd, pc, pv);
1434  if (*f0 == NULL) {
1435  Cudd_RecursiveDerefZdd(dd, pc);
1436  Cudd_RecursiveDerefZdd(dd, nc);
1437  return(1);
1438  }
1439  Cudd_Ref(*f0);
1440  *f1 = cuddZddSubset1(dd, nc, pv);
1441  if (*f1 == NULL) {
1442  Cudd_RecursiveDerefZdd(dd, pc);
1443  Cudd_RecursiveDerefZdd(dd, nc);
1444  Cudd_RecursiveDerefZdd(dd, *f0);
1445  return(1);
1446  }
1447  Cudd_Ref(*f1);
1448 
1449  *fd = cuddZddSubset0(dd, nc, pv);
1450  if (*fd == NULL) {
1451  Cudd_RecursiveDerefZdd(dd, pc);
1452  Cudd_RecursiveDerefZdd(dd, nc);
1453  Cudd_RecursiveDerefZdd(dd, *f1);
1454  Cudd_RecursiveDerefZdd(dd, *f0);
1455  return(1);
1456  }
1457  Cudd_Ref(*fd);
1458  }
1459 
1460  Cudd_RecursiveDerefZdd(dd, pc);
1461  Cudd_RecursiveDerefZdd(dd, nc);
1462  Cudd_Deref(*f1);
1463  Cudd_Deref(*f0);
1464  Cudd_Deref(*fd);
1465  }
1466  return(0);
1467 
1468 } /* end of cuddZddGetCofactors3 */
1469 
1470 
1482 int
1483 cuddZddGetCofactors2(
1484  DdManager * dd,
1485  DdNode * f,
1486  int v,
1487  DdNode ** f1,
1488  DdNode ** f0)
1489 {
1490  *f1 = cuddZddSubset1(dd, f, v);
1491  if (*f1 == NULL)
1492  return(1);
1493  *f0 = cuddZddSubset0(dd, f, v);
1494  if (*f0 == NULL) {
1495  Cudd_RecursiveDerefZdd(dd, *f1);
1496  return(1);
1497  }
1498  return(0);
1499 
1500 } /* end of cuddZddGetCofactors2 */
1501 
1502 
1517 DdNode *
1518 cuddZddComplement(
1519  DdManager * dd,
1520  DdNode *node)
1521 {
1522  DdNode *b, *isop, *zdd_I;
1523 
1524  /* Check cache */
1525  zdd_I = cuddCacheLookup1Zdd(dd, cuddZddComplement, node);
1526  if (zdd_I)
1527  return(zdd_I);
1528 
1529  b = cuddMakeBddFromZddCover(dd, node);
1530  if (!b)
1531  return(NULL);
1532  cuddRef(b);
1533  isop = cuddZddIsop(dd, Cudd_Not(b), Cudd_Not(b), &zdd_I);
1534  if (!isop) {
1535  Cudd_RecursiveDeref(dd, b);
1536  return(NULL);
1537  }
1538  cuddRef(isop);
1539  cuddRef(zdd_I);
1540  Cudd_RecursiveDeref(dd, b);
1541  Cudd_RecursiveDeref(dd, isop);
1542 
1543  cuddCacheInsert1(dd, cuddZddComplement, node, zdd_I);
1544  cuddDeref(zdd_I);
1545  return(zdd_I);
1546 } /* end of cuddZddComplement */
1547 
1548 
1560 int
1561 cuddZddGetPosVarIndex(
1562  DdManager * dd,
1563  int index)
1564 {
1565  int pv = (index >> 1) << 1;
1566  return(pv);
1567 } /* end of cuddZddGetPosVarIndex */
1568 
1569 
1581 int
1582 cuddZddGetNegVarIndex(
1583  DdManager * dd,
1584  int index)
1585 {
1586  int nv = index | 0x1;
1587  return(nv);
1588 } /* end of cuddZddGetPosVarIndex */
1589 
1590 
1602 int
1603 cuddZddGetPosVarLevel(
1604  DdManager * dd,
1605  int index)
1606 {
1607  int pv = cuddZddGetPosVarIndex(dd, index);
1608  return(dd->permZ[pv]);
1609 } /* end of cuddZddGetPosVarLevel */
1610 
1611 
1623 int
1624 cuddZddGetNegVarLevel(
1625  DdManager * dd,
1626  int index)
1627 {
1628  int nv = cuddZddGetNegVarIndex(dd, index);
1629  return(dd->permZ[nv]);
1630 } /* end of cuddZddGetNegVarLevel */
cuddRef
#define cuddRef(n)
Definition: cuddInt.h:557
Cudd_RecursiveDerefZdd
void Cudd_RecursiveDerefZdd(DdManager *table, DdNode *n)
Definition: cuddRef.c:381
cuddCacheLookup1Zdd
DdNode * cuddCacheLookup1Zdd(DdManager *table, DdNode *(*)(DdManager *, DdNode *), DdNode *f)
cuddDeref
#define cuddDeref(n)
Definition: cuddInt.h:577
Cudd_zddComplement
DdNode * Cudd_zddComplement(DdManager *dd, DdNode *node)
Definition: cuddZddFuncs.c:328
Cudd_RecursiveDeref
void Cudd_RecursiveDeref(DdManager *table, DdNode *n)
Definition: cuddRef.c:150
cuddZddDivide
DdNode * cuddZddDivide(DdManager *dd, DdNode *f, DdNode *g)
Definition: cuddZddFuncs.c:1155
DdNode
Definition: cudd.h:270
cuddZddGetNode
DdNode * cuddZddGetNode(DdManager *zdd, int id, DdNode *T, DdNode *E)
Definition: cuddTable.c:1050
Cudd_Not
#define Cudd_Not(node)
Definition: cudd.h:354
Cudd_zddProduct
DdNode * Cudd_zddProduct(DdManager *dd, DdNode *f, DdNode *g)
Definition: cuddZddFuncs.c:141
Cudd_Deref
void Cudd_Deref(DdNode *node)
Definition: cuddRef.c:434
cuddZddGetCofactors2
int cuddZddGetCofactors2(DdManager *dd, DdNode *f, int v, DdNode **f1, DdNode **f0)
Definition: cuddZddFuncs.c:1483
cuddCacheInsert1
void cuddCacheInsert1(DdManager *table, DdNode *(*)(DdManager *, DdNode *), DdNode *f, DdNode *data)
Cudd_zddWeakDiv
DdNode * Cudd_zddWeakDiv(DdManager *dd, DdNode *f, DdNode *g)
Definition: cuddZddFuncs.c:206
DdManager::permZ
int * permZ
Definition: cuddInt.h:370
cuddZddGetCofactors3
int cuddZddGetCofactors3(DdManager *dd, DdNode *f, int v, DdNode **f1, DdNode **f0, DdNode **fd)
Definition: cuddZddFuncs.c:1356
cuddZddGetPosVarLevel
int cuddZddGetPosVarLevel(DdManager *dd, int index)
Definition: cuddZddFuncs.c:1603
Cudd_MakeBddFromZddCover
DdNode * Cudd_MakeBddFromZddCover(DdManager *dd, DdNode *node)
Definition: cuddZddIsop.c:200
statLine
#define statLine(dd)
Definition: cuddInt.h:990
cuddZddUnateProduct
DdNode * cuddZddUnateProduct(DdManager *dd, DdNode *f, DdNode *g)
Definition: cuddZddFuncs.c:613
DD_UNUSED
static char rcsid [] DD_UNUSED
Definition: cuddZddFuncs.c:101
cuddZddProduct
DdNode * cuddZddProduct(DdManager *dd, DdNode *f, DdNode *g)
Definition: cuddZddFuncs.c:376
DdManager::reordered
int reordered
Definition: cuddInt.h:392
one
static DdNode * one
Definition: cuddSat.c:105
cuddZddGetNegVarIndex
int cuddZddGetNegVarIndex(DdManager *dd, int index)
Definition: cuddZddFuncs.c:1582
cuddZddIntersect
DdNode * cuddZddIntersect(DdManager *zdd, DdNode *P, DdNode *Q)
Definition: cuddZddSetop.c:638
cuddZddWeakDiv
DdNode * cuddZddWeakDiv(DdManager *dd, DdNode *f, DdNode *g)
Definition: cuddZddFuncs.c:757
cuddZddIsop
DdNode * cuddZddIsop(DdManager *dd, DdNode *L, DdNode *U, DdNode **zdd_I)
Definition: cuddZddIsop.c:231
cuddMakeBddFromZddCover
DdNode * cuddMakeBddFromZddCover(DdManager *dd, DdNode *node)
Definition: cuddZddIsop.c:797
Cudd_zddIsop
DdNode * Cudd_zddIsop(DdManager *dd, DdNode *L, DdNode *U, DdNode **zdd_I)
Definition: cuddZddIsop.c:132
Cudd_zddDivideF
DdNode * Cudd_zddDivideF(DdManager *dd, DdNode *f, DdNode *g)
Definition: cuddZddFuncs.c:295
ddMin
#define ddMin(x, y)
Definition: cuddInt.h:771
cuddZddGetPosVarIndex
int cuddZddGetPosVarIndex(DdManager *dd, int index)
Definition: cuddZddFuncs.c:1561
cuddZddWeakDivF
DdNode * cuddZddWeakDivF(DdManager *dd, DdNode *f, DdNode *g)
Definition: cuddZddFuncs.c:918
Cudd_zddWeakDivF
DdNode * Cudd_zddWeakDivF(DdManager *dd, DdNode *f, DdNode *g)
Definition: cuddZddFuncs.c:266
Cudd_zddDivide
DdNode * Cudd_zddDivide(DdManager *dd, DdNode *f, DdNode *g)
Definition: cuddZddFuncs.c:237
cuddCacheLookup2Zdd
DdNode * cuddCacheLookup2Zdd(DdManager *table, DdNode *(*)(DdManager *, DdNode *, DdNode *), DdNode *f, DdNode *g)
cuddZddSubset1
DdNode * cuddZddSubset1(DdManager *dd, DdNode *P, int var)
Definition: cuddZddSetop.c:870
cuddZddUnion
DdNode * cuddZddUnion(DdManager *zdd, DdNode *P, DdNode *Q)
Definition: cuddZddSetop.c:549
cuddZddGetNegVarLevel
int cuddZddGetNegVarLevel(DdManager *dd, int index)
Definition: cuddZddFuncs.c:1624
cuddCacheInsert2
void cuddCacheInsert2(DdManager *table, DdNode *(*)(DdManager *, DdNode *, DdNode *), DdNode *f, DdNode *g, DdNode *data)
DdNode::index
DdHalfWord index
Definition: cudd.h:271
zero
static DdNode * zero
Definition: cuddSat.c:105
Cudd_zddUnateProduct
DdNode * Cudd_zddUnateProduct(DdManager *dd, DdNode *f, DdNode *g)
Definition: cuddZddFuncs.c:172
cuddZddSubset0
DdNode * cuddZddSubset0(DdManager *dd, DdNode *P, int var)
Definition: cuddZddSetop.c:919
Cudd_Ref
void Cudd_Ref(DdNode *n)
Definition: cuddRef.c:125
DD_ONE
#define DD_ONE(dd)
Definition: cuddInt.h:864
cuddZddDivideF
DdNode * cuddZddDivideF(DdManager *dd, DdNode *f, DdNode *g)
Definition: cuddZddFuncs.c:1255
cuddZddComplement
DdNode * cuddZddComplement(DdManager *dd, DdNode *node)
Definition: cuddZddFuncs.c:1518
DD_ZERO
#define DD_ZERO(dd)
Definition: cuddInt.h:880
Generated by   doxygen 1.8.13