distr/cudd/cuddAddIte.c

   1 /**CFile***********************************************************************
   2
   3   FileName    [cuddAddIte.c]
   4
   5   PackageName [cudd]
   6
   7   Synopsis    [ADD ITE function and satellites.]
   8
   9   Description [External procedures included in this module:
  10                 <ul>
  11                 <li> Cudd_addIte()
  12                 <li> Cudd_addIteConstant()
  13                 <li> Cudd_addEvalConst()
  14                 <li> Cudd_addCmpl()
  15                 <li> Cudd_addLeq()
  16                 </ul>
  17         Internal procedures included in this module:
  18                 <ul>
  19                 <li> cuddAddIteRecur()
  20                 <li> cuddAddCmplRecur()
  21                 </ul>
  22         Static procedures included in this module:
  23                 <ul>
  24                 <li> addVarToConst()
  25                 </ul>]
  26
  27   Author      [Fabio Somenzi]
  28
  29   Copyright   [Copyright (c) 1995-2004, Regents of the University of Colorado
  30
  31   All rights reserved.
  32
  33   Redistribution and use in source and binary forms, with or without
  34   modification, are permitted provided that the following conditions
  35   are met:
  36
  37   Redistributions of source code must retain the above copyright
  38   notice, this list of conditions and the following disclaimer.
  39
  40   Redistributions in binary form must reproduce the above copyright
  41   notice, this list of conditions and the following disclaimer in the
  42   documentation and/or other materials provided with the distribution.
  43
  44   Neither the name of the University of Colorado nor the names of its
  45   contributors may be used to endorse or promote products derived from
  46   this software without specific prior written permission.
  47
  48   THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
  49   "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
  50   LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
  51   FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
  52   COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
  53   INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
  54   BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
  55   LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
  56   CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
  57   LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
  58   ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
  59   POSSIBILITY OF SUCH DAMAGE.]
  60
  61 ******************************************************************************/
  62
  63 #include "util.h"
  64 #include "cuddInt.h"
  65
  66 /*---------------------------------------------------------------------------*/
  67 /* Constant declarations                                                     */
  68 /*---------------------------------------------------------------------------*/
  69
  70
  71 /*---------------------------------------------------------------------------*/
  72 /* Stucture declarations                                                     */
  73 /*---------------------------------------------------------------------------*/
  74
  75
  76 /*---------------------------------------------------------------------------*/
  77 /* Type declarations                                                         */
  78 /*---------------------------------------------------------------------------*/
  79
  80
  81 /*---------------------------------------------------------------------------*/
  82 /* Variable declarations                                                     */
  83 /*---------------------------------------------------------------------------*/
  84
  85 #ifndef lint
  86 static char rcsid[] DD_UNUSED = "$Id: cuddAddIte.c,v 1.15 2004/08/13 18:04:45 fabio Exp $";
  87 #endif
  88
  89
  90 /*---------------------------------------------------------------------------*/
  91 /* Macro declarations                                                        */
  92 /*---------------------------------------------------------------------------*/
  93
  94
  95 /**AutomaticStart*************************************************************/
  96
  97 /*---------------------------------------------------------------------------*/
  98 /* Static function prototypes                                                */
  99 /*---------------------------------------------------------------------------*/
 100
 101 static void addVarToConst (DdNode *f, DdNode **gp, DdNode **hp, DdNode *one, DdNode *zero);
 102
 103 /**AutomaticEnd***************************************************************/
 104
 105
 106 /*---------------------------------------------------------------------------*/
 107 /* Definition of exported functions                                          */
 108 /*---------------------------------------------------------------------------*/
 109
 110
 111 /**Function********************************************************************
 112
 113   Synopsis    [Implements ITE(f,g,h).]
 114
 115   Description [Implements ITE(f,g,h). This procedure assumes that f is
 116   a 0-1 ADD.  Returns a pointer to the resulting ADD if successful; NULL
 117   otherwise.]
 118
 119   SideEffects [None]
 120
 121   SeeAlso     [Cudd_bddIte Cudd_addIteConstant Cudd_addApply]
 122
 123 ******************************************************************************/
 124 DdNode *
 125 Cudd_addIte(
 126   DdManager * dd,
 127   DdNode * f,
 128   DdNode * g,
 129   DdNode * h)
 130 {
 131     DdNode *res;
 132
 133     do {
 134         dd->reordered = 0;
 135         res = cuddAddIteRecur(dd,f,g,h);
 136     } while (dd->reordered == 1);
 137     return(res);
 138
 139 } /* end of Cudd_addIte */
 140
 141
 142 /**Function********************************************************************
 143
 144   Synopsis    [Implements ITEconstant for ADDs.]
 145
 146   Description [Implements ITEconstant for ADDs.  f must be a 0-1 ADD.
 147   Returns a pointer to the resulting ADD (which may or may not be
 148   constant) or DD_NON_CONSTANT. No new nodes are created. This function
 149   can be used, for instance, to check that g has a constant value
 150   (specified by h) whenever f is 1. If the constant value is unknown,
 151   then one should use Cudd_addEvalConst.]
 152
 153   SideEffects [None]
 154
 155   SeeAlso     [Cudd_addIte Cudd_addEvalConst Cudd_bddIteConstant]
 156
 157 ******************************************************************************/
 158 DdNode *
 159 Cudd_addIteConstant(
 160   DdManager * dd,
 161   DdNode * f,
 162   DdNode * g,
 163   DdNode * h)
 164 {
 165     DdNode *one,*zero;
 166     DdNode *Fv,*Fnv,*Gv,*Gnv,*Hv,*Hnv,*r,*t,*e;
 167     unsigned int topf,topg,toph,v;
 168
 169     statLine(dd);
 170     /* Trivial cases. */
 171     if (f == (one = DD_ONE(dd))) {      /* ITE(1,G,H) = G */
 172         return(g);
 173     }
 174     if (f == (zero = DD_ZERO(dd))) {    /* ITE(0,G,H) = H */
 175         return(h);
 176     }
 177
 178     /* From now on, f is known not to be a constant. */
 179     addVarToConst(f,&g,&h,one,zero);
 180
 181     /* Check remaining one variable cases. */
 182     if (g == h) {                       /* ITE(F,G,G) = G */
 183         return(g);
 184     }
 185     if (cuddIsConstant(g) && cuddIsConstant(h)) {
 186         return(DD_NON_CONSTANT);
 187     }
 188
 189     topf = cuddI(dd,f->index);
 190     topg = cuddI(dd,g->index);
 191     toph = cuddI(dd,h->index);
 192     v = ddMin(topg,toph);
 193
 194     /* ITE(F,G,H) = (x,G,H) (non constant) if F = (x,1,0), x < top(G,H). */
 195     if (topf < v && cuddIsConstant(cuddT(f)) && cuddIsConstant(cuddE(f))) {
 196         return(DD_NON_CONSTANT);
 197     }
 198
 199     /* Check cache. */
 200     r = cuddConstantLookup(dd,DD_ADD_ITE_CONSTANT_TAG,f,g,h);
 201     if (r != NULL) {
 202         return(r);
 203     }
 204
 205     /* Compute cofactors. */
 206     if (topf <= v) {
 207         v = ddMin(topf,v);      /* v = top_var(F,G,H) */
 208         Fv = cuddT(f); Fnv = cuddE(f);
 209     } else {
 210         Fv = Fnv = f;
 211     }
 212     if (topg == v) {
 213         Gv = cuddT(g); Gnv = cuddE(g);
 214     } else {
 215         Gv = Gnv = g;
 216     }
 217     if (toph == v) {
 218         Hv = cuddT(h); Hnv = cuddE(h);
 219     } else {
 220         Hv = Hnv = h;
 221     }
 222
 223     /* Recursive step. */
 224     t = Cudd_addIteConstant(dd,Fv,Gv,Hv);
 225     if (t == DD_NON_CONSTANT || !cuddIsConstant(t)) {
 226         cuddCacheInsert(dd, DD_ADD_ITE_CONSTANT_TAG, f, g, h, DD_NON_CONSTANT);
 227         return(DD_NON_CONSTANT);
 228     }
 229     e = Cudd_addIteConstant(dd,Fnv,Gnv,Hnv);
 230     if (e == DD_NON_CONSTANT || !cuddIsConstant(e) || t != e) {
 231         cuddCacheInsert(dd, DD_ADD_ITE_CONSTANT_TAG, f, g, h, DD_NON_CONSTANT);
 232         return(DD_NON_CONSTANT);
 233     }
 234     cuddCacheInsert(dd, DD_ADD_ITE_CONSTANT_TAG, f, g, h, t);
 235     return(t);
 236
 237 } /* end of Cudd_addIteConstant */
 238
 239
 240 /**Function********************************************************************
 241
 242   Synopsis    [Checks whether ADD g is constant whenever ADD f is 1.]
 243
 244   Description [Checks whether ADD g is constant whenever ADD f is 1.  f
 245   must be a 0-1 ADD.  Returns a pointer to the resulting ADD (which may
 246   or may not be constant) or DD_NON_CONSTANT. If f is identically 0,
 247   the check is assumed to be successful, and the background value is
 248   returned. No new nodes are created.]
 249
 250   SideEffects [None]
 251
 252   SeeAlso     [Cudd_addIteConstant Cudd_addLeq]
 253
 254 ******************************************************************************/
 255 DdNode *
 256 Cudd_addEvalConst(
 257   DdManager * dd,
 258   DdNode * f,
 259   DdNode * g)
 260 {
 261     DdNode *zero;
 262     DdNode *Fv,*Fnv,*Gv,*Gnv,*r,*t,*e;
 263     unsigned int topf,topg;
 264
 265 #ifdef DD_DEBUG
 266     assert(!Cudd_IsComplement(f));
 267 #endif
 268
 269     statLine(dd);
 270     /* Terminal cases. */
 271     if (f == DD_ONE(dd) || cuddIsConstant(g)) {
 272         return(g);
 273     }
 274     if (f == (zero = DD_ZERO(dd))) {
 275         return(dd->background);
 276     }
 277
 278 #ifdef DD_DEBUG
 279     assert(!cuddIsConstant(f));
 280 #endif
 281     /* From now on, f and g are known not to be constants. */
 282
 283     topf = cuddI(dd,f->index);
 284     topg = cuddI(dd,g->index);
 285
 286     /* Check cache. */
 287     r = cuddConstantLookup(dd,DD_ADD_EVAL_CONST_TAG,f,g,g);
 288     if (r != NULL) {
 289         return(r);
 290     }
 291
 292     /* Compute cofactors. */
 293     if (topf <= topg) {
 294         Fv = cuddT(f); Fnv = cuddE(f);
 295     } else {
 296         Fv = Fnv = f;
 297     }
 298     if (topg <= topf) {
 299         Gv = cuddT(g); Gnv = cuddE(g);
 300     } else {
 301         Gv = Gnv = g;
 302     }
 303
 304     /* Recursive step. */
 305     if (Fv != zero) {
 306         t = Cudd_addEvalConst(dd,Fv,Gv);
 307         if (t == DD_NON_CONSTANT || !cuddIsConstant(t)) {
 308             cuddCacheInsert2(dd, Cudd_addEvalConst, f, g, DD_NON_CONSTANT);
 309             return(DD_NON_CONSTANT);
 310         }
 311         if (Fnv != zero) {
 312             e = Cudd_addEvalConst(dd,Fnv,Gnv);
 313             if (e == DD_NON_CONSTANT || !cuddIsConstant(e) || t != e) {
 314                 cuddCacheInsert2(dd, Cudd_addEvalConst, f, g, DD_NON_CONSTANT);
 315                 return(DD_NON_CONSTANT);
 316             }
 317         }
 318         cuddCacheInsert2(dd,Cudd_addEvalConst,f,g,t);
 319         return(t);
 320     } else { /* Fnv must be != zero */
 321         e = Cudd_addEvalConst(dd,Fnv,Gnv);
 322         cuddCacheInsert2(dd, Cudd_addEvalConst, f, g, e);
 323         return(e);
 324     }
 325
 326 } /* end of Cudd_addEvalConst */
 327
 328
 329 /**Function********************************************************************
 330
 331   Synopsis    [Computes the complement of an ADD a la C language.]
 332
 333   Description [Computes the complement of an ADD a la C language: The
 334   complement of 0 is 1 and the complement of everything else is 0.
 335   Returns a pointer to the resulting ADD if successful; NULL otherwise.]
 336
 337   SideEffects [None]
 338
 339   SeeAlso     [Cudd_addNegate]
 340
 341 ******************************************************************************/
 342 DdNode *
 343 Cudd_addCmpl(
 344   DdManager * dd,
 345   DdNode * f)
 346 {
 347     DdNode *res;
 348
 349     do {
 350         dd->reordered = 0;
 351         res = cuddAddCmplRecur(dd,f);
 352     } while (dd->reordered == 1);
 353     return(res);
 354
 355 } /* end of Cudd_addCmpl */
 356
 357
 358 /**Function********************************************************************
 359
 360   Synopsis    [Determines whether f is less than or equal to g.]
 361
 362   Description [Returns 1 if f is less than or equal to g; 0 otherwise.
 363   No new nodes are created. This procedure works for arbitrary ADDs.
 364   For 0-1 ADDs Cudd_addEvalConst is more efficient.]
 365
 366   SideEffects [None]
 367
 368   SeeAlso     [Cudd_addIteConstant Cudd_addEvalConst Cudd_bddLeq]
 369
 370 ******************************************************************************/
 371 int
 372 Cudd_addLeq(
 373   DdManager * dd,
 374   DdNode * f,
 375   DdNode * g)
 376 {
 377     DdNode *tmp, *fv, *fvn, *gv, *gvn;
 378     unsigned int topf, topg, res;
 379
 380     /* Terminal cases. */
 381     if (f == g) return(1);
 382
 383     statLine(dd);
 384     if (cuddIsConstant(f)) {
 385         if (cuddIsConstant(g)) return(cuddV(f) <= cuddV(g));
 386         if (f == DD_MINUS_INFINITY(dd)) return(1);
 387         if (f == DD_PLUS_INFINITY(dd)) return(0); /* since f != g */
 388     }
 389     if (g == DD_PLUS_INFINITY(dd)) return(1);
 390     if (g == DD_MINUS_INFINITY(dd)) return(0); /* since f != g */
 391
 392     /* Check cache. */
 393     tmp = cuddCacheLookup2(dd,(DD_CTFP)Cudd_addLeq,f,g);
 394     if (tmp != NULL) {
 395         return(tmp == DD_ONE(dd));
 396     }
 397
 398     /* Compute cofactors. One of f and g is not constant. */
 399     topf = cuddI(dd,f->index);
 400     topg = cuddI(dd,g->index);
 401     if (topf <= topg) {
 402         fv = cuddT(f); fvn = cuddE(f);
 403     } else {
 404         fv = fvn = f;
 405     }
 406     if (topg <= topf) {
 407         gv = cuddT(g); gvn = cuddE(g);
 408     } else {
 409         gv = gvn = g;
 410     }
 411
 412     res = Cudd_addLeq(dd,fvn,gvn) && Cudd_addLeq(dd,fv,gv);
 413
 414     /* Store result in cache and return. */
 415     cuddCacheInsert2(dd,(DD_CTFP) Cudd_addLeq,f,g,
 416                      Cudd_NotCond(DD_ONE(dd),res==0));
 417     return(res);
 418
 419 } /* end of Cudd_addLeq */
 420
 421
 422 /*---------------------------------------------------------------------------*/
 423 /* Definition of internal functions                                          */
 424 /*---------------------------------------------------------------------------*/
 425
 426
 427 /**Function********************************************************************
 428
 429   Synopsis    [Implements the recursive step of Cudd_addIte(f,g,h).]
 430
 431   Description [Implements the recursive step of Cudd_addIte(f,g,h).
 432   Returns a pointer to the resulting ADD if successful; NULL
 433   otherwise.]
 434
 435   SideEffects [None]
 436
 437   SeeAlso     [Cudd_addIte]
 438
 439 ******************************************************************************/
 440 DdNode *
 441 cuddAddIteRecur(
 442   DdManager * dd,
 443   DdNode * f,
 444   DdNode * g,
 445   DdNode * h)
 446 {
 447     DdNode *one,*zero;
 448     DdNode *r,*Fv,*Fnv,*Gv,*Gnv,*Hv,*Hnv,*t,*e;
 449     unsigned int topf,topg,toph,v;
 450     int index;
 451
 452     statLine(dd);
 453     /* Trivial cases. */
 454
 455     /* One variable cases. */
 456     if (f == (one = DD_ONE(dd))) {      /* ITE(1,G,H) = G */
 457         return(g);
 458     }
 459     if (f == (zero = DD_ZERO(dd))) {    /* ITE(0,G,H) = H */
 460         return(h);
 461     }
 462
 463     /* From now on, f is known to not be a constant. */
 464     addVarToConst(f,&g,&h,one,zero);
 465
 466     /* Check remaining one variable cases. */
 467     if (g == h) {                       /* ITE(F,G,G) = G */
 468         return(g);
 469     }
 470
 471     if (g == one) {                     /* ITE(F,1,0) = F */
 472         if (h == zero) return(f);
 473     }
 474
 475     topf = cuddI(dd,f->index);
 476     topg = cuddI(dd,g->index);
 477     toph = cuddI(dd,h->index);
 478     v = ddMin(topg,toph);
 479
 480     /* A shortcut: ITE(F,G,H) = (x,G,H) if F=(x,1,0), x < top(G,H). */
 481     if (topf < v && cuddT(f) == one && cuddE(f) == zero) {
 482         r = cuddUniqueInter(dd,(int)f->index,g,h);
 483         return(r);
 484     }
 485     if (topf < v && cuddT(f) == zero && cuddE(f) == one) {
 486         r = cuddUniqueInter(dd,(int)f->index,h,g);
 487         return(r);
 488     }
 489
 490     /* Check cache. */
 491     r = cuddCacheLookup(dd,DD_ADD_ITE_TAG,f,g,h);
 492     if (r != NULL) {
 493         return(r);
 494     }
 495
 496     /* Compute cofactors. */
 497     if (topf <= v) {
 498         v = ddMin(topf,v);      /* v = top_var(F,G,H) */
 499         index = f->index;
 500         Fv = cuddT(f); Fnv = cuddE(f);
 501     } else {
 502         Fv = Fnv = f;
 503     }
 504     if (topg == v) {
 505         index = g->index;
 506         Gv = cuddT(g); Gnv = cuddE(g);
 507     } else {
 508         Gv = Gnv = g;
 509     }
 510     if (toph == v) {
 511         index = h->index;
 512         Hv = cuddT(h); Hnv = cuddE(h);
 513     } else {
 514         Hv = Hnv = h;
 515     }
 516
 517     /* Recursive step. */
 518     t = cuddAddIteRecur(dd,Fv,Gv,Hv);
 519     if (t == NULL) return(NULL);
 520     cuddRef(t);
 521
 522     e = cuddAddIteRecur(dd,Fnv,Gnv,Hnv);
 523     if (e == NULL) {
 524         Cudd_RecursiveDeref(dd,t);
 525         return(NULL);
 526     }
 527     cuddRef(e);
 528
 529     r = (t == e) ? t : cuddUniqueInter(dd,index,t,e);
 530     if (r == NULL) {
 531         Cudd_RecursiveDeref(dd,t);
 532         Cudd_RecursiveDeref(dd,e);
 533         return(NULL);
 534     }
 535     cuddDeref(t);
 536     cuddDeref(e);
 537
 538     cuddCacheInsert(dd,DD_ADD_ITE_TAG,f,g,h,r);
 539
 540     return(r);
 541
 542 } /* end of cuddAddIteRecur */
 543
 544
 545 /**Function********************************************************************
 546
 547   Synopsis    [Performs the recursive step of Cudd_addCmpl.]
 548
 549   Description [Performs the recursive step of Cudd_addCmpl. Returns a
 550   pointer to the resulting ADD if successful; NULL otherwise.]
 551
 552   SideEffects [None]
 553
 554   SeeAlso     [Cudd_addCmpl]
 555
 556 ******************************************************************************/
 557 DdNode *
 558 cuddAddCmplRecur(
 559   DdManager * dd,
 560   DdNode * f)
 561 {
 562     DdNode *one,*zero;
 563     DdNode *r,*Fv,*Fnv,*t,*e;
 564
 565     statLine(dd);
 566     one = DD_ONE(dd);
 567     zero = DD_ZERO(dd);
 568
 569     if (cuddIsConstant(f)) {
 570         if (f == zero) {
 571             return(one);
 572         } else {
 573             return(zero);
 574         }
 575     }
 576     r = cuddCacheLookup1(dd,Cudd_addCmpl,f);
 577     if (r != NULL) {
 578         return(r);
 579     }
 580     Fv = cuddT(f);
 581     Fnv = cuddE(f);
 582     t = cuddAddCmplRecur(dd,Fv);
 583     if (t == NULL) return(NULL);
 584     cuddRef(t);
 585     e = cuddAddCmplRecur(dd,Fnv);
 586     if (e == NULL) {
 587         Cudd_RecursiveDeref(dd,t);
 588         return(NULL);
 589     }
 590     cuddRef(e);
 591     r = (t == e) ? t : cuddUniqueInter(dd,(int)f->index,t,e);
 592     if (r == NULL) {
 593         Cudd_RecursiveDeref(dd, t);
 594         Cudd_RecursiveDeref(dd, e);
 595         return(NULL);
 596     }
 597     cuddDeref(t);
 598     cuddDeref(e);
 599     cuddCacheInsert1(dd,Cudd_addCmpl,f,r);
 600     return(r);
 601
 602 } /* end of cuddAddCmplRecur */
 603
 604
 605 /*---------------------------------------------------------------------------*/
 606 /* Definition of static functions                                            */
 607 /*---------------------------------------------------------------------------*/
 608
 609
 610 /**Function********************************************************************
 611
 612   Synopsis [Replaces variables with constants if possible (part of
 613   canonical form).]
 614
 615   Description []
 616
 617   SideEffects [None]
 618
 619 ******************************************************************************/
 620 static void
 621 addVarToConst(
 622   DdNode * f,
 623   DdNode ** gp,
 624   DdNode ** hp,
 625   DdNode * one,
 626   DdNode * zero)
 627 {
 628     DdNode *g = *gp;
 629     DdNode *h = *hp;
 630
 631     if (f == g) { /* ITE(F,F,H) = ITE(F,1,H) = F + H */
 632         *gp = one;
 633     }
 634
 635     if (f == h) { /* ITE(F,G,F) = ITE(F,G,0) = F * G */
 636         *hp = zero;
 637     }
 638
 639 } /* end of addVarToConst */