source: vis_dev/glu-2.3/src/cuBdd/cuddPriority.c @ 42

Last change on this file since 42 was 13, checked in by cecile, 13 years ago

library glu 2.3
File size: 57.5 KB
Line 
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-2004, 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
101static char rcsid[] DD_UNUSED = "$Id: cuddPriority.c,v 1.33 2009/02/20 02:14:58 fabio Exp $";
102#endif
103
104/*---------------------------------------------------------------------------*/
105/* Macro declarations                                                        */
106/*---------------------------------------------------------------------------*/
107
108
109/**AutomaticStart*************************************************************/
110
111/*---------------------------------------------------------------------------*/
112/* Static function prototypes                                                */
113/*---------------------------------------------------------------------------*/
114static int cuddMinHammingDistRecur (DdNode * f, int *minterm, DdHashTable * table, int upperBound);
115static DdNode * separateCube (DdManager *dd, DdNode *f, CUDD_VALUE_TYPE *distance);
116static 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 vectore
137  is a vector of auxiliary variables, used during the computation. This
138  vector is optional. If a NULL value is passed instead,
139  Cudd_PrioritySelect will create the working variables on the fly.
140  The sizes of x and y (and z if it is not NULL) should equal n.
141  The priority function Pi can be passed as a BDD, or can be built by
142  Cudd_PrioritySelect. If NULL is passed instead of a DdNode *,
143  parameter Pifunc is used by Cudd_PrioritySelect to build a BDD for the
144  priority function. (Pifunc is a pointer to a C function.) If Pi is not
145  NULL, then Pifunc is ignored. Pifunc should have the same interface as
146  the standard priority functions (e.g., Cudd_Dxygtdxz).
147  Cudd_PrioritySelect and Cudd_CProjection can sometimes be used
148  interchangeably. Specifically, calling Cudd_PrioritySelect with
149  Cudd_Xgty as Pifunc produces the same result as calling
150  Cudd_CProjection with the all-zero minterm as reference minterm.
151  However, depending on the application, one or the other may be
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******************************************************************************/
170DdNode *
171Cudd_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
243endgame:
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 &gt; y.]
260
261  Description [This function generates a BDD for the function x &gt; 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******************************************************************************/
275DdNode *
276Cudd_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******************************************************************************/
340DdNode *
341Cudd_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******************************************************************************/
403DdNode *
404Cudd_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) &gt; d(x,z).]
472
473  Description [This function generates a BDD for the function d(x,y)
474  &gt; 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******************************************************************************/
489DdNode *
490Cudd_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) &gt; d(y,z).]
599
600  Description [This function generates a BDD for the function d(x,y)
601  &gt; 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******************************************************************************/
616DdNode *
617Cudd_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 &ge; c.]
726
727  Description [This function generates a BDD for the function x -y &ge; 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******************************************************************************/
739DdNode *
740Cudd_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******************************************************************************/
927DdNode *
928Cudd_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 &le; x &le; upperB.]
1102
1103  Description [This function generates a BDD for the function
1104  lowerB &le; x &le; 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 &le; x and x &le; upperB, and they
1109  are finally conjoined.]
1110
1111  SideEffects [None]
1112
1113  SeeAlso     [Cudd_Xgty]
1114
1115******************************************************************************/
1116DdNode *
1117Cudd_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******************************************************************************/
1195DdNode *
1196Cudd_CProjection(
1197  DdManager * dd,
1198  DdNode * R,
1199  DdNode * Y)
1200{
1201    DdNode *res;
1202    DdNode *support;
1203
1204    if (cuddCheckCube(dd,Y) == 0) {
1205        (void) fprintf(dd->err,
1206        "Error: The third argument of Cudd_CProjection should be a cube\n");
1207        dd->errorCode = CUDD_INVALID_ARG;
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******************************************************************************/
1250DdNode *
1251Cudd_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******************************************************************************/
1313int
1314Cudd_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******************************************************************************/
1354DdNode *
1355Cudd_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******************************************************************************/
1420DdNode *
1421cuddCProjectionRecur(
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******************************************************************************/
1641DdNode *
1642cuddBddClosestCube(
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******************************************************************************/
1853static int
1854cuddMinHammingDistRecur(
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******************************************************************************/
1933static DdNode *
1934separateCube(
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******************************************************************************/
1982static DdNode *
1983createResult(
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 */
Note: See TracBrowser for help on using the repository browser.