distr/cudd/cuddAddApply.c

   1 /**CFile***********************************************************************
   2
   3   FileName    [cuddAddApply.c]
   4
   5   PackageName [cudd]
   6
   7   Synopsis    [Apply functions for ADDs and their operators.]
   8
   9   Description [External procedures included in this module:
  10                 <ul>
  11                 <li> Cudd_addApply()
  12                 <li> Cudd_addMonadicApply()
  13                 <li> Cudd_addPlus()
  14                 <li> Cudd_addTimes()
  15                 <li> Cudd_addThreshold()
  16                 <li> Cudd_addSetNZ()
  17                 <li> Cudd_addDivide()
  18                 <li> Cudd_addMinus()
  19                 <li> Cudd_addMinimum()
  20                 <li> Cudd_addMaximum()
  21                 <li> Cudd_addOneZeroMaximum()
  22                 <li> Cudd_addDiff()
  23                 <li> Cudd_addAgreement()
  24                 <li> Cudd_addOr()
  25                 <li> Cudd_addNand()
  26                 <li> Cudd_addNor()
  27                 <li> Cudd_addXor()
  28                 <li> Cudd_addXnor()
  29                 </ul>
  30             Internal procedures included in this module:
  31                 <ul>
  32                 <li> cuddAddApplyRecur()
  33                 <li> cuddAddMonadicApplyRecur()
  34                 </ul>]
  35
  36   Author      [Fabio Somenzi]
  37
  38   Copyright   [Copyright (c) 1995-2004, Regents of the University of Colorado
  39
  40   All rights reserved.
  41
  42   Redistribution and use in source and binary forms, with or without
  43   modification, are permitted provided that the following conditions
  44   are met:
  45
  46   Redistributions of source code must retain the above copyright
  47   notice, this list of conditions and the following disclaimer.
  48
  49   Redistributions in binary form must reproduce the above copyright
  50   notice, this list of conditions and the following disclaimer in the
  51   documentation and/or other materials provided with the distribution.
  52
  53   Neither the name of the University of Colorado nor the names of its
  54   contributors may be used to endorse or promote products derived from
  55   this software without specific prior written permission.
  56
  57   THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
  58   "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
  59   LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
  60   FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
  61   COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
  62   INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
  63   BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
  64   LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
  65   CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
  66   LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
  67   ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
  68   POSSIBILITY OF SUCH DAMAGE.]
  69
  70 ******************************************************************************/
  71
  72 #include "util.h"
  73 #include "cuddInt.h"
  74
  75 /*---------------------------------------------------------------------------*/
  76 /* Constant declarations                                                     */
  77 /*---------------------------------------------------------------------------*/
  78
  79
  80 /*---------------------------------------------------------------------------*/
  81 /* Stucture declarations                                                     */
  82 /*---------------------------------------------------------------------------*/
  83
  84
  85 /*---------------------------------------------------------------------------*/
  86 /* Type declarations                                                         */
  87 /*---------------------------------------------------------------------------*/
  88
  89
  90 /*---------------------------------------------------------------------------*/
  91 /* Variable declarations                                                     */
  92 /*---------------------------------------------------------------------------*/
  93
  94 #ifndef lint
  95 static char rcsid[] DD_UNUSED = "$Id: cuddAddApply.c,v 1.18 2009/02/19 16:15:26 fabio Exp $";
  96 #endif
  97
  98
  99 /*---------------------------------------------------------------------------*/
 100 /* Macro declarations                                                        */
 101 /*---------------------------------------------------------------------------*/
 102
 103
 104 /**AutomaticStart*************************************************************/
 105
 106 /*---------------------------------------------------------------------------*/
 107 /* Static function prototypes                                                */
 108 /*---------------------------------------------------------------------------*/
 109
 110
 111 /**AutomaticEnd***************************************************************/
 112
 113
 114 /*---------------------------------------------------------------------------*/
 115 /* Definition of exported functions                                          */
 116 /*---------------------------------------------------------------------------*/
 117
 118 /**Function********************************************************************
 119
 120   Synopsis    [Applies op to the corresponding discriminants of f and g.]
 121
 122   Description [Applies op to the corresponding discriminants of f and g.
 123   Returns a pointer to the result if succssful; NULL otherwise.]
 124
 125   SideEffects [None]
 126
 127   SeeAlso     [Cudd_addMonadicApply Cudd_addPlus Cudd_addTimes
 128   Cudd_addThreshold Cudd_addSetNZ Cudd_addDivide Cudd_addMinus Cudd_addMinimum
 129   Cudd_addMaximum Cudd_addOneZeroMaximum Cudd_addDiff Cudd_addAgreement
 130   Cudd_addOr Cudd_addNand Cudd_addNor Cudd_addXor Cudd_addXnor]
 131
 132 ******************************************************************************/
 133 DdNode *
 134 Cudd_addApply(
 135   DdManager * dd,
 136   DD_AOP op,
 137   DdNode * f,
 138   DdNode * g)
 139 {
 140     DdNode *res;
 141
 142     do {
 143         dd->reordered = 0;
 144         res = cuddAddApplyRecur(dd,op,f,g);
 145     } while (dd->reordered == 1);
 146     return(res);
 147
 148 } /* end of Cudd_addApply */
 149
 150
 151 /**Function********************************************************************
 152
 153   Synopsis    [Integer and floating point addition.]
 154
 155   Description [Integer and floating point addition. Returns NULL if not
 156   a terminal case; f+g otherwise.]
 157
 158   SideEffects [None]
 159
 160   SeeAlso     [Cudd_addApply]
 161
 162 ******************************************************************************/
 163 DdNode *
 164 Cudd_addPlus(
 165   DdManager * dd,
 166   DdNode ** f,
 167   DdNode ** g)
 168 {
 169     DdNode *res;
 170     DdNode *F, *G;
 171     CUDD_VALUE_TYPE value;
 172
 173     F = *f; G = *g;
 174     if (F == DD_ZERO(dd)) return(G);
 175     if (G == DD_ZERO(dd)) return(F);
 176     if (cuddIsConstant(F) && cuddIsConstant(G)) {
 177         value = cuddV(F)+cuddV(G);
 178         res = cuddUniqueConst(dd,value);
 179         return(res);
 180     }
 181     if (F > G) { /* swap f and g */
 182         *f = G;
 183         *g = F;
 184     }
 185     return(NULL);
 186
 187 } /* end of Cudd_addPlus */
 188
 189
 190 /**Function********************************************************************
 191
 192   Synopsis    [Integer and floating point multiplication.]
 193
 194   Description [Integer and floating point multiplication. Returns NULL
 195   if not a terminal case; f * g otherwise.  This function can be used also
 196   to take the AND of two 0-1 ADDs.]
 197
 198   SideEffects [None]
 199
 200   SeeAlso     [Cudd_addApply]
 201
 202 ******************************************************************************/
 203 DdNode *
 204 Cudd_addTimes(
 205   DdManager * dd,
 206   DdNode ** f,
 207   DdNode ** g)
 208 {
 209     DdNode *res;
 210     DdNode *F, *G;
 211     CUDD_VALUE_TYPE value;
 212
 213     F = *f; G = *g;
 214     if (F == DD_ZERO(dd) || G == DD_ZERO(dd)) return(DD_ZERO(dd));
 215     if (F == DD_ONE(dd)) return(G);
 216     if (G == DD_ONE(dd)) return(F);
 217     if (cuddIsConstant(F) && cuddIsConstant(G)) {
 218         value = cuddV(F)*cuddV(G);
 219         res = cuddUniqueConst(dd,value);
 220         return(res);
 221     }
 222     if (F > G) { /* swap f and g */
 223         *f = G;
 224         *g = F;
 225     }
 226     return(NULL);
 227
 228 } /* end of Cudd_addTimes */
 229
 230
 231 /**Function********************************************************************
 232
 233   Synopsis    [f if f&gt;=g; 0 if f&lt;g.]
 234
 235   Description [Threshold operator for Apply (f if f &gt;=g; 0 if f&lt;g).
 236   Returns NULL if not a terminal case; f op g otherwise.]
 237
 238   SideEffects [None]
 239
 240   SeeAlso     [Cudd_addApply]
 241
 242 ******************************************************************************/
 243 DdNode *
 244 Cudd_addThreshold(
 245   DdManager * dd,
 246   DdNode ** f,
 247   DdNode ** g)
 248 {
 249     DdNode *F, *G;
 250
 251     F = *f; G = *g;
 252     if (F == G || F == DD_PLUS_INFINITY(dd)) return(F);
 253     if (cuddIsConstant(F) && cuddIsConstant(G)) {
 254         if (cuddV(F) >= cuddV(G)) {
 255             return(F);
 256         } else {
 257             return(DD_ZERO(dd));
 258         }
 259     }
 260     return(NULL);
 261
 262 } /* end of Cudd_addThreshold */
 263
 264
 265 /**Function********************************************************************
 266
 267   Synopsis    [This operator sets f to the value of g wherever g != 0.]
 268
 269   Description [This operator sets f to the value of g wherever g != 0.
 270   Returns NULL if not a terminal case; f op g otherwise.]
 271
 272   SideEffects [None]
 273
 274   SeeAlso     [Cudd_addApply]
 275
 276 ******************************************************************************/
 277 DdNode *
 278 Cudd_addSetNZ(
 279   DdManager * dd,
 280   DdNode ** f,
 281   DdNode ** g)
 282 {
 283     DdNode *F, *G;
 284
 285     F = *f; G = *g;
 286     if (F == G) return(F);
 287     if (F == DD_ZERO(dd)) return(G);
 288     if (G == DD_ZERO(dd)) return(F);
 289     if (cuddIsConstant(G)) return(G);
 290     return(NULL);
 291
 292 } /* end of Cudd_addSetNZ */
 293
 294
 295 /**Function********************************************************************
 296
 297   Synopsis    [Integer and floating point division.]
 298
 299   Description [Integer and floating point division. Returns NULL if not
 300   a terminal case; f / g otherwise.]
 301
 302   SideEffects [None]
 303
 304   SeeAlso     [Cudd_addApply]
 305
 306 ******************************************************************************/
 307 DdNode *
 308 Cudd_addDivide(
 309   DdManager * dd,
 310   DdNode ** f,
 311   DdNode ** g)
 312 {
 313     DdNode *res;
 314     DdNode *F, *G;
 315     CUDD_VALUE_TYPE value;
 316
 317     F = *f; G = *g;
 318     /* We would like to use F == G -> F/G == 1, but F and G may
 319     ** contain zeroes. */
 320     if (F == DD_ZERO(dd)) return(DD_ZERO(dd));
 321     if (G == DD_ONE(dd)) return(F);
 322     if (cuddIsConstant(F) && cuddIsConstant(G)) {
 323         value = cuddV(F)/cuddV(G);
 324         res = cuddUniqueConst(dd,value);
 325         return(res);
 326     }
 327     return(NULL);
 328
 329 } /* end of Cudd_addDivide */
 330
 331
 332 /**Function********************************************************************
 333
 334   Synopsis    [Integer and floating point subtraction.]
 335
 336   Description [Integer and floating point subtraction. Returns NULL if
 337   not a terminal case; f - g otherwise.]
 338
 339   SideEffects [None]
 340
 341   SeeAlso     [Cudd_addApply]
 342
 343 ******************************************************************************/
 344 DdNode *
 345 Cudd_addMinus(
 346   DdManager * dd,
 347   DdNode ** f,
 348   DdNode ** g)
 349 {
 350     DdNode *res;
 351     DdNode *F, *G;
 352     CUDD_VALUE_TYPE value;
 353
 354     F = *f; G = *g;
 355     if (F == G) return(DD_ZERO(dd));
 356     if (F == DD_ZERO(dd)) return(cuddAddNegateRecur(dd,G));
 357     if (G == DD_ZERO(dd)) return(F);
 358     if (cuddIsConstant(F) && cuddIsConstant(G)) {
 359         value = cuddV(F)-cuddV(G);
 360         res = cuddUniqueConst(dd,value);
 361         return(res);
 362     }
 363     return(NULL);
 364
 365 } /* end of Cudd_addMinus */
 366
 367
 368 /**Function********************************************************************
 369
 370   Synopsis    [Integer and floating point min.]
 371
 372   Description [Integer and floating point min for Cudd_addApply.
 373   Returns NULL if not a terminal case; min(f,g) otherwise.]
 374
 375   SideEffects [None]
 376
 377   SeeAlso     [Cudd_addApply]
 378
 379 ******************************************************************************/
 380 DdNode *
 381 Cudd_addMinimum(
 382   DdManager * dd,
 383   DdNode ** f,
 384   DdNode ** g)
 385 {
 386     DdNode *F, *G;
 387
 388     F = *f; G = *g;
 389     if (F == DD_PLUS_INFINITY(dd)) return(G);
 390     if (G == DD_PLUS_INFINITY(dd)) return(F);
 391     if (F == G) return(F);
 392 #if 0
 393     /* These special cases probably do not pay off. */
 394     if (F == DD_MINUS_INFINITY(dd)) return(F);
 395     if (G == DD_MINUS_INFINITY(dd)) return(G);
 396 #endif
 397     if (cuddIsConstant(F) && cuddIsConstant(G)) {
 398         if (cuddV(F) <= cuddV(G)) {
 399             return(F);
 400         } else {
 401             return(G);
 402         }
 403     }
 404     if (F > G) { /* swap f and g */
 405         *f = G;
 406         *g = F;
 407     }
 408     return(NULL);
 409
 410 } /* end of Cudd_addMinimum */
 411
 412
 413 /**Function********************************************************************
 414
 415   Synopsis    [Integer and floating point max.]
 416
 417   Description [Integer and floating point max for Cudd_addApply.
 418   Returns NULL if not a terminal case; max(f,g) otherwise.]
 419
 420   SideEffects [None]
 421
 422   SeeAlso     [Cudd_addApply]
 423
 424 ******************************************************************************/
 425 DdNode *
 426 Cudd_addMaximum(
 427   DdManager * dd,
 428   DdNode ** f,
 429   DdNode ** g)
 430 {
 431     DdNode *F, *G;
 432
 433     F = *f; G = *g;
 434     if (F == G) return(F);
 435     if (F == DD_MINUS_INFINITY(dd)) return(G);
 436     if (G == DD_MINUS_INFINITY(dd)) return(F);
 437 #if 0
 438     /* These special cases probably do not pay off. */
 439     if (F == DD_PLUS_INFINITY(dd)) return(F);
 440     if (G == DD_PLUS_INFINITY(dd)) return(G);
 441 #endif
 442     if (cuddIsConstant(F) && cuddIsConstant(G)) {
 443         if (cuddV(F) >= cuddV(G)) {
 444             return(F);
 445         } else {
 446             return(G);
 447         }
 448     }
 449     if (F > G) { /* swap f and g */
 450         *f = G;
 451         *g = F;
 452     }
 453     return(NULL);
 454
 455 } /* end of Cudd_addMaximum */
 456
 457
 458 /**Function********************************************************************
 459
 460   Synopsis    [Returns 1 if f &gt; g and 0 otherwise.]
 461
 462   Description [Returns 1 if f &gt; g and 0 otherwise. Used in
 463   conjunction with Cudd_addApply. Returns NULL if not a terminal
 464   case.]
 465
 466   SideEffects [None]
 467
 468   SeeAlso     [Cudd_addApply]
 469
 470 ******************************************************************************/
 471 DdNode *
 472 Cudd_addOneZeroMaximum(
 473   DdManager * dd,
 474   DdNode ** f,
 475   DdNode ** g)
 476 {
 477
 478     if (*f == *g) return(DD_ZERO(dd));
 479     if (*g == DD_PLUS_INFINITY(dd))
 480         return DD_ZERO(dd);
 481     if (cuddIsConstant(*f) && cuddIsConstant(*g)) {
 482         if (cuddV(*f) > cuddV(*g)) {
 483             return(DD_ONE(dd));
 484         } else {
 485             return(DD_ZERO(dd));
 486         }
 487     }
 488
 489     return(NULL);
 490
 491 } /* end of Cudd_addOneZeroMaximum */
 492
 493
 494 /**Function********************************************************************
 495
 496   Synopsis    [Returns plusinfinity if f=g; returns min(f,g) if f!=g.]
 497
 498   Description [Returns NULL if not a terminal case; f op g otherwise,
 499   where f op g is plusinfinity if f=g; min(f,g) if f!=g.]
 500
 501   SideEffects [None]
 502
 503   SeeAlso     [Cudd_addApply]
 504
 505 ******************************************************************************/
 506 DdNode *
 507 Cudd_addDiff(
 508   DdManager * dd,
 509   DdNode ** f,
 510   DdNode ** g)
 511 {
 512     DdNode *F, *G;
 513
 514     F = *f; G = *g;
 515     if (F == G) return(DD_PLUS_INFINITY(dd));
 516     if (F == DD_PLUS_INFINITY(dd)) return(G);
 517     if (G == DD_PLUS_INFINITY(dd)) return(F);
 518     if (cuddIsConstant(F) && cuddIsConstant(G)) {
 519         if (cuddV(F) != cuddV(G)) {
 520             if (cuddV(F) < cuddV(G)) {
 521                 return(F);
 522             } else {
 523                 return(G);
 524             }
 525         } else {
 526             return(DD_PLUS_INFINITY(dd));
 527         }
 528     }
 529     return(NULL);
 530
 531 } /* end of Cudd_addDiff */
 532
 533
 534 /**Function********************************************************************
 535
 536   Synopsis    [f if f==g; background if f!=g.]
 537
 538   Description [Returns NULL if not a terminal case; f op g otherwise,
 539   where f op g is f if f==g; background if f!=g.]
 540
 541   SideEffects [None]
 542
 543   SeeAlso     [Cudd_addApply]
 544
 545 ******************************************************************************/
 546 DdNode *
 547 Cudd_addAgreement(
 548   DdManager * dd,
 549   DdNode ** f,
 550   DdNode ** g)
 551 {
 552     DdNode *F, *G;
 553
 554     F = *f; G = *g;
 555     if (F == G) return(F);
 556     if (F == dd->background) return(F);
 557     if (G == dd->background) return(G);
 558     if (cuddIsConstant(F) && cuddIsConstant(G)) return(dd->background);
 559     return(NULL);
 560
 561 } /* end of Cudd_addAgreement */
 562
 563
 564 /**Function********************************************************************
 565
 566   Synopsis    [Disjunction of two 0-1 ADDs.]
 567
 568   Description [Disjunction of two 0-1 ADDs. Returns NULL
 569   if not a terminal case; f OR g otherwise.]
 570
 571   SideEffects [None]
 572
 573   SeeAlso     [Cudd_addApply]
 574
 575 ******************************************************************************/
 576 DdNode *
 577 Cudd_addOr(
 578   DdManager * dd,
 579   DdNode ** f,
 580   DdNode ** g)
 581 {
 582     DdNode *F, *G;
 583
 584     F = *f; G = *g;
 585     if (F == DD_ONE(dd) || G == DD_ONE(dd)) return(DD_ONE(dd));
 586     if (cuddIsConstant(F)) return(G);
 587     if (cuddIsConstant(G)) return(F);
 588     if (F == G) return(F);
 589     if (F > G) { /* swap f and g */
 590         *f = G;
 591         *g = F;
 592     }
 593     return(NULL);
 594
 595 } /* end of Cudd_addOr */
 596
 597
 598 /**Function********************************************************************
 599
 600   Synopsis    [NAND of two 0-1 ADDs.]
 601
 602   Description [NAND of two 0-1 ADDs. Returns NULL
 603   if not a terminal case; f NAND g otherwise.]
 604
 605   SideEffects [None]
 606
 607   SeeAlso     [Cudd_addApply]
 608
 609 ******************************************************************************/
 610 DdNode *
 611 Cudd_addNand(
 612   DdManager * dd,
 613   DdNode ** f,
 614   DdNode ** g)
 615 {
 616     DdNode *F, *G;
 617
 618     F = *f; G = *g;
 619     if (F == DD_ZERO(dd) || G == DD_ZERO(dd)) return(DD_ONE(dd));
 620     if (cuddIsConstant(F) && cuddIsConstant(G)) return(DD_ZERO(dd));
 621     if (F > G) { /* swap f and g */
 622         *f = G;
 623         *g = F;
 624     }
 625     return(NULL);
 626
 627 } /* end of Cudd_addNand */
 628
 629
 630 /**Function********************************************************************
 631
 632   Synopsis    [NOR of two 0-1 ADDs.]
 633
 634   Description [NOR of two 0-1 ADDs. Returns NULL
 635   if not a terminal case; f NOR g otherwise.]
 636
 637   SideEffects [None]
 638
 639   SeeAlso     [Cudd_addApply]
 640
 641 ******************************************************************************/
 642 DdNode *
 643 Cudd_addNor(
 644   DdManager * dd,
 645   DdNode ** f,
 646   DdNode ** g)
 647 {
 648     DdNode *F, *G;
 649
 650     F = *f; G = *g;
 651     if (F == DD_ONE(dd) || G == DD_ONE(dd)) return(DD_ZERO(dd));
 652     if (cuddIsConstant(F) && cuddIsConstant(G)) return(DD_ONE(dd));
 653     if (F > G) { /* swap f and g */
 654         *f = G;
 655         *g = F;
 656     }
 657     return(NULL);
 658
 659 } /* end of Cudd_addNor */
 660
 661
 662 /**Function********************************************************************
 663
 664   Synopsis    [XOR of two 0-1 ADDs.]
 665
 666   Description [XOR of two 0-1 ADDs. Returns NULL
 667   if not a terminal case; f XOR g otherwise.]
 668
 669   SideEffects [None]
 670
 671   SeeAlso     [Cudd_addApply]
 672
 673 ******************************************************************************/
 674 DdNode *
 675 Cudd_addXor(
 676   DdManager * dd,
 677   DdNode ** f,
 678   DdNode ** g)
 679 {
 680     DdNode *F, *G;
 681
 682     F = *f; G = *g;
 683     if (F == G) return(DD_ZERO(dd));
 684     if (F == DD_ONE(dd) && G == DD_ZERO(dd)) return(DD_ONE(dd));
 685     if (G == DD_ONE(dd) && F == DD_ZERO(dd)) return(DD_ONE(dd));
 686     if (cuddIsConstant(F) && cuddIsConstant(G)) return(DD_ZERO(dd));
 687     if (F > G) { /* swap f and g */
 688         *f = G;
 689         *g = F;
 690     }
 691     return(NULL);
 692
 693 } /* end of Cudd_addXor */
 694
 695
 696 /**Function********************************************************************
 697
 698   Synopsis    [XNOR of two 0-1 ADDs.]
 699
 700   Description [XNOR of two 0-1 ADDs. Returns NULL
 701   if not a terminal case; f XNOR g otherwise.]
 702
 703   SideEffects [None]
 704
 705   SeeAlso     [Cudd_addApply]
 706
 707 ******************************************************************************/
 708 DdNode *
 709 Cudd_addXnor(
 710   DdManager * dd,
 711   DdNode ** f,
 712   DdNode ** g)
 713 {
 714     DdNode *F, *G;
 715
 716     F = *f; G = *g;
 717     if (F == G) return(DD_ONE(dd));
 718     if (F == DD_ONE(dd) && G == DD_ONE(dd)) return(DD_ONE(dd));
 719     if (G == DD_ZERO(dd) && F == DD_ZERO(dd)) return(DD_ONE(dd));
 720     if (cuddIsConstant(F) && cuddIsConstant(G)) return(DD_ZERO(dd));
 721     if (F > G) { /* swap f and g */
 722         *f = G;
 723         *g = F;
 724     }
 725     return(NULL);
 726
 727 } /* end of Cudd_addXnor */
 728
 729
 730 /**Function********************************************************************
 731
 732   Synopsis    [Applies op to the discriminants of f.]
 733
 734   Description [Applies op to the discriminants of f.
 735   Returns a pointer to the result if succssful; NULL otherwise.]
 736
 737   SideEffects [None]
 738
 739   SeeAlso     [Cudd_addApply Cudd_addLog]
 740
 741 ******************************************************************************/
 742 DdNode *
 743 Cudd_addMonadicApply(
 744   DdManager * dd,
 745   DD_MAOP op,
 746   DdNode * f)
 747 {
 748     DdNode *res;
 749
 750     do {
 751         dd->reordered = 0;
 752         res = cuddAddMonadicApplyRecur(dd,op,f);
 753     } while (dd->reordered == 1);
 754     return(res);
 755
 756 } /* end of Cudd_addMonadicApply */
 757
 758
 759 /**Function********************************************************************
 760
 761   Synopsis    [Natural logarithm of an ADD.]
 762
 763   Description [Natural logarithm of an ADDs. Returns NULL
 764   if not a terminal case; log(f) otherwise.  The discriminants of f must
 765   be positive double's.]
 766
 767   SideEffects [None]
 768
 769   SeeAlso     [Cudd_addMonadicApply]
 770
 771 ******************************************************************************/
 772 DdNode *
 773 Cudd_addLog(
 774   DdManager * dd,
 775   DdNode * f)
 776 {
 777     if (cuddIsConstant(f)) {
 778         CUDD_VALUE_TYPE value = log(cuddV(f));
 779         DdNode *res = cuddUniqueConst(dd,value);
 780         return(res);
 781     }
 782     return(NULL);
 783
 784 } /* end of Cudd_addLog */
 785
 786
 787 /*---------------------------------------------------------------------------*/
 788 /* Definition of internal functions                                          */
 789 /*---------------------------------------------------------------------------*/
 790
 791
 792 /**Function********************************************************************
 793
 794   Synopsis    [Performs the recursive step of Cudd_addApply.]
 795
 796   Description [Performs the recursive step of Cudd_addApply. Returns a
 797   pointer to the result if successful; NULL otherwise.]
 798
 799   SideEffects [None]
 800
 801   SeeAlso     [cuddAddMonadicApplyRecur]
 802
 803 ******************************************************************************/
 804 DdNode *
 805 cuddAddApplyRecur(
 806   DdManager * dd,
 807   DD_AOP op,
 808   DdNode * f,
 809   DdNode * g)
 810 {
 811     DdNode *res,
 812            *fv, *fvn, *gv, *gvn,
 813            *T, *E;
 814     unsigned int ford, gord;
 815     unsigned int index;
 816     DD_CTFP cacheOp;
 817
 818     /* Check terminal cases. Op may swap f and g to increase the
 819      * cache hit rate.
 820      */
 821     statLine(dd);
 822     res = (*op)(dd,&f,&g);
 823     if (res != NULL) return(res);
 824
 825     /* Check cache. */
 826     cacheOp = (DD_CTFP) op;
 827     res = cuddCacheLookup2(dd,cacheOp,f,g);
 828     if (res != NULL) return(res);
 829
 830     /* Recursive step. */
 831     ford = cuddI(dd,f->index);
 832     gord = cuddI(dd,g->index);
 833     if (ford <= gord) {
 834         index = f->index;
 835         fv = cuddT(f);
 836         fvn = cuddE(f);
 837     } else {
 838         index = g->index;
 839         fv = fvn = f;
 840     }
 841     if (gord <= ford) {
 842         gv = cuddT(g);
 843         gvn = cuddE(g);
 844     } else {
 845         gv = gvn = g;
 846     }
 847
 848     T = cuddAddApplyRecur(dd,op,fv,gv);
 849     if (T == NULL) return(NULL);
 850     cuddRef(T);
 851
 852     E = cuddAddApplyRecur(dd,op,fvn,gvn);
 853     if (E == NULL) {
 854         Cudd_RecursiveDeref(dd,T);
 855         return(NULL);
 856     }
 857     cuddRef(E);
 858
 859     res = (T == E) ? T : cuddUniqueInter(dd,(int)index,T,E);
 860     if (res == NULL) {
 861         Cudd_RecursiveDeref(dd, T);
 862         Cudd_RecursiveDeref(dd, E);
 863         return(NULL);
 864     }
 865     cuddDeref(T);
 866     cuddDeref(E);
 867
 868     /* Store result. */
 869     cuddCacheInsert2(dd,cacheOp,f,g,res);
 870
 871     return(res);
 872
 873 } /* end of cuddAddApplyRecur */
 874
 875
 876 /**Function********************************************************************
 877
 878   Synopsis    [Performs the recursive step of Cudd_addMonadicApply.]
 879
 880   Description [Performs the recursive step of Cudd_addMonadicApply. Returns a
 881   pointer to the result if successful; NULL otherwise.]
 882
 883   SideEffects [None]
 884
 885   SeeAlso     [cuddAddApplyRecur]
 886
 887 ******************************************************************************/
 888 DdNode *
 889 cuddAddMonadicApplyRecur(
 890   DdManager * dd,
 891   DD_MAOP op,
 892   DdNode * f)
 893 {
 894     DdNode *res, *ft, *fe, *T, *E;
 895     unsigned int index;
 896
 897     /* Check terminal cases. */
 898     statLine(dd);
 899     res = (*op)(dd,f);
 900     if (res != NULL) return(res);
 901
 902     /* Check cache. */
 903     res = cuddCacheLookup1(dd,op,f);
 904     if (res != NULL) return(res);
 905
 906     /* Recursive step. */
 907     index = f->index;
 908     ft = cuddT(f);
 909     fe = cuddE(f);
 910
 911     T = cuddAddMonadicApplyRecur(dd,op,ft);
 912     if (T == NULL) return(NULL);
 913     cuddRef(T);
 914
 915     E = cuddAddMonadicApplyRecur(dd,op,fe);
 916     if (E == NULL) {
 917         Cudd_RecursiveDeref(dd,T);
 918         return(NULL);
 919     }
 920     cuddRef(E);
 921
 922     res = (T == E) ? T : cuddUniqueInter(dd,(int)index,T,E);
 923     if (res == NULL) {
 924         Cudd_RecursiveDeref(dd, T);
 925         Cudd_RecursiveDeref(dd, E);
 926         return(NULL);
 927     }
 928     cuddDeref(T);
 929     cuddDeref(E);
 930
 931     /* Store result. */
 932     cuddCacheInsert1(dd,op,f,res);
 933
 934     return(res);
 935
 936 } /* end of cuddAddMonadicApplyRecur */
 937
 938
 939 /*---------------------------------------------------------------------------*/
 940 /* Definition of static functions                                            */
 941 /*---------------------------------------------------------------------------*/