Commit a13cc8e1 authored by Erwan Jahier's avatar Erwan Jahier

lurette 0.123 Tue, 18 Feb 2003 09:49:47 +0100 by jahier

Parent-Version:      0.122
Version-Log:

source/rnumsolver.mli:
source/rnumsolver.ml:
source/store.mli:
source/store.ml:
   Rename rnumsolver into store.

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) !

Project-Description: Lurette
parent 78f40b65
......@@ -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 2806 1037192189 44_formula.ml 1.19)
(source/formula.mli 2771 1045558187 44_formula.ml 1.20)
(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 1045489850 b/49_time.res 1.30)
(test/time-ossau.res 6399 1045558187 b/49_time.res 1.31)
(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,8 +22,9 @@
(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/prevar.ml 981 1037192189 d/18_prevar.ml 1.1)
(test/time-ecrins.exp 6406 1045489850 d/21_time-ecrin 1.4)
(test/time-ecrins.exp 6406 1045558187 d/21_time-ecrin 1.5)
(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)
......@@ -43,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 1045489850 b/48_time.exp 1.27)
(source/print.mli 1145 1033397911 46_print.mli 1.12)
(test/time-ossau.exp 6399 1045558187 b/48_time.exp 1.28)
(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 31323 1045489850 41_parse_env. 1.35)
(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 30666 1045489850 39_solver.ml 1.40)
(source/solver.ml 29712 1045558187 39_solver.ml 1.41)
(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)
(source/Makefile 1627 1044958837 c/20_Makefile 1.10)
(source/util.ml 20845 1044958837 35_util.ml 1.37)
(source/util.ml 20844 1045558187 35_util.ml 1.38)
(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 2483 1045489850 b/41_Makefile.i 1.12)
(source/Makefile.lucky 2473 1045558187 b/41_Makefile.i 1.13)
(TAGS 9825 1007379917 21_TAGS 1.6)
(mlcuddidl/rdd.ml 8746 1034006019 c/41_rdd.ml 1.1)
(source/Makefile.lurette_lib 1966 1045489850 c/2_Makefile.l 1.12)
(source/Makefile.lurette_lib 1956 1045558187 c/2_Makefile.l 1.13)
(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)
(OcamlMakefile 22765 1045558187 17_OcamlMakef 1.47)
(source/polyhedron.ml 6983 1045558187 d/25_polyhedron 1.2)
(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)
......@@ -86,15 +87,16 @@
(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 21354 1045489850 51_env_state. 1.35)
(source/env_state.ml 21336 1045558187 51_env_state. 1.36)
(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 1045489850 c/14_myrules 1.23)
(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/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)
......@@ -120,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 5977 1037625990 45_formula.ml 1.24)
(source/formula.ml 5869 1045558187 45_formula.ml 1.25)
(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)
......@@ -133,9 +135,8 @@
(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 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)
(source/print.ml 5787 1045558187 47_print.ml 1.22)
(test/ControleurPorte.h 2306 1012914629 b/18_Controleur 1.1)
(configure.in 5208 1034351455 d/11_configure. 1.1)
(cuddaux/cuddauxBridge.c 6099 1034006019 c/31_cuddauxBri 1.1)
......@@ -143,13 +144,12 @@
(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 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 2364 1045489850 c/23_value.ml 1.2)
(test/giro/allocator.lus 1087 1031732392 c/5_allocator. 1.1)
(test/time-ecrins.res 6406 1045489850 d/20_time-ecrin 1.4)
(test/time-ecrins.res 6406 1045558187 d/20_time-ecrin 1.5)
(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)
......@@ -5,7 +5,7 @@
# For updates see:
# http://www.oefai.at/~markus/ocaml_sources
#
# $Id: OcamlMakefile 1.46 Wed, 13 Nov 2002 13:56:29 +0100 jahier $
# $Id: OcamlMakefile 1.47 Tue, 18 Feb 2003 09:49:47 +0100 jahier $
#
###########################################################################
......@@ -27,7 +27,8 @@ SOURCES_LURETTE_LIB = \
$(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/env_state.mli $(LURETTE_PATH)/source/env_state.ml \
$(LURETTE_PATH)/source/rnumsolver.mli $(LURETTE_PATH)/source/rnumsolver.ml \
$(LURETTE_PATH)/source/polyhedron.mli $(LURETTE_PATH)/source/polyhedron.ml \
$(LURETTE_PATH)/source/store.mli $(LURETTE_PATH)/source/store.ml \
$(LURETTE_PATH)/source/solver.mli $(LURETTE_PATH)/source/solver.ml \
$(LURETTE_PATH)/source/show_env.mli $(LURETTE_PATH)/source/show_env.ml \
$(LURETTE_PATH)/source/automata.mli $(LURETTE_PATH)/source/automata.ml \
......
;; -*- Prcs -*-
(Created-By-Prcs-Version 1 3 3)
(Project-Description "Lurette")
(Project-Version lurette 0 122)
(Parent-Version lurette 0 121)
(Project-Version lurette 0 123)
(Parent-Version lurette 0 122)
(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/store.mli:
source/store.ml:
Rename rnumsolver into store.
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.
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) !
")
(New-Version-Log ""
)
(Checkin-Time "Mon, 17 Feb 2003 14:50:50 +0100")
(Checkin-Time "Tue, 18 Feb 2003 09:49:47 +0100")
(Checkin-Login jahier)
(Populate-Ignore ())
(Project-Keywords)
......@@ -87,37 +51,37 @@ source/ne.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.37 444))
(source/util.ml (lurette/35_util.ml 1.38 444))
(source/solver.mli (lurette/38_solver.mli 1.13 644))
(source/solver.ml (lurette/39_solver.ml 1.40 644))
(source/solver.ml (lurette/39_solver.ml 1.41 644))
(source/polyhedron.ml (lurette/d/25_polyhedron 1.1 644))
(source/polyhedron.ml (lurette/d/25_polyhedron 1.2 644))
(source/polyhedron.mli (lurette/d/26_polyhedron 1.1 644))
(source/rnumsolver.mli (lurette/b/26_rnumsolver 1.12 644))
(source/rnumsolver.ml (lurette/b/27_rnumsolver 1.19 644))
(source/store.mli (lurette/b/26_rnumsolver 1.13 644))
(source/store.ml (lurette/b/27_rnumsolver 1.20 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.35 644))
(source/parse_env.ml (lurette/41_parse_env. 1.36 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))
(source/formula.mli (lurette/44_formula.ml 1.19 644))
(source/formula.ml (lurette/45_formula.ml 1.24 644))
(source/formula.mli (lurette/44_formula.ml 1.20 644))
(source/formula.ml (lurette/45_formula.ml 1.25 644))
(source/print.mli (lurette/46_print.mli 1.12 644))
(source/print.ml (lurette/47_print.ml 1.21 644))
(source/print.mli (lurette/46_print.mli 1.13 644))
(source/print.ml (lurette/47_print.ml 1.22 644))
(source/eval.mli (lurette/48_eval.mli 1.10 644))
(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.35 644))
(source/env_state.ml (lurette/51_env_state. 1.36 644))
(source/automata.mli (lurette/b/46_automata.m 1.3 644))
(source/automata.ml (lurette/b/47_automata.m 1.6 644))
......@@ -155,18 +119,18 @@ source/ne.ml
;; Make files
(configure.in (lurette/d/11_configure. 1.1 644))
(Makefile.common.in (lurette/d/12_Makefile.c 1.2 644))
(OcamlMakefile (lurette/17_OcamlMakef 1.46 644))
(OcamlMakefile (lurette/17_OcamlMakef 1.47 644))
(Makefile.lurette (lurette/b/38_Makefile.l 1.16 644))
(user-rules (lurette/c/14_myrules 1.23 644))
(user-rules (lurette/c/14_myrules 1.24 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.12 644))
(source/Makefile.lucky (lurette/b/41_Makefile.i 1.13 644))
(source/Makefile.gen_stubs (lurette/b/42_Makefile.g 1.5 644))
(source/Makefile.lurette_lib (lurette/c/2_Makefile.l 1.12 644))
(source/Makefile.lurette_lib (lurette/c/2_Makefile.l 1.13 644))
(source/Makefile (lurette/c/20_Makefile 1.10 644))
;; Documentation
......@@ -184,10 +148,10 @@ source/ne.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.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))
(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))
;; Various files used for testing purposes
(test/usager.luc (lurette/b/14_usager.env 1.9 644))
......
......@@ -47,8 +47,8 @@ SOURCES_OCAML = \
$(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/store.mli \
$(LURETTE_PATH)/source/store.ml \
$(LURETTE_PATH)/source/env_state.mli \
$(LURETTE_PATH)/source/env_state.ml \
$(LURETTE_PATH)/source/solver.mli \
......
......@@ -34,7 +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/rnumsolver.mli $(LURETTE_PATH)/source/rnumsolver.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 \
$(LURETTE_PATH)/source/show_env.mli $(LURETTE_PATH)/source/show_env.ml \
......
......@@ -12,8 +12,6 @@ open Util
open List
open Graph
open Formula
open Rnumsolver
(****************************************************************************)
......
......@@ -38,7 +38,6 @@ and
| Bvar of string
| Eq of expr * expr (* = *)
| Neq of expr * expr (* <> *)
| Sup of expr * expr (* > *)
| SupEq of expr * expr (* >= *)
| Inf of expr * expr (* < *)
......@@ -105,7 +104,6 @@ and
| False -> "false"
| Bvar(str) -> (Prevar.format str)
| Eq(e1, e2) -> ((expr_to_string e1) ^ " = " ^ (expr_to_string e2))
| Neq(e1, e2) -> ((expr_to_string e1) ^ " <> " ^ (expr_to_string e2))
| SupEq(e1, e2) -> ((expr_to_string e1) ^ " >= " ^ (expr_to_string e2))
| Sup(e1, e2) -> ((expr_to_string e1) ^ " > " ^ (expr_to_string e2))
| InfEq(e1, e2) -> ((expr_to_string e1) ^ " <= " ^ (expr_to_string e2))
......
......@@ -40,7 +40,6 @@ and
| Bvar of string
| Eq of expr * expr (** = *)
| Neq of expr * expr (** <> *)
| Sup of expr * expr (** > *)
| SupEq of expr * expr (** >= *)
| Inf of expr * expr (** < *)
......
......@@ -755,7 +755,7 @@ and (parse_formula: in_channel -> vnt list -> aut_token -> formula) =
[< 'Genlex.Kwd "<>"; pl = parse_pragma_list ic ;
e1 = parse_expr ic vars ; e2 = parse_expr ic vars
>]
-> Neq(e1, e2)
-> Not(Eq(e1, e2))
|
[< 'Genlex.Kwd ">"; pl = parse_pragma_list ic ;
e1 = parse_expr ic vars ;e2 = parse_expr ic vars
......
......@@ -78,7 +78,8 @@ let (rat_of_float : float -> int * int) =
else
power 10 c
in
let n = (int_of_float (f*.(float_of_int d))) 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)
......@@ -93,6 +94,10 @@ let (rat_of_float : float -> int * int) =
);
(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
by Polka to parse constraints *)
let rec (ineq_to_polka_string : Constraint.ineq -> string) =
......
......@@ -23,9 +23,9 @@ let (linear_constraint : Constraint.t -> unit) =
fun af ->
print_string ((Constraint.to_string af) ^ "\n")
let (store : Rnumsolver.store -> unit) =
let (store : Store.t -> unit) =
fun s ->
print_string (Rnumsolver.store_to_string s)
print_string (Store.to_string s)
let (subst_list: subst list -> unit) =
......
......@@ -23,7 +23,7 @@ val subst_list: Formula.subst list -> unit
val arc_info : Formula.arc_info -> unit
val store : Rnumsolver.store -> unit
val store : Store.t -> unit
(*
val comb: Bdd.t -> unit
......
......@@ -15,7 +15,7 @@ open Util
open Hashtbl
open Gne
open Value
open Rnumsolver
open Store
(****************************************************************************)
......@@ -66,7 +66,7 @@ let (lookup: env_in -> subst list -> var_name -> Value.t option) =
(****************************************************************************)
type comp = SupZero | SupEqZero | EqZero | NeqZero
type comp = SupZero | SupEqZero | EqZero
let rec (formula_to_bdd : env_in -> formula -> Bdd.t * bool) =
fun input f ->
......@@ -144,10 +144,6 @@ let rec (formula_to_bdd : env_in -> formula -> Bdd.t * bool) =
let gne = expr_to_gne (Diff(e1, e2)) input in
(gne_to_bdd gne EqZero)
| Neq(e1, e2) ->
let gne = expr_to_gne (Diff(e1, e2)) input in
(gne_to_bdd gne NeqZero)
| SupEq(e1, e2) ->
let gne = expr_to_gne (Diff(e1, e2)) input in
(gne_to_bdd gne SupEqZero)
......@@ -411,37 +407,6 @@ and
gne
((Bdd.dfalse (Env_state.bdd_manager ())), false)
)
| NeqZero ->
( Gne.fold
(fun nexpr (c, dep) (acc, dep_acc) ->
let new_dep = dep || dep_acc
and bdd =
if Ne.is_a_constant nexpr
then
let cst = Ne.find "" nexpr in
match cst with
Some I(i) ->
if i = 0
then (Bdd.dfalse (Env_state.bdd_manager ()))
else (Bdd.dtrue (Env_state.bdd_manager ()))
| Some F(f) ->
if f = 0.
then (Bdd.dfalse (Env_state.bdd_manager ()))
else (Bdd.dtrue (Env_state.bdd_manager ()))
| None ->
(Bdd.dfalse (Env_state.bdd_manager ()))
else
Bdd.ithvar
(Env_state.bdd_manager ())
(Env_state.linear_constraint_to_index (EqZ(nexpr)) dep)
in
(Bdd.dor (Bdd.dand c (Bdd.dnot bdd)) acc, new_dep)
)
gne
((Bdd.dfalse (Env_state.bdd_manager ())), false)
)
(****************************************************************************)
(****************************************************************************)
......@@ -599,8 +564,8 @@ let (toss_up_one_var_index: var -> subst option) =
| _ -> None
let rec (draw_in_bdd: subst list * store -> Bdd.t -> Bdd.t ->
subst list * store * store) =
let rec (draw_in_bdd: subst list * Store.t -> Bdd.t -> Bdd.t ->
subst list * Store.t * Store.t) =
fun (sl, store) bdd comb ->
(** Returns [sl] appended to a draw of all the boolean variables
bigger than the topvar of [bdd] according to the ordering
......@@ -639,8 +604,8 @@ let rec (draw_in_bdd: subst list * store -> Bdd.t -> Bdd.t ->
draw_in_bdd_ineq ineq (sl, store) bdd comb
and (draw_in_bdd_bool: string -> subst list * store -> Bdd.t -> Bdd.t ->
subst list * store * store) =
and (draw_in_bdd_bool: string -> subst list * Store.t -> Bdd.t -> Bdd.t ->
subst list * Store.t * Store.t) =
fun var (sl, store) bdd comb ->
let bddvar = Bdd.topvar bdd in
let topvar_comb = Bdd.topvar comb in
......@@ -716,8 +681,8 @@ and (draw_in_bdd_bool: string -> subst list * store -> Bdd.t -> Bdd.t ->
flush stdout;
assert false
and (draw_in_bdd_ineq: Constraint.ineq -> subst list * store -> Bdd.t -> Bdd.t ->
subst list * store * store) =
and (draw_in_bdd_ineq: Constraint.ineq -> subst list * Store.t -> Bdd.t -> Bdd.t ->
subst list * Store.t * Store.t) =
fun cstr (sl, store) bdd comb ->
(*
When we add to the store an inequality constraint GZ(ne) or
......@@ -745,7 +710,7 @@ and (draw_in_bdd_ineq: Constraint.ineq -> subst list * store -> Bdd.t -> Bdd.t -
else
(cstr_neg, (Bdd.delse bdd), m, cstr, (Bdd.dthen bdd), n)
in
let store_copy = copy_store store in
let store_copy = Store.copy store in
let store1 = add_constraint store (Ineq cstr1) in
(* A solution will be found in this branch iff there exists
at least one path in the bdd that leads to a satisfiable
......@@ -775,8 +740,8 @@ and (draw_in_bdd_ineq: Constraint.ineq -> subst list * store -> Bdd.t -> Bdd.t -
flush stdout;
assert false
and (draw_in_bdd_eq: Ne.t -> subst list * store -> Bdd.t -> Bdd.t ->
subst list * store * store) =
and (draw_in_bdd_eq: Ne.t -> subst list * Store.t -> Bdd.t -> Bdd.t ->
subst list * Store.t * Store.t) =
fun ne (sl, store) bdd comb ->
(*
We consider 3 stores:
......@@ -801,7 +766,7 @@ and (draw_in_bdd_eq: Ne.t -> subst list * store -> Bdd.t -> Bdd.t ->
and cstr = (EqZ ne)
and not_cstr = (Ineq (GZ ne))
and not_cstr2 = (Ineq (GZ (Ne.neg_nexpr ne)))
and store_copy = copy_store store
and store_copy = Store.copy store
in
let (
cstr1, bdd1, sol_nb1,
......@@ -857,7 +822,7 @@ and (draw_in_bdd_eq: Ne.t -> subst list * store -> Bdd.t -> Bdd.t ->
draw_in_bdd (sl, store1) bdd1 comb
with
No_numeric_solution ->
let store_copy2 = copy_store store_copy in
let store_copy2 = Store.copy store_copy in
(*
The second branch is tried if no path in the first bdd
leaded to a satisfiable set of numeric constraints.
......
......@@ -4,12 +4,10 @@
** Public License
**-----------------------------------------------------------------------
**
** File: rnumsolver.ml
** File: store.ml
** Main author: jahier@imag.fr
*)
(** Numerical solver based on ranges. *)
open Formula
open Value
open Constraint
......@@ -17,7 +15,7 @@ open Polyhedron
open Util
open List
let debug_store = false
let debug_store = true
(* exported *)
exception No_numeric_solution
......@@ -30,7 +28,7 @@ type vars_domain =
| Range of (Formula.var_name, Polyhedron.range) Hashtbl.t
| Poly of (Formula.vnt list * Poly.t * (int -> string)) list
type store = {
type t = {
(**
This field is used to store where each variable ranges. It is
set to [Unsat] when the system becomes unsatisfiable, namely,
......@@ -74,7 +72,7 @@ type store = {
(* exported *)
let (new_store : Formula.vnt list -> store) =
let (new_store : Formula.vnt list -> t) =
fun vnt_l ->
let (add_one_var : (Formula.var_name, range) Hashtbl.t -> Formula.vnt
-> unit) =
......@@ -97,7 +95,7 @@ let (new_store : Formula.vnt list -> store) =
}
(* exported *)
let (copy_store : store -> store) =
let (copy : t -> t) =
fun store ->
match store.var with
Unsat -> { var = Unsat; substl = store.substl ; delay = store.delay }
......@@ -139,12 +137,12 @@ let (range_to_string : range -> string) =
("[" ^ (string_of_float min) ^ ", " ^ (string_of_float max) ^ "] ")
(* exported *)
let (store_to_string : store -> string) =
let (to_string : t -> string) =
fun s ->
let var_str = ("\n*** Variable ranges: \n" ^
match s.var with
Unsat -> "Empty store"
| Poly _ -> " XXX Rnumsolver.store_to_string: finish me ! "
| Poly _ -> " XXX Store.to_string: finish me ! "
| Range(tbl) ->
(Hashtbl.fold
(fun vn range acc ->
......@@ -176,7 +174,7 @@ let (store_to_string : store -> string) =
forever, which is really bad.
*)
(* exported *)
let (switch_to_polyhedron_representation : store -> store * store) =
let (switch_to_polyhedron_representation : t -> t * t) =
fun store ->
(* handle delayed constraints using polyhedron *)
match store.var with
......@@ -326,7 +324,7 @@ let (make_subst : vn -> Value.num -> Ne.subst) =
function returns [ne] as well as the store with the delayed
constraint [eqZ(-ne)] removed. *)
(* let (is_ineq_cstr_an_eq : Constraint.t -> store -> (store * Ne.t) option) = *)
(* let (is_ineq_cstr_an_eq : Constraint.t -> t -> (t * Ne.t) option) = *)
(* fun cstr store -> *)
(* let ne = *)
(* match cstr with *)
......@@ -372,7 +370,7 @@ let (make_subst : vn -> Value.num -> Ne.subst) =
(* exported *)
let rec (add_constraint : store -> Constraint.t -> store) =
let rec (add_constraint : t -> Constraint.t -> t) =
fun store cstr ->
let _ =
if debug_store then (
......@@ -713,7 +711,7 @@ let rec (add_constraint : store -> Constraint.t -> store) =
)
)
and (add_eq_to_store : store -> Ne.t -> store) =
and (add_eq_to_store : t -> Ne.t -> t) =
fun store ne0 ->
(*
[add_eq_to_store s e] returns the store [s] with the numeric
......@@ -803,7 +801,7 @@ and (add_eq_to_store : store -> Ne.t -> store) =
(* exported *)
let (is_store_satisfiable : store -> bool) =
let (is_store_satisfiable : t -> bool) =
fun store ->
store.var <> Unsat
......@@ -811,6 +809,8 @@ let (is_store_satisfiable : store -> bool) =
(*******************************************************************************)
(** [get_subst_from_solved_system sl] ougth to take in input a list
of pair "var_name_and_coef, normal_expr" such that the normal_expr
is reduced to a constant c. It returns the list of substitution
......@@ -832,7 +832,7 @@ let rec (get_subst_from_solved_system : ((string * Value.num) * Ne.t) list ->
let (deduce_remaining_vars : (string * Value.num) list ->