distr/cudd/cuddClip.c

   1 /**CFile***********************************************************************
   2
   3   FileName    [cuddClip.c]
   4
   5   PackageName [cudd]
   6
   7   Synopsis    [Clipping functions.]
   8
   9   Description [External procedures included in this module:
  10                 <ul>
  11                 <li> Cudd_bddClippingAnd()
  12                 <li> Cudd_bddClippingAndAbstract()
  13                 </ul>
  14        Internal procedures included in this module:
  15                 <ul>
  16                 <li> cuddBddClippingAnd()
  17                 <li> cuddBddClippingAndAbstract()
  18                 </ul>
  19        Static procedures included in this module:
  20                 <ul>
  21                 <li> cuddBddClippingAndRecur()
  22                 <li> cuddBddClipAndAbsRecur()
  23                 </ul>
  24
  25   SeeAlso     []
  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 /*---------------------------------------------------------------------------*/
  68 /* Constant declarations                                                     */
  69 /*---------------------------------------------------------------------------*/
  70
  71
  72 /*---------------------------------------------------------------------------*/
  73 /* Stucture declarations                                                     */
  74 /*---------------------------------------------------------------------------*/
  75
  76
  77 /*---------------------------------------------------------------------------*/
  78 /* Type declarations                                                         */
  79 /*---------------------------------------------------------------------------*/
  80
  81 /*---------------------------------------------------------------------------*/
  82 /* Variable declarations                                                     */
  83 /*---------------------------------------------------------------------------*/
  84
  85 #ifndef lint
  86 static char rcsid[] DD_UNUSED = "$Id: cuddClip.c,v 1.8 2004/08/13 18:04:47 fabio Exp $";
  87 #endif
  88
  89 /*---------------------------------------------------------------------------*/
  90 /* Macro declarations                                                        */
  91 /*---------------------------------------------------------------------------*/
  92
  93
  94 /**AutomaticStart*************************************************************/
  95
  96 /*---------------------------------------------------------------------------*/
  97 /* Static function prototypes                                                */
  98 /*---------------------------------------------------------------------------*/
  99
 100 static DdNode * cuddBddClippingAndRecur (DdManager *manager, DdNode *f, DdNode *g, int distance, int direction);
 101 static DdNode * cuddBddClipAndAbsRecur (DdManager *manager, DdNode *f, DdNode *g, DdNode *cube, int distance, int direction);
 102
 103 /**AutomaticEnd***************************************************************/
 104
 105
 106 /*---------------------------------------------------------------------------*/
 107 /* Definition of exported functions                                          */
 108 /*---------------------------------------------------------------------------*/
 109
 110
 111 /**Function********************************************************************
 112
 113   Synopsis    [Approximates the conjunction of two BDDs f and g.]
 114
 115   Description [Approximates the conjunction of two BDDs f and g. Returns a
 116   pointer to the resulting BDD if successful; NULL if the intermediate
 117   result blows up.]
 118
 119   SideEffects [None]
 120
 121   SeeAlso     [Cudd_bddAnd]
 122
 123 ******************************************************************************/
 124 DdNode *
 125 Cudd_bddClippingAnd(
 126   DdManager * dd /* manager */,
 127   DdNode * f /* first conjunct */,
 128   DdNode * g /* second conjunct */,
 129   int  maxDepth /* maximum recursion depth */,
 130   int  direction /* under (0) or over (1) approximation */)
 131 {
 132     DdNode *res;
 133
 134     do {
 135         dd->reordered = 0;
 136         res = cuddBddClippingAnd(dd,f,g,maxDepth,direction);
 137     } while (dd->reordered == 1);
 138     return(res);
 139
 140 } /* end of Cudd_bddClippingAnd */
 141
 142
 143 /**Function********************************************************************
 144
 145   Synopsis    [Approximates the conjunction of two BDDs f and g and
 146   simultaneously abstracts the variables in cube.]
 147
 148   Description [Approximates the conjunction of two BDDs f and g and
 149   simultaneously abstracts the variables in cube. The variables are
 150   existentially abstracted. Returns a pointer to the resulting BDD if
 151   successful; NULL if the intermediate result blows up.]
 152
 153   SideEffects [None]
 154
 155   SeeAlso     [Cudd_bddAndAbstract Cudd_bddClippingAnd]
 156
 157 ******************************************************************************/
 158 DdNode *
 159 Cudd_bddClippingAndAbstract(
 160   DdManager * dd /* manager */,
 161   DdNode * f /* first conjunct */,
 162   DdNode * g /* second conjunct */,
 163   DdNode * cube /* cube of variables to be abstracted */,
 164   int  maxDepth /* maximum recursion depth */,
 165   int  direction /* under (0) or over (1) approximation */)
 166 {
 167     DdNode *res;
 168
 169     do {
 170         dd->reordered = 0;
 171         res = cuddBddClippingAndAbstract(dd,f,g,cube,maxDepth,direction);
 172     } while (dd->reordered == 1);
 173     return(res);
 174
 175 } /* end of Cudd_bddClippingAndAbstract */
 176
 177
 178 /*---------------------------------------------------------------------------*/
 179 /* Definition of internal functions                                          */
 180 /*---------------------------------------------------------------------------*/
 181
 182
 183 /**Function********************************************************************
 184
 185   Synopsis    [Approximates the conjunction of two BDDs f and g.]
 186
 187   Description [Approximates the conjunction of two BDDs f and g. Returns a
 188   pointer to the resulting BDD if successful; NULL if the intermediate
 189   result blows up.]
 190
 191   SideEffects [None]
 192
 193   SeeAlso     [Cudd_bddClippingAnd]
 194
 195 ******************************************************************************/
 196 DdNode *
 197 cuddBddClippingAnd(
 198   DdManager * dd /* manager */,
 199   DdNode * f /* first conjunct */,
 200   DdNode * g /* second conjunct */,
 201   int  maxDepth /* maximum recursion depth */,
 202   int  direction /* under (0) or over (1) approximation */)
 203 {
 204     DdNode *res;
 205
 206     res = cuddBddClippingAndRecur(dd,f,g,maxDepth,direction);
 207
 208     return(res);
 209
 210 } /* end of cuddBddClippingAnd */
 211
 212
 213 /**Function********************************************************************
 214
 215   Synopsis    [Approximates the conjunction of two BDDs f and g and
 216   simultaneously abstracts the variables in cube.]
 217
 218   Description [Approximates the conjunction of two BDDs f and g and
 219   simultaneously abstracts the variables in cube. Returns a
 220   pointer to the resulting BDD if successful; NULL if the intermediate
 221   result blows up.]
 222
 223   SideEffects [None]
 224
 225   SeeAlso     [Cudd_bddClippingAndAbstract]
 226
 227 ******************************************************************************/
 228 DdNode *
 229 cuddBddClippingAndAbstract(
 230   DdManager * dd /* manager */,
 231   DdNode * f /* first conjunct */,
 232   DdNode * g /* second conjunct */,
 233   DdNode * cube /* cube of variables to be abstracted */,
 234   int  maxDepth /* maximum recursion depth */,
 235   int  direction /* under (0) or over (1) approximation */)
 236 {
 237     DdNode *res;
 238
 239     res = cuddBddClipAndAbsRecur(dd,f,g,cube,maxDepth,direction);
 240
 241     return(res);
 242
 243 } /* end of cuddBddClippingAndAbstract */
 244
 245
 246 /*---------------------------------------------------------------------------*/
 247 /* Definition of static functions                                            */
 248 /*---------------------------------------------------------------------------*/
 249
 250
 251 /**Function********************************************************************
 252
 253   Synopsis [Implements the recursive step of Cudd_bddClippingAnd.]
 254
 255   Description [Implements the recursive step of Cudd_bddClippingAnd by taking
 256   the conjunction of two BDDs.  Returns a pointer to the result is
 257   successful; NULL otherwise.]
 258
 259   SideEffects [None]
 260
 261   SeeAlso     [cuddBddClippingAnd]
 262
 263 ******************************************************************************/
 264 static DdNode *
 265 cuddBddClippingAndRecur(
 266   DdManager * manager,
 267   DdNode * f,
 268   DdNode * g,
 269   int  distance,
 270   int  direction)
 271 {
 272     DdNode *F, *ft, *fe, *G, *gt, *ge;
 273     DdNode *one, *zero, *r, *t, *e;
 274     unsigned int topf, topg, index;
 275     DD_CTFP cacheOp;
 276
 277     statLine(manager);
 278     one = DD_ONE(manager);
 279     zero = Cudd_Not(one);
 280
 281     /* Terminal cases. */
 282     if (f == zero || g == zero || f == Cudd_Not(g)) return(zero);
 283     if (f == g || g == one) return(f);
 284     if (f == one) return(g);
 285     if (distance == 0) {
 286         /* One last attempt at returning the right result. We sort of
 287         ** cheat by calling Cudd_bddLeq. */
 288         if (Cudd_bddLeq(manager,f,g)) return(f);
 289         if (Cudd_bddLeq(manager,g,f)) return(g);
 290         if (direction == 1) {
 291             if (Cudd_bddLeq(manager,f,Cudd_Not(g)) ||
 292                 Cudd_bddLeq(manager,g,Cudd_Not(f))) return(zero);
 293         }
 294         return(Cudd_NotCond(one,(direction == 0)));
 295     }
 296
 297     /* At this point f and g are not constant. */
 298     distance--;
 299
 300     /* Check cache. Try to increase cache efficiency by sorting the
 301     ** pointers. */
 302     if (f > g) {
 303         DdNode *tmp = f;
 304         f = g; g = tmp;
 305     }
 306     F = Cudd_Regular(f);
 307     G = Cudd_Regular(g);
 308     cacheOp = (DD_CTFP)
 309         (direction ? Cudd_bddClippingAnd : cuddBddClippingAnd);
 310     if (F->ref != 1 || G->ref != 1) {
 311         r = cuddCacheLookup2(manager, cacheOp, f, g);
 312         if (r != NULL) return(r);
 313     }
 314
 315     /* Here we can skip the use of cuddI, because the operands are known
 316     ** to be non-constant.
 317     */
 318     topf = manager->perm[F->index];
 319     topg = manager->perm[G->index];
 320
 321     /* Compute cofactors. */
 322     if (topf <= topg) {
 323         index = F->index;
 324         ft = cuddT(F);
 325         fe = cuddE(F);
 326         if (Cudd_IsComplement(f)) {
 327             ft = Cudd_Not(ft);
 328             fe = Cudd_Not(fe);
 329         }
 330     } else {
 331         index = G->index;
 332         ft = fe = f;
 333     }
 334
 335     if (topg <= topf) {
 336         gt = cuddT(G);
 337         ge = cuddE(G);
 338         if (Cudd_IsComplement(g)) {
 339             gt = Cudd_Not(gt);
 340             ge = Cudd_Not(ge);
 341         }
 342     } else {
 343         gt = ge = g;
 344     }
 345
 346     t = cuddBddClippingAndRecur(manager, ft, gt, distance, direction);
 347     if (t == NULL) return(NULL);
 348     cuddRef(t);
 349     e = cuddBddClippingAndRecur(manager, fe, ge, distance, direction);
 350     if (e == NULL) {
 351         Cudd_RecursiveDeref(manager, t);
 352         return(NULL);
 353     }
 354     cuddRef(e);
 355
 356     if (t == e) {
 357         r = t;
 358     } else {
 359         if (Cudd_IsComplement(t)) {
 360             r = cuddUniqueInter(manager,(int)index,Cudd_Not(t),Cudd_Not(e));
 361             if (r == NULL) {
 362                 Cudd_RecursiveDeref(manager, t);
 363                 Cudd_RecursiveDeref(manager, e);
 364                 return(NULL);
 365             }
 366             r = Cudd_Not(r);
 367         } else {
 368             r = cuddUniqueInter(manager,(int)index,t,e);
 369             if (r == NULL) {
 370                 Cudd_RecursiveDeref(manager, t);
 371                 Cudd_RecursiveDeref(manager, e);
 372                 return(NULL);
 373             }
 374         }
 375     }
 376     cuddDeref(e);
 377     cuddDeref(t);
 378     if (F->ref != 1 || G->ref != 1)
 379         cuddCacheInsert2(manager, cacheOp, f, g, r);
 380     return(r);
 381
 382 } /* end of cuddBddClippingAndRecur */
 383
 384
 385 /**Function********************************************************************
 386
 387   Synopsis [Approximates the AND of two BDDs and simultaneously abstracts the
 388   variables in cube.]
 389
 390   Description [Approximates the AND of two BDDs and simultaneously
 391   abstracts the variables in cube. The variables are existentially
 392   abstracted.  Returns a pointer to the result is successful; NULL
 393   otherwise.]
 394
 395   SideEffects [None]
 396
 397   SeeAlso     [Cudd_bddClippingAndAbstract]
 398
 399 ******************************************************************************/
 400 static DdNode *
 401 cuddBddClipAndAbsRecur(
 402   DdManager * manager,
 403   DdNode * f,
 404   DdNode * g,
 405   DdNode * cube,
 406   int  distance,
 407   int  direction)
 408 {
 409     DdNode *F, *ft, *fe, *G, *gt, *ge;
 410     DdNode *one, *zero, *r, *t, *e, *Cube;
 411     unsigned int topf, topg, topcube, top, index;
 412     ptruint cacheTag;
 413
 414     statLine(manager);
 415     one = DD_ONE(manager);
 416     zero = Cudd_Not(one);
 417
 418     /* Terminal cases. */
 419     if (f == zero || g == zero || f == Cudd_Not(g)) return(zero);
 420     if (f == one && g == one)   return(one);
 421     if (cube == one) {
 422         return(cuddBddClippingAndRecur(manager, f, g, distance, direction));
 423     }
 424     if (f == one || f == g) {
 425         return (cuddBddExistAbstractRecur(manager, g, cube));
 426     }
 427     if (g == one) {
 428         return (cuddBddExistAbstractRecur(manager, f, cube));
 429     }
 430     if (distance == 0) return(Cudd_NotCond(one,(direction == 0)));
 431
 432     /* At this point f, g, and cube are not constant. */
 433     distance--;
 434
 435     /* Check cache. */
 436     if (f > g) { /* Try to increase cache efficiency. */
 437         DdNode *tmp = f;
 438         f = g; g = tmp;
 439     }
 440     F = Cudd_Regular(f);
 441     G = Cudd_Regular(g);
 442     cacheTag = direction ? DD_BDD_CLIPPING_AND_ABSTRACT_UP_TAG :
 443         DD_BDD_CLIPPING_AND_ABSTRACT_DOWN_TAG;
 444     if (F->ref != 1 || G->ref != 1) {
 445         r = cuddCacheLookup(manager, cacheTag,
 446                             f, g, cube);
 447         if (r != NULL) {
 448             return(r);
 449         }
 450     }
 451
 452     /* Here we can skip the use of cuddI, because the operands are known
 453     ** to be non-constant.
 454     */
 455     topf = manager->perm[F->index];
 456     topg = manager->perm[G->index];
 457     top = ddMin(topf, topg);
 458     topcube = manager->perm[cube->index];
 459
 460     if (topcube < top) {
 461         return(cuddBddClipAndAbsRecur(manager, f, g, cuddT(cube),
 462                                       distance, direction));
 463     }
 464     /* Now, topcube >= top. */
 465
 466     if (topf == top) {
 467         index = F->index;
 468         ft = cuddT(F);
 469         fe = cuddE(F);
 470         if (Cudd_IsComplement(f)) {
 471             ft = Cudd_Not(ft);
 472             fe = Cudd_Not(fe);
 473         }
 474     } else {
 475         index = G->index;
 476         ft = fe = f;
 477     }
 478
 479     if (topg == top) {
 480         gt = cuddT(G);
 481         ge = cuddE(G);
 482         if (Cudd_IsComplement(g)) {
 483             gt = Cudd_Not(gt);
 484             ge = Cudd_Not(ge);
 485         }
 486     } else {
 487         gt = ge = g;
 488     }
 489
 490     if (topcube == top) {
 491         Cube = cuddT(cube);
 492     } else {
 493         Cube = cube;
 494     }
 495
 496     t = cuddBddClipAndAbsRecur(manager, ft, gt, Cube, distance, direction);
 497     if (t == NULL) return(NULL);
 498
 499     /* Special case: 1 OR anything = 1. Hence, no need to compute
 500     ** the else branch if t is 1.
 501     */
 502     if (t == one && topcube == top) {
 503         if (F->ref != 1 || G->ref != 1)
 504             cuddCacheInsert(manager, cacheTag, f, g, cube, one);
 505         return(one);
 506     }
 507     cuddRef(t);
 508
 509     e = cuddBddClipAndAbsRecur(manager, fe, ge, Cube, distance, direction);
 510     if (e == NULL) {
 511         Cudd_RecursiveDeref(manager, t);
 512         return(NULL);
 513     }
 514     cuddRef(e);
 515
 516     if (topcube == top) {       /* abstract */
 517         r = cuddBddClippingAndRecur(manager, Cudd_Not(t), Cudd_Not(e),
 518                                     distance, (direction == 0));
 519         if (r == NULL) {
 520             Cudd_RecursiveDeref(manager, t);
 521             Cudd_RecursiveDeref(manager, e);
 522             return(NULL);
 523         }
 524         r = Cudd_Not(r);
 525         cuddRef(r);
 526         Cudd_RecursiveDeref(manager, t);
 527         Cudd_RecursiveDeref(manager, e);
 528         cuddDeref(r);
 529     } else if (t == e) {
 530         r = t;
 531         cuddDeref(t);
 532         cuddDeref(e);
 533     } else {
 534         if (Cudd_IsComplement(t)) {
 535             r = cuddUniqueInter(manager,(int)index,Cudd_Not(t),Cudd_Not(e));
 536             if (r == NULL) {
 537                 Cudd_RecursiveDeref(manager, t);
 538                 Cudd_RecursiveDeref(manager, e);
 539                 return(NULL);
 540             }
 541             r = Cudd_Not(r);
 542         } else {
 543             r = cuddUniqueInter(manager,(int)index,t,e);
 544             if (r == NULL) {
 545                 Cudd_RecursiveDeref(manager, t);
 546                 Cudd_RecursiveDeref(manager, e);
 547                 return(NULL);
 548             }
 549         }
 550         cuddDeref(e);
 551         cuddDeref(t);
 552     }
 553     if (F->ref != 1 || G->ref != 1)
 554         cuddCacheInsert(manager, cacheTag, f, g, cube, r);
 555     return (r);
 556
 557 } /* end of cuddBddClipAndAbsRecur */
 558