Upgrade to the latest CUDD 2.4.2.

1 files changed, 57 insertions, 25 deletions

diff --git a/src/bdd/cudd/cuddAddInv.c b/src/bdd/cudd/cuddAddInv.c
index 05650c0e..cae00ca1 100644
--- a/src/bdd/cudd/cuddAddInv.c
+++ b/src/bdd/cudd/cuddAddInv.c
@@ -7,20 +7,47 @@
   Synopsis    [Function to compute the scalar inverse of an ADD.]
 
   Description [External procedures included in this module:
-        <ul>
-        <li> Cudd_addScalarInverse()
-        </ul>
-        Internal procedures included in this module:
-        <ul>
-        <li> cuddAddScalarInverseRecur()
-        </ul>]
+                <ul>
+                <li> Cudd_addScalarInverse()
+                </ul>
+            Internal procedures included in this module:
+                <ul>
+                <li> cuddAddScalarInverseRecur()
+                </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.]
 
 ******************************************************************************/
 
@@ -31,6 +58,7 @@ ABC_NAMESPACE_IMPL_START
 
 
 
+
 /*---------------------------------------------------------------------------*/
 /* Constant declarations                                                     */
 /*---------------------------------------------------------------------------*/
@@ -51,7 +79,7 @@ ABC_NAMESPACE_IMPL_START
 /*---------------------------------------------------------------------------*/
 
 #ifndef lint
-static char rcsid[] DD_UNUSED = "$Id: cuddAddInv.c,v 1.1.1.1 2003/02/24 22:23:50 wjiang Exp $";
+static char rcsid[] DD_UNUSED = "$Id: cuddAddInv.c,v 1.9 2004/08/13 18:04:45 fabio Exp $";
 #endif
 
 
@@ -97,12 +125,12 @@ Cudd_addScalarInverse(
     DdNode *res;
 
     if (!cuddIsConstant(epsilon)) {
-    (void) fprintf(dd->err,"Invalid epsilon\n");
-    return(NULL);
+        (void) fprintf(dd->err,"Invalid epsilon\n");
+        return(NULL);
     }
     do {
-    dd->reordered = 0;
-    res  = cuddAddScalarInverseRecur(dd,f,epsilon);
+        dd->reordered = 0;
+        res  = cuddAddScalarInverseRecur(dd,f,epsilon);
     } while (dd->reordered == 1);
     return(res);
 
@@ -135,10 +163,10 @@ cuddAddScalarInverseRecur(
 
     statLine(dd);
     if (cuddIsConstant(f)) {
-    if (ddAbs(cuddV(f)) < cuddV(epsilon)) return(NULL);
-    value = 1.0 / cuddV(f);
-    res = cuddUniqueConst(dd,value);
-    return(res);
+        if (ddAbs(cuddV(f)) < cuddV(epsilon)) return(NULL);
+        value = 1.0 / cuddV(f);
+        res = cuddUniqueConst(dd,value);
+        return(res);
     }
 
     res = cuddCacheLookup2(dd,Cudd_addScalarInverse,f,epsilon);
@@ -150,17 +178,19 @@ cuddAddScalarInverseRecur(
 
     e = cuddAddScalarInverseRecur(dd,cuddE(f),epsilon);
     if (e == NULL) {
-    Cudd_RecursiveDeref(dd, t);
-    return(NULL);
+        Cudd_RecursiveDeref(dd, t);
+        return(NULL);
     }
     cuddRef(e);
 
     res = (t == e) ? t : cuddUniqueInter(dd,(int)f->index,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);
 
     cuddCacheInsert2(dd,Cudd_addScalarInverse,f,epsilon,res);
 
@@ -173,5 +203,7 @@ cuddAddScalarInverseRecur(
 /* Definition of static functions                                            */
 /*---------------------------------------------------------------------------*/
 
+
 ABC_NAMESPACE_IMPL_END
 
+