Upgrade to the latest CUDD 2.4.2.

1 files changed, 67 insertions, 31 deletions

diff --git a/src/bdd/cudd/cuddAddFind.c b/src/bdd/cudd/cuddAddFind.c
index 6cc58f2d..4d63965d 100644
--- a/src/bdd/cudd/cuddAddFind.c
+++ b/src/bdd/cudd/cuddAddFind.c
@@ -8,22 +8,49 @@
   extract the i-th bit.]
 
   Description [External procedures included in this module:
-        <ul>
-        <li> Cudd_addFindMax()
-        <li> Cudd_addFindMin()
-        <li> Cudd_addIthBit()
-        </ul>
-           Static functions included in this module:
-        <ul>
-        <li> addDoIthBit()
-        </ul>]
+                <ul>
+                <li> Cudd_addFindMax()
+                <li> Cudd_addFindMin()
+                <li> Cudd_addIthBit()
+                </ul>
+               Static functions included in this module:
+                <ul>
+                <li> addDoIthBit()
+                </ul>]
 
   Author      [Fabio Somenzi]
 
-  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.]
 
 ******************************************************************************/
 
@@ -33,6 +60,7 @@
 ABC_NAMESPACE_IMPL_START
 
 
+
 /*---------------------------------------------------------------------------*/
 /* Constant declarations                                                     */
 /*---------------------------------------------------------------------------*/
@@ -53,7 +81,7 @@ ABC_NAMESPACE_IMPL_START
 /*---------------------------------------------------------------------------*/
 
 #ifndef lint
-static char rcsid[] DD_UNUSED = "$Id: cuddAddFind.c,v 1.1.1.1 2003/02/24 22:23:50 wjiang Exp $";
+static char rcsid[] DD_UNUSED = "$Id: cuddAddFind.c,v 1.8 2004/08/13 18:04:45 fabio Exp $";
 #endif
 
 
@@ -61,6 +89,9 @@ static char rcsid[] DD_UNUSED = "$Id: cuddAddFind.c,v 1.1.1.1 2003/02/24 22:23:5
 /* Macro declarations                                                        */
 /*---------------------------------------------------------------------------*/
 
+#ifdef __cplusplus
+extern "C" {
+#endif
 
 /**AutomaticStart*************************************************************/
 
@@ -68,10 +99,13 @@ static char rcsid[] DD_UNUSED = "$Id: cuddAddFind.c,v 1.1.1.1 2003/02/24 22:23:5
 /* Static function prototypes                                                */
 /*---------------------------------------------------------------------------*/
 
-static DdNode * addDoIthBit ARGS((DdManager *dd, DdNode *f, DdNode *index));
+static DdNode * addDoIthBit (DdManager *dd, DdNode *f, DdNode *index);
 
 /**AutomaticEnd***************************************************************/
 
+#ifdef __cplusplus
+}
+#endif
 
 /*---------------------------------------------------------------------------*/
 /* Definition of exported functions                                          */
@@ -95,12 +129,12 @@ Cudd_addFindMax(
 
     statLine(dd);
     if (cuddIsConstant(f)) {
-    return(f);
+        return(f);
     }
 
     res = cuddCacheLookup1(dd,Cudd_addFindMax,f);
     if (res != NULL) {
-    return(res);
+        return(res);
     }
 
     t  = Cudd_addFindMax(dd,cuddT(f));
@@ -135,12 +169,12 @@ Cudd_addFindMin(
 
     statLine(dd);
     if (cuddIsConstant(f)) {
-    return(f);
+        return(f);
     }
 
     res = cuddCacheLookup1(dd,Cudd_addFindMin,f);
     if (res != NULL) {
-    return(res);
+        return(res);
     }
 
     t  = Cudd_addFindMin(dd,cuddT(f));
@@ -192,13 +226,13 @@ Cudd_addIthBit(
     cuddRef(index);
 
     do {
-    dd->reordered = 0;
-    res = addDoIthBit(dd, f, index);
+        dd->reordered = 0;
+        res = addDoIthBit(dd, f, index);
     } while (dd->reordered == 1);
 
     if (res == NULL) {
-    Cudd_RecursiveDeref(dd, index);
-    return(NULL);
+        Cudd_RecursiveDeref(dd, index);
+        return(NULL);
     }
     cuddRef(res);
     Cudd_RecursiveDeref(dd, index);
@@ -244,9 +278,9 @@ addDoIthBit(
     statLine(dd);
     /* Check terminal case. */
     if (cuddIsConstant(f)) {
-    mask = 1 << ((int) cuddV(index));
-    value = (int) cuddV(f);
-    return((value & mask) == 0 ? DD_ZERO(dd) : DD_ONE(dd));
+        mask = 1 << ((int) cuddV(index));
+        value = (int) cuddV(f);
+        return((value & mask) == 0 ? DD_ZERO(dd) : DD_ONE(dd));
     }
 
     /* Check cache. */
@@ -263,16 +297,16 @@ addDoIthBit(
 
     E = addDoIthBit(dd,fvn,index);
     if (E == NULL) {
-    Cudd_RecursiveDeref(dd, T);
-    return(NULL);
+        Cudd_RecursiveDeref(dd, T);
+        return(NULL);
     }
     cuddRef(E);
 
     res = (T == E) ? T : cuddUniqueInter(dd,v,T,E);
     if (res == NULL) {
-    Cudd_RecursiveDeref(dd, T);
-    Cudd_RecursiveDeref(dd, E);
-    return(NULL);
+        Cudd_RecursiveDeref(dd, T);
+        Cudd_RecursiveDeref(dd, E);
+        return(NULL);
     }
     cuddDeref(T);
     cuddDeref(E);
@@ -284,5 +318,7 @@ addDoIthBit(
 
 } /* end of addDoIthBit */
 
+
 ABC_NAMESPACE_IMPL_END
 
+