Commit 7189e37a authored by Erwan Jahier's avatar Erwan Jahier
Browse files

lurette 1.6 Thu, 25 Sep 2003 17:49:07 +0200 by jahier

Parent-Version:      1.5
Version-Log:

source/solver.ml:
source/bddd.ml:
source/env_state.ml:
   Deal with the solution number table global var at the bddd module level,
   not at the env_state level. The rationale is that it makes it possible
   to have a abstract snt type that can be easily change after.

Project-Description: Lurette
parent fcdb446e
......@@ -3,7 +3,7 @@
(Created-By-Prcs-Version 1 3 3)
(cuddaux/cuddauxGenCof.c 12011 1034006019 c/29_cuddauxGen 1.1)
(source/show_env.mli 1150 1056619073 42_show_env.m 1.10)
(source/util.ml 25757 1064329011 35_util.ml 1.54)
(source/util.ml 22004 1064504947 35_util.ml 1.55)
(test/cygwin-scade/lib_pilot.vsp 1433 1055926783 f/47_lib_pilot. 1.1)
(source/constraint.mli 1606 1063029729 c/18_constraint 1.6)
(test/ControleurPorte.lus 3219 1032940601 c/17_Controleur 1.1)
......@@ -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 7747 1064415295 39_solver.ml 1.54)
(source/solver.ml 7211 1064504947 39_solver.ml 1.55)
(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,7 +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)
(source/bddd.mli 1416 1064504947 g/37_bddd.mli 1.2)
(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)
......@@ -44,10 +44,10 @@
(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)
......@@ -57,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 4394 1064415295 44_formula.ml 1.26)
(source/formula.mli 4393 1064504947 44_formula.ml 1.27)
(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)
......@@ -85,8 +85,7 @@
(ihm/xlurette/xlurette_glade_main.ml 44987 1064411282 c/12_xlurette_g 1.28)
(TAGS 9825 1007379917 21_TAGS 1.6)
(polka/C/main.tex 1961 1047029868 e/14_main.tex 1.1)
(ihm/xlurette/xlurette.glade 104718 1064411282 c/13_xlurette.g 1.22)
(test/cygwin-scade/det_mvt_mode_env.lut 333 1055926783 f/32_det_mvt_mo 1.1)
(ihm/xlurette/xlurette.glade 103210 1064504947 c/13_xlurette.g 1.23)
(test/cygwin-scade/MODULE.saofd 3026 1055926783 f/45_MODULE.sao 1.1)
(test/cygwin-scade/Command.saofd 4147 1055926783 g/6_Command.sa 1.1)
(test/cygwin-scade/lib_pilot.err 119 1055926783 f/49_lib_pilot. 1.1)
......@@ -111,7 +110,7 @@
(test/cygwin-scade/Pilot.vsw 431 1055926783 f/39_Pilot.vsw 1.1)
(share/pixmaps/open_plus.xpm 787 1055926783 f/16_open_plus. 1.1)
(share/xlurettetop.bat.in 613 1063786164 g/19_xluretteto 1.1)
(source/env_state.ml 22609 1064329011 51_env_state. 1.48)
(source/env_state.ml 21516 1064504947 51_env_state. 1.49)
(test/test8.rif.exp 341 1063786164 g/18_test8.rif. 1.1)
(polka/caml/matrix.idl 5301 1047029868 d/34_matrix.idl 1.1)
(cuddaux/cuddauxAddIte.c 12812 1034006019 c/32_cuddauxAdd 1.1)
......@@ -198,7 +197,7 @@
(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)
(source/bddd.ml 16610 1064504947 g/36_bddd.ml 1.2)
(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)
......@@ -231,7 +230,6 @@
(mlcuddidl/rdd.ml 8746 1034006019 c/41_rdd.ml 1.1)
(share/configure.in 8503 1064329011 d/11_configure. 1.14)
(test/tram.luc 1325 1063786164 b/15_tram.env 1.12)
(share/Makefile.common.in 189 1052229068 d/12_Makefile.c 1.5)
(demo-xlurette/chaudiere/buggy_chaudiere_ctrl.lus 219 1031732392 c/10_buggy_chau 1.1)
(polka/C/matrix.h 3461 1047029868 d/51_matrix.h 1.1)
(cuddaux/cuddaux.h 2381 1034006019 c/33_cuddaux.h 1.1)
......@@ -240,7 +238,7 @@
(share/lucky.el 1934 1063786164 f/7_lucky.el 1.5)
(mlcuddidl/sedscript 203 1034006019 c/38_sedscript 1.1)
(test/cygwin-scade/.lurette_rc 551 1063029729 f/29_.lurette_r 1.2)
(source/env_state.mli 6081 1064329011 50_env_state. 1.33)
(source/env_state.mli 6123 1064504947 50_env_state. 1.34)
(test/ControleurPorte.rif.exp 4688 1064329011 b/29_Controleur 1.18)
(source/show_luc.ml 4271 1063029729 e/25_show_luc.m 1.6)
(share/pixmaps/quit.xpm 494 1055926783 f/14_quit.xpm 1.1)
......@@ -271,7 +269,7 @@
(source/env.ml 8206 1064329011 16_env.ml 1.32)
(share/pixmaps/close.xpm 803 1055926783 f/21_close.xpm 1.1)
(test/time-CHAILLOL.res 8235 1063029729 g/11_time-CHAIL 1.1)
(test/time-ecrins.res 8429 1064411282 d/20_time-ecrin 1.27)
(test/time-ecrins.res 8430 1064504947 d/20_time-ecrin 1.28)
(source/value.mli 1159 1063786164 c/24_value.mli 1.4)
(polka/Makefile.config 1683 1053337243 e/20_Makefile.c 1.5)
(test/vrai_tram.lus 564 1027066799 b/6_vrai_tram. 1.2)
......@@ -284,10 +282,10 @@
(polka/documentation/Makefile 476 1047029868 e/18_Makefile 1.1)
(source/sim2chro.ml 3260 1063786164 b/24_sim2chro.m 1.20)
(cuddaux/cuddauxTDGenCof.c 15712 1034006019 c/26_cuddauxTDG 1.1)
(source/luc_exe.ml 14273 1064329011 b/32_ima_exe.ml 1.35)
(source/luc_exe.ml 14113 1064504947 b/32_ima_exe.ml 1.36)
(source/gne.mli 1853 1063029729 b/36_gne.mli 1.6)
(test/cygwin-scade/Direction_D1.saofd 1298 1055926783 f/50_Direction_ 1.1)
(source/lurette.ml 18027 1064329011 12_lurette.ml 1.74)
(source/lurette.ml 17865 1064504947 12_lurette.ml 1.75)
(polka/C/Makefile.depend 1081 1047029868 d/46_Makefile.d 1.1)
(share/lucky.bat.in 584 1063786164 g/28_lucky.bat. 1.1)
(share/lucky.sh.in 106 1063786164 g/27_lucky.sh.i 1.1)
......@@ -298,7 +296,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)
(source/formula_to_bdd.mli 1159 1064504947 g/35_formula_to 1.2)
(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)
......
......@@ -1687,6 +1687,67 @@ scade
</widget>
</widget>
<widget>
<class>GtkHBox</class>
<name>hbox33</name>
<homogeneous>False</homogeneous>
<spacing>0</spacing>
<child>
<padding>0</padding>
<expand>True</expand>
<fill>True</fill>
</child>
<widget>
<class>GtkLabel</class>
<name>label60</name>
<width>220</width>
<label> Draw Fairness versus Efficiency </label>
<justify>GTK_JUSTIFY_RIGHT</justify>
<wrap>True</wrap>
<xalign>0.5</xalign>
<yalign>0.5</yalign>
<xpad>0</xpad>
<ypad>0</ypad>
<child>
<padding>0</padding>
<expand>False</expand>
<fill>False</fill>
</child>
</widget>
<widget>
<class>GtkRadioButton</class>
<name>radiobutton_fair_draw</name>
<tooltip>Favour the draw fairness over efficiency. </tooltip>
<can_focus>True</can_focus>
<label>Fairness</label>
<active>False</active>
<draw_indicator>True</draw_indicator>
<child>
<padding>0</padding>
<expand>False</expand>
<fill>False</fill>
</child>
</widget>
<widget>
<class>GtkRadioButton</class>
<name>radiobutton10</name>
<tooltip>Favour efficiency over fairness. This means that the draw of numric variable will not be really fair (cf lucky reference manual for more explanation).</tooltip>
<can_focus>True</can_focus>
<label>Efficiency</label>
<active>True</active>
<draw_indicator>True</draw_indicator>
<group>radiobutton_fair_draw</group>
<child>
<padding>0</padding>
<expand>False</expand>
<fill>False</fill>
</child>
</widget>
</widget>
<widget>
<class>GtkHBox</class>
<name>hbox2</name>
......@@ -1877,66 +1938,6 @@ scade
</widget>
</widget>
<widget>
<class>GtkHBox</class>
<name>hbox12</name>
<homogeneous>False</homogeneous>
<spacing>0</spacing>
<child>
<padding>0</padding>
<expand>False</expand>
<fill>False</fill>
</child>
<widget>
<class>GtkLabel</class>
<name>label21</name>
<width>220</width>
<label> Use the progress bar </label>
<justify>GTK_JUSTIFY_RIGHT</justify>
<wrap>True</wrap>
<xalign>0.5</xalign>
<yalign>0.5</yalign>
<xpad>0</xpad>
<ypad>0</ypad>
<child>
<padding>0</padding>
<expand>False</expand>
<fill>False</fill>
</child>
</widget>
<widget>
<class>GtkRadioButton</class>
<name>radiobutton_show_step_on</name>
<tooltip>Migth slow down the execution a smidgin</tooltip>
<can_focus>True</can_focus>
<label>Yes</label>
<active>True</active>
<draw_indicator>True</draw_indicator>
<child>
<padding>0</padding>
<expand>False</expand>
<fill>False</fill>
</child>
</widget>
<widget>
<class>GtkRadioButton</class>
<name>radiobutton_show_step_off</name>
<can_focus>True</can_focus>
<label>No</label>
<active>False</active>
<draw_indicator>True</draw_indicator>
<group>radiobutton_show_step_on</group>
<child>
<padding>0</padding>
<expand>False</expand>
<fill>False</fill>
</child>
</widget>
</widget>
<widget>
<class>GtkHBox</class>
<name>hbox6</name>
......@@ -2058,71 +2059,6 @@ scade
</widget>
</widget>
<widget>
<class>GtkHBox</class>
<name>hbox30</name>
<homogeneous>False</homogeneous>
<spacing>0</spacing>
<child>
<padding>0</padding>
<expand>True</expand>
<fill>True</fill>
</child>
<widget>
<class>GtkLabel</class>
<name>save_session_label</name>
<label> Saved session </label>
<justify>GTK_JUSTIFY_LEFT</justify>
<wrap>False</wrap>
<xalign>0.5</xalign>
<yalign>0.5</yalign>
<xpad>0</xpad>
<ypad>0</ypad>
<child>
<padding>0</padding>
<expand>False</expand>
<fill>False</fill>
</child>
</widget>
<widget>
<class>GtkEntry</class>
<name>saved_session_file</name>
<tooltip>Name of the file the current session is saved under</tooltip>
<can_focus>True</can_focus>
<editable>True</editable>
<text_visible>True</text_visible>
<text_max_length>0</text_max_length>
<text>lurette.tgz</text>
<child>
<padding>0</padding>
<expand>False</expand>
<fill>False</fill>
</child>
</widget>
<widget>
<class>GtkButton</class>
<name>button2</name>
<border_width>4</border_width>
<tooltip>Save the current session</tooltip>
<can_focus>True</can_focus>
<signal>
<name>clicked</name>
<handler>save_session</handler>
<last_modification_time>Tue, 03 Sep 2002 14:10:44 GMT</last_modification_time>
</signal>
<label> Save session </label>
<relief>GTK_RELIEF_NORMAL</relief>
<child>
<padding>0</padding>
<expand>False</expand>
<fill>False</fill>
</child>
</widget>
</widget>
<widget>
<class>GtkLabel</class>
<name>label53</name>
......
;; -*- Prcs -*-
(Created-By-Prcs-Version 1 3 3)
(Project-Description "Lurette")
(Project-Version lurette 1 5)
(Parent-Version lurette 1 4)
(Project-Version lurette 1 6)
(Parent-Version lurette 1 5)
(Version-Log "
Split up solver.ml into 3: solver.ml, formula_to_bdd.ml, and bddd.ml.
source/solver.ml:
source/bddd.ml:
source/env_state.ml:
Deal with the solution number table global var at the bddd module level,
not at the env_state level. The rationale is that it makes it possible
to have a abstract snt type that can be easily change after.
")
(New-Version-Log ""
)
(Checkin-Time "Wed, 24 Sep 2003 16:54:55 +0200")
(Checkin-Time "Thu, 25 Sep 2003 17:49:07 +0200")
(Checkin-Login jahier)
(Populate-Ignore ())
(Project-Keywords)
......@@ -24,14 +28,14 @@ Split up solver.ml into 3: solver.ml, formula_to_bdd.ml, and bddd.ml.
;; Sources files for luc_exe
(source/luc_exe.mli (lurette/b/31_ima_exe.ml 1.2 644))
(source/luc_exe.ml (lurette/b/32_ima_exe.ml 1.35 644))
(source/luc_exe.ml (lurette/b/32_ima_exe.ml 1.36 644))
(source/command_line_luc_exe.ml (lurette/b/33_command_li 1.18 644))
(source/command_line_luc_exe.mli (lurette/b/34_command_li 1.11 644))
;; Sources files for lurette only
(source/lurette.mli (lurette/11_lurette.ml 1.13 644))
(source/lurette.ml (lurette/12_lurette.ml 1.74 644))
(source/lurette.ml (lurette/12_lurette.ml 1.75 644))
(source/command_line.ml (lurette/b/20_command_li 1.15 644))
(source/command_line.mli (lurette/b/21_command_li 1.12 644))
......@@ -43,16 +47,16 @@ Split up solver.ml into 3: solver.ml, formula_to_bdd.ml, and bddd.ml.
(source/env.mli (lurette/15_env.mli 1.19 644))
(source/env.ml (lurette/16_env.ml 1.32 644))
(source/util.ml (lurette/35_util.ml 1.54 644))
(source/util.ml (lurette/35_util.ml 1.55 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/formula_to_bdd.mli (lurette/g/35_formula_to 1.2 644))
(source/bddd.ml (lurette/g/36_bddd.ml 1.1 644))
(source/bddd.mli (lurette/g/37_bddd.mli 1.1 644))
(source/bddd.ml (lurette/g/36_bddd.ml 1.2 644))
(source/bddd.mli (lurette/g/37_bddd.mli 1.2 644))
(source/solver.mli (lurette/38_solver.mli 1.17 644))
(source/solver.ml (lurette/39_solver.ml 1.54 644))
(source/solver.ml (lurette/39_solver.ml 1.55 644))
(source/polyhedron.ml (lurette/d/25_polyhedron 1.8 644))
(source/polyhedron.mli (lurette/d/26_polyhedron 1.3 644))
......@@ -69,7 +73,7 @@ Split up solver.ml into 3: solver.ml, formula_to_bdd.ml, and bddd.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.26 644))
(source/formula.mli (lurette/44_formula.ml 1.27 644))
(source/formula.ml (lurette/45_formula.ml 1.32 644))
(source/print.mli (lurette/46_print.mli 1.13 644))
......@@ -78,8 +82,8 @@ Split up solver.ml into 3: solver.ml, formula_to_bdd.ml, and bddd.ml.
(source/eval.mli (lurette/48_eval.mli 1.11 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/env_state.mli (lurette/50_env_state. 1.34 644))
(source/env_state.ml (lurette/51_env_state. 1.49 644))
(source/automata.mli (lurette/b/46_automata.m 1.5 644))
(source/automata.ml (lurette/b/47_automata.m 1.13 644))
......@@ -152,7 +156,6 @@ Split up solver.ml into 3: solver.ml, formula_to_bdd.ml, and bddd.ml.
(share/pixmaps/button-close.xpm (lurette/f/24_button-clo 1.1 644))
(share/config.guess (lurette/f/25_config.gue 1.1 755))
(share/configure.in (lurette/d/11_configure. 1.14 644))
(share/Makefile.common.in (lurette/d/12_Makefile.c 1.5 644))
(Makefile.common.source (lurette/e/33_Makefile.c 1.5 644))
(OcamlMakefile (lurette/17_OcamlMakef 1.51 644))
(share/Makefile.lurette.in (lurette/b/38_Makefile.l 1.27 644))
......@@ -190,7 +193,7 @@ Split up solver.ml into 3: solver.ml, formula_to_bdd.ml, and bddd.ml.
(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.res (lurette/d/20_time-ecrin 1.28 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))
......@@ -244,7 +247,6 @@ Split up solver.ml into 3: solver.ml, formula_to_bdd.ml, and bddd.ml.
(test/cygwin-scade/.lurette_rc (lurette/f/29_.lurette_r 1.2 644))
(test/cygwin-scade/.lurette_rc~ (lurette/f/30_.lurette_r 1.1 644))
(test/cygwin-scade/det_mvt_mode_env.luc (lurette/f/31_det_mvt_mo 1.2 644))
(test/cygwin-scade/det_mvt_mode_env.lut (lurette/f/32_det_mvt_mo 1.1 644))
(test/cygwin-scade/det_mvt_mode_cstext.c (lurette/f/33_det_mvt_mo 1.1 644))
(test/cygwin-scade/telemetry_validation.saofd (lurette/f/34_telemetry_ 1.1 644))
(test/cygwin-scade/regulation.saofd (lurette/f/35_regulation 1.1 644))
......@@ -294,7 +296,7 @@ Split up solver.ml into 3: solver.ml, formula_to_bdd.ml, and bddd.ml.
;; xlurette
(ihm/xlurette/xlurette_glade_main.ml (lurette/c/12_xlurette_g 1.28 644))
(ihm/xlurette/xlurette.glade (lurette/c/13_xlurette.g 1.22 644))
(ihm/xlurette/xlurette.glade (lurette/c/13_xlurette.g 1.23 644))
(ihm/xlurette/xlurette_glade_interface.ml (lurette/c/15_xlurette_g 1.21 644))
(ihm/xlurette/makefile (lurette/c/16_makefile 1.17 644))
......
#
#
#
# Where to find libs
INCDIRS = @LURETTEPATH@/@HOST_TYPE@/lib @MORE_INCLUDE@
LIBDIRS = @LURETTEPATH@/@HOST_TYPE@/lib @MORE_LIB@
HOST_TYPE=@HOST_TYPE@
LURETTE_PATH = @LURETTEPATH@
......@@ -22,10 +22,58 @@ open Store
type var_idx = int
type sol_nb = Util.sol_nb
type sol_nb = float
let add_sol_nb = (+.)
let mult_sol_nb n m = n *. m
let zero_sol = 0.
let one_sol = 1.
let eq_sol_nb = (=)
let two_power_of n = 2. ** (float_of_int n)
let float_of_sol_nb sol = sol
let string_of_sol_nb = string_of_float
let rec (build_sol_nb_table: Bdd.t -> Bdd.t -> sol_nb * sol_nb) =
fun bdd comb ->
(** snt Associates to a bdd the (absolute) number of solutions
contained in its lhs (then) and rhs (else) branches. Note that
adding those two numbers only give a number of solution that is
relative to which bdd points to it.
*)
type snt = (Bdd.t, sol_nb * sol_nb) Hashtbl.t
let snt_ref = ref (Hashtbl.create 1)
let (sol_number : Bdd.t -> sol_nb * sol_nb) =
fun bdd ->
Hashtbl.find !snt_ref bdd
let (add_snt_entry : Bdd.t -> sol_nb * sol_nb -> unit) =
fun bdd sol_nb ->
Hashtbl.replace !snt_ref bdd sol_nb
let (init_snt : unit -> unit) =
fun _ ->
Hashtbl.add !snt_ref (Bdd.dtrue (Env_state.bdd_manager ())) (1.0, 0.0);
Hashtbl.add !snt_ref (Bdd.dfalse (Env_state.bdd_manager ())) (0.0, 1.0)
let (clear_snt: unit -> unit) =
fun _ ->
(* if (t mod 100) = 0
then
if Util.hashtbl_size Env_state.snt > 1000
then *)
Hashtbl.clear !snt_ref;
init_snt ()
let (sol_number_exists : Bdd.t -> snt -> bool) =
fun bdd snt ->
Hashtbl.mem snt bdd
let rec (build_sol_nb_table_rec: Bdd.t -> Bdd.t -> snt -> sol_nb * sol_nb) =
fun bdd comb snt ->
(** 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
......@@ -35,39 +83,38 @@ let rec (build_sol_nb_table: Bdd.t -> Bdd.t -> sol_nb * sol_nb) =
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
(real-time!).
[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) )
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
let (nt, ne) = Hashtbl.find snt bdd
and (not_nt, not_ne) = Hashtbl.find snt 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) ;
let (nt, not_nt) = compute_absolute_sol_nb (Bdd.dthen bdd) comb snt in
let (ne, not_ne) = compute_absolute_sol_nb (Bdd.delse bdd) comb snt in
Hashtbl.replace snt bdd (nt, ne);
Hashtbl.replace snt 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
(compute_absolute_sol_nb: Bdd.t
(* -> Store.t *)
-> Bdd.t -> sol_nb * sol_nb) =
fun sub_bdd (* store *) comb ->
-> Bdd.t -> snt -> sol_nb * sol_nb) =
fun sub_bdd (* store *) comb snt ->
(* 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].
......@@ -87,12 +134,6 @@ and
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))))
......@@ -115,11 +156,35 @@ and
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 (n0, not_n0) = build_sol_nb_table_rec sub_bdd sub_comb snt in
let factor = (two_power_of missing_vars_nb) in
(mult_sol_nb n0 factor, mult_sol_nb not_n0 factor)
let (build_sol_nb_table: Bdd.t -> Bdd.t -> unit) =
fun bdd comb ->
if
(sol_number_exists bdd !snt_ref)
then
()
else
let rec skip_unconstraint_bool_var_at_top comb v =
(* [build_sol_nb_table] supposes that the bdd and its comb
have the same top var.
*)
if Bdd.is_true comb then comb
else
let topvar = (Bdd.topvar comb) in
if v = topvar then comb
else skip_unconstraint_bool_var_at_top (Bdd.dthen comb) v
in
let comb2 = skip_unconstraint_bool_var_at_top comb (Bdd.topvar bdd) in
let _ = build_sol_nb_table_rec bdd comb2 (!snt_ref) in
()
(****************************************************************************)
(****************************************************************************)
......@@ -166,7 +231,7 @@ let (toss_up_one_var_index: var_idx -> subst option) =
| _ -> None
let rec (draw_in_bdd: subst list * Store.t -> Bdd.t -> Bdd.t ->
let rec (draw_in_bdd_rec: 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
......@@ -179,6 +244,8 @@ let rec (draw_in_bdd: subst list * Store.t -> Bdd.t -> Bdd.t ->
path in [bdd] leads to a satisfiable set of numeric
constraints.
*)
let snt = !snt_ref in
if
Bdd.is_true bdd
then
......@@ -197,99 +264,99 @@ let rec (draw_in_bdd: subst list * Store.t -> Bdd.t -> Bdd.t ->
)
else
let _ = assert (not (Bdd.is_false bdd)) in