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 ee4eb63d authored by Erwan Jahier's avatar Erwan Jahier
Browse files

lurette 0.33 Mon, 18 Feb 2002 17:52:34 +0100 by jahier

Parent-Version:      0.32
Version-Log:

Avoid recomputing everytime the list of output vars by storing it
in an env_state field.

Project-Description: Lurette
parent af07708a
......@@ -3,14 +3,14 @@
(Created-By-Prcs-Version 1 3 3)
(test/usager.env 396 1013445149 b/14_usager.env 1.2)
(doc/ocamldoc.sty 1380 1008328137 b/12_ocamldoc.s 1.1)
(source/env_state.ml 2145 1013445149 51_env_state. 1.7)
(source/env_state.ml 2296 1014051154 51_env_state. 1.9)
(source/graph.ml 2476 1012914629 14_graph.ml 1.3)
(source/util.ml 4367 1013445149 35_util.ml 1.7)
(source/wtree.ml 9645 1013517738 b/1_wtree.ml 1.7)
(source/solver.ml 11461 1013445149 39_solver.ml 1.7)
(source/command_line.ml 3846 1013500921 b/20_command_li 1.2)
(source/lurette.ml 10371 1013504295 12_lurette.ml 1.18)
(source/solver.mli 972 1013445149 38_solver.mli 1.6)
(source/util.ml 9037 1014051154 35_util.ml 1.9)
(source/wtree.ml 9644 1014051154 b/1_wtree.ml 1.8)
(source/solver.ml 12350 1014051154 39_solver.ml 1.9)
(source/command_line.ml 3971 1014048376 b/20_command_li 1.3)
(source/lurette.ml 11178 1014051154 12_lurette.ml 1.20)
(source/solver.mli 969 1014048376 38_solver.mli 1.7)
(source/env.mli 2506 1013445149 15_env.mli 1.8)
(lurette.depfull.dot 49 1007651448 b/5_lurette.de 1.2)
(source/env.ml 9036 1013517738 16_env.ml 1.14)
......@@ -21,38 +21,38 @@
(doc/archi.fig 3693 1003928781 20_archi.fig 1.1)
(source/parse_env.mli 939 1008328137 40_parse_env. 1.3)
(ID_EN_VRAC 2184 1002196285 0_ID_EN_VRAC 1.1)
(source/sim2chro.mli 1395 1013519411 b/23_sim2chro.m 1.1)
(source/sim2chro.mli 1421 1014051154 b/23_sim2chro.m 1.2)
(doc/automata_format 0 1007379917 b/3_automata_f 1.1)
(source/eval.ml 7903 1013445149 49_eval.ml 1.4)
(source/gen_stubs.ml 32194 1013519411 24_generate_l 1.16)
(source/parse_env.ml 9215 1012914629 41_parse_env. 1.4)
(test/lurette.rif.exp 4746 1013504295 b/22_lurette.ri 1.2)
(test/lurette.rif.exp 4746 1014048376 b/22_lurette.ri 1.3)
(interface/TAGS 1956 1007380262 26_TAGS 1.3)
(source/sim2chro.ml 2833 1013519411 b/24_sim2chro.m 1.1)
(source/sim2chro.ml 2668 1014051154 b/24_sim2chro.m 1.2)
(doc/Interface_draft 5232 1003928781 19_Interface_ 1.1)
(doc/ocamldoc.hva 313 1008328137 b/13_ocamldoc.h 1.1)
(source/formula.mli 1870 1013445149 44_formula.ml 1.4)
(source/command_line.mli 1266 1013500921 b/21_command_li 1.2)
(source/command_line.mli 1302 1014048376 b/21_command_li 1.3)
(TAGS 9825 1007379917 21_TAGS 1.6)
(source/wtree.mli 2964 1013517738 b/0_wtree.mli 1.5)
(source/env_state.mli 3228 1013445149 50_env_state. 1.6)
(source/env_state.mli 3605 1014051154 50_env_state. 1.8)
(test/porte.env 861 1012914629 b/16_porte.env 1.1)
(source/eval.mli 1668 1013445149 48_eval.mli 1.4)
(README 74 1011881677 10_README 1.2)
(test/ControleurPorte.c 9407 1012914629 b/19_Controleur 1.1)
(OcamlMakefile 17010 1013517738 17_OcamlMakef 1.14)
(source/show_env.ml 3167 1013445149 43_show_env.m 1.2)
(OcamlMakefile 18458 1014048376 17_OcamlMakef 1.15)
(source/show_env.ml 2961 1014048376 43_show_env.m 1.3)
(test/tram.env 806 1012914629 b/15_tram.env 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 929 1013445149 42_show_env.m 1.3)
(source/show_env.mli 826 1014048376 42_show_env.m 1.4)
(test/tram_simple.h 1746 1013519411 b/25_tram_simpl 1.1)
(Makefile 1703 1013445149 18_Makefile 1.17)
(Makefile 1641 1014051154 18_Makefile 1.19)
(test/vrai_tram.c 3060 1012914629 b/8_vrai_tram. 1.2)
(source/print.mli 417 1013445149 46_print.mli 1.4)
(source/graph.mli 1417 1012914629 13_graph.mli 1.4)
(source/print.mli 597 1014048376 46_print.mli 1.5)
(source/graph.mli 1499 1014048376 13_graph.mli 1.5)
(source/formula.ml 3689 1013445149 45_formula.ml 1.5)
(source/lurette.mli 396 1012914629 11_lurette.ml 1.10)
(source/print.ml 2706 1013445149 47_print.ml 1.5)
(source/print.ml 5316 1014048376 47_print.ml 1.6)
(test/vrai_tram.h 2468 1012914629 b/7_vrai_tram. 1.2)
......@@ -2,8 +2,8 @@ LURETTE_DIR = ..
OCAMLMAKEFILE = $(LURETTE_DIR)/OcamlMakefile
# OCAMLFLAGS = -noassert -unsafe
# OCAMLNCFLAGS = -inline 10
OCAMLFLAGS = -noassert -unsafe
OCAMLNCFLAGS = -inline 10
-include ./lurette.in
......
;; -*- Prcs -*-
(Created-By-Prcs-Version 1 3 3)
(Project-Description "Lurette")
(Project-Version lurette 0 32)
(Parent-Version lurette 0 31)
(Project-Version lurette 0 33)
(Parent-Version lurette 0 32)
(Version-Log "
Add an option --no-oracle to prevent that lurette calls the oracle.
The solution number counting function was wrong.
Also, make it easy to switch to float, or to big_int, to store
the number of solution numbers.
Avoid recomputing everytime the list of output vars by storing it
in an env_state field.
")
(New-Version-Log "")
(Checkin-Time "Mon, 18 Feb 2002 17:06:16 +0100")
(Checkin-Time "Mon, 18 Feb 2002 17:52:34 +0100")
(Checkin-Login jahier)
(Populate-Ignore ())
(Project-Keywords)
......@@ -26,7 +20,7 @@ the number of solution numbers.
;; Sources files
(source/lurette.mli (lurette/11_lurette.ml 1.10 644))
(source/lurette.ml (lurette/12_lurette.ml 1.19 644))
(source/lurette.ml (lurette/12_lurette.ml 1.20 644))
(source/graph.mli (lurette/13_graph.mli 1.5 644))
(source/graph.ml (lurette/14_graph.ml 1.3 644))
......@@ -34,10 +28,10 @@ the number of solution numbers.
(source/env.mli (lurette/15_env.mli 1.8 644))
(source/env.ml (lurette/16_env.ml 1.14 644))
(source/util.ml (lurette/35_util.ml 1.8 644))
(source/util.ml (lurette/35_util.ml 1.9 644))
(source/solver.mli (lurette/38_solver.mli 1.7 644))
(source/solver.ml (lurette/39_solver.ml 1.8 644))
(source/solver.ml (lurette/39_solver.ml 1.9 644))
(source/parse_env.mli (lurette/40_parse_env. 1.3 644))
(source/parse_env.ml (lurette/41_parse_env. 1.4 644))
......@@ -54,14 +48,14 @@ the number of solution numbers.
(source/eval.mli (lurette/48_eval.mli 1.4 644))
(source/eval.ml (lurette/49_eval.ml 1.4 644))
(source/env_state.mli (lurette/50_env_state. 1.7 644))
(source/env_state.ml (lurette/51_env_state. 1.8 644))
(source/env_state.mli (lurette/50_env_state. 1.8 644))
(source/env_state.ml (lurette/51_env_state. 1.9 644))
(source/wtree.mli (lurette/b/0_wtree.mli 1.5 644))
(source/wtree.ml (lurette/b/1_wtree.ml 1.7 644))
(source/wtree.ml (lurette/b/1_wtree.ml 1.8 644))
(source/sim2chro.mli (lurette/b/23_sim2chro.m 1.1 644))
(source/sim2chro.ml (lurette/b/24_sim2chro.m 1.1 644))
(source/sim2chro.mli (lurette/b/23_sim2chro.m 1.2 644))
(source/sim2chro.ml (lurette/b/24_sim2chro.m 1.2 644))
(source/command_line.ml (lurette/b/20_command_li 1.3 644))
(source/command_line.mli (lurette/b/21_command_li 1.3 644))
......@@ -70,7 +64,7 @@ the number of solution numbers.
;; Make files
(OcamlMakefile (lurette/17_OcamlMakef 1.15 644))
(Makefile (lurette/18_Makefile 1.18 644))
(Makefile (lurette/18_Makefile 1.19 644))
(test/Makefile (../Makefile) :symlink)
(interface/Makefile (lurette/25_Makefile 1.6 644))
(make_lurette (lurette/27_make_luret 1.7 744))
......
......@@ -23,6 +23,7 @@ open Wtree
type env_stateT = {
(* var names and types given file by file *)
mutable var_names: (string, (vnt list * vnt list * vnt list)) Hashtbl.t;
mutable output_var_names: vnt list;
mutable node_to_file_name: (int, string) Hashtbl.t;
mutable var_name_to_index: ((string, int) Hashtbl.t);
mutable index_to_var_name: ((int, string) Hashtbl.t);
......@@ -43,6 +44,7 @@ type env_stateT = {
let (env_state:env_stateT) = {
var_names = Hashtbl.create 0 ;
output_var_names = [];
node_to_file_name = Hashtbl.create 0 ;
var_name_to_index = Hashtbl.create 0 ;
index_to_var_name = Hashtbl.create 0 ;
......
......@@ -20,6 +20,9 @@ type env_stateT = {
(** Var names and types ([vnt]) of input, output, and local vars,
given module by module. *)
mutable output_var_names: vnt list;
(** Output var names and types. *)
mutable node_to_file_name: (int, string) Hashtbl.t;
(** Associates each node with its origin file name (i.e., the
[.aut] it comes from).
......
......@@ -45,6 +45,7 @@ let (var_decl_are_inconsistent : vnt list -> vnt list -> unit) =
let in_env = Util.sort_list_string_pair in_env_unsorted in
let out_env = Util.sort_list_string_pair out_env_unsorted in
env_state.output_var_names <- out_env;
if not(list_are_equals out_env in_sut) then
(
print_string "\nenv outputs: ";
......@@ -191,6 +192,10 @@ and
let () = Env.read_env_state env_llist in
let _ = Sys.command "touch lurette.rif; rm lurette.rif;" in
let rif = open_out "lurette.rif" in
let local_var_name_and_type_list_unsorted = Env_state.loc_env_unsorted () in
let local_var_name_and_type_list =
Util.sort_list_string_pair local_var_name_and_type_list_unsorted
in
(* Initialisation of pre expression and formula *)
let local0 =
......@@ -237,6 +242,7 @@ and
(fold_left (fun acc str -> (acc ^ " " ^ str)) "" (flatten env_llist)) ^ ")")
Lurette_stub.sut_input_var_name_and_type_list
Lurette_stub.sut_output_var_name_and_type_list
local_var_name_and_type_list
stdout options.display_local_var;
flush stdout;
)
......@@ -245,6 +251,7 @@ and
(fold_left (fun acc str -> (acc ^ " " ^ str)) "" (flatten env_llist)) ^ ")")
Lurette_stub.sut_input_var_name_and_type_list
Lurette_stub.sut_output_var_name_and_type_list
local_var_name_and_type_list
rif options.display_local_var;
(* Initializing Dd's libs. *)
......
......@@ -14,9 +14,9 @@ open Env_state
type ssl = (string * string) list
let (put_var_decl: string -> ssl -> ssl -> out_channel -> bool -> unit) =
let (put_var_decl: string -> ssl -> ssl -> ssl -> out_channel -> bool -> unit) =
fun title sut_input_var_name_and_type_list sut_output_var_name_and_type_list
rif display_local_var ->
local_var_name_and_type_list rif display_local_var ->
let put s = output_string rif s in
let put_vt = function
"boolean" -> put "bool"
......@@ -24,11 +24,6 @@ let (put_var_decl: string -> ssl -> ssl -> out_channel -> bool -> unit) =
in
let put_vntl = (fun (vn,vt) -> put vn; put ":"; put_vt vt; put "\n") in
let local_var_name_and_type_list_unsorted = Env_state.loc_env_unsorted () in
let local_var_name_and_type_list =
Util.sort_list_string_pair local_var_name_and_type_list_unsorted
in
put ("#program \" " ^ title ^ " \"\n");
put "#@inputs\n";
......
......@@ -22,7 +22,7 @@ open Env_state
lurette window.
*)
val put_var_decl: string -> (string * string) list -> (string * string) list
-> out_channel -> bool -> unit
-> (string * string) list -> out_channel -> bool -> unit
(**
[put_current_step_values rif t input output local display_local_var]
......
......@@ -251,16 +251,16 @@ let rec (draw_in_bdd: Bdd.t -> Bdd.t -> (var * bool) list) =
then (true, (Bdd.dthen bdd))
else (false, (Bdd.delse bdd))
in
if Bdd.is_cst newbdd then
if Bdd.is_false newbdd then
assert false (* a branch with no solution
should not have been drawn ! *)
else
(bddvar, bool)::(List.map toss_up_one_var
(Bdd.int_of_support (Bdd.dthen comb)))
let _ = assert (not (Bdd.is_false newbdd))
(* a branch with no solution should not have been drawn ! *)
in
if Bdd.is_true newbdd then
(bddvar, bool)::(List.map toss_up_one_var
(Bdd.int_of_support (Bdd.dthen comb)))
else
(bddvar, bool)::(draw_in_bdd newbdd (Bdd.dthen comb))
else
(* Combvar <> topvar *)
(toss_up_one_var combvar)::(draw_in_bdd bdd (Bdd.dthen comb))
......@@ -311,7 +311,7 @@ let (solve_formula: int -> formula list -> var_name list -> (subst list * subst
let (gen_vars, _) = split subst_l in
(sort (compare) gen_vars) = (sort (compare) vars_to_gen) )
in
let (out_vars, _) = List.split (Env_state.out_env_unsorted ()) in
let (out_vars, _) = List.split (env_state.output_var_names) in
(* Splits output and local vars. *)
List.partition (fun (vn, _) -> List.mem vn out_vars) subst_l
in
......
......@@ -51,7 +51,10 @@ let (list_are_equals: 'a list -> 'a list -> bool) =
let (list_intersec: 'a list -> 'a list -> 'a list) =
fun l1 l2 ->
List.filter (fun x -> List.mem x l1) l2
(** Checks is a list is sorted w.r.t. compare *)
let sorted list =
((List.sort (compare) list) = list)
(**
[power a b] returns a to the power of b
......
......@@ -94,13 +94,14 @@ let (build_wtree_table: wgraph -> wtree_table) =
let rec (rm_elt: node list -> wtree -> wtree) =
fun l wt ->
let _ = assert (Util.sorted l) in
(*
** To call when a (conjunction of) formula is unsatisfiable.
*)
match wt with
[] -> []
| L(w, list)::tail ->
if (Util.list_are_equals l list)
if l = list
then tail
else L(w, list)::(rm_elt l tail)
| N(w, swt)::tail ->
......@@ -168,7 +169,7 @@ let rec (choose_a_formula: formula_table -> wtree -> node list
**
** XXX check the performance penalty of that.
*)
let _ = assert ((List.sort (-) nodes_from) = nodes_from) in
let _ = assert (Util.sorted nodes_from) in
let _ = if (wt = []) then
let nodes_str =
List.fold_left (fun acc i -> acc^" "^(string_of_int i)) "" nodes_from
......
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