distr/cudd/cuddBridge.c

   1 /**CFile***********************************************************************
   2
   3   FileName    [cuddBridge.c]
   4
   5   PackageName [cudd]
   6
   7   Synopsis    [Translation from BDD to ADD and vice versa and transfer between
   8   different managers.]
   9
  10   Description [External procedures included in this file:
  11             <ul>
  12             <li> Cudd_addBddThreshold()
  13             <li> Cudd_addBddStrictThreshold()
  14             <li> Cudd_addBddInterval()
  15             <li> Cudd_addBddIthBit()
  16             <li> Cudd_BddToAdd()
  17             <li> Cudd_addBddPattern()
  18             <li> Cudd_bddTransfer()
  19             </ul>
  20         Internal procedures included in this file:
  21             <ul>
  22             <li> cuddBddTransfer()
  23             <li> cuddAddBddDoPattern()
  24             </ul>
  25         Static procedures included in this file:
  26             <ul>
  27             <li> addBddDoThreshold()
  28             <li> addBddDoStrictThreshold()
  29             <li> addBddDoInterval()
  30             <li> addBddDoIthBit()
  31             <li> ddBddToAddRecur()
  32             <li> cuddBddTransferRecur()
  33             </ul>
  34             ]
  35
  36   SeeAlso     []
  37
  38   Author      [Fabio Somenzi]
  39
  40   Copyright   [Copyright (c) 1995-2004, Regents of the University of Colorado
  41
  42   All rights reserved.
  43
  44   Redistribution and use in source and binary forms, with or without
  45   modification, are permitted provided that the following conditions
  46   are met:
  47
  48   Redistributions of source code must retain the above copyright
  49   notice, this list of conditions and the following disclaimer.
  50
  51   Redistributions in binary form must reproduce the above copyright
  52   notice, this list of conditions and the following disclaimer in the
  53   documentation and/or other materials provided with the distribution.
  54
  55   Neither the name of the University of Colorado nor the names of its
  56   contributors may be used to endorse or promote products derived from
  57   this software without specific prior written permission.
  58
  59   THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
  60   "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
  61   LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
  62   FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
  63   COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
  64   INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
  65   BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
  66   LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
  67   CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
  68   LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
  69   ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
  70   POSSIBILITY OF SUCH DAMAGE.]
  71
  72 ******************************************************************************/
  73
  74 #include "util.h"
  75 #include "cuddInt.h"
  76
  77 /*---------------------------------------------------------------------------*/
  78 /* Constant declarations                                                     */
  79 /*---------------------------------------------------------------------------*/
  80
  81
  82 /*---------------------------------------------------------------------------*/
  83 /* Stucture declarations                                                     */
  84 /*---------------------------------------------------------------------------*/
  85
  86
  87 /*---------------------------------------------------------------------------*/
  88 /* Type declarations                                                         */
  89 /*---------------------------------------------------------------------------*/
  90
  91
  92 /*---------------------------------------------------------------------------*/
  93 /* Variable declarations                                                     */
  94 /*---------------------------------------------------------------------------*/
  95
  96 #ifndef lint
  97 static char rcsid[] DD_UNUSED = "$Id: cuddBridge.c,v 1.19 2008/04/25 06:42:55 fabio Exp $";
  98 #endif
  99
 100 /*---------------------------------------------------------------------------*/
 101 /* Macro declarations                                                        */
 102 /*---------------------------------------------------------------------------*/
 103
 104
 105 #ifdef __cplusplus
 106 extern "C" {
 107 #endif
 108
 109 /**AutomaticStart*************************************************************/
 110
 111 /*---------------------------------------------------------------------------*/
 112 /* Static function prototypes                                                */
 113 /*---------------------------------------------------------------------------*/
 114
 115 static DdNode * addBddDoThreshold (DdManager *dd, DdNode *f, DdNode *val);
 116 static DdNode * addBddDoStrictThreshold (DdManager *dd, DdNode *f, DdNode *val);
 117 static DdNode * addBddDoInterval (DdManager *dd, DdNode *f, DdNode *l, DdNode *u);
 118 static DdNode * addBddDoIthBit (DdManager *dd, DdNode *f, DdNode *index);
 119 static DdNode * ddBddToAddRecur (DdManager *dd, DdNode *B);
 120 static DdNode * cuddBddTransferRecur (DdManager *ddS, DdManager *ddD, DdNode *f, st_table *table);
 121
 122 /**AutomaticEnd***************************************************************/
 123
 124 #ifdef __cplusplus
 125 }
 126 #endif
 127
 128
 129 /*---------------------------------------------------------------------------*/
 130 /* Definition of exported functions                                          */
 131 /*---------------------------------------------------------------------------*/
 132
 133
 134 /**Function********************************************************************
 135
 136   Synopsis    [Converts an ADD to a BDD.]
 137
 138   Description [Converts an ADD to a BDD by replacing all
 139   discriminants greater than or equal to value with 1, and all other
 140   discriminants with 0. Returns a pointer to the resulting BDD if
 141   successful; NULL otherwise.]
 142
 143   SideEffects [None]
 144
 145   SeeAlso     [Cudd_addBddInterval Cudd_addBddPattern Cudd_BddToAdd
 146   Cudd_addBddStrictThreshold]
 147
 148 ******************************************************************************/
 149 DdNode *
 150 Cudd_addBddThreshold(
 151   DdManager * dd,
 152   DdNode * f,
 153   CUDD_VALUE_TYPE  value)
 154 {
 155     DdNode *res;
 156     DdNode *val;
 157
 158     val = cuddUniqueConst(dd,value);
 159     if (val == NULL) return(NULL);
 160     cuddRef(val);
 161
 162     do {
 163         dd->reordered = 0;
 164         res = addBddDoThreshold(dd, f, val);
 165     } while (dd->reordered == 1);
 166
 167     if (res == NULL) {
 168         Cudd_RecursiveDeref(dd, val);
 169         return(NULL);
 170     }
 171     cuddRef(res);
 172     Cudd_RecursiveDeref(dd, val);
 173     cuddDeref(res);
 174     return(res);
 175
 176 } /* end of Cudd_addBddThreshold */
 177
 178
 179 /**Function********************************************************************
 180
 181   Synopsis    [Converts an ADD to a BDD.]
 182
 183   Description [Converts an ADD to a BDD by replacing all
 184   discriminants STRICTLY greater than value with 1, and all other
 185   discriminants with 0. Returns a pointer to the resulting BDD if
 186   successful; NULL otherwise.]
 187
 188   SideEffects [None]
 189
 190   SeeAlso     [Cudd_addBddInterval Cudd_addBddPattern Cudd_BddToAdd
 191   Cudd_addBddThreshold]
 192
 193 ******************************************************************************/
 194 DdNode *
 195 Cudd_addBddStrictThreshold(
 196   DdManager * dd,
 197   DdNode * f,
 198   CUDD_VALUE_TYPE  value)
 199 {
 200     DdNode *res;
 201     DdNode *val;
 202
 203     val = cuddUniqueConst(dd,value);
 204     if (val == NULL) return(NULL);
 205     cuddRef(val);
 206
 207     do {
 208         dd->reordered = 0;
 209         res = addBddDoStrictThreshold(dd, f, val);
 210     } while (dd->reordered == 1);
 211
 212     if (res == NULL) {
 213         Cudd_RecursiveDeref(dd, val);
 214         return(NULL);
 215     }
 216     cuddRef(res);
 217     Cudd_RecursiveDeref(dd, val);
 218     cuddDeref(res);
 219     return(res);
 220
 221 } /* end of Cudd_addBddStrictThreshold */
 222
 223
 224 /**Function********************************************************************
 225
 226   Synopsis    [Converts an ADD to a BDD.]
 227
 228   Description [Converts an ADD to a BDD by replacing all
 229   discriminants greater than or equal to lower and less than or equal to
 230   upper with 1, and all other discriminants with 0. Returns a pointer to
 231   the resulting BDD if successful; NULL otherwise.]
 232
 233   SideEffects [None]
 234
 235   SeeAlso     [Cudd_addBddThreshold Cudd_addBddStrictThreshold
 236   Cudd_addBddPattern Cudd_BddToAdd]
 237
 238 ******************************************************************************/
 239 DdNode *
 240 Cudd_addBddInterval(
 241   DdManager * dd,
 242   DdNode * f,
 243   CUDD_VALUE_TYPE  lower,
 244   CUDD_VALUE_TYPE  upper)
 245 {
 246     DdNode *res;
 247     DdNode *l;
 248     DdNode *u;
 249
 250     /* Create constant nodes for the interval bounds, so that we can use
 251     ** the global cache.
 252     */
 253     l = cuddUniqueConst(dd,lower);
 254     if (l == NULL) return(NULL);
 255     cuddRef(l);
 256     u = cuddUniqueConst(dd,upper);
 257     if (u == NULL) {
 258         Cudd_RecursiveDeref(dd,l);
 259         return(NULL);
 260     }
 261     cuddRef(u);
 262
 263     do {
 264         dd->reordered = 0;
 265         res = addBddDoInterval(dd, f, l, u);
 266     } while (dd->reordered == 1);
 267
 268     if (res == NULL) {
 269         Cudd_RecursiveDeref(dd, l);
 270         Cudd_RecursiveDeref(dd, u);
 271         return(NULL);
 272     }
 273     cuddRef(res);
 274     Cudd_RecursiveDeref(dd, l);
 275     Cudd_RecursiveDeref(dd, u);
 276     cuddDeref(res);
 277     return(res);
 278
 279 } /* end of Cudd_addBddInterval */
 280
 281
 282 /**Function********************************************************************
 283
 284   Synopsis    [Converts an ADD to a BDD by extracting the i-th bit from
 285   the leaves.]
 286
 287   Description [Converts an ADD to a BDD by replacing all
 288   discriminants whose i-th bit is equal to 1 with 1, and all other
 289   discriminants with 0. The i-th bit refers to the integer
 290   representation of the leaf value. If the value is has a fractional
 291   part, it is ignored. Repeated calls to this procedure allow one to
 292   transform an integer-valued ADD into an array of BDDs, one for each
 293   bit of the leaf values. Returns a pointer to the resulting BDD if
 294   successful; NULL otherwise.]
 295
 296   SideEffects [None]
 297
 298   SeeAlso     [Cudd_addBddInterval Cudd_addBddPattern Cudd_BddToAdd]
 299
 300 ******************************************************************************/
 301 DdNode *
 302 Cudd_addBddIthBit(
 303   DdManager * dd,
 304   DdNode * f,
 305   int  bit)
 306 {
 307     DdNode *res;
 308     DdNode *index;
 309
 310     index = cuddUniqueConst(dd,(CUDD_VALUE_TYPE) bit);
 311     if (index == NULL) return(NULL);
 312     cuddRef(index);
 313
 314     do {
 315         dd->reordered = 0;
 316         res = addBddDoIthBit(dd, f, index);
 317     } while (dd->reordered == 1);
 318
 319     if (res == NULL) {
 320         Cudd_RecursiveDeref(dd, index);
 321         return(NULL);
 322     }
 323     cuddRef(res);
 324     Cudd_RecursiveDeref(dd, index);
 325     cuddDeref(res);
 326     return(res);
 327
 328 } /* end of Cudd_addBddIthBit */
 329
 330
 331 /**Function********************************************************************
 332
 333   Synopsis    [Converts a BDD to a 0-1 ADD.]
 334
 335   Description [Converts a BDD to a 0-1 ADD. Returns a pointer to the
 336   resulting ADD if successful; NULL otherwise.]
 337
 338   SideEffects [None]
 339
 340   SeeAlso     [Cudd_addBddPattern Cudd_addBddThreshold Cudd_addBddInterval
 341   Cudd_addBddStrictThreshold]
 342
 343 ******************************************************************************/
 344 DdNode *
 345 Cudd_BddToAdd(
 346   DdManager * dd,
 347   DdNode * B)
 348 {
 349     DdNode *res;
 350
 351     do {
 352         dd->reordered = 0;
 353         res = ddBddToAddRecur(dd, B);
 354     } while (dd->reordered ==1);
 355     return(res);
 356
 357 } /* end of Cudd_BddToAdd */
 358
 359
 360 /**Function********************************************************************
 361
 362   Synopsis    [Converts an ADD to a BDD.]
 363
 364   Description [Converts an ADD to a BDD by replacing all
 365   discriminants different from 0 with 1. Returns a pointer to the
 366   resulting BDD if successful; NULL otherwise.]
 367
 368   SideEffects [None]
 369
 370   SeeAlso     [Cudd_BddToAdd Cudd_addBddThreshold Cudd_addBddInterval
 371   Cudd_addBddStrictThreshold]
 372
 373 ******************************************************************************/
 374 DdNode *
 375 Cudd_addBddPattern(
 376   DdManager * dd,
 377   DdNode * f)
 378 {
 379     DdNode *res;
 380
 381     do {
 382         dd->reordered = 0;
 383         res = cuddAddBddDoPattern(dd, f);
 384     } while (dd->reordered == 1);
 385     return(res);
 386
 387 } /* end of Cudd_addBddPattern */
 388
 389
 390 /**Function********************************************************************
 391
 392   Synopsis    [Convert a BDD from a manager to another one.]
 393
 394   Description [Convert a BDD from a manager to another one. The orders of the
 395   variables in the two managers may be different. Returns a
 396   pointer to the BDD in the destination manager if successful; NULL
 397   otherwise.]
 398
 399   SideEffects [None]
 400
 401   SeeAlso     []
 402
 403 ******************************************************************************/
 404 DdNode *
 405 Cudd_bddTransfer(
 406   DdManager * ddSource,
 407   DdManager * ddDestination,
 408   DdNode * f)
 409 {
 410     DdNode *res;
 411     do {
 412         ddDestination->reordered = 0;
 413         res = cuddBddTransfer(ddSource, ddDestination, f);
 414     } while (ddDestination->reordered == 1);
 415     return(res);
 416
 417 } /* end of Cudd_bddTransfer */
 418
 419
 420 /*---------------------------------------------------------------------------*/
 421 /* Definition of internal functions                                          */
 422 /*---------------------------------------------------------------------------*/
 423
 424
 425 /**Function********************************************************************
 426
 427   Synopsis    [Convert a BDD from a manager to another one.]
 428
 429   Description [Convert a BDD from a manager to another one. Returns a
 430   pointer to the BDD in the destination manager if successful; NULL
 431   otherwise.]
 432
 433   SideEffects [None]
 434
 435   SeeAlso     [Cudd_bddTransfer]
 436
 437 ******************************************************************************/
 438 DdNode *
 439 cuddBddTransfer(
 440   DdManager * ddS,
 441   DdManager * ddD,
 442   DdNode * f)
 443 {
 444     DdNode *res;
 445     st_table *table = NULL;
 446     st_generator *gen = NULL;
 447     DdNode *key, *value;
 448
 449     table = st_init_table(st_ptrcmp,st_ptrhash);
 450     if (table == NULL) goto failure;
 451     res = cuddBddTransferRecur(ddS, ddD, f, table);
 452     if (res != NULL) cuddRef(res);
 453
 454     /* Dereference all elements in the table and dispose of the table.
 455     ** This must be done also if res is NULL to avoid leaks in case of
 456     ** reordering. */
 457     gen = st_init_gen(table);
 458     if (gen == NULL) goto failure;
 459     while (st_gen(gen, &key, &value)) {
 460         Cudd_RecursiveDeref(ddD, value);
 461     }
 462     st_free_gen(gen); gen = NULL;
 463     st_free_table(table); table = NULL;
 464
 465     if (res != NULL) cuddDeref(res);
 466     return(res);
 467
 468 failure:
 469     /* No need to free gen because it is always NULL here. */
 470     if (table != NULL) st_free_table(table);
 471     return(NULL);
 472
 473 } /* end of cuddBddTransfer */
 474
 475
 476 /**Function********************************************************************
 477
 478   Synopsis    [Performs the recursive step for Cudd_addBddPattern.]
 479
 480   Description [Performs the recursive step for Cudd_addBddPattern. Returns a
 481   pointer to the resulting BDD if successful; NULL otherwise.]
 482
 483   SideEffects [None]
 484
 485   SeeAlso     []
 486
 487 ******************************************************************************/
 488 DdNode *
 489 cuddAddBddDoPattern(
 490   DdManager * dd,
 491   DdNode * f)
 492 {
 493     DdNode *res, *T, *E;
 494     DdNode *fv, *fvn;
 495     int v;
 496
 497     statLine(dd);
 498     /* Check terminal case. */
 499     if (cuddIsConstant(f)) {
 500         return(Cudd_NotCond(DD_ONE(dd),f == DD_ZERO(dd)));
 501     }
 502
 503     /* Check cache. */
 504     res = cuddCacheLookup1(dd,Cudd_addBddPattern,f);
 505     if (res != NULL) return(res);
 506
 507     /* Recursive step. */
 508     v = f->index;
 509     fv = cuddT(f); fvn = cuddE(f);
 510
 511     T = cuddAddBddDoPattern(dd,fv);
 512     if (T == NULL) return(NULL);
 513     cuddRef(T);
 514
 515     E = cuddAddBddDoPattern(dd,fvn);
 516     if (E == NULL) {
 517         Cudd_RecursiveDeref(dd, T);
 518         return(NULL);
 519     }
 520     cuddRef(E);
 521     if (Cudd_IsComplement(T)) {
 522         res = (T == E) ? Cudd_Not(T) : cuddUniqueInter(dd,v,Cudd_Not(T),Cudd_Not(E));
 523         if (res == NULL) {
 524             Cudd_RecursiveDeref(dd, T);
 525             Cudd_RecursiveDeref(dd, E);
 526             return(NULL);
 527         }
 528         res = Cudd_Not(res);
 529     } else {
 530         res = (T == E) ? T : cuddUniqueInter(dd,v,T,E);
 531         if (res == NULL) {
 532             Cudd_RecursiveDeref(dd, T);
 533             Cudd_RecursiveDeref(dd, E);
 534             return(NULL);
 535         }
 536     }
 537     cuddDeref(T);
 538     cuddDeref(E);
 539
 540     /* Store result. */
 541     cuddCacheInsert1(dd,Cudd_addBddPattern,f,res);
 542
 543     return(res);
 544
 545 } /* end of cuddAddBddDoPattern */
 546
 547
 548 /*---------------------------------------------------------------------------*/
 549 /* Definition of static functions                                            */
 550 /*---------------------------------------------------------------------------*/
 551
 552
 553 /**Function********************************************************************
 554
 555   Synopsis    [Performs the recursive step for Cudd_addBddThreshold.]
 556
 557   Description [Performs the recursive step for Cudd_addBddThreshold.
 558   Returns a pointer to the BDD if successful; NULL otherwise.]
 559
 560   SideEffects [None]
 561
 562   SeeAlso     [addBddDoStrictThreshold]
 563
 564 ******************************************************************************/
 565 static DdNode *
 566 addBddDoThreshold(
 567   DdManager * dd,
 568   DdNode * f,
 569   DdNode * val)
 570 {
 571     DdNode *res, *T, *E;
 572     DdNode *fv, *fvn;
 573     int v;
 574
 575     statLine(dd);
 576     /* Check terminal case. */
 577     if (cuddIsConstant(f)) {
 578         return(Cudd_NotCond(DD_ONE(dd),cuddV(f) < cuddV(val)));
 579     }
 580
 581     /* Check cache. */
 582     res = cuddCacheLookup2(dd,addBddDoThreshold,f,val);
 583     if (res != NULL) return(res);
 584
 585     /* Recursive step. */
 586     v = f->index;
 587     fv = cuddT(f); fvn = cuddE(f);
 588
 589     T = addBddDoThreshold(dd,fv,val);
 590     if (T == NULL) return(NULL);
 591     cuddRef(T);
 592
 593     E = addBddDoThreshold(dd,fvn,val);
 594     if (E == NULL) {
 595         Cudd_RecursiveDeref(dd, T);
 596         return(NULL);
 597     }
 598     cuddRef(E);
 599     if (Cudd_IsComplement(T)) {
 600         res = (T == E) ? Cudd_Not(T) : cuddUniqueInter(dd,v,Cudd_Not(T),Cudd_Not(E));
 601         if (res == NULL) {
 602             Cudd_RecursiveDeref(dd, T);
 603             Cudd_RecursiveDeref(dd, E);
 604             return(NULL);
 605         }
 606         res = Cudd_Not(res);
 607     } else {
 608         res = (T == E) ? T : cuddUniqueInter(dd,v,T,E);
 609         if (res == NULL) {
 610             Cudd_RecursiveDeref(dd, T);
 611             Cudd_RecursiveDeref(dd, E);
 612             return(NULL);
 613         }
 614     }
 615     cuddDeref(T);
 616     cuddDeref(E);
 617
 618     /* Store result. */
 619     cuddCacheInsert2(dd,addBddDoThreshold,f,val,res);
 620
 621     return(res);
 622
 623 } /* end of addBddDoThreshold */
 624
 625
 626 /**Function********************************************************************
 627
 628   Synopsis    [Performs the recursive step for Cudd_addBddStrictThreshold.]
 629
 630   Description [Performs the recursive step for Cudd_addBddStrictThreshold.
 631   Returns a pointer to the BDD if successful; NULL otherwise.]
 632
 633   SideEffects [None]
 634
 635   SeeAlso     [addBddDoThreshold]
 636
 637 ******************************************************************************/
 638 static DdNode *
 639 addBddDoStrictThreshold(
 640   DdManager * dd,
 641   DdNode * f,
 642   DdNode * val)
 643 {
 644     DdNode *res, *T, *E;
 645     DdNode *fv, *fvn;
 646     int v;
 647
 648     statLine(dd);
 649     /* Check terminal case. */
 650     if (cuddIsConstant(f)) {
 651         return(Cudd_NotCond(DD_ONE(dd),cuddV(f) <= cuddV(val)));
 652     }
 653
 654     /* Check cache. */
 655     res = cuddCacheLookup2(dd,addBddDoStrictThreshold,f,val);
 656     if (res != NULL) return(res);
 657
 658     /* Recursive step. */
 659     v = f->index;
 660     fv = cuddT(f); fvn = cuddE(f);
 661
 662     T = addBddDoStrictThreshold(dd,fv,val);
 663     if (T == NULL) return(NULL);
 664     cuddRef(T);
 665
 666     E = addBddDoStrictThreshold(dd,fvn,val);
 667     if (E == NULL) {
 668         Cudd_RecursiveDeref(dd, T);
 669         return(NULL);
 670     }
 671     cuddRef(E);
 672     if (Cudd_IsComplement(T)) {
 673         res = (T == E) ? Cudd_Not(T) : cuddUniqueInter(dd,v,Cudd_Not(T),Cudd_Not(E));
 674         if (res == NULL) {
 675             Cudd_RecursiveDeref(dd, T);
 676             Cudd_RecursiveDeref(dd, E);
 677             return(NULL);
 678         }
 679         res = Cudd_Not(res);
 680     } else {
 681         res = (T == E) ? T : cuddUniqueInter(dd,v,T,E);
 682         if (res == NULL) {
 683             Cudd_RecursiveDeref(dd, T);
 684             Cudd_RecursiveDeref(dd, E);
 685             return(NULL);
 686         }
 687     }
 688     cuddDeref(T);
 689     cuddDeref(E);
 690
 691     /* Store result. */
 692     cuddCacheInsert2(dd,addBddDoStrictThreshold,f,val,res);
 693
 694     return(res);
 695
 696 } /* end of addBddDoStrictThreshold */
 697
 698
 699 /**Function********************************************************************
 700
 701   Synopsis    [Performs the recursive step for Cudd_addBddInterval.]
 702
 703   Description [Performs the recursive step for Cudd_addBddInterval.
 704   Returns a pointer to the BDD if successful; NULL otherwise.]
 705
 706   SideEffects [None]
 707
 708   SeeAlso     [addBddDoThreshold addBddDoStrictThreshold]
 709
 710 ******************************************************************************/
 711 static DdNode *
 712 addBddDoInterval(
 713   DdManager * dd,
 714   DdNode * f,
 715   DdNode * l,
 716   DdNode * u)
 717 {
 718     DdNode *res, *T, *E;
 719     DdNode *fv, *fvn;
 720     int v;
 721
 722     statLine(dd);
 723     /* Check terminal case. */
 724     if (cuddIsConstant(f)) {
 725         return(Cudd_NotCond(DD_ONE(dd),cuddV(f) < cuddV(l) || cuddV(f) > cuddV(u)));
 726     }
 727
 728     /* Check cache. */
 729     res = cuddCacheLookup(dd,DD_ADD_BDD_DO_INTERVAL_TAG,f,l,u);
 730     if (res != NULL) return(res);
 731
 732     /* Recursive step. */
 733     v = f->index;
 734     fv = cuddT(f); fvn = cuddE(f);
 735
 736     T = addBddDoInterval(dd,fv,l,u);
 737     if (T == NULL) return(NULL);
 738     cuddRef(T);
 739
 740     E = addBddDoInterval(dd,fvn,l,u);
 741     if (E == NULL) {
 742         Cudd_RecursiveDeref(dd, T);
 743         return(NULL);
 744     }
 745     cuddRef(E);
 746     if (Cudd_IsComplement(T)) {
 747         res = (T == E) ? Cudd_Not(T) : cuddUniqueInter(dd,v,Cudd_Not(T),Cudd_Not(E));
 748         if (res == NULL) {
 749             Cudd_RecursiveDeref(dd, T);
 750             Cudd_RecursiveDeref(dd, E);
 751             return(NULL);
 752         }
 753         res = Cudd_Not(res);
 754     } else {
 755         res = (T == E) ? T : cuddUniqueInter(dd,v,T,E);
 756         if (res == NULL) {
 757             Cudd_RecursiveDeref(dd, T);
 758             Cudd_RecursiveDeref(dd, E);
 759             return(NULL);
 760         }
 761     }
 762     cuddDeref(T);
 763     cuddDeref(E);
 764
 765     /* Store result. */
 766     cuddCacheInsert(dd,DD_ADD_BDD_DO_INTERVAL_TAG,f,l,u,res);
 767
 768     return(res);
 769
 770 } /* end of addBddDoInterval */
 771
 772
 773 /**Function********************************************************************
 774
 775   Synopsis    [Performs the recursive step for Cudd_addBddIthBit.]
 776
 777   Description [Performs the recursive step for Cudd_addBddIthBit.
 778   Returns a pointer to the BDD if successful; NULL otherwise.]
 779
 780   SideEffects [None]
 781
 782   SeeAlso     []
 783
 784 ******************************************************************************/
 785 static DdNode *
 786 addBddDoIthBit(
 787   DdManager * dd,
 788   DdNode * f,
 789   DdNode * index)
 790 {
 791     DdNode *res, *T, *E;
 792     DdNode *fv, *fvn;
 793     int mask, value;
 794     int v;
 795
 796     statLine(dd);
 797     /* Check terminal case. */
 798     if (cuddIsConstant(f)) {
 799         mask = 1 << ((int) cuddV(index));
 800         value = (int) cuddV(f);
 801         return(Cudd_NotCond(DD_ONE(dd),(value & mask) == 0));
 802     }
 803
 804     /* Check cache. */
 805     res = cuddCacheLookup2(dd,addBddDoIthBit,f,index);
 806     if (res != NULL) return(res);
 807
 808     /* Recursive step. */
 809     v = f->index;
 810     fv = cuddT(f); fvn = cuddE(f);
 811
 812     T = addBddDoIthBit(dd,fv,index);
 813     if (T == NULL) return(NULL);
 814     cuddRef(T);
 815
 816     E = addBddDoIthBit(dd,fvn,index);
 817     if (E == NULL) {
 818         Cudd_RecursiveDeref(dd, T);
 819         return(NULL);
 820     }
 821     cuddRef(E);
 822     if (Cudd_IsComplement(T)) {
 823         res = (T == E) ? Cudd_Not(T) : cuddUniqueInter(dd,v,Cudd_Not(T),Cudd_Not(E));
 824         if (res == NULL) {
 825             Cudd_RecursiveDeref(dd, T);
 826             Cudd_RecursiveDeref(dd, E);
 827             return(NULL);
 828         }
 829         res = Cudd_Not(res);
 830     } else {
 831         res = (T == E) ? T : cuddUniqueInter(dd,v,T,E);
 832         if (res == NULL) {
 833             Cudd_RecursiveDeref(dd, T);
 834             Cudd_RecursiveDeref(dd, E);
 835             return(NULL);
 836         }
 837     }
 838     cuddDeref(T);
 839     cuddDeref(E);
 840
 841     /* Store result. */
 842     cuddCacheInsert2(dd,addBddDoIthBit,f,index,res);
 843
 844     return(res);
 845
 846 } /* end of addBddDoIthBit */
 847
 848
 849 /**Function********************************************************************
 850
 851   Synopsis    [Performs the recursive step for Cudd_BddToAdd.]
 852
 853   Description [Performs the recursive step for Cudd_BddToAdd. Returns a
 854   pointer to the resulting ADD if successful; NULL otherwise.]
 855
 856   SideEffects [None]
 857
 858   SeeAlso     []
 859
 860 ******************************************************************************/
 861 static DdNode *
 862 ddBddToAddRecur(
 863   DdManager * dd,
 864   DdNode * B)
 865 {
 866     DdNode *one;
 867     DdNode *res, *res1, *T, *E, *Bt, *Be;
 868     int complement = 0;
 869
 870     statLine(dd);
 871     one = DD_ONE(dd);
 872
 873     if (Cudd_IsConstant(B)) {
 874         if (B == one) {
 875             res = one;
 876         } else {
 877             res = DD_ZERO(dd);
 878         }
 879         return(res);
 880     }
 881     /* Check visited table */
 882     res = cuddCacheLookup1(dd,ddBddToAddRecur,B);
 883     if (res != NULL) return(res);
 884
 885     if (Cudd_IsComplement(B)) {
 886         complement = 1;
 887         Bt = cuddT(Cudd_Regular(B));
 888         Be = cuddE(Cudd_Regular(B));
 889     } else {
 890         Bt = cuddT(B);
 891         Be = cuddE(B);
 892     }
 893
 894     T = ddBddToAddRecur(dd, Bt);
 895     if (T == NULL) return(NULL);
 896     cuddRef(T);
 897
 898     E = ddBddToAddRecur(dd, Be);
 899     if (E == NULL) {
 900         Cudd_RecursiveDeref(dd, T);
 901         return(NULL);
 902     }
 903     cuddRef(E);
 904
 905     /* No need to check for T == E, because it is guaranteed not to happen. */
 906     res = cuddUniqueInter(dd, (int) Cudd_Regular(B)->index, T, E);
 907     if (res == NULL) {
 908         Cudd_RecursiveDeref(dd ,T);
 909         Cudd_RecursiveDeref(dd ,E);
 910         return(NULL);
 911     }
 912     cuddDeref(T);
 913     cuddDeref(E);
 914
 915     if (complement) {
 916         cuddRef(res);
 917         res1 = cuddAddCmplRecur(dd, res);
 918         if (res1 == NULL) {
 919             Cudd_RecursiveDeref(dd, res);
 920             return(NULL);
 921         }
 922         cuddRef(res1);
 923         Cudd_RecursiveDeref(dd, res);
 924         res = res1;
 925         cuddDeref(res);
 926     }
 927
 928     /* Store result. */
 929     cuddCacheInsert1(dd,ddBddToAddRecur,B,res);
 930
 931     return(res);
 932
 933 } /* end of ddBddToAddRecur */
 934
 935
 936 /**Function********************************************************************
 937
 938   Synopsis    [Performs the recursive step of Cudd_bddTransfer.]
 939
 940   Description [Performs the recursive step of Cudd_bddTransfer.
 941   Returns a pointer to the result if successful; NULL otherwise.]
 942
 943   SideEffects [None]
 944
 945   SeeAlso     [cuddBddTransfer]
 946
 947 ******************************************************************************/
 948 static DdNode *
 949 cuddBddTransferRecur(
 950   DdManager * ddS,
 951   DdManager * ddD,
 952   DdNode * f,
 953   st_table * table)
 954 {
 955     DdNode *ft, *fe, *t, *e, *var, *res;
 956     DdNode *one, *zero;
 957     int    index;
 958     int    comple = 0;
 959
 960     statLine(ddD);
 961     one = DD_ONE(ddD);
 962     comple = Cudd_IsComplement(f);
 963
 964     /* Trivial cases. */
 965     if (Cudd_IsConstant(f)) return(Cudd_NotCond(one, comple));
 966
 967     /* Make canonical to increase the utilization of the cache. */
 968     f = Cudd_NotCond(f,comple);
 969     /* Now f is a regular pointer to a non-constant node. */
 970
 971     /* Check the cache. */
 972     if (st_lookup(table, f, &res))
 973         return(Cudd_NotCond(res,comple));
 974
 975     /* Recursive step. */
 976     index = f->index;
 977     ft = cuddT(f); fe = cuddE(f);
 978
 979     t = cuddBddTransferRecur(ddS, ddD, ft, table);
 980     if (t == NULL) {
 981         return(NULL);
 982     }
 983     cuddRef(t);
 984
 985     e = cuddBddTransferRecur(ddS, ddD, fe, table);
 986     if (e == NULL) {
 987         Cudd_RecursiveDeref(ddD, t);
 988         return(NULL);
 989     }
 990     cuddRef(e);
 991
 992     zero = Cudd_Not(one);
 993     var = cuddUniqueInter(ddD,index,one,zero);
 994     if (var == NULL) {
 995         Cudd_RecursiveDeref(ddD, t);
 996         Cudd_RecursiveDeref(ddD, e);
 997         return(NULL);
 998     }
 999     res = cuddBddIteRecur(ddD,var,t,e);
1000     if (res == NULL) {
1001         Cudd_RecursiveDeref(ddD, t);
1002         Cudd_RecursiveDeref(ddD, e);
1003         return(NULL);
1004     }
1005     cuddRef(res);
1006     Cudd_RecursiveDeref(ddD, t);
1007     Cudd_RecursiveDeref(ddD, e);
1008
1009     if (st_add_direct(table, (char *) f, (char *) res) == ST_OUT_OF_MEM) {
1010         Cudd_RecursiveDeref(ddD, res);
1011         return(NULL);
1012     }
1013     return(Cudd_NotCond(res,comple));
1014
1015 } /* end of cuddBddTransferRecur */
1016