diff -dur pvs-4.2.ORIG/BDD/bdd/draw/main.c pvs-4.2/BDD/bdd/draw/main.c
--- pvs-4.2.ORIG/BDD/bdd/draw/main.c 1999-01-06 12:36:48.000000000 -0700
+++ pvs-4.2/BDD/bdd/draw/main.c 2010-01-01 14:38:49.082596637 -0700
@@ -292,7 +292,7 @@
aux_table = make_hashtab (0);
/* bdd_sizeof_user_data = sizeof (XYPOS);*/
- bdd_init ();
+ BDD_bdd_init ();
/* Create the dummy 0 var: */
/* bdd_free (bdd_create_var_last ());*/
diff -dur pvs-4.2.ORIG/BDD/bdd/src/bdd.c pvs-4.2/BDD/bdd/src/bdd.c
--- pvs-4.2.ORIG/BDD/bdd/src/bdd.c 2009-10-04 13:25:53.000000000 -0600
+++ pvs-4.2/BDD/bdd/src/bdd.c 2010-01-01 14:55:36.176596416 -0700
@@ -780,7 +780,7 @@
Depending on the use of complemented edges in the BDDs there exist
either 2 constant nodes or 3.
*/
-int bdd_size (BDDPTR f)
+int BDD_bdd_size (BDDPTR f)
{
node_counter = 0;
if (!BDD_VOID_P (f)) {
@@ -3162,7 +3162,7 @@
print_computed_table_stats (fp);
}
-void bdd_init (void)
+void BDD_bdd_init (void)
{
/* Guard against multiple initialisations: */
if (BDD_PACKAGE_INITIALIZED) {
@@ -3562,7 +3562,7 @@
return BDD_VOID_P (f) ? -1 : BDD_RANK (f);
}
-BDDPTR bdd_then (BDDPTR f)
+BDDPTR BDD_bdd_then (BDDPTR f)
{
BDDPTR R = BDD_COFACTOR_POS (f);
@@ -3570,7 +3570,7 @@
return R;
}
-BDDPTR bdd_else (BDDPTR f)
+BDDPTR BDD_bdd_else (BDDPTR f)
{
BDDPTR R = BDD_COFACTOR_NEG (f);
diff -dur pvs-4.2.ORIG/BDD/bdd/src/bdd_extern.h pvs-4.2/BDD/bdd/src/bdd_extern.h
--- pvs-4.2.ORIG/BDD/bdd/src/bdd_extern.h 2009-10-04 13:25:53.000000000 -0600
+++ pvs-4.2/BDD/bdd/src/bdd_extern.h 2010-01-01 14:54:39.558596780 -0700
@@ -90,7 +90,7 @@
/* ------------------------------------------------------------------------ */
/* Package administration related routines: */
-extern void bdd_init (void);
+extern void BDD_bdd_init (void);
extern void bdd_quit (void);
extern void bdd_print_stats (FILE *fp);
extern int bdd_gc (void);
@@ -155,8 +155,8 @@
extern int bdd_implies_taut (BDDPTR f, BDDPTR g);
extern BDDPTR bdd_nand (BDDPTR f, BDDPTR g);
extern BDDPTR bdd_invert_input_top (BDDPTR f);
-extern BDDPTR bdd_then (BDDPTR f);
-extern BDDPTR bdd_else (BDDPTR f);
+extern BDDPTR BDD_bdd_then (BDDPTR f);
+extern BDDPTR BDD_bdd_else (BDDPTR f);
extern BDDPTR bdd_constrain (BDDPTR f, BDDPTR c);
extern BDDPTR bdd_restrict (BDDPTR f, BDDPTR c);
@@ -169,7 +169,7 @@
extern BDDPTR bdd_top_var (BDDPTR f);
extern int bdd_top_var_id (BDDPTR f);
extern int bdd_top_var_rank (BDDPTR f);
-extern int bdd_size (BDDPTR f);
+extern int BDD_bdd_size (BDDPTR f);
extern int bdd_depth (BDDPTR f);
extern int bdd_size_vec (BDDPTR *f_vec, int size);
extern int bdd_size_ceil (BDDPTR f, int ceiling);
diff -dur pvs-4.2.ORIG/BDD/bdd/src/main.c pvs-4.2/BDD/bdd/src/main.c
--- pvs-4.2.ORIG/BDD/bdd/src/main.c 2008-12-15 00:50:28.000000000 -0700
+++ pvs-4.2/BDD/bdd/src/main.c 2010-01-01 14:49:11.489721954 -0700
@@ -90,7 +90,7 @@
/* Note: we don't count the dummy 0 variable! */
fprintf (stdout, "/* Size: %d, (%s minterms, %s X terms, %d vars), Depth: %d, Alive: %d */\n",
- bdd_size (f),
+ BDD_bdd_size (f),
D_sprintf (buf, bdd_count_sat_assignments (f, BDD_0), 0),
D_sprintf (buf2, bdd_count_X_terms (f), 0),
bdd_nr_vars,
@@ -316,7 +316,7 @@
/* if (!_setjmp (Context))*/
if (1) {
- bdd_init ();
+ BDD_bdd_init ();
current_interface = bdd_get_factor_interface ();
/* current_interface->out = stdout;*/
@@ -388,7 +388,7 @@
#ifdef COMMENT
/* Just for testing purposes: */
bdd_quit ();
- bdd_init ();
+ BDD_bdd_init ();
free_hashtab (var_table);
var_table = make_hashtab (3);
/* Let's not use entry nr. 0 for fun: */
diff -dur pvs-4.2.ORIG/BDD/bdd/src/template.c pvs-4.2/BDD/bdd/src/template.c
--- pvs-4.2.ORIG/BDD/bdd/src/template.c 2008-12-15 00:50:28.000000000 -0700
+++ pvs-4.2/BDD/bdd/src/template.c 2010-01-01 14:43:20.321596917 -0700
@@ -61,7 +61,7 @@
*/
/* This is a must! And should also be done prior to any BDD operation. */
- bdd_init ();
+ BDD_bdd_init ();
fprintf (stdout, "BDD Package Initialised.\n");
bdd_print_stats (stdout);
diff -dur pvs-4.2.ORIG/BDD/bdd-ld-table pvs-4.2/BDD/bdd-ld-table
--- pvs-4.2.ORIG/BDD/bdd-ld-table 2008-12-15 00:50:28.000000000 -0700
+++ pvs-4.2/BDD/bdd-ld-table 2010-01-01 14:52:28.921596712 -0700
@@ -25,8 +25,8 @@
bdd___bdd_lit_p = bdd_lit_p ;
bdd___bdd_cofactor_pos_ = bdd_cofactor_pos_ ;
bdd___bdd_cofactor_neg_ = bdd_cofactor_neg_ ;
-bdd___bdd_size = bdd_size ;
-bdd___bdd_init = bdd_init ;
+bdd___BDD_bdd_size = BDD_bdd_size ;
+bdd___BDD_bdd_init = BDD_bdd_init ;
bdd___bdd_free = bdd_free ;
bdd___bdd_gc = bdd_gc ;
bdd___bdd_ite = bdd_ite ;
@@ -57,8 +57,8 @@
bdd___bdd_1 = bdd_1 ;
bdd___bdd_X = bdd_X ;
bdd___bdd_assign = bdd_assign ;
-bdd___bdd_then = bdd_then ;
-bdd___bdd_else = bdd_else ;
+bdd___BDD_bdd_then = BDD_bdd_then ;
+bdd___BDD_bdd_else = BDD_bdd_else ;
bdd___bdd_apply = bdd_apply ;
bdd___bdd_constrain = bdd_constrain ;
/* bdd___bdd_sum_of_cubes = bdd_sum_of_cubes ; */
diff -dur pvs-4.2.ORIG/BDD/bdd.lisp pvs-4.2/BDD/bdd.lisp
--- pvs-4.2.ORIG/BDD/bdd.lisp 2008-12-15 00:50:28.000000000 -0700
+++ pvs-4.2/BDD/bdd.lisp 2010-01-01 14:37:29.132596592 -0700
@@ -89,7 +89,7 @@
(selected-sforms (select-seq sforms fnums)))
(cond ((null selected-sforms)
(values 'X nil nil))
- (t (unless *bdd-initialized* (bdd_init))
+ (t (unless *bdd-initialized* (BDD_bdd_init))
(if dynamic-ordering?
(set_bdd_do_dynamic_ordering 1)
(set_bdd_do_dynamic_ordering 0))
@@ -119,7 +119,7 @@
(defvar *ignore-boolean-equalities?* nil)
(defun bdd-simplify (expr &optional ignore-boolean-equalities?)
- (unless *bdd-initialized* (bdd_init))
+ (unless *bdd-initialized* (BDD_bdd_init))
(let* ((*pvs-bdd-hash* (make-pvs-hash-table))
(*bdd-pvs-hash* (make-hash-table))
(*recognizer-forms-alist* nil)
diff -dur pvs-4.2.ORIG/BDD/bdd-sbcl.lisp pvs-4.2/BDD/bdd-sbcl.lisp
--- pvs-4.2.ORIG/BDD/bdd-sbcl.lisp 2009-07-31 02:00:41.000000000 -0600
+++ pvs-4.2/BDD/bdd-sbcl.lisp 2010-01-01 14:52:13.539596694 -0700
@@ -207,16 +207,16 @@
;;; void bdd_traverse_pre (register BDDPTR v, void (*pre_action)(BDDPTR))
;;; void bdd_traverse_post (register BDDPTR v, void (*post_action)(BDDPTR))
-;;; int bdd_size (BDDPTR f)
-(sb-alien:define-alien-routine ("bdd___bdd_size" bdd_size)
+;;; int BDD_bdd_size (BDDPTR f)
+(sb-alien:define-alien-routine ("bdd___BDD_bdd_size" BDD_bdd_size)
(integer 32)
(f (* t)))
;;; int bdd_size_vec (BDDPTR *f_vec, int size)
;;; int bdd_size_ceil (BDDPTR f, int ceiling)
-;;; void bdd_init (void)
-(sb-alien:define-alien-routine ("bdd___bdd_init" bdd_init)
+;;; void BDD_bdd_init (void)
+(sb-alien:define-alien-routine ("bdd___BDD_bdd_init" BDD_bdd_init)
sb-alien:void)
;;; void bdd_free (BDDPTR f)
@@ -400,12 +400,12 @@
;;; BDDPTR bdd_top_var (BDDPTR f)
;;; int bdd_top_var_rank (BDDPTR f)
;;; BDDPTR bdd_then (BDDPTR f)
-(sb-alien:define-alien-routine ("bdd___bdd_then" bdd_then)
+(sb-alien:define-alien-routine ("bdd___BDD_bdd_then" BDD_bdd_then)
(* t)
(f (* t)))
;;; BDDPTR bdd_else (BDDPTR f)
-(sb-alien:define-alien-routine ("bdd___bdd_else" bdd_else)
+(sb-alien:define-alien-routine ("bdd___BDD_bdd_else" BDD_bdd_else)
(* t)
(f (* t)))
@@ -552,4 +552,4 @@
(defun bdd-interrupted? ()
(not (zerop bdd_interrupted)))
-(bdd_init)
+(BDD_bdd_init)
diff -dur pvs-4.2.ORIG/BDD/bdd_table.c pvs-4.2/BDD/bdd_table.c
--- pvs-4.2.ORIG/BDD/bdd_table.c 2008-12-15 00:50:28.000000000 -0700
+++ pvs-4.2/BDD/bdd_table.c 2010-01-01 14:52:50.567596941 -0700
@@ -61,9 +61,9 @@
return (BDDPTR) bdd_cofactor_neg_ (f);
}
-int bdd___bdd_size (BDDPTR f) {return bdd_size (f);}
+int bdd___BDD_bdd_size (BDDPTR f) {return BDD_bdd_size (f);}
-void bdd___bdd_init (void) {bdd_init ();}
+void bdd___BDD_bdd_init (void) {BDD_bdd_init ();}
void bdd___bdd_free (BDDPTR f) {bdd_free (f);}
@@ -128,9 +128,9 @@
BDDPTR bdd___bdd_assign (BDDPTR f) {return bdd_assign (f);}
-BDDPTR bdd___bdd_then (BDDPTR f) {return bdd_then (f);}
+BDDPTR bdd___BDD_bdd_then (BDDPTR f) {return BDD_bdd_then (f);}
-BDDPTR bdd___bdd_else (BDDPTR f) {return bdd_else (f);}
+BDDPTR bdd___BDD_bdd_else (BDDPTR f) {return BDD_bdd_else (f);}
BDDPTR bdd___bdd_apply (BDDPTR (*f)(BDDPTR,BDDPTR), BDDPTR a, BDDPTR b)
{return bdd_apply (f, a, b);}
diff -dur pvs-4.2.ORIG/BDD/mu/src/main.c pvs-4.2/BDD/mu/src/main.c
--- pvs-4.2.ORIG/BDD/mu/src/main.c 1998-12-31 13:30:32.000000000 -0700
+++ pvs-4.2/BDD/mu/src/main.c 2010-01-01 14:43:32.838597226 -0700
@@ -173,7 +173,7 @@
return 1;
}
- bdd_init ();
+ BDD_bdd_init ();
mu_init ();
if (optind == argc)
diff -dur pvs-4.2.ORIG/BDD/mu/src/mu.c pvs-4.2/BDD/mu/src/mu.c
--- pvs-4.2.ORIG/BDD/mu/src/mu.c 2009-10-04 13:25:53.000000000 -0600
+++ pvs-4.2/BDD/mu/src/mu.c 2010-01-01 14:49:32.575722103 -0700
@@ -753,7 +753,7 @@
int size_Tkplus1;
int size_Front;
- size_Tkplus1 = bdd_size (Tkplus1);
+ size_Tkplus1 = BDD_bdd_size (Tkplus1);
if (mu_use_restrict)
Front = bdd_restrict (Tkplus1, Tknot);
@@ -763,7 +763,7 @@
else
Front = bdd_and (Tkplus1, Tknot);
- size_Front = bdd_size (Front);
+ size_Front = BDD_bdd_size (Front);
bdd_free (Tknot);
@@ -928,7 +928,7 @@
/* D_sprintf (buf, bdd_count_sat_assignments (R, Domain), 0); */
fprintf (stdout, "Reachable took %.2f msec (%u BDD nodes).\n",
(clock () - start_t) / CLOCKS_PER_MSEC,
- bdd_size (R));
+ BDD_bdd_size (R));
fflush (stdout);
bdd_free (Domain);
}
@@ -1954,7 +1954,7 @@
R_VAR_VALUE (var) = R = mu_interpret_term (T, Ip, NULL);
if (mu_verbose) {
- fprintf (stdout, "done (%d BDD nodes).\n", bdd_size (R));
+ fprintf (stdout, "done (%d BDD nodes).\n", BDD_bdd_size (R));
fflush (stdout);
}
@@ -1991,7 +1991,7 @@
if (mu_verbose) {
fprintf (stdout, "Definition for `%s' took %.2f msec (%d BDD nodes).\n",
name, (clock () - start_t) / CLOCKS_PER_MSEC,
- bdd_size (R));
+ BDD_bdd_size (R));
fflush (stdout);
}
}
diff -dur pvs-4.2.ORIG/BDD/mu/src/yacc.y pvs-4.2/BDD/mu/src/yacc.y
--- pvs-4.2.ORIG/BDD/mu/src/yacc.y 2007-04-01 02:10:09.000000000 -0600
+++ pvs-4.2/BDD/mu/src/yacc.y 2010-01-01 14:49:43.862504601 -0700
@@ -166,7 +166,7 @@
R = mu_interpret_formula ($1, Ip, NULL);
bdd_print_as_sum_of_cubes (stdout, R, 0);
if (mu_verbose)
- fprintf (stdout, "Formula amounts to %d BDD nodes.\n", bdd_size (R));
+ fprintf (stdout, "Formula amounts to %d BDD nodes.\n", BDD_bdd_size (R));
bdd_free (R);
mu_free_formula ($1);
}
diff -dur pvs-4.2.ORIG/BDD/mu_interface.c pvs-4.2/BDD/mu_interface.c
--- pvs-4.2.ORIG/BDD/mu_interface.c 2009-10-04 13:25:53.000000000 -0600
+++ pvs-4.2/BDD/mu_interface.c 2010-01-01 14:47:29.920596857 -0700
@@ -258,7 +258,7 @@
mu_free_formula(fml);
/* bdd_print_as_sum_of_cubes (stdout, R,0) ; */
if (mu_verbose) {
- fprintf (stdout, "Formula amounts to %d BDD nodes.\n", bdd_size (R));
+ fprintf (stdout, "Formula amounts to %d BDD nodes.\n", BDD_bdd_size (R));
fflush (stdout);
}
return R;
diff -dur pvs-4.2.ORIG/BDD/mu.lisp pvs-4.2/BDD/mu.lisp
--- pvs-4.2.ORIG/BDD/mu.lisp 2009-12-29 01:45:35.000000000 -0700
+++ pvs-4.2/BDD/mu.lisp 2010-01-01 14:43:48.194596776 -0700
@@ -59,7 +59,7 @@
(defun run-musimp (ps fnums dynamic-ordering? irredundant? verbose?)
- (bdd_init)
+ (BDD_bdd_init)
;; Need to look at this, or somehow it gets a nonzero value
(bdd-interrupted?)
(mu_init)
diff -dur pvs-4.2.ORIG/pvs.system pvs-4.2/pvs.system
--- pvs-4.2.ORIG/pvs.system 2010-01-01 14:32:41.874471788 -0700
+++ pvs-4.2/pvs.system 2010-01-01 14:44:02.007596582 -0700
@@ -260,7 +260,7 @@
#+lucid (precompile-generic-functions)
#+lcl4.1 (clos::flush-pv-caches)
#-(or cmu sbcl)
- (pvs::bdd_init)
+ (pvs::BDD_bdd_init)
(when *load-pvs-prelude*
(pvs::load-prelude))
#+allegro
diff -dur pvs-4.2.ORIG/src/pvs.lisp pvs-4.2/src/pvs.lisp
--- pvs-4.2.ORIG/src/pvs.lisp 2009-10-01 03:25:19.000000000 -0600
+++ pvs-4.2/src/pvs.lisp 2010-01-01 14:44:27.400721511 -0700
@@ -115,7 +115,7 @@
#+cmu (fmakunbound 'bdd_cofactor_neg_)
#+cmu (lf "bdd-cmu") #+sbcl (lf "bdd-sbcl")
#+cmu (lf "mu-cmu") #+sbcl (lf "mu-sbcl")
- (bdd_init)
+ (BDD_bdd_init)
#+cmu (lf "dfa-foreign-cmu") #+sbcl (lf "dfa-foreign-sbcl"))
(setq *started-with-minus-q*
(or dont-load-user-lisp
diff -dur pvs-4.2.ORIG/src/WS1S/ix86_64-Linux/Makefile pvs-4.2/src/WS1S/ix86_64-Linux/Makefile
--- pvs-4.2.ORIG/src/WS1S/ix86_64-Linux/Makefile 2008-12-15 01:43:07.000000000 -0700
+++ pvs-4.2/src/WS1S/ix86_64-Linux/Makefile 2010-01-01 14:36:03.189477043 -0700
@@ -14,15 +14,7 @@
SHELL = /bin/sh
VPATH = ..:../mona/BDD:../mona/DFA:../mona/Mem
-obj = analyze.o prefix.o product.o \
- quotient.o basic.o external.o \
- makebasic.o minimize.o printdfa.o \
- project.o dfa.o \
- bdd.o bdd_double.o bdd_external.o \
- bdd_manager.o hash.o bdd_dump.o \
- bdd_trace.o bdd_cache.o \
- dlmalloc.o mem.o \
- ws1s_extended_interface.o
+obj = ws1s_table.o ws1s_extended_interface.o -lmonadfa
.SUFFIXES:
.SUFFIXES: .c .o
@@ -34,7 +26,7 @@
$(CC) $(XCFLAGS) ${CFLAGS} -c $< -o $@
ws1s.so : ${obj}
- $(LD) ../ws1s-ld-table $(LDFLAGS) -o ws1s.so ${obj}
+ $(CC) -shared $(CFLAGS) -o ws1s.so ${obj}
bdd.o: bdd.c bdd.h bdd_internal.h
bdd_double.o: bdd_double.c bdd.h bdd_internal.h
diff -dur pvs-4.2.ORIG/src/WS1S/ix86-Linux/Makefile pvs-4.2/src/WS1S/ix86-Linux/Makefile
--- pvs-4.2.ORIG/src/WS1S/ix86-Linux/Makefile 2006-09-04 18:29:55.000000000 -0600
+++ pvs-4.2/src/WS1S/ix86-Linux/Makefile 2010-01-01 14:35:19.105597056 -0700
@@ -14,15 +14,7 @@
SHELL = /bin/sh
VPATH = ..:../mona/BDD:../mona/DFA:../mona/Mem
-obj = analyze.o prefix.o product.o \
- quotient.o basic.o external.o \
- makebasic.o minimize.o printdfa.o \
- project.o dfa.o \
- bdd.o bdd_double.o bdd_external.o \
- bdd_manager.o hash.o bdd_dump.o \
- bdd_trace.o bdd_cache.o \
- dlmalloc.o mem.o \
- ws1s_extended_interface.o
+obj = ws1s_table.o ws1s_extended_interface.o -lmonadfa
.SUFFIXES:
.SUFFIXES: .c .o
@@ -34,7 +26,7 @@
$(CC) $(XCFLAGS) ${CFLAGS} -c $< -o $@
ws1s.so : ${obj}
- $(LD) ../ws1s-ld-table $(LDFLAGS) -o ws1s.so ${obj}
+ $(CC) -shared $(CFLAGS) -o ws1s.so ${obj}
bdd.o: bdd.c bdd.h bdd_internal.h
bdd_double.o: bdd_double.c bdd.h bdd_internal.h
diff -dur pvs-4.2.ORIG/src/WS1S/lisp/dfa.lisp pvs-4.2/src/WS1S/lisp/dfa.lisp
--- pvs-4.2.ORIG/src/WS1S/lisp/dfa.lisp 2006-11-02 02:06:48.000000000 -0700
+++ pvs-4.2/src/WS1S/lisp/dfa.lisp 2010-01-01 14:50:38.749596895 -0700
@@ -292,7 +292,7 @@
(defun number-of-states (a) (mona-dfa-ns (address a)))
(defun start-state (a) (mona-dfa-s (address a)))
-(defun number-of-bdd-nodes (a) (mona-bdd-size (dfa-bddm (address a))))
+(defun number-of-bdd-nodes (a) (bdd-size (dfa-bddm (address a))))
(defun number-of-transitions (a) (mona-transition-table-size (address a)))
diff -dur pvs-4.2.ORIG/src/WS1S/ws1s-ld-table pvs-4.2/src/WS1S/ws1s-ld-table
--- pvs-4.2.ORIG/src/WS1S/ws1s-ld-table 2006-11-06 13:14:58.000000000 -0700
+++ pvs-4.2/src/WS1S/ws1s-ld-table 2010-01-01 14:50:08.331477095 -0700
@@ -46,7 +46,7 @@
ws1s___dfaPrint = dfaPrint ;
ws1s___dfaPrintGraphviz = dfaPrintGraphviz ;
ws1s___dfaPrintVerbose = dfaPrintVerbose ;
-ws1s___bdd_size = mona_bdd_size ;
+ws1s___bdd_size = bdd_size ;
ws1s___dfaSetup = dfaSetup ;
ws1s___dfaAllocExceptions = dfaAllocExceptions ;
ws1s___dfaStoreException = dfaStoreException ;
diff -dur pvs-4.2.ORIG/src/WS1S/ws1s_table.c pvs-4.2/src/WS1S/ws1s_table.c
--- pvs-4.2.ORIG/src/WS1S/ws1s_table.c 2006-11-06 13:14:58.000000000 -0700
+++ pvs-4.2/src/WS1S/ws1s_table.c 2010-01-01 14:51:27.140473890 -0700
@@ -182,8 +182,8 @@
int (*ws1s___dfaPrintVerbose)(int) = dfaPrintVerbose;
-extern int mona_bdd_size (int);
-int (*ws1s___bdd_size)(int) = mona_bdd_size;
+extern int bdd_size (int);
+int (*ws1s___bdd_size)(int) = bdd_size;
extern int dfaSetup (int);
distrib
>
Fedora
>
13
>
i386
>
media
>
updates-src
>
by-pkgid
>
14136f842c46f58edd010f3cfe224ce6
>
files
>
9
