distr/cudd/cuddAddFind.c

   1 /**CFile***********************************************************************
   2
   3   FileName    [cuddAddFind.c]
   4
   5   PackageName [cudd]
   6
   7   Synopsis    [Functions to find maximum and minimum in an ADD and to
   8   extract the i-th bit.]
   9
  10   Description [External procedures included in this module:
  11                 <ul>
  12                 <li> Cudd_addFindMax()
  13                 <li> Cudd_addFindMin()
  14                 <li> Cudd_addIthBit()
  15                 </ul>
  16                Static functions included in this module:
  17                 <ul>
  18                 <li> addDoIthBit()
  19                 </ul>]
  20
  21   Author      [Fabio Somenzi]
  22
  23   Copyright   [Copyright (c) 1995-2004, Regents of the University of Colorado
  24
  25   All rights reserved.
  26
  27   Redistribution and use in source and binary forms, with or without
  28   modification, are permitted provided that the following conditions
  29   are met:
  30
  31   Redistributions of source code must retain the above copyright
  32   notice, this list of conditions and the following disclaimer.
  33
  34   Redistributions in binary form must reproduce the above copyright
  35   notice, this list of conditions and the following disclaimer in the
  36   documentation and/or other materials provided with the distribution.
  37
  38   Neither the name of the University of Colorado nor the names of its
  39   contributors may be used to endorse or promote products derived from
  40   this software without specific prior written permission.
  41
  42   THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
  43   "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
  44   LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
  45   FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
  46   COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
  47   INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
  48   BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
  49   LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
  50   CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
  51   LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
  52   ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
  53   POSSIBILITY OF SUCH DAMAGE.]
  54
  55 ******************************************************************************/
  56
  57 #include "util.h"
  58 #include "cuddInt.h"
  59
  60 /*---------------------------------------------------------------------------*/
  61 /* Constant declarations                                                     */
  62 /*---------------------------------------------------------------------------*/
  63
  64
  65 /*---------------------------------------------------------------------------*/
  66 /* Stucture declarations                                                     */
  67 /*---------------------------------------------------------------------------*/
  68
  69
  70 /*---------------------------------------------------------------------------*/
  71 /* Type declarations                                                         */
  72 /*---------------------------------------------------------------------------*/
  73
  74
  75 /*---------------------------------------------------------------------------*/
  76 /* Variable declarations                                                     */
  77 /*---------------------------------------------------------------------------*/
  78
  79 #ifndef lint
  80 static char rcsid[] DD_UNUSED = "$Id: cuddAddFind.c,v 1.8 2004/08/13 18:04:45 fabio Exp $";
  81 #endif
  82
  83
  84 /*---------------------------------------------------------------------------*/
  85 /* Macro declarations                                                        */
  86 /*---------------------------------------------------------------------------*/
  87
  88 #ifdef __cplusplus
  89 extern "C" {
  90 #endif
  91
  92 /**AutomaticStart*************************************************************/
  93
  94 /*---------------------------------------------------------------------------*/
  95 /* Static function prototypes                                                */
  96 /*---------------------------------------------------------------------------*/
  97
  98 static DdNode * addDoIthBit (DdManager *dd, DdNode *f, DdNode *index);
  99
 100 /**AutomaticEnd***************************************************************/
 101
 102 #ifdef __cplusplus
 103 }
 104 #endif
 105
 106 /*---------------------------------------------------------------------------*/
 107 /* Definition of exported functions                                          */
 108 /*---------------------------------------------------------------------------*/
 109
 110 /**Function********************************************************************
 111
 112   Synopsis    [Finds the maximum discriminant of f.]
 113
 114   Description [Returns a pointer to a constant ADD.]
 115
 116   SideEffects [None]
 117
 118 ******************************************************************************/
 119 DdNode *
 120 Cudd_addFindMax(
 121   DdManager * dd,
 122   DdNode * f)
 123 {
 124     DdNode *t, *e, *res;
 125
 126     statLine(dd);
 127     if (cuddIsConstant(f)) {
 128         return(f);
 129     }
 130
 131     res = cuddCacheLookup1(dd,Cudd_addFindMax,f);
 132     if (res != NULL) {
 133         return(res);
 134     }
 135
 136     t  = Cudd_addFindMax(dd,cuddT(f));
 137     if (t == DD_PLUS_INFINITY(dd)) return(t);
 138
 139     e  = Cudd_addFindMax(dd,cuddE(f));
 140
 141     res = (cuddV(t) >= cuddV(e)) ? t : e;
 142
 143     cuddCacheInsert1(dd,Cudd_addFindMax,f,res);
 144
 145     return(res);
 146
 147 } /* end of Cudd_addFindMax */
 148
 149
 150 /**Function********************************************************************
 151
 152   Synopsis    [Finds the minimum discriminant of f.]
 153
 154   Description [Returns a pointer to a constant ADD.]
 155
 156   SideEffects [None]
 157
 158 ******************************************************************************/
 159 DdNode *
 160 Cudd_addFindMin(
 161   DdManager * dd,
 162   DdNode * f)
 163 {
 164     DdNode *t, *e, *res;
 165
 166     statLine(dd);
 167     if (cuddIsConstant(f)) {
 168         return(f);
 169     }
 170
 171     res = cuddCacheLookup1(dd,Cudd_addFindMin,f);
 172     if (res != NULL) {
 173         return(res);
 174     }
 175
 176     t  = Cudd_addFindMin(dd,cuddT(f));
 177     if (t == DD_MINUS_INFINITY(dd)) return(t);
 178
 179     e  = Cudd_addFindMin(dd,cuddE(f));
 180
 181     res = (cuddV(t) <= cuddV(e)) ? t : e;
 182
 183     cuddCacheInsert1(dd,Cudd_addFindMin,f,res);
 184
 185     return(res);
 186
 187 } /* end of Cudd_addFindMin */
 188
 189
 190 /**Function********************************************************************
 191
 192   Synopsis    [Extracts the i-th bit from an ADD.]
 193
 194   Description [Produces an ADD from another ADD by replacing all
 195   discriminants whose i-th bit is equal to 1 with 1, and all other
 196   discriminants with 0. The i-th bit refers to the integer
 197   representation of the leaf value. If the value is has a fractional
 198   part, it is ignored. Repeated calls to this procedure allow one to
 199   transform an integer-valued ADD into an array of ADDs, one for each
 200   bit of the leaf values. Returns a pointer to the resulting ADD if
 201   successful; NULL otherwise.]
 202
 203   SideEffects [None]
 204
 205   SeeAlso     [Cudd_addBddIthBit]
 206
 207 ******************************************************************************/
 208 DdNode *
 209 Cudd_addIthBit(
 210   DdManager * dd,
 211   DdNode * f,
 212   int  bit)
 213 {
 214     DdNode *res;
 215     DdNode *index;
 216
 217     /* Use a constant node to remember the bit, so that we can use the
 218     ** global cache.
 219     */
 220     index = cuddUniqueConst(dd,(CUDD_VALUE_TYPE) bit);
 221     if (index == NULL) return(NULL);
 222     cuddRef(index);
 223
 224     do {
 225         dd->reordered = 0;
 226         res = addDoIthBit(dd, f, index);
 227     } while (dd->reordered == 1);
 228
 229     if (res == NULL) {
 230         Cudd_RecursiveDeref(dd, index);
 231         return(NULL);
 232     }
 233     cuddRef(res);
 234     Cudd_RecursiveDeref(dd, index);
 235     cuddDeref(res);
 236     return(res);
 237
 238 } /* end of Cudd_addIthBit */
 239
 240
 241 /*---------------------------------------------------------------------------*/
 242 /* Definition of internal functions                                          */
 243 /*---------------------------------------------------------------------------*/
 244
 245
 246 /*---------------------------------------------------------------------------*/
 247 /* Definition of static functions                                            */
 248 /*---------------------------------------------------------------------------*/
 249
 250
 251 /**Function********************************************************************
 252
 253   Synopsis    [Performs the recursive step for Cudd_addIthBit.]
 254
 255   Description [Performs the recursive step for Cudd_addIthBit.
 256   Returns a pointer to the BDD if successful; NULL otherwise.]
 257
 258   SideEffects [None]
 259
 260   SeeAlso     []
 261
 262 ******************************************************************************/
 263 static DdNode *
 264 addDoIthBit(
 265   DdManager * dd,
 266   DdNode * f,
 267   DdNode * index)
 268 {
 269     DdNode *res, *T, *E;
 270     DdNode *fv, *fvn;
 271     int mask, value;
 272     int v;
 273
 274     statLine(dd);
 275     /* Check terminal case. */
 276     if (cuddIsConstant(f)) {
 277         mask = 1 << ((int) cuddV(index));
 278         value = (int) cuddV(f);
 279         return((value & mask) == 0 ? DD_ZERO(dd) : DD_ONE(dd));
 280     }
 281
 282     /* Check cache. */
 283     res = cuddCacheLookup2(dd,addDoIthBit,f,index);
 284     if (res != NULL) return(res);
 285
 286     /* Recursive step. */
 287     v = f->index;
 288     fv = cuddT(f); fvn = cuddE(f);
 289
 290     T = addDoIthBit(dd,fv,index);
 291     if (T == NULL) return(NULL);
 292     cuddRef(T);
 293
 294     E = addDoIthBit(dd,fvn,index);
 295     if (E == NULL) {
 296         Cudd_RecursiveDeref(dd, T);
 297         return(NULL);
 298     }
 299     cuddRef(E);
 300
 301     res = (T == E) ? T : cuddUniqueInter(dd,v,T,E);
 302     if (res == NULL) {
 303         Cudd_RecursiveDeref(dd, T);
 304         Cudd_RecursiveDeref(dd, E);
 305         return(NULL);
 306     }
 307     cuddDeref(T);
 308     cuddDeref(E);
 309
 310     /* Store result. */
 311     cuddCacheInsert2(dd,addDoIthBit,f,index,res);
 312
 313     return(res);
 314
 315 } /* end of addDoIthBit */
 316