Commit fcdb446e authored by Erwan Jahier's avatar Erwan Jahier
Browse files

lurette 1.5 Wed, 24 Sep 2003 16:54:55 +0200 by jahier

Parent-Version:      1.4
Version-Log:

Split up solver.ml into 3: solver.ml, formula_to_bdd.ml, and bddd.ml.

Project-Description: Lurette
parent 5bf375a5
......@@ -21,7 +21,7 @@
(share/pixmaps/open.xpm 782 1055926783 f/17_open.xpm 1.1)
(source/parse_luc.mli 2297 1063029729 40_parse_env. 1.16)
(polka/C/internal.c 699 1047029868 e/8_internal.c 1.1)
(source/solver.ml 35241 1064411282 39_solver.ml 1.53)
(source/solver.ml 7747 1064415295 39_solver.ml 1.54)
(ihm/xlurette/makefile 1853 1063786164 c/16_makefile 1.17)
(share/gen_fake_lucky.sh.in 115 1063786164 g/31_gen_fake_l 1.1)
(polka/C/internal.h 958 1047029868 e/0_internal.h 1.1)
......@@ -30,6 +30,7 @@
(test/sparc-scade/libpwlinear.saofdm 1379 1055487917 e/43_libpwlinea 1.1)
(test/cygwin-scade/ConfAnnot.aty 13661 1055926783 g/4_ConfAnnot. 1.1)
(test/ControleurPorte.c 9407 1012914629 b/19_Controleur 1.1)
(source/bddd.mli 592 1064415295 g/37_bddd.mli 1.1)
(share/lucky_init.sh.in 1061 1063786164 e/24_lucky_init 1.11)
(test/heater.lus 176 1063786164 g/33_heater.lus 1.1)
(test/ControleurPorte.h 2306 1012914629 b/18_Controleur 1.1)
......@@ -40,13 +41,13 @@
(test/cygwin-scade/Pilot_cst.saofd 788 1055926783 f/38_Pilot_cst. 1.1)
(test/cygwin-scade/lib_pilot.etp 1173 1055926783 f/48_lib_pilot. 1.1)
(source/command_line.mli 1580 1064329011 b/21_command_li 1.12)
(source/Makefile.lucky 2917 1063786164 b/41_Makefile.i 1.23)
(source/Makefile.lucky 3115 1064415295 b/41_Makefile.i 1.24)
(polka/README 1437 1047029868 e/19_README 1.1)
(polka/Makefile.depend 136 1047029868 d/30_Makefile.d 1.1)
(test/test9.rif.exp 2322 1064411282 g/17_test9.rif. 1.2)
(README 2803 1056374363 10_README 1.10)
(source/pnumsolver.ml 9273 1045489850 d/23_pnumsolver 1.2)
(source/gen_stubs_scade.ml 9106 1055926783 f/5_gen_stubs_ 1.1)
(test/test9.rif.exp 2322 1064411282 g/17_test9.rif. 1.2)
(cuddaux/cuddauxMisc.c 13842 1034006019 c/27_cuddauxMis 1.1)
(source/polyhedron.ml 7871 1064411282 d/25_polyhedron 1.8)
(source/Makefile.gen_fake_lucky 528 1063786164 g/9_Makefile.g 1.2)
......@@ -56,7 +57,7 @@
(polka/C/cherni.c 28811 1047029868 e/9_cherni.c 1.1)
(source/command_line_luc_exe.mli 1276 1064329011 b/34_command_li 1.11)
(polka/C/poly.h 4314 1047029868 d/49_poly.h 1.1)
(source/formula.mli 4392 1063029729 44_formula.ml 1.25)
(source/formula.mli 4394 1064415295 44_formula.ml 1.26)
(polka/C/cherni.h 2217 1047029868 e/1_cherni.h 1.1)
(share/pixmaps/chrono.xpm 703 1055926783 f/23_chrono.xpm 1.1)
(polka/caml/polka_caml.c 6499 1047029868 d/37_polka_caml 1.1)
......@@ -72,7 +73,7 @@
(mlcuddidl/idd.ml 7061 1034006019 d/0_idd.ml 1.1)
(test/cygwin-scade/C_SQRT.saofd 214 1055926783 g/1_C_SQRT.sao 1.1)
(test/giro/onlyroll.lus 18298 1031732392 c/7_onlyroll.l 1.1)
(source/eval.ml 7245 1063029729 49_eval.ml 1.15)
(source/eval.ml 7275 1064415295 49_eval.ml 1.16)
(polka/Changes 1502 1047029868 e/22_Changes 1.1)
(source/env.mli 1937 1064329011 15_env.mli 1.19)
(test/sparc-scade/libdigital.saofdm 1256 1055487917 e/47_libdigital 1.1)
......@@ -91,13 +92,13 @@
(test/cygwin-scade/lib_pilot.err 119 1055926783 f/49_lib_pilot. 1.1)
(test/losange.luc 410 1046768487 d/27_losange.lu 1.2)
(test/gyro.rif.exp 10954 1064411282 e/36_gyro.rif.e 1.4)
(test/time-ecrins.exp 8431 1064411282 d/21_time-ecrin 1.26)
(test/time-ecrins.exp 8429 1064415295 d/21_time-ecrin 1.27)
(source/value.ml 2539 1063786164 c/23_value.ml 1.6)
(source/gne.ml 3467 1063029729 b/37_gne.ml 1.6)
(test/cygwin-scade/Pilot.vsp 2075 1055926783 f/40_Pilot.vsp 1.1)
(source/parse_c_scade.ml 5984 1055926783 e/41_parse_c_sc 1.2)
(share/lurettetop.sh.in 111 1063786164 g/25_lurettetop 1.1)
(source/formula.ml 10702 1063029729 45_formula.ml 1.31)
(source/formula.ml 10862 1064415295 45_formula.ml 1.32)
(test/cygwin-scade/position_validation.saofd 10188 1055926783 f/36_position_v 1.1)
(test/sparc-scade/exo1.saofdm 320 1055487917 e/50_exo1.saofd 1.1)
(share/pixmaps/plus.xpm 473 1055926783 f/15_plus.xpm 1.1)
......@@ -127,7 +128,7 @@
(source/call_lurette_main.c 322 1050421093 e/28_call_luret 1.1)
(polka/C/vector.c 13780 1047029868 e/3_vector.c 1.1)
(test/sparc-scade/Direction_D1.saofd 1335 1055487917 e/51_Direction_ 1.1)
(source/Makefile.lurette_lib 2620 1063029729 c/2_Makefile.l 1.21)
(source/Makefile.lurette_lib 2810 1064415295 c/2_Makefile.l 1.22)
(polka/caml/polka_parser.mly 1729 1047029868 d/40_polka_pars 1.1)
(mlcuddidl/bdd.idl 18233 1034006019 d/7_bdd.idl 1.1)
(test/heater_int.lus 170 1020068208 b/43_heater_int 1.1)
......@@ -148,7 +149,7 @@
(mlcuddidl/manager.ml 8017 1034006019 c/47_manager.ml 1.1)
(share/plot 11394 1063786164 e/35_plot 1.4)
(share/pixmaps/save.xpm 867 1055926783 f/12_save.xpm 1.1)
(source/solver.mli 1545 1064329011 38_solver.mli 1.16)
(source/solver.mli 1330 1064415295 38_solver.mli 1.17)
(test/passerelle.luc 963 1063786164 b/17_passerelle 1.12)
(source/store.ml 33533 1064411282 b/27_rnumsolver 1.27)
(mlcuddidl/mtbdd.mli 4395 1034006019 c/43_mtbdd.mli 1.1)
......@@ -164,7 +165,7 @@
(source/graph.mli 2382 1063029729 13_graph.mli 1.11)
(source/store.mli 3122 1064411282 b/26_rnumsolver 1.19)
(test/time-ossau.res 8420 1064411282 b/49_time.res 1.53)
(source/automata.ml 20675 1064329011 b/47_automata.m 1.12)
(source/automata.ml 20683 1064415295 b/47_automata.m 1.13)
(test/sparc-scade/libmath.saofdm 1378 1055487917 e/45_libmath.sa 1.1)
(Makefile 68 1051024737 d/13_Makefile 1.4)
(share/Makefile.test.in 2712 1064329011 c/25_user-rules 1.10)
......@@ -175,7 +176,7 @@
(cuddaux/Makefile 3326 1053337243 c/35_Makefile 1.7)
(polka/C/bit.c 3026 1047029868 e/10_bit.c 1.1)
(source/draw.mli 467 1055926783 f/1_draw.mli 1.1)
(test/time-ossau.exp 8420 1064411282 b/48_time.exp 1.49)
(test/time-ossau.exp 8420 1064415295 b/48_time.exp 1.50)
(polka/caml/polkaIO.ml 1652 1047029868 d/44_polkaIO.ml 1.1)
(mlcuddidl/macros.m4 11290 1034006019 c/49_macros.m4 1.1)
(source/print.ml 5732 1063029729 47_print.ml 1.24)
......@@ -193,15 +194,17 @@
(source/lurettetop.ml 46392 1064329011 c/1_lurettetop 1.41)
(source/constraint.ml 2784 1063029729 c/19_constraint 1.8)
(test/structured_type.luc 2224 1063786164 g/32_structured 1.1)
(source/formula_to_bdd.ml 13269 1064415295 g/34_formula_to 1.1)
(test/cygwin-scade/counter.saofd 587 1055926783 g/2_counter.sa 1.1)
(test/test7.rif.exp 269 1063786164 g/12_test7.rif. 1.1)
(polka/caml/Makefile.depend 744 1063029729 d/32_Makefile.d 1.3)
(source/bddd.ml 14708 1064415295 g/36_bddd.ml 1.1)
(doc/archi.fig 3693 1003928781 20_archi.fig 1.1)
(ihm/xlurette/xlurette_glade_interface.ml 76914 1064411282 c/15_xlurette_g 1.21)
(test/Makefile 2729 1064411282 c/0_Makefile 1.14)
(INSTALL 101 1056616700 f/26_INSTALL 1.2)
(test/cygwin-scade/MyConsts.saofd 153 1055926783 f/44_MyConsts.s 1.1)
(test/losange-3d2.luc 361 1063786164 e/32_losange-3d 1.3)
(test/Makefile 2729 1064411282 c/0_Makefile 1.14)
(user-rules 28768 1064411282 c/14_myrules 1.44)
(test/infinite_weight.luc 889 1063786164 g/13_infinite_w 1.1)
(mlcuddidl/cudd_caml.c 22890 1034006019 d/3_cudd_caml. 1.1)
......@@ -262,7 +265,7 @@
(polka/C/polka.h 1478 1047029868 d/50_polka.h 1.1)
(share/pixmaps/ediff-quit.xpm 494 1055926783 f/20_ediff-quit 1.1)
(test/cygwin-scade/Pilot.saofd 3645 1055926783 f/42_Pilot.saof 1.1)
(test/time-moucherotte.exp 4851 1064411282 e/37_time-mouch 1.7)
(test/time-moucherotte.exp 4862 1064415295 e/37_time-mouch 1.8)
(source/command_line_luc_exe.ml 3526 1064329011 b/33_command_li 1.18)
(source/lurette_exe.c 220 1050421093 e/27_lurette_ex 1.2)
(source/env.ml 8206 1064329011 16_env.ml 1.32)
......@@ -295,6 +298,7 @@
(source/gen_fake_lutin.ml 4709 1055487917 d/16_gen_fake_l 1.5)
(test/heater_float.lus 177 1034351455 b/44_heater_flo 1.2)
(share/set_env_var.in 949 1063786164 g/23_set_env_va 1.1)
(source/formula_to_bdd.mli 1075 1064415295 g/35_formula_to 1.1)
(polka/Makefile 1636 1047029868 e/21_Makefile 1.1)
(test/dynamic_weight.luc 563 1063786164 g/14_dynamic_we 1.1)
(test/porte.luc 1014 1063786164 b/16_porte.env 1.12)
......
;; -*- Prcs -*-
(Created-By-Prcs-Version 1 3 3)
(Project-Description "Lurette")
(Project-Version lurette 1 4)
(Parent-Version lurette 1 3)
(Project-Version lurette 1 5)
(Parent-Version lurette 1 4)
(Version-Log "
source/store.ml:
source/solver.ml:
use map instead as hashtbl for the range base store.
It is much less error-prone (evil side effect!),
leads to clearer code (no need to copy the store, which was particularly
bad when done outside that module...), and is as efficient.
Split up solver.ml into 3: solver.ml, formula_to_bdd.ml, and bddd.ml.
")
(New-Version-Log ""
)
(Checkin-Time "Wed, 24 Sep 2003 15:48:02 +0200")
(Checkin-Time "Wed, 24 Sep 2003 16:54:55 +0200")
(Checkin-Login jahier)
(Populate-Ignore ())
(Project-Keywords)
......@@ -47,8 +45,14 @@ source/solver.ml:
(source/util.ml (lurette/35_util.ml 1.54 644))
(source/solver.mli (lurette/38_solver.mli 1.16 644))
(source/solver.ml (lurette/39_solver.ml 1.53 644))
(source/formula_to_bdd.ml (lurette/g/34_formula_to 1.1 644))
(source/formula_to_bdd.mli (lurette/g/35_formula_to 1.1 644))
(source/bddd.ml (lurette/g/36_bddd.ml 1.1 644))
(source/bddd.mli (lurette/g/37_bddd.mli 1.1 644))
(source/solver.mli (lurette/38_solver.mli 1.17 644))
(source/solver.ml (lurette/39_solver.ml 1.54 644))
(source/polyhedron.ml (lurette/d/25_polyhedron 1.8 644))
(source/polyhedron.mli (lurette/d/26_polyhedron 1.3 644))
......@@ -65,20 +69,20 @@ source/solver.ml:
(source/show_env.mli (lurette/42_show_env.m 1.10 644))
(source/show_env.ml (lurette/43_show_env.m 1.19 644))
(source/formula.mli (lurette/44_formula.ml 1.25 644))
(source/formula.ml (lurette/45_formula.ml 1.31 644))
(source/formula.mli (lurette/44_formula.ml 1.26 644))
(source/formula.ml (lurette/45_formula.ml 1.32 644))
(source/print.mli (lurette/46_print.mli 1.13 644))
(source/print.ml (lurette/47_print.ml 1.24 644))
(source/eval.mli (lurette/48_eval.mli 1.11 644))
(source/eval.ml (lurette/49_eval.ml 1.15 644))
(source/eval.ml (lurette/49_eval.ml 1.16 644))
(source/env_state.mli (lurette/50_env_state. 1.33 644))
(source/env_state.ml (lurette/51_env_state. 1.48 644))
(source/automata.mli (lurette/b/46_automata.m 1.5 644))
(source/automata.ml (lurette/b/47_automata.m 1.12 644))
(source/automata.ml (lurette/b/47_automata.m 1.13 644))
(source/sim2chro.mli (lurette/b/23_sim2chro.m 1.7 644))
(source/sim2chro.ml (lurette/b/24_sim2chro.m 1.20 644))
......@@ -159,9 +163,9 @@ source/solver.ml:
(source/Makefile.lurettetop (lurette/d/14_Makefile.l 1.5 644))
(source/Makefile.gen_fake_lutin (lurette/d/17_Makefile.g 1.4 644))
(source/Makefile.show_luc (lurette/b/40_Makefile.s 1.10 644))
(source/Makefile.lucky (lurette/b/41_Makefile.i 1.23 644))
(source/Makefile.lucky (lurette/b/41_Makefile.i 1.24 644))
(source/Makefile.gen_stubs (lurette/b/42_Makefile.g 1.8 644))
(source/Makefile.lurette_lib (lurette/c/2_Makefile.l 1.21 644))
(source/Makefile.lurette_lib (lurette/c/2_Makefile.l 1.22 644))
(source/Makefile (lurette/c/20_Makefile 1.24 644))
;; Documentation
......@@ -184,11 +188,11 @@ source/solver.ml:
(share/gnuplot-rif (lurette/e/34_gnuplot-ri 1.5 744))
(share/plot (lurette/e/35_plot 1.4 744))
(test/time-ossau.exp (lurette/b/48_time.exp 1.49 644))
(test/time-ossau.exp (lurette/b/48_time.exp 1.50 644))
(test/time-ossau.res (lurette/b/49_time.res 1.53 644))
(test/time-ecrins.res (lurette/d/20_time-ecrin 1.27 644))
(test/time-ecrins.exp (lurette/d/21_time-ecrin 1.26 644))
(test/time-moucherotte.exp (lurette/e/37_time-mouch 1.7 644))
(test/time-ecrins.exp (lurette/d/21_time-ecrin 1.27 644))
(test/time-moucherotte.exp (lurette/e/37_time-mouch 1.8 644))
(test/time-moucherotte.res (lurette/e/38_time-mouch 1.8 644))
;; Various files used for testing purposes
......@@ -434,6 +438,8 @@ source/solver.ml:
;; to version 1.1(w), by jahier:
(test/heater.lus (lurette/g/33_heater.lus 1.1 644))
)
(Merge-Parents)
(New-Merge-Parents)
......@@ -60,6 +60,10 @@ SOURCES_OCAML = \
$(LURETTE_PATH)/source/store.ml \
$(LURETTE_PATH)/source/env_state.mli \
$(LURETTE_PATH)/source/env_state.ml \
$(LURETTE_PATH)/source/formula_to_bdd.mli \
$(LURETTE_PATH)/source/formula_to_bdd.ml \
$(LURETTE_PATH)/source/bddd.mli \
$(LURETTE_PATH)/source/bddd.ml \
$(LURETTE_PATH)/source/solver.mli \
$(LURETTE_PATH)/source/solver.ml \
$(LURETTE_PATH)/source/show_env.mli \
......
......@@ -51,6 +51,10 @@ SOURCES = $(SOURCES_C) \
$(LURETTE_PATH)/source/draw.mli $(LURETTE_PATH)/source/draw.ml \
$(LURETTE_PATH)/source/store.mli $(LURETTE_PATH)/source/store.ml \
$(LURETTE_PATH)/source/env_state.mli $(LURETTE_PATH)/source/env_state.ml \
$(LURETTE_PATH)/source/formula_to_bdd.mli \
$(LURETTE_PATH)/source/formula_to_bdd.ml \
$(LURETTE_PATH)/source/bddd.mli \
$(LURETTE_PATH)/source/bddd.ml \
$(LURETTE_PATH)/source/solver.mli $(LURETTE_PATH)/source/solver.ml \
$(LURETTE_PATH)/source/show_env.mli $(LURETTE_PATH)/source/show_env.ml \
$(LURETTE_PATH)/source/automata.mli $(LURETTE_PATH)/source/automata.ml \
......
......@@ -126,7 +126,7 @@ let (compute_weight : weight -> env_in -> computed_weight) =
Wint(i) -> V i
| Infinity -> Infin
| Wexpr(e) ->
let gne = Solver.expr_to_gne e input in
let gne = Formula_to_bdd.expr_to_gne e input in
match Gne.get_constant gne with
None ->
print_string (
......
(*-----------------------------------------------------------------------
** Copyright (C) 2003 - Verimag.
** This file may only be copied under the terms of the GNU Library General
** Public License
**-----------------------------------------------------------------------
**
** File: bddd.ml
** Main author: jahier@imag.fr
*)
(** In the following, we call a comb the bdd of a conjunction of
litterals (var). They provide the ordering in which litterals
appear in the bdds we manipulate.
*)
open Util
open Formula
open Value
open Constraint
open Store
type var_idx = int
type sol_nb = Util.sol_nb
let rec (build_sol_nb_table: Bdd.t -> Bdd.t -> sol_nb * sol_nb) =
fun bdd comb ->
(** Returns the relative (to which bbd points to it) number of
solutions of [bdd] and the one of its negation. Also udpates
the solution number table for [bdd] and its negation, and
recursively for all its sub-bdds.
Note that this sol number make abstraction of the volume of
polyhedron which dimension is greater than 2. It is very bad as
far as the fairness of the draw is concerned, but really,
computing it would be far too expensive for our purpose
(real-time!). XXX maybe some reasonable approximations can
easily been computed ??? Check that
[comb] is a positive cube that ougth to contain the indexes of
boolean vars that are still to be generated, and the numerical
indexes that appears in [bdd].
*)
let _ = assert (
not (Bdd.is_cst bdd) && (Bdd.topvar comb) = (Bdd.topvar bdd) )
in
let bdd_not = (Bdd.dnot bdd) in
let (sol_nb, sol_nb_not) =
try
(* either it has already been computed ... *)
let (nt, ne) = Env_state.sol_number bdd
and (not_nt, not_ne) = Env_state.sol_number bdd_not in
(* solutions numbers in the table are absolute *)
((add_sol_nb nt ne), (add_sol_nb not_nt not_ne))
with Not_found ->
(* ... or not. *)
let (nt, not_nt) = compute_absolute_sol_nb (Bdd.dthen bdd) comb in
let (ne, not_ne) = compute_absolute_sol_nb (Bdd.delse bdd) comb in
Env_state.set_sol_number bdd (nt, ne) ;
Env_state.set_sol_number bdd_not (not_nt, not_ne) ;
((add_sol_nb nt ne), (add_sol_nb not_nt not_ne))
in
(sol_nb, sol_nb_not)
and
(compute_absolute_sol_nb: Bdd.t
(* -> Store.t *)
-> Bdd.t -> sol_nb * sol_nb) =
fun sub_bdd (* store *) comb ->
(* Returns the absolute number of solutions of [sub_bdd] (and its
negation) w.r.t. [comb], where [comb] is the comb of the
father of [sub_bdd].
The [comb] is used to know which output Boolean variables are
unconstraint along a path in the bdd. Indeed, the comb is made
of all the Boolean output var indexes plus the num contraints
indexes that appears in the bdd; hence, if the topvar of the
bdd is different from the topvar of the comb, it means that
the topvar of the comb is unsconstraint and we need to
multiply the number of solution of the branch by 2.
*)
if
Bdd.is_cst sub_bdd
then
let sol_nb =
if
Bdd.is_true comb
then
(*
XXX Take into account the number of numeric solutions (max - min)
for variables of dimension 1 (it is too expensive for greater
dimension...)
*)
1.
else
(two_power_of (List.length (Bdd.list_of_support (Bdd.dthen comb))))
in
if Bdd.is_true sub_bdd then (sol_nb, 0.0) else (0.0, sol_nb)
else
let topvar = Bdd.topvar sub_bdd in
let rec
(count_missing_vars: Bdd.t -> var_idx -> int -> Bdd.t * int) =
fun comb var_idx cpt ->
(* Returns [cpt] + the number of variables occurring in [comb]
before reaching [var_idx] ([var_idx] excluded). Also returns the comb
whch topvar is [var_idx]. *)
let _ = assert (not (Bdd.is_cst comb)) in
let combvar = Bdd.topvar comb in
if var_idx = combvar
then (comb, cpt)
else count_missing_vars (Bdd.dthen comb) var_idx (cpt+1)
in
let (sub_comb, missing_vars_nb) =
count_missing_vars (Bdd.dthen comb) topvar 0
in
let (n0, not_n0) = build_sol_nb_table sub_bdd sub_comb in
let factor = (two_power_of missing_vars_nb) in
(mult_sol_nb n0 factor, mult_sol_nb not_n0 factor)
(****************************************************************************)
(****************************************************************************)
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_idx -> subst option) =
fun var_idx ->
(* if [var_idx] is a index that corresponds to a boolean variable,
this fonction performs a toss and returns a substitution for
the corresponding boolean variable. It returns [None]
otherwise (ie if it is a num).
Indeed, if it happens that a numerical constraint does not
appear along a path, we simply ignore it and hence it will not
be added to the store.
*)
let cstr = Env_state.index_to_linear_constraint var_idx in
match cstr with
Bv(v) -> (
match v.default with
Some (Formu f) ->
let (bdd, _) = Formula_to_bdd.translate (Env_state.input ()) f in
if Bdd.is_false bdd then Some(v.n, B false)
else if Bdd.is_true bdd then Some(v.n, B true)
else
(
print_string (
"*** Default values should not depend on " ^
"controllable variables, \nwhich is the case of " ^
(formula_to_string f) ^ ", the default value of " ^
v.n ^ "\n");
exit 1
)
| Some (Expre _) -> assert false
| Some (Liste l) -> assert false
| _ -> Some(toss_up_one_var v.n)
)
| _ -> None
let rec (draw_in_bdd: subst list * Store.t -> Bdd.t -> Bdd.t ->
subst list * Store.t' * Store.p) =
fun (sl, store) bdd comb ->
(** Returns [sl] appended to a draw of all the boolean variables
bigger than the topvar of [bdd] according to the ordering
induced by the comb [comb]. Also returns the (non empty) store
obtained by adding to [store] all the numeric constraints that
were encountered during this draw.
Raises the [No_numeric_solution] exception whenever no valid
path in [bdd] leads to a satisfiable set of numeric
constraints.
*)
if
Bdd.is_true bdd
then
(* Toss the remaining bool vars. *)
let (store_int, store_poly) =
Store.switch_to_polyhedron_representation store
in
(
(List.append sl
(Util.list_map_option
toss_up_one_var_index
(Bdd.list_of_support comb))
),
store_int,
store_poly
)
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 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 e (sl, store) bdd comb
| Ineq(ineq) ->
draw_in_bdd_ineq ineq (sl, store) bdd comb
and (draw_in_bdd_bool: var -> subst list * Store.t -> Bdd.t -> Bdd.t ->
subst list * Store.t' * Store.p) =
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, or we compute its default
value (cf "~default" flag). *)
let new_sl =
match toss_up_one_var_index topvar_comb with
Some(s) -> s::sl
| None -> 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.n, B(bool1))::sl),
((var.n, 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 Env_state.verbose () then
print_string "\n..................BACKTRACK!\n";
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
| e ->
print_string ((Printexc.to_string e) ^ "\n");
flush stdout;
assert false
and (draw_in_bdd_ineq: Constraint.ineq -> subst list * Store.t -> Bdd.t -> Bdd.t ->
subst list * Store.t' * Store.p) =
fun cstr (sl, store) bdd comb ->
(*
When we add to the store an inequality constraint GZ(ne) or
GeqZ(ne) ([split_store]), 2 stores are returned. The first is a
store where the inequality has been added; the second is a
store where its negation has been added.
Whether we choose the first one or the second depends on a toss
made according the (boolean) solution number in both branches
of the bdd. If no solution is found into that branch, the other
branch with the other store is tried.
*)
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 ran = Random.float 1. in
let cstr_neg = Constraint.neg_ineq cstr in
let (cstr1, bdd1, sol_nb1, cstr2, bdd2, sol_nb2) =
if
ran < ((float_of_sol_nb n) /. (float_of_sol_nb (add_sol_nb n m)))
then
(cstr, (Bdd.dthen bdd), n, cstr_neg, (Bdd.delse bdd), m)
else
(cstr_neg, (Bdd.delse bdd), m, cstr, (Bdd.dthen bdd), n)
in
let store1 = add_constraint store (Ineq cstr1) 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
if not (is_store_satisfiable store1) then raise No_numeric_solution;
draw_in_bdd (sl, store1) bdd1 comb
with
No_numeric_solution ->
let store2 = add_constraint store (Ineq cstr2) in
(*
The second branch is tried if no path in the first
bdd leaded to a satisfiable set of numeric
constraints.
*)
if
(not (eq_sol_nb sol_nb2 zero_sol))
&& is_store_satisfiable store2
then
draw_in_bdd (sl, store2) bdd2 comb
else
raise No_numeric_solution
| e ->
print_string ((Printexc.to_string e) ^ "\n");
flush stdout;
assert false
and (draw_in_bdd_eq: Ne.t -> subst list * Store.t -> Bdd.t -> Bdd.t ->
subst list * Store.t' * Store.p) =
fun ne (sl, store) bdd comb ->
(*
We consider 3 stores:
- store + [ne = 0]
- store + [ne > 0]
- store + [ne < 0]
Whether we choose the first one or not depends on toss made
according the (boolean) solution number in both branches of the
bdd. If the else branch is choosen (if it is chosen in the
first place, or if backtracking occurs because no solutions is
found in the then branch) whether we try the second or the
third store first is (fairly) tossed up.
*)
let (n, m) = Env_state.sol_number bdd in
let _ =
if ((eq_sol_nb n zero_sol) && (eq_sol_nb m zero_sol))