distr/cudd/cuddZddIsop.c

   1 /**CFile***********************************************************************
   2
   3   FileName    [cuddZddIsop.c]
   4
   5   PackageName [cudd]
   6
   7   Synopsis    [Functions to find irredundant SOP covers as ZDDs from BDDs.]
   8
   9   Description [External procedures included in this module:
  10                     <ul>
  11                     <li> Cudd_bddIsop()
  12                     <li> Cudd_zddIsop()
  13                     <li> Cudd_MakeBddFromZddCover()
  14                     </ul>
  15                Internal procedures included in this module:
  16                     <ul>
  17                     <li> cuddBddIsop()
  18                     <li> cuddZddIsop()
  19                     <li> cuddMakeBddFromZddCover()
  20                     </ul>
  21                Static procedures included in this module:
  22                     <ul>
  23                     </ul>
  24               ]
  25
  26   SeeAlso     []
  27
  28   Author      [In-Ho Moon]
  29
  30   Copyright   [Copyright (c) 1995-2004, Regents of the University of Colorado
  31
  32   All rights reserved.
  33
  34   Redistribution and use in source and binary forms, with or without
  35   modification, are permitted provided that the following conditions
  36   are met:
  37
  38   Redistributions of source code must retain the above copyright
  39   notice, this list of conditions and the following disclaimer.
  40
  41   Redistributions in binary form must reproduce the above copyright
  42   notice, this list of conditions and the following disclaimer in the
  43   documentation and/or other materials provided with the distribution.
  44
  45   Neither the name of the University of Colorado nor the names of its
  46   contributors may be used to endorse or promote products derived from
  47   this software without specific prior written permission.
  48
  49   THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
  50   "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
  51   LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
  52   FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
  53   COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
  54   INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
  55   BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
  56   LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
  57   CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
  58   LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
  59   ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
  60   POSSIBILITY OF SUCH DAMAGE.]
  61
  62 ******************************************************************************/
  63
  64 #include "util.h"
  65 #include "cuddInt.h"
  66
  67 /*---------------------------------------------------------------------------*/
  68 /* Constant declarations                                                     */
  69 /*---------------------------------------------------------------------------*/
  70
  71
  72 /*---------------------------------------------------------------------------*/
  73 /* Stucture declarations                                                     */
  74 /*---------------------------------------------------------------------------*/
  75
  76
  77 /*---------------------------------------------------------------------------*/
  78 /* Type declarations                                                         */
  79 /*---------------------------------------------------------------------------*/
  80
  81
  82 /*---------------------------------------------------------------------------*/
  83 /* Variable declarations                                                     */
  84 /*---------------------------------------------------------------------------*/
  85
  86 #ifndef lint
  87 static char rcsid[] DD_UNUSED = "$Id: cuddZddIsop.c,v 1.20 2009/02/19 16:26:12 fabio Exp $";
  88 #endif
  89
  90 /*---------------------------------------------------------------------------*/
  91 /* Macro declarations                                                        */
  92 /*---------------------------------------------------------------------------*/
  93
  94
  95 /**AutomaticStart*************************************************************/
  96
  97 /*---------------------------------------------------------------------------*/
  98 /* Static function prototypes                                                */
  99 /*---------------------------------------------------------------------------*/
 100
 101
 102 /**AutomaticEnd***************************************************************/
 103
 104 /*---------------------------------------------------------------------------*/
 105 /* Definition of exported functions                                          */
 106 /*---------------------------------------------------------------------------*/
 107
 108 /**Function********************************************************************
 109
 110   Synopsis    [Computes an ISOP in ZDD form from BDDs.]
 111
 112   Description [Computes an irredundant sum of products (ISOP) in ZDD
 113   form from BDDs. The two BDDs L and U represent the lower bound and
 114   the upper bound, respectively, of the function. The ISOP uses two
 115   ZDD variables for each BDD variable: One for the positive literal,
 116   and one for the negative literal. These two variables should be
 117   adjacent in the ZDD order. The two ZDD variables corresponding to
 118   BDD variable <code>i</code> should have indices <code>2i</code> and
 119   <code>2i+1</code>.  The result of this procedure depends on the
 120   variable order. If successful, Cudd_zddIsop returns the BDD for
 121   the function chosen from the interval. The ZDD representing the
 122   irredundant cover is returned as a side effect in zdd_I. In case of
 123   failure, NULL is returned.]
 124
 125   SideEffects [zdd_I holds the pointer to the ZDD for the ISOP on
 126   successful return.]
 127
 128   SeeAlso     [Cudd_bddIsop Cudd_zddVarsFromBddVars]
 129
 130 ******************************************************************************/
 131 DdNode  *
 132 Cudd_zddIsop(
 133   DdManager * dd,
 134   DdNode * L,
 135   DdNode * U,
 136   DdNode ** zdd_I)
 137 {
 138     DdNode      *res;
 139     int         autoDynZ;
 140
 141     autoDynZ = dd->autoDynZ;
 142     dd->autoDynZ = 0;
 143
 144     do {
 145         dd->reordered = 0;
 146         res = cuddZddIsop(dd, L, U, zdd_I);
 147     } while (dd->reordered == 1);
 148     dd->autoDynZ = autoDynZ;
 149     return(res);
 150
 151 } /* end of Cudd_zddIsop */
 152
 153
 154 /**Function********************************************************************
 155
 156   Synopsis    [Computes a BDD in the interval between L and U with a
 157   simple sum-of-produuct cover.]
 158
 159   Description [Computes a BDD in the interval between L and U with a
 160   simple sum-of-produuct cover. This procedure is similar to
 161   Cudd_zddIsop, but it does not return the ZDD for the cover. Returns
 162   a pointer to the BDD if successful; NULL otherwise.]
 163
 164   SideEffects [None]
 165
 166   SeeAlso     [Cudd_zddIsop]
 167
 168 ******************************************************************************/
 169 DdNode  *
 170 Cudd_bddIsop(
 171   DdManager * dd,
 172   DdNode * L,
 173   DdNode * U)
 174 {
 175     DdNode      *res;
 176
 177     do {
 178         dd->reordered = 0;
 179         res = cuddBddIsop(dd, L, U);
 180     } while (dd->reordered == 1);
 181     return(res);
 182
 183 } /* end of Cudd_bddIsop */
 184
 185
 186 /**Function********************************************************************
 187
 188   Synopsis [Converts a ZDD cover to a BDD graph.]
 189
 190   Description [Converts a ZDD cover to a BDD graph. If successful, it
 191   returns a BDD node, otherwise it returns NULL.]
 192
 193   SideEffects []
 194
 195   SeeAlso     [cuddMakeBddFromZddCover]
 196
 197 ******************************************************************************/
 198 DdNode  *
 199 Cudd_MakeBddFromZddCover(
 200   DdManager * dd,
 201   DdNode * node)
 202 {
 203     DdNode      *res;
 204
 205     do {
 206         dd->reordered = 0;
 207         res = cuddMakeBddFromZddCover(dd, node);
 208     } while (dd->reordered == 1);
 209     return(res);
 210 } /* end of Cudd_MakeBddFromZddCover */
 211
 212
 213 /*---------------------------------------------------------------------------*/
 214 /* Definition of internal functions                                          */
 215 /*---------------------------------------------------------------------------*/
 216
 217
 218 /**Function********************************************************************
 219
 220   Synopsis [Performs the recursive step of Cudd_zddIsop.]
 221
 222   Description []
 223
 224   SideEffects [None]
 225
 226   SeeAlso     [Cudd_zddIsop]
 227
 228 ******************************************************************************/
 229 DdNode  *
 230 cuddZddIsop(
 231   DdManager * dd,
 232   DdNode * L,
 233   DdNode * U,
 234   DdNode ** zdd_I)
 235 {
 236     DdNode      *one = DD_ONE(dd);
 237     DdNode      *zero = Cudd_Not(one);
 238     DdNode      *zdd_one = DD_ONE(dd);
 239     DdNode      *zdd_zero = DD_ZERO(dd);
 240     int         v, top_l, top_u;
 241     DdNode      *Lsub0, *Usub0, *Lsub1, *Usub1, *Ld, *Ud;
 242     DdNode      *Lsuper0, *Usuper0, *Lsuper1, *Usuper1;
 243     DdNode      *Isub0, *Isub1, *Id;
 244     DdNode      *zdd_Isub0, *zdd_Isub1, *zdd_Id;
 245     DdNode      *x;
 246     DdNode      *term0, *term1, *sum;
 247     DdNode      *Lv, *Uv, *Lnv, *Unv;
 248     DdNode      *r, *y, *z;
 249     int         index;
 250     DD_CTFP     cacheOp;
 251
 252     statLine(dd);
 253     if (L == zero) {
 254         *zdd_I = zdd_zero;
 255         return(zero);
 256     }
 257     if (U == one) {
 258         *zdd_I = zdd_one;
 259         return(one);
 260     }
 261
 262     if (U == zero || L == one) {
 263         printf("*** ERROR : illegal condition for ISOP (U < L).\n");
 264         exit(1);
 265     }
 266
 267     /* Check the cache. We store two results for each recursive call.
 268     ** One is the BDD, and the other is the ZDD. Both are needed.
 269     ** Hence we need a double hit in the cache to terminate the
 270     ** recursion. Clearly, collisions may evict only one of the two
 271     ** results. */
 272     cacheOp = (DD_CTFP) cuddZddIsop;
 273     r = cuddCacheLookup2(dd, cuddBddIsop, L, U);
 274     if (r) {
 275         *zdd_I = cuddCacheLookup2Zdd(dd, cacheOp, L, U);
 276         if (*zdd_I)
 277             return(r);
 278         else {
 279             /* The BDD result may have been dead. In that case
 280             ** cuddCacheLookup2 would have called cuddReclaim,
 281             ** whose effects we now have to undo. */
 282             cuddRef(r);
 283             Cudd_RecursiveDeref(dd, r);
 284         }
 285     }
 286
 287     top_l = dd->perm[Cudd_Regular(L)->index];
 288     top_u = dd->perm[Cudd_Regular(U)->index];
 289     v = ddMin(top_l, top_u);
 290
 291     /* Compute cofactors. */
 292     if (top_l == v) {
 293         index = Cudd_Regular(L)->index;
 294         Lv = Cudd_T(L);
 295         Lnv = Cudd_E(L);
 296         if (Cudd_IsComplement(L)) {
 297             Lv = Cudd_Not(Lv);
 298             Lnv = Cudd_Not(Lnv);
 299         }
 300     }
 301     else {
 302         index = Cudd_Regular(U)->index;
 303         Lv = Lnv = L;
 304     }
 305
 306     if (top_u == v) {
 307         Uv = Cudd_T(U);
 308         Unv = Cudd_E(U);
 309         if (Cudd_IsComplement(U)) {
 310             Uv = Cudd_Not(Uv);
 311             Unv = Cudd_Not(Unv);
 312         }
 313     }
 314     else {
 315         Uv = Unv = U;
 316     }
 317
 318     Lsub0 = cuddBddAndRecur(dd, Lnv, Cudd_Not(Uv));
 319     if (Lsub0 == NULL)
 320         return(NULL);
 321     Cudd_Ref(Lsub0);
 322     Usub0 = Unv;
 323     Lsub1 = cuddBddAndRecur(dd, Lv, Cudd_Not(Unv));
 324     if (Lsub1 == NULL) {
 325         Cudd_RecursiveDeref(dd, Lsub0);
 326         return(NULL);
 327     }
 328     Cudd_Ref(Lsub1);
 329     Usub1 = Uv;
 330
 331     Isub0 = cuddZddIsop(dd, Lsub0, Usub0, &zdd_Isub0);
 332     if (Isub0 == NULL) {
 333         Cudd_RecursiveDeref(dd, Lsub0);
 334         Cudd_RecursiveDeref(dd, Lsub1);
 335         return(NULL);
 336     }
 337     /*
 338     if ((!cuddIsConstant(Cudd_Regular(Isub0))) &&
 339         (Cudd_Regular(Isub0)->index != zdd_Isub0->index / 2 ||
 340         dd->permZ[index * 2] > dd->permZ[zdd_Isub0->index])) {
 341         printf("*** ERROR : illegal permutation in ZDD. ***\n");
 342     }
 343     */
 344     Cudd_Ref(Isub0);
 345     Cudd_Ref(zdd_Isub0);
 346     Isub1 = cuddZddIsop(dd, Lsub1, Usub1, &zdd_Isub1);
 347     if (Isub1 == NULL) {
 348         Cudd_RecursiveDeref(dd, Lsub0);
 349         Cudd_RecursiveDeref(dd, Lsub1);
 350         Cudd_RecursiveDeref(dd, Isub0);
 351         Cudd_RecursiveDerefZdd(dd, zdd_Isub0);
 352         return(NULL);
 353     }
 354     /*
 355     if ((!cuddIsConstant(Cudd_Regular(Isub1))) &&
 356         (Cudd_Regular(Isub1)->index != zdd_Isub1->index / 2 ||
 357         dd->permZ[index * 2] > dd->permZ[zdd_Isub1->index])) {
 358         printf("*** ERROR : illegal permutation in ZDD. ***\n");
 359     }
 360     */
 361     Cudd_Ref(Isub1);
 362     Cudd_Ref(zdd_Isub1);
 363     Cudd_RecursiveDeref(dd, Lsub0);
 364     Cudd_RecursiveDeref(dd, Lsub1);
 365
 366     Lsuper0 = cuddBddAndRecur(dd, Lnv, Cudd_Not(Isub0));
 367     if (Lsuper0 == NULL) {
 368         Cudd_RecursiveDeref(dd, Isub0);
 369         Cudd_RecursiveDerefZdd(dd, zdd_Isub0);
 370         Cudd_RecursiveDeref(dd, Isub1);
 371         Cudd_RecursiveDerefZdd(dd, zdd_Isub1);
 372         return(NULL);
 373     }
 374     Cudd_Ref(Lsuper0);
 375     Lsuper1 = cuddBddAndRecur(dd, Lv, Cudd_Not(Isub1));
 376     if (Lsuper1 == NULL) {
 377         Cudd_RecursiveDeref(dd, Isub0);
 378         Cudd_RecursiveDerefZdd(dd, zdd_Isub0);
 379         Cudd_RecursiveDeref(dd, Isub1);
 380         Cudd_RecursiveDerefZdd(dd, zdd_Isub1);
 381         Cudd_RecursiveDeref(dd, Lsuper0);
 382         return(NULL);
 383     }
 384     Cudd_Ref(Lsuper1);
 385     Usuper0 = Unv;
 386     Usuper1 = Uv;
 387
 388     /* Ld = Lsuper0 + Lsuper1 */
 389     Ld = cuddBddAndRecur(dd, Cudd_Not(Lsuper0), Cudd_Not(Lsuper1));
 390     if (Ld == NULL) {
 391         Cudd_RecursiveDeref(dd, Isub0);
 392         Cudd_RecursiveDerefZdd(dd, zdd_Isub0);
 393         Cudd_RecursiveDeref(dd, Isub1);
 394         Cudd_RecursiveDerefZdd(dd, zdd_Isub1);
 395         Cudd_RecursiveDeref(dd, Lsuper0);
 396         Cudd_RecursiveDeref(dd, Lsuper1);
 397         return(NULL);
 398     }
 399     Ld = Cudd_Not(Ld);
 400     Cudd_Ref(Ld);
 401     /* Ud = Usuper0 * Usuper1 */
 402     Ud = cuddBddAndRecur(dd, Usuper0, Usuper1);
 403     if (Ud == NULL) {
 404         Cudd_RecursiveDeref(dd, Isub0);
 405         Cudd_RecursiveDerefZdd(dd, zdd_Isub0);
 406         Cudd_RecursiveDeref(dd, Isub1);
 407         Cudd_RecursiveDerefZdd(dd, zdd_Isub1);
 408         Cudd_RecursiveDeref(dd, Lsuper0);
 409         Cudd_RecursiveDeref(dd, Lsuper1);
 410         Cudd_RecursiveDeref(dd, Ld);
 411         return(NULL);
 412     }
 413     Cudd_Ref(Ud);
 414     Cudd_RecursiveDeref(dd, Lsuper0);
 415     Cudd_RecursiveDeref(dd, Lsuper1);
 416
 417     Id = cuddZddIsop(dd, Ld, Ud, &zdd_Id);
 418     if (Id == NULL) {
 419         Cudd_RecursiveDeref(dd, Isub0);
 420         Cudd_RecursiveDerefZdd(dd, zdd_Isub0);
 421         Cudd_RecursiveDeref(dd, Isub1);
 422         Cudd_RecursiveDerefZdd(dd, zdd_Isub1);
 423         Cudd_RecursiveDeref(dd, Ld);
 424         Cudd_RecursiveDeref(dd, Ud);
 425         return(NULL);
 426     }
 427     /*
 428     if ((!cuddIsConstant(Cudd_Regular(Id))) &&
 429         (Cudd_Regular(Id)->index != zdd_Id->index / 2 ||
 430         dd->permZ[index * 2] > dd->permZ[zdd_Id->index])) {
 431         printf("*** ERROR : illegal permutation in ZDD. ***\n");
 432     }
 433     */
 434     Cudd_Ref(Id);
 435     Cudd_Ref(zdd_Id);
 436     Cudd_RecursiveDeref(dd, Ld);
 437     Cudd_RecursiveDeref(dd, Ud);
 438
 439     x = cuddUniqueInter(dd, index, one, zero);
 440     if (x == NULL) {
 441         Cudd_RecursiveDeref(dd, Isub0);
 442         Cudd_RecursiveDerefZdd(dd, zdd_Isub0);
 443         Cudd_RecursiveDeref(dd, Isub1);
 444         Cudd_RecursiveDerefZdd(dd, zdd_Isub1);
 445         Cudd_RecursiveDeref(dd, Id);
 446         Cudd_RecursiveDerefZdd(dd, zdd_Id);
 447         return(NULL);
 448     }
 449     Cudd_Ref(x);
 450     /* term0 = x * Isub0 */
 451     term0 = cuddBddAndRecur(dd, Cudd_Not(x), Isub0);
 452     if (term0 == NULL) {
 453         Cudd_RecursiveDeref(dd, Isub0);
 454         Cudd_RecursiveDerefZdd(dd, zdd_Isub0);
 455         Cudd_RecursiveDeref(dd, Isub1);
 456         Cudd_RecursiveDerefZdd(dd, zdd_Isub1);
 457         Cudd_RecursiveDeref(dd, Id);
 458         Cudd_RecursiveDerefZdd(dd, zdd_Id);
 459         Cudd_RecursiveDeref(dd, x);
 460         return(NULL);
 461     }
 462     Cudd_Ref(term0);
 463     Cudd_RecursiveDeref(dd, Isub0);
 464     /* term1 = x * Isub1 */
 465     term1 = cuddBddAndRecur(dd, x, Isub1);
 466     if (term1 == NULL) {
 467         Cudd_RecursiveDerefZdd(dd, zdd_Isub0);
 468         Cudd_RecursiveDeref(dd, Isub1);
 469         Cudd_RecursiveDerefZdd(dd, zdd_Isub1);
 470         Cudd_RecursiveDeref(dd, Id);
 471         Cudd_RecursiveDerefZdd(dd, zdd_Id);
 472         Cudd_RecursiveDeref(dd, x);
 473         Cudd_RecursiveDeref(dd, term0);
 474         return(NULL);
 475     }
 476     Cudd_Ref(term1);
 477     Cudd_RecursiveDeref(dd, x);
 478     Cudd_RecursiveDeref(dd, Isub1);
 479     /* sum = term0 + term1 */
 480     sum = cuddBddAndRecur(dd, Cudd_Not(term0), Cudd_Not(term1));
 481     if (sum == NULL) {
 482         Cudd_RecursiveDerefZdd(dd, zdd_Isub0);
 483         Cudd_RecursiveDerefZdd(dd, zdd_Isub1);
 484         Cudd_RecursiveDeref(dd, Id);
 485         Cudd_RecursiveDerefZdd(dd, zdd_Id);
 486         Cudd_RecursiveDeref(dd, term0);
 487         Cudd_RecursiveDeref(dd, term1);
 488         return(NULL);
 489     }
 490     sum = Cudd_Not(sum);
 491     Cudd_Ref(sum);
 492     Cudd_RecursiveDeref(dd, term0);
 493     Cudd_RecursiveDeref(dd, term1);
 494     /* r = sum + Id */
 495     r = cuddBddAndRecur(dd, Cudd_Not(sum), Cudd_Not(Id));
 496     r = Cudd_NotCond(r, r != NULL);
 497     if (r == NULL) {
 498         Cudd_RecursiveDerefZdd(dd, zdd_Isub0);
 499         Cudd_RecursiveDerefZdd(dd, zdd_Isub1);
 500         Cudd_RecursiveDeref(dd, Id);
 501         Cudd_RecursiveDerefZdd(dd, zdd_Id);
 502         Cudd_RecursiveDeref(dd, sum);
 503         return(NULL);
 504     }
 505     Cudd_Ref(r);
 506     Cudd_RecursiveDeref(dd, sum);
 507     Cudd_RecursiveDeref(dd, Id);
 508
 509     if (zdd_Isub0 != zdd_zero) {
 510         z = cuddZddGetNodeIVO(dd, index * 2 + 1, zdd_Isub0, zdd_Id);
 511         if (z == NULL) {
 512             Cudd_RecursiveDerefZdd(dd, zdd_Isub0);
 513             Cudd_RecursiveDerefZdd(dd, zdd_Isub1);
 514             Cudd_RecursiveDerefZdd(dd, zdd_Id);
 515             Cudd_RecursiveDeref(dd, r);
 516             return(NULL);
 517         }
 518     }
 519     else {
 520         z = zdd_Id;
 521     }
 522     Cudd_Ref(z);
 523     if (zdd_Isub1 != zdd_zero) {
 524         y = cuddZddGetNodeIVO(dd, index * 2, zdd_Isub1, z);
 525         if (y == NULL) {
 526             Cudd_RecursiveDerefZdd(dd, zdd_Isub0);
 527             Cudd_RecursiveDerefZdd(dd, zdd_Isub1);
 528             Cudd_RecursiveDerefZdd(dd, zdd_Id);
 529             Cudd_RecursiveDeref(dd, r);
 530             Cudd_RecursiveDerefZdd(dd, z);
 531             return(NULL);
 532         }
 533     }
 534     else
 535         y = z;
 536     Cudd_Ref(y);
 537
 538     Cudd_RecursiveDerefZdd(dd, zdd_Isub0);
 539     Cudd_RecursiveDerefZdd(dd, zdd_Isub1);
 540     Cudd_RecursiveDerefZdd(dd, zdd_Id);
 541     Cudd_RecursiveDerefZdd(dd, z);
 542
 543     cuddCacheInsert2(dd, cuddBddIsop, L, U, r);
 544     cuddCacheInsert2(dd, cacheOp, L, U, y);
 545
 546     Cudd_Deref(r);
 547     Cudd_Deref(y);
 548     *zdd_I = y;
 549     /*
 550     if (Cudd_Regular(r)->index != y->index / 2) {
 551         printf("*** ERROR : mismatch in indices between BDD and ZDD. ***\n");
 552     }
 553     */
 554     return(r);
 555
 556 } /* end of cuddZddIsop */
 557
 558
 559 /**Function********************************************************************
 560
 561   Synopsis [Performs the recursive step of Cudd_bddIsop.]
 562
 563   Description []
 564
 565   SideEffects [None]
 566
 567   SeeAlso     [Cudd_bddIsop]
 568
 569 ******************************************************************************/
 570 DdNode  *
 571 cuddBddIsop(
 572   DdManager * dd,
 573   DdNode * L,
 574   DdNode * U)
 575 {
 576     DdNode      *one = DD_ONE(dd);
 577     DdNode      *zero = Cudd_Not(one);
 578     int         v, top_l, top_u;
 579     DdNode      *Lsub0, *Usub0, *Lsub1, *Usub1, *Ld, *Ud;
 580     DdNode      *Lsuper0, *Usuper0, *Lsuper1, *Usuper1;
 581     DdNode      *Isub0, *Isub1, *Id;
 582     DdNode      *x;
 583     DdNode      *term0, *term1, *sum;
 584     DdNode      *Lv, *Uv, *Lnv, *Unv;
 585     DdNode      *r;
 586     int         index;
 587
 588     statLine(dd);
 589     if (L == zero)
 590         return(zero);
 591     if (U == one)
 592         return(one);
 593
 594     /* Check cache */
 595     r = cuddCacheLookup2(dd, cuddBddIsop, L, U);
 596     if (r)
 597         return(r);
 598
 599     top_l = dd->perm[Cudd_Regular(L)->index];
 600     top_u = dd->perm[Cudd_Regular(U)->index];
 601     v = ddMin(top_l, top_u);
 602
 603     /* Compute cofactors */
 604     if (top_l == v) {
 605         index = Cudd_Regular(L)->index;
 606         Lv = Cudd_T(L);
 607         Lnv = Cudd_E(L);
 608         if (Cudd_IsComplement(L)) {
 609             Lv = Cudd_Not(Lv);
 610             Lnv = Cudd_Not(Lnv);
 611         }
 612     }
 613     else {
 614         index = Cudd_Regular(U)->index;
 615         Lv = Lnv = L;
 616     }
 617
 618     if (top_u == v) {
 619         Uv = Cudd_T(U);
 620         Unv = Cudd_E(U);
 621         if (Cudd_IsComplement(U)) {
 622             Uv = Cudd_Not(Uv);
 623             Unv = Cudd_Not(Unv);
 624         }
 625     }
 626     else {
 627         Uv = Unv = U;
 628     }
 629
 630     Lsub0 = cuddBddAndRecur(dd, Lnv, Cudd_Not(Uv));
 631     if (Lsub0 == NULL)
 632         return(NULL);
 633     Cudd_Ref(Lsub0);
 634     Usub0 = Unv;
 635     Lsub1 = cuddBddAndRecur(dd, Lv, Cudd_Not(Unv));
 636     if (Lsub1 == NULL) {
 637         Cudd_RecursiveDeref(dd, Lsub0);
 638         return(NULL);
 639     }
 640     Cudd_Ref(Lsub1);
 641     Usub1 = Uv;
 642
 643     Isub0 = cuddBddIsop(dd, Lsub0, Usub0);
 644     if (Isub0 == NULL) {
 645         Cudd_RecursiveDeref(dd, Lsub0);
 646         Cudd_RecursiveDeref(dd, Lsub1);
 647         return(NULL);
 648     }
 649     Cudd_Ref(Isub0);
 650     Isub1 = cuddBddIsop(dd, Lsub1, Usub1);
 651     if (Isub1 == NULL) {
 652         Cudd_RecursiveDeref(dd, Lsub0);
 653         Cudd_RecursiveDeref(dd, Lsub1);
 654         Cudd_RecursiveDeref(dd, Isub0);
 655         return(NULL);
 656     }
 657     Cudd_Ref(Isub1);
 658     Cudd_RecursiveDeref(dd, Lsub0);
 659     Cudd_RecursiveDeref(dd, Lsub1);
 660
 661     Lsuper0 = cuddBddAndRecur(dd, Lnv, Cudd_Not(Isub0));
 662     if (Lsuper0 == NULL) {
 663         Cudd_RecursiveDeref(dd, Isub0);
 664         Cudd_RecursiveDeref(dd, Isub1);
 665         return(NULL);
 666     }
 667     Cudd_Ref(Lsuper0);
 668     Lsuper1 = cuddBddAndRecur(dd, Lv, Cudd_Not(Isub1));
 669     if (Lsuper1 == NULL) {
 670         Cudd_RecursiveDeref(dd, Isub0);
 671         Cudd_RecursiveDeref(dd, Isub1);
 672         Cudd_RecursiveDeref(dd, Lsuper0);
 673         return(NULL);
 674     }
 675     Cudd_Ref(Lsuper1);
 676     Usuper0 = Unv;
 677     Usuper1 = Uv;
 678
 679     /* Ld = Lsuper0 + Lsuper1 */
 680     Ld = cuddBddAndRecur(dd, Cudd_Not(Lsuper0), Cudd_Not(Lsuper1));
 681     Ld = Cudd_NotCond(Ld, Ld != NULL);
 682     if (Ld == NULL) {
 683         Cudd_RecursiveDeref(dd, Isub0);
 684         Cudd_RecursiveDeref(dd, Isub1);
 685         Cudd_RecursiveDeref(dd, Lsuper0);
 686         Cudd_RecursiveDeref(dd, Lsuper1);
 687         return(NULL);
 688     }
 689     Cudd_Ref(Ld);
 690     Ud = cuddBddAndRecur(dd, Usuper0, Usuper1);
 691     if (Ud == NULL) {
 692         Cudd_RecursiveDeref(dd, Isub0);
 693         Cudd_RecursiveDeref(dd, Isub1);
 694         Cudd_RecursiveDeref(dd, Lsuper0);
 695         Cudd_RecursiveDeref(dd, Lsuper1);
 696         Cudd_RecursiveDeref(dd, Ld);
 697         return(NULL);
 698     }
 699     Cudd_Ref(Ud);
 700     Cudd_RecursiveDeref(dd, Lsuper0);
 701     Cudd_RecursiveDeref(dd, Lsuper1);
 702
 703     Id = cuddBddIsop(dd, Ld, Ud);
 704     if (Id == NULL) {
 705         Cudd_RecursiveDeref(dd, Isub0);
 706         Cudd_RecursiveDeref(dd, Isub1);
 707         Cudd_RecursiveDeref(dd, Ld);
 708         Cudd_RecursiveDeref(dd, Ud);
 709         return(NULL);
 710     }
 711     Cudd_Ref(Id);
 712     Cudd_RecursiveDeref(dd, Ld);
 713     Cudd_RecursiveDeref(dd, Ud);
 714
 715     x = cuddUniqueInter(dd, index, one, zero);
 716     if (x == NULL) {
 717         Cudd_RecursiveDeref(dd, Isub0);
 718         Cudd_RecursiveDeref(dd, Isub1);
 719         Cudd_RecursiveDeref(dd, Id);
 720         return(NULL);
 721     }
 722     Cudd_Ref(x);
 723     term0 = cuddBddAndRecur(dd, Cudd_Not(x), Isub0);
 724     if (term0 == NULL) {
 725         Cudd_RecursiveDeref(dd, Isub0);
 726         Cudd_RecursiveDeref(dd, Isub1);
 727         Cudd_RecursiveDeref(dd, Id);
 728         Cudd_RecursiveDeref(dd, x);
 729         return(NULL);
 730     }
 731     Cudd_Ref(term0);
 732     Cudd_RecursiveDeref(dd, Isub0);
 733     term1 = cuddBddAndRecur(dd, x, Isub1);
 734     if (term1 == NULL) {
 735         Cudd_RecursiveDeref(dd, Isub1);
 736         Cudd_RecursiveDeref(dd, Id);
 737         Cudd_RecursiveDeref(dd, x);
 738         Cudd_RecursiveDeref(dd, term0);
 739         return(NULL);
 740     }
 741     Cudd_Ref(term1);
 742     Cudd_RecursiveDeref(dd, x);
 743     Cudd_RecursiveDeref(dd, Isub1);
 744     /* sum = term0 + term1 */
 745     sum = cuddBddAndRecur(dd, Cudd_Not(term0), Cudd_Not(term1));
 746     sum = Cudd_NotCond(sum, sum != NULL);
 747     if (sum == NULL) {
 748         Cudd_RecursiveDeref(dd, Id);
 749         Cudd_RecursiveDeref(dd, term0);
 750         Cudd_RecursiveDeref(dd, term1);
 751         return(NULL);
 752     }
 753     Cudd_Ref(sum);
 754     Cudd_RecursiveDeref(dd, term0);
 755     Cudd_RecursiveDeref(dd, term1);
 756     /* r = sum + Id */
 757     r = cuddBddAndRecur(dd, Cudd_Not(sum), Cudd_Not(Id));
 758     r = Cudd_NotCond(r, r != NULL);
 759     if (r == NULL) {
 760         Cudd_RecursiveDeref(dd, Id);
 761         Cudd_RecursiveDeref(dd, sum);
 762         return(NULL);
 763     }
 764     Cudd_Ref(r);
 765     Cudd_RecursiveDeref(dd, sum);
 766     Cudd_RecursiveDeref(dd, Id);
 767
 768     cuddCacheInsert2(dd, cuddBddIsop, L, U, r);
 769
 770     Cudd_Deref(r);
 771     return(r);
 772
 773 } /* end of cuddBddIsop */
 774
 775
 776 /**Function********************************************************************
 777
 778   Synopsis [Converts a ZDD cover to a BDD graph.]
 779
 780   Description [Converts a ZDD cover to a BDD graph. If successful, it
 781   returns a BDD node, otherwise it returns NULL. It is a recursive
 782   algorithm as the following. First computes 3 cofactors of a ZDD cover;
 783   f1, f0 and fd. Second, compute BDDs(b1, b0 and bd) of f1, f0 and fd.
 784   Third, compute T=b1+bd and E=b0+bd. Fourth, compute ITE(v,T,E) where v
 785   is the variable which has the index of the top node of the ZDD cover.
 786   In this case, since the index of v can be larger than either one of T or
 787   one of E, cuddUniqueInterIVO is called, here IVO stands for
 788   independent variable ordering.]
 789
 790   SideEffects []
 791
 792   SeeAlso     [Cudd_MakeBddFromZddCover]
 793
 794 ******************************************************************************/
 795 DdNode  *
 796 cuddMakeBddFromZddCover(
 797   DdManager * dd,
 798   DdNode * node)
 799 {
 800     DdNode      *neW;
 801     int         v;
 802     DdNode      *f1, *f0, *fd;
 803     DdNode      *b1, *b0, *bd;
 804     DdNode      *T, *E;
 805
 806     statLine(dd);
 807     if (node == dd->one)
 808         return(dd->one);
 809     if (node == dd->zero)
 810         return(Cudd_Not(dd->one));
 811
 812     /* Check cache */
 813     neW = cuddCacheLookup1(dd, cuddMakeBddFromZddCover, node);
 814     if (neW)
 815         return(neW);
 816
 817     v = Cudd_Regular(node)->index;      /* either yi or zi */
 818     if (cuddZddGetCofactors3(dd, node, v, &f1, &f0, &fd)) return(NULL);
 819     Cudd_Ref(f1);
 820     Cudd_Ref(f0);
 821     Cudd_Ref(fd);
 822
 823     b1 = cuddMakeBddFromZddCover(dd, f1);
 824     if (!b1) {
 825         Cudd_RecursiveDerefZdd(dd, f1);
 826         Cudd_RecursiveDerefZdd(dd, f0);
 827         Cudd_RecursiveDerefZdd(dd, fd);
 828         return(NULL);
 829     }
 830     Cudd_Ref(b1);
 831     b0 = cuddMakeBddFromZddCover(dd, f0);
 832     if (!b0) {
 833         Cudd_RecursiveDerefZdd(dd, f1);
 834         Cudd_RecursiveDerefZdd(dd, f0);
 835         Cudd_RecursiveDerefZdd(dd, fd);
 836         Cudd_RecursiveDeref(dd, b1);
 837         return(NULL);
 838     }
 839     Cudd_Ref(b0);
 840     Cudd_RecursiveDerefZdd(dd, f1);
 841     Cudd_RecursiveDerefZdd(dd, f0);
 842     if (fd != dd->zero) {
 843         bd = cuddMakeBddFromZddCover(dd, fd);
 844         if (!bd) {
 845             Cudd_RecursiveDerefZdd(dd, fd);
 846             Cudd_RecursiveDeref(dd, b1);
 847             Cudd_RecursiveDeref(dd, b0);
 848             return(NULL);
 849         }
 850         Cudd_Ref(bd);
 851         Cudd_RecursiveDerefZdd(dd, fd);
 852
 853         T = cuddBddAndRecur(dd, Cudd_Not(b1), Cudd_Not(bd));
 854         if (!T) {
 855             Cudd_RecursiveDeref(dd, b1);
 856             Cudd_RecursiveDeref(dd, b0);
 857             Cudd_RecursiveDeref(dd, bd);
 858             return(NULL);
 859         }
 860         T = Cudd_NotCond(T, T != NULL);
 861         Cudd_Ref(T);
 862         Cudd_RecursiveDeref(dd, b1);
 863         E = cuddBddAndRecur(dd, Cudd_Not(b0), Cudd_Not(bd));
 864         if (!E) {
 865             Cudd_RecursiveDeref(dd, b0);
 866             Cudd_RecursiveDeref(dd, bd);
 867             Cudd_RecursiveDeref(dd, T);
 868             return(NULL);
 869         }
 870         E = Cudd_NotCond(E, E != NULL);
 871         Cudd_Ref(E);
 872         Cudd_RecursiveDeref(dd, b0);
 873         Cudd_RecursiveDeref(dd, bd);
 874     }
 875     else {
 876         Cudd_RecursiveDerefZdd(dd, fd);
 877         T = b1;
 878         E = b0;
 879     }
 880
 881     if (Cudd_IsComplement(T)) {
 882         neW = cuddUniqueInterIVO(dd, v / 2, Cudd_Not(T), Cudd_Not(E));
 883         if (!neW) {
 884             Cudd_RecursiveDeref(dd, T);
 885             Cudd_RecursiveDeref(dd, E);
 886             return(NULL);
 887         }
 888         neW = Cudd_Not(neW);
 889     }
 890     else {
 891         neW = cuddUniqueInterIVO(dd, v / 2, T, E);
 892         if (!neW) {
 893             Cudd_RecursiveDeref(dd, T);
 894             Cudd_RecursiveDeref(dd, E);
 895             return(NULL);
 896         }
 897     }
 898     Cudd_Ref(neW);
 899     Cudd_RecursiveDeref(dd, T);
 900     Cudd_RecursiveDeref(dd, E);
 901
 902     cuddCacheInsert1(dd, cuddMakeBddFromZddCover, node, neW);
 903     Cudd_Deref(neW);
 904     return(neW);
 905
 906 } /* end of cuddMakeBddFromZddCover */
 907
 908
 909 /*---------------------------------------------------------------------------*/
 910 /* Definition of static functions                                            */
 911 /*---------------------------------------------------------------------------*/