Commit 8b44df60 authored by Erwan Jahier's avatar Erwan Jahier

lurette 0.36 Mon, 04 Mar 2002 13:50:13 +0100 by jahier

Parent-Version:      0.35
Version-Log:

Add support to handle numerical contraints. The numerical stuff is
untested, but the boolean part works as before.

source/rnumsolver.mli:
source/rnumsolver.ml:
    New files implementing a numeric solver based on intervals.

source/*.ml:
    Change the var_type type from a string to a sum type containing
    the lower and upper bounds of numeric domains.

    Do not maintain a var_name to index correspondance, but a formula to
    index one. This is to be able to handle numerical constraint in bdds.
    This field is not set at init time anymore, but in formula_to_bdd.

    Add <>, <, and <= to the type of formula.

Project-Description: Lurette
parent 429604ce
......@@ -3,56 +3,58 @@
(Created-By-Prcs-Version 1 3 3)
(test/usager.env 396 1013445149 b/14_usager.env 1.2)
(doc/ocamldoc.sty 1380 1008328137 b/12_ocamldoc.s 1.1)
(source/env_state.ml 2310 1014132434 51_env_state. 1.10)
(source/env_state.ml 2789 1015246213 51_env_state. 1.11)
(source/graph.ml 2476 1012914629 14_graph.ml 1.3)
(source/util.ml 9166 1014111658 35_util.ml 1.10)
(source/util.ml 9392 1015246213 35_util.ml 1.11)
(source/wtree.ml 9644 1014051154 b/1_wtree.ml 1.8)
(source/solver.ml 12217 1014132434 39_solver.ml 1.11)
(source/solver.ml 18003 1015246213 39_solver.ml 1.12)
(source/command_line.ml 3971 1014048376 b/20_command_li 1.3)
(source/lurette.ml 11253 1014132434 12_lurette.ml 1.22)
(source/solver.mli 969 1014048376 38_solver.mli 1.7)
(source/lurette.ml 11540 1015246213 12_lurette.ml 1.23)
(source/solver.mli 1041 1015246213 38_solver.mli 1.8)
(source/env.mli 2506 1013445149 15_env.mli 1.8)
(lurette.depfull.dot 49 1007651448 b/5_lurette.de 1.2)
(source/env.ml 9036 1013517738 16_env.ml 1.14)
(source/env.ml 8596 1015246213 16_env.ml 1.15)
(make_lurette 812 1013517738 27_make_luret 1.7)
(test/vrai_tram.lus 453 1007379917 b/6_vrai_tram. 1.1)
(lurette.dep.dot 49 1007651448 b/4_lurette.de 1.2)
(test/passerelle.env 862 1012914629 b/17_passerelle 1.1)
(doc/archi.fig 3693 1003928781 20_archi.fig 1.1)
(source/rnumsolver.ml 5159 1015246213 b/27_rnumsolver 1.1)
(source/parse_env.mli 939 1008328137 40_parse_env. 1.3)
(ID_EN_VRAC 2184 1002196285 0_ID_EN_VRAC 1.1)
(source/sim2chro.mli 1421 1014051154 b/23_sim2chro.m 1.2)
(doc/automata_format 0 1007379917 b/3_automata_f 1.1)
(source/eval.ml 8064 1014132434 49_eval.ml 1.6)
(source/eval.ml 8697 1015246213 49_eval.ml 1.7)
(source/gen_stubs.ml 32502 1014132434 24_generate_l 1.17)
(source/parse_env.ml 9215 1012914629 41_parse_env. 1.4)
(test/lurette.rif.exp 4746 1014132434 b/22_lurette.ri 1.5)
(source/parse_env.ml 9616 1015246213 41_parse_env. 1.5)
(test/lurette.rif.exp 4746 1015246213 b/22_lurette.ri 1.6)
(interface/TAGS 1956 1007380262 26_TAGS 1.3)
(source/sim2chro.ml 2639 1014132434 b/24_sim2chro.m 1.3)
(doc/Interface_draft 5232 1003928781 19_Interface_ 1.1)
(doc/ocamldoc.hva 313 1008328137 b/13_ocamldoc.h 1.1)
(source/formula.mli 1942 1014132434 44_formula.ml 1.5)
(source/formula.mli 2161 1015246213 44_formula.ml 1.6)
(source/command_line.mli 1302 1014048376 b/21_command_li 1.3)
(TAGS 9825 1007379917 21_TAGS 1.6)
(source/wtree.mli 2964 1013517738 b/0_wtree.mli 1.5)
(source/env_state.mli 3605 1014051154 50_env_state. 1.8)
(test/porte.env 861 1012914629 b/16_porte.env 1.1)
(source/eval.mli 1668 1013445149 48_eval.mli 1.4)
(source/env_state.mli 3822 1015246213 50_env_state. 1.9)
(source/rnumsolver.mli 1909 1015246213 b/26_rnumsolver 1.1)
(source/eval.mli 1682 1015246213 48_eval.mli 1.5)
(README 74 1011881677 10_README 1.2)
(test/ControleurPorte.c 9407 1012914629 b/19_Controleur 1.1)
(OcamlMakefile 18594 1014132434 17_OcamlMakef 1.17)
(source/show_env.ml 2961 1014048376 43_show_env.m 1.3)
(OcamlMakefile 18628 1015246213 17_OcamlMakef 1.18)
(test/tram.env 806 1012914629 b/15_tram.env 1.1)
(source/show_env.ml 2961 1014048376 43_show_env.m 1.3)
(doc/synthese 2556 1007379917 b/2_synthese 1.1)
(test/ControleurPorte.h 2306 1012914629 b/18_Controleur 1.1)
(interface/Makefile 197 1008255910 25_Makefile 1.6)
(source/show_env.mli 826 1014048376 42_show_env.m 1.4)
(test/tram_simple.h 1746 1013519411 b/25_tram_simpl 1.1)
(Makefile 1645 1014111658 18_Makefile 1.20)
(Makefile 1776 1015246213 18_Makefile 1.21)
(test/vrai_tram.c 3060 1012914629 b/8_vrai_tram. 1.2)
(source/print.mli 597 1014048376 46_print.mli 1.5)
(source/graph.mli 1499 1014048376 13_graph.mli 1.5)
(source/formula.ml 3967 1014132434 45_formula.ml 1.6)
(source/formula.ml 4579 1015246213 45_formula.ml 1.7)
(source/lurette.mli 396 1012914629 11_lurette.ml 1.10)
(source/print.ml 5340 1014111658 47_print.ml 1.7)
(source/print.ml 5534 1015246213 47_print.ml 1.8)
(test/vrai_tram.h 2468 1012914629 b/7_vrai_tram. 1.2)
......@@ -11,8 +11,10 @@ INCDIRS = /home/jahier/include
LIBDIRS = /home/jahier/lib /home/jahier/lib/ocaml
# Requires cudd and mldd to be installed!
LIBS = dd nums
CLIBS = dd_caml cudd mtr st epd util
LIBS = dd nums # mlpoly
CLIBS = dd_caml cudd mtr st epd util # libppl libpolyi
USE_CAMLP4 = yes
SOURCES_C = $(SUT) sut_stub.c sut_idl_stub.idl \
......@@ -26,6 +28,7 @@ SOURCES_OCAML = \
$(LURETTE_DIR)/source/parse_env.mli $(LURETTE_DIR)/source/parse_env.ml \
$(LURETTE_DIR)/source/env_state.mli $(LURETTE_DIR)/source/env_state.ml \
$(LURETTE_DIR)/source/print.mli $(LURETTE_DIR)/source/print.ml \
$(LURETTE_DIR)/source/rnumsolver.mli $(LURETTE_DIR)/source/rnumsolver.ml \
$(LURETTE_DIR)/source/solver.mli $(LURETTE_DIR)/source/solver.ml \
$(LURETTE_DIR)/source/wtree.mli $(LURETTE_DIR)/source/wtree.ml \
$(LURETTE_DIR)/source/show_env.mli $(LURETTE_DIR)/source/show_env.ml \
......
......@@ -5,7 +5,7 @@
# For updates see:
# http://miss.wu-wien.ac.at/~mottl/ocaml_sources
#
# $Id: OcamlMakefile 1.17 Tue, 19 Feb 2002 16:27:14 +0100 jahier $
# $Id: OcamlMakefile 1.18 Mon, 04 Mar 2002 13:50:13 +0100 jahier $
#
###########################################################################
......@@ -477,7 +477,7 @@ pncl: profiling-native-code-library
# Generates emacs tags
tags:
$(OTAGS) -v $(SOURCES)
$(OTAGS) -v $(SOURCES) ; cp TAGS ../source
# Generates the modules dependency graph using ocamldot
# (results in lurette.dep.ps and lurette.depfull.ps).
......@@ -504,7 +504,7 @@ try:
vroum:
../make_lurette ControleurPorte vrai_tram nc; \
time ./lurette 4500 1 1 tram.env usager.env porte.env passerelle.env -seed 1014422484 -ns2c --no-oracle
time ./lurette 4500 1 1 tram.env usager.env porte.env passerelle.env -seed 1015403953 -ns2c --no-oracle
# Non regression test
test:
......@@ -542,8 +542,8 @@ dochtml:
../source/gen_stub.mli ../source/gen_stub.ml
doctex:
ocamldoc -t "Lurette implementation description" -latex -d ../doc -stars \
-keep-code -I ../source/ $(SOURCES_OCAML) \
ocamldoc -t "Lurette implementation description" -no-stop -latex -d ../doc -stars \
-keep-code -m A -I ../source/ $(SOURCES_OCAML) \
../source/gen_stub.mli ../source/gen_stub.ml ; \
pushd ../doc ; latex doc.tex ; popd
......
;; -*- Prcs -*-
(Created-By-Prcs-Version 1 3 3)
(Project-Description "Lurette")
(Project-Version lurette 0 35)
(Parent-Version lurette 0 34)
(Version-Log " Use Hashtbl instead of assoc list to store env_in
items as eval needs to search in it very often, it might be an issue
when there is a lot of input variables.
(Project-Version lurette 0 36)
(Parent-Version lurette 0 35)
(Version-Log "
Add support to handle numerical contraints. The numerical stuff is
untested, but the boolean part works as before.
source/rnumsolver.mli:
source/rnumsolver.ml:
New files implementing a numeric solver based on intervals.
source/*.ml:
Change the var_type type from a string to a sum type containing
the lower and upper bounds of numeric domains.
Do not maintain a var_name to index correspondance, but a formula to
index one. This is to be able to handle numerical constraint in bdds.
This field is not set at init time anymore, but in formula_to_bdd.
Add <>, <, and <= to the type of formula.
")
(New-Version-Log "")
(Checkin-Time "Tue, 19 Feb 2002 16:27:14 +0100")
(Checkin-Time "Mon, 04 Mar 2002 13:50:13 +0100")
(Checkin-Login jahier)
(Populate-Ignore ())
(Project-Keywords)
......@@ -21,36 +37,39 @@ when there is a lot of input variables.
;; Sources files
(source/lurette.mli (lurette/11_lurette.ml 1.10 644))
(source/lurette.ml (lurette/12_lurette.ml 1.22 644))
(source/lurette.ml (lurette/12_lurette.ml 1.23 644))
(source/graph.mli (lurette/13_graph.mli 1.5 644))
(source/graph.ml (lurette/14_graph.ml 1.3 644))
(source/env.mli (lurette/15_env.mli 1.8 644))
(source/env.ml (lurette/16_env.ml 1.14 644))
(source/env.ml (lurette/16_env.ml 1.15 644))
(source/util.ml (lurette/35_util.ml 1.11 644))
(source/util.ml (lurette/35_util.ml 1.10 644))
(source/solver.mli (lurette/38_solver.mli 1.8 644))
(source/solver.ml (lurette/39_solver.ml 1.12 644))
(source/solver.mli (lurette/38_solver.mli 1.7 644))
(source/solver.ml (lurette/39_solver.ml 1.11 644))
(source/rnumsolver.mli (lurette/b/26_rnumsolver 1.1 644))
(source/rnumsolver.ml (lurette/b/27_rnumsolver 1.1 644))
(source/parse_env.mli (lurette/40_parse_env. 1.3 644))
(source/parse_env.ml (lurette/41_parse_env. 1.4 644))
(source/parse_env.ml (lurette/41_parse_env. 1.5 644))
(source/show_env.mli (lurette/42_show_env.m 1.4 644))
(source/show_env.ml (lurette/43_show_env.m 1.3 644))
(source/formula.mli (lurette/44_formula.ml 1.5 644))
(source/formula.ml (lurette/45_formula.ml 1.6 644))
(source/formula.mli (lurette/44_formula.ml 1.6 644))
(source/formula.ml (lurette/45_formula.ml 1.7 644))
(source/print.mli (lurette/46_print.mli 1.5 644))
(source/print.ml (lurette/47_print.ml 1.7 644))
(source/print.ml (lurette/47_print.ml 1.8 644))
(source/eval.mli (lurette/48_eval.mli 1.4 644))
(source/eval.ml (lurette/49_eval.ml 1.6 644))
(source/eval.mli (lurette/48_eval.mli 1.5 644))
(source/eval.ml (lurette/49_eval.ml 1.7 644))
(source/env_state.mli (lurette/50_env_state. 1.8 644))
(source/env_state.ml (lurette/51_env_state. 1.10 644))
(source/env_state.mli (lurette/50_env_state. 1.9 644))
(source/env_state.ml (lurette/51_env_state. 1.11 644))
(source/wtree.mli (lurette/b/0_wtree.mli 1.5 644))
(source/wtree.ml (lurette/b/1_wtree.ml 1.8 644))
......@@ -64,8 +83,8 @@ when there is a lot of input variables.
(source/gen_stubs.ml (lurette/24_generate_l 1.17 644))
;; Make files
(OcamlMakefile (lurette/17_OcamlMakef 1.17 644))
(Makefile (lurette/18_Makefile 1.20 644))
(OcamlMakefile (lurette/17_OcamlMakef 1.18 644))
(Makefile (lurette/18_Makefile 1.21 644))
(test/Makefile (../Makefile) :symlink)
(interface/Makefile (lurette/25_Makefile 1.6 644))
(make_lurette (lurette/27_make_luret 1.7 744))
......@@ -102,7 +121,7 @@ when there is a lot of input variables.
(test/vrai_tram.c (lurette/b/8_vrai_tram. 1.2 644))
(test/tram_simple.h (lurette/b/25_tram_simpl 1.1 644))
(test/lurette.rif.exp (lurette/b/22_lurette.ri 1.5 644))
(test/lurette.rif.exp (lurette/b/22_lurette.ri 1.6 644))
)
......
......@@ -21,13 +21,11 @@ open Env_state
(****************************************************************************)
(* read_env_state *)
let (read_env_state_one_file : string -> int -> int * node) =
fun file i ->
(** Returns the initial node of the automata defined in [file]
and a counter ([i]) that is used to associate an index to var
names; (returned in the lsh of the pair). Also updates the
various fields of [env_state] with the content of [file].
*)
let (read_env_state_one_file : string -> node) =
fun file ->
(** Returns the initial node of the automata defined in
[file]. Also updates the various fields of [env_state] with the
content of [file]. *)
let
(* Reads the content of [file]. *)
Parse_env.Automata(init_node, list_in, list_out, list_loc,
......@@ -41,21 +39,6 @@ let (read_env_state_one_file : string -> int -> int * node) =
raise e
in
(* Sets the [var_name_to_index] and [index_to_var_name] fields of
[env_state]. Only local and output vars need to indexed. *)
let (update_var_names_indexes : int -> vnt -> int) =
fun i (vn, _) ->
if Hashtbl.mem env_state.var_name_to_index vn then i
else
begin
Hashtbl.add env_state.var_name_to_index vn i;
Hashtbl.add env_state.index_to_var_name i vn ;
(i+1)
end
in
let j = List.fold_left (update_var_names_indexes) i list_out in
let k = List.fold_left (update_var_names_indexes) j list_loc in
(* Sets the [graph] field of [env_state]. *)
let node_nb = (List.length (Graph.get_all_nodes env_state.graph)) in
let (add_arc: Parse_env.read_arc -> unit) =
......@@ -71,17 +54,12 @@ let (read_env_state_one_file : string -> int -> int * node) =
in
List.iter (add_arc) list_arcs ;
(* Sets the [node_to_file_name] field of [env_state].
XXX We could try to find a way to avoid the traversing of
the whole list of nodes for each file here ... *)
(* 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
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);
......@@ -95,35 +73,35 @@ let (read_env_state_one_file : string -> int -> int * node) =
(Util.sort_list_string_pair
(List.append list_pre_form env_state.pre_form)) ;
(k, init_node+node_nb)
(init_node + node_nb)
let (read_env_state_list : string list -> int -> int * node list) =
fun files k ->
let (read_env_state_list : string list -> node list) =
fun files ->
(** Calls [read_env_state_one_file] on a list of files. *)
let (nk, nodes) =
let nodes =
List.fold_left
(fun (i0, nl0) file ->
let (i, n) = read_env_state_one_file file i0 in
(i, n::nl0)
(fun nl0 file ->
let n = read_env_state_one_file file in
(n::nl0)
)
(k, [])
[]
files
in
(nk, (List.rev nodes))
(List.rev nodes)
(* Exported *)
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) =
let nodes =
List.fold_left
(fun (i0, nll0) files ->
let (i, nl) = read_env_state_list files i0 in
(i, nl::nll0)
(fun nll0 files ->
let nl = read_env_state_list files in
(nl::nll0)
)
(1, [])
[]
files_ll
in
(* Sets the [current_nodes], [formula_table], and [wtree_table] fields
......@@ -143,8 +121,8 @@ type sl = subst list
let (solve_formula_list: int -> node list list ->
(node list list * sl * sl) list -> formula list -> var_name list ->
(node list list * sl * sl) list) =
fun p nll acc fl vars_to_gen ->
vnt list -> (node list list * sl * sl) list) =
fun p nll acc fl bool_vars_to_gen num_vnt_to_gen ->
(*
** Returns [p] solutions for the conjunction of formula contained
** in [fl]; a solution is a triple containing (1) the node list [nll],
......@@ -152,7 +130,7 @@ let (solve_formula_list: int -> node list list ->
** (2) a list of substitutions for output vars, and (3) a list of
** substitutions for local vars.
*)
let sl_sl_l = Solver.solve_formula p fl vars_to_gen in
let sl_sl_l = Solver.solve_formula p fl bool_vars_to_gen num_vnt_to_gen in
let nll_sl_sl_l =
(* Adds the target nodes to the substitutions *)
if acc = [] then
......@@ -174,26 +152,37 @@ let (solve_formula_list: int -> node list list ->
let (solve_formula_list_list: int -> node list list * formula list list
-> (node list list * sl * sl) list) =
fun p (nll, fll) ->
let (get_vars_from_node: var_name list -> node -> var_name list) =
fun acc node ->
(* Gets the list of output and local vars of the automata of
which [node] belongs to, and appends it to the accumulator
[acc]. *)
let (get_vars_from_node: (vn list * vnt list) -> node -> (vn list * vnt list)) =
fun (bool_acc, num_acc) node ->
(* 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 (vars, _) = List.split (List.append out loc) in
List.append vars acc
let (bool_vntl, num_vntl) =
List.partition
(fun (vn, vt) -> match vt with BoolT -> true | _ -> false)
(List.append out loc)
in
let (bool_vnl, _) = List.split bool_vntl in
((append bool_acc bool_vnl), (append num_acc num_vntl))
in
let vars_to_gen_ll =
let bvnl_nvntl_l =
(* Var names that should be generated for each group of envts. *)
List.map
(fun nl -> List.fold_left get_vars_from_node [] nl) nll
(fun nl -> List.fold_left get_vars_from_node ([], []) nl) nll
in
let nll_sl_sl_l =
List.fold_left2 (solve_formula_list p nll) [] fll vars_to_gen_ll
let ((bool_vars_to_gen_ll : vn list list),
(num_vnt_to_gen_ll : vnt list list))
=
List.fold_left
(fun (bacc, nacc) (bvnl, nvntl) -> ((append bacc [bvnl]), (append nacc [nvntl])))
([], [])
bvnl_nvntl_l
in
assert (p = (List.length nll_sl_sl_l));
nll_sl_sl_l
Util.list_fold_left3
(solve_formula_list p nll) [] fll bool_vars_to_gen_ll num_vnt_to_gen_ll
let (get_wtrees: node list list -> Wtree.wtree_table -> Wtree.wtree list) =
fun nll wtt ->
......@@ -252,7 +241,7 @@ let (env_try: int -> int -> env_in ->
let fte = Eval.eval_wtree_list input wtl cn_ll in
(* Drawing n formula *)
let nl_fl_ll =
let nl_fl_ll =
map2 (Wtree.choose_n_formula (Solver.is_satisfiable) n fte) cn_ll wtl
in
let nll_fll_l = merge_lll nl_fl_ll in
......
......@@ -25,8 +25,9 @@ type env_stateT = {
mutable var_names: (string, (vnt list * vnt list * vnt list)) Hashtbl.t;
mutable output_var_names: vnt list;
mutable node_to_file_name: (int, string) Hashtbl.t;
mutable var_name_to_index: ((string, int) Hashtbl.t);
mutable index_to_var_name: ((int, string) Hashtbl.t);
mutable atomic_formula_to_index: ((formula, int) Hashtbl.t);
mutable index_to_atomic_formula: ((int, formula) Hashtbl.t);
mutable index_cpt: int;
mutable bdd_tbl: (formula, Bdd.t) Hashtbl.t;
mutable snt: (Bdd.t, Util.sol_nb * Util.sol_nb) Hashtbl.t;
mutable pre_expr: vne list;
......@@ -46,8 +47,9 @@ let (env_state:env_stateT) = {
var_names = Hashtbl.create 0 ;
output_var_names = [];
node_to_file_name = Hashtbl.create 0 ;
var_name_to_index = Hashtbl.create 0 ;
index_to_var_name = Hashtbl.create 0 ;
atomic_formula_to_index = Hashtbl.create 0 ;
index_to_atomic_formula = Hashtbl.create 0 ;
index_cpt = 0 ;
bdd_tbl = Hashtbl.create 0;
snt = Hashtbl.create 3;
pre_expr = [] ;
......@@ -61,28 +63,47 @@ let (env_state:env_stateT) = {
local = []
}
let vn_to_index vn = Hashtbl.find env_state.var_name_to_index vn
let atomic_formula_to_index f =
try Hashtbl.find env_state.atomic_formula_to_index f
with Not_found ->
env_state.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
let index_to_vn i = Hashtbl.find env_state.index_to_var_name i
let index_to_atomic_formula i =
Hashtbl.find env_state.index_to_atomic_formula i
let in_env_unsorted _ =
Hashtbl.fold
(fun _ (x,_,_) acc -> Util.merge x acc)
env_state.var_names
[]
let vnt_list =
Hashtbl.fold
(fun _ (x,_,_) acc -> Util.merge x acc)
env_state.var_names
[]
in
vnt_list
let out_env_unsorted _ =
let out_env_unsorted _ =
let vnt_list =
Hashtbl.fold
(fun _ (_,x,_) acc -> Util.merge x acc)
env_state.var_names
[]
[]
in
vnt_list
let loc_env_unsorted _ =
let loc_env_unsorted _ =
let vnt_list =
Hashtbl.fold
(fun _ (_,_,x) acc -> Util.merge x acc)
env_state.var_names
[]
[]
in
vnt_list
......@@ -15,6 +15,8 @@
open Formula
open Wtree
(* XXX Should be abstract, really. *)
type env_stateT = {
mutable var_names: (string, (vnt list * vnt list * vnt list)) Hashtbl.t;
(** Var names and types ([vnt]) of input, output, and local vars,
......@@ -35,12 +37,14 @@ type env_stateT = {
we need to be able to know what variables are still to be drawn.
*)
mutable var_name_to_index: ((string, int) Hashtbl.t);
mutable atomic_formula_to_index: ((formula, int) Hashtbl.t);
(** This indexing of (output and local) variable names is needed
for constructing bdds in the boolean solver (for which variables
are [int], not [string]s. *)
mutable index_to_var_name: ((int, string) Hashtbl.t);
mutable index_to_atomic_formula: ((int, formula) Hashtbl.t);
(** Ditto in the other way. *)
mutable index_cpt: int;
(** Counter used to create the index *)
mutable bdd_tbl: (formula, Bdd.t) Hashtbl.t;
(** Transforming a formula into a bdd is expensive, therefore
......@@ -92,8 +96,9 @@ val out_env_unsorted : unit -> vnt list
(** Returns all the environement local variables unsorted. *)
val loc_env_unsorted : unit -> vnt list
(** Returns the index of a variable name. *)
val vn_to_index : string -> int
(** Returns the index of an atomic formula, namely, a boolean
variable or an atomic numerical constraint. *)
val atomic_formula_to_index : formula -> int
(** Returns the variable from an index. *)
val index_to_vn : int -> string
(** Returns the atomic formula of an index. *)
val index_to_atomic_formula : int -> formula
......@@ -96,10 +96,15 @@ let rec (eval : formula -> env_in -> formula) =
(Ival(i1), Ival(i2)) -> if (i1 = i2) then True else False
| (Fval(f1), Fval(f2)) ->
if (f1 = f2) then True else False
(* XXX Meaningless with floats ??? *)
| _ -> Eq(ee1, ee2)
)
| Ge(e1, e2) ->
| Neq(e1, e2) ->
(
let ee1 = eval_expr e1 input in
let ee2 = eval_expr e2 input in
Neq(ee1, ee2)
)
| SupEq(e1, e2) ->
(
let ee1 = eval_expr e1 input in
let ee2 = eval_expr e2 input in
......@@ -107,10 +112,9 @@ let rec (eval : formula -> env_in -> formula) =
(Ival(i1), Ival(i2)) -> if (i1 >= i2) then True else False
| (Fval(f1), Fval(f2)) ->
if (f1 >= f2) then True else False
(* XXX Meaningless with floats ??? *)
| _ -> Ge(ee1, ee2)
| _ -> SupEq(ee1, ee2)
)
| G(e1, e2) ->
| Sup(e1, e2) ->
(
let ee1 = eval_expr e1 input in
let ee2 = eval_expr e2 input in
......@@ -118,7 +122,27 @@ let rec (eval : formula -> env_in -> formula) =
(Ival(i1), Ival(i2)) -> if (i1 > i2) then True else False
| (Fval(f1), Fval(f2)) ->
if (f1 > f2) then True else False
| _ -> Ge(ee1, ee2)
| _ -> Sup(ee1, ee2)
)
| InfEq(e1, e2) ->
(
let ee1 = eval_expr e1 input in
let ee2 = eval_expr e2 input in
match (ee1, ee2) with
(Ival(i1), Ival(i2)) -> if (i1 <= i2) then True else False
| (Fval(f1), Fval(f2)) ->
if (f1 <= f2) then True else False
| _ -> InfEq(ee1, ee2)
)
| Inf(e1, e2) ->
(
let ee1 = eval_expr e1 input in
let ee2 = eval_expr e2 input in
match (ee1, ee2) with
(Ival(i1), Ival(i2)) -> if (i1 < i2) then True else False
| (Fval(f1), Fval(f2)) ->
if (f1 < f2) then True else False
| _ -> Inf(ee1, ee2)
)
and
(eval_expr : expr -> env_in -> expr) =
......
......@@ -14,12 +14,11 @@ open Formula
open Wtree
val eval : formula -> env_in -> formula
(**
[eval f input] returns an evaluated version of the formula f. Input
variables (namely, sut outputs) as well as variables ``under a pre''
(in the environment memory) are replaced by their values. Then,
the formula is simplified; e.g., [true and f] is simplified into [f].
*)
(** [eval f input] returns an evaluated version of the formula
f. Input variables (namely, sut outputs) as well as variables
``under a pre'' (in the environment me