ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
Functions
extraBddSet.c File Reference
#include "extraBdd.h"
Include dependency graph for extraBddSet.c:

Go to the source code of this file.

Functions

ABC_NAMESPACE_IMPL_START DdNode * Extra_zddSubSet (DdManager *dd, DdNode *X, DdNode *Y)
 
DdNode * Extra_zddSupSet (DdManager *dd, DdNode *X, DdNode *Y)
 
DdNode * Extra_zddNotSubSet (DdManager *dd, DdNode *X, DdNode *Y)
 
DdNode * Extra_zddNotSupSet (DdManager *dd, DdNode *X, DdNode *Y)
 
DdNode * Extra_zddMaxNotSupSet (DdManager *dd, DdNode *X, DdNode *Y)
 
int Extra_zddEmptyBelongs (DdManager *dd, DdNode *zS)
 
int Extra_zddIsOneSubset (DdManager *dd, DdNode *zS)
 
DdNode * extraZddSubSet (DdManager *dd, DdNode *X, DdNode *Y)
 
DdNode * extraZddSupSet (DdManager *dd, DdNode *X, DdNode *Y)
 
DdNode * extraZddNotSubSet (DdManager *dd, DdNode *X, DdNode *Y)
 
DdNode * extraZddNotSupSet (DdManager *dd, DdNode *X, DdNode *Y)
 
DdNode * extraZddMaxNotSupSet (DdManager *dd, DdNode *X, DdNode *Y)
 

Function Documentation

◆ Extra_zddEmptyBelongs()

int Extra_zddEmptyBelongs ( DdManager * dd,
DdNode * zS )

Function********************************************************************

Synopsis [Returns 1 if ZDD contains the empty combination; 0 otherwise.]

Description []

SideEffects []

SeeAlso []

Definition at line 265 of file extraBddSet.c.

268{
269 while ( zS->index != CUDD_MAXINDEX )
270 zS = cuddE( zS );
271 return (int)( zS == z1 );
272
273} /* end of Extra_zddEmptyBelongs */
z1
#define z1
Definition extraBdd.h:78
Here is the caller graph for this function:

◆ Extra_zddIsOneSubset()

int Extra_zddIsOneSubset ( DdManager * dd,
DdNode * zS )

Function********************************************************************

Synopsis [Returns 1 if the set is empty or consists of one subset only.]

Description []

SideEffects []

SeeAlso []

Definition at line 288 of file extraBddSet.c.

291{
292 while ( zS->index != CUDD_MAXINDEX )
293 {
294 assert( cuddT(zS) != z0 );
295 if ( cuddE(zS) != z0 )
296 return 0;
297 zS = cuddT( zS );
298 }
299 return (int)( zS == z1 );
300
301} /* end of Extra_zddEmptyBelongs */
z0
#define z0
Definition extraBdd.h:77
assert
#define assert(ex)
Definition util_old.h:213

◆ Extra_zddMaxNotSupSet()

DdNode * Extra_zddMaxNotSupSet ( DdManager * dd,
DdNode * X,
DdNode * Y )

Function********************************************************************

Synopsis [Computes the maximal of subsets in X not contained in any of the subsets of Y.]

Description []

SideEffects []

SeeAlso [Extra_zddSubSet, Extra_zddSupSet, Extra_zddSubSet, Extra_zddNotSupSet]

Definition at line 232 of file extraBddSet.c.

236{
237 DdNode *res;
238 int autoDynZ;
239
240 autoDynZ = dd->autoDynZ;
241 dd->autoDynZ = 0;
242
243 do {
244 dd->reordered = 0;
245 res = extraZddMaxNotSupSet(dd, X, Y);
246 } while (dd->reordered == 1);
247 dd->autoDynZ = autoDynZ;
248 return(res);
249
250} /* end of Extra_zddMaxNotSupSet */
extraZddMaxNotSupSet
DdNode * extraZddMaxNotSupSet(DdManager *dd, DdNode *X, DdNode *Y)
Definition extraBddSet.c:799
Here is the call graph for this function:

◆ Extra_zddNotSubSet()

DdNode * Extra_zddNotSubSet ( DdManager * dd,
DdNode * X,
DdNode * Y )

Function********************************************************************

Synopsis [Computes subsets in X that are not contained in any of the subsets of Y.]

Description []

SideEffects []

SeeAlso [Extra_zddSubSet, Extra_zddSupSet, Extra_zddNotSupSet]

Definition at line 165 of file extraBddSet.c.

169{
170 DdNode *res;
171 int autoDynZ;
172
173 autoDynZ = dd->autoDynZ;
174 dd->autoDynZ = 0;
175
176 do {
177 dd->reordered = 0;
178 res = extraZddNotSubSet(dd, X, Y);
179 } while (dd->reordered == 1);
180 dd->autoDynZ = autoDynZ;
181 return(res);
182
183} /* end of Extra_zddNotSubSet */
extraZddNotSubSet
DdNode * extraZddNotSubSet(DdManager *dd, DdNode *X, DdNode *Y)
Definition extraBddSet.c:550
Here is the call graph for this function:

◆ Extra_zddNotSupSet()

DdNode * Extra_zddNotSupSet ( DdManager * dd,
DdNode * X,
DdNode * Y )

Function********************************************************************

Synopsis [Computes subsets in X that do not contain any of the subsets of Y.]

Description []

SideEffects []

SeeAlso [Extra_zddSubSet, Extra_zddSupSet, Extra_zddNotSubSet]

Definition at line 198 of file extraBddSet.c.

202{
203 DdNode *res;
204 int autoDynZ;
205
206 autoDynZ = dd->autoDynZ;
207 dd->autoDynZ = 0;
208
209 do {
210 dd->reordered = 0;
211 res = extraZddNotSupSet(dd, X, Y);
212 } while (dd->reordered == 1);
213 dd->autoDynZ = autoDynZ;
214 return(res);
215
216} /* end of Extra_zddNotSupSet */
extraZddNotSupSet
DdNode * extraZddNotSupSet(DdManager *dd, DdNode *X, DdNode *Y)
Definition extraBddSet.c:676
Here is the call graph for this function:

◆ Extra_zddSubSet()

ABC_NAMESPACE_IMPL_START DdNode * Extra_zddSubSet ( DdManager * dd,
DdNode * X,
DdNode * Y )

CFile***********************************************************************

FileName [zSubSet.c]

PackageName [extra]

Synopsis [Experimental version of some ZDD operators.]

Description [External procedures included in this module:

Internal procedures included in this module:

Static procedures included in this module:

SubSet, SupSet, NotSubSet, NotSupSet were introduced by O.Coudert to solve problems arising in two-level SOP minimization. See O. Coudert, "Two-Level Logic Minimization: An Overview", Integration. Vol. 17, No. 2, pp. 97-140, Oct 1994. ]

SeeAlso []

Author [Alan Mishchenko]

Copyright []

Revision [$zSubSet.c, v.1.2, November 16, 2000, alanmi $] AutomaticStart AutomaticEnd Function********************************************************************

Synopsis [Computes subsets in X that are contained in some of the subsets of Y.]

Description []

SideEffects []

SeeAlso [Extra_zddNotSubSet, Extra_zddSupSet, Extra_zddNotSupSet]

Definition at line 100 of file extraBddSet.c.

104{
105 DdNode *res;
106 int autoDynZ;
107
108 autoDynZ = dd->autoDynZ;
109 dd->autoDynZ = 0;
110
111 do {
112 dd->reordered = 0;
113 res = extraZddSubSet(dd, X, Y);
114 } while (dd->reordered == 1);
115 dd->autoDynZ = autoDynZ;
116 return(res);
117
118} /* end of Extra_zddSubSet */
extraZddSubSet
DdNode * extraZddSubSet(DdManager *dd, DdNode *X, DdNode *Y)
Definition extraBddSet.c:319
Here is the call graph for this function:

◆ Extra_zddSupSet()

DdNode * Extra_zddSupSet ( DdManager * dd,
DdNode * X,
DdNode * Y )

Function********************************************************************

Synopsis [Computes subsets in X that contain some of the subsets of Y.]

Description []

SideEffects []

SeeAlso [Extra_zddSubSet, Extra_zddNotSubSet, Extra_zddNotSupSet]

Definition at line 133 of file extraBddSet.c.

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 = extraZddSupSet(dd, X, Y);
147 } while (dd->reordered == 1);
148 dd->autoDynZ = autoDynZ;
149 return(res);
150
151} /* end of Extra_zddSupSet */
extraZddSupSet
DdNode * extraZddSupSet(DdManager *dd, DdNode *X, DdNode *Y)
Definition extraBddSet.c:430
Here is the call graph for this function:

◆ extraZddMaxNotSupSet()

DdNode * extraZddMaxNotSupSet ( DdManager * dd,
DdNode * X,
DdNode * Y )

Function********************************************************************

Synopsis [Performs the recursive step of Extra_zddMaxNotSupSet.]

Description []

SideEffects [None]

SeeAlso []

Definition at line 799 of file extraBddSet.c.

800{
801 DdNode *zRes;
802 statLine(dd);
803 /* any comb is a superset of itself */
804 if ( X == Y )
805 return z0;
806 /* no comb in X is superset of non-existing combs */
807 if ( Y == z0 )
808 return extraZddMaximal( dd, X );
809 /* any comb in X is the superset of the empty comb */
810 if ( Extra_zddEmptyBelongs( dd, Y ) )
811 return z0;
812 /* if X is empty, the result is empty */
813 if ( X == z0 )
814 return z0;
815 /* if X is the empty comb (and Y does not contain it!), return it */
816 if ( X == z1 )
817 return z1;
818
819 /* check cache */
820 zRes = cuddCacheLookup2Zdd(dd, extraZddMaxNotSupSet, X, Y);
821 if (zRes)
822 return(zRes);
823 else
824 {
825 DdNode *zRes0, *zRes1, *zTemp;
826 int TopLevelX = dd->permZ[ X->index ];
827 int TopLevelY = dd->permZ[ Y->index ];
828
829 if ( TopLevelX < TopLevelY )
830 {
831 /* combinations of X without label that are supersets of combinations with Y */
832 zRes0 = extraZddMaxNotSupSet( dd, cuddE( X ), Y );
833 if ( zRes0 == NULL )
834 return NULL;
835 cuddRef( zRes0 );
836
837 /* combinations of X with label that are supersets of combinations with Y */
838 zRes1 = extraZddMaxNotSupSet( dd, cuddT( X ), Y );
839 if ( zRes1 == NULL )
840 {
841 Cudd_RecursiveDerefZdd( dd, zRes0 );
842 return NULL;
843 }
844 cuddRef( zRes1 );
845
846 /* ---------------------------------------------------- */
847 /* remove subsets without this element covered by subsets with this element */
848 zRes0 = extraZddNotSubSet(dd, zTemp = zRes0, zRes1);
849 if ( zRes0 == NULL )
850 {
851 Cudd_RecursiveDerefZdd(dd, zTemp);
852 Cudd_RecursiveDerefZdd(dd, zRes1);
853 return NULL;
854 }
855 cuddRef( zRes0 );
856 Cudd_RecursiveDerefZdd(dd, zTemp);
857 /* ---------------------------------------------------- */
858
859 /* compose Res0 and Res1 with the given ZDD variable */
860 zRes = cuddZddGetNode( dd, X->index, zRes1, zRes0 );
861 if ( zRes == NULL )
862 {
863 Cudd_RecursiveDerefZdd( dd, zRes0 );
864 Cudd_RecursiveDerefZdd( dd, zRes1 );
865 return NULL;
866 }
867 cuddDeref( zRes0 );
868 cuddDeref( zRes1 );
869 }
870 else if ( TopLevelX == TopLevelY )
871 {
872 /* combs of X without var that are supersets of combs of Y without var */
873 zRes0 = extraZddMaxNotSupSet( dd, cuddE( X ), cuddE( Y ) );
874 if ( zRes0 == NULL )
875 return NULL;
876 cuddRef( zRes0 );
877
878 /* merge combs of Y with and without var */
879 zTemp = cuddZddUnion( dd, cuddE( Y ), cuddT( Y ) );
880 if ( zTemp == NULL )
881 {
882 Cudd_RecursiveDerefZdd( dd, zRes0 );
883 return NULL;
884 }
885 cuddRef( zTemp );
886
887 /* combs of X with label that are supersets of combs in Temp */
888 zRes1 = extraZddMaxNotSupSet( dd, cuddT( X ), zTemp );
889 if ( zRes1 == NULL )
890 {
891 Cudd_RecursiveDerefZdd( dd, zRes0 );
892 Cudd_RecursiveDerefZdd( dd, zTemp );
893 return NULL;
894 }
895 cuddRef( zRes1 );
896 Cudd_RecursiveDerefZdd( dd, zTemp );
897
898 /* ---------------------------------------------------- */
899 /* remove subsets without this element covered by subsets with this element */
900 zRes0 = extraZddNotSubSet(dd, zTemp = zRes0, zRes1);
901 if ( zRes0 == NULL )
902 {
903 Cudd_RecursiveDerefZdd(dd, zTemp);
904 Cudd_RecursiveDerefZdd(dd, zRes1);
905 return NULL;
906 }
907 cuddRef( zRes0 );
908 Cudd_RecursiveDerefZdd(dd, zTemp);
909 /* ---------------------------------------------------- */
910
911 /* compose Res0 and Res1 with the given ZDD variable */
912 zRes = cuddZddGetNode( dd, X->index, zRes1, zRes0 );
913 if ( zRes == NULL )
914 {
915 Cudd_RecursiveDerefZdd( dd, zRes0 );
916 Cudd_RecursiveDerefZdd( dd, zRes1 );
917 return NULL;
918 }
919 cuddDeref( zRes0 );
920 cuddDeref( zRes1 );
921 }
922 else /* if ( TopLevelX > TopLevelY ) */
923 {
924 /* combs of X that are supersets of combs of Y without label */
925 zRes = extraZddMaxNotSupSet( dd, X, cuddE( Y ) );
926 if ( zRes == NULL ) return NULL;
927 }
928
929 /* insert the result into cache */
930 cuddCacheInsert2(dd, extraZddMaxNotSupSet, X, Y, zRes);
931 return zRes;
932 }
933} /* end of extraZddMaxNotSupSet */
Extra_zddEmptyBelongs
int Extra_zddEmptyBelongs(DdManager *dd, DdNode *zS)
Definition extraBddSet.c:265
extraZddMaximal
DdNode * extraZddMaximal(DdManager *dd, DdNode *S)
Definition extraBddMaxMin.c:294
extraZddMaxNotSupSet
DdNode * extraZddMaxNotSupSet(DdManager *dd, DdNode *X, DdNode *Y)
Definition extraBddSet.c:799
Here is the call graph for this function:
Here is the caller graph for this function:

◆ extraZddNotSubSet()

DdNode * extraZddNotSubSet ( DdManager * dd,
DdNode * X,
DdNode * Y )

Function********************************************************************

Synopsis [Performs the recursive step of Extra_zddNotSubSet.]

Description []

SideEffects [None]

SeeAlso []

Definition at line 550 of file extraBddSet.c.

551{
552 DdNode *zRes;
553 statLine(dd);
554 /* any comb is a subset of itself */
555 if ( X == Y )
556 return z0;
557 /* combs in X are notsubsets of non-existant combs in Y */
558 if ( Y == z0 )
559 return X;
560 /* only {()} is the subset of {()} */
561 if ( Y == z1 ) /* remove empty combination from X */
562 return cuddZddDiff( dd, X, z1 );
563 /* if X is empty, the result is empty */
564 if ( X == z0 )
565 return z0;
566 /* the empty comb is contained in all combs of Y */
567 if ( X == z1 )
568 return z0;
569
570 /* check cache */
571 zRes = cuddCacheLookup2Zdd(dd, extraZddNotSubSet, X, Y);
572 if (zRes)
573 return(zRes);
574 else
575 {
576 DdNode *zRes0, *zRes1, *zTemp;
577 int TopLevelX = dd->permZ[ X->index ];
578 int TopLevelY = dd->permZ[ Y->index ];
579
580 if ( TopLevelX < TopLevelY )
581 {
582 /* compute combs of X without var that are notsubsets of combs with Y */
583 zRes0 = extraZddNotSubSet( dd, cuddE( X ), Y );
584 if ( zRes0 == NULL )
585 return NULL;
586 cuddRef( zRes0 );
587
588 /* combs of X with var cannot be subsets of combs without var in Y */
589 zRes1 = cuddT( X );
590
591 /* compose Res0 and Res1 with the given ZDD variable */
592 zRes = cuddZddGetNode( dd, X->index, zRes1, zRes0 );
593 if ( zRes == NULL )
594 {
595 Cudd_RecursiveDerefZdd( dd, zRes0 );
596 return NULL;
597 }
598 cuddDeref( zRes0 );
599 }
600 else if ( TopLevelX == TopLevelY )
601 {
602 /* merge combs of Y with and without var */
603 zTemp = cuddZddUnion( dd, cuddE( Y ), cuddT( Y ) );
604 if ( zTemp == NULL )
605 return NULL;
606 cuddRef( zTemp );
607
608 /* compute combs of X without var that are notsubsets of combs is Temp */
609 zRes0 = extraZddNotSubSet( dd, cuddE( X ), zTemp );
610 if ( zRes0 == NULL )
611 {
612 Cudd_RecursiveDerefZdd( dd, zTemp );
613 return NULL;
614 }
615 cuddRef( zRes0 );
616 Cudd_RecursiveDerefZdd( dd, zTemp );
617
618 /* combs of X with var that are notsubsets of combs in Y with var */
619 zRes1 = extraZddNotSubSet( dd, cuddT( X ), cuddT( Y ) );
620 if ( zRes1 == NULL )
621 {
622 Cudd_RecursiveDerefZdd( dd, zRes0 );
623 return NULL;
624 }
625 cuddRef( zRes1 );
626
627 /* compose Res0 and Res1 with the given ZDD variable */
628 zRes = cuddZddGetNode( dd, X->index, zRes1, zRes0 );
629 if ( zRes == NULL )
630 {
631 Cudd_RecursiveDerefZdd( dd, zRes0 );
632 Cudd_RecursiveDerefZdd( dd, zRes1 );
633 return NULL;
634 }
635 cuddDeref( zRes0 );
636 cuddDeref( zRes1 );
637 }
638 else /* if ( TopLevelX > TopLevelY ) */
639 {
640 /* merge combs of Y with and without var */
641 zTemp = cuddZddUnion( dd, cuddE( Y ), cuddT( Y ) );
642 if ( zTemp == NULL )
643 return NULL;
644 cuddRef( zTemp );
645
646 /* compute combs that are notsubsets of Temp */
647 zRes = extraZddNotSubSet( dd, X, zTemp );
648 if ( zRes == NULL )
649 {
650 Cudd_RecursiveDerefZdd( dd, zTemp );
651 return NULL;
652 }
653 cuddRef( zRes );
654 Cudd_RecursiveDerefZdd( dd, zTemp );
655 cuddDeref( zRes );
656 }
657
658 /* insert the result into cache */
659 cuddCacheInsert2(dd, extraZddNotSubSet, X, Y, zRes);
660 return zRes;
661 }
662} /* end of extraZddNotSubSet */
extraZddNotSubSet
DdNode * extraZddNotSubSet(DdManager *dd, DdNode *X, DdNode *Y)
Definition extraBddSet.c:550
Here is the call graph for this function:
Here is the caller graph for this function:

◆ extraZddNotSupSet()

DdNode * extraZddNotSupSet ( DdManager * dd,
DdNode * X,
DdNode * Y )

Function********************************************************************

Synopsis [Performs the recursive step of Extra_zddNotSupSet.]

Description []

SideEffects [None]

SeeAlso []

Definition at line 676 of file extraBddSet.c.

677{
678 DdNode *zRes;
679 statLine(dd);
680 /* any comb is a superset of itself */
681 if ( X == Y )
682 return z0;
683 /* no comb in X is superset of non-existing combs */
684 if ( Y == z0 )
685 return X;
686 /* any comb in X is the superset of the empty comb */
687 if ( Extra_zddEmptyBelongs( dd, Y ) )
688 return z0;
689 /* if X is empty, the result is empty */
690 if ( X == z0 )
691 return z0;
692 /* if X is the empty comb (and Y does not contain it!), return it */
693 if ( X == z1 )
694 return z1;
695
696 /* check cache */
697 zRes = cuddCacheLookup2Zdd(dd, extraZddNotSupSet, X, Y);
698 if (zRes)
699 return(zRes);
700 else
701 {
702 DdNode *zRes0, *zRes1, *zTemp;
703 int TopLevelX = dd->permZ[ X->index ];
704 int TopLevelY = dd->permZ[ Y->index ];
705
706 if ( TopLevelX < TopLevelY )
707 {
708 /* combinations of X without label that are supersets of combinations of Y */
709 zRes0 = extraZddNotSupSet( dd, cuddE( X ), Y );
710 if ( zRes0 == NULL )
711 return NULL;
712 cuddRef( zRes0 );
713
714 /* combinations of X with label that are supersets of combinations of Y */
715 zRes1 = extraZddNotSupSet( dd, cuddT( X ), Y );
716 if ( zRes1 == NULL )
717 {
718 Cudd_RecursiveDerefZdd( dd, zRes0 );
719 return NULL;
720 }
721 cuddRef( zRes1 );
722
723 /* compose Res0 and Res1 with the given ZDD variable */
724 zRes = cuddZddGetNode( dd, X->index, zRes1, zRes0 );
725 if ( zRes == NULL )
726 {
727 Cudd_RecursiveDerefZdd( dd, zRes0 );
728 Cudd_RecursiveDerefZdd( dd, zRes1 );
729 return NULL;
730 }
731 cuddDeref( zRes0 );
732 cuddDeref( zRes1 );
733 }
734 else if ( TopLevelX == TopLevelY )
735 {
736 /* combs of X without var that are not supersets of combs of Y without var */
737 zRes0 = extraZddNotSupSet( dd, cuddE( X ), cuddE( Y ) );
738 if ( zRes0 == NULL )
739 return NULL;
740 cuddRef( zRes0 );
741
742 /* merge combs of Y with and without var */
743 zTemp = cuddZddUnion( dd, cuddE( Y ), cuddT( Y ) );
744 if ( zTemp == NULL )
745 {
746 Cudd_RecursiveDerefZdd( dd, zRes0 );
747 return NULL;
748 }
749 cuddRef( zTemp );
750
751 /* combs of X with label that are supersets of combs in Temp */
752 zRes1 = extraZddNotSupSet( dd, cuddT( X ), zTemp );
753 if ( zRes1 == NULL )
754 {
755 Cudd_RecursiveDerefZdd( dd, zRes0 );
756 Cudd_RecursiveDerefZdd( dd, zTemp );
757 return NULL;
758 }
759 cuddRef( zRes1 );
760 Cudd_RecursiveDerefZdd( dd, zTemp );
761
762 /* compose Res0 and Res1 with the given ZDD variable */
763 zRes = cuddZddGetNode( dd, X->index, zRes1, zRes0 );
764 if ( zRes == NULL )
765 {
766 Cudd_RecursiveDerefZdd( dd, zRes0 );
767 Cudd_RecursiveDerefZdd( dd, zRes1 );
768 return NULL;
769 }
770 cuddDeref( zRes0 );
771 cuddDeref( zRes1 );
772 }
773 else /* if ( TopLevelX > TopLevelY ) */
774 {
775 /* combs of X that are supersets of combs of Y without label */
776 zRes = extraZddNotSupSet( dd, X, cuddE( Y ) );
777 if ( zRes == NULL ) return NULL;
778 }
779
780 /* insert the result into cache */
781 cuddCacheInsert2(dd, extraZddNotSupSet, X, Y, zRes);
782 return zRes;
783 }
784} /* end of extraZddNotSupSet */
extraZddNotSupSet
DdNode * extraZddNotSupSet(DdManager *dd, DdNode *X, DdNode *Y)
Definition extraBddSet.c:676
Here is the call graph for this function:
Here is the caller graph for this function:

◆ extraZddSubSet()

DdNode * extraZddSubSet ( DdManager * dd,
DdNode * X,
DdNode * Y )

Function********************************************************************

Synopsis [Performs the recursive step of Extra_zddSubSet.]

Description []

SideEffects [None]

SeeAlso []

Definition at line 319 of file extraBddSet.c.

320{
321 DdNode *zRes;
322 statLine(dd);
323 /* any comb is a subset of itself */
324 if ( X == Y )
325 return X;
326 /* if X is empty, the result is empty */
327 if ( X == z0 )
328 return z0;
329 /* combs in X are notsubsets of non-existant combs in Y */
330 if ( Y == z0 )
331 return z0;
332 /* the empty comb is contained in all combs of Y */
333 if ( X == z1 )
334 return z1;
335 /* only {()} is the subset of {()} */
336 if ( Y == z1 ) /* check whether the empty combination is present in X */
337 return ( Extra_zddEmptyBelongs( dd, X )? z1: z0 );
338
339 /* check cache */
340 zRes = cuddCacheLookup2Zdd(dd, extraZddSubSet, X, Y);
341 if (zRes)
342 return(zRes);
343 else
344 {
345 DdNode *zRes0, *zRes1, *zTemp;
346 int TopLevelX = dd->permZ[ X->index ];
347 int TopLevelY = dd->permZ[ Y->index ];
348
349 if ( TopLevelX < TopLevelY )
350 {
351 /* compute combs of X without var that are notsubsets of combs with Y */
352 zRes = extraZddSubSet( dd, cuddE( X ), Y );
353 if ( zRes == NULL ) return NULL;
354 }
355 else if ( TopLevelX == TopLevelY )
356 {
357 /* merge combs of Y with and without var */
358 zTemp = cuddZddUnion( dd, cuddE( Y ), cuddT( Y ) );
359 if ( zTemp == NULL )
360 return NULL;
361 cuddRef( zTemp );
362
363 /* compute combs of X without var that are notsubsets of combs is Temp */
364 zRes0 = extraZddSubSet( dd, cuddE( X ), zTemp );
365 if ( zRes0 == NULL )
366 {
367 Cudd_RecursiveDerefZdd( dd, zTemp );
368 return NULL;
369 }
370 cuddRef( zRes0 );
371 Cudd_RecursiveDerefZdd( dd, zTemp );
372
373 /* combs of X with var that are notsubsets of combs in Y with var */
374 zRes1 = extraZddSubSet( dd, cuddT( X ), cuddT( Y ) );
375 if ( zRes1 == NULL )
376 {
377 Cudd_RecursiveDerefZdd( dd, zRes0 );
378 return NULL;
379 }
380 cuddRef( zRes1 );
381
382 /* compose Res0 and Res1 with the given ZDD variable */
383 zRes = cuddZddGetNode( dd, X->index, zRes1, zRes0 );
384 if ( zRes == NULL )
385 {
386 Cudd_RecursiveDerefZdd( dd, zRes0 );
387 Cudd_RecursiveDerefZdd( dd, zRes1 );
388 return NULL;
389 }
390 cuddDeref( zRes0 );
391 cuddDeref( zRes1 );
392 }
393 else /* if ( TopLevelX > TopLevelY ) */
394 {
395 /* merge combs of Y with and without var */
396 zTemp = cuddZddUnion( dd, cuddE( Y ), cuddT( Y ) );
397 if ( zTemp == NULL ) return NULL;
398 cuddRef( zTemp );
399
400 /* compute combs that are notsubsets of Temp */
401 zRes = extraZddSubSet( dd, X, zTemp );
402 if ( zRes == NULL )
403 {
404 Cudd_RecursiveDerefZdd( dd, zTemp );
405 return NULL;
406 }
407 cuddRef( zRes );
408 Cudd_RecursiveDerefZdd( dd, zTemp );
409 cuddDeref( zRes );
410 }
411
412 /* insert the result into cache */
413 cuddCacheInsert2(dd, extraZddSubSet, X, Y, zRes);
414 return zRes;
415 }
416} /* end of extraZddSubSet */
extraZddSubSet
DdNode * extraZddSubSet(DdManager *dd, DdNode *X, DdNode *Y)
Definition extraBddSet.c:319
Here is the call graph for this function:
Here is the caller graph for this function:

◆ extraZddSupSet()

DdNode * extraZddSupSet ( DdManager * dd,
DdNode * X,
DdNode * Y )

Function********************************************************************

Synopsis [Performs the recursive step of Extra_zddSupSet.]

Description []

SideEffects [None]

SeeAlso []

Definition at line 430 of file extraBddSet.c.

431{
432 DdNode *zRes;
433 statLine(dd);
434 /* any comb is a superset of itself */
435 if ( X == Y )
436 return X;
437 /* no comb in X is superset of non-existing combs */
438 if ( Y == z0 )
439 return z0;
440 /* any comb in X is the superset of the empty comb */
441 if ( Extra_zddEmptyBelongs( dd, Y ) )
442 return X;
443 /* if X is empty, the result is empty */
444 if ( X == z0 )
445 return z0;
446 /* if X is the empty comb (and Y does not contain it!), return empty */
447 if ( X == z1 )
448 return z0;
449
450 /* check cache */
451 zRes = cuddCacheLookup2Zdd(dd, extraZddSupSet, X, Y);
452 if (zRes)
453 return(zRes);
454 else
455 {
456 DdNode *zRes0, *zRes1, *zTemp;
457 int TopLevelX = dd->permZ[ X->index ];
458 int TopLevelY = dd->permZ[ Y->index ];
459
460 if ( TopLevelX < TopLevelY )
461 {
462 /* combinations of X without label that are supersets of combinations with Y */
463 zRes0 = extraZddSupSet( dd, cuddE( X ), Y );
464 if ( zRes0 == NULL ) return NULL;
465 cuddRef( zRes0 );
466
467 /* combinations of X with label that are supersets of combinations with Y */
468 zRes1 = extraZddSupSet( dd, cuddT( X ), Y );
469 if ( zRes1 == NULL )
470 {
471 Cudd_RecursiveDerefZdd( dd, zRes0 );
472 return NULL;
473 }
474 cuddRef( zRes1 );
475
476 /* compose Res0 and Res1 with the given ZDD variable */
477 zRes = cuddZddGetNode( dd, X->index, zRes1, zRes0 );
478 if ( zRes == NULL )
479 {
480 Cudd_RecursiveDerefZdd( dd, zRes0 );
481 Cudd_RecursiveDerefZdd( dd, zRes1 );
482 return NULL;
483 }
484 cuddDeref( zRes0 );
485 cuddDeref( zRes1 );
486 }
487 else if ( TopLevelX == TopLevelY )
488 {
489 /* combs of X without var that are supersets of combs of Y without var */
490 zRes0 = extraZddSupSet( dd, cuddE( X ), cuddE( Y ) );
491 if ( zRes0 == NULL ) return NULL;
492 cuddRef( zRes0 );
493
494 /* merge combs of Y with and without var */
495 zTemp = cuddZddUnion( dd, cuddE( Y ), cuddT( Y ) );
496 if ( zTemp == NULL )
497 {
498 Cudd_RecursiveDerefZdd( dd, zRes0 );
499 return NULL;
500 }
501 cuddRef( zTemp );
502
503 /* combs of X with label that are supersets of combs in Temp */
504 zRes1 = extraZddSupSet( dd, cuddT( X ), zTemp );
505 if ( zRes1 == NULL )
506 {
507 Cudd_RecursiveDerefZdd( dd, zRes0 );
508 Cudd_RecursiveDerefZdd( dd, zTemp );
509 return NULL;
510 }
511 cuddRef( zRes1 );
512 Cudd_RecursiveDerefZdd( dd, zTemp );
513
514 /* compose Res0 and Res1 with the given ZDD variable */
515 zRes = cuddZddGetNode( dd, X->index, zRes1, zRes0 );
516 if ( zRes == NULL )
517 {
518 Cudd_RecursiveDerefZdd( dd, zRes0 );
519 Cudd_RecursiveDerefZdd( dd, zRes1 );
520 return NULL;
521 }
522 cuddDeref( zRes0 );
523 cuddDeref( zRes1 );
524 }
525 else /* if ( TopLevelX > TopLevelY ) */
526 {
527 /* combs of X that are supersets of combs of Y without label */
528 zRes = extraZddSupSet( dd, X, cuddE( Y ) );
529 if ( zRes == NULL ) return NULL;
530 }
531
532 /* insert the result into cache */
533 cuddCacheInsert2(dd, extraZddSupSet, X, Y, zRes);
534 return zRes;
535 }
536} /* end of extraZddSupSet */
extraZddSupSet
DdNode * extraZddSupSet(DdManager *dd, DdNode *X, DdNode *Y)
Definition extraBddSet.c:430
Here is the call graph for this function:
Here is the caller graph for this function: