Upgrade to the latest CUDD 2.4.2.

1 files changed, 172 insertions, 142 deletions

diff --git a/src/bdd/cudd/cuddClip.c b/src/bdd/cudd/cuddClip.c
index 23331339..028474fe 100644
--- a/src/bdd/cudd/cuddClip.c
+++ b/src/bdd/cudd/cuddClip.c
@@ -7,29 +7,56 @@
   Synopsis    [Clipping functions.]
 
   Description [External procedures included in this module:
-        <ul>
-        <li> Cudd_bddClippingAnd()
-        <li> Cudd_bddClippingAndAbstract()
-        </ul>
+                <ul>
+                <li> Cudd_bddClippingAnd()
+                <li> Cudd_bddClippingAndAbstract()
+                </ul>
        Internal procedures included in this module:
-        <ul>
-        <li> cuddBddClippingAnd()
-        <li> cuddBddClippingAndAbstract()
-        </ul>
+                <ul>
+                <li> cuddBddClippingAnd()
+                <li> cuddBddClippingAndAbstract()
+                </ul>
        Static procedures included in this module:
-        <ul>
-        <li> cuddBddClippingAndRecur()
-        <li> cuddBddClipAndAbsRecur()
-        </ul>
+                <ul>
+                <li> cuddBddClippingAndRecur()
+                <li> cuddBddClipAndAbsRecur()
+                </ul>
 
   SeeAlso     []
 
   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.]
 
 ******************************************************************************/
 
@@ -40,6 +67,7 @@ ABC_NAMESPACE_IMPL_START
 
 
 
+
 /*---------------------------------------------------------------------------*/
 /* Constant declarations                                                     */
 /*---------------------------------------------------------------------------*/
@@ -59,7 +87,7 @@ ABC_NAMESPACE_IMPL_START
 /*---------------------------------------------------------------------------*/
 
 #ifndef lint
-static char rcsid[] DD_UNUSED = "$Id: cuddClip.c,v 1.1.1.1 2003/02/24 22:23:51 wjiang Exp $";
+static char rcsid[] DD_UNUSED = "$Id: cuddClip.c,v 1.8 2004/08/13 18:04:47 fabio Exp $";
 #endif
 
 /*---------------------------------------------------------------------------*/
@@ -73,8 +101,8 @@ static char rcsid[] DD_UNUSED = "$Id: cuddClip.c,v 1.1.1.1 2003/02/24 22:23:51 w
 /* Static function prototypes                                                */
 /*---------------------------------------------------------------------------*/
 
-static DdNode * cuddBddClippingAndRecur ARGS((DdManager *manager, DdNode *f, DdNode *g, int distance, int direction));
-static DdNode * cuddBddClipAndAbsRecur ARGS((DdManager *manager, DdNode *f, DdNode *g, DdNode *cube, int distance, int direction));
+static DdNode * cuddBddClippingAndRecur (DdManager *manager, DdNode *f, DdNode *g, int distance, int direction);
+static DdNode * cuddBddClipAndAbsRecur (DdManager *manager, DdNode *f, DdNode *g, DdNode *cube, int distance, int direction);
 
 /**AutomaticEnd***************************************************************/
 
@@ -108,8 +136,8 @@ Cudd_bddClippingAnd(
     DdNode *res;
 
     do {
-    dd->reordered = 0;
-    res = cuddBddClippingAnd(dd,f,g,maxDepth,direction);
+        dd->reordered = 0;
+        res = cuddBddClippingAnd(dd,f,g,maxDepth,direction);
     } while (dd->reordered == 1);
     return(res);
 
@@ -143,8 +171,8 @@ Cudd_bddClippingAndAbstract(
     DdNode *res;
 
     do {
-    dd->reordered = 0;
-    res = cuddBddClippingAndAbstract(dd,f,g,cube,maxDepth,direction);
+        dd->reordered = 0;
+        res = cuddBddClippingAndAbstract(dd,f,g,cube,maxDepth,direction);
     } while (dd->reordered == 1);
     return(res);
 
@@ -248,7 +276,7 @@ cuddBddClippingAndRecur(
     DdNode *F, *ft, *fe, *G, *gt, *ge;
     DdNode *one, *zero, *r, *t, *e;
     unsigned int topf, topg, index;
-    DdNode *(*cacheOp)(DdManager *, DdNode *, DdNode *);
+    DD_CTFP cacheOp;
 
     statLine(manager);
     one = DD_ONE(manager);
@@ -259,15 +287,15 @@ cuddBddClippingAndRecur(
     if (f == g || g == one) return(f);
     if (f == one) return(g);
     if (distance == 0) {
-    /* One last attempt at returning the right result. We sort of
-    ** cheat by calling Cudd_bddLeq. */
-    if (Cudd_bddLeq(manager,f,g)) return(f);
-    if (Cudd_bddLeq(manager,g,f)) return(g);
-    if (direction == 1) {
-        if (Cudd_bddLeq(manager,f,Cudd_Not(g)) ||
-        Cudd_bddLeq(manager,g,Cudd_Not(f))) return(zero);
-    }
-    return(Cudd_NotCond(one,(direction == 0)));
+        /* One last attempt at returning the right result. We sort of
+        ** cheat by calling Cudd_bddLeq. */
+        if (Cudd_bddLeq(manager,f,g)) return(f);
+        if (Cudd_bddLeq(manager,g,f)) return(g);
+        if (direction == 1) {
+            if (Cudd_bddLeq(manager,f,Cudd_Not(g)) ||
+                Cudd_bddLeq(manager,g,Cudd_Not(f))) return(zero);
+        }
+        return(Cudd_NotCond(one,(direction == 0)));
     }
 
     /* At this point f and g are not constant. */
@@ -276,16 +304,16 @@ cuddBddClippingAndRecur(
     /* Check cache. Try to increase cache efficiency by sorting the
     ** pointers. */
     if (f > g) {
-    DdNode *tmp = f;
-    f = g; g = tmp;
+        DdNode *tmp = f;
+        f = g; g = tmp;
     }
     F = Cudd_Regular(f);
     G = Cudd_Regular(g);
-    cacheOp = (DdNode *(*)(DdManager *, DdNode *, DdNode *))
-    (direction ? Cudd_bddClippingAnd : cuddBddClippingAnd);
+    cacheOp = (DD_CTFP)
+        (direction ? Cudd_bddClippingAnd : cuddBddClippingAnd);
     if (F->ref != 1 || G->ref != 1) {
-    r = cuddCacheLookup2(manager, cacheOp, f, g);
-    if (r != NULL) return(r);
+        r = cuddCacheLookup2(manager, cacheOp, f, g);
+        if (r != NULL) return(r);
     }
 
     /* Here we can skip the use of cuddI, because the operands are known
@@ -296,27 +324,27 @@ cuddBddClippingAndRecur(
 
     /* Compute cofactors. */
     if (topf <= topg) {
-    index = F->index;
-    ft = cuddT(F);
-    fe = cuddE(F);
-    if (Cudd_IsComplement(f)) {
-        ft = Cudd_Not(ft);
-        fe = Cudd_Not(fe);
-    }
+        index = F->index;
+        ft = cuddT(F);
+        fe = cuddE(F);
+        if (Cudd_IsComplement(f)) {
+            ft = Cudd_Not(ft);
+            fe = Cudd_Not(fe);
+        }
     } else {
-    index = G->index;
-    ft = fe = f;
+        index = G->index;
+        ft = fe = f;
     }
 
     if (topg <= topf) {
-    gt = cuddT(G);
-    ge = cuddE(G);
-    if (Cudd_IsComplement(g)) {
-        gt = Cudd_Not(gt);
-        ge = Cudd_Not(ge);
-    }
+        gt = cuddT(G);
+        ge = cuddE(G);
+        if (Cudd_IsComplement(g)) {
+            gt = Cudd_Not(gt);
+            ge = Cudd_Not(ge);
+        }
     } else {
-    gt = ge = g;
+        gt = ge = g;
     }
 
     t = cuddBddClippingAndRecur(manager, ft, gt, distance, direction);
@@ -324,35 +352,35 @@ cuddBddClippingAndRecur(
     cuddRef(t);
     e = cuddBddClippingAndRecur(manager, fe, ge, distance, direction);
     if (e == NULL) {
-    Cudd_RecursiveDeref(manager, t);
-    return(NULL);
+        Cudd_RecursiveDeref(manager, t);
+        return(NULL);
     }
     cuddRef(e);
 
     if (t == e) {
-    r = t;
+        r = t;
     } else {
-    if (Cudd_IsComplement(t)) {
-        r = cuddUniqueInter(manager,(int)index,Cudd_Not(t),Cudd_Not(e));
-        if (r == NULL) {
-        Cudd_RecursiveDeref(manager, t);
-        Cudd_RecursiveDeref(manager, e);
-        return(NULL);
-        }
-        r = Cudd_Not(r);
-    } else {
-        r = cuddUniqueInter(manager,(int)index,t,e);
-        if (r == NULL) {
-        Cudd_RecursiveDeref(manager, t);
-        Cudd_RecursiveDeref(manager, e);
-        return(NULL);
+        if (Cudd_IsComplement(t)) {
+            r = cuddUniqueInter(manager,(int)index,Cudd_Not(t),Cudd_Not(e));
+            if (r == NULL) {
+                Cudd_RecursiveDeref(manager, t);
+                Cudd_RecursiveDeref(manager, e);
+                return(NULL);
+            }
+            r = Cudd_Not(r);
+        } else {
+            r = cuddUniqueInter(manager,(int)index,t,e);
+            if (r == NULL) {
+                Cudd_RecursiveDeref(manager, t);
+                Cudd_RecursiveDeref(manager, e);
+                return(NULL);
+            }
         }
     }
-    }
     cuddDeref(e);
     cuddDeref(t);
     if (F->ref != 1 || G->ref != 1)
-    cuddCacheInsert2(manager, cacheOp, f, g, r);
+        cuddCacheInsert2(manager, cacheOp, f, g, r);
     return(r);
 
 } /* end of cuddBddClippingAndRecur */
@@ -393,15 +421,15 @@ cuddBddClipAndAbsRecur(
 
     /* Terminal cases. */
     if (f == zero || g == zero || f == Cudd_Not(g)) return(zero);
-    if (f == one && g == one)    return(one);
+    if (f == one && g == one)   return(one);
     if (cube == one) {
-    return(cuddBddClippingAndRecur(manager, f, g, distance, direction));
+        return(cuddBddClippingAndRecur(manager, f, g, distance, direction));
     }
     if (f == one || f == g) {
-    return (cuddBddExistAbstractRecur(manager, g, cube));
+        return (cuddBddExistAbstractRecur(manager, g, cube));
     }
     if (g == one) {
-    return (cuddBddExistAbstractRecur(manager, f, cube));
+        return (cuddBddExistAbstractRecur(manager, f, cube));
     }
     if (distance == 0) return(Cudd_NotCond(one,(direction == 0)));
 
@@ -410,19 +438,19 @@ cuddBddClipAndAbsRecur(
 
     /* Check cache. */
     if (f > g) { /* Try to increase cache efficiency. */
-    DdNode *tmp = f;
-    f = g; g = tmp;
+        DdNode *tmp = f;
+        f = g; g = tmp;
     }
     F = Cudd_Regular(f);
     G = Cudd_Regular(g);
     cacheTag = direction ? DD_BDD_CLIPPING_AND_ABSTRACT_UP_TAG :
-    DD_BDD_CLIPPING_AND_ABSTRACT_DOWN_TAG;
+        DD_BDD_CLIPPING_AND_ABSTRACT_DOWN_TAG;
     if (F->ref != 1 || G->ref != 1) {
-    r = cuddCacheLookup(manager, cacheTag,
-                f, g, cube);
-    if (r != NULL) {
-        return(r);
-    }
+        r = cuddCacheLookup(manager, cacheTag,
+                            f, g, cube);
+        if (r != NULL) {
+            return(r);
+        }
     }
 
     /* Here we can skip the use of cuddI, because the operands are known
@@ -434,39 +462,39 @@ cuddBddClipAndAbsRecur(
     topcube = manager->perm[cube->index];
 
     if (topcube < top) {
-    return(cuddBddClipAndAbsRecur(manager, f, g, cuddT(cube),
-                      distance, direction));
+        return(cuddBddClipAndAbsRecur(manager, f, g, cuddT(cube),
+                                      distance, direction));
     }
     /* Now, topcube >= top. */
 
     if (topf == top) {
-    index = F->index;
-    ft = cuddT(F);
-    fe = cuddE(F);
-    if (Cudd_IsComplement(f)) {
-        ft = Cudd_Not(ft);
-        fe = Cudd_Not(fe);
-    }
+        index = F->index;
+        ft = cuddT(F);
+        fe = cuddE(F);
+        if (Cudd_IsComplement(f)) {
+            ft = Cudd_Not(ft);
+            fe = Cudd_Not(fe);
+        }
     } else {
-    index = G->index;
-    ft = fe = f;
+        index = G->index;
+        ft = fe = f;
     }
 
     if (topg == top) {
-    gt = cuddT(G);
-    ge = cuddE(G);
-    if (Cudd_IsComplement(g)) {
-        gt = Cudd_Not(gt);
-        ge = Cudd_Not(ge);
-    }
+        gt = cuddT(G);
+        ge = cuddE(G);
+        if (Cudd_IsComplement(g)) {
+            gt = Cudd_Not(gt);
+            ge = Cudd_Not(ge);
+        }
     } else {
-    gt = ge = g;
+        gt = ge = g;
     }
 
     if (topcube == top) {
-    Cube = cuddT(cube);
+        Cube = cuddT(cube);
     } else {
-    Cube = cube;
+        Cube = cube;
     }
 
     t = cuddBddClipAndAbsRecur(manager, ft, gt, Cube, distance, direction);
@@ -476,61 +504,63 @@ cuddBddClipAndAbsRecur(
     ** the else branch if t is 1.
     */
     if (t == one && topcube == top) {
-    if (F->ref != 1 || G->ref != 1)
-        cuddCacheInsert(manager, cacheTag, f, g, cube, one);
-    return(one);
+        if (F->ref != 1 || G->ref != 1)
+            cuddCacheInsert(manager, cacheTag, f, g, cube, one);
+        return(one);
     }
     cuddRef(t);
 
     e = cuddBddClipAndAbsRecur(manager, fe, ge, Cube, distance, direction);
     if (e == NULL) {
-    Cudd_RecursiveDeref(manager, t);
-    return(NULL);
-    }
-    cuddRef(e);
-
-    if (topcube == top) {    /* abstract */
-    r = cuddBddClippingAndRecur(manager, Cudd_Not(t), Cudd_Not(e),
-                    distance, (direction == 0));
-    if (r == NULL) {
         Cudd_RecursiveDeref(manager, t);
-        Cudd_RecursiveDeref(manager, e);
         return(NULL);
     }
-    r = Cudd_Not(r);
-    cuddRef(r);
-    Cudd_RecursiveDeref(manager, t);
-    Cudd_RecursiveDeref(manager, e);
-    cuddDeref(r);
-    } else if (t == e) {
-    r = t;
-    cuddDeref(t);
-    cuddDeref(e);
-    } else {
-    if (Cudd_IsComplement(t)) {
-        r = cuddUniqueInter(manager,(int)index,Cudd_Not(t),Cudd_Not(e));
+    cuddRef(e);
+
+    if (topcube == top) {       /* abstract */
+        r = cuddBddClippingAndRecur(manager, Cudd_Not(t), Cudd_Not(e),
+                                    distance, (direction == 0));
         if (r == NULL) {
-        Cudd_RecursiveDeref(manager, t);
-        Cudd_RecursiveDeref(manager, e);
-        return(NULL);
+            Cudd_RecursiveDeref(manager, t);
+            Cudd_RecursiveDeref(manager, e);
+            return(NULL);
         }
         r = Cudd_Not(r);
-    } else {
-        r = cuddUniqueInter(manager,(int)index,t,e);
-        if (r == NULL) {
+        cuddRef(r);
         Cudd_RecursiveDeref(manager, t);
         Cudd_RecursiveDeref(manager, e);
-        return(NULL);
+        cuddDeref(r);
+    } else if (t == e) {
+        r = t;
+        cuddDeref(t);
+        cuddDeref(e);
+    } else {
+        if (Cudd_IsComplement(t)) {
+            r = cuddUniqueInter(manager,(int)index,Cudd_Not(t),Cudd_Not(e));
+            if (r == NULL) {
+                Cudd_RecursiveDeref(manager, t);
+                Cudd_RecursiveDeref(manager, e);
+                return(NULL);
+            }
+            r = Cudd_Not(r);
+        } else {
+            r = cuddUniqueInter(manager,(int)index,t,e);
+            if (r == NULL) {
+                Cudd_RecursiveDeref(manager, t);
+                Cudd_RecursiveDeref(manager, e);
+                return(NULL);
+            }
         }
-    }
-    cuddDeref(e);
-    cuddDeref(t);
+        cuddDeref(e);
+        cuddDeref(t);
     }
     if (F->ref != 1 || G->ref != 1)
-    cuddCacheInsert(manager, cacheTag, f, g, cube, r);
+        cuddCacheInsert(manager, cacheTag, f, g, cube, r);
     return (r);
 
 } /* end of cuddBddClipAndAbsRecur */
 
+
 ABC_NAMESPACE_IMPL_END
 
+