Commit 78f40b65 authored by Erwan Jahier's avatar Erwan Jahier

lurette 0.122 Mon, 17 Feb 2003 14:50:50 +0100 by jahier

Parent-Version:      0.121
Version-Log:

When delayed constraints are remaining at bdd leaves, we were
printing a message saying that one shoud use a polyhedron solver
based instead.  Now, I really call such a polyhedron solver in order
to solve those constraints.

This means that I use to different solvers to handle interval and
polyhedron of dimension > 1.

It also means that the satisfiability of constraints over polyhedra
is only checked at bdd leaves, which, in some circumstances, migth be
inefficient. The point is that, if we chose to check the formula
satisfiability during the bdd traversal, we take the risk that a very
polyhedron is created whereas it was not necessary (because of
forthcoming equalities). And creating polyhedron with big (>15)
dimension simply runs forever, which is really bad.

nb : drawing in poyhedron not yet plugged.

source/polyhedron.ml:
source/polyhedron.mli: (new files)
    misc functions over polyhedra. The rational for creating that file
    is that rnumsolver is already much too big (and should be splitted
    some more btw).

source/solver.ml:
   One of the main change is that now, draw_in_bdd returns 2 stores.
   One is Range based, the other one is polyhedron-based.

source/rnumsolver.mli:
source/rnumsolver.ml:
   Add the function switch_to_polyhedron_representation which
   handle delayed constraint if necessary. It is meant to be called
   at bdd leaves.

source/solver.ml:
source/rnumsolver.ml:
   Also do not use split_store anymore but add_constraint. This allows
   a much more elegant and efficient implementation of draw_in_bdd and
   draw_in_bdd_eq (Now the store is buid when and only when a new branch
   should be tried because of backtracking). It is also more efficient.

source/constraint.mli
source/constraint.ml
source/ne.mli
source/ne.ml
   Implement get_vars that retreive the variables occuring in a contraint
   or an expression.

Project-Description: Lurette
parent 34cdff0c
......@@ -6,29 +6,30 @@
(test/heater_float.lus 177 1034351455 b/44_heater_flo 1.2)
(test/passerelle.luc 984 1032789516 b/17_passerelle 1.8)
(doc/synthese 2556 1007379917 b/2_synthese 1.1)
(source/polyhedron.mli 940 1045489850 d/26_polyhedron 1.1)
(test/temp_float.luc 730 1036511217 b/51_temp_float 1.4)
(test/ControleurPorte.rif.exp 4860 1034951022 b/29_Controleur 1.11)
(doc/ocamldoc.sty 1380 1008328137 b/12_ocamldoc.s 1.1)
(mlcuddidl/Makefile 7150 1034006019 d/9_Makefile 1.1)
(test/tram_simple.h 1746 1013519411 b/25_tram_simpl 1.1)
(test/time-ossau.res 6400 1044958837 b/49_time.res 1.29)
(test/time-ossau.res 6399 1045489850 b/49_time.res 1.30)
(mlcuddidl/session.ml 603 1034006019 c/37_session.ml 1.1)
(cuddaux/cuddauxGenCof.c 12011 1034006019 c/29_cuddauxGen 1.1)
(mlcuddidl/rdd.idl 14806 1034006019 c/42_rdd.idl 1.1)
(source/constraint.mli 1478 1033732198 c/18_constraint 1.4)
(source/constraint.mli 1601 1045489850 c/18_constraint 1.5)
(cuddaux/cuddauxMisc.c 13842 1034006019 c/27_cuddauxMis 1.1)
(mlcuddidl/sedscript 203 1034006019 c/38_sedscript 1.1)
(source/automata.mli 3396 1033738731 b/46_automata.m 1.3)
(test/heater_int.rif.exp 886 1034951022 b/28_heater_int 1.10)
(source/ne.ml 8857 1044958837 c/21_ne.ml 1.4)
(source/ne.ml 9275 1045489850 c/21_ne.ml 1.5)
(source/prevar.ml 981 1037192189 d/18_prevar.ml 1.1)
(test/time-ecrins.exp 6407 1044958837 d/21_time-ecrin 1.3)
(test/time-ecrins.exp 6406 1045489850 d/21_time-ecrin 1.4)
(source/value.mli 1101 1033723811 c/24_value.mli 1.1)
(user-rules.skel 1167 1040226023 c/25_user-rules 1.2)
(source/Makefile.gen_stubs 212 1036048863 b/42_Makefile.g 1.5)
(test/heater_float.rif.exp 1485 1034951022 b/30_heater_flo 1.11)
(test/temp_int.luc 685 1033723811 b/50_temp_int.e 1.3)
(source/luc_exe.ml 12235 1037625990 b/32_ima_exe.ml 1.23)
(source/luc_exe.ml 12316 1045489850 b/32_ima_exe.ml 1.24)
(source/prevar.mli 623 1037192189 d/19_prevar.mli 1.1)
(source/graph.ml 2339 1037625990 14_graph.ml 1.8)
(ihm/xlurette/makefile 1601 1040226023 c/16_makefile 1.7)
......@@ -42,19 +43,19 @@
(source/Makefile.show_luc 1026 1037192189 b/40_Makefile.s 1.8)
(source/env_state.mli 6791 1036675177 50_env_state. 1.25)
(mlcuddidl/idd.ml 7061 1034006019 d/0_idd.ml 1.1)
(test/time-ossau.exp 6400 1044958837 b/48_time.exp 1.26)
(test/time-ossau.exp 6399 1045489850 b/48_time.exp 1.27)
(source/print.mli 1145 1033397911 46_print.mli 1.12)
(mlcuddidl/rdd.mli 7174 1034006019 c/40_rdd.mli 1.1)
(test/Makefile 32 1035531408 c/0_Makefile 1.8)
(source/parse_env.ml 31534 1044958837 41_parse_env. 1.34)
(source/parse_env.ml 31323 1045489850 41_parse_env. 1.35)
(ihm/xlurette/xlurette_glade_main.ml 23620 1036675177 c/12_xlurette_g 1.15)
(demo/chaudiere/chaudiere_oracle.lus 107 1031732392 c/8_chaudiere_ 1.1)
(source/solver.ml 30116 1044958837 39_solver.ml 1.39)
(source/pnumsolver.ml 9231 1044958837 d/23_pnumsolver 1.1)
(source/solver.ml 30666 1045489850 39_solver.ml 1.40)
(source/pnumsolver.ml 9273 1045489850 d/23_pnumsolver 1.2)
(test/ControleurPorte.lus 3219 1032940601 c/17_Controleur 1.1)
(source/gen_fake_lutin.ml 3449 1036048863 d/16_gen_fake_l 1.1)
(source/lurette.ml 14220 1044958837 12_lurette.ml 1.61)
(TODO 5068 1044958837 d/22_TODO 1.2)
(TODO 5109 1045489850 d/22_TODO 1.3)
(source/Makefile 1627 1044958837 c/20_Makefile 1.10)
(source/util.ml 20845 1044958837 35_util.ml 1.37)
(mlcuddidl/manager.mli 7912 1034006019 c/46_manager.ml 1.1)
......@@ -62,13 +63,14 @@
(source/sim2chro.mli 1524 1037625990 b/23_sim2chro.m 1.6)
(source/command_line_luc_exe.mli 1055 1036675177 b/34_command_li 1.6)
(test/giro/onlyroll.lus 18298 1031732392 c/7_onlyroll.l 1.1)
(source/Makefile.lucky 2593 1044958837 b/41_Makefile.i 1.11)
(source/Makefile.lucky 2483 1045489850 b/41_Makefile.i 1.12)
(TAGS 9825 1007379917 21_TAGS 1.6)
(mlcuddidl/rdd.ml 8746 1034006019 c/41_rdd.ml 1.1)
(source/Makefile.lurette_lib 2054 1044958837 c/2_Makefile.l 1.11)
(source/Makefile.lurette_lib 1966 1045489850 c/2_Makefile.l 1.12)
(source/parse_env.mli 1028 1036511217 40_parse_env. 1.11)
(source/gen_stubs.ml 27065 1036048863 24_generate_l 1.41)
(OcamlMakefile 22696 1037192189 17_OcamlMakef 1.46)
(source/polyhedron.ml 6854 1045489850 d/25_polyhedron 1.1)
(source/command_line.ml 4914 1035557853 b/20_command_li 1.10)
(mlcuddidl/bdd.ml 10889 1034006019 d/6_bdd.ml 1.1)
(mlcuddidl/idd_caml.c 15964 1034006019 c/50_idd_caml.c 1.1)
......@@ -81,16 +83,16 @@
(mlcuddidl/README 1574 1034006019 d/8_README 1.1)
(cuddaux/README 1427 1034006019 c/34_README 1.1)
(source/Makefile.lurettetop 368 1037192189 d/14_Makefile.l 1.2)
(source/ne.mli 2117 1044958837 c/22_ne.mli 1.3)
(source/ne.mli 2092 1045489850 c/22_ne.mli 1.4)
(README 2266 1037625990 10_README 1.5)
(test/vrai_tram.lus 564 1027066799 b/6_vrai_tram. 1.2)
(source/env_state.ml 21673 1044958837 51_env_state. 1.34)
(source/env_state.ml 21354 1045489850 51_env_state. 1.35)
(mlcuddidl/manager_caml.c 39233 1034006019 c/45_manager_ca 1.1)
(mlcuddidl/mtbdd.mli 4395 1034006019 c/43_mtbdd.mli 1.1)
(source/env.mli 2026 1040290175 15_env.mli 1.17)
(mlcuddidl/rdd_caml.c 41613 1034006019 c/39_rdd_caml.c 1.1)
(Makefile.common.in 528 1034951022 d/12_Makefile.c 1.2)
(user-rules 15450 1044958837 c/14_myrules 1.22)
(user-rules 15450 1045489850 c/14_myrules 1.23)
(doc/archi.fig 3693 1003928781 20_archi.fig 1.1)
(source/lurette.mli 448 1016027474 11_lurette.ml 1.12)
(source/gne.mli 1552 1033397911 b/36_gne.mli 1.4)
......@@ -100,7 +102,7 @@
(source/luc_exe.mli 447 1033738731 b/31_ima_exe.ml 1.2)
(lurette.dep.dot 49 1007651448 b/4_lurette.de 1.2)
(mlcuddidl/bdd.idl 18233 1034006019 d/7_bdd.idl 1.1)
(source/constraint.ml 2417 1044958837 c/19_constraint 1.5)
(source/constraint.ml 2764 1045489850 c/19_constraint 1.6)
(mlcuddidl/manager.idl 11024 1034006019 c/48_manager.id 1.1)
(test/vrai_tram.c 3060 1027066799 b/8_vrai_tram. 1.3)
(Makefile 941 1035531408 d/13_Makefile 1.1)
......@@ -110,7 +112,7 @@
(source/graph.mli 2185 1037625990 13_graph.mli 1.10)
(mlcuddidl/bdd_caml.c 57199 1034006019 d/4_bdd_caml.c 1.1)
(test/heater_int.lus 170 1020068208 b/43_heater_int 1.1)
(source/pnumsolver.mli 2321 1044958837 d/24_pnumsolver 1.1)
(source/pnumsolver.mli 2322 1045489850 d/24_pnumsolver 1.2)
(cuddaux/Changes 42 1034006019 c/36_Changes 1.1)
(test/vrai_tram.h 2468 1027066799 b/7_vrai_tram. 1.3)
(test/tram.luc 1079 1032789516 b/15_tram.env 1.8)
......@@ -131,7 +133,7 @@
(mlcuddidl/bdd.mli 8573 1034006019 d/5_bdd.mli 1.1)
(doc/automata_format 0 1007379917 b/3_automata_f 1.1)
(source/solver.mli 1003 1027092697 38_solver.mli 1.13)
(source/rnumsolver.ml 21281 1044958837 b/27_rnumsolver 1.18)
(source/rnumsolver.ml 25124 1045489850 b/27_rnumsolver 1.19)
(mlcuddidl/cudd_caml.c 22890 1034006019 d/3_cudd_caml. 1.1)
(source/print.ml 5807 1033723811 47_print.ml 1.21)
(test/ControleurPorte.h 2306 1012914629 b/18_Controleur 1.1)
......@@ -141,13 +143,13 @@
(mlcuddidl/Changes 64 1034006019 d/10_Changes 1.1)
(source/parse_poc.ml 7093 1036048863 d/15_parse_poc. 1.1)
(cuddaux/cuddauxAddIte.c 12812 1034006019 c/32_cuddauxAdd 1.1)
(source/rnumsolver.mli 2155 1044958837 b/26_rnumsolver 1.11)
(source/rnumsolver.mli 2437 1045489850 b/26_rnumsolver 1.12)
(source/sim2chro.ml 2721 1033397911 b/24_sim2chro.m 1.14)
(source/command_line_luc_exe.ml 2748 1040226023 b/33_command_li 1.9)
(mlcuddidl/cudd_caml.h 1210 1034006019 d/2_cudd_caml. 1.1)
(source/value.ml 2355 1033723811 c/23_value.ml 1.1)
(source/value.ml 2364 1045489850 c/23_value.ml 1.2)
(test/giro/allocator.lus 1087 1031732392 c/5_allocator. 1.1)
(test/time-ecrins.res 6407 1044958837 d/20_time-ecrin 1.3)
(test/time-ecrins.res 6406 1045489850 d/20_time-ecrin 1.4)
(lurette.depfull.dot 49 1007651448 b/5_lurette.de 1.2)
(mlcuddidl/idd.mli 5470 1034006019 c/51_idd.mli 1.1)
(ID_EN_VRAC 2184 1002196285 0_ID_EN_VRAC 1.1)
......@@ -4,6 +4,10 @@
*********** A faire maintenant
* Verifier si je fais le bon nombre de apply.subst
* Traité les variables stables (signaux purs)
* gen_fake_lutin devrait etre une commande lurettetop et non pas code
en dur dans xlurette...
idem pour la sauvegarde des options dans .lurette-rc.
......@@ -14,8 +18,6 @@ optionnelle (par ex "types = ...")
* Mettre a jour le parseur wrt les modifs que j'ai faite a la syntax
(noeuds transiants/stationnaires)
* Supprimer tous les trap (faire un grep "with _ ->" ...)
(1) Portage pour scade et esterel windows ...
-> structure, tableau, types structures, etc.
......
;; -*- Prcs -*-
(Created-By-Prcs-Version 1 3 3)
(Project-Description "Lurette")
(Project-Version lurette 0 121)
(Parent-Version lurette 0 120)
(Version-Log "
(Project-Version lurette 0 122)
(Parent-Version lurette 0 121)
(Version-Log "
source/pnumsolver.ml:
source/pnumsolver.mli: [new files]
Implements a numeric solver based on Polka.
(not plugged yet).
When delayed constraints are remaining at bdd leaves, we were
printing a message saying that one shoud use a polyhedron solver
based instead. Now, I really call such a polyhedron solver in order
to solve those constraints.
source/rnumsolver.ml:
Reimplement split_store so that it uses 2 calls of add_constraint
instead of doing the work twice inside split_store (in order to avoid code
duplication).
This means that I use to different solvers to handle interval and
polyhedron of dimension > 1.
Also, whenever delayed constraints becomes of dimension 1, when a add_constraint
binds a value, add them to the store.
It also means that the satisfiability of constraints over polyhedra
is only checked at bdd leaves, which, in some circumstances, migth be
inefficient. The point is that, if we chose to check the formula
satisfiability during the bdd traversal, we take the risk that a very
polyhedron is created whereas it was not necessary (because of
forthcoming equalities). And creating polyhedron with big (>15)
dimension simply runs forever, which is really bad.
Enhance error msgs whenever int and float are mixed in the same lucky
expressions.
nb : drawing in poyhedron not yet plugged.
source/rnumsolver.ml:
source/ne.ml:
rename Ne.resolve_triangular_system into get_subst_from_solved_system
and move it into rnumsolver. The rational is that is was not
really solving any triangular system: the system ougth to be already solved.
source/polyhedron.ml:
source/polyhedron.mli: (new files)
misc functions over polyhedra. The rational for creating that file
is that rnumsolver is already much too big (and should be splitted
some more btw).
source/solver.ml:
One of the main change is that now, draw_in_bdd returns 2 stores.
One is Range based, the other one is polyhedron-based.
source/parce_env.ml:
Set the max_float to max_int, otherwise, the conversion into polka rational
fails...
source/rnumsolver.mli:
source/rnumsolver.ml:
Add the function switch_to_polyhedron_representation which
handle delayed constraint if necessary. It is meant to be called
at bdd leaves.
source/solver.ml:
source/rnumsolver.ml:
Also do not use split_store anymore but add_constraint. This allows
a much more elegant and efficient implementation of draw_in_bdd and
draw_in_bdd_eq (Now the store is buid when and only when a new branch
should be tried because of backtracking). It is also more efficient.
source/constraint.mli
source/constraint.ml
source/ne.mli
source/ne.ml
Implement get_vars that retreive the variables occuring in a contraint
or an expression.
")
(New-Version-Log ""
)
(Checkin-Time "Tue, 11 Feb 2003 11:20:37 +0100")
(Checkin-Time "Mon, 17 Feb 2003 14:50:50 +0100")
(Checkin-Login jahier)
(Populate-Ignore ())
(Project-Keywords)
......@@ -46,7 +68,7 @@ source/parce_env.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.23 644))
(source/luc_exe.ml (lurette/b/32_ima_exe.ml 1.24 644))
(source/command_line_luc_exe.ml (lurette/b/33_command_li 1.9 644))
(source/command_line_luc_exe.mli (lurette/b/34_command_li 1.6 644))
......@@ -68,16 +90,19 @@ source/parce_env.ml:
(source/util.ml (lurette/35_util.ml 1.37 444))
(source/solver.mli (lurette/38_solver.mli 1.13 644))
(source/solver.ml (lurette/39_solver.ml 1.39 644))
(source/solver.ml (lurette/39_solver.ml 1.40 644))
(source/rnumsolver.mli (lurette/b/26_rnumsolver 1.11 644))
(source/rnumsolver.ml (lurette/b/27_rnumsolver 1.18 644))
(source/polyhedron.ml (lurette/d/25_polyhedron 1.1 644))
(source/polyhedron.mli (lurette/d/26_polyhedron 1.1 644))
(source/pnumsolver.ml (lurette/d/23_pnumsolver 1.1 644))
(source/pnumsolver.mli (lurette/d/24_pnumsolver 1.1 644))
(source/rnumsolver.mli (lurette/b/26_rnumsolver 1.12 644))
(source/rnumsolver.ml (lurette/b/27_rnumsolver 1.19 644))
(source/pnumsolver.ml (lurette/d/23_pnumsolver 1.2 644))
(source/pnumsolver.mli (lurette/d/24_pnumsolver 1.2 644))
(source/parse_env.mli (lurette/40_parse_env. 1.11 644))
(source/parse_env.ml (lurette/41_parse_env. 1.34 644))
(source/parse_env.ml (lurette/41_parse_env. 1.35 644))
(source/show_env.mli (lurette/42_show_env.m 1.8 644))
(source/show_env.ml (lurette/43_show_env.m 1.16 644))
......@@ -92,7 +117,7 @@ source/parce_env.ml:
(source/eval.ml (lurette/49_eval.ml 1.13 644))
(source/env_state.mli (lurette/50_env_state. 1.25 644))
(source/env_state.ml (lurette/51_env_state. 1.34 644))
(source/env_state.ml (lurette/51_env_state. 1.35 644))
(source/automata.mli (lurette/b/46_automata.m 1.3 644))
(source/automata.ml (lurette/b/47_automata.m 1.6 644))
......@@ -109,13 +134,13 @@ source/parce_env.ml:
(source/control.mli (lurette/c/3_control.ml 1.3 644))
(source/control.ml (lurette/c/4_control.ml 1.4 644))
(source/constraint.mli (lurette/c/18_constraint 1.4 644))
(source/constraint.ml (lurette/c/19_constraint 1.5 644))
(source/constraint.mli (lurette/c/18_constraint 1.5 644))
(source/constraint.ml (lurette/c/19_constraint 1.6 644))
(source/ne.ml (lurette/c/21_ne.ml 1.4 644))
(source/ne.mli (lurette/c/22_ne.mli 1.3 644))
(source/ne.ml (lurette/c/21_ne.ml 1.5 644))
(source/ne.mli (lurette/c/22_ne.mli 1.4 644))
(source/value.ml (lurette/c/23_value.ml 1.1 644))
(source/value.ml (lurette/c/23_value.ml 1.2 644))
(source/value.mli (lurette/c/24_value.mli 1.1 644))
(source/prevar.ml (lurette/d/18_prevar.ml 1.1 644))
......@@ -132,16 +157,16 @@ source/parce_env.ml:
(Makefile.common.in (lurette/d/12_Makefile.c 1.2 644))
(OcamlMakefile (lurette/17_OcamlMakef 1.46 644))
(Makefile.lurette (lurette/b/38_Makefile.l 1.16 644))
(user-rules (lurette/c/14_myrules 1.22 644))
(user-rules (lurette/c/14_myrules 1.23 644))
(user-rules.skel (lurette/c/25_user-rules 1.2 644))
(Makefile (lurette/d/13_Makefile 1.1 644))
(source/Makefile.lurettetop (lurette/d/14_Makefile.l 1.2 644))
(source/Makefile.gen_fake_lutin (lurette/d/17_Makefile.g 1.1 644))
(source/Makefile.show_luc (lurette/b/40_Makefile.s 1.8 644))
(source/Makefile.lucky (lurette/b/41_Makefile.i 1.11 644))
(source/Makefile.lucky (lurette/b/41_Makefile.i 1.12 644))
(source/Makefile.gen_stubs (lurette/b/42_Makefile.g 1.5 644))
(source/Makefile.lurette_lib (lurette/c/2_Makefile.l 1.11 644))
(source/Makefile.lurette_lib (lurette/c/2_Makefile.l 1.12 644))
(source/Makefile (lurette/c/20_Makefile 1.10 644))
;; Documentation
......@@ -159,10 +184,10 @@ source/parce_env.ml:
(lurette.depfull.dot (lurette/b/5_lurette.de 1.2 644))
(TAGS (lurette/21_TAGS 1.6 644))
(test/time-ossau.exp (lurette/b/48_time.exp 1.26 644))
(test/time-ossau.res (lurette/b/49_time.res 1.29 644))
(test/time-ecrins.res (lurette/d/20_time-ecrin 1.3 644))
(test/time-ecrins.exp (lurette/d/21_time-ecrin 1.3 644))
(test/time-ossau.exp (lurette/b/48_time.exp 1.27 644))
(test/time-ossau.res (lurette/b/49_time.res 1.30 644))
(test/time-ecrins.res (lurette/d/20_time-ecrin 1.4 644))
(test/time-ecrins.exp (lurette/d/21_time-ecrin 1.4 644))
;; Various files used for testing purposes
(test/usager.luc (lurette/b/14_usager.env 1.9 644))
......@@ -249,8 +274,7 @@ source/parce_env.ml:
(mlcuddidl/Changes (lurette/d/10_Changes 1.1 644))
(TODO (lurette/d/22_TODO 1.2 644))
(TODO (lurette/d/22_TODO 1.3 644))
)
(Merge-Parents)
......
......@@ -24,8 +24,6 @@ STATIC = yes
SOURCES_OCAML = \
$(LURETTE_PATH)/polka/caml/polkaIO.mli \
$(LURETTE_PATH)/polka/caml/polkaIO.ml \
$(LURETTE_PATH)/source/util.ml \
$(LURETTE_PATH)/source/graph.mli \
$(LURETTE_PATH)/source/graph.ml \
......@@ -47,8 +45,8 @@ SOURCES_OCAML = \
$(LURETTE_PATH)/source/control.ml \
$(LURETTE_PATH)/source/parse_env.mli \
$(LURETTE_PATH)/source/parse_env.ml \
$(LURETTE_PATH)/source/pnumsolver.mli \
$(LURETTE_PATH)/source/pnumsolver.ml \
$(LURETTE_PATH)/source/polyhedron.mli \
$(LURETTE_PATH)/source/polyhedron.ml \
$(LURETTE_PATH)/source/rnumsolver.mli \
$(LURETTE_PATH)/source/rnumsolver.ml \
$(LURETTE_PATH)/source/env_state.mli \
......
......@@ -22,7 +22,6 @@ STATIC = yes
SOURCES = \
$(LURETTE_PATH)/polka/caml/polkaIO.mli $(LURETTE_PATH)/polka/caml/polkaIO.ml \
$(LURETTE_PATH)/source/util.ml \
$(LURETTE_PATH)/source/prevar.mli $(LURETTE_PATH)/source/prevar.ml \
$(LURETTE_PATH)/source/graph.mli $(LURETTE_PATH)/source/graph.ml \
......@@ -34,8 +33,8 @@ SOURCES = \
$(LURETTE_PATH)/source/gne.mli $(LURETTE_PATH)/source/gne.ml \
$(LURETTE_PATH)/source/control.mli $(LURETTE_PATH)/source/control.ml \
$(LURETTE_PATH)/source/parse_env.mli $(LURETTE_PATH)/source/parse_env.ml \
$(LURETTE_PATH)/source/polyhedron.mli $(LURETTE_PATH)/source/polyhedron.ml \
$(LURETTE_PATH)/source/rnumsolver.mli $(LURETTE_PATH)/source/rnumsolver.ml \
$(LURETTE_PATH)/source/pnumsolver.mli $(LURETTE_PATH)/source/pnumsolver.ml \
$(LURETTE_PATH)/source/env_state.mli $(LURETTE_PATH)/source/env_state.ml \
$(LURETTE_PATH)/source/solver.mli $(LURETTE_PATH)/source/solver.ml \
$(LURETTE_PATH)/source/show_env.mli $(LURETTE_PATH)/source/show_env.ml \
......
(*-----------------------------------------------------------------------
** Copyright (C) 2002 - Verimag.
** Copyright (C) 2002, 2003 - Verimag.
** This file may only be copied under the terms of the GNU Library General
** Public License
**-----------------------------------------------------------------------
......@@ -99,3 +99,20 @@ let (to_string : t -> string) =
| Ineq(ineq) -> ineq_to_string ineq
| EqZ(ne) -> ((Ne.to_string ne) ^ " = 0 ")
(* exported *)
let (get_vars_ineq : ineq -> string list) =
fun ineq ->
match ineq with
GZ(ne) -> Ne.get_vars ne
| GeqZ(ne) -> Ne.get_vars ne
(* exported *)
let (get_vars : t -> string list) =
fun ineq ->
match ineq with
Bv vn -> [vn]
| EqZ ne -> Ne.get_vars ne
| Ineq ineq -> get_vars_ineq ineq
......@@ -28,6 +28,10 @@ type t =
val dimension : t -> int
val dimension_ineq : ineq -> int
(** returns the vars appearing in a constraint *)
val get_vars : t -> string list
val get_vars_ineq : ineq -> string list
(** [apply_subst cstr s] applies [s] to [cstr]. Note that the result could
have been multiplied by a constant. *)
val apply_subst : Ne.subst -> t -> t
......
......@@ -13,7 +13,6 @@ open List
open Graph
open Formula
open Rnumsolver
(* open Pnumsolver *)
(****************************************************************************)
......@@ -565,18 +564,6 @@ let (read_env_state_one_file : string -> node) =
(* Sets the [var_names] and [pre_var_names] fields of [env_state]. *)
set_var_names file (list_in, list_out, list_loc) ;
(* Initialize the solver *)
(* Pnumsolver.solver_init *)
(* We need to extract the numeric variable to be generated *)
(* (fst *)
(* (List.split *)
(* (List.filter *)
(* (fun (vn, vt) -> vt <> BoolT) *)
(* (list_out @ list_loc) *)
(* ) *)
(* ) *)
(* ); *)
List.iter
(fun vn -> set_pre_var_names (vn::(pre_var_names ())))
list_pre_vn;
......
......@@ -433,6 +433,12 @@ and
main ();;
try main ()
with e ->
print_string ((Printexc.to_string e) ^ "\n");
flush stdout
;;
......@@ -265,21 +265,21 @@ let (nexpr_add : (Value.num * string) -> t -> t) =
(* exported *)
let (apply_subst : t -> subst -> t) =
fun ne2 ((vn, b), ne1) ->
try
if
not (StringMap.mem vn ne2)
then
ne2
else
let _ = assert (not (Value.num_eq_zero b)) in
let a = StringMap.find vn ne2 in
let a_on_b = Value.quot_num a b in
let new_ne1 =
StringMap.map
(fun x -> Value.mult_num x a)
(fun x -> Value.mult_num x a_on_b)
ne1
in
let new_ne2 =
StringMap.map
(fun x -> Value.mult_num x b)
(StringMap.remove vn ne2)
in
add new_ne1 new_ne2
with
Not_found -> ne2
let rest_ne2 = (StringMap.remove vn ne2) in
add new_ne1 rest_ne2
(* exported *)
......@@ -294,20 +294,30 @@ let (apply_simple_subst : t -> string * Value.num -> t) =
fun ne (vn, v) ->
try
let a = StringMap.find vn ne in
let ne2 = StringMap.remove vn ne in
let rest = StringMap.remove vn ne in
(
try
let b = StringMap.find "" ne in
StringMap.add "" ((Value.add_num b (Value.mult_num v a))) ne2
StringMap.add "" (Value.add_num b (Value.mult_num v a)) rest
with
Not_found ->
StringMap.add "" (Value.mult_num v a) ne2
StringMap.add "" (Value.mult_num v a) rest
)
with
Not_found -> ne
(* exported *)
let (get_vars : t -> string list) =
fun ne ->
(StringMap.fold
(fun vn _ acc -> vn::acc)
ne
[]
)
(****************************************************************************)
......@@ -317,8 +327,15 @@ let (to_string_gen : (Value.num -> string) -> string -> t -> string) =
(StringMap.fold
(fun vn v acc ->
if vn = ""
then ((nv_to_string v) ^ acc)
else (plus ^ (nv_to_string v ) ^ "" ^ ((Prevar.format vn) ^ acc)))
then
let v_str = nv_to_string v in
match v_str with
"" -> "1" ^ acc
| "-" -> "-1" ^ acc
| _ -> (v_str ^ acc)
else
(plus ^ (nv_to_string v ) ^ "" ^ ((Prevar.format vn) ^ acc))
)
ne
""
)
......@@ -328,6 +345,11 @@ let (to_string : t -> string) =
fun ne ->
to_string_gen (num_value_to_string) " + " ne
(* exported *)
let (print : t -> unit) =
fun ne ->
print_string (to_string ne)
(* exported *)
let (substl_to_string : subst list -> string) =
fun sl ->
......
......@@ -55,9 +55,7 @@ val find : string -> t -> Value.num option
val nexpr_add : (Value.num * string) -> t -> t
(** [apply_subst ne s] applies [s] to [ne]. Note that the result can
be multiplied by a constant, so this function needs to be used for
constraint.t only. *)
(** [apply_subst ne s] applies [s] to [ne]. *)
val apply_subst : t -> subst -> t
val apply_substl : subst list -> t -> t
......@@ -65,6 +63,10 @@ val apply_substl : subst list -> t -> t
val apply_simple_subst : t -> string * Value.num -> t
(** returns the vars appearing in an normal expression *)
val get_vars : t -> string list
(** Pretty printing. *)
val substl_to_string : subst list -> string
val to_string_gen : (Value.num -> string) -> string -> t -> string
......
......@@ -37,15 +37,9 @@ let lexer = Genlex.make_lexer ["("; ")"; ","; ";"; ".";
type aut_token = Genlex.token Stream.t
let default_max_float = float_of_int max_int
(* otherwise, the conversion into polka rational would fail... *)
(* let default_max_float = 10. ** 11. *)
(* Should not be bigger that max_float/2 so that the whole domain is
not bigger than max_float
XXX What should be that default value by the way ?
*)
let default_max_float = 1000.
let default_max_int = 1000
let default_min_int = -1000
let print_err_msg ic tok tok_list func msg msg2 =
......@@ -341,7 +335,7 @@ and (parse_var: in_channel -> aut_token -> vnt) =
( match typ with
"bool" -> (var, BoolT)
| "float" -> (var, FloatT(-.default_max_float, default_max_float))
| "int" -> (var, IntT(min_int / 2, max_int / 2))
| "int" -> (var, IntT(default_min_int / 2, default_max_int / 2))
(* We divide by 2 so that domains are always smaller
than max_int *)
| str ->
......
......@@ -61,18 +61,16 @@ let (rat_of_float : float -> int * int) =
(* We need to translaste expressions into a string of the format used
by Polka to parse constraints *)
let rec (ineq_to_string : Constraint.ineq -> string) =
let rec (ineq_to_polka_string : Constraint.ineq -> string) =
fun f ->
let str =
match f with
| Constraint.GZ(ne) ->
((Ne.to_string_gen (nv_to_string) "" ne) ^ " >= 0 ")
(* XXX APPROXIMATION : David ne gere pas les inegalités strictes *)
((Ne.to_string_gen (nv_to_string) "" ne) ^ " > 0 ")
(* ZZZ : David do not hold strict inequality *)
| Constraint.GeqZ(ne) ->
((Ne.to_string_gen (nv_to_string) "" ne) ^ " >= 0 ")
in
(* XXX *)
print_string ("*** " ^ str ^ "\n"); flush stdout;
str
and
(constraint_to_string : Constraint.t -> string) =
......@@ -80,12 +78,10 @@ and
let str =
match f with
| Constraint.Bv(str) -> str
| Constraint.Ineq(ineq) -> ineq_to_string ineq
| Constraint.Ineq(ineq) -> ineq_to_polka_string ineq
| Constraint.EqZ(ne) ->
((Ne.to_string_gen (nv_to_string) "" ne) ^ " = 0 ")
in
(* xxx *)
print_string ("*** " ^ str ^ "\n"); flush stdout;
str
and
(nv_to_string : Value.num -> string) =
......@@ -113,36 +109,40 @@ let (new_store : Formula.vnt list -> store) =
if
l = 0
then
(
let p = { vntl = vnt ; poly = Poly.empty 0 } in
print_string " -> Pas de numeriques !!!\n";
flush stdout ;
let p = { vntl = vnt ; poly = Poly.empty 0 } in
(* print_string " **************** !!!\n"; *)
(* flush stdout ; *)
p
)
(* No numeric values: this store will not be used *)
p
(* No numeric values: this store will not be used *)
else
let (add_one_var : Poly.t -> Formula.vnt -> Poly.t) =
fun poly (vn, vt) ->
let (min, max) =
let (ineq_min, ineq_max) =
match vt with
Formula.IntT(min, max) ->
(int_to_string min, int_to_string max)
(
GeqZ(Ne.diff (Ne.make vn I(1)) (Ne.make "" I(min))),
GeqZ(Ne.diff (Ne.make "" I(max) (Ne.make vn I(1)))),
)
| Formula.FloatT(min, max) ->
(float_to_string min, float_to_string max)
(
GeqZ(Ne.diff (Ne.make vn F(1.)) (Ne.make "" F(min))),
GeqZ(Ne.diff (Ne.make "" F(max) (Ne.make vn F(1.)))),
)
| Formula.BoolT -> assert false
in
let v1 = PolkaIO.vector_of_constraint (min ^ "<=" ^ vn)
and v2 = PolkaIO.vector_of_constraint (vn ^ "<=" ^ max)
in
print_string ("*** " ^ min ^ "<=" ^ vn ^ "\n");
print_string ("*** " ^ vn ^ "<=" ^ max ^ "\n");
PolkaIO.poly_print (Format.std_formatter) poly ;
print_string "\n";
flush stdout ;
Poly.add_constraint (Poly.add_constraint poly v1) v2
let v1 =
PolkaIO.vector_of_constraint (ineq_to_polka_string ineq_min)
and v2 =
PolkaIO.vector_of_constraint (ineq_to_polka_string ineq_max)
in
print_string ((ineq_to_polka_string ineq_min) ^ "\n");
print_string ((ineq_to_polka_string ineq_max) ^ "\n");
PolkaIO.poly_print (Format.std_formatter) poly ;
print_string "\n";
flush stdout ;
Poly.add_constraint (Poly.add_constraint poly v1) v2
in
{
vntl = vnt ;
......
......@@ -68,3 +68,4 @@ val get_all_verteces : store -> Formula.subst list list
(** Pretty printing *)
val store_to_string : store -> string
(*-----------------------------------------------------------------------
** Copyright (C) 2003 - Verimag.
** This file may only be copied under the terms of the GNU Library General
** Public License
**-----------------------------------------------------------------------
**
** File: polyhedron.ml
** Main author: jahier@imag.fr
*)
open Constraint
open Value
module StringSet = struct
include Set.Make(struct type t = string let compare = compare end)
end
let (get_vars_cl : Constraint.ineq list -> StringSet.t) =
fun cl ->
(* get the set of variables contained in a list of inequalities *)
StringSet.remove ""
(List.fold_left
(fun set c ->
let vars = Constraint.get_vars_ineq c in
List.fold_left
(fun set var -> StringSet.add var set)