Commit 46927269 authored by Erwan Jahier's avatar Erwan Jahier

lurette 0.42 Wed, 13 Mar 2002 10:29:08 +0100 by jahier

Parent-Version:      0.41
Version-Log:

Make sure that n formula are drawn when even numeric failure occurs.
To do that, I recursively call draw_n_p_formula until the required
number of outputs have been generated.

Also fix a bug where my code was not handling cases where several
formulas corresponding to the same origin and target nodes (Lutin
probably won't generate such arcs explicitely, but it does
implicitely via epsilon transitions). The fix consist in adding
formula in wtree types instead of maintaining a table of formula
indexed by node list pairs. The env_state.formula_table is thus no
longer needed.

Project-Description: Lurette
parent 801c2882
;; This file is automatically generated, editing may cause PRCS to do
;; REALLY bad things.
(Created-By-Prcs-Version 1 3 3)
(test/usager.env 439 1015408234 b/14_usager.env 1.3)
(test/usager.env 424 1015605037 b/14_usager.env 1.4)
(doc/ocamldoc.sty 1380 1008328137 b/12_ocamldoc.s 1.1)
(source/env_state.ml 2871 1015504587 51_env_state. 1.13)
(source/graph.ml 1801 1015250295 14_graph.ml 1.4)
(source/util.ml 10405 1015514807 35_util.ml 1.13)
(source/wtree.ml 9644 1014051154 b/1_wtree.ml 1.8)
(source/solver.ml 14068 1015514807 39_solver.ml 1.15)
(source/env_state.ml 2787 1016011748 51_env_state. 1.14)
(source/graph.ml 1819 1016011748 14_graph.ml 1.5)
(source/util.ml 10907 1016011748 35_util.ml 1.14)
(source/wtree.ml 8518 1016011748 b/1_wtree.ml 1.9)
(source/solver.ml 13688 1016011748 39_solver.ml 1.16)
(source/command_line.ml 3971 1014048376 b/20_command_li 1.3)
(source/lurette.ml 11363 1015504587 12_lurette.ml 1.25)
(source/lurette.ml 11456 1016011748 12_lurette.ml 1.26)
(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 1461 1015514807 b/30_heater_flo 1.2)
(lurette.depfull.dot 49 1007651448 b/5_lurette.de 1.2)
(source/env.ml 9370 1015514807 16_env.ml 1.17)
(source/env.ml 9792 1016011748 16_env.ml 1.18)
(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 866 1015408234 b/17_passerelle 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/parse_env.mli 905 1015408234 40_parse_env. 1.5)
(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 8273 1015514807 49_eval.ml 1.10)
(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 9431 1015514807 41_parse_env. 1.7)
(source/parse_env.ml 9415 1015605037 41_parse_env. 1.8)
(interface/TAGS 1956 1007380262 26_TAGS 1.3)
(source/sim2chro.ml 2669 1015408234 b/24_sim2chro.m 1.4)
(doc/Interface_draft 5232 1003928781 19_Interface_ 1.1)
......@@ -35,16 +35,16 @@
(source/formula.mli 2161 1015250295 44_formula.ml 1.7)
(source/command_line.mli 1302 1014048376 b/21_command_li 1.3)
(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 3698 1015504587 50_env_state. 1.11)
(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/eval.mli 1665 1015408234 48_eval.mli 1.7)
(source/eval.mli 1413 1016011748 48_eval.mli 1.8)
(README 74 1011881677 10_README 1.2)
(test/ControleurPorte.c 9407 1012914629 b/19_Controleur 1.1)
(OcamlMakefile 19242 1015408234 17_OcamlMakef 1.20)
(test/ControleurPorte.rif.exp 4746 1015408234 b/29_Controleur 1.1)
(test/tram.env 944 1015408234 b/15_tram.env 1.2)
(OcamlMakefile 19189 1016011748 17_OcamlMakef 1.21)
(test/ControleurPorte.rif.exp 4746 1016011748 b/29_Controleur 1.2)
(test/tram.env 905 1015605037 b/15_tram.env 1.3)
(source/show_env.ml 2961 1014048376 43_show_env.m 1.3)
(doc/synthese 2556 1007379917 b/2_synthese 1.1)
(test/ControleurPorte.h 2306 1012914629 b/18_Controleur 1.1)
......@@ -53,10 +53,10 @@
(test/tram_simple.h 1746 1013519411 b/25_tram_simpl 1.1)
(Makefile 1758 1015514807 18_Makefile 1.23)
(test/vrai_tram.c 3060 1012914629 b/8_vrai_tram. 1.2)
(source/print.mli 597 1014048376 46_print.mli 1.5)
(source/print.mli 559 1016011748 46_print.mli 1.6)
(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 5525 1015504587 47_print.ml 1.10)
(source/print.ml 5533 1016011748 47_print.ml 1.11)
(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.20 Wed, 06 Mar 2002 10:50:34 +0100 jahier $
# $Id: OcamlMakefile 1.21 Wed, 13 Mar 2002 10:29:08 +0100 jahier $
#
###########################################################################
......@@ -520,7 +520,7 @@ test:
./lurette 30 10 10 temp_float.env --no-oracle -seed 1013219512 -ns2c ;\
diff -u heater_float.rif.exp lurette.rif > test3.res ; \
\
cat test1.res ; cat test2.res ; cat test3.res
ls -l test1.res test2.res test3.res
......@@ -541,8 +541,8 @@ gprof:
# In order to time profile lurette
ocamlprof:
$(LURETTE_DIR)/make_lurette ControleurPorte vrai_tram pbc; \
./lurette 4500 1 1 tram.env usager.env porte.env passerelle.env -seed 1014422484 -ns2c ;\
$(LURETTE_DIR)/make_lurette heater_float vrai_heater_float pbc; \
./lurette 10 10 10 temp_float.env -ns2c ;\
ocamlprof ../source/solver.ml > prof/solver.count.ml ; \
ocamlprof ../source/wtree.ml > prof/wtree.count.ml ; \
ocamlprof ../source/env.ml > prof/env.count.ml ; \
......
;; -*- Prcs -*-
(Created-By-Prcs-Version 1 3 3)
(Project-Description "Lurette")
(Project-Version lurette 0 41)
(Parent-Version lurette 0 40)
(Version-Log "
Change sligthly the ima format to make it more consistent.
(Project-Version lurette 0 42)
(Parent-Version lurette 0 41)
(Version-Log "
Make sure that n formula are drawn when even numeric failure occurs.
To do that, I recursively call draw_n_p_formula until the required
number of outputs have been generated.
Also fix a bug where my code was not handling cases where several
formulas corresponding to the same origin and target nodes (Lutin
probably won't generate such arcs explicitely, but it does
implicitely via epsilon transitions). The fix consist in adding
formula in wtree types instead of maintaining a table of formula
indexed by node list pairs. The env_state.formula_table is thus no
longer needed.
")
(New-Version-Log "")
(Checkin-Time "Fri, 08 Mar 2002 17:30:37 +0100")
(Checkin-Time "Wed, 13 Mar 2002 10:29:08 +0100")
(Checkin-Login jahier)
(Populate-Ignore ())
(Project-Keywords)
......@@ -19,18 +32,18 @@ Change sligthly the ima format to make it more consistent.
;; Sources files
(source/lurette.mli (lurette/11_lurette.ml 1.11 644))
(source/lurette.ml (lurette/12_lurette.ml 1.25 644))
(source/lurette.ml (lurette/12_lurette.ml 1.26 644))
(source/graph.mli (lurette/13_graph.mli 1.6 644))
(source/graph.ml (lurette/14_graph.ml 1.4 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.17 644))
(source/env.ml (lurette/16_env.ml 1.18 644))
(source/util.ml (lurette/35_util.ml 1.13 644))
(source/util.ml (lurette/35_util.ml 1.14 644))
(source/solver.mli (lurette/38_solver.mli 1.9 644))
(source/solver.ml (lurette/39_solver.ml 1.15 644))
(source/solver.ml (lurette/39_solver.ml 1.16 644))
(source/rnumsolver.mli (lurette/b/26_rnumsolver 1.1 644))
(source/rnumsolver.ml (lurette/b/27_rnumsolver 1.3 644))
......@@ -44,17 +57,17 @@ Change sligthly the ima format to make it more consistent.
(source/formula.mli (lurette/44_formula.ml 1.7 644))
(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.10 644))
(source/print.mli (lurette/46_print.mli 1.6 644))
(source/print.ml (lurette/47_print.ml 1.11 644))
(source/eval.mli (lurette/48_eval.mli 1.7 644))
(source/eval.ml (lurette/49_eval.ml 1.10 644))
(source/eval.mli (lurette/48_eval.mli 1.8 644))
(source/eval.ml (lurette/49_eval.ml 1.11 644))
(source/env_state.mli (lurette/50_env_state. 1.11 644))
(source/env_state.ml (lurette/51_env_state. 1.13 644))
(source/env_state.mli (lurette/50_env_state. 1.12 644))
(source/env_state.ml (lurette/51_env_state. 1.14 644))
(source/wtree.mli (lurette/b/0_wtree.mli 1.6 644))
(source/wtree.ml (lurette/b/1_wtree.ml 1.8 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.4 644))
......@@ -65,7 +78,7 @@ Change sligthly the ima format to make it more consistent.
(source/gen_stubs.ml (lurette/24_generate_l 1.19 644))
;; Make files
(OcamlMakefile (lurette/17_OcamlMakef 1.20 644))
(OcamlMakefile (lurette/17_OcamlMakef 1.21 644))
(Makefile (lurette/18_Makefile 1.23 644))
(test/Makefile (../Makefile) :symlink)
(interface/Makefile (lurette/25_Makefile 1.6 644))
......@@ -104,7 +117,7 @@ Change sligthly the ima format to make it more consistent.
(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.1 644))
(test/ControleurPorte.rif.exp (lurette/b/29_Controleur 1.2 644))
(test/heater_float.rif.exp (lurette/b/30_heater_flo 1.2 644))
......
......@@ -45,14 +45,13 @@ let _ = assert ( (add_missing_pre ["_pre3toto"; "_pre2titi"; "_pre2toto"])
= ["_pre2titi"; "_pre1titi"; "_pre3toto"; "_pre2toto"; "_pre1toto"] )
(* Exported *)
let (read_env_state_one_file : string -> node) =
fun file ->
(** Returns the initial node of the automata defined in
[file]. Also updates the various fields of [env_state] with the
content of [file]. *)
let
(* Reads the content of [file]. *)
(* Parses the content of [file]. *)
Parse_env.Automata(init_node, list_in, list_out, list_loc,
list_pre, list_arcs) =
try
......@@ -128,10 +127,9 @@ let (read_env_state : string list list -> unit) =
[]
files_ll
in
(* Sets the [current_nodes], [formula_table], and [wtree_table] fields
(* Sets the [current_nodes], and [wtree_table] fields
of [env_state]. *)
env_state.current_nodes <- nodes ;
env_state.formula_table <- (Wtree.build_formula_table env_state.graph);
env_state.wtree_table <- (Wtree.build_wtree_table env_state.graph)
......@@ -155,9 +153,9 @@ let (solve_formula_list: int -> node list list ->
** substitutions for local vars.
*)
let sl_sl_l = Solver.solve_formula p fl bool_vars_to_gen num_vnt_to_gen in
let nll_sl_sl_l =
(* Adds the target nodes to the substitutions *)
(* Adds the target nodes to the drawn substitutions *)
if acc = [] then
(* first formula *)
(List.map
(fun (sl1, sl2) ->
(nll, sl1, sl2))
......@@ -170,8 +168,7 @@ let (solve_formula_list: int -> node list list ->
sl_sl_l
acc
)
in
nll_sl_sl_l
let (solve_formula_list_list: int -> node list list * formula list list
-> (node list list * sl * sl) list) =
......@@ -204,10 +201,12 @@ let (solve_formula_list_list: int -> node list list * formula list list
([], [])
bvnl_nvntl_l
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
in
nll_sl_sl_l
let (get_wtrees: node list list -> Wtree.wtree_table -> Wtree.wtree list) =
fun nll wtt ->
(** Get the wtrees corresponding to the list of list of nodes
......@@ -250,6 +249,33 @@ let _ = assert (
[[[3]; [1; 2]], [[Bvar "c"]; [Bvar "a"; Bvar "b"]];
[[6]; [4; 5]], [[Bvar "f"]; [Bvar "d"; Bvar "e"]]]
)
let rec draw_n_p_values 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
in
let (nl_fl_ll, new_wtl) =
fold_left
(fun (acc1, acc2) (nl_fl_l, wt) ->
((append acc1 [nl_fl_l]), (append acc2 [wt])))
([], [])
nl_fl_l__wt__l
in
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 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)
(* Exported *)
......@@ -257,20 +283,11 @@ let (env_try: int -> int -> env_in ->
(node list list * env_out * env_loc) list) =
fun n p input ->
let cn_ll = env_state.current_nodes
and ft = env_state.formula_table
and wtt = env_state.wtree_table
in
let wtl = get_wtrees cn_ll wtt in
let fte = Eval.eval_wtree_list input wtl cn_ll in
(* Drawing n formula *)
let nl_fl_ll =
map2 (Wtree.choose_n_formula (Solver.is_satisfiable) n fte) cn_ll wtl
in
let nll_fll_l = merge_lll nl_fl_ll in
(* Drawing 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 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_l = flatten nll_sl_sl_ll in
assert (length nll_sl_sl_l = (n*p));
......
......@@ -34,7 +34,6 @@ type env_stateT = {
mutable snt: (Bdd.t, Util.sol_nb * Util.sol_nb) Hashtbl.t;
mutable current_nodes: node list list;
mutable graph: (node, arc_info) Graph.t ;
mutable formula_table: Wtree.formula_table ;
mutable wtree_table: Wtree.wtree_table ;
mutable pre: subst list;
mutable input : env_in ;
......@@ -57,7 +56,6 @@ let (env_state:env_stateT) = {
snt = Hashtbl.create 3;
current_nodes = [];
graph = Graph.create () ;
formula_table = Hashtbl.create 0 ;
wtree_table = Hashtbl.create 0 ;
pre = [] ;
input = Hashtbl.create 0 ;
......
......@@ -68,8 +68,6 @@ type env_stateT = {
mutable graph : (node, arc_info) Graph.t ;
(** The automata is stored in a Graph.t *)
mutable formula_table : (node * node, formula) Hashtbl.t ;
(** Mapping from pair of nodes to formula. *)
mutable wtree_table : Wtree.wtree_table ;
(** Mapping from nodes to [wtree] (see the doc of the [Wtree] module). *)
......
......@@ -12,6 +12,7 @@
open Formula
open Env_state
open Wtree
open List
(****************************************************************************)
......@@ -199,43 +200,47 @@ and
| Ival(i) -> Ival(i)
| Fval(f) -> Fval(f)
type coef = | I of int | F of float
type normal_expr = (coef * var_name) list
(* Hopefully, no variable should have that name ... *)
let (constant:var_name) = ""
let (is_constant : var_name -> bool) =
fun vn -> (vn = constant)
(* let (expr_to_nexpr: expr -> normal_expr) = *)
(* fun e -> *)
(* match e with *)
(* Sum(e1, e2) -> *)
(* | Diff(e1, e2) -> *)
(* | Prod(e1, e2) -> *)
(* | Quot(e1, e2) -> *)
(* | Mod(e1, e2) -> *)
(* | Nvar(str) -> *)
(* | Ival(i) -> Ival(i) *)
(* | Fval(f) -> Fval(f) *)
(****************************************************************************)
(****************************************************************************)
let rec (eval_wtree_list: env_in -> wtree list -> node list list ->
formula_table) =
fun input wtl nfll ->
(**
Returns a table of formula appearing in `wtl'; the formula are
evaluated w.r.t. `input'. `nfll' is the list of list of origin nodes
corresponding to the trees in `wtl' (necessary to get formula associated
to pair of nodes from env_state.formula_table).
*)
let ft = (Hashtbl.create (List.length wtl)) in
(List.iter2
(eval_wtree input ft)
wtl
nfll);
ft
and
(eval_wtree : env_in -> formula_table -> wtree -> node list -> unit) =
fun input ft wt nl ->
List.iter (eval_wnode input ft nl) wt
(* exported *)
let rec (eval_wtree : env_in -> wtree -> wtree) =
fun input wt ->
List.map (eval_wnode input) wt
and
(eval_wnode : env_in -> formula_table -> node list -> wnode -> unit) =
fun input ft nlf wn ->
(eval_wnode : env_in -> wnode -> wnode) =
fun input wn ->
match wn with
L(w, nlt) -> List.iter2 (add_formula input ft) nlf nlt
| N(w, wt) -> (eval_wtree input ft wt nlf)
and
(add_formula : env_in -> formula_table -> node -> node -> unit) =
fun input ft nf nt ->
let f = Hashtbl.find env_state.formula_table (nf, nt) in
let fe = eval f input in
Hashtbl.add ft (nf, nt) fe
L(w, nlt, fl) -> L(w, nlt, (List.map (fun f -> eval f input) fl))
| N(w, wt) -> N(w, (eval_wtree input wt))
(****************************************************************************)
......
......@@ -23,13 +23,9 @@ val eval : formula -> env_in -> formula
val eval_expr : expr -> env_in -> expr
(** Ditto for expressions. *)
val eval_wtree_list : env_in -> wtree list -> node list list
-> formula_table
(** [eval_wtree_list input wtl nfll] returns a table of the formula
appearing in [wtl]; the formula are evaluated
w.r.t. [input]. [nfll] is the list of list of origin nodes
corresponding to the trees in [wtl] (necessary to get formula
associated to pair of nodes from [env_state.formula_table]). *)
val eval_wtree : env_in -> wtree -> wtree
(** [eval_wtree input wt] returns the wtree [wt] with all its
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.,
......
......@@ -33,7 +33,7 @@ let (create: unit -> ('a, 'b) t) =
(* exported *)
let (get_list_of_target_nodes: ('a, 'b) t -> 'a -> ('a * 'b) list) =
fun g node ->
try Hashtbl.find g.table node
try List.flatten (Hashtbl.find_all g.table node)
with Not_found -> []
......
......@@ -195,6 +195,8 @@ and
and
(main2 : int -> int -> int -> 'a) =
fun s n p ->
(* Initialisation of `Env_state.env_state' *)
let env_llist = (get_env_from_args 4 []) in
let () = Env.read_env_state env_llist in
......@@ -272,6 +274,8 @@ and
and
main_loop t s n p rif sut_output =
(* let _ = print_string ("\n--- step " ^ (string_of_int t) ^ ":\n"); flush stdout in *)
(* Generates `n*p' inputs from the environment *)
let (nll_inputs_loc: (node list list * env_out * env_loc) list)
= Env.env_try n p sut_output
......
......@@ -45,19 +45,12 @@ let (arc_info : Formula.arc_info -> unit) =
open Wtree
let print_table_entry (n1, n2) f =
print_int n1 ;
print_string ", ";
print_int n2 ;
let print_table_entry nl f =
List.iter (fun i -> print_string ((string_of_int i) ^ ", ")) nl ;
print_string (" -> " ^ (Formula.formula_to_string f) ^ "\n")
let (pft: Wtree.formula_table -> unit) =
fun ft ->
Hashtbl.iter (print_table_entry) ft ;
flush stdout
(****************************************************************************)
......@@ -69,7 +62,6 @@ let (pft: Wtree.formula_table -> unit) =
(****************************************************************************)
open Wtree
let indent d =
let str = String.make d ' ' in
......@@ -81,18 +73,24 @@ let rec (pwt: int -> Wtree.wtree -> unit) =
flush stdout
and
pwn d = function
L(w, nl) ->
L(w, nl, fl) ->
indent d;
print_int w;
print_string " : node list = ";
List.iter (fun n -> print_int n; print_string ", ") nl ;
List.iter
(fun f ->
print_string (Formula.formula_to_string f);
print_string "\n")
fl;
flush stdout;
| N(w, wt) ->
indent d;
print_int w;
pwt (d+2) wt
let (pwtt: Wtree.wtree_table -> unit) =
let (pwtt: wtree_table -> unit) =
fun wtt ->
Hashtbl.iter (fun n wt ->
print_string "\nNoeud " ;
......
......@@ -12,7 +12,6 @@ val arc_info : Formula.arc_info -> unit
open Wtree
val pft: Wtree.formula_table -> unit
val pwt: int -> Wtree.wtree -> unit
val pwtt: Wtree.wtree_table -> unit
......
......@@ -303,13 +303,7 @@ let rec (draw_in_bdd: subst list * Rnumsolver.store -> Bdd.t -> Bdd.t ->
with No_numeric_solution ->
None
else
(
(* Update the table of sol nbs *)
if swap
then Hashtbl.replace env_state.snt bdd (n, zero_sol)
else Hashtbl.replace env_state.snt bdd (zero_sol, m);
None
)
None
in
match res_opt with
Some(res) -> res
......@@ -332,13 +326,7 @@ let rec (draw_in_bdd: subst list * Rnumsolver.store -> Bdd.t -> Bdd.t ->
else
draw_in_bdd (sl2, store2) bdd2 new_comb
else
(
(* Update the table of sol nbs *)
if swap
then Hashtbl.replace env_state.snt bdd (0, m)
else Hashtbl.replace env_state.snt bdd (n, 0);
raise No_numeric_solution
)
raise No_numeric_solution
else
raise No_numeric_solution
......@@ -408,5 +396,6 @@ let (solve_formula: int -> formula list -> vn list -> vnt list ->
in
try Util.unfold (draw bool_vars_to_gen num_vars_to_gen comb) bdd p
with No_numeric_solution ->
(* XXX I should rather redraw with an another formula *)
Hashtbl.replace env_state.snt bdd (zero_sol, zero_sol);
[]
......@@ -33,11 +33,27 @@ let rec (list_is_included: 'a list -> 'a list -> bool) =
list_is_included t1 (rm x1 l2)
else
false )
(** [count_empty_list llist] counts the number of empty list that
occurs in the list of list [llist] *)
let (count_empty_list : 'a list list -> int) =
fun llist ->
let (ell, _) = List.partition (fun l -> l = []) llist in
List.length ell
let _ = assert ((count_empty_list []) = 0)
let _ = assert ((count_empty_list [[1];[1];[1]]) = 0)
let _ = assert ((count_empty_list [[1];[];[1];[];[2;3]]) = 2)
(** Appends two lists and sorts the result *)
let append_and_sort l1 l2 =
List.sort (compare) (List.append l1 l2)
let append_and_sort_rev l1 l2 =
List.sort (fun x y -> compare y x) (List.append l1 l2)
(**
[list_are_equals l1 l2] tests if [l1] and [l2] contains the same elements
......
......@@ -12,47 +12,15 @@
(****************************************************************************)
open Formula
open List
type wtree = wnode list
and wnode = | L of int * node list
and wnode = | L of int * node list * formula list
| N of int * wtree
type wgraph = (node, int * formula_eps) Graph.t
type wtree_table = (node, wtree) Hashtbl.t