1 /**CFile***********************************************************************
3 FileName [cuddPriority.c]
7 Synopsis [Priority functions.]
9 Description [External procedures included in this file:
11 <li> Cudd_PrioritySelect()
17 <li> Cudd_Inequality()
18 <li> Cudd_Disequality()
19 <li> Cudd_bddInterval()
20 <li> Cudd_CProjection()
21 <li> Cudd_addHamming()
22 <li> Cudd_MinHammingDist()
23 <li> Cudd_bddClosestCube()
25 Internal procedures included in this module:
27 <li> cuddCProjectionRecur()
28 <li> cuddBddClosestCube()
30 Static procedures included in this module:
32 <li> cuddMinHammingDistRecur()
40 Author [Fabio Somenzi]
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 ******************************************************************************/
80 /*---------------------------------------------------------------------------*/
81 /* Constant declarations */
82 /*---------------------------------------------------------------------------*/
86 /*---------------------------------------------------------------------------*/
87 /* Stucture declarations */
88 /*---------------------------------------------------------------------------*/
91 /*---------------------------------------------------------------------------*/
92 /* Type declarations */
93 /*---------------------------------------------------------------------------*/
96 /*---------------------------------------------------------------------------*/
97 /* Variable declarations */
98 /*---------------------------------------------------------------------------*/
101 static char rcsid
[] DD_UNUSED
= "$Id: cuddPriority.c,v 1.33 2009/02/20 02:14:58 fabio Exp $";
104 /*---------------------------------------------------------------------------*/
105 /* Macro declarations */
106 /*---------------------------------------------------------------------------*/
109 /**AutomaticStart*************************************************************/
111 /*---------------------------------------------------------------------------*/
112 /* Static function prototypes */
113 /*---------------------------------------------------------------------------*/
114 static int cuddMinHammingDistRecur (DdNode
* f
, int *minterm
, DdHashTable
* table
, int upperBound
);
115 static DdNode
* separateCube (DdManager
*dd
, DdNode
*f
, CUDD_VALUE_TYPE
*distance
);
116 static DdNode
* createResult (DdManager
*dd
, unsigned int index
, unsigned int phase
, DdNode
*cube
, CUDD_VALUE_TYPE distance
);
118 /**AutomaticEnd***************************************************************/
121 /*---------------------------------------------------------------------------*/
122 /* Definition of exported functions */
123 /*---------------------------------------------------------------------------*/
126 /**Function********************************************************************
128 Synopsis [Selects pairs from R using a priority function.]
130 Description [Selects pairs from a relation R(x,y) (given as a BDD)
131 in such a way that a given x appears in one pair only. Uses a
132 priority function to determine which y should be paired to a given x.
133 Cudd_PrioritySelect returns a pointer to
134 the selected function if successful; NULL otherwise.
135 Three of the arguments--x, y, and z--are vectors of BDD variables.
136 The first two are the variables on which R depends. The third vectore
137 is a vector of auxiliary variables, used during the computation. This
138 vector is optional. If a NULL value is passed instead,
139 Cudd_PrioritySelect will create the working variables on the fly.
140 The sizes of x and y (and z if it is not NULL) should equal n.
141 The priority function Pi can be passed as a BDD, or can be built by
142 Cudd_PrioritySelect. If NULL is passed instead of a DdNode *,
143 parameter Pifunc is used by Cudd_PrioritySelect to build a BDD for the
144 priority function. (Pifunc is a pointer to a C function.) If Pi is not
145 NULL, then Pifunc is ignored. Pifunc should have the same interface as
146 the standard priority functions (e.g., Cudd_Dxygtdxz).
147 Cudd_PrioritySelect and Cudd_CProjection can sometimes be used
148 interchangeably. Specifically, calling Cudd_PrioritySelect with
149 Cudd_Xgty as Pifunc produces the same result as calling
150 Cudd_CProjection with the all-zero minterm as reference minterm.
151 However, depending on the application, one or the other may be
154 <li> When extracting representatives from an equivalence relation,
155 Cudd_CProjection has the advantage of nor requiring the auxiliary
157 <li> When computing matchings in general bipartite graphs,
158 Cudd_PrioritySelect normally obtains better results because it can use
159 more powerful matching schemes (e.g., Cudd_Dxygtdxz).
163 SideEffects [If called with z == NULL, will create new variables in
166 SeeAlso [Cudd_Dxygtdxz Cudd_Dxygtdyz Cudd_Xgty
167 Cudd_bddAdjPermuteX Cudd_CProjection]
169 ******************************************************************************/
172 DdManager
* dd
/* manager */,
173 DdNode
* R
/* BDD of the relation */,
174 DdNode
** x
/* array of x variables */,
175 DdNode
** y
/* array of y variables */,
176 DdNode
** z
/* array of z variables (optional: may be NULL) */,
177 DdNode
* Pi
/* BDD of the priority function (optional: may be NULL) */,
178 int n
/* size of x, y, and z */,
179 DD_PRFP Pifunc
/* function used to build Pi if it is NULL */)
182 DdNode
*zcube
= NULL
;
188 /* Create z variables if needed. */
190 if (Pi
!= NULL
) return(NULL
);
191 z
= ALLOC(DdNode
*,n
);
193 dd
->errorCode
= CUDD_MEMORY_OUT
;
197 for (i
= 0; i
< n
; i
++) {
198 if (dd
->size
>= (int) CUDD_MAXINDEX
- 1) goto endgame
;
199 z
[i
] = cuddUniqueInter(dd
,dd
->size
,dd
->one
,Cudd_Not(dd
->one
));
200 if (z
[i
] == NULL
) goto endgame
;
204 /* Create priority function BDD if needed. */
206 Pi
= Pifunc(dd
,n
,x
,y
,z
);
207 if (Pi
== NULL
) goto endgame
;
212 /* Initialize abstraction cube. */
215 for (i
= n
- 1; i
>= 0; i
--) {
217 tmpp
= Cudd_bddAnd(dd
,z
[i
],zcube
);
218 if (tmpp
== NULL
) goto endgame
;
220 Cudd_RecursiveDeref(dd
,zcube
);
224 /* Compute subset of (x,y) pairs. */
225 Rxz
= Cudd_bddSwapVariables(dd
,R
,y
,z
,n
);
226 if (Rxz
== NULL
) goto endgame
;
228 Q
= Cudd_bddAndAbstract(dd
,Rxz
,Pi
,zcube
);
230 Cudd_RecursiveDeref(dd
,Rxz
);
234 Cudd_RecursiveDeref(dd
,Rxz
);
235 res
= Cudd_bddAnd(dd
,R
,Cudd_Not(Q
));
237 Cudd_RecursiveDeref(dd
,Q
);
241 Cudd_RecursiveDeref(dd
,Q
);
244 if (zcube
!= NULL
) Cudd_RecursiveDeref(dd
,zcube
);
249 Cudd_RecursiveDeref(dd
,Pi
);
251 if (res
!= NULL
) cuddDeref(res
);
254 } /* Cudd_PrioritySelect */
257 /**Function********************************************************************
259 Synopsis [Generates a BDD for the function x > y.]
261 Description [This function generates a BDD for the function x > y.
262 Both x and y are N-bit numbers, x\[0\] x\[1\] ... x\[N-1\] and
263 y\[0\] y\[1\] ... y\[N-1\], with 0 the most significant bit.
264 The BDD is built bottom-up.
265 It has 3*N-1 internal nodes, if the variables are ordered as follows:
266 x\[0\] y\[0\] x\[1\] y\[1\] ... x\[N-1\] y\[N-1\].
267 Argument z is not used by Cudd_Xgty: it is included to make it
268 call-compatible to Cudd_Dxygtdxz and Cudd_Dxygtdyz.]
272 SeeAlso [Cudd_PrioritySelect Cudd_Dxygtdxz Cudd_Dxygtdyz]
274 ******************************************************************************/
277 DdManager
* dd
/* DD manager */,
278 int N
/* number of x and y variables */,
279 DdNode
** z
/* array of z variables: unused */,
280 DdNode
** x
/* array of x variables */,
281 DdNode
** y
/* array of y variables */)
286 /* Build bottom part of BDD outside loop. */
287 u
= Cudd_bddAnd(dd
, x
[N
-1], Cudd_Not(y
[N
-1]));
288 if (u
== NULL
) return(NULL
);
291 /* Loop to build the rest of the BDD. */
292 for (i
= N
-2; i
>= 0; i
--) {
293 v
= Cudd_bddAnd(dd
, y
[i
], Cudd_Not(u
));
295 Cudd_RecursiveDeref(dd
, u
);
299 w
= Cudd_bddAnd(dd
, Cudd_Not(y
[i
]), u
);
301 Cudd_RecursiveDeref(dd
, u
);
302 Cudd_RecursiveDeref(dd
, v
);
306 Cudd_RecursiveDeref(dd
, u
);
307 u
= Cudd_bddIte(dd
, x
[i
], Cudd_Not(v
), w
);
309 Cudd_RecursiveDeref(dd
, v
);
310 Cudd_RecursiveDeref(dd
, w
);
314 Cudd_RecursiveDeref(dd
, v
);
315 Cudd_RecursiveDeref(dd
, w
);
321 } /* end of Cudd_Xgty */
324 /**Function********************************************************************
326 Synopsis [Generates a BDD for the function x==y.]
328 Description [This function generates a BDD for the function x==y.
329 Both x and y are N-bit numbers, x\[0\] x\[1\] ... x\[N-1\] and
330 y\[0\] y\[1\] ... y\[N-1\], with 0 the most significant bit.
331 The BDD is built bottom-up.
332 It has 3*N-1 internal nodes, if the variables are ordered as follows:
333 x\[0\] y\[0\] x\[1\] y\[1\] ... x\[N-1\] y\[N-1\]. ]
337 SeeAlso [Cudd_addXeqy]
339 ******************************************************************************/
342 DdManager
* dd
/* DD manager */,
343 int N
/* number of x and y variables */,
344 DdNode
** x
/* array of x variables */,
345 DdNode
** y
/* array of y variables */)
350 /* Build bottom part of BDD outside loop. */
351 u
= Cudd_bddIte(dd
, x
[N
-1], y
[N
-1], Cudd_Not(y
[N
-1]));
352 if (u
== NULL
) return(NULL
);
355 /* Loop to build the rest of the BDD. */
356 for (i
= N
-2; i
>= 0; i
--) {
357 v
= Cudd_bddAnd(dd
, y
[i
], u
);
359 Cudd_RecursiveDeref(dd
, u
);
363 w
= Cudd_bddAnd(dd
, Cudd_Not(y
[i
]), u
);
365 Cudd_RecursiveDeref(dd
, u
);
366 Cudd_RecursiveDeref(dd
, v
);
370 Cudd_RecursiveDeref(dd
, u
);
371 u
= Cudd_bddIte(dd
, x
[i
], v
, w
);
373 Cudd_RecursiveDeref(dd
, v
);
374 Cudd_RecursiveDeref(dd
, w
);
378 Cudd_RecursiveDeref(dd
, v
);
379 Cudd_RecursiveDeref(dd
, w
);
384 } /* end of Cudd_Xeqy */
387 /**Function********************************************************************
389 Synopsis [Generates an ADD for the function x==y.]
391 Description [This function generates an ADD for the function x==y.
392 Both x and y are N-bit numbers, x\[0\] x\[1\] ... x\[N-1\] and
393 y\[0\] y\[1\] ... y\[N-1\], with 0 the most significant bit.
394 The ADD is built bottom-up.
395 It has 3*N-1 internal nodes, if the variables are ordered as follows:
396 x\[0\] y\[0\] x\[1\] y\[1\] ... x\[N-1\] y\[N-1\]. ]
402 ******************************************************************************/
405 DdManager
* dd
/* DD manager */,
406 int N
/* number of x and y variables */,
407 DdNode
** x
/* array of x variables */,
408 DdNode
** y
/* array of y variables */)
417 /* Build bottom part of ADD outside loop. */
418 v
= Cudd_addIte(dd
, y
[N
-1], one
, zero
);
419 if (v
== NULL
) return(NULL
);
421 w
= Cudd_addIte(dd
, y
[N
-1], zero
, one
);
423 Cudd_RecursiveDeref(dd
, v
);
427 u
= Cudd_addIte(dd
, x
[N
-1], v
, w
);
429 Cudd_RecursiveDeref(dd
, v
);
430 Cudd_RecursiveDeref(dd
, w
);
434 Cudd_RecursiveDeref(dd
, v
);
435 Cudd_RecursiveDeref(dd
, w
);
437 /* Loop to build the rest of the ADD. */
438 for (i
= N
-2; i
>= 0; i
--) {
439 v
= Cudd_addIte(dd
, y
[i
], u
, zero
);
441 Cudd_RecursiveDeref(dd
, u
);
445 w
= Cudd_addIte(dd
, y
[i
], zero
, u
);
447 Cudd_RecursiveDeref(dd
, u
);
448 Cudd_RecursiveDeref(dd
, v
);
452 Cudd_RecursiveDeref(dd
, u
);
453 u
= Cudd_addIte(dd
, x
[i
], v
, w
);
455 Cudd_RecursiveDeref(dd
, v
);
456 Cudd_RecursiveDeref(dd
, w
);
460 Cudd_RecursiveDeref(dd
, v
);
461 Cudd_RecursiveDeref(dd
, w
);
466 } /* end of Cudd_addXeqy */
469 /**Function********************************************************************
471 Synopsis [Generates a BDD for the function d(x,y) > d(x,z).]
473 Description [This function generates a BDD for the function d(x,y)
475 x, y, and z are N-bit numbers, x\[0\] x\[1\] ... x\[N-1\],
476 y\[0\] y\[1\] ... y\[N-1\], and z\[0\] z\[1\] ... z\[N-1\],
477 with 0 the most significant bit.
478 The distance d(x,y) is defined as:
479 \sum_{i=0}^{N-1}(|x_i - y_i| \cdot 2^{N-i-1}).
480 The BDD is built bottom-up.
481 It has 7*N-3 internal nodes, if the variables are ordered as follows:
482 x\[0\] y\[0\] z\[0\] x\[1\] y\[1\] z\[1\] ... x\[N-1\] y\[N-1\] z\[N-1\]. ]
486 SeeAlso [Cudd_PrioritySelect Cudd_Dxygtdyz Cudd_Xgty Cudd_bddAdjPermuteX]
488 ******************************************************************************/
491 DdManager
* dd
/* DD manager */,
492 int N
/* number of x, y, and z variables */,
493 DdNode
** x
/* array of x variables */,
494 DdNode
** y
/* array of y variables */,
495 DdNode
** z
/* array of z variables */)
498 DdNode
*z1
, *z2
, *z3
, *z4
, *y1_
, *y2
, *x1
;
502 zero
= Cudd_Not(one
);
504 /* Build bottom part of BDD outside loop. */
505 y1_
= Cudd_bddIte(dd
, y
[N
-1], one
, Cudd_Not(z
[N
-1]));
506 if (y1_
== NULL
) return(NULL
);
508 y2
= Cudd_bddIte(dd
, y
[N
-1], z
[N
-1], one
);
510 Cudd_RecursiveDeref(dd
, y1_
);
514 x1
= Cudd_bddIte(dd
, x
[N
-1], y1_
, y2
);
516 Cudd_RecursiveDeref(dd
, y1_
);
517 Cudd_RecursiveDeref(dd
, y2
);
521 Cudd_RecursiveDeref(dd
, y1_
);
522 Cudd_RecursiveDeref(dd
, y2
);
524 /* Loop to build the rest of the BDD. */
525 for (i
= N
-2; i
>= 0; i
--) {
526 z1
= Cudd_bddIte(dd
, z
[i
], one
, Cudd_Not(x1
));
528 Cudd_RecursiveDeref(dd
, x1
);
532 z2
= Cudd_bddIte(dd
, z
[i
], x1
, one
);
534 Cudd_RecursiveDeref(dd
, x1
);
535 Cudd_RecursiveDeref(dd
, z1
);
539 z3
= Cudd_bddIte(dd
, z
[i
], one
, x1
);
541 Cudd_RecursiveDeref(dd
, x1
);
542 Cudd_RecursiveDeref(dd
, z1
);
543 Cudd_RecursiveDeref(dd
, z2
);
547 z4
= Cudd_bddIte(dd
, z
[i
], x1
, zero
);
549 Cudd_RecursiveDeref(dd
, x1
);
550 Cudd_RecursiveDeref(dd
, z1
);
551 Cudd_RecursiveDeref(dd
, z2
);
552 Cudd_RecursiveDeref(dd
, z3
);
556 Cudd_RecursiveDeref(dd
, x1
);
557 y1_
= Cudd_bddIte(dd
, y
[i
], z2
, Cudd_Not(z1
));
559 Cudd_RecursiveDeref(dd
, z1
);
560 Cudd_RecursiveDeref(dd
, z2
);
561 Cudd_RecursiveDeref(dd
, z3
);
562 Cudd_RecursiveDeref(dd
, z4
);
566 y2
= Cudd_bddIte(dd
, y
[i
], z4
, z3
);
568 Cudd_RecursiveDeref(dd
, z1
);
569 Cudd_RecursiveDeref(dd
, z2
);
570 Cudd_RecursiveDeref(dd
, z3
);
571 Cudd_RecursiveDeref(dd
, z4
);
572 Cudd_RecursiveDeref(dd
, y1_
);
576 Cudd_RecursiveDeref(dd
, z1
);
577 Cudd_RecursiveDeref(dd
, z2
);
578 Cudd_RecursiveDeref(dd
, z3
);
579 Cudd_RecursiveDeref(dd
, z4
);
580 x1
= Cudd_bddIte(dd
, x
[i
], y1_
, y2
);
582 Cudd_RecursiveDeref(dd
, y1_
);
583 Cudd_RecursiveDeref(dd
, y2
);
587 Cudd_RecursiveDeref(dd
, y1_
);
588 Cudd_RecursiveDeref(dd
, y2
);
591 return(Cudd_Not(x1
));
593 } /* end of Cudd_Dxygtdxz */
596 /**Function********************************************************************
598 Synopsis [Generates a BDD for the function d(x,y) > d(y,z).]
600 Description [This function generates a BDD for the function d(x,y)
602 x, y, and z are N-bit numbers, x\[0\] x\[1\] ... x\[N-1\],
603 y\[0\] y\[1\] ... y\[N-1\], and z\[0\] z\[1\] ... z\[N-1\],
604 with 0 the most significant bit.
605 The distance d(x,y) is defined as:
606 \sum_{i=0}^{N-1}(|x_i - y_i| \cdot 2^{N-i-1}).
607 The BDD is built bottom-up.
608 It has 7*N-3 internal nodes, if the variables are ordered as follows:
609 x\[0\] y\[0\] z\[0\] x\[1\] y\[1\] z\[1\] ... x\[N-1\] y\[N-1\] z\[N-1\]. ]
613 SeeAlso [Cudd_PrioritySelect Cudd_Dxygtdxz Cudd_Xgty Cudd_bddAdjPermuteX]
615 ******************************************************************************/
618 DdManager
* dd
/* DD manager */,
619 int N
/* number of x, y, and z variables */,
620 DdNode
** x
/* array of x variables */,
621 DdNode
** y
/* array of y variables */,
622 DdNode
** z
/* array of z variables */)
625 DdNode
*z1
, *z2
, *z3
, *z4
, *y1_
, *y2
, *x1
;
629 zero
= Cudd_Not(one
);
631 /* Build bottom part of BDD outside loop. */
632 y1_
= Cudd_bddIte(dd
, y
[N
-1], one
, z
[N
-1]);
633 if (y1_
== NULL
) return(NULL
);
635 y2
= Cudd_bddIte(dd
, y
[N
-1], z
[N
-1], zero
);
637 Cudd_RecursiveDeref(dd
, y1_
);
641 x1
= Cudd_bddIte(dd
, x
[N
-1], y1_
, Cudd_Not(y2
));
643 Cudd_RecursiveDeref(dd
, y1_
);
644 Cudd_RecursiveDeref(dd
, y2
);
648 Cudd_RecursiveDeref(dd
, y1_
);
649 Cudd_RecursiveDeref(dd
, y2
);
651 /* Loop to build the rest of the BDD. */
652 for (i
= N
-2; i
>= 0; i
--) {
653 z1
= Cudd_bddIte(dd
, z
[i
], x1
, zero
);
655 Cudd_RecursiveDeref(dd
, x1
);
659 z2
= Cudd_bddIte(dd
, z
[i
], x1
, one
);
661 Cudd_RecursiveDeref(dd
, x1
);
662 Cudd_RecursiveDeref(dd
, z1
);
666 z3
= Cudd_bddIte(dd
, z
[i
], one
, x1
);
668 Cudd_RecursiveDeref(dd
, x1
);
669 Cudd_RecursiveDeref(dd
, z1
);
670 Cudd_RecursiveDeref(dd
, z2
);
674 z4
= Cudd_bddIte(dd
, z
[i
], one
, Cudd_Not(x1
));
676 Cudd_RecursiveDeref(dd
, x1
);
677 Cudd_RecursiveDeref(dd
, z1
);
678 Cudd_RecursiveDeref(dd
, z2
);
679 Cudd_RecursiveDeref(dd
, z3
);
683 Cudd_RecursiveDeref(dd
, x1
);
684 y1_
= Cudd_bddIte(dd
, y
[i
], z2
, z1
);
686 Cudd_RecursiveDeref(dd
, z1
);
687 Cudd_RecursiveDeref(dd
, z2
);
688 Cudd_RecursiveDeref(dd
, z3
);
689 Cudd_RecursiveDeref(dd
, z4
);
693 y2
= Cudd_bddIte(dd
, y
[i
], z4
, Cudd_Not(z3
));
695 Cudd_RecursiveDeref(dd
, z1
);
696 Cudd_RecursiveDeref(dd
, z2
);
697 Cudd_RecursiveDeref(dd
, z3
);
698 Cudd_RecursiveDeref(dd
, z4
);
699 Cudd_RecursiveDeref(dd
, y1_
);
703 Cudd_RecursiveDeref(dd
, z1
);
704 Cudd_RecursiveDeref(dd
, z2
);
705 Cudd_RecursiveDeref(dd
, z3
);
706 Cudd_RecursiveDeref(dd
, z4
);
707 x1
= Cudd_bddIte(dd
, x
[i
], y1_
, Cudd_Not(y2
));
709 Cudd_RecursiveDeref(dd
, y1_
);
710 Cudd_RecursiveDeref(dd
, y2
);
714 Cudd_RecursiveDeref(dd
, y1_
);
715 Cudd_RecursiveDeref(dd
, y2
);
718 return(Cudd_Not(x1
));
720 } /* end of Cudd_Dxygtdyz */
723 /**Function********************************************************************
725 Synopsis [Generates a BDD for the function x - y ≥ c.]
727 Description [This function generates a BDD for the function x -y ≥ c.
728 Both x and y are N-bit numbers, x\[0\] x\[1\] ... x\[N-1\] and
729 y\[0\] y\[1\] ... y\[N-1\], with 0 the most significant bit.
730 The BDD is built bottom-up.
731 It has a linear number of nodes if the variables are ordered as follows:
732 x\[0\] y\[0\] x\[1\] y\[1\] ... x\[N-1\] y\[N-1\].]
738 ******************************************************************************/
741 DdManager
* dd
/* DD manager */,
742 int N
/* number of x and y variables */,
743 int c
/* right-hand side constant */,
744 DdNode
** x
/* array of x variables */,
745 DdNode
** y
/* array of y variables */)
747 /* The nodes at level i represent values of the difference that are
748 ** multiples of 2^i. We use variables with names starting with k
749 ** to denote the multipliers of 2^i in such multiples. */
752 /* Mask used to compute the ceiling function. Since we divide by 2^i,
753 ** we want to know whether the dividend is a multiple of 2^i. If it is,
754 ** then ceiling and floor coincide; otherwise, they differ by one. */
758 DdNode
*f
= NULL
; /* the eventual result */
759 DdNode
*one
= DD_ONE(dd
);
760 DdNode
*zero
= Cudd_Not(one
);
762 /* Two x-labeled nodes are created at most at each iteration. They are
763 ** stored, along with their k values, in these variables. At each level,
764 ** the old nodes are freed and the new nodes are copied into the old map.
767 int invalidIndex
= 1 << (N
-1);
768 int index
[2] = {invalidIndex
, invalidIndex
};
770 /* This should never happen. */
771 if (N
< 0) return(NULL
);
773 /* If there are no bits, both operands are 0. The result depends on c. */
775 if (c
>= 0) return(one
);
779 /* The maximum or the minimum difference comparing to c can generate the terminal case */
780 if ((1 << N
) - 1 < c
) return(zero
);
781 else if ((-(1 << N
) + 1) >= c
) return(one
);
783 /* Build the result bottom up. */
784 for (i
= 1; i
<= N
; i
++) {
785 int kTrueLower
, kFalseLower
;
786 int leftChild
, middleChild
, rightChild
;
787 DdNode
*g0
, *g1
, *fplus
, *fequal
, *fminus
;
793 kFalseLower
= kFalse
;
794 /* kTrue = ceiling((c-1)/2^i) + 1 */
795 kTrue
= ((c
-1) >> i
) + ((c
& mask
) != 1) + 1;
796 mask
= (mask
<< 1) | 1;
797 /* kFalse = floor(c/2^i) - 1 */
798 kFalse
= (c
>> i
) - 1;
799 newIndex
[0] = invalidIndex
;
800 newIndex
[1] = invalidIndex
;
802 for (j
= kFalse
+ 1; j
< kTrue
; j
++) {
803 /* Skip if node is not reachable from top of BDD. */
804 if ((j
>= (1 << (N
- i
))) || (j
<= -(1 << (N
-i
)))) continue;
807 leftChild
= (j
<< 1) - 1;
808 if (leftChild
>= kTrueLower
) {
810 } else if (leftChild
<= kFalseLower
) {
813 assert(leftChild
== index
[0] || leftChild
== index
[1]);
814 if (leftChild
== index
[0]) {
822 middleChild
= j
<< 1;
823 if (middleChild
>= kTrueLower
) {
825 } else if (middleChild
<= kFalseLower
) {
828 assert(middleChild
== index
[0] || middleChild
== index
[1]);
829 if (middleChild
== index
[0]) {
837 rightChild
= (j
<< 1) + 1;
838 if (rightChild
>= kTrueLower
) {
840 } else if (rightChild
<= kFalseLower
) {
843 assert(rightChild
== index
[0] || rightChild
== index
[1]);
844 if (rightChild
== index
[0]) {
851 /* Build new nodes. */
852 g1
= Cudd_bddIte(dd
, y
[N
- i
], fequal
, fplus
);
854 if (index
[0] != invalidIndex
) Cudd_IterDerefBdd(dd
, map
[0]);
855 if (index
[1] != invalidIndex
) Cudd_IterDerefBdd(dd
, map
[1]);
856 if (newIndex
[0] != invalidIndex
) Cudd_IterDerefBdd(dd
, newMap
[0]);
857 if (newIndex
[1] != invalidIndex
) Cudd_IterDerefBdd(dd
, newMap
[1]);
861 g0
= Cudd_bddIte(dd
, y
[N
- i
], fminus
, fequal
);
863 Cudd_IterDerefBdd(dd
, g1
);
864 if (index
[0] != invalidIndex
) Cudd_IterDerefBdd(dd
, map
[0]);
865 if (index
[1] != invalidIndex
) Cudd_IterDerefBdd(dd
, map
[1]);
866 if (newIndex
[0] != invalidIndex
) Cudd_IterDerefBdd(dd
, newMap
[0]);
867 if (newIndex
[1] != invalidIndex
) Cudd_IterDerefBdd(dd
, newMap
[1]);
871 f
= Cudd_bddIte(dd
, x
[N
- i
], g1
, g0
);
873 Cudd_IterDerefBdd(dd
, g1
);
874 Cudd_IterDerefBdd(dd
, g0
);
875 if (index
[0] != invalidIndex
) Cudd_IterDerefBdd(dd
, map
[0]);
876 if (index
[1] != invalidIndex
) Cudd_IterDerefBdd(dd
, map
[1]);
877 if (newIndex
[0] != invalidIndex
) Cudd_IterDerefBdd(dd
, newMap
[0]);
878 if (newIndex
[1] != invalidIndex
) Cudd_IterDerefBdd(dd
, newMap
[1]);
882 Cudd_IterDerefBdd(dd
, g1
);
883 Cudd_IterDerefBdd(dd
, g0
);
885 /* Save newly computed node in map. */
886 assert(newIndex
[0] == invalidIndex
|| newIndex
[1] == invalidIndex
);
887 if (newIndex
[0] == invalidIndex
) {
896 /* Copy new map to map. */
897 if (index
[0] != invalidIndex
) Cudd_IterDerefBdd(dd
, map
[0]);
898 if (index
[1] != invalidIndex
) Cudd_IterDerefBdd(dd
, map
[1]);
901 index
[0] = newIndex
[0];
902 index
[1] = newIndex
[1];
908 } /* end of Cudd_Inequality */
911 /**Function********************************************************************
913 Synopsis [Generates a BDD for the function x - y != c.]
915 Description [This function generates a BDD for the function x -y != c.
916 Both x and y are N-bit numbers, x\[0\] x\[1\] ... x\[N-1\] and
917 y\[0\] y\[1\] ... y\[N-1\], with 0 the most significant bit.
918 The BDD is built bottom-up.
919 It has a linear number of nodes if the variables are ordered as follows:
920 x\[0\] y\[0\] x\[1\] y\[1\] ... x\[N-1\] y\[N-1\].]
926 ******************************************************************************/
929 DdManager
* dd
/* DD manager */,
930 int N
/* number of x and y variables */,
931 int c
/* right-hand side constant */,
932 DdNode
** x
/* array of x variables */,
933 DdNode
** y
/* array of y variables */)
935 /* The nodes at level i represent values of the difference that are
936 ** multiples of 2^i. We use variables with names starting with k
937 ** to denote the multipliers of 2^i in such multiples. */
941 /* Mask used to compute the ceiling function. Since we divide by 2^i,
942 ** we want to know whether the dividend is a multiple of 2^i. If it is,
943 ** then ceiling and floor coincide; otherwise, they differ by one. */
947 DdNode
*f
= NULL
; /* the eventual result */
948 DdNode
*one
= DD_ONE(dd
);
949 DdNode
*zero
= Cudd_Not(one
);
951 /* Two x-labeled nodes are created at most at each iteration. They are
952 ** stored, along with their k values, in these variables. At each level,
953 ** the old nodes are freed and the new nodes are copied into the old map.
956 int invalidIndex
= 1 << (N
-1);
957 int index
[2] = {invalidIndex
, invalidIndex
};
959 /* This should never happen. */
960 if (N
< 0) return(NULL
);
962 /* If there are no bits, both operands are 0. The result depends on c. */
964 if (c
!= 0) return(one
);
968 /* The maximum or the minimum difference comparing to c can generate the terminal case */
969 if ((1 << N
) - 1 < c
|| (-(1 << N
) + 1) > c
) return(one
);
971 /* Build the result bottom up. */
972 for (i
= 1; i
<= N
; i
++) {
973 int kTrueLbLower
, kTrueUbLower
;
974 int leftChild
, middleChild
, rightChild
;
975 DdNode
*g0
, *g1
, *fplus
, *fequal
, *fminus
;
980 kTrueLbLower
= kTrueLb
;
981 kTrueUbLower
= kTrueUb
;
982 /* kTrueLb = floor((c-1)/2^i) + 2 */
983 kTrueLb
= ((c
-1) >> i
) + 2;
984 /* kTrueUb = ceiling((c+1)/2^i) - 2 */
985 kTrueUb
= ((c
+1) >> i
) + (((c
+2) & mask
) != 1) - 2;
986 mask
= (mask
<< 1) | 1;
987 newIndex
[0] = invalidIndex
;
988 newIndex
[1] = invalidIndex
;
990 for (j
= kTrueUb
+ 1; j
< kTrueLb
; j
++) {
991 /* Skip if node is not reachable from top of BDD. */
992 if ((j
>= (1 << (N
- i
))) || (j
<= -(1 << (N
-i
)))) continue;
995 leftChild
= (j
<< 1) - 1;
996 if (leftChild
>= kTrueLbLower
|| leftChild
<= kTrueUbLower
) {
998 } else if (i
== 1 && leftChild
== kFalse
) {
1001 assert(leftChild
== index
[0] || leftChild
== index
[1]);
1002 if (leftChild
== index
[0]) {
1010 middleChild
= j
<< 1;
1011 if (middleChild
>= kTrueLbLower
|| middleChild
<= kTrueUbLower
) {
1013 } else if (i
== 1 && middleChild
== kFalse
) {
1016 assert(middleChild
== index
[0] || middleChild
== index
[1]);
1017 if (middleChild
== index
[0]) {
1025 rightChild
= (j
<< 1) + 1;
1026 if (rightChild
>= kTrueLbLower
|| rightChild
<= kTrueUbLower
) {
1028 } else if (i
== 1 && rightChild
== kFalse
) {
1031 assert(rightChild
== index
[0] || rightChild
== index
[1]);
1032 if (rightChild
== index
[0]) {
1039 /* Build new nodes. */
1040 g1
= Cudd_bddIte(dd
, y
[N
- i
], fequal
, fplus
);
1042 if (index
[0] != invalidIndex
) Cudd_IterDerefBdd(dd
, map
[0]);
1043 if (index
[1] != invalidIndex
) Cudd_IterDerefBdd(dd
, map
[1]);
1044 if (newIndex
[0] != invalidIndex
) Cudd_IterDerefBdd(dd
, newMap
[0]);
1045 if (newIndex
[1] != invalidIndex
) Cudd_IterDerefBdd(dd
, newMap
[1]);
1049 g0
= Cudd_bddIte(dd
, y
[N
- i
], fminus
, fequal
);
1051 Cudd_IterDerefBdd(dd
, g1
);
1052 if (index
[0] != invalidIndex
) Cudd_IterDerefBdd(dd
, map
[0]);
1053 if (index
[1] != invalidIndex
) Cudd_IterDerefBdd(dd
, map
[1]);
1054 if (newIndex
[0] != invalidIndex
) Cudd_IterDerefBdd(dd
, newMap
[0]);
1055 if (newIndex
[1] != invalidIndex
) Cudd_IterDerefBdd(dd
, newMap
[1]);
1059 f
= Cudd_bddIte(dd
, x
[N
- i
], g1
, g0
);
1061 Cudd_IterDerefBdd(dd
, g1
);
1062 Cudd_IterDerefBdd(dd
, g0
);
1063 if (index
[0] != invalidIndex
) Cudd_IterDerefBdd(dd
, map
[0]);
1064 if (index
[1] != invalidIndex
) Cudd_IterDerefBdd(dd
, map
[1]);
1065 if (newIndex
[0] != invalidIndex
) Cudd_IterDerefBdd(dd
, newMap
[0]);
1066 if (newIndex
[1] != invalidIndex
) Cudd_IterDerefBdd(dd
, newMap
[1]);
1070 Cudd_IterDerefBdd(dd
, g1
);
1071 Cudd_IterDerefBdd(dd
, g0
);
1073 /* Save newly computed node in map. */
1074 assert(newIndex
[0] == invalidIndex
|| newIndex
[1] == invalidIndex
);
1075 if (newIndex
[0] == invalidIndex
) {
1084 /* Copy new map to map. */
1085 if (index
[0] != invalidIndex
) Cudd_IterDerefBdd(dd
, map
[0]);
1086 if (index
[1] != invalidIndex
) Cudd_IterDerefBdd(dd
, map
[1]);
1089 index
[0] = newIndex
[0];
1090 index
[1] = newIndex
[1];
1096 } /* end of Cudd_Disequality */
1099 /**Function********************************************************************
1101 Synopsis [Generates a BDD for the function lowerB ≤ x ≤ upperB.]
1103 Description [This function generates a BDD for the function
1104 lowerB ≤ x ≤ upperB, where x is an N-bit number,
1105 x\[0\] x\[1\] ... x\[N-1\], with 0 the most significant bit (important!).
1106 The number of variables N should be sufficient to represent the bounds;
1107 otherwise, the bounds are truncated to their N least significant bits.
1108 Two BDDs are built bottom-up for lowerB ≤ x and x ≤ upperB, and they
1109 are finally conjoined.]
1115 ******************************************************************************/
1118 DdManager
* dd
/* DD manager */,
1119 int N
/* number of x variables */,
1120 DdNode
** x
/* array of x variables */,
1121 unsigned int lowerB
/* lower bound */,
1122 unsigned int upperB
/* upper bound */)
1125 DdNode
*r
, *rl
, *ru
;
1129 zero
= Cudd_Not(one
);
1136 /* Loop to build the rest of the BDDs. */
1137 for (i
= N
-1; i
>= 0; i
--) {
1139 vl
= Cudd_bddIte(dd
, x
[i
],
1140 lowerB
&1 ? rl
: one
,
1141 lowerB
&1 ? zero
: rl
);
1143 Cudd_IterDerefBdd(dd
, rl
);
1144 Cudd_IterDerefBdd(dd
, ru
);
1148 Cudd_IterDerefBdd(dd
, rl
);
1151 vu
= Cudd_bddIte(dd
, x
[i
],
1152 upperB
&1 ? ru
: zero
,
1153 upperB
&1 ? one
: ru
);
1155 Cudd_IterDerefBdd(dd
, rl
);
1156 Cudd_IterDerefBdd(dd
, ru
);
1160 Cudd_IterDerefBdd(dd
, ru
);
1165 /* Conjoin the two bounds. */
1166 r
= Cudd_bddAnd(dd
, rl
, ru
);
1168 Cudd_IterDerefBdd(dd
, rl
);
1169 Cudd_IterDerefBdd(dd
, ru
);
1173 Cudd_IterDerefBdd(dd
, rl
);
1174 Cudd_IterDerefBdd(dd
, ru
);
1178 } /* end of Cudd_bddInterval */
1181 /**Function********************************************************************
1183 Synopsis [Computes the compatible projection of R w.r.t. cube Y.]
1185 Description [Computes the compatible projection of relation R with
1186 respect to cube Y. Returns a pointer to the c-projection if
1187 successful; NULL otherwise. For a comparison between Cudd_CProjection
1188 and Cudd_PrioritySelect, see the documentation of the latter.]
1192 SeeAlso [Cudd_PrioritySelect]
1194 ******************************************************************************/
1204 if (cuddCheckCube(dd
,Y
) == 0) {
1205 (void) fprintf(dd
->err
,
1206 "Error: The third argument of Cudd_CProjection should be a cube\n");
1207 dd
->errorCode
= CUDD_INVALID_ARG
;
1211 /* Compute the support of Y, which is used by the abstraction step
1212 ** in cuddCProjectionRecur.
1214 support
= Cudd_Support(dd
,Y
);
1215 if (support
== NULL
) return(NULL
);
1220 res
= cuddCProjectionRecur(dd
,R
,Y
,support
);
1221 } while (dd
->reordered
== 1);
1224 Cudd_RecursiveDeref(dd
,support
);
1228 Cudd_RecursiveDeref(dd
,support
);
1233 } /* end of Cudd_CProjection */
1236 /**Function********************************************************************
1238 Synopsis [Computes the Hamming distance ADD.]
1240 Description [Computes the Hamming distance ADD. Returns an ADD that
1241 gives the Hamming distance between its two arguments if successful;
1242 NULL otherwise. The two vectors xVars and yVars identify the variables
1243 that form the two arguments.]
1249 ******************************************************************************/
1257 DdNode
*result
,*tempBdd
;
1258 DdNode
*tempAdd
,*temp
;
1261 result
= DD_ZERO(dd
);
1264 for (i
= 0; i
< nVars
; i
++) {
1265 tempBdd
= Cudd_bddIte(dd
,xVars
[i
],Cudd_Not(yVars
[i
]),yVars
[i
]);
1266 if (tempBdd
== NULL
) {
1267 Cudd_RecursiveDeref(dd
,result
);
1271 tempAdd
= Cudd_BddToAdd(dd
,tempBdd
);
1272 if (tempAdd
== NULL
) {
1273 Cudd_RecursiveDeref(dd
,tempBdd
);
1274 Cudd_RecursiveDeref(dd
,result
);
1278 Cudd_RecursiveDeref(dd
,tempBdd
);
1279 temp
= Cudd_addApply(dd
,Cudd_addPlus
,tempAdd
,result
);
1281 Cudd_RecursiveDeref(dd
,tempAdd
);
1282 Cudd_RecursiveDeref(dd
,result
);
1286 Cudd_RecursiveDeref(dd
,tempAdd
);
1287 Cudd_RecursiveDeref(dd
,result
);
1294 } /* end of Cudd_addHamming */
1297 /**Function********************************************************************
1299 Synopsis [Returns the minimum Hamming distance between f and minterm.]
1301 Description [Returns the minimum Hamming distance between the
1302 minterms of a function f and a reference minterm. The function is
1303 given as a BDD; the minterm is given as an array of integers, one
1304 for each variable in the manager. Returns the minimum distance if
1305 it is less than the upper bound; the upper bound if the minimum
1306 distance is at least as large; CUDD_OUT_OF_MEM in case of failure.]
1310 SeeAlso [Cudd_addHamming Cudd_bddClosestCube]
1312 ******************************************************************************/
1314 Cudd_MinHammingDist(
1315 DdManager
*dd
/* DD manager */,
1316 DdNode
*f
/* function to examine */,
1317 int *minterm
/* reference minterm */,
1318 int upperBound
/* distance above which an approximate answer is OK */)
1321 CUDD_VALUE_TYPE epsilon
;
1324 table
= cuddHashTableInit(dd
,1,2);
1325 if (table
== NULL
) {
1326 return(CUDD_OUT_OF_MEM
);
1328 epsilon
= Cudd_ReadEpsilon(dd
);
1329 Cudd_SetEpsilon(dd
,(CUDD_VALUE_TYPE
)0.0);
1330 res
= cuddMinHammingDistRecur(f
,minterm
,table
,upperBound
);
1331 cuddHashTableQuit(table
);
1332 Cudd_SetEpsilon(dd
,epsilon
);
1336 } /* end of Cudd_MinHammingDist */
1339 /**Function********************************************************************
1341 Synopsis [Finds a cube of f at minimum Hamming distance from g.]
1343 Description [Finds a cube of f at minimum Hamming distance from the
1344 minterms of g. All the minterms of the cube are at the minimum
1345 distance. If the distance is 0, the cube belongs to the
1346 intersection of f and g. Returns the cube if successful; NULL
1349 SideEffects [The distance is returned as a side effect.]
1351 SeeAlso [Cudd_MinHammingDist]
1353 ******************************************************************************/
1355 Cudd_bddClosestCube(
1361 DdNode
*res
, *acube
;
1362 CUDD_VALUE_TYPE rdist
;
1364 /* Compute the cube and distance as a single ADD. */
1367 res
= cuddBddClosestCube(dd
,f
,g
,CUDD_CONST_INDEX
+ 1.0);
1368 } while (dd
->reordered
== 1);
1369 if (res
== NULL
) return(NULL
);
1372 /* Unpack distance and cube. */
1375 acube
= separateCube(dd
, res
, &rdist
);
1376 } while (dd
->reordered
== 1);
1377 if (acube
== NULL
) {
1378 Cudd_RecursiveDeref(dd
, res
);
1382 Cudd_RecursiveDeref(dd
, res
);
1384 /* Convert cube from ADD to BDD. */
1387 res
= cuddAddBddDoPattern(dd
, acube
);
1388 } while (dd
->reordered
== 1);
1390 Cudd_RecursiveDeref(dd
, acube
);
1394 Cudd_RecursiveDeref(dd
, acube
);
1396 *distance
= (int) rdist
;
1400 } /* end of Cudd_bddClosestCube */
1403 /*---------------------------------------------------------------------------*/
1404 /* Definition of internal functions */
1405 /*---------------------------------------------------------------------------*/
1408 /**Function********************************************************************
1410 Synopsis [Performs the recursive step of Cudd_CProjection.]
1412 Description [Performs the recursive step of Cudd_CProjection. Returns
1413 the projection if successful; NULL otherwise.]
1417 SeeAlso [Cudd_CProjection]
1419 ******************************************************************************/
1421 cuddCProjectionRecur(
1427 DdNode
*res
, *res1
, *res2
, *resA
;
1428 DdNode
*r
, *y
, *RT
, *RE
, *YT
, *YE
, *Yrest
, *Ra
, *Ran
, *Gamma
, *Alpha
;
1429 unsigned int topR
, topY
, top
, index
;
1430 DdNode
*one
= DD_ONE(dd
);
1433 if (Y
== one
) return(R
);
1436 assert(!Cudd_IsConstant(Y
));
1439 if (R
== Cudd_Not(one
)) return(R
);
1441 res
= cuddCacheLookup2(dd
, Cudd_CProjection
, R
, Y
);
1442 if (res
!= NULL
) return(res
);
1444 r
= Cudd_Regular(R
);
1445 topR
= cuddI(dd
,r
->index
);
1446 y
= Cudd_Regular(Y
);
1447 topY
= cuddI(dd
,y
->index
);
1449 top
= ddMin(topR
, topY
);
1451 /* Compute the cofactors of R */
1457 RT
= Cudd_Not(RT
); RE
= Cudd_Not(RE
);
1464 /* Y does not depend on the current top variable.
1465 ** We just need to compute the results on the two cofactors of R
1466 ** and make them the children of a node labeled r->index.
1468 res1
= cuddCProjectionRecur(dd
,RT
,Y
,Ysupp
);
1469 if (res1
== NULL
) return(NULL
);
1471 res2
= cuddCProjectionRecur(dd
,RE
,Y
,Ysupp
);
1473 Cudd_RecursiveDeref(dd
,res1
);
1477 res
= cuddBddIteRecur(dd
, dd
->vars
[index
], res1
, res2
);
1479 Cudd_RecursiveDeref(dd
,res1
);
1480 Cudd_RecursiveDeref(dd
,res2
);
1483 /* If we have reached this point, res1 and res2 are now
1484 ** incorporated in res. cuddDeref is therefore sufficient.
1489 /* Compute the cofactors of Y */
1494 YT
= Cudd_Not(YT
); YE
= Cudd_Not(YE
);
1496 if (YT
== Cudd_Not(one
)) {
1497 Alpha
= Cudd_Not(dd
->vars
[index
]);
1502 Alpha
= dd
->vars
[index
];
1507 Gamma
= cuddBddExistAbstractRecur(dd
,Ra
,cuddT(Ysupp
));
1508 if (Gamma
== NULL
) return(NULL
);
1510 res1
= cuddCProjectionRecur(dd
,Ra
,Yrest
,cuddT(Ysupp
));
1511 if (res1
== NULL
) return(NULL
);
1513 res
= cuddBddAndRecur(dd
, Alpha
, res1
);
1515 Cudd_RecursiveDeref(dd
,res1
);
1519 } else if (Gamma
== Cudd_Not(one
)) {
1520 res1
= cuddCProjectionRecur(dd
,Ran
,Yrest
,cuddT(Ysupp
));
1521 if (res1
== NULL
) return(NULL
);
1523 res
= cuddBddAndRecur(dd
, Cudd_Not(Alpha
), res1
);
1525 Cudd_RecursiveDeref(dd
,res1
);
1531 resA
= cuddCProjectionRecur(dd
,Ran
,Yrest
,cuddT(Ysupp
));
1533 Cudd_RecursiveDeref(dd
,Gamma
);
1537 res2
= cuddBddAndRecur(dd
, Cudd_Not(Gamma
), resA
);
1539 Cudd_RecursiveDeref(dd
,Gamma
);
1540 Cudd_RecursiveDeref(dd
,resA
);
1544 Cudd_RecursiveDeref(dd
,Gamma
);
1545 Cudd_RecursiveDeref(dd
,resA
);
1546 res1
= cuddCProjectionRecur(dd
,Ra
,Yrest
,cuddT(Ysupp
));
1548 Cudd_RecursiveDeref(dd
,res2
);
1552 res
= cuddBddIteRecur(dd
, Alpha
, res1
, res2
);
1554 Cudd_RecursiveDeref(dd
,res1
);
1555 Cudd_RecursiveDeref(dd
,res2
);
1563 cuddCacheInsert2(dd
,Cudd_CProjection
,R
,Y
,res
);
1567 } /* end of cuddCProjectionRecur */
1570 /**Function********************************************************************
1572 Synopsis [Performs the recursive step of Cudd_bddClosestCube.]
1574 Description [Performs the recursive step of Cudd_bddClosestCube.
1575 Returns the cube if succesful; NULL otherwise. The procedure uses a
1576 four-way recursion to examine all four combinations of cofactors of
1577 <code>f</code> and <code>g</code> according to the following formula.
1579 H(f,g) = min(H(ft,gt), H(fe,ge), H(ft,ge)+1, H(fe,gt)+1)
1581 Bounding is based on the following observations.
1583 <li> If we already found two points at distance 0, there is no point in
1584 continuing. Furthermore,
1585 <li> If F == not(G) then the best we can hope for is a minimum distance
1586 of 1. If we have already found two points at distance 1, there is
1587 no point in continuing. (Indeed, H(F,G) == 1 in this case. We
1588 have to continue, though, to find the cube.)
1590 The variable <code>bound</code> is set at the largest value of the distance
1591 that we are still interested in. Therefore, we desist when
1593 (bound == -1) and (F != not(G)) or (bound == 0) and (F == not(G)).
1595 If we were maximally aggressive in using the bound, we would always
1596 set the bound to the minimum distance seen thus far minus one. That
1597 is, we would maintain the invariant
1601 except at the very beginning, when we have no value for
1602 <code>minD</code>.<p>
1604 However, we do not use <code>bound < minD</code> when examining the
1605 two negative cofactors, because we try to find a large cube at
1606 minimum distance. To do so, we try to find a cube in the negative
1607 cofactors at the same or smaller distance from the cube found in the
1608 positive cofactors.<p>
1610 When we compute <code>H(ft,ge)</code> and <code>H(fe,gt)</code> we
1611 know that we are going to add 1 to the result of the recursive call
1612 to account for the difference in the splitting variable. Therefore,
1613 we decrease the bound correspondingly.<p>
1615 Another important observation concerns the need of examining all
1616 four pairs of cofators only when both <code>f</code> and
1617 <code>g</code> depend on the top variable.<p>
1619 Suppose <code>gt == ge == g</code>. (That is, <code>g</code> does
1620 not depend on the top variable.) Then
1622 H(f,g) = min(H(ft,g), H(fe,g), H(ft,g)+1, H(fe,g)+1)
1623 = min(H(ft,g), H(fe,g)) .
1625 Therefore, under these circumstances, we skip the two "cross" cases.<p>
1627 An interesting feature of this function is the scheme used for
1628 caching the results in the global computed table. Since we have a
1629 cube and a distance, we combine them to form an ADD. The
1630 combination replaces the zero child of the top node of the cube with
1631 the negative of the distance. (The use of the negative is to avoid
1632 ambiguity with 1.) The degenerate cases (zero and one) are treated
1633 specially because the distance is known (0 for one, and infinity for
1638 SeeAlso [Cudd_bddClosestCube]
1640 ******************************************************************************/
1646 CUDD_VALUE_TYPE bound
)
1648 DdNode
*res
, *F
, *G
, *ft
, *fe
, *gt
, *ge
, *tt
, *ee
;
1649 DdNode
*ctt
, *cee
, *cte
, *cet
;
1650 CUDD_VALUE_TYPE minD
, dtt
, dee
, dte
, det
;
1651 DdNode
*one
= DD_ONE(dd
);
1652 DdNode
*lzero
= Cudd_Not(one
);
1653 DdNode
*azero
= DD_ZERO(dd
);
1654 unsigned int topf
, topg
, index
;
1657 if (bound
< (f
== Cudd_Not(g
))) return(azero
);
1658 /* Terminal cases. */
1659 if (g
== lzero
|| f
== lzero
) return(azero
);
1660 if (f
== one
&& g
== one
) return(one
);
1663 F
= Cudd_Regular(f
);
1664 G
= Cudd_Regular(g
);
1665 if (F
->ref
!= 1 || G
->ref
!= 1) {
1666 res
= cuddCacheLookup2(dd
,(DD_CTFP
) Cudd_bddClosestCube
, f
, g
);
1667 if (res
!= NULL
) return(res
);
1670 topf
= cuddI(dd
,F
->index
);
1671 topg
= cuddI(dd
,G
->index
);
1673 /* Compute cofactors. */
1678 if (Cudd_IsComplement(f
)) {
1690 if (Cudd_IsComplement(g
)) {
1698 tt
= cuddBddClosestCube(dd
,ft
,gt
,bound
);
1699 if (tt
== NULL
) return(NULL
);
1701 ctt
= separateCube(dd
,tt
,&dtt
);
1703 Cudd_RecursiveDeref(dd
, tt
);
1707 Cudd_RecursiveDeref(dd
, tt
);
1709 bound
= ddMin(bound
,minD
);
1711 ee
= cuddBddClosestCube(dd
,fe
,ge
,bound
);
1713 Cudd_RecursiveDeref(dd
, ctt
);
1717 cee
= separateCube(dd
,ee
,&dee
);
1719 Cudd_RecursiveDeref(dd
, ctt
);
1720 Cudd_RecursiveDeref(dd
, ee
);
1724 Cudd_RecursiveDeref(dd
, ee
);
1725 minD
= ddMin(dtt
, dee
);
1726 if (minD
<= CUDD_CONST_INDEX
) bound
= ddMin(bound
,minD
-1);
1728 if (minD
> 0 && topf
== topg
) {
1729 DdNode
*te
= cuddBddClosestCube(dd
,ft
,ge
,bound
-1);
1731 Cudd_RecursiveDeref(dd
, ctt
);
1732 Cudd_RecursiveDeref(dd
, cee
);
1736 cte
= separateCube(dd
,te
,&dte
);
1738 Cudd_RecursiveDeref(dd
, ctt
);
1739 Cudd_RecursiveDeref(dd
, cee
);
1740 Cudd_RecursiveDeref(dd
, te
);
1744 Cudd_RecursiveDeref(dd
, te
);
1746 minD
= ddMin(minD
, dte
);
1750 dte
= CUDD_CONST_INDEX
+ 1.0;
1752 if (minD
<= CUDD_CONST_INDEX
) bound
= ddMin(bound
,minD
-1);
1754 if (minD
> 0 && topf
== topg
) {
1755 DdNode
*et
= cuddBddClosestCube(dd
,fe
,gt
,bound
-1);
1757 Cudd_RecursiveDeref(dd
, ctt
);
1758 Cudd_RecursiveDeref(dd
, cee
);
1759 Cudd_RecursiveDeref(dd
, cte
);
1763 cet
= separateCube(dd
,et
,&det
);
1765 Cudd_RecursiveDeref(dd
, ctt
);
1766 Cudd_RecursiveDeref(dd
, cee
);
1767 Cudd_RecursiveDeref(dd
, cte
);
1768 Cudd_RecursiveDeref(dd
, et
);
1772 Cudd_RecursiveDeref(dd
, et
);
1774 minD
= ddMin(minD
, det
);
1778 det
= CUDD_CONST_INDEX
+ 1.0;
1782 if (dtt
== dee
&& ctt
== cee
) {
1783 res
= createResult(dd
,CUDD_CONST_INDEX
,1,ctt
,dtt
);
1785 res
= createResult(dd
,index
,1,ctt
,dtt
);
1787 } else if (minD
== dee
) {
1788 res
= createResult(dd
,index
,0,cee
,dee
);
1789 } else if (minD
== dte
) {
1791 assert(topf
== topg
);
1793 res
= createResult(dd
,index
,1,cte
,dte
);
1796 assert(topf
== topg
);
1798 res
= createResult(dd
,index
,0,cet
,det
);
1801 Cudd_RecursiveDeref(dd
, ctt
);
1802 Cudd_RecursiveDeref(dd
, cee
);
1803 Cudd_RecursiveDeref(dd
, cte
);
1804 Cudd_RecursiveDeref(dd
, cet
);
1808 Cudd_RecursiveDeref(dd
, ctt
);
1809 Cudd_RecursiveDeref(dd
, cee
);
1810 Cudd_RecursiveDeref(dd
, cte
);
1811 Cudd_RecursiveDeref(dd
, cet
);
1813 /* Only cache results that are different from azero to avoid
1814 ** storing results that depend on the value of the bound. */
1815 if ((F
->ref
!= 1 || G
->ref
!= 1) && res
!= azero
)
1816 cuddCacheInsert2(dd
,(DD_CTFP
) Cudd_bddClosestCube
, f
, g
, res
);
1821 } /* end of cuddBddClosestCube */
1824 /*---------------------------------------------------------------------------*/
1825 /* Definition of static functions */
1826 /*---------------------------------------------------------------------------*/
1829 /**Function********************************************************************
1831 Synopsis [Performs the recursive step of Cudd_MinHammingDist.]
1833 Description [Performs the recursive step of Cudd_MinHammingDist.
1834 It is based on the following identity. Let H(f) be the
1835 minimum Hamming distance of the minterms of f from the reference
1838 H(f) = min(H(f0)+h0,H(f1)+h1)
1840 where f0 and f1 are the two cofactors of f with respect to its top
1841 variable; h0 is 1 if the minterm assigns 1 to the top variable of f;
1842 h1 is 1 if the minterm assigns 0 to the top variable of f.
1843 The upper bound on the distance is used to bound the depth of the
1845 Returns the minimum distance unless it exceeds the upper bound or
1850 SeeAlso [Cudd_MinHammingDist]
1852 ******************************************************************************/
1854 cuddMinHammingDistRecur(
1857 DdHashTable
* table
,
1860 DdNode
*F
, *Ft
, *Fe
;
1863 DdManager
*dd
= table
->manager
;
1866 if (upperBound
== 0) return(0);
1868 F
= Cudd_Regular(f
);
1870 if (cuddIsConstant(F
)) {
1871 zero
= Cudd_Not(DD_ONE(dd
));
1872 if (f
== dd
->background
|| f
== zero
) {
1878 if ((res
= cuddHashTableLookup1(table
,f
)) != NULL
) {
1880 if (res
->ref
== 0) {
1882 dd
->constants
.dead
++;
1887 Ft
= cuddT(F
); Fe
= cuddE(F
);
1888 if (Cudd_IsComplement(f
)) {
1889 Ft
= Cudd_Not(Ft
); Fe
= Cudd_Not(Fe
);
1891 if (minterm
[F
->index
] == 0) {
1896 hT
= cuddMinHammingDistRecur(Ft
,minterm
,table
,upperBound
);
1897 if (hT
== CUDD_OUT_OF_MEM
) return(CUDD_OUT_OF_MEM
);
1901 hE
= cuddMinHammingDistRecur(Fe
,minterm
,table
,upperBound
- 1);
1902 if (hE
== CUDD_OUT_OF_MEM
) return(CUDD_OUT_OF_MEM
);
1904 h
= ddMin(hT
, hE
+ 1);
1907 ptrint fanout
= (ptrint
) F
->ref
;
1909 res
= cuddUniqueConst(dd
, (CUDD_VALUE_TYPE
) h
);
1910 if (!cuddHashTableInsert1(table
,f
,res
,fanout
)) {
1911 cuddRef(res
); Cudd_RecursiveDeref(dd
, res
);
1912 return(CUDD_OUT_OF_MEM
);
1918 } /* end of cuddMinHammingDistRecur */
1921 /**Function********************************************************************
1923 Synopsis [Separates cube from distance.]
1925 Description [Separates cube from distance. Returns the cube if
1926 successful; NULL otherwise.]
1928 SideEffects [The distance is returned as a side effect.]
1930 SeeAlso [cuddBddClosestCube createResult]
1932 ******************************************************************************/
1937 CUDD_VALUE_TYPE
*distance
)
1941 /* One and zero are special cases because the distance is implied. */
1942 if (Cudd_IsConstant(f
)) {
1943 *distance
= (f
== DD_ONE(dd
)) ? 0.0 :
1944 (1.0 + (CUDD_VALUE_TYPE
) CUDD_CONST_INDEX
);
1948 /* Find out which branch points to the distance and replace the top
1949 ** node with one pointing to zero instead. */
1951 if (Cudd_IsConstant(t
) && cuddV(t
) <= 0) {
1953 assert(!Cudd_IsConstant(cuddE(f
)) || cuddE(f
) == DD_ONE(dd
));
1955 *distance
= -cuddV(t
);
1956 cube
= cuddUniqueInter(dd
, f
->index
, DD_ZERO(dd
), cuddE(f
));
1959 assert(!Cudd_IsConstant(t
) || t
== DD_ONE(dd
));
1961 *distance
= -cuddV(cuddE(f
));
1962 cube
= cuddUniqueInter(dd
, f
->index
, t
, DD_ZERO(dd
));
1967 } /* end of separateCube */
1970 /**Function********************************************************************
1972 Synopsis [Builds a result for cache storage.]
1974 Description [Builds a result for cache storage. Returns a pointer
1975 to the resulting ADD if successful; NULL otherwise.]
1979 SeeAlso [cuddBddClosestCube separateCube]
1981 ******************************************************************************/
1988 CUDD_VALUE_TYPE distance
)
1990 DdNode
*res
, *constant
;
1992 /* Special case. The cube is either one or zero, and we do not
1993 ** add any variables. Hence, the result is also one or zero,
1994 ** and the distance remains implied by the value of the constant. */
1995 if (index
== CUDD_CONST_INDEX
&& Cudd_IsConstant(cube
)) return(cube
);
1997 constant
= cuddUniqueConst(dd
,-distance
);
1998 if (constant
== NULL
) return(NULL
);
2001 if (index
== CUDD_CONST_INDEX
) {
2002 /* Replace the top node. */
2003 if (cuddT(cube
) == DD_ZERO(dd
)) {
2004 res
= cuddUniqueInter(dd
,cube
->index
,constant
,cuddE(cube
));
2006 res
= cuddUniqueInter(dd
,cube
->index
,cuddT(cube
),constant
);
2009 /* Add a new top node. */
2011 assert(cuddI(dd
,index
) < cuddI(dd
,cube
->index
));
2014 res
= cuddUniqueInter(dd
,index
,cube
,constant
);
2016 res
= cuddUniqueInter(dd
,index
,constant
,cube
);
2020 Cudd_RecursiveDeref(dd
, constant
);
2023 cuddDeref(constant
); /* safe because constant is part of res */
2027 } /* end of createResult */