diff options
Diffstat (limited to 'src/bdd/cudd/cuddZddCount.c')
-rw-r--r-- | src/bdd/cudd/cuddZddCount.c | 152 |
1 files changed, 94 insertions, 58 deletions
diff --git a/src/bdd/cudd/cuddZddCount.c b/src/bdd/cudd/cuddZddCount.c index 8f974e5e..a422ad99 100644 --- a/src/bdd/cudd/cuddZddCount.c +++ b/src/bdd/cudd/cuddZddCount.c @@ -7,39 +7,67 @@ Synopsis [Procedures to count the number of minterms of a ZDD.] Description [External procedures included in this module: - <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(); - <li> st_zdd_count_dbl_free() - <li> st_zdd_countfree() - </ul> - ] + <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(); + <li> st_zdd_count_dbl_free() + <li> st_zdd_countfree() + </ul> + ] 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.] + 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.] ******************************************************************************/ -#include "util_hack.h" -#include "cuddInt.h" +#include "util_hack.h" +#include "cuddInt.h" ABC_NAMESPACE_IMPL_START + /*---------------------------------------------------------------------------*/ /* Constant declarations */ /*---------------------------------------------------------------------------*/ @@ -60,13 +88,16 @@ ABC_NAMESPACE_IMPL_START /*---------------------------------------------------------------------------*/ #ifndef lint -static char rcsid[] DD_UNUSED = "$Id: cuddZddCount.c,v 1.1.1.1 2003/02/24 22:23:53 wjiang Exp $"; +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 /**AutomaticStart*************************************************************/ @@ -74,13 +105,16 @@ static char rcsid[] DD_UNUSED = "$Id: cuddZddCount.c,v 1.1.1.1 2003/02/24 22:23: /* Static function prototypes */ /*---------------------------------------------------------------------------*/ -static int cuddZddCountStep ARGS((DdNode *P, st_table *table, DdNode *base, DdNode *empty)); -static double cuddZddCountDoubleStep ARGS((DdNode *P, st_table *table, DdNode *base, DdNode *empty)); -static enum st_retval st_zdd_countfree ARGS((char *key, char *value, char *arg)); -static enum st_retval st_zdd_count_dbl_free ARGS((char *key, char *value, char *arg)); +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); /**AutomaticEnd***************************************************************/ +#ifdef __cplusplus +} +#endif /*---------------------------------------------------------------------------*/ /* Definition of exported functions */ @@ -105,8 +139,8 @@ Cudd_zddCount( DdNode * P) { st_table *table; - int res; - DdNode *base, *empty; + int res; + DdNode *base, *empty; base = DD_ONE(zdd); empty = DD_ZERO(zdd); @@ -114,9 +148,9 @@ Cudd_zddCount( 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; + zdd->errorCode = CUDD_MEMORY_OUT; } - st_foreach(table, (ST_PFSR)st_zdd_countfree, NIL(char)); + st_foreach(table, st_zdd_countfree, NIL(char)); st_free_table(table); return(res); @@ -144,8 +178,8 @@ Cudd_zddCountDouble( DdNode * P) { st_table *table; - double res; - DdNode *base, *empty; + double res; + DdNode *base, *empty; base = DD_ONE(zdd); empty = DD_ZERO(zdd); @@ -153,9 +187,9 @@ Cudd_zddCountDouble( 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; + zdd->errorCode = CUDD_MEMORY_OUT; } - st_foreach(table, (ST_PFSR)st_zdd_count_dbl_free, NIL(char)); + st_foreach(table, st_zdd_count_dbl_free, NIL(char)); st_free_table(table); return(res); @@ -191,31 +225,31 @@ cuddZddCountStep( DdNode * base, DdNode * empty) { - int res; - int *dummy; + int res; + int *dummy; if (P == empty) - return(0); + return(0); if (P == base) - return(1); + return(1); /* Check cache. */ - if (st_lookup(table, (char *)P, (char **)(&dummy))) { - res = *dummy; - return(res); + if (st_lookup(table, (const char *)P, (char **)&dummy)) { + res = *dummy; + return(res); } res = cuddZddCountStep(cuddE(P), table, base, empty) + - cuddZddCountStep(cuddT(P), table, base, empty); + cuddZddCountStep(cuddT(P), table, base, empty); dummy = ABC_ALLOC(int, 1); if (dummy == NULL) { - return(CUDD_OUT_OF_MEM); + return(CUDD_OUT_OF_MEM); } *dummy = res; if (st_insert(table, (char *)P, (char *)dummy) == ST_OUT_OF_MEM) { - ABC_FREE(dummy); - return(CUDD_OUT_OF_MEM); + ABC_FREE(dummy); + return(CUDD_OUT_OF_MEM); } return(res); @@ -241,31 +275,31 @@ cuddZddCountDoubleStep( DdNode * base, DdNode * empty) { - double res; - double *dummy; + double res; + double *dummy; if (P == empty) - return((double)0.0); + return((double)0.0); if (P == base) - return((double)1.0); + return((double)1.0); /* Check cache */ - if (st_lookup(table, (char *)P, (char **)(&dummy))) { - res = *dummy; - return(res); + if (st_lookup(table, (const char *)P, (char **)&dummy)) { + res = *dummy; + return(res); } res = cuddZddCountDoubleStep(cuddE(P), table, base, empty) + - cuddZddCountDoubleStep(cuddT(P), table, base, empty); + cuddZddCountDoubleStep(cuddT(P), table, base, empty); dummy = ABC_ALLOC(double, 1); if (dummy == NULL) { - return((double)CUDD_OUT_OF_MEM); + return((double)CUDD_OUT_OF_MEM); } *dummy = res; if (st_insert(table, (char *)P, (char *)dummy) == ST_OUT_OF_MEM) { - ABC_FREE(dummy); - return((double)CUDD_OUT_OF_MEM); + ABC_FREE(dummy); + return((double)CUDD_OUT_OF_MEM); } return(res); @@ -291,7 +325,7 @@ st_zdd_countfree( char * value, char * arg) { - int *d; + int *d; d = (int *)value; ABC_FREE(d); @@ -318,12 +352,14 @@ st_zdd_count_dbl_free( char * value, char * arg) { - double *d; + double *d; d = (double *)value; ABC_FREE(d); return(ST_CONTINUE); } /* end of st_zdd_count_dbl_free */ + + ABC_NAMESPACE_IMPL_END |