Commit 66e00627 authored by Erwan Jahier's avatar Erwan Jahier

lurette 0.66 Thu, 16 May 2002 10:54:38 +0200 by jahier

Parent-Version:      0.65
Version-Log:

solver.ml:
        Fix a bug is draw_in_bdd where it was unable to draw in a true
        formula when it was a top level one. The reason was that the
        tossing of remaining vars was not done at draw_in_bdd top level,
        which is wrong since true can appear on ima transitions.

Project-Description: Lurette
parent ee70bc48
;; -*- Prcs -*-
(Created-By-Prcs-Version 1 3 3)
(Project-Description "Lurette")
(Project-Version lurette 0 65)
(Parent-Version lurette 0 64)
(Project-Version lurette 0 66)
(Parent-Version lurette 0 65)
(Version-Log "
Outputs error message on stderr rather than on stdout.
solver.ml:
Fix a bug is draw_in_bdd where it was unable to draw in a true
formula when it was a top level one. The reason was that the
tossing of remaining vars was not done at draw_in_bdd top level,
which is wrong since true can appear on ima transitions.
")
(New-Version-Log "")
(Checkin-Time "Fri, 10 May 2002 16:54:24 +0200")
(Checkin-Time "Thu, 16 May 2002 10:54:38 +0200")
(Checkin-Login jahier)
(Populate-Ignore ())
(Project-Keywords)
......@@ -20,7 +25,7 @@ Outputs error message on stderr rather than on stdout.
;; 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.10 644))
(source/ima_exe.ml (lurette/b/32_ima_exe.ml 1.11 644))
(source/command_line_ima_exe.ml (lurette/b/33_command_li 1.3 644))
(source/command_line_ima_exe.mli (lurette/b/34_command_li 1.2 644))
......@@ -33,16 +38,16 @@ Outputs error message on stderr rather than on stdout.
(source/command_line.mli (lurette/b/21_command_li 1.6 644))
;; Sources files common to lurette and ima_exe
(source/graph.mli (lurette/13_graph.mli 1.7 644))
(source/graph.ml (lurette/14_graph.ml 1.5 644))
(source/graph.mli (lurette/13_graph.mli 1.8 644))
(source/graph.ml (lurette/14_graph.ml 1.6 644))
(source/env.mli (lurette/15_env.mli 1.13 644))
(source/env.ml (lurette/16_env.ml 1.26 644))
(source/env.ml (lurette/16_env.ml 1.27 644))
(source/util.ml (lurette/35_util.ml 1.20 644))
(source/solver.mli (lurette/38_solver.mli 1.11 644))
(source/solver.ml (lurette/39_solver.ml 1.21 644))
(source/solver.ml (lurette/39_solver.ml 1.22 644))
(source/rnumsolver.mli (lurette/b/26_rnumsolver 1.3 644))
(source/rnumsolver.ml (lurette/b/27_rnumsolver 1.6 644))
......@@ -65,8 +70,8 @@ Outputs error message on stderr rather than on stdout.
(source/env_state.mli (lurette/50_env_state. 1.18 644))
(source/env_state.ml (lurette/51_env_state. 1.21 644))
(source/wtree.mli (lurette/b/0_wtree.mli 1.10 644))
(source/wtree.ml (lurette/b/1_wtree.ml 1.12 644))
(source/wtree.mli (lurette/b/0_wtree.mli 1.11 644))
(source/wtree.ml (lurette/b/1_wtree.ml 1.13 644))
(source/sim2chro.mli (lurette/b/23_sim2chro.m 1.4 644))
(source/sim2chro.ml (lurette/b/24_sim2chro.m 1.8 644))
......
......@@ -169,6 +169,10 @@ let rec draw_n_p_values input n p cn_ll wtl =
constraints. We redraw as many times ([l]) as necessary. *)
append nll_call_sl_sl_ll (draw_n_p_values input l p cn_ll new_wtl)
(* XXX ce dernier appel va eventuellement echouer si, lors du tirage, *)
(* on a coup des branches que l'on aurait pu essayer. Il faut alors *)
(* relancer la construction des wtrees ... *)
(* Exported *)
let (env_try: int -> int -> env_in ->
......
(*-----------------------------------------------------------------------
** Copyright (C) 2001 - Verimag.
** Copyright (C) 2001, 2002 - Verimag.
** This file may only be copied under the terms of the GNU Library General
** Public License
**-----------------------------------------------------------------------
**
** File: graph.ml
** Main author: jahier@imag.fr
** Author: jahier@imag.fr
*)
(*------------------------------------------------------------------------*)
......
......@@ -5,7 +5,7 @@
**-----------------------------------------------------------------------
**
** File: graph.mli
** Main author: jahier@imag.fr
** Author: jahier@imag.fr
*)
(** A graph data structure as well as various functions that operates
......
......@@ -294,6 +294,14 @@ and
let previous_nodes = (Env_state.current_nodes ()) in
let nl = List.flatten previous_nodes in
let _ =
(* xxx --verbose !!! *)
(* List.iter *)
(* (fun n -> output_string stderr ((string_of_int n) ^ " ")) *)
(* nl; *)
(* flush stderr; *)
(* xxx *)
print_string ("\n# step " ^ (string_of_int t) ^ " (") ;
if (List.length nl) > 1
then
......@@ -301,7 +309,7 @@ and
print_string "current nodes are ";
List.iter
(fun n -> print_string ((string_of_int n) ^ " "))
(List.tl nl)
nl
)
else
(
......@@ -320,12 +328,6 @@ and
[(nll, call, out, loc)] -> (nll, call, out, loc)
| _ -> assert false
in
if options.show_automata then (
Show_env.generate_env_graph (flatten (Env_state.current_nodes ()))
[] ("automata" ^ (string_of_int (Hashtbl.hash Sys.argv)))
(Env_state.graph ())
);
Env.env_step nll call out loc ;
Env.update_pre (Env_state.input ()) (Env_state.output ()) (Env_state.local ()) ;
......@@ -335,6 +337,11 @@ and
Env_state.clear_bdd () ;
write_rif_output (Env_state.out_env_unsorted ()) out ;
if options.show_automata then (
Show_env.generate_env_graph (flatten (Env_state.current_nodes ()))
[] ("automata" ^ (string_of_int (Hashtbl.hash Sys.argv)))
(Env_state.graph ())
);
main_loop (t+1)
;;
......
......@@ -44,15 +44,14 @@ type comp = SupZero | SupEqZero | EqZero | NeqZero
let rec (formula_to_bdd : env_in -> formula -> Bdd.t * bool) =
fun input f ->
(** Replaces input and pre variables by their values in the
formula [f], and translates it into a bdd.
(** Returns the bdd of [f] and replaces input and pre variables
by their values.
Also returns a flag telling whether or not the formula depends
on input and pre vars. If this flag is true, the formula is
stored (cached) in a global table ([env_state.bdd_tbl]);
Also returns a flag that is true iff the formula depends on
input and pre vars. If this flag is false, the formula is
stored (cached) in a global table ([env_state.bdd_tbl_global]);
otherwise, it is stored in a table that is cleared at each new
step ([env_state.bdd_tbl_global]).
step ([env_state.bdd_tbl]).
*)
try (Env_state.bdd f, true)
with Not_found ->
......@@ -91,7 +90,7 @@ let rec (formula_to_bdd : env_in -> formula -> Bdd.t * bool) =
( match (lookup input (Env_state.pre ()) vn) with
Some(B(bool)) ->
if bool
then (Bdd.dtrue (Env_state.bdd_manager ()), true)
then (Bdd.dtrue (Env_state.bdd_manager ()), true)
else (Bdd.dfalse (Env_state.bdd_manager ()), true)
| Some(_) ->
print_string (vn ^ " is not a boolean!\n");
......@@ -105,7 +104,7 @@ let rec (formula_to_bdd : env_in -> formula -> Bdd.t * bool) =
^ "*** or a pre on a input var at the second step in "
^ "your formula in the environment.\n ")
else (Bdd.ithvar (Env_state.bdd_manager ())
(Env_state.atomic_formula_to_index (Bv(vn))), false)
(Env_state.atomic_formula_to_index (Bv(vn))), false)
)
| Eq(e1, e2) ->
......@@ -192,16 +191,16 @@ and
( match (lookup input (Env_state.pre ()) str) with
Some(N(I(i))) ->
( (GneMap.add
(NeMap.add "" (I(i)) NeMap.empty)
(Bdd.dtrue (Env_state.bdd_manager ()))
GneMap.empty),
(NeMap.add "" (I(i)) NeMap.empty)
(Bdd.dtrue (Env_state.bdd_manager ()))
GneMap.empty),
true
)
| None ->
( (GneMap.add
(NeMap.add str (I(1)) NeMap.empty)
(Bdd.dtrue (Env_state.bdd_manager ()))
GneMap.empty),
(NeMap.add str (I(1)) NeMap.empty)
(Bdd.dtrue (Env_state.bdd_manager ()))
GneMap.empty),
false
)
| Some(N(F(f))) ->
......@@ -218,16 +217,16 @@ and
( match (lookup input (Env_state.pre ()) str) with
Some(N(F(f))) ->
( (GneMap.add
(NeMap.add "" (F(f)) NeMap.empty)
(Bdd.dtrue (Env_state.bdd_manager ()))
GneMap.empty),
(NeMap.add "" (F(f)) NeMap.empty)
(Bdd.dtrue (Env_state.bdd_manager ()))
GneMap.empty),
true
)
| None ->
( (GneMap.add
(NeMap.add str (F(1.)) NeMap.empty)
(Bdd.dtrue (Env_state.bdd_manager ()))
GneMap.empty),
(NeMap.add str (F(1.)) NeMap.empty)
(Bdd.dtrue (Env_state.bdd_manager ()))
GneMap.empty),
false
)
| Some(N(I(i))) ->
......@@ -242,17 +241,17 @@ and
| Ival(i) ->
( (GneMap.add
(NeMap.add "" (I(i)) NeMap.empty)
(Bdd.dtrue (Env_state.bdd_manager ()))
GneMap.empty),
(NeMap.add "" (I(i)) NeMap.empty)
(Bdd.dtrue (Env_state.bdd_manager ()))
GneMap.empty),
false
)
| Fval(f) ->
( (GneMap.add
(NeMap.add "" (F(f)) NeMap.empty)
(Bdd.dtrue (Env_state.bdd_manager ()))
GneMap.empty),
(NeMap.add "" (F(f)) NeMap.empty)
(Bdd.dtrue (Env_state.bdd_manager ()))
GneMap.empty),
false
)
......@@ -283,15 +282,15 @@ and
(gne, dep1 || dep2 || dep3)
in
(gne, dep)
and
(gne_to_bdd : Gne.gn_expr -> comp -> Bdd.t) =
fun gne cmp ->
(** Use [cmp] to compare [gne] with 0 and returns the
corresponding formula. E.g., if [gne] is bounded to
[e1 -> c1; e2 -> c2], then [gne_to_bdd gne SupZero] returns
(the bdd corresponding to) the formula [(c1 and (e1 > 0)) or
(c2 and (e2 > 0))] *)
corresponding formula. E.g., if [gne] is bounded to
[e1 -> c1; e2 -> c2], then [gne_to_bdd gne SupZero] returns
(the bdd corresponding to) the formula [(c1 and (e1 > 0)) or
(c2 and (e2 > 0))] *)
match cmp with
SupZero ->
( GneMap.fold
......@@ -604,117 +603,104 @@ let rec (draw_in_bdd: subst list * store -> Bdd.t -> Bdd.t ->
path in [bdd] leads to a satisfiable set of numeric
constraints.
*)
let _ = assert (not (Bdd.is_cst bdd)) in
let _ = assert (Env_state.sol_number_exists bdd) in
let bddvar = Bdd.topvar bdd in
let af = (Env_state.index_to_atomic_formula bddvar) in
let top_var_is_numeric = is_a_numeric_constraint af in
if
bddvar <> (Bdd.topvar comb) &&
not top_var_is_numeric
then
let new_sl =
match toss_up_one_var (Bdd.topvar comb) with
Some(s) -> s::sl
| None -> sl
in
draw_in_bdd (new_sl, store) bdd (Bdd.dthen comb)
else
(* bddvar = combvar xor top_var_is_numeric *)
(* nb: I handle those two cases alltogether to avoid code
duplication (i.e., retrieving sol numbers, performing the
toss, the recursive call, handling the base case where a
dtrue bdd is reached, etc). It makes the code a little
bit more obscur, but ... *)
let (n, m) = Env_state.sol_number bdd in
let _ =
if ((eq_sol_nb n zero_sol) && (eq_sol_nb m zero_sol))
then raise No_numeric_solution ;
in
let (store_plus_af, store_plus_not_af) =
(* A first trick to avoid code dup (cf nb above) *)
if top_var_is_numeric
then
split_store store af
else
(store, store)
in
let (swap, store1, bdd1, bool1, sol_nb1, store2, bdd2, bool2, sol_nb2) =
(* Depending on the result of a toss (based on the number
of solution in each branch), we try the [else] or the
[then] branch first. [swap] indicates whether or not the
[else] part is put before the [then] one. *)
let ran = Random.float 1. in
if ran < ((float_of_sol_nb n) /. (float_of_sol_nb (add_sol_nb n m)))
then
(false, store_plus_af, (Bdd.dthen bdd), true, n,
store_plus_not_af, (Bdd.delse bdd), false, m )
if Bdd.is_true bdd
then
(* Toss the remaining bool vars. *)
( (List.append sl
(Util.list_map_option toss_up_one_var (Bdd.list_of_support comb))),
store )
else
let _ = assert (not (Bdd.is_false bdd)) in
let _ = assert (Env_state.sol_number_exists bdd) in
let bddvar = Bdd.topvar bdd in
let af = (Env_state.index_to_atomic_formula bddvar) in
let top_var_is_numeric = is_a_numeric_constraint af in
if
bddvar <> (Bdd.topvar comb) &&
not top_var_is_numeric
then
let new_sl =
match toss_up_one_var (Bdd.topvar comb) with
Some(s) -> s::sl
| None -> sl
in
draw_in_bdd (new_sl, store) bdd (Bdd.dthen comb)
else
(* bddvar = combvar xor top_var_is_numeric *)
(* nb: I handle those two cases alltogether to avoid code
duplication (i.e., retrieving sol numbers, performing the
toss, the recursive call, handling the base case where a
dtrue bdd is reached, etc). It makes the code a little
bit more obscur, but ... *)
let (n, m) = Env_state.sol_number bdd in
let _ =
if ((eq_sol_nb n zero_sol) && (eq_sol_nb m zero_sol))
then raise No_numeric_solution ;
in
let (store_plus_af, store_plus_not_af) =
(* A first trick to avoid code dup (cf nb above) *)
if top_var_is_numeric
then
split_store store af
else
(true, store_plus_not_af, (Bdd.delse bdd), false, m,
store_plus_af, (Bdd.dthen bdd), true, n )
in
let (sl1, sl2, new_comb) = (
(* A second trick to avoid code dup (cf nb above) *)
match af with
Bv(vn) ->
(((vn, Formula.B(bool1))::sl),
((vn, Formula.B(bool2))::sl),
(if Bdd.is_true comb then comb else Bdd.dthen comb) )
| _ ->
(* top_var_is_numeric *)
(sl, sl, comb)
(store, store)
in
let (swap, store1, bdd1, bool1, sol_nb1, store2, bdd2, bool2, sol_nb2) =
(* Depending on the result of a toss (based on the number
of solution in each branch), we try the [else] or the
[then] branch first. [swap] indicates whether or not the
[else] part is put before the [then] one. *)
let ran = Random.float 1. in
if ran < ((float_of_sol_nb n) /. (float_of_sol_nb (add_sol_nb n m)))
then
(false, store_plus_af, (Bdd.dthen bdd), true, n,
store_plus_not_af, (Bdd.delse bdd), false, m )
else
(true, store_plus_not_af, (Bdd.delse bdd), false, m,
store_plus_af, (Bdd.dthen bdd), true, n )
in
let (sl1, sl2, new_comb) = (
(* A second trick to avoid code dup (cf nb above) *)
match af with
Bv(vn) ->
(((vn, Formula.B(bool1))::sl),
((vn, Formula.B(bool2))::sl),
(if Bdd.is_true comb then comb else Bdd.dthen comb) )
| _ ->
(* top_var_is_numeric *)
(sl, sl, comb)
)
in
let res_opt =
(* A solution will be found in this branch iff there exists
at least one path in the bdd that leads to a satisfiable
set of numeric constraints. If it is not the case,
[res_opt] is bound to [None]. *)
if not (is_empty store1)
then
try
let tail_draw1 =
if Bdd.is_true bdd1
then
(* Toss the remaining bool vars. *)
( (List.append
sl1
(Util.list_map_option toss_up_one_var (Bdd.list_of_support new_comb))),
store1
)
else
draw_in_bdd (sl1, store1) bdd1 new_comb
in
Some(tail_draw1)
with No_numeric_solution ->
in
let res_opt =
(* A solution will be found in this branch iff there exists
at least one path in the bdd that leads to a satisfiable
set of numeric constraints. If it is not the case,
[res_opt] is bound to [None]. *)
if not (is_empty store1)
then
try
let tail_draw1 = draw_in_bdd (sl1, store1) bdd1 new_comb in
Some(tail_draw1)
with No_numeric_solution ->
None
else
None
else
None
in
match res_opt with
Some(res) -> res
| None ->
(* The second branch is now tried because no path in
the first bdd leaded to a satisfiable set of
numeric constraints. *)
if not (eq_sol_nb sol_nb2 zero_sol)
then
if not (is_empty store2)
then
if Bdd.is_true bdd2
then
( (List.append
sl2
(Util.list_map_option toss_up_one_var
(Bdd.list_of_support new_comb))),
store2
)
in
match res_opt with
Some(res) -> res
| None ->
(* The second branch is now tried because no path in
the first bdd leaded to a satisfiable set of
numeric constraints. *)
if not (eq_sol_nb sol_nb2 zero_sol)
then
if not (is_empty store2)
then draw_in_bdd (sl2, store2) bdd2 new_comb
else
draw_in_bdd (sl2, store2) bdd2 new_comb
raise No_numeric_solution
else
raise No_numeric_solution
else
raise No_numeric_solution
let (draw : vn list -> vnt list -> Bdd.t -> Bdd.t -> subst list * subst list) =
......
(*-----------------------------------------------------------------------
** Copyright (C) 2001 - Verimag.
** Copyright (C) 2001, 2002 - Verimag.
** This file may only be copied under the terms of the GNU Library General
** Public License
**-----------------------------------------------------------------------
......@@ -26,37 +26,6 @@ and wnode = | L of int * node list * formula list * cpt_action list
type wgraph = (node, arc_info) Graph.t
type wtree_table = (node, wtree) Hashtbl.t
(****************************************************************************)
(****************************************************************************)
(* Exported *)
let rec (rm_elt: node list -> wtree -> wtree) =
fun nl wt ->
let _ = assert (Util.sorted nl) in
(*
** To call when a (conjunction of) formula is unsatisfiable.
*)
match wt with
[] -> []
| L(w, list, fl, act)::tail ->
if nl = list
then tail
else L(w, list, fl, act)::(rm_elt nl tail)
| N(w, swt)::tail ->
let new_swt = rm_elt nl swt in
if (new_swt = swt)
then
N(w, swt)::(rm_elt nl tail)
else
(* Each list of nodes ougth to appear at most once.
Hence it is useless to try to remove it if it has
already been removed somewhere. *)
if (new_swt = [])
(* Remove empty sub trees. *)
then tail
else N(w, new_swt)::tail
(****************************************************************************)
......@@ -145,29 +114,31 @@ let indent d =
print_string ("\n" ^ str)
let rec (pwt: int -> wtree -> unit) =
fun d wt ->
List.iter (pwn d) wt ;
flush stdout
fun d wt ->
if wt = [] then output_string stderr "[]"
else List.iter (pwn d) wt ;
flush stderr
and
pwn d = function
L(w, nl, fl, act) ->
indent d;
print_string "weigth = ";
output_string stderr "weigth = ";
print_int w;
print_string ", nodes = [";
List.iter (fun n -> print_int n; print_string ", ") nl ;
output_string stderr ", nodes = [";
List.iter (fun n -> print_int n; output_string stderr ", ") nl ;
List.iter
(fun f ->
print_string "] formula = ";
print_string (Formula.formula_to_string f);
print_string ", actions = [";
List.iter (fun ca -> print_string (cpt_action_to_string ca)) act;
print_string "]\n")
output_string stderr "] formula = ";
output_string stderr (Formula.formula_to_string f);
output_string stderr ", actions = [";
List.iter (fun ca -> output_string stderr (cpt_action_to_string ca)) act;
output_string stderr "]\n")
fl;
flush stdout;
| N(w, wt) ->
indent d;
print_string "weigth = ";
output_string stderr "weigth = ";
print_int w;
pwt (d+2) wt
......@@ -176,31 +147,34 @@ let rec (build_wtree: wgraph -> node -> wtree) =
fun graph node ->
(** Builds the [wtree] of [graph] starting from [node]. *)
let wt = build_wtree_acc false graph [] node in
try
let nlc = Env_state.get_loop_cpt node in
if nlc = 0.
then wt
else
(*
If the current node is a loop node and if its loop cpt
is different from 0, then we also compute the [wtree]
corresponding to the case where this cpt is 0, because
it will be needed whenever no formula is satisfiable
in the loop. Note that we compute it in a second pass
to avoid loops via epsilon transitions. A boolean flag
is used in argument of build_wtree_acc to associate a
weigth of 0 to that branch. Then later, when drawing a
formula in the wtree, those formula with weigth 0 will
be taken if no more formula with non-0 weigth can be
taken (because all of them are insatisfiable).
*)
let _ = Env_state.set_loop_cpt node 0. in
let wt_backtrack = build_wtree_acc true graph [] node in
Env_state.set_loop_cpt node nlc ;
(append wt wt_backtrack)
with Not_found
(* Current node is not a loop node *)
-> wt
(* try *)
(* let nlc = Env_state.get_loop_cpt node in *)
(* if nlc = 0. *)
(* then wt *)
(* else *)
(* (* *)
(* If the current node is a loop node and if its loop cpt *)
(* is different from 0, then we also compute the [wtree] *)
(* corresponding to the case where this cpt is 0, because *)
(* it will be needed whenever no formula is satisfiable *)
(* in the loop. Note that we compute it in a second pass *)
(* to avoid loops via epsilon transitions. A boolean flag *)
(* is used in argument of build_wtree_acc to associate a *)
(* weigth of 0 to that branch. Then later, when drawing a *)
(* formula in the wtree, those formula with weigth 0 will *)
(* be taken if no more formula with non-0 weigth can be *)
(* taken (because all of them are insatisfiable). *)
(* *) *)
(* let _ = Env_state.set_loop_cpt node 0. in *)
(* let wt_backtrack = build_wtree_acc true graph [] node in *)
(* Env_state.set_loop_cpt node nlc ; *)
(* (append wt wt_backtrack) *)
(* with Not_found *)