distr/cudd/cuddPriority.c

   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
 101 static 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 /*---------------------------------------------------------------------------*/
 114 static int cuddMinHammingDistRecur (DdNode * f, int *minterm, DdHashTable * table, int upperBound);
 115 static DdNode * separateCube (DdManager *dd, DdNode *f, CUDD_VALUE_TYPE *distance);
 116 static DdNode * createResult (DdManager *dd, unsigned int index, unsigned int phase, DdNode *cube, CUDD_VALUE_TYPE distance);
 117
 118 /**AutomaticEnd***************************************************************/
 119
 120
 121 /*---------------------------------------------------------------------------*/
 122 /* Definition of exported functions                                          */
 123 /*---------------------------------------------------------------------------*/
 124
 125
 126 /**Function********************************************************************
 127
 128   Synopsis    [Selects pairs from R using a priority function.]
 129
 130   Description [Selects pairs from a relation R(x,y) (given as a BDD)
 131   in such a way that a given x appears in one pair only. Uses a
 132   priority function to determine which y should be paired to a given x.
 133   Cudd_PrioritySelect returns a pointer to
 134   the selected function if successful; NULL otherwise.
 135   Three of the arguments--x, y, and z--are vectors of BDD variables.
 136   The first two are the variables on which R depends. The third 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 ******************************************************************************/
 170 DdNode *
 171 Cudd_PrioritySelect(
 172   DdManager * dd /* manager */,
 173   DdNode * R /* BDD of the relation */,
 174   DdNode ** x /* array of x variables */,
 175   DdNode ** y /* array of y variables */,
 176   DdNode ** z /* array of z variables (optional: may be NULL) */,
 177   DdNode * Pi /* BDD of the priority function (optional: may be NULL) */,
 178   int  n /* size of x, y, and z */,
 179   DD_PRFP Pifunc /* function used to build Pi if it is NULL */)
 180 {
 181     DdNode *res = NULL;
 182     DdNode *zcube = NULL;
 183     DdNode *Rxz, *Q;
 184     int createdZ = 0;
 185     int createdPi = 0;
 186     int i;
 187
 188     /* Create z variables if needed. */
 189     if (z == NULL) {
 190         if (Pi != NULL) return(NULL);
 191         z = ALLOC(DdNode *,n);
 192         if (z == NULL) {
 193             dd->errorCode = CUDD_MEMORY_OUT;
 194             return(NULL);
 195         }
 196         createdZ = 1;
 197         for (i = 0; i < n; i++) {
 198             if (dd->size >= (int) CUDD_MAXINDEX - 1) goto endgame;
 199             z[i] = cuddUniqueInter(dd,dd->size,dd->one,Cudd_Not(dd->one));
 200             if (z[i] == NULL) goto endgame;
 201         }
 202     }
 203
 204     /* Create priority function BDD if needed. */
 205     if (Pi == NULL) {
 206         Pi = Pifunc(dd,n,x,y,z);
 207         if (Pi == NULL) goto endgame;
 208         createdPi = 1;
 209         cuddRef(Pi);
 210     }
 211
 212     /* Initialize abstraction cube. */
 213     zcube = DD_ONE(dd);
 214     cuddRef(zcube);
 215     for (i = n - 1; i >= 0; i--) {
 216         DdNode *tmpp;
 217         tmpp = Cudd_bddAnd(dd,z[i],zcube);
 218         if (tmpp == NULL) goto endgame;
 219         cuddRef(tmpp);
 220         Cudd_RecursiveDeref(dd,zcube);
 221         zcube = tmpp;
 222     }
 223
 224     /* Compute subset of (x,y) pairs. */
 225     Rxz = Cudd_bddSwapVariables(dd,R,y,z,n);
 226     if (Rxz == NULL) goto endgame;
 227     cuddRef(Rxz);
 228     Q = Cudd_bddAndAbstract(dd,Rxz,Pi,zcube);
 229     if (Q == NULL) {
 230         Cudd_RecursiveDeref(dd,Rxz);
 231         goto endgame;
 232     }
 233     cuddRef(Q);
 234     Cudd_RecursiveDeref(dd,Rxz);
 235     res = Cudd_bddAnd(dd,R,Cudd_Not(Q));
 236     if (res == NULL) {
 237         Cudd_RecursiveDeref(dd,Q);
 238         goto endgame;
 239     }
 240     cuddRef(res);
 241     Cudd_RecursiveDeref(dd,Q);
 242
 243 endgame:
 244     if (zcube != NULL) Cudd_RecursiveDeref(dd,zcube);
 245     if (createdZ) {
 246         FREE(z);
 247     }
 248     if (createdPi) {
 249         Cudd_RecursiveDeref(dd,Pi);
 250     }
 251     if (res != NULL) cuddDeref(res);
 252     return(res);
 253
 254 } /* Cudd_PrioritySelect */
 255
 256
 257 /**Function********************************************************************
 258
 259   Synopsis    [Generates a BDD for the function x &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 ******************************************************************************/
 275 DdNode *
 276 Cudd_Xgty(
 277   DdManager * dd /* DD manager */,
 278   int  N /* number of x and y variables */,
 279   DdNode ** z /* array of z variables: unused */,
 280   DdNode ** x /* array of x variables */,
 281   DdNode ** y /* array of y variables */)
 282 {
 283     DdNode *u, *v, *w;
 284     int     i;
 285
 286     /* Build bottom part of BDD outside loop. */
 287     u = Cudd_bddAnd(dd, x[N-1], Cudd_Not(y[N-1]));
 288     if (u == NULL) return(NULL);
 289     cuddRef(u);
 290
 291     /* Loop to build the rest of the BDD. */
 292     for (i = N-2; i >= 0; i--) {
 293         v = Cudd_bddAnd(dd, y[i], Cudd_Not(u));
 294         if (v == NULL) {
 295             Cudd_RecursiveDeref(dd, u);
 296             return(NULL);
 297         }
 298         cuddRef(v);
 299         w = Cudd_bddAnd(dd, Cudd_Not(y[i]), u);
 300         if (w == NULL) {
 301             Cudd_RecursiveDeref(dd, u);
 302             Cudd_RecursiveDeref(dd, v);
 303             return(NULL);
 304         }
 305         cuddRef(w);
 306         Cudd_RecursiveDeref(dd, u);
 307         u = Cudd_bddIte(dd, x[i], Cudd_Not(v), w);
 308         if (u == NULL) {
 309             Cudd_RecursiveDeref(dd, v);
 310             Cudd_RecursiveDeref(dd, w);
 311             return(NULL);
 312         }
 313         cuddRef(u);
 314         Cudd_RecursiveDeref(dd, v);
 315         Cudd_RecursiveDeref(dd, w);
 316
 317     }
 318     cuddDeref(u);
 319     return(u);
 320
 321 } /* end of Cudd_Xgty */
 322
 323
 324 /**Function********************************************************************
 325
 326   Synopsis    [Generates a BDD for the function x==y.]
 327
 328   Description [This function generates a BDD for the function x==y.
 329   Both x and y are N-bit numbers, x\[0\] x\[1\] ... x\[N-1\] and
 330   y\[0\] y\[1\] ...  y\[N-1\], with 0 the most significant bit.
 331   The BDD is built bottom-up.
 332   It has 3*N-1 internal nodes, if the variables are ordered as follows:
 333   x\[0\] y\[0\] x\[1\] y\[1\] ... x\[N-1\] y\[N-1\]. ]
 334
 335   SideEffects [None]
 336
 337   SeeAlso     [Cudd_addXeqy]
 338
 339 ******************************************************************************/
 340 DdNode *
 341 Cudd_Xeqy(
 342   DdManager * dd /* DD manager */,
 343   int  N /* number of x and y variables */,
 344   DdNode ** x /* array of x variables */,
 345   DdNode ** y /* array of y variables */)
 346 {
 347     DdNode *u, *v, *w;
 348     int     i;
 349
 350     /* Build bottom part of BDD outside loop. */
 351     u = Cudd_bddIte(dd, x[N-1], y[N-1], Cudd_Not(y[N-1]));
 352     if (u == NULL) return(NULL);
 353     cuddRef(u);
 354
 355     /* Loop to build the rest of the BDD. */
 356     for (i = N-2; i >= 0; i--) {
 357         v = Cudd_bddAnd(dd, y[i], u);
 358         if (v == NULL) {
 359             Cudd_RecursiveDeref(dd, u);
 360             return(NULL);
 361         }
 362         cuddRef(v);
 363         w = Cudd_bddAnd(dd, Cudd_Not(y[i]), u);
 364         if (w == NULL) {
 365             Cudd_RecursiveDeref(dd, u);
 366             Cudd_RecursiveDeref(dd, v);
 367             return(NULL);
 368         }
 369         cuddRef(w);
 370         Cudd_RecursiveDeref(dd, u);
 371         u = Cudd_bddIte(dd, x[i], v, w);
 372         if (u == NULL) {
 373             Cudd_RecursiveDeref(dd, v);
 374             Cudd_RecursiveDeref(dd, w);
 375             return(NULL);
 376         }
 377         cuddRef(u);
 378         Cudd_RecursiveDeref(dd, v);
 379         Cudd_RecursiveDeref(dd, w);
 380     }
 381     cuddDeref(u);
 382     return(u);
 383
 384 } /* end of Cudd_Xeqy */
 385
 386
 387 /**Function********************************************************************
 388
 389   Synopsis    [Generates an ADD for the function x==y.]
 390
 391   Description [This function generates an ADD for the function x==y.
 392   Both x and y are N-bit numbers, x\[0\] x\[1\] ... x\[N-1\] and
 393   y\[0\] y\[1\] ...  y\[N-1\], with 0 the most significant bit.
 394   The ADD is built bottom-up.
 395   It has 3*N-1 internal nodes, if the variables are ordered as follows:
 396   x\[0\] y\[0\] x\[1\] y\[1\] ... x\[N-1\] y\[N-1\]. ]
 397
 398   SideEffects [None]
 399
 400   SeeAlso     [Cudd_Xeqy]
 401
 402 ******************************************************************************/
 403 DdNode *
 404 Cudd_addXeqy(
 405   DdManager * dd /* DD manager */,
 406   int  N /* number of x and y variables */,
 407   DdNode ** x /* array of x variables */,
 408   DdNode ** y /* array of y variables */)
 409 {
 410     DdNode *one, *zero;
 411     DdNode *u, *v, *w;
 412     int     i;
 413
 414     one = DD_ONE(dd);
 415     zero = DD_ZERO(dd);
 416
 417     /* Build bottom part of ADD outside loop. */
 418     v = Cudd_addIte(dd, y[N-1], one, zero);
 419     if (v == NULL) return(NULL);
 420     cuddRef(v);
 421     w = Cudd_addIte(dd, y[N-1], zero, one);
 422     if (w == NULL) {
 423         Cudd_RecursiveDeref(dd, v);
 424         return(NULL);
 425     }
 426     cuddRef(w);
 427     u = Cudd_addIte(dd, x[N-1], v, w);
 428     if (u == NULL) {
 429         Cudd_RecursiveDeref(dd, v);
 430         Cudd_RecursiveDeref(dd, w);
 431         return(NULL);
 432     }
 433     cuddRef(u);
 434     Cudd_RecursiveDeref(dd, v);
 435     Cudd_RecursiveDeref(dd, w);
 436
 437     /* Loop to build the rest of the ADD. */
 438     for (i = N-2; i >= 0; i--) {
 439         v = Cudd_addIte(dd, y[i], u, zero);
 440         if (v == NULL) {
 441             Cudd_RecursiveDeref(dd, u);
 442             return(NULL);
 443         }
 444         cuddRef(v);
 445         w = Cudd_addIte(dd, y[i], zero, u);
 446         if (w == NULL) {
 447             Cudd_RecursiveDeref(dd, u);
 448             Cudd_RecursiveDeref(dd, v);
 449             return(NULL);
 450         }
 451         cuddRef(w);
 452         Cudd_RecursiveDeref(dd, u);
 453         u = Cudd_addIte(dd, x[i], v, w);
 454         if (w == NULL) {
 455             Cudd_RecursiveDeref(dd, v);
 456             Cudd_RecursiveDeref(dd, w);
 457             return(NULL);
 458         }
 459         cuddRef(u);
 460         Cudd_RecursiveDeref(dd, v);
 461         Cudd_RecursiveDeref(dd, w);
 462     }
 463     cuddDeref(u);
 464     return(u);
 465
 466 } /* end of Cudd_addXeqy */
 467
 468
 469 /**Function********************************************************************
 470
 471   Synopsis    [Generates a BDD for the function d(x,y) &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 ******************************************************************************/
 489 DdNode *
 490 Cudd_Dxygtdxz(
 491   DdManager * dd /* DD manager */,
 492   int  N /* number of x, y, and z variables */,
 493   DdNode ** x /* array of x variables */,
 494   DdNode ** y /* array of y variables */,
 495   DdNode ** z /* array of z variables */)
 496 {
 497     DdNode *one, *zero;
 498     DdNode *z1, *z2, *z3, *z4, *y1_, *y2, *x1;
 499     int     i;
 500
 501     one = DD_ONE(dd);
 502     zero = Cudd_Not(one);
 503
 504     /* Build bottom part of BDD outside loop. */
 505     y1_ = Cudd_bddIte(dd, y[N-1], one, Cudd_Not(z[N-1]));
 506     if (y1_ == NULL) return(NULL);
 507     cuddRef(y1_);
 508     y2 = Cudd_bddIte(dd, y[N-1], z[N-1], one);
 509     if (y2 == NULL) {
 510         Cudd_RecursiveDeref(dd, y1_);
 511         return(NULL);
 512     }
 513     cuddRef(y2);
 514     x1 = Cudd_bddIte(dd, x[N-1], y1_, y2);
 515     if (x1 == NULL) {
 516         Cudd_RecursiveDeref(dd, y1_);
 517         Cudd_RecursiveDeref(dd, y2);
 518         return(NULL);
 519     }
 520     cuddRef(x1);
 521     Cudd_RecursiveDeref(dd, y1_);
 522     Cudd_RecursiveDeref(dd, y2);
 523
 524     /* Loop to build the rest of the BDD. */
 525     for (i = N-2; i >= 0; i--) {
 526         z1 = Cudd_bddIte(dd, z[i], one, Cudd_Not(x1));
 527         if (z1 == NULL) {
 528             Cudd_RecursiveDeref(dd, x1);
 529             return(NULL);
 530         }
 531         cuddRef(z1);
 532         z2 = Cudd_bddIte(dd, z[i], x1, one);
 533         if (z2 == NULL) {
 534             Cudd_RecursiveDeref(dd, x1);
 535             Cudd_RecursiveDeref(dd, z1);
 536             return(NULL);
 537         }
 538         cuddRef(z2);
 539         z3 = Cudd_bddIte(dd, z[i], one, x1);
 540         if (z3 == NULL) {
 541             Cudd_RecursiveDeref(dd, x1);
 542             Cudd_RecursiveDeref(dd, z1);
 543             Cudd_RecursiveDeref(dd, z2);
 544             return(NULL);
 545         }
 546         cuddRef(z3);
 547         z4 = Cudd_bddIte(dd, z[i], x1, zero);
 548         if (z4 == NULL) {
 549             Cudd_RecursiveDeref(dd, x1);
 550             Cudd_RecursiveDeref(dd, z1);
 551             Cudd_RecursiveDeref(dd, z2);
 552             Cudd_RecursiveDeref(dd, z3);
 553             return(NULL);
 554         }
 555         cuddRef(z4);
 556         Cudd_RecursiveDeref(dd, x1);
 557         y1_ = Cudd_bddIte(dd, y[i], z2, Cudd_Not(z1));
 558         if (y1_ == NULL) {
 559             Cudd_RecursiveDeref(dd, z1);
 560             Cudd_RecursiveDeref(dd, z2);
 561             Cudd_RecursiveDeref(dd, z3);
 562             Cudd_RecursiveDeref(dd, z4);
 563             return(NULL);
 564         }
 565         cuddRef(y1_);
 566         y2 = Cudd_bddIte(dd, y[i], z4, z3);
 567         if (y2 == NULL) {
 568             Cudd_RecursiveDeref(dd, z1);
 569             Cudd_RecursiveDeref(dd, z2);
 570             Cudd_RecursiveDeref(dd, z3);
 571             Cudd_RecursiveDeref(dd, z4);
 572             Cudd_RecursiveDeref(dd, y1_);
 573             return(NULL);
 574         }
 575         cuddRef(y2);
 576         Cudd_RecursiveDeref(dd, z1);
 577         Cudd_RecursiveDeref(dd, z2);
 578         Cudd_RecursiveDeref(dd, z3);
 579         Cudd_RecursiveDeref(dd, z4);
 580         x1 = Cudd_bddIte(dd, x[i], y1_, y2);
 581         if (x1 == NULL) {
 582             Cudd_RecursiveDeref(dd, y1_);
 583             Cudd_RecursiveDeref(dd, y2);
 584             return(NULL);
 585         }
 586         cuddRef(x1);
 587         Cudd_RecursiveDeref(dd, y1_);
 588         Cudd_RecursiveDeref(dd, y2);
 589     }
 590     cuddDeref(x1);
 591     return(Cudd_Not(x1));
 592
 593 } /* end of Cudd_Dxygtdxz */
 594
 595
 596 /**Function********************************************************************
 597
 598   Synopsis    [Generates a BDD for the function d(x,y) &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 ******************************************************************************/
 616 DdNode *
 617 Cudd_Dxygtdyz(
 618   DdManager * dd /* DD manager */,
 619   int  N /* number of x, y, and z variables */,
 620   DdNode ** x /* array of x variables */,
 621   DdNode ** y /* array of y variables */,
 622   DdNode ** z /* array of z variables */)
 623 {
 624     DdNode *one, *zero;
 625     DdNode *z1, *z2, *z3, *z4, *y1_, *y2, *x1;
 626     int     i;
 627
 628     one = DD_ONE(dd);
 629     zero = Cudd_Not(one);
 630
 631     /* Build bottom part of BDD outside loop. */
 632     y1_ = Cudd_bddIte(dd, y[N-1], one, z[N-1]);
 633     if (y1_ == NULL) return(NULL);
 634     cuddRef(y1_);
 635     y2 = Cudd_bddIte(dd, y[N-1], z[N-1], zero);
 636     if (y2 == NULL) {
 637         Cudd_RecursiveDeref(dd, y1_);
 638         return(NULL);
 639     }
 640     cuddRef(y2);
 641     x1 = Cudd_bddIte(dd, x[N-1], y1_, Cudd_Not(y2));
 642     if (x1 == NULL) {
 643         Cudd_RecursiveDeref(dd, y1_);
 644         Cudd_RecursiveDeref(dd, y2);
 645         return(NULL);
 646     }
 647     cuddRef(x1);
 648     Cudd_RecursiveDeref(dd, y1_);
 649     Cudd_RecursiveDeref(dd, y2);
 650
 651     /* Loop to build the rest of the BDD. */
 652     for (i = N-2; i >= 0; i--) {
 653         z1 = Cudd_bddIte(dd, z[i], x1, zero);
 654         if (z1 == NULL) {
 655             Cudd_RecursiveDeref(dd, x1);
 656             return(NULL);
 657         }
 658         cuddRef(z1);
 659         z2 = Cudd_bddIte(dd, z[i], x1, one);
 660         if (z2 == NULL) {
 661             Cudd_RecursiveDeref(dd, x1);
 662             Cudd_RecursiveDeref(dd, z1);
 663             return(NULL);
 664         }
 665         cuddRef(z2);
 666         z3 = Cudd_bddIte(dd, z[i], one, x1);
 667         if (z3 == NULL) {
 668             Cudd_RecursiveDeref(dd, x1);
 669             Cudd_RecursiveDeref(dd, z1);
 670             Cudd_RecursiveDeref(dd, z2);
 671             return(NULL);
 672         }
 673         cuddRef(z3);
 674         z4 = Cudd_bddIte(dd, z[i], one, Cudd_Not(x1));
 675         if (z4 == NULL) {
 676             Cudd_RecursiveDeref(dd, x1);
 677             Cudd_RecursiveDeref(dd, z1);
 678             Cudd_RecursiveDeref(dd, z2);
 679             Cudd_RecursiveDeref(dd, z3);
 680             return(NULL);
 681         }
 682         cuddRef(z4);
 683         Cudd_RecursiveDeref(dd, x1);
 684         y1_ = Cudd_bddIte(dd, y[i], z2, z1);
 685         if (y1_ == NULL) {
 686             Cudd_RecursiveDeref(dd, z1);
 687             Cudd_RecursiveDeref(dd, z2);
 688             Cudd_RecursiveDeref(dd, z3);
 689             Cudd_RecursiveDeref(dd, z4);
 690             return(NULL);
 691         }
 692         cuddRef(y1_);
 693         y2 = Cudd_bddIte(dd, y[i], z4, Cudd_Not(z3));
 694         if (y2 == NULL) {
 695             Cudd_RecursiveDeref(dd, z1);
 696             Cudd_RecursiveDeref(dd, z2);
 697             Cudd_RecursiveDeref(dd, z3);
 698             Cudd_RecursiveDeref(dd, z4);
 699             Cudd_RecursiveDeref(dd, y1_);
 700             return(NULL);
 701         }
 702         cuddRef(y2);
 703         Cudd_RecursiveDeref(dd, z1);
 704         Cudd_RecursiveDeref(dd, z2);
 705         Cudd_RecursiveDeref(dd, z3);
 706         Cudd_RecursiveDeref(dd, z4);
 707         x1 = Cudd_bddIte(dd, x[i], y1_, Cudd_Not(y2));
 708         if (x1 == NULL) {
 709             Cudd_RecursiveDeref(dd, y1_);
 710             Cudd_RecursiveDeref(dd, y2);
 711             return(NULL);
 712         }
 713         cuddRef(x1);
 714         Cudd_RecursiveDeref(dd, y1_);
 715         Cudd_RecursiveDeref(dd, y2);
 716     }
 717     cuddDeref(x1);
 718     return(Cudd_Not(x1));
 719
 720 } /* end of Cudd_Dxygtdyz */
 721
 722
 723 /**Function********************************************************************
 724
 725   Synopsis    [Generates a BDD for the function x - y &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 ******************************************************************************/
 739 DdNode *
 740 Cudd_Inequality(
 741   DdManager * dd /* DD manager */,
 742   int  N /* number of x and y variables */,
 743   int c /* right-hand side constant */,
 744   DdNode ** x /* array of x variables */,
 745   DdNode ** y /* array of y variables */)
 746 {
 747     /* The nodes at level i represent values of the difference that are
 748     ** multiples of 2^i.  We use variables with names starting with k
 749     ** to denote the multipliers of 2^i in such multiples. */
 750     int kTrue = c;
 751     int kFalse = c - 1;
 752     /* Mask used to compute the ceiling function.  Since we divide by 2^i,
 753     ** we want to know whether the dividend is a multiple of 2^i.  If it is,
 754     ** then ceiling and floor coincide; otherwise, they differ by one. */
 755     int mask = 1;
 756     int i;
 757
 758     DdNode *f = NULL;           /* the eventual result */
 759     DdNode *one = DD_ONE(dd);
 760     DdNode *zero = Cudd_Not(one);
 761
 762     /* Two x-labeled nodes are created at most at each iteration.  They are
 763     ** stored, along with their k values, in these variables.  At each level,
 764     ** the old nodes are freed and the new nodes are copied into the old map.
 765     */
 766     DdNode *map[2];
 767     int invalidIndex = 1 << (N-1);
 768     int index[2] = {invalidIndex, invalidIndex};
 769
 770     /* This should never happen. */
 771     if (N < 0) return(NULL);
 772
 773     /* If there are no bits, both operands are 0.  The result depends on c. */
 774     if (N == 0) {
 775         if (c >= 0) return(one);
 776         else return(zero);
 777     }
 778
 779     /* The maximum or the minimum difference comparing to c can generate the terminal case */
 780     if ((1 << N) - 1 < c) return(zero);
 781     else if ((-(1 << N) + 1) >= c) return(one);
 782
 783     /* Build the result bottom up. */
 784     for (i = 1; i <= N; i++) {
 785         int kTrueLower, kFalseLower;
 786         int leftChild, middleChild, rightChild;
 787         DdNode *g0, *g1, *fplus, *fequal, *fminus;
 788         int j;
 789         DdNode *newMap[2];
 790         int newIndex[2];
 791
 792         kTrueLower = kTrue;
 793         kFalseLower = kFalse;
 794         /* kTrue = ceiling((c-1)/2^i) + 1 */
 795         kTrue = ((c-1) >> i) + ((c & mask) != 1) + 1;
 796         mask = (mask << 1) | 1;
 797         /* kFalse = floor(c/2^i) - 1 */
 798         kFalse = (c >> i) - 1;
 799         newIndex[0] = invalidIndex;
 800         newIndex[1] = invalidIndex;
 801
 802         for (j = kFalse + 1; j < kTrue; j++) {
 803             /* Skip if node is not reachable from top of BDD. */
 804             if ((j >= (1 << (N - i))) || (j <= -(1 << (N -i)))) continue;
 805
 806             /* Find f- */
 807             leftChild = (j << 1) - 1;
 808             if (leftChild >= kTrueLower) {
 809                 fminus = one;
 810             } else if (leftChild <= kFalseLower) {
 811                 fminus = zero;
 812             } else {
 813                 assert(leftChild == index[0] || leftChild == index[1]);
 814                 if (leftChild == index[0]) {
 815                     fminus = map[0];
 816                 } else {
 817                     fminus = map[1];
 818                 }
 819             }
 820
 821             /* Find f= */
 822             middleChild = j << 1;
 823             if (middleChild >= kTrueLower) {
 824                 fequal = one;
 825             } else if (middleChild <= kFalseLower) {
 826                 fequal = zero;
 827             } else {
 828                 assert(middleChild == index[0] || middleChild == index[1]);
 829                 if (middleChild == index[0]) {
 830                     fequal = map[0];
 831                 } else {
 832                     fequal = map[1];
 833                 }
 834             }
 835
 836             /* Find f+ */
 837             rightChild = (j << 1) + 1;
 838             if (rightChild >= kTrueLower) {
 839                 fplus = one;
 840             } else if (rightChild <= kFalseLower) {
 841                 fplus = zero;
 842             } else {
 843                 assert(rightChild == index[0] || rightChild == index[1]);
 844                 if (rightChild == index[0]) {
 845                     fplus = map[0];
 846                 } else {
 847                     fplus = map[1];
 848                 }
 849             }
 850
 851             /* Build new nodes. */
 852             g1 = Cudd_bddIte(dd, y[N - i], fequal, fplus);
 853             if (g1 == NULL) {
 854                 if (index[0] != invalidIndex) Cudd_IterDerefBdd(dd, map[0]);
 855                 if (index[1] != invalidIndex) Cudd_IterDerefBdd(dd, map[1]);
 856                 if (newIndex[0] != invalidIndex) Cudd_IterDerefBdd(dd, newMap[0]);
 857                 if (newIndex[1] != invalidIndex) Cudd_IterDerefBdd(dd, newMap[1]);
 858                 return(NULL);
 859             }
 860             cuddRef(g1);
 861             g0 = Cudd_bddIte(dd, y[N - i], fminus, fequal);
 862             if (g0 == NULL) {
 863                 Cudd_IterDerefBdd(dd, g1);
 864                 if (index[0] != invalidIndex) Cudd_IterDerefBdd(dd, map[0]);
 865                 if (index[1] != invalidIndex) Cudd_IterDerefBdd(dd, map[1]);
 866                 if (newIndex[0] != invalidIndex) Cudd_IterDerefBdd(dd, newMap[0]);
 867                 if (newIndex[1] != invalidIndex) Cudd_IterDerefBdd(dd, newMap[1]);
 868                 return(NULL);
 869             }
 870             cuddRef(g0);
 871             f = Cudd_bddIte(dd, x[N - i], g1, g0);
 872             if (f == NULL) {
 873                 Cudd_IterDerefBdd(dd, g1);
 874                 Cudd_IterDerefBdd(dd, g0);
 875                 if (index[0] != invalidIndex) Cudd_IterDerefBdd(dd, map[0]);
 876                 if (index[1] != invalidIndex) Cudd_IterDerefBdd(dd, map[1]);
 877                 if (newIndex[0] != invalidIndex) Cudd_IterDerefBdd(dd, newMap[0]);
 878                 if (newIndex[1] != invalidIndex) Cudd_IterDerefBdd(dd, newMap[1]);
 879                 return(NULL);
 880             }
 881             cuddRef(f);
 882             Cudd_IterDerefBdd(dd, g1);
 883             Cudd_IterDerefBdd(dd, g0);
 884
 885             /* Save newly computed node in map. */
 886             assert(newIndex[0] == invalidIndex || newIndex[1] == invalidIndex);
 887             if (newIndex[0] == invalidIndex) {
 888                 newIndex[0] = j;
 889                 newMap[0] = f;
 890             } else {
 891                 newIndex[1] = j;
 892                 newMap[1] = f;
 893             }
 894         }
 895
 896         /* Copy new map to map. */
 897         if (index[0] != invalidIndex) Cudd_IterDerefBdd(dd, map[0]);
 898         if (index[1] != invalidIndex) Cudd_IterDerefBdd(dd, map[1]);
 899         map[0] = newMap[0];
 900         map[1] = newMap[1];
 901         index[0] = newIndex[0];
 902         index[1] = newIndex[1];
 903     }
 904
 905     cuddDeref(f);
 906     return(f);
 907
 908 } /* end of Cudd_Inequality */
 909
 910
 911 /**Function********************************************************************
 912
 913   Synopsis    [Generates a BDD for the function x - y != c.]
 914
 915   Description [This function generates a BDD for the function x -y != c.
 916   Both x and y are N-bit numbers, x\[0\] x\[1\] ... x\[N-1\] and
 917   y\[0\] y\[1\] ...  y\[N-1\], with 0 the most significant bit.
 918   The BDD is built bottom-up.
 919   It has a linear number of nodes if the variables are ordered as follows:
 920   x\[0\] y\[0\] x\[1\] y\[1\] ... x\[N-1\] y\[N-1\].]
 921
 922   SideEffects [None]
 923
 924   SeeAlso     [Cudd_Xgty]
 925
 926 ******************************************************************************/
 927 DdNode *
 928 Cudd_Disequality(
 929   DdManager * dd /* DD manager */,
 930   int  N /* number of x and y variables */,
 931   int c /* right-hand side constant */,
 932   DdNode ** x /* array of x variables */,
 933   DdNode ** y /* array of y variables */)
 934 {
 935     /* The nodes at level i represent values of the difference that are
 936     ** multiples of 2^i.  We use variables with names starting with k
 937     ** to denote the multipliers of 2^i in such multiples. */
 938     int kTrueLb = c + 1;
 939     int kTrueUb = c - 1;
 940     int kFalse = c;
 941     /* Mask used to compute the ceiling function.  Since we divide by 2^i,
 942     ** we want to know whether the dividend is a multiple of 2^i.  If it is,
 943     ** then ceiling and floor coincide; otherwise, they differ by one. */
 944     int mask = 1;
 945     int i;
 946
 947     DdNode *f = NULL;           /* the eventual result */
 948     DdNode *one = DD_ONE(dd);
 949     DdNode *zero = Cudd_Not(one);
 950
 951     /* Two x-labeled nodes are created at most at each iteration.  They are
 952     ** stored, along with their k values, in these variables.  At each level,
 953     ** the old nodes are freed and the new nodes are copied into the old map.
 954     */
 955     DdNode *map[2];
 956     int invalidIndex = 1 << (N-1);
 957     int index[2] = {invalidIndex, invalidIndex};
 958
 959     /* This should never happen. */
 960     if (N < 0) return(NULL);
 961
 962     /* If there are no bits, both operands are 0.  The result depends on c. */
 963     if (N == 0) {
 964         if (c != 0) return(one);
 965         else return(zero);
 966     }
 967
 968     /* The maximum or the minimum difference comparing to c can generate the terminal case */
 969     if ((1 << N) - 1 < c || (-(1 << N) + 1) > c) return(one);
 970
 971     /* Build the result bottom up. */
 972     for (i = 1; i <= N; i++) {
 973         int kTrueLbLower, kTrueUbLower;
 974         int leftChild, middleChild, rightChild;
 975         DdNode *g0, *g1, *fplus, *fequal, *fminus;
 976         int j;
 977         DdNode *newMap[2];
 978         int newIndex[2];
 979
 980         kTrueLbLower = kTrueLb;
 981         kTrueUbLower = kTrueUb;
 982         /* kTrueLb = floor((c-1)/2^i) + 2 */
 983         kTrueLb = ((c-1) >> i) + 2;
 984         /* kTrueUb = ceiling((c+1)/2^i) - 2 */
 985         kTrueUb = ((c+1) >> i) + (((c+2) & mask) != 1) - 2;
 986         mask = (mask << 1) | 1;
 987         newIndex[0] = invalidIndex;
 988         newIndex[1] = invalidIndex;
 989
 990         for (j = kTrueUb + 1; j < kTrueLb; j++) {
 991             /* Skip if node is not reachable from top of BDD. */
 992             if ((j >= (1 << (N - i))) || (j <= -(1 << (N -i)))) continue;
 993
 994             /* Find f- */
 995             leftChild = (j << 1) - 1;
 996             if (leftChild >= kTrueLbLower || leftChild <= kTrueUbLower) {
 997                 fminus = one;
 998             } else if (i == 1 && leftChild == kFalse) {
 999                 fminus = zero;
1000             } else {
1001                 assert(leftChild == index[0] || leftChild == index[1]);
1002                 if (leftChild == index[0]) {
1003                     fminus = map[0];
1004                 } else {
1005                     fminus = map[1];
1006                 }
1007             }
1008
1009             /* Find f= */
1010             middleChild = j << 1;
1011             if (middleChild >= kTrueLbLower || middleChild <= kTrueUbLower) {
1012                 fequal = one;
1013             } else if (i == 1 && middleChild == kFalse) {
1014                 fequal = zero;
1015             } else {
1016                 assert(middleChild == index[0] || middleChild == index[1]);
1017                 if (middleChild == index[0]) {
1018                     fequal = map[0];
1019                 } else {
1020                     fequal = map[1];
1021                 }
1022             }
1023
1024             /* Find f+ */
1025             rightChild = (j << 1) + 1;
1026             if (rightChild >= kTrueLbLower || rightChild <= kTrueUbLower) {
1027                 fplus = one;
1028             } else if (i == 1 && rightChild == kFalse) {
1029                 fplus = zero;
1030             } else {
1031                 assert(rightChild == index[0] || rightChild == index[1]);
1032                 if (rightChild == index[0]) {
1033                     fplus = map[0];
1034                 } else {
1035                     fplus = map[1];
1036                 }
1037             }
1038
1039             /* Build new nodes. */
1040             g1 = Cudd_bddIte(dd, y[N - i], fequal, fplus);
1041             if (g1 == NULL) {
1042                 if (index[0] != invalidIndex) Cudd_IterDerefBdd(dd, map[0]);
1043                 if (index[1] != invalidIndex) Cudd_IterDerefBdd(dd, map[1]);
1044                 if (newIndex[0] != invalidIndex) Cudd_IterDerefBdd(dd, newMap[0]);
1045                 if (newIndex[1] != invalidIndex) Cudd_IterDerefBdd(dd, newMap[1]);
1046                 return(NULL);
1047             }
1048             cuddRef(g1);
1049             g0 = Cudd_bddIte(dd, y[N - i], fminus, fequal);
1050             if (g0 == NULL) {
1051                 Cudd_IterDerefBdd(dd, g1);
1052                 if (index[0] != invalidIndex) Cudd_IterDerefBdd(dd, map[0]);
1053                 if (index[1] != invalidIndex) Cudd_IterDerefBdd(dd, map[1]);
1054                 if (newIndex[0] != invalidIndex) Cudd_IterDerefBdd(dd, newMap[0]);
1055                 if (newIndex[1] != invalidIndex) Cudd_IterDerefBdd(dd, newMap[1]);
1056                 return(NULL);
1057             }
1058             cuddRef(g0);
1059             f = Cudd_bddIte(dd, x[N - i], g1, g0);
1060             if (f == NULL) {
1061                 Cudd_IterDerefBdd(dd, g1);
1062                 Cudd_IterDerefBdd(dd, g0);
1063                 if (index[0] != invalidIndex) Cudd_IterDerefBdd(dd, map[0]);
1064                 if (index[1] != invalidIndex) Cudd_IterDerefBdd(dd, map[1]);
1065                 if (newIndex[0] != invalidIndex) Cudd_IterDerefBdd(dd, newMap[0]);
1066                 if (newIndex[1] != invalidIndex) Cudd_IterDerefBdd(dd, newMap[1]);
1067                 return(NULL);
1068             }
1069             cuddRef(f);
1070             Cudd_IterDerefBdd(dd, g1);
1071             Cudd_IterDerefBdd(dd, g0);
1072
1073             /* Save newly computed node in map. */
1074             assert(newIndex[0] == invalidIndex || newIndex[1] == invalidIndex);
1075             if (newIndex[0] == invalidIndex) {
1076                 newIndex[0] = j;
1077                 newMap[0] = f;
1078             } else {
1079                 newIndex[1] = j;
1080                 newMap[1] = f;
1081             }
1082         }
1083
1084         /* Copy new map to map. */
1085         if (index[0] != invalidIndex) Cudd_IterDerefBdd(dd, map[0]);
1086         if (index[1] != invalidIndex) Cudd_IterDerefBdd(dd, map[1]);
1087         map[0] = newMap[0];
1088         map[1] = newMap[1];
1089         index[0] = newIndex[0];
1090         index[1] = newIndex[1];
1091     }
1092
1093     cuddDeref(f);
1094     return(f);
1095
1096 } /* end of Cudd_Disequality */
1097
1098
1099 /**Function********************************************************************
1100
1101   Synopsis    [Generates a BDD for the function lowerB &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 ******************************************************************************/
1116 DdNode *
1117 Cudd_bddInterval(
1118   DdManager * dd /* DD manager */,
1119   int  N /* number of x variables */,
1120   DdNode ** x /* array of x variables */,
1121   unsigned int lowerB /* lower bound */,
1122   unsigned int upperB /* upper bound */)
1123 {
1124     DdNode *one, *zero;
1125     DdNode *r, *rl, *ru;
1126     int     i;
1127
1128     one = DD_ONE(dd);
1129     zero = Cudd_Not(one);
1130
1131     rl = one;
1132     cuddRef(rl);
1133     ru = one;
1134     cuddRef(ru);
1135
1136     /* Loop to build the rest of the BDDs. */
1137     for (i = N-1; i >= 0; i--) {
1138         DdNode *vl, *vu;
1139         vl = Cudd_bddIte(dd, x[i],
1140                          lowerB&1 ? rl : one,
1141                          lowerB&1 ? zero : rl);
1142         if (vl == NULL) {
1143             Cudd_IterDerefBdd(dd, rl);
1144             Cudd_IterDerefBdd(dd, ru);
1145             return(NULL);
1146         }
1147         cuddRef(vl);
1148         Cudd_IterDerefBdd(dd, rl);
1149         rl = vl;
1150         lowerB >>= 1;
1151         vu = Cudd_bddIte(dd, x[i],
1152                          upperB&1 ? ru : zero,
1153                          upperB&1 ? one : ru);
1154         if (vu == NULL) {
1155             Cudd_IterDerefBdd(dd, rl);
1156             Cudd_IterDerefBdd(dd, ru);
1157             return(NULL);
1158         }
1159         cuddRef(vu);
1160         Cudd_IterDerefBdd(dd, ru);
1161         ru = vu;
1162         upperB >>= 1;
1163     }
1164
1165     /* Conjoin the two bounds. */
1166     r = Cudd_bddAnd(dd, rl, ru);
1167     if (r == NULL) {
1168         Cudd_IterDerefBdd(dd, rl);
1169         Cudd_IterDerefBdd(dd, ru);
1170         return(NULL);
1171     }
1172     cuddRef(r);
1173     Cudd_IterDerefBdd(dd, rl);
1174     Cudd_IterDerefBdd(dd, ru);
1175     cuddDeref(r);
1176     return(r);
1177
1178 } /* end of Cudd_bddInterval */
1179
1180
1181 /**Function********************************************************************
1182
1183   Synopsis    [Computes the compatible projection of R w.r.t. cube Y.]
1184
1185   Description [Computes the compatible projection of relation R with
1186   respect to cube Y. Returns a pointer to the c-projection if
1187   successful; NULL otherwise. For a comparison between Cudd_CProjection
1188   and Cudd_PrioritySelect, see the documentation of the latter.]
1189
1190   SideEffects [None]
1191
1192   SeeAlso     [Cudd_PrioritySelect]
1193
1194 ******************************************************************************/
1195 DdNode *
1196 Cudd_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 ******************************************************************************/
1250 DdNode *
1251 Cudd_addHamming(
1252   DdManager * dd,
1253   DdNode ** xVars,
1254   DdNode ** yVars,
1255   int  nVars)
1256 {
1257     DdNode  *result,*tempBdd;
1258     DdNode  *tempAdd,*temp;
1259     int     i;
1260
1261     result = DD_ZERO(dd);
1262     cuddRef(result);
1263
1264     for (i = 0; i < nVars; i++) {
1265         tempBdd = Cudd_bddIte(dd,xVars[i],Cudd_Not(yVars[i]),yVars[i]);
1266         if (tempBdd == NULL) {
1267             Cudd_RecursiveDeref(dd,result);
1268             return(NULL);
1269         }
1270         cuddRef(tempBdd);
1271         tempAdd = Cudd_BddToAdd(dd,tempBdd);
1272         if (tempAdd == NULL) {
1273             Cudd_RecursiveDeref(dd,tempBdd);
1274             Cudd_RecursiveDeref(dd,result);
1275             return(NULL);
1276         }
1277         cuddRef(tempAdd);
1278         Cudd_RecursiveDeref(dd,tempBdd);
1279         temp = Cudd_addApply(dd,Cudd_addPlus,tempAdd,result);
1280         if (temp == NULL) {
1281             Cudd_RecursiveDeref(dd,tempAdd);
1282             Cudd_RecursiveDeref(dd,result);
1283             return(NULL);
1284         }
1285         cuddRef(temp);
1286         Cudd_RecursiveDeref(dd,tempAdd);
1287         Cudd_RecursiveDeref(dd,result);
1288         result = temp;
1289     }
1290
1291     cuddDeref(result);
1292     return(result);
1293
1294 } /* end of Cudd_addHamming */
1295
1296
1297 /**Function********************************************************************
1298
1299   Synopsis    [Returns the minimum Hamming distance between f and minterm.]
1300
1301   Description [Returns the minimum Hamming distance between the
1302   minterms of a function f and a reference minterm. The function is
1303   given as a BDD; the minterm is given as an array of integers, one
1304   for each variable in the manager.  Returns the minimum distance if
1305   it is less than the upper bound; the upper bound if the minimum
1306   distance is at least as large; CUDD_OUT_OF_MEM in case of failure.]
1307
1308   SideEffects [None]
1309
1310   SeeAlso     [Cudd_addHamming Cudd_bddClosestCube]
1311
1312 ******************************************************************************/
1313 int
1314 Cudd_MinHammingDist(
1315   DdManager *dd /* DD manager */,
1316   DdNode *f /* function to examine */,
1317   int *minterm /* reference minterm */,
1318   int upperBound /* distance above which an approximate answer is OK */)
1319 {
1320     DdHashTable *table;
1321     CUDD_VALUE_TYPE epsilon;
1322     int res;
1323
1324     table = cuddHashTableInit(dd,1,2);
1325     if (table == NULL) {
1326         return(CUDD_OUT_OF_MEM);
1327     }
1328     epsilon = Cudd_ReadEpsilon(dd);
1329     Cudd_SetEpsilon(dd,(CUDD_VALUE_TYPE)0.0);
1330     res = cuddMinHammingDistRecur(f,minterm,table,upperBound);
1331     cuddHashTableQuit(table);
1332     Cudd_SetEpsilon(dd,epsilon);
1333
1334     return(res);
1335
1336 } /* end of Cudd_MinHammingDist */
1337
1338
1339 /**Function********************************************************************
1340
1341   Synopsis    [Finds a cube of f at minimum Hamming distance from g.]
1342
1343   Description [Finds a cube of f at minimum Hamming distance from the
1344   minterms of g.  All the minterms of the cube are at the minimum
1345   distance.  If the distance is 0, the cube belongs to the
1346   intersection of f and g.  Returns the cube if successful; NULL
1347   otherwise.]
1348
1349   SideEffects [The distance is returned as a side effect.]
1350
1351   SeeAlso     [Cudd_MinHammingDist]
1352
1353 ******************************************************************************/
1354 DdNode *
1355 Cudd_bddClosestCube(
1356   DdManager *dd,
1357   DdNode * f,
1358   DdNode *g,
1359   int *distance)
1360 {
1361     DdNode *res, *acube;
1362     CUDD_VALUE_TYPE rdist;
1363
1364     /* Compute the cube and distance as a single ADD. */
1365     do {
1366         dd->reordered = 0;
1367         res = cuddBddClosestCube(dd,f,g,CUDD_CONST_INDEX + 1.0);
1368     } while (dd->reordered == 1);
1369     if (res == NULL) return(NULL);
1370     cuddRef(res);
1371
1372     /* Unpack distance and cube. */
1373     do {
1374         dd->reordered = 0;
1375         acube = separateCube(dd, res, &rdist);
1376     } while (dd->reordered == 1);
1377     if (acube == NULL) {
1378         Cudd_RecursiveDeref(dd, res);
1379         return(NULL);
1380     }
1381     cuddRef(acube);
1382     Cudd_RecursiveDeref(dd, res);
1383
1384     /* Convert cube from ADD to BDD. */
1385     do {
1386         dd->reordered = 0;
1387         res = cuddAddBddDoPattern(dd, acube);
1388     } while (dd->reordered == 1);
1389     if (res == NULL) {
1390         Cudd_RecursiveDeref(dd, acube);
1391         return(NULL);
1392     }
1393     cuddRef(res);
1394     Cudd_RecursiveDeref(dd, acube);
1395
1396     *distance = (int) rdist;
1397     cuddDeref(res);
1398     return(res);
1399
1400 } /* end of Cudd_bddClosestCube */
1401
1402
1403 /*---------------------------------------------------------------------------*/
1404 /* Definition of internal functions                                          */
1405 /*---------------------------------------------------------------------------*/
1406
1407
1408 /**Function********************************************************************
1409
1410   Synopsis    [Performs the recursive step of Cudd_CProjection.]
1411
1412   Description [Performs the recursive step of Cudd_CProjection. Returns
1413   the projection if successful; NULL otherwise.]
1414
1415   SideEffects [None]
1416
1417   SeeAlso     [Cudd_CProjection]
1418
1419 ******************************************************************************/
1420 DdNode *
1421 cuddCProjectionRecur(
1422   DdManager * dd,
1423   DdNode * R,
1424   DdNode * Y,
1425   DdNode * Ysupp)
1426 {
1427     DdNode *res, *res1, *res2, *resA;
1428     DdNode *r, *y, *RT, *RE, *YT, *YE, *Yrest, *Ra, *Ran, *Gamma, *Alpha;
1429     unsigned int topR, topY, top, index;
1430     DdNode *one = DD_ONE(dd);
1431
1432     statLine(dd);
1433     if (Y == one) return(R);
1434
1435 #ifdef DD_DEBUG
1436     assert(!Cudd_IsConstant(Y));
1437 #endif
1438
1439     if (R == Cudd_Not(one)) return(R);
1440
1441     res = cuddCacheLookup2(dd, Cudd_CProjection, R, Y);
1442     if (res != NULL) return(res);
1443
1444     r = Cudd_Regular(R);
1445     topR = cuddI(dd,r->index);
1446     y = Cudd_Regular(Y);
1447     topY = cuddI(dd,y->index);
1448
1449     top = ddMin(topR, topY);
1450
1451     /* Compute the cofactors of R */
1452     if (topR == top) {
1453         index = r->index;
1454         RT = cuddT(r);
1455         RE = cuddE(r);
1456         if (r != R) {
1457             RT = Cudd_Not(RT); RE = Cudd_Not(RE);
1458         }
1459     } else {
1460         RT = RE = R;
1461     }
1462
1463     if (topY > top) {
1464         /* Y does not depend on the current top variable.
1465         ** We just need to compute the results on the two cofactors of R
1466         ** and make them the children of a node labeled r->index.
1467         */
1468         res1 = cuddCProjectionRecur(dd,RT,Y,Ysupp);
1469         if (res1 == NULL) return(NULL);
1470         cuddRef(res1);
1471         res2 = cuddCProjectionRecur(dd,RE,Y,Ysupp);
1472         if (res2 == NULL) {
1473             Cudd_RecursiveDeref(dd,res1);
1474             return(NULL);
1475         }
1476         cuddRef(res2);
1477         res = cuddBddIteRecur(dd, dd->vars[index], res1, res2);
1478         if (res == NULL) {
1479             Cudd_RecursiveDeref(dd,res1);
1480             Cudd_RecursiveDeref(dd,res2);
1481             return(NULL);
1482         }
1483         /* If we have reached this point, res1 and res2 are now
1484         ** incorporated in res. cuddDeref is therefore sufficient.
1485         */
1486         cuddDeref(res1);
1487         cuddDeref(res2);
1488     } else {
1489         /* Compute the cofactors of Y */
1490         index = y->index;
1491         YT = cuddT(y);
1492         YE = cuddE(y);
1493         if (y != Y) {
1494             YT = Cudd_Not(YT); YE = Cudd_Not(YE);
1495         }
1496         if (YT == Cudd_Not(one)) {
1497             Alpha  = Cudd_Not(dd->vars[index]);
1498             Yrest = YE;
1499             Ra = RE;
1500             Ran = RT;
1501         } else {
1502             Alpha = dd->vars[index];
1503             Yrest = YT;
1504             Ra = RT;
1505             Ran = RE;
1506         }
1507         Gamma = cuddBddExistAbstractRecur(dd,Ra,cuddT(Ysupp));
1508         if (Gamma == NULL) return(NULL);
1509         if (Gamma == one) {
1510             res1 = cuddCProjectionRecur(dd,Ra,Yrest,cuddT(Ysupp));
1511             if (res1 == NULL) return(NULL);
1512             cuddRef(res1);
1513             res = cuddBddAndRecur(dd, Alpha, res1);
1514             if (res == NULL) {
1515                 Cudd_RecursiveDeref(dd,res1);
1516                 return(NULL);
1517             }
1518             cuddDeref(res1);
1519         } else if (Gamma == Cudd_Not(one)) {
1520             res1 = cuddCProjectionRecur(dd,Ran,Yrest,cuddT(Ysupp));
1521             if (res1 == NULL) return(NULL);
1522             cuddRef(res1);
1523             res = cuddBddAndRecur(dd, Cudd_Not(Alpha), res1);
1524             if (res == NULL) {
1525                 Cudd_RecursiveDeref(dd,res1);
1526                 return(NULL);
1527             }
1528             cuddDeref(res1);
1529         } else {
1530             cuddRef(Gamma);
1531             resA = cuddCProjectionRecur(dd,Ran,Yrest,cuddT(Ysupp));
1532             if (resA == NULL) {
1533                 Cudd_RecursiveDeref(dd,Gamma);
1534                 return(NULL);
1535             }
1536             cuddRef(resA);
1537             res2 = cuddBddAndRecur(dd, Cudd_Not(Gamma), resA);
1538             if (res2 == NULL) {
1539                 Cudd_RecursiveDeref(dd,Gamma);
1540                 Cudd_RecursiveDeref(dd,resA);
1541                 return(NULL);
1542             }
1543             cuddRef(res2);
1544             Cudd_RecursiveDeref(dd,Gamma);
1545             Cudd_RecursiveDeref(dd,resA);
1546             res1 = cuddCProjectionRecur(dd,Ra,Yrest,cuddT(Ysupp));
1547             if (res1 == NULL) {
1548                 Cudd_RecursiveDeref(dd,res2);
1549                 return(NULL);
1550             }
1551             cuddRef(res1);
1552             res = cuddBddIteRecur(dd, Alpha, res1, res2);
1553             if (res == NULL) {
1554                 Cudd_RecursiveDeref(dd,res1);
1555                 Cudd_RecursiveDeref(dd,res2);
1556                 return(NULL);
1557             }
1558             cuddDeref(res1);
1559             cuddDeref(res2);
1560         }
1561     }
1562
1563     cuddCacheInsert2(dd,Cudd_CProjection,R,Y,res);
1564
1565     return(res);
1566
1567 } /* end of cuddCProjectionRecur */
1568
1569
1570 /**Function********************************************************************
1571
1572   Synopsis    [Performs the recursive step of Cudd_bddClosestCube.]
1573
1574   Description [Performs the recursive step of Cudd_bddClosestCube.
1575   Returns the cube if succesful; NULL otherwise.  The procedure uses a
1576   four-way recursion to examine all four combinations of cofactors of
1577   <code>f</code> and <code>g</code> according to the following formula.
1578   <pre>
1579     H(f,g) = min(H(ft,gt), H(fe,ge), H(ft,ge)+1, H(fe,gt)+1)
1580   </pre>
1581   Bounding is based on the following observations.
1582   <ul>
1583   <li> If we already found two points at distance 0, there is no point in
1584        continuing.  Furthermore,
1585   <li> If F == not(G) then the best we can hope for is a minimum distance
1586        of 1.  If we have already found two points at distance 1, there is
1587        no point in continuing.  (Indeed, H(F,G) == 1 in this case.  We
1588        have to continue, though, to find the cube.)
1589   </ul>
1590   The variable <code>bound</code> is set at the largest value of the distance
1591   that we are still interested in.  Therefore, we desist when
1592   <pre>
1593     (bound == -1) and (F != not(G)) or (bound == 0) and (F == not(G)).
1594   </pre>
1595   If we were maximally aggressive in using the bound, we would always
1596   set the bound to the minimum distance seen thus far minus one.  That
1597   is, we would maintain the invariant
1598   <pre>
1599     bound < minD,
1600   </pre>
1601   except at the very beginning, when we have no value for
1602   <code>minD</code>.<p>
1603
1604   However, we do not use <code>bound < minD</code> when examining the
1605   two negative cofactors, because we try to find a large cube at
1606   minimum distance.  To do so, we try to find a cube in the negative
1607   cofactors at the same or smaller distance from the cube found in the
1608   positive cofactors.<p>
1609
1610   When we compute <code>H(ft,ge)</code> and <code>H(fe,gt)</code> we
1611   know that we are going to add 1 to the result of the recursive call
1612   to account for the difference in the splitting variable.  Therefore,
1613   we decrease the bound correspondingly.<p>
1614
1615   Another important observation concerns the need of examining all
1616   four pairs of cofators only when both <code>f</code> and
1617   <code>g</code> depend on the top variable.<p>
1618
1619   Suppose <code>gt == ge == g</code>.  (That is, <code>g</code> does
1620   not depend on the top variable.)  Then
1621   <pre>
1622     H(f,g) = min(H(ft,g), H(fe,g), H(ft,g)+1, H(fe,g)+1)
1623            = min(H(ft,g), H(fe,g)) .
1624   </pre>
1625   Therefore, under these circumstances, we skip the two "cross" cases.<p>
1626
1627   An interesting feature of this function is the scheme used for
1628   caching the results in the global computed table.  Since we have a
1629   cube and a distance, we combine them to form an ADD.  The
1630   combination replaces the zero child of the top node of the cube with
1631   the negative of the distance.  (The use of the negative is to avoid
1632   ambiguity with 1.)  The degenerate cases (zero and one) are treated
1633   specially because the distance is known (0 for one, and infinity for
1634   zero).]
1635
1636   SideEffects [None]
1637
1638   SeeAlso     [Cudd_bddClosestCube]
1639
1640 ******************************************************************************/
1641 DdNode *
1642 cuddBddClosestCube(
1643   DdManager *dd,
1644   DdNode *f,
1645   DdNode *g,
1646   CUDD_VALUE_TYPE bound)
1647 {
1648     DdNode *res, *F, *G, *ft, *fe, *gt, *ge, *tt, *ee;
1649     DdNode *ctt, *cee, *cte, *cet;
1650     CUDD_VALUE_TYPE minD, dtt, dee, dte, det;
1651     DdNode *one = DD_ONE(dd);
1652     DdNode *lzero = Cudd_Not(one);
1653     DdNode *azero = DD_ZERO(dd);
1654     unsigned int topf, topg, index;
1655
1656     statLine(dd);
1657     if (bound < (f == Cudd_Not(g))) return(azero);
1658     /* Terminal cases. */
1659     if (g == lzero || f == lzero) return(azero);
1660     if (f == one && g == one) return(one);
1661
1662     /* Check cache. */
1663     F = Cudd_Regular(f);
1664     G = Cudd_Regular(g);
1665     if (F->ref != 1 || G->ref != 1) {
1666         res = cuddCacheLookup2(dd,(DD_CTFP) Cudd_bddClosestCube, f, g);
1667         if (res != NULL) return(res);
1668     }
1669
1670     topf = cuddI(dd,F->index);
1671     topg = cuddI(dd,G->index);
1672
1673     /* Compute cofactors. */
1674     if (topf <= topg) {
1675         index = F->index;
1676         ft = cuddT(F);
1677         fe = cuddE(F);
1678         if (Cudd_IsComplement(f)) {
1679             ft = Cudd_Not(ft);
1680             fe = Cudd_Not(fe);
1681         }
1682     } else {
1683         index = G->index;
1684         ft = fe = f;
1685     }
1686
1687     if (topg <= topf) {
1688         gt = cuddT(G);
1689         ge = cuddE(G);
1690         if (Cudd_IsComplement(g)) {
1691             gt = Cudd_Not(gt);
1692             ge = Cudd_Not(ge);
1693         }
1694     } else {
1695         gt = ge = g;
1696     }
1697
1698     tt = cuddBddClosestCube(dd,ft,gt,bound);
1699     if (tt == NULL) return(NULL);
1700     cuddRef(tt);
1701     ctt = separateCube(dd,tt,&dtt);
1702     if (ctt == NULL) {
1703         Cudd_RecursiveDeref(dd, tt);
1704         return(NULL);
1705     }
1706     cuddRef(ctt);
1707     Cudd_RecursiveDeref(dd, tt);
1708     minD = dtt;
1709     bound = ddMin(bound,minD);
1710
1711     ee = cuddBddClosestCube(dd,fe,ge,bound);
1712     if (ee == NULL) {
1713         Cudd_RecursiveDeref(dd, ctt);
1714         return(NULL);
1715     }
1716     cuddRef(ee);
1717     cee = separateCube(dd,ee,&dee);
1718     if (cee == NULL) {
1719         Cudd_RecursiveDeref(dd, ctt);
1720         Cudd_RecursiveDeref(dd, ee);
1721         return(NULL);
1722     }
1723     cuddRef(cee);
1724     Cudd_RecursiveDeref(dd, ee);
1725     minD = ddMin(dtt, dee);
1726     if (minD <= CUDD_CONST_INDEX) bound = ddMin(bound,minD-1);
1727
1728     if (minD > 0 && topf == topg) {
1729         DdNode *te = cuddBddClosestCube(dd,ft,ge,bound-1);
1730         if (te == NULL) {
1731             Cudd_RecursiveDeref(dd, ctt);
1732             Cudd_RecursiveDeref(dd, cee);
1733             return(NULL);
1734         }
1735         cuddRef(te);
1736         cte = separateCube(dd,te,&dte);
1737         if (cte == NULL) {
1738             Cudd_RecursiveDeref(dd, ctt);
1739             Cudd_RecursiveDeref(dd, cee);
1740             Cudd_RecursiveDeref(dd, te);
1741             return(NULL);
1742         }
1743         cuddRef(cte);
1744         Cudd_RecursiveDeref(dd, te);
1745         dte += 1.0;
1746         minD = ddMin(minD, dte);
1747     } else {
1748         cte = azero;
1749         cuddRef(cte);
1750         dte = CUDD_CONST_INDEX + 1.0;
1751     }
1752     if (minD <= CUDD_CONST_INDEX) bound = ddMin(bound,minD-1);
1753
1754     if (minD > 0 && topf == topg) {
1755         DdNode *et = cuddBddClosestCube(dd,fe,gt,bound-1);
1756         if (et == NULL) {
1757             Cudd_RecursiveDeref(dd, ctt);
1758             Cudd_RecursiveDeref(dd, cee);
1759             Cudd_RecursiveDeref(dd, cte);
1760             return(NULL);
1761         }
1762         cuddRef(et);
1763         cet = separateCube(dd,et,&det);
1764         if (cet == NULL) {
1765             Cudd_RecursiveDeref(dd, ctt);
1766             Cudd_RecursiveDeref(dd, cee);
1767             Cudd_RecursiveDeref(dd, cte);
1768             Cudd_RecursiveDeref(dd, et);
1769             return(NULL);
1770         }
1771         cuddRef(cet);
1772         Cudd_RecursiveDeref(dd, et);
1773         det += 1.0;
1774         minD = ddMin(minD, det);
1775     } else {
1776         cet = azero;
1777         cuddRef(cet);
1778         det = CUDD_CONST_INDEX + 1.0;
1779     }
1780
1781     if (minD == dtt) {
1782         if (dtt == dee && ctt == cee) {
1783             res = createResult(dd,CUDD_CONST_INDEX,1,ctt,dtt);
1784         } else {
1785             res = createResult(dd,index,1,ctt,dtt);
1786         }
1787     } else if (minD == dee) {
1788         res = createResult(dd,index,0,cee,dee);
1789     } else if (minD == dte) {
1790 #ifdef DD_DEBUG
1791         assert(topf == topg);
1792 #endif
1793         res = createResult(dd,index,1,cte,dte);
1794     } else {
1795 #ifdef DD_DEBUG
1796         assert(topf == topg);
1797 #endif
1798         res = createResult(dd,index,0,cet,det);
1799     }
1800     if (res == NULL) {
1801         Cudd_RecursiveDeref(dd, ctt);
1802         Cudd_RecursiveDeref(dd, cee);
1803         Cudd_RecursiveDeref(dd, cte);
1804         Cudd_RecursiveDeref(dd, cet);
1805         return(NULL);
1806     }
1807     cuddRef(res);
1808     Cudd_RecursiveDeref(dd, ctt);
1809     Cudd_RecursiveDeref(dd, cee);
1810     Cudd_RecursiveDeref(dd, cte);
1811     Cudd_RecursiveDeref(dd, cet);
1812
1813     /* Only cache results that are different from azero to avoid
1814     ** storing results that depend on the value of the bound. */
1815     if ((F->ref != 1 || G->ref != 1) && res != azero)
1816         cuddCacheInsert2(dd,(DD_CTFP) Cudd_bddClosestCube, f, g, res);
1817
1818     cuddDeref(res);
1819     return(res);
1820
1821 } /* end of cuddBddClosestCube */
1822
1823
1824 /*---------------------------------------------------------------------------*/
1825 /* Definition of static functions                                            */
1826 /*---------------------------------------------------------------------------*/
1827
1828
1829 /**Function********************************************************************
1830
1831   Synopsis    [Performs the recursive step of Cudd_MinHammingDist.]
1832
1833   Description [Performs the recursive step of Cudd_MinHammingDist.
1834   It is based on the following identity. Let H(f) be the
1835   minimum Hamming distance of the minterms of f from the reference
1836   minterm. Then:
1837   <xmp>
1838     H(f) = min(H(f0)+h0,H(f1)+h1)
1839   </xmp>
1840   where f0 and f1 are the two cofactors of f with respect to its top
1841   variable; h0 is 1 if the minterm assigns 1 to the top variable of f;
1842   h1 is 1 if the minterm assigns 0 to the top variable of f.
1843   The upper bound on the distance is used to bound the depth of the
1844   recursion.
1845   Returns the minimum distance unless it exceeds the upper bound or
1846   computation fails.]
1847
1848   SideEffects [None]
1849
1850   SeeAlso     [Cudd_MinHammingDist]
1851
1852 ******************************************************************************/
1853 static int
1854 cuddMinHammingDistRecur(
1855   DdNode * f,
1856   int *minterm,
1857   DdHashTable * table,
1858   int upperBound)
1859 {
1860     DdNode      *F, *Ft, *Fe;
1861     double      h, hT, hE;
1862     DdNode      *zero, *res;
1863     DdManager   *dd = table->manager;
1864
1865     statLine(dd);
1866     if (upperBound == 0) return(0);
1867
1868     F = Cudd_Regular(f);
1869
1870     if (cuddIsConstant(F)) {
1871         zero = Cudd_Not(DD_ONE(dd));
1872         if (f == dd->background || f == zero) {
1873             return(upperBound);
1874         } else {
1875             return(0);
1876         }
1877     }
1878     if ((res = cuddHashTableLookup1(table,f)) != NULL) {
1879         h = cuddV(res);
1880         if (res->ref == 0) {
1881             dd->dead++;
1882             dd->constants.dead++;
1883         }
1884         return((int) h);
1885     }
1886
1887     Ft = cuddT(F); Fe = cuddE(F);
1888     if (Cudd_IsComplement(f)) {
1889         Ft = Cudd_Not(Ft); Fe = Cudd_Not(Fe);
1890     }
1891     if (minterm[F->index] == 0) {
1892         DdNode *temp = Ft;
1893         Ft = Fe; Fe = temp;
1894     }
1895
1896     hT = cuddMinHammingDistRecur(Ft,minterm,table,upperBound);
1897     if (hT == CUDD_OUT_OF_MEM) return(CUDD_OUT_OF_MEM);
1898     if (hT == 0) {
1899         hE = upperBound;
1900     } else {
1901         hE = cuddMinHammingDistRecur(Fe,minterm,table,upperBound - 1);
1902         if (hE == CUDD_OUT_OF_MEM) return(CUDD_OUT_OF_MEM);
1903     }
1904     h = ddMin(hT, hE + 1);
1905
1906     if (F->ref != 1) {
1907         ptrint fanout = (ptrint) F->ref;
1908         cuddSatDec(fanout);
1909         res = cuddUniqueConst(dd, (CUDD_VALUE_TYPE) h);
1910         if (!cuddHashTableInsert1(table,f,res,fanout)) {
1911             cuddRef(res); Cudd_RecursiveDeref(dd, res);
1912             return(CUDD_OUT_OF_MEM);
1913         }
1914     }
1915
1916     return((int) h);
1917
1918 } /* end of cuddMinHammingDistRecur */
1919
1920
1921 /**Function********************************************************************
1922
1923   Synopsis    [Separates cube from distance.]
1924
1925   Description [Separates cube from distance.  Returns the cube if
1926   successful; NULL otherwise.]
1927
1928   SideEffects [The distance is returned as a side effect.]
1929
1930   SeeAlso     [cuddBddClosestCube createResult]
1931
1932 ******************************************************************************/
1933 static DdNode *
1934 separateCube(
1935   DdManager *dd,
1936   DdNode *f,
1937   CUDD_VALUE_TYPE *distance)
1938 {
1939     DdNode *cube, *t;
1940
1941     /* One and zero are special cases because the distance is implied. */
1942     if (Cudd_IsConstant(f)) {
1943         *distance = (f == DD_ONE(dd)) ? 0.0 :
1944             (1.0 + (CUDD_VALUE_TYPE) CUDD_CONST_INDEX);
1945         return(f);
1946     }
1947
1948     /* Find out which branch points to the distance and replace the top
1949     ** node with one pointing to zero instead. */
1950     t = cuddT(f);
1951     if (Cudd_IsConstant(t) && cuddV(t) <= 0) {
1952 #ifdef DD_DEBUG
1953         assert(!Cudd_IsConstant(cuddE(f)) || cuddE(f) == DD_ONE(dd));
1954 #endif
1955         *distance = -cuddV(t);
1956         cube = cuddUniqueInter(dd, f->index, DD_ZERO(dd), cuddE(f));
1957     } else {
1958 #ifdef DD_DEBUG
1959         assert(!Cudd_IsConstant(t) || t == DD_ONE(dd));
1960 #endif
1961         *distance = -cuddV(cuddE(f));
1962         cube = cuddUniqueInter(dd, f->index, t, DD_ZERO(dd));
1963     }
1964
1965     return(cube);
1966
1967 } /* end of separateCube */
1968
1969
1970 /**Function********************************************************************
1971
1972   Synopsis    [Builds a result for cache storage.]
1973
1974   Description [Builds a result for cache storage.  Returns a pointer
1975   to the resulting ADD if successful; NULL otherwise.]
1976
1977   SideEffects [None]
1978
1979   SeeAlso     [cuddBddClosestCube separateCube]
1980
1981 ******************************************************************************/
1982 static DdNode *
1983 createResult(
1984   DdManager *dd,
1985   unsigned int index,
1986   unsigned int phase,
1987   DdNode *cube,
1988   CUDD_VALUE_TYPE distance)
1989 {
1990     DdNode *res, *constant;
1991
1992     /* Special case.  The cube is either one or zero, and we do not
1993     ** add any variables.  Hence, the result is also one or zero,
1994     ** and the distance remains implied by the value of the constant. */
1995     if (index == CUDD_CONST_INDEX && Cudd_IsConstant(cube)) return(cube);
1996
1997     constant = cuddUniqueConst(dd,-distance);
1998     if (constant == NULL) return(NULL);
1999     cuddRef(constant);
2000
2001     if (index == CUDD_CONST_INDEX) {
2002         /* Replace the top node. */
2003         if (cuddT(cube) == DD_ZERO(dd)) {
2004             res = cuddUniqueInter(dd,cube->index,constant,cuddE(cube));
2005         } else {
2006             res = cuddUniqueInter(dd,cube->index,cuddT(cube),constant);
2007         }
2008     } else {
2009         /* Add a new top node. */
2010 #ifdef DD_DEBUG
2011         assert(cuddI(dd,index) < cuddI(dd,cube->index));
2012 #endif
2013         if (phase) {
2014             res = cuddUniqueInter(dd,index,cube,constant);
2015         } else {
2016             res = cuddUniqueInter(dd,index,constant,cube);
2017         }
2018     }
2019     if (res == NULL) {
2020         Cudd_RecursiveDeref(dd, constant);
2021         return(NULL);
2022     }
2023     cuddDeref(constant); /* safe because constant is part of res */
2024
2025     return(res);
2026
2027 } /* end of createResult */