Upgrade to the latest CUDD 2.4.2.

1.txt

+M src\bdd\cudd\cudd.h
+M src\bdd\cudd\cuddAPI.c
+M src\bdd\cudd\cuddAddAbs.c
+M src\bdd\cudd\cuddAddApply.c
+M src\bdd\cudd\cuddAddFind.c
+M src\bdd\cudd\cuddAddInv.c
+M src\bdd\cudd\cuddAddIte.c
+M src\bdd\cudd\cuddAddNeg.c
+M src\bdd\cudd\cuddAddWalsh.c
+M src\bdd\cudd\cuddAndAbs.c
+M src\bdd\cudd\cuddAnneal.c
+M src\bdd\cudd\cuddApa.c
+M src\bdd\cudd\cuddApprox.c
+M src\bdd\cudd\cuddBddAbs.c
+M src\bdd\cudd\cuddBddCorr.c
+M src\bdd\cudd\cuddBddIte.c
+M src\bdd\cudd\cuddBridge.c
+M src\bdd\cudd\cuddCache.c
+M src\bdd\cudd\cuddCheck.c
+M src\bdd\cudd\cuddClip.c
+M src\bdd\cudd\cuddCof.c
+M src\bdd\cudd\cuddCompose.c
+M src\bdd\cudd\cuddDecomp.c
+M src\bdd\cudd\cuddEssent.c
+M src\bdd\cudd\cuddExact.c
+M src\bdd\cudd\cuddExport.c
+M src\bdd\cudd\cuddGenCof.c
+M src\bdd\cudd\cuddGenetic.c
+M src\bdd\cudd\cuddGroup.c
+M src\bdd\cudd\cuddHarwell.c
+M src\bdd\cudd\cuddInit.c
+M src\bdd\cudd\cuddInt.h
+M src\bdd\cudd\cuddInteract.c
+M src\bdd\cudd\cuddLCache.c
+M src\bdd\cudd\cuddLevelQ.c
+M src\bdd\cudd\cuddLinear.c
+M src\bdd\cudd\cuddLiteral.c
+M src\bdd\cudd\cuddMatMult.c
+M src\bdd\cudd\cuddPriority.c
+M src\bdd\cudd\cuddRead.c
+M src\bdd\cudd\cuddRef.c
+M src\bdd\cudd\cuddReorder.c
+M src\bdd\cudd\cuddSat.c
+M src\bdd\cudd\cuddSign.c
+M src\bdd\cudd\cuddSolve.c
+M src\bdd\cudd\cuddSplit.c
+M src\bdd\cudd\cuddSubsetHB.c
+M src\bdd\cudd\cuddSubsetSP.c
+M src\bdd\cudd\cuddSymmetry.c
+M src\bdd\cudd\cuddTable.c
+M src\bdd\cudd\cuddUtil.c
+M src\bdd\cudd\cuddWindow.c
+M src\bdd\cudd\cuddZddCount.c
+M src\bdd\cudd\cuddZddFuncs.c
+M src\bdd\cudd\cuddZddGroup.c
+M src\bdd\cudd\cuddZddIsop.c
+M src\bdd\cudd\cuddZddLin.c
+M src\bdd\cudd\cuddZddMisc.c
+M src\bdd\cudd\cuddZddPort.c
+M src\bdd\cudd\cuddZddReord.c
+M src\bdd\cudd\cuddZddSetop.c
+M src\bdd\cudd\cuddZddSymm.c
+M src\bdd\cudd\cuddZddUtil.c
+M src\bdd\cudd\r7x8.1.mat
+M src\bdd\cudd\testcudd.c
+? 1.txt
+? src\bdd\cudd\Makefile
+? src\bdd\cudd\r7x8.1.out

src/bdd/cudd/Makefile

+# $Id$
+#
+#    Cudd - DD package
+#---------------------------
+.SUFFIXES: .o .c .u
+
+CC	= gcc
+RANLIB	= ranlib
+PURE	=
+# Define EXE as .exe for MS-DOS and derivatives.
+EXE	=
+#EXE	= .exe
+
+MFLAG	=
+ICFLAGS	= -g
+XCFLAGS	= -DDD_STATS
+CFLAGS	= $(ICFLAGS) $(MFLAG) $(XCFLAGS)
+#DDDEBUG	= -DDD_DEBUG -DDD_CACHE_PROFILE -DDD_VERBOSE -DDD_UNIQUE_PROFILE
+DDDEBUG	=
+
+LINTFLAGS = -u -n -DDD_STATS -DDD_CACHE_PROFILE -DDD_VERBOSE -DDD_DEBUG -DDD_UNIQUE_PROFILE
+
+# this is to create the lint library
+LINTSWITCH = -o
+
+WHERE	= ..
+
+INCLUDE = $(WHERE)/include
+
+LIBS	= ./libcudd.a $(WHERE)/mtr/libmtr.a \
+	$(WHERE)/st/libst.a $(WHERE)/util/libutil.a $(WHERE)/epd/libepd.a
+
+MNEMLIB =
+
+BLIBS	= -kL. -klcudd -kL$(WHERE)/mtr -klmtr \
+	-kL$(WHERE)/st -klst -kL$(WHERE)/util -klutil -kL$(WHERE)/epd -klepd
+
+LINTLIBS = ./llib-lcudd.ln $(WHERE)/mtr/llib-lmtr.ln \
+	$(WHERE)/st/llib-lst.ln $(WHERE)/util/llib-lutil.ln \
+	$(WHERE)/epd/llib-lepd.ln
+
+LDFLAGS	=
+
+# files for the package
+P	= cudd
+PSRC	= cuddAPI.c cuddAddAbs.c cuddAddApply.c cuddAddFind.c cuddAddIte.c \
+	  cuddAddInv.c cuddAddNeg.c cuddAddWalsh.c cuddAndAbs.c \
+	  cuddAnneal.c cuddApa.c cuddApprox.c cuddBddAbs.c cuddBddCorr.c \
+	  cuddBddIte.c cuddBridge.c cuddCache.c cuddCheck.c cuddClip.c \
+	  cuddCof.c cuddCompose.c cuddDecomp.c cuddEssent.c \
+	  cuddExact.c cuddExport.c cuddGenCof.c cuddGenetic.c \
+	  cuddGroup.c cuddHarwell.c cuddInit.c cuddInteract.c \
+	  cuddLCache.c cuddLevelQ.c \
+	  cuddLinear.c cuddLiteral.c cuddMatMult.c cuddPriority.c \
+	  cuddRead.c cuddRef.c cuddReorder.c cuddSat.c cuddSign.c \
+	  cuddSolve.c cuddSplit.c cuddSubsetHB.c cuddSubsetSP.c cuddSymmetry.c \
+	  cuddTable.c cuddUtil.c cuddWindow.c cuddZddCount.c cuddZddFuncs.c \
+	  cuddZddGroup.c cuddZddIsop.c cuddZddLin.c cuddZddMisc.c \
+	  cuddZddPort.c cuddZddReord.c cuddZddSetop.c cuddZddSymm.c \
+	  cuddZddUtil.c
+PHDR    = cudd.h cuddInt.h
+POBJ	= $(PSRC:.c=.o)
+PUBJ	= $(PSRC:.c=.u)
+TARGET	= test$(P)$(EXE)
+TARGETu = test$(P)-u
+
+# files for the test program
+SRC	= test$(P).c
+OBJ	= $(SRC:.c=.o)
+UBJ	= $(SRC:.c=.u)
+
+#------------------------------------------------------
+
+lib$(P).a: $(POBJ)
+	ar rv $@ $?
+	$(RANLIB) $@
+
+.c.o: $(PSRC) $(PHDR)
+	$(CC) -c  $< -I$(INCLUDE) $(CFLAGS) $(DDDEBUG) 
+
+optimize_dec: lib$(P).b
+
+lib$(P).b: $(PUBJ)
+	ar rv $@ $?
+	$(RANLIB) $@
+
+.c.u: $(PSRC) $(PHDR)
+	cc -j $< -I$(INCLUDE) $(XCFLAGS)
+
+# if the header files change, recompile
+$(POBJ): $(PHDR)
+$(PUBJ): $(PHDR)
+$(OBJ): $(PHDR)
+$(UBJ): $(PHDR)
+
+$(TARGET): $(SRC) $(OBJ) $(HDR) $(LIBS) $(MNEMLIB)
+	$(PURE) $(CC) $(CFLAGS) $(LDFLAGS) -o $@ $(OBJ) $(LIBS) $(MNEMLIB) -lm
+
+# optimize (DECstations and Alphas only: uses u-code)
+$(TARGETu): $(SRC) $(UBJ) $(HDR) $(LIBS:.a=.b)
+	$(CC) -O3 -Olimit 1000 $(XCFLAGS) $(LDFLAGS) -o $@ $(UBJ) $(BLIBS) -lm
+
+lint: llib-l$(P).ln
+
+llib-l$(P).ln: $(PSRC) $(PHDR)
+	lint $(LINTFLAGS) $(LINTSWITCH)$(P) -I$(INCLUDE) $(PSRC)
+
+lintpgm: lint
+	lint $(LINTFLAGS) -I$(INCLUDE) $(SRC) $(LINTLIBS)
+
+tags: $(PSRC) $(PHDR)
+	ctags $(PSRC) $(PHDR)
+
+all: lib$(P).a lib$(P).b llib-l$(P).ln tags
+
+programs: $(TARGET) $(TARGETu) lintpgm
+
+clean:
+	rm -f *.o *.u mon.out gmon.out *.pixie *.Addrs *.Counts mnem.* \
+	.pure core *.warnings
+
+distclean: clean
+	rm -f $(TARGET) $(TARGETu) lib*.a lib$(P).b llib-l$(P).ln \
+	*.bak *~ tags .gdb_history *.qv *.qx

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
 
+

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
 
+

src/bdd/cudd/cuddAddNeg.c

@@ -4,35 +4,63 @@
 
   PackageName [cudd]
 
-  Synopsis    [function to compute the negation of an ADD.]
+  Synopsis    [Function to compute the negation of an ADD.]
 
   Description [External procedures included in this module:
-        <ul>
-        <li> Cudd_addNegate()
-        <li> Cudd_addRoundOff()
-        </ul>
-    Internal procedures included in this module:
-        <ul>
-        <li> cuddAddNegateRecur()
-        <li> cuddAddRoundOffRecur()
-        </ul> ]
+                <ul>
+                <li> Cudd_addNegate()
+                <li> Cudd_addRoundOff()
+                </ul>
+        Internal procedures included in this module:
+                <ul>
+                <li> cuddAddNegateRecur()
+                <li> cuddAddRoundOffRecur()
+                </ul> ]
 
   Author      [Fabio Somenzi, Balakrishna Kumthekar]
 
-  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 "util_hack.h"
 #include "cuddInt.h"
 
 ABC_NAMESPACE_IMPL_START
 
 
 
+
 /*---------------------------------------------------------------------------*/
 /* Constant declarations                                                     */
 /*---------------------------------------------------------------------------*/
@@ -53,7 +81,7 @@ ABC_NAMESPACE_IMPL_START
 /*---------------------------------------------------------------------------*/
 
 #ifndef lint
-static char rcsid[] DD_UNUSED = "$Id: cuddAddNeg.c,v 1.1.1.1 2003/02/24 22:23:50 wjiang Exp $";
+static char rcsid[] DD_UNUSED = "$Id: cuddAddNeg.c,v 1.12 2009/02/20 02:14:58 fabio Exp $";
 #endif
 
 
@@ -96,7 +124,7 @@ Cudd_addNegate(
     DdNode *res;
 
     do {
-    res = cuddAddNegateRecur(dd,f);
+        res = cuddAddNegateRecur(dd,f);
     } while (dd->reordered == 1);
     return(res);
 
@@ -126,7 +154,7 @@ Cudd_addRoundOff(
     double trunc = pow(10.0,(double)N);
 
     do {
-    res = cuddAddRoundOffRecur(dd,f,trunc);
+        res = cuddAddRoundOffRecur(dd,f,trunc);
     } while (dd->reordered == 1);
     return(res);
 
@@ -154,14 +182,14 @@ cuddAddNegateRecur(
   DdNode * f)
 {
     DdNode *res,
-        *fv, *fvn,
-        *T, *E;
+            *fv, *fvn,
+            *T, *E;
 
     statLine(dd);
     /* Check terminal cases. */
     if (cuddIsConstant(f)) {
-    res = cuddUniqueConst(dd,-cuddV(f));
-    return(res);
+        res = cuddUniqueConst(dd,-cuddV(f));
+        return(res);
     }
 
     /* Check cache */
@@ -177,15 +205,15 @@ cuddAddNegateRecur(
 
     E = cuddAddNegateRecur(dd,fvn);
     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);
@@ -217,15 +245,15 @@ cuddAddRoundOffRecur(
 
     DdNode *res, *fv, *fvn, *T, *E;
     double n;
-    DdNode *(*cacheOp)(DdManager *, DdNode *);
-  
+    DD_CTFP1 cacheOp;
+
     statLine(dd);
     if (cuddIsConstant(f)) {
         n = ceil(cuddV(f)*trunc)/trunc;
-    res = cuddUniqueConst(dd,n);
-    return(res);
+        res = cuddUniqueConst(dd,n);
+        return(res);
     }
-    cacheOp = (DdNode *(*)(DdManager *, DdNode *)) Cudd_addRoundOff;
+    cacheOp = (DD_CTFP1) Cudd_addRoundOff;
     res = cuddCacheLookup1(dd,cacheOp,f);
     if (res != NULL) {
         return(res);
@@ -241,14 +269,14 @@ cuddAddRoundOffRecur(
     E = cuddAddRoundOffRecur(dd,fvn,trunc);
     if (E == NULL) {
         Cudd_RecursiveDeref(dd,T);
-    return(NULL);
+        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,E);
+        return(NULL);
     }
     cuddDeref(T);
     cuddDeref(E);
@@ -256,12 +284,13 @@ cuddAddRoundOffRecur(
     /* Store result. */
     cuddCacheInsert1(dd,cacheOp,f,res);
     return(res);
-  
+
 } /* end of cuddAddRoundOffRecur */
 
 /*---------------------------------------------------------------------------*/
 /* Definition of static functions                                            */
 /*---------------------------------------------------------------------------*/
 
+
 ABC_NAMESPACE_IMPL_END
 

src/bdd/cudd/cuddCof.c

@@ -7,34 +7,62 @@
   Synopsis    [Cofactoring functions.]
 
   Description [External procedures included in this module:
-        <ul>
-        <li> Cudd_Cofactor()
-        </ul>
-           Internal procedures included in this module:
-        <ul>
-        <li> cuddGetBranches()
-        <li> cuddCheckCube()
-        <li> cuddCofactorRecur()
-        </ul>
-          ]
+                <ul>
+                <li> Cudd_Cofactor()
+                </ul>
+               Internal procedures included in this module:
+                <ul>
+                <li> cuddGetBranches()
+                <li> cuddCheckCube()
+                <li> cuddCofactorRecur()
+                </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.]
 
 ******************************************************************************/
 
-#include    "util_hack.h"
-#include    "cuddInt.h"
+#include "util_hack.h"
+#include "cuddInt.h"
 
 ABC_NAMESPACE_IMPL_START
 
 
+
 /*---------------------------------------------------------------------------*/
 /* Constant declarations                                                     */
 /*---------------------------------------------------------------------------*/
@@ -55,7 +83,7 @@ ABC_NAMESPACE_IMPL_START
 /*---------------------------------------------------------------------------*/
 
 #ifndef lint
-static char rcsid[] DD_UNUSED = "$Id: cuddCof.c,v 1.1.1.1 2003/02/24 22:23:51 wjiang Exp $";
+static char rcsid[] DD_UNUSED = "$Id: cuddCof.c,v 1.9 2004/08/13 18:04:47 fabio Exp $";
 #endif
 
 /*---------------------------------------------------------------------------*/
@@ -101,13 +129,13 @@ Cudd_Cofactor(
 
     zero = Cudd_Not(DD_ONE(dd));
     if (g == zero || g == DD_ZERO(dd)) {
-    (void) fprintf(dd->err,"Cudd_Cofactor: Invalid restriction 1\n");
-    dd->errorCode = CUDD_INVALID_ARG;
-    return(NULL);
+        (void) fprintf(dd->err,"Cudd_Cofactor: Invalid restriction 1\n");
+        dd->errorCode = CUDD_INVALID_ARG;
+        return(NULL);
     }
     do {
-    dd->reordered = 0;
-    res = cuddCofactorRecur(dd,f,g);
+        dd->reordered = 0;
+        res = cuddCofactorRecur(dd,f,g);
     } while (dd->reordered == 1);
     return(res);
 
@@ -136,13 +164,13 @@ cuddGetBranches(
   DdNode ** g1,
   DdNode ** g0)
 {
-    DdNode    *G = Cudd_Regular(g);
+    DdNode      *G = Cudd_Regular(g);
 
     *g1 = cuddT(G);
     *g0 = cuddE(G);
     if (Cudd_IsComplement(g)) {
-    *g1 = Cudd_Not(*g1);
-    *g0 = Cudd_Not(*g0);
+        *g1 = Cudd_Not(*g1);
+        *g0 = Cudd_Not(*g0);
     }
 
 } /* end of cuddGetBranches */
@@ -224,7 +252,7 @@ cuddCofactorRecur(
     comple = f != F;
     r = cuddCacheLookup2(dd,Cudd_Cofactor,F,g);
     if (r != NULL) {
-    return(Cudd_NotCond(r,comple));
+        return(Cudd_NotCond(r,comple));
     }
 
     topf = dd->perm[F->index];
@@ -237,57 +265,57 @@ cuddCofactorRecur(
     ** remembers whether we have to complement the result or not.
     */
     if (topf <= topg) {
-    f1 = cuddT(F); f0 = cuddE(F);
+        f1 = cuddT(F); f0 = cuddE(F);
     } else {
-    f1 = f0 = F;
+        f1 = f0 = F;
     }
     if (topg <= topf) {
-    g1 = cuddT(G); g0 = cuddE(G);
-    if (g != G) { g1 = Cudd_Not(g1); g0 = Cudd_Not(g0); }
+        g1 = cuddT(G); g0 = cuddE(G);
+        if (g != G) { g1 = Cudd_Not(g1); g0 = Cudd_Not(g0); }
     } else {
-    g1 = g0 = g;
+        g1 = g0 = g;
     }
 
     zero = Cudd_Not(one);
     if (topf >= topg) {
-    if (g0 == zero || g0 == DD_ZERO(dd)) {
-        r = cuddCofactorRecur(dd, f1, g1);
-    } else if (g1 == zero || g1 == DD_ZERO(dd)) {
-        r = cuddCofactorRecur(dd, f0, g0);
-    } else {
-        (void) fprintf(dd->out,
-               "Cudd_Cofactor: Invalid restriction 2\n");
-        dd->errorCode = CUDD_INVALID_ARG;
-        return(NULL);
-    }
-    if (r == NULL) return(NULL);
+        if (g0 == zero || g0 == DD_ZERO(dd)) {
+            r = cuddCofactorRecur(dd, f1, g1);
+        } else if (g1 == zero || g1 == DD_ZERO(dd)) {
+            r = cuddCofactorRecur(dd, f0, g0);
+        } else {
+            (void) fprintf(dd->out,
+                           "Cudd_Cofactor: Invalid restriction 2\n");
+            dd->errorCode = CUDD_INVALID_ARG;
+            return(NULL);
+        }
+        if (r == NULL) return(NULL);
     } else /* if (topf < topg) */ {
-    t = cuddCofactorRecur(dd, f1, g);
-    if (t == NULL) return(NULL);
+        t = cuddCofactorRecur(dd, f1, g);
+        if (t == NULL) return(NULL);
         cuddRef(t);
         e = cuddCofactorRecur(dd, f0, g);
-    if (e == NULL) {
-        Cudd_RecursiveDeref(dd, t);
-        return(NULL);
-    }
-    cuddRef(e);
-
-    if (t == e) {
-        r = t;
-    } else if (Cudd_IsComplement(t)) {
-        r = cuddUniqueInter(dd,(int)F->index,Cudd_Not(t),Cudd_Not(e));
-        if (r != NULL)
-        r = Cudd_Not(r);
-    } else {
-        r = cuddUniqueInter(dd,(int)F->index,t,e);
-    }
-    if (r == NULL) {
-        Cudd_RecursiveDeref(dd ,e);
-        Cudd_RecursiveDeref(dd ,t);
-        return(NULL);
-    }
-    cuddDeref(t);
-    cuddDeref(e);
+        if (e == NULL) {
+            Cudd_RecursiveDeref(dd, t);
+            return(NULL);
+        }
+        cuddRef(e);
+
+        if (t == e) {
+            r = t;
+        } else if (Cudd_IsComplement(t)) {
+            r = cuddUniqueInter(dd,(int)F->index,Cudd_Not(t),Cudd_Not(e));
+            if (r != NULL)
+                r = Cudd_Not(r);
+        } else {
+            r = cuddUniqueInter(dd,(int)F->index,t,e);
+        }
+        if (r == NULL) {
+            Cudd_RecursiveDeref(dd ,e);
+            Cudd_RecursiveDeref(dd ,t);
+            return(NULL);
+        }
+        cuddDeref(t);
+        cuddDeref(e);
     }
 
     cuddCacheInsert2(dd,Cudd_Cofactor,F,g,r);
@@ -301,5 +329,7 @@ cuddCofactorRecur(
 /* Definition of static functions                                            */
 /*---------------------------------------------------------------------------*/
 
+
 ABC_NAMESPACE_IMPL_END
 
+

src/bdd/cudd/cuddInit.c

@@ -7,35 +7,61 @@
   Synopsis    [Functions to initialize and shut down the DD manager.]
 
   Description [External procedures included in this module:
-        <ul>
-        <li> Cudd_Init()
-        <li> Cudd_Quit()
-        </ul>
-           Internal procedures included in this module:
-        <ul>
-        <li> cuddZddInitUniv()
-        <li> cuddZddFreeUniv()
-        </ul>
-          ]
+                <ul>
+                <li> Cudd_Init()
+                <li> Cudd_Quit()
+                </ul>
+               Internal procedures included in this module:
+                <ul>
+                <li> cuddZddInitUniv()
+                <li> cuddZddFreeUniv()
+                </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.]
 
 ******************************************************************************/
 
-#include    "util_hack.h"
-#define CUDD_MAIN
-#include    "cuddInt.h"
+#include "util_hack.h"
+#include "cuddInt.h"
 
 ABC_NAMESPACE_IMPL_START
 
-#undef CUDD_MAIN
+
 
 /*---------------------------------------------------------------------------*/
 /* Constant declarations                                                     */
@@ -57,7 +83,7 @@ ABC_NAMESPACE_IMPL_START
 /*---------------------------------------------------------------------------*/
 
 #ifndef lint
-static char rcsid[] DD_UNUSED = "$Id: cuddInit.c,v 1.1.1.1 2003/02/24 22:23:52 wjiang Exp $";
+static char rcsid[] DD_UNUSED = "$Id: cuddInit.c,v 1.33 2007/07/01 05:10:50 fabio Exp $";
 #endif
 
 /*---------------------------------------------------------------------------*/
@@ -108,19 +134,19 @@ Cudd_Init(
     DdNode *one, *zero;
     unsigned int maxCacheSize;
     unsigned int looseUpTo;
-//    extern void (*MMoutOfMemory)(long);
-    void (*saveHandler)(long);
+    extern DD_OOMFP MMoutOfMemory;
+    DD_OOMFP saveHandler;
 
     if (maxMemory == 0) {
-    maxMemory = getSoftDataLimit();
+        maxMemory = getSoftDataLimit();
     }
     looseUpTo = (unsigned int) ((maxMemory / sizeof(DdNode)) /
-                DD_MAX_LOOSE_FRACTION);
+                                DD_MAX_LOOSE_FRACTION);
     unique = cuddInitTable(numVars,numVarsZ,numSlots,looseUpTo);
-    unique->maxmem = (unsigned) maxMemory / 10 * 9;
     if (unique == NULL) return(NULL);
+    unique->maxmem = (unsigned long) maxMemory / 10 * 9;
     maxCacheSize = (unsigned int) ((maxMemory / sizeof(DdCache)) /
-                   DD_MAX_CACHE_FRACTION);
+                                   DD_MAX_CACHE_FRACTION);
     result = cuddInitCache(unique,cacheSize,maxCacheSize);
     if (result == 0) return(NULL);
 
@@ -129,7 +155,7 @@ Cudd_Init(
     unique->stash = ABC_ALLOC(char,(maxMemory / DD_STASH_FRACTION) + 4);
     MMoutOfMemory = saveHandler;
     if (unique->stash == NULL) {
-    (void) fprintf(unique->err,"Unable to set aside memory\n");
+        (void) fprintf(unique->err,"Unable to set aside memory\n");
     }
 
     /* Initialize constants. */
@@ -141,9 +167,9 @@ Cudd_Init(
     cuddRef(unique->zero);
 #ifdef HAVE_IEEE_754
     if (DD_PLUS_INF_VAL != DD_PLUS_INF_VAL * 3 ||
-    DD_PLUS_INF_VAL != DD_PLUS_INF_VAL / 3) {
-    (void) fprintf(unique->err,"Warning: Crippled infinite values\n");
-    (void) fprintf(unique->err,"Recompile without -DHAVE_IEEE_754\n");
+        DD_PLUS_INF_VAL != DD_PLUS_INF_VAL / 3) {
+        (void) fprintf(unique->err,"Warning: Crippled infinite values\n");
+        (void) fprintf(unique->err,"Recompile without -DHAVE_IEEE_754\n");
     }
 #endif
     unique->plusinfinity = cuddUniqueConst(unique,DD_PLUS_INF_VAL);
@@ -160,17 +186,17 @@ Cudd_Init(
     /* Create the projection functions. */
     unique->vars = ABC_ALLOC(DdNodePtr,unique->maxSize);
     if (unique->vars == NULL) {
-    unique->errorCode = CUDD_MEMORY_OUT;
-    return(NULL);
+        unique->errorCode = CUDD_MEMORY_OUT;
+        return(NULL);
     }
     for (i = 0; i < unique->size; i++) {
-    unique->vars[i] = cuddUniqueInter(unique,i,one,zero);
-    if (unique->vars[i] == NULL) return(0);
-    cuddRef(unique->vars[i]);
+        unique->vars[i] = cuddUniqueInter(unique,i,one,zero);
+        if (unique->vars[i] == NULL) return(0);
+        cuddRef(unique->vars[i]);
     }
 
     if (unique->sizeZ)
-    cuddZddInitUniv(unique);
+        cuddZddInitUniv(unique);
 
     unique->memused += sizeof(DdNode *) * unique->maxSize;
 
@@ -226,29 +252,29 @@ int
 cuddZddInitUniv(
   DdManager * zdd)
 {
-    DdNode    *p, *res;
-    int        i;
+    DdNode      *p, *res;
+    int         i;
 
     zdd->univ = ABC_ALLOC(DdNodePtr, zdd->sizeZ);
     if (zdd->univ == NULL) {
-    zdd->errorCode = CUDD_MEMORY_OUT;
-    return(0);
+        zdd->errorCode = CUDD_MEMORY_OUT;
+        return(0);
     }
 
     res = DD_ONE(zdd);
     cuddRef(res);
     for (i = zdd->sizeZ - 1; i >= 0; i--) {
-    unsigned int index = zdd->invpermZ[i];
-    p = res;
-    res = cuddUniqueInterZdd(zdd, index, p, p);
-    if (res == NULL) {
-        Cudd_RecursiveDerefZdd(zdd,p);
-        ABC_FREE(zdd->univ);
-        return(0);
-    }
-    cuddRef(res);
-    cuddDeref(p);
-    zdd->univ[i] = res;
+        unsigned int index = zdd->invpermZ[i];
+        p = res;
+        res = cuddUniqueInterZdd(zdd, index, p, p);
+        if (res == NULL) {
+            Cudd_RecursiveDerefZdd(zdd,p);
+            ABC_FREE(zdd->univ);
+            return(0);
+        }
+        cuddRef(res);
+        cuddDeref(p);
+        zdd->univ[i] = res;
     }
 
 #ifdef DD_VERBOSE
@@ -276,8 +302,8 @@ cuddZddFreeUniv(
   DdManager * zdd)
 {
     if (zdd->univ) {
-    Cudd_RecursiveDerefZdd(zdd, zdd->univ[0]);
-    ABC_FREE(zdd->univ);
+        Cudd_RecursiveDerefZdd(zdd, zdd->univ[0]);
+        ABC_FREE(zdd->univ);
     }
 
 } /* end of cuddZddFreeUniv */
@@ -287,5 +313,7 @@ cuddZddFreeUniv(
 /* Definition of static functions                                            */
 /*---------------------------------------------------------------------------*/
 
+
 ABC_NAMESPACE_IMPL_END
 
+

src/bdd/cudd/cuddInteract.c

@@ -7,18 +7,18 @@
   Synopsis    [Functions to manipulate the variable interaction matrix.]
 
   Description [Internal procedures included in this file:
-    <ul>
-    <li> cuddSetInteract()
-    <li> cuddTestInteract()
-    <li> cuddInitInteract()
-    </ul>
+        <ul>
+        <li> cuddSetInteract()
+        <li> cuddTestInteract()
+        <li> cuddInitInteract()
+        </ul>
   Static procedures included in this file:
-    <ul>
-    <li> ddSuppInteract()
-    <li> ddClearLocal()
-    <li> ddUpdateInteract()
-    <li> ddClearGlobal()
-    </ul>
+        <ul>
+        <li> ddSuppInteract()
+        <li> ddClearLocal()
+        <li> ddUpdateInteract()
+        <li> ddClearGlobal()
+        </ul>
   The interaction matrix tells whether two variables are
   both in the support of some function of the DD. The main use of the
   interaction matrix is in the in-place swapping. Indeed, if two
@@ -40,10 +40,37 @@
 
   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.]
 
 ******************************************************************************/
 
@@ -53,6 +80,7 @@
 ABC_NAMESPACE_IMPL_START
 
 
+
 /*---------------------------------------------------------------------------*/
 /* Constant declarations                                                     */
 /*---------------------------------------------------------------------------*/
@@ -80,7 +108,7 @@ ABC_NAMESPACE_IMPL_START
 /*---------------------------------------------------------------------------*/
 
 #ifndef lint
-static char rcsid[] DD_UNUSED = "$Id: cuddInteract.c,v 1.1.1.1 2003/02/24 22:23:52 wjiang Exp $";
+static char rcsid[] DD_UNUSED = "$Id: cuddInteract.c,v 1.12 2004/08/13 18:04:49 fabio Exp $";
 #endif
 
 /*---------------------------------------------------------------------------*/
@@ -94,10 +122,10 @@ static char rcsid[] DD_UNUSED = "$Id: cuddInteract.c,v 1.1.1.1 2003/02/24 22:23:
 /* Static function prototypes                                                */
 /*---------------------------------------------------------------------------*/
 
-static void ddSuppInteract ARGS((DdNode *f, int *support));
-static void ddClearLocal ARGS((DdNode *f));
-static void ddUpdateInteract ARGS((DdManager *table, int *support));
-static void ddClearGlobal ARGS((DdManager *table));
+static void ddSuppInteract (DdNode *f, int *support);
+static void ddClearLocal (DdNode *f);
+static void ddUpdateInteract (DdManager *table, int *support);
+static void ddClearGlobal (DdManager *table);
 
 /**AutomaticEnd***************************************************************/
 
@@ -168,9 +196,9 @@ cuddTestInteract(
     int posn, word, bit, result;
 
     if (x > y) {
-    int tmp = x;
-    x = y;
-    y = tmp;
+        int tmp = x;
+        x = y;
+        y = tmp;
     }
 #ifdef DD_DEBUG
     assert(x < y);
@@ -222,43 +250,43 @@ cuddInitInteract(
     words = ((n * (n-1)) >> (1 + LOGBPL)) + 1;
     table->interact = interact = ABC_ALLOC(long,words);
     if (interact == NULL) {
-    table->errorCode = CUDD_MEMORY_OUT;
-    return(0);
+        table->errorCode = CUDD_MEMORY_OUT;
+        return(0);
     }
     for (i = 0; i < words; i++) {
-    interact[i] = 0;
+        interact[i] = 0;
     }
 
     support = ABC_ALLOC(int,n);
     if (support == NULL) {
-    table->errorCode = CUDD_MEMORY_OUT;
-    ABC_FREE(interact);
-    return(0);
+        table->errorCode = CUDD_MEMORY_OUT;
+        ABC_FREE(interact);
+        return(0);
     }
 
     for (i = 0; i < n; i++) {
-    nodelist = table->subtables[i].nodelist;
-    slots = table->subtables[i].slots;
-    for (j = 0; j < slots; j++) {
-        f = nodelist[j];
-        while (f != sentinel) {
-        /* A node is a root of the DAG if it cannot be
-        ** reached by nodes above it. If a node was never
-        ** reached during the previous depth-first searches,
-        ** then it is a root, and we start a new depth-first
-        ** search from it.
-        */
-        if (!Cudd_IsComplement(f->next)) {
-            for (k = 0; k < n; k++) {
-            support[k] = 0;
+        nodelist = table->subtables[i].nodelist;
+        slots = table->subtables[i].slots;
+        for (j = 0; j < slots; j++) {
+            f = nodelist[j];
+            while (f != sentinel) {
+                /* A node is a root of the DAG if it cannot be
+                ** reached by nodes above it. If a node was never
+                ** reached during the previous depth-first searches,
+                ** then it is a root, and we start a new depth-first
+                ** search from it.
+                */
+                if (!Cudd_IsComplement(f->next)) {
+                    for (k = 0; k < n; k++) {
+                        support[k] = 0;
+                    }
+                    ddSuppInteract(f,support);
+                    ddClearLocal(f);
+                    ddUpdateInteract(table,support);
+                }
+                f = Cudd_Regular(f->next);
             }
-            ddSuppInteract(f,support);
-            ddClearLocal(f);
-            ddUpdateInteract(table,support);
         }
-        f = Cudd_Regular(f->next);
-        }
-    }
     }
     ddClearGlobal(table);
 
@@ -291,7 +319,7 @@ ddSuppInteract(
   int * support)
 {
     if (cuddIsConstant(f) || Cudd_IsComplement(cuddT(f))) {
-    return;
+        return;
     }
 
     support[f->index] = 1;
@@ -321,7 +349,7 @@ ddClearLocal(
   DdNode * f)
 {
     if (cuddIsConstant(f) || !Cudd_IsComplement(cuddT(f))) {
-    return;
+        return;
     }
     /* clear visited flag */
     cuddT(f) = Cudd_Regular(cuddT(f));
@@ -354,14 +382,14 @@ ddUpdateInteract(
     int n = table->size;
 
     for (i = 0; i < n-1; i++) {
-    if (support[i] == 1) {
-        for (j = i+1; j < n; j++) {
-        if (support[j] == 1) {
-            cuddSetInteract(table,i,j);
-        }
+        if (support[i] == 1) {
+            for (j = i+1; j < n; j++) {
+                if (support[j] == 1) {
+                    cuddSetInteract(table,i,j);
+                }
+            }
         }
     }
-    }
 
 } /* end of ddUpdateInteract */
 
@@ -390,18 +418,20 @@ ddClearGlobal(
     int slots;
 
     for (i = 0; i < table->size; i++) {
-    nodelist = table->subtables[i].nodelist;
-    slots = table->subtables[i].slots;
-    for (j = 0; j < slots; j++) {
-        f = nodelist[j];
-        while (f != sentinel) {
-        f->next = Cudd_Regular(f->next);
-        f = f->next;
+        nodelist = table->subtables[i].nodelist;
+        slots = table->subtables[i].slots;
+        for (j = 0; j < slots; j++) {
+            f = nodelist[j];
+            while (f != sentinel) {
+                f->next = Cudd_Regular(f->next);
+                f = f->next;
+            }
         }
     }
-    }
 
 } /* end of ddClearGlobal */
 
+
 ABC_NAMESPACE_IMPL_END
 
+

src/bdd/cudd/cuddLiteral.c

@@ -8,20 +8,47 @@
   BDDs.]
 
   Description [External procedures included in this file:
-        <ul>
-        <li> Cudd_bddLiteralSetIntersection()
-        </ul>
-        Internal procedures included in this file:
-        <ul>
-        <li> cuddBddLiteralSetIntersectionRecur()
-        </ul>]
+                <ul>
+                <li> Cudd_bddLiteralSetIntersection()
+                </ul>
+            Internal procedures included in this file:
+                <ul>
+                <li> cuddBddLiteralSetIntersectionRecur()
+                </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.]
 
 ******************************************************************************/
 
@@ -32,6 +59,7 @@ ABC_NAMESPACE_IMPL_START
 
 
 
+
 /*---------------------------------------------------------------------------*/
 /* Constant declarations                                                     */
 /*---------------------------------------------------------------------------*/
@@ -49,7 +77,7 @@ ABC_NAMESPACE_IMPL_START
 /*---------------------------------------------------------------------------*/
 
 #ifndef lint
-static char rcsid[] DD_UNUSED = "$Id: cuddLiteral.c,v 1.1.1.1 2003/02/24 22:23:52 wjiang Exp $";
+static char rcsid[] DD_UNUSED = "$Id: cuddLiteral.c,v 1.8 2004/08/13 18:04:50 fabio Exp $";
 #endif
 
 /*---------------------------------------------------------------------------*/
@@ -95,8 +123,8 @@ Cudd_bddLiteralSetIntersection(
     DdNode *res;
 
     do {
-    dd->reordered = 0;
-    res = cuddBddLiteralSetIntersectionRecur(dd,f,g);
+        dd->reordered = 0;
+        res = cuddBddLiteralSetIntersectionRecur(dd,f,g);
     } while (dd->reordered == 1);
     return(res);
 
@@ -155,27 +183,27 @@ cuddBddLiteralSetIntersectionRecur(
     ** loop will stop when the constant node is reached in both cubes.
     */
     while (topf != topg) {
-    if (topf < topg) {    /* move down on f */
-        comple = f != F;
-        f = cuddT(F);
-        if (comple) f = Cudd_Not(f);
-        if (f == zero) {
-        f = cuddE(F);
-        if (comple) f = Cudd_Not(f);
-        }
-        F = Cudd_Regular(f);
-        topf = cuddI(dd,F->index);
-    } else if (topg < topf) {
-        comple = g != G;
-        g = cuddT(G);
-        if (comple) g = Cudd_Not(g);
-        if (g == zero) {
-        g = cuddE(G);
-        if (comple) g = Cudd_Not(g);
+        if (topf < topg) {      /* move down on f */
+            comple = f != F;
+            f = cuddT(F);
+            if (comple) f = Cudd_Not(f);
+            if (f == zero) {
+                f = cuddE(F);
+                if (comple) f = Cudd_Not(f);
+            }
+            F = Cudd_Regular(f);
+            topf = cuddI(dd,F->index);
+        } else if (topg < topf) {
+            comple = g != G;
+            g = cuddT(G);
+            if (comple) g = Cudd_Not(g);
+            if (g == zero) {
+                g = cuddE(G);
+                if (comple) g = Cudd_Not(g);
+            }
+            G = Cudd_Regular(g);
+            topg = cuddI(dd,G->index);
         }
-        G = Cudd_Regular(g);
-        topg = cuddI(dd,G->index);
-    }
     }
 
     /* At this point, f == one <=> g == 1. It suffices to test one of them. */
@@ -183,7 +211,7 @@ cuddBddLiteralSetIntersectionRecur(
 
     res = cuddCacheLookup2(dd,Cudd_bddLiteralSetIntersection,f,g);
     if (res != NULL) {
-    return(res);
+        return(res);
     }
 
     /* Here f and g are both non constant and have the same top variable. */
@@ -192,39 +220,39 @@ cuddBddLiteralSetIntersectionRecur(
     phasef = 1;
     if (comple) fc = Cudd_Not(fc);
     if (fc == zero) {
-    fc = cuddE(F);
-    phasef = 0;
-    if (comple) fc = Cudd_Not(fc);
+        fc = cuddE(F);
+        phasef = 0;
+        if (comple) fc = Cudd_Not(fc);
     }
     comple = g != G;
     gc = cuddT(G);
     phaseg = 1;
     if (comple) gc = Cudd_Not(gc);
     if (gc == zero) {
-    gc = cuddE(G);
-    phaseg = 0;
-    if (comple) gc = Cudd_Not(gc);
+        gc = cuddE(G);
+        phaseg = 0;
+        if (comple) gc = Cudd_Not(gc);
     }
 
     tmp = cuddBddLiteralSetIntersectionRecur(dd,fc,gc);
     if (tmp == NULL) {
-    return(NULL);
+        return(NULL);
     }
 
     if (phasef != phaseg) {
-    res = tmp;
-    } else {
-    cuddRef(tmp);
-    if (phasef == 0) {
-        res = cuddBddAndRecur(dd,Cudd_Not(dd->vars[F->index]),tmp);
+        res = tmp;
     } else {
-        res = cuddBddAndRecur(dd,dd->vars[F->index],tmp);
-    }
-    if (res == NULL) {
-        Cudd_RecursiveDeref(dd,tmp);
-        return(NULL);
-    }
-    cuddDeref(tmp); /* Just cuddDeref, because it is included in result */
+        cuddRef(tmp);
+        if (phasef == 0) {
+            res = cuddBddAndRecur(dd,Cudd_Not(dd->vars[F->index]),tmp);
+        } else {
+            res = cuddBddAndRecur(dd,dd->vars[F->index],tmp);
+        }
+        if (res == NULL) {
+            Cudd_RecursiveDeref(dd,tmp);
+            return(NULL);
+        }
+        cuddDeref(tmp); /* Just cuddDeref, because it is included in result */
     }
 
     cuddCacheInsert2(dd,Cudd_bddLiteralSetIntersection,f,g,res);
@@ -238,5 +266,7 @@ cuddBddLiteralSetIntersectionRecur(
 /* Definition of static functions                                            */
 /*---------------------------------------------------------------------------*/
 
+
 ABC_NAMESPACE_IMPL_END
 
+

src/bdd/cudd/cuddSolve.c

@@ -7,24 +7,51 @@
   Synopsis    [Boolean equation solver and related functions.]
 
   Description [External functions included in this modoule:
-        <ul>
-        <li> Cudd_SolveEqn()
-        <li> Cudd_VerifySol()
-        </ul>
-    Internal functions included in this module:
-        <ul>
-        <li> cuddSolveEqnRecur()
-        <li> cuddVerifySol()
-        </ul> ]
+                <ul>
+                <li> Cudd_SolveEqn()
+                <li> Cudd_VerifySol()
+                </ul>
+        Internal functions included in this module:
+                <ul>
+                <li> cuddSolveEqnRecur()
+                <li> cuddVerifySol()
+                </ul> ]
 
   SeeAlso     []
 
   Author      [Balakrishna Kumthekar]
 
-  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.]
 
 ******************************************************************************/
 
@@ -34,6 +61,7 @@
 ABC_NAMESPACE_IMPL_START
 
 
+
 /*---------------------------------------------------------------------------*/
 /* Constant declarations                                                     */
 /*---------------------------------------------------------------------------*/
@@ -54,7 +82,7 @@ ABC_NAMESPACE_IMPL_START
 /*---------------------------------------------------------------------------*/
 
 #ifndef lint
-static char rcsid[] DD_UNUSED = "$Id: cuddSolve.c,v 1.1.1.1 2003/02/24 22:23:53 wjiang Exp $";
+static char rcsid[] DD_UNUSED = "$Id: cuddSolve.c,v 1.12 2004/08/13 18:04:51 fabio Exp $";
 #endif
 
 /*---------------------------------------------------------------------------*/
@@ -108,15 +136,15 @@ Cudd_SolveEqn(
 
     *yIndex = temp = ABC_ALLOC(int, n);
     if (temp == NULL) {
-    bdd->errorCode = CUDD_MEMORY_OUT;
-    (void) fprintf(bdd->out,
-               "Cudd_SolveEqn: Out of memory for yIndex\n");
-    return(NULL);
+        bdd->errorCode = CUDD_MEMORY_OUT;
+        (void) fprintf(bdd->out,
+                       "Cudd_SolveEqn: Out of memory for yIndex\n");
+        return(NULL);
     }
 
     do {
-    bdd->reordered = 0;
-    res = cuddSolveEqnRecur(bdd, F, Y, G, n, temp, 0);
+        bdd->reordered = 0;
+        res = cuddSolveEqnRecur(bdd, F, Y, G, n, temp, 0);
     } while (bdd->reordered == 1);
 
     return(res);
@@ -148,8 +176,8 @@ Cudd_VerifySol(
     DdNode *res;
 
     do {
-    bdd->reordered = 0;
-    res = cuddVerifySol(bdd, F, G, yIndex, n);
+        bdd->reordered = 0;
+        res = cuddVerifySol(bdd, F, G, yIndex, n);
     } while (bdd->reordered == 1);
 
     ABC_FREE(yIndex);
@@ -199,7 +227,7 @@ cuddSolveEqnRecur(
 
     /* Base condition. */
     if (Y == one) {
-    return F;
+        return F;
     }
 
     /* Cofactor of Y. */
@@ -209,61 +237,61 @@ cuddSolveEqnRecur(
     /* Universal abstraction of F with respect to the top variable index. */
     Fm1 = cuddBddExistAbstractRecur(bdd, Cudd_Not(F), variables[yIndex[i]]);
     if (Fm1) {
-    Fm1 = Cudd_Not(Fm1);
-    cuddRef(Fm1);
+        Fm1 = Cudd_Not(Fm1);
+        cuddRef(Fm1);
     } else {
-    return(NULL);
+        return(NULL);
     }
 
     Fn = cuddSolveEqnRecur(bdd, Fm1, nextY, G, n, yIndex, i+1);
     if (Fn) {
-    cuddRef(Fn);
+        cuddRef(Fn);
     } else {
-    Cudd_RecursiveDeref(bdd, Fm1);
-    return(NULL);
+        Cudd_RecursiveDeref(bdd, Fm1);
+        return(NULL);
     }
 
     Fv = cuddCofactorRecur(bdd, F, variables[yIndex[i]]);
     if (Fv) {
-    cuddRef(Fv);
+        cuddRef(Fv);
     } else {
-    Cudd_RecursiveDeref(bdd, Fm1);
-    Cudd_RecursiveDeref(bdd, Fn);
-    return(NULL);
+        Cudd_RecursiveDeref(bdd, Fm1);
+        Cudd_RecursiveDeref(bdd, Fn);
+        return(NULL);
     }
 
     Fvbar = cuddCofactorRecur(bdd, F, Cudd_Not(variables[yIndex[i]]));
     if (Fvbar) {
-    cuddRef(Fvbar);
+        cuddRef(Fvbar);
     } else {
-    Cudd_RecursiveDeref(bdd, Fm1);
-    Cudd_RecursiveDeref(bdd, Fn);
-    Cudd_RecursiveDeref(bdd, Fv);
-    return(NULL);
+        Cudd_RecursiveDeref(bdd, Fm1);
+        Cudd_RecursiveDeref(bdd, Fn);
+        Cudd_RecursiveDeref(bdd, Fv);
+        return(NULL);
     }
 
     /* Build i-th component of the solution. */
     w = cuddBddIteRecur(bdd, variables[yIndex[i]], Cudd_Not(Fv), Fvbar);
     if (w) {
-    cuddRef(w);
+        cuddRef(w);
     } else {
-    Cudd_RecursiveDeref(bdd, Fm1);
-    Cudd_RecursiveDeref(bdd, Fn);
-    Cudd_RecursiveDeref(bdd, Fv);
-    Cudd_RecursiveDeref(bdd, Fvbar);
-    return(NULL);
+        Cudd_RecursiveDeref(bdd, Fm1);
+        Cudd_RecursiveDeref(bdd, Fn);
+        Cudd_RecursiveDeref(bdd, Fv);
+        Cudd_RecursiveDeref(bdd, Fvbar);
+        return(NULL);
     }
 
     T = cuddBddRestrictRecur(bdd, w, Cudd_Not(Fm1));
     if(T) {
-    cuddRef(T);
+        cuddRef(T);
     } else {
-    Cudd_RecursiveDeref(bdd, Fm1);
-    Cudd_RecursiveDeref(bdd, Fn);
-    Cudd_RecursiveDeref(bdd, Fv);
-    Cudd_RecursiveDeref(bdd, Fvbar);
-    Cudd_RecursiveDeref(bdd, w);
-    return(NULL);
+        Cudd_RecursiveDeref(bdd, Fm1);
+        Cudd_RecursiveDeref(bdd, Fn);
+        Cudd_RecursiveDeref(bdd, Fv);
+        Cudd_RecursiveDeref(bdd, Fvbar);
+        Cudd_RecursiveDeref(bdd, w);
+        return(NULL);
     }
 
     Cudd_RecursiveDeref(bdd,Fm1);
@@ -273,16 +301,16 @@ cuddSolveEqnRecur(
 
     /* Substitute components of solution already found into solution. */
     for (j = n-1; j > i; j--) {
-    w = cuddBddComposeRecur(bdd,T, G[j], variables[yIndex[j]]);
-    if(w) {
-        cuddRef(w);
-    } else {
-        Cudd_RecursiveDeref(bdd, Fn);
-        Cudd_RecursiveDeref(bdd, T);
-        return(NULL);
-    }
-    Cudd_RecursiveDeref(bdd,T);
-    T = w;
+        w = cuddBddComposeRecur(bdd,T, G[j], variables[yIndex[j]]);
+        if(w) {
+            cuddRef(w);
+        } else {
+            Cudd_RecursiveDeref(bdd, Fn);
+            Cudd_RecursiveDeref(bdd, T);
+            return(NULL);
+        }
+        Cudd_RecursiveDeref(bdd,T);
+        T = w;
     }
     G[i] = T;
 
@@ -319,14 +347,14 @@ cuddVerifySol(
     R = F;
     cuddRef(R);
     for(j = n - 1; j >= 0; j--) {
-     w = Cudd_bddCompose(bdd, R, G[j], yIndex[j]);
-    if (w) {
-        cuddRef(w);
-    } else {
-        return(NULL); 
-    }
-    Cudd_RecursiveDeref(bdd,R);
-    R = w;
+         w = Cudd_bddCompose(bdd, R, G[j], yIndex[j]);
+        if (w) {
+            cuddRef(w);
+        } else {
+            return(NULL); 
+        }
+        Cudd_RecursiveDeref(bdd,R);
+        R = w;
     }
 
     cuddDeref(R);
@@ -340,5 +368,7 @@ cuddVerifySol(
 /* Definition of static functions                                            */
 /*---------------------------------------------------------------------------*/
 
+
 ABC_NAMESPACE_IMPL_END
 
+

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
 

src/bdd/cudd/cuddZddMisc.c

@@ -4,41 +4,69 @@
 
   PackageName [cudd]
 
-  Synopsis    [.]
+  Synopsis    [Miscellaneous utility functions for ZDDs.]
 
   Description [External procedures included in this module:
-            <ul>
-            <li> Cudd_zddDagSize()
-            <li> Cudd_zddCountMinterm()
-            <li> Cudd_zddPrintSubtable()
-            </ul>
-           Internal procedures included in this module:
-            <ul>
-            </ul>
-           Static procedures included in this module:
-            <ul>
-            <li> cuddZddDagInt()
-            </ul>
-          ]
+                    <ul>
+                    <li> Cudd_zddDagSize()
+                    <li> Cudd_zddCountMinterm()
+                    <li> Cudd_zddPrintSubtable()
+                    </ul>
+               Internal procedures included in this module:
+                    <ul>
+                    </ul>
+               Static procedures included in this module:
+                    <ul>
+                    <li> cuddZddDagInt()
+                    </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    <math.h>
-#include    "util_hack.h"
-#include    "cuddInt.h"
+#include <math.h>
+#include "util_hack.h"
+#include "cuddInt.h"
 
 ABC_NAMESPACE_IMPL_START
 
 
+
 /*---------------------------------------------------------------------------*/
 /* Constant declarations                                                     */
 /*---------------------------------------------------------------------------*/
@@ -59,7 +87,7 @@ ABC_NAMESPACE_IMPL_START
 /*---------------------------------------------------------------------------*/
 
 #ifndef lint
-static char rcsid[] DD_UNUSED = "$Id: cuddZddMisc.c,v 1.1.1.1 2003/02/24 22:23:54 wjiang Exp $";
+static char rcsid[] DD_UNUSED = "$Id: cuddZddMisc.c,v 1.16 2009/02/20 02:14:58 fabio Exp $";
 #endif
 
 /*---------------------------------------------------------------------------*/
@@ -73,7 +101,7 @@ static char rcsid[] DD_UNUSED = "$Id: cuddZddMisc.c,v 1.1.1.1 2003/02/24 22:23:5
 /* Static function prototypes                                                */
 /*---------------------------------------------------------------------------*/
 
-static int cuddZddDagInt ARGS((DdNode *n, st_table *tab));
+static int cuddZddDagInt (DdNode *n, st_table *tab);
 
 /**AutomaticEnd***************************************************************/
 
@@ -100,7 +128,7 @@ Cudd_zddDagSize(
   DdNode * p_node)
 {
 
-    int        i;    
+    int         i;
     st_table    *table;
 
     table = st_init_table(st_ptrcmp, st_ptrhash);
@@ -132,7 +160,7 @@ Cudd_zddCountMinterm(
   DdNode * node,
   int  path)
 {
-    double    dc_var, minterms;    
+    double      dc_var, minterms;
 
     dc_var = (double)((double)(zdd->sizeZ) - (double)path);
     minterms = Cudd_zddCountDouble(zdd, node) / pow(2.0, dc_var);
@@ -156,61 +184,61 @@ void
 Cudd_zddPrintSubtable(
   DdManager * table)
 {
-    int        i, j;
-    DdNode     *z1, *z1_next, *base;
-    DdSubtable    *ZSubTable;
+    int         i, j;
+    DdNode      *z1, *z1_next, *base;
+    DdSubtable  *ZSubTable;
 
     base = table->one;
     for (i = table->sizeZ - 1; i >= 0; i--) {
-    ZSubTable = &(table->subtableZ[i]);
-    printf("subtable[%d]:\n", i);
-    for (j = ZSubTable->slots - 1; j >= 0; j--) {
-        z1 = ZSubTable->nodelist[j];
-        while (z1 != NIL(DdNode)) {
-        (void) fprintf(table->out,
+        ZSubTable = &(table->subtableZ[i]);
+        printf("subtable[%d]:\n", i);
+        for (j = ZSubTable->slots - 1; j >= 0; j--) {
+            z1 = ZSubTable->nodelist[j];
+            while (z1 != NIL(DdNode)) {
+                (void) fprintf(table->out,
 #if SIZEOF_VOID_P == 8
-            "ID = 0x%lx\tindex = %d\tr = %d\t",
-            (unsigned long) z1 / (unsigned long) sizeof(DdNode),
-            z1->index, z1->ref);
+                    "ID = 0x%lx\tindex = %u\tr = %u\t",
+                    (ptruint) z1 / (ptruint) sizeof(DdNode),
+                    z1->index, z1->ref);
 #else
-            "ID = 0x%x\tindex = %d\tr = %d\t",
-            (unsigned) z1 / (unsigned) sizeof(DdNode),
-            z1->index, z1->ref);
+                    "ID = 0x%x\tindex = %hu\tr = %hu\t",
+                    (ptruint) z1 / (ptruint) sizeof(DdNode),
+                    z1->index, z1->ref);
 #endif
-        z1_next = cuddT(z1);
-        if (Cudd_IsConstant(z1_next)) {
-            (void) fprintf(table->out, "T = %d\t\t",
-            (z1_next == base));
-        }
-        else {
+                z1_next = cuddT(z1);
+                if (Cudd_IsConstant(z1_next)) {
+                    (void) fprintf(table->out, "T = %d\t\t",
+                        (z1_next == base));
+                }
+                else {
 #if SIZEOF_VOID_P == 8
-            (void) fprintf(table->out, "T = 0x%lx\t",
-            (unsigned long) z1_next / (unsigned long) sizeof(DdNode));
+                    (void) fprintf(table->out, "T = 0x%lx\t",
+                        (ptruint) z1_next / (ptruint) sizeof(DdNode));
 #else
-            (void) fprintf(table->out, "T = 0x%x\t",
-            (unsigned) z1_next / (unsigned) sizeof(DdNode));
+                    (void) fprintf(table->out, "T = 0x%x\t",
+                        (ptruint) z1_next / (ptruint) sizeof(DdNode));
 #endif
-        }
-        z1_next = cuddE(z1);
-        if (Cudd_IsConstant(z1_next)) {
-            (void) fprintf(table->out, "E = %d\n",
-            (z1_next == base));
-        }
-        else {
+                }
+                z1_next = cuddE(z1);
+                if (Cudd_IsConstant(z1_next)) {
+                    (void) fprintf(table->out, "E = %d\n",
+                        (z1_next == base));
+                }
+                else {
 #if SIZEOF_VOID_P == 8
-            (void) fprintf(table->out, "E = 0x%lx\n",
-            (unsigned long) z1_next / (unsigned long) sizeof(DdNode));
+                    (void) fprintf(table->out, "E = 0x%lx\n",
+                        (ptruint) z1_next / (ptruint) sizeof(DdNode));
 #else
-            (void) fprintf(table->out, "E = 0x%x\n",
-            (unsigned) z1_next / (unsigned) sizeof(DdNode));
+                    (void) fprintf(table->out, "E = 0x%x\n",
+                        (ptruint) z1_next / (ptruint) sizeof(DdNode));
 #endif
-        }
+                }
 
-        z1_next = z1->next;
-        z1 = z1_next;
+                z1_next = z1->next;
+                z1 = z1_next;
+            }
         }
     }
-    }
     putchar('\n');
 
 } /* Cudd_zddPrintSubtable */
@@ -239,19 +267,20 @@ cuddZddDagInt(
   st_table * tab)
 {
     if (n == NIL(DdNode))
-    return(0);
+        return(0);
 
     if (st_is_member(tab, (char *)n) == 1)
-    return(0);
+        return(0);
 
     if (Cudd_IsConstant(n))
-    return(0);
+        return(0);
 
     (void)st_insert(tab, (char *)n, NIL(char));
     return(1 + cuddZddDagInt(cuddT(n), tab) +
-    cuddZddDagInt(cuddE(n), tab));
+        cuddZddDagInt(cuddE(n), tab));
 
 } /* cuddZddDagInt */
 
+
 ABC_NAMESPACE_IMPL_END
 

src/bdd/cudd/r7x8.1.out

+# TestCudd Version #1.0, Release date 3/17/01
+# ./testcudd -p 2 r7x8.1.mat
+:name: r7x8.1.mat: 7 rows 9 columns
+:1: M: 63 nodes 5 leaves 52 minterms
+000000--  1
+000001-0  1
+000001-1  4
+000010-0  4
+000010-1  3
+000011-0  2
+000011-1  4
+000100--  3
+000101-0  3
+000110-0  1
+000110-1  2
+000111-0  4
+001000--  1
+001001-0  4
+001010-0  2
+001010-1  1
+001011-1  4
+001100-0  2
+001100-1  3
+001101-0  3
+001110-0  4
+001110-1  1
+0100-0-0  3
+011000-0  3
+011010-0  1
+100000-0  2
+100000-1  3
+100001-0  2
+100001-1  4
+100010--  3
+100011--  4
+100100--  1
+100101-0  2
+100110-0  1
+100110-1  3
+100111-0  3
+101000-1  1
+101001-0  1
+101001-1  4
+101100-0  2
+101100-1  4
+101101-0  4
+110000-0  2
+110010-0  4
+111000-0  2
+
+:2: time to read the matrix = 0.00 sec
+:3: C: 22 nodes 1 leaves 52 minterms
+0000----  1
+0001-0--  1
+0001-1-0  1
+001000--  1
+001001-0  1
+001010--  1
+001011-1  1
+001100--  1
+001101-0  1
+001110--  1
+01-0-0-0  1
+1000----  1
+1001-0--  1
+1001-1-0  1
+101000-1  1
+101001--  1
+101100--  1
+101101-0  1
+1100-0-0  1
+111000-0  1
+
+Testing iterator on cubes:
+000000-- 1
+000001-0 1
+000001-1 4
+000010-0 4
+000010-1 3
+000011-0 2
+000011-1 4
+000100-- 3
+000101-0 3
+000110-0 1
+000110-1 2
+000111-0 4
+001000-- 1
+001001-0 4
+001010-0 2
+001010-1 1
+001011-1 4
+001100-0 2
+001100-1 3
+001101-0 3
+001110-0 4
+001110-1 1
+0100-0-0 3
+011000-0 3
+011010-0 1
+100000-0 2
+100000-1 3
+100001-0 2
+100001-1 4
+100010-- 3
+100011-- 4
+100100-- 1
+100101-0 2
+100110-0 1
+100110-1 3
+100111-0 3
+101000-1 1
+101001-0 1
+101001-1 4
+101100-0 2
+101100-1 4
+101101-0 4
+110000-0 2
+110010-0 4
+111000-0 2
+
+Testing prime expansion of cubes:
+-000---- 1
+-00--0-- 1
+0--0-0-0 1
+--00-0-0 1
+-0-100-- 1
+10-001-- 1
+-00----0 1
+00---0-- 1
+-1-000-0 1
+-0--01-0 1
+-0--00-1 1
+00-01--1 1
+
+Testing iterator on primes (CNF):
+-0-0---- 1
+-0---0-- 1
+0-0-0--- 1
+-0-----0 1
+---0-0-0 1
+0101-1-1 1
+--0-00-1 1
+1-0-10-0 1
+
+Cache used slots = 58.06% (expected 58.92%)
+xor1: 14 nodes 1 leaves 28 minterms
+000--1-1  1
+001-11-1  1
+01---0-0  1
+100--1-1  1
+101-00-0  1
+101-01-1  1
+110--0-0  1
+111-00-0  1
+
+Chosen minterm for Hamming distance test: : 9 nodes 1 leaves 1 minterms
+11110010  1
+
+Minimum Hamming distance = 1
+ycube: 5 nodes 1 leaves 8 minterms
+-0-0-0-0  1
+
+CP: 11 nodes 1 leaves 7 minterms
+00-0-0-0  1
+1000-0-0  1
+101000-1  1
+
+:4: ineq: 10 nodes 1 leaves 42 minterms
+001000--  1
+00101---  1
+1000----  1
+100100--  1
+10011---  1
+101-----  1
+111000--  1
+11101---  1
+
+10------ 1
+-01----- 1
+1-1----- 1
+-0-0---- 1
+1--0---- 1
+-0--10-- 1
+--1010-- 1
+1---10-- 1
+
+:4: ess: 1 nodes 1 leaves 128 minterms
+--------  1
+
+:5: shortP: 7 nodes 1 leaves 2 minterms
+000000--  1
+
+:5b: largest: 4 nodes 1 leaves 16 minterms
+01-1----  1
+
+The value of M along the chosen shortest path is 1
+:6: shortP: 5 nodes 1 leaves 8 minterms
+0000----  1
+
+Average distance: 4133.34
+Number of variables =      8    Number of slots     =   2304
+Number of keys      =    995    Number of min dead  =   9216
+walsh1: 16 nodes 2 leaves 256 minterms
+-0--0--0--0-  1
+-0--0--0--10  1
+-0--0--0--11 -1
+-0--0--10-0-  1
+-0--0--10-10  1
+-0--0--10-11 -1
+-0--0--11-0- -1
+-0--0--11-10 -1
+-0--0--11-11  1
+-0--10-0--0-  1
+-0--10-0--10  1
+-0--10-0--11 -1
+-0--10-10-0-  1
+-0--10-10-10  1
+-0--10-10-11 -1
+-0--10-11-0- -1
+-0--10-11-10 -1
+-0--10-11-11  1
+-0--11-0--0- -1
+-0--11-0--10 -1
+-0--11-0--11  1
+-0--11-10-0- -1
+-0--11-10-10 -1
+-0--11-10-11  1
+-0--11-11-0-  1
+-0--11-11-10  1
+-0--11-11-11 -1
+-10-0--0--0-  1
+-10-0--0--10  1
+-10-0--0--11 -1
+-10-0--10-0-  1
+-10-0--10-10  1
+-10-0--10-11 -1
+-10-0--11-0- -1
+-10-0--11-10 -1
+-10-0--11-11  1
+-10-10-0--0-  1
+-10-10-0--10  1
+-10-10-0--11 -1
+-10-10-10-0-  1
+-10-10-10-10  1
+-10-10-10-11 -1
+-10-10-11-0- -1
+-10-10-11-10 -1
+-10-10-11-11  1
+-10-11-0--0- -1
+-10-11-0--10 -1
+-10-11-0--11  1
+-10-11-10-0- -1
+-10-11-10-10 -1
+-10-11-10-11  1
+-10-11-11-0-  1
+-10-11-11-10  1
+-10-11-11-11 -1
+-11-0--0--0- -1
+-11-0--0--10 -1
+-11-0--0--11  1
+-11-0--10-0- -1
+-11-0--10-10 -1
+-11-0--10-11  1
+-11-0--11-0-  1
+-11-0--11-10  1
+-11-0--11-11 -1
+-11-10-0--0- -1
+-11-10-0--10 -1
+-11-10-0--11  1
+-11-10-10-0- -1
+-11-10-10-10 -1
+-11-10-10-11  1
+-11-10-11-0-  1
+-11-10-11-10  1
+-11-10-11-11 -1
+-11-11-0--0-  1
+-11-11-0--10  1
+-11-11-0--11 -1
+-11-11-10-0-  1
+-11-11-10-10  1
+-11-11-10-11 -1
+-11-11-11-0- -1
+-11-11-11-10 -1
+-11-11-11-11  1
+
+wtw: 14 nodes 2 leaves 16 minterms
+0-00-00-00-0  16
+0-00-00-01-1  16
+0-00-01-10-0  16
+0-00-01-11-1  16
+0-01-10-00-0  16
+0-01-10-01-1  16
+0-01-11-10-0  16
+0-01-11-11-1  16
+1-10-00-00-0  16
+1-10-00-01-1  16
+1-10-01-10-0  16
+1-10-01-11-1  16
+1-11-10-00-0  16
+1-11-10-01-1  16
+1-11-11-10-0  16
+1-11-11-11-1  16
+
+Average length of non-empty lists = 1
+**** CUDD modifiable parameters ****
+Hard limit for cache size: 7645866
+Cache hit threshold for resizing: 30%
+Garbage collection enabled: yes
+Limit for fast unique table growth: 4587520
+Maximum number of variables sifted per reordering: 1000
+Maximum number of variable swaps per reordering: 2000000
+Maximum growth while sifting a variable: 1.2
+Dynamic reordering of BDDs enabled: no
+Default BDD reordering method: 4
+Dynamic reordering of ZDDs enabled: no
+Default ZDD reordering method: 4
+Realignment of ZDDs to BDDs enabled: no
+Realignment of BDDs to ZDDs enabled: no
+Dead nodes counted in triggering reordering: no
+Group checking criterion: 7
+Recombination threshold: 0
+Symmetry violation threshold: 0
+Arc violation threshold: 0
+GA population size: 0
+Number of crossovers for GA: 0
+Next reordering threshold: 4004
+**** CUDD non-modifiable parameters ****
+Memory in use: 4274484
+Peak number of nodes: 2044
+Peak number of live nodes: 119
+Number of BDD variables: 9
+Number of ZDD variables: 0
+Number of cache entries: 2048
+Number of cache look-ups: 2846
+Number of cache hits: 715
+Number of cache insertions: 2289
+Number of cache collisions: 937
+Number of cache deletions: 1348
+Cache used slots = 66.02% (expected 67.30%)
+Soft limit for cache size: 13312
+Number of buckets in unique table: 2560
+Used buckets in unique table: 0.51% (expected 0.51%)
+Number of BDD and ADD nodes: 13
+Number of ZDD nodes: 0
+Number of dead BDD and ADD nodes: 0
+Number of dead ZDD nodes: 0
+Total number of nodes allocated: 1091
+Total number of nodes reclaimed: 950
+Garbage collections so far: 1
+Time for garbage collection: 0.00 sec
+Reorderings so far: 0
+Time for reordering: 0.00 sec
+total time = 0.00 sec
+Runtime Statistics
+------------------
+Machine name: jobim.colorado.edu
+User time      0.0 seconds
+System time    0.0 seconds
+
+Average resident text size       =     0K
+Average resident data+stack size =     0K
+Maximum resident size            =     0K
+
+Virtual text size                = 131644K
+Virtual data size                =   151K
+    data size initialized        =    17K
+    data size uninitialized      =     0K
+    data size sbrk               =   134K
+Virtual memory limit             = 358400K (4194304K)
+
+Major page faults = 0
+Minor page faults = 1318
+Swaps = 0
+Input blocks = 0
+Output blocks = 0
+Context switch (voluntary) = 1
+Context switch (involuntary) = 1