Commit 3ea22e95 authored by Erwan Jahier's avatar Erwan Jahier

lurette 0.124 Fri, 21 Feb 2003 14:29:21 +0100 by jahier

Parent-Version:      0.123
Version-Log:

Implement the polyhedron drawing primitives.

source/util.ml.in:
   Change my_string_of_float so that it truncates floats 4 digits after the
dot.
   The rational is that, for testing, we do not care the extra precision and
   too much precision may kill Polka. This precison ougth to be a parameter
   though.

source/solver.ml:
source/polyhedron.ml:
source/store.ml:
    Implement the polyhedron drawing primitives.

source/store.ml:
   Apply the substitutions in store.subtsl to the cstr to add.

Project-Description: Lurette
parent a13cc8e1
......@@ -2,7 +2,7 @@
;; REALLY bad things.
(Created-By-Prcs-Version 1 3 3)
(source/automata.ml 15954 1036675177 b/47_automata.m 1.6)
(source/formula.mli 2771 1045558187 44_formula.ml 1.20)
(source/formula.mli 2811 1045834161 44_formula.ml 1.21)
(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)
......@@ -12,7 +12,7 @@
(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 6399 1045558187 b/49_time.res 1.31)
(test/time-ossau.res 6399 1045834161 b/49_time.res 1.32)
(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)
......@@ -22,13 +22,13 @@
(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 9275 1045489850 c/21_ne.ml 1.5)
(source/store.mli 2723 1045558187 b/26_rnumsolver 1.13)
(source/store.mli 2967 1045834161 b/26_rnumsolver 1.14)
(source/prevar.ml 981 1037192189 d/18_prevar.ml 1.1)
(test/time-ecrins.exp 6406 1045558187 d/21_time-ecrin 1.5)
(test/time-ecrins.exp 6398 1045834161 d/21_time-ecrin 1.6)
(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/heater_float.rif.exp 1116 1045834161 b/30_heater_flo 1.12)
(test/temp_int.luc 685 1033723811 b/50_temp_int.e 1.3)
(source/luc_exe.ml 12316 1045489850 b/32_ima_exe.ml 1.24)
(source/prevar.mli 623 1037192189 d/19_prevar.mli 1.1)
......@@ -44,34 +44,34 @@
(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 6399 1045558187 b/48_time.exp 1.28)
(test/time-ossau.exp 6399 1045834161 b/48_time.exp 1.29)
(source/print.mli 1136 1045558187 46_print.mli 1.13)
(mlcuddidl/rdd.mli 7174 1034006019 c/40_rdd.mli 1.1)
(test/Makefile 32 1035531408 c/0_Makefile 1.8)
(source/parse_env.ml 31326 1045558187 41_parse_env. 1.36)
(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 29712 1045558187 39_solver.ml 1.41)
(source/solver.ml 29805 1045834161 39_solver.ml 1.42)
(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 5109 1045489850 d/22_TODO 1.3)
(TODO 5540 1045834161 d/22_TODO 1.4)
(source/Makefile 1627 1044958837 c/20_Makefile 1.10)
(source/util.ml 20844 1045558187 35_util.ml 1.38)
(source/util.ml 21117 1045834161 35_util.ml 1.39)
(mlcuddidl/manager.mli 7912 1034006019 c/46_manager.ml 1.1)
(doc/Interface_draft 5232 1003928781 19_Interface_ 1.1)
(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 2473 1045558187 b/41_Makefile.i 1.13)
(source/Makefile.lucky 2562 1045834161 b/41_Makefile.i 1.14)
(TAGS 9825 1007379917 21_TAGS 1.6)
(mlcuddidl/rdd.ml 8746 1034006019 c/41_rdd.ml 1.1)
(source/Makefile.lurette_lib 1956 1045558187 c/2_Makefile.l 1.13)
(source/Makefile.lurette_lib 2023 1045834161 c/2_Makefile.l 1.14)
(source/parse_env.mli 1028 1036511217 40_parse_env. 1.11)
(source/gen_stubs.ml 27065 1036048863 24_generate_l 1.41)
(OcamlMakefile 22765 1045558187 17_OcamlMakef 1.47)
(source/polyhedron.ml 6983 1045558187 d/25_polyhedron 1.2)
(source/polyhedron.ml 7493 1045834161 d/25_polyhedron 1.3)
(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)
......@@ -84,7 +84,7 @@
(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 2092 1045489850 c/22_ne.mli 1.4)
(source/ne.mli 2116 1045834161 c/22_ne.mli 1.5)
(README 2266 1037625990 10_README 1.5)
(test/vrai_tram.lus 564 1027066799 b/6_vrai_tram. 1.2)
(source/env_state.ml 21336 1045558187 51_env_state. 1.36)
......@@ -96,7 +96,7 @@
(user-rules 15719 1045558187 c/14_myrules 1.24)
(doc/archi.fig 3693 1003928781 20_archi.fig 1.1)
(source/lurette.mli 448 1016027474 11_lurette.ml 1.12)
(source/store.ml 24968 1045558187 b/27_rnumsolver 1.20)
(source/store.ml 30305 1045834161 b/27_rnumsolver 1.21)
(source/gne.mli 1552 1033397911 b/36_gne.mli 1.4)
(test/giro/giro.luc 2755 1033738731 c/6_giro.ima 1.4)
(source/show_env.mli 1091 1033738731 42_show_env.m 1.8)
......@@ -122,7 +122,7 @@
(mlcuddidl/mtbdd.ml 10185 1034006019 c/44_mtbdd.ml 1.1)
(demo/chaudiere/chaudiere_ctrl.lus 177 1031732392 c/9_chaudiere_ 1.1)
(source/control.mli 3208 1036675177 c/3_control.ml 1.3)
(source/formula.ml 5869 1045558187 45_formula.ml 1.25)
(source/formula.ml 5909 1045834161 45_formula.ml 1.26)
(cuddaux/Makefile 3091 1034006019 c/35_Makefile 1.1)
(test/test_gen_stubs.h 1818 1020068208 b/45_test_gen_s 1.1)
(doc/ocamldoc.hva 313 1008328137 b/13_ocamldoc.h 1.1)
......@@ -149,7 +149,7 @@
(mlcuddidl/cudd_caml.h 1210 1034006019 d/2_cudd_caml. 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 6406 1045558187 d/20_time-ecrin 1.5)
(test/time-ecrins.res 6398 1045834161 d/20_time-ecrin 1.6)
(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,7 +4,8 @@
*********** A faire maintenant
* Verifier si je fais le bon nombre de apply.subst
* Rajouter la precision des calculs comme parametres de lurette/lucky
* Traité les variables stables (signaux purs)
......@@ -16,7 +17,7 @@
optionnelle (par ex "types = ...")
* Mettre a jour le parseur wrt les modifs que j'ai faite a la syntax
(noeuds transiants/stationnaires)
(noeuds transiants/stationnaires + formula = ...)
(1) Portage pour scade et esterel windows ...
......@@ -40,6 +41,13 @@ optionnelle (par ex "types = ...")
* Faire un gestionnaire de sessions comme le propose Pascal
* Si jamais on a à faire a des polyedres trop gros, on pourrait
peut-etre chercher a remettre en cause les choix qui ont été faits
lors des egalités (ie, le choix de la variable à substituer). Ce calcul
coute peut-etre un peu cher (car, comment faire autrement qu'essayer
toutes les possxibilités), mais au moins, ca donnerais une solution
dans des cas ou les polyedres peteraient...
* zipper et dezipper les .rif a la vollée (cf zlib)
......
;; -*- Prcs -*-
(Created-By-Prcs-Version 1 3 3)
(Project-Description "Lurette")
(Project-Version lurette 0 123)
(Parent-Version lurette 0 122)
(Project-Version lurette 0 124)
(Parent-Version lurette 0 123)
(Version-Log "
source/rnumsolver.mli:
source/rnumsolver.ml:
source/store.mli:
source/store.ml:
Rename rnumsolver into store.
Implement the polyhedron drawing primitives.
source/util.ml.in:
Change my_string_of_float so that it truncates floats 4 digits after the dot.
The rational is that, for testing, we do not care the extra precision and
too much precision may kill Polka. This precison ougth to be a parameter
though.
source/solver.ml:
source/parse_env.ml:
Do not explicitely handle dis-equalities but transform it using
not and = instead. The rational for this change is to avoid code duplication
(which was buggy !!!), but also to allow handle dis-equalities with
the optimized algorithm I had for eqalities (for free) !
source/polyhedron.ml:
source/store.ml:
Implement the polyhedron drawing primitives.
source/store.ml:
Apply the substitutions in store.subtsl to the cstr to add.
")
(New-Version-Log ""
)
(Checkin-Time "Tue, 18 Feb 2003 09:49:47 +0100")
(Checkin-Time "Fri, 21 Feb 2003 14:29:21 +0100")
(Checkin-Login jahier)
(Populate-Ignore ())
(Project-Keywords)
......@@ -51,16 +54,16 @@ source/parse_env.ml:
(source/env.mli (lurette/15_env.mli 1.17 644))
(source/env.ml (lurette/16_env.ml 1.29 644))
(source/util.ml (lurette/35_util.ml 1.38 444))
(source/util.ml (lurette/35_util.ml 1.39 444))
(source/solver.mli (lurette/38_solver.mli 1.13 644))
(source/solver.ml (lurette/39_solver.ml 1.41 644))
(source/solver.ml (lurette/39_solver.ml 1.42 644))
(source/polyhedron.ml (lurette/d/25_polyhedron 1.2 644))
(source/polyhedron.ml (lurette/d/25_polyhedron 1.3 644))
(source/polyhedron.mli (lurette/d/26_polyhedron 1.1 644))
(source/store.mli (lurette/b/26_rnumsolver 1.13 644))
(source/store.ml (lurette/b/27_rnumsolver 1.20 644))
(source/store.mli (lurette/b/26_rnumsolver 1.14 644))
(source/store.ml (lurette/b/27_rnumsolver 1.21 644))
(source/pnumsolver.ml (lurette/d/23_pnumsolver 1.2 644))
(source/pnumsolver.mli (lurette/d/24_pnumsolver 1.2 644))
......@@ -71,8 +74,8 @@ source/parse_env.ml:
(source/show_env.mli (lurette/42_show_env.m 1.8 644))
(source/show_env.ml (lurette/43_show_env.m 1.16 644))
(source/formula.mli (lurette/44_formula.ml 1.20 644))
(source/formula.ml (lurette/45_formula.ml 1.25 644))
(source/formula.mli (lurette/44_formula.ml 1.21 644))
(source/formula.ml (lurette/45_formula.ml 1.26 644))
(source/print.mli (lurette/46_print.mli 1.13 644))
(source/print.ml (lurette/47_print.ml 1.22 644))
......@@ -102,7 +105,7 @@ source/parse_env.ml:
(source/constraint.ml (lurette/c/19_constraint 1.6 644))
(source/ne.ml (lurette/c/21_ne.ml 1.5 644))
(source/ne.mli (lurette/c/22_ne.mli 1.4 644))
(source/ne.mli (lurette/c/22_ne.mli 1.5 644))
(source/value.ml (lurette/c/23_value.ml 1.2 644))
(source/value.mli (lurette/c/24_value.mli 1.1 644))
......@@ -128,9 +131,9 @@ source/parse_env.ml:
(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.13 644))
(source/Makefile.lucky (lurette/b/41_Makefile.i 1.14 644))
(source/Makefile.gen_stubs (lurette/b/42_Makefile.g 1.5 644))
(source/Makefile.lurette_lib (lurette/c/2_Makefile.l 1.13 644))
(source/Makefile.lurette_lib (lurette/c/2_Makefile.l 1.14 644))
(source/Makefile (lurette/c/20_Makefile 1.10 644))
;; Documentation
......@@ -148,10 +151,10 @@ source/parse_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.28 644))
(test/time-ossau.res (lurette/b/49_time.res 1.31 644))
(test/time-ecrins.res (lurette/d/20_time-ecrin 1.5 644))
(test/time-ecrins.exp (lurette/d/21_time-ecrin 1.5 644))
(test/time-ossau.exp (lurette/b/48_time.exp 1.29 644))
(test/time-ossau.res (lurette/b/49_time.res 1.32 644))
(test/time-ecrins.res (lurette/d/20_time-ecrin 1.6 644))
(test/time-ecrins.exp (lurette/d/21_time-ecrin 1.6 644))
;; Various files used for testing purposes
(test/usager.luc (lurette/b/14_usager.env 1.9 644))
......@@ -172,7 +175,7 @@ source/parse_env.ml:
(test/heater_int.rif.exp (lurette/b/28_heater_int 1.10 644))
(test/ControleurPorte.rif.exp (lurette/b/29_Controleur 1.11 644))
(test/heater_float.rif.exp (lurette/b/30_heater_flo 1.11 644))
(test/heater_float.rif.exp (lurette/b/30_heater_flo 1.12 644))
(test/heater_int.lus (lurette/b/43_heater_int 1.1 644))
(test/heater_float.lus (lurette/b/44_heater_flo 1.2 644))
(test/test_gen_stubs.h (lurette/b/45_test_gen_s 1.1 644))
......@@ -238,7 +241,7 @@ source/parse_env.ml:
(mlcuddidl/Changes (lurette/d/10_Changes 1.1 644))
(TODO (lurette/d/22_TODO 1.3 644))
(TODO (lurette/d/22_TODO 1.4 644))
)
(Merge-Parents)
......
......@@ -47,6 +47,8 @@ SOURCES_OCAML = \
$(LURETTE_PATH)/source/parse_env.ml \
$(LURETTE_PATH)/source/polyhedron.mli \
$(LURETTE_PATH)/source/polyhedron.ml \
$(LURETTE_PATH)/source/draw.mli \
$(LURETTE_PATH)/source/draw.ml \
$(LURETTE_PATH)/source/store.mli \
$(LURETTE_PATH)/source/store.ml \
$(LURETTE_PATH)/source/env_state.mli \
......
......@@ -34,6 +34,7 @@ SOURCES = \
$(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/draw.mli $(LURETTE_PATH)/source/draw.ml \
$(LURETTE_PATH)/source/store.mli $(LURETTE_PATH)/source/store.ml \
$(LURETTE_PATH)/source/env_state.mli $(LURETTE_PATH)/source/env_state.ml \
$(LURETTE_PATH)/source/solver.mli $(LURETTE_PATH)/source/solver.ml \
......
......@@ -62,6 +62,7 @@ type var_name = string
type vn = var_name
type subst = (var_name * Value.t)
type num_subst = (var_name * Value.num)
type var_type = BoolT | IntT of int * int | FloatT of float * float
type vnt = var_name * var_type
......
......@@ -66,6 +66,7 @@ type vn = var_name
type subst = (var_name * Value.t)
type num_subst = (var_name * Value.num)
type var_type = BoolT | IntT of int * int | FloatT of float * float
type vnt = var_name * var_type
......
......@@ -59,7 +59,7 @@ val nexpr_add : (Value.num * string) -> t -> t
val apply_subst : t -> subst -> t
val apply_substl : subst list -> t -> t
(** This one does not multiply the result. *)
(** [apply_simple_subst ne (x, v)] substitutes [x] by [v] in [ne]. *)
val apply_simple_subst : t -> string * Value.num -> t
......
......@@ -65,37 +65,63 @@ let rec (power : int -> int -> int) =
if m = 0 then 1 else n * (power n (m-1))
let number_of_ending_zero str =
(* count the number of '0' at the end of str *)
let rec aux str i =
if
String.get str i = '0'
then
aux str (i-1)
else
i
in
let l = (String.length str) - 1 in
l - (aux str l)
(* Polka constraint parser only parses rationals *)
let (rat_of_float : float -> int * int) =
fun f ->
let c = -2 + (String.length (string_of_float (fst (modf (abs_float f))))) in
let d =
let sof = Util.my_string_of_float in
let (f_frac, f_integral) = modf (abs_float f) in
let f_frac_str = (sof f_frac) in
let c = (String.length f_frac_str) - 2 in
let f_integral_str = string_of_int (int_of_float f_integral) in
let exp =
if
(* What should be the precision ??? *)
c > 6
f_frac = 0.
then
power 10 6
else
power 10 c
0
else
c - (number_of_ending_zero f_frac_str)
in
let fd = f*. (float_of_int d)in
let n = int_of_float fd in
let new_f = (float_of_int n) /. (float_of_int d) in
if
((abs_float (f -. new_f)) > 0.001)
then
(
print_string
("*** Aborting...\n*** Fail to convert the float " ^
(string_of_float f) ^ " into a rational (with an error greater than " ^
(string_of_float (abs_float (f -. new_f))) ^ ")\n");
flush stdout;
assert false
);
let d = power 10 exp in
let n_str = (
(if f > 0. then "" else "-") ^
f_integral_str ^(String.sub (sof f_frac) 2 exp)
)
in
let n = int_of_string n_str in
let _ =
assert (
let new_f = (float_of_int n) /. (float_of_int d) in
if
((abs_float ((f -. new_f))) > 0.01)
then
(
print_string
("*** Aborting...\n*** Fail to convert the float " ^
(string_of_float f) ^
" into a rational (with an error greater than " ^
(string_of_float (abs_float (f -. new_f))) ^ ")\n");
flush stdout;
false
)
else
true
)
in
(n, d)
let _ = assert (rat_of_float 4.1 = (41, 10))
let _ = assert (rat_of_float 999.991863362 = (999991863, 1000000))
(* We need to translaste expressions into a string of the format used
......@@ -226,10 +252,10 @@ let (build_poly_list_from_delayed_cstr :
and ineq_max_str = (ineq_to_polka_string ineq_max)
in
let v1 =
print_string (" ==> " ^ ineq_min_str ^ "\n");
(* print_string (" ==> " ^ ineq_min_str ^ "\n"); *)
Vector.of_constraint (name_to_rank) dim ineq_min_str
and v2 =
print_string (" ==> " ^ ineq_max_str ^ "\n");
(* print_string (" ==> " ^ ineq_max_str ^ "\n"); *)
Vector.of_constraint (name_to_rank) dim ineq_max_str
in
(
......@@ -245,7 +271,7 @@ let (build_poly_list_from_delayed_cstr :
(fun poly ineq ->
(* add the constraint [ineq] to polyhedron [poly] *)
let ineq_str = ineq_to_polka_string ineq in
print_string (" ==> " ^ ineq_str ^ "\n");
(* print_string (" ==> " ^ ineq_str ^ "\n"); *)
Poly.add_constraint poly
(Vector.of_constraint (name_to_rank) dim ineq_str)
)
......
......@@ -851,7 +851,7 @@ and (draw_in_bdd_eq: Ne.t -> subst list * Store.t -> Bdd.t -> Bdd.t ->
(****************************************************************************)
(* exported *)
let (draw : vn list -> vnt list -> Bdd.t -> Bdd.t -> subst list * subst list) =
fun bool_vars_to_gen num_vnt_to_gen comb bdd ->
......@@ -859,7 +859,7 @@ let (draw : vn list -> vnt list -> Bdd.t -> Bdd.t -> subst list * subst list) =
let (bool_subst_l, store_range, store_poly) =
draw_in_bdd ([], (new_store num_vnt_to_gen)) bdd comb
in
let num_subst_l =
let num_subst_l0 =
if
num_vnt_to_gen = []
then
......@@ -867,11 +867,19 @@ let (draw : vn list -> vnt list -> Bdd.t -> Bdd.t -> subst list * subst list) =
else
match Env_state.draw_mode () with
Env_state.Verteces ->
rev_append (draw_verteces store_range) (draw_verteces store_poly)
| Env_state.Edges ->
rev_append (draw_edges store_range) (draw_edges store_poly)
| Env_state.Inside ->
rev_append (draw_inside store_range) (draw_inside store_poly)
let sl = (draw_verteces store_poly []) in
draw_verteces store_range sl
| Env_state.Edges ->
let sl = draw_edges store_poly [] in
draw_edges store_range sl
| Env_state.Inside ->
let sl = draw_inside store_poly [] in
draw_inside store_range sl
in
let num_subst_l =
List.map
(fun (vn, num) -> (vn, N num))
num_subst_l0
in
let subst_l = append bool_subst_l num_subst_l in
let (out_vars, _) = List.split (Env_state.output_var_names ())
......
......@@ -14,8 +14,9 @@ open Constraint
open Polyhedron
open Util
open List
open Draw
let debug_store = true
let debug_store = false
(* exported *)
exception No_numeric_solution
......@@ -187,16 +188,18 @@ let (switch_to_polyhedron_representation : t -> t * t) =
(store, {var = Poly []; substl = []; delay = [] })
else
let poly_l =
(* This functions removes from [store] variables that are
moved to the polyhedron store *)
Polyhedron.build_poly_list_from_delayed_cstr tbl store.delay
in
List.iter
(fun (_, poly, _) ->
if Poly.is_empty poly then
(
print_string "Empty polyhedron!!\n";
flush stdout;
raise No_numeric_solution
)
if Poly.is_empty poly then (
if debug_store then (
print_string "\n The polyhedron is empty .\n";
flush stdout );
raise No_numeric_solution
)
)
poly_l;
(store, {var = Poly poly_l; substl = []; delay = []})
......@@ -276,11 +279,11 @@ let (normalise : Constraint.ineq -> var_name * nac ) =
| (I(i), F(f)) ->
failwith ("*** Error: " ^ (string_of_int i)
^ "is an integer and "
^ " is an integer and "
^ (string_of_float f) ^ " is a float.\n")
| (F(f), I(i)) ->
failwith ("*** Error: " ^ (string_of_int i)
^ "is an integer and "
^ " is an integer and "
^ (string_of_float f) ^ " is a float.\n")
)
......@@ -371,11 +374,16 @@ let (make_subst : vn -> Value.num -> Ne.subst) =
(* exported *)
let rec (add_constraint : t -> Constraint.t -> t) =
fun store cstr0 ->
let cstr = Constraint.apply_substl store.substl cstr0 in
add_constraint_do store cstr
and (add_constraint_do : t -> Constraint.t -> t) =
fun store cstr ->
let _ =
if debug_store then (
(* print_string "\n***********************************************\n " ; *)
(* print_string (store_to_string store); *)
print_string "\n***********************************************\n " ;
print_string (to_string store);
print_string "\n**** add_constraint: " ;
print_string (Constraint.to_string cstr);
(* print_string "\n"; *)
......@@ -475,8 +483,11 @@ let rec (add_constraint : t -> Constraint.t -> t) =
let s = make_subst vn (I max) in
let (d_awake, d_delay) =
List.partition
(fun ineq -> Constraint.dimension_ineq ineq <= 1)
(List.map (Constraint.apply_subst_ineq s) d)
(fun ineq ->
Constraint.dimension_ineq ineq <= 1)
(List.map
(Constraint.apply_subst_ineq s)
d)
in
Hashtbl.remove tbl vn;
(s::sl, d_delay, d_awake)
......@@ -495,7 +506,7 @@ let rec (add_constraint : t -> Constraint.t -> t) =
print_string (Constraint.ineq_to_string cstr);
flush stdout
);
add_constraint acc (Ineq cstr))
add_constraint_do acc (Ineq cstr))
{ var=Range(tbl) ; substl=sl1 ; delay=d1 }
da
|
......@@ -516,8 +527,11 @@ let rec (add_constraint : t -> Constraint.t -> t) =
let s = make_subst vn (I min) in
let (d_awake, d_delay) =
List.partition
(fun ineq -> Constraint.dimension_ineq ineq <= 1)
(List.map (Constraint.apply_subst_ineq s) d)
(fun ineq ->
Constraint.dimension_ineq ineq <= 1)
(List.map
(Constraint.apply_subst_ineq s)
d)
in
Hashtbl.remove tbl vn;
(s::sl, d_delay, d_awake)
......@@ -536,7 +550,7 @@ let rec (add_constraint : t -> Constraint.t -> t) =
print_string (Constraint.ineq_to_string cstr);
flush stdout
);
add_constraint acc (Ineq cstr))
add_constraint_do acc (Ineq cstr))
{ var=Range(tbl) ; substl=sl1 ; delay=d1 }
da
......@@ -558,8 +572,11 @@ let rec (add_constraint : t -> Constraint.t -> t) =
let s = make_subst vn (F max) in
let (d_awake, d_delay) =
List.partition
(fun ineq -> Constraint.dimension_ineq ineq <= 1)
(List.map (Constraint.apply_subst_ineq s) d)
(fun ineq ->
Constraint.dimension_ineq ineq <= 1)
(List.map
(Constraint.apply_subst_ineq s)
d)
in
Hashtbl.remove tbl vn;
(s::sl, d_delay, d_awake)
......@@ -578,7 +595,7 @@ let rec (add_constraint : t -> Constraint.t -> t) =
print_string (Constraint.ineq_to_string cstr);
flush stdout
);
add_constraint acc (Ineq cstr))
add_constraint_do acc (Ineq cstr))
{ var=Range(tbl) ; substl=sl1 ; delay=d1 }
da
......@@ -600,8 +617,11 @@ let rec (add_constraint : t -> Constraint.t -> t) =
let s = make_subst vn (F min) in
let (d_awake, d_delay) =
List.partition
(fun ineq -> Constraint.dimension_ineq ineq <= 1)
(List.map (Constraint.apply_subst_ineq s) d)
(fun ineq ->
Constraint.dimension_ineq ineq <= 1)
(List.map
(Constraint.apply_subst_ineq s)
d)
in
Hashtbl.remove tbl vn;
(s::sl, d_delay, d_awake)
......@@ -620,7 +640,7 @@ let rec (add_constraint : t -> Constraint.t -> t) =
print_string (Constraint.ineq_to_string cstr);
flush stdout
);
add_constraint acc (Ineq cstr))
add_constraint_do acc (Ineq cstr))
{ var=Range(tbl) ; substl=sl1 ; delay=d1 }
da
......@@ -641,8 +661,11 @@ let rec (add_constraint : t -> Constraint.t -> t) =
let s = make_subst vn (F max) in
let (d_awake, d_delay) =
List.partition
(fun ineq -> Constraint.dimension_ineq ineq <= 1)
(List.map (Constraint.apply_subst_ineq s) d)
(fun ineq ->
Constraint.dimension_ineq ineq <= 1)
(List.map
(Constraint.apply_subst_ineq s)
d)
in
Hashtbl.remove tbl vn;
(s::sl, d_delay, d_awake)
......@@ -661,7 +684,7 @@ let rec (add_constraint : t -> Constraint.t -> t) =
print_string (Constraint.ineq_to_string cstr);
flush stdout
);
add_constraint acc (Ineq cstr))
add_constraint_do acc (Ineq cstr))
{ var=Range(tbl) ; substl=sl1 ; delay=d1 }
da
......@@ -683,8 +706,11 @@ let rec (add_constraint : t -> Constraint.t -> t) =
let s = make_subst vn (F min) in
let (d_awake, d_delay) =
List.partition
(fun ineq -> Constraint.dimension_ineq ineq <= 1)
(List.map (Constraint.apply_subst_ineq s) d)
(fun ineq ->
Constraint.dimension_ineq ineq <= 1)
(List.map
(Constraint.apply_subst_ineq s)
d)
in
Hashtbl.remove tbl vn;
(s::sl, d_delay, d_awake)
......@@ -703,7 +729,7 @@ let rec (add_constraint : t -> Constraint.t -> t) =
print_string (Constraint.ineq_to_string cstr);
flush stdout
);