Commit 9f11061a authored by Erwan Jahier's avatar Erwan Jahier

lurette 0.95 Mon, 30 Sep 2002 09:32:45 +0200 by jahier

Parent-Version:      0.94
Version-Log:

Continue to prepare things for the next change (which will try to
handle equalities smartly).

test/test*.res:
   fix the expected results as this change adds a random toss
   that disturbs the random values.

source/solver.ml:
source/rnumsolver.ml:
   Add code to handle the fact that the negation of a equality
   is the disjunction of two inegalities, which can not be added
   to store as it is. So we first try with >, and if it fails,
   we try with < (or the other way aroung, depending on a fair toss).

   Also split up the code in Solver.draw_in_bdd depending on the
   fact that the current constraint is a boolean, an eq, or an ineg.

source/solver.ml:
   split toss_up_one_var into toss_up_one_var and toss_up_one_var_index,
   one performing the the toss from a var, the other one from a var index.

Project-Description: Lurette
parent f8219704
......@@ -8,15 +8,15 @@
(bin/Makefile.ima_exe 2013 1027066799 b/41_Makefile.i 1.3)
(test/giro/onlyroll.lus 18298 1031732392 c/7_onlyroll.l 1.1)
(source/util.ml 15446 1032510467 35_util.ml 1.26)
(test/time.exp 5580 1033125605 b/48_time.exp 1.5)
(source/solver.ml 25138 1033125605 39_solver.ml 1.28)
(test/time.exp 5580 1033371165 b/48_time.exp 1.6)
(source/solver.ml 28777 1033371165 39_solver.ml 1.29)
(test/test_gen_stubs.h 1818 1020068208 b/45_test_gen_s 1.1)
(source/command_line.ml 4625 1031053030 b/20_command_li 1.8)
(source/lurette.ml 13388 1032510467 12_lurette.ml 1.52)
(myrules 10516 1033125605 c/14_myrules 1.5)
(source/solver.mli 1003 1027092697 38_solver.mli 1.13)
(source/env.mli 2028 1027349504 15_env.mli 1.15)
(test/heater_float.rif.exp 1459 1032362091 b/30_heater_flo 1.7)
(test/heater_float.rif.exp 1468 1033371165 b/30_heater_flo 1.8)
(lurette.depfull.dot 49 1007651448 b/5_lurette.de 1.2)
(source/env.ml 8013 1027349504 16_env.ml 1.29)
(make_lurette 1303 1032940601 27_make_luret 1.16)
......@@ -26,7 +26,7 @@
(test/porte.ima 1050 1032789516 b/16_porte.env 1.8)
(doc/archi.fig 3693 1003928781 20_archi.fig 1.1)
(source/constraint.ml 2387 1033125605 c/19_constraint 1.1)
(source/rnumsolver.ml 17099 1033125605 b/27_rnumsolver 1.8)
(source/rnumsolver.ml 16394 1033371165 b/27_rnumsolver 1.9)
(ID_EN_VRAC 2184 1002196285 0_ID_EN_VRAC 1.1)
(source/parse_env.mli 1025 1027066799 40_parse_env. 1.9)
(source/sim2chro.mli 1455 1027943375 b/23_sim2chro.m 1.5)
......@@ -46,11 +46,11 @@
(demo/chaudiere/chaudiere.ima 446 1032789516 c/11_chaudiere. 1.5)
(demo/chaudiere/buggy_chaudiere_ctrl.lus 219 1031732392 c/10_buggy_chau 1.1)
(demo/chaudiere/chaudiere_oracle.lus 107 1031732392 c/8_chaudiere_ 1.1)
(test/time.res 5580 1033125605 b/49_time.res 1.8)
(test/time.res 5580 1033371165 b/49_time.res 1.9)
(TAGS 9825 1007379917 21_TAGS 1.6)
(source/command_line.mli 1442 1031053030 b/21_command_li 1.7)
(source/env_state.mli 6734 1033125605 50_env_state. 1.24)
(source/rnumsolver.mli 1996 1033125605 b/26_rnumsolver 1.5)
(source/rnumsolver.mli 2246 1033371165 b/26_rnumsolver 1.6)
(source/ima_exe.mli 447 1016127950 b/31_ima_exe.ml 1.1)
(source/eval.mli 1395 1027066799 48_eval.mli 1.10)
(test/giro/giro.ima 2828 1032789516 c/6_giro.ima 1.2)
......@@ -86,7 +86,7 @@
(ihm/xlurette/xlurette.glade 43485 1032531447 c/13_xlurette.g 1.4)
(test/heater_int.lus 170 1020068208 b/43_heater_int 1.1)
(source/graph.mli 2218 1027066799 13_graph.mli 1.9)
(test/heater_int.rif.exp 860 1028297733 b/28_heater_int 1.6)
(test/heater_int.rif.exp 850 1033371165 b/28_heater_int 1.7)
(source/formula.ml 5786 1033125605 45_formula.ml 1.20)
(source/lurette.mli 448 1016027474 11_lurette.ml 1.12)
(source/constraint.mli 1619 1033125605 c/18_constraint 1.1)
......
;; -*- Prcs -*-
(Created-By-Prcs-Version 1 3 3)
(Project-Description "Lurette")
(Project-Version lurette 0 94)
(Parent-Version lurette 0 93)
(Project-Version lurette 0 95)
(Parent-Version lurette 0 94)
(Version-Log "
Continue to prepare things for the next change (which will try to
handle equalities smartly).
Prepare things for the next change (which will try to handle equalities
smartly).
test/test*.res:
fix the expected results as this change adds a random toss
that disturbs the random values.
source/solver.ml:
source/rnumsolver.ml:
atomic_formula do not need both < and > (ditto for <= and >=).
Indeed, I just need to take the opposite, and everything is fine.
One advantage is that there are less cases to handle. But the key
advantage is that it make the representation of constraint normal,
which is important at least when I will try to detect equalities.
Also add a subst list and constraint list fields to the store
that will ebe used in the forthcoming change. They will resp.
be used for removeing a dimension when an equality is encountered
and to delay constraint with more than one variable.
source/constraint.ml,mli: (new files)
Move there from formula.ml everything that is related to the internal
representation of constraints.
Also change the name of atomic_formula to linear_constraint, which is
more informative.
Add code to handle the fact that the negation of a equality
is the disjunction of two inegalities, which can not be added
to store as it is. So we first try with >, and if it fails,
we try with < (or the other way aroung, depending on a fair toss).
Also split up the code in Solver.draw_in_bdd depending on the
fact that the current constraint is a boolean, an eq, or an ineg.
source/solver.ml:
split toss_up_one_var into toss_up_one_var and toss_up_one_var_index,
one performing the the toss from a var, the other one from a var index.
")
(New-Version-Log ""
)
(Checkin-Time "Fri, 27 Sep 2002 13:20:05 +0200")
(Checkin-Time "Mon, 30 Sep 2002 09:32:45 +0200")
(Checkin-Login jahier)
(Populate-Ignore ())
(Project-Keywords)
......@@ -68,10 +63,10 @@ source/constraint.ml,mli: (new files)
(source/util.ml (lurette/35_util.ml 1.26 644))
(source/solver.mli (lurette/38_solver.mli 1.13 644))
(source/solver.ml (lurette/39_solver.ml 1.28 644))
(source/solver.ml (lurette/39_solver.ml 1.29 644))
(source/rnumsolver.mli (lurette/b/26_rnumsolver 1.5 644))
(source/rnumsolver.ml (lurette/b/27_rnumsolver 1.8 644))
(source/rnumsolver.mli (lurette/b/26_rnumsolver 1.6 644))
(source/rnumsolver.ml (lurette/b/27_rnumsolver 1.9 644))
(source/parse_env.mli (lurette/40_parse_env. 1.9 644))
(source/parse_env.ml (lurette/41_parse_env. 1.28 644))
......@@ -137,8 +132,8 @@ source/constraint.ml,mli: (new files)
(lurette.depfull.dot (lurette/b/5_lurette.de 1.2 644))
(TAGS (lurette/21_TAGS 1.6 644))
(test/time.exp (lurette/b/48_time.exp 1.5 644))
(test/time.res (lurette/b/49_time.res 1.8 644))
(test/time.exp (lurette/b/48_time.exp 1.6 644))
(test/time.res (lurette/b/49_time.res 1.9 644))
;; Various files used for testing purposes
(test/usager.ima (lurette/b/14_usager.env 1.9 644))
......@@ -156,9 +151,9 @@ source/constraint.ml,mli: (new files)
(test/vrai_tram.c (lurette/b/8_vrai_tram. 1.3 644))
(test/tram_simple.h (lurette/b/25_tram_simpl 1.1 644))
(test/heater_int.rif.exp (lurette/b/28_heater_int 1.6 644))
(test/heater_int.rif.exp (lurette/b/28_heater_int 1.7 644))
(test/ControleurPorte.rif.exp (lurette/b/29_Controleur 1.9 644))
(test/heater_float.rif.exp (lurette/b/30_heater_flo 1.7 644))
(test/heater_float.rif.exp (lurette/b/30_heater_flo 1.8 644))
(test/heater_int.lus (lurette/b/43_heater_int 1.1 644))
(test/heater_float.lus (lurette/b/44_heater_flo 1.1 644))
(test/test_gen_stubs.h (lurette/b/45_test_gen_s 1.1 644))
......
......@@ -22,20 +22,10 @@ type range =
| ValI of int (* whenever min = max *)
| ValF of float (* Ditto for floats *)
let (range_to_string : range -> string) =
fun range ->
match range with
RangeI(min, max) ->
("[" ^ (string_of_int min) ^ ", " ^ (string_of_int max) ^ "] ")
| RangeF(min, max) ->
("[" ^ (string_of_float min) ^ ", " ^ (string_of_float max) ^ "] ")
| ValI(v) ->
("[" ^ (string_of_int v) ^ ", " ^ (string_of_int v) ^ "] ")
| ValF(v) ->
("[" ^ (string_of_float v) ^ ", " ^ (string_of_float v) ^ "] ")
(* For substituing a variable by an expression. This is to deal with
(**
For substituing a variable by an expression. This is to deal with
equalities: when an equality is encountered, we can remove one
dimension by putting the equality into a substitution. Then we
apply it to all the other relations. Its value is then obtained
......@@ -51,7 +41,9 @@ let (range_to_string : range -> string) =
type subst = (num_value * string) * n_expr
type substl = subst list
(* When the dimension of an atomic formula is greater than 1, we
(**
When the dimension of an atomic formula is greater than 1, we
delay its addition to the store until an equality makes it a
constraint of dimension 1 (i.e., it contains only 1 var). At bdd
leaves, if this list is not empty, it means that the current
......@@ -63,22 +55,11 @@ type delay = Constraint.t list
type store = {
var : ((Formula.var_name, range) Hashtbl.t) option ;
(* set to None when it becomes unsatisfiable *)
substl : substl;
delay : delay
}
let (store_to_string : store -> string) =
fun s ->
match s.var with
None -> "Empty store"
| Some(tbl) ->
(Hashtbl.fold
(fun vn range acc ->
(vn ^ " in " ^ (range_to_string range) ^ " ; " ^ acc)
)
tbl
"\n"
)
(* exported *)
let (new_store : Formula.vnt list -> store) =
......@@ -132,11 +113,11 @@ let (div : int -> int -> int) =
let (normalise : Constraint.t -> (var_name * nac)
(* option *)
) =
fun af ->
fun cstr ->
(* Transform atomic formula into a data type that is easier to
process from a range solver point of vue.
process.
Returns None if [af] contains more than one variable (in which
Returns None if [cstr] contains more than one variable (in which
case the constraint will be delayed).
*)
let (get_vn_and_constant : n_expr -> (
......@@ -171,47 +152,10 @@ let (normalise : Constraint.t -> (var_name * nac)
failwith ("*** Can only solve numeric constraints " ^
"over intervals, sorry.\n")
in
match af with
match cstr with
EqZ(ne) ->
failwith "XXX finish me !!!"
(* match get_vn_and_constant ne with *)
(* None -> None *)
(* | Some(I(i_cst), I(_), "") -> *)
(* if i_cst = O *)
(* then *)
(* else raise No_numeric_solution *)
(* | Some(F(_), F(f_cst), "") -> *)
(* *)
(* | Some(I(i_cst), I(i_cst), vn) -> *)
(* *)
(* | Some(F(f_cst), F(f_cst), vn) -> *)
(* *)
(* | Some(F(_), I(_), vn) -> assert false *)
(* | Some(I(_), F(_), vn) -> assert false *)
(*
let (b, a, x) = get_x_and_constant ne in
( match (b, a) with
(I(i_b), I(i_a)) ->
let i = div (- i_b) i_a in
if i_a > 0
then
if (i_b mod i_a) = 0
then (x, NSupEqI(i+1))
else (x, NSupEqI(i))
else
if (i_b mod i_a) = 0
then (x, NInfEqI(i-1))
else (x, NInfEqI(i-1))
| (F(f_b), F(f_a)) ->
if f_a > 0.
then (x, NSupF(-.f_b /. f_a))
else (x, NSupF( .f_b /. f_a))
| (I(_), F(_)) -> assert false
| (F(_), I(_)) -> assert false
)
*)
assert false
| GZ(ne) ->
let (cst, coeff, vn) = get_vn_and_constant ne in
( match (cst, coeff) with
......@@ -268,14 +212,19 @@ let (make_subst : vn -> num_value -> subst) =
((I(1), vn), (NeMap.add "" value NeMap.empty))
(* exported *)
let (split_store_eq : store -> Constraint.t -> store * store * store) =
fun store cstr ->
failwith "XXX write me !!!"
(* exported *)
let (split_store : store -> Constraint.t -> store * store) =
fun store af ->
fun store cstr ->
let (sl, d) = (store.substl, store.delay) in
match store.var with
None -> assert false
| Some(tbl) ->
let (vn, nac) = normalise af in
let (vn, nac) = normalise cstr in
( match (nac, (Hashtbl.find tbl vn)) with
(NSupEqI(i), RangeI(min, max)) ->
if i <= min
......@@ -623,12 +572,10 @@ let (split_store : store -> Constraint.t -> store * store) =
)
(* exported *)
let (is_empty : store -> bool) =
let (is_store_satisfiable : store -> bool) =
fun store ->
store.var = None
store.var <> None
(* exported *)
......@@ -701,5 +648,35 @@ let (draw_edges : store -> Formula.subst list) =
(* exported *)
(* let (get_center_of_gravity : store -> Formula.subst list) =
fun -> *)
(****************************************************************************)
(* Pretty printing *)
(* exported *)
let (range_to_string : range -> string) =
fun range ->
match range with
RangeI(min, max) ->
("[" ^ (string_of_int min) ^ ", " ^ (string_of_int max) ^ "] ")
| RangeF(min, max) ->
("[" ^ (string_of_float min) ^ ", " ^ (string_of_float max) ^ "] ")
| ValI(v) ->
("[" ^ (string_of_int v) ^ ", " ^ (string_of_int v) ^ "] ")
| ValF(v) ->
("[" ^ (string_of_float v) ^ ", " ^ (string_of_float v) ^ "] ")
(* exported *)
let (store_to_string : store -> string) =
fun s ->
match s.var with
None -> "Empty store"
| Some(tbl) ->
(Hashtbl.fold
(fun vn range acc ->
(vn ^ " in " ^ (range_to_string range) ^ " ; " ^ acc)
)
tbl
"\n"
)
......@@ -20,12 +20,24 @@ val new_store : Formula.vnt list -> store
val split_store : store -> Constraint.t -> store * store
(** [split s c] returns the store [s] with the numeric constraint
[c] (resp [not c]) added in the lhs of the pair (resp rhs). *)
(** If [c] is not an equality constraint, [split_store s c] returns
the store [s] with the numeric constraint [c] (resp [not c])
added in the lhs of the pair (resp rhs).
val is_empty : store -> bool
(** Returns true iff one of the variable of the store has an empty
domain. *)
Fails if [c] is an equality constraint (for which [split_store_eq]
in made). *)
val split_store_eq : store -> Constraint.t -> store * store * store
(** If [c] = EqZ(e) is an equality constraint, [split_store_eq s c]
returns the store [s] with the numeric constraint [c], [GZ(e)],
and [GZ(-e)] in first, second and third position respectively.
Fails if [c] is not an equality constraint (for which [split_store]
in made). *)
val is_store_satisfiable : store -> bool
(** Returns false iff the constraint added to the store leaded to an
inconsistency. *)
val draw_inside : store -> Formula.subst list
......@@ -51,12 +63,4 @@ val draw_verteces : store -> Formula.subst list
(** Pretty printing *)
val store_to_string : store -> string
(** [draw bool_vars_to_gen num_vnt_to_gen comb bdd] draws in [bdd]
the output and local vars to be generated by the environnent. *)
(* val draw : vn list -> vnt list -> Bdd.t -> Bdd.t -> subst list * subst list *)
(* exported *)
(* exception No_numeric_solution *)
val store_to_string : store -> string
(*-----------------------------------------------------------------------
** Copyright (C) 2001, 2002 - Verimag.
** Copyright (C) 2001, 2002 - Verimag.
** This file may only be copied under the terms of the GNU Library General
** Public License
**-----------------------------------------------------------------------
......@@ -549,10 +549,19 @@ and
(****************************************************************************)
(****************************************************************************)
(* exported *)
(* Raised during the toss if no solution is found in the branch *)
exception No_numeric_solution
let (toss_up_one_var: var -> subst option) =
let (toss_up_one_var: var_name -> subst) =
fun var ->
(* *)
let ran = Random.float 1. in
if (ran < 0.5)
then (var, B(true))
else (var, B(false))
let (toss_up_one_var_index: var -> subst option) =
fun var ->
(* if [var] is a index that corresponds to a boolean variable,
this fonction performs a toss and returns a substitution for
......@@ -563,19 +572,16 @@ let (toss_up_one_var: var -> subst option) =
appear along a path, we simply ignore it and hence it will not
be added to the store.
*)
let af = Env_state.index_to_linear_constraint var in
match af with
Bv(vn) ->
let ran = Random.float 1. in
if (ran < 0.5)
then Some(vn, B(true))
else Some(vn, B(false))
let cstr = Env_state.index_to_linear_constraint var in
match cstr with
Bv(vn) -> Some(toss_up_one_var vn)
| _ -> None
let (is_a_numeric_constraint : Constraint.t -> bool) =
fun af ->
match af with
fun cstr ->
match cstr with
Bv(_) -> false
| GZ(_) -> true
| GeqZ(_) -> true
......@@ -601,116 +607,242 @@ let rec (draw_in_bdd: subst list * store -> Bdd.t -> Bdd.t ->
then
(* Toss the remaining bool vars. *)
( (List.append sl
(Util.list_map_option toss_up_one_var (Bdd.list_of_support comb))),
(Util.list_map_option toss_up_one_var_index (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 topvar_comb = Bdd.topvar comb in
let af = (Env_state.index_to_linear_constraint bddvar) in
let top_var_is_numeric = is_a_numeric_constraint af in
if
bddvar <> topvar_comb
&& not top_var_is_numeric
let cstr = (Env_state.index_to_linear_constraint bddvar) in
match cstr with
Bv(var) -> draw_in_bdd_bool var (sl, store) bdd comb
| EqZ(e) -> draw_in_bdd_eq cstr (sl, store) bdd comb
| _ -> draw_in_bdd_ineq cstr (sl, store) bdd comb
and (draw_in_bdd_bool: string -> subst list * store -> Bdd.t -> Bdd.t ->
subst list * store) =
fun var (sl, store) bdd comb ->
let bddvar = Bdd.topvar bdd in
let topvar_comb = Bdd.topvar comb in
if
bddvar <> topvar_comb
then
(* that condition means that topvar_comb is an unconstraint
boolean var; hence we toss it up. *)
let new_sl = (toss_up_one_var var)::sl in
draw_in_bdd (new_sl, store) bdd (Bdd.dthen comb)
else
(* bddvar = combvar *)
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 (
bdd1, bool1, sol_nb1,
bdd2, bool2, sol_nb2
) =
let ran = Random.float 1.
and sol_nb_ratio =
((float_of_sol_nb n) /. (float_of_sol_nb (add_sol_nb n m)))
in
if
ran < sol_nb_ratio
(*
Depending on the result of a toss (based on the number
of solution in each branch), we try the [then] or the
[else] branch first.
*)
then
((Bdd.dthen bdd), true, n,
(Bdd.delse bdd), false, m )
else
((Bdd.delse bdd), false, m,
(Bdd.dthen bdd), true, n )
in
let (sl1, sl2, new_comb) = (
((var, B(bool1))::sl),
((var, B(bool2))::sl),
(if Bdd.is_true comb then comb else Bdd.dthen comb)
)
in
(*
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].
*)
try
draw_in_bdd (sl1, store) bdd1 new_comb
with No_numeric_solution ->
if not (eq_sol_nb sol_nb2 zero_sol)
then draw_in_bdd (sl2, store) bdd2 new_comb
(*
The second branch is now tried because no path in
the first bdd leaded to a satisfiable set of
numeric constraints.
*)
else raise No_numeric_solution
and (draw_in_bdd_eq: Constraint.t -> subst list * store -> Bdd.t -> Bdd.t ->
subst list * store) =
fun cstr (sl, store) bdd comb ->
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_cstr, store_plus_not_cstr, store_plus_not_cstr2) =
split_store_eq store cstr
in
let (
store1, bdd1, sol_nb1,
store2, bdd2, sol_nb2,
store3, bdd3, sol_nb3
) =
let ran0 = Random.float 1.
and ran = Random.float 1.
and sol_nb_ratio =
((float_of_sol_nb n) /. (float_of_sol_nb (add_sol_nb n m)))
in
if
ran0 < 0.5
(*
When taking the negation of an equality, we can
either try > or <. Here, We toss which one we
will try first.
*)
then
(* that condition means that topvar_comb is an unconstraint
boolean var; hence we toss it up. *)
let new_sl =
match toss_up_one_var topvar_comb with
Some(s) -> s::sl
| None -> sl (* unconstraint num var will be drawn later (in draw) *)
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 it avoid code dup... *)
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
(* match af with *)
(* EqZ(ne) -> *)
(* *)
(* | _ -> *)
(* if *)
(* (dimension af) = 1 *)
(* then *)
(* let (st1, st2) = *)
split_store store af
(* in *)
(* *)
(* *)
(* else *)
(* () *)
else
(store, store)
in
let (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 [then] or the
[else] branch first. *)
let ran = Random.float 1. in
if ran < ((float_of_sol_nb n) /. (float_of_sol_nb (add_sol_nb n m)))
then
(store_plus_af, (Bdd.dthen bdd), true, n,
store_plus_not_af, (Bdd.delse bdd), false, m)
else
(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, B(bool1))::sl),
((vn, 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 = draw_in_bdd (sl1, store1) bdd1 new_comb in
Some(tail_draw1)