distr/cudd/cuddGenCof.c

   1 /**CFile***********************************************************************
   2
   3   FileName    [cuddGenCof.c]
   4
   5   PackageName [cudd]
   6
   7   Synopsis    [Generalized cofactors for BDDs and ADDs.]
   8
   9   Description [External procedures included in this module:
  10                 <ul>
  11                 <li> Cudd_bddConstrain()
  12                 <li> Cudd_bddRestrict()
  13                 <li> Cudd_bddNPAnd()
  14                 <li> Cudd_addConstrain()
  15                 <li> Cudd_bddConstrainDecomp()
  16                 <li> Cudd_addRestrict()
  17                 <li> Cudd_bddCharToVect()
  18                 <li> Cudd_bddLICompaction()
  19                 <li> Cudd_bddSqueeze()
  20                 <li> Cudd_SubsetCompress()
  21                 <li> Cudd_SupersetCompress()
  22                 </ul>
  23             Internal procedures included in this module:
  24                 <ul>
  25                 <li> cuddBddConstrainRecur()
  26                 <li> cuddBddRestrictRecur()
  27                 <li> cuddBddNPAndRecur()
  28                 <li> cuddAddConstrainRecur()
  29                 <li> cuddAddRestrictRecur()
  30                 <li> cuddBddLICompaction()
  31                 </ul>
  32             Static procedures included in this module:
  33                 <ul>
  34                 <li> cuddBddConstrainDecomp()
  35                 <li> cuddBddCharToVect()
  36                 <li> cuddBddLICMarkEdges()
  37                 <li> cuddBddLICBuildResult()
  38                 <li> cuddBddSqueeze()
  39                 </ul>
  40                 ]
  41
  42   Author      [Fabio Somenzi]
  43
  44   Copyright   [Copyright (c) 1995-2004, Regents of the University of Colorado
  45
  46   All rights reserved.
  47
  48   Redistribution and use in source and binary forms, with or without
  49   modification, are permitted provided that the following conditions
  50   are met:
  51
  52   Redistributions of source code must retain the above copyright
  53   notice, this list of conditions and the following disclaimer.
  54
  55   Redistributions in binary form must reproduce the above copyright
  56   notice, this list of conditions and the following disclaimer in the
  57   documentation and/or other materials provided with the distribution.
  58
  59   Neither the name of the University of Colorado nor the names of its
  60   contributors may be used to endorse or promote products derived from
  61   this software without specific prior written permission.
  62
  63   THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
  64   "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
  65   LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
  66   FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
  67   COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
  68   INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
  69   BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
  70   LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
  71   CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
  72   LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
  73   ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
  74   POSSIBILITY OF SUCH DAMAGE.]
  75
  76 ******************************************************************************/
  77
  78 #include "util.h"
  79 #include "cuddInt.h"
  80
  81
  82 /*---------------------------------------------------------------------------*/
  83 /* Constant declarations                                                     */
  84 /*---------------------------------------------------------------------------*/
  85
  86 /* Codes for edge markings in Cudd_bddLICompaction.  The codes are defined
  87 ** so that they can be bitwise ORed to implement the code priority scheme.
  88 */
  89 #define DD_LIC_DC 0
  90 #define DD_LIC_1  1
  91 #define DD_LIC_0  2
  92 #define DD_LIC_NL 3
  93
  94 /*---------------------------------------------------------------------------*/
  95 /* Stucture declarations                                                     */
  96 /*---------------------------------------------------------------------------*/
  97
  98
  99 /*---------------------------------------------------------------------------*/
 100 /* Type declarations                                                         */
 101 /*---------------------------------------------------------------------------*/
 102
 103 /* Key for the cache used in the edge marking phase. */
 104 typedef struct MarkCacheKey {
 105     DdNode *f;
 106     DdNode *c;
 107 } MarkCacheKey;
 108
 109 /*---------------------------------------------------------------------------*/
 110 /* Variable declarations                                                     */
 111 /*---------------------------------------------------------------------------*/
 112
 113 #ifndef lint
 114 static char rcsid[] DD_UNUSED = "$Id: cuddGenCof.c,v 1.38 2005/05/14 17:27:11 fabio Exp $";
 115 #endif
 116
 117 /*---------------------------------------------------------------------------*/
 118 /* Macro declarations                                                        */
 119 /*---------------------------------------------------------------------------*/
 120
 121 #ifdef __cplusplus
 122 extern "C" {
 123 #endif
 124
 125 /**AutomaticStart*************************************************************/
 126
 127 /*---------------------------------------------------------------------------*/
 128 /* Static function prototypes                                                */
 129 /*---------------------------------------------------------------------------*/
 130
 131 static int cuddBddConstrainDecomp (DdManager *dd, DdNode *f, DdNode **decomp);
 132 static DdNode * cuddBddCharToVect (DdManager *dd, DdNode *f, DdNode *x);
 133 static int cuddBddLICMarkEdges (DdManager *dd, DdNode *f, DdNode *c, st_table *table, st_table *cache);
 134 static DdNode * cuddBddLICBuildResult (DdManager *dd, DdNode *f, st_table *cache, st_table *table);
 135 static int MarkCacheHash (char *ptr, int modulus);
 136 static int MarkCacheCompare (const char *ptr1, const char *ptr2);
 137 static enum st_retval MarkCacheCleanUp (char *key, char *value, char *arg);
 138 static DdNode * cuddBddSqueeze (DdManager *dd, DdNode *l, DdNode *u);
 139
 140 /**AutomaticEnd***************************************************************/
 141
 142 #ifdef __cplusplus
 143 }
 144 #endif
 145
 146 /*---------------------------------------------------------------------------*/
 147 /* Definition of exported functions                                          */
 148 /*---------------------------------------------------------------------------*/
 149
 150
 151 /**Function********************************************************************
 152
 153   Synopsis    [Computes f constrain c.]
 154
 155   Description [Computes f constrain c (f @ c).
 156   Uses a canonical form: (f' @ c) = ( f @ c)'.  (Note: this is not true
 157   for c.)  List of special cases:
 158     <ul>
 159     <li> f @ 0 = 0
 160     <li> f @ 1 = f
 161     <li> 0 @ c = 0
 162     <li> 1 @ c = 1
 163     <li> f @ f = 1
 164     <li> f @ f'= 0
 165     </ul>
 166   Returns a pointer to the result if successful; NULL otherwise. Note that if
 167   F=(f1,...,fn) and reordering takes place while computing F @ c, then the
 168   image restriction property (Img(F,c) = Img(F @ c)) is lost.]
 169
 170   SideEffects [None]
 171
 172   SeeAlso     [Cudd_bddRestrict Cudd_addConstrain]
 173
 174 ******************************************************************************/
 175 DdNode *
 176 Cudd_bddConstrain(
 177   DdManager * dd,
 178   DdNode * f,
 179   DdNode * c)
 180 {
 181     DdNode *res;
 182
 183     do {
 184         dd->reordered = 0;
 185         res = cuddBddConstrainRecur(dd,f,c);
 186     } while (dd->reordered == 1);
 187     return(res);
 188
 189 } /* end of Cudd_bddConstrain */
 190
 191
 192 /**Function********************************************************************
 193
 194   Synopsis [BDD restrict according to Coudert and Madre's algorithm
 195   (ICCAD90).]
 196
 197   Description [BDD restrict according to Coudert and Madre's algorithm
 198   (ICCAD90). Returns the restricted BDD if successful; otherwise NULL.
 199   If application of restrict results in a BDD larger than the input
 200   BDD, the input BDD is returned.]
 201
 202   SideEffects [None]
 203
 204   SeeAlso     [Cudd_bddConstrain Cudd_addRestrict]
 205
 206 ******************************************************************************/
 207 DdNode *
 208 Cudd_bddRestrict(
 209   DdManager * dd,
 210   DdNode * f,
 211   DdNode * c)
 212 {
 213     DdNode *suppF, *suppC, *commonSupport;
 214     DdNode *cplus, *res;
 215     int retval;
 216     int sizeF, sizeRes;
 217
 218     /* Check terminal cases here to avoid computing supports in trivial cases.
 219     ** This also allows us notto check later for the case c == 0, in which
 220     ** there is no common support. */
 221     if (c == Cudd_Not(DD_ONE(dd))) return(Cudd_Not(DD_ONE(dd)));
 222     if (Cudd_IsConstant(f)) return(f);
 223     if (f == c) return(DD_ONE(dd));
 224     if (f == Cudd_Not(c)) return(Cudd_Not(DD_ONE(dd)));
 225
 226     /* Check if supports intersect. */
 227     retval = Cudd_ClassifySupport(dd,f,c,&commonSupport,&suppF,&suppC);
 228     if (retval == 0) {
 229         return(NULL);
 230     }
 231     cuddRef(commonSupport); cuddRef(suppF); cuddRef(suppC);
 232     Cudd_IterDerefBdd(dd,suppF);
 233
 234     if (commonSupport == DD_ONE(dd)) {
 235         Cudd_IterDerefBdd(dd,commonSupport);
 236         Cudd_IterDerefBdd(dd,suppC);
 237         return(f);
 238     }
 239     Cudd_IterDerefBdd(dd,commonSupport);
 240
 241     /* Abstract from c the variables that do not appear in f. */
 242     cplus = Cudd_bddExistAbstract(dd, c, suppC);
 243     if (cplus == NULL) {
 244         Cudd_IterDerefBdd(dd,suppC);
 245         return(NULL);
 246     }
 247     cuddRef(cplus);
 248     Cudd_IterDerefBdd(dd,suppC);
 249
 250     do {
 251         dd->reordered = 0;
 252         res = cuddBddRestrictRecur(dd, f, cplus);
 253     } while (dd->reordered == 1);
 254     if (res == NULL) {
 255         Cudd_IterDerefBdd(dd,cplus);
 256         return(NULL);
 257     }
 258     cuddRef(res);
 259     Cudd_IterDerefBdd(dd,cplus);
 260     /* Make restric safe by returning the smaller of the input and the
 261     ** result. */
 262     sizeF = Cudd_DagSize(f);
 263     sizeRes = Cudd_DagSize(res);
 264     if (sizeF <= sizeRes) {
 265         Cudd_IterDerefBdd(dd, res);
 266         return(f);
 267     } else {
 268         cuddDeref(res);
 269         return(res);
 270     }
 271
 272 } /* end of Cudd_bddRestrict */
 273
 274
 275 /**Function********************************************************************
 276
 277   Synopsis    [Computes f non-polluting-and g.]
 278
 279   Description [Computes f non-polluting-and g.  The non-polluting AND
 280   of f and g is a hybrid of AND and Restrict.  From Restrict, this
 281   operation takes the idea of existentially quantifying the top
 282   variable of the second operand if it does not appear in the first.
 283   Therefore, the variables that appear in the result also appear in f.
 284   For the rest, the function behaves like AND.  Since the two operands
 285   play different roles, non-polluting AND is not commutative.
 286
 287   Returns a pointer to the result if successful; NULL otherwise.]
 288
 289   SideEffects [None]
 290
 291   SeeAlso     [Cudd_bddConstrain Cudd_bddRestrict]
 292
 293 ******************************************************************************/
 294 DdNode *
 295 Cudd_bddNPAnd(
 296   DdManager * dd,
 297   DdNode * f,
 298   DdNode * g)
 299 {
 300     DdNode *res;
 301
 302     do {
 303         dd->reordered = 0;
 304         res = cuddBddNPAndRecur(dd,f,g);
 305     } while (dd->reordered == 1);
 306     return(res);
 307
 308 } /* end of Cudd_bddNPAnd */
 309
 310
 311 /**Function********************************************************************
 312
 313   Synopsis    [Computes f constrain c for ADDs.]
 314
 315   Description [Computes f constrain c (f @ c), for f an ADD and c a 0-1
 316   ADD.  List of special cases:
 317     <ul>
 318     <li> F @ 0 = 0
 319     <li> F @ 1 = F
 320     <li> 0 @ c = 0
 321     <li> 1 @ c = 1
 322     <li> F @ F = 1
 323     </ul>
 324   Returns a pointer to the result if successful; NULL otherwise.]
 325
 326   SideEffects [None]
 327
 328   SeeAlso     [Cudd_bddConstrain]
 329
 330 ******************************************************************************/
 331 DdNode *
 332 Cudd_addConstrain(
 333   DdManager * dd,
 334   DdNode * f,
 335   DdNode * c)
 336 {
 337     DdNode *res;
 338
 339     do {
 340         dd->reordered = 0;
 341         res = cuddAddConstrainRecur(dd,f,c);
 342     } while (dd->reordered == 1);
 343     return(res);
 344
 345 } /* end of Cudd_addConstrain */
 346
 347
 348 /**Function********************************************************************
 349
 350   Synopsis [BDD conjunctive decomposition as in McMillan's CAV96 paper.]
 351
 352   Description [BDD conjunctive decomposition as in McMillan's CAV96
 353   paper.  The decomposition is canonical only for a given variable
 354   order. If canonicity is required, variable ordering must be disabled
 355   after the decomposition has been computed. Returns an array with one
 356   entry for each BDD variable in the manager if successful; otherwise
 357   NULL. The components of the solution have their reference counts
 358   already incremented (unlike the results of most other functions in
 359   the package.]
 360
 361   SideEffects [None]
 362
 363   SeeAlso     [Cudd_bddConstrain Cudd_bddExistAbstract]
 364
 365 ******************************************************************************/
 366 DdNode **
 367 Cudd_bddConstrainDecomp(
 368   DdManager * dd,
 369   DdNode * f)
 370 {
 371     DdNode **decomp;
 372     int res;
 373     int i;
 374
 375     /* Create an initialize decomposition array. */
 376     decomp = ALLOC(DdNode *,dd->size);
 377     if (decomp == NULL) {
 378         dd->errorCode = CUDD_MEMORY_OUT;
 379         return(NULL);
 380     }
 381     for (i = 0; i < dd->size; i++) {
 382         decomp[i] = NULL;
 383     }
 384     do {
 385         dd->reordered = 0;
 386         /* Clean up the decomposition array in case reordering took place. */
 387         for (i = 0; i < dd->size; i++) {
 388             if (decomp[i] != NULL) {
 389                 Cudd_IterDerefBdd(dd, decomp[i]);
 390                 decomp[i] = NULL;
 391             }
 392         }
 393         res = cuddBddConstrainDecomp(dd,f,decomp);
 394     } while (dd->reordered == 1);
 395     if (res == 0) {
 396         FREE(decomp);
 397         return(NULL);
 398     }
 399     /* Missing components are constant ones. */
 400     for (i = 0; i < dd->size; i++) {
 401         if (decomp[i] == NULL) {
 402             decomp[i] = DD_ONE(dd);
 403             cuddRef(decomp[i]);
 404         }
 405     }
 406     return(decomp);
 407
 408 } /* end of Cudd_bddConstrainDecomp */
 409
 410
 411 /**Function********************************************************************
 412
 413   Synopsis [ADD restrict according to Coudert and Madre's algorithm
 414   (ICCAD90).]
 415
 416   Description [ADD restrict according to Coudert and Madre's algorithm
 417   (ICCAD90). Returns the restricted ADD if successful; otherwise NULL.
 418   If application of restrict results in an ADD larger than the input
 419   ADD, the input ADD is returned.]
 420
 421   SideEffects [None]
 422
 423   SeeAlso     [Cudd_addConstrain Cudd_bddRestrict]
 424
 425 ******************************************************************************/
 426 DdNode *
 427 Cudd_addRestrict(
 428   DdManager * dd,
 429   DdNode * f,
 430   DdNode * c)
 431 {
 432     DdNode *supp_f, *supp_c;
 433     DdNode *res, *commonSupport;
 434     int intersection;
 435     int sizeF, sizeRes;
 436
 437     /* Check if supports intersect. */
 438     supp_f = Cudd_Support(dd, f);
 439     if (supp_f == NULL) {
 440         return(NULL);
 441     }
 442     cuddRef(supp_f);
 443     supp_c = Cudd_Support(dd, c);
 444     if (supp_c == NULL) {
 445         Cudd_RecursiveDeref(dd,supp_f);
 446         return(NULL);
 447     }
 448     cuddRef(supp_c);
 449     commonSupport = Cudd_bddLiteralSetIntersection(dd, supp_f, supp_c);
 450     if (commonSupport == NULL) {
 451         Cudd_RecursiveDeref(dd,supp_f);
 452         Cudd_RecursiveDeref(dd,supp_c);
 453         return(NULL);
 454     }
 455     cuddRef(commonSupport);
 456     Cudd_RecursiveDeref(dd,supp_f);
 457     Cudd_RecursiveDeref(dd,supp_c);
 458     intersection = commonSupport != DD_ONE(dd);
 459     Cudd_RecursiveDeref(dd,commonSupport);
 460
 461     if (intersection) {
 462         do {
 463             dd->reordered = 0;
 464             res = cuddAddRestrictRecur(dd, f, c);
 465         } while (dd->reordered == 1);
 466         sizeF = Cudd_DagSize(f);
 467         sizeRes = Cudd_DagSize(res);
 468         if (sizeF <= sizeRes) {
 469             cuddRef(res);
 470             Cudd_RecursiveDeref(dd, res);
 471             return(f);
 472         } else {
 473             return(res);
 474         }
 475     } else {
 476         return(f);
 477     }
 478
 479 } /* end of Cudd_addRestrict */
 480
 481
 482 /**Function********************************************************************
 483
 484   Synopsis    [Computes a vector whose image equals a non-zero function.]
 485
 486   Description [Computes a vector of BDDs whose image equals a non-zero
 487   function.
 488   The result depends on the variable order. The i-th component of the vector
 489   depends only on the first i variables in the order.  Each BDD in the vector
 490   is not larger than the BDD of the given characteristic function.  This
 491   function is based on the description of char-to-vect in "Verification of
 492   Sequential Machines Using Boolean Functional Vectors" by O. Coudert, C.
 493   Berthet and J. C. Madre.
 494   Returns a pointer to an array containing the result if successful; NULL
 495   otherwise. The size of the array equals the number of variables in the
 496   manager. The components of the solution have their reference counts
 497   already incremented (unlike the results of most other functions in
 498   the package).]
 499
 500   SideEffects [None]
 501
 502   SeeAlso     [Cudd_bddConstrain]
 503
 504 ******************************************************************************/
 505 DdNode **
 506 Cudd_bddCharToVect(
 507   DdManager * dd,
 508   DdNode * f)
 509 {
 510     int i, j;
 511     DdNode **vect;
 512     DdNode *res = NULL;
 513
 514     if (f == Cudd_Not(DD_ONE(dd))) return(NULL);
 515
 516     vect = ALLOC(DdNode *, dd->size);
 517     if (vect == NULL) {
 518         dd->errorCode = CUDD_MEMORY_OUT;
 519         return(NULL);
 520     }
 521
 522     do {
 523         dd->reordered = 0;
 524         for (i = 0; i < dd->size; i++) {
 525             res = cuddBddCharToVect(dd,f,dd->vars[dd->invperm[i]]);
 526             if (res == NULL) {
 527                 /* Clean up the vector array in case reordering took place. */
 528                 for (j = 0; j < i; j++) {
 529                     Cudd_IterDerefBdd(dd, vect[dd->invperm[j]]);
 530                 }
 531                 break;
 532             }
 533             cuddRef(res);
 534             vect[dd->invperm[i]] = res;
 535         }
 536     } while (dd->reordered == 1);
 537     if (res == NULL) {
 538         FREE(vect);
 539         return(NULL);
 540     }
 541     return(vect);
 542
 543 } /* end of Cudd_bddCharToVect */
 544
 545
 546 /**Function********************************************************************
 547
 548   Synopsis    [Performs safe minimization of a BDD.]
 549
 550   Description [Performs safe minimization of a BDD. Given the BDD
 551   <code>f</code> of a function to be minimized and a BDD
 552   <code>c</code> representing the care set, Cudd_bddLICompaction
 553   produces the BDD of a function that agrees with <code>f</code>
 554   wherever <code>c</code> is 1.  Safe minimization means that the size
 555   of the result is guaranteed not to exceed the size of
 556   <code>f</code>. This function is based on the DAC97 paper by Hong et
 557   al..  Returns a pointer to the result if successful; NULL
 558   otherwise.]
 559
 560   SideEffects [None]
 561
 562   SeeAlso     [Cudd_bddRestrict]
 563
 564 ******************************************************************************/
 565 DdNode *
 566 Cudd_bddLICompaction(
 567   DdManager * dd /* manager */,
 568   DdNode * f /* function to be minimized */,
 569   DdNode * c /* constraint (care set) */)
 570 {
 571     DdNode *res;
 572
 573     do {
 574         dd->reordered = 0;
 575         res = cuddBddLICompaction(dd,f,c);
 576     } while (dd->reordered == 1);
 577     return(res);
 578
 579 } /* end of Cudd_bddLICompaction */
 580
 581
 582 /**Function********************************************************************
 583
 584   Synopsis    [Finds a small BDD in a function interval.]
 585
 586   Description [Finds a small BDD in a function interval. Given BDDs
 587   <code>l</code> and <code>u</code>, representing the lower bound and
 588   upper bound of a function interval, Cudd_bddSqueeze produces the BDD
 589   of a function within the interval with a small BDD.  Returns a
 590   pointer to the result if successful; NULL otherwise.]
 591
 592   SideEffects [None]
 593
 594   SeeAlso     [Cudd_bddRestrict Cudd_bddLICompaction]
 595
 596 ******************************************************************************/
 597 DdNode *
 598 Cudd_bddSqueeze(
 599   DdManager * dd /* manager */,
 600   DdNode * l /* lower bound */,
 601   DdNode * u /* upper bound */)
 602 {
 603     DdNode *res;
 604     int sizeRes, sizeL, sizeU;
 605
 606     do {
 607         dd->reordered = 0;
 608         res = cuddBddSqueeze(dd,l,u);
 609     } while (dd->reordered == 1);
 610     if (res == NULL) return(NULL);
 611     /* We now compare the result with the bounds and return the smallest.
 612     ** We first compare to u, so that in case l == 0 and u == 1, we return
 613     ** 0 as in other minimization algorithms. */
 614     sizeRes = Cudd_DagSize(res);
 615     sizeU = Cudd_DagSize(u);
 616     if (sizeU <= sizeRes) {
 617         cuddRef(res);
 618         Cudd_IterDerefBdd(dd,res);
 619         res = u;
 620         sizeRes = sizeU;
 621     }
 622     sizeL = Cudd_DagSize(l);
 623     if (sizeL <= sizeRes) {
 624         cuddRef(res);
 625         Cudd_IterDerefBdd(dd,res);
 626         res = l;
 627         sizeRes = sizeL;
 628     }
 629     return(res);
 630
 631 } /* end of Cudd_bddSqueeze */
 632
 633
 634 /**Function********************************************************************
 635
 636   Synopsis    [Finds a small BDD that agrees with <code>f</code> over
 637   <code>c</code>.]
 638
 639   Description [Finds a small BDD that agrees with <code>f</code> over
 640   <code>c</code>.  Returns a pointer to the result if successful; NULL
 641   otherwise.]
 642
 643   SideEffects [None]
 644
 645   SeeAlso     [Cudd_bddRestrict Cudd_bddLICompaction Cudd_bddSqueeze]
 646
 647 ******************************************************************************/
 648 DdNode *
 649 Cudd_bddMinimize(
 650   DdManager * dd,
 651   DdNode * f,
 652   DdNode * c)
 653 {
 654     DdNode *cplus, *res;
 655
 656     if (c == Cudd_Not(DD_ONE(dd))) return(c);
 657     if (Cudd_IsConstant(f)) return(f);
 658     if (f == c) return(DD_ONE(dd));
 659     if (f == Cudd_Not(c)) return(Cudd_Not(DD_ONE(dd)));
 660
 661     cplus = Cudd_RemapOverApprox(dd,c,0,0,1.0);
 662     if (cplus == NULL) return(NULL);
 663     cuddRef(cplus);
 664     res = Cudd_bddLICompaction(dd,f,cplus);
 665     if (res == NULL) {
 666         Cudd_IterDerefBdd(dd,cplus);
 667         return(NULL);
 668     }
 669     cuddRef(res);
 670     Cudd_IterDerefBdd(dd,cplus);
 671     cuddDeref(res);
 672     return(res);
 673
 674 } /* end of Cudd_bddMinimize */
 675
 676
 677 /**Function********************************************************************
 678
 679   Synopsis    [Find a dense subset of BDD <code>f</code>.]
 680
 681   Description [Finds a dense subset of BDD <code>f</code>. Density is
 682   the ratio of number of minterms to number of nodes.  Uses several
 683   techniques in series. It is more expensive than other subsetting
 684   procedures, but often produces better results. See
 685   Cudd_SubsetShortPaths for a description of the threshold and nvars
 686   parameters.  Returns a pointer to the result if successful; NULL
 687   otherwise.]
 688
 689   SideEffects [None]
 690
 691   SeeAlso     [Cudd_SubsetRemap Cudd_SubsetShortPaths Cudd_SubsetHeavyBranch
 692   Cudd_bddSqueeze]
 693
 694 ******************************************************************************/
 695 DdNode *
 696 Cudd_SubsetCompress(
 697   DdManager * dd /* manager */,
 698   DdNode * f /* BDD whose subset is sought */,
 699   int  nvars /* number of variables in the support of f */,
 700   int  threshold /* maximum number of nodes in the subset */)
 701 {
 702     DdNode *res, *tmp1, *tmp2;
 703
 704     tmp1 = Cudd_SubsetShortPaths(dd, f, nvars, threshold, 0);
 705     if (tmp1 == NULL) return(NULL);
 706     cuddRef(tmp1);
 707     tmp2 = Cudd_RemapUnderApprox(dd,tmp1,nvars,0,1.0);
 708     if (tmp2 == NULL) {
 709         Cudd_IterDerefBdd(dd,tmp1);
 710         return(NULL);
 711     }
 712     cuddRef(tmp2);
 713     Cudd_IterDerefBdd(dd,tmp1);
 714     res = Cudd_bddSqueeze(dd,tmp2,f);
 715     if (res == NULL) {
 716         Cudd_IterDerefBdd(dd,tmp2);
 717         return(NULL);
 718     }
 719     cuddRef(res);
 720     Cudd_IterDerefBdd(dd,tmp2);
 721     cuddDeref(res);
 722     return(res);
 723
 724 } /* end of Cudd_SubsetCompress */
 725
 726
 727 /**Function********************************************************************
 728
 729   Synopsis    [Find a dense superset of BDD <code>f</code>.]
 730
 731   Description [Finds a dense superset of BDD <code>f</code>. Density is
 732   the ratio of number of minterms to number of nodes.  Uses several
 733   techniques in series. It is more expensive than other supersetting
 734   procedures, but often produces better results. See
 735   Cudd_SupersetShortPaths for a description of the threshold and nvars
 736   parameters.  Returns a pointer to the result if successful; NULL
 737   otherwise.]
 738
 739   SideEffects [None]
 740
 741   SeeAlso     [Cudd_SubsetCompress Cudd_SupersetRemap Cudd_SupersetShortPaths
 742   Cudd_SupersetHeavyBranch Cudd_bddSqueeze]
 743
 744 ******************************************************************************/
 745 DdNode *
 746 Cudd_SupersetCompress(
 747   DdManager * dd /* manager */,
 748   DdNode * f /* BDD whose superset is sought */,
 749   int  nvars /* number of variables in the support of f */,
 750   int  threshold /* maximum number of nodes in the superset */)
 751 {
 752     DdNode *subset;
 753
 754     subset = Cudd_SubsetCompress(dd, Cudd_Not(f),nvars,threshold);
 755
 756     return(Cudd_NotCond(subset, (subset != NULL)));
 757
 758 } /* end of Cudd_SupersetCompress */
 759
 760
 761 /*---------------------------------------------------------------------------*/
 762 /* Definition of internal functions                                          */
 763 /*---------------------------------------------------------------------------*/
 764
 765
 766 /**Function********************************************************************
 767
 768   Synopsis    [Performs the recursive step of Cudd_bddConstrain.]
 769
 770   Description [Performs the recursive step of Cudd_bddConstrain.
 771   Returns a pointer to the result if successful; NULL otherwise.]
 772
 773   SideEffects [None]
 774
 775   SeeAlso     [Cudd_bddConstrain]
 776
 777 ******************************************************************************/
 778 DdNode *
 779 cuddBddConstrainRecur(
 780   DdManager * dd,
 781   DdNode * f,
 782   DdNode * c)
 783 {
 784     DdNode       *Fv, *Fnv, *Cv, *Cnv, *t, *e, *r;
 785     DdNode       *one, *zero;
 786     unsigned int topf, topc;
 787     int          index;
 788     int          comple = 0;
 789
 790     statLine(dd);
 791     one = DD_ONE(dd);
 792     zero = Cudd_Not(one);
 793
 794     /* Trivial cases. */
 795     if (c == one)               return(f);
 796     if (c == zero)              return(zero);
 797     if (Cudd_IsConstant(f))     return(f);
 798     if (f == c)                 return(one);
 799     if (f == Cudd_Not(c))       return(zero);
 800
 801     /* Make canonical to increase the utilization of the cache. */
 802     if (Cudd_IsComplement(f)) {
 803         f = Cudd_Not(f);
 804         comple = 1;
 805     }
 806     /* Now f is a regular pointer to a non-constant node; c is also
 807     ** non-constant, but may be complemented.
 808     */
 809
 810     /* Check the cache. */
 811     r = cuddCacheLookup2(dd, Cudd_bddConstrain, f, c);
 812     if (r != NULL) {
 813         return(Cudd_NotCond(r,comple));
 814     }
 815
 816     /* Recursive step. */
 817     topf = dd->perm[f->index];
 818     topc = dd->perm[Cudd_Regular(c)->index];
 819     if (topf <= topc) {
 820         index = f->index;
 821         Fv = cuddT(f); Fnv = cuddE(f);
 822     } else {
 823         index = Cudd_Regular(c)->index;
 824         Fv = Fnv = f;
 825     }
 826     if (topc <= topf) {
 827         Cv = cuddT(Cudd_Regular(c)); Cnv = cuddE(Cudd_Regular(c));
 828         if (Cudd_IsComplement(c)) {
 829             Cv = Cudd_Not(Cv);
 830             Cnv = Cudd_Not(Cnv);
 831         }
 832     } else {
 833         Cv = Cnv = c;
 834     }
 835
 836     if (!Cudd_IsConstant(Cv)) {
 837         t = cuddBddConstrainRecur(dd, Fv, Cv);
 838         if (t == NULL)
 839             return(NULL);
 840     } else if (Cv == one) {
 841         t = Fv;
 842     } else {            /* Cv == zero: return Fnv @ Cnv */
 843         if (Cnv == one) {
 844             r = Fnv;
 845         } else {
 846             r = cuddBddConstrainRecur(dd, Fnv, Cnv);
 847             if (r == NULL)
 848                 return(NULL);
 849         }
 850         return(Cudd_NotCond(r,comple));
 851     }
 852     cuddRef(t);
 853
 854     if (!Cudd_IsConstant(Cnv)) {
 855         e = cuddBddConstrainRecur(dd, Fnv, Cnv);
 856         if (e == NULL) {
 857             Cudd_IterDerefBdd(dd, t);
 858             return(NULL);
 859         }
 860     } else if (Cnv == one) {
 861         e = Fnv;
 862     } else {            /* Cnv == zero: return Fv @ Cv previously computed */
 863         cuddDeref(t);
 864         return(Cudd_NotCond(t,comple));
 865     }
 866     cuddRef(e);
 867
 868     if (Cudd_IsComplement(t)) {
 869         t = Cudd_Not(t);
 870         e = Cudd_Not(e);
 871         r = (t == e) ? t : cuddUniqueInter(dd, index, t, e);
 872         if (r == NULL) {
 873             Cudd_IterDerefBdd(dd, e);
 874             Cudd_IterDerefBdd(dd, t);
 875             return(NULL);
 876         }
 877         r = Cudd_Not(r);
 878     } else {
 879         r = (t == e) ? t : cuddUniqueInter(dd, index, t, e);
 880         if (r == NULL) {
 881             Cudd_IterDerefBdd(dd, e);
 882             Cudd_IterDerefBdd(dd, t);
 883             return(NULL);
 884         }
 885     }
 886     cuddDeref(t);
 887     cuddDeref(e);
 888
 889     cuddCacheInsert2(dd, Cudd_bddConstrain, f, c, r);
 890     return(Cudd_NotCond(r,comple));
 891
 892 } /* end of cuddBddConstrainRecur */
 893
 894
 895 /**Function********************************************************************
 896
 897   Synopsis    [Performs the recursive step of Cudd_bddRestrict.]
 898
 899   Description [Performs the recursive step of Cudd_bddRestrict.
 900   Returns the restricted BDD if successful; otherwise NULL.]
 901
 902   SideEffects [None]
 903
 904   SeeAlso     [Cudd_bddRestrict]
 905
 906 ******************************************************************************/
 907 DdNode *
 908 cuddBddRestrictRecur(
 909   DdManager * dd,
 910   DdNode * f,
 911   DdNode * c)
 912 {
 913     DdNode       *Fv, *Fnv, *Cv, *Cnv, *t, *e, *r, *one, *zero;
 914     unsigned int topf, topc;
 915     int          index;
 916     int          comple = 0;
 917
 918     statLine(dd);
 919     one = DD_ONE(dd);
 920     zero = Cudd_Not(one);
 921
 922     /* Trivial cases */
 923     if (c == one)               return(f);
 924     if (c == zero)              return(zero);
 925     if (Cudd_IsConstant(f))     return(f);
 926     if (f == c)                 return(one);
 927     if (f == Cudd_Not(c))       return(zero);
 928
 929     /* Make canonical to increase the utilization of the cache. */
 930     if (Cudd_IsComplement(f)) {
 931         f = Cudd_Not(f);
 932         comple = 1;
 933     }
 934     /* Now f is a regular pointer to a non-constant node; c is also
 935     ** non-constant, but may be complemented.
 936     */
 937
 938     /* Check the cache. */
 939     r = cuddCacheLookup2(dd, Cudd_bddRestrict, f, c);
 940     if (r != NULL) {
 941         return(Cudd_NotCond(r,comple));
 942     }
 943
 944     topf = dd->perm[f->index];
 945     topc = dd->perm[Cudd_Regular(c)->index];
 946
 947     if (topc < topf) {  /* abstract top variable from c */
 948         DdNode *d, *s1, *s2;
 949
 950         /* Find complements of cofactors of c. */
 951         if (Cudd_IsComplement(c)) {
 952             s1 = cuddT(Cudd_Regular(c));
 953             s2 = cuddE(Cudd_Regular(c));
 954         } else {
 955             s1 = Cudd_Not(cuddT(c));
 956             s2 = Cudd_Not(cuddE(c));
 957         }
 958         /* Take the OR by applying DeMorgan. */
 959         d = cuddBddAndRecur(dd, s1, s2);
 960         if (d == NULL) return(NULL);
 961         d = Cudd_Not(d);
 962         cuddRef(d);
 963         r = cuddBddRestrictRecur(dd, f, d);
 964         if (r == NULL) {
 965             Cudd_IterDerefBdd(dd, d);
 966             return(NULL);
 967         }
 968         cuddRef(r);
 969         Cudd_IterDerefBdd(dd, d);
 970         cuddCacheInsert2(dd, Cudd_bddRestrict, f, c, r);
 971         cuddDeref(r);
 972         return(Cudd_NotCond(r,comple));
 973     }
 974
 975     /* Recursive step. Here topf <= topc. */
 976     index = f->index;
 977     Fv = cuddT(f); Fnv = cuddE(f);
 978     if (topc == topf) {
 979         Cv = cuddT(Cudd_Regular(c)); Cnv = cuddE(Cudd_Regular(c));
 980         if (Cudd_IsComplement(c)) {
 981             Cv = Cudd_Not(Cv);
 982             Cnv = Cudd_Not(Cnv);
 983         }
 984     } else {
 985         Cv = Cnv = c;
 986     }
 987
 988     if (!Cudd_IsConstant(Cv)) {
 989         t = cuddBddRestrictRecur(dd, Fv, Cv);
 990         if (t == NULL) return(NULL);
 991     } else if (Cv == one) {
 992         t = Fv;
 993     } else {            /* Cv == zero: return(Fnv @ Cnv) */
 994         if (Cnv == one) {
 995             r = Fnv;
 996         } else {
 997             r = cuddBddRestrictRecur(dd, Fnv, Cnv);
 998             if (r == NULL) return(NULL);
 999         }
1000         return(Cudd_NotCond(r,comple));
1001     }
1002     cuddRef(t);
1003
1004     if (!Cudd_IsConstant(Cnv)) {
1005         e = cuddBddRestrictRecur(dd, Fnv, Cnv);
1006         if (e == NULL) {
1007             Cudd_IterDerefBdd(dd, t);
1008             return(NULL);
1009         }
1010     } else if (Cnv == one) {
1011         e = Fnv;
1012     } else {            /* Cnv == zero: return (Fv @ Cv) previously computed */
1013         cuddDeref(t);
1014         return(Cudd_NotCond(t,comple));
1015     }
1016     cuddRef(e);
1017
1018     if (Cudd_IsComplement(t)) {
1019         t = Cudd_Not(t);
1020         e = Cudd_Not(e);
1021         r = (t == e) ? t : cuddUniqueInter(dd, index, t, e);
1022         if (r == NULL) {
1023             Cudd_IterDerefBdd(dd, e);
1024             Cudd_IterDerefBdd(dd, t);
1025             return(NULL);
1026         }
1027         r = Cudd_Not(r);
1028     } else {
1029         r = (t == e) ? t : cuddUniqueInter(dd, index, t, e);
1030         if (r == NULL) {
1031             Cudd_IterDerefBdd(dd, e);
1032             Cudd_IterDerefBdd(dd, t);
1033             return(NULL);
1034         }
1035     }
1036     cuddDeref(t);
1037     cuddDeref(e);
1038
1039     cuddCacheInsert2(dd, Cudd_bddRestrict, f, c, r);
1040     return(Cudd_NotCond(r,comple));
1041
1042 } /* end of cuddBddRestrictRecur */
1043
1044
1045 /**Function********************************************************************
1046
1047   Synopsis [Implements the recursive step of Cudd_bddAnd.]
1048
1049   Description [Implements the recursive step of Cudd_bddNPAnd.
1050   Returns a pointer to the result is successful; NULL otherwise.]
1051
1052   SideEffects [None]
1053
1054   SeeAlso     [Cudd_bddNPAnd]
1055
1056 ******************************************************************************/
1057 DdNode *
1058 cuddBddNPAndRecur(
1059   DdManager * manager,
1060   DdNode * f,
1061   DdNode * g)
1062 {
1063     DdNode *F, *ft, *fe, *G, *gt, *ge;
1064     DdNode *one, *r, *t, *e;
1065     unsigned int topf, topg, index;
1066
1067     statLine(manager);
1068     one = DD_ONE(manager);
1069
1070     /* Terminal cases. */
1071     F = Cudd_Regular(f);
1072     G = Cudd_Regular(g);
1073     if (F == G) {
1074         if (f == g) return(one);
1075         else return(Cudd_Not(one));
1076     }
1077     if (G == one) {
1078         if (g == one) return(f);
1079         else return(g);
1080     }
1081     if (F == one) {
1082         return(f);
1083     }
1084
1085     /* At this point f and g are not constant. */
1086     /* Check cache. */
1087     if (F->ref != 1 || G->ref != 1) {
1088         r = cuddCacheLookup2(manager, Cudd_bddNPAnd, f, g);
1089         if (r != NULL) return(r);
1090     }
1091
1092     /* Here we can skip the use of cuddI, because the operands are known
1093     ** to be non-constant.
1094     */
1095     topf = manager->perm[F->index];
1096     topg = manager->perm[G->index];
1097
1098     if (topg < topf) {  /* abstract top variable from g */
1099         DdNode *d;
1100
1101         /* Find complements of cofactors of g. */
1102         if (Cudd_IsComplement(g)) {
1103             gt = cuddT(G);
1104             ge = cuddE(G);
1105         } else {
1106             gt = Cudd_Not(cuddT(g));
1107             ge = Cudd_Not(cuddE(g));
1108         }
1109         /* Take the OR by applying DeMorgan. */
1110         d = cuddBddAndRecur(manager, gt, ge);
1111         if (d == NULL) return(NULL);
1112         d = Cudd_Not(d);
1113         cuddRef(d);
1114         r = cuddBddNPAndRecur(manager, f, d);
1115         if (r == NULL) {
1116             Cudd_IterDerefBdd(manager, d);
1117             return(NULL);
1118         }
1119         cuddRef(r);
1120         Cudd_IterDerefBdd(manager, d);
1121         cuddCacheInsert2(manager, Cudd_bddNPAnd, f, g, r);
1122         cuddDeref(r);
1123         return(r);
1124     }
1125
1126     /* Compute cofactors. */
1127     index = F->index;
1128     ft = cuddT(F);
1129     fe = cuddE(F);
1130     if (Cudd_IsComplement(f)) {
1131       ft = Cudd_Not(ft);
1132       fe = Cudd_Not(fe);
1133     }
1134
1135     if (topg == topf) {
1136         gt = cuddT(G);
1137         ge = cuddE(G);
1138         if (Cudd_IsComplement(g)) {
1139             gt = Cudd_Not(gt);
1140             ge = Cudd_Not(ge);
1141         }
1142     } else {
1143         gt = ge = g;
1144     }
1145
1146     t = cuddBddAndRecur(manager, ft, gt);
1147     if (t == NULL) return(NULL);
1148     cuddRef(t);
1149
1150     e = cuddBddAndRecur(manager, fe, ge);
1151     if (e == NULL) {
1152         Cudd_IterDerefBdd(manager, t);
1153         return(NULL);
1154     }
1155     cuddRef(e);
1156
1157     if (t == e) {
1158         r = t;
1159     } else {
1160         if (Cudd_IsComplement(t)) {
1161             r = cuddUniqueInter(manager,(int)index,Cudd_Not(t),Cudd_Not(e));
1162             if (r == NULL) {
1163                 Cudd_IterDerefBdd(manager, t);
1164                 Cudd_IterDerefBdd(manager, e);
1165                 return(NULL);
1166             }
1167             r = Cudd_Not(r);
1168         } else {
1169             r = cuddUniqueInter(manager,(int)index,t,e);
1170             if (r == NULL) {
1171                 Cudd_IterDerefBdd(manager, t);
1172                 Cudd_IterDerefBdd(manager, e);
1173                 return(NULL);
1174             }
1175         }
1176     }
1177     cuddDeref(e);
1178     cuddDeref(t);
1179     if (F->ref != 1 || G->ref != 1)
1180         cuddCacheInsert2(manager, Cudd_bddNPAnd, f, g, r);
1181     return(r);
1182
1183 } /* end of cuddBddNPAndRecur */
1184
1185
1186 /**Function********************************************************************
1187
1188   Synopsis    [Performs the recursive step of Cudd_addConstrain.]
1189
1190   Description [Performs the recursive step of Cudd_addConstrain.
1191   Returns a pointer to the result if successful; NULL otherwise.]
1192
1193   SideEffects [None]
1194
1195   SeeAlso     [Cudd_addConstrain]
1196
1197 ******************************************************************************/
1198 DdNode *
1199 cuddAddConstrainRecur(
1200   DdManager * dd,
1201   DdNode * f,
1202   DdNode * c)
1203 {
1204     DdNode       *Fv, *Fnv, *Cv, *Cnv, *t, *e, *r;
1205     DdNode       *one, *zero;
1206     unsigned int topf, topc;
1207     int          index;
1208
1209     statLine(dd);
1210     one = DD_ONE(dd);
1211     zero = DD_ZERO(dd);
1212
1213     /* Trivial cases. */
1214     if (c == one)               return(f);
1215     if (c == zero)              return(zero);
1216     if (Cudd_IsConstant(f))     return(f);
1217     if (f == c)                 return(one);
1218
1219     /* Now f and c are non-constant. */
1220
1221     /* Check the cache. */
1222     r = cuddCacheLookup2(dd, Cudd_addConstrain, f, c);
1223     if (r != NULL) {
1224         return(r);
1225     }
1226
1227     /* Recursive step. */
1228     topf = dd->perm[f->index];
1229     topc = dd->perm[c->index];
1230     if (topf <= topc) {
1231         index = f->index;
1232         Fv = cuddT(f); Fnv = cuddE(f);
1233     } else {
1234         index = c->index;
1235         Fv = Fnv = f;
1236     }
1237     if (topc <= topf) {
1238         Cv = cuddT(c); Cnv = cuddE(c);
1239     } else {
1240         Cv = Cnv = c;
1241     }
1242
1243     if (!Cudd_IsConstant(Cv)) {
1244         t = cuddAddConstrainRecur(dd, Fv, Cv);
1245         if (t == NULL)
1246             return(NULL);
1247     } else if (Cv == one) {
1248         t = Fv;
1249     } else {            /* Cv == zero: return Fnv @ Cnv */
1250         if (Cnv == one) {
1251             r = Fnv;
1252         } else {
1253             r = cuddAddConstrainRecur(dd, Fnv, Cnv);
1254             if (r == NULL)
1255                 return(NULL);
1256         }
1257         return(r);
1258     }
1259     cuddRef(t);
1260
1261     if (!Cudd_IsConstant(Cnv)) {
1262         e = cuddAddConstrainRecur(dd, Fnv, Cnv);
1263         if (e == NULL) {
1264             Cudd_RecursiveDeref(dd, t);
1265             return(NULL);
1266         }
1267     } else if (Cnv == one) {
1268         e = Fnv;
1269     } else {            /* Cnv == zero: return Fv @ Cv previously computed */
1270         cuddDeref(t);
1271         return(t);
1272     }
1273     cuddRef(e);
1274
1275     r = (t == e) ? t : cuddUniqueInter(dd, index, t, e);
1276     if (r == NULL) {
1277         Cudd_RecursiveDeref(dd, e);
1278         Cudd_RecursiveDeref(dd, t);
1279         return(NULL);
1280     }
1281     cuddDeref(t);
1282     cuddDeref(e);
1283
1284     cuddCacheInsert2(dd, Cudd_addConstrain, f, c, r);
1285     return(r);
1286
1287 } /* end of cuddAddConstrainRecur */
1288
1289
1290 /**Function********************************************************************
1291
1292   Synopsis    [Performs the recursive step of Cudd_addRestrict.]
1293
1294   Description [Performs the recursive step of Cudd_addRestrict.
1295   Returns the restricted ADD if successful; otherwise NULL.]
1296
1297   SideEffects [None]
1298
1299   SeeAlso     [Cudd_addRestrict]
1300
1301 ******************************************************************************/
1302 DdNode *
1303 cuddAddRestrictRecur(
1304   DdManager * dd,
1305   DdNode * f,
1306   DdNode * c)
1307 {
1308     DdNode       *Fv, *Fnv, *Cv, *Cnv, *t, *e, *r, *one, *zero;
1309     unsigned int topf, topc;
1310     int          index;
1311
1312     statLine(dd);
1313     one = DD_ONE(dd);
1314     zero = DD_ZERO(dd);
1315
1316     /* Trivial cases */
1317     if (c == one)               return(f);
1318     if (c == zero)              return(zero);
1319     if (Cudd_IsConstant(f))     return(f);
1320     if (f == c)                 return(one);
1321
1322     /* Now f and c are non-constant. */
1323
1324     /* Check the cache. */
1325     r = cuddCacheLookup2(dd, Cudd_addRestrict, f, c);
1326     if (r != NULL) {
1327         return(r);
1328     }
1329
1330     topf = dd->perm[f->index];
1331     topc = dd->perm[c->index];
1332
1333     if (topc < topf) {  /* abstract top variable from c */
1334         DdNode *d, *s1, *s2;
1335
1336         /* Find cofactors of c. */
1337         s1 = cuddT(c);
1338         s2 = cuddE(c);
1339         /* Take the OR by applying DeMorgan. */
1340         d = cuddAddApplyRecur(dd, Cudd_addOr, s1, s2);
1341         if (d == NULL) return(NULL);
1342         cuddRef(d);
1343         r = cuddAddRestrictRecur(dd, f, d);
1344         if (r == NULL) {
1345             Cudd_RecursiveDeref(dd, d);
1346             return(NULL);
1347         }
1348         cuddRef(r);
1349         Cudd_RecursiveDeref(dd, d);
1350         cuddCacheInsert2(dd, Cudd_addRestrict, f, c, r);
1351         cuddDeref(r);
1352         return(r);
1353     }
1354
1355     /* Recursive step. Here topf <= topc. */
1356     index = f->index;
1357     Fv = cuddT(f); Fnv = cuddE(f);
1358     if (topc == topf) {
1359         Cv = cuddT(c); Cnv = cuddE(c);
1360     } else {
1361         Cv = Cnv = c;
1362     }
1363
1364     if (!Cudd_IsConstant(Cv)) {
1365         t = cuddAddRestrictRecur(dd, Fv, Cv);
1366         if (t == NULL) return(NULL);
1367     } else if (Cv == one) {
1368         t = Fv;
1369     } else {            /* Cv == zero: return(Fnv @ Cnv) */
1370         if (Cnv == one) {
1371             r = Fnv;
1372         } else {
1373             r = cuddAddRestrictRecur(dd, Fnv, Cnv);
1374             if (r == NULL) return(NULL);
1375         }
1376         return(r);
1377     }
1378     cuddRef(t);
1379
1380     if (!Cudd_IsConstant(Cnv)) {
1381         e = cuddAddRestrictRecur(dd, Fnv, Cnv);
1382         if (e == NULL) {
1383             Cudd_RecursiveDeref(dd, t);
1384             return(NULL);
1385         }
1386     } else if (Cnv == one) {
1387         e = Fnv;
1388     } else {            /* Cnv == zero: return (Fv @ Cv) previously computed */
1389         cuddDeref(t);
1390         return(t);
1391     }
1392     cuddRef(e);
1393
1394     r = (t == e) ? t : cuddUniqueInter(dd, index, t, e);
1395     if (r == NULL) {
1396         Cudd_RecursiveDeref(dd, e);
1397         Cudd_RecursiveDeref(dd, t);
1398         return(NULL);
1399     }
1400     cuddDeref(t);
1401     cuddDeref(e);
1402
1403     cuddCacheInsert2(dd, Cudd_addRestrict, f, c, r);
1404     return(r);
1405
1406 } /* end of cuddAddRestrictRecur */
1407
1408
1409
1410 /**Function********************************************************************
1411
1412   Synopsis    [Performs safe minimization of a BDD.]
1413
1414   Description [Performs safe minimization of a BDD. Given the BDD
1415   <code>f</code> of a function to be minimized and a BDD
1416   <code>c</code> representing the care set, Cudd_bddLICompaction
1417   produces the BDD of a function that agrees with <code>f</code>
1418   wherever <code>c</code> is 1.  Safe minimization means that the size
1419   of the result is guaranteed not to exceed the size of
1420   <code>f</code>. This function is based on the DAC97 paper by Hong et
1421   al..  Returns a pointer to the result if successful; NULL
1422   otherwise.]
1423
1424   SideEffects [None]
1425
1426   SeeAlso     [Cudd_bddLICompaction]
1427
1428 ******************************************************************************/
1429 DdNode *
1430 cuddBddLICompaction(
1431   DdManager * dd /* manager */,
1432   DdNode * f /* function to be minimized */,
1433   DdNode * c /* constraint (care set) */)
1434 {
1435     st_table *marktable, *markcache, *buildcache;
1436     DdNode *res, *zero;
1437
1438     zero = Cudd_Not(DD_ONE(dd));
1439     if (c == zero) return(zero);
1440
1441     /* We need to use local caches for both steps of this operation.
1442     ** The results of the edge marking step are only valid as long as the
1443     ** edge markings themselves are available. However, the edge markings
1444     ** are lost at the end of one invocation of Cudd_bddLICompaction.
1445     ** Hence, the cache entries for the edge marking step must be
1446     ** invalidated at the end of this function.
1447     ** For the result of the building step we argue as follows. The result
1448     ** for a node and a given constrain depends on the BDD in which the node
1449     ** appears. Hence, the same node and constrain may give different results
1450     ** in successive invocations.
1451     */
1452     marktable = st_init_table(st_ptrcmp,st_ptrhash);
1453     if (marktable == NULL) {
1454         return(NULL);
1455     }
1456     markcache = st_init_table(MarkCacheCompare,MarkCacheHash);
1457     if (markcache == NULL) {
1458         st_free_table(marktable);
1459         return(NULL);
1460     }
1461     if (cuddBddLICMarkEdges(dd,f,c,marktable,markcache) == CUDD_OUT_OF_MEM) {
1462         st_foreach(markcache, MarkCacheCleanUp, NULL);
1463         st_free_table(marktable);
1464         st_free_table(markcache);
1465         return(NULL);
1466     }
1467     st_foreach(markcache, MarkCacheCleanUp, NULL);
1468     st_free_table(markcache);
1469     buildcache = st_init_table(st_ptrcmp,st_ptrhash);
1470     if (buildcache == NULL) {
1471         st_free_table(marktable);
1472         return(NULL);
1473     }
1474     res = cuddBddLICBuildResult(dd,f,buildcache,marktable);
1475     st_free_table(buildcache);
1476     st_free_table(marktable);
1477     return(res);
1478
1479 } /* end of cuddBddLICompaction */
1480
1481
1482 /*---------------------------------------------------------------------------*/
1483 /* Definition of static functions                                            */
1484 /*---------------------------------------------------------------------------*/
1485
1486
1487 /**Function********************************************************************
1488
1489   Synopsis    [Performs the recursive step of Cudd_bddConstrainDecomp.]
1490
1491   Description [Performs the recursive step of Cudd_bddConstrainDecomp.
1492   Returns f super (i) if successful; otherwise NULL.]
1493
1494   SideEffects [None]
1495
1496   SeeAlso     [Cudd_bddConstrainDecomp]
1497
1498 ******************************************************************************/
1499 static int
1500 cuddBddConstrainDecomp(
1501   DdManager * dd,
1502   DdNode * f,
1503   DdNode ** decomp)
1504 {
1505     DdNode *F, *fv, *fvn;
1506     DdNode *fAbs;
1507     DdNode *result;
1508     int ok;
1509
1510     if (Cudd_IsConstant(f)) return(1);
1511     /* Compute complements of cofactors. */
1512     F = Cudd_Regular(f);
1513     fv = cuddT(F);
1514     fvn = cuddE(F);
1515     if (F == f) {
1516         fv = Cudd_Not(fv);
1517         fvn = Cudd_Not(fvn);
1518     }
1519     /* Compute abstraction of top variable. */
1520     fAbs = cuddBddAndRecur(dd, fv, fvn);
1521     if (fAbs == NULL) {
1522         return(0);
1523     }
1524     cuddRef(fAbs);
1525     fAbs = Cudd_Not(fAbs);
1526     /* Recursively find the next abstraction and the components of the
1527     ** decomposition. */
1528     ok = cuddBddConstrainDecomp(dd, fAbs, decomp);
1529     if (ok == 0) {
1530         Cudd_IterDerefBdd(dd,fAbs);
1531         return(0);
1532     }
1533     /* Compute the component of the decomposition corresponding to the
1534     ** top variable and store it in the decomposition array. */
1535     result = cuddBddConstrainRecur(dd, f, fAbs);
1536     if (result == NULL) {
1537         Cudd_IterDerefBdd(dd,fAbs);
1538         return(0);
1539     }
1540     cuddRef(result);
1541     decomp[F->index] = result;
1542     Cudd_IterDerefBdd(dd, fAbs);
1543     return(1);
1544
1545 } /* end of cuddBddConstrainDecomp */
1546
1547
1548 /**Function********************************************************************
1549
1550   Synopsis    [Performs the recursive step of Cudd_bddCharToVect.]
1551
1552   Description [Performs the recursive step of Cudd_bddCharToVect.
1553   This function maintains the invariant that f is non-zero.
1554   Returns the i-th component of the vector if successful; otherwise NULL.]
1555
1556   SideEffects [None]
1557
1558   SeeAlso     [Cudd_bddCharToVect]
1559
1560 ******************************************************************************/
1561 static DdNode *
1562 cuddBddCharToVect(
1563   DdManager * dd,
1564   DdNode * f,
1565   DdNode * x)
1566 {
1567     unsigned int topf;
1568     unsigned int level;
1569     int comple;
1570
1571     DdNode *one, *zero, *res, *F, *fT, *fE, *T, *E;
1572
1573     statLine(dd);
1574     /* Check the cache. */
1575     res = cuddCacheLookup2(dd, cuddBddCharToVect, f, x);
1576     if (res != NULL) {
1577         return(res);
1578     }
1579
1580     F = Cudd_Regular(f);
1581
1582     topf = cuddI(dd,F->index);
1583     level = dd->perm[x->index];
1584
1585     if (topf > level) return(x);
1586
1587     one = DD_ONE(dd);
1588     zero = Cudd_Not(one);
1589
1590     comple = F != f;
1591     fT = Cudd_NotCond(cuddT(F),comple);
1592     fE = Cudd_NotCond(cuddE(F),comple);
1593
1594     if (topf == level) {
1595         if (fT == zero) return(zero);
1596         if (fE == zero) return(one);
1597         return(x);
1598     }
1599
1600     /* Here topf < level. */
1601     if (fT == zero) return(cuddBddCharToVect(dd, fE, x));
1602     if (fE == zero) return(cuddBddCharToVect(dd, fT, x));
1603
1604     T = cuddBddCharToVect(dd, fT, x);
1605     if (T == NULL) {
1606         return(NULL);
1607     }
1608     cuddRef(T);
1609     E = cuddBddCharToVect(dd, fE, x);
1610     if (E == NULL) {
1611         Cudd_IterDerefBdd(dd,T);
1612         return(NULL);
1613     }
1614     cuddRef(E);
1615     res = cuddBddIteRecur(dd, dd->vars[F->index], T, E);
1616     if (res == NULL) {
1617         Cudd_IterDerefBdd(dd,T);
1618         Cudd_IterDerefBdd(dd,E);
1619         return(NULL);
1620     }
1621     cuddDeref(T);
1622     cuddDeref(E);
1623     cuddCacheInsert2(dd, cuddBddCharToVect, f, x, res);
1624     return(res);
1625
1626 } /* end of cuddBddCharToVect */
1627
1628
1629 /**Function********************************************************************
1630
1631   Synopsis    [Performs the edge marking step of Cudd_bddLICompaction.]
1632
1633   Description [Performs the edge marking step of Cudd_bddLICompaction.
1634   Returns the LUB of the markings of the two outgoing edges of <code>f</code>
1635   if successful; otherwise CUDD_OUT_OF_MEM.]
1636
1637   SideEffects [None]
1638
1639   SeeAlso     [Cudd_bddLICompaction cuddBddLICBuildResult]
1640
1641 ******************************************************************************/
1642 static int
1643 cuddBddLICMarkEdges(
1644   DdManager * dd,
1645   DdNode * f,
1646   DdNode * c,
1647   st_table * table,
1648   st_table * cache)
1649 {
1650     DdNode *Fv, *Fnv, *Cv, *Cnv;
1651     DdNode *one, *zero;
1652     unsigned int topf, topc;
1653     int comple;
1654     int resT, resE, res, retval;
1655     char **slot;
1656     MarkCacheKey *key;
1657
1658     one = DD_ONE(dd);
1659     zero = Cudd_Not(one);
1660
1661     /* Terminal cases. */
1662     if (c == zero) return(DD_LIC_DC);
1663     if (f == one)  return(DD_LIC_1);
1664     if (f == zero) return(DD_LIC_0);
1665
1666     /* Make canonical to increase the utilization of the cache. */
1667     comple = Cudd_IsComplement(f);
1668     f = Cudd_Regular(f);
1669     /* Now f is a regular pointer to a non-constant node; c may be
1670     ** constant, or it may be complemented.
1671     */
1672
1673     /* Check the cache. */
1674     key = ALLOC(MarkCacheKey, 1);
1675     if (key == NULL) {
1676         dd->errorCode = CUDD_MEMORY_OUT;
1677         return(CUDD_OUT_OF_MEM);
1678     }
1679     key->f = f; key->c = c;
1680     if (st_lookup_int(cache, (char *)key, &res)) {
1681         FREE(key);
1682         if (comple) {
1683             if (res == DD_LIC_0) res = DD_LIC_1;
1684             else if (res == DD_LIC_1) res = DD_LIC_0;
1685         }
1686         return(res);
1687     }
1688
1689     /* Recursive step. */
1690     topf = dd->perm[f->index];
1691     topc = cuddI(dd,Cudd_Regular(c)->index);
1692     if (topf <= topc) {
1693         Fv = cuddT(f); Fnv = cuddE(f);
1694     } else {
1695         Fv = Fnv = f;
1696     }
1697     if (topc <= topf) {
1698         /* We know that c is not constant because f is not. */
1699         Cv = cuddT(Cudd_Regular(c)); Cnv = cuddE(Cudd_Regular(c));
1700         if (Cudd_IsComplement(c)) {
1701             Cv = Cudd_Not(Cv);
1702             Cnv = Cudd_Not(Cnv);
1703         }
1704     } else {
1705         Cv = Cnv = c;
1706     }
1707
1708     resT = cuddBddLICMarkEdges(dd, Fv, Cv, table, cache);
1709     if (resT == CUDD_OUT_OF_MEM) {
1710         FREE(key);
1711         return(CUDD_OUT_OF_MEM);
1712     }
1713     resE = cuddBddLICMarkEdges(dd, Fnv, Cnv, table, cache);
1714     if (resE == CUDD_OUT_OF_MEM) {
1715         FREE(key);
1716         return(CUDD_OUT_OF_MEM);
1717     }
1718
1719     /* Update edge markings. */
1720     if (topf <= topc) {
1721         retval = st_find_or_add(table, (char *)f, (char ***)&slot);
1722         if (retval == 0) {
1723             *slot = (char *) (ptrint)((resT << 2) | resE);
1724         } else if (retval == 1) {
1725             *slot = (char *) (ptrint)((int)((ptrint) *slot) | (resT << 2) | resE);
1726         } else {
1727             FREE(key);
1728             return(CUDD_OUT_OF_MEM);
1729         }
1730     }
1731
1732     /* Cache result. */
1733     res = resT | resE;
1734     if (st_insert(cache, (char *)key, (char *)(ptrint)res) == ST_OUT_OF_MEM) {
1735         FREE(key);
1736         return(CUDD_OUT_OF_MEM);
1737     }
1738
1739     /* Take into account possible complementation. */
1740     if (comple) {
1741         if (res == DD_LIC_0) res = DD_LIC_1;
1742         else if (res == DD_LIC_1) res = DD_LIC_0;
1743     }
1744     return(res);
1745
1746 } /* end of cuddBddLICMarkEdges */
1747
1748
1749 /**Function********************************************************************
1750
1751   Synopsis    [Builds the result of Cudd_bddLICompaction.]
1752
1753   Description [Builds the results of Cudd_bddLICompaction.
1754   Returns a pointer to the minimized BDD if successful; otherwise NULL.]
1755
1756   SideEffects [None]
1757
1758   SeeAlso     [Cudd_bddLICompaction cuddBddLICMarkEdges]
1759
1760 ******************************************************************************/
1761 static DdNode *
1762 cuddBddLICBuildResult(
1763   DdManager * dd,
1764   DdNode * f,
1765   st_table * cache,
1766   st_table * table)
1767 {
1768     DdNode *Fv, *Fnv, *r, *t, *e;
1769     DdNode *one, *zero;
1770     int index;
1771     int comple;
1772     int markT, markE, markings;
1773
1774     one = DD_ONE(dd);
1775     zero = Cudd_Not(one);
1776
1777     if (Cudd_IsConstant(f)) return(f);
1778     /* Make canonical to increase the utilization of the cache. */
1779     comple = Cudd_IsComplement(f);
1780     f = Cudd_Regular(f);
1781
1782     /* Check the cache. */
1783     if (st_lookup(cache, f, &r)) {
1784         return(Cudd_NotCond(r,comple));
1785     }
1786
1787     /* Retrieve the edge markings. */
1788     if (st_lookup_int(table, (char *)f, &markings) == 0)
1789         return(NULL);
1790     markT = markings >> 2;
1791     markE = markings & 3;
1792
1793     index = f->index;
1794     Fv = cuddT(f); Fnv = cuddE(f);
1795
1796     if (markT == DD_LIC_NL) {
1797         t = cuddBddLICBuildResult(dd,Fv,cache,table);
1798         if (t == NULL) {
1799             return(NULL);
1800         }
1801     } else if (markT == DD_LIC_1) {
1802         t = one;
1803     } else {
1804         t = zero;
1805     }
1806     cuddRef(t);
1807     if (markE == DD_LIC_NL) {
1808         e = cuddBddLICBuildResult(dd,Fnv,cache,table);
1809         if (e == NULL) {
1810             Cudd_IterDerefBdd(dd,t);
1811             return(NULL);
1812         }
1813     } else if (markE == DD_LIC_1) {
1814         e = one;
1815     } else {
1816         e = zero;
1817     }
1818     cuddRef(e);
1819
1820     if (markT == DD_LIC_DC && markE != DD_LIC_DC) {
1821         r = e;
1822     } else if (markT != DD_LIC_DC && markE == DD_LIC_DC) {
1823         r = t;
1824     } else {
1825         if (Cudd_IsComplement(t)) {
1826             t = Cudd_Not(t);
1827             e = Cudd_Not(e);
1828             r = (t == e) ? t : cuddUniqueInter(dd, index, t, e);
1829             if (r == NULL) {
1830                 Cudd_IterDerefBdd(dd, e);
1831                 Cudd_IterDerefBdd(dd, t);
1832                 return(NULL);
1833             }
1834             r = Cudd_Not(r);
1835         } else {
1836             r = (t == e) ? t : cuddUniqueInter(dd, index, t, e);
1837             if (r == NULL) {
1838                 Cudd_IterDerefBdd(dd, e);
1839                 Cudd_IterDerefBdd(dd, t);
1840                 return(NULL);
1841             }
1842         }
1843     }
1844     cuddDeref(t);
1845     cuddDeref(e);
1846
1847     if (st_insert(cache, (char *)f, (char *)r) == ST_OUT_OF_MEM) {
1848         cuddRef(r);
1849         Cudd_IterDerefBdd(dd,r);
1850         return(NULL);
1851     }
1852
1853     return(Cudd_NotCond(r,comple));
1854
1855 } /* end of cuddBddLICBuildResult */
1856
1857
1858 /**Function********************************************************************
1859
1860   Synopsis    [Hash function for the computed table of cuddBddLICMarkEdges.]
1861
1862   Description [Hash function for the computed table of
1863   cuddBddLICMarkEdges.  Returns the bucket number.]
1864
1865   SideEffects [None]
1866
1867   SeeAlso     [Cudd_bddLICompaction]
1868
1869 ******************************************************************************/
1870 static int
1871 MarkCacheHash(
1872   char * ptr,
1873   int  modulus)
1874 {
1875     int val = 0;
1876     MarkCacheKey *entry;
1877
1878     entry = (MarkCacheKey *) ptr;
1879
1880     val = (int) (ptrint) entry->f;
1881     val = val * 997 + (int) (ptrint) entry->c;
1882
1883     return ((val < 0) ? -val : val) % modulus;
1884
1885 } /* end of MarkCacheHash */
1886
1887
1888 /**Function********************************************************************
1889
1890   Synopsis    [Comparison function for the computed table of
1891   cuddBddLICMarkEdges.]
1892
1893   Description [Comparison function for the computed table of
1894   cuddBddLICMarkEdges. Returns 0 if the two nodes of the key are equal; 1
1895   otherwise.]
1896
1897   SideEffects [None]
1898
1899   SeeAlso     [Cudd_bddLICompaction]
1900
1901 ******************************************************************************/
1902 static int
1903 MarkCacheCompare(
1904   const char * ptr1,
1905   const char * ptr2)
1906 {
1907     MarkCacheKey *entry1, *entry2;
1908
1909     entry1 = (MarkCacheKey *) ptr1;
1910     entry2 = (MarkCacheKey *) ptr2;
1911
1912     return((entry1->f != entry2->f) || (entry1->c != entry2->c));
1913
1914 } /* end of MarkCacheCompare */
1915
1916
1917
1918 /**Function********************************************************************
1919
1920   Synopsis    [Frees memory associated with computed table of
1921   cuddBddLICMarkEdges.]
1922
1923   Description [Frees memory associated with computed table of
1924   cuddBddLICMarkEdges. Returns ST_CONTINUE.]
1925
1926   SideEffects [None]
1927
1928   SeeAlso     [Cudd_bddLICompaction]
1929
1930 ******************************************************************************/
1931 static enum st_retval
1932 MarkCacheCleanUp(
1933   char * key,
1934   char * value,
1935   char * arg)
1936 {
1937     MarkCacheKey *entry;
1938
1939     entry = (MarkCacheKey *) key;
1940     FREE(entry);
1941     return ST_CONTINUE;
1942
1943 } /* end of MarkCacheCleanUp */
1944
1945
1946 /**Function********************************************************************
1947
1948   Synopsis    [Performs the recursive step of Cudd_bddSqueeze.]
1949
1950   Description [Performs the recursive step of Cudd_bddSqueeze.  This
1951   procedure exploits the fact that if we complement and swap the
1952   bounds of the interval we obtain a valid solution by taking the
1953   complement of the solution to the original problem. Therefore, we
1954   can enforce the condition that the upper bound is always regular.
1955   Returns a pointer to the result if successful; NULL otherwise.]
1956
1957   SideEffects [None]
1958
1959   SeeAlso     [Cudd_bddSqueeze]
1960
1961 ******************************************************************************/
1962 static DdNode *
1963 cuddBddSqueeze(
1964   DdManager * dd,
1965   DdNode * l,
1966   DdNode * u)
1967 {
1968     DdNode *one, *zero, *r, *lt, *le, *ut, *ue, *t, *e;
1969 #if 0
1970     DdNode *ar;
1971 #endif
1972     int comple = 0;
1973     unsigned int topu, topl;
1974     int index;
1975
1976     statLine(dd);
1977     if (l == u) {
1978         return(l);
1979     }
1980     one = DD_ONE(dd);
1981     zero = Cudd_Not(one);
1982     /* The only case when l == zero && u == one is at the top level,
1983     ** where returning either one or zero is OK. In all other cases
1984     ** the procedure will detect such a case and will perform
1985     ** remapping. Therefore the order in which we test l and u at this
1986     ** point is immaterial. */
1987     if (l == zero) return(l);
1988     if (u == one)  return(u);
1989
1990     /* Make canonical to increase the utilization of the cache. */
1991     if (Cudd_IsComplement(u)) {
1992         DdNode *temp;
1993         temp = Cudd_Not(l);
1994         l = Cudd_Not(u);
1995         u = temp;
1996         comple = 1;
1997     }
1998     /* At this point u is regular and non-constant; l is non-constant, but
1999     ** may be complemented. */
2000
2001     /* Here we could check the relative sizes. */
2002
2003     /* Check the cache. */
2004     r = cuddCacheLookup2(dd, Cudd_bddSqueeze, l, u);
2005     if (r != NULL) {
2006         return(Cudd_NotCond(r,comple));
2007     }
2008
2009     /* Recursive step. */
2010     topu = dd->perm[u->index];
2011     topl = dd->perm[Cudd_Regular(l)->index];
2012     if (topu <= topl) {
2013         index = u->index;
2014         ut = cuddT(u); ue = cuddE(u);
2015     } else {
2016         index = Cudd_Regular(l)->index;
2017         ut = ue = u;
2018     }
2019     if (topl <= topu) {
2020         lt = cuddT(Cudd_Regular(l)); le = cuddE(Cudd_Regular(l));
2021         if (Cudd_IsComplement(l)) {
2022             lt = Cudd_Not(lt);
2023             le = Cudd_Not(le);
2024         }
2025     } else {
2026         lt = le = l;
2027     }
2028
2029     /* If one interval is contained in the other, use the smaller
2030     ** interval. This corresponds to one-sided matching. */
2031     if ((lt == zero || Cudd_bddLeq(dd,lt,le)) &&
2032         (ut == one  || Cudd_bddLeq(dd,ue,ut))) { /* remap */
2033         r = cuddBddSqueeze(dd, le, ue);
2034         if (r == NULL)
2035             return(NULL);
2036         return(Cudd_NotCond(r,comple));
2037     } else if ((le == zero || Cudd_bddLeq(dd,le,lt)) &&
2038                (ue == one  || Cudd_bddLeq(dd,ut,ue))) { /* remap */
2039         r = cuddBddSqueeze(dd, lt, ut);
2040         if (r == NULL)
2041             return(NULL);
2042         return(Cudd_NotCond(r,comple));
2043     } else if ((le == zero || Cudd_bddLeq(dd,le,Cudd_Not(ut))) &&
2044                (ue == one  || Cudd_bddLeq(dd,Cudd_Not(lt),ue))) { /* c-remap */
2045         t = cuddBddSqueeze(dd, lt, ut);
2046         cuddRef(t);
2047         if (Cudd_IsComplement(t)) {
2048             r = cuddUniqueInter(dd, index, Cudd_Not(t), t);
2049             if (r == NULL) {
2050                 Cudd_IterDerefBdd(dd, t);
2051                 return(NULL);
2052             }
2053             r = Cudd_Not(r);
2054         } else {
2055             r = cuddUniqueInter(dd, index, t, Cudd_Not(t));
2056             if (r == NULL) {
2057                 Cudd_IterDerefBdd(dd, t);
2058                 return(NULL);
2059             }
2060         }
2061         cuddDeref(t);
2062         if (r == NULL)
2063             return(NULL);
2064         cuddCacheInsert2(dd, Cudd_bddSqueeze, l, u, r);
2065         return(Cudd_NotCond(r,comple));
2066     } else if ((lt == zero || Cudd_bddLeq(dd,lt,Cudd_Not(ue))) &&
2067                (ut == one  || Cudd_bddLeq(dd,Cudd_Not(le),ut))) { /* c-remap */
2068         e = cuddBddSqueeze(dd, le, ue);
2069         cuddRef(e);
2070         if (Cudd_IsComplement(e)) {
2071             r = cuddUniqueInter(dd, index, Cudd_Not(e), e);
2072             if (r == NULL) {
2073                 Cudd_IterDerefBdd(dd, e);
2074                 return(NULL);
2075             }
2076         } else {
2077             r = cuddUniqueInter(dd, index, e, Cudd_Not(e));
2078             if (r == NULL) {
2079                 Cudd_IterDerefBdd(dd, e);
2080                 return(NULL);
2081             }
2082             r = Cudd_Not(r);
2083         }
2084         cuddDeref(e);
2085         if (r == NULL)
2086             return(NULL);
2087         cuddCacheInsert2(dd, Cudd_bddSqueeze, l, u, r);
2088         return(Cudd_NotCond(r,comple));
2089     }
2090
2091 #if 0
2092     /* If the two intervals intersect, take a solution from
2093     ** the intersection of the intervals. This guarantees that the
2094     ** splitting variable will not appear in the result.
2095     ** This approach corresponds to two-sided matching, and is very
2096     ** expensive. */
2097     if (Cudd_bddLeq(dd,lt,ue) && Cudd_bddLeq(dd,le,ut)) {
2098         DdNode *au, *al;
2099         au = cuddBddAndRecur(dd,ut,ue);
2100         if (au == NULL)
2101             return(NULL);
2102         cuddRef(au);
2103         al = cuddBddAndRecur(dd,Cudd_Not(lt),Cudd_Not(le));
2104         if (al == NULL) {
2105             Cudd_IterDerefBdd(dd,au);
2106             return(NULL);
2107         }
2108         cuddRef(al);
2109         al = Cudd_Not(al);
2110         ar = cuddBddSqueeze(dd, al, au);
2111         if (ar == NULL) {
2112             Cudd_IterDerefBdd(dd,au);
2113             Cudd_IterDerefBdd(dd,al);
2114             return(NULL);
2115         }
2116         cuddRef(ar);
2117         Cudd_IterDerefBdd(dd,au);
2118         Cudd_IterDerefBdd(dd,al);
2119     } else {
2120         ar = NULL;
2121     }
2122 #endif
2123
2124     t = cuddBddSqueeze(dd, lt, ut);
2125     if (t == NULL) {
2126         return(NULL);
2127     }
2128     cuddRef(t);
2129     e = cuddBddSqueeze(dd, le, ue);
2130     if (e == NULL) {
2131         Cudd_IterDerefBdd(dd,t);
2132         return(NULL);
2133     }
2134     cuddRef(e);
2135
2136     if (Cudd_IsComplement(t)) {
2137         t = Cudd_Not(t);
2138         e = Cudd_Not(e);
2139         r = (t == e) ? t : cuddUniqueInter(dd, index, t, e);
2140         if (r == NULL) {
2141             Cudd_IterDerefBdd(dd, e);
2142             Cudd_IterDerefBdd(dd, t);
2143             return(NULL);
2144         }
2145         r = Cudd_Not(r);
2146     } else {
2147         r = (t == e) ? t : cuddUniqueInter(dd, index, t, e);
2148         if (r == NULL) {
2149             Cudd_IterDerefBdd(dd, e);
2150             Cudd_IterDerefBdd(dd, t);
2151             return(NULL);
2152         }
2153     }
2154     cuddDeref(t);
2155     cuddDeref(e);
2156
2157 #if 0
2158     /* Check whether there is a result obtained by abstraction and whether
2159     ** it is better than the one obtained by recursion. */
2160     cuddRef(r);
2161     if (ar != NULL) {
2162         if (Cudd_DagSize(ar) <= Cudd_DagSize(r)) {
2163             Cudd_IterDerefBdd(dd, r);
2164             r = ar;
2165         } else {
2166             Cudd_IterDerefBdd(dd, ar);
2167         }
2168     }
2169     cuddDeref(r);
2170 #endif
2171
2172     cuddCacheInsert2(dd, Cudd_bddSqueeze, l, u, r);
2173     return(Cudd_NotCond(r,comple));
2174
2175 } /* end of cuddBddSqueeze */