cuddZddCount.c 10.5 KB
Newer Older
Alan Mishchenko committed
1 2 3 4 5 6 7 8 9
/**CFile***********************************************************************

  FileName    [cuddZddCount.c]

  PackageName [cudd]

  Synopsis    [Procedures to count the number of minterms of a ZDD.]

  Description [External procedures included in this module:
10 11 12 13 14 15 16 17 18 19 20
                    <ul>
                    <li> Cudd_zddCount();
                    <li> Cudd_zddCountDouble();
                    </ul>
               Internal procedures included in this module:
                    <ul>
                    </ul>
               Static procedures included in this module:
                    <ul>
                    <li> cuddZddCountStep();
                    <li> cuddZddCountDoubleStep();
21 22
                    <li> st__zdd_count_dbl_free()
                    <li> st__zdd_countfree()
23 24
                    </ul>
              ]
Alan Mishchenko committed
25 26 27 28 29

  SeeAlso     []

  Author      [Hyong-Kyoon Shin, In-Ho Moon]

30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60
  Copyright   [Copyright (c) 1995-2004, Regents of the University of Colorado

  All rights reserved.

  Redistribution and use in source and binary forms, with or without
  modification, are permitted provided that the following conditions
  are met:

  Redistributions of source code must retain the above copyright
  notice, this list of conditions and the following disclaimer.

  Redistributions in binary form must reproduce the above copyright
  notice, this list of conditions and the following disclaimer in the
  documentation and/or other materials provided with the distribution.

  Neither the name of the University of Colorado nor the names of its
  contributors may be used to endorse or promote products derived from
  this software without specific prior written permission.

  THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
  "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
  LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
  FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
  COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
  INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
  BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
  LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
  CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
  LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
  ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
  POSSIBILITY OF SUCH DAMAGE.]
Alan Mishchenko committed
61 62 63

******************************************************************************/

64
#include "misc/util/util_hack.h"
65
#include "cuddInt.h"
Alan Mishchenko committed
66

67 68 69
ABC_NAMESPACE_IMPL_START


70

Alan Mishchenko committed
71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90
/*---------------------------------------------------------------------------*/
/* Constant declarations                                                     */
/*---------------------------------------------------------------------------*/


/*---------------------------------------------------------------------------*/
/* Stucture declarations                                                     */
/*---------------------------------------------------------------------------*/


/*---------------------------------------------------------------------------*/
/* Type declarations                                                         */
/*---------------------------------------------------------------------------*/


/*---------------------------------------------------------------------------*/
/* Variable declarations                                                     */
/*---------------------------------------------------------------------------*/

#ifndef lint
91
static char rcsid[] DD_UNUSED = "$Id: cuddZddCount.c,v 1.14 2004/08/13 18:04:53 fabio Exp $";
Alan Mishchenko committed
92 93 94 95 96 97 98 99 100 101 102 103
#endif

/*---------------------------------------------------------------------------*/
/* Macro declarations                                                        */
/*---------------------------------------------------------------------------*/

/**AutomaticStart*************************************************************/

/*---------------------------------------------------------------------------*/
/* Static function prototypes                                                */
/*---------------------------------------------------------------------------*/

104 105 106 107
static int cuddZddCountStep (DdNode *P, st__table *table, DdNode *base, DdNode *empty);
static double cuddZddCountDoubleStep (DdNode *P, st__table *table, DdNode *base, DdNode *empty);
static enum st__retval st__zdd_countfree (char *key, char *value, char *arg);
static enum st__retval st__zdd_count_dbl_free (char *key, char *value, char *arg);
Alan Mishchenko committed
108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132

/**AutomaticEnd***************************************************************/

/*---------------------------------------------------------------------------*/
/* Definition of exported functions                                          */
/*---------------------------------------------------------------------------*/


/**Function********************************************************************

  Synopsis [Counts the number of minterms in a ZDD.]

  Description [Returns an integer representing the number of minterms
  in a ZDD.]

  SideEffects [None]

  SeeAlso     [Cudd_zddCountDouble]

******************************************************************************/
int
Cudd_zddCount(
  DdManager * zdd,
  DdNode * P)
{
133
    st__table    *table;
134 135
    int         res;
    DdNode      *base, *empty;
Alan Mishchenko committed
136 137 138

    base  = DD_ONE(zdd);
    empty = DD_ZERO(zdd);
139
    table = st__init_table( st__ptrcmp, st__ptrhash);
Alan Mishchenko committed
140 141 142
    if (table == NULL) return(CUDD_OUT_OF_MEM);
    res = cuddZddCountStep(P, table, base, empty);
    if (res == CUDD_OUT_OF_MEM) {
143
        zdd->errorCode = CUDD_MEMORY_OUT;
Alan Mishchenko committed
144
    }
145 146
    st__foreach(table, st__zdd_countfree, NIL(char));
    st__free_table(table);
Alan Mishchenko committed
147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171

    return(res);

} /* end of Cudd_zddCount */


/**Function********************************************************************

  Synopsis [Counts the number of minterms of a ZDD.]

  Description [Counts the number of minterms of a ZDD. The result is
  returned as a double. If the procedure runs out of memory, it
  returns (double) CUDD_OUT_OF_MEM. This procedure is used in
  Cudd_zddCountMinterm.]

  SideEffects [None]

  SeeAlso     [Cudd_zddCountMinterm Cudd_zddCount]

******************************************************************************/
double
Cudd_zddCountDouble(
  DdManager * zdd,
  DdNode * P)
{
172
    st__table    *table;
173 174
    double      res;
    DdNode      *base, *empty;
Alan Mishchenko committed
175 176 177

    base  = DD_ONE(zdd);
    empty = DD_ZERO(zdd);
178
    table = st__init_table( st__ptrcmp, st__ptrhash);
Alan Mishchenko committed
179 180 181
    if (table == NULL) return((double)CUDD_OUT_OF_MEM);
    res = cuddZddCountDoubleStep(P, table, base, empty);
    if (res == (double)CUDD_OUT_OF_MEM) {
182
        zdd->errorCode = CUDD_MEMORY_OUT;
Alan Mishchenko committed
183
    }
184 185
    st__foreach(table, st__zdd_count_dbl_free, NIL(char));
    st__free_table(table);
Alan Mishchenko committed
186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215

    return(res);

} /* end of Cudd_zddCountDouble */


/*---------------------------------------------------------------------------*/
/* Definition of internal functions                                          */
/*---------------------------------------------------------------------------*/


/*---------------------------------------------------------------------------*/
/* Definition of static functions                                            */
/*---------------------------------------------------------------------------*/


/**Function********************************************************************

  Synopsis [Performs the recursive step of Cudd_zddCount.]

  Description []

  SideEffects [None]

  SeeAlso     []

******************************************************************************/
static int
cuddZddCountStep(
  DdNode * P,
216
  st__table * table,
Alan Mishchenko committed
217 218 219
  DdNode * base,
  DdNode * empty)
{
220 221
    int         res;
    int         *dummy;
Alan Mishchenko committed
222 223

    if (P == empty)
224
        return(0);
Alan Mishchenko committed
225
    if (P == base)
226
        return(1);
Alan Mishchenko committed
227 228

    /* Check cache. */
229
    if ( st__lookup(table, (const char *)P, (char **)&dummy)) {
230 231
        res = *dummy;
        return(res);
Alan Mishchenko committed
232 233 234
    }

    res = cuddZddCountStep(cuddE(P), table, base, empty) +
235
        cuddZddCountStep(cuddT(P), table, base, empty);
Alan Mishchenko committed
236

Alan Mishchenko committed
237
    dummy = ABC_ALLOC(int, 1);
Alan Mishchenko committed
238
    if (dummy == NULL) {
239
        return(CUDD_OUT_OF_MEM);
Alan Mishchenko committed
240 241
    }
    *dummy = res;
242
    if ( st__insert(table, (char *)P, (char *)dummy) == st__OUT_OF_MEM) {
243 244
        ABC_FREE(dummy);
        return(CUDD_OUT_OF_MEM);
Alan Mishchenko committed
245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265
    }

    return(res);

} /* end of cuddZddCountStep */


/**Function********************************************************************

  Synopsis [Performs the recursive step of Cudd_zddCountDouble.]

  Description []

  SideEffects [None]

  SeeAlso     []

******************************************************************************/
static double
cuddZddCountDoubleStep(
  DdNode * P,
266
  st__table * table,
Alan Mishchenko committed
267 268 269
  DdNode * base,
  DdNode * empty)
{
270 271
    double      res;
    double      *dummy;
Alan Mishchenko committed
272 273

    if (P == empty)
274
        return((double)0.0);
Alan Mishchenko committed
275
    if (P == base)
276
        return((double)1.0);
Alan Mishchenko committed
277 278

    /* Check cache */
279
    if ( st__lookup(table, (const char *)P, (char **)&dummy)) {
280 281
        res = *dummy;
        return(res);
Alan Mishchenko committed
282 283 284
    }

    res = cuddZddCountDoubleStep(cuddE(P), table, base, empty) +
285
        cuddZddCountDoubleStep(cuddT(P), table, base, empty);
Alan Mishchenko committed
286

Alan Mishchenko committed
287
    dummy = ABC_ALLOC(double, 1);
Alan Mishchenko committed
288
    if (dummy == NULL) {
289
        return((double)CUDD_OUT_OF_MEM);
Alan Mishchenko committed
290 291
    }
    *dummy = res;
292
    if ( st__insert(table, (char *)P, (char *)dummy) == st__OUT_OF_MEM) {
293 294
        ABC_FREE(dummy);
        return((double)CUDD_OUT_OF_MEM);
Alan Mishchenko committed
295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313
    }

    return(res);

} /* end of cuddZddCountDoubleStep */


/**Function********************************************************************

  Synopsis [Frees the memory associated with the computed table of
  Cudd_zddCount.]

  Description []

  SideEffects [None]

  SeeAlso     []

******************************************************************************/
314 315
static enum st__retval
 st__zdd_countfree(
Alan Mishchenko committed
316 317 318 319
  char * key,
  char * value,
  char * arg)
{
320
    int *d;
Alan Mishchenko committed
321 322

    d = (int *)value;
Alan Mishchenko committed
323
    ABC_FREE(d);
324
    return( st__CONTINUE);
Alan Mishchenko committed
325

326
} /* end of st__zdd_countfree */
Alan Mishchenko committed
327 328 329 330 331 332 333 334 335 336 337 338 339 340


/**Function********************************************************************

  Synopsis [Frees the memory associated with the computed table of
  Cudd_zddCountDouble.]

  Description []

  SideEffects [None]

  SeeAlso     []

******************************************************************************/
341 342
static enum st__retval
 st__zdd_count_dbl_free(
Alan Mishchenko committed
343 344 345 346
  char * key,
  char * value,
  char * arg)
{
347
    double      *d;
Alan Mishchenko committed
348 349

    d = (double *)value;
Alan Mishchenko committed
350
    ABC_FREE(d);
351
    return( st__CONTINUE);
Alan Mishchenko committed
352

353
} /* end of st__zdd_count_dbl_free */
354 355


356 357
ABC_NAMESPACE_IMPL_END