Vous avez reçu un message "Your GitLab account has been locked ..." ? Pas d'inquiétude : lisez cet article https://docs.gricad-pages.univ-grenoble-alpes.fr/help/unlock/

Commit f8219704 authored by Erwan Jahier's avatar Erwan Jahier
Browse files

lurette 0.94 Fri, 27 Sep 2002 13:20:05 +0200 by jahier

Parent-Version:      0.93
Version-Log:

Prepare things for the next change (which will try to handle equalities
smartly).

source/solver.ml:
source/rnumsolver.ml:
   atomic_formula do not need both < and > (ditto for <= and >=).
   Indeed, I just need to take the opposite, and everything is fine.
   One advantage is that there are less cases to handle. But the key
   advantage is that it make the representation of constraint normal,
   which is important at least when I will try to detect equalities.

   Also add a subst list and constraint list fields to the store
   that will ebe used in the forthcoming change. They will resp.
   be used for removeing a dimension when an equality is encountered
   and to delay constraint with more than one variable.

source/constraint.ml,mli: (new files)
   Move there from formula.ml everything that is related to the internal
   representation of constraints.

   Also change the name of atomic_formula to linear_constraint, which is
   more informative.

Project-Description: Lurette
parent e9325bcf
......@@ -3,17 +3,17 @@
(Created-By-Prcs-Version 1 3 3)
(source/command_line_ima_exe.mli 1082 1021651153 b/34_command_li 1.3)
(doc/ocamldoc.sty 1380 1008328137 b/12_ocamldoc.s 1.1)
(source/env_state.ml 20581 1032510467 51_env_state. 1.28)
(source/env_state.ml 20707 1033125605 51_env_state. 1.29)
(source/graph.ml 2563 1027066799 14_graph.ml 1.7)
(bin/Makefile.ima_exe 2013 1027066799 b/41_Makefile.i 1.3)
(test/giro/onlyroll.lus 18298 1031732392 c/7_onlyroll.l 1.1)
(source/util.ml 15446 1032510467 35_util.ml 1.26)
(test/time.exp 5580 1032940601 b/48_time.exp 1.4)
(source/solver.ml 24592 1032940601 39_solver.ml 1.27)
(myrules 10429 1032940601 c/14_myrules 1.4)
(test/time.exp 5580 1033125605 b/48_time.exp 1.5)
(source/solver.ml 25138 1033125605 39_solver.ml 1.28)
(test/test_gen_stubs.h 1818 1020068208 b/45_test_gen_s 1.1)
(source/command_line.ml 4625 1031053030 b/20_command_li 1.8)
(source/lurette.ml 13388 1032510467 12_lurette.ml 1.52)
(myrules 10516 1033125605 c/14_myrules 1.5)
(source/solver.mli 1003 1027092697 38_solver.mli 1.13)
(source/env.mli 2028 1027349504 15_env.mli 1.15)
(test/heater_float.rif.exp 1459 1032362091 b/30_heater_flo 1.7)
......@@ -25,7 +25,8 @@
(lurette.dep.dot 49 1007651448 b/4_lurette.de 1.2)
(test/porte.ima 1050 1032789516 b/16_porte.env 1.8)
(doc/archi.fig 3693 1003928781 20_archi.fig 1.1)
(source/rnumsolver.ml 11348 1031053030 b/27_rnumsolver 1.7)
(source/constraint.ml 2387 1033125605 c/19_constraint 1.1)
(source/rnumsolver.ml 17099 1033125605 b/27_rnumsolver 1.8)
(ID_EN_VRAC 2184 1002196285 0_ID_EN_VRAC 1.1)
(source/parse_env.mli 1025 1027066799 40_parse_env. 1.9)
(source/sim2chro.mli 1455 1027943375 b/23_sim2chro.m 1.5)
......@@ -35,21 +36,21 @@
(doc/automata_format 0 1007379917 b/3_automata_f 1.1)
(source/control.ml 4416 1030975996 c/4_control.ml 1.3)
(source/eval.ml 7755 1027066799 49_eval.ml 1.13)
(source/gen_stubs.ml 34392 1032355637 24_generate_l 1.34)
(source/gen_stubs.ml 34425 1033125605 24_generate_l 1.35)
(source/parse_env.ml 24436 1032940601 41_parse_env. 1.28)
(doc/ocamldoc.hva 313 1008328137 b/13_ocamldoc.h 1.1)
(source/automata.mli 3397 1027349504 b/46_automata.m 1.2)
(source/sim2chro.ml 2716 1032355637 b/24_sim2chro.m 1.12)
(doc/Interface_draft 5232 1003928781 19_Interface_ 1.1)
(source/formula.mli 3694 1032940601 44_formula.ml 1.16)
(source/automata.mli 3397 1027349504 b/46_automata.m 1.2)
(source/sim2chro.ml 2732 1033125605 b/24_sim2chro.m 1.13)
(source/formula.mli 2813 1033125605 44_formula.ml 1.17)
(demo/chaudiere/chaudiere.ima 446 1032789516 c/11_chaudiere. 1.5)
(demo/chaudiere/buggy_chaudiere_ctrl.lus 219 1031732392 c/10_buggy_chau 1.1)
(demo/chaudiere/chaudiere_oracle.lus 107 1031732392 c/8_chaudiere_ 1.1)
(test/time.res 5580 1032940601 b/49_time.res 1.7)
(test/time.res 5580 1033125605 b/49_time.res 1.8)
(TAGS 9825 1007379917 21_TAGS 1.6)
(source/command_line.mli 1442 1031053030 b/21_command_li 1.7)
(source/env_state.mli 6729 1032355637 50_env_state. 1.23)
(source/rnumsolver.mli 1736 1031053030 b/26_rnumsolver 1.4)
(source/env_state.mli 6734 1033125605 50_env_state. 1.24)
(source/rnumsolver.mli 1996 1033125605 b/26_rnumsolver 1.5)
(source/ima_exe.mli 447 1016127950 b/31_ima_exe.ml 1.1)
(source/eval.mli 1395 1027066799 48_eval.mli 1.10)
(test/giro/giro.ima 2828 1032789516 c/6_giro.ima 1.2)
......@@ -57,38 +58,39 @@
(README 74 1011881677 10_README 1.2)
(demo/chaudiere/chaudiere_ctrl.lus 177 1031732392 c/9_chaudiere_ 1.1)
(test/ControleurPorte.c 9407 1012914629 b/19_Controleur 1.1)
(OcamlMakefile 22373 1032940601 17_OcamlMakef 1.40)
(OcamlMakefile 22451 1033125605 17_OcamlMakef 1.41)
(source/command_line_ima_exe.ml 2792 1031732392 b/33_command_li 1.5)
(test/ControleurPorte.rif.exp 4756 1032789516 b/29_Controleur 1.9)
(Makefile.lurette 698 1032940601 b/38_Makefile.l 1.11)
(source/show_env.ml 3603 1030532285 43_show_env.m 1.12)
(source/gne.mli 1079 1027066799 b/36_gne.mli 1.2)
(source/gne.mli 1093 1033125605 b/36_gne.mli 1.3)
(source/automata.ml 15818 1032355637 b/47_automata.m 1.4)
(ihm/xlurette/xlurette_glade_main.ml 16705 1032789516 c/12_xlurette_g 1.6)
(doc/synthese 2556 1007379917 b/2_synthese 1.1)
(bin/Makefile.lurette_lib 1768 1031732392 c/2_Makefile.l 1.2)
(bin/Makefile.lurette_lib 1846 1033125605 c/2_Makefile.l 1.3)
(bin/Makefile.gen_stubs 472 1030532285 b/42_Makefile.g 1.2)
(test/ControleurPorte.h 2306 1012914629 b/18_Controleur 1.1)
(source/show_env.mli 1091 1027066799 42_show_env.m 1.7)
(test/Makefile 105 1031732392 c/0_Makefile 1.4)
(ihm/xlurette/makefile 783 1032355637 c/16_makefile 1.1)
(test/temp_int.ima 686 1032789516 b/50_temp_int.e 1.2)
(source/gne.ml 8173 1027066799 b/37_gne.ml 1.2)
(source/gne.ml 8168 1033125605 b/37_gne.ml 1.3)
(test/tram_simple.h 1746 1013519411 b/25_tram_simpl 1.1)
(test/temp_float.ima 728 1032789516 b/51_temp_float 1.3)
(test/tram.ima 1079 1032789516 b/15_tram.env 1.8)
(test/giro/allocator.lus 1087 1031732392 c/5_allocator. 1.1)
(test/heater_float.lus 175 1020068208 b/44_heater_flo 1.1)
(test/vrai_tram.c 3060 1027066799 b/8_vrai_tram. 1.3)
(source/print.mli 773 1027066799 46_print.mli 1.10)
(source/print.mli 1158 1033125605 46_print.mli 1.11)
(source/lurettetop.ml 24867 1032510467 c/1_lurettetop 1.10)
(ihm/xlurette/xlurette.glade 43485 1032531447 c/13_xlurette.g 1.4)
(test/heater_int.lus 170 1020068208 b/43_heater_int 1.1)
(source/graph.mli 2218 1027066799 13_graph.mli 1.9)
(test/heater_int.rif.exp 860 1028297733 b/28_heater_int 1.6)
(source/formula.ml 7428 1032940601 45_formula.ml 1.19)
(source/formula.ml 5786 1033125605 45_formula.ml 1.20)
(source/lurette.mli 448 1016027474 11_lurette.ml 1.12)
(source/print.ml 5883 1030532285 47_print.ml 1.18)
(source/constraint.mli 1619 1033125605 c/18_constraint 1.1)
(source/print.ml 5831 1033125605 47_print.ml 1.19)
(test/vrai_tram.h 2468 1027066799 b/7_vrai_tram. 1.3)
(bin/Makefile.show_ima 1039 1027066799 b/40_Makefile.s 1.4)
(source/control.mli 3202 1030975671 c/3_control.ml 1.2)
......@@ -5,7 +5,7 @@
# For updates see:
# http://www.oefai.at/~markus/ocaml_sources
#
# $Id: OcamlMakefile 1.40 Wed, 25 Sep 2002 09:56:41 +0200 jahier $
# $Id: OcamlMakefile 1.41 Fri, 27 Sep 2002 13:20:05 +0200 jahier $
#
###########################################################################
......@@ -16,6 +16,7 @@ SOURCES_LURETTE_LIB = \
$(LURETTE_PATH)/source/util.ml \
$(LURETTE_PATH)/source/graph.mli $(LURETTE_PATH)/source/graph.ml \
$(LURETTE_PATH)/source/command_line.mli $(LURETTE_PATH)/source/command_line.ml \
$(LURETTE_PATH)/source/constraint.mli $(LURETTE_PATH)/source/constraint.ml \
$(LURETTE_PATH)/source/formula.mli $(LURETTE_PATH)/source/formula.ml \
$(LURETTE_PATH)/source/gne.mli $(LURETTE_PATH)/source/gne.ml \
$(LURETTE_PATH)/source/control.mli $(LURETTE_PATH)/source/control.ml \
......
......@@ -32,6 +32,7 @@ SOURCES = \
$(LURETTE_PATH)/source/util.ml \
$(LURETTE_PATH)/source/graph.mli $(LURETTE_PATH)/source/graph.ml \
$(LURETTE_PATH)/source/command_line.mli $(LURETTE_PATH)/source/command_line.ml \
$(LURETTE_PATH)/source/constraint.mli $(LURETTE_PATH)/source/constraint.ml \
$(LURETTE_PATH)/source/formula.mli $(LURETTE_PATH)/source/formula.ml \
$(LURETTE_PATH)/source/gne.mli $(LURETTE_PATH)/source/gne.ml \
$(LURETTE_PATH)/source/control.mli $(LURETTE_PATH)/source/control.ml \
......
;; -*- Prcs -*-
(Created-By-Prcs-Version 1 3 3)
(Project-Description "Lurette")
(Project-Version lurette 0 93)
(Parent-Version lurette 0 92)
(Project-Version lurette 0 94)
(Parent-Version lurette 0 93)
(Version-Log "
source/formula.ml:
Prepare things for the next change (which will try to handle equalities
smartly).
source/solver.ml:
source/parse_env.ml:
Handle boolean equalities with Bdd.eq instead of manually
converting it with <<and>>, <<not>> and <<or>>.
source/rnumsolver.ml:
atomic_formula do not need both < and > (ditto for <= and >=).
Indeed, I just need to take the opposite, and everything is fine.
One advantage is that there are less cases to handle. But the key
advantage is that it make the representation of constraint normal,
which is important at least when I will try to detect equalities.
Also add a subst list and constraint list fields to the store
that will ebe used in the forthcoming change. They will resp.
be used for removeing a dimension when an equality is encountered
and to delay constraint with more than one variable.
source/constraint.ml,mli: (new files)
Move there from formula.ml everything that is related to the internal
representation of constraints.
Also change the name of atomic_formula to linear_constraint, which is
more informative.
")
(New-Version-Log ""
)
(Checkin-Time "Wed, 25 Sep 2002 09:56:41 +0200")
(Checkin-Time "Fri, 27 Sep 2002 13:20:05 +0200")
(Checkin-Login jahier)
(Populate-Ignore ())
(Project-Keywords)
......@@ -47,10 +68,10 @@ source/parse_env.ml:
(source/util.ml (lurette/35_util.ml 1.26 644))
(source/solver.mli (lurette/38_solver.mli 1.13 644))
(source/solver.ml (lurette/39_solver.ml 1.27 644))
(source/solver.ml (lurette/39_solver.ml 1.28 644))
(source/rnumsolver.mli (lurette/b/26_rnumsolver 1.4 644))
(source/rnumsolver.ml (lurette/b/27_rnumsolver 1.7 644))
(source/rnumsolver.mli (lurette/b/26_rnumsolver 1.5 644))
(source/rnumsolver.ml (lurette/b/27_rnumsolver 1.8 644))
(source/parse_env.mli (lurette/40_parse_env. 1.9 644))
(source/parse_env.ml (lurette/41_parse_env. 1.28 644))
......@@ -58,44 +79,48 @@ source/parse_env.ml:
(source/show_env.mli (lurette/42_show_env.m 1.7 644))
(source/show_env.ml (lurette/43_show_env.m 1.12 644))
(source/formula.mli (lurette/44_formula.ml 1.16 644))
(source/formula.ml (lurette/45_formula.ml 1.19 644))
(source/formula.mli (lurette/44_formula.ml 1.17 644))
(source/formula.ml (lurette/45_formula.ml 1.20 644))
(source/print.mli (lurette/46_print.mli 1.10 644))
(source/print.ml (lurette/47_print.ml 1.18 644))
(source/print.mli (lurette/46_print.mli 1.11 644))
(source/print.ml (lurette/47_print.ml 1.19 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.23 644))
(source/env_state.ml (lurette/51_env_state. 1.28 644))
(source/env_state.mli (lurette/50_env_state. 1.24 644))
(source/env_state.ml (lurette/51_env_state. 1.29 644))
(source/automata.mli (lurette/b/46_automata.m 1.2 644))
(source/automata.ml (lurette/b/47_automata.m 1.4 644))
(source/sim2chro.mli (lurette/b/23_sim2chro.m 1.5 644))
(source/sim2chro.ml (lurette/b/24_sim2chro.m 1.12 644))
(source/sim2chro.ml (lurette/b/24_sim2chro.m 1.13 644))
(source/gne.mli (lurette/b/36_gne.mli 1.2 644))
(source/gne.ml (lurette/b/37_gne.ml 1.2 644))
(source/gne.mli (lurette/b/36_gne.mli 1.3 644))
(source/gne.ml (lurette/b/37_gne.ml 1.3 644))
(source/lurettetop.ml (lurette/c/1_lurettetop 1.10 644))
(source/gen_stubs.ml (lurette/24_generate_l 1.34 644))
(source/gen_stubs.ml (lurette/24_generate_l 1.35 644))
(source/control.mli (lurette/c/3_control.ml 1.2 644))
(source/control.ml (lurette/c/4_control.ml 1.3 644))
(source/constraint.mli (lurette/c/18_constraint 1.1 644))
(source/constraint.ml (lurette/c/19_constraint 1.1 644))
; little script that sets env vars and starts the lurette build
(make_lurette (lurette/27_make_luret 1.16 755))
;; Make files
(OcamlMakefile (lurette/17_OcamlMakef 1.40 644))
(OcamlMakefile (lurette/17_OcamlMakef 1.41 644))
(Makefile.lurette (lurette/b/38_Makefile.l 1.11 644))
(myrules (lurette/c/14_myrules 1.5 644))
(bin/Makefile.show_ima (lurette/b/40_Makefile.s 1.4 644))
(bin/Makefile.ima_exe (lurette/b/41_Makefile.i 1.3 644))
(bin/Makefile.gen_stubs (lurette/b/42_Makefile.g 1.2 644))
(bin/Makefile.lurette_lib (lurette/c/2_Makefile.l 1.2 644))
(bin/Makefile.lurette_lib (lurette/c/2_Makefile.l 1.3 644))
;; Documentation
(doc/Interface_draft (lurette/19_Interface_ 1.1 644))
......@@ -112,8 +137,8 @@ source/parse_env.ml:
(lurette.depfull.dot (lurette/b/5_lurette.de 1.2 644))
(TAGS (lurette/21_TAGS 1.6 644))
(test/time.exp (lurette/b/48_time.exp 1.4 644))
(test/time.res (lurette/b/49_time.res 1.7 644))
(test/time.exp (lurette/b/48_time.exp 1.5 644))
(test/time.res (lurette/b/49_time.res 1.8 644))
;; Various files used for testing purposes
(test/usager.ima (lurette/b/14_usager.env 1.9 644))
......@@ -163,17 +188,11 @@ source/parse_env.ml:
(demo/chaudiere/chaudiere.ima (lurette/c/11_chaudiere. 1.5 644))
(myrules (lurette/c/14_myrules 1.4 644))
;; Files added by populate at Tue, 24 Sep 2002 15:30:27 +0200,
;; to version 0.92(w), by jahier:
(test/ControleurPorte.lus (lurette/c/17_Controleur 1.1 644))
)
(Merge-Parents)
(New-Merge-Parents)
......@@ -201,6 +201,7 @@ release:
$(LURETTE_PATH)/source/ima_exe.mli $(LURETTE_PATH)/source/ima_exe.ml \
$(LURETTE_PATH)/source/command_line_ima_exe.mli $(LURETTE_PATH)/source/command_line_ima_exe.ml \
$(LURETTE_PATH)/source/command_line.mli $(LURETTE_PATH)/source/command_line.ml \
$(LURETTE_PATH)/source/constraint.mli $(LURETTE_PATH)/source/constraint.ml \
$(LURETTE_PATH)/source/formula.mli $(LURETTE_PATH)/source/formula.ml \
$(LURETTE_PATH)/source/gne.mli $(LURETTE_PATH)/source/gne.ml \
$(LURETTE_PATH)/source/parse_env.mli $(LURETTE_PATH)/source/parse_env.ml \
......
(*-----------------------------------------------------------------------
** Copyright (C) 2001 - Verimag.
** This file may only be copied under the terms of the GNU Library General
** Public License
**-----------------------------------------------------------------------
**
** File: constraint.ml
** Main author: jahier@imag.fr
*)
(****************************************************************************)
(* exported *)
type num_value = I of int | F of float
type var_value = B of bool | N of num_value
(****************************************************************************)
(* exported *)
module NeMap = struct
include Map.Make(struct type t = string let compare = compare end)
end
(* exported *)
type n_expr = num_value NeMap.t
(* exported *)
let (is_n_expr_a_constant : n_expr -> bool) =
fun ne ->
(NeMap.remove "" ne) = NeMap.empty
(* exported *)
let (neg_nexpr : n_expr -> n_expr) =
fun ne ->
NeMap.map (fun x -> match x with I(i) -> I(-i) | F(f) -> F(-.f)) ne
(****************************************************************************)
(* exported *)
type t =
| Bv of string (** booleans *)
| GZ of n_expr (** expr > 0 *)
| GeqZ of n_expr (** expr >= 0 *)
| EqZ of n_expr (** expr = 0 *)
(****************************************************************************)
(* Pretty prints formula and expressions *)
(* exported *)
let (num_value_to_string : num_value -> string) =
fun n ->
match n with
I(i) -> string_of_int i
| F(f) -> Util.my_string_of_float f
(* exported *)
let (n_expr_to_string : n_expr -> string) =
fun ne ->
(NeMap.fold
(fun vn v acc ->
if vn = ""
then ((num_value_to_string v) ^ acc)
else (" + " ^ (num_value_to_string v ) ^ "*" ^ vn ^ acc ))
ne
""
)
(* exported *)
let (linear_constraint_to_string : t -> string) =
fun f ->
match f with
| Bv(str) -> str
| GZ(ne) -> ((n_expr_to_string ne) ^ " > 0 ")
| GeqZ(ne) -> ((n_expr_to_string ne) ^ " >= 0 ")
| EqZ(ne) -> ((n_expr_to_string ne) ^ " = 0 ")
(* exported *)
let print_var_value oc e =
match e with
N(I(i)) -> output_string oc ((string_of_int i) ^ " ")
| N(F(f)) -> output_string oc ((Util.my_string_of_float f) ^ " ")
| B(true) -> output_string oc "t "
| B(false) -> output_string oc "f "
(*-----------------------------------------------------------------------
** Copyright (C) 2001 - Verimag.
** This file may only be copied under the terms of the GNU Library General
** Public License
**-----------------------------------------------------------------------
**
** File: constraint.mli
** Main author: jahier@imag.fr
*)
(** Defines internal representation of constraints used in formula,
namely, linear constraints over booleans, intergers, and floats. *)
(** Internal representation of values. *)
type num_value = I of int | F of float
type var_value = B of bool | N of num_value
(** Map indexed by strings (variable names). *)
module NeMap : Map.S with type key = string
(** Normal expressions.
Keys are var names, and the content is the coefficient of the
monomial. By convention, "" maps the constant value. For instance,
[("a" -> I(3) ; "b" -> I(-2) ; "" -> I(11))] represents the
expression [3*a - 2*b + 11].
*)
type n_expr = num_value NeMap.t
(** [is_n_expr_a_constant ne] returns true iff [ne] is a constant. *)
val is_n_expr_a_constant : n_expr -> bool
(** [neg_nexpr ne] returns the opposite of [ne], namely, [-ne]. *)
val neg_nexpr : n_expr -> n_expr
(** Normalised linear constraints. *)
type t =
| Bv of string (** booleans *)
| GZ of n_expr (** expr > 0 *)
| GeqZ of n_expr (** expr >= 0 *)
| EqZ of n_expr (** expr = 0 *)
(** Pretty printing. *)
val num_value_to_string : num_value -> string
val n_expr_to_string : n_expr -> string
val print_var_value : out_channel -> var_value -> unit
val linear_constraint_to_string : t -> string
......@@ -46,15 +46,15 @@ type env_stateT = {
we need to be able to know what variables are still to be drawn.
*)
atomic_formula_to_index: ((atomic_formula, int) Hashtbl.t);
linear_constraint_to_index: ((Constraint.t, int) Hashtbl.t);
(** This indexing of (output and local) variable names is used
for constructing bdds in the boolean solver (for which variables
are [int], not [string]s). *)
index_to_atomic_formula: ((int, atomic_formula) Hashtbl.t);
index_to_linear_constraint: ((int, Constraint.t) Hashtbl.t);
(** Ditto in the other way. *)
global_atomic_formula_to_index: ((atomic_formula, int) Hashtbl.t);
index_to_global_atomic_formula: ((int, atomic_formula) Hashtbl.t);
global_linear_constraint_to_index: ((Constraint.t, int) Hashtbl.t);
index_to_global_linear_constraint: ((int, Constraint.t) Hashtbl.t);
(** The same as the tables above, except that they only contain the
formula which content does npt depend on input nor pre variables.
We need to maitain those two kinds of tables because unlike the
......@@ -132,10 +132,10 @@ let (env_state:env_stateT) = {
draw_mode = Inside;
bdd_tbl = Hashtbl.create 0;
bdd_tbl_global = Hashtbl.create 0;
atomic_formula_to_index = Hashtbl.create 0;
index_to_atomic_formula = Hashtbl.create 0;
global_atomic_formula_to_index = Hashtbl.create 0;
index_to_global_atomic_formula = Hashtbl.create 0;
linear_constraint_to_index = Hashtbl.create 0;
index_to_linear_constraint = Hashtbl.create 0;
global_linear_constraint_to_index = Hashtbl.create 0;
index_to_global_linear_constraint = Hashtbl.create 0;
index_cpt = 0 ;
free_index_list = []
}
......@@ -348,19 +348,19 @@ let (free_indexes : int list -> unit) =
(* exported *)
let (atomic_formula_to_index : atomic_formula -> bool -> int) =
let (linear_constraint_to_index : Constraint.t -> bool -> int) =
fun f depend_on_input ->
if
depend_on_input
then
(
try Hashtbl.find env_state.atomic_formula_to_index f
try Hashtbl.find env_state.linear_constraint_to_index f
with Not_found ->
let index = get_an_index () in
Hashtbl.add env_state.atomic_formula_to_index f index;
Hashtbl.add env_state.index_to_atomic_formula index f;
Hashtbl.add env_state.linear_constraint_to_index f index;
Hashtbl.add env_state.index_to_linear_constraint index f;
(* output_string stderr ( *)
(* (atomic_formula_to_string f) ^ "\t<-> " ^ *)
(* (linear_constraint_to_string f) ^ "\t<-> " ^ *)
(* (string_of_int index) ^ "\n" ) ; *)
(* flush stderr; *)
......@@ -368,41 +368,41 @@ let (atomic_formula_to_index : atomic_formula -> bool -> int) =
)
else
(
try Hashtbl.find env_state.global_atomic_formula_to_index f
try Hashtbl.find env_state.global_linear_constraint_to_index f
with Not_found ->
let index = get_an_index () in
Hashtbl.add env_state.global_atomic_formula_to_index f index;
Hashtbl.add env_state.index_to_global_atomic_formula index f;
Hashtbl.add env_state.global_linear_constraint_to_index f index;
Hashtbl.add env_state.index_to_global_linear_constraint index f;
index
)
(* exported *)
let (index_to_atomic_formula : int -> atomic_formula) =
let (index_to_linear_constraint : int -> Constraint.t) =
fun i ->
try Hashtbl.find env_state.index_to_global_atomic_formula i
try Hashtbl.find env_state.index_to_global_linear_constraint i
with Not_found ->
Hashtbl.find env_state.index_to_atomic_formula i
Hashtbl.find env_state.index_to_linear_constraint i
(* exported *)
let (clear_atomic_formula_index : unit -> unit) =
let (clear_linear_constraint_index : unit -> unit) =
fun _ ->
let index_to_free =
Hashtbl.fold
(fun index _ acc -> index::acc)
env_state.index_to_atomic_formula
env_state.index_to_linear_constraint
[];
in
Hashtbl.clear env_state.index_to_atomic_formula ;
Hashtbl.clear env_state.atomic_formula_to_index ;
Hashtbl.clear env_state.index_to_linear_constraint ;
Hashtbl.clear env_state.linear_constraint_to_index ;
free_indexes index_to_free
(* exported *)
let (clear_global_atomic_formula_index : unit -> unit) =
let (clear_global_linear_constraint_index : unit -> unit) =
fun _ ->
Hashtbl.clear env_state.index_to_global_atomic_formula ;
Hashtbl.clear env_state.global_atomic_formula_to_index ;
Hashtbl.clear env_state.index_to_global_linear_constraint ;
Hashtbl.clear env_state.global_linear_constraint_to_index ;
env_state.index_cpt <- 0;
env_state.free_index_list <- []
......@@ -419,7 +419,7 @@ let (set_output_var_names: vnt list -> unit) =
env_state.output_var_names <- vntl0
(*
Initializing the atomic_formula <-> index table for
Initializing the linear_constraint <-> index table for
boolean var now and once for all so that boolean var
to be generated are stored for small indexes so that
we can clear those index table at each step for bigger
......@@ -564,7 +564,7 @@ let (read_env_state : string list list -> unit) =
let (clear_step : unit -> unit) =
fun _ ->
clear_bdd () ;
clear_atomic_formula_index () ;
clear_linear_constraint_index () ;
(* if (t mod 100) = 0
then
......@@ -580,7 +580,7 @@ let (clear_step : unit -> unit) =
let (clear_all : unit -> unit) =
fun _ ->
clear_bdd_global () ;
clear_global_atomic_formula_index () ;
clear_global_linear_constraint_index () ;
clear_ima ();
clear_step ();
Manager.free env_state.bdd_manager ;
......@@ -609,20 +609,22 @@ let (dump_env_state_stat : out_channel -> unit) =
(string_of_int (hashtbl_size env_state.node_to_file_name)));
dump "\n";
dump ("*** atomic_formula_to_index:" ^
(string_of_int (hashtbl_size env_state.atomic_formula_to_index)));
dump ("*** linear_constraint_to_index:" ^
(string_of_int (hashtbl_size env_state.linear_constraint_to_index)));
dump "\n";
dump ("*** index_to_atomic_formula:" ^
(string_of_int (hashtbl_size env_state.index_to_atomic_formula)));
dump ("*** index_to_linear_constraint:" ^
(string_of_int (hashtbl_size env_state.index_to_linear_constraint)));
dump "\n";
dump ("*** global_atomic_formula_to_index:" ^
(string_of_int (hashtbl_size env_state.global_atomic_formula_to_index)));
dump ("*** global_linear_constraint_to_index:" ^
(string_of_int
(hashtbl_size env_state.global_linear_constraint_to_index)));
dump "\n";
dump ("*** index_to_global_atomic_formula:" ^
(string_of_int (hashtbl_size env_state.index_to_global_atomic_formula)));
dump ("*** index_to_global_linear_constraint:" ^
(string_of_int
(hashtbl_size env_state.index_to_global_linear_constraint)));
dump "\n";
dump ("*** cpt_index:" ^
......@@ -630,7 +632,8 @@ let (dump_env_state_stat : out_channel -> unit) =
dump "\n";
dump ("*** free_index_list: " ^
(fold_left (fun acc i -> acc ^ ", " ^ (string_of_int i)) "" env_state.free_index_list));
(fold_left (fun acc i -> acc ^ ", " ^ (string_of_int i)) ""
env_state.free_index_list));
dump "\n";
......
......@@ -137,7 +137,7 @@ val sol_number_exists : Bdd.t -> bool
table. Formula that does not depend on pre nor input vars are
stored in a different table that is not cleared at each new step
(cf [bdd_global] and [set_bdd_global] versus [bdd] and [set_bdd]).
Ditto for the atomic_formula <-> bdd index tables.
Ditto for the linear_constraint <-> bdd index tables.
*)
(** Returns the bdd of a formula if it is available in [env_state],
......@@ -158,10 +158,10 @@ val set_bdd_global : formula -> Bdd.t -> unit