1 /**CFile***********************************************************************
3 FileName [cuddBridge.c]
7 Synopsis [Translation from BDD to ADD and vice versa and transfer between
10 Description [External procedures included in this file:
12 <li> Cudd_addBddThreshold()
13 <li> Cudd_addBddStrictThreshold()
14 <li> Cudd_addBddInterval()
15 <li> Cudd_addBddIthBit()
17 <li> Cudd_addBddPattern()
18 <li> Cudd_bddTransfer()
20 Internal procedures included in this file:
22 <li> cuddBddTransfer()
23 <li> cuddAddBddDoPattern()
25 Static procedures included in this file:
27 <li> addBddDoThreshold()
28 <li> addBddDoStrictThreshold()
29 <li> addBddDoInterval()
31 <li> ddBddToAddRecur()
32 <li> cuddBddTransferRecur()
38 Author [Fabio Somenzi]
40 Copyright [Copyright (c) 1995-2004, Regents of the University of Colorado
44 Redistribution and use in source and binary forms, with or without
45 modification, are permitted provided that the following conditions
48 Redistributions of source code must retain the above copyright
49 notice, this list of conditions and the following disclaimer.
51 Redistributions in binary form must reproduce the above copyright
52 notice, this list of conditions and the following disclaimer in the
53 documentation and/or other materials provided with the distribution.
55 Neither the name of the University of Colorado nor the names of its
56 contributors may be used to endorse or promote products derived from
57 this software without specific prior written permission.
59 THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
60 "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
61 LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
62 FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
63 COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
64 INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
65 BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
66 LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
67 CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
68 LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
69 ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
70 POSSIBILITY OF SUCH DAMAGE.]
72 ******************************************************************************/
77 /*---------------------------------------------------------------------------*/
78 /* Constant declarations */
79 /*---------------------------------------------------------------------------*/
82 /*---------------------------------------------------------------------------*/
83 /* Stucture declarations */
84 /*---------------------------------------------------------------------------*/
87 /*---------------------------------------------------------------------------*/
88 /* Type declarations */
89 /*---------------------------------------------------------------------------*/
92 /*---------------------------------------------------------------------------*/
93 /* Variable declarations */
94 /*---------------------------------------------------------------------------*/
97 static char rcsid
[] DD_UNUSED
= "$Id: cuddBridge.c,v 1.19 2008/04/25 06:42:55 fabio Exp $";
100 /*---------------------------------------------------------------------------*/
101 /* Macro declarations */
102 /*---------------------------------------------------------------------------*/
109 /**AutomaticStart*************************************************************/
111 /*---------------------------------------------------------------------------*/
112 /* Static function prototypes */
113 /*---------------------------------------------------------------------------*/
115 static DdNode
* addBddDoThreshold (DdManager
*dd
, DdNode
*f
, DdNode
*val
);
116 static DdNode
* addBddDoStrictThreshold (DdManager
*dd
, DdNode
*f
, DdNode
*val
);
117 static DdNode
* addBddDoInterval (DdManager
*dd
, DdNode
*f
, DdNode
*l
, DdNode
*u
);
118 static DdNode
* addBddDoIthBit (DdManager
*dd
, DdNode
*f
, DdNode
*index
);
119 static DdNode
* ddBddToAddRecur (DdManager
*dd
, DdNode
*B
);
120 static DdNode
* cuddBddTransferRecur (DdManager
*ddS
, DdManager
*ddD
, DdNode
*f
, st_table
*table
);
122 /**AutomaticEnd***************************************************************/
129 /*---------------------------------------------------------------------------*/
130 /* Definition of exported functions */
131 /*---------------------------------------------------------------------------*/
134 /**Function********************************************************************
136 Synopsis [Converts an ADD to a BDD.]
138 Description [Converts an ADD to a BDD by replacing all
139 discriminants greater than or equal to value with 1, and all other
140 discriminants with 0. Returns a pointer to the resulting BDD if
141 successful; NULL otherwise.]
145 SeeAlso [Cudd_addBddInterval Cudd_addBddPattern Cudd_BddToAdd
146 Cudd_addBddStrictThreshold]
148 ******************************************************************************/
150 Cudd_addBddThreshold(
153 CUDD_VALUE_TYPE value
)
158 val
= cuddUniqueConst(dd
,value
);
159 if (val
== NULL
) return(NULL
);
164 res
= addBddDoThreshold(dd
, f
, val
);
165 } while (dd
->reordered
== 1);
168 Cudd_RecursiveDeref(dd
, val
);
172 Cudd_RecursiveDeref(dd
, val
);
176 } /* end of Cudd_addBddThreshold */
179 /**Function********************************************************************
181 Synopsis [Converts an ADD to a BDD.]
183 Description [Converts an ADD to a BDD by replacing all
184 discriminants STRICTLY greater than value with 1, and all other
185 discriminants with 0. Returns a pointer to the resulting BDD if
186 successful; NULL otherwise.]
190 SeeAlso [Cudd_addBddInterval Cudd_addBddPattern Cudd_BddToAdd
191 Cudd_addBddThreshold]
193 ******************************************************************************/
195 Cudd_addBddStrictThreshold(
198 CUDD_VALUE_TYPE value
)
203 val
= cuddUniqueConst(dd
,value
);
204 if (val
== NULL
) return(NULL
);
209 res
= addBddDoStrictThreshold(dd
, f
, val
);
210 } while (dd
->reordered
== 1);
213 Cudd_RecursiveDeref(dd
, val
);
217 Cudd_RecursiveDeref(dd
, val
);
221 } /* end of Cudd_addBddStrictThreshold */
224 /**Function********************************************************************
226 Synopsis [Converts an ADD to a BDD.]
228 Description [Converts an ADD to a BDD by replacing all
229 discriminants greater than or equal to lower and less than or equal to
230 upper with 1, and all other discriminants with 0. Returns a pointer to
231 the resulting BDD if successful; NULL otherwise.]
235 SeeAlso [Cudd_addBddThreshold Cudd_addBddStrictThreshold
236 Cudd_addBddPattern Cudd_BddToAdd]
238 ******************************************************************************/
243 CUDD_VALUE_TYPE lower
,
244 CUDD_VALUE_TYPE upper
)
250 /* Create constant nodes for the interval bounds, so that we can use
253 l
= cuddUniqueConst(dd
,lower
);
254 if (l
== NULL
) return(NULL
);
256 u
= cuddUniqueConst(dd
,upper
);
258 Cudd_RecursiveDeref(dd
,l
);
265 res
= addBddDoInterval(dd
, f
, l
, u
);
266 } while (dd
->reordered
== 1);
269 Cudd_RecursiveDeref(dd
, l
);
270 Cudd_RecursiveDeref(dd
, u
);
274 Cudd_RecursiveDeref(dd
, l
);
275 Cudd_RecursiveDeref(dd
, u
);
279 } /* end of Cudd_addBddInterval */
282 /**Function********************************************************************
284 Synopsis [Converts an ADD to a BDD by extracting the i-th bit from
287 Description [Converts an ADD to a BDD by replacing all
288 discriminants whose i-th bit is equal to 1 with 1, and all other
289 discriminants with 0. The i-th bit refers to the integer
290 representation of the leaf value. If the value is has a fractional
291 part, it is ignored. Repeated calls to this procedure allow one to
292 transform an integer-valued ADD into an array of BDDs, one for each
293 bit of the leaf values. Returns a pointer to the resulting BDD if
294 successful; NULL otherwise.]
298 SeeAlso [Cudd_addBddInterval Cudd_addBddPattern Cudd_BddToAdd]
300 ******************************************************************************/
310 index
= cuddUniqueConst(dd
,(CUDD_VALUE_TYPE
) bit
);
311 if (index
== NULL
) return(NULL
);
316 res
= addBddDoIthBit(dd
, f
, index
);
317 } while (dd
->reordered
== 1);
320 Cudd_RecursiveDeref(dd
, index
);
324 Cudd_RecursiveDeref(dd
, index
);
328 } /* end of Cudd_addBddIthBit */
331 /**Function********************************************************************
333 Synopsis [Converts a BDD to a 0-1 ADD.]
335 Description [Converts a BDD to a 0-1 ADD. Returns a pointer to the
336 resulting ADD if successful; NULL otherwise.]
340 SeeAlso [Cudd_addBddPattern Cudd_addBddThreshold Cudd_addBddInterval
341 Cudd_addBddStrictThreshold]
343 ******************************************************************************/
353 res
= ddBddToAddRecur(dd
, B
);
354 } while (dd
->reordered
==1);
357 } /* end of Cudd_BddToAdd */
360 /**Function********************************************************************
362 Synopsis [Converts an ADD to a BDD.]
364 Description [Converts an ADD to a BDD by replacing all
365 discriminants different from 0 with 1. Returns a pointer to the
366 resulting BDD if successful; NULL otherwise.]
370 SeeAlso [Cudd_BddToAdd Cudd_addBddThreshold Cudd_addBddInterval
371 Cudd_addBddStrictThreshold]
373 ******************************************************************************/
383 res
= cuddAddBddDoPattern(dd
, f
);
384 } while (dd
->reordered
== 1);
387 } /* end of Cudd_addBddPattern */
390 /**Function********************************************************************
392 Synopsis [Convert a BDD from a manager to another one.]
394 Description [Convert a BDD from a manager to another one. The orders of the
395 variables in the two managers may be different. Returns a
396 pointer to the BDD in the destination manager if successful; NULL
403 ******************************************************************************/
406 DdManager
* ddSource
,
407 DdManager
* ddDestination
,
412 ddDestination
->reordered
= 0;
413 res
= cuddBddTransfer(ddSource
, ddDestination
, f
);
414 } while (ddDestination
->reordered
== 1);
417 } /* end of Cudd_bddTransfer */
420 /*---------------------------------------------------------------------------*/
421 /* Definition of internal functions */
422 /*---------------------------------------------------------------------------*/
425 /**Function********************************************************************
427 Synopsis [Convert a BDD from a manager to another one.]
429 Description [Convert a BDD from a manager to another one. Returns a
430 pointer to the BDD in the destination manager if successful; NULL
435 SeeAlso [Cudd_bddTransfer]
437 ******************************************************************************/
445 st_table
*table
= NULL
;
446 st_generator
*gen
= NULL
;
449 table
= st_init_table(st_ptrcmp
,st_ptrhash
);
450 if (table
== NULL
) goto failure
;
451 res
= cuddBddTransferRecur(ddS
, ddD
, f
, table
);
452 if (res
!= NULL
) cuddRef(res
);
454 /* Dereference all elements in the table and dispose of the table.
455 ** This must be done also if res is NULL to avoid leaks in case of
457 gen
= st_init_gen(table
);
458 if (gen
== NULL
) goto failure
;
459 while (st_gen(gen
, &key
, &value
)) {
460 Cudd_RecursiveDeref(ddD
, value
);
462 st_free_gen(gen
); gen
= NULL
;
463 st_free_table(table
); table
= NULL
;
465 if (res
!= NULL
) cuddDeref(res
);
469 /* No need to free gen because it is always NULL here. */
470 if (table
!= NULL
) st_free_table(table
);
473 } /* end of cuddBddTransfer */
476 /**Function********************************************************************
478 Synopsis [Performs the recursive step for Cudd_addBddPattern.]
480 Description [Performs the recursive step for Cudd_addBddPattern. Returns a
481 pointer to the resulting BDD if successful; NULL otherwise.]
487 ******************************************************************************/
498 /* Check terminal case. */
499 if (cuddIsConstant(f
)) {
500 return(Cudd_NotCond(DD_ONE(dd
),f
== DD_ZERO(dd
)));
504 res
= cuddCacheLookup1(dd
,Cudd_addBddPattern
,f
);
505 if (res
!= NULL
) return(res
);
507 /* Recursive step. */
509 fv
= cuddT(f
); fvn
= cuddE(f
);
511 T
= cuddAddBddDoPattern(dd
,fv
);
512 if (T
== NULL
) return(NULL
);
515 E
= cuddAddBddDoPattern(dd
,fvn
);
517 Cudd_RecursiveDeref(dd
, T
);
521 if (Cudd_IsComplement(T
)) {
522 res
= (T
== E
) ? Cudd_Not(T
) : cuddUniqueInter(dd
,v
,Cudd_Not(T
),Cudd_Not(E
));
524 Cudd_RecursiveDeref(dd
, T
);
525 Cudd_RecursiveDeref(dd
, E
);
530 res
= (T
== E
) ? T
: cuddUniqueInter(dd
,v
,T
,E
);
532 Cudd_RecursiveDeref(dd
, T
);
533 Cudd_RecursiveDeref(dd
, E
);
541 cuddCacheInsert1(dd
,Cudd_addBddPattern
,f
,res
);
545 } /* end of cuddAddBddDoPattern */
548 /*---------------------------------------------------------------------------*/
549 /* Definition of static functions */
550 /*---------------------------------------------------------------------------*/
553 /**Function********************************************************************
555 Synopsis [Performs the recursive step for Cudd_addBddThreshold.]
557 Description [Performs the recursive step for Cudd_addBddThreshold.
558 Returns a pointer to the BDD if successful; NULL otherwise.]
562 SeeAlso [addBddDoStrictThreshold]
564 ******************************************************************************/
576 /* Check terminal case. */
577 if (cuddIsConstant(f
)) {
578 return(Cudd_NotCond(DD_ONE(dd
),cuddV(f
) < cuddV(val
)));
582 res
= cuddCacheLookup2(dd
,addBddDoThreshold
,f
,val
);
583 if (res
!= NULL
) return(res
);
585 /* Recursive step. */
587 fv
= cuddT(f
); fvn
= cuddE(f
);
589 T
= addBddDoThreshold(dd
,fv
,val
);
590 if (T
== NULL
) return(NULL
);
593 E
= addBddDoThreshold(dd
,fvn
,val
);
595 Cudd_RecursiveDeref(dd
, T
);
599 if (Cudd_IsComplement(T
)) {
600 res
= (T
== E
) ? Cudd_Not(T
) : cuddUniqueInter(dd
,v
,Cudd_Not(T
),Cudd_Not(E
));
602 Cudd_RecursiveDeref(dd
, T
);
603 Cudd_RecursiveDeref(dd
, E
);
608 res
= (T
== E
) ? T
: cuddUniqueInter(dd
,v
,T
,E
);
610 Cudd_RecursiveDeref(dd
, T
);
611 Cudd_RecursiveDeref(dd
, E
);
619 cuddCacheInsert2(dd
,addBddDoThreshold
,f
,val
,res
);
623 } /* end of addBddDoThreshold */
626 /**Function********************************************************************
628 Synopsis [Performs the recursive step for Cudd_addBddStrictThreshold.]
630 Description [Performs the recursive step for Cudd_addBddStrictThreshold.
631 Returns a pointer to the BDD if successful; NULL otherwise.]
635 SeeAlso [addBddDoThreshold]
637 ******************************************************************************/
639 addBddDoStrictThreshold(
649 /* Check terminal case. */
650 if (cuddIsConstant(f
)) {
651 return(Cudd_NotCond(DD_ONE(dd
),cuddV(f
) <= cuddV(val
)));
655 res
= cuddCacheLookup2(dd
,addBddDoStrictThreshold
,f
,val
);
656 if (res
!= NULL
) return(res
);
658 /* Recursive step. */
660 fv
= cuddT(f
); fvn
= cuddE(f
);
662 T
= addBddDoStrictThreshold(dd
,fv
,val
);
663 if (T
== NULL
) return(NULL
);
666 E
= addBddDoStrictThreshold(dd
,fvn
,val
);
668 Cudd_RecursiveDeref(dd
, T
);
672 if (Cudd_IsComplement(T
)) {
673 res
= (T
== E
) ? Cudd_Not(T
) : cuddUniqueInter(dd
,v
,Cudd_Not(T
),Cudd_Not(E
));
675 Cudd_RecursiveDeref(dd
, T
);
676 Cudd_RecursiveDeref(dd
, E
);
681 res
= (T
== E
) ? T
: cuddUniqueInter(dd
,v
,T
,E
);
683 Cudd_RecursiveDeref(dd
, T
);
684 Cudd_RecursiveDeref(dd
, E
);
692 cuddCacheInsert2(dd
,addBddDoStrictThreshold
,f
,val
,res
);
696 } /* end of addBddDoStrictThreshold */
699 /**Function********************************************************************
701 Synopsis [Performs the recursive step for Cudd_addBddInterval.]
703 Description [Performs the recursive step for Cudd_addBddInterval.
704 Returns a pointer to the BDD if successful; NULL otherwise.]
708 SeeAlso [addBddDoThreshold addBddDoStrictThreshold]
710 ******************************************************************************/
723 /* Check terminal case. */
724 if (cuddIsConstant(f
)) {
725 return(Cudd_NotCond(DD_ONE(dd
),cuddV(f
) < cuddV(l
) || cuddV(f
) > cuddV(u
)));
729 res
= cuddCacheLookup(dd
,DD_ADD_BDD_DO_INTERVAL_TAG
,f
,l
,u
);
730 if (res
!= NULL
) return(res
);
732 /* Recursive step. */
734 fv
= cuddT(f
); fvn
= cuddE(f
);
736 T
= addBddDoInterval(dd
,fv
,l
,u
);
737 if (T
== NULL
) return(NULL
);
740 E
= addBddDoInterval(dd
,fvn
,l
,u
);
742 Cudd_RecursiveDeref(dd
, T
);
746 if (Cudd_IsComplement(T
)) {
747 res
= (T
== E
) ? Cudd_Not(T
) : cuddUniqueInter(dd
,v
,Cudd_Not(T
),Cudd_Not(E
));
749 Cudd_RecursiveDeref(dd
, T
);
750 Cudd_RecursiveDeref(dd
, E
);
755 res
= (T
== E
) ? T
: cuddUniqueInter(dd
,v
,T
,E
);
757 Cudd_RecursiveDeref(dd
, T
);
758 Cudd_RecursiveDeref(dd
, E
);
766 cuddCacheInsert(dd
,DD_ADD_BDD_DO_INTERVAL_TAG
,f
,l
,u
,res
);
770 } /* end of addBddDoInterval */
773 /**Function********************************************************************
775 Synopsis [Performs the recursive step for Cudd_addBddIthBit.]
777 Description [Performs the recursive step for Cudd_addBddIthBit.
778 Returns a pointer to the BDD if successful; NULL otherwise.]
784 ******************************************************************************/
797 /* Check terminal case. */
798 if (cuddIsConstant(f
)) {
799 mask
= 1 << ((int) cuddV(index
));
800 value
= (int) cuddV(f
);
801 return(Cudd_NotCond(DD_ONE(dd
),(value
& mask
) == 0));
805 res
= cuddCacheLookup2(dd
,addBddDoIthBit
,f
,index
);
806 if (res
!= NULL
) return(res
);
808 /* Recursive step. */
810 fv
= cuddT(f
); fvn
= cuddE(f
);
812 T
= addBddDoIthBit(dd
,fv
,index
);
813 if (T
== NULL
) return(NULL
);
816 E
= addBddDoIthBit(dd
,fvn
,index
);
818 Cudd_RecursiveDeref(dd
, T
);
822 if (Cudd_IsComplement(T
)) {
823 res
= (T
== E
) ? Cudd_Not(T
) : cuddUniqueInter(dd
,v
,Cudd_Not(T
),Cudd_Not(E
));
825 Cudd_RecursiveDeref(dd
, T
);
826 Cudd_RecursiveDeref(dd
, E
);
831 res
= (T
== E
) ? T
: cuddUniqueInter(dd
,v
,T
,E
);
833 Cudd_RecursiveDeref(dd
, T
);
834 Cudd_RecursiveDeref(dd
, E
);
842 cuddCacheInsert2(dd
,addBddDoIthBit
,f
,index
,res
);
846 } /* end of addBddDoIthBit */
849 /**Function********************************************************************
851 Synopsis [Performs the recursive step for Cudd_BddToAdd.]
853 Description [Performs the recursive step for Cudd_BddToAdd. Returns a
854 pointer to the resulting ADD if successful; NULL otherwise.]
860 ******************************************************************************/
867 DdNode
*res
, *res1
, *T
, *E
, *Bt
, *Be
;
873 if (Cudd_IsConstant(B
)) {
881 /* Check visited table */
882 res
= cuddCacheLookup1(dd
,ddBddToAddRecur
,B
);
883 if (res
!= NULL
) return(res
);
885 if (Cudd_IsComplement(B
)) {
887 Bt
= cuddT(Cudd_Regular(B
));
888 Be
= cuddE(Cudd_Regular(B
));
894 T
= ddBddToAddRecur(dd
, Bt
);
895 if (T
== NULL
) return(NULL
);
898 E
= ddBddToAddRecur(dd
, Be
);
900 Cudd_RecursiveDeref(dd
, T
);
905 /* No need to check for T == E, because it is guaranteed not to happen. */
906 res
= cuddUniqueInter(dd
, (int) Cudd_Regular(B
)->index
, T
, E
);
908 Cudd_RecursiveDeref(dd
,T
);
909 Cudd_RecursiveDeref(dd
,E
);
917 res1
= cuddAddCmplRecur(dd
, res
);
919 Cudd_RecursiveDeref(dd
, res
);
923 Cudd_RecursiveDeref(dd
, res
);
929 cuddCacheInsert1(dd
,ddBddToAddRecur
,B
,res
);
933 } /* end of ddBddToAddRecur */
936 /**Function********************************************************************
938 Synopsis [Performs the recursive step of Cudd_bddTransfer.]
940 Description [Performs the recursive step of Cudd_bddTransfer.
941 Returns a pointer to the result if successful; NULL otherwise.]
945 SeeAlso [cuddBddTransfer]
947 ******************************************************************************/
949 cuddBddTransferRecur(
955 DdNode
*ft
, *fe
, *t
, *e
, *var
, *res
;
962 comple
= Cudd_IsComplement(f
);
965 if (Cudd_IsConstant(f
)) return(Cudd_NotCond(one
, comple
));
967 /* Make canonical to increase the utilization of the cache. */
968 f
= Cudd_NotCond(f
,comple
);
969 /* Now f is a regular pointer to a non-constant node. */
971 /* Check the cache. */
972 if (st_lookup(table
, f
, &res
))
973 return(Cudd_NotCond(res
,comple
));
975 /* Recursive step. */
977 ft
= cuddT(f
); fe
= cuddE(f
);
979 t
= cuddBddTransferRecur(ddS
, ddD
, ft
, table
);
985 e
= cuddBddTransferRecur(ddS
, ddD
, fe
, table
);
987 Cudd_RecursiveDeref(ddD
, t
);
992 zero
= Cudd_Not(one
);
993 var
= cuddUniqueInter(ddD
,index
,one
,zero
);
995 Cudd_RecursiveDeref(ddD
, t
);
996 Cudd_RecursiveDeref(ddD
, e
);
999 res
= cuddBddIteRecur(ddD
,var
,t
,e
);
1001 Cudd_RecursiveDeref(ddD
, t
);
1002 Cudd_RecursiveDeref(ddD
, e
);
1006 Cudd_RecursiveDeref(ddD
, t
);
1007 Cudd_RecursiveDeref(ddD
, e
);
1009 if (st_add_direct(table
, (char *) f
, (char *) res
) == ST_OUT_OF_MEM
) {
1010 Cudd_RecursiveDeref(ddD
, res
);
1013 return(Cudd_NotCond(res
,comple
));
1015 } /* end of cuddBddTransferRecur */