Commit 5bf375a5 authored by Erwan Jahier's avatar Erwan Jahier

lurette 1.4 Wed, 24 Sep 2003 15:48:02 +0200 by jahier

Parent-Version:      1.3
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.

Project-Description: Lurette
parent d66521bd
......@@ -8,7 +8,7 @@
(source/constraint.mli 1606 1063029729 c/18_constraint 1.6)
(test/ControleurPorte.lus 3219 1032940601 c/17_Controleur 1.1)
(mlcuddidl/Changes 64 1034006019 d/10_Changes 1.1)
(TODO 5308 1064329011 d/22_TODO 1.24)
(TODO 5996 1064411282 d/22_TODO 1.25)
(share/gen_fake_lutin.sh.in 115 1063786164 g/30_gen_fake_l 1.1)
(mlcuddidl/rdd.mli 7174 1034006019 c/40_rdd.mli 1.1)
(source/ne.mli 2220 1063029729 c/22_ne.mli 1.7)
......@@ -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 34807 1064329011 39_solver.ml 1.52)
(source/solver.ml 35241 1064411282 39_solver.ml 1.53)
(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)
......@@ -33,7 +33,7 @@
(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)
(test/test10.rif.exp 3813 1063786164 g/16_test10.rif 1.1)
(test/test10.rif.exp 3815 1064411282 g/16_test10.rif 1.2)
(test/test-scade-cygwin.res 0 1055926783 f/28_test-scade 1.1)
(source/gen_stubs_common.ml 6381 1055487917 e/39_gen_stubs_ 1.1)
(doc/synthese 2556 1007379917 b/2_synthese 1.1)
......@@ -46,9 +46,9 @@
(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 1063786164 g/17_test9.rif. 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 7793 1063029729 d/25_polyhedron 1.7)
(source/polyhedron.ml 7871 1064411282 d/25_polyhedron 1.8)
(source/Makefile.gen_fake_lucky 528 1063786164 g/9_Makefile.g 1.2)
(polka/C/poly.c 48492 1047029868 e/5_poly.c 1.1)
(source/luc_exe.mli 447 1033738731 b/31_ima_exe.ml 1.2)
......@@ -62,7 +62,7 @@
(polka/caml/polka_caml.c 6499 1047029868 d/37_polka_caml 1.1)
(source/gen_stubs_poc.mli 636 1055926783 f/4_gen_stubs_ 1.1)
(test/losange-3d.luc 514 1063786164 d/28_losange-3d 1.4)
(test/time-moucherotte.res 4851 1064329011 e/38_time-mouch 1.7)
(test/time-moucherotte.res 4862 1064411282 e/38_time-mouch 1.8)
(polka/caml/poly.idl 8449 1047029868 d/33_poly.idl 1.1)
(polka/documentation/texinfo.tex 200195 1047029868 e/16_texinfo.te 1.1)
(polka/caml/polka_caml.h 1922 1047029868 d/36_polka_caml 1.1)
......@@ -81,17 +81,17 @@
(source/print.mli 1136 1045558187 46_print.mli 1.13)
(polka/caml/Makefile 6559 1047029868 d/45_Makefile 1.1)
(test/cygwin-scade/det_mvt_mode.saofd 4184 1055926783 f/51_det_mvt_mo 1.1)
(ihm/xlurette/xlurette_glade_main.ml 44984 1064329011 c/12_xlurette_g 1.27)
(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 104700 1064329011 c/13_xlurette.g 1.21)
(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)
(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)
(test/losange.luc 410 1046768487 d/27_losange.lu 1.2)
(test/gyro.rif.exp 10953 1063029729 e/36_gyro.rif.e 1.3)
(test/time-ecrins.exp 8233 1064329011 d/21_time-ecrin 1.25)
(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)
(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)
......@@ -150,7 +150,7 @@
(share/pixmaps/save.xpm 867 1055926783 f/12_save.xpm 1.1)
(source/solver.mli 1545 1064329011 38_solver.mli 1.16)
(test/passerelle.luc 963 1063786164 b/17_passerelle 1.12)
(source/store.ml 33806 1064329011 b/27_rnumsolver 1.26)
(source/store.ml 33533 1064411282 b/27_rnumsolver 1.27)
(mlcuddidl/mtbdd.mli 4395 1034006019 c/43_mtbdd.mli 1.1)
(test/sparc-scade/exo1.vsp 2089 1055487917 e/49_exo1.vsp 1.1)
(polka/C/satmat.h 1254 1047029868 d/48_satmat.h 1.1)
......@@ -162,8 +162,8 @@
(demo-xlurette/chaudiere/chaudiere_oracle.lus 107 1031732392 c/8_chaudiere_ 1.1)
(share/Makefile.lurette.in 4414 1063029729 b/38_Makefile.l 1.27)
(source/graph.mli 2382 1063029729 13_graph.mli 1.11)
(source/store.mli 3265 1064329011 b/26_rnumsolver 1.18)
(test/time-ossau.res 8420 1064329011 b/49_time.res 1.52)
(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)
(test/sparc-scade/libmath.saofdm 1378 1055487917 e/45_libmath.sa 1.1)
(Makefile 68 1051024737 d/13_Makefile 1.4)
......@@ -175,7 +175,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 8240 1064329011 b/48_time.exp 1.48)
(test/time-ossau.exp 8420 1064411282 b/48_time.exp 1.49)
(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)
......@@ -197,12 +197,12 @@
(test/test7.rif.exp 269 1063786164 g/12_test7.rif. 1.1)
(polka/caml/Makefile.depend 744 1063029729 d/32_Makefile.d 1.3)
(doc/archi.fig 3693 1003928781 20_archi.fig 1.1)
(ihm/xlurette/xlurette_glade_interface.ml 76896 1064329011 c/15_xlurette_g 1.20)
(ihm/xlurette/xlurette_glade_interface.ml 76914 1064411282 c/15_xlurette_g 1.21)
(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 2756 1064329011 c/0_Makefile 1.13)
(user-rules 28780 1064329011 c/14_myrules 1.43)
(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)
(polka/C/config.h 77 1047029868 e/13_config.h 1.1)
......@@ -255,24 +255,24 @@
(source/Makefile.gen_stubs 741 1063786164 b/42_Makefile.g 1.8)
(test/temp_float.luc 680 1063786164 b/51_temp_float 1.10)
(polka/C/polka.c 4969 1047029868 e/6_polka.c 1.1)
(source/polyhedron.mli 970 1063029729 d/26_polyhedron 1.2)
(source/polyhedron.mli 1153 1064411282 d/26_polyhedron 1.3)
(test/test_losange.lus 88 1055926783 f/27_test_losan 1.1)
(mlcuddidl/bdd.mli 8573 1034006019 d/5_bdd.mli 1.1)
(test/cygwin-scade/compute_path.saofd 1662 1055926783 g/5_compute_pa 1.1)
(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 4415 1063029729 e/37_time-mouch 1.6)
(test/time-moucherotte.exp 4851 1064411282 e/37_time-mouch 1.7)
(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)
(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 8431 1064329011 d/20_time-ecrin 1.26)
(test/time-ecrins.res 8429 1064411282 d/20_time-ecrin 1.27)
(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)
(source/Makefile 9290 1063786164 c/20_Makefile 1.23)
(source/Makefile 9338 1064411282 c/20_Makefile 1.24)
(source/graph.ml 3504 1063029729 14_graph.ml 1.9)
(test/cudd_gc_problem.luc 208372 1063029729 e/29_cudd_gc_pr 1.2)
(test/time-CHAILLOL.exp 8235 1063029729 g/10_time-CHAIL 1.1)
......
......@@ -40,21 +40,31 @@
- volumes des polyhedres pas calculés (=> pb d'equité)
- pour le choix des entiers, on travaille dans les reels,
puis on tronque (truncate) => l'entier tiré n'est alors parfois
meme pas solution des contraintes !!!
* dire aussi comment le tirage pour les entiers est effectué (cf brrr)
en dimension > 2
meme pas solution des contraintes !!! (cf brrr)
* dire dans la doc que on ne peut avoir qu'au plus une transition sortante
avec un poids infini (ca n'a pas un sens bien clair et on peut toujours
faire autrement). Dire aussi que 2 transitions ne peuvent a la fois avoir
meme origine et arrivée.
* expliquer la difference entre avoir f et f' sur 2 transitions differentes,
et avoir "f or f'" sur une seule transition, du point de vue des probas.
par ex, si f=(0<c<3) et f'=(3<c<4), on a respectivement 50% de chances d'etre
dans ]0;3[ dans le 1er contre 75% dans le 2eme.
* Il faut aussi documenter les probas de f=1.0 vs 0<f<1. Avec un pas de 10,
ca donne 10% vs 90% ... On pourrait donner un pas plus petit, mais ca
desiquilibrerait l'importance des reels par rapport aux entiers et
aux Booleens. Et puis f=1.0 est une valeur particuliere qu'il est légitime
de vouloir tester plus souvent...
(2) Faire une doc utilisateur pour lurette (moins urgent depuis qu'il y
a lurettetop et xlurette...)
*********** A faire
* Rajouter la precision comme un parametre externe
* Integrer la possibilité d'utiliser des types structurés avec lurette et scade
......@@ -76,7 +86,8 @@
(1) Portage Reluc
* Verifier s'il existe des methodes approximatives assez rapides
pour calculer le volume d'un polyhedre
* ajouter les options --product-mode {multiply | arbiter}
qui disent comment on multiplie 2 automates (cf papier)
......
......@@ -3817,7 +3817,7 @@ The Test Thickness (TT) is therefore given by the formula:
TT = DF x DB x (DI + DE + DV)
Note that if one of the Draw All Formula or Draw All Vertices modes is on, the TT migth change from one step to another.
Note that if one of the Draw All Formula (via DF) or Draw All Vertices (via DV) modes is on, the TT migth change from one step to another.
</label>
<justify>GTK_JUSTIFY_FILL</justify>
<wrap>True</wrap>
......
......@@ -3035,7 +3035,7 @@ The Test Thickness (TT) is therefore given by the formula:
TT = DF x DB x (DI + DE + DV)
Note that if one of the Draw All Formula or Draw All Vertices modes is on, the TT migth change from one step to another.
Note that if one of the Draw All Formula (via DF) or Draw All Vertices (via DV) modes is on, the TT migth change from one step to another.
"
~packing:(vbox24#pack ~padding:0
~fill:false
......
......@@ -609,14 +609,14 @@ class customized_callbacks = object(self)
exit 0
method on_quit_xlurette_button_clicked () =
self#top_quit_window#quit_window#show ()
method on_quit_yes_clicked () =
output_string oc "\n \n q\n" ;
flush oc;
(* (try Unix.kill (!gp_pid) Sys.sigkill with _ -> () ); *)
(* (try Unix.kill (!gp_pid) Sys.sigkill with _ -> () ); *)
(try Unix.kill (!lpid) Sys.sigkill with _ -> () );
(try Unix.kill (!pid) Sys.sigkill with _ -> () );
self#top_quit_window#quit_window#show ()
method on_quit_yes_clicked () =
self#quit ()
method on_quit_no_clicked () =
......
;; -*- Prcs -*-
(Created-By-Prcs-Version 1 3 3)
(Project-Description "Lurette")
(Project-Version lurette 1 3)
(Parent-Version lurette 1 2)
(Project-Version lurette 1 4)
(Parent-Version lurette 1 3)
(Version-Log "
source/store.ml:
source/store.ml:
source/solver.ml:
Add a numeric thickness at the numeric level.
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.
")
(New-Version-Log ""
)
(Checkin-Time "Tue, 23 Sep 2003 16:56:51 +0200")
(Checkin-Time "Wed, 24 Sep 2003 15:48:02 +0200")
(Checkin-Login jahier)
(Populate-Ignore ())
(Project-Keywords)
......@@ -46,13 +48,13 @@ 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.52 644))
(source/solver.ml (lurette/39_solver.ml 1.53 644))
(source/polyhedron.ml (lurette/d/25_polyhedron 1.7 644))
(source/polyhedron.mli (lurette/d/26_polyhedron 1.2 644))
(source/polyhedron.ml (lurette/d/25_polyhedron 1.8 644))
(source/polyhedron.mli (lurette/d/26_polyhedron 1.3 644))
(source/store.mli (lurette/b/26_rnumsolver 1.18 644))
(source/store.ml (lurette/b/27_rnumsolver 1.26 644))
(source/store.mli (lurette/b/26_rnumsolver 1.19 644))
(source/store.ml (lurette/b/27_rnumsolver 1.27 644))
(source/pnumsolver.ml (lurette/d/23_pnumsolver 1.2 644))
(source/pnumsolver.mli (lurette/d/24_pnumsolver 1.2 644))
......@@ -150,7 +152,7 @@ source/solver.ml:
(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))
(user-rules (lurette/c/14_myrules 1.43 644))
(user-rules (lurette/c/14_myrules 1.44 644))
(share/Makefile.test.in (lurette/c/25_user-rules 1.10 644))
(Makefile (lurette/d/13_Makefile 1.4 644))
......@@ -160,7 +162,7 @@ source/solver.ml:
(source/Makefile.lucky (lurette/b/41_Makefile.i 1.23 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/c/20_Makefile 1.23 644))
(source/Makefile (lurette/c/20_Makefile 1.24 644))
;; Documentation
(doc/Interface_draft (lurette/19_Interface_ 1.1 644))
......@@ -175,19 +177,19 @@ source/solver.ml:
(ID_EN_VRAC (lurette/0_ID_EN_VRAC 1.1 644))
(INSTALL (lurette/f/26_INSTALL 1.2 744))
(TAGS (lurette/21_TAGS 1.6 644))
(TODO (lurette/d/22_TODO 1.24 644))
(TODO (lurette/d/22_TODO 1.25 644))
(share/lucky_init.csh.in (lurette/e/23_lucky_init 1.8 644))
(share/lucky_init.sh.in (lurette/e/24_lucky_init 1.11 644))
(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.48 644))
(test/time-ossau.res (lurette/b/49_time.res 1.52 644))
(test/time-ecrins.res (lurette/d/20_time-ecrin 1.26 644))
(test/time-ecrins.exp (lurette/d/21_time-ecrin 1.25 644))
(test/time-moucherotte.exp (lurette/e/37_time-mouch 1.6 644))
(test/time-moucherotte.res (lurette/e/38_time-mouch 1.7 644))
(test/time-ossau.exp (lurette/b/48_time.exp 1.49 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-moucherotte.res (lurette/e/38_time-mouch 1.8 644))
;; Various files used for testing purposes
(test/cudd_gc_problem.luc (lurette/e/29_cudd_gc_pr 1.2 644))
......@@ -209,7 +211,7 @@ source/solver.ml:
(test/test_losange.lus (lurette/f/27_test_losan 1.1 644))
(test/losange-3d2.luc (lurette/e/32_losange-3d 1.3 644))
(test/onlyroll.lus (../demo-xlurette/Gyro/onlyroll.lus) :symlink)
(test/gyro.rif.exp (lurette/e/36_gyro.rif.e 1.3 644))
(test/gyro.rif.exp (lurette/e/36_gyro.rif.e 1.4 644))
(test/giro.luc (../demo-xlurette/Gyro/giro.luc) :symlink)
(test/allocator.lus (../demo-xlurette/Gyro/allocator.lus) :symlink)
......@@ -280,16 +282,16 @@ source/solver.ml:
(test/infinite_weight.luc (lurette/g/13_infinite_w 1.1 644))
(test/dynamic_weight.luc (lurette/g/14_dynamic_we 1.1 644))
(test/window.luc (lurette/g/15_window.luc 1.1 644))
(test/test10.rif.exp (lurette/g/16_test10.rif 1.1 644))
(test/test9.rif.exp (lurette/g/17_test9.rif. 1.1 644))
(test/test10.rif.exp (lurette/g/16_test10.rif 1.2 644))
(test/test9.rif.exp (lurette/g/17_test9.rif. 1.2 644))
(test/test8.rif.exp (lurette/g/18_test8.rif. 1.1 644))
(test/Makefile (lurette/c/0_Makefile 1.13 644))
(test/Makefile (lurette/c/0_Makefile 1.14 644))
;; xlurette
(ihm/xlurette/xlurette_glade_main.ml (lurette/c/12_xlurette_g 1.27 644))
(ihm/xlurette/xlurette.glade (lurette/c/13_xlurette.g 1.21 644))
(ihm/xlurette/xlurette_glade_interface.ml (lurette/c/15_xlurette_g 1.20 644))
(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_interface.ml (lurette/c/15_xlurette_g 1.21 644))
(ihm/xlurette/makefile (lurette/c/16_makefile 1.17 644))
......
......@@ -16,6 +16,9 @@ else
endif
toto:
echo "$(LURETTE_PATH)/$(HOST_TYPE)/lib"
liblurette_lib_nc.a:
cd lurette_util ; rm *; \
ar rcs liblurette_lib_nc.a ../lurette_lib.o$(EXE) ;\
......
......@@ -11,6 +11,7 @@
open Formula
open Constraint
open Value
open Util
module StringSet = struct
include Set.Make(struct type t = string let compare = compare end)
......@@ -186,7 +187,7 @@ type range =
let (build_poly_list_from_delayed_cstr :
(Formula.var_name, range) Hashtbl.t -> Constraint.ineq list ->
range Util.StringMap.t -> Constraint.ineq list -> range Util.StringMap.t *
var_name list * (Formula.vnt list * Poly.t * (int -> string)) list) =
fun tbl delayed ->
let cll = partition_constraint (List.map (fun c -> [c]) delayed) in
......@@ -232,7 +233,7 @@ let (build_poly_list_from_delayed_cstr :
for each variables in [vars_of_cl]
*)
let (ineq_min, ineq_max, vnt) =
match (Hashtbl.find tbl var) with
match (StringMap.find var tbl) with
RangeI(min, max) ->
(
(Constraint.GeqZ
......@@ -292,10 +293,14 @@ let (build_poly_list_from_delayed_cstr :
)
cll
in
Hashtbl.iter
(fun var _ ->
let all_vars_list = StringSet.elements all_vars in
let tbl2 =
List.fold_left
(fun acc var -> StringMap.remove var acc)
(* remove delayed constraints from the store *)
if StringSet.mem var all_vars then Hashtbl.remove tbl var;
)
tbl;
(StringSet.elements all_vars, res)
tbl
all_vars_list
in
(tbl2, all_vars_list, res)
......@@ -22,7 +22,13 @@ type range =
[cl] in several polyhedra (one polyhedra per group of constraints
holding on disjunct set of variables), taking into account
constraints already made on vars (which can be found in [tbl]).
Also returns the list of variables involved in [cl] as well as a new
[tbl] where the delayed constraints have been removed from the range based
store.
*)
val build_poly_list_from_delayed_cstr : (Formula.var_name, range) Hashtbl.t ->
Constraint.ineq list ->
Formula.var_name list * (Formula.vnt list * Poly.t * (int -> string)) list
val build_poly_list_from_delayed_cstr :
range Util.StringMap.t -> Constraint.ineq list ->
( range Util.StringMap.t
* Formula.var_name list
* (Formula.vnt list * Poly.t * (int -> string)) list)
......@@ -109,6 +109,7 @@ let rec (formula_to_bdd : env_in -> formula -> Bdd.t * bool) =
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]).
*)
try (Env_state.bdd f, true)
with Not_found ->
......@@ -546,22 +547,31 @@ let rec (build_sol_nb_table: Bdd.t -> Bdd.t -> sol_nb * sol_nb) =
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) )
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) ;
......@@ -570,15 +580,17 @@ let rec (build_sol_nb_table: Bdd.t -> Bdd.t -> sol_nb * sol_nb) =
in
(sol_nb, sol_nb_not)
and
(compute_absolute_sol_nb: Bdd.t -> Bdd.t -> sol_nb * sol_nb) =
fun sub_bdd comb ->
(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
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
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
......@@ -590,7 +602,8 @@ and
let sol_nb =
if
Bdd.is_true comb
then
then
(*
XXX Take into account the number of numeric solutions (max - min)
for variables of dimension 1 (it is too expensive for greater
......@@ -621,7 +634,6 @@ and
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)
(****************************************************************************)
......@@ -818,7 +830,6 @@ and (draw_in_bdd_ineq: Constraint.ineq -> subst list * Store.t -> Bdd.t -> Bdd.t
else
(cstr_neg, (Bdd.delse bdd), m, cstr, (Bdd.dthen bdd), n)
in
let store_copy = Store.copy store 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
......@@ -830,7 +841,7 @@ and (draw_in_bdd_ineq: Constraint.ineq -> subst list * Store.t -> Bdd.t -> Bdd.t
draw_in_bdd (sl, store1) bdd1 comb
with
No_numeric_solution ->
let store2 = add_constraint store_copy (Ineq cstr2) in
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
......@@ -874,7 +885,6 @@ and (draw_in_bdd_eq: Ne.t -> subst list * Store.t -> Bdd.t -> Bdd.t ->
and cstr = (EqZ ne)
and not_cstr = (Ineq (GZ ne))
and not_cstr2 = (Ineq (GZ (Ne.neg_nexpr ne)))
and store_copy = Store.copy store
in
let sol_nb_ratio =
((float_of_sol_nb n) /. (float_of_sol_nb (add_sol_nb n m)))
......@@ -933,12 +943,11 @@ and (draw_in_bdd_eq: Ne.t -> subst list * Store.t -> Bdd.t -> Bdd.t ->
draw_in_bdd (sl, store1) bdd1 comb
with
No_numeric_solution ->
let store_copy2 = Store.copy store_copy in
(*
The second branch is tried if no path in the first bdd
leaded to a satisfiable set of numeric constraints.
*)
let store2 = add_constraint store_copy cstr2 in
let store2 = add_constraint store cstr2 in
try
if
(not (is_store_satisfiable store2)) || (sol_nb2 = 0.0)
......@@ -947,7 +956,7 @@ and (draw_in_bdd_eq: Ne.t -> subst list * Store.t -> Bdd.t -> Bdd.t ->
draw_in_bdd (sl, store2) bdd2 comb
with
No_numeric_solution ->
let store3 = add_constraint store_copy2 cstr3 in
let store3 = add_constraint store cstr3 in
if
(not (is_store_satisfiable store3)) || (sol_nb3 = 0.0)
then
......@@ -961,36 +970,38 @@ and (draw_in_bdd_eq: Ne.t -> subst list * Store.t -> Bdd.t -> Bdd.t ->
(****************************************************************************)
let (compute_default_value : Store.t' -> Formula.var list -> num_subst list) =
let (compute_default_value : Store.t' -> Formula.var list ->
Store.t' * num_subst list) =
fun st varl ->
(* [varl] is the list of variable that have not been constrained at all.
For the variables that have a default value, we compute it and remove it
from the variables that still need to be drawned.
For the variables that have a default value, we compute them and remove
them from the variables that still need to be drawned.
*)
let (maybe_compute_value : num_subst list -> Formula.var -> num_subst list) =
let (maybe_compute_value : Store.t' * num_subst list -> Formula.var ->
Store.t' * num_subst list) =
fun acc var ->
match var.default with
None -> acc
| Some (Expre e) ->
let gne = expr_to_gne e (Env_state.input ()) in
(match Gne.get_constant gne with
None ->
print_string (
"*** Default values should not depend on " ^
"controllable variables, \nwhich is the case of " ^
(expr_to_string e) ^ ", the default value of " ^
var.n ^ "\n");
exit 1
| Some (I i) ->
Store.remove_var_from_range_store st var ;
(var.n, (I i))::acc
| Some (F f) ->
Store.remove_var_from_range_store st var ;
(var.n, (F f))::acc
)
| Some _ -> assert false
match var.default with
None -> acc
| Some (Expre e) ->
let gne = expr_to_gne e (Env_state.input ()) in
(match Gne.get_constant gne with
None ->
print_string (
"*** Default values should not depend on " ^
"controllable variables, \nwhich is the case of " ^
(expr_to_string e) ^ ", the default value of " ^
var.n ^ "\n");
exit 1
| Some (I i) ->
Store.remove_var_from_range_store (fst acc) var,
((var.n, (I i))::(snd acc))
| Some (F f) ->
Store.remove_var_from_range_store (fst acc) var,
((var.n, (F f))::(snd acc))
)
| Some _ -> assert false
in
List.fold_left (maybe_compute_value) [] varl
List.fold_left (maybe_compute_value) (st, []) varl
(* exported *)
......@@ -1004,7 +1015,7 @@ let (draw : num_thickness -> vn list -> var list -> Bdd.t -> Bdd.t ->
fun (k1, k2, vertices_nb) bool_vars_to_gen num_vnt_to_gen comb bdd ->
(** Draw the output and local vars to be generated by the environnent. *)
let (bool_subst_l, store_range, store_poly) =
let (bool_subst_l, store_range0, store_poly) =
draw_in_bdd ([], (Store.create num_vnt_to_gen)) bdd comb
in
let num_subst_ll0 =
......@@ -1013,8 +1024,8 @@ let (draw : num_thickness -> vn list -> var list -> Bdd.t -> Bdd.t ->
then
[]
else
let sl0 =
compute_default_value store_range (Store.get_untouched_var store_range)
let (store_range, sl0) =
compute_default_value store_range0 (Store.get_untouched_var store_range0)
in
let sll1 = draw_inside store_range store_poly k1 sl0 in
let sll2 = draw_edges store_range store_poly k2 sl0 in
......
......@@ -24,7 +24,7 @@ exception No_numeric_solution
type p = (Formula.vnt list * Poly.t * (int -> string)) list
type range_store = (Formula.var_name, Polyhedron.range) Hashtbl.t
type range_store = Polyhedron.range Util.StringMap.t
type vars_domain =
Unsat
......@@ -90,9 +90,14 @@ let (rm : Formula.var list -> var_name -> Formula.var list) =
fun varl vn ->
fst (List.partition (fun v -> v.n <> vn) varl)
let (remove_var_from_range_store : t' -> Formula.var -> unit) =
let (remove_var_from_range_store : t' -> Formula.var -> t') =
fun st var ->
Hashtbl.remove st.range var.n
{
range = StringMap.remove var.n st.range;
substl' = st.substl';
untouched' = st.untouched'
}
let (get_untouched_var : t' -> Formula.var list) =
fun st ->
......@@ -102,8 +107,7 @@ let (get_untouched_var : t' -> Formula.var list) =
(* exported *)
let (create : Formula.var list -> t) =
fun var_l ->
let (add_one_var : (Formula.var_name, range) Hashtbl.t -> Formula.var
-> unit) =
let (add_one_var :