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

lurette 0.25 Wed, 06 Feb 2002 13:48:27 +0100 by jahier

Parent-Version:      0.24
Version-Log:

command_line.ml,mli: (New files)
lurette.ml:
        Handle options at the lurette command line.

        Give better error messages.

Project-Description: Lurette
parent eb46e24b
...@@ -3,12 +3,13 @@ ...@@ -3,12 +3,13 @@
(Created-By-Prcs-Version 1 3 3) (Created-By-Prcs-Version 1 3 3)
(test/usager.env 392 1012914629 b/14_usager.env 1.1) (test/usager.env 392 1012914629 b/14_usager.env 1.1)
(doc/ocamldoc.sty 1380 1008328137 b/12_ocamldoc.s 1.1) (doc/ocamldoc.sty 1380 1008328137 b/12_ocamldoc.s 1.1)
(source/env_state.ml 2347 1012914629 51_env_state. 1.5) (source/env_state.ml 2183 1012999707 51_env_state. 1.6)
(source/graph.ml 2476 1012914629 14_graph.ml 1.3) (source/graph.ml 2476 1012914629 14_graph.ml 1.3)
(source/util.ml 4248 1011881677 35_util.ml 1.6) (source/util.ml 4248 1011881677 35_util.ml 1.6)
(source/wtree.ml 9831 1012914629 b/1_wtree.ml 1.5) (source/wtree.ml 9831 1012914629 b/1_wtree.ml 1.5)
(source/solver.ml 11387 1012914629 39_solver.ml 1.5) (source/solver.ml 11388 1012999707 39_solver.ml 1.6)
(source/lurette.ml 8437 1012914629 12_lurette.ml 1.14) (source/command_line.ml 3650 1012999707 b/20_command_li 1.1)
(source/lurette.ml 9264 1012999707 12_lurette.ml 1.15)
(source/solver.mli 971 1012914629 38_solver.mli 1.5) (source/solver.mli 971 1012914629 38_solver.mli 1.5)
(source/env.mli 2524 1008328137 15_env.mli 1.7) (source/env.mli 2524 1008328137 15_env.mli 1.7)
(lurette.depfull.dot 49 1007651448 b/5_lurette.de 1.2) (lurette.depfull.dot 49 1007651448 b/5_lurette.de 1.2)
...@@ -28,6 +29,7 @@ ...@@ -28,6 +29,7 @@
(doc/Interface_draft 5232 1003928781 19_Interface_ 1.1) (doc/Interface_draft 5232 1003928781 19_Interface_ 1.1)
(doc/ocamldoc.hva 313 1008328137 b/13_ocamldoc.h 1.1) (doc/ocamldoc.hva 313 1008328137 b/13_ocamldoc.h 1.1)
(source/formula.mli 1693 1008328137 44_formula.ml 1.3) (source/formula.mli 1693 1008328137 44_formula.ml 1.3)
(source/command_line.mli 1154 1012999707 b/21_command_li 1.1)
(TAGS 9825 1007379917 21_TAGS 1.6) (TAGS 9825 1007379917 21_TAGS 1.6)
(source/wtree.mli 2860 1008328137 b/0_wtree.mli 1.3) (source/wtree.mli 2860 1008328137 b/0_wtree.mli 1.3)
(source/env_state.mli 3229 1012914629 50_env_state. 1.5) (source/env_state.mli 3229 1012914629 50_env_state. 1.5)
...@@ -35,15 +37,15 @@ ...@@ -35,15 +37,15 @@
(interface/sut_idl_stub.ml 338 1006263457 34_sut_idl_st 1.1) (interface/sut_idl_stub.ml 338 1006263457 34_sut_idl_st 1.1)
(source/eval.mli 1690 1008328137 48_eval.mli 1.3) (source/eval.mli 1690 1008328137 48_eval.mli 1.3)
(README 74 1011881677 10_README 1.2) (README 74 1011881677 10_README 1.2)
(OcamlMakefile 16807 1012914629 17_OcamlMakef 1.10)
(test/ControleurPorte.c 9407 1012914629 b/19_Controleur 1.1) (test/ControleurPorte.c 9407 1012914629 b/19_Controleur 1.1)
(OcamlMakefile 16807 1012914629 17_OcamlMakef 1.10)
(source/show_env.ml 3303 1007379917 43_show_env.m 1.1) (source/show_env.ml 3303 1007379917 43_show_env.m 1.1)
(test/tram.env 806 1012914629 b/15_tram.env 1.1) (test/tram.env 806 1012914629 b/15_tram.env 1.1)
(doc/synthese 2556 1007379917 b/2_synthese 1.1) (doc/synthese 2556 1007379917 b/2_synthese 1.1)
(test/ControleurPorte.h 2306 1012914629 b/18_Controleur 1.1) (test/ControleurPorte.h 2306 1012914629 b/18_Controleur 1.1)
(interface/Makefile 197 1008255910 25_Makefile 1.6) (interface/Makefile 197 1008255910 25_Makefile 1.6)
(source/show_env.mli 868 1008328137 42_show_env.m 1.2) (source/show_env.mli 868 1008328137 42_show_env.m 1.2)
(Makefile 1603 1012914629 18_Makefile 1.15) (Makefile 1692 1012999707 18_Makefile 1.16)
(test/vrai_tram.c 3060 1012914629 b/8_vrai_tram. 1.2) (test/vrai_tram.c 3060 1012914629 b/8_vrai_tram. 1.2)
(source/print.mli 412 1012914629 46_print.mli 1.3) (source/print.mli 412 1012914629 46_print.mli 1.3)
(source/graph.mli 1417 1012914629 13_graph.mli 1.4) (source/graph.mli 1417 1012914629 13_graph.mli 1.4)
......
...@@ -31,6 +31,7 @@ SOURCES_OCAML = lurette_stub.ml \ ...@@ -31,6 +31,7 @@ SOURCES_OCAML = lurette_stub.ml \
$(LURETTE_DIR)/source/parse_env.mli $(LURETTE_DIR)/source/parse_env.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/env.mli $(LURETTE_DIR)/source/env.ml \
$(LURETTE_DIR)/source/show_env.mli $(LURETTE_DIR)/source/show_env.ml \ $(LURETTE_DIR)/source/show_env.mli $(LURETTE_DIR)/source/show_env.ml \
$(LURETTE_DIR)/source/command_line.mli $(LURETTE_DIR)/source/command_line.ml \
$(LURETTE_DIR)/source/lurette.mli $(LURETTE_DIR)/source/lurette.ml $(LURETTE_DIR)/source/lurette.mli $(LURETTE_DIR)/source/lurette.ml
SOURCES = $(SOURCES_C) \ SOURCES = $(SOURCES_C) \
......
;; -*- Prcs -*- ;; -*- Prcs -*-
(Created-By-Prcs-Version 1 3 3) (Created-By-Prcs-Version 1 3 3)
(Project-Description "Lurette") (Project-Description "Lurette")
(Project-Version lurette 0 24) (Project-Version lurette 0 25)
(Parent-Version lurette 0 23) (Parent-Version lurette 0 24)
(Version-Log " (Version-Log "
Make the examples of Yvan work. Fix a bunch of bugs alonf the way... command_line.ml,mli: (New files)
lurette.ml:
Handle options at the lurette command line.
Give better error messages.
") ")
(New-Version-Log "") (New-Version-Log "")
(Checkin-Time "Tue, 05 Feb 2002 14:10:29 +0100") (Checkin-Time "Wed, 06 Feb 2002 13:48:27 +0100")
(Checkin-Login jahier) (Checkin-Login jahier)
(Populate-Ignore ()) (Populate-Ignore ())
(Project-Keywords) (Project-Keywords)
...@@ -21,7 +23,7 @@ Make the examples of Yvan work. Fix a bunch of bugs alonf the way... ...@@ -21,7 +23,7 @@ Make the examples of Yvan work. Fix a bunch of bugs alonf the way...
;; Sources files ;; Sources files
(source/lurette.mli (lurette/11_lurette.ml 1.10 644)) (source/lurette.mli (lurette/11_lurette.ml 1.10 644))
(source/lurette.ml (lurette/12_lurette.ml 1.14 644)) (source/lurette.ml (lurette/12_lurette.ml 1.15 644))
(source/graph.mli (lurette/13_graph.mli 1.4 644)) (source/graph.mli (lurette/13_graph.mli 1.4 644))
(source/graph.ml (lurette/14_graph.ml 1.3 644)) (source/graph.ml (lurette/14_graph.ml 1.3 644))
...@@ -32,7 +34,7 @@ Make the examples of Yvan work. Fix a bunch of bugs alonf the way... ...@@ -32,7 +34,7 @@ Make the examples of Yvan work. Fix a bunch of bugs alonf the way...
(source/util.ml (lurette/35_util.ml 1.6 644)) (source/util.ml (lurette/35_util.ml 1.6 644))
(source/solver.mli (lurette/38_solver.mli 1.5 644)) (source/solver.mli (lurette/38_solver.mli 1.5 644))
(source/solver.ml (lurette/39_solver.ml 1.5 644)) (source/solver.ml (lurette/39_solver.ml 1.6 644))
(source/parse_env.mli (lurette/40_parse_env. 1.3 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.4 644))
...@@ -50,16 +52,19 @@ Make the examples of Yvan work. Fix a bunch of bugs alonf the way... ...@@ -50,16 +52,19 @@ Make the examples of Yvan work. Fix a bunch of bugs alonf the way...
(source/eval.ml (lurette/49_eval.ml 1.3 644)) (source/eval.ml (lurette/49_eval.ml 1.3 644))
(source/env_state.mli (lurette/50_env_state. 1.5 644)) (source/env_state.mli (lurette/50_env_state. 1.5 644))
(source/env_state.ml (lurette/51_env_state. 1.5 644)) (source/env_state.ml (lurette/51_env_state. 1.6 644))
(source/wtree.mli (lurette/b/0_wtree.mli 1.3 644)) (source/wtree.mli (lurette/b/0_wtree.mli 1.3 644))
(source/wtree.ml (lurette/b/1_wtree.ml 1.5 644)) (source/wtree.ml (lurette/b/1_wtree.ml 1.5 644))
(source/command_line.ml (lurette/b/20_command_li 1.1 644))
(source/command_line.mli (lurette/b/21_command_li 1.1 644))
(source/gen_stubs.ml (lurette/24_generate_l 1.13 644)) (source/gen_stubs.ml (lurette/24_generate_l 1.13 644))
;; Make files ;; Make files
(OcamlMakefile (lurette/17_OcamlMakef 1.10 644)) (OcamlMakefile (lurette/17_OcamlMakef 1.10 644))
(Makefile (lurette/18_Makefile 1.15 644)) (Makefile (lurette/18_Makefile 1.16 644))
(test/Makefile (../Makefile) :symlink) (test/Makefile (../Makefile) :symlink)
(interface/Makefile (lurette/25_Makefile 1.6 644)) (interface/Makefile (lurette/25_Makefile 1.6 644))
(make_lurette (lurette/27_make_luret 1.6 744)) (make_lurette (lurette/27_make_luret 1.6 744))
......
(*-----------------------------------------------------------------------
** Copyright (C) 2001 - Verimag.
** This file may only be copied under the terms of the GNU Library General
** Public License
**-----------------------------------------------------------------------
**
** File: command_line.ml
** Main author: jahier@imag.fr
*)
type optionsT = {
mutable step_by_step : bool ;
mutable display_local_var : bool ;
mutable display_sim2chro : bool ;
mutable cudd_heap_init : int
}
type cmd_line_optionT =
Step | NoStep
| DisplayLocalVar | NoDisplayLocalVar
| Sim2chro | NoSim2chro
| CuddHeapInit
(* Names of the command line options to override the defaults. *)
let (string_to_option: (string * cmd_line_optionT) list) = [
("--no-step", NoStep);
("--step", Step);
("-s", Step);
("--display-local-var", DisplayLocalVar);
("--do-not-display-local-var", NoDisplayLocalVar);
("-nlv", NoDisplayLocalVar);
("--call-sim2chro", Sim2chro);
("--do-not-call-sim2chro", NoSim2chro);
("-ns2c", NoSim2chro);
("--init-cudd-heap", CuddHeapInit)
]
let (option_to_usage: cmd_line_optionT -> string) =
fun opt ->
match opt with
Step -> "Run lurette step by step.\n"
| NoStep -> "Do not run lurette step by step (Default).\n"
| DisplayLocalVar -> "Display environment local variables in sim2chro (Default).\n"
| NoDisplayLocalVar -> "Do not display environment local variables in sim2chro.\n"
| Sim2chro -> "Call sim2chro when lurette resumes (Default).\n"
| NoSim2chro -> "Do not call sim2chro when lurette resumes.\n"
| CuddHeapInit -> "Sets a magic number (related to the gc) that is used by mldd \n\t\t\tfor initializing Dd (Default is 20).\n"
let (group_common_options: (string * cmd_line_optionT) list ->
(string * cmd_line_optionT) list) =
fun list ->
List.fold_left
(fun acc (str, opt) ->
match acc with
(str2, opt2)::tail ->
if
(opt = opt2)
then
(((str2 ^ "\n\t\t" ^ str), opt)::tail)
else
((str, opt)::(str2, opt2)::tail)
| [] -> [(str, opt)]
)
[]
list
let usage_options =
List.fold_left
(fun acc (str, opt) -> acc ^ "\n\t\t" ^ str ^ "\n\t\t\t" ^ (option_to_usage opt))
""
(List.rev (group_common_options string_to_option))
let usage =
("\n\nusage: ./lurette length n p [options]* <file>.env ([x] <file>.env)* \n" ^
" where: \n\t o `length' is the number of steps that will be run " ^
"\n\t o `n' is the number of formula that are drawn at each step" ^
"\n\t o `p' is the number of solutions that are drawn in each formula" ^
"\n\t (resulting in a test ``thickness'' of n*p) " ^
"\n\t o `<file>.env' contains an environment automata. Environments " ^
"\n\t separated by `x' will executed as if their automata where " ^
"\n\t multiplied (necessary if they have common output variables).\n " ^
"\n\t o `options' is a list of options. The available options are: " ^
usage_options ^ "\n\n" ^
"Example: ./lurette 1000 3 4 env1.env x env2.env x env3.env env4\n\t" ^
"will run during 1000 steps; at each step, it will draw 3 formula in the \n\t" ^
"automata, and it will draw 4 times in each formula (leading to a thickness of 12). \n\t" ^
"The environment `env1', `env2', and `env3' will be run as a product, \n\t" ^
"and `env4' in parallel.\n\n ")
let cmd_line_string_to_int str errmsg =
try
(int_of_string str)
with Failure("int_of_string")
->
print_string usage ;
print_string errmsg ;
flush stdout ;
failwith "\n *** Error when calling lurette.\n"
(*-----------------------------------------------------------------------
** Copyright (C) 2001 - Verimag.
** This file may only be copied under the terms of the GNU Library General
** Public License
**-----------------------------------------------------------------------
**
** File: command_line.mli
** Main author: jahier@imag.fr
*)
(** Handles everything that is related to command line lurette calls:
printing lurette usage message, handling command line options, etc.
*)
type optionsT = {
mutable step_by_step : bool ;
mutable display_local_var : bool ;
mutable display_sim2chro : bool ;
mutable cudd_heap_init : int
}
val usage : string
(** Usage message to be printed if an error occur when lurette is called. *)
val cmd_line_string_to_int : string -> string -> int
(** [cmd_line_string_to_int str errmsg] converts a string (of the
command line) into an integer, and prints [errmsg] before aborting if
the convertion failed.
*)
type cmd_line_optionT =
Step | NoStep
| DisplayLocalVar | NoDisplayLocalVar
| Sim2chro | NoSim2chro
| CuddHeapInit
val string_to_option: (string * cmd_line_optionT) list
(** XXX *)
...@@ -40,11 +40,6 @@ type env_stateT = { ...@@ -40,11 +40,6 @@ type env_stateT = {
mutable local : env_loc mutable local : env_loc
} }
(* Initializing Bdd libs.
XXX Where should I do that ?
55 marche le mieux avec la passerelle. bertrand dit entre 20 et 30...
*)
let _ = Dd.initialize 0 55
let (env_state:env_stateT) = { let (env_state:env_stateT) = {
......
...@@ -14,12 +14,19 @@ open Util ...@@ -14,12 +14,19 @@ open Util
open Formula open Formula
open Env_state open Env_state
open List open List
open Command_line
(*------------------------------------------------------------------------*)
let (options:Command_line.optionsT) = {
step_by_step = false ;
display_local_var = true ;
display_sim2chro = true ;
cudd_heap_init = 20
}
(* XXX set those via an option at command the line !!! *)
let step_by_step = false
let display_local_var = true
let print_vntl vl = let print_vntl vl =
List.iter List.iter
(fun (v, t) -> print_string ("\n " ^ v ^ " of type " ^ t ^ ",")) (fun (v, t) -> print_string ("\n " ^ v ^ " of type " ^ t ^ ","))
...@@ -87,60 +94,87 @@ let (read_var_names: string -> vnt list * vnt list) = ...@@ -87,60 +94,87 @@ let (read_var_names: string -> vnt list * vnt list) =
let arg_nb = (Array.length Sys.argv) let arg_nb = (Array.length Sys.argv)
let usage =
("\n\nusage: lurette s n p env_list \n" ^
" where: \n\t - `s' is the test length " ^
"\n\t - `n' is the number of formula that are drawn at each step" ^
"\n\t - `p' is the number of solutions that are drawn for each " ^
"\n\t formula (thus resulting in a test ``thickness'' of n*p) " ^
"\n\t - `env_list' is a non empty sequence of .env files, possibly" ^
"\n\t separated by the character `x'; environments separated by `x'" ^
"\n\t will executed as if their automata where multiplied.\n " ^
"\n For example, `lurette 1000 3 3 env1 x env2 x env3 env4' will run " ^
"\n`env1', `env2', and `env3' as a product, and `env4' in parallel.\n\n ")
let rec (main : unit -> 'a) = let rec (main : unit -> 'a) =
fun _ -> fun _ ->
if (arg_nb < 5) then print_string usage try
else if (arg_nb < 5) then print_string usage
let s = int_of_string Sys.argv.(1) in else
let n = int_of_string Sys.argv.(2) in let s = (cmd_line_string_to_int Sys.argv.(1)
let p = int_of_string Sys.argv.(3) in "*** int expected as first argument." )
let res = main2 s n p in and n = (cmd_line_string_to_int Sys.argv.(2)
let _ = "*** int expected as second argument." )
if not step_by_step then ( and p = (cmd_line_string_to_int Sys.argv.(3)
Sim2chro.call_sim2chro () "*** int expected as third argument." )
) in
else () let res = main2 s n p in
in if (not options.step_by_step && options.display_sim2chro)
res then Sim2chro.call_sim2chro ()
else () ;
res
with
Failure(errmsg) -> print_string errmsg
| e -> raise e
and
(get_lurette_options: int -> int) =
fun n ->
try
begin
let opt = List.assoc Sys.argv.(n) Command_line.string_to_option in
match opt with
Step -> options.step_by_step <- true ; (n+1)
| NoStep -> options.step_by_step <- false ; (n+1)
| DisplayLocalVar -> options.display_local_var <- true ; (n+1)
| NoDisplayLocalVar -> options.display_local_var <- false ; (n+1)
| Sim2chro -> options.display_sim2chro <- true ; (n+1)
| NoSim2chro -> options.display_sim2chro <- false ; (n+1)
| CuddHeapInit ->
let str = (Sys.argv.(n+1)) in
cmd_line_string_to_int str
("*** Error when calling lurette: an " ^
"integer is expected after the " ^
"option --init-cudd-heap\n") ;
end
with Not_found -> n
and and
(get_env_from_args: int -> string list list -> string list list) = (get_env_from_args: int -> string list list -> string list list) =
fun n file_ll -> fun n file_ll ->
(** put the environment file names given at top-level into a list (** Returns the environment file names given at top-level into a
of list. e.g., if the call `lurette 10 2 3 env1 x env2 x env3 list of list. E.g., if the call [lurette 10 2 3 env1 x env2 x
env4' is done, then `get_env_from_args 10 []' (where 10 is the env3 env4] is done, then [get_env_from_args 10 []] (where 10 is
arg nb) returns `[["env1"; "env2"; "env3"]; ["env4"]]'. the arg nb) returns [[["env1"; "env2"; "env3"]; ["env4"]]].
*)
if (n = 3) then file_ll Also set the lurette command line options if any.
*)
if (n = arg_nb) then file_ll
else else
let arg = Sys.argv.(n) in let m = get_lurette_options n in
if (arg = "x") then (* m > n iff Sys.argv.(n) is an option *)
match file_ll with if
sl::sll -> (m > n)
let env = Sys.argv.(n-1) in then
get_env_from_args (n-2) ((env::sl)::sll) get_env_from_args m file_ll
| [] -> assert false
else else
get_env_from_args (n-1) ([arg]::file_ll) let arg = Sys.argv.(m) in
if
(arg = "x")
then
match file_ll with
sl::sll ->
let env = Sys.argv.(n+1) in
get_env_from_args (n+2) ((env::sl)::sll)
| [] -> assert false
else
get_env_from_args (n+1) ([arg]::file_ll)
and and
(main2 : int -> int -> int -> 'a) = (main2 : int -> int -> int -> 'a) =
fun s n p -> fun s n p ->
(* Initialisation of `Env_state.env_state' *) (* Initialisation of `Env_state.env_state' *)
let () = Env.read_env_state (get_env_from_args (arg_nb-1) []) in let env_llist = (get_env_from_args 4 []) in
let () = Env.read_env_state env_llist in
let _ = Sys.command "touch lurette.rif; rm lurette.rif;" in let _ = Sys.command "touch lurette.rif; rm lurette.rif;" in
let rif = open_out "lurette.rif" in let rif = open_out "lurette.rif" in
...@@ -168,16 +202,17 @@ and ...@@ -168,16 +202,17 @@ and
var_decl_are_inconsistent Lurette_stub.sut_input_var_name_and_type_list var_decl_are_inconsistent Lurette_stub.sut_input_var_name_and_type_list
Lurette_stub.sut_output_var_name_and_type_list; Lurette_stub.sut_output_var_name_and_type_list;
if step_by_step then ( if options.step_by_step then (
Show_env.generate_env_graph [] "environment" ; Show_env.generate_env_graph [] "environment" ;
Show_env.gv ("environment.ps"); Show_env.gv ("environment.ps");
Sim2chro.put_var_decl stdout display_local_var; Sim2chro.put_var_decl stdout options.display_local_var;
) )
else Sim2chro.put_var_decl rif display_local_var; else Sim2chro.put_var_decl rif options.display_local_var;
(* Initializing Dd (bdd's) libs. *)
Dd.initialize 0 options.cudd_heap_init ;
try main_loop 1 s n p rif Lurette_stub.sut_out_init main_loop 1 s n p rif Lurette_stub.sut_out_init ;
with Failure(errmsg) -> print_string errmsg
| e -> raise e ;
flush stdout; flush stdout;
flush rif; flush rif;
...@@ -260,17 +295,17 @@ and ...@@ -260,17 +295,17 @@ and
(* Decides whether to loop once more *) (* Decides whether to loop once more *)
let str = let str =
if (step_by_step) then ( if (options.step_by_step) then (
Show_env.generate_env_graph [] "environment" ; Show_env.generate_env_graph [] "environment" ;
Sim2chro.put_current_step_values Sim2chro.put_current_step_values
stdout t input output env_state.local display_local_var; stdout t input output env_state.local options.display_local_var;
print_string print_string
"\nOne more loop ? [type any char to stop, `CR' to continue]\n"; "\nOne more loop ? [type any char to stop, `CR' to continue]\n";
read_line () read_line ()
) )
else ( else (
Sim2chro.put_current_step_values Sim2chro.put_current_step_values
rif t input output env_state.local display_local_var; rif t input output env_state.local options.display_local_var;
"" ""
) )
in in
......
...@@ -326,6 +326,6 @@ let (solve_formula: int -> formula list -> var_name list -> (subst list * subst ...@@ -326,6 +326,6 @@ let (solve_formula: int -> formula list -> var_name list -> (subst list * subst
let f = formula_list_to_conj fl in let f = formula_list_to_conj fl in
let bdd = Hashtbl.find env_state.bdd_tbl f in let bdd = Hashtbl.find env_state.bdd_tbl f in
let snt = (Hashtbl.create 1) in let snt = (Hashtbl.create 1) in
let _ = build_sol_nb_table bdd snt support in let _ = build_sol_nb_table bdd snt support in
Util.unfold (draw_and_split) (bdd, snt) p Util.unfold (draw_and_split) (bdd, snt) p
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment