Skip to content

GitLab

L
lutin
Commit da9a1255 authored by Erwan Jahier's avatar Erwan Jahier
Browse files
Options

lurette 1.32 Wed, 30 Jun 2004 14:03:33 +0200 by jahier 

Parent-Version:      1.31
Version-Log:

source/fair_bddd.ml:
   Fix a bug where the distribution was not correct according
  to the solution number

Project-Description: Lurette
parent 693db19e
Expand all Hide whitespace changes
Inline Side-by-side
Showing with 579 additions and 462 deletions
.lurette.prcs_aux
View file @ da9a1255
......@@ -2,17 +2,17 @@
;; REALLY bad things.
(Created-By-Prcs-Version 1 3 3)
(cuddaux/cuddauxGenCof.c 12011 1034006019 c/29_cuddauxGen 1.1)
(source/show_env.mli 1148 1088412276 42_show_env.m 1.13)
(source/util.ml 22751 1088412276 35_util.ml 1.69)
(test/time-asti.res 4566 1088432998 h/40_time-asti. 1.2)
(source/show_env.mli 1198 1088597013 42_show_env.m 1.14)
(source/util.ml 22779 1088597013 35_util.ml 1.70)
(test/time-asti.res 4580 1088597013 h/40_time-asti. 1.3)
(test/cygwin-scade/lib_pilot.vsp 1433 1055926783 f/47_lib_pilot. 1.1)
(source/constraint.mli 1697 1082533083 c/18_constraint 1.10)
(test/ControleurPorte.lus 3219 1032940601 c/17_Controleur 1.1)
(mlcuddidl/Changes 129 1071844798 d/10_Changes 1.2)
(TODO 5160 1088432998 d/22_TODO 1.48)
(TODO 5593 1088597013 d/22_TODO 1.49)
(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/fair_bddd.ml 20312 1078751438 g/38_fair_bddd. 1.7)
(source/fair_bddd.ml 21502 1088597013 g/38_fair_bddd. 1.8)
(source/type.mli 733 1078751438 h/11_type.mli 1.2)
(source/ne.mli 2258 1078751438 c/22_ne.mli 1.10)
(share/config.guess 39153 1055926783 f/25_config.gue 1.1)
......@@ -89,7 +89,7 @@
(test/sparc-scade/libdigital.saofdm 1256 1055487917 e/47_libdigital 1.1)
(test/temp_int.luc 517 1063786164 b/50_temp_int.e 1.7)
(source/print.mli 1130 1078751438 46_print.mli 1.15)
(test/time-joly.exp 10279 1088412276 b/48_time.exp 1.64)
(test/time-joly.exp 10271 1088597013 b/48_time.exp 1.65)
(polka/caml/Makefile 6586 1071844798 d/45_Makefile 1.4)
(test/cygwin-scade/det_mvt_mode.saofd 4184 1055926783 f/51_det_mvt_mo 1.1)
(ihm/xlurette/xlurette_glade_main.ml 62065 1088432998 c/12_xlurette_g 1.42)
......@@ -126,7 +126,7 @@
(source/env_state.ml 16403 1088432998 51_env_state. 1.61)
(test/test8.rif.exp 470 1082533083 g/18_test8.rif. 1.7)
(polka/caml/matrix.idl 6467 1076684617 d/34_matrix.idl 1.4)
(source/fair_bddd.mli 2478 1078751438 g/39_fair_bddd. 1.6)
(source/fair_bddd.mli 2479 1088597013 g/39_fair_bddd. 1.7)
(cuddaux/cuddauxAddIte.c 12812 1034006019 c/32_cuddauxAdd 1.1)
(source/gen_stubs_scade.mli 653 1078751438 f/6_gen_stubs_ 1.3)
(share/pixmaps/clean-up.xpm 1565 1055926783 f/22_clean-up.x 1.1)
......@@ -168,7 +168,7 @@
(share/pixmaps/save.xpm 867 1055926783 f/12_save.xpm 1.1)
(source/solver.mli 1790 1078751438 38_solver.mli 1.24)
(test/passerelle.luc 963 1063786164 b/17_passerelle 1.12)
(source/store.ml 36616 1083336219 b/27_rnumsolver 1.42)
(source/store.ml 36676 1088597013 b/27_rnumsolver 1.43)
(mlcuddidl/mtbdd.mli 4395 1034006019 c/43_mtbdd.mli 1.1)
(test/sparc-scade/exo1.vsp 2123 1074519403 e/49_exo1.vsp 1.2)
(polka/C/satmat.h 1254 1047029868 d/48_satmat.h 1.1)
......@@ -193,7 +193,7 @@
(test/sparc-scade/exo1.vsw 400 1055487917 e/48_exo1.vsw 1.1)
(test/heater_float.rif.exp 1305 1083336219 b/30_heater_flo 1.23)
(cuddaux/Makefile 3375 1078749975 c/35_Makefile 1.10)
(doc/lurette-man/lurette-man.tex 38450 1088412276 h/33_lurette-ma 1.1)
(doc/lurette-man/lurette-man.tex 38493 1088597013 h/33_lurette-ma 1.2)
(polka/C/bit.c 3301 1071844798 e/10_bit.c 1.2)
(source/draw.mli 446 1088412276 f/1_draw.mli 1.4)
(polka/caml/polkaIO.ml 1651 1071844798 d/44_polkaIO.ml 1.2)
......@@ -209,28 +209,28 @@
(demo-xlurette/chaudiere/chaudiere.luc 442 1076684617 c/11_chaudiere. 1.9)
(source/parser.mly 6759 1078751438 h/19_parser.mly 1.1)
(test/giro/allocator.lus 1087 1031732392 c/5_allocator. 1.1)
(source/run_aut.ml 23347 1088432998 b/47_automata.m 1.27)
(source/run_aut.ml 23378 1088597013 b/47_automata.m 1.28)
(cuddaux/README 1427 1034006019 c/34_README 1.1)
(source/gen_stubs_sildex.ml 8922 1088412276 h/38_gen_stubs_ 1.1)
(mlcuddidl/bdd.ml 11038 1071844798 d/6_bdd.ml 1.2)
(source/lurettetop.ml 66605 1088432998 c/1_lurettetop 1.55)
(source/lexeme.mli 382 1078751438 h/21_lexeme.mli 1.1)
(test/tram/tramway.luc 1138 1080290901 h/2_tramway.lu 1.2)
(source/constraint.ml 3154 1078751438 c/19_constraint 1.11)
(test/structured_type.luc 2346 1079084640 g/32_structured 1.4)
(source/constraint.ml 3143 1088597013 c/19_constraint 1.12)
(test/structured_type.luc 2301 1088597013 g/32_structured 1.5)
(source/formula_to_bdd.ml 17977 1083336219 g/34_formula_to 1.10)
(test/cygwin-scade/counter.saofd 587 1055926783 g/2_counter.sa 1.1)
(test/test7.rif.exp 470 1088412276 g/12_test7.rif. 1.10)
(test/poly-int/poly.lus 72 1073401581 h/7_poly.lus 1.1)
(source/bddd.ml 18371 1079014759 g/36_bddd.ml 1.9)
(source/bddd.ml 18395 1088597013 g/36_bddd.ml 1.10)
(ihm/xlurette/xlurette_glade_interface.ml 84937 1088432998 c/15_xlurette_g 1.30)
(source/oracle.ml 2807 1088412276 h/31_oracle.ml 1.3)
(INSTALL 479 1082533083 f/26_INSTALL 1.3)
(test/cygwin-scade/MyConsts.saofd 153 1055926783 f/44_MyConsts.s 1.1)
(test/losange-3d2.luc 355 1076684617 e/32_losange-3d 1.6)
(test/Makefile 4080 1088432998 c/0_Makefile 1.21)
(user-rules 41630 1088432998 c/14_myrules 1.63)
(test/infinite_weight.luc 1114 1083336219 g/13_infinite_w 1.3)
(user-rules 42123 1088597013 c/14_myrules 1.64)
(test/infinite_weight.luc 1114 1088597013 g/13_infinite_w 1.4)
(mlcuddidl/cudd_caml.c 23483 1071844798 d/3_cudd_caml. 1.2)
(polka/C/config.h 78 1071844798 e/13_config.h 1.2)
(test/usager.luc 454 1063786164 b/14_usager.env 1.13)
......@@ -239,9 +239,9 @@
(mlcuddidl/manager.idl 11064 1071844798 c/48_manager.id 1.2)
(source/rif.ml 7410 1088412276 h/27_rif.ml 1.3)
(mlcuddidl/cudd_caml.h 1178 1071844798 d/2_cudd_caml. 1.2)
(source/show_env.ml 3432 1088412276 43_show_env.m 1.22)
(source/show_env.ml 3430 1088597013 43_show_env.m 1.23)
(polka/C/essai.c 1001 1047029868 e/11_essai.c 1.1)
(test/time-asti.exp 4158 1088412276 h/41_time-asti. 1.1)
(test/time-asti.exp 4566 1088597013 h/41_time-asti. 1.2)
(demo-xlurette/fault-tolerant-heater/heater_control_env.luc 382 1076684617 h/16_heater_con 1.1)
(share/pixmaps/button-close.xpm 746 1055926783 f/24_button-clo 1.1)
(test/cygwin-scade/regulation.saofd 15074 1055926783 f/35_regulation 1.1)
......@@ -253,7 +253,7 @@
(OcamlMakefile 21318 1078749975 17_OcamlMakef 1.52)
(polka/caml/polka.ml 5602 1071844798 d/39_polka.ml 1.2)
(source/lurette.mli 752 1078751438 11_lurette.ml 1.17)
(test/time-rey.res 10275 1088432998 h/14_time-rey.r 1.9)
(test/time-rey.res 10276 1088597013 h/14_time-rey.r 1.10)
(share/pixmaps/halt.xpm 511 1055926783 f/18_halt.xpm 1.1)
(share/xlurette_sh.in 779 1063786164 g/20_xlurette_s 1.1)
(polka/C/matrix.c 26957 1071844798 e/7_matrix.c 1.2)
......@@ -271,7 +271,7 @@
(test/cygwin-scade/.lurette_rc 551 1063029729 f/29_.lurette_r 1.2)
(source/env_state.mli 1750 1082533083 50_env_state. 1.41)
(test/ControleurPorte.rif.exp 5436 1083336219 b/29_Controleur 1.26)
(source/show_luc.ml 4490 1088412276 e/25_show_luc.m 1.10)
(source/show_luc.ml 4509 1088597013 e/25_show_luc.m 1.11)
(share/pixmaps/quit.xpm 494 1055926783 f/14_quit.xpm 1.1)
(share/xlurette.sh.in 115 1080290901 g/21_xlurette.s 1.2)
(polka/caml/polka_lexer.mli 200 1047029868 d/41_polka_lexe 1.1)
......@@ -282,7 +282,7 @@
(polka/caml/polka_lexer.mll 786 1047029868 d/42_polka_lexe 1.1)
(cuddaux/cuddauxInt.h 2058 1034006019 c/28_cuddauxInt 1.1)
(polka/caml/polkaIO.mli 1517 1047029868 d/43_polkaIO.ml 1.1)
(test/time-joly.res 10271 1088432998 b/49_time.res 1.70)
(test/time-joly.res 10267 1088597013 b/49_time.res 1.71)
(test/cygwin-scade/det_mvt_mode_cstext.c 703 1055926783 f/33_det_mvt_mo 1.1)
(test/cygwin-scade/pilot.saofdm 394 1055926783 f/41_pilot.saof 1.1)
(source/parse_poc.mli 1131 1078751438 d/29_parse_poc. 1.5)
......@@ -319,12 +319,12 @@
(source/type.ml 2853 1078751438 h/12_type.ml 1.2)
(source/poly_draw.ml 21804 1078751438 g/43_polyDraw.m 1.4)
(cuddaux/cuddauxTDGenCof.c 15712 1034006019 c/26_cuddauxTDG 1.1)
(source/luc_exe.ml 10562 1088412276 b/32_ima_exe.ml 1.51)
(source/luc_exe.ml 10660 1088597013 b/32_ima_exe.ml 1.52)
(source/gne.mli 1845 1082533083 b/36_gne.mli 1.8)
(test/test13.rif.exp 594 1082533083 h/26_test13.rif 1.3)
(demo-xlurette/fault-tolerant-heater/degradable-sensors.luc 1366 1088412276 h/15_wearing-se 1.2)
(test/cygwin-scade/Direction_D1.saofd 1298 1055926783 f/50_Direction_ 1.1)
(source/lurette.ml 18114 1088412276 12_lurette.ml 1.92)
(source/lurette.ml 18181 1088597013 12_lurette.ml 1.93)
(share/lucky.bat.in 584 1063786164 g/28_lucky.bat. 1.1)
(share/lucky.sh.in 111 1080290901 g/27_lucky.sh.i 1.2)
(test/sparc-scade/liblinear.saofdm 1301 1055487917 e/46_liblinear. 1.1)
......@@ -349,4 +349,4 @@
(source/rif.mli 719 1080290901 h/28_rif.mli 1.1)
(mlcuddidl/Makefile 7482 1078749975 d/9_Makefile 1.12)
(source/Makefile.show_luc 1506 1076684617 b/40_Makefile.s 1.14)
(test/time-rey.exp 10279 1088412276 h/13_time-rey.e 1.7)
(test/time-rey.exp 10275 1088597013 h/13_time-rey.e 1.8)
TODO
View file @ da9a1255
......@@ -18,8 +18,27 @@ et je ne suis plus oblig
ne sont pas mis a jour) -> le retester
* time lucky -l 100 six_lines.luc
prend 5 secondes pour n=1000 alors que
time lucky -l 10 six_lines.luc
prend 170 secondes pour n=10000
!!!
*********** A faire
* Faire une experience ou je n'utilise plus du tout les bdds mais je
passe par une forme normale pour les booleans pour voir
on pourrait ainsi avoir 2 modes, pasque avec les bdds (j=1 or j=2)
donne une repartition 25/75, et depend de l'ordre dans lequel
apparaissent les monomes...
* Portage Sildex
* Un TP de Lurette pour le 2 juillet pour les partenaire de Safeair.
......
doc/lurette-man/lurette-man.tex
View file @ da9a1255
\documentclass[twoside, titlepage]{article}
\usepackage{/usr/local/common/TEXINPUTS/verimagreport}
\usepackage{/usr/local/common/TEXINPUTS/verimagreport/usr/local/common/TEXINPUTS/verimagreport}
%\usepackage{verimagreport}
\usepackage{ifthen}
......@@ -33,7 +33,7 @@
\usepackage{color,xcolor,wrapfig}
\usepackage{hyperlatex}
% \usepackage{hyperlatex}
\input{macros}
......
lurette.prj
View file @ da9a1255
;; -*- Prcs -*-
(Created-By-Prcs-Version 1 3 3)
(Project-Description "Lurette")
(Project-Version lurette 1 31)
(Parent-Version lurette 1 30)
(Project-Version lurette 1 32)
(Parent-Version lurette 1 31)
(Version-Log "
source/run_aut.ml:
source/graph.ml:
source/env_state.ml
source/lucky.ml:
source/env_state.ml:
Graph.t in now a side effet-free DT.
source/fair_bddd.ml:
Fix a bug where the distribution was not correct according
to the solution number
source/lurettetop.ml:
xlurette/xlurette.glade:
provide an error msg to xlurette when gnuplot is not installed.
")
(New-Version-Log ""
)
(Checkin-Time "Mon, 28 Jun 2004 16:29:58 +0200")
(Checkin-Time "Wed, 30 Jun 2004 14:03:33 +0200")
(Checkin-Login jahier)
(Populate-Ignore ())
(Project-Keywords)
......@@ -33,14 +24,14 @@ xlurette/xlurette.glade:
;; Sources files for luc_exe
(source/luc_exe.mli (lurette/b/31_ima_exe.ml 1.5 644))
(source/luc_exe.ml (lurette/b/32_ima_exe.ml 1.51 644))
(source/luc_exe.ml (lurette/b/32_ima_exe.ml 1.52 644))
(source/command_line_luc_exe.ml (lurette/b/33_command_li 1.27 644))
(source/command_line_luc_exe.mli (lurette/b/34_command_li 1.17 644))
;; Sources files for lurette only
(source/lurette.mli (lurette/11_lurette.ml 1.17 644))
(source/lurette.ml (lurette/12_lurette.ml 1.92 644))
(source/lurette.ml (lurette/12_lurette.ml 1.93 644))
(source/command_line.ml (lurette/b/20_command_li 1.22 644))
(source/command_line.mli (lurette/b/21_command_li 1.18 644))
......@@ -52,14 +43,14 @@ xlurette/xlurette.glade:
(source/lucky.mli (lurette/15_env.mli 1.25 644))
(source/lucky.ml (lurette/16_env.ml 1.44 644))
(source/util.ml (lurette/35_util.ml 1.69 644))
(source/util.ml (lurette/35_util.ml 1.70 644))
(source/formula_to_bdd.ml (lurette/g/34_formula_to 1.10 644))
(source/formula_to_bdd.mli (lurette/g/35_formula_to 1.7 644))
(source/fair_bddd.ml (lurette/g/38_fair_bddd. 1.7 644))
(source/fair_bddd.mli (lurette/g/39_fair_bddd. 1.6 644))
(source/bddd.ml (lurette/g/36_bddd.ml 1.9 644))
(source/fair_bddd.ml (lurette/g/38_fair_bddd. 1.8 644))
(source/fair_bddd.mli (lurette/g/39_fair_bddd. 1.7 644))
(source/bddd.ml (lurette/g/36_bddd.ml 1.10 644))
(source/bddd.mli (lurette/g/37_bddd.mli 1.10 644))
(source/solver.mli (lurette/38_solver.mli 1.24 644))
......@@ -69,13 +60,13 @@ xlurette/xlurette.glade:
(source/polyhedron.mli (lurette/d/26_polyhedron 1.10 644))
(source/store.mli (lurette/b/26_rnumsolver 1.26 644))
(source/store.ml (lurette/b/27_rnumsolver 1.42 644))
(source/store.ml (lurette/b/27_rnumsolver 1.43 644))
(source/parse_luc.mli (lurette/40_parse_env. 1.25 644))
(source/parse_luc.ml (lurette/41_parse_env. 1.62 644))
(source/show_env.mli (lurette/42_show_env.m 1.13 644))
(source/show_env.ml (lurette/43_show_env.m 1.22 644))
(source/show_env.mli (lurette/42_show_env.m 1.14 644))
(source/show_env.ml (lurette/43_show_env.m 1.23 644))
(source/print.mli (lurette/46_print.mli 1.15 644))
(source/print.ml (lurette/47_print.ml 1.27 644))
......@@ -84,7 +75,7 @@ xlurette/xlurette.glade:
(source/env_state.ml (lurette/51_env_state. 1.61 644))
(source/run_aut.mli (lurette/b/46_automata.m 1.12 644))
(source/run_aut.ml (lurette/b/47_automata.m 1.27 644))
(source/run_aut.ml (lurette/b/47_automata.m 1.28 644))
(source/sim2chro.mli (lurette/b/23_sim2chro.m 1.12 644))
(source/sim2chro.ml (lurette/b/24_sim2chro.m 1.28 644))
......@@ -111,7 +102,7 @@ xlurette/xlurette.glade:
(source/control.ml (lurette/c/4_control.ml 1.6 644))
(source/constraint.mli (lurette/c/18_constraint 1.10 644))
(source/constraint.ml (lurette/c/19_constraint 1.11 644))
(source/constraint.ml (lurette/c/19_constraint 1.12 644))
(source/ne.ml (lurette/c/21_ne.ml 1.13 644))
(source/ne.mli (lurette/c/22_ne.mli 1.10 644))
......@@ -126,7 +117,7 @@ xlurette/xlurette.glade:
(source/parse_poc.mli (lurette/d/29_parse_poc. 1.5 644))
(source/gen_fake_lutin.ml (lurette/d/16_gen_fake_l 1.8 644))
(source/show_luc.ml (lurette/e/25_show_luc.m 1.10 644))
(source/show_luc.ml (lurette/e/25_show_luc.m 1.11 644))
(source/ocaml2c.idl (lurette/e/26_ocaml2c.id 1.3 644))
(source/lurette_exe.c (lurette/e/27_lurette_ex 1.2 644))
(source/call_lurette_main.c (lurette/e/28_call_luret 1.1 644))
......@@ -156,7 +147,7 @@ xlurette/xlurette.glade:
(Makefile.common.source (lurette/e/33_Makefile.c 1.11 644))
(OcamlMakefile (lurette/17_OcamlMakef 1.52 644))
(share/Makefile.lurette.in (lurette/b/38_Makefile.l 1.32 644))
(user-rules (lurette/c/14_myrules 1.63 644))
(user-rules (lurette/c/14_myrules 1.64 644))
(share/Makefile.test.in (lurette/c/25_user-rules 1.13 644))
(Makefile (lurette/d/13_Makefile 1.4 644))
......@@ -180,17 +171,17 @@ xlurette/xlurette.glade:
(ID_EN_VRAC (lurette/0_ID_EN_VRAC 1.1 644))
(INSTALL (lurette/f/26_INSTALL 1.3 744))
(TAGS (lurette/21_TAGS 1.6 644))
(TODO (lurette/d/22_TODO 1.48 644))
(TODO (lurette/d/22_TODO 1.49 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.12 644))
(share/gnuplot-rif (lurette/e/34_gnuplot-ri 1.11 744))
(share/plot (lurette/e/35_plot 1.12 744))
(test/time-rey.exp (lurette/h/13_time-rey.e 1.7 644))
(test/time-rey.res (lurette/h/14_time-rey.r 1.9 644))
(test/time-joly.exp (lurette/b/48_time.exp 1.64 644))
(test/time-joly.res (lurette/b/49_time.res 1.70 644))
(test/time-rey.exp (lurette/h/13_time-rey.e 1.8 644))
(test/time-rey.res (lurette/h/14_time-rey.r 1.10 644))
(test/time-joly.exp (lurette/b/48_time.exp 1.65 644))
(test/time-joly.res (lurette/b/49_time.res 1.71 644))
(test/time-ecrins.res (lurette/d/20_time-ecrin 1.46 644))
(test/time-ecrins.exp (lurette/d/21_time-ecrin 1.45 644))
(test/time-moucherotte.exp (lurette/e/37_time-mouch 1.23 644))
......@@ -283,7 +274,7 @@ xlurette/xlurette.glade:
(test/losange-3d.rif.exp (lurette/e/31_losange-3d 1.10 644))
(test/test7.rif.exp (lurette/g/12_test7.rif. 1.10 644))
(test/infinite_weight.luc (lurette/g/13_infinite_w 1.3 644))
(test/infinite_weight.luc (lurette/g/13_infinite_w 1.4 644))
(test/dynamic_weight.luc (lurette/g/14_dynamic_we 1.6 644))
(test/window.luc (lurette/g/15_window.luc 1.1 644))
(test/test10.rif.exp (lurette/g/16_test10.rif 1.8 644))
......@@ -424,7 +415,7 @@ xlurette/xlurette.glade:
;; Files added by populate at Wed, 17 Sep 2003 09:47:12 +0200,
;; to version 1.1(w), by jahier:
(test/structured_type.luc (lurette/g/32_structured 1.4 644))
(test/structured_type.luc (lurette/g/32_structured 1.5 644))
;; Files added by populate at Wed, 17 Sep 2003 09:49:00 +0200,
;; to version 1.1(w), by jahier:
......@@ -586,7 +577,7 @@ xlurette/xlurette.glade:
;; Files added by populate at Tue, 01 Jun 2004 10:04:18 +0200,
;; to version 1.29(w), by jahier:
(doc/lurette-man/lurette-man.tex (lurette/h/33_lurette-ma 1.1 644))
(doc/lurette-man/lurette-man.tex (lurette/h/33_lurette-ma 1.2 644))
;; Files added by populate at Tue, 01 Jun 2004 10:04:29 +0200,
;; to version 1.29(w), by jahier:
......@@ -609,8 +600,8 @@ xlurette/xlurette.glade:
;; Files added by populate at Mon, 28 Jun 2004 10:29:06 +0200,
;; to version 1.29(w), by jahier:
(test/time-asti.res (lurette/h/40_time-asti. 1.2 644))
(test/time-asti.exp (lurette/h/41_time-asti. 1.1 644))
(test/time-asti.res (lurette/h/40_time-asti. 1.3 644))
(test/time-asti.exp (lurette/h/41_time-asti. 1.2 644))
)
(Merge-Parents)
(New-Merge-Parents)
source/bddd.ml
View file @ da9a1255
......@@ -69,7 +69,7 @@ let (sol_number_snt : snt -> Bdd.t -> sol_nb * sol_nb) =
let (sol_number : Bdd.t -> sol_nb * sol_nb) =
(sol_number_snt !snt_ref)
(sol_number_snt !snt_ref)
let (add_snt_entry : Bdd.t -> sol_nb * sol_nb -> unit) =
......@@ -191,7 +191,8 @@ and
in
let 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
let res = mult_sol_nb n0 factor in
res
......
source/constraint.ml
View file @ da9a1255
(*-----------------------------------------------------------------------
** Copyright (C) 2002, 2003 - Verimag.
** Copyright (C) - Verimag.
** This file may only be copied under the terms of the GNU Library General
** Public License
**-----------------------------------------------------------------------
......
source/fair_bddd.ml
View file @ da9a1255
......@@ -24,7 +24,6 @@ open Env_state
type sol_nb = float
let add_sol_nb = (+.)
let mult_sol_nb n m = n *. m
let zero_sol = 0.
let one_sol = 1.
......@@ -34,13 +33,26 @@ let string_of_sol_nb = string_of_float
type one_or_two = | One of float | Two of float * float
let add_sol_nb n1 n2 =
match n2 with
One m -> n1 +. m
| Two(m1, m2) -> n1 +. m1 +. m2
(** 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.
Note it may happen that the then part is splitted in 2 when we have
added an equality (ne = a): in that case, it contains the number of
solutions corresponding to the "ne < a" and to the "ne > a" part.
*)
type snt = (Bdd.t * Store.t, float * float) Hashtbl.t
type snt = (Bdd.t * Store.t, float * one_or_two) Hashtbl.t
let snt_build = ref false
(* let print_snt snt = *)
......@@ -53,7 +65,7 @@ let snt_build = ref false
(* snt *)
let snt_ref = ref (Hashtbl.create 1)
exception Solution of float * float
exception Solution of float * one_or_two
(*
nb : in bddd.ml, it was ok to look at not(bdd) in the snt
......@@ -64,6 +76,7 @@ exception Solution of float * float
constraints that were added to obtain the store) is not that easy
as switching the "then" and the "else" branches.
*)
(* exported *)
let (sol_number : Bdd.t -> sol_nb * sol_nb) =
fun bdd ->
if Bdd.is_true bdd then (1.0, 0.0)
......@@ -83,7 +96,10 @@ let (sol_number : Bdd.t -> sol_nb * sol_nb) =
raise Not_found
with
Solution(sol_nb_t, sol_nb_e) ->
sol_nb_t, sol_nb_e
match sol_nb_e with
| One m -> (sol_nb_t, m)
| Two (m1,m2) -> (sol_nb_t, (m1+.m2))
let (add_snt_entry : Bdd.t -> sol_nb * sol_nb -> unit) =
......@@ -149,7 +165,8 @@ let rec (build_sol_nb_table_rec: Bdd.t -> Bdd.t -> Store.t -> snt -> sol_nb) =
let nt = compute_absolute_sol_nb bdd_t comb store snt
and ne = compute_absolute_sol_nb bdd_e comb store snt
in
(nt, ne)
Hashtbl.replace snt (bdd, store) (nt, One ne);
(nt, One ne)
| Ineq ineq ->
let nt =
......@@ -168,7 +185,8 @@ let rec (build_sol_nb_table_rec: Bdd.t -> Bdd.t -> Store.t -> snt -> sol_nb) =
with
Store.No_numeric_solution -> 0.0
in
(nt, ne)
Hashtbl.replace snt (bdd, store) (nt, One ne);
(nt, One ne)
| EqZ ne ->
let ne_sup = (Ineq (GZ(ne)))
......@@ -182,7 +200,7 @@ let rec (build_sol_nb_table_rec: Bdd.t -> Bdd.t -> Store.t -> snt -> sol_nb) =
Store.No_numeric_solution -> 0.0
in
let ne_inf =
let n_inf =
try
let store_inf = Store.add_constraint store ne_inf in
compute_absolute_sol_nb bdd_e comb store_inf snt
......@@ -190,7 +208,7 @@ let rec (build_sol_nb_table_rec: Bdd.t -> Bdd.t -> Store.t -> snt -> sol_nb) =
Store.No_numeric_solution -> 0.0
in
let ne_sup =
let n_sup =
try
let store_sup = Store.add_constraint store ne_sup in
compute_absolute_sol_nb bdd_e comb store_sup snt
......@@ -198,9 +216,9 @@ let rec (build_sol_nb_table_rec: Bdd.t -> Bdd.t -> Store.t -> snt -> sol_nb) =
Store.No_numeric_solution -> 0.0
in
(nt, (ne_inf +. ne_sup))
Hashtbl.replace snt (bdd, store) (nt, Two (n_inf, n_sup));
(nt, Two(n_inf, n_sup))
in
Hashtbl.replace snt (bdd, store) (nt, ne);
(add_sol_nb nt ne)
in
sol_nb
......@@ -442,7 +460,11 @@ and (draw_in_bdd_rec_bool: Var.env_in -> Env_state.t -> var ->
draw_in_bdd_rec input state (new_sl, store) bdd (Bdd.dthen comb)
else
(* bddvar = combvar *)
let (n, m) = Hashtbl.find snt (bdd, store) in
let (n, m) =
match Hashtbl.find snt (bdd, store) with
(n, One m) -> n, m
| (_, Two _) -> assert false
in
let _ =
if ((eq_sol_nb n zero_sol) && (eq_sol_nb m zero_sol))
then raise No_numeric_solution ;
......@@ -453,7 +475,7 @@ and (draw_in_bdd_rec_bool: Var.env_in -> Env_state.t -> var ->
) =
let ran = Random.float 1.
and sol_nb_ratio =
(n /. (add_sol_nb n m))
(n /. (add_sol_nb n (One m)))
in
if
ran < sol_nb_ratio
......@@ -515,7 +537,11 @@ and (draw_in_bdd_rec_ineq: Var.env_in -> Env_state.t -> Constraint.ineq ->
of the bdd. If no solution is found into that branch, the other
branch with the other store is tried.
*)
let (n, m) = Hashtbl.find snt (bdd, store) in
let (n, m) =
match Hashtbl.find snt (bdd, store) with
(n, One m) -> n, m
| (_, Two _) -> assert false
in
let _ =
if ((eq_sol_nb n zero_sol) && (eq_sol_nb m zero_sol))
then raise No_numeric_solution ;
......@@ -524,7 +550,7 @@ and (draw_in_bdd_rec_ineq: Var.env_in -> Env_state.t -> Constraint.ineq ->
let cstr_neg = Constraint.neg_ineq cstr in
let (cstr1, bdd1, sol_nb1, cstr2, bdd2, sol_nb2) =
if
ran < ((n) /. ((add_sol_nb n m)))
ran < ((n) /. ((add_sol_nb n (One m))))
then
(cstr, (Bdd.dthen bdd), n, cstr_neg, (Bdd.delse bdd), m)
else
......@@ -576,78 +602,114 @@ and (draw_in_bdd_rec_eq: Var.env_in -> Env_state.t -> Ne.t ->
found in the then branch) whether we try the second or the
third store first is (fairly) tossed up.
*)
let (n, m) = Hashtbl.find snt (bdd, store) in
let (n1, n2, n3) =
match (Hashtbl.find snt (bdd, store)) with
| (ne, One _) -> assert false
| (ne, Two(nt1, nt2)) -> ne, nt1, nt2
in
let _ =
if ((eq_sol_nb n zero_sol) && (eq_sol_nb m zero_sol))
then raise No_numeric_solution ;
if (eq_sol_nb (n1+.n2+.n3) zero_sol)
then raise No_numeric_solution
in
let ran = Random.float 1.
and cstr1 = (EqZ ne)
and cstr2 = (Ineq (GZ (Ne.neg_nexpr ne)))
and cstr3 = (Ineq (GZ ne))
in
let ran0 = Random.float 1.
and ran = Random.float 1.
and cstr = (EqZ ne)
and not_cstr = (Ineq (GZ ne))
and not_cstr2 = (Ineq (GZ (Ne.neg_nexpr ne)))
let p12 = (n1 /. (n1 +. n2))
and p21 = (n2 /. (n1 +. n2))
and p23 = (n2 /. (n3 +. n2))
and p32 = (n3 /. (n3 +. n2))
and p13 = (n1 /. (n1 +. n3))
and p31 = (n3 /. (n1 +. n3))
in
let p123 = p12 *. p23
and p132 = p13 *. p32
and p213 = p21 *. p13
and p231 = p23 *. p32
and p312 = p31 *. p21
and p321 = p32 *. p21
in
let bddt = Bdd.dthen bdd
and bdde = Bdd.delse bdd
in
let c123 = (
cstr1, bddt, n1,
cstr2, bdde, n2,
cstr3, bdde, n3
)
and c132 = (
cstr1, bddt, n1,
cstr3, bdde, n3,
cstr2, bdde, n2
)
and c213 = (
cstr2, bdde, n2,
cstr1, bddt, n1,
cstr3, bdde, n3
)
and c231 = (
cstr2, bdde, n2,
cstr3, bdde, n3,
cstr1, bddt, n1
)
and c312 = (
cstr3, bdde, n3,
cstr1, bddt, n1,
cstr2, bdde, n2
)
and c321 = (
cstr3, bdde, n3,
cstr2, bdde, n2,
cstr1, bddt, n1
)
in
let sol_nb_ratio = ((n) /. ((n +. m))) in
let (
cstr1, bdd1, sol_nb1,
cstr2, bdd2, sol_nb2,
cstr3, bdd3, sol_nb3) =
cstr1', bdd1, sol_nb1,
cstr2', bdd2, sol_nb2,
cstr3', bdd3, sol_nb3) =
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.
*)
(ran < p123)
then
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
(cstr, (Bdd.dthen bdd), n,
not_cstr, (Bdd.delse bdd), m,
not_cstr2, (Bdd.delse bdd), m)
else
(not_cstr, (Bdd.delse bdd), m,
cstr, (Bdd.dthen bdd), n,
not_cstr2, (Bdd.delse bdd), m)
else
if
ran < sol_nb_ratio
(* Ditto *)
then
(cstr, (Bdd.dthen bdd), n,
not_cstr2, (Bdd.delse bdd), m,
not_cstr, (Bdd.delse bdd), m)
else
(not_cstr2, (Bdd.delse bdd), m,
cstr, (Bdd.dthen bdd), n,
not_cstr, (Bdd.delse bdd), m)
c123