Commit 010423f4 authored by Erwan Jahier's avatar Erwan Jahier

lurette 0.23 Thu, 24 Jan 2002 15:14:37 +0100 by jahier

Parent-Version:      0.22
Version-Log:

Add a bdd-based boolean solver to draw inside formula.

Also remove several module opening and use explicit module
qualification instead

lurette.ml:
env_state.ml:
    Define a function in env.ml to get the list of input and outputs var names
    and use it in lurette.ml

env_state.ml:
    Add several fields to the env_state structure:
    * node_to_file_name: to be able to retrieve the list of vars that
      ougth to be generated from a list of nodes (Indeed, some vars
      that should be tossed up 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 variable are still to be drawn).
    * var_name_to_index and index_to_var_name: to index output and local
      variable names. Indeed, the bdd library we use manipulates var as int,
      not string.
    * bdd_tbl: be cause transforming a formula into a bdd is expensive,
      we store the result of this transformation in a table.

    Define the var_names field as an Hashtbl instead of a list for homogeneity.

    Define functions that retrieve the list of input (resp output and local)
    vars from env_state to avois code duplication.

env.ml:
    Initialize the new fields of env_state.

util.ml:
util.mli:
    Add a new function that computes the intersection of 2 lists.

solver.ml:
    Implement a real boolean solver using bdds.

Project-Description: Lurette
parent 6f110b29
......@@ -3,19 +3,19 @@
(Created-By-Prcs-Version 1 3 3)
(test/vrai.h 1120 1006183551 31_vrai.h 1.1)
(doc/ocamldoc.sty 1380 1008328137 b/12_ocamldoc.s 1.1)
(source/env_state.ml 1468 1007648245 51_env_state. 1.3)
(source/env_state.ml 2268 1011881677 51_env_state. 1.4)
(source/graph.ml 2397 1003932490 14_graph.ml 1.2)
(test/tram_env_porte.env 882 1007638809 b/11_tram_env_p 1.2)
(source/util.ml 3869 1008328137 35_util.ml 1.5)
(source/wtree.ml 9186 1008328137 b/1_wtree.ml 1.3)
(source/solver.ml 2091 1007651448 39_solver.ml 1.3)
(source/lurette.ml 8309 1007648245 12_lurette.ml 1.12)
(source/solver.mli 742 1008328137 38_solver.mli 1.3)
(source/util.ml 4248 1011881677 35_util.ml 1.6)
(source/wtree.ml 9221 1011881677 b/1_wtree.ml 1.4)
(source/solver.ml 11173 1011881677 39_solver.ml 1.4)
(source/lurette.ml 8290 1011881677 12_lurette.ml 1.13)
(source/solver.mli 934 1011881677 38_solver.mli 1.4)
(source/env.mli 2524 1008328137 15_env.mli 1.7)
(test/vrai.lus 65 1006182545 28_vrai.lus 1.1)
(lurette.depfull.dot 49 1007651448 b/5_lurette.de 1.2)
(test/tram_env_tramway.env 1228 1007638809 b/10_tram_env_t 1.2)
(source/env.ml 8250 1008328137 16_env.ml 1.10)
(source/env.ml 9609 1011881677 16_env.ml 1.11)
(make_lurette 1027 1007398490 27_make_luret 1.5)
(test/vrai_tram.lus 453 1007379917 b/6_vrai_tram. 1.1)
(test/edge.c 1693 1006263320 32_edge.c 1.1)
......@@ -35,23 +35,23 @@
(test/tram_env_usager.env 826 1007638809 b/9_tram_env_u 1.2)
(TAGS 9825 1007379917 21_TAGS 1.6)
(source/wtree.mli 2860 1008328137 b/0_wtree.mli 1.3)
(source/env_state.mli 996 1008328137 50_env_state. 1.3)
(source/env_state.mli 3216 1011881677 50_env_state. 1.4)
(interface/sut_idl_stub.ml 338 1006263457 34_sut_idl_st 1.1)
(source/eval.mli 1690 1008328137 48_eval.mli 1.3)
(README 0 1002791390 10_README 1.1)
(OcamlMakefile 16584 1008328137 17_OcamlMakef 1.8)
(README 74 1011881677 10_README 1.2)
(OcamlMakefile 16726 1011881677 17_OcamlMakef 1.9)
(source/show_env.ml 3303 1007379917 43_show_env.m 1.1)
(test/tram_simple.c 5627 1006433610 37_tram_simpl 1.1)
(doc/synthese 2556 1007379917 b/2_synthese 1.1)
(interface/Makefile 197 1008255910 25_Makefile 1.6)
(source/show_env.mli 868 1008328137 42_show_env.m 1.2)
(test/tram_simple.h 1746 1006433610 36_tram_simpl 1.1)
(Makefile 1393 1008328137 18_Makefile 1.13)
(Makefile 1601 1011881677 18_Makefile 1.14)
(test/vrai_tram.c 2855 1007379917 b/8_vrai_tram. 1.1)
(source/print.mli 108 1007379917 46_print.mli 1.1)
(source/print.mli 339 1011881677 46_print.mli 1.2)
(source/graph.mli 1340 1008328137 13_graph.mli 1.3)
(source/formula.ml 3109 1008328137 45_formula.ml 1.3)
(test/vrai.c 1405 1006183551 30_vrai.c 1.1)
(source/lurette.mli 397 1008328137 11_lurette.ml 1.9)
(source/print.ml 1599 1008328137 47_print.ml 1.2)
(source/print.ml 2462 1011881677 47_print.ml 1.3)
(test/vrai_tram.h 2293 1007379917 b/7_vrai_tram. 1.1)
LURETTE_DIR = ..
OCAMLMAKEFILE = $(LURETTE_DIR)/OcamlMakefile
# It seems that there is no speed up with those options...
# OCAMLFLAGS = -noassert -unsafe
# It seems that there is no speed up with those options... Give it another try.
# OCAMLFLAGS = -noassert -unsafe -inline 10
-include ./lurette.in
INCDIRS = /home/jahier/include
LIBDIRS = /home/jahier/lib /home/jahier/lib/ocaml
# Requires cudd and mldd to be installed!
LIBS = dd
CLIBS = dd_caml cudd mtr st epd util
SOURCES_C = $(SUT) sut_stub.c sut_idl_stub.idl \
$(ORACLE) oracle_stub.c oracle_idl_stub.idl
......@@ -16,9 +25,9 @@ SOURCES_OCAML = lurette_stub.ml \
$(LURETTE_DIR)/source/env_state.mli $(LURETTE_DIR)/source/env_state.ml \
$(LURETTE_DIR)/source/sim2chro.mli $(LURETTE_DIR)/source/sim2chro.ml \
$(LURETTE_DIR)/source/eval.mli $(LURETTE_DIR)/source/eval.ml \
$(LURETTE_DIR)/source/print.mli $(LURETTE_DIR)/source/print.ml \
$(LURETTE_DIR)/source/solver.mli $(LURETTE_DIR)/source/solver.ml \
$(LURETTE_DIR)/source/wtree.mli $(LURETTE_DIR)/source/wtree.ml \
$(LURETTE_DIR)/source/print.mli $(LURETTE_DIR)/source/print.ml \
$(LURETTE_DIR)/source/parse_env.mli $(LURETTE_DIR)/source/parse_env.ml \
$(LURETTE_DIR)/source/env.mli $(LURETTE_DIR)/source/env.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.8 Fri, 14 Dec 2001 12:08:57 +0100 jahier $
# $Id: OcamlMakefile 1.9 Thu, 24 Jan 2002 15:14:37 +0100 jahier $
#
###########################################################################
......@@ -498,17 +498,20 @@ try:
./lurette 50 10 10 tram_env_porte.env x tram_env_usager.env tram_env_tramway.env
dochtml:
ocamldoc -t "Lurette implementation description" -html -d ../doc/html -stars \
-keep-code -colorize-code -I ../source/ $(SOURCES_OCAML)
ocamldoc -t "Lurette implementation description" -html -d ../doc/html -stars \
-keep-code -colorize-code -I ../source/ $(SOURCES_OCAML) \
../source/gen_stub.mli ../source/gen_stub.ml
doctex:
ocamldoc -t "Lurette implementation description" -latex -d ../doc -stars \
-keep-code -I ../source/ $(SOURCES_OCAML) ; \
-keep-code -I ../source/ $(SOURCES_OCAML) \
../source/gen_stub.mli ../source/gen_stub.ml ; \
pushd ../doc ; latex doc.tex ; popd
docman:
ocamldoc -t "Lurette implementation description" -man -d ../doc/man -stars \
-keep-code -I ../source/ $(SOURCES_OCAML)
ocamldoc -t "Lurette implementation description" -man -d ../doc/man -stars \
-keep-code -I ../source/ $(SOURCES_OCAML) \
../source/gen_stub.mli ../source/gen_stub.ml
###########################################################################
# LOW LEVEL RULES
......
No use of objets nor labels.
No side effect outside of env_state fields.
\ No newline at end of file
;; -*- Prcs -*-
(Created-By-Prcs-Version 1 3 3)
(Project-Description "Lurette")
(Project-Version lurette 0 22)
(Parent-Version lurette 0 21)
(Project-Version lurette 0 23)
(Parent-Version lurette 0 22)
(Version-Log "
Change the comments layout so that ocamldoc is able to process them nicely.")
Add a bdd-based boolean solver to draw inside formula.
Also remove several module opening and use explicit module
qualification instead
lurette.ml:
env_state.ml:
Define a function in env.ml to get the list of input and outputs var names
and use it in lurette.ml
env_state.ml:
Add several fields to the env_state structure:
* node_to_file_name: to be able to retrieve the list of vars that
ougth to be generated from a list of nodes (Indeed, some vars
that should be tossed up 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 variable are still to be drawn).
* var_name_to_index and index_to_var_name: to index output and local
variable names. Indeed, the bdd library we use manipulates var as int,
not string.
* bdd_tbl: be cause transforming a formula into a bdd is expensive,
we store the result of this transformation in a table.
Define the var_names field as an Hashtbl instead of a list for homogeneity.
Define functions that retrieve the list of input (resp output and local)
vars from env_state to avois code duplication.
env.ml:
Initialize the new fields of env_state.
util.ml:
util.mli:
Add a new function that computes the intersection of 2 lists.
solver.ml:
Implement a real boolean solver using bdds.
")
(New-Version-Log "")
(Checkin-Time "Fri, 14 Dec 2001 12:08:57 +0100")
(Checkin-Time "Thu, 24 Jan 2002 15:14:37 +0100")
(Checkin-Login jahier)
(Populate-Ignore ())
(Project-Keywords)
......@@ -18,18 +56,18 @@ Change the comments layout so that ocamldoc is able to process them nicely.")
;; Sources files
(source/lurette.mli (lurette/11_lurette.ml 1.9 644))
(source/lurette.ml (lurette/12_lurette.ml 1.12 644))
(source/lurette.ml (lurette/12_lurette.ml 1.13 644))
(source/graph.mli (lurette/13_graph.mli 1.3 644))
(source/graph.ml (lurette/14_graph.ml 1.2 644))
(source/env.mli (lurette/15_env.mli 1.7 644))
(source/env.ml (lurette/16_env.ml 1.10 644))
(source/env.ml (lurette/16_env.ml 1.11 644))
(source/util.ml (lurette/35_util.ml 1.5 644))
(source/util.ml (lurette/35_util.ml 1.6 644))
(source/solver.mli (lurette/38_solver.mli 1.3 644))
(source/solver.ml (lurette/39_solver.ml 1.3 644))
(source/solver.mli (lurette/38_solver.mli 1.4 644))
(source/solver.ml (lurette/39_solver.ml 1.4 644))
(source/parse_env.mli (lurette/40_parse_env. 1.3 644))
(source/parse_env.ml (lurette/41_parse_env. 1.3 644))
......@@ -40,23 +78,23 @@ Change the comments layout so that ocamldoc is able to process them nicely.")
(source/formula.mli (lurette/44_formula.ml 1.3 644))
(source/formula.ml (lurette/45_formula.ml 1.3 644))
(source/print.mli (lurette/46_print.mli 1.1 644))
(source/print.ml (lurette/47_print.ml 1.2 644))
(source/print.mli (lurette/46_print.mli 1.2 644))
(source/print.ml (lurette/47_print.ml 1.3 644))
(source/eval.mli (lurette/48_eval.mli 1.3 644))
(source/eval.ml (lurette/49_eval.ml 1.2 644))
(source/env_state.mli (lurette/50_env_state. 1.3 644))
(source/env_state.ml (lurette/51_env_state. 1.3 644))
(source/env_state.mli (lurette/50_env_state. 1.4 644))
(source/env_state.ml (lurette/51_env_state. 1.4 644))
(source/wtree.mli (lurette/b/0_wtree.mli 1.3 644))
(source/wtree.ml (lurette/b/1_wtree.ml 1.3 644))
(source/wtree.ml (lurette/b/1_wtree.ml 1.4 644))
(source/gen_stubs.ml (lurette/24_generate_l 1.13 644))
;; Make files
(OcamlMakefile (lurette/17_OcamlMakef 1.8 644))
(Makefile (lurette/18_Makefile 1.13 644))
(OcamlMakefile (lurette/17_OcamlMakef 1.9 644))
(Makefile (lurette/18_Makefile 1.14 644))
(test/Makefile (../Makefile) :symlink)
(interface/Makefile (lurette/25_Makefile 1.6 644))
(make_lurette (lurette/27_make_luret 1.5 744))
......@@ -71,7 +109,7 @@ Change the comments layout so that ocamldoc is able to process them nicely.")
(doc/ocamldoc.hva (lurette/b/13_ocamldoc.h 1.1 644))
;; Misc
(README (lurette/10_README 1.1 644))
(README (lurette/10_README 1.2 644))
(ID_EN_VRAC (lurette/0_ID_EN_VRAC 1.1 644))
(lurette.dep.dot (lurette/b/4_lurette.de 1.2 644))
(lurette.depfull.dot (lurette/b/5_lurette.de 1.2 644))
......
......@@ -11,228 +11,271 @@
(****************************************************************************)
open Lurette_stub
open Graph
open List
open Util
open Formula
open Env_state
open Parse_env
open Wtree
(****************************************************************************)
(****************************************************************************)
(* read_env_state *)
let (read_env_state_one_file : string -> node) =
fun file ->
(*
** returns the initial node of the automata defined in `file'.
** Also updates the global variable `env_state'.
*)
let cpt = (List.length (get_all_nodes env_state.graph)) in
let Automata(init_node, list_in, list_out, list_loc, list_pre_expr,
list_pre_form, list_arcs) =
try Parse_env.parse_automata(lexer(Stream.of_channel (open_in file)))
with _ -> failwith "*** Error while parsing the environment file.\n"
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
(* Reads the content of [file]. *)
Parse_env.Automata(init_node, list_in, list_out, list_loc,
list_pre_expr, list_pre_form, list_arcs) =
try
Parse_env.parse_automata(
Parse_env.lexer(Stream.of_channel (open_in file)))
with _ ->
failwith ("*** Error while parsing the environment file " ^ file ^ "\n")
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 (add_arc: read_arc -> unit) =
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) =
fun arc ->
match arc with
Arc(node_from, arc_info, node_to) ->
Parse_env.Arc(node_from, arc_info, node_to) ->
(Graph.add_trans
env_state.graph
(node_from+cpt)
(node_from+node_nb)
arc_info
(node_to+cpt))
(node_to+node_nb))
in
List.iter (add_arc) list_arcs ;
env_state.var_names <- (file, (list_in, list_out, list_loc))::env_state.var_names ;
env_state.pre_expr <- (Util.sort_list_string_pair (List.append list_pre_expr env_state.pre_expr)) ;
env_state.pre_form <- (Util.sort_list_string_pair (List.append list_pre_form env_state.pre_form)) ;
(init_node+cpt)
(* 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 ... *)
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);
(* Sets the [var_names], [pre_expr], and [pre_form] fields
of [env_state]. *)
Hashtbl.add env_state.var_names file (list_in, list_out, list_loc) ;
env_state.pre_expr <-
(Util.sort_list_string_pair
(List.append list_pre_expr env_state.pre_expr)) ;
env_state.pre_form <-
(Util.sort_list_string_pair
(List.append list_pre_form env_state.pre_form)) ;
(k, init_node+node_nb)
let (read_env_state_list : string list -> node list) =
fun files_l ->
List.map (read_env_state_one_file) files_l
let (read_env_state_list : string list -> int -> int * node list) =
fun files k ->
(** Calls [read_env_state_one_file] on a list of files. *)
let (nk, nodes) =
List.fold_left
(fun (i0, nl0) file ->
let (i, n) = read_env_state_one_file file i0 in
(i, n::nl0)
)
(k, [])
files
in
(nk, (List.rev nodes))
(* Exported *)
let (read_env_state : string list list -> unit) =
fun files_ll ->
(*
** Updates the global variable `env_state' using the automata defined
** in the list of list `files_ll'. The idea behind having a list of list
** there is that automata given in inner lists should be run as a product,
** and outter ones should be run in parallel.
** For example, (read_env_state [["foo1"; "foo2"]; ["foo3"]]) means that
** the automata given in `foo1' and `foo2' are run as if their automata
** were multiplied (in the classical sense of the automata product),
** and `foo3' is run in parallel. Of course, `foo3' should not share any
** variables with `foo1' and `foo2'.
*)
env_state.current_nodes <- List.map (read_env_state_list) files_ll ;
env_state.formula_table <- (build_formula_table env_state.graph);
env_state.wtree_table <- (build_wtree_table env_state.graph)
(** Calls [read_env_state_one_file] on a list of list of files. *)
let (_, nodes) =
List.fold_left
(fun (i0, nll0) files ->
let (i, nl) = read_env_state_list files i0 in
(i, nl::nll0)
)
(1, [])
files_ll
in
(* Sets the [current_nodes], [formula_table], and [wtree_table] fields
of [env_state]. *)
env_state.current_nodes <- nodes ;
env_state.formula_table <- (Wtree.build_formula_table env_state.graph);
env_state.wtree_table <- (Wtree.build_wtree_table env_state.graph)
(****************************************************************************)
(****************************************************************************)
(* env_try *)
type nl = node list
type nl = node list
type nll = node list list
type sl = subst list
(* type output = node list list * subst list * env_loc *)
type sl = subst list
let (tuplise_env_outputs: node list list * subst list * env_loc ->
node list list * env_out * env_loc) =
(*
** The environement provides a list of substitution whereas lurette
** expects tuples of values, where the different variable values are
** sorted lexicographically w.r.t. their names. E.g.,
** (tuplise_env_outputs ([], [("b", Bool(true)); ("a", Int(1))], [])
** = ([], (1, true), []))
*)
(** The environement provides a list of substitution whereas
lurette expects tuples of values, where the different variable
values are sorted lexicographically w.r.t. their names. The
transation is done by this function. E.g., [(tuplise_env_outputs
([], [("b", Bool(true)); ("a", Int(1))], []) = ([], (1, true),
[]))].
*)
fun (nl, sl, loc) ->
(*
** Sorts substitutions lexicographically w.r.t. to var names.
*)
let (sort_subst: subst list -> subst list) =
fun list ->
(* Sorts substitutions lexicographically w.r.t. to var names. *)
List.sort (fun (n1, v1) (n2, v2) -> compare n1 n2) list
in
let (project_2: subst list -> atomic_expr list) =
(*
** Removes var names from the subst.
*)
List.map (fun (n, v) -> v)
in
(nl, (list_ae_to_sut_in (project_2 (sort_subst sl))), loc)
let (_, vals) = List.split (sort_subst sl) in
(nl, (Lurette_stub.list_ae_to_sut_in vals), loc)
let (env_try : int -> int -> sut_out -> (node list list * sut_in * env_loc) list) =
(*
** [env_try n p input] returns a list of `n*p' possible outputs of the
** environment with input `input'. This function actually returns a list
** of 3-tuple `node list list * env_out * env_loc' because we need to know
** which arcs produced which outputs later (namely, when performing an
** `env_step').
**
** Also sets (side effect) the environment input values to `input'.
*)
fun n p input ->
let (solve_formula_list: int -> node list list -> (node list list * sl * sl) list ->
formula list -> (node list list * sl * sl) list) =
fun p nll acc fl ->
(*
** returns `p' solutions for the conjunction of formula contained
** in `fl'; a solution is a triple containing (1) the node list `nll',
** which is the target node corresponding to the formula in `ft'
** (2) a list od substitutions for outputs vars, and (3) a list of
** substitutions for local vars.
*)
let sl_sl_l = Solver.solve_formula p fl in
if acc = [] then
(List.map
(fun (sl1, sl2) ->
(nll, sl1, sl2))
sl_sl_l
)
else
(List.map2
(fun (sl1, sl2) (nll, sl1_acc, sl2_acc) ->
(nll, (append sl1 sl1_acc), (append sl2 sl2_acc)))
sl_sl_l
acc
)
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 ->
(*
** Returns [p] solutions for the conjunction of formula contained
** in [fl]; a solution is a triple containing (1) the node list [nll],
** which are the target nodes corresponding to the formula in [fl]
** (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 in
if acc = [] then
(List.map
(fun (sl1, sl2) ->
(nll, sl1, sl2))
sl_sl_l
)
else
(List.map2
(fun (sl1, sl2) (nll, sl1_acc, sl2_acc) ->
(nll, (append sl1 sl1_acc), (append sl2 sl2_acc)))
sl_sl_l
acc
)
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 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
in
let (solve_formula_list_list: int -> node list list * formula list list
-> (node list list * sl * sl) list) =
fun p (nll, fll) ->
let nll_sl_sl_l = List.fold_left (solve_formula_list p nll) [] fll in
let _ = assert (p = (List.length nll_sl_sl_l)) in
nll_sl_sl_l
let vars_to_gen_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
in
let (get_wtrees: node list list -> wtree_table -> wtree list) =
fun nll wtt ->
(*
** Get the wtrees corresponding to the list of list of nodes nll,
** and then multiply the wtrees in the inner lists. E.g., the list
** [[n1; n2], [n3]] leads to the list of list of wtrees [[t1;t2];[t3]]
** which is transformed into [t1 x t2; t3], where `x' is the wtree
** product.
*)
let wtll = map (map (Hashtbl.find wtt)) nll in
map (fun nl -> fold_left (wtree_product) (hd nl) (tl nl))
wtll
let nll_sl_sl_l =
List.fold_left2 (solve_formula_list p nll) [] fll vars_to_gen_l
in
assert (p = (List.length nll_sl_sl_l));
nll_sl_sl_l
let (get_wtrees: node list list -> Wtree.wtree_table -> Wtree.wtree list) =
fun nll wtt ->
(** Get the wtrees corresponding to the list of list of nodes
[nll], and then multiply the wtrees in the inner
lists. E.g., the list [[[n1; n2]; [n3]]] leads to the list
of list of wtrees [[[t1; t2]; [t3]]] which is transformed
into [[t1 x t2; t3]], where [x] is the wtree product. *)
let wtll = map (map (Hashtbl.find wtt)) nll in
map (fun nl -> fold_left (Wtree.wtree_product) (hd nl) (tl nl)) wtll
let (merge_lll: ('a list * 'f list) list list ->
('a list list * 'f list list) list) =
fun nl_fl_ll ->
(*
** distributes the last `l' of `nl_fl_ll' over `nl' and `fl'
*)
match nl_fl_ll with
[] -> assert false
| nl_fl_l0::nl_fl_ll_tail ->
let nll_fll_l0 =
map (fun (nl0, fl0) -> ([nl0], [fl0])) nl_fl_l0
in
(fold_left
(fun nll_fll_l nl_fl_l ->
(map2
(fun (nl, fl) (nll, fll) -> (nl::nll, fl::fll))
nl_fl_l
nll_fll_l
)
)
nll_fll_l0
nl_fl_ll_tail)
let (merge_lll: ('a list * 'f list) list list ->
('a list list * 'f list list) list) =
fun nl_fl_ll ->
(* Distributes the last ``[l]'' of [nl_fl_ll] over [nl] and [fl]. *)
match nl_fl_ll with
[] -> assert false
| nl_fl_l0::nl_fl_ll_tail ->
let nll_fll_l0 =
map (fun (nl0, fl0) -> ([nl0], [fl0])) nl_fl_l0
in
(fold_left
(fun nll_fll_l nl_fl_l ->
(map2
(fun (nl, fl) (nll, fll) -> (nl::nll, fl::fll))
nl_fl_l
nll_fll_l
)
)
nll_fll_l0
nl_fl_ll_tail)
in
let _ = assert (
(* n = 2, env1 x env2 env3 *)
(merge_lll
[[([1;2], [Bvar("a");Bvar("b")]);
([4;5], [Bvar("d");Bvar("e")])];
[([3], [Bvar("c")]);
([6], [Bvar("f")])]])
=