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_CProjection() |
---|
18 | <li> Cudd_addHamming() |
---|
19 | <li> Cudd_MinHammingDist() |
---|
20 | <li> Cudd_bddClosestCube() |
---|
21 | </ul> |
---|
22 | Internal procedures included in this module: |
---|
23 | <ul> |
---|
24 | <li> cuddCProjectionRecur() |
---|
25 | <li> cuddBddClosestCube() |
---|
26 | </ul> |
---|
27 | Static procedures included in this module: |
---|
28 | <ul> |
---|
29 | <li> cuddMinHammingDistRecur() |
---|
30 | <li> separateCube() |
---|
31 | <li> createResult() |
---|
32 | </ul> |
---|
33 | ] |
---|
34 | |
---|
35 | SeeAlso [] |
---|
36 | |
---|
37 | Author [Fabio Somenzi] |
---|
38 | |
---|
39 | Copyright [Copyright (c) 1995-2004, Regents of the University of Colorado |
---|
40 | |
---|
41 | All rights reserved. |
---|
42 | |
---|
43 | Redistribution and use in source and binary forms, with or without |
---|
44 | modification, are permitted provided that the following conditions |
---|
45 | are met: |
---|
46 | |
---|
47 | Redistributions of source code must retain the above copyright |
---|
48 | notice, this list of conditions and the following disclaimer. |
---|
49 | |
---|
50 | Redistributions in binary form must reproduce the above copyright |
---|
51 | notice, this list of conditions and the following disclaimer in the |
---|
52 | documentation and/or other materials provided with the distribution. |
---|
53 | |
---|
54 | Neither the name of the University of Colorado nor the names of its |
---|
55 | contributors may be used to endorse or promote products derived from |
---|
56 | this software without specific prior written permission. |
---|
57 | |
---|
58 | THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS |
---|
59 | "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT |
---|
60 | LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS |
---|
61 | FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE |
---|
62 | COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, |
---|
63 | INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, |
---|
64 | BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; |
---|
65 | LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER |
---|
66 | CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT |
---|
67 | LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN |
---|
68 | ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE |
---|
69 | POSSIBILITY OF SUCH DAMAGE.] |
---|
70 | |
---|
71 | ******************************************************************************/ |
---|
72 | |
---|
73 | #include "util.h" |
---|
74 | #include "cuddInt.h" |
---|
75 | |
---|
76 | |
---|
77 | /*---------------------------------------------------------------------------*/ |
---|
78 | /* Constant declarations */ |
---|
79 | /*---------------------------------------------------------------------------*/ |
---|
80 | |
---|
81 | #define DD_DEBUG 1 |
---|
82 | |
---|
83 | /*---------------------------------------------------------------------------*/ |
---|
84 | /* Stucture declarations */ |
---|
85 | /*---------------------------------------------------------------------------*/ |
---|
86 | |
---|
87 | |
---|
88 | /*---------------------------------------------------------------------------*/ |
---|
89 | /* Type declarations */ |
---|
90 | /*---------------------------------------------------------------------------*/ |
---|
91 | |
---|
92 | |
---|
93 | /*---------------------------------------------------------------------------*/ |
---|
94 | /* Variable declarations */ |
---|
95 | /*---------------------------------------------------------------------------*/ |
---|
96 | |
---|
97 | #ifndef lint |
---|
98 | static char rcsid[] DD_UNUSED = "$Id: cuddPriority.c,v 1.26 2004/08/13 18:04:50 fabio Exp $"; |
---|
99 | #endif |
---|
100 | |
---|
101 | /*---------------------------------------------------------------------------*/ |
---|
102 | /* Macro declarations */ |
---|
103 | /*---------------------------------------------------------------------------*/ |
---|
104 | |
---|
105 | |
---|
106 | /**AutomaticStart*************************************************************/ |
---|
107 | |
---|
108 | /*---------------------------------------------------------------------------*/ |
---|
109 | /* Static function prototypes */ |
---|
110 | /*---------------------------------------------------------------------------*/ |
---|
111 | static int cuddMinHammingDistRecur (DdNode * f, int *minterm, DdHashTable * table, int upperBound); |
---|
112 | static DdNode * separateCube (DdManager *dd, DdNode *f, CUDD_VALUE_TYPE *distance); |
---|
113 | static DdNode * createResult (DdManager *dd, unsigned int index, unsigned int phase, DdNode *cube, CUDD_VALUE_TYPE distance); |
---|
114 | |
---|
115 | /**AutomaticEnd***************************************************************/ |
---|
116 | |
---|
117 | |
---|
118 | /*---------------------------------------------------------------------------*/ |
---|
119 | /* Definition of exported functions */ |
---|
120 | /*---------------------------------------------------------------------------*/ |
---|
121 | |
---|
122 | |
---|
123 | /**Function******************************************************************** |
---|
124 | |
---|
125 | Synopsis [Selects pairs from R using a priority function.] |
---|
126 | |
---|
127 | Description [Selects pairs from a relation R(x,y) (given as a BDD) |
---|
128 | in such a way that a given x appears in one pair only. Uses a |
---|
129 | priority function to determine which y should be paired to a given x. |
---|
130 | Cudd_PrioritySelect returns a pointer to |
---|
131 | the selected function if successful; NULL otherwise. |
---|
132 | Three of the arguments--x, y, and z--are vectors of BDD variables. |
---|
133 | The first two are the variables on which R depends. The third vectore |
---|
134 | is a vector of auxiliary variables, used during the computation. This |
---|
135 | vector is optional. If a NULL value is passed instead, |
---|
136 | Cudd_PrioritySelect will create the working variables on the fly. |
---|
137 | The sizes of x and y (and z if it is not NULL) should equal n. |
---|
138 | The priority function Pi can be passed as a BDD, or can be built by |
---|
139 | Cudd_PrioritySelect. If NULL is passed instead of a DdNode *, |
---|
140 | parameter Pifunc is used by Cudd_PrioritySelect to build a BDD for the |
---|
141 | priority function. (Pifunc is a pointer to a C function.) If Pi is not |
---|
142 | NULL, then Pifunc is ignored. Pifunc should have the same interface as |
---|
143 | the standard priority functions (e.g., Cudd_Dxygtdxz). |
---|
144 | Cudd_PrioritySelect and Cudd_CProjection can sometimes be used |
---|
145 | interchangeably. Specifically, calling Cudd_PrioritySelect with |
---|
146 | Cudd_Xgty as Pifunc produces the same result as calling |
---|
147 | Cudd_CProjection with the all-zero minterm as reference minterm. |
---|
148 | However, depending on the application, one or the other may be |
---|
149 | preferable: |
---|
150 | <ul> |
---|
151 | <li> When extracting representatives from an equivalence relation, |
---|
152 | Cudd_CProjection has the advantage of nor requiring the auxiliary |
---|
153 | variables. |
---|
154 | <li> When computing matchings in general bipartite graphs, |
---|
155 | Cudd_PrioritySelect normally obtains better results because it can use |
---|
156 | more powerful matching schemes (e.g., Cudd_Dxygtdxz). |
---|
157 | </ul> |
---|
158 | ] |
---|
159 | |
---|
160 | SideEffects [If called with z == NULL, will create new variables in |
---|
161 | the manager.] |
---|
162 | |
---|
163 | SeeAlso [Cudd_Dxygtdxz Cudd_Dxygtdyz Cudd_Xgty |
---|
164 | Cudd_bddAdjPermuteX Cudd_CProjection] |
---|
165 | |
---|
166 | ******************************************************************************/ |
---|
167 | DdNode * |
---|
168 | Cudd_PrioritySelect( |
---|
169 | DdManager * dd /* manager */, |
---|
170 | DdNode * R /* BDD of the relation */, |
---|
171 | DdNode ** x /* array of x variables */, |
---|
172 | DdNode ** y /* array of y variables */, |
---|
173 | DdNode ** z /* array of z variables (optional: may be NULL) */, |
---|
174 | DdNode * Pi /* BDD of the priority function (optional: may be NULL) */, |
---|
175 | int n /* size of x, y, and z */, |
---|
176 | DD_PRFP Pifunc /* function used to build Pi if it is NULL */) |
---|
177 | { |
---|
178 | DdNode *res = NULL; |
---|
179 | DdNode *zcube = NULL; |
---|
180 | DdNode *Rxz, *Q; |
---|
181 | int createdZ = 0; |
---|
182 | int createdPi = 0; |
---|
183 | int i; |
---|
184 | |
---|
185 | /* Create z variables if needed. */ |
---|
186 | if (z == NULL) { |
---|
187 | if (Pi != NULL) return(NULL); |
---|
188 | z = ALLOC(DdNode *,n); |
---|
189 | if (z == NULL) { |
---|
190 | dd->errorCode = CUDD_MEMORY_OUT; |
---|
191 | return(NULL); |
---|
192 | } |
---|
193 | createdZ = 1; |
---|
194 | for (i = 0; i < n; i++) { |
---|
195 | if (dd->size >= (int) CUDD_MAXINDEX - 1) goto endgame; |
---|
196 | z[i] = cuddUniqueInter(dd,dd->size,dd->one,Cudd_Not(dd->one)); |
---|
197 | if (z[i] == NULL) goto endgame; |
---|
198 | } |
---|
199 | } |
---|
200 | |
---|
201 | /* Create priority function BDD if needed. */ |
---|
202 | if (Pi == NULL) { |
---|
203 | Pi = Pifunc(dd,n,x,y,z); |
---|
204 | if (Pi == NULL) goto endgame; |
---|
205 | createdPi = 1; |
---|
206 | cuddRef(Pi); |
---|
207 | } |
---|
208 | |
---|
209 | /* Initialize abstraction cube. */ |
---|
210 | zcube = DD_ONE(dd); |
---|
211 | cuddRef(zcube); |
---|
212 | for (i = n - 1; i >= 0; i--) { |
---|
213 | DdNode *tmpp; |
---|
214 | tmpp = Cudd_bddAnd(dd,z[i],zcube); |
---|
215 | if (tmpp == NULL) goto endgame; |
---|
216 | cuddRef(tmpp); |
---|
217 | Cudd_RecursiveDeref(dd,zcube); |
---|
218 | zcube = tmpp; |
---|
219 | } |
---|
220 | |
---|
221 | /* Compute subset of (x,y) pairs. */ |
---|
222 | Rxz = Cudd_bddSwapVariables(dd,R,y,z,n); |
---|
223 | if (Rxz == NULL) goto endgame; |
---|
224 | cuddRef(Rxz); |
---|
225 | Q = Cudd_bddAndAbstract(dd,Rxz,Pi,zcube); |
---|
226 | if (Q == NULL) { |
---|
227 | Cudd_RecursiveDeref(dd,Rxz); |
---|
228 | goto endgame; |
---|
229 | } |
---|
230 | cuddRef(Q); |
---|
231 | Cudd_RecursiveDeref(dd,Rxz); |
---|
232 | res = Cudd_bddAnd(dd,R,Cudd_Not(Q)); |
---|
233 | if (res == NULL) { |
---|
234 | Cudd_RecursiveDeref(dd,Q); |
---|
235 | goto endgame; |
---|
236 | } |
---|
237 | cuddRef(res); |
---|
238 | Cudd_RecursiveDeref(dd,Q); |
---|
239 | |
---|
240 | endgame: |
---|
241 | if (zcube != NULL) Cudd_RecursiveDeref(dd,zcube); |
---|
242 | if (createdZ) { |
---|
243 | FREE(z); |
---|
244 | } |
---|
245 | if (createdPi) { |
---|
246 | Cudd_RecursiveDeref(dd,Pi); |
---|
247 | } |
---|
248 | if (res != NULL) cuddDeref(res); |
---|
249 | return(res); |
---|
250 | |
---|
251 | } /* Cudd_PrioritySelect */ |
---|
252 | |
---|
253 | |
---|
254 | /**Function******************************************************************** |
---|
255 | |
---|
256 | Synopsis [Generates a BDD for the function x > y.] |
---|
257 | |
---|
258 | Description [This function generates a BDD for the function x > y. |
---|
259 | Both x and y are N-bit numbers, x\[0\] x\[1\] ... x\[N-1\] and |
---|
260 | y\[0\] y\[1\] ... y\[N-1\], with 0 the most significant bit. |
---|
261 | The BDD is built bottom-up. |
---|
262 | It has 3*N-1 internal nodes, if the variables are ordered as follows: |
---|
263 | x\[0\] y\[0\] x\[1\] y\[1\] ... x\[N-1\] y\[N-1\]. |
---|
264 | Argument z is not used by Cudd_Xgty: it is included to make it |
---|
265 | call-compatible to Cudd_Dxygtdxz and Cudd_Dxygtdyz.] |
---|
266 | |
---|
267 | SideEffects [None] |
---|
268 | |
---|
269 | SeeAlso [Cudd_PrioritySelect Cudd_Dxygtdxz Cudd_Dxygtdyz] |
---|
270 | |
---|
271 | ******************************************************************************/ |
---|
272 | DdNode * |
---|
273 | Cudd_Xgty( |
---|
274 | DdManager * dd /* DD manager */, |
---|
275 | int N /* number of x and y variables */, |
---|
276 | DdNode ** z /* array of z variables: unused */, |
---|
277 | DdNode ** x /* array of x variables */, |
---|
278 | DdNode ** y /* array of y variables */) |
---|
279 | { |
---|
280 | DdNode *u, *v, *w; |
---|
281 | int i; |
---|
282 | |
---|
283 | /* Build bottom part of BDD outside loop. */ |
---|
284 | u = Cudd_bddAnd(dd, x[N-1], Cudd_Not(y[N-1])); |
---|
285 | if (u == NULL) return(NULL); |
---|
286 | cuddRef(u); |
---|
287 | |
---|
288 | /* Loop to build the rest of the BDD. */ |
---|
289 | for (i = N-2; i >= 0; i--) { |
---|
290 | v = Cudd_bddAnd(dd, y[i], Cudd_Not(u)); |
---|
291 | if (v == NULL) { |
---|
292 | Cudd_RecursiveDeref(dd, u); |
---|
293 | return(NULL); |
---|
294 | } |
---|
295 | cuddRef(v); |
---|
296 | w = Cudd_bddAnd(dd, Cudd_Not(y[i]), u); |
---|
297 | if (w == NULL) { |
---|
298 | Cudd_RecursiveDeref(dd, u); |
---|
299 | Cudd_RecursiveDeref(dd, v); |
---|
300 | return(NULL); |
---|
301 | } |
---|
302 | cuddRef(w); |
---|
303 | Cudd_RecursiveDeref(dd, u); |
---|
304 | u = Cudd_bddIte(dd, x[i], Cudd_Not(v), w); |
---|
305 | if (u == NULL) { |
---|
306 | Cudd_RecursiveDeref(dd, v); |
---|
307 | Cudd_RecursiveDeref(dd, w); |
---|
308 | return(NULL); |
---|
309 | } |
---|
310 | cuddRef(u); |
---|
311 | Cudd_RecursiveDeref(dd, v); |
---|
312 | Cudd_RecursiveDeref(dd, w); |
---|
313 | |
---|
314 | } |
---|
315 | cuddDeref(u); |
---|
316 | return(u); |
---|
317 | |
---|
318 | } /* end of Cudd_Xgty */ |
---|
319 | |
---|
320 | |
---|
321 | /**Function******************************************************************** |
---|
322 | |
---|
323 | Synopsis [Generates a BDD for the function x==y.] |
---|
324 | |
---|
325 | Description [This function generates a BDD for the function x==y. |
---|
326 | Both x and y are N-bit numbers, x\[0\] x\[1\] ... x\[N-1\] and |
---|
327 | y\[0\] y\[1\] ... y\[N-1\], with 0 the most significant bit. |
---|
328 | The BDD is built bottom-up. |
---|
329 | It has 3*N-1 internal nodes, if the variables are ordered as follows: |
---|
330 | x\[0\] y\[0\] x\[1\] y\[1\] ... x\[N-1\] y\[N-1\]. ] |
---|
331 | |
---|
332 | SideEffects [None] |
---|
333 | |
---|
334 | SeeAlso [Cudd_addXeqy] |
---|
335 | |
---|
336 | ******************************************************************************/ |
---|
337 | DdNode * |
---|
338 | Cudd_Xeqy( |
---|
339 | DdManager * dd /* DD manager */, |
---|
340 | int N /* number of x and y variables */, |
---|
341 | DdNode ** x /* array of x variables */, |
---|
342 | DdNode ** y /* array of y variables */) |
---|
343 | { |
---|
344 | DdNode *u, *v, *w; |
---|
345 | int i; |
---|
346 | |
---|
347 | /* Build bottom part of BDD outside loop. */ |
---|
348 | u = Cudd_bddIte(dd, x[N-1], y[N-1], Cudd_Not(y[N-1])); |
---|
349 | if (u == NULL) return(NULL); |
---|
350 | cuddRef(u); |
---|
351 | |
---|
352 | /* Loop to build the rest of the BDD. */ |
---|
353 | for (i = N-2; i >= 0; i--) { |
---|
354 | v = Cudd_bddAnd(dd, y[i], u); |
---|
355 | if (v == NULL) { |
---|
356 | Cudd_RecursiveDeref(dd, u); |
---|
357 | return(NULL); |
---|
358 | } |
---|
359 | cuddRef(v); |
---|
360 | w = Cudd_bddAnd(dd, Cudd_Not(y[i]), u); |
---|
361 | if (w == NULL) { |
---|
362 | Cudd_RecursiveDeref(dd, u); |
---|
363 | Cudd_RecursiveDeref(dd, v); |
---|
364 | return(NULL); |
---|
365 | } |
---|
366 | cuddRef(w); |
---|
367 | Cudd_RecursiveDeref(dd, u); |
---|
368 | u = Cudd_bddIte(dd, x[i], v, w); |
---|
369 | if (u == NULL) { |
---|
370 | Cudd_RecursiveDeref(dd, v); |
---|
371 | Cudd_RecursiveDeref(dd, w); |
---|
372 | return(NULL); |
---|
373 | } |
---|
374 | cuddRef(u); |
---|
375 | Cudd_RecursiveDeref(dd, v); |
---|
376 | Cudd_RecursiveDeref(dd, w); |
---|
377 | } |
---|
378 | cuddDeref(u); |
---|
379 | return(u); |
---|
380 | |
---|
381 | } /* end of Cudd_Xeqy */ |
---|
382 | |
---|
383 | |
---|
384 | /**Function******************************************************************** |
---|
385 | |
---|
386 | Synopsis [Generates an ADD for the function x==y.] |
---|
387 | |
---|
388 | Description [This function generates an ADD for the function x==y. |
---|
389 | Both x and y are N-bit numbers, x\[0\] x\[1\] ... x\[N-1\] and |
---|
390 | y\[0\] y\[1\] ... y\[N-1\], with 0 the most significant bit. |
---|
391 | The ADD is built bottom-up. |
---|
392 | It has 3*N-1 internal nodes, if the variables are ordered as follows: |
---|
393 | x\[0\] y\[0\] x\[1\] y\[1\] ... x\[N-1\] y\[N-1\]. ] |
---|
394 | |
---|
395 | SideEffects [None] |
---|
396 | |
---|
397 | SeeAlso [Cudd_Xeqy] |
---|
398 | |
---|
399 | ******************************************************************************/ |
---|
400 | DdNode * |
---|
401 | Cudd_addXeqy( |
---|
402 | DdManager * dd /* DD manager */, |
---|
403 | int N /* number of x and y variables */, |
---|
404 | DdNode ** x /* array of x variables */, |
---|
405 | DdNode ** y /* array of y variables */) |
---|
406 | { |
---|
407 | DdNode *one, *zero; |
---|
408 | DdNode *u, *v, *w; |
---|
409 | int i; |
---|
410 | |
---|
411 | one = DD_ONE(dd); |
---|
412 | zero = DD_ZERO(dd); |
---|
413 | |
---|
414 | /* Build bottom part of ADD outside loop. */ |
---|
415 | v = Cudd_addIte(dd, y[N-1], one, zero); |
---|
416 | if (v == NULL) return(NULL); |
---|
417 | cuddRef(v); |
---|
418 | w = Cudd_addIte(dd, y[N-1], zero, one); |
---|
419 | if (w == NULL) { |
---|
420 | Cudd_RecursiveDeref(dd, v); |
---|
421 | return(NULL); |
---|
422 | } |
---|
423 | cuddRef(w); |
---|
424 | u = Cudd_addIte(dd, x[N-1], v, w); |
---|
425 | if (w == NULL) { |
---|
426 | Cudd_RecursiveDeref(dd, v); |
---|
427 | Cudd_RecursiveDeref(dd, w); |
---|
428 | return(NULL); |
---|
429 | } |
---|
430 | cuddRef(u); |
---|
431 | Cudd_RecursiveDeref(dd, v); |
---|
432 | Cudd_RecursiveDeref(dd, w); |
---|
433 | |
---|
434 | /* Loop to build the rest of the ADD. */ |
---|
435 | for (i = N-2; i >= 0; i--) { |
---|
436 | v = Cudd_addIte(dd, y[i], u, zero); |
---|
437 | if (v == NULL) { |
---|
438 | Cudd_RecursiveDeref(dd, u); |
---|
439 | return(NULL); |
---|
440 | } |
---|
441 | cuddRef(v); |
---|
442 | w = Cudd_addIte(dd, y[i], zero, u); |
---|
443 | if (w == NULL) { |
---|
444 | Cudd_RecursiveDeref(dd, u); |
---|
445 | Cudd_RecursiveDeref(dd, v); |
---|
446 | return(NULL); |
---|
447 | } |
---|
448 | cuddRef(w); |
---|
449 | Cudd_RecursiveDeref(dd, u); |
---|
450 | u = Cudd_addIte(dd, x[i], v, w); |
---|
451 | if (w == NULL) { |
---|
452 | Cudd_RecursiveDeref(dd, v); |
---|
453 | Cudd_RecursiveDeref(dd, w); |
---|
454 | return(NULL); |
---|
455 | } |
---|
456 | cuddRef(u); |
---|
457 | Cudd_RecursiveDeref(dd, v); |
---|
458 | Cudd_RecursiveDeref(dd, w); |
---|
459 | } |
---|
460 | cuddDeref(u); |
---|
461 | return(u); |
---|
462 | |
---|
463 | } /* end of Cudd_addXeqy */ |
---|
464 | |
---|
465 | |
---|
466 | /**Function******************************************************************** |
---|
467 | |
---|
468 | Synopsis [Generates a BDD for the function d(x,y) > d(x,z).] |
---|
469 | |
---|
470 | Description [This function generates a BDD for the function d(x,y) |
---|
471 | > d(x,z); |
---|
472 | x, y, and z are N-bit numbers, x\[0\] x\[1\] ... x\[N-1\], |
---|
473 | y\[0\] y\[1\] ... y\[N-1\], and z\[0\] z\[1\] ... z\[N-1\], |
---|
474 | with 0 the most significant bit. |
---|
475 | The distance d(x,y) is defined as: |
---|
476 | \sum_{i=0}^{N-1}(|x_i - y_i| \cdot 2^{N-i-1}). |
---|
477 | The BDD is built bottom-up. |
---|
478 | It has 7*N-3 internal nodes, if the variables are ordered as follows: |
---|
479 | x\[0\] y\[0\] z\[0\] x\[1\] y\[1\] z\[1\] ... x\[N-1\] y\[N-1\] z\[N-1\]. ] |
---|
480 | |
---|
481 | SideEffects [None] |
---|
482 | |
---|
483 | SeeAlso [Cudd_PrioritySelect Cudd_Dxygtdyz Cudd_Xgty Cudd_bddAdjPermuteX] |
---|
484 | |
---|
485 | ******************************************************************************/ |
---|
486 | DdNode * |
---|
487 | Cudd_Dxygtdxz( |
---|
488 | DdManager * dd /* DD manager */, |
---|
489 | int N /* number of x, y, and z variables */, |
---|
490 | DdNode ** x /* array of x variables */, |
---|
491 | DdNode ** y /* array of y variables */, |
---|
492 | DdNode ** z /* array of z variables */) |
---|
493 | { |
---|
494 | DdNode *one, *zero; |
---|
495 | DdNode *z1, *z2, *z3, *z4, *y1_, *y2, *x1; |
---|
496 | int i; |
---|
497 | |
---|
498 | one = DD_ONE(dd); |
---|
499 | zero = Cudd_Not(one); |
---|
500 | |
---|
501 | /* Build bottom part of BDD outside loop. */ |
---|
502 | y1_ = Cudd_bddIte(dd, y[N-1], one, Cudd_Not(z[N-1])); |
---|
503 | if (y1_ == NULL) return(NULL); |
---|
504 | cuddRef(y1_); |
---|
505 | y2 = Cudd_bddIte(dd, y[N-1], z[N-1], one); |
---|
506 | if (y2 == NULL) { |
---|
507 | Cudd_RecursiveDeref(dd, y1_); |
---|
508 | return(NULL); |
---|
509 | } |
---|
510 | cuddRef(y2); |
---|
511 | x1 = Cudd_bddIte(dd, x[N-1], y1_, y2); |
---|
512 | if (x1 == NULL) { |
---|
513 | Cudd_RecursiveDeref(dd, y1_); |
---|
514 | Cudd_RecursiveDeref(dd, y2); |
---|
515 | return(NULL); |
---|
516 | } |
---|
517 | cuddRef(x1); |
---|
518 | Cudd_RecursiveDeref(dd, y1_); |
---|
519 | Cudd_RecursiveDeref(dd, y2); |
---|
520 | |
---|
521 | /* Loop to build the rest of the BDD. */ |
---|
522 | for (i = N-2; i >= 0; i--) { |
---|
523 | z1 = Cudd_bddIte(dd, z[i], one, Cudd_Not(x1)); |
---|
524 | if (z1 == NULL) { |
---|
525 | Cudd_RecursiveDeref(dd, x1); |
---|
526 | return(NULL); |
---|
527 | } |
---|
528 | cuddRef(z1); |
---|
529 | z2 = Cudd_bddIte(dd, z[i], x1, one); |
---|
530 | if (z2 == NULL) { |
---|
531 | Cudd_RecursiveDeref(dd, x1); |
---|
532 | Cudd_RecursiveDeref(dd, z1); |
---|
533 | return(NULL); |
---|
534 | } |
---|
535 | cuddRef(z2); |
---|
536 | z3 = Cudd_bddIte(dd, z[i], one, x1); |
---|
537 | if (z3 == NULL) { |
---|
538 | Cudd_RecursiveDeref(dd, x1); |
---|
539 | Cudd_RecursiveDeref(dd, z1); |
---|
540 | Cudd_RecursiveDeref(dd, z2); |
---|
541 | return(NULL); |
---|
542 | } |
---|
543 | cuddRef(z3); |
---|
544 | z4 = Cudd_bddIte(dd, z[i], x1, zero); |
---|
545 | if (z4 == NULL) { |
---|
546 | Cudd_RecursiveDeref(dd, x1); |
---|
547 | Cudd_RecursiveDeref(dd, z1); |
---|
548 | Cudd_RecursiveDeref(dd, z2); |
---|
549 | Cudd_RecursiveDeref(dd, z3); |
---|
550 | return(NULL); |
---|
551 | } |
---|
552 | cuddRef(z4); |
---|
553 | Cudd_RecursiveDeref(dd, x1); |
---|
554 | y1_ = Cudd_bddIte(dd, y[i], z2, Cudd_Not(z1)); |
---|
555 | if (y1_ == NULL) { |
---|
556 | Cudd_RecursiveDeref(dd, z1); |
---|
557 | Cudd_RecursiveDeref(dd, z2); |
---|
558 | Cudd_RecursiveDeref(dd, z3); |
---|
559 | Cudd_RecursiveDeref(dd, z4); |
---|
560 | return(NULL); |
---|
561 | } |
---|
562 | cuddRef(y1_); |
---|
563 | y2 = Cudd_bddIte(dd, y[i], z4, z3); |
---|
564 | if (y2 == NULL) { |
---|
565 | Cudd_RecursiveDeref(dd, z1); |
---|
566 | Cudd_RecursiveDeref(dd, z2); |
---|
567 | Cudd_RecursiveDeref(dd, z3); |
---|
568 | Cudd_RecursiveDeref(dd, z4); |
---|
569 | Cudd_RecursiveDeref(dd, y1_); |
---|
570 | return(NULL); |
---|
571 | } |
---|
572 | cuddRef(y2); |
---|
573 | Cudd_RecursiveDeref(dd, z1); |
---|
574 | Cudd_RecursiveDeref(dd, z2); |
---|
575 | Cudd_RecursiveDeref(dd, z3); |
---|
576 | Cudd_RecursiveDeref(dd, z4); |
---|
577 | x1 = Cudd_bddIte(dd, x[i], y1_, y2); |
---|
578 | if (x1 == NULL) { |
---|
579 | Cudd_RecursiveDeref(dd, y1_); |
---|
580 | Cudd_RecursiveDeref(dd, y2); |
---|
581 | return(NULL); |
---|
582 | } |
---|
583 | cuddRef(x1); |
---|
584 | Cudd_RecursiveDeref(dd, y1_); |
---|
585 | Cudd_RecursiveDeref(dd, y2); |
---|
586 | } |
---|
587 | cuddDeref(x1); |
---|
588 | return(Cudd_Not(x1)); |
---|
589 | |
---|
590 | } /* end of Cudd_Dxygtdxz */ |
---|
591 | |
---|
592 | |
---|
593 | /**Function******************************************************************** |
---|
594 | |
---|
595 | Synopsis [Generates a BDD for the function d(x,y) > d(y,z).] |
---|
596 | |
---|
597 | Description [This function generates a BDD for the function d(x,y) |
---|
598 | > d(y,z); |
---|
599 | x, y, and z are N-bit numbers, x\[0\] x\[1\] ... x\[N-1\], |
---|
600 | y\[0\] y\[1\] ... y\[N-1\], and z\[0\] z\[1\] ... z\[N-1\], |
---|
601 | with 0 the most significant bit. |
---|
602 | The distance d(x,y) is defined as: |
---|
603 | \sum_{i=0}^{N-1}(|x_i - y_i| \cdot 2^{N-i-1}). |
---|
604 | The BDD is built bottom-up. |
---|
605 | It has 7*N-3 internal nodes, if the variables are ordered as follows: |
---|
606 | x\[0\] y\[0\] z\[0\] x\[1\] y\[1\] z\[1\] ... x\[N-1\] y\[N-1\] z\[N-1\]. ] |
---|
607 | |
---|
608 | SideEffects [None] |
---|
609 | |
---|
610 | SeeAlso [Cudd_PrioritySelect Cudd_Dxygtdxz Cudd_Xgty Cudd_bddAdjPermuteX] |
---|
611 | |
---|
612 | ******************************************************************************/ |
---|
613 | DdNode * |
---|
614 | Cudd_Dxygtdyz( |
---|
615 | DdManager * dd /* DD manager */, |
---|
616 | int N /* number of x, y, and z variables */, |
---|
617 | DdNode ** x /* array of x variables */, |
---|
618 | DdNode ** y /* array of y variables */, |
---|
619 | DdNode ** z /* array of z variables */) |
---|
620 | { |
---|
621 | DdNode *one, *zero; |
---|
622 | DdNode *z1, *z2, *z3, *z4, *y1_, *y2, *x1; |
---|
623 | int i; |
---|
624 | |
---|
625 | one = DD_ONE(dd); |
---|
626 | zero = Cudd_Not(one); |
---|
627 | |
---|
628 | /* Build bottom part of BDD outside loop. */ |
---|
629 | y1_ = Cudd_bddIte(dd, y[N-1], one, z[N-1]); |
---|
630 | if (y1_ == NULL) return(NULL); |
---|
631 | cuddRef(y1_); |
---|
632 | y2 = Cudd_bddIte(dd, y[N-1], z[N-1], zero); |
---|
633 | if (y2 == NULL) { |
---|
634 | Cudd_RecursiveDeref(dd, y1_); |
---|
635 | return(NULL); |
---|
636 | } |
---|
637 | cuddRef(y2); |
---|
638 | x1 = Cudd_bddIte(dd, x[N-1], y1_, Cudd_Not(y2)); |
---|
639 | if (x1 == NULL) { |
---|
640 | Cudd_RecursiveDeref(dd, y1_); |
---|
641 | Cudd_RecursiveDeref(dd, y2); |
---|
642 | return(NULL); |
---|
643 | } |
---|
644 | cuddRef(x1); |
---|
645 | Cudd_RecursiveDeref(dd, y1_); |
---|
646 | Cudd_RecursiveDeref(dd, y2); |
---|
647 | |
---|
648 | /* Loop to build the rest of the BDD. */ |
---|
649 | for (i = N-2; i >= 0; i--) { |
---|
650 | z1 = Cudd_bddIte(dd, z[i], x1, zero); |
---|
651 | if (z1 == NULL) { |
---|
652 | Cudd_RecursiveDeref(dd, x1); |
---|
653 | return(NULL); |
---|
654 | } |
---|
655 | cuddRef(z1); |
---|
656 | z2 = Cudd_bddIte(dd, z[i], x1, one); |
---|
657 | if (z2 == NULL) { |
---|
658 | Cudd_RecursiveDeref(dd, x1); |
---|
659 | Cudd_RecursiveDeref(dd, z1); |
---|
660 | return(NULL); |
---|
661 | } |
---|
662 | cuddRef(z2); |
---|
663 | z3 = Cudd_bddIte(dd, z[i], one, x1); |
---|
664 | if (z3 == NULL) { |
---|
665 | Cudd_RecursiveDeref(dd, x1); |
---|
666 | Cudd_RecursiveDeref(dd, z1); |
---|
667 | Cudd_RecursiveDeref(dd, z2); |
---|
668 | return(NULL); |
---|
669 | } |
---|
670 | cuddRef(z3); |
---|
671 | z4 = Cudd_bddIte(dd, z[i], one, Cudd_Not(x1)); |
---|
672 | if (z4 == NULL) { |
---|
673 | Cudd_RecursiveDeref(dd, x1); |
---|
674 | Cudd_RecursiveDeref(dd, z1); |
---|
675 | Cudd_RecursiveDeref(dd, z2); |
---|
676 | Cudd_RecursiveDeref(dd, z3); |
---|
677 | return(NULL); |
---|
678 | } |
---|
679 | cuddRef(z4); |
---|
680 | Cudd_RecursiveDeref(dd, x1); |
---|
681 | y1_ = Cudd_bddIte(dd, y[i], z2, z1); |
---|
682 | if (y1_ == NULL) { |
---|
683 | Cudd_RecursiveDeref(dd, z1); |
---|
684 | Cudd_RecursiveDeref(dd, z2); |
---|
685 | Cudd_RecursiveDeref(dd, z3); |
---|
686 | Cudd_RecursiveDeref(dd, z4); |
---|
687 | return(NULL); |
---|
688 | } |
---|
689 | cuddRef(y1_); |
---|
690 | y2 = Cudd_bddIte(dd, y[i], z4, Cudd_Not(z3)); |
---|
691 | if (y2 == NULL) { |
---|
692 | Cudd_RecursiveDeref(dd, z1); |
---|
693 | Cudd_RecursiveDeref(dd, z2); |
---|
694 | Cudd_RecursiveDeref(dd, z3); |
---|
695 | Cudd_RecursiveDeref(dd, z4); |
---|
696 | Cudd_RecursiveDeref(dd, y1_); |
---|
697 | return(NULL); |
---|
698 | } |
---|
699 | cuddRef(y2); |
---|
700 | Cudd_RecursiveDeref(dd, z1); |
---|
701 | Cudd_RecursiveDeref(dd, z2); |
---|
702 | Cudd_RecursiveDeref(dd, z3); |
---|
703 | Cudd_RecursiveDeref(dd, z4); |
---|
704 | x1 = Cudd_bddIte(dd, x[i], y1_, Cudd_Not(y2)); |
---|
705 | if (x1 == NULL) { |
---|
706 | Cudd_RecursiveDeref(dd, y1_); |
---|
707 | Cudd_RecursiveDeref(dd, y2); |
---|
708 | return(NULL); |
---|
709 | } |
---|
710 | cuddRef(x1); |
---|
711 | Cudd_RecursiveDeref(dd, y1_); |
---|
712 | Cudd_RecursiveDeref(dd, y2); |
---|
713 | } |
---|
714 | cuddDeref(x1); |
---|
715 | return(Cudd_Not(x1)); |
---|
716 | |
---|
717 | } /* end of Cudd_Dxygtdyz */ |
---|
718 | |
---|
719 | |
---|
720 | /**Function******************************************************************** |
---|
721 | |
---|
722 | Synopsis [Computes the compatible projection of R w.r.t. cube Y.] |
---|
723 | |
---|
724 | Description [Computes the compatible projection of relation R with |
---|
725 | respect to cube Y. Returns a pointer to the c-projection if |
---|
726 | successful; NULL otherwise. For a comparison between Cudd_CProjection |
---|
727 | and Cudd_PrioritySelect, see the documentation of the latter.] |
---|
728 | |
---|
729 | SideEffects [None] |
---|
730 | |
---|
731 | SeeAlso [Cudd_PrioritySelect] |
---|
732 | |
---|
733 | ******************************************************************************/ |
---|
734 | DdNode * |
---|
735 | Cudd_CProjection( |
---|
736 | DdManager * dd, |
---|
737 | DdNode * R, |
---|
738 | DdNode * Y) |
---|
739 | { |
---|
740 | DdNode *res; |
---|
741 | DdNode *support; |
---|
742 | |
---|
743 | if (cuddCheckCube(dd,Y) == 0) { |
---|
744 | (void) fprintf(dd->err, |
---|
745 | "Error: The third argument of Cudd_CProjection should be a cube\n"); |
---|
746 | dd->errorCode = CUDD_INVALID_ARG; |
---|
747 | return(NULL); |
---|
748 | } |
---|
749 | |
---|
750 | /* Compute the support of Y, which is used by the abstraction step |
---|
751 | ** in cuddCProjectionRecur. |
---|
752 | */ |
---|
753 | support = Cudd_Support(dd,Y); |
---|
754 | if (support == NULL) return(NULL); |
---|
755 | cuddRef(support); |
---|
756 | |
---|
757 | do { |
---|
758 | dd->reordered = 0; |
---|
759 | res = cuddCProjectionRecur(dd,R,Y,support); |
---|
760 | } while (dd->reordered == 1); |
---|
761 | |
---|
762 | if (res == NULL) { |
---|
763 | Cudd_RecursiveDeref(dd,support); |
---|
764 | return(NULL); |
---|
765 | } |
---|
766 | cuddRef(res); |
---|
767 | Cudd_RecursiveDeref(dd,support); |
---|
768 | cuddDeref(res); |
---|
769 | |
---|
770 | return(res); |
---|
771 | |
---|
772 | } /* end of Cudd_CProjection */ |
---|
773 | |
---|
774 | |
---|
775 | /**Function******************************************************************** |
---|
776 | |
---|
777 | Synopsis [Computes the Hamming distance ADD.] |
---|
778 | |
---|
779 | Description [Computes the Hamming distance ADD. Returns an ADD that |
---|
780 | gives the Hamming distance between its two arguments if successful; |
---|
781 | NULL otherwise. The two vectors xVars and yVars identify the variables |
---|
782 | that form the two arguments.] |
---|
783 | |
---|
784 | SideEffects [None] |
---|
785 | |
---|
786 | SeeAlso [] |
---|
787 | |
---|
788 | ******************************************************************************/ |
---|
789 | DdNode * |
---|
790 | Cudd_addHamming( |
---|
791 | DdManager * dd, |
---|
792 | DdNode ** xVars, |
---|
793 | DdNode ** yVars, |
---|
794 | int nVars) |
---|
795 | { |
---|
796 | DdNode *result,*tempBdd; |
---|
797 | DdNode *tempAdd,*temp; |
---|
798 | int i; |
---|
799 | |
---|
800 | result = DD_ZERO(dd); |
---|
801 | cuddRef(result); |
---|
802 | |
---|
803 | for (i = 0; i < nVars; i++) { |
---|
804 | tempBdd = Cudd_bddIte(dd,xVars[i],Cudd_Not(yVars[i]),yVars[i]); |
---|
805 | if (tempBdd == NULL) { |
---|
806 | Cudd_RecursiveDeref(dd,result); |
---|
807 | return(NULL); |
---|
808 | } |
---|
809 | cuddRef(tempBdd); |
---|
810 | tempAdd = Cudd_BddToAdd(dd,tempBdd); |
---|
811 | if (tempAdd == NULL) { |
---|
812 | Cudd_RecursiveDeref(dd,tempBdd); |
---|
813 | Cudd_RecursiveDeref(dd,result); |
---|
814 | return(NULL); |
---|
815 | } |
---|
816 | cuddRef(tempAdd); |
---|
817 | Cudd_RecursiveDeref(dd,tempBdd); |
---|
818 | temp = Cudd_addApply(dd,Cudd_addPlus,tempAdd,result); |
---|
819 | if (temp == NULL) { |
---|
820 | Cudd_RecursiveDeref(dd,tempAdd); |
---|
821 | Cudd_RecursiveDeref(dd,result); |
---|
822 | return(NULL); |
---|
823 | } |
---|
824 | cuddRef(temp); |
---|
825 | Cudd_RecursiveDeref(dd,tempAdd); |
---|
826 | Cudd_RecursiveDeref(dd,result); |
---|
827 | result = temp; |
---|
828 | } |
---|
829 | |
---|
830 | cuddDeref(result); |
---|
831 | return(result); |
---|
832 | |
---|
833 | } /* end of Cudd_addHamming */ |
---|
834 | |
---|
835 | |
---|
836 | /**Function******************************************************************** |
---|
837 | |
---|
838 | Synopsis [Returns the minimum Hamming distance between f and minterm.] |
---|
839 | |
---|
840 | Description [Returns the minimum Hamming distance between the |
---|
841 | minterms of a function f and a reference minterm. The function is |
---|
842 | given as a BDD; the minterm is given as an array of integers, one |
---|
843 | for each variable in the manager. Returns the minimum distance if |
---|
844 | it is less than the upper bound; the upper bound if the minimum |
---|
845 | distance is at least as large; CUDD_OUT_OF_MEM in case of failure.] |
---|
846 | |
---|
847 | SideEffects [None] |
---|
848 | |
---|
849 | SeeAlso [Cudd_addHamming Cudd_bddClosestCube] |
---|
850 | |
---|
851 | ******************************************************************************/ |
---|
852 | int |
---|
853 | Cudd_MinHammingDist( |
---|
854 | DdManager *dd /* DD manager */, |
---|
855 | DdNode *f /* function to examine */, |
---|
856 | int *minterm /* reference minterm */, |
---|
857 | int upperBound /* distance above which an approximate answer is OK */) |
---|
858 | { |
---|
859 | DdHashTable *table; |
---|
860 | CUDD_VALUE_TYPE epsilon; |
---|
861 | int res; |
---|
862 | |
---|
863 | table = cuddHashTableInit(dd,1,2); |
---|
864 | if (table == NULL) { |
---|
865 | return(CUDD_OUT_OF_MEM); |
---|
866 | } |
---|
867 | epsilon = Cudd_ReadEpsilon(dd); |
---|
868 | Cudd_SetEpsilon(dd,(CUDD_VALUE_TYPE)0.0); |
---|
869 | res = cuddMinHammingDistRecur(f,minterm,table,upperBound); |
---|
870 | cuddHashTableQuit(table); |
---|
871 | Cudd_SetEpsilon(dd,epsilon); |
---|
872 | |
---|
873 | return(res); |
---|
874 | |
---|
875 | } /* end of Cudd_MinHammingDist */ |
---|
876 | |
---|
877 | |
---|
878 | /**Function******************************************************************** |
---|
879 | |
---|
880 | Synopsis [Finds a cube of f at minimum Hamming distance from g.] |
---|
881 | |
---|
882 | Description [Finds a cube of f at minimum Hamming distance from the |
---|
883 | minterms of g. All the minterms of the cube are at the minimum |
---|
884 | distance. If the distance is 0, the cube belongs to the |
---|
885 | intersection of f and g. Returns the cube if successful; NULL |
---|
886 | otherwise.] |
---|
887 | |
---|
888 | SideEffects [The distance is returned as a side effect.] |
---|
889 | |
---|
890 | SeeAlso [Cudd_MinHammingDist] |
---|
891 | |
---|
892 | ******************************************************************************/ |
---|
893 | DdNode * |
---|
894 | Cudd_bddClosestCube( |
---|
895 | DdManager *dd, |
---|
896 | DdNode * f, |
---|
897 | DdNode *g, |
---|
898 | int *distance) |
---|
899 | { |
---|
900 | DdNode *res, *acube; |
---|
901 | CUDD_VALUE_TYPE rdist; |
---|
902 | |
---|
903 | /* Compute the cube and distance as a single ADD. */ |
---|
904 | do { |
---|
905 | dd->reordered = 0; |
---|
906 | res = cuddBddClosestCube(dd,f,g,CUDD_CONST_INDEX + 1.0); |
---|
907 | } while (dd->reordered == 1); |
---|
908 | if (res == NULL) return(NULL); |
---|
909 | cuddRef(res); |
---|
910 | |
---|
911 | /* Unpack distance and cube. */ |
---|
912 | do { |
---|
913 | dd->reordered = 0; |
---|
914 | acube = separateCube(dd, res, &rdist); |
---|
915 | } while (dd->reordered == 1); |
---|
916 | if (acube == NULL) { |
---|
917 | Cudd_RecursiveDeref(dd, res); |
---|
918 | return(NULL); |
---|
919 | } |
---|
920 | cuddRef(acube); |
---|
921 | Cudd_RecursiveDeref(dd, res); |
---|
922 | |
---|
923 | /* Convert cube from ADD to BDD. */ |
---|
924 | do { |
---|
925 | dd->reordered = 0; |
---|
926 | res = cuddAddBddDoPattern(dd, acube); |
---|
927 | } while (dd->reordered == 1); |
---|
928 | if (res == NULL) { |
---|
929 | Cudd_RecursiveDeref(dd, acube); |
---|
930 | return(NULL); |
---|
931 | } |
---|
932 | cuddRef(res); |
---|
933 | Cudd_RecursiveDeref(dd, acube); |
---|
934 | |
---|
935 | *distance = (int) rdist; |
---|
936 | cuddDeref(res); |
---|
937 | return(res); |
---|
938 | |
---|
939 | } /* end of Cudd_bddClosestCube */ |
---|
940 | |
---|
941 | |
---|
942 | /*---------------------------------------------------------------------------*/ |
---|
943 | /* Definition of internal functions */ |
---|
944 | /*---------------------------------------------------------------------------*/ |
---|
945 | |
---|
946 | |
---|
947 | /**Function******************************************************************** |
---|
948 | |
---|
949 | Synopsis [Performs the recursive step of Cudd_CProjection.] |
---|
950 | |
---|
951 | Description [Performs the recursive step of Cudd_CProjection. Returns |
---|
952 | the projection if successful; NULL otherwise.] |
---|
953 | |
---|
954 | SideEffects [None] |
---|
955 | |
---|
956 | SeeAlso [Cudd_CProjection] |
---|
957 | |
---|
958 | ******************************************************************************/ |
---|
959 | DdNode * |
---|
960 | cuddCProjectionRecur( |
---|
961 | DdManager * dd, |
---|
962 | DdNode * R, |
---|
963 | DdNode * Y, |
---|
964 | DdNode * Ysupp) |
---|
965 | { |
---|
966 | DdNode *res, *res1, *res2, *resA; |
---|
967 | DdNode *r, *y, *RT, *RE, *YT, *YE, *Yrest, *Ra, *Ran, *Gamma, *Alpha; |
---|
968 | unsigned int topR, topY, top, index; |
---|
969 | DdNode *one = DD_ONE(dd); |
---|
970 | |
---|
971 | statLine(dd); |
---|
972 | if (Y == one) return(R); |
---|
973 | |
---|
974 | #ifdef DD_DEBUG |
---|
975 | assert(!Cudd_IsConstant(Y)); |
---|
976 | #endif |
---|
977 | |
---|
978 | if (R == Cudd_Not(one)) return(R); |
---|
979 | |
---|
980 | res = cuddCacheLookup2(dd, Cudd_CProjection, R, Y); |
---|
981 | if (res != NULL) return(res); |
---|
982 | |
---|
983 | r = Cudd_Regular(R); |
---|
984 | topR = cuddI(dd,r->index); |
---|
985 | y = Cudd_Regular(Y); |
---|
986 | topY = cuddI(dd,y->index); |
---|
987 | |
---|
988 | top = ddMin(topR, topY); |
---|
989 | |
---|
990 | /* Compute the cofactors of R */ |
---|
991 | if (topR == top) { |
---|
992 | index = r->index; |
---|
993 | RT = cuddT(r); |
---|
994 | RE = cuddE(r); |
---|
995 | if (r != R) { |
---|
996 | RT = Cudd_Not(RT); RE = Cudd_Not(RE); |
---|
997 | } |
---|
998 | } else { |
---|
999 | RT = RE = R; |
---|
1000 | } |
---|
1001 | |
---|
1002 | if (topY > top) { |
---|
1003 | /* Y does not depend on the current top variable. |
---|
1004 | ** We just need to compute the results on the two cofactors of R |
---|
1005 | ** and make them the children of a node labeled r->index. |
---|
1006 | */ |
---|
1007 | res1 = cuddCProjectionRecur(dd,RT,Y,Ysupp); |
---|
1008 | if (res1 == NULL) return(NULL); |
---|
1009 | cuddRef(res1); |
---|
1010 | res2 = cuddCProjectionRecur(dd,RE,Y,Ysupp); |
---|
1011 | if (res2 == NULL) { |
---|
1012 | Cudd_RecursiveDeref(dd,res1); |
---|
1013 | return(NULL); |
---|
1014 | } |
---|
1015 | cuddRef(res2); |
---|
1016 | res = cuddBddIteRecur(dd, dd->vars[index], res1, res2); |
---|
1017 | if (res == NULL) { |
---|
1018 | Cudd_RecursiveDeref(dd,res1); |
---|
1019 | Cudd_RecursiveDeref(dd,res2); |
---|
1020 | return(NULL); |
---|
1021 | } |
---|
1022 | /* If we have reached this point, res1 and res2 are now |
---|
1023 | ** incorporated in res. cuddDeref is therefore sufficient. |
---|
1024 | */ |
---|
1025 | cuddDeref(res1); |
---|
1026 | cuddDeref(res2); |
---|
1027 | } else { |
---|
1028 | /* Compute the cofactors of Y */ |
---|
1029 | index = y->index; |
---|
1030 | YT = cuddT(y); |
---|
1031 | YE = cuddE(y); |
---|
1032 | if (y != Y) { |
---|
1033 | YT = Cudd_Not(YT); YE = Cudd_Not(YE); |
---|
1034 | } |
---|
1035 | if (YT == Cudd_Not(one)) { |
---|
1036 | Alpha = Cudd_Not(dd->vars[index]); |
---|
1037 | Yrest = YE; |
---|
1038 | Ra = RE; |
---|
1039 | Ran = RT; |
---|
1040 | } else { |
---|
1041 | Alpha = dd->vars[index]; |
---|
1042 | Yrest = YT; |
---|
1043 | Ra = RT; |
---|
1044 | Ran = RE; |
---|
1045 | } |
---|
1046 | Gamma = cuddBddExistAbstractRecur(dd,Ra,cuddT(Ysupp)); |
---|
1047 | if (Gamma == NULL) return(NULL); |
---|
1048 | if (Gamma == one) { |
---|
1049 | res1 = cuddCProjectionRecur(dd,Ra,Yrest,cuddT(Ysupp)); |
---|
1050 | if (res1 == NULL) return(NULL); |
---|
1051 | cuddRef(res1); |
---|
1052 | res = cuddBddAndRecur(dd, Alpha, res1); |
---|
1053 | if (res == NULL) { |
---|
1054 | Cudd_RecursiveDeref(dd,res1); |
---|
1055 | return(NULL); |
---|
1056 | } |
---|
1057 | cuddDeref(res1); |
---|
1058 | } else if (Gamma == Cudd_Not(one)) { |
---|
1059 | res1 = cuddCProjectionRecur(dd,Ran,Yrest,cuddT(Ysupp)); |
---|
1060 | if (res1 == NULL) return(NULL); |
---|
1061 | cuddRef(res1); |
---|
1062 | res = cuddBddAndRecur(dd, Cudd_Not(Alpha), res1); |
---|
1063 | if (res == NULL) { |
---|
1064 | Cudd_RecursiveDeref(dd,res1); |
---|
1065 | return(NULL); |
---|
1066 | } |
---|
1067 | cuddDeref(res1); |
---|
1068 | } else { |
---|
1069 | cuddRef(Gamma); |
---|
1070 | resA = cuddCProjectionRecur(dd,Ran,Yrest,cuddT(Ysupp)); |
---|
1071 | if (resA == NULL) { |
---|
1072 | Cudd_RecursiveDeref(dd,Gamma); |
---|
1073 | return(NULL); |
---|
1074 | } |
---|
1075 | cuddRef(resA); |
---|
1076 | res2 = cuddBddAndRecur(dd, Cudd_Not(Gamma), resA); |
---|
1077 | if (res2 == NULL) { |
---|
1078 | Cudd_RecursiveDeref(dd,Gamma); |
---|
1079 | Cudd_RecursiveDeref(dd,resA); |
---|
1080 | return(NULL); |
---|
1081 | } |
---|
1082 | cuddRef(res2); |
---|
1083 | Cudd_RecursiveDeref(dd,Gamma); |
---|
1084 | Cudd_RecursiveDeref(dd,resA); |
---|
1085 | res1 = cuddCProjectionRecur(dd,Ra,Yrest,cuddT(Ysupp)); |
---|
1086 | if (res1 == NULL) { |
---|
1087 | Cudd_RecursiveDeref(dd,res2); |
---|
1088 | return(NULL); |
---|
1089 | } |
---|
1090 | cuddRef(res1); |
---|
1091 | res = cuddBddIteRecur(dd, Alpha, res1, res2); |
---|
1092 | if (res == NULL) { |
---|
1093 | Cudd_RecursiveDeref(dd,res1); |
---|
1094 | Cudd_RecursiveDeref(dd,res2); |
---|
1095 | return(NULL); |
---|
1096 | } |
---|
1097 | cuddDeref(res1); |
---|
1098 | cuddDeref(res2); |
---|
1099 | } |
---|
1100 | } |
---|
1101 | |
---|
1102 | cuddCacheInsert2(dd,Cudd_CProjection,R,Y,res); |
---|
1103 | |
---|
1104 | return(res); |
---|
1105 | |
---|
1106 | } /* end of cuddCProjectionRecur */ |
---|
1107 | |
---|
1108 | |
---|
1109 | /**Function******************************************************************** |
---|
1110 | |
---|
1111 | Synopsis [Performs the recursive step of Cudd_bddClosestCube.] |
---|
1112 | |
---|
1113 | Description [Performs the recursive step of Cudd_bddClosestCube. |
---|
1114 | Returns the cube if succesful; NULL otherwise. The procedure uses a |
---|
1115 | four-way recursion to examine all four combinations of cofactors of |
---|
1116 | <code>f</code> and <code>g</code> according to the following formula. |
---|
1117 | <pre> |
---|
1118 | H(f,g) = min(H(ft,gt), H(fe,ge), H(ft,ge)+1, H(fe,gt)+1) |
---|
1119 | </pre> |
---|
1120 | Bounding is based on the following observations. |
---|
1121 | <ul> |
---|
1122 | <li> If we already found two points at distance 0, there is no point in |
---|
1123 | continuing. Furthermore, |
---|
1124 | <li> If F == not(G) then the best we can hope for is a minimum distance |
---|
1125 | of 1. If we have already found two points at distance 1, there is |
---|
1126 | no point in continuing. (Indeed, H(F,G) == 1 in this case. We |
---|
1127 | have to continue, though, to find the cube.) |
---|
1128 | </ul> |
---|
1129 | The variable <code>bound</code> is set at the largest value of the distance |
---|
1130 | that we are still interested in. Therefore, we desist when |
---|
1131 | <pre> |
---|
1132 | (bound == -1) and (F != not(G)) or (bound == 0) and (F == not(G)). |
---|
1133 | </pre> |
---|
1134 | If we were maximally aggressive in using the bound, we would always |
---|
1135 | set the bound to the minimum distance seen thus far minus one. That |
---|
1136 | is, we would maintain the invariant |
---|
1137 | <pre> |
---|
1138 | bound < minD, |
---|
1139 | </pre> |
---|
1140 | except at the very beginning, when we have no value for |
---|
1141 | <code>minD</code>.<p> |
---|
1142 | |
---|
1143 | However, we do not use <code>bound < minD</code> when examining the |
---|
1144 | two negative cofactors, because we try to find a large cube at |
---|
1145 | minimum distance. To do so, we try to find a cube in the negative |
---|
1146 | cofactors at the same or smaller distance from the cube found in the |
---|
1147 | positive cofactors.<p> |
---|
1148 | |
---|
1149 | When we compute <code>H(ft,ge)</code> and <code>H(fe,gt)</code> we |
---|
1150 | know that we are going to add 1 to the result of the recursive call |
---|
1151 | to account for the difference in the splitting variable. Therefore, |
---|
1152 | we decrease the bound correspondingly.<p> |
---|
1153 | |
---|
1154 | Another important observation concerns the need of examining all |
---|
1155 | four pairs of cofators only when both <code>f</code> and |
---|
1156 | <code>g</code> depend on the top variable.<p> |
---|
1157 | |
---|
1158 | Suppose <code>gt == ge == g</code>. (That is, <code>g</code> does |
---|
1159 | not depend on the top variable.) Then |
---|
1160 | <pre> |
---|
1161 | H(f,g) = min(H(ft,g), H(fe,g), H(ft,g)+1, H(fe,g)+1) |
---|
1162 | = min(H(ft,g), H(fe,g)) . |
---|
1163 | </pre> |
---|
1164 | Therefore, under these circumstances, we skip the two "cross" cases.<p> |
---|
1165 | |
---|
1166 | An interesting feature of this function is the scheme used for |
---|
1167 | caching the results in the global computed table. Since we have a |
---|
1168 | cube and a distance, we combine them to form an ADD. The |
---|
1169 | combination replaces the zero child of the top node of the cube with |
---|
1170 | the negative of the distance. (The use of the negative is to avoid |
---|
1171 | ambiguity with 1.) The degenerate cases (zero and one) are treated |
---|
1172 | specially because the distance is known (0 for one, and infinity for |
---|
1173 | zero).] |
---|
1174 | |
---|
1175 | SideEffects [None] |
---|
1176 | |
---|
1177 | SeeAlso [Cudd_bddClosestCube] |
---|
1178 | |
---|
1179 | ******************************************************************************/ |
---|
1180 | DdNode * |
---|
1181 | cuddBddClosestCube( |
---|
1182 | DdManager *dd, |
---|
1183 | DdNode *f, |
---|
1184 | DdNode *g, |
---|
1185 | CUDD_VALUE_TYPE bound) |
---|
1186 | { |
---|
1187 | DdNode *res, *F, *G, *ft, *fe, *gt, *ge, *tt, *ee; |
---|
1188 | DdNode *ctt, *cee, *cte, *cet; |
---|
1189 | CUDD_VALUE_TYPE minD, dtt, dee, dte, det; |
---|
1190 | DdNode *one = DD_ONE(dd); |
---|
1191 | DdNode *lzero = Cudd_Not(one); |
---|
1192 | DdNode *azero = DD_ZERO(dd); |
---|
1193 | unsigned int topf, topg, index; |
---|
1194 | |
---|
1195 | statLine(dd); |
---|
1196 | if (bound < (f == Cudd_Not(g))) return(azero); |
---|
1197 | /* Terminal cases. */ |
---|
1198 | if (g == lzero || f == lzero) return(azero); |
---|
1199 | if (f == one && g == one) return(one); |
---|
1200 | |
---|
1201 | /* Check cache. */ |
---|
1202 | F = Cudd_Regular(f); |
---|
1203 | G = Cudd_Regular(g); |
---|
1204 | if (F->ref != 1 || G->ref != 1) { |
---|
1205 | res = cuddCacheLookup2(dd,(DD_CTFP) Cudd_bddClosestCube, f, g); |
---|
1206 | if (res != NULL) return(res); |
---|
1207 | } |
---|
1208 | |
---|
1209 | topf = cuddI(dd,F->index); |
---|
1210 | topg = cuddI(dd,G->index); |
---|
1211 | |
---|
1212 | /* Compute cofactors. */ |
---|
1213 | if (topf <= topg) { |
---|
1214 | index = F->index; |
---|
1215 | ft = cuddT(F); |
---|
1216 | fe = cuddE(F); |
---|
1217 | if (Cudd_IsComplement(f)) { |
---|
1218 | ft = Cudd_Not(ft); |
---|
1219 | fe = Cudd_Not(fe); |
---|
1220 | } |
---|
1221 | } else { |
---|
1222 | index = G->index; |
---|
1223 | ft = fe = f; |
---|
1224 | } |
---|
1225 | |
---|
1226 | if (topg <= topf) { |
---|
1227 | gt = cuddT(G); |
---|
1228 | ge = cuddE(G); |
---|
1229 | if (Cudd_IsComplement(g)) { |
---|
1230 | gt = Cudd_Not(gt); |
---|
1231 | ge = Cudd_Not(ge); |
---|
1232 | } |
---|
1233 | } else { |
---|
1234 | gt = ge = g; |
---|
1235 | } |
---|
1236 | |
---|
1237 | tt = cuddBddClosestCube(dd,ft,gt,bound); |
---|
1238 | if (tt == NULL) return(NULL); |
---|
1239 | cuddRef(tt); |
---|
1240 | ctt = separateCube(dd,tt,&dtt); |
---|
1241 | if (ctt == NULL) { |
---|
1242 | Cudd_RecursiveDeref(dd, tt); |
---|
1243 | return(NULL); |
---|
1244 | } |
---|
1245 | cuddRef(ctt); |
---|
1246 | Cudd_RecursiveDeref(dd, tt); |
---|
1247 | minD = dtt; |
---|
1248 | bound = ddMin(bound,minD); |
---|
1249 | |
---|
1250 | ee = cuddBddClosestCube(dd,fe,ge,bound); |
---|
1251 | if (ee == NULL) { |
---|
1252 | Cudd_RecursiveDeref(dd, ctt); |
---|
1253 | return(NULL); |
---|
1254 | } |
---|
1255 | cuddRef(ee); |
---|
1256 | cee = separateCube(dd,ee,&dee); |
---|
1257 | if (cee == NULL) { |
---|
1258 | Cudd_RecursiveDeref(dd, ctt); |
---|
1259 | Cudd_RecursiveDeref(dd, ee); |
---|
1260 | return(NULL); |
---|
1261 | } |
---|
1262 | cuddRef(cee); |
---|
1263 | Cudd_RecursiveDeref(dd, ee); |
---|
1264 | minD = ddMin(dtt, dee); |
---|
1265 | if (minD <= CUDD_CONST_INDEX) bound = ddMin(bound,minD-1); |
---|
1266 | |
---|
1267 | if (minD > 0 && topf == topg) { |
---|
1268 | DdNode *te = cuddBddClosestCube(dd,ft,ge,bound-1); |
---|
1269 | if (te == NULL) { |
---|
1270 | Cudd_RecursiveDeref(dd, ctt); |
---|
1271 | Cudd_RecursiveDeref(dd, cee); |
---|
1272 | return(NULL); |
---|
1273 | } |
---|
1274 | cuddRef(te); |
---|
1275 | cte = separateCube(dd,te,&dte); |
---|
1276 | if (cte == NULL) { |
---|
1277 | Cudd_RecursiveDeref(dd, ctt); |
---|
1278 | Cudd_RecursiveDeref(dd, cee); |
---|
1279 | Cudd_RecursiveDeref(dd, te); |
---|
1280 | return(NULL); |
---|
1281 | } |
---|
1282 | cuddRef(cte); |
---|
1283 | Cudd_RecursiveDeref(dd, te); |
---|
1284 | dte += 1.0; |
---|
1285 | minD = ddMin(minD, dte); |
---|
1286 | } else { |
---|
1287 | cte = azero; |
---|
1288 | cuddRef(cte); |
---|
1289 | dte = CUDD_CONST_INDEX + 1.0; |
---|
1290 | } |
---|
1291 | if (minD <= CUDD_CONST_INDEX) bound = ddMin(bound,minD-1); |
---|
1292 | |
---|
1293 | if (minD > 0 && topf == topg) { |
---|
1294 | DdNode *et = cuddBddClosestCube(dd,fe,gt,bound-1); |
---|
1295 | if (et == NULL) { |
---|
1296 | Cudd_RecursiveDeref(dd, ctt); |
---|
1297 | Cudd_RecursiveDeref(dd, cee); |
---|
1298 | Cudd_RecursiveDeref(dd, cte); |
---|
1299 | return(NULL); |
---|
1300 | } |
---|
1301 | cuddRef(et); |
---|
1302 | cet = separateCube(dd,et,&det); |
---|
1303 | if (cet == NULL) { |
---|
1304 | Cudd_RecursiveDeref(dd, ctt); |
---|
1305 | Cudd_RecursiveDeref(dd, cee); |
---|
1306 | Cudd_RecursiveDeref(dd, cte); |
---|
1307 | Cudd_RecursiveDeref(dd, et); |
---|
1308 | return(NULL); |
---|
1309 | } |
---|
1310 | cuddRef(cet); |
---|
1311 | Cudd_RecursiveDeref(dd, et); |
---|
1312 | det += 1.0; |
---|
1313 | minD = ddMin(minD, det); |
---|
1314 | } else { |
---|
1315 | cet = azero; |
---|
1316 | cuddRef(cet); |
---|
1317 | det = CUDD_CONST_INDEX + 1.0; |
---|
1318 | } |
---|
1319 | |
---|
1320 | if (minD == dtt) { |
---|
1321 | if (dtt == dee && ctt == cee) { |
---|
1322 | res = createResult(dd,CUDD_CONST_INDEX,1,ctt,dtt); |
---|
1323 | } else { |
---|
1324 | res = createResult(dd,index,1,ctt,dtt); |
---|
1325 | } |
---|
1326 | } else if (minD == dee) { |
---|
1327 | res = createResult(dd,index,0,cee,dee); |
---|
1328 | } else if (minD == dte) { |
---|
1329 | #ifdef DD_DEBUG |
---|
1330 | assert(topf == topg); |
---|
1331 | #endif |
---|
1332 | res = createResult(dd,index,1,cte,dte); |
---|
1333 | } else { |
---|
1334 | #ifdef DD_DEBUG |
---|
1335 | assert(topf == topg); |
---|
1336 | #endif |
---|
1337 | res = createResult(dd,index,0,cet,det); |
---|
1338 | } |
---|
1339 | if (res == NULL) { |
---|
1340 | Cudd_RecursiveDeref(dd, ctt); |
---|
1341 | Cudd_RecursiveDeref(dd, cee); |
---|
1342 | Cudd_RecursiveDeref(dd, cte); |
---|
1343 | Cudd_RecursiveDeref(dd, cet); |
---|
1344 | return(NULL); |
---|
1345 | } |
---|
1346 | cuddRef(res); |
---|
1347 | Cudd_RecursiveDeref(dd, ctt); |
---|
1348 | Cudd_RecursiveDeref(dd, cee); |
---|
1349 | Cudd_RecursiveDeref(dd, cte); |
---|
1350 | Cudd_RecursiveDeref(dd, cet); |
---|
1351 | |
---|
1352 | /* Only cache results that are different from azero to avoid |
---|
1353 | ** storing results that depend on the value of the bound. */ |
---|
1354 | if ((F->ref != 1 || G->ref != 1) && res != azero) |
---|
1355 | cuddCacheInsert2(dd,(DD_CTFP) Cudd_bddClosestCube, f, g, res); |
---|
1356 | |
---|
1357 | cuddDeref(res); |
---|
1358 | return(res); |
---|
1359 | |
---|
1360 | } /* end of cuddBddClosestCube */ |
---|
1361 | |
---|
1362 | |
---|
1363 | /*---------------------------------------------------------------------------*/ |
---|
1364 | /* Definition of static functions */ |
---|
1365 | /*---------------------------------------------------------------------------*/ |
---|
1366 | |
---|
1367 | |
---|
1368 | /**Function******************************************************************** |
---|
1369 | |
---|
1370 | Synopsis [Performs the recursive step of Cudd_MinHammingDist.] |
---|
1371 | |
---|
1372 | Description [Performs the recursive step of Cudd_MinHammingDist. |
---|
1373 | It is based on the following identity. Let H(f) be the |
---|
1374 | minimum Hamming distance of the minterms of f from the reference |
---|
1375 | minterm. Then: |
---|
1376 | <xmp> |
---|
1377 | H(f) = min(H(f0)+h0,H(f1)+h1) |
---|
1378 | </xmp> |
---|
1379 | where f0 and f1 are the two cofactors of f with respect to its top |
---|
1380 | variable; h0 is 1 if the minterm assigns 1 to the top variable of f; |
---|
1381 | h1 is 1 if the minterm assigns 0 to the top variable of f. |
---|
1382 | The upper bound on the distance is used to bound the depth of the |
---|
1383 | recursion. |
---|
1384 | Returns the minimum distance unless it exceeds the upper bound or |
---|
1385 | computation fails.] |
---|
1386 | |
---|
1387 | SideEffects [None] |
---|
1388 | |
---|
1389 | SeeAlso [Cudd_MinHammingDist] |
---|
1390 | |
---|
1391 | ******************************************************************************/ |
---|
1392 | static int |
---|
1393 | cuddMinHammingDistRecur( |
---|
1394 | DdNode * f, |
---|
1395 | int *minterm, |
---|
1396 | DdHashTable * table, |
---|
1397 | int upperBound) |
---|
1398 | { |
---|
1399 | DdNode *F, *Ft, *Fe; |
---|
1400 | double h, hT, hE; |
---|
1401 | DdNode *zero, *res; |
---|
1402 | DdManager *dd = table->manager; |
---|
1403 | |
---|
1404 | statLine(dd); |
---|
1405 | if (upperBound == 0) return(0); |
---|
1406 | |
---|
1407 | F = Cudd_Regular(f); |
---|
1408 | |
---|
1409 | if (cuddIsConstant(F)) { |
---|
1410 | zero = Cudd_Not(DD_ONE(dd)); |
---|
1411 | if (f == dd->background || f == zero) { |
---|
1412 | return(upperBound); |
---|
1413 | } else { |
---|
1414 | return(0); |
---|
1415 | } |
---|
1416 | } |
---|
1417 | if ((res = cuddHashTableLookup1(table,f)) != NULL) { |
---|
1418 | h = cuddV(res); |
---|
1419 | if (res->ref == 0) { |
---|
1420 | dd->dead++; |
---|
1421 | dd->constants.dead++; |
---|
1422 | } |
---|
1423 | return((int) h); |
---|
1424 | } |
---|
1425 | |
---|
1426 | Ft = cuddT(F); Fe = cuddE(F); |
---|
1427 | if (Cudd_IsComplement(f)) { |
---|
1428 | Ft = Cudd_Not(Ft); Fe = Cudd_Not(Fe); |
---|
1429 | } |
---|
1430 | if (minterm[F->index] == 0) { |
---|
1431 | DdNode *temp = Ft; |
---|
1432 | Ft = Fe; Fe = temp; |
---|
1433 | } |
---|
1434 | |
---|
1435 | hT = cuddMinHammingDistRecur(Ft,minterm,table,upperBound); |
---|
1436 | if (hT == CUDD_OUT_OF_MEM) return(CUDD_OUT_OF_MEM); |
---|
1437 | if (hT == 0) { |
---|
1438 | hE = upperBound; |
---|
1439 | } else { |
---|
1440 | hE = cuddMinHammingDistRecur(Fe,minterm,table,upperBound - 1); |
---|
1441 | if (hE == CUDD_OUT_OF_MEM) return(CUDD_OUT_OF_MEM); |
---|
1442 | } |
---|
1443 | h = ddMin(hT, hE + 1); |
---|
1444 | |
---|
1445 | if (F->ref != 1) { |
---|
1446 | ptrint fanout = (ptrint) F->ref; |
---|
1447 | cuddSatDec(fanout); |
---|
1448 | res = cuddUniqueConst(dd, (CUDD_VALUE_TYPE) h); |
---|
1449 | if (!cuddHashTableInsert1(table,f,res,fanout)) { |
---|
1450 | cuddRef(res); Cudd_RecursiveDeref(dd, res); |
---|
1451 | return(CUDD_OUT_OF_MEM); |
---|
1452 | } |
---|
1453 | } |
---|
1454 | |
---|
1455 | return((int) h); |
---|
1456 | |
---|
1457 | } /* end of cuddMinHammingDistRecur */ |
---|
1458 | |
---|
1459 | |
---|
1460 | /**Function******************************************************************** |
---|
1461 | |
---|
1462 | Synopsis [Separates cube from distance.] |
---|
1463 | |
---|
1464 | Description [Separates cube from distance. Returns the cube if |
---|
1465 | successful; NULL otherwise.] |
---|
1466 | |
---|
1467 | SideEffects [The distance is returned as a side effect.] |
---|
1468 | |
---|
1469 | SeeAlso [cuddBddClosestCube createResult] |
---|
1470 | |
---|
1471 | ******************************************************************************/ |
---|
1472 | static DdNode * |
---|
1473 | separateCube( |
---|
1474 | DdManager *dd, |
---|
1475 | DdNode *f, |
---|
1476 | CUDD_VALUE_TYPE *distance) |
---|
1477 | { |
---|
1478 | DdNode *cube, *t; |
---|
1479 | |
---|
1480 | /* One and zero are special cases because the distance is implied. */ |
---|
1481 | if (Cudd_IsConstant(f)) { |
---|
1482 | *distance = (f == DD_ONE(dd)) ? 0.0 : |
---|
1483 | (1.0 + (CUDD_VALUE_TYPE) CUDD_CONST_INDEX); |
---|
1484 | return(f); |
---|
1485 | } |
---|
1486 | |
---|
1487 | /* Find out which branch points to the distance and replace the top |
---|
1488 | ** node with one pointing to zero instead. */ |
---|
1489 | t = cuddT(f); |
---|
1490 | if (Cudd_IsConstant(t) && cuddV(t) <= 0) { |
---|
1491 | #ifdef DD_DEBUG |
---|
1492 | assert(!Cudd_IsConstant(cuddE(f)) || cuddE(f) == DD_ONE(dd)); |
---|
1493 | #endif |
---|
1494 | *distance = -cuddV(t); |
---|
1495 | cube = cuddUniqueInter(dd, f->index, DD_ZERO(dd), cuddE(f)); |
---|
1496 | } else { |
---|
1497 | #ifdef DD_DEBUG |
---|
1498 | assert(!Cudd_IsConstant(t) || t == DD_ONE(dd)); |
---|
1499 | #endif |
---|
1500 | *distance = -cuddV(cuddE(f)); |
---|
1501 | cube = cuddUniqueInter(dd, f->index, t, DD_ZERO(dd)); |
---|
1502 | } |
---|
1503 | |
---|
1504 | return(cube); |
---|
1505 | |
---|
1506 | } /* end of separateCube */ |
---|
1507 | |
---|
1508 | |
---|
1509 | /**Function******************************************************************** |
---|
1510 | |
---|
1511 | Synopsis [Builds a result for cache storage.] |
---|
1512 | |
---|
1513 | Description [Builds a result for cache storage. Returns a pointer |
---|
1514 | to the resulting ADD if successful; NULL otherwise.] |
---|
1515 | |
---|
1516 | SideEffects [None] |
---|
1517 | |
---|
1518 | SeeAlso [cuddBddClosestCube separateCube] |
---|
1519 | |
---|
1520 | ******************************************************************************/ |
---|
1521 | static DdNode * |
---|
1522 | createResult( |
---|
1523 | DdManager *dd, |
---|
1524 | unsigned int index, |
---|
1525 | unsigned int phase, |
---|
1526 | DdNode *cube, |
---|
1527 | CUDD_VALUE_TYPE distance) |
---|
1528 | { |
---|
1529 | DdNode *res, *constant; |
---|
1530 | |
---|
1531 | /* Special case. The cube is either one or zero, and we do not |
---|
1532 | ** add any variables. Hence, the result is also one or zero, |
---|
1533 | ** and the distance remains implied by the value of the constant. */ |
---|
1534 | if (index == CUDD_CONST_INDEX && Cudd_IsConstant(cube)) return(cube); |
---|
1535 | |
---|
1536 | constant = cuddUniqueConst(dd,-distance); |
---|
1537 | if (constant == NULL) return(NULL); |
---|
1538 | cuddRef(constant); |
---|
1539 | |
---|
1540 | if (index == CUDD_CONST_INDEX) { |
---|
1541 | /* Replace the top node. */ |
---|
1542 | if (cuddT(cube) == DD_ZERO(dd)) { |
---|
1543 | res = cuddUniqueInter(dd,cube->index,constant,cuddE(cube)); |
---|
1544 | } else { |
---|
1545 | res = cuddUniqueInter(dd,cube->index,cuddT(cube),constant); |
---|
1546 | } |
---|
1547 | } else { |
---|
1548 | /* Add a new top node. */ |
---|
1549 | #ifdef DD_DEBUG |
---|
1550 | assert(cuddI(dd,index) < cuddI(dd,cube->index)); |
---|
1551 | #endif |
---|
1552 | if (phase) { |
---|
1553 | res = cuddUniqueInter(dd,index,cube,constant); |
---|
1554 | } else { |
---|
1555 | res = cuddUniqueInter(dd,index,constant,cube); |
---|
1556 | } |
---|
1557 | } |
---|
1558 | if (res == NULL) { |
---|
1559 | Cudd_RecursiveDeref(dd, constant); |
---|
1560 | return(NULL); |
---|
1561 | } |
---|
1562 | cuddDeref(constant); /* safe because constant is part of res */ |
---|
1563 | |
---|
1564 | return(res); |
---|
1565 | |
---|
1566 | } /* end of createResult */ |
---|