src/bdd/cudd/cuddZddCount.c File Reference

#include "util_hack.h"
#include "cuddInt.h"

Include dependency graph for cuddZddCount.c:

Go to the source code of this file.

Functions
static int cuddZddCountStep	ARGS ((DdNode *P, st_table *table, DdNode *base, DdNode *empty))
static enum st_retval st_zdd_countfree	ARGS ((char *key, char *value, char *arg))
int	Cudd_zddCount (DdManager *zdd, DdNode *P)
double	Cudd_zddCountDouble (DdManager *zdd, DdNode *P)
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)
Variables
static char rcsid[]	DD_UNUSED = "$Id: cuddZddCount.c,v 1.1.1.1 2003/02/24 22:23:53 wjiang Exp $"

---

Function Documentation

static enum st_retval st_zdd_count_dbl_free ARGS

(

(char *key, char *value, char *arg)

)

[static]

static double cuddZddCountDoubleStep ARGS

(

(DdNode *P, st_table *table, DdNode *base, DdNode *empty)

)

[static]

AutomaticStart

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 100 of file cuddZddCount.c.

{
    st_table    *table;
    int         res;
    DdNode      *base, *empty;

    base  = DD_ONE(zdd);
    empty = DD_ZERO(zdd);
    table = st_init_table(st_ptrcmp, st_ptrhash);
    if (table == NULL) return(CUDD_OUT_OF_MEM);
    res = cuddZddCountStep(P, table, base, empty);
    if (res == CUDD_OUT_OF_MEM) {
        zdd->errorCode = CUDD_MEMORY_OUT;
    }
    st_foreach(table, st_zdd_countfree, NIL(char));
    st_free_table(table);

    return(res);

} /* 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 139 of file cuddZddCount.c.

{
    st_table    *table;
    double      res;
    DdNode      *base, *empty;

    base  = DD_ONE(zdd);
    empty = DD_ZERO(zdd);
    table = st_init_table(st_ptrcmp, st_ptrhash);
    if (table == NULL) return((double)CUDD_OUT_OF_MEM);
    res = cuddZddCountDoubleStep(P, table, base, empty);
    if (res == (double)CUDD_OUT_OF_MEM) {
        zdd->errorCode = CUDD_MEMORY_OUT;
    }
    st_foreach(table, st_zdd_count_dbl_free, NIL(char));
    st_free_table(table);

    return(res);

} /* 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 235 of file cuddZddCount.c.

{
    double      res;
    double      *dummy;

    if (P == empty)
        return((double)0.0);
    if (P == base)
        return((double)1.0);

    /* Check cache */
    if (st_lookup(table, (char *)P, (char **)(&dummy))) {
        res = *dummy;
        return(res);
    }

    res = cuddZddCountDoubleStep(cuddE(P), table, base, empty) +
        cuddZddCountDoubleStep(cuddT(P), table, base, empty);

    dummy = ALLOC(double, 1);
    if (dummy == NULL) {
        return((double)CUDD_OUT_OF_MEM);
    }
    *dummy = res;
    if (st_insert(table, (char *)P, (char *)dummy) == ST_OUT_OF_MEM) {
        FREE(dummy);
        return((double)CUDD_OUT_OF_MEM);
    }

    return(res);

} /* end of cuddZddCountDoubleStep */

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

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

Synopsis [Performs the recursive step of Cudd_zddCount.]

Description []

SideEffects [None]

SeeAlso []

Definition at line 185 of file cuddZddCount.c.

{
    int         res;
    int         *dummy;

    if (P == empty)
        return(0);
    if (P == base)
        return(1);

    /* Check cache. */
    if (st_lookup(table, (char *)P, (char **)(&dummy))) {
        res = *dummy;
        return(res);
    }

    res = cuddZddCountStep(cuddE(P), table, base, empty) +
        cuddZddCountStep(cuddT(P), table, base, empty);

    dummy = ALLOC(int, 1);
    if (dummy == NULL) {
        return(CUDD_OUT_OF_MEM);
    }
    *dummy = res;
    if (st_insert(table, (char *)P, (char *)dummy) == ST_OUT_OF_MEM) {
        FREE(dummy);
        return(CUDD_OUT_OF_MEM);
    }

    return(res);

} /* 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 313 of file cuddZddCount.c.

{
    double      *d;

    d = (double *)value;
    FREE(d);
    return(ST_CONTINUE);

} /* 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 286 of file cuddZddCount.c.

{
    int *d;

    d = (int *)value;
    FREE(d);
    return(ST_CONTINUE);

} /* end of st_zdd_countfree */

---

Variable Documentation

char rcsid [] DD_UNUSED = "$Id: cuddZddCount.c,v 1.1.1.1 2003/02/24 22:23:53 wjiang 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:

• Cudd_zddCount();
• Cudd_zddCountDouble();

Internal procedures included in this module:

procedures included in this module:

• cuddZddCountStep();
• cuddZddCountDoubleStep();
• st_zdd_count_dbl_free()
• st_zdd_countfree()

]

SeeAlso []

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

Copyright [ This file was created at the University of Colorado at Boulder. The University of Colorado at Boulder makes no warranty about the suitability of this software for any purpose. It is presented on an AS IS basis.]

Definition at line 60 of file cuddZddCount.c.