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 f0aff2da authored by Erwan Jahier's avatar Erwan Jahier
Browse files

lurette 0.54 Tue, 02 Apr 2002 14:25:12 +0200 by jahier

Parent-Version:      0.53
Version-Log:

Cosmetic change:

Encapsulates the various fields of Env_state.

Project-Description: Lurette
parent 1347da63
......@@ -4,18 +4,18 @@
(test/usager.env 446 1017156165 b/14_usager.env 1.5)
(source/command_line_ima_exe.mli 989 1016127950 b/34_command_li 1.1)
(doc/ocamldoc.sty 1380 1008328137 b/12_ocamldoc.s 1.1)
(source/env_state.ml 2978 1016803757 51_env_state. 1.15)
(source/env_state.ml 9471 1017750312 51_env_state. 1.16)
(source/graph.ml 1819 1016011748 14_graph.ml 1.5)
(source/util.ml 11251 1017335442 35_util.ml 1.16)
(source/wtree.ml 8518 1016011748 b/1_wtree.ml 1.9)
(source/solver.ml 22945 1017335442 39_solver.ml 1.19)
(source/command_line.ml 3998 1016024341 b/20_command_li 1.4)
(source/lurette.ml 11217 1017247563 12_lurette.ml 1.30)
(source/solver.ml 23024 1017750312 39_solver.ml 1.20)
(source/command_line.ml 4234 1017396284 b/20_command_li 1.5)
(source/lurette.ml 11288 1017750312 12_lurette.ml 1.32)
(source/solver.mli 1135 1016803757 38_solver.mli 1.10)
(source/env.mli 2517 1016803757 15_env.mli 1.10)
(source/env.mli 2593 1017396284 15_env.mli 1.11)
(test/heater_float.rif.exp 1461 1015514807 b/30_heater_flo 1.2)
(lurette.depfull.dot 49 1007651448 b/5_lurette.de 1.2)
(source/env.ml 10994 1017247563 16_env.ml 1.21)
(source/env.ml 10895 1017750312 16_env.ml 1.23)
(make_lurette 1149 1017335442 27_make_luret 1.8)
(test/vrai_tram.lus 453 1007379917 b/6_vrai_tram. 1.1)
(lurette.dep.dot 49 1007651448 b/4_lurette.de 1.2)
......@@ -25,7 +25,7 @@
(source/parse_env.mli 907 1016127950 40_parse_env. 1.6)
(ID_EN_VRAC 2184 1002196285 0_ID_EN_VRAC 1.1)
(source/sim2chro.mli 1427 1015250295 b/23_sim2chro.m 1.3)
(source/ima_exe.ml 7153 1017247563 b/32_ima_exe.ml 1.3)
(source/ima_exe.ml 7206 1017750312 b/32_ima_exe.ml 1.4)
(doc/automata_format 0 1007379917 b/3_automata_f 1.1)
(source/eval.ml 7749 1016803757 49_eval.ml 1.12)
(source/gen_stubs.ml 35425 1017335442 24_generate_l 1.21)
......@@ -36,21 +36,21 @@
(doc/ocamldoc.hva 313 1008328137 b/13_ocamldoc.h 1.1)
(source/formula.mli 3354 1016803757 44_formula.ml 1.9)
(TAGS 9825 1007379917 21_TAGS 1.6)
(test/Makefile_ima_exe 1622 1016803757 b/35_Makefile_i 1.2)
(source/command_line.mli 1317 1016024341 b/21_command_li 1.4)
(test/Makefile_ima_exe 1625 1017750312 b/35_Makefile_i 1.3)
(source/command_line.mli 1384 1017396284 b/21_command_li 1.5)
(source/wtree.mli 2340 1016011748 b/0_wtree.mli 1.7)
(test/porte.env 950 1017156165 b/16_porte.env 1.4)
(source/env_state.mli 3851 1016803757 50_env_state. 1.13)
(source/env_state.mli 5168 1017750312 50_env_state. 1.15)
(source/rnumsolver.mli 1764 1017335442 b/26_rnumsolver 1.3)
(source/ima_exe.mli 447 1016127950 b/31_ima_exe.ml 1.1)
(source/eval.mli 1389 1016803757 48_eval.mli 1.9)
(README 74 1011881677 10_README 1.2)
(test/ControleurPorte.c 9407 1012914629 b/19_Controleur 1.1)
(OcamlMakefile 19266 1017335442 17_OcamlMakef 1.24)
(OcamlMakefile 19265 1017396284 17_OcamlMakef 1.25)
(source/command_line_ima_exe.ml 2400 1016803757 b/33_command_li 1.2)
(test/ControleurPorte.rif.exp 4746 1016803757 b/29_Controleur 1.4)
(test/tram.env 990 1017156165 b/15_tram.env 1.4)
(source/show_env.ml 2961 1014048376 43_show_env.m 1.3)
(source/show_env.ml 2971 1017750312 43_show_env.m 1.4)
(source/gne.mli 1107 1016803757 b/36_gne.mli 1.1)
(doc/synthese 2556 1007379917 b/2_synthese 1.1)
(test/ControleurPorte.h 2306 1012914629 b/18_Controleur 1.1)
......@@ -58,7 +58,7 @@
(source/show_env.mli 765 1015250295 42_show_env.m 1.5)
(source/gne.ml 8204 1016803757 b/37_gne.ml 1.1)
(test/tram_simple.h 1746 1013519411 b/25_tram_simpl 1.1)
(Makefile 1837 1017335442 18_Makefile 1.25)
(Makefile 1839 1017750312 18_Makefile 1.26)
(test/vrai_tram.c 3060 1012914629 b/8_vrai_tram. 1.2)
(source/print.mli 789 1016803757 46_print.mli 1.8)
(source/graph.mli 1493 1015250295 13_graph.mli 1.6)
......
......@@ -3,7 +3,7 @@ OCAMLMAKEFILE = $(LURETTE_DIR)/OcamlMakefile
# OCAMLFLAGS = -noassert -unsafe
OCAMLNCFLAGS = -inline 10
# OCAMLNCFLAGS = -inline 10
-include ./lurette.in
......
;; -*- Prcs -*-
(Created-By-Prcs-Version 1 3 3)
(Project-Description "Lurette")
(Project-Version lurette 0 53)
(Parent-Version lurette 0 52)
(Project-Version lurette 0 54)
(Parent-Version lurette 0 53)
(Version-Log "
Add a --verbose and a --help options to the command line.
Cosmetic change:
Encapsulates the various fields of Env_state.
Also clean up a little bit comments in various places.
")
(New-Version-Log "")
(Checkin-Time "Fri, 29 Mar 2002 11:04:44 +0100")
(Checkin-Time "Tue, 02 Apr 2002 14:25:12 +0200")
(Checkin-Login jahier)
(Populate-Ignore ())
(Project-Keywords)
......@@ -21,14 +23,14 @@ Also clean up a little bit comments in various places.
;; Sources files for ima_exe
(source/ima_exe.mli (lurette/b/31_ima_exe.ml 1.1 644))
(source/ima_exe.ml (lurette/b/32_ima_exe.ml 1.3 644))
(source/ima_exe.ml (lurette/b/32_ima_exe.ml 1.4 644))
(source/command_line_ima_exe.ml (lurette/b/33_command_li 1.2 644))
(source/command_line_ima_exe.mli (lurette/b/34_command_li 1.1 644))
;; Sources files for lurette only
(source/lurette.mli (lurette/11_lurette.ml 1.12 644))
(source/lurette.ml (lurette/12_lurette.ml 1.31 644))
(source/lurette.ml (lurette/12_lurette.ml 1.32 644))
(source/command_line.ml (lurette/b/20_command_li 1.5 644))
(source/command_line.mli (lurette/b/21_command_li 1.5 644))
......@@ -38,12 +40,12 @@ Also clean up a little bit comments in various places.
(source/graph.ml (lurette/14_graph.ml 1.5 644))
(source/env.mli (lurette/15_env.mli 1.11 644))
(source/env.ml (lurette/16_env.ml 1.22 644))
(source/env.ml (lurette/16_env.ml 1.23 644))
(source/util.ml (lurette/35_util.ml 1.16 644))
(source/solver.mli (lurette/38_solver.mli 1.10 644))
(source/solver.ml (lurette/39_solver.ml 1.19 644))
(source/solver.ml (lurette/39_solver.ml 1.20 644))
(source/rnumsolver.mli (lurette/b/26_rnumsolver 1.3 644))
(source/rnumsolver.ml (lurette/b/27_rnumsolver 1.5 644))
......@@ -52,7 +54,7 @@ Also clean up a little bit comments in various places.
(source/parse_env.ml (lurette/41_parse_env. 1.13 644))
(source/show_env.mli (lurette/42_show_env.m 1.5 644))
(source/show_env.ml (lurette/43_show_env.m 1.3 644))
(source/show_env.ml (lurette/43_show_env.m 1.4 644))
(source/formula.mli (lurette/44_formula.ml 1.9 644))
(source/formula.ml (lurette/45_formula.ml 1.11 644))
......@@ -63,8 +65,8 @@ Also clean up a little bit comments in various places.
(source/eval.mli (lurette/48_eval.mli 1.9 644))
(source/eval.ml (lurette/49_eval.ml 1.12 644))
(source/env_state.mli (lurette/50_env_state. 1.14 644))
(source/env_state.ml (lurette/51_env_state. 1.15 644))
(source/env_state.mli (lurette/50_env_state. 1.15 644))
(source/env_state.ml (lurette/51_env_state. 1.16 644))
(source/wtree.mli (lurette/b/0_wtree.mli 1.7 644))
(source/wtree.ml (lurette/b/1_wtree.ml 1.9 644))
......@@ -76,9 +78,9 @@ Also clean up a little bit comments in various places.
;; Make files
(OcamlMakefile (lurette/17_OcamlMakef 1.25 644))
(Makefile (lurette/18_Makefile 1.25 644))
(Makefile (lurette/18_Makefile 1.26 644))
(interface/Makefile (lurette/25_Makefile 1.6 644))
(test/Makefile_ima_exe (lurette/b/35_Makefile_i 1.2 644))
(test/Makefile_ima_exe (lurette/b/35_Makefile_i 1.3 644))
(make_lurette (lurette/27_make_luret 1.8 744))
......
......@@ -14,7 +14,6 @@
open List
open Solver
open Formula
open Env_state
(****************************************************************************)
......@@ -66,14 +65,14 @@ let (read_env_state_one_file : string -> node) =
let list_pre_vn = add_missing_pre list_pre_vn0 in
(* Sets the [graph] field of [env_state]. *)
let node_nb = (List.length (Graph.get_all_nodes env_state.graph)) in
let node_nb = (List.length (Graph.get_all_nodes (Env_state.graph ()))) in
let (add_arc: Parse_env.read_arc -> unit) =
fun arc ->
match arc with
Parse_env.Arc(node_from, arc_info, node_to) ->
(Graph.add_trans
(-)
env_state.graph
(Env_state.graph ())
(node_from+node_nb)
arc_info
(node_to+node_nb));
......@@ -82,7 +81,7 @@ let (read_env_state_one_file : string -> node) =
(* Checks that there is no hole in the node numbers (which
would mean that the node number is not equal to the biggest node) *)
let new_node_nb = (List.length (Graph.get_all_nodes env_state.graph)) in
let new_node_nb = (List.length (Graph.get_all_nodes (Env_state.graph ()))) in
if (for_all
(fun arc ->
match arc with
......@@ -94,18 +93,14 @@ let (read_env_state_one_file : string -> node) =
(* Sets the [node_to_file_name] field of [env_state]. *)
List.iter
(fun node ->
if Hashtbl.mem env_state.node_to_file_name node
then ()
else Hashtbl.add env_state.node_to_file_name node file
)
(Graph.get_all_nodes env_state.graph);
(fun node -> Env_state.set_file_name (node+node_nb) file)
(Graph.get_all_nodes (Env_state.graph ()));
(* Sets the [var_names] and [pre_var_names] fields of [env_state]. *)
Hashtbl.add env_state.var_names file (list_in, list_out, list_loc) ;
Env_state.set_var_names file (list_in, list_out, list_loc) ;
List.iter
(fun vn -> env_state.pre_var_names <- (vn::env_state.pre_var_names))
(fun vn -> Env_state.set_pre_var_names (vn::(Env_state.pre_var_names ())))
list_pre_vn;
(init_node + node_nb)
......@@ -117,8 +112,8 @@ let (read_env_state : string list list -> unit) =
fun files_ll ->
(** Calls [read_env_state_one_file] on a list of list of files. *)
let nodes = map (map (read_env_state_one_file)) files_ll in
env_state.current_nodes <- nodes ;
env_state.wtree_table <- (Wtree.build_wtree_table env_state.graph)
Env_state.set_current_nodes nodes ;
Env_state.set_wtree_table (Wtree.build_wtree_table (Env_state.graph ()))
(****************************************************************************)
......@@ -166,8 +161,8 @@ let (solve_formula_list_list: env_in -> int -> node list list * formula list lis
(* Gets the list of (output and local) boolean and numeric
vars of the automata of which [node] belongs to, and
appends it to the accumulator [acc]. *)
let file = Hashtbl.find env_state.node_to_file_name node in
let (_, out, loc) = Hashtbl.find env_state.var_names file in
let file = Env_state.file_name node in
let (_, out, loc) = Env_state.var_names file in
let (bool_vntl, num_vntl) =
List.partition
(fun (vn, vt) -> match vt with BoolT -> true | _ -> false)
......@@ -270,15 +265,15 @@ let rec draw_n_p_values input n p cn_ll wtl =
let (env_try: int -> int -> env_in ->
(node list list * env_out * env_loc) list) =
fun n p input ->
let cn_ll = env_state.current_nodes
and wtt = env_state.wtree_table
let cn_ll = (Env_state.current_nodes ())
and wtt = (Env_state.wtree_table ())
in
let wtl = get_wtrees cn_ll wtt in
let nll_sl_sl_ll = draw_n_p_values input n p cn_ll wtl in
let nll_sl_sl_l = flatten nll_sl_sl_ll in
assert (length nll_sl_sl_l = (n*p));
env_state.input <- input;
Env_state.set_input input;
nll_sl_sl_l
(*****************************************************************************)
......@@ -288,9 +283,9 @@ let (env_try: int -> int -> env_in ->
(* Exported *)
let (env_step : node list list -> env_out -> env_loc -> unit) =
fun nodes_to output local ->
env_state.current_nodes <- nodes_to ;
env_state.output <- output ;
env_state.local <- local
Env_state.set_current_nodes nodes_to ;
Env_state.set_output output ;
Env_state.set_local local
(****************************************************************************)
......@@ -325,17 +320,17 @@ let (update_pre: env_in -> env_out -> env_loc -> unit) =
the env starts generate outputs. *)
None
in
let maybe_pre = List.map (maybe_update_one_pre_var) env_state.pre_var_names in
env_state.pre <-
List.fold_left
(fun acc ms ->
match ms with
Some(s) -> (s::acc)
| None -> acc
)
[]
maybe_pre
let maybe_pre = List.map (maybe_update_one_pre_var) (Env_state.pre_var_names ()) in
Env_state.set_pre
( List.fold_left
(fun acc ms ->
match ms with
Some(s) -> (s::acc)
| None -> acc
)
[]
maybe_pre
)
......
......@@ -21,55 +21,284 @@ open Wtree
*)
type env_stateT = {
(* var names and types given file by file *)
mutable var_names: (string, (vnt list * vnt list * vnt list)) Hashtbl.t;
var_names: (string, (vnt list * vnt list * vnt list)) Hashtbl.t;
(** Var names and types ([vnt]) of input, output, and local vars,
given module by module. *)
mutable pre_var_names: var_name list;
(** internal names of pre variables. *)
mutable output_var_names: vnt list;
mutable node_to_file_name: (int, string) Hashtbl.t;
mutable atomic_formula_to_index: ((atomic_formula, int) Hashtbl.t);
mutable index_to_atomic_formula: ((int, atomic_formula) Hashtbl.t);
(** Output var names and types. *)
node_to_file_name: (int, string) Hashtbl.t;
(** Associates each node in the environment automata with its
origin file name (i.e., the [.env] file it comes from).
We need that information to be able to retrieve the list of
variables that ougth to be generated from a list of nodes (the
current nodes in the (virtual) automata product). Indeed, some
variables that should be drawn do no necessarily appear in
formula; and once the whole bdd has been traversed for the draw,
we need to be able to know what variables are still to be drawn.
*)
atomic_formula_to_index: ((atomic_formula, 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);
(** Ditto in the other way. *)
mutable index_cpt: int;
mutable bdd_manager: Manager.t;
mutable bdd_tbl_global: (formula, Bdd.t) Hashtbl.t;
mutable bdd_tbl: (formula, Bdd.t) Hashtbl.t;
mutable snt: (Bdd.t, Util.sol_nb * Util.sol_nb) Hashtbl.t;
mutable current_nodes: node list list;
mutable graph: (node, arc_info) Graph.t ;
mutable wtree_table: Wtree.wtree_table ;
(** Counter used to create the index above. *)
bdd_manager: Manager.t;
(** bdd engine internal state. *)
bdd_tbl_global: (formula, Bdd.t) Hashtbl.t;
bdd_tbl: (formula, Bdd.t) Hashtbl.t;
(** Transforming a formula into a bdd is expensive, therefore we
store the result of this transformation in a table. Only formula
does not depend on pre nor input vars are stored in
[bdd_tbl_global]. The other ones are stored in the table
[bdd_tbl], which is cleared at each new step. *)
snt: (Bdd.t, Util.sol_nb * Util.sol_nb) Hashtbl.t;
(** Associates to a bdd the (absolute) number of solutions
contained in its lhs (then) and rhs (else) branches. Note that
adding those two numbers only give a number of solution that is
relative to which bdd points to it. *)
mutable current_nodes : node list list;
(** List of the automata current nodes (there are as many nodes as
there are environment run in parallel). *)
mutable graph : (node, arc_info) Graph.t ;
(** The automata is stored in a Graph.t *)
mutable wtree_table : Wtree.wtree_table ;
(** Mapping from nodes to [wtree] (see the doc of the [Wtree] module). *)
mutable pre: subst list;
mutable input : env_in ;
mutable output: env_out ;
mutable local : env_loc
(** Stores the values of pre variables. *)
mutable input : env_in ;
(** Ditto for input vars. *)
mutable output: env_out ;
(** Ditto for output vars. *)
mutable local : env_loc
(** Ditto for local vars. *)
}
let (env_state:env_stateT) = {
var_names = Hashtbl.create 0 ;
pre_var_names = [];
output_var_names = [];
node_to_file_name = Hashtbl.create 0 ;
atomic_formula_to_index = Hashtbl.create 0 ;
index_to_atomic_formula = Hashtbl.create 0 ;
index_cpt = 0 ;
bdd_manager = Manager.make 10 10 0 0 0;
bdd_tbl = Hashtbl.create 0;
bdd_tbl_global = Hashtbl.create 0;
snt = Hashtbl.create 3;
current_nodes = [];
graph = Graph.create () ;
wtree_table = Hashtbl.create 0 ;
pre = [] ;
input = Hashtbl.create 0 ;
output = [] ;
local = []
var_names = Hashtbl.create 0;
pre_var_names = [];
output_var_names = [];
node_to_file_name = Hashtbl.create 0 ;
bdd_manager = Manager.make 10 10 0 0 0;
graph = Graph.create () ;
wtree_table = Hashtbl.create 0 ;
(** The following values (possibly) change at each step *)
pre = [];
input = Hashtbl.create 0;
output = [];
local = [];
current_nodes = [];
snt = Hashtbl.create 3;
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;
index_cpt = 0
}
(****************************************************************************)
let (var_names: string -> vnt list * vnt list * vnt list) =
fun file ->
Hashtbl.find env_state.var_names file
let (set_var_names : string -> vnt list * vnt list * vnt list -> unit) =
fun file vntl ->
Hashtbl.replace env_state.var_names file vntl
let (in_env_unsorted : unit -> vnt list) =
fun _ ->
let vnt_list =
Hashtbl.fold
(fun _ (x,_,_) acc -> Util.merge x acc)
env_state.var_names
[]
in
vnt_list
let (out_env_unsorted : unit -> vnt list) =
fun _ ->
let vnt_list =
Hashtbl.fold
(fun _ (_,x,_) acc -> Util.merge x acc)
env_state.var_names
[]
in
vnt_list
let (loc_env_unsorted : unit -> vnt list) =
fun _ ->
let vnt_list =
Hashtbl.fold
(fun _ (_,_,x) acc -> Util.merge x acc)
env_state.var_names
[]
in
vnt_list
(****************************************************************************)
let (pre_var_names: unit -> var_name list) =
fun _ ->
env_state.pre_var_names
let (set_pre_var_names: var_name list -> unit) =
fun vnl ->
env_state.pre_var_names <- vnl
(****************************************************************************)
let (output_var_names: unit -> vnt list) =
fun _ ->
env_state.output_var_names
let (set_output_var_names: vnt list -> unit) =
fun vntl ->
env_state.output_var_names <- vntl
(****************************************************************************)
let (file_name: Formula.node -> string) =
fun node ->
Hashtbl.find env_state.node_to_file_name node
let (set_file_name: Formula.node -> string -> unit) =
fun node file ->
Hashtbl.replace env_state.node_to_file_name node file
(****************************************************************************)
let (bdd_manager : unit -> Manager.t) =
fun _ ->
env_state.bdd_manager
(****************************************************************************)
(****************************************************************************)
(** The following values change at each step *)
(****************************************************************************)
let (graph : unit -> (node, arc_info) Graph.t) =
fun _ ->
env_state.graph
let (set_graph : (node, arc_info) Graph.t -> unit) =
fun g ->
env_state.graph <- g
(****************************************************************************)
let (wtree_table : unit -> Wtree.wtree_table) =
fun _ ->
env_state.wtree_table
let (set_wtree_table : Wtree.wtree_table -> unit) =
fun wtt ->
env_state.wtree_table <- wtt
(****************************************************************************)
let (pre: unit -> subst list) =
fun _ ->
env_state.pre
let (set_pre: subst list -> unit) =
fun sl ->
env_state.pre <- sl
let (input : unit -> env_in) =
fun _ ->
env_state.input
let (set_input: env_in -> unit) =
fun input ->
env_state.input <- input
let (output: unit -> env_out) =
fun _ ->
env_state.output
let (set_output: env_out -> unit) =
fun output ->
env_state.output <- output
let (local : unit -> env_loc) =
fun _ ->
env_state.local
let (set_local: env_loc -> unit) =
fun local ->
env_state.local <- local
(****************************************************************************)
let (current_nodes : unit -> node list list) =
fun _ ->
env_state.current_nodes
let (set_current_nodes: node list list -> unit) =
fun nll ->
env_state.current_nodes <- nll
(****************************************************************************)
let (sol_number : Bdd.t -> Util.sol_nb * Util.sol_nb) =
fun bdd ->
Hashtbl.find env_state.snt bdd
let (set_sol_number : Bdd.t -> Util.sol_nb * Util.sol_nb -> unit) =
fun bdd sol_nb ->
Hashtbl.replace env_state.snt bdd sol_nb
let (clear_sol_numbers: unit -> unit) =
fun _ ->
Hashtbl.clear env_state.snt
let (sol_number_exists : Bdd.t -> bool) =
fun bdd ->
Hashtbl.mem env_state.snt bdd
(****************************************************************************)
let (bdd : formula -> Bdd.t) =
fun f ->
Hashtbl.find env_state.bdd_tbl f
let (set_bdd : formula -> Bdd.t -> unit) =
fun f bdd ->
Hashtbl.replace env_state.bdd_tbl f bdd
let (clear_bdd: unit -> unit) =
fun _ ->
Hashtbl.clear env_state.bdd_tbl
let (bdd_global : formula -> Bdd.t) =
fun f ->
Hashtbl.find env_state.bdd_tbl_global f
let (set_bdd_global : formula -> Bdd.t -> unit) =
fun f bdd ->
Hashtbl.replace env_state.bdd_tbl_global f bdd
(****************************************************************************)
let (index_cpt: unit -> int) =
fun _ ->
env_state.index_cpt
let (set_index_cpt: int -> unit) =
fun i ->
env_state.index_cpt <- i
let (atomic_formula_to_index : atomic_formula -> int) =
fun f ->
try Hashtbl.find env_state.atomic_formula_to_index f
with Not_found ->
env_state.index_cpt <- (env_state.index_cpt + 1);
set_index_cpt (env_state.index_cpt + 1);
Hashtbl.add env_state.atomic_formula_to_index f env_state.index_cpt;
Hashtbl.add env_state.index_to_atomic_formula env_state.index_cpt f;
env_state.index_cpt
......@@ -78,36 +307,3 @@ let (index_to_atomic_formula : int -> atomic_formula) =
fun i ->
Hashtbl.find env_state.index_to_atomic_formula i