distr/cudd/cuddBddIte.c

   1 /**CFile***********************************************************************
   2
   3   FileName    [cuddBddIte.c]
   4
   5   PackageName [cudd]
   6
   7   Synopsis    [BDD ITE function and satellites.]
   8
   9   Description [External procedures included in this module:
  10                 <ul>
  11                 <li> Cudd_bddIte()
  12                 <li> Cudd_bddIteConstant()
  13                 <li> Cudd_bddIntersect()
  14                 <li> Cudd_bddAnd()
  15                 <li> Cudd_bddAndLimit()
  16                 <li> Cudd_bddOr()
  17                 <li> Cudd_bddNand()
  18                 <li> Cudd_bddNor()
  19                 <li> Cudd_bddXor()
  20                 <li> Cudd_bddXnor()
  21                 <li> Cudd_bddLeq()
  22                 </ul>
  23        Internal procedures included in this module:
  24                 <ul>
  25                 <li> cuddBddIteRecur()
  26                 <li> cuddBddIntersectRecur()
  27                 <li> cuddBddAndRecur()
  28                 <li> cuddBddXorRecur()
  29                 </ul>
  30        Static procedures included in this module:
  31                 <ul>
  32                 <li> bddVarToConst()
  33                 <li> bddVarToCanonical()
  34                 <li> bddVarToCanonicalSimple()
  35                 </ul>]
  36
  37   SeeAlso     []
  38
  39   Author      [Fabio Somenzi]
  40
  41   Copyright   [Copyright (c) 1995-2004, Regents of the University of Colorado
  42
  43   All rights reserved.
  44
  45   Redistribution and use in source and binary forms, with or without
  46   modification, are permitted provided that the following conditions
  47   are met:
  48
  49   Redistributions of source code must retain the above copyright
  50   notice, this list of conditions and the following disclaimer.
  51
  52   Redistributions in binary form must reproduce the above copyright
  53   notice, this list of conditions and the following disclaimer in the
  54   documentation and/or other materials provided with the distribution.
  55
  56   Neither the name of the University of Colorado nor the names of its
  57   contributors may be used to endorse or promote products derived from
  58   this software without specific prior written permission.
  59
  60   THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
  61   "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
  62   LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
  63   FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
  64   COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
  65   INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
  66   BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
  67   LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
  68   CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
  69   LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
  70   ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
  71   POSSIBILITY OF SUCH DAMAGE.]
  72
  73 ******************************************************************************/
  74
  75 #include "util.h"
  76 #include "cuddInt.h"
  77
  78
  79 /*---------------------------------------------------------------------------*/
  80 /* Constant declarations                                                     */
  81 /*---------------------------------------------------------------------------*/
  82
  83
  84 /*---------------------------------------------------------------------------*/
  85 /* Stucture declarations                                                     */
  86 /*---------------------------------------------------------------------------*/
  87
  88
  89 /*---------------------------------------------------------------------------*/
  90 /* Type declarations                                                         */
  91 /*---------------------------------------------------------------------------*/
  92
  93
  94 /*---------------------------------------------------------------------------*/
  95 /* Variable declarations                                                     */
  96 /*---------------------------------------------------------------------------*/
  97
  98 #ifndef lint
  99 static char rcsid[] DD_UNUSED = "$Id: cuddBddIte.c,v 1.24 2004/08/13 18:04:46 fabio Exp $";
 100 #endif
 101
 102 /*---------------------------------------------------------------------------*/
 103 /* Macro declarations                                                        */
 104 /*---------------------------------------------------------------------------*/
 105
 106
 107 /**AutomaticStart*************************************************************/
 108
 109 /*---------------------------------------------------------------------------*/
 110 /* Static function prototypes                                                */
 111 /*---------------------------------------------------------------------------*/
 112
 113 static void bddVarToConst (DdNode *f, DdNode **gp, DdNode **hp, DdNode *one);
 114 static int bddVarToCanonical (DdManager *dd, DdNode **fp, DdNode **gp, DdNode **hp, unsigned int *topfp, unsigned int *topgp, unsigned int *tophp);
 115 static int bddVarToCanonicalSimple (DdManager *dd, DdNode **fp, DdNode **gp, DdNode **hp, unsigned int *topfp, unsigned int *topgp, unsigned int *tophp);
 116
 117 /**AutomaticEnd***************************************************************/
 118
 119
 120 /*---------------------------------------------------------------------------*/
 121 /* Definition of exported functions                                          */
 122 /*---------------------------------------------------------------------------*/
 123
 124
 125 /**Function********************************************************************
 126
 127   Synopsis    [Implements ITE(f,g,h).]
 128
 129   Description [Implements ITE(f,g,h). Returns a pointer to the
 130   resulting BDD if successful; NULL if the intermediate result blows
 131   up.]
 132
 133   SideEffects [None]
 134
 135   SeeAlso     [Cudd_addIte Cudd_bddIteConstant Cudd_bddIntersect]
 136
 137 ******************************************************************************/
 138 DdNode *
 139 Cudd_bddIte(
 140   DdManager * dd,
 141   DdNode * f,
 142   DdNode * g,
 143   DdNode * h)
 144 {
 145     DdNode *res;
 146
 147     do {
 148         dd->reordered = 0;
 149         res = cuddBddIteRecur(dd,f,g,h);
 150     } while (dd->reordered == 1);
 151     return(res);
 152
 153 } /* end of Cudd_bddIte */
 154
 155
 156 /**Function********************************************************************
 157
 158   Synopsis    [Implements ITEconstant(f,g,h).]
 159
 160   Description [Implements ITEconstant(f,g,h). Returns a pointer to the
 161   resulting BDD (which may or may not be constant) or DD_NON_CONSTANT.
 162   No new nodes are created.]
 163
 164   SideEffects [None]
 165
 166   SeeAlso     [Cudd_bddIte Cudd_bddIntersect Cudd_bddLeq Cudd_addIteConstant]
 167
 168 ******************************************************************************/
 169 DdNode *
 170 Cudd_bddIteConstant(
 171   DdManager * dd,
 172   DdNode * f,
 173   DdNode * g,
 174   DdNode * h)
 175 {
 176     DdNode       *r, *Fv, *Fnv, *Gv, *Gnv, *H, *Hv, *Hnv, *t, *e;
 177     DdNode       *one = DD_ONE(dd);
 178     DdNode       *zero = Cudd_Not(one);
 179     int          comple;
 180     unsigned int topf, topg, toph, v;
 181
 182     statLine(dd);
 183     /* Trivial cases. */
 184     if (f == one)                       /* ITE(1,G,H) => G */
 185         return(g);
 186
 187     if (f == zero)                      /* ITE(0,G,H) => H */
 188         return(h);
 189
 190     /* f now not a constant. */
 191     bddVarToConst(f, &g, &h, one);      /* possibly convert g or h */
 192                                         /* to constants */
 193
 194     if (g == h)                         /* ITE(F,G,G) => G */
 195         return(g);
 196
 197     if (Cudd_IsConstant(g) && Cudd_IsConstant(h))
 198         return(DD_NON_CONSTANT);        /* ITE(F,1,0) or ITE(F,0,1) */
 199                                         /* => DD_NON_CONSTANT */
 200
 201     if (g == Cudd_Not(h))
 202         return(DD_NON_CONSTANT);        /* ITE(F,G,G') => DD_NON_CONSTANT */
 203                                         /* if F != G and F != G' */
 204
 205     comple = bddVarToCanonical(dd, &f, &g, &h, &topf, &topg, &toph);
 206
 207     /* Cache lookup. */
 208     r = cuddConstantLookup(dd, DD_BDD_ITE_CONSTANT_TAG, f, g, h);
 209     if (r != NULL) {
 210         return(Cudd_NotCond(r,comple && r != DD_NON_CONSTANT));
 211     }
 212
 213     v = ddMin(topg, toph);
 214
 215     /* ITE(F,G,H) = (v,G,H) (non constant) if F = (v,1,0), v < top(G,H). */
 216     if (topf < v && cuddT(f) == one && cuddE(f) == zero) {
 217         return(DD_NON_CONSTANT);
 218     }
 219
 220     /* Compute cofactors. */
 221     if (topf <= v) {
 222         v = ddMin(topf, v);             /* v = top_var(F,G,H) */
 223         Fv = cuddT(f); Fnv = cuddE(f);
 224     } else {
 225         Fv = Fnv = f;
 226     }
 227
 228     if (topg == v) {
 229         Gv = cuddT(g); Gnv = cuddE(g);
 230     } else {
 231         Gv = Gnv = g;
 232     }
 233
 234     if (toph == v) {
 235         H = Cudd_Regular(h);
 236         Hv = cuddT(H); Hnv = cuddE(H);
 237         if (Cudd_IsComplement(h)) {
 238             Hv = Cudd_Not(Hv);
 239             Hnv = Cudd_Not(Hnv);
 240         }
 241     } else {
 242         Hv = Hnv = h;
 243     }
 244
 245     /* Recursion. */
 246     t = Cudd_bddIteConstant(dd, Fv, Gv, Hv);
 247     if (t == DD_NON_CONSTANT || !Cudd_IsConstant(t)) {
 248         cuddCacheInsert(dd, DD_BDD_ITE_CONSTANT_TAG, f, g, h, DD_NON_CONSTANT);
 249         return(DD_NON_CONSTANT);
 250     }
 251     e = Cudd_bddIteConstant(dd, Fnv, Gnv, Hnv);
 252     if (e == DD_NON_CONSTANT || !Cudd_IsConstant(e) || t != e) {
 253         cuddCacheInsert(dd, DD_BDD_ITE_CONSTANT_TAG, f, g, h, DD_NON_CONSTANT);
 254         return(DD_NON_CONSTANT);
 255     }
 256     cuddCacheInsert(dd, DD_BDD_ITE_CONSTANT_TAG, f, g, h, t);
 257     return(Cudd_NotCond(t,comple));
 258
 259 } /* end of Cudd_bddIteConstant */
 260
 261
 262 /**Function********************************************************************
 263
 264   Synopsis    [Returns a function included in the intersection of f and g.]
 265
 266   Description [Computes a function included in the intersection of f and
 267   g. (That is, a witness that the intersection is not empty.)
 268   Cudd_bddIntersect tries to build as few new nodes as possible. If the
 269   only result of interest is whether f and g intersect,
 270   Cudd_bddLeq should be used instead.]
 271
 272   SideEffects [None]
 273
 274   SeeAlso     [Cudd_bddLeq Cudd_bddIteConstant]
 275
 276 ******************************************************************************/
 277 DdNode *
 278 Cudd_bddIntersect(
 279   DdManager * dd /* manager */,
 280   DdNode * f /* first operand */,
 281   DdNode * g /* second operand */)
 282 {
 283     DdNode *res;
 284
 285     do {
 286         dd->reordered = 0;
 287         res = cuddBddIntersectRecur(dd,f,g);
 288     } while (dd->reordered == 1);
 289
 290     return(res);
 291
 292 } /* end of Cudd_bddIntersect */
 293
 294
 295 /**Function********************************************************************
 296
 297   Synopsis    [Computes the conjunction of two BDDs f and g.]
 298
 299   Description [Computes the conjunction of two BDDs f and g. Returns a
 300   pointer to the resulting BDD if successful; NULL if the intermediate
 301   result blows up.]
 302
 303   SideEffects [None]
 304
 305   SeeAlso     [Cudd_bddIte Cudd_addApply Cudd_bddAndAbstract Cudd_bddIntersect
 306   Cudd_bddOr Cudd_bddNand Cudd_bddNor Cudd_bddXor Cudd_bddXnor]
 307
 308 ******************************************************************************/
 309 DdNode *
 310 Cudd_bddAnd(
 311   DdManager * dd,
 312   DdNode * f,
 313   DdNode * g)
 314 {
 315     DdNode *res;
 316
 317     do {
 318         dd->reordered = 0;
 319         res = cuddBddAndRecur(dd,f,g);
 320     } while (dd->reordered == 1);
 321     return(res);
 322
 323 } /* end of Cudd_bddAnd */
 324
 325
 326 /**Function********************************************************************
 327
 328   Synopsis    [Computes the conjunction of two BDDs f and g.  Returns
 329   NULL if too many nodes are required.]
 330
 331   Description [Computes the conjunction of two BDDs f and g. Returns a
 332   pointer to the resulting BDD if successful; NULL if the intermediate
 333   result blows up or more new nodes than <code>limit</code> are
 334   required.]
 335
 336   SideEffects [None]
 337
 338   SeeAlso     [Cudd_bddAnd]
 339
 340 ******************************************************************************/
 341 DdNode *
 342 Cudd_bddAndLimit(
 343   DdManager * dd,
 344   DdNode * f,
 345   DdNode * g,
 346   unsigned int limit)
 347 {
 348     DdNode *res;
 349     unsigned int saveLimit = dd->maxLive;
 350
 351     dd->maxLive = (dd->keys - dd->dead) + (dd->keysZ - dd->deadZ) + limit;
 352     do {
 353         dd->reordered = 0;
 354         res = cuddBddAndRecur(dd,f,g);
 355     } while (dd->reordered == 1);
 356     dd->maxLive = saveLimit;
 357     return(res);
 358
 359 } /* end of Cudd_bddAndLimit */
 360
 361
 362 /**Function********************************************************************
 363
 364   Synopsis    [Computes the disjunction of two BDDs f and g.]
 365
 366   Description [Computes the disjunction of two BDDs f and g. Returns a
 367   pointer to the resulting BDD if successful; NULL if the intermediate
 368   result blows up.]
 369
 370   SideEffects [None]
 371
 372   SeeAlso     [Cudd_bddIte Cudd_addApply Cudd_bddAnd Cudd_bddNand Cudd_bddNor
 373   Cudd_bddXor Cudd_bddXnor]
 374
 375 ******************************************************************************/
 376 DdNode *
 377 Cudd_bddOr(
 378   DdManager * dd,
 379   DdNode * f,
 380   DdNode * g)
 381 {
 382     DdNode *res;
 383
 384     do {
 385         dd->reordered = 0;
 386         res = cuddBddAndRecur(dd,Cudd_Not(f),Cudd_Not(g));
 387     } while (dd->reordered == 1);
 388     res = Cudd_NotCond(res,res != NULL);
 389     return(res);
 390
 391 } /* end of Cudd_bddOr */
 392
 393
 394 /**Function********************************************************************
 395
 396   Synopsis    [Computes the NAND of two BDDs f and g.]
 397
 398   Description [Computes the NAND of two BDDs f and g. Returns a
 399   pointer to the resulting BDD if successful; NULL if the intermediate
 400   result blows up.]
 401
 402   SideEffects [None]
 403
 404   SeeAlso     [Cudd_bddIte Cudd_addApply Cudd_bddAnd Cudd_bddOr Cudd_bddNor
 405   Cudd_bddXor Cudd_bddXnor]
 406
 407 ******************************************************************************/
 408 DdNode *
 409 Cudd_bddNand(
 410   DdManager * dd,
 411   DdNode * f,
 412   DdNode * g)
 413 {
 414     DdNode *res;
 415
 416     do {
 417         dd->reordered = 0;
 418         res = cuddBddAndRecur(dd,f,g);
 419     } while (dd->reordered == 1);
 420     res = Cudd_NotCond(res,res != NULL);
 421     return(res);
 422
 423 } /* end of Cudd_bddNand */
 424
 425
 426 /**Function********************************************************************
 427
 428   Synopsis    [Computes the NOR of two BDDs f and g.]
 429
 430   Description [Computes the NOR of two BDDs f and g. Returns a
 431   pointer to the resulting BDD if successful; NULL if the intermediate
 432   result blows up.]
 433
 434   SideEffects [None]
 435
 436   SeeAlso     [Cudd_bddIte Cudd_addApply Cudd_bddAnd Cudd_bddOr Cudd_bddNand
 437   Cudd_bddXor Cudd_bddXnor]
 438
 439 ******************************************************************************/
 440 DdNode *
 441 Cudd_bddNor(
 442   DdManager * dd,
 443   DdNode * f,
 444   DdNode * g)
 445 {
 446     DdNode *res;
 447
 448     do {
 449         dd->reordered = 0;
 450         res = cuddBddAndRecur(dd,Cudd_Not(f),Cudd_Not(g));
 451     } while (dd->reordered == 1);
 452     return(res);
 453
 454 } /* end of Cudd_bddNor */
 455
 456
 457 /**Function********************************************************************
 458
 459   Synopsis    [Computes the exclusive OR of two BDDs f and g.]
 460
 461   Description [Computes the exclusive OR of two BDDs f and g. Returns a
 462   pointer to the resulting BDD if successful; NULL if the intermediate
 463   result blows up.]
 464
 465   SideEffects [None]
 466
 467   SeeAlso     [Cudd_bddIte Cudd_addApply Cudd_bddAnd Cudd_bddOr
 468   Cudd_bddNand Cudd_bddNor Cudd_bddXnor]
 469
 470 ******************************************************************************/
 471 DdNode *
 472 Cudd_bddXor(
 473   DdManager * dd,
 474   DdNode * f,
 475   DdNode * g)
 476 {
 477     DdNode *res;
 478
 479     do {
 480         dd->reordered = 0;
 481         res = cuddBddXorRecur(dd,f,g);
 482     } while (dd->reordered == 1);
 483     return(res);
 484
 485 } /* end of Cudd_bddXor */
 486
 487
 488 /**Function********************************************************************
 489
 490   Synopsis    [Computes the exclusive NOR of two BDDs f and g.]
 491
 492   Description [Computes the exclusive NOR of two BDDs f and g. Returns a
 493   pointer to the resulting BDD if successful; NULL if the intermediate
 494   result blows up.]
 495
 496   SideEffects [None]
 497
 498   SeeAlso     [Cudd_bddIte Cudd_addApply Cudd_bddAnd Cudd_bddOr
 499   Cudd_bddNand Cudd_bddNor Cudd_bddXor]
 500
 501 ******************************************************************************/
 502 DdNode *
 503 Cudd_bddXnor(
 504   DdManager * dd,
 505   DdNode * f,
 506   DdNode * g)
 507 {
 508     DdNode *res;
 509
 510     do {
 511         dd->reordered = 0;
 512         res = cuddBddXorRecur(dd,f,Cudd_Not(g));
 513     } while (dd->reordered == 1);
 514     return(res);
 515
 516 } /* end of Cudd_bddXnor */
 517
 518
 519 /**Function********************************************************************
 520
 521   Synopsis    [Determines whether f is less than or equal to g.]
 522
 523   Description [Returns 1 if f is less than or equal to g; 0 otherwise.
 524   No new nodes are created.]
 525
 526   SideEffects [None]
 527
 528   SeeAlso     [Cudd_bddIteConstant Cudd_addEvalConst]
 529
 530 ******************************************************************************/
 531 int
 532 Cudd_bddLeq(
 533   DdManager * dd,
 534   DdNode * f,
 535   DdNode * g)
 536 {
 537     DdNode *one, *zero, *tmp, *F, *fv, *fvn, *gv, *gvn;
 538     unsigned int topf, topg, res;
 539
 540     statLine(dd);
 541     /* Terminal cases and normalization. */
 542     if (f == g) return(1);
 543
 544     if (Cudd_IsComplement(g)) {
 545         /* Special case: if f is regular and g is complemented,
 546         ** f(1,...,1) = 1 > 0 = g(1,...,1).
 547         */
 548         if (!Cudd_IsComplement(f)) return(0);
 549         /* Both are complemented: Swap and complement because
 550         ** f <= g <=> g' <= f' and we want the second argument to be regular.
 551         */
 552         tmp = g;
 553         g = Cudd_Not(f);
 554         f = Cudd_Not(tmp);
 555     } else if (Cudd_IsComplement(f) && g < f) {
 556         tmp = g;
 557         g = Cudd_Not(f);
 558         f = Cudd_Not(tmp);
 559     }
 560
 561     /* Now g is regular and, if f is not regular, f < g. */
 562     one = DD_ONE(dd);
 563     if (g == one) return(1);    /* no need to test against zero */
 564     if (f == one) return(0);    /* since at this point g != one */
 565     if (Cudd_Not(f) == g) return(0); /* because neither is constant */
 566     zero = Cudd_Not(one);
 567     if (f == zero) return(1);
 568
 569     /* Here neither f nor g is constant. */
 570
 571     /* Check cache. */
 572     tmp = cuddCacheLookup2(dd,(DD_CTFP)Cudd_bddLeq,f,g);
 573     if (tmp != NULL) {
 574         return(tmp == one);
 575     }
 576
 577     /* Compute cofactors. */
 578     F = Cudd_Regular(f);
 579     topf = dd->perm[F->index];
 580     topg = dd->perm[g->index];
 581     if (topf <= topg) {
 582         fv = cuddT(F); fvn = cuddE(F);
 583         if (f != F) {
 584             fv = Cudd_Not(fv);
 585             fvn = Cudd_Not(fvn);
 586         }
 587     } else {
 588         fv = fvn = f;
 589     }
 590     if (topg <= topf) {
 591         gv = cuddT(g); gvn = cuddE(g);
 592     } else {
 593         gv = gvn = g;
 594     }
 595
 596     /* Recursive calls. Since we want to maximize the probability of
 597     ** the special case f(1,...,1) > g(1,...,1), we consider the negative
 598     ** cofactors first. Indeed, the complementation parity of the positive
 599     ** cofactors is the same as the one of the parent functions.
 600     */
 601     res = Cudd_bddLeq(dd,fvn,gvn) && Cudd_bddLeq(dd,fv,gv);
 602
 603     /* Store result in cache and return. */
 604     cuddCacheInsert2(dd,(DD_CTFP)Cudd_bddLeq,f,g,(res ? one : zero));
 605     return(res);
 606
 607 } /* end of Cudd_bddLeq */
 608
 609
 610 /*---------------------------------------------------------------------------*/
 611 /* Definition of internal functions                                          */
 612 /*---------------------------------------------------------------------------*/
 613
 614
 615 /**Function********************************************************************
 616
 617   Synopsis    [Implements the recursive step of Cudd_bddIte.]
 618
 619   Description [Implements the recursive step of Cudd_bddIte. Returns a
 620   pointer to the resulting BDD. NULL if the intermediate result blows
 621   up or if reordering occurs.]
 622
 623   SideEffects [None]
 624
 625   SeeAlso     []
 626
 627 ******************************************************************************/
 628 DdNode *
 629 cuddBddIteRecur(
 630   DdManager * dd,
 631   DdNode * f,
 632   DdNode * g,
 633   DdNode * h)
 634 {
 635     DdNode       *one, *zero, *res;
 636     DdNode       *r, *Fv, *Fnv, *Gv, *Gnv, *H, *Hv, *Hnv, *t, *e;
 637     unsigned int topf, topg, toph, v;
 638     int          index;
 639     int          comple;
 640
 641     statLine(dd);
 642     /* Terminal cases. */
 643
 644     /* One variable cases. */
 645     if (f == (one = DD_ONE(dd)))        /* ITE(1,G,H) = G */
 646         return(g);
 647
 648     if (f == (zero = Cudd_Not(one)))    /* ITE(0,G,H) = H */
 649         return(h);
 650
 651     /* From now on, f is known not to be a constant. */
 652     if (g == one || f == g) {   /* ITE(F,F,H) = ITE(F,1,H) = F + H */
 653         if (h == zero) {        /* ITE(F,1,0) = F */
 654             return(f);
 655         } else {
 656             res = cuddBddAndRecur(dd,Cudd_Not(f),Cudd_Not(h));
 657             return(Cudd_NotCond(res,res != NULL));
 658         }
 659     } else if (g == zero || f == Cudd_Not(g)) { /* ITE(F,!F,H) = ITE(F,0,H) = !F * H */
 660         if (h == one) {         /* ITE(F,0,1) = !F */
 661             return(Cudd_Not(f));
 662         } else {
 663             res = cuddBddAndRecur(dd,Cudd_Not(f),h);
 664             return(res);
 665         }
 666     }
 667     if (h == zero || f == h) {    /* ITE(F,G,F) = ITE(F,G,0) = F * G */
 668         res = cuddBddAndRecur(dd,f,g);
 669         return(res);
 670     } else if (h == one || f == Cudd_Not(h)) { /* ITE(F,G,!F) = ITE(F,G,1) = !F + G */
 671         res = cuddBddAndRecur(dd,f,Cudd_Not(g));
 672         return(Cudd_NotCond(res,res != NULL));
 673     }
 674
 675     /* Check remaining one variable case. */
 676     if (g == h) {               /* ITE(F,G,G) = G */
 677         return(g);
 678     } else if (g == Cudd_Not(h)) { /* ITE(F,G,!G) = F <-> G */
 679         res = cuddBddXorRecur(dd,f,h);
 680         return(res);
 681     }
 682
 683     /* From here, there are no constants. */
 684     comple = bddVarToCanonicalSimple(dd, &f, &g, &h, &topf, &topg, &toph);
 685
 686     /* f & g are now regular pointers */
 687
 688     v = ddMin(topg, toph);
 689
 690     /* A shortcut: ITE(F,G,H) = (v,G,H) if F = (v,1,0), v < top(G,H). */
 691     if (topf < v && cuddT(f) == one && cuddE(f) == zero) {
 692         r = cuddUniqueInter(dd, (int) f->index, g, h);
 693         return(Cudd_NotCond(r,comple && r != NULL));
 694     }
 695
 696     /* Check cache. */
 697     r = cuddCacheLookup(dd, DD_BDD_ITE_TAG, f, g, h);
 698     if (r != NULL) {
 699         return(Cudd_NotCond(r,comple));
 700     }
 701
 702     /* Compute cofactors. */
 703     if (topf <= v) {
 704         v = ddMin(topf, v);     /* v = top_var(F,G,H) */
 705         index = f->index;
 706         Fv = cuddT(f); Fnv = cuddE(f);
 707     } else {
 708         Fv = Fnv = f;
 709     }
 710     if (topg == v) {
 711         index = g->index;
 712         Gv = cuddT(g); Gnv = cuddE(g);
 713     } else {
 714         Gv = Gnv = g;
 715     }
 716     if (toph == v) {
 717         H = Cudd_Regular(h);
 718         index = H->index;
 719         Hv = cuddT(H); Hnv = cuddE(H);
 720         if (Cudd_IsComplement(h)) {
 721             Hv = Cudd_Not(Hv);
 722             Hnv = Cudd_Not(Hnv);
 723         }
 724     } else {
 725         Hv = Hnv = h;
 726     }
 727
 728     /* Recursive step. */
 729     t = cuddBddIteRecur(dd,Fv,Gv,Hv);
 730     if (t == NULL) return(NULL);
 731     cuddRef(t);
 732
 733     e = cuddBddIteRecur(dd,Fnv,Gnv,Hnv);
 734     if (e == NULL) {
 735         Cudd_IterDerefBdd(dd,t);
 736         return(NULL);
 737     }
 738     cuddRef(e);
 739
 740     r = (t == e) ? t : cuddUniqueInter(dd,index,t,e);
 741     if (r == NULL) {
 742         Cudd_IterDerefBdd(dd,t);
 743         Cudd_IterDerefBdd(dd,e);
 744         return(NULL);
 745     }
 746     cuddDeref(t);
 747     cuddDeref(e);
 748
 749     cuddCacheInsert(dd, DD_BDD_ITE_TAG, f, g, h, r);
 750     return(Cudd_NotCond(r,comple));
 751
 752 } /* end of cuddBddIteRecur */
 753
 754
 755 /**Function********************************************************************
 756
 757   Synopsis    [Implements the recursive step of Cudd_bddIntersect.]
 758
 759   Description []
 760
 761   SideEffects [None]
 762
 763   SeeAlso     [Cudd_bddIntersect]
 764
 765 ******************************************************************************/
 766 DdNode *
 767 cuddBddIntersectRecur(
 768   DdManager * dd,
 769   DdNode * f,
 770   DdNode * g)
 771 {
 772     DdNode *res;
 773     DdNode *F, *G, *t, *e;
 774     DdNode *fv, *fnv, *gv, *gnv;
 775     DdNode *one, *zero;
 776     unsigned int index, topf, topg;
 777
 778     statLine(dd);
 779     one = DD_ONE(dd);
 780     zero = Cudd_Not(one);
 781
 782     /* Terminal cases. */
 783     if (f == zero || g == zero || f == Cudd_Not(g)) return(zero);
 784     if (f == g || g == one) return(f);
 785     if (f == one) return(g);
 786
 787     /* At this point f and g are not constant. */
 788     if (f > g) { DdNode *tmp = f; f = g; g = tmp; }
 789     res = cuddCacheLookup2(dd,Cudd_bddIntersect,f,g);
 790     if (res != NULL) return(res);
 791
 792     /* Find splitting variable. Here we can skip the use of cuddI,
 793     ** because the operands are known to be non-constant.
 794     */
 795     F = Cudd_Regular(f);
 796     topf = dd->perm[F->index];
 797     G = Cudd_Regular(g);
 798     topg = dd->perm[G->index];
 799
 800     /* Compute cofactors. */
 801     if (topf <= topg) {
 802         index = F->index;
 803         fv = cuddT(F);
 804         fnv = cuddE(F);
 805         if (Cudd_IsComplement(f)) {
 806             fv = Cudd_Not(fv);
 807             fnv = Cudd_Not(fnv);
 808         }
 809     } else {
 810         index = G->index;
 811         fv = fnv = f;
 812     }
 813
 814     if (topg <= topf) {
 815         gv = cuddT(G);
 816         gnv = cuddE(G);
 817         if (Cudd_IsComplement(g)) {
 818             gv = Cudd_Not(gv);
 819             gnv = Cudd_Not(gnv);
 820         }
 821     } else {
 822         gv = gnv = g;
 823     }
 824
 825     /* Compute partial results. */
 826     t = cuddBddIntersectRecur(dd,fv,gv);
 827     if (t == NULL) return(NULL);
 828     cuddRef(t);
 829     if (t != zero) {
 830         e = zero;
 831     } else {
 832         e = cuddBddIntersectRecur(dd,fnv,gnv);
 833         if (e == NULL) {
 834             Cudd_IterDerefBdd(dd, t);
 835             return(NULL);
 836         }
 837     }
 838     cuddRef(e);
 839
 840     if (t == e) { /* both equal zero */
 841         res = t;
 842     } else if (Cudd_IsComplement(t)) {
 843         res = cuddUniqueInter(dd,(int)index,Cudd_Not(t),Cudd_Not(e));
 844         if (res == NULL) {
 845             Cudd_IterDerefBdd(dd, t);
 846             Cudd_IterDerefBdd(dd, e);
 847             return(NULL);
 848         }
 849         res = Cudd_Not(res);
 850     } else {
 851         res = cuddUniqueInter(dd,(int)index,t,e);
 852         if (res == NULL) {
 853             Cudd_IterDerefBdd(dd, t);
 854             Cudd_IterDerefBdd(dd, e);
 855             return(NULL);
 856         }
 857     }
 858     cuddDeref(e);
 859     cuddDeref(t);
 860
 861     cuddCacheInsert2(dd,Cudd_bddIntersect,f,g,res);
 862
 863     return(res);
 864
 865 } /* end of cuddBddIntersectRecur */
 866
 867
 868 /**Function********************************************************************
 869
 870   Synopsis [Implements the recursive step of Cudd_bddAnd.]
 871
 872   Description [Implements the recursive step of Cudd_bddAnd by taking
 873   the conjunction of two BDDs.  Returns a pointer to the result is
 874   successful; NULL otherwise.]
 875
 876   SideEffects [None]
 877
 878   SeeAlso     [Cudd_bddAnd]
 879
 880 ******************************************************************************/
 881 DdNode *
 882 cuddBddAndRecur(
 883   DdManager * manager,
 884   DdNode * f,
 885   DdNode * g)
 886 {
 887     DdNode *F, *fv, *fnv, *G, *gv, *gnv;
 888     DdNode *one, *r, *t, *e;
 889     unsigned int topf, topg, index;
 890
 891     statLine(manager);
 892     one = DD_ONE(manager);
 893
 894     /* Terminal cases. */
 895     F = Cudd_Regular(f);
 896     G = Cudd_Regular(g);
 897     if (F == G) {
 898         if (f == g) return(f);
 899         else return(Cudd_Not(one));
 900     }
 901     if (F == one) {
 902         if (f == one) return(g);
 903         else return(f);
 904     }
 905     if (G == one) {
 906         if (g == one) return(f);
 907         else return(g);
 908     }
 909
 910     /* At this point f and g are not constant. */
 911     if (f > g) { /* Try to increase cache efficiency. */
 912         DdNode *tmp = f;
 913         f = g;
 914         g = tmp;
 915         F = Cudd_Regular(f);
 916         G = Cudd_Regular(g);
 917     }
 918
 919     /* Check cache. */
 920     if (F->ref != 1 || G->ref != 1) {
 921         r = cuddCacheLookup2(manager, Cudd_bddAnd, f, g);
 922         if (r != NULL) return(r);
 923     }
 924
 925     /* Here we can skip the use of cuddI, because the operands are known
 926     ** to be non-constant.
 927     */
 928     topf = manager->perm[F->index];
 929     topg = manager->perm[G->index];
 930
 931     /* Compute cofactors. */
 932     if (topf <= topg) {
 933         index = F->index;
 934         fv = cuddT(F);
 935         fnv = cuddE(F);
 936         if (Cudd_IsComplement(f)) {
 937             fv = Cudd_Not(fv);
 938             fnv = Cudd_Not(fnv);
 939         }
 940     } else {
 941         index = G->index;
 942         fv = fnv = f;
 943     }
 944
 945     if (topg <= topf) {
 946         gv = cuddT(G);
 947         gnv = cuddE(G);
 948         if (Cudd_IsComplement(g)) {
 949             gv = Cudd_Not(gv);
 950             gnv = Cudd_Not(gnv);
 951         }
 952     } else {
 953         gv = gnv = g;
 954     }
 955
 956     t = cuddBddAndRecur(manager, fv, gv);
 957     if (t == NULL) return(NULL);
 958     cuddRef(t);
 959
 960     e = cuddBddAndRecur(manager, fnv, gnv);
 961     if (e == NULL) {
 962         Cudd_IterDerefBdd(manager, t);
 963         return(NULL);
 964     }
 965     cuddRef(e);
 966
 967     if (t == e) {
 968         r = t;
 969     } else {
 970         if (Cudd_IsComplement(t)) {
 971             r = cuddUniqueInter(manager,(int)index,Cudd_Not(t),Cudd_Not(e));
 972             if (r == NULL) {
 973                 Cudd_IterDerefBdd(manager, t);
 974                 Cudd_IterDerefBdd(manager, e);
 975                 return(NULL);
 976             }
 977             r = Cudd_Not(r);
 978         } else {
 979             r = cuddUniqueInter(manager,(int)index,t,e);
 980             if (r == NULL) {
 981                 Cudd_IterDerefBdd(manager, t);
 982                 Cudd_IterDerefBdd(manager, e);
 983                 return(NULL);
 984             }
 985         }
 986     }
 987     cuddDeref(e);
 988     cuddDeref(t);
 989     if (F->ref != 1 || G->ref != 1)
 990         cuddCacheInsert2(manager, Cudd_bddAnd, f, g, r);
 991     return(r);
 992
 993 } /* end of cuddBddAndRecur */
 994
 995
 996 /**Function********************************************************************
 997
 998   Synopsis [Implements the recursive step of Cudd_bddXor.]
 999
1000   Description [Implements the recursive step of Cudd_bddXor by taking
1001   the exclusive OR of two BDDs.  Returns a pointer to the result is
1002   successful; NULL otherwise.]
1003
1004   SideEffects [None]
1005
1006   SeeAlso     [Cudd_bddXor]
1007
1008 ******************************************************************************/
1009 DdNode *
1010 cuddBddXorRecur(
1011   DdManager * manager,
1012   DdNode * f,
1013   DdNode * g)
1014 {
1015     DdNode *fv, *fnv, *G, *gv, *gnv;
1016     DdNode *one, *zero, *r, *t, *e;
1017     unsigned int topf, topg, index;
1018
1019     statLine(manager);
1020     one = DD_ONE(manager);
1021     zero = Cudd_Not(one);
1022
1023     /* Terminal cases. */
1024     if (f == g) return(zero);
1025     if (f == Cudd_Not(g)) return(one);
1026     if (f > g) { /* Try to increase cache efficiency and simplify tests. */
1027         DdNode *tmp = f;
1028         f = g;
1029         g = tmp;
1030     }
1031     if (g == zero) return(f);
1032     if (g == one) return(Cudd_Not(f));
1033     if (Cudd_IsComplement(f)) {
1034         f = Cudd_Not(f);
1035         g = Cudd_Not(g);
1036     }
1037     /* Now the first argument is regular. */
1038     if (f == one) return(Cudd_Not(g));
1039
1040     /* At this point f and g are not constant. */
1041
1042     /* Check cache. */
1043     r = cuddCacheLookup2(manager, Cudd_bddXor, f, g);
1044     if (r != NULL) return(r);
1045
1046     /* Here we can skip the use of cuddI, because the operands are known
1047     ** to be non-constant.
1048     */
1049     topf = manager->perm[f->index];
1050     G = Cudd_Regular(g);
1051     topg = manager->perm[G->index];
1052
1053     /* Compute cofactors. */
1054     if (topf <= topg) {
1055         index = f->index;
1056         fv = cuddT(f);
1057         fnv = cuddE(f);
1058     } else {
1059         index = G->index;
1060         fv = fnv = f;
1061     }
1062
1063     if (topg <= topf) {
1064         gv = cuddT(G);
1065         gnv = cuddE(G);
1066         if (Cudd_IsComplement(g)) {
1067             gv = Cudd_Not(gv);
1068             gnv = Cudd_Not(gnv);
1069         }
1070     } else {
1071         gv = gnv = g;
1072     }
1073
1074     t = cuddBddXorRecur(manager, fv, gv);
1075     if (t == NULL) return(NULL);
1076     cuddRef(t);
1077
1078     e = cuddBddXorRecur(manager, fnv, gnv);
1079     if (e == NULL) {
1080         Cudd_IterDerefBdd(manager, t);
1081         return(NULL);
1082     }
1083     cuddRef(e);
1084
1085     if (t == e) {
1086         r = t;
1087     } else {
1088         if (Cudd_IsComplement(t)) {
1089             r = cuddUniqueInter(manager,(int)index,Cudd_Not(t),Cudd_Not(e));
1090             if (r == NULL) {
1091                 Cudd_IterDerefBdd(manager, t);
1092                 Cudd_IterDerefBdd(manager, e);
1093                 return(NULL);
1094             }
1095             r = Cudd_Not(r);
1096         } else {
1097             r = cuddUniqueInter(manager,(int)index,t,e);
1098             if (r == NULL) {
1099                 Cudd_IterDerefBdd(manager, t);
1100                 Cudd_IterDerefBdd(manager, e);
1101                 return(NULL);
1102             }
1103         }
1104     }
1105     cuddDeref(e);
1106     cuddDeref(t);
1107     cuddCacheInsert2(manager, Cudd_bddXor, f, g, r);
1108     return(r);
1109
1110 } /* end of cuddBddXorRecur */
1111
1112
1113 /*---------------------------------------------------------------------------*/
1114 /* Definition of static functions                                            */
1115 /*---------------------------------------------------------------------------*/
1116
1117
1118 /**Function********************************************************************
1119
1120   Synopsis [Replaces variables with constants if possible.]
1121
1122   Description [This function performs part of the transformation to
1123   standard form by replacing variables with constants if possible.]
1124
1125   SideEffects [None]
1126
1127   SeeAlso     [bddVarToCanonical bddVarToCanonicalSimple]
1128
1129 ******************************************************************************/
1130 static void
1131 bddVarToConst(
1132   DdNode * f,
1133   DdNode ** gp,
1134   DdNode ** hp,
1135   DdNode * one)
1136 {
1137     DdNode *g = *gp;
1138     DdNode *h = *hp;
1139
1140     if (f == g) {    /* ITE(F,F,H) = ITE(F,1,H) = F + H */
1141         *gp = one;
1142     } else if (f == Cudd_Not(g)) {    /* ITE(F,!F,H) = ITE(F,0,H) = !F * H */
1143         *gp = Cudd_Not(one);
1144     }
1145     if (f == h) {    /* ITE(F,G,F) = ITE(F,G,0) = F * G */
1146         *hp = Cudd_Not(one);
1147     } else if (f == Cudd_Not(h)) {    /* ITE(F,G,!F) = ITE(F,G,1) = !F + G */
1148         *hp = one;
1149     }
1150
1151 } /* end of bddVarToConst */
1152
1153
1154 /**Function********************************************************************
1155
1156   Synopsis [Picks unique member from equiv expressions.]
1157
1158   Description [Reduces 2 variable expressions to canonical form.]
1159
1160   SideEffects [None]
1161
1162   SeeAlso     [bddVarToConst bddVarToCanonicalSimple]
1163
1164 ******************************************************************************/
1165 static int
1166 bddVarToCanonical(
1167   DdManager * dd,
1168   DdNode ** fp,
1169   DdNode ** gp,
1170   DdNode ** hp,
1171   unsigned int * topfp,
1172   unsigned int * topgp,
1173   unsigned int * tophp)
1174 {
1175     register DdNode             *F, *G, *H, *r, *f, *g, *h;
1176     register unsigned int       topf, topg, toph;
1177     DdNode                      *one = dd->one;
1178     int                         comple, change;
1179
1180     f = *fp;
1181     g = *gp;
1182     h = *hp;
1183     F = Cudd_Regular(f);
1184     G = Cudd_Regular(g);
1185     H = Cudd_Regular(h);
1186     topf = cuddI(dd,F->index);
1187     topg = cuddI(dd,G->index);
1188     toph = cuddI(dd,H->index);
1189
1190     change = 0;
1191
1192     if (G == one) {                     /* ITE(F,c,H) */
1193         if ((topf > toph) || (topf == toph && f > h)) {
1194             r = h;
1195             h = f;
1196             f = r;                      /* ITE(F,1,H) = ITE(H,1,F) */
1197             if (g != one) {     /* g == zero */
1198                 f = Cudd_Not(f);                /* ITE(F,0,H) = ITE(!H,0,!F) */
1199                 h = Cudd_Not(h);
1200             }
1201             change = 1;
1202         }
1203     } else if (H == one) {              /* ITE(F,G,c) */
1204         if ((topf > topg) || (topf == topg && f > g)) {
1205             r = g;
1206             g = f;
1207             f = r;                      /* ITE(F,G,0) = ITE(G,F,0) */
1208             if (h == one) {
1209                 f = Cudd_Not(f);                /* ITE(F,G,1) = ITE(!G,!F,1) */
1210                 g = Cudd_Not(g);
1211             }
1212             change = 1;
1213         }
1214     } else if (g == Cudd_Not(h)) {      /* ITE(F,G,!G) = ITE(G,F,!F) */
1215         if ((topf > topg) || (topf == topg && f > g)) {
1216             r = f;
1217             f = g;
1218             g = r;
1219             h = Cudd_Not(r);
1220             change = 1;
1221         }
1222     }
1223     /* adjust pointers so that the first 2 arguments to ITE are regular */
1224     if (Cudd_IsComplement(f) != 0) {    /* ITE(!F,G,H) = ITE(F,H,G) */
1225         f = Cudd_Not(f);
1226         r = g;
1227         g = h;
1228         h = r;
1229         change = 1;
1230     }
1231     comple = 0;
1232     if (Cudd_IsComplement(g) != 0) {    /* ITE(F,!G,H) = !ITE(F,G,!H) */
1233         g = Cudd_Not(g);
1234         h = Cudd_Not(h);
1235         change = 1;
1236         comple = 1;
1237     }
1238     if (change != 0) {
1239         *fp = f;
1240         *gp = g;
1241         *hp = h;
1242     }
1243     *topfp = cuddI(dd,f->index);
1244     *topgp = cuddI(dd,g->index);
1245     *tophp = cuddI(dd,Cudd_Regular(h)->index);
1246
1247     return(comple);
1248
1249 } /* end of bddVarToCanonical */
1250
1251
1252 /**Function********************************************************************
1253
1254   Synopsis [Picks unique member from equiv expressions.]
1255
1256   Description [Makes sure the first two pointers are regular.  This
1257   mat require the complementation of the result, which is signaled by
1258   returning 1 instead of 0.  This function is simpler than the general
1259   case because it assumes that no two arguments are the same or
1260   complementary, and no argument is constant.]
1261
1262   SideEffects [None]
1263
1264   SeeAlso     [bddVarToConst bddVarToCanonical]
1265
1266 ******************************************************************************/
1267 static int
1268 bddVarToCanonicalSimple(
1269   DdManager * dd,
1270   DdNode ** fp,
1271   DdNode ** gp,
1272   DdNode ** hp,
1273   unsigned int * topfp,
1274   unsigned int * topgp,
1275   unsigned int * tophp)
1276 {
1277     register DdNode             *r, *f, *g, *h;
1278     int                         comple, change;
1279
1280     f = *fp;
1281     g = *gp;
1282     h = *hp;
1283
1284     change = 0;
1285
1286     /* adjust pointers so that the first 2 arguments to ITE are regular */
1287     if (Cudd_IsComplement(f)) { /* ITE(!F,G,H) = ITE(F,H,G) */
1288         f = Cudd_Not(f);
1289         r = g;
1290         g = h;
1291         h = r;
1292         change = 1;
1293     }
1294     comple = 0;
1295     if (Cudd_IsComplement(g)) { /* ITE(F,!G,H) = !ITE(F,G,!H) */
1296         g = Cudd_Not(g);
1297         h = Cudd_Not(h);
1298         change = 1;
1299         comple = 1;
1300     }
1301     if (change) {
1302         *fp = f;
1303         *gp = g;
1304         *hp = h;
1305     }
1306
1307     /* Here we can skip the use of cuddI, because the operands are known
1308     ** to be non-constant.
1309     */
1310     *topfp = dd->perm[f->index];
1311     *topgp = dd->perm[g->index];
1312     *tophp = dd->perm[Cudd_Regular(h)->index];
1313
1314     return(comple);
1315
1316 } /* end of bddVarToCanonicalSimple */
1317