[patch] sci-mathematics/pvs/files/pvs-4.2-patch-bddp

pvs-4.2-patch-bddp (text/plain), 30.25 KB, created by Jonathan-Christofer Demay on 2009-03-25 10:44:43 UTC

diff -Naur pvs4.2-orig/BDD/bdd/ex/test.pl pvs4.2-bddp/BDD/bdd/ex/test.pl
--- pvs4.2-orig/BDD/bdd/ex/test.pl	2007-07-02 20:07:41.000000000 +0000
+++ pvs4.2-bddp/BDD/bdd/ex/test.pl	2009-03-24 18:49:23.000000000 +0000
@@ -8,11 +8,11 @@
 
 (y implies x) and (y equiv a or not a) -> (x equiv y) .
 
-not E :- ((A and W) implies P), /* Superman */
-         (not A implies I),
+not F :- ((B and W) implies P), /* Superman */
+         (not B implies I),
          (not W implies M),
          (not P),
-         (E implies not I and not M) .
+         (F implies not I and not M) .
 
 /* Portrait in the casket */
 G :-
diff -Naur pvs4.2-orig/BDD/bdd/src/appl.c pvs4.2-bddp/BDD/bdd/src/appl.c
--- pvs4.2-orig/BDD/bdd/src/appl.c	2007-07-02 20:07:41.000000000 +0000
+++ pvs4.2-bddp/BDD/bdd/src/appl.c	2009-03-24 18:49:23.000000000 +0000
@@ -105,7 +105,7 @@
   int flag;
 
   /* LET introduced names come first! */
-  if (lookup (aux_table, s, len, &info.voidptr, LOOKUP) != NOT_PRESENT) {
+  if (lookup (aux_table, s, len, &info.voidptr, LOOKUP_PTR) != NOT_PRESENT) {
     /* This name is indeed used for a secondary variable. */
     if (!BDD_VOID_P (info.bddptr)) {
       BDD_GC_PROTECT (info.bddptr);
@@ -118,7 +118,7 @@
   }
 
   /* Here define as primary variable: */
-  flag = (int) INSERT;
+  flag = INSERT;
   index = lookup (var_table, s, len, NULL, &flag);
   if (flag == INDEED_INSERTED) {
     var_count++;
@@ -132,12 +132,12 @@
   int index;
   int flag;
 
-  if (lookup (aux_table, s, len, NULL, LOOKUP) != NOT_PRESENT)
+  if (lookup (aux_table, s, len, NULL, LOOKUP_PTR) != NOT_PRESENT)
     if (warnings)
     fprintf (stderr,
      "Warning: secondary variable %s already exists.\n", s);
 
-  flag = (int) INSERT;
+  flag = INSERT;
   index = lookup (var_table, s, len, NULL, &flag);
   if (flag == INDEED_INSERTED) {
     var_count++;
@@ -148,12 +148,12 @@
 
 int make_sub_var (char *s, int len)
 {
-  if (lookup (var_table, s, len, NULL, LOOKUP) != NOT_PRESENT)
+  if (lookup (var_table, s, len, NULL, LOOKUP_PTR) != NOT_PRESENT)
     if (warnings)
     fprintf (stderr,
      "Warning: primary variable %s already exists.\n", s);
 
-  return lookup (aux_table, s, len, NULL, INSERT);
+  return lookup (aux_table, s, len, NULL, INSERT_PTR);
 }
 
 BDDPTR make_definition (int id_index, BDDPTR function)
diff -Naur pvs4.2-orig/BDD/bdd/src/bdd.c pvs4.2-bddp/BDD/bdd/src/bdd.c
--- pvs4.2-orig/BDD/bdd/src/bdd.c	2007-09-05 00:04:00.000000000 +0000
+++ pvs4.2-bddp/BDD/bdd/src/bdd.c	2009-03-24 18:49:23.000000000 +0000
@@ -214,13 +214,13 @@
    falls apart. This is tested in bdd_alloc().
 */
 #define BDD_F_MASK	0x80000000
-#define BDD_F_SET(F)	((BDDPTR) (((int) (F)) | BDD_F_MASK))
+#define BDD_F_SET(F)	((BDDPTR) (BITS (F) | BDD_F_MASK))
 #define BDD_F_SET_SAVE(F)	\
 	(bdd_ok_to_use_MSB ? BDD_F_SET(F) \
                            : (fputs( \
 "[bdd]: Not allowed to use MSB of BDD pointer.\n", stderr), \
 			      exit(1), BDD_VOID))
-#define BDD_FUNC_P(F)	(bdd_ok_to_use_MSB && (((int) (F)) & BDD_F_MASK))
+#define BDD_FUNC_P(F)	(bdd_ok_to_use_MSB && (BITS (F) & BDD_F_MASK))
 
 /* ------------------------------------------------------------------------ */
 /* LOCAL TYPE DEFINITIONS                                                   */
@@ -592,8 +592,8 @@
 
   if ((reason = bdd_valid_p (f)) != 0) {
     fprintf (stderr,
-	     "[bdd_check_valid]: 0x%x, %s%s%s.\n",
-	     (Nat) f, mess[reason],
+	     "[bdd_check_valid]: %p, %s%s%s.\n",
+	     f, mess[reason],
 	     text ? ", " : "", text);
     exit (1);
   }
@@ -967,7 +967,7 @@
 static Nat ceil_log2(Nat n)
 {
   Nat mask = 0x0000FFFF;
-  Bool not2pow = 0;
+  Nat not2pow = 0;
   Nat r =  0;
   Nat d = 16;
 
@@ -991,19 +991,20 @@
 /* Using muliplicative method in hashing. Constant A according Knuth:
    A = (PHI - 1) * 2^32, with PHI = golden ratio = (1 + sqrt(5))/2
    PHI-1 = 0.61803 39887 49894 84820 ...
-   A = 26544357690 = -1640531527 = 0x9E3779B9U
+   A = 2654435769 = -1640531527 = 0x9E3779B9U
+   The nearest prime number is 2654435761 = 0x9E3779B1U
 */
 
 /* Hashes Nat `k' to a value in the range [0..2^log2size-1]. */
-#define BDD_HASH(k,log2size)	div_pow2(0x9E3779B9U*(k), NAT_BIT-(log2size))
+#define BDD_HASH(k,log2size)	div_pow2(0x9E3779B1U*(k), NAT_BIT-(log2size))
 
 #define hash_U(T, E, log2size) \
-     BDD_HASH((((Nat) (T) >> 2) ^ ((Nat) (E) << 3)), (log2size))
+     BDD_HASH((Nat)((BITS (T) >> 2) ^ (BITS (E) << 3)), (log2size))
 
 /*  ((((v) ^ ((int) T << 7) ^ ((int) (E) << 9)) & INT_MAX) % size)*/
 
 #define hash_C(F, G, H, log2size) \
-     BDD_HASH((((Nat) F) ^ ((Nat) (G) << 7) ^ ((Nat) (H) << 9)), (log2size))
+     BDD_HASH((Nat)(BITS (F) ^ (BITS (G) << 7) ^ (BITS (H) << 9)), (log2size))
 
 static
 BDDPTR bdd_lookup_computed_table_no_reclaim (BDDPTR F, BDDPTR G, BDDPTR H)
@@ -3100,11 +3101,11 @@
     fprintf (global_fp, "%3d, [%3d], ", BDD_VARID (v), BDD_RANK (v));
   fprintf (global_fp, "(M:%s), ", BDD_MARK (v) ? "1" : "0");
 
-  fprintf (global_fp, "&v: 0x%08x, Refs: %3d, Then: 0x%08x, Else: 0x%08x\n",
-	   (Nat) v,
+  fprintf (global_fp, "&v: %p, Refs: %3d, Then: %p, Else: %p\n",
+	   v,
 	   BDD_REFCOUNT (v),
-	   (Nat) BDD_THEN (v),
-	   (Nat) BDD_ELSE (v));
+	   BDD_THEN (v),
+	   BDD_ELSE (v));
 }
 
 void bdd_print_node (FILE *fp, BDDPTR v)
diff -Naur pvs4.2-orig/BDD/bdd/src/bdd_fns.c pvs4.2-bddp/BDD/bdd/src/bdd_fns.c
--- pvs4.2-orig/BDD/bdd/src/bdd_fns.c	2007-07-02 20:07:41.000000000 +0000
+++ pvs4.2-bddp/BDD/bdd/src/bdd_fns.c	2009-03-24 18:49:23.000000000 +0000
@@ -833,7 +833,7 @@
 
 static int rank_less_or_equal (void *a, void *b)
 {
-  return BDD_VAR_RANK ((int) a) - BDD_VAR_RANK ((int) b);
+  return BDD_VAR_RANK ((int) (long) a) - BDD_VAR_RANK ((int) (long) b);
 }
 
 /* Destructively reorders `vars' to obtain all variable elements in
@@ -848,8 +848,9 @@
 
 static void collect_cube_vars_action (int index, int neg, int first)
 {
-  list_of_cube_varids = bdd_list_append_cont ((void *) (neg ? -index : index),
-					      list_of_cube_varids);
+  list_of_cube_varids =
+    bdd_list_append_cont ((void *) (long) (neg ? -index : index),
+			  list_of_cube_varids);
 }
 
 BDD_LIST bdd_cube_as_list_of_vars (BDDPTR cube)
@@ -2544,7 +2545,7 @@
 static int occupancy = 0;
 
 #define hash_sop(a) \
-  ((((int) a) & INT_MAX) % SOP_CACHE_SIZE)
+  ((BITS (a) & INT_MAX) % SOP_CACHE_SIZE)
 
 /* Looks up BDD f in sop_cache and when a sum-of-cubes list is present
    for it returns a full copy of the list (list elements are BDD cubes
diff -Naur pvs4.2-orig/BDD/bdd/src/bdd.h pvs4.2-bddp/BDD/bdd/src/bdd.h
--- pvs4.2-orig/BDD/bdd/src/bdd.h	2007-07-02 20:07:41.000000000 +0000
+++ pvs4.2-bddp/BDD/bdd/src/bdd.h	2009-03-24 18:49:23.000000000 +0000
@@ -31,7 +31,7 @@
 /* IMPORTANT NOTICE!!!
 
    This package freely uses the two least significant bits of a pointer
-   value, which by the way is also assumed to be a 32-bit quantity.
+   value, which is assumed to be a 32-bit or 64-bit quantity.
    It therefore is assumed that BDD structs are all aligned on a word
    boundary (for addresses both bits are always 0). Since the package
    does it own BDD nodes allocation in blocks, this is always assured.
@@ -76,12 +76,15 @@
 #define BDD_MAXRANK		BDD_MAXVARID
 
 /* Attributed edges masks: output and input inverters: */
-#define BDD_O_INV_MASK		0x1
-#define BDD_I_INV_MASK		0x2
+#define BDD_O_INV_MASK		0x1L
+#define BDD_I_INV_MASK		0x2L
 #define BDD_INV_MASK		(BDD_O_INV_MASK | BDD_I_INV_MASK)
 
+/* Look at edge as a set of bits: */
+#define BITS(F)			((long) F)
+
 /* Look at edge as a real pointer: */
-#define PTR(F)			((BDDPTR) (((int) (F)) & ~BDD_INV_MASK))
+#define PTR(F)			((BDDPTR) (BITS (F) & ~BDD_INV_MASK))
 
 /* Access to various fields of BDD node: */
 /* Not guarded against BDD_VOID arg! */
@@ -158,23 +161,23 @@
 #define BDD_DEAD_P(F)		(BDD_REFCOUNT (F) == 0)
 
 /* Test whether edge v is postive or negative: */
-#define BDD_NEG_P(F)		(!!(((int) (F)) & BDD_O_INV_MASK))
-#define BDD_POS_P(F)		!BDD_NEG_P (F)
+#define BDD_POS_P(F)		(!(BITS (F) & BDD_O_INV_MASK))
+#define BDD_NEG_P(F)		!BDD_POS_P (F)
 
 #define BDD_O_INV_EDGE_P(F)	BDD_NEG_P (F)
 
 /* Test whether edge v refers to inverted input node: */
-#define BDD_I_INV_EDGE_P(F)	(!!(((int) (F)) & BDD_I_INV_MASK))
+#define BDD_I_INV_EDGE_P(F)	(!!(BITS (F) & BDD_I_INV_MASK))
 
 /* Setting and clearing of edge attribute bits: */
-#define BDD_O_OFF(F)	((BDDPTR) (((int) (F)) & ~BDD_O_INV_MASK))
-#define BDD_O_SET_U(F)  ((BDDPTR) (((int) (F)) | BDD_O_INV_MASK))
+#define BDD_O_OFF(F)	((BDDPTR) (BITS (F) & ~BDD_O_INV_MASK))
+#define BDD_O_SET_U(F)  ((BDDPTR) (BITS (F) | BDD_O_INV_MASK))
 /* Special case for BDD_X and user terminals. Never have O_INV bit set! */
 #define BDD_O_SET(F)	((BDD_TERM_P (F) && !BDD_BOOL_P (F)) ? (F) \
 			 : BDD_O_SET_U (F))
 
-#define BDD_I_OFF(F)	((BDDPTR) (((int) (F)) & ~BDD_I_INV_MASK))
-#define BDD_I_SET_U(F)	((BDDPTR) (((int) (F)) | BDD_I_INV_MASK))
+#define BDD_I_OFF(F)	((BDDPTR) (BITS (F) & ~BDD_I_INV_MASK))
+#define BDD_I_SET_U(F)	((BDDPTR) (BITS (F) | BDD_I_INV_MASK))
 /* Special case for terminals. Never have I_INV bit set! */
 #define BDD_I_SET(F)	(BDD_TERM_P (F) ? (F) : BDD_I_SET_U (F))
 
@@ -244,7 +247,7 @@
 /* Are functions each other's complement:
    (Only correct when bdd_use_neg_edges == 1)
 */
-#define BDD_COMPL_P(F1, F2)	((((int) F1) ^ ((int) F2)) == BDD_O_INV_MASK)
+#define BDD_COMPL_P(F1, F2)	((BITS (F1) ^ BITS (F2)) == BDD_O_INV_MASK)
 
 /* The rank value of variable id; lowest rank is 0. */
 #define BDD_VAR_RANK(v)		(((v) == BDD_TERMID) \
@@ -335,6 +338,9 @@
   unsigned int inedge_cnt    :  NR_INEDGE_COUNT_BITS;
   unsigned int pos_size      :  NR_SIZE_BITS;
   unsigned int neg_size      :  NR_SIZE_BITS;
+#if BITS64 == 1
+  unsigned int padding;
+#endif
 } factor1_aux;
 
 typedef struct {
@@ -342,6 +348,9 @@
   unsigned int root_flag     :  1;
   unsigned int subexpr_flag  :  1;
   unsigned int subexpr_index :  NR_INDEX_BITS;
+#if BITS64 == 1
+  unsigned int padding;
+#endif
 } factor2_aux;
 
 /* ------------------------------------------------------------------------ */
@@ -363,6 +372,9 @@
   unsigned int length0      : 31;
   unsigned int follow_then1 :  1;
   unsigned int length1      : 31;
+#if BITS64 == 1
+  unsigned long padding;
+#endif
 } path_rec;
 
 /* ------------------------------------------------------------------------ */
@@ -418,6 +430,9 @@
   unsigned flag :1;		/* Left/Right flag used in BDD traversal */
   unsigned mark :1;		/* mark bit used in BDD traversal */
   unsigned refcount:BDD_NR_RC_BITS; /* saturating reference count */
+#if BITS64 == 1
+  unsigned padding;
+#endif
   BDDPTR then_link;		/* child for variable = 1 */
   BDDPTR else_link;		/* child for variable = 0 */
   BDDPTR next;			/* chaining in unique table */
diff -Naur pvs4.2-orig/BDD/bdd/src/bdd_list.h pvs4.2-bddp/BDD/bdd/src/bdd_list.h
--- pvs4.2-orig/BDD/bdd/src/bdd_list.h	2007-07-02 20:07:41.000000000 +0000
+++ pvs4.2-bddp/BDD/bdd/src/bdd_list.h	2009-03-24 18:49:23.000000000 +0000
@@ -27,8 +27,8 @@
 #define BDD_LIST_END_FOR_EACH_ELEM	END_FOR_EACH_LIST_ELEM
 #define BDD_ELEM_CALLOC			CALLOC_LIST_ELEM
 #define BDD_ELEM_CONTENTS(e)		((BDDPTR) ELEM_CONTENTS(e))
-#define BDD_ELEM_CONTENTS_I(e)		((int) ELEM_CONTENTS(e))
-#define BDD_ELEM_SET_CONTENTS(e,v)	(ELEM_CONTENTS(e) = (void *) (v))
+#define BDD_ELEM_CONTENTS_I(e)		((int) (long) ELEM_CONTENTS(e))
+#define BDD_ELEM_SET_CONTENTS(e,v)	(ELEM_CONTENTS(e) = (void *) (long)(v))
 #define BDD_LIST_FIRST			LIST_FIRST
 #define BDD_LIST_NEXT			LIST_NEXT
 #define BDD_LIST_LAST			LIST_LAST
diff -Naur pvs4.2-orig/BDD/bdd/src/bdd_quant.c pvs4.2-bddp/BDD/bdd/src/bdd_quant.c
--- pvs4.2-orig/BDD/bdd/src/bdd_quant.c	2007-07-02 20:07:41.000000000 +0000
+++ pvs4.2-bddp/BDD/bdd/src/bdd_quant.c	2009-03-24 18:49:23.000000000 +0000
@@ -777,14 +777,15 @@
 /* Using muliplicative method in hashing. Constant A according Knuth:
    A = (PHI - 1) * 2^32, with PHI = golden ratio = (1 + sqrt(5))/2
    PHI-1 = 0.61803 39887 49894 84820 ...
-   A = 26544357690 = -1640531527 = 0x9E3779B9U
+   A = 2654435769 = -1640531527 = 0x9E3779B9U
+   The nearest prime number is 2654435761 = 0x9E3779B1U
 */
 
 /* Hashes Nat `k' to a value in the range [0..2^log2size-1]. */
-#define BDD_HASH(k,log2size)	div_pow2(0x9E3779B9U*(k), NAT_BIT-(log2size))
+#define BDD_HASH(k,log2size)	div_pow2(0x9E3779B1U*(k), NAT_BIT-(log2size))
 
 #define hash_and_smooth(a, b) \
-    BDD_HASH((((Nat) (a)) ^ ((Nat) (b) << 15)), BDD_AND_SMOOTH_CACHE_LOG2SIZE)
+  BDD_HASH((Nat)((BITS (a)) ^ (BITS (b) << 15)), BDD_AND_SMOOTH_CACHE_LOG2SIZE)
 
 static BDDPTR bdd_lookup_and_smooth_cache (BDDPTR f, BDDPTR g)
 {
diff -Naur pvs4.2-orig/BDD/bdd/src/bdd_vfns.c pvs4.2-bddp/BDD/bdd/src/bdd_vfns.c
--- pvs4.2-orig/BDD/bdd/src/bdd_vfns.c	2007-07-02 20:07:41.000000000 +0000
+++ pvs4.2-bddp/BDD/bdd/src/bdd_vfns.c	2009-03-24 18:49:23.000000000 +0000
@@ -40,7 +40,7 @@
     BDDPTR *F;
 
     F = CALLOC_ARRAY (size+1, BDDPTR);
-    F[0] = (BDDPTR) size;
+    F[0] = (BDDPTR) (long) size;
     return F+1;
   }
   return NULL;
diff -Naur pvs4.2-orig/BDD/bdd/src/bdd_vfns.h pvs4.2-bddp/BDD/bdd/src/bdd_vfns.h
--- pvs4.2-orig/BDD/bdd/src/bdd_vfns.h	2007-07-02 20:07:41.000000000 +0000
+++ pvs4.2-bddp/BDD/bdd/src/bdd_vfns.h	2009-03-24 18:49:23.000000000 +0000
@@ -10,7 +10,7 @@
  - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
 */
 
-#define BDDVEC_SIZE(F)			((F) ? ((int *) F)[-1] : 0)
+#define BDDVEC_SIZE(F)			((F) ? (int) BITS (F[-1]) : 0)
 
 extern BDDPTR *MakeBDDVec		(int size);
 extern   void  FreeBDDVec		(BDDPTR *F);
diff -Naur pvs4.2-orig/BDD/bdd/src/ChangeLog pvs4.2-bddp/BDD/bdd/src/ChangeLog
--- pvs4.2-orig/BDD/bdd/src/ChangeLog	2007-07-02 20:07:41.000000000 +0000
+++ pvs4.2-bddp/BDD/bdd/src/ChangeLog	2009-03-24 18:49:23.000000000 +0000
@@ -1,3 +1,17 @@
[phone]  Jerry James  <[e-mail]>
+
+	* Makefile
+	* appl.c
+	* bdd.c:
+	* bdd.h:
+	* bdd_fns.c:
+	* bdd_list.h:
+	* bdd_quant.c:
+	* bdd_vfns.c:
+	* bdd_vfns.h
+	* template.c:
+	* yacc.y: Support compilation on 64-bit machines.
+
 Thu Apr 16 10:25:56 1998  Geert Janssen  <[e-mail]>
 
 	* bdd_quant.c (bdd_lookup_and_smooth_cache): also using
diff -Naur pvs4.2-orig/BDD/bdd/src/main.c pvs4.2-bddp/BDD/bdd/src/main.c
--- pvs4.2-orig/BDD/bdd/src/main.c	2007-07-02 20:07:41.000000000 +0000
+++ pvs4.2-bddp/BDD/bdd/src/main.c	2009-03-24 18:49:23.000000000 +0000
@@ -309,7 +309,7 @@
 
   var_table = make_hashtab (3);
   /* Let's not use entry nr. 0 for fun: */
-/*  lookup (var_table, "", 0, NULL, INSERT);*/
+/*  lookup (var_table, "", 0, NULL, INSERT_PTR);*/
 
   aux_table = make_hashtab (0);
 
diff -Naur pvs4.2-orig/BDD/bdd/src/Makefile pvs4.2-bddp/BDD/bdd/src/Makefile
--- pvs4.2-orig/BDD/bdd/src/Makefile	2007-07-02 20:07:41.000000000 +0000
+++ pvs4.2-bddp/BDD/bdd/src/Makefile	2009-03-24 18:49:23.000000000 +0000
@@ -11,9 +11,9 @@
 # specify appropriate C compiler flags here:
 #CFLAGS=  -Aa -D_POSIX_SOURCE $(INCLUDES)
 #CFLAGS= -D_POSIX_SOURCE $(INCLUDES)
-CFLAGS= -g -O $(INCLUDES)
-XCFLAGS= -O
-XLDFLAGS=-s
+CFLAGS= -march=core2 -g -Wall -O2 -D_FORTIFY_SOURCE=2 -pipe $(INCLUDES)
+XCFLAGS= 
+XLDFLAGS=
 
 obj= bdd_factor.o bdd.o bdd_quant.o bdd_fns.o bdd_vfns.o appl.o y.tab.o \
      lex.yy.o main.o
@@ -26,23 +26,24 @@
 
 .c.o : ; $(CC) ${XCFLAGS} ${CFLAGS} -c $*.c
 
-bdd_factor.o : bdd_factor.c bdd_factor.h
-bdd.o : bdd.c bdd.h bdd_extern.h
-bdd_fns.o : bdd_fns.c bdd_fns.h bdd.h bdd_extern.h
-bdd_quant.o : bdd_quant.c bdd_fns.h bdd.h bdd_extern.h
-bdd_vfns.o : bdd_vfns.c bdd_vfns.h bdd_fns.h bdd.h bdd_extern.h
-appl.o : appl.c appl.h bdd_fns.h bdd.h bdd_extern.h
-main.o : main.c appl.h bdd_fns.h bdd.h bdd_extern.h
-y.tab.c : yacc.y bdd_fns.h bdd.h bdd_extern.h
+bdd_factor.o : bdd_factor.c bdd_factor.h bdd.h bdd_extern.h bdd_list.h
+bdd.o : bdd.c bdd.h bdd_extern.h bdd_list.h
+bdd_fns.o : bdd_fns.c bdd_fns.h bdd.h bdd_extern.h bdd_list.h bdd_quant.h
+bdd_quant.o : bdd_quant.c bdd_fns.h bdd.h bdd_extern.h bdd_list.h bdd_quant.h
+bdd_vfns.o : bdd_vfns.c bdd_vfns.h bdd_fns.h bdd.h bdd_extern.h bdd_list.h \
+  bdd_quant.h
+appl.o : appl.c appl.h bdd_fns.h bdd.h bdd_extern.h bdd_list.h bdd_quant.h
+main.o : main.c appl.h bdd.h bdd_extern.h bdd_factor.h bdd_fns.h bdd_list.h \
+  bdd_quant.h bdd_vfns.h
+y.tab.h : y.tab.c
+y.tab.c : yacc.y
 	# Don't worry about the 1 shift/reduce conflicts!
 	yacc -d yacc.y
-y.tab.h : yacc.y
-	yacc -d yacc.y
-	# Don't worry about the 1 shift/reduce conflicts!
-y.tab.o : y.tab.c bdd_fns.h bdd.h bdd_extern.h
+y.tab.o : y.tab.c y.tab.h appl.h bdd.h bdd_extern.h bdd_fns.h bdd_list.h \
+  bdd_quant.h bdd_vfns.h
 lex.yy.c : lex.l
-	lex lex.l
-lex.yy.o : lex.yy.c y.tab.h bdd.h bdd_extern.h
+	lex -l lex.l
+lex.yy.o : lex.yy.c y.tab.h bdd.h bdd_extern.h bdd_list.h
 	$(CC) -c ${CFLAGS} -w lex.yy.c
 
 clean : 
diff -Naur pvs4.2-orig/BDD/bdd/src/template.c pvs4.2-bddp/BDD/bdd/src/template.c
--- pvs4.2-orig/BDD/bdd/src/template.c	2007-07-02 20:07:41.000000000 +0000
+++ pvs4.2-bddp/BDD/bdd/src/template.c	2009-03-24 18:49:23.000000000 +0000
@@ -51,7 +51,7 @@
 int main (int argc, char *argv[])
 {
   /* Declare some variables that will hold Boolean functions. */
-  BDDPTR f, g;
+  BDDPTR f;
   BDDPTR a, b, c, d;
   BDDPTR tmp1, tmp2, tmp3;
 
@@ -227,4 +227,5 @@
   fprintf (stdout, "Quitting the BDD Package.\n");
   bdd_quit ();
   bdd_print_stats (stdout);
+  return EXIT_SUCCESS;
 }
diff -Naur pvs4.2-orig/BDD/bdd/src/yacc.y pvs4.2-bddp/BDD/bdd/src/yacc.y
--- pvs4.2-orig/BDD/bdd/src/yacc.y	2007-07-02 20:07:41.000000000 +0000
+++ pvs4.2-bddp/BDD/bdd/src/yacc.y	2009-03-24 18:49:23.000000000 +0000
@@ -99,6 +99,7 @@
 extern void action (BDDPTR *F);
 extern void parse_complete (void);
 
+int yylex (void);
 void yyerror (char *format, ...);
 void yywarning (char *format, ...);
 
diff -Naur pvs4.2-orig/BDD/bdd/utils/alloc.c pvs4.2-bddp/BDD/bdd/utils/alloc.c
--- pvs4.2-orig/BDD/bdd/utils/alloc.c	2007-07-02 20:07:41.000000000 +0000
+++ pvs4.2-bddp/BDD/bdd/utils/alloc.c	2009-03-24 18:49:23.000000000 +0000
@@ -101,10 +101,7 @@
 {
   long nr_bytes = nr_elems * bytes_per_elem;
   void *p = MA_Malloc (nr_bytes, r, fn, ln);
-  char *q = (char *) p;
-
-  while (nr_bytes-- > 0) *q++ = '\0';
-  return p;
+  return memset(p, 0, nr_bytes);
 }
 
 #if COMMENT
diff -Naur pvs4.2-orig/BDD/bdd/utils/alloc.h pvs4.2-bddp/BDD/bdd/utils/alloc.h
--- pvs4.2-orig/BDD/bdd/utils/alloc.h	2007-07-02 20:07:41.000000000 +0000
+++ pvs4.2-bddp/BDD/bdd/utils/alloc.h	2009-03-24 18:49:23.000000000 +0000
@@ -29,7 +29,7 @@
 		     const char* fn, long ln);
 
 #ifdef HAVE_ALLOCA
-extern void *alloca ();
+#include <alloca.h>
 #endif
 
 /* Allocates n consecutive bytes, returns pointer of type. */
diff -Naur pvs4.2-orig/BDD/bdd/utils/general.h pvs4.2-bddp/BDD/bdd/utils/general.h
--- pvs4.2-orig/BDD/bdd/utils/general.h	2007-07-02 20:07:41.000000000 +0000
+++ pvs4.2-bddp/BDD/bdd/utils/general.h	2009-03-24 18:49:23.000000000 +0000
@@ -30,6 +30,13 @@
 /* Number of bits in a Nat: */
 #define NAT_BIT			32
 
+/* Whether we are compiling for a 64-bit machine */
+#if LONG_MAX == 9223372036854775807L
+#define BITS64			1
+#else
+#define BITS64			0
+#endif
+
 /* What's the max unsigned integer value that fits in `n' bits: */
 #define UBITS_MAX(n)		(~(-1 << (n)))
 
@@ -77,15 +84,9 @@
 /* TYPE DEFINITIONS                                                         */
 /* ------------------------------------------------------------------------ */
 
-/* Xlib.h seems to define this! */
-#ifdef Bool
-#undef Bool
-#endif
-
 typedef   signed char		TinyInt;
 typedef    short int		SmallInt;
 typedef          int		Int;
-typedef unsigned char		Bool;
 typedef unsigned char		Byte;
 typedef unsigned char		TinyNat;
 typedef unsigned short int	SmallNat;
diff -Naur pvs4.2-orig/BDD/bdd/utils/hash.c pvs4.2-bddp/BDD/bdd/utils/hash.c
--- pvs4.2-orig/BDD/bdd/utils/hash.c	2007-07-02 20:07:41.000000000 +0000
+++ pvs4.2-bddp/BDD/bdd/utils/hash.c	2009-03-24 18:49:23.000000000 +0000
@@ -290,7 +290,7 @@
   for (i = 0; i < /*old*/ old_size; i++, entryp++)
     if (*entryp) {
       /* Entry i is occupied; insert it in new table: */
-      insert_var = (int) INSERT;
+      insert_var = INSERT;
       /* lookup_1 returns index of this entry in tab: */
       newi = lookup_1 (tab, *entryp, &insert_var);
       /* Call user supplied function to account for change: */
@@ -440,9 +440,12 @@
   entry.keylen = len;
   entry.info   = info ? *info : NULL;
 
-  if (do_insert == LOOKUP || do_insert == INSERT)
+  if (do_insert == LOOKUP_PTR)
     /* No reporting back possible. */
-    insert_var = (int) do_insert;
+    insert_var = LOOKUP;
+  else if (do_insert == INSERT_PTR)
+    /* No reporting back possible. */
+    insert_var = INSERT;
   else {
     /* Assume do_insert holds address of int variable. */
     insert_var = *do_insert;
@@ -522,7 +525,7 @@
   do {
     sprintf (startp, "%d", gen_counter++);
     len = strlen (buf);
-    inserted = (int) INSERT;
+    inserted = INSERT;
     i = lookup (tab, buf, len, NULL, &inserted);
   } while (inserted == ALREADY_PRESENT);
 
@@ -591,9 +594,9 @@
   while (gets (s)) {
     lc++;
     if (lc & 1)
-      lookup (hashtab , s, strlen (s), NULL, INSERT);
+      lookup (hashtab , s, strlen (s), NULL, INSERT_PTR);
     else
-      lookup (hashtab2, s, strlen (s), NULL, INSERT);
+      lookup (hashtab2, s, strlen (s), NULL, INSERT_PTR);
   }
   print_hashtab (hashtab);
   print_hashtab (hashtab2);
diff -Naur pvs4.2-orig/BDD/bdd/utils/hash.h pvs4.2-bddp/BDD/bdd/utils/hash.h
--- pvs4.2-orig/BDD/bdd/utils/hash.h	2007-07-02 20:07:41.000000000 +0000
+++ pvs4.2-bddp/BDD/bdd/utils/hash.h	2009-03-24 18:49:23.000000000 +0000
@@ -40,7 +40,7 @@
 */
 #define ALLOW_REHASH
 
-/* Define this to allow for automatically use of a shadow table of indices.
+/* Define this to allow for automatic use of a shadow table of indices.
    This shadow table indirects lookups by always going through it to the
    real hash table.
    This is subordinate to ALLOW_REHASH, i.e. to be effective ALLOW_REHASH
@@ -98,8 +98,10 @@
 #define HASHTAB_SIZE(tab)	((tab) ? (tab)->size : 0)
 
 /* Useful symbols for values of do_insert in lookup (). */
-#define LOOKUP			((int *)0)
-#define INSERT			((int *)1)
+#define LOOKUP			0
+#define INSERT			1
+#define LOOKUP_PTR		((int *)LOOKUP)
+#define INSERT_PTR		((int *)INSERT)
 
 /* Symbols for values returned by do_insert in lookup (). */
 #define ALREADY_PRESENT		0
diff -Naur pvs4.2-orig/BDD/bdd/utils/list.c pvs4.2-bddp/BDD/bdd/utils/list.c
--- pvs4.2-orig/BDD/bdd/utils/list.c	2007-07-02 20:07:41.000000000 +0000
+++ pvs4.2-bddp/BDD/bdd/utils/list.c	2009-03-24 18:49:23.000000000 +0000
@@ -462,8 +462,15 @@
   q = LIST_FIRST(list2);
 
   while (p && q) {
-    int comp = comparison ? (*comparison)(ELEM_CONTENTS(p), ELEM_CONTENTS(q))
-      			  : (int) ELEM_CONTENTS(p) - (int) ELEM_CONTENTS(q);
+    int comp;
+    if (comparison)
+      comp = (*comparison)(ELEM_CONTENTS(p), ELEM_CONTENTS(q));
+    else if (ELEM_CONTENTS(p) > ELEM_CONTENTS(q))
+      comp = 1;
+    else if (ELEM_CONTENTS(p) < ELEM_CONTENTS(q))
+      comp = -1;
+    else
+      comp = 0;
 
     if (!comp) {		/* ==> p = q */
       if (remove_duplicates) {
diff -Naur pvs4.2-orig/BDD/bdd/utils/Makefile pvs4.2-bddp/BDD/bdd/utils/Makefile
--- pvs4.2-orig/BDD/bdd/utils/Makefile	2007-07-02 20:07:41.000000000 +0000
+++ pvs4.2-bddp/BDD/bdd/utils/Makefile	2009-03-24 18:49:23.000000000 +0000
@@ -26,7 +26,7 @@
 double.o : double.c double.h
 list.o : list.c list.h alloc.h
 hash.o : hash.c hash.h alloc.h
-alloc.o : alloc.c
+alloc.o : alloc.c alloc.h
 
 dag.o : dag.c dag.h dag_customize.h general.h
 tree.o : tree.c tree.h tree_customize.h general.h
diff -Naur pvs4.2-orig/BDD/ix86-MacOSX/Makefile pvs4.2-bddp/BDD/ix86-MacOSX/Makefile
--- pvs4.2-orig/BDD/ix86-MacOSX/Makefile	2007-07-02 20:07:41.000000000 +0000
+++ pvs4.2-bddp/BDD/ix86-MacOSX/Makefile	2009-03-24 18:49:24.000000000 +0000
@@ -2,8 +2,11 @@
 MU = ../mu/src
 UTILS = ../bdd/utils
 INCLUDES = -I/usr/include -I$(BDD) -I$(UTILS) -I$(MU)
+# MACOSX_DEPLOYMENT_TARGET and -weak_library are needed so that dylibs work
+# for both leopard and tiger
+MACOSX_DEPLOYMENT_TARGET=10.2
 LD = ld
-LDFLAGS = -bundle /usr/lib/bundle1.o -flat_namespace -undefined suppress -L./
+LDFLAGS = -bundle /usr/lib/bundle1.o -flat_namespace -undefined suppress -L./ -weak_library /usr/lib/libSystem.B.dylib
 CC = cc
 CFLAGS = -dynamic -DNDEBUG $(INCLUDES)
 XCFLAGS = -O
diff -Naur pvs4.2-orig/BDD/mu/src/lex.l pvs4.2-bddp/BDD/mu/src/lex.l
--- pvs4.2-orig/BDD/mu/src/lex.l	2007-07-02 20:07:41.000000000 +0000
+++ pvs4.2-bddp/BDD/mu/src/lex.l	2009-03-24 18:49:24.000000000 +0000
@@ -229,7 +229,7 @@
 /* unimportant white space or new_line */	}
 
 .						{
-	lexerr (ill_char_mess (yytchar));	}
+	lexerr (ill_char_mess (yytext[0]));	}
 
 %%
 
diff -Naur pvs4.2-orig/BDD/mu/src/Makefile pvs4.2-bddp/BDD/mu/src/Makefile
--- pvs4.2-orig/BDD/mu/src/Makefile	2007-07-02 20:07:41.000000000 +0000
+++ pvs4.2-bddp/BDD/mu/src/Makefile	2009-03-24 18:49:24.000000000 +0000
@@ -1,8 +1,8 @@
 # Copyright (c) 1992-1995 G. Janssen
 
 BIN=$(HOME)/bin
-UTILS=../utils
-BDD=../bdd/src
+UTILS=../../bdd/utils
+BDD=../../bdd/src
 
 INCLUDES   = -I$(BDD) -I$(UTILS)
 
@@ -30,7 +30,7 @@
 	yacc -d yacc.y
 y.tab.o : y.tab.c mu.h
 lex.yy.c : lex.l mu.h
-	lex lex.l
+	lex -l lex.l
 lex.yy.o : lex.yy.c y.tab.h mu.h
 	$(CC) ${CFLAGS} -w -c lex.yy.c
 
diff -Naur pvs4.2-orig/BDD/mu/src/mu.c pvs4.2-bddp/BDD/mu/src/mu.c
--- pvs4.2-orig/BDD/mu/src/mu.c	2007-09-06 18:49:37.000000000 +0000
+++ pvs4.2-bddp/BDD/mu/src/mu.c	2009-03-24 18:49:24.000000000 +0000
@@ -450,7 +450,7 @@
 /* Used in print_list. */
 static void print_var (FILE *fp, void *bdd_idx)
 {
-  fputs (B_VAR_NAME (BDD_IDX_2_VAR_ID ((int) bdd_idx)), fp);
+  fputs (B_VAR_NAME (BDD_IDX_2_VAR_ID ((int) (long) bdd_idx)), fp);
 }
 
 /* ------------------------------------------------------------------------ */
@@ -667,8 +667,8 @@
     int x = PHV_ID_2_BDD_IDX (  i);
     int y = PHV_ID_2_BDD_IDX (n+i);
 
-    x_list    = append_cont ((void *) x, x_list);
-    y_list    = append_cont ((void *) y, y_list);
+    x_list    = append_cont ((void *) (long) x, x_list);
+    y_list    = append_cont ((void *) (long) y, y_list);
     x_bdds[i] = bdd_create_var (x);
 
     /* For a quick substitute it would be nice to have the x vars close
@@ -961,7 +961,7 @@
 
   i = 0;
   FOR_EACH_LIST_ELEM (vars, elem) {
-    int x = (int) ELEM_CONTENTS (elem);
+    int x = (int) (long) ELEM_CONTENTS (elem);
     int d = PHV_ID_2_BDD_IDX (i);
 
     d_bdds[i] = bdd_create_var (d);
@@ -979,7 +979,7 @@
   if (mu_debug) {
     i = 0;
     FOR_EACH_LIST_ELEM (vars, elem) {
-      int x = (int) ELEM_CONTENTS (elem);
+      int x = (int) (long) ELEM_CONTENTS (elem);
       int d = PHV_ID_2_BDD_IDX (i);
 
       fprintf (stderr, "/* %s (rank:%d) <- $%d (rank:%d) */\n", 
@@ -1185,12 +1185,12 @@
       bdd_print_as_sum_of_cubes (stderr, args[i], 0);
       bdd_set_output_string (BDD_END_S, str);
 
-      bdd_idxs = append_cont ((void *) PHV_ID_2_BDD_IDX (i), bdd_idxs);
+      bdd_idxs = append_cont ((void *) (long) PHV_ID_2_BDD_IDX (i), bdd_idxs);
     }
   }
   else
     for (i = 0; i < nr_args; i++)
-      bdd_idxs = append_cont ((void *) PHV_ID_2_BDD_IDX (i), bdd_idxs);
+      bdd_idxs = append_cont ((void *) (long) PHV_ID_2_BDD_IDX (i), bdd_idxs);
 
   R = bdd_subst_par (args, bdd_idxs, t);
   free_list (bdd_idxs, 0);
@@ -1205,10 +1205,10 @@
 static LIST mu_varids_to_bdd_indices_aux (LIST vars)
 {
   FOR_EACH_LIST_ELEM (vars, elem) {
-    int var_id = (int) ELEM_CONTENTS (elem);
+    int var_id = (int) (long) ELEM_CONTENTS (elem);
     int bdd_idx = VAR_ID_2_BDD_IDX (var_id);
 
-    ELEM_CONTENTS (elem) = (void *) bdd_idx;
+    ELEM_CONTENTS (elem) = (void *) (long) bdd_idx;
   } END_FOR_EACH_LIST_ELEM;
 
   return vars;
@@ -1540,7 +1540,7 @@
 {
   union formulaptr info = { NULL };
 
-  lookup (signature->table, name, strlen (name), &info.voidptr, LOOKUP);
+  lookup (signature->table, name, strlen (name), &info.voidptr, LOOKUP_PTR);
 
   return info.formulaptr;
 }
@@ -1716,7 +1716,7 @@
   int index;
   int flag;
 
-  flag = (int) INSERT;
+  flag = INSERT;
   index = lookup (Ip->table, name, strlen (name), NULL, &flag);
   if (flag == INDEED_INSERTED) {
     Term  T = CALLOC_STRUCT (_Term);
@@ -1748,7 +1748,7 @@
     fflush (stdout);
   }
 
-  flag = (int) INSERT;
+  flag = INSERT;
   index = lookup (Ip->table, name, strlen (name), NULL, &flag);
   if (flag == INDEED_INSERTED) {
     Term  T = CALLOC_TERM ();
@@ -1781,7 +1781,7 @@
 
       FOR_EACH_LIST_ELEM (args, elem) {
 	Formula  argi = (Formula) ELEM_CONTENTS (elem);
-	int     lvari = (int) ELEM_CONTENTS (lvars);
+	int     lvari = (int) (long) ELEM_CONTENTS (lvars);
 
 	if (F_TYPE (argi) != MU_B_VAR || F_VAR (argi) != lvari)
 	  /* vi != argi */
@@ -1849,7 +1849,7 @@
       var_id = mu_check_bool_var (buf);
 
       /* Create list of var id's for L <varid's> . */
-      vars = append_cont ((void *) var_id, vars);
+      vars = append_cont ((void *) (long) var_id, vars);
       /* Add as Formula to args: */
       args = append_cont ((void *) B_VAR_INFO (var_id), args);
     }
@@ -2026,7 +2026,7 @@
   _TRUE_TERM.arity   = MU_ANY_ARITY;
 
   /* We do not use entry nr. 0: */
-  lookup (signature->table, "", 0, NULL, INSERT);
+  lookup (signature->table, "", 0, NULL, INSERT_PTR);
 
   /* Change style of bdd_sum_of_cubes printing: */
   bdd_set_output_string (BDD_BEG_S, "");
@@ -2118,7 +2118,7 @@
     int index;
     int flag;
 
-    flag = (int) INSERT;
+    flag = INSERT;
     index = lookup (signature->table, name, strlen (name), NULL, &flag);
     if (flag == INDEED_INSERTED) {
       Formula f = CALLOC_FORMULA ();
@@ -2144,7 +2144,7 @@
   int index;
   int flag;
 
-  flag = (int) INSERT;
+  flag = INSERT;
   index = lookup (signature->table, var, strlen (var), NULL, &flag);
   if (flag == INDEED_INSERTED) {
     Formula f = CALLOC_FORMULA ();
@@ -2169,7 +2169,7 @@
 */
 static int when_even (void *p)
 {
-  if (ODD ((int) p))
+  if (ODD ((int) (long) p))
     return 0;
   user_vars = append_cont (p, user_vars);
   return 1;
@@ -2260,7 +2260,7 @@
     LIST bdd_idxs = NULL_LIST;
 
     /* Get maximum place-holder BDD index: */
-    while ((idx = (int) pop_cont (&vars)) != 0)
+    while ((idx = (int) (long) pop_cont (&vars)) != 0)
       if (idx > max_idx) max_idx = idx;
     /* Here: vars == NULL_LIST */
 
@@ -2278,11 +2278,11 @@
       var_id   = mu_check_bool_var (buf);
 
       /* Create list of var id's for L <varid's> . */
-      vars     = append_cont ((void *) var_id, vars);
+      vars     = append_cont ((void *) (long) var_id, vars);
       /* vars as BDDs: */
       args[i]  = F_BDD (B_VAR_INFO (var_id));
       /* Create list of corresponding BDD indices: */
-      bdd_idxs = append_cont ((void *) PHV_ID_2_BDD_IDX (i), bdd_idxs);
+      bdd_idxs = append_cont ((void *) (long) PHV_ID_2_BDD_IDX (i), bdd_idxs);
     }
 
     /* Substitute lambda vars for place-holder vars in Term's BDD: */