distr/cudd/cuddZddCount.c

   1 /**CFile***********************************************************************
   2
   3   FileName    [cuddZddCount.c]
   4
   5   PackageName [cudd]
   6
   7   Synopsis    [Procedures to count the number of minterms of a ZDD.]
   8
   9   Description [External procedures included in this module:
  10                     <ul>
  11                     <li> Cudd_zddCount();
  12                     <li> Cudd_zddCountDouble();
  13                     </ul>
  14                Internal procedures included in this module:
  15                     <ul>
  16                     </ul>
  17                Static procedures included in this module:
  18                     <ul>
  19                     <li> cuddZddCountStep();
  20                     <li> cuddZddCountDoubleStep();
  21                     <li> st_zdd_count_dbl_free()
  22                     <li> st_zdd_countfree()
  23                     </ul>
  24               ]
  25
  26   SeeAlso     []
  27
  28   Author      [Hyong-Kyoon Shin, In-Ho Moon]
  29
  30   Copyright   [Copyright (c) 1995-2004, Regents of the University of Colorado
  31
  32   All rights reserved.
  33
  34   Redistribution and use in source and binary forms, with or without
  35   modification, are permitted provided that the following conditions
  36   are met:
  37
  38   Redistributions of source code must retain the above copyright
  39   notice, this list of conditions and the following disclaimer.
  40
  41   Redistributions in binary form must reproduce the above copyright
  42   notice, this list of conditions and the following disclaimer in the
  43   documentation and/or other materials provided with the distribution.
  44
  45   Neither the name of the University of Colorado nor the names of its
  46   contributors may be used to endorse or promote products derived from
  47   this software without specific prior written permission.
  48
  49   THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
  50   "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
  51   LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
  52   FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
  53   COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
  54   INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
  55   BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
  56   LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
  57   CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
  58   LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
  59   ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
  60   POSSIBILITY OF SUCH DAMAGE.]
  61
  62 ******************************************************************************/
  63
  64 #include "util.h"
  65 #include "cuddInt.h"
  66
  67 /*---------------------------------------------------------------------------*/
  68 /* Constant declarations                                                     */
  69 /*---------------------------------------------------------------------------*/
  70
  71
  72 /*---------------------------------------------------------------------------*/
  73 /* Stucture declarations                                                     */
  74 /*---------------------------------------------------------------------------*/
  75
  76
  77 /*---------------------------------------------------------------------------*/
  78 /* Type declarations                                                         */
  79 /*---------------------------------------------------------------------------*/
  80
  81
  82 /*---------------------------------------------------------------------------*/
  83 /* Variable declarations                                                     */
  84 /*---------------------------------------------------------------------------*/
  85
  86 #ifndef lint
  87 static char rcsid[] DD_UNUSED = "$Id: cuddZddCount.c,v 1.14 2004/08/13 18:04:53 fabio Exp $";
  88 #endif
  89
  90 /*---------------------------------------------------------------------------*/
  91 /* Macro declarations                                                        */
  92 /*---------------------------------------------------------------------------*/
  93
  94 #ifdef __cplusplus
  95 extern "C" {
  96 #endif
  97
  98 /**AutomaticStart*************************************************************/
  99
 100 /*---------------------------------------------------------------------------*/
 101 /* Static function prototypes                                                */
 102 /*---------------------------------------------------------------------------*/
 103
 104 static int cuddZddCountStep (DdNode *P, st_table *table, DdNode *base, DdNode *empty);
 105 static double cuddZddCountDoubleStep (DdNode *P, st_table *table, DdNode *base, DdNode *empty);
 106 static enum st_retval st_zdd_countfree (char *key, char *value, char *arg);
 107 static enum st_retval st_zdd_count_dbl_free (char *key, char *value, char *arg);
 108
 109 /**AutomaticEnd***************************************************************/
 110
 111 #ifdef __cplusplus
 112 }
 113 #endif
 114
 115 /*---------------------------------------------------------------------------*/
 116 /* Definition of exported functions                                          */
 117 /*---------------------------------------------------------------------------*/
 118
 119
 120 /**Function********************************************************************
 121
 122   Synopsis [Counts the number of minterms in a ZDD.]
 123
 124   Description [Returns an integer representing the number of minterms
 125   in a ZDD.]
 126
 127   SideEffects [None]
 128
 129   SeeAlso     [Cudd_zddCountDouble]
 130
 131 ******************************************************************************/
 132 int
 133 Cudd_zddCount(
 134   DdManager * zdd,
 135   DdNode * P)
 136 {
 137     st_table    *table;
 138     int         res;
 139     DdNode      *base, *empty;
 140
 141     base  = DD_ONE(zdd);
 142     empty = DD_ZERO(zdd);
 143     table = st_init_table(st_ptrcmp, st_ptrhash);
 144     if (table == NULL) return(CUDD_OUT_OF_MEM);
 145     res = cuddZddCountStep(P, table, base, empty);
 146     if (res == CUDD_OUT_OF_MEM) {
 147         zdd->errorCode = CUDD_MEMORY_OUT;
 148     }
 149     st_foreach(table, st_zdd_countfree, NIL(char));
 150     st_free_table(table);
 151
 152     return(res);
 153
 154 } /* end of Cudd_zddCount */
 155
 156
 157 /**Function********************************************************************
 158
 159   Synopsis [Counts the number of minterms of a ZDD.]
 160
 161   Description [Counts the number of minterms of a ZDD. The result is
 162   returned as a double. If the procedure runs out of memory, it
 163   returns (double) CUDD_OUT_OF_MEM. This procedure is used in
 164   Cudd_zddCountMinterm.]
 165
 166   SideEffects [None]
 167
 168   SeeAlso     [Cudd_zddCountMinterm Cudd_zddCount]
 169
 170 ******************************************************************************/
 171 double
 172 Cudd_zddCountDouble(
 173   DdManager * zdd,
 174   DdNode * P)
 175 {
 176     st_table    *table;
 177     double      res;
 178     DdNode      *base, *empty;
 179
 180     base  = DD_ONE(zdd);
 181     empty = DD_ZERO(zdd);
 182     table = st_init_table(st_ptrcmp, st_ptrhash);
 183     if (table == NULL) return((double)CUDD_OUT_OF_MEM);
 184     res = cuddZddCountDoubleStep(P, table, base, empty);
 185     if (res == (double)CUDD_OUT_OF_MEM) {
 186         zdd->errorCode = CUDD_MEMORY_OUT;
 187     }
 188     st_foreach(table, st_zdd_count_dbl_free, NIL(char));
 189     st_free_table(table);
 190
 191     return(res);
 192
 193 } /* end of Cudd_zddCountDouble */
 194
 195
 196 /*---------------------------------------------------------------------------*/
 197 /* Definition of internal functions                                          */
 198 /*---------------------------------------------------------------------------*/
 199
 200
 201 /*---------------------------------------------------------------------------*/
 202 /* Definition of static functions                                            */
 203 /*---------------------------------------------------------------------------*/
 204
 205
 206 /**Function********************************************************************
 207
 208   Synopsis [Performs the recursive step of Cudd_zddCount.]
 209
 210   Description []
 211
 212   SideEffects [None]
 213
 214   SeeAlso     []
 215
 216 ******************************************************************************/
 217 static int
 218 cuddZddCountStep(
 219   DdNode * P,
 220   st_table * table,
 221   DdNode * base,
 222   DdNode * empty)
 223 {
 224     int         res;
 225     int         *dummy;
 226
 227     if (P == empty)
 228         return(0);
 229     if (P == base)
 230         return(1);
 231
 232     /* Check cache. */
 233     if (st_lookup(table, P, &dummy)) {
 234         res = *dummy;
 235         return(res);
 236     }
 237
 238     res = cuddZddCountStep(cuddE(P), table, base, empty) +
 239         cuddZddCountStep(cuddT(P), table, base, empty);
 240
 241     dummy = ALLOC(int, 1);
 242     if (dummy == NULL) {
 243         return(CUDD_OUT_OF_MEM);
 244     }
 245     *dummy = res;
 246     if (st_insert(table, (char *)P, (char *)dummy) == ST_OUT_OF_MEM) {
 247         FREE(dummy);
 248         return(CUDD_OUT_OF_MEM);
 249     }
 250
 251     return(res);
 252
 253 } /* end of cuddZddCountStep */
 254
 255
 256 /**Function********************************************************************
 257
 258   Synopsis [Performs the recursive step of Cudd_zddCountDouble.]
 259
 260   Description []
 261
 262   SideEffects [None]
 263
 264   SeeAlso     []
 265
 266 ******************************************************************************/
 267 static double
 268 cuddZddCountDoubleStep(
 269   DdNode * P,
 270   st_table * table,
 271   DdNode * base,
 272   DdNode * empty)
 273 {
 274     double      res;
 275     double      *dummy;
 276
 277     if (P == empty)
 278         return((double)0.0);
 279     if (P == base)
 280         return((double)1.0);
 281
 282     /* Check cache */
 283     if (st_lookup(table, P, &dummy)) {
 284         res = *dummy;
 285         return(res);
 286     }
 287
 288     res = cuddZddCountDoubleStep(cuddE(P), table, base, empty) +
 289         cuddZddCountDoubleStep(cuddT(P), table, base, empty);
 290
 291     dummy = ALLOC(double, 1);
 292     if (dummy == NULL) {
 293         return((double)CUDD_OUT_OF_MEM);
 294     }
 295     *dummy = res;
 296     if (st_insert(table, (char *)P, (char *)dummy) == ST_OUT_OF_MEM) {
 297         FREE(dummy);
 298         return((double)CUDD_OUT_OF_MEM);
 299     }
 300
 301     return(res);
 302
 303 } /* end of cuddZddCountDoubleStep */
 304
 305
 306 /**Function********************************************************************
 307
 308   Synopsis [Frees the memory associated with the computed table of
 309   Cudd_zddCount.]
 310
 311   Description []
 312
 313   SideEffects [None]
 314
 315   SeeAlso     []
 316
 317 ******************************************************************************/
 318 static enum st_retval
 319 st_zdd_countfree(
 320   char * key,
 321   char * value,
 322   char * arg)
 323 {
 324     int *d;
 325
 326     d = (int *)value;
 327     FREE(d);
 328     return(ST_CONTINUE);
 329
 330 } /* end of st_zdd_countfree */
 331
 332
 333 /**Function********************************************************************
 334
 335   Synopsis [Frees the memory associated with the computed table of
 336   Cudd_zddCountDouble.]
 337
 338   Description []
 339
 340   SideEffects [None]
 341
 342   SeeAlso     []
 343
 344 ******************************************************************************/
 345 static enum st_retval
 346 st_zdd_count_dbl_free(
 347   char * key,
 348   char * value,
 349   char * arg)
 350 {
 351     double      *d;
 352
 353     d = (double *)value;
 354     FREE(d);
 355     return(ST_CONTINUE);
 356
 357 } /* end of st_zdd_count_dbl_free */