1 /**CFile***********************************************************************
2
3 FileName [cuddPriority.c]
4
5 PackageName [cudd]
6
7 Synopsis [Priority functions.]
8
9 Description [External procedures included in this file:
10 <ul>
11 <li> Cudd_PrioritySelect()
12 <li> Cudd_Xgty()
13 <li> Cudd_Xeqy()
14 <li> Cudd_addXeqy()
15 <li> Cudd_Dxygtdxz()
16 <li> Cudd_Dxygtdyz()
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()
24 </ul>
25 Internal procedures included in this module:
26 <ul>
27 <li> cuddCProjectionRecur()
28 <li> cuddBddClosestCube()
29 </ul>
30 Static procedures included in this module:
31 <ul>
32 <li> cuddMinHammingDistRecur()
33 <li> separateCube()
34 <li> createResult()
35 </ul>
36 ]
37
38 SeeAlso []
39
40 Author [Fabio Somenzi]
41
42 Copyright [Copyright (c) 1995-2012, Regents of the University of Colorado
43
44 All rights reserved.
45
46 Redistribution and use in source and binary forms, with or without
47 modification, are permitted provided that the following conditions
48 are met:
49
50 Redistributions of source code must retain the above copyright
51 notice, this list of conditions and the following disclaimer.
52
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.
56
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.
60
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.]
73
74 ******************************************************************************/
75
76 #include "util.h"
77 #include "cuddInt.h"
78
79
80 /*---------------------------------------------------------------------------*/
81 /* Constant declarations */
82 /*---------------------------------------------------------------------------*/
83
84 #define DD_DEBUG 1
85
86 /*---------------------------------------------------------------------------*/
87 /* Stucture declarations */
88 /*---------------------------------------------------------------------------*/
89
90
91 /*---------------------------------------------------------------------------*/
92 /* Type declarations */
93 /*---------------------------------------------------------------------------*/
94
95
96 /*---------------------------------------------------------------------------*/
97 /* Variable declarations */
98 /*---------------------------------------------------------------------------*/
99
100 #ifndef lint
101 static char rcsid[] DD_UNUSED = "$Id: cuddPriority.c,v 1.36 2012/02/05 01:07:19 fabio Exp $";
102 #endif
103
104 /*---------------------------------------------------------------------------*/
105 /* Macro declarations */
106 /*---------------------------------------------------------------------------*/
107
108
109 /**AutomaticStart*************************************************************/
110
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);
117
118 /**AutomaticEnd***************************************************************/
119
120
121 /*---------------------------------------------------------------------------*/
122 /* Definition of exported functions */
123 /*---------------------------------------------------------------------------*/
124
125
126 /**Function********************************************************************
127
128 Synopsis [Selects pairs from R using a priority function.]
129
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 vector
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
152 preferable:
153 <ul>
154 <li> When extracting representatives from an equivalence relation,
155 Cudd_CProjection has the advantage of nor requiring the auxiliary
156 variables.
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).
160 </ul>
161 ]
162
163 SideEffects [If called with z == NULL, will create new variables in
164 the manager.]
165
166 SeeAlso [Cudd_Dxygtdxz Cudd_Dxygtdyz Cudd_Xgty
167 Cudd_bddAdjPermuteX Cudd_CProjection]
168
169 ******************************************************************************/
170 DdNode *
Cudd_PrioritySelect(DdManager * dd,DdNode * R,DdNode ** x,DdNode ** y,DdNode ** z,DdNode * Pi,int n,DD_PRFP Pifunc)171 Cudd_PrioritySelect(
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 */)
180 {
181 DdNode *res = NULL;
182 DdNode *zcube = NULL;
183 DdNode *Rxz, *Q;
184 int createdZ = 0;
185 int createdPi = 0;
186 int i;
187
188 /* Create z variables if needed. */
189 if (z == NULL) {
190 if (Pi != NULL) return(NULL);
191 z = ALLOC(DdNode *,n);
192 if (z == NULL) {
193 dd->errorCode = CUDD_MEMORY_OUT;
194 return(NULL);
195 }
196 createdZ = 1;
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;
201 }
202 }
203
204 /* Create priority function BDD if needed. */
205 if (Pi == NULL) {
206 Pi = Pifunc(dd,n,x,y,z);
207 if (Pi == NULL) goto endgame;
208 createdPi = 1;
209 cuddRef(Pi);
210 }
211
212 /* Initialize abstraction cube. */
213 zcube = DD_ONE(dd);
214 cuddRef(zcube);
215 for (i = n - 1; i >= 0; i--) {
216 DdNode *tmpp;
217 tmpp = Cudd_bddAnd(dd,z[i],zcube);
218 if (tmpp == NULL) goto endgame;
219 cuddRef(tmpp);
220 Cudd_RecursiveDeref(dd,zcube);
221 zcube = tmpp;
222 }
223
224 /* Compute subset of (x,y) pairs. */
225 Rxz = Cudd_bddSwapVariables(dd,R,y,z,n);
226 if (Rxz == NULL) goto endgame;
227 cuddRef(Rxz);
228 Q = Cudd_bddAndAbstract(dd,Rxz,Pi,zcube);
229 if (Q == NULL) {
230 Cudd_RecursiveDeref(dd,Rxz);
231 goto endgame;
232 }
233 cuddRef(Q);
234 Cudd_RecursiveDeref(dd,Rxz);
235 res = Cudd_bddAnd(dd,R,Cudd_Not(Q));
236 if (res == NULL) {
237 Cudd_RecursiveDeref(dd,Q);
238 goto endgame;
239 }
240 cuddRef(res);
241 Cudd_RecursiveDeref(dd,Q);
242
243 endgame:
244 if (zcube != NULL) Cudd_RecursiveDeref(dd,zcube);
245 if (createdZ) {
246 FREE(z);
247 }
248 if (createdPi) {
249 Cudd_RecursiveDeref(dd,Pi);
250 }
251 if (res != NULL) cuddDeref(res);
252 return(res);
253
254 } /* Cudd_PrioritySelect */
255
256
257 /**Function********************************************************************
258
259 Synopsis [Generates a BDD for the function x > y.]
260
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.]
269
270 SideEffects [None]
271
272 SeeAlso [Cudd_PrioritySelect Cudd_Dxygtdxz Cudd_Dxygtdyz]
273
274 ******************************************************************************/
275 DdNode *
Cudd_Xgty(DdManager * dd,int N,DdNode ** z,DdNode ** x,DdNode ** y)276 Cudd_Xgty(
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 */)
282 {
283 DdNode *u, *v, *w;
284 int i;
285
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);
289 cuddRef(u);
290
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));
294 if (v == NULL) {
295 Cudd_RecursiveDeref(dd, u);
296 return(NULL);
297 }
298 cuddRef(v);
299 w = Cudd_bddAnd(dd, Cudd_Not(y[i]), u);
300 if (w == NULL) {
301 Cudd_RecursiveDeref(dd, u);
302 Cudd_RecursiveDeref(dd, v);
303 return(NULL);
304 }
305 cuddRef(w);
306 Cudd_RecursiveDeref(dd, u);
307 u = Cudd_bddIte(dd, x[i], Cudd_Not(v), w);
308 if (u == NULL) {
309 Cudd_RecursiveDeref(dd, v);
310 Cudd_RecursiveDeref(dd, w);
311 return(NULL);
312 }
313 cuddRef(u);
314 Cudd_RecursiveDeref(dd, v);
315 Cudd_RecursiveDeref(dd, w);
316
317 }
318 cuddDeref(u);
319 return(u);
320
321 } /* end of Cudd_Xgty */
322
323
324 /**Function********************************************************************
325
326 Synopsis [Generates a BDD for the function x==y.]
327
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\]. ]
334
335 SideEffects [None]
336
337 SeeAlso [Cudd_addXeqy]
338
339 ******************************************************************************/
340 DdNode *
Cudd_Xeqy(DdManager * dd,int N,DdNode ** x,DdNode ** y)341 Cudd_Xeqy(
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 */)
346 {
347 DdNode *u, *v, *w;
348 int i;
349
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);
353 cuddRef(u);
354
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);
358 if (v == NULL) {
359 Cudd_RecursiveDeref(dd, u);
360 return(NULL);
361 }
362 cuddRef(v);
363 w = Cudd_bddAnd(dd, Cudd_Not(y[i]), u);
364 if (w == NULL) {
365 Cudd_RecursiveDeref(dd, u);
366 Cudd_RecursiveDeref(dd, v);
367 return(NULL);
368 }
369 cuddRef(w);
370 Cudd_RecursiveDeref(dd, u);
371 u = Cudd_bddIte(dd, x[i], v, w);
372 if (u == NULL) {
373 Cudd_RecursiveDeref(dd, v);
374 Cudd_RecursiveDeref(dd, w);
375 return(NULL);
376 }
377 cuddRef(u);
378 Cudd_RecursiveDeref(dd, v);
379 Cudd_RecursiveDeref(dd, w);
380 }
381 cuddDeref(u);
382 return(u);
383
384 } /* end of Cudd_Xeqy */
385
386
387 /**Function********************************************************************
388
389 Synopsis [Generates an ADD for the function x==y.]
390
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\]. ]
397
398 SideEffects [None]
399
400 SeeAlso [Cudd_Xeqy]
401
402 ******************************************************************************/
403 DdNode *
Cudd_addXeqy(DdManager * dd,int N,DdNode ** x,DdNode ** y)404 Cudd_addXeqy(
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 */)
409 {
410 DdNode *one, *zero;
411 DdNode *u, *v, *w;
412 int i;
413
414 one = DD_ONE(dd);
415 zero = DD_ZERO(dd);
416
417 /* Build bottom part of ADD outside loop. */
418 v = Cudd_addIte(dd, y[N-1], one, zero);
419 if (v == NULL) return(NULL);
420 cuddRef(v);
421 w = Cudd_addIte(dd, y[N-1], zero, one);
422 if (w == NULL) {
423 Cudd_RecursiveDeref(dd, v);
424 return(NULL);
425 }
426 cuddRef(w);
427 u = Cudd_addIte(dd, x[N-1], v, w);
428 if (u == NULL) {
429 Cudd_RecursiveDeref(dd, v);
430 Cudd_RecursiveDeref(dd, w);
431 return(NULL);
432 }
433 cuddRef(u);
434 Cudd_RecursiveDeref(dd, v);
435 Cudd_RecursiveDeref(dd, w);
436
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);
440 if (v == NULL) {
441 Cudd_RecursiveDeref(dd, u);
442 return(NULL);
443 }
444 cuddRef(v);
445 w = Cudd_addIte(dd, y[i], zero, u);
446 if (w == NULL) {
447 Cudd_RecursiveDeref(dd, u);
448 Cudd_RecursiveDeref(dd, v);
449 return(NULL);
450 }
451 cuddRef(w);
452 Cudd_RecursiveDeref(dd, u);
453 u = Cudd_addIte(dd, x[i], v, w);
454 if (w == NULL) {
455 Cudd_RecursiveDeref(dd, v);
456 Cudd_RecursiveDeref(dd, w);
457 return(NULL);
458 }
459 cuddRef(u);
460 Cudd_RecursiveDeref(dd, v);
461 Cudd_RecursiveDeref(dd, w);
462 }
463 cuddDeref(u);
464 return(u);
465
466 } /* end of Cudd_addXeqy */
467
468
469 /**Function********************************************************************
470
471 Synopsis [Generates a BDD for the function d(x,y) > d(x,z).]
472
473 Description [This function generates a BDD for the function d(x,y)
474 > d(x,z);
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\]. ]
483
484 SideEffects [None]
485
486 SeeAlso [Cudd_PrioritySelect Cudd_Dxygtdyz Cudd_Xgty Cudd_bddAdjPermuteX]
487
488 ******************************************************************************/
489 DdNode *
Cudd_Dxygtdxz(DdManager * dd,int N,DdNode ** x,DdNode ** y,DdNode ** z)490 Cudd_Dxygtdxz(
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 */)
496 {
497 DdNode *one, *zero;
498 DdNode *z1, *z2, *z3, *z4, *y1_, *y2, *x1;
499 int i;
500
501 one = DD_ONE(dd);
502 zero = Cudd_Not(one);
503
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);
507 cuddRef(y1_);
508 y2 = Cudd_bddIte(dd, y[N-1], z[N-1], one);
509 if (y2 == NULL) {
510 Cudd_RecursiveDeref(dd, y1_);
511 return(NULL);
512 }
513 cuddRef(y2);
514 x1 = Cudd_bddIte(dd, x[N-1], y1_, y2);
515 if (x1 == NULL) {
516 Cudd_RecursiveDeref(dd, y1_);
517 Cudd_RecursiveDeref(dd, y2);
518 return(NULL);
519 }
520 cuddRef(x1);
521 Cudd_RecursiveDeref(dd, y1_);
522 Cudd_RecursiveDeref(dd, y2);
523
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));
527 if (z1 == NULL) {
528 Cudd_RecursiveDeref(dd, x1);
529 return(NULL);
530 }
531 cuddRef(z1);
532 z2 = Cudd_bddIte(dd, z[i], x1, one);
533 if (z2 == NULL) {
534 Cudd_RecursiveDeref(dd, x1);
535 Cudd_RecursiveDeref(dd, z1);
536 return(NULL);
537 }
538 cuddRef(z2);
539 z3 = Cudd_bddIte(dd, z[i], one, x1);
540 if (z3 == NULL) {
541 Cudd_RecursiveDeref(dd, x1);
542 Cudd_RecursiveDeref(dd, z1);
543 Cudd_RecursiveDeref(dd, z2);
544 return(NULL);
545 }
546 cuddRef(z3);
547 z4 = Cudd_bddIte(dd, z[i], x1, zero);
548 if (z4 == NULL) {
549 Cudd_RecursiveDeref(dd, x1);
550 Cudd_RecursiveDeref(dd, z1);
551 Cudd_RecursiveDeref(dd, z2);
552 Cudd_RecursiveDeref(dd, z3);
553 return(NULL);
554 }
555 cuddRef(z4);
556 Cudd_RecursiveDeref(dd, x1);
557 y1_ = Cudd_bddIte(dd, y[i], z2, Cudd_Not(z1));
558 if (y1_ == NULL) {
559 Cudd_RecursiveDeref(dd, z1);
560 Cudd_RecursiveDeref(dd, z2);
561 Cudd_RecursiveDeref(dd, z3);
562 Cudd_RecursiveDeref(dd, z4);
563 return(NULL);
564 }
565 cuddRef(y1_);
566 y2 = Cudd_bddIte(dd, y[i], z4, z3);
567 if (y2 == NULL) {
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_);
573 return(NULL);
574 }
575 cuddRef(y2);
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);
581 if (x1 == NULL) {
582 Cudd_RecursiveDeref(dd, y1_);
583 Cudd_RecursiveDeref(dd, y2);
584 return(NULL);
585 }
586 cuddRef(x1);
587 Cudd_RecursiveDeref(dd, y1_);
588 Cudd_RecursiveDeref(dd, y2);
589 }
590 cuddDeref(x1);
591 return(Cudd_Not(x1));
592
593 } /* end of Cudd_Dxygtdxz */
594
595
596 /**Function********************************************************************
597
598 Synopsis [Generates a BDD for the function d(x,y) > d(y,z).]
599
600 Description [This function generates a BDD for the function d(x,y)
601 > d(y,z);
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\]. ]
610
611 SideEffects [None]
612
613 SeeAlso [Cudd_PrioritySelect Cudd_Dxygtdxz Cudd_Xgty Cudd_bddAdjPermuteX]
614
615 ******************************************************************************/
616 DdNode *
Cudd_Dxygtdyz(DdManager * dd,int N,DdNode ** x,DdNode ** y,DdNode ** z)617 Cudd_Dxygtdyz(
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 */)
623 {
624 DdNode *one, *zero;
625 DdNode *z1, *z2, *z3, *z4, *y1_, *y2, *x1;
626 int i;
627
628 one = DD_ONE(dd);
629 zero = Cudd_Not(one);
630
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);
634 cuddRef(y1_);
635 y2 = Cudd_bddIte(dd, y[N-1], z[N-1], zero);
636 if (y2 == NULL) {
637 Cudd_RecursiveDeref(dd, y1_);
638 return(NULL);
639 }
640 cuddRef(y2);
641 x1 = Cudd_bddIte(dd, x[N-1], y1_, Cudd_Not(y2));
642 if (x1 == NULL) {
643 Cudd_RecursiveDeref(dd, y1_);
644 Cudd_RecursiveDeref(dd, y2);
645 return(NULL);
646 }
647 cuddRef(x1);
648 Cudd_RecursiveDeref(dd, y1_);
649 Cudd_RecursiveDeref(dd, y2);
650
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);
654 if (z1 == NULL) {
655 Cudd_RecursiveDeref(dd, x1);
656 return(NULL);
657 }
658 cuddRef(z1);
659 z2 = Cudd_bddIte(dd, z[i], x1, one);
660 if (z2 == NULL) {
661 Cudd_RecursiveDeref(dd, x1);
662 Cudd_RecursiveDeref(dd, z1);
663 return(NULL);
664 }
665 cuddRef(z2);
666 z3 = Cudd_bddIte(dd, z[i], one, x1);
667 if (z3 == NULL) {
668 Cudd_RecursiveDeref(dd, x1);
669 Cudd_RecursiveDeref(dd, z1);
670 Cudd_RecursiveDeref(dd, z2);
671 return(NULL);
672 }
673 cuddRef(z3);
674 z4 = Cudd_bddIte(dd, z[i], one, Cudd_Not(x1));
675 if (z4 == NULL) {
676 Cudd_RecursiveDeref(dd, x1);
677 Cudd_RecursiveDeref(dd, z1);
678 Cudd_RecursiveDeref(dd, z2);
679 Cudd_RecursiveDeref(dd, z3);
680 return(NULL);
681 }
682 cuddRef(z4);
683 Cudd_RecursiveDeref(dd, x1);
684 y1_ = Cudd_bddIte(dd, y[i], z2, z1);
685 if (y1_ == NULL) {
686 Cudd_RecursiveDeref(dd, z1);
687 Cudd_RecursiveDeref(dd, z2);
688 Cudd_RecursiveDeref(dd, z3);
689 Cudd_RecursiveDeref(dd, z4);
690 return(NULL);
691 }
692 cuddRef(y1_);
693 y2 = Cudd_bddIte(dd, y[i], z4, Cudd_Not(z3));
694 if (y2 == NULL) {
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_);
700 return(NULL);
701 }
702 cuddRef(y2);
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));
708 if (x1 == NULL) {
709 Cudd_RecursiveDeref(dd, y1_);
710 Cudd_RecursiveDeref(dd, y2);
711 return(NULL);
712 }
713 cuddRef(x1);
714 Cudd_RecursiveDeref(dd, y1_);
715 Cudd_RecursiveDeref(dd, y2);
716 }
717 cuddDeref(x1);
718 return(Cudd_Not(x1));
719
720 } /* end of Cudd_Dxygtdyz */
721
722
723 /**Function********************************************************************
724
725 Synopsis [Generates a BDD for the function x - y ≥ c.]
726
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\].]
733
734 SideEffects [None]
735
736 SeeAlso [Cudd_Xgty]
737
738 ******************************************************************************/
739 DdNode *
Cudd_Inequality(DdManager * dd,int N,int c,DdNode ** x,DdNode ** y)740 Cudd_Inequality(
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 */)
746 {
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. */
750 int kTrue = c;
751 int kFalse = c - 1;
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. */
755 int mask = 1;
756 int i;
757
758 DdNode *f = NULL; /* the eventual result */
759 DdNode *one = DD_ONE(dd);
760 DdNode *zero = Cudd_Not(one);
761
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.
765 */
766 DdNode *map[2];
767 int invalidIndex = 1 << (N-1);
768 int index[2] = {invalidIndex, invalidIndex};
769
770 /* This should never happen. */
771 if (N < 0) return(NULL);
772
773 /* If there are no bits, both operands are 0. The result depends on c. */
774 if (N == 0) {
775 if (c >= 0) return(one);
776 else return(zero);
777 }
778
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);
782
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;
788 int j;
789 DdNode *newMap[2];
790 int newIndex[2];
791
792 kTrueLower = kTrue;
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;
801
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;
805
806 /* Find f- */
807 leftChild = (j << 1) - 1;
808 if (leftChild >= kTrueLower) {
809 fminus = one;
810 } else if (leftChild <= kFalseLower) {
811 fminus = zero;
812 } else {
813 assert(leftChild == index[0] || leftChild == index[1]);
814 if (leftChild == index[0]) {
815 fminus = map[0];
816 } else {
817 fminus = map[1];
818 }
819 }
820
821 /* Find f= */
822 middleChild = j << 1;
823 if (middleChild >= kTrueLower) {
824 fequal = one;
825 } else if (middleChild <= kFalseLower) {
826 fequal = zero;
827 } else {
828 assert(middleChild == index[0] || middleChild == index[1]);
829 if (middleChild == index[0]) {
830 fequal = map[0];
831 } else {
832 fequal = map[1];
833 }
834 }
835
836 /* Find f+ */
837 rightChild = (j << 1) + 1;
838 if (rightChild >= kTrueLower) {
839 fplus = one;
840 } else if (rightChild <= kFalseLower) {
841 fplus = zero;
842 } else {
843 assert(rightChild == index[0] || rightChild == index[1]);
844 if (rightChild == index[0]) {
845 fplus = map[0];
846 } else {
847 fplus = map[1];
848 }
849 }
850
851 /* Build new nodes. */
852 g1 = Cudd_bddIte(dd, y[N - i], fequal, fplus);
853 if (g1 == NULL) {
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]);
858 return(NULL);
859 }
860 cuddRef(g1);
861 g0 = Cudd_bddIte(dd, y[N - i], fminus, fequal);
862 if (g0 == NULL) {
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]);
868 return(NULL);
869 }
870 cuddRef(g0);
871 f = Cudd_bddIte(dd, x[N - i], g1, g0);
872 if (f == NULL) {
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]);
879 return(NULL);
880 }
881 cuddRef(f);
882 Cudd_IterDerefBdd(dd, g1);
883 Cudd_IterDerefBdd(dd, g0);
884
885 /* Save newly computed node in map. */
886 assert(newIndex[0] == invalidIndex || newIndex[1] == invalidIndex);
887 if (newIndex[0] == invalidIndex) {
888 newIndex[0] = j;
889 newMap[0] = f;
890 } else {
891 newIndex[1] = j;
892 newMap[1] = f;
893 }
894 }
895
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]);
899 map[0] = newMap[0];
900 map[1] = newMap[1];
901 index[0] = newIndex[0];
902 index[1] = newIndex[1];
903 }
904
905 cuddDeref(f);
906 return(f);
907
908 } /* end of Cudd_Inequality */
909
910
911 /**Function********************************************************************
912
913 Synopsis [Generates a BDD for the function x - y != c.]
914
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\].]
921
922 SideEffects [None]
923
924 SeeAlso [Cudd_Xgty]
925
926 ******************************************************************************/
927 DdNode *
Cudd_Disequality(DdManager * dd,int N,int c,DdNode ** x,DdNode ** y)928 Cudd_Disequality(
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 */)
934 {
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. */
938 int kTrueLb = c + 1;
939 int kTrueUb = c - 1;
940 int kFalse = c;
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. */
944 int mask = 1;
945 int i;
946
947 DdNode *f = NULL; /* the eventual result */
948 DdNode *one = DD_ONE(dd);
949 DdNode *zero = Cudd_Not(one);
950
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.
954 */
955 DdNode *map[2];
956 int invalidIndex = 1 << (N-1);
957 int index[2] = {invalidIndex, invalidIndex};
958
959 /* This should never happen. */
960 if (N < 0) return(NULL);
961
962 /* If there are no bits, both operands are 0. The result depends on c. */
963 if (N == 0) {
964 if (c != 0) return(one);
965 else return(zero);
966 }
967
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);
970
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;
976 int j;
977 DdNode *newMap[2];
978 int newIndex[2];
979
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;
989
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;
993
994 /* Find f- */
995 leftChild = (j << 1) - 1;
996 if (leftChild >= kTrueLbLower || leftChild <= kTrueUbLower) {
997 fminus = one;
998 } else if (i == 1 && leftChild == kFalse) {
999 fminus = zero;
1000 } else {
1001 assert(leftChild == index[0] || leftChild == index[1]);
1002 if (leftChild == index[0]) {
1003 fminus = map[0];
1004 } else {
1005 fminus = map[1];
1006 }
1007 }
1008
1009 /* Find f= */
1010 middleChild = j << 1;
1011 if (middleChild >= kTrueLbLower || middleChild <= kTrueUbLower) {
1012 fequal = one;
1013 } else if (i == 1 && middleChild == kFalse) {
1014 fequal = zero;
1015 } else {
1016 assert(middleChild == index[0] || middleChild == index[1]);
1017 if (middleChild == index[0]) {
1018 fequal = map[0];
1019 } else {
1020 fequal = map[1];
1021 }
1022 }
1023
1024 /* Find f+ */
1025 rightChild = (j << 1) + 1;
1026 if (rightChild >= kTrueLbLower || rightChild <= kTrueUbLower) {
1027 fplus = one;
1028 } else if (i == 1 && rightChild == kFalse) {
1029 fplus = zero;
1030 } else {
1031 assert(rightChild == index[0] || rightChild == index[1]);
1032 if (rightChild == index[0]) {
1033 fplus = map[0];
1034 } else {
1035 fplus = map[1];
1036 }
1037 }
1038
1039 /* Build new nodes. */
1040 g1 = Cudd_bddIte(dd, y[N - i], fequal, fplus);
1041 if (g1 == NULL) {
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]);
1046 return(NULL);
1047 }
1048 cuddRef(g1);
1049 g0 = Cudd_bddIte(dd, y[N - i], fminus, fequal);
1050 if (g0 == NULL) {
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]);
1056 return(NULL);
1057 }
1058 cuddRef(g0);
1059 f = Cudd_bddIte(dd, x[N - i], g1, g0);
1060 if (f == NULL) {
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]);
1067 return(NULL);
1068 }
1069 cuddRef(f);
1070 Cudd_IterDerefBdd(dd, g1);
1071 Cudd_IterDerefBdd(dd, g0);
1072
1073 /* Save newly computed node in map. */
1074 assert(newIndex[0] == invalidIndex || newIndex[1] == invalidIndex);
1075 if (newIndex[0] == invalidIndex) {
1076 newIndex[0] = j;
1077 newMap[0] = f;
1078 } else {
1079 newIndex[1] = j;
1080 newMap[1] = f;
1081 }
1082 }
1083
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]);
1087 map[0] = newMap[0];
1088 map[1] = newMap[1];
1089 index[0] = newIndex[0];
1090 index[1] = newIndex[1];
1091 }
1092
1093 cuddDeref(f);
1094 return(f);
1095
1096 } /* end of Cudd_Disequality */
1097
1098
1099 /**Function********************************************************************
1100
1101 Synopsis [Generates a BDD for the function lowerB ≤ x ≤ upperB.]
1102
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.]
1110
1111 SideEffects [None]
1112
1113 SeeAlso [Cudd_Xgty]
1114
1115 ******************************************************************************/
1116 DdNode *
Cudd_bddInterval(DdManager * dd,int N,DdNode ** x,unsigned int lowerB,unsigned int upperB)1117 Cudd_bddInterval(
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 */)
1123 {
1124 DdNode *one, *zero;
1125 DdNode *r, *rl, *ru;
1126 int i;
1127
1128 one = DD_ONE(dd);
1129 zero = Cudd_Not(one);
1130
1131 rl = one;
1132 cuddRef(rl);
1133 ru = one;
1134 cuddRef(ru);
1135
1136 /* Loop to build the rest of the BDDs. */
1137 for (i = N-1; i >= 0; i--) {
1138 DdNode *vl, *vu;
1139 vl = Cudd_bddIte(dd, x[i],
1140 lowerB&1 ? rl : one,
1141 lowerB&1 ? zero : rl);
1142 if (vl == NULL) {
1143 Cudd_IterDerefBdd(dd, rl);
1144 Cudd_IterDerefBdd(dd, ru);
1145 return(NULL);
1146 }
1147 cuddRef(vl);
1148 Cudd_IterDerefBdd(dd, rl);
1149 rl = vl;
1150 lowerB >>= 1;
1151 vu = Cudd_bddIte(dd, x[i],
1152 upperB&1 ? ru : zero,
1153 upperB&1 ? one : ru);
1154 if (vu == NULL) {
1155 Cudd_IterDerefBdd(dd, rl);
1156 Cudd_IterDerefBdd(dd, ru);
1157 return(NULL);
1158 }
1159 cuddRef(vu);
1160 Cudd_IterDerefBdd(dd, ru);
1161 ru = vu;
1162 upperB >>= 1;
1163 }
1164
1165 /* Conjoin the two bounds. */
1166 r = Cudd_bddAnd(dd, rl, ru);
1167 if (r == NULL) {
1168 Cudd_IterDerefBdd(dd, rl);
1169 Cudd_IterDerefBdd(dd, ru);
1170 return(NULL);
1171 }
1172 cuddRef(r);
1173 Cudd_IterDerefBdd(dd, rl);
1174 Cudd_IterDerefBdd(dd, ru);
1175 cuddDeref(r);
1176 return(r);
1177
1178 } /* end of Cudd_bddInterval */
1179
1180
1181 /**Function********************************************************************
1182
1183 Synopsis [Computes the compatible projection of R w.r.t. cube Y.]
1184
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.]
1189
1190 SideEffects [None]
1191
1192 SeeAlso [Cudd_PrioritySelect]
1193
1194 ******************************************************************************/
1195 DdNode *
Cudd_CProjection(DdManager * dd,DdNode * R,DdNode * Y)1196 Cudd_CProjection(
1197 DdManager * dd,
1198 DdNode * R,
1199 DdNode * Y)
1200 {
1201 DdNode *res;
1202 DdNode *support;
1203
1204 if (Cudd_CheckCube(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;
1208 return(NULL);
1209 }
1210
1211 /* Compute the support of Y, which is used by the abstraction step
1212 ** in cuddCProjectionRecur.
1213 */
1214 support = Cudd_Support(dd,Y);
1215 if (support == NULL) return(NULL);
1216 cuddRef(support);
1217
1218 do {
1219 dd->reordered = 0;
1220 res = cuddCProjectionRecur(dd,R,Y,support);
1221 } while (dd->reordered == 1);
1222
1223 if (res == NULL) {
1224 Cudd_RecursiveDeref(dd,support);
1225 return(NULL);
1226 }
1227 cuddRef(res);
1228 Cudd_RecursiveDeref(dd,support);
1229 cuddDeref(res);
1230
1231 return(res);
1232
1233 } /* end of Cudd_CProjection */
1234
1235
1236 /**Function********************************************************************
1237
1238 Synopsis [Computes the Hamming distance ADD.]
1239
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.]
1244
1245 SideEffects [None]
1246
1247 SeeAlso []
1248
1249 ******************************************************************************/
1250 DdNode *
Cudd_addHamming(DdManager * dd,DdNode ** xVars,DdNode ** yVars,int nVars)1251 Cudd_addHamming(
1252 DdManager * dd,
1253 DdNode ** xVars,
1254 DdNode ** yVars,
1255 int nVars)
1256 {
1257 DdNode *result,*tempBdd;
1258 DdNode *tempAdd,*temp;
1259 int i;
1260
1261 result = DD_ZERO(dd);
1262 cuddRef(result);
1263
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);
1268 return(NULL);
1269 }
1270 cuddRef(tempBdd);
1271 tempAdd = Cudd_BddToAdd(dd,tempBdd);
1272 if (tempAdd == NULL) {
1273 Cudd_RecursiveDeref(dd,tempBdd);
1274 Cudd_RecursiveDeref(dd,result);
1275 return(NULL);
1276 }
1277 cuddRef(tempAdd);
1278 Cudd_RecursiveDeref(dd,tempBdd);
1279 temp = Cudd_addApply(dd,Cudd_addPlus,tempAdd,result);
1280 if (temp == NULL) {
1281 Cudd_RecursiveDeref(dd,tempAdd);
1282 Cudd_RecursiveDeref(dd,result);
1283 return(NULL);
1284 }
1285 cuddRef(temp);
1286 Cudd_RecursiveDeref(dd,tempAdd);
1287 Cudd_RecursiveDeref(dd,result);
1288 result = temp;
1289 }
1290
1291 cuddDeref(result);
1292 return(result);
1293
1294 } /* end of Cudd_addHamming */
1295
1296
1297 /**Function********************************************************************
1298
1299 Synopsis [Returns the minimum Hamming distance between f and minterm.]
1300
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.]
1307
1308 SideEffects [None]
1309
1310 SeeAlso [Cudd_addHamming Cudd_bddClosestCube]
1311
1312 ******************************************************************************/
1313 int
Cudd_MinHammingDist(DdManager * dd,DdNode * f,int * minterm,int upperBound)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 */)
1319 {
1320 DdHashTable *table;
1321 CUDD_VALUE_TYPE epsilon;
1322 int res;
1323
1324 table = cuddHashTableInit(dd,1,2);
1325 if (table == NULL) {
1326 return(CUDD_OUT_OF_MEM);
1327 }
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);
1333
1334 return(res);
1335
1336 } /* end of Cudd_MinHammingDist */
1337
1338
1339 /**Function********************************************************************
1340
1341 Synopsis [Finds a cube of f at minimum Hamming distance from g.]
1342
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
1347 otherwise.]
1348
1349 SideEffects [The distance is returned as a side effect.]
1350
1351 SeeAlso [Cudd_MinHammingDist]
1352
1353 ******************************************************************************/
1354 DdNode *
Cudd_bddClosestCube(DdManager * dd,DdNode * f,DdNode * g,int * distance)1355 Cudd_bddClosestCube(
1356 DdManager *dd,
1357 DdNode * f,
1358 DdNode *g,
1359 int *distance)
1360 {
1361 DdNode *res, *acube;
1362 CUDD_VALUE_TYPE rdist;
1363
1364 /* Compute the cube and distance as a single ADD. */
1365 do {
1366 dd->reordered = 0;
1367 res = cuddBddClosestCube(dd,f,g,CUDD_CONST_INDEX + 1.0);
1368 } while (dd->reordered == 1);
1369 if (res == NULL) return(NULL);
1370 cuddRef(res);
1371
1372 /* Unpack distance and cube. */
1373 do {
1374 dd->reordered = 0;
1375 acube = separateCube(dd, res, &rdist);
1376 } while (dd->reordered == 1);
1377 if (acube == NULL) {
1378 Cudd_RecursiveDeref(dd, res);
1379 return(NULL);
1380 }
1381 cuddRef(acube);
1382 Cudd_RecursiveDeref(dd, res);
1383
1384 /* Convert cube from ADD to BDD. */
1385 do {
1386 dd->reordered = 0;
1387 res = cuddAddBddDoPattern(dd, acube);
1388 } while (dd->reordered == 1);
1389 if (res == NULL) {
1390 Cudd_RecursiveDeref(dd, acube);
1391 return(NULL);
1392 }
1393 cuddRef(res);
1394 Cudd_RecursiveDeref(dd, acube);
1395
1396 *distance = (int) rdist;
1397 cuddDeref(res);
1398 return(res);
1399
1400 } /* end of Cudd_bddClosestCube */
1401
1402
1403 /*---------------------------------------------------------------------------*/
1404 /* Definition of internal functions */
1405 /*---------------------------------------------------------------------------*/
1406
1407
1408 /**Function********************************************************************
1409
1410 Synopsis [Performs the recursive step of Cudd_CProjection.]
1411
1412 Description [Performs the recursive step of Cudd_CProjection. Returns
1413 the projection if successful; NULL otherwise.]
1414
1415 SideEffects [None]
1416
1417 SeeAlso [Cudd_CProjection]
1418
1419 ******************************************************************************/
1420 DdNode *
cuddCProjectionRecur(DdManager * dd,DdNode * R,DdNode * Y,DdNode * Ysupp)1421 cuddCProjectionRecur(
1422 DdManager * dd,
1423 DdNode * R,
1424 DdNode * Y,
1425 DdNode * Ysupp)
1426 {
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);
1431
1432 statLine(dd);
1433 if (Y == one) return(R);
1434
1435 #ifdef DD_DEBUG
1436 assert(!Cudd_IsConstant(Y));
1437 #endif
1438
1439 if (R == Cudd_Not(one)) return(R);
1440
1441 res = cuddCacheLookup2(dd, Cudd_CProjection, R, Y);
1442 if (res != NULL) return(res);
1443
1444 r = Cudd_Regular(R);
1445 topR = cuddI(dd,r->index);
1446 y = Cudd_Regular(Y);
1447 topY = cuddI(dd,y->index);
1448
1449 top = ddMin(topR, topY);
1450
1451 /* Compute the cofactors of R */
1452 if (topR == top) {
1453 index = r->index;
1454 RT = cuddT(r);
1455 RE = cuddE(r);
1456 if (r != R) {
1457 RT = Cudd_Not(RT); RE = Cudd_Not(RE);
1458 }
1459 } else {
1460 RT = RE = R;
1461 }
1462
1463 if (topY > top) {
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.
1467 */
1468 res1 = cuddCProjectionRecur(dd,RT,Y,Ysupp);
1469 if (res1 == NULL) return(NULL);
1470 cuddRef(res1);
1471 res2 = cuddCProjectionRecur(dd,RE,Y,Ysupp);
1472 if (res2 == NULL) {
1473 Cudd_RecursiveDeref(dd,res1);
1474 return(NULL);
1475 }
1476 cuddRef(res2);
1477 res = cuddBddIteRecur(dd, dd->vars[index], res1, res2);
1478 if (res == NULL) {
1479 Cudd_RecursiveDeref(dd,res1);
1480 Cudd_RecursiveDeref(dd,res2);
1481 return(NULL);
1482 }
1483 /* If we have reached this point, res1 and res2 are now
1484 ** incorporated in res. cuddDeref is therefore sufficient.
1485 */
1486 cuddDeref(res1);
1487 cuddDeref(res2);
1488 } else {
1489 /* Compute the cofactors of Y */
1490 index = y->index;
1491 YT = cuddT(y);
1492 YE = cuddE(y);
1493 if (y != Y) {
1494 YT = Cudd_Not(YT); YE = Cudd_Not(YE);
1495 }
1496 if (YT == Cudd_Not(one)) {
1497 Alpha = Cudd_Not(dd->vars[index]);
1498 Yrest = YE;
1499 Ra = RE;
1500 Ran = RT;
1501 } else {
1502 Alpha = dd->vars[index];
1503 Yrest = YT;
1504 Ra = RT;
1505 Ran = RE;
1506 }
1507 Gamma = cuddBddExistAbstractRecur(dd,Ra,cuddT(Ysupp));
1508 if (Gamma == NULL) return(NULL);
1509 if (Gamma == one) {
1510 res1 = cuddCProjectionRecur(dd,Ra,Yrest,cuddT(Ysupp));
1511 if (res1 == NULL) return(NULL);
1512 cuddRef(res1);
1513 res = cuddBddAndRecur(dd, Alpha, res1);
1514 if (res == NULL) {
1515 Cudd_RecursiveDeref(dd,res1);
1516 return(NULL);
1517 }
1518 cuddDeref(res1);
1519 } else if (Gamma == Cudd_Not(one)) {
1520 res1 = cuddCProjectionRecur(dd,Ran,Yrest,cuddT(Ysupp));
1521 if (res1 == NULL) return(NULL);
1522 cuddRef(res1);
1523 res = cuddBddAndRecur(dd, Cudd_Not(Alpha), res1);
1524 if (res == NULL) {
1525 Cudd_RecursiveDeref(dd,res1);
1526 return(NULL);
1527 }
1528 cuddDeref(res1);
1529 } else {
1530 cuddRef(Gamma);
1531 resA = cuddCProjectionRecur(dd,Ran,Yrest,cuddT(Ysupp));
1532 if (resA == NULL) {
1533 Cudd_RecursiveDeref(dd,Gamma);
1534 return(NULL);
1535 }
1536 cuddRef(resA);
1537 res2 = cuddBddAndRecur(dd, Cudd_Not(Gamma), resA);
1538 if (res2 == NULL) {
1539 Cudd_RecursiveDeref(dd,Gamma);
1540 Cudd_RecursiveDeref(dd,resA);
1541 return(NULL);
1542 }
1543 cuddRef(res2);
1544 Cudd_RecursiveDeref(dd,Gamma);
1545 Cudd_RecursiveDeref(dd,resA);
1546 res1 = cuddCProjectionRecur(dd,Ra,Yrest,cuddT(Ysupp));
1547 if (res1 == NULL) {
1548 Cudd_RecursiveDeref(dd,res2);
1549 return(NULL);
1550 }
1551 cuddRef(res1);
1552 res = cuddBddIteRecur(dd, Alpha, res1, res2);
1553 if (res == NULL) {
1554 Cudd_RecursiveDeref(dd,res1);
1555 Cudd_RecursiveDeref(dd,res2);
1556 return(NULL);
1557 }
1558 cuddDeref(res1);
1559 cuddDeref(res2);
1560 }
1561 }
1562
1563 cuddCacheInsert2(dd,Cudd_CProjection,R,Y,res);
1564
1565 return(res);
1566
1567 } /* end of cuddCProjectionRecur */
1568
1569
1570 /**Function********************************************************************
1571
1572 Synopsis [Performs the recursive step of Cudd_bddClosestCube.]
1573
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.
1578 <pre>
1579 H(f,g) = min(H(ft,gt), H(fe,ge), H(ft,ge)+1, H(fe,gt)+1)
1580 </pre>
1581 Bounding is based on the following observations.
1582 <ul>
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.)
1589 </ul>
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
1592 <pre>
1593 (bound == -1) and (F != not(G)) or (bound == 0) and (F == not(G)).
1594 </pre>
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
1598 <pre>
1599 bound < minD,
1600 </pre>
1601 except at the very beginning, when we have no value for
1602 <code>minD</code>.<p>
1603
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>
1609
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>
1614
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>
1618
1619 Suppose <code>gt == ge == g</code>. (That is, <code>g</code> does
1620 not depend on the top variable.) Then
1621 <pre>
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)) .
1624 </pre>
1625 Therefore, under these circumstances, we skip the two "cross" cases.<p>
1626
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
1634 zero).]
1635
1636 SideEffects [None]
1637
1638 SeeAlso [Cudd_bddClosestCube]
1639
1640 ******************************************************************************/
1641 DdNode *
cuddBddClosestCube(DdManager * dd,DdNode * f,DdNode * g,CUDD_VALUE_TYPE bound)1642 cuddBddClosestCube(
1643 DdManager *dd,
1644 DdNode *f,
1645 DdNode *g,
1646 CUDD_VALUE_TYPE bound)
1647 {
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;
1655
1656 statLine(dd);
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);
1661
1662 /* Check cache. */
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);
1668 }
1669
1670 topf = cuddI(dd,F->index);
1671 topg = cuddI(dd,G->index);
1672
1673 /* Compute cofactors. */
1674 if (topf <= topg) {
1675 index = F->index;
1676 ft = cuddT(F);
1677 fe = cuddE(F);
1678 if (Cudd_IsComplement(f)) {
1679 ft = Cudd_Not(ft);
1680 fe = Cudd_Not(fe);
1681 }
1682 } else {
1683 index = G->index;
1684 ft = fe = f;
1685 }
1686
1687 if (topg <= topf) {
1688 gt = cuddT(G);
1689 ge = cuddE(G);
1690 if (Cudd_IsComplement(g)) {
1691 gt = Cudd_Not(gt);
1692 ge = Cudd_Not(ge);
1693 }
1694 } else {
1695 gt = ge = g;
1696 }
1697
1698 tt = cuddBddClosestCube(dd,ft,gt,bound);
1699 if (tt == NULL) return(NULL);
1700 cuddRef(tt);
1701 ctt = separateCube(dd,tt,&dtt);
1702 if (ctt == NULL) {
1703 Cudd_RecursiveDeref(dd, tt);
1704 return(NULL);
1705 }
1706 cuddRef(ctt);
1707 Cudd_RecursiveDeref(dd, tt);
1708 minD = dtt;
1709 bound = ddMin(bound,minD);
1710
1711 ee = cuddBddClosestCube(dd,fe,ge,bound);
1712 if (ee == NULL) {
1713 Cudd_RecursiveDeref(dd, ctt);
1714 return(NULL);
1715 }
1716 cuddRef(ee);
1717 cee = separateCube(dd,ee,&dee);
1718 if (cee == NULL) {
1719 Cudd_RecursiveDeref(dd, ctt);
1720 Cudd_RecursiveDeref(dd, ee);
1721 return(NULL);
1722 }
1723 cuddRef(cee);
1724 Cudd_RecursiveDeref(dd, ee);
1725 minD = ddMin(dtt, dee);
1726 if (minD <= CUDD_CONST_INDEX) bound = ddMin(bound,minD-1);
1727
1728 if (minD > 0 && topf == topg) {
1729 DdNode *te = cuddBddClosestCube(dd,ft,ge,bound-1);
1730 if (te == NULL) {
1731 Cudd_RecursiveDeref(dd, ctt);
1732 Cudd_RecursiveDeref(dd, cee);
1733 return(NULL);
1734 }
1735 cuddRef(te);
1736 cte = separateCube(dd,te,&dte);
1737 if (cte == NULL) {
1738 Cudd_RecursiveDeref(dd, ctt);
1739 Cudd_RecursiveDeref(dd, cee);
1740 Cudd_RecursiveDeref(dd, te);
1741 return(NULL);
1742 }
1743 cuddRef(cte);
1744 Cudd_RecursiveDeref(dd, te);
1745 dte += 1.0;
1746 minD = ddMin(minD, dte);
1747 } else {
1748 cte = azero;
1749 cuddRef(cte);
1750 dte = CUDD_CONST_INDEX + 1.0;
1751 }
1752 if (minD <= CUDD_CONST_INDEX) bound = ddMin(bound,minD-1);
1753
1754 if (minD > 0 && topf == topg) {
1755 DdNode *et = cuddBddClosestCube(dd,fe,gt,bound-1);
1756 if (et == NULL) {
1757 Cudd_RecursiveDeref(dd, ctt);
1758 Cudd_RecursiveDeref(dd, cee);
1759 Cudd_RecursiveDeref(dd, cte);
1760 return(NULL);
1761 }
1762 cuddRef(et);
1763 cet = separateCube(dd,et,&det);
1764 if (cet == NULL) {
1765 Cudd_RecursiveDeref(dd, ctt);
1766 Cudd_RecursiveDeref(dd, cee);
1767 Cudd_RecursiveDeref(dd, cte);
1768 Cudd_RecursiveDeref(dd, et);
1769 return(NULL);
1770 }
1771 cuddRef(cet);
1772 Cudd_RecursiveDeref(dd, et);
1773 det += 1.0;
1774 minD = ddMin(minD, det);
1775 } else {
1776 cet = azero;
1777 cuddRef(cet);
1778 det = CUDD_CONST_INDEX + 1.0;
1779 }
1780
1781 if (minD == dtt) {
1782 if (dtt == dee && ctt == cee) {
1783 res = createResult(dd,CUDD_CONST_INDEX,1,ctt,dtt);
1784 } else {
1785 res = createResult(dd,index,1,ctt,dtt);
1786 }
1787 } else if (minD == dee) {
1788 res = createResult(dd,index,0,cee,dee);
1789 } else if (minD == dte) {
1790 #ifdef DD_DEBUG
1791 assert(topf == topg);
1792 #endif
1793 res = createResult(dd,index,1,cte,dte);
1794 } else {
1795 #ifdef DD_DEBUG
1796 assert(topf == topg);
1797 #endif
1798 res = createResult(dd,index,0,cet,det);
1799 }
1800 if (res == NULL) {
1801 Cudd_RecursiveDeref(dd, ctt);
1802 Cudd_RecursiveDeref(dd, cee);
1803 Cudd_RecursiveDeref(dd, cte);
1804 Cudd_RecursiveDeref(dd, cet);
1805 return(NULL);
1806 }
1807 cuddRef(res);
1808 Cudd_RecursiveDeref(dd, ctt);
1809 Cudd_RecursiveDeref(dd, cee);
1810 Cudd_RecursiveDeref(dd, cte);
1811 Cudd_RecursiveDeref(dd, cet);
1812
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);
1817
1818 cuddDeref(res);
1819 return(res);
1820
1821 } /* end of cuddBddClosestCube */
1822
1823
1824 /*---------------------------------------------------------------------------*/
1825 /* Definition of static functions */
1826 /*---------------------------------------------------------------------------*/
1827
1828
1829 /**Function********************************************************************
1830
1831 Synopsis [Performs the recursive step of Cudd_MinHammingDist.]
1832
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
1836 minterm. Then:
1837 <xmp>
1838 H(f) = min(H(f0)+h0,H(f1)+h1)
1839 </xmp>
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
1844 recursion.
1845 Returns the minimum distance unless it exceeds the upper bound or
1846 computation fails.]
1847
1848 SideEffects [None]
1849
1850 SeeAlso [Cudd_MinHammingDist]
1851
1852 ******************************************************************************/
1853 static int
cuddMinHammingDistRecur(DdNode * f,int * minterm,DdHashTable * table,int upperBound)1854 cuddMinHammingDistRecur(
1855 DdNode * f,
1856 int *minterm,
1857 DdHashTable * table,
1858 int upperBound)
1859 {
1860 DdNode *F, *Ft, *Fe;
1861 double h, hT, hE;
1862 DdNode *zero, *res;
1863 DdManager *dd = table->manager;
1864
1865 statLine(dd);
1866 if (upperBound == 0) return(0);
1867
1868 F = Cudd_Regular(f);
1869
1870 if (cuddIsConstant(F)) {
1871 zero = Cudd_Not(DD_ONE(dd));
1872 if (f == dd->background || f == zero) {
1873 return(upperBound);
1874 } else {
1875 return(0);
1876 }
1877 }
1878 if ((res = cuddHashTableLookup1(table,f)) != NULL) {
1879 h = cuddV(res);
1880 if (res->ref == 0) {
1881 dd->dead++;
1882 dd->constants.dead++;
1883 }
1884 return((int) h);
1885 }
1886
1887 Ft = cuddT(F); Fe = cuddE(F);
1888 if (Cudd_IsComplement(f)) {
1889 Ft = Cudd_Not(Ft); Fe = Cudd_Not(Fe);
1890 }
1891 if (minterm[F->index] == 0) {
1892 DdNode *temp = Ft;
1893 Ft = Fe; Fe = temp;
1894 }
1895
1896 hT = cuddMinHammingDistRecur(Ft,minterm,table,upperBound);
1897 if (hT == CUDD_OUT_OF_MEM) return(CUDD_OUT_OF_MEM);
1898 if (hT == 0) {
1899 hE = upperBound;
1900 } else {
1901 hE = cuddMinHammingDistRecur(Fe,minterm,table,upperBound - 1);
1902 if (hE == CUDD_OUT_OF_MEM) return(CUDD_OUT_OF_MEM);
1903 }
1904 h = ddMin(hT, hE + 1);
1905
1906 if (F->ref != 1) {
1907 ptrint fanout = (ptrint) F->ref;
1908 cuddSatDec(fanout);
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);
1913 }
1914 }
1915
1916 return((int) h);
1917
1918 } /* end of cuddMinHammingDistRecur */
1919
1920
1921 /**Function********************************************************************
1922
1923 Synopsis [Separates cube from distance.]
1924
1925 Description [Separates cube from distance. Returns the cube if
1926 successful; NULL otherwise.]
1927
1928 SideEffects [The distance is returned as a side effect.]
1929
1930 SeeAlso [cuddBddClosestCube createResult]
1931
1932 ******************************************************************************/
1933 static DdNode *
separateCube(DdManager * dd,DdNode * f,CUDD_VALUE_TYPE * distance)1934 separateCube(
1935 DdManager *dd,
1936 DdNode *f,
1937 CUDD_VALUE_TYPE *distance)
1938 {
1939 DdNode *cube, *t;
1940
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);
1945 return(f);
1946 }
1947
1948 /* Find out which branch points to the distance and replace the top
1949 ** node with one pointing to zero instead. */
1950 t = cuddT(f);
1951 if (Cudd_IsConstant(t) && cuddV(t) <= 0) {
1952 #ifdef DD_DEBUG
1953 assert(!Cudd_IsConstant(cuddE(f)) || cuddE(f) == DD_ONE(dd));
1954 #endif
1955 *distance = -cuddV(t);
1956 cube = cuddUniqueInter(dd, f->index, DD_ZERO(dd), cuddE(f));
1957 } else {
1958 #ifdef DD_DEBUG
1959 assert(!Cudd_IsConstant(t) || t == DD_ONE(dd));
1960 #endif
1961 *distance = -cuddV(cuddE(f));
1962 cube = cuddUniqueInter(dd, f->index, t, DD_ZERO(dd));
1963 }
1964
1965 return(cube);
1966
1967 } /* end of separateCube */
1968
1969
1970 /**Function********************************************************************
1971
1972 Synopsis [Builds a result for cache storage.]
1973
1974 Description [Builds a result for cache storage. Returns a pointer
1975 to the resulting ADD if successful; NULL otherwise.]
1976
1977 SideEffects [None]
1978
1979 SeeAlso [cuddBddClosestCube separateCube]
1980
1981 ******************************************************************************/
1982 static DdNode *
createResult(DdManager * dd,unsigned int index,unsigned int phase,DdNode * cube,CUDD_VALUE_TYPE distance)1983 createResult(
1984 DdManager *dd,
1985 unsigned int index,
1986 unsigned int phase,
1987 DdNode *cube,
1988 CUDD_VALUE_TYPE distance)
1989 {
1990 DdNode *res, *constant;
1991
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);
1996
1997 constant = cuddUniqueConst(dd,-distance);
1998 if (constant == NULL) return(NULL);
1999 cuddRef(constant);
2000
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));
2005 } else {
2006 res = cuddUniqueInter(dd,cube->index,cuddT(cube),constant);
2007 }
2008 } else {
2009 /* Add a new top node. */
2010 #ifdef DD_DEBUG
2011 assert(cuddI(dd,index) < cuddI(dd,cube->index));
2012 #endif
2013 if (phase) {
2014 res = cuddUniqueInter(dd,index,cube,constant);
2015 } else {
2016 res = cuddUniqueInter(dd,index,constant,cube);
2017 }
2018 }
2019 if (res == NULL) {
2020 Cudd_RecursiveDeref(dd, constant);
2021 return(NULL);
2022 }
2023 cuddDeref(constant); /* safe because constant is part of res */
2024
2025 return(res);
2026
2027 } /* end of createResult */
2028