src/cuBdd/cuddZddCount.c

Go to the documentation of this file.

#include "util.h"
#include "cuddInt.h"

/*---------------------------------------------------------------------------*/
/* Constant declarations                                                     */
/*---------------------------------------------------------------------------*/


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


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


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

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

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

#ifdef __cplusplus
extern "C" {
#endif

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

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);

#ifdef __cplusplus
}
#endif

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


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


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


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


static int
cuddZddCountStep(
  DdNode * P,
  st_table * table,
  DdNode * base,
  DdNode * empty)
{
    int         res;
    int         *dummy;

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

    /* Check cache. */
    if (st_lookup(table, P, &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 double
cuddZddCountDoubleStep(
  DdNode * P,
  st_table * table,
  DdNode * base,
  DdNode * empty)
{
    double      res;
    double      *dummy;

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

    /* Check cache */
    if (st_lookup(table, P, &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 enum st_retval
st_zdd_countfree(
  char * key,
  char * value,
  char * arg)
{
    int *d;

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

} /* end of st_zdd_countfree */


static enum st_retval
st_zdd_count_dbl_free(
  char * key,
  char * value,
  char * arg)
{
    double      *d;

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

} /* end of st_zdd_count_dbl_free */

---