distr/cudd/cuddBddAbs.c

   1 /**CFile***********************************************************************
   2
   3   FileName    [cuddBddAbs.c]
   4
   5   PackageName [cudd]
   6
   7   Synopsis    [Quantification functions for BDDs.]
   8
   9   Description [External procedures included in this module:
  10                 <ul>
  11                 <li> Cudd_bddExistAbstract()
  12                 <li> Cudd_bddXorExistAbstract()
  13                 <li> Cudd_bddUnivAbstract()
  14                 <li> Cudd_bddBooleanDiff()
  15                 <li> Cudd_bddVarIsDependent()
  16                 </ul>
  17         Internal procedures included in this module:
  18                 <ul>
  19                 <li> cuddBddExistAbstractRecur()
  20                 <li> cuddBddXorExistAbstractRecur()
  21                 <li> cuddBddBooleanDiffRecur()
  22                 </ul>
  23         Static procedures included in this module:
  24                 <ul>
  25                 <li> bddCheckPositiveCube()
  26                 </ul>
  27                 ]
  28
  29   Author      [Fabio Somenzi]
  30
  31   Copyright   [Copyright (c) 1995-2004, Regents of the University of Colorado
  32
  33   All rights reserved.
  34
  35   Redistribution and use in source and binary forms, with or without
  36   modification, are permitted provided that the following conditions
  37   are met:
  38
  39   Redistributions of source code must retain the above copyright
  40   notice, this list of conditions and the following disclaimer.
  41
  42   Redistributions in binary form must reproduce the above copyright
  43   notice, this list of conditions and the following disclaimer in the
  44   documentation and/or other materials provided with the distribution.
  45
  46   Neither the name of the University of Colorado nor the names of its
  47   contributors may be used to endorse or promote products derived from
  48   this software without specific prior written permission.
  49
  50   THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
  51   "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
  52   LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
  53   FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
  54   COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
  55   INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
  56   BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
  57   LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
  58   CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
  59   LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
  60   ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
  61   POSSIBILITY OF SUCH DAMAGE.]
  62
  63 ******************************************************************************/
  64
  65 #include "util.h"
  66 #include "cuddInt.h"
  67
  68
  69 /*---------------------------------------------------------------------------*/
  70 /* Constant declarations                                                     */
  71 /*---------------------------------------------------------------------------*/
  72
  73
  74 /*---------------------------------------------------------------------------*/
  75 /* Stucture declarations                                                     */
  76 /*---------------------------------------------------------------------------*/
  77
  78
  79 /*---------------------------------------------------------------------------*/
  80 /* Type declarations                                                         */
  81 /*---------------------------------------------------------------------------*/
  82
  83
  84 /*---------------------------------------------------------------------------*/
  85 /* Variable declarations                                                     */
  86 /*---------------------------------------------------------------------------*/
  87
  88 #ifndef lint
  89 static char rcsid[] DD_UNUSED = "$Id: cuddBddAbs.c,v 1.26 2004/08/13 18:04:46 fabio Exp $";
  90 #endif
  91
  92 /*---------------------------------------------------------------------------*/
  93 /* Macro declarations                                                        */
  94 /*---------------------------------------------------------------------------*/
  95
  96
  97 /**AutomaticStart*************************************************************/
  98
  99 /*---------------------------------------------------------------------------*/
 100 /* Static function prototypes                                                */
 101 /*---------------------------------------------------------------------------*/
 102
 103 static int bddCheckPositiveCube (DdManager *manager, DdNode *cube);
 104
 105 /**AutomaticEnd***************************************************************/
 106
 107
 108 /*---------------------------------------------------------------------------*/
 109 /* Definition of exported functions                                          */
 110 /*---------------------------------------------------------------------------*/
 111
 112
 113 /**Function********************************************************************
 114
 115   Synopsis [Existentially abstracts all the variables in cube from f.]
 116
 117   Description [Existentially abstracts all the variables in cube from f.
 118   Returns the abstracted BDD if successful; NULL otherwise.]
 119
 120   SideEffects [None]
 121
 122   SeeAlso     [Cudd_bddUnivAbstract Cudd_addExistAbstract]
 123
 124 ******************************************************************************/
 125 DdNode *
 126 Cudd_bddExistAbstract(
 127   DdManager * manager,
 128   DdNode * f,
 129   DdNode * cube)
 130 {
 131     DdNode *res;
 132
 133     if (bddCheckPositiveCube(manager, cube) == 0) {
 134         (void) fprintf(manager->err,
 135                        "Error: Can only abstract positive cubes\n");
 136         manager->errorCode = CUDD_INVALID_ARG;
 137         return(NULL);
 138     }
 139
 140     do {
 141         manager->reordered = 0;
 142         res = cuddBddExistAbstractRecur(manager, f, cube);
 143     } while (manager->reordered == 1);
 144
 145     return(res);
 146
 147 } /* end of Cudd_bddExistAbstract */
 148
 149
 150 /**Function********************************************************************
 151
 152   Synopsis [Takes the exclusive OR of two BDDs and simultaneously abstracts the
 153   variables in cube.]
 154
 155   Description [Takes the exclusive OR of two BDDs and simultaneously abstracts
 156   the variables in cube. The variables are existentially abstracted.  Returns a
 157   pointer to the result is successful; NULL otherwise.]
 158
 159   SideEffects [None]
 160
 161   SeeAlso     [Cudd_bddUnivAbstract Cudd_bddExistAbstract Cudd_bddAndAbstract]
 162
 163 ******************************************************************************/
 164 DdNode *
 165 Cudd_bddXorExistAbstract(
 166   DdManager * manager,
 167   DdNode * f,
 168   DdNode * g,
 169   DdNode * cube)
 170 {
 171     DdNode *res;
 172
 173     if (bddCheckPositiveCube(manager, cube) == 0) {
 174         (void) fprintf(manager->err,
 175                        "Error: Can only abstract positive cubes\n");
 176         manager->errorCode = CUDD_INVALID_ARG;
 177         return(NULL);
 178     }
 179
 180     do {
 181         manager->reordered = 0;
 182         res = cuddBddXorExistAbstractRecur(manager, f, g, cube);
 183     } while (manager->reordered == 1);
 184
 185     return(res);
 186
 187 } /* end of Cudd_bddXorExistAbstract */
 188
 189
 190 /**Function********************************************************************
 191
 192   Synopsis    [Universally abstracts all the variables in cube from f.]
 193
 194   Description [Universally abstracts all the variables in cube from f.
 195   Returns the abstracted BDD if successful; NULL otherwise.]
 196
 197   SideEffects [None]
 198
 199   SeeAlso     [Cudd_bddExistAbstract Cudd_addUnivAbstract]
 200
 201 ******************************************************************************/
 202 DdNode *
 203 Cudd_bddUnivAbstract(
 204   DdManager * manager,
 205   DdNode * f,
 206   DdNode * cube)
 207 {
 208     DdNode      *res;
 209
 210     if (bddCheckPositiveCube(manager, cube) == 0) {
 211         (void) fprintf(manager->err,
 212                        "Error: Can only abstract positive cubes\n");
 213         manager->errorCode = CUDD_INVALID_ARG;
 214         return(NULL);
 215     }
 216
 217     do {
 218         manager->reordered = 0;
 219         res = cuddBddExistAbstractRecur(manager, Cudd_Not(f), cube);
 220     } while (manager->reordered == 1);
 221     if (res != NULL) res = Cudd_Not(res);
 222
 223     return(res);
 224
 225 } /* end of Cudd_bddUnivAbstract */
 226
 227
 228 /**Function********************************************************************
 229
 230   Synopsis    [Computes the boolean difference of f with respect to x.]
 231
 232   Description [Computes the boolean difference of f with respect to the
 233   variable with index x.  Returns the BDD of the boolean difference if
 234   successful; NULL otherwise.]
 235
 236   SideEffects [None]
 237
 238   SeeAlso     []
 239
 240 ******************************************************************************/
 241 DdNode *
 242 Cudd_bddBooleanDiff(
 243   DdManager * manager,
 244   DdNode * f,
 245   int  x)
 246 {
 247     DdNode *res, *var;
 248
 249     /* If the variable is not currently in the manager, f cannot
 250     ** depend on it.
 251     */
 252     if (x >= manager->size) return(Cudd_Not(DD_ONE(manager)));
 253     var = manager->vars[x];
 254
 255     do {
 256         manager->reordered = 0;
 257         res = cuddBddBooleanDiffRecur(manager, Cudd_Regular(f), var);
 258     } while (manager->reordered == 1);
 259
 260     return(res);
 261
 262 } /* end of Cudd_bddBooleanDiff */
 263
 264
 265 /**Function********************************************************************
 266
 267   Synopsis    [Checks whether a variable is dependent on others in a
 268   function.]
 269
 270   Description [Checks whether a variable is dependent on others in a
 271   function.  Returns 1 if the variable is dependent; 0 otherwise. No
 272   new nodes are created.]
 273
 274   SideEffects [None]
 275
 276   SeeAlso     []
 277
 278 ******************************************************************************/
 279 int
 280 Cudd_bddVarIsDependent(
 281   DdManager *dd,                /* manager */
 282   DdNode *f,                    /* function */
 283   DdNode *var                   /* variable */)
 284 {
 285     DdNode *F, *res, *zero, *ft, *fe;
 286     unsigned topf, level;
 287     DD_CTFP cacheOp;
 288     int retval;
 289
 290     zero = Cudd_Not(DD_ONE(dd));
 291     if (Cudd_IsConstant(f)) return(f == zero);
 292
 293     /* From now on f is not constant. */
 294     F = Cudd_Regular(f);
 295     topf = (unsigned) dd->perm[F->index];
 296     level = (unsigned) dd->perm[var->index];
 297
 298     /* Check terminal case. If topf > index of var, f does not depend on var.
 299     ** Therefore, var is not dependent in f. */
 300     if (topf > level) {
 301         return(0);
 302     }
 303
 304     cacheOp = (DD_CTFP) Cudd_bddVarIsDependent;
 305     res = cuddCacheLookup2(dd,cacheOp,f,var);
 306     if (res != NULL) {
 307         return(res != zero);
 308     }
 309
 310     /* Compute cofactors. */
 311     ft = Cudd_NotCond(cuddT(F), f != F);
 312     fe = Cudd_NotCond(cuddE(F), f != F);
 313
 314     if (topf == level) {
 315         retval = Cudd_bddLeq(dd,ft,Cudd_Not(fe));
 316     } else {
 317         retval = Cudd_bddVarIsDependent(dd,ft,var) &&
 318             Cudd_bddVarIsDependent(dd,fe,var);
 319     }
 320
 321     cuddCacheInsert2(dd,cacheOp,f,var,Cudd_NotCond(zero,retval));
 322
 323     return(retval);
 324
 325 } /* Cudd_bddVarIsDependent */
 326
 327
 328 /*---------------------------------------------------------------------------*/
 329 /* Definition of internal functions                                          */
 330 /*---------------------------------------------------------------------------*/
 331
 332
 333 /**Function********************************************************************
 334
 335   Synopsis    [Performs the recursive steps of Cudd_bddExistAbstract.]
 336
 337   Description [Performs the recursive steps of Cudd_bddExistAbstract.
 338   Returns the BDD obtained by abstracting the variables
 339   of cube from f if successful; NULL otherwise. It is also used by
 340   Cudd_bddUnivAbstract.]
 341
 342   SideEffects [None]
 343
 344   SeeAlso     [Cudd_bddExistAbstract Cudd_bddUnivAbstract]
 345
 346 ******************************************************************************/
 347 DdNode *
 348 cuddBddExistAbstractRecur(
 349   DdManager * manager,
 350   DdNode * f,
 351   DdNode * cube)
 352 {
 353     DdNode      *F, *T, *E, *res, *res1, *res2, *one;
 354
 355     statLine(manager);
 356     one = DD_ONE(manager);
 357     F = Cudd_Regular(f);
 358
 359     /* Cube is guaranteed to be a cube at this point. */
 360     if (cube == one || F == one) {
 361         return(f);
 362     }
 363     /* From now on, f and cube are non-constant. */
 364
 365     /* Abstract a variable that does not appear in f. */
 366     while (manager->perm[F->index] > manager->perm[cube->index]) {
 367         cube = cuddT(cube);
 368         if (cube == one) return(f);
 369     }
 370
 371     /* Check the cache. */
 372     if (F->ref != 1 && (res = cuddCacheLookup2(manager, Cudd_bddExistAbstract, f, cube)) != NULL) {
 373         return(res);
 374     }
 375
 376     /* Compute the cofactors of f. */
 377     T = cuddT(F); E = cuddE(F);
 378     if (f != F) {
 379         T = Cudd_Not(T); E = Cudd_Not(E);
 380     }
 381
 382     /* If the two indices are the same, so are their levels. */
 383     if (F->index == cube->index) {
 384         if (T == one || E == one || T == Cudd_Not(E)) {
 385             return(one);
 386         }
 387         res1 = cuddBddExistAbstractRecur(manager, T, cuddT(cube));
 388         if (res1 == NULL) return(NULL);
 389         if (res1 == one) {
 390             if (F->ref != 1)
 391                 cuddCacheInsert2(manager, Cudd_bddExistAbstract, f, cube, one);
 392             return(one);
 393         }
 394         cuddRef(res1);
 395         res2 = cuddBddExistAbstractRecur(manager, E, cuddT(cube));
 396         if (res2 == NULL) {
 397             Cudd_IterDerefBdd(manager,res1);
 398             return(NULL);
 399         }
 400         cuddRef(res2);
 401         res = cuddBddAndRecur(manager, Cudd_Not(res1), Cudd_Not(res2));
 402         if (res == NULL) {
 403             Cudd_IterDerefBdd(manager, res1);
 404             Cudd_IterDerefBdd(manager, res2);
 405             return(NULL);
 406         }
 407         res = Cudd_Not(res);
 408         cuddRef(res);
 409         Cudd_IterDerefBdd(manager, res1);
 410         Cudd_IterDerefBdd(manager, res2);
 411         if (F->ref != 1)
 412             cuddCacheInsert2(manager, Cudd_bddExistAbstract, f, cube, res);
 413         cuddDeref(res);
 414         return(res);
 415     } else { /* if (cuddI(manager,F->index) < cuddI(manager,cube->index)) */
 416         res1 = cuddBddExistAbstractRecur(manager, T, cube);
 417         if (res1 == NULL) return(NULL);
 418         cuddRef(res1);
 419         res2 = cuddBddExistAbstractRecur(manager, E, cube);
 420         if (res2 == NULL) {
 421             Cudd_IterDerefBdd(manager, res1);
 422             return(NULL);
 423         }
 424         cuddRef(res2);
 425         /* ITE takes care of possible complementation of res1 and of the
 426         ** case in which res1 == res2. */
 427         res = cuddBddIteRecur(manager, manager->vars[F->index], res1, res2);
 428         if (res == NULL) {
 429             Cudd_IterDerefBdd(manager, res1);
 430             Cudd_IterDerefBdd(manager, res2);
 431             return(NULL);
 432         }
 433         cuddDeref(res1);
 434         cuddDeref(res2);
 435         if (F->ref != 1)
 436             cuddCacheInsert2(manager, Cudd_bddExistAbstract, f, cube, res);
 437         return(res);
 438     }
 439
 440 } /* end of cuddBddExistAbstractRecur */
 441
 442
 443 /**Function********************************************************************
 444
 445   Synopsis [Takes the exclusive OR of two BDDs and simultaneously abstracts the
 446   variables in cube.]
 447
 448   Description [Takes the exclusive OR of two BDDs and simultaneously abstracts
 449   the variables in cube. The variables are existentially abstracted.  Returns a
 450   pointer to the result is successful; NULL otherwise.]
 451
 452   SideEffects [None]
 453
 454   SeeAlso     [Cudd_bddAndAbstract]
 455
 456 ******************************************************************************/
 457 DdNode *
 458 cuddBddXorExistAbstractRecur(
 459   DdManager * manager,
 460   DdNode * f,
 461   DdNode * g,
 462   DdNode * cube)
 463 {
 464     DdNode *F, *fv, *fnv, *G, *gv, *gnv;
 465     DdNode *one, *zero, *r, *t, *e, *Cube;
 466     unsigned int topf, topg, topcube, top, index;
 467
 468     statLine(manager);
 469     one = DD_ONE(manager);
 470     zero = Cudd_Not(one);
 471
 472     /* Terminal cases. */
 473     if (f == g) {
 474         return(zero);
 475     }
 476     if (f == Cudd_Not(g)) {
 477         return(one);
 478     }
 479     if (cube == one) {
 480         return(cuddBddXorRecur(manager, f, g));
 481     }
 482     if (f == one) {
 483         return(cuddBddExistAbstractRecur(manager, Cudd_Not(g), cube));
 484     }
 485     if (g == one) {
 486         return(cuddBddExistAbstractRecur(manager, Cudd_Not(f), cube));
 487     }
 488     if (f == zero) {
 489         return(cuddBddExistAbstractRecur(manager, g, cube));
 490     }
 491     if (g == zero) {
 492         return(cuddBddExistAbstractRecur(manager, f, cube));
 493     }
 494
 495     /* At this point f, g, and cube are not constant. */
 496
 497     if (f > g) { /* Try to increase cache efficiency. */
 498         DdNode *tmp = f;
 499         f = g;
 500         g = tmp;
 501     }
 502
 503     /* Check cache. */
 504     r = cuddCacheLookup(manager, DD_BDD_XOR_EXIST_ABSTRACT_TAG, f, g, cube);
 505     if (r != NULL) {
 506         return(r);
 507     }
 508
 509     /* Here we can skip the use of cuddI, because the operands are known
 510     ** to be non-constant.
 511     */
 512     F = Cudd_Regular(f);
 513     topf = manager->perm[F->index];
 514     G = Cudd_Regular(g);
 515     topg = manager->perm[G->index];
 516     top = ddMin(topf, topg);
 517     topcube = manager->perm[cube->index];
 518
 519     if (topcube < top) {
 520         return(cuddBddXorExistAbstractRecur(manager, f, g, cuddT(cube)));
 521     }
 522     /* Now, topcube >= top. */
 523
 524     if (topf == top) {
 525         index = F->index;
 526         fv = cuddT(F);
 527         fnv = cuddE(F);
 528         if (Cudd_IsComplement(f)) {
 529             fv = Cudd_Not(fv);
 530             fnv = Cudd_Not(fnv);
 531         }
 532     } else {
 533         index = G->index;
 534         fv = fnv = f;
 535     }
 536
 537     if (topg == top) {
 538         gv = cuddT(G);
 539         gnv = cuddE(G);
 540         if (Cudd_IsComplement(g)) {
 541             gv = Cudd_Not(gv);
 542             gnv = Cudd_Not(gnv);
 543         }
 544     } else {
 545         gv = gnv = g;
 546     }
 547
 548     if (topcube == top) {
 549         Cube = cuddT(cube);
 550     } else {
 551         Cube = cube;
 552     }
 553
 554     t = cuddBddXorExistAbstractRecur(manager, fv, gv, Cube);
 555     if (t == NULL) return(NULL);
 556
 557     /* Special case: 1 OR anything = 1. Hence, no need to compute
 558     ** the else branch if t is 1.
 559     */
 560     if (t == one && topcube == top) {
 561         cuddCacheInsert(manager, DD_BDD_XOR_EXIST_ABSTRACT_TAG, f, g, cube, one);
 562         return(one);
 563     }
 564     cuddRef(t);
 565
 566     e = cuddBddXorExistAbstractRecur(manager, fnv, gnv, Cube);
 567     if (e == NULL) {
 568         Cudd_IterDerefBdd(manager, t);
 569         return(NULL);
 570     }
 571     cuddRef(e);
 572
 573     if (topcube == top) {       /* abstract */
 574         r = cuddBddAndRecur(manager, Cudd_Not(t), Cudd_Not(e));
 575         if (r == NULL) {
 576             Cudd_IterDerefBdd(manager, t);
 577             Cudd_IterDerefBdd(manager, e);
 578             return(NULL);
 579         }
 580         r = Cudd_Not(r);
 581         cuddRef(r);
 582         Cudd_IterDerefBdd(manager, t);
 583         Cudd_IterDerefBdd(manager, e);
 584         cuddDeref(r);
 585     } else if (t == e) {
 586         r = t;
 587         cuddDeref(t);
 588         cuddDeref(e);
 589     } else {
 590         if (Cudd_IsComplement(t)) {
 591             r = cuddUniqueInter(manager,(int)index,Cudd_Not(t),Cudd_Not(e));
 592             if (r == NULL) {
 593                 Cudd_IterDerefBdd(manager, t);
 594                 Cudd_IterDerefBdd(manager, e);
 595                 return(NULL);
 596             }
 597             r = Cudd_Not(r);
 598         } else {
 599             r = cuddUniqueInter(manager,(int)index,t,e);
 600             if (r == NULL) {
 601                 Cudd_IterDerefBdd(manager, t);
 602                 Cudd_IterDerefBdd(manager, e);
 603                 return(NULL);
 604             }
 605         }
 606         cuddDeref(e);
 607         cuddDeref(t);
 608     }
 609     cuddCacheInsert(manager, DD_BDD_XOR_EXIST_ABSTRACT_TAG, f, g, cube, r);
 610     return (r);
 611
 612 } /* end of cuddBddXorExistAbstractRecur */
 613
 614
 615 /**Function********************************************************************
 616
 617   Synopsis    [Performs the recursive steps of Cudd_bddBoleanDiff.]
 618
 619   Description [Performs the recursive steps of Cudd_bddBoleanDiff.
 620   Returns the BDD obtained by XORing the cofactors of f with respect to
 621   var if successful; NULL otherwise. Exploits the fact that dF/dx =
 622   dF'/dx.]
 623
 624   SideEffects [None]
 625
 626   SeeAlso     []
 627
 628 ******************************************************************************/
 629 DdNode *
 630 cuddBddBooleanDiffRecur(
 631   DdManager * manager,
 632   DdNode * f,
 633   DdNode * var)
 634 {
 635     DdNode *T, *E, *res, *res1, *res2;
 636
 637     statLine(manager);
 638     if (cuddI(manager,f->index) > manager->perm[var->index]) {
 639         /* f does not depend on var. */
 640         return(Cudd_Not(DD_ONE(manager)));
 641     }
 642
 643     /* From now on, f is non-constant. */
 644
 645     /* If the two indices are the same, so are their levels. */
 646     if (f->index == var->index) {
 647         res = cuddBddXorRecur(manager, cuddT(f), cuddE(f));
 648         return(res);
 649     }
 650
 651     /* From now on, cuddI(manager,f->index) < cuddI(manager,cube->index). */
 652
 653     /* Check the cache. */
 654     res = cuddCacheLookup2(manager, cuddBddBooleanDiffRecur, f, var);
 655     if (res != NULL) {
 656         return(res);
 657     }
 658
 659     /* Compute the cofactors of f. */
 660     T = cuddT(f); E = cuddE(f);
 661
 662     res1 = cuddBddBooleanDiffRecur(manager, T, var);
 663     if (res1 == NULL) return(NULL);
 664     cuddRef(res1);
 665     res2 = cuddBddBooleanDiffRecur(manager, Cudd_Regular(E), var);
 666     if (res2 == NULL) {
 667         Cudd_IterDerefBdd(manager, res1);
 668         return(NULL);
 669     }
 670     cuddRef(res2);
 671     /* ITE takes care of possible complementation of res1 and of the
 672     ** case in which res1 == res2. */
 673     res = cuddBddIteRecur(manager, manager->vars[f->index], res1, res2);
 674     if (res == NULL) {
 675         Cudd_IterDerefBdd(manager, res1);
 676         Cudd_IterDerefBdd(manager, res2);
 677         return(NULL);
 678     }
 679     cuddDeref(res1);
 680     cuddDeref(res2);
 681     cuddCacheInsert2(manager, cuddBddBooleanDiffRecur, f, var, res);
 682     return(res);
 683
 684 } /* end of cuddBddBooleanDiffRecur */
 685
 686
 687 /*---------------------------------------------------------------------------*/
 688 /* Definition of static functions                                            */
 689 /*---------------------------------------------------------------------------*/
 690
 691 /**Function********************************************************************
 692
 693   Synopsis [Checks whether cube is an BDD representing the product of
 694   positive literals.]
 695
 696   Description [Returns 1 in case of success; 0 otherwise.]
 697
 698   SideEffects [None]
 699
 700 ******************************************************************************/
 701 static int
 702 bddCheckPositiveCube(
 703   DdManager * manager,
 704   DdNode * cube)
 705 {
 706     if (Cudd_IsComplement(cube)) return(0);
 707     if (cube == DD_ONE(manager)) return(1);
 708     if (cuddIsConstant(cube)) return(0);
 709     if (cuddE(cube) == Cudd_Not(DD_ONE(manager))) {
 710         return(bddCheckPositiveCube(manager, cuddT(cube)));
 711     }
 712     return(0);
 713
 714 } /* end of bddCheckPositiveCube */
 715