1 /**CFile***********************************************************************
3 FileName [cuddBddIte.c]
7 Synopsis [BDD ITE function and satellites.]
9 Description [External procedures included in this module:
12 <li> Cudd_bddIteConstant()
13 <li> Cudd_bddIntersect()
15 <li> Cudd_bddAndLimit()
23 Internal procedures included in this module:
25 <li> cuddBddIteRecur()
26 <li> cuddBddIntersectRecur()
27 <li> cuddBddAndRecur()
28 <li> cuddBddXorRecur()
30 Static procedures included in this module:
33 <li> bddVarToCanonical()
34 <li> bddVarToCanonicalSimple()
39 Author [Fabio Somenzi]
41 Copyright [Copyright (c) 1995-2004, Regents of the University of Colorado
45 Redistribution and use in source and binary forms, with or without
46 modification, are permitted provided that the following conditions
49 Redistributions of source code must retain the above copyright
50 notice, this list of conditions and the following disclaimer.
52 Redistributions in binary form must reproduce the above copyright
53 notice, this list of conditions and the following disclaimer in the
54 documentation and/or other materials provided with the distribution.
56 Neither the name of the University of Colorado nor the names of its
57 contributors may be used to endorse or promote products derived from
58 this software without specific prior written permission.
60 THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
61 "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
62 LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
63 FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
64 COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
65 INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
66 BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
67 LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
68 CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
69 LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
70 ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
71 POSSIBILITY OF SUCH DAMAGE.]
73 ******************************************************************************/
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: cuddBddIte.c,v 1.24 2004/08/13 18:04:46 fabio Exp $";
102 /*---------------------------------------------------------------------------*/
103 /* Macro declarations */
104 /*---------------------------------------------------------------------------*/
107 /**AutomaticStart*************************************************************/
109 /*---------------------------------------------------------------------------*/
110 /* Static function prototypes */
111 /*---------------------------------------------------------------------------*/
113 static void bddVarToConst (DdNode
*f
, DdNode
**gp
, DdNode
**hp
, DdNode
*one
);
114 static int bddVarToCanonical (DdManager
*dd
, DdNode
**fp
, DdNode
**gp
, DdNode
**hp
, unsigned int *topfp
, unsigned int *topgp
, unsigned int *tophp
);
115 static int bddVarToCanonicalSimple (DdManager
*dd
, DdNode
**fp
, DdNode
**gp
, DdNode
**hp
, unsigned int *topfp
, unsigned int *topgp
, unsigned int *tophp
);
117 /**AutomaticEnd***************************************************************/
120 /*---------------------------------------------------------------------------*/
121 /* Definition of exported functions */
122 /*---------------------------------------------------------------------------*/
125 /**Function********************************************************************
127 Synopsis [Implements ITE(f,g,h).]
129 Description [Implements ITE(f,g,h). Returns a pointer to the
130 resulting BDD if successful; NULL if the intermediate result blows
135 SeeAlso [Cudd_addIte Cudd_bddIteConstant Cudd_bddIntersect]
137 ******************************************************************************/
149 res
= cuddBddIteRecur(dd
,f
,g
,h
);
150 } while (dd
->reordered
== 1);
153 } /* end of Cudd_bddIte */
156 /**Function********************************************************************
158 Synopsis [Implements ITEconstant(f,g,h).]
160 Description [Implements ITEconstant(f,g,h). Returns a pointer to the
161 resulting BDD (which may or may not be constant) or DD_NON_CONSTANT.
162 No new nodes are created.]
166 SeeAlso [Cudd_bddIte Cudd_bddIntersect Cudd_bddLeq Cudd_addIteConstant]
168 ******************************************************************************/
176 DdNode
*r
, *Fv
, *Fnv
, *Gv
, *Gnv
, *H
, *Hv
, *Hnv
, *t
, *e
;
177 DdNode
*one
= DD_ONE(dd
);
178 DdNode
*zero
= Cudd_Not(one
);
180 unsigned int topf
, topg
, toph
, v
;
184 if (f
== one
) /* ITE(1,G,H) => G */
187 if (f
== zero
) /* ITE(0,G,H) => H */
190 /* f now not a constant. */
191 bddVarToConst(f
, &g
, &h
, one
); /* possibly convert g or h */
194 if (g
== h
) /* ITE(F,G,G) => G */
197 if (Cudd_IsConstant(g
) && Cudd_IsConstant(h
))
198 return(DD_NON_CONSTANT
); /* ITE(F,1,0) or ITE(F,0,1) */
199 /* => DD_NON_CONSTANT */
201 if (g
== Cudd_Not(h
))
202 return(DD_NON_CONSTANT
); /* ITE(F,G,G') => DD_NON_CONSTANT */
203 /* if F != G and F != G' */
205 comple
= bddVarToCanonical(dd
, &f
, &g
, &h
, &topf
, &topg
, &toph
);
208 r
= cuddConstantLookup(dd
, DD_BDD_ITE_CONSTANT_TAG
, f
, g
, h
);
210 return(Cudd_NotCond(r
,comple
&& r
!= DD_NON_CONSTANT
));
213 v
= ddMin(topg
, toph
);
215 /* ITE(F,G,H) = (v,G,H) (non constant) if F = (v,1,0), v < top(G,H). */
216 if (topf
< v
&& cuddT(f
) == one
&& cuddE(f
) == zero
) {
217 return(DD_NON_CONSTANT
);
220 /* Compute cofactors. */
222 v
= ddMin(topf
, v
); /* v = top_var(F,G,H) */
223 Fv
= cuddT(f
); Fnv
= cuddE(f
);
229 Gv
= cuddT(g
); Gnv
= cuddE(g
);
236 Hv
= cuddT(H
); Hnv
= cuddE(H
);
237 if (Cudd_IsComplement(h
)) {
246 t
= Cudd_bddIteConstant(dd
, Fv
, Gv
, Hv
);
247 if (t
== DD_NON_CONSTANT
|| !Cudd_IsConstant(t
)) {
248 cuddCacheInsert(dd
, DD_BDD_ITE_CONSTANT_TAG
, f
, g
, h
, DD_NON_CONSTANT
);
249 return(DD_NON_CONSTANT
);
251 e
= Cudd_bddIteConstant(dd
, Fnv
, Gnv
, Hnv
);
252 if (e
== DD_NON_CONSTANT
|| !Cudd_IsConstant(e
) || t
!= e
) {
253 cuddCacheInsert(dd
, DD_BDD_ITE_CONSTANT_TAG
, f
, g
, h
, DD_NON_CONSTANT
);
254 return(DD_NON_CONSTANT
);
256 cuddCacheInsert(dd
, DD_BDD_ITE_CONSTANT_TAG
, f
, g
, h
, t
);
257 return(Cudd_NotCond(t
,comple
));
259 } /* end of Cudd_bddIteConstant */
262 /**Function********************************************************************
264 Synopsis [Returns a function included in the intersection of f and g.]
266 Description [Computes a function included in the intersection of f and
267 g. (That is, a witness that the intersection is not empty.)
268 Cudd_bddIntersect tries to build as few new nodes as possible. If the
269 only result of interest is whether f and g intersect,
270 Cudd_bddLeq should be used instead.]
274 SeeAlso [Cudd_bddLeq Cudd_bddIteConstant]
276 ******************************************************************************/
279 DdManager
* dd
/* manager */,
280 DdNode
* f
/* first operand */,
281 DdNode
* g
/* second operand */)
287 res
= cuddBddIntersectRecur(dd
,f
,g
);
288 } while (dd
->reordered
== 1);
292 } /* end of Cudd_bddIntersect */
295 /**Function********************************************************************
297 Synopsis [Computes the conjunction of two BDDs f and g.]
299 Description [Computes the conjunction of two BDDs f and g. Returns a
300 pointer to the resulting BDD if successful; NULL if the intermediate
305 SeeAlso [Cudd_bddIte Cudd_addApply Cudd_bddAndAbstract Cudd_bddIntersect
306 Cudd_bddOr Cudd_bddNand Cudd_bddNor Cudd_bddXor Cudd_bddXnor]
308 ******************************************************************************/
319 res
= cuddBddAndRecur(dd
,f
,g
);
320 } while (dd
->reordered
== 1);
323 } /* end of Cudd_bddAnd */
326 /**Function********************************************************************
328 Synopsis [Computes the conjunction of two BDDs f and g. Returns
329 NULL if too many nodes are required.]
331 Description [Computes the conjunction of two BDDs f and g. Returns a
332 pointer to the resulting BDD if successful; NULL if the intermediate
333 result blows up or more new nodes than <code>limit</code> are
338 SeeAlso [Cudd_bddAnd]
340 ******************************************************************************/
349 unsigned int saveLimit
= dd
->maxLive
;
351 dd
->maxLive
= (dd
->keys
- dd
->dead
) + (dd
->keysZ
- dd
->deadZ
) + limit
;
354 res
= cuddBddAndRecur(dd
,f
,g
);
355 } while (dd
->reordered
== 1);
356 dd
->maxLive
= saveLimit
;
359 } /* end of Cudd_bddAndLimit */
362 /**Function********************************************************************
364 Synopsis [Computes the disjunction of two BDDs f and g.]
366 Description [Computes the disjunction of two BDDs f and g. Returns a
367 pointer to the resulting BDD if successful; NULL if the intermediate
372 SeeAlso [Cudd_bddIte Cudd_addApply Cudd_bddAnd Cudd_bddNand Cudd_bddNor
373 Cudd_bddXor Cudd_bddXnor]
375 ******************************************************************************/
386 res
= cuddBddAndRecur(dd
,Cudd_Not(f
),Cudd_Not(g
));
387 } while (dd
->reordered
== 1);
388 res
= Cudd_NotCond(res
,res
!= NULL
);
391 } /* end of Cudd_bddOr */
394 /**Function********************************************************************
396 Synopsis [Computes the NAND of two BDDs f and g.]
398 Description [Computes the NAND of two BDDs f and g. Returns a
399 pointer to the resulting BDD if successful; NULL if the intermediate
404 SeeAlso [Cudd_bddIte Cudd_addApply Cudd_bddAnd Cudd_bddOr Cudd_bddNor
405 Cudd_bddXor Cudd_bddXnor]
407 ******************************************************************************/
418 res
= cuddBddAndRecur(dd
,f
,g
);
419 } while (dd
->reordered
== 1);
420 res
= Cudd_NotCond(res
,res
!= NULL
);
423 } /* end of Cudd_bddNand */
426 /**Function********************************************************************
428 Synopsis [Computes the NOR of two BDDs f and g.]
430 Description [Computes the NOR of two BDDs f and g. Returns a
431 pointer to the resulting BDD if successful; NULL if the intermediate
436 SeeAlso [Cudd_bddIte Cudd_addApply Cudd_bddAnd Cudd_bddOr Cudd_bddNand
437 Cudd_bddXor Cudd_bddXnor]
439 ******************************************************************************/
450 res
= cuddBddAndRecur(dd
,Cudd_Not(f
),Cudd_Not(g
));
451 } while (dd
->reordered
== 1);
454 } /* end of Cudd_bddNor */
457 /**Function********************************************************************
459 Synopsis [Computes the exclusive OR of two BDDs f and g.]
461 Description [Computes the exclusive OR of two BDDs f and g. Returns a
462 pointer to the resulting BDD if successful; NULL if the intermediate
467 SeeAlso [Cudd_bddIte Cudd_addApply Cudd_bddAnd Cudd_bddOr
468 Cudd_bddNand Cudd_bddNor Cudd_bddXnor]
470 ******************************************************************************/
481 res
= cuddBddXorRecur(dd
,f
,g
);
482 } while (dd
->reordered
== 1);
485 } /* end of Cudd_bddXor */
488 /**Function********************************************************************
490 Synopsis [Computes the exclusive NOR of two BDDs f and g.]
492 Description [Computes the exclusive NOR of two BDDs f and g. Returns a
493 pointer to the resulting BDD if successful; NULL if the intermediate
498 SeeAlso [Cudd_bddIte Cudd_addApply Cudd_bddAnd Cudd_bddOr
499 Cudd_bddNand Cudd_bddNor Cudd_bddXor]
501 ******************************************************************************/
512 res
= cuddBddXorRecur(dd
,f
,Cudd_Not(g
));
513 } while (dd
->reordered
== 1);
516 } /* end of Cudd_bddXnor */
519 /**Function********************************************************************
521 Synopsis [Determines whether f is less than or equal to g.]
523 Description [Returns 1 if f is less than or equal to g; 0 otherwise.
524 No new nodes are created.]
528 SeeAlso [Cudd_bddIteConstant Cudd_addEvalConst]
530 ******************************************************************************/
537 DdNode
*one
, *zero
, *tmp
, *F
, *fv
, *fvn
, *gv
, *gvn
;
538 unsigned int topf
, topg
, res
;
541 /* Terminal cases and normalization. */
542 if (f
== g
) return(1);
544 if (Cudd_IsComplement(g
)) {
545 /* Special case: if f is regular and g is complemented,
546 ** f(1,...,1) = 1 > 0 = g(1,...,1).
548 if (!Cudd_IsComplement(f
)) return(0);
549 /* Both are complemented: Swap and complement because
550 ** f <= g <=> g' <= f' and we want the second argument to be regular.
555 } else if (Cudd_IsComplement(f
) && g
< f
) {
561 /* Now g is regular and, if f is not regular, f < g. */
563 if (g
== one
) return(1); /* no need to test against zero */
564 if (f
== one
) return(0); /* since at this point g != one */
565 if (Cudd_Not(f
) == g
) return(0); /* because neither is constant */
566 zero
= Cudd_Not(one
);
567 if (f
== zero
) return(1);
569 /* Here neither f nor g is constant. */
572 tmp
= cuddCacheLookup2(dd
,(DD_CTFP
)Cudd_bddLeq
,f
,g
);
577 /* Compute cofactors. */
579 topf
= dd
->perm
[F
->index
];
580 topg
= dd
->perm
[g
->index
];
582 fv
= cuddT(F
); fvn
= cuddE(F
);
591 gv
= cuddT(g
); gvn
= cuddE(g
);
596 /* Recursive calls. Since we want to maximize the probability of
597 ** the special case f(1,...,1) > g(1,...,1), we consider the negative
598 ** cofactors first. Indeed, the complementation parity of the positive
599 ** cofactors is the same as the one of the parent functions.
601 res
= Cudd_bddLeq(dd
,fvn
,gvn
) && Cudd_bddLeq(dd
,fv
,gv
);
603 /* Store result in cache and return. */
604 cuddCacheInsert2(dd
,(DD_CTFP
)Cudd_bddLeq
,f
,g
,(res
? one
: zero
));
607 } /* end of Cudd_bddLeq */
610 /*---------------------------------------------------------------------------*/
611 /* Definition of internal functions */
612 /*---------------------------------------------------------------------------*/
615 /**Function********************************************************************
617 Synopsis [Implements the recursive step of Cudd_bddIte.]
619 Description [Implements the recursive step of Cudd_bddIte. Returns a
620 pointer to the resulting BDD. NULL if the intermediate result blows
621 up or if reordering occurs.]
627 ******************************************************************************/
635 DdNode
*one
, *zero
, *res
;
636 DdNode
*r
, *Fv
, *Fnv
, *Gv
, *Gnv
, *H
, *Hv
, *Hnv
, *t
, *e
;
637 unsigned int topf
, topg
, toph
, v
;
642 /* Terminal cases. */
644 /* One variable cases. */
645 if (f
== (one
= DD_ONE(dd
))) /* ITE(1,G,H) = G */
648 if (f
== (zero
= Cudd_Not(one
))) /* ITE(0,G,H) = H */
651 /* From now on, f is known not to be a constant. */
652 if (g
== one
|| f
== g
) { /* ITE(F,F,H) = ITE(F,1,H) = F + H */
653 if (h
== zero
) { /* ITE(F,1,0) = F */
656 res
= cuddBddAndRecur(dd
,Cudd_Not(f
),Cudd_Not(h
));
657 return(Cudd_NotCond(res
,res
!= NULL
));
659 } else if (g
== zero
|| f
== Cudd_Not(g
)) { /* ITE(F,!F,H) = ITE(F,0,H) = !F * H */
660 if (h
== one
) { /* ITE(F,0,1) = !F */
663 res
= cuddBddAndRecur(dd
,Cudd_Not(f
),h
);
667 if (h
== zero
|| f
== h
) { /* ITE(F,G,F) = ITE(F,G,0) = F * G */
668 res
= cuddBddAndRecur(dd
,f
,g
);
670 } else if (h
== one
|| f
== Cudd_Not(h
)) { /* ITE(F,G,!F) = ITE(F,G,1) = !F + G */
671 res
= cuddBddAndRecur(dd
,f
,Cudd_Not(g
));
672 return(Cudd_NotCond(res
,res
!= NULL
));
675 /* Check remaining one variable case. */
676 if (g
== h
) { /* ITE(F,G,G) = G */
678 } else if (g
== Cudd_Not(h
)) { /* ITE(F,G,!G) = F <-> G */
679 res
= cuddBddXorRecur(dd
,f
,h
);
683 /* From here, there are no constants. */
684 comple
= bddVarToCanonicalSimple(dd
, &f
, &g
, &h
, &topf
, &topg
, &toph
);
686 /* f & g are now regular pointers */
688 v
= ddMin(topg
, toph
);
690 /* A shortcut: ITE(F,G,H) = (v,G,H) if F = (v,1,0), v < top(G,H). */
691 if (topf
< v
&& cuddT(f
) == one
&& cuddE(f
) == zero
) {
692 r
= cuddUniqueInter(dd
, (int) f
->index
, g
, h
);
693 return(Cudd_NotCond(r
,comple
&& r
!= NULL
));
697 r
= cuddCacheLookup(dd
, DD_BDD_ITE_TAG
, f
, g
, h
);
699 return(Cudd_NotCond(r
,comple
));
702 /* Compute cofactors. */
704 v
= ddMin(topf
, v
); /* v = top_var(F,G,H) */
706 Fv
= cuddT(f
); Fnv
= cuddE(f
);
712 Gv
= cuddT(g
); Gnv
= cuddE(g
);
719 Hv
= cuddT(H
); Hnv
= cuddE(H
);
720 if (Cudd_IsComplement(h
)) {
728 /* Recursive step. */
729 t
= cuddBddIteRecur(dd
,Fv
,Gv
,Hv
);
730 if (t
== NULL
) return(NULL
);
733 e
= cuddBddIteRecur(dd
,Fnv
,Gnv
,Hnv
);
735 Cudd_IterDerefBdd(dd
,t
);
740 r
= (t
== e
) ? t
: cuddUniqueInter(dd
,index
,t
,e
);
742 Cudd_IterDerefBdd(dd
,t
);
743 Cudd_IterDerefBdd(dd
,e
);
749 cuddCacheInsert(dd
, DD_BDD_ITE_TAG
, f
, g
, h
, r
);
750 return(Cudd_NotCond(r
,comple
));
752 } /* end of cuddBddIteRecur */
755 /**Function********************************************************************
757 Synopsis [Implements the recursive step of Cudd_bddIntersect.]
763 SeeAlso [Cudd_bddIntersect]
765 ******************************************************************************/
767 cuddBddIntersectRecur(
773 DdNode
*F
, *G
, *t
, *e
;
774 DdNode
*fv
, *fnv
, *gv
, *gnv
;
776 unsigned int index
, topf
, topg
;
780 zero
= Cudd_Not(one
);
782 /* Terminal cases. */
783 if (f
== zero
|| g
== zero
|| f
== Cudd_Not(g
)) return(zero
);
784 if (f
== g
|| g
== one
) return(f
);
785 if (f
== one
) return(g
);
787 /* At this point f and g are not constant. */
788 if (f
> g
) { DdNode
*tmp
= f
; f
= g
; g
= tmp
; }
789 res
= cuddCacheLookup2(dd
,Cudd_bddIntersect
,f
,g
);
790 if (res
!= NULL
) return(res
);
792 /* Find splitting variable. Here we can skip the use of cuddI,
793 ** because the operands are known to be non-constant.
796 topf
= dd
->perm
[F
->index
];
798 topg
= dd
->perm
[G
->index
];
800 /* Compute cofactors. */
805 if (Cudd_IsComplement(f
)) {
817 if (Cudd_IsComplement(g
)) {
825 /* Compute partial results. */
826 t
= cuddBddIntersectRecur(dd
,fv
,gv
);
827 if (t
== NULL
) return(NULL
);
832 e
= cuddBddIntersectRecur(dd
,fnv
,gnv
);
834 Cudd_IterDerefBdd(dd
, t
);
840 if (t
== e
) { /* both equal zero */
842 } else if (Cudd_IsComplement(t
)) {
843 res
= cuddUniqueInter(dd
,(int)index
,Cudd_Not(t
),Cudd_Not(e
));
845 Cudd_IterDerefBdd(dd
, t
);
846 Cudd_IterDerefBdd(dd
, e
);
851 res
= cuddUniqueInter(dd
,(int)index
,t
,e
);
853 Cudd_IterDerefBdd(dd
, t
);
854 Cudd_IterDerefBdd(dd
, e
);
861 cuddCacheInsert2(dd
,Cudd_bddIntersect
,f
,g
,res
);
865 } /* end of cuddBddIntersectRecur */
868 /**Function********************************************************************
870 Synopsis [Implements the recursive step of Cudd_bddAnd.]
872 Description [Implements the recursive step of Cudd_bddAnd by taking
873 the conjunction of two BDDs. Returns a pointer to the result is
874 successful; NULL otherwise.]
878 SeeAlso [Cudd_bddAnd]
880 ******************************************************************************/
887 DdNode
*F
, *fv
, *fnv
, *G
, *gv
, *gnv
;
888 DdNode
*one
, *r
, *t
, *e
;
889 unsigned int topf
, topg
, index
;
892 one
= DD_ONE(manager
);
894 /* Terminal cases. */
898 if (f
== g
) return(f
);
899 else return(Cudd_Not(one
));
902 if (f
== one
) return(g
);
906 if (g
== one
) return(f
);
910 /* At this point f and g are not constant. */
911 if (f
> g
) { /* Try to increase cache efficiency. */
920 if (F
->ref
!= 1 || G
->ref
!= 1) {
921 r
= cuddCacheLookup2(manager
, Cudd_bddAnd
, f
, g
);
922 if (r
!= NULL
) return(r
);
925 /* Here we can skip the use of cuddI, because the operands are known
926 ** to be non-constant.
928 topf
= manager
->perm
[F
->index
];
929 topg
= manager
->perm
[G
->index
];
931 /* Compute cofactors. */
936 if (Cudd_IsComplement(f
)) {
948 if (Cudd_IsComplement(g
)) {
956 t
= cuddBddAndRecur(manager
, fv
, gv
);
957 if (t
== NULL
) return(NULL
);
960 e
= cuddBddAndRecur(manager
, fnv
, gnv
);
962 Cudd_IterDerefBdd(manager
, t
);
970 if (Cudd_IsComplement(t
)) {
971 r
= cuddUniqueInter(manager
,(int)index
,Cudd_Not(t
),Cudd_Not(e
));
973 Cudd_IterDerefBdd(manager
, t
);
974 Cudd_IterDerefBdd(manager
, e
);
979 r
= cuddUniqueInter(manager
,(int)index
,t
,e
);
981 Cudd_IterDerefBdd(manager
, t
);
982 Cudd_IterDerefBdd(manager
, e
);
989 if (F
->ref
!= 1 || G
->ref
!= 1)
990 cuddCacheInsert2(manager
, Cudd_bddAnd
, f
, g
, r
);
993 } /* end of cuddBddAndRecur */
996 /**Function********************************************************************
998 Synopsis [Implements the recursive step of Cudd_bddXor.]
1000 Description [Implements the recursive step of Cudd_bddXor by taking
1001 the exclusive OR of two BDDs. Returns a pointer to the result is
1002 successful; NULL otherwise.]
1006 SeeAlso [Cudd_bddXor]
1008 ******************************************************************************/
1011 DdManager
* manager
,
1015 DdNode
*fv
, *fnv
, *G
, *gv
, *gnv
;
1016 DdNode
*one
, *zero
, *r
, *t
, *e
;
1017 unsigned int topf
, topg
, index
;
1020 one
= DD_ONE(manager
);
1021 zero
= Cudd_Not(one
);
1023 /* Terminal cases. */
1024 if (f
== g
) return(zero
);
1025 if (f
== Cudd_Not(g
)) return(one
);
1026 if (f
> g
) { /* Try to increase cache efficiency and simplify tests. */
1031 if (g
== zero
) return(f
);
1032 if (g
== one
) return(Cudd_Not(f
));
1033 if (Cudd_IsComplement(f
)) {
1037 /* Now the first argument is regular. */
1038 if (f
== one
) return(Cudd_Not(g
));
1040 /* At this point f and g are not constant. */
1043 r
= cuddCacheLookup2(manager
, Cudd_bddXor
, f
, g
);
1044 if (r
!= NULL
) return(r
);
1046 /* Here we can skip the use of cuddI, because the operands are known
1047 ** to be non-constant.
1049 topf
= manager
->perm
[f
->index
];
1050 G
= Cudd_Regular(g
);
1051 topg
= manager
->perm
[G
->index
];
1053 /* Compute cofactors. */
1066 if (Cudd_IsComplement(g
)) {
1068 gnv
= Cudd_Not(gnv
);
1074 t
= cuddBddXorRecur(manager
, fv
, gv
);
1075 if (t
== NULL
) return(NULL
);
1078 e
= cuddBddXorRecur(manager
, fnv
, gnv
);
1080 Cudd_IterDerefBdd(manager
, t
);
1088 if (Cudd_IsComplement(t
)) {
1089 r
= cuddUniqueInter(manager
,(int)index
,Cudd_Not(t
),Cudd_Not(e
));
1091 Cudd_IterDerefBdd(manager
, t
);
1092 Cudd_IterDerefBdd(manager
, e
);
1097 r
= cuddUniqueInter(manager
,(int)index
,t
,e
);
1099 Cudd_IterDerefBdd(manager
, t
);
1100 Cudd_IterDerefBdd(manager
, e
);
1107 cuddCacheInsert2(manager
, Cudd_bddXor
, f
, g
, r
);
1110 } /* end of cuddBddXorRecur */
1113 /*---------------------------------------------------------------------------*/
1114 /* Definition of static functions */
1115 /*---------------------------------------------------------------------------*/
1118 /**Function********************************************************************
1120 Synopsis [Replaces variables with constants if possible.]
1122 Description [This function performs part of the transformation to
1123 standard form by replacing variables with constants if possible.]
1127 SeeAlso [bddVarToCanonical bddVarToCanonicalSimple]
1129 ******************************************************************************/
1140 if (f
== g
) { /* ITE(F,F,H) = ITE(F,1,H) = F + H */
1142 } else if (f
== Cudd_Not(g
)) { /* ITE(F,!F,H) = ITE(F,0,H) = !F * H */
1143 *gp
= Cudd_Not(one
);
1145 if (f
== h
) { /* ITE(F,G,F) = ITE(F,G,0) = F * G */
1146 *hp
= Cudd_Not(one
);
1147 } else if (f
== Cudd_Not(h
)) { /* ITE(F,G,!F) = ITE(F,G,1) = !F + G */
1151 } /* end of bddVarToConst */
1154 /**Function********************************************************************
1156 Synopsis [Picks unique member from equiv expressions.]
1158 Description [Reduces 2 variable expressions to canonical form.]
1162 SeeAlso [bddVarToConst bddVarToCanonicalSimple]
1164 ******************************************************************************/
1171 unsigned int * topfp
,
1172 unsigned int * topgp
,
1173 unsigned int * tophp
)
1175 register DdNode
*F
, *G
, *H
, *r
, *f
, *g
, *h
;
1176 register unsigned int topf
, topg
, toph
;
1177 DdNode
*one
= dd
->one
;
1183 F
= Cudd_Regular(f
);
1184 G
= Cudd_Regular(g
);
1185 H
= Cudd_Regular(h
);
1186 topf
= cuddI(dd
,F
->index
);
1187 topg
= cuddI(dd
,G
->index
);
1188 toph
= cuddI(dd
,H
->index
);
1192 if (G
== one
) { /* ITE(F,c,H) */
1193 if ((topf
> toph
) || (topf
== toph
&& f
> h
)) {
1196 f
= r
; /* ITE(F,1,H) = ITE(H,1,F) */
1197 if (g
!= one
) { /* g == zero */
1198 f
= Cudd_Not(f
); /* ITE(F,0,H) = ITE(!H,0,!F) */
1203 } else if (H
== one
) { /* ITE(F,G,c) */
1204 if ((topf
> topg
) || (topf
== topg
&& f
> g
)) {
1207 f
= r
; /* ITE(F,G,0) = ITE(G,F,0) */
1209 f
= Cudd_Not(f
); /* ITE(F,G,1) = ITE(!G,!F,1) */
1214 } else if (g
== Cudd_Not(h
)) { /* ITE(F,G,!G) = ITE(G,F,!F) */
1215 if ((topf
> topg
) || (topf
== topg
&& f
> g
)) {
1223 /* adjust pointers so that the first 2 arguments to ITE are regular */
1224 if (Cudd_IsComplement(f
) != 0) { /* ITE(!F,G,H) = ITE(F,H,G) */
1232 if (Cudd_IsComplement(g
) != 0) { /* ITE(F,!G,H) = !ITE(F,G,!H) */
1243 *topfp
= cuddI(dd
,f
->index
);
1244 *topgp
= cuddI(dd
,g
->index
);
1245 *tophp
= cuddI(dd
,Cudd_Regular(h
)->index
);
1249 } /* end of bddVarToCanonical */
1252 /**Function********************************************************************
1254 Synopsis [Picks unique member from equiv expressions.]
1256 Description [Makes sure the first two pointers are regular. This
1257 mat require the complementation of the result, which is signaled by
1258 returning 1 instead of 0. This function is simpler than the general
1259 case because it assumes that no two arguments are the same or
1260 complementary, and no argument is constant.]
1264 SeeAlso [bddVarToConst bddVarToCanonical]
1266 ******************************************************************************/
1268 bddVarToCanonicalSimple(
1273 unsigned int * topfp
,
1274 unsigned int * topgp
,
1275 unsigned int * tophp
)
1277 register DdNode
*r
, *f
, *g
, *h
;
1286 /* adjust pointers so that the first 2 arguments to ITE are regular */
1287 if (Cudd_IsComplement(f
)) { /* ITE(!F,G,H) = ITE(F,H,G) */
1295 if (Cudd_IsComplement(g
)) { /* ITE(F,!G,H) = !ITE(F,G,!H) */
1307 /* Here we can skip the use of cuddI, because the operands are known
1308 ** to be non-constant.
1310 *topfp
= dd
->perm
[f
->index
];
1311 *topgp
= dd
->perm
[g
->index
];
1312 *tophp
= dd
->perm
[Cudd_Regular(h
)->index
];
1316 } /* end of bddVarToCanonicalSimple */