distr/cudd/cuddAndAbs.c

   1 /**CFile***********************************************************************
   2
   3   FileName    [cuddAndAbs.c]
   4
   5   PackageName [cudd]
   6
   7   Synopsis    [Combined AND and existential abstraction for BDDs]
   8
   9   Description [External procedures included in this module:
  10                 <ul>
  11                 <li> Cudd_bddAndAbstract()
  12                 <li> Cudd_bddAndAbstractLimit()
  13                 </ul>
  14             Internal procedures included in this module:
  15                 <ul>
  16                 <li> cuddBddAndAbstractRecur()
  17                 </ul>]
  18
  19   Author      [Fabio Somenzi]
  20
  21   Copyright   [Copyright (c) 1995-2004, Regents of the University of Colorado
  22
  23   All rights reserved.
  24
  25   Redistribution and use in source and binary forms, with or without
  26   modification, are permitted provided that the following conditions
  27   are met:
  28
  29   Redistributions of source code must retain the above copyright
  30   notice, this list of conditions and the following disclaimer.
  31
  32   Redistributions in binary form must reproduce the above copyright
  33   notice, this list of conditions and the following disclaimer in the
  34   documentation and/or other materials provided with the distribution.
  35
  36   Neither the name of the University of Colorado nor the names of its
  37   contributors may be used to endorse or promote products derived from
  38   this software without specific prior written permission.
  39
  40   THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
  41   "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
  42   LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
  43   FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
  44   COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
  45   INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
  46   BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
  47   LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
  48   CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
  49   LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
  50   ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
  51   POSSIBILITY OF SUCH DAMAGE.]
  52
  53 ******************************************************************************/
  54
  55 #include "util.h"
  56 #include "cuddInt.h"
  57
  58
  59 /*---------------------------------------------------------------------------*/
  60 /* Constant declarations                                                     */
  61 /*---------------------------------------------------------------------------*/
  62
  63
  64 /*---------------------------------------------------------------------------*/
  65 /* Stucture declarations                                                     */
  66 /*---------------------------------------------------------------------------*/
  67
  68
  69 /*---------------------------------------------------------------------------*/
  70 /* Type declarations                                                         */
  71 /*---------------------------------------------------------------------------*/
  72
  73
  74 /*---------------------------------------------------------------------------*/
  75 /* Variable declarations                                                     */
  76 /*---------------------------------------------------------------------------*/
  77
  78 #ifndef lint
  79 static char rcsid[] DD_UNUSED = "$Id: cuddAndAbs.c,v 1.19 2004/08/13 18:04:46 fabio Exp $";
  80 #endif
  81
  82
  83 /*---------------------------------------------------------------------------*/
  84 /* Macro declarations                                                        */
  85 /*---------------------------------------------------------------------------*/
  86
  87
  88 /**AutomaticStart*************************************************************/
  89
  90 /*---------------------------------------------------------------------------*/
  91 /* Static function prototypes                                                */
  92 /*---------------------------------------------------------------------------*/
  93
  94
  95 /**AutomaticEnd***************************************************************/
  96
  97
  98 /*---------------------------------------------------------------------------*/
  99 /* Definition of exported functions                                          */
 100 /*---------------------------------------------------------------------------*/
 101
 102
 103 /**Function********************************************************************
 104
 105   Synopsis [Takes the AND of two BDDs and simultaneously abstracts the
 106   variables in cube.]
 107
 108   Description [Takes the AND of two BDDs and simultaneously abstracts
 109   the variables in cube. The variables are existentially abstracted.
 110   Returns a pointer to the result is successful; NULL otherwise.
 111   Cudd_bddAndAbstract implements the semiring matrix multiplication
 112   algorithm for the boolean semiring.]
 113
 114   SideEffects [None]
 115
 116   SeeAlso     [Cudd_addMatrixMultiply Cudd_addTriangle Cudd_bddAnd]
 117
 118 ******************************************************************************/
 119 DdNode *
 120 Cudd_bddAndAbstract(
 121   DdManager * manager,
 122   DdNode * f,
 123   DdNode * g,
 124   DdNode * cube)
 125 {
 126     DdNode *res;
 127
 128     do {
 129         manager->reordered = 0;
 130         res = cuddBddAndAbstractRecur(manager, f, g, cube);
 131     } while (manager->reordered == 1);
 132     return(res);
 133
 134 } /* end of Cudd_bddAndAbstract */
 135
 136
 137 /**Function********************************************************************
 138
 139   Synopsis [Takes the AND of two BDDs and simultaneously abstracts the
 140   variables in cube.  Returns NULL if too many nodes are required.]
 141
 142   Description [Takes the AND of two BDDs and simultaneously abstracts
 143   the variables in cube. The variables are existentially abstracted.
 144   Returns a pointer to the result is successful; NULL otherwise.
 145   In particular, if the number of new nodes created exceeds
 146   <code>limit</code>, this function returns NULL.]
 147
 148   SideEffects [None]
 149
 150   SeeAlso     [Cudd_bddAndAbstract]
 151
 152 ******************************************************************************/
 153 DdNode *
 154 Cudd_bddAndAbstractLimit(
 155   DdManager * manager,
 156   DdNode * f,
 157   DdNode * g,
 158   DdNode * cube,
 159   unsigned int limit)
 160 {
 161     DdNode *res;
 162     unsigned int saveLimit = manager->maxLive;
 163
 164     manager->maxLive = (manager->keys - manager->dead) +
 165       (manager->keysZ - manager->deadZ) + limit;
 166     do {
 167         manager->reordered = 0;
 168         res = cuddBddAndAbstractRecur(manager, f, g, cube);
 169     } while (manager->reordered == 1);
 170     manager->maxLive = saveLimit;
 171     return(res);
 172
 173 } /* end of Cudd_bddAndAbstractLimit */
 174
 175
 176 /*---------------------------------------------------------------------------*/
 177 /* Definition of internal functions                                          */
 178 /*---------------------------------------------------------------------------*/
 179
 180
 181 /**Function********************************************************************
 182
 183   Synopsis [Takes the AND of two BDDs and simultaneously abstracts the
 184   variables in cube.]
 185
 186   Description [Takes the AND of two BDDs and simultaneously abstracts
 187   the variables in cube. The variables are existentially abstracted.
 188   Returns a pointer to the result is successful; NULL otherwise.]
 189
 190   SideEffects [None]
 191
 192   SeeAlso     [Cudd_bddAndAbstract]
 193
 194 ******************************************************************************/
 195 DdNode *
 196 cuddBddAndAbstractRecur(
 197   DdManager * manager,
 198   DdNode * f,
 199   DdNode * g,
 200   DdNode * cube)
 201 {
 202     DdNode *F, *ft, *fe, *G, *gt, *ge;
 203     DdNode *one, *zero, *r, *t, *e;
 204     unsigned int topf, topg, topcube, top, index;
 205
 206     statLine(manager);
 207     one = DD_ONE(manager);
 208     zero = Cudd_Not(one);
 209
 210     /* Terminal cases. */
 211     if (f == zero || g == zero || f == Cudd_Not(g)) return(zero);
 212     if (f == one && g == one)   return(one);
 213
 214     if (cube == one) {
 215         return(cuddBddAndRecur(manager, f, g));
 216     }
 217     if (f == one || f == g) {
 218         return(cuddBddExistAbstractRecur(manager, g, cube));
 219     }
 220     if (g == one) {
 221         return(cuddBddExistAbstractRecur(manager, f, cube));
 222     }
 223     /* At this point f, g, and cube are not constant. */
 224
 225     if (f > g) { /* Try to increase cache efficiency. */
 226         DdNode *tmp = f;
 227         f = g;
 228         g = tmp;
 229     }
 230
 231     /* Here we can skip the use of cuddI, because the operands are known
 232     ** to be non-constant.
 233     */
 234     F = Cudd_Regular(f);
 235     G = Cudd_Regular(g);
 236     topf = manager->perm[F->index];
 237     topg = manager->perm[G->index];
 238     top = ddMin(topf, topg);
 239     topcube = manager->perm[cube->index];
 240
 241     while (topcube < top) {
 242         cube = cuddT(cube);
 243         if (cube == one) {
 244             return(cuddBddAndRecur(manager, f, g));
 245         }
 246         topcube = manager->perm[cube->index];
 247     }
 248     /* Now, topcube >= top. */
 249
 250     /* Check cache. */
 251     if (F->ref != 1 || G->ref != 1) {
 252         r = cuddCacheLookup(manager, DD_BDD_AND_ABSTRACT_TAG, f, g, cube);
 253         if (r != NULL) {
 254             return(r);
 255         }
 256     }
 257
 258     if (topf == top) {
 259         index = F->index;
 260         ft = cuddT(F);
 261         fe = cuddE(F);
 262         if (Cudd_IsComplement(f)) {
 263             ft = Cudd_Not(ft);
 264             fe = Cudd_Not(fe);
 265         }
 266     } else {
 267         index = G->index;
 268         ft = fe = f;
 269     }
 270
 271     if (topg == top) {
 272         gt = cuddT(G);
 273         ge = cuddE(G);
 274         if (Cudd_IsComplement(g)) {
 275             gt = Cudd_Not(gt);
 276             ge = Cudd_Not(ge);
 277         }
 278     } else {
 279         gt = ge = g;
 280     }
 281
 282     if (topcube == top) {       /* quantify */
 283         DdNode *Cube = cuddT(cube);
 284         t = cuddBddAndAbstractRecur(manager, ft, gt, Cube);
 285         if (t == NULL) return(NULL);
 286         /* Special case: 1 OR anything = 1. Hence, no need to compute
 287         ** the else branch if t is 1. Likewise t + t * anything == t.
 288         ** Notice that t == fe implies that fe does not depend on the
 289         ** variables in Cube. Likewise for t == ge.
 290         */
 291         if (t == one || t == fe || t == ge) {
 292             if (F->ref != 1 || G->ref != 1)
 293                 cuddCacheInsert(manager, DD_BDD_AND_ABSTRACT_TAG,
 294                                 f, g, cube, t);
 295             return(t);
 296         }
 297         cuddRef(t);
 298         /* Special case: t + !t * anything == t + anything. */
 299         if (t == Cudd_Not(fe)) {
 300             e = cuddBddExistAbstractRecur(manager, ge, Cube);
 301         } else if (t == Cudd_Not(ge)) {
 302             e = cuddBddExistAbstractRecur(manager, fe, Cube);
 303         } else {
 304             e = cuddBddAndAbstractRecur(manager, fe, ge, Cube);
 305         }
 306         if (e == NULL) {
 307             Cudd_IterDerefBdd(manager, t);
 308             return(NULL);
 309         }
 310         if (t == e) {
 311             r = t;
 312             cuddDeref(t);
 313         } else {
 314             cuddRef(e);
 315             r = cuddBddAndRecur(manager, Cudd_Not(t), Cudd_Not(e));
 316             if (r == NULL) {
 317                 Cudd_IterDerefBdd(manager, t);
 318                 Cudd_IterDerefBdd(manager, e);
 319                 return(NULL);
 320             }
 321             r = Cudd_Not(r);
 322             cuddRef(r);
 323             Cudd_DelayedDerefBdd(manager, t);
 324             Cudd_DelayedDerefBdd(manager, e);
 325             cuddDeref(r);
 326         }
 327     } else {
 328         t = cuddBddAndAbstractRecur(manager, ft, gt, cube);
 329         if (t == NULL) return(NULL);
 330         cuddRef(t);
 331         e = cuddBddAndAbstractRecur(manager, fe, ge, cube);
 332         if (e == NULL) {
 333             Cudd_IterDerefBdd(manager, t);
 334             return(NULL);
 335         }
 336         if (t == e) {
 337             r = t;
 338             cuddDeref(t);
 339         } else {
 340             cuddRef(e);
 341             if (Cudd_IsComplement(t)) {
 342                 r = cuddUniqueInter(manager, (int) index,
 343                                     Cudd_Not(t), Cudd_Not(e));
 344                 if (r == NULL) {
 345                     Cudd_IterDerefBdd(manager, t);
 346                     Cudd_IterDerefBdd(manager, e);
 347                     return(NULL);
 348                 }
 349                 r = Cudd_Not(r);
 350             } else {
 351                 r = cuddUniqueInter(manager,(int)index,t,e);
 352                 if (r == NULL) {
 353                     Cudd_IterDerefBdd(manager, t);
 354                     Cudd_IterDerefBdd(manager, e);
 355                     return(NULL);
 356                 }
 357             }
 358             cuddDeref(e);
 359             cuddDeref(t);
 360         }
 361     }
 362
 363     if (F->ref != 1 || G->ref != 1)
 364         cuddCacheInsert(manager, DD_BDD_AND_ABSTRACT_TAG, f, g, cube, r);
 365     return (r);
 366
 367 } /* end of cuddBddAndAbstractRecur */
 368
 369
 370 /*---------------------------------------------------------------------------*/
 371 /* Definition of static functions                                            */
 372 /*---------------------------------------------------------------------------*/
 373