Import cudd-2.5.1.tar.gz

Author: fsomenzi

Makefile

@@ -8,6 +8,7 @@
 
 # C++ compiler
 CXX	= g++
+#CXX	= clang++
 #CXX	= icpc
 #CXX	= ecpc
 #CXX	= CC
@@ -25,9 +26,10 @@ CXXFLAGS =
 #CXXFLAGS = +a1
 
 # C compiler used for all targets except optimize_dec, which always uses cc.
+CC	= gcc
+#CC	= clang
 #CC	= cc
 #CC	= /usr/local/opt/SUNWspro/bin/cc
-CC	= gcc
 #CC	= icc
 #CC	= ecc
 #CC	= /usr/ucb/cc
@@ -59,13 +61,13 @@ ICFLAGS	= -g -O3
 #  Linux
 #
 # Gcc 4.2.4 or higher on i686.
-XCFLAGS	= -mtune=native -malign-double -DHAVE_IEEE_754 -DBSD
+#XCFLAGS	= -mtune=native -malign-double -DHAVE_IEEE_754 -DBSD
 # Gcc 3.2.2 or higher on i686.
 #XCFLAGS	= -mtune=pentium4 -malign-double -DHAVE_IEEE_754 -DBSD
 # Gcc 2.8.1 on i686.
 #XCFLAGS	= -mcpu=pentiumpro -malign-double -DHAVE_IEEE_754 -DBSD
 # Gcc 4.2.4 or higher on x86_64 (64-bit compilation)
-#XCFLAGS	= -mtune=native -DHAVE_IEEE_754 -DBSD -DSIZEOF_VOID_P=8 -DSIZEOF_LONG=8
+XCFLAGS	= -mtune=native -DHAVE_IEEE_754 -DBSD -DSIZEOF_VOID_P=8 -DSIZEOF_LONG=8
 # Gcc 4.2.4 or higher on x86_64 (32-bit compilation)
 #XCFLAGS	= -m32 -mtune=native -malign-double -DHAVE_IEEE_754 -DBSD
 # Icc on i686 (older versions may not support -xHost).
@@ -208,7 +210,7 @@ DIRS	= $(BDIRS) nanotrav
 .PHONY : check_leaks
 .PHONY : optimize_dec
 .PHONY : testcudd
-.PHONY : libobj
+.PHONY : objlib
 .PHONY : testobj
 .PHONY : testdddmp
 .PHONY : testmtr
@@ -220,7 +222,7 @@ DIRS	= $(BDIRS) nanotrav
 
 build:
 	sh ./setup.sh
-	@for dir in $(DIRS); do \
+	@+for dir in $(DIRS); do \
 		(cd $$dir; \
 		echo Making $$dir ...; \
 		make CC=$(CC) RANLIB=$(RANLIB) MFLAG= MNEMLIB= ICFLAGS="$(ICFLAGS)" XCFLAGS="$(XCFLAGS)" DDDEBUG="$(DDDEBUG)" MTRDEBUG="$(MTRDEBUG)" LDFLAGS="$(LDFLAGS)" PURE="$(PURE)" EXE="$(EXE)" )\
@@ -230,78 +232,78 @@ nanotrav: build
 
 check_leaks:
 	sh ./setup.sh
-	@for dir in mnemosyne $(DIRS); do \
+	@+for dir in mnemosyne $(DIRS); do \
 		(cd $$dir; \
 		echo Making $$dir ...; \
 		make CC=$(CC) RANLIB=$(RANLIB) MFLAG=$(MFLAG) MNEMLIB=$(MNEMLIB) ICFLAGS="$(ICFLAGS)" XCFLAGS="$(XCFLAGS)" DDDEBUG="$(DDDEBUG)" MTRDEBUG="$(MTRDEBUG)" LDFLAGS="$(LDFLAGS)" EXE="$(EXE)" )\
 	done
 
 optimize_dec:
 	sh ./setup.sh
-	@for dir in $(DIRS); do \
+	@+for dir in $(DIRS); do \
 		(cd $$dir; \
 		echo Making $$dir ...; \
 		make CC=$(CC) RANLIB=$(RANLIB) XCFLAGS="$(XCFLAGS)" LDFLAGS="$(LDFLAGS)" optimize_dec )\
 	done
 
 lint:
 	sh ./setup.sh
-	@for dir in $(DIRS) obj; do \
+	@+for dir in $(DIRS) obj; do \
 		(cd $$dir; \
 		echo Making lint in $$dir ...; \
 		make CC=$(CC) lint )\
 	done
 
 tags:
 	sh ./setup.sh
-	@for dir in $(DIRS) obj; do \
+	@+for dir in $(DIRS) obj; do \
 		(cd $$dir; \
 		echo Making tags in $$dir ...; \
 		make CC=$(CC) tags )\
 	done
 
 all:
 	sh ./setup.sh
-	@for dir in $(DIRS); do \
+	@+for dir in $(DIRS); do \
 		(cd $$dir; \
 		echo Making all in $$dir ...; \
 		make CC=$(CC) RANLIB=$(RANLIB) MFLAG= MNEMLIB= ICFLAGS="$(ICFLAGS)" XCFLAGS="$(XCFLAGS)" DDDEBUG="$(DDDEBUG)" MTRDEBUG="$(MTRDEBUG)" LDFLAGS="$(LDFLAGS)" PURE="$(PURE)" EXE="$(EXE)" all )\
 	done
 
 testcudd:
 	sh ./setup.sh
-	@for dir in util st mtr epd; do \
+	@+for dir in util st mtr epd; do \
 		(cd $$dir; \
 		echo Making $$dir ...; \
 		make CC=$(CC) RANLIB=$(RANLIB) MFLAG= MNEMLIB= ICFLAGS="$(ICFLAGS)" XCFLAGS="$(XCFLAGS)" DDDEBUG="$(DDDEBUG)" MTRDEBUG="$(MTRDEBUG)" LDFLAGS="$(LDFLAGS)" PURE="$(PURE)" EXE="$(EXE)" )\
 	done
-	@(cd cudd; \
+	@+(cd cudd; \
 	echo Making testcudd ...; \
 	make CC=$(CC) RANLIB=$(RANLIB) MFLAG= MNEMLIB= ICFLAGS="$(ICFLAGS)" XCFLAGS="$(XCFLAGS)" DDDEBUG="$(DDDEBUG)" MTRDEBUG="$(MTRDEBUG)" LDFLAGS="$(LDFLAGS)" PURE="$(PURE)" EXE="$(EXE)" testcudd$(EXE) )
 
 objlib:
 	sh ./setup.sh
-	@for dir in $(BDIRS); do \
+	@+for dir in $(BDIRS); do \
 		(cd $$dir; \
 		echo Making $$dir ...; \
 		make CC=$(CC) RANLIB=$(RANLIB) MFLAG= MNEMLIB= ICFLAGS="$(ICFLAGS)" XCFLAGS="$(XCFLAGS)" DDDEBUG="$(DDDEBUG)" MTRDEBUG="$(MTRDEBUG)" LDFLAGS="$(LDFLAGS)" PURE="$(PURE)" EXE="$(EXE)" )\
 	done
-	@(cd obj; \
+	@+(cd obj; \
 	echo Making obj ...; \
 	make CXX=$(CXX) CXXFLAGS=$(CXXFLAGS) RANLIB=$(RANLIB) MFLAG= MNEMLIB= ICFLAGS="$(ICFLAGS)" XCFLAGS="$(XCFLAGS)" DDDEBUG="$(DDDEBUG)" MTRDEBUG="$(MTRDEBUG)" LDFLAGS="$(LDFLAGS)" PURE="$(PURE)" EXE="$(EXE)" )
 
 testobj: objlib
-	@(cd obj; \
+	@+(cd obj; \
 	echo Making testobj ...; \
 	make CXX=$(CXX) CXXFLAGS=$(CXXFLAGS) RANLIB=$(RANLIB) MFLAG= MNEMLIB= ICFLAGS="$(ICFLAGS)" XCFLAGS="$(XCFLAGS)" DDDEBUG="$(DDDEBUG)" MTRDEBUG="$(MTRDEBUG)" LDFLAGS="$(LDFLAGS)" PURE="$(PURE)" EXE="$(EXE)" testobj$(EXE) )
 
 testdddmp: build
-	@(cd dddmp; \
+	@+(cd dddmp; \
 	echo Making testdddmp ...; \
 	make CC=$(CC) RANLIB=$(RANLIB) MFLAG= MNEMLIB= ICFLAGS="$(ICFLAGS)" XCFLAGS="$(XCFLAGS)" DDDEBUG="$(DDDEBUG)" MTRDEBUG="$(MTRDEBUG)" LDFLAGS="$(LDFLAGS)" PURE="$(PURE)" EXE="$(EXE)" testdddmp$(EXE) )
 
 testmtr: build
-	@(cd mtr; \
+	@+(cd mtr; \
 	echo Making testmtr ...; \
 	make CC=$(CC) RANLIB=$(RANLIB) MFLAG= MNEMLIB= ICFLAGS="$(ICFLAGS)" XCFLAGS="$(XCFLAGS)" DDDEBUG="$(DDDEBUG)" MTRDEBUG="$(MTRDEBUG)" LDFLAGS="$(LDFLAGS)" PURE="$(PURE)" EXE="$(EXE)" testmtr$(EXE) )
 

README

@@ -159,7 +159,7 @@ nanotrav that uses mnemosyne may work.
 
 DOCUMENTATION
 
-Directory cudd-2.5.0/cudd/doc contains HTML documentation for the CUDD
+Directory cudd-2.5.1/cudd/doc contains HTML documentation for the CUDD
 package. The recommended starting point is cuddIntro.html. Documentation
 in both postscript(tm) format and plain text format is also provided.
 Documentation for the auxiliary libraries (except for the util library)

RELEASE.NOTES

@@ -1,4 +1,37 @@
-Release 2.5.0 of Cudd introduces the ability to set timeouts.  The
+Release 2.5.1 of Cudd improves support for multi-threaded applications.
+Specifically, an application may now register a callback function that
+is called from time to time to check whether computation should be
+terminated because another thread has found the result.
+
+The C++ interface allows the application to register variable names with
+the manager and implements operator<< for BDDs.  The interfaces of
+SolveEqn and VerifySol now take std::vectors instead of plain arrays.
+
+Fixed a few bugs in CUDD and a bug in the mtr package.
+
+Added const qualifiers to dumping function interfaces
+(Cudd_DumpDot,...).
+
+The Makefile now supports gmake's -j option.  Change "@+" back to "@" if
+this causes problems with your make program.
+
+Buggy documentation that was shipped with 2.5.0 has been fixed.
+
+New functions:
+
+extern int Cudd_bddIsVar(DdManager * dd, DdNode * f);
+
+extern void Cudd_RegisterTerminationCallback(DdManager *unique,
+
+extern void Cudd_UnregisterTerminationCallback(DdManager *unique);
+
+extern void Cudd_SetApplicationHook(DdManager *dd, void * value);
+
+extern void * Cudd_ReadApplicationHook(DdManager *dd);
+
+extern char * Cudd_FactoredFormString(DdManager *dd, DdNode *f, char const * const * inames);
+
+Releas 2.5.0 of Cudd introduces the ability to set timeouts.  The
 function that is interrupted returns NULL (which the application must
 be prepared to handle,) but the BDDs are uncorrupted and the invoking
 program can continue to use the manager.

cudd/cudd.h

@@ -50,7 +50,7 @@
   ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
   POSSIBILITY OF SUCH DAMAGE.]
 
-  Revision    [$Id: cudd.h,v 1.180 2012/02/05 01:07:18 fabio Exp $]
+  Revision    [$Id: cudd.h,v 1.182 2015/01/03 18:21:34 fabio Exp $]
 
 ******************************************************************************/
 
@@ -72,7 +72,7 @@ extern "C" {
 /* Constant declarations                                                     */
 /*---------------------------------------------------------------------------*/
 
-#define CUDD_VERSION "2.5.0"
+#define CUDD_VERSION "2.5.1"
 
 #ifndef SIZEOF_VOID_P
 #define SIZEOF_VOID_P 4
@@ -219,6 +219,7 @@ typedef enum {
     CUDD_TOO_MANY_NODES,
     CUDD_MAX_MEM_EXCEEDED,
     CUDD_TIMEOUT_EXPIRED,
+    CUDD_TERMINATION,
     CUDD_INVALID_ARG,
     CUDD_INTERNAL_ERROR
 } Cudd_ErrorType;
@@ -311,6 +312,8 @@ typedef DdNode * (*DD_CTFP1)(DdManager *, DdNode *);
 typedef void (*DD_OOMFP)(long);
 /* Type of comparison function for qsort. */
 typedef int (*DD_QSFP)(const void *, const void *);
+/* Type of termination handler. */
+typedef int (*DD_THFP)(const void *);
 
 /*---------------------------------------------------------------------------*/
 /* Variable declarations                                                     */
@@ -620,6 +623,7 @@ extern DdNode * Cudd_addNewVar (DdManager *dd);
 extern DdNode * Cudd_addNewVarAtLevel (DdManager *dd, int level);
 extern DdNode * Cudd_bddNewVar (DdManager *dd);
 extern DdNode * Cudd_bddNewVarAtLevel (DdManager *dd, int level);
+extern int Cudd_bddIsVar(DdManager * dd, DdNode * f);
 extern DdNode * Cudd_addIthVar (DdManager *dd, int i);
 extern DdNode * Cudd_bddIthVar (DdManager *dd, int i);
 extern DdNode * Cudd_zddIthVar (DdManager *dd, int i);
@@ -636,6 +640,8 @@ extern void Cudd_UpdateTimeLimit(DdManager * unique);
 extern void Cudd_IncreaseTimeLimit(DdManager * unique, unsigned long increase);
 extern void Cudd_UnsetTimeLimit(DdManager *unique);
 extern int Cudd_TimeLimited(DdManager *unique);
+extern void Cudd_RegisterTerminationCallback(DdManager *unique, DD_THFP callback, void * callback_arg);
+extern void Cudd_UnregisterTerminationCallback(DdManager *unique);
 extern void Cudd_AutodynEnable (DdManager *unique, Cudd_ReorderingType method);
 extern void Cudd_AutodynDisable (DdManager *unique);
 extern int Cudd_ReorderingStatus (DdManager *unique, Cudd_ReorderingType *method);
@@ -748,6 +754,8 @@ extern int Cudd_PrintGroupedOrder(DdManager * dd, const char *str, void *data);
 extern int Cudd_EnableOrderingMonitoring(DdManager *dd);
 extern int Cudd_DisableOrderingMonitoring(DdManager *dd);
 extern int Cudd_OrderingMonitoring(DdManager *dd);
+extern void Cudd_SetApplicationHook(DdManager *dd, void * value);
+extern void * Cudd_ReadApplicationHook(DdManager *dd);
 extern Cudd_ErrorType Cudd_ReadErrorCode (DdManager *dd);
 extern void Cudd_ClearErrorCode (DdManager *dd);
 extern FILE * Cudd_ReadStdout (DdManager *dd);
@@ -888,12 +896,13 @@ extern DdTlcInfo * Cudd_FindTwoLiteralClauses (DdManager * dd, DdNode * f);
 extern int Cudd_PrintTwoLiteralClauses (DdManager * dd, DdNode * f, char **names, FILE *fp);
 extern int Cudd_ReadIthClause (DdTlcInfo * tlc, int i, DdHalfWord *var1, DdHalfWord *var2, int *phase1, int *phase2);
 extern void Cudd_tlcInfoFree (DdTlcInfo * t);
-extern int Cudd_DumpBlif (DdManager *dd, int n, DdNode **f, char **inames, char **onames, char *mname, FILE *fp, int mv);
-extern int Cudd_DumpBlifBody (DdManager *dd, int n, DdNode **f, char **inames, char **onames, FILE *fp, int mv);
-extern int Cudd_DumpDot (DdManager *dd, int n, DdNode **f, char **inames, char **onames, FILE *fp);
-extern int Cudd_DumpDaVinci (DdManager *dd, int n, DdNode **f, char **inames, char **onames, FILE *fp);
-extern int Cudd_DumpDDcal (DdManager *dd, int n, DdNode **f, char **inames, char **onames, FILE *fp);
-extern int Cudd_DumpFactoredForm (DdManager *dd, int n, DdNode **f, char **inames, char **onames, FILE *fp);
+extern int Cudd_DumpBlif (DdManager *dd, int n, DdNode **f, char const * const *inames, char const * const *onames, char *mname, FILE *fp, int mv);
+extern int Cudd_DumpBlifBody (DdManager *dd, int n, DdNode **f, char const * const *inames, char const * const *onames, FILE *fp, int mv);
+extern int Cudd_DumpDot (DdManager *dd, int n, DdNode **f, char const * const *inames, char const * const *onames, FILE *fp);
+extern int Cudd_DumpDaVinci (DdManager *dd, int n, DdNode **f, char const * const *inames, char const * const *onames, FILE *fp);
+extern int Cudd_DumpDDcal (DdManager *dd, int n, DdNode **f, char const * const *inames, char const * const *onames, FILE *fp);
+extern int Cudd_DumpFactoredForm (DdManager *dd, int n, DdNode **f, char const * const *inames, char const * const *onames, FILE *fp);
+extern char * Cudd_FactoredFormString(DdManager *dd, DdNode *f, char const * const * inames);
 extern DdNode * Cudd_bddConstrain (DdManager *dd, DdNode *f, DdNode *c);
 extern DdNode * Cudd_bddRestrict (DdManager *dd, DdNode *f, DdNode *c);
 extern DdNode * Cudd_bddNPAnd (DdManager *dd, DdNode *f, DdNode *c);
@@ -1044,7 +1053,7 @@ extern DdGen * Cudd_zddFirstPath (DdManager *zdd, DdNode *f, int **path);
 extern int Cudd_zddNextPath (DdGen *gen, int **path);
 extern char * Cudd_zddCoverPathToString (DdManager *zdd, int *path, char *str);
 extern DdNode * Cudd_zddSupport(DdManager * dd, DdNode * f);
-extern int Cudd_zddDumpDot (DdManager *dd, int n, DdNode **f, char **inames, char **onames, FILE *fp);
+extern int Cudd_zddDumpDot (DdManager *dd, int n, DdNode **f, char const * const *inames, char const * const *onames, FILE *fp);
 extern int Cudd_bddSetPiVar (DdManager *dd, int index);
 extern int Cudd_bddSetPsVar (DdManager *dd, int index);
 extern int Cudd_bddSetNsVar (DdManager *dd, int index);