ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
extraBddMaxMin.c
Go to the documentation of this file.
1
49
50#include "extraBdd.h"
51
52ABC_NAMESPACE_IMPL_START
53
54/*---------------------------------------------------------------------------*/
55/* Constant declarations */
56/*---------------------------------------------------------------------------*/
57
58/*---------------------------------------------------------------------------*/
59/* Stucture declarations */
60/*---------------------------------------------------------------------------*/
61
62/*---------------------------------------------------------------------------*/
63/* Type declarations */
64/*---------------------------------------------------------------------------*/
65
66/*---------------------------------------------------------------------------*/
67/* Variable declarations */
68/*---------------------------------------------------------------------------*/
69
70/*---------------------------------------------------------------------------*/
71/* Macro declarations */
72/*---------------------------------------------------------------------------*/
73
74
76
77/*---------------------------------------------------------------------------*/
78/* StaTc Function prototypes */
79/*---------------------------------------------------------------------------*/
80
82
83
84/*---------------------------------------------------------------------------*/
85/* Definition of exported Functions */
86/*---------------------------------------------------------------------------*/
87
88
100DdNode *
101Extra_zddMaximal(
102 DdManager * dd,
103 DdNode * S)
104{
105 DdNode *res;
106 do {
107 dd->reordered = 0;
108 res = extraZddMaximal(dd, S);
109 } while (dd->reordered == 1);
110 return(res);
111
112} /* end of Extra_zddMaximal */
113
114
126DdNode *
127Extra_zddMinimal(
128 DdManager * dd,
129 DdNode * S)
130{
131 DdNode *res;
132 do {
133 dd->reordered = 0;
134 res = extraZddMinimal(dd, S);
135 } while (dd->reordered == 1);
136 return(res);
137
138} /* end of Extra_zddMinimal */
139
140
152DdNode *
153Extra_zddMaxUnion(
154 DdManager * dd,
155 DdNode * S,
156 DdNode * T)
157{
158 DdNode *res;
159 do {
160 dd->reordered = 0;
161 res = extraZddMaxUnion(dd, S, T);
162 } while (dd->reordered == 1);
163 return(res);
164
165} /* end of Extra_zddMaxUnion */
166
167
179DdNode *
180Extra_zddMinUnion(
181 DdManager * dd,
182 DdNode * S,
183 DdNode * T)
184{
185 DdNode *res;
186 do {
187 dd->reordered = 0;
188 res = extraZddMinUnion(dd, S, T);
189 } while (dd->reordered == 1);
190 return(res);
191
192} /* end of Extra_zddMinUnion */
193
194
207DdNode *
208Extra_zddDotProduct(
209 DdManager * dd,
210 DdNode * S,
211 DdNode * T)
212{
213 DdNode *res;
214 do {
215 dd->reordered = 0;
216 res = extraZddDotProduct(dd, S, T);
217 } while (dd->reordered == 1);
218 return(res);
219
220} /* end of Extra_zddDotProduct */
221
222
235DdNode *
236Extra_zddCrossProduct(
237 DdManager * dd,
238 DdNode * S,
239 DdNode * T)
240{
241 DdNode *res;
242 do {
243 dd->reordered = 0;
244 res = extraZddCrossProduct(dd, S, T);
245 } while (dd->reordered == 1);
246 return(res);
247
248} /* end of Extra_zddCrossProduct */
249
250
262DdNode *
263Extra_zddMaxDotProduct(
264 DdManager * dd,
265 DdNode * S,
266 DdNode * T)
267{
268 DdNode *res;
269 do {
270 dd->reordered = 0;
271 res = extraZddMaxDotProduct(dd, S, T);
272 } while (dd->reordered == 1);
273 return(res);
274
275} /* end of Extra_zddMaxDotProduct */
276
277
278/*---------------------------------------------------------------------------*/
279/* Definition of internal Functions */
280/*---------------------------------------------------------------------------*/
281
293DdNode *
294extraZddMaximal(
295 DdManager * dd,
296 DdNode * zSet)
297{
298 DdNode *zRes;
299 statLine(dd);
300
301 /* consider terminal cases */
302 if ( zSet == z0 || zSet == z1 )
303 return zSet;
304
305 /* check cache */
306 zRes = cuddCacheLookup1Zdd(dd, extraZddMaximal, zSet);
307 if (zRes)
308 return(zRes);
309 else
310 {
311 DdNode *zSet0, *zSet1, *zRes0, *zRes1;
312
313 /* compute maximal for subsets without the top-most element */
314 zSet0 = extraZddMaximal(dd, cuddE(zSet));
315 if ( zSet0 == NULL )
316 return NULL;
317 cuddRef( zSet0 );
318
319 /* compute maximal for subsets with the top-most element */
320 zSet1 = extraZddMaximal(dd, cuddT(zSet));
321 if ( zSet1 == NULL )
322 {
323 Cudd_RecursiveDerefZdd(dd, zSet0);
324 return NULL;
325 }
326 cuddRef( zSet1 );
327
328 /* remove subsets without this element covered by subsets with this element */
329 zRes0 = extraZddNotSubSet(dd, zSet0, zSet1);
330 if ( zRes0 == NULL )
331 {
332 Cudd_RecursiveDerefZdd(dd, zSet0);
333 Cudd_RecursiveDerefZdd(dd, zSet1);
334 return NULL;
335 }
336 cuddRef( zRes0 );
337 Cudd_RecursiveDerefZdd(dd, zSet0);
338
339 /* subset with this element remains unchanged */
340 zRes1 = zSet1;
341
342 /* create the new node */
343 zRes = cuddZddGetNode( dd, zSet->index, zRes1, zRes0 );
344 if ( zRes == NULL )
345 {
346 Cudd_RecursiveDerefZdd( dd, zRes0 );
347 Cudd_RecursiveDerefZdd( dd, zRes1 );
348 return NULL;
349 }
350 cuddDeref( zRes0 );
351 cuddDeref( zRes1 );
352
353 /* insert the result into cache */
354 cuddCacheInsert1(dd, extraZddMaximal, zSet, zRes);
355 return zRes;
356 }
357} /* end of extraZddMaximal */
358
359
360
372DdNode *
373extraZddMinimal(
374 DdManager * dd,
375 DdNode * zSet)
376{
377 DdNode *zRes;
378 statLine(dd);
379
380 /* consider terminal cases */
381 if ( zSet == z0 )
382 return zSet;
383 /* the empty combinaTon, if present, is the only minimal combinaTon */
384 if ( Extra_zddEmptyBelongs(dd, zSet) )
385 return z1;
386
387 /* check cache */
388 zRes = cuddCacheLookup1Zdd(dd, extraZddMinimal, zSet);
389 if (zRes)
390 return(zRes);
391 else
392 {
393 DdNode *zSet0, *zSet1, *zRes0, *zRes1;
394
395 /* compute minimal for subsets without the top-most element */
396 zSet0 = extraZddMinimal(dd, cuddE(zSet));
397 if ( zSet0 == NULL )
398 return NULL;
399 cuddRef( zSet0 );
400
401 /* compute minimal for subsets with the top-most element */
402 zSet1 = extraZddMinimal(dd, cuddT(zSet));
403 if ( zSet1 == NULL )
404 {
405 Cudd_RecursiveDerefZdd(dd, zSet0);
406 return NULL;
407 }
408 cuddRef( zSet1 );
409
410 /* subset without this element remains unchanged */
411 zRes0 = zSet0;
412
413 /* remove subsets with this element that contain subsets without this element */
414 zRes1 = extraZddNotSupSet(dd, zSet1, zSet0);
415 if ( zRes1 == NULL )
416 {
417 Cudd_RecursiveDerefZdd(dd, zSet0);
418 Cudd_RecursiveDerefZdd(dd, zSet1);
419 return NULL;
420 }
421 cuddRef( zRes1 );
422 Cudd_RecursiveDerefZdd(dd, zSet1);
423
424 /* create the new node */
425 zRes = cuddZddGetNode( dd, zSet->index, zRes1, zRes0 );
426 if ( zRes == NULL )
427 {
428 Cudd_RecursiveDerefZdd( dd, zRes0 );
429 Cudd_RecursiveDerefZdd( dd, zRes1 );
430 return NULL;
431 }
432 cuddDeref( zRes0 );
433 cuddDeref( zRes1 );
434
435 /* insert the result into cache */
436 cuddCacheInsert1(dd, extraZddMinimal, zSet, zRes);
437 return zRes;
438 }
439} /* end of extraZddMinimal */
440
441
453DdNode *
454extraZddMaxUnion(
455 DdManager * dd,
456 DdNode * S,
457 DdNode * T)
458{
459 DdNode *zRes;
460 int TopS, TopT;
461 statLine(dd);
462
463 /* consider terminal cases */
464 if ( S == z0 )
465 return T;
466 if ( T == z0 )
467 return S;
468 if ( S == T )
469 return S;
470 if ( S == z1 )
471 return T;
472 if ( T == z1 )
473 return S;
474
475 /* the operation is commutative - normalize the problem */
476 TopS = dd->permZ[S->index];
477 TopT = dd->permZ[T->index];
478
479 if ( TopS > TopT || (TopS == TopT && S > T) )
480 return extraZddMaxUnion(dd, T, S);
481
482 /* check cache */
483 zRes = cuddCacheLookup2Zdd(dd, extraZddMaxUnion, S, T);
484 if (zRes)
485 return zRes;
486 else
487 {
488 DdNode *zSet0, *zSet1, *zRes0, *zRes1;
489
490 if ( TopS == TopT )
491 {
492 /* compute maximal for subsets without the top-most element */
493 zSet0 = extraZddMaxUnion(dd, cuddE(S), cuddE(T) );
494 if ( zSet0 == NULL )
495 return NULL;
496 cuddRef( zSet0 );
497
498 /* compute maximal for subsets with the top-most element */
499 zSet1 = extraZddMaxUnion(dd, cuddT(S), cuddT(T) );
500 if ( zSet1 == NULL )
501 {
502 Cudd_RecursiveDerefZdd(dd, zSet0);
503 return NULL;
504 }
505 cuddRef( zSet1 );
506 }
507 else /* if ( TopS < TopT ) */
508 {
509 /* compute maximal for subsets without the top-most element */
510 zSet0 = extraZddMaxUnion(dd, cuddE(S), T );
511 if ( zSet0 == NULL )
512 return NULL;
513 cuddRef( zSet0 );
514
515 /* subset with this element is just the cofactor of S */
516 zSet1 = cuddT(S);
517 cuddRef( zSet1 );
518 }
519
520 /* remove subsets without this element covered by subsets with this element */
521 zRes0 = extraZddNotSubSet(dd, zSet0, zSet1);
522 if ( zRes0 == NULL )
523 {
524 Cudd_RecursiveDerefZdd(dd, zSet0);
525 Cudd_RecursiveDerefZdd(dd, zSet1);
526 return NULL;
527 }
528 cuddRef( zRes0 );
529 Cudd_RecursiveDerefZdd(dd, zSet0);
530
531 /* subset with this element remains unchanged */
532 zRes1 = zSet1;
533
534 /* create the new node */
535 zRes = cuddZddGetNode( dd, S->index, zRes1, zRes0 );
536 if ( zRes == NULL )
537 {
538 Cudd_RecursiveDerefZdd( dd, zRes0 );
539 Cudd_RecursiveDerefZdd( dd, zRes1 );
540 return NULL;
541 }
542 cuddDeref( zRes0 );
543 cuddDeref( zRes1 );
544
545 /* insert the result into cache */
546 cuddCacheInsert2(dd, extraZddMaxUnion, S, T, zRes);
547 return zRes;
548 }
549} /* end of extraZddMaxUnion */
550
551
563DdNode *
564extraZddMinUnion(
565 DdManager * dd,
566 DdNode * S,
567 DdNode * T)
568{
569 DdNode *zRes;
570 int TopS, TopT;
571 statLine(dd);
572
573 /* consider terminal cases */
574 if ( S == z0 )
575 return T;
576 if ( T == z0 )
577 return S;
578 if ( S == T )
579 return S;
580 /* the empty combination, if present, is the only minimal combination */
581 if ( Extra_zddEmptyBelongs(dd, S) || Extra_zddEmptyBelongs(dd, T) )
582 return z1;
583
584 /* the operation is commutative - normalize the problem */
585 TopS = dd->permZ[S->index];
586 TopT = dd->permZ[T->index];
587
588 if ( TopS > TopT || (TopS == TopT && S > T) )
589 return extraZddMinUnion(dd, T, S);
590
591 /* check cache */
592 zRes = cuddCacheLookup2Zdd(dd, extraZddMinUnion, S, T);
593 if (zRes)
594 return(zRes);
595 else
596 {
597 DdNode *zSet0, *zSet1, *zRes0, *zRes1;
598 if ( TopS == TopT )
599 {
600 /* compute maximal for subsets without the top-most element */
601 zSet0 = extraZddMinUnion(dd, cuddE(S), cuddE(T) );
602 if ( zSet0 == NULL )
603 return NULL;
604 cuddRef( zSet0 );
605
606 /* compute maximal for subsets with the top-most element */
607 zSet1 = extraZddMinUnion(dd, cuddT(S), cuddT(T) );
608 if ( zSet1 == NULL )
609 {
610 Cudd_RecursiveDerefZdd(dd, zSet0);
611 return NULL;
612 }
613 cuddRef( zSet1 );
614 }
615 else /* if ( TopS < TopT ) */
616 {
617 /* compute maximal for subsets without the top-most element */
618 zSet0 = extraZddMinUnion(dd, cuddE(S), T );
619 if ( zSet0 == NULL )
620 return NULL;
621 cuddRef( zSet0 );
622
623 /* subset with this element is just the cofactor of S */
624 zSet1 = cuddT(S);
625 cuddRef( zSet1 );
626 }
627
628 /* subset without this element remains unchanged */
629 zRes0 = zSet0;
630
631 /* remove subsets with this element that contain subsets without this element */
632 zRes1 = extraZddNotSupSet(dd, zSet1, zSet0);
633 if ( zRes1 == NULL )
634 {
635 Cudd_RecursiveDerefZdd(dd, zSet0);
636 Cudd_RecursiveDerefZdd(dd, zSet1);
637 return NULL;
638 }
639 cuddRef( zRes1 );
640 Cudd_RecursiveDerefZdd(dd, zSet1);
641
642 /* create the new node */
643 zRes = cuddZddGetNode( dd, S->index, zRes1, zRes0 );
644 if ( zRes == NULL )
645 {
646 Cudd_RecursiveDerefZdd( dd, zRes0 );
647 Cudd_RecursiveDerefZdd( dd, zRes1 );
648 return NULL;
649 }
650 cuddDeref( zRes0 );
651 cuddDeref( zRes1 );
652
653 /* insert the result into cache */
654 cuddCacheInsert2(dd, extraZddMinUnion, S, T, zRes);
655 return zRes;
656 }
657} /* end of extraZddMinUnion */
658
659
671DdNode *
672extraZddDotProduct(
673 DdManager * dd,
674 DdNode * S,
675 DdNode * T)
676{
677 DdNode *zRes;
678 int TopS, TopT;
679 statLine(dd);
680
681 /* consider terminal cases */
682 if ( S == z0 || T == z0 )
683 return z0;
684 if ( S == z1 )
685 return T;
686 if ( T == z1 )
687 return S;
688
689 /* the operation is commutative - normalize the problem */
690 TopS = dd->permZ[S->index];
691 TopT = dd->permZ[T->index];
692
693 if ( TopS > TopT || (TopS == TopT && S > T) )
694 return extraZddDotProduct(dd, T, S);
695
696 /* check cache */
697 zRes = cuddCacheLookup2Zdd(dd, extraZddDotProduct, S, T);
698 if (zRes)
699 return zRes;
700 else
701 {
702 DdNode *zSet0, *zSet1, *zRes0, *zRes1, *zTemp;
703 if ( TopS == TopT )
704 {
705 /* compute the union of two cofactors of T (T0+T1) */
706 zTemp = cuddZddUnion(dd, cuddE(T), cuddT(T) );
707 if ( zTemp == NULL )
708 return NULL;
709 cuddRef( zTemp );
710
711 /* compute DotProduct with the top element for subsets (S1, T0+T1) */
712 zSet0 = extraZddDotProduct(dd, cuddT(S), zTemp );
713 if ( zSet0 == NULL )
714 {
715 Cudd_RecursiveDerefZdd(dd, zTemp);
716 return NULL;
717 }
718 cuddRef( zSet0 );
719 Cudd_RecursiveDerefZdd(dd, zTemp);
720
721 /* compute DotProduct with the top element for subsets (S0, T1) */
722 zSet1 = extraZddDotProduct(dd, cuddE(S), cuddT(T) );
723 if ( zSet1 == NULL )
724 {
725 Cudd_RecursiveDerefZdd(dd, zSet0);
726 return NULL;
727 }
728 cuddRef( zSet1 );
729
730 /* compute the union of these two partial results (zSet0 + zSet1) */
731 zRes1 = cuddZddUnion(dd, zSet0, zSet1 );
732 if ( zRes1 == NULL )
733 {
734 Cudd_RecursiveDerefZdd(dd, zSet0);
735 Cudd_RecursiveDerefZdd(dd, zSet1);
736 return NULL;
737 }
738 cuddRef( zRes1 );
739 Cudd_RecursiveDerefZdd(dd, zSet0);
740 Cudd_RecursiveDerefZdd(dd, zSet1);
741
742 /* compute DotProduct for subsets without the top-most element */
743 zRes0 = extraZddDotProduct(dd, cuddE(S), cuddE(T) );
744 if ( zRes0 == NULL )
745 {
746 Cudd_RecursiveDerefZdd(dd, zRes1);
747 return NULL;
748 }
749 cuddRef( zRes0 );
750 }
751 else /* if ( TopS < TopT ) */
752 {
753 /* compute DotProduct with the top element for subsets (S1, T) */
754 zRes1 = extraZddDotProduct(dd, cuddT(S), T );
755 if ( zRes1 == NULL )
756 return NULL;
757 cuddRef( zRes1 );
758
759 /* compute DotProduct for subsets without the top-most element */
760 zRes0 = extraZddDotProduct(dd, cuddE(S), T );
761 if ( zRes0 == NULL )
762 {
763 Cudd_RecursiveDerefZdd(dd, zRes1);
764 return NULL;
765 }
766 cuddRef( zRes0 );
767 }
768
769 /* create the new node */
770 zRes = cuddZddGetNode( dd, S->index, zRes1, zRes0 );
771 if ( zRes == NULL )
772 {
773 Cudd_RecursiveDerefZdd( dd, zRes0 );
774 Cudd_RecursiveDerefZdd( dd, zRes1 );
775 return NULL;
776 }
777 cuddDeref( zRes0 );
778 cuddDeref( zRes1 );
779
780 /* insert the result into cache */
781 cuddCacheInsert2(dd, extraZddDotProduct, S, T, zRes);
782 return zRes;
783 }
784} /* end of extraZddDotProduct */
785
786
798DdNode *
799extraZddCrossProduct(
800 DdManager * dd,
801 DdNode * S,
802 DdNode * T)
803{
804 DdNode *zRes;
805 int TopS, TopT;
806 statLine(dd);
807
808 /* consider terminal cases */
809 if ( S == z0 || T == z0 )
810 return z0;
811 if ( S == z1 || T == z1 )
812 return z1;
813
814 /* the operation is commutative - normalize the problem */
815 TopS = dd->permZ[S->index];
816 TopT = dd->permZ[T->index];
817
818 if ( TopS > TopT || (TopS == TopT && S > T) )
819 return extraZddCrossProduct(dd, T, S);
820
821 /* check cache */
822 zRes = cuddCacheLookup2Zdd(dd, extraZddCrossProduct, S, T);
823 if (zRes)
824 return zRes;
825 else
826 {
827 DdNode *zSet0, *zSet1, *zRes0, *zRes1, *zTemp;
828
829 if ( TopS == TopT )
830 {
831 /* compute the union of two cofactors of T (T0+T1) */
832 zTemp = cuddZddUnion(dd, cuddE(T), cuddT(T) );
833 if ( zTemp == NULL )
834 return NULL;
835 cuddRef( zTemp );
836
837 /* compute CrossProduct without the top element for subsets (S0, T0+T1) */
838 zSet0 = extraZddCrossProduct(dd, cuddE(S), zTemp );
839 if ( zSet0 == NULL )
840 {
841 Cudd_RecursiveDerefZdd(dd, zTemp);
842 return NULL;
843 }
844 cuddRef( zSet0 );
845 Cudd_RecursiveDerefZdd(dd, zTemp);
846
847 /* compute CrossProduct without the top element for subsets (S1, T0) */
848 zSet1 = extraZddCrossProduct(dd, cuddT(S), cuddE(T) );
849 if ( zSet1 == NULL )
850 {
851 Cudd_RecursiveDerefZdd(dd, zSet0);
852 return NULL;
853 }
854 cuddRef( zSet1 );
855
856 /* compute the union of these two partial results (zSet0 + zSet1) */
857 zRes0 = cuddZddUnion(dd, zSet0, zSet1 );
858 if ( zRes0 == NULL )
859 {
860 Cudd_RecursiveDerefZdd(dd, zSet0);
861 Cudd_RecursiveDerefZdd(dd, zSet1);
862 return NULL;
863 }
864 cuddRef( zRes0 );
865 Cudd_RecursiveDerefZdd(dd, zSet0);
866 Cudd_RecursiveDerefZdd(dd, zSet1);
867
868 /* compute CrossProduct for subsets with the top-most element */
869 zRes1 = extraZddCrossProduct(dd, cuddT(S), cuddT(T) );
870 if ( zRes1 == NULL )
871 {
872 Cudd_RecursiveDerefZdd(dd, zRes0);
873 return NULL;
874 }
875 cuddRef( zRes1 );
876
877 /* create the new node */
878 zRes = cuddZddGetNode( dd, S->index, zRes1, zRes0 );
879 if ( zRes == NULL )
880 {
881 Cudd_RecursiveDerefZdd( dd, zRes0 );
882 Cudd_RecursiveDerefZdd( dd, zRes1 );
883 return NULL;
884 }
885 cuddDeref( zRes0 );
886 cuddDeref( zRes1 );
887 }
888 else /* if ( TopS < TopT ) */
889 {
890 /* compute CrossProduct without the top element (S0, T) */
891 zSet0 = extraZddCrossProduct(dd, cuddE(S), T );
892 if ( zSet0 == NULL )
893 return NULL;
894 cuddRef( zSet0 );
895
896 /* compute CrossProduct without the top element (S1, T) */
897 zSet1 = extraZddCrossProduct(dd, cuddT(S), T );
898 if ( zSet1 == NULL )
899 {
900 Cudd_RecursiveDerefZdd(dd, zSet0);
901 return NULL;
902 }
903 cuddRef( zSet1 );
904
905 /* compute the union of these two partial results (zSet0 + zSet1) */
906 zRes = cuddZddUnion(dd, zSet0, zSet1 );
907 if ( zRes == NULL )
908 {
909 Cudd_RecursiveDerefZdd(dd, zSet0);
910 Cudd_RecursiveDerefZdd(dd, zSet1);
911 return NULL;
912 }
913 cuddRef( zRes );
914 Cudd_RecursiveDerefZdd(dd, zSet0);
915 Cudd_RecursiveDerefZdd(dd, zSet1);
916 cuddDeref( zRes );
917 }
918
919 /* insert the result into cache */
920 cuddCacheInsert2(dd, extraZddCrossProduct, S, T, zRes);
921 return zRes;
922 }
923} /* end of extraZddCrossProduct */
924
925
937DdNode *
938extraZddMaxDotProduct(
939 DdManager * dd,
940 DdNode * S,
941 DdNode * T)
942{
943 DdNode *zRes;
944 int TopS, TopT;
945 statLine(dd);
946
947 /* consider terminal cases */
948 if ( S == z0 || T == z0 )
949 return z0;
950 if ( S == z1 )
951 return T;
952 if ( T == z1 )
953 return S;
954
955 /* the operation is commutative - normalize the problem */
956 TopS = dd->permZ[S->index];
957 TopT = dd->permZ[T->index];
958
959 if ( TopS > TopT || (TopS == TopT && S > T) )
960 return extraZddMaxDotProduct(dd, T, S);
961
962 /* check cache */
963 zRes = cuddCacheLookup2Zdd(dd, extraZddMaxDotProduct, S, T);
964 if (zRes)
965 return zRes;
966 else
967 {
968 DdNode *zSet0, *zSet1, *zRes0, *zRes1, *zTemp;
969 if ( TopS == TopT )
970 {
971 /* compute the union of two cofactors of T (T0+T1) */
972 zTemp = extraZddMaxUnion(dd, cuddE(T), cuddT(T) );
973 if ( zTemp == NULL )
974 return NULL;
975 cuddRef( zTemp );
976
977 /* compute MaxDotProduct with the top element for subsets (S1, T0+T1) */
978 zSet0 = extraZddMaxDotProduct(dd, cuddT(S), zTemp );
979 if ( zSet0 == NULL )
980 {
981 Cudd_RecursiveDerefZdd(dd, zTemp);
982 return NULL;
983 }
984 cuddRef( zSet0 );
985 Cudd_RecursiveDerefZdd(dd, zTemp);
986
987 /* compute MaxDotProduct with the top element for subsets (S0, T1) */
988 zSet1 = extraZddMaxDotProduct(dd, cuddE(S), cuddT(T) );
989 if ( zSet1 == NULL )
990 {
991 Cudd_RecursiveDerefZdd(dd, zSet0);
992 return NULL;
993 }
994 cuddRef( zSet1 );
995
996 /* compute the union of these two partial results (zSet0 + zSet1) */
997 zRes1 = extraZddMaxUnion(dd, zSet0, zSet1 );
998 if ( zRes1 == NULL )
999 {
1000 Cudd_RecursiveDerefZdd(dd, zSet0);
1001 Cudd_RecursiveDerefZdd(dd, zSet1);
1002 return NULL;
1003 }
1004 cuddRef( zRes1 );
1005 Cudd_RecursiveDerefZdd(dd, zSet0);
1006 Cudd_RecursiveDerefZdd(dd, zSet1);
1007
1008 /* compute MaxDotProduct for subsets without the top-most element */
1009 zRes0 = extraZddMaxDotProduct(dd, cuddE(S), cuddE(T) );
1010 if ( zRes0 == NULL )
1011 {
1012 Cudd_RecursiveDerefZdd(dd, zRes1);
1013 return NULL;
1014 }
1015 cuddRef( zRes0 );
1016 }
1017 else /* if ( TopS < TopT ) */
1018 {
1019 /* compute MaxDotProduct with the top element for subsets (S1, T) */
1020 zRes1 = extraZddMaxDotProduct(dd, cuddT(S), T );
1021 if ( zRes1 == NULL )
1022 return NULL;
1023 cuddRef( zRes1 );
1024
1025 /* compute MaxDotProduct for subsets without the top-most element */
1026 zRes0 = extraZddMaxDotProduct(dd, cuddE(S), T );
1027 if ( zRes0 == NULL )
1028 {
1029 Cudd_RecursiveDerefZdd(dd, zRes1);
1030 return NULL;
1031 }
1032 cuddRef( zRes0 );
1033 }
1034
1035 /* remove subsets without this element covered by subsets with this element */
1036 zRes0 = extraZddNotSubSet(dd, zTemp = zRes0, zRes1);
1037 if ( zRes0 == NULL )
1038 {
1039 Cudd_RecursiveDerefZdd(dd, zTemp);
1040 Cudd_RecursiveDerefZdd(dd, zRes1);
1041 return NULL;
1042 }
1043 cuddRef( zRes0 );
1044 Cudd_RecursiveDerefZdd(dd, zTemp);
1045
1046 /* create the new node */
1047 zRes = cuddZddGetNode( dd, S->index, zRes1, zRes0 );
1048 if ( zRes == NULL )
1049 {
1050 Cudd_RecursiveDerefZdd( dd, zRes0 );
1051 Cudd_RecursiveDerefZdd( dd, zRes1 );
1052 return NULL;
1053 }
1054 cuddDeref( zRes0 );
1055 cuddDeref( zRes1 );
1056
1057 /* insert the result into cache */
1058 cuddCacheInsert2(dd, extraZddMaxDotProduct, S, T, zRes);
1059 return zRes;
1060 }
1061} /* end of extraZddMaxDotProduct */
1062
1063/*---------------------------------------------------------------------------*/
1064/* Definition of staTc Functions */
1065/*---------------------------------------------------------------------------*/
1066
1067ABC_NAMESPACE_IMPL_END
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition abc_namespaces.h:54
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition abc_namespaces.h:55
extraZddMaxDotProduct
DdNode * extraZddMaxDotProduct(DdManager *dd, DdNode *S, DdNode *T)
Definition extraBddMaxMin.c:938
Extra_zddMaximal
ABC_NAMESPACE_IMPL_START DdNode * Extra_zddMaximal(DdManager *dd, DdNode *S)
Definition extraBddMaxMin.c:101
Extra_zddDotProduct
DdNode * Extra_zddDotProduct(DdManager *dd, DdNode *S, DdNode *T)
Definition extraBddMaxMin.c:208
extraZddDotProduct
DdNode * extraZddDotProduct(DdManager *dd, DdNode *S, DdNode *T)
Definition extraBddMaxMin.c:672
Extra_zddMinimal
DdNode * Extra_zddMinimal(DdManager *dd, DdNode *S)
Definition extraBddMaxMin.c:127
Extra_zddMaxUnion
DdNode * Extra_zddMaxUnion(DdManager *dd, DdNode *S, DdNode *T)
Definition extraBddMaxMin.c:153
extraZddMaximal
DdNode * extraZddMaximal(DdManager *dd, DdNode *zSet)
Definition extraBddMaxMin.c:294
extraZddMinimal
DdNode * extraZddMinimal(DdManager *dd, DdNode *zSet)
Definition extraBddMaxMin.c:373
extraZddCrossProduct
DdNode * extraZddCrossProduct(DdManager *dd, DdNode *S, DdNode *T)
Definition extraBddMaxMin.c:799
extraZddMinUnion
DdNode * extraZddMinUnion(DdManager *dd, DdNode *S, DdNode *T)
Definition extraBddMaxMin.c:564
Extra_zddMinUnion
DdNode * Extra_zddMinUnion(DdManager *dd, DdNode *S, DdNode *T)
Definition extraBddMaxMin.c:180
extraZddMaxUnion
DdNode * extraZddMaxUnion(DdManager *dd, DdNode *S, DdNode *T)
Definition extraBddMaxMin.c:454
Extra_zddMaxDotProduct
DdNode * Extra_zddMaxDotProduct(DdManager *dd, DdNode *S, DdNode *T)
Definition extraBddMaxMin.c:263
Extra_zddCrossProduct
DdNode * Extra_zddCrossProduct(DdManager *dd, DdNode *S, DdNode *T)
Definition extraBddMaxMin.c:236
extraZddMaximal
DdNode * extraZddMaximal(DdManager *dd, DdNode *S)
Definition extraBddMaxMin.c:294
extraZddMinimal
DdNode * extraZddMinimal(DdManager *dd, DdNode *S)
Definition extraBddMaxMin.c:373
Extra_zddEmptyBelongs
int Extra_zddEmptyBelongs(DdManager *dd, DdNode *zS)
Definition extraBddSet.c:265
extraZddMaxDotProduct
DdNode * extraZddMaxDotProduct(DdManager *dd, DdNode *S, DdNode *T)
Definition extraBddMaxMin.c:938
z0
#define z0
Definition extraBdd.h:77
extraZddNotSubSet
DdNode * extraZddNotSubSet(DdManager *dd, DdNode *X, DdNode *Y)
Definition extraBddSet.c:550
extraZddNotSupSet
DdNode * extraZddNotSupSet(DdManager *dd, DdNode *X, DdNode *Y)
Definition extraBddSet.c:676
extraZddDotProduct
DdNode * extraZddDotProduct(DdManager *dd, DdNode *S, DdNode *T)
Definition extraBddMaxMin.c:672
extraZddCrossProduct
DdNode * extraZddCrossProduct(DdManager *dd, DdNode *S, DdNode *T)
Definition extraBddMaxMin.c:799
z1
#define z1
Definition extraBdd.h:78
extraZddMinUnion
DdNode * extraZddMinUnion(DdManager *dd, DdNode *S, DdNode *T)
Definition extraBddMaxMin.c:564
extraZddMaxUnion
DdNode * extraZddMaxUnion(DdManager *dd, DdNode *S, DdNode *T)
Definition extraBddMaxMin.c:454