Commit 3cde6aa1 authored by erwan's avatar erwan

Update: monadisation of Lutin, part 5 + remove support for the fair mode.

Rationale: make rdbg time traveling work.

Rationale for removing the fair mode:
 - the code for choosing the mode was ugly
 - it duplicates the effort
 - they other means to be fair (via weigths)
 - it can be very expensive (it breaks the sharing in the bdd, and computing
   polyedron volume is costly). hence it is not in the spirit of all the tradeoffs
   used elsewhere in design choices.
 - I've never used it (well, except in the tuto...)
parent 9d0c853a
......@@ -41,7 +41,7 @@ Library lutin
Install:true
CompiledObject: native
XMETAEnable: true
InternalModules: Auto2Lucky,AutoGen,Bddd,CheckEnv,CheckType,CkIdentInfo,CkTypeEff,CoAlgExp,CoIdent,CoTraceExp,Constraint,Draw,Exp,ExpEval,Expand,ExprUtil,FGen,Fair_bddd,Formula_to_bdd,GenOcamlGlue,Glue,Gne,Guard,Lexeme,LoopWeights,Luc2alice,Luc2c,LucFGen,Lucky,LutErrors,LutExe,LutLexer,LutParser,LutPredef,LutProg,Version,MainArg,Ne,Parsers,Poly_draw,Polyhedron,Prevar,Prog,Reactive,Rif,Sol_nb,Solver,Store,Syntaxe,SyntaxeDump,Thickness,Type,Util,Utils,Value,Var,Verbose
InternalModules: Auto2Lucky,AutoGen,Bddd,CheckEnv,CheckType,CkIdentInfo,CkTypeEff,CoAlgExp,CoIdent,CoTraceExp,Constraint,Draw,Exp,ExpEval,Expand,ExprUtil,FGen,Formula_to_bdd,GenOcamlGlue,Glue,Gne,Guard,Lexeme,LoopWeights,Luc2alice,Luc2c,LucFGen,Lucky,LutErrors,LutExe,LutLexer,LutParser,LutPredef,LutProg,Version,MainArg,Ne,Parsers,Poly_draw,Polyhedron,Prevar,Prog,Reactive,Rif,Sol_nb,Solver,Store,Syntaxe,SyntaxeDump,Thickness,Type,Util,Utils,Value,Var,Verbose
DllLib: libgmp.so dllcamlidl.so
Library bddrand
......
......@@ -491,15 +491,8 @@ and
(* Manager.disable_autodyn (Env_state.bdd_manager ()); *)
(* selecting the draw mode *)
if
options.compute_volume
then
Solver.set_fair_mode ()
else
Solver.set_efficient_mode ();
(* Initializing the solution number table *)
!Solver.init_snt ();
itime := 0;
(* Luciole communication channels *)
......
......@@ -512,9 +512,6 @@ let (start : unit -> Event.t) =
let loc = None in
let _ =
if args.compute_volume then Solver.set_fair_mode ()
else Solver.set_efficient_mode ();
!Solver.init_snt ();
Random.init seed;
Rif.write oc ("# This is lurette Version " ^ Version.str ^
......
(* Time-stamp: <modified the 20/11/2018 (at 10:05) by Erwan Jahier> *)
(* Time-stamp: <modified the 12/04/2019 (at 15:40) by Erwan Jahier> *)
(** todo : Parse constraints given in Lustre/Lutin like syntax *)
let (contraints : string -> (string * bool) list) = fun f -> assert false
......@@ -21,8 +21,9 @@ let (draw : ?number:int -> Exp.var list -> Exp.var list -> Exp.formula ->
fun ?(number=1) bvl nvl f ->
let bool_vars_to_gen: Exp.formula = get_vars_f bvl in
let output_var_names : Var.name list list = [List.map Var.name bvl] in
let outs_l =
Solver.solve_formula empty empty !verbose "[BddRandom.draw]"
let snt = Solver.init () in
let snt, outs_l =
Solver.solve_formula snt empty empty !verbose "[BddRandom.draw]"
output_var_names number (1, 0, AtMost 0) bool_vars_to_gen nvl f
in
let outs_l = fst (List.split outs_l) in (* throw numerics away for the time being *)
......
This diff is collapsed.
......@@ -15,10 +15,10 @@
ZZZ : To be used by Solver only !!
*)
type t
val draw_in_bdd : Var.env_in -> Var.env -> int -> string -> Exp.var list ->
Bdd.t -> Bdd.t -> Var.env * Store.t' * Store.p
val draw_in_bdd : t -> Var.env_in -> Var.env -> int -> string -> Exp.var list ->
Bdd.t -> Bdd.t -> t * Var.env * Store.t' * Store.p
(** [draw_in_bdd memory verbose_level ctx_msg state vars bdd comb]
returns a draw of the Boolean variables as well as a range based
and a polyhedron based representation of numeric constraints
......@@ -32,21 +32,16 @@ val draw_in_bdd : Var.env_in -> Var.env -> int -> string -> Exp.var list ->
open Sol_nb
val sol_number : Bdd.t -> sol_nb * sol_nb
val sol_number : t -> Bdd.t -> sol_nb * sol_nb
(** [sol_number bdd] returns the solution number in the [then] and [else]
branches of [bdd]. *)
(**/**)
val add_snt_entry : Bdd.t -> sol_nb * sol_nb -> unit
val add_snt_entry : t -> Bdd.t -> sol_nb * sol_nb -> t
(** mofifies an entry. usefull whenever we realize latter that a bdd
represents a formula that is unsatifiable for numerical reasons. *)
val init_snt : unit -> unit
val clear_snt : unit -> unit
(** For debugging *)
val bdd_to_int : (Bdd.t, int) Hashtbl.t
val init_snt : unit -> t
......@@ -131,7 +131,10 @@ and
in
let ctx_msg = Prog.ctrl_state_to_string_long state.d.ctrl_state in
Utils.time_C "is_sat";
let sat = (Solver.is_satisfiable input state.d.memory state.d.verbose ctx_msg facc' "") in
let snt, sat =
assert false;
Solver.is_satisfiable state.d.snt input state.d.memory state.d.verbose ctx_msg facc' ""
in
Utils.time_R "is_sat";
if sat then (cont', facc', n)
else choose_one_formula_atomic input state facc cont'
......
......@@ -41,13 +41,14 @@ let (draw_values : Var.env_in -> Prog.state -> int -> Thickness.numeric ->
let ctx_msg = Prog.ctrl_state_to_string_long state.d.ctrl_state in
let vl = state.d.verbose in
let ra, f, cs = ra.FGen.choose_one_formula () in
match
Solver.solve_formula input state.d.memory vl ctx_msg state.s.output_var_names p
num_thickness bool_to_gen_f num_to_gen f
assert false;
match
Solver.solve_formula state.d.snt input state.d.memory vl ctx_msg
state.s.output_var_names p num_thickness bool_to_gen_f num_to_gen f
with
| [] -> (* The constraint is unsatisfiable because of the numerics *)
| snt, [] -> (* The constraint is unsatisfiable because of the numerics *)
loop_choose_formula bool_to_gen_f num_to_gen ra
| sol_l -> ra, f, cs, sol_l
| _,sol_l -> ra, f, cs, sol_l
in
let (ral, fl, csl, sol_ll) =
Util.list_split4(
......@@ -182,57 +183,57 @@ let (env_try : Thickness.t -> env_in -> Prog.state -> FGen.t list ->
(*****************************************************************************)
(* Exported *)
let (env_step : step_mode -> env_in -> Prog.state -> FGen.t list ->
Prog.state * solution) =
Prog.state * solution) =
fun step_mode input state ral ->
let thick =
match step_mode with
| StepInside -> (1, 0, Thickness.AtMost 0)
| StepEdges -> (0, 1, Thickness.AtMost 0)
| StepVertices -> (0, 0, Thickness.AtMost 1)
in
try
Utils.time_C "env_try_do";
let (_ral', csl, soll) = env_try_do (1, thick) input state ral [] in
Utils.time_R "env_try_do";
let (output, local) = assert( soll <> []); List.hd soll in
let new_state_dyn = {
memory = update_pre input output local state;
ctrl_state = csl;
last_input = input;
last_output = output;
last_local = local;
verbose = state.d.verbose
}
in
let new_state = { d = new_state_dyn ; s = state.s } in
(* Clean-up cached info that depends on pre or inputs *)
Formula_to_bdd.clear_step ();
!Solver.clear_snt ();
previous_output := Some output;
previous_local := Some local;
(new_state, (output, local))
with
FGen.NoMoreFormula ->
match (!previous_output, !previous_local) with
| Some(out), Some(loc) ->
if state.s.reactive then
(
if state.d.verbose >= 1 then
print_string (
"### No transition is available; " ^
"values of the previous cycle are used.\n");
flush stdout;
(state, (out, loc))
)
else
(
if state.d.verbose >= 1 then
print_string (
"# No transition is labelled by a satisfiable formula.\n" ^
"# The program is blocked.\n");
flush stdout;
raise FGen.NoMoreFormula
)
| _, _ -> raise FGen.NoMoreFormula
let thick =
match step_mode with
| StepInside -> (1, 0, Thickness.AtMost 0)
| StepEdges -> (0, 1, Thickness.AtMost 0)
| StepVertices -> (0, 0, Thickness.AtMost 1)
in
try
Utils.time_C "env_try_do";
let (_ral', csl, soll) = env_try_do (1, thick) input state ral [] in
Utils.time_R "env_try_do";
let (output, local) = assert( soll <> []); List.hd soll in
let new_state_dyn = {
memory = update_pre input output local state;
ctrl_state = csl;
last_input = input;
last_output = output;
last_local = local;
snt = state.d.snt;
verbose = state.d.verbose
}
in
let new_state = { d = new_state_dyn ; s = state.s } in
(* Clean-up cached info that depends on pre or inputs *)
Formula_to_bdd.clear_step ();
previous_output := Some output;
previous_local := Some local;
(new_state, (output, local))
with
FGen.NoMoreFormula ->
match (!previous_output, !previous_local) with
| Some(out), Some(loc) ->
if state.s.reactive then
(
if state.d.verbose >= 1 then
print_string (
"### No transition is available; " ^
"values of the previous cycle are used.\n");
flush stdout;
(state, (out, loc))
)
else
(
if state.d.verbose >= 1 then
print_string (
"# No transition is labelled by a satisfiable formula.\n" ^
"# The program is blocked.\n");
flush stdout;
raise FGen.NoMoreFormula
)
| _, _ -> raise FGen.NoMoreFormula
......@@ -75,30 +75,11 @@ let (bool2bool : Value.t -> value) =
(****************************************************************************)
let sol_number = ref Bddd.sol_number
let draw_in_bdd = ref Bddd.draw_in_bdd
let add_snt_entry = ref Bddd.add_snt_entry
let init_snt = ref Bddd.init_snt
let clear_snt = ref Bddd.clear_snt
let (set_efficient_mode : unit -> unit) =
fun _ ->
sol_number := Bddd.sol_number;
draw_in_bdd := Bddd.draw_in_bdd;
add_snt_entry := Bddd.add_snt_entry;
init_snt := Bddd.init_snt;
clear_snt := Bddd.clear_snt;
!clear_snt ()
let (set_fair_mode : unit -> unit) =
fun _ ->
sol_number := Fair_bddd.sol_number;
draw_in_bdd := Fair_bddd.draw_in_bdd;
add_snt_entry := Fair_bddd.add_snt_entry;
init_snt := Fair_bddd.init_snt;
clear_snt := Fair_bddd.clear_snt;
!clear_snt ()
let sol_number = Bddd.sol_number
let draw_in_bdd = Bddd.draw_in_bdd
let add_snt_entry = Bddd.add_snt_entry
let init_snt = Bddd.init_snt
(****************************************************************************)
......@@ -343,7 +324,7 @@ let (draw : ?mode:(draw_mode) -> ?verbose:(int) -> solutions_set -> solution lis
let (k1, k2, k3) = mode in
let msg = Prog.ctrl_state_to_string_long ss.state.d.ctrl_state in
let (bool_subst_tab, store_range, store_poly) =
!draw_in_bdd Value.OfIdent.empty ss.state.d.memory ss.state.d.verbose msg ss.nums_tg ss.bdd ss.comb
draw_in_bdd Value.OfIdent.empty ss.state.d.memory ss.state.d.verbose msg ss.nums_tg ss.bdd ss.comb
in
let bool_subst_l = Value.OfIdent.content bool_subst_tab in
let num_subst_ll0 =
......@@ -435,7 +416,6 @@ let (print_solution : solution -> unit) =
let _ =
!init_snt ();
random_seed ()
(******************************************************************************)
......
(** Time-stamp: <modified the 15/07/2011 (at 10:15) by Erwan Jahier> *)
(** Time-stamp: <modified the 12/04/2019 (at 14:34) by Erwan Jahier> *)
(*
** File: luckyDraw.mli
** Author: jahier@imag.fr
......@@ -128,18 +128,6 @@ type draw_mode = int * int * int
val draw : ?mode:(draw_mode) -> ?verbose:(int) -> solutions_set -> solution list
(******************************************************************************)
(** {2 Drawing heuristics} *)
val set_efficient_mode : unit -> unit
(** Default mode. The draw in the set of solutions is not fair w.r.t numeric variables. *)
val set_fair_mode : unit -> unit
(** In that mode, we take into account the number of numeric
solutions by computing (an approx.) of the volume of polyhedra to
perform the draw. It is therefore more expensive. Moreover, some
of the sharing of the BDDs is lost. *)
(******************************************************************************)
(** {2 Pretty-printing} *)
......
......@@ -77,6 +77,7 @@ type t = {
bool_vars_to_gen: Exp.formula;
(* ... and var list for nums ! *)
num_vars_to_gen: Exp.var list;
snt: Solver.t;
}
let in_var_list it = it.in_vars
......@@ -228,6 +229,7 @@ let of_expanded_code (opt:MainArg.t) (exped: Expand.t) = (
out_var_names = ovns;
bool_vars_to_gen = bvf;
num_vars_to_gen = nvs;
snt = Solver.init();
}
)
......@@ -251,7 +253,6 @@ let make opt infile mnode = (
let tlenv = CheckType.check_pack libs mainprg in
Verbose.put ~flag:dbg "LutExe.make: CheckType.check_pack OK\n";
let _ = !Solver.clear_snt (); !Solver.init_snt () in
let mnode = if mnode <> "" then mnode else (
let all_nodes = Hashtbl.fold
(fun n _ acc -> n::acc)
......@@ -417,7 +418,7 @@ let find_some_sols
let zesol,bdd = (
let solver_vl = ref 0 in
Verbose.exe ~flag:dbg (fun _ -> solver_vl := 3);
let is_bool_sat,bdd = Solver.is_satisfiable_bdd
let snt, is_bool_sat,bdd = Solver.is_satisfiable_bdd it.snt
Value.OfIdent.empty (* input: Var.env_in *)
Value.OfIdent.empty (* memory: Var.env *)
(* !solver_vl *)
......@@ -429,7 +430,7 @@ let find_some_sols
if not is_bool_sat then (
[],bdd
) else (
let sols = Solver.solve_formula
let snt, sols = Solver.solve_formula snt
Value.OfIdent.empty (* input: Var.env_in *)
Value.OfIdent.empty (* memory: Var.env *)
(* !solver_vl (* vl: int *) *)
......@@ -2477,9 +2478,7 @@ let (step: t -> control_state -> data_state -> control_state * data_state) =
(* clean tabulated results to avoid memory leaks.
Cleanning at every step may be overkill though...
*)
Formula_to_bdd.clear_step ();
!Solver.clear_snt ();
MainArg.event_incr prog.arg_opt; (* call *)
in
let bg = get_behavior_gen prog data.ins data.mems ctrl in
......@@ -2520,8 +2519,7 @@ let (step_ldbg: ctx -> string -> t -> control_state -> data_state ->
(* clean tabulated results to avoid memory leaks.
Cleanning at every step may be overkill though...
*)
Formula_to_bdd.clear_step ();
!Solver.clear_snt ();
Formula_to_bdd.clear_all ();
in
let datal =
(List.map (fun (n,v) -> n, Value.to_data_val v) (Value.OfIdent.content data.ins)) @
......
......@@ -698,6 +698,7 @@ let get_init_state ?(verb_level=0) zelutprog zeprog = (
List.fold_left get_init_vals Value.OfIdent.empty (zeprog.Prog.out_vars);
Prog.last_local =
List.fold_left get_init_vals Value.OfIdent.empty (zeprog.Prog.loc_vars);
Prog.snt = Solver.init();
Prog.verbose = verb_level
}
}
......
......@@ -118,7 +118,7 @@ let dump_prog p = (
let gnuplot_pid_ref = ref None
let gnuplot_oc = ref None
(* simu *)
(* simu : old lutin main *)
let rec to_simu oc infile mnode opt = (
(* Parse and build the internal structure *)
let (zelutprog, zeprog) = LutProg.make ~libs:(MainArg.libs opt) infile mnode in
......@@ -138,10 +138,6 @@ let rec to_simu oc infile mnode opt = (
let noo = not (MainArg.only_outputs opt) in
Random.init seed;
if MainArg.compute_volume opt then Solver.set_fair_mode ()
else Solver.set_efficient_mode ();
!Solver.init_snt ();
Rif.write oc msg;
Rif.write_interface oc init_state.Prog.s.Prog.in_vars
init_state.Prog.s.Prog.out_vars loc None;
......@@ -230,7 +226,6 @@ and main_loop_core oc opt t init_state init_pre_lut_output state pre_lut_output
(* Clean-up cached info that depend on pre or inputs *)
Formula_to_bdd.clear_step ();
!Solver.clear_snt ();
match MainArg.max_steps opt with
| None -> main_loop oc opt (t+1) init_state init_pre_lut_output
......@@ -272,7 +267,6 @@ let to_exe oc infile mnode opt = (
(* Clean-up cached info that depend on pre or inputs *)
Formula_to_bdd.clear_step ();
!Solver.clear_snt ();
Verbose.put "#Main.to_exe: step %d\n" cpt;
let bg = LutExe.get_behavior_gen exe ins pres ctrl in
......
......@@ -40,7 +40,8 @@
*)
open Sol_nb
val draw_in_bdd : Var.env_in -> Var.env -> int -> string ->
Exp.var list -> Bdd.t -> Bdd.t -> Var.env * Store.t' * Store.p
(** [draw_in_bdd inputs memory verbose_level msg vars bdd comb]
......
......@@ -38,6 +38,7 @@ type dynamic_state_fields = {
last_input : Var.env;
last_output : Var.env;
last_local : Var.env;
snt: Solver.t;
verbose : int
}
......
......@@ -60,6 +60,7 @@ and dynamic_state_fields = {
last_input : Var.env;
last_output : Var.env;
last_local : Var.env;
snt: Solver.t;
verbose : int
}
and state = {
......
......@@ -9,6 +9,7 @@
*)
type sol_nb = (float * int)
(** This type is used to represent the number of solutions of a
......
This diff is collapsed.
......@@ -27,10 +27,11 @@
*)
val is_satisfiable :
Var.env_in -> Var.env -> int -> string -> Exp.formula -> string -> bool
(* The solver monad *)
type t
val init : unit -> t
val is_satisfiable : t ->
Var.env_in -> Var.env -> int -> string -> Exp.formula -> string -> t * bool
(** [is_satisfiable input memory verbose_level msg f] suceeds iff the
formula [f], once evaluated w.r.t. [input] and memories, is
satisfiable from the Boolean point of vue. At this level, each
......@@ -40,13 +41,13 @@ val is_satisfiable :
because it is very expensive.
*)
val is_satisfiable_bdd :
Var.env_in -> Var.env -> int -> string -> Exp.formula -> string -> bool * Bdd.t
val is_satisfiable_bdd : t ->
Var.env_in -> Var.env -> int -> string -> Exp.formula -> string -> t * bool * Bdd.t
(* idem, but returns the corresponding bdd *)
val solve_formula : Var.env_in -> Var.env -> int -> string ->
val solve_formula : t -> Var.env_in -> Var.env -> int -> string ->
Var.name list list -> Thickness.formula_draw_nb -> Thickness.numeric ->
Exp.formula -> Exp.var list -> Exp.formula -> (Var.env * Var.env) list
Exp.formula -> Exp.var list -> Exp.formula -> t * (Var.env * Var.env) list
(** [solve_formula input memory verbose_level msg output_var_names
fdn tn bools nums f] randomly assigns [tn] values to variables
in [bools] and [nums] (which ought to contains all output and
......@@ -70,12 +71,6 @@ val solve_formula : Var.env_in -> Var.env -> int -> string ->
ZZZ : solve_formula should have been called once to be able to use
this function with this flag set to [true], as it uses the solution
number table. *)
val print_bdd_with_dot: Bdd.t -> string -> bool -> unit
val print_bdd_with_dot: t -> Bdd.t -> string -> bool -> unit
val init_snt : (unit -> unit) ref
val clear_snt : (unit -> unit) ref
(** XXX *)
val set_efficient_mode : unit -> unit
val set_fair_mode : unit -> unit
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