Commit 429604ce authored by Erwan Jahier's avatar Erwan Jahier

lurette 0.35 Tue, 19 Feb 2002 16:27:14 +0100 by jahier

Parent-Version:      0.34
Version-Log:
 Use Hashtbl instead of assoc list to store env_in
items as eval needs to search in it very often, it might be an issue
when there is a lot of input variables.

Project-Description: Lurette
parent dba4992a
......@@ -3,13 +3,13 @@
(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 2296 1014051154 51_env_state. 1.9)
(source/env_state.ml 2310 1014132434 51_env_state. 1.10)
(source/graph.ml 2476 1012914629 14_graph.ml 1.3)
(source/util.ml 9166 1014111658 35_util.ml 1.10)
(source/wtree.ml 9644 1014051154 b/1_wtree.ml 1.8)
(source/solver.ml 12281 1014111658 39_solver.ml 1.10)
(source/solver.ml 12217 1014132434 39_solver.ml 1.11)
(source/command_line.ml 3971 1014048376 b/20_command_li 1.3)
(source/lurette.ml 11196 1014111658 12_lurette.ml 1.21)
(source/lurette.ml 11253 1014132434 12_lurette.ml 1.22)
(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)
......@@ -23,15 +23,15 @@
(ID_EN_VRAC 2184 1002196285 0_ID_EN_VRAC 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 7930 1014111658 49_eval.ml 1.5)
(source/gen_stubs.ml 32194 1013519411 24_generate_l 1.16)
(source/eval.ml 8064 1014132434 49_eval.ml 1.6)
(source/gen_stubs.ml 32502 1014132434 24_generate_l 1.17)
(source/parse_env.ml 9215 1012914629 41_parse_env. 1.4)
(test/lurette.rif.exp 4746 1014111658 b/22_lurette.ri 1.4)
(test/lurette.rif.exp 4746 1014132434 b/22_lurette.ri 1.5)
(interface/TAGS 1956 1007380262 26_TAGS 1.3)
(source/sim2chro.ml 2668 1014051154 b/24_sim2chro.m 1.2)
(source/sim2chro.ml 2639 1014132434 b/24_sim2chro.m 1.3)
(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/formula.mli 1942 1014132434 44_formula.ml 1.5)
(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)
......@@ -40,7 +40,7 @@
(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 18631 1014111658 17_OcamlMakef 1.16)
(OcamlMakefile 18594 1014132434 17_OcamlMakef 1.17)
(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)
......@@ -52,7 +52,7 @@
(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 1499 1014048376 13_graph.mli 1.5)
(source/formula.ml 3689 1013445149 45_formula.ml 1.5)
(source/formula.ml 3967 1014132434 45_formula.ml 1.6)
(source/lurette.mli 396 1012914629 11_lurette.ml 1.10)
(source/print.ml 5340 1014111658 47_print.ml 1.7)
(test/vrai_tram.h 2468 1012914629 b/7_vrai_tram. 1.2)
......@@ -5,7 +5,7 @@
# For updates see:
# http://miss.wu-wien.ac.at/~mottl/ocaml_sources
#
# $Id: OcamlMakefile 1.16 Tue, 19 Feb 2002 10:40:58 +0100 jahier $
# $Id: OcamlMakefile 1.17 Tue, 19 Feb 2002 16:27:14 +0100 jahier $
#
###########################################################################
......@@ -493,18 +493,18 @@ dot:
cp $(RESULT).dep.ps ../doc ; cp $(RESULT).depfull.ps ../doc ; popd
install:
pushd ../interface ; make; popd ; $(LURETTE_DIR)/make_lurette ControleurPorte vrai_tram dc
pushd ../interface ; make; popd ; ../make_lurette ControleurPorte vrai_tram dc
runbug:
./lurette 10 1 1 tram.env usager.env porte.env passerelle.env -ns2c -seed 1013388978
try:
$(LURETTE_DIR)/make_lurette ControleurPorte vrai_tram; \
../make_lurette ControleurPorte vrai_tram; \
# ./lurette 10 2 2 tram.env usager.env porte.env passerelle.env | sim2chro -ecran
./lurette 10 2 2 tram.env usager.env porte.env passerelle.env
vroum:
$(LURETTE_DIR)/make_lurette ControleurPorte vrai_tram nc; \
times ./lurette 4500 1 1 tram.env usager.env porte.env passerelle.env -seed 1014422484 -ns2c --no-oracle
../make_lurette ControleurPorte vrai_tram nc; \
time ./lurette 4500 1 1 tram.env usager.env porte.env passerelle.env -seed 1014422484 -ns2c --no-oracle
# Non regression test
test:
......
;; -*- Prcs -*-
(Created-By-Prcs-Version 1 3 3)
(Project-Description "Lurette")
(Project-Version lurette 0 34)
(Parent-Version lurette 0 33)
(Version-Log "
Fix a bug when computing the power of two.
(Project-Version lurette 0 35)
(Parent-Version lurette 0 34)
(Version-Log " Use Hashtbl instead of assoc list to store env_in
items as eval needs to search in it very often, it might be an issue
when there is a lot of input variables.
")
(New-Version-Log "")
(Checkin-Time "Tue, 19 Feb 2002 10:40:58 +0100")
(Checkin-Time "Tue, 19 Feb 2002 16:27:14 +0100")
(Checkin-Login jahier)
(Populate-Ignore ())
(Project-Keywords)
......@@ -19,7 +21,7 @@ Fix a bug when computing the power of two.
;; Sources files
(source/lurette.mli (lurette/11_lurette.ml 1.10 644))
(source/lurette.ml (lurette/12_lurette.ml 1.21 644))
(source/lurette.ml (lurette/12_lurette.ml 1.22 644))
(source/graph.mli (lurette/13_graph.mli 1.5 644))
(source/graph.ml (lurette/14_graph.ml 1.3 644))
......@@ -30,7 +32,7 @@ Fix a bug when computing the power of two.
(source/util.ml (lurette/35_util.ml 1.10 644))
(source/solver.mli (lurette/38_solver.mli 1.7 644))
(source/solver.ml (lurette/39_solver.ml 1.10 644))
(source/solver.ml (lurette/39_solver.ml 1.11 644))
(source/parse_env.mli (lurette/40_parse_env. 1.3 644))
(source/parse_env.ml (lurette/41_parse_env. 1.4 644))
......@@ -38,31 +40,31 @@ Fix a bug when computing the power of two.
(source/show_env.mli (lurette/42_show_env.m 1.4 644))
(source/show_env.ml (lurette/43_show_env.m 1.3 644))
(source/formula.mli (lurette/44_formula.ml 1.4 644))
(source/formula.ml (lurette/45_formula.ml 1.5 644))
(source/formula.mli (lurette/44_formula.ml 1.5 644))
(source/formula.ml (lurette/45_formula.ml 1.6 644))
(source/print.mli (lurette/46_print.mli 1.5 644))
(source/print.ml (lurette/47_print.ml 1.7 644))
(source/eval.mli (lurette/48_eval.mli 1.4 644))
(source/eval.ml (lurette/49_eval.ml 1.5 644))
(source/eval.ml (lurette/49_eval.ml 1.6 644))
(source/env_state.mli (lurette/50_env_state. 1.8 644))
(source/env_state.ml (lurette/51_env_state. 1.9 644))
(source/env_state.ml (lurette/51_env_state. 1.10 644))
(source/wtree.mli (lurette/b/0_wtree.mli 1.5 644))
(source/wtree.ml (lurette/b/1_wtree.ml 1.8 644))
(source/sim2chro.mli (lurette/b/23_sim2chro.m 1.2 644))
(source/sim2chro.ml (lurette/b/24_sim2chro.m 1.2 644))
(source/sim2chro.ml (lurette/b/24_sim2chro.m 1.3 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))
(source/gen_stubs.ml (lurette/24_generate_l 1.16 644))
(source/gen_stubs.ml (lurette/24_generate_l 1.17 644))
;; Make files
(OcamlMakefile (lurette/17_OcamlMakef 1.16 644))
(OcamlMakefile (lurette/17_OcamlMakef 1.17 644))
(Makefile (lurette/18_Makefile 1.20 644))
(test/Makefile (../Makefile) :symlink)
(interface/Makefile (lurette/25_Makefile 1.6 644))
......@@ -100,7 +102,7 @@ Fix a bug when computing the power of two.
(test/vrai_tram.c (lurette/b/8_vrai_tram. 1.2 644))
(test/tram_simple.h (lurette/b/25_tram_simpl 1.1 644))
(test/lurette.rif.exp (lurette/b/22_lurette.ri 1.4 644))
(test/lurette.rif.exp (lurette/b/22_lurette.ri 1.5 644))
)
......
......@@ -56,7 +56,7 @@ let (env_state:env_stateT) = {
graph = Graph.create () ;
formula_table = Hashtbl.create 0 ;
wtree_table = Hashtbl.create 0 ;
input = [] ;
input = Hashtbl.create 0 ;
output = [] ;
local = []
}
......
......@@ -17,12 +17,18 @@ open Wtree
let (lookup: subst list -> var_name -> atomic_expr option) =
fun sl v ->
try
let v = List.assoc v sl in
Some(v)
let (lookup: env_in -> var_name -> atomic_expr option) =
fun env_in_tbl v ->
try Some(Hashtbl.find env_in_tbl v)
with Not_found -> None
let (lookup_loc: var_name -> atomic_expr option) =
fun v ->
try
let v = List.assoc v env_state.local in
Some(v)
with Not_found -> None
(****************************************************************************)
(****************************************************************************)
......@@ -73,7 +79,7 @@ let rec (eval : formula -> env_in -> formula) =
print_string (str ^ " is not a boolean!\n");
assert false
| None ->
(match (lookup env_state.local str) with
(match (lookup_loc str) with
Some(Bool(bool)) ->
if bool then True else False
| Some(_) ->
......@@ -178,7 +184,7 @@ and
^ "is a bool, not an int nor of float!\n");
assert false
| None ->
( match (lookup env_state.local str) with
( match (lookup_loc str) with
Some(Int(i)) -> Ival(i)
| Some(Float(f)) -> Fval(f)
| Some(Bool(f)) ->
......
......@@ -60,7 +60,7 @@ type vnt = var_name * var_type
type vne = var_name * (expr * expr)
type vnf = var_name * (formula * formula)
type env_in = subst list
type env_in = (var_name, atomic_expr) Hashtbl.t
type env_out = subst list
type env_loc = subst list
......@@ -127,9 +127,21 @@ let (print_subst_list : subst list -> out_channel -> unit) =
fun sl oc ->
List.iter
(fun (vn, e) ->
print_string vn ;
print_string "=";
output_string oc vn ;
output_string oc "=";
print_atomic_expr e oc;
print_string " "
output_string oc " "
)
(Util.sort_list_string_pair sl)
let (print_env_in : env_in -> out_channel -> unit) =
fun tbl oc ->
Hashtbl.iter
(fun vn e ->
output_string oc vn ;
output_string oc "=";
print_atomic_expr e oc;
output_string oc " "
)
tbl
......@@ -64,7 +64,7 @@ type vnt = var_name * var_type
type vne = var_name * (expr * expr)
type vnf = var_name * (formula * formula)
type env_in = subst list
type env_in = (var_name, atomic_expr) Hashtbl.t
type env_out = subst list
type env_loc = subst list
......@@ -81,3 +81,4 @@ val expr_to_string : expr -> string
val arc_info_to_string : arc_info -> string
val print_atomic_expr : atomic_expr -> out_channel -> unit
val print_subst_list : subst list -> out_channel -> unit
val print_env_in : env_in -> out_channel -> unit
......@@ -648,6 +648,7 @@ let (generate_lurette_stub_file: vn_ct_mlt_fvn list * vn_ct_mlt_fvn list -> unit
put "(* Automatically generated from sut_idl_stub.ml by interface/gen_stubs. *)\n" ;
put "open Format\n";
put "open Hashtbl\n";
put "open Formula\n\n";
(*
......@@ -661,55 +662,72 @@ let (generate_lurette_stub_file: vn_ct_mlt_fvn list * vn_ct_mlt_fvn list -> unit
put (format_string_list " * " mltl_out) ;
put "\n\n" ;
(*
** Defines subst_list_to_sut_in which transform a list of atomic_expr
** into a sut_in, i.e., a tuple of values.
*)
put "(****************************************************************) \n\n";
put "(** Converting tuples to subst lists and vive-versa *) \n";
put "let (subst_list_to_sut_in: subst list -> sut_in) =\n" ;
put " fun sl ->\n" ;
put " let sl_sorted = Util.sort_list_string_pair sl in\n";
put " match sl_sorted with\n" ;
put " [" ;
put (format_string_list "; \n\t " vn_val_in) ;
put "] \n\t -> (" ;
put (format_string_list ", " fvnl_in) ;
put ")\n";
put " | [] -> (" ;
put_fake_value (List.hd sut_in) ;
List.iter
(fun x -> put ", "; put_fake_value x)
(List.tl sut_in) ;
put ")\n";
put " | _ -> assert false\n\n" ;
(* Ditto for sut_out. *)
put "let (subst_list_to_sut_out: subst list -> sut_out) =\n" ;
put " fun sl ->\n" ;
put " let sl_sorted = Util.sort_list_string_pair sl in\n";
put " match sl_sorted with\n" ;
put " [" ;
put (format_string_list "; \n\t " vn_val_out) ;
put "] \n\t -> (" ;
(*
** Defines subst_list_to_sut_in which transform a list of atomic_expr
** into a sut_in, i.e., a tuple of values.
*)
put "(****************************************************************) \n\n";
put "(** Converting tuples to subst lists and vive-versa *) \n";
put "let (subst_list_to_sut_in: subst list -> sut_in) =\n" ;
put " fun sl ->\n" ;
put " let sl_sorted = Util.sort_list_string_pair sl in\n";
put " match sl_sorted with\n" ;
put " [" ;
put (format_string_list "; \n\t " vn_val_in) ;
put "] \n\t -> (" ;
put (format_string_list ", " fvnl_in) ;
put ")\n";
put " | [] -> (" ;
put_fake_value (List.hd sut_in) ;
List.iter
(fun x -> put ", "; put_fake_value x)
(List.tl sut_in) ;
put ")\n";
put " | _ -> assert false\n\n" ;
put "(****************************************************************) \n";
put "(** Converting tuples to Hashtbl and vive-versa *) \n";
put "let (env_in_to_sut_out: env_in -> sut_out) =\n" ;
put " fun tbl ->\n" ;
put " try (\n" ;
List.iter2
(fun x y->
put " let "; put y; put "_found = (Hashtbl.find tbl \"";
put x;
put "\") in \n";
)
vnl_out
fvnl_out;
put "\tmatch (" ;
put (format_string_list "_found, " fvnl_out) ;
put "_found) with \n (";
put (format_string_list ", " fael_out) ;
put ")\n\t -> (" ;
put (format_string_list ", " fvnl_out) ;
put ")\n";
put " | [] -> (" ;
put_fake_value (List.hd sut_out) ;
List.iter
(fun x -> put ", "; put_fake_value x)
(List.tl sut_out) ;
put ")\n";
put " | _ -> assert false\n\n" ;
put ")\n | _ -> assert false \n" ;
put " )\n" ;
put " with Not_found -> assert false\n\n" ;
(* Ditto, but the other way around *)
put "let (sut_out_to_subst_list: sut_out -> subst list) =\n" ;
put " fun sut_out ->\n match sut_out with\n" ;
put " (" ;
put "let (sut_out_to_env_in: sut_out -> env_in) =\n" ;
put " fun (" ;
put (format_string_list ", " fvnl_out) ;
put ") \n\t->\n\t [" ;
put (format_string_list "; \n\t " vn_val_out) ;
put "]\n\n\n" ;
put ") \n ->\n\tlet tbl = create " ;
put (string_of_int (List.length fvnl_out));
put " in\n";
List.iter2
(fun x y ->
put "\t Hashtbl.add tbl \""; put x; put "\" ("; put y; put ");\n")
vnl_out
fael_out ;
put "\t tbl\n\n" ;
(*
......@@ -720,40 +738,40 @@ let (generate_lurette_stub_file: vn_ct_mlt_fvn list * vn_ct_mlt_fvn list -> unit
put "(** Stubs provided by camlidl manipulates tuples whereas we \n" ;
put " manipulate subst lists. Thefore we define here our own \n" ;
put " versions of sut_try, sut_step, etc.\n *) \n\n";
put ("let (sut_try: Formula.subst list -> Formula.subst list) = \n") ;
put ("let (sut_try: Formula.subst list -> Formula.env_in) = \n") ;
put " fun input_sl ->\n let (" ;
put (format_string_list ", " fvnl_in) ;
put ") = subst_list_to_sut_in input_sl in \n" ;
put " let output_tuple = Sut_idl_stub.sut_try " ;
put (format_string_list " " fvnl_in) ;
put " in \n" ;
put " sut_out_to_subst_list output_tuple \n\n" ;
put " sut_out_to_env_in output_tuple \n\n" ;
(*
** Ditto for `sut_step'.
*)
put ("let (sut_step: Formula.subst list -> Formula.subst list) = \n") ;
put ("let (sut_step: Formula.subst list -> Formula.env_in) = \n") ;
put " fun input_sl ->\n let (" ;
put (format_string_list ", " fvnl_in) ;
put ") = subst_list_to_sut_in input_sl in \n" ;
put " let output_tuple = Sut_idl_stub.sut_step " ;
put (format_string_list " " fvnl_in) ;
put " in \n" ;
put " sut_out_to_subst_list output_tuple \n\n" ;
put " sut_out_to_env_in output_tuple \n\n" ;
(*
** Ditto for `oracle_try'.
*)
put ("let (oracle_try: Formula.subst list -> Formula.subst list -> bool) = \n") ;
put " fun input_sl output_sl -> \n";
put ("let (oracle_try: Formula.subst list -> Formula.env_in -> bool) = \n") ;
put " fun sut_input sut_output -> \n";
put " let (";
put (format_string_list ", " fvnl_in) ;
put ") = subst_list_to_sut_in input_sl in \n" ;
put ") = subst_list_to_sut_in sut_input in \n" ;
put " let (";
put (format_string_list ", " fvnl_out) ;
put ") = subst_list_to_sut_out output_sl in \n" ;
put ") = env_in_to_sut_out sut_output in \n" ;
put " Oracle_idl_stub.oracle_try " ;
put (format_string_list " " fvnl_in) ;
put " " ;
......@@ -763,14 +781,14 @@ let (generate_lurette_stub_file: vn_ct_mlt_fvn list * vn_ct_mlt_fvn list -> unit
(*
** Ditto for `oracle_step'.
*)
put ("let (oracle_step: Formula.subst list -> Formula.subst list -> bool) = \n") ;
put " fun input_sl output_sl -> \n";
put ("let (oracle_step: Formula.subst list -> Formula.env_in -> bool) = \n") ;
put " fun sut_input sut_output -> \n";
put " let (";
put (format_string_list ", " fvnl_in) ;
put ") = subst_list_to_sut_in input_sl in \n" ;
put ") = subst_list_to_sut_in sut_input in \n" ;
put " let (";
put (format_string_list ", " fvnl_out) ;
put ") = subst_list_to_sut_out output_sl in \n" ;
put ") = env_in_to_sut_out sut_output in \n" ;
put " Oracle_idl_stub.oracle_step " ;
put (format_string_list " " fvnl_in) ;
put " " ;
......
......@@ -264,18 +264,18 @@ and
Hashtbl.add env_state.snt
(Bdd.dfalse ()) (Util.zero_sol, Util.one_sol);
main_loop 1 s n p rif [] ;
main_loop 1 s n p rif (Hashtbl.create 0) ;
flush stdout;
flush rif;
close_out rif;
and
main_loop t s n p rif output =
main_loop t s n p rif sut_output =
(* Generates `n*p' inputs from the environment *)
let (nll_inputs_loc: (node list list * env_out * env_loc) list)
= Env.env_try n p output
= Env.env_try n p sut_output
in
(* Extracts the inputs from the triple `node list * env_out * env_loc' *)
......@@ -284,17 +284,17 @@ and
in
(* Tries the sut `n*p'^nth times *)
let (outputs: env_in list) = List.map Lurette_stub.sut_try inputs in
let (sut_outputs: env_in list) = List.map Lurette_stub.sut_try inputs in
let _ =
if options.oracle
then
(* Tries the oracle `n*p'^nth times *)
let (results: bool list) =
List.map2 (fun x y -> Lurette_stub.oracle_try x y) inputs outputs
List.map2 (fun x y -> Lurette_stub.oracle_try x y) inputs sut_outputs
in
(* Aborts if at least one of the pairs (input, output) breaks the oracle *)
(* Aborts if at least one of the pairs (input, sut_output) breaks the oracle *)
if (List.mem false results)
then (
......@@ -322,13 +322,13 @@ and
print_string "\n*** sut inputs:" ;
print_subst_list i stdout;
print_string " sut outputs: " ;
print_subst_list o stdout
print_env_in o stdout
)
else
()
)
inputs
outputs
sut_outputs
results ;
flush stdout;
flush rif;
......@@ -342,19 +342,19 @@ and
(* Chooses among the `n*p' possible pairs (input, ouput) *)
let ran = Random.int (n*p) in
let new_output = List.nth outputs ran in
let new_sut_output = List.nth sut_outputs ran in
let (nll, input, loc) = List.nth nll_inputs_loc ran in
(* Performs the steps *)
let _ = Lurette_stub.sut_step input in
let _ = if (options.oracle) then Lurette_stub.oracle_step input output else true in
let _ = if (options.oracle) then Lurette_stub.oracle_step input new_sut_output else true in
Env.env_step nll input loc ;
let str =
if (options.step_by_step) then (
Show_env.generate_env_graph previous_nodes "environment" ;
Sim2chro.put_current_step_values
stdout t input output env_state.local options.display_local_var;
stdout t input sut_output env_state.local options.display_local_var;
output_string stderr
"\nOne more loop ? [type any char to stop, `CR' to continue]\n";
flush stderr;
......@@ -362,15 +362,15 @@ and
read_line ()
)
else (
Sim2chro.put_current_step_values
rif t input output env_state.local options.display_local_var;
Sim2chro.put_current_step_values
rif t input sut_output env_state.local options.display_local_var;
""
)
in
(* Decides whether to loop once more *)
if ((str = "") && (s > t))
then main_loop (t+1) s n p rif new_output else ();
then main_loop (t+1) s n p rif new_sut_output else ();
;;
......
......@@ -49,9 +49,9 @@ let (put_current_step_values: out_channel -> int -> env_out -> env_in -> env_loc
(fun (_, e) -> (print_atomic_expr e rif; put " "))
(Util.sort_list_string_pair input);
put "#outs ";
List.iter
(fun (_, e) -> (print_atomic_expr e rif; put " "))
(Util.sort_list_string_pair output);
Hashtbl.iter
(fun _ e -> (print_atomic_expr e rif; put " "))
output;
if display_local_var then
List.iter
......
......@@ -318,18 +318,18 @@ let (solve_formula: int -> formula list -> var_name list -> (subst list * subst
(* XXX Recompute the solution number everytime as long as the bdds interface sucks *)
let _ =
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 _ =
if not (Hashtbl.mem env_state.snt bdd)
then
let _ =
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 _ =
if not (Hashtbl.mem env_state.snt bdd)
then
let rec skip_var comb v =
if v = (Bdd.topvar comb) then comb else skip_var (Bdd.dthen comb) v
in
......
......@@ -20,200 +20,200 @@ rentrer_pass:bool
#step 1
f f f f f t f t t #outs
#step 2
f f t f f f t t f #outs t f f f f
f f t f f f t t f #outs f t f f f
#step 3
t f f t f f t f f #outs t f f f f
t f f t f f t f f #outs f t f f f
#step 4
t t f t f t f f t #outs t f f f f
t t f t f t f f t #outs f t f f f
#step 5
t f f t t f t f f #outs f t f t f
t f f t t f t f f #outs t f t f f
#step 6
t f f t f f t t t #outs f f f f f
#step 7
t t f t f f t t f #outs t f f f t