Commit c9f9ddd4 authored by Erwan Jahier's avatar Erwan Jahier

lurette 1.46 Wed, 15 Apr 2009 11:14:47 +0200 by jahier

Parent-Version:      1.45
Version-Log:

Use polkag instead of polkai to build the binaries, as the latter raises
some seg fault when its capacity is exceded.
Project-Description: Lurette
parent 89aedffe
......@@ -13,7 +13,7 @@
(install/pixmaps/gnuplot.bmp 822 1137765987 n/2_gnuplot.bm 1.1)
(examples/xlurette/Sildex/oracle_sildex.c 11793 1138025047 o/28_oracle_sil 1.1)
(examples/lucky/other/structured_type.luc 2289 1137765987 k/50_structured 1.1)
(examples/luckyDraw/ocaml/draw-ex.out 472 1196700198 l/6_draw-ex.ou 1.4)
(examples/luckyDraw/ocaml/draw-ex.out 472 1239786887 l/6_draw-ex.ou 1.5)
(xlurette/Scade/GenMake_l4sim.tcl 21042 1165588586 j/16_GenMake_l4 1.2.1.1)
(examples/lucky/tut-solution/Makefile 315 1137765987 k/17_Makefile 1.1)
(examples/xlurette/Sildex/oracle_sildex.h 1516 1138025047 o/26_oracle_sil 1.1)
......@@ -38,7 +38,7 @@
(xlurette/Scade/rif.ini 2117 1122044801 j/11_rif.ini 1.1)
(polka/C/internal.h 916 1071844798 e/0_internal.h 1.2)
(examples/xlurette/tram/time-joly.res 25174 1138025047 o/12_time-joly. 1.1)
(examples/xlurette/fault-tolerant-heater/test.rif.exp 35339 1138025047 n/48_test.rif.e 1.1)
(examples/xlurette/fault-tolerant-heater/test.rif.exp 35327 1239786887 n/48_test.rif.e 1.2)
(polka/C/cherni.h 2458 1071844798 e/1_cherni.h 1.2)
(source/fair_bddd.ml 22221 1137765987 g/38_fair_bddd. 1.12)
(examples/ocaml/crazy-rabbit/obstacle.luc 449 1137765987 j/44_obstacle.l 1.1)
......@@ -290,7 +290,7 @@
(examples/lucky/other/test2.rif.exp 400 1137765987 k/38_test2.rif. 1.1)
(source/formula_to_bdd.ml 22535 1222100401 g/34_formula_to 1.14)
(source/Makefile.lurette_ocaml_lib 2978 1137765987 j/1_Makefile.l 1.2)
(examples/ocaml/crazy-rabbit/rabbit.ml 8853 1196700198 k/4_rabbit.ml 1.3)
(examples/ocaml/crazy-rabbit/rabbit.ml 8854 1239786887 k/4_rabbit.ml 1.4)
(doc/figs/heater_sensors.fig 2392 1138034376 r/4_heater_sen 1.1)
(examples/ocaml/crazy-rabbit/rabbit.out.exp 31899 1137765987 j/50_rabbit.out 1.1)
(examples/xlurette/Gyro/onlyroll.batch 381 1137765987 m/32_onlyroll.b 1.1)
......@@ -308,9 +308,9 @@
(GBDDML/Makefile 3166 1172658530 r/30_Makefile 1.2)
(examples/rml/window.out.exp 2210 1137765987 k/6_window.out 1.1)
(examples/xlurette/heater/test1.res 0 1137765987 m/22_test1.res 1.1)
(source/version.ml 15 1222100401 n/43_version.ml 1.12)
(source/version.ml 15 1239786887 n/43_version.ml 1.13)
(examples/xlurette/Scade-win32/Pilot.ewo 785 1137765987 l/28_Pilot.ewo 1.1)
(RELEASE-NOTES 3896 1222100401 h/45_RELEASE-NO 1.7.1.2)
(RELEASE-NOTES 4038 1239786887 h/45_RELEASE-NO 1.7.1.3)
(examples/lucky/C/test.res 0 1149596800 r/18_test.res 1.1)
(source/Ezdl_c.c 10643 1127735479 j/19_Ezdl_c.c 1.1)
(examples/xlurette/Scade-sparc/config_types.h 85 1137765987 l/11_config_typ 1.1)
......@@ -329,7 +329,7 @@
(source/gen_stubs_sildex.ml 9755 1122044801 h/38_gen_stubs_ 1.5)
(source/gen_stubs_scade.mli 793 1122044801 f/6_gen_stubs_ 1.4)
(source/luc4c.mli 3003 1149596800 r/15_luc4c.mli 1.1)
(source/Makefile 22009 1222100401 c/20_Makefile 1.54)
(source/Makefile 22009 1239786887 c/20_Makefile 1.55)
(examples/xlurette/Scade-win32/Pilot.vsw 431 1137765987 l/44_Pilot.vsw 1.1)
(examples/xlurette/Scade-win32/MyConsts.saofd 153 1137765987 l/48_MyConsts.s 1.1)
(examples/xlurette/Scade-win32/Direction_D1.saofd 1298 1137765987 m/3_Direction_ 1.1)
......@@ -345,7 +345,7 @@
(install/pixmaps/build.xpm 7000 1137765987 n/5_build.xpm 1.1)
(source/Ezdl.ml 1574 1127735479 j/17_Ezdl.ml 1.1)
(doc/tutorial/macros.tex 5209 1138032075 q/28_macros.tex 1.1)
(examples/luckyDraw/ocaml/draw-ex.out.exp 472 1165477648 l/5_draw-ex.ou 1.2)
(examples/luckyDraw/ocaml/draw-ex.out.exp 472 1239786887 l/5_draw-ex.ou 1.3)
(source/lustreExp.mli 2340 1222100401 g/46_lustreExp. 1.13)
(utils/luckytolatex 1517 1196700198 n/30_luckytolat 1.2)
(install/pixmaps/open.xpm 782 1137765987 n/20_open.xpm 1.1)
......@@ -355,8 +355,8 @@
(source/rif.ml 7464 1122044801 h/27_rif.ml 1.4)
(doc/tutorial/simple.tex 267 1138032075 q/26_simple.tex 1.1)
(examples/xlurette/tram/Makefile 1311 1196700198 o/19_Makefile 1.1.1.4)
(examples/xlurette/fault-tolerant-heater/Makefile 864 1196700198 n/47_Makefile 1.1.1.3)
(source/Makefile.release 14289 1222100401 n/41_Makefile.r 1.12)
(examples/xlurette/fault-tolerant-heater/Makefile 864 1239786887 n/47_Makefile 1.1.1.4)
(source/Makefile.release 14348 1239786887 n/41_Makefile.r 1.13)
(source/socket_client_serveur.ml 1844 1122044801 i/42_socket_cli 1.1)
(xlurette/Scade/LuretteTcl.c 752 1122044801 j/15_LuretteTcl 1.1)
(source/Makefile.lutinlib 1691 1138025047 n/44_Makefile.l 1.1)
......@@ -415,7 +415,7 @@
(examples/lucky/other/test1.rif.exp 33449 1137765987 k/41_test1.rif. 1.1)
(polka/Makefile.config 2427 1196700198 e/20_Makefile.c 1.10.1.2)
(examples/xlurette/Scade-sparc/exo1.vsw 400 1137765987 l/16_exo1.vsw 1.1)
(examples/xlurette/fault-tolerant-heater/degradable-sensors.luc 1383 1222100401 h/15_wearing-se 1.4)
(examples/xlurette/fault-tolerant-heater/degradable-sensors.luc 1384 1239786887 h/15_wearing-se 1.5)
(examples/lucky/external_code/Makefile 1677 1196700198 j/24_Makefile 1.5)
(examples/xlurette/Scade-sparc/libpwlinear.saofdm 1379 1137765987 l/12_libpwlinea 1.1)
(examples/xlurette/Scade-sparc/Direction_D1/Direction_D1.c 935 1137765987 l/25_Direction_ 1.1)
......@@ -465,7 +465,7 @@
(source/ocaml2c.idl 1569 1083336219 e/26_ocaml2c.id 1.3)
(install/pixmaps/lugenlu.bmp 822 1137765987 n/1_lugenlu.bm 1.1)
(source/gen_fake_lucky.ml 11873 1169542477 g/8_gen_fake_l 1.15)
(source/ne.ml 13862 1222100401 c/21_ne.ml 1.16)
(source/ne.ml 12958 1239786887 c/21_ne.ml 1.17)
(examples/xlurette/Scade-win32/Makefile 521 1137765987 l/27_Makefile 1.1)
(install/pixmaps/lurette.jpg 5356 1137765987 n/8_lurette.jp 1.1)
(examples/xlurette/tram/controleur_env.luc 433 1138025047 o/20_controleur 1.1)
......@@ -516,7 +516,7 @@
(polka/caml/vector.idl 10381 1076684617 d/35_vector.idl 1.4)
(install/pixmaps/config-params2.xpm 1376 1137765987 n/10_config-par 1.1)
(polka/caml/poly.idl 10352 1076684617 d/33_poly.idl 1.3)
(source/polyhedron.ml 15752 1222100401 d/25_polyhedron 1.22)
(source/polyhedron.ml 16278 1239786887 d/25_polyhedron 1.23)
(test/time-CHAILLOL.exp 8235 1063029729 g/10_time-CHAIL 1.1)
(examples/rml/window.out 2210 1137765987 k/7_window.out 1.1)
(examples/Makefile 909 1196700198 j/38_Makefile 1.7)
......@@ -542,7 +542,7 @@
(doc/figs/obj-code-gen.fig.bak 1635 1138034376 q/39_obj-code-g 1.1)
(examples/xlurette/tram/tramway.lus 4985 1138025047 o/14_tramway.lu 1.1)
(source/luckyCapi.ml 665 1137765987 n/40_luckyCapi. 1.1)
(VERSION 70 1222100401 j/25_VERSION 1.2.1.4)
(VERSION 70 1239786887 j/25_VERSION 1.2.1.5)
(source/Makefile.luckyDraw 4827 1172658530 j/6_Makefile.l 1.5)
(source/sim2chro.mli 1532 1078751438 b/23_sim2chro.m 1.12)
(examples/lucky/other/losange-3d2.luc 355 1137765987 k/44_losange-3d 1.1)
......
V1.46 (22/09/2009)
* Use polkag instead of polkai to build the binaries, as the latter raises
some seg fault when its capacity is exceded.
V1.45 (22/09/2008)
* Fix an embarassing bug in the integer solver (in dimension 1).
......
VERSION_DATE=26-02-08
VERSION=1.44
VERSION_DATE=15-04-09
VERSION=1.45
export VERSION
export VERSION_DATE
......@@ -20,8 +20,8 @@ x=16.9628921217
x=16.6986337542
x=10.01
x=10.01
Z=9411 z=-60 y=50 x=60
Z=6254 z=99 y=99 x=-148
Z=-10000 y=99 z=99 x=-148
Z=-10000 y=99 z=99 x=-148
Z=9411 y=-60 x=50 z=60
Z=6254 y=99 x=99 z=-148
Z=-10000 x=99 y=99 z=-148
Z=-10000 x=99 y=99 z=-148
Z=t y=f x=f
......@@ -20,8 +20,8 @@ x=16.9628921217
x=16.6986337542
x=10.01
x=10.01
Z=9411 z=-60 y=50 x=60
Z=6254 z=99 y=99 x=-148
Z=-10000 y=99 z=99 x=-148
Z=-10000 y=99 z=99 x=-148
Z=9411 y=-60 x=50 z=60
Z=6254 y=99 x=99 z=-148
Z=-10000 x=99 y=99 z=-148
Z=-10000 x=99 y=99 z=-148
Z=t y=f x=f
(*
Demonstrate the use of Lucky from Ocaml.
......
......@@ -5,7 +5,7 @@ LURETTETOP=$(LTOP) -go --precision 2 --sut heater_control.lus \
--main-oracle-node not_a_sauna --sut-compiler verimag \
--oracle-compiler verimag --test-length 500 --thick-draw 1 \
--draw-inside 0 --draw-edges 0 --draw-vertices 0 --draw-all-vertices \
--step-mode Inside --local-var --no-sim2chro --seed 1 \
--step-mode Inside --local-var --no-sim2chro --seed 3 \
--do-not-show-step
......
......@@ -35,6 +35,7 @@ transitions {
-- 3 sensors are working properly
t1 -> s1 ~cond invariant and new_T1 and new_T2 and new_T3 ;
s1 -> t1 ~weight 1000 ;
s1 -> t2 ~weight pre cpt;
-- One sensor is broken
......
;; -*- Prcs -*-
(Created-By-Prcs-Version 1 3 3)
(Project-Description "Lurette")
(Project-Version lurette 1 45)
(Parent-Version lurette 1 44)
(Project-Version lurette 1 46)
(Parent-Version lurette 1 45)
(Version-Log "
Fix an embarassing bug in the integer solver (in dimension 1).
")
Use polkag instead of polkai to build the binaries, as the latter raises
some seg fault when its capacity is exceded.")
(New-Version-Log ""
)
(Checkin-Time "Mon, 22 Sep 2008 18:20:01 +0200")
(Checkin-Time "Wed, 15 Apr 2009 11:14:47 +0200")
(Checkin-Login jahier)
(Populate-Ignore ())
(Project-Keywords)
......@@ -53,7 +52,7 @@ Fix an embarassing bug in the integer solver (in dimension 1).
(source/solver.mli (lurette/38_solver.mli 1.25 644))
(source/solver.ml (lurette/39_solver.ml 1.68 644))
(source/polyhedron.ml (lurette/d/25_polyhedron 1.22 644))
(source/polyhedron.ml (lurette/d/25_polyhedron 1.23 644))
(source/polyhedron.mli (lurette/d/26_polyhedron 1.11 644))
(source/store.mli (lurette/b/26_rnumsolver 1.27 644))
......@@ -101,7 +100,7 @@ Fix an embarassing bug in the integer solver (in dimension 1).
(source/constraint.mli (lurette/c/18_constraint 1.11 644))
(source/constraint.ml (lurette/c/19_constraint 1.14 644))
(source/ne.ml (lurette/c/21_ne.ml 1.16 644))
(source/ne.ml (lurette/c/21_ne.ml 1.17 644))
(source/ne.mli (lurette/c/22_ne.mli 1.12 644))
(source/value.ml (lurette/c/23_value.ml 1.10 644))
......@@ -136,7 +135,7 @@ Fix an embarassing bug in the integer solver (in dimension 1).
(source/Makefile.lucky (lurette/b/41_Makefile.i 1.39.1.4 644))
(source/Makefile.gen_stubs (lurette/b/42_Makefile.g 1.15.1.1 644))
(source/Makefile.lurette_lib (lurette/c/2_Makefile.l 1.37 644))
(source/Makefile (lurette/c/20_Makefile 1.54 644))
(source/Makefile (lurette/c/20_Makefile 1.55 644))
;; Documentation
(doc/Interface_draft (lurette/19_Interface_ 1.1 644))
......@@ -300,7 +299,7 @@ Fix an embarassing bug in the integer solver (in dimension 1).
;; Files added by populate at Wed, 04 Feb 2004 17:09:41 +0100,
;; to version 1.19(w), by jahier:
(examples/xlurette/fault-tolerant-heater/degradable-sensors.luc (lurette/h/15_wearing-se 1.4 644))
(examples/xlurette/fault-tolerant-heater/degradable-sensors.luc (lurette/h/15_wearing-se 1.5 644))
(examples/xlurette/fault-tolerant-heater/heater_control_env.luc (lurette/h/16_heater_con 1.4 644))
(examples/xlurette/fault-tolerant-heater/heater_control.lus (lurette/h/17_heater_con 1.4.1.1 644))
(examples/xlurette/fault-tolerant-heater/sensors.luc (lurette/h/18_sensors.lu 1.4 644))
......@@ -388,7 +387,7 @@ Fix an embarassing bug in the integer solver (in dimension 1).
;; Files added by populate at Tue, 27 Jul 2004 12:24:20 +0200,
;; to version 1.35(w), by jahier:
(RELEASE-NOTES (lurette/h/45_RELEASE-NO 1.7.1.2 644))
(RELEASE-NOTES (lurette/h/45_RELEASE-NO 1.7.1.3 644))
;; Files added by populate at Wed, 06 Oct 2004 11:46:42 +0200,
;; to version 1.37(w), by jahier:
......@@ -493,7 +492,7 @@ Fix an embarassing bug in the integer solver (in dimension 1).
;; Files added by populate at Fri, 16 Sep 2005 14:49:05 +0200,
;; to version 1.40(w), by jahier:
(VERSION (lurette/j/25_VERSION 1.2.1.4 644))
(VERSION (lurette/j/25_VERSION 1.2.1.5 644))
;; Files added by populate at Fri, 16 Sep 2005 14:50:55 +0200,
......@@ -543,7 +542,7 @@ Fix an embarassing bug in the integer solver (in dimension 1).
(examples/ocaml/crazy-rabbit/rabbit-speed.luc (lurette/k/1_rabbit-spe 1.1 644))
(examples/ocaml/crazy-rabbit/test.res (lurette/k/2_test.res 1.1 644))
(examples/ocaml/crazy-rabbit/Makefile (lurette/k/3_Makefile 1.4 644))
(examples/ocaml/crazy-rabbit/rabbit.ml (lurette/k/4_rabbit.ml 1.3 644))
(examples/ocaml/crazy-rabbit/rabbit.ml (lurette/k/4_rabbit.ml 1.4 644))
(examples/ocaml/crazy-rabbit/up_and_down_macro (lurette/k/5_up_and_dow 1.1 644))
(examples/bin (../i386-linux-gcc3/bin) :symlink)
(examples/rml/window.out.exp (lurette/k/6_window.out 1.1 644))
......@@ -590,8 +589,8 @@ Fix an embarassing bug in the integer solver (in dimension 1).
(examples/luckyDraw/c/essai.c (lurette/l/2_essai.c 1.2 640))
(examples/luckyDraw/c/Makefile (lurette/l/4_Makefile 1.7 640))
(examples/luckyDraw/ocaml/draw-ex.out.exp (lurette/l/5_draw-ex.ou 1.2 644))
(examples/luckyDraw/ocaml/draw-ex.out (lurette/l/6_draw-ex.ou 1.4 644))
(examples/luckyDraw/ocaml/draw-ex.out.exp (lurette/l/5_draw-ex.ou 1.3 644))
(examples/luckyDraw/ocaml/draw-ex.out (lurette/l/6_draw-ex.ou 1.5 644))
(examples/luckyDraw/ocaml/test.res (lurette/l/7_test.res 1.1 644))
(examples/luckyDraw/ocaml/draw-ex.ml (lurette/l/8_draw-ex.ml 1.2 644))
(examples/luckyDraw/ocaml/Makefile (lurette/l/9_Makefile 1.4 644))
......@@ -738,16 +737,16 @@ Fix an embarassing bug in the integer solver (in dimension 1).
(source/luckyCapi_stubs.c (lurette/n/38_luckyCapi_ 1.1 644))
(source/luckyCapi.idl (lurette/n/39_luckyCapi. 1.1 644))
(source/luckyCapi.ml (lurette/n/40_luckyCapi. 1.1 644))
(source/Makefile.release (lurette/n/41_Makefile.r 1.12 644))
(source/Makefile.release (lurette/n/41_Makefile.r 1.13 644))
(source/version.ml (lurette/n/43_version.ml 1.12 644))
(source/version.ml (lurette/n/43_version.ml 1.13 644))
(source/Makefile.lutinlib (lurette/n/44_Makefile.l 1.1 644))
(source/Makefile.luc2c (lurette/n/45_Makefile.l 1.3 644))
(source/luc2c.ml (lurette/n/46_luc2c.ml 1.7 644))
(examples/xlurette/fault-tolerant-heater/Makefile (lurette/n/47_Makefile 1.1.1.3 644))
(examples/xlurette/fault-tolerant-heater/test.rif.exp (lurette/n/48_test.rif.e 1.1 644))
(examples/xlurette/fault-tolerant-heater/Makefile (lurette/n/47_Makefile 1.1.1.4 644))
(examples/xlurette/fault-tolerant-heater/test.rif.exp (lurette/n/48_test.rif.e 1.2 644))
(examples/xlurette/tram/test2.rif.exp (lurette/n/51_test2.rif. 1.1 644))
(examples/xlurette/tram/test1.rif.exp (lurette/o/0_test1.rif. 1.1 644))
......
......@@ -31,9 +31,9 @@ liblucky_nc.a:
ar r liblucky_nc.a *.o && rm -rf *.o &&\
ar x $(LURETTE_PATH)/$(HOST_TYPE)/lib/libbdd_stubs.a &&\
ar r liblucky_nc.a *.o && rm -rf *.o &&\
ar x $(LURETTE_PATH)/$(HOST_TYPE)/lib/libpolkai_caml.a &&\
ar x $(LURETTE_PATH)/$(HOST_TYPE)/lib/libpolkag_caml.a &&\
ar r liblucky_nc.a *.o && rm *.o &&\
ar x $(LURETTE_PATH)/$(HOST_TYPE)/lib/libpolkai.a &&\
ar x $(LURETTE_PATH)/$(HOST_TYPE)/lib/libpolkag.a &&\
ar r liblucky_nc.a *.o && rm *.o &&\
ar x $(OCAMLLIB)/libcamlidl.a &&\
ar r liblucky_nc.a *.o && rm *.o &&\
......
......@@ -316,6 +316,7 @@ rel: lurette-rel lucky-rel draw-rel luc4ocaml-rel
\
cd /tmp && tar cvfz $(ALL_RELEASE_NAME).tgz $(ALL_RELEASE_NAME)
cp /tmp/$(ALL_RELEASE_NAME).tgz $(SYNCHRONE_DIR)/lurette/
cp $(LURETTE_PATH)/RELEASE-NOTES $(SYNCHRONE_DIR)/lurette
test-rel:
cp $(SYNCHRONE_DIR)/lurette/$(ALL_RELEASE_NAME).tgz /tmp && \
......
......@@ -345,26 +345,8 @@ let split_res_to_string = function
(* exported *)
let (split_old : t -> split_res) =
fun ne ->
let f = fun var num_val acc ->
match acc with
None, ne ->
if var = "" then
None, StringMap.add var num_val ne
else
Some(var, num_val), ne
| Some(v, nv), ne -> Some(v, nv), (StringMap.add var num_val ne)
in (
match StringMap.fold f ne (None, StringMap.empty) with
| None,_ -> No_solution
| Some(v,c), ne -> Split(v,c,ne)
)
let (split : t -> split_res) =
fun ne ->
(* let res2 = split2 ne in *)
let list_to_ne =
List.fold_left (fun acc (c,v) -> StringMap.add v c acc) StringMap.empty
in
......@@ -373,12 +355,12 @@ let (split : t -> split_res) =
| I i1, I i2 -> (i2/i1)*i1 = i2
| _ ,_ -> true
in
let cl = List.rev (StringMap.fold (fun v c acc -> (c,v)::acc) ne []) in
let cl = (StringMap.fold (fun v c acc -> (c,v)::acc) ne []) in
let res =
match cl with
| []
| [_,_] ->
print_string "The impossible occured!\n"; flush stdout;
print_string "The impossible occured!\n"; flush stdout;
assert false (* dim > 0 *)
| (F f_cst,"")::(F f, v)::rest
| (F f, v)::(F f_cst,"")::rest
......@@ -413,16 +395,6 @@ let (split : t -> split_res) =
Not_found -> Dont_know
)
in
(* if res <> res2 then ( *)
(* print_string ("Split : result differs on "^(to_string ne)^ ": \n" ^ *)
(* (split_res_to_string res) ^ *)
(* " <> \n" ^ *)
(* (split_res_to_string res2) ^ *)
(* "\n"); *)
(* flush stdout; *)
(* assert false *)
(* ) *)
(* else *)
res
(* exported *)
......
......@@ -201,19 +201,19 @@ let (range_to_string : range -> string) =
let already_initialized = ref false
let polka_init = ref 100
let poly_cache_tbl = Hashtbl.create 1
let polka_dim = ref 0
let rec (build_poly_list_from_delayed_cstr : int -> range Util.StringMap.t ->
Constraint.ineq list ->
range Util.StringMap.t *
Var.name list *
(Var.vnt list * Poly.t * (int -> string) * Constraint.ineq list) list ) =
Constraint.ineq list ->
range Util.StringMap.t *
Var.name list *
(Var.vnt list * Poly.t * (int -> string) * Constraint.ineq list) list ) =
fun verb tbl delayed ->
try
Hashtbl.find poly_cache_tbl (tbl, delayed)
with Not_found ->
(* print_string "\n-------------------\n"; *)
(* flush stdout; *)
(* print_string "\n-------------------\n"; *)
(* flush stdout; *)
try
let cll = partition_constraint (List.map (fun c -> [c]) delayed) in
let all_vars = get_vars_cl delayed in
......@@ -225,14 +225,22 @@ let rec (build_poly_list_from_delayed_cstr : int -> range Util.StringMap.t ->
)
0
cll
in
in
let res =
if max_dim+3 > !polka_dim then (
polka_dim := max_dim+3;
already_initialized := false
);
if Util.hashtbl_size poly_cache_tbl > 100 then
(* Do not let that table explode...*)
Hashtbl.clear poly_cache_tbl;
if !already_initialized then () else
(
Polka.initialize true (max_dim+3) !polka_init;
(* print_string ("# Polka.initialize "^ *)
(* (string_of_int !polka_dim) ^ " " ^ *)
(* (string_of_int !polka_init) ^"\n"); *)
(* flush stdout; *)
Polka.initialize true !polka_dim !polka_init;
already_initialized := true
);
List.map
......@@ -258,8 +266,8 @@ let rec (build_poly_list_from_delayed_cstr : int -> range Util.StringMap.t ->
StringSet.fold
(fun var (vntl, poly, cl_init)->
(*
Add the constraint present in tbl to the polyhedron
for each variables in [vars_of_cl]
Add the constraint present in tbl to the polyhedron
for each variables in [vars_of_cl]
*)
let (ineq_min, ineq_max, vnt) =
match (StringMap.find var tbl) with
......@@ -292,12 +300,12 @@ let rec (build_poly_list_from_delayed_cstr : int -> range Util.StringMap.t ->
and ineq_max_str = (ineq_to_polka_string ineq_max)
in
let v1 =
(* print_string (" ==> " ^ ineq_min_str ^ "\n"); *)
(* flush stdout; *)
(* print_string (" ==> " ^ ineq_min_str ^ "\n"); *)
(* flush stdout; *)
Vector.of_constraint (name_to_rank) dim ineq_min_str
and v2 =
(* print_string (" ==> " ^ ineq_max_str ^ "\n"); *)
(* flush stdout; *)
(* print_string (" ==> " ^ ineq_max_str ^ "\n"); *)
(* flush stdout; *)
Vector.of_constraint (name_to_rank) dim ineq_max_str
in
(
......@@ -346,9 +354,9 @@ let rec (build_poly_list_from_delayed_cstr : int -> range Util.StringMap.t ->
if verb >= 2 then (
print_string (
"\n*** " ^
(string_of_int (List.length res)) ^
" polyhedra was/were used. " ^
"Variables are grouped as follows: \n");
(string_of_int (List.length res)) ^
" polyhedra was/were used. " ^
"Variables are grouped as follows: \n");
List.iter
(fun (vntl, _, _, cl) ->
print_string " ==> ";
......@@ -364,7 +372,7 @@ let rec (build_poly_list_from_delayed_cstr : int -> range Util.StringMap.t ->
flush stdout;
);
(tbl2, all_vars_list, res)
with
Failure "int_of_string" ->
assert false
......
let str="1.44"
let str="1.45"
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment