src/cuBdd/cuddZddCount.c File Reference

#include "util.h"
#include "cuddInt.h"
Include dependency graph for cuddZddCount.c:

Go to the source code of this file.

Functions

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)
int Cudd_zddCount (DdManager *zdd, DdNode *P)
double Cudd_zddCountDouble (DdManager *zdd, DdNode *P)

Variables

static char rcsid[] DD_UNUSED = "$Id: cuddZddCount.c,v 1.14 2004/08/13 18:04:53 fabio Exp $"

Function Documentation

int Cudd_zddCount ( DdManager *  zdd,
DdNode *  P 
)

AutomaticEnd 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]

Definition at line 133 of file cuddZddCount.c.

00136 {
00137     st_table    *table;
00138     int         res;
00139     DdNode      *base, *empty;
00140 
00141     base  = DD_ONE(zdd);
00142     empty = DD_ZERO(zdd);
00143     table = st_init_table(st_ptrcmp, st_ptrhash);
00144     if (table == NULL) return(CUDD_OUT_OF_MEM);
00145     res = cuddZddCountStep(P, table, base, empty);
00146     if (res == CUDD_OUT_OF_MEM) {
00147         zdd->errorCode = CUDD_MEMORY_OUT;
00148     }
00149     st_foreach(table, st_zdd_countfree, NIL(char));
00150     st_free_table(table);
00151 
00152     return(res);
00153 
00154 } /* end of Cudd_zddCount */

double Cudd_zddCountDouble ( DdManager *  zdd,
DdNode *  P 
)

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]

Definition at line 172 of file cuddZddCount.c.

00175 {
00176     st_table    *table;
00177     double      res;
00178     DdNode      *base, *empty;
00179 
00180     base  = DD_ONE(zdd);
00181     empty = DD_ZERO(zdd);
00182     table = st_init_table(st_ptrcmp, st_ptrhash);
00183     if (table == NULL) return((double)CUDD_OUT_OF_MEM);
00184     res = cuddZddCountDoubleStep(P, table, base, empty);
00185     if (res == (double)CUDD_OUT_OF_MEM) {
00186         zdd->errorCode = CUDD_MEMORY_OUT;
00187     }
00188     st_foreach(table, st_zdd_count_dbl_free, NIL(char));
00189     st_free_table(table);
00190 
00191     return(res);
00192 
00193 } /* end of Cudd_zddCountDouble */

static double cuddZddCountDoubleStep ( DdNode *  P,
st_table *  table,
DdNode *  base,
DdNode *  empty 
) [static]

Function********************************************************************

Synopsis [Performs the recursive step of Cudd_zddCountDouble.]

Description []

SideEffects [None]

SeeAlso []

Definition at line 268 of file cuddZddCount.c.

00273 {
00274     double      res;
00275     double      *dummy;
00276 
00277     if (P == empty)
00278         return((double)0.0);
00279     if (P == base)
00280         return((double)1.0);
00281 
00282     /* Check cache */
00283     if (st_lookup(table, P, &dummy)) {
00284         res = *dummy;
00285         return(res);
00286     }
00287 
00288     res = cuddZddCountDoubleStep(cuddE(P), table, base, empty) +
00289         cuddZddCountDoubleStep(cuddT(P), table, base, empty);
00290 
00291     dummy = ALLOC(double, 1);
00292     if (dummy == NULL) {
00293         return((double)CUDD_OUT_OF_MEM);
00294     }
00295     *dummy = res;
00296     if (st_insert(table, (char *)P, (char *)dummy) == ST_OUT_OF_MEM) {
00297         FREE(dummy);
00298         return((double)CUDD_OUT_OF_MEM);
00299     }
00300 
00301     return(res);
00302 
00303 } /* end of cuddZddCountDoubleStep */

static int cuddZddCountStep ( DdNode *  P,
st_table *  table,
DdNode *  base,
DdNode *  empty 
) [static]

AutomaticStart

Function********************************************************************

Synopsis [Performs the recursive step of Cudd_zddCount.]

Description []

SideEffects [None]

SeeAlso []

Definition at line 218 of file cuddZddCount.c.

00223 {
00224     int         res;
00225     int         *dummy;
00226 
00227     if (P == empty)
00228         return(0);
00229     if (P == base)
00230         return(1);
00231 
00232     /* Check cache. */
00233     if (st_lookup(table, P, &dummy)) {
00234         res = *dummy;
00235         return(res);
00236     }
00237 
00238     res = cuddZddCountStep(cuddE(P), table, base, empty) +
00239         cuddZddCountStep(cuddT(P), table, base, empty);
00240 
00241     dummy = ALLOC(int, 1);
00242     if (dummy == NULL) {
00243         return(CUDD_OUT_OF_MEM);
00244     }
00245     *dummy = res;
00246     if (st_insert(table, (char *)P, (char *)dummy) == ST_OUT_OF_MEM) {
00247         FREE(dummy);
00248         return(CUDD_OUT_OF_MEM);
00249     }
00250 
00251     return(res);
00252 
00253 } /* end of cuddZddCountStep */

static enum st_retval st_zdd_count_dbl_free ( char *  key,
char *  value,
char *  arg 
) [static]

Function********************************************************************

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

Description []

SideEffects [None]

SeeAlso []

Definition at line 346 of file cuddZddCount.c.

00350 {
00351     double      *d;
00352 
00353     d = (double *)value;
00354     FREE(d);
00355     return(ST_CONTINUE);
00356 
00357 } /* end of st_zdd_count_dbl_free */

static enum st_retval st_zdd_countfree ( char *  key,
char *  value,
char *  arg 
) [static]

Function********************************************************************

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

Description []

SideEffects [None]

SeeAlso []

Definition at line 319 of file cuddZddCount.c.

00323 {
00324     int *d;
00325 
00326     d = (int *)value;
00327     FREE(d);
00328     return(ST_CONTINUE);
00329 
00330 } /* end of st_zdd_countfree */

Variable Documentation

char rcsid [] DD_UNUSED = "$Id: cuddZddCount.c,v 1.14 2004/08/13 18:04:53 fabio Exp $" [static]

CFile***********************************************************************

FileName [cuddZddCount.c]

PackageName [cudd]

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

Description [External procedures included in this module:

Internal procedures included in this module:

procedures included in this module:

]

SeeAlso []

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

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.]

Definition at line 87 of file cuddZddCount.c.

Generated on Tue Jan 12 13:57:22 2010 for glu-2.2 by  doxygen 1.6.1