Vous avez reçu un message "Your GitLab account has been locked ..." ? Pas d'inquiétude : lisez cet article https://docs.gricad-pages.univ-grenoble-alpes.fr/help/unlock/

Commit 1c7769db authored by Erwan Jahier's avatar Erwan Jahier
Browse files

lurette 0.48 Fri, 22 Mar 2002 14:29:17 +0100 by jahier

Parent-Version:      0.47
Version-Log:

Add support for (boolean and numeric) if-then-else.

Remove the eval.ml module as the replacement of pre and input
vars is now done in Solver.formula_to_bdd.

Add a new module gne.ml that provides a garded normal expressions
data structure that is used to handle if-then-elses.

Also introduce a new field to env_state called bdd_tbl_global which
is used to cache the result of formula_to_bdd for bdds that do not
depend on pre nor input vars. The field bdd_tbl which cache the other
reults is now cleared at each step because it is useless to store results
that depends on pre and inputs.

Project-Description: Lurette
parent 606164a8
......@@ -4,64 +4,66 @@
(test/usager.env 424 1015605037 b/14_usager.env 1.4)
(source/command_line_ima_exe.mli 989 1016127950 b/34_command_li 1.1)
(doc/ocamldoc.sty 1380 1008328137 b/12_ocamldoc.s 1.1)
(source/env_state.ml 2787 1016011748 51_env_state. 1.14)
(source/env_state.ml 2978 1016803757 51_env_state. 1.15)
(source/graph.ml 1819 1016011748 14_graph.ml 1.5)
(source/util.ml 10907 1016011748 35_util.ml 1.14)
(source/util.ml 10907 1016803757 35_util.ml 1.15)
(source/wtree.ml 8518 1016011748 b/1_wtree.ml 1.9)
(source/solver.ml 13688 1016011748 39_solver.ml 1.16)
(source/solver.ml 22670 1016803757 39_solver.ml 1.17)
(source/command_line.ml 3998 1016024341 b/20_command_li 1.4)
(source/lurette.ml 10729 1016027474 12_lurette.ml 1.28)
(source/solver.mli 1059 1015250295 38_solver.mli 1.9)
(source/env.mli 2389 1015250295 15_env.mli 1.9)
(source/lurette.ml 11199 1016803757 12_lurette.ml 1.29)
(source/solver.mli 1135 1016803757 38_solver.mli 1.10)
(source/env.mli 2517 1016803757 15_env.mli 1.10)
(test/heater_float.rif.exp 1461 1015514807 b/30_heater_flo 1.2)
(lurette.depfull.dot 49 1007651448 b/5_lurette.de 1.2)
(source/env.ml 9771 1016013431 16_env.ml 1.19)
(source/env.ml 10689 1016803757 16_env.ml 1.20)
(make_lurette 812 1013517738 27_make_luret 1.7)
(test/vrai_tram.lus 453 1007379917 b/6_vrai_tram. 1.1)
(lurette.dep.dot 49 1007651448 b/4_lurette.de 1.2)
(test/passerelle.env 821 1015605037 b/17_passerelle 1.3)
(doc/archi.fig 3693 1003928781 20_archi.fig 1.1)
(source/rnumsolver.ml 7438 1015514807 b/27_rnumsolver 1.3)
(source/rnumsolver.ml 10788 1016803757 b/27_rnumsolver 1.4)
(source/parse_env.mli 907 1016127950 40_parse_env. 1.6)
(ID_EN_VRAC 2184 1002196285 0_ID_EN_VRAC 1.1)
(source/sim2chro.mli 1427 1015250295 b/23_sim2chro.m 1.3)
(source/ima_exe.ml 7125 1016127950 b/32_ima_exe.ml 1.1)
(source/ima_exe.ml 7152 1016803757 b/32_ima_exe.ml 1.2)
(doc/automata_format 0 1007379917 b/3_automata_f 1.1)
(source/eval.ml 8050 1016011748 49_eval.ml 1.11)
(source/gen_stubs.ml 33424 1015408234 24_generate_l 1.19)
(source/parse_env.ml 11322 1016024020 41_parse_env. 1.9)
(source/eval.ml 7749 1016803757 49_eval.ml 1.12)
(source/gen_stubs.ml 33406 1016803757 24_generate_l 1.20)
(source/parse_env.ml 12471 1016803757 41_parse_env. 1.10)
(interface/TAGS 1956 1007380262 26_TAGS 1.3)
(source/sim2chro.ml 2669 1016127950 b/24_sim2chro.m 1.5)
(source/sim2chro.ml 2663 1016803757 b/24_sim2chro.m 1.6)
(doc/Interface_draft 5232 1003928781 19_Interface_ 1.1)
(doc/ocamldoc.hva 313 1008328137 b/13_ocamldoc.h 1.1)
(source/formula.mli 2206 1016127950 44_formula.ml 1.8)
(source/formula.mli 3354 1016803757 44_formula.ml 1.9)
(TAGS 9825 1007379917 21_TAGS 1.6)
(test/Makefile_ima_exe 1624 1016127950 b/35_Makefile_i 1.1)
(test/Makefile_ima_exe 1622 1016803757 b/35_Makefile_i 1.2)
(source/command_line.mli 1317 1016024341 b/21_command_li 1.4)
(source/wtree.mli 2340 1016011748 b/0_wtree.mli 1.7)
(test/porte.env 834 1015605037 b/16_porte.env 1.3)
(source/env_state.mli 3589 1016011748 50_env_state. 1.12)
(source/rnumsolver.mli 1909 1015246213 b/26_rnumsolver 1.1)
(source/env_state.mli 3851 1016803757 50_env_state. 1.13)
(source/rnumsolver.mli 1758 1016803757 b/26_rnumsolver 1.2)
(source/ima_exe.mli 447 1016127950 b/31_ima_exe.ml 1.1)
(source/eval.mli 1413 1016011748 48_eval.mli 1.8)
(source/eval.mli 1389 1016803757 48_eval.mli 1.9)
(README 74 1011881677 10_README 1.2)
(test/ControleurPorte.c 9407 1012914629 b/19_Controleur 1.1)
(OcamlMakefile 19280 1016127950 17_OcamlMakef 1.22)
(source/command_line_ima_exe.ml 2381 1016127950 b/33_command_li 1.1)
(test/ControleurPorte.rif.exp 4746 1016013431 b/29_Controleur 1.3)
(source/command_line_ima_exe.ml 2400 1016803757 b/33_command_li 1.2)
(test/ControleurPorte.rif.exp 4746 1016803757 b/29_Controleur 1.4)
(test/tram.env 905 1015605037 b/15_tram.env 1.3)
(source/show_env.ml 2961 1014048376 43_show_env.m 1.3)
(source/gne.mli 1107 1016803757 b/36_gne.mli 1.1)
(doc/synthese 2556 1007379917 b/2_synthese 1.1)
(test/ControleurPorte.h 2306 1012914629 b/18_Controleur 1.1)
(interface/Makefile 197 1008255910 25_Makefile 1.6)
(source/show_env.mli 765 1015250295 42_show_env.m 1.5)
(source/gne.ml 8204 1016803757 b/37_gne.ml 1.1)
(test/tram_simple.h 1746 1013519411 b/25_tram_simpl 1.1)
(Makefile 1758 1015514807 18_Makefile 1.23)
(Makefile 1756 1016803757 18_Makefile 1.24)
(test/vrai_tram.c 3060 1012914629 b/8_vrai_tram. 1.2)
(source/print.mli 606 1016027474 46_print.mli 1.7)
(source/print.mli 789 1016803757 46_print.mli 1.8)
(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 4780 1016127950 45_formula.ml 1.10)
(source/formula.ml 6652 1016803757 45_formula.ml 1.11)
(source/lurette.mli 448 1016027474 11_lurette.ml 1.12)
(source/print.ml 5700 1016027474 47_print.ml 1.12)
(source/print.ml 6298 1016803757 47_print.ml 1.13)
(test/vrai_tram.h 2468 1012914629 b/7_vrai_tram. 1.2)
......@@ -25,14 +25,14 @@ SOURCES_OCAML = \
$(LURETTE_DIR)/source/graph.mli $(LURETTE_DIR)/source/graph.ml \
$(LURETTE_DIR)/source/command_line.mli $(LURETTE_DIR)/source/command_line.ml \
$(LURETTE_DIR)/source/formula.mli $(LURETTE_DIR)/source/formula.ml \
$(LURETTE_DIR)/source/gne.mli $(LURETTE_DIR)/source/gne.ml \
$(LURETTE_DIR)/source/parse_env.mli $(LURETTE_DIR)/source/parse_env.ml \
$(LURETTE_DIR)/source/env_state.mli $(LURETTE_DIR)/source/env_state.ml \
$(LURETTE_DIR)/source/print.mli $(LURETTE_DIR)/source/print.ml \
$(LURETTE_DIR)/source/rnumsolver.mli $(LURETTE_DIR)/source/rnumsolver.ml \
$(LURETTE_DIR)/source/print.mli $(LURETTE_DIR)/source/print.ml \
$(LURETTE_DIR)/source/solver.mli $(LURETTE_DIR)/source/solver.ml \
$(LURETTE_DIR)/source/wtree.mli $(LURETTE_DIR)/source/wtree.ml \
$(LURETTE_DIR)/source/show_env.mli $(LURETTE_DIR)/source/show_env.ml \
$(LURETTE_DIR)/source/eval.mli $(LURETTE_DIR)/source/eval.ml \
$(LURETTE_DIR)/source/sim2chro.mli $(LURETTE_DIR)/source/sim2chro.ml \
$(LURETTE_DIR)/source/env.mli $(LURETTE_DIR)/source/env.ml \
lurette_stub.ml \
......
;; -*- Prcs -*-
(Created-By-Prcs-Version 1 3 3)
(Project-Description "Lurette")
(Project-Version lurette 0 47)
(Parent-Version lurette 0 46)
(Project-Version lurette 0 48)
(Parent-Version lurette 0 47)
(Version-Log "
Implement an ima_exe that lets one imterprets .env automata offline
via a rif dialogue (e.g., to be used from lulu).
Add support for (boolean and numeric) if-then-else.
Remove the eval.ml module as the replacement of pre and input
vars is now done in Solver.formula_to_bdd.
Add a new module gne.ml that provides a garded normal expressions
data structure that is used to handle if-then-elses.
Also introduce a new field to env_state called bdd_tbl_global which
is used to cache the result of formula_to_bdd for bdds that do not
depend on pre nor input vars. The field bdd_tbl which cache the other
reults is now cleared at each step because it is useless to store results
that depends on pre and inputs.
")
(New-Version-Log "")
(Checkin-Time "Thu, 14 Mar 2002 18:45:50 +0100")
(Checkin-Time "Fri, 22 Mar 2002 14:29:17 +0100")
(Checkin-Login jahier)
(Populate-Ignore ())
(Project-Keywords)
......@@ -21,14 +32,14 @@ via a rif dialogue (e.g., to be used from lulu).
;; Sources files for ima_exe
(source/ima_exe.mli (lurette/b/31_ima_exe.ml 1.1 644))
(source/ima_exe.ml (lurette/b/32_ima_exe.ml 1.1 644))
(source/ima_exe.ml (lurette/b/32_ima_exe.ml 1.2 644))
(source/command_line_ima_exe.ml (lurette/b/33_command_li 1.1 644))
(source/command_line_ima_exe.ml (lurette/b/33_command_li 1.2 644))
(source/command_line_ima_exe.mli (lurette/b/34_command_li 1.1 644))
;; Sources files for lurette only
(source/lurette.mli (lurette/11_lurette.ml 1.12 644))
(source/lurette.ml (lurette/12_lurette.ml 1.28 644))
(source/lurette.ml (lurette/12_lurette.ml 1.29 644))
(source/command_line.ml (lurette/b/20_command_li 1.4 644))
(source/command_line.mli (lurette/b/21_command_li 1.4 644))
......@@ -37,48 +48,48 @@ via a rif dialogue (e.g., to be used from lulu).
(source/graph.mli (lurette/13_graph.mli 1.6 644))
(source/graph.ml (lurette/14_graph.ml 1.5 644))
(source/env.mli (lurette/15_env.mli 1.9 644))
(source/env.ml (lurette/16_env.ml 1.19 644))
(source/env.mli (lurette/15_env.mli 1.10 644))
(source/env.ml (lurette/16_env.ml 1.20 644))
(source/util.ml (lurette/35_util.ml 1.14 644))
(source/util.ml (lurette/35_util.ml 1.15 644))
(source/solver.mli (lurette/38_solver.mli 1.9 644))
(source/solver.ml (lurette/39_solver.ml 1.16 644))
(source/solver.mli (lurette/38_solver.mli 1.10 644))
(source/solver.ml (lurette/39_solver.ml 1.17 644))
(source/rnumsolver.mli (lurette/b/26_rnumsolver 1.1 644))
(source/rnumsolver.ml (lurette/b/27_rnumsolver 1.3 644))
(source/rnumsolver.mli (lurette/b/26_rnumsolver 1.2 644))
(source/rnumsolver.ml (lurette/b/27_rnumsolver 1.4 644))
(source/parse_env.mli (lurette/40_parse_env. 1.6 644))
(source/parse_env.ml (lurette/41_parse_env. 1.9 644))
(source/parse_env.ml (lurette/41_parse_env. 1.10 644))
(source/show_env.mli (lurette/42_show_env.m 1.5 644))
(source/show_env.ml (lurette/43_show_env.m 1.3 644))
(source/formula.mli (lurette/44_formula.ml 1.8 644))
(source/formula.ml (lurette/45_formula.ml 1.10 644))
(source/formula.mli (lurette/44_formula.ml 1.9 644))
(source/formula.ml (lurette/45_formula.ml 1.11 644))
(source/print.mli (lurette/46_print.mli 1.7 644))
(source/print.ml (lurette/47_print.ml 1.12 644))
(source/print.mli (lurette/46_print.mli 1.8 644))
(source/print.ml (lurette/47_print.ml 1.13 644))
(source/eval.mli (lurette/48_eval.mli 1.8 644))
(source/eval.ml (lurette/49_eval.ml 1.11 644))
(source/eval.mli (lurette/48_eval.mli 1.9 644))
(source/eval.ml (lurette/49_eval.ml 1.12 644))
(source/env_state.mli (lurette/50_env_state. 1.12 644))
(source/env_state.ml (lurette/51_env_state. 1.14 644))
(source/env_state.mli (lurette/50_env_state. 1.13 644))
(source/env_state.ml (lurette/51_env_state. 1.15 644))
(source/wtree.mli (lurette/b/0_wtree.mli 1.7 644))
(source/wtree.ml (lurette/b/1_wtree.ml 1.9 644))
(source/sim2chro.mli (lurette/b/23_sim2chro.m 1.3 644))
(source/sim2chro.ml (lurette/b/24_sim2chro.m 1.5 644))
(source/sim2chro.ml (lurette/b/24_sim2chro.m 1.6 644))
(source/gen_stubs.ml (lurette/24_generate_l 1.19 644))
(source/gen_stubs.ml (lurette/24_generate_l 1.20 644))
;; Make files
(OcamlMakefile (lurette/17_OcamlMakef 1.22 644))
(Makefile (lurette/18_Makefile 1.23 644))
(Makefile (lurette/18_Makefile 1.24 644))
(interface/Makefile (lurette/25_Makefile 1.6 644))
(test/Makefile_ima_exe (lurette/b/35_Makefile_i 1.1 644))
(test/Makefile_ima_exe (lurette/b/35_Makefile_i 1.2 644))
(make_lurette (lurette/27_make_luret 1.7 744))
......@@ -114,12 +125,18 @@ via a rif dialogue (e.g., to be used from lulu).
(test/tram_simple.h (lurette/b/25_tram_simpl 1.1 644))
(test/heater_int.rif.exp (lurette/b/28_heater_int 1.1 644))
(test/ControleurPorte.rif.exp (lurette/b/29_Controleur 1.3 644))
(test/ControleurPorte.rif.exp (lurette/b/29_Controleur 1.4 644))
(test/heater_float.rif.exp (lurette/b/30_heater_flo 1.2 644))
;; Files added by populate at Mon, 18 Mar 2002 16:20:57 +0100,
;; to version 0.47(w), by jahier:
(source/gne.mli (lurette/b/36_gne.mli 1.1 644))
(source/gne.ml (lurette/b/37_gne.ml 1.1 644))
)
(Merge-Parents)
(New-Merge-Parents)
......@@ -20,6 +20,7 @@ type cmd_line_optionT =
(* Names of the command line options to override the defaults. *)
let (string_to_option: (string * cmd_line_optionT) list) = [
("-b", Boot);
("-boot", Boot);
("--boot", Boot);
("--with-seed", Seed);
......
......@@ -129,10 +129,10 @@ type nl = node list
type nll = node list list
type sl = subst list
let (solve_formula_list: int -> node list list ->
let (solve_formula_list: env_in -> int -> node list list ->
(node list list * sl * sl) list -> formula list -> var_name list ->
vnt list -> (node list list * sl * sl) list) =
fun p nll acc fl bool_vars_to_gen num_vnt_to_gen ->
fun input p nll acc fl bool_vars_to_gen num_vnt_to_gen ->
(*
** Returns [p] solutions for the conjunction of formula contained
** in [fl]; a solution is a triple containing (1) the node list [nll],
......@@ -140,7 +140,7 @@ let (solve_formula_list: int -> node list list ->
** (2) a list of substitutions for output vars, and (3) a list of
** substitutions for local vars.
*)
let sl_sl_l = Solver.solve_formula p fl bool_vars_to_gen num_vnt_to_gen in
let sl_sl_l = Solver.solve_formula input p fl bool_vars_to_gen num_vnt_to_gen in
(* Adds the target nodes to the drawn substitutions *)
if acc = [] then
(* first formula *)
......@@ -158,9 +158,9 @@ let (solve_formula_list: int -> node list list ->
)
let (solve_formula_list_list: int -> node list list * formula list list
let (solve_formula_list_list: env_in -> int -> node list list * formula list list
-> (node list list * sl * sl) list) =
fun p (nll, fll) ->
fun input p (nll, fll) ->
let (get_vars_from_node: (vn list * vnt list) -> node -> (vn list * vnt list)) =
fun (bool_acc, num_acc) node ->
(* Gets the list of (output and local) boolean and numeric
......@@ -191,7 +191,7 @@ let (solve_formula_list_list: int -> node list list * formula list list
in
let nll_sl_sl_l =
Util.list_fold_left3
(solve_formula_list p nll) [] fll bool_vars_to_gen_ll num_vnt_to_gen_ll
(solve_formula_list input p nll) [] fll bool_vars_to_gen_ll num_vnt_to_gen_ll
in
nll_sl_sl_l
......@@ -240,10 +240,10 @@ let _ = assert (
let rec draw_n_p_values n p cn_ll wtl =
let rec draw_n_p_values input n p cn_ll wtl =
let nl_fl_l__wt__l =
(* Draw n formula *)
map2 (Wtree.choose_n_formula (Solver.is_satisfiable) n) cn_ll wtl
map2 (Wtree.choose_n_formula (Solver.is_satisfiable input) n) cn_ll wtl
in
let (nl_fl_ll, new_wtl) =
fold_left
......@@ -255,14 +255,14 @@ let rec draw_n_p_values n p cn_ll wtl =
let nll_fll_l = merge_lll nl_fl_ll in
(* Draw p solutions for each of the n formula *)
let nll_sl_sl_ll = List.map (solve_formula_list_list p) nll_fll_l in
let nll_sl_sl_ll = List.map (solve_formula_list_list input p) nll_fll_l in
let l = Util.count_empty_list nll_sl_sl_ll in
if l = 0
then nll_sl_sl_ll
else
(* At least one formula was not satisfiable because of numeric
constraints. We redraw as many times (l) as necessary. *)
append nll_sl_sl_ll (draw_n_p_values l p cn_ll new_wtl)
append nll_sl_sl_ll (draw_n_p_values input l p cn_ll new_wtl)
......@@ -274,8 +274,7 @@ let (env_try: int -> int -> env_in ->
and wtt = env_state.wtree_table
in
let wtl = get_wtrees cn_ll wtt in
let wtle = List.map (Eval.eval_wtree input) wtl in
let nll_sl_sl_ll = draw_n_p_values n p cn_ll wtle in
let nll_sl_sl_ll = draw_n_p_values input n p cn_ll wtl in
let nll_sl_sl_l = flatten nll_sl_sl_ll in
assert (length nll_sl_sl_l = (n*p));
......@@ -294,6 +293,35 @@ let (env_step : node list list -> env_out -> env_loc -> unit) =
env_state.local <- local
(****************************************************************************)
let (get_pre_var: var_name -> var_name) =
fun pre_n_vn ->
let (n, vn) = Util.split_pre_var_string pre_n_vn in
if (n-1) <> 0
then ("_pre" ^ (string_of_int (n-1)) ^ vn)
else vn
let _ = assert ((get_pre_var "_pre3toto") = "_pre2toto")
let _ = assert ((get_pre_var "_pre1toto") = "toto")
(* exported *)
let (update_pre: env_in -> env_out -> env_loc -> unit) =
fun input output local ->
let (update_one_pre_var : var_name -> subst) =
fun pre_vn ->
let vn = get_pre_var pre_vn in
let pre_value =
try Hashtbl.find input vn
with Not_found ->
try List.assoc vn output
with Not_found ->
try List.assoc vn local
with Not_found -> assert false
in
(pre_vn, pre_value)
in
env_state.pre <- List.map (update_one_pre_var) env_state.pre_var_names
......
......@@ -61,6 +61,8 @@ val env_step : node list list -> env_out -> env_loc -> unit
*)
val update_pre: env_in -> env_out -> env_loc -> unit
(** Updates the values of pre variables (updating [env_state.pre]). *)
......
......@@ -26,10 +26,11 @@ type env_stateT = {
mutable pre_var_names: var_name list;
mutable output_var_names: vnt list;
mutable node_to_file_name: (int, string) Hashtbl.t;
mutable atomic_formula_to_index: ((formula, int) Hashtbl.t);
mutable index_to_atomic_formula: ((int, formula) Hashtbl.t);
mutable atomic_formula_to_index: ((atomic_formula, int) Hashtbl.t);
mutable index_to_atomic_formula: ((int, atomic_formula) Hashtbl.t);
mutable index_cpt: int;
mutable bdd_manager: Manager.t;
mutable bdd_tbl_global: (formula, Bdd.t) Hashtbl.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;
......@@ -53,6 +54,7 @@ let (env_state:env_stateT) = {
index_cpt = 0 ;
bdd_manager = Manager.make 10 10 0 0 0;
bdd_tbl = Hashtbl.create 0;
bdd_tbl_global = Hashtbl.create 0;
snt = Hashtbl.create 3;
current_nodes = [];
graph = Graph.create () ;
......@@ -63,16 +65,18 @@ let (env_state:env_stateT) = {
local = []
}
let atomic_formula_to_index f =
try Hashtbl.find env_state.atomic_formula_to_index f
with Not_found ->
env_state.index_cpt <- (env_state.index_cpt + 1);
Hashtbl.add env_state.atomic_formula_to_index f env_state.index_cpt;
Hashtbl.add env_state.index_to_atomic_formula env_state.index_cpt f;
env_state.index_cpt
let index_to_atomic_formula i =
Hashtbl.find env_state.index_to_atomic_formula i
let (atomic_formula_to_index : atomic_formula -> int) =
fun f ->
try Hashtbl.find env_state.atomic_formula_to_index f
with Not_found ->
env_state.index_cpt <- (env_state.index_cpt + 1);
Hashtbl.add env_state.atomic_formula_to_index f env_state.index_cpt;
Hashtbl.add env_state.index_to_atomic_formula env_state.index_cpt f;
env_state.index_cpt
let (index_to_atomic_formula : int -> atomic_formula) =
fun i ->
Hashtbl.find env_state.index_to_atomic_formula i
let in_env_unsorted _ =
......
......@@ -39,11 +39,11 @@ type env_stateT = {
we need to be able to know what variables are still to be drawn.
*)
mutable atomic_formula_to_index: ((formula, int) Hashtbl.t);
mutable atomic_formula_to_index: ((atomic_formula, int) Hashtbl.t);
(** This indexing of (output and local) variable names is needed
for constructing bdds in the boolean solver (for which variables
are [int], not [string]s. *)
mutable index_to_atomic_formula: ((int, formula) Hashtbl.t);
mutable index_to_atomic_formula: ((int, atomic_formula) Hashtbl.t);
(** Ditto in the other way. *)
mutable index_cpt: int;
(** Counter used to create the index *)
......@@ -51,9 +51,13 @@ type env_stateT = {
mutable bdd_manager: Manager.t;
(** bdd state *)
mutable bdd_tbl_global: (formula, Bdd.t) Hashtbl.t;
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. *)
(** Transforming a formula into a bdd is expensive, therefore we
store the result of this transformation in a table. Only formula
does not depend on pre nor input vars are stored in
[bdd_tbl_global]. The other ones are stored in the table
[bdd_tbl], which is cleared at each new step. *)
mutable snt: (Bdd.t, Util.sol_nb * Util.sol_nb) Hashtbl.t;
(** Associates to a bdd the (absolute) number of solutions
......@@ -95,7 +99,7 @@ val loc_env_unsorted : unit -> vnt list
(** Returns the index of an atomic formula, namely, a boolean
variable or an atomic numerical constraint. *)
val atomic_formula_to_index : formula -> int
val atomic_formula_to_index : atomic_formula -> int
(** Returns the atomic formula of an index. *)
val index_to_atomic_formula : int -> formula
val index_to_atomic_formula : int -> atomic_formula
......@@ -14,17 +14,6 @@ open Env_state
open Wtree
open List
(****************************************************************************)
let (lookup: env_in -> subst list -> var_name -> atomic_expr option) =
fun input pre vn ->
try Some(Hashtbl.find input vn)
with Not_found ->
try Some(List.assoc vn pre)
with Not_found -> None
(****************************************************************************)
(****************************************************************************)
......
......@@ -28,8 +28,7 @@ val eval_wtree : env_in -> wtree -> wtree
formula evaluated w.r.t. `input'. *)
val update_pre: env_in -> env_out -> env_loc -> unit
(** Computes the values of pre expressions and formula (i.e.,
updates [env_state.pre]). *)
(** Updates the values of pre variables (updating [env_state.pre]). *)
val expr_to_atomic: expr -> atomic_expr
......
......@@ -19,11 +19,15 @@ type expr =
| Ival of int
| Fval of float
| Nvar of string
type formula =
| Ivar of string
| Fvar of string
| Ite of formula * expr * expr
and
formula =
| And of formula * formula
| Or of formula * formula
| IteB of formula * formula * formula
| Not of formula
| True
......@@ -47,38 +51,72 @@ type node = int
type weigth = int
type arc = node * node
type arc_info = weigth * formula_eps
(* XXX This is a bad name. Change it ! *)
type atomic_expr =
| Int of int
| Bool of bool
| Float of float
type num_var_name = I of string | F of string
type var_name = string
type vn = var_name
type subst = (var_name * atomic_expr)
type num_value = I of int | F of float
type var_value = B of bool | N of num_value
type subst = (var_name * var_value)
type var_type = BoolT | IntT of int * int | FloatT of float * float
type vnt = var_name * var_type
type vne = var_name * (expr * expr)
type vnf = var_name * (formula * formula)
type env_in = (var_name, atomic_expr) Hashtbl.t
type env_in = (var_name, var_value) Hashtbl.t
type env_out = subst list
type env_loc = subst list
(****************************************************************************)
(****************************************************************************)
(**
Pretty prints formula and expressions
*)
(* exported *)
module NeMap = struct
include Map.Make(struct type t = string let compare = compare end)
end
(* exported *)
type n_expr = num_value NeMap.t
type atomic_formula =
| Bv of string
| GZ of n_expr (** expr > 0 *)
| GeqZ of n_expr (** expr >= 0 *)
| SZ of n_expr (** expr < 0 *)
| SeqZ of n_expr (** expr <= 0 *)
let (is_n_expr_a_constant : n_expr -> bool) =
fun ne ->
(NeMap.remove "" ne) = NeMap.empty
(****************************************************************************)
(* Pretty prints formula and expressions *)
let (num_value_to_string : num_value -> string) =
fun n ->
match n with
I(i) -> string_of_int i
| F(f) -> string_of_float f
let (n_expr_to_string : n_expr -> string) =
fun ne ->
(NeMap.fold
(fun vn v acc ->
if vn = ""
then ((num_value_to_string v) ^ acc)
else (" + " ^ (num_value_to_string v ) ^ "*" ^ vn ^ acc ))
ne
""
)
let rec
(formula_eps_to_string: formula_eps -> string) =
fun fe -> match fe with
......@@ -91,6 +129,9 @@ and
(formula_to_string f2) ^ ")")
| Or(f1, f2) -> ("(" ^ (formula_to_string f1) ^ " or " ^
(formula_to_string f2) ^ ")")
| IteB(f1, f2, f3) -> ("(if " ^ (formula_to_string f1) ^ " then " ^
(formula_to_string f2) ^ " else " ^
(formula_to_string f3) ^ ")")
| Not(f1) -> ("not(" ^ (formula_to_string f1) ^ ")")
| True -> "true"
| False -> "false"
......@@ -114,9 +155,23 @@ and
(expr_to_string e2) ^ ")")
| Mod(e1, e2) -> ("(" ^ (expr_to_string e1) ^ " mod " ^
(expr_to_string e2) ^ ")")
| Nvar(str) -> str
| Ivar(str) -> str
| Fvar(str) -> str
| Ival(i) -> string_of_int i