distr/cudd/cuddZddSetop.c

   1 /**CFile***********************************************************************
   2
   3   FileName    [cuddZddSetop.c]
   4
   5   PackageName [cudd]
   6
   7   Synopsis    [Set operations on ZDDs.]
   8
   9   Description [External procedures included in this module:
  10                     <ul>
  11                     <li> Cudd_zddIte()
  12                     <li> Cudd_zddUnion()
  13                     <li> Cudd_zddIntersect()
  14                     <li> Cudd_zddDiff()
  15                     <li> Cudd_zddDiffConst()
  16                     <li> Cudd_zddSubset1()
  17                     <li> Cudd_zddSubset0()
  18                     <li> Cudd_zddChange()
  19                     </ul>
  20                Internal procedures included in this module:
  21                     <ul>
  22                     <li> cuddZddIte()
  23                     <li> cuddZddUnion()
  24                     <li> cuddZddIntersect()
  25                     <li> cuddZddDiff()
  26                     <li> cuddZddChangeAux()
  27                     <li> cuddZddSubset1()
  28                     <li> cuddZddSubset0()
  29                     </ul>
  30                Static procedures included in this module:
  31                     <ul>
  32                     <li> zdd_subset1_aux()
  33                     <li> zdd_subset0_aux()
  34                     <li> zddVarToConst()
  35                     </ul>
  36               ]
  37
  38   SeeAlso     []
  39
  40   Author      [Hyong-Kyoon Shin, In-Ho Moon]
  41
  42   Copyright   [Copyright (c) 1995-2004, Regents of the University of Colorado
  43
  44   All rights reserved.
  45
  46   Redistribution and use in source and binary forms, with or without
  47   modification, are permitted provided that the following conditions
  48   are met:
  49
  50   Redistributions of source code must retain the above copyright
  51   notice, this list of conditions and the following disclaimer.
  52
  53   Redistributions in binary form must reproduce the above copyright
  54   notice, this list of conditions and the following disclaimer in the
  55   documentation and/or other materials provided with the distribution.
  56
  57   Neither the name of the University of Colorado nor the names of its
  58   contributors may be used to endorse or promote products derived from
  59   this software without specific prior written permission.
  60
  61   THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
  62   "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
  63   LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
  64   FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
  65   COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
  66   INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
  67   BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
  68   LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
  69   CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
  70   LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
  71   ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
  72   POSSIBILITY OF SUCH DAMAGE.]
  73
  74 ******************************************************************************/
  75
  76 #include "util.h"
  77 #include "cuddInt.h"
  78
  79 /*---------------------------------------------------------------------------*/
  80 /* 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: cuddZddSetop.c,v 1.25 2004/08/13 18:04:54 fabio Exp $";
 100 #endif
 101
 102 /*---------------------------------------------------------------------------*/
 103 /* Macro declarations                                                        */
 104 /*---------------------------------------------------------------------------*/
 105
 106 #ifdef __cplusplus
 107 extern "C" {
 108 #endif
 109
 110 /**AutomaticStart*************************************************************/
 111
 112 /*---------------------------------------------------------------------------*/
 113 /* Static function prototypes                                                */
 114 /*---------------------------------------------------------------------------*/
 115
 116 static DdNode * zdd_subset1_aux (DdManager *zdd, DdNode *P, DdNode *zvar);
 117 static DdNode * zdd_subset0_aux (DdManager *zdd, DdNode *P, DdNode *zvar);
 118 static void zddVarToConst (DdNode *f, DdNode **gp, DdNode **hp, DdNode *base, DdNode *empty);
 119
 120 /**AutomaticEnd***************************************************************/
 121
 122 #ifdef __cplusplus
 123 }
 124 #endif
 125
 126 /*---------------------------------------------------------------------------*/
 127 /* Definition of exported functions                                          */
 128 /*---------------------------------------------------------------------------*/
 129
 130
 131 /**Function********************************************************************
 132
 133   Synopsis [Computes the ITE of three ZDDs.]
 134
 135   Description [Computes the ITE of three ZDDs. Returns a pointer to the
 136   result if successful; NULL otherwise.]
 137
 138   SideEffects [None]
 139
 140   SeeAlso     []
 141
 142 ******************************************************************************/
 143 DdNode *
 144 Cudd_zddIte(
 145   DdManager * dd,
 146   DdNode * f,
 147   DdNode * g,
 148   DdNode * h)
 149 {
 150     DdNode *res;
 151
 152     do {
 153         dd->reordered = 0;
 154         res = cuddZddIte(dd, f, g, h);
 155     } while (dd->reordered == 1);
 156     return(res);
 157
 158 } /* end of Cudd_zddIte */
 159
 160
 161 /**Function********************************************************************
 162
 163   Synopsis [Computes the union of two ZDDs.]
 164
 165   Description [Computes the union of two ZDDs. Returns a pointer to the
 166   result if successful; NULL otherwise.]
 167
 168   SideEffects [None]
 169
 170   SeeAlso     []
 171
 172 ******************************************************************************/
 173 DdNode *
 174 Cudd_zddUnion(
 175   DdManager * dd,
 176   DdNode * P,
 177   DdNode * Q)
 178 {
 179     DdNode *res;
 180
 181     do {
 182         dd->reordered = 0;
 183         res = cuddZddUnion(dd, P, Q);
 184     } while (dd->reordered == 1);
 185     return(res);
 186
 187 } /* end of Cudd_zddUnion */
 188
 189
 190 /**Function********************************************************************
 191
 192   Synopsis [Computes the intersection of two ZDDs.]
 193
 194   Description [Computes the intersection of two ZDDs. Returns a pointer to
 195   the result if successful; NULL otherwise.]
 196
 197   SideEffects [None]
 198
 199   SeeAlso     []
 200
 201 ******************************************************************************/
 202 DdNode *
 203 Cudd_zddIntersect(
 204   DdManager * dd,
 205   DdNode * P,
 206   DdNode * Q)
 207 {
 208     DdNode *res;
 209
 210     do {
 211         dd->reordered = 0;
 212         res = cuddZddIntersect(dd, P, Q);
 213     } while (dd->reordered == 1);
 214     return(res);
 215
 216 } /* end of Cudd_zddIntersect */
 217
 218
 219 /**Function********************************************************************
 220
 221   Synopsis [Computes the difference of two ZDDs.]
 222
 223   Description [Computes the difference of two ZDDs. Returns a pointer to the
 224   result if successful; NULL otherwise.]
 225
 226   SideEffects [None]
 227
 228   SeeAlso     [Cudd_zddDiffConst]
 229
 230 ******************************************************************************/
 231 DdNode *
 232 Cudd_zddDiff(
 233   DdManager * dd,
 234   DdNode * P,
 235   DdNode * Q)
 236 {
 237     DdNode *res;
 238
 239     do {
 240         dd->reordered = 0;
 241         res = cuddZddDiff(dd, P, Q);
 242     } while (dd->reordered == 1);
 243     return(res);
 244
 245 } /* end of Cudd_zddDiff */
 246
 247
 248 /**Function********************************************************************
 249
 250   Synopsis [Performs the inclusion test for ZDDs (P implies Q).]
 251
 252   Description [Inclusion test for ZDDs (P implies Q). No new nodes are
 253   generated by this procedure. Returns empty if true;
 254   a valid pointer different from empty or DD_NON_CONSTANT otherwise.]
 255
 256   SideEffects [None]
 257
 258   SeeAlso     [Cudd_zddDiff]
 259
 260 ******************************************************************************/
 261 DdNode *
 262 Cudd_zddDiffConst(
 263   DdManager * zdd,
 264   DdNode * P,
 265   DdNode * Q)
 266 {
 267     int         p_top, q_top;
 268     DdNode      *empty = DD_ZERO(zdd), *t, *res;
 269     DdManager   *table = zdd;
 270
 271     statLine(zdd);
 272     if (P == empty)
 273         return(empty);
 274     if (Q == empty)
 275         return(P);
 276     if (P == Q)
 277         return(empty);
 278
 279     /* Check cache.  The cache is shared by cuddZddDiff(). */
 280     res = cuddCacheLookup2Zdd(table, cuddZddDiff, P, Q);
 281     if (res != NULL)
 282         return(res);
 283
 284     if (cuddIsConstant(P))
 285         p_top = P->index;
 286     else
 287         p_top = zdd->permZ[P->index];
 288     if (cuddIsConstant(Q))
 289         q_top = Q->index;
 290     else
 291         q_top = zdd->permZ[Q->index];
 292     if (p_top < q_top) {
 293         res = DD_NON_CONSTANT;
 294     } else if (p_top > q_top) {
 295         res = Cudd_zddDiffConst(zdd, P, cuddE(Q));
 296     } else {
 297         t = Cudd_zddDiffConst(zdd, cuddT(P), cuddT(Q));
 298         if (t != empty)
 299             res = DD_NON_CONSTANT;
 300         else
 301             res = Cudd_zddDiffConst(zdd, cuddE(P), cuddE(Q));
 302     }
 303
 304     cuddCacheInsert2(table, cuddZddDiff, P, Q, res);
 305
 306     return(res);
 307
 308 } /* end of Cudd_zddDiffConst */
 309
 310
 311 /**Function********************************************************************
 312
 313   Synopsis [Computes the positive cofactor of a ZDD w.r.t. a variable.]
 314
 315   Description [Computes the positive cofactor of a ZDD w.r.t. a
 316   variable. In terms of combinations, the result is the set of all
 317   combinations in which the variable is asserted. Returns a pointer to
 318   the result if successful; NULL otherwise.]
 319
 320   SideEffects [None]
 321
 322   SeeAlso     [Cudd_zddSubset0]
 323
 324 ******************************************************************************/
 325 DdNode *
 326 Cudd_zddSubset1(
 327   DdManager * dd,
 328   DdNode * P,
 329   int  var)
 330 {
 331     DdNode      *r;
 332
 333     do {
 334         dd->reordered = 0;
 335         r = cuddZddSubset1(dd, P, var);
 336     } while (dd->reordered == 1);
 337
 338     return(r);
 339
 340 } /* end of Cudd_zddSubset1 */
 341
 342
 343 /**Function********************************************************************
 344
 345   Synopsis [Computes the negative cofactor of a ZDD w.r.t. a variable.]
 346
 347   Description [Computes the negative cofactor of a ZDD w.r.t. a
 348   variable. In terms of combinations, the result is the set of all
 349   combinations in which the variable is negated. Returns a pointer to
 350   the result if successful; NULL otherwise.]
 351
 352   SideEffects [None]
 353
 354   SeeAlso     [Cudd_zddSubset1]
 355
 356 ******************************************************************************/
 357 DdNode *
 358 Cudd_zddSubset0(
 359   DdManager * dd,
 360   DdNode * P,
 361   int  var)
 362 {
 363     DdNode      *r;
 364
 365     do {
 366         dd->reordered = 0;
 367         r = cuddZddSubset0(dd, P, var);
 368     } while (dd->reordered == 1);
 369
 370     return(r);
 371
 372 } /* end of Cudd_zddSubset0 */
 373
 374
 375 /**Function********************************************************************
 376
 377   Synopsis [Substitutes a variable with its complement in a ZDD.]
 378
 379   Description [Substitutes a variable with its complement in a ZDD.
 380   returns a pointer to the result if successful; NULL otherwise.]
 381
 382   SideEffects [None]
 383
 384   SeeAlso     []
 385
 386 ******************************************************************************/
 387 DdNode *
 388 Cudd_zddChange(
 389   DdManager * dd,
 390   DdNode * P,
 391   int  var)
 392 {
 393     DdNode      *res;
 394
 395     if ((unsigned int) var >= CUDD_MAXINDEX - 1) return(NULL);
 396
 397     do {
 398         dd->reordered = 0;
 399         res = cuddZddChange(dd, P, var);
 400     } while (dd->reordered == 1);
 401     return(res);
 402
 403 } /* end of Cudd_zddChange */
 404
 405
 406 /*---------------------------------------------------------------------------*/
 407 /* Definition of internal functions                                          */
 408 /*---------------------------------------------------------------------------*/
 409
 410
 411 /**Function********************************************************************
 412
 413   Synopsis    [Performs the recursive step of Cudd_zddIte.]
 414
 415   Description []
 416
 417   SideEffects [None]
 418
 419   SeeAlso     []
 420
 421 ******************************************************************************/
 422 DdNode *
 423 cuddZddIte(
 424   DdManager * dd,
 425   DdNode * f,
 426   DdNode * g,
 427   DdNode * h)
 428 {
 429     DdNode *tautology, *empty;
 430     DdNode *r,*Gv,*Gvn,*Hv,*Hvn,*t,*e;
 431     unsigned int topf,topg,toph,v,top;
 432     int index;
 433
 434     statLine(dd);
 435     /* Trivial cases. */
 436     /* One variable cases. */
 437     if (f == (empty = DD_ZERO(dd))) {   /* ITE(0,G,H) = H */
 438         return(h);
 439     }
 440     topf = cuddIZ(dd,f->index);
 441     topg = cuddIZ(dd,g->index);
 442     toph = cuddIZ(dd,h->index);
 443     v = ddMin(topg,toph);
 444     top  = ddMin(topf,v);
 445
 446     tautology = (top == CUDD_MAXINDEX) ? DD_ONE(dd) : dd->univ[top];
 447     if (f == tautology) {                       /* ITE(1,G,H) = G */
 448         return(g);
 449     }
 450
 451     /* From now on, f is known to not be a constant. */
 452     zddVarToConst(f,&g,&h,tautology,empty);
 453
 454     /* Check remaining one variable cases. */
 455     if (g == h) {                       /* ITE(F,G,G) = G */
 456         return(g);
 457     }
 458
 459     if (g == tautology) {                       /* ITE(F,1,0) = F */
 460         if (h == empty) return(f);
 461     }
 462
 463     /* Check cache. */
 464     r = cuddCacheLookupZdd(dd,DD_ZDD_ITE_TAG,f,g,h);
 465     if (r != NULL) {
 466         return(r);
 467     }
 468
 469     /* Recompute these because they may have changed in zddVarToConst. */
 470     topg = cuddIZ(dd,g->index);
 471     toph = cuddIZ(dd,h->index);
 472     v = ddMin(topg,toph);
 473
 474     if (topf < v) {
 475         r = cuddZddIte(dd,cuddE(f),g,h);
 476         if (r == NULL) return(NULL);
 477     } else if (topf > v) {
 478         if (topg > v) {
 479             Gvn = g;
 480             index = h->index;
 481         } else {
 482             Gvn = cuddE(g);
 483             index = g->index;
 484         }
 485         if (toph > v) {
 486             Hv = empty; Hvn = h;
 487         } else {
 488             Hv = cuddT(h); Hvn = cuddE(h);
 489         }
 490         e = cuddZddIte(dd,f,Gvn,Hvn);
 491         if (e == NULL) return(NULL);
 492         cuddRef(e);
 493         r = cuddZddGetNode(dd,index,Hv,e);
 494         if (r == NULL) {
 495             Cudd_RecursiveDerefZdd(dd,e);
 496             return(NULL);
 497         }
 498         cuddDeref(e);
 499     } else {
 500         index = f->index;
 501         if (topg > v) {
 502             Gv = empty; Gvn = g;
 503         } else {
 504             Gv = cuddT(g); Gvn = cuddE(g);
 505         }
 506         if (toph > v) {
 507             Hv = empty; Hvn = h;
 508         } else {
 509             Hv = cuddT(h); Hvn = cuddE(h);
 510         }
 511         e = cuddZddIte(dd,cuddE(f),Gvn,Hvn);
 512         if (e == NULL) return(NULL);
 513         cuddRef(e);
 514         t = cuddZddIte(dd,cuddT(f),Gv,Hv);
 515         if (t == NULL) {
 516             Cudd_RecursiveDerefZdd(dd,e);
 517             return(NULL);
 518         }
 519         cuddRef(t);
 520         r = cuddZddGetNode(dd,index,t,e);
 521         if (r == NULL) {
 522             Cudd_RecursiveDerefZdd(dd,e);
 523             Cudd_RecursiveDerefZdd(dd,t);
 524             return(NULL);
 525         }
 526         cuddDeref(t);
 527         cuddDeref(e);
 528     }
 529
 530     cuddCacheInsert(dd,DD_ZDD_ITE_TAG,f,g,h,r);
 531
 532     return(r);
 533
 534 } /* end of cuddZddIte */
 535
 536
 537 /**Function********************************************************************
 538
 539   Synopsis [Performs the recursive step of Cudd_zddUnion.]
 540
 541   Description []
 542
 543   SideEffects [None]
 544
 545   SeeAlso     []
 546
 547 ******************************************************************************/
 548 DdNode *
 549 cuddZddUnion(
 550   DdManager * zdd,
 551   DdNode * P,
 552   DdNode * Q)
 553 {
 554     int         p_top, q_top;
 555     DdNode      *empty = DD_ZERO(zdd), *t, *e, *res;
 556     DdManager   *table = zdd;
 557
 558     statLine(zdd);
 559     if (P == empty)
 560         return(Q);
 561     if (Q == empty)
 562         return(P);
 563     if (P == Q)
 564         return(P);
 565
 566     /* Check cache */
 567     res = cuddCacheLookup2Zdd(table, cuddZddUnion, P, Q);
 568     if (res != NULL)
 569         return(res);
 570
 571     if (cuddIsConstant(P))
 572         p_top = P->index;
 573     else
 574         p_top = zdd->permZ[P->index];
 575     if (cuddIsConstant(Q))
 576         q_top = Q->index;
 577     else
 578         q_top = zdd->permZ[Q->index];
 579     if (p_top < q_top) {
 580         e = cuddZddUnion(zdd, cuddE(P), Q);
 581         if (e == NULL) return (NULL);
 582         cuddRef(e);
 583         res = cuddZddGetNode(zdd, P->index, cuddT(P), e);
 584         if (res == NULL) {
 585             Cudd_RecursiveDerefZdd(table, e);
 586             return(NULL);
 587         }
 588         cuddDeref(e);
 589     } else if (p_top > q_top) {
 590         e = cuddZddUnion(zdd, P, cuddE(Q));
 591         if (e == NULL) return(NULL);
 592         cuddRef(e);
 593         res = cuddZddGetNode(zdd, Q->index, cuddT(Q), e);
 594         if (res == NULL) {
 595             Cudd_RecursiveDerefZdd(table, e);
 596             return(NULL);
 597         }
 598         cuddDeref(e);
 599     } else {
 600         t = cuddZddUnion(zdd, cuddT(P), cuddT(Q));
 601         if (t == NULL) return(NULL);
 602         cuddRef(t);
 603         e = cuddZddUnion(zdd, cuddE(P), cuddE(Q));
 604         if (e == NULL) {
 605             Cudd_RecursiveDerefZdd(table, t);
 606             return(NULL);
 607         }
 608         cuddRef(e);
 609         res = cuddZddGetNode(zdd, P->index, t, e);
 610         if (res == NULL) {
 611             Cudd_RecursiveDerefZdd(table, t);
 612             Cudd_RecursiveDerefZdd(table, e);
 613             return(NULL);
 614         }
 615         cuddDeref(t);
 616         cuddDeref(e);
 617     }
 618
 619     cuddCacheInsert2(table, cuddZddUnion, P, Q, res);
 620
 621     return(res);
 622
 623 } /* end of cuddZddUnion */
 624
 625
 626 /**Function********************************************************************
 627
 628   Synopsis [Performs the recursive step of Cudd_zddIntersect.]
 629
 630   Description []
 631
 632   SideEffects [None]
 633
 634   SeeAlso     []
 635
 636 ******************************************************************************/
 637 DdNode *
 638 cuddZddIntersect(
 639   DdManager * zdd,
 640   DdNode * P,
 641   DdNode * Q)
 642 {
 643     int         p_top, q_top;
 644     DdNode      *empty = DD_ZERO(zdd), *t, *e, *res;
 645     DdManager   *table = zdd;
 646
 647     statLine(zdd);
 648     if (P == empty)
 649         return(empty);
 650     if (Q == empty)
 651         return(empty);
 652     if (P == Q)
 653         return(P);
 654
 655     /* Check cache. */
 656     res = cuddCacheLookup2Zdd(table, cuddZddIntersect, P, Q);
 657     if (res != NULL)
 658         return(res);
 659
 660     if (cuddIsConstant(P))
 661         p_top = P->index;
 662     else
 663         p_top = zdd->permZ[P->index];
 664     if (cuddIsConstant(Q))
 665         q_top = Q->index;
 666     else
 667         q_top = zdd->permZ[Q->index];
 668     if (p_top < q_top) {
 669         res = cuddZddIntersect(zdd, cuddE(P), Q);
 670         if (res == NULL) return(NULL);
 671     } else if (p_top > q_top) {
 672         res = cuddZddIntersect(zdd, P, cuddE(Q));
 673         if (res == NULL) return(NULL);
 674     } else {
 675         t = cuddZddIntersect(zdd, cuddT(P), cuddT(Q));
 676         if (t == NULL) return(NULL);
 677         cuddRef(t);
 678         e = cuddZddIntersect(zdd, cuddE(P), cuddE(Q));
 679         if (e == NULL) {
 680             Cudd_RecursiveDerefZdd(table, t);
 681             return(NULL);
 682         }
 683         cuddRef(e);
 684         res = cuddZddGetNode(zdd, P->index, t, e);
 685         if (res == NULL) {
 686             Cudd_RecursiveDerefZdd(table, t);
 687             Cudd_RecursiveDerefZdd(table, e);
 688             return(NULL);
 689         }
 690         cuddDeref(t);
 691         cuddDeref(e);
 692     }
 693
 694     cuddCacheInsert2(table, cuddZddIntersect, P, Q, res);
 695
 696     return(res);
 697
 698 } /* end of cuddZddIntersect */
 699
 700
 701 /**Function********************************************************************
 702
 703   Synopsis [Performs the recursive step of Cudd_zddDiff.]
 704
 705   Description []
 706
 707   SideEffects [None]
 708
 709   SeeAlso     []
 710
 711 ******************************************************************************/
 712 DdNode *
 713 cuddZddDiff(
 714   DdManager * zdd,
 715   DdNode * P,
 716   DdNode * Q)
 717 {
 718     int         p_top, q_top;
 719     DdNode      *empty = DD_ZERO(zdd), *t, *e, *res;
 720     DdManager   *table = zdd;
 721
 722     statLine(zdd);
 723     if (P == empty)
 724         return(empty);
 725     if (Q == empty)
 726         return(P);
 727     if (P == Q)
 728         return(empty);
 729
 730     /* Check cache.  The cache is shared by Cudd_zddDiffConst(). */
 731     res = cuddCacheLookup2Zdd(table, cuddZddDiff, P, Q);
 732     if (res != NULL && res != DD_NON_CONSTANT)
 733         return(res);
 734
 735     if (cuddIsConstant(P))
 736         p_top = P->index;
 737     else
 738         p_top = zdd->permZ[P->index];
 739     if (cuddIsConstant(Q))
 740         q_top = Q->index;
 741     else
 742         q_top = zdd->permZ[Q->index];
 743     if (p_top < q_top) {
 744         e = cuddZddDiff(zdd, cuddE(P), Q);
 745         if (e == NULL) return(NULL);
 746         cuddRef(e);
 747         res = cuddZddGetNode(zdd, P->index, cuddT(P), e);
 748         if (res == NULL) {
 749             Cudd_RecursiveDerefZdd(table, e);
 750             return(NULL);
 751         }
 752         cuddDeref(e);
 753     } else if (p_top > q_top) {
 754         res = cuddZddDiff(zdd, P, cuddE(Q));
 755         if (res == NULL) return(NULL);
 756     } else {
 757         t = cuddZddDiff(zdd, cuddT(P), cuddT(Q));
 758         if (t == NULL) return(NULL);
 759         cuddRef(t);
 760         e = cuddZddDiff(zdd, cuddE(P), cuddE(Q));
 761         if (e == NULL) {
 762             Cudd_RecursiveDerefZdd(table, t);
 763             return(NULL);
 764         }
 765         cuddRef(e);
 766         res = cuddZddGetNode(zdd, P->index, t, e);
 767         if (res == NULL) {
 768             Cudd_RecursiveDerefZdd(table, t);
 769             Cudd_RecursiveDerefZdd(table, e);
 770             return(NULL);
 771         }
 772         cuddDeref(t);
 773         cuddDeref(e);
 774     }
 775
 776     cuddCacheInsert2(table, cuddZddDiff, P, Q, res);
 777
 778     return(res);
 779
 780 } /* end of cuddZddDiff */
 781
 782
 783 /**Function********************************************************************
 784
 785   Synopsis [Performs the recursive step of Cudd_zddChange.]
 786
 787   Description []
 788
 789   SideEffects [None]
 790
 791   SeeAlso     []
 792
 793 ******************************************************************************/
 794 DdNode *
 795 cuddZddChangeAux(
 796   DdManager * zdd,
 797   DdNode * P,
 798   DdNode * zvar)
 799 {
 800     int         top_var, level;
 801     DdNode      *res, *t, *e;
 802     DdNode      *base = DD_ONE(zdd);
 803     DdNode      *empty = DD_ZERO(zdd);
 804
 805     statLine(zdd);
 806     if (P == empty)
 807         return(empty);
 808     if (P == base)
 809         return(zvar);
 810
 811     /* Check cache. */
 812     res = cuddCacheLookup2Zdd(zdd, cuddZddChangeAux, P, zvar);
 813     if (res != NULL)
 814         return(res);
 815
 816     top_var = zdd->permZ[P->index];
 817     level = zdd->permZ[zvar->index];
 818
 819     if (top_var > level) {
 820         res = cuddZddGetNode(zdd, zvar->index, P, DD_ZERO(zdd));
 821         if (res == NULL) return(NULL);
 822     } else if (top_var == level) {
 823         res = cuddZddGetNode(zdd, zvar->index, cuddE(P), cuddT(P));
 824         if (res == NULL) return(NULL);
 825     } else {
 826         t = cuddZddChangeAux(zdd, cuddT(P), zvar);
 827         if (t == NULL) return(NULL);
 828         cuddRef(t);
 829         e = cuddZddChangeAux(zdd, cuddE(P), zvar);
 830         if (e == NULL) {
 831             Cudd_RecursiveDerefZdd(zdd, t);
 832             return(NULL);
 833         }
 834         cuddRef(e);
 835         res = cuddZddGetNode(zdd, P->index, t, e);
 836         if (res == NULL) {
 837             Cudd_RecursiveDerefZdd(zdd, t);
 838             Cudd_RecursiveDerefZdd(zdd, e);
 839             return(NULL);
 840         }
 841         cuddDeref(t);
 842         cuddDeref(e);
 843     }
 844
 845     cuddCacheInsert2(zdd, cuddZddChangeAux, P, zvar, res);
 846
 847     return(res);
 848
 849 } /* end of cuddZddChangeAux */
 850
 851
 852 /**Function********************************************************************
 853
 854   Synopsis [Computes the positive cofactor of a ZDD w.r.t. a variable.]
 855
 856   Description [Computes the positive cofactor of a ZDD w.r.t. a
 857   variable. In terms of combinations, the result is the set of all
 858   combinations in which the variable is asserted. Returns a pointer to
 859   the result if successful; NULL otherwise. cuddZddSubset1 performs
 860   the same function as Cudd_zddSubset1, but does not restart if
 861   reordering has taken place. Therefore it can be called from within a
 862   recursive procedure.]
 863
 864   SideEffects [None]
 865
 866   SeeAlso     [cuddZddSubset0 Cudd_zddSubset1]
 867
 868 ******************************************************************************/
 869 DdNode *
 870 cuddZddSubset1(
 871   DdManager * dd,
 872   DdNode * P,
 873   int  var)
 874 {
 875     DdNode      *zvar, *r;
 876     DdNode      *base, *empty;
 877
 878     base = DD_ONE(dd);
 879     empty = DD_ZERO(dd);
 880
 881     zvar = cuddUniqueInterZdd(dd, var, base, empty);
 882     if (zvar == NULL) {
 883         return(NULL);
 884     } else {
 885         cuddRef(zvar);
 886         r = zdd_subset1_aux(dd, P, zvar);
 887         if (r == NULL) {
 888             Cudd_RecursiveDerefZdd(dd, zvar);
 889             return(NULL);
 890         }
 891         cuddRef(r);
 892         Cudd_RecursiveDerefZdd(dd, zvar);
 893     }
 894
 895     cuddDeref(r);
 896     return(r);
 897
 898 } /* end of cuddZddSubset1 */
 899
 900
 901 /**Function********************************************************************
 902
 903   Synopsis [Computes the negative cofactor of a ZDD w.r.t. a variable.]
 904
 905   Description [Computes the negative cofactor of a ZDD w.r.t. a
 906   variable. In terms of combinations, the result is the set of all
 907   combinations in which the variable is negated. Returns a pointer to
 908   the result if successful; NULL otherwise. cuddZddSubset0 performs
 909   the same function as Cudd_zddSubset0, but does not restart if
 910   reordering has taken place. Therefore it can be called from within a
 911   recursive procedure.]
 912
 913   SideEffects [None]
 914
 915   SeeAlso     [cuddZddSubset1 Cudd_zddSubset0]
 916
 917 ******************************************************************************/
 918 DdNode *
 919 cuddZddSubset0(
 920   DdManager * dd,
 921   DdNode * P,
 922   int  var)
 923 {
 924     DdNode      *zvar, *r;
 925     DdNode      *base, *empty;
 926
 927     base = DD_ONE(dd);
 928     empty = DD_ZERO(dd);
 929
 930     zvar = cuddUniqueInterZdd(dd, var, base, empty);
 931     if (zvar == NULL) {
 932         return(NULL);
 933     } else {
 934         cuddRef(zvar);
 935         r = zdd_subset0_aux(dd, P, zvar);
 936         if (r == NULL) {
 937             Cudd_RecursiveDerefZdd(dd, zvar);
 938             return(NULL);
 939         }
 940         cuddRef(r);
 941         Cudd_RecursiveDerefZdd(dd, zvar);
 942     }
 943
 944     cuddDeref(r);
 945     return(r);
 946
 947 } /* end of cuddZddSubset0 */
 948
 949
 950 /**Function********************************************************************
 951
 952   Synopsis [Substitutes a variable with its complement in a ZDD.]
 953
 954   Description [Substitutes a variable with its complement in a ZDD.
 955   returns a pointer to the result if successful; NULL
 956   otherwise. cuddZddChange performs the same function as
 957   Cudd_zddChange, but does not restart if reordering has taken
 958   place. Therefore it can be called from within a recursive
 959   procedure.]
 960
 961   SideEffects [None]
 962
 963   SeeAlso     [Cudd_zddChange]
 964
 965 ******************************************************************************/
 966 DdNode *
 967 cuddZddChange(
 968   DdManager * dd,
 969   DdNode * P,
 970   int  var)
 971 {
 972     DdNode      *zvar, *res;
 973
 974     zvar = cuddUniqueInterZdd(dd, var, DD_ONE(dd), DD_ZERO(dd));
 975     if (zvar == NULL) return(NULL);
 976     cuddRef(zvar);
 977
 978     res = cuddZddChangeAux(dd, P, zvar);
 979     if (res == NULL) {
 980         Cudd_RecursiveDerefZdd(dd,zvar);
 981         return(NULL);
 982     }
 983     cuddRef(res);
 984     Cudd_RecursiveDerefZdd(dd,zvar);
 985     cuddDeref(res);
 986     return(res);
 987
 988 } /* end of cuddZddChange */
 989
 990
 991 /*---------------------------------------------------------------------------*/
 992 /* Definition of static functions                                            */
 993 /*---------------------------------------------------------------------------*/
 994
 995
 996 /**Function********************************************************************
 997
 998   Synopsis [Performs the recursive step of Cudd_zddSubset1.]
 999
1000   Description []
1001
1002   SideEffects [None]
1003
1004   SeeAlso     []
1005
1006 ******************************************************************************/
1007 static DdNode *
1008 zdd_subset1_aux(
1009   DdManager * zdd,
1010   DdNode * P,
1011   DdNode * zvar)
1012 {
1013     int         top_var, level;
1014     DdNode      *res, *t, *e;
1015     DdNode      *empty;
1016
1017     statLine(zdd);
1018     empty = DD_ZERO(zdd);
1019
1020     /* Check cache. */
1021     res = cuddCacheLookup2Zdd(zdd, zdd_subset1_aux, P, zvar);
1022     if (res != NULL)
1023         return(res);
1024
1025     if (cuddIsConstant(P)) {
1026         res = empty;
1027         cuddCacheInsert2(zdd, zdd_subset1_aux, P, zvar, res);
1028         return(res);
1029     }
1030
1031     top_var = zdd->permZ[P->index];
1032     level = zdd->permZ[zvar->index];
1033
1034     if (top_var > level) {
1035         res = empty;
1036     } else if (top_var == level) {
1037         res = cuddT(P);
1038     } else {
1039         t = zdd_subset1_aux(zdd, cuddT(P), zvar);
1040         if (t == NULL) return(NULL);
1041         cuddRef(t);
1042         e = zdd_subset1_aux(zdd, cuddE(P), zvar);
1043         if (e == NULL) {
1044             Cudd_RecursiveDerefZdd(zdd, t);
1045             return(NULL);
1046         }
1047         cuddRef(e);
1048         res = cuddZddGetNode(zdd, P->index, t, e);
1049         if (res == NULL) {
1050             Cudd_RecursiveDerefZdd(zdd, t);
1051             Cudd_RecursiveDerefZdd(zdd, e);
1052             return(NULL);
1053         }
1054         cuddDeref(t);
1055         cuddDeref(e);
1056     }
1057
1058     cuddCacheInsert2(zdd, zdd_subset1_aux, P, zvar, res);
1059
1060     return(res);
1061
1062 } /* end of zdd_subset1_aux */
1063
1064
1065 /**Function********************************************************************
1066
1067   Synopsis [Performs the recursive step of Cudd_zddSubset0.]
1068
1069   Description []
1070
1071   SideEffects [None]
1072
1073   SeeAlso     []
1074
1075 ******************************************************************************/
1076 static DdNode *
1077 zdd_subset0_aux(
1078   DdManager * zdd,
1079   DdNode * P,
1080   DdNode * zvar)
1081 {
1082     int         top_var, level;
1083     DdNode      *res, *t, *e;
1084
1085     statLine(zdd);
1086
1087     /* Check cache. */
1088     res = cuddCacheLookup2Zdd(zdd, zdd_subset0_aux, P, zvar);
1089     if (res != NULL)
1090         return(res);
1091
1092     if (cuddIsConstant(P)) {
1093         res = P;
1094         cuddCacheInsert2(zdd, zdd_subset0_aux, P, zvar, res);
1095         return(res);
1096     }
1097
1098     top_var = zdd->permZ[P->index];
1099     level = zdd->permZ[zvar->index];
1100
1101     if (top_var > level) {
1102         res = P;
1103     }
1104     else if (top_var == level) {
1105         res = cuddE(P);
1106     }
1107     else {
1108         t = zdd_subset0_aux(zdd, cuddT(P), zvar);
1109         if (t == NULL) return(NULL);
1110         cuddRef(t);
1111         e = zdd_subset0_aux(zdd, cuddE(P), zvar);
1112         if (e == NULL) {
1113             Cudd_RecursiveDerefZdd(zdd, t);
1114             return(NULL);
1115         }
1116         cuddRef(e);
1117         res = cuddZddGetNode(zdd, P->index, t, e);
1118         if (res == NULL) {
1119             Cudd_RecursiveDerefZdd(zdd, t);
1120             Cudd_RecursiveDerefZdd(zdd, e);
1121             return(NULL);
1122         }
1123         cuddDeref(t);
1124         cuddDeref(e);
1125     }
1126
1127     cuddCacheInsert2(zdd, zdd_subset0_aux, P, zvar, res);
1128
1129     return(res);
1130
1131 } /* end of zdd_subset0_aux */
1132
1133
1134 /**Function********************************************************************
1135
1136   Synopsis    [Replaces variables with constants if possible (part of
1137   canonical form).]
1138
1139   Description []
1140
1141   SideEffects [None]
1142
1143   SeeAlso     []
1144
1145 ******************************************************************************/
1146 static void
1147 zddVarToConst(
1148   DdNode * f,
1149   DdNode ** gp,
1150   DdNode ** hp,
1151   DdNode * base,
1152   DdNode * empty)
1153 {
1154     DdNode *g = *gp;
1155     DdNode *h = *hp;
1156
1157     if (f == g) { /* ITE(F,F,H) = ITE(F,1,H) = F + H */
1158         *gp = base;
1159     }
1160
1161     if (f == h) { /* ITE(F,G,F) = ITE(F,G,0) = F * G */
1162         *hp = empty;
1163     }
1164
1165 } /* end of zddVarToConst */
1166