Commit 4579cc26 authored by Erwan Jahier's avatar Erwan Jahier

lurette 0.39 Thu, 07 Mar 2002 13:36:27 +0100 by jahier

Parent-Version:      0.38
Version-Log:

Use the new cudd interface based on camlidl (mlcuddidl).

Now, bdds do not leaks anymore.  Remove debugging stuff that was used
to track that problem.

Project-Description: Lurette
parent c3c5f045
......@@ -3,13 +3,13 @@
(Created-By-Prcs-Version 1 3 3)
(test/usager.env 439 1015408234 b/14_usager.env 1.3)
(doc/ocamldoc.sty 1380 1008328137 b/12_ocamldoc.s 1.1)
(source/env_state.ml 2795 1015408234 51_env_state. 1.12)
(source/env_state.ml 2871 1015504587 51_env_state. 1.13)
(source/graph.ml 1801 1015250295 14_graph.ml 1.4)
(source/util.ml 9430 1015250295 35_util.ml 1.12)
(source/wtree.ml 9644 1014051154 b/1_wtree.ml 1.8)
(source/solver.ml 18273 1015408234 39_solver.ml 1.13)
(source/solver.ml 14080 1015504587 39_solver.ml 1.14)
(source/command_line.ml 3971 1014048376 b/20_command_li 1.3)
(source/lurette.ml 11196 1015408234 12_lurette.ml 1.24)
(source/lurette.ml 11363 1015504587 12_lurette.ml 1.25)
(source/solver.mli 1059 1015250295 38_solver.mli 1.9)
(source/env.mli 2389 1015250295 15_env.mli 1.9)
(test/heater_float.rif.exp 1577 1015408234 b/30_heater_flo 1.1)
......@@ -25,7 +25,7 @@
(ID_EN_VRAC 2184 1002196285 0_ID_EN_VRAC 1.1)
(source/sim2chro.mli 1427 1015250295 b/23_sim2chro.m 1.3)
(doc/automata_format 0 1007379917 b/3_automata_f 1.1)
(source/eval.ml 7987 1015408234 49_eval.ml 1.8)
(source/eval.ml 7990 1015504587 49_eval.ml 1.9)
(source/gen_stubs.ml 33424 1015408234 24_generate_l 1.19)
(source/parse_env.ml 9431 1015408234 41_parse_env. 1.6)
(interface/TAGS 1956 1007380262 26_TAGS 1.3)
......@@ -37,7 +37,7 @@
(TAGS 9825 1007379917 21_TAGS 1.6)
(source/wtree.mli 2931 1015250295 b/0_wtree.mli 1.6)
(test/porte.env 879 1015408234 b/16_porte.env 1.2)
(source/env_state.mli 3644 1015408234 50_env_state. 1.10)
(source/env_state.mli 3698 1015504587 50_env_state. 1.11)
(source/rnumsolver.mli 1909 1015246213 b/26_rnumsolver 1.1)
(source/eval.mli 1665 1015408234 48_eval.mli 1.7)
(README 74 1011881677 10_README 1.2)
......@@ -51,12 +51,12 @@
(interface/Makefile 197 1008255910 25_Makefile 1.6)
(source/show_env.mli 765 1015250295 42_show_env.m 1.5)
(test/tram_simple.h 1746 1013519411 b/25_tram_simpl 1.1)
(Makefile 1776 1015246213 18_Makefile 1.21)
(Makefile 1756 1015504587 18_Makefile 1.22)
(test/vrai_tram.c 3060 1012914629 b/8_vrai_tram. 1.2)
(source/print.mli 597 1014048376 46_print.mli 1.5)
(source/graph.mli 1493 1015250295 13_graph.mli 1.6)
(test/heater_int.rif.exp 785 1015408234 b/28_heater_int 1.1)
(source/formula.ml 4618 1015408234 45_formula.ml 1.9)
(source/lurette.mli 433 1015250295 11_lurette.ml 1.11)
(source/print.ml 5524 1015250295 47_print.ml 1.9)
(source/print.ml 5525 1015504587 47_print.ml 1.10)
(test/vrai_tram.h 2468 1012914629 b/7_vrai_tram. 1.2)
......@@ -2,17 +2,17 @@ LURETTE_DIR = ..
OCAMLMAKEFILE = $(LURETTE_DIR)/OcamlMakefile
# OCAMLFLAGS = -noassert -unsafe
# OCAMLNCFLAGS = -inline 10
OCAMLFLAGS = -noassert -unsafe
OCAMLNCFLAGS = -inline 10
-include ./lurette.in
INCDIRS = /home/jahier/include
LIBDIRS = /home/jahier/lib /home/jahier/lib/ocaml
LIBDIRS = /home/jahier/lib
# Requires cudd and mldd to be installed!
LIBS = dd nums # mlpoly
CLIBS = dd_caml cudd mtr st epd util # libppl libpolyi
LIBS = nums # mlpoly
CLIBS = cudd_caml cuddaux cudd mtr st epd util # libppl libpolyi
USE_CAMLP4 = yes
......
;; -*- Prcs -*-
(Created-By-Prcs-Version 1 3 3)
(Project-Description "Lurette")
(Project-Version lurette 0 38)
(Parent-Version lurette 0 37)
(Project-Version lurette 0 39)
(Parent-Version lurette 0 38)
(Version-Log "
With this change, lurette is now able to handle numeric variables
over intervals !
Use the new cudd interface based on camlidl (mlcuddidl).
Now, bdds do not leaks anymore. Remove debugging stuff that was used
to track that problem.
")
(New-Version-Log "")
(Checkin-Time "Wed, 06 Mar 2002 10:50:34 +0100")
(Checkin-Time "Thu, 07 Mar 2002 13:36:27 +0100")
(Checkin-Login jahier)
(Populate-Ignore ())
(Project-Keywords)
......@@ -21,7 +23,7 @@ over intervals !
;; Sources files
(source/lurette.mli (lurette/11_lurette.ml 1.11 644))
(source/lurette.ml (lurette/12_lurette.ml 1.24 644))
(source/lurette.ml (lurette/12_lurette.ml 1.25 644))
(source/graph.mli (lurette/13_graph.mli 1.6 644))
(source/graph.ml (lurette/14_graph.ml 1.4 644))
......@@ -32,7 +34,7 @@ over intervals !
(source/util.ml (lurette/35_util.ml 1.12 644))
(source/solver.mli (lurette/38_solver.mli 1.9 644))
(source/solver.ml (lurette/39_solver.ml 1.13 644))
(source/solver.ml (lurette/39_solver.ml 1.14 644))
(source/rnumsolver.mli (lurette/b/26_rnumsolver 1.1 644))
(source/rnumsolver.ml (lurette/b/27_rnumsolver 1.2 644))
......@@ -47,13 +49,13 @@ over intervals !
(source/formula.ml (lurette/45_formula.ml 1.9 644))
(source/print.mli (lurette/46_print.mli 1.5 644))
(source/print.ml (lurette/47_print.ml 1.9 644))
(source/print.ml (lurette/47_print.ml 1.10 644))
(source/eval.mli (lurette/48_eval.mli 1.7 644))
(source/eval.ml (lurette/49_eval.ml 1.8 644))
(source/eval.ml (lurette/49_eval.ml 1.9 644))
(source/env_state.mli (lurette/50_env_state. 1.10 644))
(source/env_state.ml (lurette/51_env_state. 1.12 644))
(source/env_state.mli (lurette/50_env_state. 1.11 644))
(source/env_state.ml (lurette/51_env_state. 1.13 644))
(source/wtree.mli (lurette/b/0_wtree.mli 1.6 644))
(source/wtree.ml (lurette/b/1_wtree.ml 1.8 644))
......@@ -68,7 +70,7 @@ over intervals !
;; Make files
(OcamlMakefile (lurette/17_OcamlMakef 1.20 644))
(Makefile (lurette/18_Makefile 1.21 644))
(Makefile (lurette/18_Makefile 1.22 644))
(test/Makefile (../Makefile) :symlink)
(interface/Makefile (lurette/25_Makefile 1.6 644))
(make_lurette (lurette/27_make_luret 1.7 744))
......
......@@ -29,6 +29,7 @@ type env_stateT = {
mutable atomic_formula_to_index: ((formula, int) Hashtbl.t);
mutable index_to_atomic_formula: ((int, formula) Hashtbl.t);
mutable index_cpt: int;
mutable bdd_manager: Manager.t;
mutable bdd_tbl: (formula, Bdd.t) Hashtbl.t;
mutable snt: (Bdd.t, Util.sol_nb * Util.sol_nb) Hashtbl.t;
mutable current_nodes: node list list;
......@@ -51,6 +52,7 @@ let (env_state:env_stateT) = {
atomic_formula_to_index = Hashtbl.create 0 ;
index_to_atomic_formula = Hashtbl.create 0 ;
index_cpt = 0 ;
bdd_manager = Manager.make 10 10 0 0 0;
bdd_tbl = Hashtbl.create 0;
snt = Hashtbl.create 3;
current_nodes = [];
......
......@@ -48,6 +48,9 @@ type env_stateT = {
mutable index_cpt: int;
(** Counter used to create the index *)
mutable bdd_manager: Manager.t;
(** bdd state *)
mutable bdd_tbl: (formula, Bdd.t) Hashtbl.t;
(** Transforming a formula into a bdd is expensive, therefore
we store the result of this transformation in a table. *)
......
......@@ -199,6 +199,8 @@ and
| Ival(i) -> Ival(i)
| Fval(f) -> Fval(f)
(****************************************************************************)
(****************************************************************************)
......
......@@ -208,7 +208,7 @@ and
let local_var_name_and_type_list =
Util.sort_list_string_pair local_var_name_and_type_list_unsorted
in
(* Initialisation of the random engine *)
let seed =
if (options.user_seed = 0)
......@@ -250,14 +250,18 @@ and
rif options.display_local_var;
(* Initializing Dd's libs. *)
Dd.initialize 0 options.cudd_heap_init ;
Dd.disable_autoreorder ();
(* Dd.initialize 0 options.cudd_heap_init ; *)
(* env_state.bdd_manager <- Manager.make 10 10 0 0 0; *)
(* Dd.disable_autoreorder (); *)
Manager.disable_autodyn env_state.bdd_manager;
(* Initializing the solution number table *)
Hashtbl.add env_state.snt
(Bdd.dtrue ()) (Util.one_sol, Util.zero_sol);
(Bdd.dtrue env_state.bdd_manager) (Util.one_sol, Util.zero_sol);
Hashtbl.add env_state.snt
(Bdd.dfalse ()) (Util.zero_sol, Util.one_sol);
(Bdd.dfalse env_state.bdd_manager) (Util.zero_sol, Util.one_sol);
main_loop 1 s n p rif (Hashtbl.create 0) ;
......
......@@ -108,7 +108,7 @@ let (comb2: Bdd.t -> unit) =
(fun var -> print_string (var ^ " "))
(List.map
(fun index -> (Formula.formula_to_string (Env_state.index_to_atomic_formula index)))
(Bdd.int_of_support supp));
(Bdd.list_of_support supp));
print_string "\n" ;
flush stdout
......
......@@ -38,30 +38,30 @@ let rec (formula_to_bdd : formula -> Bdd.t) =
with Not_found ->
let bdd =
match f with
Not(f1) -> Bdd.dnot (formula_to_bdd f1)
Not(f1) -> Bdd.dnot (formula_to_bdd f1)
| Or(f1, f2) -> Bdd.dor (formula_to_bdd f1) (formula_to_bdd f2)
| And(f1, f2) -> Bdd.dand (formula_to_bdd f1) (formula_to_bdd f2)
| True -> Bdd.dtrue ()
| False -> Bdd.dfalse ()
| Bvar(vn) -> Bdd.var (Env_state.atomic_formula_to_index f)
| True -> Bdd.dtrue env_state.bdd_manager
| False -> Bdd.dfalse env_state.bdd_manager
| Bvar(vn) -> Bdd.ithvar env_state.bdd_manager (Env_state.atomic_formula_to_index f)
| Eq(e1, e2) ->
(* We transform [e1 = e2] into [e1 <= e2 ^ e1 >= e2] as the
numeric solver can not handle disequalities *)
( Bdd.dand
(Bdd.var (Env_state.atomic_formula_to_index (SupEq(e1, e2))))
(Bdd.var (Env_state.atomic_formula_to_index (InfEq(e1, e2)))) )
(Bdd.ithvar env_state.bdd_manager (Env_state.atomic_formula_to_index (SupEq(e1, e2))))
(Bdd.ithvar env_state.bdd_manager (Env_state.atomic_formula_to_index (InfEq(e1, e2)))) )
| Neq(e1, e2) ->
(* We transform [e1 <> e2] into [e1 < e2 ^ e1 > e2] as the
numeric solver can not handle disequalities *)
( Bdd.dand
(Bdd.var (Env_state.atomic_formula_to_index (Sup(e1, e2))))
(Bdd.var (Env_state.atomic_formula_to_index (Inf(e1, e2)))) )
| SupEq(e1, e2) -> Bdd.var (Env_state.atomic_formula_to_index f)
| Sup(e1, e2) -> Bdd.var (Env_state.atomic_formula_to_index f)
| InfEq(e1, e2) -> Bdd.var (Env_state.atomic_formula_to_index f)
| Inf(e1, e2) -> Bdd.var (Env_state.atomic_formula_to_index f)
(Bdd.ithvar env_state.bdd_manager (Env_state.atomic_formula_to_index (Sup(e1, e2))))
(Bdd.ithvar env_state.bdd_manager (Env_state.atomic_formula_to_index (Inf(e1, e2)))) )
| SupEq(e1, e2) -> Bdd.ithvar env_state.bdd_manager (Env_state.atomic_formula_to_index f)
| Sup(e1, e2) -> Bdd.ithvar env_state.bdd_manager (Env_state.atomic_formula_to_index f)
| InfEq(e1, e2) -> Bdd.ithvar env_state.bdd_manager (Env_state.atomic_formula_to_index f)
| Inf(e1, e2) -> Bdd.ithvar env_state.bdd_manager (Env_state.atomic_formula_to_index f)
in
let _ = match f with
Not(nf) -> ()
......@@ -103,85 +103,6 @@ type var = int
appear in the bdds we manipulate.
*)
(* XXX To remove when mldd is fixed *)
let check_sol_nb_build bdd bdd_not comb ne nt not_ne not_nt =
(**) let card_sol_t =
(**) (Bdd.cardinal
(**) (List.length
(**) (Bdd.int_of_support (Bdd.dthen comb))) (Bdd.dthen bdd)) in
(**) let card_sol_e =
(**) (Bdd.cardinal
(**) (List.length
(**) (Bdd.int_of_support (Bdd.dthen comb))) (Bdd.delse bdd)) in
(**) let nt_float = float_of_sol_nb nt in
(**) let ne_float = float_of_sol_nb ne in
(**)
(**) let card_sol_t_not =
(**) (Bdd.cardinal
(**) (List.length
(**) (Bdd.int_of_support (Bdd.dthen comb)))
(**) (Bdd.dthen bdd_not)) in
(**) let card_sol_e_not =
(**) (Bdd.cardinal
(**) (List.length
(**) (Bdd.int_of_support (Bdd.dthen comb)))
(**) (Bdd.delse bdd_not)) in
(**) let nt_float_not = float_of_sol_nb not_nt in
(**) let ne_float_not = float_of_sol_nb not_ne in
(**) if
(**) (card_sol_t <> nt_float) ||
(**) (card_sol_e <> ne_float) ||
(**) (card_sol_t_not <> nt_float_not) ||
(**) (card_sol_e_not <> ne_float_not)
(**) then
(**) begin
(**) print_string "Lurette computes: ";
(**) print_string (string_of_sol_nb (add_sol_nb nt ne));
(**) print_string " = ";
(**) print_string (string_of_sol_nb nt);
(**) print_string " + ";print_string (string_of_sol_nb ne);
(**) print_string "\nBdd.cardinal computes: ";
(**) print_float (Bdd.cardinal
(**) (List.length (Bdd.int_of_support comb))
(**) bdd);
(**) print_string " = "; print_float card_sol_t;
(**) print_string " + "; print_float card_sol_e ;
(**) print_string "\n\n"; flush stdout ;
(**) Print.bdd_with_dot
(**) bdd
(**) (fun index ->
(**) Formula.formula_to_string
(**) (Env_state.index_to_atomic_formula index))
(**) "bdd" ;
(**)
(**) print_string "(Not) Lurette computes: ";
(**) print_string (string_of_sol_nb (add_sol_nb not_nt not_ne));
(**) print_string " = ";print_string (string_of_sol_nb not_nt);
(**) print_string " + ";print_string (string_of_sol_nb not_ne);
(**) print_string "\nBdd.cardinal computes: ";
(**) print_float (Bdd.cardinal
(**) (List.length (Bdd.int_of_support comb))
(**) bdd_not);
(**) print_string " = "; print_float card_sol_t_not;
(**) print_string " + "; print_float card_sol_e_not ;
(**) print_string "\n\n"; flush stdout ;
(**) Print.bdd_with_dot
(**) bdd_not
(**) (fun index ->
(**) Formula.formula_to_string
(**) (Env_state.index_to_atomic_formula index))
(**) "bdd_not" ;
(**)
(**) Util.gv "bdd.ps";
(**) Util.gv "bdd_not.ps";
(**) false
(**) end
(**) else
(**) true
let rec (count_missing_vars: Bdd.t -> var -> int -> Bdd.t * int) =
fun comb var cpt ->
(* Returns [cpt] + the number of variables occurring in [comb]
......@@ -212,10 +133,6 @@ let rec (build_sol_nb_table: Bdd.t -> Bdd.t -> sol_nb * sol_nb) =
let _ = assert (not (Bdd.is_cst bdd)) in
let (nt, not_nt) = compute_absolute_sol_nb (Bdd.dthen bdd) comb in
let (ne, not_ne) = compute_absolute_sol_nb (Bdd.delse bdd) comb in
(* let _ = assert ( (* XXX Debugging stuff *) *)
(* check_sol_nb_build bdd bdd_not comb ne nt not_ne not_nt) *)
(* in *)
Hashtbl.add env_state.snt bdd (nt, ne) ;
Hashtbl.add env_state.snt bdd_not (not_nt, not_ne) ;
((add_sol_nb nt ne), (add_sol_nb not_nt not_ne))
......@@ -232,7 +149,7 @@ and
let sol_nb =
if Bdd.is_true comb (* iff no bool are to be gen *)
then one_sol
else (two_power_of (List.length (Bdd.int_of_support (Bdd.dthen comb))))
else (two_power_of (List.length (Bdd.list_of_support (Bdd.dthen comb))))
in
if Bdd.is_true sub_bdd
then (sol_nb, zero_sol)
......@@ -252,48 +169,6 @@ and
(****************************************************************************)
(****************************************************************************)
(*XXX Debugging stuff (to remove when the ML in mldd is fixed) *)
let check_sol_nb comb bdd n m t =
(*XXX*) let card_sol_t =
(*XXX*) (Bdd.cardinal (List.length
(*XXX*) (Bdd.int_of_support (Bdd.dthen comb))) (Bdd.dthen bdd))
(*XXX*) and card_sol_e =
(*XXX*) (Bdd.cardinal (List.length
(*XXX*) (Bdd.int_of_support (Bdd.dthen comb))) (Bdd.delse bdd))
(*XXX*) and n_float = float_of_sol_nb n
(*XXX*) and m_float = float_of_sol_nb m
(*XXX*) in
(*XXX*) if
(*XXX*) ( (card_sol_t <> n_float) || (card_sol_e <> m_float) )
(*XXX*) && (card_sol_t < 10. ** 12.)
(*XXX*) (* Bdd.cardinal ougth to do rounding errors after 10^12 *)
(*XXX*) && (card_sol_e < 10. ** 12.)
(*XXX*) then
(*XXX*) begin
(*XXX*) print_string "Lurette computes: ";
print_string (string_of_sol_nb t);
(*XXX*) print_string " = ";print_string (string_of_sol_nb n);
(*XXX*) print_string " + ";print_string (string_of_sol_nb m);
(*XXX*) print_string "\nBdd.cardinal computes: ";
(*XXX*) print_float (Bdd.cardinal
(List.length (Bdd.int_of_support comb))
bdd);
(*XXX*) print_string " = "; print_float card_sol_t;
(*XXX*) print_string " + "; print_float card_sol_e ;
(*XXX*) print_string "\n\n"; flush stdout ;
(*XXX*) Print.bdd_with_dot
(*XXX*) bdd
(*XXX*) (fun index ->
Formula.formula_to_string
(Env_state.index_to_atomic_formula index))
(*XXX*) "bbd" ;
(*XXX*) Util.gv "bdd.ps";
(*XXX*) false
(*XXX*) end
(*XXX*) else
(*XXX*) true
(*XXX*)
let (toss_up_one_var: var -> subst) =
fun var ->
......@@ -369,8 +244,6 @@ let rec (draw_in_bdd: subst list * Rnumsolver.store -> Bdd.t -> Bdd.t ->
let _ =
if ((eq_sol_nb n zero_sol) && (eq_sol_nb m zero_sol))
then raise No_numeric_solution ;
(* XXX Debug stuff (to remove when the mem leak in mldd is fixed) *)
(* assert (check_sol_nb comb bdd n m (add_sol_nb n m)) *)
in
let (store_plus_af, store_plus_not_af) =
(* A first trick to avoid code dup (cf nb above) *)
......@@ -420,7 +293,7 @@ let rec (draw_in_bdd: subst list * Rnumsolver.store -> Bdd.t -> Bdd.t ->
(* Toss the remaining bool vars. *)
( (List.append
sl1
(map toss_up_one_var (Bdd.int_of_support new_comb))),
(map toss_up_one_var (Bdd.list_of_support new_comb))),
store1
)
else
......@@ -453,7 +326,7 @@ let rec (draw_in_bdd: subst list * Rnumsolver.store -> Bdd.t -> Bdd.t ->
( (List.append
sl2
(List.map toss_up_one_var
(Bdd.int_of_support new_comb))),
(Bdd.list_of_support new_comb))),
store2
)
else
......@@ -510,16 +383,16 @@ let (solve_formula: int -> formula list -> vn list -> vnt list ->
in
let comb = formula_to_bdd bool_vars_to_gen_f in
(**) let _ =
(**) (* XXX Recompute the solution number everytime as long as mldd sucks *)
(**) begin
(**) Hashtbl.clear env_state.snt ;
(**) Hashtbl.add env_state.snt
(**) (Bdd.dtrue ()) (one_sol, zero_sol);
(**) Hashtbl.add env_state.snt
(**) (Bdd.dfalse ()) (zero_sol, one_sol)
(**) end
(**) in
(* (**) let _ = *)
(* (**) (* XXX Recompute the solution number everytime as long as mldd sucks *) *)
(* (**) begin *)
(* (**) Hashtbl.clear env_state.snt ; *)
(* (**) Hashtbl.add env_state.snt *)
(* (**) (Bdd.dtrue env_state.bdd_manager) (one_sol, zero_sol); *)
(* (**) Hashtbl.add env_state.snt *)
(* (**) (Bdd.dfalse env_state.bdd_manager) (zero_sol, one_sol) *)
(* (**) end *)
(* (**) in *)
let _ =
if not (Hashtbl.mem env_state.snt bdd)
then
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment