1 /**CFile***********************************************************************
3 FileName [cuddZddSetop.c]
7 Synopsis [Set operations on ZDDs.]
9 Description [External procedures included in this module:
13 <li> Cudd_zddIntersect()
15 <li> Cudd_zddDiffConst()
16 <li> Cudd_zddSubset1()
17 <li> Cudd_zddSubset0()
20 Internal procedures included in this module:
24 <li> cuddZddIntersect()
26 <li> cuddZddChangeAux()
30 Static procedures included in this module:
32 <li> zdd_subset1_aux()
33 <li> zdd_subset0_aux()
40 Author [Hyong-Kyoon Shin, In-Ho Moon]
42 Copyright [Copyright (c) 1995-2004, Regents of the University of Colorado
46 Redistribution and use in source and binary forms, with or without
47 modification, are permitted provided that the following conditions
50 Redistributions of source code must retain the above copyright
51 notice, this list of conditions and the following disclaimer.
53 Redistributions in binary form must reproduce the above copyright
54 notice, this list of conditions and the following disclaimer in the
55 documentation and/or other materials provided with the distribution.
57 Neither the name of the University of Colorado nor the names of its
58 contributors may be used to endorse or promote products derived from
59 this software without specific prior written permission.
61 THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
62 "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
63 LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
64 FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
65 COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
66 INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
67 BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
68 LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
69 CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
70 LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
71 ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
72 POSSIBILITY OF SUCH DAMAGE.]
74 ******************************************************************************/
79 /*---------------------------------------------------------------------------*/
80 /* Constant declarations */
81 /*---------------------------------------------------------------------------*/
84 /*---------------------------------------------------------------------------*/
85 /* Stucture declarations */
86 /*---------------------------------------------------------------------------*/
89 /*---------------------------------------------------------------------------*/
90 /* Type declarations */
91 /*---------------------------------------------------------------------------*/
94 /*---------------------------------------------------------------------------*/
95 /* Variable declarations */
96 /*---------------------------------------------------------------------------*/
99 static char rcsid
[] DD_UNUSED
= "$Id: cuddZddSetop.c,v 1.25 2004/08/13 18:04:54 fabio Exp $";
102 /*---------------------------------------------------------------------------*/
103 /* Macro declarations */
104 /*---------------------------------------------------------------------------*/
110 /**AutomaticStart*************************************************************/
112 /*---------------------------------------------------------------------------*/
113 /* Static function prototypes */
114 /*---------------------------------------------------------------------------*/
116 static DdNode
* zdd_subset1_aux (DdManager
*zdd
, DdNode
*P
, DdNode
*zvar
);
117 static DdNode
* zdd_subset0_aux (DdManager
*zdd
, DdNode
*P
, DdNode
*zvar
);
118 static void zddVarToConst (DdNode
*f
, DdNode
**gp
, DdNode
**hp
, DdNode
*base
, DdNode
*empty
);
120 /**AutomaticEnd***************************************************************/
126 /*---------------------------------------------------------------------------*/
127 /* Definition of exported functions */
128 /*---------------------------------------------------------------------------*/
131 /**Function********************************************************************
133 Synopsis [Computes the ITE of three ZDDs.]
135 Description [Computes the ITE of three ZDDs. Returns a pointer to the
136 result if successful; NULL otherwise.]
142 ******************************************************************************/
154 res
= cuddZddIte(dd
, f
, g
, h
);
155 } while (dd
->reordered
== 1);
158 } /* end of Cudd_zddIte */
161 /**Function********************************************************************
163 Synopsis [Computes the union of two ZDDs.]
165 Description [Computes the union of two ZDDs. Returns a pointer to the
166 result if successful; NULL otherwise.]
172 ******************************************************************************/
183 res
= cuddZddUnion(dd
, P
, Q
);
184 } while (dd
->reordered
== 1);
187 } /* end of Cudd_zddUnion */
190 /**Function********************************************************************
192 Synopsis [Computes the intersection of two ZDDs.]
194 Description [Computes the intersection of two ZDDs. Returns a pointer to
195 the result if successful; NULL otherwise.]
201 ******************************************************************************/
212 res
= cuddZddIntersect(dd
, P
, Q
);
213 } while (dd
->reordered
== 1);
216 } /* end of Cudd_zddIntersect */
219 /**Function********************************************************************
221 Synopsis [Computes the difference of two ZDDs.]
223 Description [Computes the difference of two ZDDs. Returns a pointer to the
224 result if successful; NULL otherwise.]
228 SeeAlso [Cudd_zddDiffConst]
230 ******************************************************************************/
241 res
= cuddZddDiff(dd
, P
, Q
);
242 } while (dd
->reordered
== 1);
245 } /* end of Cudd_zddDiff */
248 /**Function********************************************************************
250 Synopsis [Performs the inclusion test for ZDDs (P implies Q).]
252 Description [Inclusion test for ZDDs (P implies Q). No new nodes are
253 generated by this procedure. Returns empty if true;
254 a valid pointer different from empty or DD_NON_CONSTANT otherwise.]
258 SeeAlso [Cudd_zddDiff]
260 ******************************************************************************/
268 DdNode
*empty
= DD_ZERO(zdd
), *t
, *res
;
269 DdManager
*table
= zdd
;
279 /* Check cache. The cache is shared by cuddZddDiff(). */
280 res
= cuddCacheLookup2Zdd(table
, cuddZddDiff
, P
, Q
);
284 if (cuddIsConstant(P
))
287 p_top
= zdd
->permZ
[P
->index
];
288 if (cuddIsConstant(Q
))
291 q_top
= zdd
->permZ
[Q
->index
];
293 res
= DD_NON_CONSTANT
;
294 } else if (p_top
> q_top
) {
295 res
= Cudd_zddDiffConst(zdd
, P
, cuddE(Q
));
297 t
= Cudd_zddDiffConst(zdd
, cuddT(P
), cuddT(Q
));
299 res
= DD_NON_CONSTANT
;
301 res
= Cudd_zddDiffConst(zdd
, cuddE(P
), cuddE(Q
));
304 cuddCacheInsert2(table
, cuddZddDiff
, P
, Q
, res
);
308 } /* end of Cudd_zddDiffConst */
311 /**Function********************************************************************
313 Synopsis [Computes the positive cofactor of a ZDD w.r.t. a variable.]
315 Description [Computes the positive cofactor of a ZDD w.r.t. a
316 variable. In terms of combinations, the result is the set of all
317 combinations in which the variable is asserted. Returns a pointer to
318 the result if successful; NULL otherwise.]
322 SeeAlso [Cudd_zddSubset0]
324 ******************************************************************************/
335 r
= cuddZddSubset1(dd
, P
, var
);
336 } while (dd
->reordered
== 1);
340 } /* end of Cudd_zddSubset1 */
343 /**Function********************************************************************
345 Synopsis [Computes the negative cofactor of a ZDD w.r.t. a variable.]
347 Description [Computes the negative cofactor of a ZDD w.r.t. a
348 variable. In terms of combinations, the result is the set of all
349 combinations in which the variable is negated. Returns a pointer to
350 the result if successful; NULL otherwise.]
354 SeeAlso [Cudd_zddSubset1]
356 ******************************************************************************/
367 r
= cuddZddSubset0(dd
, P
, var
);
368 } while (dd
->reordered
== 1);
372 } /* end of Cudd_zddSubset0 */
375 /**Function********************************************************************
377 Synopsis [Substitutes a variable with its complement in a ZDD.]
379 Description [Substitutes a variable with its complement in a ZDD.
380 returns a pointer to the result if successful; NULL otherwise.]
386 ******************************************************************************/
395 if ((unsigned int) var
>= CUDD_MAXINDEX
- 1) return(NULL
);
399 res
= cuddZddChange(dd
, P
, var
);
400 } while (dd
->reordered
== 1);
403 } /* end of Cudd_zddChange */
406 /*---------------------------------------------------------------------------*/
407 /* Definition of internal functions */
408 /*---------------------------------------------------------------------------*/
411 /**Function********************************************************************
413 Synopsis [Performs the recursive step of Cudd_zddIte.]
421 ******************************************************************************/
429 DdNode
*tautology
, *empty
;
430 DdNode
*r
,*Gv
,*Gvn
,*Hv
,*Hvn
,*t
,*e
;
431 unsigned int topf
,topg
,toph
,v
,top
;
436 /* One variable cases. */
437 if (f
== (empty
= DD_ZERO(dd
))) { /* ITE(0,G,H) = H */
440 topf
= cuddIZ(dd
,f
->index
);
441 topg
= cuddIZ(dd
,g
->index
);
442 toph
= cuddIZ(dd
,h
->index
);
443 v
= ddMin(topg
,toph
);
446 tautology
= (top
== CUDD_MAXINDEX
) ? DD_ONE(dd
) : dd
->univ
[top
];
447 if (f
== tautology
) { /* ITE(1,G,H) = G */
451 /* From now on, f is known to not be a constant. */
452 zddVarToConst(f
,&g
,&h
,tautology
,empty
);
454 /* Check remaining one variable cases. */
455 if (g
== h
) { /* ITE(F,G,G) = G */
459 if (g
== tautology
) { /* ITE(F,1,0) = F */
460 if (h
== empty
) return(f
);
464 r
= cuddCacheLookupZdd(dd
,DD_ZDD_ITE_TAG
,f
,g
,h
);
469 /* Recompute these because they may have changed in zddVarToConst. */
470 topg
= cuddIZ(dd
,g
->index
);
471 toph
= cuddIZ(dd
,h
->index
);
472 v
= ddMin(topg
,toph
);
475 r
= cuddZddIte(dd
,cuddE(f
),g
,h
);
476 if (r
== NULL
) return(NULL
);
477 } else if (topf
> v
) {
488 Hv
= cuddT(h
); Hvn
= cuddE(h
);
490 e
= cuddZddIte(dd
,f
,Gvn
,Hvn
);
491 if (e
== NULL
) return(NULL
);
493 r
= cuddZddGetNode(dd
,index
,Hv
,e
);
495 Cudd_RecursiveDerefZdd(dd
,e
);
504 Gv
= cuddT(g
); Gvn
= cuddE(g
);
509 Hv
= cuddT(h
); Hvn
= cuddE(h
);
511 e
= cuddZddIte(dd
,cuddE(f
),Gvn
,Hvn
);
512 if (e
== NULL
) return(NULL
);
514 t
= cuddZddIte(dd
,cuddT(f
),Gv
,Hv
);
516 Cudd_RecursiveDerefZdd(dd
,e
);
520 r
= cuddZddGetNode(dd
,index
,t
,e
);
522 Cudd_RecursiveDerefZdd(dd
,e
);
523 Cudd_RecursiveDerefZdd(dd
,t
);
530 cuddCacheInsert(dd
,DD_ZDD_ITE_TAG
,f
,g
,h
,r
);
534 } /* end of cuddZddIte */
537 /**Function********************************************************************
539 Synopsis [Performs the recursive step of Cudd_zddUnion.]
547 ******************************************************************************/
555 DdNode
*empty
= DD_ZERO(zdd
), *t
, *e
, *res
;
556 DdManager
*table
= zdd
;
567 res
= cuddCacheLookup2Zdd(table
, cuddZddUnion
, P
, Q
);
571 if (cuddIsConstant(P
))
574 p_top
= zdd
->permZ
[P
->index
];
575 if (cuddIsConstant(Q
))
578 q_top
= zdd
->permZ
[Q
->index
];
580 e
= cuddZddUnion(zdd
, cuddE(P
), Q
);
581 if (e
== NULL
) return (NULL
);
583 res
= cuddZddGetNode(zdd
, P
->index
, cuddT(P
), e
);
585 Cudd_RecursiveDerefZdd(table
, e
);
589 } else if (p_top
> q_top
) {
590 e
= cuddZddUnion(zdd
, P
, cuddE(Q
));
591 if (e
== NULL
) return(NULL
);
593 res
= cuddZddGetNode(zdd
, Q
->index
, cuddT(Q
), e
);
595 Cudd_RecursiveDerefZdd(table
, e
);
600 t
= cuddZddUnion(zdd
, cuddT(P
), cuddT(Q
));
601 if (t
== NULL
) return(NULL
);
603 e
= cuddZddUnion(zdd
, cuddE(P
), cuddE(Q
));
605 Cudd_RecursiveDerefZdd(table
, t
);
609 res
= cuddZddGetNode(zdd
, P
->index
, t
, e
);
611 Cudd_RecursiveDerefZdd(table
, t
);
612 Cudd_RecursiveDerefZdd(table
, e
);
619 cuddCacheInsert2(table
, cuddZddUnion
, P
, Q
, res
);
623 } /* end of cuddZddUnion */
626 /**Function********************************************************************
628 Synopsis [Performs the recursive step of Cudd_zddIntersect.]
636 ******************************************************************************/
644 DdNode
*empty
= DD_ZERO(zdd
), *t
, *e
, *res
;
645 DdManager
*table
= zdd
;
656 res
= cuddCacheLookup2Zdd(table
, cuddZddIntersect
, P
, Q
);
660 if (cuddIsConstant(P
))
663 p_top
= zdd
->permZ
[P
->index
];
664 if (cuddIsConstant(Q
))
667 q_top
= zdd
->permZ
[Q
->index
];
669 res
= cuddZddIntersect(zdd
, cuddE(P
), Q
);
670 if (res
== NULL
) return(NULL
);
671 } else if (p_top
> q_top
) {
672 res
= cuddZddIntersect(zdd
, P
, cuddE(Q
));
673 if (res
== NULL
) return(NULL
);
675 t
= cuddZddIntersect(zdd
, cuddT(P
), cuddT(Q
));
676 if (t
== NULL
) return(NULL
);
678 e
= cuddZddIntersect(zdd
, cuddE(P
), cuddE(Q
));
680 Cudd_RecursiveDerefZdd(table
, t
);
684 res
= cuddZddGetNode(zdd
, P
->index
, t
, e
);
686 Cudd_RecursiveDerefZdd(table
, t
);
687 Cudd_RecursiveDerefZdd(table
, e
);
694 cuddCacheInsert2(table
, cuddZddIntersect
, P
, Q
, res
);
698 } /* end of cuddZddIntersect */
701 /**Function********************************************************************
703 Synopsis [Performs the recursive step of Cudd_zddDiff.]
711 ******************************************************************************/
719 DdNode
*empty
= DD_ZERO(zdd
), *t
, *e
, *res
;
720 DdManager
*table
= zdd
;
730 /* Check cache. The cache is shared by Cudd_zddDiffConst(). */
731 res
= cuddCacheLookup2Zdd(table
, cuddZddDiff
, P
, Q
);
732 if (res
!= NULL
&& res
!= DD_NON_CONSTANT
)
735 if (cuddIsConstant(P
))
738 p_top
= zdd
->permZ
[P
->index
];
739 if (cuddIsConstant(Q
))
742 q_top
= zdd
->permZ
[Q
->index
];
744 e
= cuddZddDiff(zdd
, cuddE(P
), Q
);
745 if (e
== NULL
) return(NULL
);
747 res
= cuddZddGetNode(zdd
, P
->index
, cuddT(P
), e
);
749 Cudd_RecursiveDerefZdd(table
, e
);
753 } else if (p_top
> q_top
) {
754 res
= cuddZddDiff(zdd
, P
, cuddE(Q
));
755 if (res
== NULL
) return(NULL
);
757 t
= cuddZddDiff(zdd
, cuddT(P
), cuddT(Q
));
758 if (t
== NULL
) return(NULL
);
760 e
= cuddZddDiff(zdd
, cuddE(P
), cuddE(Q
));
762 Cudd_RecursiveDerefZdd(table
, t
);
766 res
= cuddZddGetNode(zdd
, P
->index
, t
, e
);
768 Cudd_RecursiveDerefZdd(table
, t
);
769 Cudd_RecursiveDerefZdd(table
, e
);
776 cuddCacheInsert2(table
, cuddZddDiff
, P
, Q
, res
);
780 } /* end of cuddZddDiff */
783 /**Function********************************************************************
785 Synopsis [Performs the recursive step of Cudd_zddChange.]
793 ******************************************************************************/
802 DdNode
*base
= DD_ONE(zdd
);
803 DdNode
*empty
= DD_ZERO(zdd
);
812 res
= cuddCacheLookup2Zdd(zdd
, cuddZddChangeAux
, P
, zvar
);
816 top_var
= zdd
->permZ
[P
->index
];
817 level
= zdd
->permZ
[zvar
->index
];
819 if (top_var
> level
) {
820 res
= cuddZddGetNode(zdd
, zvar
->index
, P
, DD_ZERO(zdd
));
821 if (res
== NULL
) return(NULL
);
822 } else if (top_var
== level
) {
823 res
= cuddZddGetNode(zdd
, zvar
->index
, cuddE(P
), cuddT(P
));
824 if (res
== NULL
) return(NULL
);
826 t
= cuddZddChangeAux(zdd
, cuddT(P
), zvar
);
827 if (t
== NULL
) return(NULL
);
829 e
= cuddZddChangeAux(zdd
, cuddE(P
), zvar
);
831 Cudd_RecursiveDerefZdd(zdd
, t
);
835 res
= cuddZddGetNode(zdd
, P
->index
, t
, e
);
837 Cudd_RecursiveDerefZdd(zdd
, t
);
838 Cudd_RecursiveDerefZdd(zdd
, e
);
845 cuddCacheInsert2(zdd
, cuddZddChangeAux
, P
, zvar
, res
);
849 } /* end of cuddZddChangeAux */
852 /**Function********************************************************************
854 Synopsis [Computes the positive cofactor of a ZDD w.r.t. a variable.]
856 Description [Computes the positive cofactor of a ZDD w.r.t. a
857 variable. In terms of combinations, the result is the set of all
858 combinations in which the variable is asserted. Returns a pointer to
859 the result if successful; NULL otherwise. cuddZddSubset1 performs
860 the same function as Cudd_zddSubset1, but does not restart if
861 reordering has taken place. Therefore it can be called from within a
862 recursive procedure.]
866 SeeAlso [cuddZddSubset0 Cudd_zddSubset1]
868 ******************************************************************************/
876 DdNode
*base
, *empty
;
881 zvar
= cuddUniqueInterZdd(dd
, var
, base
, empty
);
886 r
= zdd_subset1_aux(dd
, P
, zvar
);
888 Cudd_RecursiveDerefZdd(dd
, zvar
);
892 Cudd_RecursiveDerefZdd(dd
, zvar
);
898 } /* end of cuddZddSubset1 */
901 /**Function********************************************************************
903 Synopsis [Computes the negative cofactor of a ZDD w.r.t. a variable.]
905 Description [Computes the negative cofactor of a ZDD w.r.t. a
906 variable. In terms of combinations, the result is the set of all
907 combinations in which the variable is negated. Returns a pointer to
908 the result if successful; NULL otherwise. cuddZddSubset0 performs
909 the same function as Cudd_zddSubset0, but does not restart if
910 reordering has taken place. Therefore it can be called from within a
911 recursive procedure.]
915 SeeAlso [cuddZddSubset1 Cudd_zddSubset0]
917 ******************************************************************************/
925 DdNode
*base
, *empty
;
930 zvar
= cuddUniqueInterZdd(dd
, var
, base
, empty
);
935 r
= zdd_subset0_aux(dd
, P
, zvar
);
937 Cudd_RecursiveDerefZdd(dd
, zvar
);
941 Cudd_RecursiveDerefZdd(dd
, zvar
);
947 } /* end of cuddZddSubset0 */
950 /**Function********************************************************************
952 Synopsis [Substitutes a variable with its complement in a ZDD.]
954 Description [Substitutes a variable with its complement in a ZDD.
955 returns a pointer to the result if successful; NULL
956 otherwise. cuddZddChange performs the same function as
957 Cudd_zddChange, but does not restart if reordering has taken
958 place. Therefore it can be called from within a recursive
963 SeeAlso [Cudd_zddChange]
965 ******************************************************************************/
974 zvar
= cuddUniqueInterZdd(dd
, var
, DD_ONE(dd
), DD_ZERO(dd
));
975 if (zvar
== NULL
) return(NULL
);
978 res
= cuddZddChangeAux(dd
, P
, zvar
);
980 Cudd_RecursiveDerefZdd(dd
,zvar
);
984 Cudd_RecursiveDerefZdd(dd
,zvar
);
988 } /* end of cuddZddChange */
991 /*---------------------------------------------------------------------------*/
992 /* Definition of static functions */
993 /*---------------------------------------------------------------------------*/
996 /**Function********************************************************************
998 Synopsis [Performs the recursive step of Cudd_zddSubset1.]
1006 ******************************************************************************/
1014 DdNode
*res
, *t
, *e
;
1018 empty
= DD_ZERO(zdd
);
1021 res
= cuddCacheLookup2Zdd(zdd
, zdd_subset1_aux
, P
, zvar
);
1025 if (cuddIsConstant(P
)) {
1027 cuddCacheInsert2(zdd
, zdd_subset1_aux
, P
, zvar
, res
);
1031 top_var
= zdd
->permZ
[P
->index
];
1032 level
= zdd
->permZ
[zvar
->index
];
1034 if (top_var
> level
) {
1036 } else if (top_var
== level
) {
1039 t
= zdd_subset1_aux(zdd
, cuddT(P
), zvar
);
1040 if (t
== NULL
) return(NULL
);
1042 e
= zdd_subset1_aux(zdd
, cuddE(P
), zvar
);
1044 Cudd_RecursiveDerefZdd(zdd
, t
);
1048 res
= cuddZddGetNode(zdd
, P
->index
, t
, e
);
1050 Cudd_RecursiveDerefZdd(zdd
, t
);
1051 Cudd_RecursiveDerefZdd(zdd
, e
);
1058 cuddCacheInsert2(zdd
, zdd_subset1_aux
, P
, zvar
, res
);
1062 } /* end of zdd_subset1_aux */
1065 /**Function********************************************************************
1067 Synopsis [Performs the recursive step of Cudd_zddSubset0.]
1075 ******************************************************************************/
1083 DdNode
*res
, *t
, *e
;
1088 res
= cuddCacheLookup2Zdd(zdd
, zdd_subset0_aux
, P
, zvar
);
1092 if (cuddIsConstant(P
)) {
1094 cuddCacheInsert2(zdd
, zdd_subset0_aux
, P
, zvar
, res
);
1098 top_var
= zdd
->permZ
[P
->index
];
1099 level
= zdd
->permZ
[zvar
->index
];
1101 if (top_var
> level
) {
1104 else if (top_var
== level
) {
1108 t
= zdd_subset0_aux(zdd
, cuddT(P
), zvar
);
1109 if (t
== NULL
) return(NULL
);
1111 e
= zdd_subset0_aux(zdd
, cuddE(P
), zvar
);
1113 Cudd_RecursiveDerefZdd(zdd
, t
);
1117 res
= cuddZddGetNode(zdd
, P
->index
, t
, e
);
1119 Cudd_RecursiveDerefZdd(zdd
, t
);
1120 Cudd_RecursiveDerefZdd(zdd
, e
);
1127 cuddCacheInsert2(zdd
, zdd_subset0_aux
, P
, zvar
, res
);
1131 } /* end of zdd_subset0_aux */
1134 /**Function********************************************************************
1136 Synopsis [Replaces variables with constants if possible (part of
1145 ******************************************************************************/
1157 if (f
== g
) { /* ITE(F,F,H) = ITE(F,1,H) = F + H */
1161 if (f
== h
) { /* ITE(F,G,F) = ITE(F,G,0) = F * G */
1165 } /* end of zddVarToConst */