Upgrade to the latest CUDD 2.4.2.

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